1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/isac/smltest/ME/script.sml Wed Jul 21 13:53:39 2010 +0200
1.3 @@ -0,0 +1,250 @@
1.4 +(* tests for ME/script.sml
1.5 + TODO.WN0509 collect typical tests from systest here !!!!!
1.6 + author: Walther Neuper 050908
1.7 + (c) copyright due to lincense terms.
1.8 +
1.9 +use"../smltest/ME/script.sml";
1.10 +use"script.sml";
1.11 +*)
1.12 +"-----------------------------------------------------------------";
1.13 +"table of contents -----------------------------------------------";
1.14 +"-----------------------------------------------------------------";
1.15 +"----------- WN0509 why does next_tac doesnt find Substitute -----";
1.16 +"----------- WN0509 Substitute 2nd part --------------------------";
1.17 +"----------- fun sel_appl_atomic_tacs ----------------------------";
1.18 +"-----------------------------------------------------------------";
1.19 +"-----------------------------------------------------------------";
1.20 +"-----------------------------------------------------------------";
1.21 +
1.22 +
1.23 +"----------- WN0509 why does next_tac doesnt find Substitute -----";
1.24 +"----------- WN0509 why does next_tac doesnt find Substitute -----";
1.25 +"----------- WN0509 why does next_tac doesnt find Substitute -----";
1.26 +
1.27 +(*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
1.28 +val str = (*#1#*)
1.29 +"Script BiegelinieScript \
1.30 +\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
1.31 +\(rb_::bool list) (rm_::bool list) = \
1.32 +\ (let q___ = Take (M_b v_ = q__); \
1.33 +\ (M1__::bool) = ((Substitute [v_ = 0])) q___ \
1.34 +\ in True)";
1.35 +val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.36 +
1.37 +val str = (*#2#*)
1.38 +"Script BiegelinieScript \
1.39 +\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
1.40 +\(rb_::bool list) (rm_::bool list) = \
1.41 +\ (let q___ = Take (q_ v_ = q__); \
1.42 +\ (M1__::bool) = ((Substitute [v_ = 0]) @@ \
1.43 +\ (Substitute [M_b 0 = 0])) q___ \
1.44 +\ in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*)
1.45 +
1.46 +val str = (*#3#*)
1.47 +"Script BiegelinieScript \
1.48 +\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
1.49 +\(rb_::bool list) (rm_::bool list) = \
1.50 +\ (let q___ = Take (q_ v_ = q__); \
1.51 +\ (M1__::bool) = Substitute [v_ = 0] q___ ; \
1.52 +\ M1__ = Substitute [M_b 0 = 0] M1__ \
1.53 +\ in True)"
1.54 +;
1.55 +val str = (*#4#*)
1.56 +"Script BiegelinieScript \
1.57 +\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
1.58 +\(rb_::bool list) (rm_::bool list) = \
1.59 +\ (let q___ = Take (q_ v_ = q__); \
1.60 +\ (M1__::bool) = Substitute [v_ = 0] q___ ; \
1.61 +\ M1__ = Substitute [v_ = 1] q___ ; \
1.62 +\ M1__ = Substitute [v_ = 2] q___ ; \
1.63 +\ M1__ = Substitute [v_ = 3] q___ ; \
1.64 +\ M1__ = Substitute [M_b 0 = 0] M1__ \
1.65 +\ in True)"
1.66 +;
1.67 +val str = (*#5#*)
1.68 +"Script BiegelinieScript \
1.69 +\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
1.70 +\(rb_::bool list) (rm_::bool list) = \
1.71 +\ (let q___ = Take (M_b v_ = q__); \
1.72 +\ (M1__::bool) = Substitute [v_ = 0] q___ ; \
1.73 +\ M2__ = Take q___ ; \
1.74 +\ M2__ = Substitute [v_ = 2] q___ \
1.75 +\ in True)"
1.76 +;
1.77 +val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.78 +atomty sc';
1.79 +val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
1.80 +(*---------------------------------------------------------------------
1.81 +if sc = sc' then () else raise error"script.sml, doesnt find Substitute #1";
1.82 +---------------------------------------------------------------------*)
1.83 +
1.84 +val fmz = ["Traegerlaenge L",
1.85 + "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
1.86 + "Biegelinie y",
1.87 + "RandbedingungenBiegung [y 0 = 0, y L = 0]",
1.88 + "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
1.89 + "FunktionsVariable x"];
1.90 +val (dI',pI',mI') =
1.91 + ("Biegelinie.thy",["MomentBestimmte","Biegelinien"],
1.92 + ["IntegrierenUndKonstanteBestimmen"]);
1.93 +val p = e_pos'; val c = [];
1.94 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.95 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.96 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.97 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.98 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.99 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.100 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.101 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.102 +case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
1.103 + | _ => raise error "script.sml, doesnt find Substitute #2";
1.104 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.105 +(* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)
1.106 +(* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)
1.107 +
1.108 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.109 +(* *** generate1: not impl.for Empty_Tac_ !!!!!!!!!!(*#3#*)!!!!!!!!!!!*)
1.110 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.111 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.112 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.113 +(*---------------------------------------------------------------------*)
1.114 +case nxt of (_, End_Proof') => ()
1.115 + | _ => raise error "script.sml, doesnt find Substitute #3";
1.116 +(*---------------------------------------------------------------------*)
1.117 +(*the reason, that next_tac didnt find the 2nd Substitute, was that
1.118 + the Take inbetween was missing, and thus the 2nd Substitute was applied
1.119 + the last formula in ctree, and not to argument from script*)
1.120 +
1.121 +
1.122 +"----------- WN0509 Substitute 2nd part --------------------------";
1.123 +"----------- WN0509 Substitute 2nd part --------------------------";
1.124 +"----------- WN0509 Substitute 2nd part --------------------------";
1.125 +(*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
1.126 +val str = (*Substitute ; Substitute works*)
1.127 +"Script BiegelinieScript \
1.128 +\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
1.129 +\(rb_::bool list) (rm_::bool list) = "^
1.130 +(*begin after the 2nd integrate*)
1.131 +" (let M__ = Take (M_b v_ = q__); \
1.132 +\ e1__ = nth_ 1 rm_ ; \
1.133 +\ (x1__::real) = argument_in (lhs e1__); \
1.134 +\ (M1__::bool) = Substitute [v_ = x1__] M__; \
1.135 +\ M1__ = Substitute [e1__] M1__ \
1.136 +\ in True)"
1.137 +;
1.138 +(*---^^^-OK-----------------------------------------------------------------*)
1.139 +val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.140 +atomty sc';
1.141 +(*---vvv-NOT ok-------------------------------------------------------------*)
1.142 +val str = (*Substitute @@ Substitute does NOT work???*)
1.143 +"Script BiegelinieScript \
1.144 +\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
1.145 +\(rb_::bool list) (rm_::bool list) = "^
1.146 +(*begin after the 2nd integrate*)
1.147 +" (let M__ = Take (M_b v_ = q__); \
1.148 +\ e1__ = nth_ 1 rm_ ; \
1.149 +\ (x1__::real) = argument_in (lhs e1__); \
1.150 +\ (M1__::bool) = ((Substitute [v_ = x1__]) @@ \
1.151 +\ (Substitute [e1__])) M__ \
1.152 +\ in True)"
1.153 +;
1.154 +
1.155 +val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
1.156 +(*---------------------------------------------------------------------
1.157 +if sc = sc' then () else raise error"script.sml, doesnt find Substitute #1";
1.158 +---------------------------------------------------------------------*)
1.159 +val fmz = ["Traegerlaenge L",
1.160 + "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
1.161 + "Biegelinie y",
1.162 + "RandbedingungenBiegung [y 0 = 0, y L = 0]",
1.163 + "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
1.164 + "FunktionsVariable x"];
1.165 +val (dI',pI',mI') =
1.166 + ("Biegelinie.thy",["MomentBestimmte","Biegelinien"],
1.167 + ["IntegrierenUndKonstanteBestimmen"]);
1.168 +val p = e_pos'; val c = [];
1.169 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.170 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.171 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.172 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.173 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.174 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.175 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.176 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.177 +case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
1.178 + | _ => raise error "script.sml, doesnt find Substitute #2";
1.179 +trace_rewrite:=true;
1.180 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
1.181 +trace_rewrite:=false;
1.182 +(*Exception TYPE raised:
1.183 +Illegal type for constant "op =" :: "[real, bool] => bool"
1.184 +Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
1.185 +ListG.nth_ (1 + -1 + -1) []
1.186 +Exception-
1.187 + TYPE
1.188 + ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
1.189 + [],
1.190 + [Const ("Trueprop", "bool => prop") $
1.191 + (Const ("op =", "[RealDef.real, bool] => bool") $ ... $ ...)])
1.192 + raised
1.193 +... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
1.194 +ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
1.195 +thus corrected eval_argument_in OK*)
1.196 +
1.197 +val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
1.198 +val e1__ = str2term"nth_ 1 [M_b 0 = 0, M_b L = 0]";
1.199 +val e1__ = eval_listexpr_ Biegelinie.thy srls e1__; term2str e1__;
1.200 +if term2str e1__ = "M_b 0 = 0" then () else
1.201 +raise error"script.sml diff.beh. eval_listexpr_ nth_ 1 [...";
1.202 +
1.203 +(*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
1.204 +val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
1.205 +val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__;
1.206 +(*no rewrite*)
1.207 +calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__;
1.208 +val Some (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
1.209 +
1.210 +val l__ = str2term"lhs (M_b 0 = 0)";
1.211 +val l__ = eval_listexpr_ Biegelinie.thy srls l__; term2str l__;
1.212 +val Some (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;
1.213 +
1.214 +
1.215 +trace_rewrite:=true;
1.216 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
1.217 +trace_rewrite:=false;
1.218 +
1.219 +show_mets();
1.220 +
1.221 +"----------- fun sel_appl_atomic_tacs ----------------------------";
1.222 +"----------- fun sel_appl_atomic_tacs ----------------------------";
1.223 +"----------- fun sel_appl_atomic_tacs ----------------------------";
1.224 +states:=[];
1.225 +CalcTree
1.226 +[(["equality (x+1=2)", "solveFor x","solutions L"],
1.227 + ("Test.thy",
1.228 + ["sqroot-test","univariate","equation","test"],
1.229 + ["Test","squ-equ-test-subpbl1"]))];
1.230 +Iterator 1;
1.231 +moveActiveRoot 1;
1.232 +autoCalculate 1 CompleteCalcHead;
1.233 +autoCalculate 1 (Step 1);
1.234 +autoCalculate 1 (Step 1);
1.235 +val ((pt, p), _) = get_calc 1; show_pt pt;
1.236 +val appltacs = sel_appl_atomic_tacs pt p;
1.237 +if appltacs =
1.238 + [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
1.239 + Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
1.240 + Calculate "times"] then ()
1.241 +else raise error "script.sml fun sel_appl_atomic_tacs diff.behav.";
1.242 +
1.243 +trace_script := true;
1.244 +trace_script := false;
1.245 +applyTactic 1 p (hd appltacs);
1.246 +val ((pt, p), _) = get_calc 1; show_pt pt;
1.247 +val appltacs = sel_appl_atomic_tacs pt p;
1.248 +
1.249 +"----- WN080102 these vvv do not work, because locatetac starts the search\
1.250 + \1 stac too low";
1.251 +applyTactic 1 p (hd appltacs);
1.252 +autoCalculate 1 CompleteCalc;
1.253 +