diff options
Diffstat (limited to '')
| -rw-r--r-- | stdlib/source/specification/lux/abstract/order.lux | 93 | ||||
| -rw-r--r-- | stdlib/source/specification/lux/math/arithmetic.lux | 46 |
2 files changed, 98 insertions, 41 deletions
diff --git a/stdlib/source/specification/lux/abstract/order.lux b/stdlib/source/specification/lux/abstract/order.lux index ae7dc3355..1bf62b3cc 100644 --- a/stdlib/source/specification/lux/abstract/order.lux +++ b/stdlib/source/specification/lux/abstract/order.lux @@ -3,57 +3,68 @@ [lux (.except) [abstract [monad (.only do)]] + [data + ["[0]" bit (.use "[1]#[0]" equivalence)]] [math ["[0]" random (.only Random)]] [test ["_" property (.only Test)]]]] [\\library - ["[0]" /]]) + ["[0]" /]] + [// + ["[0]S" equivalence]]) -(def .public (spec (open "@//[0]") generator) - (All (_ a) (-> (/.Order a) (Random a) Test)) +(def .public (spec (open "/#[0]") random) + (All (_ of) + (-> (/.Order of) (Random of) + Test)) (<| (_.for [/.Order]) (all _.and + (_.for [/.equivalence] + (equivalenceS.spec /#equivalence random)) + (do random.monad - [parameter generator - subject generator] - (_.test "Values are either ordered, or they are equal. All options(_ are mutually exclusive." - (cond (@//< parameter subject) - (not (or (@//< subject parameter) - (@//= parameter subject))) + [parameter random + subject random + .let [equal_or_ordered! + (let [equal! + (/#= parameter subject) - (@//< subject parameter) - (not (@//= parameter subject)) + ordered! + (or (and (/#< parameter subject) + (not (/#< subject parameter))) + (and (/#< subject parameter) + (not (/#< parameter subject))))] + (bit#= equal! (not ordered!)))] - ... else - (@//= parameter subject)))) - (do random.monad - [parameter generator - subject (random.only (|>> (@//= parameter) not) - generator) + subject (random.only (|>> (/#= parameter) not) + random) extra (random.only (function (_ value) - (not (or (@//= parameter value) - (@//= subject value)))) - generator)] - (_.test "Transitive property." - (if (@//< parameter subject) - (let [greater? (and (@//< subject extra) - (@//< parameter extra)) - lesser? (and (@//< extra parameter) - (@//< extra subject)) - in_between? (and (@//< parameter extra) - (@//< extra subject))] - (or greater? - lesser? - in_between?)) - ... (@//< subject parameter) - (let [greater? (and (@//< extra subject) - (@//< extra parameter)) - lesser? (and (@//< parameter extra) - (@//< subject extra)) - in_between? (and (@//< subject extra) - (@//< extra parameter))] - (or greater? - lesser? - in_between?))))) + (not (or (/#= parameter value) + (/#= subject value)))) + random) + .let [transitive_property! + (if (/#< parameter subject) + (let [greater? (and (/#< subject extra) + (/#< parameter extra)) + lesser? (and (/#< extra parameter) + (/#< extra subject)) + in_between? (and (/#< parameter extra) + (/#< extra subject))] + (or greater? + lesser? + in_between?)) + ... (/#< subject parameter) + (let [greater? (and (/#< extra subject) + (/#< extra parameter)) + lesser? (and (/#< parameter extra) + (/#< subject extra)) + in_between? (and (/#< subject extra) + (/#< extra parameter))] + (or greater? + lesser? + in_between?)))]] + (_.coverage [/.<] + (and equal_or_ordered! + transitive_property!))) ))) diff --git a/stdlib/source/specification/lux/math/arithmetic.lux b/stdlib/source/specification/lux/math/arithmetic.lux new file mode 100644 index 000000000..7ae9f3f06 --- /dev/null +++ b/stdlib/source/specification/lux/math/arithmetic.lux @@ -0,0 +1,46 @@ +(.require + [library + [lux (.except) + [abstract + [equivalence (.only Equivalence)] + [monad (.only do)]] + [math + ["[0]" random (.only Random)]] + [test + ["_" property (.only Test)]]]] + [\\library + ["[0]" /]]) + +(def .public (spec (open "[0]") (open "[0]") random) + (All (_ of) + (-> (Equivalence of) (/.Arithmetic of) (Random of) + Test)) + (do random.monad + [any random + .let [zero (- any any) + non_zero (random.only (|>> (= zero) not) + random)] + left non_zero + right non_zero + .let [one (/ right right)]] + (<| (_.covering /._) + (_.for [/.Arithmetic]) + (all _.and + (_.coverage [/.+ /.-] + (and (|> left (+ right) (- right) (= left)) + (|> left (- right) (+ right) (= left)) + (|> left (+ zero) (= left)) + (|> left (- zero) (= left)) + (|> left (- left) (= zero)))) + (_.coverage [/.* /./] + (and (|> left (* right) (/ right) (= left)) + (|> left (* one) (= left)) + (|> left (/ one) (= left)) + (|> left (/ left) (= one)) + (|> left (* zero) (= zero)))) + (_.coverage [/.%] + (let [rem (% left right) + div (|> right (- rem) (/ left))] + (= right + (|> div (* left) (+ rem))))) + )))) |