256

1 
(* Title: Pure/type.ML


2 
Author: Tobias Nipkow & Lawrence C Paulson

0

3 
ID: $Id$


4 

256

5 
Types and Sorts. Type Inference.


6 


7 
TODO:


8 
Maybe type classes should go in a separate module?


9 
Maybe type inference part (excl unify) should go in a separate module?

0

10 
*)


11 


12 
signature TYPE =


13 
sig

256

14 
structure Symtab: SYMTAB

0

15 
type type_sig

200

16 
val rep_tsig: type_sig >

256

17 
{classes: class list,


18 
subclass: (class * class list) list,


19 
default: sort,


20 
args: (string * int) list,


21 
abbrs: (string * (indexname list * typ)) list,


22 
coreg: (string * (class * sort list) list) list}

0

23 
val defaultS: type_sig > sort

256

24 
val logical_types: type_sig > string list


25 
val tsig0: type_sig


26 
val extend_tsig: type_sig >


27 
(class * class list) list * sort * (string list * int) list *


28 
(string list * (sort list * class)) list > type_sig


29 
val ext_tsig_abbrs: type_sig > (string * (indexname list * typ)) list


30 
> type_sig


31 
val merge_tsigs: type_sig * type_sig > type_sig


32 
val cert_typ: type_sig > typ > typ


33 
val norm_typ: type_sig > typ > typ

0

34 
val freeze: (indexname > bool) > term > term


35 
val freeze_vars: typ > typ


36 
val infer_types: type_sig * typ Symtab.table * (indexname > typ option) *

256

37 
(indexname > sort option) * typ * term > term * (indexname * typ) list


38 
val inst_term_tvars: type_sig * (indexname * typ) list > term > term

0

39 
val thaw_vars: typ > typ

256

40 
val typ_errors: type_sig > typ * string list > string list

0

41 
val typ_instance: type_sig * typ * typ > bool

256

42 
val typ_match: type_sig > (indexname * typ) list * (typ * typ)


43 
> (indexname * typ) list


44 
val unify: type_sig > (typ * typ) * (indexname * typ) list


45 
> (indexname * typ) list

0

46 
val varifyT: typ > typ


47 
val varify: term * string list > term


48 
exception TUNIFY

256

49 
exception TYPE_MATCH

0

50 
end;


51 

256

52 
functor TypeFun(structure Symtab: SYMTAB and Syntax: SYNTAX) (*: TYPE*) (* FIXME debug *) =

0

53 
struct


54 

256

55 
structure Symtab = Symtab;

0

56 


57 

256

58 
(*** type classes ***) (* FIXME improve comment *)

0

59 


60 
type domain = sort list;


61 
type arity = domain * class;


62 

256

63 
fun str_of_sort S = parents "{" "}" (commas S);


64 
fun str_of_dom dom = parents "(" ")" (commas (map str_of_sort dom));


65 
fun str_of_decl (t, w, C) = t ^ " :: " ^ str_of_dom w ^ " " ^ C;


66 


67 


68 


69 
(** type signature **)


70 


71 
(*


72 
classes:


73 
a list of all declared classes;

0

74 

256

75 
subclass:


76 
association list representation of subclass relationship; (c, cs) is


77 
interpreted as "c is a proper subclass of all elemenst of cs"; note that


78 
c itself is not a memeber of cs;


79 


80 
default:


81 
the default sort attached to all unconstrained type vars;


82 


83 
args:


84 
an association list of all declared types with the number of their


85 
arguments;


86 


87 
abbrs:


88 
an association list of type abbreviations;


89 


90 
coreg:


91 
a twofold association list of all type arities; (t, al) means that type


92 
constructor t has the arities in al; an element (c, ss) of al represents


93 
the arity (ss)c;

0

94 
*)


95 

256

96 
datatype type_sig =


97 
TySg of {


98 
classes: class list,


99 
subclass: (class * class list) list,


100 
default: sort,


101 
args: (string * int) list,


102 
abbrs: (string * (indexname list * typ)) list,


103 
coreg: (string * (class * domain) list) list};


104 

189

105 
fun rep_tsig (TySg comps) = comps;

0

106 

256

107 
fun defaultS (TySg {default, ...}) = default;


108 


109 


110 


111 
(* FIXME move *)

0

112 

256

113 
fun undcl_class c = "Undeclared class: " ^ quote c;


114 
val err_undcl_class = error o undcl_class;

0

115 

256

116 
fun undcl_type c = "Undeclared type constructor: " ^ quote c;


117 
val err_undcl_type = error o undcl_type;


118 

0

119 


120 


121 
(* 'leq' checks the partial order on classes according to the


122 
statements in the association list 'a' (i.e.'subclass')


123 
*)


124 

256

125 
fun less a (C, D) = case assoc (a, C) of

0

126 
Some(ss) => D mem ss

256

127 
 None => err_undcl_class (C) ;

0

128 

256

129 
fun leq a (C, D) = C = D orelse less a (C, D);

0

130 


131 

256

132 

0

133 


134 
(* 'logical_type' checks if some type declaration t has as range


135 
a class which is a subclass of "logic" *)


136 

256

137 
fun logical_type(tsig as TySg{subclass, coreg, ...}) t =


138 
let fun is_log C = leq subclass (C, "logic")


139 
in case assoc (coreg, t) of

0

140 
Some(ars) => exists (is_log o #1) ars

256

141 
 None => err_undcl_type(t)

0

142 
end;


143 

162

144 
fun logical_types (tsig as TySg {args, ...}) =


145 
filter (logical_type tsig) (map #1 args);


146 

256

147 
(* 'sortorder' checks the ordering on sets of classes, i.e. on sorts:


148 
S1 <= S2 , iff for every class C2 in S2 there exists a class C1 in S1

0

149 
with C1 <= C2 (according to an association list 'a')


150 
*)


151 

256

152 
fun sortorder a (S1, S2) =


153 
forall (fn C2 => exists (fn C1 => leq a (C1, C2)) S1) S2;

0

154 


155 


156 
(* 'inj' inserts a new class C into a given class set S (i.e.sort) only if


157 
there exists no class in S which is <= C;


158 
the resulting set is minimal if S was minimal


159 
*)


160 

256

161 
fun inj a (C, S) =

0

162 
let fun inj1 [] = [C]

256

163 
 inj1 (D::T) = if leq a (D, C) then D::T


164 
else if leq a (C, D) then inj1 T

0

165 
else D::(inj1 T)


166 
in inj1 S end;


167 


168 


169 
(* 'union_sort' forms the minimal union set of two sorts S1 and S2


170 
under the assumption that S2 is minimal *)

256

171 
(* FIXME rename to inter_sort (?) *)

0

172 


173 
fun union_sort a = foldr (inj a);


174 


175 


176 
(* 'elementwise_union' forms elementwise the minimal union set of two


177 
sort lists under the assumption that the two lists have the same length

256

178 
*)

0

179 

256

180 
fun elementwise_union a (Ss1, Ss2) = map (union_sort a) (Ss1~~Ss2);


181 

0

182 


183 
(* 'lew' checks for two sort lists the ordering for all corresponding list


184 
elements (i.e. sorts) *)


185 

256

186 
fun lew a (w1, w2) = forall (sortorder a) (w1~~w2);


187 

0

188 

256

189 
(* 'is_min' checks if a class C is minimal in a given sort S under the


190 
assumption that S contains C *)

0

191 

256

192 
fun is_min a S C = not (exists (fn (D) => less a (D, C)) S);

0

193 


194 


195 
(* 'min_sort' reduces a sort to its minimal classes *)


196 


197 
fun min_sort a S = distinct(filter (is_min a S) S);


198 


199 


200 
(* 'min_domain' minimizes the domain sorts of type declarationsl;

256

201 
the function will be applied on the type declarations in extensions *)

0

202 


203 
fun min_domain subclass =

256

204 
let fun one_min (f, (doms, ran)) = (f, (map (min_sort subclass) doms, ran))

0

205 
in map one_min end;


206 


207 


208 
(* 'min_filter' filters a list 'ars' consisting of arities (domain * class)

256

209 
and gives back a list of those range classes whose domains meet the

0

210 
predicate 'pred' *)

256

211 

0

212 
fun min_filter a pred ars =

256

213 
let fun filt ([], l) = l


214 
 filt ((c, x)::xs, l) = if pred(x) then filt (xs, inj a (c, l))


215 
else filt (xs, l)


216 
in filt (ars, []) end;

0

217 


218 


219 
(* 'cod_above' filters all arities whose domains are elementwise >= than

256

220 
a given domain 'w' and gives back a list of the corresponding range

0

221 
classes *)


222 

256

223 
fun cod_above (a, w, ars) = min_filter a (fn w' => lew a (w, w')) ars;


224 


225 

0

226 

200

227 
(*Instantiation of type variables in types*)


228 
(*Pre: instantiations obey restrictions! *)


229 
fun inst_typ tye =

256

230 
let fun inst(Type(a, Ts)) = Type(a, map inst Ts)

200

231 
 inst(T as TFree _) = T

256

232 
 inst(T as TVar(v, _)) =


233 
(case assoc(tye, v) of Some U => inst U  None => T)

200

234 
in inst end;

0

235 


236 
(* 'least_sort' returns for a given type its maximum sort:


237 
 type variables, free types: the sort brought with


238 
 type constructors: recursive determination of the maximum sort of the

256

239 
arguments if the type is declared in 'coreg' of the


240 
given type signature *)

0

241 

256

242 
fun least_sort (tsig as TySg{subclass, coreg, ...}) =


243 
let fun ls(T as Type(a, Ts)) =


244 
(case assoc (coreg, a) of


245 
Some(ars) => cod_above(subclass, map ls Ts, ars)


246 
 None => raise TYPE(undcl_type a, [T], []))


247 
 ls(TFree(a, S)) = S


248 
 ls(TVar(a, S)) = S

0

249 
in ls end;


250 


251 

256

252 
fun check_has_sort(tsig as TySg{subclass, coreg, ...}, T, S) =


253 
if sortorder subclass ((least_sort tsig T), S) then ()


254 
else raise TYPE("Type not of sort " ^ (str_of_sort S), [T], [])

0

255 


256 


257 
(*Instantiation of type variables in types *)

256

258 
fun inst_typ_tvars(tsig, tye) =


259 
let fun inst(Type(a, Ts)) = Type(a, map inst Ts)


260 
 inst(T as TFree _) = T


261 
 inst(T as TVar(v, S)) = (case assoc(tye, v) of


262 
None => T  Some(U) => (check_has_sort(tsig, U, S); U))

0

263 
in inst end;


264 


265 
(*Instantiation of type variables in terms *)

256

266 
fun inst_term_tvars(tsig, tye) = map_term_types (inst_typ_tvars(tsig, tye));

200

267 


268 


269 
(* expand_typ *)


270 

256

271 
fun expand_typ (TySg {abbrs, ...}) ty =


272 
let


273 
fun exptyp (Type (a, Ts)) =


274 
(case assoc (abbrs, a) of


275 
Some (vs, U) => exptyp (inst_typ (vs ~~ Ts) U)


276 
 None => Type (a, map exptyp Ts))


277 
 exptyp T = T


278 
in


279 
exptyp ty


280 
end;


281 


282 


283 
(* norm_typ *) (* FIXME norm sorts *)


284 


285 
val norm_typ = expand_typ;


286 


287 


288 


289 
(** type matching **)

200

290 

0

291 
exception TYPE_MATCH;


292 

256

293 
(*typ_match (s, (U, T)) = s' <==> s'(U) = T and s' is an extension of s*)


294 
fun typ_match tsig =


295 
let


296 
fun match (subs, (TVar (v, S), T)) =


297 
(case assoc (subs, v) of


298 
None => ((v, (check_has_sort (tsig, T, S); T)) :: subs


299 
handle TYPE _ => raise TYPE_MATCH)


300 
 Some U => if U = T then subs else raise TYPE_MATCH) (* FIXME ??? *)


301 
 match (subs, (Type (a, Ts), Type (b, Us))) =


302 
if a <> b then raise TYPE_MATCH


303 
else foldl match (subs, Ts ~~ Us)


304 
 match (subs, (TFree x, TFree y)) = (* FIXME assert equal sorts, don't compare sorts *)


305 
if x = y then subs else raise TYPE_MATCH


306 
 match _ = raise TYPE_MATCH;


307 
in match end;

0

308 


309 

256

310 
fun typ_instance (tsig, T, U) =


311 
(typ_match tsig ([], (U, T)); true) handle TYPE_MATCH => false;


312 


313 


314 
(*(* FIXME old *)


315 
fun typ_instance (tsig, T, U) =


316 
let val x = typ_match tsig ([], (U, T)) in true end


317 
handle TYPE_MATCH => false;


318 
*)


319 


320 


321 


322 
(** build type signatures **)


323 


324 
val tsig0 =


325 
TySg {


326 
classes = [],


327 
subclass = [],


328 
default = [],


329 
args = [],


330 
abbrs = [],


331 
coreg = []};


332 

0

333 


334 
fun not_ident(s) = error("Must be an identifier: " ^ s);


335 


336 
fun twice(a) = error("Type constructor " ^a^ " has already been declared.");


337 

256

338 
fun tyab_conflict(a) = error("Can't declare type "^(quote a)^"!\nAn abbreviation with this name exists already.");

0

339 


340 

256

341 
(* typ_errors *) (* FIXME check, improve *)


342 


343 
(*check validity of (not necessarily normal) type;


344 
accumulates error messages in "errs"*)


345 


346 
fun typ_errors (TySg {classes, args, abbrs, ...}) ty =


347 
let


348 
fun class_err (errs, C) =


349 
if C mem classes then errs


350 
else undcl_class C :: errs;


351 


352 
val sort_err = foldl class_err;

0

353 

256

354 
fun typ_errs (Type (c, Us), errs) =


355 
let


356 
val errs' = foldr typ_errs (Us, errs);


357 
fun nargs n =


358 
if n = length Us then errs'


359 
else ("Wrong number of arguments: " ^ quote c) :: errs';


360 
in


361 
(case assoc (args, c) of


362 
Some n => nargs n


363 
 None =>


364 
(case assoc (abbrs, c) of


365 
Some (vs, _) => nargs (length vs)


366 
 None => undcl_type c :: errs))


367 
end


368 
 typ_errs (TFree (_, S), errs) = sort_err (errs, S)


369 
 typ_errs (TVar (_, S), errs) = sort_err (errs, S); (* FIXME index >= 0 (?) *)


370 
in


371 
typ_errs ty


372 
end;


373 


374 


375 
(* cert_typ *)


376 


377 
(*check and normalize typ wrt. tsig; errors are indicated by exception TYPE*)


378 


379 
fun cert_typ tsig ty =


380 
(case typ_errors tsig (ty, []) of


381 
[] => norm_typ tsig ty


382 
 errs => raise_type (cat_lines errs) [ty] []);


383 


384 


385 


386 
(* 'add_class' adds a new class to the list of all existing classes *)


387 


388 
fun add_class (classes, (s, _)) =

0

389 
if s mem classes then error("Class " ^ s ^ " declared twice.")


390 
else s::classes;


391 


392 
(* 'add_subclass' adds a tuple consisiting of a new class (the new class


393 
has already been inserted into the 'classes' list) and its

256

394 
superclasses (they must be declared in 'classes' too) to the 'subclass'


395 
list of the given type signature;


396 
furthermore all inherited superclasses according to the superclasses

0

397 
brought with are inserted and there is a check that there are no


398 
cycles (i.e. C <= D <= C, with C <> D); *)


399 

256

400 
fun add_subclass classes (subclass, (s, ges)) =


401 
let fun upd (subclass, s') = if s' mem classes then


402 
let val Some(ges') = assoc (subclass, s)


403 
in case assoc (subclass, s') of

0

404 
Some(sups) => if s mem sups


405 
then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s )

256

406 
else overwrite (subclass, (s, sups union ges'))

0

407 
 None => subclass


408 
end

256

409 
else err_undcl_class(s')


410 
in foldl upd (subclass@[(s, ges)], ges) end;

0

411 


412 


413 
(* 'extend_classes' inserts all new classes into the corresponding

256

414 
lists ('classes', 'subclass') if possible *)

0

415 

256

416 
fun extend_classes (classes, subclass, newclasses) =


417 
if newclasses = [] then (classes, subclass) else


418 
let val classes' = foldl add_class (classes, newclasses);


419 
val subclass' = foldl (add_subclass classes') (subclass, newclasses);


420 
in (classes', subclass') end;


421 

0

422 


423 
(* Corregularity *)


424 


425 
(* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *)


426 

256

427 
fun is_unique_decl coreg (t, (s, w)) = case assoc2 (coreg, (t, s)) of

0

428 
Some(w1) => if w = w1 then () else

256

429 
error("There are two declarations\n" ^


430 
str_of_decl(t, w, s) ^ " and\n" ^


431 
str_of_decl(t, w1, s) ^ "\n" ^

0

432 
"with the same result class.")


433 
 None => ();


434 


435 
(* 'restr2' checks if there are two declarations t:(Ss1)C1 and t:(Ss2)C2


436 
such that C1 >= C2 then Ss1 >= Ss2 (elementwise) *)


437 

256

438 
fun subs (classes, subclass) C =


439 
let fun sub (rl, l) = if leq subclass (l, C) then l::rl else rl


440 
in foldl sub ([], classes) end;

0

441 

256

442 
fun coreg_err(t, (w1, C), (w2, D)) =


443 
error("Declarations " ^ str_of_decl(t, w1, C) ^ " and "


444 
^ str_of_decl(t, w2, D) ^ " are in conflict");

0

445 

256

446 
fun restr2 classes (subclass, coreg) (t, (s, w)) =


447 
let fun restr ([], test) = ()


448 
 restr (s1::Ss, test) = (case assoc2 (coreg, (t, s1)) of


449 
Some (dom) => if lew subclass (test (w, dom)) then restr (Ss, test)


450 
else coreg_err (t, (w, s), (dom, s1))


451 
 None => restr (Ss, test))


452 
fun forward (t, (s, w)) =


453 
let val s_sups = case assoc (subclass, s) of


454 
Some(s_sups) => s_sups  None => err_undcl_class(s);


455 
in restr (s_sups, I) end


456 
fun backward (t, (s, w)) =


457 
let val s_subs = subs (classes, subclass) s


458 
in restr (s_subs, fn (x, y) => (y, x)) end


459 
in (backward (t, (s, w)); forward (t, (s, w))) end;

0

460 


461 

256

462 
fun varying_decls t =


463 
error ("Type constructor " ^ quote t ^ " has varying number of arguments");

0

464 


465 


466 
(* 'coregular' checks


467 
 the two restriction conditions 'is_unique_decl' and 'restr2'

256

468 
 if the classes in the new type declarations are known in the

0

469 
given type signature


470 
 if one type constructor has always the same number of arguments;

256

471 
if one type declaration has passed all checks it is inserted into

0

472 
the 'coreg' association list of the given type signatrure *)


473 

256

474 
fun coregular (classes, subclass, args) =


475 
let fun ex C = if C mem classes then () else err_undcl_class(C);

0

476 

256

477 
fun addar(w, C) (coreg, t) = case assoc(args, t) of

0

478 
Some(n) => if n <> length w then varying_decls(t) else

256

479 
(is_unique_decl coreg (t, (C, w));


480 
(seq o seq) ex w;


481 
restr2 classes (subclass, coreg) (t, (C, w));


482 
let val Some(ars) = assoc(coreg, t)


483 
in overwrite(coreg, (t, (C, w) ins ars)) end)


484 
 None => err_undcl_type(t);

0

485 

256

486 
fun addts(coreg, (ts, ar)) = foldl (addar ar) (coreg, ts)

0

487 


488 
in addts end;


489 


490 


491 
(* 'close' extends the 'coreg' association list after all new type


492 
declarations have been inserted successfully:


493 
for every declaration t:(Ss)C , for all classses D with C <= D:


494 
if there is no declaration t:(Ss')C' with C < C' and C' <= D


495 
then insert the declaration t:(Ss)D into 'coreg'


496 
this means, if there exists a declaration t:(Ss)C and there is


497 
no declaration t:(Ss')D with C <=D then the declaration holds

256

498 
for all range classes more general than C *)


499 


500 
fun close (coreg, subclass) =


501 
let fun check sl (l, (s, dom)) = case assoc (subclass, s) of

0

502 
Some(sups) =>

256

503 
let fun close_sup (l, sup) =


504 
if exists (fn s'' => less subclass (s, s'') andalso


505 
leq subclass (s'', sup)) sl

0

506 
then l

256

507 
else (sup, dom)::l


508 
in foldl close_sup (l, sups) end

0

509 
 None => l;

256

510 
fun ext (s, l) = (s, foldl (check (map #1 l)) (l, l));

0

511 
in map ext coreg end;


512 

256

513 
fun add_types(aca, (ts, n)) =


514 
let fun add_type((args, coreg, abbrs), t) = case assoc(args, t) of


515 
Some _ => twice(t)


516 
 None => (case assoc(abbrs, t) of Some _ => tyab_conflict(t)


517 
 None => ((t, n)::args, (t, [])::coreg, abbrs))

0

518 
in if n<0


519 
then error("Type constructor cannot have negative number of arguments")

256

520 
else foldl add_type (aca, ts)

0

521 
end;


522 

256

523 


524 


525 
(* ext_tsig_abbrs *) (* FIXME clean, check, improve *)


526 

200

527 
(* check_abbr *)


528 

256

529 
fun check_abbr ((a, (lhs_vs, U)), tsig as TySg {args, abbrs, ...}) =


530 
let


531 
val rhs_vs = map #1 (add_typ_tvars (U, []));


532 
fun err_abbr a = "Error in type abbreviation " ^ quote a;


533 
in


534 
if not (rhs_vs subset lhs_vs)


535 
then [err_abbr a, ("Extra variables on rhs")] (* FIXME improve *)


536 
else


537 
(case duplicates lhs_vs of


538 
dups as _ :: _ =>


539 
[err_abbr a, "Duplicate variables on lhs: " ^ commas (map (quote o #1) dups)] (* FIXME string_of_vname *)


540 
 [] =>


541 
if is_some (assoc (args, a)) then


542 
[err_abbr a, ("A type with this name already exists")]


543 
else if is_some (assoc (abbrs, a)) then


544 
[err_abbr a, ("An abbreviation with this name already exists")]


545 
else (* FIXME remove (?) or move up! *)


546 
(case typ_errors tsig (U, []) of


547 
[] => []


548 
 errs => err_abbr a :: errs))

200

549 
end;


550 

256

551 
(* FIXME improve *)


552 
(* FIXME set all sorts to [] (?) *)


553 
fun add_abbr (tsig as TySg {classes, default, subclass, args, coreg, abbrs}, newabbr) =


554 
(case check_abbr (newabbr, tsig) of


555 
[] => TySg {classes = classes, default = default, subclass = subclass,


556 
args = args, coreg = coreg, abbrs = newabbr :: abbrs}


557 
 errs => error (cat_lines errs)); (* FIXME error!? *)

200

558 

256

559 
fun ext_tsig_abbrs tsig abbrs = foldl add_abbr (tsig, abbrs);

200

560 


561 

256

562 
(* 'extend_tsig' takes the above described check and extendfunctions to

0

563 
extend a given type signature with new classes and new type declarations *)


564 

256

565 
fun extend_tsig (TySg{classes, default, subclass, args, coreg, abbrs})


566 
(newclasses, newdefault, types, arities) =


567 
let val (classes', subclass') = extend_classes(classes, subclass, newclasses);


568 
val (args', coreg', _) = foldl add_types ((args, coreg, abbrs), types);

0

569 
val old_coreg = map #1 coreg;

256

570 
fun is_old(c) = if c mem old_coreg then () else err_undcl_type(c);

0

571 
fun is_new(c) = if c mem old_coreg then twice(c) else ();

256

572 
val coreg'' = foldl (coregular (classes', subclass', args'))


573 
(coreg', min_domain subclass' arities);


574 
val coreg''' = close (coreg'', subclass');

0

575 
val default' = if null newdefault then default else newdefault;

256

576 
in TySg{classes=classes', default=default', subclass=subclass', args=args',


577 
coreg=coreg''', abbrs=abbrs} end;

0

578 


579 


580 
(* 'assoc_union' merges two association lists if the contents associated


581 
the keys are lists *)


582 

256

583 
fun assoc_union (as1, []) = as1


584 
 assoc_union (as1, (key, l2)::as2) = case assoc (as1, key) of


585 
Some(l1) => assoc_union (overwrite(as1, (key, l1 union l2)), as2)


586 
 None => assoc_union ((key, l2)::as1, as2);

0

587 


588 


589 
fun trcl r =


590 
let val r' = transitive_closure r


591 
in if exists (op mem) r' then error("Cyclic class structure!") else r' end;


592 


593 


594 
(* 'merge_coreg' builds the union of two 'coreg' lists;


595 
it only checks the two restriction conditions and inserts afterwards

256

596 
all elements of the second list into the first one *)

0

597 


598 
fun merge_coreg classes subclass1 =

256

599 
let fun test_ar classes (t, ars1) (coreg1, (s, w)) =


600 
(is_unique_decl coreg1 (t, (s, w));


601 
restr2 classes (subclass1, coreg1) (t, (s, w));


602 
overwrite (coreg1, (t, (s, w) ins ars1)));

0

603 

256

604 
fun merge_c (coreg1, (c as (t, ars2))) = case assoc (coreg1, t) of


605 
Some(ars1) => foldl (test_ar classes (t, ars1)) (coreg1, ars2)

0

606 
 None => c::coreg1


607 
in foldl merge_c end;


608 

256

609 
fun merge_args(args, (t, n)) = case assoc(args, t) of

0

610 
Some(m) => if m=n then args else varying_decls(t)

256

611 
 None => (t, n)::args;

0

612 

256

613 
(* FIXME raise ... *)


614 
fun merge_abbrs (abbrs1, abbrs2) =


615 
let


616 
val abbrs = abbrs1 union abbrs2;


617 
val names = map fst abbrs;


618 
in


619 
(case duplicates names of


620 
[] => abbrs


621 
 dups => error ("Duplicate declaration of type abbreviations: " ^


622 
commas (map quote dups)))


623 
end;

0

624 

256

625 


626 
(* 'merge_tsigs' takes the above declared functions to merge two type signatures *)


627 


628 
fun merge_tsigs(TySg{classes=classes1, default=default1, subclass=subclass1, args=args1,


629 
coreg=coreg1, abbrs=abbrs1},


630 
TySg{classes=classes2, default=default2, subclass=subclass2, args=args2,


631 
coreg=coreg2, abbrs=abbrs2}) =

0

632 
let val classes' = classes1 union classes2;

256

633 
val subclass' = trcl (assoc_union (subclass1, subclass2));


634 
val args' = foldl merge_args (args1, args2)


635 
val coreg' = merge_coreg classes' subclass' (coreg1, coreg2);

200

636 
val default' = min_sort subclass' (default1 @ default2);

256

637 
val abbrs' = merge_abbrs(abbrs1, abbrs2);


638 
in TySg{classes=classes' , default=default', subclass=subclass', args=args',


639 
coreg=coreg' , abbrs = abbrs' }

0

640 
end;


641 

200

642 

0

643 
(**** TYPE INFERENCE ****)


644 


645 
(*


646 


647 
Input:


648 
 a 'raw' term which contains only dummy types and some explicit type


649 
constraints encoded as terms.


650 
 the expected type of the term.


651 


652 
Output:


653 
 the correctly typed term


654 
 the substitution needed to unify the actual type of the term with its


655 
expected type; only the TVars in the expected type are included.


656 


657 
During type inference all TVars in the term have negative index. This keeps


658 
them apart from normal TVars, which is essential, because at the end the type


659 
of the term is unified with the expected type, which contains normal TVars.


660 


661 
1. Add initial type information to the term (add_types).


662 
This freezes (freeze_vars) TVars in explicitly provided types (eg


663 
constraints or defaults) by turning them into TFrees.


664 
2. Carry out type inference, possibly introducing new negative TVars.


665 
3. Unify actual and expected type.


666 
4. Turn all (negative) TVars into unique new TFrees (freeze).


667 
5. Thaw all TVars frozen in step 1 (thaw_vars).


668 


669 
*)


670 


671 
(*Raised if types are not unifiable*)


672 
exception TUNIFY;


673 


674 
val tyvar_count = ref(~1);


675 


676 
fun tyinit() = (tyvar_count := ~1);


677 


678 
fun new_tvar_inx() = (tyvar_count := !tyvar_count1; !tyvar_count)


679 


680 
(*


681 
Generate new TVar. Index is < ~1 to distinguish it from TVars generated from


682 
variable names (see id_type). Name is arbitrary because index is new.


683 
*)


684 

256

685 
fun gen_tyvar(S) = TVar(("'a", new_tvar_inx()), S);

0

686 


687 
(*Occurs check: type variable occurs in type?*)


688 
fun occ v tye =

256

689 
let fun occ(Type(_, Ts)) = exists occ Ts

0

690 
 occ(TFree _) = false

256

691 
 occ(TVar(w, _)) = v=w orelse


692 
(case assoc(tye, w) of

0

693 
None => false


694 
 Some U => occ U);


695 
in occ end;


696 

256

697 
(*Chase variable assignments in tye.


698 
If devar (T, tye) returns a type var then it must be unassigned.*)


699 
fun devar (T as TVar(v, _), tye) = (case assoc(tye, v) of


700 
Some U => devar (U, tye)

0

701 
 None => T)

256

702 
 devar (T, tye) = T;

0

703 


704 


705 
(* 'dom' returns for a type constructor t the list of those domains


706 
which deliver a given range class C *)


707 

256

708 
fun dom coreg t C = case assoc2 (coreg, (t, C)) of

0

709 
Some(Ss) => Ss


710 
 None => raise TUNIFY;


711 


712 


713 
(* 'Dom' returns the union of all domain lists of 'dom' for a given sort S


714 
(i.e. a set of range classes ); the union is carried out elementwise


715 
for the seperate sorts in the domains *)


716 

256

717 
fun Dom (subclass, coreg) (t, S) =

0

718 
let val domlist = map (dom coreg t) S;


719 
in if null domlist then []

256

720 
else foldl (elementwise_union subclass) (hd domlist, tl domlist)

0

721 
end;


722 


723 

256

724 
fun W ((T, S), tsig as TySg{subclass, coreg, ...}, tye) =


725 
let fun Wd ((T, S), tye) = W ((devar (T, tye), S), tsig, tye)


726 
fun Wk(T as TVar(v, S')) =


727 
if sortorder subclass (S', S) then tye


728 
else (v, gen_tyvar(union_sort subclass (S', S)))::tye


729 
 Wk(T as TFree(v, S')) = if sortorder subclass (S', S) then tye


730 
else raise TUNIFY


731 
 Wk(T as Type(f, Ts)) =


732 
if null S then tye


733 
else foldr Wd (Ts~~(Dom (subclass, coreg) (f, S)) , tye)

0

734 
in Wk(T) end;


735 


736 


737 
(* Ordersorted Unification of Types (U) *)


738 


739 
(* Precondition: both types are wellformed w.r.t. type constructor arities *)

256

740 
fun unify (tsig as TySg{subclass, coreg, ...}) =


741 
let fun unif ((T, U), tye) =


742 
case (devar(T, tye), devar(U, tye)) of


743 
(T as TVar(v, S1), U as TVar(w, S2)) =>

0

744 
if v=w then tye else

256

745 
if sortorder subclass (S1, S2) then (w, T)::tye else


746 
if sortorder subclass (S2, S1) then (v, U)::tye


747 
else let val nu = gen_tyvar (union_sort subclass (S1, S2))


748 
in (v, nu)::(w, nu)::tye end


749 
 (T as TVar(v, S), U) =>


750 
if occ v tye U then raise TUNIFY else W ((U, S), tsig, (v, U)::tye)


751 
 (U, T as TVar (v, S)) =>


752 
if occ v tye U then raise TUNIFY else W ((U, S), tsig, (v, U)::tye)


753 
 (Type(a, Ts), Type(b, Us)) =>


754 
if a<>b then raise TUNIFY else foldr unif (Ts~~Us, tye)


755 
 (T, U) => if T=U then tye else raise TUNIFY

0

756 
in unif end;


757 


758 


759 
(*Type inference for polymorphic term*)


760 
fun infer tsig =

256

761 
let fun inf(Ts, Const (_, T), tye) = (T, tye)


762 
 inf(Ts, Free (_, T), tye) = (T, tye)


763 
 inf(Ts, Bound i, tye) = ((nth_elem(i, Ts) , tye)

0

764 
handle LIST _=> raise TYPE ("loose bound variable", [], [Bound i]))

256

765 
 inf(Ts, Var (_, T), tye) = (T, tye)


766 
 inf(Ts, Abs (_, T, body), tye) =


767 
let val (U, tye') = inf(T::Ts, body, tye) in (T>U, tye') end

0

768 
 inf(Ts, f$u, tye) =

256

769 
let val (U, tyeU) = inf(Ts, u, tye);


770 
val (T, tyeT) = inf(Ts, f, tyeU);

0

771 
fun err s =


772 
raise TYPE(s, [inst_typ tyeT T, inst_typ tyeT U], [f$u])

256

773 
in case T of


774 
Type("fun", [T1, T2]) =>


775 
( (T2, unify tsig ((T1, U), tyeT))

0

776 
handle TUNIFY => err"type mismatch in application" )

256

777 
 TVar _ =>

0

778 
let val T2 = gen_tyvar([])


779 
in (T2, unify tsig ((T, U>T2), tyeT))


780 
handle TUNIFY => err"type mismatch in application"


781 
end


782 
 _ => err"rator must have function type"


783 
end


784 
in inf end;


785 

256

786 
fun freeze_vars(Type(a, Ts)) = Type(a, map freeze_vars Ts)

0

787 
 freeze_vars(T as TFree _) = T

256

788 
 freeze_vars(TVar(v, S)) = TFree(Syntax.string_of_vname v, S);

0

789 


790 
(* Attach a type to a constant *)

256

791 
fun type_const (a, T) = Const(a, incr_tvar (new_tvar_inx()) T);

0

792 


793 
(*Find type of ident. If not in table then use ident's name for tyvar


794 
to get consistent typing.*)

256

795 
fun new_id_type a = TVar(("'"^a, new_tvar_inx()), []);


796 
fun type_of_ixn(types, ixn as (a, _)) =


797 
case types ixn of Some T => freeze_vars T  None => TVar(("'"^a, ~1), []);

0

798 

256

799 
fun constrain(term, T) = Const(Syntax.constrainC, T>T) $ term;


800 
fun constrainAbs(Abs(a, _, body), T) = Abs(a, T, body);


801 

0

802 


803 
(*

256

804 
Attach types to a term. Input is a "parse tree" containing dummy types.


805 
Type constraints are translated and checked for validity wrt tsig. TVars in


806 
constraints are frozen.

0

807 

256

808 
The atoms in the resulting term satisfy the following spec:

0

809 

256

810 
Const (a, T):


811 
T is a renamed copy of the generic type of a; renaming decreases index of


812 
all TVars by new_tvar_inx(), which is less than ~1. The index of all


813 
TVars in the generic type must be 0 for this to work!

0

814 

256

815 
Free (a, T), Var (ixn, T):


816 
T is either the frozen default type of a or TVar (("'"^a, ~1), [])

0

817 

256

818 
Abs (a, T, _):


819 
T is either a type constraint or TVar (("'" ^ a, i), []), where i is


820 
generated by new_tvar_inx(). Thus different abstractions can have the


821 
bound variables of the same name but different types.

0

822 
*)


823 

256

824 
(* FIXME replace const_tab by (const_typ: string > typ option) (?) *)


825 
(* FIXME improve handling of sort constraints *)


826 


827 
fun add_types (tsig, const_tab, types, sorts) =


828 
let


829 
val S0 = defaultS tsig;


830 
fun defS0 ixn = if_none (sorts ixn) S0;


831 


832 
fun prepareT typ =


833 
freeze_vars (cert_typ tsig (Syntax.typ_of_term defS0 typ));


834 


835 
fun add (Const (a, _)) =


836 
(case Symtab.lookup (const_tab, a) of


837 
Some T => type_const (a, T)


838 
 None => raise_type ("No such constant: " ^ quote a) [] [])


839 
 add (Bound i) = Bound i


840 
 add (Free (a, _)) =


841 
(case Symtab.lookup (const_tab, a) of


842 
Some T => type_const (a, T)


843 
 None => Free (a, type_of_ixn (types, (a, ~1))))


844 
 add (Var (ixn, _)) = Var (ixn, type_of_ixn (types, ixn))


845 
 add (Abs (a, _, body)) = Abs (a, new_id_type a, add body)


846 
 add ((f as Const (a, _) $ t1) $ t2) =


847 
if a = Syntax.constrainC then


848 
constrain (add t1, prepareT t2)


849 
else if a = Syntax.constrainAbsC then


850 
constrainAbs (add t1, prepareT t2)


851 
else add f $ add t2


852 
 add (f $ t) = add f $ add t;


853 
in add end;

0

854 


855 


856 
(* PostProcessing *)


857 


858 


859 
(*Instantiation of type variables in terms*)


860 
fun inst_types tye = map_term_types (inst_typ tye);


861 


862 
(*Delete explicit constraints  occurrences of "_constrain" *)

256

863 
fun unconstrain (Abs(a, T, t)) = Abs(a, T, unconstrain t)


864 
 unconstrain ((f as Const(a, _)) $ t) =

0

865 
if a=Syntax.constrainC then unconstrain t


866 
else unconstrain f $ unconstrain t


867 
 unconstrain (f$t) = unconstrain f $ unconstrain t


868 
 unconstrain (t) = t;


869 


870 


871 
(* Turn all TVars which satisfy p into new TFrees *)


872 
fun freeze p t =

256

873 
let val fs = add_term_tfree_names(t, []);


874 
val inxs = filter p (add_term_tvar_ixns(t, []));

0

875 
val vmap = inxs ~~ variantlist(map #1 inxs, fs);

256

876 
fun free(Type(a, Ts)) = Type(a, map free Ts)


877 
 free(T as TVar(v, S)) =


878 
(case assoc(vmap, v) of None => T  Some(a) => TFree(a, S))

0

879 
 free(T as TFree _) = T


880 
in map_term_types free t end;


881 


882 
(* Thaw all TVars that were frozen in freeze_vars *)

256

883 
fun thaw_vars(Type(a, Ts)) = Type(a, map thaw_vars Ts)


884 
 thaw_vars(T as TFree(a, S)) = (case explode a of


885 
"?"::"'"::vn => let val ((b, i), _) = Syntax.scan_varname vn


886 
in TVar(("'"^b, i), S) end


887 
 _ => T)

0

888 
 thaw_vars(T) = T;


889 


890 


891 
fun restrict tye =

256

892 
let fun clean(tye1, ((a, i), T)) =


893 
if i < 0 then tye1 else ((a, i), inst_typ tye T) :: tye1


894 
in foldl clean ([], tye) end

0

895 


896 


897 
(*Infer types for term t using tables. Check that t's type and T unify *)


898 

256

899 
fun infer_term (tsig, const_tab, types, sorts, T, t) =


900 
let val u = add_types (tsig, const_tab, types, sorts) t;


901 
val (U, tye) = infer tsig ([], u, []);

0

902 
val uu = unconstrain u;

256

903 
val tye' = unify tsig ((T, U), tye) handle TUNIFY => raise TYPE


904 
("Term does not have expected type", [T, U], [inst_types tye uu])

0

905 
val Ttye = restrict tye' (* restriction to TVars in T *)


906 
val all = Const("", Type("", map snd Ttye)) $ (inst_types tye' uu)


907 
(* all is a dummy term which contains all exported TVars *)

256

908 
val Const(_, Type(_, Ts)) $ u'' =


909 
map_term_types thaw_vars (freeze (fn (_, i) => i<0) all)

0

910 
(* turn all internally generated TVars into TFrees


911 
and thaw all initially frozen TVars *)


912 
in (u'', (map fst Ttye) ~~ Ts) end;


913 


914 
fun infer_types args = (tyinit(); infer_term args);


915 


916 


917 
(* Turn TFrees into TVars to allow types & axioms to be written without "?" *)

256

918 
fun varifyT (Type (a, Ts)) = Type (a, map varifyT Ts)


919 
 varifyT (TFree (a, S)) = TVar ((a, 0), S)


920 
 varifyT T = T;

0

921 


922 
(* Turn TFrees except those in fixed into new TVars *)

256

923 
fun varify (t, fixed) =


924 
let val fs = add_term_tfree_names(t, []) \\ fixed;


925 
val ixns = add_term_tvar_ixns(t, []);

0

926 
val fmap = fs ~~ variantlist(fs, map #1 ixns)

256

927 
fun thaw(Type(a, Ts)) = Type(a, map thaw Ts)

0

928 
 thaw(T as TVar _) = T

256

929 
 thaw(T as TFree(a, S)) =


930 
(case assoc(fmap, a) of None => T  Some b => TVar((b, 0), S))

0

931 
in map_term_types thaw t end;


932 


933 


934 
end;

256

935 
