intermed. ctxt ..: calculation x+1=2 goes through
1.1 --- a/src/Tools/isac/Interpret/script.sml Wed May 18 10:20:11 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Wed May 18 11:58:48 2011 +0200
1.3 @@ -398,7 +398,7 @@
1.4 (Substitute ((subte2sube o isalist2list) isasub), Empty_Tac_)
1.5
1.6 | stac2tac_ pt thy (Const("Script.Check'_elementwise",_) $ _ $
1.7 - (set as Const ("Collect",_) $ Abs (_,_,pred))) =
1.8 + (set as Const ("Set.Collect",_) $ Abs (_,_,pred))) =
1.9 (Check_elementwise (Print_Mode.setmp [] (Syntax.string_of_term
1.10 (thy2ctxt thy)) pred), (*set*)Empty_Tac_)
1.11
1.12 @@ -1279,184 +1279,100 @@
1.13
1.14
1.15 datatype appy_ = (*as argument in nxt_up, nstep_up, from appy*)
1.16 - (* Appy is only (final) returnvalue, not argument during search
1.17 - |*) Napp_ (*ev. detects 'script is not appropriate for this example'*)
1.18 - | Skip_; (*detects 'script successfully finished'
1.19 - also used as init-value for resuming; this works,
1.20 - because 'nxt_up Or e1' treats as Appy*)
1.21 + (* Appy is only (final) returnvalue, not argument during search *)
1.22 + Napp_ (*ev. detects 'script is not appropriate for this example'*)
1.23 + | Skip_; (*detects 'script successfully finished'
1.24 + also used as init-value for resuming; this works,
1.25 + because 'nxt_up Or e1' treats as Appy*)
1.26
1.27 -fun appy thy ptp E l
1.28 - (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v =
1.29 -(* val (thy, ptp, E, l, t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b)),a, v)=
1.30 - (thy, ptp, E, up@[R,D], body, a, v);
1.31 - appy thy ptp E l t a v;
1.32 - *)
1.33 - ((*tracing("### appy Let$e$Abs: is=");
1.34 - tracing(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
1.35 - case appy thy ptp E (l@[L,R]) e a v of
1.36 - Skip (res, E) =>
1.37 - let (*val _= tracing("### appy Let "^(term2str t));
1.38 - val _= tracing("### appy Let: Skip res ="^(term2str res));*)
1.39 - (*val (i',b') = variant_abs (i,T,b); WN.15.5.03
1.40 - val i = mk_Free(i',T); WN.15.5.03 *)
1.41 - val E' = upd_env E (Free (i,T), res);
1.42 - in appy thy ptp E' (l@[R,D]) b a v end
1.43 - | ay => ay)
1.44 +fun appy thy ptp E l (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v =
1.45 + (case appy thy ptp E (l@[L,R]) e a v of
1.46 + Skip (res, E) =>
1.47 + let val E' = upd_env E (Free (i,T), res);
1.48 + in appy thy ptp E' (l@[R,D]) b a v end
1.49 + | ay => ay)
1.50
1.51 - | appy (thy as (th,sr)) ptp E l
1.52 - (t as Const ("Script.While"(*1*),_) $ c $ e $ a) _ v = (*ohne n. 28.9.00*)
1.53 - ((*tracing("### appy While $ c $ e $ a, upd_env= "^
1.54 - (subst2str (upd_env E (a,v))));*)
1.55 - if eval_true_ th sr (subst_atomic (upd_env E (a,v)) c)
1.56 - then appy thy ptp E (l@[L,R]) e (SOME a) v
1.57 - else Skip (v, E))
1.58 + | appy (thy as (th,sr)) ptp E l (t as Const ("Script.While"(*1*),_) $ c $ e $ a) _ v =
1.59 + (if eval_true_ th sr (subst_atomic (upd_env E (a,v)) c)
1.60 + then appy thy ptp E (l@[L,R]) e (SOME a) v
1.61 + else Skip (v, E))
1.62
1.63 - | appy (thy as (th,sr)) ptp E l
1.64 - (t as Const ("Script.While"(*2*),_) $ c $ e) a v =(*ohne nachdenken 28.9.00*)
1.65 - ((*tracing("### appy While $ c $ e, upd_env= "^
1.66 - (subst2str (upd_env_opt E (a,v))));*)
1.67 - if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
1.68 - then appy thy ptp E (l@[R]) e a v
1.69 - else Skip (v, E))
1.70 + | appy (thy as (th,sr)) ptp E l (t as Const ("Script.While"(*2*),_) $ c $ e) a v =
1.71 + (if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
1.72 + then appy thy ptp E (l@[R]) e a v
1.73 + else Skip (v, E))
1.74
1.75 | appy (thy as (th,sr)) ptp E l (t as Const ("If",_) $ c $ e1 $ e2) a v =
1.76 - ((*tracing("### appy If: t= "^(term2str t));
1.77 - tracing("### appy If: c= "^(term2str(subst_atomic(upd_env_opt E(a,v))c)));
1.78 - tracing("### appy If: thy= "^(fst thy));*)
1.79 - if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
1.80 - then ((*tracing("### appy If: true");*)appy thy ptp E (l@[L,R]) e1 a v)
1.81 - else ((*tracing("### appy If: false");*)appy thy ptp E (l@[ R]) e2 a v))
1.82 -(* val (thy, ptp, E, l, (Const ("Script.Repeat",_) $ e $ a), _, v) =
1.83 - (thy, ptp, E, (l@[R]), e, a, v);
1.84 - *)
1.85 - | appy thy ptp E (*env*) l
1.86 - (Const ("Script.Repeat"(*1*),_) $ e $ a) _ v =
1.87 - ((*tracing("### appy Repeat a: ");*)
1.88 - appy thy ptp E (*env*) (l@[L,R]) e (SOME a) v)
1.89 -(* val (thy, ptp, E, l, (Const ("Script.Repeat",_) $ e), _, v) =
1.90 - (thy, ptp, E, (l@[R]), e, a, v);
1.91 - *)
1.92 - | appy thy ptp E (*env*) l
1.93 - (Const ("Script.Repeat"(*2*),_) $ e) a v =
1.94 - ((*tracing("3### appy Repeat: a= " ^ term2str a);*)
1.95 - appy thy ptp E (*env*) (l@[R]) e a v)
1.96 -(* val (thy, ptp, E, l, (t as Const ("Script.Try",_) $ e $ a), _, v)=
1.97 - (thy, ptp, E, (l@[R]), e2, a, v);
1.98 - *)
1.99 - | appy thy ptp E l
1.100 - (t as Const ("Script.Try",_) $ e $ a) _ v =
1.101 - (case appy thy ptp E (l@[L,R]) e (SOME a) v of
1.102 - Napp E => ((*tracing("### appy Try " ^ term2str t);*)
1.103 - Skip (v, E))
1.104 - | ay => ay)
1.105 -(* val (thy, ptp, E, l, (t as Const ("Script.Try",_) $ e), _, v)=
1.106 - (thy, ptp, E, (l@[R]), e2, a, v);
1.107 - val (thy, ptp, E, l, (t as Const ("Script.Try",_) $ e), _, v)=
1.108 - (thy, ptp, E, (l@[L,R]), e1, a, v);
1.109 - *)
1.110 - | appy thy ptp E l
1.111 - (t as Const ("Script.Try",_) $ e) a v =
1.112 - (case appy thy ptp E (l@[R]) e a v of
1.113 - Napp E => ((*tracing("### appy Try " ^ term2str t);*)
1.114 - Skip (v, E))
1.115 - | ay => ay)
1.116 + (if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
1.117 + then ((*tracing("### appy If: true");*)appy thy ptp E (l@[L,R]) e1 a v)
1.118 + else ((*tracing("### appy If: false");*)appy thy ptp E (l@[ R]) e2 a v))
1.119
1.120 + | appy thy ptp E l (Const ("Script.Repeat"(*1*),_) $ e $ a) _ v =
1.121 + (appy thy ptp E (l@[L,R]) e (SOME a) v)
1.122
1.123 - | appy thy ptp E l
1.124 - (Const ("Script.Or"(*1*),_) $e1 $ e2 $ a) _ v =
1.125 - (case appy thy ptp E (l@[L,L,R]) e1 (SOME a) v of
1.126 - Appy lme => Appy lme
1.127 - | _ => appy thy ptp E (*env*) (l@[L,R]) e2 (SOME a) v)
1.128 + | appy thy ptp E l (Const ("Script.Repeat"(*2*),_) $ e) a v =
1.129 + (appy thy ptp E (l@[R]) e a v)
1.130 +
1.131 + | appy thy ptp E l (t as Const ("Script.Try",_) $ e $ a) _ v =
1.132 + (case appy thy ptp E (l@[L,R]) e (SOME a) v of
1.133 + Napp E => (Skip (v, E))
1.134 + | ay => ay)
1.135 +
1.136 + | appy thy ptp E l(t as Const ("Script.Try",_) $ e) a v =
1.137 + (case appy thy ptp E (l@[R]) e a v of
1.138 + Napp E => (Skip (v, E))
1.139 + | ay => ay)
1.140 +
1.141 + | appy thy ptp E l (Const ("Script.Or"(*1*),_) $e1 $ e2 $ a) _ v =
1.142 + (case appy thy ptp E (l@[L,L,R]) e1 (SOME a) v of
1.143 + Appy lme => Appy lme
1.144 + | _ => appy thy ptp E (*env*) (l@[L,R]) e2 (SOME a) v)
1.145
1.146 - | appy thy ptp E l
1.147 - (Const ("Script.Or"(*2*),_) $e1 $ e2) a v =
1.148 - (case appy thy ptp E (l@[L,R]) e1 a v of
1.149 - Appy lme => Appy lme
1.150 + | appy thy ptp E l (Const ("Script.Or"(*2*),_) $e1 $ e2) a v =
1.151 + (case appy thy ptp E (l@[L,R]) e1 a v of
1.152 + Appy lme => Appy lme
1.153 | _ => appy thy ptp E (l@[R]) e2 a v)
1.154
1.155 -(* val (thy, ptp, E, l, (Const ("Script.Seq",_) $ e1 $ e2 $ a), _, v)=
1.156 - (thy, ptp, E,(up@[R]),e2, a, v);
1.157 - val (thy, ptp, E, l, (Const ("Script.Seq",_) $ e1 $ e2 $ a), _, v)=
1.158 - (thy, ptp, E,(up@[R,D]),body, a, v);
1.159 - *)
1.160 - | appy thy ptp E l
1.161 - (Const ("Script.Seq"(*1*),_) $ e1 $ e2 $ a) _ v =
1.162 - ((*tracing("### appy Seq $ e1 $ e2 $ a, upd_env= "^
1.163 - (subst2str (upd_env E (a,v))));*)
1.164 - case appy thy ptp E (l@[L,L,R]) e1 (SOME a) v of
1.165 - Skip (v,E) => appy thy ptp E (l@[L,R]) e2 (SOME a) v
1.166 + | appy thy ptp E l (Const ("Script.Seq"(*1*),_) $ e1 $ e2 $ a) _ v =
1.167 + (case appy thy ptp E (l@[L,L,R]) e1 (SOME a) v of
1.168 + Skip (v,E) => appy thy ptp E (l@[L,R]) e2 (SOME a) v
1.169 | ay => ay)
1.170
1.171 -(* val (thy, ptp, E, l, (Const ("Script.Seq",_) $ e1 $ e2), _, v)=
1.172 - (thy, ptp, E,(up@[R]),e2, a, v);
1.173 - val (thy, ptp, E, l, (Const ("Script.Seq",_) $ e1 $ e2), _, v)=
1.174 - (thy, ptp, E,(l@[R]), e2, a, v);
1.175 - val (thy, ptp, E, l, (Const ("Script.Seq",_) $ e1 $ e2), _, v)=
1.176 - (thy, ptp, E,(up@[R,D]),body, a, v);
1.177 - *)
1.178 - | appy thy ptp E l
1.179 - (Const ("Script.Seq",_) $ e1 $ e2) a v =
1.180 - (case appy thy ptp E (l@[L,R]) e1 a v of
1.181 - Skip (v,E) => appy thy ptp E (l@[R]) e2 a v
1.182 + | appy thy ptp E l (Const ("Script.Seq",_) $ e1 $ e2) a v =
1.183 + (case appy thy ptp E (l@[L,R]) e1 a v of
1.184 + Skip (v,E) => appy thy ptp E (l@[R]) e2 a v
1.185 | ay => ay)
1.186
1.187 - (*.a leaf has been found*)
1.188 + (* a leaf has been found *)
1.189 | appy (thy as (th,sr)) (pt, p) E l t a v =
1.190 -(* val (thy as (th,sr),(pt, p),E, l, t, a, v) =
1.191 - (thy, ptp, E, up@[R,D], body, a, v);
1.192 - val (thy as (th,sr),(pt, p),E, l, t, a, v) =
1.193 - (thy, ptp, E, l@[L,R], e, a, v);
1.194 - val (thy as (th,sr),(pt, p),E, l, t, a, v) =
1.195 - (thy, ptp, E,(l@[R]), e, a, v);
1.196 - *)
1.197 - (case handle_leaf "next " th sr E a v t of
1.198 -(* val (a', Expr s) = handle_leaf "next " th sr E a v t;
1.199 - *)
1.200 - (a', Expr s) => Skip (s, E)
1.201 -(* val (a', STac stac) = handle_leaf "next " th sr E a v t;
1.202 - *)
1.203 - | (a', STac stac) =>
1.204 - let
1.205 - (*val _= tracing("### appy t, vor stac2tac_ is=");
1.206 - val _= tracing(istate2str (ScrState (E,l,a',v,Sundef,false)));*)
1.207 - val (m,m') = stac2tac_ pt (assoc_thy th) stac
1.208 - in case m of
1.209 - Subproblem _ => Appy (m', (E,l,a',tac_2res m',Sundef,false))
1.210 - | _ => (case applicable_in p pt m of
1.211 -(* val Appl m' = applicable_in p pt m;
1.212 - *)
1.213 - Appl m' =>
1.214 - ((*tracing("### appy: Appy");*)
1.215 - Appy (m', (E,l,a',tac_2res m',Sundef,false)))
1.216 - | _ => ((*tracing("### appy: Napp");*)Napp E))
1.217 - end);
1.218 + (case handle_leaf "next " th sr E a v t of
1.219 + (a', Expr s) => Skip (s, E)
1.220 + | (a', STac stac) =>
1.221 + let val (m,m') = stac2tac_ pt (assoc_thy th) stac
1.222 + in
1.223 + case m of
1.224 + Subproblem _ => Appy (m', (E,l,a',tac_2res m',Sundef,false))
1.225 + | _ =>
1.226 + (case applicable_in p pt m of
1.227 + Appl m' => (Appy (m', (E,l,a',tac_2res m',Sundef,false)))
1.228 + | _ => ((*tracing("### appy: Napp");*)Napp E))
1.229 + end);
1.230
1.231 -
1.232 -(* val (scr as Script sc, l, t as Const ("HOL.Let",_) $ _) =
1.233 - (Script sc, up, go up sc);
1.234 - nxt_up thy ptp (Script sc) E l ay t a v;
1.235 -
1.236 - val (thy,ptp,scr as (Script sc),E,l, ay, t as Const ("HOL.Let",_) $ _, a, v)=
1.237 - (thy,ptp,Script sc, E,up,ay, go up sc, a, v);
1.238 - nxt_up thy ptp scr E l ay t a v;
1.239 - *)
1.240 fun nxt_up thy ptp (scr as (Script sc)) E l ay
1.241 (t as Const ("HOL.Let",_) $ _) a v = (*comes from let=...*)
1.242 - ((*tracing("### nxt_up1 Let$e: is=");
1.243 - tracing(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
1.244 - if ay = Napp_
1.245 - then nstep_up thy ptp scr E (drop_last l) Napp_ a v
1.246 - else (*Skip_*)
1.247 - let val up = drop_last l;
1.248 - val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc;
1.249 + (if ay = Napp_
1.250 + then nstep_up thy ptp scr E (drop_last l) Napp_ a v
1.251 + else (*Skip_*)
1.252 + let
1.253 + val up = drop_last l;
1.254 + val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc;
1.255 val i = mk_Free (i, T);
1.256 val E = upd_env E (i, v);
1.257 - (*val _= tracing("### nxt_up2 Let$e: is=");
1.258 - val _= tracing(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
1.259 - in case appy thy ptp (E) (up@[R,D]) body a v of
1.260 - Appy lre => Appy lre
1.261 - | Napp E => nstep_up thy ptp scr E up Napp_ a v
1.262 - | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v end)
1.263 + in
1.264 + case appy thy ptp E (up@[R,D]) body a v of
1.265 + Appy lre => Appy lre
1.266 + | Napp E => nstep_up thy ptp scr E up Napp_ a v
1.267 + | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v end)
1.268
1.269 | nxt_up thy ptp scr E l ay
1.270 (t as Abs (_,_,_)) a v =
1.271 @@ -1581,16 +1497,12 @@
1.272 (thy, ptp, sc, E, l, Skip_, a, v);
1.273 *)
1.274 and nstep_up thy ptp (Script sc) E l ay a v =
1.275 - ((*tracing ("### nstep_up from: " ^ (loc_2str l));
1.276 - tracing ("### nstep_up from: " ^ term2str (go l sc));*)
1.277 - if 1 < length l
1.278 + (if 1 < length l
1.279 then
1.280 - let
1.281 - val up = drop_last l;
1.282 - in ((*tracing("### nstep_up to: " ^ term2str (go up sc));*)
1.283 - nxt_up thy ptp (Script sc) E up ay (go up sc) a v ) end
1.284 + let val up = drop_last l;
1.285 + in (nxt_up thy ptp (Script sc) E up ay (go up sc) a v ) end
1.286 else (*interpreted to end*)
1.287 - if ay = Skip_ then Skip (v, E) else Napp E
1.288 + if ay = Skip_ then Skip (v, E) else Napp E
1.289 );
1.290
1.291 (* decide for the next applicable stac in the script;
1.292 @@ -1618,9 +1530,9 @@
1.293 (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
1.294 end
1.295
1.296 - | next_tac thy (ptp as (pt,pos as (p,_)):ptree * pos') (sc as Script (h $ body))
1.297 + | next_tac thy (ptp as (pt, pos as (p, _)):ptree * pos') (sc as Script (h $ body))
1.298 (ScrState (E,l,a,v,s,b), ctxt) =
1.299 - let val ctxt = get_ctxt pt pos
1.300 + let val ctxt = get_ctxt pt pos (*WN110518 we have ctxt twice -- redesign*)
1.301 in
1.302 (case if l = []
1.303 then appy thy ptp E [R] body NONE v
2.1 --- a/test/Tools/isac/Minisubpbl/500-met-sub-to-root.sml Wed May 18 10:20:11 2011 +0200
2.2 +++ b/test/Tools/isac/Minisubpbl/500-met-sub-to-root.sml Wed May 18 11:58:48 2011 +0200
2.3 @@ -27,12 +27,17 @@
2.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
2.6 val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set_Inst isolate_bdv*);
2.7 -get_ctxt pt p |> is_e_ctxt; (*true ...?!?*)
2.8 -get_loc pt p |> snd |> is_e_ctxt; (*true ...?!?*)
2.9 +get_ctxt pt p |> is_e_ctxt; (*false*)
2.10 +val ctxt = get_ctxt pt p;
2.11 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
2.12 +get_loc pt p |> snd |> is_e_ctxt; (*false*)
2.13 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
2.14 -get_ctxt pt p |> is_e_ctxt; (*true ...?!?*)
2.15 -get_loc pt p |> snd |> is_e_ctxt; (*true ...?!?*)
2.16 +get_ctxt pt p |> is_e_ctxt; (*false*)
2.17 +val ctxt = get_ctxt pt p;
2.18 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
2.19 +get_loc pt p |> snd |> is_e_ctxt; (*false*)
2.20 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
2.21 +val (pt'''', p'''') = (pt, p);
2.22 "~~~~~ fun me, args:"; val (_,tac) = nxt;
2.23 val (pt, p) = case locatetac tac (pt,p) of
2.24 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
2.25 @@ -44,8 +49,32 @@
2.26 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
2.27 val thy' = get_obj g_domID pt (par_pblobj pt p);
2.28 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
2.29 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
2.30 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), (sc as Script (h $ body)),
2.31 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
2.32 +val ctxt = get_ctxt pt pos
2.33 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
2.34 l; (*= [R, R, D, L, R]*)
2.35 -"~~~~~ dont like to go into nstep_up...";
2.36 -
2.37 +"~~~~~ fun nstep_up, args:"; val (thy, ptp, (Script sc), E, l, ay, a, v) =
2.38 + (thy, ptp, sc, E, l, Skip_, a, v);
2.39 +1 < length l; (*true*)
2.40 +val up = drop_last l;
2.41 +go up sc; (* = Const ("HOL.Let", *)
2.42 +"~~~~~ fun nxt_up, args:"; val (thy, ptp, (scr as (Script sc)), E, l, ay,
2.43 + (t as Const ("HOL.Let",_) $ _), a, v) =
2.44 + (thy, ptp, (Script sc), E, up, ay, (go up sc), a, v);
2.45 +ay = Napp_; (*false*)
2.46 +val up = drop_last l;
2.47 +val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc;
2.48 +val i = mk_Free (i, T);
2.49 +val E = upd_env E (i, v);
2.50 +body; (*= Const ("Script.Check'_elementwise"*)
2.51 +"~~~~~ fun appy, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v)=
2.52 + (thy, ptp, E, (up@[R,D]), body, a, v);
2.53 +handle_leaf "next " th sr E a v t; (*= (NONE, STac (Const ("Script.Check'_elementwise"*)
2.54 +val (a', STac stac) = handle_leaf "next " th sr E a v t;
2.55 +"~~~~~ fun stac2tac_, args:"; val (pt, thy, (Const("Script.Check'_elementwise",_) $ _ $
2.56 + (set as Const ("Set.Collect",_) $ Abs (_,_,pred)))) = (pt, (assoc_thy th), stac);
2.57 +(*2011 changed ^^^^^ *)
2.58 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*WAS nxt = ("Empty_Tac", Empty_Tac)*)
2.59 +if nxt = ("Check_elementwise", Check_elementwise "Assumptions") then ()
2.60 +else error "Check_elementwise changed; after switch sub-->root-method"
3.1 --- a/test/Tools/isac/Minisubpbl/600-postcond.sml Wed May 18 10:20:11 2011 +0200
3.2 +++ b/test/Tools/isac/Minisubpbl/600-postcond.sml Wed May 18 11:58:48 2011 +0200
3.3 @@ -18,7 +18,6 @@
3.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.6 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Subproblem"*)
3.7 -(*
3.8 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.9 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.10 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.11 @@ -27,4 +26,12 @@
3.12 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.13 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.14 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.15 -*)
3.16 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.17 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.18 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.19 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.20 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.21 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.22 +if nxt = ("End_Proof'", End_Proof') andalso p = ([], Res)
3.23 +andalso get_obj g_res pt (fst p) = str2term "[x=1]" then ()
3.24 +else error "calculation not finished correctly";
4.1 --- a/test/Tools/isac/Test_Isac.thy Wed May 18 10:20:11 2011 +0200
4.2 +++ b/test/Tools/isac/Test_Isac.thy Wed May 18 11:58:48 2011 +0200
4.3 @@ -172,77 +172,7 @@
4.4 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
4.5
4.6 ML {*
4.7 -(*500-met-sub-to-root*)
4.8 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
4.9 -val (dI',pI',mI') =
4.10 - ("Test", ["sqroot-test","univariate","equation","test"],
4.11 - ["Test","squ-equ-test-subpbl1"]);
4.12 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.13 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.14 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.15 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.16 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.17 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.18 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.19 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
4.20 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.21 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.22 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
4.23 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.24 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.25 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.26 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.27 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.28 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.29 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.30 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
4.31 -val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set_Inst isolate_bdv*);
4.32 -get_ctxt pt p |> is_e_ctxt; (*false*)
4.33 -val ctxt = get_ctxt pt p;
4.34 -val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
4.35 -get_loc pt p |> snd |> is_e_ctxt; (*false*)
4.36 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
4.37 -get_ctxt pt p |> is_e_ctxt; (*false*)
4.38 -val ctxt = get_ctxt pt p;
4.39 -val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
4.40 -get_loc pt p |> snd |> is_e_ctxt; (*false*)
4.41 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
4.42 -val (pt'', p'') = (pt, p);
4.43 *}
4.44 -ML {*
4.45 -val (pt'', p'') = (pt, p);
4.46 -"~~~~~ fun me, args:"; val (_,tac) = nxt;
4.47 -val (pt, p) = case locatetac tac (pt,p) of
4.48 - ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
4.49 -show_pt pt; (*...(([3], Res), [x = 1])]... back in root, OK *)
4.50 -"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
4.51 -val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)
4.52 -tacis; (*= []*)
4.53 -member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
4.54 -"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
4.55 -val thy' = get_obj g_domID pt (par_pblobj pt p);
4.56 -val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
4.57 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
4.58 - (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
4.59 -l; (*= [R, R, D, L, R]*)
4.60 -"~~~~~ dont like to go into nstep_up...";
4.61 -*}
4.62 -ML {*
4.63 -*}
4.64 -ML {*
4.65 -*}
4.66 -ML {*
4.67 -*}
4.68 -ML {*
4.69 -*}
4.70 -ML {*
4.71 -*}
4.72 -ML {*
4.73 -*}
4.74 -ML {*
4.75 -val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*WAS nxt = ("Empty_Tac", Empty_Tac)*)
4.76 -*}
4.77 -
4.78 end
4.79
4.80 (*=== inhibit exn ?=============================================================