1.1 --- a/src/Tools/isac/Interpret/appl.sml	Sat May 21 09:54:39 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Sat May 21 12:52:59 2011 +0200
     1.3 @@ -356,7 +356,7 @@
     1.4    | applicable_in (p,p_) pt (Check_Postcond pI) =
     1.5        if member op = [Pbl,Met] p_                  
     1.6        then Notappl ((tac2str (Check_Postcond pI)) ^ " not for pos "^(pos'2str (p,p_)))
     1.7 -      else Appl (Check_Postcond' (pI, (e_term, [(*in solve assigned the returnvalue of scr*)])))
     1.8 +      else Appl (Check_Postcond' (pI, (e_term, [(*fun solve assignes the returnvalue of scr*)])))
     1.9  
    1.10    (*these are always applicable*)
    1.11    | applicable_in (p,p_) _ (Take str) = Appl (Take' (str2term str))

     2.1 --- a/src/Tools/isac/Interpret/ctree.sml	Sat May 21 09:54:39 2011 +0200
     2.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Sat May 21 12:52:59 2011 +0200
     2.3 @@ -523,97 +523,95 @@
     2.4  (* tac_ is made from tac in applicable_in,
     2.5    and carries all data necessary for generate *)
     2.6  datatype tac_ = 
     2.7 -  Init_Proof' of ((cterm' list) * spec)
     2.8 -| Model_Problem' of pblID * 
     2.9 -		    itm list *  (*the 'untouched' pbl*)
    2.10 -		    itm list    (*the casually completed met*)
    2.11 -| Refine_Tacitly' of pblID *    (*input*)
    2.12 -		     pblID *    (*the refined from applicable_in*)
    2.13 -		     domID *    (*from new pbt?! filled in specify*)
    2.14 -		     metID *    (*from new pbt?! filled in specify*)
    2.15 -		     itm list   (*drop ! 9.03: remains [] for
    2.16 +    Init_Proof' of ((cterm' list) * spec)
    2.17 +  | Model_Problem' of
    2.18 +      pblID * 
    2.19 +		  itm list *  (*the 'untouched' pbl*)
    2.20 +		  itm list    (*the casually completed met*)
    2.21 +  | Refine_Tacitly' of
    2.22 +      pblID *    (*input*)
    2.23 +		  pblID *    (*the refined from applicable_in*)
    2.24 +		  domID *    (*from new pbt?! filled in specify*)
    2.25 +		  metID *    (*from new pbt?! filled in specify*)
    2.26 +		  itm list   (*drop ! 9.03: remains [] for
    2.27                                    Model_Problem recognizing its activation*)
    2.28 -| Refine_Problem' of (pblID * (itm list * (bool * Term.term) list))
    2.29 - (*FIXME?040215 drop: done automatically in init_proof + Subproblem'*)
    2.30 -| Add_Given'    of cterm' *
    2.31 -		   itm list (*updated with input in fun specify_additem*)
    2.32 -| Add_Find'     of cterm' *
    2.33 -		   itm list (*updated with input in fun specify_additem*)
    2.34 -| Add_Relation' of cterm' *
    2.35 -		 itm list (*updated with input in fun specify_additem*)
    2.36 -| Del_Given' of cterm'   | Del_Find' of cterm'   | Del_Relation' of cterm'
    2.37 -  (*4.00.: all..    term: in applicable_in ..? Syn ?only for FormFK?*)
    2.38 -
    2.39 -| Specify_Theory' of domID              
    2.40 -| Specify_Problem' of (pblID *        (*               *)
    2.41 -		       (bool *        (* matches	     *)
    2.42 -			(itm list *   (* ppc	     *)
    2.43 -			 (bool * term) list))) (* preconditions *)
    2.44 -| Specify_Method' of metID *
    2.45 -		     ori list * (*repl. "#undef"*)
    2.46 -		     itm list   (*... updated from pbl to met*)
    2.47 -| Apply_Method' of metID * 
    2.48 -		   (term option) * (*init_form*)
    2.49 -		   istate * Proof.context
    2.50 -| Check_Postcond' of 
    2.51 -  pblID * 
    2.52 -  (term *      (*returnvalue of script in solve*)
    2.53 -   term list)  (*collect by get_assumptions_ in applicable_in, except if 
    2.54 +  | Refine_Problem' of (pblID * (itm list * (bool * Term.term) list))
    2.55 +    (*FIXME?040215 drop: done automatically in init_proof + Subproblem'*)
    2.56 +  | Add_Given' of
    2.57 +      cterm' *
    2.58 +		  itm list (*updated with input in fun specify_additem*)
    2.59 +  | Add_Find' of cterm' * itm list (* see Add_Given' *)
    2.60 +  | Add_Relation' of cterm' * itm list (* see Add_Given' *)
    2.61 +  | Del_Given' of cterm'   | Del_Find' of cterm'   | Del_Relation' of cterm'
    2.62 +    (*4.00.: all..    term: in applicable_in ..? Syn ?only for FormFK?*)
    2.63 +  | Specify_Theory' of domID              
    2.64 +  | Specify_Problem' of
    2.65 +      (pblID *        (*               *)
    2.66 +		    (bool *        (* matches	     *)
    2.67 +			    (itm list *   (* ppc	     *)
    2.68 +			      (bool * term) list))) (* preconditions *)
    2.69 +  | Specify_Method' of
    2.70 +      metID *
    2.71 +		  ori list * (*repl. "#undef"*)
    2.72 +		  itm list   (*... updated from pbl to met*)
    2.73 +  | Apply_Method' of
    2.74 +      metID * 
    2.75 +		  (term option) * (*init_form*)
    2.76 +		  istate * Proof.context
    2.77 +  | Check_Postcond' of 
    2.78 +      pblID * 
    2.79 +      (term *      (*returnvalue of script in solve*)
    2.80 +        term list)  (*collect by get_assumptions_ in applicable_in, except if 
    2.81                   butlast tac is Check_elementwise: take only these asms*)
    2.82 -| Free_Solve'
    2.83 -
    2.84 -| Rewrite_Inst' of theory' * rew_ord' * rls
    2.85 -		   * bool * subst * thm' * term * (term  * term list)
    2.86 -| Rewrite' of theory' * rew_ord' * rls * bool * thm' * 
    2.87 -	      term * (term * term list)
    2.88 -| Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm' * 
    2.89 -  term * (term * term list)
    2.90 -| Rewrite_Set_Inst' of theory' * bool * subst * rls * 
    2.91 -		       term * (term * term list)
    2.92 -| Detail_Set_Inst' of theory' * bool * subst * rls * 
    2.93 -		      term * (term * term list)
    2.94 -| Rewrite_Set' of theory' * bool * rls * term * (term * term list)
    2.95 -| Detail_Set' of theory' * bool * rls * term * (term * term list)
    2.96 -| End_Detail' of (term * (term list)) (*see End_Trans'*)
    2.97 -| End_Ruleset' of term
    2.98 -| Derive' of rls
    2.99 -| Calculate' of theory' * string * term * (term * thm') 
   2.100 -	      (*WN.29.4.03 asm?: * term list??*)
   2.101 -| Substitute' of subte  (*the 'substitution': terms of type bool*) 
   2.102 -		 * term (*to be substituted in*)
   2.103 -		 * term (*resulting from the substitution*)
   2.104 -| Apply_Assumption' of term list * term
   2.105 -
   2.106 -| Take' of term                         | Take_Inst' of term  
   2.107 -| Group' of (con * int list * term)
   2.108 -| Subproblem' of (spec * 
   2.109 -		(ori list) *    (* filled in assod Subproblem' *)
   2.110 -		 term *         (*-"-, headline of calc-head *)
   2.111 -		 fmz_ * 
   2.112 -     Proof.context *(* transported from assod to generate1 *)
   2.113 -		 term)          (* Subproblem(dom,pbl) OR cascmd*)  
   2.114 -| CAScmd' of term
   2.115 -| End_Subproblem' of term (*???*)
   2.116 -| Split_And' of term                    | Conclude_And' of term
   2.117 -| Split_Or' of term                     | Conclude_Or' of term
   2.118 -| Begin_Trans' of term                  | End_Trans' of (term * (term list))
   2.119 -| Begin_Sequ'                           | End_Sequ'(* substitute root.env*)
   2.120 -| Split_Intersect' of term              | End_Intersect' of term
   2.121 -| Check_elementwise' of (*special case:*)
   2.122 -  term *   (*(1)the current formula: [x=1,x=...]*)
   2.123 -  string * (*(2)the pred from Check_elementwise   *)
   2.124 -  (term *  (*(3)composed from (1) and (2): {x. pred}*)
   2.125 -   term list) (*20.5.03 assumptions*)
   2.126 -
   2.127 -| Or_to_List' of term * term            (* (a | b, [a,b]) *)
   2.128 -| Collect_Trues' of term
   2.129 -
   2.130 -| Empty_Tac_                          | Tac_ of  (*for dummies*)
   2.131 -                                            theory *
   2.132 -                                            string * (*form*)
   2.133 -					    string * (*in Tac*)
   2.134 -					    string   (*result of Tac".."*)
   2.135 -| User' (*internal for ets*)            | End_Proof'';(*End_Proof:inout*)
   2.136 +  | Free_Solve'
   2.137 +  | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm' * term * (term  * term list)
   2.138 +  | Rewrite' of theory' * rew_ord' * rls * bool * thm' * term * (term * term list)
   2.139 +  | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm' * term * (term * term list)
   2.140 +  | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * (term * term list)
   2.141 +  | Detail_Set_Inst' of theory' * bool * subst * rls * term * (term * term list)
   2.142 +  | Rewrite_Set' of theory' * bool * rls * term * (term * term list)
   2.143 +  | Detail_Set' of theory' * bool * rls * term * (term * term list)
   2.144 +  | End_Detail' of (term * (term list)) (*see End_Trans'*)
   2.145 +  | End_Ruleset' of term
   2.146 +  | Derive' of rls
   2.147 +  | Calculate' of theory' * string * term * (term * thm') 
   2.148 +  | Substitute' of
   2.149 +      subte *   (*the 'substitution': terms of type bool*) 
   2.150 +		  term * (*to be substituted in*)
   2.151 +		  term (*resulting from the substitution*)
   2.152 +  | Apply_Assumption' of term list * term
   2.153 +  | Take' of term
   2.154 +  | Take_Inst' of term  
   2.155 +  | Group' of (con * int list * term)
   2.156 +  | Subproblem' of
   2.157 +      (spec * 
   2.158 +		  (ori list) *    (* filled in assod Subproblem' *)
   2.159 +		  term *         (*-"-, headline of calc-head *)
   2.160 +		  fmz_ * 
   2.161 +      Proof.context *(* transported from assod to generate1 *)
   2.162 +		  term)          (* Subproblem(dom,pbl) OR cascmd*)  
   2.163 +  | CAScmd' of term
   2.164 +  | End_Subproblem' of term (*???*)
   2.165 +  | Split_And' of term                    | Conclude_And' of term
   2.166 +  | Split_Or' of term                     | Conclude_Or' of term
   2.167 +  | Begin_Trans' of term                  | End_Trans' of (term * (term list))
   2.168 +  | Begin_Sequ'                           | End_Sequ'(* substitute root.env*)
   2.169 +  | Split_Intersect' of term              | End_Intersect' of term
   2.170 +  | Check_elementwise' of (*special case:*)
   2.171 +      term *   (*(1)the current formula: [x=1,x=...]*)
   2.172 +      string * (*(2)the pred from Check_elementwise   *)
   2.173 +      (term *  (*(3)composed from (1) and (2): {x. pred}*)
   2.174 +        term list) (*20.5.03 assumptions*)
   2.175 +  | Or_to_List' of term * term            (* (a | b, [a,b]) *)
   2.176 +  | Collect_Trues' of term
   2.177 +  | Empty_Tac_
   2.178 +  | Tac_ of  (*for dummies*)
   2.179 +      theory *
   2.180 +      string * (*form*)
   2.181 +		  string * (*in Tac*)
   2.182 +		  string   (*result of Tac".."*)
   2.183 +  | User' (*internal for ets FIXME.WN110521 delete this and check occurrences of others*)
   2.184 +  | End_Proof'';(*End_Proof:inout*)
   2.185  
   2.186  fun tac_2str ma = case ma of
   2.187      Init_Proof' (ppc, spec)  => 

     3.1 --- a/src/Tools/isac/Interpret/generate.sml	Sat May 21 09:54:39 2011 +0200
     3.2 +++ b/src/Tools/isac/Interpret/generate.sml	Sat May 21 12:52:59 2011 +0200
     3.3 @@ -181,7 +181,7 @@
     3.4    | edit2str Protect = "Protect";
     3.5  
     3.6  
     3.7 -datatype inout =
     3.8 +datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*)
     3.9    New_User | End_User                                          (*<->*)
    3.10  | New_Proof | End_Proof                                        (*<->*)
    3.11  | Command of user_cmd                                          (*-->*)

     4.1 --- a/src/Tools/isac/Interpret/mstools.sml	Sat May 21 09:54:39 2011 +0200
     4.2 +++ b/src/Tools/isac/Interpret/mstools.sml	Sat May 21 12:52:59 2011 +0200
     4.3 @@ -157,11 +157,9 @@
     4.4      val get_assumptions : Proof.context -> term list
     4.5      val get_environments : Proof.context -> (term * term) list
     4.6      val insert_assumptions : term list -> Proof.context -> Proof.context
     4.7 -    val insert_environments :
     4.8 -          (term * term) list -> Proof.context -> Proof.context
     4.9 -    val transfer_from_subproblem :
    4.10 -          Proof.context -> Proof.context -> Proof.context
    4.11 +    val insert_environments : (term * term) list -> Proof.context -> Proof.context
    4.12      val transfer_asms_from_to : Proof.context -> Proof.context -> Proof.context
    4.13 +    val from_subpbl_to_caller : Proof.context -> term -> Proof.context -> Proof.context
    4.14   
    4.15    end
    4.16  
    4.17 @@ -1010,10 +1008,6 @@
    4.18    fun insert_environments envs = map (fn t => Env t) envs |> insert_ctxt;
    4.19  end
    4.20  
    4.21 -(* transfer information set by Variable.declare_constraints *)
    4.22 -fun transfer_from_subproblem ctxt_sub ctxt =
    4.23 -  insert_assumptions (get_assumptions ctxt_sub) ctxt;
    4.24 -
    4.25  (* transfer assumptions from one to another ctxt.
    4.26     do NOT respect scope: in a calculation identifiers are unique.
    4.27     but environments are scoped as usual in Luacs-interpretation.
    4.28 @@ -1028,6 +1022,14 @@
    4.29              else transfer fas (insert_assumptions [from_asm] to_ctxt)
    4.30    in transfer (get_assumptions from_ctxt) to_ctxt end
    4.31  
    4.32 +(* exported from a subproblem to the context of the calling method:
    4.33 +   # 'scrval': the result of script interpretation and
    4.34 +   # those assumptions in the subproblem wich contain a variable known
    4.35 +     in the calling method. *)
    4.36 +fun from_subpbl_to_caller sub_ctxt scrval caller_ctxt =
    4.37 +  let val caller_ctxt = (scrval |> dest_list' |> insert_assumptions) caller_ctxt
    4.38 +  in transfer_asms_from_to sub_ctxt caller_ctxt end;
    4.39 +
    4.40  (*----------------------------------------------------------*)
    4.41  end
    4.42  open SpecifyTools;

     5.1 --- a/src/Tools/isac/Interpret/script.sml	Sat May 21 09:54:39 2011 +0200
     5.2 +++ b/src/Tools/isac/Interpret/script.sml	Sat May 21 12:52:59 2011 +0200
     5.3 @@ -1532,7 +1532,7 @@
     5.4                (case par_pbl_det pt p of
     5.5  	               (true, p', _) => 
     5.6  	                  let val (_,pblID,_) = get_obj g_spec pt p';
     5.7 -	                  in (Check_Postcond' (pblID, (v, [(*WN030608 NO asms???*)])), 
     5.8 +	                  in (Check_Postcond' (pblID, (v, [(*assigned in next step*)])), 
     5.9  	                    (e_istate, ctxt), (v,s)) 
    5.10                      end
    5.11  	             | (_, p', rls') => 

     6.1 --- a/src/Tools/isac/Interpret/solve.sml	Sat May 21 09:54:39 2011 +0200
     6.2 +++ b/src/Tools/isac/Interpret/solve.sml	Sat May 21 12:52:59 2011 +0200
     6.3 @@ -212,7 +212,7 @@
     6.4  	          val metID = get_obj g_metID pt ppp;
     6.5              val sc = (#scr o get_met) metID;
     6.6              val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm); 
     6.7 -	          val ctxt'' = transfer_from_subproblem ctxt ctxt'
     6.8 +	          val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
     6.9              val ((p,p_),ps,f,pt) = 
    6.10  	            generate1 thy (Check_Postcond' (pI, (scval, asm)))
    6.11  		            (ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;
    6.12 @@ -332,7 +332,7 @@
    6.13  	          val metID = get_obj g_metID pt ppp;
    6.14  	          val {scr,...} = get_met metID;
    6.15              val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
    6.16 -	          val ctxt'' = transfer_from_subproblem ctxt ctxt'
    6.17 +	          val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
    6.18              val tac_ = Check_Postcond' (pI, (scval, asm))
    6.19  	          val is = ScrState (E,l,a,scval,scsaf,b)
    6.20              val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt'') (pp, Res) pt;

     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy	Sat May 21 12:52:59 2011 +0200
     7.3 @@ -0,0 +1,121 @@
     7.4 +theory All_Ctxt imports Isac begin
     7.5 +
     7.6 +text {* all changes of context are demonstrated in a mini example.
     7.7 +  see test/../mstools.sml --- all ctxt changes in minimsubpbl x+1=2 --- *}
     7.8 +
     7.9 +section {* start of the mini example *}
    7.10 +
    7.11 +ML {*
    7.12 +  val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    7.13 +  val (dI',pI',mI') =
    7.14 +    ("Test", ["sqroot-test","univariate","equation","test"],
    7.15 +     ["Test","squ-equ-test-subpbl1"]);
    7.16 +  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    7.17 +*}
    7.18 +
    7.19 +section {* start of specify phase *}
    7.20 +
    7.21 +text {* variables known from formalisation provide type-inference 
    7.22 +  for further input *}
    7.23 +
    7.24 +ML {*
    7.25 +  val ctxt = get_ctxt pt p;
    7.26 +  val SOME known_x = parseNEW ctxt "x + y + z";
    7.27 +  val SOME unknown = parseNEW ctxt "a + b + c";
    7.28 +*}
    7.29 +
    7.30 +ML {*
    7.31 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.32 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.33 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.34 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.35 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.36 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.37 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.38 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.39 +*}
    7.40 +
    7.41 +section {* start interpretation of method *}
    7.42 +
    7.43 +text {* preconditions are known at start of interpretation of (root-)method *}
    7.44 +
    7.45 +ML {*
    7.46 +  get_assumptions_ pt p |> terms2strs;
    7.47 +*}
    7.48 +
    7.49 +ML {*
    7.50 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.51 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.52 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.53 +*}
    7.54 +
    7.55 +section {* start a subproblem: specification *}
    7.56 +
    7.57 +text {* variables known from arguments of (sub-)method provide type-inference for further input *}
    7.58 +
    7.59 +ML {*
    7.60 +  val ctxt = get_ctxt pt p;
    7.61 +  val SOME known_x = parseNEW ctxt "x+y+z";
    7.62 +  val SOME unknown = parseNEW ctxt "a+b+c";
    7.63 +*}
    7.64 +
    7.65 +ML {*
    7.66 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.67 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.68 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.69 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.70 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.71 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.72 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.73 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
    7.74 +*}
    7.75 +
    7.76 +section {* interpretation of subproblem's method *}
    7.77 +
    7.78 +text {* preconds are known at start of interpretation of (sub-)method *}
    7.79 +
    7.80 +ML {*
    7.81 + get_assumptions_ pt p |> terms2strs
    7.82 +*}
    7.83 +
    7.84 +ML {*
    7.85 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
    7.86 +*}
    7.87 +
    7.88 +ML {*
    7.89 +  "artifically inject assumptions";
    7.90 +  val (SOME (iform, cform), SOME (ires, cres)) = get_obj g_loc pt (fst p);
    7.91 +  val ctxt = insert_assumptions [str2term "x < sub_asm_out",
    7.92 +                                 str2term "a < sub_asm_local"] cres;
    7.93 +  val pt = update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt));
    7.94 +*}
    7.95 +
    7.96 +ML {*
    7.97 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.98 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.99 +*}
   7.100 +
   7.101 +section {* finish subproblem, return to calling method*}
   7.102 +
   7.103 +text {* transfer non-local assumptions and result from sub-method to root-method.
   7.104 +  non-local assumptions are those contaning a variable known in root-method.
   7.105 +*}
   7.106 +
   7.107 +ML {*
   7.108 +  terms2strs (get_assumptions_ pt p);
   7.109 +*}
   7.110 +
   7.111 +ML {*
   7.112 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   7.113 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   7.114 +*}
   7.115 +
   7.116 +section {* finish Lucas interpretation *}
   7.117 +
   7.118 +text {* assumptions collected during lucas-interpretation for proof of postcondition *}
   7.119 +
   7.120 +ML {*
   7.121 +  terms2strs (get_assumptions_ pt p);
   7.122 +*}
   7.123 +
   7.124 +end
   7.125 \ No newline at end of file

     8.1 --- a/test/Tools/isac/Interpret/mstools.sml	Sat May 21 09:54:39 2011 +0200
     8.2 +++ b/test/Tools/isac/Interpret/mstools.sml	Sat May 21 12:52:59 2011 +0200
     8.3 @@ -12,7 +12,7 @@
     8.4  "----------- fun declare_constraints --------------------";
     8.5  "----------- fun get_assumptions, fun get_environments --";
     8.6  "----------- fun transfer_asms_from_to ------------------";
     8.7 -"----------- fun transfer_from_subproblem ---------------";
     8.8 +"----------- fun from_subpbl_to_caller ------------------";
     8.9  "----------- all ctxt changes in minimsubpbl x+1=2 ------";
    8.10  "----------- go through Model_Problem until nxt_tac -----";
    8.11  "--------------------------------------------------------";
    8.12 @@ -77,17 +77,19 @@
    8.13  if terms2strs (get_assumptions new_ctxt) = ["b < fro", "b < to", "c < to"]
    8.14  then () else error "fun transfer_asms_from_to changed"
    8.15  
    8.16 -"----------- fun transfer_from_subproblem ---------------";
    8.17 -"----------- fun transfer_from_subproblem ---------------";
    8.18 -"----------- fun transfer_from_subproblem ---------------";
    8.19 -terms2str (get_assumptions ctxt);
    8.20 -val ctxt = insert_assumptions [@{term "x * v"}, @{term "2 * u"}] ctxt;
    8.21 -val ctxt_sub = insert_assumptions [@{term "x ~= 0"}] ctxt;
    8.22 -val ctxt' = transfer_from_subproblem ctxt_sub ctxt;
    8.23 -terms2str (get_assumptions ctxt');
    8.24 -if get_assumptions ctxt' = [@{term "x ~= 0"}, @{term "x * v"}, @{term "2 * u"}]
    8.25 -then () else error "mstools.sml transfer_from_subproblem changed."
    8.26 -
    8.27 +"----------- fun from_subpbl_to_caller ------------------";
    8.28 +"----------- fun from_subpbl_to_caller ------------------";
    8.29 +"----------- fun from_subpbl_to_caller ------------------";
    8.30 +val ctxt = ProofContext.init_global @{theory "Isac"}
    8.31 +val sub_ctxt = insert_assumptions
    8.32 +  [str2term "a < (fro::int)", str2term "b < (fro::int)"] ctxt
    8.33 +val caller_ctxt = insert_assumptions
    8.34 +  [str2term "b < (to::int)", str2term "c < (to::int)"] ctxt
    8.35 +val scrval = str2term "[x_1 = 1, x_2 = 2, x_3 = 3]";
    8.36 +val new_ctxt = from_subpbl_to_caller sub_ctxt scrval caller_ctxt;
    8.37 +if terms2strs (get_assumptions new_ctxt) =
    8.38 +["b < fro", "x_1 = 1", "x_2 = 2", "x_3 = 3", "b < to", "c < to"]
    8.39 +then () else error "fun from_subpbl_to_caller changed"
    8.40  
    8.41  "----------- all ctxt changes in minimsubpbl x+1=2 ------";
    8.42  "----------- all ctxt changes in minimsubpbl x+1=2 ------";
    8.43 @@ -159,18 +161,17 @@
    8.44  
    8.45  "=(5)= transfer non-local assumptions and result from sub-method to root-method." ^
    8.46  "      non-local assumptions are those contaning a variable known in root-method";
    8.47 -(*del*)terms2strs (get_assumptions_ pt p);
    8.48 -get_assumptions_ pt p = [(*precond_rootmet, precond_submet, sub_asm_out, sub_res*)];
    8.49 -(*TODO check like =(4)=*)
    8.50 +if terms2strs (get_assumptions_ pt p) =
    8.51 +  ["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"]
    8.52 +  then () else error "x+1=2 transfer from sub-met to root-met changed";
    8.53  
    8.54  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt=Check_P["sqroot-test","univariate","equation","test"*)
    8.55  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    8.56  
    8.57  "=(6)= assumptions collected during lucas-interpretation for proof of postcondition";
    8.58 -get_assumptions_ pt p = [(*precond_rootmet, precond_submet, sub_asm_out, sub_res, root_res*)];
    8.59 -terms2strs (get_assumptions_ pt p);
    8.60 -(*TODO check like =(4)=*)
    8.61 -
    8.62 +if terms2strs (get_assumptions_ pt p) = (*weak check: sub-result = root-result = [x = 1]*)
    8.63 +  ["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"]
    8.64 +  then () else error "x+1=2 transfer from sub-met to root-met changed";
    8.65  
    8.66  
    8.67  "----------- go through Model_Problem until nxt_tac -----";

     9.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml	Sat May 21 09:54:39 2011 +0200
     9.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml	Sat May 21 12:52:59 2011 +0200
     9.3 @@ -70,7 +70,7 @@
     9.4  	          val metID = get_obj g_metID pt ppp;
     9.5  	          val {scr,...} = get_met metID;
     9.6              val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
     9.7 -          val ctxt'' = transfer_from_subproblem ctxt ctxt'
     9.8 +          val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
     9.9              val tac_ = Check_Postcond' (pI, (scval, asm))
    9.10  	          val is = ScrState (E,l,a,scval,scsaf,b);
    9.11  "~~~~~ fun generate1, args:"; val (thy, (Check_Postcond' (pI, (scval, asm))), l, (p,p_), pt) =

    10.1 --- a/test/Tools/isac/Minisubpbl/500-met-sub-to-root.sml	Sat May 21 09:54:39 2011 +0200
    10.2 +++ b/test/Tools/isac/Minisubpbl/500-met-sub-to-root.sml	Sat May 21 12:52:59 2011 +0200
    10.3 @@ -34,6 +34,7 @@
    10.4  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
    10.5  val (pt''', p''') = (pt, p);
    10.6  
    10.7 +(*WN110521 worked without testing*)
    10.8  
    10.9  val (p,_,f,nxt,_,pt) = me nxt p''' [] pt'''; (*nxt = Check_elementwise "Assumptions"*)
   10.10  if nxt = ("Check_elementwise", Check_elementwise "Assumptions") then ()

    11.1 --- a/test/Tools/isac/Test_Isac.thy	Sat May 21 09:54:39 2011 +0200
    11.2 +++ b/test/Tools/isac/Test_Isac.thy	Sat May 21 12:52:59 2011 +0200
    11.3 @@ -12,6 +12,7 @@
    11.4    Isac
    11.5    "Knowledge/Rational_Test"
    11.6    "ADDTESTS/Ctxt"
    11.7 +  "ADDTESTS/All_Ctxt"
    11.8   
    11.9  uses 
   11.10    (         "library.sml")
   11.11 @@ -170,44 +171,11 @@
   11.12    ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
   11.13  
   11.14  ML {*
   11.15 -
   11.16 +*}
   11.17 +ML {*
   11.18  *}
   11.19    ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
   11.20  ML {*
   11.21 -"----------- Minisubplb/500-met-sub-to-root.sml ------------------";
   11.22 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
   11.23 -val (dI',pI',mI') =
   11.24 -   ("Test", ["sqroot-test","univariate","equation","test"],
   11.25 -    ["Test","squ-equ-test-subpbl1"]);
   11.26 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
   11.27 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.28 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.29 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.30 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.31 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.32 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.33 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
   11.34 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.35 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.36 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
   11.37 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.38 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.39 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.40 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.41 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.42 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.43 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.44 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
   11.45 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst isolate_bdv*);
   11.46 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
   11.47 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
   11.48 -val (pt''', p''') = (pt, p);
   11.49 -
   11.50 -*}
   11.51 -ML {*
   11.52 -
   11.53 -*}
   11.54 -ML {*
   11.55  *}
   11.56  ML {*
   11.57  *}
   11.58 @@ -217,16 +185,7 @@
   11.59  *}
   11.60  ML {*
   11.61  *}
   11.62 -ML {*
   11.63  
   11.64 -
   11.65 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
   11.66 -if nxt = ("Check_elementwise", Check_elementwise "Assumptions") then ()
   11.67 -else error "Check_elementwise changed; after switch sub-->root-method"*}
   11.68 -ML {*
   11.69 -*}
   11.70 -ML {*
   11.71 -*}
   11.72  end
   11.73  
   11.74  (*=== inhibit exn ?=============================================================