# HG changeset patch # User wenzelm # Date 1176640327 -7200 # Node ID d4696154264f1f9efeea9870713ec952a8bc32cd # Parent 6199df39688dbed21272bc525dc2147a685548a7 legacy_infer_term/prop -- including intern_term; diff -r 6199df39688d -r d4696154264f src/HOLCF/domain/axioms.ML --- a/src/HOLCF/domain/axioms.ML Sun Apr 15 14:32:05 2007 +0200 +++ b/src/HOLCF/domain/axioms.ML Sun Apr 15 14:32:07 2007 +0200 @@ -14,8 +14,6 @@ infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; -fun infer_types thy' = map (Theory.inferT_axm thy'); - fun calc_axioms comp_dname (eqs : eq list) n (((dname,_),cons) : eq)= let @@ -111,11 +109,13 @@ [take_def, finite_def]) end; (* let *) +fun infer_props thy = map (apsnd (FixrecPackage.legacy_infer_prop thy)); + fun add_axioms_i x = snd o PureThy.add_axioms_i (map Thm.no_attributes x); -fun add_axioms_infer axms thy = add_axioms_i (infer_types thy axms) thy; +fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy; fun add_defs_i x = snd o (PureThy.add_defs_i false) (map Thm.no_attributes x); -fun add_defs_infer defs thy = add_defs_i (infer_types thy defs) thy; +fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; in (* local *) diff -r 6199df39688d -r d4696154264f src/HOLCF/domain/library.ML --- a/src/HOLCF/domain/library.ML Sun Apr 15 14:32:05 2007 +0200 +++ b/src/HOLCF/domain/library.ML Sun Apr 15 14:32:07 2007 +0200 @@ -134,6 +134,7 @@ val pcpoN = "Pcpo.pcpo" val pcpoS = [pcpoN]; + (* ----- support for type and mixfix expressions ----- *) infixr 5 -->; @@ -152,20 +153,9 @@ fun mk_lam (x,T) = Abs(x,dummyT,T); fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P); fun mk_ex (x,P) = mk_exists (x,dummyT,P); -local - fun sg [s] = %:s - | sg (s::ss) = %%:"_classes" $ %:s $ sg ss - | sg _ = Imposs "library:sg"; - fun sf [] = %%:"_emptysort" - | sf s = %%:"_sort" $ sg s - fun tf (Type (s,args)) = Library.foldl (op $) (%:s,map tf args) - | tf (TFree(s,sort)) = %%:"_ofsort" $ %:s $ sf sort - | tf _ = Imposs "library:tf"; -in -fun mk_constrain (typ,T) = %%:"_constrain" $ T $ tf typ; -fun mk_constrainall (x,typ,P) = %%:"All" $ (%%:"_constrainAbs" $ mk_lam(x,P) $ tf typ); -end; -end; +fun mk_constrain (typ,T) = TypeInfer.constrain T typ; +fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (mk_lam(x,P)) (typ --> boolT)); +end fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *) diff -r 6199df39688d -r d4696154264f src/HOLCF/domain/theorems.ML --- a/src/HOLCF/domain/theorems.ML Sun Apr 15 14:32:05 2007 +0200 +++ b/src/HOLCF/domain/theorems.ML Sun Apr 15 14:32:07 2007 +0200 @@ -54,19 +54,9 @@ (* ----- general proof facilities ------------------------------------------- *) -(* FIXME better avoid this low-level stuff *) -fun inferT sg pre_tm = - let - val pp = Sign.pp sg; - val consts = Sign.consts_of sg; - val (t, _) = - Sign.infer_types pp sg consts (K NONE) (K NONE) Name.context true - ([pre_tm],propT); - in t end; - fun pg'' thy defs t tacs = let - val t' = inferT thy t; + val t' = FixrecPackage.legacy_infer_term thy t; val asms = Logic.strip_imp_prems t'; val prop = Logic.strip_imp_concl t'; fun tac prems = diff -r 6199df39688d -r d4696154264f src/HOLCF/fixrec_package.ML --- a/src/HOLCF/fixrec_package.ML Sun Apr 15 14:32:05 2007 +0200 +++ b/src/HOLCF/fixrec_package.ML Sun Apr 15 14:32:07 2007 +0200 @@ -7,6 +7,8 @@ signature FIXREC_PACKAGE = sig + val legacy_infer_term: theory -> term -> term + val legacy_infer_prop: theory -> term -> term val add_fixrec: bool -> ((string * Attrib.src list) * string) list list -> theory -> theory val add_fixrec_i: bool -> ((string * attribute list) * term) list list -> theory -> theory val add_fixpat: (string * Attrib.src list) * string list -> theory -> theory @@ -16,6 +18,15 @@ structure FixrecPackage: FIXREC_PACKAGE = struct +(* legacy type inference *) + +fun legacy_infer_types thy (t, T) = + #1 (singleton (ProofContext.infer_types (ProofContext.init thy)) (Sign.intern_term thy t, T)); + +fun legacy_infer_term thy t = legacy_infer_types thy (t, dummyT); +fun legacy_infer_prop thy t = legacy_infer_types thy (t, propT); + + val fix_eq2 = thm "fix_eq2"; val def_fix_ind = thm "def_fix_ind"; @@ -50,12 +61,6 @@ infix 1 ===; fun S === T = %%:"op =" $ S $ T; infix 9 ` ; fun f ` x = %%:"Cfun.Rep_CFun" $ f $ x; -(* infers the type of a term *) (* FIXME better avoid this low-level stuff *) -(* similar to Theory.inferT_axm, but allows any type, not just propT *) -fun infer sg t = - fst (Sign.infer_types (Sign.pp sg) sg (Sign.consts_of sg) (K NONE) (K NONE) Name.context true - ([t],dummyT)); - (* builds the expression (LAM v. rhs) *) fun big_lambda v rhs = %%:"Cfun.Abs_CFun"$(Term.lambda v rhs); @@ -91,12 +96,12 @@ | defs (l::ls) r = one_def l (%%:"Cprod.cfst"`r) :: defs ls (%%:"Cprod.csnd"`r); val (names, pre_fixdefs) = ListPair.unzip (defs lhss fixpoint); - val fixdefs = map (Theory.inferT_axm thy) pre_fixdefs; + val fixdefs = map (apsnd (legacy_infer_prop thy)) pre_fixdefs; val (fixdef_thms, thy') = PureThy.add_defs_i false (map Thm.no_attributes fixdefs) thy; val ctuple_fixdef_thm = foldr1 (fn (x,y) => cpair_equalI OF [x,y]) fixdef_thms; - val ctuple_unfold = infer thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss)); + val ctuple_unfold = legacy_infer_term thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss)); val ctuple_unfold_thm = Goal.prove_global thy' [] [] ctuple_unfold (fn _ => EVERY [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1, simp_tac (simpset_of thy') 1]); @@ -232,7 +237,7 @@ fun unconcat [] _ = [] | unconcat (n::ns) xs = List.take (xs,n) :: unconcat ns (List.drop (xs,n)); val pattern_blocks = unconcat lengths (map Logic.strip_imp_concl eqn_ts'); - val compiled_ts = map (infer thy o compile_pats) pattern_blocks; + val compiled_ts = map (legacy_infer_term thy o compile_pats) pattern_blocks; val (thy', cnames, fixdef_thms, unfold_thms) = add_fixdefs compiled_ts thy; in if strict then let (* only prove simp rules if strict = true *)