# HG changeset patch # User Mathias Lehnfeld # Date 1302880054 -7200 # Node ID 703d656a62913fe971192ea83dc5bff3481900ad # Parent 03151cfbdc025a67d13633aa96ed57d178ed503a intermed. ctxt integration - assumptions now in context diff -r 03151cfbdc02 -r 703d656a6291 src/Tools/isac/Frontend/interface.sml --- a/src/Tools/isac/Frontend/interface.sml Fri Apr 15 15:58:52 2011 +0200 +++ b/src/Tools/isac/Frontend/interface.sml Fri Apr 15 17:07:34 2011 +0200 @@ -286,7 +286,7 @@ (*WN0502 @see ME/ctree: type asms: illdesigned, thus no positions returned*) fun getAccumulatedAsms cI (p:pos') = (let val ((pt, _), _) = get_calc cI - val ass = map fst (get_assumptions_ pt p) + val ass = get_assumptions_ pt p in (*getaccuasmsOK2xml cI (get_assumptions_ pt p)*) getasmsOK2xml cI ass end) handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms"; diff -r 03151cfbdc02 -r 703d656a6291 src/Tools/isac/Interpret/appl.sml --- a/src/Tools/isac/Interpret/appl.sml Fri Apr 15 15:58:52 2011 +0200 +++ b/src/Tools/isac/Interpret/appl.sml Fri Apr 15 17:07:34 2011 +0200 @@ -93,7 +93,7 @@ | mk_set thy pt p (Const ("Tools.UniversalList",_)) pred = (e_term, if pred <> Const ("Script.Assumptions",bool) then [pred] - else (map fst) (get_assumptions_ pt (p,Res))) + else get_assumptions_ pt (p,Res)) (* val pred = (term_of o the o (parse thy)) pred; val consts as Const ("List.list.Cons",_) $ eq $ _ = ft; @@ -103,7 +103,7 @@ let val (bdv,_) = HOLogic.dest_eq eq; val pred = if pred <> Const ("Script.Assumptions",bool) then [pred] - else (map fst) (get_assumptions_ pt (p,Res)) + else get_assumptions_ pt (p,Res) in (bdv, pred) end | mk_set thy _ _ l _ = diff -r 03151cfbdc02 -r 703d656a6291 src/Tools/isac/Interpret/ctree.sml --- a/src/Tools/isac/Interpret/ctree.sml Fri Apr 15 15:58:52 2011 +0200 +++ b/src/Tools/isac/Interpret/ctree.sml Fri Apr 15 17:07:34 2011 +0200 @@ -193,8 +193,6 @@ val e_pos' = ([],Und):pos'; fun res2str (t, ts) = pair2str (term2str t, terms2str ts); -fun asm2str (t, p:pos) = pair2str (term2str t, ints2str' p); -fun asms2str asms = (strs2str' o (map asm2str)) asms; @@ -1347,47 +1345,7 @@ fun get_istate pt p = get_loc pt p |> #1; fun get_ctxt pt p = get_loc pt p |> #2; -(*.collect the assumptions within a problem up to a certain position.*) -type asms = (term * pos) list;(*WN0502 should be (pos' * term) list - ...........===^===*) - -fun get_asm (b:pos, p:pos) (Nd (PblObj {result=(_,asm),...},_)) = - ((*tracing ("### get_asm PblObj:(b,p)= "^ - (pair2str(ints2str b, ints2str p)));*) - (map (rpair b) asm):asms) - | get_asm (b, p) (Nd (PrfObj {result=(_,asm),...}, [])) = - ((*tracing ("### get_asm PrfObj []:(b,p)= "^ - (pair2str(ints2str b, ints2str p)));*) - (map (rpair b) asm)) - | get_asm (b, p:pos) (Nd (PrfObj _, nds)) = - let (*val _= tracing ("### get_asm PrfObj nds:(b,p)= "^ - (pair2str(ints2str b, ints2str p)));*) - val levdn = - if p <> [] then (b @ [hd p]:pos, tl p:pos) - else (b @ [1], [99999]) (*_deeper_ nesting is always _before_ p*) - in gets_asm levdn 1 nds end -and gets_asm _ _ [] = [] - | gets_asm (b, p' as p::ps) i (nd::nds) = - if p < i then [] - else ((*tracing ("### gets_asm: (b,p')= "^(pair2str(ints2str b, - ints2str p')));*) - (get_asm (b @ [i], ps) nd) @ (gets_asm (b, p') (i + 1) nds)); - -fun get_assumptions_ (Nd (PblObj {result=(r,asm),...}, cn)) (([], _):pos') = - if r = e_term then gets_asm ([], [99999]) 1 cn - else map (rpair []) asm - | get_assumptions_ pt (p,p_) = - let val (cn, base) = par_children pt p - val offset = drop (length base, p) - val base' = replicate (length base) 1 - val offset' = case p_ of - Frm => let val (qs,q) = split_last offset - in qs @ [q - 1] end - | _ => offset - (*val _= tracing ("... get_assumptions: (b,o)= "^ - (pair2str(ints2str base',ints2str offset)))*) - in gets_asm (base', offset) 1 cn end; - +fun get_assumptions_ pt p = get_ctxt pt p |> get_assumptions; (*--------- end diff -r 03151cfbdc02 -r 703d656a6291 src/Tools/isac/Interpret/generate.sml --- a/src/Tools/isac/Interpret/generate.sml Fri Apr 15 15:58:52 2011 +0200 +++ b/src/Tools/isac/Interpret/generate.sml Fri Apr 15 17:07:34 2011 +0200 @@ -373,18 +373,21 @@ in ((p',Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end - | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f',asm))) l (p,p_) pt = + | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f',asm))) (is, ctxt) + (p,p_) pt = let (*val _= tracing("###generate1 Rewrite_Inst': pos= "^pos'2str (p,p_));*) - val (pt,c) = cappend_atomic pt p l f + val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f (Rewrite_Inst (subst2subs subs',thm')) (f',asm) Complete; val pt = update_branch pt p TransitiveB (*040312*) (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*) in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end - | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) l (p,p_) pt = + | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) (is, ctxt) + (p,p_) pt = let (*val _= tracing("###generate1 Rewrite': pos= "^pos'2str (p,p_))*) - val (pt,c) = cappend_atomic pt p l f (Rewrite thm') (f',asm) Complete + val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f + (Rewrite thm') (f',asm) Complete val pt = update_branch pt p TransitiveB (*040312*) (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*) in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), @@ -393,44 +396,46 @@ | generate1 thy (Rewrite_Asm' all) l p pt = generate1 thy (Rewrite' all) l p pt - | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) l (p,p_) pt = + | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) (is, ctxt) + (p,p_) pt = (* val (thy, Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm)), l, (p,p_), pt) = (assoc_thy "Isac", tac_, is, pos, pt); *) let (*val _=tracing("###generate1 Rewrite_Set_Inst': pos= "^pos'2str(p,p_))*) - val (pt,c) = cappend_atomic pt p l f + val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f (Rewrite_Set_Inst (subst2subs subs',id_rls rls')) (f',asm) Complete val pt = update_branch pt p TransitiveB (*040312*) (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*) in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end - | generate1 thy (Detail_Set_Inst' (_,_,subs,rls,f,(f',asm))) l (p,p_) pt = - let val (pt,c) = cappend_form pt p l f + | generate1 thy (Detail_Set_Inst' (_,_,subs,rls,f,(f',asm))) (is, ctxt) (p,p_) + pt = + let val ctxt' = insert_assumptions asm ctxt + val (pt,c) = cappend_form pt p (is, ctxt') f val pt = update_branch pt p TransitiveB (*040312*) + val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f + val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt') + val pos' = ((lev_on o lev_dn) p, Frm) + in (*implicit Take*) generate1 thy tac_ (is, ctxt') pos' pt end - val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f - val tac_ = Apply_Method' (e_metID, SOME t, is, e_ctxt) - val pos' = ((lev_on o lev_dn) p, Frm) - in (*implicit Take*) generate1 thy tac_ (is, e_ctxt) pos' pt end - - | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) l (p,p_) pt = + | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) (is, ctxt) (p,p_) pt = let (*val _= tracing("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))*) - val (pt,c) = cappend_atomic pt p l f + val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f (Rewrite_Set (id_rls rls')) (f',asm) Complete val pt = update_branch pt p TransitiveB (*040312*) (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*) in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end - | generate1 thy (Detail_Set' (_,_,rls,f,(f',asm))) l (p,p_) pt = - let val (pt,c) = cappend_form pt p l f + | generate1 thy (Detail_Set' (_,_,rls,f,(f',asm))) (is, ctxt) (p,p_) pt = + let val (pt,c) = cappend_form pt p (is, ctxt) f val pt = update_branch pt p TransitiveB (*040312*) val is = init_istate (Rewrite_Set (id_rls rls)) f - val tac_ = Apply_Method' (e_metID, SOME t, is, e_ctxt) + val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt) val pos' = ((lev_on o lev_dn) p, Frm) - in (*implicit Take*) generate1 thy tac_ (is, e_ctxt) pos' pt end + in (*implicit Take*) generate1 thy tac_ (is, ctxt) pos' pt end | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt = let (*val _=tracing("###generate1 Check_Postcond': pos= "^pos'2str(p,p_))*) @@ -552,7 +557,7 @@ val (SOME (ist, ctxt),_) = get_obj g_loc pt p val form = get_obj g_form pt p (*val p = lev_on p; ---------------only difference to (..,Res) below*) - val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, e_ctxt))) + val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, ctxt))) ::(insert_pos ((lev_on o lev_dn) p) tacis) @ [(End_Trans, End_Trans' (res, asm), (pos_plus (length tacis) (lev_dn p, Res), @@ -573,7 +578,7 @@ val (_, SOME (ist, ctxt)) = get_obj g_loc pt p val (f,a) = get_obj g_result pt p val p = lev_on p(*---------------only difference to (..,Frm) above*); - val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, e_ctxt))) + val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, ctxt))) ::(insert_pos ((lev_on o lev_dn) p) tacis) @ [(End_Trans, End_Trans' (res, asm), (pos_plus (length tacis) (lev_dn p, Res), diff -r 03151cfbdc02 -r 703d656a6291 src/Tools/isac/Interpret/mstools.sml --- a/src/Tools/isac/Interpret/mstools.sml Fri Apr 15 15:58:52 2011 +0200 +++ b/src/Tools/isac/Interpret/mstools.sml Fri Apr 15 17:07:34 2011 +0200 @@ -2,7 +2,7 @@ modspec.sml. The types are separated from calchead.sml into this file, because some of them are stored in the calc-tree, and thus are required _before_ ctree.sml. - author: Walther Neuper + author: Walther Neuper, Mathias Lehnfeld (c) due to copyright terms use"ME/mstools.sml" (*re-evaluate sml/ from scratch!*); @@ -153,6 +153,12 @@ val vts_cnt : int list -> itm list -> (int * int) list val vts_in : itm list -> int list (* val w_itms2str_ : Proof.context -> itm list -> unit *) + val get_assumptions : Proof.context -> term list + val get_environments : Proof.context -> (term * term) list + val insert_assumptions : term list -> Proof.context -> Proof.context + val insert_environments : + (term * term) list -> Proof.context -> Proof.context + end (*----------------------------------------------------------*) @@ -973,6 +979,33 @@ val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars; in fold Variable.declare_constraints ts ctxt end; +datatype Isac_Ctxt = + Env of term * term + | Asm of term; + +structure ContextData = Proof_Data + (type T = Isac_Ctxt list + fun init _ = []); + +local + fun unpack_asms (Asm t::ts) = t::(unpack_asms ts) + | unpack_asms (Env _::ts) = unpack_asms ts + | unpack_asms [] = []; + fun unpack_envs (Env t::ts) = t::(unpack_envs ts) + | unpack_envs (Asm _::ts) = unpack_envs ts + | unpack_envs [] = []; +in + fun get_assumptions ctxt = ContextData.get ctxt |> unpack_asms; + fun get_environments ctxt = ContextData.get ctxt |> unpack_envs; +end + +local + fun insert_ctxt data = ContextData.map (fn xs => distinct data@xs); +in + fun insert_assumptions asms = map (fn t => Asm t) asms |> insert_ctxt; + fun insert_environments envs = map (fn t => Env t) envs |> insert_ctxt; +end + (*----------------------------------------------------------*) end open SpecifyTools; diff -r 03151cfbdc02 -r 703d656a6291 src/Tools/isac/Interpret/solve.sml --- a/src/Tools/isac/Interpret/solve.sml Fri Apr 15 15:58:52 2011 +0200 +++ b/src/Tools/isac/Interpret/solve.sml Fri Apr 15 17:07:34 2011 +0200 @@ -200,7 +200,7 @@ val asm = (case get_obj g_tac pt p of Check_elementwise _ => (*collects and instantiates asms*) (snd o (get_obj g_result pt)) p - | _ => ((map fst) o (get_assumptions_ pt)) (p,p_)) + | _ => get_assumptions_ pt (p,p_)) handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*) val metID = get_obj g_metID pt pp; val {srls=srls,scr=sc,...} = get_met metID; @@ -356,7 +356,7 @@ val asm = (case get_obj g_tac pt p of Check_elementwise _ => (*collects and instantiates asms*) (snd o (get_obj g_result pt)) p - | _ => ((map fst) o (get_assumptions_ pt)) (p,p_)) + | _ => get_assumptions_ pt (p,p_)) handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*) val metID = get_obj g_metID pt pp; val {srls=srls,scr=sc,...} = get_met metID; diff -r 03151cfbdc02 -r 703d656a6291 test/Tools/isac/Interpret/ctree.sml --- a/test/Tools/isac/Interpret/ctree.sml Fri Apr 15 15:58:52 2011 +0200 +++ b/test/Tools/isac/Interpret/ctree.sml Fri Apr 15 17:07:34 2011 +0200 @@ -64,7 +64,7 @@ "this build should be detailed each time a test fails later \ \i.e. all the tests should be caught here first \ \and linked with a reference to the respective test environment"; -val fmz = ["equality (x+1=(2::real))", +val fmz = ["equality (x+1=(2::int))", "solveFor x","solutions L"]; val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"], diff -r 03151cfbdc02 -r 703d656a6291 test/Tools/isac/Interpret/mstools.sml --- a/test/Tools/isac/Interpret/mstools.sml Fri Apr 15 15:58:52 2011 +0200 +++ b/test/Tools/isac/Interpret/mstools.sml Fri Apr 15 17:07:34 2011 +0200 @@ -1,5 +1,5 @@ (* Title: tests for Interpret/mstools.sml - Author: Walther Neuper 100930 + Author: Walther Neuper 100930, Mathias Lehnfeld (c) copyright due to lincense terms. 12345678901234567890123456789012345678901234567890123456789012345678901234567890 @@ -9,6 +9,7 @@ "table of contents --------------------------------------"; "--------------------------------------------------------"; "----------- fun declare_constraints --------------------"; +"----------- fun get_assumptions, fun get_environments --"; "--------------------------------------------------------"; "--------------------------------------------------------"; "--------------------------------------------------------"; @@ -26,8 +27,20 @@ if ((lhs t) |> type_of) = @{typ int} then () else error "mstools: incorrect type inference from parseNEW ctxt"; -(*========== inhibit exn ======================================================= -============ inhibit exn =====================================================*) -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) +"----------- fun get_assumptions, fun get_environments --"; +"----------- fun get_assumptions, fun get_environments --"; +"----------- fun get_assumptions, fun get_environments --"; +val ctxt = insert_assumptions + [@{term "x * v"}, @{term "2 * u"}, @{term "2 * u"}] ctxt; +val ctxt = insert_environments + [(@{term "y"}, @{term "17"}), (@{term "z"}, @{term "y"})] ctxt; + +val asms = get_assumptions ctxt; +if asms = [@{term "x * v"}, @{term "2 * u"}] then () +else error "mstools.sml insert_/get_assumptions changed."; + +val envs = get_environments ctxt; +if envs = [(@{term "y"}, @{term "17"}), (@{term "z"}, @{term "y"})] then () +else error "mstools.sml insert_/get_environments changed."; +