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
127
128
129
130
131
132
133
134
135
136
137
138
|
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) ]));
Alcotest.(check string) "reference" "#Person"
(print (Result.get_ok (Sol.Term.reference "Person")))
let test_reference_validation () =
Alcotest.(check bool) "well-formed" true
(Result.is_ok (Sol.Term.reference "Person"));
Alcotest.(check bool) "empty rejected" false
(Result.is_ok (Sol.Term.reference ""));
Alcotest.(check bool) "leading digit rejected" false
(Result.is_ok (Sol.Term.reference "1st"))
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;
Alcotest.test_case "reference validation" `Quick
test_reference_validation;
] );
]
|
