blob: cf79d89a6b7b483e7e004a536f9ded0ffc6e1ff8 (
plain) (
tree)
|
|
(** Canonical terms: the values of Sol.
Every literal denotes a member of a domain, and every composite
value is a labeled tuple (a record). A [t] is canonical by
construction: no reducible rational, no integer disguised as a
rational, no duplicate attribute. Structural equality is
therefore value equality, which content addressing relies on.
The constructors are exposed [private]: pattern match freely,
build only through the smart constructors below. *)
type t = private
| Integer of Z.t
| Rational of Q.t
(** Irreducible and with denominator strictly greater than
one. An integer-valued rational normalizes to {!Integer},
its minimal shape, so integer membership inclusion holds
literally. *)
| String of string
| Nil (** The empty sequence, written [#()]. *)
| Record of t Label.Map.t
(** A nonempty labeled tuple. Attribute order is canonical
(by {!Label.compare}), never source order. *)
val integer : Z.t -> t
val string : string -> t
val nil : t
(** The empty sequence, [#()]. The distinguished base every
{!sequence} chain ends in. *)
val rational : num:Z.t -> den:Z.t -> (t, [ `Zero_denominator ]) result
(** Normalizes on entry: reduces by the gcd, moves the sign to the
numerator, and collapses to {!Integer} when the reduced
denominator is one. [rational ~num:4 ~den:2] is [Integer 2]. *)
val record : (Label.t * t) list -> (t, [ `Empty_record | `Duplicate_label of Label.t ]) result
(** Builds a labeled tuple. Rejects duplicates rather than choosing
one, and rejects emptiness ({!Nil} is the only empty term). *)
val sequence : t list -> t
(** The published elaboration of [#(a b c)]: a right fold of
[{head: _ tail: _}] records ending in {!Nil}. *)
val cons : head:t -> tail:t -> t
(** One sequence cell, [{head: _ tail: _}]. [sequence] iterates
this; exposed for building improper or streamed chains. *)
val equal : t -> t -> bool
(** Value equality. Sound as plain structural comparison precisely
because every [t] is canonical. *)
val compare : t -> t -> int
(** A total order compatible with {!equal}. Exists to key maps and
to make serialization deterministic; it is not a semantic order
on domains. *)
val pp : Format.formatter -> t -> unit
(** Prints Sol notation: [123], [1/4], ["s"], [#()], [{a: 1 b: 2}].
A record chain shaped like a sequence prints as [#(1 2 3)]. *)
|
