src/Pure/type.ML
author wenzelm
Thu, 09 Jun 1994 11:00:01 +0200
changeset 416 12f9f36e4484
parent 401 324ad2e02826
child 422 8f194014a9c8
permissions -rw-r--r--
restored functor sig; added str_of_sort, str_of_arity, rem_sorts; minor internal cleanup;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
     1
(*  Title:      Pure/type.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
     3
    Author:     Tobias Nipkow & Lawrence C Paulson
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
     5
Type classes and sorts. Type signatures. Type unification and inference.
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
     6
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
     7
TODO:
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
     8
  move type unification and inference to type_unify.ML (TypeUnify) (?)
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
     9
  rename args -> tycons, coreg -> arities (?)
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    10
  clean err msgs
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
signature TYPE =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
sig
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    15
  structure Symtab: SYMTAB
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    16
  val str_of_sort: sort -> string
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    17
  val str_of_arity: string * sort list * sort -> string
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  type type_sig
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
    19
  val rep_tsig: type_sig ->
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    20
    {classes: class list,
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    21
     subclass: (class * class list) list,
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    22
     default: sort,
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    23
     args: (string * int) list,
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    24
     abbrs: (string * (indexname list * typ)) list,
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    25
     coreg: (string * (class * sort list) list) list}
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  val defaultS: type_sig -> sort
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    27
  val tsig0: type_sig
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    28
  val logical_types: type_sig -> string list
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    29
  val extend_tsig: type_sig ->
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    30
    (class * class list) list * sort * (string list * int) list *
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    31
    (string list * (sort list * class)) list -> type_sig
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    32
  val ext_subclass: type_sig -> (class * class) list -> type_sig
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    33
  val ext_tsig_abbrs: type_sig -> (string * (indexname list * typ)) list
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    34
    -> type_sig
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    35
  val merge_tsigs: type_sig * type_sig -> type_sig
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    36
  val subsort: type_sig -> sort * sort -> bool
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    37
  val norm_sort: type_sig -> sort -> sort
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    38
  val rem_sorts: typ -> typ
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    39
  val cert_typ: type_sig -> typ -> typ
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    40
  val norm_typ: type_sig -> typ -> typ
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
  val freeze: (indexname -> bool) -> term -> term
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
  val freeze_vars: typ -> typ
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
  val infer_types: type_sig * typ Symtab.table * (indexname -> typ option) *
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    44
    (indexname -> sort option) * typ * term -> term * (indexname * typ) list
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    45
  val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
  val thaw_vars: typ -> typ
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    47
  val typ_errors: type_sig -> typ * string list -> string list
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
  val typ_instance: type_sig * typ * typ -> bool
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    49
  val typ_match: type_sig -> (indexname * typ) list * (typ * typ)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    50
    -> (indexname * typ) list
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    51
  val unify: type_sig -> (typ * typ) * (indexname * typ) list
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    52
    -> (indexname * typ) list
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
  val varifyT: typ -> typ
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
  val varify: term * string list -> term
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
  exception TUNIFY
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    56
  exception TYPE_MATCH
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    59
functor TypeFun(structure Symtab: SYMTAB and Syntax: SYNTAX): TYPE =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    62
structure Symtab = Symtab;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    65
(*** type classes and sorts ***)
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    66
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    67
(*
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    68
  Classes denote (possibly empty) collections of types (e.g. sets of types)
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    69
  and are partially ordered by 'inclusion'. They are represented by strings.
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    70
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    71
  Sorts are intersections of finitely many classes. They are represented by
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    72
  lists of classes.
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    73
*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
type domain = sort list;
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    76
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    77
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    78
(* print sorts and arities *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    80
fun str_of_sort [c] = c
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    81
  | str_of_sort cs = parents "{" "}" (commas cs);
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    82
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    83
fun str_of_dom dom = parents "(" ")" (commas (map str_of_sort dom));
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    84
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    85
fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    86
  | str_of_arity (t, SS, S) =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    87
      t ^ " :: " ^ str_of_dom SS ^ " " ^ str_of_sort S;
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    88
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    89
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    90
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    91
(*** type signatures ***)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    92
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    93
(*
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    94
  classes:
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    95
    a list of all declared classes;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    97
  subclass:
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
    98
    an association list representing the subclass relation; (c, cs) is
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
    99
    interpreted as "c is a proper subclass of all elemenst of cs"; note that
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   100
    c itself is not a memeber of cs;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   101
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   102
  default:
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   103
    the default sort attached to all unconstrained type vars;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   104
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   105
  args:
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   106
    an association list of all declared types with the number of their
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   107
    arguments;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   108
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   109
  abbrs:
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   110
    an association list of type abbreviations;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   111
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   112
  coreg:
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   113
    a two-fold association list of all type arities; (t, al) means that type
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   114
    constructor t has the arities in al; an element (c, ss) of al represents
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   115
    the arity (ss)c;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   118
datatype type_sig =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   119
  TySg of {
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   120
    classes: class list,
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   121
    subclass: (class * class list) list,
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   122
    default: sort,
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   123
    args: (string * int) list,
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   124
    abbrs: (string * (indexname list * typ)) list,
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   125
    coreg: (string * (class * domain) list) list};
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   126
189
831a9a7ab9f3 added rep_tsig
nipkow
parents: 162
diff changeset
   127
fun rep_tsig (TySg comps) = comps;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   129
fun defaultS (TySg {default, ...}) = default;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   130
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   131
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   132
(* error messages *)    (* FIXME move? *)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   133
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   134
fun undcl_class c = "Undeclared class " ^ quote c;
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   135
val err_undcl_class = error o undcl_class;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   137
(* FIXME not yet checked? *)
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   138
fun err_dup_class c =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   139
  error ("Duplicate declaration of class " ^ quote c);
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   140
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   141
fun undcl_type c = "Undeclared type constructor " ^ quote c;
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   142
val err_undcl_type = error o undcl_type;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   143
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   144
fun err_dup_tycon c =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   145
  error ("Duplicate declaration of type constructor " ^ quote c);
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   146
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   147
fun err_neg_args c =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   148
  error ("Negative number of arguments of type constructor " ^ quote c);
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   149
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   150
fun err_dup_tyabbr c =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   151
  error ("Duplicate declaration of type abbreviation " ^ quote c);
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   152
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   153
fun ty_confl c = "Conflicting type constructor and abbreviation " ^ quote c;
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   154
val err_ty_confl = error o ty_confl;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
(* 'leq' checks the partial order on classes according to the
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
   statements in the association list 'a' (i.e.'subclass')
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   161
fun less a (C, D) = case assoc (a, C) of
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
     Some(ss) => D mem ss
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   163
   | None => err_undcl_class (C) ;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   165
fun leq a (C, D)  =  C = D orelse less a (C, D);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   168
(* logical_types *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   170
(*return all logical types of tsig, i.e. all types t with some arity t::(ss)c
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   171
  and c <= logic*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   173
fun logical_types tsig =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   174
  let
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   175
    val TySg {subclass, coreg, args, ...} = tsig;
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   176
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   177
    fun log_class c = leq subclass (c, logicC);
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   178
    fun log_type t = exists (log_class o #1) (assocs coreg t);
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   179
  in
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   180
    filter log_type (map #1 args)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
162
58d54dc482d1 added logical_types
nipkow
parents: 0
diff changeset
   183
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   184
(* 'sortorder' checks the ordering on sets of classes, i.e. on sorts:
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   185
   S1 <= S2 , iff for every class C2 in S2 there exists a class C1 in S1
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
   with C1 <= C2 (according to an association list 'a')
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   189
fun sortorder a (S1, S2) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   190
  forall  (fn C2 => exists  (fn C1 => leq a (C1, C2))  S1)  S2;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
(* 'inj' inserts a new class C into a given class set S (i.e.sort) only if
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
  there exists no class in S which is <= C;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
  the resulting set is minimal if S was minimal
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   198
fun inj a (C, S) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
  let fun inj1 [] = [C]
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   200
        | inj1 (D::T) = if leq a (D, C) then D::T
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   201
                        else if leq a (C, D) then inj1 T
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
                             else D::(inj1 T)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
  in inj1 S end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
(* 'union_sort' forms the minimal union set of two sorts S1 and S2
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
   under the assumption that S2 is minimal *)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   208
(* FIXME rename to inter_sort (?) *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
fun union_sort a = foldr (inj a);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
(* 'elementwise_union' forms elementwise the minimal union set of two
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
   sort lists under the assumption that the two lists have the same length
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   215
*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   217
fun elementwise_union a (Ss1, Ss2) = map (union_sort a) (Ss1~~Ss2);
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   218
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
(* 'lew' checks for two sort lists the ordering for all corresponding list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
   elements (i.e. sorts) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   223
fun lew a (w1, w2) = forall (sortorder a)  (w1~~w2);
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   224
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   226
(* 'is_min' checks if a class C is minimal in a given sort S under the
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   227
   assumption that S contains C *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   229
fun is_min a S C = not (exists (fn (D) => less a (D, C)) S);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
(* 'min_sort' reduces a sort to its minimal classes *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
fun min_sort a S = distinct(filter (is_min a S) S);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
(* 'min_domain' minimizes the domain sorts of type declarationsl;
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   238
   the function will be applied on the type declarations in extensions *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
fun min_domain subclass =
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   241
  let fun one_min (f, (doms, ran)) = (f, (map (min_sort subclass) doms, ran))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
  in map one_min end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
(* 'min_filter' filters a list 'ars' consisting of arities (domain * class)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   246
   and gives back a list of those range classes whose domains meet the
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
   predicate 'pred' *)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   248
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
fun min_filter a pred ars =
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   250
  let fun filt ([], l) = l
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   251
        | filt ((c, x)::xs, l) = if pred(x) then filt (xs, inj a (c, l))
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   252
                               else filt (xs, l)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   253
  in filt (ars, []) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
(* 'cod_above' filters all arities whose domains are elementwise >= than
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   257
   a given domain 'w' and gives back a list of the corresponding range
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
   classes *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   260
fun cod_above (a, w, ars) = min_filter a (fn w' => lew a (w, w')) ars;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   261
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   262
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
   264
(*Instantiation of type variables in types*)
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
   265
(*Pre: instantiations obey restrictions! *)
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
   266
fun inst_typ tye =
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   267
  let fun inst(Type(a, Ts)) = Type(a, map inst Ts)
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
   268
        | inst(T as TFree _) = T
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   269
        | inst(T as TVar(v, _)) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   270
            (case assoc(tye, v) of Some U => inst U | None => T)
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
   271
  in inst end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
(* 'least_sort' returns for a given type its maximum sort:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
   - type variables, free types: the sort brought with
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
   - type constructors: recursive determination of the maximum sort of the
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   276
                    arguments if the type is declared in 'coreg' of the
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   277
                    given type signature  *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   279
fun least_sort (tsig as TySg{subclass, coreg, ...}) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   280
  let fun ls(T as Type(a, Ts)) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   281
                 (case assoc (coreg, a) of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   282
                          Some(ars) => cod_above(subclass, map ls Ts, ars)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   283
                        | None => raise TYPE(undcl_type a, [T], []))
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   284
        | ls(TFree(a, S)) = S
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   285
        | ls(TVar(a, S)) = S
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
  in ls end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   289
fun check_has_sort(tsig as TySg{subclass, coreg, ...}, T, S) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   290
  if sortorder subclass ((least_sort tsig T), S) then ()
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   291
  else raise TYPE("Type not of sort " ^ (str_of_sort S), [T], [])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
(*Instantiation of type variables in types *)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   295
fun inst_typ_tvars(tsig, tye) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   296
  let fun inst(Type(a, Ts)) = Type(a, map inst Ts)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   297
        | inst(T as TFree _) = T
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   298
        | inst(T as TVar(v, S)) = (case assoc(tye, v) of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   299
                None => T | Some(U) => (check_has_sort(tsig, U, S); U))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
  in inst end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
(*Instantiation of type variables in terms *)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   303
fun inst_term_tvars(tsig, tye) = map_term_types (inst_typ_tvars(tsig, tye));
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
   304
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
   305
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
   306
(* expand_typ *)
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
   307
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   308
fun expand_typ (TySg {abbrs, ...}) ty =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   309
  let
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   310
    fun exptyp (Type (a, Ts)) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   311
          (case assoc (abbrs, a) of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   312
            Some (vs, U) => exptyp (inst_typ (vs ~~ Ts) U)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   313
          | None => Type (a, map exptyp Ts))
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   314
      | exptyp T = T
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   315
  in
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   316
    exptyp ty
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   317
  end;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   318
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   319
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   320
(* norm_typ *)      (* FIXME norm sorts *)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   321
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   322
val norm_typ = expand_typ;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   323
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   324
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   325
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   326
(** type matching **)
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
   327
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
exception TYPE_MATCH;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   330
(*typ_match (s, (U, T)) = s' <==> s'(U) = T and s' is an extension of s*)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   331
fun typ_match tsig =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   332
  let
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   333
    fun match (subs, (TVar (v, S), T)) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   334
          (case assoc (subs, v) of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   335
            None => ((v, (check_has_sort (tsig, T, S); T)) :: subs
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   336
              handle TYPE _ => raise TYPE_MATCH)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   337
          | Some U => if U = T then subs else raise TYPE_MATCH)   (* FIXME ??? *)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   338
      | match (subs, (Type (a, Ts), Type (b, Us))) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   339
          if a <> b then raise TYPE_MATCH
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   340
          else foldl match (subs, Ts ~~ Us)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   341
      | match (subs, (TFree x, TFree y)) =      (* FIXME assert equal sorts, don't compare sorts *)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   342
          if x = y then subs else raise TYPE_MATCH
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   343
      | match _ = raise TYPE_MATCH;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   344
  in match end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   345
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   346
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   347
fun typ_instance (tsig, T, U) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   348
  (typ_match tsig ([], (U, T)); true) handle TYPE_MATCH => false;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   349
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   350
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   351
(*(* FIXME old *)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   352
fun typ_instance (tsig, T, U) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   353
  let val x = typ_match tsig ([], (U, T)) in true end
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   354
    handle TYPE_MATCH => false;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   355
*)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   356
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   357
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   358
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   359
(** build type signatures **)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   360
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   361
fun make_tsig (classes, subclass, default, args, abbrs, coreg) =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   362
  TySg {classes = classes, subclass = subclass, default = default,
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   363
    args = args, abbrs = abbrs, coreg = coreg};
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   364
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   365
val tsig0 = make_tsig ([], [], [], [], [], []);
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   366
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   367
401
324ad2e02826 replaced "logic" by logicC;
wenzelm
parents: 256
diff changeset
   368
(* sorts *)
324ad2e02826 replaced "logic" by logicC;
wenzelm
parents: 256
diff changeset
   369
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   370
fun subsort (TySg {subclass, ...}) (S1, S2) =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   371
  sortorder subclass (S1, S2);
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   372
401
324ad2e02826 replaced "logic" by logicC;
wenzelm
parents: 256
diff changeset
   373
fun norm_sort (TySg {subclass, ...}) S =
324ad2e02826 replaced "logic" by logicC;
wenzelm
parents: 256
diff changeset
   374
  sort_strings (min_sort subclass S);
324ad2e02826 replaced "logic" by logicC;
wenzelm
parents: 256
diff changeset
   375
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   376
fun rem_sorts (Type (a, tys)) = Type (a, map rem_sorts tys)
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   377
  | rem_sorts (TFree (x, _)) = TFree (x, [])
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   378
  | rem_sorts (TVar (xi, _)) = TVar (xi, []);
401
324ad2e02826 replaced "logic" by logicC;
wenzelm
parents: 256
diff changeset
   379
324ad2e02826 replaced "logic" by logicC;
wenzelm
parents: 256
diff changeset
   380
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   381
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   382
fun twice(a) = error("Type constructor " ^a^ " has already been declared.");
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   383
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   384
fun tyab_conflict(a) = error("Can't declare type "^(quote a)^"!\nAn abbreviation with this name exists already.");
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   385
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   386
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   387
(* typ_errors *)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   388
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   389
(*check validity of (not necessarily normal) type; accumulate error messages*)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   390
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   391
fun typ_errors tsig (typ, errors) =
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   392
  let
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   393
    val TySg {classes, args, abbrs, ...} = tsig;
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   394
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   395
    fun class_err (errs, c) =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   396
      if c mem classes then errs
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   397
      else undcl_class c ins errs;
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   398
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   399
    val sort_err = foldl class_err;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   400
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   401
    fun typ_errs (Type (c, Us), errs) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   402
          let
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   403
            val errs' = foldr typ_errs (Us, errs);
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   404
            fun nargs n =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   405
              if n = length Us then errs'
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   406
              else ("Wrong number of arguments: " ^ quote c) ins errs';
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   407
          in
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   408
            (case assoc (args, c) of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   409
              Some n => nargs n
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   410
            | None =>
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   411
                (case assoc (abbrs, c) of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   412
                  Some (vs, _) => nargs (length vs)
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   413
                | None => undcl_type c ins errs))
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   414
          end
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   415
    | typ_errs (TFree (_, S), errs) = sort_err (errs, S)
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   416
    | typ_errs (TVar ((x, i), S), errs) =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   417
        if i < 0 then
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   418
          ("Negative index for TVar " ^ quote x) ins sort_err (errs, S)
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   419
        else sort_err (errs, S);
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   420
  in
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   421
    typ_errs (typ, errors)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   422
  end;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   423
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   424
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   425
(* cert_typ *)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   426
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   427
(*check and normalize typ wrt. tsig; errors are indicated by exception TYPE*)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   428
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   429
fun cert_typ tsig ty =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   430
  (case typ_errors tsig (ty, []) of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   431
    [] => norm_typ tsig ty
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   432
  | errs => raise_type (cat_lines errs) [ty] []);
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   433
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   434
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   435
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   436
(** extend type signature **)
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   437
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   438
(* 'add_class' adds a new class to the list of all existing classes *)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   439
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   440
fun add_class (classes, (s, _)) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   441
  if s mem classes then error("Class " ^ s ^ " declared twice.")
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   442
  else s :: classes;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   443
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   444
(* 'add_subclass' adds a tuple consisiting of a new class (the new class
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   445
   has already been inserted into the 'classes' list) and its
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   446
   superclasses (they must be declared in 'classes' too) to the 'subclass'
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   447
   list of the given type signature;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   448
   furthermore all inherited superclasses according to the superclasses
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   449
   brought with are inserted and there is a check that there are no
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   450
   cycles (i.e. C <= D <= C, with C <> D); *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   451
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   452
fun add_subclass classes (subclass, (s, ges)) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   453
let fun upd (subclass, s') = if s' mem classes then
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   454
        let val ges' = the (assoc (subclass, s))
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   455
        in case assoc (subclass, s') of
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   456
             Some sups => if s mem sups
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   457
                           then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s )
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   458
                           else overwrite (subclass, (s, sups union ges'))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   459
           | None => subclass
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   460
         end
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   461
         else err_undcl_class(s')
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   462
in foldl upd (subclass@[(s, ges)], ges) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   463
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   464
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   465
(* 'extend_classes' inserts all new classes into the corresponding
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   466
   lists ('classes', 'subclass') if possible *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   467
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   468
fun extend_classes (classes, subclass, newclasses) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   469
  if newclasses = [] then (classes, subclass) else
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   470
  let val classes' = foldl add_class (classes, newclasses);
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   471
      val subclass' = foldl (add_subclass classes') (subclass, newclasses);
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   472
  in (classes', subclass') end;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   473
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   474
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   475
(* ext_subclass *) (* FIXME check, test *)
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   476
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   477
(* FIXME disallow (c, c) (?) *)
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   478
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   479
fun ext_subclass tsig pairs =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   480
  let
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   481
    val TySg {classes, subclass, default, args, abbrs, coreg} = tsig;
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   482
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   483
    val subclass' = foldl (add_subclass classes)
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   484
      (subclass, map (fn (c1, c2) => (c1, [c2])) pairs);
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   485
  in
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   486
    make_tsig (classes, subclass', default, args, abbrs, coreg)
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   487
  end;
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   488
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   489
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   490
(* Coregularity *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   491
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   492
(* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   493
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   494
fun is_unique_decl coreg (t, (s, w)) = case assoc2 (coreg, (t, s)) of
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   495
      Some(w1) => if w = w1 then () else
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   496
        error("There are two declarations\n" ^
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   497
              str_of_arity(t, w, [s]) ^ " and\n" ^
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   498
              str_of_arity(t, w1, [s]) ^ "\n" ^
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   499
              "with the same result class.")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   500
    | None => ();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   501
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   502
(* 'restr2' checks if there are two declarations t:(Ss1)C1 and t:(Ss2)C2
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   503
   such that C1 >= C2 then Ss1 >= Ss2 (elementwise) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   504
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   505
fun subs (classes, subclass) C =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   506
  let fun sub (rl, l) = if leq subclass (l, C) then l::rl else rl
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   507
  in foldl sub ([], classes) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   508
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   509
fun coreg_err(t, (w1, C), (w2, D)) =
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   510
    error("Declarations " ^ str_of_arity(t, w1, [C]) ^ " and "
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   511
                          ^ str_of_arity(t, w2, [D]) ^ " are in conflict");
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   512
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   513
fun restr2 classes (subclass, coreg) (t, (s, w)) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   514
  let fun restr ([], test) = ()
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   515
        | restr (s1::Ss, test) =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   516
            (case assoc2 (coreg, (t, s1)) of
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   517
              Some dom =>
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   518
                if lew subclass (test (w, dom))
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   519
                then restr (Ss, test)
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   520
                else coreg_err (t, (w, s), (dom, s1))
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   521
            | None => restr (Ss, test))
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   522
      fun forward (t, (s, w)) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   523
        let val s_sups = case assoc (subclass, s) of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   524
                   Some(s_sups) => s_sups | None => err_undcl_class(s);
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   525
        in restr (s_sups, I) end
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   526
      fun backward (t, (s, w)) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   527
        let val s_subs = subs (classes, subclass) s
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   528
        in restr (s_subs, fn (x, y) => (y, x)) end
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   529
  in (backward (t, (s, w)); forward (t, (s, w))) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   530
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   531
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   532
fun varying_decls t =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   533
  error ("Type constructor " ^ quote t ^ " has varying number of arguments");
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   534
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   535
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   536
(* 'coregular' checks
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   537
   - the two restriction conditions 'is_unique_decl' and 'restr2'
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   538
   - if the classes in the new type declarations are known in the
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   539
     given type signature
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   540
   - if one type constructor has always the same number of arguments;
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   541
   if one type declaration has passed all checks it is inserted into
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   542
   the 'coreg' association list of the given type signatrure  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   543
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   544
fun coregular (classes, subclass, args) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   545
  let fun ex C = if C mem classes then () else err_undcl_class(C);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   546
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   547
      fun addar(w, C) (coreg, t) = case assoc(args, t) of
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   548
            Some(n) => if n <> length w then varying_decls(t) else
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   549
                     (is_unique_decl coreg (t, (C, w));
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   550
                      (seq o seq) ex w;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   551
                      restr2 classes (subclass, coreg) (t, (C, w));
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   552
                      let val ars = the (assoc(coreg, t))
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   553
                      in overwrite(coreg, (t, (C, w) ins ars)) end)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   554
          | None => err_undcl_type(t);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   555
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   556
      fun addts(coreg, (ts, ar)) = foldl (addar ar) (coreg, ts)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   557
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   558
  in addts end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   559
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   560
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   561
(* 'close' extends the 'coreg' association list after all new type
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   562
   declarations have been inserted successfully:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   563
   for every declaration t:(Ss)C , for all classses D with C <= D:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   564
      if there is no declaration t:(Ss')C' with C < C' and C' <= D
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   565
      then insert the declaration t:(Ss)D into 'coreg'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   566
   this means, if there exists a declaration t:(Ss)C and there is
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   567
   no declaration t:(Ss')D with C <=D then the declaration holds
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   568
   for all range classes more general than C *)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   569
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   570
fun close (coreg, subclass) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   571
  let fun check sl (l, (s, dom)) = case assoc (subclass, s) of
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   572
          Some(sups) =>
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   573
            let fun close_sup (l, sup) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   574
                  if exists (fn s'' => less subclass (s, s'') andalso
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   575
                                       leq subclass (s'', sup)) sl
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   576
                  then l
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   577
                  else (sup, dom)::l
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   578
            in foldl close_sup (l, sups) end
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   579
        | None => l;
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   580
      fun ext (s, l) = (s, foldl (check (map #1 l)) (l, l));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   581
  in map ext coreg end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   582
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   583
fun add_types (aca, (ts, n)) =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   584
  let
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   585
    fun add_type ((args, coreg, abbrs), t) =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   586
      case assoc(args, t) of              (* FIXME from new *)
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   587
        Some _ => twice(t)
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   588
      | None =>
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   589
          (case assoc(abbrs, t) of
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   590
            Some _ => tyab_conflict(t)
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   591
          | None => ((t, n)::args, (t, [])::coreg, abbrs))
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   592
  in
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   593
    if n < 0 then     (* FIXME err_neg_args *)
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   594
      error ("Type constructor cannot have negative number of arguments")
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   595
    else foldl add_type (aca, ts)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   596
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   597
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   598
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   599
(* add type abbreviations *)    (* FIXME test *)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   600
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   601
fun abbr_errors tsig (a, (lhs_vs, rhs)) =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   602
  let
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   603
    val TySg {args, abbrs, ...} = tsig;
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   604
    val rhs_vs = map #1 (typ_tvars rhs);
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   605
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   606
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   607
    val show_idxs = commas_quote o map fst;
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   608
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   609
    val dup_lhs_vars =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   610
      (case duplicates lhs_vs of
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   611
        [] => []
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   612
      | vs => ["Duplicate variables on lhs: " ^ show_idxs vs]);
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   613
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   614
    val extra_rhs_vars =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   615
      (case gen_rems (op =) (rhs_vs, lhs_vs) of
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   616
        [] => []
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   617
      | vs => ["Extra variables on rhs: " ^ show_idxs vs]);
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   618
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   619
    val tycon_confl =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   620
      if is_none (assoc (args, a)) then []
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   621
      else [ty_confl a];
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   622
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   623
    val dup_abbr =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   624
      if is_none (assoc (abbrs, a)) then []
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   625
      else ["Duplicate declaration of abbreviation"];
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   626
  in
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   627
    dup_lhs_vars @ extra_rhs_vars @ tycon_confl @ dup_abbr @
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   628
      typ_errors tsig (rhs, [])
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   629
  end;
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   630
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   631
fun add_abbr (tsig, abbr as (a, _)) =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   632
  let
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   633
    val TySg {classes, subclass, default, args, coreg, abbrs} = tsig;
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   634
  in
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   635
    (case abbr_errors tsig abbr of
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   636
      [] => make_tsig (classes, subclass, default, args, abbr :: abbrs, coreg)
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   637
    | errs => (seq writeln errs;
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   638
        error ("The error(s) above occurred in type abbreviation " ^ quote a)))
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   639
  end;
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   640
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   641
fun ext_tsig_abbrs tsig abbrs = foldl add_abbr (tsig, abbrs);
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   642
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   643
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   644
(***
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   645
(* FIXME old *)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   646
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
   647
(* check_abbr *)
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
   648
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   649
fun check_abbr ((a, (lhs_vs, U)), tsig as TySg {args, abbrs, ...}) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   650
  let
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   651
    val rhs_vs = map #1 (add_typ_tvars (U, []));
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   652
    fun err_abbr a = "Error in type abbreviation " ^ quote a;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   653
  in
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   654
    if not (rhs_vs subset lhs_vs)
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   655
    then [err_abbr a, ("Extra variables on rhs")]
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   656
    else
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   657
      (case duplicates lhs_vs of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   658
        dups as _ :: _ =>
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   659
          [err_abbr a, "Duplicate variables on lhs: " ^ commas (map (quote o #1) dups)]
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   660
      | [] =>
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   661
        if is_some (assoc (args, a)) then
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   662
          [err_abbr a, ("A type with this name already exists")]
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   663
        else if is_some (assoc (abbrs, a)) then
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   664
          [err_abbr a, ("An abbreviation with this name already exists")]
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   665
        else
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   666
          (case typ_errors tsig (U, []) of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   667
            [] => []
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   668
          | errs => err_abbr a :: errs))
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
   669
  end;
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
   670
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   671
fun add_abbr (tsig as TySg {classes, default, subclass, args, coreg, abbrs}, newabbr) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   672
  (case check_abbr (newabbr, tsig) of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   673
    [] => TySg {classes = classes, default = default, subclass = subclass,
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   674
      args = args, coreg = coreg, abbrs = newabbr :: abbrs}
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   675
  | errs => error (cat_lines errs));
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
   676
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   677
fun ext_tsig_abbrs tsig abbrs = foldl add_abbr (tsig, abbrs);
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   678
***)
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
   679
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
   680
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   681
(* 'extend_tsig' takes the above described check- and extend-functions to
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   682
   extend a given type signature with new classes and new type declarations *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   683
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   684
fun extend_tsig (TySg{classes, default, subclass, args, coreg, abbrs})
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   685
            (newclasses, newdefault, types, arities) =
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   686
  let
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   687
    val (classes', subclass') = extend_classes(classes, subclass, newclasses);
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   688
    val (args', coreg', _) = foldl add_types ((args, coreg, abbrs), types);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   689
    val old_coreg = map #1 coreg;
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   690
    fun is_old c =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   691
      if c mem old_coreg then ()
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   692
      else err_undcl_type c;
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   693
    fun is_new c =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   694
      if c mem old_coreg
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   695
      then twice c else ();
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   696
    val coreg'' =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   697
      foldl (coregular (classes', subclass', args'))
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   698
        (coreg', min_domain subclass' arities);
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   699
    val coreg''' = close (coreg'', subclass');
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   700
    val default' = if null newdefault then default else newdefault;
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   701
  in
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   702
    TySg {classes = classes', subclass = subclass', default = default',
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   703
      args = args', coreg = coreg''', abbrs = abbrs}
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   704
  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   705
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   706
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   707
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   708
(** merge type signatures **)
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   709
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   710
(* 'assoc_union' merges two association lists if the contents associated
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   711
   the keys are lists *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   712
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   713
fun assoc_union (as1, []) = as1
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   714
  | assoc_union (as1, (key, l2)::as2) = case assoc (as1, key) of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   715
        Some(l1) => assoc_union (overwrite(as1, (key, l1 union l2)), as2)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   716
      | None => assoc_union ((key, l2)::as1, as2);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   717
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   718
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   719
fun trcl r =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   720
  let val r' = transitive_closure r
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   721
  in if exists (op mem) r' then error("Cyclic class structure!") else r' end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   722
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   723
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   724
(* 'merge_coreg' builds the union of two 'coreg' lists;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   725
   it only checks the two restriction conditions and inserts afterwards
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   726
   all elements of the second list into the first one *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   727
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   728
fun merge_coreg classes subclass1 =
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   729
  let fun test_ar classes (t, ars1) (coreg1, (s, w)) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   730
        (is_unique_decl coreg1 (t, (s, w));
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   731
         restr2 classes (subclass1, coreg1) (t, (s, w));
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   732
         overwrite (coreg1, (t, (s, w) ins ars1)));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   733
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   734
      fun merge_c (coreg1, (c as (t, ars2))) = case assoc (coreg1, t) of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   735
          Some(ars1) => foldl (test_ar classes (t, ars1)) (coreg1, ars2)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   736
        | None => c::coreg1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   737
  in foldl merge_c end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   738
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   739
fun merge_args (args, (t, n)) =
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   740
  (case assoc (args, t) of
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   741
    Some m => if m = n then args else varying_decls t
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   742
  | None => (t, n) :: args);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   743
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   744
(* FIXME raise ... *)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   745
fun merge_abbrs (abbrs1, abbrs2) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   746
  let
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   747
    val abbrs = abbrs1 union abbrs2;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   748
    val names = map fst abbrs;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   749
  in
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   750
    (case duplicates names of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   751
      [] => abbrs
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   752
    | dups => error ("Duplicate declaration of type abbreviations: " ^
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   753
        commas_quote dups))
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   754
  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   755
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   756
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   757
(* 'merge_tsigs' takes the above declared functions to merge two type
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   758
  signatures *)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   759
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   760
fun merge_tsigs(TySg{classes=classes1, default=default1, subclass=subclass1, args=args1,
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   761
           coreg=coreg1, abbrs=abbrs1},
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   762
          TySg{classes=classes2, default=default2, subclass=subclass2, args=args2,
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   763
           coreg=coreg2, abbrs=abbrs2}) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   764
  let val classes' = classes1 union classes2;
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   765
      val subclass' = trcl (assoc_union (subclass1, subclass2));
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   766
      val args' = foldl merge_args (args1, args2)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   767
      val coreg' = merge_coreg classes' subclass' (coreg1, coreg2);
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
   768
      val default' = min_sort subclass' (default1 @ default2);
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   769
      val abbrs' = merge_abbrs(abbrs1, abbrs2);
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   770
  in TySg{classes=classes' , default=default', subclass=subclass', args=args',
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   771
          coreg=coreg' , abbrs = abbrs' }
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   772
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   773
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 189
diff changeset
   774
416
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   775
12f9f36e4484 restored functor sig;
wenzelm
parents: 401
diff changeset
   776
(*** type unification and inference ***)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   777
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   778
(*
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   779
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   780
Input:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   781
- a 'raw' term which contains only dummy types and some explicit type
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   782
  constraints encoded as terms.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   783
- the expected type of the term.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   784
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   785
Output:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   786
- the correctly typed term
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   787
- the substitution needed to unify the actual type of the term with its
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   788
  expected type; only the TVars in the expected type are included.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   789
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   790
During type inference all TVars in the term have negative index. This keeps
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   791
them apart from normal TVars, which is essential, because at the end the type
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   792
of the term is unified with the expected type, which contains normal TVars.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   793
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   794
1. Add initial type information to the term (add_types).
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   795
   This freezes (freeze_vars) TVars in explicitly provided types (eg
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   796
   constraints or defaults) by turning them into TFrees.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   797
2. Carry out type inference, possibly introducing new negative TVars.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   798
3. Unify actual and expected type.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   799
4. Turn all (negative) TVars into unique new TFrees (freeze).
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   800
5. Thaw all TVars frozen in step 1 (thaw_vars).
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   801
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   802
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   803
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   804
(*Raised if types are not unifiable*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   805
exception TUNIFY;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   806
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   807
val tyvar_count = ref(~1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   808
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   809
fun tyinit() = (tyvar_count := ~1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   810
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   811
fun new_tvar_inx() = (tyvar_count := !tyvar_count-1; !tyvar_count)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   812
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   813
(*
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   814
Generate new TVar.  Index is < ~1 to distinguish it from TVars generated from
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   815
variable names (see id_type).  Name is arbitrary because index is new.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   816
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   817
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   818
fun gen_tyvar(S) = TVar(("'a", new_tvar_inx()), S);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   819
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   820
(*Occurs check: type variable occurs in type?*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   821
fun occ v tye =
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   822
  let fun occ(Type(_, Ts)) = exists occ Ts
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   823
        | occ(TFree _) = false
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   824
        | occ(TVar(w, _)) = v=w orelse
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   825
                           (case assoc(tye, w) of
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   826
                              None   => false
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   827
                            | Some U => occ U);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   828
  in occ end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   829
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   830
(*Chase variable assignments in tye.
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   831
  If devar (T, tye) returns a type var then it must be unassigned.*)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   832
fun devar (T as TVar(v, _), tye) = (case  assoc(tye, v)  of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   833
          Some U =>  devar (U, tye)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   834
        | None   =>  T)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   835
  | devar (T, tye) = T;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   836
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   837
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   838
(* 'dom' returns for a type constructor t the list of those domains
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   839
   which deliver a given range class C *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   840
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   841
fun dom coreg t C = case assoc2 (coreg, (t, C)) of
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   842
    Some(Ss) => Ss
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   843
  | None => raise TUNIFY;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   844
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   845
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   846
(* 'Dom' returns the union of all domain lists of 'dom' for a given sort S
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   847
   (i.e. a set of range classes ); the union is carried out elementwise
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   848
   for the seperate sorts in the domains *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   849
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   850
fun Dom (subclass, coreg) (t, S) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   851
  let val domlist = map (dom coreg t) S;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   852
  in if null domlist then []
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   853
     else foldl (elementwise_union subclass) (hd domlist, tl domlist)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   854
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   855
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   856
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   857
fun W ((T, S), tsig as TySg{subclass, coreg, ...}, tye) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   858
  let fun Wd ((T, S), tye) = W ((devar (T, tye), S), tsig, tye)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   859
      fun Wk(T as TVar(v, S')) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   860
              if sortorder subclass (S', S) then tye
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   861
              else (v, gen_tyvar(union_sort subclass (S', S)))::tye
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   862
        | Wk(T as TFree(v, S')) = if sortorder subclass (S', S) then tye
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   863
                                 else raise TUNIFY
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   864
        | Wk(T as Type(f, Ts)) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   865
           if null S then tye
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   866
           else foldr Wd (Ts~~(Dom (subclass, coreg) (f, S)) , tye)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   867
  in Wk(T) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   868
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   869
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   870
(* Order-sorted Unification of Types (U)  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   871
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   872
(* Precondition: both types are well-formed w.r.t. type constructor arities *)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   873
fun unify (tsig as TySg{subclass, coreg, ...}) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   874
  let fun unif ((T, U), tye) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   875
        case (devar(T, tye), devar(U, tye)) of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   876
          (T as TVar(v, S1), U as TVar(w, S2)) =>
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   877
             if v=w then tye else
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   878
             if sortorder subclass (S1, S2) then (w, T)::tye else
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   879
             if sortorder subclass (S2, S1) then (v, U)::tye
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   880
             else let val nu = gen_tyvar (union_sort subclass (S1, S2))
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   881
                  in (v, nu)::(w, nu)::tye end
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   882
        | (T as TVar(v, S), U) =>
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   883
             if occ v tye U then raise TUNIFY else W ((U, S), tsig, (v, U)::tye)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   884
        | (U, T as TVar (v, S)) =>
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   885
             if occ v tye U then raise TUNIFY else W ((U, S), tsig, (v, U)::tye)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   886
        | (Type(a, Ts), Type(b, Us)) =>
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   887
             if a<>b then raise TUNIFY else foldr unif (Ts~~Us, tye)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   888
        | (T, U) => if T=U then tye else raise TUNIFY
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   889
  in unif end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   890
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   891
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   892
(*Type inference for polymorphic term*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   893
fun infer tsig =
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   894
  let fun inf(Ts, Const (_, T), tye) = (T, tye)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   895
        | inf(Ts, Free  (_, T), tye) = (T, tye)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   896
        | inf(Ts, Bound i, tye) = ((nth_elem(i, Ts) , tye)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   897
          handle LIST _=> raise TYPE ("loose bound variable", [], [Bound i]))
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   898
        | inf(Ts, Var (_, T), tye) = (T, tye)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   899
        | inf(Ts, Abs (_, T, body), tye) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   900
            let val (U, tye') = inf(T::Ts, body, tye) in  (T-->U, tye')  end
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   901
        | inf(Ts, f$u, tye) =
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   902
            let val (U, tyeU) = inf(Ts, u, tye);
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   903
                val (T, tyeT) = inf(Ts, f, tyeU);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   904
                fun err s =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   905
                  raise TYPE(s, [inst_typ tyeT T, inst_typ tyeT U], [f$u])
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   906
            in case T of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   907
                 Type("fun", [T1, T2]) =>
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   908
                   ( (T2, unify tsig ((T1, U), tyeT))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   909
                     handle TUNIFY => err"type mismatch in application" )
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   910
               | TVar _ =>
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   911
                   let val T2 = gen_tyvar([])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   912
                   in (T2, unify tsig ((T, U-->T2), tyeT))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   913
                      handle TUNIFY => err"type mismatch in application"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   914
                   end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   915
               | _ => err"rator must have function type"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   916
           end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   917
  in inf end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   918
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   919
fun freeze_vars(Type(a, Ts)) = Type(a, map freeze_vars Ts)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   920
  | freeze_vars(T as TFree _) = T
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   921
  | freeze_vars(TVar(v, S)) = TFree(Syntax.string_of_vname v, S);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   922
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   923
(* Attach a type to a constant *)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   924
fun type_const (a, T) = Const(a, incr_tvar (new_tvar_inx()) T);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   925
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   926
(*Find type of ident.  If not in table then use ident's name for tyvar
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   927
  to get consistent typing.*)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   928
fun new_id_type a = TVar(("'"^a, new_tvar_inx()), []);
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   929
fun type_of_ixn(types, ixn as (a, _)) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   930
        case types ixn of Some T => freeze_vars T | None => TVar(("'"^a, ~1), []);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   931
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   932
fun constrain(term, T) = Const(Syntax.constrainC, T-->T) $ term;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   933
fun constrainAbs(Abs(a, _, body), T) = Abs(a, T, body);
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   934
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   935
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   936
(*
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   937
  Attach types to a term. Input is a "parse tree" containing dummy types.
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   938
  Type constraints are translated and checked for validity wrt tsig. TVars in
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   939
  constraints are frozen.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   940
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   941
  The atoms in the resulting term satisfy the following spec:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   942
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   943
  Const (a, T):
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   944
    T is a renamed copy of the generic type of a; renaming decreases index of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   945
    all TVars by new_tvar_inx(), which is less than ~1. The index of all
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   946
    TVars in the generic type must be 0 for this to work!
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   947
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   948
  Free (a, T), Var (ixn, T):
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   949
    T is either the frozen default type of a or TVar (("'"^a, ~1), [])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   950
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   951
  Abs (a, T, _):
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   952
    T is either a type constraint or TVar (("'" ^ a, i), []), where i is
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   953
    generated by new_tvar_inx(). Thus different abstractions can have the
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   954
    bound variables of the same name but different types.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   955
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   956
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   957
(* FIXME replace const_tab by (const_typ: string -> typ option) (?) *)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   958
(* FIXME improve handling of sort constraints *)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   959
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   960
fun add_types (tsig, const_tab, types, sorts) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   961
  let
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   962
    val S0 = defaultS tsig;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   963
    fun defS0 ixn = if_none (sorts ixn) S0;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   964
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   965
    fun prepareT typ =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   966
      freeze_vars (cert_typ tsig (Syntax.typ_of_term defS0 typ));
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   967
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   968
    fun add (Const (a, _)) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   969
          (case Symtab.lookup (const_tab, a) of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   970
            Some T => type_const (a, T)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   971
          | None => raise_type ("No such constant: " ^ quote a) [] [])
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   972
      | add (Bound i) = Bound i
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   973
      | add (Free (a, _)) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   974
          (case Symtab.lookup (const_tab, a) of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   975
            Some T => type_const (a, T)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   976
          | None => Free (a, type_of_ixn (types, (a, ~1))))
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   977
      | add (Var (ixn, _)) = Var (ixn, type_of_ixn (types, ixn))
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   978
      | add (Abs (a, _, body)) = Abs (a, new_id_type a, add body)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   979
      | add ((f as Const (a, _) $ t1) $ t2) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   980
          if a = Syntax.constrainC then
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   981
            constrain (add t1, prepareT t2)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   982
          else if a = Syntax.constrainAbsC then
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   983
            constrainAbs (add t1, prepareT t2)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   984
          else add f $ add t2
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   985
      | add (f $ t) = add f $ add t;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   986
  in add end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   987
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   988
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   989
(* Post-Processing *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   990
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   991
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   992
(*Instantiation of type variables in terms*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   993
fun inst_types tye = map_term_types (inst_typ tye);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   994
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   995
(*Delete explicit constraints -- occurrences of "_constrain" *)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   996
fun unconstrain (Abs(a, T, t)) = Abs(a, T, unconstrain t)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
   997
  | unconstrain ((f as Const(a, _)) $ t) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   998
      if a=Syntax.constrainC then unconstrain t
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   999
      else unconstrain f $ unconstrain t
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1000
  | unconstrain (f$t) = unconstrain f $ unconstrain t
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1001
  | unconstrain (t) = t;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1002
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1003
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1004
(* Turn all TVars which satisfy p into new TFrees *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1005
fun freeze p t =
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1006
  let val fs = add_term_tfree_names(t, []);
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1007
      val inxs = filter p (add_term_tvar_ixns(t, []));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1008
      val vmap = inxs ~~ variantlist(map #1 inxs, fs);
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1009
      fun free(Type(a, Ts)) = Type(a, map free Ts)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1010
        | free(T as TVar(v, S)) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1011
            (case assoc(vmap, v) of None => T | Some(a) => TFree(a, S))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1012
        | free(T as TFree _) = T
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1013
  in map_term_types free t end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1014
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1015
(* Thaw all TVars that were frozen in freeze_vars *)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1016
fun thaw_vars(Type(a, Ts)) = Type(a, map thaw_vars Ts)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1017
  | thaw_vars(T as TFree(a, S)) = (case explode a of
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1018
          "?"::"'"::vn => let val ((b, i), _) = Syntax.scan_varname vn
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1019
                          in TVar(("'"^b, i), S) end
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1020
        | _ => T)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1021
  | thaw_vars(T) = T;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1022
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1023
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1024
fun restrict tye =
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1025
  let fun clean(tye1, ((a, i), T)) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1026
        if i < 0 then tye1 else ((a, i), inst_typ tye T) :: tye1
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1027
  in foldl clean ([], tye) end
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1028
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1029
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1030
(*Infer types for term t using tables. Check that t's type and T unify *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1031
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1032
fun infer_term (tsig, const_tab, types, sorts, T, t) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1033
  let val u = add_types (tsig, const_tab, types, sorts) t;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1034
      val (U, tye) = infer tsig ([], u, []);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1035
      val uu = unconstrain u;
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1036
      val tye' = unify tsig ((T, U), tye) handle TUNIFY => raise TYPE
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1037
        ("Term does not have expected type", [T, U], [inst_types tye uu])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1038
      val Ttye = restrict tye' (* restriction to TVars in T *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1039
      val all = Const("", Type("", map snd Ttye)) $ (inst_types tye' uu)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1040
        (* all is a dummy term which contains all exported TVars *)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1041
      val Const(_, Type(_, Ts)) $ u'' =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1042
            map_term_types thaw_vars (freeze (fn (_, i) => i<0) all)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1043
        (* turn all internally generated TVars into TFrees
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1044
           and thaw all initially frozen TVars *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1045
  in (u'', (map fst Ttye) ~~ Ts) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1046
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1047
fun infer_types args = (tyinit(); infer_term args);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1048
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1049
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1050
(* Turn TFrees into TVars to allow types & axioms to be written without "?" *)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1051
fun varifyT (Type (a, Ts)) = Type (a, map varifyT Ts)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1052
  | varifyT (TFree (a, S)) = TVar ((a, 0), S)
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1053
  | varifyT T = T;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1054
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1055
(* Turn TFrees except those in fixed into new TVars *)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1056
fun varify (t, fixed) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1057
  let val fs = add_term_tfree_names(t, []) \\ fixed;
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1058
      val ixns = add_term_tvar_ixns(t, []);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1059
      val fmap = fs ~~ variantlist(fs, map #1 ixns)
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1060
      fun thaw(Type(a, Ts)) = Type(a, map thaw Ts)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1061
        | thaw(T as TVar _) = T
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1062
        | thaw(T as TFree(a, S)) =
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1063
            (case assoc(fmap, a) of None => T | Some b => TVar((b, 0), S))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1064
  in map_term_types thaw t end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1065
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1066
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
  1067
end;
256
b401c3d06024 (this is a preliminary release)
wenzelm
parents: 200
diff changeset
  1068