aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/specification
diff options
context:
space:
mode:
authorEduardo Julian2022-11-25 01:26:00 -0400
committerEduardo Julian2022-11-25 01:26:00 -0400
commit09a29c952edb851e13edd454bd118c1c1ae83ade (patch)
treec27287569bdb0ffd190549a4bb1eb1899b9b20f4 /stdlib/source/specification
parent44cff1dcbd6cd23ef455923b707104302dde1aad (diff)
Added support for saturation arithmetic.
Diffstat (limited to 'stdlib/source/specification')
-rw-r--r--stdlib/source/specification/lux/abstract/functor.lux80
1 files changed, 38 insertions, 42 deletions
diff --git a/stdlib/source/specification/lux/abstract/functor.lux b/stdlib/source/specification/lux/abstract/functor.lux
index 232e9316a..d0f8327d5 100644
--- a/stdlib/source/specification/lux/abstract/functor.lux
+++ b/stdlib/source/specification/lux/abstract/functor.lux
@@ -15,49 +15,45 @@
[\\library
["[0]" / (.only Functor)]])
-(type .public (Injection f)
- (All (_ a) (-> a (f a))))
+(type .public (Injection !)
+ (All (_ of)
+ (-> of
+ (! of))))
-(type .public (Comparison f)
- (All (_ a)
- (-> (Equivalence a)
- (Equivalence (f a)))))
+(type .public (Comparison !)
+ (All (_ of)
+ (-> (Equivalence of)
+ (Equivalence (! of)))))
-(def (identity injection comparison (open "@//[0]"))
- (All (_ f) (-> (Injection f) (Comparison f) (Functor f) Test))
- (do [! random.monad]
- [sample (at ! each injection random.nat)]
- (_.test "Identity."
- ((comparison n.=)
- (@//each function.identity sample)
- sample))))
-
-(def (homomorphism injection comparison (open "@//[0]"))
- (All (_ f) (-> (Injection f) (Comparison f) (Functor f) Test))
- (do [! random.monad]
- [sample random.nat
- increase (at ! each n.+ random.nat)]
- (_.test "Homomorphism."
- ((comparison n.=)
- (@//each increase (injection sample))
- (injection (increase sample))))))
+(def .public (spec injection comparison functor)
+ (All (_ !)
+ (-> (Injection !) (Comparison !) (Functor !)
+ Test))
+ (<| (do [! random.monad]
+ [sample random.nat
+ increase (at ! each n.+ random.nat)
+ decrease (at ! each n.- random.nat)])
+ (_.for [/.Functor])
+ (_.coverage [/.each]
+ (let [(open "/#[0]") functor
+
+ identity!
+ ((comparison n.=)
+ (/#each function.identity (injection sample))
+ (injection sample))
-(def (composition injection comparison (open "@//[0]"))
- (All (_ f) (-> (Injection f) (Comparison f) (Functor f) Test))
- (do [! random.monad]
- [sample (at ! each injection random.nat)
- increase (at ! each n.+ random.nat)
- decrease (at ! each n.- random.nat)]
- (_.test "Composition."
- ((comparison n.=)
- (|> sample (@//each increase) (@//each decrease))
- (|> sample (@//each (|>> increase decrease)))))))
+ homomorphism!
+ ((comparison n.=)
+ (/#each increase (injection sample))
+ (injection (increase sample)))
-(def .public (spec injection comparison functor)
- (All (_ f) (-> (Injection f) (Comparison f) (Functor f) Test))
- (<| (_.for [/.Functor])
- (all _.and
- (..identity injection comparison functor)
- (..homomorphism injection comparison functor)
- (..composition injection comparison functor)
- )))
+ composition!
+ ((comparison n.=)
+ (|> (injection sample)
+ (/#each increase)
+ (/#each decrease))
+ (|> (injection sample)
+ (/#each (|>> increase decrease))))]
+ (and identity!
+ homomorphism!
+ composition!)))))