src/Pure/type_infer.ML
changeset 27263 a6b7f934fbc4
parent 24848 5dbbd33c3236
child 29606 fedb8be05f24
     1.1 --- a/src/Pure/type_infer.ML	Wed Jun 18 22:32:01 2008 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Wed Jun 18 22:32:02 2008 +0200
     1.3 @@ -17,8 +17,8 @@
     1.4    val fixate_params: Name.context -> term list -> term list
     1.5    val appl_error: Pretty.pp -> string -> term -> typ -> term -> typ -> string list
     1.6    val infer_types: Pretty.pp -> Type.tsig -> (typ list -> typ list) ->
     1.7 -    (string -> typ option) -> (indexname -> typ option) -> Name.context -> int -> bool option ->
     1.8 -    (term * typ) list -> (term * typ) list * (indexname * typ) list
     1.9 +    (string -> typ option) -> (indexname -> typ option) -> Name.context -> int ->
    1.10 +    term list -> term list
    1.11  end;
    1.12  
    1.13  structure TypeInfer: TYPE_INFER =
    1.14 @@ -32,9 +32,7 @@
    1.15  (*indicate polymorphic Vars*)
    1.16  fun polymorphicT T = Type ("_polymorphic_", [T]);
    1.17  
    1.18 -fun constrain T t =
    1.19 -  if T = dummyT then t
    1.20 -  else Const ("_type_constraint_", T --> T) $ t;
    1.21 +val constrain = Syntax.type_constraint;
    1.22  
    1.23  
    1.24  (* user parameters *)
    1.25 @@ -230,18 +228,16 @@
    1.26  
    1.27  (* typs_terms_of *)                             (*DESTRUCTIVE*)
    1.28  
    1.29 -fun typs_terms_of used mk_var prfx (Ts, ts) =
    1.30 +fun typs_terms_of used maxidx (Ts, ts) =
    1.31    let
    1.32 -    fun elim (r as ref (Param S), x) = r := mk_var (x, S)
    1.33 +    fun elim (r as ref (Param S), x) = r := PTVar ((x, maxidx + 1), S)
    1.34        | elim _ = ();
    1.35  
    1.36      val used' = fold add_names ts (fold add_namesT Ts used);
    1.37      val parms = rev (fold add_parms ts (fold add_parmsT Ts []));
    1.38 -    val names = Name.invents used' (prfx ^ Name.aT) (length parms);
    1.39 -  in
    1.40 -    ListPair.app elim (parms, names);
    1.41 -    (map simple_typ_of Ts, map simple_term_of ts)
    1.42 -  end;
    1.43 +    val names = Name.invents used' ("?" ^ Name.aT) (length parms);
    1.44 +    val _ = ListPair.app elim (parms, names);
    1.45 +  in (map simple_typ_of Ts, map simple_term_of ts) end;
    1.46  
    1.47  
    1.48  
    1.49 @@ -333,11 +329,12 @@
    1.50  
    1.51      fun prep_output bs ts Ts =
    1.52        let
    1.53 -        val (Ts_bTs', ts') = typs_terms_of Name.context PTFree "??" (Ts @ map snd bs, ts);
    1.54 +        val (Ts_bTs', ts') = typs_terms_of Name.context ~1 (Ts @ map snd bs, ts);
    1.55          val (Ts', Ts'') = chop (length Ts) Ts_bTs';
    1.56 -        val xs = map Free (map fst bs ~~ Ts'');
    1.57 -        val ts'' = map (fn t => subst_bounds (xs, t)) ts';
    1.58 -      in (ts'', Ts') end;
    1.59 +        fun prep t =
    1.60 +          let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
    1.61 +          in Term.subst_bounds (map Syntax.mark_boundT xs, t) end;
    1.62 +      in (map prep ts', Ts') end;
    1.63  
    1.64      fun err_loose i =
    1.65        raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], []);
    1.66 @@ -394,13 +391,8 @@
    1.67  
    1.68  (* infer_types *)
    1.69  
    1.70 -fun infer_types pp tsig check_typs const_type var_type used maxidx freeze_mode args =
    1.71 +fun infer_types pp tsig check_typs const_type var_type used maxidx raw_ts =
    1.72    let
    1.73 -    (*check types*)
    1.74 -    val (raw_ts, raw_Ts) = split_list args;
    1.75 -    val ts = burrow_types check_typs raw_ts;
    1.76 -    val Ts = check_typs raw_Ts;
    1.77 -
    1.78      (*constrain vars*)
    1.79      val get_type = the_default dummyT o var_type;
    1.80      val constrain_vars = Term.map_aterms
    1.81 @@ -408,26 +400,13 @@
    1.82          | Var (xi, T) => constrain T (Var (xi, get_type xi))
    1.83          | t => t);
    1.84  
    1.85 -    (*convert to preterms/typs*)
    1.86 -    val (Ts', Tps) = fold_map (pretyp_of (K true)) Ts Vartab.empty;
    1.87 +    (*convert to preterms*)
    1.88 +    val ts = burrow_types check_typs raw_ts;
    1.89      val (ts', (vps, ps)) =
    1.90 -      fold_map (preterm_of const_type is_param o constrain_vars) ts (Vartab.empty, Tps);
    1.91 -
    1.92 -    (*run type inference*)
    1.93 -    val tTs' = ListPair.map Constraint (ts', Ts');
    1.94 -    val _ = List.app (fn t => (infer pp tsig t; ())) tTs';
    1.95 +      fold_map (preterm_of const_type is_param o constrain_vars) ts (Vartab.empty, Vartab.empty);
    1.96  
    1.97 -    (*convert back to terms/typs*)
    1.98 -    val mk_var =
    1.99 -      if the_default false freeze_mode then PTFree
   1.100 -      else (fn (x, S) => PTVar ((x, maxidx + 1), S));
   1.101 -    val prfx = if is_some freeze_mode then "" else "?";
   1.102 -    val (final_Ts, final_ts) = typs_terms_of used mk_var prfx (Ts', ts');
   1.103 -
   1.104 -    (*collect result unifier*)
   1.105 -    val redundant = fn (xi, TVar (yi, _)) => xi = yi | _ => false;
   1.106 -    val env = filter_out redundant (map (apsnd simple_typ_of) (Vartab.dest Tps));
   1.107 -
   1.108 -  in (final_ts ~~ final_Ts, env) end;
   1.109 +    (*do type inference*)
   1.110 +    val _ = List.app (ignore o infer pp tsig) ts';
   1.111 +  in #2 (typs_terms_of used maxidx ([], ts')) end;
   1.112  
   1.113  end;