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;
     1 (*  Title:      Pure/type_infer.ML
     2     Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     3 
     4 Basic representation of type-inference problems.
     5 *)
     6 
     7 signature TYPE_INFER =
     8 sig
     9   val is_param: indexname -> bool
    10   val is_paramT: typ -> bool
    11   val param_maxidx: term -> int -> int
    12   val param_maxidx_of: term list -> int
    13   val param: int -> string * sort -> typ
    14   val mk_param: int -> sort -> typ
    15   val anyT: sort -> typ
    16   val paramify_vars: typ -> typ
    17   val deref: typ Vartab.table -> typ -> typ
    18   val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list
    19   val object_logic: bool Config.T
    20   val fixate: Proof.context -> bool -> term list -> term list
    21 end;
    22 
    23 structure Type_Infer: TYPE_INFER =
    24 struct
    25 
    26 (** type parameters and constraints **)
    27 
    28 (* type inference parameters -- may get instantiated *)
    29 
    30 fun is_param (x, _: int) = String.isPrefix "?" x;
    31 
    32 fun is_paramT (TVar (xi, _)) = is_param xi
    33   | is_paramT _ = false;
    34 
    35 val param_maxidx =
    36   (Term.fold_types o Term.fold_atyps)
    37     (fn (TVar (xi as (_, i), _)) => if is_param xi then Integer.max i else I | _ => I);
    38 
    39 fun param_maxidx_of ts = fold param_maxidx ts ~1;
    40 
    41 fun param i (x, S) = TVar (("?" ^ x, i), S);
    42 
    43 fun mk_param i S = TVar (("?'a", i), S);
    44 
    45 
    46 (* pre-stage parameters *)
    47 
    48 fun anyT S = TFree ("'_dummy_", S);
    49 
    50 val paramify_vars =
    51   Same.commit
    52     (Term_Subst.map_atypsT_same
    53       (fn TVar ((x, i), S) => (param i (x, S)) | _ => raise Same.SAME));
    54 
    55 
    56 
    57 (** results **)
    58 
    59 (* dereferenced views *)
    60 
    61 fun deref tye (T as TVar (xi, _)) =
    62       (case Vartab.lookup tye xi of
    63         NONE => T
    64       | SOME U => deref tye U)
    65   | deref _ T = T;
    66 
    67 fun add_parms tye T =
    68   (case deref tye T of
    69     Type (_, Ts) => fold (add_parms tye) Ts
    70   | TVar (xi, _) => if is_param xi then insert (op =) xi else I
    71   | _ => I);
    72 
    73 fun add_names tye T =
    74   (case deref tye T of
    75     Type (_, Ts) => fold (add_names tye) Ts
    76   | TFree (x, _) => Name.declare x
    77   | TVar ((x, i), _) => if is_param (x, i) then I else Name.declare x);
    78 
    79 
    80 (* finish -- standardize remaining parameters *)
    81 
    82 fun finish ctxt tye (Ts, ts) =
    83   let
    84     val used =
    85       (fold o fold_types) (add_names tye) ts (fold (add_names tye) Ts (Variable.names_of ctxt));
    86     val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts []));
    87     val names = Name.invent used ("?" ^ Name.aT) (length parms);
    88     val tab = Vartab.make (parms ~~ names);
    89 
    90     fun finish_typ T =
    91       (case deref tye T of
    92         Type (a, Ts) => Type (a, map finish_typ Ts)
    93       | U as TFree _ => U
    94       | U as TVar (xi, S) =>
    95           (case Vartab.lookup tab xi of
    96             NONE => U
    97           | SOME a => TVar ((a, 0), S)));
    98   in (map finish_typ Ts, map (Type.strip_constraints o Term.map_types finish_typ) ts) end;
    99 
   100 
   101 (* fixate -- introduce fresh type variables *)
   102 
   103 val object_logic =
   104   Config.bool (Config.declare ("Type_Infer.object_logic", \<^here>) (K (Config.Bool true)));
   105 
   106 fun fixate ctxt pattern ts =
   107   let
   108     val base_sort = Object_Logic.get_base_sort ctxt;
   109     val improve_sort =
   110       if is_some base_sort andalso not pattern andalso Config.get ctxt object_logic
   111       then fn [] => the base_sort | S => S else I;
   112 
   113     fun subst_param (xi, S) (inst, used) =
   114       if is_param xi then
   115         let
   116           val [a] = Name.invent used Name.aT 1;
   117           val used' = Name.declare a used;
   118         in (((xi, S), TFree (a, improve_sort S)) :: inst, used') end
   119       else (inst, used);
   120     val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
   121     val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
   122   in (map o map_types) (Term_Subst.instantiateT inst) ts end;
   123 
   124 end;