1.1 --- a/src/Tools/isac/CalcElements/libraryC.sml Sun Feb 09 12:48:18 2020 +0100
1.2 +++ b/src/Tools/isac/CalcElements/libraryC.sml Sun Feb 09 16:21:26 2020 +0100
1.3 @@ -14,7 +14,7 @@
1.4
1.5 infix 1 ~~~
1.6
1.7 -signature LIBRARYC =
1.8 +signature LIBRARY_C =
1.9 sig
1.10 val and_: bool * bool -> bool
1.11 val cand_: bool -> bool -> bool
1.12 @@ -98,7 +98,7 @@
1.13 end;
1.14
1.15 (**)
1.16 -structure LibraryC(*: RULE*) =
1.17 +structure LibraryC(**): LIBRARY_C(**) =
1.18 struct
1.19 (**)
1.20
2.1 --- a/src/Tools/isac/Interpret/li-tool.sml Sun Feb 09 12:48:18 2020 +0100
2.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Sun Feb 09 16:21:26 2020 +0100
2.3 @@ -36,7 +36,6 @@
2.4 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.5 (*NONE*)
2.6 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.7 - val is_spec_pos : Ctree.pos_ -> bool
2.8 val itms2args : 'a -> Celem.metID -> Model.itm list -> term list
2.9 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.10
2.11 @@ -100,7 +99,7 @@
2.12 in (implode o scan o Symbol.explode) str end;
2.13
2.14 fun init_form thy (Rule.Prog sc) env =
2.15 - (case Prog_Tac.get_stac thy sc of NONE => NONE | SOME stac => SOME (subst_atomic env stac))
2.16 + (case Prog_Tac.get_first thy sc of NONE => NONE | SOME stac => SOME (subst_atomic env stac))
2.17 | init_form _ _ _ = error "init_form: no match";
2.18
2.19 type dsc = typ; (* <-> nam..unknow in Descript.thy *)
2.20 @@ -529,17 +528,7 @@
2.21 else (srls(*..\<in> is*), get_loc pt (p,p_), scr)
2.22 end;
2.23
2.24 -(*.get the stactics and problems of a script as tacs
2.25 - instantiated with the current environment;
2.26 - l is the location which generated the given formula.*)
2.27 -(*WN.12.5.03: quick-and-dirty repair for listexpressions*)
2.28 -fun is_spec_pos Pbl = true
2.29 - | is_spec_pos Met = true
2.30 - | is_spec_pos _ = false;
2.31 -
2.32 -(* handle a leaf at the end of recursive descent:
2.33 - a leaf is either a tactic or an 'expr' in "let v = expr"
2.34 - where "expr" does not contain a tactic.
2.35 +(* handle a leaf at the end of recursive descent; a leaf is either a Prog_Tac or an Prog_Expr.
2.36 Handling a leaf comprises
2.37 (1) 'subst_stacexpr' substitute Env.update and complete curried tactic
2.38 (2) rewrite the leaf by 'srls'
2.39 @@ -563,14 +552,14 @@
2.40 (if (! trace_script)
2.41 then tracing("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> Expr '" ^ Rule.term2str lexpr' ^ "'")
2.42 else ();
2.43 - (Program.Expr lexpr', a')) (*lexpr' is the value of the Expr*)
2.44 + (Program.Expr lexpr', a'))
2.45 end;
2.46
2.47 (*. fetch _all_ tactics from script .*)
2.48 -fun sel_rules _ (([],Res):pos') =
2.49 +fun sel_rules _ ([], Res) =
2.50 raise PTREE "no tactics applicable at the end of a calculation"
2.51 | sel_rules pt (p,p_) =
2.52 - if is_spec_pos p_
2.53 + if Pos.on_specification p_
2.54 then [get_obj g_tac pt p]
2.55 else
2.56 let
2.57 @@ -592,7 +581,7 @@
2.58 fun sel_appl_atomic_tacs _ (([], Res) : pos') =
2.59 raise PTREE "no tactics applicable at the end of a calculation"
2.60 | sel_appl_atomic_tacs pt (p, p_) =
2.61 - if is_spec_pos p_
2.62 + if Pos.on_specification p_
2.63 then [get_obj g_tac pt p]
2.64 else
2.65 let
3.1 --- a/src/Tools/isac/MathEngBasic/position.sml Sun Feb 09 12:48:18 2020 +0100
3.2 +++ b/src/Tools/isac/MathEngBasic/position.sml Sun Feb 09 16:21:26 2020 +0100
3.3 @@ -28,7 +28,7 @@
3.4 val start_new_level: pos' -> pos'
3.5 val next_in_prog': pos' -> pos'
3.6 val next_in_prog: pos' -> pos
3.7 -
3.8 + val on_specification : pos_ -> bool
3.9
3.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.11 val pos's2str: pos' list -> string
3.12 @@ -123,4 +123,10 @@
3.13 | next_in_prog (p, Res) = lev_on p
3.14 | next_in_prog pos = raise ERROR ("Step_Solve.by_tactic: call by " ^ pos'2str pos);
3.15
3.16 +(*WN.12.5.03: quick-and-dirty repair for listexpressions*)
3.17 +fun on_specification Pbl = true
3.18 + | on_specification Met = true
3.19 + | on_specification _ = false;
3.20 +
3.21 +
3.22 end
4.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Sun Feb 09 12:48:18 2020 +0100
4.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Sun Feb 09 16:21:26 2020 +0100
4.3 @@ -58,8 +58,8 @@
4.4 signature PROGAM_TACTIC =
4.5 sig
4.6 val dest_spec : term -> Celem.spec
4.7 - val get_stac : 'a -> term -> term option (*rename get_first*)
4.8 - val eval_leaf: (term * term) list -> term option -> term -> term -> Program.leaf * term option
4.9 + val get_first : 'a -> term -> term option (*rename get_first*)
4.10 + val eval_leaf: Env.T -> term option -> term -> term -> Program.leaf * term option
4.11 val is: term -> bool
4.12 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.13 (*NONE*)
4.14 @@ -80,7 +80,7 @@
4.15 | dest_spec t = raise TERM ("dest_spec: called with ", [t])
4.16
4.17 (* get argument of first Prog_Tac in a progam for init_form *)
4.18 -fun get_stac thy (_ $ body) =
4.19 +fun get_first thy (_ $ body) =
4.20 let
4.21 (* entries occur twice, for form curried by #> or non-curried *)
4.22 fun get_t y (Const ("Tactical.Chain",_) $ e1 $ e2) a =
4.23 @@ -120,19 +120,19 @@
4.24
4.25 | get_t _ _ _ = ((*tracing ("### get_t yac: list-expr "^(term2str x));*) NONE)
4.26 in get_t thy body Rule.e_term end
4.27 - | get_stac _ t = error ("get_stac: no fun-def. for " ^ Rule.term2str t);
4.28 + | get_first _ t = error ("get_first: no fun-def. for " ^ Rule.term2str t);
4.29
4.30 (* substitute the Istate.T's environment to a leaf of the program
4.31 and attach the curried argument of a tactic, if any.
4.32 CAUTION: (1) currying with #> requires 2 patterns for each tactic
4.33 (2) the non-curried version must return NONE for a
4.34 - (3) non-matching patterns become an Program.Expr by fall-through.
4.35 + (3) non-matching patterns become a Prog_Expr by fall-through.
4.36 WN060906 quick and dirty fix: due to (2) a is returned, too *)
4.37 fun eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite"(*1*), _) $ _ $ _)) =
4.38 (Program.Tac (subst_atomic E t), NONE)
4.39 | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite"(*2*), _) $ _)) =
4.40 (Program.Tac (
4.41 - case a of SOME a' => (subst_atomic E (t $ a'))
4.42 + case a of SOME a' => (subst_atomic E (t $ a'))
4.43 | NONE => ((subst_atomic E t) $ v)),
4.44 a)
4.45 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite'_Inst"(*1*), _) $ _ $ _ $ _)) =
5.1 --- a/src/Tools/isac/TODO.thy Sun Feb 09 12:48:18 2020 +0100
5.2 +++ b/src/Tools/isac/TODO.thy Sun Feb 09 16:21:26 2020 +0100
5.3 @@ -34,36 +34,21 @@
5.4 \item xxx
5.5 \item xxx
5.6 \item xxx
5.7 - \item reformat + rename "fun eval_leaf"+"fun get_stac"
5.8 - (*1*)(*2*)
5.9 - ?consistency with subst term?
5.10 - \item Tactic.Rewrite*': drop "bool"
5.11 \item xxx
5.12 \item xxx
5.13 - \item Prog_Tac: fun get_stac takes both Prog_Tac + Program --- wait for separate Tactical
5.14 - then shift into common descendant
5.15 - rename get_stac --> ?ptac?
5.16 \item xxx
5.17 \item xxx
5.18 \item /-------------------------------------------------------------------
5.19 \item check occurences of KEStore_Elems.add_rlss [("list_rls",
5.20 - \item rename list_rls accordingly
5.21 + \item rename list_rls accordingly ?prog_expr?
5.22 \item ------------------------------------------------------------------/
5.23 \item xxx
5.24 \item xxx
5.25 - \item signature LIBRARY_C
5.26 - \item Program.thy (*=========== record these ^^^ in 'tacs' in program.ML =========*)
5.27 - \item sig/struc ..elems --> elem
5.28 - \item xxx
5.29 - \item xxx
5.30 - \end{itemize}
5.31 \item xxx
5.32 \item xxx
5.33 - \item distribute test/../scrtools.sml
5.34 + \item distribute test/../scrtools.sml: WAIT FOR FINAL CLEANUP OF src/../Interpret
5.35 \item xxx
5.36 \item xxx
5.37 - \item simplify calls of scan_dn1, scan_dn etc
5.38 - \item open Istate in LI
5.39 \end{itemize}
5.40 \<close>
5.41 subsection \<open>Postponed from current changeset\<close>
5.42 @@ -173,6 +158,7 @@
5.43 \item xxx
5.44 \item exception PROG analogous to TERM
5.45 \item xxx
5.46 + \item sig/struc ..elems --> ..elem
5.47 \item xxx
5.48 \item xxx
5.49 \item xxx
5.50 @@ -319,6 +305,7 @@
5.51 text \<open>
5.52 \begin{itemize}
5.53 \item xxx
5.54 + \item xxx
5.55 \item re-organise code for Interpret
5.56 \begin{itemize}
5.57 \item Step*:
5.58 @@ -355,6 +342,8 @@
5.59 INTERMEDIATE STEP: Step.do_next is still Math_Engine.do_next
5.60 \end{itemize}
5.61 \item xxx
5.62 + \item Prog_Tac: fun get_first takes both Prog_Tac + Program --- wait for separate Tactical
5.63 + then shift into common descendant
5.64 \item xxx
5.65 \end{itemize}
5.66 \item xxx
6.1 --- a/test/Tools/isac/BridgeLibisabelle/interface.sml Sun Feb 09 12:48:18 2020 +0100
6.2 +++ b/test/Tools/isac/BridgeLibisabelle/interface.sml Sun Feb 09 16:21:26 2020 +0100
6.3 @@ -3,19 +3,19 @@
6.4 Use is subject to license terms.
6.5 *)
6.6
6.7 -"-----------------------------------------------------------------------------";
6.8 -"-----------------------------------------------------------------------------";
6.9 -"table of contents -----------------------------------------------------------";
6.10 -"-----------------------------------------------------------------------------";
6.11 -"-------- test_applyFormula --------------------------------------------------";
6.12 +"-----------------------------------------------------------------------------------------------";
6.13 +"table of contents -----------------------------------------------------------------------------";
6.14 +"-----------------------------------------------------------------------------------------------";
6.15 +"-----------------------------------------------------------------------------------------------";
6.16 +"-------- test_applyFormula --------------------------------------------------------------------";
6.17 +"-------- get_interval from ctree with move_dn:modspec.sml -------------------";
6.18 "-----------------------------------------------------------------------------";
6.19 "-----------------------------------------------------------------------------";
6.20
6.21
6.22 -"-------- TODO ---------------------------------------------------------------";
6.23 -"-------- TODO ---------------------------------------------------------------";
6.24 -"-------- TODO ---------------------------------------------------------------";
6.25 -
6.26 +"-------- test_applyFormula --------------------------------------------------------------------";
6.27 +"-------- test_applyFormula --------------------------------------------------------------------";
6.28 +"-------- test_applyFormula --------------------------------------------------------------------";
6.29 "----- this shows the principle how Isac's math-engine is made parallel ------";
6.30 (* a store of simplified states *)
6.31 val test_states = Unsynchronized.ref ([]: (int * string list) list)
6.32 @@ -44,4 +44,191 @@
6.33
6.34 val cI = 123;
6.35 test_upd_calc cI ["initialize 123"];
6.36 -appendFormula cI;
6.37 \ No newline at end of file
6.38 +appendFormula cI;
6.39 +
6.40 +"-------- get_interval from ctree with move_dn:modspec.sml -------------------";
6.41 +"-------- get_interval from ctree with move_dn:modspec.sml -------------------";
6.42 +"-------- get_interval from ctree with move_dn:modspec.sml -------------------";
6.43 +"=====new ctree 1: crippled by cut_level_'_ ======================";
6.44 +reset_states ();
6.45 +CalcTree
6.46 +[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
6.47 + "solveFor x","solutions L"],
6.48 + ("RatEq",["univariate","equation"],["no_met"]))];
6.49 +Iterator 1; moveActiveRoot 1;
6.50 +autoCalculate 1 CompleteCalc;
6.51 +
6.52 +getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*)
6.53 +getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*)
6.54 +getTactic 1 ([3],Res);(*Rewrite_Set RatEq_eliminate*)
6.55 +getTactic 1 ([4,1],Res);(*Rewrite all_left*)
6.56 +getTactic 1 ([4,2],Res);(*Rewrite_Set expand_binoms*)
6.57 +getTactic 1 ([4,3],Res);(*Rewrite_Set_Inst make_ratpoly_in*)
6.58 +
6.59 +moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
6.60 +moveActiveFormula 1 ([2],Res)(**ME_Isa: 'expand' not known*);
6.61 +moveActiveFormula 1 ([3],Res)(*3.1.*);
6.62 +moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
6.63 +moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Program Stepwise t_=*);
6.64 +
6.65 +moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
6.66 +interSteps 1 ([1],Res)(*..is activeFormula !?!*);
6.67 +
6.68 +getTactic 1 ([1,1],Res);(*Rewrite real_diff_minus*)
6.69 +getTactic 1 ([1,2],Res);(*Rewrite real_diff_minus*)
6.70 +getTactic 1 ([1,3],Res);(*Rewrite real_diff_minus*)
6.71 +getTactic 1 ([1,4],Res);(*Rewrite real_rat_mult_1*)
6.72 +
6.73 +moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
6.74 +interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
6.75 +val ((pt,_),_) = get_calc 1;
6.76 +writeln(pr_ctree pr_short pt);
6.77 +(*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
6.78 + ###########################################################################*)
6.79 +val (pt, _) = cut_level_'_ [] [] pt ([4,1],Frm); (*#*)
6.80 +(*##########################################################################*)
6.81 +writeln(pr_ctree pr_short pt);
6.82 +(*##########################################################################
6.83 + attention: the ctree in states is still the old (perfect) !!!
6.84 +############################################################################*)
6.85 +
6.86 +writeln(pr_ctree pr_short pt);
6.87 +writeln(posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
6.88 +
6.89 +case map fst3 (get_interval ([],Frm) ([],Res) 99999 pt) of
6.90 + [([], Frm),
6.91 + ([1], Frm),
6.92 + ([1, 1], Frm),
6.93 + ([1, 1], Res),
6.94 + ([1, 2], Res),
6.95 + ([1, 3], Res),
6.96 + ([1, 4], Res),
6.97 + ([1], Res),
6.98 + ([2], Res),
6.99 + ([3], Res),
6.100 + ([4], Pbl),
6.101 + ([4, 1], Frm),
6.102 + ([4, 1, 1], Frm),
6.103 + ([4, 1, 1], Res),
6.104 + ([4, 1], Res),
6.105 + ([4, 2], Res),
6.106 + ([4, 3], Pbl),
6.107 + ([4, 3, 1], Frm),
6.108 + ([4, 3, 1], Res),
6.109 + ([4, 3, 2], Res),
6.110 + ([4, 3, 3], Res),
6.111 + ([4, 3, 4], Res),
6.112 + ([4, 3, 5], Res),
6.113 + ([4, 3], Res),
6.114 + ([4], Res),
6.115 + ([5], Res),
6.116 + ([], Res)] => ()
6.117 + | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";
6.118 +case map fst3 (get_interval ([],Frm) ([],Res) 1 pt) of
6.119 + [([], Frm),
6.120 + ([1], Frm),
6.121 + ([1], Res),
6.122 + ([2], Res),
6.123 + ([3], Res),
6.124 + ([4], Pbl),
6.125 + ([4], Res),
6.126 + ([5], Res),
6.127 + ([], Res)] => ()
6.128 + | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";
6.129 +case map fst3 (get_interval ([],Frm) ([],Res) 0 pt) of
6.130 + [([], Frm),
6.131 + ([], Res)] => ()
6.132 + | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";
6.133 +
6.134 +case map fst3 (get_interval ([1,3],Res) ([4,1,1],Frm) 99999 pt) of
6.135 + [([1, 3], Res),
6.136 + ([1, 4], Res),
6.137 + ([1], Res),
6.138 + ([2], Res),
6.139 + ([3], Res),
6.140 + ([4], Pbl),
6.141 + ([4, 1], Frm),
6.142 + ([4, 1, 1], Frm)] => ()
6.143 + | _ => error "diff.behav.in ctree.sml: get_interval lev 1a";
6.144 +
6.145 +(*this pos' is not generated bu move_dn:......vvv: goes to end of calc*)
6.146 +case map fst3 (get_interval ([2],Res) ([4,3,2],Frm) 99999 pt) of
6.147 + [([2], Res),
6.148 + ([3], Res),
6.149 + ([4], Pbl),
6.150 + ([4, 1], Frm),
6.151 + ([4, 1, 1], Frm),
6.152 + ([4, 1, 1], Res),
6.153 + ([4, 1], Res),
6.154 + ([4, 2], Res),
6.155 + ([4, 3], Pbl),
6.156 + ([4, 3, 1], Frm),
6.157 + ([4, 3, 1], Res),
6.158 + ([4, 3, 2], Res),
6.159 + ([4, 3, 3], Res),(*this is beyond 'to'*)
6.160 + ([4, 3, 4], Res),(*this is beyond 'to'*)
6.161 + ([4, 3, 5], Res),(*this is beyond 'to'*)
6.162 + ([4, 3], Res), (*this is beyond 'to'*)
6.163 + ([4], Res), (*this is beyond 'to'*)
6.164 + ([5], Res), (*this is beyond 'to'*)
6.165 + ([], Res)] => () (*this is beyond 'to'*)
6.166 + | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";
6.167 +case map fst3 (get_interval ([1,4],Res) ([4,3,1],Frm) 99999 pt) of
6.168 + [([1, 4], Res),
6.169 + ([1], Res),
6.170 + ([2], Res),
6.171 + ([3], Res),
6.172 + ([4], Pbl),
6.173 + ([4, 1], Frm),
6.174 + ([4, 1, 1], Frm),
6.175 + ([4, 1, 1], Res),
6.176 + ([4, 1], Res),
6.177 + ([4, 2], Res),
6.178 + ([4, 3], Pbl),
6.179 + ([4, 3, 1], Frm)] => ()
6.180 + | _ => error "diff.behav.in ctree.sml: get_interval lev 1c";
6.181 +case map fst3 (get_interval ([4,2],Res) ([5],Res) 99999 pt) of
6.182 + [([4, 2], Res),
6.183 + ([4, 3], Pbl),
6.184 + ([4, 3, 1], Frm),
6.185 + ([4, 3, 1], Res),
6.186 + ([4, 3, 2], Res),
6.187 + ([4, 3, 3], Res),
6.188 + ([4, 3, 4], Res),
6.189 + ([4, 3, 5], Res),
6.190 + ([4, 3], Res),
6.191 + ([4], Res),
6.192 + ([5], Res)]=>()
6.193 + | _ => error "diff.behav.in ctree.sml: get_interval lev 1d";
6.194 +case map fst3 (get_interval ([],Frm) ([4,3,2],Res) 99999 pt) of
6.195 + [([], Frm),
6.196 + ([1], Frm),
6.197 + ([1, 1], Frm),
6.198 + ([1, 1], Res),
6.199 + ([1, 2], Res),
6.200 + ([1, 3], Res),
6.201 + ([1, 4], Res),
6.202 + ([1], Res),
6.203 + ([2], Res),
6.204 + ([3], Res),
6.205 + ([4], Pbl),
6.206 + ([4, 1], Frm),
6.207 + ([4, 1, 1], Frm),
6.208 + ([4, 1, 1], Res),
6.209 + ([4, 1], Res),
6.210 + ([4, 2], Res),
6.211 + ([4, 3], Pbl),
6.212 + ([4, 3, 1], Frm),
6.213 + ([4, 3, 1], Res),
6.214 + ([4, 3, 2], Res)] => ()
6.215 + | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
6.216 +case map fst3 (get_interval ([4,3],Frm) ([4,3],Res) 99999 pt) of
6.217 + [([4, 3], Frm),
6.218 + ([4, 3, 1], Frm),
6.219 + ([4, 3, 1], Res),
6.220 + ([4, 3, 2], Res),
6.221 + ([4, 3, 3], Res),
6.222 + ([4, 3, 4], Res),
6.223 + ([4, 3, 5], Res),
6.224 + ([4, 3], Res)] => ()
6.225 + | _ => error "diff.behav.in ctree.sml: get_interval lev 1g";
7.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sun Feb 09 12:48:18 2020 +0100
7.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sun Feb 09 16:21:26 2020 +0100
7.3 @@ -1386,7 +1386,7 @@
7.4 if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
7.5 error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
7.6 (* for getting the list in whole length ...
7.7 -(*default_print_depth 99*) map fst (get_interval ([1],Res) ([],Res) 9999 pt); (*default_print_depth 3*)
7.8 +(*default_print_depth 99*) map fst3 (get_interval ([1],Res) ([],Res) 9999 pt); (*default_print_depth 3*)
7.9 *)
7.10 if map fst3 (get_interval ([1],Res) ([],Res) 9999 pt) =
7.11 [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
8.1 --- a/test/Tools/isac/Interpret/li-tool.sml Sun Feb 09 12:48:18 2020 +0100
8.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Sun Feb 09 16:21:26 2020 +0100
8.3 @@ -6,7 +6,7 @@
8.4 "table of contents -----------------------------------------------";
8.5 "-----------------------------------------------------------------";
8.6 "----------- fun sel_appl_atomic_tacs ----------------------------";
8.7 -"----------- fun init_form, fun get_stac -------------------------";
8.8 +"----------- fun init_form, fun get_first -------------------------";
8.9 "----------- fun sel_rules ---------------------------------------";
8.10 "----------- fun sel_appl_atomic_tacs ----------------------------";
8.11 "----------- fun de_esc_underscore -------------------------------";
8.12 @@ -91,9 +91,9 @@
8.13 autoCalculate 1 CompleteCalc; (* ONE ERROR *)
8.14 ==============================^^^^^^^^^^^^^*)
8.15
8.16 -"----------- fun init_form, fun get_stac -------------------------";
8.17 -"----------- fun init_form, fun get_stac -------------------------";
8.18 -"----------- fun init_form, fun get_stac -------------------------";
8.19 +"----------- fun init_form, fun get_first -------------------------";
8.20 +"----------- fun init_form, fun get_first -------------------------";
8.21 +"----------- fun init_form, fun get_first -------------------------";
8.22 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
8.23 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
8.24 ["Test","squ-equ-test-subpbl1"]);
8.25 @@ -120,8 +120,8 @@
8.26 val (is as Pstate {env, ...}, ctxt, sc) = init_pstate srls ctxt itms mI;
8.27 val ini = init_form thy sc env;
8.28 "----- fun init_form, args:"; val (Prog sc) = sc;
8.29 -"----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
8.30 -case get_stac thy sc of SOME (Free ("e_e", _)) => ()
8.31 +"----- fun get_first, args:"; val (y, h $ body) = (thy, sc);
8.32 +case get_first thy sc of SOME (Free ("e_e", _)) => ()
8.33 | _ => error "script: Const (?, ?) in script (as term) changed";;
8.34
8.35 "----------- fun sel_rules ---------------------------------------";
8.36 @@ -200,7 +200,7 @@
8.37 *)
8.38
8.39 "~~~~~ fun sel_appl_atomic_tacs , args:"; val (pt, (p, p_)) = (pt, p);
8.40 -is_spec_pos p_ = false;
8.41 +Pos.on_specification p_ = false;
8.42 val pp = par_pblobj pt p
8.43 val thy' = (get_obj g_domID pt pp):theory'
8.44 val thy = assoc_thy thy'
9.1 --- a/test/Tools/isac/Interpret/me.sml Sun Feb 09 12:48:18 2020 +0100
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,532 +0,0 @@
9.4 -(* tests on me.sml
9.5 - author: Walther Neuper
9.6 - 060225,
9.7 - (c) due to copyright terms
9.8 -
9.9 -use"../smltest/ME/me.sml";
9.10 -use"me.sml";
9.11 -*)
9.12 -
9.13 -"-----------------------------------------------------------------";
9.14 -"table of contents -----------------------------------------------";
9.15 -"-----------------------------------------------------------------";
9.16 -"=====new ctree 1: crippled by cut_level_'_ ======================";
9.17 -"-------------- get_interval from ctree with move_dn:modspec.sml -";
9.18 -"=====new ctree 2 without changes ================================";
9.19 -"-------------- getFormulaeFromTo --------------------------------";
9.20 -"autoCalculate";
9.21 -"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
9.22 -"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
9.23 -"--------- maximum-example: complete_metitms ---------------------";
9.24 -"--------- maximum-example: complete_mod -------------------------";
9.25 -"-----------------------------------------------------------------";
9.26 -"-----------------------------------------------------------------";
9.27 -"-----------------------------------------------------------------";
9.28 -
9.29 -
9.30 -
9.31 -"=====new ctree 1: crippled by cut_level_'_ ======================";
9.32 -"=====new ctree 1: crippled by cut_level_'_ ======================";
9.33 -"=====new ctree 1: crippled by cut_level_'_ ======================";
9.34 -reset_states ();
9.35 -CalcTree
9.36 -[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
9.37 - "solveFor x","solutions L"],
9.38 - ("RatEq",["univariate","equation"],["no_met"]))];
9.39 -Iterator 1; moveActiveRoot 1;
9.40 -autoCalculate 1 CompleteCalc;
9.41 -
9.42 -getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*)
9.43 -getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*)
9.44 -getTactic 1 ([3],Res);(*Rewrite_Set RatEq_eliminate*)
9.45 -getTactic 1 ([4,1],Res);(*Rewrite all_left*)
9.46 -getTactic 1 ([4,2],Res);(*Rewrite_Set expand_binoms*)
9.47 -getTactic 1 ([4,3],Res);(*Rewrite_Set_Inst make_ratpoly_in*)
9.48 -
9.49 -moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
9.50 -moveActiveFormula 1 ([2],Res)(**ME_Isa: 'expand' not known*);
9.51 -moveActiveFormula 1 ([3],Res)(*3.1.*);
9.52 -moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
9.53 -moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Program Stepwise t_=*);
9.54 -
9.55 -moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
9.56 -interSteps 1 ([1],Res)(*..is activeFormula !?!*);
9.57 -
9.58 -getTactic 1 ([1,1],Res);(*Rewrite real_diff_minus*)
9.59 -getTactic 1 ([1,2],Res);(*Rewrite real_diff_minus*)
9.60 -getTactic 1 ([1,3],Res);(*Rewrite real_diff_minus*)
9.61 -getTactic 1 ([1,4],Res);(*Rewrite real_rat_mult_1*)
9.62 -
9.63 -moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
9.64 -interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
9.65 -val ((pt,_),_) = get_calc 1;
9.66 -writeln(pr_ctree pr_short pt);
9.67 -(*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
9.68 - ###########################################################################*)
9.69 -val (pt, _) = cut_level_'_ [] [] pt ([4,1],Frm); (*#*)
9.70 -(*##########################################################################*)
9.71 -writeln(pr_ctree pr_short pt);
9.72 -(*##########################################################################
9.73 - attention: the ctree in states is still the old (perfect) !!!
9.74 -############################################################################*)
9.75 -
9.76 -
9.77 -
9.78 -"-------------- get_interval from ctree with move_dn:modspec.sml -";
9.79 -"-------------- get_interval from ctree with move_dn:modspec.sml -";
9.80 -"-------------- get_interval from ctree with move_dn:modspec.sml -";
9.81 -writeln(pr_ctree pr_short pt);
9.82 -writeln(posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
9.83 -
9.84 -case map fst (get_interval ([],Frm) ([],Res) 99999 pt) of
9.85 - [([], Frm),
9.86 - ([1], Frm),
9.87 - ([1, 1], Frm),
9.88 - ([1, 1], Res),
9.89 - ([1, 2], Res),
9.90 - ([1, 3], Res),
9.91 - ([1, 4], Res),
9.92 - ([1], Res),
9.93 - ([2], Res),
9.94 - ([3], Res),
9.95 - ([4], Pbl),
9.96 - ([4, 1], Frm),
9.97 - ([4, 1, 1], Frm),
9.98 - ([4, 1, 1], Res),
9.99 - ([4, 1], Res),
9.100 - ([4, 2], Res),
9.101 - ([4, 3], Pbl),
9.102 - ([4, 3, 1], Frm),
9.103 - ([4, 3, 1], Res),
9.104 - ([4, 3, 2], Res),
9.105 - ([4, 3, 3], Res),
9.106 - ([4, 3, 4], Res),
9.107 - ([4, 3, 5], Res),
9.108 - ([4, 3], Res),
9.109 - ([4], Res),
9.110 - ([5], Res),
9.111 - ([], Res)] => ()
9.112 - | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";
9.113 -case map fst (get_interval ([],Frm) ([],Res) 1 pt) of
9.114 - [([], Frm),
9.115 - ([1], Frm),
9.116 - ([1], Res),
9.117 - ([2], Res),
9.118 - ([3], Res),
9.119 - ([4], Pbl),
9.120 - ([4], Res),
9.121 - ([5], Res),
9.122 - ([], Res)] => ()
9.123 - | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";
9.124 -case map fst (get_interval ([],Frm) ([],Res) 0 pt) of
9.125 - [([], Frm),
9.126 - ([], Res)] => ()
9.127 - | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";
9.128 -
9.129 -case map fst (get_interval ([1,3],Res) ([4,1,1],Frm) 99999 pt) of
9.130 - [([1, 3], Res),
9.131 - ([1, 4], Res),
9.132 - ([1], Res),
9.133 - ([2], Res),
9.134 - ([3], Res),
9.135 - ([4], Pbl),
9.136 - ([4, 1], Frm),
9.137 - ([4, 1, 1], Frm)] => ()
9.138 - | _ => error "diff.behav.in ctree.sml: get_interval lev 1a";
9.139 -
9.140 -(*this pos' is not generated bu move_dn:......vvv: goes to end of calc*)
9.141 -case map fst (get_interval ([2],Res) ([4,3,2],Frm) 99999 pt) of
9.142 - [([2], Res),
9.143 - ([3], Res),
9.144 - ([4], Pbl),
9.145 - ([4, 1], Frm),
9.146 - ([4, 1, 1], Frm),
9.147 - ([4, 1, 1], Res),
9.148 - ([4, 1], Res),
9.149 - ([4, 2], Res),
9.150 - ([4, 3], Pbl),
9.151 - ([4, 3, 1], Frm),
9.152 - ([4, 3, 1], Res),
9.153 - ([4, 3, 2], Res),
9.154 - ([4, 3, 3], Res),(*this is beyond 'to'*)
9.155 - ([4, 3, 4], Res),(*this is beyond 'to'*)
9.156 - ([4, 3, 5], Res),(*this is beyond 'to'*)
9.157 - ([4, 3], Res), (*this is beyond 'to'*)
9.158 - ([4], Res), (*this is beyond 'to'*)
9.159 - ([5], Res), (*this is beyond 'to'*)
9.160 - ([], Res)] => () (*this is beyond 'to'*)
9.161 - | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";
9.162 -case map fst (get_interval ([1,4],Res) ([4,3,1],Frm) 99999 pt) of
9.163 - [([1, 4], Res),
9.164 - ([1], Res),
9.165 - ([2], Res),
9.166 - ([3], Res),
9.167 - ([4], Pbl),
9.168 - ([4, 1], Frm),
9.169 - ([4, 1, 1], Frm),
9.170 - ([4, 1, 1], Res),
9.171 - ([4, 1], Res),
9.172 - ([4, 2], Res),
9.173 - ([4, 3], Pbl),
9.174 - ([4, 3, 1], Frm)] => ()
9.175 - | _ => error "diff.behav.in ctree.sml: get_interval lev 1c";
9.176 -case map fst (get_interval ([4,2],Res) ([5],Res) 99999 pt) of
9.177 - [([4, 2], Res),
9.178 - ([4, 3], Pbl),
9.179 - ([4, 3, 1], Frm),
9.180 - ([4, 3, 1], Res),
9.181 - ([4, 3, 2], Res),
9.182 - ([4, 3, 3], Res),
9.183 - ([4, 3, 4], Res),
9.184 - ([4, 3, 5], Res),
9.185 - ([4, 3], Res),
9.186 - ([4], Res),
9.187 - ([5], Res)]=>()
9.188 - | _ => error "diff.behav.in ctree.sml: get_interval lev 1d";
9.189 -case map fst (get_interval ([],Frm) ([4,3,2],Res) 99999 pt) of
9.190 - [([], Frm),
9.191 - ([1], Frm),
9.192 - ([1, 1], Frm),
9.193 - ([1, 1], Res),
9.194 - ([1, 2], Res),
9.195 - ([1, 3], Res),
9.196 - ([1, 4], Res),
9.197 - ([1], Res),
9.198 - ([2], Res),
9.199 - ([3], Res),
9.200 - ([4], Pbl),
9.201 - ([4, 1], Frm),
9.202 - ([4, 1, 1], Frm),
9.203 - ([4, 1, 1], Res),
9.204 - ([4, 1], Res),
9.205 - ([4, 2], Res),
9.206 - ([4, 3], Pbl),
9.207 - ([4, 3, 1], Frm),
9.208 - ([4, 3, 1], Res),
9.209 - ([4, 3, 2], Res)] => ()
9.210 - | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
9.211 -case map fst (get_interval ([4,3],Frm) ([4,3],Res) 99999 pt) of
9.212 - [([4, 3], Frm),
9.213 - ([4, 3, 1], Frm),
9.214 - ([4, 3, 1], Res),
9.215 - ([4, 3, 2], Res),
9.216 - ([4, 3, 3], Res),
9.217 - ([4, 3, 4], Res),
9.218 - ([4, 3, 5], Res),
9.219 - ([4, 3], Res)] => ()
9.220 - | _ => error "diff.behav.in ctree.sml: get_interval lev 1g";
9.221 -
9.222 -
9.223 -
9.224 -
9.225 -"=====new ctree 2 without changes ================================";
9.226 -"=====new ctree 2 without changes ================================";
9.227 -"=====new ctree 2 without changes ================================";
9.228 -reset_states ();
9.229 -CalcTree
9.230 -[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
9.231 - "solveFor x","solutions L"],
9.232 - ("RatEq",["univariate","equation"],["no_met"]))];
9.233 -Iterator 1; moveActiveRoot 1;
9.234 -autoCalculate 1 CompleteCalc;
9.235 -val ((pt,_),_) = get_calc 1;
9.236 -val p = get_pos 1 1;
9.237 -val (Form f, tac, asms) = pt_extract (pt, p);
9.238 -if term2str f = "[x = 6 / 5]" andalso p = ([], Res) then ()
9.239 - else error "after ===new ctree 2 without changes ===";
9.240 -writeln(pr_ctree pr_short pt);
9.241 -
9.242 -
9.243 -"-------------- getFormulaeFromTo --------------------------------";
9.244 -"-------------- getFormulaeFromTo --------------------------------";
9.245 -"-------------- getFormulaeFromTo --------------------------------";
9.246 -getFormulaeFromTo 1 ([4, 2], Res) ([4, 4], Pbl) 000;
9.247 -(*
9.248 -"@@@@@begin@@@@@" //...................................................
9.249 -+ " 1" //..............................................................
9.250 -+ "<GETELEMENTSFROMTO>" //...................................................
9.251 -+ " <CALCID> 1 </CALCID>" //..........................................
9.252 -+ " <POSFORMHEADS>" //................................................
9.253 -+ " <POSFORM>" //...................................................
9.254 -+ " <GENERATED>" //...............................................
9.255 -+ " <INTLIST>" //...............................................
9.256 -+ " <INT> 4 </INT>" //........................................
9.257 -+ " <INT> 3 </INT>" //........................................
9.258 -+ " </INTLIST>" //..............................................
9.259 -+ " <POS> Res </POS>" //........................................
9.260 -+ " </GENERATED>" //..............................................
9.261 -+ " <FORMULA>" //.................................................
9.262 -+ " <MATHML>" //................................................
9.263 -+ " <ISA> -6 * x + 5 * x ^^^ 2 = 0 </ISA>" //.................
9.264 -+ " </MATHML>" //...............................................
9.265 -+ " </FORMULA>" //................................................
9.266 -+ " </POSFORM>" //..................................................
9.267 -+ " <POSHEAD>" //...................................................
9.268 -+ " <GENERATED>" //...............................................
9.269 -+ " <INTLIST>" //...............................................
9.270 -+ " <INT> 4 </INT>" //........................................
9.271 -+ " <INT> 4 </INT>" //........................................
9.272 -+ " </INTLIST>" //..............................................
9.273 -+ " <POS> Pbl </POS>" //........................................
9.274 -+ " </GENERATED>" //..............................................
9.275 -+ " <CALCHEAD status = "correct">" //.............................
9.276 -+ " <HEAD>" //...................................................
9.277 -+ " <MATHML>" //...............................................
9.278 -+ " <ISA> solve (-6 * x + 5 * x ^^^ 2 = 0, x) </ISA>" //.....
9.279 -+ " </MATHML>" //..............................................
9.280 -+ " </HEAD>" //..................................................
9.281 -+ " <MODEL>" //.................................................
9.282 -+ " <GIVEN>" //...............................................
9.283 -+ " <ITEM status="correct">" //.............................
9.284 -+ " <MATHML>" //..........................................
9.285 -+ " <ISA> equality (-6 * x + 5 * x ^^^ 2 = 0) </ISA>" //
9.286 -+ " </MATHML>" //.........................................
9.287 -+ " </ITEM>" //.............................................
9.288 -+ " <ITEM status="correct">" //.............................
9.289 -+ " <MATHML>" //..........................................
9.290 -+ " <ISA> solveFor x </ISA>" //.........................
9.291 -+ " </MATHML>" //.........................................
9.292 -+ " </ITEM>" //.............................................
9.293 -+ " </GIVEN>" //..............................................
9.294 -+ " <WHERE>" //...............................................
9.295 -+ " <ITEM status="correct">" //.............................
9.296 -+ " <MATHML>" //..........................................
9.297 -+ " <ISA> matches (?a * ?v_ + ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"
9.298 -+ "matches (?v_ + ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" //......
9.299 -+ "matches (?v_ + ?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"
9.300 -+ "matches (?a * ?v_ + ?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"
9.301 -+ "matches (?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" //............
9.302 -+ "matches (?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) </ISA>" //..
9.303 -+ " </MATHML>" //.........................................
9.304 -+ " </ITEM>" //.............................................
9.305 -+ " </WHERE>" //..............................................
9.306 -+ " <FIND>" //................................................
9.307 -+ " <ITEM status="correct">" //.............................
9.308 -+ " <MATHML>" //..........................................
9.309 -+ " <ISA> solutions x_i </ISA>" //......................
9.310 -+ " </MATHML>" //.........................................
9.311 -+ " </ITEM>" //.............................................
9.312 -+ " </FIND>" //...............................................
9.313 -+ " <RELATE> </RELATE>" //...................................
9.314 -+ " </MODEL>" //................................................
9.315 -+ " <BELONGSTO> Pbl </BELONGSTO>" //............................
9.316 -+ " <SPECIFICATION>" //.........................................
9.317 -+ " <THEORYID> PolyEq.thy </THEORYID>" //.....................
9.318 -+ " <PROBLEMID>" //...........................................
9.319 -+ " <STRINGLIST>" //........................................
9.320 -+ " <STRING> bdv_only </STRING>" //.......................
9.321 -+ " <STRING> degree_2 </STRING>" //.......................
9.322 -+ " <STRING> polynomial </STRING>" //.....................
9.323 -+ " <STRING> univariate </STRING>" //.....................
9.324 -+ " <STRING> equation </STRING>" //.......................
9.325 -+ " </STRINGLIST>" //.......................................
9.326 -+ " </PROBLEMID>" //..........................................
9.327 -+ " <METHODID>" //............................................
9.328 -+ " <STRINGLIST>" //........................................
9.329 -+ " <STRING> PolyEq </STRING>" //.........................
9.330 -+ " <STRING> solve_d2_polyeq_bdvonly_equation </STRING>"
9.331 -+ " </STRINGLIST>" //.......................................
9.332 -+ " </METHODID>" //...........................................
9.333 -+ " </SPECIFICATION>" //........................................
9.334 -+ " </CALCHEAD>" //...............................................
9.335 -+ " </POSHEAD>" //..................................................
9.336 -+ " <POSFORMHEADS>" //................................................
9.337 -+ "</GETELEMENTSFROMTO>" //..................................................
9.338 -+ "@@@@@end@@@@@"
9.339 -*)
9.340 -
9.341 -
9.342 -"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
9.343 -"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
9.344 -"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
9.345 - val c = [];
9.346 - val (p,_,f,nxt,_,pt) = CalcTreeTEST
9.347 - [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
9.348 - ("Test",
9.349 - ["LINEAR","univariate","equation","test"],
9.350 - ["Test","solve_linear"]))];
9.351 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.352 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.353 - (*xt = Add_Given "solveFor x"*)
9.354 - writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p)));
9.355 -(*[
9.356 -(0 ,[] ,false ,#Given ,Inc solveFor ,(??.empty, [])),
9.357 -(0 ,[] ,false ,#Find ,Inc solutions [] ,(??.empty, [])),
9.358 -(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0]))]*)
9.359 - val (pt,p) = complete_mod (pt, p);
9.360 - if itms2str_ ctxt (get_obj g_pbl pt (fst p)) = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]" then ()
9.361 - else error "completetest.sml: new behav. in complete_mod 1";
9.362 - writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p)));
9.363 -(*[
9.364 -(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
9.365 -(2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
9.366 -(3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)
9.367 - val mits = get_obj g_met pt (fst p);
9.368 - if itms2str_ ctxt mits = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]"
9.369 - then () else error "completetest.sml: new behav. in complete_mod 2";
9.370 - writeln (itms2str_ ctxt mits);
9.371 -(*[
9.372 -(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
9.373 -(2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
9.374 -(3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)
9.375 -
9.376 -
9.377 -
9.378 -"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
9.379 -"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
9.380 -"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
9.381 - reset_states ();
9.382 - CalcTree (*start of calculation, return No.1*)
9.383 - [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
9.384 - ("Test",
9.385 - ["LINEAR","univariate","equation","test"],
9.386 - ["Test","solve_linear"]))];
9.387 - Iterator 1; moveActiveRoot 1;
9.388 -
9.389 -(*
9.390 - autoCalculate 1 CompleteCalcHead;
9.391 - autoCalculate 1 (Steps 1);
9.392 - refFormula 1 (get_pos 1 1);
9.393 -
9.394 -... works
9.395 -
9.396 - autoCalculate 1 CompleteCalcHead;
9.397 - fetchProposedTactic 1; (*-> Apply_Method*);
9.398 - setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
9.399 - autoCalculate 1 (Steps 1);
9.400 - refFormula 1 (get_pos 1 1);
9.401 -
9.402 -... works *)
9.403 -
9.404 - autoCalculate 1 (Steps 1);
9.405 - refFormula 1 (get_pos 1 1);
9.406 -
9.407 - autoCalculate 1 CompleteModel;
9.408 - refFormula 1 (get_pos 1 1);
9.409 -
9.410 - autoCalculate 1 CompleteCalcHead;
9.411 -(* *** complete_mod: only impl.for Pbl, called with ([], Met) FIXXXXXXXXXXME*)
9.412 -
9.413 -
9.414 -
9.415 -"--------- maximum-example: complete_metitms ---------------------";
9.416 -"--------- maximum-example: complete_metitms ---------------------";
9.417 -"--------- maximum-example: complete_metitms ---------------------";
9.418 - val (p,_,f,nxt,_,pt) =
9.419 - CalcTreeTEST
9.420 - [(["fixedValues [r=Arbfix]","maximum A",
9.421 - "valuesFor [a,b]",
9.422 - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
9.423 - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
9.424 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
9.425 -
9.426 - "boundVariable a","boundVariable b","boundVariable alpha",
9.427 - "interval {x::real. 0 <= x & x <= 2*r}",
9.428 - "interval {x::real. 0 <= x & x <= 2*r}",
9.429 - "interval {x::real. 0 <= x & x <= pi}",
9.430 - "errorBound (eps=(0::real))"],
9.431 - ("DiffApp",["maximum_of","function"],["DiffApp","max_by_calculus"])
9.432 - )];
9.433 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.434 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.435 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.436 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.437 - val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;
9.438 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.439 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.440 - (*nxt = Specify_Theory "DiffApp"*)
9.441 - val (oris, _, _) = get_obj g_origin pt (fst p);
9.442 - writeln (oris2str oris);
9.443 -(*[
9.444 -(1, ["1","2","3"], #Given,fixedValues, ["[r = Arbfix]"]),
9.445 -(2, ["1","2","3"], #Find,maximum, ["A"]),
9.446 -(3, ["1","2","3"], #Find,valuesFor, ["[a]","[b]"]),
9.447 -(4, ["1","2"], #Relate,relations, ["[A = a * b]","[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"]),
9.448 -(5, ["3"], #Relate,relations, ["[A = a * b]","[a / 2 = r * sin alpha]","[b / 2 = r * cos alpha]"]),
9.449 -(6, ["1"], #undef,boundVariable, ["a"]),
9.450 -(7, ["2"], #undef,boundVariable, ["b"]),
9.451 -(8, ["3"], #undef,boundVariable, ["alpha"]),
9.452 -(9, ["1","2"], #undef,interval, ["{x. 0 <= x & x <= 2 * r}"]),
9.453 -(10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]),
9.454 -(11, ["1","2","3"], #undef,errorBound, ["eps = 0"])]*)
9.455 - val pits = get_obj g_pbl pt (fst p);
9.456 - writeln (itms2str_ ctxt pits);
9.457 -(*[
9.458 -(1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])),
9.459 -(2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])),
9.460 -(3 ,[1,2,3] ,true,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
9.461 -(4 ,[1,2] ,true,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
9.462 -2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
9.463 - val mits = get_obj g_met pt (fst p);
9.464 - val mits = complete_metitms oris pits []
9.465 - ((#ppc o get_met) ["DiffApp","max_by_calculus"]);
9.466 - writeln (itms2str_ ctxt mits);
9.467 -(*[
9.468 -(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
9.469 -(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
9.470 -(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
9.471 -(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
9.472 -2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
9.473 -(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
9.474 -(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
9.475 -0 <= x & x <= 2 * r}])),
9.476 -(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
9.477 - if itms2str_ ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then ()
9.478 - else error "completetest.sml: new behav. in complete_metitms 1";
9.479 -
9.480 -
9.481 -"--------- maximum-example: complete_mod -------------------------";
9.482 -"--------- maximum-example: complete_mod -------------------------";
9.483 -"--------- maximum-example: complete_mod -------------------------";
9.484 - val (p,_,f,nxt,_,pt) =
9.485 - CalcTreeTEST
9.486 - [(["fixedValues [r=Arbfix]","maximum A",
9.487 - "valuesFor [a,b]",
9.488 - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
9.489 - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
9.490 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
9.491 -
9.492 - "boundVariable a","boundVariable b","boundVariable alpha",
9.493 - "interval {x::real. 0 <= x & x <= 2*r}",
9.494 - "interval {x::real. 0 <= x & x <= 2*r}",
9.495 - "interval {x::real. 0 <= x & x <= pi}",
9.496 - "errorBound (eps=(0::real))"],
9.497 - ("DiffApp",["maximum_of","function"],["DiffApp","max_by_calculus"])
9.498 - )];
9.499 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.500 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.501 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.502 - (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)
9.503 - val pits = get_obj g_pbl pt (fst p);
9.504 - writeln (itms2str_ ctxt pits);
9.505 -(*[
9.506 -(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
9.507 -(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),
9.508 -(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
9.509 -(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)
9.510 - val (pt,p) = complete_mod (pt,p);
9.511 - val pits = get_obj g_pbl pt (fst p);
9.512 - if itms2str_ ctxt pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]"
9.513 - then () else error "completetest.sml: new behav. in complete_mod 3";
9.514 - writeln (itms2str_ ctxt pits);
9.515 -(*[
9.516 -(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
9.517 -(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
9.518 -(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
9.519 -(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
9.520 -2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
9.521 - val mits = get_obj g_met pt (fst p);
9.522 - if itms2str_ ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]"
9.523 - then () else error "completetest.sml: new behav. in complete_mod 3";
9.524 - writeln (itms2str_ ctxt mits);
9.525 -(*[
9.526 -(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
9.527 -(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
9.528 -(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
9.529 -(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
9.530 -2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
9.531 -(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
9.532 -(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
9.533 -0 <= x & x <= 2 * r}])),
9.534 -(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
9.535 -
10.1 --- a/test/Tools/isac/MathEngBasic/ctree.sml Sun Feb 09 12:48:18 2020 +0100
10.2 +++ b/test/Tools/isac/MathEngBasic/ctree.sml Sun Feb 09 16:21:26 2020 +0100
10.3 @@ -30,7 +30,7 @@
10.4 "=====new ctree 3a ===============================================";
10.5 "-------------- move_dn in Incomplete ctree ----------------------";
10.6 "=====new ctree 4: crooked by cut_level_'_ =======================";
10.7 -(*############## development stopped 0501 ########################*)
10.8 +(*//############## development stopped 0501 ########################\\*)
10.9 (******************************************************************)
10.10 (* val SAVE_get_trace = get_trace; *)
10.11 (******************************************************************)
10.12 @@ -38,7 +38,7 @@
10.13 (******************************************************************)
10.14 (* val get_trace = SAVE_get_trace; *)
10.15 (******************************************************************)
10.16 -(*############## development stopped 0501 ########################*)
10.17 +(*\\############## development stopped 0501 ########################//*)
10.18 "=====new ctree 4 ratequation ====================================";
10.19 "-------------- pt_extract form, tac, asm<>[] --------------------";
10.20 "=====new ctree 5 minisubpbl =====================================";
11.1 --- a/test/Tools/isac/OLDTESTS/modspec.sml Sun Feb 09 12:48:18 2020 +0100
11.2 +++ b/test/Tools/isac/OLDTESTS/modspec.sml Sun Feb 09 16:21:26 2020 +0100
11.3 @@ -24,14 +24,14 @@
11.4 val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
11.5 val ((pt,_),_) = get_calc 1;
11.6
11.7 -(*default_print_depth 99;*)map fst (get_interval ([],Pbl) ([],Res) 9999 pt);(*default_print_depth 3;*)
11.8 -if map fst (get_interval ([],Pbl) ([],Res) 9999 pt) =
11.9 +(*default_print_depth 99;*)map fst3 (get_interval ([],Pbl) ([],Res) 9999 pt);(*default_print_depth 3;*)
11.10 +if map fst3 (get_interval ([],Pbl) ([],Res) 9999 pt) =
11.11 [([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm),
11.12 ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
11.13 ([3, 2], Res)] then () else
11.14 error "modspec.sml: diff.behav. get_interval after replace} other 2 a";
11.15
11.16 -(*default_print_depth 99;*)map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); (*default_print_depth 3;*)
11.17 -if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) =
11.18 +(*default_print_depth 99;*)map fst3 (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); (*default_print_depth 3;*)
11.19 +if map fst3 (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) =
11.20 [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else
11.21 error "modspec.sml: diff.behav. get_interval after replace} other 2 b";
12.1 --- a/test/Tools/isac/Specify/specify.sml Sun Feb 09 12:48:18 2020 +0100
12.2 +++ b/test/Tools/isac/Specify/specify.sml Sun Feb 09 16:21:26 2020 +0100
12.3 @@ -7,11 +7,134 @@
12.4 "table of contents -----------------------------------------------------------------------------";
12.5 "-----------------------------------------------------------------------------------------------";
12.6 "-----------------------------------------------------------------------------------------------";
12.7 -"----------- TODO -------------------------- ---------------------------------------------------";
12.8 +"----------- maximum-example: complete_mod ERROR formalisation inconsistent w.r.t. type inferenc";
12.9 +"----------- maximum-example: complete_metitms -------------------------------------------------";
12.10 "-----------------------------------------------------------------------------------------------";
12.11 "-----------------------------------------------------------------------------------------------";
12.12 "-----------------------------------------------------------------------------------------------";
12.13
12.14 -"----------- TODO -------------------------- ---------------------------------------------------";
12.15 -"----------- TODO -------------------------- ---------------------------------------------------";
12.16 -"----------- TODO -------------------------- ---------------------------------------------------";
12.17 +"----------- maximum-example: complete_mod ERROR formalisation inconsistent w.r.t. type inferenc";
12.18 +"----------- maximum-example: complete_mod ERROR formalisation inconsistent w.r.t. type inferenc";
12.19 +"----------- maximum-example: complete_mod ERROR formalisation inconsistent w.r.t. type inferenc";
12.20 +(*//-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --\\* )
12.21 + val (p,_,f,nxt,_,pt) =
12.22 + CalcTreeTEST
12.23 + [(["fixedValues [r=Arbfix]","maximum A",
12.24 + "valuesFor [a,b]",
12.25 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
12.26 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
12.27 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
12.28 +
12.29 + "boundVariable a","boundVariable b","boundVariable alpha",
12.30 + "interval {x::real. 0 <= x & x <= 2*r}",
12.31 + "interval {x::real. 0 <= x & x <= 2*r}",
12.32 + "interval {x::real. 0 <= x & x <= pi}",
12.33 + "errorBound (eps=(0::real))"],
12.34 + ("DiffApp",["maximum_of","function"],["DiffApp","max_by_calculus"])
12.35 + )];
12.36 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.37 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.38 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.39 + (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)
12.40 + val pits = get_obj g_pbl pt (fst p);
12.41 + writeln (itms2str_ ctxt pits);
12.42 +(*[
12.43 +(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
12.44 +(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),
12.45 +(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
12.46 +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)
12.47 + val (pt,p) = complete_mod (pt,p);
12.48 + val pits = get_obj g_pbl pt (fst p);
12.49 + if itms2str_ ctxt pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]"
12.50 + then () else error "completetest.sml: new behav. in complete_mod 3";
12.51 + writeln (itms2str_ ctxt pits);
12.52 +(*[
12.53 +(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
12.54 +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
12.55 +(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
12.56 +(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
12.57 +2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
12.58 + val mits = get_obj g_met pt (fst p);
12.59 + if itms2str_ ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]"
12.60 + then () else error "completetest.sml: new behav. in complete_mod 3";
12.61 + writeln (itms2str_ ctxt mits);
12.62 +(*[
12.63 +(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
12.64 +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
12.65 +(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
12.66 +(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
12.67 +2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
12.68 +(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
12.69 +(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
12.70 +0 <= x & x <= 2 * r}])),
12.71 +(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
12.72 +( *\\-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --//*)
12.73 +
12.74 +"----------- maximum-example: complete_metitms -------------------------------------------------";
12.75 +"----------- maximum-example: complete_metitms -------------------------------------------------";
12.76 +"----------- maximum-example: complete_metitms -------------------------------------------------";
12.77 +val c = [];
12.78 + val (p,_,f,nxt,_,pt) =
12.79 + CalcTreeTEST
12.80 + [(["fixedValues [r=Arbfix]","maximum A",
12.81 + "valuesFor [a,b]",
12.82 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
12.83 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
12.84 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
12.85 +
12.86 + "boundVariable a","boundVariable b","boundVariable alpha",
12.87 + "interval {x::real. 0 <= x & x <= 2*r}",
12.88 + "interval {x::real. 0 <= x & x <= 2*r}",
12.89 + "interval {x::real. 0 <= x & x <= pi}",
12.90 + "errorBound (eps=(0::real))"],
12.91 + ("DiffApp",["maximum_of","function"],["DiffApp","max_by_calculus"])
12.92 + )];
12.93 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.94 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.95 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.96 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.97 + val (p,_,f,nxt,_,pt) = (me nxt p c pt) (*handle e => OldGoals.print_exn e;*)
12.98 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.99 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.100 + (*nxt = Specify_Theory "DiffApp"*)
12.101 + val (oris, _, _) = get_obj g_origin pt (fst p);
12.102 + writeln (oris2str oris);
12.103 +(*[
12.104 +(1, ["1","2","3"], #Given,fixedValues, ["[r = Arbfix]"]),
12.105 +(2, ["1","2","3"], #Find,maximum, ["A"]),
12.106 +(3, ["1","2","3"], #Find,valuesFor, ["[a]","[b]"]),
12.107 +(4, ["1","2"], #Relate,relations, ["[A = a * b]","[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"]),
12.108 +(5, ["3"], #Relate,relations, ["[A = a * b]","[a / 2 = r * sin alpha]","[b / 2 = r * cos alpha]"]),
12.109 +(6, ["1"], #undef,boundVariable, ["a"]),
12.110 +(7, ["2"], #undef,boundVariable, ["b"]),
12.111 +(8, ["3"], #undef,boundVariable, ["alpha"]),
12.112 +(9, ["1","2"], #undef,interval, ["{x. 0 <= x & x <= 2 * r}"]),
12.113 +(10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]),
12.114 +(11, ["1","2","3"], #undef,errorBound, ["eps = 0"])]*)
12.115 + val pits = get_obj g_pbl pt (fst p);
12.116 + writeln (itms2str_ ctxt pits);
12.117 +(*[
12.118 +(1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])),
12.119 +(2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])),
12.120 +(3 ,[1,2,3] ,true,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
12.121 +(4 ,[1,2] ,true,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
12.122 +2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
12.123 + val mits = get_obj g_met pt (fst p);
12.124 + val mits = complete_metitms oris pits []
12.125 + ((#ppc o get_met) ["DiffApp","max_by_calculus"]);
12.126 + writeln (itms2str_ ctxt mits);
12.127 +(*[
12.128 +(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
12.129 +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
12.130 +(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
12.131 +(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
12.132 +2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
12.133 +(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
12.134 +(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
12.135 +0 <= x & x <= 2 * r}])),
12.136 +(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
12.137 +if itms2str_ ctxt mits
12.138 + = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_m, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(v_s, [[a, b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(r_s, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_v, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 \<le> x \<and> x \<le> 2 * r} ,(i_tv, [{x. 0 \<le> x \<and> x \<le> 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(e_rr, [eps = 0]))]"
12.139 +then () else error "completetest.sml: new behav. in complete_metitms 1";
12.140 +
12.141 +
13.1 --- a/test/Tools/isac/Test_Isac_Short.thy Sun Feb 09 12:48:18 2020 +0100
13.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Sun Feb 09 16:21:26 2020 +0100
13.3 @@ -212,9 +212,8 @@
13.4 ML_file "Specify/generate.sml"
13.5 ML_file "Specify/calchead.sml"
13.6 ML_file "Specify/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *)
13.7 + ML_file "Specify/step-specify.sml"
13.8 ML_file "Specify/specify.sml"
13.9 - ML_file "Specify/step-specify.sml"
13.10 -
13.11 ML_file "Interpret/rewtools.sml"
13.12 ML_file "Interpret/li-tool.sml"
13.13 ML_file "Interpret/inform.sml"
14.1 --- a/test/Tools/isac/Test_Some.thy Sun Feb 09 12:48:18 2020 +0100
14.2 +++ b/test/Tools/isac/Test_Some.thy Sun Feb 09 16:21:26 2020 +0100
14.3 @@ -86,6 +86,12 @@
14.4 \<close> ML \<open>
14.5 \<close>
14.6
14.7 +section \<open>===================================================================================\<close>
14.8 +ML \<open>
14.9 +\<close> ML \<open>
14.10 +\<close> ML \<open>
14.11 +\<close>
14.12 +
14.13 section \<open>===========--- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x"===============\<close>
14.14 ML \<open>
14.15 "~~~~~ fun xxx , args:"; val () = ();