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