canonical term algebra: labels, records, rationals, sequences

1 files changed, 126 insertions, 0 deletions

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;
+        ] );
+    ]