aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/spec
diff options
context:
space:
mode:
Diffstat (limited to 'stdlib/source/spec')
-rw-r--r--stdlib/source/spec/lux/abstract/apply.lux73
-rw-r--r--stdlib/source/spec/lux/abstract/codec.lux26
-rw-r--r--stdlib/source/spec/lux/abstract/enum.lux26
-rw-r--r--stdlib/source/spec/lux/abstract/equivalence.lux23
-rw-r--r--stdlib/source/spec/lux/abstract/fold.lux22
-rw-r--r--stdlib/source/spec/lux/abstract/functor.lux62
-rw-r--r--stdlib/source/spec/lux/abstract/interval.lux22
-rw-r--r--stdlib/source/spec/lux/abstract/monad.lux57
-rw-r--r--stdlib/source/spec/lux/abstract/monoid.lux31
-rw-r--r--stdlib/source/spec/lux/abstract/order.lux27
10 files changed, 369 insertions, 0 deletions
diff --git a/stdlib/source/spec/lux/abstract/apply.lux b/stdlib/source/spec/lux/abstract/apply.lux
new file mode 100644
index 000000000..4220de34c
--- /dev/null
+++ b/stdlib/source/spec/lux/abstract/apply.lux
@@ -0,0 +1,73 @@
+(.module:
+ [lux #*
+ [abstract
+ [monad (#+ do)]]
+ [data
+ [number
+ ["n" nat]]]
+ [control
+ ["." function]]
+ [math
+ ["." random]]
+ ["_" test (#+ Test)]]
+ {1
+ ["." / (#+ Apply)]}
+ [//
+ [functor (#+ Injection Comparison)]])
+
+(def: (identity injection comparison (^open "_@."))
+ (All [f] (-> (Injection f) (Comparison f) (Apply f) Test))
+ (do {@ random.monad}
+ [sample (:: @ map injection random.nat)]
+ (_.test "Identity."
+ ((comparison n.=)
+ (_@apply (injection function.identity) sample)
+ sample))))
+
+(def: (homomorphism injection comparison (^open "_@."))
+ (All [f] (-> (Injection f) (Comparison f) (Apply f) Test))
+ (do {@ random.monad}
+ [sample random.nat
+ increase (:: @ map n.+ random.nat)]
+ (_.test "Homomorphism."
+ ((comparison n.=)
+ (_@apply (injection increase) (injection sample))
+ (injection (increase sample))))))
+
+(def: (interchange injection comparison (^open "_@."))
+ (All [f] (-> (Injection f) (Comparison f) (Apply f) Test))
+ (do {@ random.monad}
+ [sample random.nat
+ increase (:: @ map n.+ random.nat)]
+ (_.test "Interchange."
+ ((comparison n.=)
+ (_@apply (injection increase) (injection sample))
+ (_@apply (injection (function (_ f) (f sample))) (injection increase))))))
+
+(def: (composition injection comparison (^open "_@."))
+ (All [f] (-> (Injection f) (Comparison f) (Apply f) Test))
+ (do {@ random.monad}
+ [sample random.nat
+ increase (:: @ map n.+ random.nat)
+ decrease (:: @ map n.- random.nat)]
+ (_.test "Composition."
+ ((comparison n.=)
+ (_$ _@apply
+ (injection function.compose)
+ (injection increase)
+ (injection decrease)
+ (injection sample))
+ ($_ _@apply
+ (injection increase)
+ (injection decrease)
+ (injection sample))))))
+
+(def: #export (spec injection comparison apply)
+ (All [f] (-> (Injection f) (Comparison f) (Apply f) Test))
+ (_.with-cover [/.Apply]
+ ($_ _.and
+ (..identity injection comparison apply)
+ (..homomorphism injection comparison apply)
+ (..interchange injection comparison apply)
+ (..composition injection comparison apply)
+ )))
diff --git a/stdlib/source/spec/lux/abstract/codec.lux b/stdlib/source/spec/lux/abstract/codec.lux
new file mode 100644
index 000000000..ece213c31
--- /dev/null
+++ b/stdlib/source/spec/lux/abstract/codec.lux
@@ -0,0 +1,26 @@
+(.module:
+ [lux #*
+ ["_" test (#+ Test)]
+ [abstract
+ [monad (#+ do)]]
+ [control
+ ["." try]]
+ [math
+ ["." random (#+ Random)]]]
+ {1
+ ["." /
+ [//
+ [equivalence (#+ Equivalence)]]]})
+
+(def: #export (spec (^open "/@.") (^open "/@.") generator)
+ (All [m a] (-> (Equivalence a) (/.Codec m a) (Random a) Test))
+ (do random.monad
+ [expected generator]
+ (_.with-cover [/.Codec]
+ (_.test "Isomorphism."
+ (case (|> expected /@encode /@decode)
+ (#try.Success actual)
+ (/@= expected actual)
+
+ (#try.Failure _)
+ false)))))
diff --git a/stdlib/source/spec/lux/abstract/enum.lux b/stdlib/source/spec/lux/abstract/enum.lux
new file mode 100644
index 000000000..198d3da50
--- /dev/null
+++ b/stdlib/source/spec/lux/abstract/enum.lux
@@ -0,0 +1,26 @@
+(.module:
+ [lux #*
+ ["_" test (#+ Test)]
+ [abstract
+ [monad (#+ do)]]
+ [math
+ ["." random (#+ Random)]]]
+ {1
+ ["." /]})
+
+(def: #export (spec (^open "/@.") gen-sample)
+ (All [a] (-> (/.Enum a) (Random a) Test))
+ (do random.monad
+ [sample gen-sample]
+ (<| (_.with-cover [/.Enum])
+ ($_ _.and
+ (_.test "Successor and predecessor are inverse functions."
+ (and (/@= (|> sample /@succ /@pred)
+ sample)
+ (/@= (|> sample /@pred /@succ)
+ sample)
+ (not (/@= (/@succ sample)
+ sample))
+ (not (/@= (/@pred sample)
+ sample))))
+ ))))
diff --git a/stdlib/source/spec/lux/abstract/equivalence.lux b/stdlib/source/spec/lux/abstract/equivalence.lux
new file mode 100644
index 000000000..b511ba176
--- /dev/null
+++ b/stdlib/source/spec/lux/abstract/equivalence.lux
@@ -0,0 +1,23 @@
+(.module:
+ [lux #*
+ ["_" test (#+ Test)]
+ [abstract
+ [monad (#+ do)]]
+ [math
+ ["." random (#+ Random)]]]
+ {1
+ ["." / (#+ Equivalence)]})
+
+(def: #export (spec (^open "_@.") generator)
+ (All [a] (-> (Equivalence a) (Random a) Test))
+ (do random.monad
+ [left generator
+ right generator]
+ (<| (_.with-cover [/.Equivalence])
+ ($_ _.and
+ (_.test "Reflexivity."
+ (_@= left left))
+ (_.test "Symmetry."
+ (if (_@= left right)
+ (_@= right left)
+ (not (_@= right left))))))))
diff --git a/stdlib/source/spec/lux/abstract/fold.lux b/stdlib/source/spec/lux/abstract/fold.lux
new file mode 100644
index 000000000..71377f991
--- /dev/null
+++ b/stdlib/source/spec/lux/abstract/fold.lux
@@ -0,0 +1,22 @@
+(.module:
+ [lux #*
+ ["_" test (#+ Test)]
+ [abstract
+ [monad (#+ do)]]
+ [data
+ [number
+ ["n" nat]]]
+ [math
+ ["." random]]]
+ [//
+ [functor (#+ Injection Comparison)]]
+ {1 ["." /]})
+
+(def: #export (spec injection comparison (^open "/@."))
+ (All [f] (-> (Injection f) (Comparison f) (/.Fold f) Test))
+ (do random.monad
+ [subject random.nat
+ parameter random.nat]
+ (_.cover [/.Fold]
+ (n.= (/@fold n.+ parameter (injection subject))
+ (n.+ parameter subject)))))
diff --git a/stdlib/source/spec/lux/abstract/functor.lux b/stdlib/source/spec/lux/abstract/functor.lux
new file mode 100644
index 000000000..2cb086b7a
--- /dev/null
+++ b/stdlib/source/spec/lux/abstract/functor.lux
@@ -0,0 +1,62 @@
+(.module:
+ [lux #*
+ ["_" test (#+ Test)]
+ [abstract
+ [equivalence (#+ Equivalence)]
+ [monad (#+ do)]]
+ [control
+ ["." function]]
+ [data
+ [number
+ ["n" nat]]]
+ [math
+ ["." random]]]
+ {1
+ ["." / (#+ Functor)]})
+
+(type: #export (Injection f)
+ (All [a] (-> a (f a))))
+
+(type: #export (Comparison f)
+ (All [a]
+ (-> (Equivalence a)
+ (Equivalence (f a)))))
+
+(def: (identity injection comparison (^open "/@."))
+ (All [f] (-> (Injection f) (Comparison f) (Functor f) Test))
+ (do {@ random.monad}
+ [sample (:: @ map injection random.nat)]
+ (_.test "Identity."
+ ((comparison n.=)
+ (/@map function.identity sample)
+ sample))))
+
+(def: (homomorphism injection comparison (^open "/@."))
+ (All [f] (-> (Injection f) (Comparison f) (Functor f) Test))
+ (do {@ random.monad}
+ [sample random.nat
+ increase (:: @ map n.+ random.nat)]
+ (_.test "Homomorphism."
+ ((comparison n.=)
+ (/@map increase (injection sample))
+ (injection (increase sample))))))
+
+(def: (composition injection comparison (^open "/@."))
+ (All [f] (-> (Injection f) (Comparison f) (Functor f) Test))
+ (do {@ random.monad}
+ [sample (:: @ map injection random.nat)
+ increase (:: @ map n.+ random.nat)
+ decrease (:: @ map n.- random.nat)]
+ (_.test "Composition."
+ ((comparison n.=)
+ (|> sample (/@map increase) (/@map decrease))
+ (|> sample (/@map (|>> increase decrease)))))))
+
+(def: #export (spec injection comparison functor)
+ (All [f] (-> (Injection f) (Comparison f) (Functor f) Test))
+ (<| (_.with-cover [/.Functor])
+ ($_ _.and
+ (..identity injection comparison functor)
+ (..homomorphism injection comparison functor)
+ (..composition injection comparison functor)
+ )))
diff --git a/stdlib/source/spec/lux/abstract/interval.lux b/stdlib/source/spec/lux/abstract/interval.lux
new file mode 100644
index 000000000..1541f1cee
--- /dev/null
+++ b/stdlib/source/spec/lux/abstract/interval.lux
@@ -0,0 +1,22 @@
+(.module:
+ [lux #*
+ ["_" test (#+ Test)]
+ [abstract
+ [monad (#+ do)]
+ ["." order]]
+ [math
+ ["." random (#+ Random)]]]
+ {1
+ ["." /]})
+
+(def: #export (spec (^open "/@.") gen-sample)
+ (All [a] (-> (/.Interval a) (Random a) Test))
+ (<| (_.with-cover [/.Interval])
+ (do random.monad
+ [sample gen-sample]
+ ($_ _.and
+ (_.test "No value is bigger than the top."
+ (/@< /@top sample))
+ (_.test "No value is smaller than the bottom."
+ (order.> /@&order /@bottom sample))
+ ))))
diff --git a/stdlib/source/spec/lux/abstract/monad.lux b/stdlib/source/spec/lux/abstract/monad.lux
new file mode 100644
index 000000000..d2eac535f
--- /dev/null
+++ b/stdlib/source/spec/lux/abstract/monad.lux
@@ -0,0 +1,57 @@
+(.module:
+ [lux #*
+ [data
+ [number
+ ["n" nat]]]
+ [math
+ ["." random]]
+ ["_" test (#+ Test)]]
+ {1
+ ["." / (#+ Monad do)]}
+ [//
+ [functor (#+ Injection Comparison)]])
+
+(def: (left-identity injection comparison (^open "_@."))
+ (All [f] (-> (Injection f) (Comparison f) (Monad f) Test))
+ (do {@ random.monad}
+ [sample random.nat
+ morphism (:: @ map (function (_ diff)
+ (|>> (n.+ diff) _@wrap))
+ random.nat)]
+ (_.test "Left identity."
+ ((comparison n.=)
+ (|> (injection sample) (_@map morphism) _@join)
+ (morphism sample)))))
+
+(def: (right-identity injection comparison (^open "_@."))
+ (All [f] (-> (Injection f) (Comparison f) (Monad f) Test))
+ (do random.monad
+ [sample random.nat]
+ (_.test "Right identity."
+ ((comparison n.=)
+ (|> (injection sample) (_@map _@wrap) _@join)
+ (injection sample)))))
+
+(def: (associativity injection comparison (^open "_@."))
+ (All [f] (-> (Injection f) (Comparison f) (Monad f) Test))
+ (do {@ random.monad}
+ [sample random.nat
+ increase (:: @ map (function (_ diff)
+ (|>> (n.+ diff) _@wrap))
+ random.nat)
+ decrease (:: @ map (function (_ diff)
+ (|>> (n.- diff) _@wrap))
+ random.nat)]
+ (_.test "Associativity."
+ ((comparison n.=)
+ (|> (injection sample) (_@map increase) _@join (_@map decrease) _@join)
+ (|> (injection sample) (_@map (|>> increase (_@map decrease) _@join)) _@join)))))
+
+(def: #export (spec injection comparison monad)
+ (All [f] (-> (Injection f) (Comparison f) (Monad f) Test))
+ (<| (_.with-cover [/.Monad])
+ ($_ _.and
+ (..left-identity injection comparison monad)
+ (..right-identity injection comparison monad)
+ (..associativity injection comparison monad)
+ )))
diff --git a/stdlib/source/spec/lux/abstract/monoid.lux b/stdlib/source/spec/lux/abstract/monoid.lux
new file mode 100644
index 000000000..eca057360
--- /dev/null
+++ b/stdlib/source/spec/lux/abstract/monoid.lux
@@ -0,0 +1,31 @@
+(.module:
+ [lux #*
+ ["_" test (#+ Test)]
+ [abstract
+ [monad (#+ do)]]
+ [math
+ ["." random (#+ Random)]]]
+ {1
+ ["." /
+ [//
+ [equivalence (#+ Equivalence)]]]})
+
+(def: #export (spec (^open "/@.") (^open "/@.") gen-sample)
+ (All [a] (-> (Equivalence a) (/.Monoid a) (Random a) Test))
+ (do random.monad
+ [sample gen-sample
+ left gen-sample
+ mid gen-sample
+ right gen-sample]
+ (<| (_.with-cover [/.Monoid])
+ ($_ _.and
+ (_.test "Left identity."
+ (/@= sample
+ (/@compose /@identity sample)))
+ (_.test "Right identity."
+ (/@= sample
+ (/@compose sample /@identity)))
+ (_.test "Associativity."
+ (/@= (/@compose left (/@compose mid right))
+ (/@compose (/@compose left mid) right)))
+ ))))
diff --git a/stdlib/source/spec/lux/abstract/order.lux b/stdlib/source/spec/lux/abstract/order.lux
new file mode 100644
index 000000000..4cdb5689a
--- /dev/null
+++ b/stdlib/source/spec/lux/abstract/order.lux
@@ -0,0 +1,27 @@
+(.module:
+ [lux #*
+ ["_" test (#+ Test)]
+ [abstract
+ [monad (#+ do)]]
+ [math
+ ["." random (#+ Random)]]]
+ {1
+ ["." /]})
+
+(def: #export (spec (^open "/@.") generator)
+ (All [a] (-> (/.Order a) (Random a) Test))
+ (<| (_.with-cover [/.Order])
+ (do random.monad
+ [parameter generator
+ subject generator])
+ ($_ _.and
+ (_.test "Values are either ordered, or they are equal. All options are mutually exclusive."
+ (cond (/@< parameter subject)
+ (not (or (/@< subject parameter)
+ (/@= parameter subject)))
+
+ (/@< subject parameter)
+ (not (/@= parameter subject))
+
+ ## else
+ (/@= parameter subject))))))
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 18:57:46 +0000