diff options
Diffstat (limited to 'stdlib/source/parser')
| -rw-r--r-- | stdlib/source/parser/lux/data/binary.lux | 308 | ||||
| -rw-r--r-- | stdlib/source/parser/lux/tool/compiler/language/lux/synthesis.lux | 162 |
2 files changed, 470 insertions, 0 deletions
diff --git a/stdlib/source/parser/lux/data/binary.lux b/stdlib/source/parser/lux/data/binary.lux new file mode 100644 index 000000000..1a49d5315 --- /dev/null +++ b/stdlib/source/parser/lux/data/binary.lux @@ -0,0 +1,308 @@ +(.using + [library + [lux (.except and or nat int rev list type symbol) + [ffi (.only)] + [type (.only sharing)] + [abstract + [hash (.only Hash)] + [monad (.only do)]] + [control + ["//" parser (.open: "[1]#[0]" monad)] + ["[0]" try (.only Try)] + ["[0]" exception (.only exception:)]] + [data + ["/" binary + ["[1]" \\unsafe (.only Binary)]] + [text + ["%" \\format (.only format)] + [encoding + ["[0]" utf8]]] + [collection + ["[0]" list] + ["[0]" sequence (.only Sequence)] + ["[0]" set (.only Set)] + [array + [\\unsafe (.only)]]]] + [macro + ["^" pattern] + ["[0]" template]] + [math + [number + ["n" nat] + ["[0]" frac]]]]]) + +(type: .public Offset + Nat) + +(type: .public Parser + (//.Parser [Offset Binary])) + +(exception: .public (binary_was_not_fully_read [binary_length Nat + bytes_read Nat]) + (exception.report + "Binary length" (%.nat binary_length) + "Bytes read" (%.nat bytes_read))) + +(with_template [<name> <extension>] + [(def: <name> + (template (<name> <parameter> <subject>) + [(<extension> <parameter> <subject>)]))] + + [n#= "lux i64 ="] + [n#+ "lux i64 +"] + [n#- "lux i64 -"] + ) + +(def: .public (result parser input) + (All (_ a) (-> (Parser a) Binary (Try a))) + (case (parser [0 input]) + {try.#Success [[end _] output]} + (let [length (/.size input)] + (if (n#= end length) + {try.#Success output} + (exception.except ..binary_was_not_fully_read [length end]))) + + failure + (as_expected failure))) + +(def: .public end? + (Parser Bit) + (function (_ (^.let input [offset data])) + {try.#Success [input (n#= offset (/.size data))]})) + +(def: .public offset + (Parser Offset) + (function (_ (^.let input [offset data])) + {try.#Success [input offset]})) + +(def: .public remaining + (Parser Nat) + (function (_ (^.let input [offset data])) + {try.#Success [input (n#- offset (/.size data))]})) + +(type: .public Size + Nat) + +(def: .public size_8 Size 1) +(def: .public size_16 Size (n.* 2 size_8)) +(def: .public size_32 Size (n.* 2 size_16)) +(def: .public size_64 Size (n.* 2 size_32)) + +(exception: .public (range_out_of_bounds [length Nat + start Nat + end Nat]) + (exception.report + "Length" (%.nat length) + "Range start" (%.nat start) + "Range end" (%.nat end))) + +(with_template [<name> <size> <read>] + [(def: .public <name> + (Parser I64) + (function (_ [start binary]) + (let [end (n#+ <size> start)] + (if (n.< end (/.size binary)) + (exception.except ..range_out_of_bounds [(/.size binary) start end]) + (|> (<read> start binary) + [[end binary]] + {try.#Success})))))] + + [bits_8 ..size_8 /.bits_8] + [bits_16 ..size_16 /.bits_16] + [bits_32 ..size_32 /.bits_32] + [bits_64 ..size_64 /.bits_64] + ) + +(with_template [<name> <type>] + [(def: .public <name> (Parser <type>) ..bits_64)] + + [nat Nat] + [int Int] + [rev Rev] + ) + +(def: .public frac + (Parser Frac) + (//#each frac.of_bits ..bits_64)) + +(exception: .public (invalid_tag [range Nat + byte Nat]) + (exception.report + "Tag range" (%.nat range) + "Tag value" (%.nat byte))) + +(def: !variant + (template (!variant <case>+) + [(do [! //.monad] + [flag (is (Parser Nat) + ..bits_8)] + (with_expansions [<case>+' (template.spliced <case>+)] + (case flag + (^.with_template [<number> <tag> <parser>] + [<number> (`` (at ! each (|>> {(~~ (template.spliced <tag>))}) <parser>))]) + (<case>+') + + _ (//.lifted (exception.except ..invalid_tag [(template.amount [<case>+]) flag])))))])) + +(def: .public (or left right) + (All (_ l r) (-> (Parser l) (Parser r) (Parser (Or l r)))) + (!variant [[0 [.#Left] left] + [1 [.#Right] right]])) + +(def: .public (rec body) + (All (_ a) (-> (-> (Parser a) (Parser a)) (Parser a))) + (function (_ input) + (let [parser (body (rec body))] + (parser input)))) + +(def: .public any + (Parser Any) + (//#in [])) + +(exception: .public (not_a_bit [value Nat]) + (exception.report + "Expected values" "either 0 or 1" + "Actual value" (%.nat value))) + +(def: .public bit + (Parser Bit) + (do //.monad + [value (is (Parser Nat) + ..bits_8)] + (case value + 0 (in #0) + 1 (in #1) + _ (//.lifted (exception.except ..not_a_bit [value]))))) + +(def: .public (segment size) + (-> Nat (Parser Binary)) + (case size + 0 (//#in (/.empty 0)) + _ (function (_ [start binary]) + (let [end (n#+ size start)] + (if (n.< end (/.size binary)) + (exception.except ..range_out_of_bounds [(/.size binary) start end]) + (|> binary + (/.slice start size) + [[end binary]] + {try.#Success})))))) + +(with_template [<size> <name> <bits>] + [(`` (def: .public <name> + (Parser Binary) + (do //.monad + [size (//#each (|>> .nat) <bits>)] + (..segment size))))] + + [08 binary_8 ..bits_8] + [16 binary_16 ..bits_16] + [32 binary_32 ..bits_32] + [64 binary_64 ..bits_64] + ) + +(with_template [<size> <name> <binary>] + [(`` (def: .public <name> + (Parser Text) + (do //.monad + [utf8 <binary>] + (//.lifted (at utf8.codec decoded utf8)))))] + + [08 utf8_8 ..binary_8] + [16 utf8_16 ..binary_16] + [32 utf8_32 ..binary_32] + [64 utf8_64 ..binary_64] + ) + +(def: .public text ..utf8_64) + +(with_template [<size> <name> <bits>] + [(def: .public (<name> valueP) + (All (_ v) (-> (Parser v) (Parser (Sequence v)))) + (do //.monad + [amount (is (Parser Nat) + <bits>)] + (loop (again [index 0 + output (sharing [v] + (Parser v) + valueP + + (Sequence v) + sequence.empty)]) + (if (n.< amount index) + (do //.monad + [value valueP] + (again (.++ index) + (sequence.suffix value output))) + (//#in output)))))] + + [08 sequence_8 ..bits_8] + [16 sequence_16 ..bits_16] + [32 sequence_32 ..bits_32] + [64 sequence_64 ..bits_64] + ) + +(def: .public maybe + (All (_ a) (-> (Parser a) (Parser (Maybe a)))) + (..or ..any)) + +(def: .public (list value) + (All (_ a) (-> (Parser a) (Parser (List a)))) + (..rec + (|>> (//.and value) + (..or ..any)))) + +(exception: .public set_elements_are_not_unique) + +(def: .public (set hash value) + (All (_ a) (-> (Hash a) (Parser a) (Parser (Set a)))) + (do //.monad + [raw (..list value) + .let [output (set.of_list hash raw)] + _ (//.assertion (exception.error ..set_elements_are_not_unique []) + (n#= (list.size raw) + (set.size output)))] + (in output))) + +(def: .public symbol + (Parser Symbol) + (//.and ..text ..text)) + +(def: .public type + (Parser Type) + (..rec + (function (_ type) + (let [pair (//.and type type) + indexed ..nat + quantified (//.and (..list type) type)] + (!variant [[0 [.#Primitive] (//.and ..text (..list type))] + [1 [.#Sum] pair] + [2 [.#Product] pair] + [3 [.#Function] pair] + [4 [.#Parameter] indexed] + [5 [.#Var] indexed] + [6 [.#Ex] indexed] + [7 [.#UnivQ] quantified] + [8 [.#ExQ] quantified] + [9 [.#Apply] pair] + [10 [.#Named] (//.and ..symbol type)]]))))) + +(def: .public location + (Parser Location) + (all //.and ..text ..nat ..nat)) + +(def: .public code + (Parser Code) + (..rec + (function (_ again) + (let [sequence (..list again)] + (//.and ..location + (!variant [[0 [.#Bit] ..bit] + [1 [.#Nat] ..nat] + [2 [.#Int] ..int] + [3 [.#Rev] ..rev] + [4 [.#Frac] ..frac] + [5 [.#Text] ..text] + [6 [.#Symbol] ..symbol] + [7 [.#Form] sequence] + [8 [.#Variant] sequence] + [9 [.#Tuple] sequence]])))))) diff --git a/stdlib/source/parser/lux/tool/compiler/language/lux/synthesis.lux b/stdlib/source/parser/lux/tool/compiler/language/lux/synthesis.lux new file mode 100644 index 000000000..c6537531f --- /dev/null +++ b/stdlib/source/parser/lux/tool/compiler/language/lux/synthesis.lux @@ -0,0 +1,162 @@ +(.using + [library + [lux (.except function loop i64 local) + [abstract + [monad (.only do)]] + [control + ["//" parser] + ["[0]" try (.only Try)] + ["[0]" exception (.only exception:)]] + [data + ["[0]" bit] + ["[0]" text (.only) + ["%" \\format (.only format)]] + [collection + ["[0]" list]]] + [math + [number + ["n" nat] + ["[0]" i64] + ["[0]" frac]]] + [meta + ["[0]" symbol]] + [tool + [compiler + [reference (.only) + [variable (.only Register)]] + [arity (.only Arity)] + [language + [lux + [analysis (.only Environment)]]]]]]] + [\\library + ["[0]" / (.only Synthesis Abstraction)]]) + +(exception: .public (cannot_parse [input (List Synthesis)]) + (exception.report + "Input" (exception.listing /.%synthesis input))) + +(exception: .public (unconsumed_input [input (List Synthesis)]) + (exception.report + "Input" (exception.listing /.%synthesis input))) + +(exception: .public (expected_empty_input [input (List Synthesis)]) + (exception.report + "Input" (exception.listing /.%synthesis input))) + +(exception: .public (wrong_arity [expected Arity + actual Arity]) + (exception.report + "Expected" (%.nat expected) + "Actual" (%.nat actual))) + +(exception: .public empty_input) + +(type: .public Parser + (//.Parser (List Synthesis))) + +(def: .public (result parser input) + (All (_ a) (-> (Parser a) (List Synthesis) (Try a))) + (case (parser input) + {try.#Failure error} + {try.#Failure error} + + {try.#Success [{.#End} value]} + {try.#Success value} + + {try.#Success [unconsumed _]} + (exception.except ..unconsumed_input unconsumed))) + +(def: .public any + (Parser Synthesis) + (.function (_ input) + (case input + {.#End} + (exception.except ..empty_input []) + + {.#Item [head tail]} + {try.#Success [tail head]}))) + +(def: .public end + (Parser Any) + (.function (_ tokens) + (case tokens + {.#End} {try.#Success [tokens []]} + _ (exception.except ..expected_empty_input [tokens])))) + +(def: .public end? + (Parser Bit) + (.function (_ tokens) + {try.#Success [tokens (case tokens + {.#End} true + _ false)]})) + +(with_template [<query> <assertion> <tag> <type> <eq>] + [(`` (def: .public <query> + (Parser <type>) + (.function (_ input) + (case input + (pattern (list.partial (<tag> x) input')) + {try.#Success [input' x]} + + _ + (exception.except ..cannot_parse input))))) + + (`` (def: .public (<assertion> expected) + (-> <type> (Parser Any)) + (.function (_ input) + (case input + (pattern (list.partial (<tag> actual) input')) + (if (at <eq> = expected actual) + {try.#Success [input' []]} + (exception.except ..cannot_parse input)) + + _ + (exception.except ..cannot_parse input)))))] + + [bit this_bit /.bit Bit bit.equivalence] + [i64 this_i64 /.i64 I64 i64.equivalence] + [f64 this_f64 /.f64 Frac frac.equivalence] + [text this_text /.text Text text.equivalence] + [local this_local /.variable/local Nat n.equivalence] + [foreign this_foreign /.variable/foreign Nat n.equivalence] + [constant this_constant /.constant Symbol symbol.equivalence] + ) + +(def: .public (tuple parser) + (All (_ a) (-> (Parser a) (Parser a))) + (.function (_ input) + (case input + (pattern (list.partial (/.tuple head) tail)) + (do try.monad + [output (..result parser head)] + {try.#Success [tail output]}) + + _ + (exception.except ..cannot_parse input)))) + +(def: .public (function expected parser) + (All (_ a) (-> Arity (Parser a) (Parser [(Environment Synthesis) a]))) + (.function (_ input) + (case input + (pattern (list.partial (/.function/abstraction [environment actual body]) tail)) + (if (n.= expected actual) + (do try.monad + [output (..result parser (list body))] + {try.#Success [tail [environment output]]}) + (exception.except ..wrong_arity [expected actual])) + + _ + (exception.except ..cannot_parse input)))) + +(def: .public (loop init_parsers iteration_parser) + (All (_ a b) (-> (Parser a) (Parser b) (Parser [Register a b]))) + (.function (_ input) + (case input + (pattern (list.partial (/.loop/scope [start inits iteration]) tail)) + (do try.monad + [inits (..result init_parsers inits) + iteration (..result iteration_parser (list iteration))] + {try.#Success [tail [start inits iteration]]}) + + _ + (exception.except ..cannot_parse input)))) |