Module Typedecl_properties

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 use unit 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. The req argument must be a list of the same size as decls, providing the user requirement for each declaration.

val compute_property_noreq : ('prop, unit) property -> Env.t -> (Ident.t * decl) list -> (Ident.t * decl) list