clasohm@0: (* Title: Types and Sorts nipkow@200: Author: Tobias Nipkow & Lawrence C Paulson clasohm@0: ID: $Id$ clasohm@0: clasohm@0: Maybe type classes should go in a separate module? clasohm@0: *) clasohm@0: clasohm@0: clasohm@0: signature TYPE = clasohm@0: sig clasohm@0: structure Symtab:SYMTAB clasohm@0: type type_sig nipkow@200: val rep_tsig: type_sig -> nipkow@200: {classes: class list, default: sort, nipkow@200: subclass: (class * class list) list, nipkow@200: args: (string * int) list, nipkow@200: coreg: (string * (class * sort list) list) list, nipkow@200: abbr: (string * (indexname list * typ) ) list} clasohm@0: val defaultS: type_sig -> sort nipkow@200: val add_abbrs : type_sig * (string * (indexname list * typ)) list nipkow@200: -> type_sig nipkow@200: val expand_typ: type_sig -> typ -> typ clasohm@0: val extend: type_sig * (class * class list)list * sort * clasohm@0: (string list * int)list * clasohm@0: (string list * (sort list * class))list -> type_sig clasohm@0: val freeze: (indexname -> bool) -> term -> term clasohm@0: val freeze_vars: typ -> typ clasohm@0: val infer_types: type_sig * typ Symtab.table * (indexname -> typ option) * clasohm@0: (indexname -> sort option) * (typ -> string) * typ * term clasohm@0: -> term * (indexname*typ)list clasohm@0: val inst_term_tvars: type_sig * (indexname * typ)list -> term -> term clasohm@0: val logical_type: type_sig -> string -> bool nipkow@189: val logical_types: type_sig -> string list clasohm@0: val merge: type_sig * type_sig -> type_sig clasohm@0: val thaw_vars: typ -> typ clasohm@0: val tsig0: type_sig nipkow@200: val type_errors: type_sig -> typ * string list -> string list clasohm@0: val typ_instance: type_sig * typ * typ -> bool clasohm@0: val typ_match: type_sig -> (indexname*typ)list * (typ*typ) -> clasohm@0: (indexname*typ)list clasohm@0: val unify: type_sig -> (typ*typ) * (indexname*typ)list -> (indexname*typ)list clasohm@0: val varifyT: typ -> typ clasohm@0: val varify: term * string list -> term clasohm@0: exception TUNIFY clasohm@0: exception TYPE_MATCH; clasohm@0: end; clasohm@0: nipkow@200: functor TypeFun(structure Symtab:SYMTAB and Syntax:SYNTAX) (*: TYPE*) = clasohm@0: struct clasohm@0: structure Symtab = Symtab clasohm@0: clasohm@0: (* Miscellany *) clasohm@0: clasohm@0: val commas = space_implode ","; clasohm@0: fun str_of_sort S = "{" ^ commas S ^ "}"; clasohm@0: fun str_of_dom dom = "(" ^ commas (map str_of_sort dom) ^ ")"; clasohm@0: fun str_of_decl(t,w,C) = t ^ ": " ^ str_of_dom w ^ C; clasohm@0: clasohm@0: clasohm@0: (* Association list Manipulation *) clasohm@0: clasohm@0: clasohm@0: (* two-fold Association list lookup *) clasohm@0: clasohm@0: fun assoc2 (aal,(key1,key2)) = case assoc (aal,key1) of clasohm@0: Some (al) => assoc (al,key2) clasohm@0: | None => None; clasohm@0: clasohm@0: clasohm@0: clasohm@0: (**** TYPE CLASSES ****) clasohm@0: clasohm@0: type domain = sort list; clasohm@0: type arity = domain * class; clasohm@0: clasohm@0: datatype type_sig = clasohm@0: TySg of {classes: class list, clasohm@0: default: sort, clasohm@0: subclass: (class * class list) list, clasohm@0: args: (string * int) list, nipkow@200: coreg: (string * (class * domain) list) list, nipkow@200: abbr: (string * (indexname list * typ) ) list }; clasohm@0: clasohm@0: (* classes: a list of all declared classes; clasohm@0: default: the default sort attached to all unconstrained TVars clasohm@0: occurring in a term to be type-inferred; clasohm@0: subclass: association list representation of subclass relationship; clasohm@0: (c,cs) is interpreted as "c is a proper subclass of all clasohm@0: elemenst of cs". Note that c itself is not a memeber of cs. clasohm@0: args: an association list of all declared types with the number of their clasohm@0: arguments clasohm@0: coreg: a two-fold association list of all type arities; (t,al) means that clasohm@0: type constructor t has the arities in al; an element (c,ss) of al clasohm@0: represents the arity (ss)c nipkow@200: abbr: an association list of type abbreviations clasohm@0: *) clasohm@0: nipkow@189: fun rep_tsig (TySg comps) = comps; nipkow@200: clasohm@0: clasohm@0: val tsig0 = TySg{classes = [], clasohm@0: default = [], clasohm@0: subclass = [], clasohm@0: args = [], nipkow@200: coreg = [], nipkow@200: abbr = []}; clasohm@0: clasohm@0: fun undcl_class (s) = error("Class " ^ s ^ " has not been declared"); clasohm@0: clasohm@0: fun undcl_type(c) = "Undeclared type: " ^ c; clasohm@0: fun undcl_type_err(c) = error(undcl_type(c)); clasohm@0: clasohm@0: clasohm@0: (* 'leq' checks the partial order on classes according to the clasohm@0: statements in the association list 'a' (i.e.'subclass') clasohm@0: *) clasohm@0: clasohm@0: fun less a (C,D) = case assoc (a,C) of clasohm@0: Some(ss) => D mem ss clasohm@0: | None => undcl_class (C) ; clasohm@0: clasohm@0: fun leq a (C,D) = C = D orelse less a (C,D); clasohm@0: clasohm@0: clasohm@0: fun defaultS(TySg{default,...}) = default; clasohm@0: clasohm@0: (* 'logical_type' checks if some type declaration t has as range clasohm@0: a class which is a subclass of "logic" *) clasohm@0: clasohm@0: fun logical_type(tsig as TySg{subclass,coreg,...}) t = clasohm@0: let fun is_log C = leq subclass (C,"logic") clasohm@0: in case assoc (coreg,t) of clasohm@0: Some(ars) => exists (is_log o #1) ars clasohm@0: | None => undcl_type_err(t) clasohm@0: end; clasohm@0: nipkow@162: fun logical_types (tsig as TySg {args, ...}) = nipkow@162: filter (logical_type tsig) (map #1 args); nipkow@162: clasohm@0: (* 'sortorder' checks the ordering on sets of classes,i.e. on sorts: clasohm@0: S1 <= S2 ,iff for every class C2 in S2 there exists a class C1 in S1 clasohm@0: with C1 <= C2 (according to an association list 'a') clasohm@0: *) clasohm@0: clasohm@0: fun sortorder a (S1,S2) = clasohm@0: forall (fn C2 => exists (fn C1 => leq a (C1,C2)) S1) S2; clasohm@0: clasohm@0: clasohm@0: (* 'inj' inserts a new class C into a given class set S (i.e.sort) only if clasohm@0: there exists no class in S which is <= C; clasohm@0: the resulting set is minimal if S was minimal clasohm@0: *) clasohm@0: clasohm@0: fun inj a (C,S) = clasohm@0: let fun inj1 [] = [C] clasohm@0: | inj1 (D::T) = if leq a (D,C) then D::T clasohm@0: else if leq a (C,D) then inj1 T clasohm@0: else D::(inj1 T) clasohm@0: in inj1 S end; clasohm@0: clasohm@0: clasohm@0: (* 'union_sort' forms the minimal union set of two sorts S1 and S2 clasohm@0: under the assumption that S2 is minimal *) clasohm@0: clasohm@0: fun union_sort a = foldr (inj a); clasohm@0: clasohm@0: clasohm@0: (* 'elementwise_union' forms elementwise the minimal union set of two clasohm@0: sort lists under the assumption that the two lists have the same length clasohm@0: *) clasohm@0: clasohm@0: fun elementwise_union a (Ss1,Ss2) = map (union_sort a) (Ss1~~Ss2); clasohm@0: clasohm@0: clasohm@0: (* 'lew' checks for two sort lists the ordering for all corresponding list clasohm@0: elements (i.e. sorts) *) clasohm@0: clasohm@0: fun lew a (w1,w2) = forall (sortorder a) (w1~~w2); clasohm@0: clasohm@0: clasohm@0: (* 'is_min' checks if a class C is minimal in a given sort S under the clasohm@0: assumption that S contains C *) clasohm@0: clasohm@0: fun is_min a S C = not (exists (fn (D) => less a (D,C)) S); clasohm@0: clasohm@0: clasohm@0: (* 'min_sort' reduces a sort to its minimal classes *) clasohm@0: clasohm@0: fun min_sort a S = distinct(filter (is_min a S) S); clasohm@0: clasohm@0: clasohm@0: (* 'min_domain' minimizes the domain sorts of type declarationsl; clasohm@0: the function will be applied on the type declarations in extensions *) clasohm@0: clasohm@0: fun min_domain subclass = clasohm@0: let fun one_min (f,(doms,ran)) = (f, (map (min_sort subclass) doms, ran)) clasohm@0: in map one_min end; clasohm@0: clasohm@0: clasohm@0: (* 'min_filter' filters a list 'ars' consisting of arities (domain * class) clasohm@0: and gives back a list of those range classes whose domains meet the clasohm@0: predicate 'pred' *) clasohm@0: clasohm@0: fun min_filter a pred ars = clasohm@0: let fun filt ([],l) = l clasohm@0: | filt ((c,x)::xs,l) = if pred(x) then filt (xs,inj a (c,l)) clasohm@0: else filt (xs,l) clasohm@0: in filt (ars,[]) end; clasohm@0: clasohm@0: clasohm@0: (* 'cod_above' filters all arities whose domains are elementwise >= than clasohm@0: a given domain 'w' and gives back a list of the corresponding range clasohm@0: classes *) clasohm@0: clasohm@0: fun cod_above (a,w,ars) = min_filter a (fn w' => lew a (w,w')) ars; clasohm@0: nipkow@200: (*Instantiation of type variables in types*) nipkow@200: (*Pre: instantiations obey restrictions! *) nipkow@200: fun inst_typ tye = nipkow@200: let fun inst(Type(a,Ts)) = Type(a, map inst Ts) nipkow@200: | inst(T as TFree _) = T nipkow@200: | inst(T as TVar(v,_)) = nipkow@200: (case assoc(tye,v) of Some U => inst U | None => T) nipkow@200: in inst end; clasohm@0: clasohm@0: (* 'least_sort' returns for a given type its maximum sort: clasohm@0: - type variables, free types: the sort brought with clasohm@0: - type constructors: recursive determination of the maximum sort of the clasohm@0: arguments if the type is declared in 'coreg' of the clasohm@0: given type signature *) clasohm@0: nipkow@200: fun least_sort (tsig as TySg{subclass,coreg,abbr,...}) = clasohm@0: let fun ls(T as Type(a,Ts)) = nipkow@200: (case assoc(abbr,a) of nipkow@200: Some(v,U) => ls(inst_typ(v~~Ts) U) nipkow@200: | None => (case assoc (coreg,a) of nipkow@200: Some(ars) => cod_above(subclass,map ls Ts,ars) nipkow@200: | None => raise TYPE(undcl_type a,[T],[]))) clasohm@0: | ls(TFree(a,S)) = S clasohm@0: | ls(TVar(a,S)) = S clasohm@0: in ls end; clasohm@0: clasohm@0: clasohm@0: fun check_has_sort(tsig as TySg{subclass,coreg,...},T,S) = clasohm@0: if sortorder subclass ((least_sort tsig T),S) then () clasohm@0: else raise TYPE("Type not of sort " ^ (str_of_sort S),[T],[]) clasohm@0: clasohm@0: clasohm@0: (*Instantiation of type variables in types *) clasohm@0: fun inst_typ_tvars(tsig,tye) = clasohm@0: let fun inst(Type(a,Ts)) = Type(a, map inst Ts) clasohm@0: | inst(T as TFree _) = T clasohm@0: | inst(T as TVar(v,S)) = (case assoc(tye,v) of clasohm@0: None => T | Some(U) => (check_has_sort(tsig,U,S); U)) clasohm@0: in inst end; clasohm@0: clasohm@0: (*Instantiation of type variables in terms *) clasohm@0: fun inst_term_tvars(tsig,tye) = map_term_types (inst_typ_tvars(tsig,tye)); clasohm@0: nipkow@200: nipkow@200: (* expand1_typ *) nipkow@200: nipkow@200: fun expand1_typ(abbr,a,Ts) = nipkow@200: ( case assoc(abbr,a) of Some(v,U) => Some(inst_typ(v~~Ts) U) nipkow@200: | None => None ); nipkow@200: nipkow@200: (* expand_typ *) nipkow@200: nipkow@200: fun expand_typ(tsig as TySg{abbr,...}) = nipkow@200: let fun exptyp(Type(a,Ts)) = nipkow@200: ( case assoc(abbr,a) of nipkow@200: Some (v,U) => exptyp(inst_typ(v~~Ts) U) nipkow@200: | None => Type(a, map exptyp Ts) ) nipkow@200: | exptyp(T) = T nipkow@200: in exptyp end; nipkow@200: clasohm@0: exception TYPE_MATCH; clasohm@0: clasohm@0: (* Typ matching clasohm@0: typ_match(ts,s,(U,T)) = s' <=> s'(U)=T and s' is an extension of s *) nipkow@200: fun typ_match (tsig as TySg{abbr,...}) = clasohm@0: let fun tm(subs, (TVar(v,S), T)) = (case assoc(subs,v) of clasohm@0: None => ( (v, (check_has_sort(tsig,T,S); T))::subs clasohm@0: handle TYPE _ => raise TYPE_MATCH ) nipkow@200: | Some(U) => if expand_typ tsig U = expand_typ tsig T nipkow@200: then subs nipkow@200: else raise TYPE_MATCH) nipkow@200: | tm(subs, (T as Type(a,Ts), U as Type(b,Us))) = nipkow@200: if a<>b then nipkow@200: (case (expand1_typ(abbr,a,Ts), expand1_typ(abbr,b,Us)) of nipkow@200: (None,None) => raise TYPE_MATCH nipkow@200: | (None,Some(U)) => tm(subs,(T,U)) nipkow@200: | (Some(T),None) => tm(subs,(T,U)) nipkow@200: | (Some(T),Some(U)) => tm(subs,(T,U))) clasohm@0: else foldl tm (subs, Ts~~Us) clasohm@0: | tm(subs, (TFree(x), TFree(y))) = clasohm@0: if x=y then subs else raise TYPE_MATCH clasohm@0: | tm _ = raise TYPE_MATCH clasohm@0: in tm end; clasohm@0: clasohm@0: fun typ_instance(tsig,T,U) = let val x = typ_match tsig ([],(U,T)) in true end clasohm@0: handle TYPE_MATCH => false; clasohm@0: clasohm@0: clasohm@0: (* EXTENDING AND MERGIN TYPE SIGNATURES *) clasohm@0: clasohm@0: fun not_ident(s) = error("Must be an identifier: " ^ s); clasohm@0: clasohm@0: fun twice(a) = error("Type constructor " ^a^ " has already been declared."); clasohm@0: nipkow@200: fun tyab_conflict(a) = error("Canīt declare type "^(quote a)^"!\nAn abbreviation with this name exists already."); nipkow@200: clasohm@0: (*Is the type valid? Accumulates error messages in "errs".*) nipkow@200: fun type_errors (tsig as TySg{classes,args,abbr,...}) = nipkow@200: let fun class_err(errs,C) = nipkow@200: if C mem classes then errs nipkow@200: else ("Class " ^ quote C ^ " has not been declared") :: errs nipkow@200: val sort_err = foldl class_err nipkow@200: fun errors(Type(c,Us), errs) = clasohm@0: let val errs' = foldr errors (Us,errs) nipkow@200: fun nargs n = if n=length(Us) then errs' nipkow@200: else ("Wrong number of arguments: " ^ c) :: errs' clasohm@0: in case assoc(args,c) of nipkow@200: Some(n) => nargs n nipkow@200: | None => (case assoc(abbr,c) of nipkow@200: Some(v,_) => nargs(length v) nipkow@200: | None => (undcl_type c) :: errs) clasohm@0: end nipkow@200: | errors(TFree(_,S), errs) = sort_err(errs,S) nipkow@200: | errors(TVar(_,S), errs) = sort_err(errs,S) nipkow@200: in errors end; clasohm@0: clasohm@0: clasohm@0: (* 'add_class' adds a new class to the list of all existing classes *) clasohm@0: clasohm@0: fun add_class (classes,(s,_)) = clasohm@0: if s mem classes then error("Class " ^ s ^ " declared twice.") clasohm@0: else s::classes; clasohm@0: clasohm@0: (* 'add_subclass' adds a tuple consisiting of a new class (the new class clasohm@0: has already been inserted into the 'classes' list) and its clasohm@0: superclasses (they must be declared in 'classes' too) to the 'subclass' clasohm@0: list of the given type signature; clasohm@0: furthermore all inherited superclasses according to the superclasses clasohm@0: brought with are inserted and there is a check that there are no clasohm@0: cycles (i.e. C <= D <= C, with C <> D); *) clasohm@0: clasohm@0: fun add_subclass classes (subclass,(s,ges)) = clasohm@0: let fun upd (subclass,s') = if s' mem classes then clasohm@0: let val Some(ges') = assoc (subclass,s) clasohm@0: in case assoc (subclass,s') of clasohm@0: Some(sups) => if s mem sups clasohm@0: then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s ) clasohm@0: else overwrite (subclass,(s,sups union ges')) clasohm@0: | None => subclass clasohm@0: end clasohm@0: else undcl_class(s') clasohm@0: in foldl upd (subclass@[(s,ges)],ges) end; clasohm@0: clasohm@0: clasohm@0: (* 'extend_classes' inserts all new classes into the corresponding clasohm@0: lists ('classes','subclass') if possible *) clasohm@0: clasohm@0: fun extend_classes (classes,subclass,newclasses) = clasohm@0: if newclasses = [] then (classes,subclass) else clasohm@0: let val classes' = foldl add_class (classes,newclasses); clasohm@0: val subclass' = foldl (add_subclass classes') (subclass,newclasses); clasohm@0: in (classes',subclass') end; clasohm@0: clasohm@0: (* Corregularity *) clasohm@0: clasohm@0: (* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *) clasohm@0: clasohm@0: fun is_unique_decl coreg (t,(s,w)) = case assoc2 (coreg,(t,s)) of clasohm@0: Some(w1) => if w = w1 then () else clasohm@0: error("There are two declarations\n" ^ clasohm@0: str_of_decl(t,w,s) ^ " and\n" ^ clasohm@0: str_of_decl(t,w1,s) ^ "\n" ^ clasohm@0: "with the same result class.") clasohm@0: | None => (); clasohm@0: clasohm@0: (* 'restr2' checks if there are two declarations t:(Ss1)C1 and t:(Ss2)C2 clasohm@0: such that C1 >= C2 then Ss1 >= Ss2 (elementwise) *) clasohm@0: clasohm@0: fun subs (classes,subclass) C = clasohm@0: let fun sub (rl,l) = if leq subclass (l,C) then l::rl else rl clasohm@0: in foldl sub ([],classes) end; clasohm@0: clasohm@0: fun coreg_err(t,(w1,C),(w2,D)) = clasohm@0: error("Declarations " ^ str_of_decl(t,w1,C) ^ " and " clasohm@0: ^ str_of_decl(t,w2,D) ^ " are in conflict"); clasohm@0: clasohm@0: fun restr2 classes (subclass,coreg) (t,(s,w)) = clasohm@0: let fun restr ([],test) = () clasohm@0: | restr (s1::Ss,test) = (case assoc2 (coreg,(t,s1)) of clasohm@0: Some (dom) => if lew subclass (test (w,dom)) then restr (Ss,test) clasohm@0: else coreg_err (t,(w,s),(dom,s1)) clasohm@0: | None => restr (Ss,test)) clasohm@0: fun forward (t,(s,w)) = clasohm@0: let val s_sups = case assoc (subclass,s) of clasohm@0: Some(s_sups) => s_sups | None => undcl_class(s); clasohm@0: in restr (s_sups,I) end clasohm@0: fun backward (t,(s,w)) = clasohm@0: let val s_subs = subs (classes,subclass) s clasohm@0: in restr (s_subs,fn (x,y) => (y,x)) end clasohm@0: in (backward (t,(s,w)); forward (t,(s,w))) end; clasohm@0: clasohm@0: clasohm@0: fun varying_decls(t) = clasohm@0: error("Type constructor "^t^" has varying number of arguments."); clasohm@0: clasohm@0: clasohm@0: clasohm@0: (* 'coregular' checks clasohm@0: - the two restriction conditions 'is_unique_decl' and 'restr2' clasohm@0: - if the classes in the new type declarations are known in the clasohm@0: given type signature clasohm@0: - if one type constructor has always the same number of arguments; clasohm@0: if one type declaration has passed all checks it is inserted into clasohm@0: the 'coreg' association list of the given type signatrure *) clasohm@0: clasohm@0: fun coregular (classes,subclass,args) = clasohm@0: let fun ex C = if C mem classes then () else undcl_class(C); clasohm@0: clasohm@0: fun addar(w,C) (coreg,t) = case assoc(args,t) of clasohm@0: Some(n) => if n <> length w then varying_decls(t) else clasohm@0: (is_unique_decl coreg (t,(C,w)); clasohm@0: (seq o seq) ex w; clasohm@0: restr2 classes (subclass,coreg) (t,(C,w)); clasohm@0: let val Some(ars) = assoc(coreg,t) clasohm@0: in overwrite(coreg,(t,(C,w) ins ars)) end) clasohm@0: | None => undcl_type_err(t); clasohm@0: clasohm@0: fun addts(coreg,(ts,ar)) = foldl (addar ar) (coreg,ts) clasohm@0: clasohm@0: in addts end; clasohm@0: clasohm@0: clasohm@0: (* 'close' extends the 'coreg' association list after all new type clasohm@0: declarations have been inserted successfully: clasohm@0: for every declaration t:(Ss)C , for all classses D with C <= D: clasohm@0: if there is no declaration t:(Ss')C' with C < C' and C' <= D clasohm@0: then insert the declaration t:(Ss)D into 'coreg' clasohm@0: this means, if there exists a declaration t:(Ss)C and there is clasohm@0: no declaration t:(Ss')D with C <=D then the declaration holds clasohm@0: for all range classes more general than C *) clasohm@0: clasohm@0: fun close (coreg,subclass) = clasohm@0: let fun check sl (l,(s,dom)) = case assoc (subclass,s) of clasohm@0: Some(sups) => clasohm@0: let fun close_sup (l,sup) = clasohm@0: if exists (fn s'' => less subclass (s,s'') andalso clasohm@0: leq subclass (s'',sup)) sl clasohm@0: then l clasohm@0: else (sup,dom)::l clasohm@0: in foldl close_sup (l,sups) end clasohm@0: | None => l; clasohm@0: fun ext (s,l) = (s, foldl (check (map #1 l)) (l,l)); clasohm@0: in map ext coreg end; clasohm@0: nipkow@200: fun add_types(aca,(ts,n)) = nipkow@200: let fun add_type((args,coreg,abbr),t) = case assoc(args,t) of nipkow@200: Some _ => twice(t) nipkow@200: | None => (case assoc(abbr,t) of Some _ => tyab_conflict(t) nipkow@200: | None => ((t,n)::args,(t,[])::coreg,abbr)) clasohm@0: in if n<0 clasohm@0: then error("Type constructor cannot have negative number of arguments") nipkow@200: else foldl add_type (aca,ts) clasohm@0: end; clasohm@0: nipkow@200: (* check_abbr *) nipkow@200: nipkow@200: fun check_abbr( (a,(vs,U)), tsig as TySg{abbr,args,...} ) = nipkow@200: let val (ndxname,_) = split_list(add_typ_tvars(U,[])) nipkow@200: fun err_abbr a = ("ERROR in abbreviation "^ quote a) nipkow@200: in if not( (ndxname subset vs) andalso (vs subset ndxname) ) nipkow@200: then [err_abbr a,("Not the same set of variables on lhs and rhs")] nipkow@200: else nipkow@200: (case findrep(vs) of nipkow@200: (v,_)::_ => [err_abbr a,("Variable "^v^" occurs twice on lhs")] nipkow@200: |[] => nipkow@200: (case assoc(args,a) of nipkow@200: Some _ => [err_abbr a,("A type with this name exists already")] nipkow@200: |None => nipkow@200: (case assoc(abbr,a) of nipkow@200: Some _ => [err_abbr a,("An abbreviation with this name exists already")] nipkow@200: |None => nipkow@200: (case type_errors (tsig) (U,[]) of nipkow@200: [] => [] nipkow@200: |errs => (err_abbr a) :: errs nipkow@200: ) nipkow@200: ) nipkow@200: ) nipkow@200: ) nipkow@200: end; nipkow@200: nipkow@200: (* add_abbrs *) nipkow@200: nipkow@200: fun add_abbr (tsig as TySg{classes,default,subclass,args,coreg,abbr}, nipkow@200: newabbr) = nipkow@200: case check_abbr (newabbr,tsig) of nipkow@200: [] => TySg{classes=classes,default=default,subclass=subclass,args=args, nipkow@200: coreg=coreg, abbr = (newabbr) :: abbr} nipkow@200: | errs => error(cat_lines errs) ; nipkow@200: nipkow@200: val add_abbrs = foldl add_abbr; nipkow@200: nipkow@200: clasohm@0: (* 'extend' takes the above described check- and extend-functions to clasohm@0: extend a given type signature with new classes and new type declarations *) clasohm@0: nipkow@200: fun extend (TySg{classes,default,subclass,args,coreg,abbr}, clasohm@0: newclasses,newdefault,types,arities) = clasohm@0: let val (classes',subclass') = extend_classes(classes,subclass,newclasses); nipkow@200: val (args',coreg',_) = foldl add_types ((args,coreg,abbr),types); clasohm@0: val old_coreg = map #1 coreg; clasohm@0: fun is_old(c) = if c mem old_coreg then () else undcl_type_err(c); clasohm@0: fun is_new(c) = if c mem old_coreg then twice(c) else (); clasohm@0: val coreg'' = foldl (coregular (classes',subclass',args')) clasohm@0: (coreg',min_domain subclass' arities); clasohm@0: val coreg''' = close (coreg'',subclass'); clasohm@0: val default' = if null newdefault then default else newdefault; clasohm@0: in TySg{classes=classes', default=default',subclass=subclass', args=args', nipkow@200: coreg=coreg''',abbr=abbr} end; clasohm@0: clasohm@0: clasohm@0: (* 'assoc_union' merges two association lists if the contents associated clasohm@0: the keys are lists *) clasohm@0: clasohm@0: fun assoc_union (as1,[]) = as1 clasohm@0: | assoc_union (as1,(key,l2)::as2) = case assoc (as1,key) of clasohm@0: Some(l1) => assoc_union (overwrite(as1,(key,l1 union l2)),as2) clasohm@0: | None => assoc_union ((key,l2)::as1,as2); clasohm@0: clasohm@0: clasohm@0: fun trcl r = clasohm@0: let val r' = transitive_closure r clasohm@0: in if exists (op mem) r' then error("Cyclic class structure!") else r' end; clasohm@0: clasohm@0: clasohm@0: (* 'merge_coreg' builds the union of two 'coreg' lists; clasohm@0: it only checks the two restriction conditions and inserts afterwards clasohm@0: all elements of the second list into the first one *) clasohm@0: clasohm@0: fun merge_coreg classes subclass1 = clasohm@0: let fun test_ar classes (t,ars1) (coreg1,(s,w)) = clasohm@0: (is_unique_decl coreg1 (t,(s,w)); clasohm@0: restr2 classes (subclass1,coreg1) (t,(s,w)); clasohm@0: overwrite (coreg1,(t,(s,w) ins ars1))); clasohm@0: clasohm@0: fun merge_c (coreg1,(c as (t,ars2))) = case assoc (coreg1,t) of clasohm@0: Some(ars1) => foldl (test_ar classes (t,ars1)) (coreg1,ars2) clasohm@0: | None => c::coreg1 clasohm@0: in foldl merge_c end; clasohm@0: clasohm@0: fun merge_args(args,(t,n)) = case assoc(args,t) of clasohm@0: Some(m) => if m=n then args else varying_decls(t) clasohm@0: | None => (t,n)::args; clasohm@0: nipkow@200: fun merge_abbrs(abbr1,abbr2) = nipkow@200: let val abbru = abbr1 union abbr2 nipkow@200: val names = map fst abbru nipkow@200: in ( case findrep names of nipkow@200: [] => abbru nipkow@200: |a::_ => error("ERROR in Type.merge: abbreviation "^a^" declared twice") ) end; nipkow@200: clasohm@0: (* 'merge' takes the above declared functions to merge two type signatures *) clasohm@0: clasohm@0: fun merge(TySg{classes=classes1,default=default1,subclass=subclass1,args=args1, nipkow@200: coreg=coreg1,abbr=abbr1}, clasohm@0: TySg{classes=classes2,default=default2,subclass=subclass2,args=args2, nipkow@200: coreg=coreg2,abbr=abbr2}) = clasohm@0: let val classes' = classes1 union classes2; clasohm@0: val subclass' = trcl (assoc_union (subclass1,subclass2)); clasohm@0: val args' = foldl merge_args (args1,args2) clasohm@0: val coreg' = merge_coreg classes' subclass' (coreg1,coreg2); nipkow@200: val default' = min_sort subclass' (default1 @ default2); nipkow@200: val abbr' = merge_abbrs(abbr1, abbr2); clasohm@0: in TySg{classes=classes' , default=default',subclass=subclass', args=args', nipkow@200: coreg=coreg' , abbr = abbr' } clasohm@0: end; clasohm@0: nipkow@200: clasohm@0: (**** TYPE INFERENCE ****) clasohm@0: clasohm@0: (* clasohm@0: clasohm@0: Input: clasohm@0: - a 'raw' term which contains only dummy types and some explicit type clasohm@0: constraints encoded as terms. clasohm@0: - the expected type of the term. clasohm@0: clasohm@0: Output: clasohm@0: - the correctly typed term clasohm@0: - the substitution needed to unify the actual type of the term with its clasohm@0: expected type; only the TVars in the expected type are included. clasohm@0: clasohm@0: During type inference all TVars in the term have negative index. This keeps clasohm@0: them apart from normal TVars, which is essential, because at the end the type clasohm@0: of the term is unified with the expected type, which contains normal TVars. clasohm@0: clasohm@0: 1. Add initial type information to the term (add_types). clasohm@0: This freezes (freeze_vars) TVars in explicitly provided types (eg clasohm@0: constraints or defaults) by turning them into TFrees. clasohm@0: 2. Carry out type inference, possibly introducing new negative TVars. clasohm@0: 3. Unify actual and expected type. clasohm@0: 4. Turn all (negative) TVars into unique new TFrees (freeze). clasohm@0: 5. Thaw all TVars frozen in step 1 (thaw_vars). clasohm@0: clasohm@0: *) clasohm@0: clasohm@0: (*Raised if types are not unifiable*) clasohm@0: exception TUNIFY; clasohm@0: clasohm@0: val tyvar_count = ref(~1); clasohm@0: clasohm@0: fun tyinit() = (tyvar_count := ~1); clasohm@0: clasohm@0: fun new_tvar_inx() = (tyvar_count := !tyvar_count-1; !tyvar_count) clasohm@0: clasohm@0: (* clasohm@0: Generate new TVar. Index is < ~1 to distinguish it from TVars generated from clasohm@0: variable names (see id_type). Name is arbitrary because index is new. clasohm@0: *) clasohm@0: clasohm@0: fun gen_tyvar(S) = TVar(("'a", new_tvar_inx()),S); clasohm@0: clasohm@0: (*Occurs check: type variable occurs in type?*) clasohm@0: fun occ v tye = clasohm@0: let fun occ(Type(_,Ts)) = exists occ Ts clasohm@0: | occ(TFree _) = false clasohm@0: | occ(TVar(w,_)) = v=w orelse clasohm@0: (case assoc(tye,w) of clasohm@0: None => false clasohm@0: | Some U => occ U); clasohm@0: in occ end; clasohm@0: clasohm@0: (*Chase variable assignments in tye. clasohm@0: If devar (T,tye) returns a type var then it must be unassigned.*) clasohm@0: fun devar (T as TVar(v,_), tye) = (case assoc(tye,v) of clasohm@0: Some U => devar (U,tye) clasohm@0: | None => T) clasohm@0: | devar (T,tye) = T; clasohm@0: clasohm@0: clasohm@0: (* 'dom' returns for a type constructor t the list of those domains clasohm@0: which deliver a given range class C *) clasohm@0: clasohm@0: fun dom coreg t C = case assoc2 (coreg, (t,C)) of clasohm@0: Some(Ss) => Ss clasohm@0: | None => raise TUNIFY; clasohm@0: clasohm@0: clasohm@0: (* 'Dom' returns the union of all domain lists of 'dom' for a given sort S clasohm@0: (i.e. a set of range classes ); the union is carried out elementwise clasohm@0: for the seperate sorts in the domains *) clasohm@0: clasohm@0: fun Dom (subclass,coreg) (t,S) = clasohm@0: let val domlist = map (dom coreg t) S; clasohm@0: in if null domlist then [] clasohm@0: else foldl (elementwise_union subclass) (hd domlist,tl domlist) clasohm@0: end; clasohm@0: clasohm@0: clasohm@0: fun W ((T,S),tsig as TySg{subclass,coreg,...},tye) = clasohm@0: let fun Wd ((T,S),tye) = W ((devar (T,tye),S),tsig,tye) clasohm@0: fun Wk(T as TVar(v,S')) = clasohm@0: if sortorder subclass (S',S) then tye clasohm@0: else (v,gen_tyvar(union_sort subclass (S',S)))::tye clasohm@0: | Wk(T as TFree(v,S')) = if sortorder subclass (S',S) then tye clasohm@0: else raise TUNIFY clasohm@0: | Wk(T as Type(f,Ts)) = clasohm@0: if null S then tye clasohm@0: else foldr Wd (Ts~~(Dom (subclass,coreg) (f,S)) ,tye) clasohm@0: in Wk(T) end; clasohm@0: clasohm@0: clasohm@0: (* Order-sorted Unification of Types (U) *) clasohm@0: clasohm@0: (* Precondition: both types are well-formed w.r.t. type constructor arities *) nipkow@200: fun unify (tsig as TySg{subclass,coreg,abbr,...}) = clasohm@0: let fun unif ((T,U),tye) = clasohm@0: case (devar(T,tye), devar(U,tye)) of clasohm@0: (T as TVar(v,S1), U as TVar(w,S2)) => clasohm@0: if v=w then tye else clasohm@0: if sortorder subclass (S1,S2) then (w,T)::tye else clasohm@0: if sortorder subclass (S2,S1) then (v,U)::tye clasohm@0: else let val nu = gen_tyvar (union_sort subclass (S1,S2)) clasohm@0: in (v,nu)::(w,nu)::tye end clasohm@0: | (T as TVar(v,S), U) => clasohm@0: if occ v tye U then raise TUNIFY else W ((U,S),tsig,(v,U)::tye) clasohm@0: | (U, T as TVar (v,S)) => clasohm@0: if occ v tye U then raise TUNIFY else W ((U,S),tsig,(v,U)::tye) nipkow@200: | (T as Type(a,Ts),U as Type(b,Us)) => nipkow@200: if a<>b then nipkow@200: (case (expand1_typ(abbr,a,Ts), expand1_typ(abbr,b,Us)) of nipkow@200: (None,None) => raise TUNIFY nipkow@200: | (None,Some(U)) => unif((T,U),tye) nipkow@200: | (Some(T),None) => unif((T,U),tye) nipkow@200: | (Some(T),Some(U)) => unif((T,U),tye)) nipkow@200: else foldr unif (Ts~~Us,tye) clasohm@0: | (T,U) => if T=U then tye else raise TUNIFY clasohm@0: in unif end; clasohm@0: clasohm@0: clasohm@0: (*Type inference for polymorphic term*) clasohm@0: fun infer tsig = clasohm@0: let fun inf(Ts, Const (_,T), tye) = (T,tye) clasohm@0: | inf(Ts, Free (_,T), tye) = (T,tye) clasohm@0: | inf(Ts, Bound i, tye) = ((nth_elem(i,Ts) , tye) clasohm@0: handle LIST _=> raise TYPE ("loose bound variable", [], [Bound i])) clasohm@0: | inf(Ts, Var (_,T), tye) = (T,tye) clasohm@0: | inf(Ts, Abs (_,T,body), tye) = clasohm@0: let val (U,tye') = inf(T::Ts, body, tye) in (T-->U, tye') end clasohm@0: | inf(Ts, f$u, tye) = clasohm@0: let val (U,tyeU) = inf(Ts, u, tye); clasohm@0: val (T,tyeT) = inf(Ts, f, tyeU); clasohm@0: fun err s = clasohm@0: raise TYPE(s, [inst_typ tyeT T, inst_typ tyeT U], [f$u]) clasohm@0: in case T of clasohm@0: Type("fun",[T1,T2]) => clasohm@0: ( (T2, unify tsig ((T1,U), tyeT)) clasohm@0: handle TUNIFY => err"type mismatch in application" ) clasohm@0: | TVar _ => clasohm@0: let val T2 = gen_tyvar([]) clasohm@0: in (T2, unify tsig ((T, U-->T2), tyeT)) clasohm@0: handle TUNIFY => err"type mismatch in application" clasohm@0: end clasohm@0: | _ => err"rator must have function type" clasohm@0: end clasohm@0: in inf end; clasohm@0: clasohm@0: fun freeze_vars(Type(a,Ts)) = Type(a,map freeze_vars Ts) clasohm@0: | freeze_vars(T as TFree _) = T clasohm@0: | freeze_vars(TVar(v,S)) = TFree(Syntax.string_of_vname v, S); clasohm@0: clasohm@0: (* Attach a type to a constant *) clasohm@0: fun type_const (a,T) = Const(a, incr_tvar (new_tvar_inx()) T); clasohm@0: clasohm@0: (*Find type of ident. If not in table then use ident's name for tyvar clasohm@0: to get consistent typing.*) nipkow@200: fun new_id_type a = TVar(("'"^a,new_tvar_inx()),[]); clasohm@0: fun type_of_ixn(types,ixn as (a,_)) = nipkow@200: case types ixn of Some T => freeze_vars T | None => TVar(("'"^a,~1),[]); clasohm@0: clasohm@0: fun constrain(term,T) = Const(Syntax.constrainC,T-->T) $ term; clasohm@0: fun constrainAbs(Abs(a,_,body),T) = Abs(a,T,body); clasohm@0: clasohm@0: (* clasohm@0: clasohm@0: Attach types to a term. Input is a "parse tree" containing dummy types. clasohm@0: Type constraints are translated and checked for validity wrt tsig. clasohm@0: TVars in constraints are frozen. clasohm@0: clasohm@0: The atoms in the resulting term satisfy the following spec: clasohm@0: clasohm@0: Const(a,T): clasohm@0: T is a renamed copy of the generic type of a; renaming decreases index of clasohm@0: all TVars by new_tvar_inx(), which is less than ~1. The index of all TVars clasohm@0: in the generic type must be 0 for this to work! clasohm@0: clasohm@0: Free(a,T), Var(ixn,T): clasohm@0: T is either the frozen default type of a or TVar(("'"^a,~1),[]) clasohm@0: clasohm@0: Abs(a,T,_): clasohm@0: T is either a type constraint or TVar(("'"^a,i),[]), where i is generated clasohm@0: by new_tvar_inx(). Thus different abstractions can have the bound variables clasohm@0: of the same name but different types. clasohm@0: clasohm@0: *) clasohm@0: clasohm@0: fun add_types (tsig, const_tab, types, sorts, string_of_typ) = clasohm@0: let val S0 = defaultS tsig; clasohm@0: fun defS0 ixn = case sorts ixn of Some S => S | None => S0; clasohm@0: fun prepareT(typ) = clasohm@0: let val T = Syntax.typ_of_term defS0 typ; clasohm@0: val T' = freeze_vars T nipkow@200: in case type_errors (tsig) (T,[]) of clasohm@0: [] => T' clasohm@0: | errs => raise TYPE(cat_lines errs,[T],[]) clasohm@0: end clasohm@0: fun add (Const(a,_)) = clasohm@0: (case Symtab.lookup(const_tab, a) of clasohm@0: Some T => type_const(a,T) clasohm@0: | None => raise TYPE ("No such constant: "^a, [], [])) clasohm@0: | add (Bound i) = Bound i clasohm@0: | add (Free(a,_)) = clasohm@0: (case Symtab.lookup(const_tab, a) of clasohm@0: Some T => type_const(a,T) clasohm@0: | None => Free(a, type_of_ixn(types,(a,~1)))) clasohm@0: | add (Var(ixn,_)) = Var(ixn, type_of_ixn(types,ixn)) clasohm@0: | add (Abs(a,_,body)) = Abs(a, new_id_type a, add body) clasohm@0: | add ((f as Const(a,_)$t1)$t2) = clasohm@0: if a=Syntax.constrainC then constrain(add t1,prepareT t2) else clasohm@0: if a=Syntax.constrainAbsC then constrainAbs(add t1,prepareT t2) clasohm@0: else add f $ add t2 clasohm@0: | add (f$t) = add f $ add t clasohm@0: in add end; clasohm@0: clasohm@0: clasohm@0: (* Post-Processing *) clasohm@0: clasohm@0: clasohm@0: (*Instantiation of type variables in terms*) clasohm@0: fun inst_types tye = map_term_types (inst_typ tye); clasohm@0: clasohm@0: (*Delete explicit constraints -- occurrences of "_constrain" *) clasohm@0: fun unconstrain (Abs(a,T,t)) = Abs(a, T, unconstrain t) clasohm@0: | unconstrain ((f as Const(a,_)) $ t) = clasohm@0: if a=Syntax.constrainC then unconstrain t clasohm@0: else unconstrain f $ unconstrain t clasohm@0: | unconstrain (f$t) = unconstrain f $ unconstrain t clasohm@0: | unconstrain (t) = t; clasohm@0: clasohm@0: clasohm@0: (* Turn all TVars which satisfy p into new TFrees *) clasohm@0: fun freeze p t = clasohm@0: let val fs = add_term_tfree_names(t,[]); clasohm@0: val inxs = filter p (add_term_tvar_ixns(t,[])); clasohm@0: val vmap = inxs ~~ variantlist(map #1 inxs, fs); clasohm@0: fun free(Type(a,Ts)) = Type(a, map free Ts) clasohm@0: | free(T as TVar(v,S)) = clasohm@0: (case assoc(vmap,v) of None => T | Some(a) => TFree(a,S)) clasohm@0: | free(T as TFree _) = T clasohm@0: in map_term_types free t end; clasohm@0: clasohm@0: (* Thaw all TVars that were frozen in freeze_vars *) clasohm@0: fun thaw_vars(Type(a,Ts)) = Type(a, map thaw_vars Ts) clasohm@0: | thaw_vars(T as TFree(a,S)) = (case explode a of clasohm@0: "?"::"'"::vn => let val ((b,i),_) = Syntax.scan_varname vn clasohm@0: in TVar(("'"^b,i),S) end clasohm@0: | _ => T) clasohm@0: | thaw_vars(T) = T; clasohm@0: clasohm@0: clasohm@0: fun restrict tye = clasohm@0: let fun clean(tye1, ((a,i),T)) = clasohm@0: if i < 0 then tye1 else ((a,i),inst_typ tye T) :: tye1 clasohm@0: in foldl clean ([],tye) end clasohm@0: clasohm@0: clasohm@0: (*Infer types for term t using tables. Check that t's type and T unify *) clasohm@0: clasohm@0: fun infer_term (tsig, const_tab, types, sorts, string_of_typ, T, t) = clasohm@0: let val u = add_types (tsig, const_tab, types, sorts, string_of_typ) t; clasohm@0: val (U,tye) = infer tsig ([], u, []); clasohm@0: val uu = unconstrain u; clasohm@0: val tye' = unify tsig ((T,U),tye) handle TUNIFY => raise TYPE clasohm@0: ("Term does not have expected type", [T, U], [inst_types tye uu]) clasohm@0: val Ttye = restrict tye' (* restriction to TVars in T *) clasohm@0: val all = Const("", Type("", map snd Ttye)) $ (inst_types tye' uu) clasohm@0: (* all is a dummy term which contains all exported TVars *) clasohm@0: val Const(_,Type(_,Ts)) $ u'' = clasohm@0: map_term_types thaw_vars (freeze (fn (_,i) => i<0) all) clasohm@0: (* turn all internally generated TVars into TFrees clasohm@0: and thaw all initially frozen TVars *) clasohm@0: in (u'', (map fst Ttye) ~~ Ts) end; clasohm@0: clasohm@0: fun infer_types args = (tyinit(); infer_term args); clasohm@0: clasohm@0: clasohm@0: (* Turn TFrees into TVars to allow types & axioms to be written without "?" *) clasohm@0: fun varifyT(Type(a,Ts)) = Type(a,map varifyT Ts) clasohm@0: | varifyT(TFree(a,S)) = TVar((a,0),S) clasohm@0: | varifyT(T) = T; clasohm@0: clasohm@0: (* Turn TFrees except those in fixed into new TVars *) clasohm@0: fun varify(t,fixed) = clasohm@0: let val fs = add_term_tfree_names(t,[]) \\ fixed; clasohm@0: val ixns = add_term_tvar_ixns(t,[]); clasohm@0: val fmap = fs ~~ variantlist(fs, map #1 ixns) clasohm@0: fun thaw(Type(a,Ts)) = Type(a, map thaw Ts) clasohm@0: | thaw(T as TVar _) = T clasohm@0: | thaw(T as TFree(a,S)) = clasohm@0: (case assoc(fmap,a) of None => T | Some b => TVar((b,0),S)) clasohm@0: in map_term_types thaw t end; clasohm@0: clasohm@0: clasohm@0: end;