From e814f667aed509a70bd386dcd54628929134def4 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Thu, 26 Aug 2021 02:34:05 -0400 Subject: "Interface" instead of "interface:", and "Rec" can be used in type definition. --- stdlib/source/library/lux.lux | 351 +++++++++++------------------------------- 1 file changed, 86 insertions(+), 265 deletions(-) (limited to 'stdlib/source/library/lux.lux') diff --git a/stdlib/source/library/lux.lux b/stdlib/source/library/lux.lux index 389635abc..c87b674f0 100644 --- a/stdlib/source/library/lux.lux +++ b/stdlib/source/library/lux.lux @@ -138,19 +138,20 @@ ["None" "Some"] #1) -... (type: .public #rec Type -... (#Primitive Text (List Type)) -... (#Sum Type Type) -... (#Product Type Type) -... (#Function Type Type) -... (#Parameter Nat) -... (#Var Nat) -... (#Ex Nat) -... (#UnivQ (List Type) Type) -... (#ExQ (List Type) Type) -... (#Apply Type Type) -... (#Named Name Type) -... ) +... (type: .public Type +... (Rec Type +... (Variant +... (#Primitive Text (List Type)) +... (#Sum Type Type) +... (#Product Type Type) +... (#Function Type Type) +... (#Parameter Nat) +... (#Var Nat) +... (#Ex Nat) +... (#UnivQ (List Type) Type) +... (#ExQ (List Type) Type) +... (#Apply Type Type) +... (#Named Name Type)))) ("lux def type tagged" Type (9 #1 ["library/lux" "Type"] ({Type @@ -194,9 +195,7 @@ ("lux type check type" (9 #0 Type List)))} ("lux type check type" (9 #0 (4 #0 1) (4 #0 0))))) [dummy_location - (9 #1 (#Item [[dummy_location (7 #0 ["library/lux" "type_rec?"])] - [dummy_location (0 #0 #1)]] - #End))] + (9 #1 #End)] ["Primitive" "Sum" "Product" "Function" "Parameter" "Var" "Ex" "UnivQ" "ExQ" "Apply" "Named"] #1) @@ -1399,11 +1398,12 @@ (failure "Wrong syntax for $_")} tokens)) -... (interface: (Monad m) -... (: (All [a] (-> a (m a))) -... in) -... (: (All [a b] (-> (-> a (m b)) (m a) (m b))) -... then)) +... (type: (Monad m) +... (Interface +... (: (All [a] (-> a (m a))) +... in) +... (: (All [a b] (-> (-> a (m b)) (m a) (m b))) +... then))) ("lux def type tagged" Monad (#Named ["library/lux" "Monad"] (All [m] @@ -2404,17 +2404,6 @@ (local_identifier$ ($_ text\composite "__gensym__" prefix (nat\encoded seed))))} state)) -(macro:' .public (Rec tokens) - ({(#Item [_ (#Identifier "" name)] (#Item body #End)) - (let' [body' (|> body - nested_quantification - (with_replacements (list [name (` (#.Apply (~ (type_parameter 1)) (~ (type_parameter 0))))])))] - (in_meta (list (` (#.Apply .Nothing (#.UnivQ #.End (~ body'))))))) - - _ - (failure "Wrong syntax for Rec")} - tokens)) - (macro:' .public (exec tokens) (list) ({(#Item value actions) @@ -3367,7 +3356,7 @@ (#Some [tokens' [slot type]]) _ - #.None)) + #None)) (def: un_paired (-> (List [Code Code]) (List Code)) @@ -3395,21 +3384,11 @@ _ (failure "Wrong syntax for Record"))) -(def: (recP tokens) - (-> (List Code) [(List Code) Bit]) - (case tokens - (^ (list& [_ (#Tag ["" "rec"])] tokens')) - [tokens' #1] - - _ - [tokens #0])) - (def: (typeP tokens) - (-> (List Code) (Maybe [Code Bit Text (List Text) (List [Code Code]) Code])) + (-> (List Code) (Maybe [Code Text (List Text) (List [Code Code]) Code])) (|> (do maybe_monad [% (anyP tokens) .let' [[tokens export_policy] %] - .let' [[tokens rec?] (recP tokens)] % (local_declarationP tokens) .let' [[tokens [name parameters]] %] % (annotationsP tokens) @@ -3417,42 +3396,35 @@ % (anyP tokens) .let' [[tokens definition] %] _ (endP tokens)] - (in [export_policy rec? name parameters annotations definition])) - ... (^ (list _export_policy _rec _declaration _annotations _body)) + (in [export_policy name parameters annotations definition])) ... (^ (list _export_policy _declaration _annotations _body)) (maybe\else' (do maybe_monad - [.let' [[tokens rec?] (recP tokens)] - % (local_declarationP tokens) + [% (local_declarationP tokens) .let' [[tokens [name parameters]] %] % (annotationsP tokens) .let' [[tokens annotations] %] % (anyP tokens) .let' [[tokens definition] %] _ (endP tokens)] - (in [(` ..private) rec? name parameters annotations definition]))) - ... (^ (list _rec _declaration _annotations _body)) + (in [(` ..private) name parameters annotations definition]))) ... (^ (list _declaration _annotations _body)) (maybe\else' (do maybe_monad - [.let' [[tokens rec?] (recP tokens)] - % (local_declarationP tokens) + [% (local_declarationP tokens) .let' [[tokens [name parameters]] %] % (anyP tokens) .let' [[tokens definition] %] _ (endP tokens)] - (in [(` ..private) rec? name parameters #End definition]))) - ... (^ (list _rec _declaration _body)) + (in [(` ..private) name parameters #End definition]))) ... (^ (list _declaration _body)) (maybe\else' (do maybe_monad [% (anyP tokens) .let' [[tokens export_policy] %] - .let' [[tokens rec?] (recP tokens)] % (local_declarationP tokens) .let' [[tokens [name parameters]] %] % (anyP tokens) .let' [[tokens definition] %] _ (endP tokens)] - (in [export_policy rec? name parameters #End definition]))) - ... (^ (list _export_policy _rec _declaration _body)) + (in [export_policy name parameters #End definition]))) ... (^ (list _export_policy _declaration _body)) )) @@ -3491,32 +3463,20 @@ (macro: .public (type: tokens) (case (typeP tokens) - (#Some [export_policy rec? name args meta type_codes]) + (#Some [export_policy name args meta type_codes]) (do meta_monad [type+tags?? (..type_declaration type_codes) module_name current_module_name .let' [type_name (local_identifier$ name) [type tags??] type+tags?? type' (: (Maybe Code) - (if rec? - (if (empty? args) - (let [g!param (local_identifier$ "") - prime_name (local_identifier$ name) - type+ (with_replacements (list [name (` ((~ prime_name) .Nothing))]) - type)] - (#Some (` ((All (~ prime_name) [(~ g!param)] (~ type+)) - .Nothing)))) - #None) - (case args - #End - (#Some type) + (case args + #End + (#Some type) - _ - (#Some (` (.All (~ type_name) [(~+ (list\each local_identifier$ args))] (~ type))))))) - total_meta (let [meta (definition_annotations meta) - meta (if rec? - (` (#.Item (~ (flag_meta "type_rec?")) (~ meta))) - meta)] + _ + (#Some (` (.All (~ type_name) [(~+ (list\each local_identifier$ args))] (~ type)))))) + total_meta (let [meta (definition_annotations meta)] (` [(~ location_code) (#.Record (~ meta))]))]] (case type' @@ -3545,64 +3505,6 @@ #None (failure "Wrong syntax for type:"))) -(def:' .private (interfaceP tokens) - (-> (List Code) (Maybe [Code Text (List Text) (List [Code Code]) (List Code)])) - (|> (do maybe_monad - [% (declarationP tokens) - .let' [[tokens [export_policy name parameters]] %] - % (annotationsP tokens) - .let' [[tokens annotations] %]] - (in [export_policy name parameters annotations tokens])) - ... (^ (list _export_policy _declaration _annotations _body)) - ... (^ (list _declaration _annotations _body)) - (maybe\else' (do maybe_monad - [% (local_declarationP tokens) - .let' [[tokens [name parameters]] %]] - (in [(` ..private) name parameters #End tokens]))) - ... (^ (list _declaration _body)) - (maybe\else' (do maybe_monad - [% (declarationP tokens) - .let' [[tokens [export_policy name parameters]] %]] - (in [export_policy name parameters #End tokens]))) - ... (^ (list _export_policy _declaration _body)) - )) - -(macro: .public (interface: tokens) - (case (interfaceP tokens) - (#Some [export_policy name args annotations methods]) - (do meta_monad - [methods' (monad\each meta_monad expansion methods) - members (: (Meta (List [Text Code])) - (monad\each meta_monad - (: (-> Code (Meta [Text Code])) - (function (_ token) - (case token - (^ [_ (#Form (list [_ (#Text "lux type check")] type [_ (#Identifier ["" name])]))]) - (in [name type]) - - _ - (failure "Interfaces require typed members!")))) - (list\conjoint methods'))) - .let [def_name (local_identifier$ name) - interface_type (` (..Record - (~ (record$ (list\each (: (-> [Text Code] [Code Code]) - (function (_ [module_name m_type]) - [(local_tag$ module_name) m_type])) - members))))) - usage (case args - #End - def_name - - _ - (` ((~ def_name) (~+ (list\each local_identifier$ args)))))]] - (in_meta (list (` (..type: (~ export_policy) - (~ usage) - (~ (record$ annotations)) - (~ interface_type)))))) - - #None - (failure "Wrong syntax for interface:"))) - (template [ ] [(def: .public ( value) (-> (I64 Any) ) @@ -3926,7 +3828,7 @@ code\encoded)))) )) -(def: (only p xs) +(def: (list\only p xs) (All [a] (-> (-> a Bit) (List a) (List a))) (case xs #End @@ -3934,8 +3836,8 @@ (#Item x xs') (if (p x) - (#Item x (only p xs')) - (only p xs')))) + (#Item x (list\only p xs')) + (list\only p xs')))) (def: (is_member? cases name) (-> (List Text) Text Bit) @@ -4377,7 +4279,7 @@ (do meta_monad [*defs (exported_definitions module_name) _ (test_referrals module_name *defs _defs)] - (in (..only (|>> (is_member? _defs) not) *defs))) + (in (..list\only (|>> (is_member? _defs) not) *defs))) #Ignore (in (list)) @@ -4643,47 +4545,6 @@ _ (failure "Wrong syntax for ^template"))) -(def: (baseline_column code) - (-> Code Nat) - (case code - (^template [] - [[[_ _ column] ( _)] - column]) - ([#Bit] - [#Nat] - [#Int] - [#Rev] - [#Frac] - [#Text] - [#Identifier] - [#Tag]) - - (^template [] - [[[_ _ column] ( parts)] - (list\mix n/min column (list\each baseline_column parts))]) - ([#Form] - [#Tuple]) - - [[_ _ column] (#Record pairs)] - (list\mix n/min column - (list\composite (list\each (|>> product\left baseline_column) pairs) - (list\each (|>> product\right baseline_column) pairs))) - )) - -(type: Documentation_Fragment - (Variant - (#Documentation_Comment Text) - (#Documentation_Example Code))) - -(def: (documentation_fragment code) - (-> Code Documentation_Fragment) - (case code - [_ (#Text comment)] - (#Documentation_Comment comment) - - _ - (#Documentation_Example code))) - (template [ ] [(def: .public (All [s] (-> (I64 s) (I64 s))) @@ -4693,92 +4554,6 @@ [-- "lux i64 -"] ) -(def: tag\encoded - (-> Name Text) - (|>> name\encoded - (text\composite "#"))) - -(def: (repeated n x) - (All [a] (-> Int a (List a))) - (if ("lux i64 <" n +0) - (#Item x (repeated ("lux i64 +" -1 n) x)) - #End)) - -(def: (location_padding baseline [_ old_line old_column] [_ new_line new_column]) - (-> Nat Location Location Text) - (if ("lux i64 =" old_line new_line) - (text\interposed "" (repeated (.int ("lux i64 -" old_column new_column)) " ")) - (let [extra_lines (text\interposed "" (repeated (.int ("lux i64 -" old_line new_line)) ..\n)) - space_padding (text\interposed "" (repeated (.int ("lux i64 -" baseline new_column)) " "))] - (text\composite extra_lines space_padding)))) - -(def: (text\size x) - (-> Text Nat) - ("lux text size" x)) - -(def: (updated_location [file line column] code_text) - (-> Location Text Location) - [file line ("lux i64 +" column (text\size code_text))]) - -(def: (example_documentation prev_location baseline example) - (-> Location Nat Code [Location Text]) - (case example - (^template [ ] - [[new_location ( value)] - (let [as_text ( value)] - [(updated_location new_location as_text) - (text\composite (location_padding baseline prev_location new_location) - as_text)])]) - ([#Bit bit\encoded] - [#Nat nat\encoded] - [#Int int\encoded] - [#Frac frac\encoded] - [#Text text\encoded] - [#Identifier name\encoded] - [#Tag tag\encoded]) - - (^template [ ] - [[group_location ( parts)] - (let [[group_location' parts_text] (list\mix (function (_ part [last_location text_accum]) - (let [[part_location part_text] (example_documentation last_location baseline part)] - [part_location (text\composite text_accum part_text)])) - [(revised@ #column ++ group_location) ""] - ( parts))] - [(revised@ #column ++ group_location') - ($_ text\composite (location_padding baseline prev_location group_location) - - parts_text - )])]) - ([#Form "(" ")" |>] - [#Tuple "[" "]" |>] - [#Record "{" "}" ..un_paired]) - - [new_location (#Rev value)] - ("lux io error" "@example_documentation Undefined behavior.") - )) - -(def: (fragment_documentation fragment) - (-> Documentation_Fragment Text) - (case fragment - (#Documentation_Comment comment) - (|> comment - (text\all_split_by ..\n) - (list\each (function (_ line) ($_ text\composite "... " line ..\n))) - (text\interposed "")) - - (#Documentation_Example example) - (let [baseline (baseline_column example) - [location _] example - [_ text] (..example_documentation (with@ #column baseline location) baseline example)] - (text\composite text "\n\n")))) - -(macro: .public (example tokens) - (in_meta (list (` [(~ location_code) - (#.Text (~ (|> tokens - (list\each (|>> ..documentation_fragment ..fragment_documentation)) - (text\interposed "") - text$)))])))) - (def: (interleaved xs ys) (All [a] (-> (List a) (List a) (List a))) (case xs @@ -5557,3 +5332,49 @@ _ (..failure (..wrong_syntax_error (name_of ..try))))) + +(def: (methodP tokens) + (-> (List Code) (Maybe [(List Code) [Text Code]])) + (case tokens + (^ (list& [_ (#Form (list [_ (#Text "lux type check")] type [_ (#Identifier ["" name])]))] + tokens')) + (#Some [tokens' [name type]]) + + _ + #None)) + +(macro: .public (Interface tokens) + (do meta_monad + [methods' (monad\each meta_monad expansion tokens)] + (case (everyP methodP (list\conjoint methods')) + (#Some methods) + (in (list (` (..Tuple (~+ (list\each product\right methods)))) + (tuple$ (list\each (|>> product\left text$) methods)))) + + #None + (failure "Wrong syntax for Interface")))) + +(def: (recursive_type name body) + (-> Text Code Code) + (let [body' (|> body + nested_quantification + (with_replacements (list [name (` (#.Apply .Nothing (~ (type_parameter 0))))])))] + (` (#.Apply .Nothing (#.UnivQ #.End (~ body')))))) + +(macro: .public (Rec tokens) + (case tokens + (^ (list [_ (#Identifier "" name)] body)) + (do meta_monad + [body' (expansion body)] + (case body' + (^ (list body' labels)) + (in (list (..recursive_type name body') labels)) + + (^ (list body')) + (in (list (..recursive_type name body'))) + + _ + (failure "Wrong syntax for Rec"))) + + _ + (failure "Wrong syntax for Rec"))) -- cgit v1.2.3