From a8d76e48df01d0f5326faa8456797f91cb2cbeba Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Thu, 30 Jun 2022 22:53:23 -0400 Subject: Alternative names for (un)quoting macros. --- stdlib/source/parser/lux/data/binary.lux | 5 +- stdlib/source/parser/lux/meta/type.lux | 351 +++++++++++++++++++++++++++++++ stdlib/source/parser/lux/program.lux | 8 +- stdlib/source/parser/lux/type.lux | 350 ------------------------------ 4 files changed, 358 insertions(+), 356 deletions(-) create mode 100644 stdlib/source/parser/lux/meta/type.lux delete mode 100644 stdlib/source/parser/lux/type.lux (limited to 'stdlib/source/parser') diff --git a/stdlib/source/parser/lux/data/binary.lux b/stdlib/source/parser/lux/data/binary.lux index 1e1ac7704..00c3d3656 100644 --- a/stdlib/source/parser/lux/data/binary.lux +++ b/stdlib/source/parser/lux/data/binary.lux @@ -2,7 +2,6 @@ [library [lux (.except and or nat int rev list symbol type) [ffi (.only)] - [type (.only sharing)] [abstract [hash (.only Hash)] [monad (.only do)]] @@ -29,7 +28,9 @@ [math [number ["n" nat] - ["[0]" frac]]]]]) + ["[0]" frac]]] + [meta + [type (.only sharing)]]]]) (.type .public Offset Nat) diff --git a/stdlib/source/parser/lux/meta/type.lux b/stdlib/source/parser/lux/meta/type.lux new file mode 100644 index 000000000..7c7090474 --- /dev/null +++ b/stdlib/source/parser/lux/meta/type.lux @@ -0,0 +1,351 @@ +(.require + [library + [lux (.except function local parameter) + [abstract + ["[0]" monad (.only do)]] + [control + ["//" parser] + ["[0]" try (.only Try)] + ["[0]" exception (.only exception)] + ["[0]" function]] + [data + ["[0]" text (.use "[1]#[0]" monoid) + ["%" \\format (.only format)]] + [collection + ["[0]" list (.use "[1]#[0]" functor)] + ["[0]" dictionary (.only Dictionary)]]] + [macro + ["^" pattern] + ["[0]" code]] + [math + [number + ["n" nat (.use "[1]#[0]" decimal)]]]]] + [\\library + ["[0]" / (.use "[1]#[0]" equivalence) + ["[0]" check]]]) + +(def |recursion_dummy| + (template (|recursion_dummy|) + [{.#Primitive "" {.#End}}])) + +(with_template [] + [(exception .public ( [type Type]) + (exception.report + "Type" (%.type type)))] + + [not_existential] + [not_recursive] + [not_named] + [not_parameter] + [unknown_parameter] + [not_function] + [not_application] + [not_polymorphic] + [not_variant] + [not_tuple] + ) + +(with_template [] + [(exception .public ( [expected Type + actual Type]) + (exception.report + "Expected" (%.type expected) + "Actual" (%.type actual)))] + + [types_do_not_match] + [wrong_parameter] + ) + +(exception .public empty_input) + +(exception .public (unconsumed_input [remaining (List Type)]) + (exception.report + "Types" (|> remaining + (list#each (|>> %.type (format text.new_line "* "))) + (text.interposed "")))) + +(type .public Env + (Dictionary Nat [Type Code])) + +(type .public (Parser a) + (//.Parser [Env (List Type)] a)) + +(def .public fresh + Env + (dictionary.empty n.hash)) + +(def (result' env poly types) + (All (_ a) (-> Env (Parser a) (List Type) (Try a))) + (case (//.result poly [env types]) + {try.#Failure error} + {try.#Failure error} + + {try.#Success [[env' remaining] output]} + (case remaining + {.#End} + {try.#Success output} + + _ + (exception.except ..unconsumed_input remaining)))) + +(def .public (result poly type) + (All (_ a) (-> (Parser a) Type (Try a))) + (result' ..fresh poly (list type))) + +(def .public env + (Parser Env) + (.function (_ [env inputs]) + {try.#Success [[env inputs] env]})) + +(def (with_env temp poly) + (All (_ a) (-> Env (Parser a) (Parser a))) + (.function (_ [env inputs]) + (case (//.result poly [temp inputs]) + {try.#Failure error} + {try.#Failure error} + + {try.#Success [[_ remaining] output]} + {try.#Success [[env remaining] output]}))) + +(def .public next + (Parser Type) + (.function (_ [env inputs]) + (case inputs + {.#End} + (exception.except ..empty_input []) + + {.#Item headT tail} + {try.#Success [[env inputs] headT]}))) + +(def .public any + (Parser Type) + (.function (_ [env inputs]) + (case inputs + {.#End} + (exception.except ..empty_input []) + + {.#Item headT tail} + {try.#Success [[env tail] headT]}))) + +(def .public (local types poly) + (All (_ a) (-> (List Type) (Parser a) (Parser a))) + (.function (_ [env pass_through]) + (case (result' env poly types) + {try.#Failure error} + {try.#Failure error} + + {try.#Success output} + {try.#Success [[env pass_through] output]}))) + +(def (label idx) + (-> Nat Code) + (code.local (all text#composite "label" text.tab (n#encoded idx)))) + +(def .public (with_extension type poly) + (All (_ a) (-> Type (Parser a) (Parser [Code a]))) + (.function (_ [env inputs]) + (let [current_id (dictionary.size env) + g!var (label current_id)] + (case (//.result poly + [(dictionary.has current_id [type g!var] env) + inputs]) + {try.#Failure error} + {try.#Failure error} + + {try.#Success [[_ inputs'] output]} + {try.#Success [[env inputs'] [g!var output]]})))) + +(with_template [ ] + [(`` (def .public ( poly) + (All (_ a) (-> (Parser a) (Parser a))) + (do //.monad + [headT ..any] + (let [members ( (/.anonymous headT))] + (if (n.> 1 (list.size members)) + (local members poly) + (//.failure (exception.error headT)))))))] + + [variant /.flat_variant ..not_variant] + [tuple /.flat_tuple ..not_tuple] + ) + +(def polymorphic' + (Parser [Nat Type]) + (do //.monad + [headT any + .let [[num_arg bodyT] (/.flat_univ_q (/.anonymous headT))]] + (if (n.= 0 num_arg) + (//.failure (exception.error ..not_polymorphic headT)) + (in [num_arg bodyT])))) + +(def .public (polymorphic poly) + (All (_ a) (-> (Parser a) (Parser [Code (List Code) a]))) + (do [! //.monad] + [headT any + funcI (at ! each dictionary.size ..env) + [num_args non_poly] (local (list headT) ..polymorphic') + env ..env + .let [funcL (label funcI) + [all_varsL env'] (loop (again [current_arg 0 + env' env + all_varsL (is (List Code) (list))]) + (if (n.< num_args current_arg) + (if (n.= 0 current_arg) + (let [varL (label (++ funcI))] + (again (++ current_arg) + (|> env' + (dictionary.has funcI [headT funcL]) + (dictionary.has (++ funcI) [{.#Parameter (++ funcI)} varL])) + {.#Item varL all_varsL})) + (let [partialI (|> current_arg (n.* 2) (n.+ funcI)) + partial_varI (++ partialI) + partial_varL (label partial_varI) + partialC (` ((~ funcL) (~+ (|> (list.indices num_args) + (list#each (|>> (n.* 2) ++ (n.+ funcI) label)) + list.reversed))))] + (again (++ current_arg) + (|> env' + (dictionary.has partialI [(|recursion_dummy|) partialC]) + (dictionary.has partial_varI [{.#Parameter partial_varI} partial_varL])) + {.#Item partial_varL all_varsL}))) + [all_varsL env']))]] + (<| (with_env env') + (local (list non_poly)) + (do ! + [output poly] + (in [funcL all_varsL output]))))) + +(def .public (function in_poly out_poly) + (All (_ i o) (-> (Parser i) (Parser o) (Parser [i o]))) + (do //.monad + [headT any + .let [[inputsT outputT] (/.flat_function (/.anonymous headT))]] + (if (n.> 0 (list.size inputsT)) + (//.and (local inputsT in_poly) + (local (list outputT) out_poly)) + (//.failure (exception.error ..not_function headT))))) + +(def .public (applied poly) + (All (_ a) (-> (Parser a) (Parser a))) + (do //.monad + [headT any + .let [[funcT paramsT] (/.flat_application (/.anonymous headT))]] + (if (n.= 0 (list.size paramsT)) + (//.failure (exception.error ..not_application headT)) + (..local {.#Item funcT paramsT} poly)))) + +(with_template [ ] + [(def .public ( expected) + (-> Type (Parser Any)) + (do //.monad + [actual any] + (if ( expected actual) + (in []) + (//.failure (exception.error ..types_do_not_match [expected actual])))))] + + [exactly /#=] + [sub check.subsumes?] + [super (function.flipped check.subsumes?)] + ) + +(def .public (argument env idx) + (-> Env Nat Nat) + (let [env_level (n./ 2 (dictionary.size env)) + parameter_level (n./ 2 idx) + parameter_idx (n.% 2 idx)] + (|> env_level -- (n.- parameter_level) (n.* 2) (n.+ parameter_idx)))) + +(def .public parameter + (Parser Code) + (do //.monad + [env ..env + headT any] + (case headT + {.#Parameter idx} + (case (dictionary.value (..argument env idx) env) + {.#Some [poly_type poly_code]} + (in poly_code) + + {.#None} + (//.failure (exception.error ..unknown_parameter headT))) + + _ + (//.failure (exception.error ..not_parameter headT))))) + +(def .public (this_parameter id) + (-> Nat (Parser Any)) + (do //.monad + [env ..env + headT any] + (case headT + {.#Parameter idx} + (if (n.= id (..argument env idx)) + (in []) + (//.failure (exception.error ..wrong_parameter [{.#Parameter id} headT]))) + + _ + (//.failure (exception.error ..not_parameter headT))))) + +(def .public existential + (Parser Nat) + (do //.monad + [headT any] + (case headT + {.#Ex ex_id} + (in ex_id) + + _ + (//.failure (exception.error ..not_existential headT))))) + +(def .public named + (Parser [Symbol Type]) + (do //.monad + [inputT any] + (case inputT + {.#Named name anonymousT} + (in [name anonymousT]) + + _ + (//.failure (exception.error ..not_named inputT))))) + +(def .public (recursive poly) + (All (_ a) (-> (Parser a) (Parser [Code a]))) + (do [! //.monad] + [headT any] + (case (/.anonymous headT) + (pattern {.#Apply (|recursion_dummy|) {.#UnivQ _ headT'}}) + (do ! + [[recT _ output] (|> poly + (with_extension (|recursion_dummy|)) + (with_extension headT) + (local (list headT')))] + (in [recT output])) + + _ + (//.failure (exception.error ..not_recursive headT))))) + +(def .public recursive_self + (Parser Code) + (do //.monad + [env ..env + headT any] + (case (/.anonymous headT) + (^.multi (pattern {.#Apply (|recursion_dummy|) {.#Parameter funcT_idx}}) + (n.= 0 (..argument env funcT_idx)) + [(dictionary.value 0 env) {.#Some [self_type self_call]}]) + (in self_call) + + _ + (//.failure (exception.error ..not_recursive headT))))) + +(def .public recursive_call + (Parser Code) + (do [! //.monad] + [env ..env + [funcT argsT] (..applied (//.and any (//.many any))) + _ (local (list funcT) (..this_parameter 0)) + allC (let [allT (list.partial funcT argsT)] + (|> allT + (monad.each ! (function.constant ..parameter)) + (local allT)))] + (in (` ((~+ allC)))))) diff --git a/stdlib/source/parser/lux/program.lux b/stdlib/source/parser/lux/program.lux index e834136d8..eff42b3ad 100644 --- a/stdlib/source/parser/lux/program.lux +++ b/stdlib/source/parser/lux/program.lux @@ -59,9 +59,6 @@ (function (_ inputs) (loop (again [immediate inputs]) (case (//.result cli immediate) - {try.#Success [remaining output]} - {try.#Success [remaining output]} - {try.#Failure try} (case immediate {.#End} @@ -71,7 +68,10 @@ (do try.monad [[remaining output] (again immediate')] (in [{.#Item to_omit remaining} - output]))))))) + output]))) + + success + success)))) (def .public end (Parser Any) diff --git a/stdlib/source/parser/lux/type.lux b/stdlib/source/parser/lux/type.lux deleted file mode 100644 index a107a1778..000000000 --- a/stdlib/source/parser/lux/type.lux +++ /dev/null @@ -1,350 +0,0 @@ -(.require - [library - [lux (.except function local parameter) - [abstract - ["[0]" monad (.only do)]] - [control - ["//" parser] - ["[0]" try (.only Try)] - ["[0]" exception (.only exception)] - ["[0]" function]] - [data - ["[0]" text (.use "[1]#[0]" monoid) - ["%" \\format (.only format)]] - [collection - ["[0]" list (.use "[1]#[0]" functor)] - ["[0]" dictionary (.only Dictionary)]]] - [macro - ["^" pattern] - ["[0]" code]] - [math - [number - ["n" nat (.use "[1]#[0]" decimal)]]] - ["[0]" type (.use "[1]#[0]" equivalence) - ["[0]" check]]]]) - -(def |recursion_dummy| - (template (|recursion_dummy|) - [{.#Primitive "" {.#End}}])) - -(with_template [] - [(exception .public ( [type Type]) - (exception.report - "Type" (%.type type)))] - - [not_existential] - [not_recursive] - [not_named] - [not_parameter] - [unknown_parameter] - [not_function] - [not_application] - [not_polymorphic] - [not_variant] - [not_tuple] - ) - -(with_template [] - [(exception .public ( [expected Type - actual Type]) - (exception.report - "Expected" (%.type expected) - "Actual" (%.type actual)))] - - [types_do_not_match] - [wrong_parameter] - ) - -(exception .public empty_input) - -(exception .public (unconsumed_input [remaining (List Type)]) - (exception.report - "Types" (|> remaining - (list#each (|>> %.type (format text.new_line "* "))) - (text.interposed "")))) - -(type .public Env - (Dictionary Nat [Type Code])) - -(type .public (Parser a) - (//.Parser [Env (List Type)] a)) - -(def .public fresh - Env - (dictionary.empty n.hash)) - -(def (result' env poly types) - (All (_ a) (-> Env (Parser a) (List Type) (Try a))) - (case (//.result poly [env types]) - {try.#Failure error} - {try.#Failure error} - - {try.#Success [[env' remaining] output]} - (case remaining - {.#End} - {try.#Success output} - - _ - (exception.except ..unconsumed_input remaining)))) - -(def .public (result poly type) - (All (_ a) (-> (Parser a) Type (Try a))) - (result' ..fresh poly (list type))) - -(def .public env - (Parser Env) - (.function (_ [env inputs]) - {try.#Success [[env inputs] env]})) - -(def (with_env temp poly) - (All (_ a) (-> Env (Parser a) (Parser a))) - (.function (_ [env inputs]) - (case (//.result poly [temp inputs]) - {try.#Failure error} - {try.#Failure error} - - {try.#Success [[_ remaining] output]} - {try.#Success [[env remaining] output]}))) - -(def .public next - (Parser Type) - (.function (_ [env inputs]) - (case inputs - {.#End} - (exception.except ..empty_input []) - - {.#Item headT tail} - {try.#Success [[env inputs] headT]}))) - -(def .public any - (Parser Type) - (.function (_ [env inputs]) - (case inputs - {.#End} - (exception.except ..empty_input []) - - {.#Item headT tail} - {try.#Success [[env tail] headT]}))) - -(def .public (local types poly) - (All (_ a) (-> (List Type) (Parser a) (Parser a))) - (.function (_ [env pass_through]) - (case (result' env poly types) - {try.#Failure error} - {try.#Failure error} - - {try.#Success output} - {try.#Success [[env pass_through] output]}))) - -(def (label idx) - (-> Nat Code) - (code.local (all text#composite "label" text.tab (n#encoded idx)))) - -(def .public (with_extension type poly) - (All (_ a) (-> Type (Parser a) (Parser [Code a]))) - (.function (_ [env inputs]) - (let [current_id (dictionary.size env) - g!var (label current_id)] - (case (//.result poly - [(dictionary.has current_id [type g!var] env) - inputs]) - {try.#Failure error} - {try.#Failure error} - - {try.#Success [[_ inputs'] output]} - {try.#Success [[env inputs'] [g!var output]]})))) - -(with_template [ ] - [(`` (def .public ( poly) - (All (_ a) (-> (Parser a) (Parser a))) - (do //.monad - [headT ..any] - (let [members ( (type.anonymous headT))] - (if (n.> 1 (list.size members)) - (local members poly) - (//.failure (exception.error headT)))))))] - - [variant type.flat_variant ..not_variant] - [tuple type.flat_tuple ..not_tuple] - ) - -(def polymorphic' - (Parser [Nat Type]) - (do //.monad - [headT any - .let [[num_arg bodyT] (type.flat_univ_q (type.anonymous headT))]] - (if (n.= 0 num_arg) - (//.failure (exception.error ..not_polymorphic headT)) - (in [num_arg bodyT])))) - -(def .public (polymorphic poly) - (All (_ a) (-> (Parser a) (Parser [Code (List Code) a]))) - (do [! //.monad] - [headT any - funcI (at ! each dictionary.size ..env) - [num_args non_poly] (local (list headT) ..polymorphic') - env ..env - .let [funcL (label funcI) - [all_varsL env'] (loop (again [current_arg 0 - env' env - all_varsL (is (List Code) (list))]) - (if (n.< num_args current_arg) - (if (n.= 0 current_arg) - (let [varL (label (++ funcI))] - (again (++ current_arg) - (|> env' - (dictionary.has funcI [headT funcL]) - (dictionary.has (++ funcI) [{.#Parameter (++ funcI)} varL])) - {.#Item varL all_varsL})) - (let [partialI (|> current_arg (n.* 2) (n.+ funcI)) - partial_varI (++ partialI) - partial_varL (label partial_varI) - partialC (` ((~ funcL) (~+ (|> (list.indices num_args) - (list#each (|>> (n.* 2) ++ (n.+ funcI) label)) - list.reversed))))] - (again (++ current_arg) - (|> env' - (dictionary.has partialI [(|recursion_dummy|) partialC]) - (dictionary.has partial_varI [{.#Parameter partial_varI} partial_varL])) - {.#Item partial_varL all_varsL}))) - [all_varsL env']))]] - (<| (with_env env') - (local (list non_poly)) - (do ! - [output poly] - (in [funcL all_varsL output]))))) - -(def .public (function in_poly out_poly) - (All (_ i o) (-> (Parser i) (Parser o) (Parser [i o]))) - (do //.monad - [headT any - .let [[inputsT outputT] (type.flat_function (type.anonymous headT))]] - (if (n.> 0 (list.size inputsT)) - (//.and (local inputsT in_poly) - (local (list outputT) out_poly)) - (//.failure (exception.error ..not_function headT))))) - -(def .public (applied poly) - (All (_ a) (-> (Parser a) (Parser a))) - (do //.monad - [headT any - .let [[funcT paramsT] (type.flat_application (type.anonymous headT))]] - (if (n.= 0 (list.size paramsT)) - (//.failure (exception.error ..not_application headT)) - (..local {.#Item funcT paramsT} poly)))) - -(with_template [ ] - [(def .public ( expected) - (-> Type (Parser Any)) - (do //.monad - [actual any] - (if ( expected actual) - (in []) - (//.failure (exception.error ..types_do_not_match [expected actual])))))] - - [exactly type#=] - [sub check.subsumes?] - [super (function.flipped check.subsumes?)] - ) - -(def .public (argument env idx) - (-> Env Nat Nat) - (let [env_level (n./ 2 (dictionary.size env)) - parameter_level (n./ 2 idx) - parameter_idx (n.% 2 idx)] - (|> env_level -- (n.- parameter_level) (n.* 2) (n.+ parameter_idx)))) - -(def .public parameter - (Parser Code) - (do //.monad - [env ..env - headT any] - (case headT - {.#Parameter idx} - (case (dictionary.value (..argument env idx) env) - {.#Some [poly_type poly_code]} - (in poly_code) - - {.#None} - (//.failure (exception.error ..unknown_parameter headT))) - - _ - (//.failure (exception.error ..not_parameter headT))))) - -(def .public (this_parameter id) - (-> Nat (Parser Any)) - (do //.monad - [env ..env - headT any] - (case headT - {.#Parameter idx} - (if (n.= id (..argument env idx)) - (in []) - (//.failure (exception.error ..wrong_parameter [{.#Parameter id} headT]))) - - _ - (//.failure (exception.error ..not_parameter headT))))) - -(def .public existential - (Parser Nat) - (do //.monad - [headT any] - (case headT - {.#Ex ex_id} - (in ex_id) - - _ - (//.failure (exception.error ..not_existential headT))))) - -(def .public named - (Parser [Symbol Type]) - (do //.monad - [inputT any] - (case inputT - {.#Named name anonymousT} - (in [name anonymousT]) - - _ - (//.failure (exception.error ..not_named inputT))))) - -(def .public (recursive poly) - (All (_ a) (-> (Parser a) (Parser [Code a]))) - (do [! //.monad] - [headT any] - (case (type.anonymous headT) - (pattern {.#Apply (|recursion_dummy|) {.#UnivQ _ headT'}}) - (do ! - [[recT _ output] (|> poly - (with_extension (|recursion_dummy|)) - (with_extension headT) - (local (list headT')))] - (in [recT output])) - - _ - (//.failure (exception.error ..not_recursive headT))))) - -(def .public recursive_self - (Parser Code) - (do //.monad - [env ..env - headT any] - (case (type.anonymous headT) - (^.multi (pattern {.#Apply (|recursion_dummy|) {.#Parameter funcT_idx}}) - (n.= 0 (..argument env funcT_idx)) - [(dictionary.value 0 env) {.#Some [self_type self_call]}]) - (in self_call) - - _ - (//.failure (exception.error ..not_recursive headT))))) - -(def .public recursive_call - (Parser Code) - (do [! //.monad] - [env ..env - [funcT argsT] (..applied (//.and any (//.many any))) - _ (local (list funcT) (..this_parameter 0)) - allC (let [allT (list.partial funcT argsT)] - (|> allT - (monad.each ! (function.constant ..parameter)) - (local allT)))] - (in (` ((~+ allC)))))) -- cgit v1.2.3