src/Pure/type_infer.ML
author wenzelm
Mon Sep 13 13:20:18 2010 +0200 (2010-09-13)
changeset 39296 e275d581a218
parent 39295 6e8b0672c6a2
child 40286 b928e3960446
permissions -rw-r--r--
tuned signature;
tuned comments;
     1 (*  Title:      Pure/type_infer.ML
     2     Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     3 
     4 Representation of type-inference problems.  Simple type inference.
     5 *)
     6 
     7 signature TYPE_INFER =
     8 sig
     9   val is_param: indexname -> bool
    10   val is_paramT: typ -> bool
    11   val param: int -> string * sort -> typ
    12   val anyT: sort -> typ
    13   val paramify_vars: typ -> typ
    14   val paramify_dummies: typ -> int -> typ * int
    15   val deref: typ Vartab.table -> typ -> typ
    16   val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list
    17   val fixate: Proof.context -> term list -> term list
    18   val prepare: Proof.context -> (string -> typ option) -> (string * int -> typ option) ->
    19     term list -> int * term list
    20   val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) ->
    21     term list -> term list
    22 end;
    23 
    24 structure Type_Infer: TYPE_INFER =
    25 struct
    26 
    27 (** type parameters and constraints **)
    28 
    29 (* type inference parameters -- may get instantiated *)
    30 
    31 fun is_param (x, _: int) = String.isPrefix "?" x;
    32 
    33 fun is_paramT (TVar (xi, _)) = is_param xi
    34   | is_paramT _ = false;
    35 
    36 fun param i (x, S) = TVar (("?" ^ x, i), S);
    37 
    38 fun mk_param i S = TVar (("?'a", i), S);
    39 
    40 
    41 (* pre-stage parameters *)
    42 
    43 fun anyT S = TFree ("'_dummy_", S);
    44 
    45 val paramify_vars =
    46   Same.commit
    47     (Term_Subst.map_atypsT_same
    48       (fn TVar ((x, i), S) => (param i (x, S)) | _ => raise Same.SAME));
    49 
    50 val paramify_dummies =
    51   let
    52     fun dummy S maxidx = (param (maxidx + 1) ("'dummy", S), maxidx + 1);
    53 
    54     fun paramify (TFree ("'_dummy_", S)) maxidx = dummy S maxidx
    55       | paramify (Type ("dummy", _)) maxidx = dummy [] maxidx
    56       | paramify (Type (a, Ts)) maxidx =
    57           let val (Ts', maxidx') = fold_map paramify Ts maxidx
    58           in (Type (a, Ts'), maxidx') end
    59       | paramify T maxidx = (T, maxidx);
    60   in paramify end;
    61 
    62 
    63 
    64 (** prepare types/terms: create inference parameters **)
    65 
    66 (* prepare_typ *)
    67 
    68 fun prepare_typ typ params_idx =
    69   let
    70     val (params', idx) = fold_atyps
    71       (fn TVar (xi as (x, _), S) =>
    72           (fn ps_idx as (ps, idx) =>
    73             if is_param xi andalso not (Vartab.defined ps xi)
    74             then (Vartab.update (xi, mk_param idx S) ps, idx + 1) else ps_idx)
    75         | _ => I) typ params_idx;
    76 
    77     fun prepare (T as Type (a, Ts)) idx =
    78           if T = dummyT then (mk_param idx [], idx + 1)
    79           else
    80             let val (Ts', idx') = fold_map prepare Ts idx
    81             in (Type (a, Ts'), idx') end
    82       | prepare (T as TVar (xi, _)) idx =
    83           (case Vartab.lookup params' xi of
    84             NONE => T
    85           | SOME p => p, idx)
    86       | prepare (TFree ("'_dummy_", S)) idx = (mk_param idx S, idx + 1)
    87       | prepare (T as TFree _) idx = (T, idx);
    88 
    89     val (typ', idx') = prepare typ idx;
    90   in (typ', (params', idx')) end;
    91 
    92 
    93 (* prepare_term *)
    94 
    95 fun prepare_term const_type tm (vparams, params, idx) =
    96   let
    97     fun add_vparm xi (ps_idx as (ps, idx)) =
    98       if not (Vartab.defined ps xi) then
    99         (Vartab.update (xi, mk_param idx []) ps, idx + 1)
   100       else ps_idx;
   101 
   102     val (vparams', idx') = fold_aterms
   103       (fn Var (_, Type ("_polymorphic_", _)) => I
   104         | Var (xi, _) => add_vparm xi
   105         | Free (x, _) => add_vparm (x, ~1)
   106         | _ => I)
   107       tm (vparams, idx);
   108     fun var_param xi = the (Vartab.lookup vparams' xi);
   109 
   110     fun polyT_of T idx = apsnd snd (prepare_typ (paramify_vars T) (Vartab.empty, idx));
   111 
   112     fun constraint T t ps =
   113       if T = dummyT then (t, ps)
   114       else
   115         let val (T', ps') = prepare_typ T ps
   116         in (Type.constraint T' t, ps') end;
   117 
   118     fun prepare (Const ("_type_constraint_", T) $ t) ps_idx =
   119           let
   120             val (T', ps_idx') = prepare_typ T ps_idx;
   121             val (t', ps_idx'') = prepare t ps_idx';
   122           in (Const ("_type_constraint_", T') $ t', ps_idx'') end
   123       | prepare (Const (c, T)) (ps, idx) =
   124           (case const_type c of
   125             SOME U =>
   126               let val (U', idx') = polyT_of U idx
   127               in constraint T (Const (c, U')) (ps, idx') end
   128           | NONE => error ("Undeclared constant: " ^ quote c))
   129       | prepare (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) =
   130           let val (T', idx') = polyT_of T idx
   131           in (Var (xi, T'), (ps, idx')) end
   132       | prepare (Var (xi, T)) ps_idx = constraint T (Var (xi, var_param xi)) ps_idx
   133       | prepare (Free (x, T)) ps_idx = constraint T (Free (x, var_param (x, ~1))) ps_idx
   134       | prepare (Bound i) ps_idx = (Bound i, ps_idx)
   135       | prepare (Abs (x, T, t)) ps_idx =
   136           let
   137             val (T', ps_idx') = prepare_typ T ps_idx;
   138             val (t', ps_idx'') = prepare t ps_idx';
   139           in (Abs (x, T', t'), ps_idx'') end
   140       | prepare (t $ u) ps_idx =
   141           let
   142             val (t', ps_idx') = prepare t ps_idx;
   143             val (u', ps_idx'') = prepare u ps_idx';
   144           in (t' $ u', ps_idx'') end;
   145 
   146     val (tm', (params', idx'')) = prepare tm (params, idx');
   147   in (tm', (vparams', params', idx'')) end;
   148 
   149 
   150 
   151 (** results **)
   152 
   153 (* dereferenced views *)
   154 
   155 fun deref tye (T as TVar (xi, _)) =
   156       (case Vartab.lookup tye xi of
   157         NONE => T
   158       | SOME U => deref tye U)
   159   | deref tye T = T;
   160 
   161 fun add_parms tye T =
   162   (case deref tye T of
   163     Type (_, Ts) => fold (add_parms tye) Ts
   164   | TVar (xi, _) => if is_param xi then insert (op =) xi else I
   165   | _ => I);
   166 
   167 fun add_names tye T =
   168   (case deref tye T of
   169     Type (_, Ts) => fold (add_names tye) Ts
   170   | TFree (x, _) => Name.declare x
   171   | TVar ((x, i), _) => if is_param (x, i) then I else Name.declare x);
   172 
   173 
   174 (* finish -- standardize remaining parameters *)
   175 
   176 fun finish ctxt tye (Ts, ts) =
   177   let
   178     val used =
   179       (fold o fold_types) (add_names tye) ts (fold (add_names tye) Ts (Variable.names_of ctxt));
   180     val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts []));
   181     val names = Name.invents used ("?" ^ Name.aT) (length parms);
   182     val tab = Vartab.make (parms ~~ names);
   183 
   184     fun finish_typ T =
   185       (case deref tye T of
   186         Type (a, Ts) => Type (a, map finish_typ Ts)
   187       | U as TFree _ => U
   188       | U as TVar (xi, S) =>
   189           (case Vartab.lookup tab xi of
   190             NONE => U
   191           | SOME a => TVar ((a, 0), S)));
   192   in (map finish_typ Ts, map (Type.strip_constraints o Term.map_types finish_typ) ts) end;
   193 
   194 
   195 (* fixate -- introduce fresh type variables *)
   196 
   197 fun fixate ctxt ts =
   198   let
   199     fun subst_param (xi, S) (inst, used) =
   200       if is_param xi then
   201         let
   202           val [a] = Name.invents used Name.aT 1;
   203           val used' = Name.declare a used;
   204         in (((xi, S), TFree (a, S)) :: inst, used') end
   205       else (inst, used);
   206     val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
   207     val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
   208   in (map o map_types) (Term_Subst.instantiateT inst) ts end;
   209 
   210 
   211 
   212 (** order-sorted unification of types **)
   213 
   214 exception NO_UNIFIER of string * typ Vartab.table;
   215 
   216 fun unify ctxt pp =
   217   let
   218     val thy = ProofContext.theory_of ctxt;
   219     val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy);
   220 
   221 
   222     (* adjust sorts of parameters *)
   223 
   224     fun not_of_sort x S' S =
   225       "Variable " ^ x ^ "::" ^ Syntax.string_of_sort ctxt S' ^ " not of sort " ^
   226         Syntax.string_of_sort ctxt S;
   227 
   228     fun meet (_, []) tye_idx = tye_idx
   229       | meet (Type (a, Ts), S) (tye_idx as (tye, _)) =
   230           meets (Ts, arity_sorts a S handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx
   231       | meet (TFree (x, S'), S) (tye_idx as (tye, _)) =
   232           if Sign.subsort thy (S', S) then tye_idx
   233           else raise NO_UNIFIER (not_of_sort x S' S, tye)
   234       | meet (TVar (xi, S'), S) (tye_idx as (tye, idx)) =
   235           if Sign.subsort thy (S', S) then tye_idx
   236           else if is_param xi then
   237             (Vartab.update_new (xi, mk_param idx (Sign.inter_sort thy (S', S))) tye, idx + 1)
   238           else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye)
   239     and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) =
   240           meets (Ts, Ss) (meet (deref tye T, S) tye_idx)
   241       | meets _ tye_idx = tye_idx;
   242 
   243 
   244     (* occurs check and assignment *)
   245 
   246     fun occurs_check tye xi (TVar (xi', S)) =
   247           if xi = xi' then raise NO_UNIFIER ("Occurs check!", tye)
   248           else
   249             (case Vartab.lookup tye xi' of
   250               NONE => ()
   251             | SOME T => occurs_check tye xi T)
   252       | occurs_check tye xi (Type (_, Ts)) = List.app (occurs_check tye xi) Ts
   253       | occurs_check _ _ _ = ();
   254 
   255     fun assign xi (T as TVar (xi', _)) S env =
   256           if xi = xi' then env
   257           else env |> meet (T, S) |>> Vartab.update_new (xi, T)
   258       | assign xi T S (env as (tye, _)) =
   259           (occurs_check tye xi T; env |> meet (T, S) |>> Vartab.update_new (xi, T));
   260 
   261 
   262     (* unification *)
   263 
   264     fun show_tycon (a, Ts) =
   265       quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT)));
   266 
   267     fun unif (T1, T2) (env as (tye, _)) =
   268       (case pairself (`is_paramT o deref tye) (T1, T2) of
   269         ((true, TVar (xi, S)), (_, T)) => assign xi T S env
   270       | ((_, T), (true, TVar (xi, S))) => assign xi T S env
   271       | ((_, Type (a, Ts)), (_, Type (b, Us))) =>
   272           if a <> b then
   273             raise NO_UNIFIER
   274               ("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye)
   275           else fold unif (Ts ~~ Us) env
   276       | ((_, T), (_, U)) => if T = U then env else raise NO_UNIFIER ("", tye));
   277 
   278   in unif end;
   279 
   280 
   281 
   282 (** simple type inference **)
   283 
   284 (* infer *)
   285 
   286 fun infer ctxt =
   287   let
   288     val pp = Syntax.pp ctxt;
   289 
   290 
   291     (* errors *)
   292 
   293     fun prep_output tye bs ts Ts =
   294       let
   295         val (Ts_bTs', ts') = finish ctxt tye (Ts @ map snd bs, ts);
   296         val (Ts', Ts'') = chop (length Ts) Ts_bTs';
   297         fun prep t =
   298           let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
   299           in Term.subst_bounds (map Syntax.mark_boundT xs, t) end;
   300       in (map prep ts', Ts') end;
   301 
   302     fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
   303 
   304     fun unif_failed msg =
   305       "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
   306 
   307     fun err_appl msg tye bs t T u U =
   308       let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]
   309       in error (unif_failed msg ^ Type.appl_error pp t' T' u' U' ^ "\n") end;
   310 
   311 
   312     (* main *)
   313 
   314     fun inf _ (Const (_, T)) tye_idx = (T, tye_idx)
   315       | inf _ (Free (_, T)) tye_idx = (T, tye_idx)
   316       | inf _ (Var (_, T)) tye_idx = (T, tye_idx)
   317       | inf bs (Bound i) tye_idx =
   318           (snd (nth bs i handle Subscript => err_loose i), tye_idx)
   319       | inf bs (Abs (x, T, t)) tye_idx =
   320           let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx
   321           in (T --> U, tye_idx') end
   322       | inf bs (t $ u) tye_idx =
   323           let
   324             val (T, tye_idx') = inf bs t tye_idx;
   325             val (U, (tye, idx)) = inf bs u tye_idx';
   326             val V = mk_param idx [];
   327             val tye_idx'' = unify ctxt pp (U --> V, T) (tye, idx + 1)
   328               handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U;
   329           in (V, tye_idx'') end;
   330 
   331   in inf [] end;
   332 
   333 
   334 (* main interfaces *)
   335 
   336 fun prepare ctxt const_type var_type raw_ts =
   337   let
   338     val get_type = the_default dummyT o var_type;
   339     val constrain_vars = Term.map_aterms
   340       (fn Free (x, T) => Type.constraint T (Free (x, get_type (x, ~1)))
   341         | Var (xi, T) => Type.constraint T (Var (xi, get_type xi))
   342         | t => t);
   343 
   344     val ts = burrow_types (Syntax.check_typs ctxt) raw_ts;
   345     val (ts', (_, _, idx)) =
   346       fold_map (prepare_term const_type o constrain_vars) ts
   347       (Vartab.empty, Vartab.empty, 0);
   348   in (idx, ts') end;
   349 
   350 fun infer_types ctxt const_type var_type raw_ts =
   351   let
   352     val (idx, ts) = prepare ctxt const_type var_type raw_ts;
   353     val (tye, _) = fold (snd oo infer ctxt) ts (Vartab.empty, idx);
   354     val (_, ts') = finish ctxt tye ([], ts);
   355   in ts' end;
   356 
   357 end;