canonical term algebra: labels, records, rationals, sequences

5 files changed, 228 insertions, 0 deletions

diff --git a/lib/dune b/lib/dune
new file mode 100644
index 0000000..ca7e7b7
--- /dev/null
+++ b/lib/dune
@@ -0,0 +1,4 @@
+(library
+ (name sol)
+ (public_name sol)
+ (libraries zarith))
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. *)
diff --git a/lib/term.ml b/lib/term.ml
new file mode 100644
index 0000000..a0dc760
--- /dev/null
+++ b/lib/term.ml
@@ -0,0 +1,113 @@
+type t =
+  | Integer of Z.t
+  | Rational of Q.t
+  | String of string
+  | Nil
+  | Record of t Label.Map.t
+
+let integer z = Integer z
+let string s = String s
+let nil = Nil
+
+let rational ~num ~den =
+  if Z.equal den Z.zero then Error `Zero_denominator
+  else
+    (* Q.make reduces by the gcd and moves the sign to the
+       numerator; collapsing den = 1 to Integer is the minimal-shape
+       rule that makes integer inclusion literal. *)
+    let q = Q.make num den in
+    if Z.equal (Q.den q) Z.one then Ok (Integer (Q.num q))
+    else Ok (Rational q)
+
+let record bindings =
+  match bindings with
+  | [] -> Error `Empty_record
+  | _ ->
+      let step acc (label, term) =
+        match acc with
+        | Error _ as e -> e
+        | Ok map ->
+            if Label.Map.mem label map then Error (`Duplicate_label label)
+            else Ok (Label.Map.add label term map)
+      in
+      Result.map
+        (fun map -> Record map)
+        (List.fold_left step (Ok Label.Map.empty) bindings)
+
+(* The head/tail labels of sequence cells. Direct construction:
+   both spellings are well formed by inspection. *)
+let head_label =
+  match Label.of_string "head" with Ok l -> l | Error _ -> assert false
+
+let tail_label =
+  match Label.of_string "tail" with Ok l -> l | Error _ -> assert false
+
+let cons ~head ~tail =
+  Record Label.Map.(empty |> add head_label head |> add tail_label tail)
+
+let sequence items = List.fold_right (fun x acc -> cons ~head:x ~tail:acc) items Nil
+
+let rec compare a b =
+  match (a, b) with
+  | Integer x, Integer y -> Z.compare x y
+  | Rational x, Rational y -> Q.compare x y
+  | String x, String y -> String.compare x y
+  | Nil, Nil -> 0
+  | Record x, Record y -> Label.Map.compare compare x y
+  | Integer _, _ -> -1
+  | _, Integer _ -> 1
+  | Rational _, _ -> -1
+  | _, Rational _ -> 1
+  | String _, _ -> -1
+  | _, String _ -> 1
+  | Nil, _ -> -1
+  | _, Nil -> 1
+
+let equal a b = compare a b = 0
+
+(* A record prints as #( ... ) exactly when it is a cell of the
+   sequence elaboration: the two labels head and tail, nothing else. *)
+let as_cell = function
+  | Record map when Label.Map.cardinal map = 2 -> (
+      match
+        (Label.Map.find_opt head_label map, Label.Map.find_opt tail_label map)
+      with
+      | Some head, Some tail -> Some (head, tail)
+      | _ -> None)
+  | _ -> None
+
+let rec pp fmt t =
+  match t with
+  | Integer z -> Z.pp_print fmt z
+  | Rational q -> Q.pp_print fmt q
+  | String s -> Format.fprintf fmt "%S" s
+  | Nil -> Format.pp_print_string fmt "#()"
+  | Record map -> (
+      match as_cell t with
+      | Some (head, tail) -> pp_sequence fmt head tail
+      | None ->
+          Format.fprintf fmt "@[<hv 1>{";
+          let first = ref true in
+          Label.Map.iter
+            (fun label term ->
+              if not !first then Format.fprintf fmt "@ ";
+              first := false;
+              Format.fprintf fmt "%a %a" Label.pp label pp term)
+            map;
+          Format.fprintf fmt "}@]")
+
+and pp_sequence fmt head tail =
+  Format.fprintf fmt "@[<hv 2>#(%a" pp head;
+  let rec spine = function
+    | Nil -> ()
+    | t -> (
+        match as_cell t with
+        | Some (h, rest) ->
+            Format.fprintf fmt "@ %a" pp h;
+            spine rest
+        | None ->
+            (* An improper chain: honest about the dangling tail. *)
+            Format.fprintf fmt "@ | %a" pp t)
+  in
+  spine tail;
+  Format.fprintf fmt ")@]"
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)]. *)