src/Pure/type_infer.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 64556 851ae0e7b09c
child 69575 f77cc54f6d47
permissions -rw-r--r--
more robust sorted_entries;
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@62958
    19
  val object_logic: bool Config.T
wenzelm@62958
    20
  val fixate: Proof.context -> bool -> 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@2957
    55
wenzelm@2957
    56
wenzelm@39296
    57
(** results **)
wenzelm@2957
    58
wenzelm@39294
    59
(* dereferenced views *)
wenzelm@2957
    60
wenzelm@39294
    61
fun deref tye (T as TVar (xi, _)) =
wenzelm@39294
    62
      (case Vartab.lookup tye xi of
wenzelm@39294
    63
        NONE => T
wenzelm@39294
    64
      | SOME U => deref tye U)
wenzelm@42400
    65
  | deref _ T = T;
wenzelm@39294
    66
wenzelm@39294
    67
fun add_parms tye T =
wenzelm@32146
    68
  (case deref tye T of
wenzelm@39294
    69
    Type (_, Ts) => fold (add_parms tye) Ts
wenzelm@39294
    70
  | TVar (xi, _) => if is_param xi then insert (op =) xi else I
wenzelm@32146
    71
  | _ => I);
wenzelm@2957
    72
wenzelm@39294
    73
fun add_names tye T =
wenzelm@32146
    74
  (case deref tye T of
wenzelm@39294
    75
    Type (_, Ts) => fold (add_names tye) Ts
wenzelm@39294
    76
  | TFree (x, _) => Name.declare x
wenzelm@39294
    77
  | TVar ((x, i), _) => if is_param (x, i) then I else Name.declare x);
wenzelm@2957
    78
wenzelm@2957
    79
wenzelm@39296
    80
(* finish -- standardize remaining parameters *)
wenzelm@2957
    81
wenzelm@39294
    82
fun finish ctxt tye (Ts, ts) =
wenzelm@39294
    83
  let
wenzelm@39294
    84
    val used =
wenzelm@39294
    85
      (fold o fold_types) (add_names tye) ts (fold (add_names tye) Ts (Variable.names_of ctxt));
wenzelm@39294
    86
    val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts []));
wenzelm@43329
    87
    val names = Name.invent used ("?" ^ Name.aT) (length parms);
wenzelm@39294
    88
    val tab = Vartab.make (parms ~~ names);
wenzelm@2957
    89
wenzelm@39294
    90
    fun finish_typ T =
wenzelm@39294
    91
      (case deref tye T of
wenzelm@39294
    92
        Type (a, Ts) => Type (a, map finish_typ Ts)
wenzelm@39294
    93
      | U as TFree _ => U
wenzelm@39294
    94
      | U as TVar (xi, S) =>
wenzelm@39294
    95
          (case Vartab.lookup tab xi of
wenzelm@39294
    96
            NONE => U
wenzelm@39295
    97
          | SOME a => TVar ((a, 0), S)));
wenzelm@39294
    98
  in (map finish_typ Ts, map (Type.strip_constraints o Term.map_types finish_typ) ts) end;
wenzelm@2957
    99
wenzelm@2957
   100
wenzelm@39296
   101
(* fixate -- introduce fresh type variables *)
wenzelm@39296
   102
wenzelm@62958
   103
val object_logic =
wenzelm@64556
   104
  Config.bool (Config.declare ("Type_Infer.object_logic", \<^here>) (K (Config.Bool true)));
wenzelm@62958
   105
wenzelm@62958
   106
fun fixate ctxt pattern ts =
wenzelm@39296
   107
  let
wenzelm@62958
   108
    val base_sort = Object_Logic.get_base_sort ctxt;
wenzelm@62958
   109
    val improve_sort =
wenzelm@62958
   110
      if is_some base_sort andalso not pattern andalso Config.get ctxt object_logic
wenzelm@62958
   111
      then fn [] => the base_sort | S => S else I;
wenzelm@62958
   112
wenzelm@39296
   113
    fun subst_param (xi, S) (inst, used) =
wenzelm@39296
   114
      if is_param xi then
wenzelm@39296
   115
        let
wenzelm@43329
   116
          val [a] = Name.invent used Name.aT 1;
wenzelm@39296
   117
          val used' = Name.declare a used;
wenzelm@62958
   118
        in (((xi, S), TFree (a, improve_sort S)) :: inst, used') end
wenzelm@39296
   119
      else (inst, used);
wenzelm@39296
   120
    val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
wenzelm@39296
   121
    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
wenzelm@39296
   122
  in (map o map_types) (Term_Subst.instantiateT inst) ts end;
wenzelm@39296
   123
wenzelm@2957
   124
end;