1.1 --- a/src/Tools/isac/Interpret/script.sml Sun Oct 14 14:43:41 2012 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Sun Oct 14 20:00:27 2012 +0200
1.3 @@ -212,10 +212,7 @@
1.4 NONE)
1.5 in get_t thy body e_term end;
1.6
1.7 -(*FIXME: get 1st stac by next_stac [] instead of ... ?? 29.7.02*)
1.8 -(* val Script sc = scr;
1.9 - *)
1.10 -fun init_form thy (Script sc) env =
1.11 +fun init_form thy (Prog sc) env =
1.12 (case get_stac thy sc of
1.13 NONE => NONE
1.14 (*error ("init_form: no 1st stac in "^
1.15 @@ -1027,7 +1024,7 @@
1.16 )
1.17 end);
1.18
1.19 -fun ass_up (ys as (y,ctxt,s,Script sc,d)) (is as (E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ _) =
1.20 +fun ass_up (ys as (y,ctxt,s,Prog sc,d)) (is as (E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ _) =
1.21 let
1.22 (*val _= tracing("### ass_up1 Let$e: is=")
1.23 val _= tracing(istate2str (ScrState is))*)
1.24 @@ -1057,7 +1054,7 @@
1.25 | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _) =
1.26 astep_up ysa iss (*2*: comes from e2*)
1.27
1.28 - | ass_up (ysa as (y,ctxt,s,Script sc,d)) (is as (E,l,a,v,S,b),ss)
1.29 + | ass_up (ysa as (y,ctxt,s,Prog sc,d)) (is as (E,l,a,v,S,b),ss)
1.30 (Const ("Script.Seq",_) $ _ ) = (*2*: comes from e1, goes to e2*)
1.31 let
1.32 val up = drop_last l;
1.33 @@ -1132,16 +1129,8 @@
1.34
1.35 | ass_up y iss t =
1.36 error ("ass_up not impl for t= "^(term2str t))
1.37 -(* 9.6.03
1.38 - val (ys as (_,_,Script sc,_), ss) =
1.39 - ((thy',srls,scr,d), [(m,EmptyMout,pt,p,[])]:step list);
1.40 - astep_up ys ((E,l,a,v,S,b),ss);
1.41 - val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
1.42 - (ysa, iss);
1.43 - val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
1.44 - ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
1.45 - *)
1.46 -and astep_up (ys as (_,_,_,Script sc,_)) ((E,l,a,v,S,b),ss) =
1.47 +
1.48 +and astep_up (ys as (_,_,_,Prog sc,_)) ((E,l,a,v,S,b),ss) =
1.49 if 1 < length l
1.50 then
1.51 let val up = drop_last l;
1.52 @@ -1209,7 +1198,7 @@
1.53 Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
1.54
1.55 | locate_gen (thy',srls) (m:tac_) ((pt,p):ptree * pos')
1.56 - (scr as Script (h $ body),d) (ScrState (E,l,a,v,S,b), ctxt) =
1.57 + (scr as Prog (h $ body),d) (ScrState (E,l,a,v,S,b), ctxt) =
1.58 let val thy = assoc_thy thy';
1.59 in
1.60 case if l = [] orelse ((*init.in solve..Apply_Method...*)
1.61 @@ -1343,7 +1332,7 @@
1.62 | _ => ((*tracing("### appy: Napp");*)Napp E))
1.63 end);
1.64
1.65 -fun nxt_up thy ptp (scr as (Script sc)) E l ay
1.66 +fun nxt_up thy ptp (scr as (Prog sc)) E l ay
1.67 (t as Const ("HOL.Let",_) $ _) a v = (*comes from let=...*)
1.68 (if ay = Napp_
1.69 then nstep_up thy ptp scr E (drop_last l) Napp_ a v
1.70 @@ -1391,8 +1380,6 @@
1.71 | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v
1.72 else nstep_up thy ptp scr E l Skip_ a v
1.73
1.74 -(* val (scr, l) = (Script sc, up);
1.75 - *)
1.76 | nxt_up thy ptp scr E l ay (Const ("If",_) $ _ $ _ $ _) a v =
1.77 nstep_up thy ptp scr E l ay a v
1.78
1.79 @@ -1415,18 +1402,12 @@
1.80 | Skip (v,E) => ((*tracing("### nxt_up Repeat: Skip res ="^
1.81 (Sign.string_of_term(sign_of (assoc_thy thy)) res'));*)
1.82 nstep_up thy ptp scr E l Skip_ a v))
1.83 -(* val (thy, ptp, scr, E, l, _,(t as Const ("Script.Try",_) $ e $ _), a, v) =
1.84 - (thy, ptp, (Script sc),
1.85 - E, up, ay,(go up sc), a, v);
1.86 - *)
1.87 +
1.88 | nxt_up thy ptp scr E l _ (*makes Napp to Skip*)
1.89 (t as Const ("Script.Try",_) $ e $ _) a v =
1.90 ((*tracing("### nxt_up Try " ^ term2str t);*)
1.91 nstep_up thy ptp scr E l Skip_ a v )
1.92 -(* val (thy, ptp, scr, E, l, _,(t as Const ("Script.Try",_) $ e), a, v) =
1.93 - (thy, ptp, (Script sc),
1.94 - E, up, ay,(go up sc), a, v);
1.95 - *)
1.96 +
1.97 | nxt_up thy ptp scr E l _ (*makes Napp to Skip*)
1.98 (t as Const ("Script.Try"(*2*),_) $ e) a v =
1.99 ((*tracing("### nxt_up Try " ^ term2str t);*)
1.100 @@ -1442,25 +1423,16 @@
1.101 | nxt_up thy ptp scr E l ay
1.102 (Const ("Script.Or",_) $ _ ) a v =
1.103 nstep_up thy ptp scr E (drop_last l) ay a v
1.104 -(* val (thy, ptp, scr, E, l, ay, (Const ("Script.Seq",_) $ _ $ _ $ _), a, v) =
1.105 - (thy, ptp, (Script sc),
1.106 - E, up, ay,(go up sc), a, v);
1.107 - *)
1.108 +
1.109 | nxt_up thy ptp scr E l ay (*all has been done in (*2*) below*)
1.110 (Const ("Script.Seq"(*1*),_) $ _ $ _ $ _) a v =
1.111 nstep_up thy ptp scr E l ay a v
1.112 -(* val (thy, ptp, scr, E, l, ay, (Const ("Script.Seq",_) $ _ $ e2), a, v) =
1.113 - (thy, ptp, (Script sc),
1.114 - E, up, ay,(go up sc), a, v);
1.115 - *)
1.116 +
1.117 | nxt_up thy ptp scr E l ay (*comes from e2*)
1.118 (Const ("Script.Seq"(*2*),_) $ _ $ e2) a v =
1.119 nstep_up thy ptp scr E l ay a v
1.120 -(* val (thy, ptp, scr, E, l, ay, (Const ("Script.Seq",_) $ _), a, v) =
1.121 - (thy, ptp, (Script sc),
1.122 - E, up, ay,(go up sc), a, v);
1.123 - *)
1.124 - | nxt_up thy ptp (scr as Script sc) E l ay (*comes from e1*)
1.125 +
1.126 + | nxt_up thy ptp (scr as Prog sc) E l ay (*comes from e1*)
1.127 (Const ("Script.Seq",_) $ _) a v =
1.128 if ay = Napp_
1.129 then nstep_up thy ptp scr E (drop_last l) Napp_ a v
1.130 @@ -1474,11 +1446,11 @@
1.131
1.132 | nxt_up (thy,_) ptp scr E l ay t a v = error ("nxt_up not impl for " ^ term2str t)
1.133
1.134 -and nstep_up thy ptp (Script sc) E l ay a v =
1.135 +and nstep_up thy ptp (Prog sc) E l ay a v =
1.136 (if 1 < length l
1.137 then
1.138 let val up = drop_last l;
1.139 - in (nxt_up thy ptp (Script sc) E up ay (go up sc) a v ) end
1.140 + in (nxt_up thy ptp (Prog sc) E up ay (go up sc) a v ) end
1.141 else (*interpreted to end*)
1.142 if ay = Skip_ then Skip (v, E) else Napp E
1.143 );
1.144 @@ -1505,7 +1477,7 @@
1.145 (id, string_of_thmI thm), f,(e_term,[(*!?!8.6.03*)])),
1.146 (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
1.147
1.148 - | next_tac thy (ptp as (pt, pos as (p, _)):ptree * pos') (sc as Script (h $ body))
1.149 + | next_tac thy (ptp as (pt, pos as (p, _)):ptree * pos') (sc as Prog (h $ body))
1.150 (ScrState (E,l,a,v,s,b), ctxt) =
1.151 (case if l = [] then appy thy ptp E [R] body NONE v
1.152 else nstep_up thy ptp sc E l Skip_ a v of
1.153 @@ -1528,7 +1500,7 @@
1.154 fun init_scrstate thy itms metID =
1.155 let
1.156 val actuals = itms2args thy metID itms
1.157 - val scr as Script sc = (#scr o get_met) metID
1.158 + val scr as Prog sc = (#scr o get_met) metID
1.159 val formals = formal_args sc
1.160 (*expects same sequence of (actual) args in itms and (formal) args in met*)
1.161 fun relate_args env [] [] = env
1.162 @@ -1637,17 +1609,10 @@
1.163 val metID = get_obj g_metID pt pp;
1.164 val metID' =if metID =e_metID then(thd3 o snd3)(get_obj g_origin pt pp)
1.165 else metID
1.166 - val {scr=Script sc,srls,...} = get_met metID'
1.167 + val {scr = Prog sc,srls,...} = get_met metID'
1.168 val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_);
1.169 in map ((stac2tac pt thy) o rep_stacexpr o #2 o
1.170 (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc) end;
1.171 -(*
1.172 -> val Script sc = (#scr o get_met) ("SqRoot","sqrt-equ-test");
1.173 -> val env = [((term_of o the o (parse (Thy_Info.get_theory "Isac"))) "bdv",
1.174 - (term_of o the o (parse (Thy_Info.get_theory "Isac"))) "x")];
1.175 -> map ((stac2tac pt thy) o #2 o(subst_stacexpr env NONE e_term)) (stacpbls sc);
1.176 -*)
1.177 -
1.178
1.179 (*. fetch tactics from script and filter _applicable_ tactics;
1.180 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics .*)
1.181 @@ -1666,7 +1631,7 @@
1.182 if metID = e_metID
1.183 then (thd3 o snd3) (get_obj g_origin pt pp)
1.184 else metID
1.185 - val {scr=Script sc,srls,erls,rew_ord'=ro,...} = get_met metID'
1.186 + val {scr = Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'
1.187 val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)
1.188 val alltacs = (*we expect at least 1 stac in a script*)
1.189 map ((stac2tac pt thy) o rep_stacexpr o #2 o