module Make (T : TermInner.S) : sig .. end
type T.t
type 'a env = ('a, ty) Env.t
We only consider monomorphic types
type
Cache for memoizing cardinality computations
val create_cache : ?default_card:int -> unit -> cache
default_card : if provided, the uninterpreted types we
know nothing about will be considered as having this card
val cardinality_ty : ?cache:cache ->
'a env -> ty -> Cardinality.t
cardinality_ty ty computes the cardinality of the type
ty, which
must be monomorphic.
RaisesEmptyData if there is some ill-defined data in envPolymorphic if the type is polymorphic,
or depends on polymorphic types
val cardinality_ty_id : ?cache:cache ->
'a env -> ID.t -> Cardinality.t
cardinality id computes the cardinality of the type
named
id.
RaisesEmptyData if there is some ill-defined data in envError if id is not a valid type in envPolymorphic if the type is polymorphic,
or depends on polymorphic types
val check_non_zero : ?cache:cache ->
'a env -> ('a, ty) Statement.t -> unit
check_non_zero env stmt checks that stmt is not a definition of
an empty datatype
val is_incomplete : 'a env -> ty -> bool
Is the type incomplete, that is, some values from the input type
are not present in this encoding?
val is_abstract : 'a env -> ty -> bool
Is the type a quotient over the input types (i.e. several distinct
values of the input types are encoded as one value)?