Add compilation to scheme.

Extract parser as an independent project.

1 files changed, 0 insertions, 733 deletions

diff --git a/src/Inky/Parser.idr b/src/Inky/Parser.idr
deleted file mode 100644
index 94d8eb8..0000000
--- a/src/Inky/Parser.idr
+++ /dev/null
@@ -1,733 +0,0 @@
-module Inky.Parser
-
-import public Data.List.Quantifiers
-
-import Control.WellFounded
-import Data.Bool
-import Data.DPair
-import Data.List
-import Data.List1
-import Data.Nat
-import Data.So
-import Data.String.Extra
-import Inky.Data.Context
-import Inky.Data.Context.Var
-import Inky.Data.SnocList.Quantifiers
-import Inky.Data.SnocList.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 : LengthOf locked2} ->
-  Parser i nil locked1 free1 a -> Parser i nil locked2 free2 a
-public export
-renameChain :
-  locked1 `Thins` locked2 ->
-  free1 `Thins` free2 ->
-  {auto len : LengthOf locked2} ->
-  ParserChain i nil locked1 free1 a -> ParserChain i nil locked2 free2 a
-public export
-renameAll :
-  locked1 `Thins` locked2 ->
-  free1 `Thins` free2 ->
-  {auto len : LengthOf locked2} ->
-  {0 nils : List Bool} ->
-  All (\nil => Parser i nil locked1 free1 a) nils ->
-  All (\nil => Parser i nil locked2 free2 a) nils
-
-rename f g (Var i) = Var (toVar $ indexPos g i.pos)
-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 : LengthOf free2) ->
-  {auto len2 : LengthOf locked} ->
-  Parser i nil (free2 ++ locked) free1 a -> Parser i nil locked (free1 ++ free2) a
-public export
-weakenChain :
-  (len1 : LengthOf free2) ->
-  {auto len2 : LengthOf locked} ->
-  ParserChain i nil (free2 ++ locked) free1 a -> ParserChain i nil locked (free1 ++ free2) a
-public export
-weakenAll :
-  (len1 : LengthOf free2) ->
-  {auto len2 : LengthOf locked} ->
-  {0 nils : List Bool} ->
-  All (\nil => Parser i nil (free2 ++ locked) free1 a) nils ->
-  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
-
--- Substitution ----------------------------------------------------------------
-
-public export
-sub :
-  {auto len : LengthOf locked2} ->
-  (f : All (Assoc0 $ (\nilA => Parser i (fst nilA) [<] (free2 ++ locked2) (snd nilA))) locked1) ->
-  (g : All (Assoc0 $ (\nilA => Parser i (fst nilA) locked2 free2 (snd nilA))) free1) ->
-  Parser i nil locked1 free1 a -> Parser i nil locked2 free2 a
-public export
-subChain :
-  {auto len : LengthOf locked2} ->
-  (f : All (Assoc0 $ (\nilA => Parser i (fst nilA) [<] (free2 ++ locked2) (snd nilA))) locked1) ->
-  (g : All (Assoc0 $ (\nilA => Parser i (fst nilA) locked2 free2 (snd nilA))) free1) ->
-  ParserChain i nil locked1 free1 a -> ParserChain i nil locked2 free2 a
-public export
-subAll :
-  {auto len : LengthOf locked2} ->
-  (f : All (Assoc0 $ (\nilA => Parser i (fst nilA) [<] (free2 ++ locked2) (snd nilA))) locked1) ->
-  (g : All (Assoc0 $ (\nilA => Parser i (fst nilA) locked2 free2 (snd nilA))) free1) ->
-  {0 nils : List Bool} ->
-  All (\nil => Parser i nil locked1 free1 a) nils -> All (\nil => Parser i nil locked2 free2 a) nils
-
-sub f g (Var x) = (indexAll x.pos g).value
-sub f g (Lit text) = Lit text
-sub f g (Seq ps) = Seq (subChain f g ps)
-sub f g (OneOf ps) = OneOf (subAll f g ps)
-sub f g (Fix x p) =
-  Fix x $
-  sub
-    (mapProperty (map $ rename Id (Drop Id)) f :< (x :- Var (%%% x)))
-    (mapProperty (map $ rename (Drop Id) Id) g)
-    p
-sub f g (Map h p) = Map h (sub f g p)
-sub f g (WithBounds p) = WithBounds (sub f g p)
-
-subChain f g [] = []
-subChain f g ((::) {nil1 = False} p ps) =
-  sub f g p ::
-  subChain [<] (mapProperty (map $ weaken len) g ++ f) ps
-subChain f g ((::) {nil1 = True} p ps) = sub f g p :: subChain f g ps
-
-subAll f g [] = []
-subAll f g (p :: ps) = sub f g p :: subAll f g ps
-
--- Typing ----------------------------------------------------------------------
-
--- Lists are sufficient, as we assume each symbol appears once.
--- TODO: switch to some efficient tree?
-
-public export
-peek :
-  (env : All (Assoc0 $ const $ List i) free) ->
-  Parser i nil locked free a -> List i
-public export
-peekChain :
-  (env : All (Assoc0 $ const $ List i) free) ->
-  ParserChain i nil locked free a -> List i
-public export
-peekAll :
-  (env : All (Assoc0 $ const $ List i) free) ->
-  {0 nils : List Bool} ->
-  All (\nil => Parser i nil locked free a) nils ->
-  All (const $ List i) nils
-
-peek env (Var x) = (indexAll x.pos env).value
-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 (Assoc0 $ const $ List i) locked) ->
-  (penv2 : All (Assoc0 $ const $ List i) free) ->
-  (fenv1 : All (Assoc0 $ const $ List i) locked) ->
-  (fenv2 : All (Assoc0 $ const $ List i) free) ->
-  Parser i nil locked free a -> List i
-public export
-followChain :
-  (penv1 : All (Assoc0 $ const $ List i) locked) ->
-  (penv2 : All (Assoc0 $ const $ List i) free) ->
-  (fenv1 : All (Assoc0 $ const $ List i) locked) ->
-  (fenv2 : All (Assoc0 $ const $ List i) free) ->
-  ParserChain i nil locked free a -> List i
-public export
-followAll :
-  (penv1 : All (Assoc0 $ const $ List i) locked) ->
-  (penv2 : All (Assoc0 $ const $ List i) free) ->
-  (fenv1 : All (Assoc0 $ const $ List i) locked) ->
-  (fenv2 : All (Assoc0 $ const $ List i) free) ->
-  {0 nils : List Bool} ->
-  All (\nil => Parser i nil locked free a) nils ->
-  List i
-
-follow penv1 penv2 fenv1 fenv2 (Var x) = (indexAll x.pos fenv2).value
-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 (Assoc0 $ const $ List i) locked) ->
-    (penv2 : All (Assoc0 $ const $ List i) free) ->
-    (fenv1 : All (Assoc0 $ const $ List i) locked) ->
-    (fenv2 : All (Assoc0 $ const $ List i) free) ->
-    Parser i nil locked free a ->
-    Bool
-  public export
-  wellTypedChain :
-    (e : Eq i) ->
-    (penv1 : All (Assoc0 $ const $ List i) locked) ->
-    (penv2 : All (Assoc0 $ const $ List i) free) ->
-    (fenv1 : All (Assoc0 $ const $ List i) locked) ->
-    (fenv2 : All (Assoc0 $ const $ List i) free) ->
-    ParserChain i nil locked free a ->
-    Bool
-  public export
-  allWellTyped :
-    (e : Eq i) ->
-    (penv1 : All (Assoc0 $ const $ List i) locked) ->
-    (penv2 : All (Assoc0 $ const $ List i) free) ->
-    (fenv1 : All (Assoc0 $ const $ List i) locked) ->
-    (fenv2 : All (Assoc0 $ const $ List i) free) ->
-    {0 nils : List Bool} ->
-    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
-  pure : {xs : List a} -> (x : b) -> M xs True b
-  pure x = Ok x xs (Lax reflexive)
-
-  export
-  (>>=) :
-    M xs nil b ->
-    (b -> {ys : List a} -> {auto 0 prf : SmallerX nil ys xs} -> M ys nil' c) ->
-    M xs (nil && nil') c
-  Err str >>= f = Err str
-  Ok res ys prf >>= f =
-    case f {ys, prf} res of
-      Err str => Err str
-      Ok res' zs prf' => Ok res' zs (rewrite andCommutative nil nil' in transX prf' prf)
-
-  export
-  take :
-    Eq a =>
-    Interpolation a =>
-    (toks : List a) ->
-    (xs : List (WithBounds (Token a))) ->
-    M xs False String
-  take [tok] [] = Err "expected \{tok}; got end of input"
-  take toks [] = Err "expected one of: \{join ", " $ map (\k => "\{k}") toks}; got end of input"
-  take toks (x :: xs) =
-    if x.val.kind `elem` toks
-    then Ok x.val.text xs (Strict reflexive)
-    else case toks of
-      [tok] => Err "\{x.bounds}: expected \{tok}; got \{x.val.kind}"
-      toks => Err "\{x.bounds}: expected one of: \{join ", " $ map (\k => "\{k}") toks}; got \{x.val.kind}"
-
-  export
-  bounds : (xs : List (WithBounds a)) -> M xs True (Bool, Bounds)
-  bounds [] = Ok (True, MkBounds (-1) (-1) (-1) (-1)) [] (Lax reflexive)
-  bounds (x :: xs) = Ok (x.isIrrelevant, x.bounds) (x :: xs) (Lax reflexive)
-
-  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
-
-||| Searches `sets` for the first occurence of `x`.
-||| On failure, returns the index for the nil element, if it exists.
-|||
-||| # Unsafe Invariants
-||| * `nils` has at most one `True` element
-||| * `sets` are disjoint
-lookahead :
-  Eq a =>
-  (x : Maybe a) ->
-  (nils : List Bool) ->
-  (sets : Lazy (All (const $ List a) nils)) ->
-  Maybe (Any (const ()) nils)
-lookahead x [] [] = Nothing
-lookahead x (nil :: nils) (set :: sets) =
-  (do
-    x <- x
-    if x `elem` set then Just (Here ()) else Nothing)
-  <|> There <$> lookahead x nils sets
-  <|> (if nil then Just (Here ()) else Nothing)
-
-parser :
-  (e : Eq i) => Interpolation i =>
-  (p : Parser i nil locked free a) ->
-  {penv1 : _} ->
-  {penv2 : _} ->
-  {0 fenv1 : _} ->
-  {0 fenv2 : _} ->
-  (0 wf : So (wellTyped e penv1 penv2 fenv1 fenv2 p)) ->
-  (xs : List (WithBounds (Token i))) ->
-  All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x)) locked ->
-  All (Assoc0 (\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 : _} ->
-  {0 fenv1 : _} ->
-  {0 fenv2 : _} ->
-  (0 wf : So (wellTypedChain e penv1 penv2 fenv1 fenv2 ps)) ->
-  (xs : List (WithBounds (Token i))) ->
-  All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x)) locked ->
-  All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x)) free ->
-  M xs nil (HList as)
-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 : _} ->
-  {0 fenv1 : _} ->
-  {0 fenv2 : _} ->
-  (0 wf : So (allWellTyped e penv1 penv2 fenv1 fenv2 ps)) ->
-  (xs : List (WithBounds (Token i))) ->
-  All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x)) locked ->
-  All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x)) free ->
-  M xs (any Basics.id nils) a
-
-parser (Var x) wf xs env1 env2 = (indexAll x.pos env2).value xs (Lax reflexive)
-parser (Lit text) wf xs env1 env2 = take [text] xs
-parser (Seq ps) wf xs env1 env2 =
-  parserChain ps wf xs env1 env2
-parser (OneOf {nils} ps) wf [] env1 env2 =
-  let 0 wfs = soAnd {a = disjoint (forget $ peekAll penv2 ps)} wf in
-  let sets = peekAll penv2 ps in
-  case lookahead Nothing nils sets of
-    Nothing => Err "unexpected end of input"
-    Just at => parserOneOf at ps (snd wfs) [] env1 env2
-parser (OneOf {nils} ps) wf (x :: xs) env1 env2 =
-  let 0 wfs = soAnd {a = disjoint (forget $ peekAll penv2 ps)} wf in
-  let sets = peekAll penv2 ps in
-  case lookahead (Just x.val.kind) nils sets of
-    Nothing => Err "\{x.bounds}: expected one of: \{join ", " $ map (\k => "\{k}") $ concat $ forget sets}; got \{x.val.kind}"
-    Just at => parserOneOf at ps (snd wfs) (x :: xs) env1 env2
-parser (Fix {a, nil} x p) wf xs env1 env2 =
-  let f = parser p wf in
-  sizeInd {P = \ys => (0 prf : SmallerX True ys xs) -> M ys nil a}
-    (\ys, rec, lte =>
-      f ys
-        (  mapProperty (map (\f, zs, 0 prf => f zs $ transX prf lte)) env1
-        :< (x :- (\zs, prf => rec zs (toSmaller prf) (forget $ transX prf lte)))
-        )
-        (mapProperty (map (\f, zs, prf => f zs $ transX prf lte)) env2))
-    xs (Lax reflexive)
-parser (Map f p) wf xs env1 env2 =
-  f <$> parser p wf xs env1 env2
-parser (WithBounds p) wf xs env1 env2 = do
-  (irrel, bounds) <- bounds xs
-  rewrite sym $ andTrueNeutral nil
-  x <- parser p wf _
-         (mapProperty (map (\f, zs, 0 prf => f zs $ transX {b2 = True} prf %search)) env1)
-         (mapProperty (map (\f, zs, 0 prf => f zs $ transX prf %search)) env2)
-  pure (MkBounded x irrel bounds)
-
-parserChain [] wf xs env1 env2 = Ok [] xs (Lax reflexive)
-parserChain ((::) {nil1 = False, nil2} p ps) wf xs env1 env2 =
-  let 0 wfs = soAnd wf in
-  let 0 wfs' = soAnd (snd wfs) in do
-    x <- parser p (fst wfs') xs env1 env2
-    y <- parserChain ps (snd wfs')
-          _
-          [<]
-          (  mapProperty (map (\f, zs, 0 prf => f zs $ forget $ transX {b2 = False} prf %search)) env2
-          ++ mapProperty (map (\f, zs, 0 prf => f zs $ transX prf %search)) env1
-          )
-    pure (x :: y)
-parserChain ((::) {nil1 = True, nil2} p ps) wf xs env1 env2 =
-  let 0 wfs = soAnd wf in
-  let 0 wfs' = soAnd (snd wfs) in do
-    x <- parser p (fst wfs') xs env1 env2
-    rewrite sym $ andTrueNeutral nil2
-    y <- parserChain ps (snd wfs')
-           _
-           (mapProperty (map (\f, zs, prf => f zs $ transX {b2 = True} prf %search)) env1)
-           (mapProperty (map (\f, zs, prf => f zs $ transX prf %search)) env2)
-    pure (x :: y)
-
-parserOneOf {nils = nil :: nils} (Here ()) (p :: ps) wf xs env1 env2 =
-  let 0 wfs = soAnd wf in
-  anyR nils (parser p (fst wfs) xs env1 env2)
-parserOneOf {nils = nil :: nils} (There at) (p :: ps) wf xs env1 env2 =
-  let 0 wfs = soAnd {a = wellTyped e penv1 penv2 fenv1 fenv2 p} wf in
-  anyL nil (parserOneOf at ps (snd wfs) 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 wf 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 : LengthOf 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 : LengthOf 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 : LengthOf 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 : LengthOf 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)