# HG changeset patch # User Walther Neuper # Date 1282212046 -7200 # Node ID dfec2cf32f772d4f7e299a8c2994da147cbc4977 # Parent 183e35109ddaa28511aa3d7bb0354e8ddd85e544 updated ME/generate diff -r 183e35109dda -r dfec2cf32f77 src/Tools/isac/Isac_Mathengine.thy --- a/src/Tools/isac/Isac_Mathengine.thy Wed Aug 18 16:03:27 2010 +0200 +++ b/src/Tools/isac/Isac_Mathengine.thy Thu Aug 19 12:00:46 2010 +0200 @@ -35,16 +35,15 @@ use "ME/mstools.sml" use "ME/ctree.sml" use "ME/ptyps.sml" - +use "ME/generate.sml" ML {* -member; -@{term 111}; +thy2ctxt; *} + (* -use "ME/generate.sml" use "ME/calchead.sml" use "ME/appl.sml" use "ME/rewtools.sml" diff -r 183e35109dda -r dfec2cf32f77 src/Tools/isac/ME/ctree.sml --- a/src/Tools/isac/ME/ctree.sml Wed Aug 18 16:03:27 2010 +0200 +++ b/src/Tools/isac/ME/ctree.sml Thu Aug 19 12:00:46 2010 +0200 @@ -1510,7 +1510,7 @@ (apfst bool2str)))) bts; fun ocalhd2str ((b, p, hdf, itms, prec, spec):ocalhd) = "("^bool2str b^", "^pos_2str p^", "^term2str hdf^ - ", "^itms2str_ (thy2ctxt "Isac") itms^ + ", "^itms2str_ (thy2ctxt' "Isac") itms^ ", "^preconds2str prec^", \n"^spec2str spec^" )"; diff -r 183e35109dda -r dfec2cf32f77 src/Tools/isac/ME/generate.sml --- a/src/Tools/isac/ME/generate.sml Wed Aug 18 16:03:27 2010 +0200 +++ b/src/Tools/isac/ME/generate.sml Thu Aug 19 12:00:46 2010 +0200 @@ -478,7 +478,7 @@ val pt = update_pblppc pt p pbl;--------4.9.03->Model_Problem*) (*val _= writeln("### generate1: is([3],Frm)= "^ (istate2str (get_istate pt ([3],Frm))));*) - val f = Sign.string_of_term (sign_of thy) f; + val f = Syntax.string_of_term (thy2ctxt thy) f; in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end | generate1 thy m' _ _ _ = diff -r 183e35109dda -r dfec2cf32f77 src/Tools/isac/ME/mstools.sml --- a/src/Tools/isac/ME/mstools.sml Wed Aug 18 16:03:27 2010 +0200 +++ b/src/Tools/isac/ME/mstools.sml Thu Aug 19 12:00:46 2010 +0200 @@ -399,7 +399,7 @@ fun getval (id, values) = case values of [] => raise error ("penv_value: no values in '"^ - (Syntax.string_of_term (thy2ctxt "Tools") id)) + (Syntax.string_of_term (thy2ctxt' "Tools") id)) | [v] => (id, v) | (v1::v2::_) => (case v1 of Const ("Script.Arbfix",_) => (id, v2) @@ -809,7 +809,7 @@ "Mis "^ Syntax.string_of_term ctxt d ^ " "^ Syntax.string_of_term ctxt pid | itm_2str_ ctxt (Par s) = "Trm "^s; -fun itm_2str t = itm_2str_ (thy2ctxt "Isac") t; +fun itm_2str t = itm_2str_ (thy2ctxt' "Isac") t; fun itm2str_ ctxt ((i,is,b,s,itm_):itm) = "("^(string_of_int i)^" ,"^(ints2str' is)^" ,"^(bool2str b)^" ,"^ s^" ,"^(itm_2str_ ctxt itm_)^")"; diff -r 183e35109dda -r dfec2cf32f77 src/Tools/isac/ME/ptyps.sml --- a/src/Tools/isac/ME/ptyps.sml Wed Aug 18 16:03:27 2010 +0200 +++ b/src/Tools/isac/ME/ptyps.sml Thu Aug 19 12:00:46 2010 +0200 @@ -7,27 +7,24 @@ *) (*-----------------------------------------vvv-(1) aus modspec.sml 23.3.02*) -val dsc_unknown = (term_of o the o (parseold Script.thy)) +val dsc_unknown = (term_of o the o (parseold @{theory Script})) "unknown::'a => unknow"; (*-----------------------------------------^^^-(1) aus modspec.sml 23.3.02*) (*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*) - - - -fun itm_2item thy (Cor ((d,ts),_))= Correct(string_of_cterm (comp_dts thy(d,ts))) - | itm_2item thy (Syn c) = SyntaxE c - | itm_2item thy (Typ c) = TypeE c - | itm_2item thy (Inc ((d,ts),_))= Incompl(string_of_cterm (comp_dts thy(d,ts))) - | itm_2item thy (Sup (d,ts)) = Superfl(string_of_cterm (comp_dts thy(d,ts))) - | itm_2item thy (Mis (d,pid)) = - Missing (Sign.string_of_term (sign_of thy) d ^" "^ - Sign.string_of_term (sign_of thy) pid); - - - +fun itm_2item thy (Cor ((d,ts),_)) = + Correct (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts))) + | itm_2item _ (Syn c) = SyntaxE c + | itm_2item _ (Typ c) = TypeE c + | itm_2item thy (Inc ((d,ts),_)) = + Incompl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts))) + | itm_2item thy (Sup (d,ts)) = + Superfl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts))) + | itm_2item _ (Mis (d,pid)) = + Missing (Syntax.string_of_term (ctxt_Isac"") d ^" "^ + Syntax.string_of_term (ctxt_Isac"") pid); (* --- 8.3.00 @@ -102,7 +99,7 @@ else (e_term, [t]) (*??? 9.01 just copied*) end) handle _ => raise error ("split_dsc: called with "^ - (Sign.string_of_term (sign_of thy) t)); + (Syntax.string_of_term (ctxt_Isac"") t)); (* > val t1 = (term_of o the o (parse thy)) "errorBound err_"; > split_dsc t1; @@ -132,19 +129,19 @@ (let val (hd,[arg]) = strip_comb t in (hd,arg) end) handle _ => raise error ("split_did: doesn't match (hd,[arg]) for t = " - ^(Sign.string_of_term (sign_of Script.thy) t)); + ^(Syntax.string_of_term (thy2ctxt' "Script") t)); (*create output-string for itm_*) -fun itm_out thy (Cor ((d,ts),_)) = (string_of_cterm (comp_dts thy(d,ts))) +fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) | itm_out thy (Syn c) = c | itm_out thy (Typ c) = c - | itm_out thy (Inc ((d,ts),_)) = (string_of_cterm (comp_dts thy(d,ts))) - | itm_out thy (Sup (d,ts)) = (string_of_cterm (comp_dts thy(d,ts))) + | itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) + | itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) | itm_out thy (Mis (d,pid)) = - Sign.string_of_term (sign_of thy) d ^" "^ - Sign.string_of_term (sign_of thy) pid; + Syntax.string_of_term (ctxt_Isac"") d ^" "^ + Syntax.string_of_term (ctxt_Isac"") pid; (*22.11.00 unused fun itm_ppc2str thy ipc = (ppc2str o (mappc (itm__2str thy))) ipc;*) @@ -166,15 +163,15 @@ *) (*--3.3.00 fun itm2item ((_,_,_,_,Cor (d,ts)):itm) = - Correct (string_of_cterm (comp_dts thy(d,ts))) + Correct (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) | itm2item (_,_,_,_,Syn (c)) = SyntaxE c | itm2item (_,_,_,_,Typ (c)) = TypeE c | itm2item (_,_,_,_,Fal (d,ts)) = - False (string_of_cterm (comp_dts thy(d,ts))) + False (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) | itm2item (_,_,_,_,Inc (d,ts)) = - Incompl (string_of_cterm (comp_dts thy(d,ts))) + Incompl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) | itm2item (_,_,_,_,Sup (d,ts)) = - Superfl (string_of_cterm (comp_dts thy(d,ts))); + Superfl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))); *) fun boolterm2item (true, term) = Correct (term2str term) @@ -202,7 +199,7 @@ then ("#Relate",d,ts) else ("#undef",d,ts); (* 28.1.00 raise error ("add_field: '"^ - (Sign.string_of_term (sign_of thy) d)^ + (Syntax.string_of_term (ctxt_Isac"") d)^ "' not in ppc-description "); *) ------9.3. *) @@ -214,7 +211,7 @@ [(fi,(dsc,_))] => (fi,d,ts) | [] => ("#undef",d,ts) (*may come with met.ppc*) | _ => raise error ("add_field: "^ - (Sign.string_of_term (sign_of thy) d)^ + (Syntax.string_of_term (ctxt_Isac"") d)^ " more than once in pbt") end; @@ -229,10 +226,10 @@ [(fi,(dsc,_))] => [(i,v,fi,d,ts)] | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*) (*raise error ("add_field': "^ - (Sign.string_of_term (sign_of thy) d)^ + (Syntax.string_of_term (ctxt_Isac"") d)^ " not in met"*) | _ => raise error ("add_field': "^ - (Sign.string_of_term (sign_of thy) d)^ + (Syntax.string_of_term (ctxt_Isac"") d)^ " more than once in met"); in (flat ((map (repl mpc)) ori)):ori list end; @@ -449,7 +446,7 @@ (*this is the model-pattern; it contains "#Given","#Where","#Find","#Relate"-patterns*) met : metID list}; (* methods solving the pbt*) -val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=ProtoPure.thy, +val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=theory "Pure", cas=NONE,prls=Erls,where_=[],ppc=[],met=[]}:pbt; fun pbt2 (str, (t1, t2)) = pair2str (str, pair2str (term2str t1, term2str t2)); @@ -498,15 +495,15 @@ (*TODO: search generalized for subthy*) fun get_pbt (pblID:pblID) = let val pblRD = rev pblID; - in get_py ProtoPure.thy pblID pblRD (!ptyps) end; + in get_py (theory "Pure") pblID pblRD (!ptyps) end; (* get_pbt thy ["1"]; get_pbt thy ["21","2"]; *) (*TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument !!!!!*) -fun get_met (metID:metID) = get_py ProtoPure.thy metID metID (!mets); -fun get_the (theID:theID) = get_py ProtoPure.thy theID theID (!thehier); +fun get_met (metID:metID) = get_py (theory "Pure") metID metID (!mets); +fun get_the (theID:theID) = get_py (theory "Pure") theID theID (!thehier); @@ -586,7 +583,7 @@ fun check_pblguh_unique (guh:guh) (pbls: (pbt ptyp) list) = - if guh mem (coll_pblguhs pbls) + if member op = (coll_pblguhs pbls) guh then error ("check_guh_unique failed with '"^guh^"';\n"^ "use 'sort_pblguhs()' for a list of guhs;\n"^ "consider setting 'check_guhs_unique := false'") @@ -594,7 +591,7 @@ (* val (guh, mets) = ("met_test", !mets); *) fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) = - if guh mem (coll_metguhs mets) + if member op = (coll_metguhs mets) guh then error ("check_guh_unique failed with '"^guh^"';\n"^ "use 'sort_metguhs()' for a list of guhs;\n"^ "consider setting 'check_guhs_unique := false'") @@ -818,7 +815,7 @@ (*+ transform oris +*) -fun coll_vats (vats, ((_,vs,_,_,_):ori)) = vats union vs; +fun coll_vats (vats, ((_,vs,_,_,_):ori)) = union op = vats vs; (*> coll_vats [11,22] (hd oris); val it = [22,11,1,2,3] : int list @@ -836,7 +833,14 @@ (9,[1,2],"#undef",Const (#,#),[# $ #]), (11,[1,2,3],"#undef",Const (#,#),[# $ #])] : ori list *) -fun filter_vat oris i = filter ((curry (op mem) i)o(#2:ori -> int list))oris; +local +infix mem; (*from Isabelle2002*) +fun x mem [] = false + | x mem (y :: ys) = x = y orelse x mem ys; +in +fun filter_vat oris i = + filter ((curry (op mem) i) o (#2 : ori -> int list)) oris; +end; (*> map (filter_vat oris) [1,2,3]; val it = [[(1,[1,2,3],"#Given",Const (#,#),[# $ #]), @@ -861,9 +865,8 @@ (10,[3],"#undef",Const (#,#),[# $ #]), (11,[1,2,3],"#undef",Const (#,#),[# $ #])]] : ori list list*) - fun separate_vats oris = - let val vats = foldl coll_vats ([],oris); + let val vats = foldl coll_vats ([] : int list, oris); in map (filter_vat oris) vats end; (*^^^ end preparational work 8.01.*) @@ -948,7 +951,8 @@ val itms = itms; val (pbt,pre) = (ppc, pre); *) fun match_itms thy itms (pbt,pre,prls) = - (let fun okv mvat (_,vats,b,_,_) = mvat mem vats andalso b; + (let fun okv mvat (_,vats,b,_,_) = member op = vats mvat + andalso b; val itms' = map (chk_ thy pbt) itms; (*all found are #3 true*) val mvat = max_vt itms'; val itms'' = filter (okv mvat) itms'; @@ -985,7 +989,7 @@ (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris; val news = (flat o (map (oris2itms oris))) mis; - (*3*)fun mem_vat (_,vats,b,_,_) = mv mem vats; + (*3*)fun mem_vat (_,vats,b,_,_) = member op = vats mv; val newitms = filter mem_vat news; (*4*)val itms' = pbl @ newitms; val pre' = check_preconds' prls pre itms' mv diff -r 183e35109dda -r dfec2cf32f77 src/Tools/isac/calcelems.sml --- a/src/Tools/isac/calcelems.sml Wed Aug 18 16:03:27 2010 +0200 +++ b/src/Tools/isac/calcelems.sml Thu Aug 19 12:00:46 2010 +0200 @@ -131,13 +131,14 @@ (*1.8.02 ad (how to restrict type ???): scr should be usable indepentently from rls, and then contain both Script _AND_ Rfuns !!!*) -fun thy2ctxt thy' = ProofContext.init_global (theory thy'); (*FIXXXME thy-ctxt*) +fun thy2ctxt' thy' = ProofContext.init_global (theory thy');(*FIXXXME thy-ctxt*) +fun thy2ctxt thy = ProofContext.init_global thy;(*FIXXXME thy-ctxt*) (*ctxt for retrieval of all thms in HOL; FIXME make this local?*) (*val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");*) -val ctxt_HOL = thy2ctxt "Complex_Main"; +val ctxt_HOL = thy2ctxt' "Complex_Main"; (*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*) -fun ctxt_Isac _ = thy2ctxt "Isac"; +fun ctxt_Isac _ = thy2ctxt' "Isac"; fun Isac _ = ProofContext.theory_of (ctxt_Isac""); val e_rule = Thm ("refl", ProofContext.get_thm ctxt_HOL "refl" ); @@ -548,9 +549,10 @@ (*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy)) handle _ => raise error ("ME_Isa: thy '"^thy^"' not in system");*) -fun assoc_thy (thy:theory') = theory - ((implode o (curry takelast 4) o explode) thy); - +fun assoc_thy (thy:theory') = (*FIXME100818 abolish*) + (theory ((implode o (curry takelast 4) o explode) thy)) + handle _ => raise error ("ME_Isa: thy '" ^ thy ^ "' not in system"); + (*.associate an rls-identifier with an rls; related to 'fun assoc_rls'; these are NOT compatible to "fun assoc_thm'" in that they do NOT handle overlays by re-using an identifier in different thys.*)