Module Typedecl_properties

An abstract interface for properties of type definitions, such as variance and immediacy, that are computed by a fixpoint on mutually-recursive type declarations. This interface contains all the operations needed to initialize and run the fixpoint computation, and then (optionally) check that the result is consistent with the declaration or user expectations.

type ('prop, 'req) property = {
  1. eq : 'prop -> 'prop -> bool;
  2. merge : prop:'prop -> new_prop:'prop -> 'prop;
  3. default : decl -> 'prop;
  4. compute : Env.t -> decl -> 'req -> 'prop;
  5. update_decl : decl -> 'prop -> decl;
  6. 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