aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--stdlib/source/experiment/compiler.lux15
-rw-r--r--stdlib/source/library/lux.lux8
-rw-r--r--stdlib/source/library/lux/tool/compiler.lux4
-rw-r--r--stdlib/source/library/lux/tool/compiler/default/platform.lux39
-rw-r--r--stdlib/source/library/lux/tool/compiler/language/lux/analysis/inference.lux43
-rw-r--r--stdlib/source/library/lux/tool/compiler/language/lux/analysis/type.lux18
-rw-r--r--stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/function.lux94
-rw-r--r--stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/lux.lux8
-rw-r--r--stdlib/source/library/lux/type.lux83
-rw-r--r--stdlib/source/library/lux/type/check.lux204
-rw-r--r--stdlib/source/test/lux/target/python.lux27
-rw-r--r--stdlib/source/test/lux/tool.lux4
-rw-r--r--stdlib/source/test/lux/tool/compiler/language/lux/analysis/inference.lux2
-rw-r--r--stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/complex.lux1
-rw-r--r--stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/function.lux360
15 files changed, 647 insertions, 263 deletions
diff --git a/stdlib/source/experiment/compiler.lux b/stdlib/source/experiment/compiler.lux
new file mode 100644
index 000000000..f17f6c499
--- /dev/null
+++ b/stdlib/source/experiment/compiler.lux
@@ -0,0 +1,15 @@
+(.using
+ [library
+ [lux "*"
+ [control
+ ["[0]" try]]
+ [tool
+ ["[0]" compiler {"+" Custom}]]]])
+
+(def: .public (dummy parameters)
+ (Custom Nat [] [])
+ {try.#Success
+ [0 (function (_ input)
+ [compiler.#dependencies (list)
+ compiler.#process (function (_ state archive)
+ {try.#Failure "YOLO"})])]})
diff --git a/stdlib/source/library/lux.lux b/stdlib/source/library/lux.lux
index e6a3e5e6f..7ddfa427f 100644
--- a/stdlib/source/library/lux.lux
+++ b/stdlib/source/library/lux.lux
@@ -5128,10 +5128,10 @@
(def: (recursive_type g!self g!dummy name body)
(-> Code Code Text Code Code)
- (` ((.All ((~ g!self) (~ g!dummy))
- (~ (let$ (local_symbol$ name) (` {.#Apply (..Primitive "") (~ g!self)})
- body)))
- (..Primitive ""))))
+ (` {.#Apply (..Primitive "")
+ (.All ((~ g!self) (~ g!dummy))
+ (~ (let$ (local_symbol$ name) (` {.#Apply (..Primitive "") (~ g!self)})
+ body)))}))
(macro: .public (Rec tokens)
(case tokens
diff --git a/stdlib/source/library/lux/tool/compiler.lux b/stdlib/source/library/lux/tool/compiler.lux
index 138f2ccf9..f2210209a 100644
--- a/stdlib/source/library/lux/tool/compiler.lux
+++ b/stdlib/source/library/lux/tool/compiler.lux
@@ -40,6 +40,10 @@
(type: .public (Compiler s d o)
(-> Input (Compilation s d o)))
+(type: .public Custom
+ (Ex (_ state document object)
+ (-> (List Text) (Try [state (Compiler state document object)]))))
+
(type: .public (Instancer s d o)
(-> (Key d) (List Parameter) (Compiler s d o)))
diff --git a/stdlib/source/library/lux/tool/compiler/default/platform.lux b/stdlib/source/library/lux/tool/compiler/default/platform.lux
index 42d8b9958..ef79450e9 100644
--- a/stdlib/source/library/lux/tool/compiler/default/platform.lux
+++ b/stdlib/source/library/lux/tool/compiler/default/platform.lux
@@ -1,9 +1,9 @@
(.using
[library
[lux "*"
- [type {"+" :sharing}]
["@" target]
["[0]" debug]
+ ["[0]" meta]
[abstract
["[0]" monad {"+" Monad do}]]
[control
@@ -27,6 +27,8 @@
["[0]" list ("[1]#[0]" monoid functor mix)]]
[format
["_" binary {"+" Writer}]]]
+ [type {"+" :sharing}
+ ["[0]" check]]
[world
["[0]" file {"+" Path}]
["[0]" console]]]]
@@ -49,7 +51,8 @@
[phase
["[0]" extension {"+" Extender}]]]]
[meta
- [cli {"+" Compilation Library}]
+ [cli {"+" Compilation Library}
+ ["[0]" compiler {"+" Compiler}]]
["[0]" archive {"+" Output Archive}
["[0]" registry {"+" Registry}]
["[0]" artifact]
@@ -716,6 +719,13 @@
[_ (ioW.freeze (value@ #&file_system platform) static archive)]
(async#in {try.#Failure error}))))))))
+ (exception: .public (invalid_custom_compiler [definition Symbol
+ type Type])
+ (exception.report
+ ["Definition" (%.symbol definition)]
+ ["Expected Type" (%.type ///.Custom)]
+ ["Actual Type" (%.type type)]))
+
(def: .public (compile phase_wrapper import static expander platform compilation context)
(All (_ <type_vars>)
(-> ///phase.Wrapper Import Static Expander <Platform> Compilation <Context> <Return>))
@@ -723,5 +733,28 @@
compiler (|> (..compiler phase_wrapper expander platform)
(serial_compiler import static platform sources)
(..parallel context))]
- (compiler descriptor.runtime module)))
+ (do [! ..monad]
+ [customs (|> compilers
+ (list#each (function (_ it)
+ (let [/#definition (value@ compiler.#definition it)
+ [/#module /#name] /#definition
+ /#parameters (value@ compiler.#parameters it)]
+ (do !
+ [[archive state] (compiler descriptor.runtime /#module)
+ .let [meta_state (value@ [extension.#state
+ ///directive.#analysis
+ ///directive.#state
+ extension.#state]
+ state)]
+ [_ /#type /#value] (|> /#definition
+ meta.export
+ (meta.result meta_state)
+ async#in)]
+ (async#in (if (check.subsumes? ///.Custom /#type)
+ (|> /#value
+ (:as ///.Custom)
+ (function.on /#parameters))
+ (exception.except ..invalid_custom_compiler [/#definition /#type])))))))
+ (monad.all !))]
+ (compiler descriptor.runtime module))))
)))
diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/analysis/inference.lux b/stdlib/source/library/lux/tool/compiler/language/lux/analysis/inference.lux
index 893f9df5a..1b693629a 100644
--- a/stdlib/source/library/lux/tool/compiler/language/lux/analysis/inference.lux
+++ b/stdlib/source/library/lux/tool/compiler/language/lux/analysis/inference.lux
@@ -7,6 +7,7 @@
[control
[pipe {"+" case>}]
["[0]" maybe]
+ ["[0]" try]
["[0]" exception {"+" exception:}]]
[data
["[0]" text
@@ -71,6 +72,38 @@
[id _] (/type.check check.existential)]
(in {.#Primitive (format ..prefix module "#" (%.nat id)) (list)})))
+(def: .public (quantified @var @parameter :it:)
+ (-> check.Var Nat Type Type)
+ (case :it:
+ {.#Primitive name co_variant}
+ {.#Primitive name (list#each (quantified @var @parameter) co_variant)}
+
+ (^template [<tag>]
+ [{<tag> left right}
+ {<tag> (quantified @var @parameter left)
+ (quantified @var @parameter right)}])
+ ([.#Sum]
+ [.#Product]
+ [.#Function]
+ [.#Apply])
+
+ {.#Var @}
+ (if (n.= @var @)
+ {.#Parameter @parameter}
+ :it:)
+
+ (^template [<tag>]
+ [{<tag> env body}
+ {<tag> (list#each (quantified @var @parameter) env)
+ (quantified @var (n.+ 2 @parameter) body)}])
+ ([.#UnivQ]
+ [.#ExQ])
+
+ (^or {.#Parameter @}
+ {.#Ex @}
+ {.#Named name anonymous})
+ :it:))
+
... Type-inference works by applying some (potentially quantified) type
... to a sequence of values.
... Function types are used for this, although inference is not always
@@ -93,13 +126,13 @@
{.#UnivQ _}
(do phase.monad
- [[var_id varT] (/type.check check.var)]
- (general archive analyse (maybe.trusted (type.applied (list varT) inferT)) args))
+ [[@var :var:] (/type.check check.var)]
+ (general archive analyse (maybe.trusted (type.applied (list :var:) inferT)) args))
{.#ExQ _}
- (do [! phase.monad]
- [exT ..existential]
- (general archive analyse (maybe.trusted (type.applied (list exT) inferT)) args))
+ (do phase.monad
+ [:ex: ..existential]
+ (general archive analyse (maybe.trusted (type.applied (list :ex:) inferT)) args))
{.#Apply inputT transT}
(case (type.applied (list inputT) transT)
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 7e06dc71a..c066115ec 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
@@ -43,10 +43,20 @@
[expectedT (extension.lifted meta.expected_type)]
(..check (check.check expectedT actualT))))
+(def: .public (with_var it)
+ (All (_ a) (-> (-> [check.Var Type] (Operation a))
+ (Operation a)))
+ (do phase.monad
+ [var (..check check.var)
+ .let [[@it :it:] var]
+ it (it var)
+ _ (..check (check.forget! @it))]
+ (in it)))
+
(def: .public (inferring action)
(All (_ a) (-> (Operation a) (Operation [Type a])))
(do phase.monad
- [[_ varT] (..check check.var)
- output (..expecting varT action)
- knownT (..check (check.clean varT))]
- (in [knownT output])))
+ [[@it :it:] (..check check.var)
+ it (..expecting :it: action)
+ :it: (..check (check.clean :it:))]
+ (in [:it: it])))
diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/function.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/function.lux
index 347604a35..b91550f39 100644
--- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/function.lux
+++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/function.lux
@@ -6,12 +6,16 @@
monad]
[control
["[0]" maybe]
- ["ex" exception {"+" exception:}]]
+ ["[0]" try]
+ ["[0]" exception {"+" exception:}]]
[data
["[0]" text
["%" format {"+" format}]]
[collection
["[0]" list ("[1]#[0]" monoid monad)]]]
+ [math
+ [number
+ ["n" nat]]]
["[0]" type
["[0]" check]]]]
["[0]" /// "_"
@@ -30,29 +34,44 @@
function Text
argument Text
body Code])
- (ex.report ["Type" (%.type expected)]
- ["Function" function]
- ["Argument" argument]
- ["Body" (%.code body)]))
+ (exception.report
+ ["Type" (%.type expected)]
+ ["Function" function]
+ ["Argument" argument]
+ ["Body" (%.code body)]))
-(exception: .public (cannot_apply [functionT Type
+(exception: .public (cannot_apply [:function: Type
functionC Code
arguments (List Code)])
- (ex.report ["Function type" (%.type functionT)]
- ["Function" (%.code functionC)]
- ["Arguments" (|> arguments
- list.enumeration
- (list#each (.function (_ [idx argC])
- (format (%.nat idx) " " (%.code argC))))
- (text.interposed text.new_line))]))
+ (exception.report
+ ["Function type" (%.type :function:)]
+ ["Function" (%.code functionC)]
+ ["Arguments" (|> arguments
+ list.enumeration
+ (list#each (.function (_ [idx argC])
+ (format (%.nat idx) " " (%.code argC))))
+ (text.interposed text.new_line))]))
(def: .public (function analyse function_name arg_name archive body)
(-> Phase Text Text Phase)
(do [! ///.monad]
- [functionT (///extension.lifted meta.expected_type)]
- (loop [expectedT functionT]
+ [:function: (///extension.lifted meta.expected_type)]
+ (loop [expectedT :function:]
(/.with_exception ..cannot_analyse [expectedT function_name arg_name body]
(case expectedT
+ {.#Function :input: :output:}
+ (<| (# ! each (.function (_ [scope bodyA])
+ {/.#Function (list#each (|>> /.variable)
+ (/scope.environment scope))
+ bodyA}))
+ /scope.with
+ ... Functions have access not only to their argument, but
+ ... also to themselves, through a local variable.
+ (/scope.with_local [function_name expectedT])
+ (/scope.with_local [arg_name :input:])
+ (/type.expecting :output:)
+ (analyse archive body))
+
{.#Named name unnamedT}
(again unnamedT)
@@ -62,7 +81,7 @@
(again value)
{.#None}
- (/.failure (ex.error cannot_analyse [expectedT function_name arg_name body])))
+ (/.failure (exception.error ..cannot_analyse [expectedT function_name arg_name body])))
(^template [<tag> <instancer>]
[{<tag> _}
@@ -82,33 +101,34 @@
... Inference
_
(do !
- [[input_id inputT] (/type.check check.var)
- [output_id outputT] (/type.check check.var)
- .let [functionT {.#Function inputT outputT}]
- functionA (again functionT)
- _ (/type.check (check.check expectedT functionT))]
+ [[@input :input:] (/type.check check.var)
+ [@output :output:] (/type.check check.var)
+ .let [:function: {.#Function :input: :output:}]
+ functionA (again :function:)
+ specialization (/type.check (check.try (check.identity (list @output) @input)))
+ :function: (case specialization
+ {try.#Success :input:'}
+ (in :function:)
+
+ {try.#Failure _}
+ (/type.check
+ (do [! check.monad]
+ [? (check.linked? @input @output)]
+ (# ! each
+ (|>> {.#Function :input:} (/inference.quantified @input 1) {.#UnivQ (list)})
+ (if ?
+ (in :input:)
+ (check.identity (list @input) @output))))))
+ _ (/type.check (check.check expectedT :function:))]
(in functionA))))
- {.#Function inputT outputT}
- (<| (# ! each (.function (_ [scope bodyA])
- {/.#Function (list#each (|>> /.variable)
- (/scope.environment scope))
- bodyA}))
- /scope.with
- ... Functions have access not only to their argument, but
- ... also to themselves, through a local variable.
- (/scope.with_local [function_name expectedT])
- (/scope.with_local [arg_name inputT])
- (/type.expecting outputT)
- (analyse archive body))
-
_
(/.failure "")
)))))
-(def: .public (apply analyse argsC+ functionT functionA archive functionC)
+(def: .public (apply analyse argsC+ :function: functionA archive functionC)
(-> Phase (List Code) Type Analysis Phase)
- (<| (/.with_exception ..cannot_apply [functionT functionC argsC+])
+ (<| (/.with_exception ..cannot_apply [:function: functionC argsC+])
(do ///.monad
- [[applyT argsA+] (/inference.general archive analyse functionT argsC+)])
+ [[applyT argsA+] (/inference.general archive analyse :function: argsC+)])
(in (/.reified [functionA argsA+]))))
diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/lux.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/lux.lux
index 4632aa193..d747ff070 100644
--- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/lux.lux
+++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/lux.lux
@@ -124,10 +124,10 @@
(def: lux::is
Handler
(function (_ extension_name analyse archive args)
- (do ////.monad
- [[var_id varT] (typeA.check check.var)]
- ((binary varT varT Bit extension_name)
- analyse archive args))))
+ (<| typeA.with_var
+ (function (_ [@var :var:]))
+ ((binary :var: :var: Bit extension_name)
+ analyse archive args))))
... "lux try" provides a simple way to interact with the host platform's
... error_handling facilities.
diff --git a/stdlib/source/library/lux/type.lux b/stdlib/source/library/lux/type.lux
index 380331c40..ac81fe26b 100644
--- a/stdlib/source/library/lux/type.lux
+++ b/stdlib/source/library/lux/type.lux
@@ -1,31 +1,31 @@
(.using
- [library
- [lux {"-" function :as}
- ["@" target]
- [abstract
- [equivalence {"+" Equivalence}]
- [monad {"+" Monad do}]]
- [control
- ["[0]" function]
- ["[0]" maybe]
- ["[0]" exception {"+" exception:}]
- ["<>" parser
- ["<[0]>" code {"+" Parser}]]]
- [data
- ["[0]" product]
- ["[0]" text ("[1]#[0]" monoid equivalence)]
- [collection
- ["[0]" array]
- ["[0]" list ("[1]#[0]" functor monoid mix)]]]
- ["[0]" macro
- [syntax {"+" syntax:}]
- ["[0]" code]]
- [math
- [number
- ["n" nat ("[1]#[0]" decimal)]]]
- ["[0]" meta
- ["[0]" location]
- ["[0]" symbol ("[1]#[0]" equivalence codec)]]]])
+ [library
+ [lux {"-" function :as}
+ ["@" target]
+ [abstract
+ [equivalence {"+" Equivalence}]
+ [monad {"+" Monad do}]]
+ [control
+ ["[0]" function]
+ ["[0]" maybe]
+ ["[0]" exception {"+" exception:}]
+ ["<>" parser
+ ["<[0]>" code {"+" Parser}]]]
+ [data
+ ["[0]" product]
+ ["[0]" text ("[1]#[0]" monoid equivalence)]
+ [collection
+ ["[0]" array]
+ ["[0]" list ("[1]#[0]" functor monoid mix)]]]
+ ["[0]" macro
+ [syntax {"+" syntax:}]
+ ["[0]" code]]
+ [math
+ [number
+ ["n" nat ("[1]#[0]" decimal)]]]
+ ["[0]" meta
+ ["[0]" location]
+ ["[0]" symbol ("[1]#[0]" equivalence codec)]]]])
(template [<name> <tag>]
[(def: .public (<name> type)
@@ -466,3 +466,32 @@
(~ extraction)
... The value of this expression will never be relevant, so it doesn't matter what it is.
(.:as .Nothing [])))))))
+
+(def: .public (replaced before after)
+ (-> Type Type Type Type)
+ (.function (again it)
+ (if (# ..equivalence = before it)
+ after
+ (case it
+ {.#Primitive name co_variant}
+ {.#Primitive name (list#each again co_variant)}
+
+ (^template [<tag>]
+ [{<tag> left right}
+ {<tag> (again left) (again right)}])
+ ([.#Sum]
+ [.#Product]
+ [.#Function]
+ [.#Apply])
+
+ (^template [<tag>]
+ [{<tag> env body}
+ {<tag> (list#each again env) (again body)}])
+ ([.#UnivQ]
+ [.#ExQ])
+
+ (^or {.#Parameter _}
+ {.#Var _}
+ {.#Ex _}
+ {.#Named _})
+ it))))
diff --git a/stdlib/source/library/lux/type/check.lux b/stdlib/source/library/lux/type/check.lux
index 90e94478b..31ec9da05 100644
--- a/stdlib/source/library/lux/type/check.lux
+++ b/stdlib/source/library/lux/type/check.lux
@@ -1,25 +1,25 @@
(.using
- [library
- [lux "*"
- ["@" target]
- [abstract
- [functor {"+" Functor}]
- [apply {"+" Apply}]
- ["[0]" monad {"+" Monad do}]]
- [control
- ["[0]" maybe]
- ["[0]" try {"+" Try}]
- ["[0]" exception {"+" Exception exception:}]]
- [data
- ["[0]" product]
- ["[0]" text ("[1]#[0]" monoid equivalence)]
- [collection
- ["[0]" list]
- ["[0]" set {"+" Set}]]]
- [math
- [number
- ["n" nat ("[1]#[0]" decimal)]]]]]
- ["[0]" // ("[1]#[0]" equivalence)])
+ [library
+ [lux {"-" try}
+ ["@" target]
+ [abstract
+ [functor {"+" Functor}]
+ [apply {"+" Apply}]
+ ["[0]" monad {"+" Monad do}]]
+ [control
+ ["[0]" maybe]
+ ["[0]" try {"+" Try}]
+ ["[0]" exception {"+" Exception exception:}]]
+ [data
+ ["[0]" product]
+ ["[0]" text ("[1]#[0]" monoid equivalence)]
+ [collection
+ ["[0]" list ("[1]#[0]" mix)]
+ ["[0]" set {"+" Set}]]]
+ [math
+ [number
+ ["n" nat ("[1]#[0]" decimal)]]]]]
+ ["[0]" // ("[1]#[0]" equivalence)])
(template: (!n#= reference subject)
[("lux i64 =" reference subject)])
@@ -249,17 +249,21 @@
_
(exception.except ..unknown_type_var id))))
-(def: (re_bind type id)
- (-> Type Var (Check Any))
+(def: (re_bind' ?type id)
+ (-> (Maybe Type) Var (Check Any))
(function (_ context)
(case (|> context (value@ .#var_bindings) (var::get id))
{.#Some _}
- {try.#Success [(revised@ .#var_bindings (var::put id {.#Some type}) context)
+ {try.#Success [(revised@ .#var_bindings (var::put id ?type) context)
[]]}
_
(exception.except ..unknown_type_var id))))
+(def: (re_bind type id)
+ (-> Type Var (Check Any))
+ (re_bind' {.#Some type} id))
+
(def: .public var
(Check [Var Type])
(function (_ context)
@@ -298,26 +302,21 @@
(type: Ring
(Set Var))
-(def: empty_ring
- Ring
- (set.empty n.hash))
-
-... TODO: Optimize this by not using sets anymore.
-(def: (ring start)
- (-> Var (Check Ring))
+(def: (ring' start)
+ (-> Var (Check (List Var)))
(function (_ context)
(loop [current start
- output (set.has start empty_ring)]
+ output (list start)]
(case (|> context (value@ .#var_bindings) (var::get current))
{.#Some {.#Some type}}
(case type
- {.#Var post}
- (if (!n#= start post)
+ {.#Var next}
+ (if (!n#= start next)
{try.#Success [context output]}
- (again post (set.has post output)))
+ (again next (list& next output)))
_
- {try.#Success [context empty_ring]})
+ {try.#Success [context (list)]})
{.#Some {.#None}}
{try.#Success [context output]}
@@ -325,22 +324,114 @@
{.#None}
(exception.except ..unknown_type_var current)))))
+... TODO: Optimize this by not using sets anymore.
+(def: ring
+ (-> Var (Check Ring))
+ (|>> ..ring'
+ (check#each (set.of_list n.hash))))
+
+(def: .public (linked? @0 @1)
+ (-> Var Var (Check Bit))
+ (check#each (function (_ it)
+ (set.member? it @1))
+ (..ring @0)))
+
+(exception: (invalid_alias [var Var
+ expected (List Var)
+ actual (List Var)])
+ (exception.report
+ ["Var" (n#encoded var)]
+ ["Expected" (exception.listing n#encoded expected)]
+ ["Actual" (exception.listing n#encoded actual)]))
+
+(exception: (cannot_identify [var Var])
+ (exception.report
+ ["Var" (n#encoded var)]))
+
+(def: .public (identity aliases @)
+ (-> (List Var) Var (Check Type))
+ (do [! ..monad]
+ [:bound: (..peek @)]
+ (case :bound:
+ {.#Some :bound:}
+ (in :bound:)
+
+ {.#None}
+ (do !
+ [existing_aliases (..ring @)
+ _ (if (list.every? (set.member? existing_aliases) aliases)
+ (in [])
+ (..except ..invalid_alias [@ aliases (set.list existing_aliases)]))
+ .let [forbidden_aliases (set.of_list n.hash (list& @ aliases))
+ allowed_aliases (set.difference forbidden_aliases existing_aliases)]]
+ (case (set.list allowed_aliases)
+ {.#Item identity _}
+ (in {.#Var identity})
+
+ {.#None}
+ (..except ..cannot_identify [@]))))))
+
+(def: (erase! @)
+ (-> Var (Check Any))
+ (function (_ context)
+ {try.#Success [(revised@ .#var_bindings
+ (list#mix (: (:let [binding [Nat (Maybe Type)]]
+ (-> binding
+ (List binding)
+ (List binding)))
+ (function (_ in out)
+ (let [[@var :var:] in]
+ (if (n.= @ @var)
+ out
+ (list& in out)))))
+ (: (List [Nat (Maybe Type)])
+ (list)))
+ context)
+ []]}))
+
+(def: .public (forget! @)
+ (-> Var (Check Any))
+ (do [! ..monad]
+ [ring (..ring' @)]
+ (case ring
+ (^ (list))
+ (in [])
+
+ (^ (list @me))
+ (erase! @me)
+
+ (^ (list @other @me))
+ (do !
+ [_ (re_bind' {.#None} @other)]
+ (erase! @me))
+
+ (^ (list& @prev _))
+ (case (list.reversed ring)
+ (^ (list& @me @next _))
+ (do !
+ [_ (re_bind {.#Var @next} @prev)
+ _ (re_bind {.#Var @prev} @next)]
+ (erase! @me))
+
+ _
+ (undefined)))))
+
+(def: .public (try it)
+ (All (_ a) (-> (Check a) (Check (Try a))))
+ (function (_ context)
+ (case (it context)
+ {try.#Success [context' output]}
+ {try.#Success [context' {try.#Success output}]}
+
+ {try.#Failure error}
+ {try.#Success [context {try.#Failure error}]})))
+
(def: .public fresh_context
Type_Context
[.#var_counter 0
.#ex_counter 0
.#var_bindings (list)])
-(def: (attempt op)
- (All (_ a) (-> (Check a) (Check (Maybe a))))
- (function (_ context)
- (case (op context)
- {try.#Success [context' output]}
- {try.#Success [context' {.#Some output}]}
-
- {try.#Failure _}
- {try.#Success [context {.#None}]})))
-
(def: (either left right)
(All (_ a) (-> (Check a) (Check a) (Check a)))
(function (_ context)
@@ -396,17 +487,17 @@
(if (!n#= idE idA)
(check#in assumptions)
(do [! ..monad]
- [ebound (attempt (..bound idE))
- abound (attempt (..bound idA))]
+ [ebound (..try (..bound idE))
+ abound (..try (..bound idA))]
(case [ebound abound]
... Link the 2 variables circularly
- [{.#None} {.#None}]
+ [{try.#Failure _} {try.#Failure _}]
(do !
[_ (link/2 idE idA)]
(in assumptions))
... Interpose new variable between 2 existing links
- [{.#Some etype} {.#None}]
+ [{try.#Success etype} {try.#Failure _}]
(case etype
{.#Var targetE}
(do !
@@ -417,7 +508,7 @@
(check' assumptions etype {.#Var idA}))
... Interpose new variable between 2 existing links
- [{.#None} {.#Some atype}]
+ [{try.#Failure _} {try.#Success atype}]
(case atype
{.#Var targetA}
(do !
@@ -427,7 +518,7 @@
_
(check' assumptions {.#Var idE} atype))
- [{.#Some etype} {.#Some atype}]
+ [{try.#Success etype} {try.#Success atype}]
(case [etype atype]
[{.#Var targetE} {.#Var targetA}]
(do !
@@ -702,9 +793,9 @@
(check#each (|>> {<tag> leftT'}))))])
([.#Sum] [.#Product] [.#Function] [.#Apply])
- {.#Var id}
+ {.#Var @}
(do ..monad
- [?actualT (peek id)]
+ [?actualT (peek @)]
(case ?actualT
{.#Some actualT}
(clean actualT)
@@ -715,7 +806,8 @@
(^template [<tag>]
[{<tag> envT+ unquantifiedT}
(do [! ..monad]
- [envT+' (monad.each ! clean envT+)]
- (in {<tag> envT+' unquantifiedT}))])
+ [envT+' (monad.each ! clean envT+)
+ unquantifiedT' (clean unquantifiedT)]
+ (in {<tag> envT+' unquantifiedT'}))])
([.#UnivQ] [.#ExQ])
))
diff --git a/stdlib/source/test/lux/target/python.lux b/stdlib/source/test/lux/target/python.lux
index 39c51b2a7..6eed5ecab 100644
--- a/stdlib/source/test/lux/target/python.lux
+++ b/stdlib/source/test/lux/target/python.lux
@@ -324,6 +324,31 @@
(list (/.float float/0) (/.float float/1) (/.float float/2)))))
)))
+(def: test|var
+ Test
+ (do [! random.monad]
+ [expected/0 random.safe_frac
+ expected/1 random.safe_frac
+ choice (# ! each (n.% 2) random.nat)
+ .let [expected/? (case choice
+ 0 expected/0
+ _ expected/1)]
+ $var (# ! each (|>> %.nat (format "v") /.var) random.nat)
+ $choice (# ! each (|>> %.nat (format "c") /.var) random.nat)]
+ ($_ _.and
+ (_.cover [/.Single /.SVar /.var]
+ (expression (|>> (:as Frac) (f.= expected/0))
+ (/.apply/* (/.lambda (list $var) $var)
+ (list (/.float expected/0)))))
+ (_.cover [/.Poly /.PVar /.poly]
+ (expression (|>> (:as Frac) (f.= expected/?))
+ (/.apply/* (/.lambda (list $choice (/.poly $var))
+ (/.item $choice $var))
+ (list (/.int (.int choice))
+ (/.float expected/0)
+ (/.float expected/1)))))
+ )))
+
(def: test|expression
Test
(do [! random.monad]
@@ -335,6 +360,8 @@
(_.for [/.Computation]
..test|computation)
..test|function
+ (_.for [/.Var]
+ ..test|var)
))))
(def: .public test
diff --git a/stdlib/source/test/lux/tool.lux b/stdlib/source/test/lux/tool.lux
index 0f42f81db..c9a5cfb7c 100644
--- a/stdlib/source/test/lux/tool.lux
+++ b/stdlib/source/test/lux/tool.lux
@@ -17,7 +17,8 @@
["[1]/[0]" analysis "_"
["[1]/[0]" simple]
["[1]/[0]" complex]
- ["[1]/[0]" reference]]
+ ["[1]/[0]" reference]
+ ["[1]/[0]" function]]
... ["[1]/[0]" synthesis]
]]]
["[1][0]" meta "_"
@@ -41,6 +42,7 @@
/phase/analysis/simple.test
/phase/analysis/complex.test
/phase/analysis/reference.test
+ /phase/analysis/function.test
... /syntax.test
... /synthesis.test
))
diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/analysis/inference.lux b/stdlib/source/test/lux/tool/compiler/language/lux/analysis/inference.lux
index fa3df9c67..97bdb7a54 100644
--- a/stdlib/source/test/lux/tool/compiler/language/lux/analysis/inference.lux
+++ b/stdlib/source/test/lux/tool/compiler/language/lux/analysis/inference.lux
@@ -78,7 +78,7 @@
{try.#Failure error}
(text.contains? (value@ exception.#label exception) error)))
-(def: simple_parameter
+(def: .public simple_parameter
(Random [Type Code])
(`` ($_ random.either
(~~ (template [<type> <random> <code>]
diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/complex.lux b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/complex.lux
index f559e98c4..ed111c5e4 100644
--- a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/complex.lux
+++ b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/complex.lux
@@ -230,7 +230,6 @@
(list.item tag)
(maybe.else ""))]]
($_ _.and
- ..test|sum
(_.cover [/.variant]
(let [expected_variant? (: (-> Symbol Bit)
(function (_ tag)
diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/function.lux b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/function.lux
index 815b488fe..50fbc1c50 100644
--- a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/function.lux
+++ b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/function.lux
@@ -1,133 +1,253 @@
(.using
+ [library
[lux "*"
- [abstract
- ["[0]" monad {"+" do}]]
- [data
- ["%" text/format {"+" format}]]
- ["r" math/random {"+" Random}]
["_" test {"+" Test}]
+ [abstract
+ [monad {"+" do}]]
[control
- pipe
- ["[0]" maybe]
- ["[0]" try]]
+ [pipe {"+" case>}]
+ ["[0]" function]
+ ["[0]" try ("[1]#[0]" functor)]
+ ["[0]" exception]]
[data
["[0]" product]
- ["[0]" text ("[1]#[0]" equivalence)]
- [number
- ["n" nat]]
+ ["[0]" text
+ ["%" format]]
[collection
- ["[0]" list ("[1]#[0]" functor)]]]
- ["[0]" type]
- ["[0]" macro
+ ["[0]" list]]]
+ [macro
["[0]" code]]
+ [math
+ ["[0]" random]
+ [number
+ ["n" nat]]]
[meta
- ["[0]" symbol]]]
- [//
- ["_[0]" primitive]
- ["_[0]" structure]]
- [\\
- ["[0]" /
- ["/[1]" //
- ["[1][0]" module]
- ["[1][0]" type]
- ["/[1]" // "_"
- ["/[1]" //
- ["[1][0]" analysis {"+" Analysis Operation}]
- [///
- ["[1][0]" reference]
- ["[0]" phase]
- [meta
- ["[0]" archive]]]]]]]])
-
-(def: (check_apply expectedT num_args analysis)
- (-> Type Nat (Operation Analysis) Bit)
- (|> analysis
- (//type.with_type expectedT)
- (phase.result _primitive.state)
- (case> {try.#Success applyA}
- (let [[funcA argsA] (////analysis.application applyA)]
- (n.= num_args (list.size argsA)))
-
- {try.#Failure _}
- false)))
-
-(def: abstraction
- (do r.monad
- [func_name (r.unicode 5)
- arg_name (|> (r.unicode 5) (r.only (|>> (text#= func_name) not)))
- [outputT outputC] _primitive.primitive
- [inputT _] _primitive.primitive
- .let [g!arg (code.local_symbol arg_name)]]
- (<| (_.context (%.symbol (symbol /.function)))
- ($_ _.and
- (_.test "Can analyse function."
- (and (|> (//type.with_type (All (_ a) (-> a outputT))
- (/.function _primitive.phase func_name arg_name archive.empty outputC))
- _structure.check_succeeds)
- (|> (//type.with_type (All (_ a) (-> a a))
- (/.function _primitive.phase func_name arg_name archive.empty g!arg))
- _structure.check_succeeds)))
- (_.test "Generic functions can always be specialized."
- (and (|> (//type.with_type (-> inputT outputT)
- (/.function _primitive.phase func_name arg_name archive.empty outputC))
- _structure.check_succeeds)
- (|> (//type.with_type (-> inputT inputT)
- (/.function _primitive.phase func_name arg_name archive.empty g!arg))
- _structure.check_succeeds)))
- (_.test "The function's name is bound to the function's type."
- (|> (//type.with_type (Rec self (-> inputT self))
- (/.function _primitive.phase func_name arg_name archive.empty (code.local_symbol func_name)))
- _structure.check_succeeds))
- ))))
+ ["[0]" symbol "_"
+ ["$[1]" \\test]]]
+ ["[0]" type ("[1]#[0]" equivalence)
+ ["$[1]" \\test]
+ ["[0]" check]]]]
+ [\\library
+ ["[0]" /
+ ["/[1]" //
+ [//
+ ["[1][0]" extension
+ ["[1]/[0]" analysis "_"
+ ["[1]" lux]]]
+ [//
+ ["[1][0]" analysis {"+" Analysis}
+ [evaluation {"+" Eval}]
+ ["[2][0]" macro]
+ ["[2][0]" scope]
+ ["[2][0]" module]
+ ["[2][0]" type
+ ["$[1]" \\test]]
+ ["[2][0]" inference "_"
+ ["$[1]" \\test]]]
+ [///
+ ["[1][0]" phase ("[1]#[0]" monad)]
+ [meta
+ ["[0]" archive]]]]]]]])
-(def: apply
- (do [! r.monad]
- [full_args (|> r.nat (# ! each (|>> (n.% 10) (n.max 2))))
- partial_args (|> r.nat (# ! each (n.% full_args)))
- var_idx (|> r.nat (# ! each (|>> (n.% full_args) (n.max 1))))
- inputsTC (r.list full_args _primitive.primitive)
- .let [inputsT (list#each product.left inputsTC)
- inputsC (list#each product.right inputsTC)]
- [outputT outputC] _primitive.primitive
- .let [funcT (type.function inputsT outputT)
- partialT (type.function (list.after partial_args inputsT) outputT)
- varT {.#Parameter 1}
- polyT (<| (type.univ_q 1)
- (type.function (list.together (list (list.first var_idx inputsT)
- (list varT)
- (list.after (++ var_idx) inputsT))))
- varT)
- poly_inputT (maybe.trusted (list.item var_idx inputsT))
- partial_poly_inputsT (list.after (++ var_idx) inputsT)
- partial_polyT1 (<| (type.function partial_poly_inputsT)
- poly_inputT)
- partial_polyT2 (<| (type.univ_q 1)
- (type.function {.#Item varT partial_poly_inputsT})
- varT)
- dummy_function {////analysis.#Function (list) {////analysis.#Reference (////reference.local 1)}}]]
- (<| (_.context (%.symbol (symbol /.apply)))
- ($_ _.and
- (_.test "Can analyse monomorphic type application."
- (|> (/.apply _primitive.phase inputsC funcT dummy_function archive.empty (' []))
- (check_apply outputT full_args)))
- (_.test "Can partially apply functions."
- (|> (/.apply _primitive.phase (list.first partial_args inputsC) funcT dummy_function archive.empty (' []))
- (check_apply partialT partial_args)))
- (_.test "Can apply polymorphic functions."
- (|> (/.apply _primitive.phase inputsC polyT dummy_function archive.empty (' []))
- (check_apply poly_inputT full_args)))
- (_.test "Polymorphic partial application propagates found type-vars."
- (|> (/.apply _primitive.phase (list.first (++ var_idx) inputsC) polyT dummy_function archive.empty (' []))
- (check_apply partial_polyT1 (++ var_idx))))
- (_.test "Polymorphic partial application preserves quantification for type-vars."
- (|> (/.apply _primitive.phase (list.first var_idx inputsC) polyT dummy_function archive.empty (' []))
- (check_apply partial_polyT2 var_idx)))
- ))))
+(def: (eval archive type term)
+ Eval
+ (//phase#in []))
+
+(def: (expander macro inputs state)
+ //macro.Expander
+ {try.#Success ((.macro macro) inputs state)})
+
+(def: analysis
+ //analysis.Phase
+ (//.phase ..expander))
+
+(def: test|function
+ Test
+ (do [! random.monad]
+ [lux $//type.random_state
+ .let [state [//extension.#bundle (//extension/analysis.bundle ..eval)
+ //extension.#state lux]]
+ input/0 ($type.random 0)
+ input/1 ($type.random 0)
+ function/0 (random.ascii/lower 1)
+ function/1 (random.ascii/lower 2)
+ argument/0 (random.ascii/lower 3)
+ argument/1 (random.ascii/lower 4)
+ module/0 (random.ascii/lower 5)
+ [output/0 term/0] $//inference.simple_parameter
+ [output/1 term/1] (random.only (|>> product.left (same? output/0) not)
+ $//inference.simple_parameter)
+ name/0 ($symbol.random 1 1)
+ .let [$function/0 (code.local_symbol function/0)
+ $function/1 (code.local_symbol function/1)
+ $argument/0 (code.local_symbol argument/0)
+ $argument/1 (code.local_symbol argument/1)]]
+ ($_ _.and
+ (_.cover [/.function]
+ (let [function?' (: (-> Type Code (-> [(List Analysis) Analysis] Bit) Bit)
+ (function (_ function_type output_term ?)
+ (|> (do //phase.monad
+ [analysis (|> (/.function ..analysis function/0 argument/0 archive.empty
+ output_term)
+ (//type.expecting function_type))]
+ (in (case analysis
+ {//analysis.#Function it}
+ (? it)
+
+ _
+ false)))
+ (//module.with 0 module/0)
+ (//phase#each product.right)
+ (//phase.result state)
+ (try.else false))))
+ function? (: (-> Type Code Bit)
+ (function (_ function_type output_term)
+ (function?' function_type output_term (function.constant true))))
+ inferring? (: (-> Type Code Bit)
+ (function (_ :expected: term)
+ (|> (do //phase.monad
+ [[:actual: analysis] (|> (/.function ..analysis function/0 argument/0 archive.empty
+ term)
+ //type.inferring)]
+ (in (case analysis
+ {//analysis.#Function [actual_env actual_body]}
+ (type#= :expected: :actual:)
+
+ _
+ false)))
+ (//module.with 0 module/0)
+ (//phase#each product.right)
+ (//phase.result state)
+ (try.else false))))]
+ (and (function? (-> input/0 output/0) term/0)
+ (function? (-> input/0 input/0) $argument/0)
+
+ (function? {.#Named name/0 (-> input/0 output/0)} term/0)
+
+ (function? (All (_ a) (-> a a)) $argument/0)
+ (function? (Ex (_ a) (-> a a)) $argument/0)
+ (function? (Ex (_ a) (-> input/0 a)) term/0)
+ (function? (Ex (_ a) (-> a a)) term/0)
+ (function? (Rec self (-> input/0 self)) $function/0)
+
+ (function? (type ((All (_ a) (-> a a)) output/0)) term/0)
+ (not (function? (type ((All (_ a) (-> a a)) output/1)) term/0))
+
+ (function? (type ((Ex (_ a) (-> a a)) output/0)) term/0)
+ (not (function? (type ((Ex (_ a) (-> a a)) output/1)) term/0))
+
+ (function?' (-> input/0 input/1 input/0) (` ([(~ $function/1) (~ $argument/1)] (~ $argument/0)))
+ (function (_ [outer body])
+ (and (list.empty? outer)
+ (case body
+ {//analysis.#Function [inner body]}
+ (n.= 1 (list.size inner))
+
+ _
+ false))))
+ (function?' (-> input/0 input/1 input/1) (` ([(~ $function/1) (~ $argument/1)] (~ $argument/1)))
+ (function (_ [outer body])
+ (and (list.empty? outer)
+ (case body
+ {//analysis.#Function [inner body]}
+ (n.= 0 (list.size inner))
+
+ _
+ false))))
+
+ (|> (do //phase.monad
+ [[@var :var:] (//type.check check.var)
+ _ (//type.check (check.check :var: (-> input/0 output/0)))
+ analysis (|> (/.function ..analysis function/0 argument/0 archive.empty
+ term/0)
+ (//type.expecting :var:))]
+ (in (case analysis
+ {//analysis.#Function [actual_env actual_body]}
+ true
+
+ _
+ false)))
+ (//module.with 0 module/0)
+ (//phase#each product.right)
+ (//phase.result state)
+ (try.else false))
+
+ (inferring? (All (_ a) (-> a output/0)) term/0)
+ (inferring? (All (_ a) (-> a a)) $argument/0)
+ (inferring? (All (_ @0) (-> @0 @0 (And .Bit @0)))
+ (` ([(~ $function/1) (~ $argument/1)]
+ [("lux is" (~ $argument/0) (~ $argument/1))
+ (~ $argument/1)]))))))
+ (_.cover [/.cannot_analyse]
+ (|> (do //phase.monad
+ [analysis (|> (/.function ..analysis function/0 argument/0 archive.empty
+ term/1)
+ (//type.expecting (-> input/0 output/0)))]
+ (in (case analysis
+ {//analysis.#Function [actual_env actual_body]}
+ true
+
+ _
+ false)))
+ (//module.with 0 module/0)
+ (//phase#each product.right)
+ (//phase.result state)
+ (exception.otherwise (text.contains? (value@ exception.#label /.cannot_analyse)))))
+ )))
(def: .public test
Test
- (<| (_.context (symbol.module (symbol /._)))
- ($_ _.and
- ..abstraction
- ..apply
- )))
+ (<| (_.covering /._)
+ (do [! random.monad]
+ [lux $//type.random_state
+ .let [state [//extension.#bundle (//extension/analysis.bundle ..eval)
+ //extension.#state lux]]
+ [input/0 term/0] $//inference.simple_parameter
+ [input/1 term/1] $//inference.simple_parameter
+ output/0 ($type.random 0)
+ module/0 (random.ascii/lower 1)]
+ ($_ _.and
+ ..test|function
+ (_.cover [/.apply]
+ (let [reification? (: (-> Type (List Code) Type Bit)
+ (function (_ :abstraction: terms :expected:)
+ (|> (do //phase.monad
+ [[:actual: analysis] (|> (/.apply ..analysis terms
+ :abstraction:
+ (//analysis.unit)
+ archive.empty
+ (' []))
+ //type.inferring)]
+ (in (and (check.subsumes? :expected: :actual:)
+ (case analysis
+ {//analysis.#Apply _}
+ true
+
+ _
+ false))))
+ (//module.with 0 module/0)
+ (//phase#each product.right)
+ (//phase.result state)
+ (try.else false))))]
+ (and (reification? (-> input/0 input/1 output/0) (list term/0 term/1) output/0)
+ (reification? (-> input/0 input/1 output/0) (list term/0) (-> input/1 output/0))
+ (reification? (All (_ a) (-> a a)) (list term/0) input/0)
+ (reification? (All (_ a) (-> a a a)) (list term/0) (-> input/0 input/0))
+ (reification? (All (_ a) (-> input/0 a)) (list term/0) .Nothing)
+ (reification? (All (_ a b) (-> a b a)) (list term/0) (All (_ b) (-> b input/0)))
+ (reification? (Ex (_ a) (-> a input/0)) (list (` ("lux io error" ""))) input/0)
+ (reification? (Ex (_ a) (-> input/0 a)) (list term/0) .Any))))
+ (_.cover [/.cannot_apply]
+ (|> (do //phase.monad
+ [_ (|> (/.apply ..analysis (list term/1 term/0)
+ (-> input/0 input/1 output/0)
+ (//analysis.unit)
+ archive.empty
+ (' []))
+ (//type.expecting output/0))]
+ (in false))
+ (//module.with 0 module/0)
+ (//phase#each product.right)
+ (//phase.result state)
+ (exception.otherwise (text.contains? (value@ exception.#label /.cannot_apply)))))
+ ))))