src/Pure/type_infer.ML
author wenzelm
Sun Nov 11 20:31:46 2012 +0100 (2012-11-11)
changeset 50081 9b92ee8dec98
parent 43329 84472e198515
child 53672 df8068269e90
permissions -rw-r--r--
tuned;
     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 paramify_dummies: typ -> int -> typ * int
    18   val deref: typ Vartab.table -> typ -> typ
    19   val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list
    20   val fixate: Proof.context -> 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 val paramify_dummies =
    56   let
    57     fun dummy S maxidx = (param (maxidx + 1) ("'dummy", S), maxidx + 1);
    58 
    59     fun paramify (TFree ("'_dummy_", S)) maxidx = dummy S maxidx
    60       | paramify (Type ("dummy", _)) maxidx = dummy [] maxidx
    61       | paramify (Type (a, Ts)) maxidx =
    62           let val (Ts', maxidx') = fold_map paramify Ts maxidx
    63           in (Type (a, Ts'), maxidx') end
    64       | paramify T maxidx = (T, maxidx);
    65   in paramify end;
    66 
    67 
    68 
    69 (** results **)
    70 
    71 (* dereferenced views *)
    72 
    73 fun deref tye (T as TVar (xi, _)) =
    74       (case Vartab.lookup tye xi of
    75         NONE => T
    76       | SOME U => deref tye U)
    77   | deref _ T = T;
    78 
    79 fun add_parms tye T =
    80   (case deref tye T of
    81     Type (_, Ts) => fold (add_parms tye) Ts
    82   | TVar (xi, _) => if is_param xi then insert (op =) xi else I
    83   | _ => I);
    84 
    85 fun add_names tye T =
    86   (case deref tye T of
    87     Type (_, Ts) => fold (add_names tye) Ts
    88   | TFree (x, _) => Name.declare x
    89   | TVar ((x, i), _) => if is_param (x, i) then I else Name.declare x);
    90 
    91 
    92 (* finish -- standardize remaining parameters *)
    93 
    94 fun finish ctxt tye (Ts, ts) =
    95   let
    96     val used =
    97       (fold o fold_types) (add_names tye) ts (fold (add_names tye) Ts (Variable.names_of ctxt));
    98     val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts []));
    99     val names = Name.invent used ("?" ^ Name.aT) (length parms);
   100     val tab = Vartab.make (parms ~~ names);
   101 
   102     fun finish_typ T =
   103       (case deref tye T of
   104         Type (a, Ts) => Type (a, map finish_typ Ts)
   105       | U as TFree _ => U
   106       | U as TVar (xi, S) =>
   107           (case Vartab.lookup tab xi of
   108             NONE => U
   109           | SOME a => TVar ((a, 0), S)));
   110   in (map finish_typ Ts, map (Type.strip_constraints o Term.map_types finish_typ) ts) end;
   111 
   112 
   113 (* fixate -- introduce fresh type variables *)
   114 
   115 fun fixate ctxt ts =
   116   let
   117     fun subst_param (xi, S) (inst, used) =
   118       if is_param xi then
   119         let
   120           val [a] = Name.invent used Name.aT 1;
   121           val used' = Name.declare a used;
   122         in (((xi, S), TFree (a, S)) :: inst, used') end
   123       else (inst, used);
   124     val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
   125     val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
   126   in (map o map_types) (Term_Subst.instantiateT inst) ts end;
   127 
   128 end;