canonical term algebra: labels, records, rationals, sequences

1 files changed, 61 insertions, 0 deletions

diff --git a/lib/term.mli b/lib/term.mli
new file mode 100644
index 0000000..cf79d89
--- /dev/null
+++ b/lib/term.mli
@@ -0,0 +1,61 @@
+(** 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)]. *)