aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/library/lux/meta/type.lux
diff options
context:
space:
mode:
Diffstat (limited to 'stdlib/source/library/lux/meta/type.lux')
-rw-r--r--stdlib/source/library/lux/meta/type.lux102
1 files changed, 67 insertions, 35 deletions
diff --git a/stdlib/source/library/lux/meta/type.lux b/stdlib/source/library/lux/meta/type.lux
index afe41bec4..7952b99d8 100644
--- a/stdlib/source/library/lux/meta/type.lux
+++ b/stdlib/source/library/lux/meta/type.lux
@@ -6,7 +6,8 @@
[lux (.except function as let)
[abstract
[equivalence (.only Equivalence)]
- [monad (.only Monad do)]]
+ [monad (.only Monad do)]
+ [codec (.only Codec)]]
[control
["<>" parser]
["[0]" function]
@@ -22,7 +23,7 @@
["n" nat (.use "[1]#[0]" decimal)]]]
["[0]" meta (.only)
["[0]" location]
- ["[0]" symbol (.use "[1]#[0]" equivalence codec)]
+ ["[0]" symbol (.use "[1]#[0]" equivalence)]
["[0]" code (.only)
["<[1]>" \\parser (.only Parser)]]
["[0]" macro (.only)
@@ -33,7 +34,8 @@
(with_template [<name> <tag>]
[(def .public (<name> type)
- (-> Type [Nat Type])
+ (-> Type
+ [Nat Type])
(loop (again [num_args 0
type type])
(when type
@@ -48,7 +50,8 @@
)
(def .public (flat_function type)
- (-> Type [(List Type) Type])
+ (-> Type
+ [(List Type) Type])
(when type
{.#Function in out'}
(.let [[ins out] (flat_function out')]
@@ -58,7 +61,8 @@
[(list) type]))
(def .public (flat_application type)
- (-> Type [Type (List Type)])
+ (-> Type
+ [Type (List Type)])
(when type
{.#Apply arg func'}
(.let [[func args] (flat_application func')]
@@ -69,7 +73,8 @@
(with_template [<name> <tag>]
[(def .public (<name> type)
- (-> Type (List Type))
+ (-> Type
+ (List Type))
(when type
{<tag> left right}
(list.partial left (<name> right))
@@ -81,15 +86,16 @@
[flat_tuple .#Product]
)
-(`` (def .public (format type)
- (-> Type Text)
+(`` (def (format symbol_codec type)
+ (-> (Codec Text Symbol) Type
+ Text)
(when type
{.#Nominal name params}
(all text#composite
"(Nominal "
(text.enclosed' text.double_quote name)
(|> params
- (list#each (|>> format (text#composite " ")))
+ (list#each (|>> (format symbol_codec) (text#composite " ")))
(list#mix (function.flipped text#composite) ""))
")")
@@ -97,7 +103,7 @@
[{<tag> _}
(all text#composite <open>
(|> (<flat> type)
- (list#each format)
+ (list#each (format symbol_codec))
list.reversed
(list.interposed " ")
(list#mix text#composite ""))
@@ -110,11 +116,11 @@
(.let [[ins out] (flat_function type)]
(all text#composite "(-> "
(|> ins
- (list#each format)
+ (list#each (format symbol_codec))
list.reversed
(list.interposed " ")
(list#mix text#composite ""))
- " " (format out) ")"))
+ " " (format symbol_codec out) ")"))
{.#Parameter idx}
(n#encoded idx)
@@ -127,22 +133,33 @@
{.#Apply param fun}
(.let [[type_func type_args] (flat_application type)]
- (all text#composite "(" (format type_func) " " (|> type_args (list#each format) list.reversed (list.interposed " ") (list#mix text#composite "")) ")"))
+ (all text#composite "(" (format symbol_codec type_func) " " (|> type_args (list#each (format symbol_codec)) list.reversed (list.interposed " ") (list#mix text#composite "")) ")"))
(,, (with_template [<tag> <desc>]
[{<tag> env body}
- (all text#composite "(" <desc> " {" (|> env (list#each format) (text.interposed " ")) "} " (format body) ")")]
+ (all text#composite "(" <desc> " {" (|> env (list#each (format symbol_codec)) (text.interposed " ")) "} " (format symbol_codec body) ")")]
[.#UnivQ "All"]
[.#ExQ "Ex"]))
{.#Named name type}
- (symbol#encoded name)
+ (of symbol_codec encoded name)
)))
+(def .public absolute_format
+ (-> Type
+ Text)
+ (..format symbol.absolute))
+
+(def .public (relative_format module)
+ (-> Text Type
+ Text)
+ (..format (symbol.relative module)))
+
... https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reduction
(`` (def (reduced env type)
- (-> (List Type) Type Type)
+ (-> (List Type) Type
+ Type)
(when type
{.#Nominal name params}
{.#Nominal name (list#each (reduced env) params)}
@@ -175,7 +192,7 @@
(list#each (.function (_ [index type])
(all text#composite
(n#encoded index)
- " " (..format type))))
+ " " (..absolute_format type))))
(text.interposed (text#composite text.new_line " ")))))
(list.item idx env))
@@ -240,7 +257,8 @@
))))))
(`` (def .public (applied params func)
- (-> (List Type) Type (Maybe Type))
+ (-> (List Type) Type
+ (Maybe Type))
(when params
{.#End}
{.#Some func}
@@ -266,7 +284,8 @@
{.#None}))))
(`` (def .public (code type)
- (-> Type Code)
+ (-> Type
+ Code)
(when type
{.#Nominal name params}
(` {.#Nominal (, (code.text name))
@@ -303,7 +322,8 @@
)))
(def .public (de_aliased type)
- (-> Type Type)
+ (-> Type
+ Type)
(when type
{.#Named _ {.#Named name type'}}
(de_aliased {.#Named name type'})
@@ -312,7 +332,8 @@
type))
(def .public (anonymous type)
- (-> Type Type)
+ (-> Type
+ Type)
(when type
{.#Named name type'}
(anonymous type')
@@ -322,7 +343,8 @@
(with_template [<name> <base> <ctor>]
[(def .public (<name> types)
- (-> (List Type) Type)
+ (-> (List Type)
+ Type)
(when types
{.#End}
<base>
@@ -338,7 +360,8 @@
)
(def .public (function inputs output)
- (-> (List Type) Type Type)
+ (-> (List Type) Type
+ Type)
(when inputs
{.#End}
output
@@ -347,7 +370,8 @@
{.#Function input (function inputs' output)}))
(def .public (application params quant)
- (-> (List Type) Type Type)
+ (-> (List Type) Type
+ Type)
(when params
{.#End}
quant
@@ -357,7 +381,8 @@
(with_template [<name> <tag>]
[(def .public (<name> size body)
- (-> Nat Type Type)
+ (-> Nat Type
+ Type)
(when size
0 body
_ (|> body (<name> (-- size)) {<tag> (list)})))]
@@ -367,7 +392,8 @@
)
(`` (def .public (quantified? type)
- (-> Type Bit)
+ (-> Type
+ Bit)
(when type
{.#Named [module name] _type}
(quantified? _type)
@@ -388,7 +414,8 @@
false)))
(def .public (array depth element_type)
- (-> Nat Type Type)
+ (-> Nat Type
+ Type)
(when depth
0 element_type
_ (|> element_type
@@ -397,7 +424,8 @@
{.#Nominal array.nominal})))
(def .public (flat_array type)
- (-> Type [Nat Type])
+ (-> Type
+ [Nat Type])
(with_expansions [<default> [0 type]]
(when type
{.#Nominal name (list element_type)}
@@ -410,7 +438,8 @@
<default>)))
(def .public array?
- (-> Type Bit)
+ (-> Type
+ Bit)
(|>> ..flat_array
product.left
(n.> 0)))
@@ -432,16 +461,17 @@
(do meta.monad
[location meta.location
valueT (meta.type valueN)
- .let [_ (.log!# (all text#composite
- (symbol#encoded (symbol ..log!)) " " (location.format location) text.new_line
+ .let [[@ _ _] location
+ _ (.log!# (all text#composite
+ (of symbol.absolute encoded (symbol ..log!)) " " (location.format location) text.new_line
"Expression: " (when valueC
{.#Some valueC}
(code.format valueC)
{.#None}
- (symbol#encoded valueN))
+ (of symbol.absolute encoded valueN))
text.new_line
- " Type: " (..format valueT)))]]
+ " Type: " (..relative_format @ valueT)))]]
(in (list (code.symbol valueN))))
{.#Right valueC}
@@ -475,7 +505,8 @@
#expression Code]))
(def (typed lux)
- (-> Lux (Parser Typed))
+ (-> Lux
+ (Parser Typed))
(do <>.monad
[it <code>.any
type_check (<>.of_try (meta.result lux (expansion.complete it)))]
@@ -510,7 +541,8 @@
(.as .Nothing [])))))))))
(`` (def .public (replaced before after)
- (-> Type Type Type Type)
+ (-> Type Type Type
+ Type)
(.function (again it)
(if (of ..equivalence = before it)
after
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-29 01:37:29 +0000