1.1 --- a/src/Tools/isac/Interpret/script.sml Wed Mar 14 17:12:43 2012 +0100
1.2 +++ b/src/Tools/isac/Interpret/script.sml Sat Mar 17 11:06:46 2012 +0100
1.3 @@ -567,16 +567,7 @@
1.4 if f = f_ then Ass (m,f') else AssWeak (m,f')
1.5 else NotAss
1.6 | _ => NotAss)
1.7 -(*
1.8 - | assod pt _ (m as Check_elementwise' (consts,_,(consts_chkd,_)))
1.9 - (Const ("Script.Check'_elementwise",_) $ consts' $ _) =
1.10 - (tracing("### assod Check'_elementwise: consts= "^(term2str consts)^
1.11 - ", consts'= "^(term2str consts'));
1.12 - atomty consts; atomty consts';
1.13 - if consts = consts'
1.14 - then (tracing"### assod Check'_elementwise: Ass"; Ass (m, consts_chkd))
1.15 - else (tracing"### assod Check'_elementwise: NotAss"; NotAss))
1.16 -*)
1.17 +
1.18 | assod pt _ (m as Check_elementwise' (consts,_,(consts_chkd,_)))
1.19 (Const ("Script.Check'_elementwise",_) $ consts' $ _) =
1.20 if consts = consts'
1.21 @@ -1349,7 +1340,7 @@
1.22 | _ =>
1.23 (case applicable_in p pt m of
1.24 Appl m' => (Appy (m', (E,l,a',tac_2res m',Sundef,false)))
1.25 - | _ => ((*tracing("### appy: Napp");*)Napp E))
1.26 + | _ => ((*tracing("### appy: Napp");*)Napp E))
1.27 end);
1.28
1.29 fun nxt_up thy ptp (scr as (Script sc)) E l ay
1.30 @@ -1371,15 +1362,14 @@
1.31 | nxt_up thy ptp scr E l ay
1.32 (t as Abs (_,_,_)) a v =
1.33 ((*tracing("### nxt_up Abs: " ^ term2str t);*)
1.34 - nstep_up thy ptp scr E (*enr*) l ay a v)
1.35 + nstep_up thy ptp scr E l ay a v)
1.36
1.37 | nxt_up thy ptp scr E l ay
1.38 (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v =
1.39 ((*tracing("### nxt_up Let$e$Abs: is=");
1.40 tracing(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
1.41 (*tracing("### nxt_up Let e Abs: " ^ term2str t);*)
1.42 - nstep_up thy ptp scr (*upd_env*) E (*a,v)*)
1.43 - (*eno,upd_env env (iar,res),iar,res,saf*) l ay a v)
1.44 + nstep_up thy ptp scr E l ay a v)
1.45
1.46 (*no appy_: never causes Napp -> Helpless*)
1.47 | nxt_up (thy as (th,sr)) ptp scr E l _
1.48 @@ -1482,14 +1472,8 @@
1.49 | Napp E => nstep_up thy ptp scr E up Napp_ a v
1.50 | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v end
1.51
1.52 - | nxt_up (thy,_) ptp scr E l ay t a v =
1.53 - error ("nxt_up not impl for " ^ term2str t)
1.54 + | nxt_up (thy,_) ptp scr E l ay t a v = error ("nxt_up not impl for " ^ term2str t)
1.55
1.56 -(* val (thy, ptp, (Script sc), E, l, ay, a, v)=
1.57 - (thy, ptp, scr, E, l, Skip_, a, v);
1.58 - val (thy, ptp, (Script sc), E, l, ay, a, v)=
1.59 - (thy, ptp, sc, E, l, Skip_, a, v);
1.60 - *)
1.61 and nstep_up thy ptp (Script sc) E l ay a v =
1.62 (if 1 < length l
1.63 then
1.64 @@ -1510,34 +1494,32 @@
1.65 20.8.02: do NOT return safe (is only changed in locate !!!)
1.66 *)
1.67 fun next_tac (thy,_) (pt,p) (Rfuns {next_rule,...}) (RrlsState(f,f',rss,_), ctxt) =
1.68 - if f = f'
1.69 - then (End_Detail' (f',[])(*8.6.03*), (Uistate, ctxt),
1.70 - (f', Sundef(*FIXME is no value of next_tac! vor 8.6.03*))) (*finished*)
1.71 - else
1.72 - (case next_rule rss f of
1.73 - NONE => (Empty_Tac_, (Uistate, ctxt), (e_term, Sundef)) (*helpless*)
1.74 - | SOME (Thm (id,thm))(*8.6.03: muss auch f' liefern ?!!*) =>
1.75 - (Rewrite' (thy, "e_rew_ord", e_rls,(*!?!8.6.03*) false,
1.76 - (id, string_of_thmI thm), f,(e_term,[(*!?!8.6.03*)])),
1.77 - (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
1.78 + if f = f'
1.79 + then (End_Detail' (f',[])(*8.6.03*), (Uistate, ctxt),
1.80 + (f', Sundef(*FIXME is no value of next_tac! vor 8.6.03*))) (*finished*)
1.81 + else
1.82 + (case next_rule rss f of
1.83 + NONE => (Empty_Tac_, (Uistate, ctxt), (e_term, Sundef)) (*helpless*)
1.84 + | SOME (Thm (id,thm))(*8.6.03: muss auch f' liefern ?!!*) =>
1.85 + (Rewrite' (thy, "e_rew_ord", e_rls,(*!?!8.6.03*) false,
1.86 + (id, string_of_thmI thm), f,(e_term,[(*!?!8.6.03*)])),
1.87 + (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
1.88
1.89 | next_tac thy (ptp as (pt, pos as (p, _)):ptree * pos') (sc as Script (h $ body))
1.90 - (ScrState (E,l,a,v,s,b), ctxt) =
1.91 - (case if l = []
1.92 - then appy thy ptp E [R] body NONE v
1.93 - else nstep_up thy ptp sc E l Skip_ a v of
1.94 - Skip (v, _) => (*finished*)
1.95 - (case par_pbl_det pt p of
1.96 - (true, p', _) =>
1.97 - let val (_,pblID,_) = get_obj g_spec pt p';
1.98 - in (Check_Postcond' (pblID, (v, [(*assigned in next step*)])),
1.99 - (e_istate, ctxt), (v,s))
1.100 - end
1.101 - | (_, p', rls') =>
1.102 - (End_Detail' (e_term,[])(*8.6.03*), (e_istate, ctxt), (v,s)))
1.103 - | Napp _ => (Empty_Tac_, (e_istate, ctxt), (e_term, Sundef)) (*helpless*)
1.104 - | Appy (m', scrst as (_,_,_,v,_,_)) =>
1.105 - (m', (ScrState scrst, ctxt), (v, Sundef))) (*next stac*)
1.106 + (ScrState (E,l,a,v,s,b), ctxt) =
1.107 + (case if l = [] then appy thy ptp E [R] body NONE v
1.108 + else nstep_up thy ptp sc E l Skip_ a v of
1.109 + Skip (v, _) => (*finished*)
1.110 + (case par_pbl_det pt p of
1.111 + (true, p', _) =>
1.112 + let
1.113 + val (_,pblID,_) = get_obj g_spec pt p';
1.114 + in (Check_Postcond' (pblID, (v, [(*assigned in next step*)])),
1.115 + (e_istate, ctxt), (v,s))
1.116 + end
1.117 + | (_, p', rls') => (End_Detail' (e_term,[])(*8.6.03*), (e_istate, ctxt), (v,s)))
1.118 + | Napp _ => (Empty_Tac_, (e_istate, ctxt), (e_term, Sundef)) (*helpless*)
1.119 + | Appy (m', scrst as (_,_,_,v,_,_)) => (m', (ScrState scrst, ctxt), (v, Sundef))) (*next stac*)
1.120
1.121 | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (istate2str is));
1.122