aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/specification
diff options
context:
space:
mode:
Diffstat (limited to 'stdlib/source/specification')
-rw-r--r--stdlib/source/specification/lux/abstract/apply.lux101
-rw-r--r--stdlib/source/specification/lux/abstract/comonad.lux77
2 files changed, 79 insertions, 99 deletions
diff --git a/stdlib/source/specification/lux/abstract/apply.lux b/stdlib/source/specification/lux/abstract/apply.lux
index 607024f11..eaf4d741c 100644
--- a/stdlib/source/specification/lux/abstract/apply.lux
+++ b/stdlib/source/specification/lux/abstract/apply.lux
@@ -16,64 +16,53 @@
[\\library
["[0]" / (.only Apply)]]
[//
- [functor (.only Injection Comparison)]])
+ ["[0]S" functor (.only Injection Comparison)]])
-(def (identity injection comparison (open "/#[0]"))
+(def .public (spec injection comparison it)
(All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test))
- (do [! random.monad]
- [sample (at ! each injection random.nat)]
- (_.test "Identity."
- ((comparison n.=)
- (/#on sample (injection function.identity))
- sample))))
+ (<| (_.for [/.Apply])
+ (type.let [:$/1: (-> Nat Nat)])
+ (do [! random.monad]
+ [sample random.nat
+ increase (is (Random :$/1:)
+ (at ! each n.+ random.nat))
+ decrease (is (Random :$/1:)
+ (at ! each n.- random.nat))])
+ (all _.and
+ (_.for [/.functor]
+ (functorS.spec injection comparison (the /.functor it)))
-(def (homomorphism injection comparison (open "/#[0]"))
- (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test))
- (do [! random.monad]
- [sample random.nat
- increase (at ! each n.+ random.nat)]
- (_.test "Homomorphism."
- ((comparison n.=)
- (/#on (injection sample) (injection increase))
- (injection (increase sample))))))
+ (_.coverage [/.on]
+ (let [(open "/#[0]") it
-(def (interchange injection comparison (open "/#[0]"))
- (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test))
- (do [! random.monad]
- [sample random.nat
- increase (at ! each n.+ random.nat)]
- (_.test "Interchange."
- ((comparison n.=)
- (/#on (injection sample) (injection increase))
- (/#on (injection increase) (injection (is (-> (-> Nat Nat) Nat)
- (function (_ f) (f sample)))))))))
+ identity!
+ ((comparison n.=)
+ (/#on (injection sample)
+ (injection function.identity))
+ (injection sample))
-(def (composition injection comparison (open "/#[0]"))
- (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test))
- (type.let [:$/1: (-> Nat Nat)]
- (do [! random.monad]
- [sample random.nat
- increase (is (Random :$/1:)
- (at ! each n.+ random.nat))
- decrease (is (Random :$/1:)
- (at ! each n.- random.nat))]
- (_.test "Composition."
- ((comparison n.=)
- (|> (injection (is (-> :$/1: :$/1: :$/1:)
- function.composite))
- (/#on (injection increase))
- (/#on (injection decrease))
- (/#on (injection sample)))
- (/#on (/#on (injection sample)
- (injection increase))
- (injection decrease)))))))
-
-(def .public (spec injection comparison apply)
- (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test))
- (_.for [/.Apply]
- (all _.and
- (..identity injection comparison apply)
- (..homomorphism injection comparison apply)
- (..interchange injection comparison apply)
- (..composition injection comparison apply)
- )))
+ homomorphism!
+ ((comparison n.=)
+ (/#on (injection sample) (injection increase))
+ (injection (increase sample)))
+
+ interchange!
+ ((comparison n.=) (/#on (injection sample) (injection increase))
+ (/#on (injection increase) (injection (is (-> (-> Nat Nat) Nat)
+ (function (_ f) (f sample))))))
+
+ composition!
+ ((comparison n.=)
+ (|> (injection (is (-> :$/1: :$/1: :$/1:)
+ function.composite))
+ (/#on (injection increase))
+ (/#on (injection decrease))
+ (/#on (injection sample)))
+ (/#on (/#on (injection sample)
+ (injection increase))
+ (injection decrease)))]
+ (and identity!
+ homomorphism!
+ interchange!
+ composition!)))
+ )))
diff --git a/stdlib/source/specification/lux/abstract/comonad.lux b/stdlib/source/specification/lux/abstract/comonad.lux
index 2583715f2..9763f136b 100644
--- a/stdlib/source/specification/lux/abstract/comonad.lux
+++ b/stdlib/source/specification/lux/abstract/comonad.lux
@@ -12,51 +12,42 @@
[\\library
["[0]" / (.only CoMonad)]]
[//
- [functor (.only Injection Comparison)]])
+ ["[0]S" functor (.only Injection Comparison)]])
-(def (left_identity injection (open "_//[0]"))
- (All (_ f) (-> (Injection f) (CoMonad f) Test))
- (do [! random.monad]
- [sample random.nat
- morphism (at ! each (function (_ diff)
- (|>> _//out (n.+ diff)))
- random.nat)
- .let [start (injection sample)]]
- (_.test "Left identity."
- (n.= (morphism start)
- (|> start _//disjoint (_//each morphism) _//out)))))
-
-(def (right_identity injection comparison (open "_//[0]"))
- (All (_ f) (-> (Injection f) (Comparison f) (CoMonad f) Test))
- (do random.monad
- [sample random.nat
- .let [start (injection sample)
- == (comparison n.=)]]
- (_.test "Right identity."
- (== start
- (|> start _//disjoint (_//each _//out))))))
-
-(def (associativity injection comparison (open "_//[0]"))
- (All (_ f) (-> (Injection f) (Comparison f) (CoMonad f) Test))
- (do [! random.monad]
- [sample random.nat
- increase (at ! each (function (_ diff)
- (|>> _//out (n.+ diff)))
- random.nat)
- decrease (at ! each (function (_ diff)
- (|>> _//out(n.- diff)))
- random.nat)
- .let [start (injection sample)
- == (comparison n.=)]]
- (_.test "Associativity."
- (== (|> start _//disjoint (_//each (|>> _//disjoint (_//each increase) decrease)))
- (|> start _//disjoint (_//each increase) _//disjoint (_//each decrease))))))
-
-(def .public (spec injection comparison subject)
+(def .public (spec injection comparison it)
(All (_ f) (-> (Injection f) (Comparison f) (CoMonad f) Test))
(<| (_.for [/.CoMonad])
+ (do [! random.monad]
+ [.let [(open "/#[0]") it]
+ sample random.nat
+ increase (at ! each (function (_ diff)
+ (|>> /#out (n.+ diff)))
+ random.nat)
+ decrease (at ! each (function (_ diff)
+ (|>> /#out (n.- diff)))
+ random.nat)
+ morphism (at ! each (function (_ diff)
+ (|>> /#out (n.+ diff)))
+ random.nat)
+ .let [start (injection sample)
+ == (comparison n.=)]])
(all _.and
- (..left_identity injection subject)
- (..right_identity injection comparison subject)
- (..associativity injection comparison subject)
+ (_.for [/.functor]
+ (functorS.spec injection comparison (the /.functor it)))
+
+ (_.coverage [/.disjoint /.out]
+ (let [left_identity!
+ (n.= (morphism start)
+ (|> start /#disjoint (/#each morphism) /#out))
+
+ right_identity!
+ (== start
+ (|> start /#disjoint (/#each /#out)))
+
+ associativity!
+ (== (|> start /#disjoint (/#each (|>> /#disjoint (/#each increase) decrease)))
+ (|> start /#disjoint (/#each increase) /#disjoint (/#each decrease)))]
+ (and left_identity!
+ right_identity!
+ associativity!)))
)))
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-03 01:55:23 +0000