1.1 --- a/src/Tools/isac/Interpret/script.sml Sun May 15 13:59:05 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Tue May 17 09:55:30 2011 +0200
1.3 @@ -65,22 +65,24 @@
1.4 (*.makes a (rule,term) list to a Step (m, mout, pt', p', cid) for solve;
1.5 complicated with current t in rrlsstate.*)
1.6 fun rts2steps steps ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) [(r, (f', am))] =
1.7 - let val thy = assoc_thy thy'
1.8 - val m = Rewrite' (thy',ro,er,pa, rule2thm' r, f, (f', am))
1.9 - val is = RrlsState (f',f'',rss,rts)
1.10 - val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)
1.11 - val (p', cid, mout, pt') = generate1 thy m (is, e_ctxt) p pt
1.12 - in (is, (m, mout, pt', p', cid)::steps) end
1.13 - | rts2steps steps ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa))
1.14 - ((r, (f', am))::rts') =
1.15 - let val thy = assoc_thy thy'
1.16 - val m = Rewrite' (thy',ro,er,pa, rule2thm' r, f, (f', am))
1.17 - val is = RrlsState (f',f'',rss,rts)
1.18 - val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)
1.19 - val (p', cid, mout, pt') = generate1 thy m (is, e_ctxt) p pt
1.20 - in rts2steps ((m, mout, pt', p', cid)::steps)
1.21 - ((pt',p'),(f',f'',rss,rts),(thy',ro,er,pa)) rts' end;
1.22 -
1.23 + let
1.24 + val thy = assoc_thy thy'
1.25 + val ctxt = get_ctxt pt p |> insert_assumptions am
1.26 + val m = Rewrite' (thy', ro, er, pa, rule2thm' r, f, (f', am))
1.27 + val is = RrlsState (f', f'', rss, rts)
1.28 + val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)
1.29 + val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt
1.30 + in (is, (m, mout, pt', p', cid) :: steps) end
1.31 + | rts2steps steps ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) ((r, (f', am))::rts') =
1.32 + let
1.33 + val thy = assoc_thy thy'
1.34 + val ctxt = get_ctxt pt p |> insert_assumptions am
1.35 + val m = Rewrite' (thy',ro,er,pa, rule2thm' r, f, (f', am))
1.36 + val is = RrlsState (f',f'',rss,rts)
1.37 + val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)
1.38 + val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt
1.39 + in rts2steps ((m, mout, pt', p', cid)::steps)
1.40 + ((pt',p'),(f',f'',rss,rts),(thy',ro,er,pa)) rts' end;
1.41
1.42 (*. functions for the environment stack .*)
1.43 fun accessenv id es = the (assoc((top es):env, id))
1.44 @@ -261,20 +263,18 @@
1.45 (*.get the identifier of the script out of the scripts parsetree.*)
1.46 fun id_of_scr sc = (id_of o fst o strip_comb) sc;
1.47
1.48 -
1.49 (*WN020526: not clear, when a is available in ass_up for eva-_true*)
1.50 (*WN060906: in "fun handle_leaf" eg. uses "SOME M__"(from some PREVIOUS
1.51 curried Rewrite) for CURRENT value (which may be different from PREVIOUS);
1.52 thus "NONE" must be set at the end of currying (ill designed anyway)*)
1.53 fun upd_env_opt env (SOME a, v) = upd_env env (a,v)
1.54 | upd_env_opt env (NONE, v) =
1.55 - (tracing("*** upd_env_opt: (NONE,"^(term2str v)^")");env);
1.56 -
1.57 + (tracing ("*** upd_env_opt: (NONE," ^ term2str v ^ ")"); env);
1.58
1.59 type dsc = typ; (*<-> nam..unknow in Descript.thy*)
1.60 fun typ_str (Type (s,_)) = s
1.61 | typ_str (TFree(s,_)) = s
1.62 - | typ_str (TVar ((s,i),_)) = s^(string_of_int i);
1.63 + | typ_str (TVar ((s,i),_)) = s ^ (string_of_int i);
1.64
1.65 (*get the _result_-type of a description*)
1.66 fun dsc_valT (Const (_,(Type (_,[_,T])))) = (strip_thy o typ_str) T;
1.67 @@ -859,36 +859,34 @@
1.68 FIXXXXME: simplify rep_tac_*)
1.69
1.70
1.71 -(*.handle a leaf;
1.72 +(* handle a leaf at the end of recursive descent:
1.73 a leaf is either a tactic or an 'exp' in 'let v = expr'
1.74 where 'exp' does not contain a tactic.
1.75 handling a leaf comprises
1.76 (1) 'subst_stacexpr' substitute env and complete curried tactic
1.77 (2) rewrite the leaf by 'srls'
1.78 -WN060906 quick and dirty fix: return a' too (for updating E later)
1.79 -.*)
1.80 +*)
1.81 fun handle_leaf call thy srls E a v t =
1.82 - (*WN050916 'upd_env_opt' is a blind copy from previous version*)
1.83 - case subst_stacexpr E a v t of
1.84 - (a', STac stac) => (*script-tactic*)
1.85 - let val stac' = eval_listexpr_ (assoc_thy thy) srls
1.86 - (subst_atomic (upd_env_opt E (a,v)) stac)
1.87 - in (if (!trace_script)
1.88 - then tracing ("@@@ "^call^" leaf '"^term2str t^"' ---> STac '"^
1.89 - term2str stac'^"'")
1.90 - else ();
1.91 - (a', STac stac'))
1.92 - end
1.93 - | (a', Expr lexpr) => (*leaf-expression*)
1.94 - let val lexpr' = eval_listexpr_ (assoc_thy thy) srls
1.95 - (subst_atomic (upd_env_opt E (a,v)) lexpr)
1.96 - in (if (!trace_script)
1.97 - then tracing("@@@ "^call^" leaf '"^term2str t^"' ---> Expr '"^
1.98 - term2str lexpr'^"'")
1.99 - else ();
1.100 - (a', Expr lexpr'))
1.101 - end;
1.102 -
1.103 + (*WN050916 'upd_env_opt' is a blind copy from previous version*)
1.104 + case subst_stacexpr E a v t of
1.105 + (a', STac stac) => (*script-tactic*)
1.106 + let val stac' =
1.107 + eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac)
1.108 + in
1.109 + (if (!trace_script)
1.110 + then tracing ("@@@ "^call^" leaf '"^term2str t^"' ---> STac '"^term2str stac'^"'")
1.111 + else ();
1.112 + (a', STac stac'))
1.113 + end
1.114 + | (a', Expr lexpr) => (*leaf-expression*)
1.115 + let val lexpr' =
1.116 + eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) lexpr)
1.117 + in
1.118 + (if (!trace_script)
1.119 + then tracing("@@@ "^call^" leaf '"^term2str t^"' ---> Expr '"^term2str lexpr'^"'")
1.120 + else ();
1.121 + (a', Expr lexpr'))
1.122 + end;
1.123
1.124
1.125 (** locate an applicable stactic in a script **)
1.126 @@ -927,167 +925,114 @@
1.127 astep_up does only get to the parentnode of the scriptexpr.
1.128 consequence:
1.129 * call of (2) means _always_ that in this branch below
1.130 - there was an appl.stac (Repeat, Or e1, ...)
1.131 + there was an appl.stac (Repeat, Or e1, ...) found by the previous step.
1.132 *)
1.133 -fun assy ya (is as (E,l,a,v,S,b),ss)
1.134 - (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))) =
1.135 -(* val (ya, (is as (E,l,a,v,S,b),ss),Const ("HOL.Let",_) $ e $ (Abs (id,T,body))) =
1.136 - (*1*)(((ts,d),Aundef), ((E,[R],a,v,S,b),[(m,EmptyMout,pt,p,[])]), body);
1.137 - *)
1.138 - ((*tracing("### assy Let$e$Abs: is=");
1.139 - tracing(istate2str (ScrState is));*)
1.140 - case assy ya ((E , l@[L,R], a,v,S,b),ss) e of
1.141 - NasApp ((E',l,a,v,S,bb),ss) =>
1.142 - let val id' = mk_Free (id, T);
1.143 - val E' = upd_env E' (id', v);
1.144 - (*val _=tracing("### assy Let -> NasApp");*)
1.145 - in assy ya ((E', l@[R,D], a,v,S,b),ss) body end
1.146 - | NasNap (v,E) =>
1.147 - let val id' = mk_Free (id, T);
1.148 - val E' = upd_env E (id', v);
1.149 - (*val _=tracing("### assy Let -> NasNap");*)
1.150 - in assy ya ((E', l@[R,D], a,v,S,b),ss) body end
1.151 - | ay => ay)
1.152 +fun assy ya (is as (E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))) =
1.153 + (case assy ya ((E , l@[L,R], a,v,S,b),ss) e of
1.154 + NasApp ((E',l,a,v,S,bb),ss) =>
1.155 + let
1.156 + val id' = mk_Free (id, T);
1.157 + val E' = upd_env E' (id', v);
1.158 + in assy ya ((E', l@[R,D], a,v,S,b),ss) body end
1.159 + | NasNap (v,E) =>
1.160 + let
1.161 + val id' = mk_Free (id, T);
1.162 + val E' = upd_env E (id', v);
1.163 + in assy ya ((E', l@[R,D], a,v,S,b),ss) body end
1.164 + | ay => ay)
1.165
1.166 - | assy (ya as (((thy,srls),_),_)) ((E,l,_,v,S,b),ss)
1.167 - (Const ("Script.While",_) $ c $ e $ a) =
1.168 - ((*tracing("### assy While $ c $ e $ a, upd_env= "^
1.169 - (subst2str (upd_env E (a,v))));*)
1.170 - if eval_true_ thy srls (subst_atomic (upd_env E (a,v)) c)
1.171 - then assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e
1.172 - else NasNap (v, E))
1.173 -
1.174 - | assy (ya as (((thy,srls),_),_)) ((E,l,a,v,S,b),ss)
1.175 - (Const ("Script.While",_) $ c $ e) =
1.176 - ((*tracing("### assy While, l= "^(loc_2str l));*)
1.177 - if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c)
1.178 - then assy ya ((E, l@[R], a,v,S,b),ss) e
1.179 - else NasNap (v, E))
1.180 + | assy (ya as (((thy,srls),_),_)) ((E,l,_,v,S,b),ss) (Const ("Script.While",_) $ c $ e $ a) =
1.181 + (if eval_true_ thy srls (subst_atomic (upd_env E (a,v)) c)
1.182 + then assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e
1.183 + else NasNap (v, E))
1.184 + | assy (ya as (((thy,srls),_),_)) ((E,l,a,v,S,b),ss) (Const ("Script.While",_) $ c $ e) =
1.185 + (if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c)
1.186 + then assy ya ((E, l@[R], a,v,S,b),ss) e
1.187 + else NasNap (v, E))
1.188
1.189 - | assy (ya as (((thy,srls),_),_)) ((E,l,a,v,S,b),ss)
1.190 - (Const ("If",_) $ c $ e1 $ e2) =
1.191 - (if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c)
1.192 - then assy ya ((E, l@[L,R], a,v,S,b),ss) e1
1.193 - else assy ya ((E, l@[ R], a,v,S,b),ss) e2)
1.194 + | assy (ya as (((thy,srls),_),_)) ((E,l,a,v,S,b),ss) (Const ("If",_) $ c $ e1 $ e2) =
1.195 + (if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c)
1.196 + then assy ya ((E, l@[L,R], a,v,S,b),ss) e1
1.197 + else assy ya ((E, l@[ R], a,v,S,b),ss) e2)
1.198
1.199 | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Try",_) $ e $ a) =
1.200 - ((*tracing("### assy Try $ e $ a, l= "^(loc_2str l));*)
1.201 - case assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e of
1.202 - ay => ay)
1.203 + (case assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e of
1.204 + ay => ay)
1.205 + | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Try",_) $ e) =
1.206 + (case assy ya ((E, l@[R], a,v,S,b),ss) e of
1.207 + ay => ay)
1.208
1.209 - | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Try",_) $ e) =
1.210 - ((*tracing("### assy Try $ e, l= "^(loc_2str l));*)
1.211 - case assy ya ((E, l@[R], a,v,S,b),ss) e of
1.212 - ay => ay)
1.213 -(* val (ya, ((E,l,_,v,S,b),ss), (Const ("Script.Seq",_) $e1 $ e2 $ a)) =
1.214 - (*2*)(ya, ((E , l@[L,R], a,v,S,b),ss), e);
1.215 - *)
1.216 | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Seq",_) $e1 $ e2 $ a) =
1.217 - ((*tracing("### assy Seq $e1 $ e2 $ a, E= "^(subst2str E));*)
1.218 - case assy ya ((E, l@[L,L,R], SOME a,v,S,b),ss) e1 of
1.219 - NasNap (v, E) => assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e2
1.220 - | NasApp ((E,_,_,v,_,_),ss) =>
1.221 - assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e2
1.222 + (case assy ya ((E, l@[L,L,R], SOME a,v,S,b),ss) e1 of
1.223 + NasNap (v, E) => assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e2
1.224 + | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e2
1.225 | ay => ay)
1.226 -
1.227 | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Seq",_) $e1 $ e2) =
1.228 - (case assy ya ((E, l@[L,R], a,v,S,b),ss) e1 of
1.229 - NasNap (v, E) => assy ya ((E, l@[R], a,v,S,b),ss) e2
1.230 - | NasApp ((E,_,_,v,_,_),ss) =>
1.231 - assy ya ((E, l@[R], a,v,S,b),ss) e2
1.232 + (case assy ya ((E, l@[L,R], a,v,S,b),ss) e1 of
1.233 + NasNap (v, E) => assy ya ((E, l@[R], a,v,S,b),ss) e2
1.234 + | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l@[R], a,v,S,b),ss) e2
1.235 | ay => ay)
1.236
1.237 | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Repeat",_) $ e $ a) =
1.238 - assy ya ((E,(l@[L,R]),SOME a,v,S,b),ss) e
1.239 + assy ya ((E,(l@[L,R]),SOME a,v,S,b),ss) e
1.240 + | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Repeat",_) $ e) =
1.241 + assy ya ((E,(l@[R]),a,v,S,b),ss) e
1.242
1.243 - | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Repeat",_) $ e) =
1.244 - assy ya ((E,(l@[R]),a,v,S,b),ss) e
1.245 -
1.246 -(*15.6.02: ass,app Or nochmals "uberlegen FIXXXME*)
1.247 | assy (y, Aundef) ((E,l,_,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2 $ a) =
1.248 - (case assy (y, AssOnly) ((E,(l@[L,L,R]),SOME a,v,S,b),ss) e1 of
1.249 - NasNap (v, E) =>
1.250 - (case assy (y, AssOnly) ((E,(l@[L,R]),SOME a,v,S,b),ss) e2 of
1.251 - NasNap (v, E) =>
1.252 - (case assy (y, AssGen) ((E,(l@[L,L,R]),SOME a,v,S,b),ss) e1 of
1.253 + (case assy (y, AssOnly) ((E,(l@[L,L,R]),SOME a,v,S,b),ss) e1 of
1.254 NasNap (v, E) =>
1.255 - assy (y, AssGen) ((E, (l@[L,R]), SOME a,v,S,b),ss) e2
1.256 - | ay => ay)
1.257 - | ay =>(ay))
1.258 + (case assy (y, AssOnly) ((E,(l@[L,R]),SOME a,v,S,b),ss) e2 of
1.259 + NasNap (v, E) =>
1.260 + (case assy (y, AssGen) ((E,(l@[L,L,R]),SOME a,v,S,b),ss) e1 of
1.261 + NasNap (v, E) =>
1.262 + assy (y, AssGen) ((E, (l@[L,R]), SOME a,v,S,b),ss) e2
1.263 + | ay => ay)
1.264 + | ay =>(ay))
1.265 | NasApp _ => error ("assy: FIXXXME ///must not return NasApp///")
1.266 | ay => (ay))
1.267 -
1.268 | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2) =
1.269 - (case assy ya ((E,(l@[L,R]),a,v,S,b),ss) e1 of
1.270 - NasNap (v, E) =>
1.271 - assy ya ((E,(l@[R]),a,v,S,b),ss) e2
1.272 + (case assy ya ((E,(l@[L,R]),a,v,S,b),ss) e1 of
1.273 + NasNap (v, E) => assy ya ((E,(l@[R]),a,v,S,b),ss) e2
1.274 | ay => (ay))
1.275 -(* val ((m,_,pt,(p,p_),c)::ss) = [(m,EmptyMout,pt,p,[])];
1.276 - val t = (term_of o the o (parse (Thy_Info.get_theory "Isac"))) "Rewrite rmult_1 False";
1.277 -
1.278 - val (ap,(p,p_),c,ss) = (Aundef,p,[],[]);
1.279 - assy (((thy',srls),d),ap) ((E,l,a,v,S,b), (m,EmptyMout,pt,(p,p_),c)::ss) t;
1.280 -val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
1.281 - ();
1.282 - *)
1.283
1.284 | assy (((thy',sr),d),ap) (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss) t =
1.285 - ((*tracing("### assy, m = "^tac_2str m);
1.286 - tracing("### assy, (p,p_) = "^pos'2str (p,p_));
1.287 - tracing("### assy, is= ");
1.288 - tracing(istate2str (ScrState is));*)
1.289 - case handle_leaf "locate" thy' sr E a v t of
1.290 - (a', Expr s) =>
1.291 - ((*tracing("### assy: listexpr t= "^(term2str t));
1.292 - tracing("### assy, E= "^(env2str E));
1.293 - tracing("### assy, eval(..)= "^(term2str
1.294 - (eval_listexpr_ (assoc_thy thy') sr
1.295 - (subst_atomic (upd_env_opt E (a',v)) t))));*)
1.296 - NasNap (eval_listexpr_ (assoc_thy thy') sr
1.297 - (subst_atomic (upd_env_opt E (a',v)) t), E))
1.298 - (* val (_,STac stac) = subst_stacexpr E a v t;
1.299 - *)
1.300 - | (a', STac stac) =>
1.301 - let (*val _=tracing("### assy, stac = "^term2str stac);*)
1.302 - val p' = case p_ of Frm => p | Res => lev_on p
1.303 - | _ => error ("assy: call by "^
1.304 - (pos'2str (p,p_)));
1.305 - in case assod pt d m stac of
1.306 - Ass (m,v') =>
1.307 - let (*val _=tracing("### assy: Ass ("^tac_2str m^", "^
1.308 - term2str v'^")");*)
1.309 - val (p'',c',f',pt') = generate1 (assoc_thy thy') m
1.310 - (ScrState (E,l,a',v',S,true), e_ctxt) (p',p_) pt;
1.311 - in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
1.312 - | AssWeak (m,v') =>
1.313 - let (*val _=tracing("### assy: Ass Weak("^tac_2str m^", "^
1.314 - term2str v'^")");*)
1.315 - val (p'',c',f',pt') = generate1 (assoc_thy thy') m
1.316 - (ScrState (E,l,a',v',S,false), e_ctxt) (p',p_) pt;
1.317 - in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
1.318 - | NotAss =>
1.319 - ((*tracing("### assy, NotAss");*)
1.320 - case ap of (*switch for Or: 1st AssOnly, 2nd AssGen*)
1.321 - AssOnly => (NasNap (v, E))
1.322 - | gen => (case applicable_in (p,p_) pt
1.323 - (stac2tac pt (assoc_thy thy') stac) of
1.324 - Appl m' =>
1.325 - let val is = (E,l,a',tac_2res m',S,false(*FIXXXME*))
1.326 - val (p'',c',f',pt') =
1.327 - generate1 (assoc_thy thy') m' (ScrState is, e_ctxt) (p',p_) pt;
1.328 - in NasApp (is,(m,f',pt',p'',c @ c')::ss) end
1.329 - | Notappl _ =>
1.330 - (NasNap (v, E))
1.331 - )
1.332 - )
1.333 - end);
1.334 -(* (astep_up ((thy',scr,d),NasApp_) ((E,l,a,v,S,b),[(m,EmptyMout,pt,p,[])])) handle e => print_exn_G e;
1.335 - *)
1.336 + (case handle_leaf "locate" thy' sr E a v t of
1.337 + (a', Expr s) =>
1.338 + (NasNap (eval_listexpr_ (assoc_thy thy') sr
1.339 + (subst_atomic (upd_env_opt E (a',v)) t), E))
1.340 + | (a', STac stac) =>
1.341 + let
1.342 + val ctxt = get_ctxt pt (p,p_)
1.343 + val p' =
1.344 + case p_ of Frm => p
1.345 + | Res => lev_on p
1.346 + | _ => error ("assy: call by " ^ pos'2str (p,p_));
1.347 + in
1.348 + case assod pt d m stac of
1.349 + Ass (m,v') =>
1.350 + let val (p'',c',f',pt') =
1.351 + generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
1.352 + in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
1.353 + | AssWeak (m,v') =>
1.354 + let val (p'',c',f',pt') =
1.355 + generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,false), ctxt) (p',p_) pt;
1.356 + in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
1.357 + | NotAss =>
1.358 + (case ap of (*switch for Or: 1st AssOnly, 2nd AssGen*)
1.359 + AssOnly => (NasNap (v, E))
1.360 + | gen =>
1.361 + (case applicable_in (p,p_) pt (stac2tac pt (assoc_thy thy') stac) of
1.362 + Appl m' =>
1.363 + let
1.364 + val is = (E,l,a',tac_2res m',S,false(*FIXXXME.WN0?*))
1.365 + val (p'',c',f',pt') =
1.366 + generate1 (assoc_thy thy') m' (ScrState is, ctxt) (p',p_) pt;
1.367 + in NasApp (is,(m,f',pt',p'',c @ c')::ss) end
1.368 + | Notappl _ => (NasNap (v, E))
1.369 + )
1.370 + )
1.371 + end);
1.372
1.373 -
1.374 -(* val (ys as (y,s,Script sc,d),(is as (E,l,a,v,S,b),ss),Const ("HOL.Let",_) $ _) =
1.375 - (ys, ((E,up,a,v,S,b),ss), go up sc);
1.376 - *)
1.377 fun ass_up (ys as (y,s,Script sc,d)) (is as (E,l,a,v,S,b),ss)
1.378 (Const ("HOL.Let",_) $ _) =
1.379 let (*val _= tracing("### ass_up1 Let$e: is=")
1.380 @@ -1694,125 +1639,116 @@
1.381 (.. not true for other details ..PrfObj ??????????????????
1.382 20.8.02: do NOT return safe (is only changed in locate !!!)
1.383 *)
1.384 -(* val (thy, (pt,p), Rfuns {next_rule=ne,...}, RrlsState (f,f',rss,_)) =
1.385 - (thy', (pt,p), sc, RrlsState (ii t));
1.386 - val (thy, (pt,p), Rfuns {next_rule=ne,...}, RrlsState (f,f',rss,_)) =
1.387 - (thy', (pt',p'), sc, is');
1.388 - *)
1.389 -fun next_tac (thy,_) (pt,p) (Rfuns {next_rule,...}) (RrlsState(f,f',rss,_), ctxt)=
1.390 - if f = f' then (End_Detail' (f',[])(*8.6.03*), (Uistate, e_ctxt),
1.391 - (f', Sundef(*FIXME is no value of next_tac! vor 8.6.03*)))
1.392 - (*finished*)
1.393 - else (case next_rule rss f of
1.394 - NONE => (Empty_Tac_, (Uistate, e_ctxt), (e_term, Sundef)) (*helpless*)
1.395 -(* val SOME (Thm (id,thm)) = next_rule rss f;
1.396 - *)
1.397 - | SOME (Thm (id,thm))(*8.6.03: muss auch f' liefern ?!!*) =>
1.398 - (Rewrite' (thy, "e_rew_ord", e_rls,(*!?!8.6.03*) false,
1.399 - (id, string_of_thmI thm), f,(e_term,[(*!?!8.6.03*)])),
1.400 - (Uistate, e_ctxt), (e_term, Sundef))) (*next stac*)
1.401 -
1.402 -(* val(thy, ptp as (pt,(p,_)), sc as Script (h $ body),ScrState (E,l,a,v,s,b))=
1.403 - ((thy',srls), (pt,pos), sc, is);
1.404 - *)
1.405 - | next_tac thy (ptp as (pt,(p,_)):ptree * pos') (sc as Script (h $ body))
1.406 - (ScrState (E,l,a,v,s,b), ctxt) =
1.407 - ((*tracing("### next_tac-----------------: E= ");
1.408 - tracing( istate2str (ScrState (E,l,a,v,s,b)));*)
1.409 - case if l = []
1.410 - then appy thy ptp E [R] body NONE v
1.411 - else nstep_up thy ptp sc E l Skip_ a v of
1.412 - Skip (v, _) => (*finished*)
1.413 - (case par_pbl_det pt p of
1.414 - (true, p', _) =>
1.415 - let val (_,pblID,_) = get_obj g_spec pt p';
1.416 - in (Check_Postcond' (pblID, (v, [(*8.6.03 NO asms???*)])),
1.417 - (e_istate, e_ctxt), (v,s))
1.418 - end
1.419 - | (_, p', rls') =>
1.420 - (End_Detail' (e_term,[])(*8.6.03*), (e_istate, e_ctxt), (v,s)))
1.421 - | Napp _ => (Empty_Tac_, (e_istate, e_ctxt), (e_term, Sundef))(*helpless*)
1.422 - | Appy (m', scrst as (_,_,_,v,_,_)) =>
1.423 - (m', (ScrState scrst, e_ctxt), (v, Sundef))) (*next stac*)
1.424 -
1.425 +fun next_tac (thy,_) (pt,p) (Rfuns {next_rule,...}) (RrlsState(f,f',rss,_), ctxt) =
1.426 + let val ctxt = get_ctxt pt p
1.427 + in
1.428 + if f = f'
1.429 + then (End_Detail' (f',[])(*8.6.03*), (Uistate, ctxt),
1.430 + (f', Sundef(*FIXME is no value of next_tac! vor 8.6.03*))) (*finished*)
1.431 + else
1.432 + (case next_rule rss f of
1.433 + NONE => (Empty_Tac_, (Uistate, ctxt), (e_term, Sundef)) (*helpless*)
1.434 + | SOME (Thm (id,thm))(*8.6.03: muss auch f' liefern ?!!*) =>
1.435 + (Rewrite' (thy, "e_rew_ord", e_rls,(*!?!8.6.03*) false,
1.436 + (id, string_of_thmI thm), f,(e_term,[(*!?!8.6.03*)])),
1.437 + (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
1.438 + end
1.439 + | next_tac thy (ptp as (pt,pos as (p,_)):ptree * pos') (sc as Script (h $ body))
1.440 + (ScrState (E,l,a,v,s,b), ctxt) =
1.441 + let val ctxt = get_ctxt pt pos
1.442 + in
1.443 + (case if l = []
1.444 + then appy thy ptp E [R] body NONE v
1.445 + else nstep_up thy ptp sc E l Skip_ a v of
1.446 + Skip (v, _) => (*finished*)
1.447 + (case par_pbl_det pt p of
1.448 + (true, p', _) =>
1.449 + let val (_,pblID,_) = get_obj g_spec pt p';
1.450 + in (Check_Postcond' (pblID, (v, [(*8.6.03 NO asms???*)])),
1.451 + (e_istate, ctxt), (v,s))
1.452 + end
1.453 + | (_, p', rls') =>
1.454 + (End_Detail' (e_term,[])(*8.6.03*), (e_istate, ctxt), (v,s)))
1.455 + | Napp _ => (Empty_Tac_, (e_istate, ctxt), (e_term, Sundef)) (*helpless*)
1.456 + | Appy (m', scrst as (_,_,_,v,_,_)) =>
1.457 + (m', (ScrState scrst, ctxt), (v, Sundef))) (*next stac*)
1.458 + end
1.459 | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (istate2str is));
1.460
1.461
1.462 (*.create the initial interpreter state from the items of the guard.*)
1.463 -(* val (thy, itms, metID) = (thy, itms, mI);
1.464 - *)
1.465 fun init_scrstate thy itms metID =
1.466 - let val actuals = itms2args thy metID itms;
1.467 - val scr as Script sc = (#scr o get_met) metID;
1.468 - val formals = formal_args sc
1.469 - (*expects same sequence of (actual) args in itms
1.470 - and (formal) args in met*)
1.471 - fun relate_args env [] [] = env
1.472 - | relate_args env _ [] =
1.473 - error ("ERROR in creating the environment for '"
1.474 - ^id_of_scr sc^"' from \nthe items of the guard of "
1.475 - ^metID2str metID^",\n\
1.476 - \formal arg(s), from the script,\
1.477 - \ miss actual arg(s), from the guards env:\n"
1.478 - ^(string_of_int o length) formals
1.479 - ^" formals: "^terms2str formals^"\n"
1.480 - ^(string_of_int o length) actuals
1.481 - ^" actuals: "^terms2str actuals)
1.482 - | relate_args env [] actual_finds = env (*may drop Find!*)
1.483 - | relate_args env (a::aa) (f::ff) =
1.484 - if type_of a = type_of f
1.485 - then relate_args (env @ [(a, f)]) aa ff else
1.486 - error ("ERROR in creating the environment for '"
1.487 - ^id_of_scr sc^"' from \nthe items of the guard of "
1.488 - ^metID2str metID^",\n\
1.489 - \different types of formal arg, from the script,\
1.490 - \ and actual arg, from the guards env:'\n\
1.491 - \formal: '"^term2str a^"::"^(type2str o type_of) a^"'\n\
1.492 - \actual: '"^term2str f^"::"^(type2str o type_of) f^"'\n\
1.493 - \in\n\
1.494 - \formals: "^terms2str formals^"\n\
1.495 - \actuals: "^terms2str actuals)
1.496 - val env = relate_args [] formals actuals;
1.497 - in (ScrState (env,[],NONE,e_term,Safe,true), e_ctxt, scr):istate * Proof.context * scr end;
1.498 + let
1.499 + val actuals = itms2args thy metID itms;
1.500 + val scr as Script sc = (#scr o get_met) metID;
1.501 + val formals = formal_args sc
1.502 + (*expects same sequence of (actual) args in itms and (formal) args in met*)
1.503 + fun relate_args env [] [] = env
1.504 + | relate_args env _ [] =
1.505 + error ("ERROR in creating the environment for '" ^
1.506 + id_of_scr sc ^ "' from \nthe items of the guard of " ^
1.507 + metID2str metID ^ ",\n" ^
1.508 + "formal arg(s), from the script, miss actual arg(s), from the guards env:\n" ^
1.509 + (string_of_int o length) formals ^
1.510 + " formals: " ^ terms2str formals ^ "\n" ^
1.511 + (string_of_int o length) actuals ^
1.512 + " actuals: " ^ terms2str actuals)
1.513 + | relate_args env [] actual_finds = env (*may drop Find!*)
1.514 + | relate_args env (a::aa) (f::ff) =
1.515 + if type_of a = type_of f
1.516 + then relate_args (env @ [(a, f)]) aa ff
1.517 + else
1.518 + error ("ERROR in creating the environment for '" ^
1.519 + id_of_scr sc ^ "' from \nthe items of the guard of " ^
1.520 + metID2str metID ^ ",\n" ^
1.521 + "different types of formal arg, from the script, " ^
1.522 + "and actual arg, from the guards env:'\n" ^
1.523 + "formal: '" ^ term2str a ^ "::" ^ (type2str o type_of) a ^ "'\n" ^
1.524 + "actual: '" ^ term2str f ^ "::" ^ (type2str o type_of) f ^ "'\n" ^
1.525 + "in\n" ^
1.526 + "formals: " ^ terms2str formals ^ "\n" ^
1.527 + "actuals: " ^ terms2str actuals)
1.528 + val env = relate_args [] formals actuals;
1.529 + in (ScrState (env,[],NONE,e_term,Safe,true), e_ctxt, scr):istate * Proof.context * scr end;
1.530
1.531 -(*.decide, where to get script/istate from:
1.532 +(* decide, where to get script/istate from:
1.533 (*1*) from PblObj.env: at begin of script if no init_form
1.534 (*2*) from PblObj/PrfObj: if stac is in the middle of the script
1.535 - (*3*) from rls/PrfObj: in case of detail a ruleset.*)
1.536 -(* val (thy', (p,p_), pt) = (thy', (p,p_), pt);
1.537 - *)
1.538 + (*3*) from rls/PrfObj: in case of detail a ruleset *)
1.539 fun from_pblobj_or_detail' thy' (p,p_) pt =
1.540 + let val ctxt = get_ctxt pt (p,p_)
1.541 + in
1.542 if member op = [Pbl,Met] p_
1.543 then case get_obj g_env pt p of
1.544 - NONE => error "from_pblobj_or_detail': no istate"
1.545 - | SOME is =>
1.546 - let val metID = get_obj g_metID pt p
1.547 - val {srls,...} = get_met metID
1.548 - in (srls, is, (#scr o get_met) metID) end
1.549 + NONE => error "from_pblobj_or_detail': no istate"
1.550 + | SOME is =>
1.551 + let
1.552 + val metID = get_obj g_metID pt p
1.553 + val {srls,...} = get_met metID
1.554 + in (srls, is, (#scr o get_met) metID) end
1.555 else
1.556 - let val (pbl,p',rls') = par_pbl_det pt p
1.557 - in if pbl
1.558 - then (*2*)
1.559 - let val thy = assoc_thy thy'
1.560 - val PblObj{meth=itms,...} = get_obj I pt p'
1.561 - val metID = get_obj g_metID pt p'
1.562 - val {srls,...} = get_met metID
1.563 - in (*if last_elem p = 0 (*nothing written to pt yet*)
1.564 - then let val (is, ctxt, sc) = init_scrstate thy itms metID
1.565 - in (srls, is, sc) end
1.566 - else*) (srls, get_loc pt (p,p_), (#scr o get_met) metID)
1.567 - end
1.568 - else (*3*)
1.569 - (e_rls, (*FIXME: get from pbl or met !!!
1.570 - unused for Rrls in locate_gen, next_tac*)
1.571 - get_loc pt (p,p_),
1.572 - case rls' of
1.573 - Rls {scr=scr,...} => scr
1.574 - | Seq {scr=scr,...} => scr
1.575 - | Rrls {scr=rfuns,...} => rfuns)
1.576 - end;
1.577 + let val (pbl,p',rls') = par_pbl_det pt p
1.578 + in if pbl
1.579 + then (*2*)
1.580 + let
1.581 + val thy = assoc_thy thy'
1.582 + val PblObj{meth=itms,...} = get_obj I pt p'
1.583 + val metID = get_obj g_metID pt p'
1.584 + val {srls,...} = get_met metID
1.585 + in (*if last_elem p = 0 nothing written to pt yet*)
1.586 + (srls, get_loc pt (p,p_), (#scr o get_met) metID)
1.587 + end
1.588 + else (*3*)
1.589 + (e_rls, (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in locate_gen, next_tac*)
1.590 + get_loc pt (p,p_),
1.591 + case rls' of
1.592 + Rls {scr=scr,...} => scr
1.593 + | Seq {scr=scr,...} => scr
1.594 + | Rrls {scr=rfuns,...} => rfuns)
1.595 + end
1.596 + end;
1.597
1.598 -(*.get script and istate from PblObj, see (*1*) above.*)
1.599 +(*.get script and istate from PblObj, see (*1*) above.*)
1.600 fun from_pblobj' thy' (p,p_) pt =
1.601 let val p' = par_pblobj pt p
1.602 val thy = assoc_thy thy'