Name.context for used'';
authorwenzelm
Wed Jul 19 12:12:04 2006 +0200 (2006-07-19)
changeset 20161b8b1d4a380aa
parent 20160 550e36c6a2d1
child 20162 d4bcb27686f9
Name.context for used'';
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Wed Jul 19 12:12:03 2006 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Wed Jul 19 12:12:04 2006 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4    val infer_types: Pretty.pp
     1.5      -> Type.tsig -> (string -> typ option) -> (indexname -> typ option)
     1.6      -> (indexname -> sort option) -> (string -> string) -> (typ -> typ)
     1.7 -    -> (sort -> sort) -> string list -> bool -> typ list -> term list
     1.8 +    -> (sort -> sort) -> Name.context -> bool -> typ list -> term list
     1.9      -> term list * (indexname * typ) list
    1.10  end;
    1.11  
    1.12 @@ -208,11 +208,11 @@
    1.13  
    1.14  (* add_names *)
    1.15  
    1.16 -fun add_namesT (PType (_, Ts)) xs = fold add_namesT Ts xs
    1.17 -  | add_namesT (PTFree (x, _)) xs = x ins_string xs
    1.18 -  | add_namesT (PTVar ((x, _), _)) xs = x ins_string xs
    1.19 -  | add_namesT (Link (ref T)) xs = add_namesT T xs
    1.20 -  | add_namesT (Param _) xs = xs;
    1.21 +fun add_namesT (PType (_, Ts)) = fold add_namesT Ts
    1.22 +  | add_namesT (PTFree (x, _)) = Name.declare x
    1.23 +  | add_namesT (PTVar ((x, _), _)) = Name.declare x
    1.24 +  | add_namesT (Link (ref T)) = add_namesT T
    1.25 +  | add_namesT (Param _) = I;
    1.26  
    1.27  val add_names = fold_pretyps add_namesT;
    1.28  
    1.29 @@ -245,7 +245,7 @@
    1.30  
    1.31      val used' = fold add_names ts (fold add_namesT Ts used);
    1.32      val parms = rev (fold add_parms ts (fold add_parmsT Ts []));
    1.33 -    val names = Name.invent_list used' (prfx ^ "'a") (length parms);
    1.34 +    val names = Name.invents used' (prfx ^ "'a") (length parms);
    1.35    in
    1.36      ListPair.app elim (parms, names);
    1.37      (map simple_typ_of Ts, map simple_term_of ts)
    1.38 @@ -340,7 +340,7 @@
    1.39  
    1.40      fun prep_output bs ts Ts =
    1.41        let
    1.42 -        val (Ts_bTs', ts') = typs_terms_of [] PTFree "??" (Ts @ map snd bs, ts);
    1.43 +        val (Ts_bTs', ts') = typs_terms_of Name.context PTFree "??" (Ts @ map snd bs, ts);
    1.44          val (Ts', Ts'') = chop (length Ts) Ts_bTs';
    1.45          val xs = map Free (map fst bs ~~ Ts'');
    1.46          val ts'' = map (fn t => subst_bounds (xs, t)) ts';
    1.47 @@ -522,7 +522,7 @@
    1.48    const_type: name mapping and signature lookup
    1.49    def_type: partial map from indexnames to types (constrains Frees and Vars)
    1.50    def_sort: partial map from indexnames to sorts (constrains TFrees and TVars)
    1.51 -  used: list of already used type variables
    1.52 +  used: context of already used type variables
    1.53    freeze: if true then generated parameters are turned into TFrees, else TVars*)
    1.54  
    1.55  fun infer_types pp tsig const_type def_type def_sort