1.1 --- a/test/Tools/isac/Interpret/inform.sml Tue May 22 07:00:53 2012 +0200
1.2 +++ b/test/Tools/isac/Interpret/inform.sml Tue May 22 13:40:06 2012 +0200
1.3 @@ -36,6 +36,7 @@
1.4 "--------- build fun check_error_patterns ------------------------";
1.5 "--------- embed fun check_error_patterns ------------------------";
1.6 "--------- embed fun find_fillpatterns ---------------------------";
1.7 +"--------- embed fun get_fillform --------------------------------";
1.8 "-----------------------------------------------------------------";
1.9 "-----------------------------------------------------------------";
1.10 "-----------------------------------------------------------------";
1.11 @@ -931,7 +932,7 @@
1.12 val pos_pred = lev_back' pos
1.13 (* f_pred ---"step pos cs"---> f_succ in appendFormula
1.14 TODO.WN120517: one starting point for redesign of pos' *)
1.15 -val (f_pred, f_succ) = (get_pred_formula (pt, pos_pred), get_pred_formula (pt, pos));
1.16 +val (f_pred, f_succ) = (get_curr_formula (pt, pos_pred), get_curr_formula (pt, pos));
1.17
1.18 term2str f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))";
1.19 term2str f_succ = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";
1.20 @@ -971,13 +972,14 @@
1.21 autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
1.22 appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";
1.23 (*<CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>*)
1.24 - (*TODO BACK TO <CALCMESSAGE> no derivation found </CALCMESSAGE>*)
1.25 + (*or
1.26 + <CALCMESSAGE> no derivation found </CALCMESSAGE>*)
1.27
1.28 "~~~~~ fun FindFillpatterns, args:"; val (cI, errpatID) = (1, "chain-rule-diff-both");
1.29 val ((pt, _), _) = get_calc cI
1.30 val pos = get_pos cI 1;
1.31 - "~~~~~ fun find_fillpatterns, args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
1.32 - val f_curr = get_pred_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*)
1.33 +"~~~~~ fun find_fillpatterns, args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
1.34 + val f_curr = get_curr_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*)
1.35 val pp = par_pblobj pt p
1.36 val {errpats, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)
1.37 val ScrState (env, _, _, _, _, _) = get_istate pt pos
1.38 @@ -988,13 +990,13 @@
1.39 |> flat;
1.40
1.41 case map (get_fillpats subst f_curr errpatID) errpatthms |> flat of
1.42 - ("fill-d_d-arg",
1.43 - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1")
1.44 - :: _ => ()
1.45 -| _ => error "find_fillpatterns changed"
1.46 + ("fill-d_d-arg", tm) :: _ => if term2str tm =
1.47 + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1"
1.48 + then () else error "find_fillpatterns changed 1a"
1.49 +| _ => error "find_fillpatterns changed 1b"
1.50
1.51 "~~~~~ fun get_fillpats, args:"; val (subst, form, errpatID, thm) =
1.52 - (subst, f_curr, errpatID, hd errpatthms);
1.53 + (subst, f_curr, errpatID, hd (*simulate beginning of "map"*) errpatthms);
1.54 val thmDeriv = Thm.get_name_hint thm
1.55 val (part, thyID) = thy_containing_thm thmDeriv
1.56 val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
1.57 @@ -1002,8 +1004,104 @@
1.58 val some = map (get_fillform subst form errpatID) fillpats;
1.59
1.60 case some |> filter is_some |> map the of
1.61 - ("fill-d_d-arg",
1.62 - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1")
1.63 - :: _ => ()
1.64 -| _ => error "get_fillpats changed"
1.65 + ("fill-d_d-arg", tm) :: _ => if term2str tm =
1.66 + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1"
1.67 + then () else error "find_fillpatterns changed 2a"
1.68 +| _ => error "find_fillpatterns changed 2b"
1.69
1.70 +"~~~~~ fun get_fillform, args:"; val (subst, form, errpatID, ((fillpatID, pat, erpaID): fillpat)) =
1.71 + (subst, form, errpatID, hd (*simulate beginning of "map"*) fillpats);
1.72 + val (form', _, _, rewritten) =
1.73 + rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) form;
1.74 +
1.75 +if term2str form' = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" then ()
1.76 +else error "find_fillpatterns changed 3";
1.77 +
1.78 +"~~~~~ to FindFillpatterns return val:"; val (fillpats) =
1.79 + (map (get_fillpats subst f_curr errpatID) errpatthms |> flat) (*only from "hd errpatthms"*);
1.80 +
1.81 +val msg = "fill patterns " ^ ((map (apsnd term2str) fillpats) |> map pair2str_ |> strs2str_);
1.82 +if msg =
1.83 + "fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
1.84 + " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" ^
1.85 + "#fill-both-args#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
1.86 + " =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3" ^
1.87 + "#fill-d_d#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
1.88 + " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1 x (x ^^^ 4)" ^
1.89 + "#fill-inner-deriv#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
1.90 + " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1" ^
1.91 + "#fill-all#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = d_d x (x ^^^ 2) + ?_dummy_1#"
1.92 +then () else error "find_fillpatterns changed 4";
1.93 +
1.94 +
1.95 +"--------- embed fun get_fillform --------------------------------";
1.96 +"--------- embed fun get_fillform --------------------------------";
1.97 +"--------- embed fun get_fillform --------------------------------";
1.98 +states := [];
1.99 +CalcTree
1.100 +[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
1.101 + ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
1.102 +Iterator 1;
1.103 +moveActiveRoot 1;
1.104 +autoCalculate 1 CompleteCalcHead;
1.105 +autoCalculate 1 (Step 1);
1.106 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
1.107 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";
1.108 +(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
1.109 + would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
1.110 + results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
1.111 + instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
1.112 +FindFillpatterns 1 "chain-rule-diff-both";
1.113 +(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
1.114 + d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
1.115 +
1.116 +"~~~~~ fun requestFillformula, args:"; val (cI, (errpatID, fillpatID)) =
1.117 + (1, ("chain-rule-diff-both", "fill-both-args"));
1.118 +val ((pt, _), _) = get_calc cI
1.119 +val pos = get_pos cI 1; (* = ([1], Res)*)
1.120 +
1.121 +"~~~~~ fun get_fillformula, args:"; val ((pt, pos as (p, _)), (errpatID, fillpatID)) =
1.122 + ((pt, pos), (errpatID, fillpatID));
1.123 +val fillforms = find_fillpatterns (pt, pos) errpatID
1.124 +val fillforms =
1.125 + filter ((curry op = fillpatID) o (#1: (fillpatID * term -> fillpatID))) fillforms;
1.126 +
1.127 +val [(fillpatID, fillform)] = fillforms;
1.128 +case (fillpatID, fillform) of
1.129 + ("fill-both-args", tm) => if term2str tm =
1.130 + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"
1.131 + then () else error "get_fillformula changed 1a"
1.132 +| _ => error "get_fillformula changed 1b";
1.133 +
1.134 + val f_curr = get_curr_formula (pt, pos); (*already done in find_fillpatterns, too*)
1.135 +term2str f_curr = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))";
1.136 +
1.137 +"~~~~~ fun generate_inconsistent, args:";
1.138 + val (_, (Rewrite' (_,_,_,_, thm', f, (f', asm))), (is, ctxt), (p,_), pt) =
1.139 + (0,
1.140 + (Rewrite' ("","",e_rls,true, (fillpatID, ""(*errpatthm known in find_fillpatterns*)),
1.141 + f_curr, (fillform, []))),
1.142 + (get_loc pt pos), (lev_on p, Und), pt);
1.143 +if p = [2] then () else error "generate_inconsistent changed 1";
1.144 +
1.145 +val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.146 + (Rewrite thm') (f', asm) Inconsistent
1.147 +val pt = update_branch pt p TransitiveB;
1.148 +
1.149 +"~~~~~ to get_fillformula return val:"; val (pos', _, _, pt) =
1.150 + ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt);
1.151 +if pos' = ([2], Res) then () else error "generate_inconsistent changed 2";
1.152 +
1.153 +upd_calc cI ((pt, pos'), []); upd_ipos cI 1 pos';
1.154 +autocalculateOK2xml cI pos pos' pos';
1.155 +
1.156 +"~~~~~ final check:";
1.157 +val ((pt,pos),_) = get_calc 1;
1.158 +val p = get_pos 1 1;
1.159 +val (Form f, tac, asms) = pt_extract (pt, p);
1.160 +if p = ([2], Res) andalso term2str f =
1.161 + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"
1.162 +then () else error "";
1.163 +
1.164 +show_pt pt; (*ATTENTION: omits the last step, if pt is incomplete, ([2], Res) EXISTS !*)
1.165 +