canonical term algebra: labels, records, rationals, sequences

1 files changed, 31 insertions, 0 deletions

diff --git a/lib/label.mli b/lib/label.mli
new file mode 100644
index 0000000..6f9f273
--- /dev/null
+++ b/lib/label.mli
@@ -0,0 +1,31 @@
+(** Attribute labels.
+
+    A label names an attribute of a record or a relation schema,
+    written [name:] in Sol source. Labels are the keys of every
+    {!Term.t} record, so the whole term algebra sits on them. *)
+
+type t
+(** A validated label. Values of this type always hold a well-formed
+    label name, by construction. *)
+
+val of_string : string -> (t, [ `Invalid_label of string ]) result
+(** The only way in. A well-formed label starts with a lowercase
+    letter, followed by letters, digits, or underscores. Everything
+    that builds or looks up record attributes goes through labels
+    made here. *)
+
+val to_string : t -> string
+(** The label name, without the colon. *)
+
+val equal : t -> t -> bool
+
+val compare : t -> t -> int
+(** Total order on names. Gives records a canonical attribute order
+    regardless of how the source spelled them, which {!Term.equal}
+    and content addressing rely on. *)
+
+val pp : Format.formatter -> t -> unit
+(** Prints [name:], as in Sol source. *)
+
+module Map : Map.S with type key = t
+(** Attribute maps, used by {!Term.t} records. *)