1.1 --- a/test/Tools/isac/Interpret/inform.sml Tue Oct 18 12:05:03 2016 +0200
1.2 +++ b/test/Tools/isac/Interpret/inform.sml Thu Oct 20 10:26:29 2016 +0200
1.3 @@ -160,8 +160,8 @@
1.4
1.5 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
1.6 val (_,(tac,_,_)::_) = get_calc 1;
1.7 - if tac = Rewrite_Set "norm_equation" then ()
1.8 - else error "inform.sml: diff.behav.appendFormula: on Frm + equ 2";
1.9 + case tac of Rewrite_Set "norm_equation" => ()
1.10 + | _ => error "inform.sml: diff.behav.appendFormula: on Frm + equ 2";
1.11 autoCalculate 1 CompleteCalc;
1.12 val ((pt,_),_) = get_calc 1;
1.13 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
1.14 @@ -190,8 +190,8 @@
1.15
1.16 fetchProposedTactic 1;
1.17 val (_,(tac,_,_)::_) = get_calc 1;
1.18 - if tac = Rewrite_Set "Test_simplify" then ()
1.19 - else error "inform.sml: diff.behav.appendFormula: Res + NOder 2";
1.20 + case tac of Rewrite_Set "Test_simplify" => ()
1.21 + | _ => error "inform.sml: diff.behav.appendFormula: Res + NOder 2";
1.22 autoCalculate 1 CompleteCalc;
1.23 val ((pt,_),_) = get_calc 1;
1.24 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
1.25 @@ -220,8 +220,8 @@
1.26
1.27 fetchProposedTactic 1;
1.28 val (_,(tac,_,_)::_) = get_calc 1;
1.29 - if tac = Check_Postcond ["LINEAR", "univariate", "equation", "test"] then ()
1.30 - else error "inform.sml: diff.behav.appendFormula: Res + late d 2";
1.31 + case tac of Check_Postcond ["LINEAR", "univariate", "equation", "test"] => ()
1.32 + | _ => error "inform.sml: diff.behav.appendFormula: Res + late d 2";
1.33 autoCalculate 1 CompleteCalc;
1.34 val ((pt,_),_) = get_calc 1;
1.35 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
1.36 @@ -1217,10 +1217,13 @@
1.37 val p = get_pos 1 1;
1.38 val (Form f, _, asms) = pt_extract (pt, p);
1.39
1.40 - if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
1.41 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"],
1.42 - ("diff_sum", str2term "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
1.43 - then () else error "embed fun get_fillform changed 1";
1.44 + if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then
1.45 + case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"],
1.46 + ("diff_sum", thm)) =>
1.47 + if (term2str o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
1.48 + else error "embed fun get_fillform changed 11"
1.49 + | _ => error "embed fun get_fillform changed 12"
1.50 + else error "embed fun get_fillform changed 13";
1.51
1.52 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
1.53 (*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
1.54 @@ -1229,21 +1232,27 @@
1.55 val p = get_pos 1 1;
1.56
1.57 val (Form f, _, asms) = pt_extract (pt, p);
1.58 - if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
1.59 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"],
1.60 - ("diff_sum", str2term "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
1.61 - then () else error "embed fun get_fillform changed 2";
1.62 + if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then
1.63 + case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"],
1.64 + ("diff_sum", thm)) =>
1.65 + if (term2str o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
1.66 + else error "embed fun get_fillform changed 21"
1.67 + | _ => error "embed fun get_fillform changed 22"
1.68 + else error "embed fun get_fillform changed 23";
1.69
1.70 requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
1.71 (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
1.72 val ((pt,pos),_) = get_calc 1;
1.73 val p = get_pos 1 1;
1.74 val (Form f, _, asms) = pt_extract (pt, p);
1.75 - if p = ([1], Res) andalso existpt [2] pt andalso
1.76 - term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
1.77 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"],
1.78 - ("diff_sum", str2term "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
1.79 - then () else error "embed fun get_fillform changed 3";
1.80 + if p = ([1], Res) andalso existpt [2] pt
1.81 + andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
1.82 + then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"],
1.83 + ("diff_sum", thm)) =>
1.84 + if (term2str o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
1.85 + else error "embed fun get_fillform changed 31"
1.86 + | _ => error "embed fun get_fillform changed 32"
1.87 + else error "embed fun get_fillform changed 33";
1.88
1.89 (* input a formula which exactly fills the gaps in a "fillformula"
1.90 presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)":
1.91 @@ -1260,7 +1269,7 @@
1.92 val p' = lev_on p;
1.93 val tac = get_obj g_tac pt p';
1.94 val Rewrite_Inst ([bbb as "(bdv, x)"], ("diff_sin_chain", ttt)) = tac;
1.95 -if term2str ttt = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
1.96 +if (term2str o Thm.prop_of) ttt = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
1.97 else error "inputFillFormula changed 10";
1.98 val Appl rew = applicable_in pos pt tac;
1.99 val Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) = rew;
1.100 @@ -1275,9 +1284,11 @@
1.101 val ((pt, _),_) = get_calc 1;
1.102 val p = get_pos 1 1;
1.103 val (Form f, _, asms) = pt_extract (pt, p);
1.104 -if p = ([2], Res) andalso
1.105 - term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso
1.106 - get_obj g_tac pt (fst p) =
1.107 - Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", str2term "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"))
1.108 -then () else error "inputFillFormula changed 11";
1.109 + if p = ([2], Res) andalso term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)"
1.110 + then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"],
1.111 + ("diff_sin_chain", thm)) =>
1.112 + if (term2str o Thm.prop_of) thm = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
1.113 + else error "inputFillFormula changed 111"
1.114 + | _ => error "inputFillFormula changed 112"
1.115 + else error "inputFillFormula changed 113";
1.116