Parameter Make.NF

Module signature for normal form computations.

type constant

The type of constant values.

Atomic variables cannot be decomposed further.

val type_info : Atom.t -> Ty.t

type_info a returns the type of atomic variable x.

Composite variables are obtained through a combination of atomic variables (e.g. a multi-variate polynomial).

val fold_composite : (Atom.t -> 'a -> 'a) -> Composite.t -> 'a -> 'a

fold_composite f c acc folds f over all the atoms that make up c.

type t =
  1. | Constant of constant
    (*

    A constant value.

    *)
  2. | Atom of Atom.t * constant
    (*

    An atomic variable with a constant offset.

    *)
  3. | Composite of Composite.t * constant
    (*

    A composite variable with a constant offset.

    *)

The type of normal forms.

val normal_form : AltErgoLib.Domains_intf.X.r -> t

normal_form e computes the normal form of expression e.