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