1.1 --- a/src/Tools/isac/Frontend/interface.sml	Fri Apr 15 15:58:52 2011 +0200
     1.2 +++ b/src/Tools/isac/Frontend/interface.sml	Fri Apr 15 17:07:34 2011 +0200
     1.3 @@ -286,7 +286,7 @@
     1.4  (*WN0502 @see ME/ctree: type asms: illdesigned, thus no positions returned*)
     1.5  fun getAccumulatedAsms cI (p:pos') =
     1.6      (let val ((pt, _), _) = get_calc cI
     1.7 -	 val ass = map fst (get_assumptions_ pt p)
     1.8 +	 val ass = get_assumptions_ pt p
     1.9       in (*getaccuasmsOK2xml cI (get_assumptions_ pt p)*)
    1.10       getasmsOK2xml cI ass end)
    1.11      handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms";

     2.1 --- a/src/Tools/isac/Interpret/appl.sml	Fri Apr 15 15:58:52 2011 +0200
     2.2 +++ b/src/Tools/isac/Interpret/appl.sml	Fri Apr 15 17:07:34 2011 +0200
     2.3 @@ -93,7 +93,7 @@
     2.4    | mk_set thy pt p (Const ("Tools.UniversalList",_)) pred =
     2.5      (e_term, if pred <> Const ("Script.Assumptions",bool)
     2.6  	     then [pred] 
     2.7 -	     else (map fst) (get_assumptions_ pt (p,Res)))
     2.8 +	     else get_assumptions_ pt (p,Res))
     2.9  
    2.10  (* val pred = (term_of o the o (parse thy)) pred;
    2.11     val consts as Const ("List.list.Cons",_) $ eq $ _ = ft;
    2.12 @@ -103,7 +103,7 @@
    2.13    let val (bdv,_) = HOLogic.dest_eq eq;
    2.14      val pred = if pred <> Const ("Script.Assumptions",bool)
    2.15  		 then [pred] 
    2.16 -	       else (map fst) (get_assumptions_ pt (p,Res))
    2.17 +	       else get_assumptions_ pt (p,Res)
    2.18    in (bdv, pred) end
    2.19  
    2.20    | mk_set thy _ _ l _ = 

     3.1 --- a/src/Tools/isac/Interpret/ctree.sml	Fri Apr 15 15:58:52 2011 +0200
     3.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Fri Apr 15 17:07:34 2011 +0200
     3.3 @@ -193,8 +193,6 @@
     3.4  val e_pos' = ([],Und):pos';
     3.5  
     3.6  fun res2str (t, ts) = pair2str (term2str t, terms2str ts);
     3.7 -fun asm2str (t, p:pos) = pair2str (term2str t, ints2str' p);
     3.8 -fun asms2str asms = (strs2str' o (map asm2str)) asms;
     3.9  
    3.10  
    3.11  
    3.12 @@ -1347,47 +1345,7 @@
    3.13  fun get_istate pt p = get_loc pt p |> #1;
    3.14  fun get_ctxt pt p = get_loc pt p |> #2;
    3.15  
    3.16 -(*.collect the assumptions within a problem up to a certain position.*)
    3.17 -type asms = (term * pos) list;(*WN0502 should be (pos' * term) list
    3.18 -				       ...........===^===*)
    3.19 -
    3.20 -fun get_asm (b:pos, p:pos) (Nd (PblObj {result=(_,asm),...},_)) = 
    3.21 -    ((*tracing ("### get_asm PblObj:(b,p)= "^
    3.22 -		(pair2str(ints2str b, ints2str p)));*)
    3.23 -     (map (rpair b) asm):asms)
    3.24 -  | get_asm (b, p) (Nd (PrfObj {result=(_,asm),...}, [])) = 
    3.25 -    ((*tracing ("### get_asm PrfObj []:(b,p)= "^
    3.26 -	      (pair2str(ints2str b, ints2str p)));*)
    3.27 -     (map (rpair b) asm))
    3.28 -  | get_asm (b, p:pos) (Nd (PrfObj _, nds)) = 
    3.29 -    let (*val _= tracing ("### get_asm PrfObj nds:(b,p)= "^
    3.30 -	      (pair2str(ints2str b, ints2str p)));*)
    3.31 -	val levdn = 
    3.32 -	    if p <> [] then (b @ [hd p]:pos, tl p:pos) 
    3.33 -	    else (b @ [1], [99999]) (*_deeper_ nesting is always _before_ p*)
    3.34 -    in gets_asm levdn 1 nds end
    3.35 -and gets_asm _ _ [] = []
    3.36 -  | gets_asm (b, p' as p::ps) i (nd::nds) = 
    3.37 -    if p < i then [] 
    3.38 -    else ((*tracing ("### gets_asm: (b,p')= "^(pair2str(ints2str b,
    3.39 -						      ints2str p')));*)
    3.40 -	  (get_asm (b @ [i], ps) nd) @ (gets_asm (b, p') (i + 1) nds));
    3.41 -
    3.42 -fun get_assumptions_ (Nd (PblObj {result=(r,asm),...}, cn)) (([], _):pos') = 
    3.43 -    if r = e_term then gets_asm ([], [99999]) 1 cn
    3.44 -    else map (rpair []) asm
    3.45 -  | get_assumptions_ pt (p,p_) =
    3.46 -    let val (cn, base) = par_children pt p
    3.47 -	val offset = drop (length base, p)
    3.48 -	val base' = replicate (length base) 1
    3.49 -	val offset' = case p_ of 
    3.50 -			 Frm => let val (qs,q) = split_last offset
    3.51 -				in qs @ [q - 1] end
    3.52 -		       | _ => offset
    3.53 -        (*val _= tracing ("... get_assumptions: (b,o)= "^
    3.54 -			(pair2str(ints2str base',ints2str offset)))*)
    3.55 -    in gets_asm (base', offset) 1 cn end;
    3.56 -
    3.57 +fun get_assumptions_ pt p = get_ctxt pt p |> get_assumptions;
    3.58  
    3.59  (*---------
    3.60  end

     4.1 --- a/src/Tools/isac/Interpret/generate.sml	Fri Apr 15 15:58:52 2011 +0200
     4.2 +++ b/src/Tools/isac/Interpret/generate.sml	Fri Apr 15 17:07:34 2011 +0200
     4.3 @@ -373,18 +373,21 @@
     4.4    in ((p',Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)),
     4.5        pt) end
     4.6  
     4.7 -  | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f',asm))) l (p,p_) pt =
     4.8 +  | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f',asm))) (is, ctxt)
     4.9 +      (p,p_) pt =
    4.10    let (*val _= tracing("###generate1 Rewrite_Inst': pos= "^pos'2str (p,p_));*)
    4.11 -      val (pt,c) = cappend_atomic pt p l f
    4.12 +      val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
    4.13        (Rewrite_Inst (subst2subs subs',thm')) (f',asm) Complete;
    4.14        val pt = update_branch pt p TransitiveB (*040312*)
    4.15      (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*)
    4.16    in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
    4.17        pt) end
    4.18  
    4.19 -  | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) l (p,p_) pt =
    4.20 +  | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) (is, ctxt)
    4.21 +      (p,p_) pt =
    4.22    let (*val _= tracing("###generate1 Rewrite': pos= "^pos'2str (p,p_))*)
    4.23 -      val (pt,c) = cappend_atomic pt p l f (Rewrite thm') (f',asm) Complete
    4.24 +      val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
    4.25 +        (Rewrite thm') (f',asm) Complete
    4.26        val pt = update_branch pt p TransitiveB (*040312*)
    4.27      (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*)
    4.28    in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
    4.29 @@ -393,44 +396,46 @@
    4.30    | generate1 thy (Rewrite_Asm' all) l p pt = 
    4.31      generate1 thy (Rewrite' all) l p pt
    4.32  
    4.33 -  | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) l (p,p_) pt =
    4.34 +  | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) (is, ctxt)
    4.35 +      (p,p_) pt =
    4.36  (* val (thy, Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm)), l, (p,p_), pt) = 
    4.37         (assoc_thy "Isac", tac_, is, pos, pt);
    4.38     *)
    4.39    let (*val _=tracing("###generate1 Rewrite_Set_Inst': pos= "^pos'2str(p,p_))*)
    4.40 -      val (pt,c) = cappend_atomic pt p l f 
    4.41 +      val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f 
    4.42        (Rewrite_Set_Inst (subst2subs subs',id_rls rls')) (f',asm) Complete
    4.43        val pt = update_branch pt p TransitiveB (*040312*)
    4.44      (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*)
    4.45    in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
    4.46        pt) end
    4.47  
    4.48 -  | generate1 thy (Detail_Set_Inst' (_,_,subs,rls,f,(f',asm))) l (p,p_) pt =
    4.49 -  let val (pt,c) = cappend_form pt p l f 
    4.50 +  | generate1 thy (Detail_Set_Inst' (_,_,subs,rls,f,(f',asm))) (is, ctxt) (p,p_)
    4.51 +      pt =
    4.52 +  let val ctxt' = insert_assumptions asm ctxt
    4.53 +      val (pt,c) = cappend_form pt p (is, ctxt') f 
    4.54        val pt = update_branch pt p TransitiveB (*040312*)
    4.55 +      val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f 
    4.56 +      val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')
    4.57 +      val pos' = ((lev_on o lev_dn) p, Frm)
    4.58 +  in (*implicit Take*) generate1 thy tac_ (is, ctxt') pos' pt end
    4.59  
    4.60 -      val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f 
    4.61 -      val tac_ = Apply_Method' (e_metID, SOME t, is, e_ctxt)
    4.62 -      val pos' = ((lev_on o lev_dn) p, Frm)
    4.63 -  in (*implicit Take*) generate1 thy tac_ (is, e_ctxt) pos' pt end
    4.64 -
    4.65 -  | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) l (p,p_) pt =
    4.66 +  | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) (is, ctxt) (p,p_) pt =
    4.67    let (*val _= tracing("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))*)
    4.68 -      val (pt,c) = cappend_atomic pt p l f 
    4.69 +      val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f 
    4.70        (Rewrite_Set (id_rls rls')) (f',asm) Complete
    4.71        val pt = update_branch pt p TransitiveB (*040312*)
    4.72      (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*)
    4.73    in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
    4.74        pt) end
    4.75  
    4.76 -  | generate1 thy (Detail_Set' (_,_,rls,f,(f',asm))) l (p,p_) pt =
    4.77 -  let val (pt,c) = cappend_form pt p l f 
    4.78 +  | generate1 thy (Detail_Set' (_,_,rls,f,(f',asm))) (is, ctxt) (p,p_) pt =
    4.79 +  let val (pt,c) = cappend_form pt p (is, ctxt) f 
    4.80        val pt = update_branch pt p TransitiveB (*040312*)
    4.81  
    4.82        val is = init_istate (Rewrite_Set (id_rls rls)) f
    4.83 -      val tac_ = Apply_Method' (e_metID, SOME t, is, e_ctxt)
    4.84 +      val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt)
    4.85        val pos' = ((lev_on o lev_dn) p, Frm)
    4.86 -  in (*implicit Take*) generate1 thy tac_ (is, e_ctxt) pos' pt end
    4.87 +  in (*implicit Take*) generate1 thy tac_ (is, ctxt) pos' pt end
    4.88  
    4.89    | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt =
    4.90      let (*val _=tracing("###generate1 Check_Postcond': pos= "^pos'2str(p,p_))*)
    4.91 @@ -552,7 +557,7 @@
    4.92  	val (SOME (ist, ctxt),_) = get_obj g_loc pt p
    4.93  	val form = get_obj g_form pt p
    4.94        (*val p = lev_on p; ---------------only difference to (..,Res) below*)
    4.95 -	val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, e_ctxt)))
    4.96 +	val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, ctxt)))
    4.97  		    ::(insert_pos ((lev_on o lev_dn) p) tacis)
    4.98  		    @ [(End_Trans, End_Trans' (res, asm),
    4.99  			(pos_plus (length tacis) (lev_dn p, Res), 
   4.100 @@ -573,7 +578,7 @@
   4.101  	val (_, SOME (ist, ctxt)) = get_obj g_loc pt p
   4.102  	val (f,a) = get_obj g_result pt p
   4.103  	val p = lev_on p(*---------------only difference to (..,Frm) above*);
   4.104 -	val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, e_ctxt)))
   4.105 +	val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, ctxt)))
   4.106  		    ::(insert_pos ((lev_on o lev_dn) p) tacis)
   4.107  		    @ [(End_Trans, End_Trans' (res, asm), 
   4.108  			(pos_plus (length tacis) (lev_dn p, Res), 

     5.1 --- a/src/Tools/isac/Interpret/mstools.sml	Fri Apr 15 15:58:52 2011 +0200
     5.2 +++ b/src/Tools/isac/Interpret/mstools.sml	Fri Apr 15 17:07:34 2011 +0200
     5.3 @@ -2,7 +2,7 @@
     5.4     modspec.sml. The types are separated from calchead.sml into this file,
     5.5     because some of them are stored in the calc-tree, and thus are required
     5.6     _before_ ctree.sml. 
     5.7 -   author: Walther Neuper
     5.8 +   author: Walther Neuper, Mathias Lehnfeld
     5.9     (c) due to copyright terms
    5.10  
    5.11  use"ME/mstools.sml" (*re-evaluate sml/ from scratch!*);
    5.12 @@ -153,6 +153,12 @@
    5.13      val vts_cnt : int list -> itm list -> (int * int) list
    5.14      val vts_in : itm list -> int list
    5.15     (* val w_itms2str_ : Proof.context -> itm list -> unit *)
    5.16 +    val get_assumptions : Proof.context -> term list
    5.17 +    val get_environments : Proof.context -> (term * term) list
    5.18 +    val insert_assumptions : term list -> Proof.context -> Proof.context
    5.19 +    val insert_environments :
    5.20 +          (term * term) list -> Proof.context -> Proof.context
    5.21 +
    5.22    end
    5.23  
    5.24  (*----------------------------------------------------------*)
    5.25 @@ -973,6 +979,33 @@
    5.26        val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
    5.27      in fold Variable.declare_constraints ts ctxt end;
    5.28  
    5.29 +datatype Isac_Ctxt =
    5.30 +    Env of term * term
    5.31 +  | Asm of term;
    5.32 +
    5.33 +structure ContextData = Proof_Data
    5.34 +  (type T = Isac_Ctxt list
    5.35 +   fun init _ = []);
    5.36 +
    5.37 +local
    5.38 +  fun unpack_asms (Asm t::ts) = t::(unpack_asms ts)
    5.39 +    | unpack_asms (Env _::ts) = unpack_asms ts
    5.40 +    | unpack_asms [] = [];
    5.41 +  fun unpack_envs (Env t::ts) = t::(unpack_envs ts)
    5.42 +    | unpack_envs (Asm _::ts) = unpack_envs ts
    5.43 +    | unpack_envs [] = [];
    5.44 +in
    5.45 +  fun get_assumptions ctxt = ContextData.get ctxt |> unpack_asms;
    5.46 +  fun get_environments ctxt = ContextData.get ctxt |> unpack_envs;
    5.47 +end
    5.48 +
    5.49 +local
    5.50 +  fun insert_ctxt data = ContextData.map (fn xs => distinct data@xs);
    5.51 +in
    5.52 +  fun insert_assumptions asms = map (fn t => Asm t) asms |> insert_ctxt;
    5.53 +  fun insert_environments envs = map (fn t => Env t) envs |> insert_ctxt;
    5.54 +end
    5.55 +
    5.56  (*----------------------------------------------------------*)
    5.57  end
    5.58  open SpecifyTools;

     6.1 --- a/src/Tools/isac/Interpret/solve.sml	Fri Apr 15 15:58:52 2011 +0200
     6.2 +++ b/src/Tools/isac/Interpret/solve.sml	Fri Apr 15 17:07:34 2011 +0200
     6.3 @@ -200,7 +200,7 @@
     6.4        val asm = (case get_obj g_tac pt p of
     6.5  		    Check_elementwise _ => (*collects and instantiates asms*)
     6.6  		    (snd o (get_obj g_result pt)) p
     6.7 -		  | _ => ((map fst) o (get_assumptions_ pt)) (p,p_))
     6.8 +		  | _ => get_assumptions_ pt (p,p_))
     6.9  	  handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
    6.10        val metID = get_obj g_metID pt pp;
    6.11        val {srls=srls,scr=sc,...} = get_met metID;
    6.12 @@ -356,7 +356,7 @@
    6.13        val asm = (case get_obj g_tac pt p of
    6.14  		    Check_elementwise _ => (*collects and instantiates asms*)
    6.15  		    (snd o (get_obj g_result pt)) p
    6.16 -		  | _ => ((map fst) o (get_assumptions_ pt)) (p,p_))
    6.17 +		  | _ => get_assumptions_ pt (p,p_))
    6.18  	  handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
    6.19        val metID = get_obj g_metID pt pp;
    6.20        val {srls=srls,scr=sc,...} = get_met metID;

     7.1 --- a/test/Tools/isac/Interpret/ctree.sml	Fri Apr 15 15:58:52 2011 +0200
     7.2 +++ b/test/Tools/isac/Interpret/ctree.sml	Fri Apr 15 17:07:34 2011 +0200
     7.3 @@ -64,7 +64,7 @@
     7.4  "this build should be detailed each time a test fails later    \
     7.5  \i.e. all the tests should be caught here first                \
     7.6  \and linked with a reference to the respective test environment";
     7.7 -val fmz = ["equality (x+1=(2::real))",
     7.8 +val fmz = ["equality (x+1=(2::int))",
     7.9  	   "solveFor x","solutions L"];
    7.10  val (dI',pI',mI') =
    7.11    ("Test",["sqroot-test","univariate","equation","test"],

     8.1 --- a/test/Tools/isac/Interpret/mstools.sml	Fri Apr 15 15:58:52 2011 +0200
     8.2 +++ b/test/Tools/isac/Interpret/mstools.sml	Fri Apr 15 17:07:34 2011 +0200
     8.3 @@ -1,5 +1,5 @@
     8.4  (* Title: tests for Interpret/mstools.sml
     8.5 -   Author: Walther Neuper 100930
     8.6 +   Author: Walther Neuper 100930, Mathias Lehnfeld
     8.7     (c) copyright due to lincense terms.
     8.8  
     8.9  12345678901234567890123456789012345678901234567890123456789012345678901234567890
    8.10 @@ -9,6 +9,7 @@
    8.11  "table of contents --------------------------------------";
    8.12  "--------------------------------------------------------";
    8.13  "----------- fun declare_constraints --------------------";
    8.14 +"----------- fun get_assumptions, fun get_environments --";
    8.15  "--------------------------------------------------------";
    8.16  "--------------------------------------------------------";
    8.17  "--------------------------------------------------------";
    8.18 @@ -26,8 +27,20 @@
    8.19  if ((lhs t) |> type_of) = @{typ int} then ()
    8.20    else error "mstools: incorrect type inference from parseNEW ctxt";
    8.21  
    8.22 -(*========== inhibit exn =======================================================
    8.23 -============ inhibit exn =====================================================*)
    8.24  
    8.25 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    8.26 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
    8.27 +"----------- fun get_assumptions, fun get_environments --";
    8.28 +"----------- fun get_assumptions, fun get_environments --";
    8.29 +"----------- fun get_assumptions, fun get_environments --";
    8.30 +val ctxt = insert_assumptions
    8.31 +      [@{term "x * v"}, @{term "2 * u"}, @{term "2 * u"}] ctxt;
    8.32 +val ctxt = insert_environments
    8.33 +      [(@{term "y"}, @{term "17"}), (@{term "z"}, @{term "y"})] ctxt;
    8.34 +
    8.35 +val asms = get_assumptions ctxt;
    8.36 +if asms = [@{term "x * v"}, @{term "2 * u"}] then ()
    8.37 +else error "mstools.sml insert_/get_assumptions changed.";
    8.38 +
    8.39 +val envs = get_environments ctxt;
    8.40 +if envs = [(@{term "y"}, @{term "17"}), (@{term "z"}, @{term "y"})] then ()
    8.41 +else error "mstools.sml insert_/get_environments changed.";
    8.42 +