diff options
Diffstat (limited to 'stdlib/source/specification')
-rw-r--r-- | stdlib/source/specification/lux/abstract/functor.lux | 80 |
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!))))) |