# HG changeset patch # User wenzelm # Date 1194450180 -3600 # Node ID f71105742e2ca8039decce222690b60144bcbae0 # Parent c65608a84919b190240cd4dbc027fbbb25ffba9b discontinued ProofContext.read_prop_legacy; removed obsolete Sign.read_tyname/const (cf. ProofContext); refined notion of consts within the local scope; diff -r c65608a84919 -r f71105742e2c src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Nov 07 16:42:59 2007 +0100 +++ b/src/Pure/Isar/proof_context.ML Wed Nov 07 16:43:00 2007 +0100 @@ -51,6 +51,11 @@ val get_skolem: Proof.context -> string -> string val revert_skolem: Proof.context -> string -> string val revert_skolems: Proof.context -> term -> term + val infer_type: Proof.context -> string -> typ + val inferred_param: string -> Proof.context -> (string * typ) * Proof.context + val inferred_fixes: Proof.context -> (string * typ) list * Proof.context + val read_tyname: Proof.context -> string -> typ + val read_const: Proof.context -> string -> term val decode_term: Proof.context -> term -> term val read_term_pattern: Proof.context -> string -> term val read_term_schematic: Proof.context -> string -> term @@ -58,14 +63,8 @@ val read_termTs_schematic: Proof.context -> (string -> bool) -> (indexname -> typ option) -> (indexname -> sort option) -> string list -> (string * typ) list -> term list * (indexname * typ) list - val read_prop_legacy: Proof.context -> string -> term val cert_term: Proof.context -> term -> term val cert_prop: Proof.context -> term -> term - val infer_type: Proof.context -> string -> typ - val inferred_param: string -> Proof.context -> (string * typ) * Proof.context - val inferred_fixes: Proof.context -> (string * typ) list * Proof.context - val read_tyname: Proof.context -> string -> typ - val read_const: Proof.context -> string -> term val goal_export: Proof.context -> Proof.context -> thm list -> thm list val export: Proof.context -> Proof.context -> thm list -> thm list val export_morphism: Proof.context -> Proof.context -> morphism @@ -388,6 +387,44 @@ (** prepare terms and propositions **) +(* inferred types of parameters *) + +fun infer_type ctxt x = + Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) + (Free (x, dummyT))); + +fun inferred_param x ctxt = + let val T = infer_type ctxt x + in ((x, T), ctxt |> Variable.declare_term (Free (x, T))) end; + +fun inferred_fixes ctxt = + fold_map inferred_param (rev (map #2 (Variable.fixes_of ctxt))) ctxt; + + +(* type and constant names *) + +(* type and constant names *) + +fun read_tyname ctxt c = + if Syntax.is_tid c then + TFree (c, the_default (Sign.defaultS (theory_of ctxt)) (Variable.def_sort ctxt (c, ~1))) + else + let + val thy = theory_of ctxt; + val d = Sign.intern_type thy c; + in Type (d, replicate (Sign.arity_number thy d) dummyT) end; + +fun read_const' ctxt c = + (case Variable.lookup_const ctxt c of + SOME d => Const (d, Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => error msg) + | NONE => Consts.read_const (consts_of ctxt) c); + +fun read_const ctxt c = + (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of + (SOME x, false) => Free (x, infer_type ctxt x) + | _ => read_const' ctxt c); + + (* read_term *) fun read_term_mode mode ctxt = Syntax.read_term (set_mode mode ctxt); @@ -474,7 +511,7 @@ fun legacy_intern_skolem ctxt internal def_type x = (* FIXME cleanup this mess *) let val sko = lookup_skolem ctxt x; - val is_const = can (Consts.read_const (consts_of ctxt)) x; + val is_const = can (read_const' ctxt) x; val is_scoped_const = Variable.is_const ctxt x; val is_free = (is_some sko orelse not is_const) andalso not is_scoped_const; val is_internal = internal x; @@ -492,7 +529,7 @@ fun term_context ctxt = let val thy = theory_of ctxt in {get_sort = Sign.get_sort thy (Variable.def_sort ctxt), - map_const = try (#1 o Term.dest_Const o Consts.read_const (consts_of ctxt)), + map_const = try (#1 o Term.dest_Const o read_const' ctxt), map_free = legacy_intern_skolem ctxt (K false) (Variable.def_type ctxt false), map_type = Sign.intern_tycons thy, map_sort = Sign.intern_sort thy} @@ -511,12 +548,6 @@ Sign.read_def_terms' pp (Sign.is_logtype (theory_of ctxt)) syn (consts_of ctxt) fixed ctxt (types, sorts) used freeze sTs; -fun read_def_termT freeze pp syn ctxt defaults fixed sT = - apfst hd (read_def_termTs freeze pp syn ctxt defaults fixed [sT]); - -fun read_prop_thy freeze pp syn thy defaults fixed s = - #1 (read_def_termT freeze pp syn thy defaults fixed (s, propT)); - fun append_env e1 e2 x = (case e2 x of NONE => e1 x | some => some); fun gen_read' read app schematic ctxt0 internal more_types more_sorts more_used s = @@ -533,16 +564,10 @@ |> app (singleton (prepare_patterns ctxt)) end; -fun gen_read read app schematic ctxt = - gen_read' read app schematic ctxt (K false) (K NONE) (K NONE) []; - in val read_termTs_schematic = gen_read' (read_def_termTs false) (apfst o map) true; -fun read_prop_legacy ctxt = - gen_read' (read_prop_thy true) I false ctxt (K true) (K NONE) (K NONE) []; - end; @@ -604,33 +629,6 @@ end; -(* inferred types of parameters *) - -fun infer_type ctxt x = - Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) - (Free (x, dummyT))); - -fun inferred_param x ctxt = - let val T = infer_type ctxt x - in ((x, T), ctxt |> Variable.declare_term (Free (x, T))) end; - -fun inferred_fixes ctxt = - fold_map inferred_param (rev (map #2 (Variable.fixes_of ctxt))) ctxt; - - -(* type and constant names *) - -fun read_tyname ctxt c = - if Syntax.is_tid c then - TFree (c, the_default (Sign.defaultS (theory_of ctxt)) (Variable.def_sort ctxt (c, ~1))) - else Sign.read_tyname (theory_of ctxt) c; - -fun read_const ctxt c = - (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of - (SOME x, false) => Free (x, infer_type ctxt x) - | _ => Consts.read_const (consts_of ctxt) c); - - (** inner syntax operations **)