{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE StandaloneDeriving #-} -- For Show (ParsingError inp)
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE UnboxedTuples #-} -- For nextInput
{-# LANGUAGE UndecidableInstances #-} -- For Show (ParsingError inp)
module Symantic.Parser.Machine.Generate where

import Control.Monad (Monad(..))
import Data.Bool (Bool)
import Data.Char (Char)
import Data.Either (Either(..), either)
import Data.Function (($), (.), id, const, on)
import Data.Functor (Functor, (<$>), (<$))
import Data.Foldable (foldMap', toList)
import Data.Int (Int)
import Data.List.NonEmpty (NonEmpty(..))
import Data.Map (Map)
import Data.Maybe (Maybe(..))
import Data.Ord (Ord(..), Ordering(..))
import Data.Semigroup (Semigroup(..))
import Data.Set (Set)
import Data.String (String)
import Data.Traversable (Traversable(..))
import GHC.TypeLits (symbolVal)
import Language.Haskell.TH (CodeQ)
import Prelude ((+), (-), error)
import Text.Show (Show(..))
-- import qualified Control.Monad.Trans.State.Strict as MT
import qualified Data.HashMap.Strict as HM
import qualified Data.List as List
import qualified Data.List.NonEmpty as NE
import qualified Data.Map.Internal as Map_
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import qualified Language.Haskell.TH as TH
import qualified Language.Haskell.TH.Syntax as TH

import Symantic.Univariant.Letable
import Symantic.Univariant.Trans
import Symantic.Parser.Grammar.Combinators (ErrorItem(..))
import Symantic.Parser.Machine.Input
import Symantic.Parser.Machine.Instructions
import qualified Language.Haskell.TH.HideName as TH
import qualified Symantic.Parser.Haskell as H

--import Debug.Trace

genCode :: TermInstr a -> CodeQ a
genCode = trans

-- * Type 'Gen'
-- | Generate the 'CodeQ' parsing the input.
data Gen inp vs a = Gen
  { genAnalysisByLet :: LetMapFix (CallTrace -> GenAnalysis)
    -- ^ 'genAnalysis' for each 'defLet' and 'defJoin' of the 'Machine'.
  , genAnalysis :: LetMapTo (CallTrace -> GenAnalysis)
    -- ^ Synthetized (bottom-up) static genAnalysis of the 'Machine'.
  , unGen ::
      GenCtx inp vs a ->
      CodeQ (Either (ParsingError inp) a)
  }

-- | @('generateCode' input mach)@ generates @TemplateHaskell@ code
-- parsing the given 'input' according to the given 'Machine'.
generateCode ::
  Ord (InputToken inp) =>
  Show (InputToken inp) =>
  TH.Lift (InputToken inp) =>
  -- InputToken inp ~ Char =>
  Input inp =>
  Show (Cursor inp) =>
  Gen inp '[] a ->
  CodeQ (inp -> Either (ParsingError inp) a)
generateCode k = [|| \(input :: inp) ->
  -- Pattern bindings containing unlifted types
  -- should use an outermost bang pattern.
  let !(# init, readMore, readNext #) = $$(cursorOf [||input||]) in
  let finalRet = \_farInp _farExp v _inp -> Right v in
  let finalRaise :: forall b. (Catcher inp b)
        = \_failInp !farInp !farExp ->
        Left ParsingErrorStandard
        { parsingErrorOffset = offset farInp
        , parsingErrorUnexpected =
            if readMore farInp
            then Just (let (# c, _ #) = readNext farInp in c)
            else Nothing
        , parsingErrorExpecting = Set.fromList farExp
        } in
  $$(unGen k GenCtx
    { valueStack = ValueStackEmpty
    , catchStackByLabel = Map.empty
    , defaultCatch = [||finalRaise||]
    , callStack = []
    , retCode = [||finalRet||]
    , input = [||init||]
    , nextInput = [||readNext||]
    , moreInput = [||readMore||]
    -- , farthestError = [||Nothing||]
    , farthestInput = [||init||]
    , farthestExpecting = [|| [] ||]
    , checkedHorizon = 0
    , horizonStack = []
    , finalGenAnalysisByLet = runGenAnalysis (genAnalysisByLet k)
    })
  ||]

-- ** Type 'ParsingError'
data ParsingError inp
  =  ParsingErrorStandard
  {  parsingErrorOffset :: Offset
    -- | Note that if an 'ErrorItemHorizon' greater than 1
    -- is amongst the 'parsingErrorExpecting'
    -- then this is only the 'InputToken'
    -- at the begining of the expected 'Horizon'.
  ,  parsingErrorUnexpected :: Maybe (InputToken inp)
  ,  parsingErrorExpecting :: Set (ErrorItem (InputToken inp))
  }
deriving instance Show (InputToken inp) => Show (ParsingError inp)

-- ** Type 'ErrorLabel'
type ErrorLabel = String

-- * Type 'GenAnalysis'
data GenAnalysis = GenAnalysis
  { minReads :: Either ErrorLabel Horizon
  , mayRaise :: Map ErrorLabel ()
  } deriving (Show)

-- | Tie the knot between mutually recursive 'TH.Name's
-- introduced by 'defLet' and 'defJoin'.
-- and provide the empty initial 'CallTrace' stack
runGenAnalysis ::
  LetMapFix (CallTrace -> GenAnalysis) ->
  LetMap GenAnalysis
runGenAnalysis ga = (($ []) <$>) $ polyfix ga

-- | Poly-variadic fixpoint combinator.
-- Used to express mutual recursion and to transparently introduce memoization.
-- Used to "tie the knot" between observed sharing ('defLet', 'call', 'jump')
-- and join points ('defJoin', 'refJoin').
-- All mutually dependent functions are restricted to the same polymorphic type @(a)@.
-- See http://okmij.org/ftp/Computation/fixed-point-combinators.html#Poly-variadic
polyfix :: Functor f => f (f a -> a) -> f a
polyfix fs = fix $ \finals -> ($ finals) <$> fs

fix :: (a -> a) -> a
fix f = final where final = f final

type LetMap = HM.HashMap TH.Name
type LetMapTo a = LetMap a -> a
type LetMapFix a = LetMap (LetMap a -> a)

-- | Call trace stack updated by 'call' and 'refJoin'.
-- Used to avoid infinite loops when tying the knot with 'polyfix'.
type CallTrace = [TH.Name]

-- ** Type 'Offset'
type Offset = Int
-- ** Type 'Horizon'
-- | Minimal input length required for a successful parsing.
type Horizon = Offset

-- seqGenAnalysis = 
-- altGenAnalysis = List.foldl' (\acc x -> either Left (\h -> Right (either (const h) (min h) acc)) x)
seqGenAnalysis :: NonEmpty GenAnalysis -> GenAnalysis
seqGenAnalysis aas@(a:|as) = GenAnalysis
  { minReads = List.foldl' (\acc x ->
        acc >>= \r -> (r +) <$> minReads x
      ) (minReads a) as
  , mayRaise = sconcat (mayRaise <$> aas)
  }
altGenAnalysis :: NonEmpty GenAnalysis -> GenAnalysis
altGenAnalysis aas@(a:|as) = GenAnalysis
  { minReads = List.foldl' (\acc x ->
      either
        (\l -> either (const (Left  l)) Right)
        (\r -> either (const (Right r)) (Right . min r))
        acc (minReads x)
      ) (minReads a) as
  , mayRaise = sconcat (mayRaise <$> aas)
  }


{-
-- *** Type 'FarthestError'
data FarthestError inp = FarthestError
  { farthestInput :: Cursor inp
  , farthestExpecting :: [ErrorItem (InputToken inp)]
  }
-}

-- ** Type 'GenCtx'
-- | This is an inherited (top-down) context
-- only present at compile-time, to build TemplateHaskell splices.
data GenCtx inp vs a =
  ( TH.Lift (InputToken inp)
  , Cursorable (Cursor inp)
  , Show (InputToken inp)
  ) => GenCtx
  { valueStack :: ValueStack vs
  , catchStackByLabel :: Map ErrorLabel (NonEmpty (CodeQ (Catcher inp a)))
    -- | Default 'Catcher' defined at the begining of the generated 'CodeQ',
    -- hence a constant within the 'Gen'eration.
  , defaultCatch :: forall b. CodeQ (Catcher inp b)
    -- | Used by 'checkToken' to get 'GenAnalysis' from 'genAnalysis'.
  , callStack :: [TH.Name]
  , retCode :: CodeQ (Cont inp a a)
  , input :: CodeQ (Cursor inp)
  , moreInput :: CodeQ (Cursor inp -> Bool)
  , nextInput :: CodeQ (Cursor inp -> (# InputToken inp, Cursor inp #))
  , farthestInput :: CodeQ (Cursor inp)
  , farthestExpecting :: CodeQ [ErrorItem (InputToken inp)]
    -- | Remaining horizon already checked.
    -- Use to factorize 'input' length checks,
    -- instead of checking the 'input' length
    -- one 'InputToken' at a time at each 'read'.
    -- Updated by 'checkHorizon'
    -- and reset elsewhere when needed.
  , checkedHorizon :: Horizon
  -- | Used by 'pushInput' and 'loadInput'
  -- to restore the 'Horizon' at the restored 'input'.
  , horizonStack :: [Horizon]
  -- | Output of 'runGenAnalysis'.
  , finalGenAnalysisByLet :: LetMap GenAnalysis
  }

-- ** Type 'ValueStack'
data ValueStack vs where
  ValueStackEmpty :: ValueStack '[]
  ValueStackCons ::
    { valueStackHead :: TermInstr v
    , valueStackTail :: ValueStack vs
    } -> ValueStack (v ': vs)

instance InstrValuable Gen where
  pushValue x k = k
    { unGen = \ctx -> {-trace "unGen.pushValue" $-} unGen k ctx
      { valueStack = ValueStackCons x (valueStack ctx) }
    }
  popValue k = k
    { unGen = \ctx -> {-trace "unGen.popValue" $-} unGen k ctx
      { valueStack = valueStackTail (valueStack ctx) }
    }
  lift2Value f k = k
    { unGen = \ctx -> {-trace "unGen.lift2Value" $-} unGen k ctx
      { valueStack =
        let ValueStackCons y (ValueStackCons x vs) = valueStack ctx in
        ValueStackCons (f H.:@ x H.:@ y) vs
      }
    }
  swapValue k = k
    { unGen = \ctx -> {-trace "unGen.swapValue" $-} unGen k ctx
      { valueStack =
          let ValueStackCons y (ValueStackCons x vs) = valueStack ctx in
          ValueStackCons x (ValueStackCons y vs)
      }
    }
instance InstrBranchable Gen where
  caseBranch kx ky = Gen
    { genAnalysisByLet = genAnalysisByLet kx <> genAnalysisByLet ky
    , genAnalysis = \final ct -> altGenAnalysis $ genAnalysis kx final ct :| [genAnalysis ky final ct]
    , unGen = \ctx -> {-trace "unGen.caseBranch" $-}
      let ValueStackCons v vs = valueStack ctx in
      [||
        case $$(genCode v) of
          Left  x -> $$(unGen kx ctx{ valueStack = ValueStackCons (H.Term [||x||]) vs })
          Right y -> $$(unGen ky ctx{ valueStack = ValueStackCons (H.Term [||y||]) vs })
      ||]
    }
  choicesBranch fs ks kd = Gen
    { genAnalysisByLet = sconcat $ genAnalysisByLet kd :| (genAnalysisByLet <$> ks)
    , genAnalysis = \final ct -> altGenAnalysis $ (\k -> genAnalysis k final ct) <$> (kd:|ks)
    , unGen = \ctx -> {-trace "unGen.choicesBranch" $-}
      let ValueStackCons v vs = valueStack ctx in
      go ctx{valueStack = vs} v fs ks
    }
    where
    go ctx x (f:fs') (k:ks') = [||
      if $$(genCode (H.optimizeTerm (f H.:@ x)))
      then
        let _ = "choicesBranch.then" in
        $$({-trace "unGen.choicesBranch.k" $-} unGen k ctx)
      else
        let _ = "choicesBranch.else" in
        $$(go ctx x fs' ks')
      ||]
    go ctx _ _ _ = unGen kd ctx
instance InstrExceptionable Gen where
  raiseException lbl failExp = Gen
    { genAnalysisByLet = HM.empty
    , genAnalysis = \_final _ct -> GenAnalysis
        { minReads = Left (symbolVal lbl)
        , mayRaise = Map.singleton (symbolVal lbl) ()
        }
    , unGen = \ctx@GenCtx{} -> {-trace ("unGen.raiseException: "<>symbolVal lbl) $-} [||
      let (# farInp, farExp #) =
            case $$compareOffset $$(farthestInput ctx) $$(input ctx) of
              LT -> (# $$(input ctx), failExp #)
              EQ -> (# $$(farthestInput ctx), $$(farthestExpecting ctx) <> failExp #)
              GT -> (# $$(farthestInput ctx), $$(farthestExpecting ctx) #) in
        $$(NE.head $ Map.findWithDefault
            (NE.singleton (defaultCatch ctx))
            (symbolVal lbl)
            (catchStackByLabel ctx))
        $$(input ctx) farInp farExp
      ||]
    }
  popException lbl k = k
    { unGen = \ctx -> {-trace ("unGen.popException: "<>symbolVal lbl) $-}
      unGen k ctx{catchStackByLabel = Map.update (\case
          _r0:|(r1:rs) -> Just (r1:|rs)
          _ -> Nothing
        ) (symbolVal lbl) (catchStackByLabel ctx)
      }
    }
  catchException lbl ok ko = Gen
    { genAnalysisByLet = genAnalysisByLet ok <> genAnalysisByLet ko
    , genAnalysis = \final ct ->
        let ga = altGenAnalysis $ genAnalysis ok final ct :| [ genAnalysis ko final ct ] in
        ga { mayRaise = Map.delete (symbolVal lbl) (mayRaise ga) }
    , unGen = \ctx@GenCtx{} -> {-trace ("unGen.catchException: "<>symbolVal lbl) $-} [||
        let _ = $$(liftTypedString ("catchException lbl="<>symbolVal lbl)) in
        let catchHandler !failInp !farInp !farExp =
              let _ = $$(liftTypedString ("catchException.ko lbl="<>symbolVal lbl)) in
              $$({-trace ("unGen.catchException.ko: "<>symbolVal lbl) $-} unGen ko ctx
                -- Push 'input' and 'checkedHorizon'
                -- as they were when entering 'catchException'.
                { valueStack =
                    ValueStackCons (H.Term (input ctx)) $
                    valueStack ctx
                , horizonStack =
                    checkedHorizon ctx : horizonStack ctx
                -- Note that 'catchStackByLabel' is reset.
                -- Move the input to the failing position.
                , input = [||failInp||]
                -- The 'checkedHorizon' at the 'raiseException's
                -- are not known here.
                -- Nor whether 'failInp' is after
                -- 'checkedHorizon' 'ctx' or not.
                , checkedHorizon = 0
                -- Set the farthestInput to the farthest computed by 'fail'.
                , farthestInput = [||farInp||]
                , farthestExpecting = [||farExp||]
                })
        in
        $$({-trace ("unGen.catchException.ok: "<>symbolVal lbl) $-} unGen ok ctx
        { catchStackByLabel = Map.insertWith (<>) (symbolVal lbl)
            (NE.singleton [||catchHandler||]) (catchStackByLabel ctx)
        }
      ) ||]
    }

-- ** Type 'Catcher'
type Catcher inp a =
  {-failureInput-}Cursor inp ->
  {-farthestInput-}Cursor inp ->
  {-farthestExpecting-}[ErrorItem (InputToken inp)] ->
  Either (ParsingError inp) a
instance InstrInputable Gen where
  pushInput k = k
    { unGen = \ctx ->
        {-trace "unGen.pushInput" $-}
        unGen k ctx
          { valueStack = H.Term (input ctx) `ValueStackCons` valueStack ctx
          , horizonStack = checkedHorizon ctx : horizonStack ctx
          }
    }
  loadInput k = k
    { unGen = \ctx ->
        {-trace "unGen.loadInput" $-}
        let ValueStackCons input vs = valueStack ctx in
        let (h, hs) = case horizonStack ctx of
                        [] -> (0, [])
                        x:xs -> (x, xs) in
        unGen k ctx
          { valueStack = vs
          , horizonStack = hs
          , input = genCode input
          , checkedHorizon = h
          }
    , genAnalysis = \final ct -> GenAnalysis
        { minReads = 0 <$ minReads (genAnalysis k final ct)
        , mayRaise = mayRaise (genAnalysis k final ct)
        }
    }
instance InstrCallable Gen where
  defLet defs k = k
    { unGen = \ctx@GenCtx{} ->
        {-trace ("unGen.defLet: defs="<>show (HM.keys defs)) $-}
        TH.unsafeCodeCoerce $ do
          decls <- traverse (makeDecl ctx) (HM.toList defs)
          body <- TH.unTypeQ $ TH.examineCode $
            {-trace "unGen.defLet.body" $-}
            unGen k ctx
          return $ TH.LetE (
            -- | Try to output more deterministic code to be able to golden test it,
            -- at the cost of more computations (at compile-time only though).
            List.sortBy (compare `on` TH.hideName) $
            toList decls
            ) body
    , genAnalysisByLet =
        foldMap' (\(SomeLet sub) -> genAnalysisByLet sub) defs <>
        ((\(SomeLet sub) -> genAnalysis sub) <$> defs) <>
        genAnalysisByLet k
    }
    where
    makeDecl ctx (n, SomeLet sub) = do
      body <- TH.unTypeQ $ TH.examineCode $ [|| -- buildRec in Parsley
        -- Called by 'call' or 'jump'.
        \ !ok{-from generateSuspend or retCode-}
          !inp
          !koByLabel{- 'catchStackByLabel' from the 'call'-site -} ->
          $$({-trace ("unGen.defLet.sub: "<>show n) $-} unGen sub ctx
            { valueStack = ValueStackEmpty
            -- Build a 'catchStackByLabel' from the one available at the 'call'-site.
            -- Note that all the 'mayRaise' of the 'sub'routine may not be available,
            -- hence 'Map.findWithDefault' is used instead of 'Map.!'.
            , catchStackByLabel = Map.mapWithKey
                (\lbl () -> NE.singleton [||Map.findWithDefault $$(defaultCatch ctx) lbl koByLabel||])
                ({-trace ("mayRaise: "<>show n) $-}
                  mayRaise (finalGenAnalysisByLet ctx HM.! n))
            , input = [||inp||]
            , retCode = {-trace ("unGen.defLet.sub.retCode: "<>show n) $-} [||ok||]

            -- These are passed by the caller via 'ok' or 'ko'
            -- , farthestInput = 
            -- , farthestExpecting = 

            -- Some callers can call this 'defLet'
            -- with zero 'checkedHorizon', hence use this minimum.
            -- TODO: maybe it could be improved a bit
            -- by taking the minimum of the checked horizons
            -- before all the 'call's and 'jump's to this 'defLet'.
            , checkedHorizon = 0
            })
        ||]
      let decl = TH.FunD n [TH.Clause [] (TH.NormalB body) []]
      return decl
  jump (LetName n) = Gen
    { genAnalysisByLet = HM.empty
    , genAnalysis = \final ct ->
        if n`List.elem`ct
        then GenAnalysis
          { minReads = Right 0
          , mayRaise = Map.empty
          }
        else (final HM.! n) (n:ct)
    , unGen = \ctx -> {-trace ("unGen.jump: "<>show n) $-} [||
      let _ = "jump" in
      $$(TH.unsafeCodeCoerce (return (TH.VarE n)))
        {-ok-}$$(retCode ctx)
        $$(input ctx)
        $$(liftTypedRaiseByLabel $
          catchStackByLabel ctx
          -- Pass only the labels raised by the 'defLet'.
          `Map.intersection`
          (mayRaise $ finalGenAnalysisByLet ctx HM.! n)
        )
      ||]
    }
  call (LetName n) k = k
    { genAnalysis = \final ct ->
        if n`List.elem`ct
        then GenAnalysis
          { minReads = Right 0
          , mayRaise = Map.empty
          }
        else seqGenAnalysis $
          (final HM.! n) (n:ct) :|
          [ genAnalysis k final ct ]
    , unGen = {-trace ("unGen.call: "<>show n) $-} \ctx ->
      -- let ks = (Map.keys (catchStackByLabel ctx)) in
      [||
      -- let _ = $$(liftTypedString $ "call exceptByLet("<>show n<>")="<>show (Map.keys (Map.findWithDefault Map.empty n (exceptByLet ctx))) <> " catchStackByLabel(ctx)="<> show ks) in
      $$(TH.unsafeCodeCoerce (return (TH.VarE n)))
        {-ok-}$$(generateSuspend k ctx{callStack = n : callStack ctx})
        $$(input ctx)
        $$(liftTypedRaiseByLabel $
          catchStackByLabel ctx
          -- Pass only the labels raised by the 'defLet'.
          `Map.intersection`
          (mayRaise $ finalGenAnalysisByLet ctx HM.! n)
        )
      ||]
    }
  ret = Gen
    { genAnalysisByLet = HM.empty
    , genAnalysis = \_final _ct -> GenAnalysis
        { minReads = Right 0
        , mayRaise = Map.empty
        }
    , unGen = \ctx -> {-trace "unGen.ret" $-} unGen ({-trace "unGen.ret.generateResume" $-} generateResume ({-trace "unGen.ret.retCode" $-} retCode ctx)) ctx
    }

-- | Like 'TH.liftString' but on 'TH.Code'.
-- Useful to get a 'TH.StringL' instead of a 'TH.ListE'.
liftTypedString :: String -> TH.Code TH.Q a
liftTypedString = TH.unsafeCodeCoerce . TH.liftString

-- | Like 'TH.liftTyped' but adjusted to work on 'catchStackByLabel'
-- which already contains 'CodeQ' terms.
-- Moreover, only the 'Catcher' at the top of the stack
-- is needed and thus generated in the resulting 'CodeQ'.
--
-- TODO: Use an 'Array' instead of a 'Map'?
liftTypedRaiseByLabel :: TH.Lift k => Map k (NonEmpty (CodeQ a)) -> CodeQ (Map k a)
liftTypedRaiseByLabel Map_.Tip = [|| Map_.Tip ||]
liftTypedRaiseByLabel (Map_.Bin s k (h:|_hs) l r) =
  [|| Map_.Bin s k $$h $$(liftTypedRaiseByLabel l) $$(liftTypedRaiseByLabel r) ||]

-- ** Type 'Cont'
type Cont inp v a =
  {-farthestInput-}Cursor inp ->
  {-farthestExpecting-}[ErrorItem (InputToken inp)] ->
  v ->
  Cursor inp ->
  Either (ParsingError inp) a

-- | Generate a 'retCode' 'Cont'inuation to be called with 'generateResume'.
-- Used when 'call' 'ret'urns.
-- The return 'v'alue is 'pushValue'-ed on the 'valueStack'.
generateSuspend ::
  {-k-}Gen inp (v ': vs) a ->
  GenCtx inp vs a ->
  CodeQ (Cont inp v a)
generateSuspend k ctx = [||
  let _ = $$(liftTypedString $ "suspend") in
  \farInp farExp v !inp ->
    $$({-trace "unGen.generateSuspend" $-} unGen k ctx
      { valueStack = ValueStackCons ({-trace "unGen.generateSuspend.value" $-} H.Term [||v||]) (valueStack ctx)
      , input = [||inp||]
      , farthestInput = [||farInp||]
      , farthestExpecting = [||farExp||]
      , checkedHorizon = 0
      }
    )
  ||]

-- | Generate a call to the 'generateSuspend' continuation.
-- Used when 'call' 'ret'urns.
generateResume ::
  CodeQ (Cont inp v a) ->
  Gen inp (v ': vs) a
generateResume k = Gen
  { genAnalysisByLet = HM.empty
  , genAnalysis = \_final _ct -> GenAnalysis
      { minReads = Right 0
      , mayRaise = Map.empty
      }
  , unGen = \ctx -> {-trace "unGen.generateResume" $-} [||
    let _ = "resume" in
    $$k
      $$(farthestInput ctx)
      $$(farthestExpecting ctx)
      (let _ = "resume.genCode" in $$({-trace "unGen.generateResume.genCode" $-} genCode $ H.optimizeTerm $
        valueStackHead $ valueStack ctx))
      $$(input ctx)
    ||]
  }

instance InstrJoinable Gen where
  defJoin (LetName n) sub k = k
    { unGen =
        \ctx ->
        {-trace ("unGen.defJoin: "<>show n) $-}
        TH.unsafeCodeCoerce $ do
          next <- TH.unTypeQ $ TH.examineCode $ [||
            -- Called by 'generateResume'.
            \farInp farExp v !inp ->
              $$({-trace ("unGen.defJoin.next: "<>show n) $-} unGen sub ctx
                { valueStack = ValueStackCons (H.Term [||v||]) (valueStack ctx)
                , input = [||inp||]
                , farthestInput = [||farInp||]
                , farthestExpecting = [||farExp||]
                , checkedHorizon = 0
                {- FIXME:
                , catchStackByLabel = Map.mapWithKey
                    (\lbl () -> NE.singleton [||koByLabel Map.! lbl||])
                    (mayRaise sub raiseLabelsByLetButSub)
                -}
                })
            ||]
          let decl = TH.FunD n [TH.Clause [] (TH.NormalB next) []]
          expr <- TH.unTypeQ (TH.examineCode ({-trace ("unGen.defJoin.expr: "<>show n) $-} unGen k ctx))
          return (TH.LetE [decl] expr)
    , genAnalysisByLet =
        (genAnalysisByLet sub <>) $
        HM.insert n (genAnalysis sub) $
        genAnalysisByLet k
    }
  refJoin (LetName n) = Gen
    { unGen = \ctx ->
        {-trace ("unGen.refJoin: "<>show n) $-}
        unGen (generateResume
          (TH.unsafeCodeCoerce (return (TH.VarE n)))) ctx
    , genAnalysisByLet = HM.empty
    , genAnalysis = \final ct ->
        if n`List.elem`ct -- FIXME: useless
        then GenAnalysis
          { minReads = Right 0
          , mayRaise = Map.empty
          }
        else HM.findWithDefault
          (error (show (n,ct,HM.keys final)))
          n final (n:ct)
    }
instance InstrReadable Char Gen where
  read farExp p = checkHorizon . checkToken farExp p

checkHorizon ::
  TH.Lift (InputToken inp) =>
  {-ok-}Gen inp vs a ->
  Gen inp vs a
checkHorizon ok = ok
  { genAnalysis = \final ct -> seqGenAnalysis $
      GenAnalysis { minReads = Right 1
                  , mayRaise = Map.singleton "fail" ()
                  } :|
      [ genAnalysis ok final ct ]
  , unGen = \ctx0@GenCtx{} ->
    {-trace "unGen.checkHorizon" $-}
    let raiseFail =
          NE.head (Map.findWithDefault
            (NE.singleton (defaultCatch ctx0))
            "fail" (catchStackByLabel ctx0)) in
    [||
      -- Factorize generated code for raising the "fail".
      let readFail = $$(raiseFail) in
      $$(
        let ctx = ctx0{catchStackByLabel =
                    Map.adjust (\(_r:|rs) -> [||readFail||] :| rs)
                      "fail" (catchStackByLabel ctx0)} in
        if checkedHorizon ctx >= 1
        then unGen ok ctx0{checkedHorizon = checkedHorizon ctx - 1}
        else let minHoriz =
                    either (\err -> 0) id $
                    minReads $ finalGenAnalysis ctx ok in
          [||
          if $$(moreInput ctx)
               $$(if minHoriz > 0
                 then [||$$shiftRight minHoriz $$(input ctx)||]
                 else input ctx)
          then $$(unGen ok ctx{checkedHorizon = minHoriz})
          else let _ = "checkHorizon.else" in
            -- TODO: return a resuming continuation (eg. Partial)
            $$(unGen (fail [ErrorItemHorizon (minHoriz + 1)]) ctx)
          ||]
      )
    ||]
  }

finalGenAnalysis :: GenCtx inp vs a -> Gen inp cs a -> GenAnalysis
finalGenAnalysis ctx k =
  --(\f -> f (error "callTrace")) $
  (\f -> f (callStack ctx)) $
  genAnalysis k $
  ((\f _ct -> f) <$>) $
  finalGenAnalysisByLet ctx

checkToken ::
  Ord (InputToken inp) =>
  TH.Lift (InputToken inp) =>
  [ErrorItem (InputToken inp)] ->
  {-predicate-}TermInstr (InputToken inp -> Bool) ->
  {-ok-}Gen inp (InputToken inp ': vs) a ->
  Gen inp vs a
checkToken farExp p ok = ok
  { unGen = \ctx -> {-trace "unGen.read" $-} [||
    let !(# c, cs #) = $$(nextInput ctx) $$(input ctx) in
    if $$(genCode p) c
    then $$(unGen ok ctx
      { valueStack = ValueStackCons (H.Term [||c||]) (valueStack ctx)
      , input = [||cs||]
      })
    else let _ = "checkToken.else" in $$(unGen (fail farExp) ctx)
    ||]
  }