src/Pure/type_infer.ML
changeset 42405 13ecdb3057d8
parent 42400 26c8c9cabb24
child 43329 84472e198515
     1.1 --- a/src/Pure/type_infer.ML	Tue Apr 19 16:13:04 2011 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Tue Apr 19 20:47:02 2011 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/type_infer.ML
     1.5      Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Representation of type-inference problems.  Simple type inference.
     1.8 +Basic representation of type-inference problems.
     1.9  *)
    1.10  
    1.11  signature TYPE_INFER =
    1.12 @@ -18,10 +18,6 @@
    1.13    val deref: typ Vartab.table -> typ -> typ
    1.14    val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list
    1.15    val fixate: Proof.context -> term list -> term list
    1.16 -  val prepare: Proof.context -> (string -> typ option) -> (string * int -> typ option) ->
    1.17 -    term list -> int * term list
    1.18 -  val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) ->
    1.19 -    term list -> term list
    1.20  end;
    1.21  
    1.22  structure Type_Infer: TYPE_INFER =
    1.23 @@ -70,96 +66,6 @@
    1.24  
    1.25  
    1.26  
    1.27 -(** prepare types/terms: create inference parameters **)
    1.28 -
    1.29 -(* prepare_typ *)
    1.30 -
    1.31 -fun prepare_typ typ params_idx =
    1.32 -  let
    1.33 -    val (params', idx) = fold_atyps
    1.34 -      (fn TVar (xi, S) =>
    1.35 -          (fn ps_idx as (ps, idx) =>
    1.36 -            if is_param xi andalso not (Vartab.defined ps xi)
    1.37 -            then (Vartab.update (xi, mk_param idx S) ps, idx + 1) else ps_idx)
    1.38 -        | _ => I) typ params_idx;
    1.39 -
    1.40 -    fun prepare (T as Type (a, Ts)) idx =
    1.41 -          if T = dummyT then (mk_param idx [], idx + 1)
    1.42 -          else
    1.43 -            let val (Ts', idx') = fold_map prepare Ts idx
    1.44 -            in (Type (a, Ts'), idx') end
    1.45 -      | prepare (T as TVar (xi, _)) idx =
    1.46 -          (case Vartab.lookup params' xi of
    1.47 -            NONE => T
    1.48 -          | SOME p => p, idx)
    1.49 -      | prepare (TFree ("'_dummy_", S)) idx = (mk_param idx S, idx + 1)
    1.50 -      | prepare (T as TFree _) idx = (T, idx);
    1.51 -
    1.52 -    val (typ', idx') = prepare typ idx;
    1.53 -  in (typ', (params', idx')) end;
    1.54 -
    1.55 -
    1.56 -(* prepare_term *)
    1.57 -
    1.58 -fun prepare_term ctxt const_type tm (vparams, params, idx) =
    1.59 -  let
    1.60 -    fun add_vparm xi (ps_idx as (ps, idx)) =
    1.61 -      if not (Vartab.defined ps xi) then
    1.62 -        (Vartab.update (xi, mk_param idx []) ps, idx + 1)
    1.63 -      else ps_idx;
    1.64 -
    1.65 -    val (vparams', idx') = fold_aterms
    1.66 -      (fn Var (_, Type ("_polymorphic_", _)) => I
    1.67 -        | Var (xi, _) => add_vparm xi
    1.68 -        | Free (x, _) => add_vparm (x, ~1)
    1.69 -        | _ => I)
    1.70 -      tm (vparams, idx);
    1.71 -    fun var_param xi = the (Vartab.lookup vparams' xi);
    1.72 -
    1.73 -    fun polyT_of T idx = apsnd snd (prepare_typ (paramify_vars T) (Vartab.empty, idx));
    1.74 -
    1.75 -    fun constraint T t ps =
    1.76 -      if T = dummyT then (t, ps)
    1.77 -      else
    1.78 -        let val (T', ps') = prepare_typ T ps
    1.79 -        in (Type.constraint T' t, ps') end;
    1.80 -
    1.81 -    fun prepare (Const ("_type_constraint_", T) $ t) ps_idx =
    1.82 -          let
    1.83 -            fun err () =
    1.84 -              error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T);
    1.85 -            val A = (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ());
    1.86 -            val (A', ps_idx') = prepare_typ A ps_idx;
    1.87 -            val (t', ps_idx'') = prepare t ps_idx';
    1.88 -          in (Const ("_type_constraint_", A' --> A') $ t', ps_idx'') end
    1.89 -      | prepare (Const (c, T)) (ps, idx) =
    1.90 -          (case const_type c of
    1.91 -            SOME U =>
    1.92 -              let val (U', idx') = polyT_of U idx
    1.93 -              in constraint T (Const (c, U')) (ps, idx') end
    1.94 -          | NONE => error ("Undeclared constant: " ^ quote c))
    1.95 -      | prepare (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) =
    1.96 -          let val (T', idx') = polyT_of T idx
    1.97 -          in (Var (xi, T'), (ps, idx')) end
    1.98 -      | prepare (Var (xi, T)) ps_idx = constraint T (Var (xi, var_param xi)) ps_idx
    1.99 -      | prepare (Free (x, T)) ps_idx = constraint T (Free (x, var_param (x, ~1))) ps_idx
   1.100 -      | prepare (Bound i) ps_idx = (Bound i, ps_idx)
   1.101 -      | prepare (Abs (x, T, t)) ps_idx =
   1.102 -          let
   1.103 -            val (T', ps_idx') = prepare_typ T ps_idx;
   1.104 -            val (t', ps_idx'') = prepare t ps_idx';
   1.105 -          in (Abs (x, T', t'), ps_idx'') end
   1.106 -      | prepare (t $ u) ps_idx =
   1.107 -          let
   1.108 -            val (t', ps_idx') = prepare t ps_idx;
   1.109 -            val (u', ps_idx'') = prepare u ps_idx';
   1.110 -          in (t' $ u', ps_idx'') end;
   1.111 -
   1.112 -    val (tm', (params', idx'')) = prepare tm (params, idx');
   1.113 -  in (tm', (vparams', params', idx'')) end;
   1.114 -
   1.115 -
   1.116 -
   1.117  (** results **)
   1.118  
   1.119  (* dereferenced views *)
   1.120 @@ -219,149 +125,4 @@
   1.121      val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
   1.122    in (map o map_types) (Term_Subst.instantiateT inst) ts end;
   1.123  
   1.124 -
   1.125 -
   1.126 -(** order-sorted unification of types **)
   1.127 -
   1.128 -exception NO_UNIFIER of string * typ Vartab.table;
   1.129 -
   1.130 -fun unify ctxt =
   1.131 -  let
   1.132 -    val thy = Proof_Context.theory_of ctxt;
   1.133 -    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
   1.134 -
   1.135 -
   1.136 -    (* adjust sorts of parameters *)
   1.137 -
   1.138 -    fun not_of_sort x S' S =
   1.139 -      "Variable " ^ x ^ "::" ^ Syntax.string_of_sort ctxt S' ^ " not of sort " ^
   1.140 -        Syntax.string_of_sort ctxt S;
   1.141 -
   1.142 -    fun meet (_, []) tye_idx = tye_idx
   1.143 -      | meet (Type (a, Ts), S) (tye_idx as (tye, _)) =
   1.144 -          meets (Ts, arity_sorts a S handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx
   1.145 -      | meet (TFree (x, S'), S) (tye_idx as (tye, _)) =
   1.146 -          if Sign.subsort thy (S', S) then tye_idx
   1.147 -          else raise NO_UNIFIER (not_of_sort x S' S, tye)
   1.148 -      | meet (TVar (xi, S'), S) (tye_idx as (tye, idx)) =
   1.149 -          if Sign.subsort thy (S', S) then tye_idx
   1.150 -          else if is_param xi then
   1.151 -            (Vartab.update_new (xi, mk_param idx (Sign.inter_sort thy (S', S))) tye, idx + 1)
   1.152 -          else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye)
   1.153 -    and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) =
   1.154 -          meets (Ts, Ss) (meet (deref tye T, S) tye_idx)
   1.155 -      | meets _ tye_idx = tye_idx;
   1.156 -
   1.157 -
   1.158 -    (* occurs check and assignment *)
   1.159 -
   1.160 -    fun occurs_check tye xi (TVar (xi', _)) =
   1.161 -          if xi = xi' then raise NO_UNIFIER ("Occurs check!", tye)
   1.162 -          else
   1.163 -            (case Vartab.lookup tye xi' of
   1.164 -              NONE => ()
   1.165 -            | SOME T => occurs_check tye xi T)
   1.166 -      | occurs_check tye xi (Type (_, Ts)) = List.app (occurs_check tye xi) Ts
   1.167 -      | occurs_check _ _ _ = ();
   1.168 -
   1.169 -    fun assign xi (T as TVar (xi', _)) S env =
   1.170 -          if xi = xi' then env
   1.171 -          else env |> meet (T, S) |>> Vartab.update_new (xi, T)
   1.172 -      | assign xi T S (env as (tye, _)) =
   1.173 -          (occurs_check tye xi T; env |> meet (T, S) |>> Vartab.update_new (xi, T));
   1.174 -
   1.175 -
   1.176 -    (* unification *)
   1.177 -
   1.178 -    fun show_tycon (a, Ts) =
   1.179 -      quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT)));
   1.180 -
   1.181 -    fun unif (T1, T2) (env as (tye, _)) =
   1.182 -      (case pairself (`is_paramT o deref tye) (T1, T2) of
   1.183 -        ((true, TVar (xi, S)), (_, T)) => assign xi T S env
   1.184 -      | ((_, T), (true, TVar (xi, S))) => assign xi T S env
   1.185 -      | ((_, Type (a, Ts)), (_, Type (b, Us))) =>
   1.186 -          if a <> b then
   1.187 -            raise NO_UNIFIER
   1.188 -              ("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye)
   1.189 -          else fold unif (Ts ~~ Us) env
   1.190 -      | ((_, T), (_, U)) => if T = U then env else raise NO_UNIFIER ("", tye));
   1.191 -
   1.192 -  in unif end;
   1.193 -
   1.194 -
   1.195 -
   1.196 -(** simple type inference **)
   1.197 -
   1.198 -(* infer *)
   1.199 -
   1.200 -fun infer ctxt =
   1.201 -  let
   1.202 -    (* errors *)
   1.203 -
   1.204 -    fun prep_output tye bs ts Ts =
   1.205 -      let
   1.206 -        val (Ts_bTs', ts') = finish ctxt tye (Ts @ map snd bs, ts);
   1.207 -        val (Ts', Ts'') = chop (length Ts) Ts_bTs';
   1.208 -        fun prep t =
   1.209 -          let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
   1.210 -          in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end;
   1.211 -      in (map prep ts', Ts') end;
   1.212 -
   1.213 -    fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
   1.214 -
   1.215 -    fun unif_failed msg =
   1.216 -      "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
   1.217 -
   1.218 -    fun err_appl msg tye bs t T u U =
   1.219 -      let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]
   1.220 -      in error (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n") end;
   1.221 -
   1.222 -
   1.223 -    (* main *)
   1.224 -
   1.225 -    fun inf _ (Const (_, T)) tye_idx = (T, tye_idx)
   1.226 -      | inf _ (Free (_, T)) tye_idx = (T, tye_idx)
   1.227 -      | inf _ (Var (_, T)) tye_idx = (T, tye_idx)
   1.228 -      | inf bs (Bound i) tye_idx =
   1.229 -          (snd (nth bs i handle Subscript => err_loose i), tye_idx)
   1.230 -      | inf bs (Abs (x, T, t)) tye_idx =
   1.231 -          let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx
   1.232 -          in (T --> U, tye_idx') end
   1.233 -      | inf bs (t $ u) tye_idx =
   1.234 -          let
   1.235 -            val (T, tye_idx') = inf bs t tye_idx;
   1.236 -            val (U, (tye, idx)) = inf bs u tye_idx';
   1.237 -            val V = mk_param idx [];
   1.238 -            val tye_idx'' = unify ctxt (U --> V, T) (tye, idx + 1)
   1.239 -              handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U;
   1.240 -          in (V, tye_idx'') end;
   1.241 -
   1.242 -  in inf [] end;
   1.243 -
   1.244 -
   1.245 -(* main interfaces *)
   1.246 -
   1.247 -fun prepare ctxt const_type var_type raw_ts =
   1.248 -  let
   1.249 -    val get_type = the_default dummyT o var_type;
   1.250 -    val constrain_vars = Term.map_aterms
   1.251 -      (fn Free (x, T) => Type.constraint T (Free (x, get_type (x, ~1)))
   1.252 -        | Var (xi, T) => Type.constraint T (Var (xi, get_type xi))
   1.253 -        | t => t);
   1.254 -
   1.255 -    val ts = burrow_types (Syntax.check_typs ctxt) raw_ts;
   1.256 -    val idx = param_maxidx_of ts + 1;
   1.257 -    val (ts', (_, _, idx')) =
   1.258 -      fold_map (prepare_term ctxt const_type o constrain_vars) ts
   1.259 -        (Vartab.empty, Vartab.empty, idx);
   1.260 -  in (idx', ts') end;
   1.261 -
   1.262 -fun infer_types ctxt const_type var_type raw_ts =
   1.263 -  let
   1.264 -    val (idx, ts) = prepare ctxt const_type var_type raw_ts;
   1.265 -    val (tye, _) = fold (snd oo infer ctxt) ts (Vartab.empty, idx);
   1.266 -    val (_, ts') = finish ctxt tye ([], ts);
   1.267 -  in ts' end;
   1.268 -
   1.269  end;