Module Literal.Make

Parameters

module Sem : Xliteral.S

Signature

type elt = Sem.t

The type of semantic elements literals.

type t

The type of syntaxic or semantic literals.

val make : elt view -> t

Create a new literal given its view.

val view : t -> elt view

Extract a view from a literal (for pattern-matching).

val pp : t Fmt.t

Pretty-printer for literals.

val hash : t -> int

Hash function for literals.

val equal : t -> t -> bool

Equality of literals. Note that this does not try to look into the semantic content of syntaxic literals: x = y as a term and x = y as a semantic literal (where x and y are semantic values) are distinct.

val compare : t -> t -> int

Comparison function over literals. The order is unspecified.

val neg : t -> t

neg t is the boolean negation of t.

val normal_form : t -> t * bool

normal_form l returns the normal form of l. The normal form of l is a pair l', is_neg such that:

  • l' is neg l if is_neg is true
  • l' is l if is_neg is false
  • normal_form l' is l', false
val is_ground : t -> bool

normal_form l returns the normal form of l. The normal form of l is a pair l', is_neg such that:

  • l' is neg l if is_neg is true
  • l' is l if is_neg is false
  • normal_form l' is l', false

is_ground l is always true if l is a semantic literal, and otherwise is true iff the syntaxic literal is ground (does not contain free variables nor free type variables).

module Table : Stdlib.Hashtbl.S with type key = t

Hash tables over literals.

module Set : Stdlib.Set.S with type elt = t

Sets of literals.

module Map : Stdlib.Map.S with type key = t

Maps over literals.