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