1.1 --- a/src/Tools/isac/Interpret/script.sml Fri Sep 23 08:30:35 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Fri Sep 23 09:41:11 2011 +0200
1.3 @@ -924,16 +924,16 @@
1.4 in assy ya ((E', l@[R,D], a,v,S,b),ss) body end
1.5 | ay => ay)
1.6
1.7 - | assy (ya as (((thy,srls),_),_)) ((E,l,_,v,S,b),ss) (Const ("Script.While",_) $ c $ e $ a) =
1.8 + | assy (ya as (thy,ctxt,srls,_,_)) ((E,l,_,v,S,b),ss) (Const ("Script.While",_) $ c $ e $ a) =
1.9 (if eval_true_ thy srls (subst_atomic (upd_env E (a,v)) c)
1.10 then assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e
1.11 else NasNap (v, E))
1.12 - | assy (ya as (((thy,srls),_),_)) ((E,l,a,v,S,b),ss) (Const ("Script.While",_) $ c $ e) =
1.13 + | assy (ya as (thy,ctxt,srls,_,_)) ((E,l,a,v,S,b),ss) (Const ("Script.While",_) $ c $ e) =
1.14 (if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c)
1.15 then assy ya ((E, l@[R], a,v,S,b),ss) e
1.16 else NasNap (v, E))
1.17
1.18 - | assy (ya as (((thy,srls),_),_)) ((E,l,a,v,S,b),ss) (Const ("If",_) $ c $ e1 $ e2) =
1.19 + | assy (ya as (thy,ctxt,srls,_,_)) ((E,l,a,v,S,b),ss) (Const ("If",_) $ c $ e1 $ e2) =
1.20 (if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c)
1.21 then assy ya ((E, l@[L,R], a,v,S,b),ss) e1
1.22 else assy ya ((E, l@[ R], a,v,S,b),ss) e2)
1.23 @@ -961,14 +961,14 @@
1.24 | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Repeat",_) $ e) =
1.25 assy ya ((E,(l@[R]),a,v,S,b),ss) e
1.26
1.27 - | assy (y, Aundef) ((E,l,_,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2 $ a) =
1.28 - (case assy (y, AssOnly) ((E,(l@[L,L,R]),SOME a,v,S,b),ss) e1 of
1.29 + | assy (y,x,s,sc,Aundef) ((E,l,_,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2 $ a) =
1.30 + (case assy (y,x,s,sc,AssOnly) ((E,(l@[L,L,R]),SOME a,v,S,b),ss) e1 of
1.31 NasNap (v, E) =>
1.32 - (case assy (y, AssOnly) ((E,(l@[L,R]),SOME a,v,S,b),ss) e2 of
1.33 + (case assy (y,x,s,sc,AssOnly) ((E,(l@[L,R]),SOME a,v,S,b),ss) e2 of
1.34 NasNap (v, E) =>
1.35 - (case assy (y, AssGen) ((E,(l@[L,L,R]),SOME a,v,S,b),ss) e1 of
1.36 + (case assy (y,x,s,sc,AssGen) ((E,(l@[L,L,R]),SOME a,v,S,b),ss) e1 of
1.37 NasNap (v, E) =>
1.38 - assy (y, AssGen) ((E, (l@[L,R]), SOME a,v,S,b),ss) e2
1.39 + assy (y,x,s,sc,AssGen) ((E, (l@[L,R]), SOME a,v,S,b),ss) e2
1.40 | ay => ay)
1.41 | ay =>(ay))
1.42 | NasApp _ => error ("assy: FIXXXME ///must not return NasApp///")
1.43 @@ -979,7 +979,7 @@
1.44 | ay => (ay))
1.45
1.46 (*here is not a tactical like TRY etc, but a tactic creating a step in calculation*)
1.47 - | assy (((thy',sr),d),ap) (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss) t =
1.48 + | assy (thy',ctxt,sr,d,ap) (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss) t =
1.49 (case handle_leaf "locate" thy' sr E a v t of
1.50 (a', Expr s) =>
1.51 (NasNap (eval_listexpr_ (assoc_thy thy') sr
1.52 @@ -1017,7 +1017,7 @@
1.53 )
1.54 end);
1.55
1.56 -fun ass_up (ys as (y,s,Script sc,d)) (is as (E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ _) =
1.57 +fun ass_up (ys as (y,ctxt,s,Script sc,d)) (is as (E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ _) =
1.58 let
1.59 (*val _= tracing("### ass_up1 Let$e: is=")
1.60 val _= tracing(istate2str (ScrState is))*)
1.61 @@ -1026,7 +1026,7 @@
1.62 val i = mk_Free (i, T);
1.63 val E = upd_env E (i, v);
1.64 (*val _=tracing("### ass_up2 Let$e: E="^(subst2str E));*)
1.65 - in case assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body of
1.66 + in case assy (y,ctxt,s,d,Aundef) ((E, l@[R,D], a,v,S,b),ss) body of
1.67 Assoc iss => Assoc iss
1.68 | NasApp iss => astep_up ys iss
1.69 | NasNap (v, E) => astep_up ys ((E,l,a,v,S,b),ss) end
1.70 @@ -1047,7 +1047,7 @@
1.71 | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _) =
1.72 astep_up ysa iss (*2*: comes from e2*)
1.73
1.74 - | ass_up (ysa as (y,s,Script sc,d)) (is as (E,l,a,v,S,b),ss)
1.75 + | ass_up (ysa as (y,ctxt,s,Script sc,d)) (is as (E,l,a,v,S,b),ss)
1.76 (Const ("Script.Seq",_) $ _ ) = (*2*: comes from e1, goes to e2*)
1.77 (* val ((ysa as (y,s,Script sc,d)), (is as (E,l,a,v,S,b),ss),
1.78 (Const ("Script.Seq",_) $ _ )) =
1.79 @@ -1057,7 +1057,7 @@
1.80 val Const ("Script.Seq",_) $ _ $ e2 = go up sc
1.81 (*val _= tracing("### ass_up Seq$e: is=")
1.82 val _= tracing(istate2str (ScrState is))*)
1.83 - in case assy (((y,s),d),Aundef) ((E, up@[R], a,v,S,b),ss) e2 of
1.84 + in case assy (y,ctxt,s,d,Aundef) ((E, up@[R], a,v,S,b),ss) e2 of
1.85 NasNap (v,E) => astep_up ysa ((E,up,a,v,S,b),ss)
1.86 | NasApp iss => astep_up ysa iss
1.87 | ay => ay end
1.88 @@ -1075,13 +1075,13 @@
1.89 ((*tracing("### ass_up Try $ e");*)
1.90 astep_up ysa iss)
1.91
1.92 - | ass_up (ys as (y,s,_,d)) ((E,l,_,v,S,b),ss)
1.93 + | ass_up (ys as (y,ctxt,s,_,d)) ((E,l,_,v,S,b),ss)
1.94 (*(Const ("Script.While",_) $ c $ e $ a) = WN050930 blind fix*)
1.95 (t as Const ("Script.While",_) $ c $ e $ a) =
1.96 ((*tracing("### ass_up: While c= "^
1.97 (term2str (subst_atomic (upd_env E (a,v)) c)));*)
1.98 if eval_true_ y s (subst_atomic (upd_env E (a,v)) c)
1.99 - then (case assy (((y,s),d),Aundef) ((E, l@[L,R], SOME a,v,S,b),ss) e of
1.100 + then (case assy (y,ctxt,s,d,Aundef) ((E, l@[L,R], SOME a,v,S,b),ss) e of
1.101 NasNap (v,E') => astep_up ys ((E',l, SOME a,v,S,b),ss)
1.102 | NasApp ((E',l,a,v,S,b),ss) =>
1.103 ass_up ys ((E',l,a,v,S,b),ss) t (*WN050930 't' was not assigned*)
1.104 @@ -1089,11 +1089,11 @@
1.105 else astep_up ys ((E,l, SOME a,v,S,b),ss)
1.106 )
1.107
1.108 - | ass_up (ys as (y,s,_,d)) ((E,l,a,v,S,b),ss)
1.109 + | ass_up (ys as (y,ctxt,s,_,d)) ((E,l,a,v,S,b),ss)
1.110 (*(Const ("Script.While",_) $ c $ e) = WN050930 blind fix*)
1.111 (t as Const ("Script.While",_) $ c $ e) =
1.112 if eval_true_ y s (subst_atomic (upd_env_opt E (a,v)) c)
1.113 - then (case assy (((y,s),d),Aundef) ((E, l@[R], a,v,S,b),ss) e of
1.114 + then (case assy (y,ctxt,s,d,Aundef) ((E, l@[R], a,v,S,b),ss) e of
1.115 NasNap (v,E') => astep_up ys ((E',l, a,v,S,b),ss)
1.116 | NasApp ((E',l,a,v,S,b),ss) =>
1.117 ass_up ys ((E',l,a,v,S,b),ss) t (*WN050930 't' was not assigned*)
1.118 @@ -1102,17 +1102,17 @@
1.119
1.120 | ass_up y iss (Const ("If",_) $ _ $ _ $ _) = astep_up y iss
1.121
1.122 - | ass_up (ys as (y,s,_,d)) ((E,l,_,v,S,b),ss)
1.123 + | ass_up (ys as (y,ctxt,s,_,d)) ((E,l,_,v,S,b),ss)
1.124 (t as Const ("Script.Repeat",_) $ e $ a) =
1.125 - (case assy (((y,s),d), Aundef) ((E, (l@[L,R]), SOME a,v,S,b),ss) e of
1.126 + (case assy (y,ctxt,s,d, Aundef) ((E, (l@[L,R]), SOME a,v,S,b),ss) e of
1.127 NasNap (v,E') => astep_up ys ((E',l, SOME a,v,S,b),ss)
1.128 | NasApp ((E',l,a,v,S,b),ss) =>
1.129 ass_up ys ((E',l,a,v,S,b),ss) t
1.130 | ay => ay)
1.131
1.132 - | ass_up (ys as (y,s,_,d)) (is as ((E,l,a,v,S,b),ss))
1.133 + | ass_up (ys as (y,ctxt,s,_,d)) (is as ((E,l,a,v,S,b),ss))
1.134 (t as Const ("Script.Repeat",_) $ e) =
1.135 - (case assy (((y,s),d), Aundef) ((E, (l@[R]), a,v,S,b),ss) e of
1.136 + (case assy (y,ctxt,s,d,Aundef) ((E, (l@[R]), a,v,S,b),ss) e of
1.137 NasNap (v', E') => astep_up ys ((E',l,a,v',S,b),ss)
1.138 | NasApp ((E',l,a,v',S,bb),ss) =>
1.139 ass_up ys ((E',l,a,v',S,b),ss) t
1.140 @@ -1136,7 +1136,7 @@
1.141 val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
1.142 ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
1.143 *)
1.144 -and astep_up (ys as (_,_,Script sc,_)) ((E,l,a,v,S,b),ss) =
1.145 +and astep_up (ys as (_,_,_,Script sc,_)) ((E,l,a,v,S,b),ss) =
1.146 if 1 < length l
1.147 then
1.148 let val up = drop_last l;
1.149 @@ -1196,21 +1196,21 @@
1.150 NOT IMPL. -- "error: do other step before"
1.151 NotLocatable: thus generate_hard
1.152 *)
1.153 -fun locate_gen (thy',_) (Rewrite'(_,ro,er,pa,(id,str),f,_)) (pt,p)
1.154 +fun locate_gen (thy',g_) (Rewrite'(_,ro,er,pa,(id,str),f,_)) (pt,p)
1.155 (Rfuns {locate_rule=lo,...}, d) (RrlsState (_,f'',rss,rts), ctxt) =
1.156 (case lo rss f (Thm (id, mk_thm (assoc_thy thy') str)) of
1.157 [] => NotLocatable
1.158 | rts' =>
1.159 Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
1.160
1.161 - | locate_gen (ts as (thy',srls)) (m:tac_) ((pt,p):ptree * pos')
1.162 + | locate_gen (thy',srls) (m:tac_) ((pt,p):ptree * pos')
1.163 (scr as Script (h $ body),d) (ScrState (E,l,a,v,S,b), ctxt) =
1.164 let val thy = assoc_thy thy';
1.165 in
1.166 case if l = [] orelse ((*init.in solve..Apply_Method...*)
1.167 (last_elem o fst) p = 0 andalso snd p = Res)
1.168 - then (assy ((ts,d),Aundef) ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]) body)
1.169 - else (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) of
1.170 + then (assy (thy',ctxt,srls,d,Aundef) ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]) body)
1.171 + else (astep_up (thy',ctxt,srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) of
1.172 Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =>
1.173 (if bb
1.174 then Steps (ScrState is, ss)