type decl = Types.type_declaration
type ('prop, 'req) property = {
eq : 'prop -> 'prop -> bool;
merge : prop:'prop -> new_prop:'prop -> 'prop;
default : decl -> 'prop;
compute : Env.t -> decl -> 'req -> 'prop;
update_decl : decl -> 'prop -> decl;
check : Env.t -> Ident.t -> decl -> 'req -> unit;
}
'prop
represents the type of property values (Types.Variance.t
, just 'bool' for immediacy, etc).'req
represents the property value required by the author of the declaration, if they gave an expectation:type +'a t = ...
.Some properties have no natural notion of user requirement, or their requirement is global, or already stored in
type_declaration
; they can just useunit
as'req
parameter.
val compute_property : ('prop, 'req) property -> Env.t -> (Ident.t * decl) list -> 'req list -> (Ident.t * decl) list
compute_property prop env decls req
performs a fixpoint computation to determine the final values of a property on a set of mutually-recursive type declarations. Thereq
argument must be a list of the same size asdecls
, providing the user requirement for each declaration.