From b4a2485afbf74e99e2147086fbca0568b7e2b7b8 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sun, 12 Jul 2026 17:55:27 -0300 Subject: relation references as a term kind, written #Name --- lib/term.mli | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'lib/term.mli') diff --git a/lib/term.mli b/lib/term.mli index cf79d89..8dc201e 100644 --- a/lib/term.mli +++ b/lib/term.mli @@ -17,6 +17,11 @@ type t = private 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 @@ -30,6 +35,10 @@ 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 -- cgit v1.2.3