1.1 --- a/src/Tools/isac/Isac_Mathengine.thy Wed Aug 18 16:03:27 2010 +0200
1.2 +++ b/src/Tools/isac/Isac_Mathengine.thy Thu Aug 19 12:00:46 2010 +0200
1.3 @@ -35,16 +35,15 @@
1.4 use "ME/mstools.sml"
1.5 use "ME/ctree.sml"
1.6 use "ME/ptyps.sml"
1.7 -
1.8 +use "ME/generate.sml"
1.9
1.10 ML {*
1.11 -member;
1.12 -@{term 111};
1.13 +thy2ctxt;
1.14 *}
1.15
1.16
1.17 +
1.18 (*
1.19 -use "ME/generate.sml"
1.20 use "ME/calchead.sml"
1.21 use "ME/appl.sml"
1.22 use "ME/rewtools.sml"
2.1 --- a/src/Tools/isac/ME/ctree.sml Wed Aug 18 16:03:27 2010 +0200
2.2 +++ b/src/Tools/isac/ME/ctree.sml Thu Aug 19 12:00:46 2010 +0200
2.3 @@ -1510,7 +1510,7 @@
2.4 (apfst bool2str)))) bts;
2.5 fun ocalhd2str ((b, p, hdf, itms, prec, spec):ocalhd) =
2.6 "("^bool2str b^", "^pos_2str p^", "^term2str hdf^
2.7 - ", "^itms2str_ (thy2ctxt "Isac") itms^
2.8 + ", "^itms2str_ (thy2ctxt' "Isac") itms^
2.9 ", "^preconds2str prec^", \n"^spec2str spec^" )";
2.10
2.11
3.1 --- a/src/Tools/isac/ME/generate.sml Wed Aug 18 16:03:27 2010 +0200
3.2 +++ b/src/Tools/isac/ME/generate.sml Thu Aug 19 12:00:46 2010 +0200
3.3 @@ -478,7 +478,7 @@
3.4 val pt = update_pblppc pt p pbl;--------4.9.03->Model_Problem*)
3.5 (*val _= writeln("### generate1: is([3],Frm)= "^
3.6 (istate2str (get_istate pt ([3],Frm))));*)
3.7 - val f = Sign.string_of_term (sign_of thy) f;
3.8 + val f = Syntax.string_of_term (thy2ctxt thy) f;
3.9 in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
3.10
3.11 | generate1 thy m' _ _ _ =
4.1 --- a/src/Tools/isac/ME/mstools.sml Wed Aug 18 16:03:27 2010 +0200
4.2 +++ b/src/Tools/isac/ME/mstools.sml Thu Aug 19 12:00:46 2010 +0200
4.3 @@ -399,7 +399,7 @@
4.4 fun getval (id, values) =
4.5 case values of
4.6 [] => raise error ("penv_value: no values in '"^
4.7 - (Syntax.string_of_term (thy2ctxt "Tools") id))
4.8 + (Syntax.string_of_term (thy2ctxt' "Tools") id))
4.9 | [v] => (id, v)
4.10 | (v1::v2::_) => (case v1 of
4.11 Const ("Script.Arbfix",_) => (id, v2)
4.12 @@ -809,7 +809,7 @@
4.13 "Mis "^ Syntax.string_of_term ctxt d ^
4.14 " "^ Syntax.string_of_term ctxt pid
4.15 | itm_2str_ ctxt (Par s) = "Trm "^s;
4.16 -fun itm_2str t = itm_2str_ (thy2ctxt "Isac") t;
4.17 +fun itm_2str t = itm_2str_ (thy2ctxt' "Isac") t;
4.18 fun itm2str_ ctxt ((i,is,b,s,itm_):itm) =
4.19 "("^(string_of_int i)^" ,"^(ints2str' is)^" ,"^(bool2str b)^" ,"^
4.20 s^" ,"^(itm_2str_ ctxt itm_)^")";
5.1 --- a/src/Tools/isac/ME/ptyps.sml Wed Aug 18 16:03:27 2010 +0200
5.2 +++ b/src/Tools/isac/ME/ptyps.sml Thu Aug 19 12:00:46 2010 +0200
5.3 @@ -7,27 +7,24 @@
5.4 *)
5.5
5.6 (*-----------------------------------------vvv-(1) aus modspec.sml 23.3.02*)
5.7 -val dsc_unknown = (term_of o the o (parseold Script.thy))
5.8 +val dsc_unknown = (term_of o the o (parseold @{theory Script}))
5.9 "unknown::'a => unknow";
5.10 (*-----------------------------------------^^^-(1) aus modspec.sml 23.3.02*)
5.11
5.12
5.13 (*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*)
5.14
5.15 -
5.16 -
5.17 -
5.18 -fun itm_2item thy (Cor ((d,ts),_))= Correct(string_of_cterm (comp_dts thy(d,ts)))
5.19 - | itm_2item thy (Syn c) = SyntaxE c
5.20 - | itm_2item thy (Typ c) = TypeE c
5.21 - | itm_2item thy (Inc ((d,ts),_))= Incompl(string_of_cterm (comp_dts thy(d,ts)))
5.22 - | itm_2item thy (Sup (d,ts)) = Superfl(string_of_cterm (comp_dts thy(d,ts)))
5.23 - | itm_2item thy (Mis (d,pid)) =
5.24 - Missing (Sign.string_of_term (sign_of thy) d ^" "^
5.25 - Sign.string_of_term (sign_of thy) pid);
5.26 -
5.27 -
5.28 -
5.29 +fun itm_2item thy (Cor ((d,ts),_)) =
5.30 + Correct (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts)))
5.31 + | itm_2item _ (Syn c) = SyntaxE c
5.32 + | itm_2item _ (Typ c) = TypeE c
5.33 + | itm_2item thy (Inc ((d,ts),_)) =
5.34 + Incompl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts)))
5.35 + | itm_2item thy (Sup (d,ts)) =
5.36 + Superfl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts)))
5.37 + | itm_2item _ (Mis (d,pid)) =
5.38 + Missing (Syntax.string_of_term (ctxt_Isac"") d ^" "^
5.39 + Syntax.string_of_term (ctxt_Isac"") pid);
5.40
5.41
5.42 (* --- 8.3.00
5.43 @@ -102,7 +99,7 @@
5.44 else (e_term, [t]) (*??? 9.01 just copied*)
5.45 end)
5.46 handle _ => raise error ("split_dsc: called with "^
5.47 - (Sign.string_of_term (sign_of thy) t));
5.48 + (Syntax.string_of_term (ctxt_Isac"") t));
5.49 (*
5.50 > val t1 = (term_of o the o (parse thy)) "errorBound err_";
5.51 > split_dsc t1;
5.52 @@ -132,19 +129,19 @@
5.53 (let val (hd,[arg]) = strip_comb t
5.54 in (hd,arg) end)
5.55 handle _ => raise error ("split_did: doesn't match (hd,[arg]) for t = "
5.56 - ^(Sign.string_of_term (sign_of Script.thy) t));
5.57 + ^(Syntax.string_of_term (thy2ctxt' "Script") t));
5.58
5.59
5.60
5.61 (*create output-string for itm_*)
5.62 -fun itm_out thy (Cor ((d,ts),_)) = (string_of_cterm (comp_dts thy(d,ts)))
5.63 +fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
5.64 | itm_out thy (Syn c) = c
5.65 | itm_out thy (Typ c) = c
5.66 - | itm_out thy (Inc ((d,ts),_)) = (string_of_cterm (comp_dts thy(d,ts)))
5.67 - | itm_out thy (Sup (d,ts)) = (string_of_cterm (comp_dts thy(d,ts)))
5.68 + | itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
5.69 + | itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
5.70 | itm_out thy (Mis (d,pid)) =
5.71 - Sign.string_of_term (sign_of thy) d ^" "^
5.72 - Sign.string_of_term (sign_of thy) pid;
5.73 + Syntax.string_of_term (ctxt_Isac"") d ^" "^
5.74 + Syntax.string_of_term (ctxt_Isac"") pid;
5.75
5.76 (*22.11.00 unused
5.77 fun itm_ppc2str thy ipc = (ppc2str o (mappc (itm__2str thy))) ipc;*)
5.78 @@ -166,15 +163,15 @@
5.79 *)
5.80 (*--3.3.00
5.81 fun itm2item ((_,_,_,_,Cor (d,ts)):itm) =
5.82 - Correct (string_of_cterm (comp_dts thy(d,ts)))
5.83 + Correct (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
5.84 | itm2item (_,_,_,_,Syn (c)) = SyntaxE c
5.85 | itm2item (_,_,_,_,Typ (c)) = TypeE c
5.86 | itm2item (_,_,_,_,Fal (d,ts)) =
5.87 - False (string_of_cterm (comp_dts thy(d,ts)))
5.88 + False (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
5.89 | itm2item (_,_,_,_,Inc (d,ts)) =
5.90 - Incompl (string_of_cterm (comp_dts thy(d,ts)))
5.91 + Incompl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
5.92 | itm2item (_,_,_,_,Sup (d,ts)) =
5.93 - Superfl (string_of_cterm (comp_dts thy(d,ts)));
5.94 + Superfl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)));
5.95 *)
5.96
5.97 fun boolterm2item (true, term) = Correct (term2str term)
5.98 @@ -202,7 +199,7 @@
5.99 then ("#Relate",d,ts)
5.100 else ("#undef",d,ts);
5.101 (* 28.1.00 raise error ("add_field: '"^
5.102 - (Sign.string_of_term (sign_of thy) d)^
5.103 + (Syntax.string_of_term (ctxt_Isac"") d)^
5.104 "' not in ppc-description "); *)
5.105 ------9.3. *)
5.106
5.107 @@ -214,7 +211,7 @@
5.108 [(fi,(dsc,_))] => (fi,d,ts)
5.109 | [] => ("#undef",d,ts) (*may come with met.ppc*)
5.110 | _ => raise error ("add_field: "^
5.111 - (Sign.string_of_term (sign_of thy) d)^
5.112 + (Syntax.string_of_term (ctxt_Isac"") d)^
5.113 " more than once in pbt")
5.114 end;
5.115
5.116 @@ -229,10 +226,10 @@
5.117 [(fi,(dsc,_))] => [(i,v,fi,d,ts)]
5.118 | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)
5.119 (*raise error ("add_field': "^
5.120 - (Sign.string_of_term (sign_of thy) d)^
5.121 + (Syntax.string_of_term (ctxt_Isac"") d)^
5.122 " not in met"*)
5.123 | _ => raise error ("add_field': "^
5.124 - (Sign.string_of_term (sign_of thy) d)^
5.125 + (Syntax.string_of_term (ctxt_Isac"") d)^
5.126 " more than once in met");
5.127 in (flat ((map (repl mpc)) ori)):ori list end;
5.128
5.129 @@ -449,7 +446,7 @@
5.130 (*this is the model-pattern;
5.131 it contains "#Given","#Where","#Find","#Relate"-patterns*)
5.132 met : metID list}; (* methods solving the pbt*)
5.133 -val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=ProtoPure.thy,
5.134 +val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=theory "Pure",
5.135 cas=NONE,prls=Erls,where_=[],ppc=[],met=[]}:pbt;
5.136 fun pbt2 (str, (t1, t2)) =
5.137 pair2str (str, pair2str (term2str t1, term2str t2));
5.138 @@ -498,15 +495,15 @@
5.139 (*TODO: search generalized for subthy*)
5.140 fun get_pbt (pblID:pblID) =
5.141 let val pblRD = rev pblID;
5.142 - in get_py ProtoPure.thy pblID pblRD (!ptyps) end;
5.143 + in get_py (theory "Pure") pblID pblRD (!ptyps) end;
5.144 (* get_pbt thy ["1"];
5.145 get_pbt thy ["21","2"];
5.146 *)
5.147
5.148 (*TODO: throws exn 'get_pbt not found: ' ... confusing !!
5.149 take 'ketype' as an argument !!!!!*)
5.150 -fun get_met (metID:metID) = get_py ProtoPure.thy metID metID (!mets);
5.151 -fun get_the (theID:theID) = get_py ProtoPure.thy theID theID (!thehier);
5.152 +fun get_met (metID:metID) = get_py (theory "Pure") metID metID (!mets);
5.153 +fun get_the (theID:theID) = get_py (theory "Pure") theID theID (!thehier);
5.154
5.155
5.156
5.157 @@ -586,7 +583,7 @@
5.158
5.159
5.160 fun check_pblguh_unique (guh:guh) (pbls: (pbt ptyp) list) =
5.161 - if guh mem (coll_pblguhs pbls)
5.162 + if member op = (coll_pblguhs pbls) guh
5.163 then error ("check_guh_unique failed with '"^guh^"';\n"^
5.164 "use 'sort_pblguhs()' for a list of guhs;\n"^
5.165 "consider setting 'check_guhs_unique := false'")
5.166 @@ -594,7 +591,7 @@
5.167 (* val (guh, mets) = ("met_test", !mets);
5.168 *)
5.169 fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) =
5.170 - if guh mem (coll_metguhs mets)
5.171 + if member op = (coll_metguhs mets) guh
5.172 then error ("check_guh_unique failed with '"^guh^"';\n"^
5.173 "use 'sort_metguhs()' for a list of guhs;\n"^
5.174 "consider setting 'check_guhs_unique := false'")
5.175 @@ -818,7 +815,7 @@
5.176
5.177 (*+ transform oris +*)
5.178
5.179 -fun coll_vats (vats, ((_,vs,_,_,_):ori)) = vats union vs;
5.180 +fun coll_vats (vats, ((_,vs,_,_,_):ori)) = union op = vats vs;
5.181 (*> coll_vats [11,22] (hd oris);
5.182 val it = [22,11,1,2,3] : int list
5.183
5.184 @@ -836,7 +833,14 @@
5.185 (9,[1,2],"#undef",Const (#,#),[# $ #]),
5.186 (11,[1,2,3],"#undef",Const (#,#),[# $ #])] : ori list *)
5.187
5.188 -fun filter_vat oris i = filter ((curry (op mem) i)o(#2:ori -> int list))oris;
5.189 +local
5.190 +infix mem; (*from Isabelle2002*)
5.191 +fun x mem [] = false
5.192 + | x mem (y :: ys) = x = y orelse x mem ys;
5.193 +in
5.194 +fun filter_vat oris i =
5.195 + filter ((curry (op mem) i) o (#2 : ori -> int list)) oris;
5.196 +end;
5.197 (*> map (filter_vat oris) [1,2,3];
5.198 val it =
5.199 [[(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
5.200 @@ -861,9 +865,8 @@
5.201 (10,[3],"#undef",Const (#,#),[# $ #]),
5.202 (11,[1,2,3],"#undef",Const (#,#),[# $ #])]] : ori list list*)
5.203
5.204 -
5.205 fun separate_vats oris =
5.206 - let val vats = foldl coll_vats ([],oris);
5.207 + let val vats = foldl coll_vats ([] : int list, oris);
5.208 in map (filter_vat oris) vats end;
5.209 (*^^^ end preparational work 8.01.*)
5.210
5.211 @@ -948,7 +951,8 @@
5.212 val itms = itms; val (pbt,pre) = (ppc, pre);
5.213 *)
5.214 fun match_itms thy itms (pbt,pre,prls) =
5.215 - (let fun okv mvat (_,vats,b,_,_) = mvat mem vats andalso b;
5.216 + (let fun okv mvat (_,vats,b,_,_) = member op = vats mvat
5.217 + andalso b;
5.218 val itms' = map (chk_ thy pbt) itms; (*all found are #3 true*)
5.219 val mvat = max_vt itms';
5.220 val itms'' = filter (okv mvat) itms';
5.221 @@ -985,7 +989,7 @@
5.222 (*2*)fun oris2itms oris mis1 =
5.223 ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
5.224 val news = (flat o (map (oris2itms oris))) mis;
5.225 - (*3*)fun mem_vat (_,vats,b,_,_) = mv mem vats;
5.226 + (*3*)fun mem_vat (_,vats,b,_,_) = member op = vats mv;
5.227 val newitms = filter mem_vat news;
5.228 (*4*)val itms' = pbl @ newitms;
5.229 val pre' = check_preconds' prls pre itms' mv
6.1 --- a/src/Tools/isac/calcelems.sml Wed Aug 18 16:03:27 2010 +0200
6.2 +++ b/src/Tools/isac/calcelems.sml Thu Aug 19 12:00:46 2010 +0200
6.3 @@ -131,13 +131,14 @@
6.4 (*1.8.02 ad (how to restrict type ???): scr should be usable indepentently
6.5 from rls, and then contain both Script _AND_ Rfuns !!!*)
6.6
6.7 -fun thy2ctxt thy' = ProofContext.init_global (theory thy'); (*FIXXXME thy-ctxt*)
6.8 +fun thy2ctxt' thy' = ProofContext.init_global (theory thy');(*FIXXXME thy-ctxt*)
6.9 +fun thy2ctxt thy = ProofContext.init_global thy;(*FIXXXME thy-ctxt*)
6.10
6.11 (*ctxt for retrieval of all thms in HOL; FIXME make this local?*)
6.12 (*val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");*)
6.13 -val ctxt_HOL = thy2ctxt "Complex_Main";
6.14 +val ctxt_HOL = thy2ctxt' "Complex_Main";
6.15 (*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*)
6.16 -fun ctxt_Isac _ = thy2ctxt "Isac";
6.17 +fun ctxt_Isac _ = thy2ctxt' "Isac";
6.18 fun Isac _ = ProofContext.theory_of (ctxt_Isac"");
6.19
6.20 val e_rule = Thm ("refl", ProofContext.get_thm ctxt_HOL "refl" );
6.21 @@ -548,9 +549,10 @@
6.22
6.23 (*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
6.24 handle _ => raise error ("ME_Isa: thy '"^thy^"' not in system");*)
6.25 -fun assoc_thy (thy:theory') = theory
6.26 - ((implode o (curry takelast 4) o explode) thy);
6.27 -
6.28 +fun assoc_thy (thy:theory') = (*FIXME100818 abolish*)
6.29 + (theory ((implode o (curry takelast 4) o explode) thy))
6.30 + handle _ => raise error ("ME_Isa: thy '" ^ thy ^ "' not in system");
6.31 +
6.32 (*.associate an rls-identifier with an rls; related to 'fun assoc_rls';
6.33 these are NOT compatible to "fun assoc_thm'" in that they do NOT handle
6.34 overlays by re-using an identifier in different thys.*)