1.1 --- a/test/Tools/isac/Interpret/script.sml Thu Jul 21 12:01:56 2011 +0200
1.2 +++ b/test/Tools/isac/Interpret/script.sml Thu Jul 21 16:57:21 2011 +0200
1.3 @@ -15,7 +15,6 @@
1.4 "-----------------------------------------------------------------";
1.5 "-----------------------------------------------------------------";
1.6
1.7 -(*========== inhibit exn 110503 ================================================
1.8
1.9 "----------- WN0509 why does next_tac doesnt find Substitute -----";
1.10 "----------- WN0509 why does next_tac doesnt find Substitute -----";
1.11 @@ -29,7 +28,9 @@
1.12 \ (let q___ = Take (M_b v_v = q__); \
1.13 \ (M1__::bool) = ((Substitute [v_ = 0])) q___ \
1.14 \ in True)";
1.15 +(*========== inhibit exn 110721 ================================================
1.16 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.17 +(========= inhibit exn 110721 ================================================*)
1.18
1.19 val str = (*#2#*)
1.20 "Script BiegelinieScript \
1.21 @@ -71,8 +72,12 @@
1.22 \ M2__ = Substitute [v_ = 2] q___ \
1.23 \ in True)"
1.24 ;
1.25 +
1.26 +(*========== inhibit exn 110721 ================================================
1.27 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.28 atomty sc';
1.29 +========== inhibit exn 110721 ================================================*)
1.30 +
1.31 val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
1.32 (*---------------------------------------------------------------------
1.33 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
1.34 @@ -84,10 +89,13 @@
1.35 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
1.36 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
1.37 "FunktionsVariable x"];
1.38 +
1.39 val (dI',pI',mI') =
1.40 ("Biegelinie",["MomentBestimmte","Biegelinien"],
1.41 ["IntegrierenUndKonstanteBestimmen"]);
1.42 +
1.43 val p = e_pos'; val c = [];
1.44 +
1.45 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.46 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.47 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.48 @@ -96,8 +104,10 @@
1.49 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.50 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.51 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.52 +
1.53 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
1.54 | _ => error "script.sml, doesnt find Substitute #2";
1.55 +(*========== inhibit exn 110721 ================================================
1.56 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.57 (* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)
1.58 (* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)
1.59 @@ -108,12 +118,15 @@
1.60 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.61 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.62 (*---------------------------------------------------------------------*)
1.63 +
1.64 case nxt of (_, End_Proof') => ()
1.65 | _ => error "script.sml, doesnt find Substitute #3";
1.66 (*---------------------------------------------------------------------*)
1.67 (*the reason, that next_tac didnt find the 2nd Substitute, was that
1.68 the Take inbetween was missing, and thus the 2nd Substitute was applied
1.69 the last formula in ctree, and not to argument from script*)
1.70 +========== inhibit exn 110721 ================================================*)
1.71 +
1.72
1.73
1.74 "----------- WN0509 Substitute 2nd part --------------------------";
1.75 @@ -132,10 +145,13 @@
1.76 \ M1__ = Substitute [e1__] M1__ \
1.77 \ in True)"
1.78 ;
1.79 +(*========== inhibit exn 110721 ================================================
1.80 (*---^^^-OK-----------------------------------------------------------------*)
1.81 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.82 atomty sc';
1.83 (*---vvv-NOT ok-------------------------------------------------------------*)
1.84 +========== inhibit exn 110721 ================================================*)
1.85 +
1.86 val str = (*Substitute @@ Substitute does NOT work???*)
1.87 "Script BiegelinieScript \
1.88 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
1.89 @@ -173,6 +189,8 @@
1.90 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.91 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
1.92 | _ => error "script.sml, doesnt find Substitute #2";
1.93 +
1.94 +(*========== inhibit exn 110721 ================================================
1.95 trace_rewrite:=true;
1.96 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
1.97 trace_rewrite:=false;
1.98 @@ -190,12 +208,16 @@
1.99 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
1.100 ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
1.101 thus corrected eval_argument_in OK*)
1.102 +========== inhibit exn 110721 ================================================*)
1.103
1.104 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
1.105 -val e1__ = str2term"nth_ 1 [M_b 0 = 0, M_b L = 0]";
1.106 +val e1__ = str2term "nth_nth 1 [M_b 0 = 0, M_b L = 0]";
1.107 +(*========== inhibit exn 110721 ================================================
1.108 val e1__ = eval_listexpr_ Biegelinie.thy srls e1__; term2str e1__;
1.109 +
1.110 if term2str e1__ = "M_b 0 = 0" then () else
1.111 -error"script.sml diff.beh. eval_listexpr_ nth_ 1 [...";
1.112 +error"script.sml diff.beh. eval_listexpr_ nth_nth 1 [...";
1.113 +========== inhibit exn 110721 ================================================*)
1.114
1.115 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
1.116 val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
1.117 @@ -205,6 +227,7 @@
1.118 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
1.119
1.120 val l__ = str2term"lhs (M_b 0 = 0)";
1.121 +(*========== inhibit exn 110721 ================================================
1.122 val l__ = eval_listexpr_ Biegelinie.thy srls l__; term2str l__;
1.123 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;
1.124
1.125 @@ -212,12 +235,14 @@
1.126 trace_rewrite:=true;
1.127 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
1.128 trace_rewrite:=false;
1.129 +========== inhibit exn 110721 ================================================*)
1.130
1.131 show_mets();
1.132
1.133 "----------- fun sel_appl_atomic_tacs ----------------------------";
1.134 "----------- fun sel_appl_atomic_tacs ----------------------------";
1.135 "----------- fun sel_appl_atomic_tacs ----------------------------";
1.136 +
1.137 states:=[];
1.138 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.139 ("Test", ["sqroot-test","univariate","equation","test"],
1.140 @@ -229,11 +254,22 @@
1.141 autoCalculate 1 (Step 1);
1.142 val ((pt, p), _) = get_calc 1; show_pt pt;
1.143 val appltacs = sel_appl_atomic_tacs pt p;
1.144 +
1.145 +(*
1.146 +(*These SHOULD be the same*)
1.147 + print_depth(999);
1.148 + appltacs;
1.149 + [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
1.150 + Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
1.151 + Calculate "times"];*)
1.152 +
1.153 +(*========== inhibit exn 110721 ================================================
1.154 if appltacs =
1.155 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
1.156 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
1.157 Calculate "times"] then ()
1.158 else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
1.159 +========== inhibit exn 110721 ================================================*)
1.160
1.161 trace_script := true;
1.162 trace_script := false;
1.163 @@ -241,11 +277,13 @@
1.164 val ((pt, p), _) = get_calc 1; show_pt pt;
1.165 val appltacs = sel_appl_atomic_tacs pt p;
1.166
1.167 +(*========== inhibit exn 110721 ================================================
1.168 "----- WN080102 these vvv do not work, because locatetac starts the search\
1.169 \1 stac too low";
1.170 +(* ERROR: assy: call by ([3], Pbl) *)
1.171 applyTactic 1 p (hd appltacs);
1.172 autoCalculate 1 CompleteCalc;
1.173 -============ inhibit exn 110503 ==============================================*)
1.174 +============ inhibit exn 110721 ==============================================*)
1.175
1.176 "----------- fun init_form, fun get_stac -------------------------";
1.177 "----------- fun init_form, fun get_stac -------------------------";