    module Agda.Compiler.ToTreeless
      ( toTreeless
      , closedTermToTreeless
      ) where

    import Control.Arrow        ( first )
    import Control.Monad        ( filterM, foldM, forM, zipWithM )
    import Control.Monad.Reader ( MonadReader(..), asks, ReaderT, runReaderT )
    import Control.Monad.Trans  ( lift )

    import Data.Maybe
    import Data.Map (Map)
    import qualified Data.Map  as Map
    import qualified Data.List as List

    import Agda.Syntax.Common
    import Agda.Syntax.Internal as I
    import Agda.Syntax.Literal
    import qualified Agda.Syntax.Treeless as C
    import Agda.Syntax.Treeless (TTerm, EvaluationStrategy, ArgUsage(..))

    import Agda.TypeChecking.CompiledClause as CC
    import qualified Agda.TypeChecking.CompiledClause.Compile as CC
    import Agda.TypeChecking.EtaContract (binAppView, BinAppView(..))
    import Agda.TypeChecking.Monad as TCM
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Records (getRecordConstructor)
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute

    import Agda.Compiler.Treeless.AsPatterns
    import Agda.Compiler.Treeless.Builtin
    import Agda.Compiler.Treeless.Erase
    import Agda.Compiler.Treeless.Identity
    import Agda.Compiler.Treeless.Simplify
    import Agda.Compiler.Treeless.Uncase
    import Agda.Compiler.Treeless.Unused

    import Agda.Utils.Function
    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Pretty (prettyShow)
    import qualified Agda.Utils.Pretty as P
    import qualified Agda.Utils.SmallSet as SmallSet

    import Agda.Utils.Impossible

    prettyPure :: P.Pretty a => a -> TCM Doc
    prettyPure :: forall a. Pretty a => a -> TCMT IO Doc
    prettyPure = Doc -> TCMT IO Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCMT IO Doc) -> (a -> Doc) -> a -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty

    -- | Recompile clauses with forcing translation turned on.
    getCompiledClauses :: QName -> TCM CC.CompiledClauses
    getCompiledClauses :: QName -> TCM CompiledClauses
    getCompiledClauses QName
    q = do
      Definition
    def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
      let cs :: [Clause]
    cs = Definition -> [Clause]
    defClauses Definition
    def
          isProj :: Bool
    isProj | Function{ funProjection :: Defn -> Maybe Projection
    funProjection = Maybe Projection
    proj } <- Definition -> Defn
    theDef Definition
    def = Maybe QName -> Bool
    forall a. Maybe a -> Bool
    isJust (Projection -> Maybe QName
    projProper (Projection -> Maybe QName) -> Maybe Projection -> Maybe QName
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Maybe Projection
    proj)
                 | Bool
    otherwise = Bool
    False
          translate :: RunRecordPatternTranslation
    translate | Bool
    isProj    = RunRecordPatternTranslation
    CC.DontRunRecordPatternTranslation
                    | Bool
    otherwise = RunRecordPatternTranslation
    CC.RunRecordPatternTranslation
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "treeless.convert" Int
    40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "-- before clause compiler" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ (QName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty QName
    q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "=") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <?> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ((Clause -> TCMT IO Doc) -> [Clause] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Clause -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Clause]
    cs)
      let mst :: Maybe SplitTree
    mst = Defn -> Maybe SplitTree
    funSplitTree (Defn -> Maybe SplitTree) -> Defn -> Maybe SplitTree
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef Definition
    def
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "treeless.convert" Int
    70 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
        Maybe SplitTree
    -> TCMT IO Doc -> (SplitTree -> TCMT IO Doc) -> TCMT IO Doc
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe SplitTree
    mst TCMT IO Doc
    "-- not using split tree" ((SplitTree -> TCMT IO Doc) -> TCMT IO Doc)
    -> (SplitTree -> TCMT IO Doc) -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ \SplitTree
    st ->
          TCMT IO Doc
    "-- using split tree" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ SplitTree -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty SplitTree
    st
      RunRecordPatternTranslation
    -> [Clause] -> Maybe SplitTree -> TCM CompiledClauses
    CC.compileClauses' RunRecordPatternTranslation
    translate [Clause]
    cs Maybe SplitTree
    mst

    -- | Converts compiled clauses to treeless syntax.
    --
    -- Note: Do not use any of the concrete names in the returned
    -- term for identification purposes! If you wish to do so,
    -- first apply the Agda.Compiler.Treeless.NormalizeNames
    -- transformation.
    toTreeless :: EvaluationStrategy -> QName -> TCM (Maybe C.TTerm)
    toTreeless :: EvaluationStrategy -> QName -> TCM (Maybe TTerm)
    toTreeless EvaluationStrategy
    eval QName
    q = TCMT IO Bool
    -> TCM (Maybe TTerm) -> TCM (Maybe TTerm) -> TCM (Maybe TTerm)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> TCMT IO Bool
    alwaysInline QName
    q) (Maybe TTerm -> TCM (Maybe TTerm)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe TTerm
    forall a. Maybe a
    Nothing) (TCM (Maybe TTerm) -> TCM (Maybe TTerm))
    -> TCM (Maybe TTerm) -> TCM (Maybe TTerm)
    forall a b. (a -> b) -> a -> b
    $ TTerm -> Maybe TTerm
    forall a. a -> Maybe a
    Just (TTerm -> Maybe TTerm) -> TCMT IO TTerm -> TCM (Maybe TTerm)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> EvaluationStrategy -> QName -> TCMT IO TTerm
    toTreeless' EvaluationStrategy
    eval QName
    q

    toTreeless' :: EvaluationStrategy -> QName -> TCM C.TTerm
    toTreeless' :: EvaluationStrategy -> QName -> TCMT IO TTerm
    toTreeless' EvaluationStrategy
    eval QName
    q =
      (TCMT IO TTerm -> TCM (Maybe TTerm) -> TCMT IO TTerm)
    -> TCM (Maybe TTerm) -> TCMT IO TTerm -> TCMT IO TTerm
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip TCMT IO TTerm -> TCM (Maybe TTerm) -> TCMT IO TTerm
    forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
    fromMaybeM (QName -> TCM (Maybe TTerm)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe TTerm)
    getTreeless QName
    q) (TCMT IO TTerm -> TCMT IO TTerm) -> TCMT IO TTerm -> TCMT IO TTerm
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> [Char] -> TCMT IO TTerm -> TCMT IO TTerm
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m a -> m a
    verboseBracket [Char]
    "treeless.convert" Int
    20 ([Char]
    "compiling " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    q) (TCMT IO TTerm -> TCMT IO TTerm) -> TCMT IO TTerm -> TCMT IO TTerm
    forall a b. (a -> b) -> a -> b
    $ do
        CompiledClauses
    cc <- QName -> TCM CompiledClauses
    getCompiledClauses QName
    q
        TCMT IO Bool -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (QName -> TCMT IO Bool
    alwaysInline QName
    q) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> TTerm -> TCMT IO ()
    setTreeless QName
    q (QName -> TTerm
    C.TDef QName
    q)
          -- so recursive inlining doesn't loop, but not for always inlined
          -- functions, since that would risk inlining to fail.
        EvaluationStrategy -> QName -> CompiledClauses -> TCMT IO TTerm
    ccToTreeless EvaluationStrategy
    eval QName
    q CompiledClauses
    cc

    -- | Does not require the name to refer to a function.
    cacheTreeless :: EvaluationStrategy -> QName -> TCM ()
    cacheTreeless :: EvaluationStrategy -> QName -> TCMT IO ()
    cacheTreeless EvaluationStrategy
    eval QName
    q = do
      Defn
    def <- Definition -> Defn
    theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
      case Defn
    def of
        Function{} -> () () -> TCMT IO TTerm -> TCMT IO ()
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ EvaluationStrategy -> QName -> TCMT IO TTerm
    toTreeless' EvaluationStrategy
    eval QName
    q
        Defn
    _          -> () -> TCMT IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    ccToTreeless :: EvaluationStrategy -> QName -> CC.CompiledClauses -> TCM C.TTerm
    ccToTreeless :: EvaluationStrategy -> QName -> CompiledClauses -> TCMT IO TTerm
    ccToTreeless EvaluationStrategy
    eval QName
    q CompiledClauses
    cc = do
      let pbody :: TTerm -> TCMT IO Doc
    pbody TTerm
    b = [Char] -> TTerm -> TCMT IO Doc
    pbody' [Char]
    "" TTerm
    b
          pbody' :: [Char] -> TTerm -> TCMT IO Doc
    pbody' [Char]
    suf TTerm
    b = [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    q [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    suf) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "=", Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TTerm -> TCMT IO Doc
    forall a. Pretty a => a -> TCMT IO Doc
    prettyPure TTerm
    b ]
      Int
    v <- TCMT IO Bool -> TCMT IO Int -> TCMT IO Int -> TCMT IO Int
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> TCMT IO Bool
    alwaysInline QName
    q) (Int -> TCMT IO Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    20) (Int -> TCMT IO Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    0)
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "treeless.convert" (Int
    30 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    v) (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "-- compiled clauses of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (CompiledClauses -> TCMT IO Doc
    forall a. Pretty a => a -> TCMT IO Doc
    prettyPure CompiledClauses
    cc)
      TTerm
    body <- EvaluationStrategy -> CompiledClauses -> TCMT IO TTerm
    casetreeTop EvaluationStrategy
    eval CompiledClauses
    cc
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "treeless.opt.converted" (Int
    30 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    v) (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "-- converted" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ TTerm -> TCMT IO Doc
    pbody TTerm
    body
      TTerm
    body <- EvaluationStrategy -> QName -> Pipeline -> TTerm -> TCMT IO TTerm
    runPipeline EvaluationStrategy
    eval QName
    q (Int -> QName -> Pipeline
    compilerPipeline Int
    v QName
    q) TTerm
    body
      [ArgUsage]
    used <- QName -> TTerm -> TCM [ArgUsage]
    usedArguments QName
    q TTerm
    body
      Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (ArgUsage
    ArgUnused ArgUsage -> [ArgUsage] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [ArgUsage]
    used) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
        [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "treeless.opt.unused" (Int
    30 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    v) (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
          TCMT IO Doc
    "-- used args:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep [ if ArgUsage
    u ArgUsage -> ArgUsage -> Bool
    forall a. Eq a => a -> a -> Bool
    == ArgUsage
    ArgUsed then [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text [Char
    x] else TCMT IO Doc
    "_" | (Char
    x, ArgUsage
    u) <- [Char] -> [ArgUsage] -> [(Char, ArgUsage)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Char
    'a'..] [ArgUsage]
    used ] TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$
          [Char] -> TTerm -> TCMT IO Doc
    pbody' [Char]
    "[stripped]" ([ArgUsage] -> TTerm -> TTerm
    stripUnusedArguments [ArgUsage]
    used TTerm
    body)
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "treeless.opt.final" (Int
    20 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    v) (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TTerm -> TCMT IO Doc
    pbody TTerm
    body
      QName -> TTerm -> TCMT IO ()
    setTreeless QName
    q TTerm
    body
      QName -> [ArgUsage] -> TCMT IO ()
    setCompiledArgUse QName
    q [ArgUsage]
    used
      TTerm -> TCMT IO TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    body

    data Pipeline = FixedPoint Int Pipeline
                  | Sequential [Pipeline]
                  | SinglePass CompilerPass

    data CompilerPass = CompilerPass
      { CompilerPass -> [Char]
    passTag       :: String
      , CompilerPass -> Int
    passVerbosity :: Int
      , CompilerPass -> [Char]
    passName      :: String
      , CompilerPass -> EvaluationStrategy -> TTerm -> TCMT IO TTerm
    passCode      :: EvaluationStrategy -> TTerm -> TCM TTerm
      }

    compilerPass :: String -> Int -> String -> (EvaluationStrategy -> TTerm -> TCM TTerm) -> Pipeline
    compilerPass :: [Char]
    -> Int
    -> [Char]
    -> (EvaluationStrategy -> TTerm -> TCMT IO TTerm)
    -> Pipeline
    compilerPass [Char]
    tag Int
    v [Char]
    name EvaluationStrategy -> TTerm -> TCMT IO TTerm
    code = CompilerPass -> Pipeline
    SinglePass ([Char]
    -> Int
    -> [Char]
    -> (EvaluationStrategy -> TTerm -> TCMT IO TTerm)
    -> CompilerPass
    CompilerPass [Char]
    tag Int
    v [Char]
    name EvaluationStrategy -> TTerm -> TCMT IO TTerm
    code)

    compilerPipeline :: Int -> QName -> Pipeline
    compilerPipeline :: Int -> QName -> Pipeline
    compilerPipeline Int
    v QName
    q =
      [Pipeline] -> Pipeline
    Sequential
        -- Issue #4967: No simplification step before builtin translation! Simplification relies
        --              on either all or no builtins being translated. Since we might have inlined
        --              functions that have had the builtin translation applied, we need to apply it
        --              first.
        -- [ compilerPass "simpl"   (35 + v) "simplification"      $ const simplifyTTerm
        [ [Char]
    -> Int
    -> [Char]
    -> (EvaluationStrategy -> TTerm -> TCMT IO TTerm)
    -> Pipeline
    compilerPass [Char]
    "builtin" (Int
    30 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    v) [Char]
    "builtin translation" ((EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline)
    -> (EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline
    forall a b. (a -> b) -> a -> b
    $ (TTerm -> TCMT IO TTerm)
    -> EvaluationStrategy -> TTerm -> TCMT IO TTerm
    forall a b. a -> b -> a
    const TTerm -> TCMT IO TTerm
    translateBuiltins
        , Int -> Pipeline -> Pipeline
    FixedPoint Int
    5 (Pipeline -> Pipeline) -> Pipeline -> Pipeline
    forall a b. (a -> b) -> a -> b
    $ [Pipeline] -> Pipeline
    Sequential
          [ [Char]
    -> Int
    -> [Char]
    -> (EvaluationStrategy -> TTerm -> TCMT IO TTerm)
    -> Pipeline
    compilerPass [Char]
    "simpl"  (Int
    30 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    v) [Char]
    "simplification"     ((EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline)
    -> (EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline
    forall a b. (a -> b) -> a -> b
    $ (TTerm -> TCMT IO TTerm)
    -> EvaluationStrategy -> TTerm -> TCMT IO TTerm
    forall a b. a -> b -> a
    const TTerm -> TCMT IO TTerm
    simplifyTTerm
          , [Char]
    -> Int
    -> [Char]
    -> (EvaluationStrategy -> TTerm -> TCMT IO TTerm)
    -> Pipeline
    compilerPass [Char]
    "erase"  (Int
    30 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    v) [Char]
    "erasure"            ((EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline)
    -> (EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline
    forall a b. (a -> b) -> a -> b
    $ QName -> EvaluationStrategy -> TTerm -> TCMT IO TTerm
    eraseTerms QName
    q
          , [Char]
    -> Int
    -> [Char]
    -> (EvaluationStrategy -> TTerm -> TCMT IO TTerm)
    -> Pipeline
    compilerPass [Char]
    "uncase" (Int
    30 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    v) [Char]
    "uncase"             ((EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline)
    -> (EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline
    forall a b. (a -> b) -> a -> b
    $ (TTerm -> TCMT IO TTerm)
    -> EvaluationStrategy -> TTerm -> TCMT IO TTerm
    forall a b. a -> b -> a
    const TTerm -> TCMT IO TTerm
    forall (m :: * -> *). Monad m => TTerm -> m TTerm
    caseToSeq
          , [Char]
    -> Int
    -> [Char]
    -> (EvaluationStrategy -> TTerm -> TCMT IO TTerm)
    -> Pipeline
    compilerPass [Char]
    "aspat"  (Int
    30 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    v) [Char]
    "@-pattern recovery" ((EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline)
    -> (EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline
    forall a b. (a -> b) -> a -> b
    $ (TTerm -> TCMT IO TTerm)
    -> EvaluationStrategy -> TTerm -> TCMT IO TTerm
    forall a b. a -> b -> a
    const TTerm -> TCMT IO TTerm
    forall (m :: * -> *). Monad m => TTerm -> m TTerm
    recoverAsPatterns
          ]
        , [Char]
    -> Int
    -> [Char]
    -> (EvaluationStrategy -> TTerm -> TCMT IO TTerm)
    -> Pipeline
    compilerPass [Char]
    "id" (Int
    30 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    v) [Char]
    "identity function detection" ((EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline)
    -> (EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline
    forall a b. (a -> b) -> a -> b
    $ (TTerm -> TCMT IO TTerm)
    -> EvaluationStrategy -> TTerm -> TCMT IO TTerm
    forall a b. a -> b -> a
    const (QName -> TTerm -> TCMT IO TTerm
    detectIdentityFunctions QName
    q)
        ]

    runPipeline :: EvaluationStrategy -> QName -> Pipeline -> TTerm -> TCM TTerm
    runPipeline :: EvaluationStrategy -> QName -> Pipeline -> TTerm -> TCMT IO TTerm
    runPipeline EvaluationStrategy
    eval QName
    q Pipeline
    pipeline TTerm
    t = case Pipeline
    pipeline of
      SinglePass CompilerPass
    p   -> EvaluationStrategy
    -> QName -> CompilerPass -> TTerm -> TCMT IO TTerm
    runCompilerPass EvaluationStrategy
    eval QName
    q CompilerPass
    p TTerm
    t
      Sequential [Pipeline]
    ps  -> (TTerm -> Pipeline -> TCMT IO TTerm)
    -> TTerm -> [Pipeline] -> TCMT IO TTerm
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM ((Pipeline -> TTerm -> TCMT IO TTerm)
    -> TTerm -> Pipeline -> TCMT IO TTerm
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ((Pipeline -> TTerm -> TCMT IO TTerm)
     -> TTerm -> Pipeline -> TCMT IO TTerm)
    -> (Pipeline -> TTerm -> TCMT IO TTerm)
    -> TTerm
    -> Pipeline
    -> TCMT IO TTerm
    forall a b. (a -> b) -> a -> b
    $ EvaluationStrategy -> QName -> Pipeline -> TTerm -> TCMT IO TTerm
    runPipeline EvaluationStrategy
    eval QName
    q) TTerm
    t [Pipeline]
    ps
      FixedPoint Int
    n Pipeline
    p -> Int
    -> EvaluationStrategy
    -> QName
    -> Pipeline
    -> TTerm
    -> TCMT IO TTerm
    runFixedPoint Int
    n EvaluationStrategy
    eval QName
    q Pipeline
    p TTerm
    t

    runCompilerPass :: EvaluationStrategy -> QName -> CompilerPass -> TTerm -> TCM TTerm
    runCompilerPass :: EvaluationStrategy
    -> QName -> CompilerPass -> TTerm -> TCMT IO TTerm
    runCompilerPass EvaluationStrategy
    eval QName
    q CompilerPass
    p TTerm
    t = do
      TTerm
    t' <- CompilerPass -> EvaluationStrategy -> TTerm -> TCMT IO TTerm
    passCode CompilerPass
    p EvaluationStrategy
    eval TTerm
    t
      let dbg :: (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO ()
    dbg TCMT IO Doc -> TCMT IO Doc
    f   = [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc ([Char]
    "treeless.opt." [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ CompilerPass -> [Char]
    passTag CompilerPass
    p) (CompilerPass -> Int
    passVerbosity CompilerPass
    p) (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> TCMT IO Doc
    f (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char]
    "-- " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ CompilerPass -> [Char]
    passName CompilerPass
    p)
          pbody :: TTerm -> TCMT IO Doc
    pbody TTerm
    b = [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    q) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "=", Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TTerm -> TCMT IO Doc
    forall a. Pretty a => a -> TCMT IO Doc
    prettyPure TTerm
    b ]
      (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO ()
    dbg ((TCMT IO Doc -> TCMT IO Doc) -> TCMT IO ())
    -> (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ if | TTerm
    t TTerm -> TTerm -> Bool
    forall a. Eq a => a -> a -> Bool
    == TTerm
    t'   -> (TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "(No effect)")
               | Bool
    otherwise -> (TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ TTerm -> TCMT IO Doc
    pbody TTerm
    t')
      TTerm -> TCMT IO TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t'

    runFixedPoint :: Int -> EvaluationStrategy -> QName -> Pipeline -> TTerm -> TCM TTerm
    runFixedPoint :: Int
    -> EvaluationStrategy
    -> QName
    -> Pipeline
    -> TTerm
    -> TCMT IO TTerm
    runFixedPoint Int
    n EvaluationStrategy
    eval QName
    q Pipeline
    pipeline = Int -> TTerm -> TCMT IO TTerm
    go Int
    1
      where
        go :: Int -> TTerm -> TCMT IO TTerm
    go Int
    i TTerm
    t | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    n = do
          [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "treeless.opt.loop" Int
    20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "++ Optimisation loop reached maximum iterations (" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    n [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ")"
          TTerm -> TCMT IO TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t
        go Int
    i TTerm
    t = do
          [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "treeless.opt.loop" Int
    30 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "++ Optimisation loop iteration " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    i
          TTerm
    t' <- EvaluationStrategy -> QName -> Pipeline -> TTerm -> TCMT IO TTerm
    runPipeline EvaluationStrategy
    eval QName
    q Pipeline
    pipeline TTerm
    t
          if | TTerm
    t TTerm -> TTerm -> Bool
    forall a. Eq a => a -> a -> Bool
    == TTerm
    t'   -> do
                [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "treeless.opt.loop" Int
    30 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "++ Optimisation loop terminating after " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    i [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " iterations"
                TTerm -> TCMT IO TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t'
             | Bool
    otherwise -> Int -> TTerm -> TCMT IO TTerm
    go (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) TTerm
    t'

    closedTermToTreeless :: EvaluationStrategy -> I.Term -> TCM C.TTerm
    closedTermToTreeless :: EvaluationStrategy -> Term -> TCMT IO TTerm
    closedTermToTreeless EvaluationStrategy
    eval Term
    t = do
      Term -> CC TTerm
    substTerm Term
    t CC TTerm -> CCEnv -> TCMT IO TTerm
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    `runReaderT` EvaluationStrategy -> CCEnv
    initCCEnv EvaluationStrategy
    eval

    alwaysInline :: QName -> TCM Bool
    alwaysInline :: QName -> TCMT IO Bool
    alwaysInline QName
    q = do
      Defn
    def <- Definition -> Defn
    theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
      Bool -> TCMT IO Bool
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ case Defn
    def of  -- always inline with functions and pattern lambdas
        Function{funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cs} -> (Maybe ExtLamInfo -> Bool
    forall a. Maybe a -> Bool
    isJust (Defn -> Maybe ExtLamInfo
    funExtLam Defn
    def) Bool -> Bool -> Bool
    && Bool -> Bool
    not Bool
    recursive) Bool -> Bool -> Bool
    || Maybe QName -> Bool
    forall a. Maybe a -> Bool
    isJust (Defn -> Maybe QName
    funWith Defn
    def)
                where
                  recursive :: Bool
    recursive = (Clause -> Bool) -> [Clause] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (Bool -> Maybe Bool -> Bool
    forall a. a -> Maybe a -> a
    fromMaybe Bool
    True (Maybe Bool -> Bool) -> (Clause -> Maybe Bool) -> Clause -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> Maybe Bool
    clauseRecursive) [Clause]
    cs
        Defn
    _ -> Bool
    False

    -- | Initial environment for expression generation.
    initCCEnv :: EvaluationStrategy -> CCEnv
    initCCEnv :: EvaluationStrategy -> CCEnv
    initCCEnv EvaluationStrategy
    eval = CCEnv :: [Int] -> Maybe Int -> EvaluationStrategy -> CCEnv
    CCEnv
      { ccCxt :: [Int]
    ccCxt        = []
      , ccCatchAll :: Maybe Int
    ccCatchAll   = Maybe Int
    forall a. Maybe a
    Nothing
      , ccEvaluation :: EvaluationStrategy
    ccEvaluation = EvaluationStrategy
    eval
      }

    -- | Environment for naming of local variables.
    data CCEnv = CCEnv
      { CCEnv -> [Int]
    ccCxt        :: CCContext  -- ^ Maps case tree de-bruijn indices to TTerm de-bruijn indices
      , CCEnv -> Maybe Int
    ccCatchAll   :: Maybe Int  -- ^ TTerm de-bruijn index of the current catch all
      -- If an inner case has no catch-all clause, we use the one from its parent.
      , CCEnv -> EvaluationStrategy
    ccEvaluation :: EvaluationStrategy
      }

    type CCContext = [Int]
    type CC = ReaderT CCEnv TCM

    shift :: Int -> CCContext -> CCContext
    shift :: Int -> [Int] -> [Int]
    shift Int
    n = (Int -> Int) -> [Int] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    n)

    -- | Term variables are de Bruijn indices.
    lookupIndex :: Int -- ^ Case tree de bruijn index.
        -> CCContext
        -> Int -- ^ TTerm de bruijn index.
    lookupIndex :: Int -> [Int] -> Int
    lookupIndex Int
    i [Int]
    xs = Int -> Maybe Int -> Int
    forall a. a -> Maybe a -> a
    fromMaybe Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Int -> Int) -> Maybe Int -> Int
    forall a b. (a -> b) -> a -> b
    $ [Int]
    xs [Int] -> Int -> Maybe Int
    forall a. [a] -> Int -> Maybe a
    !!! Int
    i

    -- | Case variables are de Bruijn levels.
    lookupLevel :: Int -- ^ case tree de bruijn level
        -> CCContext
        -> Int -- ^ TTerm de bruijn index
    lookupLevel :: Int -> [Int] -> Int
    lookupLevel Int
    l [Int]
    xs = Int -> Maybe Int -> Int
    forall a. a -> Maybe a -> a
    fromMaybe Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Int -> Int) -> Maybe Int -> Int
    forall a b. (a -> b) -> a -> b
    $ [Int]
    xs [Int] -> Int -> Maybe Int
    forall a. [a] -> Int -> Maybe a
    !!! ([Int] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Int]
    xs Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    l)

    -- | Compile a case tree into nested case and record expressions.
    casetreeTop :: EvaluationStrategy -> CC.CompiledClauses -> TCM C.TTerm
    casetreeTop :: EvaluationStrategy -> CompiledClauses -> TCMT IO TTerm
    casetreeTop EvaluationStrategy
    eval CompiledClauses
    cc = (CC TTerm -> CCEnv -> TCMT IO TTerm)
    -> CCEnv -> CC TTerm -> TCMT IO TTerm
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip CC TTerm -> CCEnv -> TCMT IO TTerm
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT (EvaluationStrategy -> CCEnv
    initCCEnv EvaluationStrategy
    eval) (CC TTerm -> TCMT IO TTerm) -> CC TTerm -> TCMT IO TTerm
    forall a b. (a -> b) -> a -> b
    $ do
      let a :: Int
    a = CompiledClauses -> Int
    commonArity CompiledClauses
    cc
      TCMT IO () -> ReaderT CCEnv TCM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> ReaderT CCEnv TCM ())
    -> TCMT IO () -> ReaderT CCEnv TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "treeless.convert.arity" Int
    40 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "-- common arity: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    a
      Int -> CC TTerm -> CC TTerm
    lambdasUpTo Int
    a (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
    forall a b. (a -> b) -> a -> b
    $ CompiledClauses -> CC TTerm
    casetree CompiledClauses
    cc

    casetree :: CC.CompiledClauses -> CC C.TTerm
    casetree :: CompiledClauses -> CC TTerm
    casetree CompiledClauses
    cc = do
      case CompiledClauses
    cc of
        CC.Fail [Arg [Char]]
    xs -> Int -> CC TTerm -> CC TTerm
    withContextSize ([Arg [Char]] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Arg [Char]]
    xs) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
    forall a b. (a -> b) -> a -> b
    $ TTerm -> CC TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    C.tUnreachable
        CC.Done [Arg [Char]]
    xs Term
    v -> Int -> CC TTerm -> CC TTerm
    withContextSize ([Arg [Char]] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Arg [Char]]
    xs) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
    forall a b. (a -> b) -> a -> b
    $ do
          -- Issue 2469: Body context size (`length xs`) may be smaller than current context size
          -- if some arguments are not used in the body.
          Term
    v <- TCM Term -> ReaderT CCEnv TCM Term
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (AllowedReductions -> TCM Term -> TCM Term
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    AllowedReductions -> m a -> m a
    putAllowedReductions ([AllowedReduction] -> AllowedReductions
    forall a. SmallSetElement a => [a] -> SmallSet a
    SmallSet.fromList [AllowedReduction
    ProjectionReductions, AllowedReduction
    CopatternReductions]) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
    forall a b. (a -> b) -> a -> b
    $ Term -> TCM Term
    forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
    normalise Term
    v)
          [Int]
    cxt <- (CCEnv -> [Int]) -> ReaderT CCEnv TCM [Int]
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks CCEnv -> [Int]
    ccCxt
          TTerm
    v' <- Term -> CC TTerm
    substTerm Term
    v
          [Char] -> Int -> [TCMT IO Doc] -> ReaderT CCEnv TCM ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    [Char] -> Int -> a -> m ()
    reportS [Char]
    "treeless.convert.casetree" Int
    40 ([TCMT IO Doc] -> ReaderT CCEnv TCM ())
    -> [TCMT IO Doc] -> ReaderT CCEnv TCM ()
    forall a b. (a -> b) -> a -> b
    $
            [ TCMT IO Doc
    "-- casetree, calling substTerm:"
            , TCMT IO Doc
    "--   cxt =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Int] -> TCMT IO Doc
    forall a. Pretty a => a -> TCMT IO Doc
    prettyPure [Int]
    cxt
            , TCMT IO Doc
    "--   v   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a. Pretty a => a -> TCMT IO Doc
    prettyPure Term
    v
            , TCMT IO Doc
    "--   v'  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TTerm -> TCMT IO Doc
    forall a. Pretty a => a -> TCMT IO Doc
    prettyPure TTerm
    v'
            ]
          TTerm -> CC TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    v'
        CC.Case Arg Int
    _ (CC.Branches Bool
    True Map QName (WithArity CompiledClauses)
    _ Maybe (ConHead, WithArity CompiledClauses)
    _ Map Literal CompiledClauses
    _ Just{} Maybe Bool
    _ Bool
    _) -> CC TTerm
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          -- Andreas, 2016-06-03, issue #1986: Ulf: "no catch-all for copatterns!"
          -- lift $ do
          --   typeError . GenericDocError =<< do
          --     "Not yet implemented: compilation of copattern matching with catch-all clause"
        CC.Case (Arg ArgInfo
    _ Int
    n) (CC.Branches Bool
    True Map QName (WithArity CompiledClauses)
    conBrs Maybe (ConHead, WithArity CompiledClauses)
    _ Map Literal CompiledClauses
    _ Maybe CompiledClauses
    Nothing Maybe Bool
    _ Bool
    _) -> Int -> CC TTerm -> CC TTerm
    lambdasUpTo Int
    n (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
    forall a b. (a -> b) -> a -> b
    $ do
          Map QName TTerm -> CC TTerm
    mkRecord (Map QName TTerm -> CC TTerm)
    -> ReaderT CCEnv TCM (Map QName TTerm) -> CC TTerm
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (CompiledClauses -> CC TTerm)
    -> Map QName CompiledClauses -> ReaderT CCEnv TCM (Map QName TTerm)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse CompiledClauses -> CC TTerm
    casetree (WithArity CompiledClauses -> CompiledClauses
    forall c. WithArity c -> c
    CC.content (WithArity CompiledClauses -> CompiledClauses)
    -> Map QName (WithArity CompiledClauses)
    -> Map QName CompiledClauses
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Map QName (WithArity CompiledClauses)
    conBrs)
        CC.Case (Arg ArgInfo
    i Int
    n) (CC.Branches Bool
    False Map QName (WithArity CompiledClauses)
    conBrs Maybe (ConHead, WithArity CompiledClauses)
    etaBr Map Literal CompiledClauses
    litBrs Maybe CompiledClauses
    catchAll Maybe Bool
    _ Bool
    lazy) -> Int -> CC TTerm -> CC TTerm
    lambdasUpTo (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
    forall a b. (a -> b) -> a -> b
    $ do
                        -- We can treat eta-matches as regular matches here.
          let conBrs' :: Map QName (WithArity CompiledClauses)
    conBrs' = Maybe (ConHead, WithArity CompiledClauses)
    -> Map QName (WithArity CompiledClauses)
    -> ((ConHead, WithArity CompiledClauses)
        -> Map QName (WithArity CompiledClauses))
    -> Map QName (WithArity CompiledClauses)
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe (ConHead, WithArity CompiledClauses)
    etaBr Map QName (WithArity CompiledClauses)
    conBrs (((ConHead, WithArity CompiledClauses)
      -> Map QName (WithArity CompiledClauses))
     -> Map QName (WithArity CompiledClauses))
    -> ((ConHead, WithArity CompiledClauses)
        -> Map QName (WithArity CompiledClauses))
    -> Map QName (WithArity CompiledClauses)
    forall a b. (a -> b) -> a -> b
    $ \ (ConHead
    c, WithArity CompiledClauses
    br) -> (WithArity CompiledClauses
     -> WithArity CompiledClauses -> WithArity CompiledClauses)
    -> QName
    -> WithArity CompiledClauses
    -> Map QName (WithArity CompiledClauses)
    -> Map QName (WithArity CompiledClauses)
    forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
    Map.insertWith (\ WithArity CompiledClauses
    new WithArity CompiledClauses
    old -> WithArity CompiledClauses
    old) (ConHead -> QName
    conName ConHead
    c) WithArity CompiledClauses
    br Map QName (WithArity CompiledClauses)
    conBrs
          if Map QName (WithArity CompiledClauses) -> Bool
    forall k a. Map k a -> Bool
    Map.null Map QName (WithArity CompiledClauses)
    conBrs' Bool -> Bool -> Bool
    && Map Literal CompiledClauses -> Bool
    forall k a. Map k a -> Bool
    Map.null Map Literal CompiledClauses
    litBrs then do
            -- there are no branches, just return default
            Maybe CompiledClauses -> CC TTerm -> CC TTerm
    updateCatchAll Maybe CompiledClauses
    catchAll CC TTerm
    fromCatchAll
          else do
            -- Get the type of the scrutinee.
            CaseType
    caseTy <-
              case (Map QName (WithArity CompiledClauses) -> [QName]
    forall k a. Map k a -> [k]
    Map.keys Map QName (WithArity CompiledClauses)
    conBrs', Map Literal CompiledClauses -> [Literal]
    forall k a. Map k a -> [k]
    Map.keys Map Literal CompiledClauses
    litBrs) of
                ([QName]
    cs, []) -> TCM CaseType -> ReaderT CCEnv TCM CaseType
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM CaseType -> ReaderT CCEnv TCM CaseType)
    -> TCM CaseType -> ReaderT CCEnv TCM CaseType
    forall a b. (a -> b) -> a -> b
    $ [QName] -> TCM CaseType
    go [QName]
    cs
                  where
                  go :: [QName] -> TCM CaseType
    go (QName
    c:[QName]
    cs) = QName -> TCM QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    canonicalName QName
    c TCM QName -> (QName -> TCMT IO Definition) -> TCMT IO Definition
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo TCMT IO Definition -> (Definition -> Defn) -> TCMT IO Defn
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> Definition -> Defn
    theDef TCMT IO Defn -> (Defn -> TCM CaseType) -> TCM CaseType
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                    Constructor{QName
    conData :: Defn -> QName
    conData :: QName
    conData} ->
                      CaseType -> TCM CaseType
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CaseType -> TCM CaseType) -> CaseType -> TCM CaseType
    forall a b. (a -> b) -> a -> b
    $ Quantity -> QName -> CaseType
    C.CTData (ArgInfo -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity ArgInfo
    i) QName
    conData
                    Defn
    _ -> [QName] -> TCM CaseType
    go [QName]
    cs
                  go [] = TCM CaseType
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                ([], LitChar   Char
    _ : [Literal]
    _) -> CaseType -> ReaderT CCEnv TCM CaseType
    forall (m :: * -> *) a. Monad m => a -> m a
    return CaseType
    C.CTChar
                ([], LitString Text
    _ : [Literal]
    _) -> CaseType -> ReaderT CCEnv TCM CaseType
    forall (m :: * -> *) a. Monad m => a -> m a
    return CaseType
    C.CTString
                ([], LitFloat  Double
    _ : [Literal]
    _) -> CaseType -> ReaderT CCEnv TCM CaseType
    forall (m :: * -> *) a. Monad m => a -> m a
    return CaseType
    C.CTFloat
                ([], LitQName  QName
    _ : [Literal]
    _) -> CaseType -> ReaderT CCEnv TCM CaseType
    forall (m :: * -> *) a. Monad m => a -> m a
    return CaseType
    C.CTQName
                ([QName], [Literal])
    _ -> ReaderT CCEnv TCM CaseType
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            Maybe CompiledClauses -> CC TTerm -> CC TTerm
    updateCatchAll Maybe CompiledClauses
    catchAll (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
    forall a b. (a -> b) -> a -> b
    $ do
              Int
    x <- (CCEnv -> Int) -> ReaderT CCEnv TCM Int
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (Int -> [Int] -> Int
    lookupLevel Int
    n ([Int] -> Int) -> (CCEnv -> [Int]) -> CCEnv -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CCEnv -> [Int]
    ccCxt)
              TTerm
    def <- CC TTerm
    fromCatchAll
              let caseInfo :: CaseInfo
    caseInfo = CaseInfo :: Bool -> CaseType -> CaseInfo
    C.CaseInfo { caseType :: CaseType
    caseType = CaseType
    caseTy, caseLazy :: Bool
    caseLazy = Bool
    lazy }
              Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
    C.TCase Int
    x CaseInfo
    caseInfo TTerm
    def ([TAlt] -> TTerm) -> ReaderT CCEnv TCM [TAlt] -> CC TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
                [TAlt]
    br1 <- Int
    -> Map QName (WithArity CompiledClauses)
    -> ReaderT CCEnv TCM [TAlt]
    conAlts Int
    n Map QName (WithArity CompiledClauses)
    conBrs'
                [TAlt]
    br2 <- Int -> Map Literal CompiledClauses -> ReaderT CCEnv TCM [TAlt]
    litAlts Int
    n Map Literal CompiledClauses
    litBrs
                [TAlt] -> ReaderT CCEnv TCM [TAlt]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([TAlt]
    br1 [TAlt] -> [TAlt] -> [TAlt]
    forall a. [a] -> [a] -> [a]
    ++ [TAlt]
    br2)
      where
        -- normally, Agda should make sure that a pattern match is total,
        -- so we set the default to unreachable if no default has been provided.
        fromCatchAll :: CC C.TTerm
        fromCatchAll :: CC TTerm
    fromCatchAll = (CCEnv -> TTerm) -> CC TTerm
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (TTerm -> (Int -> TTerm) -> Maybe Int -> TTerm
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe TTerm
    C.tUnreachable Int -> TTerm
    C.TVar (Maybe Int -> TTerm) -> (CCEnv -> Maybe Int) -> CCEnv -> TTerm
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CCEnv -> Maybe Int
    ccCatchAll)

    commonArity :: CC.CompiledClauses -> Int
    commonArity :: CompiledClauses -> Int
    commonArity CompiledClauses
    cc =
      case Int -> CompiledClauses -> [Int]
    forall {a}. Int -> CompiledClauses' a -> [Int]
    arities Int
    0 CompiledClauses
    cc of
        [] -> Int
    0
        [Int]
    as -> [Int] -> Int
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    minimum [Int]
    as
      where
        arities :: Int -> CompiledClauses' a -> [Int]
    arities Int
    cxt (Case (Arg ArgInfo
    _ Int
    x) (Branches Bool
    False Map QName (WithArity (CompiledClauses' a))
    cons Maybe (ConHead, WithArity (CompiledClauses' a))
    eta Map Literal (CompiledClauses' a)
    lits Maybe (CompiledClauses' a)
    def Maybe Bool
    _ Bool
    _)) =
          (WithArity (CompiledClauses' a) -> [Int])
    -> [WithArity (CompiledClauses' a)] -> [Int]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (Int -> WithArity (CompiledClauses' a) -> [Int]
    wArities Int
    cxt') (Map QName (WithArity (CompiledClauses' a))
    -> [WithArity (CompiledClauses' a)]
    forall k a. Map k a -> [a]
    Map.elems Map QName (WithArity (CompiledClauses' a))
    cons) [Int] -> [Int] -> [Int]
    forall a. [a] -> [a] -> [a]
    ++
          ((ConHead, WithArity (CompiledClauses' a)) -> [Int])
    -> [(ConHead, WithArity (CompiledClauses' a))] -> [Int]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ((Int -> WithArity (CompiledClauses' a) -> [Int]
    wArities Int
    cxt') (WithArity (CompiledClauses' a) -> [Int])
    -> ((ConHead, WithArity (CompiledClauses' a))
        -> WithArity (CompiledClauses' a))
    -> (ConHead, WithArity (CompiledClauses' a))
    -> [Int]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ConHead, WithArity (CompiledClauses' a))
    -> WithArity (CompiledClauses' a)
    forall a b. (a, b) -> b
    snd) (Maybe (ConHead, WithArity (CompiledClauses' a))
    -> [(ConHead, WithArity (CompiledClauses' a))]
    forall a. Maybe a -> [a]
    maybeToList Maybe (ConHead, WithArity (CompiledClauses' a))
    eta) [Int] -> [Int] -> [Int]
    forall a. [a] -> [a] -> [a]
    ++
          (CompiledClauses' a -> [Int]) -> [CompiledClauses' a] -> [Int]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (Int -> WithArity (CompiledClauses' a) -> [Int]
    wArities Int
    cxt' (WithArity (CompiledClauses' a) -> [Int])
    -> (CompiledClauses' a -> WithArity (CompiledClauses' a))
    -> CompiledClauses' a
    -> [Int]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> CompiledClauses' a -> WithArity (CompiledClauses' a)
    forall c. Int -> c -> WithArity c
    WithArity Int
    0) (Map Literal (CompiledClauses' a) -> [CompiledClauses' a]
    forall k a. Map k a -> [a]
    Map.elems Map Literal (CompiledClauses' a)
    lits) [Int] -> [Int] -> [Int]
    forall a. [a] -> [a] -> [a]
    ++
          [[Int]] -> [Int]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [ Int -> CompiledClauses' a -> [Int]
    arities Int
    cxt' CompiledClauses' a
    c | Just CompiledClauses' a
    c <- [Maybe (CompiledClauses' a)
    def] ] -- ??
          where cxt' :: Int
    cxt' = Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    max (Int
    x Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) Int
    cxt
        arities Int
    cxt (Case Arg Int
    _ Branches{projPatterns :: forall c. Case c -> Bool
    projPatterns = Bool
    True}) = [Int
    cxt]
        arities Int
    cxt (Done [Arg [Char]]
    xs a
    _) = [Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    max Int
    cxt ([Arg [Char]] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Arg [Char]]
    xs)]
        arities Int
    cxt (Fail [Arg [Char]]
    xs)   = [Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    max Int
    cxt ([Arg [Char]] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Arg [Char]]
    xs)]

        wArities :: Int -> WithArity (CompiledClauses' a) -> [Int]
    wArities Int
    cxt (WithArity Int
    k CompiledClauses' a
    c) = (Int -> Int) -> [Int] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ Int
    x -> Int
    x Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    k Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) ([Int] -> [Int]) -> [Int] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Int -> CompiledClauses' a -> [Int]
    arities (Int
    cxt Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    k) CompiledClauses' a
    c

    updateCatchAll :: Maybe CC.CompiledClauses -> (CC C.TTerm -> CC C.TTerm)
    updateCatchAll :: Maybe CompiledClauses -> CC TTerm -> CC TTerm
    updateCatchAll Maybe CompiledClauses
    Nothing CC TTerm
    cont = CC TTerm
    cont
    updateCatchAll (Just CompiledClauses
    cc) CC TTerm
    cont = do
      TTerm
    def <- CompiledClauses -> CC TTerm
    casetree CompiledClauses
    cc
      [Int]
    cxt <- (CCEnv -> [Int]) -> ReaderT CCEnv TCM [Int]
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks CCEnv -> [Int]
    ccCxt
      [Char] -> Int -> [TCMT IO Doc] -> ReaderT CCEnv TCM ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    [Char] -> Int -> a -> m ()
    reportS [Char]
    "treeless.convert.lambdas" Int
    40 ([TCMT IO Doc] -> ReaderT CCEnv TCM ())
    -> [TCMT IO Doc] -> ReaderT CCEnv TCM ()
    forall a b. (a -> b) -> a -> b
    $
        [ TCMT IO Doc
    "-- updateCatchAll:"
        , TCMT IO Doc
    "--   cxt =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Int] -> TCMT IO Doc
    forall a. Pretty a => a -> TCMT IO Doc
    prettyPure [Int]
    cxt
        , TCMT IO Doc
    "--   def =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TTerm -> TCMT IO Doc
    forall a. Pretty a => a -> TCMT IO Doc
    prettyPure TTerm
    def
        ]
      (CCEnv -> CCEnv) -> CC TTerm -> CC TTerm
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (\ CCEnv
    e -> CCEnv
    e { ccCatchAll :: Maybe Int
    ccCatchAll = Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    0, ccCxt :: [Int]
    ccCxt = Int -> [Int] -> [Int]
    shift Int
    1 [Int]
    cxt }) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
    forall a b. (a -> b) -> a -> b
    $ do
        TTerm -> TTerm -> TTerm
    C.mkLet TTerm
    def (TTerm -> TTerm) -> CC TTerm -> CC TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> CC TTerm
    cont

    -- | Shrinks or grows the context to the given size.
    -- Does not update the catchAll expression, the catchAll expression
    -- MUST NOT be used inside `cont`.
    withContextSize :: Int -> CC C.TTerm -> CC C.TTerm
    withContextSize :: Int -> CC TTerm -> CC TTerm
    withContextSize Int
    n CC TTerm
    cont = do
      Int
    diff <- (CCEnv -> Int) -> ReaderT CCEnv TCM Int
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (((Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    -) (Int -> Int) -> ([Int] -> Int) -> [Int] -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Int] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length) ([Int] -> Int) -> (CCEnv -> [Int]) -> CCEnv -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CCEnv -> [Int]
    ccCxt)
      if Int
    diff Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    1 then Int -> CC TTerm -> CC TTerm
    createLambdas Int
    diff CC TTerm
    cont else do
        let diff' :: Int
    diff' = -Int
    diff
        [Int]
    cxt <- -- shift diff .
           -- Andreas, 2021-04-10, issue #5288
           -- The @shift diff@ is wrong, since we are returning to the original
           -- context from @cont@, and then we would have to reverse
           -- the effect of @shift diff@.
           -- We need to make sure that the result of @cont@ make sense
           -- in the **present** context, not the changed context
           -- where it is constructed.
           --
           -- Ulf, 2021-04-12, https://github.com/agda/agda/pull/5311/files#r611452551
           --
           -- This looks correct, but I can't quite follow the explanation. Here's my understanding:
           --
           -- We are building a `TTerm` case tree from `CompiledClauses`. In order
           -- to be able to match we bind all variables we'll need in a top-level
           -- lambda `λ a b c d → ..` (say). As we compute the `TTerm` we keep a
           -- context (list) of `TTerm` deBruijn indices for each `CompiledClause`
           -- variable. This is a renaming from the *source* context of the
           -- `CompiledClause` to the *target* context of the `TTerm`.
           --
           -- After some pattern matching we might have
           -- ```
           -- λ a b c d →
           --   case c of
           --     e :: f → {cxt = [d, f, e, b, a]}
           -- ```
           -- Now, what's causing the problems here is that `CompiledClauses` can be
           -- underapplied, so you might have matched on a variable only to find
           -- that in the catch-all the variable you matched on is bound in a lambda
           -- in the right-hand side! Extending the example, we might have
           -- `CompiledClauses` looking like this:
           -- ```
           -- case 2 of
           --   _::_ → done[d, f, e, b, a] ...
           --   _    → done[b, a] (λ c d → ...)
           -- ```
           -- When we get to the catch-all, the context will be `[d, c, b, a]` but
           -- the right-hand side is only expecting `a` and `b` to be bound. What we
           -- need to do is compile the right-hand side and then apply it to the
           -- variables `c` and `d` that we already bound. This is what
           -- `withContextSize` does.
           --
           -- Crucially (and this is where the bug was), we are not changing the
           -- target context, only the source context (we want a `TTerm` that makes
           -- sense at this point). This means that the correct move is to drop the
           -- entries for the additional source variables, but not change what
           -- target variables the remaining source variables map to. Hence, `drop`
           -- but no `shift`.
           --
           Int -> [Int] -> [Int]
    forall a. Int -> [a] -> [a]
    drop Int
    diff' ([Int] -> [Int])
    -> ReaderT CCEnv TCM [Int] -> ReaderT CCEnv TCM [Int]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (CCEnv -> [Int]) -> ReaderT CCEnv TCM [Int]
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks CCEnv -> [Int]
    ccCxt
        (CCEnv -> CCEnv) -> CC TTerm -> CC TTerm
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (\ CCEnv
    e -> CCEnv
    e { ccCxt :: [Int]
    ccCxt = [Int]
    cxt }) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
    forall a b. (a -> b) -> a -> b
    $ do
          [Char] -> Int -> [TCMT IO Doc] -> ReaderT CCEnv TCM ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    [Char] -> Int -> a -> m ()
    reportS [Char]
    "treeless.convert.lambdas" Int
    40 ([TCMT IO Doc] -> ReaderT CCEnv TCM ())
    -> [TCMT IO Doc] -> ReaderT CCEnv TCM ()
    forall a b. (a -> b) -> a -> b
    $
            [ TCMT IO Doc
    "-- withContextSize:"
            , TCMT IO Doc
    "--   n   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Int -> TCMT IO Doc
    forall a. Pretty a => a -> TCMT IO Doc
    prettyPure Int
    n
            , TCMT IO Doc
    "--   diff=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Int -> TCMT IO Doc
    forall a. Pretty a => a -> TCMT IO Doc
    prettyPure Int
    diff
            , TCMT IO Doc
    "--   cxt =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Int] -> TCMT IO Doc
    forall a. Pretty a => a -> TCMT IO Doc
    prettyPure [Int]
    cxt
            ]
          CC TTerm
    cont CC TTerm -> (TTerm -> TTerm) -> CC TTerm
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> (TTerm -> Args -> TTerm
    `C.mkTApp` (Int -> TTerm) -> [Int] -> Args
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> TTerm
    C.TVar (Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    diff'))

    -- | Prepend the given positive number of lambdas.
    -- Does not update the catchAll expression,
    -- the catchAll expression must be updated separately (or not be used).
    createLambdas :: Int -> CC C.TTerm -> CC C.TTerm
    createLambdas :: Int -> CC TTerm -> CC TTerm
    createLambdas Int
    diff CC TTerm
    cont = do
      Bool -> ReaderT CCEnv TCM () -> ReaderT CCEnv TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Int
    diff Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    1) ReaderT CCEnv TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      [Int]
    cxt <- ([Int
    0 .. Int
    diffInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1] [Int] -> [Int] -> [Int]
    forall a. [a] -> [a] -> [a]
    ++) ([Int] -> [Int]) -> ([Int] -> [Int]) -> [Int] -> [Int]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> [Int] -> [Int]
    shift Int
    diff ([Int] -> [Int])
    -> ReaderT CCEnv TCM [Int] -> ReaderT CCEnv TCM [Int]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (CCEnv -> [Int]) -> ReaderT CCEnv TCM [Int]
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks CCEnv -> [Int]
    ccCxt
      (CCEnv -> CCEnv) -> CC TTerm -> CC TTerm
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (\ CCEnv
    e -> CCEnv
    e { ccCxt :: [Int]
    ccCxt = [Int]
    cxt }) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
    forall a b. (a -> b) -> a -> b
    $ do
        [Char] -> Int -> [TCMT IO Doc] -> ReaderT CCEnv TCM ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    [Char] -> Int -> a -> m ()
    reportS [Char]
    "treeless.convert.lambdas" Int
    40 ([TCMT IO Doc] -> ReaderT CCEnv TCM ())
    -> [TCMT IO Doc] -> ReaderT CCEnv TCM ()
    forall a b. (a -> b) -> a -> b
    $
          [ TCMT IO Doc
    "-- createLambdas:"
          , TCMT IO Doc
    "--   diff =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Int -> TCMT IO Doc
    forall a. Pretty a => a -> TCMT IO Doc
    prettyPure Int
    diff
          , TCMT IO Doc
    "--   cxt  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Int] -> TCMT IO Doc
    forall a. Pretty a => a -> TCMT IO Doc
    prettyPure [Int]
    cxt
          ]
        -- Prepend diff lambdas
        CC TTerm
    cont CC TTerm -> (TTerm -> TTerm) -> CC TTerm
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ TTerm
    t -> (TTerm -> TTerm) -> TTerm -> Args
    forall a. (a -> a) -> a -> [a]
    List.iterate TTerm -> TTerm
    C.TLam TTerm
    t Args -> Int -> TTerm
    forall a. [a] -> Int -> a
    !! Int
    diff

    -- | Adds lambdas until the context has at least the given size.
    -- Updates the catchAll expression to take the additional lambdas into account.
    lambdasUpTo :: Int -> CC C.TTerm -> CC C.TTerm
    lambdasUpTo :: Int -> CC TTerm -> CC TTerm
    lambdasUpTo Int
    n CC TTerm
    cont = do
      Int
    diff <- (CCEnv -> Int) -> ReaderT CCEnv TCM Int
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (((Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    -) (Int -> Int) -> ([Int] -> Int) -> [Int] -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Int] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length) ([Int] -> Int) -> (CCEnv -> [Int]) -> CCEnv -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CCEnv -> [Int]
    ccCxt)

      if Int
    diff Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    0 then CC TTerm
    cont -- no new lambdas needed
      else do
        Int -> CC TTerm -> CC TTerm
    createLambdas Int
    diff (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
    forall a b. (a -> b) -> a -> b
    $ do
          (CCEnv -> Maybe Int) -> ReaderT CCEnv TCM (Maybe Int)
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks CCEnv -> Maybe Int
    ccCatchAll ReaderT CCEnv TCM (Maybe Int)
    -> (Maybe Int -> CC TTerm) -> CC TTerm
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Just Int
    catchAll -> do
              [Int]
    cxt <- (CCEnv -> [Int]) -> ReaderT CCEnv TCM [Int]
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks CCEnv -> [Int]
    ccCxt
              [Char] -> Int -> [TCMT IO Doc] -> ReaderT CCEnv TCM ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    [Char] -> Int -> a -> m ()
    reportS [Char]
    "treeless.convert.lambdas" Int
    40 ([TCMT IO Doc] -> ReaderT CCEnv TCM ())
    -> [TCMT IO Doc] -> ReaderT CCEnv TCM ()
    forall a b. (a -> b) -> a -> b
    $
                [ TCMT IO Doc
    "lambdasUpTo: n =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> (Int -> [Char]) -> Int -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> [Char]
    forall a. Show a => a -> [Char]
    show) Int
    n
                , TCMT IO Doc
    "  diff         =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> (Int -> [Char]) -> Int -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> [Char]
    forall a. Show a => a -> [Char]
    show) Int
    n
                , TCMT IO Doc
    "  catchAll     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Int -> TCMT IO Doc
    forall a. Pretty a => a -> TCMT IO Doc
    prettyPure Int
    catchAll
                , TCMT IO Doc
    "  ccCxt        =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Int] -> TCMT IO Doc
    forall a. Pretty a => a -> TCMT IO Doc
    prettyPure [Int]
    cxt
                ]
              -- the catch all doesn't know about the additional lambdas, so just directly
              -- apply it again to the newly introduced lambda arguments.
              -- we also bind the catch all to a let, to avoid code duplication
              (CCEnv -> CCEnv) -> CC TTerm -> CC TTerm
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (\CCEnv
    e -> CCEnv
    e { ccCatchAll :: Maybe Int
    ccCatchAll = Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    0
                             , ccCxt :: [Int]
    ccCxt = Int -> [Int] -> [Int]
    shift Int
    1 [Int]
    cxt }) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
    forall a b. (a -> b) -> a -> b
    $ do
                let catchAllArgs :: Args
    catchAllArgs = (Int -> TTerm) -> [Int] -> Args
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> TTerm
    C.TVar ([Int] -> Args) -> [Int] -> Args
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    diff
                TTerm -> TTerm -> TTerm
    C.mkLet (TTerm -> Args -> TTerm
    C.mkTApp (Int -> TTerm
    C.TVar (Int -> TTerm) -> Int -> TTerm
    forall a b. (a -> b) -> a -> b
    $ Int
    catchAll Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    diff) Args
    catchAllArgs)
                  (TTerm -> TTerm) -> CC TTerm -> CC TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> CC TTerm
    cont
            Maybe Int
    Nothing -> CC TTerm
    cont

    conAlts :: Int -> Map QName (CC.WithArity CC.CompiledClauses) -> CC [C.TAlt]
    conAlts :: Int
    -> Map QName (WithArity CompiledClauses)
    -> ReaderT CCEnv TCM [TAlt]
    conAlts Int
    x Map QName (WithArity CompiledClauses)
    br = [(QName, WithArity CompiledClauses)]
    -> ((QName, WithArity CompiledClauses) -> ReaderT CCEnv TCM TAlt)
    -> ReaderT CCEnv TCM [TAlt]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM (Map QName (WithArity CompiledClauses)
    -> [(QName, WithArity CompiledClauses)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map QName (WithArity CompiledClauses)
    br) (((QName, WithArity CompiledClauses) -> ReaderT CCEnv TCM TAlt)
     -> ReaderT CCEnv TCM [TAlt])
    -> ((QName, WithArity CompiledClauses) -> ReaderT CCEnv TCM TAlt)
    -> ReaderT CCEnv TCM [TAlt]
    forall a b. (a -> b) -> a -> b
    $ \ (QName
    c, CC.WithArity Int
    n CompiledClauses
    cc) -> do
      QName
    c' <- TCM QName -> ReaderT CCEnv TCM QName
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM QName -> ReaderT CCEnv TCM QName)
    -> TCM QName -> ReaderT CCEnv TCM QName
    forall a b. (a -> b) -> a -> b
    $ QName -> TCM QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    canonicalName QName
    c
      Int -> Int -> ReaderT CCEnv TCM TAlt -> ReaderT CCEnv TCM TAlt
    forall a. Int -> Int -> CC a -> CC a
    replaceVar Int
    x Int
    n (ReaderT CCEnv TCM TAlt -> ReaderT CCEnv TCM TAlt)
    -> ReaderT CCEnv TCM TAlt -> ReaderT CCEnv TCM TAlt
    forall a b. (a -> b) -> a -> b
    $ do
        (TTerm -> TAlt) -> CompiledClauses -> ReaderT CCEnv TCM TAlt
    branch (QName -> Int -> TTerm -> TAlt
    C.TACon QName
    c' Int
    n) CompiledClauses
    cc

    litAlts :: Int -> Map Literal CC.CompiledClauses -> CC [C.TAlt]
    litAlts :: Int -> Map Literal CompiledClauses -> ReaderT CCEnv TCM [TAlt]
    litAlts Int
    x Map Literal CompiledClauses
    br = [(Literal, CompiledClauses)]
    -> ((Literal, CompiledClauses) -> ReaderT CCEnv TCM TAlt)
    -> ReaderT CCEnv TCM [TAlt]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM (Map Literal CompiledClauses -> [(Literal, CompiledClauses)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map Literal CompiledClauses
    br) (((Literal, CompiledClauses) -> ReaderT CCEnv TCM TAlt)
     -> ReaderT CCEnv TCM [TAlt])
    -> ((Literal, CompiledClauses) -> ReaderT CCEnv TCM TAlt)
    -> ReaderT CCEnv TCM [TAlt]
    forall a b. (a -> b) -> a -> b
    $ \ (Literal
    l, CompiledClauses
    cc) ->
      -- Issue1624: we need to drop the case scrutinee from the environment here!
      Int -> Int -> ReaderT CCEnv TCM TAlt -> ReaderT CCEnv TCM TAlt
    forall a. Int -> Int -> CC a -> CC a
    replaceVar Int
    x Int
    0 (ReaderT CCEnv TCM TAlt -> ReaderT CCEnv TCM TAlt)
    -> ReaderT CCEnv TCM TAlt -> ReaderT CCEnv TCM TAlt
    forall a b. (a -> b) -> a -> b
    $ do
        (TTerm -> TAlt) -> CompiledClauses -> ReaderT CCEnv TCM TAlt
    branch (Literal -> TTerm -> TAlt
    C.TALit Literal
    l ) CompiledClauses
    cc

    branch :: (C.TTerm -> C.TAlt) -> CC.CompiledClauses -> CC C.TAlt
    branch :: (TTerm -> TAlt) -> CompiledClauses -> ReaderT CCEnv TCM TAlt
    branch TTerm -> TAlt
    alt CompiledClauses
    cc = TTerm -> TAlt
    alt (TTerm -> TAlt) -> CC TTerm -> ReaderT CCEnv TCM TAlt
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> CompiledClauses -> CC TTerm
    casetree CompiledClauses
    cc

    -- | Replace de Bruijn Level @x@ by @n@ new variables.
    replaceVar :: Int -> Int -> CC a -> CC a
    replaceVar :: forall a. Int -> Int -> CC a -> CC a
    replaceVar Int
    x Int
    n CC a
    cont = do
      let upd :: [Int] -> [Int]
    upd [Int]
    cxt = Int -> [Int] -> [Int]
    shift Int
    n [Int]
    ys [Int] -> [Int] -> [Int]
    forall a. [a] -> [a] -> [a]
    ++ [Int]
    ixs [Int] -> [Int] -> [Int]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Int] -> [Int]
    shift Int
    n [Int]
    zs
           where
             -- compute the de Bruijn index
             i :: Int
    i = [Int] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Int]
    cxt Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    x
             -- discard index i
             ([Int]
    ys, Int
    _:[Int]
    zs) = Int -> [Int] -> ([Int], [Int])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    i [Int]
    cxt
             -- compute the de-bruijn indexes of the newly inserted variables
             ixs :: [Int]
    ixs = [Int
    0..(Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1)]
      (CCEnv -> CCEnv) -> CC a -> CC a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (\CCEnv
    e -> CCEnv
    e { ccCxt :: [Int]
    ccCxt = [Int] -> [Int]
    upd (CCEnv -> [Int]
    ccCxt CCEnv
    e) , ccCatchAll :: Maybe Int
    ccCatchAll = (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    n) (Int -> Int) -> Maybe Int -> Maybe Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> CCEnv -> Maybe Int
    ccCatchAll CCEnv
    e }) (CC a -> CC a) -> CC a -> CC a
    forall a b. (a -> b) -> a -> b
    $
        CC a
    cont

    -- | Precondition: Map not empty.
    mkRecord :: Map QName C.TTerm -> CC C.TTerm
    mkRecord :: Map QName TTerm -> CC TTerm
    mkRecord Map QName TTerm
    fs = TCMT IO TTerm -> CC TTerm
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO TTerm -> CC TTerm) -> TCMT IO TTerm -> CC TTerm
    forall a b. (a -> b) -> a -> b
    $ do
      -- Get the name of the first field
      let p1 :: QName
    p1 = (QName, TTerm) -> QName
    forall a b. (a, b) -> a
    fst ((QName, TTerm) -> QName) -> (QName, TTerm) -> QName
    forall a b. (a -> b) -> a -> b
    $ (QName, TTerm) -> [(QName, TTerm)] -> (QName, TTerm)
    forall a. a -> [a] -> a
    headWithDefault (QName, TTerm)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([(QName, TTerm)] -> (QName, TTerm))
    -> [(QName, TTerm)] -> (QName, TTerm)
    forall a b. (a -> b) -> a -> b
    $ Map QName TTerm -> [(QName, TTerm)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map QName TTerm
    fs
      -- Use the field name to get the record constructor and the field names.
      I.ConHead QName
    c IsRecord{} Induction
    _ind [Arg QName]
    xs <- Defn -> ConHead
    conSrcCon (Defn -> ConHead) -> (Definition -> Defn) -> Definition -> ConHead
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef (Definition -> ConHead) -> TCMT IO Definition -> TCMT IO ConHead
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo (QName -> TCMT IO Definition) -> TCM QName -> TCMT IO Definition
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> TCM QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    canonicalName (QName -> TCM QName) -> (ConHead -> QName) -> ConHead -> TCM QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ConHead -> QName
    I.conName (ConHead -> TCM QName) -> TCMT IO ConHead -> TCM QName
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> TCMT IO ConHead
    recConFromProj QName
    p1)
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "treeless.convert.mkRecord" Int
    60 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text [Char]
    "record constructor fields: xs      = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> ([Arg QName] -> [Char]) -> [Arg QName] -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Arg QName] -> [Char]
    forall a. Show a => a -> [Char]
    show) [Arg QName]
    xs
        , [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text [Char]
    "to be filled with content: keys fs = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> ([QName] -> [Char]) -> [QName] -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [QName] -> [Char]
    forall a. Show a => a -> [Char]
    show) (Map QName TTerm -> [QName]
    forall k a. Map k a -> [k]
    Map.keys Map QName TTerm
    fs)
        ]
      -- Convert the constructor
      let (Args
    args :: [C.TTerm]) = [Arg QName] -> (Arg QName -> TTerm) -> Args
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for [Arg QName]
    xs ((Arg QName -> TTerm) -> Args) -> (Arg QName -> TTerm) -> Args
    forall a b. (a -> b) -> a -> b
    $ \ Arg QName
    x -> TTerm -> QName -> Map QName TTerm -> TTerm
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault TTerm
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Arg QName -> QName
    forall e. Arg e -> e
    unArg Arg QName
    x) Map QName TTerm
    fs
      TTerm -> TCMT IO TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TTerm -> TCMT IO TTerm) -> TTerm -> TCMT IO TTerm
    forall a b. (a -> b) -> a -> b
    $ TTerm -> Args -> TTerm
    C.mkTApp (QName -> TTerm
    C.TCon QName
    c) Args
    args

    recConFromProj :: QName -> TCM I.ConHead
    recConFromProj :: QName -> TCMT IO ConHead
    recConFromProj QName
    q = do
      TCMT IO (Maybe Projection)
    -> TCMT IO ConHead
    -> (Projection -> TCMT IO ConHead)
    -> TCMT IO ConHead
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (QName -> TCMT IO (Maybe Projection)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe Projection)
    isProjection QName
    q) TCMT IO ConHead
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ((Projection -> TCMT IO ConHead) -> TCMT IO ConHead)
    -> (Projection -> TCMT IO ConHead) -> TCMT IO ConHead
    forall a b. (a -> b) -> a -> b
    $ \ Projection
    proj -> do
        -- Get the record type name @d@ from the projection.
        let d :: QName
    d = Arg QName -> QName
    forall e. Arg e -> e
    unArg (Arg QName -> QName) -> Arg QName -> QName
    forall a b. (a -> b) -> a -> b
    $ Projection -> Arg QName
    projFromType Projection
    proj
        QName -> TCMT IO ConHead
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
    QName -> m ConHead
    getRecordConstructor QName
    d

    -- | Translate the actual Agda terms, with an environment of all the bound variables
    --   from patternmatching. Agda terms are in de Bruijn indices, but the expected
    --   TTerm de bruijn indexes may differ. This is due to additional let-bindings
    --   introduced by the catch-all machinery, so we need to lookup casetree de bruijn
    --   indices in the environment as well.
    substTerm :: I.Term -> CC C.TTerm
    substTerm :: Term -> CC TTerm
    substTerm Term
    term = Term -> ReaderT CCEnv TCM Term
    normaliseStatic Term
    term ReaderT CCEnv TCM Term -> (Term -> CC TTerm) -> CC TTerm
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ Term
    term ->
      case Term -> Term
    I.unSpine (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Term
    etaContractErased Term
    term of
        I.Var Int
    ind Elims
    es -> do
          Int
    ind' <- (CCEnv -> Int) -> ReaderT CCEnv TCM Int
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (Int -> [Int] -> Int
    lookupIndex Int
    ind ([Int] -> Int) -> (CCEnv -> [Int]) -> CCEnv -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CCEnv -> [Int]
    ccCxt)
          let args :: [Arg Term]
    args = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    I.allApplyElims Elims
    es
          TTerm -> Args -> TTerm
    C.mkTApp (Int -> TTerm
    C.TVar Int
    ind') (Args -> TTerm) -> ReaderT CCEnv TCM Args -> CC TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Arg Term] -> ReaderT CCEnv TCM Args
    substArgs [Arg Term]
    args
        I.Lam ArgInfo
    _ Abs Term
    ab ->
          TTerm -> TTerm
    C.TLam (TTerm -> TTerm) -> CC TTerm -> CC TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
            (CCEnv -> CCEnv) -> CC TTerm -> CC TTerm
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (\CCEnv
    e -> CCEnv
    e { ccCxt :: [Int]
    ccCxt = Int
    0 Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : Int -> [Int] -> [Int]
    shift Int
    1 (CCEnv -> [Int]
    ccCxt CCEnv
    e) })
              (Term -> CC TTerm
    substTerm (Term -> CC TTerm) -> Term -> CC TTerm
    forall a b. (a -> b) -> a -> b
    $ Abs Term -> Term
    forall a. Abs a -> a
    I.unAbs Abs Term
    ab)
        I.Lit Literal
    l -> TTerm -> CC TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TTerm -> CC TTerm) -> TTerm -> CC TTerm
    forall a b. (a -> b) -> a -> b
    $ Literal -> TTerm
    C.TLit Literal
    l
        I.Level Level
    _ -> TTerm -> CC TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    C.TUnit
        I.Def QName
    q Elims
    es -> do
          let args :: [Arg Term]
    args = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    I.allApplyElims Elims
    es
          QName -> [Arg Term] -> CC TTerm
    maybeInlineDef QName
    q [Arg Term]
    args
        I.Con ConHead
    c ConInfo
    ci Elims
    es -> do
            let args :: [Arg Term]
    args = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    I.allApplyElims Elims
    es
            QName
    c' <- TCM QName -> ReaderT CCEnv TCM QName
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM QName -> ReaderT CCEnv TCM QName)
    -> TCM QName -> ReaderT CCEnv TCM QName
    forall a b. (a -> b) -> a -> b
    $ QName -> TCM QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    canonicalName (QName -> TCM QName) -> QName -> TCM QName
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    I.conName ConHead
    c
            TTerm -> Args -> TTerm
    C.mkTApp (QName -> TTerm
    C.TCon QName
    c') (Args -> TTerm) -> ReaderT CCEnv TCM Args -> CC TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Arg Term] -> ReaderT CCEnv TCM Args
    substArgs [Arg Term]
    args
        I.Pi Dom Type
    _ Abs Type
    _ -> TTerm -> CC TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    C.TUnit
        I.Sort Sort
    _  -> TTerm -> CC TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    C.TSort
        I.MetaV MetaId
    x Elims
    _ -> TTerm -> CC TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TTerm -> CC TTerm) -> TTerm -> CC TTerm
    forall a b. (a -> b) -> a -> b
    $ TError -> TTerm
    C.TError (TError -> TTerm) -> TError -> TTerm
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TError
    C.TMeta ([Char] -> TError) -> [Char] -> TError
    forall a b. (a -> b) -> a -> b
    $ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    x
        I.DontCare Term
    _ -> TTerm -> CC TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    C.TErased
        I.Dummy{} -> CC TTerm
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- Andreas, 2019-07-10, issue #3792
    -- | Eta-contract erased lambdas.
    --
    -- Should also be fine for strict backends:
    --
    --   * eta-contraction is semantics-preserving for total, effect-free languages.
    --   * should a user rely on thunking, better not used an erased abstraction!
    --
    -- A live-or-death issue for the GHC 8.0 backend.  Consider:
    -- @
    --   foldl : ∀ {A} (B : Nat → Set)
    --         → (f : ∀ {@0 n} → B n → A → B (suc n))
    --         → (z : B 0)
    --         → ∀ {@0 n} → Vec A n → B n
    --   foldl B f z (x ∷ xs) = foldl (λ n → B (suc n)) (λ{@0 x} → f {suc x}) (f z x) xs
    --   foldl B f z [] = z
    -- @
    -- The hidden composition of @f@ with @suc@, term @(λ{@0 x} → f {suc x})@,
    -- can be eta-contracted to just @f@ by the compiler, since the first argument
    -- of @f@ is erased.
    --
    -- GHC >= 8.2 seems to be able to do the optimization himself, but not 8.0.
    --
    etaContractErased :: I.Term -> I.Term
    etaContractErased :: Term -> Term
    etaContractErased = (Term -> Either Term Term) -> Term -> Term
    forall a b. (a -> Either b a) -> a -> b
    trampoline Term -> Either Term Term
    etaErasedOnce
      where
      etaErasedOnce :: I.Term -> Either I.Term I.Term  -- Left = done, Right = jump again
      etaErasedOnce :: Term -> Either Term Term
    etaErasedOnce Term
    t =
        case Term
    t of

          -- If the abstraction is void, we don't have to strengthen.
          I.Lam ArgInfo
    _ (NoAbs [Char]
    _ Term
    v) ->
            case Term -> BinAppView
    binAppView Term
    v of
              -- If the body is an application ending with an erased argument, eta-reduce!
              App Term
    u Arg Term
    arg | Bool -> Bool
    not (Arg Term -> Bool
    forall a. LensModality a => a -> Bool
    usableModality Arg Term
    arg) -> Term -> Either Term Term
    forall a b. b -> Either a b
    Right Term
    u
              BinAppView
    _ -> Either Term Term
    done

          -- If the abstraction is non-void, only eta-contract if erased.
          I.Lam ArgInfo
    ai (Abs [Char]
    _ Term
    v) | Bool -> Bool
    not (ArgInfo -> Bool
    forall a. LensModality a => a -> Bool
    usableModality ArgInfo
    ai) ->
            case Term -> BinAppView
    binAppView Term
    v of
              -- If the body is an application ending with an erased argument, eta-reduce!
              -- We need to strengthen the function part then.
              App Term
    u Arg Term
    arg | Bool -> Bool
    not (Arg Term -> Bool
    forall a. LensModality a => a -> Bool
    usableModality Arg Term
    arg) -> Term -> Either Term Term
    forall a b. b -> Either a b
    Right (Term -> Either Term Term) -> Term -> Either Term Term
    forall a b. (a -> b) -> a -> b
    $ Int -> SubstArg Term -> Term -> Term
    forall a. Subst a => Int -> SubstArg a -> a -> a
    subst Int
    0 (Term -> Term
    DontCare Term
    HasCallStack => Term
    __DUMMY_TERM__) Term
    u
              BinAppView
    _ -> Either Term Term
    done

          Term
    _ -> Either Term Term
    done
        where
        done :: Either Term Term
    done = Term -> Either Term Term
    forall a b. a -> Either a b
    Left Term
    t

    normaliseStatic :: I.Term -> CC I.Term
    normaliseStatic :: Term -> ReaderT CCEnv TCM Term
    normaliseStatic v :: Term
    v@(I.Def QName
    f Elims
    es) = TCM Term -> ReaderT CCEnv TCM Term
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM Term -> ReaderT CCEnv TCM Term)
    -> TCM Term -> ReaderT CCEnv TCM Term
    forall a b. (a -> b) -> a -> b
    $ do
      Bool
    static <- Defn -> Bool
    isStaticFun (Defn -> Bool) -> (Definition -> Defn) -> Definition -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef (Definition -> Bool) -> TCMT IO Definition -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
      if Bool
    static then Term -> TCM Term
    forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
    normalise Term
    v else Term -> TCM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    v
    normaliseStatic Term
    v = Term -> ReaderT CCEnv TCM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    v

    maybeInlineDef :: I.QName -> I.Args -> CC C.TTerm
    maybeInlineDef :: QName -> [Arg Term] -> CC TTerm
    maybeInlineDef QName
    q [Arg Term]
    vs = do
      EvaluationStrategy
    eval <- (CCEnv -> EvaluationStrategy)
    -> ReaderT CCEnv TCM EvaluationStrategy
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks CCEnv -> EvaluationStrategy
    ccEvaluation
      ReaderT CCEnv TCM Bool -> CC TTerm -> CC TTerm -> CC TTerm
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (TCMT IO Bool -> ReaderT CCEnv TCM Bool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO Bool -> ReaderT CCEnv TCM Bool)
    -> TCMT IO Bool -> ReaderT CCEnv TCM Bool
    forall a b. (a -> b) -> a -> b
    $ QName -> TCMT IO Bool
    alwaysInline QName
    q) (EvaluationStrategy -> CC TTerm
    doinline EvaluationStrategy
    eval) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
    forall a b. (a -> b) -> a -> b
    $ do
        TCMT IO () -> ReaderT CCEnv TCM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> ReaderT CCEnv TCM ())
    -> TCMT IO () -> ReaderT CCEnv TCM ()
    forall a b. (a -> b) -> a -> b
    $ EvaluationStrategy -> QName -> TCMT IO ()
    cacheTreeless EvaluationStrategy
    eval QName
    q
        Definition
    def <- TCMT IO Definition -> ReaderT CCEnv TCM Definition
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO Definition -> ReaderT CCEnv TCM Definition)
    -> TCMT IO Definition -> ReaderT CCEnv TCM Definition
    forall a b. (a -> b) -> a -> b
    $ QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
        case Definition -> Defn
    theDef Definition
    def of
          fun :: Defn
    fun@Function{}
            | Defn
    fun Defn -> Lens' Bool Defn -> Bool
    forall o i. o -> Lens' i o -> i
    ^. Lens' Bool Defn
    funInline -> EvaluationStrategy -> CC TTerm
    doinline EvaluationStrategy
    eval
            | Bool
    otherwise -> do
            -- If ArgUsage hasn't been computed yet, we assume all arguments are used.
            [ArgUsage]
    used <- TCM [ArgUsage] -> ReaderT CCEnv TCM [ArgUsage]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM [ArgUsage] -> ReaderT CCEnv TCM [ArgUsage])
    -> TCM [ArgUsage] -> ReaderT CCEnv TCM [ArgUsage]
    forall a b. (a -> b) -> a -> b
    $ [ArgUsage] -> Maybe [ArgUsage] -> [ArgUsage]
    forall a. a -> Maybe a -> a
    fromMaybe [] (Maybe [ArgUsage] -> [ArgUsage])
    -> TCMT IO (Maybe [ArgUsage]) -> TCM [ArgUsage]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO (Maybe [ArgUsage])
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe [ArgUsage])
    getCompiledArgUse QName
    q
            let substUsed :: Arg Term -> ArgUsage -> CC TTerm
    substUsed Arg Term
    _   ArgUsage
    ArgUnused = TTerm -> CC TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    C.TErased
                substUsed Arg Term
    arg ArgUsage
    ArgUsed   = Arg Term -> CC TTerm
    substArg Arg Term
    arg
            TTerm -> Args -> TTerm
    C.mkTApp (QName -> TTerm
    C.TDef QName
    q) (Args -> TTerm) -> ReaderT CCEnv TCM Args -> CC TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Arg Term -> ArgUsage -> CC TTerm)
    -> [Arg Term] -> [ArgUsage] -> ReaderT CCEnv TCM Args
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM Arg Term -> ArgUsage -> CC TTerm
    substUsed [Arg Term]
    vs ([ArgUsage]
    used [ArgUsage] -> [ArgUsage] -> [ArgUsage]
    forall a. [a] -> [a] -> [a]
    ++ ArgUsage -> [ArgUsage]
    forall a. a -> [a]
    repeat ArgUsage
    ArgUsed)
          Defn
    _ -> TTerm -> Args -> TTerm
    C.mkTApp (QName -> TTerm
    C.TDef QName
    q) (Args -> TTerm) -> ReaderT CCEnv TCM Args -> CC TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Arg Term] -> ReaderT CCEnv TCM Args
    substArgs [Arg Term]
    vs
      where
        doinline :: EvaluationStrategy -> CC TTerm
    doinline EvaluationStrategy
    eval = TTerm -> Args -> TTerm
    C.mkTApp (TTerm -> Args -> TTerm)
    -> CC TTerm -> ReaderT CCEnv TCM (Args -> TTerm)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> EvaluationStrategy -> QName -> CC TTerm
    forall {t :: (* -> *) -> * -> *}.
    MonadTrans t =>
    EvaluationStrategy -> QName -> t TCM TTerm
    inline EvaluationStrategy
    eval QName
    q ReaderT CCEnv TCM (Args -> TTerm)
    -> ReaderT CCEnv TCM Args -> CC TTerm
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Arg Term] -> ReaderT CCEnv TCM Args
    substArgs [Arg Term]
    vs
        inline :: EvaluationStrategy -> QName -> t TCM TTerm
    inline EvaluationStrategy
    eval QName
    q = TCMT IO TTerm -> t TCM TTerm
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO TTerm -> t TCM TTerm) -> TCMT IO TTerm -> t TCM TTerm
    forall a b. (a -> b) -> a -> b
    $ EvaluationStrategy -> QName -> TCMT IO TTerm
    toTreeless' EvaluationStrategy
    eval QName
    q

    substArgs :: [Arg I.Term] -> CC [C.TTerm]
    substArgs :: [Arg Term] -> ReaderT CCEnv TCM Args
    substArgs = (Arg Term -> CC TTerm) -> [Arg Term] -> ReaderT CCEnv TCM Args
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse Arg Term -> CC TTerm
    substArg

    substArg :: Arg I.Term -> CC C.TTerm
    substArg :: Arg Term -> CC TTerm
    substArg Arg Term
    x | Arg Term -> Bool
    forall a. LensModality a => a -> Bool
    usableModality Arg Term
    x = Term -> CC TTerm
    substTerm (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    x)
               | Bool
    otherwise = TTerm -> CC TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    C.TErased