From 44cff1dcbd6cd23ef455923b707104302dde1aad Mon Sep 17 00:00:00 2001
From: Eduardo Julian
Date: Wed, 23 Nov 2022 20:35:07 -0400
Subject: New arithmetic abstraction + common file extensions as constants.

---
 stdlib/source/specification/lux/abstract/order.lux | 93 ++++++++++++----------
 .../source/specification/lux/math/arithmetic.lux   | 46 +++++++++++
 2 files changed, 98 insertions(+), 41 deletions(-)
 create mode 100644 stdlib/source/specification/lux/math/arithmetic.lux

(limited to 'stdlib/source/specification')

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)))))
+             ))))
-- 
cgit v1.2.3