aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--docs/terms.org48
-rw-r--r--lib/dune4
-rw-r--r--lib/label.ml19
-rw-r--r--lib/label.mli31
-rw-r--r--lib/term.ml113
-rw-r--r--lib/term.mli61
-rw-r--r--test/dune3
-rw-r--r--test/test_term.ml126
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;
+ ] );
+ ]
generated by cgit v1.2.3 (git 2.25.1) at 2026-11-04 05:42:53 +0000