1.1 --- a/test/Tools/isac/Interpret/inform.sml Sun Oct 16 13:58:46 2016 +0200
1.2 +++ b/test/Tools/isac/Interpret/inform.sml Tue Oct 18 12:05:03 2016 +0200
1.3 @@ -131,7 +131,7 @@
1.4 val der = fod' @ (map rev_deriv' rifod');
1.5 (writeln o trtas2str) der;
1.6 "----------------------------------------------------------";
1.7 -
1.8 +DEconstrCalcTree 1;
1.9
1.10 "--------- appendFormula: on Frm + equ_nrls ----------------------";
1.11 "--------- appendFormula: on Frm + equ_nrls ----------------------";
1.12 @@ -166,7 +166,7 @@
1.13 val ((pt,_),_) = get_calc 1;
1.14 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
1.15 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
1.16 -
1.17 +DEconstrCalcTree 1;
1.18
1.19 "--------- appendFormula: on Res + NO deriv ----------------------";
1.20 "--------- appendFormula: on Res + NO deriv ----------------------";
1.21 @@ -196,7 +196,7 @@
1.22 val ((pt,_),_) = get_calc 1;
1.23 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
1.24 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
1.25 -
1.26 +DEconstrCalcTree 1;
1.27
1.28 "--------- appendFormula: on Res + late deriv --------------------";
1.29 "--------- appendFormula: on Res + late deriv --------------------";
1.30 @@ -226,7 +226,7 @@
1.31 val ((pt,_),_) = get_calc 1;
1.32 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
1.33 else error "inform.sml: diff.behav.appendFormula: Res + late d 3";
1.34 -
1.35 +DEconstrCalcTree 1;
1.36
1.37 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
1.38 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
1.39 @@ -250,8 +250,7 @@
1.40 if "[x = 3 + -2 * 1]" = term2str (fst (get_obj g_result pt [])) then ()
1.41 (* ~~~~~~~~~~ simplify as last step in any script ?!*)
1.42 else error "inform.sml: diff.behav.appendFormula: Res + latEE 2";
1.43 -
1.44 -
1.45 +DEconstrCalcTree 1;
1.46
1.47 "--------- replaceFormula: on Res + = ----------------------------";
1.48 "--------- replaceFormula: on Res + = ----------------------------";
1.49 @@ -297,6 +296,7 @@
1.50 val ((pt,pos as (p,_)),_) = get_calc 1;
1.51 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst) (get_obj g_result pt p) then()
1.52 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
1.53 +DEconstrCalcTree 1;
1.54
1.55 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
1.56 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
1.57 @@ -320,7 +320,7 @@
1.58 val ((pt,pos as (p,_)),_) = get_calc 1;
1.59 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst)(get_obj g_result pt p) then()
1.60 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
1.61 -
1.62 +DEconstrCalcTree 1;
1.63
1.64 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
1.65 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
1.66 @@ -343,7 +343,7 @@
1.67 val ((pt,pos as (p,_)),_) = get_calc 1;
1.68 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst)(get_obj g_result pt p) then()
1.69 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
1.70 -
1.71 +DEconstrCalcTree 1;
1.72
1.73 "--------- replaceFormula: cut calculation -----------------------";
1.74 "--------- replaceFormula: cut calculation -----------------------";
1.75 @@ -440,6 +440,7 @@
1.76
1.77 modifycalcheadOK2xml 111 (bool2str b) ocalhd;
1.78 *)
1.79 +DEconstrCalcTree 1;
1.80
1.81 "--------- syntax error ------------------------------------------";
1.82 "--------- syntax error ------------------------------------------";
1.83 @@ -459,7 +460,7 @@
1.84 writeln str;
1.85 if str = ". ----- pblobj -----\n1. x + 1 = 2\n" then ()
1.86 else error "inform.sml: diff.behav.appendFormula: syntax error";
1.87 -
1.88 +DEconstrCalcTree 1;
1.89
1.90 "--------- CAS-command on ([],Pbl) -------------------------------";
1.91 "--------- CAS-command on ([],Pbl) -------------------------------";
1.92 @@ -473,7 +474,7 @@
1.93 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.94 if p = ([1], Frm) andalso f2str f = "x + 1 = 2" then ()
1.95 else error "inform.sml: diff.behav. CAScmd ([],Pbl)";
1.96 -
1.97 +DEconstrCalcTree 1;
1.98
1.99 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
1.100 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
1.101 @@ -488,7 +489,7 @@
1.102 show_pt pt;
1.103 if p = ([], Res) then ()
1.104 else error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
1.105 -
1.106 +DEconstrCalcTree 1;
1.107
1.108 "--------- inform [rational,simplification] ----------------------";
1.109 "--------- inform [rational,simplification] ----------------------";
1.110 @@ -619,6 +620,7 @@
1.111 (([6], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f)),
1.112 (([], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f))]
1.113 *)
1.114 +DEconstrCalcTree 1;
1.115
1.116 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
1.117 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
1.118 @@ -684,6 +686,7 @@
1.119 show_pt pt;
1.120 if p = ([], Res) andalso term2str res = "1 + 2 * x" then ()
1.121 else error "diff.sml behav.changed for Diff (x^2 + x + 1, x)";
1.122 +DEconstrCalcTree 1;
1.123
1.124 "--------- Take as 1st tac, start from exp -----------------------";
1.125 "--------- Take as 1st tac, start from exp -----------------------";
1.126 @@ -725,6 +728,7 @@
1.127 val Form res = (#1 o pt_extract) (pt, p);
1.128 if term2str res = "d_d x (x ^^^ 2 + x + 1)" then ()
1.129 else error "diff.sml Diff (x^2 + x + 1, x) from exp";
1.130 +DEconstrCalcTree 1;
1.131
1.132 "--------- init_form, start with <NEW> (CAS input) ---------------";
1.133 "--------- init_form, start with <NEW> (CAS input) ---------------";
1.134 @@ -986,6 +990,7 @@
1.135 @{thm diff_ln_chain}, @{thm diff_exp_chain}])]: errpat list;
1.136 case check_error_patterns (res, inf) (prog, env) (errpats, rls) of SOME _ => ()
1.137 | NONE => error "check_error_patterns broken";
1.138 +DEconstrCalcTree 1;
1.139
1.140 "--------- embed fun check_error_patterns ------------------------";
1.141 "--------- embed fun check_error_patterns ------------------------";
1.142 @@ -1106,6 +1111,7 @@
1.143 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r';
1.144 if term2str t' = "cos (x ^^^ 4) * d_d x ?_dummy_1" then ()
1.145 else error "get_fillpats changed 1"
1.146 +DEconstrCalcTree 1;
1.147
1.148 "--------- embed fun find_fillpatterns ---------------------------";
1.149 "--------- embed fun find_fillpatterns ---------------------------";
1.150 @@ -1188,6 +1194,7 @@
1.151 if (map #1 fillpats) =
1.152 ["fill-d_d-arg", "fill-both-args", "fill-d_d", "fill-inner-deriv", "fill-all"]
1.153 then () else error "find_fillpatterns changed 4b";
1.154 +DEconstrCalcTree 1;
1.155
1.156 "--------- build fun is_exactly_equal, inputFillFormula ----------";
1.157 "--------- build fun is_exactly_equal, inputFillFormula ----------";
1.158 @@ -1212,7 +1219,7 @@
1.159
1.160 if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
1.161 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"],
1.162 - ("diff_sum", "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
1.163 + ("diff_sum", str2term "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
1.164 then () else error "embed fun get_fillform changed 1";
1.165
1.166 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
1.167 @@ -1224,7 +1231,7 @@
1.168 val (Form f, _, asms) = pt_extract (pt, p);
1.169 if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
1.170 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"],
1.171 - ("diff_sum", "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
1.172 + ("diff_sum", str2term "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
1.173 then () else error "embed fun get_fillform changed 2";
1.174
1.175 requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
1.176 @@ -1235,7 +1242,7 @@
1.177 if p = ([1], Res) andalso existpt [2] pt andalso
1.178 term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
1.179 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"],
1.180 - ("diff_sum", "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
1.181 + ("diff_sum", str2term "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
1.182 then () else error "embed fun get_fillform changed 3";
1.183
1.184 (* input a formula which exactly fills the gaps in a "fillformula"
1.185 @@ -1252,8 +1259,9 @@
1.186 val SOME ifo = parseNEW (assoc_thy "Isac" |> thy2ctxt) istr
1.187 val p' = lev_on p;
1.188 val tac = get_obj g_tac pt p';
1.189 -if tac = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"))
1.190 -then () else error "inputFillFormula changed 10";
1.191 +val Rewrite_Inst ([bbb as "(bdv, x)"], ("diff_sin_chain", ttt)) = tac;
1.192 +if term2str ttt = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
1.193 +else error "inputFillFormula changed 10";
1.194 val Appl rew = applicable_in pos pt tac;
1.195 val Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) = rew;
1.196
1.197 @@ -1270,6 +1278,6 @@
1.198 if p = ([2], Res) andalso
1.199 term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso
1.200 get_obj g_tac pt (fst p) =
1.201 - Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"))
1.202 + Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", str2term "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"))
1.203 then () else error "inputFillFormula changed 11";
1.204