1.1 --- a/src/Tools/isac/Interpret/appl.sml	Sun May 15 10:25:42 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Sun May 15 11:32:41 2011 +0200
     1.3 @@ -336,15 +336,17 @@
     1.4  			      [(*filled in specify*)]))
     1.5  
     1.6    | applicable_in (p,p_) pt (Apply_Method mI) =                
     1.7 -  if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  
     1.8 -    then Notappl ((tac2str (Apply_Method mI))^
     1.9 -	   " not for pos "^(pos'2str (p,p_)))
    1.10 -  else let
    1.11 -    val (PblObj{origin = (_, (dI, pI, _), _), probl, ...}) = get_obj I pt p;
    1.12 -    val {where_, ...} = get_pbt pI
    1.13 -    val pres = map (mk_env probl |> subst_atomic) where_
    1.14 -    val ctxt = assoc_thy dI |> ProofContext.init_global 
    1.15 -          |> insert_assumptions pres
    1.16 +      if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  
    1.17 +      then Notappl ((tac2str (Apply_Method mI)) ^ " not for pos " ^ (pos'2str (p,p_)))
    1.18 +      else
    1.19 +        let
    1.20 +          val (PblObj{origin = (_, (dI, pI, _), _), probl, ctxt, ...}) = get_obj I pt p;
    1.21 +          val {where_, ...} = get_pbt pI
    1.22 +          val pres = map (mk_env probl |> subst_atomic) where_
    1.23 +          val ctxt = 
    1.24 +            if is_e_ctxt ctxt
    1.25 +            then assoc_thy dI |> ProofContext.init_global |> insert_assumptions pres
    1.26 +            else ctxt
    1.27      (*TODO.WN110416 here do evalprecond according to fun check_preconds'
    1.28        and then decide on Notappl/Appl accordingly once more.
    1.29        Implement after all tests are running, since this changes

     2.1 --- a/src/Tools/isac/Interpret/ctree.sml	Sun May 15 10:25:42 2011 +0200
     2.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Sun May 15 11:32:41 2011 +0200
     2.3 @@ -274,7 +274,10 @@
     2.4         | ScrState of scrstate    (*for script interpreter*)
     2.5         | RrlsState of rrlsstate; (*for reverse rewriting*)
     2.6  val e_istate = (ScrState ([],[],NONE,e_term,Sundef,false)):istate;
     2.7 -val e_ctxt = ProofContext.init_global @{theory};
     2.8 +val e_ctxt = ProofContext.init_global @{theory "Pure"};
     2.9 +
    2.10 +(* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*)
    2.11 +fun is_e_ctxt ctxt = Theory.eq_thy (ProofContext.theory_of ctxt, @{theory "Pure"});
    2.12  
    2.13  type iist = istate option * istate option;
    2.14  (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*) 

     3.1 --- a/src/Tools/isac/Interpret/script.sml	Sun May 15 10:25:42 2011 +0200
     3.2 +++ b/src/Tools/isac/Interpret/script.sml	Sun May 15 11:32:41 2011 +0200
     3.3 @@ -437,11 +437,13 @@
     3.4  	      val {cas,ppc,thy,...} = get_pbt pI
     3.5  	      val dI = theory2theory' thy (*.take dI from _refined_ pbl.*)
     3.6  	      val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt));
     3.7 +        val ctxt = ProofContext.init_global 
     3.8 +        val ctxt = dI |> Thy_Info.get_theory |> ProofContext.init_global 
     3.9 +          |> declare_constraints' vals
    3.10  	      val hdl =
    3.11            case cas of
    3.12  		        NONE => pblterm dI pI
    3.13  		      | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
    3.14 -        val ctxt = declare_constraints' vals (ProofContext.init_global thy)
    3.15          val f = subpbl (strip_thy dI) pI
    3.16        in (Subproblem (dI, pI),	Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
    3.17        end
    3.18 @@ -618,16 +620,15 @@
    3.19  		        handle ERROR "actual args do not match formal args"
    3.20  			      => (match_ags_msg pI stac ags(*raise exn*);[]), mI);
    3.21          val (fmz_, vals) = oris2fmz_vals pors;
    3.22 -	      val {cas, ppc,...} = get_pbt pI
    3.23  	      val {cas, ppc, thy,...} = get_pbt pI
    3.24  	      val dI = theory2theory' thy (*take dI from _refined_ pbl*)
    3.25  	      val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt))
    3.26 -	      val thy' = (maxthy (assoc_thy dI) (rootthy pt))
    3.27 +	      val ctxt = dI |> Thy_Info.get_theory |> ProofContext.init_global 
    3.28 +          |> declare_constraints' vals
    3.29  	      val hdl = 
    3.30            case cas of
    3.31  		        NONE => pblterm dI pI
    3.32  		      | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
    3.33 -        val ctxt = declare_constraints' vals (ProofContext.init_global thy')
    3.34          val f = subpbl (strip_thy dI) pI
    3.35        in 
    3.36          if domID = dI andalso pblID = pI

     4.1 --- a/test/Tools/isac/Interpret/ctree.sml	Sun May 15 10:25:42 2011 +0200
     4.2 +++ b/test/Tools/isac/Interpret/ctree.sml	Sun May 15 11:32:41 2011 +0200
     4.3 @@ -69,22 +69,21 @@
     4.4     ["Test","squ-equ-test-subpbl1"]);
     4.5  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
     4.6  (get_ctxt pt p)
     4.7 -  handle _ => error "ctree.sml: not even some ctxt found in PblObj";
     4.8 +  handle _ => error "--- fun get_ctxt not even some ctxt found in PblObj";
     4.9  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    4.10  (get_ctxt pt p)
    4.11 -  handle _ => error "ctree.sml: not even some ctxt found in PrfObj";
    4.12 +  handle _ => error "--- fun get_ctxt not even some ctxt found in PrfObj";
    4.13  
    4.14  "-------------- fun update_ctxt, fun g_ctxt ----------------------";
    4.15  "-------------- fun update_ctxt, fun g_ctxt ----------------------";
    4.16  "-------------- fun update_ctxt, fun g_ctxt ----------------------";
    4.17 -val pt = append_problem [] (e_istate, e_ctxt) e_fmz ([(*oris*)], e_spec, e_term) EmptyPtree;
    4.18 -if (get_obj g_ctxt pt [] |> ProofContext.theory_of |> Context.theory_name)
    4.19 -    = "Interpret"
    4.20 -then () else error "TODO";
    4.21 +val pt = EmptyPtree;
    4.22 +val pt = append_problem [] (e_istate, e_ctxt) e_fmz ([(*oris*)], e_spec, e_term) pt;
    4.23 +val ctxt = get_obj g_ctxt pt [];
    4.24 +if is_e_ctxt ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed";
    4.25  val pt = update_ctxt pt [] (ProofContext.init_global @{theory "Isac"});
    4.26 -if (get_obj g_ctxt pt [] |> ProofContext.theory_of |> Context.theory_name)
    4.27 -    = "Isac"
    4.28 -then () else error "TODO";
    4.29 +if (get_obj g_ctxt pt [] |> ProofContext.theory_of |> Context.theory_name) = "Isac"
    4.30 +then () else error "--- fun update_ctxt, fun g_ctxt changed";
    4.31  
    4.32  "-------------- check positions in miniscript --------------------";
    4.33  "-------------- check positions in miniscript --------------------";
    4.34 @@ -1337,3 +1336,4 @@
    4.35  *)
    4.36  
    4.37  ===== inhibit exn ?===========================================================*)
    4.38 +

     5.1 --- a/test/Tools/isac/Test_Isac.thy	Sun May 15 10:25:42 2011 +0200
     5.2 +++ b/test/Tools/isac/Test_Isac.thy	Sun May 15 11:32:41 2011 +0200
     5.3 @@ -99,47 +99,34 @@
     5.4    use "Minisubpbl/200-start-method.sml"
     5.5    use "Minisubpbl/300-init-subpbl.sml"
     5.6  ML {*
     5.7 -(*test/./400-start-meth-subpbl*)
     5.8 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
     5.9 -val (dI',pI',mI') =
    5.10 -   ("Test", ["sqroot-test","univariate","equation","test"],
    5.11 -    ["Test","squ-equ-test-subpbl1"]);
    5.12 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    5.13 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    5.14 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    5.15 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    5.16 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    5.17 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    5.18 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    5.19 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    5.20 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    5.21 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    5.22 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
    5.23 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    5.24 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    5.25 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    5.26 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    5.27 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    5.28 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    5.29 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    5.30 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    5.31 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst isolate_bdv*);
    5.32 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
    5.33 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
    5.34 -(*-----nxt = ("Empty_Tac", Empty_Tac): tac'_
    5.35 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions *);
    5.36 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond["sqroot-test", "univariate", ...]) *);
    5.37 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("End_Proof'" *);
    5.38 ------*)
    5.39 +val dI = "Integrate";
    5.40 +Thy_Info.get_theory dI;
    5.41 +val vals = [];
    5.42  *}
    5.43  ML {*
    5.44 -(*is_empty*)
    5.45 +dI |> Thy_Info.get_theory |> ProofContext.init_global |> declare_constraints' vals
    5.46 +*}
    5.47 +ML {*
    5.48 +*}
    5.49 +ML {*
    5.50 +*}
    5.51 +ML {*
    5.52 +*}
    5.53 +ML {*
    5.54 +is_e_ctxt e_ctxt;
    5.55  *}
    5.56    use "Minisubpbl/400-start-meth-subpbl.sml"
    5.57    use "Minisubpbl/500-postcond.sml"
    5.58    ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl %%%%%%%%%%%%%%%%%%%%%%%";*}
    5.59    ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
    5.60    use "Interpret/mstools.sml"       (*new 2010*)
    5.61 +ML {*
    5.62 +(*test/../ctree.sml*)
    5.63 +val pt = EmptyPtree;
    5.64 +val pt = append_problem [] (e_istate, e_ctxt) e_fmz ([(*oris*)], e_spec, e_term) pt;
    5.65 +val ctxt = get_obj g_ctxt pt [];
    5.66 +if is_e_ctxt ctxt then () else error "TODO";
    5.67 +*}
    5.68    use "Interpret/ctree.sml"         (*!...!see(25)*)
    5.69    use "Interpret/ptyps.sml"         (*    *)
    5.70  (*use "Interpret/generate.sml"        new 2011*)