1.1 --- a/test/Tools/isac/Interpret/script.sml Thu Jul 21 17:04:04 2011 +0200
1.2 +++ b/test/Tools/isac/Interpret/script.sml Fri Jul 22 15:57:22 2011 +0200
1.3 @@ -22,55 +22,55 @@
1.4
1.5 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
1.6 val str = (*#1#*)
1.7 -"Script BiegelinieScript \
1.8 -\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
1.9 -\(rb_::bool list) (rm_::bool list) = \
1.10 -\ (let q___ = Take (M_b v_v = q__); \
1.11 -\ (M1__::bool) = ((Substitute [v_ = 0])) q___ \
1.12 -\ in True)";
1.13 +"Script BiegelinieScript " ^
1.14 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
1.15 +"(rb_rb::bool list) (rm_rm::bool list) = " ^
1.16 +" (let q___q = Take (M_b v_v = q__q); " ^
1.17 +" (M1__M1::bool) = ((Substitute [v_v = 0])) q___q " ^
1.18 +" in True)";
1.19 +
1.20 (*========== inhibit exn 110721 ================================================
1.21 +(* ERROR: parse thy Can't unify theory to domID * rls*)
1.22 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.23 -(========= inhibit exn 110721 ================================================*)
1.24 +========= inhibit exn 110721 ================================================*)
1.25
1.26 val str = (*#2#*)
1.27 -"Script BiegelinieScript \
1.28 -\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
1.29 -\(rb_::bool list) (rm_::bool list) = \
1.30 -\ (let q___ = Take (q_ v_v = q__); \
1.31 -\ (M1__::bool) = ((Substitute [v_ = 0]) @@ \
1.32 -\ (Substitute [M_b 0 = 0])) q___ \
1.33 -\ in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*)
1.34 +"Script BiegelinieScript " ^
1.35 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
1.36 +"(rb_rb::bool list) (rm_rm::bool list) = " ^
1.37 +" (M1__M1::bool) = ((Substitute [v_v = 0]) @@ " ^
1.38 +" in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*)
1.39
1.40 val str = (*#3#*)
1.41 -"Script BiegelinieScript \
1.42 -\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
1.43 -\(rb_::bool list) (rm_::bool list) = \
1.44 -\ (let q___ = Take (q_ v_v = q__); \
1.45 -\ (M1__::bool) = Substitute [v_ = 0] q___ ; \
1.46 -\ M1__ = Substitute [M_b 0 = 0] M1__ \
1.47 -\ in True)"
1.48 +"Script BiegelinieScript " ^
1.49 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
1.50 +"(rb_rb::bool list) (rm_rm::bool list) = " ^
1.51 +" (let q___q = Take (q_q v_v = q__q); " ^
1.52 +" (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
1.53 +" M1__m1 = Substitute [M_b 0 = 0] M1__M1 " ^
1.54 +" in True)"
1.55 ;
1.56 val str = (*#4#*)
1.57 -"Script BiegelinieScript \
1.58 -\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
1.59 -\(rb_::bool list) (rm_::bool list) = \
1.60 -\ (let q___ = Take (q_ v_v = q__); \
1.61 -\ (M1__::bool) = Substitute [v_ = 0] q___ ; \
1.62 -\ M1__ = Substitute [v_ = 1] q___ ; \
1.63 -\ M1__ = Substitute [v_ = 2] q___ ; \
1.64 -\ M1__ = Substitute [v_ = 3] q___ ; \
1.65 -\ M1__ = Substitute [M_b 0 = 0] M1__ \
1.66 -\ in True)"
1.67 +"Script BiegelinieScript " ^
1.68 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
1.69 +"(rb_rb::bool list) (rm_rm::bool list) = " ^
1.70 +" (let q___q = Take (q_q v_v = q__q); " ^
1.71 +" (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
1.72 +" M1__M1 = Substitute [v_v = 1] q___q ; " ^
1.73 +" M1__M1 = Substitute [v_v = 2] q___q ; " ^
1.74 +" M1__M1 = Substitute [v_v = 3] q___q ; " ^
1.75 +" M1__M1 = Substitute [M_b 0 = 0] M1__M1 " ^
1.76 +" in True)"
1.77 ;
1.78 val str = (*#5#*)
1.79 -"Script BiegelinieScript \
1.80 -\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
1.81 -\(rb_::bool list) (rm_::bool list) = \
1.82 -\ (let q___ = Take (M_b v_v = q__); \
1.83 -\ (M1__::bool) = Substitute [v_ = 0] q___ ; \
1.84 -\ M2__ = Take q___ ; \
1.85 -\ M2__ = Substitute [v_ = 2] q___ \
1.86 -\ in True)"
1.87 +"Script BiegelinieScript " ^
1.88 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
1.89 +"(rb_rb::bool list) (rm_rm::bool list) = " ^
1.90 +" (let q___q = Take (M_b v_v = q__q); " ^
1.91 +" (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
1.92 +" M2__M2 = Take q___q ; " ^
1.93 +" M2__M2 = Substitute [v_v = 2] q___q " ^
1.94 +" in True)"
1.95 ;
1.96
1.97 (*========== inhibit exn 110721 ================================================
1.98 @@ -78,7 +78,7 @@
1.99 atomty sc';
1.100 ========== inhibit exn 110721 ================================================*)
1.101
1.102 -val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
1.103 +val {scr = Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
1.104 (*---------------------------------------------------------------------
1.105 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
1.106 ---------------------------------------------------------------------*)
1.107 @@ -97,18 +97,32 @@
1.108 val p = e_pos'; val c = [];
1.109
1.110 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.111 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.112 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.113 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.114 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.115 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.116 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.117 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.118 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.119 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.120 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.121 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.122 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.123
1.124 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
1.125 | _ => error "script.sml, doesnt find Substitute #2";
1.126 -(*========== inhibit exn 110721 ================================================
1.127 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.128 +
1.129 +(*========== inhibit exn AK110721 ================================================
1.130 +
1.131 +(* AK110722 f2str f is NOT working anywhere - deprecated?????*)
1.132 +
1.133 +(*(* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.134 + (* ERROR: exception PTREE "get_obj: pos = [0] does not exist" raised
1.135 + (line 908 of "src/Tools/isac/Interpret/ctree.sml")*)*)
1.136 +(*f2str f;
1.137 + (* ERROR: exception Match raised (line 416 of "src/Tools/isac/Interpret/mathengine.sml")*)*)
1.138 +(* "~~~~~ fun f2str, args:"; val ((Form' (FormKF (_, _, _, _, cterm')))) = (f);
1.139 + (* ERROR: exception Bind raised *)*)
1.140 +
1.141 + f;
1.142 + f2str;*)
1.143 +
1.144 (* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)
1.145 (* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)
1.146
1.147 @@ -125,8 +139,7 @@
1.148 (*the reason, that next_tac didnt find the 2nd Substitute, was that
1.149 the Take inbetween was missing, and thus the 2nd Substitute was applied
1.150 the last formula in ctree, and not to argument from script*)
1.151 -========== inhibit exn 110721 ================================================*)
1.152 -
1.153 +========== inhibit exn AK110721 ================================================*)
1.154
1.155
1.156 "----------- WN0509 Substitute 2nd part --------------------------";
1.157 @@ -134,16 +147,16 @@
1.158 "----------- WN0509 Substitute 2nd part --------------------------";
1.159 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
1.160 val str = (*Substitute ; Substitute works*)
1.161 -"Script BiegelinieScript \
1.162 -\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
1.163 -\(rb_::bool list) (rm_::bool list) = "^
1.164 +"Script BiegelinieScript " ^
1.165 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
1.166 +"(rb_rb::bool list) (rm_rm::bool list) = "^
1.167 (*begin after the 2nd integrate*)
1.168 -" (let M__ = Take (M_b v_v = q__); \
1.169 -\ e1__ = nth_ 1 rm_ ; \
1.170 -\ (x1__::real) = argument_in (lhs e1__); \
1.171 -\ (M1__::bool) = Substitute [v_ = x1__] M__; \
1.172 -\ M1__ = Substitute [e1__] M1__ \
1.173 -\ in True)"
1.174 +" (let M__M = Take (M_b v_v = q__q); " ^
1.175 +" e1__e1 = nth_nth 1 rm_rm ; " ^
1.176 +" (x1__x1::real) = argument_in (lhs e1__e1); " ^
1.177 +" (M1__M1::bool) = Substitute [v_v = x1__x1] M__M; " ^
1.178 +" M1__M1 = Substitute [e1__e1] M1__M1 " ^
1.179 +" in True)"
1.180 ;
1.181 (*========== inhibit exn 110721 ================================================
1.182 (*---^^^-OK-----------------------------------------------------------------*)
1.183 @@ -153,21 +166,21 @@
1.184 ========== inhibit exn 110721 ================================================*)
1.185
1.186 val str = (*Substitute @@ Substitute does NOT work???*)
1.187 -"Script BiegelinieScript \
1.188 -\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
1.189 -\(rb_::bool list) (rm_::bool list) = "^
1.190 +"Script BiegelinieScript " ^
1.191 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
1.192 +"(rb_rb::bool list) (rm_rm::bool list) = "^
1.193 (*begin after the 2nd integrate*)
1.194 -" (let M__ = Take (M_b v_v = q__); \
1.195 -\ e1__ = nth_ 1 rm_ ; \
1.196 -\ (x1__::real) = argument_in (lhs e1__); \
1.197 -\ (M1__::bool) = ((Substitute [v_ = x1__]) @@ \
1.198 -\ (Substitute [e1__])) M__ \
1.199 -\ in True)"
1.200 +" (let M__M = Take (M_b v_v = q__q); " ^
1.201 +" e1__e1 = nth_nth 1 rm_rm ; " ^
1.202 +" (x1__x1::real) = argument_in (lhs e1__e1); " ^
1.203 +" (M1__M1::bool) = ((Substitute [v_v = x1__x1]) @@ " ^
1.204 +" (Substitute [e1__e1])) M__M " ^
1.205 +" in True)"
1.206 ;
1.207
1.208 -val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
1.209 +val {scr = Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
1.210 (*---------------------------------------------------------------------
1.211 -if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
1.212 +if sc = sc' then () else error "script.sml, doesnt find Substitute #1";
1.213 ---------------------------------------------------------------------*)
1.214 val fmz = ["Traegerlaenge L",
1.215 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
1.216 @@ -180,60 +193,66 @@
1.217 ["IntegrierenUndKonstanteBestimmen"]);
1.218 val p = e_pos'; val c = [];
1.219 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.220 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.221 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.222 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.223 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.224 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.225 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.226 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.227 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.228 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.229 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.230 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.231 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.232 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
1.233 | _ => error "script.sml, doesnt find Substitute #2";
1.234
1.235 -(*========== inhibit exn 110721 ================================================
1.236 +(*========== inhibit exn AK110721 ================================================
1.237 +(* ERROR: caused by f2str f *)
1.238 trace_rewrite:=true;
1.239 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
1.240 trace_rewrite:=false;
1.241 -(*Exception TYPE raised:
1.242 -Illegal type for constant "HOL.eq" :: "[real, bool] => bool"
1.243 -Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
1.244 -ListG.nth_ (1 + -1 + -1) []
1.245 -Exception-
1.246 - TYPE
1.247 - ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
1.248 - [],
1.249 - [Const ("HOL.Trueprop", "bool => prop") $
1.250 - (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])
1.251 - raised
1.252 -... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
1.253 -ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
1.254 -thus corrected eval_argument_in OK*)
1.255 -========== inhibit exn 110721 ================================================*)
1.256 + (*Exception TYPE raised:
1.257 + Illegal type for constant "HOL.eq" :: "[real, bool] => bool"
1.258 + Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
1.259 + ListG.nth_ (1 + -1 + -1) []
1.260 + Exception-
1.261 + TYPE
1.262 + ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
1.263 + [],
1.264 + [Const ("HOL.Trueprop", "bool => prop") $
1.265 + (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])
1.266 + raised
1.267 + ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
1.268 + ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
1.269 + thus corrected eval_argument_in OK*)
1.270 +========== inhibit exn AK110721 ================================================*)
1.271
1.272 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
1.273 -val e1__ = str2term "nth_nth 1 [M_b 0 = 0, M_b L = 0]";
1.274 +val e1__e1 = str2term "nth_nth 1 [M_b 0 = 0, M_b L = 0]";
1.275 +val e1__e1 = eval_listexpr_ @{theory Biegelinie} srls e1__e1; term2str e1__e1;
1.276 +
1.277 (*========== inhibit exn 110721 ================================================
1.278 -val e1__ = eval_listexpr_ Biegelinie.thy srls e1__; term2str e1__;
1.279 +(*AK110722
1.280 + TRIAL: Should be the same
1.281 + term2str e1__e1 = "M_b 0 = 0";
1.282 + term2str e1__e1;*)
1.283
1.284 -if term2str e1__ = "M_b 0 = 0" then () else
1.285 -error"script.sml diff.beh. eval_listexpr_ nth_nth 1 [...";
1.286 +if term2str e1__e1 = "M_b 0 = 0"
1.287 + then ()
1.288 + else error"script.sml diff.beh. eval_listexpr_ nth_nth 1 [...";
1.289 ========== inhibit exn 110721 ================================================*)
1.290
1.291 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
1.292 -val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
1.293 -val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__;
1.294 -(*no rewrite*)
1.295 -calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__;
1.296 -val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
1.297 + val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
1.298 + val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__;
1.299 + (*no rewrite*)
1.300 + calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__;
1.301 + val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
1.302
1.303 -val l__ = str2term"lhs (M_b 0 = 0)";
1.304 +val l__l = str2term "lhs (M_b 0 = 0)";
1.305 +(*AK110722 eval_listexpr_ is prob. without _ ????*)
1.306 +val l__l = eval_listexpr_ @{theory Biegelinie} srls l__l; term2str l__l;
1.307 +val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term "lhs (M_b 0 = 0)") 0;
1.308 (*========== inhibit exn 110721 ================================================
1.309 -val l__ = eval_listexpr_ Biegelinie.thy srls l__; term2str l__;
1.310 -val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;
1.311 -
1.312 -
1.313 trace_rewrite:=true;
1.314 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
1.315 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f (*------------------------*);
1.316 trace_rewrite:=false;
1.317 ========== inhibit exn 110721 ================================================*)
1.318
1.319 @@ -255,21 +274,20 @@
1.320 val ((pt, p), _) = get_calc 1; show_pt pt;
1.321 val appltacs = sel_appl_atomic_tacs pt p;
1.322
1.323 -(*
1.324 -(*These SHOULD be the same*)
1.325 +(*========== inhibit exn AK110721 ================================================
1.326 +(*(*These SHOULD be the same*)
1.327 print_depth(999);
1.328 appltacs;
1.329 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
1.330 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
1.331 - Calculate "times"];*)
1.332 + Calculate "TIMES"];*)
1.333
1.334 -(*========== inhibit exn 110721 ================================================
1.335 if appltacs =
1.336 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
1.337 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
1.338 - Calculate "times"] then ()
1.339 + Calculate "TIMES"] then ()
1.340 else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
1.341 -========== inhibit exn 110721 ================================================*)
1.342 +========== inhibit exn AK110721 ================================================*)
1.343
1.344 trace_script := true;
1.345 trace_script := false;
1.346 @@ -277,13 +295,58 @@
1.347 val ((pt, p), _) = get_calc 1; show_pt pt;
1.348 val appltacs = sel_appl_atomic_tacs pt p;
1.349
1.350 -(*========== inhibit exn 110721 ================================================
1.351 -"----- WN080102 these vvv do not work, because locatetac starts the search\
1.352 - \1 stac too low";
1.353 -(* ERROR: assy: call by ([3], Pbl) *)
1.354 +(*(* AK110722 Debugging start*)
1.355 +(*applyTactic 1 p (hd appltacs); WAS assy: call by ([3], Pbl)*)
1.356 +"~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs));
1.357 +val ((pt, _), _) = get_calc cI;
1.358 +val p = get_pos cI 1;
1.359 +
1.360 +locatetac;
1.361 +locatetac tac;
1.362 +locatetac tac;
1.363 +
1.364 +(*locatetac tac (pt, ip); (*WAS assy: call by ([3], Pbl)*)*)
1.365 +"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
1.366 +val (mI,m) = mk_tac'_ tac;
1.367 +
1.368 +applicable_in p pt m ; (*Appl*)
1.369 +
1.370 +member op = specsteps mI; (*false*)
1.371 +
1.372 +(*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
1.373 +loc_solve_; (*without _ ??? result is -> lOc writing error ???*)
1.374 +(*val it = fn: string * tac_ -> ptree * (pos * pos_) -> lOc_*)
1.375 +(mI,m); (*string * tac*)
1.376 +ptp (*ptree * pos'*);
1.377 +
1.378 +"~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = ((mI,m), ptp);
1.379 +(*val (msg, cs') = solve m (pt, pos);
1.380 +(*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
1.381 +
1.382 +m;
1.383 +(pt, pos);
1.384 +
1.385 +"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
1.386 +(*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*)
1.387 +
1.388 +e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
1.389 +val ctxt = get_ctxt pt po;
1.390 +
1.391 +(*generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) m (e_istate, ctxt) (p,p_) pt;
1.392 +(*Argument: m : tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
1.393 +(assoc_thy (get_obj g_domID pt (par_pblobj pt p)));
1.394 +assoc_thy;
1.395 +
1.396 +(*not finished - error continues in fun generate1*)
1.397 +(* AK110722 Debugging end*)*)
1.398 +(*========== inhibit exn AK110721 ================================================
1.399 +"----- WN080102 these vvv do not work, because locatetac starts the search" ^
1.400 + "1 stac too low";
1.401 +(* AK110722 ERROR: assy: call by ([3], Pbl) *)
1.402 applyTactic 1 p (hd appltacs);
1.403 +============ inhibit exn AK110721 ==============================================*)
1.404 +
1.405 autoCalculate 1 CompleteCalc;
1.406 -============ inhibit exn 110721 ==============================================*)
1.407
1.408 "----------- fun init_form, fun get_stac -------------------------";
1.409 "----------- fun init_form, fun get_stac -------------------------";
1.410 @@ -365,4 +428,3 @@
1.411 "----------- x+1=2 set ctxt in Subproblem ------------------------";
1.412 "----------- x+1=2 set ctxt in Subproblem ------------------------";
1.413 "----------- x+1=2 set ctxt in Subproblem ------------------------";
1.414 -