canonical term algebra: labels, records, rationals, sequences

2 files changed, 50 insertions, 0 deletions

diff --git a/lib/label.ml b/lib/label.ml
new file mode 100644
index 0000000..acc3e49
--- /dev/null
+++ b/lib/label.ml
@@ -0,0 +1,19 @@
+type t = string
+
+let is_lower c = c >= 'a' && c <= 'z'
+
+let is_body c =
+  is_lower c || (c >= 'A' && c <= 'Z') || (c >= '0' && c <= '9') || c = '_'
+
+let well_formed s =
+  String.length s > 0
+  && is_lower s.[0]
+  && String.for_all is_body s
+
+let of_string s = if well_formed s then Ok s else Error (`Invalid_label s)
+let to_string t = t
+let equal = String.equal
+let compare = String.compare
+let pp fmt t = Format.fprintf fmt "%s:" t
+
+module Map = Map.Make (String)
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. *)