1.1 --- a/src/sml/FE-interface/interface.sml Wed Jan 02 14:42:04 2008 +0100
1.2 +++ b/src/sml/FE-interface/interface.sml Wed Jan 02 18:13:59 2008 +0100
1.3 @@ -161,6 +161,8 @@
1.4 end;
1.5
1.6 (*. apply a tactic at a position and update the calc-tree if applicable .*)
1.7 +(* val (cI, ip, tac) = (1, p, hd appltacs);
1.8 + *)
1.9 fun applyTactic (cI:calcID) ip tac =
1.10 let val ((pt, _), _) = get_calc cI
1.11 val p = get_pos cI 1
2.1 --- a/src/sml/ME/mathengine.sml Wed Jan 02 14:42:04 2008 +0100
2.2 +++ b/src/sml/ME/mathengine.sml Wed Jan 02 18:13:59 2008 +0100
2.3 @@ -107,10 +107,11 @@
2.4 HElpless (**)
2.5 | Nexts of calcstate; (**)
2.6
2.7 +(*. locate a tactic in a script and apply it if possible .*)
2.8 (*report applicability of tac in tacis; pt is dropped in setNextTactic*)
2.9 fun locatetac _ (ptp as (_,([],Res))) = ("end-of-calculation", ([], [], ptp))
2.10 -(* val ptp as (pt, p) = (pt, ip);
2.11 - val ptp as (pt, p) = (pt, p);
2.12 +(* val ptp as (pt, p) = (pt, p);
2.13 + val ptp as (pt, p) = (pt, ip);
2.14 *)
2.15 | locatetac tac (ptp as (pt, p)) =
2.16 let val (mI,m) = mk_tac'_ tac;
3.1 --- a/src/sml/ME/rewtools.sml Wed Jan 02 14:42:04 2008 +0100
3.2 +++ b/src/sml/ME/rewtools.sml Wed Jan 02 18:13:59 2008 +0100
3.3 @@ -619,7 +619,8 @@
3.4 | find r12 = eq_rule r12
3.5 and finds [] = false
3.6 | finds (r1 :: rs) = if eq_rule (r, r1) then true else finds rs;
3.7 - in finds (get_rules rls) end;
3.8 + in writeln ("### contains_rule: r = "^rule2str r^", rls = "^rls2str rls);
3.9 + finds (get_rules rls) end;
3.10
3.11 (*. try if a rewrite-rule is applicable to a given formula;
3.12 in case of rule-sets (recursivley) collect all _atomic_ rewrites .*)
4.1 --- a/src/sml/ME/script.sml Wed Jan 02 14:42:04 2008 +0100
4.2 +++ b/src/sml/ME/script.sml Wed Jan 02 18:13:59 2008 +0100
4.3 @@ -648,9 +648,9 @@
4.4 AssWeak (m,f'))
4.5 else ((*writeln"3### assod ..NotAss";*)NotAss))
4.6 | (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =>
4.7 - if contains_rule (Thm (thmID, refl(*dummy*))) rls then
4.8 - if f = f_ then Ass (m,f') else AssWeak (m,f')
4.9 - else NotAss
4.10 + if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_) then
4.11 + if f = f_ then Ass (m,f') else AssWeak (m,f')
4.12 + else NotAss
4.13 | _ => NotAss)
4.14
4.15 (*val f = (term_of o the o (parse thy))"#0+(sqrt(sqrt(sqrt a))^^^#2)^^^#2=#0";
4.16 @@ -1082,8 +1082,8 @@
4.17 (* val (ya, (is as (E,l,a,v,S,b),ss),Const ("Let",_) $ e $ (Abs (id,T,body))) =
4.18 (*1*)(((ts,d),Aundef), ((E,[R],a,v,S,b),[(m,EmptyMout,pt,p,[])]), body);
4.19 *)
4.20 - ((*writeln("### assy Let$e$Abs: is=");
4.21 - writeln(istate2str (ScrState is));*)
4.22 + ((**)writeln("### assy Let$e$Abs: is=");
4.23 + writeln(istate2str (ScrState is));(**)
4.24 case assy ya ((E , l@[L,R], a,v,S,b),ss) e of
4.25 NasApp ((E',l,a,v,S,bb),ss) =>
4.26 let val id' = mk_Free (id, T);
4.27 @@ -1119,12 +1119,12 @@
4.28 else assy ya ((E, l@[ R], a,v,S,b),ss) e2)
4.29
4.30 | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Try",_) $ e $ a) =
4.31 - ((*writeln("### assy Try, l= "^(loc_2str l));*)
4.32 + ((**)writeln("### assy Try $ e $ a, l= "^(loc_2str l));(**)
4.33 case assy ya ((E, l@[L,R], Some a,v,S,b),ss) e of
4.34 ay => ay)
4.35
4.36 | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Try",_) $ e) =
4.37 - ((*writeln("### assy Try, l= "^(loc_2str l));*)
4.38 + ((**)writeln("### assy Try $ e, l= "^(loc_2str l));(**)
4.39 case assy ya ((E, l@[R], a,v,S,b),ss) e of
4.40 ay => ay)
4.41 (* val (ya, ((E,l,_,v,S,b),ss), (Const ("Script.Seq",_) $e1 $ e2 $ a)) =
4.42 @@ -1180,35 +1180,37 @@
4.43 *)
4.44
4.45 | assy (((thy',sr),d),ap) (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss) t =
4.46 - ((*writeln("### assy, m = "^tac_2str m);
4.47 + ((**)writeln("### assy, m = "^tac_2str m);
4.48 writeln("### assy, (p,p_) = "^pos'2str (p,p_));
4.49 writeln("### assy, is= ");
4.50 - writeln(istate2str (ScrState is));*)
4.51 + writeln(istate2str (ScrState is));(**)
4.52 case handle_leaf "locate" thy' sr E a v t of
4.53 (a', Expr s) =>
4.54 - ((*writeln("### assy: listexpr t= "^(term2str t));
4.55 + ((**)writeln("### assy: listexpr t= "^(term2str t));
4.56 writeln("### assy, E= "^(env2str E));
4.57 writeln("### assy, eval(..)= "^(term2str
4.58 (eval_listexpr_ (assoc_thy thy') sr
4.59 - (subst_atomic (upd_env_opt E (a',v)) t))));*)
4.60 + (subst_atomic (upd_env_opt E (a',v)) t))));(**)
4.61 NasNap (eval_listexpr_ (assoc_thy thy') sr
4.62 (subst_atomic (upd_env_opt E (a',v)) t), E))
4.63 (* val (_,STac stac) = subst_stacexpr E a v t;
4.64 *)
4.65 | (a', STac stac) =>
4.66 - let (*val _=writeln("### assy, stac = "^term2str stac);*)
4.67 + let (**)val _=writeln("### assy, stac = "^term2str stac);(**)
4.68 val p' = case p_ of Frm => p | Res => lev_on p
4.69 | _ => raise error ("assy: call by "^
4.70 (pos'2str (p,p_)));
4.71 in case assod pt d m stac of
4.72 Ass (m,v') =>
4.73 - let (*val _=writeln("### assy: Ass ("^tac_2str m^",
4.74 - "^term2str v'^")");*)
4.75 + let (**)val _=writeln("### assy: Ass ("^tac_2str m^", "^
4.76 + term2str v'^")");(**)
4.77 val (p'',c',f',pt') = generate1 (assoc_thy thy') m
4.78 (ScrState (E,l,a',v',S,true)) (p',p_) pt;
4.79 in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
4.80 | AssWeak (m,v') =>
4.81 - let val (p'',c',f',pt') = generate1 (assoc_thy thy') m
4.82 + let (**)val _=writeln("### assy: Ass Weak("^tac_2str m^", "^
4.83 + term2str v'^")");(**)
4.84 + val (p'',c',f',pt') = generate1 (assoc_thy thy') m
4.85 (ScrState (E,l,a',v',S,false)) (p',p_) pt;
4.86 in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
4.87 | NotAss =>
4.88 @@ -1236,8 +1238,8 @@
4.89 *)
4.90 fun ass_up (ys as (y,s,Script sc,d)) (is as (E,l,a,v,S,b),ss)
4.91 (Const ("Let",_) $ _) =
4.92 - let (*val _= writeln("### ass_up1 Let$e: is=")
4.93 - val _= writeln(istate2str (ScrState is))*)
4.94 + let (**)val _= writeln("### ass_up1 Let$e: is=")
4.95 + val _= writeln(istate2str (ScrState is))(**)
4.96 val l = drop_last l; (*comes from e, goes to Abs*)
4.97 val (Const ("Let",_) $ e $ (Abs (i,T,body))) = go l sc;
4.98 val i = mk_Free (i, T);
4.99 @@ -1248,19 +1250,20 @@
4.100 | NasApp iss => astep_up ys iss
4.101 | NasNap (v, E) => astep_up ys ((E,l,a,v,S,b),ss) end
4.102
4.103 - | ass_up ys iss (Abs (_,_,_)) =
4.104 - astep_up ys iss (*TODO 5.9.00: env ?*)
4.105 + | ass_up ys (iss as (is,_)) (Abs (_,_,_)) =
4.106 + ((**)writeln("### ass_up Abs: is=");
4.107 + writeln(istate2str (ScrState is));(**)
4.108 + astep_up ys iss) (*TODO 5.9.00: env ?*)
4.109
4.110 | ass_up ys (iss as (is,_)) (Const ("Let",_) $ e $ (Abs (i,T,b)))=
4.111 - ((*writeln("### ass_up Let$e$Abs: is=");
4.112 - writeln(istate2str (ScrState is));*)
4.113 + ((**)writeln("### ass_up Let $ e $ Abs: is=");
4.114 + writeln(istate2str (ScrState is));(**)
4.115 astep_up ys iss) (*TODO 5.9.00: env ?*)
4.116
4.117 -
4.118 - | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _ $ _) =
4.119 (* val (ysa, iss, (Const ("Script.Seq",_) $ _ $ _ $ _)) =
4.120 (ys, ((E,up,a,v,S,b),ss), (go up sc));
4.121 *)
4.122 + | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _ $ _) =
4.123 astep_up ysa iss (*all has been done in (*2*) below*)
4.124
4.125 | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _) =
4.126 @@ -1284,17 +1287,18 @@
4.127 | NasApp iss => astep_up ysa iss
4.128 | ay => ay end
4.129
4.130 - | ass_up ysa iss (Const ("Script.Try",_) $ e $ _) =
4.131 (* val (ysa, iss, (Const ("Script.Try",_) $ e $ _)) =
4.132 (ys, ((E,up,a,v,S,b),ss), (go up sc));
4.133 *)
4.134 + | ass_up ysa iss (Const ("Script.Try",_) $ e $ _) =
4.135 astep_up ysa iss
4.136
4.137 + (* val (ysa, iss, (Const ("Script.Try",_) $ e)) =
4.138 + (ys, ((E,up,a,v,S,b),ss), (go up sc));
4.139 + *)
4.140 | ass_up ysa iss (Const ("Script.Try",_) $ e) =
4.141 - (* val (ysa, iss, (Const ("Script.Try",_) $ e)) =
4.142 - (ys, ((E,up,a,v,S,b),ss), (go up sc));
4.143 - *)
4.144 - astep_up ysa iss
4.145 + ((**)writeln("### ass_up Try $ e");(**)
4.146 + astep_up ysa iss)
4.147
4.148 | ass_up (ys as (y,s,_,d)) ((E,l,_,v,S,b),ss)
4.149 (*(Const ("Script.While",_) $ c $ e $ a) = WN050930 blind fix*)
4.150 @@ -1346,24 +1350,22 @@
4.151 | ass_up y ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $ _ ) =
4.152 astep_up y ((E, (drop_last l), a,v,S,b),ss)
4.153
4.154 - | ass_up y iss t =
4.155 + | ass_up y iss t =
4.156 raise error ("ass_up not impl for t= "^(term2str t))
4.157 (* 9.6.03
4.158 val (ys as (_,_,Script sc,_), ss) =
4.159 ((thy',srls,scr,d), [(m,EmptyMout,pt,p,[])]:step list);
4.160 astep_up ys ((E,l,a,v,S,b),ss);
4.161 -
4.162 + val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
4.163 + (ysa, iss);
4.164 val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
4.165 ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
4.166 -
4.167 - val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
4.168 - (ysa, iss);
4.169 *)
4.170 and astep_up (ys as (_,_,Script sc,_)) ((E,l,a,v,S,b),ss) =
4.171 - if 1 < length l
4.172 + if 1 < length l
4.173 then
4.174 let val up = drop_last l;
4.175 - (*val _= writeln("### astep_up: E= "env2str E);*)
4.176 + (**)val _= writeln("### astep_up: E= "^env2str E);(**)
4.177 in ass_up ys ((E,up,a,v,S,b),ss) (go up sc) end
4.178 else (NasNap (v, E))
4.179 ;
5.1 --- a/src/smltest/IsacKnowledge/polyminus.sml Wed Jan 02 14:42:04 2008 +0100
5.2 +++ b/src/smltest/IsacKnowledge/polyminus.sml Wed Jan 02 18:13:59 2008 +0100
5.3 @@ -277,15 +277,35 @@
5.4 autoCalculate 1 CompleteCalcHead;
5.5 autoCalculate 1 (Step 1);
5.6 autoCalculate 1 (Step 1);
5.7 +val ((pt,p),_) = get_calc 1; show_pt pt;
5.8
5.9 -val ((pt,p),_) = get_calc 1;
5.10 -show_pt pt;
5.11 fetchApplicableTactics 1 0 p;
5.12 val appltacs = sel_appl_atomic_tacs pt p;
5.13 +applyTactic 1 p (hd appltacs);
5.14 +val ((pt,p),_) = get_calc 1; show_pt pt;
5.15 +
5.16 +applyTactic 1 p (hd (sel_appl_atomic_tacs pt p));
5.17 +val ((pt,p),_) = get_calc 1; show_pt pt;
5.18 +
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 +applyTactic 1 p (hd (sel_appl_atomic_tacs pt p));
5.23 +val ((pt,p),_) = get_calc 1; show_pt pt;
5.24 +
5.25 +applyTactic 1 p (hd (sel_appl_atomic_tacs pt p));
5.26 +val ((pt,p),_) = get_calc 1; show_pt pt;
5.27 +
5.28 +(**)
5.29 +applyTactic 1 p (hd (sel_appl_atomic_tacs pt p));
5.30 +val ((pt,p),_) = get_calc 1; show_pt pt;
5.31 +
5.32 +
5.33 +
5.34 +
5.35 +
5.36
5.37 (*vvv this gives <CALCMESSAGE> failure </CALCMESSAGE>*)
5.38 -applyTactic 1 p (hd appltacs);
5.39 -applyTactic 1 p ((hd o tl) appltacs);
5.40
5.41 (*vvv only this (= autoCalculate tac) works*)
5.42 applyTactic 1 p (Rewrite_Set "fasse_zusammen");
6.1 --- a/src/smltest/ME/script.sml Wed Jan 02 14:42:04 2008 +0100
6.2 +++ b/src/smltest/ME/script.sml Wed Jan 02 18:13:59 2008 +0100
6.3 @@ -230,7 +230,6 @@
6.4 autoCalculate 1 (Step 1);
6.5 autoCalculate 1 (Step 1);
6.6 val ((pt, p), _) = get_calc 1; show_pt pt;
6.7 -show_pt pt;
6.8 val appltacs = sel_appl_atomic_tacs pt p;
6.9 if appltacs =
6.10 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
6.11 @@ -238,14 +237,14 @@
6.12 Calculate "op *"(*..wrong opID: TODO.WN080102 "times" ok*)] then ()
6.13 else raise error "script.sml fun sel_appl_atomic_tacs diff.behav.";
6.14
6.15 -setNextTactic 1 (*p*) (Rewrite_Set "Test_simplify");
6.16 -(*^^^ this tac (= as by autoCalculate !) gives <MESSAGE> ok </MESSAGE>*)
6.17 +trace_script := true;
6.18 +trace_script := false;
6.19 +applyTactic 1 p (hd appltacs);
6.20 +val ((pt, p), _) = get_calc 1; show_pt pt;
6.21 +val appltacs = sel_appl_atomic_tacs pt p;
6.22
6.23 -(*--------------------- while this vvv (<> as by autoCalculate !) gives
6.24 +"----- WN080102 these vvv do not work, because locatetac starts the search\
6.25 + \1 stac too low";
6.26 +applyTactic 1 p (hd appltacs);
6.27 +autoCalculate 1 CompleteCalc;
6.28
6.29 -> setNextTactic 1 (*p*) (Rewrite ("radd_commute", "?m + ?n = ?n + ?m"));
6.30 -*** upd_env_opt: (None,Subproblem (Test.thy, [linear, univariate, ...]))
6.31 -*** assy: call by ([3], Pbl)
6.32 -
6.33 -applyTactic 1 p (hd appltacs);
6.34 -----------------------------------------------------------------------*)
6.35 \ No newline at end of file