1.1 --- a/src/sml/ME/script.sml Mon Dec 08 17:11:47 2003 +0100
1.2 +++ b/src/sml/ME/script.sml Mon Dec 08 17:11:48 2003 +0100
1.3 @@ -55,6 +55,7 @@
1.4 * ptree (*containing node created by tac_ + resp. scrstate*)
1.5 * pos' (*position in ptree; ptree * pos' is the proofstate*)
1.6 * cid(*pos' list TODO*);(*of ptree-nodes ev. cut (by fst tac_)*)
1.7 +val e_step = (Empty_Tac_, EmptyMout, EmptyPtree, e_pos',[]:cid):step;
1.8
1.9 fun rule2thm' (Thm (id, thm)) = (id, string_of_thm thm):thm'
1.10 | rule2thm' r = raise error ("rule2thm': not defined for "^(rule2str r));
1.11 @@ -399,14 +400,11 @@
1.12 | mout2term thy (Form' (PpcKF _)) = e_term;(*3.8.01: res of subpbl
1.13 at time of detection in script*)
1.14
1.15 -(* gets data from script which are necessary for next_stac (=tac);
1.16 - (other data are fetched from pt in 'appl_in')
1.17 - 12.1.01: returnvalue term is useful for appl_in
1.18 - 26.9.00: still necessary? ~~was ? *)
1.19 +(*.convert a script-tac to a tac (and SubProblem to tac_, too).*)
1.20 fun stac2tac_ thy (Const ("Script.Rewrite",_) $ Free (thmID,_) $ _ $ f) =
1.21 let val tid = (de_esc_underscore o strip_thy) thmID
1.22 in (Rewrite (tid, (de_quote o string_of_thm o
1.23 - (assoc_thm' thy)) (tid,"")), f) end
1.24 + (assoc_thm' thy)) (tid,"")), Empty_Tac_) end
1.25 (* val (thy,
1.26 mm as(Const ("Script.Rewrite'_Inst",_) $ sub $ Free(thmID,_) $ _ $ f))
1.27 = (assoc_thy th,stac);
1.28 @@ -422,40 +420,53 @@
1.29 val tid = (de_esc_underscore o strip_thy) thmID (*4.10.02 unnoetig*)
1.30 in (Rewrite_Inst
1.31 (subStr, (tid, (de_quote o string_of_thm o
1.32 - (assoc_thm' thy)) (tid,""))), f) end
1.33 + (assoc_thm' thy)) (tid,""))), Empty_Tac_) end
1.34
1.35 | stac2tac_ thy (Const ("Script.Rewrite'_Set",_) $ Free (rls,_) $ _ $ f)=
1.36 - (Rewrite_Set ((de_esc_underscore o strip_thy) rls), f)
1.37 + (Rewrite_Set ((de_esc_underscore o strip_thy) rls), Empty_Tac_)
1.38
1.39 | stac2tac_ thy (Const ("Script.Rewrite'_Set'_Inst",_) $
1.40 sub $ Free (rls,_) $ _ $ f) =
1.41 let val subML = ((map isapair2pair) o isalist2list) sub;
1.42 val subStr = subst2subs subML;
1.43 - in (Rewrite_Set_Inst (subStr,rls), f) end
1.44 + in (Rewrite_Set_Inst (subStr,rls), Empty_Tac_) end
1.45
1.46 | stac2tac_ thy (Const ("Script.Calculate",_) $ Free (op_,_) $ f) =
1.47 - (Calculate op_, f)
1.48 + (Calculate op_, Empty_Tac_)
1.49
1.50 (*12.1.01.*)
1.51 | stac2tac_ thy (Const("Script.Check'_elementwise",_) $ _ $
1.52 (set as Const ("Collect",_) $ Abs (_,_,pred))) =
1.53 - (Check_elementwise (Sign.string_of_term (sign_of thy) pred), set)
1.54 + (Check_elementwise (Sign.string_of_term (sign_of thy) pred),
1.55 + (*set*)Empty_Tac_)
1.56
1.57 | stac2tac_ thy (Const("Script.Or'_to'_List",_) $ _ ) =
1.58 - (Or_to_List, e_term)
1.59 + (Or_to_List, Empty_Tac_)
1.60
1.61 (*12.1.01.for subproblem_equation_dummy in root-equation *)
1.62 | stac2tac_ thy (Const ("Script.Tac",_) $ Free (str,_)) =
1.63 - (Tac ((de_esc_underscore o strip_thy) str), e_term)
1.64 + (Tac ((de_esc_underscore o strip_thy) str), Empty_Tac_)
1.65 (*L_ will come from pt in appl_in*)
1.66
1.67 + (*3.12.03 copied from assod SubProblem*)
1.68 | stac2tac_ thy (Const ("Script.SubProblem",_) $
1.69 - (Const ("Pair",_) $ Free (thy',_) $
1.70 - (Const ("Pair",_) $ pblID' $ _)) $ ags') =
1.71 - let val pblID = ((map (de_esc_underscore o free2str))
1.72 - o isalist2list) pblID'
1.73 - val thy_ = ((implode o drop_last o explode) thy')^".thy"
1.74 - in (Subproblem (thy_, pblID), subpbl thy' pblID) end
1.75 + (Const ("Pair",_) $
1.76 + Free (dI',_) $
1.77 + (Const ("Pair",_) $ pI' $ mI')) $ ags') =
1.78 + let val dI = ((implode o drop_last o explode) dI')^".thy";
1.79 + val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
1.80 + val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
1.81 + val {cas, ppc,...} = get_pbt pI
1.82 + val ags = isalist2list ags' (*"bool_ (-1+x=0) FIXXXXXME: equality !!*)
1.83 + val fmz_ = map term2str ags
1.84 + val hdl = case cas of
1.85 + None => pblterm dI pI
1.86 + | Some t => subst_atomic ((vars_of_pbl_ ppc)~~ ags) t
1.87 + val oris = match_ags (assoc_thy dI) ppc ags;
1.88 + val f = subpbl dI' pI
1.89 + in (Subproblem (dI, pI),
1.90 + Subproblem' ((dI, pI, mI), oris, hdl, fmz_, f))
1.91 + end
1.92
1.93 | stac2tac_ thy t = raise error
1.94 ("stac2tac_ TODO: no match for "^
1.95 @@ -497,6 +508,8 @@
1.96 fun rep_stacexpr (STac t ) = t
1.97 | rep_stacexpr (Expr t) =
1.98 raise error ("rep_stacexpr called with t= "^(term2str t));
1.99 +
1.100 +(*FIXME curried args: subst_stacexpr NEEDS SPOURIOUSLY: E a v *)
1.101 fun subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ $ _ ))=
1.102 STac (subst_atomic (case a of Some a => upd_env E (a,v) | None => E) t)
1.103
1.104 @@ -921,7 +934,8 @@
1.105
1.106 (* val (Rewrite_Inst'(thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))=m;
1.107 *)
1.108 -(*decompose tac_ to a rule and to (lhs,rhs) for ets*)
1.109 +(*decompose tac_ to a rule and to (lhs,rhs) for ets FIXME.12.03: obsolete!
1.110 + NOTE.12.03: also used for msg 'not locatable' ?!: 'Subproblem' missing !!!*)
1.111 fun rep_tac_ (Rewrite_Inst'
1.112 (thy',rod,rls,put,subs,(thmID,thm),f,(f',asm))) =
1.113 let val fT = type_of f;
1.114 @@ -1051,6 +1065,8 @@
1.115 > lhs'=lhs;
1.116 val it = true : bool*)
1.117 | rep_tac_ (Check_elementwise' (t,str,(t',asm))) = (Erule, (e_term, t'))
1.118 + | rep_tac_ (Subproblem' (_,_,_,_,t')) = (Erule, (e_term, t'))
1.119 + | rep_tac_ (Or_to_List' (t, t')) = (Erule, (t, t'))
1.120 | rep_tac_ m = raise error ("rep_tac_: not impl.for "^
1.121 (tac_2str m));
1.122
1.123 @@ -1108,9 +1124,11 @@
1.124 there was an appl.stac (Repeat, Or e1, ...)
1.125 *)
1.126
1.127 -fun assy ya ((E,l,a,v,S,b),ss)
1.128 +fun assy ya (is as (E,l,a,v,S,b),ss)
1.129 (Const ("Let",_) $ e $ (Abs (id,T,body))) =
1.130 - (case assy ya ((E , l@[L,R], a,v,S,b),ss) e of
1.131 + ((*writeln("### assy Let$e$Abs: is=");
1.132 + writeln(istate2str (ScrState is));*)
1.133 + case assy ya ((E , l@[L,R], a,v,S,b),ss) e of
1.134 NasApp ((E',l,a,v,S,bb),ss) =>
1.135 let val id' = mk_Free (id, T);
1.136 val E' = upd_env E' (id', v);
1.137 @@ -1201,8 +1219,10 @@
1.138 assy (((thy',srls),d),ap) ((E,l,a,v,S,b), (m,EmptyMout,pt,(p,p_),c)::ss) t;
1.139 *)
1.140
1.141 - | assy (((thy',sr),d),ap) ((E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss) t =
1.142 - case subst_stacexpr E a v t of
1.143 + | assy (((thy',sr),d),ap) (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss) t =
1.144 + ((*writeln("### assy, is= ");
1.145 + writeln(istate2str (ScrState is));*)
1.146 + case subst_stacexpr E a v t of
1.147 Expr s =>
1.148 ((*writeln("### assy: listexpr t= "^(term2str t));
1.149 writeln("### assy, E= "^(env2str E));
1.150 @@ -1240,20 +1260,22 @@
1.151 (NasNap (v, E))
1.152 )
1.153 )
1.154 - end;
1.155 + end);
1.156 (* (astep_up ((thy',scr,d),NasApp_) ((E,l,a,v,S,b),[(m,EmptyMout,pt,p,[])])) handle e => print_exn_G e;
1.157 *)
1.158
1.159
1.160 (* val (ys as (y,s,Script sc,d), Const ("Let",_) $ _) = (ys, go up sc);
1.161 *)
1.162 -fun ass_up (ys as (y,s,Script sc,d)) ((E,l,a,v,S,b),ss)
1.163 +fun ass_up (ys as (y,s,Script sc,d)) (is as (E,l,a,v,S,b),ss)
1.164 (Const ("Let",_) $ _) =
1.165 - let val l = drop_last l; (*comes from e, goes to Abs*)
1.166 + let (*val _= writeln("### ass_up1 Let$e: is=")
1.167 + val _= writeln(istate2str (ScrState is))*)
1.168 + val l = drop_last l; (*comes from e, goes to Abs*)
1.169 val (Const ("Let",_) $ e $ (Abs (i,T,body))) = go l sc;
1.170 val i = mk_Free (i, T);
1.171 val E = upd_env E (i, v);
1.172 - (*val _=writeln("### ass_up Let e: E="^(subst2str E));*)
1.173 + (*val _=writeln("### ass_up2 Let$e: E="^(subst2str E));*)
1.174 in case assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body of
1.175 Assoc iss => Assoc iss
1.176 | NasApp iss => astep_up ys iss
1.177 @@ -1262,8 +1284,10 @@
1.178 | ass_up ys iss (Abs (_,_,_)) =
1.179 astep_up ys iss (*TODO 5.9.00: env ?*)
1.180
1.181 - | ass_up ys iss (Const ("Let",_) $ e $ (Abs (i,T,b))) =
1.182 - astep_up ys iss (*TODO 5.9.00: env ?*)
1.183 + | ass_up ys (iss as (is,_)) (Const ("Let",_) $ e $ (Abs (i,T,b)))=
1.184 + ((*writeln("### ass_up Let$e$Abs: is=");
1.185 + writeln(istate2str (ScrState is));*)
1.186 + astep_up ys iss) (*TODO 5.9.00: env ?*)
1.187
1.188
1.189 | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _ $ _) =
1.190 @@ -1272,10 +1296,12 @@
1.191 | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _) =
1.192 astep_up ysa iss (*2*: comes from e2*)
1.193
1.194 - | ass_up (ysa as (y,s,Script sc,d)) ((E,l,a,v,S,b),ss)
1.195 + | ass_up (ysa as (y,s,Script sc,d)) (is as (E,l,a,v,S,b),ss)
1.196 (Const ("Script.Seq",_) $ _ ) = (*2*: comes from e1, goes to e2*)
1.197 let val up = drop_last l;
1.198 - val Const ("Script.Seq",_) $ _ $ e2 = go up sc;
1.199 + val Const ("Script.Seq",_) $ _ $ e2 = go up sc
1.200 + (*val _= writeln("### ass_up Seq$e: is=")
1.201 + val _= writeln(istate2str (ScrState is))*)
1.202 in case assy (((y,s),d),Aundef) ((E, up@[R], a,v,S,b),ss) e2 of
1.203 NasNap (v,E) => astep_up ysa ((E,up,a,v,S,b),ss)
1.204 | NasApp iss => astep_up ysa iss
1.205 @@ -1346,7 +1372,7 @@
1.206 if 1 < length l
1.207 then
1.208 let val up = drop_last l;
1.209 - (*val _= writeln("### astep_up: v= "^(term2str v));*)
1.210 + (*val _= writeln("### astep_up: E= "env2str E);*)
1.211 in ass_up ys ((E,up,a,v,S,b),ss) (go up sc) end
1.212 else (NasNap (v, E))
1.213 ;
1.214 @@ -1419,19 +1445,23 @@
1.215 val p = (p,p_);
1.216 val (scr as Script (h $ body)) = (sc);
1.217 val ScrState (E,l,a,v,S,b) = (is);
1.218 +
1.219 + val (ts as (thy',srls), m, (pt,p), (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b))) = ((thy',srls), m, (pt,(p,p_)), (sc,d), is);
1.220 locate_gen (thy',srls) m (pt,p) (Script(h $ body),d)(ScrState(E,l,a,v,S,b));
1.221 *)
1.222 | locate_gen (ts as (thy',srls)) (m:tac_) ((pt,p):ptree * pos')
1.223 (scr as Script (h $ body),d) (ScrState (E,l,a,v,S,b)) =
1.224 - let (*val _= writeln("### locate_gen: p="^(pos'2str p));*)
1.225 + let (*val _= writeln("### locate_gen-----------------: is=");
1.226 + val _= writeln( istate2str (ScrState (E,l,a,v,S,b)));*)
1.227 val thy = assoc_thy thy';
1.228 in case if l=[] then (assy ((ts,d),Aundef) ((E,[R],a,v,S,b),
1.229 [(m,EmptyMout,pt,p,[])]) body)
1.230 (* val Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =
1.231 + (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b),[(m,EmptyMout,pt,p,[])]));
1.232 (assy ((ts,d),Aundef) ((E,[R],a,v,S,b),[(m,EmptyMout,pt,p,[])]) body);
1.233 *)
1.234 else (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b),
1.235 - [(m,EmptyMout,pt,p,[])]) ) of
1.236 + [(m,EmptyMout,pt,p,[])]) ) of
1.237 Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =>
1.238 ((*writeln("### locate_gen: p'="^(pos'2str p'));*)
1.239 if bb then Steps (ScrState is, ss)
1.240 @@ -1439,6 +1469,8 @@
1.241 then let (*val _=writeln("### locate_gen, bef g1: p="^(pos'2str p));*)
1.242 val (po,p_) = p;
1.243 val po' = case p_ of Frm => po | Res => lev_on po
1.244 + (*WN.12.03: noticed, that pos is also updated in assy !?!
1.245 + instead take p' from Assoc ?????????????????????????????*)
1.246 val (p'',c'',f'',pt'') =
1.247 generate1 thy m (ScrState is) (po',p_) pt;
1.248 (*val _=writeln("### locate_gen, aft g1: p''="^(pos'2str p''));*)
1.249 @@ -1504,7 +1536,9 @@
1.250
1.251 fun appy thy ptp E l
1.252 (t as Const ("Let",_) $ e $ (Abs (i,T,b))) a v =
1.253 - (case appy thy ptp E (l@[L,R]) e a v of
1.254 + ((*writeln("### appy Let$e$Abs: is=");
1.255 + writeln(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
1.256 + case appy thy ptp E (l@[L,R]) e a v of
1.257 Skip (res, E) =>
1.258 let (*val _= writeln("### appy Let "^(term2str t));
1.259 val _= writeln("### appy Let: Skip res ="^(term2str res));*)
1.260 @@ -1626,7 +1660,7 @@
1.261 appy (th,sr) (pt, p) E l t a v;
1.262 *)
1.263 | appy (thy as (th,sr)) (pt, p) E l t a v =
1.264 - case subst_stacexpr E a v t of
1.265 + (case subst_stacexpr E a v t of
1.266 Expr s => ((*writeln("### appy, listexpr= "^(term2str t));
1.267 writeln("### appy, E= "^(env2str E));
1.268 writeln("### appy, eval(..)= "^(term2str
1.269 @@ -1638,20 +1672,19 @@
1.270 *)
1.271 | STac stac =>
1.272 let
1.273 - (*val _= writeln("### appy t, E= "^(subst2str E));
1.274 -val t =(term_of o the o (parse Isac.thy))"Rewrite_Set make_polyomial False g_";
1.275 -val v =(term_of o the o (parse Isac.thy))"x+1=0";
1.276 - val _= writeln("### appy t, a= "^(termopt2str a));
1.277 - val _= writeln("### appy t, v= "^(term2str v));
1.278 - val _= writeln("### appy t, stac= "^(term2str stac));
1.279 - val _= writeln("### appy t, vor stac2tac");
1.280 - val _= writeln("### appy t, l = "^(loc_2str l));*)
1.281 - val (m,_) = stac2tac_ (assoc_thy th) stac;
1.282 + (*val _= writeln("### appy t, stac= "^(term2str stac));*)
1.283 + (*val _= writeln("### appy t, vor stac2tac_ is=");
1.284 + val _= writeln(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
1.285 + val (m,m') = stac2tac_ (assoc_thy th) stac;
1.286 (*val _= writeln("### appy t, nach stac2tac, m= "^(tac2str m));*)
1.287 - in (case applicable_in p pt m of
1.288 - Appl m' => ((*writeln("### appy: Appy");*)
1.289 - Appy (m', (E,l,a,v,Sundef,false(*18.8.03??*))))
1.290 - | _ => ((*writeln("### appy: Napp");*)Napp E)) end;
1.291 + in case m of
1.292 + Subproblem _ => Appy (m', (E,l,a,tac_2res m',Sundef,false))
1.293 + | _ => (case applicable_in p pt m of
1.294 + Appl m' =>
1.295 + ((*writeln("### appy: Appy");*)
1.296 + Appy (m', (E,l,a,tac_2res m',Sundef,false)))
1.297 + | _ => ((*writeln("### appy: Napp");*)Napp E))
1.298 + end);
1.299
1.300
1.301 (* val (scr as Script sc, l, t as Const ("Let",_) $ _) =
1.302 @@ -1660,15 +1693,21 @@
1.303 *)
1.304 fun nxt_up thy ptp (scr as (Script sc)) E l ay
1.305 (t as Const ("Let",_) $ _) a v = (*comes from let=...*)
1.306 - if ay = Napp_
1.307 + ((*writeln("### nxt_up1 Let$e: is=");
1.308 + writeln(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
1.309 + if ay = Napp_
1.310 then nstep_up thy ptp scr E (drop_last l) Napp_ a v
1.311 else (*Skip_*)
1.312 let val up = drop_last l;
1.313 val (Const ("Let",_) $ e $ (Abs (i,T,body))) = go up sc;
1.314 - in case appy thy ptp E (up@[R,D]) body a v of
1.315 + val i = mk_Free (i, T);
1.316 + val E = upd_env E (i, v);
1.317 + (*val _= writeln("### nxt_up2 Let$e: is=");
1.318 + val _= writeln(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
1.319 + in case appy thy ptp (E) (up@[R,D]) body a v of
1.320 Appy lre => Appy lre
1.321 | Napp E => nstep_up thy ptp scr E up Napp_ a v
1.322 - | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v end
1.323 + | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v end)
1.324
1.325 | nxt_up thy ptp scr E l ay
1.326 (t as Abs (_,_,_)) a v =
1.327 @@ -1678,7 +1717,9 @@
1.328
1.329 | nxt_up thy ptp scr E l ay
1.330 (t as Const ("Let",_) $ e $ (Abs (i,T,b))) a v =
1.331 - ((*writeln("### nxt_up Let e Abs: "^
1.332 + ((*writeln("### nxt_up Let$e$Abs: is=");
1.333 + writeln(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
1.334 + (*writeln("### nxt_up Let e Abs: "^
1.335 (Sign.string_of_term (sign_of (assoc_thy thy)) t));*)
1.336 nstep_up thy ptp scr (*upd_env*) E (*a,v)*)
1.337 (*eno,upd_env env (iar,res),iar,res,saf*) l ay a v)
1.338 @@ -1843,25 +1884,27 @@
1.339
1.340 val(thy, ptp as (pt,(p,_)), sc as Script (h $ body),ScrState (E,l,a,v,s,b))=
1.341 ((thy',srls), (pt,(p,p_)), sc, ScrState (E,l,a,scval,scsaf,b));
1.342 +
1.343 + val(thy, ptp as (pt,(p,_)), sc as Script (h $ body),ScrState (E,l,a,v,s,b))=
1.344 + ((thy',srls), (pt,pos), sc, is);
1.345 next_tac thy ptp (Script (h $ body)) (ScrState (E,l,a,v,s,b));
1.346 *)
1.347 | next_tac thy (ptp as (pt,(p,_)):ptree * pos') (sc as Script (h $ body))
1.348 (ScrState (E,l,a,v,s,b)) =
1.349 - ((*writeln("### next_tac: p = "^(ints2str p));
1.350 - writeln("### next_tac: ist= "^(istate2str (E,l,a,v,s,b)));
1.351 - writeln("### next_tac: = "^());*)
1.352 + ((*writeln("### next_tac-----------------: E= ");
1.353 + writeln( istate2str (ScrState (E,l,a,v,s,b)));*)
1.354 case if l=[] then appy thy ptp E [R] body None e_term
1.355 else nstep_up thy ptp sc E l Skip_ a v of
1.356 Skip (v,_) => (*finished*)
1.357 (case par_pbl_det pt p of
1.358 (true, p', _) =>
1.359 let val (_,pblID,_) = get_obj g_spec pt p';
1.360 - in (Check_Postcond' (pblID, (v, [(*8.6.03NO asms???*)])),
1.361 + in (Check_Postcond' (pblID, (v, [(*8.6.03 NO asms???*)])),
1.362 e_istate, (v,s)) end
1.363 | (_,p',rls') => (End_Detail' e_term(*8.6.03*), e_istate, (v,s)))
1.364 | Napp _ => (Empty_Tac_, e_istate, (e_term, Sundef)) (*helpless*)
1.365 - | Appy (m', scrst) => (m', ScrState scrst,
1.366 - (e_term, Sundef))) (*next stac*)
1.367 + | Appy (m', scrst as (_,_,_,v,_,_)) => (m', ScrState scrst,
1.368 + (v, Sundef))) (*next stac*)
1.369
1.370 | next_tac _ _ _ is = raise error ("next_tac: not impl for "^
1.371 (istate2str is));