1.1 --- a/src/Tools/isac/Build_Isac.thy Sun Sep 22 15:15:37 2019 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Sun Sep 22 16:52:14 2019 +0200
1.3 @@ -26,7 +26,6 @@
1.4 ML_file calculate.sml
1.5 theory ListC imports "~~/src/Tools/isac/CalcElements/CalcElements"
1.6 theory Prog_Expr imports Calculate ListC
1.7 -
1.8 theory Program imports "~~/src/Tools/isac/CalcElements/CalcElements"
1.9 theory Prog_Tac imports "~~/src/Tools/isac/CalcElements/CalcElements"
1.10 theory Tactical imports "~~/src/Tools/isac/CalcElements/CalcElements"
2.1 --- a/src/Tools/isac/TODO.thy Sun Sep 22 15:15:37 2019 +0200
2.2 +++ b/src/Tools/isac/TODO.thy Sun Sep 22 16:52:14 2019 +0200
2.3 @@ -20,12 +20,9 @@
2.4 \item xxx
2.5 \item xxx
2.6 \item separate code required in both, ProgLang & Interpret
2.7 - \begin{itemize}
2.8 \item xxx
2.9 \item /-------------------------------------------------------------------
2.10 \item Atools.thy (*> tests*) -> /test/..
2.11 - \item Atools.thy then SOME
2.12 - HOLogic ... indentations
2.13 \item check occurences of KEStore_Elems.add_rlss [("list_rls",
2.14 \item rename list_rls accordingly
2.15 \item + see subsection \<open>overall structure of code\<close>
2.16 @@ -47,7 +44,7 @@
2.17 \end{itemize}
2.18 \item xxx
2.19 \item xxx
2.20 - \item xxx
2.21 + \item distribute test/../scrtools.sml
2.22 \item xxx
2.23 \item xxx
2.24 \item simplify calls of assy, appy etc
2.25 @@ -63,7 +60,7 @@
2.26 rm tactic Check_elementwise "Assumptions" in a way, which keeps it for Minisubpbl
2.27 rm Assumptions :: bool (* TODO: remove with making ^^^ idle *)
2.28 \item xxx
2.29 - \item clenup fun me:
2.30 + \item cleanup fun me:
2.31 fun me (*(_, Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
2.32 | me*) (_, tac) p _(*NEW remove*) pt =
2.33 + -------------------------^^^^^^
3.1 --- a/test/Tools/isac/CalcElements/calcelems.sml Sun Sep 22 15:15:37 2019 +0200
3.2 +++ b/test/Tools/isac/CalcElements/calcelems.sml Sun Sep 22 16:52:14 2019 +0200
3.3 @@ -1,5 +1,6 @@
3.4 -(* tests for sml/calcelems.sml
3.5 - author: Walther Neuper 060113
3.6 +(* Title: CalcElements/calcelems.sml
3.7 + Author: Walther Neuper 060113
3.8 + (c) due to copyright terms
3.9 *)
3.10
3.11 "--------------------------------------------------------";
3.12 @@ -12,7 +13,7 @@
3.13 "-------- fun thmID_of_derivation_name 000---------------";
3.14 "-------- fun merge_rlss -----------------------------------------------------";
3.15 "-------- fun update_ptyps --------------------------------------------------";
3.16 -"----------- fun subst2str' --------------------------------------------------------------------";
3.17 +"-------- fun subst2str' -----------------------------------------------------------------------";
3.18 "--------------------------------------------------------";
3.19 "--------------------------------------------------------";
3.20 "--------------------------------------------------------";
4.1 --- a/test/Tools/isac/CalcElements/listC.sml Sun Sep 22 15:15:37 2019 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,100 +0,0 @@
4.4 -(* Title: tests for ListC
4.5 - Author: Walther Neuper 030501
4.6 - (c) copyright due to lincense terms.
4.7 -*)
4.8 -
4.9 -"-----------------------------------------------------------------------------";
4.10 -"-----------------------------------------------------------------------------";
4.11 -"table of contents -----------------------------------------------------------";
4.12 -"-----------------------------------------------------------------------------";
4.13 -"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
4.14 -"--------------------- NTH ---------------------------------------------------";
4.15 -"--------------------- LENGTH ------------------------------------------------";
4.16 -"--------------------- tl ----------------------------------------------------";
4.17 -"-----------------------------------------------------------------------------";
4.18 -"-----------------------------------------------------------------------------";
4.19 -
4.20 -"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
4.21 -"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
4.22 -"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
4.23 -(* ML representation *)
4.24 -val t1 = @{term "{|| ||}"};
4.25 -val t2 = @{term "{||1,2,3||}"};
4.26 -
4.27 -(* pretty printing *)
4.28 -if Print_Mode.setmp []
4.29 - (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t1
4.30 - = "{|| ||}"
4.31 -then () else error "CHANGED pretty printing of '{|| ||}'";
4.32 -
4.33 -if Print_Mode.setmp []
4.34 - (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t2
4.35 - = "{|| 1::'a, 2::'a, 3::'a ||}"
4.36 -then () else error "CHANGED pretty printing of '{||1,2,3||}'"
4.37 -
4.38 -(* parsing *)
4.39 -Syntax.read_term_global @{theory} "{|| ||}";
4.40 -Syntax.read_term_global @{theory} "{||1,2,3||}";
4.41 -
4.42 -"--------------------- NTH ---------------------------------------------------";
4.43 -"--------------------- NTH ---------------------------------------------------";
4.44 -"--------------------- NTH ---------------------------------------------------";
4.45 -val list_rls = assoc_rls "list_rls"
4.46 -
4.47 -val t = str2term "NTH 1 [a,b,c,d,e]";
4.48 -atomty t;
4.49 -val thm = (#prop o Thm.rep_thm o num_str) @{thm NTH_NIL};
4.50 -atomty thm;
4.51 -val SOME (t', _) = rewrite_ thy dummy_ord list_rls false (num_str @{thm NTH_NIL}) t;
4.52 -if term2str t' = "a" then ()
4.53 -else error "NTH 1 [a,b,c,d,e] = a ..changed";
4.54 -
4.55 -val t = str2term "NTH 3 [a,b,c,d,e]";
4.56 -val Const ("ListC.NTH", _) $ Free ("3", _) $ (Const ("List.list.Cons", _) $ Free ("a", _) $
4.57 - (Const ("List.list.Cons", _) $ Free ("b", _) $
4.58 - (Const _ $ Free _ $ (Const _ $ Free _ $ (Const _ $ Free _ $ Const _))))) = t;
4.59 -atomty t;
4.60 -val thm = (#prop o Thm.rep_thm o num_str) @{thm NTH_CONS};
4.61 -atomty thm;
4.62 -val SOME (t', _) = rewrite_ thy dummy_ord list_rls false (num_str @{thm NTH_CONS}) t;
4.63 -if term2str t' = "NTH (3 + -1) [b, c, d, e]" then ()
4.64 -else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
4.65 -
4.66 -(* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
4.67 -val t = str2term "NTH 3 [a,b,c,d,e]";
4.68 -atomty t;
4.69 -trace_rewrite := false;
4.70 -val SOME (t', _) = rewrite_set_ thy false list_rls t;
4.71 -trace_rewrite := false;
4.72 -if term2str t' = "c" then ()
4.73 -else error "NTH 3 [a,b,c,d,e] = c ..changed";
4.74 -
4.75 -"--------------------- LENGTH ------------------------------------------------";
4.76 -"--------------------- LENGTH ------------------------------------------------";
4.77 -"--------------------- LENGTH ------------------------------------------------";
4.78 -val list_rls = assoc_rls "list_rls"
4.79 -
4.80 -val thy = @{theory ListC};
4.81 -val t = str2term "LENGTH [1, 1, 1]";
4.82 -val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
4.83 -term2str t = "1 + LENGTH [1, 1]";
4.84 -val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
4.85 -term2str t = "1 + (1 + LENGTH [1])";
4.86 -val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
4.87 -term2str t = "1 + (1 + (1 + LENGTH []))";
4.88 -val NONE = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
4.89 -val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
4.90 -val NONE = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
4.91 -if term2str t = "1 + (1 + (1 + 0))" then ()
4.92 -else error "LENGTH [1, 1, 1] = 1 + (1 + (1 + 0)) ..changed";
4.93 -
4.94 -val t = str2term "LENGTH [1, 1, 1]";
4.95 -val SOME (t, asm) = rewrite_set_ thy false list_rls t;
4.96 -if term2str t = "3" then ()
4.97 -else error "LENGTH [1, 1, 1] = 3 ..list_rls changed";
4.98 -
4.99 -val t = str2term "LENGTH [1, 1, 1]";
4.100 -val t = eval_listexpr_ thy list_rls t;
4.101 -case t of Free ("3", _) => ()
4.102 -| _ => error "LENGTH [1, 1, 1] = 3 ..eval_listexpr_ changed";
4.103 -
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/test/Tools/isac/CalcElements/rule.sml Sun Sep 22 16:52:14 2019 +0200
5.3 @@ -0,0 +1,20 @@
5.4 +(* Title: CalcElements/rule.sml
5.5 + Author: Walther Neuper 190922
5.6 + (c) due to copyright terms
5.7 +*)
5.8 +
5.9 +"-----------------------------------------------------------------------------------------------";
5.10 +"-----------------------------------------------------------------------------------------------";
5.11 +"table of contents -----------------------------------------------------------------------------";
5.12 +"-----------------------------------------------------------------------------------------------";
5.13 +"-------- xxx ------";
5.14 +"-------- xxx ------";
5.15 +"-------- xxx ------";
5.16 +"-----------------------------------------------------------------------------------------------";
5.17 +"-----------------------------------------------------------------------------------------------";
5.18 +"-----------------------------------------------------------------------------------------------";
5.19 +
5.20 +
5.21 +"-------- xxx ------";
5.22 +"-------- xxx ------";
5.23 +"-------- xxx ------";
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Sun Sep 22 16:52:14 2019 +0200
6.3 @@ -0,0 +1,295 @@
6.4 +(* Title: ProgLang/auto_prog.sml
6.5 + Author: Walther Neuper 190922
6.6 + (c) due to copyright terms
6.7 +*)
6.8 +
6.9 +"-----------------------------------------------------------------------------------------------";
6.10 +"-----------------------------------------------------------------------------------------------";
6.11 +"table of contents -----------------------------------------------------------------------------";
6.12 +"-----------------------------------------------------------------------------------------------";
6.13 +"-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
6.14 +"-------- test the same called by interSteps norm_Poly -----------------------------------------";
6.15 +"-------- test the same called by interSteps norm_Rational -------------------------------------";
6.16 +"-------- fun op @@ ----------------------------------------------------------------------------";
6.17 +"-------- fun rules2scr_Rls --------------------------------------------------------------------";
6.18 +"-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
6.19 +"-------- fun stacpbls -------------------------------------------------------------------------";
6.20 +"-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
6.21 +"-----------------------------------------------------------------------------------------------";
6.22 +"-----------------------------------------------------------------------------------------------";
6.23 +"-----------------------------------------------------------------------------------------------";
6.24 +
6.25 +
6.26 +"-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
6.27 +"-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
6.28 +"-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
6.29 +val rls = assoc_rls "integration";
6.30 +val Seq {scr = Prog auto_script,...} = rls;
6.31 +writeln(term2str auto_script);
6.32 +
6.33 +if contain_bdv (get_rules rls) then ()
6.34 +else error "scrtools.sml: contain_bdv doesnt work for 'integration'";
6.35 +
6.36 +if terms2str (formal_args auto_script) = "[\"t_t\",\"v\"]"
6.37 +then () else error "formal_args of auto-gen.script changed";
6.38 +init_istate (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules"))
6.39 + (str2term "someTermWithBdv");
6.40 +
6.41 +"-------- test the same called by interSteps norm_Poly -----------------------------------------";
6.42 +"-------- test the same called by interSteps norm_Poly -----------------------------------------";
6.43 +"-------- test the same called by interSteps norm_Poly -----------------------------------------";
6.44 +val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";
6.45 +writeln(term2str auto_script);
6.46 +(*Program Stepwise t_t =
6.47 + (Try (Rewrite_Set discard_minus False) @@
6.48 + Try (Rewrite_Set expand_poly_ False) @@
6.49 + Try (Repeat (Calculate TIMES)) @@
6.50 + Try (Rewrite_Set order_mult_rls_ False) @@
6.51 + Try (Rewrite_Set simplify_power_ False) @@
6.52 + Try (Rewrite_Set calc_add_mult_pow_ False) @@
6.53 + Try (Rewrite_Set reduce_012_mult_ False) @@
6.54 + Try (Rewrite_Set order_add_rls_ False) @@
6.55 + Try (Rewrite_Set collect_numerals_ False) @@
6.56 + Try (Rewrite_Set reduce_012_ False) @@
6.57 + Try (Rewrite_Set discard_parentheses1 False))
6.58 + ??.empty ..WORKS, NEVERTHELESS *)
6.59 +atomty auto_script;
6.60 +
6.61 +reset_states (); (*<-- evaluate, if ML-blocks are edited below*)
6.62 +CalcTree
6.63 +[(["Term (b + a - b)", "normalform N"],
6.64 + ("Poly",["polynomial","simplification"],
6.65 + ["simplification","for_polynomials"]))];
6.66 +Iterator 1;
6.67 +moveActiveRoot 1;
6.68 +
6.69 +autoCalculate 1 CompleteCalc;
6.70 +val ((pt,p),_) = get_calc 1;
6.71 +show_pt pt;
6.72 +(* isabisac17 = 15 [
6.73 +(([], Frm), Simplify (b + a - b)),
6.74 +(([1], Frm), b + a - b),
6.75 +(([1], Res), a),
6.76 +(([], Res), a)] *)
6.77 +
6.78 +interSteps 1 ([], Res);
6.79 +val ((pt,p),_) = get_calc 1; show_pt pt;
6.80 +show_pt pt;
6.81 +(* isabisac17 = 15 [
6.82 +(([], Frm), Simplify (b + a - b)),
6.83 +(([1], Frm), b + a - b),
6.84 +(([1], Res), a),
6.85 +(([], Res), a)] *)
6.86 +
6.87 +interSteps 1 ([1], Res);(*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 8</ERROR></SYSERROR>*)
6.88 +"~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1], Res));
6.89 + val ((pt, p), tacis) = get_calc cI;
6.90 +(*if*) (not o is_interpos) ip = false;
6.91 +val ip' = lev_pred' pt ip;
6.92 +
6.93 +(*Math_Engine.detailstep pt ip ..ERROR interSteps>..>init_istate: "norm_Poly" has EmptyScr*)
6.94 +val ("donesteps", ctree_BEFORE_step_into, pos'_BEFORE_step_into) = Math_Engine.detailstep pt ip;
6.95 +"~~~~~ fun detailstep, args:"; val (pt, (pos as (p, _))) = (pt, ip);
6.96 + val nd = Ctree.get_nd pt p
6.97 + val cn = Ctree.children nd;
6.98 +(*if*) null cn = false;
6.99 +
6.100 +"~~~~~ to detailrls return val:";
6.101 +(*else*)
6.102 +val return_val = ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Ctree.Res));
6.103 +if p @ [length (Ctree.children (Ctree.get_nd pt p))] = [1, 4]
6.104 +then () else error "detailrls: auto-generated norm_Poly doesnt work";
6.105 +
6.106 +val ((pt,p),_) = get_calc 1; show_pt pt;
6.107 +show_pt pt; (*[
6.108 +(([], Frm), Simplify (b + a - b)),
6.109 +(([1], Frm), b + a - b),
6.110 +(([1,1], Frm), b + a - b),
6.111 +(([1,1], Res), b + a + -1 * b),
6.112 +(([1,2], Res), a + b + -1 * b),
6.113 +(([1,3], Res), a + 0 * b),
6.114 +(([1,4], Res), a),
6.115 +(([1], Res), a),
6.116 +(([], Res), a)] *)
6.117 +if existpt' ([1,4], Res) pt then ()
6.118 +else error "auto-generated norm_Poly doesnt work";
6.119 +
6.120 +"-------- test the same called by interSteps norm_Rational -------------------------------------";
6.121 +"-------- test the same called by interSteps norm_Rational -------------------------------------";
6.122 +"-------- test the same called by interSteps norm_Rational -------------------------------------";
6.123 +val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Rational";
6.124 +writeln(term2str auto_script);
6.125 +atomty auto_script;
6.126 +(***
6.127 +*** Const (Program.Stepwise, 'z => 'z => 'z)
6.128 +*** . Free (t_t, 'z)
6.129 +*** . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
6.130 +*** . . Const (Program.Try, ('a => 'a) => 'a => 'a)
6.131 +*** . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
6.132 +*** . . . . Free (discard_minus, ID)
6.133 +*** . . . . Const (HOL.False, bool)
6.134 +*** . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
6.135 +*** . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
6.136 +*** . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
6.137 +*** . . . . . Free (rat_mult_poly, ID)
6.138 +*** . . . . . Const (HOL.False, bool)
6.139 +*** . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
6.140 +*** . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
6.141 +*** . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
6.142 +*** . . . . . . Free (make_rat_poly_with_parentheses, ID)
6.143 +*** . . . . . . Const (HOL.False, bool)
6.144 +*** . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
6.145 +*** . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
6.146 +*** . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
6.147 +*** . . . . . . . Free (cancel_p_rls, ID)
6.148 +*** . . . . . . . Const (HOL.False, bool)
6.149 +*** . . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
6.150 +*** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
6.151 +*** . . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
6.152 +*** . . . . . . . . Free (norm_Rational_rls, ID)
6.153 +*** . . . . . . . . Const (HOL.False, bool)
6.154 +*** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
6.155 +*** . . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
6.156 +*** . . . . . . . . Free (discard_parentheses1, ID)
6.157 +*** . . . . . . . . Const (HOL.False, bool)
6.158 +*** . . Const (empty, 'a)
6.159 +***)
6.160 +reset_states ();
6.161 +CalcTree
6.162 +[(["Term (b + a - b)", "normalform N"],
6.163 + ("Poly",["polynomial","simplification"],
6.164 + ["simplification","of_rationals"]))];
6.165 +Iterator 1;
6.166 +moveActiveRoot 1;
6.167 +autoCalculate 1 CompleteCalc;
6.168 +
6.169 +interSteps 1 ([], Res);
6.170 +val ((pt,p),_) = get_calc 1; show_pt pt;
6.171 +
6.172 +interSteps 1 ([1], Res);
6.173 +val ((pt,p),_) = get_calc 1; show_pt pt;
6.174 +
6.175 +(*with "Program SimplifyScript (t_::real) = \
6.176 + \ ((Rewrite_Set norm_Rational False) t_)"
6.177 +val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));
6.178 +*)
6.179 +val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
6.180 +case (term2str form, tac, terms2strs asm) of
6.181 + ("a", Check_Postcond ["polynomial", "simplification"], []) => ()
6.182 + | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work";
6.183 +
6.184 +"-------- fun op @@ ----------------------------------------------------------------------------";
6.185 +"-------- fun op @@ ----------------------------------------------------------------------------";
6.186 +"-------- fun op @@ ----------------------------------------------------------------------------";
6.187 + val rules = (#rules o rep_rls) isolate_root;
6.188 + val rs = map (rule2stac @{theory}) rules;
6.189 + val t = @@ rs;
6.190 +if term2str t = "Try (Repeat (Rewrite ''rroot_to_lhs'' False)) @@\n" ^
6.191 + "Try (Repeat (Rewrite ''rroot_to_lhs_mult'' False)) @@\n" ^
6.192 + "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'' False)) @@\n" ^
6.193 + "Try (Repeat (Rewrite ''risolate_root_add'' False)) @@\n" ^
6.194 + "Try (Repeat (Rewrite ''risolate_root_mult'' False)) @@\n" ^
6.195 + "Try (Repeat (Rewrite ''risolate_root_div'' False))"
6.196 +then () else error "fun @@ changed"
6.197 +
6.198 +"-------- fun rules2scr_Rls --------------------------------------------------------------------";
6.199 +"-------- fun rules2scr_Rls --------------------------------------------------------------------";
6.200 +"-------- fun rules2scr_Rls --------------------------------------------------------------------";
6.201 +(*compare Prog_Expr.*)
6.202 +val prog = Auto_Prog.rules2scr_Rls @{theory} [Rule.Thm ("thm111", @{thm thm111}), Rule.Thm ("refl", @{thm refl})]
6.203 +;
6.204 +writeln (t2str @{theory} prog);
6.205 +(*auto_generated t_t =
6.206 +Repeat
6.207 + ((Try (Repeat (Rewrite ''thm111'' False)) @@
6.208 + Try (Repeat (Rewrite ''refl'' False)))
6.209 + ??.empty)*)
6.210 +;
6.211 +if t2str @{theory} prog =
6.212 +"auto_generated t_t =\nRepeat\n ((Try (Repeat (Rewrite ''thm111'' False)) @@\n Try (Repeat (Rewrite ''refl'' False)))\n ??.empty)"
6.213 +then () else error "rules2scr_Rls auto_generated changed"
6.214 +
6.215 +"-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
6.216 +"-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
6.217 +"-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
6.218 +val t = rule2stac @{theory} (Thm ("real_diff_minus", num_str @{thm real_diff_minus}));
6.219 +if term2str t = "Try (Repeat (Rewrite ''real_diff_minus'' False))" then ()
6.220 +else error "rule2stac Thm.. changed";
6.221 +
6.222 +val t = rule2stac @{theory} (Calc ("Groups.plus_class.plus", eval_binop "#add_"));
6.223 +if term2str t = "Try (Repeat (Calculate ''PLUS''))" then ()
6.224 +else error "rule2stac Calc.. changed";
6.225 +
6.226 +val t = rule2stac @{theory} (Rls_ rearrange_assoc);
6.227 +if term2str t = "Try (Rewrite_Set ''rearrange_assoc'' False)" then ()
6.228 +else error "rule2stac Rls_.. changed";
6.229 +
6.230 +val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", num_str @{thm risolate_bdv_add}));
6.231 +if term2str t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'' False))" then ()
6.232 +else error "rule2stac_inst Thm.. changed";
6.233 +case t of
6.234 + (Const ("Tactical.Try", _) $
6.235 + (Const ("Tactical.Repeat", _) $
6.236 + (Const ("Prog_Tac.Rewrite'_Inst", _) $
6.237 + (Const ("List.list.Cons", _) $
6.238 + (Const ("Product_Type.Pair", _) $
6.239 + bdv $
6.240 + Free ("v", _)) $
6.241 + Const ("List.list.Nil", _)) $
6.242 + risolate_bdv_add $
6.243 + Const ("HOL.False", _)))) =>
6.244 + (if HOLogic.dest_string bdv = "bdv" andalso
6.245 + HOLogic.dest_string risolate_bdv_add = "risolate_bdv_add" then ()
6.246 + else error "rule2stac_inst changed 1")
6.247 +| _ => error "rule2stac_inst changed 2";
6.248 +
6.249 +"-------- fun stacpbls -------------------------------------------------------------------------";
6.250 +"-------- fun stacpbls -------------------------------------------------------------------------";
6.251 +"-------- fun stacpbls -------------------------------------------------------------------------";
6.252 +val {scr, ...} = get_met ["Test","sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
6.253 +case stacpbls sc of
6.254 + [Const ("Prog_Tac.Rewrite", _) $ square_equation_left $ Const ("HOL.True", _),
6.255 + Const ("Prog_Tac.Rewrite'_Set", _) $ Test_simplify $ Const ("HOL.False", _),
6.256 + Const ("Prog_Tac.Rewrite'_Set", _) $ rearrange_assoc $ Const ("HOL.False", _),
6.257 + Const ("Prog_Tac.Rewrite'_Set", _) $ isolate_root $ Const ("HOL.False", _),
6.258 + Const ("Prog_Tac.Rewrite'_Set", _) $ norm_equation $ Const ("HOL.False", _),
6.259 + Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $
6.260 + (Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ bdv $ Free ("v_v", _)) $
6.261 + Const ("List.list.Nil", _)) $
6.262 + isolate_bdv $ Const ("HOL.False", _)] =>
6.263 + if HOLogic.dest_string square_equation_left = "square_equation_left" andalso
6.264 + HOLogic.dest_string Test_simplify = "Test_simplify" andalso
6.265 + HOLogic.dest_string rearrange_assoc = "rearrange_assoc" andalso
6.266 + HOLogic.dest_string isolate_root = "isolate_root" andalso
6.267 + HOLogic.dest_string norm_equation = "norm_equation" andalso
6.268 + HOLogic.dest_string bdv = "bdv" andalso
6.269 + HOLogic.dest_string isolate_bdv = "isolate_bdv"
6.270 + then () else error "stacpbls (Test.Solve_root_equation) changed 2"
6.271 +| _ => error "stacpbls (Test.Solve_root_equation) changed 1";
6.272 +
6.273 +(* inappropriate input is skipped *)
6.274 +val t = @{term "(a::real) = (rhs (NTH 1 sol_a))"};
6.275 +case stacpbls t of [] => () | _ => error "stacpbls rhs (NTH 1 sol_a) changed";
6.276 +
6.277 +@{term "(SubProblem (BiegelinieX,[vonBelastungZu,Biegelinien], [Biegelinien,ausBelastung]) [REAL q__q, REAL v_v])"};
6.278 +case stacpbls t of [] => () | _ => error "stacpbls (SubProblem ...) changed";
6.279 +
6.280 +"-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
6.281 +"-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
6.282 +"-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
6.283 +val rls = prep_rls @{theory} Test_simplify; (* adds the Program *)
6.284 +val Prog sc = (#scr o rep_rls) rls;
6.285 +val stacs = stacpbls sc;
6.286 +
6.287 +val calcs = filter is_calc stacs;
6.288 +val ids = map op_of_calc calcs;
6.289 +case ids of
6.290 + ["PLUS", "TIMES", "DIVIDE", "POWER"] => ()
6.291 +| _ => error "op_of_calc";
6.292 +
6.293 +val calcs = ((assoc_calc' @{theory} |> map) o (map Auto_Prog.op_of_calc) o
6.294 + (filter Auto_Prog.is_calc) o Auto_Prog.stacpbls) sc;
6.295 +case calcs of
6.296 + [("PLUS", ("Groups.plus_class.plus", _)), ("TIMES", ("Groups.times_class.times", _)),
6.297 + ("DIVIDE", ("Rings.divide_class.divide", _)), ("POWER", ("Prog_Expr.pow", _))] => ()
6.298 +| _ => error "get_calcs changed"
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/test/Tools/isac/ProgLang/listC.sml Sun Sep 22 16:52:14 2019 +0200
7.3 @@ -0,0 +1,100 @@
7.4 +(* Title: tests for ListC
7.5 + Author: Walther Neuper 030501
7.6 + (c) copyright due to lincense terms.
7.7 +*)
7.8 +
7.9 +"-----------------------------------------------------------------------------";
7.10 +"-----------------------------------------------------------------------------";
7.11 +"table of contents -----------------------------------------------------------";
7.12 +"-----------------------------------------------------------------------------";
7.13 +"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
7.14 +"--------------------- NTH ---------------------------------------------------";
7.15 +"--------------------- LENGTH ------------------------------------------------";
7.16 +"--------------------- tl ----------------------------------------------------";
7.17 +"-----------------------------------------------------------------------------";
7.18 +"-----------------------------------------------------------------------------";
7.19 +
7.20 +"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
7.21 +"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
7.22 +"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
7.23 +(* ML representation *)
7.24 +val t1 = @{term "{|| ||}"};
7.25 +val t2 = @{term "{||1,2,3||}"};
7.26 +
7.27 +(* pretty printing *)
7.28 +if Print_Mode.setmp []
7.29 + (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t1
7.30 + = "{|| ||}"
7.31 +then () else error "CHANGED pretty printing of '{|| ||}'";
7.32 +
7.33 +if Print_Mode.setmp []
7.34 + (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t2
7.35 + = "{|| 1::'a, 2::'a, 3::'a ||}"
7.36 +then () else error "CHANGED pretty printing of '{||1,2,3||}'"
7.37 +
7.38 +(* parsing *)
7.39 +Syntax.read_term_global @{theory} "{|| ||}";
7.40 +Syntax.read_term_global @{theory} "{||1,2,3||}";
7.41 +
7.42 +"--------------------- NTH ---------------------------------------------------";
7.43 +"--------------------- NTH ---------------------------------------------------";
7.44 +"--------------------- NTH ---------------------------------------------------";
7.45 +val list_rls = assoc_rls "list_rls"
7.46 +
7.47 +val t = str2term "NTH 1 [a,b,c,d,e]";
7.48 +atomty t;
7.49 +val thm = (#prop o Thm.rep_thm o num_str) @{thm NTH_NIL};
7.50 +atomty thm;
7.51 +val SOME (t', _) = rewrite_ thy dummy_ord list_rls false (num_str @{thm NTH_NIL}) t;
7.52 +if term2str t' = "a" then ()
7.53 +else error "NTH 1 [a,b,c,d,e] = a ..changed";
7.54 +
7.55 +val t = str2term "NTH 3 [a,b,c,d,e]";
7.56 +val Const ("ListC.NTH", _) $ Free ("3", _) $ (Const ("List.list.Cons", _) $ Free ("a", _) $
7.57 + (Const ("List.list.Cons", _) $ Free ("b", _) $
7.58 + (Const _ $ Free _ $ (Const _ $ Free _ $ (Const _ $ Free _ $ Const _))))) = t;
7.59 +atomty t;
7.60 +val thm = (#prop o Thm.rep_thm o num_str) @{thm NTH_CONS};
7.61 +atomty thm;
7.62 +val SOME (t', _) = rewrite_ thy dummy_ord list_rls false (num_str @{thm NTH_CONS}) t;
7.63 +if term2str t' = "NTH (3 + -1) [b, c, d, e]" then ()
7.64 +else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
7.65 +
7.66 +(* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
7.67 +val t = str2term "NTH 3 [a,b,c,d,e]";
7.68 +atomty t;
7.69 +trace_rewrite := false;
7.70 +val SOME (t', _) = rewrite_set_ thy false list_rls t;
7.71 +trace_rewrite := false;
7.72 +if term2str t' = "c" then ()
7.73 +else error "NTH 3 [a,b,c,d,e] = c ..changed";
7.74 +
7.75 +"--------------------- LENGTH ------------------------------------------------";
7.76 +"--------------------- LENGTH ------------------------------------------------";
7.77 +"--------------------- LENGTH ------------------------------------------------";
7.78 +val list_rls = assoc_rls "list_rls"
7.79 +
7.80 +val thy = @{theory ListC};
7.81 +val t = str2term "LENGTH [1, 1, 1]";
7.82 +val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
7.83 +term2str t = "1 + LENGTH [1, 1]";
7.84 +val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
7.85 +term2str t = "1 + (1 + LENGTH [1])";
7.86 +val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
7.87 +term2str t = "1 + (1 + (1 + LENGTH []))";
7.88 +val NONE = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
7.89 +val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
7.90 +val NONE = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
7.91 +if term2str t = "1 + (1 + (1 + 0))" then ()
7.92 +else error "LENGTH [1, 1, 1] = 1 + (1 + (1 + 0)) ..changed";
7.93 +
7.94 +val t = str2term "LENGTH [1, 1, 1]";
7.95 +val SOME (t, asm) = rewrite_set_ thy false list_rls t;
7.96 +if term2str t = "3" then ()
7.97 +else error "LENGTH [1, 1, 1] = 3 ..list_rls changed";
7.98 +
7.99 +val t = str2term "LENGTH [1, 1, 1]";
7.100 +val t = eval_listexpr_ thy list_rls t;
7.101 +case t of Free ("3", _) => ()
7.102 +| _ => error "LENGTH [1, 1, 1] = 3 ..eval_listexpr_ changed";
7.103 +
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml Sun Sep 22 16:52:14 2019 +0200
8.3 @@ -0,0 +1,20 @@
8.4 +(* Title: ProgLang/program.sml
8.5 + Author: Walther Neuper 190922
8.6 + (c) due to copyright terms
8.7 +*)
8.8 +
8.9 +"-----------------------------------------------------------------------------------------------";
8.10 +"-----------------------------------------------------------------------------------------------";
8.11 +"table of contents -----------------------------------------------------------------------------";
8.12 +"-----------------------------------------------------------------------------------------------";
8.13 +"-------- xxx ------";
8.14 +"-------- xxx ------";
8.15 +"-------- xxx ------";
8.16 +"-----------------------------------------------------------------------------------------------";
8.17 +"-----------------------------------------------------------------------------------------------";
8.18 +"-----------------------------------------------------------------------------------------------";
8.19 +
8.20 +
8.21 +"-------- xxx ------";
8.22 +"-------- xxx ------";
8.23 +"-------- xxx ------";
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/test/Tools/isac/ProgLang/prog_tac.sml Sun Sep 22 16:52:14 2019 +0200
9.3 @@ -0,0 +1,33 @@
9.4 +(* Title: ProgLang/prog_tac.sml
9.5 + Author: Walther Neuper 190922
9.6 + (c) due to copyright terms
9.7 +*)
9.8 +
9.9 +"-----------------------------------------------------------------------------------------------";
9.10 +"-----------------------------------------------------------------------------------------------";
9.11 +"table of contents -----------------------------------------------------------------------------";
9.12 +"-----------------------------------------------------------------------------------------------";
9.13 +"-------- fun subst_stacexpr -------------------------------------------------------------------";
9.14 +"-------- xxx ------";
9.15 +"-------- xxx ------";
9.16 +"-----------------------------------------------------------------------------------------------";
9.17 +"-----------------------------------------------------------------------------------------------";
9.18 +"-----------------------------------------------------------------------------------------------";
9.19 +
9.20 +
9.21 +"-------- fun subst_stacexpr -------------------------------------------------------------------";
9.22 +"-------- fun subst_stacexpr -------------------------------------------------------------------";
9.23 +"-------- fun subst_stacexpr -------------------------------------------------------------------";
9.24 +val {scr = Prog sc, ...} = get_met ["Test","sqrt-equ-test"];
9.25 +case subst_stacexpr [] NONE e_term sc of
9.26 +(NONE, Expr (Const ("HOL.eq", _) $
9.27 + (Const ("Test.solve_root_equ", _) $ Free ("e_e", _) $ Free ("v_v", _)) $
9.28 + (Const ("HOL.Let", _) $
9.29 + (Const ("Tactical.Seq", _) $
9.30 + (Const ("Tactical.While", _) $ _ $
9.31 + _ ) $
9.32 + (_) $
9.33 + Free ("e_e", _)) $
9.34 + Abs ("e_e", _, Const ("List.list.Cons", _) $ Free ("e_e", _) $ Const ("List.list.Nil", _)) )
9.35 +)) => ()
9.36 +| _ => error "subst_stacexpr [] NONE e_term";
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/test/Tools/isac/ProgLang/program.sml Sun Sep 22 16:52:14 2019 +0200
10.3 @@ -0,0 +1,55 @@
10.4 +(* Title: ProgLang/program.sml
10.5 + Author: Walther Neuper 190922
10.6 + (c) due to copyright terms
10.7 +*)
10.8 +
10.9 +"-----------------------------------------------------------------------------------------------";
10.10 +"-----------------------------------------------------------------------------------------------";
10.11 +"table of contents -----------------------------------------------------------------------------";
10.12 +"-----------------------------------------------------------------------------------------------";
10.13 +"-------- fun get_fun_id -----------------------------------------------------------------------";
10.14 +"-------- xxx ------";
10.15 +"-------- xxx ------";
10.16 +"-----------------------------------------------------------------------------------------------";
10.17 +"-----------------------------------------------------------------------------------------------";
10.18 +"-----------------------------------------------------------------------------------------------";
10.19 +
10.20 +
10.21 +"-------- fun get_fun_id -----------------------------------------------------------------------";
10.22 +"-------- fun get_fun_id -----------------------------------------------------------------------";
10.23 +"-------- fun get_fun_id -----------------------------------------------------------------------";
10.24 +(* fun_id is nested into arguments, compare ... *)
10.25 +val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
10.26 + (((((((Const (const_id, const_typ) $ _) $ _) $ _) $ _) $ _) $ _) $ _) $ _) =
10.27 + Thm.prop_of @{thm biegelinie.simps};
10.28 +(* ... to: *)
10.29 +val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
10.30 + (Const (const_id, const_typ) $ _) $ _) =
10.31 + Thm.prop_of @{thm simplify.simps};
10.32 +
10.33 +(* get fun_id out of nesting *)
10.34 +val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
10.35 + nested $ _) =
10.36 + Thm.prop_of @{thm biegelinie.simps};
10.37 +val (Const ("Biegelinie.biegelinie", _) $
10.38 + Var (("l", 0), _) $
10.39 + Var (("q", 0), _) $
10.40 + Var (("v", 0), _) $
10.41 + Var (("b", 0), _) $
10.42 + Var (("s", 0), _) $
10.43 + Var (("vs", 0), _) $
10.44 + Var (("id_abl", 0), _)) = nested;
10.45 +strip_comb nested;
10.46 +(*val it =
10.47 + (Const ("Biegelinie.biegelinie", "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> bool")
10.48 + ,
10.49 + [Var (("l", 0), "real"), Var (("q", 0), "real"), Var (("v", 0), "real"),
10.50 + Var (("b", 0), "real \<Rightarrow> real"), Var (("s", 0), "bool list")]):
10.51 + term * term list*)
10.52 +
10.53 +case get_fun_id (prep_program @{thm biegelinie.simps}) of
10.54 + ("Biegelinie.biegelinie", _) => ()
10.55 +| _ => error "get_fun_id changed";
10.56 +case get_fun_id (prep_program @{thm simplify.simps}) of
10.57 + ("PolyMinus.simplify", _) => ()
10.58 +| _ => error "get_fun_id changed";
11.1 --- a/test/Tools/isac/ProgLang/scrtools.sml Sun Sep 22 15:15:37 2019 +0200
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,351 +0,0 @@
11.4 -(* Title: "ProgLang/scrtools.sml"
11.5 - tests on tools for scripts
11.6 - Author: Walther Neuper 060605
11.7 - (c) due to copyright terms
11.8 -*)
11.9 -"-----------------------------------------------------------------";
11.10 -"table of contents -----------------------------------------------";
11.11 -"-----------------------------------------------------------------";
11.12 -"-------- test the same called by interSteps norm_Poly -----------";
11.13 -"-------- test the same called by interSteps norm_Rational -------";
11.14 -"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
11.15 -"-------- distinguish input to Model -----------------------------------------";
11.16 -"-------- fun subpbl, fun pblterm --------------------------------------------";
11.17 -"-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
11.18 -"-------- fun is_calc, fun op_of_calc ----------------------------------------";
11.19 -"-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
11.20 -"-------- fun op @@ ----------------------------------------------------------";
11.21 -"-------- fun get_fun_id -----------------------------------------------------";
11.22 -"-------- fun rules2scr_Rls --------------------------------------------------";
11.23 -"-----------------------------------------------------------------------------";
11.24 -"-----------------------------------------------------------------------------";
11.25 -"-----------------------------------------------------------------------------";
11.26 -
11.27 -"-------- test the same called by interSteps norm_Poly -----------";
11.28 -"-------- test the same called by interSteps norm_Poly -----------";
11.29 -"-------- test the same called by interSteps norm_Poly -----------";
11.30 -val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";
11.31 -writeln(term2str auto_script);
11.32 -(*Program Stepwise t_t =
11.33 - (Try (Rewrite_Set discard_minus False) @@
11.34 - Try (Rewrite_Set expand_poly_ False) @@
11.35 - Try (Repeat (Calculate TIMES)) @@
11.36 - Try (Rewrite_Set order_mult_rls_ False) @@
11.37 - Try (Rewrite_Set simplify_power_ False) @@
11.38 - Try (Rewrite_Set calc_add_mult_pow_ False) @@
11.39 - Try (Rewrite_Set reduce_012_mult_ False) @@
11.40 - Try (Rewrite_Set order_add_rls_ False) @@
11.41 - Try (Rewrite_Set collect_numerals_ False) @@
11.42 - Try (Rewrite_Set reduce_012_ False) @@
11.43 - Try (Rewrite_Set discard_parentheses1 False))
11.44 - ??.empty ..WORKS, NEVERTHELESS *)
11.45 -atomty auto_script;
11.46 -
11.47 -reset_states (); (*<-- evaluate, if ML-blocks are edited below*)
11.48 -CalcTree
11.49 -[(["Term (b + a - b)", "normalform N"],
11.50 - ("Poly",["polynomial","simplification"],
11.51 - ["simplification","for_polynomials"]))];
11.52 -Iterator 1;
11.53 -moveActiveRoot 1;
11.54 -
11.55 -autoCalculate 1 CompleteCalc;
11.56 -val ((pt,p),_) = get_calc 1;
11.57 -show_pt pt;
11.58 -(* isabisac17 = 15 [
11.59 -(([], Frm), Simplify (b + a - b)),
11.60 -(([1], Frm), b + a - b),
11.61 -(([1], Res), a),
11.62 -(([], Res), a)] *)
11.63 -
11.64 -interSteps 1 ([], Res);
11.65 -val ((pt,p),_) = get_calc 1; show_pt pt;
11.66 -show_pt pt;
11.67 -(* isabisac17 = 15 [
11.68 -(([], Frm), Simplify (b + a - b)),
11.69 -(([1], Frm), b + a - b),
11.70 -(([1], Res), a),
11.71 -(([], Res), a)] *)
11.72 -
11.73 -interSteps 1 ([1], Res);(*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 8</ERROR></SYSERROR>*)
11.74 -"~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1], Res));
11.75 - val ((pt, p), tacis) = get_calc cI;
11.76 -(*if*) (not o is_interpos) ip = false;
11.77 -val ip' = lev_pred' pt ip;
11.78 -
11.79 -(*Math_Engine.detailstep pt ip ..ERROR interSteps>..>init_istate: "norm_Poly" has EmptyScr*)
11.80 -val ("donesteps", ctree_BEFORE_step_into, pos'_BEFORE_step_into) = Math_Engine.detailstep pt ip;
11.81 -"~~~~~ fun detailstep, args:"; val (pt, (pos as (p, _))) = (pt, ip);
11.82 - val nd = Ctree.get_nd pt p
11.83 - val cn = Ctree.children nd;
11.84 -(*if*) null cn = false;
11.85 -
11.86 -"~~~~~ to detailrls return val:";
11.87 -(*else*)
11.88 -val return_val = ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Ctree.Res));
11.89 -if p @ [length (Ctree.children (Ctree.get_nd pt p))] = [1, 4]
11.90 -then () else error "detailrls: auto-generated norm_Poly doesnt work";
11.91 -
11.92 -val ((pt,p),_) = get_calc 1; show_pt pt;
11.93 -show_pt pt; (*[
11.94 -(([], Frm), Simplify (b + a - b)),
11.95 -(([1], Frm), b + a - b),
11.96 -(([1,1], Frm), b + a - b),
11.97 -(([1,1], Res), b + a + -1 * b),
11.98 -(([1,2], Res), a + b + -1 * b),
11.99 -(([1,3], Res), a + 0 * b),
11.100 -(([1,4], Res), a),
11.101 -(([1], Res), a),
11.102 -(([], Res), a)] *)
11.103 -if existpt' ([1,4], Res) pt then ()
11.104 -else error "auto-generated norm_Poly doesnt work";
11.105 -
11.106 -
11.107 -"-------- test the same called by interSteps norm_Rational -------";
11.108 -"-------- test the same called by interSteps norm_Rational -------";
11.109 -"-------- test the same called by interSteps norm_Rational -------";
11.110 -
11.111 -val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Rational";
11.112 -writeln(term2str auto_script);
11.113 -atomty auto_script;
11.114 -(***
11.115 -*** Const (Program.Stepwise, 'z => 'z => 'z)
11.116 -*** . Free (t_t, 'z)
11.117 -*** . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
11.118 -*** . . Const (Program.Try, ('a => 'a) => 'a => 'a)
11.119 -*** . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
11.120 -*** . . . . Free (discard_minus, ID)
11.121 -*** . . . . Const (HOL.False, bool)
11.122 -*** . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
11.123 -*** . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
11.124 -*** . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
11.125 -*** . . . . . Free (rat_mult_poly, ID)
11.126 -*** . . . . . Const (HOL.False, bool)
11.127 -*** . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
11.128 -*** . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
11.129 -*** . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
11.130 -*** . . . . . . Free (make_rat_poly_with_parentheses, ID)
11.131 -*** . . . . . . Const (HOL.False, bool)
11.132 -*** . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
11.133 -*** . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
11.134 -*** . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
11.135 -*** . . . . . . . Free (cancel_p_rls, ID)
11.136 -*** . . . . . . . Const (HOL.False, bool)
11.137 -*** . . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
11.138 -*** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
11.139 -*** . . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
11.140 -*** . . . . . . . . Free (norm_Rational_rls, ID)
11.141 -*** . . . . . . . . Const (HOL.False, bool)
11.142 -*** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
11.143 -*** . . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
11.144 -*** . . . . . . . . Free (discard_parentheses1, ID)
11.145 -*** . . . . . . . . Const (HOL.False, bool)
11.146 -*** . . Const (empty, 'a)
11.147 -***)
11.148 -reset_states ();
11.149 -CalcTree
11.150 -[(["Term (b + a - b)", "normalform N"],
11.151 - ("Poly",["polynomial","simplification"],
11.152 - ["simplification","of_rationals"]))];
11.153 -Iterator 1;
11.154 -moveActiveRoot 1;
11.155 -autoCalculate 1 CompleteCalc;
11.156 -
11.157 -interSteps 1 ([], Res);
11.158 -val ((pt,p),_) = get_calc 1; show_pt pt;
11.159 -
11.160 -interSteps 1 ([1], Res);
11.161 -val ((pt,p),_) = get_calc 1; show_pt pt;
11.162 -
11.163 -(*with "Program SimplifyScript (t_::real) = \
11.164 - \ ((Rewrite_Set norm_Rational False) t_)"
11.165 -val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));
11.166 -*)
11.167 -val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
11.168 -case (term2str form, tac, terms2strs asm) of
11.169 - ("a", Check_Postcond ["polynomial", "simplification"], []) => ()
11.170 - | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work";
11.171 -
11.172 -"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
11.173 -"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
11.174 -"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
11.175 -val rls = assoc_rls "integration";
11.176 -val Seq {scr = Prog auto_script,...} = rls;
11.177 -writeln(term2str auto_script);
11.178 -
11.179 -if contain_bdv (get_rules rls) then ()
11.180 -else error "scrtools.sml: contain_bdv doesnt work for 'integration'";
11.181 -
11.182 -if terms2str (formal_args auto_script) = "[\"t_t\",\"v\"]"
11.183 -then () else error "formal_args of auto-gen.script changed";
11.184 -init_istate (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules"))
11.185 - (str2term "someTermWithBdv");
11.186 -
11.187 -"-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
11.188 -"-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
11.189 -"-------- fun subst_stacexpr, fun stacpbls -----------------------------------";
11.190 -val {scr, ...} = get_met ["Test","sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
11.191 -case stacpbls sc of
11.192 - [Const ("Prog_Tac.Rewrite", _) $ square_equation_left $ Const ("HOL.True", _),
11.193 - Const ("Prog_Tac.Rewrite'_Set", _) $ Test_simplify $ Const ("HOL.False", _),
11.194 - Const ("Prog_Tac.Rewrite'_Set", _) $ rearrange_assoc $ Const ("HOL.False", _),
11.195 - Const ("Prog_Tac.Rewrite'_Set", _) $ isolate_root $ Const ("HOL.False", _),
11.196 - Const ("Prog_Tac.Rewrite'_Set", _) $ norm_equation $ Const ("HOL.False", _),
11.197 - Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $
11.198 - (Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ bdv $ Free ("v_v", _)) $
11.199 - Const ("List.list.Nil", _)) $
11.200 - isolate_bdv $ Const ("HOL.False", _)] =>
11.201 - if HOLogic.dest_string square_equation_left = "square_equation_left" andalso
11.202 - HOLogic.dest_string Test_simplify = "Test_simplify" andalso
11.203 - HOLogic.dest_string rearrange_assoc = "rearrange_assoc" andalso
11.204 - HOLogic.dest_string isolate_root = "isolate_root" andalso
11.205 - HOLogic.dest_string norm_equation = "norm_equation" andalso
11.206 - HOLogic.dest_string bdv = "bdv" andalso
11.207 - HOLogic.dest_string isolate_bdv = "isolate_bdv"
11.208 - then () else error "stacpbls (Test.Solve_root_equation) changed 2"
11.209 -| _ => error "stacpbls (Test.Solve_root_equation) changed 1";
11.210 -
11.211 -(* inappropriate input is skipped *)
11.212 -val t = @{term "(a::real) = (rhs (NTH 1 sol_a))"};
11.213 -case stacpbls t of [] => () | _ => error "stacpbls rhs (NTH 1 sol_a) changed";
11.214 -
11.215 -@{term "(SubProblem (BiegelinieX,[vonBelastungZu,Biegelinien], [Biegelinien,ausBelastung]) [REAL q__q, REAL v_v])"};
11.216 -case stacpbls t of [] => () | _ => error "stacpbls (SubProblem ...) changed";
11.217 -
11.218 -(* --- fun subst_stacexpr *)
11.219 -case subst_stacexpr [] NONE e_term sc of
11.220 -(NONE, Expr (Const ("HOL.eq", _) $
11.221 - (Const ("Test.solve_root_equ", _) $ Free ("e_e", _) $ Free ("v_v", _)) $
11.222 - (Const ("HOL.Let", _) $
11.223 - (Const ("Tactical.Seq", _) $
11.224 - (Const ("Tactical.While", _) $ _ $
11.225 - _ ) $
11.226 - (_) $
11.227 - Free ("e_e", _)) $
11.228 - Abs ("e_e", _, Const ("List.list.Cons", _) $ Free ("e_e", _) $ Const ("List.list.Nil", _)) )
11.229 -)) => ()
11.230 -| _ => error "subst_stacexpr [] NONE e_term";
11.231 -
11.232 -"-------- fun is_calc, fun op_of_calc ----------------------------------------";
11.233 -"-------- fun is_calc, fun op_of_calc ----------------------------------------";
11.234 -"-------- fun is_calc, fun op_of_calc ----------------------------------------";
11.235 -val rls = prep_rls @{theory} Test_simplify; (* adds the Program *)
11.236 -val Prog sc = (#scr o rep_rls) rls;
11.237 -val stacs = stacpbls sc;
11.238 -
11.239 -val calcs = filter is_calc stacs;
11.240 -val ids = map op_of_calc calcs;
11.241 -case ids of
11.242 - ["PLUS", "TIMES", "DIVIDE", "POWER"] => ()
11.243 -| _ => error "op_of_calc";
11.244 -
11.245 -val calcs = ((assoc_calc' @{theory} |> map) o (map Auto_Prog.op_of_calc) o
11.246 - (filter Auto_Prog.is_calc) o Auto_Prog.stacpbls) sc;
11.247 -case calcs of
11.248 - [("PLUS", ("Groups.plus_class.plus", _)), ("TIMES", ("Groups.times_class.times", _)),
11.249 - ("DIVIDE", ("Rings.divide_class.divide", _)), ("POWER", ("Prog_Expr.pow", _))] => ()
11.250 -| _ => error "get_calcs changed"
11.251 -
11.252 -"-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
11.253 -"-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
11.254 -"-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
11.255 -val t = rule2stac @{theory} (Thm ("real_diff_minus", num_str @{thm real_diff_minus}));
11.256 -if term2str t = "Try (Repeat (Rewrite ''real_diff_minus'' False))" then ()
11.257 -else error "rule2stac Thm.. changed";
11.258 -
11.259 -val t = rule2stac @{theory} (Calc ("Groups.plus_class.plus", eval_binop "#add_"));
11.260 -if term2str t = "Try (Repeat (Calculate ''PLUS''))" then ()
11.261 -else error "rule2stac Calc.. changed";
11.262 -
11.263 -val t = rule2stac @{theory} (Rls_ rearrange_assoc);
11.264 -if term2str t = "Try (Rewrite_Set ''rearrange_assoc'' False)" then ()
11.265 -else error "rule2stac Rls_.. changed";
11.266 -
11.267 -val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", num_str @{thm risolate_bdv_add}));
11.268 -if term2str t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'' False))" then ()
11.269 -else error "rule2stac_inst Thm.. changed";
11.270 -case t of
11.271 - (Const ("Tactical.Try", _) $
11.272 - (Const ("Tactical.Repeat", _) $
11.273 - (Const ("Prog_Tac.Rewrite'_Inst", _) $
11.274 - (Const ("List.list.Cons", _) $
11.275 - (Const ("Product_Type.Pair", _) $
11.276 - bdv $
11.277 - Free ("v", _)) $
11.278 - Const ("List.list.Nil", _)) $
11.279 - risolate_bdv_add $
11.280 - Const ("HOL.False", _)))) =>
11.281 - (if HOLogic.dest_string bdv = "bdv" andalso
11.282 - HOLogic.dest_string risolate_bdv_add = "risolate_bdv_add" then ()
11.283 - else error "rule2stac_inst changed 1")
11.284 -| _ => error "rule2stac_inst changed 2"
11.285 -
11.286 -"-------- fun op @@ ----------------------------------------------------------";
11.287 -"-------- fun op @@ ----------------------------------------------------------";
11.288 -"-------- fun op @@ ----------------------------------------------------------";
11.289 - val rules = (#rules o rep_rls) isolate_root;
11.290 - val rs = map (rule2stac @{theory}) rules;
11.291 - val t = @@ rs;
11.292 -if term2str t = "Try (Repeat (Rewrite ''rroot_to_lhs'' False)) @@\n" ^
11.293 - "Try (Repeat (Rewrite ''rroot_to_lhs_mult'' False)) @@\n" ^
11.294 - "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'' False)) @@\n" ^
11.295 - "Try (Repeat (Rewrite ''risolate_root_add'' False)) @@\n" ^
11.296 - "Try (Repeat (Rewrite ''risolate_root_mult'' False)) @@\n" ^
11.297 - "Try (Repeat (Rewrite ''risolate_root_div'' False))"
11.298 -then () else error "fun @@ changed"
11.299 -
11.300 -"-------- fun get_fun_id -----------------------------------------------------";
11.301 -"-------- fun get_fun_id -----------------------------------------------------";
11.302 -"-------- fun get_fun_id -----------------------------------------------------";
11.303 -(* fun_id is nested into arguments, compare ... *)
11.304 -val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
11.305 - (((((((Const (const_id, const_typ) $ _) $ _) $ _) $ _) $ _) $ _) $ _) $ _) =
11.306 - Thm.prop_of @{thm biegelinie.simps};
11.307 -(* ... to: *)
11.308 -val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
11.309 - (Const (const_id, const_typ) $ _) $ _) =
11.310 - Thm.prop_of @{thm simplify.simps};
11.311 -
11.312 -(* get fun_id out of nesting *)
11.313 -val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
11.314 - nested $ _) =
11.315 - Thm.prop_of @{thm biegelinie.simps};
11.316 -val (Const ("Biegelinie.biegelinie", _) $
11.317 - Var (("l", 0), _) $
11.318 - Var (("q", 0), _) $
11.319 - Var (("v", 0), _) $
11.320 - Var (("b", 0), _) $
11.321 - Var (("s", 0), _) $
11.322 - Var (("vs", 0), _) $
11.323 - Var (("id_abl", 0), _)) = nested;
11.324 -strip_comb nested;
11.325 -(*val it =
11.326 - (Const ("Biegelinie.biegelinie", "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> bool")
11.327 - ,
11.328 - [Var (("l", 0), "real"), Var (("q", 0), "real"), Var (("v", 0), "real"),
11.329 - Var (("b", 0), "real \<Rightarrow> real"), Var (("s", 0), "bool list")]):
11.330 - term * term list*)
11.331 -
11.332 -case get_fun_id (prep_program @{thm biegelinie.simps}) of
11.333 - ("Biegelinie.biegelinie", _) => ()
11.334 -| _ => error "get_fun_id changed";
11.335 -case get_fun_id (prep_program @{thm simplify.simps}) of
11.336 - ("PolyMinus.simplify", _) => ()
11.337 -| _ => error "get_fun_id changed";
11.338 -
11.339 -"-------- fun rules2scr_Rls --------------------------------------------------";
11.340 -"-------- fun rules2scr_Rls --------------------------------------------------";
11.341 -"-------- fun rules2scr_Rls --------------------------------------------------";
11.342 -(*compare Prog_Expr.*)
11.343 -val prog = Auto_Prog.rules2scr_Rls @{theory} [Rule.Thm ("thm111", @{thm thm111}), Rule.Thm ("refl", @{thm refl})]
11.344 -;
11.345 -writeln (t2str @{theory} prog);
11.346 -(*auto_generated t_t =
11.347 -Repeat
11.348 - ((Try (Repeat (Rewrite ''thm111'' False)) @@
11.349 - Try (Repeat (Rewrite ''refl'' False)))
11.350 - ??.empty)*)
11.351 -;
11.352 -if t2str @{theory} prog =
11.353 -"auto_generated t_t =\nRepeat\n ((Try (Repeat (Rewrite ''thm111'' False)) @@\n Try (Repeat (Rewrite ''refl'' False)))\n ??.empty)"
11.354 -then () else error "rules2scr_Rls auto_generated changed"
12.1 --- a/test/Tools/isac/ProgLang/scrtools.thy Sun Sep 22 15:15:37 2019 +0200
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,75 +0,0 @@
12.4 -
12.5 -theory scrtools
12.6 -imports Isac.Build_Thydata
12.7 -begin
12.8 -
12.9 -subsection \<open> Compare with scrtools.sml: "--- test auto-generated script" \<close>
12.10 -
12.11 -partial_function (tailrec) stepwise_test :: "real => real"
12.12 - where
12.13 -"stepwise_test t_t =
12.14 - (Try (Rewrite_Set ''discard_minus'' False) @@
12.15 - Try (Rewrite_Set ''expand_poly'' False) @@
12.16 - Try (Repeat (Calculate ''TIMES'')) @@
12.17 - Try (Rewrite_Set ''order_mult_rls'' False) @@
12.18 - Try (Rewrite_Set ''simplify_power'' False) @@
12.19 - Try (Rewrite_Set ''calc_add_mult_pow'' False) @@
12.20 - Try (Rewrite_Set ''reduce_012_mult'' False) @@
12.21 - Try (Rewrite_Set ''order_add_rls'' False) @@
12.22 - Try (Rewrite_Set ''collect_numerals'' False) @@
12.23 - Try (Rewrite_Set ''reduce_012'' False) @@
12.24 - Try (Rewrite_Set ''discard_parentheses'' False))
12.25 - t_t"
12.26 -setup \<open>KEStore_Elems.add_mets
12.27 - [Specify.prep_met @{theory "Test"} "met_testinter" [] Celem.e_metID
12.28 - (["Test","test_interSteps_1"],
12.29 - [("#Given" ,["Term t_t"]), ("#Find" ,["normalform n_n"])],
12.30 - {rew_ord' = "dummy_ord", rls' = tval_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
12.31 - crls=tval_rls, errpats = [], nrls = Rule.e_rls},
12.32 - @{thm stepwise_test.simps}
12.33 - (*"Program Stepwise t_t = \
12.34 - \(Try (Rewrite_Set ''discard_minus'' False) @@ \
12.35 - \ Try (Rewrite_Set ''expand_poly'' False) @@ \
12.36 - \ Try (Repeat (Calculate ''TIMES'')) @@ \
12.37 - \ Try (Rewrite_Set ''order_mult_rls'' False) @@ \
12.38 - \ Try (Rewrite_Set ''simplify_power'' False) @@ \
12.39 - \ Try (Rewrite_Set ''calc_add_mult_pow'' False) @@ \
12.40 - \ Try (Rewrite_Set ''reduce_012_mult'' False) @@ \
12.41 - \ Try (Rewrite_Set ''order_add_rls'' False) @@ \
12.42 - \ Try (Rewrite_Set ''collect_numerals'' False) @@ \
12.43 - \ Try (Rewrite_Set ''reduce_012'' False) @@ \
12.44 - \ Try (Rewrite_Set ''discard_parentheses'' False)) \
12.45 - \ t_t"*)
12.46 - (*presently this script cannot become equal in types to auto_script, because:
12.47 - this t_t must be either 'real' or 'bool' #1#,
12.48 - while the auto_script must be 'z and type-instantiated before usage*))]
12.49 -\<close>
12.50 -text \<open> see scrtools.sml "--- test auto-generated script" \<close>
12.51 -
12.52 -subsection \<open> Handle Var from parsing by partial_function \<close>
12.53 -partial_function (tailrec) xxx ::
12.54 - "bool \<Rightarrow> bool list"
12.55 - where
12.56 - "xxx e_e = (let e_e = (Rewrite_Set ''yyy'' False) e_e in [e_e])"
12.57 -text \<open> see scrtools.sml "--- Handle Var from parsing by partial_function" \<close>
12.58 -
12.59 -subsection \<open> Compare program terms: from old parsing | from partial_function \<close>
12.60 -partial_function (tailrec) minisubpbl ::
12.61 - "bool \<Rightarrow> real \<Rightarrow> bool list"
12.62 -where "minisubpbl e_e v_v =
12.63 - (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@
12.64 - (Try (Rewrite_Set ''Test_simplify'' False))) e_e;
12.65 - (L_L::bool list) =
12.66 - (SubProblem (''TestX'',
12.67 - [''LINEAR'', ''univariate'', ''equation'', ''test''],
12.68 - [''Test'', ''solve_linear''])
12.69 - [BOOL e_e, REAL v_v])
12.70 - in Check_elementwise L_L {(v_v::real). Assumptions})"
12.71 -
12.72 -thm "minisubpbl.simps"
12.73 -
12.74 -ML \<open>
12.75 -\<close> ML \<open>
12.76 -\<close>
12.77 -
12.78 -end
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/test/Tools/isac/ProgLang/tactical.sml Sun Sep 22 16:52:14 2019 +0200
13.3 @@ -0,0 +1,20 @@
13.4 +(* Title: ProgLang/tactical.sml
13.5 + Author: Walther Neuper 190922
13.6 + (c) due to copyright terms
13.7 +*)
13.8 +
13.9 +"-----------------------------------------------------------------------------------------------";
13.10 +"-----------------------------------------------------------------------------------------------";
13.11 +"table of contents -----------------------------------------------------------------------------";
13.12 +"-----------------------------------------------------------------------------------------------";
13.13 +"-------- xxx ------";
13.14 +"-------- xxx ------";
13.15 +"-------- xxx ------";
13.16 +"-----------------------------------------------------------------------------------------------";
13.17 +"-----------------------------------------------------------------------------------------------";
13.18 +"-----------------------------------------------------------------------------------------------";
13.19 +
13.20 +
13.21 +"-------- xxx ------";
13.22 +"-------- xxx ------";
13.23 +"-------- xxx ------";
14.1 --- a/test/Tools/isac/Test_Isac_Short.thy Sun Sep 22 15:15:37 2019 +0200
14.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Sun Sep 22 16:52:14 2019 +0200
14.3 @@ -81,10 +81,6 @@
14.4 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
14.5 "~~/test/Tools/isac/Interpret/ptyps" (* setup for ptyps.sml *)
14.6 "~~/test/Tools/isac/ProgLang/calculate" (* setup for calculate.sml*)
14.7 -
14.8 -
14.9 -
14.10 - "~~/test/Tools/isac/ProgLang/scrtools" (* setup for scrtools.sml *)
14.11 "~~/test/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
14.12 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
14.13 (*"~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) Test_Isac_Short*)
14.14 @@ -155,14 +151,20 @@
14.15 subsection \<open>basic code first\<close>
14.16 ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>
14.17 ML_file "CalcElements/libraryC.sml"
14.18 + ML_file "CalcElements/rule.sml"
14.19 ML_file "CalcElements/calcelems.sml"
14.20 + ML_file "CalcElements/termC.sml"
14.21 + ML_file "CalcElements/contextC.sml"
14.22 + ML_file "CalcElements/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
14.23 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
14.24 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
14.25 - ML_file "CalcElements/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
14.26 - ML_file "CalcElements/termC.sml"
14.27 - ML_file "CalcElements/listC.sml"
14.28 - ML_file "CalcElements/contextC.sml"
14.29 ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *)
14.30 + ML_file "ProgLang/listC.sml"
14.31 + ML_file "ProgLang/prog_expr.sml"
14.32 + ML_file "ProgLang/program.sml"
14.33 + ML_file "ProgLang/prog_tac.sml"
14.34 + ML_file "ProgLang/tactical.sml"
14.35 + ML_file "ProgLang/auto_prog.sml"
14.36 ML_file "ProgLang/rewrite.sml"
14.37 ML_file "ProgLang/scrtools.sml"
14.38 ML_file "ProgLang/tools.sml"