1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Tue Jul 20 14:37:56 2021 +0200
1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Tue Jul 27 11:21:14 2021 +0200
1.3 @@ -44,7 +44,6 @@
1.4 "-----------------------------------------------------------------";
1.5
1.6
1.7 -(*TOODOO broken with "reduce the number of TermC.parse*"------------------------------------\\
1.8 "--------- appendFormula: on Res + equ_nrls ----------------------";
1.9 "--------- appendFormula: on Res + equ_nrls ----------------------";
1.10 "--------- appendFormula: on Res + equ_nrls ----------------------";
1.11 @@ -169,7 +168,6 @@
1.12 if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
1.13 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
1.14 DEconstrCalcTree 1;
1.15 ------ broken with "reduce the number of TermC.parse*"---------------------------------------//*)
1.16
1.17 "--------- appendFormula: on Res + NO deriv ----------------------";
1.18 "--------- appendFormula: on Res + NO deriv ----------------------";
1.19 @@ -201,7 +199,6 @@
1.20 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
1.21 DEconstrCalcTree 1;
1.22
1.23 -(*TOODOO broken with "reduce the number of TermC.parse*"------------------------------------\\
1.24 "--------- appendFormula: on Res + late deriv --------------------";
1.25 "--------- appendFormula: on Res + late deriv --------------------";
1.26 "--------- appendFormula: on Res + late deriv --------------------";
1.27 @@ -258,9 +255,7 @@
1.28 (* ~~~~~~~~~~ simplify as last step in any script ?!*)
1.29 else error "inform.sml: diff.behav.appendFormula: Res + latEE 2";
1.30 DEconstrCalcTree 1;
1.31 ------ broken with "reduce the number of TermC.parse*"---------------------------------------//*)
1.32
1.33 -(*TOODOO broken with "reduce the number of TermC.parse*"------------------------------------\\
1.34 "--------- replaceFormula: on Res + = ----------------------------";
1.35 "--------- replaceFormula: on Res + = ----------------------------";
1.36 "--------- replaceFormula: on Res + = ----------------------------";
1.37 @@ -306,9 +301,7 @@
1.38 if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst) (get_obj g_result pt p) then()
1.39 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
1.40 DEconstrCalcTree 1;
1.41 ------ broken with "reduce the number of TermC.parse*"---------------------------------------//*)
1.42
1.43 -(*TOODOO broken with "reduce the number of TermC.parse*"------------------------------------\\
1.44 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
1.45 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
1.46 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
1.47 @@ -332,7 +325,6 @@
1.48 if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then()
1.49 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
1.50 DEconstrCalcTree 1;
1.51 ------ broken with "reduce the number of TermC.parse*"---------------------------------------//*)
1.52
1.53 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
1.54 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
1.55 @@ -348,18 +340,14 @@
1.56 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
1.57 val ((pt,_),_) = get_calc 1;
1.58 val str = pr_ctree pr_short pt;
1.59 -(*TOODOO broken with "reduce the number of TermC.parse*"------------------------------------\\
1.60 - str = ". ----- pblobj -----\n1. x + 1 = 2\n";
1.61 -
1.62 + writeln str;
1.63 if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = - 2 + 4\n1.4. x + 1 = - 2 + 4\n" then ()
1.64 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
1.65 autoCalculate 1 CompleteCalc;
1.66 val ((pt,pos as (p,_)),_) = get_calc 1;
1.67 -(**)pos = ([1], Met)
1.68 if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then()
1.69 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
1.70 DEconstrCalcTree 1;
1.71 ------ broken with "reduce the number of TermC.parse*"---------------------------------------//*)
1.72
1.73 "--------- replaceFormula: cut calculation -----------------------";
1.74 "--------- replaceFormula: cut calculation -----------------------";
1.75 @@ -378,11 +366,8 @@
1.76 val ((pt,p),_) = get_calc 1;
1.77 val str = pr_ctree pr_short pt;
1.78 writeln str;
1.79 -(*TOODOO broken with "reduce the number of TermC.parse*"------------------------------------\\
1.80 - p = ([], Res)
1.81 if p = ([1], Res) then ()
1.82 else error "inform.sml: diff.behav. cut calculation 2";
1.83 ------ broken with "reduce the number of TermC.parse*"---------------------------------------//*)
1.84
1.85
1.86 (* 040307 copied from informtest.sml; ... old version
1.87 @@ -486,12 +471,8 @@
1.88 "--------- CAS-command on ([],Pbl) -------------------------------";
1.89 val (p,_,f,nxt,_,pt) =
1.90 CalcTreeTEST [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
1.91 -val ifo = "solve (x + 1 = (2::real), x::real)";
1.92 -(*TOODOO broken with "reduce the number of TermC.parse*"------------------------------------\\
1.93 -ERROR lev_back': called by ([],_)
1.94 -
1.95 -val (_,(_,c,(pt,p))) = Step_Solve.by_term (pt,p) "solve (x + 1 = (2::real), x::real)";
1.96 ------ broken with "reduce the number of TermC.parse*"---------------------------------------//*)
1.97 +val ifo = "solve(x+1=2,x)";
1.98 +val (_,(_,c,(pt,p))) = Step_Solve.by_term (pt,p) "solve(x+1=2,x)";
1.99 (*
1.100 This trick \<up> \<up> \<up> micked input of \<up> \<up> \<up> \<up> \<up> ^^ in the front-end.
1.101 The trick worked in changeset fbaff8cf0179, it does not work in 59c5dd27d589 anymore
1.102 @@ -514,17 +495,13 @@
1.103 CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
1.104 Iterator 1;
1.105 moveActiveRoot 1;
1.106 -replaceFormula 1 "solve(x + 1 = (2::real), x)";
1.107 +replaceFormula 1 "solve(x+1=2,x)";
1.108 autoCalculate 1 CompleteCalc;
1.109 val ((pt,p),_) = get_calc 1;
1.110 Test_Tool.show_pt pt;
1.111 -(*TOODOO broken with "reduce the number of TermC.parse*"------------------------------------\\
1.112 - p = ([], Pbl)
1.113 -
1.114 if p = ([], Res) then ()
1.115 else error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
1.116 DEconstrCalcTree 1;
1.117 ------ broken with "reduce the number of TermC.parse*"---------------------------------------//*)
1.118
1.119 "--------- inform [rational,simplification] ----------------------";
1.120 "--------- inform [rational,simplification] ----------------------";
1.121 @@ -574,10 +551,6 @@
1.122 (([2], Res), (a * d + c * b) / (b * d) + e / f)]
1.123 *)
1.124 val ((pt,p),_) = get_calc 1;
1.125 -
1.126 -(*TOODOO broken with "reduce the number of TermC.parse*"------------------------------------\\* )
1.127 - p = ([9], Res)
1.128 -
1.129 if p = ([2], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
1.130 else error ("inform.sml: [rational,simplification] 1");
1.131
1.132 @@ -660,7 +633,6 @@
1.133 (([], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f))]
1.134 *)
1.135 DEconstrCalcTree 1;
1.136 ------ broken with "reduce the number of TermC.parse*"------------------------------------//*)
1.137
1.138 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
1.139 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
1.140 @@ -1054,7 +1026,8 @@
1.141 "~~~~~ fun Step_Solve.by_term , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Calc.state_post), istr)
1.142 = (cs', (encode ifo));
1.143 val ctxt = get_ctxt pt pos (*see TODO.thy*)
1.144 - val SOME f_in = (*case*) TermC.parseNEW (ThyC.id_to_ctxt "Isac_Knowledge") istr (*of*);
1.145 + val SOME f_in = (*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*);
1.146 + val f_in = Thm.term_of f_in
1.147 val pos_pred = lev_back' pos
1.148 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
1.149 (*if*) f_pred = f_in; (*else*)