# HG changeset patch
# User wneuper
# Date 1199294039 -3600
# Node ID 7cb662bd345d601b53e472a69f9f1281d33d45f8
# Parent a95383a1f7585cfbd90d5c60042011c3836aea67
sel_rules + sel_appl_atomic_tacs + applyTactic, intermediate state
diff -r a95383a1f758 -r 7cb662bd345d src/sml/FE-interface/interface.sml
--- a/src/sml/FE-interface/interface.sml Wed Jan 02 14:42:04 2008 +0100
+++ b/src/sml/FE-interface/interface.sml Wed Jan 02 18:13:59 2008 +0100
@@ -161,6 +161,8 @@
end;
(*. apply a tactic at a position and update the calc-tree if applicable .*)
+(* val (cI, ip, tac) = (1, p, hd appltacs);
+ *)
fun applyTactic (cI:calcID) ip tac =
let val ((pt, _), _) = get_calc cI
val p = get_pos cI 1
diff -r a95383a1f758 -r 7cb662bd345d src/sml/ME/mathengine.sml
--- a/src/sml/ME/mathengine.sml Wed Jan 02 14:42:04 2008 +0100
+++ b/src/sml/ME/mathengine.sml Wed Jan 02 18:13:59 2008 +0100
@@ -107,10 +107,11 @@
HElpless (**)
| Nexts of calcstate; (**)
+(*. locate a tactic in a script and apply it if possible .*)
(*report applicability of tac in tacis; pt is dropped in setNextTactic*)
fun locatetac _ (ptp as (_,([],Res))) = ("end-of-calculation", ([], [], ptp))
-(* val ptp as (pt, p) = (pt, ip);
- val ptp as (pt, p) = (pt, p);
+(* val ptp as (pt, p) = (pt, p);
+ val ptp as (pt, p) = (pt, ip);
*)
| locatetac tac (ptp as (pt, p)) =
let val (mI,m) = mk_tac'_ tac;
diff -r a95383a1f758 -r 7cb662bd345d src/sml/ME/rewtools.sml
--- a/src/sml/ME/rewtools.sml Wed Jan 02 14:42:04 2008 +0100
+++ b/src/sml/ME/rewtools.sml Wed Jan 02 18:13:59 2008 +0100
@@ -619,7 +619,8 @@
| find r12 = eq_rule r12
and finds [] = false
| finds (r1 :: rs) = if eq_rule (r, r1) then true else finds rs;
- in finds (get_rules rls) end;
+ in writeln ("### contains_rule: r = "^rule2str r^", rls = "^rls2str rls);
+ finds (get_rules rls) end;
(*. try if a rewrite-rule is applicable to a given formula;
in case of rule-sets (recursivley) collect all _atomic_ rewrites .*)
diff -r a95383a1f758 -r 7cb662bd345d src/sml/ME/script.sml
--- a/src/sml/ME/script.sml Wed Jan 02 14:42:04 2008 +0100
+++ b/src/sml/ME/script.sml Wed Jan 02 18:13:59 2008 +0100
@@ -648,9 +648,9 @@
AssWeak (m,f'))
else ((*writeln"3### assod ..NotAss";*)NotAss))
| (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =>
- if contains_rule (Thm (thmID, refl(*dummy*))) rls then
- if f = f_ then Ass (m,f') else AssWeak (m,f')
- else NotAss
+ if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_) then
+ if f = f_ then Ass (m,f') else AssWeak (m,f')
+ else NotAss
| _ => NotAss)
(*val f = (term_of o the o (parse thy))"#0+(sqrt(sqrt(sqrt a))^^^#2)^^^#2=#0";
@@ -1082,8 +1082,8 @@
(* val (ya, (is as (E,l,a,v,S,b),ss),Const ("Let",_) $ e $ (Abs (id,T,body))) =
(*1*)(((ts,d),Aundef), ((E,[R],a,v,S,b),[(m,EmptyMout,pt,p,[])]), body);
*)
- ((*writeln("### assy Let$e$Abs: is=");
- writeln(istate2str (ScrState is));*)
+ ((**)writeln("### assy Let$e$Abs: is=");
+ writeln(istate2str (ScrState is));(**)
case assy ya ((E , l@[L,R], a,v,S,b),ss) e of
NasApp ((E',l,a,v,S,bb),ss) =>
let val id' = mk_Free (id, T);
@@ -1119,12 +1119,12 @@
else assy ya ((E, l@[ R], a,v,S,b),ss) e2)
| assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Try",_) $ e $ a) =
- ((*writeln("### assy Try, l= "^(loc_2str l));*)
+ ((**)writeln("### assy Try $ e $ a, l= "^(loc_2str l));(**)
case assy ya ((E, l@[L,R], Some a,v,S,b),ss) e of
ay => ay)
| assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Try",_) $ e) =
- ((*writeln("### assy Try, l= "^(loc_2str l));*)
+ ((**)writeln("### assy Try $ e, l= "^(loc_2str l));(**)
case assy ya ((E, l@[R], a,v,S,b),ss) e of
ay => ay)
(* val (ya, ((E,l,_,v,S,b),ss), (Const ("Script.Seq",_) $e1 $ e2 $ a)) =
@@ -1180,35 +1180,37 @@
*)
| assy (((thy',sr),d),ap) (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss) t =
- ((*writeln("### assy, m = "^tac_2str m);
+ ((**)writeln("### assy, m = "^tac_2str m);
writeln("### assy, (p,p_) = "^pos'2str (p,p_));
writeln("### assy, is= ");
- writeln(istate2str (ScrState is));*)
+ writeln(istate2str (ScrState is));(**)
case handle_leaf "locate" thy' sr E a v t of
(a', Expr s) =>
- ((*writeln("### assy: listexpr t= "^(term2str t));
+ ((**)writeln("### assy: listexpr t= "^(term2str t));
writeln("### assy, E= "^(env2str E));
writeln("### assy, eval(..)= "^(term2str
(eval_listexpr_ (assoc_thy thy') sr
- (subst_atomic (upd_env_opt E (a',v)) t))));*)
+ (subst_atomic (upd_env_opt E (a',v)) t))));(**)
NasNap (eval_listexpr_ (assoc_thy thy') sr
(subst_atomic (upd_env_opt E (a',v)) t), E))
(* val (_,STac stac) = subst_stacexpr E a v t;
*)
| (a', STac stac) =>
- let (*val _=writeln("### assy, stac = "^term2str stac);*)
+ let (**)val _=writeln("### assy, stac = "^term2str stac);(**)
val p' = case p_ of Frm => p | Res => lev_on p
| _ => raise error ("assy: call by "^
(pos'2str (p,p_)));
in case assod pt d m stac of
Ass (m,v') =>
- let (*val _=writeln("### assy: Ass ("^tac_2str m^",
- "^term2str v'^")");*)
+ let (**)val _=writeln("### assy: Ass ("^tac_2str m^", "^
+ term2str v'^")");(**)
val (p'',c',f',pt') = generate1 (assoc_thy thy') m
(ScrState (E,l,a',v',S,true)) (p',p_) pt;
in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
| AssWeak (m,v') =>
- let val (p'',c',f',pt') = generate1 (assoc_thy thy') m
+ let (**)val _=writeln("### assy: Ass Weak("^tac_2str m^", "^
+ term2str v'^")");(**)
+ val (p'',c',f',pt') = generate1 (assoc_thy thy') m
(ScrState (E,l,a',v',S,false)) (p',p_) pt;
in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
| NotAss =>
@@ -1236,8 +1238,8 @@
*)
fun ass_up (ys as (y,s,Script sc,d)) (is as (E,l,a,v,S,b),ss)
(Const ("Let",_) $ _) =
- let (*val _= writeln("### ass_up1 Let$e: is=")
- val _= writeln(istate2str (ScrState is))*)
+ let (**)val _= writeln("### ass_up1 Let$e: is=")
+ val _= writeln(istate2str (ScrState is))(**)
val l = drop_last l; (*comes from e, goes to Abs*)
val (Const ("Let",_) $ e $ (Abs (i,T,body))) = go l sc;
val i = mk_Free (i, T);
@@ -1248,19 +1250,20 @@
| NasApp iss => astep_up ys iss
| NasNap (v, E) => astep_up ys ((E,l,a,v,S,b),ss) end
- | ass_up ys iss (Abs (_,_,_)) =
- astep_up ys iss (*TODO 5.9.00: env ?*)
+ | ass_up ys (iss as (is,_)) (Abs (_,_,_)) =
+ ((**)writeln("### ass_up Abs: is=");
+ writeln(istate2str (ScrState is));(**)
+ astep_up ys iss) (*TODO 5.9.00: env ?*)
| ass_up ys (iss as (is,_)) (Const ("Let",_) $ e $ (Abs (i,T,b)))=
- ((*writeln("### ass_up Let$e$Abs: is=");
- writeln(istate2str (ScrState is));*)
+ ((**)writeln("### ass_up Let $ e $ Abs: is=");
+ writeln(istate2str (ScrState is));(**)
astep_up ys iss) (*TODO 5.9.00: env ?*)
-
- | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _ $ _) =
(* val (ysa, iss, (Const ("Script.Seq",_) $ _ $ _ $ _)) =
(ys, ((E,up,a,v,S,b),ss), (go up sc));
*)
+ | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _ $ _) =
astep_up ysa iss (*all has been done in (*2*) below*)
| ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _) =
@@ -1284,17 +1287,18 @@
| NasApp iss => astep_up ysa iss
| ay => ay end
- | ass_up ysa iss (Const ("Script.Try",_) $ e $ _) =
(* val (ysa, iss, (Const ("Script.Try",_) $ e $ _)) =
(ys, ((E,up,a,v,S,b),ss), (go up sc));
*)
+ | ass_up ysa iss (Const ("Script.Try",_) $ e $ _) =
astep_up ysa iss
+ (* val (ysa, iss, (Const ("Script.Try",_) $ e)) =
+ (ys, ((E,up,a,v,S,b),ss), (go up sc));
+ *)
| ass_up ysa iss (Const ("Script.Try",_) $ e) =
- (* val (ysa, iss, (Const ("Script.Try",_) $ e)) =
- (ys, ((E,up,a,v,S,b),ss), (go up sc));
- *)
- astep_up ysa iss
+ ((**)writeln("### ass_up Try $ e");(**)
+ astep_up ysa iss)
| ass_up (ys as (y,s,_,d)) ((E,l,_,v,S,b),ss)
(*(Const ("Script.While",_) $ c $ e $ a) = WN050930 blind fix*)
@@ -1346,24 +1350,22 @@
| ass_up y ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $ _ ) =
astep_up y ((E, (drop_last l), a,v,S,b),ss)
- | ass_up y iss t =
+ | ass_up y iss t =
raise error ("ass_up not impl for t= "^(term2str t))
(* 9.6.03
val (ys as (_,_,Script sc,_), ss) =
((thy',srls,scr,d), [(m,EmptyMout,pt,p,[])]:step list);
astep_up ys ((E,l,a,v,S,b),ss);
-
+ val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
+ (ysa, iss);
val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
-
- val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
- (ysa, iss);
*)
and astep_up (ys as (_,_,Script sc,_)) ((E,l,a,v,S,b),ss) =
- if 1 < length l
+ if 1 < length l
then
let val up = drop_last l;
- (*val _= writeln("### astep_up: E= "env2str E);*)
+ (**)val _= writeln("### astep_up: E= "^env2str E);(**)
in ass_up ys ((E,up,a,v,S,b),ss) (go up sc) end
else (NasNap (v, E))
;
diff -r a95383a1f758 -r 7cb662bd345d src/smltest/IsacKnowledge/polyminus.sml
--- a/src/smltest/IsacKnowledge/polyminus.sml Wed Jan 02 14:42:04 2008 +0100
+++ b/src/smltest/IsacKnowledge/polyminus.sml Wed Jan 02 18:13:59 2008 +0100
@@ -277,15 +277,35 @@
autoCalculate 1 CompleteCalcHead;
autoCalculate 1 (Step 1);
autoCalculate 1 (Step 1);
+val ((pt,p),_) = get_calc 1; show_pt pt;
-val ((pt,p),_) = get_calc 1;
-show_pt pt;
fetchApplicableTactics 1 0 p;
val appltacs = sel_appl_atomic_tacs pt p;
+applyTactic 1 p (hd appltacs);
+val ((pt,p),_) = get_calc 1; show_pt pt;
+
+applyTactic 1 p (hd (sel_appl_atomic_tacs pt p));
+val ((pt,p),_) = get_calc 1; show_pt pt;
+
+applyTactic 1 p (hd (sel_appl_atomic_tacs pt p));
+val ((pt,p),_) = get_calc 1; show_pt pt;
+
+applyTactic 1 p (hd (sel_appl_atomic_tacs pt p));
+val ((pt,p),_) = get_calc 1; show_pt pt;
+
+applyTactic 1 p (hd (sel_appl_atomic_tacs pt p));
+val ((pt,p),_) = get_calc 1; show_pt pt;
+
+(**)
+applyTactic 1 p (hd (sel_appl_atomic_tacs pt p));
+val ((pt,p),_) = get_calc 1; show_pt pt;
+
+
+
+
+
(*vvv this gives failure *)
-applyTactic 1 p (hd appltacs);
-applyTactic 1 p ((hd o tl) appltacs);
(*vvv only this (= autoCalculate tac) works*)
applyTactic 1 p (Rewrite_Set "fasse_zusammen");
diff -r a95383a1f758 -r 7cb662bd345d src/smltest/ME/script.sml
--- a/src/smltest/ME/script.sml Wed Jan 02 14:42:04 2008 +0100
+++ b/src/smltest/ME/script.sml Wed Jan 02 18:13:59 2008 +0100
@@ -230,7 +230,6 @@
autoCalculate 1 (Step 1);
autoCalculate 1 (Step 1);
val ((pt, p), _) = get_calc 1; show_pt pt;
-show_pt pt;
val appltacs = sel_appl_atomic_tacs pt p;
if appltacs =
[Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
@@ -238,14 +237,14 @@
Calculate "op *"(*..wrong opID: TODO.WN080102 "times" ok*)] then ()
else raise error "script.sml fun sel_appl_atomic_tacs diff.behav.";
-setNextTactic 1 (*p*) (Rewrite_Set "Test_simplify");
-(*^^^ this tac (= as by autoCalculate !) gives ok *)
+trace_script := true;
+trace_script := false;
+applyTactic 1 p (hd appltacs);
+val ((pt, p), _) = get_calc 1; show_pt pt;
+val appltacs = sel_appl_atomic_tacs pt p;
-(*--------------------- while this vvv (<> as by autoCalculate !) gives
+"----- WN080102 these vvv do not work, because locatetac starts the search\
+ \1 stac too low";
+applyTactic 1 p (hd appltacs);
+autoCalculate 1 CompleteCalc;
-> setNextTactic 1 (*p*) (Rewrite ("radd_commute", "?m + ?n = ?n + ?m"));
-*** upd_env_opt: (None,Subproblem (Test.thy, [linear, univariate, ...]))
-*** assy: call by ([3], Pbl)
-
-applyTactic 1 p (hd appltacs);
-----------------------------------------------------------------------*)
\ No newline at end of file