# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1304431084 -7200
# Node ID a350b4ed575bd7738b88042eb8b1cccc2353f9a7
# Parent  3228aa46fd300b532779ed2f6087a1b1d36c5a2e
tuned, tests work

diff -r 3228aa46fd30 -r a350b4ed575b src/Tools/isac/ProgLang/Script.thy
--- a/src/Tools/isac/ProgLang/Script.thy	Tue May 03 11:16:55 2011 +0200
+++ b/src/Tools/isac/ProgLang/Script.thy	Tue May 03 15:58:04 2011 +0200
@@ -162,7 +162,7 @@
    "Take","Subproblem","Or'_to'_List"]));
 
 val screxpr = Unsynchronized.ref (distinct (remove op = ""
-  ["HOL.Let","If","Repeat","While","Try","Or"]));
+  ["Let","If","Repeat","While","Try","Or"]));
 
 val listfuns = Unsynchronized.ref [(*_all_ functions in Isa99.List.thy *)
     "@","filter","concat","foldl","hd","last","set","list_all",
diff -r 3228aa46fd30 -r a350b4ed575b test/Tools/isac/Interpret/script.sml
--- a/test/Tools/isac/Interpret/script.sml	Tue May 03 11:16:55 2011 +0200
+++ b/test/Tools/isac/Interpret/script.sml	Tue May 03 15:58:04 2011 +0200
@@ -12,10 +12,12 @@
 "----------- WN0509 why does next_tac doesnt find Substitute -----";
 "----------- WN0509 Substitute 2nd part --------------------------";
 "----------- fun sel_appl_atomic_tacs ----------------------------";
+"----------- fun init_form, fun get_stac -------------------------";
 "-----------------------------------------------------------------";
 "-----------------------------------------------------------------";
 "-----------------------------------------------------------------";
 
+(*========== inhibit exn 110503 ================================================
 
 "----------- WN0509 why does next_tac doesnt find Substitute -----";
 "----------- WN0509 why does next_tac doesnt find Substitute -----";
@@ -247,4 +249,37 @@
  \1 stac too low";
 applyTactic 1 p (hd appltacs);
 autoCalculate 1 CompleteCalc;
+============ inhibit exn 110503 ==============================================*)
 
+"----------- fun init_form, fun get_stac -------------------------";
+"----------- fun init_form, fun get_stac -------------------------";
+"----------- fun init_form, fun get_stac -------------------------";
+val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
+val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
+  ["Test","squ-equ-test-subpbl1"]);
+val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
+val (p,_,f,nxt,_,pt) = me nxt p [] pt;
+val (p,_,f,nxt,_,pt) = me nxt p [] pt;
+val (p,_,f,nxt,_,pt) = me nxt p [] pt;
+val (p,_,f,nxt,_,pt) = me nxt p [] pt;
+val (p,_,f,nxt,_,pt) = me nxt p [] pt;
+val (p,_,f,nxt,_,pt) = me nxt p [] pt;
+val (p,_,f,nxt,_,pt) = me nxt p [] pt;
+"~~~~~ fun me, args:"; val (_,tac) = nxt;
+"~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
+val (mI,m) = mk_tac'_ tac;
+val Appl m = applicable_in p pt m;
+member op = specsteps mI; (*false*)
+"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
+"~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
+val {srls, ...} = get_met mI;
+val PblObj {meth=itms, ...} = get_obj I pt p;
+val thy' = get_obj g_domID pt p;
+val thy = assoc_thy thy';
+val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
+val ini = init_form thy sc env;
+"----- fun init_form, args:"; val (Script sc) = sc;
+"----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
+case get_stac thy sc of SOME (Free ("e_e", _)) => ()
+| _ => error "script: Const (?, ?) in script (as term) changed";;
+
diff -r 3228aa46fd30 -r a350b4ed575b test/Tools/isac/Test_Isac.thy
--- a/test/Tools/isac/Test_Isac.thy	Tue May 03 11:16:55 2011 +0200
+++ b/test/Tools/isac/Test_Isac.thy	Tue May 03 15:58:04 2011 +0200
@@ -68,10 +68,8 @@
   ("Knowledge/diophanteq.sml")
   ("Knowledge/isac.sml")
 
-
 begin
 
-  ML {*print_depth 100*}
   ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
   use          "library.sml"        (*new 2011*)
   use          "calcelems.sml"      (*complete*)
@@ -84,113 +82,13 @@
   ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
   ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
   use "Interpret/mstools.sml"       (*empty*)
-
-ML {*print_depth 5;
-val fmz = ["equality (x+1=(2::real))", (*FIRST OF ALL TESTS*) "solveFor x", "solutions L"];
-val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
-  ["Test","squ-equ-test-subpbl1"]);
-val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
-val (p,_,f,nxt,_,pt) = me nxt p [] pt;
-val (p,_,f,nxt,_,pt) = me nxt p [] pt;
-val (p,_,f,nxt,_,pt) = me nxt p [] pt;
-val (p,_,f,nxt,_,pt) = me nxt p [] pt;
-val (p,_,f,nxt,_,pt) = me nxt p [] pt;
-val (p,_,f,nxt,_,pt) = me nxt p [] pt;
-val (p,_,f,nxt,_,pt) = me nxt p [] pt;
-"----- fun me, args:"; val (_,tac) = nxt;
-"----- fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
-val (mI,m) = mk_tac'_ tac;
-val Appl m = applicable_in p pt m;
-member op = specsteps mI; (*false*)
-"----- fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
-"----- fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
-val {srls, ...} = get_met mI;
-val PblObj {meth=itms, ...} = get_obj I pt p;
-val thy' = get_obj g_domID pt p;
-val thy = assoc_thy thy';
-val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
-val ini = init_form thy sc env; (*NONE*)
-*}
-ML {*
-"----- fun init_form, args:"; val (Script sc) = sc;
-"----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
-*}
-ML {*
-    fun get_t y (Const ("Script.Seq",_) $ e1 $ e2) a = 
-    	(writeln "Script.Seq";
-    	  case get_t y e1 a of NONE => get_t y e2 a | la => la)
-      | get_t y (Const ("Script.Seq",_) $ e1 $ e2 $ a) _ = 
-    	(case get_t y e1 a of NONE => get_t y e2 a | la => la)
-      | get_t y (Const ("Script.Try",_) $ e) a = (writeln "Script.Try 1";
-                                                  get_t y e a)
-      | get_t y (Const ("Script.Try",_) $ e $ a) _ = (writeln "Script.Try 2";
-                                                  get_t y e a)
-      | get_t y (Const ("Script.Repeat",_) $ e) a = get_t y e a
-      | get_t y (Const ("Script.Repeat",_) $ e $ a) _ = get_t y e a
-      | get_t y (Const ("Script.Or",_) $e1 $ e2) a =
-    	(case get_t y e1 a of NONE => get_t y e2 a | la => la)
-      | get_t y (Const ("Script.Or",_) $e1 $ e2 $ a) _ =
-    	(case get_t y e1 a of NONE => get_t y e2 a | la => la)
-      | get_t y (Const ("Script.While",_) $ c $ e) a = get_t y e a
-      | get_t y (Const ("Script.While",_) $ c $ e $ a) _ = get_t y e a
-      | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_,_,e2)) a = 
-    	(case get_t y e1 a of NONE => get_t y e2 a | la => la)
-    (*| get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
-    	(tracing("get_t: Let e1= "^(term2str e1)^", e2= "^(term2str e2));
-	 case get_t y e1 a of NONE => get_t y e2 a | la => la)
-      | get_t y (Abs (_,_,e)) a = get_t y e a*)
-      | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
-    	(writeln "HOL.Let";
-    	  get_t y e1 a (*don't go deeper without evaluation !*))
-      | get_t y (Const ("If",_) $ c $ e1 $ e2) a = NONE
-    	(*(case get_t y e1 a of NONE => get_t y e2 a | la => la)*)
-    
-      | get_t y (Const ("Script.Rewrite",_) $ _ $ _ $ a) _ = SOME a
-      | get_t y (Const ("Script.Rewrite",_) $ _ $ _    ) a = SOME a
-      | get_t y (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ a) _ = SOME a
-      | get_t y (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ )    a = SOME a
-      | get_t y (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ a) _ = 
-                                                (writeln "Script.Rewrite'_Set 1";
-                                                 SOME a)
-      | get_t y (Const ("Script.Rewrite'_Set",_) $ _ $ _ )    a = 
-                                                (writeln "Script.Rewrite'_Set 2";
-                                                 SOME a)
-      | get_t y (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $a)_ =SOME a
-      | get_t y (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ )  a =SOME a
-      | get_t y (Const ("Script.Calculate",_) $ _ $ a) _ = SOME a
-      | get_t y (Const ("Script.Calculate",_) $ _ )    a = SOME a
-    
-      | get_t y (Const ("Script.Substitute",_) $ _ $ a) _ = SOME a
-      | get_t y (Const ("Script.Substitute",_) $ _ )    a = SOME a
-    
-      | get_t y (Const ("Script.SubProblem",_) $ _ $ _) _ = NONE
-
-      | get_t y x _ =  
-	((*tracing ("### get_t yac: list-expr "^(term2str x));*)
-	 NONE);
-*}
-ML {*
-case get_t thy body e_term of SOME (Free ("e_e", _)) => ()
-| _ => error "script: Const in script (as term) changed";
-get_stac thy sc;
-(*========== inhibit exn 110323 ================================================
-print_depth 999; sc;
-val p = lev_dn p;
-val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
-val Check_Postcond' (_, (ttt,_)) = m';
-term2str ttt; (*is the whole script*)
-solve m (pt, pos);
-loc_solve_ (mI,m) ptp;
-locatetac tac (pt,p);
-============ inhibit exn 110loc_solve_ (mI,m) ptp323 ==============================================*)
-*}
   use "Interpret/ctree.sml"
   use "Interpret/ptyps.sml"         (*    *)
 (*use "Interpret/generate.sml"        new 2011*)
   use "Interpret/calchead.sml"      (*    *)
 (*use "Interpret/appl.sml"            new 2011*)
   use "Interpret/rewtools.sml"      (*    *)
-(*use "Interpret/script.sml"          TODO*)
+  use "Interpret/script.sml"        (*TODO*)
 (*use "Interpret/solve.sml"           TODO*)
 (*use "Interpret/inform.sml"          TODO*)
   use "Interpret/mathengine.sml"(*part.*)
@@ -249,12 +147,12 @@
 (*=== inhibit exn ?=============================================================
 ===== inhibit exn ?===========================================================*)
 
-(*========== inhibit exn 110323 ================================================
+(*========== inhibit exn 110503 ================================================
 
 "########### testcode inserted vvv ###########################################";
 "########### testcode inserted ^^^ ###########################################";
 
-============ inhibit exn 110323 ==============================================*)
+============ inhibit exn 110503 ==============================================*)
 
 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)