(.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
    ["[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]]]]]
 ["[0]" // (.open: "[1]#[0]" monad)])

(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]]))))))