src/Pure/type_infer.ML
author wenzelm
Wed Dec 12 23:36:07 2012 +0100 (2012-12-12 ago)
changeset 50499 f496b2b7bafb
parent 43329 84472e198515
child 53672 df8068269e90
permissions -rw-r--r--
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
wenzelm@2957
     1
(*  Title:      Pure/type_infer.ML
wenzelm@2957
     2
    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
wenzelm@2957
     3
wenzelm@42405
     4
Basic representation of type-inference problems.
wenzelm@2957
     5
*)
wenzelm@2957
     6
wenzelm@2957
     7
signature TYPE_INFER =
wenzelm@2957
     8
sig
wenzelm@24504
     9
  val is_param: indexname -> bool
wenzelm@39294
    10
  val is_paramT: typ -> bool
wenzelm@42400
    11
  val param_maxidx: term -> int -> int
wenzelm@42400
    12
  val param_maxidx_of: term list -> int
wenzelm@14788
    13
  val param: int -> string * sort -> typ
wenzelm@40286
    14
  val mk_param: int -> sort -> typ
wenzelm@39296
    15
  val anyT: sort -> typ
wenzelm@22771
    16
  val paramify_vars: typ -> typ
wenzelm@18339
    17
  val paramify_dummies: typ -> int -> typ * int
wenzelm@39296
    18
  val deref: typ Vartab.table -> typ -> typ
wenzelm@39296
    19
  val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list
wenzelm@39296
    20
  val fixate: Proof.context -> term list -> term list
wenzelm@2957
    21
end;
wenzelm@2957
    22
wenzelm@37145
    23
structure Type_Infer: TYPE_INFER =
wenzelm@2957
    24
struct
wenzelm@2957
    25
wenzelm@22698
    26
(** type parameters and constraints **)
wenzelm@2957
    27
wenzelm@39286
    28
(* type inference parameters -- may get instantiated *)
wenzelm@2957
    29
wenzelm@24504
    30
fun is_param (x, _: int) = String.isPrefix "?" x;
wenzelm@39294
    31
wenzelm@39294
    32
fun is_paramT (TVar (xi, _)) = is_param xi
wenzelm@39294
    33
  | is_paramT _ = false;
wenzelm@39294
    34
wenzelm@42400
    35
val param_maxidx =
wenzelm@42400
    36
  (Term.fold_types o Term.fold_atyps)
wenzelm@42400
    37
    (fn (TVar (xi as (_, i), _)) => if is_param xi then Integer.max i else I | _ => I);
wenzelm@42400
    38
wenzelm@42400
    39
fun param_maxidx_of ts = fold param_maxidx ts ~1;
wenzelm@42400
    40
wenzelm@22698
    41
fun param i (x, S) = TVar (("?" ^ x, i), S);
wenzelm@22698
    42
wenzelm@39294
    43
fun mk_param i S = TVar (("?'a", i), S);
wenzelm@39294
    44
wenzelm@39296
    45
wenzelm@39296
    46
(* pre-stage parameters *)
wenzelm@39296
    47
wenzelm@39296
    48
fun anyT S = TFree ("'_dummy_", S);
wenzelm@39296
    49
wenzelm@32002
    50
val paramify_vars =
wenzelm@32146
    51
  Same.commit
wenzelm@32146
    52
    (Term_Subst.map_atypsT_same
wenzelm@32146
    53
      (fn TVar ((x, i), S) => (param i (x, S)) | _ => raise Same.SAME));
wenzelm@22771
    54
wenzelm@22698
    55
val paramify_dummies =
wenzelm@22698
    56
  let
wenzelm@22698
    57
    fun dummy S maxidx = (param (maxidx + 1) ("'dummy", S), maxidx + 1);
wenzelm@2957
    58
wenzelm@22698
    59
    fun paramify (TFree ("'_dummy_", S)) maxidx = dummy S maxidx
wenzelm@22698
    60
      | paramify (Type ("dummy", _)) maxidx = dummy [] maxidx
wenzelm@22698
    61
      | paramify (Type (a, Ts)) maxidx =
wenzelm@22698
    62
          let val (Ts', maxidx') = fold_map paramify Ts maxidx
wenzelm@22698
    63
          in (Type (a, Ts'), maxidx') end
wenzelm@22698
    64
      | paramify T maxidx = (T, maxidx);
wenzelm@22698
    65
  in paramify end;
wenzelm@2957
    66
wenzelm@2957
    67
wenzelm@2957
    68
wenzelm@39296
    69
(** results **)
wenzelm@2957
    70
wenzelm@39294
    71
(* dereferenced views *)
wenzelm@2957
    72
wenzelm@39294
    73
fun deref tye (T as TVar (xi, _)) =
wenzelm@39294
    74
      (case Vartab.lookup tye xi of
wenzelm@39294
    75
        NONE => T
wenzelm@39294
    76
      | SOME U => deref tye U)
wenzelm@42400
    77
  | deref _ T = T;
wenzelm@39294
    78
wenzelm@39294
    79
fun add_parms tye T =
wenzelm@32146
    80
  (case deref tye T of
wenzelm@39294
    81
    Type (_, Ts) => fold (add_parms tye) Ts
wenzelm@39294
    82
  | TVar (xi, _) => if is_param xi then insert (op =) xi else I
wenzelm@32146
    83
  | _ => I);
wenzelm@2957
    84
wenzelm@39294
    85
fun add_names tye T =
wenzelm@32146
    86
  (case deref tye T of
wenzelm@39294
    87
    Type (_, Ts) => fold (add_names tye) Ts
wenzelm@39294
    88
  | TFree (x, _) => Name.declare x
wenzelm@39294
    89
  | TVar ((x, i), _) => if is_param (x, i) then I else Name.declare x);
wenzelm@2957
    90
wenzelm@2957
    91
wenzelm@39296
    92
(* finish -- standardize remaining parameters *)
wenzelm@2957
    93
wenzelm@39294
    94
fun finish ctxt tye (Ts, ts) =
wenzelm@39294
    95
  let
wenzelm@39294
    96
    val used =
wenzelm@39294
    97
      (fold o fold_types) (add_names tye) ts (fold (add_names tye) Ts (Variable.names_of ctxt));
wenzelm@39294
    98
    val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts []));
wenzelm@43329
    99
    val names = Name.invent used ("?" ^ Name.aT) (length parms);
wenzelm@39294
   100
    val tab = Vartab.make (parms ~~ names);
wenzelm@2957
   101
wenzelm@39294
   102
    fun finish_typ T =
wenzelm@39294
   103
      (case deref tye T of
wenzelm@39294
   104
        Type (a, Ts) => Type (a, map finish_typ Ts)
wenzelm@39294
   105
      | U as TFree _ => U
wenzelm@39294
   106
      | U as TVar (xi, S) =>
wenzelm@39294
   107
          (case Vartab.lookup tab xi of
wenzelm@39294
   108
            NONE => U
wenzelm@39295
   109
          | SOME a => TVar ((a, 0), S)));
wenzelm@39294
   110
  in (map finish_typ Ts, map (Type.strip_constraints o Term.map_types finish_typ) ts) end;
wenzelm@2957
   111
wenzelm@2957
   112
wenzelm@39296
   113
(* fixate -- introduce fresh type variables *)
wenzelm@39296
   114
wenzelm@39296
   115
fun fixate ctxt ts =
wenzelm@39296
   116
  let
wenzelm@39296
   117
    fun subst_param (xi, S) (inst, used) =
wenzelm@39296
   118
      if is_param xi then
wenzelm@39296
   119
        let
wenzelm@43329
   120
          val [a] = Name.invent used Name.aT 1;
wenzelm@39296
   121
          val used' = Name.declare a used;
wenzelm@39296
   122
        in (((xi, S), TFree (a, S)) :: inst, used') end
wenzelm@39296
   123
      else (inst, used);
wenzelm@39296
   124
    val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
wenzelm@39296
   125
    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
wenzelm@39296
   126
  in (map o map_types) (Term_Subst.instantiateT inst) ts end;
wenzelm@39296
   127
wenzelm@2957
   128
end;