1.1 --- a/src/Tools/isac/Interpret/script.sml Sun May 01 17:16:57 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Tue May 03 11:16:55 2011 +0200
1.3 @@ -150,7 +150,7 @@
1.4 \ (let e_ = Try (Rewrite square_equation_left True eq_) \
1.5 \ in [e_])");
1.6 ______ compares head_of !!
1.7 -> get [] (eq_str "Let") sss; [R]
1.8 +> get [] (eq_str "HOL.Let") sss; [R]
1.9 > get [] (eq_str "Script.Try") sss; [R,L,R]
1.10 > get [] (eq_str "Script.Rewrite") sss; [R,L,R,R]
1.11 > get [] (eq_str "HOL.True") sss; [R,L,R,R,L,R]
1.12 @@ -163,8 +163,6 @@
1.13
1.14 (*.get argument of first stactic in a script for init_form.*)
1.15 fun get_stac thy (h $ body) =
1.16 -(*
1.17 - *)
1.18 let
1.19 fun get_t y (Const ("Script.Seq",_) $ e1 $ e2) a =
1.20 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.21 @@ -182,11 +180,11 @@
1.22 | get_t y (Const ("Script.While",_) $ c $ e $ a) _ = get_t y e a
1.23 | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_,_,e2)) a =
1.24 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.25 - (*| get_t y (Const ("Let",_) $ e1 $ Abs (_,_,e2)) a =
1.26 + (*| get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
1.27 (tracing("get_t: Let e1= "^(term2str e1)^", e2= "^(term2str e2));
1.28 case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.29 | get_t y (Abs (_,_,e)) a = get_t y e a*)
1.30 - | get_t y (Const ("Let",_) $ e1 $ Abs (_,_,e2)) a =
1.31 + | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
1.32 get_t y e1 a (*don't go deeper without evaluation !*)
1.33 | get_t y (Const ("If",_) $ c $ e1 $ e2) a = NONE
1.34 (*(case get_t y e1 a of NONE => get_t y e2 a | la => la)*)
1.35 @@ -981,8 +979,8 @@
1.36 there was an appl.stac (Repeat, Or e1, ...)
1.37 *)
1.38 fun assy ya (is as (E,l,a,v,S,b),ss)
1.39 - (Const ("Let",_) $ e $ (Abs (id,T,body))) =
1.40 -(* val (ya, (is as (E,l,a,v,S,b),ss),Const ("Let",_) $ e $ (Abs (id,T,body))) =
1.41 + (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))) =
1.42 +(* val (ya, (is as (E,l,a,v,S,b),ss),Const ("HOL.Let",_) $ e $ (Abs (id,T,body))) =
1.43 (*1*)(((ts,d),Aundef), ((E,[R],a,v,S,b),[(m,EmptyMout,pt,p,[])]), body);
1.44 *)
1.45 ((*tracing("### assy Let$e$Abs: is=");
1.46 @@ -1136,15 +1134,15 @@
1.47 *)
1.48
1.49
1.50 -(* val (ys as (y,s,Script sc,d),(is as (E,l,a,v,S,b),ss),Const ("Let",_) $ _) =
1.51 +(* val (ys as (y,s,Script sc,d),(is as (E,l,a,v,S,b),ss),Const ("HOL.Let",_) $ _) =
1.52 (ys, ((E,up,a,v,S,b),ss), go up sc);
1.53 *)
1.54 fun ass_up (ys as (y,s,Script sc,d)) (is as (E,l,a,v,S,b),ss)
1.55 - (Const ("Let",_) $ _) =
1.56 + (Const ("HOL.Let",_) $ _) =
1.57 let (*val _= tracing("### ass_up1 Let$e: is=")
1.58 val _= tracing(istate2str (ScrState is))*)
1.59 val l = drop_last l; (*comes from e, goes to Abs*)
1.60 - val (Const ("Let",_) $ e $ (Abs (i,T,body))) = go l sc;
1.61 + val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
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 @@ -1158,7 +1156,7 @@
1.66 tracing(istate2str (ScrState is));*)
1.67 astep_up ys iss) (*TODO 5.9.00: env ?*)
1.68
1.69 - | ass_up ys (iss as (is,_)) (Const ("Let",_) $ e $ (Abs (i,T,b)))=
1.70 + | ass_up ys (iss as (is,_)) (Const ("HOL.Let",_) $ e $ (Abs (i,T,b)))=
1.71 ((*tracing("### ass_up Let $ e $ Abs: is=");
1.72 tracing(istate2str (ScrState is));*)
1.73 astep_up ys iss) (*TODO 5.9.00: env ?*)
1.74 @@ -1428,8 +1426,8 @@
1.75 because 'nxt_up Or e1' treats as Appy*)
1.76
1.77 fun appy thy ptp E l
1.78 - (t as Const ("Let",_) $ e $ (Abs (i,T,b))) a v =
1.79 -(* val (thy, ptp, E, l, t as Const ("Let",_) $ e $ (Abs (i,T,b)),a, v)=
1.80 + (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v =
1.81 +(* val (thy, ptp, E, l, t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b)),a, v)=
1.82 (thy, ptp, E, up@[R,D], body, a, v);
1.83 appy thy ptp E l t a v;
1.84 *)
1.85 @@ -1574,23 +1572,23 @@
1.86 end);
1.87
1.88
1.89 -(* val (scr as Script sc, l, t as Const ("Let",_) $ _) =
1.90 +(* val (scr as Script sc, l, t as Const ("HOL.Let",_) $ _) =
1.91 (Script sc, up, go up sc);
1.92 nxt_up thy ptp (Script sc) E l ay t a v;
1.93
1.94 - val (thy,ptp,scr as (Script sc),E,l, ay, t as Const ("Let",_) $ _, a, v)=
1.95 + val (thy,ptp,scr as (Script sc),E,l, ay, t as Const ("HOL.Let",_) $ _, a, v)=
1.96 (thy,ptp,Script sc, E,up,ay, go up sc, a, v);
1.97 nxt_up thy ptp scr E l ay t a v;
1.98 *)
1.99 fun nxt_up thy ptp (scr as (Script sc)) E l ay
1.100 - (t as Const ("Let",_) $ _) a v = (*comes from let=...*)
1.101 + (t as Const ("HOL.Let",_) $ _) a v = (*comes from let=...*)
1.102 ((*tracing("### nxt_up1 Let$e: is=");
1.103 tracing(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
1.104 if ay = Napp_
1.105 then nstep_up thy ptp scr E (drop_last l) Napp_ a v
1.106 else (*Skip_*)
1.107 let val up = drop_last l;
1.108 - val (Const ("Let",_) $ e $ (Abs (i,T,body))) = go up sc;
1.109 + val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc;
1.110 val i = mk_Free (i, T);
1.111 val E = upd_env E (i, v);
1.112 (*val _= tracing("### nxt_up2 Let$e: is=");
1.113 @@ -1606,7 +1604,7 @@
1.114 nstep_up thy ptp scr E (*enr*) l ay a v)
1.115
1.116 | nxt_up thy ptp scr E l ay
1.117 - (t as Const ("Let",_) $ e $ (Abs (i,T,b))) a v =
1.118 + (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v =
1.119 ((*tracing("### nxt_up Let$e$Abs: is=");
1.120 tracing(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
1.121 (*tracing("### nxt_up Let e Abs: " ^ term2str t);*)