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);*)
2.1 --- a/src/Tools/isac/Interpret/solve.sml Sun May 01 17:16:57 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/solve.sml Tue May 03 11:16:55 2011 +0200
2.3 @@ -1,8 +1,8 @@
2.4 -(* solve an example by interpreting a method's script
2.5 - (c) Walther Neuper 1999
2.6 -
2.7 -use"ME/solve.sml";
2.8 -use"solve.sml";
2.9 +(* Title: solve an example by interpreting a method's script
2.10 + Author: Walther Neuper 1999
2.11 + (c) copyright due to lincense terms.
2.12 +1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
2.13 + 10 20 30 40 50 60 70 80 90 100
2.14 *)
2.15
2.16 fun safe (ScrState (_,_,_,_,s,_)) = s
2.17 @@ -142,10 +142,9 @@
2.18 (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m);
2.19 val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos);
2.20 *)
2.21 -fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _))
2.22 - (pt:ptree, (pos as (p,_))) =
2.23 - let val {srls,...} = get_met mI;
2.24 - val PblObj{meth=itms,...} = get_obj I pt p;
2.25 +fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) (pt:ptree, (pos as (p,_))) =
2.26 + let val {srls, ...} = get_met mI;
2.27 + val PblObj {meth=itms, ...} = get_obj I pt p;
2.28 val thy' = get_obj g_domID pt p;
2.29 val thy = assoc_thy thy';
2.30 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
3.1 --- a/src/Tools/isac/ProgLang/Script.thy Sun May 01 17:16:57 2011 +0200
3.2 +++ b/src/Tools/isac/ProgLang/Script.thy Tue May 03 11:16:55 2011 +0200
3.3 @@ -162,7 +162,7 @@
3.4 "Take","Subproblem","Or'_to'_List"]));
3.5
3.6 val screxpr = Unsynchronized.ref (distinct (remove op = ""
3.7 - ["Let","If","Repeat","While","Try","Or"]));
3.8 + ["HOL.Let","If","Repeat","While","Try","Or"]));
3.9
3.10 val listfuns = Unsynchronized.ref [(*_all_ functions in Isa99.List.thy *)
3.11 "@","filter","concat","foldl","hd","last","set","list_all",
4.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Sun May 01 17:16:57 2011 +0200
4.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Tue May 03 11:16:55 2011 +0200
4.3 @@ -262,7 +262,7 @@
4.4
4.5 fun stacpbls (h $ body) =
4.6 let
4.7 - fun scan ts (Const ("Let",_) $ e $ (Abs (v,T,b))) =
4.8 + fun scan ts (Const ("HOL.Let",_) $ e $ (Abs (v,T,b))) =
4.9 (scan ts e) @ (scan ts b)
4.10 | scan ts (Const ("If",_) $ c $ e1 $ e2) = (scan ts e1) @ (scan ts e2)
4.11 | scan ts (Const ("Script.While",_) $ c $ e $ _) = scan ts e
5.1 --- a/src/Tools/isac/ProgLang/termC.sml Sun May 01 17:16:57 2011 +0200
5.2 +++ b/src/Tools/isac/ProgLang/termC.sml Tue May 03 11:16:55 2011 +0200
5.3 @@ -818,10 +818,10 @@
5.4 | inst_abs thy (Free sT) = Free sT
5.5 | inst_abs thy (Bound n) = Bound n
5.6 | inst_abs thy (Var iT) = Var iT
5.7 - | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v, T2, b))) =
5.8 + | inst_abs thy (Const ("HOL.Let",T1) $ e $ (Abs (v, T2, b))) =
5.9 let val b' = subst_bound (Free (v, T2), b);
5.10 (*fun variant_abs: term.ML*)
5.11 - in Const ("Let", T1) $ inst_abs thy e $ (Abs (v, T2, inst_abs thy b')) end
5.12 + in Const ("HOL.Let", T1) $ inst_abs thy e $ (Abs (v, T2, inst_abs thy b')) end
5.13 | inst_abs thy (t1 $ t2) = inst_abs thy t1 $ inst_abs thy t2
5.14 | inst_abs thy t = t;
5.15 (*val scr =
6.1 --- a/test/Tools/isac/Interpret/ctree.sml Sun May 01 17:16:57 2011 +0200
6.2 +++ b/test/Tools/isac/Interpret/ctree.sml Tue May 03 11:16:55 2011 +0200
6.3 @@ -11,6 +11,7 @@
6.4 "-----------------------------------------------------------------";
6.5 "-----------------------------------------------------------------";
6.6 "-------------- build miniscript stepwise BEFORE ALL TESTS -------";
6.7 +"-------------- check positions in miniscript --------------------";
6.8 "-------------- get_allpos' (from ptree above)--------------------";
6.9 (**#####################################################################(**)
6.10 "-------------- cut_level (from ptree above)----------------------";
6.11 @@ -61,9 +62,23 @@
6.12 "-------------- build miniscript stepwise BEFORE ALL TESTS -------";
6.13 "-------------- build miniscript stepwise BEFORE ALL TESTS -------";
6.14 "-------------- build miniscript stepwise BEFORE ALL TESTS -------";
6.15 -"this build should be detailed each time a test fails later \
6.16 -\i.e. all the tests should be caught here first \
6.17 -\and linked with a reference to the respective test environment";
6.18 +"this build should be detailed each time a test fails later ";
6.19 +"i.e. all the tests should be caught here first ";
6.20 +"and linked with a reference to the respective test environment ";
6.21 +val fmz = ["equality (x+1=(2::int))", (*FIRST OF ALL TESTS*) "solveFor x", "solutions L"];
6.22 +val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
6.23 + ["Test","squ-equ-test-subpbl1"]);
6.24 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.25 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.26 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.27 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.28 +
6.29 +
6.30 +
6.31 +
6.32 +"-------------- check positions in miniscript --------------------";
6.33 +"-------------- check positions in miniscript --------------------";
6.34 +"-------------- check positions in miniscript --------------------";
6.35 val fmz = ["equality (x+1=(2::int))",
6.36 "solveFor x","solutions L"];
6.37 val (dI',pI',mI') =
7.1 --- a/test/Tools/isac/Test_Isac.thy Sun May 01 17:16:57 2011 +0200
7.2 +++ b/test/Tools/isac/Test_Isac.thy Tue May 03 11:16:55 2011 +0200
7.3 @@ -4,6 +4,8 @@
7.4
7.5 $ cd /usr/local/isabisac/test/Tools/isac
7.6 $ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy &
7.7 +1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
7.8 + 10 20 30 40 50 60 70 80 90 100
7.9 *)
7.10
7.11 theory Test_Isac imports Isac
7.12 @@ -82,7 +84,106 @@
7.13 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
7.14 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
7.15 use "Interpret/mstools.sml" (*empty*)
7.16 -ML {*print_depth 5*}
7.17 +
7.18 +ML {*print_depth 5;
7.19 +val fmz = ["equality (x+1=(2::real))", (*FIRST OF ALL TESTS*) "solveFor x", "solutions L"];
7.20 +val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
7.21 + ["Test","squ-equ-test-subpbl1"]);
7.22 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.23 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.24 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.25 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.26 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.27 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.28 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.29 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.30 +"----- fun me, args:"; val (_,tac) = nxt;
7.31 +"----- fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
7.32 +val (mI,m) = mk_tac'_ tac;
7.33 +val Appl m = applicable_in p pt m;
7.34 +member op = specsteps mI; (*false*)
7.35 +"----- fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
7.36 +"----- fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
7.37 +val {srls, ...} = get_met mI;
7.38 +val PblObj {meth=itms, ...} = get_obj I pt p;
7.39 +val thy' = get_obj g_domID pt p;
7.40 +val thy = assoc_thy thy';
7.41 +val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
7.42 +val ini = init_form thy sc env; (*NONE*)
7.43 +*}
7.44 +ML {*
7.45 +"----- fun init_form, args:"; val (Script sc) = sc;
7.46 +"----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
7.47 +*}
7.48 +ML {*
7.49 + fun get_t y (Const ("Script.Seq",_) $ e1 $ e2) a =
7.50 + (writeln "Script.Seq";
7.51 + case get_t y e1 a of NONE => get_t y e2 a | la => la)
7.52 + | get_t y (Const ("Script.Seq",_) $ e1 $ e2 $ a) _ =
7.53 + (case get_t y e1 a of NONE => get_t y e2 a | la => la)
7.54 + | get_t y (Const ("Script.Try",_) $ e) a = (writeln "Script.Try 1";
7.55 + get_t y e a)
7.56 + | get_t y (Const ("Script.Try",_) $ e $ a) _ = (writeln "Script.Try 2";
7.57 + get_t y e a)
7.58 + | get_t y (Const ("Script.Repeat",_) $ e) a = get_t y e a
7.59 + | get_t y (Const ("Script.Repeat",_) $ e $ a) _ = get_t y e a
7.60 + | get_t y (Const ("Script.Or",_) $e1 $ e2) a =
7.61 + (case get_t y e1 a of NONE => get_t y e2 a | la => la)
7.62 + | get_t y (Const ("Script.Or",_) $e1 $ e2 $ a) _ =
7.63 + (case get_t y e1 a of NONE => get_t y e2 a | la => la)
7.64 + | get_t y (Const ("Script.While",_) $ c $ e) a = get_t y e a
7.65 + | get_t y (Const ("Script.While",_) $ c $ e $ a) _ = get_t y e a
7.66 + | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_,_,e2)) a =
7.67 + (case get_t y e1 a of NONE => get_t y e2 a | la => la)
7.68 + (*| get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
7.69 + (tracing("get_t: Let e1= "^(term2str e1)^", e2= "^(term2str e2));
7.70 + case get_t y e1 a of NONE => get_t y e2 a | la => la)
7.71 + | get_t y (Abs (_,_,e)) a = get_t y e a*)
7.72 + | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
7.73 + (writeln "HOL.Let";
7.74 + get_t y e1 a (*don't go deeper without evaluation !*))
7.75 + | get_t y (Const ("If",_) $ c $ e1 $ e2) a = NONE
7.76 + (*(case get_t y e1 a of NONE => get_t y e2 a | la => la)*)
7.77 +
7.78 + | get_t y (Const ("Script.Rewrite",_) $ _ $ _ $ a) _ = SOME a
7.79 + | get_t y (Const ("Script.Rewrite",_) $ _ $ _ ) a = SOME a
7.80 + | get_t y (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ a) _ = SOME a
7.81 + | get_t y (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ ) a = SOME a
7.82 + | get_t y (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ a) _ =
7.83 + (writeln "Script.Rewrite'_Set 1";
7.84 + SOME a)
7.85 + | get_t y (Const ("Script.Rewrite'_Set",_) $ _ $ _ ) a =
7.86 + (writeln "Script.Rewrite'_Set 2";
7.87 + SOME a)
7.88 + | get_t y (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $a)_ =SOME a
7.89 + | get_t y (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ ) a =SOME a
7.90 + | get_t y (Const ("Script.Calculate",_) $ _ $ a) _ = SOME a
7.91 + | get_t y (Const ("Script.Calculate",_) $ _ ) a = SOME a
7.92 +
7.93 + | get_t y (Const ("Script.Substitute",_) $ _ $ a) _ = SOME a
7.94 + | get_t y (Const ("Script.Substitute",_) $ _ ) a = SOME a
7.95 +
7.96 + | get_t y (Const ("Script.SubProblem",_) $ _ $ _) _ = NONE
7.97 +
7.98 + | get_t y x _ =
7.99 + ((*tracing ("### get_t yac: list-expr "^(term2str x));*)
7.100 + NONE);
7.101 +*}
7.102 +ML {*
7.103 +case get_t thy body e_term of SOME (Free ("e_e", _)) => ()
7.104 +| _ => error "script: Const in script (as term) changed";
7.105 +get_stac thy sc;
7.106 +(*========== inhibit exn 110323 ================================================
7.107 +print_depth 999; sc;
7.108 +val p = lev_dn p;
7.109 +val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
7.110 +val Check_Postcond' (_, (ttt,_)) = m';
7.111 +term2str ttt; (*is the whole script*)
7.112 +solve m (pt, pos);
7.113 +loc_solve_ (mI,m) ptp;
7.114 +locatetac tac (pt,p);
7.115 +============ inhibit exn 110loc_solve_ (mI,m) ptp323 ==============================================*)
7.116 +*}
7.117 use "Interpret/ctree.sml"
7.118 use "Interpret/ptyps.sml" (* *)
7.119 (*use "Interpret/generate.sml" new 2011*)