0

1 
(* Title: Types and Sorts

200

2 
Author: Tobias Nipkow & Lawrence C Paulson

0

3 
ID: $Id$


4 


5 
Maybe type classes should go in a separate module?


6 
*)


7 


8 


9 
signature TYPE =


10 
sig


11 
structure Symtab:SYMTAB


12 
type type_sig

200

13 
val rep_tsig: type_sig >


14 
{classes: class list, default: sort,


15 
subclass: (class * class list) list,


16 
args: (string * int) list,


17 
coreg: (string * (class * sort list) list) list,


18 
abbr: (string * (indexname list * typ) ) list}

0

19 
val defaultS: type_sig > sort

200

20 
val add_abbrs : type_sig * (string * (indexname list * typ)) list


21 
> type_sig


22 
val expand_typ: type_sig > typ > typ

0

23 
val extend: type_sig * (class * class list)list * sort *


24 
(string list * int)list *


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


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


27 
val freeze_vars: typ > typ


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


29 
(indexname > sort option) * (typ > string) * typ * term


30 
> term * (indexname*typ)list


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


32 
val logical_type: type_sig > string > bool

189

33 
val logical_types: type_sig > string list

0

34 
val merge: type_sig * type_sig > type_sig


35 
val thaw_vars: typ > typ


36 
val tsig0: type_sig

200

37 
val type_errors: type_sig > typ * string list > string list

0

38 
val typ_instance: type_sig * typ * typ > bool


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


40 
(indexname*typ)list


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


42 
val varifyT: typ > typ


43 
val varify: term * string list > term


44 
exception TUNIFY


45 
exception TYPE_MATCH;


46 
end;


47 

200

48 
functor TypeFun(structure Symtab:SYMTAB and Syntax:SYNTAX) (*: TYPE*) =

0

49 
struct


50 
structure Symtab = Symtab


51 


52 
(* Miscellany *)


53 


54 
val commas = space_implode ",";


55 
fun str_of_sort S = "{" ^ commas S ^ "}";


56 
fun str_of_dom dom = "(" ^ commas (map str_of_sort dom) ^ ")";


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


58 


59 


60 
(* Association list Manipulation *)


61 


62 


63 
(* twofold Association list lookup *)


64 


65 
fun assoc2 (aal,(key1,key2)) = case assoc (aal,key1) of


66 
Some (al) => assoc (al,key2)


67 
 None => None;


68 


69 


70 


71 
(**** TYPE CLASSES ****)


72 


73 
type domain = sort list;


74 
type arity = domain * class;


75 


76 
datatype type_sig =


77 
TySg of {classes: class list,


78 
default: sort,


79 
subclass: (class * class list) list,


80 
args: (string * int) list,

200

81 
coreg: (string * (class * domain) list) list,


82 
abbr: (string * (indexname list * typ) ) list };

0

83 


84 
(* classes: a list of all declared classes;


85 
default: the default sort attached to all unconstrained TVars


86 
occurring in a term to be typeinferred;


87 
subclass: association list representation of subclass relationship;


88 
(c,cs) is interpreted as "c is a proper subclass of all


89 
elemenst of cs". Note that c itself is not a memeber of cs.


90 
args: an association list of all declared types with the number of their


91 
arguments


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


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


94 
represents the arity (ss)c

200

95 
abbr: an association list of type abbreviations

0

96 
*)


97 

189

98 
fun rep_tsig (TySg comps) = comps;

200

99 

0

100 


101 
val tsig0 = TySg{classes = [],


102 
default = [],


103 
subclass = [],


104 
args = [],

200

105 
coreg = [],


106 
abbr = []};

0

107 


108 
fun undcl_class (s) = error("Class " ^ s ^ " has not been declared");


109 


110 
fun undcl_type(c) = "Undeclared type: " ^ c;


111 
fun undcl_type_err(c) = error(undcl_type(c));


112 


113 


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


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


116 
*)


117 


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


119 
Some(ss) => D mem ss


120 
 None => undcl_class (C) ;


121 


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


123 


124 


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


126 


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


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


129 


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


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


132 
in case assoc (coreg,t) of


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


134 
 None => undcl_type_err(t)


135 
end;


136 

162

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


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


139 

0

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


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


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


143 
*)


144 


145 
fun sortorder a (S1,S2) =


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


147 


148 


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


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


151 
the resulting set is minimal if S was minimal


152 
*)


153 


154 
fun inj a (C,S) =


155 
let fun inj1 [] = [C]


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


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


158 
else D::(inj1 T)


159 
in inj1 S end;


160 


161 


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


163 
under the assumption that S2 is minimal *)


164 


165 
fun union_sort a = foldr (inj a);


166 


167 


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


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


170 
*)


171 


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


173 


174 


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


176 
elements (i.e. sorts) *)


177 


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


179 


180 


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


182 
assumption that S contains C *)


183 


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


185 


186 


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


188 


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


190 


191 


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


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


194 


195 
fun min_domain subclass =


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


197 
in map one_min end;


198 


199 


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


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


202 
predicate 'pred' *)


203 


204 
fun min_filter a pred ars =


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


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


207 
else filt (xs,l)


208 
in filt (ars,[]) end;


209 


210 


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


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


213 
classes *)


214 


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


216 

200

217 
(*Instantiation of type variables in types*)


218 
(*Pre: instantiations obey restrictions! *)


219 
fun inst_typ tye =


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


221 
 inst(T as TFree _) = T


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


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


224 
in inst end;

0

225 


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


227 
 type variables, free types: the sort brought with


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


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


230 
given type signature *)


231 

200

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

0

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

200

234 
(case assoc(abbr,a) of


235 
Some(v,U) => ls(inst_typ(v~~Ts) U)


236 
 None => (case assoc (coreg,a) of


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


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

0

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


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


241 
in ls end;


242 


243 


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


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


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


247 


248 


249 
(*Instantiation of type variables in types *)


250 
fun inst_typ_tvars(tsig,tye) =


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


252 
 inst(T as TFree _) = T


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


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


255 
in inst end;


256 


257 
(*Instantiation of type variables in terms *)


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


259 

200

260 


261 
(* expand1_typ *)


262 


263 
fun expand1_typ(abbr,a,Ts) =


264 
( case assoc(abbr,a) of Some(v,U) => Some(inst_typ(v~~Ts) U)


265 
 None => None );


266 


267 
(* expand_typ *)


268 


269 
fun expand_typ(tsig as TySg{abbr,...}) =


270 
let fun exptyp(Type(a,Ts)) =


271 
( case assoc(abbr,a) of


272 
Some (v,U) => exptyp(inst_typ(v~~Ts) U)


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


274 
 exptyp(T) = T


275 
in exptyp end;


276 

0

277 
exception TYPE_MATCH;


278 


279 
(* Typ matching


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

200

281 
fun typ_match (tsig as TySg{abbr,...}) =

0

282 
let fun tm(subs, (TVar(v,S), T)) = (case assoc(subs,v) of


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


284 
handle TYPE _ => raise TYPE_MATCH )

200

285 
 Some(U) => if expand_typ tsig U = expand_typ tsig T


286 
then subs


287 
else raise TYPE_MATCH)


288 
 tm(subs, (T as Type(a,Ts), U as Type(b,Us))) =


289 
if a<>b then


290 
(case (expand1_typ(abbr,a,Ts), expand1_typ(abbr,b,Us)) of


291 
(None,None) => raise TYPE_MATCH


292 
 (None,Some(U)) => tm(subs,(T,U))


293 
 (Some(T),None) => tm(subs,(T,U))


294 
 (Some(T),Some(U)) => tm(subs,(T,U)))

0

295 
else foldl tm (subs, Ts~~Us)


296 
 tm(subs, (TFree(x), TFree(y))) =


297 
if x=y then subs else raise TYPE_MATCH


298 
 tm _ = raise TYPE_MATCH


299 
in tm end;


300 


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


302 
handle TYPE_MATCH => false;


303 


304 


305 
(* EXTENDING AND MERGIN TYPE SIGNATURES *)


306 


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


308 


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


310 

200

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


312 

0

313 
(*Is the type valid? Accumulates error messages in "errs".*)

200

314 
fun type_errors (tsig as TySg{classes,args,abbr,...}) =


315 
let fun class_err(errs,C) =


316 
if C mem classes then errs


317 
else ("Class " ^ quote C ^ " has not been declared") :: errs


318 
val sort_err = foldl class_err


319 
fun errors(Type(c,Us), errs) =

0

320 
let val errs' = foldr errors (Us,errs)

200

321 
fun nargs n = if n=length(Us) then errs'


322 
else ("Wrong number of arguments: " ^ c) :: errs'

0

323 
in case assoc(args,c) of

200

324 
Some(n) => nargs n


325 
 None => (case assoc(abbr,c) of


326 
Some(v,_) => nargs(length v)


327 
 None => (undcl_type c) :: errs)

0

328 
end

200

329 
 errors(TFree(_,S), errs) = sort_err(errs,S)


330 
 errors(TVar(_,S), errs) = sort_err(errs,S)


331 
in errors end;

0

332 


333 


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


335 


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


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


338 
else s::classes;


339 


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


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


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


343 
list of the given type signature;


344 
furthermore all inherited superclasses according to the superclasses


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


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


347 


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


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


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


351 
in case assoc (subclass,s') of


352 
Some(sups) => if s mem sups


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


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


355 
 None => subclass


356 
end


357 
else undcl_class(s')


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


359 


360 


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


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


363 


364 
fun extend_classes (classes,subclass,newclasses) =


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


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


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


368 
in (classes',subclass') end;


369 


370 
(* Corregularity *)


371 


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


373 


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


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


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


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


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


379 
"with the same result class.")


380 
 None => ();


381 


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


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


384 


385 
fun subs (classes,subclass) C =


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


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


388 


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


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


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


392 


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


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


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


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


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


398 
 None => restr (Ss,test))


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


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


401 
Some(s_sups) => s_sups  None => undcl_class(s);


402 
in restr (s_sups,I) end


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


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


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


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


407 


408 


409 
fun varying_decls(t) =


410 
error("Type constructor "^t^" has varying number of arguments.");


411 


412 


413 


414 
(* 'coregular' checks


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


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


417 
given type signature


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


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


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


421 


422 
fun coregular (classes,subclass,args) =


423 
let fun ex C = if C mem classes then () else undcl_class(C);


424 


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


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


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


428 
(seq o seq) ex w;


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


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


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


432 
 None => undcl_type_err(t);


433 


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


435 


436 
in addts end;


437 


438 


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


440 
declarations have been inserted successfully:


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


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


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


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


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


446 
for all range classes more general than C *)


447 


448 
fun close (coreg,subclass) =


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


450 
Some(sups) =>


451 
let fun close_sup (l,sup) =


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


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


454 
then l


455 
else (sup,dom)::l


456 
in foldl close_sup (l,sups) end


457 
 None => l;


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


459 
in map ext coreg end;


460 

200

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


462 
let fun add_type((args,coreg,abbr),t) = case assoc(args,t) of


463 
Some _ => twice(t)


464 
 None => (case assoc(abbr,t) of Some _ => tyab_conflict(t)


465 
 None => ((t,n)::args,(t,[])::coreg,abbr))

0

466 
in if n<0


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

200

468 
else foldl add_type (aca,ts)

0

469 
end;


470 

200

471 
(* check_abbr *)


472 


473 
fun check_abbr( (a,(vs,U)), tsig as TySg{abbr,args,...} ) =


474 
let val (ndxname,_) = split_list(add_typ_tvars(U,[]))


475 
fun err_abbr a = ("ERROR in abbreviation "^ quote a)


476 
in if not( (ndxname subset vs) andalso (vs subset ndxname) )


477 
then [err_abbr a,("Not the same set of variables on lhs and rhs")]


478 
else


479 
(case findrep(vs) of


480 
(v,_)::_ => [err_abbr a,("Variable "^v^" occurs twice on lhs")]


481 
[] =>


482 
(case assoc(args,a) of


483 
Some _ => [err_abbr a,("A type with this name exists already")]


484 
None =>


485 
(case assoc(abbr,a) of


486 
Some _ => [err_abbr a,("An abbreviation with this name exists already")]


487 
None =>


488 
(case type_errors (tsig) (U,[]) of


489 
[] => []


490 
errs => (err_abbr a) :: errs


491 
)


492 
)


493 
)


494 
)


495 
end;


496 


497 
(* add_abbrs *)


498 


499 
fun add_abbr (tsig as TySg{classes,default,subclass,args,coreg,abbr},


500 
newabbr) =


501 
case check_abbr (newabbr,tsig) of


502 
[] => TySg{classes=classes,default=default,subclass=subclass,args=args,


503 
coreg=coreg, abbr = (newabbr) :: abbr}


504 
 errs => error(cat_lines errs) ;


505 


506 
val add_abbrs = foldl add_abbr;


507 


508 

0

509 
(* 'extend' takes the above described check and extendfunctions to


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


511 

200

512 
fun extend (TySg{classes,default,subclass,args,coreg,abbr},

0

513 
newclasses,newdefault,types,arities) =


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

200

515 
val (args',coreg',_) = foldl add_types ((args,coreg,abbr),types);

0

516 
val old_coreg = map #1 coreg;


517 
fun is_old(c) = if c mem old_coreg then () else undcl_type_err(c);


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


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


520 
(coreg',min_domain subclass' arities);


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


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


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

200

524 
coreg=coreg''',abbr=abbr} end;

0

525 


526 


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


528 
the keys are lists *)


529 


530 
fun assoc_union (as1,[]) = as1


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


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


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


534 


535 


536 
fun trcl r =


537 
let val r' = transitive_closure r


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


539 


540 


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


542 
it only checks the two restriction conditions and inserts afterwards


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


544 


545 
fun merge_coreg classes subclass1 =


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


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


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


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


550 


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


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


553 
 None => c::coreg1


554 
in foldl merge_c end;


555 


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


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


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


559 

200

560 
fun merge_abbrs(abbr1,abbr2) =


561 
let val abbru = abbr1 union abbr2


562 
val names = map fst abbru


563 
in ( case findrep names of


564 
[] => abbru


565 
a::_ => error("ERROR in Type.merge: abbreviation "^a^" declared twice") ) end;


566 

0

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


568 


569 
fun merge(TySg{classes=classes1,default=default1,subclass=subclass1,args=args1,

200

570 
coreg=coreg1,abbr=abbr1},

0

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

200

572 
coreg=coreg2,abbr=abbr2}) =

0

573 
let val classes' = classes1 union classes2;


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


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


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

200

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


578 
val abbr' = merge_abbrs(abbr1, abbr2);

0

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

200

580 
coreg=coreg' , abbr = abbr' }

0

581 
end;


582 

200

583 

0

584 
(**** TYPE INFERENCE ****)


585 


586 
(*


587 


588 
Input:


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


590 
constraints encoded as terms.


591 
 the expected type of the term.


592 


593 
Output:


594 
 the correctly typed term


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


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


597 


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


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


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


601 


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


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


604 
constraints or defaults) by turning them into TFrees.


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


606 
3. Unify actual and expected type.


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


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


609 


610 
*)


611 


612 
(*Raised if types are not unifiable*)


613 
exception TUNIFY;


614 


615 
val tyvar_count = ref(~1);


616 


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


618 


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


620 


621 
(*


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


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


624 
*)


625 


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


627 


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


629 
fun occ v tye =


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


631 
 occ(TFree _) = false


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


633 
(case assoc(tye,w) of


634 
None => false


635 
 Some U => occ U);


636 
in occ end;


637 


638 
(*Chase variable assignments in tye.


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


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


641 
Some U => devar (U,tye)


642 
 None => T)


643 
 devar (T,tye) = T;


644 


645 


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


647 
which deliver a given range class C *)


648 


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


650 
Some(Ss) => Ss


651 
 None => raise TUNIFY;


652 


653 


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


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


656 
for the seperate sorts in the domains *)


657 


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


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


660 
in if null domlist then []


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


662 
end;


663 


664 


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


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


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


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


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


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


671 
else raise TUNIFY


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


673 
if null S then tye


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


675 
in Wk(T) end;


676 


677 


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


679 


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

200

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

0

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


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


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


685 
if v=w then tye else


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


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


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


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


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


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


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


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

200

694 
 (T as Type(a,Ts),U as Type(b,Us)) =>


695 
if a<>b then


696 
(case (expand1_typ(abbr,a,Ts), expand1_typ(abbr,b,Us)) of


697 
(None,None) => raise TUNIFY


698 
 (None,Some(U)) => unif((T,U),tye)


699 
 (Some(T),None) => unif((T,U),tye)


700 
 (Some(T),Some(U)) => unif((T,U),tye))


701 
else foldr unif (Ts~~Us,tye)

0

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


703 
in unif end;


704 


705 


706 
(*Type inference for polymorphic term*)


707 
fun infer tsig =


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


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


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


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


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


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


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


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


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


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


718 
fun err s =


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


720 
in case T of


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


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


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


724 
 TVar _ =>


725 
let val T2 = gen_tyvar([])


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


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


728 
end


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


730 
end


731 
in inf end;


732 


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


734 
 freeze_vars(T as TFree _) = T


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


736 


737 
(* Attach a type to a constant *)


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


739 


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


741 
to get consistent typing.*)

200

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

0

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

200

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

0

745 


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


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


748 


749 
(*


750 


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


752 
Type constraints are translated and checked for validity wrt tsig.


753 
TVars in constraints are frozen.


754 


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


756 


757 
Const(a,T):


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


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


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


761 


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


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


764 


765 
Abs(a,T,_):


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


767 
by new_tvar_inx(). Thus different abstractions can have the bound variables


768 
of the same name but different types.


769 


770 
*)


771 


772 
fun add_types (tsig, const_tab, types, sorts, string_of_typ) =


773 
let val S0 = defaultS tsig;


774 
fun defS0 ixn = case sorts ixn of Some S => S  None => S0;


775 
fun prepareT(typ) =


776 
let val T = Syntax.typ_of_term defS0 typ;


777 
val T' = freeze_vars T

200

778 
in case type_errors (tsig) (T,[]) of

0

779 
[] => T'


780 
 errs => raise TYPE(cat_lines errs,[T],[])


781 
end


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


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


784 
Some T => type_const(a,T)


785 
 None => raise TYPE ("No such constant: "^a, [], []))


786 
 add (Bound i) = Bound i


787 
 add (Free(a,_)) =


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


789 
Some T => type_const(a,T)


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


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


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


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


794 
if a=Syntax.constrainC then constrain(add t1,prepareT t2) else


795 
if a=Syntax.constrainAbsC then constrainAbs(add t1,prepareT t2)


796 
else add f $ add t2


797 
 add (f$t) = add f $ add t


798 
in add end;


799 


800 


801 
(* PostProcessing *)


802 


803 


804 
(*Instantiation of type variables in terms*)


805 
fun inst_types tye = map_term_types (inst_typ tye);


806 


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


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


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


810 
if a=Syntax.constrainC then unconstrain t


811 
else unconstrain f $ unconstrain t


812 
 unconstrain (f$t) = unconstrain f $ unconstrain t


813 
 unconstrain (t) = t;


814 


815 


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


817 
fun freeze p t =


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


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


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


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


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


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


824 
 free(T as TFree _) = T


825 
in map_term_types free t end;


826 


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


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


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


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


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


832 
 _ => T)


833 
 thaw_vars(T) = T;


834 


835 


836 
fun restrict tye =


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


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


839 
in foldl clean ([],tye) end


840 


841 


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


843 


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


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


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


847 
val uu = unconstrain u;


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


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


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


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


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


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


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


855 
(* turn all internally generated TVars into TFrees


856 
and thaw all initially frozen TVars *)


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


858 


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


860 


861 


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


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


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


865 
 varifyT(T) = T;


866 


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


868 
fun varify(t,fixed) =


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


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


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


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


873 
 thaw(T as TVar _) = T


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


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


876 
in map_term_types thaw t end;


877 


878 


879 
end;
