diff options
Diffstat (limited to '')
| -rw-r--r-- | stdlib/source/test/lux/math/modular.lux | 214 |
1 files changed, 95 insertions, 119 deletions
diff --git a/stdlib/source/test/lux/math/modular.lux b/stdlib/source/test/lux/math/modular.lux index 66eb047fc..849159da2 100644 --- a/stdlib/source/test/lux/math/modular.lux +++ b/stdlib/source/test/lux/math/modular.lux @@ -3,7 +3,13 @@ ["_" test (#+ Test)] ["." type ("#\." equivalence)] [abstract - [monad (#+ do)]] + [monad (#+ do)] + {[0 #spec] + [/ + ["$." equivalence] + ["$." order] + ["$." monoid] + ["$." codec]]}] [control ["." try] ["." exception]] @@ -14,133 +20,103 @@ ["i" int]]] [math ["." random (#+ Random)]]] + ["$." // #_ + ["#" modulus]] {1 ["." / ["/#" // #_ ["#" modulus]]]}) -(def: %3 (//.literal +3)) -(`` (type: Mod3 (~~ (:of %3)))) - -(def: modulusR - (Random Int) - (|> random.int - (\ random.monad map (i.% +1000)) - (random.filter (|>> (i.= +0) not)))) - -(def: valueR - (Random Int) - (|> random.int (\ random.monad map (i.% +1000)))) - -(def: (modR modulus) - (All [m] (-> (//.Modulus m) (Random [Int (/.Mod m)]))) - (do random.monad - [raw valueR] - (wrap [raw (/.modular modulus raw)]))) - -(def: value - (All [m] (-> (/.Mod m) Int)) - (|>> /.un_modular product.right)) - -(def: (comparison m/? i/?) - (All [m] - (-> (-> (/.Mod m) (/.Mod m) Bit) - (-> Int Int Bit) - (-> (/.Mod m) (/.Mod m) Bit))) - (function (_ param subject) - (bit\= (m/? param subject) - (i/? (value param) - (value subject))))) - -(def: (arithmetic modulus m/! i/!) - (All [m] - (-> (//.Modulus m) - (-> (/.Mod m) (/.Mod m) (/.Mod m)) - (-> Int Int Int) - (-> (/.Mod m) (/.Mod m) Bit))) - (function (_ param subject) - (|> (i/! (value param) - (value subject)) - (/.modular modulus) - (/.= (m/! param subject))))) +(def: #export (random modulus) + (All [%] (-> (//.Modulus %) (Random (/.Mod %)))) + (\ random.monad map + (/.modular modulus) + random.int)) (def: #export test Test (<| (_.covering /._) + (_.for [/.Mod]) (do random.monad - [_normalM modulusR - _alternativeM (|> modulusR (random.filter (|>> (i.= _normalM) not))) - #let [normalM (|> _normalM //.modulus try.assume) - alternativeM (|> _alternativeM //.modulus try.assume)] - [_param param] (modR normalM) - [_subject subject] (modR normalM) - #let [copyM (|> normalM //.divisor //.modulus try.assume)]] - ($_ _.and - (_.test "Every modulus has a unique type, even if the numeric value is the same as another." - (and (type\= (:of normalM) - (:of normalM)) - (not (type\= (:of normalM) - (:of alternativeM))) - (not (type\= (:of normalM) - (:of copyM))))) - ## (_.test "Can extract the original integer from the modulus." - ## (i.= _normalM - ## (//.divisor normalM))) - ## (_.test "Can compare mod'ed values." - ## (and (/.= subject subject) - ## ((comparison /.= i.=) param subject) - ## ((comparison /.< i.<) param subject) - ## ((comparison /.<= i.<=) param subject) - ## ((comparison /.> i.>) param subject) - ## ((comparison /.>= i.>=) param subject))) - ## (_.test "Mod'ed values are ordered." - ## (and (bit\= (/.< param subject) - ## (not (/.>= param subject))) - ## (bit\= (/.> param subject) - ## (not (/.<= param subject))) - ## (bit\= (/.= param subject) - ## (not (or (/.< param subject) - ## (/.> param subject)))))) - ## (_.test "Can do arithmetic." - ## (and ((arithmetic normalM /.+ i.+) param subject) - ## ((arithmetic normalM /.- i.-) param subject) - ## ((arithmetic normalM /.* i.*) param subject))) - ## (_.test "Can sometimes find multiplicative inverse." - ## (case (/.inverse subject) - ## (#.Some subject^-1) - ## (|> subject - ## (/.* subject^-1) - ## (/.= (/.modular normalM +1))) - - ## #.None - ## true)) - ## (_.test "Can encode/decode to text." - ## (let [(^open "mod/.") (/.codec normalM)] - ## (case (|> subject mod/encode mod/decode) - ## (#try.Success output) - ## (/.= subject output) - - ## (#try.Failure error) - ## false))) - ## (_.test "Can equalize 2 moduli if they are equal." - ## (case (/.equalize (/.modular normalM _subject) - ## (/.modular copyM _param)) - ## (#try.Success paramC) - ## (/.= param paramC) + [param\\% ($//.random +1,000,000) + param (..random param\\%) - ## (#try.Failure error) - ## false)) - ## (_.test "Cannot equalize 2 moduli if they are the different." - ## (case (/.equalize (/.modular normalM _subject) - ## (/.modular alternativeM _param)) - ## (#try.Success paramA) - ## false + subject\\% (random.filter (|>> (//.= param\\%) not) + ($//.random +1,000,000)) + subject (..random subject\\%) + another (..random subject\\%)] + (`` ($_ _.and + (_.for [/.equivalence /.=] + ($equivalence.spec /.equivalence (..random subject\\%))) + (_.for [/.order /.<] + ($order.spec /.order (..random subject\\%))) + (~~ (template [<compose> <monoid>] + [(_.for [<monoid> <compose>] + ($monoid.spec /.equivalence (<monoid> subject\\%) (..random subject\\%)))] + + [/.+ /.addition] + [/.* /.multiplication] + )) + (_.for [/.codec] + ($codec.spec /.equivalence (/.codec subject\\%) (..random subject\\%))) - ## (#try.Failure error) - ## true)) - ## (_.test "All numbers are congruent to themselves." - ## (//.congruent? normalM _subject _subject)) - ## (_.test "If 2 numbers are congruent under a modulus, then they must also be equal under the same modulus." - ## (bit\= (//.congruent? normalM _param _subject) - ## (/.= param subject))) - )))) + (_.cover [/.incorrect_modulus] + (case (|> param + (\ (/.codec param\\%) encode) + (\ (/.codec subject\\%) decode)) + (#try.Failure error) + (exception.match? /.incorrect_modulus error) + + (#try.Success _) + false)) + (_.cover [/.modulus] + (and (type\= (:of (/.modulus subject)) + (:of (/.modulus subject))) + (not (type\= (:of (/.modulus subject)) + (:of (/.modulus param)))))) + (_.cover [/.modular /.value] + (/.= subject + (/.modular (/.modulus subject) (/.value subject)))) + (_.cover [/.>] + (bit\= (/.> another subject) + (/.< subject another))) + (_.cover [/.<= /.>=] + (bit\= (/.<= another subject) + (/.>= subject another))) + (_.cover [/.-] + (let [zero (/.modular (/.modulus subject) +0)] + (and (/.= zero + (/.- subject subject)) + (/.= subject + (/.- zero subject))))) + (_.cover [/.inverse] + (let [one (/.modular (/.modulus subject) +1) + co-prime? (i.co-prime? (//.divisor (/.modulus subject)) + (/.value subject))] + (case (/.inverse subject) + (#.Some subject^-1) + (and co-prime? + (|> subject + (/.* subject^-1) + (/.= one))) + + #.None + (not co-prime?)))) + (_.cover [/.adapter] + (<| (try.default false) + (do try.monad + [copy\\% (//.modulus (//.divisor subject\\%)) + adapt (/.adapter subject\\% copy\\%)] + (wrap (|> subject + /.value + (/.modular copy\\%) + adapt + (/.= subject)))))) + (_.cover [/.moduli_are_not_equal] + (case (/.adapter subject\\% param\\%) + (#try.Failure error) + (exception.match? /.moduli_are_not_equal error) + + (#try.Success _) + false)) + ))))) |