1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
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;
] );
]
|
