src/Pure/type_infer.ML
changeset 24764 4c2b872f8cf6
parent 24682 29306b20079b
child 24848 5dbbd33c3236
     1.1 --- a/src/Pure/type_infer.ML	Sat Sep 29 21:39:48 2007 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Sat Sep 29 21:39:49 2007 +0200
     1.3 @@ -14,10 +14,11 @@
     1.4    val param: int -> string * sort -> typ
     1.5    val paramify_vars: typ -> typ
     1.6    val paramify_dummies: typ -> int -> typ * int
     1.7 +  val fixate_params: Name.context -> term list -> term list
     1.8    val appl_error: Pretty.pp -> string -> term -> typ -> term -> typ -> string list
     1.9    val infer_types: Pretty.pp -> Type.tsig -> (typ list -> typ list) ->
    1.10 -    (string -> typ option) -> (indexname -> typ option) ->
    1.11 -    Name.context -> bool -> (term * typ) list -> (term * typ) list * (indexname * typ) list
    1.12 +    (string -> typ option) -> (indexname -> typ option) -> Name.context -> int -> bool option ->
    1.13 +    (term * typ) list -> (term * typ) list * (indexname * typ) list
    1.14  end;
    1.15  
    1.16  structure TypeInfer: TYPE_INFER =
    1.17 @@ -55,6 +56,19 @@
    1.18        | paramify T maxidx = (T, maxidx);
    1.19    in paramify end;
    1.20  
    1.21 +fun fixate_params name_context ts =
    1.22 +  let
    1.23 +    fun subst_param (xi, S) (inst, used) =
    1.24 +      if is_param xi then
    1.25 +        let
    1.26 +          val [a] = Name.invents used "'a" 1;
    1.27 +          val used' = Name.declare a used;
    1.28 +        in (((xi, S), TFree (a, S)) :: inst, used') end
    1.29 +      else (inst, used);
    1.30 +    val name_context' = (fold o fold_types) Term.declare_typ_names ts name_context;
    1.31 +    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], name_context');
    1.32 +  in (map o map_types) (TermSubst.instantiateT inst) ts end;
    1.33 +
    1.34  
    1.35  
    1.36  (** pretyps and preterms **)
    1.37 @@ -380,7 +394,7 @@
    1.38  
    1.39  (* infer_types *)
    1.40  
    1.41 -fun infer_types pp tsig check_typs const_type var_type used freeze args =
    1.42 +fun infer_types pp tsig check_typs const_type var_type used maxidx freeze_mode args =
    1.43    let
    1.44      (*check types*)
    1.45      val (raw_ts, raw_Ts) = split_list args;
    1.46 @@ -405,9 +419,10 @@
    1.47  
    1.48      (*convert back to terms/typs*)
    1.49      val mk_var =
    1.50 -      if freeze then PTFree
    1.51 -      else (fn (x, S) => PTVar ((x, 0), S));
    1.52 -    val (final_Ts, final_ts) = typs_terms_of used mk_var "" (Ts', ts');
    1.53 +      if the_default false freeze_mode then PTFree
    1.54 +      else (fn (x, S) => PTVar ((x, maxidx + 1), S));
    1.55 +    val prfx = if is_some freeze_mode then "" else "?";
    1.56 +    val (final_Ts, final_ts) = typs_terms_of used mk_var prfx (Ts', ts');
    1.57  
    1.58      (*collect result unifier*)
    1.59      val redundant = fn (xi, TVar (yi, _)) => xi = yi | _ => false;