1.1 --- a/src/Tools/isac/Frontend/interface.sml Thu Jul 21 17:04:04 2011 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Fri Jul 22 15:57:22 2011 +0200
1.3 @@ -157,10 +157,11 @@
1.4 *)
1.5 fun applyTactic (cI:calcID) ip tac =
1.6 let val ((pt, _), _) = get_calc cI
1.7 - val p = get_pos cI 1
1.8 - in case locatetac tac (pt, ip) of
1.9 -(* val ("ok", (tacis, c, (pt',p'))) = locatetac tac (pt, ip);
1.10 - *)
1.11 + val p = get_pos cI 1
1.12 + in
1.13 + case locatetac tac (pt, ip)
1.14 + of
1.15 +(* val ("ok", (tacis, c, (pt',p'))) = locatetac tac (pt, ip);*)
1.16 ("ok", (_, c, ptp as (_,p'))) =>
1.17 (upd_calc cI (ptp, []); upd_ipos cI 1 p';
1.18 autocalculateOK2xml cI p (if null c then p'
1.19 @@ -174,7 +175,6 @@
1.20 autocalculateOK2xml cI p (if null c then p'
1.21 else last_elem c) p')
1.22
1.23 -
1.24 | (str,_) => autocalculateERROR2xml cI "failure"
1.25 end;
1.26
2.1 --- a/test/Tools/isac/Interpret/script.sml Thu Jul 21 17:04:04 2011 +0200
2.2 +++ b/test/Tools/isac/Interpret/script.sml Fri Jul 22 15:57:22 2011 +0200
2.3 @@ -22,55 +22,55 @@
2.4
2.5 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
2.6 val str = (*#1#*)
2.7 -"Script BiegelinieScript \
2.8 -\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
2.9 -\(rb_::bool list) (rm_::bool list) = \
2.10 -\ (let q___ = Take (M_b v_v = q__); \
2.11 -\ (M1__::bool) = ((Substitute [v_ = 0])) q___ \
2.12 -\ in True)";
2.13 +"Script BiegelinieScript " ^
2.14 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
2.15 +"(rb_rb::bool list) (rm_rm::bool list) = " ^
2.16 +" (let q___q = Take (M_b v_v = q__q); " ^
2.17 +" (M1__M1::bool) = ((Substitute [v_v = 0])) q___q " ^
2.18 +" in True)";
2.19 +
2.20 (*========== inhibit exn 110721 ================================================
2.21 +(* ERROR: parse thy Can't unify theory to domID * rls*)
2.22 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.23 -(========= inhibit exn 110721 ================================================*)
2.24 +========= inhibit exn 110721 ================================================*)
2.25
2.26 val str = (*#2#*)
2.27 -"Script BiegelinieScript \
2.28 -\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
2.29 -\(rb_::bool list) (rm_::bool list) = \
2.30 -\ (let q___ = Take (q_ v_v = q__); \
2.31 -\ (M1__::bool) = ((Substitute [v_ = 0]) @@ \
2.32 -\ (Substitute [M_b 0 = 0])) q___ \
2.33 -\ in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*)
2.34 +"Script BiegelinieScript " ^
2.35 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
2.36 +"(rb_rb::bool list) (rm_rm::bool list) = " ^
2.37 +" (M1__M1::bool) = ((Substitute [v_v = 0]) @@ " ^
2.38 +" in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*)
2.39
2.40 val str = (*#3#*)
2.41 -"Script BiegelinieScript \
2.42 -\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
2.43 -\(rb_::bool list) (rm_::bool list) = \
2.44 -\ (let q___ = Take (q_ v_v = q__); \
2.45 -\ (M1__::bool) = Substitute [v_ = 0] q___ ; \
2.46 -\ M1__ = Substitute [M_b 0 = 0] M1__ \
2.47 -\ in True)"
2.48 +"Script BiegelinieScript " ^
2.49 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
2.50 +"(rb_rb::bool list) (rm_rm::bool list) = " ^
2.51 +" (let q___q = Take (q_q v_v = q__q); " ^
2.52 +" (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
2.53 +" M1__m1 = Substitute [M_b 0 = 0] M1__M1 " ^
2.54 +" in True)"
2.55 ;
2.56 val str = (*#4#*)
2.57 -"Script BiegelinieScript \
2.58 -\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
2.59 -\(rb_::bool list) (rm_::bool list) = \
2.60 -\ (let q___ = Take (q_ v_v = q__); \
2.61 -\ (M1__::bool) = Substitute [v_ = 0] q___ ; \
2.62 -\ M1__ = Substitute [v_ = 1] q___ ; \
2.63 -\ M1__ = Substitute [v_ = 2] q___ ; \
2.64 -\ M1__ = Substitute [v_ = 3] q___ ; \
2.65 -\ M1__ = Substitute [M_b 0 = 0] M1__ \
2.66 -\ in True)"
2.67 +"Script BiegelinieScript " ^
2.68 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
2.69 +"(rb_rb::bool list) (rm_rm::bool list) = " ^
2.70 +" (let q___q = Take (q_q v_v = q__q); " ^
2.71 +" (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
2.72 +" M1__M1 = Substitute [v_v = 1] q___q ; " ^
2.73 +" M1__M1 = Substitute [v_v = 2] q___q ; " ^
2.74 +" M1__M1 = Substitute [v_v = 3] q___q ; " ^
2.75 +" M1__M1 = Substitute [M_b 0 = 0] M1__M1 " ^
2.76 +" in True)"
2.77 ;
2.78 val str = (*#5#*)
2.79 -"Script BiegelinieScript \
2.80 -\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
2.81 -\(rb_::bool list) (rm_::bool list) = \
2.82 -\ (let q___ = Take (M_b v_v = q__); \
2.83 -\ (M1__::bool) = Substitute [v_ = 0] q___ ; \
2.84 -\ M2__ = Take q___ ; \
2.85 -\ M2__ = Substitute [v_ = 2] q___ \
2.86 -\ in True)"
2.87 +"Script BiegelinieScript " ^
2.88 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
2.89 +"(rb_rb::bool list) (rm_rm::bool list) = " ^
2.90 +" (let q___q = Take (M_b v_v = q__q); " ^
2.91 +" (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
2.92 +" M2__M2 = Take q___q ; " ^
2.93 +" M2__M2 = Substitute [v_v = 2] q___q " ^
2.94 +" in True)"
2.95 ;
2.96
2.97 (*========== inhibit exn 110721 ================================================
2.98 @@ -78,7 +78,7 @@
2.99 atomty sc';
2.100 ========== inhibit exn 110721 ================================================*)
2.101
2.102 -val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
2.103 +val {scr = Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
2.104 (*---------------------------------------------------------------------
2.105 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
2.106 ---------------------------------------------------------------------*)
2.107 @@ -97,18 +97,32 @@
2.108 val p = e_pos'; val c = [];
2.109
2.110 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.111 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.112 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.113 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.114 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.115 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.116 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.117 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.118 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.119 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.120 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.121 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.122 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.123
2.124 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
2.125 | _ => error "script.sml, doesnt find Substitute #2";
2.126 -(*========== inhibit exn 110721 ================================================
2.127 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.128 +
2.129 +(*========== inhibit exn AK110721 ================================================
2.130 +
2.131 +(* AK110722 f2str f is NOT working anywhere - deprecated?????*)
2.132 +
2.133 +(*(* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.134 + (* ERROR: exception PTREE "get_obj: pos = [0] does not exist" raised
2.135 + (line 908 of "src/Tools/isac/Interpret/ctree.sml")*)*)
2.136 +(*f2str f;
2.137 + (* ERROR: exception Match raised (line 416 of "src/Tools/isac/Interpret/mathengine.sml")*)*)
2.138 +(* "~~~~~ fun f2str, args:"; val ((Form' (FormKF (_, _, _, _, cterm')))) = (f);
2.139 + (* ERROR: exception Bind raised *)*)
2.140 +
2.141 + f;
2.142 + f2str;*)
2.143 +
2.144 (* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)
2.145 (* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)
2.146
2.147 @@ -125,8 +139,7 @@
2.148 (*the reason, that next_tac didnt find the 2nd Substitute, was that
2.149 the Take inbetween was missing, and thus the 2nd Substitute was applied
2.150 the last formula in ctree, and not to argument from script*)
2.151 -========== inhibit exn 110721 ================================================*)
2.152 -
2.153 +========== inhibit exn AK110721 ================================================*)
2.154
2.155
2.156 "----------- WN0509 Substitute 2nd part --------------------------";
2.157 @@ -134,16 +147,16 @@
2.158 "----------- WN0509 Substitute 2nd part --------------------------";
2.159 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
2.160 val str = (*Substitute ; Substitute works*)
2.161 -"Script BiegelinieScript \
2.162 -\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
2.163 -\(rb_::bool list) (rm_::bool list) = "^
2.164 +"Script BiegelinieScript " ^
2.165 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
2.166 +"(rb_rb::bool list) (rm_rm::bool list) = "^
2.167 (*begin after the 2nd integrate*)
2.168 -" (let M__ = Take (M_b v_v = q__); \
2.169 -\ e1__ = nth_ 1 rm_ ; \
2.170 -\ (x1__::real) = argument_in (lhs e1__); \
2.171 -\ (M1__::bool) = Substitute [v_ = x1__] M__; \
2.172 -\ M1__ = Substitute [e1__] M1__ \
2.173 -\ in True)"
2.174 +" (let M__M = Take (M_b v_v = q__q); " ^
2.175 +" e1__e1 = nth_nth 1 rm_rm ; " ^
2.176 +" (x1__x1::real) = argument_in (lhs e1__e1); " ^
2.177 +" (M1__M1::bool) = Substitute [v_v = x1__x1] M__M; " ^
2.178 +" M1__M1 = Substitute [e1__e1] M1__M1 " ^
2.179 +" in True)"
2.180 ;
2.181 (*========== inhibit exn 110721 ================================================
2.182 (*---^^^-OK-----------------------------------------------------------------*)
2.183 @@ -153,21 +166,21 @@
2.184 ========== inhibit exn 110721 ================================================*)
2.185
2.186 val str = (*Substitute @@ Substitute does NOT work???*)
2.187 -"Script BiegelinieScript \
2.188 -\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
2.189 -\(rb_::bool list) (rm_::bool list) = "^
2.190 +"Script BiegelinieScript " ^
2.191 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
2.192 +"(rb_rb::bool list) (rm_rm::bool list) = "^
2.193 (*begin after the 2nd integrate*)
2.194 -" (let M__ = Take (M_b v_v = q__); \
2.195 -\ e1__ = nth_ 1 rm_ ; \
2.196 -\ (x1__::real) = argument_in (lhs e1__); \
2.197 -\ (M1__::bool) = ((Substitute [v_ = x1__]) @@ \
2.198 -\ (Substitute [e1__])) M__ \
2.199 -\ in True)"
2.200 +" (let M__M = Take (M_b v_v = q__q); " ^
2.201 +" e1__e1 = nth_nth 1 rm_rm ; " ^
2.202 +" (x1__x1::real) = argument_in (lhs e1__e1); " ^
2.203 +" (M1__M1::bool) = ((Substitute [v_v = x1__x1]) @@ " ^
2.204 +" (Substitute [e1__e1])) M__M " ^
2.205 +" in True)"
2.206 ;
2.207
2.208 -val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
2.209 +val {scr = Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
2.210 (*---------------------------------------------------------------------
2.211 -if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
2.212 +if sc = sc' then () else error "script.sml, doesnt find Substitute #1";
2.213 ---------------------------------------------------------------------*)
2.214 val fmz = ["Traegerlaenge L",
2.215 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
2.216 @@ -180,60 +193,66 @@
2.217 ["IntegrierenUndKonstanteBestimmen"]);
2.218 val p = e_pos'; val c = [];
2.219 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.220 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.221 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.222 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.223 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.224 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.225 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.226 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.227 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.228 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.229 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.230 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.231 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.232 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
2.233 | _ => error "script.sml, doesnt find Substitute #2";
2.234
2.235 -(*========== inhibit exn 110721 ================================================
2.236 +(*========== inhibit exn AK110721 ================================================
2.237 +(* ERROR: caused by f2str f *)
2.238 trace_rewrite:=true;
2.239 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
2.240 trace_rewrite:=false;
2.241 -(*Exception TYPE raised:
2.242 -Illegal type for constant "HOL.eq" :: "[real, bool] => bool"
2.243 -Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
2.244 -ListG.nth_ (1 + -1 + -1) []
2.245 -Exception-
2.246 - TYPE
2.247 - ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
2.248 - [],
2.249 - [Const ("HOL.Trueprop", "bool => prop") $
2.250 - (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])
2.251 - raised
2.252 -... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
2.253 -ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
2.254 -thus corrected eval_argument_in OK*)
2.255 -========== inhibit exn 110721 ================================================*)
2.256 + (*Exception TYPE raised:
2.257 + Illegal type for constant "HOL.eq" :: "[real, bool] => bool"
2.258 + Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
2.259 + ListG.nth_ (1 + -1 + -1) []
2.260 + Exception-
2.261 + TYPE
2.262 + ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
2.263 + [],
2.264 + [Const ("HOL.Trueprop", "bool => prop") $
2.265 + (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])
2.266 + raised
2.267 + ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
2.268 + ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
2.269 + thus corrected eval_argument_in OK*)
2.270 +========== inhibit exn AK110721 ================================================*)
2.271
2.272 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
2.273 -val e1__ = str2term "nth_nth 1 [M_b 0 = 0, M_b L = 0]";
2.274 +val e1__e1 = str2term "nth_nth 1 [M_b 0 = 0, M_b L = 0]";
2.275 +val e1__e1 = eval_listexpr_ @{theory Biegelinie} srls e1__e1; term2str e1__e1;
2.276 +
2.277 (*========== inhibit exn 110721 ================================================
2.278 -val e1__ = eval_listexpr_ Biegelinie.thy srls e1__; term2str e1__;
2.279 +(*AK110722
2.280 + TRIAL: Should be the same
2.281 + term2str e1__e1 = "M_b 0 = 0";
2.282 + term2str e1__e1;*)
2.283
2.284 -if term2str e1__ = "M_b 0 = 0" then () else
2.285 -error"script.sml diff.beh. eval_listexpr_ nth_nth 1 [...";
2.286 +if term2str e1__e1 = "M_b 0 = 0"
2.287 + then ()
2.288 + else error"script.sml diff.beh. eval_listexpr_ nth_nth 1 [...";
2.289 ========== inhibit exn 110721 ================================================*)
2.290
2.291 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
2.292 -val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
2.293 -val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__;
2.294 -(*no rewrite*)
2.295 -calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__;
2.296 -val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
2.297 + val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
2.298 + val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__;
2.299 + (*no rewrite*)
2.300 + calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__;
2.301 + val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
2.302
2.303 -val l__ = str2term"lhs (M_b 0 = 0)";
2.304 +val l__l = str2term "lhs (M_b 0 = 0)";
2.305 +(*AK110722 eval_listexpr_ is prob. without _ ????*)
2.306 +val l__l = eval_listexpr_ @{theory Biegelinie} srls l__l; term2str l__l;
2.307 +val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term "lhs (M_b 0 = 0)") 0;
2.308 (*========== inhibit exn 110721 ================================================
2.309 -val l__ = eval_listexpr_ Biegelinie.thy srls l__; term2str l__;
2.310 -val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;
2.311 -
2.312 -
2.313 trace_rewrite:=true;
2.314 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
2.315 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f (*------------------------*);
2.316 trace_rewrite:=false;
2.317 ========== inhibit exn 110721 ================================================*)
2.318
2.319 @@ -255,21 +274,20 @@
2.320 val ((pt, p), _) = get_calc 1; show_pt pt;
2.321 val appltacs = sel_appl_atomic_tacs pt p;
2.322
2.323 -(*
2.324 -(*These SHOULD be the same*)
2.325 +(*========== inhibit exn AK110721 ================================================
2.326 +(*(*These SHOULD be the same*)
2.327 print_depth(999);
2.328 appltacs;
2.329 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
2.330 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
2.331 - Calculate "times"];*)
2.332 + Calculate "TIMES"];*)
2.333
2.334 -(*========== inhibit exn 110721 ================================================
2.335 if appltacs =
2.336 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
2.337 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
2.338 - Calculate "times"] then ()
2.339 + Calculate "TIMES"] then ()
2.340 else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
2.341 -========== inhibit exn 110721 ================================================*)
2.342 +========== inhibit exn AK110721 ================================================*)
2.343
2.344 trace_script := true;
2.345 trace_script := false;
2.346 @@ -277,13 +295,58 @@
2.347 val ((pt, p), _) = get_calc 1; show_pt pt;
2.348 val appltacs = sel_appl_atomic_tacs pt p;
2.349
2.350 -(*========== inhibit exn 110721 ================================================
2.351 -"----- WN080102 these vvv do not work, because locatetac starts the search\
2.352 - \1 stac too low";
2.353 -(* ERROR: assy: call by ([3], Pbl) *)
2.354 +(*(* AK110722 Debugging start*)
2.355 +(*applyTactic 1 p (hd appltacs); WAS assy: call by ([3], Pbl)*)
2.356 +"~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs));
2.357 +val ((pt, _), _) = get_calc cI;
2.358 +val p = get_pos cI 1;
2.359 +
2.360 +locatetac;
2.361 +locatetac tac;
2.362 +locatetac tac;
2.363 +
2.364 +(*locatetac tac (pt, ip); (*WAS assy: call by ([3], Pbl)*)*)
2.365 +"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
2.366 +val (mI,m) = mk_tac'_ tac;
2.367 +
2.368 +applicable_in p pt m ; (*Appl*)
2.369 +
2.370 +member op = specsteps mI; (*false*)
2.371 +
2.372 +(*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
2.373 +loc_solve_; (*without _ ??? result is -> lOc writing error ???*)
2.374 +(*val it = fn: string * tac_ -> ptree * (pos * pos_) -> lOc_*)
2.375 +(mI,m); (*string * tac*)
2.376 +ptp (*ptree * pos'*);
2.377 +
2.378 +"~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = ((mI,m), ptp);
2.379 +(*val (msg, cs') = solve m (pt, pos);
2.380 +(*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
2.381 +
2.382 +m;
2.383 +(pt, pos);
2.384 +
2.385 +"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
2.386 +(*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*)
2.387 +
2.388 +e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
2.389 +val ctxt = get_ctxt pt po;
2.390 +
2.391 +(*generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) m (e_istate, ctxt) (p,p_) pt;
2.392 +(*Argument: m : tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
2.393 +(assoc_thy (get_obj g_domID pt (par_pblobj pt p)));
2.394 +assoc_thy;
2.395 +
2.396 +(*not finished - error continues in fun generate1*)
2.397 +(* AK110722 Debugging end*)*)
2.398 +(*========== inhibit exn AK110721 ================================================
2.399 +"----- WN080102 these vvv do not work, because locatetac starts the search" ^
2.400 + "1 stac too low";
2.401 +(* AK110722 ERROR: assy: call by ([3], Pbl) *)
2.402 applyTactic 1 p (hd appltacs);
2.403 +============ inhibit exn AK110721 ==============================================*)
2.404 +
2.405 autoCalculate 1 CompleteCalc;
2.406 -============ inhibit exn 110721 ==============================================*)
2.407
2.408 "----------- fun init_form, fun get_stac -------------------------";
2.409 "----------- fun init_form, fun get_stac -------------------------";
2.410 @@ -365,4 +428,3 @@
2.411 "----------- x+1=2 set ctxt in Subproblem ------------------------";
2.412 "----------- x+1=2 set ctxt in Subproblem ------------------------";
2.413 "----------- x+1=2 set ctxt in Subproblem ------------------------";
2.414 -
3.1 --- a/test/Tools/isac/ProgLang/termC.sml Thu Jul 21 17:04:04 2011 +0200
3.2 +++ b/test/Tools/isac/ProgLang/termC.sml Fri Jul 22 15:57:22 2011 +0200
3.3 @@ -34,13 +34,15 @@
3.4 else error "termC.sml inst_bdv 1";
3.5
3.6 (*===== inhibit exn AK110721 ============================================================
3.7 - if string_of_thm (num_str @{thm separate_bdvs_add}) =
3.8 - "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\
3.9 - \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\""
3.10 + (*AK110722 string_of_thm isn't working correctly*)
3.11 +if string_of_thm (num_str @{thm separate_bdvs_add}) =
3.12 + "[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a"^
3.13 + " ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)"
3.14 then ()
3.15 else error "termC.sml separate_bdvs_add";
3.16 ===== inhibit exn AK110721 ============================================================*)
3.17 -
3.18 +*}
3.19 +ML {*
3.20 val subst = [(str2term "bdv_1", str2term "c"),
3.21 (str2term "bdv_2", str2term "c_2"),
3.22 (str2term "bdv_3", str2term "c_3"),
4.1 --- a/test/Tools/isac/Test_Isac.thy Thu Jul 21 17:04:04 2011 +0200
4.2 +++ b/test/Tools/isac/Test_Isac.thy Fri Jul 22 15:57:22 2011 +0200
4.3 @@ -48,8 +48,8 @@
4.4 ("Interpret/calchead.sml")
4.5 (*("Interpret/appl.sml")*)
4.6 ("Interpret/rewtools.sml")
4.7 -(*("Interpret/script.sml")
4.8 - ("Interpret/solve.sml")
4.9 + ("Interpret/script.sml")
4.10 +(* ("Interpret/solve.sml")
4.11 ("Interpret/inform.sml")*)
4.12 ("Interpret/mathengine.sml")
4.13
5.1 --- a/test/Tools/isac/Test_Some.thy Thu Jul 21 17:04:04 2011 +0200
5.2 +++ b/test/Tools/isac/Test_Some.thy Fri Jul 22 15:57:22 2011 +0200
5.3 @@ -13,6 +13,539 @@
5.4
5.5
5.6
5.7 +(* Title: tests on solve.sml
5.8 + Author: Walther Neuper 060508,
5.9 + (c) due to copyright terms
5.10 +
5.11 +is NOT ONLY dependent on Test, but on other thys:
5.12 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
5.13 +uses from Rational.ML: Rrls cancel_p, Rrls cancel
5.14 +which in turn
5.15 +uses from Poly.ML: Rls make_polynomial, Rls expand_binom
5.16 +
5.17 +use"../smltest/ME/solve.sml";
5.18 +use"solve.sml";
5.19 +*)
5.20 +
5.21 +"-----------------------------------------------------------------";
5.22 +"table of contents -----------------------------------------------";
5.23 +"-----------------------------------------------------------------";
5.24 +"--------- interSteps on norm_Rational ---------------------------";
5.25 +(*---vvv NOT working after meNEW.04mmdd*)
5.26 +"###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
5.27 +"--------- prepare pbl, met --------------------------------------";
5.28 +"-------- cancel, without detail ------------------------------";
5.29 +"-------- cancel, detail rev-rew (cancel) afterwards ----------";
5.30 +"-------------- cancel_p, without detail ------------------------------";
5.31 +"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
5.32 +(*---^^^ NOT working*)
5.33 +"on 'miniscript with mini-subpbl':";
5.34 +"------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
5.35 +"------ interSteps'detailrls' after CompleteCalc -----------------";
5.36 +"------ interSteps after appendFormula ---------------------------";
5.37 +(*---vvv not brought to work 0403*)
5.38 +"------ Detail_Set -----------------------------------------------";
5.39 +"###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
5.40 +"-----------------------------------------------------------------";
5.41 +"-----------------------------------------------------------------";
5.42 +"-----------------------------------------------------------------";
5.43 +
5.44 +
5.45 +"--------- interSteps on norm_Rational ---------------------------";
5.46 +"--------- interSteps on norm_Rational ---------------------------";
5.47 +"--------- interSteps on norm_Rational ---------------------------";
5.48 + states:=[];(*exp_IsacCore_Simp_Rat_Double_No-7.xml*)
5.49 + CalcTree [(["Term ((2/(x+3) + 2/(x - 3)) / (8*x/(x^2 - 9)))","normalform N"],
5.50 + ("Rational",
5.51 + ["rational","simplification"],
5.52 + ["simplification","of_rationals"]))];
5.53 + moveActiveRoot 1;
5.54 + autoCalculate 1 CompleteCalc;
5.55 + val ((pt,_),_) = get_calc 1; show_pt pt;
5.56 +
5.57 +(*with "Script SimplifyScript (t_::real) = -----------------
5.58 + \ ((Rewrite_Set norm_Rational False) t_)"
5.59 +case pt of Nd (PblObj _, [Nd _]) => ((*met only applies norm_Rational*))
5.60 + | _ => error "solve.sml: interSteps on norm_Rational 1";
5.61 +interSteps 1 ([1], Res);
5.62 +getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false;
5.63 +interSteps 1 ([1,3], Res);
5.64 +
5.65 +getTactic 1 ([1,4], Res) (*here get the tactic, and ...*);
5.66 +interSteps 1 ([1,5], Res) (*... here get the intermediate steps above*);
5.67 +
5.68 +getTactic 1 ([1,5,1], Frm);
5.69 +val ((pt,_),_) = get_calc 1; show_pt pt;
5.70 +
5.71 +getTactic 1 ([1,8], Res) (*Rewrite_Set "common_nominator_p" *);
5.72 +interSteps 1 ([1,9], Res)(*TODO.WN060606 reverse rew*);
5.73 +--------------------------------------------------------------------*)
5.74 +
5.75 +case pt of Nd (PblObj _, [Nd _, Nd _, Nd _, Nd _, Nd _, Nd _]) => ()
5.76 + | _ => error "solve.sml: interSteps on norm_Rational 1";
5.77 +(*these have been done now by the script ^^^ immediately...
5.78 +interSteps 1 ([1], Res);
5.79 +getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false;
5.80 +*)
5.81 +interSteps 1 ([6], Res);
5.82 +(*========== inhibit exn AK110721 ================================================
5.83 +
5.84 +getTactic 1 ([6,1], Frm) (*here get the tactic, and ...*);
5.85 +interSteps 1 ([6,1], Res) (*... here get the intermediate steps above*);
5.86 +
5.87 +getTactic 1 ([3,4,1], Frm);
5.88 +val ((pt,_),_) = get_calc 1; show_pt pt;
5.89 +val (Form form, SOME tac, asm) = pt_extract (pt, ([6], Res));
5.90 +case (term2str form, tac, terms2strs asm) of
5.91 + ("1 / 2", Check_Postcond ["rational", "simplification"],
5.92 + ["-36 * x + 4 * x ^^^ 3 ~= 0"]) => ()
5.93 + | _ => error "solve.sml: interSteps on norm_Rational 2";
5.94 +
5.95 +
5.96 +
5.97 +"###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
5.98 +"###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
5.99 +"###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
5.100 +val intermediate_ptyps = !ptyps;
5.101 +val intermediate_mets = !mets;
5.102 +
5.103 +"--------- prepare pbl, met --------------------------------------";
5.104 +"--------- prepare pbl, met --------------------------------------";
5.105 +"--------- prepare pbl, met --------------------------------------";
5.106 +store_pbt
5.107 + (prep_pbt Test.thy "pbl_ttestt" [] e_pblID
5.108 + (["test"],
5.109 + [],
5.110 + e_rls, NONE, []));
5.111 +store_pbt
5.112 + (prep_pbt Test.thy "pbl_ttestt_detail" [] e_pblID
5.113 + (["detail","test"],
5.114 + [("#Given" ,["realTestGiven t_"]),
5.115 + ("#Find" ,["realTestFind s_"])
5.116 + ],
5.117 + e_rls, NONE, [["Test","test_detail"]]));
5.118 +
5.119 +store_met
5.120 + (prep_met Test.thy "met_detbin" [] e_metID
5.121 + (["Test","test_detail_binom"]:metID,
5.122 + [("#Given" ,["realTestGiven t_"]),
5.123 + ("#Find" ,["realTestFind s_"])
5.124 + ],
5.125 + {rew_ord'="sqrt_right",rls'=tval_rls,calc = [],srls=e_rls,prls=e_rls,
5.126 + crls=tval_rls, nrls=e_rls(*,
5.127 + asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]*)},
5.128 + "Script Testterm (g_::real) = \
5.129 + \(((Rewrite_Set expand_binoms False) @@\
5.130 + \ (Rewrite_Set cancel False)) g_)"
5.131 + ));
5.132 +store_met
5.133 + (prep_met Test.thy "met_detpoly" [] e_metID
5.134 + (["Test","test_detail_poly"]:metID,
5.135 + [("#Given" ,["realTestGiven t_"]),
5.136 + ("#Find" ,["realTestFind s_"])
5.137 + ],
5.138 + {rew_ord'="sqrt_right",rls'=tval_rls,calc=[],srls=e_rls,prls=e_rls,
5.139 + crls=tval_rls, nrls=e_rls(*,
5.140 + asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]*)},
5.141 + "Script Testterm (g_::real) = \
5.142 + \(((Rewrite_Set make_polynomial False) @@\
5.143 + \ (Rewrite_Set cancel_p False)) g_)"
5.144 + ));
5.145 +
5.146 +(*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*)
5.147 +
5.148 +"-------- cancel, without detail ------------------------------";
5.149 +"-------- cancel, without detail ------------------------------";
5.150 +"-------- cancel, without detail ------------------------------";
5.151 +val fmz = ["realTestGiven (((3 + x) * (3 - x)) / ((3 + x) * (3 + x)))",
5.152 + "realTestFind s"];
5.153 +val (dI',pI',mI') =
5.154 + ("Test",["detail","test"],["Test","test_detail_binom"]);
5.155 +
5.156 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.157 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.158 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.159 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.160 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.161 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.162 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.163 +(*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*)
5.164 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.165 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.166 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.167 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.168 +(*"(3 + -1 * x) / (3 + x)"*)
5.169 +if nxt = ("End_Proof'",End_Proof') then ()
5.170 +else error "details.sml, changed behaviour in: without detail";
5.171 +
5.172 + val str = pr_ptree pr_short pt;
5.173 + writeln str;
5.174 +
5.175 +
5.176 +"-------- cancel, detail rev-rew (cancel) afterwards ----------";
5.177 +"-------- cancel, detail rev-rew (cancel) afterwards ----------";
5.178 +"-------- cancel, detail rev-rew (cancel) afterwards ----------";
5.179 + val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.180 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.181 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.182 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.183 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.184 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.185 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.186 + (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*)
5.187 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.188 + (*val nxt = ("Rewrite_Set",Rewrite_Set "expand_binoms")*)
5.189 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
5.190 +(* val nxt = ("Detail",Detail);"----------------------";*)
5.191 +
5.192 +
5.193 +(*WN.11.9.03: after meNEW not yet implemented -------------------------*)
5.194 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.195 +(*FIXXXXXME.040216 #####################################################
5.196 +# val nxt = ("Detail", Detail) : string * tac
5.197 +val it = "----------------------" : string
5.198 +> val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.199 +val f = Form' (FormKF (~1, EdUndef, ...)) : mout
5.200 +val nxt = ("Empty_Tac", Empty_Tac) : string * tac
5.201 +val p = ([2, 1], Res) : pos'
5.202 +#########################################################################
5.203 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.204 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.205 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.206 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.207 + (*val nxt = ("End_Detail",End_Detail)*)
5.208 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.209 + (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel")*)
5.210 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
5.211 + val nxt = ("Detail",Detail);"----------------------";
5.212 + val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
5.213 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.214 +(*15.10.02*)
5.215 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.216 +(*
5.217 +rewrite "Rationals" "tless_true""e_rls"true("sym_real_plus_minus_binom","")
5.218 + "3 ^^^ 2 - x ^^^ 2";
5.219 +*)
5.220 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.221 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.222 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.223 + val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
5.224 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.225 +if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 - x) / (3 + x)"))
5.226 + andalso nxt = ("End_Proof'",End_Proof') then ()
5.227 +else error "new behaviour in details.sml, \
5.228 + \cancel, rev-rew (cancel) afterwards";
5.229 +FIXXXXXME.040216 #####################################################*)
5.230 +
5.231 +(*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*)
5.232 +
5.233 +"-------------- cancel_p, without detail ------------------------------";
5.234 +"-------------- cancel_p, without detail ------------------------------";
5.235 +"-------------- cancel_p, without detail ------------------------------";
5.236 +val fmz = ["realTestGiven (((3 + x)*(3+(-1)*x)) / ((3+x) * (3+x)))",
5.237 + "realTestFind s"];
5.238 +val (dI',pI',mI') =
5.239 + ("Test",["detail","test"],["Test","test_detail_poly"]);
5.240 +
5.241 +(*val p = e_pos'; val c = [];
5.242 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
5.243 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
5.244 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.245 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.246 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.247 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.248 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.249 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.250 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.251 +(*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*)
5.252 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.253 +"(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))";
5.254 +
5.255 + (*14.3.03*)
5.256 +(*---------------WN060614?!?---
5.257 + val t = str2term "(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))";
5.258 + val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
5.259 + "(9 + - (x ^^^ 2)) / (9 + 6 * x + x ^^^ 2)";
5.260 + val SOME (t,_) = rewrite_set_ thy false cancel_p t; term2str t;
5.261 + cancel_p_ thy t;
5.262 +(---------------WN060614?!?---*)
5.263 +
5.264 + val t = str2term "(3 + x) * (3 + -1 * x)";
5.265 + val SOME (t,_) = rewrite_set_ thy false expand_poly t; term2str t;
5.266 + "3 * 3 + 3 * (-1 * x) + (x * 3 + x * (-1 * x))";
5.267 + val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;
5.268 + "3 * 3 + (3 * x + (-1 * (3 * x) + -1 * (x * x)))";
5.269 + val SOME (t,_) = rewrite_set_ thy false simplify_power t; term2str t;
5.270 + "3 ^^^ 2 + (3 * x + (-1 * (3 * x) + -1 * x ^^^ 2))";
5.271 + val SOME (t,_) = rewrite_set_ thy false collect_numerals t; term2str t;
5.272 + "9 + (0 * x + -1 * x ^^^ 2)";
5.273 + val SOME (t,_) = rewrite_set_ thy false reduce_012 t; term2str t;
5.274 + "9 + - (x ^^^ 2)";
5.275 + (*14.3.03*)
5.276 +
5.277 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.278 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.279 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.280 +(*"(3 + -1 * x) / (3 + x)"*)
5.281 +if nxt = ("End_Proof'",End_Proof') then ()
5.282 +else error "details.sml, changed behaviour in: cancel_p, without detail";
5.283 +
5.284 +"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
5.285 +"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
5.286 +"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
5.287 +(* val p = e_pos'; val c = [];
5.288 + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
5.289 + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
5.290 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.291 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.292 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.293 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.294 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.295 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.296 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.297 + (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail_poly"))*)
5.298 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.299 + (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)
5.300 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
5.301 +
5.302 +(*14.3.03.FIXXXXXME since Isa02/reverse-rew.sml:
5.303 + fun make_deriv ... Rls_ not yet impl. (| Thm | Calc)
5.304 + Rls_ needed for make_polynomial ----------------------
5.305 + val nxt = ("Detail",Detail);"----------------------";
5.306 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.307 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.308 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.309 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.310 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.311 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.312 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.313 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.314 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.315 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.316 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.317 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.318 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.319 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.320 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.321 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.322 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.323 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.324 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.325 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.326 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.327 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.328 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.329 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.330 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.331 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.332 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.333 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.334 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.335 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.336 + if nxt = ("End_Detail",End_Detail) then ()
5.337 + else error "details.sml: new behav. in Detail make_polynomial";
5.338 +----------------------------------------------------------------------*)
5.339 +
5.340 +(*---------------
5.341 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.342 + (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel_p")*)
5.343 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
5.344 + val nxt = ("Detail",Detail);"----------------------";
5.345 + val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
5.346 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.347 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.348 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.349 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.350 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.351 + val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
5.352 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.353 +if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 + x) / (3 - x)"))
5.354 + andalso nxt = ("End_Proof'",End_Proof') then ()
5.355 +else error "new behaviour in details.sml, cancel_p afterwards";
5.356 +
5.357 +----------------*)
5.358 +
5.359 +
5.360 +
5.361 +
5.362 +
5.363 +val fmz = ["realTestGiven ((x+3)+(-1)*(2+6*x))",
5.364 + "realTestFind s"];
5.365 +val (dI',pI',mI') =
5.366 + ("Test",["detail","test"],["Test","test_detail_poly"]);
5.367 +
5.368 +(* val p = e_pos'; val c = [];
5.369 + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
5.370 + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
5.371 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.372 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.373 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.374 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.375 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.376 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.377 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.378 + (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail_poly"))*)
5.379 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.380 +(*16.10.02 --- kommt auf POLY_EXCEPTION ?!??? ----------------------------
5.381 + (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)
5.382 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
5.383 + val nxt = ("Detail",Detail);"----------------------";
5.384 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.385 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.386 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.387 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.388 +-------------------------------------------------------------------------*)
5.389 +
5.390 +
5.391 +"------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
5.392 +"------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
5.393 +"------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
5.394 + states:=[];
5.395 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
5.396 + ("Test", ["sqroot-test","univariate","equation","test"],
5.397 + ["Test","squ-equ-test-subpbl1"]))];
5.398 + Iterator 1;
5.399 + moveActiveRoot 1;
5.400 + autoCalculate 1 CompleteCalc;
5.401 + moveActiveRoot 1;
5.402 +
5.403 + interSteps 1 ([],Res);
5.404 + val [(_,(((pt,_),_),[(_,ip)]))] = !states;
5.405 + val ("donesteps",_(*,ss*), lastpos) = detailstep pt ip;
5.406 + (*case ss of [(_,_,t1),(_,_,t2),(_,_,t3),(_,_,t4),(_,_,t5),(_,_,t6)] =>
5.407 + (writeln o terms2str) [t1,t2,t3,t4,t5,t6]
5.408 + | _ => error "details.sml: diff.behav. in detail miniscript";*) if lastpos = ([4], Res) then ()
5.409 + else error "details.sml: diff.behav. in interSteps'donesteps' 1";
5.410 +
5.411 + moveActiveDown 1;
5.412 + moveActiveDown 1;
5.413 + moveActiveDown 1;
5.414 + moveActiveDown 1;
5.415 +
5.416 + interSteps 1 ([3],Pbl) (*subproblem*);
5.417 + val [(_,(((pt,_),_),[(_,ip)]))] = !states;
5.418 + val ("donesteps",_(*,ss*), lastpos) = detailstep pt ip;
5.419 + (*case ss of [(_,_,t1),(_,_,t2),(_,_,t3)] =>
5.420 + (writeln o terms2str) [t1,t2,t3]
5.421 + | _ => error "details.sml: diff.behav. in detail miniscript";*) if lastpos = ([3, 2], Res) then ()
5.422 + else error "details.sml: diff.behav. in interSteps'donesteps' 1";
5.423 +
5.424 +
5.425 +(* val [(_,(((pt,_),_),[(_,ip)]))] = !states;
5.426 + writeln (pr_ptree pr_short pt);
5.427 + get_obj g_tac pt [4];
5.428 + *)
5.429 +
5.430 +
5.431 +"------ interSteps'detailrls' after CompleteCalc -----------------";
5.432 +"------ interSteps'detailrls' after CompleteCalc -----------------";
5.433 +"------ interSteps'detailrls' after CompleteCalc -----------------";
5.434 + states:=[];
5.435 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
5.436 + ("Test", ["sqroot-test","univariate","equation","test"],
5.437 + ["Test","squ-equ-test-subpbl1"]))];
5.438 + Iterator 1;
5.439 + moveActiveRoot 1;
5.440 + autoCalculate 1 CompleteCalc;
5.441 + interSteps 1 ([],Res);
5.442 + moveActiveRoot 1;
5.443 + moveActiveDown 1;
5.444 + moveActiveDown 1;
5.445 + moveActiveDown 1;
5.446 + refFormula 1 (get_pos 1 1); (* 2 Res, <ISA> -1 + x = 0 </ISA> *)
5.447 +
5.448 + interSteps 1 ([2],Res);
5.449 + val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;
5.450 + if length (children (get_nd pt p)) = 6 then ()
5.451 + else error "details.sml: diff.behav. in interSteps'detailrls' 1";
5.452 +
5.453 + moveActiveDown 1;
5.454 + moveActiveDown 1; refFormula 1 (get_pos 1 1); (* 3,1 Frm, <ISA> -1 + x = 0 </ISA> *);
5.455 +
5.456 + interSteps 1 ([3,1],Frm) (*<ERROR> first formula on level has NO detail </E*);
5.457 + val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;
5.458 + if length (children (get_nd pt p)) = 0 then () (*NO detail at ([xxx,1],Frm)*)
5.459 + else error "details.sml: diff.behav. in interSteps'detailrls' 2";
5.460 +
5.461 + moveActiveDown 1;
5.462 + refFormula 1 (get_pos 1 1); (* 3,1 Res, <ISA> x = 0 + -1 * -1 </ISA> *)
5.463 +
5.464 + interSteps 1 ([3,1],Res);
5.465 + val ((pt,p),_) = get_calc 1; show_pt pt;
5.466 + term2str (get_obj g_res pt [3,1,1]);(*"x = 0 + -1 * -1" ok*)
5.467 + term2str (get_obj g_form pt [3,2]); (*"x = 0 + -1 * -1" ok*)
5.468 + get_obj g_tac pt [3,1,1]; (*Rewrite_Inst.."risolate_bdv_add ok*)
5.469 +
5.470 + moveActiveDown 1;
5.471 + refFormula 1 (get_pos 1 1); (* 3,2 Res, <ISA> x = 1 </ISA> *)
5.472 +
5.473 + interSteps 1 ([3,2],Res);
5.474 + val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;
5.475 + if length (children (get_nd pt p)) = 2 then ()
5.476 + else error "details.sml: diff.behav. in interSteps'detailrls' 3";
5.477 +
5.478 + val ((pt,p),_) = get_calc 1; show_pt pt;
5.479 +
5.480 +
5.481 +"------ interSteps after appendFormula ---------------------------";
5.482 +"------ interSteps after appendFormula ---------------------------";
5.483 +"------ interSteps after appendFormula ---------------------------";
5.484 +states:=[];
5.485 +CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
5.486 + ("Test", ["sqroot-test","univariate","equation","test"],
5.487 + ["Test","squ-equ-test-subpbl1"]))];
5.488 +Iterator 1;
5.489 +moveActiveRoot 1;
5.490 +autoCalculate 1 CompleteCalcHead;
5.491 +autoCalculate 1 (Step 1);
5.492 +autoCalculate 1 (Step 1);
5.493 +appendFormula 1 "x - 1 = 0"(*generates intermediate steps*);
5.494 +(*these are not shown, because the resulting formula is on the same
5.495 + level as the previous formula*)
5.496 +interSteps 1 ([2],Res) (*error: last unchanged was ([2, 9], Res)*);
5.497 +(*...and these are the internals*)
5.498 +val ((pt,p),_) = get_calc 1; show_pt pt;
5.499 +val (_,_,lastpos) =detailstep pt p;
5.500 +if p = ([2], Res) andalso lastpos = ([2, 9], Res) then ()
5.501 +else error "solve.sml: diff.beh. after appendFormula x - 1 = 0";
5.502 +
5.503 +
5.504 +"------ Detail_Set -----------------------------------------------";
5.505 +"------ Detail_Set -----------------------------------------------";
5.506 +"------ Detail_Set -----------------------------------------------";
5.507 + states:=[]; (*start of calculation, return No.1*)
5.508 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
5.509 + ("Test", ["sqroot-test","univariate","equation","test"],
5.510 + ["Test","squ-equ-test-subpbl1"]))];
5.511 + Iterator 1; moveActiveRoot 1;
5.512 + autoCalculate 1 CompleteCalcHead;
5.513 + autoCalculate 1 (Step 1);
5.514 + autoCalculate 1 (Step 1);
5.515 +
5.516 + fetchProposedTactic 1 (*DG decides to do this tactic in detail*);
5.517 + (*TODO ...*)
5.518 + setNextTactic 1 (Detail_Set "Test_simplify");
5.519 +
5.520 +
5.521 + val ((pt,p),tacis) = get_calc 1;
5.522 + val str = pr_ptree pr_short pt;
5.523 + writeln str;
5.524 +
5.525 + print_depth 3;
5.526 + term2str (fst (get_obj g_result pt [1]));
5.527 +
5.528 +
5.529 +
5.530 +
5.531 +"###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
5.532 +"###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
5.533 +"###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
5.534 +ptyps:= intermediate_ptyps;
5.535 +mets:= intermediate_mets;
5.536 +========== inhibit exn AK110721 ================================================*)
5.537 +
5.538 +
5.539 +
5.540
5.541 *}
5.542 ML{*