From e3f6c988699be9f83fbc4a2bc4730f7df7f8eca0 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Sun, 24 Dec 2017 18:09:07 -0400 Subject: - Added type-safe modular arithmetic. --- stdlib/source/lux/data/text/format.lux | 14 ++- stdlib/source/lux/math/modular.lux | 167 +++++++++++++++++++++++++++++++++ stdlib/test/test/lux/math/modular.lux | 146 ++++++++++++++++++++++++++++ stdlib/test/tests.lux | 2 +- 4 files changed, 324 insertions(+), 5 deletions(-) create mode 100644 stdlib/source/lux/math/modular.lux create mode 100644 stdlib/test/test/lux/math/modular.lux (limited to 'stdlib') diff --git a/stdlib/source/lux/data/text/format.lux b/stdlib/source/lux/data/text/format.lux index 1c56f1cb9..80d672d67 100644 --- a/stdlib/source/lux/data/text/format.lux +++ b/stdlib/source/lux/data/text/format.lux @@ -12,6 +12,7 @@ (time [instant] [duration] [date]) + (math [modular]) [macro] (macro [code] ["s" syntax #+ syntax: Syntax]) @@ -26,14 +27,14 @@ (wrap (list (` (let [(~ g!compose) (:: (~! text.Monoid) (~' compose))] ($_ (~ g!compose) (~+ fragments)))))))) -## [Formatters] -(type: #export (Formatter a) +## [Formats] +(type: #export (Format a) {#.doc "A way to produce readable text from values."} (-> a Text)) (do-template [ ] [(def: #export - (Formatter ) + (Format ) )] [%b Bool (:: bool.Codec encode)] @@ -55,8 +56,13 @@ [%date date.Date (:: date.Codec encode)] ) +(def: #export (%mod modular) + (All [m] (Format (modular.Mod m))) + (let [[_ modulus] (modular.un-mod modular)] + (:: (modular.Codec modulus) encode modular))) + (def: #export (%list formatter) - (All [a] (-> (Formatter a) (Formatter (List a)))) + (All [a] (-> (Format a) (Format (List a)))) (function [values] (case values #.Nil diff --git a/stdlib/source/lux/math/modular.lux b/stdlib/source/lux/math/modular.lux new file mode 100644 index 000000000..7618a3a55 --- /dev/null +++ b/stdlib/source/lux/math/modular.lux @@ -0,0 +1,167 @@ +(.module: + lux + (lux (control ["ex" exception #+ exception:] + ["p" parser] + [codec #+ Codec] + [monad #+ do]) + (data ["e" error #+ Error] + [number "int/" Codec] + [text "text/" Monoid] + (text ["l" lexer #+ Lexer])) + (type abstract) + (macro [code] + ["s" syntax #+ syntax:]) + [math])) + +(exception: #export Zero-Cannot-Be-A-Modulus) +(exception: #export Cannot-Equalize-Numbers) +(exception: #export Incorrect-Modulus) + +(abstract: #export (Modulus m) + {#.doc "A number used as a modulus in modular arithmetic. + It cannot be 0."} + + Int + + (def: #export (from-int value) + (Ex [m] (-> Int (Error (Modulus m)))) + (if (i/= 0 value) + (#e.Error (Zero-Cannot-Be-A-Modulus "")) + (#e.Success (@abstraction value)))) + + (def: #export (to-int modulus) + (All [m] (-> (Modulus m) Int)) + (|> modulus @representation)) + ) + +(def: #export (congruent? modulus reference sample) + (All [m] (-> (Modulus m) Int Int Bool)) + (|> sample + (i/- reference) + (i/% (to-int modulus)) + (i/= 0))) + +(syntax: #export (modulus [modulus s.int]) + (case (from-int modulus) + (#e.Success _) + (wrap (list (` (e.assume (..from-int (~ (code.int modulus))))))) + + (#e.Error error) + (p.fail error))) + +(def: (i/mod (^|> modulus [to-int]) + value) + (All [m] (-> (Modulus m) Int Int)) + (let [raw (i/% modulus value)] + (if (i/< 0 raw) + (let [shift (if (i/< 0 modulus) i/- i/+)] + (|> raw (shift modulus))) + raw))) + +(def: intL + (Lexer Int) + (p.codec number.Codec + (p.either (l.seq (l.one-of "-") (l.many l.decimal)) + (l.many l.decimal)))) + +(abstract: #export (Mod m) + {#.doc "A number under a modulus."} + + {#remainder Int + #modulus (Modulus m)} + + (def: #export (mod modulus) + (All [m] (-> (Modulus m) (-> Int (Mod m)))) + (function [value] + (@abstraction {#remainder (i/mod modulus value) + #modulus modulus}))) + + (def: #export (un-mod modular) + (All [m] (-> (Mod m) [Int (Modulus m)])) + (@representation modular)) + + (def: separator Text " mod ") + + (struct: #export (Codec modulus) + (All [m] (-> (Modulus m) (Codec Text (Mod m)))) + + (def: (encode modular) + (let [[remainder modulus] (@representation modular)] + ($_ text/compose + (int/encode remainder) + separator + (int/encode (to-int modulus))))) + + (def: (decode text) + (<| (l.run text) + (do p.Monad + [[remainder _ _modulus] ($_ p.seq intL (l.this separator) intL) + _ (p.assert (Incorrect-Modulus + ($_ text/compose + "Expected modulus: " (int/encode (to-int modulus)) "\n" + " Actual modulus: " (int/encode _modulus) "\n")) + (i/= (to-int modulus) _modulus))] + (wrap (mod modulus remainder)))))) + + (def: #export (equalize reference sample) + (All [r s] (-> (Mod r) (Mod s) (Error (Mod r)))) + (let [[reference reference-modulus] (@representation reference) + [sample sample-modulus] (@representation sample)] + (if (i/= (to-int reference-modulus) + (to-int sample-modulus)) + (#e.Success (@abstraction {#remainder sample + #modulus reference-modulus})) + (#e.Error (Cannot-Equalize-Numbers + ($_ text/compose + "Reference modulus: " (int/encode (to-int reference-modulus)) "\n" + " Sample modulus: " (int/encode (to-int sample-modulus)) "\n")))))) + + (do-template [ ] + [(def: #export ( reference sample) + (All [m] (-> (Mod m) (Mod m) Bool)) + (let [[reference _] (@representation reference) + [sample _] (@representation sample)] + ( reference sample)))] + + [m/= i/=] + [m/< i/<] + [m/<= i/<=] + [m/> i/>] + [m/>= i/>=] + ) + + (do-template [ ] + [(def: #export ( param subject) + (All [m] (-> (Mod m) (Mod m) (Mod m))) + (let [[param modulus] (@representation param) + [subject _] (@representation subject)] + (@abstraction {#remainder (|> subject + ( param) + (i/mod modulus)) + #modulus modulus})))] + + [m/+ i/+] + [m/- i/-] + [m/* i/*]) + + (def: (i/gcd+ a b) + (-> Int Int [Int Int Int]) + (if (i/= 0 a) + [0 1 b] + (let [[ak bk gcd] (i/gcd+ (i/% a b) a)] + [(i/- (i/* ak + (i// a b)) + bk) + ak + gcd]))) + + (def: #export (inverse modular) + (All [m] (-> (Mod m) (Maybe (Mod m)))) + (let [[value modulus] (@representation modular) + _modulus (to-int modulus) + [vk mk gcd] (i/gcd+ value _modulus) + co-prime? (i/= 1 gcd)] + (if co-prime? + (#.Some (mod modulus vk)) + #.None))) + ) diff --git a/stdlib/test/test/lux/math/modular.lux b/stdlib/test/test/lux/math/modular.lux new file mode 100644 index 000000000..76d56cbc2 --- /dev/null +++ b/stdlib/test/test/lux/math/modular.lux @@ -0,0 +1,146 @@ +(.module: + lux + (lux (control [monad #+ do]) + (data [product] + [bool "bool/" Eq] + ["e" error] + text/format) + (math ["r" random] + ["/" modular]) + (lang [type "type/" Eq])) + lux/test) + +(def: %3 (/.modulus 3)) +(def: Mod3 Type (type-of %3)) + +(def: modulusR + (r.Random Int) + (|> r.int + (:: r.Monad map (i/% 1000)) + (r.filter (|>> (i/= 0) not)))) + +(def: valueR + (r.Random Int) + (|> r.int (:: r.Monad map (i/% 1000)))) + +(def: (modR modulus) + (All [m] (-> (/.Modulus m) (r.Random [Int (/.Mod m)]))) + (do r.Monad + [raw valueR] + (wrap [raw (/.mod modulus raw)]))) + +(def: value + (All [m] (-> (/.Mod m) Int)) + (|>> /.un-mod product.left)) + +(def: (comparison m/? i/?) + (All [m] + (-> (-> (/.Mod m) (/.Mod m) Bool) + (-> Int Int Bool) + (-> (/.Mod m) (/.Mod m) Bool))) + (function [param subject] + (bool/= (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) Bool))) + (function [param subject] + (|> (i/! (value param) + (value subject)) + (/.mod modulus) + (/.m/= (m/! param subject))))) + +(context: "Modular arithmetic." + (<| (times +100) + (do @ + [_normalM modulusR + _alternativeM (|> modulusR (r.filter (|>> (i/= _normalM) not))) + #let [normalM (|> _normalM /.from-int e.assume) + alternativeM (|> _alternativeM /.from-int e.assume)] + [_param param] (modR normalM) + [_subject subject] (modR normalM) + #let [copyM (|> normalM /.to-int /.from-int e.assume)]] + ($_ seq + (test "Every modulus has a unique type, even if the numeric value is the same as another." + (and (type/= (type-of normalM) + (type-of normalM)) + (not (type/= (type-of normalM) + (type-of alternativeM))) + (not (type/= (type-of normalM) + (type-of copyM))))) + + (test "Can extract the original integer from the modulus." + (i/= _normalM + (/.to-int normalM))) + + (test "Can compare mod'ed values." + (and (/.m/= subject subject) + ((comparison /.m/= i/=) param subject) + ((comparison /.m/< i/<) param subject) + ((comparison /.m/<= i/<=) param subject) + ((comparison /.m/> i/>) param subject) + ((comparison /.m/>= i/>=) param subject))) + + (test "Mod'ed values are ordered." + (and (bool/= (/.m/< param subject) + (not (/.m/>= param subject))) + (bool/= (/.m/> param subject) + (not (/.m/<= param subject))) + (bool/= (/.m/= param subject) + (not (or (/.m/< param subject) + (/.m/> param subject)))))) + + (test "Can do arithmetic." + (and ((arithmetic normalM /.m/+ i/+) param subject) + ((arithmetic normalM /.m/- i/-) param subject) + ((arithmetic normalM /.m/* i/*) param subject))) + + (test "Can sometimes find multiplicative inverse." + (case (/.inverse subject) + (#.Some subject^-1) + (|> subject + (/.m/* subject^-1) + (/.m/= (/.mod normalM 1))) + + #.None + true)) + + (test "Can encode/decode to text." + (let [(^open "mod/") (/.Codec normalM)] + (case (|> subject mod/encode mod/decode) + (#e.Success output) + (/.m/= subject output) + + (#e.Error error) + false))) + + (test "Can equalize 2 moduli if they are equal." + (case (/.equalize (/.mod normalM _subject) + (/.mod copyM _param)) + (#e.Success paramC) + (/.m/= param paramC) + + (#e.Error error) + false)) + + (test "Cannot equalize 2 moduli if they are the different." + (case (/.equalize (/.mod normalM _subject) + (/.mod alternativeM _param)) + (#e.Success paramA) + false + + (#e.Error 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." + (bool/= (/.congruent? normalM _param _subject) + (/.m/= param subject))) + )))) diff --git a/stdlib/test/tests.lux b/stdlib/test/tests.lux index 899582b54..1742334d8 100644 --- a/stdlib/test/tests.lux +++ b/stdlib/test/tests.lux @@ -56,6 +56,7 @@ ["_." regex])) ["_." math] (math ["_." random] + ["_." modular] (logic ["_." continuous] ["_." fuzzy])) (macro ["_." code] @@ -82,7 +83,6 @@ [html] [css]) (coll (tree ["tree_." parser]))) - (math [random]) [macro] (macro (poly [json])) (type [unit]) -- cgit v1.2.3