# HG changeset patch # User wenzelm # Date 1153303917 -7200 # Node ID da0505518e690bc456204fe19e2482936d46977f # Parent c709a29f1363846c3069c387ab0f3cd9608e7c4f Sign.infer_types: Name.context; diff -r c709a29f1363 -r da0505518e69 TFL/tfl.ML --- a/TFL/tfl.ML Wed Jul 19 12:11:56 2006 +0200 +++ b/TFL/tfl.ML Wed Jul 19 12:11:57 2006 +0200 @@ -367,7 +367,7 @@ (*For Isabelle, the lhs of a definition must be a constant.*) fun mk_const_def sign (c, Ty, rhs) = - Sign.infer_types (Sign.pp sign) sign (Sign.consts_of sign) (K NONE) (K NONE) [] false + Sign.infer_types (Sign.pp sign) sign (Sign.consts_of sign) (K NONE) (K NONE) Name.context false ([Const("==",dummyT) $ Const(c,Ty) $ rhs], propT) |> #1; diff -r c709a29f1363 -r da0505518e69 src/HOLCF/domain/theorems.ML --- a/src/HOLCF/domain/theorems.ML Wed Jul 19 12:11:56 2006 +0200 +++ b/src/HOLCF/domain/theorems.ML Wed Jul 19 12:11:57 2006 +0200 @@ -60,7 +60,7 @@ val pp = Sign.pp sg; val consts = Sign.consts_of sg; val (t, _) = - Sign.infer_types pp sg consts (K NONE) (K NONE) [] true + Sign.infer_types pp sg consts (K NONE) (K NONE) Name.context true ([pre_tm],propT); in t end; diff -r c709a29f1363 -r da0505518e69 src/HOLCF/fixrec_package.ML --- a/src/HOLCF/fixrec_package.ML Wed Jul 19 12:11:56 2006 +0200 +++ b/src/HOLCF/fixrec_package.ML Wed Jul 19 12:11:57 2006 +0200 @@ -57,7 +57,7 @@ (* 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) [] true + 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) *) diff -r c709a29f1363 -r da0505518e69 src/Pure/Tools/nbe.ML --- a/src/Pure/Tools/nbe.ML Wed Jul 19 12:11:56 2006 +0200 +++ b/src/Pure/Tools/nbe.ML Wed Jul 19 12:11:57 2006 +0200 @@ -100,8 +100,7 @@ val vtab = var_tab t; val ty = type_of t; fun restrain ty t = Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy) - (K NONE) (K NONE) - [] false ([t], ty) |> fst; + (K NONE) (K NONE) Name.context false ([t], ty) |> fst; val _ = trace (fn () => "Normalized:\n" ^ NBE_Eval.string_of_nterm nt); val t' = NBE_Codegen.nterm_to_term thy nt; val _ = trace (fn () =>"Converted back:\n" ^ Display.raw_string_of_term t'); diff -r c709a29f1363 -r da0505518e69 src/Pure/sign.ML --- a/src/Pure/sign.ML Wed Jul 19 12:11:56 2006 +0200 +++ b/src/Pure/sign.ML Wed Jul 19 12:11:57 2006 +0200 @@ -177,14 +177,14 @@ val read_tyname: theory -> string -> typ val read_const: theory -> string -> term val infer_types_simult: Pretty.pp -> theory -> Consts.T -> (indexname -> typ option) -> - (indexname -> sort option) -> string list -> bool + (indexname -> sort option) -> Name.context -> bool -> (term list * typ) list -> term list * (indexname * typ) list val infer_types: Pretty.pp -> theory -> Consts.T -> (indexname -> typ option) -> - (indexname -> sort option) -> string list -> bool + (indexname -> sort option) -> Name.context -> bool -> term list * typ -> term * (indexname * typ) list val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax -> Consts.T -> Context.generic -> (indexname -> typ option) * (indexname -> sort option) -> - string list -> bool -> (string * typ) list -> term list * (indexname * typ) list + Name.context -> bool -> (string * typ) list -> term list * (indexname * typ) list val read_def_terms: theory * (indexname -> typ option) * (indexname -> sort option) -> string list -> bool -> (string * typ) list -> term list * (indexname * typ) list @@ -574,7 +574,7 @@ (* def_type: partial map from indexnames to types (constrains Frees and Vars) def_sort: partial map from indexnames to sorts (constrains TFrees and TVars) - used: list of already used type variables + used: context of already used type variables freeze: if true then generated parameters are turned into TFrees, else TVars termss: lists of alternative parses (only one combination should be type-correct) @@ -627,9 +627,9 @@ in (Syntax.read context is_logtype syn T' s, T') end; in infer_types_simult pp thy consts types sorts used freeze (map read sTs) end; -fun read_def_terms (thy, types, sorts) = +fun read_def_terms (thy, types, sorts) used = read_def_terms' (pp thy) (is_logtype thy) (syn_of thy) (consts_of thy) - (Context.Theory thy) (types, sorts); + (Context.Theory thy) (types, sorts) (Name.make_context used); fun simple_read_term thy T s = let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)] diff -r c709a29f1363 -r da0505518e69 src/Pure/theory.ML --- a/src/Pure/theory.ML Wed Jul 19 12:11:56 2006 +0200 +++ b/src/Pure/theory.ML Wed Jul 19 12:11:57 2006 +0200 @@ -195,7 +195,8 @@ let val ts = Syntax.read (Context.Theory thy) (Sign.is_logtype thy) (Sign.syn_of thy) propT str; val (t, _) = - Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy) types sorts used true (ts, propT); + Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy) + types sorts (Name.make_context used) true (ts, propT); in cert_axm thy (name, t) end handle ERROR msg => err_in_axm msg name; @@ -205,7 +206,8 @@ let val pp = Sign.pp thy; val (t, _) = - Sign.infer_types pp thy (Sign.consts_of thy) (K NONE) (K NONE) [] true ([pre_tm], propT); + Sign.infer_types pp thy (Sign.consts_of thy) + (K NONE) (K NONE) Name.context true ([pre_tm], propT); in (name, Sign.no_vars pp t) end handle ERROR msg => err_in_axm msg name;