diff options
| -rw-r--r-- | commands.md | 20 | ||||
| -rw-r--r-- | documentation/research/Testing.md | 4 | ||||
| -rw-r--r-- | documentation/research/database.md | 1 | ||||
| -rw-r--r-- | stdlib/source/lux/data/number/i64.lux | 67 | ||||
| -rw-r--r-- | stdlib/source/program/aedifex/project.lux | 27 | ||||
| -rw-r--r-- | stdlib/source/test/aedifex.lux | 2 | ||||
| -rw-r--r-- | stdlib/source/test/aedifex/parser.lux | 8 | ||||
| -rw-r--r-- | stdlib/source/test/aedifex/project.lux | 96 | ||||
| -rw-r--r-- | stdlib/source/test/lux/data/number/i64.lux | 18 | ||||
| -rw-r--r-- | stdlib/source/test/lux/data/sum.lux | 107 | ||||
| -rw-r--r-- | stdlib/source/test/lux/target/jvm.lux | 15 |
11 files changed, 283 insertions, 82 deletions
diff --git a/commands.md b/commands.md index 617772bf3..26e5d971a 100644 --- a/commands.md +++ b/commands.md @@ -39,16 +39,6 @@ cd ~/lux/jbe/ && ./jbe.sh --- -# Leiningen plugin - -## Install - -``` -cd ~/lux/lux-lein/ && lein install -``` - ---- - # Standard Library ## Test @@ -98,6 +88,16 @@ cd ~/lux/stdlib/ && lein clean && lein with-profile aedifex lux auto test --- +# Leiningen plugin + +## Install + +``` +cd ~/lux/lux-lein/ && lein install +``` + +--- + # Licentia: License maker ## Build diff --git a/documentation/research/Testing.md b/documentation/research/Testing.md index baaf83fa4..6d6e57f1a 100644 --- a/documentation/research/Testing.md +++ b/documentation/research/Testing.md @@ -1,3 +1,7 @@ +# Symbolic + +1. [Crux](https://crux.galois.com/) + # White box 1. [Ricardo Peña - White-Box Path Generation in Recursive Programs - Lambda Days 2020](https://www.youtube.com/watch?v=7RXJhPaQCkc) diff --git a/documentation/research/database.md b/documentation/research/database.md index c8b641bae..c51c603aa 100644 --- a/documentation/research/database.md +++ b/documentation/research/database.md @@ -15,6 +15,7 @@ # Query +1. [A Short Story About SQL’s Biggest Rival](https://www.holistics.io/blog/quel-vs-sql/) 1. https://calcite.apache.org/ 1. https://juxt.pro/blog/crux-sql 1. https://www.influxdata.com/blog/why-were-building-flux-a-new-data-scripting-and-query-language/ diff --git a/stdlib/source/lux/data/number/i64.lux b/stdlib/source/lux/data/number/i64.lux index 26bc0cdc9..79bf7632d 100644 --- a/stdlib/source/lux/data/number/i64.lux +++ b/stdlib/source/lux/data/number/i64.lux @@ -1,5 +1,5 @@ (.module: - [lux (#- and or not) + [lux (#- and or not false true) [abstract [equivalence (#+ Equivalence)] [hash (#+ Hash)] @@ -16,8 +16,8 @@ (def: #export width Nat - (n.* bits-per-byte - bytes-per-i64)) + (n.* ..bits-per-byte + ..bytes-per-i64)) (template [<parameter-type> <name> <op> <doc>] [(def: #export (<name> parameter subject) @@ -39,17 +39,32 @@ (All [s] (-> (I64 s) (I64 s))) (xor (:coerce I64 -1))) -(type: #export Mask I64) +(type: #export Mask + I64) -(def: #export (mask bits) +(def: #export false + Mask + (.i64 0)) + +(def: #export true + Mask + (..not ..false)) + +(def: #export (mask amount-of-bits) + (-> Nat Mask) + (case amount-of-bits + 0 ..false + bits (case (n.% ..width bits) + 0 ..true + bits (|> 1 .i64 (..left-shift (n.% ..width bits)) .dec)))) + +(def: #export (bit position) (-> Nat Mask) - (let [multiple-of-width? (.and (.not (n.= 0 bits)) - (n.= 0 (n.% ..width bits)))] - (if multiple-of-width? - (.i64 -1) - (|> 1 .i64 (..left-shift (n.% ..width bits)) .dec)))) + (|> 1 .i64 (..left-shift (n.% ..width position)))) -(def: #export sign Mask (|> 1 .i64 (..left-shift 63))) +(def: #export sign + Mask + (..bit 63)) (def: (add-shift shift value) (-> Nat Nat Nat) @@ -68,20 +83,16 @@ (add-shift 32) (..and 127)))) -(def: (flag idx) - (-> Nat I64) - (|> 1 (:coerce I64) (left-shift idx))) - (def: #export (clear idx input) {#.doc "Clear bit at given index."} (All [s] (-> Nat (I64 s) (I64 s))) - (|> idx flag ..not (..and input))) + (|> idx ..bit ..not (..and input))) (template [<name> <op> <doc>] [(def: #export (<name> idx input) {#.doc <doc>} (All [s] (-> Nat (I64 s) (I64 s))) - (|> idx flag (<op> input)))] + (|> idx ..bit (<op> input)))] [set ..or "Set bit at given index."] [flip ..xor "Flip bit at given index."] @@ -89,7 +100,7 @@ (def: #export (set? idx input) (-> Nat (I64 Any) Bit) - (|> input (:coerce I64) (..and (flag idx)) (n.= 0) .not)) + (|> input (:coerce I64) (..and (..bit idx)) (n.= 0) .not)) (template [<name> <main> <comp>] [(def: #export (<name> distance input) @@ -120,18 +131,16 @@ (def: hash .nat)) -(structure: #export disjunction - (All [a] (Monoid (I64 a))) - - (def: identity (.i64 0)) - (def: compose ..or) - ) +(template [<monoid> <identity> <compose>] + [(structure: #export <monoid> + (All [a] (Monoid (I64 a))) -(structure: #export conjunction - (All [a] (Monoid (I64 a))) + (def: identity <identity>) + (def: compose <compose>) + )] - (def: identity (.i64 (..not 0))) - (def: compose ..and) + [disjunction ..false ..or] + [conjunction ..true ..and] ) (type: #export (Sub size) @@ -145,7 +154,7 @@ (n.< ..width width)) (let [top (dec width) shift (n.- width ..width) - sign (: Mask (|> 1 .i64 (..left-shift top))) + sign (..bit top) number (..mask (dec width))] (#.Some {#narrow (function (narrow value) (..or (|> value (..and ..sign) (..logic-right-shift shift)) diff --git a/stdlib/source/program/aedifex/project.lux b/stdlib/source/program/aedifex/project.lux index 15abd9ee1..071f54b12 100644 --- a/stdlib/source/program/aedifex/project.lux +++ b/stdlib/source/program/aedifex/project.lux @@ -1,8 +1,9 @@ (.module: [lux (#- Name) [abstract - ["." monad (#+ do)] - ["." equivalence (#+ Equivalence)]] + [equivalence (#+ Equivalence)] + [monoid (#+ Monoid)] + ["." monad (#+ do)]] [control ["." try (#+ Try)] ["." exception (#+ exception:)]] @@ -19,13 +20,23 @@ (type: #export Project (Dictionary Name Profile)) -(def: #export empty - (dictionary.from-list text.hash (list [//.default (:: //.monoid identity)]))) +(def: #export (project name profile) + (-> Name Profile Project) + (dictionary.from-list text.hash (list [name profile]))) (def: #export equivalence (Equivalence Project) (dictionary.equivalence //.equivalence)) +(structure: #export monoid + (Monoid Project) + + (def: identity + (dictionary.new text.hash)) + + (def: compose + (dictionary.merge-with (:: //.monoid compose)))) + (exception: #export (unknown-profile {name Name}) (exception.report ["Name" (%.text name)])) @@ -50,12 +61,12 @@ (get@ #//.parents profile))] (wrap (list@fold (function (_ parent child) (:: //.monoid compose child parent)) - profile + (set@ #//.parents (list) profile) parents)))) #.None (exception.throw ..unknown-profile [name]))) -(def: #export (profile project name) - (-> Project Name (Try Profile)) - (profile' (set.new text.hash) project name)) +(def: #export (profile name project) + (-> Name Project (Try Profile)) + (..profile' (set.new text.hash) project name)) diff --git a/stdlib/source/test/aedifex.lux b/stdlib/source/test/aedifex.lux index de52e6a9e..48ecc9189 100644 --- a/stdlib/source/test/aedifex.lux +++ b/stdlib/source/test/aedifex.lux @@ -8,6 +8,7 @@ ["." / #_ ["#." artifact] ["#." profile] + ["#." project] ["#." cli] ["#." parser]]) @@ -16,6 +17,7 @@ ($_ _.and /artifact.test /profile.test + /project.test /cli.test /parser.test )) diff --git a/stdlib/source/test/aedifex/parser.lux b/stdlib/source/test/aedifex/parser.lux index 988883779..a171e694d 100644 --- a/stdlib/source/test/aedifex/parser.lux +++ b/stdlib/source/test/aedifex/parser.lux @@ -73,9 +73,7 @@ (case> (#try.Success actual) (|> expected ..with-default-sources - [//.default] - list - (dictionary.from-list text.hash) + (//project.project //.default) (:: //project.equivalence = actual)) (#try.Failure error) @@ -84,7 +82,7 @@ (def: (with-empty-profile project) (-> Project Project) (if (dictionary.empty? project) - //project.empty + (//project.project //.default (:: //.monoid identity)) project)) (def: multiple-profiles @@ -102,7 +100,7 @@ dictionary.entries (list@map (function (_ [name profile]) [name (..with-default-sources profile)])) - (dictionary.from-list text.hash) + (dictionary.from-list text.hash) (:: //project.equivalence = actual)) (#try.Failure error) diff --git a/stdlib/source/test/aedifex/project.lux b/stdlib/source/test/aedifex/project.lux new file mode 100644 index 000000000..f2c2917a2 --- /dev/null +++ b/stdlib/source/test/aedifex/project.lux @@ -0,0 +1,96 @@ +(.module: + [lux #* + ["_" test (#+ Test)] + [abstract + [monad (#+ do)] + {[0 #spec] + [/ + ["$." equivalence] + ["$." monoid]]}] + [control + ["." try ("#@." functor)] + ["." exception]] + [data + ["." product] + ["." text ("#@." equivalence)] + [number + ["n" nat]]] + [math + ["." random (#+ Random) ("#@." monad)]]] + [// + ["@." profile]] + {#program + ["." / + ["/#" // #_ + ["#" profile]]]}) + +(def: profile + (Random [//.Name //.Profile]) + (|> @profile.random + (random@map (set@ #//.parents (list))) + (random.and (random.ascii/alpha 1)))) + +(def: #export random + (Random /.Project) + (do random.monad + [[name profile] ..profile] + (wrap (/.project name profile)))) + +(def: #export test + Test + (<| (_.covering /._) + (_.with-cover [/.Project /.project] + ($_ _.and + (_.with-cover [/.equivalence] + ($equivalence.spec /.equivalence ..random)) + (_.with-cover [/.monoid] + ($monoid.spec /.equivalence /.monoid ..random)) + + (do random.monad + [[super-name super-profile] ..profile + [dummy-name dummy-profile] (random.filter (|>> product.left (text@= super-name) not) + ..profile) + [sub-name sub-profile] (random.filter (function (_ [name profile]) + (and (not (text@= super-name name)) + (not (text@= dummy-name name)))) + ..profile) + fake-name (random.filter (function (_ name) + (and (not (text@= super-name name)) + (not (text@= dummy-name name)) + (not (text@= sub-name name)))) + (random.ascii/alpha 1)) + #let [project ($_ (:: /.monoid compose) + (/.project super-name super-profile) + (/.project dummy-name dummy-profile) + (/.project sub-name (set@ #//.parents (list super-name) sub-profile))) + circular ($_ (:: /.monoid compose) + (/.project super-name (set@ #//.parents (list sub-name) super-profile)) + (/.project dummy-name dummy-profile) + (/.project sub-name (set@ #//.parents (list super-name) sub-profile)))]] + ($_ _.and + (_.cover [/.profile] + (and (|> (/.profile super-name project) + (try@map (:: //.equivalence = super-profile)) + (try.default false)) + (|> (/.profile dummy-name project) + (try@map (:: //.equivalence = dummy-profile)) + (try.default false)) + (|> (/.profile sub-name project) + (try@map (:: //.equivalence = (:: //.monoid compose sub-profile super-profile))) + (try.default false)))) + (_.cover [/.unknown-profile] + (case (/.profile fake-name project) + (#try.Success _) + false + + (#try.Failure error) + (exception.match? /.unknown-profile error))) + (_.cover [/.circular-dependency] + (case (/.profile sub-name circular) + (#try.Success _) + false + + (#try.Failure error) + (exception.match? /.circular-dependency error))) + )) + )))) diff --git a/stdlib/source/test/lux/data/number/i64.lux b/stdlib/source/test/lux/data/number/i64.lux index 390861169..592b5fe41 100644 --- a/stdlib/source/test/lux/data/number/i64.lux +++ b/stdlib/source/test/lux/data/number/i64.lux @@ -87,4 +87,22 @@ (if (i.< +0 value) (i.< +0 (/.arithmetic-right-shift idx value)) (i.>= +0 (/.arithmetic-right-shift idx value))))) + (_.cover [/.mask] + (let [mask (/.mask idx) + idempotent? (:: /.equivalence = + (/.and mask pattern) + (/.and mask (/.and mask pattern))) + + limit (inc (.nat mask)) + below-limit? (if (//nat.< limit pattern) + (//nat.= pattern (/.and mask pattern)) + (//nat.< limit (/.and mask pattern))) + + with-empty-mask? (//nat.= 0 (/.and (/.mask 0) pattern)) + with-full-mask? (//nat.= pattern (/.and (/.mask /.width) pattern))] + (and idempotent? + below-limit? + + with-empty-mask? + with-full-mask?))) )))) diff --git a/stdlib/source/test/lux/data/sum.lux b/stdlib/source/test/lux/data/sum.lux index 7434d7509..972677361 100644 --- a/stdlib/source/test/lux/data/sum.lux +++ b/stdlib/source/test/lux/data/sum.lux @@ -1,7 +1,11 @@ (.module: [lux #* ["_" test (#+ Test)] - ["%" data/text/format (#+ format)] + [abstract + [monad (#+ do)] + {[0 #spec] + [/ + ["$." equivalence]]}] [control pipe] [data @@ -9,33 +13,86 @@ [number ["n" nat]] [collection - ["." list]]]] + ["." list ("#@." functor)]]] + [math + ["." random]]] {1 ["." /]}) (def: #export test Test - (<| (_.context (%.name (name-of .|))) - (let [(^open "list/.") (list.equivalence text.equivalence)] - ($_ _.and - (_.test "Can inject values into Either." - (and (|> (/.left "Hello") (case> (0 #0 "Hello") #1 _ #0)) - (|> (/.right "World") (case> (0 #1 "World") #1 _ #0)))) - (_.test "Can discriminate eithers based on their cases." - (let [[_lefts _rights] (/.partition (: (List (| Text Text)) - (list (0 #0 "0") (0 #1 "1") (0 #0 "2"))))] - (and (list/= _lefts - (/.lefts (: (List (| Text Text)) - (list (0 #0 "0") (0 #1 "1") (0 #0 "2"))))) + (<| (_.covering /._) + (do {@ random.monad} + [expected random.nat + shift random.nat]) + ($_ _.and + (_.with-cover [/.equivalence] + ($equivalence.spec (/.equivalence n.equivalence n.equivalence) + (random.or random.nat random.nat))) - (list/= _rights - (/.rights (: (List (| Text Text)) - (list (0 #0 "0") (0 #1 "1") (0 #0 "2")))))))) - (_.test "Can apply a function to an Either value depending on the case." - (and (n.= 10 (/.either (function (_ _) 10) - (function (_ _) 20) - (: (| Text Text) (0 #0 "")))) - (n.= 20 (/.either (function (_ _) 10) - (function (_ _) 20) - (: (| Text Text) (0 #1 "")))))) - )))) + (_.cover [/.left] + (|> (/.left expected) + (: (| Nat Nat)) + (case> (0 #0 actual) (n.= expected actual) + _ false))) + (_.cover [/.right] + (|> (/.right expected) + (: (| Nat Nat)) + (case> (0 #1 actual) (n.= expected actual) + _ false))) + (_.cover [/.either] + (and (|> (/.left expected) + (: (| Nat Nat)) + (/.either (n.+ shift) (n.- shift)) + (n.= (n.+ shift expected))) + (|> (/.right expected) + (: (| Nat Nat)) + (/.either (n.+ shift) (n.- shift)) + (n.= (n.- shift expected))))) + (_.cover [/.each] + (and (|> (/.left expected) + (: (| Nat Nat)) + (/.each (n.+ shift) (n.- shift)) + (case> (0 #0 actual) (n.= (n.+ shift expected) actual) _ false)) + (|> (/.right expected) + (: (| Nat Nat)) + (/.each (n.+ shift) (n.- shift)) + (case> (0 #1 actual) (n.= (n.- shift expected) actual) _ false)))) + (do @ + [size (:: @ map (n.% 5) random.nat) + expected (random.list size random.nat)] + ($_ _.and + (_.cover [/.lefts] + (let [actual (: (List (| Nat Nat)) + (list@map /.left expected))] + (and (:: (list.equivalence n.equivalence) = + expected + (/.lefts actual)) + (:: (list.equivalence n.equivalence) = + (list) + (/.rights actual))))) + (_.cover [/.rights] + (let [actual (: (List (| Nat Nat)) + (list@map /.right expected))] + (and (:: (list.equivalence n.equivalence) = + expected + (/.rights actual)) + (:: (list.equivalence n.equivalence) = + (list) + (/.lefts actual))))) + (_.cover [/.partition] + (let [[lefts rights] (|> expected + (list@map (function (_ value) + (if (n.even? value) + (/.left value) + (/.right value)))) + (: (List (| Nat Nat))) + /.partition)] + (and (:: (list.equivalence n.equivalence) = + (list.filter n.even? expected) + lefts) + (:: (list.equivalence n.equivalence) = + (list.filter (|>> n.even? not) expected) + rights)))) + )) + ))) diff --git a/stdlib/source/test/lux/target/jvm.lux b/stdlib/source/test/lux/target/jvm.lux index 28ea97944..b9639a82f 100644 --- a/stdlib/source/test/lux/target/jvm.lux +++ b/stdlib/source/test/lux/target/jvm.lux @@ -251,6 +251,11 @@ #random ..$Double::random #literal ..$Double::literal}) +(def: valid-double + (Random java/lang/Double) + (random.filter (|>> (:coerce Frac) f.not-a-number? not) + ..$Double::random)) + (def: $Character (/type.class "java.lang.Character" (list))) (def: $Character::wrap @@ -1192,15 +1197,15 @@ (let [test (!::= java/lang/Double "jvm deq" "jvm double =")] ($_ _.and (_.lift "DSTORE_0/DLOAD_0" - (store-and-load ..$Double::random ..$Double::literal ..$Double::wrap [(function.constant /.dstore-0) (function.constant /.dload-0)] test)) + (store-and-load ..valid-double ..$Double::literal ..$Double::wrap [(function.constant /.dstore-0) (function.constant /.dload-0)] test)) (_.lift "DSTORE_1/DLOAD_1" - (store-and-load ..$Double::random ..$Double::literal ..$Double::wrap [(function.constant /.dstore-1) (function.constant /.dload-1)] test)) + (store-and-load ..valid-double ..$Double::literal ..$Double::wrap [(function.constant /.dstore-1) (function.constant /.dload-1)] test)) (_.lift "DSTORE_2/DLOAD_2" - (store-and-load ..$Double::random ..$Double::literal ..$Double::wrap [(function.constant /.dstore-2) (function.constant /.dload-2)] test)) + (store-and-load ..valid-double ..$Double::literal ..$Double::wrap [(function.constant /.dstore-2) (function.constant /.dload-2)] test)) (_.lift "DSTORE_3/DLOAD_3" - (store-and-load ..$Double::random ..$Double::literal ..$Double::wrap [(function.constant /.dstore-3) (function.constant /.dload-3)] test)) + (store-and-load ..valid-double ..$Double::literal ..$Double::wrap [(function.constant /.dstore-3) (function.constant /.dload-3)] test)) (_.lift "DSTORE/DLOAD" - (store-and-load ..$Double::random ..$Double::literal ..$Double::wrap [/.dstore /.dload] test))))) + (store-and-load ..valid-double ..$Double::literal ..$Double::wrap [/.dstore /.dload] test))))) (<| (_.context "object") (let [test (: (-> java/lang/String Any Bit) (function (_ expected actual) |