1.1 --- a/src/Tools/isac/Interpret/ctree.sml Sun May 15 13:59:05 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/ctree.sml Tue May 17 09:55:30 2011 +0200
1.3 @@ -256,23 +256,11 @@
1.4 only used during ass_dn/up*)
1.5 val e_scrstate = ([],[],NONE,e_term,Sundef,false):scrstate;
1.6
1.7 -
1.8 -(*21.8.02 ---> definitions.sml for datatype scr
1.9 -type rrlsstate = (*state for reverse rewriting*)
1.10 - (term * (*the current formula*)
1.11 - rule list (*of reverse rewrite set (#1#)*)
1.12 - list * (*may be serveral, eg. in norm_rational*)
1.13 - (rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
1.14 - (term * (*... rewrite with ...*)
1.15 - term list)) (*... assumptions*)
1.16 - list); (*derivation from given term to normalform
1.17 - in reverse order with sym_thm;
1.18 - (#1#) could be extracted from here #1*) --------*)
1.19 -
1.20 -datatype istate = (*interpreter state*)
1.21 - Uistate (*undefined in modspec, in '_deriv'ation*)
1.22 - | ScrState of scrstate (*for script interpreter*)
1.23 - | RrlsState of rrlsstate; (*for reverse rewriting*)
1.24 +(* for handling type istate see fun from_pblobj_or_detail', +? *)
1.25 +datatype istate = (*interpreter state*)
1.26 + Uistate (*undefined in modspec, in '_deriv'ation*)
1.27 + | ScrState of scrstate (*for script interpreter*)
1.28 + | RrlsState of rrlsstate; (*for reverse rewriting*)
1.29 val e_istate = (ScrState ([],[],NONE,e_term,Sundef,false)):istate;
1.30 val e_ctxt = ProofContext.init_global @{theory "Pure"};
1.31
1.32 @@ -1280,7 +1268,8 @@
1.33 1.00 not used anymore*)
1.34
1.35 (*FIXME.WN.12.03: update_X X pos pt -> pt could be chained by o (efficiency?)*)
1.36 -fun update_ctxt pt pos x = appl_obj (repl_ctxt x) pt pos;
1.37 +fun update_ctxt pt pos x = appl_obj (repl_ctxt x) pt pos; (*for use on PblObj,
1.38 +otherwise use generate1; compare fun get_ctxt*)
1.39 fun update_env pt pos x = appl_obj (repl_env x) pt pos;
1.40 fun update_domID pt pos x = appl_obj (repl_domID x) pt pos;
1.41 fun update_pblID pt pos x = appl_obj (repl_pblID x) pt pos;
2.1 --- a/src/Tools/isac/Interpret/script.sml Sun May 15 13:59:05 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/script.sml Tue May 17 09:55:30 2011 +0200
2.3 @@ -65,22 +65,24 @@
2.4 (*.makes a (rule,term) list to a Step (m, mout, pt', p', cid) for solve;
2.5 complicated with current t in rrlsstate.*)
2.6 fun rts2steps steps ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) [(r, (f', am))] =
2.7 - let val thy = assoc_thy thy'
2.8 - val m = Rewrite' (thy',ro,er,pa, rule2thm' r, f, (f', am))
2.9 - val is = RrlsState (f',f'',rss,rts)
2.10 - val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)
2.11 - val (p', cid, mout, pt') = generate1 thy m (is, e_ctxt) p pt
2.12 - in (is, (m, mout, pt', p', cid)::steps) end
2.13 - | rts2steps steps ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa))
2.14 - ((r, (f', am))::rts') =
2.15 - let val thy = assoc_thy thy'
2.16 - val m = Rewrite' (thy',ro,er,pa, rule2thm' r, f, (f', am))
2.17 - val is = RrlsState (f',f'',rss,rts)
2.18 - val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)
2.19 - val (p', cid, mout, pt') = generate1 thy m (is, e_ctxt) p pt
2.20 - in rts2steps ((m, mout, pt', p', cid)::steps)
2.21 - ((pt',p'),(f',f'',rss,rts),(thy',ro,er,pa)) rts' end;
2.22 -
2.23 + let
2.24 + val thy = assoc_thy thy'
2.25 + val ctxt = get_ctxt pt p |> insert_assumptions am
2.26 + val m = Rewrite' (thy', ro, er, pa, rule2thm' r, f, (f', am))
2.27 + val is = RrlsState (f', f'', rss, rts)
2.28 + val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)
2.29 + val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt
2.30 + in (is, (m, mout, pt', p', cid) :: steps) end
2.31 + | rts2steps steps ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) ((r, (f', am))::rts') =
2.32 + let
2.33 + val thy = assoc_thy thy'
2.34 + val ctxt = get_ctxt pt p |> insert_assumptions am
2.35 + val m = Rewrite' (thy',ro,er,pa, rule2thm' r, f, (f', am))
2.36 + val is = RrlsState (f',f'',rss,rts)
2.37 + val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)
2.38 + val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt
2.39 + in rts2steps ((m, mout, pt', p', cid)::steps)
2.40 + ((pt',p'),(f',f'',rss,rts),(thy',ro,er,pa)) rts' end;
2.41
2.42 (*. functions for the environment stack .*)
2.43 fun accessenv id es = the (assoc((top es):env, id))
2.44 @@ -261,20 +263,18 @@
2.45 (*.get the identifier of the script out of the scripts parsetree.*)
2.46 fun id_of_scr sc = (id_of o fst o strip_comb) sc;
2.47
2.48 -
2.49 (*WN020526: not clear, when a is available in ass_up for eva-_true*)
2.50 (*WN060906: in "fun handle_leaf" eg. uses "SOME M__"(from some PREVIOUS
2.51 curried Rewrite) for CURRENT value (which may be different from PREVIOUS);
2.52 thus "NONE" must be set at the end of currying (ill designed anyway)*)
2.53 fun upd_env_opt env (SOME a, v) = upd_env env (a,v)
2.54 | upd_env_opt env (NONE, v) =
2.55 - (tracing("*** upd_env_opt: (NONE,"^(term2str v)^")");env);
2.56 -
2.57 + (tracing ("*** upd_env_opt: (NONE," ^ term2str v ^ ")"); env);
2.58
2.59 type dsc = typ; (*<-> nam..unknow in Descript.thy*)
2.60 fun typ_str (Type (s,_)) = s
2.61 | typ_str (TFree(s,_)) = s
2.62 - | typ_str (TVar ((s,i),_)) = s^(string_of_int i);
2.63 + | typ_str (TVar ((s,i),_)) = s ^ (string_of_int i);
2.64
2.65 (*get the _result_-type of a description*)
2.66 fun dsc_valT (Const (_,(Type (_,[_,T])))) = (strip_thy o typ_str) T;
2.67 @@ -859,36 +859,34 @@
2.68 FIXXXXME: simplify rep_tac_*)
2.69
2.70
2.71 -(*.handle a leaf;
2.72 +(* handle a leaf at the end of recursive descent:
2.73 a leaf is either a tactic or an 'exp' in 'let v = expr'
2.74 where 'exp' does not contain a tactic.
2.75 handling a leaf comprises
2.76 (1) 'subst_stacexpr' substitute env and complete curried tactic
2.77 (2) rewrite the leaf by 'srls'
2.78 -WN060906 quick and dirty fix: return a' too (for updating E later)
2.79 -.*)
2.80 +*)
2.81 fun handle_leaf call thy srls E a v t =
2.82 - (*WN050916 'upd_env_opt' is a blind copy from previous version*)
2.83 - case subst_stacexpr E a v t of
2.84 - (a', STac stac) => (*script-tactic*)
2.85 - let val stac' = eval_listexpr_ (assoc_thy thy) srls
2.86 - (subst_atomic (upd_env_opt E (a,v)) stac)
2.87 - in (if (!trace_script)
2.88 - then tracing ("@@@ "^call^" leaf '"^term2str t^"' ---> STac '"^
2.89 - term2str stac'^"'")
2.90 - else ();
2.91 - (a', STac stac'))
2.92 - end
2.93 - | (a', Expr lexpr) => (*leaf-expression*)
2.94 - let val lexpr' = eval_listexpr_ (assoc_thy thy) srls
2.95 - (subst_atomic (upd_env_opt E (a,v)) lexpr)
2.96 - in (if (!trace_script)
2.97 - then tracing("@@@ "^call^" leaf '"^term2str t^"' ---> Expr '"^
2.98 - term2str lexpr'^"'")
2.99 - else ();
2.100 - (a', Expr lexpr'))
2.101 - end;
2.102 -
2.103 + (*WN050916 'upd_env_opt' is a blind copy from previous version*)
2.104 + case subst_stacexpr E a v t of
2.105 + (a', STac stac) => (*script-tactic*)
2.106 + let val stac' =
2.107 + eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac)
2.108 + in
2.109 + (if (!trace_script)
2.110 + then tracing ("@@@ "^call^" leaf '"^term2str t^"' ---> STac '"^term2str stac'^"'")
2.111 + else ();
2.112 + (a', STac stac'))
2.113 + end
2.114 + | (a', Expr lexpr) => (*leaf-expression*)
2.115 + let val lexpr' =
2.116 + eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) lexpr)
2.117 + in
2.118 + (if (!trace_script)
2.119 + then tracing("@@@ "^call^" leaf '"^term2str t^"' ---> Expr '"^term2str lexpr'^"'")
2.120 + else ();
2.121 + (a', Expr lexpr'))
2.122 + end;
2.123
2.124
2.125 (** locate an applicable stactic in a script **)
2.126 @@ -927,167 +925,114 @@
2.127 astep_up does only get to the parentnode of the scriptexpr.
2.128 consequence:
2.129 * call of (2) means _always_ that in this branch below
2.130 - there was an appl.stac (Repeat, Or e1, ...)
2.131 + there was an appl.stac (Repeat, Or e1, ...) found by the previous step.
2.132 *)
2.133 -fun assy ya (is as (E,l,a,v,S,b),ss)
2.134 - (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))) =
2.135 -(* val (ya, (is as (E,l,a,v,S,b),ss),Const ("HOL.Let",_) $ e $ (Abs (id,T,body))) =
2.136 - (*1*)(((ts,d),Aundef), ((E,[R],a,v,S,b),[(m,EmptyMout,pt,p,[])]), body);
2.137 - *)
2.138 - ((*tracing("### assy Let$e$Abs: is=");
2.139 - tracing(istate2str (ScrState is));*)
2.140 - case assy ya ((E , l@[L,R], a,v,S,b),ss) e of
2.141 - NasApp ((E',l,a,v,S,bb),ss) =>
2.142 - let val id' = mk_Free (id, T);
2.143 - val E' = upd_env E' (id', v);
2.144 - (*val _=tracing("### assy Let -> NasApp");*)
2.145 - in assy ya ((E', l@[R,D], a,v,S,b),ss) body end
2.146 - | NasNap (v,E) =>
2.147 - let val id' = mk_Free (id, T);
2.148 - val E' = upd_env E (id', v);
2.149 - (*val _=tracing("### assy Let -> NasNap");*)
2.150 - in assy ya ((E', l@[R,D], a,v,S,b),ss) body end
2.151 - | ay => ay)
2.152 +fun assy ya (is as (E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))) =
2.153 + (case assy ya ((E , l@[L,R], a,v,S,b),ss) e of
2.154 + NasApp ((E',l,a,v,S,bb),ss) =>
2.155 + let
2.156 + val id' = mk_Free (id, T);
2.157 + val E' = upd_env E' (id', v);
2.158 + in assy ya ((E', l@[R,D], a,v,S,b),ss) body end
2.159 + | NasNap (v,E) =>
2.160 + let
2.161 + val id' = mk_Free (id, T);
2.162 + val E' = upd_env E (id', v);
2.163 + in assy ya ((E', l@[R,D], a,v,S,b),ss) body end
2.164 + | ay => ay)
2.165
2.166 - | assy (ya as (((thy,srls),_),_)) ((E,l,_,v,S,b),ss)
2.167 - (Const ("Script.While",_) $ c $ e $ a) =
2.168 - ((*tracing("### assy While $ c $ e $ a, upd_env= "^
2.169 - (subst2str (upd_env E (a,v))));*)
2.170 - if eval_true_ thy srls (subst_atomic (upd_env E (a,v)) c)
2.171 - then assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e
2.172 - else NasNap (v, E))
2.173 -
2.174 - | assy (ya as (((thy,srls),_),_)) ((E,l,a,v,S,b),ss)
2.175 - (Const ("Script.While",_) $ c $ e) =
2.176 - ((*tracing("### assy While, l= "^(loc_2str l));*)
2.177 - if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c)
2.178 - then assy ya ((E, l@[R], a,v,S,b),ss) e
2.179 - else NasNap (v, E))
2.180 + | assy (ya as (((thy,srls),_),_)) ((E,l,_,v,S,b),ss) (Const ("Script.While",_) $ c $ e $ a) =
2.181 + (if eval_true_ thy srls (subst_atomic (upd_env E (a,v)) c)
2.182 + then assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e
2.183 + else NasNap (v, E))
2.184 + | assy (ya as (((thy,srls),_),_)) ((E,l,a,v,S,b),ss) (Const ("Script.While",_) $ c $ e) =
2.185 + (if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c)
2.186 + then assy ya ((E, l@[R], a,v,S,b),ss) e
2.187 + else NasNap (v, E))
2.188
2.189 - | assy (ya as (((thy,srls),_),_)) ((E,l,a,v,S,b),ss)
2.190 - (Const ("If",_) $ c $ e1 $ e2) =
2.191 - (if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c)
2.192 - then assy ya ((E, l@[L,R], a,v,S,b),ss) e1
2.193 - else assy ya ((E, l@[ R], a,v,S,b),ss) e2)
2.194 + | assy (ya as (((thy,srls),_),_)) ((E,l,a,v,S,b),ss) (Const ("If",_) $ c $ e1 $ e2) =
2.195 + (if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c)
2.196 + then assy ya ((E, l@[L,R], a,v,S,b),ss) e1
2.197 + else assy ya ((E, l@[ R], a,v,S,b),ss) e2)
2.198
2.199 | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Try",_) $ e $ a) =
2.200 - ((*tracing("### assy Try $ e $ a, l= "^(loc_2str l));*)
2.201 - case assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e of
2.202 - ay => ay)
2.203 + (case assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e of
2.204 + ay => ay)
2.205 + | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Try",_) $ e) =
2.206 + (case assy ya ((E, l@[R], a,v,S,b),ss) e of
2.207 + ay => ay)
2.208
2.209 - | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Try",_) $ e) =
2.210 - ((*tracing("### assy Try $ e, l= "^(loc_2str l));*)
2.211 - case assy ya ((E, l@[R], a,v,S,b),ss) e of
2.212 - ay => ay)
2.213 -(* val (ya, ((E,l,_,v,S,b),ss), (Const ("Script.Seq",_) $e1 $ e2 $ a)) =
2.214 - (*2*)(ya, ((E , l@[L,R], a,v,S,b),ss), e);
2.215 - *)
2.216 | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Seq",_) $e1 $ e2 $ a) =
2.217 - ((*tracing("### assy Seq $e1 $ e2 $ a, E= "^(subst2str E));*)
2.218 - case assy ya ((E, l@[L,L,R], SOME a,v,S,b),ss) e1 of
2.219 - NasNap (v, E) => assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e2
2.220 - | NasApp ((E,_,_,v,_,_),ss) =>
2.221 - assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e2
2.222 + (case assy ya ((E, l@[L,L,R], SOME a,v,S,b),ss) e1 of
2.223 + NasNap (v, E) => assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e2
2.224 + | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e2
2.225 | ay => ay)
2.226 -
2.227 | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Seq",_) $e1 $ e2) =
2.228 - (case assy ya ((E, l@[L,R], a,v,S,b),ss) e1 of
2.229 - NasNap (v, E) => assy ya ((E, l@[R], a,v,S,b),ss) e2
2.230 - | NasApp ((E,_,_,v,_,_),ss) =>
2.231 - assy ya ((E, l@[R], a,v,S,b),ss) e2
2.232 + (case assy ya ((E, l@[L,R], a,v,S,b),ss) e1 of
2.233 + NasNap (v, E) => assy ya ((E, l@[R], a,v,S,b),ss) e2
2.234 + | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l@[R], a,v,S,b),ss) e2
2.235 | ay => ay)
2.236
2.237 | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Repeat",_) $ e $ a) =
2.238 - assy ya ((E,(l@[L,R]),SOME a,v,S,b),ss) e
2.239 + assy ya ((E,(l@[L,R]),SOME a,v,S,b),ss) e
2.240 + | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Repeat",_) $ e) =
2.241 + assy ya ((E,(l@[R]),a,v,S,b),ss) e
2.242
2.243 - | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Repeat",_) $ e) =
2.244 - assy ya ((E,(l@[R]),a,v,S,b),ss) e
2.245 -
2.246 -(*15.6.02: ass,app Or nochmals "uberlegen FIXXXME*)
2.247 | assy (y, Aundef) ((E,l,_,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2 $ a) =
2.248 - (case assy (y, AssOnly) ((E,(l@[L,L,R]),SOME a,v,S,b),ss) e1 of
2.249 - NasNap (v, E) =>
2.250 - (case assy (y, AssOnly) ((E,(l@[L,R]),SOME a,v,S,b),ss) e2 of
2.251 - NasNap (v, E) =>
2.252 - (case assy (y, AssGen) ((E,(l@[L,L,R]),SOME a,v,S,b),ss) e1 of
2.253 + (case assy (y, AssOnly) ((E,(l@[L,L,R]),SOME a,v,S,b),ss) e1 of
2.254 NasNap (v, E) =>
2.255 - assy (y, AssGen) ((E, (l@[L,R]), SOME a,v,S,b),ss) e2
2.256 - | ay => ay)
2.257 - | ay =>(ay))
2.258 + (case assy (y, AssOnly) ((E,(l@[L,R]),SOME a,v,S,b),ss) e2 of
2.259 + NasNap (v, E) =>
2.260 + (case assy (y, AssGen) ((E,(l@[L,L,R]),SOME a,v,S,b),ss) e1 of
2.261 + NasNap (v, E) =>
2.262 + assy (y, AssGen) ((E, (l@[L,R]), SOME a,v,S,b),ss) e2
2.263 + | ay => ay)
2.264 + | ay =>(ay))
2.265 | NasApp _ => error ("assy: FIXXXME ///must not return NasApp///")
2.266 | ay => (ay))
2.267 -
2.268 | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2) =
2.269 - (case assy ya ((E,(l@[L,R]),a,v,S,b),ss) e1 of
2.270 - NasNap (v, E) =>
2.271 - assy ya ((E,(l@[R]),a,v,S,b),ss) e2
2.272 + (case assy ya ((E,(l@[L,R]),a,v,S,b),ss) e1 of
2.273 + NasNap (v, E) => assy ya ((E,(l@[R]),a,v,S,b),ss) e2
2.274 | ay => (ay))
2.275 -(* val ((m,_,pt,(p,p_),c)::ss) = [(m,EmptyMout,pt,p,[])];
2.276 - val t = (term_of o the o (parse (Thy_Info.get_theory "Isac"))) "Rewrite rmult_1 False";
2.277 -
2.278 - val (ap,(p,p_),c,ss) = (Aundef,p,[],[]);
2.279 - assy (((thy',srls),d),ap) ((E,l,a,v,S,b), (m,EmptyMout,pt,(p,p_),c)::ss) t;
2.280 -val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
2.281 - ();
2.282 - *)
2.283
2.284 | assy (((thy',sr),d),ap) (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss) t =
2.285 - ((*tracing("### assy, m = "^tac_2str m);
2.286 - tracing("### assy, (p,p_) = "^pos'2str (p,p_));
2.287 - tracing("### assy, is= ");
2.288 - tracing(istate2str (ScrState is));*)
2.289 - case handle_leaf "locate" thy' sr E a v t of
2.290 - (a', Expr s) =>
2.291 - ((*tracing("### assy: listexpr t= "^(term2str t));
2.292 - tracing("### assy, E= "^(env2str E));
2.293 - tracing("### assy, eval(..)= "^(term2str
2.294 - (eval_listexpr_ (assoc_thy thy') sr
2.295 - (subst_atomic (upd_env_opt E (a',v)) t))));*)
2.296 - NasNap (eval_listexpr_ (assoc_thy thy') sr
2.297 - (subst_atomic (upd_env_opt E (a',v)) t), E))
2.298 - (* val (_,STac stac) = subst_stacexpr E a v t;
2.299 - *)
2.300 - | (a', STac stac) =>
2.301 - let (*val _=tracing("### assy, stac = "^term2str stac);*)
2.302 - val p' = case p_ of Frm => p | Res => lev_on p
2.303 - | _ => error ("assy: call by "^
2.304 - (pos'2str (p,p_)));
2.305 - in case assod pt d m stac of
2.306 - Ass (m,v') =>
2.307 - let (*val _=tracing("### assy: Ass ("^tac_2str m^", "^
2.308 - term2str v'^")");*)
2.309 - val (p'',c',f',pt') = generate1 (assoc_thy thy') m
2.310 - (ScrState (E,l,a',v',S,true), e_ctxt) (p',p_) pt;
2.311 - in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
2.312 - | AssWeak (m,v') =>
2.313 - let (*val _=tracing("### assy: Ass Weak("^tac_2str m^", "^
2.314 - term2str v'^")");*)
2.315 - val (p'',c',f',pt') = generate1 (assoc_thy thy') m
2.316 - (ScrState (E,l,a',v',S,false), e_ctxt) (p',p_) pt;
2.317 - in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
2.318 - | NotAss =>
2.319 - ((*tracing("### assy, NotAss");*)
2.320 - case ap of (*switch for Or: 1st AssOnly, 2nd AssGen*)
2.321 - AssOnly => (NasNap (v, E))
2.322 - | gen => (case applicable_in (p,p_) pt
2.323 - (stac2tac pt (assoc_thy thy') stac) of
2.324 - Appl m' =>
2.325 - let val is = (E,l,a',tac_2res m',S,false(*FIXXXME*))
2.326 - val (p'',c',f',pt') =
2.327 - generate1 (assoc_thy thy') m' (ScrState is, e_ctxt) (p',p_) pt;
2.328 - in NasApp (is,(m,f',pt',p'',c @ c')::ss) end
2.329 - | Notappl _ =>
2.330 - (NasNap (v, E))
2.331 - )
2.332 - )
2.333 - end);
2.334 -(* (astep_up ((thy',scr,d),NasApp_) ((E,l,a,v,S,b),[(m,EmptyMout,pt,p,[])])) handle e => print_exn_G e;
2.335 - *)
2.336 + (case handle_leaf "locate" thy' sr E a v t of
2.337 + (a', Expr s) =>
2.338 + (NasNap (eval_listexpr_ (assoc_thy thy') sr
2.339 + (subst_atomic (upd_env_opt E (a',v)) t), E))
2.340 + | (a', STac stac) =>
2.341 + let
2.342 + val ctxt = get_ctxt pt (p,p_)
2.343 + val p' =
2.344 + case p_ of Frm => p
2.345 + | Res => lev_on p
2.346 + | _ => error ("assy: call by " ^ pos'2str (p,p_));
2.347 + in
2.348 + case assod pt d m stac of
2.349 + Ass (m,v') =>
2.350 + let val (p'',c',f',pt') =
2.351 + generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
2.352 + in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
2.353 + | AssWeak (m,v') =>
2.354 + let val (p'',c',f',pt') =
2.355 + generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,false), ctxt) (p',p_) pt;
2.356 + in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
2.357 + | NotAss =>
2.358 + (case ap of (*switch for Or: 1st AssOnly, 2nd AssGen*)
2.359 + AssOnly => (NasNap (v, E))
2.360 + | gen =>
2.361 + (case applicable_in (p,p_) pt (stac2tac pt (assoc_thy thy') stac) of
2.362 + Appl m' =>
2.363 + let
2.364 + val is = (E,l,a',tac_2res m',S,false(*FIXXXME.WN0?*))
2.365 + val (p'',c',f',pt') =
2.366 + generate1 (assoc_thy thy') m' (ScrState is, ctxt) (p',p_) pt;
2.367 + in NasApp (is,(m,f',pt',p'',c @ c')::ss) end
2.368 + | Notappl _ => (NasNap (v, E))
2.369 + )
2.370 + )
2.371 + end);
2.372
2.373 -
2.374 -(* val (ys as (y,s,Script sc,d),(is as (E,l,a,v,S,b),ss),Const ("HOL.Let",_) $ _) =
2.375 - (ys, ((E,up,a,v,S,b),ss), go up sc);
2.376 - *)
2.377 fun ass_up (ys as (y,s,Script sc,d)) (is as (E,l,a,v,S,b),ss)
2.378 (Const ("HOL.Let",_) $ _) =
2.379 let (*val _= tracing("### ass_up1 Let$e: is=")
2.380 @@ -1694,125 +1639,116 @@
2.381 (.. not true for other details ..PrfObj ??????????????????
2.382 20.8.02: do NOT return safe (is only changed in locate !!!)
2.383 *)
2.384 -(* val (thy, (pt,p), Rfuns {next_rule=ne,...}, RrlsState (f,f',rss,_)) =
2.385 - (thy', (pt,p), sc, RrlsState (ii t));
2.386 - val (thy, (pt,p), Rfuns {next_rule=ne,...}, RrlsState (f,f',rss,_)) =
2.387 - (thy', (pt',p'), sc, is');
2.388 - *)
2.389 -fun next_tac (thy,_) (pt,p) (Rfuns {next_rule,...}) (RrlsState(f,f',rss,_), ctxt)=
2.390 - if f = f' then (End_Detail' (f',[])(*8.6.03*), (Uistate, e_ctxt),
2.391 - (f', Sundef(*FIXME is no value of next_tac! vor 8.6.03*)))
2.392 - (*finished*)
2.393 - else (case next_rule rss f of
2.394 - NONE => (Empty_Tac_, (Uistate, e_ctxt), (e_term, Sundef)) (*helpless*)
2.395 -(* val SOME (Thm (id,thm)) = next_rule rss f;
2.396 - *)
2.397 - | SOME (Thm (id,thm))(*8.6.03: muss auch f' liefern ?!!*) =>
2.398 - (Rewrite' (thy, "e_rew_ord", e_rls,(*!?!8.6.03*) false,
2.399 - (id, string_of_thmI thm), f,(e_term,[(*!?!8.6.03*)])),
2.400 - (Uistate, e_ctxt), (e_term, Sundef))) (*next stac*)
2.401 -
2.402 -(* val(thy, ptp as (pt,(p,_)), sc as Script (h $ body),ScrState (E,l,a,v,s,b))=
2.403 - ((thy',srls), (pt,pos), sc, is);
2.404 - *)
2.405 - | next_tac thy (ptp as (pt,(p,_)):ptree * pos') (sc as Script (h $ body))
2.406 - (ScrState (E,l,a,v,s,b), ctxt) =
2.407 - ((*tracing("### next_tac-----------------: E= ");
2.408 - tracing( istate2str (ScrState (E,l,a,v,s,b)));*)
2.409 - case if l = []
2.410 - then appy thy ptp E [R] body NONE v
2.411 - else nstep_up thy ptp sc E l Skip_ a v of
2.412 - Skip (v, _) => (*finished*)
2.413 - (case par_pbl_det pt p of
2.414 - (true, p', _) =>
2.415 - let val (_,pblID,_) = get_obj g_spec pt p';
2.416 - in (Check_Postcond' (pblID, (v, [(*8.6.03 NO asms???*)])),
2.417 - (e_istate, e_ctxt), (v,s))
2.418 - end
2.419 - | (_, p', rls') =>
2.420 - (End_Detail' (e_term,[])(*8.6.03*), (e_istate, e_ctxt), (v,s)))
2.421 - | Napp _ => (Empty_Tac_, (e_istate, e_ctxt), (e_term, Sundef))(*helpless*)
2.422 - | Appy (m', scrst as (_,_,_,v,_,_)) =>
2.423 - (m', (ScrState scrst, e_ctxt), (v, Sundef))) (*next stac*)
2.424 -
2.425 +fun next_tac (thy,_) (pt,p) (Rfuns {next_rule,...}) (RrlsState(f,f',rss,_), ctxt) =
2.426 + let val ctxt = get_ctxt pt p
2.427 + in
2.428 + if f = f'
2.429 + then (End_Detail' (f',[])(*8.6.03*), (Uistate, ctxt),
2.430 + (f', Sundef(*FIXME is no value of next_tac! vor 8.6.03*))) (*finished*)
2.431 + else
2.432 + (case next_rule rss f of
2.433 + NONE => (Empty_Tac_, (Uistate, ctxt), (e_term, Sundef)) (*helpless*)
2.434 + | SOME (Thm (id,thm))(*8.6.03: muss auch f' liefern ?!!*) =>
2.435 + (Rewrite' (thy, "e_rew_ord", e_rls,(*!?!8.6.03*) false,
2.436 + (id, string_of_thmI thm), f,(e_term,[(*!?!8.6.03*)])),
2.437 + (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
2.438 + end
2.439 + | next_tac thy (ptp as (pt,pos as (p,_)):ptree * pos') (sc as Script (h $ body))
2.440 + (ScrState (E,l,a,v,s,b), ctxt) =
2.441 + let val ctxt = get_ctxt pt pos
2.442 + in
2.443 + (case if l = []
2.444 + then appy thy ptp E [R] body NONE v
2.445 + else nstep_up thy ptp sc E l Skip_ a v of
2.446 + Skip (v, _) => (*finished*)
2.447 + (case par_pbl_det pt p of
2.448 + (true, p', _) =>
2.449 + let val (_,pblID,_) = get_obj g_spec pt p';
2.450 + in (Check_Postcond' (pblID, (v, [(*8.6.03 NO asms???*)])),
2.451 + (e_istate, ctxt), (v,s))
2.452 + end
2.453 + | (_, p', rls') =>
2.454 + (End_Detail' (e_term,[])(*8.6.03*), (e_istate, ctxt), (v,s)))
2.455 + | Napp _ => (Empty_Tac_, (e_istate, ctxt), (e_term, Sundef)) (*helpless*)
2.456 + | Appy (m', scrst as (_,_,_,v,_,_)) =>
2.457 + (m', (ScrState scrst, ctxt), (v, Sundef))) (*next stac*)
2.458 + end
2.459 | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (istate2str is));
2.460
2.461
2.462 (*.create the initial interpreter state from the items of the guard.*)
2.463 -(* val (thy, itms, metID) = (thy, itms, mI);
2.464 - *)
2.465 fun init_scrstate thy itms metID =
2.466 - let val actuals = itms2args thy metID itms;
2.467 - val scr as Script sc = (#scr o get_met) metID;
2.468 - val formals = formal_args sc
2.469 - (*expects same sequence of (actual) args in itms
2.470 - and (formal) args in met*)
2.471 - fun relate_args env [] [] = env
2.472 - | relate_args env _ [] =
2.473 - error ("ERROR in creating the environment for '"
2.474 - ^id_of_scr sc^"' from \nthe items of the guard of "
2.475 - ^metID2str metID^",\n\
2.476 - \formal arg(s), from the script,\
2.477 - \ miss actual arg(s), from the guards env:\n"
2.478 - ^(string_of_int o length) formals
2.479 - ^" formals: "^terms2str formals^"\n"
2.480 - ^(string_of_int o length) actuals
2.481 - ^" actuals: "^terms2str actuals)
2.482 - | relate_args env [] actual_finds = env (*may drop Find!*)
2.483 - | relate_args env (a::aa) (f::ff) =
2.484 - if type_of a = type_of f
2.485 - then relate_args (env @ [(a, f)]) aa ff else
2.486 - error ("ERROR in creating the environment for '"
2.487 - ^id_of_scr sc^"' from \nthe items of the guard of "
2.488 - ^metID2str metID^",\n\
2.489 - \different types of formal arg, from the script,\
2.490 - \ and actual arg, from the guards env:'\n\
2.491 - \formal: '"^term2str a^"::"^(type2str o type_of) a^"'\n\
2.492 - \actual: '"^term2str f^"::"^(type2str o type_of) f^"'\n\
2.493 - \in\n\
2.494 - \formals: "^terms2str formals^"\n\
2.495 - \actuals: "^terms2str actuals)
2.496 - val env = relate_args [] formals actuals;
2.497 - in (ScrState (env,[],NONE,e_term,Safe,true), e_ctxt, scr):istate * Proof.context * scr end;
2.498 + let
2.499 + val actuals = itms2args thy metID itms;
2.500 + val scr as Script sc = (#scr o get_met) metID;
2.501 + val formals = formal_args sc
2.502 + (*expects same sequence of (actual) args in itms and (formal) args in met*)
2.503 + fun relate_args env [] [] = env
2.504 + | relate_args env _ [] =
2.505 + error ("ERROR in creating the environment for '" ^
2.506 + id_of_scr sc ^ "' from \nthe items of the guard of " ^
2.507 + metID2str metID ^ ",\n" ^
2.508 + "formal arg(s), from the script, miss actual arg(s), from the guards env:\n" ^
2.509 + (string_of_int o length) formals ^
2.510 + " formals: " ^ terms2str formals ^ "\n" ^
2.511 + (string_of_int o length) actuals ^
2.512 + " actuals: " ^ terms2str actuals)
2.513 + | relate_args env [] actual_finds = env (*may drop Find!*)
2.514 + | relate_args env (a::aa) (f::ff) =
2.515 + if type_of a = type_of f
2.516 + then relate_args (env @ [(a, f)]) aa ff
2.517 + else
2.518 + error ("ERROR in creating the environment for '" ^
2.519 + id_of_scr sc ^ "' from \nthe items of the guard of " ^
2.520 + metID2str metID ^ ",\n" ^
2.521 + "different types of formal arg, from the script, " ^
2.522 + "and actual arg, from the guards env:'\n" ^
2.523 + "formal: '" ^ term2str a ^ "::" ^ (type2str o type_of) a ^ "'\n" ^
2.524 + "actual: '" ^ term2str f ^ "::" ^ (type2str o type_of) f ^ "'\n" ^
2.525 + "in\n" ^
2.526 + "formals: " ^ terms2str formals ^ "\n" ^
2.527 + "actuals: " ^ terms2str actuals)
2.528 + val env = relate_args [] formals actuals;
2.529 + in (ScrState (env,[],NONE,e_term,Safe,true), e_ctxt, scr):istate * Proof.context * scr end;
2.530
2.531 -(*.decide, where to get script/istate from:
2.532 +(* decide, where to get script/istate from:
2.533 (*1*) from PblObj.env: at begin of script if no init_form
2.534 (*2*) from PblObj/PrfObj: if stac is in the middle of the script
2.535 - (*3*) from rls/PrfObj: in case of detail a ruleset.*)
2.536 -(* val (thy', (p,p_), pt) = (thy', (p,p_), pt);
2.537 - *)
2.538 + (*3*) from rls/PrfObj: in case of detail a ruleset *)
2.539 fun from_pblobj_or_detail' thy' (p,p_) pt =
2.540 + let val ctxt = get_ctxt pt (p,p_)
2.541 + in
2.542 if member op = [Pbl,Met] p_
2.543 then case get_obj g_env pt p of
2.544 - NONE => error "from_pblobj_or_detail': no istate"
2.545 - | SOME is =>
2.546 - let val metID = get_obj g_metID pt p
2.547 - val {srls,...} = get_met metID
2.548 - in (srls, is, (#scr o get_met) metID) end
2.549 + NONE => error "from_pblobj_or_detail': no istate"
2.550 + | SOME is =>
2.551 + let
2.552 + val metID = get_obj g_metID pt p
2.553 + val {srls,...} = get_met metID
2.554 + in (srls, is, (#scr o get_met) metID) end
2.555 else
2.556 - let val (pbl,p',rls') = par_pbl_det pt p
2.557 - in if pbl
2.558 - then (*2*)
2.559 - let val thy = assoc_thy thy'
2.560 - val PblObj{meth=itms,...} = get_obj I pt p'
2.561 - val metID = get_obj g_metID pt p'
2.562 - val {srls,...} = get_met metID
2.563 - in (*if last_elem p = 0 (*nothing written to pt yet*)
2.564 - then let val (is, ctxt, sc) = init_scrstate thy itms metID
2.565 - in (srls, is, sc) end
2.566 - else*) (srls, get_loc pt (p,p_), (#scr o get_met) metID)
2.567 - end
2.568 - else (*3*)
2.569 - (e_rls, (*FIXME: get from pbl or met !!!
2.570 - unused for Rrls in locate_gen, next_tac*)
2.571 - get_loc pt (p,p_),
2.572 - case rls' of
2.573 - Rls {scr=scr,...} => scr
2.574 - | Seq {scr=scr,...} => scr
2.575 - | Rrls {scr=rfuns,...} => rfuns)
2.576 - end;
2.577 + let val (pbl,p',rls') = par_pbl_det pt p
2.578 + in if pbl
2.579 + then (*2*)
2.580 + let
2.581 + val thy = assoc_thy thy'
2.582 + val PblObj{meth=itms,...} = get_obj I pt p'
2.583 + val metID = get_obj g_metID pt p'
2.584 + val {srls,...} = get_met metID
2.585 + in (*if last_elem p = 0 nothing written to pt yet*)
2.586 + (srls, get_loc pt (p,p_), (#scr o get_met) metID)
2.587 + end
2.588 + else (*3*)
2.589 + (e_rls, (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in locate_gen, next_tac*)
2.590 + get_loc pt (p,p_),
2.591 + case rls' of
2.592 + Rls {scr=scr,...} => scr
2.593 + | Seq {scr=scr,...} => scr
2.594 + | Rrls {scr=rfuns,...} => rfuns)
2.595 + end
2.596 + end;
2.597
2.598 -(*.get script and istate from PblObj, see (*1*) above.*)
2.599 +(*.get script and istate from PblObj, see (*1*) above.*)
2.600 fun from_pblobj' thy' (p,p_) pt =
2.601 let val p' = par_pblobj pt p
2.602 val thy = assoc_thy thy'
3.1 --- a/test/Tools/isac/Test_Isac.thy Sun May 15 13:59:05 2011 +0200
3.2 +++ b/test/Tools/isac/Test_Isac.thy Tue May 17 09:55:30 2011 +0200
3.3 @@ -183,6 +183,16 @@
3.4 ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*}
3.5 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
3.6
3.7 +ML {*
3.8 +val am = [];
3.9 +insert_assumptions am
3.10 +*}
3.11 +ML {*
3.12 +get_ctxt pt p |> insert_assumptions am
3.13 +*}
3.14 +ML {*
3.15 +from_pblobj_or_detail'
3.16 +*}
3.17 end
3.18
3.19 (*=== inhibit exn ?=============================================================