1.1 --- a/src/Tools/isac/Test_Isac.thy	Fri Mar 18 18:27:10 2011 +0100
     1.2 +++ b/src/Tools/isac/Test_Isac.thy	Sat Mar 19 13:06:19 2011 +0100
     1.3 @@ -54,8 +54,7 @@
     1.4  cd"smltest/ME";
     1.5  *)
     1.6  use "../../../test/Tools/isac/Interpret/mstools.sml" (*empty*)
     1.7 -(*      use"ctree.sml";
     1.8 -*)
     1.9 +use "../../../test/Tools/isac/Interpret/ctree.sml"   (*part.*)
    1.10  use "../../../test/Tools/isac/Interpret/ptyps.sml"   (*TODO*)
    1.11  use "../../../test/Tools/isac/Interpret/calchead.sml"
    1.12  
    1.13 @@ -105,13 +104,14 @@
    1.14          ((SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)), ctxt),
    1.15            NONE),
    1.16  *)
    1.17 -
    1.18  *}
    1.19  
    1.20  ML {*
    1.21  "===== interactive specification: from origin to specification (probl)";
    1.22 -val (p,_,_,nxt,_,pt) = me nxt p [1] pt; (*Model_Problem*)
    1.23 +val (p,_,_,nxt,_,pt) = me nxt p [1] pt; 
    1.24 +  (*nxt =("Add_Given", Model_Problem)*)
    1.25  val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
    1.26 +  (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
    1.27  "----- ";
    1.28  (* call sequence: me Model_Problem 
    1.29                  > me ("Add_Given", Add_Given "realTestGiven (((1 + 2) * 4 / 3) ^^^ 2)")
    1.30 @@ -128,43 +128,58 @@
    1.31     FROM parse thy str
    1.32     TO   parseNEW ctxt str
    1.33  *)
    1.34 +val (p,_,_,nxt,_,pt) = me nxt p [1] pt; 
    1.35 +  (*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
    1.36 +val (p,_,_,nxt,_,pt) = me nxt p [1] pt; 
    1.37 +  (*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
    1.38  *}
    1.39  
    1.40  ML {*
    1.41 -
    1.42 -
    1.43  "===== end specify: from specification (probl) to guard (method)";
    1.44 -val (p,_,_,nxt,_,pt) = me nxt p [1] pt; 
    1.45 -val (p,_,_,nxt,_,pt) = me nxt p [1] pt; 
    1.46 -"----- ";
    1.47 -
    1.48 -
    1.49 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.50 +  (*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)
    1.51  *}
    1.52  
    1.53  ML {*
    1.54 -
    1.55 +"===== start interpretation: from guard to environment";
    1.56 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.57 +  (*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)
    1.58 +"----- ";
    1.59 +(* call sequence: me ("Apply_Method",...
    1.60 +                > locatetac
    1.61 +                > loc_solve_
    1.62 +                > solve ("Apply_Method",...
    1.63 +*)
    1.64 +val ((_,tac), ptp) = (nxt, (pt, p));
    1.65 +locatetac tac (pt,p);
    1.66 +  val (mI, m) = mk_tac'_ tac;
    1.67 +  val Appl m = applicable_in p pt m;
    1.68 +  member op = specsteps mI;
    1.69 +  loc_solve_ (mI,m) ptp;
    1.70 +    val (m, (pt, pos)) = ((mI,m), ptp);
    1.71 +    solve m (pt, pos);
    1.72 +      val ((_, m as Apply_Method' (mI, _, _)), (pt, (pos as (p,_)))) = 
    1.73 +        (m, (pt, pos));
    1.74 +      val {srls,...} = get_met mI;
    1.75 +      val PblObj{meth=itms,...} = get_obj I pt p;
    1.76 +      val thy' = get_obj g_domID pt p;
    1.77 +      val thy = assoc_thy thy';
    1.78 +      val (is as ScrState (env,_,_,_,_,_), sc) = init_scrstate thy itms mI;
    1.79  *}
    1.80  
    1.81  ML {*
    1.82  *}
    1.83  
    1.84  ML {*
    1.85 -
    1.86 -
    1.87 -"===== start interpretation: from guard to environment";
    1.88 -"----- ";
    1.89 -
    1.90 -
    1.91 -
    1.92 -
    1.93  "===== tactic Subproblem: from environment to origin";
    1.94  "----- ";
    1.95 +TODO
    1.96 +*}
    1.97  
    1.98  
    1.99  
   1.100  
   1.101  
   1.102 -*}
   1.103  
   1.104  ML {*print_depth 999*}
   1.105  use "../../../test/Tools/isac/Interpret/rewtools.sml" (**)
   1.106 @@ -298,12 +313,12 @@
   1.107  ===== inhibit exn ?===========================================================*)
   1.108  
   1.109  
   1.110 -(*========== inhibit exn WN110318 ==============================================
   1.111 +(*========== inhibit exn WN110319 ==============================================
   1.112  
   1.113  "########### testcode inserted vvv ###########################################";
   1.114  "########### testcode inserted ^^^ ###########################################";
   1.115  
   1.116 -============ inhibit exn WN110318 ============================================*)
   1.117 +============ inhibit exn WN110319 ============================================*)
   1.118  
   1.119  
   1.120  (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

     2.1 --- a/test/Tools/isac/Interpret/ctree.sml	Fri Mar 18 18:27:10 2011 +0100
     2.2 +++ b/test/Tools/isac/Interpret/ctree.sml	Sat Mar 19 13:06:19 2011 +0100
     2.3 @@ -94,6 +94,7 @@
     2.4  "ctree.sml-------------- cappend on complete ctree from above ----";
     2.5  val (pt', cuts) = cappend_form pt [1] e_istate (str2term "Inform[1]");
     2.6  "----------------------------------------------------------------/";
     2.7 +(*========== inhibit exn WN110319 ==============================================
     2.8  val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[1]*);
     2.9  val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[1]*);
    2.10  val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[2]*);
    2.11 @@ -119,7 +120,9 @@
    2.12  else error "new behaviour in test: miniscript with mini-subpbl";
    2.13  
    2.14   show_pt pt;
    2.15 +============ inhibit exn WN110319 ============================================*)
    2.16  
    2.17 +(*=== inhibit exn ?=============================================================
    2.18  
    2.19  "-------------- get_allpos' (from ptree above)--------------------";
    2.20  "-------------- get_allpos' (from ptree above)--------------------";
    2.21 @@ -1322,3 +1325,4 @@
    2.22  show_pt pt;
    2.23  *)
    2.24  
    2.25 +===== inhibit exn ?===========================================================*)