diff options
Diffstat (limited to 'stdlib/source/lux/type/unit.lux')
| -rw-r--r-- | stdlib/source/lux/type/unit.lux | 183 |
1 files changed, 183 insertions, 0 deletions
diff --git a/stdlib/source/lux/type/unit.lux b/stdlib/source/lux/type/unit.lux new file mode 100644 index 000000000..de00fb82d --- /dev/null +++ b/stdlib/source/lux/type/unit.lux @@ -0,0 +1,183 @@ +(;module: + lux + (lux (control [monad #+ do Monad] + ["p" parser "p/" Monad<Parser>] + [eq #+ Eq] + [order #+ Order] + [enum #+ Enum]) + (data text/format + (number ["r" ratio])) + [meta] + (meta [code] + ["s" syntax #+ syntax:] + (syntax ["cs" common] + (common ["csr" reader] + ["csw" writer]))))) + +(type: #export (Qty unit) + [Int unit]) + +(sig: #export (Scale s) + (: (All [u] (-> (Qty u) (Qty (s u)))) + scale) + (: (All [u] (-> (Qty (s u)) (Qty u))) + de-scale) + (: r;Ratio + ratio)) + +(type: #export Pure + (Qty [])) + +(type: #export (Per d n) + (-> d n)) + +(type: #export (Inverse u) + (|> Pure (Per u))) + +(type: #export (Product p s) + (|> s (Per (Inverse p)))) + +(def: #export (in carrier magnitude) + (All [unit] (-> unit Int (Qty unit))) + [magnitude carrier]) + +(def: #export (pure magnitude) + (-> Int Pure) + (in [] magnitude)) + +(def: #export (out quantity) + (All [unit] (-> (Qty unit) Int)) + (let [[magnitude carrier] quantity] + magnitude)) + +(def: (carrier quantity) + (All [unit] (-> (Qty unit) unit)) + (let [[magnitude carrier] quantity] + carrier)) + +(do-template [<name> <tag>] + [(def: <name> + (-> Text Text) + (|>. (format "{" kind "@" module "}") + (let [[module kind] (ident-for <tag>)])))] + + [unit-name #;;Unit] + [scale-name #;;Scale] + ) + +(syntax: #export (unit: [export csr;export] + [name s;local-symbol] + [annotations (p;default cs;empty-annotations csr;annotations)]) + (wrap (list (` (type: (~@ (csw;export export)) (~ (code;local-symbol name)) + (~ (csw;annotations annotations)) + (primitive (~ (code;local-symbol (unit-name name)))))) + (` (def: (~@ (csw;export export)) (~ (code;local-symbol (format "@" name))) + (~ (code;local-symbol name)) + (:!! []))) + ))) + +(def: ratio^ + (s;Syntax r;Ratio) + (s;tuple (do p;Monad<Parser> + [numerator s;int + _ (p;assert (format "Numerator must be positive: " (%i numerator)) + (i.> 0 numerator)) + denominator s;int + _ (p;assert (format "Denominator must be positive: " (%i denominator)) + (i.> 0 denominator))] + (wrap [(int-to-nat numerator) (int-to-nat denominator)])))) + +(syntax: #export (scale: [export csr;export] + [name s;local-symbol] + [(^slots [#r;numerator #r;denominator]) ratio^] + [annotations (p;default cs;empty-annotations csr;annotations)]) + (let [g!scale (code;local-symbol name)] + (wrap (list (` (type: (~@ (csw;export export)) ((~ g!scale) (~' u)) + (~ (csw;annotations annotations)) + (primitive (~ (code;local-symbol (scale-name name))) [(~' u)]))) + (` (struct: (~@ (csw;export export)) (~ (code;local-symbol (format "@" name))) + (;;Scale (~ g!scale)) + (def: (~' scale) + (|>. ;;out + (i.* (~ (code;int (nat-to-int numerator)))) + (i./ (~ (code;int (nat-to-int denominator)))) + (;;in (:! ((~ g!scale) ($ +0)) [])))) + (def: (~' de-scale) + (|>. ;;out + (i.* (~ (code;int (nat-to-int denominator)))) + (i./ (~ (code;int (nat-to-int numerator)))) + (;;in (:! ($ +0) [])))) + (def: (~' ratio) + [(~ (code;nat numerator)) (~ (code;nat denominator))]))) + )))) + +(do-template [<name> <op>] + [(def: #export (<name> param subject) + (All [unit] (-> (Qty unit) (Qty unit) (Qty unit))) + (|> (out subject) (<op> (out param)) (in (carrier subject))))] + + [++ i.+] + [-- i.-] + ) + +(def: #export (// param subject) + (All [p s] (-> (Qty p) (Qty s) (|> (Qty s) (Per (Qty p))))) + (function [input] + (|> (out subject) + (i.* (out input)) + (i./ (out param)) + (in (carrier subject))))) + +(def: #export (** param subject) + (All [p s] (-> (Qty p) (Qty s) (Product (Qty p) (Qty s)))) + (function [input] + (|> (out subject) + (i.* (out (input param))) + (in (carrier subject))))) + +(def: #export (re-scale from to quantity) + (All [si so u] (-> (Scale si) (Scale so) (Qty (si u)) (Qty (so u)))) + (let [[numerator denominator] (|> (:: to ratio) (r;q./ (:: from ratio)))] + (|> quantity out + (i.* (nat-to-int numerator)) + (i./ (nat-to-int denominator)) + (in (:! (($ +1) ($ +2)) []))))) + +(scale: #export Kilo [1 1_000]) +(scale: #export Mega [1 1_000_000]) +(scale: #export Giga [1 1_000_000_000]) + +(scale: #export Milli [ 1_000 1]) +(scale: #export Micro [ 1_000_000 1]) +(scale: #export Nano [1_000_000_000 1]) + +(def: #export (as scale unit magnitude) + (All [s u] (-> (Scale s) u Int (Qty (s u)))) + (let [[_ carrier] (|> 0 (in unit) (:: scale scale))] + [magnitude carrier])) + +(unit: #export Gram) +(unit: #export Meter) +(unit: #export Litre) +(unit: #export Second) + +(struct: #export Eq<Unit> (All [unit] (Eq (Qty unit))) + (def: (= reference sample) + (i.= (out reference) (out sample)))) + +(struct: #export Order<Unit> (All [unit] (Order (Qty unit))) + (def: eq Eq<Unit>) + + (do-template [<name> <func>] + [(def: (<name> reference sample) + (<func> (out reference) (out sample)))] + + [< i.<] + [<= i.<=] + [> i.>] + [>= i.>=])) + +(struct: #export Enum<Unit> (All [unit] (Enum (Qty unit))) + (def: order Order<Unit>) + (def: (succ qty) (|> (out qty) i.inc (in (carrier qty)))) + (def: (pred qty) (|> (out qty) i.dec (in (carrier qty))))) |