diff options
Diffstat (limited to 'stdlib/source/library/lux/type/unit.lux')
| -rw-r--r-- | stdlib/source/library/lux/type/unit.lux | 137 |
1 files changed, 18 insertions, 119 deletions
diff --git a/stdlib/source/library/lux/type/unit.lux b/stdlib/source/library/lux/type/unit.lux index 6c6fec8a3..1d2cc20ca 100644 --- a/stdlib/source/library/lux/type/unit.lux +++ b/stdlib/source/library/lux/type/unit.lux @@ -1,53 +1,40 @@ (.using [library [lux (.except type) - ["[0]" meta] [abstract - [monad (.only Monad do)] [equivalence (.only Equivalence)] [order (.only Order)] [enum (.only Enum)]] [control - ["<>" parser (.open: "[1]#[0]" monad) - ["<[0]>" code (.only Parser)]]] - [data - ["[0]" text (.only) - ["%" \\format (.only format)]]] + [parser + ["<[0]>" code]]] ["[0]" macro (.only) - ["[0]" code] - ["[0]" template] - [syntax (.only syntax) - ["|[0]|" export]]] + [syntax (.only syntax)]] [math [number - ["n" nat] - ["i" int] - ["[0]" ratio (.only Ratio)]]]]] + ["i" int]]]]] ["[0]" // (.only) [primitive (.except)]]) -(primitive: .public (Qty unit) +(primitive: .public (Qty scale unit) Int - (type: .public Pure - (Qty Any)) - - (def: .public pure - (-> Int Pure) + (def: .public quantity + (All (_ scale unit) (-> Int (Qty scale unit))) (|>> abstraction)) (def: .public number - (-> Pure Int) + (All (_ scale unit) (-> (Qty scale unit) Int)) (|>> representation)) (def: .public equivalence - (All (_ unit) (Equivalence (Qty unit))) + (All (_ scale unit) (Equivalence (Qty scale unit))) (implementation (def: (= reference sample) (i.= (representation reference) (representation sample))))) (def: .public order - (All (_ unit) (Order (Qty unit))) + (All (_ scale unit) (Order (Qty scale unit))) (implementation (def: equivalence ..equivalence) @@ -55,7 +42,7 @@ (i.< (representation reference) (representation sample))))) (def: .public enum - (All (_ unit) (Enum (Qty unit))) + (All (_ scale unit) (Enum (Qty scale unit))) (implementation (def: order ..order) (def: succ (|>> representation ++ abstraction)) @@ -63,7 +50,7 @@ (with_template [<name> <op>] [(def: .public (<name> param subject) - (All (_ unit) (-> (Qty unit) (Qty unit) (Qty unit))) + (All (_ scale unit) (-> (Qty scale unit) (Qty scale unit) (Qty scale unit))) (abstraction (<op> (representation param) (representation subject))))] @@ -73,7 +60,7 @@ (with_template [<name> <op> <p> <s> <p*s>] [(def: .public (<name> param subject) - (All (_ p s) (-> (Qty <p>) (Qty <s>) (Qty <p*s>))) + (All (_ scale p s) (-> (Qty scale <p>) (Qty scale <s>) (Qty scale <p*s>))) (abstraction (<op> (representation param) (representation subject))))] @@ -83,31 +70,23 @@ (type: .public (Unit a) (Interface - (is (-> Int (Qty a)) + (is (-> Int (Qty Any a)) in) - (is (-> (Qty a) Int) + (is (-> (Qty Any a) Int) out))) (def: .public (unit _) (Ex (_ a) (-> Any (Unit a))) (implementation - (def: in (|>> abstraction)) - (def: out (|>> representation)))) - - (def: in' - (All (_ unit) (-> Int (Qty unit))) - (|>> abstraction)) - - (def: out' - (All (_ unit) (-> (Qty unit) Int)) - (|>> representation)) + (def: in ..quantity) + (def: out ..number))) ) (def: .public type (syntax (_ [it <code>.any]) (macro.with_symbols [g!a] (in (list (` ((~! //.by_example) [(~ g!a)] - (Unit (~ g!a)) + (..Unit (~ g!a)) (~ it) (~ g!a)))))))) @@ -124,83 +103,3 @@ [litre Litre] [second Second] ) - -(type: .public (Scale s) - (Interface - (is (All (_ u) (-> (Qty u) (Qty (s u)))) - scale) - (is (All (_ u) (-> (Qty (s u)) (Qty u))) - de_scale) - (is Ratio - ratio))) - -(def: scaleP - (Parser Ratio) - (<code>.tuple (do <>.monad - [numerator <code>.nat - _ (<>.assertion (format "Numerator must be positive: " (%.nat numerator)) - (n.> 0 numerator)) - denominator <code>.nat - _ (<>.assertion (format "Denominator must be positive: " (%.nat denominator)) - (n.> 0 denominator))] - (in [numerator denominator])))) - -(def: .public scale: - (syntax (_ [[export_policy type_name scale_name ratio] - (|export|.parser - (all <>.and - <code>.local - <code>.local - ..scaleP))]) - (do meta.monad - [.let [(open "_[0]") ratio] - @ meta.current_module_name - .let [g!scale (code.local type_name)]] - (in (list (` (type: (~ export_policy) ((~ g!scale) (~' u)) - (Primitive (~ (code.text (%.symbol [@ type_name]))) [(~' u)]))) - - (` (def: (~ export_policy) (~ (code.local scale_name)) - (..Scale (~ g!scale)) - (implementation - (def: (~' scale) - (|>> ((~! ..out')) - (i.* (~ (code.int (.int _#numerator)))) - (i./ (~ (code.int (.int _#denominator)))) - ((~! ..in')))) - (def: (~' de_scale) - (|>> ((~! ..out')) - (i.* (~ (code.int (.int _#denominator)))) - (i./ (~ (code.int (.int _#numerator)))) - ((~! ..in')))) - (def: (~' ratio) - [(~ (code.nat _#numerator)) - (~ (code.nat _#denominator))])))) - ))))) - -(def: .public (re_scaled from to quantity) - (All (_ si so u) (-> (Scale si) (Scale so) (Qty (si u)) (Qty (so u)))) - (let [[numerator denominator] (ratio./ (at from ratio) - (at to ratio))] - (|> quantity - out' - (i.* (.int numerator)) - (i./ (.int denominator)) - in'))) - -(def: implementation_name - (syntax (_ [type_name <code>.local]) - (in (list (code.local (text.lower_cased type_name)))))) - -(with_template [<type> <from> <to>] - [(`` (scale: .public <type> - (~~ (implementation_name <type>)) - [<from> <to>]))] - - [Kilo 1 1,000] - [Mega 1 1,000,000] - [Giga 1 1,000,000,000] - - [Milli 1,000 1] - [Micro 1,000,000 1] - [Nano 1,000,000,000 1] - ) |