wenzelm@256: (* Title: Pure/type.ML wenzelm@256: Author: Tobias Nipkow & Lawrence C Paulson clasohm@0: ID: $Id$ clasohm@0: wenzelm@256: Types and Sorts. Type Inference. wenzelm@256: wenzelm@256: TODO: wenzelm@256: Maybe type classes should go in a separate module? wenzelm@256: Maybe type inference part (excl unify) should go in a separate module? clasohm@0: *) clasohm@0: clasohm@0: signature TYPE = clasohm@0: sig wenzelm@256: structure Symtab: SYMTAB clasohm@0: type type_sig nipkow@200: val rep_tsig: type_sig -> wenzelm@256: {classes: class list, wenzelm@256: subclass: (class * class list) list, wenzelm@256: default: sort, wenzelm@256: args: (string * int) list, wenzelm@256: abbrs: (string * (indexname list * typ)) list, wenzelm@256: coreg: (string * (class * sort list) list) list} clasohm@0: val defaultS: type_sig -> sort wenzelm@256: val logical_types: type_sig -> string list wenzelm@256: val tsig0: type_sig wenzelm@256: val extend_tsig: type_sig -> wenzelm@256: (class * class list) list * sort * (string list * int) list * wenzelm@256: (string list * (sort list * class)) list -> type_sig wenzelm@256: val ext_tsig_abbrs: type_sig -> (string * (indexname list * typ)) list wenzelm@256: -> type_sig wenzelm@256: val merge_tsigs: type_sig * type_sig -> type_sig wenzelm@256: val cert_typ: type_sig -> typ -> typ wenzelm@256: val norm_typ: type_sig -> typ -> typ 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) * wenzelm@256: (indexname -> sort option) * typ * term -> term * (indexname * typ) list wenzelm@256: val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term clasohm@0: val thaw_vars: typ -> typ wenzelm@256: val typ_errors: type_sig -> typ * string list -> string list clasohm@0: val typ_instance: type_sig * typ * typ -> bool wenzelm@256: val typ_match: type_sig -> (indexname * typ) list * (typ * typ) wenzelm@256: -> (indexname * typ) list wenzelm@256: val unify: type_sig -> (typ * typ) * (indexname * typ) list wenzelm@256: -> (indexname * typ) list clasohm@0: val varifyT: typ -> typ clasohm@0: val varify: term * string list -> term clasohm@0: exception TUNIFY wenzelm@256: exception TYPE_MATCH clasohm@0: end; clasohm@0: wenzelm@256: functor TypeFun(structure Symtab: SYMTAB and Syntax: SYNTAX) (*: TYPE*) (* FIXME debug *) = clasohm@0: struct clasohm@0: wenzelm@256: structure Symtab = Symtab; clasohm@0: clasohm@0: wenzelm@256: (*** type classes ***) (* FIXME improve comment *) clasohm@0: clasohm@0: type domain = sort list; clasohm@0: type arity = domain * class; clasohm@0: wenzelm@256: fun str_of_sort S = parents "{" "}" (commas S); wenzelm@256: fun str_of_dom dom = parents "(" ")" (commas (map str_of_sort dom)); wenzelm@256: fun str_of_decl (t, w, C) = t ^ " :: " ^ str_of_dom w ^ " " ^ C; wenzelm@256: wenzelm@256: wenzelm@256: wenzelm@256: (** type signature **) wenzelm@256: wenzelm@256: (* wenzelm@256: classes: wenzelm@256: a list of all declared classes; clasohm@0: wenzelm@256: subclass: wenzelm@256: association list representation of subclass relationship; (c, cs) is wenzelm@256: interpreted as "c is a proper subclass of all elemenst of cs"; note that wenzelm@256: c itself is not a memeber of cs; wenzelm@256: wenzelm@256: default: wenzelm@256: the default sort attached to all unconstrained type vars; wenzelm@256: wenzelm@256: args: wenzelm@256: an association list of all declared types with the number of their wenzelm@256: arguments; wenzelm@256: wenzelm@256: abbrs: wenzelm@256: an association list of type abbreviations; wenzelm@256: wenzelm@256: coreg: wenzelm@256: a two-fold association list of all type arities; (t, al) means that type wenzelm@256: constructor t has the arities in al; an element (c, ss) of al represents wenzelm@256: the arity (ss)c; clasohm@0: *) clasohm@0: wenzelm@256: datatype type_sig = wenzelm@256: TySg of { wenzelm@256: classes: class list, wenzelm@256: subclass: (class * class list) list, wenzelm@256: default: sort, wenzelm@256: args: (string * int) list, wenzelm@256: abbrs: (string * (indexname list * typ)) list, wenzelm@256: coreg: (string * (class * domain) list) list}; wenzelm@256: nipkow@189: fun rep_tsig (TySg comps) = comps; clasohm@0: wenzelm@256: fun defaultS (TySg {default, ...}) = default; wenzelm@256: wenzelm@256: wenzelm@256: wenzelm@256: (* FIXME move *) clasohm@0: wenzelm@256: fun undcl_class c = "Undeclared class: " ^ quote c; wenzelm@256: val err_undcl_class = error o undcl_class; clasohm@0: wenzelm@256: fun undcl_type c = "Undeclared type constructor: " ^ quote c; wenzelm@256: val err_undcl_type = error o undcl_type; wenzelm@256: 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: wenzelm@256: fun less a (C, D) = case assoc (a, C) of clasohm@0: Some(ss) => D mem ss wenzelm@256: | None => err_undcl_class (C) ; clasohm@0: wenzelm@256: fun leq a (C, D) = C = D orelse less a (C, D); clasohm@0: clasohm@0: wenzelm@256: 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: wenzelm@256: fun logical_type(tsig as TySg{subclass, coreg, ...}) t = wenzelm@256: let fun is_log C = leq subclass (C, "logic") wenzelm@256: in case assoc (coreg, t) of clasohm@0: Some(ars) => exists (is_log o #1) ars wenzelm@256: | None => err_undcl_type(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: wenzelm@256: (* 'sortorder' checks the ordering on sets of classes, i.e. on sorts: wenzelm@256: 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: wenzelm@256: fun sortorder a (S1, S2) = wenzelm@256: 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: wenzelm@256: fun inj a (C, S) = clasohm@0: let fun inj1 [] = [C] wenzelm@256: | inj1 (D::T) = if leq a (D, C) then D::T wenzelm@256: 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 *) wenzelm@256: (* FIXME rename to inter_sort (?) *) 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 wenzelm@256: *) clasohm@0: wenzelm@256: fun elementwise_union a (Ss1, Ss2) = map (union_sort a) (Ss1~~Ss2); wenzelm@256: clasohm@0: clasohm@0: (* 'lew' checks for two sort lists the ordering for all corresponding list clasohm@0: elements (i.e. sorts) *) clasohm@0: wenzelm@256: fun lew a (w1, w2) = forall (sortorder a) (w1~~w2); wenzelm@256: clasohm@0: wenzelm@256: (* 'is_min' checks if a class C is minimal in a given sort S under the wenzelm@256: assumption that S contains C *) clasohm@0: wenzelm@256: 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; wenzelm@256: the function will be applied on the type declarations in extensions *) clasohm@0: clasohm@0: fun min_domain subclass = wenzelm@256: 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) wenzelm@256: and gives back a list of those range classes whose domains meet the clasohm@0: predicate 'pred' *) wenzelm@256: clasohm@0: fun min_filter a pred ars = wenzelm@256: let fun filt ([], l) = l wenzelm@256: | filt ((c, x)::xs, l) = if pred(x) then filt (xs, inj a (c, l)) wenzelm@256: else filt (xs, l) wenzelm@256: in filt (ars, []) end; clasohm@0: clasohm@0: clasohm@0: (* 'cod_above' filters all arities whose domains are elementwise >= than wenzelm@256: a given domain 'w' and gives back a list of the corresponding range clasohm@0: classes *) clasohm@0: wenzelm@256: fun cod_above (a, w, ars) = min_filter a (fn w' => lew a (w, w')) ars; wenzelm@256: wenzelm@256: clasohm@0: nipkow@200: (*Instantiation of type variables in types*) nipkow@200: (*Pre: instantiations obey restrictions! *) nipkow@200: fun inst_typ tye = wenzelm@256: let fun inst(Type(a, Ts)) = Type(a, map inst Ts) nipkow@200: | inst(T as TFree _) = T wenzelm@256: | inst(T as TVar(v, _)) = wenzelm@256: (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 wenzelm@256: arguments if the type is declared in 'coreg' of the wenzelm@256: given type signature *) clasohm@0: wenzelm@256: fun least_sort (tsig as TySg{subclass, coreg, ...}) = wenzelm@256: let fun ls(T as Type(a, Ts)) = wenzelm@256: (case assoc (coreg, a) of wenzelm@256: Some(ars) => cod_above(subclass, map ls Ts, ars) wenzelm@256: | None => raise TYPE(undcl_type a, [T], [])) wenzelm@256: | ls(TFree(a, S)) = S wenzelm@256: | ls(TVar(a, S)) = S clasohm@0: in ls end; clasohm@0: clasohm@0: wenzelm@256: fun check_has_sort(tsig as TySg{subclass, coreg, ...}, T, S) = wenzelm@256: if sortorder subclass ((least_sort tsig T), S) then () wenzelm@256: else raise TYPE("Type not of sort " ^ (str_of_sort S), [T], []) clasohm@0: clasohm@0: clasohm@0: (*Instantiation of type variables in types *) wenzelm@256: fun inst_typ_tvars(tsig, tye) = wenzelm@256: let fun inst(Type(a, Ts)) = Type(a, map inst Ts) wenzelm@256: | inst(T as TFree _) = T wenzelm@256: | inst(T as TVar(v, S)) = (case assoc(tye, v) of wenzelm@256: 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 *) wenzelm@256: fun inst_term_tvars(tsig, tye) = map_term_types (inst_typ_tvars(tsig, tye)); nipkow@200: nipkow@200: nipkow@200: (* expand_typ *) nipkow@200: wenzelm@256: fun expand_typ (TySg {abbrs, ...}) ty = wenzelm@256: let wenzelm@256: fun exptyp (Type (a, Ts)) = wenzelm@256: (case assoc (abbrs, a) of wenzelm@256: Some (vs, U) => exptyp (inst_typ (vs ~~ Ts) U) wenzelm@256: | None => Type (a, map exptyp Ts)) wenzelm@256: | exptyp T = T wenzelm@256: in wenzelm@256: exptyp ty wenzelm@256: end; wenzelm@256: wenzelm@256: wenzelm@256: (* norm_typ *) (* FIXME norm sorts *) wenzelm@256: wenzelm@256: val norm_typ = expand_typ; wenzelm@256: wenzelm@256: wenzelm@256: wenzelm@256: (** type matching **) nipkow@200: clasohm@0: exception TYPE_MATCH; clasohm@0: wenzelm@256: (*typ_match (s, (U, T)) = s' <==> s'(U) = T and s' is an extension of s*) wenzelm@256: fun typ_match tsig = wenzelm@256: let wenzelm@256: fun match (subs, (TVar (v, S), T)) = wenzelm@256: (case assoc (subs, v) of wenzelm@256: None => ((v, (check_has_sort (tsig, T, S); T)) :: subs wenzelm@256: handle TYPE _ => raise TYPE_MATCH) wenzelm@256: | Some U => if U = T then subs else raise TYPE_MATCH) (* FIXME ??? *) wenzelm@256: | match (subs, (Type (a, Ts), Type (b, Us))) = wenzelm@256: if a <> b then raise TYPE_MATCH wenzelm@256: else foldl match (subs, Ts ~~ Us) wenzelm@256: | match (subs, (TFree x, TFree y)) = (* FIXME assert equal sorts, don't compare sorts *) wenzelm@256: if x = y then subs else raise TYPE_MATCH wenzelm@256: | match _ = raise TYPE_MATCH; wenzelm@256: in match end; clasohm@0: clasohm@0: wenzelm@256: fun typ_instance (tsig, T, U) = wenzelm@256: (typ_match tsig ([], (U, T)); true) handle TYPE_MATCH => false; wenzelm@256: wenzelm@256: wenzelm@256: (*(* FIXME old *) wenzelm@256: fun typ_instance (tsig, T, U) = wenzelm@256: let val x = typ_match tsig ([], (U, T)) in true end wenzelm@256: handle TYPE_MATCH => false; wenzelm@256: *) wenzelm@256: wenzelm@256: wenzelm@256: wenzelm@256: (** build type signatures **) wenzelm@256: wenzelm@256: val tsig0 = wenzelm@256: TySg { wenzelm@256: classes = [], wenzelm@256: subclass = [], wenzelm@256: default = [], wenzelm@256: args = [], wenzelm@256: abbrs = [], wenzelm@256: coreg = []}; wenzelm@256: 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: wenzelm@256: fun tyab_conflict(a) = error("Can't declare type "^(quote a)^"!\nAn abbreviation with this name exists already."); clasohm@0: clasohm@0: wenzelm@256: (* typ_errors *) (* FIXME check, improve *) wenzelm@256: wenzelm@256: (*check validity of (not necessarily normal) type; wenzelm@256: accumulates error messages in "errs"*) wenzelm@256: wenzelm@256: fun typ_errors (TySg {classes, args, abbrs, ...}) ty = wenzelm@256: let wenzelm@256: fun class_err (errs, C) = wenzelm@256: if C mem classes then errs wenzelm@256: else undcl_class C :: errs; wenzelm@256: wenzelm@256: val sort_err = foldl class_err; clasohm@0: wenzelm@256: fun typ_errs (Type (c, Us), errs) = wenzelm@256: let wenzelm@256: val errs' = foldr typ_errs (Us, errs); wenzelm@256: fun nargs n = wenzelm@256: if n = length Us then errs' wenzelm@256: else ("Wrong number of arguments: " ^ quote c) :: errs'; wenzelm@256: in wenzelm@256: (case assoc (args, c) of wenzelm@256: Some n => nargs n wenzelm@256: | None => wenzelm@256: (case assoc (abbrs, c) of wenzelm@256: Some (vs, _) => nargs (length vs) wenzelm@256: | None => undcl_type c :: errs)) wenzelm@256: end wenzelm@256: | typ_errs (TFree (_, S), errs) = sort_err (errs, S) wenzelm@256: | typ_errs (TVar (_, S), errs) = sort_err (errs, S); (* FIXME index >= 0 (?) *) wenzelm@256: in wenzelm@256: typ_errs ty wenzelm@256: end; wenzelm@256: wenzelm@256: wenzelm@256: (* cert_typ *) wenzelm@256: wenzelm@256: (*check and normalize typ wrt. tsig; errors are indicated by exception TYPE*) wenzelm@256: wenzelm@256: fun cert_typ tsig ty = wenzelm@256: (case typ_errors tsig (ty, []) of wenzelm@256: [] => norm_typ tsig ty wenzelm@256: | errs => raise_type (cat_lines errs) [ty] []); wenzelm@256: wenzelm@256: wenzelm@256: wenzelm@256: (* 'add_class' adds a new class to the list of all existing classes *) wenzelm@256: wenzelm@256: 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 wenzelm@256: superclasses (they must be declared in 'classes' too) to the 'subclass' wenzelm@256: list of the given type signature; wenzelm@256: 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: wenzelm@256: fun add_subclass classes (subclass, (s, ges)) = wenzelm@256: let fun upd (subclass, s') = if s' mem classes then wenzelm@256: let val Some(ges') = assoc (subclass, s) wenzelm@256: in case assoc (subclass, s') of clasohm@0: Some(sups) => if s mem sups clasohm@0: then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s ) wenzelm@256: else overwrite (subclass, (s, sups union ges')) clasohm@0: | None => subclass clasohm@0: end wenzelm@256: else err_undcl_class(s') wenzelm@256: in foldl upd (subclass@[(s, ges)], ges) end; clasohm@0: clasohm@0: clasohm@0: (* 'extend_classes' inserts all new classes into the corresponding wenzelm@256: lists ('classes', 'subclass') if possible *) clasohm@0: wenzelm@256: fun extend_classes (classes, subclass, newclasses) = wenzelm@256: if newclasses = [] then (classes, subclass) else wenzelm@256: let val classes' = foldl add_class (classes, newclasses); wenzelm@256: val subclass' = foldl (add_subclass classes') (subclass, newclasses); wenzelm@256: in (classes', subclass') end; wenzelm@256: clasohm@0: clasohm@0: (* Corregularity *) clasohm@0: clasohm@0: (* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *) clasohm@0: wenzelm@256: fun is_unique_decl coreg (t, (s, w)) = case assoc2 (coreg, (t, s)) of clasohm@0: Some(w1) => if w = w1 then () else wenzelm@256: error("There are two declarations\n" ^ wenzelm@256: str_of_decl(t, w, s) ^ " and\n" ^ wenzelm@256: 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: wenzelm@256: fun subs (classes, subclass) C = wenzelm@256: let fun sub (rl, l) = if leq subclass (l, C) then l::rl else rl wenzelm@256: in foldl sub ([], classes) end; clasohm@0: wenzelm@256: fun coreg_err(t, (w1, C), (w2, D)) = wenzelm@256: error("Declarations " ^ str_of_decl(t, w1, C) ^ " and " wenzelm@256: ^ str_of_decl(t, w2, D) ^ " are in conflict"); clasohm@0: wenzelm@256: fun restr2 classes (subclass, coreg) (t, (s, w)) = wenzelm@256: let fun restr ([], test) = () wenzelm@256: | restr (s1::Ss, test) = (case assoc2 (coreg, (t, s1)) of wenzelm@256: Some (dom) => if lew subclass (test (w, dom)) then restr (Ss, test) wenzelm@256: else coreg_err (t, (w, s), (dom, s1)) wenzelm@256: | None => restr (Ss, test)) wenzelm@256: fun forward (t, (s, w)) = wenzelm@256: let val s_sups = case assoc (subclass, s) of wenzelm@256: Some(s_sups) => s_sups | None => err_undcl_class(s); wenzelm@256: in restr (s_sups, I) end wenzelm@256: fun backward (t, (s, w)) = wenzelm@256: let val s_subs = subs (classes, subclass) s wenzelm@256: in restr (s_subs, fn (x, y) => (y, x)) end wenzelm@256: in (backward (t, (s, w)); forward (t, (s, w))) end; clasohm@0: clasohm@0: wenzelm@256: fun varying_decls t = wenzelm@256: error ("Type constructor " ^ quote t ^ " has varying number of arguments"); clasohm@0: clasohm@0: clasohm@0: (* 'coregular' checks clasohm@0: - the two restriction conditions 'is_unique_decl' and 'restr2' wenzelm@256: - 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; wenzelm@256: 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: wenzelm@256: fun coregular (classes, subclass, args) = wenzelm@256: let fun ex C = if C mem classes then () else err_undcl_class(C); clasohm@0: wenzelm@256: fun addar(w, C) (coreg, t) = case assoc(args, t) of clasohm@0: Some(n) => if n <> length w then varying_decls(t) else wenzelm@256: (is_unique_decl coreg (t, (C, w)); wenzelm@256: (seq o seq) ex w; wenzelm@256: restr2 classes (subclass, coreg) (t, (C, w)); wenzelm@256: let val Some(ars) = assoc(coreg, t) wenzelm@256: in overwrite(coreg, (t, (C, w) ins ars)) end) wenzelm@256: | None => err_undcl_type(t); clasohm@0: wenzelm@256: 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 wenzelm@256: for all range classes more general than C *) wenzelm@256: wenzelm@256: fun close (coreg, subclass) = wenzelm@256: let fun check sl (l, (s, dom)) = case assoc (subclass, s) of clasohm@0: Some(sups) => wenzelm@256: let fun close_sup (l, sup) = wenzelm@256: if exists (fn s'' => less subclass (s, s'') andalso wenzelm@256: leq subclass (s'', sup)) sl clasohm@0: then l wenzelm@256: else (sup, dom)::l wenzelm@256: in foldl close_sup (l, sups) end clasohm@0: | None => l; wenzelm@256: fun ext (s, l) = (s, foldl (check (map #1 l)) (l, l)); clasohm@0: in map ext coreg end; clasohm@0: wenzelm@256: fun add_types(aca, (ts, n)) = wenzelm@256: let fun add_type((args, coreg, abbrs), t) = case assoc(args, t) of wenzelm@256: Some _ => twice(t) wenzelm@256: | None => (case assoc(abbrs, t) of Some _ => tyab_conflict(t) wenzelm@256: | None => ((t, n)::args, (t, [])::coreg, abbrs)) clasohm@0: in if n<0 clasohm@0: then error("Type constructor cannot have negative number of arguments") wenzelm@256: else foldl add_type (aca, ts) clasohm@0: end; clasohm@0: wenzelm@256: wenzelm@256: wenzelm@256: (* ext_tsig_abbrs *) (* FIXME clean, check, improve *) wenzelm@256: nipkow@200: (* check_abbr *) nipkow@200: wenzelm@256: fun check_abbr ((a, (lhs_vs, U)), tsig as TySg {args, abbrs, ...}) = wenzelm@256: let wenzelm@256: val rhs_vs = map #1 (add_typ_tvars (U, [])); wenzelm@256: fun err_abbr a = "Error in type abbreviation " ^ quote a; wenzelm@256: in wenzelm@256: if not (rhs_vs subset lhs_vs) wenzelm@256: then [err_abbr a, ("Extra variables on rhs")] (* FIXME improve *) wenzelm@256: else wenzelm@256: (case duplicates lhs_vs of wenzelm@256: dups as _ :: _ => wenzelm@256: [err_abbr a, "Duplicate variables on lhs: " ^ commas (map (quote o #1) dups)] (* FIXME string_of_vname *) wenzelm@256: | [] => wenzelm@256: if is_some (assoc (args, a)) then wenzelm@256: [err_abbr a, ("A type with this name already exists")] wenzelm@256: else if is_some (assoc (abbrs, a)) then wenzelm@256: [err_abbr a, ("An abbreviation with this name already exists")] wenzelm@256: else (* FIXME remove (?) or move up! *) wenzelm@256: (case typ_errors tsig (U, []) of wenzelm@256: [] => [] wenzelm@256: | errs => err_abbr a :: errs)) nipkow@200: end; nipkow@200: wenzelm@256: (* FIXME improve *) wenzelm@256: (* FIXME set all sorts to [] (?) *) wenzelm@256: fun add_abbr (tsig as TySg {classes, default, subclass, args, coreg, abbrs}, newabbr) = wenzelm@256: (case check_abbr (newabbr, tsig) of wenzelm@256: [] => TySg {classes = classes, default = default, subclass = subclass, wenzelm@256: args = args, coreg = coreg, abbrs = newabbr :: abbrs} wenzelm@256: | errs => error (cat_lines errs)); (* FIXME error!? *) nipkow@200: wenzelm@256: fun ext_tsig_abbrs tsig abbrs = foldl add_abbr (tsig, abbrs); nipkow@200: nipkow@200: wenzelm@256: (* 'extend_tsig' 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: wenzelm@256: fun extend_tsig (TySg{classes, default, subclass, args, coreg, abbrs}) wenzelm@256: (newclasses, newdefault, types, arities) = wenzelm@256: let val (classes', subclass') = extend_classes(classes, subclass, newclasses); wenzelm@256: val (args', coreg', _) = foldl add_types ((args, coreg, abbrs), types); clasohm@0: val old_coreg = map #1 coreg; wenzelm@256: fun is_old(c) = if c mem old_coreg then () else err_undcl_type(c); clasohm@0: fun is_new(c) = if c mem old_coreg then twice(c) else (); wenzelm@256: val coreg'' = foldl (coregular (classes', subclass', args')) wenzelm@256: (coreg', min_domain subclass' arities); wenzelm@256: val coreg''' = close (coreg'', subclass'); clasohm@0: val default' = if null newdefault then default else newdefault; wenzelm@256: in TySg{classes=classes', default=default', subclass=subclass', args=args', wenzelm@256: coreg=coreg''', abbrs=abbrs} 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: wenzelm@256: fun assoc_union (as1, []) = as1 wenzelm@256: | assoc_union (as1, (key, l2)::as2) = case assoc (as1, key) of wenzelm@256: Some(l1) => assoc_union (overwrite(as1, (key, l1 union l2)), as2) wenzelm@256: | 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 wenzelm@256: all elements of the second list into the first one *) clasohm@0: clasohm@0: fun merge_coreg classes subclass1 = wenzelm@256: let fun test_ar classes (t, ars1) (coreg1, (s, w)) = wenzelm@256: (is_unique_decl coreg1 (t, (s, w)); wenzelm@256: restr2 classes (subclass1, coreg1) (t, (s, w)); wenzelm@256: overwrite (coreg1, (t, (s, w) ins ars1))); clasohm@0: wenzelm@256: fun merge_c (coreg1, (c as (t, ars2))) = case assoc (coreg1, t) of wenzelm@256: Some(ars1) => foldl (test_ar classes (t, ars1)) (coreg1, ars2) clasohm@0: | None => c::coreg1 clasohm@0: in foldl merge_c end; clasohm@0: wenzelm@256: fun merge_args(args, (t, n)) = case assoc(args, t) of clasohm@0: Some(m) => if m=n then args else varying_decls(t) wenzelm@256: | None => (t, n)::args; clasohm@0: wenzelm@256: (* FIXME raise ... *) wenzelm@256: fun merge_abbrs (abbrs1, abbrs2) = wenzelm@256: let wenzelm@256: val abbrs = abbrs1 union abbrs2; wenzelm@256: val names = map fst abbrs; wenzelm@256: in wenzelm@256: (case duplicates names of wenzelm@256: [] => abbrs wenzelm@256: | dups => error ("Duplicate declaration of type abbreviations: " ^ wenzelm@256: commas (map quote dups))) wenzelm@256: end; clasohm@0: wenzelm@256: wenzelm@256: (* 'merge_tsigs' takes the above declared functions to merge two type signatures *) wenzelm@256: wenzelm@256: fun merge_tsigs(TySg{classes=classes1, default=default1, subclass=subclass1, args=args1, wenzelm@256: coreg=coreg1, abbrs=abbrs1}, wenzelm@256: TySg{classes=classes2, default=default2, subclass=subclass2, args=args2, wenzelm@256: coreg=coreg2, abbrs=abbrs2}) = clasohm@0: let val classes' = classes1 union classes2; wenzelm@256: val subclass' = trcl (assoc_union (subclass1, subclass2)); wenzelm@256: val args' = foldl merge_args (args1, args2) wenzelm@256: val coreg' = merge_coreg classes' subclass' (coreg1, coreg2); nipkow@200: val default' = min_sort subclass' (default1 @ default2); wenzelm@256: val abbrs' = merge_abbrs(abbrs1, abbrs2); wenzelm@256: in TySg{classes=classes' , default=default', subclass=subclass', args=args', wenzelm@256: coreg=coreg' , abbrs = abbrs' } 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: wenzelm@256: 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 = wenzelm@256: let fun occ(Type(_, Ts)) = exists occ Ts clasohm@0: | occ(TFree _) = false wenzelm@256: | occ(TVar(w, _)) = v=w orelse wenzelm@256: (case assoc(tye, w) of clasohm@0: None => false clasohm@0: | Some U => occ U); clasohm@0: in occ end; clasohm@0: wenzelm@256: (*Chase variable assignments in tye. wenzelm@256: If devar (T, tye) returns a type var then it must be unassigned.*) wenzelm@256: fun devar (T as TVar(v, _), tye) = (case assoc(tye, v) of wenzelm@256: Some U => devar (U, tye) clasohm@0: | None => T) wenzelm@256: | 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: wenzelm@256: 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: wenzelm@256: fun Dom (subclass, coreg) (t, S) = clasohm@0: let val domlist = map (dom coreg t) S; clasohm@0: in if null domlist then [] wenzelm@256: else foldl (elementwise_union subclass) (hd domlist, tl domlist) clasohm@0: end; clasohm@0: clasohm@0: wenzelm@256: fun W ((T, S), tsig as TySg{subclass, coreg, ...}, tye) = wenzelm@256: let fun Wd ((T, S), tye) = W ((devar (T, tye), S), tsig, tye) wenzelm@256: fun Wk(T as TVar(v, S')) = wenzelm@256: if sortorder subclass (S', S) then tye wenzelm@256: else (v, gen_tyvar(union_sort subclass (S', S)))::tye wenzelm@256: | Wk(T as TFree(v, S')) = if sortorder subclass (S', S) then tye wenzelm@256: else raise TUNIFY wenzelm@256: | Wk(T as Type(f, Ts)) = wenzelm@256: if null S then tye wenzelm@256: 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 *) wenzelm@256: fun unify (tsig as TySg{subclass, coreg, ...}) = wenzelm@256: let fun unif ((T, U), tye) = wenzelm@256: case (devar(T, tye), devar(U, tye)) of wenzelm@256: (T as TVar(v, S1), U as TVar(w, S2)) => clasohm@0: if v=w then tye else wenzelm@256: if sortorder subclass (S1, S2) then (w, T)::tye else wenzelm@256: if sortorder subclass (S2, S1) then (v, U)::tye wenzelm@256: else let val nu = gen_tyvar (union_sort subclass (S1, S2)) wenzelm@256: in (v, nu)::(w, nu)::tye end wenzelm@256: | (T as TVar(v, S), U) => wenzelm@256: if occ v tye U then raise TUNIFY else W ((U, S), tsig, (v, U)::tye) wenzelm@256: | (U, T as TVar (v, S)) => wenzelm@256: if occ v tye U then raise TUNIFY else W ((U, S), tsig, (v, U)::tye) wenzelm@256: | (Type(a, Ts), Type(b, Us)) => wenzelm@256: if a<>b then raise TUNIFY else foldr unif (Ts~~Us, tye) wenzelm@256: | (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 = wenzelm@256: let fun inf(Ts, Const (_, T), tye) = (T, tye) wenzelm@256: | inf(Ts, Free (_, T), tye) = (T, tye) wenzelm@256: | inf(Ts, Bound i, tye) = ((nth_elem(i, Ts) , tye) clasohm@0: handle LIST _=> raise TYPE ("loose bound variable", [], [Bound i])) wenzelm@256: | inf(Ts, Var (_, T), tye) = (T, tye) wenzelm@256: | inf(Ts, Abs (_, T, body), tye) = wenzelm@256: let val (U, tye') = inf(T::Ts, body, tye) in (T-->U, tye') end clasohm@0: | inf(Ts, f$u, tye) = wenzelm@256: let val (U, tyeU) = inf(Ts, u, tye); wenzelm@256: 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]) wenzelm@256: in case T of wenzelm@256: Type("fun", [T1, T2]) => wenzelm@256: ( (T2, unify tsig ((T1, U), tyeT)) clasohm@0: handle TUNIFY => err"type mismatch in application" ) wenzelm@256: | 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: wenzelm@256: fun freeze_vars(Type(a, Ts)) = Type(a, map freeze_vars Ts) clasohm@0: | freeze_vars(T as TFree _) = T wenzelm@256: | freeze_vars(TVar(v, S)) = TFree(Syntax.string_of_vname v, S); clasohm@0: clasohm@0: (* Attach a type to a constant *) wenzelm@256: 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.*) wenzelm@256: fun new_id_type a = TVar(("'"^a, new_tvar_inx()), []); wenzelm@256: fun type_of_ixn(types, ixn as (a, _)) = wenzelm@256: case types ixn of Some T => freeze_vars T | None => TVar(("'"^a, ~1), []); clasohm@0: wenzelm@256: fun constrain(term, T) = Const(Syntax.constrainC, T-->T) $ term; wenzelm@256: fun constrainAbs(Abs(a, _, body), T) = Abs(a, T, body); wenzelm@256: clasohm@0: clasohm@0: (* wenzelm@256: Attach types to a term. Input is a "parse tree" containing dummy types. wenzelm@256: Type constraints are translated and checked for validity wrt tsig. TVars in wenzelm@256: constraints are frozen. clasohm@0: wenzelm@256: The atoms in the resulting term satisfy the following spec: clasohm@0: wenzelm@256: Const (a, T): wenzelm@256: T is a renamed copy of the generic type of a; renaming decreases index of wenzelm@256: all TVars by new_tvar_inx(), which is less than ~1. The index of all wenzelm@256: TVars in the generic type must be 0 for this to work! clasohm@0: wenzelm@256: Free (a, T), Var (ixn, T): wenzelm@256: T is either the frozen default type of a or TVar (("'"^a, ~1), []) clasohm@0: wenzelm@256: Abs (a, T, _): wenzelm@256: T is either a type constraint or TVar (("'" ^ a, i), []), where i is wenzelm@256: generated by new_tvar_inx(). Thus different abstractions can have the wenzelm@256: bound variables of the same name but different types. clasohm@0: *) clasohm@0: wenzelm@256: (* FIXME replace const_tab by (const_typ: string -> typ option) (?) *) wenzelm@256: (* FIXME improve handling of sort constraints *) wenzelm@256: wenzelm@256: fun add_types (tsig, const_tab, types, sorts) = wenzelm@256: let wenzelm@256: val S0 = defaultS tsig; wenzelm@256: fun defS0 ixn = if_none (sorts ixn) S0; wenzelm@256: wenzelm@256: fun prepareT typ = wenzelm@256: freeze_vars (cert_typ tsig (Syntax.typ_of_term defS0 typ)); wenzelm@256: wenzelm@256: fun add (Const (a, _)) = wenzelm@256: (case Symtab.lookup (const_tab, a) of wenzelm@256: Some T => type_const (a, T) wenzelm@256: | None => raise_type ("No such constant: " ^ quote a) [] []) wenzelm@256: | add (Bound i) = Bound i wenzelm@256: | add (Free (a, _)) = wenzelm@256: (case Symtab.lookup (const_tab, a) of wenzelm@256: Some T => type_const (a, T) wenzelm@256: | None => Free (a, type_of_ixn (types, (a, ~1)))) wenzelm@256: | add (Var (ixn, _)) = Var (ixn, type_of_ixn (types, ixn)) wenzelm@256: | add (Abs (a, _, body)) = Abs (a, new_id_type a, add body) wenzelm@256: | add ((f as Const (a, _) $ t1) $ t2) = wenzelm@256: if a = Syntax.constrainC then wenzelm@256: constrain (add t1, prepareT t2) wenzelm@256: else if a = Syntax.constrainAbsC then wenzelm@256: constrainAbs (add t1, prepareT t2) wenzelm@256: else add f $ add t2 wenzelm@256: | add (f $ t) = add f $ add t; wenzelm@256: 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" *) wenzelm@256: fun unconstrain (Abs(a, T, t)) = Abs(a, T, unconstrain t) wenzelm@256: | 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 = wenzelm@256: let val fs = add_term_tfree_names(t, []); wenzelm@256: val inxs = filter p (add_term_tvar_ixns(t, [])); clasohm@0: val vmap = inxs ~~ variantlist(map #1 inxs, fs); wenzelm@256: fun free(Type(a, Ts)) = Type(a, map free Ts) wenzelm@256: | free(T as TVar(v, S)) = wenzelm@256: (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 *) wenzelm@256: fun thaw_vars(Type(a, Ts)) = Type(a, map thaw_vars Ts) wenzelm@256: | thaw_vars(T as TFree(a, S)) = (case explode a of wenzelm@256: "?"::"'"::vn => let val ((b, i), _) = Syntax.scan_varname vn wenzelm@256: in TVar(("'"^b, i), S) end wenzelm@256: | _ => T) clasohm@0: | thaw_vars(T) = T; clasohm@0: clasohm@0: clasohm@0: fun restrict tye = wenzelm@256: let fun clean(tye1, ((a, i), T)) = wenzelm@256: if i < 0 then tye1 else ((a, i), inst_typ tye T) :: tye1 wenzelm@256: 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: wenzelm@256: fun infer_term (tsig, const_tab, types, sorts, T, t) = wenzelm@256: let val u = add_types (tsig, const_tab, types, sorts) t; wenzelm@256: val (U, tye) = infer tsig ([], u, []); clasohm@0: val uu = unconstrain u; wenzelm@256: val tye' = unify tsig ((T, U), tye) handle TUNIFY => raise TYPE wenzelm@256: ("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 *) wenzelm@256: val Const(_, Type(_, Ts)) $ u'' = wenzelm@256: 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 "?" *) wenzelm@256: fun varifyT (Type (a, Ts)) = Type (a, map varifyT Ts) wenzelm@256: | varifyT (TFree (a, S)) = TVar ((a, 0), S) wenzelm@256: | varifyT T = T; clasohm@0: clasohm@0: (* Turn TFrees except those in fixed into new TVars *) wenzelm@256: fun varify (t, fixed) = wenzelm@256: let val fs = add_term_tfree_names(t, []) \\ fixed; wenzelm@256: val ixns = add_term_tvar_ixns(t, []); clasohm@0: val fmap = fs ~~ variantlist(fs, map #1 ixns) wenzelm@256: fun thaw(Type(a, Ts)) = Type(a, map thaw Ts) clasohm@0: | thaw(T as TVar _) = T wenzelm@256: | thaw(T as TFree(a, S)) = wenzelm@256: (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; wenzelm@256: