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