module Inky.Parser

import public Data.List.Quantifiers
import public Data.Nat

import Control.WellFounded
import Data.Bool
import Data.DPair
import Data.List
import Data.List1
import Data.So
import Data.String.Extra
import Inky.Context
import Inky.Thinning
import Text.Lexer

export
Interpolation Bounds where
  interpolate bounds = "\{show (1 + bounds.startLine)}:\{show bounds.startCol}--\{show (1 + bounds.endLine)}:\{show bounds.endCol}"

-- Parser Expressions ----------------------------------------------------------

export infixl 3 <**>, **>, <**
export infixr 2 <||>

public export
linUnless : Bool -> Context a -> Context a
linUnless False ctx = [<]
linUnless True ctx = ctx

public export
linUnlessLin : (0 a : Type) -> (b : Bool) -> linUnless {a} b [<] = [<]
linUnlessLin a False = Refl
linUnlessLin a True = Refl

public export
data Parser : (i : Type) -> (nil : Bool) -> (locked, free : Context (Bool, Type)) -> Type -> Type

public export
data ParserChain : (i : Type) -> (nil : Bool) -> (locked, free : Context (Bool, Type)) -> List Type -> Type

data Parser where
  Var : Var free (nil, a) -> Parser i nil locked free a
  Lit : (text : i) -> Parser i False locked free String
  Seq :
    ParserChain i nil locked free as ->
    Parser i nil locked free (HList as)
  OneOf :
    {nils : List Bool} ->
    All (\nil => Parser i nil locked free a) nils ->
    {auto 0 prf : length (filter Basics.id nils) `LTE` 1} ->
    Parser i (any Basics.id nils) locked free a
  Fix :
    (0 x : String) ->
    Parser i nil (locked :< (x :- (nil, a))) free a ->
    Parser i nil locked free a
  Map : (a -> b) -> Parser i nil locked free a -> Parser i nil locked free b
  WithBounds : Parser i nil locked free a -> Parser i nil locked free (WithBounds a)

data ParserChain where
  Nil : ParserChain i True locked free []
  (::) :
    {nil1, nil2 : Bool} ->
    Parser i nil1 locked free a ->
    ParserChain i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) as ->
    ParserChain i (nil1 && nil2) locked free (a :: as)

%name Parser p, q
%name ParserChain ps, qs

-- Weakening -------------------------------------------------------------------

public export
rename :
  locked1 `Thins` locked2 ->
  free1 `Thins` free2 ->
  {auto len : Length locked2} ->
  Parser i nil locked1 free1 a -> Parser i nil locked2 free2 a
public export
renameChain :
  locked1 `Thins` locked2 ->
  free1 `Thins` free2 ->
  {auto len : Length locked2} ->
  ParserChain i nil locked1 free1 a -> ParserChain i nil locked2 free2 a
public export
renameAll :
  locked1 `Thins` locked2 ->
  free1 `Thins` free2 ->
  {auto len : Length locked2} ->
  All.All (\nil => Parser i nil locked1 free1 a) nils ->
  All.All (\nil => Parser i nil locked2 free2 a) nils

rename f g (Var i) = Var (index g i)
rename f g (Lit text) = Lit text
rename f g (Seq ps) = Seq (renameChain f g ps)
rename f g (OneOf ps) = OneOf (renameAll f g ps)
rename f g (Fix x p) = Fix x (rename (Keep f) g p)
rename f g (Map h p) = Map h (rename f g p)
rename f g (WithBounds p) = WithBounds (rename f g p)

renameChain f g [] = []
renameChain f g ((::) {nil1 = False} p ps) = rename f g p :: renameChain Id (append g f) ps
renameChain f g ((::) {nil1 = True} p ps) = rename f g p :: renameChain f g ps

renameAll f g [] = []
renameAll f g (p :: ps) = rename f g p :: renameAll f g ps

public export
weaken :
  (len1 : Length free2) ->
  {auto len2 : Length locked} ->
  Parser i nil (free2 ++ locked) free1 a -> Parser i nil locked (free1 ++ free2) a
public export
weakenChain :
  (len1 : Length free2) ->
  {auto len2 : Length locked} ->
  ParserChain i nil (free2 ++ locked) free1 a -> ParserChain i nil locked (free1 ++ free2) a
public export
weakenAll :
  (len1 : Length free2) ->
  {auto len2 : Length locked} ->
  All.All (\nil => Parser i nil (free2 ++ locked) free1 a) nils ->
  All.All (\nil => Parser i nil locked (free1 ++ free2) a) nils

weaken len1 (Var x) = Var (wknL x)
weaken len1 (Lit text) = Lit text
weaken len1 (Seq ps) = Seq (weakenChain len1 ps)
weaken len1 (OneOf ps) = OneOf (weakenAll len1 ps)
weaken len1 (Fix x p) = Fix x (weaken len1 p)
weaken len1 (Map f p) = Map f (weaken len1 p)
weaken len1 (WithBounds p) = WithBounds (weaken len1 p)

weakenChain len1 [] = []
weakenChain len1 ((::) {nil1 = False} p ps) = weaken len1 p :: renameChain Id (assoc len2) ps
weakenChain len1 ((::) {nil1 = True} p ps) = weaken len1 p :: weakenChain len1 ps

weakenAll len1 [] = []
weakenAll len1 (p :: ps) = weaken len1 p :: weakenAll len1 ps

-- Typing ----------------------------------------------------------------------

-- Lists are sufficient, as we assume each symbol appears once.
-- TODO: switch to some efficient tree?

public export
peek :
  (env : All (const (List i)) free) ->
  Parser i nil locked free a -> List i
public export
peekChain :
  (env : All (const (List i)) free) ->
  ParserChain i nil locked free a -> List i
public export
peekAll :
  (env : All (const (List i)) free) ->
  All.All (\nil => Parser i nil locked free a) nils ->
  All.All (const $ List i) nils

peek env (Var x) = indexAll x env
peek env (Lit text) = [text]
peek env (Seq ps) = peekChain env ps
peek env (OneOf ps) = concat (forget $ peekAll env ps)
peek env (Fix x p) = peek env p
peek env (Map f p) = peek env p
peek env (WithBounds p) = peek env p

peekChain env [] = []
peekChain env ((::) {nil1 = False} p ps) = peek env p
peekChain env ((::) {nil1 = True} p ps) = peek env p ++ peekChain env ps

peekAll env [] = []
peekAll env (p :: ps) = peek env p :: peekAll env ps

public export
follow :
  (penv1 : All (const (List i)) locked) ->
  (penv2 : All (const (List i)) free) ->
  (fenv1 : All (const (List i)) locked) ->
  (fenv2 : All (const (List i)) free) ->
  Parser i nil locked free a -> List i
public export
followChain :
  (penv1 : All (const (List i)) locked) ->
  (penv2 : All (const (List i)) free) ->
  (fenv1 : All (const (List i)) locked) ->
  (fenv2 : All (const (List i)) free) ->
  ParserChain i nil locked free a -> List i
public export
followAll :
  (penv1 : All (const (List i)) locked) ->
  (penv2 : All (const (List i)) free) ->
  (fenv1 : All (const (List i)) locked) ->
  (fenv2 : All (const (List i)) free) ->
  All.All (\nil => Parser i nil locked free a) nils -> List i

follow penv1 penv2 fenv1 fenv2 (Var x) = indexAll x fenv2
follow penv1 penv2 fenv1 fenv2 (Lit text) = []
follow penv1 penv2 fenv1 fenv2 (Seq ps) = followChain penv1 penv2 fenv1 fenv2 ps
follow penv1 penv2 fenv1 fenv2 (OneOf ps) = followAll penv1 penv2 fenv1 fenv2 ps
follow penv1 penv2 fenv1 fenv2 (Fix x p) =
  -- Conjecture: The fix point converges after one step
  -- Proof:
  --   - we always add information
  --   - no step depends on existing information
  follow (penv1 :< (x :- peek penv2 p)) penv2 (fenv1 :< (x :- empty)) fenv2 p
follow penv1 penv2 fenv1 fenv2 (Map f p) = follow penv1 penv2 fenv1 fenv2 p
follow penv1 penv2 fenv1 fenv2 (WithBounds p) = follow penv1 penv2 fenv1 fenv2 p

followChain penv1 penv2 fenv1 fenv2 [] = []
followChain penv1 penv2 fenv1 fenv2 ((::) {nil1 = False, nil2} p ps) =
  (if nil2
  then peekChain (penv2 ++ penv1) ps ++ follow penv1 penv2 fenv1 fenv2 p
  else []) ++
  followChain [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1) ps
followChain penv1 penv2 fenv1 fenv2 ((::) {nil1 = True, nil2} p ps) =
  (if nil2
  then peekChain penv2 ps ++ follow penv1 penv2 fenv1 fenv2 p
  else []) ++
  followChain penv1 penv2 fenv1 fenv2 ps

followAll penv1 penv2 fenv1 fenv2 [] = []
followAll penv1 penv2 fenv1 fenv2 (p :: ps) =
  follow penv1 penv2 fenv1 fenv2 p ++
  followAll penv1 penv2 fenv1 fenv2 ps

public export
all' : (a -> Bool) -> List a -> Bool
all' f [] = True
all' f (x :: xs) = f x && all' f xs

allTrue : (xs : List a) -> all' (const True) xs = True
allTrue [] = Refl
allTrue (x :: xs) = allTrue xs

public export
disjoint : Eq a => List (List a) -> Bool
disjoint [] = True
disjoint (xs :: xss) = all' (\ys => all' (\x => not (x `elem` ys)) xs) xss && disjoint xss

namespace WellTyped
  public export
  wellTyped :
    (e : Eq i) ->
    (penv1 : All (const (List i)) locked) ->
    (penv2 : All (const (List i)) free) ->
    (fenv1 : All (const (List i)) locked) ->
    (fenv2 : All (const (List i)) free) ->
    Parser i nil locked free a ->
    Bool
  public export
  wellTypedChain :
    (e : Eq i) ->
    (penv1 : All (const (List i)) locked) ->
    (penv2 : All (const (List i)) free) ->
    (fenv1 : All (const (List i)) locked) ->
    (fenv2 : All (const (List i)) free) ->
    ParserChain i nil locked free a ->
    Bool
  public export
  allWellTyped :
    (e : Eq i) ->
    (penv1 : All (const (List i)) locked) ->
    (penv2 : All (const (List i)) free) ->
    (fenv1 : All (const (List i)) locked) ->
    (fenv2 : All (const (List i)) free) ->
    All.All (\nil => Parser i nil locked free a) nils ->
    Bool

  wellTyped e penv1 penv2 fenv1 fenv2 (Var i) = True
  wellTyped e penv1 penv2 fenv1 fenv2 (Lit txt) = True
  wellTyped e penv1 penv2 fenv1 fenv2 (Seq ps) = wellTypedChain e penv1 penv2 fenv1 fenv2 ps
  wellTyped e penv1 penv2 fenv1 fenv2 (OneOf {nils, prf} ps) =
    disjoint (forget $ peekAll penv2 ps) && allWellTyped e penv1 penv2 fenv1 fenv2 ps
  wellTyped e penv1 penv2 fenv1 fenv2 (Fix x p) =
    wellTyped e
      (penv1 :< (x :- peek penv2 p))
      penv2
      (fenv1 :< (x :- follow (penv1 :< (x :- peek penv2 p)) penv2 (fenv1 :< (x :- [])) fenv2 p))
      fenv2
      p
  wellTyped e penv1 penv2 fenv1 fenv2 (Map f p) = wellTyped e penv1 penv2 fenv1 fenv2 p
  wellTyped e penv1 penv2 fenv1 fenv2 (WithBounds p) = wellTyped e penv1 penv2 fenv1 fenv2 p

  wellTypedChain e penv1 penv2 fenv1 fenv2 [] = True
  wellTypedChain e penv1 penv2 fenv1 fenv2 ((::) {nil1 = False} p ps) =
    disjoint [follow penv1 penv2 fenv1 fenv2 p, peekChain (penv2 ++ penv1) ps] &&
    wellTyped e penv1 penv2 fenv1 fenv2 p &&
    wellTypedChain e [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1) ps
  wellTypedChain e penv1 penv2 fenv1 fenv2 ((::) {nil1 = True} p ps) =
    disjoint [follow penv1 penv2 fenv1 fenv2 p, peekChain penv2 ps] &&
    wellTyped e penv1 penv2 fenv1 fenv2 p &&
    wellTypedChain e penv1 penv2 fenv1 fenv2 ps

  allWellTyped e penv1 penv2 fenv1 fenv2 [] = True
  allWellTyped e penv1 penv2 fenv1 fenv2 (p :: ps) =
    wellTyped e penv1 penv2 fenv1 fenv2 p &&
    allWellTyped e penv1 penv2 fenv1 fenv2 ps

-- Parsing Function ------------------------------------------------------------

-- Utilty for recursion

public export
data SmallerX : Bool -> List a -> List a -> Type where
  Strict : {0 xs, ys : List a} -> xs `Smaller` ys -> SmallerX False xs ys
  Lax : {0 xs, ys : List a} -> size xs `LTE` size ys -> SmallerX True xs ys

transX :
  {xs, ys, zs : List a} ->
  SmallerX b1 xs ys -> SmallerX b2 ys zs -> SmallerX (b1 && b2) xs zs
transX (Strict prf1) (Strict prf2) = Strict (transitive prf1 (lteSuccLeft prf2))
transX (Strict prf1) (Lax prf2) = Strict (transitive prf1 prf2)
transX (Lax prf1) (Strict prf2) = Strict (transitive (LTESucc prf1) prf2)
transX (Lax prf1) (Lax prf2) = Lax (transitive prf1 prf2)

ofSmaller : {b : Bool} -> {0 xs, ys : List a} -> xs `Smaller` ys -> SmallerX b xs ys
ofSmaller {b = False} prf = Strict prf
ofSmaller {b = True} prf = Lax (lteSuccLeft prf)

wknSmallerL : SmallerX b1 xs ys -> (b2 : Bool) -> SmallerX (b1 || b2) xs ys
wknSmallerL (Strict prf) _ = ofSmaller prf
wknSmallerL (Lax prf) _ = Lax prf

wknSmallerR : (b1 : Bool) -> SmallerX b2 xs ys -> SmallerX (b1 || b2) xs ys
wknSmallerR b1 (Strict prf) =
  if b1 then ofSmaller prf else ofSmaller prf
wknSmallerR b1 (Lax prf) =
  if b1 then Lax prf else Lax prf

forget : SmallerX b xs ys -> SmallerX True xs ys
forget = wknSmallerR True

toSmaller : {xs, ys : List a} -> (0 _ : SmallerX False xs ys) -> xs `Smaller` ys
toSmaller {xs = []} {ys = []} (Strict prf) impossible
toSmaller {xs = []} {ys = (y :: ys)} (Strict prf) = LTESucc LTEZero
toSmaller {xs = (x :: xs)} {ys = []} (Strict prf) impossible
toSmaller {xs = (x :: xs)} {ys = (y :: ys)} (Strict (LTESucc prf)) = LTESucc (toSmaller (Strict prf))

anyCons : (b : Bool) -> (bs : List Bool) -> any Basics.id (b :: bs) = b || any Basics.id bs
anyCons b [] = sym (orFalseNeutral b)
anyCons b (b' :: bs) =
  trans (anyCons (b || b') bs) $
  trans (sym $ orAssociative b b' (any id bs))
        (cong (b ||) (sym $ anyCons b' bs))

anyTrue : (bs : List Bool) -> any Basics.id (True :: bs) = True
anyTrue = anyCons True

-- Return Type

namespace M
  public export
  data M : List a -> Bool -> Type -> Type where
    Err : String -> M xs nil b
    Ok : (res : b) -> (ys : List a) -> (0 prf : SmallerX nil ys xs) -> M xs nil b

  export
  Functor (M xs nil) where
    map f (Err msg) = Err msg
    map f (Ok res ys prf) = Ok (f res) ys prf

  export
  wknL : M xs b1 a -> (b2 : Bool) -> M xs (b1 || b2) a
  wknL (Err msg) b2 = Err msg
  wknL (Ok res ys prf) b2 = Ok res ys (wknSmallerL prf b2)

  export
  wknR : (b1 : Bool) -> M xs b2 a -> M xs (b1 || b2) a
  wknR b1 (Err msg) = Err msg
  wknR b1 (Ok res ys prf) = Ok res ys (wknSmallerR b1 prf)

  export
  anyL :
    (b : Bool) -> {0 bs : List Bool} ->
    M xs (any Basics.id bs) a -> M xs (any Basics.id (b :: bs)) a
  anyL b m = rewrite anyCons b bs in wknR b m

  export
  anyR : (bs : List Bool) -> M xs b a -> M xs (any Basics.id (b :: bs)) a
  anyR bs m = rewrite anyCons b bs in wknL m (any id bs)

-- The Big Function

data FirstNil : List Bool -> Type where
  Here : FirstNil (True :: bs)
  There : FirstNil bs -> FirstNil (False :: bs)

findNil : (nils : List Bool) -> Maybe (FirstNil nils)
findNil [] = Nothing
findNil (False :: bs) = There <$> findNil bs
findNil (True :: bs) = Just Here

memberOf : Eq a => (x : a) -> All.All (const $ List a) xs -> Maybe (Any (const ()) xs)
memberOf x [] = Nothing
memberOf x (xs :: xss) =
  if x `elem` xs
  then Just (Here ())
  else There <$> (x `memberOf` xss)

parser :
  (e : Eq i) => Interpolation i =>
  (p : Parser i nil locked free a) ->
  (penv1 : _) ->
  (penv2 : _) ->
  (fenv1 : _) ->
  (fenv2 : _) ->
  {auto 0 wf : So (wellTyped e penv1 penv2 fenv1 fenv2 p)} ->
  (xs : List (WithBounds (Token i))) ->
  All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x) locked ->
  All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x) free ->
  M xs nil a
parserChain :
  (e : Eq i) => Interpolation i =>
  (ps : ParserChain i nil locked free as) ->
  (penv1 : _) ->
  (penv2 : _) ->
  (fenv1 : _) ->
  (fenv2 : _) ->
  {auto 0 wf : So (wellTypedChain e penv1 penv2 fenv1 fenv2 ps)} ->
  (xs : List (WithBounds (Token i))) ->
  All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x) locked ->
  All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x) free ->
  M xs nil (HList as)
parserNil :
  (e : Eq i) => Interpolation i =>
  (at : FirstNil nils) ->
  (ps : All (\nil => Parser i nil locked free a) nils) ->
  (penv1 : _) ->
  (penv2 : _) ->
  (fenv1 : _) ->
  (fenv2 : _) ->
  {auto 0 wf : So (allWellTyped e penv1 penv2 fenv1 fenv2 ps)} ->
  (xs : List (WithBounds (Token i))) ->
  All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x) locked ->
  All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x) free ->
  M xs (any Basics.id nils) a
parserOneOf :
  (e : Eq i) => Interpolation i =>
  {nils : List Bool} ->
  (at : Any (const ()) nils) ->
  (ps : All (\nil => Parser i nil locked free a) nils) ->
  (penv1 : _) ->
  (penv2 : _) ->
  (fenv1 : _) ->
  (fenv2 : _) ->
  {auto 0 wf : So (allWellTyped e penv1 penv2 fenv1 fenv2 ps)} ->
  (xs : List1 (WithBounds (Token i))) ->
  All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys (forget xs)) -> uncurry (M ys) x) locked ->
  All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys (forget xs)) -> uncurry (M ys) x) free ->
  M (forget xs) (any Basics.id nils) a

parser (Var x) penv1 penv2 fenv1 fenv2 xs env1 env2 =
  indexAll x env2 xs (Lax reflexive)
parser (Lit text) penv1 penv2 fenv1 fenv2 xs env1 env2 =
  case xs of
    [] => Err "expected \{text}, got end of file"
    y :: ys =>
      if y.val.kind == text
      then Ok y.val.text ys (Strict reflexive)
      else Err "\{y.bounds}: expected \{text}, got \{y.val.kind}"
parser (Seq ps) penv1 penv2 fenv1 fenv2 xs env1 env2 =
  parserChain ps penv1 penv2 fenv1 fenv2 xs env1 env2
parser (OneOf {nils} ps) penv1 penv2 fenv1 fenv2 [] env1 env2 {wf} =
  let 0 wfs = soAnd {a = disjoint (forget $ peekAll penv2 ps)} wf in
  case findNil nils of
    Nothing => Err "unexpected end of input"
    Just at => parserNil at ps penv1 penv2 fenv1 fenv2 [] env1 env2
parser (OneOf {nils} ps) penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2 {wf = wf} =
  let 0 wfs = soAnd {a = disjoint (forget $ peekAll penv2 ps)} wf in
  let sets = peekAll penv2 ps in
  case x.val.kind `memberOf` sets of
    Just at => parserOneOf at ps penv1 penv2 fenv1 fenv2 (x ::: xs) env1 env2
    Nothing => case findNil nils of
      Nothing =>
        Err
          "\{x.bounds}: expected one of: \{join ", " $ map (\k => "\{k}") $ concat $ forget sets}; got \{x.val.kind}"
      Just at => parserNil at ps penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2
parser (Fix {a, nil} x p) penv1 penv2 fenv1 fenv2 xs env1 env2 =
  let f = parser p _ _ _ _ {wf} in
  let
    res : M xs nil a
    res =
      sizeInd {P = \ys => (0 prf : SmallerX True ys xs) -> M ys nil a}
        (\ys, rec, lte =>
          f ys
            (  mapProperty (\f, zs, 0 prf => f zs $ transX prf lte) env1
            :< (x :- (\zs, prf => rec zs (toSmaller prf) (forget $ transX prf lte)))
            )
            (mapProperty (\f, zs, prf => f zs $ transX prf lte) env2))
        xs
        (Lax reflexive)
  in
  res
parser (Map f p) penv1 penv2 fenv1 fenv2 xs env1 env2 =
  f <$> parser p penv1 penv2 fenv1 fenv2 xs env1 env2
parser (WithBounds p) penv1 penv2 fenv1 fenv2 xs env1 env2 =
  case xs of
    [] => irrelevantBounds <$> parser p penv1 penv2 fenv1 fenv2 [] env1 env2
    (x :: xs) =>
      (\y => MkBounded y x.isIrrelevant x.bounds) <$>
      parser p penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2

parserChain [] penv1 penv2 fenv1 fenv2 xs env1 env2 = Ok [] xs (Lax reflexive)
parserChain ((::) {nil1 = False, nil2} p ps) penv1 penv2 fenv1 fenv2 xs env1 env2 =
  let 0 wfs = soAnd wf in
  let 0 wfs' = soAnd (snd wfs) in
  case parser p penv1 penv2 fenv1 fenv2 xs env1 env2 of
    Err msg => Err msg
    Ok x ys lt =>
      case
        parserChain ps [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1)
          ys
          [<]
          (  mapProperty (\f, zs, 0 prf => f zs $ forget $ transX prf lt) env2
          ++ mapProperty (\f, zs, 0 prf => f zs $ transX prf lt) env1
          )
      of
        Err msg => Err msg
        Ok y zs prf => Ok (x :: y) zs (rewrite sym $ andFalseFalse nil2 in transX prf lt)
parserChain ((::) {nil1 = True, nil2} p ps) penv1 penv2 fenv1 fenv2 xs env1 env2 =
  let 0 wfs = soAnd wf in
  let 0 wfs' = soAnd (snd wfs) in
  case parser p penv1 penv2 fenv1 fenv2 xs env1 env2 of
    Err msg => Err msg
    Ok x ys lte =>
      case
        parserChain ps penv1 penv2 fenv1 fenv2
          ys
          (mapProperty (\f, zs, prf => f zs $ transX prf lte) env1)
          (mapProperty (\f, zs, prf => f zs $ transX prf lte) env2)
      of
        Err msg => Err msg
        Ok y zs prf => Ok (x :: y) zs (rewrite sym $ andTrueNeutral nil2 in transX prf lte)

parserNil {nils = True :: nils} Here (p :: ps) penv1 penv2 fenv1 fenv2 xs env1 env2 =
  let 0 wfs = soAnd wf in
  rewrite anyTrue nils in
  parser p penv1 penv2 fenv1 fenv2 xs env1 env2
parserNil (There at) (p :: ps) penv1 penv2 fenv1 fenv2 xs env1 env2 =
  let 0 wfs = soAnd {a = wellTyped e penv1 penv2 fenv1 fenv2 p} wf in
  parserNil at ps penv1 penv2 fenv1 fenv2 xs env1 env2

parserOneOf {nils = nil :: nils} (Here ()) (p :: ps) penv1 penv2 fenv1 fenv2 xs env1 env2 =
  let 0 wfs = soAnd wf in
  anyR nils (parser p penv1 penv2 fenv1 fenv2 (forget xs) env1 env2)
parserOneOf {nils = nil :: nils} (There at) (p :: ps) penv1 penv2 fenv1 fenv2 xs env1 env2 =
  let 0 wfs = soAnd {a = wellTyped e penv1 penv2 fenv1 fenv2 p} wf in
  anyL nil (parserOneOf at ps penv1 penv2 fenv1 fenv2 xs env1 env2)

export
parse :
  (e : Eq i) => Interpolation i =>
  (p : Parser i nil [<] [<] a) ->
  {auto 0 wf : So (wellTyped e [<] [<] [<] [<] p)} ->
  (xs : List (WithBounds (Token i))) -> M xs nil a
parse p xs = parser p [<] [<] [<] [<] xs [<] [<]

-- Functor ---------------------------------------------------------------------

public export
(++) :
  {nil2 : Bool} ->
  ParserChain i nil1 locked free as ->
  ParserChain i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) bs ->
  ParserChain i (nil1 && nil2) locked free (as ++ bs)
[] ++ qs = qs
((::) {nil1 = False, nil2} p ps) ++ qs =
  p ::
  (  ps
  ++ rewrite linUnlessLin (Bool, Type) nil2 in
     rewrite linUnlessLin (Bool, Type) (not nil2) in
     qs)
((::) {nil1 = True, nil2} p ps) ++ qs = p :: (ps ++ qs)

public export
(<**>) :
  {nil1, nil2 : Bool} ->
  Parser i nil1 locked free a ->
  Parser i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) b ->
  Parser i (nil1 && nil2) locked free (a, b)
p <**> Seq ps = Map (\(x :: xs) => (x, xs)) $ Seq (p :: ps)
-- HACK: andTrueNeutral isn't public, so do a full case split.
(<**>) {nil1 = True, nil2 = True} p q = Map (\[x, y] => (x, y)) $ Seq [p, q]
(<**>) {nil1 = True, nil2 = False} p q = Map (\[x, y] => (x, y)) $ Seq [p, q]
(<**>) {nil1 = False, nil2 = True} p q = Map (\[x, y] => (x, y)) $ Seq [p, q]
(<**>) {nil1 = False, nil2 = False} p q = Map (\[x, y] => (x, y)) $ Seq [p, q]

public export
Functor (Parser i nil locked free) where
  map f (Map g p) = Map (f . g) p
  map f p = Map f p

public export
Applicative (Parser i True locked free) where
  pure x = map (const x) (Seq [])
  p <*> q = map (\(f, x) => f x) (p <**> q)

-- Combinator ------------------------------------------------------------------

public export
(<|>) :
  {nil1, nil2 : Bool} ->
  Parser i nil1 locked free a ->
  Parser i nil2 locked free a ->
  {auto 0 prf : length (filter Basics.id [nil1, nil2]) `LTE` 1} ->
  Parser i (nil1 || nil2) locked free a
p <|> q = OneOf [p, q]

public export
(<||>) :
  {nil1, nil2 : Bool} ->
  Parser i nil1 locked free a ->
  Parser i nil2 locked free b ->
  {auto 0 prf : length (filter Basics.id [nil1, nil2]) `LTE` 1} ->
  Parser i (nil1 || nil2) locked free (Either a b)
p <||> q = Left <$> p <|> Right <$> q

public export
(**>) :
  {nil1, nil2 : Bool} ->
  Parser i nil1 locked free a ->
  Parser i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) b ->
  Parser i (nil1 && nil2) locked free b
p **> q = snd <$> (p <**> q)

public export
(<**) :
  {nil1, nil2 : Bool} ->
  Parser i nil1 locked free a ->
  Parser i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) b ->
  Parser i (nil1 && nil2) locked free a
p <** q = fst <$> (p <**> q)

public export
match : TokenKind i => (kind : i) -> Parser i False locked free (TokType kind)
match kind = Map (tokValue kind) $ Lit kind

public export
enclose :
  {b1, b2, b3 : Bool} ->
  (left : Parser i b1 locked free ()) ->
  (right :
    Parser i b3
      (linUnless b2 (linUnless b1 locked))
      ((free ++ linUnless (not b1) locked) ++ linUnless (not b2) (linUnless b1 locked))
      ()) ->
  Parser i b2 (linUnless b1 locked) (free ++ linUnless (not b1) locked) a ->
  Parser i (b1 && b2 && b3 && True) locked free a
enclose left right p = (\[_, x, _] => x) <$> Seq {as = [(), a, ()]} [left, p, right]

public export
option : Parser i False locked free a -> Parser i True locked free (Maybe a)
option p = (Just <$> p) <|> pure Nothing

public export
plus :
  {auto len : Length locked} ->
  Parser i False locked free a ->
  Parser i False locked free (List1 a)
plus p =
  Fix "plus"
    (   uncurry (:::)
    <$> (rename (Drop Id) Id p <**> maybe [] forget <$> option (Var $ %% "plus")))

public export
star :
  {auto len : Length locked} ->
  Parser i False locked free a ->
  Parser i True locked free (List a)
star p = maybe [] forget <$> option (plus p)

public export
sepBy1 :
  {auto len : Length locked} ->
  (sep : Parser i False locked free ()) ->
  Parser i False locked free a ->
  Parser i False locked free (List1 a)
sepBy1 sep p = uncurry (:::) <$> (p <**> star (weaken len sep **> weaken len p))

public export
sepBy :
  {auto len : Length locked} ->
  (sep : Parser i False locked free ()) ->
  Parser i False locked free a ->
  Parser i True locked free (List a)
sepBy sep p = maybe [] forget <$> option (sepBy1 sep p)