1.1 --- a/src/Tools/isac/ProgLang/Script.thy Tue May 03 11:16:55 2011 +0200
1.2 +++ b/src/Tools/isac/ProgLang/Script.thy Tue May 03 15:58:04 2011 +0200
1.3 @@ -162,7 +162,7 @@
1.4 "Take","Subproblem","Or'_to'_List"]));
1.5
1.6 val screxpr = Unsynchronized.ref (distinct (remove op = ""
1.7 - ["HOL.Let","If","Repeat","While","Try","Or"]));
1.8 + ["Let","If","Repeat","While","Try","Or"]));
1.9
1.10 val listfuns = Unsynchronized.ref [(*_all_ functions in Isa99.List.thy *)
1.11 "@","filter","concat","foldl","hd","last","set","list_all",
2.1 --- a/test/Tools/isac/Interpret/script.sml Tue May 03 11:16:55 2011 +0200
2.2 +++ b/test/Tools/isac/Interpret/script.sml Tue May 03 15:58:04 2011 +0200
2.3 @@ -12,10 +12,12 @@
2.4 "----------- WN0509 why does next_tac doesnt find Substitute -----";
2.5 "----------- WN0509 Substitute 2nd part --------------------------";
2.6 "----------- fun sel_appl_atomic_tacs ----------------------------";
2.7 +"----------- fun init_form, fun get_stac -------------------------";
2.8 "-----------------------------------------------------------------";
2.9 "-----------------------------------------------------------------";
2.10 "-----------------------------------------------------------------";
2.11
2.12 +(*========== inhibit exn 110503 ================================================
2.13
2.14 "----------- WN0509 why does next_tac doesnt find Substitute -----";
2.15 "----------- WN0509 why does next_tac doesnt find Substitute -----";
2.16 @@ -247,4 +249,37 @@
2.17 \1 stac too low";
2.18 applyTactic 1 p (hd appltacs);
2.19 autoCalculate 1 CompleteCalc;
2.20 +============ inhibit exn 110503 ==============================================*)
2.21
2.22 +"----------- fun init_form, fun get_stac -------------------------";
2.23 +"----------- fun init_form, fun get_stac -------------------------";
2.24 +"----------- fun init_form, fun get_stac -------------------------";
2.25 +val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
2.26 +val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
2.27 + ["Test","squ-equ-test-subpbl1"]);
2.28 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.29 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.30 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.31 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.32 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.33 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.34 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.35 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.36 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
2.37 +"~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
2.38 +val (mI,m) = mk_tac'_ tac;
2.39 +val Appl m = applicable_in p pt m;
2.40 +member op = specsteps mI; (*false*)
2.41 +"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
2.42 +"~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
2.43 +val {srls, ...} = get_met mI;
2.44 +val PblObj {meth=itms, ...} = get_obj I pt p;
2.45 +val thy' = get_obj g_domID pt p;
2.46 +val thy = assoc_thy thy';
2.47 +val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
2.48 +val ini = init_form thy sc env;
2.49 +"----- fun init_form, args:"; val (Script sc) = sc;
2.50 +"----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
2.51 +case get_stac thy sc of SOME (Free ("e_e", _)) => ()
2.52 +| _ => error "script: Const (?, ?) in script (as term) changed";;
2.53 +
3.1 --- a/test/Tools/isac/Test_Isac.thy Tue May 03 11:16:55 2011 +0200
3.2 +++ b/test/Tools/isac/Test_Isac.thy Tue May 03 15:58:04 2011 +0200
3.3 @@ -68,10 +68,8 @@
3.4 ("Knowledge/diophanteq.sml")
3.5 ("Knowledge/isac.sml")
3.6
3.7 -
3.8 begin
3.9
3.10 - ML {*print_depth 100*}
3.11 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
3.12 use "library.sml" (*new 2011*)
3.13 use "calcelems.sml" (*complete*)
3.14 @@ -84,113 +82,13 @@
3.15 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
3.16 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
3.17 use "Interpret/mstools.sml" (*empty*)
3.18 -
3.19 -ML {*print_depth 5;
3.20 -val fmz = ["equality (x+1=(2::real))", (*FIRST OF ALL TESTS*) "solveFor x", "solutions L"];
3.21 -val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
3.22 - ["Test","squ-equ-test-subpbl1"]);
3.23 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.24 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.25 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.26 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.27 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.28 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.29 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.30 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.31 -"----- fun me, args:"; val (_,tac) = nxt;
3.32 -"----- fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
3.33 -val (mI,m) = mk_tac'_ tac;
3.34 -val Appl m = applicable_in p pt m;
3.35 -member op = specsteps mI; (*false*)
3.36 -"----- fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
3.37 -"----- fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
3.38 -val {srls, ...} = get_met mI;
3.39 -val PblObj {meth=itms, ...} = get_obj I pt p;
3.40 -val thy' = get_obj g_domID pt p;
3.41 -val thy = assoc_thy thy';
3.42 -val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
3.43 -val ini = init_form thy sc env; (*NONE*)
3.44 -*}
3.45 -ML {*
3.46 -"----- fun init_form, args:"; val (Script sc) = sc;
3.47 -"----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
3.48 -*}
3.49 -ML {*
3.50 - fun get_t y (Const ("Script.Seq",_) $ e1 $ e2) a =
3.51 - (writeln "Script.Seq";
3.52 - case get_t y e1 a of NONE => get_t y e2 a | la => la)
3.53 - | get_t y (Const ("Script.Seq",_) $ e1 $ e2 $ a) _ =
3.54 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
3.55 - | get_t y (Const ("Script.Try",_) $ e) a = (writeln "Script.Try 1";
3.56 - get_t y e a)
3.57 - | get_t y (Const ("Script.Try",_) $ e $ a) _ = (writeln "Script.Try 2";
3.58 - get_t y e a)
3.59 - | get_t y (Const ("Script.Repeat",_) $ e) a = get_t y e a
3.60 - | get_t y (Const ("Script.Repeat",_) $ e $ a) _ = get_t y e a
3.61 - | get_t y (Const ("Script.Or",_) $e1 $ e2) a =
3.62 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
3.63 - | get_t y (Const ("Script.Or",_) $e1 $ e2 $ a) _ =
3.64 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
3.65 - | get_t y (Const ("Script.While",_) $ c $ e) a = get_t y e a
3.66 - | get_t y (Const ("Script.While",_) $ c $ e $ a) _ = get_t y e a
3.67 - | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_,_,e2)) a =
3.68 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
3.69 - (*| get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
3.70 - (tracing("get_t: Let e1= "^(term2str e1)^", e2= "^(term2str e2));
3.71 - case get_t y e1 a of NONE => get_t y e2 a | la => la)
3.72 - | get_t y (Abs (_,_,e)) a = get_t y e a*)
3.73 - | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
3.74 - (writeln "HOL.Let";
3.75 - get_t y e1 a (*don't go deeper without evaluation !*))
3.76 - | get_t y (Const ("If",_) $ c $ e1 $ e2) a = NONE
3.77 - (*(case get_t y e1 a of NONE => get_t y e2 a | la => la)*)
3.78 -
3.79 - | get_t y (Const ("Script.Rewrite",_) $ _ $ _ $ a) _ = SOME a
3.80 - | get_t y (Const ("Script.Rewrite",_) $ _ $ _ ) a = SOME a
3.81 - | get_t y (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ a) _ = SOME a
3.82 - | get_t y (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ ) a = SOME a
3.83 - | get_t y (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ a) _ =
3.84 - (writeln "Script.Rewrite'_Set 1";
3.85 - SOME a)
3.86 - | get_t y (Const ("Script.Rewrite'_Set",_) $ _ $ _ ) a =
3.87 - (writeln "Script.Rewrite'_Set 2";
3.88 - SOME a)
3.89 - | get_t y (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $a)_ =SOME a
3.90 - | get_t y (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ ) a =SOME a
3.91 - | get_t y (Const ("Script.Calculate",_) $ _ $ a) _ = SOME a
3.92 - | get_t y (Const ("Script.Calculate",_) $ _ ) a = SOME a
3.93 -
3.94 - | get_t y (Const ("Script.Substitute",_) $ _ $ a) _ = SOME a
3.95 - | get_t y (Const ("Script.Substitute",_) $ _ ) a = SOME a
3.96 -
3.97 - | get_t y (Const ("Script.SubProblem",_) $ _ $ _) _ = NONE
3.98 -
3.99 - | get_t y x _ =
3.100 - ((*tracing ("### get_t yac: list-expr "^(term2str x));*)
3.101 - NONE);
3.102 -*}
3.103 -ML {*
3.104 -case get_t thy body e_term of SOME (Free ("e_e", _)) => ()
3.105 -| _ => error "script: Const in script (as term) changed";
3.106 -get_stac thy sc;
3.107 -(*========== inhibit exn 110323 ================================================
3.108 -print_depth 999; sc;
3.109 -val p = lev_dn p;
3.110 -val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
3.111 -val Check_Postcond' (_, (ttt,_)) = m';
3.112 -term2str ttt; (*is the whole script*)
3.113 -solve m (pt, pos);
3.114 -loc_solve_ (mI,m) ptp;
3.115 -locatetac tac (pt,p);
3.116 -============ inhibit exn 110loc_solve_ (mI,m) ptp323 ==============================================*)
3.117 -*}
3.118 use "Interpret/ctree.sml"
3.119 use "Interpret/ptyps.sml" (* *)
3.120 (*use "Interpret/generate.sml" new 2011*)
3.121 use "Interpret/calchead.sml" (* *)
3.122 (*use "Interpret/appl.sml" new 2011*)
3.123 use "Interpret/rewtools.sml" (* *)
3.124 -(*use "Interpret/script.sml" TODO*)
3.125 + use "Interpret/script.sml" (*TODO*)
3.126 (*use "Interpret/solve.sml" TODO*)
3.127 (*use "Interpret/inform.sml" TODO*)
3.128 use "Interpret/mathengine.sml"(*part.*)
3.129 @@ -249,12 +147,12 @@
3.130 (*=== inhibit exn ?=============================================================
3.131 ===== inhibit exn ?===========================================================*)
3.132
3.133 -(*========== inhibit exn 110323 ================================================
3.134 +(*========== inhibit exn 110503 ================================================
3.135
3.136 "########### testcode inserted vvv ###########################################";
3.137 "########### testcode inserted ^^^ ###########################################";
3.138
3.139 -============ inhibit exn 110323 ==============================================*)
3.140 +============ inhibit exn 110503 ==============================================*)
3.141
3.142 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
3.143 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)