src/Pure/type_infer.ML
author wenzelm
Mon, 09 Nov 1998 15:42:08 +0100
changeset 5840 e2d2b896c717
parent 5635 b7d6b7f66131
child 7639 538bd31709cb
permissions -rw-r--r--
Object logic specific operations.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/type_infer.ML
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
     3
    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
     4
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
     5
Type inference.
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
     6
*)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
     7
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
     8
signature TYPE_INFER =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
     9
sig
2979
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
    10
  val infer_types: (term -> Pretty.T) -> (typ -> Pretty.T)
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
    11
    -> (string -> typ option) -> Sorts.classrel -> Sorts.arities
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    12
    -> string list -> bool -> (indexname -> bool) -> term list -> typ list
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    13
    -> term list * typ list * (indexname * typ) list
5635
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
    14
  val appl_error: (term -> Pretty.T) -> (typ -> Pretty.T)
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
    15
    -> string -> term -> typ -> term -> typ -> string list
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    16
end;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    17
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    18
structure TypeInfer: TYPE_INFER =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    19
struct
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    20
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    21
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    22
(** term encodings **)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    23
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    24
(*
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    25
  Flavours of term encodings:
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    26
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    27
    parse trees (type term):
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    28
      A very complicated structure produced by the syntax module's
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    29
      read functions.  Encodes types and sorts as terms; may contain
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    30
      explicit constraints and partial typing information (where
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    31
      dummyT serves as wildcard).
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    32
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    33
      Parse trees are INTERNAL! Users should never encounter them,
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    34
      except in parse / print translation functions.
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    35
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    36
    raw terms (type term):
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    37
      Provide the user interface to type inferences.  They may contain
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    38
      partial type information (dummyT is wildcard) or explicit type
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    39
      constraints (introduced via constrain: term -> typ -> term).
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    40
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    41
      The type inference function also lets users specify a certain
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    42
      subset of TVars to be treated as non-rigid inference parameters.
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    43
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    44
    preterms (type preterm):
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    45
      The internal representation for type inference.
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    46
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    47
    well-typed term (type term):
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    48
      Fully typed lambda terms to be accepted by appropriate
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    49
      certification functions.
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    50
*)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    51
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    52
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    53
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    54
(** pretyps and preterms **)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    55
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    56
(*links to parameters may get instantiated, anything else is rigid*)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    57
datatype pretyp =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    58
  PType of string * pretyp list |
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    59
  PTFree of string * sort |
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    60
  PTVar of indexname * sort |
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    61
  Param of sort |
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    62
  Link of pretyp ref;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    63
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    64
datatype preterm =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    65
  PConst of string * pretyp |
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    66
  PFree of string * pretyp |
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    67
  PVar of indexname * pretyp |
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    68
  PBound of int |
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    69
  PAbs of string * pretyp * preterm |
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    70
  PAppl of preterm * preterm |
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    71
  Constraint of preterm * pretyp;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    72
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    73
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    74
(* utils *)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    75
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    76
val mk_param = Link o ref o Param;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    77
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    78
fun deref (T as Link (ref (Param _))) = T
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    79
  | deref (Link (ref T)) = deref T
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    80
  | deref T = T;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    81
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    82
fun foldl_pretyps f (x, PConst (_, T)) = f (x, T)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    83
  | foldl_pretyps f (x, PFree (_, T)) = f (x, T)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    84
  | foldl_pretyps f (x, PVar (_, T)) = f (x, T)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    85
  | foldl_pretyps _ (x, PBound _) = x
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    86
  | foldl_pretyps f (x, PAbs (_, T, t)) = foldl_pretyps f (f (x, T), t)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    87
  | foldl_pretyps f (x, PAppl (t, u)) = foldl_pretyps f (foldl_pretyps f (x, t), u)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    88
  | foldl_pretyps f (x, Constraint (t, T)) = f (foldl_pretyps f (x, t), T);
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    89
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    90
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    91
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    92
(** raw typs/terms to pretyps/preterms **)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    93
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    94
(* pretyp(s)_of *)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    95
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    96
fun pretyp_of is_param (params, typ) =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    97
  let
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    98
    fun add_parms (ps, TVar (xi as (x, _), S)) =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
    99
          if is_param xi andalso is_none (assoc (ps, xi))
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   100
          then (xi, mk_param S) :: ps else ps
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   101
      | add_parms (ps, TFree _) = ps
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   102
      | add_parms (ps, Type (_, Ts)) = foldl add_parms (ps, Ts);
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   103
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   104
    val params' = add_parms (params, typ);
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   105
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   106
    fun pre_of (TVar (v as (xi, _))) =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   107
          (case assoc (params', xi) of
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   108
            None => PTVar v
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   109
          | Some p => p)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   110
      | pre_of (TFree v) = PTFree v
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   111
      | pre_of (T as Type (a, Ts)) =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   112
          if T = dummyT then mk_param []
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   113
          else PType (a, map pre_of Ts);
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   114
  in (params', pre_of typ) end;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   115
4957
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   116
fun pretyps_of is_param = foldl_map (pretyp_of is_param);
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   117
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   118
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   119
(* preterm(s)_of *)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   120
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   121
fun preterm_of const_type is_param ((vparams, params), tm) =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   122
  let
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   123
    fun add_vparm (ps, xi) =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   124
      if is_none (assoc (ps, xi)) then
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   125
        (xi, mk_param []) :: ps
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   126
      else ps;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   127
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   128
    fun add_vparms (ps, Var (xi, _)) = add_vparm (ps, xi)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   129
      | add_vparms (ps, Free (x, _)) = add_vparm (ps, (x, ~1))
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   130
      | add_vparms (ps, Abs (_, _, t)) = add_vparms (ps, t)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   131
      | add_vparms (ps, t $ u) = add_vparms (add_vparms (ps, t), u)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   132
      | add_vparms (ps, _) = ps;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   133
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   134
    val vparams' = add_vparms (vparams, tm);
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   135
    fun var_param xi = the (assoc (vparams', xi));
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   136
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   137
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   138
    val preT_of = pretyp_of is_param;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   139
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   140
    fun constrain (ps, t) T =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   141
      if T = dummyT then (ps, t)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   142
      else
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   143
        let val (ps', T') = preT_of (ps, T) in
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   144
          (ps', Constraint (t, T'))
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   145
        end;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   146
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   147
    fun pre_of (ps, Const (c, T)) =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   148
          (case const_type c of
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   149
            Some U => constrain (ps, PConst (c, snd (pretyp_of (K true) ([], U)))) T
3784
3b15cda31c97 eliminated raise_term, raise_typ;
wenzelm
parents: 3510
diff changeset
   150
          | None => raise TYPE ("No such constant: " ^ quote c, [], []))
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   151
      | pre_of (ps, Free (x, T)) = constrain (ps, PFree (x, var_param (x, ~1))) T
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   152
      | pre_of (ps, Var (xi, T)) = constrain (ps, PVar (xi, var_param xi)) T
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   153
      | pre_of (ps, Const ("_type_constraint_", T) $ t) = constrain (pre_of (ps, t)) T
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   154
      | pre_of (ps, Bound i) = (ps, PBound i)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   155
      | pre_of (ps, Abs (x, T, t)) =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   156
          let
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   157
            val (ps', T') = preT_of (ps, T);
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   158
            val (ps'', t') = pre_of (ps', t);
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   159
          in (ps'', PAbs (x, T', t')) end
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   160
      | pre_of (ps, t $ u) =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   161
          let
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   162
            val (ps', t') = pre_of (ps, t);
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   163
            val (ps'', u') = pre_of (ps', u);
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   164
          in (ps'', PAppl (t', u')) end;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   165
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   166
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   167
    val (params', tm') = pre_of (params, tm);
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   168
  in
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   169
    ((vparams', params'), tm')
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   170
  end;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   171
4957
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   172
fun preterms_of const_type is_param = foldl_map (preterm_of const_type is_param);
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   173
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   174
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   175
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   176
(** pretyps/terms to typs/terms **)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   177
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   178
(* add_parms *)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   179
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   180
fun add_parmsT (rs, PType (_, Ts)) = foldl add_parmsT (rs, Ts)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   181
  | add_parmsT (rs, Link (r as ref (Param _))) = r ins rs
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   182
  | add_parmsT (rs, Link (ref T)) = add_parmsT (rs, T)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   183
  | add_parmsT (rs, _) = rs;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   184
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   185
val add_parms = foldl_pretyps add_parmsT;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   186
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   187
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   188
(* add_names *)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   189
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   190
fun add_namesT (xs, PType (_, Ts)) = foldl add_namesT (xs, Ts)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   191
  | add_namesT (xs, PTFree (x, _)) = x ins xs
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   192
  | add_namesT (xs, PTVar ((x, _), _)) = x ins xs
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   193
  | add_namesT (xs, Link (ref T)) = add_namesT (xs, T)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   194
  | add_namesT (xs, Param _) = xs;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   195
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   196
val add_names = foldl_pretyps add_namesT;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   197
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   198
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   199
(* simple_typ/term_of *)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   200
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   201
(*deref links, fail on params*)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   202
fun simple_typ_of (PType (a, Ts)) = Type (a, map simple_typ_of Ts)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   203
  | simple_typ_of (PTFree v) = TFree v
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   204
  | simple_typ_of (PTVar v) = TVar v
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   205
  | simple_typ_of (Link (ref T)) = simple_typ_of T
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   206
  | simple_typ_of (Param _) = sys_error "simple_typ_of: illegal Param";
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   207
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   208
(*convert types, drop constraints*)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   209
fun simple_term_of (PConst (c, T)) = Const (c, simple_typ_of T)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   210
  | simple_term_of (PFree (x, T)) = Free (x, simple_typ_of T)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   211
  | simple_term_of (PVar (xi, T)) = Var (xi, simple_typ_of T)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   212
  | simple_term_of (PBound i) = Bound i
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   213
  | simple_term_of (PAbs (x, T, t)) = Abs (x, simple_typ_of T, simple_term_of t)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   214
  | simple_term_of (PAppl (t, u)) = simple_term_of t $ simple_term_of u
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   215
  | simple_term_of (Constraint (t, _)) = simple_term_of t;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   216
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   217
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   218
(* typs_terms_of *)                             (*DESTRUCTIVE*)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   219
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   220
fun typs_terms_of used mk_var prfx (Ts, ts) =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   221
  let
4957
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   222
    fun elim (r as ref (Param S), x) = r := mk_var (x, S)
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   223
      | elim _ = ();
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   224
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   225
    val used' = foldl add_names (foldl add_namesT (used, Ts), ts);
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   226
    val parms = rev (foldl add_parms (foldl add_parmsT ([], Ts), ts));
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   227
    val pre_names = replicate (length parms) (prfx ^ "'");
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   228
    val names = variantlist (pre_names, prfx ^ "'" :: used');
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   229
  in
4957
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   230
    seq2 elim (parms, names);
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   231
    (map simple_typ_of Ts, map simple_term_of ts)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   232
  end;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   233
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   234
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   235
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   236
(** order-sorted unification of types **)       (*DESTRUCTIVE*)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   237
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   238
exception NO_UNIFIER of string;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   239
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   240
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   241
fun unify classrel arities =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   242
  let
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   243
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   244
    (* adjust sorts of parameters *)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   245
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   246
    fun not_in_sort x S' S =
2989
8189a4870d19 tuned err msg;
wenzelm
parents: 2980
diff changeset
   247
      "Variable " ^ x ^ "::" ^ Sorts.str_of_sort S' ^ " not of sort " ^
2979
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   248
        Sorts.str_of_sort S ^ ".";
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   249
4957
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   250
    fun meet (_, []) = ()
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   251
      | meet (Link (r as (ref (Param S'))), S) =
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   252
          if Sorts.sort_le classrel (S', S) then ()
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   253
          else r := mk_param (Sorts.inter_sort classrel (S', S))
4957
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   254
      | meet (Link (ref T), S) = meet (T, S)
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   255
      | meet (PType (a, Ts), S) =
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   256
          seq2 meet (Ts, Sorts.mg_domain classrel arities a S
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   257
            handle TYPE (msg, _, _) => raise NO_UNIFIER msg)
4957
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   258
      | meet (PTFree (x, S'), S) =
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   259
          if Sorts.sort_le classrel (S', S) then ()
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   260
          else raise NO_UNIFIER (not_in_sort x S' S)
4957
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   261
      | meet (PTVar (xi, S'), S) =
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   262
          if Sorts.sort_le classrel (S', S) then ()
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   263
          else raise NO_UNIFIER (not_in_sort (Syntax.string_of_vname xi) S' S)
4957
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   264
      | meet (Param _, _) = sys_error "meet";
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   265
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   266
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   267
    (* occurs check and assigment *)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   268
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   269
    fun occurs_check r (Link (r' as ref T)) =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   270
          if r = r' then raise NO_UNIFIER "Occurs check!"
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   271
          else occurs_check r T
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   272
      | occurs_check r (PType (_, Ts)) = seq (occurs_check r) Ts
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   273
      | occurs_check _ _ = ();
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   274
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   275
    fun assign r T S =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   276
      (case deref T of
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   277
        T' as Link (r' as ref (Param _)) =>
4957
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   278
          if r = r' then () else (r := T'; meet (T', S))
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   279
      | T' => (occurs_check r T'; r := T'; meet (T', S)));
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   280
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   281
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   282
    (* unification *)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   283
4957
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   284
    fun unif (Link (r as ref (Param S)), T) = assign r T S
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   285
      | unif (T, Link (r as ref (Param S))) = assign r T S
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   286
      | unif (Link (ref T), U) = unif (T, U)
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   287
      | unif (T, Link (ref U)) = unif (T, U)
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   288
      | unif (PType (a, Ts), PType (b, Us)) =
2979
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   289
          if a <> b then
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   290
            raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b ^ ".")
4957
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   291
          else seq2 unif (Ts, Us)
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   292
      | unif (T, U) = if T = U then () else raise NO_UNIFIER "";
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   293
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   294
  in unif end;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   295
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   296
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   297
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   298
(** type inference **)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   299
5635
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
   300
fun appl_error prt prT why t T u U =
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
   301
  ["Type error in application: " ^ why,
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
   302
   "",
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
   303
   Pretty.string_of
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
   304
    (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, prt t,
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
   305
                   Pretty.str " ::", Pretty.brk 1, prT T]),
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
   306
   Pretty.string_of
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
   307
     (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, prt u,
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
   308
                    Pretty.str " ::", Pretty.brk 1, prT U]),
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
   309
   ""];
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
   310
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   311
(* infer *)                                     (*DESTRUCTIVE*)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   312
2979
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   313
fun infer prt prT classrel arities =
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   314
  let
2979
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   315
    (* errors *)
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   316
2979
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   317
    fun unif_failed msg =
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   318
      "Type unification failed" ^ (if msg = "" then "." else ": " ^ msg) ^ "\n";
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   319
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   320
    fun prep_output bs ts Ts =
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   321
      let
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   322
        val (Ts_bTs', ts') = typs_terms_of [] PTFree "??" (Ts @ map snd bs, ts);
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   323
        val len = length Ts;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   324
        val Ts' = take (len, Ts_bTs');
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   325
        val xs = map Free (map fst bs ~~ drop (len, Ts_bTs'));
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   326
        val ts'' = map (fn t => subst_bounds (xs, t)) ts';
2979
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   327
      in (ts'', Ts') end;
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   328
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   329
    fun err_loose i =
3784
3b15cda31c97 eliminated raise_term, raise_typ;
wenzelm
parents: 3510
diff changeset
   330
      raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], []);
2979
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   331
3510
24d235feeb2a improved type checking errors;
wenzelm
parents: 2989
diff changeset
   332
    fun err_appl msg bs t T u U =
2979
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   333
      let
3510
24d235feeb2a improved type checking errors;
wenzelm
parents: 2989
diff changeset
   334
        val ([t', u'], [T', U']) = prep_output bs [t, u] [T, U];
24d235feeb2a improved type checking errors;
wenzelm
parents: 2989
diff changeset
   335
        val why =
24d235feeb2a improved type checking errors;
wenzelm
parents: 2989
diff changeset
   336
          (case T' of
24d235feeb2a improved type checking errors;
wenzelm
parents: 2989
diff changeset
   337
            Type ("fun", _) => "Incompatible operand type."
24d235feeb2a improved type checking errors;
wenzelm
parents: 2989
diff changeset
   338
          | _ => "Operator not of function type.");
5635
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
   339
        val text = unif_failed msg ^
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
   340
                   cat_lines (appl_error prt prT why t' T' u' U');
3784
3b15cda31c97 eliminated raise_term, raise_typ;
wenzelm
parents: 3510
diff changeset
   341
      in raise TYPE (text, [T', U'], [t', u']) end;
2979
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   342
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   343
    fun err_constraint msg bs t T U =
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   344
      let
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   345
        val ([t'], [T', U']) = prep_output bs [t] [T, U];
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   346
        val text = cat_lines
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   347
         [unif_failed msg,
5635
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
   348
          "Cannot meet type constraint:", "",
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
   349
          Pretty.string_of
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
   350
           (Pretty.block [Pretty.str "Term:", Pretty.brk 2, prt t',
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
   351
                          Pretty.str " ::", Pretty.brk 1, prT T']),
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
   352
          Pretty.string_of
b7d6b7f66131 Unified treatment of type error msgs.
nipkow
parents: 5634
diff changeset
   353
           (Pretty.block [Pretty.str "Type:", Pretty.brk 2, prT U']), ""];
3784
3b15cda31c97 eliminated raise_term, raise_typ;
wenzelm
parents: 3510
diff changeset
   354
      in raise TYPE (text, [T', U'], [t']) end;
2979
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   355
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   356
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   357
    (* main *)
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   358
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   359
    val unif = unify classrel arities;
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   360
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   361
    fun inf _ (PConst (_, T)) = T
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   362
      | inf _ (PFree (_, T)) = T
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   363
      | inf _ (PVar (_, T)) = T
2979
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   364
      | inf bs (PBound i) = snd (nth_elem (i, bs) handle LIST _ => err_loose i)
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   365
      | inf bs (PAbs (x, T, t)) = PType ("fun", [T, inf ((x, T) :: bs) t])
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   366
      | inf bs (PAppl (t, u)) =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   367
          let
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   368
            val T = inf bs t;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   369
            val U = inf bs u;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   370
            val V = mk_param [];
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   371
            val U_to_V = PType ("fun", [U, V]);
4957
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   372
            val _ = unif (U_to_V, T) handle NO_UNIFIER msg => err_appl msg bs t T u U;
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   373
          in V end
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   374
      | inf bs (Constraint (t, U)) =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   375
          let val T = inf bs t in
4957
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   376
            unif (T, U) handle NO_UNIFIER msg => err_constraint msg bs t T U;
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   377
            T
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   378
          end;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   379
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   380
  in inf [] end;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   381
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   382
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   383
(* infer_types *)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   384
2979
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   385
fun infer_types prt prT const_type classrel arities used freeze is_param ts Ts =
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   386
  let
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   387
    (*convert to preterms/typs*)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   388
    val (Tps, Ts') = pretyps_of (K true) ([], Ts);
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   389
    val ((vps, ps), ts') = preterms_of const_type is_param (([], Tps), ts);
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   390
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   391
    (*run type inference*)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   392
    val tTs' = ListPair.map Constraint (ts', Ts');
2979
db6941221197 improved type check error messages;
wenzelm
parents: 2957
diff changeset
   393
    val _ = seq (fn t => (infer prt prT classrel arities t; ())) tTs';
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   394
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   395
    (*collect result unifier*)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   396
    fun ch_var (xi, Link (r as ref (Param S))) = (r := PTVar (xi, S); None)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   397
      | ch_var xi_T = Some xi_T;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   398
    val env = mapfilter ch_var Tps;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   399
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   400
    (*convert back to terms/typs*)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   401
    val mk_var =
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   402
      if freeze then PTFree
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   403
      else (fn (x, S) => PTVar ((x, 0), S));
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   404
    val (final_Ts, final_ts) = typs_terms_of used mk_var "" (Ts', ts');
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   405
    val final_env = map (apsnd simple_typ_of) env;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   406
  in
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   407
    (final_ts, final_Ts, final_env)
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   408
  end;
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   409
4957
30c49821e61f remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents: 3784
diff changeset
   410
2957
d35fca99b3be Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff changeset
   411
end;