1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Mon Apr 19 11:45:43 2021 +0200
1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Mon Apr 19 15:02:00 2021 +0200
1.3 @@ -27,7 +27,7 @@
1.4
1.5
1.6 (*
1.7 -> val t = (Thm.term_of o the o (parse thy)) "#2^^^#3";
1.8 +> val t = (Thm.term_of o the o (TermC.parse thy)) "#2^^^#3";
1.9 > val eval_fn = the (LibraryC.assoc (!eval_list, "pow"));
1.10 > val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
1.11 > Syntax.string_of_term (ThyC.to_ctxt thy) t';
1.12 @@ -101,7 +101,7 @@
1.13 "solutions L::real set" ,
1.14 "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
1.15 val thy = (theory "Isac_Knowledge");
1.16 -val formals = map (the o (parse thy)) origin;
1.17 +val formals = map (the o (TermC.parse thy)) origin;
1.18
1.19 val given = ["equation (l=(r::real))",
1.20 "bound_variable bdv", (* TODO type *)
1.21 @@ -112,13 +112,13 @@
1.22 val find = ["solutions (L::bool list)"];
1.23 val with_ = [(* parseold ...
1.24 "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
1.25 -val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1.26 -val givens = map (the o (parse thy)) given;
1.27 +val chkpbl = map (the o (TermC.parse thy)) (given @ where_ @ find @ with_);
1.28 +val givens = map (the o (TermC.parse thy)) given;
1.29 parseold thy "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < apx}";
1.30
1.31 " --- subproblem 2: linear-equation --- ";
1.32 val origin = ["x + 4 = (0::real)", "x::real"];
1.33 -val formals = map (the o (parse thy)) origin;
1.34 +val formals = map (the o (TermC.parse thy)) origin;
1.35
1.36 val given = ["equation (l=(0::real))",
1.37 "bound_variable bdv"];
1.38 @@ -126,13 +126,13 @@
1.39 val find = ["l::real"];
1.40 val with_ = ["l = (%x. l) bdv"];
1.41 val chkpbl = map (the o (parseold thy)) (given @ where_ @ find @ with_);
1.42 -val givens = map (the o (parse thy)) given;
1.43 +val givens = map (the o (TermC.parse thy)) given;
1.44
1.45
1.46 " _________________ rewrite_ x+4_________________ ";
1.47 " _________________ rewrite_ x+4_________________ ";
1.48 " _________________ rewrite_ x+4_________________ ";
1.49 -val t = (Thm.term_of o the o (parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
1.50 +val t = (Thm.term_of o the o (TermC.parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
1.51 val thm = ThmC.numerals_to_Free @{thm square_equation_left};
1.52 val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t);
1.53 val rls = Test_simplify;
1.54 @@ -187,7 +187,7 @@
1.55 val rls = Test_simplify;
1.56 val (t,_) = the (rewrite_set_ thy false rls t);
1.57 val rls = isolate_bdv;
1.58 -val subst = [(str2term "bdv", str2term "x")];
1.59 +val subst = [(TermC.str2term "bdv", TermC.str2term "x")];
1.60 val (t,_) = the (rewrite_set_inst_ thy false subst rls t);
1.61 val rls = Test_simplify;
1.62 val (t,_) = the (rewrite_set_ thy false rls t);
1.63 @@ -200,8 +200,8 @@
1.64 " _________________ rewrite x=4_________________ ";
1.65 (*
1.66 rewrite thy' "tless_true" "tval_rls" true (ThmC.numerals_to_Free @{thm rbinom_power_2}) ct;
1.67 -atomty (Thm.prop_of (!tthm));
1.68 -atomty (Thm.term_of (!tct));
1.69 +TermC.atomty (Thm.prop_of (!tthm));
1.70 +TermC.atomty (Thm.term_of (!tct));
1.71 *)
1.72 val thy' = "Test";
1.73 val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
1.74 @@ -248,7 +248,7 @@
1.75 " _________________ rewrite + cappend _________________ ";
1.76 " _________________ rewrite + cappend _________________ ";
1.77 val thy' = "Test";
1.78 -val ct = str2term"sqrt(9+4*x)=sqrt x + sqrt(5+x)";
1.79 +val ct = TermC.str2term"sqrt(9+4*x)=sqrt x + sqrt(5+x)";
1.80 val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)", "x::real", "0"];
1.81 val oris = O_Model.init ctl thy
1.82 ((#ppc o Problem.from_store)
1.83 @@ -291,70 +291,70 @@
1.84 val pos = (lev_on o lev_dn) pos;
1.85 val thm = ("square_equation_left", ""); val ctold = ct;
1.86 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm (UnparseC.term ct));
1.87 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac (fst thm)) (str2term ct,[])Complete;
1.88 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac (fst thm)) (TermC.str2term ct,[])Complete;
1.89 (*val pt = union_asm pt [] (map (rpair []) asm);*)
1.90
1.91 val pos = lev_on pos;
1.92 -val rls = ("Test_simplify"); val ctold = str2term ct;
1.93 +val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
1.94 val (ct,_) = the (rewrite_set thy' false rls ct);
1.95 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
1.96 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.97
1.98 val pos = lev_on pos;
1.99 -val rls = ("rearrange_assoc"); val ctold = str2term ct;
1.100 +val rls = ("rearrange_assoc"); val ctold = TermC.str2term ct;
1.101 val (ct,_) = the (rewrite_set thy' false rls ct);
1.102 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
1.103 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.104
1.105 val pos = lev_on pos;
1.106 -val rls = ("isolate_root"); val ctold = str2term ct;
1.107 +val rls = ("isolate_root"); val ctold = TermC.str2term ct;
1.108 val (ct,_) = the (rewrite_set thy' false rls ct);
1.109 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
1.110 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.111
1.112 val pos = lev_on pos;
1.113 -val rls = ("Test_simplify"); val ctold = str2term ct;
1.114 +val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
1.115 val (ct,_) = the (rewrite_set thy' false rls ct);
1.116 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
1.117 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.118
1.119 val pos = lev_on pos;
1.120 -val thm = ("square_equation_left", ""); val ctold = str2term ct;
1.121 +val thm = ("square_equation_left", ""); val ctold = TermC.str2term ct;
1.122 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
1.123 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
1.124 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.125 (*val pt = union_asm pt [] (map (rpair []) asm);*)
1.126
1.127 val pos = lev_up pos;
1.128 -val (pt,_) = append_result pt pos Istate.empty (str2term ct,[]) Complete;
1.129 +val (pt,_) = append_result pt pos Istate.empty (TermC.str2term ct,[]) Complete;
1.130
1.131 val pos = lev_on pos;
1.132 -val rls = ("Test_simplify"); val ctold = str2term ct;
1.133 +val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
1.134 val (ct,_) = the (rewrite_set thy' false rls ct);
1.135 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
1.136 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.137
1.138 val pos = lev_on pos;
1.139 -val rls = ("norm_equation"); val ctold = str2term ct;
1.140 +val rls = ("norm_equation"); val ctold = TermC.str2term ct;
1.141 val (ct,_) = the (rewrite_set thy' false rls ct);
1.142 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
1.143 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.144
1.145 val pos = lev_on pos;
1.146 -val rls = ("Test_simplify"); val ctold = str2term ct;
1.147 +val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
1.148 val (ct,_) = the (rewrite_set thy' false rls ct);
1.149 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
1.150 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.151
1.152 (* --- see comments in interface_ME_ISA/instantiate''
1.153 val rlsdat' = instantiate_rls' thy' [("bdv", "x")] ("isolate_bdv");
1.154 val (ct,_) = the (rewrite_set thy' false
1.155 ("#isolate_bdv",rlsdat') ct); *)
1.156 val pos = lev_on pos;
1.157 -val rls = ("isolate_bdv"); val ctold = str2term ct;
1.158 +val rls = ("isolate_bdv"); val ctold = TermC.str2term ct;
1.159 val (ct,_) = the (rewrite_set_inst thy' false
1.160 [("bdv", "x")] rls ct);
1.161 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
1.162 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.163
1.164 val pos = lev_on pos;
1.165 -val rls = ("Test_simplify"); val ctold = str2term ct;
1.166 +val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
1.167 val (ct,_) = the (rewrite_set thy' false rls ct);
1.168 -val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
1.169 +val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
1.170
1.171 val pos = lev_up pos;
1.172 -val (pt,pos) = append_result pt pos Istate.empty (str2term ct,[]) Complete;
1.173 +val (pt,pos) = append_result pt pos Istate.empty (TermC.str2term ct,[]) Complete;
1.174 Ctree.get_assumptions pt ([],Res);
1.175
1.176 writeln (pr_ctree pr_short pt);
1.177 @@ -375,8 +375,8 @@
1.178 *)
1.179
1.180 (*
1.181 -val t = (Thm.term_of o the o (parse thy)) "solutions (L::real set)";
1.182 -atomty t;
1.183 +val t = (Thm.term_of o the o (TermC.parse thy)) "solutions (L::real set)";
1.184 +TermC.atomty t;
1.185 *)
1.186
1.187
1.188 @@ -530,7 +530,7 @@
1.189 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.190
1.191 (*.9.6.03
1.192 - val t = str2term "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";
1.193 + val t = TermC.str2term "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";
1.194 val SOME (t',asm) = rewrite_set_ thy false rls t;
1.195 UnparseC.term t';
1.196 > Rewrite.trace_on:=true;
1.197 @@ -557,7 +557,7 @@
1.198
1.199
1.200
1.201 -val ttt = (Thm.term_of o the o (parse Test.thy))
1.202 +val ttt = (Thm.term_of o the o (TermC.parse Test.thy))
1.203 "Let (((While contains_root e_e Do\
1.204 \Rewrite square_equation_left #>\
1.205 \Try (Rewrite_Set Test_simplify) #>\