tuned signature;
authorwenzelm
Mon Sep 13 13:20:18 2010 +0200 (2010-09-13)
changeset 39296e275d581a218
parent 39295 6e8b0672c6a2
child 39304 2f38fa28e124
tuned signature;
tuned comments;
src/Pure/Isar/proof_context.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Sep 13 12:42:08 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Sep 13 13:20:18 2010 +0200
     1.3 @@ -599,7 +599,7 @@
     1.4  
     1.5  fun prepare_patterns ctxt =
     1.6    let val Mode {pattern, ...} = get_mode ctxt in
     1.7 -    Type_Infer.fixate_params ctxt #>
     1.8 +    Type_Infer.fixate ctxt #>
     1.9      pattern ? Variable.polymorphic ctxt #>
    1.10      (map o Term.map_types) (prepare_patternT ctxt) #>
    1.11      (if pattern then prepare_dummies else map (check_dummies ctxt))
     2.1 --- a/src/Pure/type_infer.ML	Mon Sep 13 12:42:08 2010 +0200
     2.2 +++ b/src/Pure/type_infer.ML	Mon Sep 13 13:20:18 2010 +0200
     2.3 @@ -1,18 +1,22 @@
     2.4  (*  Title:      Pure/type_infer.ML
     2.5      Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     2.6  
     2.7 -Simple type inference.
     2.8 +Representation of type-inference problems.  Simple type inference.
     2.9  *)
    2.10  
    2.11  signature TYPE_INFER =
    2.12  sig
    2.13 -  val anyT: sort -> typ
    2.14    val is_param: indexname -> bool
    2.15    val is_paramT: typ -> bool
    2.16    val param: int -> string * sort -> typ
    2.17 +  val anyT: sort -> typ
    2.18    val paramify_vars: typ -> typ
    2.19    val paramify_dummies: typ -> int -> typ * int
    2.20 -  val fixate_params: Proof.context -> term list -> term list
    2.21 +  val deref: typ Vartab.table -> typ -> typ
    2.22 +  val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list
    2.23 +  val fixate: Proof.context -> term list -> term list
    2.24 +  val prepare: Proof.context -> (string -> typ option) -> (string * int -> typ option) ->
    2.25 +    term list -> int * term list
    2.26    val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) ->
    2.27      term list -> term list
    2.28  end;
    2.29 @@ -20,12 +24,8 @@
    2.30  structure Type_Infer: TYPE_INFER =
    2.31  struct
    2.32  
    2.33 -
    2.34  (** type parameters and constraints **)
    2.35  
    2.36 -fun anyT S = TFree ("'_dummy_", S);
    2.37 -
    2.38 -
    2.39  (* type inference parameters -- may get instantiated *)
    2.40  
    2.41  fun is_param (x, _: int) = String.isPrefix "?" x;
    2.42 @@ -37,6 +37,11 @@
    2.43  
    2.44  fun mk_param i S = TVar (("?'a", i), S);
    2.45  
    2.46 +
    2.47 +(* pre-stage parameters *)
    2.48 +
    2.49 +fun anyT S = TFree ("'_dummy_", S);
    2.50 +
    2.51  val paramify_vars =
    2.52    Same.commit
    2.53      (Term_Subst.map_atypsT_same
    2.54 @@ -54,19 +59,6 @@
    2.55        | paramify T maxidx = (T, maxidx);
    2.56    in paramify end;
    2.57  
    2.58 -fun fixate_params ctxt ts =
    2.59 -  let
    2.60 -    fun subst_param (xi, S) (inst, used) =
    2.61 -      if is_param xi then
    2.62 -        let
    2.63 -          val [a] = Name.invents used Name.aT 1;
    2.64 -          val used' = Name.declare a used;
    2.65 -        in (((xi, S), TFree (a, S)) :: inst, used') end
    2.66 -      else (inst, used);
    2.67 -    val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
    2.68 -    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
    2.69 -  in (map o map_types) (Term_Subst.instantiateT inst) ts end;
    2.70 -
    2.71  
    2.72  
    2.73  (** prepare types/terms: create inference parameters **)
    2.74 @@ -156,7 +148,7 @@
    2.75  
    2.76  
    2.77  
    2.78 -(** finish types/terms: standardize remaining parameters **)
    2.79 +(** results **)
    2.80  
    2.81  (* dereferenced views *)
    2.82  
    2.83 @@ -179,7 +171,7 @@
    2.84    | TVar ((x, i), _) => if is_param (x, i) then I else Name.declare x);
    2.85  
    2.86  
    2.87 -(* finish *)
    2.88 +(* finish -- standardize remaining parameters *)
    2.89  
    2.90  fun finish ctxt tye (Ts, ts) =
    2.91    let
    2.92 @@ -200,6 +192,22 @@
    2.93    in (map finish_typ Ts, map (Type.strip_constraints o Term.map_types finish_typ) ts) end;
    2.94  
    2.95  
    2.96 +(* fixate -- introduce fresh type variables *)
    2.97 +
    2.98 +fun fixate ctxt ts =
    2.99 +  let
   2.100 +    fun subst_param (xi, S) (inst, used) =
   2.101 +      if is_param xi then
   2.102 +        let
   2.103 +          val [a] = Name.invents used Name.aT 1;
   2.104 +          val used' = Name.declare a used;
   2.105 +        in (((xi, S), TFree (a, S)) :: inst, used') end
   2.106 +      else (inst, used);
   2.107 +    val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
   2.108 +    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
   2.109 +  in (map o map_types) (Term_Subst.instantiateT inst) ts end;
   2.110 +
   2.111 +
   2.112  
   2.113  (** order-sorted unification of types **)
   2.114  
   2.115 @@ -271,7 +279,7 @@
   2.116  
   2.117  
   2.118  
   2.119 -(** type inference **)
   2.120 +(** simple type inference **)
   2.121  
   2.122  (* infer *)
   2.123  
   2.124 @@ -323,25 +331,27 @@
   2.125    in inf [] end;
   2.126  
   2.127  
   2.128 -(* infer_types *)
   2.129 +(* main interfaces *)
   2.130  
   2.131 -fun infer_types ctxt const_type var_type raw_ts =
   2.132 +fun prepare ctxt const_type var_type raw_ts =
   2.133    let
   2.134 -    (*constrain vars*)
   2.135      val get_type = the_default dummyT o var_type;
   2.136      val constrain_vars = Term.map_aterms
   2.137        (fn Free (x, T) => Type.constraint T (Free (x, get_type (x, ~1)))
   2.138          | Var (xi, T) => Type.constraint T (Var (xi, get_type xi))
   2.139          | t => t);
   2.140  
   2.141 -    (*convert to preterms*)
   2.142      val ts = burrow_types (Syntax.check_typs ctxt) raw_ts;
   2.143      val (ts', (_, _, idx)) =
   2.144        fold_map (prepare_term const_type o constrain_vars) ts
   2.145        (Vartab.empty, Vartab.empty, 0);
   2.146 +  in (idx, ts') end;
   2.147  
   2.148 -    (*do type inference*)
   2.149 -    val (tye, _) = fold (snd oo infer ctxt) ts' (Vartab.empty, idx);
   2.150 -  in #2 (finish ctxt tye ([], ts')) end;
   2.151 +fun infer_types ctxt const_type var_type raw_ts =
   2.152 +  let
   2.153 +    val (idx, ts) = prepare ctxt const_type var_type raw_ts;
   2.154 +    val (tye, _) = fold (snd oo infer ctxt) ts (Vartab.empty, idx);
   2.155 +    val (_, ts') = finish ctxt tye ([], ts);
   2.156 +  in ts' end;
   2.157  
   2.158  end;