1.1 --- a/src/sml/FE-interface/interface.sml Mon Dec 31 14:18:53 2007 +0100
1.2 +++ b/src/sml/FE-interface/interface.sml Mon Dec 31 17:56:24 2007 +0100
1.3 @@ -250,16 +250,13 @@
1.4 handle _ => sysERROR2xml cI "error in kernel";
1.5 (*.version 2: fetch _applicable_ _elementary_ (ie. recursively
1.6 decompose rule-sets) Rewrite*, Calculate .*)
1.7 -(*
1.8 fun fetchApplicableTactics cI (scope:int) (p:pos') =
1.9 (let val ((pt, _), _) = get_calc cI
1.10 - val alltacs = sel_rules pt p
1.11 - val tacs = @@@@@@@@@
1.12 - in (applicabletacticsOK cI tacs)
1.13 + in (applicabletacticsOK cI (sel_appl_atomic_tacs pt p))
1.14 handle PTREE str => sysERROR2xml cI str
1.15 end)
1.16 handle _ => sysERROR2xml cI "error in kernel";
1.17 -*)
1.18 +
1.19 fun getAssumptions cI (p:pos') =
1.20 (let val ((pt,_),_) = get_calc cI
1.21 val (_, _, asms) = pt_extract (pt, p)
2.1 --- a/src/sml/ME/ctree.sml Mon Dec 31 14:18:53 2007 +0100
2.2 +++ b/src/sml/ME/ctree.sml Mon Dec 31 17:56:24 2007 +0100
2.3 @@ -531,7 +531,6 @@
2.4 | rule2tac _ rule =
2.5 raise error ("rule2tac: called with '" ^ rule2str rule ^ "'");
2.6
2.7 -
2.8 type fmz_ = cterm' list;
2.9
2.10 (*.a formalization of an example containing data
3.1 --- a/src/sml/ME/rewtools.sml Mon Dec 31 14:18:53 2007 +0100
3.2 +++ b/src/sml/ME/rewtools.sml Mon Dec 31 17:56:24 2007 +0100
3.3 @@ -612,25 +612,55 @@
3.4 > thms_of_rls rls;
3.5 *)
3.6
3.7 -(**. get all rules in a rule set (recursivley containing rule sets)
3.8 - applicable to a given formula.**)
3.9 -fun try_rew thy ((_, ro) : rew_ord) erls (subst : subst) f
3.10 - (thm' as Thm (_, thm)) =
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 .*)
3.13 +fun try_rew thy ((_, ro):rew_ord) erls (subst:subst) f (thm' as Thm(id, thm)) =
3.14 if contains_bdv thm
3.15 then case rewrite_inst_ thy ro erls false subst thm f of
3.16 - Some _ => [rule2tac subst thm']
3.17 + Some (f',_) => (writeln("@@@ try_rew: "^id^" -> "^term2str f');
3.18 + [rule2tac subst thm'])
3.19 | None => []
3.20 else (case rewrite_ thy ro erls false thm f of
3.21 - Some_ => [rule2tac [] thm']
3.22 + Some (f',_) => (writeln("@@@ try_rew: "^id^" -> "^term2str f');
3.23 + [rule2tac [] thm'])
3.24 | None => [])
3.25 | try_rew thy _ _ _ f (cal as Calc c) =
3.26 (case get_calculation_ thy c f of
3.27 - Some _ => [rule2tac [] cal]
3.28 + Some (str, _) => (writeln("@@@ try_rew: Calc -> "^str);
3.29 + [rule2tac [] cal])
3.30 | None => [])
3.31 - | try_rew thy _ _ subst f (Rls_ rls) =
3.32 - flat (filter_appl_rews thy subst f rls)
3.33 + | try_rew thy _ _ subst f (Rls_ rls) = filter_appl_rews thy subst f rls
3.34 and filter_appl_rews thy subst f (Rls {rew_ord = ro, erls, rules,...}) =
3.35 - map (try_rew thy ro erls subst f) rules;
3.36 + distinct (flat (map (try_rew thy ro erls subst f) rules))
3.37 + | filter_appl_rews thy subst f (Seq {rew_ord = ro, erls, rules,...}) =
3.38 + distinct (flat (map (try_rew thy ro erls subst f) rules))
3.39 + | filter_appl_rews thy subst f (Rrls _) = [];
3.40 +
3.41 +(*. decide if a tactic is applicable to a given formula;
3.42 + in case of Rewrite_Set* go down to _atomic_ rewrite-tactics .*)
3.43 +(* val
3.44 + *)
3.45 +fun atomic_appl_tacs thy _ _ f (Calculate calcID) =
3.46 + try_rew thy e_rew_ordX e_rls [] f (Calc (snd(assoc1 (!calclist', calcID))))
3.47 +
3.48 + | atomic_appl_tacs thy ro erls f (Rewrite (thm' as (thmID, _))) =
3.49 + try_rew thy (ro, assoc_rew_ord ro) erls [] f
3.50 + (Thm (thmID, assoc_thm' thy thm'))
3.51 + | atomic_appl_tacs thy ro erls f (Rewrite_Inst (subs, thm' as (thmID, _))) =
3.52 + try_rew thy (ro, assoc_rew_ord ro) erls (subs2subst thy subs) f
3.53 + (Thm (thmID, assoc_thm' thy thm'))
3.54 +
3.55 + | atomic_appl_tacs thy _ _ f (Rewrite_Set rls') =
3.56 + filter_appl_rews thy [] f (assoc_rls rls')
3.57 + | atomic_appl_tacs thy _ _ f (Rewrite_Set_Inst (subs, rls')) =
3.58 + filter_appl_rews thy (subs2subst thy subs) f (assoc_rls rls')
3.59 + | atomic_appl_tacs _ _ _ _ tac =
3.60 + (writeln ("### atomic_appl_tacs: not impl. for tac = '"^ tac2str tac ^"'");
3.61 + []);
3.62 +
3.63 +
3.64 +
3.65 +
3.66
3.67 (*.not only for thydata, but also for thy's etc.*)
3.68 fun theID2guh (theID:theID) =
4.1 --- a/src/sml/ME/script.sml Mon Dec 31 14:18:53 2007 +0100
4.2 +++ b/src/sml/ME/script.sml Mon Dec 31 17:56:24 2007 +0100
4.3 @@ -4,7 +4,6 @@
4.4 use"ME/script.sml";
4.5 use"script.sml";
4.6 *)
4.7 -
4.8 signature INTERPRETER =
4.9 sig
4.10 (*type ets (list of executed tactics) see sequent.sml*)
4.11 @@ -2012,12 +2011,34 @@
4.12 > map ((stac2tac pt thy) o #2 o(subst_stacexpr env None e_term)) (stacpbls sc);
4.13 *)
4.14
4.15 -(*. filter applicable tactics while recursively decompose rule-sets
4.16 - to atomic (Rewrite*, Calculate) tactics .*)
4.17 -(*
4.18 -fun @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@2
4.19 -*)
4.20
4.21 +(*. fetch tactics from script and filter _applicable_ tactics;
4.22 + in case of Rewrite_Set* go down to _atomic_ rewrite-tactics .*)
4.23 +fun sel_appl_atomic_tacs _ (([],Res):pos') =
4.24 + raise PTREE "no tactics applicable at the end of a calculation"
4.25 + | sel_appl_atomic_tacs pt (p,p_) =
4.26 + if is_spec_pos p_
4.27 + then [get_obj g_tac pt p]
4.28 + else
4.29 + let val pp = par_pblobj pt p
4.30 + val thy' = (get_obj g_domID pt pp):theory'
4.31 + val thy = assoc_thy thy'
4.32 + val metID = get_obj g_metID pt pp
4.33 + val metID' =if metID = e_metID
4.34 + then (thd3 o snd3) (get_obj g_origin pt pp)
4.35 + else metID
4.36 + val {scr=Script sc,srls,erls,rew_ord'=ro,...} = get_met metID'
4.37 + val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)
4.38 + val alltacs = (*we expect at least 1 stac in a script*)
4.39 + map ((stac2tac pt thy) o rep_stacexpr o #2 o
4.40 + (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)
4.41 + val f = case p_ of
4.42 + Frm => get_obj g_form pt p
4.43 + | Res => (fst o (get_obj g_result pt)) p
4.44 + (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
4.45 + in (distinct o flat o
4.46 + (map (atomic_appl_tacs thy ro erls f))) alltacs end;
4.47 +
4.48
4.49 (*
4.50 end
5.1 --- a/src/sml/calcelems.sml Mon Dec 31 14:18:53 2007 +0100
5.2 +++ b/src/sml/calcelems.sml Mon Dec 31 17:56:24 2007 +0100
5.3 @@ -46,10 +46,14 @@
5.4
5.5 (*TODO.WN060610 make use of "type rew_ord" total*)
5.6 type rew_ord' = string;
5.7 +val e_rew_ord' = "e_rew_ord" : rew_ord';
5.8 +type rew_ord_ = subst -> Term.term * Term.term -> bool;
5.9 fun dummy_ord (_:subst) (_:term,_:term) = true;
5.10 -type rew_ord_ = subst -> Term.term * Term.term -> bool;
5.11 +val e_rew_ord_ = dummy_ord;
5.12 type rew_ord = rew_ord' * rew_ord_;
5.13 -val e_rew_ord = dummy_ord;
5.14 +val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
5.15 +val e_rew_ordX = (e_rew_ord', e_rew_ord_) : rew_ord;
5.16 +
5.17
5.18 datatype rule =
5.19 Erule (*WN.3.6.03 for rep_tac_ Check_elementwise*)
6.1 --- a/src/smltest/ME/rewtools.sml Mon Dec 31 14:18:53 2007 +0100
6.2 +++ b/src/smltest/ME/rewtools.sml Mon Dec 31 17:56:24 2007 +0100
6.3 @@ -500,20 +500,16 @@
6.4 "----------- fun filter_appl_rews --------------------------------";
6.5 "----------- fun filter_appl_rews --------------------------------";
6.6 "----------- fun filter_appl_rews --------------------------------";
6.7 -val f = str2term "a + z + 2*3*x + 4*a + 5+6";
6.8 +val f = str2term "a + z + 2*a + 3*z + 5 + 6";
6.9 val thy = assoc_thy "Isac.thy";
6.10 val subst = [(*TODO.WN071231 test Rewrite_Inst*)];
6.11 val rls = Test_simplify;
6.12 -val Rls {rew_ord = ro, erls, rules,...} = rls;
6.13 +(* val rls = rls_p_33; filter_appl_rews ---> length 2
6.14 + val rls = norm_Poly; filter_appl_rews ---> length 1
6.15 + *)
6.16 +if filter_appl_rews thy subst f rls =
6.17 + [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
6.18 + Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
6.19 + Calculate "op +"] then ()
6.20 +else raise error "rewtools.sml filter_appl_rews a + z + 2*a + 3*z + 5 + 6";
6.21
6.22 -(*
6.23 -
6.24 -rewrite_ thy ro erls false thm f;
6.25 -
6.26 -rewrite_inst_ thy ro erls false subst thm f;
6.27 -
6.28 -print_depth 19;
6.29 - Test_simplify;
6.30 -print_depth 3;
6.31 -
6.32 -*)
6.33 \ No newline at end of file
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/smltest/ME/script.sml Mon Dec 31 17:56:24 2007 +0100
7.3 @@ -0,0 +1,238 @@
7.4 +(* tests for ME/script.sml
7.5 + TODO.WN0509 collect typical tests from systest here !!!!!
7.6 + author: Walther Neuper 050908
7.7 + (c) copyright due to lincense terms.
7.8 +
7.9 +use"../smltest/ME/script.sml";
7.10 +use"script.sml";
7.11 +*)
7.12 +"-----------------------------------------------------------------";
7.13 +"table of contents -----------------------------------------------";
7.14 +"-----------------------------------------------------------------";
7.15 +"----------- WN0509 why does next_tac doesnt find Substitute -----";
7.16 +"----------- WN0509 Substitute 2nd part --------------------------";
7.17 +"----------- fun sel_appl_atomic_tacs ----------------------------";
7.18 +"-----------------------------------------------------------------";
7.19 +"-----------------------------------------------------------------";
7.20 +"-----------------------------------------------------------------";
7.21 +
7.22 +
7.23 +"----------- WN0509 why does next_tac doesnt find Substitute -----";
7.24 +"----------- WN0509 why does next_tac doesnt find Substitute -----";
7.25 +"----------- WN0509 why does next_tac doesnt find Substitute -----";
7.26 +
7.27 +(*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
7.28 +val str = (*#1#*)
7.29 +"Script BiegelinieScript \
7.30 +\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
7.31 +\(rb_::bool list) (rm_::bool list) = \
7.32 +\ (let q___ = Take (M_b v_ = q__); \
7.33 +\ (M1__::bool) = ((Substitute [v_ = 0])) q___ \
7.34 +\ in True)";
7.35 +val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.36 +
7.37 +val str = (*#2#*)
7.38 +"Script BiegelinieScript \
7.39 +\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
7.40 +\(rb_::bool list) (rm_::bool list) = \
7.41 +\ (let q___ = Take (q_ v_ = q__); \
7.42 +\ (M1__::bool) = ((Substitute [v_ = 0]) @@ \
7.43 +\ (Substitute [M_b 0 = 0])) q___ \
7.44 +\ in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*)
7.45 +
7.46 +val str = (*#3#*)
7.47 +"Script BiegelinieScript \
7.48 +\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
7.49 +\(rb_::bool list) (rm_::bool list) = \
7.50 +\ (let q___ = Take (q_ v_ = q__); \
7.51 +\ (M1__::bool) = Substitute [v_ = 0] q___ ; \
7.52 +\ M1__ = Substitute [M_b 0 = 0] M1__ \
7.53 +\ in True)"
7.54 +;
7.55 +val str = (*#4#*)
7.56 +"Script BiegelinieScript \
7.57 +\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
7.58 +\(rb_::bool list) (rm_::bool list) = \
7.59 +\ (let q___ = Take (q_ v_ = q__); \
7.60 +\ (M1__::bool) = Substitute [v_ = 0] q___ ; \
7.61 +\ M1__ = Substitute [v_ = 1] q___ ; \
7.62 +\ M1__ = Substitute [v_ = 2] q___ ; \
7.63 +\ M1__ = Substitute [v_ = 3] q___ ; \
7.64 +\ M1__ = Substitute [M_b 0 = 0] M1__ \
7.65 +\ in True)"
7.66 +;
7.67 +val str = (*#5#*)
7.68 +"Script BiegelinieScript \
7.69 +\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
7.70 +\(rb_::bool list) (rm_::bool list) = \
7.71 +\ (let q___ = Take (M_b v_ = q__); \
7.72 +\ (M1__::bool) = Substitute [v_ = 0] q___ ; \
7.73 +\ M2__ = Take q___ ; \
7.74 +\ M2__ = Substitute [v_ = 2] q___ \
7.75 +\ in True)"
7.76 +;
7.77 +val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.78 +atomty sc';
7.79 +val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
7.80 +(*---------------------------------------------------------------------
7.81 +if sc = sc' then () else raise error"script.sml, doesnt find Substitute #1";
7.82 +---------------------------------------------------------------------*)
7.83 +
7.84 +val fmz = ["Traegerlaenge L",
7.85 + "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
7.86 + "Biegelinie y",
7.87 + "RandbedingungenBiegung [y 0 = 0, y L = 0]",
7.88 + "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
7.89 + "FunktionsVariable x"];
7.90 +val (dI',pI',mI') =
7.91 + ("Biegelinie.thy",["MomentBestimmte","Biegelinien"],
7.92 + ["IntegrierenUndKonstanteBestimmen"]);
7.93 +val p = e_pos'; val c = [];
7.94 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.95 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.96 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.97 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.98 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.99 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.100 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.101 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.102 +case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
7.103 + | _ => raise error "script.sml, doesnt find Substitute #2";
7.104 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
7.105 +(* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)
7.106 +(* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)
7.107 +
7.108 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
7.109 +(* *** generate1: not impl.for Empty_Tac_ !!!!!!!!!!(*#3#*)!!!!!!!!!!!*)
7.110 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
7.111 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
7.112 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
7.113 +(*---------------------------------------------------------------------*)
7.114 +case nxt of (_, End_Proof') => ()
7.115 + | _ => raise error "script.sml, doesnt find Substitute #3";
7.116 +(*---------------------------------------------------------------------*)
7.117 +(*the reason, that next_tac didnt find the 2nd Substitute, was that
7.118 + the Take inbetween was missing, and thus the 2nd Substitute was applied
7.119 + the last formula in ctree, and not to argument from script*)
7.120 +
7.121 +
7.122 +"----------- WN0509 Substitute 2nd part --------------------------";
7.123 +"----------- WN0509 Substitute 2nd part --------------------------";
7.124 +"----------- WN0509 Substitute 2nd part --------------------------";
7.125 +(*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
7.126 +val str = (*Substitute ; Substitute works*)
7.127 +"Script BiegelinieScript \
7.128 +\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
7.129 +\(rb_::bool list) (rm_::bool list) = "^
7.130 +(*begin after the 2nd integrate*)
7.131 +" (let M__ = Take (M_b v_ = q__); \
7.132 +\ e1__ = nth_ 1 rm_ ; \
7.133 +\ (x1__::real) = argument_in (lhs e1__); \
7.134 +\ (M1__::bool) = Substitute [v_ = x1__] M__; \
7.135 +\ M1__ = Substitute [e1__] M1__ \
7.136 +\ in True)"
7.137 +;
7.138 +(*---^^^-OK-----------------------------------------------------------------*)
7.139 +val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.140 +atomty sc';
7.141 +(*---vvv-NOT ok-------------------------------------------------------------*)
7.142 +val str = (*Substitute @@ Substitute does NOT work???*)
7.143 +"Script BiegelinieScript \
7.144 +\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
7.145 +\(rb_::bool list) (rm_::bool list) = "^
7.146 +(*begin after the 2nd integrate*)
7.147 +" (let M__ = Take (M_b v_ = q__); \
7.148 +\ e1__ = nth_ 1 rm_ ; \
7.149 +\ (x1__::real) = argument_in (lhs e1__); \
7.150 +\ (M1__::bool) = ((Substitute [v_ = x1__]) @@ \
7.151 +\ (Substitute [e1__])) M__ \
7.152 +\ in True)"
7.153 +;
7.154 +
7.155 +val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
7.156 +(*---------------------------------------------------------------------
7.157 +if sc = sc' then () else raise error"script.sml, doesnt find Substitute #1";
7.158 +---------------------------------------------------------------------*)
7.159 +val fmz = ["Traegerlaenge L",
7.160 + "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
7.161 + "Biegelinie y",
7.162 + "RandbedingungenBiegung [y 0 = 0, y L = 0]",
7.163 + "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
7.164 + "FunktionsVariable x"];
7.165 +val (dI',pI',mI') =
7.166 + ("Biegelinie.thy",["MomentBestimmte","Biegelinien"],
7.167 + ["IntegrierenUndKonstanteBestimmen"]);
7.168 +val p = e_pos'; val c = [];
7.169 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.170 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.171 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.172 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.173 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.174 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.175 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.176 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.177 +case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
7.178 + | _ => raise error "script.sml, doesnt find Substitute #2";
7.179 +trace_rewrite:=true;
7.180 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
7.181 +trace_rewrite:=false;
7.182 +(*Exception TYPE raised:
7.183 +Illegal type for constant "op =" :: "[real, bool] => bool"
7.184 +Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
7.185 +ListG.nth_ (1 + -1 + -1) []
7.186 +Exception-
7.187 + TYPE
7.188 + ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
7.189 + [],
7.190 + [Const ("Trueprop", "bool => prop") $
7.191 + (Const ("op =", "[RealDef.real, bool] => bool") $ ... $ ...)])
7.192 + raised
7.193 +... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
7.194 +ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
7.195 +thus corrected eval_argument_in OK*)
7.196 +
7.197 +val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
7.198 +val e1__ = str2term"nth_ 1 [M_b 0 = 0, M_b L = 0]";
7.199 +val e1__ = eval_listexpr_ Biegelinie.thy srls e1__; term2str e1__;
7.200 +if term2str e1__ = "M_b 0 = 0" then () else
7.201 +raise error"script.sml diff.beh. eval_listexpr_ nth_ 1 [...";
7.202 +
7.203 +(*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
7.204 +val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
7.205 +val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__;
7.206 +(*no rewrite*)
7.207 +calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__;
7.208 +val Some (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
7.209 +
7.210 +val l__ = str2term"lhs (M_b 0 = 0)";
7.211 +val l__ = eval_listexpr_ Biegelinie.thy srls l__; term2str l__;
7.212 +val Some (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;
7.213 +
7.214 +
7.215 +trace_rewrite:=true;
7.216 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
7.217 +trace_rewrite:=false;
7.218 +
7.219 +show_mets();
7.220 +
7.221 +"----------- fun sel_appl_atomic_tacs ----------------------------";
7.222 +"----------- fun sel_appl_atomic_tacs ----------------------------";
7.223 +"----------- fun sel_appl_atomic_tacs ----------------------------";
7.224 +states:=[];
7.225 +CalcTree
7.226 +[(["equality (x+1=2)", "solveFor x","solutions L"],
7.227 + ("Test.thy",
7.228 + ["sqroot-test","univariate","equation","test"],
7.229 + ["Test","squ-equ-test-subpbl1"]))];
7.230 +Iterator 1;
7.231 +moveActiveRoot 1;
7.232 +autoCalculate 1 CompleteCalcHead;
7.233 +autoCalculate 1 (Step 1);
7.234 +autoCalculate 1 (Step 1);
7.235 +val ((pt, (p, p_)), _) = get_calc 1; show_pt pt;
7.236 +show_pt pt;
7.237 +if sel_appl_atomic_tacs pt (p,p_) =
7.238 + [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
7.239 + Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
7.240 + Calculate "op *"] then ()
7.241 +else raise error "script.sml fun sel_appl_atomic_tacs diff.behav.";