support polymorphic Vars;
authorwenzelm
Thu Mar 30 14:20:42 2000 +0200 (2000-03-30)
changeset 861149166d549426
parent 8610 f0f7600b2605
child 8612 e8ef58d6d6eb
support polymorphic Vars;
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Thu Mar 30 14:20:13 2000 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Thu Mar 30 14:20:42 2000 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  sig
     1.5    val anyT: sort -> typ
     1.6    val logicT: typ
     1.7 +  val polymorphicT: typ -> typ
     1.8    val infer_types: (term -> Pretty.T) -> (typ -> Pretty.T)
     1.9      -> (string -> typ option) -> Sorts.classrel -> Sorts.arities
    1.10      -> string list -> bool -> (indexname -> bool) -> term list -> typ list
    1.11 @@ -99,6 +100,9 @@
    1.12  fun anyT S = TFree ("'_dummy_", S);
    1.13  val logicT = anyT logicS;
    1.14  
    1.15 +(*indicate polymorphic Vars*)
    1.16 +fun polymorphicT T = Type ("_polymorphic_", [T]);
    1.17 +
    1.18  fun pretyp_of is_param (params, typ) =
    1.19    let
    1.20      fun add_parms (ps, TVar (xi as (x, _), S)) =
    1.21 @@ -132,7 +136,8 @@
    1.22          (xi, mk_param []) :: ps
    1.23        else ps;
    1.24  
    1.25 -    fun add_vparms (ps, Var (xi, _)) = add_vparm (ps, xi)
    1.26 +    fun add_vparms (ps, Var (xi, Type ("_polymorphic_", _))) = ps
    1.27 +      | add_vparms (ps, Var (xi, _)) = add_vparm (ps, xi)
    1.28        | add_vparms (ps, Free (x, _)) = add_vparm (ps, (x, ~1))
    1.29        | add_vparms (ps, Abs (_, _, t)) = add_vparms (ps, t)
    1.30        | add_vparms (ps, t $ u) = add_vparms (add_vparms (ps, t), u)
    1.31 @@ -154,8 +159,10 @@
    1.32            (case const_type c of
    1.33              Some U => constrain (ps, PConst (c, snd (pretyp_of (K true) ([], U)))) T
    1.34            | None => raise TYPE ("No such constant: " ^ quote c, [], []))
    1.35 +      | pre_of (ps, Var (xi, Type ("_polymorphic_", [T]))) =
    1.36 +          (ps, PVar (xi, snd (pretyp_of (K true) ([], T))))
    1.37 +      | pre_of (ps, Var (xi, T)) = constrain (ps, PVar (xi, var_param xi)) T
    1.38        | pre_of (ps, Free (x, T)) = constrain (ps, PFree (x, var_param (x, ~1))) T
    1.39 -      | pre_of (ps, Var (xi, T)) = constrain (ps, PVar (xi, var_param xi)) T
    1.40        | pre_of (ps, Const ("_type_constraint_", T) $ t) = constrain (pre_of (ps, t)) T
    1.41        | pre_of (ps, Bound i) = (ps, PBound i)
    1.42        | pre_of (ps, Abs (x, T, t)) =
    1.43 @@ -169,11 +176,8 @@
    1.44              val (ps'', u') = pre_of (ps', u);
    1.45            in (ps'', PAppl (t', u')) end;
    1.46  
    1.47 -
    1.48      val (params', tm') = pre_of (params, tm);
    1.49 -  in
    1.50 -    ((vparams', params'), tm')
    1.51 -  end;
    1.52 +  in ((vparams', params'), tm') end;
    1.53  
    1.54  fun preterms_of const_type is_param = foldl_map (preterm_of const_type is_param);
    1.55