Sign.infer_types: Name.context;
authorwenzelm
Wed Jul 19 12:11:57 2006 +0200 (2006-07-19)
changeset 20155da0505518e69
parent 20154 c709a29f1363
child 20156 7a7898b1cfa4
Sign.infer_types: Name.context;
TFL/tfl.ML
src/HOLCF/domain/theorems.ML
src/HOLCF/fixrec_package.ML
src/Pure/Tools/nbe.ML
src/Pure/sign.ML
src/Pure/theory.ML
     1.1 --- a/TFL/tfl.ML	Wed Jul 19 12:11:56 2006 +0200
     1.2 +++ b/TFL/tfl.ML	Wed Jul 19 12:11:57 2006 +0200
     1.3 @@ -367,7 +367,7 @@
     1.4  
     1.5  (*For Isabelle, the lhs of a definition must be a constant.*)
     1.6  fun mk_const_def sign (c, Ty, rhs) =
     1.7 -    Sign.infer_types (Sign.pp sign) sign (Sign.consts_of sign) (K NONE) (K NONE) [] false
     1.8 +    Sign.infer_types (Sign.pp sign) sign (Sign.consts_of sign) (K NONE) (K NONE) Name.context false
     1.9                 ([Const("==",dummyT) $ Const(c,Ty) $ rhs], propT)
    1.10      |> #1;
    1.11  
     2.1 --- a/src/HOLCF/domain/theorems.ML	Wed Jul 19 12:11:56 2006 +0200
     2.2 +++ b/src/HOLCF/domain/theorems.ML	Wed Jul 19 12:11:57 2006 +0200
     2.3 @@ -60,7 +60,7 @@
     2.4      val pp = Sign.pp sg;
     2.5      val consts = Sign.consts_of sg;
     2.6      val (t, _) =
     2.7 -      Sign.infer_types pp sg consts (K NONE) (K NONE) [] true
     2.8 +      Sign.infer_types pp sg consts (K NONE) (K NONE) Name.context true
     2.9          ([pre_tm],propT);
    2.10    in t end;
    2.11  
     3.1 --- a/src/HOLCF/fixrec_package.ML	Wed Jul 19 12:11:56 2006 +0200
     3.2 +++ b/src/HOLCF/fixrec_package.ML	Wed Jul 19 12:11:57 2006 +0200
     3.3 @@ -57,7 +57,7 @@
     3.4  (* infers the type of a term *)  (* FIXME better avoid this low-level stuff *)
     3.5  (* similar to Theory.inferT_axm, but allows any type, not just propT *)
     3.6  fun infer sg t =
     3.7 -  fst (Sign.infer_types (Sign.pp sg) sg (Sign.consts_of sg) (K NONE) (K NONE) [] true
     3.8 +  fst (Sign.infer_types (Sign.pp sg) sg (Sign.consts_of sg) (K NONE) (K NONE) Name.context true
     3.9      ([t],dummyT));
    3.10  
    3.11  (* builds the expression (LAM v. rhs) *)
     4.1 --- a/src/Pure/Tools/nbe.ML	Wed Jul 19 12:11:56 2006 +0200
     4.2 +++ b/src/Pure/Tools/nbe.ML	Wed Jul 19 12:11:57 2006 +0200
     4.3 @@ -100,8 +100,7 @@
     4.4          val vtab = var_tab t;
     4.5          val ty = type_of t;
     4.6          fun restrain ty t = Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy)
     4.7 -            (K NONE) (K NONE)
     4.8 -            [] false ([t], ty) |> fst;
     4.9 +            (K NONE) (K NONE) Name.context false ([t], ty) |> fst;
    4.10          val _ = trace (fn () => "Normalized:\n" ^ NBE_Eval.string_of_nterm nt);
    4.11          val t' = NBE_Codegen.nterm_to_term thy nt;
    4.12          val _ = trace (fn () =>"Converted back:\n" ^ Display.raw_string_of_term t');
     5.1 --- a/src/Pure/sign.ML	Wed Jul 19 12:11:56 2006 +0200
     5.2 +++ b/src/Pure/sign.ML	Wed Jul 19 12:11:57 2006 +0200
     5.3 @@ -177,14 +177,14 @@
     5.4    val read_tyname: theory -> string -> typ
     5.5    val read_const: theory -> string -> term
     5.6    val infer_types_simult: Pretty.pp -> theory -> Consts.T -> (indexname -> typ option) ->
     5.7 -    (indexname -> sort option) -> string list -> bool
     5.8 +    (indexname -> sort option) -> Name.context -> bool
     5.9      -> (term list * typ) list -> term list * (indexname * typ) list
    5.10    val infer_types: Pretty.pp -> theory -> Consts.T -> (indexname -> typ option) ->
    5.11 -    (indexname -> sort option) -> string list -> bool
    5.12 +    (indexname -> sort option) -> Name.context -> bool
    5.13      -> term list * typ -> term * (indexname * typ) list
    5.14    val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax -> Consts.T ->
    5.15      Context.generic -> (indexname -> typ option) * (indexname -> sort option) ->
    5.16 -    string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
    5.17 +    Name.context -> bool -> (string * typ) list -> term list * (indexname * typ) list
    5.18    val read_def_terms:
    5.19      theory * (indexname -> typ option) * (indexname -> sort option) ->
    5.20      string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
    5.21 @@ -574,7 +574,7 @@
    5.22  (*
    5.23    def_type: partial map from indexnames to types (constrains Frees and Vars)
    5.24    def_sort: partial map from indexnames to sorts (constrains TFrees and TVars)
    5.25 -  used: list of already used type variables
    5.26 +  used: context of already used type variables
    5.27    freeze: if true then generated parameters are turned into TFrees, else TVars
    5.28  
    5.29    termss: lists of alternative parses (only one combination should be type-correct)
    5.30 @@ -627,9 +627,9 @@
    5.31        in (Syntax.read context is_logtype syn T' s, T') end;
    5.32    in infer_types_simult pp thy consts types sorts used freeze (map read sTs) end;
    5.33  
    5.34 -fun read_def_terms (thy, types, sorts) =
    5.35 +fun read_def_terms (thy, types, sorts) used =
    5.36    read_def_terms' (pp thy) (is_logtype thy) (syn_of thy) (consts_of thy)
    5.37 -    (Context.Theory thy) (types, sorts);
    5.38 +    (Context.Theory thy) (types, sorts) (Name.make_context used);
    5.39  
    5.40  fun simple_read_term thy T s =
    5.41    let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)]
     6.1 --- a/src/Pure/theory.ML	Wed Jul 19 12:11:56 2006 +0200
     6.2 +++ b/src/Pure/theory.ML	Wed Jul 19 12:11:57 2006 +0200
     6.3 @@ -195,7 +195,8 @@
     6.4    let
     6.5      val ts = Syntax.read (Context.Theory thy) (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
     6.6      val (t, _) =
     6.7 -      Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy) types sorts used true (ts, propT);
     6.8 +      Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy)
     6.9 +        types sorts (Name.make_context used) true (ts, propT);
    6.10    in cert_axm thy (name, t) end
    6.11    handle ERROR msg => err_in_axm msg name;
    6.12  
    6.13 @@ -205,7 +206,8 @@
    6.14    let
    6.15      val pp = Sign.pp thy;
    6.16      val (t, _) =
    6.17 -      Sign.infer_types pp thy (Sign.consts_of thy) (K NONE) (K NONE) [] true ([pre_tm], propT);
    6.18 +      Sign.infer_types pp thy (Sign.consts_of thy)
    6.19 +        (K NONE) (K NONE) Name.context true ([pre_tm], propT);
    6.20    in (name, Sign.no_vars pp t) end
    6.21    handle ERROR msg => err_in_axm msg name;
    6.22