diff options
Diffstat (limited to 'stdlib/source/specification')
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)) |