Type_Infer.preterm: eliminated separate Constraint;
authorwenzelm
Sun Sep 12 22:28:59 2010 +0200 (2010-09-12)
changeset 392926f085332c7d3
parent 39291 4b632bb847a8
child 39293 651e5a3e8cfd
Type_Infer.preterm: eliminated separate Constraint;
src/Pure/type.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type.ML	Sun Sep 12 21:24:23 2010 +0200
     1.2 +++ b/src/Pure/type.ML	Sun Sep 12 22:28:59 2010 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    (*constraints*)
     1.5    val mark_polymorphic: typ -> typ
     1.6    val constraint: typ -> term -> term
     1.7 +  val strip_constraints: term -> term
     1.8    val appl_error: Pretty.pp -> term -> typ -> term -> typ -> string
     1.9    (*type signatures and certified types*)
    1.10    datatype decl =
    1.11 @@ -109,6 +110,11 @@
    1.12    if T = dummyT then t
    1.13    else Const ("_type_constraint_", T --> T) $ t;
    1.14  
    1.15 +fun strip_constraints (Const ("_type_constraint_", _) $ t) = strip_constraints t
    1.16 +  | strip_constraints (t $ u) = strip_constraints t $ strip_constraints u
    1.17 +  | strip_constraints (Abs (x, T, t)) = Abs (x, T, strip_constraints t)
    1.18 +  | strip_constraints a = a;
    1.19 +
    1.20  fun appl_error pp (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U =
    1.21        cat_lines
    1.22         ["Failed to meet type constraint:", "",
     2.1 --- a/src/Pure/type_infer.ML	Sun Sep 12 21:24:23 2010 +0200
     2.2 +++ b/src/Pure/type_infer.ML	Sun Sep 12 22:28:59 2010 +0200
     2.3 @@ -76,8 +76,7 @@
     2.4    PVar of indexname * pretyp |
     2.5    PBound of int |
     2.6    PAbs of string * pretyp * preterm |
     2.7 -  PAppl of preterm * preterm |
     2.8 -  Constraint of preterm * pretyp;
     2.9 +  PAppl of preterm * preterm;
    2.10  
    2.11  
    2.12  (* utils *)
    2.13 @@ -93,8 +92,7 @@
    2.14    | fold_pretyps f (PVar (_, T)) x = f T x
    2.15    | fold_pretyps _ (PBound _) x = x
    2.16    | fold_pretyps f (PAbs (_, T, t)) x = fold_pretyps f t (f T x)
    2.17 -  | fold_pretyps f (PAppl (t, u)) x = fold_pretyps f u (fold_pretyps f t x)
    2.18 -  | fold_pretyps f (Constraint (t, T)) x = f T (fold_pretyps f t x);
    2.19 +  | fold_pretyps f (PAppl (t, u)) x = fold_pretyps f u (fold_pretyps f t x);
    2.20  
    2.21  
    2.22  
    2.23 @@ -150,7 +148,7 @@
    2.24        if T = dummyT then (t, ps)
    2.25        else
    2.26          let val (T', ps') = pretyp_of T ps
    2.27 -        in (Constraint (t, T'), ps') end;
    2.28 +        in (PAppl (PConst ("_type_constraint_", PType ("fun", [T', T'])), t), ps') end;
    2.29  
    2.30      fun pre_of (Const (c, T)) (ps, idx) =
    2.31            (case const_type c of
    2.32 @@ -158,13 +156,16 @@
    2.33                let val (pU, idx') = polyT_of U idx
    2.34                in constraint T (PConst (c, pU)) (ps, idx') end
    2.35            | NONE => error ("Undeclared constant: " ^ quote c))
    2.36 +      | pre_of (Const ("_type_constraint_", T) $ t) ps_idx =
    2.37 +          let
    2.38 +            val (T', ps_idx') = pretyp_of T ps_idx;
    2.39 +            val (t', ps_idx'') = pre_of t ps_idx';
    2.40 +          in (PAppl (PConst ("_type_constraint_", T'), t'), ps_idx'') end
    2.41        | pre_of (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) =
    2.42            let val (pT, idx') = polyT_of T idx
    2.43            in (PVar (xi, pT), (ps, idx')) end
    2.44        | pre_of (Var (xi, T)) ps_idx = constraint T (PVar (xi, var_param xi)) ps_idx
    2.45        | pre_of (Free (x, T)) ps_idx = constraint T (PFree (x, var_param (x, ~1))) ps_idx
    2.46 -      | pre_of (Const ("_type_constraint_", Type ("fun", [T, _])) $ t) ps_idx =
    2.47 -          pre_of t ps_idx |-> constraint T
    2.48        | pre_of (Bound i) ps_idx = (PBound i, ps_idx)
    2.49        | pre_of (Abs (x, T, t)) ps_idx =
    2.50            let
    2.51 @@ -216,7 +217,6 @@
    2.52    | PTVar v => TVar v
    2.53    | Param (i, S) => TVar (f i, S));
    2.54  
    2.55 -(*convert types, drop constraints*)
    2.56  fun simple_term_of tye f (PConst (c, T)) = Const (c, simple_typ_of tye f T)
    2.57    | simple_term_of tye f (PFree (x, T)) = Free (x, simple_typ_of tye f T)
    2.58    | simple_term_of tye f (PVar (xi, T)) = Var (xi, simple_typ_of tye f T)
    2.59 @@ -224,8 +224,7 @@
    2.60    | simple_term_of tye f (PAbs (x, T, t)) =
    2.61        Abs (x, simple_typ_of tye f T, simple_term_of tye f t)
    2.62    | simple_term_of tye f (PAppl (t, u)) =
    2.63 -      simple_term_of tye f t $ simple_term_of tye f u
    2.64 -  | simple_term_of tye f (Constraint (t, _)) = simple_term_of tye f t;
    2.65 +      simple_term_of tye f t $ simple_term_of tye f u;
    2.66  
    2.67  
    2.68  (* typs_terms_of *)
    2.69 @@ -239,7 +238,7 @@
    2.70  
    2.71      val maxidx = Variable.maxidx_of ctxt;
    2.72      fun f i = (the (Inttab.lookup tab i), maxidx + 1);
    2.73 -  in (map (simple_typ_of tye f) Ts, map (simple_term_of tye f) ts) end;
    2.74 +  in (map (simple_typ_of tye f) Ts, map (Type.strip_constraints o simple_term_of tye f) ts) end;
    2.75  
    2.76  
    2.77  
    2.78 @@ -344,12 +343,6 @@
    2.79        let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]
    2.80        in error (unif_failed msg ^ Type.appl_error pp t' T' u' U' ^ "\n") end;
    2.81  
    2.82 -    fun err_constraint msg tye bs t T U =
    2.83 -      let val ([t'], [T', U']) = prep_output tye bs [t] [T, U] in
    2.84 -        error (unif_failed msg ^
    2.85 -          Type.appl_error pp (Const ("_type_constraint_", U' --> U')) (U' --> U') t' T' ^ "\n")
    2.86 -      end;
    2.87 -
    2.88  
    2.89      (* main *)
    2.90  
    2.91 @@ -369,13 +362,7 @@
    2.92              val U_to_V = PType ("fun", [U, V]);
    2.93              val tye_idx'' = unify ctxt pp (U_to_V, T) (tye, idx + 1)
    2.94                handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U;
    2.95 -          in (V, tye_idx'') end
    2.96 -      | inf bs (Constraint (t, U)) tye_idx =
    2.97 -          let val (T, tye_idx') = inf bs t tye_idx in
    2.98 -            (T,
    2.99 -             unify ctxt pp (T, U) tye_idx'
   2.100 -               handle NO_UNIFIER (msg, tye) => err_constraint msg tye bs t T U)
   2.101 -          end;
   2.102 +          in (V, tye_idx'') end;
   2.103  
   2.104    in inf [] end;
   2.105