1.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Jun 21 22:08:01 2021 +0200
1.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Sun Jul 18 18:15:27 2021 +0200
1.3 @@ -210,7 +210,7 @@
1.4
1.5 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_''' p'''''_''' [] pt'''''_'''; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
1.6 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
1.7 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + x = 0)"*)
1.8 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
1.9 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
1.10 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
1.11 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
1.12 @@ -228,10 +228,10 @@
1.13 if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
1.14 ". ----- pblobj -----\n" ^
1.15 "1. x + 1 = 2\n" ^
1.16 - "2. x + 1 + -1 * 2 = 0\n" ^
1.17 + "2. x + 1 + - 1 * 2 = 0\n" ^
1.18 "3. ----- pblobj -----\n" ^
1.19 - "3.1. -1 + x = 0\n" ^
1.20 - "3.2. x = 0 + -1 * -1\n" ^
1.21 + "3.1. - 1 + x = 0\n" ^
1.22 + "3.2. x = 0 + - 1 * - 1\n" ^
1.23 "4. [x = 1]\n"
1.24 then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_tactic changed 1"
1.25 else error "re-build: fun locate_input_tactic changed 2";
1.26 @@ -249,28 +249,40 @@
1.27 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.28 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.29 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
1.30 +
1.31 +(*+*)val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f
1.32 +
1.33 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
1.34
1.35 +(*+*)val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f;
1.36 +
1.37 (*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
1.38 ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
1.39 - "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")"]
1.40 - then () else error "specific_from_prog ([1], Res) CHANGED";
1.41 + "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
1.42 +(*this is new since ThmC.numerals_to_Free..*)
1.43 + "Calculate PLUS"]
1.44 + then () else error "specific_from_prog ([1], Res) CHANGED"; (*GOON*)
1.45 (*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
1.46
1.47 (*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
1.48 - ["Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")", "Rewrite (\"tausche_plus_minus\", \"?b kleiner ?c \<Longrightarrow> ?a + ?c - ?b = ?a - ?b + ?c\")",
1.49 + ["Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")",
1.50 + "Rewrite (\"tausche_plus_minus\", \"?b kleiner ?c \<Longrightarrow> ?a + ?c - ?b = ?a - ?b + ?c\")",
1.51 "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
1.52 - "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", "Calculate MINUS"]
1.53 + "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
1.54 + "Calculate PLUS", (*..this is new since ThmC.numerals_to_Free*)
1.55 + "Calculate MINUS"]
1.56 then () else error "specific_from_prog ([1], Res) CHANGED";
1.57 +
1.58 (* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
1.59
1.60 (*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
1.61 -(** )val ("ok", (_, _, ptp as (pt, p))) =( **)
1.62 +(** )val ("ok", ([(Rewrite ("tausche_minus_plus", _), _, _)], _, _)) = ( *isa*)
1.63 Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
1.64 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (hd (specific_from_prog pt p), (pt, p));
1.65 val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
1.66 (*if*) Tactic.for_specify' m; (*false*)
1.67
1.68 +(** )val ("ok", ([(Rewrite ("tausche_minus_plus", _), _, _)], _, _)) = ( *isa*)
1.69 Step_Solve.by_tactic m (pt, p);
1.70 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
1.71 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
1.72 @@ -329,6 +341,9 @@
1.73 val LItool.Not_Associated = (*case*)
1.74 LItool.associate pt ctxt (tac, prog_tac) (*of*);
1.75 val _(*ORundef*) = (*case*) or (*of*);
1.76 +
1.77 +(*+*)Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p);
1.78 +
1.79 val Applicable.Yes m' =
1.80 (*case*) Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p) (*of*);
1.81
1.82 @@ -361,6 +376,8 @@
1.83 then () else error "locate_input_tactic Helpless, but applicable CHANGED";
1.84 ( *\----- original before child of 7e314dd233fd -------------------------------------------------/*)
1.85
1.86 +(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt'''''; (*nxt = Rewrite_Set "fasse_zusammen"*)
1.87 +
1.88
1.89 "----------- re-build: fun find_next_step, mini ------------------------------------------------";
1.90 "----------- re-build: fun find_next_step, mini ------------------------------------------------";
1.91 @@ -524,14 +541,14 @@
1.92 (*+*)if f2str f = "x + 1 = 2" then () else error "locate_input_term at ([1], Frm) CHANGED";
1.93
1.94 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "Test_simplify"*)
1.95 -(*+*)if f2str f = "x + 1 + -1 * 2 = 0" then () else error "locate_input_term at ([1], Frm) CHANGED";
1.96 +(*+*)if f2str f = "x + 1 + - 1 * 2 = 0" then () else error "locate_input_term at ([1], Frm) CHANGED";
1.97
1.98 Test_Tool.show_pt_tac pt; (*[
1.99 ([], Frm), solve (x + 1 = 2, x)
1.100 . . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
1.101 ([1], Frm), x + 1 = 2
1.102 . . . . . . . . . . Rewrite_Set "norm_equation",
1.103 -([1], Res), x + 1 + -1 * 2 = 0 ///Check_Postcond..ERROR*)
1.104 +([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond..ERROR*)
1.105
1.106 (*//---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------\\*)
1.107 "~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: TermC.as_string) = ((**) "x = 1");
1.108 @@ -545,7 +562,7 @@
1.109 (*+*). . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
1.110 (*+*)([1], Frm), x + 1 = 2
1.111 (*+*). . . . . . . . . . Rewrite_Set "norm_equation",
1.112 -(*+*)([1], Res), x + 1 + -1 * 2 = 0 ///Check_Postcond*)
1.113 +(*+*)([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond*)
1.114
1.115 val ("ok", cs' as (_, _, ptp')) =
1.116 (*case*) Step.do_next pos cs (*of*);
1.117 @@ -602,7 +619,7 @@
1.118 (*//----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----\\* )
1.119 (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
1.120 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
1.121 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + x = 0)"*)
1.122 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
1.123 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
1.124 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
1.125 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
1.126 @@ -622,11 +639,11 @@
1.127 if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
1.128 ". ----- pblobj -----\n" ^
1.129 "1. x + 1 = 2\n" ^
1.130 - "2. x + 1 + -1 * 2 = 0\n" ^
1.131 + "2. x + 1 + - 1 * 2 = 0\n" ^
1.132 "3. ----- pblobj -----\n" ^
1.133 - "3.1. -1 + x = 0\n" ^
1.134 - "3.2. x = 0 + -1 * -1\n" ^
1.135 - "3.2.1. x = 0 + -1 * -1\n" ^
1.136 + "3.1. - 1 + x = 0\n" ^
1.137 + "3.2. x = 0 + - 1 * - 1\n" ^
1.138 + "3.2.1. x = 0 + - 1 * - 1\n" ^
1.139 "3.2.2. x = 0 + 1\n" (*ATTENTION: see complete Calc below*)
1.140 then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_term CHANGED 1"
1.141 else error "re-build: fun locate_input_term CHANGED 2";
1.142 @@ -636,18 +653,18 @@
1.143 . . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
1.144 ([1], Frm), x + 1 = 2
1.145 . . . . . . . . . . Rewrite_Set "norm_equation",
1.146 -([1], Res), x + 1 + -1 * 2 = 0
1.147 +([1], Res), x + 1 + - 1 * 2 = 0
1.148 . . . . . . . . . . Rewrite_Set "Test_simplify",
1.149 -([2], Res), -1 + x = 0
1.150 +([2], Res), - 1 + x = 0
1.151 . . . . . . . . . . Subproblem (Test, ["LINEAR", "univariate", "equation", "test"]),
1.152 -([3], Pbl), solve (-1 + x = 0, x)
1.153 +([3], Pbl), solve (- 1 + x = 0, x)
1.154 . . . . . . . . . . Apply_Method ["Test", "solve_linear"],
1.155 -([3,1], Frm), -1 + x = 0
1.156 +([3,1], Frm), - 1 + x = 0
1.157 . . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv"),
1.158 -([3,1], Res), x = 0 + -1 * -1
1.159 +([3,1], Res), x = 0 + - 1 * - 1
1.160 . . . . . . . . . . Derive Test_simplify,
1.161 -([3,2,1], Frm), x = 0 + -1 * -1
1.162 -. . . . . . . . . . Rewrite ("#: -1 * -1 = 1", "-1 * -1 = 1"),
1.163 +([3,2,1], Frm), x = 0 + - 1 * - 1
1.164 +. . . . . . . . . . Rewrite ("#: - 1 * - 1 = 1", "- 1 * - 1 = 1"),
1.165 ([3,2,1], Res), x = 0 + 1
1.166 . . . . . . . . . . Rewrite ("radd_0", "0 + ?k = ?k"),
1.167 ([3,2,2], Res), x = 1