1.1 --- a/src/Tools/isac/Frontend/interface.sml Thu May 24 17:13:58 2012 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Thu May 24 18:40:07 2012 +0200
1.3 @@ -811,13 +811,10 @@
1.4 in
1.5 case filter ((curry op = fillpatID) o
1.6 (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms of
1.7 - (fillpatID, fillform, thm, bdvopt) :: _ =>
1.8 + (_, fillform, thm, sube_opt) :: _ =>
1.9 let
1.10 - val f_curr = get_curr_formula (pt, pos) (*already done in find_fillpatterns, too*)
1.11 - val (pos', _, _, pt) = generate_inconsistent 0
1.12 - (Rewrite' ("","",e_rls,true, (fillpatID, ""(*errpatthm known in find_fillpatterns*)),
1.13 - f_curr, (fillform, [])))
1.14 - (get_loc pt pos) (lev_on p, Und) pt
1.15 + val (pt, pos') = generate_inconsistent_rew (sube_opt, thm'_of_thm thm)
1.16 + (fillform, []) (get_loc pt pos) (lev_on p, Und) pt
1.17 in
1.18 (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)
1.19 autocalculateOK2xml cI pos pos' pos')
2.1 --- a/src/Tools/isac/Interpret/generate.sml Thu May 24 17:13:58 2012 +0200
2.2 +++ b/src/Tools/isac/Interpret/generate.sml Thu May 24 18:40:07 2012 +0200
2.3 @@ -470,12 +470,17 @@
2.4 | generate1 thy m' _ _ _ =
2.5 error ("generate1: not impl.for "^(tac_2str m'));
2.6
2.7 -fun generate_inconsistent _ (Rewrite' (_,_,_,_, thm', f, (f', asm))) (is, ctxt) (p,_) pt =
2.8 - let
2.9 - val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
2.10 +fun generate_inconsistent_rew (subs_opt, thm') (f', asm) (is, ctxt) (pos as (p,_)) pt =
2.11 + let
2.12 + val f = get_curr_formula (pt, pos) (*already done in find_fillpatterns, too*)
2.13 + val (pt,c) =
2.14 + case subs_opt of
2.15 + NONE => cappend_atomic pt p (is, insert_assumptions asm ctxt) f
2.16 (Rewrite thm') (f', asm) Inconsistent
2.17 - val pt = update_branch pt p TransitiveB
2.18 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt)end
2.19 + | SOME subs => cappend_atomic pt p (is, insert_assumptions asm ctxt) f
2.20 + (Rewrite_Inst (subs, thm')) (f', asm) Inconsistent
2.21 + val pt = update_branch pt p TransitiveB
2.22 + in (pt, (p,Res)) end
2.23
2.24 fun generate_hard thy m' (p,p_) pt =
2.25 let
3.1 --- a/src/Tools/isac/calcelems.sml Thu May 24 17:13:58 2012 +0200
3.2 +++ b/src/Tools/isac/calcelems.sml Thu May 24 18:40:07 2012 +0200
3.3 @@ -18,7 +18,10 @@
3.4 val empty_cterm' = "empty_cterm'";
3.5
3.6 type thmID = string; (* identifier for a thm (the shortest possible identifier) *)
3.7 -type thmDeriv = string; (* thyID ^"."^ xxx ^"."^ thmID, see fun thmID_of_derivation_name *)
3.8 +type thmDeriv = string; (* WN120524 deprecated
3.9 + thyID ^"."^ xxx ^"."^ thmID, see fun thmID_of_derivation_name
3.10 + WN120524: dont use Thm.derivation_name, this is destroyed by num_str;
3.11 + Thm.get_name_hint survives num_str and seems perfectly reliable *)
3.12
3.13 type thm' = thmID * cterm';(*WN060610 deprecated in favour of thm''*)
3.14 type thm'' = thmID * term;
3.15 @@ -151,6 +154,9 @@
3.16
3.17 fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
3.18 fun thyID_of_derivation_name dn = hd (space_explode "." dn);
3.19 +fun thm'_of_thm thm =
3.20 + ((thyID_of_derivation_name o Thm.get_name_hint) thm,
3.21 + (thmID_of_derivation_name o Thm.get_name_hint) thm): thm'
3.22
3.23 fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
3.24 (strip_thy thmid1) = (strip_thy thmid2);
4.1 --- a/test/Tools/isac/Interpret/inform.sml Thu May 24 17:13:58 2012 +0200
4.2 +++ b/test/Tools/isac/Interpret/inform.sml Thu May 24 18:40:07 2012 +0200
4.3 @@ -1106,72 +1106,4 @@
4.4 then () else error "";
4.5
4.6 show_pt pt; (*ATTENTION: omits the last step, if pt is incomplete, ([2], Res) EXISTS !*)
4.7 -"--------- embed fun get_fillformula -----------------------------";
4.8 -states := [];
4.9 -CalcTree
4.10 -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
4.11 - ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
4.12 -Iterator 1;
4.13 -moveActiveRoot 1;
4.14 -autoCalculate 1 CompleteCalcHead;
4.15 -autoCalculate 1 (Step 1);
4.16 -autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
4.17 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";
4.18 -(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
4.19 - would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
4.20 - results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
4.21 - instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
4.22 -findFillpatterns 1 "chain-rule-diff-both";
4.23 -(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
4.24 - d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
4.25
4.26 -"~~~~~ fun requestFillformula, args:"; val (cI, (errpatID, fillpatID)) =
4.27 - (1, ("chain-rule-diff-both", "fill-both-args"));
4.28 -val ((pt, _), _) = get_calc cI
4.29 -val pos = get_pos cI 1; (* = ([1], Res)*)
4.30 -
4.31 -"~~~~~ fun get_fillformula, args:"; val ((pt, pos as (p, _)), (errpatID, fillpatID)) =
4.32 - ((pt, pos), (errpatID, fillpatID));
4.33 -val fillforms = find_fillpatterns (pt, pos) errpatID
4.34 -val fillforms =
4.35 - filter ((curry op = fillpatID) o (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms;
4.36 -
4.37 -val [(fillpatID, fillform, thm, subs_opt)] = fillforms;
4.38 -case (fillpatID, fillform, thm, subs_opt) of
4.39 - ("fill-both-args", tm, thm, subs_opt) => if term2str tm =
4.40 - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"
4.41 - then () else error "get_fillformula changed 1a"
4.42 -| _ => error "get_fillformula changed 1b";
4.43 -
4.44 - val f_curr = get_curr_formula (pt, pos); (*already done in find_fillpatterns, too*)
4.45 -term2str f_curr = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))";
4.46 -
4.47 -"~~~~~ fun generate_inconsistent, args:";
4.48 - val (_, (Rewrite' (_,_,_,_, thm', f, (f', asm))), (is, ctxt), (p,_), pt) =
4.49 - (0,
4.50 - (Rewrite' ("","",e_rls,true, (fillpatID, ""(*errpatthm known in find_fillpatterns*)),
4.51 - f_curr, (fillform, []))),
4.52 - (get_loc pt pos), (lev_on p, Und), pt);
4.53 -if p = [2] then () else error "generate_inconsistent changed 1";
4.54 -
4.55 -val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
4.56 - (Rewrite thm') (f', asm) Inconsistent
4.57 -val pt = update_branch pt p TransitiveB;
4.58 -
4.59 -"~~~~~ to get_fillformula return val:"; val (pos', _, _, pt) =
4.60 - ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt);
4.61 -if pos' = ([2], Res) then () else error "generate_inconsistent changed 2";
4.62 -
4.63 -upd_calc cI ((pt, pos'), []); upd_ipos cI 1 pos';
4.64 -autocalculateOK2xml cI pos pos' pos';
4.65 -
4.66 -"~~~~~ final check:";
4.67 -val ((pt,pos),_) = get_calc 1;
4.68 -val p = get_pos 1 1;
4.69 -val (Form f, tac, asms) = pt_extract (pt, p);
4.70 -if p = ([2], Res) andalso term2str f =
4.71 - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"
4.72 -then () else error "";
4.73 -
4.74 -show_pt pt; (*ATTENTION: omits the last step, if pt is incomplete, ([2], Res) EXISTS !*)
4.75 -
5.1 --- a/test/Tools/isac/Test_Some.thy Thu May 24 17:13:58 2012 +0200
5.2 +++ b/test/Tools/isac/Test_Some.thy Thu May 24 18:40:07 2012 +0200
5.3 @@ -13,6 +13,7 @@
5.4 ML {* (*================== --> test/../inform.sml*)
5.5 "--------- UC errpat, fillpat ---------------------------"; (*--> test/../interface.sml*)
5.6 "--------- build fun is_exactly_equal, .....----------------------"; (*--> test/../inform.sml*)
5.7 +"--------- build fun is_exactly_equal, .....----------------------"; (*--> test/../inform.sml*)
5.8 states := [];
5.9 CalcTree
5.10 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
5.11 @@ -66,10 +67,13 @@
5.12
5.13 *}
5.14 ML {*
5.15 -get_obj g_tac pt (lev_on p)
5.16 +print_depth 999;
5.17 +get_obj g_tac pt (lev_on p);
5.18 +print_depth 999;
5.19 *}
5.20 ML {*
5.21 -Rewrite_Inst
5.22 +Rewrite_Inst';
5.23 +("",""): thm';
5.24 *}
5.25 ML {*
5.26 val Appl (rewtac as Rewrite' (_, _, _, _, _, _, (res, _))) =
5.27 @@ -80,13 +84,52 @@
5.28 thmID_of_derivation_name
5.29 *}
5.30 ML {*
5.31 +Thm.get_name_hint;
5.32 +Thm.derivation_name;
5.33 +*}
5.34 +ML {* (*================== already in code*)
5.35 +fun thm'_of_thm thm =
5.36 + ((thyID_of_derivation_name o Thm.get_name_hint) thm,
5.37 + (thmID_of_derivation_name o Thm.get_name_hint) thm): thm'
5.38 +fun generate_inconsistent_rew (subs_opt, thm') (f', asm) (is, ctxt) (pos as (p,_)) pt =
5.39 + let
5.40 + val f = get_curr_formula (pt, pos) (*already done in find_fillpatterns, too*)
5.41 + val (pt,c) =
5.42 + case subs_opt of
5.43 + NONE => cappend_atomic pt p (is, insert_assumptions asm ctxt) f
5.44 + (Rewrite thm') (f', asm) Inconsistent
5.45 + | SOME subs => cappend_atomic pt p (is, insert_assumptions asm ctxt) f
5.46 + (Rewrite_Inst (subs, thm')) (f', asm) Inconsistent
5.47 + val pt = update_branch pt p TransitiveB
5.48 + in (pt, (p,Res)) end
5.49 +*}
5.50 +text {*
5.51 +Rewrite_Inst' (theory', rew_ord', rls, bool, subst, thm', term, (res, term list))
5.52 +*}
5.53 +ML {*
5.54 +fun requestFillformula cI (errpatID, fillpatID) =
5.55 + let
5.56 + val ((pt, _), _) = get_calc cI
5.57 + val pos as (p, _) = get_pos cI 1
5.58 + val fillforms = find_fillpatterns (pt, pos) errpatID
5.59 + in
5.60 + case filter ((curry op = fillpatID) o
5.61 + (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms of
5.62 + (_, fillform, thm, sube_opt) :: _ =>
5.63 + let
5.64 + val (pt, pos') = generate_inconsistent_rew (sube_opt, thm'_of_thm thm)
5.65 + (fillform, []) (get_loc pt pos) (lev_on p, Und) pt
5.66 + in
5.67 + (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)
5.68 + autocalculateOK2xml cI pos pos' pos')
5.69 + end
5.70 + | _ => autocalculateERROR2xml cI "no fillpattern found"
5.71 + end;
5.72 +
5.73 *}
5.74 ML {*
5.75 *}
5.76 -ML {*
5.77 -*}
5.78 -ML {* (*================== changed here, not in code*)
5.79 -*}
5.80 +
5.81 ML {* (*==================*)
5.82
5.83 *}