aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/parser
diff options
context:
space:
mode:
Diffstat (limited to 'stdlib/source/parser')
-rw-r--r--stdlib/source/parser/lux/data/binary.lux308
-rw-r--r--stdlib/source/parser/lux/tool/compiler/language/lux/synthesis.lux162
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))))