canonical term algebra: labels, records, rationals, sequences

8 files changed, 405 insertions, 0 deletions

diff --git a/docs/terms.org b/docs/terms.org
new file mode 100644
index 0000000..638863d
--- /dev/null
+++ b/docs/terms.org
@@ -0,0 +1,48 @@
+#+TITLE: Terms
+
+* About
+
+This document describes =lib/label= and =lib/term=, the first modules
+of the Sol implementation. They realize the term algebra of the
+language specification and the canonical form discipline of decision
+12 in the integration document.
+
+* Labels
+
+A label names an attribute, like =age:= or =dept_id:=. The module
+validates on construction: lowercase first letter, then letters,
+digits or underscores. Since the type is sealed, holding a =Label.t=
+is proof the name is well formed. Labels carry a total order, and
+that order is what gives records a canonical attribute layout
+independent of how the source spelled them.
+
+* Terms
+
+A =Term.t= is a value of Sol: an integer, a rational, a string, the
+empty sequence =#()=, or a record (a labeled tuple). The type is
+exposed as private, so anyone can pattern match on it, but building
+one goes through the smart constructors. This is where the canonical
+form rules live:
+
+- rationals reduce by the gcd and carry the sign on the numerator;
+- a rational with denominator one collapses to the integer itself,
+  the minimal shape, so an integer valued rational is literally an
+  integer and inclusion of the integers in the rationals holds with
+  no coercion;
+- a denominator of zero is rejected at construction;
+- records reject duplicate labels instead of picking one, and reject
+  emptiness, since =#()= is the only empty term;
+- sequences are sugar: =#(1 2 3)= elaborates to nested
+  ={head: 1 tail: ...}= records ending in =#()=, exactly as the
+  specification publishes.
+
+Because every term is canonical by construction, structural equality
+is value equality. Content addressing later hashes terms directly and
+relies on this.
+
+* Printing
+
+Terms print back as Sol notation: =42=, =1/4=, ="Sun"=, =#()=,
+={a: 1 b: 2}=. A record chain shaped like a sequence prints as
+=#(1 2 3)=. An improper chain prints with an explicit dangling tail,
+=#(1 | X)=, so nothing pretends to be a proper list that is not.
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)]. *)
diff --git a/test/dune b/test/dune
new file mode 100644
index 0000000..66418bb
--- /dev/null
+++ b/test/dune
@@ -0,0 +1,3 @@
+(test
+ (name test_term)
+ (libraries sol zarith alcotest))
diff --git a/test/test_term.ml b/test/test_term.ml
new file mode 100644
index 0000000..20b2f1a
--- /dev/null
+++ b/test/test_term.ml
@@ -0,0 +1,126 @@
+let label s =
+  match Sol.Label.of_string s with
+  | Ok l -> l
+  | Error (`Invalid_label s) -> Alcotest.failf "invalid label in test: %s" s
+
+let term = Alcotest.testable Sol.Term.pp Sol.Term.equal
+
+let rational num den =
+  match Sol.Term.rational ~num:(Z.of_int num) ~den:(Z.of_int den) with
+  | Ok t -> t
+  | Error `Zero_denominator -> Alcotest.fail "unexpected zero denominator"
+
+let record bindings =
+  match Sol.Term.record bindings with
+  | Ok t -> t
+  | Error `Empty_record -> Alcotest.fail "unexpected empty record"
+  | Error (`Duplicate_label _) -> Alcotest.fail "unexpected duplicate label"
+
+let int n = Sol.Term.integer (Z.of_int n)
+
+(* Canonical forms: Decision 12, minimal shape. *)
+
+let test_rational_reduces () =
+  Alcotest.check term "2/4 = 1/2" (rational 1 2) (rational 2 4)
+
+let test_rational_collapses_to_integer () =
+  Alcotest.check term "4/2 = 2" (int 2) (rational 4 2);
+  Alcotest.check term "2/2 = 1" (int 1) (rational 2 2);
+  Alcotest.check term "0/5 = 0" (int 0) (rational 0 5)
+
+let test_rational_sign_normalizes () =
+  Alcotest.check term "1/-2 = -1/2" (rational (-1) 2) (rational 1 (-2));
+  Alcotest.check term "-1/-2 = 1/2" (rational 1 2) (rational (-1) (-2))
+
+let test_rational_zero_denominator () =
+  match Sol.Term.rational ~num:Z.one ~den:Z.zero with
+  | Error `Zero_denominator -> ()
+  | Ok _ -> Alcotest.fail "1/0 must be rejected"
+
+(* Records: label order is irrelevant, duplicates are rejected. *)
+
+let test_record_label_order_irrelevant () =
+  let ab = record [ (label "a", int 1); (label "b", int 2) ] in
+  let ba = record [ (label "b", int 2); (label "a", int 1) ] in
+  Alcotest.check term "{a: 1 b: 2} = {b: 2 a: 1}" ab ba
+
+let test_record_duplicate_rejected () =
+  match Sol.Term.record [ (label "a", int 1); (label "a", int 2) ] with
+  | Error (`Duplicate_label l) ->
+      Alcotest.(check string) "offending label" "a" (Sol.Label.to_string l)
+  | Ok _ -> Alcotest.fail "duplicate label must be rejected"
+  | Error `Empty_record -> Alcotest.fail "wrong error"
+
+let test_record_empty_rejected () =
+  match Sol.Term.record [] with
+  | Error `Empty_record -> ()
+  | Ok _ | Error (`Duplicate_label _) ->
+      Alcotest.fail "empty record must be rejected"
+
+(* Sequences: the published elaboration into head/tail cells. *)
+
+let test_sequence_elaboration () =
+  let expected =
+    Sol.Term.cons ~head:(int 1)
+      ~tail:(Sol.Term.cons ~head:(int 2) ~tail:Sol.Term.nil)
+  in
+  Alcotest.check term "#(1 2) elaborates to nested cells" expected
+    (Sol.Term.sequence [ int 1; int 2 ])
+
+let test_empty_sequence_is_nil () =
+  Alcotest.check term "#() is Nil" Sol.Term.nil (Sol.Term.sequence [])
+
+(* Printing: Sol notation back out. *)
+
+let print t = Format.asprintf "%a" Sol.Term.pp t
+
+let test_printing () =
+  Alcotest.(check string) "integer" "42" (print (int 42));
+  Alcotest.(check string) "rational" "1/4" (print (rational 1 4));
+  Alcotest.(check string) "string" {|"Sun"|} (print (Sol.Term.string "Sun"));
+  Alcotest.(check string) "empty sequence" "#()" (print Sol.Term.nil);
+  Alcotest.(check string) "sequence" "#(1 2 3)"
+    (print (Sol.Term.sequence [ int 1; int 2; int 3 ]));
+  Alcotest.(check string) "record" "{a: 1 b: 2}"
+    (print (record [ (label "b", int 2); (label "a", int 1) ]))
+
+let test_label_validation () =
+  let ok s = Result.is_ok (Sol.Label.of_string s) in
+  Alcotest.(check bool) "dept_id" true (ok "dept_id");
+  Alcotest.(check bool) "empty" false (ok "");
+  Alcotest.(check bool) "capitalized" false (ok "Name");
+  Alcotest.(check bool) "leading digit" false (ok "1a")
+
+let () =
+  Alcotest.run "sol"
+    [
+      ( "canonical forms",
+        [
+          Alcotest.test_case "rational reduces" `Quick test_rational_reduces;
+          Alcotest.test_case "integer-valued rational is an integer" `Quick
+            test_rational_collapses_to_integer;
+          Alcotest.test_case "sign normalizes" `Quick
+            test_rational_sign_normalizes;
+          Alcotest.test_case "zero denominator rejected" `Quick
+            test_rational_zero_denominator;
+        ] );
+      ( "records",
+        [
+          Alcotest.test_case "label order irrelevant" `Quick
+            test_record_label_order_irrelevant;
+          Alcotest.test_case "duplicate label rejected" `Quick
+            test_record_duplicate_rejected;
+          Alcotest.test_case "empty record rejected" `Quick
+            test_record_empty_rejected;
+        ] );
+      ( "sequences",
+        [
+          Alcotest.test_case "elaboration" `Quick test_sequence_elaboration;
+          Alcotest.test_case "empty is nil" `Quick test_empty_sequence_is_nil;
+        ] );
+      ( "notation",
+        [
+          Alcotest.test_case "printing" `Quick test_printing;
+          Alcotest.test_case "label validation" `Quick test_label_validation;
+        ] );
+    ]