Module Mlsem_types.Abstract

Abstract types: opaque parameterized type constructors, such as ref('a), whose parameters are invariant.

Abstract types: opaque parameterized type constructors, such as ref('a), whose parameters are invariant.

type t
val define : string -> int -> t

define name arity creates a fresh abstract type constructor.

val arity : t -> int
val any : t -> Ty.t
val mk : t -> Ty.t list -> Ty.t
val dnf : t -> Ty.t -> Ty.t list list list

The disjunctive normal form of the given abstract type's part of a type: a disjunction of conjunctions of parameter tuples.

val top_transform : ((t * (Ty.t list list * Ty.t list list) list) -> (Ty.t list list * Ty.t list list) list) -> Ty.t -> Ty.t

Rewrites the abstract atoms occurring at the top level of a type. The function receives, for one abstract constructor, its normal form as a list of (positive tuples, negative tuples) pairs.

val transform : ((t * (Ty.t list list * Ty.t list list) list) -> (Ty.t list list * Ty.t list list) list) -> Ty.t -> Ty.t

Like top_transform, but rewrites abstract atoms at every depth, including under other constructors and inside recursive types.