MWE.lean

inductive hprod (f : Type → Type) : list Type → Type 1
| nil : hprod []
| cons {α αs} (x : f α) (xs : hprod αs) : hprod (α :: αs)

namespace hprod
variable {f : Type → Type}

notation `⟦` l:(foldr `, ` (h t, cons h t) nil `⟧`) := l

protected def pure (x : ∀{β}, f β) : ∀{αs}, hprod f αs
| [] := nil
| (α::αs) := cons x pure

def head {α αs} : hprod f (α::αs) → f α
| (cons x _) := x

def tail {α αs} : hprod f (α::αs) → hprod f αs
| (cons _ xs) := xs

end hprod

def parser (α : Type) :=
list char → list (list char × α)

namespace parser
variables {α β : Type}

protected def pure (value : α) : parser α :=
λ input, [⟨input, value⟩]

protected def bind (p : parser α) (f : α → parser β) : parser β :=
λ input₁, do ⟨input₂, value⟩ ← p input₁, f value input₂

protected def failure : parser α :=
λ _, []

protected def orelse (p q : parser α) : parser α :=
λ input, p input ++ q input

instance : monad parser :=
{ pure := @parser.pure, bind := @parser.bind }

instance : alternative parser :=
{ failure := @parser.failure, orelse := @parser.orelse }

def sat (pred : char → Prop) [decidable_pred pred] : parser char
| [] := []
| (c::input) := do guard (pred c), pure ⟨input, c⟩

def sat_option (pred : char → option α) : parser α
| [] := []
| (c::input) :=
  match pred c with
  | some x := [⟨input, x⟩]
  | none := []
  end

def any_char : parser char :=
sat (λ_, tt)

def ch (c : char) : parser char :=
sat (= c)

def ch' (c : char) : parser unit :=
ch c $> ⟨⟩

def one_of (cs : list char) : parser char :=
sat (∈ cs)

def str (s : string) : parser unit :=
s.to_list.mmap' ch

def eof : parser unit
| [] := [⟨[], ⟨⟩⟩]
| _ := failure

private def fixN_core {αs} (f : hprod parser αs → hprod parser αs) : ℕ → hprod parser αs  
| 0 := hprod.pure @parser.failure
| (n + 1) := f (fixN_core n)

def fixN : ∀{αs}, (hprod parser αs → hprod parser αs) → hprod parser αs
| [] f := hprod.nil
| (α::αs) f :=
  hprod.cons
    (λ input, (fixN_core f (input.length + 1)).head input)
    (fixN (hprod.tail ∘ f ∘ hprod.cons failure))

private def fix_core (f : parser α → parser α) : ℕ → parser α
| 0 := failure
| (n + 1) := f (fix_core n)

def fix (f : parser α → parser α) : parser α :=
λ input, fix_core f (input.length + 1) input

private def foldr_core (f : α → β → β) (p : parser α) (b : β) : ℕ → parser β
| 0 := failure
| (n + 1) := (do x ← p, xs ← foldr_core n, pure (f x xs)) <|> pure b

def foldr (f : α → β → β) (p : parser α) (b : β) : parser β :=
λ input, foldr_core f p b (input.length + 1) input

def many (p : parser α) : parser (list α) :=
foldr (::) p []

def some (p : parser α) : parser (list α) :=
do x ← p, xs ← many p, pure (x :: xs)

def sep_by1 (sep : parser unit) (p : parser α) : parser (list α) :=
do x ← p, xs ← many (sep >> p), pure (x :: xs)

def sep_by (sep : parser unit) (p : parser α) : parser (list α) :=
sep_by1 sep p <|> pure []

def between (before after : parser β) (p : parser α) : parser α :=
  before *> p <* after

def digit : parser ℕ :=
do c ← sat char.is_digit, pure (c.to_nat - '0'.to_nat)

def nat : parser ℕ :=
list.foldl (λn digit, n * 10 + digit) 0 <$> some digit

def run (p : parser α) (input : string) : option α :=
prod.snd <$> ((p <* eof) input.to_list).nth 0

end parser

namespace MWE
open parser

def parsers : hprod parser [list char, list char] :=
fixN $ λ parsers, match parsers with | ⟦a, b⟧ :=
⟦ -- a
  (::) <$> ch 'a' <*> (b <|> eof $> [])
, -- b
  (::) <$> ch 'b' <*> (a <|> eof $> [])
⟧
end

def abab := list.as_string <$> (parsers.head <|> parsers.tail.head)

#eval abab.run "abab"

end MWE

-- namespace aeson
--   open parser
  
--   inductive value
--   | string : string → value
--   | object : list (string × value) → value
--   | array : list value → value
--   | number : ℕ → value
--   | bool : bool → value
--   | null : value

--   meta def value.repr : value → string
--   | (value.string s) := repr s
--   | (value.object members) := repr (prod.map id value.repr <$> members)
--   | (value.array elements) := repr (value.repr <$> elements)
--   | (value.number n) := repr n
--   | (value.bool b) := repr b
--   | value.null := "null"

--   meta instance : has_repr value := ⟨value.repr⟩

--   def ws :=
--   optional (one_of (char.of_nat <$> [9, 10, 13, 32])) $> ()
  
--   def hex :=
--   digit <|>
--   (λ c, char.to_nat c - 'a'.to_nat) <$> one_of ['a', 'b', 'c', 'd', 'e', 'f'] <|>
--   (λ c, char.to_nat c - 'A'.to_nat) <$> one_of ['A', 'B', 'C', 'D', 'E', 'F']

--   def escape_char : char → option char
--   | '"' := some '"'
--   | '\\' := some '\\'
--   | '/' := some '/'
--   | 'n' := some '\n'
--   | 't' := some '\t'
--   -- todo: b, f, r
--   | _ := none

--   def escape :=
--   sat_option escape_char <|>
--   do ch 'u', digits <- monad.sequence [hex, hex, hex, hex],
--      pure (char.of_nat (digits.foldl (λ n d, n * 16 + d) 0))

--   def character :=
--   sat (λ x, x ≠ '\\' ∧ x ≠ '"') <|>
--   ch '\\' *> escape

--   def characters :=
--   list.as_string <$> many character

--   def stringP :=
--   ch '"' *> characters <* ch '"'

--   def parsers : hprod parser
--     [ value -- element
--     , list value -- elements
--     , value -- value
--     , list (string × value) -- object
--     , string × value -- member
--     , list (string × value) -- members
--     , list value -- array
--     ] :=
--   fixN $ λp, match p with
--   | ⟦element, elements, valueP, object, member, members, array⟧ :=
--     ⟦ -- element
--       ws *> valueP <* ws
--     , -- elements
--       sep_by1 (ch' ',') element
--     , --value
--       value.object <$> object <|>
--       value.array <$> array <|>
--       value.string <$> stringP <|>
--       value.number <$> nat <|>
--       value.bool true <$ str "true" <|>
--       value.bool false <$ str "false" <|>
--       value.null <$ str "null"
--     , -- object
--       [] <$ (ch '{' *> ws <* ch '}') <|>
--       (ch '{' *> members <* ch '}')
--     , -- member
--       (do key <- ws *> stringP <* ws,
--          ch ':',
--          value <- element,
--          pure ⟨key, value⟩)
--     , -- members
--       sep_by1 (ch' ',') member
--     , -- array
--       [] <$ (ch '[' *> ws <* ch ']') <|>
--       (ch '[' *> elements <* ch ']')
--     ⟧
--   end

--   def json_parser : parser value := parsers.head

--   #eval json_parser.run "[{\"1\\n\\u0030\": 1}, 2]"
--     -- (some ["[(\"10\", \"1\")]", "2"])
-- end aeson