aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/test/lux/tool/compiler/language/lux/synthesis/side.lux
diff options
context:
space:
mode:
authorEduardo Julian2022-03-01 02:29:52 -0400
committerEduardo Julian2022-03-01 02:29:52 -0400
commit8023df0f5dae4638021fef7b8194a3d0a16b32e4 (patch)
tree8d64ad88decb0832d85b46a9ef7e734e6b816c35 /stdlib/source/test/lux/tool/compiler/language/lux/synthesis/side.lux
parent62436b809630ecd3e40bd6e2b45a8870a2866934 (diff)
Still more fixes for JVM interop.
Diffstat (limited to '')
-rw-r--r--stdlib/source/test/lux/tool/compiler/language/lux/synthesis/side.lux43
1 files changed, 43 insertions, 0 deletions
diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/synthesis/side.lux b/stdlib/source/test/lux/tool/compiler/language/lux/synthesis/side.lux
new file mode 100644
index 000000000..3dccec159
--- /dev/null
+++ b/stdlib/source/test/lux/tool/compiler/language/lux/synthesis/side.lux
@@ -0,0 +1,43 @@
+(.using
+ [library
+ [lux "*"
+ ["_" test {"+" Test}]
+ [abstract
+ [monad {"+" do}]
+ [\\specification
+ ["$[0]" equivalence]
+ ["$[0]" hash]]]
+ [data
+ ["[0]" bit ("[1]#[0]" equivalence)]
+ ["[0]" text ("[1]#[0]" equivalence)]]
+ [math
+ ["[0]" random {"+" Random}]
+ [number
+ ["n" nat]]]]]
+ [\\library
+ ["[0]" /]])
+
+(def: .public random
+ (Random /.Side)
+ ($_ random.and
+ random.nat
+ random.bit
+ ))
+
+(def: .public test
+ Test
+ (<| (_.covering /._)
+ (_.for [/.Side])
+ (do [! random.monad]
+ [left ..random
+ right ..random]
+ ($_ _.and
+ (_.for [/.equivalence]
+ ($equivalence.spec /.equivalence ..random))
+ (_.for [/.hash]
+ ($hash.spec /.hash ..random))
+
+ (_.cover [/.format]
+ (bit#= (# /.equivalence = left right)
+ (text#= (/.format left) (/.format right))))
+ ))))