1.1 --- a/src/Tools/isac/Interpret/calchead.sml Fri Jul 15 10:17:51 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Fri Jul 15 13:51:50 2011 +0200
1.3 @@ -1724,17 +1724,16 @@
1.4 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1.5 fun all_modspec (pt, (p,_):pos') =
1.6 let
1.7 - val (PblObj{fmz=(fmz_,_), origin=(pors, spec as (dI,pI,mI), hdl),
1.8 - ...}) = get_obj I pt p;
1.9 + val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
1.10 val thy = assoc_thy dI;
1.11 - val {ppc,...} = get_met mI;
1.12 + val {ppc, ...} = get_met mI;
1.13 val mors = prep_ori fmz_ thy ppc |> #1;
1.14 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1.15 val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
1.16 val pt = update_spec pt p (dI,pI,mI);
1.17 in (pt, (p,Met): pos') end;
1.18
1.19 -(*WN.12.03: use in nxt_spec, too ? what about variants ???*)
1.20 +(*WN0312: use in nxt_spec, too ? what about variants ???*)
1.21 fun is_complete_mod_ ([]: itm list) = false
1.22 | is_complete_mod_ itms =
1.23 foldl and_ (true, (map #3 itms));
2.1 --- a/src/Tools/isac/Interpret/solve.sml Fri Jul 15 10:17:51 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/solve.sml Fri Jul 15 13:51:50 2011 +0200
2.3 @@ -411,12 +411,11 @@
2.4 | (_, c', ptp') => complete_solve auto (c @ c') ptp'
2.5
2.6 and all_solve auto c (ptp as (pt, pos as (p,_)): ptree * pos') =
2.7 - let
2.8 - val (_,_,mI) = get_obj g_spec pt p;
2.9 - val ctxt = get_ctxt pt pos
2.10 - val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt))
2.11 - (e_istate, ctxt) ptp;
2.12 - in complete_solve auto (c @ c') ptp end;
2.13 + let
2.14 + val (_,_,mI) = get_obj g_spec pt p;
2.15 + val ctxt = get_ctxt pt pos
2.16 + val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
2.17 + in complete_solve auto (c @ c') ptp end;
2.18
2.19 fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') =
2.20 if p = ([], Res)
2.21 @@ -452,8 +451,7 @@
2.22 let
2.23 val (_,_,mI) = get_obj g_spec pt p
2.24 val ctxt = get_ctxt pt pos
2.25 - val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt))
2.26 - (e_istate, ctxt) ptp
2.27 + val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp
2.28 in complete_solve auto (c @ c') ptp end;
2.29
2.30 (* aux.fun for detailrls with Rrls, reverse rewriting *)
3.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Fri Jul 15 10:17:51 2011 +0200
3.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Fri Jul 15 13:51:50 2011 +0200
3.3 @@ -88,7 +88,7 @@
3.4 Presently, ISAC uses a slightly different representation for terms (which soon
3.5 will disappear), which does not encode numerals as binary numbers:
3.6 *}
3.7 -ML {* val SOME t = parse (theory "Isac") "a + b * 3";
3.8 +ML {* val SOME t = parse @{theory "Isac"} "a + b * 3";
3.9 atomwy (term_of t);
3.10 *}
3.11 text {* From the above we see: the internal representation of a term contains
3.12 @@ -114,7 +114,7 @@
3.13 For instance, in the theory 'HOL' (short for high order logic) even more basic knowledge is
3.14 defined ('=' etc), but not yet '+' and '*', so you get 'NONE':
3.15 *}
3.16 -ML {* parse (theory "HOL") "a + b * 3";
3.17 +ML {* parse @{theory "HOL"} "a + b * 3";
3.18 *}
3.19 text {* ISAC uses comparatively few definitions and theorems from Isabelle, see
3.20 \begin{itemize}
4.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Fri Jul 15 10:17:51 2011 +0200
4.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Fri Jul 15 13:51:50 2011 +0200
4.3 @@ -35,7 +35,7 @@
4.4 ML {*
4.5 print_depth 1;
4.6 val (thy, ro, er, inst) =
4.7 - (theory "Isac", tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
4.8 + (@{theory "Isac"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
4.9 *}
4.10 text {* ... and let us differentiate the term t: *}
4.11 ML {*
4.12 @@ -95,7 +95,7 @@
4.13 Isabelle to show all brackets:
4.14 *}
4.15 ML {*
4.16 -show_brackets := true;
4.17 +(*show_brackets := true; TODO*)
4.18 val t0 = (term_of o the o (parse thy)) "2*a + 3*b + 4*a"; term2str t0;
4.19 (*show_brackets := false;*)
4.20 *}
4.21 @@ -144,7 +144,7 @@
4.22 Here are examples of of how ISAC's simplifier work:
4.23 *}
4.24 ML {*
4.25 -show_brackets := false;
4.26 +(*show_brackets := false; TODO*)
4.27 val t1 = (term_of o the o (parse thy)) "(a - b) * (a^^^2 + a*b + b^^^2)";
4.28 val SOME (t, _) = rewrite_set_ thy true make_polynomial t1; term2str t;
4.29 *}
5.1 --- a/test/Tools/isac/Test_Isac.thy Fri Jul 15 10:17:51 2011 +0200
5.2 +++ b/test/Tools/isac/Test_Isac.thy Fri Jul 15 13:51:50 2011 +0200
5.3 @@ -166,17 +166,43 @@
5.4 (* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*)*)
5.5 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p))) = (auto, (c @ c'), ptp');
5.6 p = ([], Res) (*false p = ([2], Res)*);
5.7 +member op = [Pbl,Met] p_ (*false*);
5.8 val (_, c', ptp') = nxt_solve_ ptp;
5.9 (* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*)*)
5.10 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p))) = (auto, (c @ c'), ptp');
5.11 p = ([], Res) (*false p = ([3], Pbl)*);
5.12 -(*val ((Subproblem _, tac_, (_, is))::_, c', ptp') = nxt_solve_ ptp;
5.13 -(*from_pblobj_or_detail': no istate*)*)
5.14 -
5.15 -(* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*)*)
5.16 +member op = [Pbl,Met] p_ (*true*);
5.17 +(*val ptp = all_modspec ptp; (*WAS Type unification failed...*)*)
5.18 +"~~~~~ fun all_modspec, args:"; val (pt, (p,_):pos') = (ptp);
5.19 *}
5.20 ML {*
5.21 -p
5.22 + val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
5.23 + val thy = assoc_thy dI;
5.24 + val {ppc, ...} = get_met mI;
5.25 + *}
5.26 +ML {*
5.27 +fmz_; ppc;
5.28 +*}
5.29 +ML {*
5.30 +*}
5.31 +ML {*
5.32 +(* val (mors, ctxt) = prep_ori fmz_ thy ppc; *)
5.33 +*}
5.34 +ML {*
5.35 +*}
5.36 +ML {*
5.37 +*}
5.38 +ML {*
5.39 +*}
5.40 +ML {*
5.41 +*}
5.42 +ML {*
5.43 +*}
5.44 +ML {*
5.45 +*}
5.46 +ML {*
5.47 +
5.48 +
5.49 *}
5.50 ML {*
5.51 *}