(** 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
  | Reference of string
      (** A relation reference, written [#Name]: a first-class
          value denoting a relation by name, resolved through the
          catalog of a state. Distinct from {!String} on purpose;
          identity is not representation. *)
  | 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 reference : string -> (t, [ `Invalid_reference of string ]) result
(** A relation reference. Validates the name: a letter, then
    letters, digits, or underscores. *)

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)]. *)