diff options
Diffstat (limited to '')
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))))) + )))) |