diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/test_rnt.ml | 2 | ||||
| -rw-r--r-- | test/unit/concepts/Cardinality.ml | 24 |
2 files changed, 26 insertions, 0 deletions
diff --git a/test/test_rnt.ml b/test/test_rnt.ml index d9936ea..b9c5962 100644 --- a/test/test_rnt.ml +++ b/test/test_rnt.ml @@ -1,5 +1,7 @@ let all_suites = Unit.Backend.Storage.suites () + @ Unit.Concepts.Cardinality.suites () + @ Unit.Kernel.EphemeralRelation.suites () @ Unit.Kernel.Merkle.suites () @ Unit.Kernel.SubstantialRelation.suites () @ Unit.Evaluators.FOL.suites () diff --git a/test/unit/concepts/Cardinality.ml b/test/unit/concepts/Cardinality.ml new file mode 100644 index 0000000..a60c472 --- /dev/null +++ b/test/unit/concepts/Cardinality.ml @@ -0,0 +1,24 @@ +open Alcotest + +module C = Rnt.Concepts.Cardinality + +let klass = testable (fun ppf c -> Format.pp_print_string ppf (C.to_string c)) C.equal + +let chain () = + check bool "empty is least" true (C.leq C.Empty C.Countable); + check bool "a tighter ceiling is smaller" true (C.leq (C.Bounded 2) (C.Bounded 5)); + check bool "a ceiling is finite" true (C.leq (C.Bounded 5) C.Finite); + check bool "countable is greatest" true (C.leq C.Finite C.Countable); + check bool "and nothing above it" false (C.leq C.Countable C.Finite) + +let exhaustion () = + check bool "a bounded generator can be exhausted" true (C.exhaustible (C.Bounded 3)); + check bool "a countable one cannot" false (C.exhaustible C.Countable) + +let emptiness () = check klass "a ceiling of zero is emptiness" C.Empty (C.bounded 0) + +let suites () = + [ ( "concepts/cardinality", + [ test_case "chain" `Quick chain; + test_case "exhaustion" `Quick exhaustion; + test_case "emptiness" `Quick emptiness ] ) ] |