1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
(** 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)]. *)
|
