aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lux-mode/lux-mode.el2
-rw-r--r--stdlib/source/library/lux/data/format/css/value.lux22
-rw-r--r--stdlib/source/library/lux/tool/compiler/language/lux/analysis/type.lux2
-rw-r--r--stdlib/source/library/lux/type/unit.lux153
-rw-r--r--stdlib/source/test/lux/type/unit.lux6
5 files changed, 93 insertions, 92 deletions
diff --git a/lux-mode/lux-mode.el b/lux-mode/lux-mode.el
index 6979865fd..c395fb841 100644
--- a/lux-mode/lux-mode.el
+++ b/lux-mode/lux-mode.el
@@ -375,7 +375,7 @@ Called by `imenu--generic-function'."
"type"))
(type//checking (altRE "is" "as" "let" "as_expected" "type_of" "sharing" "by_example" "hole"))
(type//primitive (altRE "primitive:" "abstraction" "representation" "transmutation"))
- (type//unit (altRE "unit:" "scale:"))
+ (type//unit (altRE "scale:"))
(type//poly (altRE "polytypic"))
(type//dynamic (altRE "dynamic" "static"))
(type//capability (altRE "capability:"))
diff --git a/stdlib/source/library/lux/data/format/css/value.lux b/stdlib/source/library/lux/data/format/css/value.lux
index 79636d63a..e2bf08a20 100644
--- a/stdlib/source/library/lux/data/format/css/value.lux
+++ b/stdlib/source/library/lux/data/format/css/value.lux
@@ -50,14 +50,6 @@
(template.spliced <definition>+))]))
-(def: multi:
- (template (multi: <multi> <type> <separator>)
- [(def: .public (<multi> pre post)
- (-> (Value <type>) (Value <type>) (Value <type>))
- (abstraction (format (representation pre)
- <separator>
- (representation post))))]))
-
(def: (%number value)
(Format Frac)
(let [raw (%.frac value)]
@@ -1334,9 +1326,17 @@
(%.int index)
(%.nat (.nat index)))))
- (multi: multi_image Image ",")
- (multi: multi_shadow Shadow ",")
- (multi: multi_content Content " ")
+ (with_template [<separator> <type> <multi>]
+ [(def: .public (<multi> pre post)
+ (-> (Value <type>) (Value <type>) (Value <type>))
+ (abstraction (format (representation pre)
+ <separator>
+ (representation post))))]
+
+ ["," Image multi_image]
+ ["," Shadow multi_shadow]
+ [" " Content multi_content]
+ )
... https://developer.mozilla.org/en-US/docs/Web/CSS/calc()
(with_template [<name> <parameter>]
diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/analysis/type.lux b/stdlib/source/library/lux/tool/compiler/language/lux/analysis/type.lux
index f1a2943ff..dba3ad176 100644
--- a/stdlib/source/library/lux/tool/compiler/language/lux/analysis/type.lux
+++ b/stdlib/source/library/lux/tool/compiler/language/lux/analysis/type.lux
@@ -57,7 +57,7 @@
(Operation Type)
(do phase.monad
[module (extension.lifted meta.current_module_name)
- [id _] (..check check.existential)]
+ id (extension.lifted meta.seed)]
(in (..existential' module id))))
(def: .public (expecting expected)
diff --git a/stdlib/source/library/lux/type/unit.lux b/stdlib/source/library/lux/type/unit.lux
index bae4b1bfb..6c6fec8a3 100644
--- a/stdlib/source/library/lux/type/unit.lux
+++ b/stdlib/source/library/lux/type/unit.lux
@@ -1,6 +1,6 @@
(.using
[library
- [lux (.except)
+ [lux (.except type)
["[0]" meta]
[abstract
[monad (.only Monad do)]
@@ -13,7 +13,7 @@
[data
["[0]" text (.only)
["%" \\format (.only format)]]]
- [macro
+ ["[0]" macro (.only)
["[0]" code]
["[0]" template]
[syntax (.only syntax)
@@ -22,21 +22,45 @@
[number
["n" nat]
["i" int]
- ["[0]" ratio (.only Ratio)]]]
- [type
- [primitive (.except)]]]])
+ ["[0]" ratio (.only Ratio)]]]]]
+ ["[0]" // (.only)
+ [primitive (.except)]])
(primitive: .public (Qty unit)
Int
-
- (def: in'
- (All (_ unit) (-> Int (Qty unit)))
+
+ (type: .public Pure
+ (Qty Any))
+
+ (def: .public pure
+ (-> Int Pure)
(|>> abstraction))
- (def: out'
- (All (_ unit) (-> (Qty unit) Int))
+ (def: .public number
+ (-> Pure Int)
(|>> representation))
+ (def: .public equivalence
+ (All (_ unit) (Equivalence (Qty unit)))
+ (implementation
+ (def: (= reference sample)
+ (i.= (representation reference) (representation sample)))))
+
+ (def: .public order
+ (All (_ unit) (Order (Qty unit)))
+ (implementation
+ (def: equivalence ..equivalence)
+
+ (def: (< reference sample)
+ (i.< (representation reference) (representation sample)))))
+
+ (def: .public enum
+ (All (_ unit) (Enum (Qty unit)))
+ (implementation
+ (def: order ..order)
+ (def: succ (|>> representation ++ abstraction))
+ (def: pred (|>> representation -- abstraction))))
+
(with_template [<name> <op>]
[(def: .public (<name> param subject)
(All (_ unit) (-> (Qty unit) (Qty unit) (Qty unit)))
@@ -56,14 +80,50 @@
[* i.* p s [p s]]
[/ i./ p [p s] s]
)
+
+ (type: .public (Unit a)
+ (Interface
+ (is (-> Int (Qty a))
+ in)
+ (is (-> (Qty 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))
)
-(type: .public (Unit a)
- (Interface
- (is (-> Int (Qty a))
- in)
- (is (-> (Qty a) Int)
- out)))
+(def: .public type
+ (syntax (_ [it <code>.any])
+ (macro.with_symbols [g!a]
+ (in (list (` ((~! //.by_example) [(~ g!a)]
+ (Unit (~ g!a))
+ (~ it)
+
+ (~ g!a))))))))
+
+(with_template [<unit> <type>]
+ [(def: .public <unit>
+ (..unit []))
+
+ (type: .public <type>
+ (~ (..type <unit>)))]
+
+ [gram Gram]
+ [meter Meter]
+ [litre Litre]
+ [second Second]
+ )
(type: .public (Scale s)
(Interface
@@ -74,36 +134,6 @@
(is Ratio
ratio)))
-(type: .public Pure
- (Qty Any))
-
-(def: .public pure
- (-> Int Pure)
- ..in')
-
-(def: .public number
- (-> Pure Int)
- ..out')
-
-(def: .public unit:
- (syntax (_ [[export_policy type_name unit_name]
- (|export|.parser
- (all <>.and
- <code>.local
- <code>.local))])
- (do meta.monad
- [@ meta.current_module_name
- .let [g!type (code.local type_name)]]
- (in (list (` (type: (~ export_policy) (~ g!type)
- (Primitive (~ (code.text (%.symbol [@ type_name]))))))
-
- (` (def: (~ export_policy) (~ (code.local unit_name))
- (..Unit (~ g!type))
- (implementation
- (def: (~' in) (~! ..in'))
- (def: (~' out) (~! ..out')))))
- )))))
-
(def: scaleP
(Parser Ratio)
(<code>.tuple (do <>.monad
@@ -174,34 +204,3 @@
[Micro 1,000,000 1]
[Nano 1,000,000,000 1]
)
-
-(with_template [<type>]
- [(`` (unit: .public <type>
- (~~ (implementation_name <type>))))]
-
- [Gram]
- [Meter]
- [Litre]
- [Second]
- )
-
-(def: .public equivalence
- (All (_ unit) (Equivalence (Qty unit)))
- (implementation
- (def: (= reference sample)
- (i.= (..out' reference) (..out' sample)))))
-
-(def: .public order
- (All (_ unit) (Order (Qty unit)))
- (implementation
- (def: equivalence ..equivalence)
-
- (def: (< reference sample)
- (i.< (..out' reference) (..out' sample)))))
-
-(def: .public enum
- (All (_ unit) (Enum (Qty unit)))
- (implementation
- (def: order ..order)
- (def: succ (|>> ..out' ++ ..in'))
- (def: pred (|>> ..out' -- ..in'))))
diff --git a/stdlib/source/test/lux/type/unit.lux b/stdlib/source/test/lux/type/unit.lux
index 1006d9dbb..b4662133e 100644
--- a/stdlib/source/test/lux/type/unit.lux
+++ b/stdlib/source/test/lux/type/unit.lux
@@ -45,7 +45,8 @@
($enum.spec /.enum (..meter 1,000)))
))
-(/.unit: What what)
+(def: what (/.unit []))
+(def: What (/.type what))
(def: unit
Test
@@ -70,9 +71,10 @@
/.pure
/.number
(i.= expected)))
- (_.coverage [/.unit:]
+ (_.coverage [/.unit /.type]
(|> expected
(at ..what in)
+ (is (/.Qty What))
(at ..what out)
(i.= expected)))
)))))
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 18:11:35 +0000