1.1 --- a/src/Tools/isac/ME/ptyps.sml Wed Aug 18 16:03:27 2010 +0200
1.2 +++ b/src/Tools/isac/ME/ptyps.sml Thu Aug 19 12:00:46 2010 +0200
1.3 @@ -7,27 +7,24 @@
1.4 *)
1.5
1.6 (*-----------------------------------------vvv-(1) aus modspec.sml 23.3.02*)
1.7 -val dsc_unknown = (term_of o the o (parseold Script.thy))
1.8 +val dsc_unknown = (term_of o the o (parseold @{theory Script}))
1.9 "unknown::'a => unknow";
1.10 (*-----------------------------------------^^^-(1) aus modspec.sml 23.3.02*)
1.11
1.12
1.13 (*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*)
1.14
1.15 -
1.16 -
1.17 -
1.18 -fun itm_2item thy (Cor ((d,ts),_))= Correct(string_of_cterm (comp_dts thy(d,ts)))
1.19 - | itm_2item thy (Syn c) = SyntaxE c
1.20 - | itm_2item thy (Typ c) = TypeE c
1.21 - | itm_2item thy (Inc ((d,ts),_))= Incompl(string_of_cterm (comp_dts thy(d,ts)))
1.22 - | itm_2item thy (Sup (d,ts)) = Superfl(string_of_cterm (comp_dts thy(d,ts)))
1.23 - | itm_2item thy (Mis (d,pid)) =
1.24 - Missing (Sign.string_of_term (sign_of thy) d ^" "^
1.25 - Sign.string_of_term (sign_of thy) pid);
1.26 -
1.27 -
1.28 -
1.29 +fun itm_2item thy (Cor ((d,ts),_)) =
1.30 + Correct (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts)))
1.31 + | itm_2item _ (Syn c) = SyntaxE c
1.32 + | itm_2item _ (Typ c) = TypeE c
1.33 + | itm_2item thy (Inc ((d,ts),_)) =
1.34 + Incompl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts)))
1.35 + | itm_2item thy (Sup (d,ts)) =
1.36 + Superfl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts)))
1.37 + | itm_2item _ (Mis (d,pid)) =
1.38 + Missing (Syntax.string_of_term (ctxt_Isac"") d ^" "^
1.39 + Syntax.string_of_term (ctxt_Isac"") pid);
1.40
1.41
1.42 (* --- 8.3.00
1.43 @@ -102,7 +99,7 @@
1.44 else (e_term, [t]) (*??? 9.01 just copied*)
1.45 end)
1.46 handle _ => raise error ("split_dsc: called with "^
1.47 - (Sign.string_of_term (sign_of thy) t));
1.48 + (Syntax.string_of_term (ctxt_Isac"") t));
1.49 (*
1.50 > val t1 = (term_of o the o (parse thy)) "errorBound err_";
1.51 > split_dsc t1;
1.52 @@ -132,19 +129,19 @@
1.53 (let val (hd,[arg]) = strip_comb t
1.54 in (hd,arg) end)
1.55 handle _ => raise error ("split_did: doesn't match (hd,[arg]) for t = "
1.56 - ^(Sign.string_of_term (sign_of Script.thy) t));
1.57 + ^(Syntax.string_of_term (thy2ctxt' "Script") t));
1.58
1.59
1.60
1.61 (*create output-string for itm_*)
1.62 -fun itm_out thy (Cor ((d,ts),_)) = (string_of_cterm (comp_dts thy(d,ts)))
1.63 +fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
1.64 | itm_out thy (Syn c) = c
1.65 | itm_out thy (Typ c) = c
1.66 - | itm_out thy (Inc ((d,ts),_)) = (string_of_cterm (comp_dts thy(d,ts)))
1.67 - | itm_out thy (Sup (d,ts)) = (string_of_cterm (comp_dts thy(d,ts)))
1.68 + | itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
1.69 + | itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
1.70 | itm_out thy (Mis (d,pid)) =
1.71 - Sign.string_of_term (sign_of thy) d ^" "^
1.72 - Sign.string_of_term (sign_of thy) pid;
1.73 + Syntax.string_of_term (ctxt_Isac"") d ^" "^
1.74 + Syntax.string_of_term (ctxt_Isac"") pid;
1.75
1.76 (*22.11.00 unused
1.77 fun itm_ppc2str thy ipc = (ppc2str o (mappc (itm__2str thy))) ipc;*)
1.78 @@ -166,15 +163,15 @@
1.79 *)
1.80 (*--3.3.00
1.81 fun itm2item ((_,_,_,_,Cor (d,ts)):itm) =
1.82 - Correct (string_of_cterm (comp_dts thy(d,ts)))
1.83 + Correct (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
1.84 | itm2item (_,_,_,_,Syn (c)) = SyntaxE c
1.85 | itm2item (_,_,_,_,Typ (c)) = TypeE c
1.86 | itm2item (_,_,_,_,Fal (d,ts)) =
1.87 - False (string_of_cterm (comp_dts thy(d,ts)))
1.88 + False (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
1.89 | itm2item (_,_,_,_,Inc (d,ts)) =
1.90 - Incompl (string_of_cterm (comp_dts thy(d,ts)))
1.91 + Incompl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
1.92 | itm2item (_,_,_,_,Sup (d,ts)) =
1.93 - Superfl (string_of_cterm (comp_dts thy(d,ts)));
1.94 + Superfl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)));
1.95 *)
1.96
1.97 fun boolterm2item (true, term) = Correct (term2str term)
1.98 @@ -202,7 +199,7 @@
1.99 then ("#Relate",d,ts)
1.100 else ("#undef",d,ts);
1.101 (* 28.1.00 raise error ("add_field: '"^
1.102 - (Sign.string_of_term (sign_of thy) d)^
1.103 + (Syntax.string_of_term (ctxt_Isac"") d)^
1.104 "' not in ppc-description "); *)
1.105 ------9.3. *)
1.106
1.107 @@ -214,7 +211,7 @@
1.108 [(fi,(dsc,_))] => (fi,d,ts)
1.109 | [] => ("#undef",d,ts) (*may come with met.ppc*)
1.110 | _ => raise error ("add_field: "^
1.111 - (Sign.string_of_term (sign_of thy) d)^
1.112 + (Syntax.string_of_term (ctxt_Isac"") d)^
1.113 " more than once in pbt")
1.114 end;
1.115
1.116 @@ -229,10 +226,10 @@
1.117 [(fi,(dsc,_))] => [(i,v,fi,d,ts)]
1.118 | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)
1.119 (*raise error ("add_field': "^
1.120 - (Sign.string_of_term (sign_of thy) d)^
1.121 + (Syntax.string_of_term (ctxt_Isac"") d)^
1.122 " not in met"*)
1.123 | _ => raise error ("add_field': "^
1.124 - (Sign.string_of_term (sign_of thy) d)^
1.125 + (Syntax.string_of_term (ctxt_Isac"") d)^
1.126 " more than once in met");
1.127 in (flat ((map (repl mpc)) ori)):ori list end;
1.128
1.129 @@ -449,7 +446,7 @@
1.130 (*this is the model-pattern;
1.131 it contains "#Given","#Where","#Find","#Relate"-patterns*)
1.132 met : metID list}; (* methods solving the pbt*)
1.133 -val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=ProtoPure.thy,
1.134 +val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=theory "Pure",
1.135 cas=NONE,prls=Erls,where_=[],ppc=[],met=[]}:pbt;
1.136 fun pbt2 (str, (t1, t2)) =
1.137 pair2str (str, pair2str (term2str t1, term2str t2));
1.138 @@ -498,15 +495,15 @@
1.139 (*TODO: search generalized for subthy*)
1.140 fun get_pbt (pblID:pblID) =
1.141 let val pblRD = rev pblID;
1.142 - in get_py ProtoPure.thy pblID pblRD (!ptyps) end;
1.143 + in get_py (theory "Pure") pblID pblRD (!ptyps) end;
1.144 (* get_pbt thy ["1"];
1.145 get_pbt thy ["21","2"];
1.146 *)
1.147
1.148 (*TODO: throws exn 'get_pbt not found: ' ... confusing !!
1.149 take 'ketype' as an argument !!!!!*)
1.150 -fun get_met (metID:metID) = get_py ProtoPure.thy metID metID (!mets);
1.151 -fun get_the (theID:theID) = get_py ProtoPure.thy theID theID (!thehier);
1.152 +fun get_met (metID:metID) = get_py (theory "Pure") metID metID (!mets);
1.153 +fun get_the (theID:theID) = get_py (theory "Pure") theID theID (!thehier);
1.154
1.155
1.156
1.157 @@ -586,7 +583,7 @@
1.158
1.159
1.160 fun check_pblguh_unique (guh:guh) (pbls: (pbt ptyp) list) =
1.161 - if guh mem (coll_pblguhs pbls)
1.162 + if member op = (coll_pblguhs pbls) guh
1.163 then error ("check_guh_unique failed with '"^guh^"';\n"^
1.164 "use 'sort_pblguhs()' for a list of guhs;\n"^
1.165 "consider setting 'check_guhs_unique := false'")
1.166 @@ -594,7 +591,7 @@
1.167 (* val (guh, mets) = ("met_test", !mets);
1.168 *)
1.169 fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) =
1.170 - if guh mem (coll_metguhs mets)
1.171 + if member op = (coll_metguhs mets) guh
1.172 then error ("check_guh_unique failed with '"^guh^"';\n"^
1.173 "use 'sort_metguhs()' for a list of guhs;\n"^
1.174 "consider setting 'check_guhs_unique := false'")
1.175 @@ -818,7 +815,7 @@
1.176
1.177 (*+ transform oris +*)
1.178
1.179 -fun coll_vats (vats, ((_,vs,_,_,_):ori)) = vats union vs;
1.180 +fun coll_vats (vats, ((_,vs,_,_,_):ori)) = union op = vats vs;
1.181 (*> coll_vats [11,22] (hd oris);
1.182 val it = [22,11,1,2,3] : int list
1.183
1.184 @@ -836,7 +833,14 @@
1.185 (9,[1,2],"#undef",Const (#,#),[# $ #]),
1.186 (11,[1,2,3],"#undef",Const (#,#),[# $ #])] : ori list *)
1.187
1.188 -fun filter_vat oris i = filter ((curry (op mem) i)o(#2:ori -> int list))oris;
1.189 +local
1.190 +infix mem; (*from Isabelle2002*)
1.191 +fun x mem [] = false
1.192 + | x mem (y :: ys) = x = y orelse x mem ys;
1.193 +in
1.194 +fun filter_vat oris i =
1.195 + filter ((curry (op mem) i) o (#2 : ori -> int list)) oris;
1.196 +end;
1.197 (*> map (filter_vat oris) [1,2,3];
1.198 val it =
1.199 [[(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
1.200 @@ -861,9 +865,8 @@
1.201 (10,[3],"#undef",Const (#,#),[# $ #]),
1.202 (11,[1,2,3],"#undef",Const (#,#),[# $ #])]] : ori list list*)
1.203
1.204 -
1.205 fun separate_vats oris =
1.206 - let val vats = foldl coll_vats ([],oris);
1.207 + let val vats = foldl coll_vats ([] : int list, oris);
1.208 in map (filter_vat oris) vats end;
1.209 (*^^^ end preparational work 8.01.*)
1.210
1.211 @@ -948,7 +951,8 @@
1.212 val itms = itms; val (pbt,pre) = (ppc, pre);
1.213 *)
1.214 fun match_itms thy itms (pbt,pre,prls) =
1.215 - (let fun okv mvat (_,vats,b,_,_) = mvat mem vats andalso b;
1.216 + (let fun okv mvat (_,vats,b,_,_) = member op = vats mvat
1.217 + andalso b;
1.218 val itms' = map (chk_ thy pbt) itms; (*all found are #3 true*)
1.219 val mvat = max_vt itms';
1.220 val itms'' = filter (okv mvat) itms';
1.221 @@ -985,7 +989,7 @@
1.222 (*2*)fun oris2itms oris mis1 =
1.223 ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
1.224 val news = (flat o (map (oris2itms oris))) mis;
1.225 - (*3*)fun mem_vat (_,vats,b,_,_) = mv mem vats;
1.226 + (*3*)fun mem_vat (_,vats,b,_,_) = member op = vats mv;
1.227 val newitms = filter mem_vat news;
1.228 (*4*)val itms' = pbl @ newitms;
1.229 val pre' = check_preconds' prls pre itms' mv