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