1.1 --- a/src/sml/FE-interface/interface.sml Fri Jan 04 11:16:28 2008 +0100
1.2 +++ b/src/sml/FE-interface/interface.sml Fri Jan 04 16:08:52 2008 +0100
1.3 @@ -162,12 +162,13 @@
1.4
1.5 (*. apply a tactic at a position and update the calc-tree if applicable .*)
1.6 (* val (cI, ip, tac) = (1, p, hd appltacs);
1.7 + val (cI, ip, tac) = (1, p, (hd (sel_appl_atomic_tacs pt p)));
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
1.12 in case locatetac tac (pt, ip) of
1.13 -(* val ("ok", (tacis, c, (_,p'))) = locatetac tac (pt, ip);
1.14 +(* val ("ok", (tacis, c, (pt',p'))) = locatetac tac (pt, ip);
1.15 *)
1.16 ("ok", (_, c, ptp as (_,p'))) =>
1.17 (upd_calc cI (ptp, []); upd_ipos cI 1 p';
2.1 --- a/src/sml/IsacKnowledge/PolyMinus.ML Fri Jan 04 11:16:28 2008 +0100
2.2 +++ b/src/sml/IsacKnowledge/PolyMinus.ML Fri Jan 04 16:08:52 2008 +0100
2.3 @@ -116,11 +116,11 @@
2.4 Thm ("real_one_collect_assoc_r",num_str real_one_collect_assoc_r),
2.5 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
2.6
2.7 - Thm ("addiere_x_plus_minus",num_str addiere_x_plus_minus),
2.8 + Thm ("subtrahiere_x_plus_minus",num_str subtrahiere_x_plus_minus),
2.9 (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)
2.10 - Thm ("addiere_x_minus_plus",num_str addiere_x_minus_plus),
2.11 + Thm ("subtrahiere_x_minus_plus",num_str subtrahiere_x_minus_plus),
2.12 (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)
2.13 - Thm ("addiere_x_minus_minus",num_str addiere_x_minus_minus),
2.14 + Thm ("subtrahiere_x_minus_minus",num_str subtrahiere_x_minus_minus),
2.15 (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*)
2.16
2.17 Calc ("op +", eval_binop "#add_"),
2.18 @@ -209,9 +209,9 @@
2.19 (["polynom","vereinfachen"],
2.20 [("#Given" ,["term t_"]),
2.21 ("#Where" ,["t_ is_polyexp",
2.22 - "Not (matchsub (?a + (?b + ?c)) t_ & \
2.23 - \ matchsub (?a + (?b - ?c)) t_ & \
2.24 - \ matchsub (?a - (?b + ?c)) t_ & \
2.25 + "Not (matchsub (?a + (?b + ?c)) t_ | \
2.26 + \ matchsub (?a + (?b - ?c)) t_ | \
2.27 + \ matchsub (?a - (?b + ?c)) t_ | \
2.28 \ matchsub (?a + (?b - ?c)) t_ )"]),
2.29 ("#Find" ,["normalform n_"])
2.30 ],
2.31 @@ -280,9 +280,9 @@
2.32 (["simplification","for_polynomials","with_minus"],
2.33 [("#Given" ,["term t_"]),
2.34 ("#Where" ,["t_ is_polyexp",
2.35 - "Not (matchsub (?a + (?b + ?c)) t_ & \
2.36 - \ matchsub (?a + (?b - ?c)) t_ & \
2.37 - \ matchsub (?a - (?b + ?c)) t_ & \
2.38 + "Not (matchsub (?a + (?b + ?c)) t_ | \
2.39 + \ matchsub (?a + (?b - ?c)) t_ | \
2.40 + \ matchsub (?a - (?b + ?c)) t_ | \
2.41 \ matchsub (?a + (?b - ?c)) t_ )"]),
2.42 ("#Find" ,["normalform n_"])
2.43 ],
3.1 --- a/src/sml/IsacKnowledge/PolyMinus.thy Fri Jan 04 11:16:28 2008 +0100
3.2 +++ b/src/sml/IsacKnowledge/PolyMinus.thy Fri Jan 04 16:08:52 2008 +0100
3.3 @@ -30,19 +30,22 @@
3.4
3.5 rules
3.6
3.7 - tausche_plus "[| a kleiner b; b ist_monom |] ==> (b + a) = (a + b)"
3.8 - tausche_minus "[| a kleiner b; b ist_monom |] ==> (b - a) = (-a + b)"
3.9 + (*commute with invariant (a.b).c -association*)
3.10 + tausche_plus "[| b ist_monom; a kleiner b |] ==> \
3.11 + \(b + a) = (a + b)"
3.12 + tausche_minus "[| b ist_monom; a kleiner b |] ==> \
3.13 + \(b - a) = (-a + b)"
3.14 tausche_plus_plus "b kleiner c ==> (a + c + b) = (a + b + c)"
3.15 tausche_plus_minus "b kleiner c ==> (a + c - b) = (a - b + c)"
3.16 tausche_minus_plus "b kleiner c ==> (a - c + b) = (a + b - c)"
3.17 tausche_minus_minus "b kleiner c ==> (a - c - b) = (a - b - c)"
3.18
3.19 - addiere_x_plus_minus "[| l is_const; m is_const |] ==> \
3.20 - \(k + m * n) - l * n = k + (m - l) * n"
3.21 - addiere_x_minus_plus "[| l is_const; m is_const |] ==> \
3.22 - \(k - m * n) + l * n = k + (-m + l) * n"
3.23 - addiere_x_minus_minus "[| l is_const; m is_const |] ==> \
3.24 - \(k - m * n) - l * n = k + (-m - l) * n"
3.25 + subtrahiere_x_plus_minus "[| l is_const; m is_const |] ==> \
3.26 + \(k + m * n) - l * n = k + (m - l) * n"
3.27 + subtrahiere_x_minus_plus "[| l is_const; m is_const |] ==> \
3.28 + \(k - m * n) + l * n = k + (-m + l) * n"
3.29 + subtrahiere_x_minus_minus "[| l is_const; m is_const |] ==> \
3.30 + \(k - m * n) - l * n = k + (-m - l) * n"
3.31
3.32 vorzeichen_minus_weg1 "l kleiner 0 ==> a + l * b = a - -1*l * b"
3.33 vorzeichen_minus_weg2 "l kleiner 0 ==> a - l * b = a + -1*l * b"
4.1 --- a/src/sml/ME/mathengine.sml Fri Jan 04 11:16:28 2008 +0100
4.2 +++ b/src/sml/ME/mathengine.sml Fri Jan 04 16:08:52 2008 +0100
4.3 @@ -89,6 +89,7 @@
4.4 (Error' (Error_ e)) => ERror e
4.5 | _ => Updated ([], [], (pt,p)) end;
4.6
4.7 +(*. TODO push return-value cs' into solve and rename solve->loc_solve?_? .*)
4.8 (* val (m, pos) = ((mI,m), ip);
4.9 val (m,(pt,pos) ) = ((mI,m), ptp);
4.10 *)
5.1 --- a/src/sml/ME/rewtools.sml Fri Jan 04 11:16:28 2008 +0100
5.2 +++ b/src/sml/ME/rewtools.sml Fri Jan 04 16:08:52 2008 +0100
5.3 @@ -619,8 +619,10 @@
5.4 | find r12 = eq_rule r12
5.5 and finds [] = false
5.6 | finds (r1 :: rs) = if eq_rule (r, r1) then true else finds rs;
5.7 - in writeln ("### contains_rule: r = "^rule2str r^", rls = "^rls2str rls);
5.8 - finds (get_rules rls) end;
5.9 + in
5.10 + (*writeln ("### contains_rule: r = "^rule2str r^", rls = "^rls2str rls);*)
5.11 + finds (get_rules rls)
5.12 + end;
5.13
5.14 (*. try if a rewrite-rule is applicable to a given formula;
5.15 in case of rule-sets (recursivley) collect all _atomic_ rewrites .*)
6.1 --- a/src/sml/ME/script.sml Fri Jan 04 11:16:28 2008 +0100
6.2 +++ b/src/sml/ME/script.sml Fri Jan 04 16:08:52 2008 +0100
6.3 @@ -1082,8 +1082,8 @@
6.4 (* val (ya, (is as (E,l,a,v,S,b),ss),Const ("Let",_) $ e $ (Abs (id,T,body))) =
6.5 (*1*)(((ts,d),Aundef), ((E,[R],a,v,S,b),[(m,EmptyMout,pt,p,[])]), body);
6.6 *)
6.7 - ((**)writeln("### assy Let$e$Abs: is=");
6.8 - writeln(istate2str (ScrState is));(**)
6.9 + ((*writeln("### assy Let$e$Abs: is=");
6.10 + writeln(istate2str (ScrState is));*)
6.11 case assy ya ((E , l@[L,R], a,v,S,b),ss) e of
6.12 NasApp ((E',l,a,v,S,bb),ss) =>
6.13 let val id' = mk_Free (id, T);
6.14 @@ -1119,12 +1119,12 @@
6.15 else assy ya ((E, l@[ R], a,v,S,b),ss) e2)
6.16
6.17 | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Try",_) $ e $ a) =
6.18 - ((**)writeln("### assy Try $ e $ a, l= "^(loc_2str l));(**)
6.19 + ((*writeln("### assy Try $ e $ a, l= "^(loc_2str l));*)
6.20 case assy ya ((E, l@[L,R], Some a,v,S,b),ss) e of
6.21 ay => ay)
6.22
6.23 | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Try",_) $ e) =
6.24 - ((**)writeln("### assy Try $ e, l= "^(loc_2str l));(**)
6.25 + ((*writeln("### assy Try $ e, l= "^(loc_2str l));*)
6.26 case assy ya ((E, l@[R], a,v,S,b),ss) e of
6.27 ay => ay)
6.28 (* val (ya, ((E,l,_,v,S,b),ss), (Const ("Script.Seq",_) $e1 $ e2 $ a)) =
6.29 @@ -1180,36 +1180,36 @@
6.30 *)
6.31
6.32 | assy (((thy',sr),d),ap) (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss) t =
6.33 - ((**)writeln("### assy, m = "^tac_2str m);
6.34 + ((*writeln("### assy, m = "^tac_2str m);
6.35 writeln("### assy, (p,p_) = "^pos'2str (p,p_));
6.36 writeln("### assy, is= ");
6.37 - writeln(istate2str (ScrState is));(**)
6.38 + writeln(istate2str (ScrState is));*)
6.39 case handle_leaf "locate" thy' sr E a v t of
6.40 (a', Expr s) =>
6.41 - ((**)writeln("### assy: listexpr t= "^(term2str t));
6.42 + ((*writeln("### assy: listexpr t= "^(term2str t));
6.43 writeln("### assy, E= "^(env2str E));
6.44 writeln("### assy, eval(..)= "^(term2str
6.45 (eval_listexpr_ (assoc_thy thy') sr
6.46 - (subst_atomic (upd_env_opt E (a',v)) t))));(**)
6.47 + (subst_atomic (upd_env_opt E (a',v)) t))));*)
6.48 NasNap (eval_listexpr_ (assoc_thy thy') sr
6.49 (subst_atomic (upd_env_opt E (a',v)) t), E))
6.50 (* val (_,STac stac) = subst_stacexpr E a v t;
6.51 *)
6.52 | (a', STac stac) =>
6.53 - let (**)val _=writeln("### assy, stac = "^term2str stac);(**)
6.54 + let (*val _=writeln("### assy, stac = "^term2str stac);*)
6.55 val p' = case p_ of Frm => p | Res => lev_on p
6.56 | _ => raise error ("assy: call by "^
6.57 (pos'2str (p,p_)));
6.58 in case assod pt d m stac of
6.59 Ass (m,v') =>
6.60 - let (**)val _=writeln("### assy: Ass ("^tac_2str m^", "^
6.61 - term2str v'^")");(**)
6.62 + let (*val _=writeln("### assy: Ass ("^tac_2str m^", "^
6.63 + term2str v'^")");*)
6.64 val (p'',c',f',pt') = generate1 (assoc_thy thy') m
6.65 (ScrState (E,l,a',v',S,true)) (p',p_) pt;
6.66 in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
6.67 | AssWeak (m,v') =>
6.68 - let (**)val _=writeln("### assy: Ass Weak("^tac_2str m^", "^
6.69 - term2str v'^")");(**)
6.70 + let (*val _=writeln("### assy: Ass Weak("^tac_2str m^", "^
6.71 + term2str v'^")");*)
6.72 val (p'',c',f',pt') = generate1 (assoc_thy thy') m
6.73 (ScrState (E,l,a',v',S,false)) (p',p_) pt;
6.74 in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
6.75 @@ -1238,8 +1238,8 @@
6.76 *)
6.77 fun ass_up (ys as (y,s,Script sc,d)) (is as (E,l,a,v,S,b),ss)
6.78 (Const ("Let",_) $ _) =
6.79 - let (**)val _= writeln("### ass_up1 Let$e: is=")
6.80 - val _= writeln(istate2str (ScrState is))(**)
6.81 + let (*val _= writeln("### ass_up1 Let$e: is=")
6.82 + val _= writeln(istate2str (ScrState is))*)
6.83 val l = drop_last l; (*comes from e, goes to Abs*)
6.84 val (Const ("Let",_) $ e $ (Abs (i,T,body))) = go l sc;
6.85 val i = mk_Free (i, T);
6.86 @@ -1251,13 +1251,13 @@
6.87 | NasNap (v, E) => astep_up ys ((E,l,a,v,S,b),ss) end
6.88
6.89 | ass_up ys (iss as (is,_)) (Abs (_,_,_)) =
6.90 - ((**)writeln("### ass_up Abs: is=");
6.91 - writeln(istate2str (ScrState is));(**)
6.92 + ((*writeln("### ass_up Abs: is=");
6.93 + writeln(istate2str (ScrState is));*)
6.94 astep_up ys iss) (*TODO 5.9.00: env ?*)
6.95
6.96 | ass_up ys (iss as (is,_)) (Const ("Let",_) $ e $ (Abs (i,T,b)))=
6.97 - ((**)writeln("### ass_up Let $ e $ Abs: is=");
6.98 - writeln(istate2str (ScrState is));(**)
6.99 + ((*writeln("### ass_up Let $ e $ Abs: is=");
6.100 + writeln(istate2str (ScrState is));*)
6.101 astep_up ys iss) (*TODO 5.9.00: env ?*)
6.102
6.103 (* val (ysa, iss, (Const ("Script.Seq",_) $ _ $ _ $ _)) =
6.104 @@ -1297,7 +1297,7 @@
6.105 (ys, ((E,up,a,v,S,b),ss), (go up sc));
6.106 *)
6.107 | ass_up ysa iss (Const ("Script.Try",_) $ e) =
6.108 - ((**)writeln("### ass_up Try $ e");(**)
6.109 + ((*writeln("### ass_up Try $ e");*)
6.110 astep_up ysa iss)
6.111
6.112 | ass_up (ys as (y,s,_,d)) ((E,l,_,v,S,b),ss)
6.113 @@ -1365,7 +1365,7 @@
6.114 if 1 < length l
6.115 then
6.116 let val up = drop_last l;
6.117 - (**)val _= writeln("### astep_up: E= "^env2str E);(**)
6.118 + (*val _= writeln("### astep_up: E= "^env2str E);*)
6.119 in ass_up ys ((E,up,a,v,S,b),ss) (go up sc) end
6.120 else (NasNap (v, E))
6.121 ;
6.122 @@ -1454,7 +1454,7 @@
6.123
6.124 val (ts as (thy',srls), m, (pt,p),
6.125 (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b))) =
6.126 - ((thy',srls), m, (pt,(p, p_)), (sc,d), is);
6.127 + ((thy',srls), m, (pt,(p,p_)), (sc,d), is);
6.128 *)
6.129 | locate_gen (ts as (thy',srls)) (m:tac_) ((pt,p):ptree * pos')
6.130 (scr as Script (h $ body),d) (ScrState (E,l,a,v,S,b)) =
6.131 @@ -1473,12 +1473,15 @@
6.132 else (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b),
6.133 [(m,EmptyMout,pt,p,[])]) ) of
6.134 Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =>
6.135 +(* val Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =
6.136 + (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b),
6.137 + [(m,EmptyMout,pt,p,[])]) );
6.138 + *)
6.139 ((*writeln("### locate_gen Assoc: p'="^(pos'2str p'));*)
6.140 if bb then Steps (ScrState is, ss)
6.141 - else if rew_only ss (*andalso 'not bb'= associated weakly*)
6.142 - then let (*val _=writeln("### locate_gen, bef g1: p="^(pos'2str p));*)
6.143 - val (po,p_) = p;
6.144 - val po' = case p_ of Frm => po | Res => lev_on po
6.145 + else if rew_only ss (*andalso 'not bb'= associated weakly*)
6.146 + then let val (po,p_) = p
6.147 + val po' = case p_ of Frm => po | Res => lev_on po
6.148 (*WN.12.03: noticed, that pos is also updated in assy !?!
6.149 instead take p' from Assoc ?????????????????????????????*)
6.150 val (p'',c'',f'',pt'') =
7.1 --- a/src/smltest/IsacKnowledge/polyminus.sml Fri Jan 04 11:16:28 2008 +0100
7.2 +++ b/src/smltest/IsacKnowledge/polyminus.sml Fri Jan 04 16:08:52 2008 +0100
7.3 @@ -281,24 +281,32 @@
7.4 "----- 1 ^^^";
7.5 fetchApplicableTactics 1 0 p;
7.6 val appltacs = sel_appl_atomic_tacs pt p;
7.7 -applyTactic 1 p (hd appltacs);
7.8 +applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*);
7.9 val ((pt,p),_) = get_calc 1; show_pt pt;
7.10 "----- 2 ^^^";
7.11 -applyTactic 1 p (hd (sel_appl_atomic_tacs pt p));
7.12 +trace_rewrite := true;
7.13 +val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
7.14 +val Some (t',_) =
7.15 + rewrite_ Isac.thy e_rew_ord erls_ordne_alphabetisch false tausche_minus t;
7.16 +term2str t'; "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g";
7.17 +trace_rewrite := false;
7.18 +
7.19 +
7.20 +applyTactic 1 p (hd (sel_appl_atomic_tacs pt p)) (*tausche_minus*);
7.21 val ((pt,p),_) = get_calc 1; show_pt pt;
7.22 "----- 3 ^^^";
7.23 -applyTactic 1 p (hd (sel_appl_atomic_tacs pt p));
7.24 +applyTactic 1 p (hd (sel_appl_atomic_tacs pt p)) (**);
7.25 val ((pt,p),_) = get_calc 1; show_pt pt;
7.26 "----- 4 ^^^";
7.27 -applyTactic 1 p (hd (sel_appl_atomic_tacs pt p));
7.28 +applyTactic 1 p (hd (sel_appl_atomic_tacs pt p)) (**);
7.29 val ((pt,p),_) = get_calc 1; show_pt pt;
7.30 "----- 5 ^^^";
7.31 -applyTactic 1 p (hd (sel_appl_atomic_tacs pt p));
7.32 +applyTactic 1 p (hd (sel_appl_atomic_tacs pt p)) (**);
7.33 val ((pt,p),_) = get_calc 1; show_pt pt;
7.34 "----- 6 ^^^";
7.35
7.36 (*<CALCMESSAGE> failure </CALCMESSAGE>
7.37 -applyTactic 1 p (hd (sel_appl_atomic_tacs pt p));
7.38 +applyTactic 1 p (hd (sel_appl_atomic_tacs pt p)) (**);
7.39 val ((pt,p),_) = get_calc 1; show_pt pt;
7.40 "----- 7 ^^^";
7.41 *)
7.42 @@ -315,3 +323,11 @@
7.43 use"polyminus.sml";
7.44 *)
7.45
7.46 +states:=[];
7.47 +CalcTree [(["term ((- 4 + 6) * f)",
7.48 + "normalform N"],
7.49 + ("PolyMinus.thy",["polynom","vereinfachen"],
7.50 + ["simplification","for_polynomials","with_minus"]))];
7.51 +moveActiveRoot 1;
7.52 +autoCalculate 1 CompleteCalc;
7.53 +val ((pt,p),_) = get_calc 1; show_pt pt;