src/Pure/type_infer.ML
author wenzelm
Mon Sep 16 23:04:13 2013 +0200 (2013-09-16)
changeset 53672 df8068269e90
parent 43329 84472e198515
child 62958 b41c1cb5e251
permissions -rw-r--r--
removed dead code (see also 69d4543811d0);
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@39296
    17
  val deref: typ Vartab.table -> typ -> typ
wenzelm@39296
    18
  val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list
wenzelm@39296
    19
  val fixate: Proof.context -> term list -> term list
wenzelm@2957
    20
end;
wenzelm@2957
    21
wenzelm@37145
    22
structure Type_Infer: TYPE_INFER =
wenzelm@2957
    23
struct
wenzelm@2957
    24
wenzelm@22698
    25
(** type parameters and constraints **)
wenzelm@2957
    26
wenzelm@39286
    27
(* type inference parameters -- may get instantiated *)
wenzelm@2957
    28
wenzelm@24504
    29
fun is_param (x, _: int) = String.isPrefix "?" x;
wenzelm@39294
    30
wenzelm@39294
    31
fun is_paramT (TVar (xi, _)) = is_param xi
wenzelm@39294
    32
  | is_paramT _ = false;
wenzelm@39294
    33
wenzelm@42400
    34
val param_maxidx =
wenzelm@42400
    35
  (Term.fold_types o Term.fold_atyps)
wenzelm@42400
    36
    (fn (TVar (xi as (_, i), _)) => if is_param xi then Integer.max i else I | _ => I);
wenzelm@42400
    37
wenzelm@42400
    38
fun param_maxidx_of ts = fold param_maxidx ts ~1;
wenzelm@42400
    39
wenzelm@22698
    40
fun param i (x, S) = TVar (("?" ^ x, i), S);
wenzelm@22698
    41
wenzelm@39294
    42
fun mk_param i S = TVar (("?'a", i), S);
wenzelm@39294
    43
wenzelm@39296
    44
wenzelm@39296
    45
(* pre-stage parameters *)
wenzelm@39296
    46
wenzelm@39296
    47
fun anyT S = TFree ("'_dummy_", S);
wenzelm@39296
    48
wenzelm@32002
    49
val paramify_vars =
wenzelm@32146
    50
  Same.commit
wenzelm@32146
    51
    (Term_Subst.map_atypsT_same
wenzelm@32146
    52
      (fn TVar ((x, i), S) => (param i (x, S)) | _ => raise Same.SAME));
wenzelm@22771
    53
wenzelm@2957
    54
wenzelm@2957
    55
wenzelm@39296
    56
(** results **)
wenzelm@2957
    57
wenzelm@39294
    58
(* dereferenced views *)
wenzelm@2957
    59
wenzelm@39294
    60
fun deref tye (T as TVar (xi, _)) =
wenzelm@39294
    61
      (case Vartab.lookup tye xi of
wenzelm@39294
    62
        NONE => T
wenzelm@39294
    63
      | SOME U => deref tye U)
wenzelm@42400
    64
  | deref _ T = T;
wenzelm@39294
    65
wenzelm@39294
    66
fun add_parms tye T =
wenzelm@32146
    67
  (case deref tye T of
wenzelm@39294
    68
    Type (_, Ts) => fold (add_parms tye) Ts
wenzelm@39294
    69
  | TVar (xi, _) => if is_param xi then insert (op =) xi else I
wenzelm@32146
    70
  | _ => I);
wenzelm@2957
    71
wenzelm@39294
    72
fun add_names tye T =
wenzelm@32146
    73
  (case deref tye T of
wenzelm@39294
    74
    Type (_, Ts) => fold (add_names tye) Ts
wenzelm@39294
    75
  | TFree (x, _) => Name.declare x
wenzelm@39294
    76
  | TVar ((x, i), _) => if is_param (x, i) then I else Name.declare x);
wenzelm@2957
    77
wenzelm@2957
    78
wenzelm@39296
    79
(* finish -- standardize remaining parameters *)
wenzelm@2957
    80
wenzelm@39294
    81
fun finish ctxt tye (Ts, ts) =
wenzelm@39294
    82
  let
wenzelm@39294
    83
    val used =
wenzelm@39294
    84
      (fold o fold_types) (add_names tye) ts (fold (add_names tye) Ts (Variable.names_of ctxt));
wenzelm@39294
    85
    val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts []));
wenzelm@43329
    86
    val names = Name.invent used ("?" ^ Name.aT) (length parms);
wenzelm@39294
    87
    val tab = Vartab.make (parms ~~ names);
wenzelm@2957
    88
wenzelm@39294
    89
    fun finish_typ T =
wenzelm@39294
    90
      (case deref tye T of
wenzelm@39294
    91
        Type (a, Ts) => Type (a, map finish_typ Ts)
wenzelm@39294
    92
      | U as TFree _ => U
wenzelm@39294
    93
      | U as TVar (xi, S) =>
wenzelm@39294
    94
          (case Vartab.lookup tab xi of
wenzelm@39294
    95
            NONE => U
wenzelm@39295
    96
          | SOME a => TVar ((a, 0), S)));
wenzelm@39294
    97
  in (map finish_typ Ts, map (Type.strip_constraints o Term.map_types finish_typ) ts) end;
wenzelm@2957
    98
wenzelm@2957
    99
wenzelm@39296
   100
(* fixate -- introduce fresh type variables *)
wenzelm@39296
   101
wenzelm@39296
   102
fun fixate ctxt ts =
wenzelm@39296
   103
  let
wenzelm@39296
   104
    fun subst_param (xi, S) (inst, used) =
wenzelm@39296
   105
      if is_param xi then
wenzelm@39296
   106
        let
wenzelm@43329
   107
          val [a] = Name.invent used Name.aT 1;
wenzelm@39296
   108
          val used' = Name.declare a used;
wenzelm@39296
   109
        in (((xi, S), TFree (a, S)) :: inst, used') end
wenzelm@39296
   110
      else (inst, used);
wenzelm@39296
   111
    val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
wenzelm@39296
   112
    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
wenzelm@39296
   113
  in (map o map_types) (Term_Subst.instantiateT inst) ts end;
wenzelm@39296
   114
wenzelm@2957
   115
end;