aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/specification
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--stdlib/source/specification/lux/abstract/apply.lux68
-rw-r--r--stdlib/source/specification/lux/abstract/comonad.lux10
-rw-r--r--stdlib/source/specification/lux/abstract/functor.lux59
-rw-r--r--stdlib/source/specification/lux/abstract/mix.lux6
-rw-r--r--stdlib/source/specification/lux/abstract/monad.lux7
5 files changed, 12 insertions, 138 deletions
diff --git a/stdlib/source/specification/lux/abstract/apply.lux b/stdlib/source/specification/lux/abstract/apply.lux
deleted file mode 100644
index 1b9c0c941..000000000
--- a/stdlib/source/specification/lux/abstract/apply.lux
+++ /dev/null
@@ -1,68 +0,0 @@
-(.require
- [library
- [lux (.except)
- [abstract
- [monad (.only do)]]
- [control
- ["[0]" function]]
- [math
- ["[0]" random (.only Random)]
- [number
- ["n" nat]]]
- [meta
- ["[0]" type]]
- [test
- ["_" property (.only Test)]]]]
- [\\library
- ["[0]" / (.only Apply)]]
- [//
- ["[0]S" functor (.only Injection Comparison)]])
-
-(def .public (spec injection comparison it)
- (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test))
- (<| (_.for [/.Apply])
- (type.let [:$/1: (-> Nat Nat)])
- (do [! random.monad]
- [sample random.nat
- increase (is (Random :$/1:)
- (of ! each n.+ random.nat))
- decrease (is (Random :$/1:)
- (of ! each n.- random.nat))])
- (all _.and
- (_.for [/.functor]
- (functorS.spec injection comparison (the /.functor it)))
-
- (_.coverage [/.on]
- (let [(open "/#[0]") it
-
- identity!
- ((comparison n.=)
- (/#on (injection sample)
- (injection function.identity))
- (injection sample))
-
- 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 536970182..2b89691ec 100644
--- a/stdlib/source/specification/lux/abstract/comonad.lux
+++ b/stdlib/source/specification/lux/abstract/comonad.lux
@@ -2,7 +2,9 @@
[library
[lux (.except)
[abstract
- [monad (.only do)]]
+ [monad (.only do)]
+ ["[0]" functor
+ ["[1]T" \\test (.only Injection Comparison)]]]
[math
["[0]" random]
[number
@@ -10,9 +12,7 @@
[test
["_" property (.only Test)]]]]
[\\library
- ["[0]" / (.only CoMonad)]]
- [//
- ["[0]S" functor (.only Injection Comparison)]])
+ ["[0]" / (.only CoMonad)]])
(def .public (spec injection comparison it)
(All (_ f) (-> (Injection f) (Comparison f) (CoMonad f) Test))
@@ -33,7 +33,7 @@
== (comparison n.=)]])
(all _.and
(_.for [/.functor]
- (functorS.spec injection comparison (the /.functor it)))
+ (functorT.spec injection comparison (the /.functor it)))
(_.coverage [/.disjoint /.out]
(let [left_identity!
diff --git a/stdlib/source/specification/lux/abstract/functor.lux b/stdlib/source/specification/lux/abstract/functor.lux
deleted file mode 100644
index c64be9401..000000000
--- a/stdlib/source/specification/lux/abstract/functor.lux
+++ /dev/null
@@ -1,59 +0,0 @@
-(.require
- [library
- [lux (.except)
- [abstract
- [equivalence (.only Equivalence)]
- [monad (.only do)]]
- [control
- ["[0]" function]]
- [math
- ["[0]" random]
- [number
- ["n" nat]]]
- [test
- ["_" property (.only Test)]]]]
- [\\library
- ["[0]" / (.only Functor)]])
-
-(type .public (Injection !)
- (All (_ of)
- (-> of
- (! of))))
-
-(type .public (Comparison !)
- (All (_ of)
- (-> (Equivalence of)
- (Equivalence (! of)))))
-
-(def .public (spec injection comparison functor)
- (All (_ !)
- (-> (Injection !) (Comparison !) (Functor !)
- Test))
- (<| (do [! random.monad]
- [sample random.nat
- increase (of ! each n.+ random.nat)
- decrease (of ! each n.- random.nat)])
- (_.for [/.Functor])
- (_.coverage [/.each]
- (let [(open "/#[0]") functor
-
- identity!
- ((comparison n.=)
- (/#each function.identity (injection sample))
- (injection sample))
-
- homomorphism!
- ((comparison n.=)
- (/#each increase (injection sample))
- (injection (increase sample)))
-
- composition!
- ((comparison n.=)
- (|> (injection sample)
- (/#each increase)
- (/#each decrease))
- (|> (injection sample)
- (/#each (|>> increase decrease))))]
- (and identity!
- homomorphism!
- composition!)))))
diff --git a/stdlib/source/specification/lux/abstract/mix.lux b/stdlib/source/specification/lux/abstract/mix.lux
index 51c2d5d71..614b7439f 100644
--- a/stdlib/source/specification/lux/abstract/mix.lux
+++ b/stdlib/source/specification/lux/abstract/mix.lux
@@ -2,15 +2,15 @@
[library
[lux (.except)
[abstract
- [monad (.only do)]]
+ [monad (.only do)]
+ [functor
+ [\\test (.only Injection Comparison)]]]
[math
["[0]" random]
[number
["n" nat]]]
[test
["_" property (.only Test)]]]]
- [//
- [functor (.only Injection Comparison)]]
[\\library
["[0]" /]])
diff --git a/stdlib/source/specification/lux/abstract/monad.lux b/stdlib/source/specification/lux/abstract/monad.lux
index 82a7ff55b..48db743b8 100644
--- a/stdlib/source/specification/lux/abstract/monad.lux
+++ b/stdlib/source/specification/lux/abstract/monad.lux
@@ -1,6 +1,9 @@
(.require
[library
[lux (.except)
+ [abstract
+ [functor
+ [\\test (.only Injection Comparison)]]]
[math
["[0]" random]
[number
@@ -8,9 +11,7 @@
[test
["_" property (.only Test)]]]]
[\\library
- ["[0]" / (.only do)]]
- [//
- [functor (.only Injection Comparison)]])
+ ["[0]" / (.only do)]])
(def (left_identity injection comparison (open "_//[0]"))
(All (_ f) (-> (Injection f) (Comparison f) (/.Monad f) Test))