1.1 --- a/src/sml/IsacKnowledge/PolyMinus.ML Wed Jan 02 18:13:59 2008 +0100
1.2 +++ b/src/sml/IsacKnowledge/PolyMinus.ML Fri Jan 04 11:16:28 2008 +0100
1.3 @@ -300,9 +300,9 @@
1.4 (*"(~ False) = True"*)],
1.5 crls = e_rls, nrls = rls_p_33},
1.6 "Script SimplifyScript (t_::real) = \
1.7 -\ (((Try (Rewrite_Set ordne_alphabetisch False)) @@ \
1.8 -\ (Try (Rewrite_Set fasse_zusammen False)) @@ \
1.9 -\ (Try (Rewrite_Set verschoenere False))) t_)"
1.10 +\ ((Repeat((Try (Rewrite_Set ordne_alphabetisch False)) @@ \
1.11 +\ (Try (Rewrite_Set fasse_zusammen False)) @@ \
1.12 +\ (Try (Rewrite_Set verschoenere False)))) t_)"
1.13 ));
1.14
1.15 store_met
2.1 --- a/src/sml/ME/ctree.sml Wed Jan 02 18:13:59 2008 +0100
2.2 +++ b/src/sml/ME/ctree.sml Fri Jan 04 11:16:28 2008 +0100
2.3 @@ -514,14 +514,7 @@
2.4 | rls_of_rewset (Detail_Set_Inst (subs, rls)) =
2.5 (rls, Some ((subs2subst (assoc_thy "Isac.thy") subs):subst));
2.6
2.7 -(*fun rule2tac (Thm (thmID, thm)) =
2.8 - Rewrite (thmID, string_of_thmI thm)
2.9 - | rule2tac (Rls_ rls) = Rewrite_Set (id_rls rls)
2.10 - | rule2tac (Rls_ rls) = Rewrite_Set (id_rls rls)
2.11 - | rule2tac rule =
2.12 - raise error ("rule2tac: called with '" ^ rule2str rule ^ "'");
2.13 -WN071231*)
2.14 -fun rule2tac _ (Calc (opID, thm)) = Calculate opID
2.15 +fun rule2tac _ (Calc (opID, thm)) = Calculate (calID2calcID opID)
2.16 | rule2tac [] (Thm (thmID, thm)) = Rewrite (thmID, string_of_thmI thm)
2.17 | rule2tac subst (Thm (thmID, thm)) =
2.18 Rewrite_Inst (subst2subs subst, (thmID, string_of_thmI thm))
3.1 --- a/src/sml/ME/rewtools.sml Wed Jan 02 18:13:59 2008 +0100
3.2 +++ b/src/sml/ME/rewtools.sml Fri Jan 04 11:16:28 2008 +0100
3.3 @@ -647,9 +647,8 @@
3.4 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics .*)
3.5 (* val
3.6 *)
3.7 -fun atomic_appl_tacs thy _ _ f (Calculate calcID) =
3.8 - try_rew thy e_rew_ordX e_rls [] f (Calc (snd(assoc1 (!calclist', calcID))))
3.9 -
3.10 +fun atomic_appl_tacs thy _ _ f (Calculate scrID) =
3.11 + try_rew thy e_rew_ordX e_rls [] f (Calc (snd(assoc1 (!calclist', scrID))))
3.12 | atomic_appl_tacs thy ro erls f (Rewrite (thm' as (thmID, _))) =
3.13 try_rew thy (ro, assoc_rew_ord ro) erls [] f
3.14 (Thm (thmID, assoc_thm' thy thm'))
4.1 --- a/src/sml/calcelems.sml Wed Jan 02 18:13:59 2008 +0100
4.2 +++ b/src/sml/calcelems.sml Fri Jan 04 11:16:28 2008 +0100
4.3 @@ -36,9 +36,11 @@
4.4 type eval_fn = (string -> term -> theory -> (string * term) option);
4.5 fun e_evalfn (_:'a) (_:term) (_:theory) = None:(string * term) option;
4.6 (*. op in isa-term 'Const(op,_)' .*)
4.7 -type cal = (string * eval_fn);
4.8 +type calID = string;
4.9 +type cal = (calID * eval_fn);
4.10 (*. fun calculate_ fetches the evaluation-function via this list. *)
4.11 -type calc = (string * cal);
4.12 +type calcID = string;
4.13 +type calc = (calcID * cal);
4.14
4.15 type subs' = (cterm' * cterm') list; (*16.11.00 for FE-KE*)
4.16 type subst = (term * term) list; (*here for ets2str*)
4.17 @@ -561,12 +563,19 @@
4.18 fun assoc_calc ([], key) = raise error ("assoc_calc: '"^ key ^"' not found")
4.19 | assoc_calc ((calc, (keyi, xi)) :: pairs, key) =
4.20 if key = keyi then calc else assoc_calc (pairs, key);
4.21 -(*only used for !calclist'*)
4.22 +(*only used for !calclist'...*)
4.23 fun assoc1 ([], key) = raise error ("assoc1 (for met.calc=): '"^ key
4.24 ^"' not found")
4.25 | assoc1 ((all as (keyi, _)) :: pairs, key) =
4.26 if key = keyi then all else assoc1 (pairs, key);
4.27 -(*fun assoc_thm' requires mk_thm, num_str; see Scripts/rewrite.sml*)
4.28 +
4.29 +(*WN080102 clarify usage of type cal and type calc..*)
4.30 +fun calID2calcID (calID : calID) =
4.31 + let fun ass [] = raise error ("calID2calcID: "^calID^"not in calclist'")
4.32 + | ass ((calci, (cali, eval_fn))::ids) =
4.33 + if calID = cali then calci
4.34 + else ass ids
4.35 + in ass (!calclist') : calcID end;
4.36
4.37
4.38 fun termopt2str (Some t) =
5.1 --- a/src/smltest/IsacKnowledge/polyminus.sml Wed Jan 02 18:13:59 2008 +0100
5.2 +++ b/src/smltest/IsacKnowledge/polyminus.sml Fri Jan 04 11:16:28 2008 +0100
5.3 @@ -278,37 +278,37 @@
5.4 autoCalculate 1 (Step 1);
5.5 autoCalculate 1 (Step 1);
5.6 val ((pt,p),_) = get_calc 1; show_pt pt;
5.7 -
5.8 +"----- 1 ^^^";
5.9 fetchApplicableTactics 1 0 p;
5.10 val appltacs = sel_appl_atomic_tacs pt p;
5.11 applyTactic 1 p (hd appltacs);
5.12 val ((pt,p),_) = get_calc 1; show_pt pt;
5.13 -
5.14 +"----- 2 ^^^";
5.15 applyTactic 1 p (hd (sel_appl_atomic_tacs pt p));
5.16 val ((pt,p),_) = get_calc 1; show_pt pt;
5.17 -
5.18 +"----- 3 ^^^";
5.19 applyTactic 1 p (hd (sel_appl_atomic_tacs pt p));
5.20 val ((pt,p),_) = get_calc 1; show_pt pt;
5.21 -
5.22 +"----- 4 ^^^";
5.23 applyTactic 1 p (hd (sel_appl_atomic_tacs pt p));
5.24 val ((pt,p),_) = get_calc 1; show_pt pt;
5.25 -
5.26 +"----- 5 ^^^";
5.27 applyTactic 1 p (hd (sel_appl_atomic_tacs pt p));
5.28 val ((pt,p),_) = get_calc 1; show_pt pt;
5.29 +"----- 6 ^^^";
5.30
5.31 -(**)
5.32 +(*<CALCMESSAGE> failure </CALCMESSAGE>
5.33 applyTactic 1 p (hd (sel_appl_atomic_tacs pt p));
5.34 val ((pt,p),_) = get_calc 1; show_pt pt;
5.35 +"----- 7 ^^^";
5.36 +*)
5.37
5.38 -
5.39 -
5.40 -
5.41 -
5.42 -
5.43 -(*vvv this gives <CALCMESSAGE> failure </CALCMESSAGE>*)
5.44 -
5.45 -(*vvv only this (= autoCalculate tac) works*)
5.46 -applyTactic 1 p (Rewrite_Set "fasse_zusammen");
5.47 +autoCalculate 1 CompleteCalc;
5.48 +val ((pt,p),_) = get_calc 1; show_pt pt;
5.49 +(*independent from failure above: met_simp_poly_minus not confluent:
5.50 +(([9], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f)),
5.51 +(([], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f))]
5.52 +~~~~~~~~~~~###~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
5.53
5.54 (*
5.55 use"../smltest/IsacKnowledge/polyminus.sml";
6.1 --- a/src/smltest/ME/rewtools.sml Wed Jan 02 18:13:59 2008 +0100
6.2 +++ b/src/smltest/ME/rewtools.sml Fri Jan 04 11:16:28 2008 +0100
6.3 @@ -511,7 +511,7 @@
6.4 if filter_appl_rews thy subst f rls =
6.5 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
6.6 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
6.7 - Calculate "op +"] then ()
6.8 + Calculate "plus"] then ()
6.9 else raise error "rewtools.sml filter_appl_rews a + z + 2*a + 3*z + 5 + 6";
6.10
6.11
7.1 --- a/src/smltest/ME/script.sml Wed Jan 02 18:13:59 2008 +0100
7.2 +++ b/src/smltest/ME/script.sml Fri Jan 04 11:16:28 2008 +0100
7.3 @@ -234,7 +234,7 @@
7.4 if appltacs =
7.5 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
7.6 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
7.7 - Calculate "op *"(*..wrong opID: TODO.WN080102 "times" ok*)] then ()
7.8 + Calculate "times"] then ()
7.9 else raise error "script.sml fun sel_appl_atomic_tacs diff.behav.";
7.10
7.11 trace_script := true;