support for dummy variables (anyT, logicT);
authorwenzelm
Wed Jan 05 11:37:44 2000 +0100 (2000-01-05)
changeset 80874187ef29d826
parent 8086 78e254305ae6
child 8088 6ae943d080de
support for dummy variables (anyT, logicT);
improved error msg: meet *before* assign;
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Wed Jan 05 11:35:18 2000 +0100
     1.2 +++ b/src/Pure/type_infer.ML	Wed Jan 05 11:37:44 2000 +0100
     1.3 @@ -7,6 +7,8 @@
     1.4  
     1.5  signature TYPE_INFER =
     1.6  sig
     1.7 +  val anyT: sort -> typ
     1.8 +  val logicT: typ
     1.9    val infer_types: (term -> Pretty.T) -> (typ -> Pretty.T)
    1.10      -> (string -> typ option) -> Sorts.classrel -> Sorts.arities
    1.11      -> string list -> bool -> (indexname -> bool) -> term list -> typ list
    1.12 @@ -28,15 +30,16 @@
    1.13        A very complicated structure produced by the syntax module's
    1.14        read functions.  Encodes types and sorts as terms; may contain
    1.15        explicit constraints and partial typing information (where
    1.16 -      dummyT serves as wildcard).
    1.17 +      dummies serve as wildcards).
    1.18  
    1.19        Parse trees are INTERNAL! Users should never encounter them,
    1.20        except in parse / print translation functions.
    1.21  
    1.22      raw terms (type term):
    1.23        Provide the user interface to type inferences.  They may contain
    1.24 -      partial type information (dummyT is wildcard) or explicit type
    1.25 -      constraints (introduced via constrain: term -> typ -> term).
    1.26 +      partial type information (dummies are wildcards) or explicit
    1.27 +      type constraints (introduced via constrain: term -> typ ->
    1.28 +      term).
    1.29  
    1.30        The type inference function also lets users specify a certain
    1.31        subset of TVars to be treated as non-rigid inference parameters.
    1.32 @@ -93,6 +96,9 @@
    1.33  
    1.34  (* pretyp(s)_of *)
    1.35  
    1.36 +fun anyT S = TFree ("'_dummy_", S);
    1.37 +val logicT = anyT logicS;
    1.38 +
    1.39  fun pretyp_of is_param (params, typ) =
    1.40    let
    1.41      fun add_parms (ps, TVar (xi as (x, _), S)) =
    1.42 @@ -107,6 +113,7 @@
    1.43            (case assoc (params', xi) of
    1.44              None => PTVar v
    1.45            | Some p => p)
    1.46 +      | pre_of (TFree ("'_dummy_", S)) = mk_param S
    1.47        | pre_of (TFree v) = PTFree v
    1.48        | pre_of (T as Type (a, Ts)) =
    1.49            if T = dummyT then mk_param []
    1.50 @@ -140,9 +147,8 @@
    1.51      fun constrain (ps, t) T =
    1.52        if T = dummyT then (ps, t)
    1.53        else
    1.54 -        let val (ps', T') = preT_of (ps, T) in
    1.55 -          (ps', Constraint (t, T'))
    1.56 -        end;
    1.57 +        let val (ps', T') = preT_of (ps, T)
    1.58 +        in (ps', Constraint (t, T')) end;
    1.59  
    1.60      fun pre_of (ps, Const (c, T)) =
    1.61            (case const_type c of
    1.62 @@ -277,8 +283,8 @@
    1.63      fun assign r T S =
    1.64        (case deref T of
    1.65          T' as Link (r' as ref (Param _)) =>
    1.66 -          if r = r' then () else (r := T'; meet (T', S))
    1.67 -      | T' => (occurs_check r T'; r := T'; meet (T', S)));
    1.68 +          if r = r' then () else (meet (T', S); r := T')
    1.69 +      | T' => (occurs_check r T'; meet (T', S); r := T'));
    1.70  
    1.71  
    1.72      (* unification *)
    1.73 @@ -300,15 +306,14 @@
    1.74  (** type inference **)
    1.75  
    1.76  fun appl_error prt prT why t T u U =
    1.77 -  ["Type error in application: " ^ why,
    1.78 -   "",
    1.79 -   Pretty.string_of
    1.80 -    (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, prt t,
    1.81 -                   Pretty.str " ::", Pretty.brk 1, prT T]),
    1.82 -   Pretty.string_of
    1.83 -     (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, prt u,
    1.84 -                    Pretty.str " ::", Pretty.brk 1, prT U]),
    1.85 -   ""];
    1.86 + ["Type error in application: " ^ why,
    1.87 +  "",
    1.88 +  Pretty.string_of (Pretty.block
    1.89 +    [Pretty.str "Operator:", Pretty.brk 2, prt t, Pretty.str " ::", Pretty.brk 1, prT T]),
    1.90 +  Pretty.string_of (Pretty.block
    1.91 +    [Pretty.str "Operand:", Pretty.brk 3, prt u, Pretty.str " ::", Pretty.brk 1, prT U]),
    1.92 +  ""];
    1.93 +
    1.94  
    1.95  (* infer *)                                     (*DESTRUCTIVE*)
    1.96