From 469b171e5793422a4dbd27f4f2fab8a261c9ccf9 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Thu, 10 Feb 2022 03:34:29 -0400 Subject: Finishing the meta-compiler [Part 2] --- stdlib/source/library/lux.lux | 8 +- stdlib/source/library/lux/tool/compiler.lux | 4 + .../library/lux/tool/compiler/default/platform.lux | 39 +++- .../compiler/language/lux/analysis/inference.lux | 43 ++++- .../tool/compiler/language/lux/analysis/type.lux | 18 +- .../language/lux/phase/analysis/function.lux | 94 ++++++---- .../language/lux/phase/extension/analysis/lux.lux | 8 +- stdlib/source/library/lux/type.lux | 83 ++++++--- stdlib/source/library/lux/type/check.lux | 204 +++++++++++++++------ 9 files changed, 361 insertions(+), 140 deletions(-) (limited to 'stdlib/source/library') 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 (_ ) (-> ///phase.Wrapper Import Static Expander Compilation )) @@ -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 [] + [{ left right} + { (quantified @var @parameter left) + (quantified @var @parameter right)}]) + ([.#Sum] + [.#Product] + [.#Function] + [.#Apply]) + + {.#Var @} + (if (n.= @var @) + {.#Parameter @parameter} + :it:) + + (^template [] + [{ env body} + { (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 [ ] [{ _} @@ -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 [ ] [(def: .public ( 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 [] + [{ left right} + { (again left) (again right)}]) + ([.#Sum] + [.#Product] + [.#Function] + [.#Apply]) + + (^template [] + [{ env body} + { (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 (|>> { 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 [] [{ envT+ unquantifiedT} (do [! ..monad] - [envT+' (monad.each ! clean envT+)] - (in { envT+' unquantifiedT}))]) + [envT+' (monad.each ! clean envT+) + unquantifiedT' (clean unquantifiedT)] + (in { envT+' unquantifiedT'}))]) ([.#UnivQ] [.#ExQ]) )) -- cgit v1.2.3