aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/specification
diff options
context:
space:
mode:
authorEduardo Julian2022-11-23 20:35:07 -0400
committerEduardo Julian2022-11-23 20:35:07 -0400
commit44cff1dcbd6cd23ef455923b707104302dde1aad (patch)
tree8351360a41980e01cbb8124a03264d17775553fd /stdlib/source/specification
parent224797231a8144f6ead1baab3b4b01a74cab629c (diff)
New arithmetic abstraction + common file extensions as constants.
Diffstat (limited to '')
-rw-r--r--stdlib/source/specification/lux/abstract/order.lux93
-rw-r--r--stdlib/source/specification/lux/math/arithmetic.lux46
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)))))
+ ))))