    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.Compiler.ToTreeless
      ( toTreeless
      , toTreelessWith
      , closedTermToTreeless
      , Pipeline(..)
      , CompilerPass(..)
      , compilerPass
      , compilerPipeline
      , CCConfig
      , CCSubst(..)
      ) where

    import Prelude hiding ((!!))

    import Control.Monad.Reader ( MonadReader(..), asks, ReaderT, runReaderT )

    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.Datatypes
    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.Syntax.Common.Pretty (prettyShow)
    import qualified Agda.Syntax.Common.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 a. a -> TCMT IO a
    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
      def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
      let cs = Definition -> [Clause]
    defClauses Definition
    def
          isProj | Function{ funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Right Projection
    x } <- Definition -> Defn
    theDef Definition
    def = Maybe QName -> Bool
    forall a. Maybe a -> Bool
    isJust (Projection -> Maybe QName
    projProper Projection
    x)
                 | Bool
    otherwise = Bool
    False
          translate | Bool
    isProj    = RunRecordPatternTranslation
    CC.DontRunRecordPatternTranslation
                    | Bool
    otherwise = RunRecordPatternTranslation
    CC.RunRecordPatternTranslation
      reportSDoc "treeless.convert" 40 $ "-- before clause compiler" $$ (pretty q <+> "=") <?> vcat (map pretty cs)
      let mst = Defn -> Maybe SplitTree
    funSplitTree (Defn -> Maybe SplitTree) -> Defn -> Maybe SplitTree
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef Definition
    def
      reportSDoc "treeless.convert" 70 $
        caseMaybe mst "-- not using split tree" $ \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
      CC.compileClauses' q translate cs mst

    -- ** Types of pipelines; different backends might use their own custom pipeline.
    type BuildPipeline = Int -> QName -> Pipeline

    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 -> TCM TTerm
    passCode      :: EvaluationStrategy -> TTerm -> TCM TTerm
      }

    type CC        = ReaderT CCEnv TCM
    type CCContext = [Int]
    data CCSubst   = EraseUnused | IgnoreUnused deriving CCSubst -> CCSubst -> Bool
    (CCSubst -> CCSubst -> Bool)
    -> (CCSubst -> CCSubst -> Bool) -> Eq CCSubst
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: CCSubst -> CCSubst -> Bool
    == :: CCSubst -> CCSubst -> Bool
    $c/= :: CCSubst -> CCSubst -> Bool
    /= :: CCSubst -> CCSubst -> Bool
    Eq

    -- | Environment for treeless conversion.
    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
        -- ^ Which evaluation strategy does the backend assumes.
      , CCEnv -> CCSubst
    ccSubstUnused :: CCSubst
        -- ^ Whether to erase unused arguments.
      }

    type CCConfig  = (EvaluationStrategy, CCSubst)

    -- | Initial environment for expression generation.
    initCCEnv :: CCConfig -> CCEnv
    initCCEnv :: CCConfig -> CCEnv
    initCCEnv (EvaluationStrategy
    eval, CCSubst
    su) = CCEnv
      { ccCxt :: [Int]
    ccCxt         = []
      , ccCatchall :: Maybe Int
    ccCatchall    = Maybe Int
    forall a. Maybe a
    Nothing
      , ccEvaluation :: EvaluationStrategy
    ccEvaluation  = EvaluationStrategy
    eval
      , ccSubstUnused :: CCSubst
    ccSubstUnused = CCSubst
    su
      }

    -- | 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.
    toTreelessWith :: BuildPipeline -> CCConfig -> QName -> TCM (Maybe C.TTerm)
    toTreelessWith :: BuildPipeline -> CCConfig -> QName -> TCM (Maybe TTerm)
    toTreelessWith BuildPipeline
    pl CCConfig
    cfg 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 a. a -> TCMT IO a
    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) -> TCM TTerm -> TCM (Maybe TTerm)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BuildPipeline -> CCConfig -> QName -> TCM TTerm
    toTreelessWith' BuildPipeline
    pl CCConfig
    cfg QName
    q

    toTreeless :: EvaluationStrategy -> QName -> TCM (Maybe C.TTerm)
    toTreeless :: EvaluationStrategy -> QName -> TCM (Maybe TTerm)
    toTreeless EvaluationStrategy
    eval = BuildPipeline -> CCConfig -> QName -> TCM (Maybe TTerm)
    toTreelessWith BuildPipeline
    compilerPipeline (EvaluationStrategy
    eval, CCSubst
    EraseUnused)

    toTreelessWith' :: BuildPipeline -> CCConfig -> QName -> TCM C.TTerm
    toTreelessWith' :: BuildPipeline -> CCConfig -> QName -> TCM TTerm
    toTreelessWith' BuildPipeline
    pl CCConfig
    cfg QName
    q =
      (TCM TTerm -> TCM (Maybe TTerm) -> TCM TTerm)
    -> TCM (Maybe TTerm) -> TCM TTerm -> TCM TTerm
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip TCM TTerm -> TCM (Maybe TTerm) -> TCM 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) (TCM TTerm -> TCM TTerm) -> TCM TTerm -> TCM TTerm
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> [Char] -> TCM TTerm -> TCM TTerm
    forall a. [Char] -> Int -> [Char] -> TCMT IO a -> TCMT IO a
    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) (TCM TTerm -> TCM TTerm) -> TCM TTerm -> TCM TTerm
    forall a b. (a -> b) -> a -> b
    $ do
        cc <- QName -> TCM CompiledClauses
    getCompiledClauses QName
    q
        unlessM (alwaysInline q) $ setTreeless q (C.TDef q)
          -- so recursive inlining doesn't loop, but not for always inlined
          -- functions, since that would risk inlining to fail.
        ccToTreelessWith pl cfg q cc

    toTreeless' :: EvaluationStrategy -> QName -> TCM C.TTerm
    toTreeless' :: EvaluationStrategy -> QName -> TCM TTerm
    toTreeless' EvaluationStrategy
    eval = BuildPipeline -> CCConfig -> QName -> TCM TTerm
    toTreelessWith' BuildPipeline
    compilerPipeline (EvaluationStrategy
    eval, CCSubst
    EraseUnused)

    ccToTreelessWith :: BuildPipeline -> CCConfig -> QName -> CC.CompiledClauses -> TCM C.TTerm
    ccToTreelessWith :: BuildPipeline -> CCConfig -> QName -> CompiledClauses -> TCM TTerm
    ccToTreelessWith BuildPipeline
    pl cfg :: CCConfig
    cfg@(EvaluationStrategy
    eval, CCSubst
    su) 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 ]
      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 a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    20) (Int -> TCMT IO Int
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    0)
      reportSDoc "treeless.convert" (30 + v) $ "-- compiled clauses of" <+> prettyTCM q $$ nest 2 (prettyPure cc)
      body <- casetreeTop cfg cc
      reportSDoc "treeless.opt.converted" (30 + v) $ "-- converted" $$ pbody body
      body <- runPipeline eval q (pl v q) body
      used <- usedArguments q body
      when (su == EraseUnused && ArgUnused `elem` used) $
        reportSDoc "treeless.opt.unused" (30 + v) $
          "-- used args:" <+> hsep [ if u == ArgUsed then text [x] else "_" | (x, u) <- zip ['a'..] used ] $$
          pbody' "[stripped]" (stripUnusedArguments used body)
      reportSDoc "treeless.opt.final" (20 + v) $ pbody body
      setTreeless q body
      setCompiledArgUse q used
      return body

    ccToTreeless :: EvaluationStrategy -> QName -> CC.CompiledClauses -> TCM C.TTerm
    ccToTreeless :: EvaluationStrategy -> QName -> CompiledClauses -> TCM TTerm
    ccToTreeless EvaluationStrategy
    eval = BuildPipeline -> CCConfig -> QName -> CompiledClauses -> TCM TTerm
    ccToTreelessWith BuildPipeline
    compilerPipeline (EvaluationStrategy
    eval, CCSubst
    EraseUnused)

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

    compilerPipeline :: BuildPipeline
    compilerPipeline :: BuildPipeline
    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 -> TCM TTerm)
    -> Pipeline
    compilerPass [Char]
    "builtin" (Int
    30 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    v) [Char]
    "builtin translation" ((EvaluationStrategy -> TTerm -> TCM TTerm) -> Pipeline)
    -> (EvaluationStrategy -> TTerm -> TCM TTerm) -> Pipeline
    forall a b. (a -> b) -> a -> b
    $ (TTerm -> TCM TTerm) -> EvaluationStrategy -> TTerm -> TCM TTerm
    forall a b. a -> b -> a
    const TTerm -> TCM 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 -> TCM TTerm)
    -> Pipeline
    compilerPass [Char]
    "simpl"  (Int
    30 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    v) [Char]
    "simplification"     ((EvaluationStrategy -> TTerm -> TCM TTerm) -> Pipeline)
    -> (EvaluationStrategy -> TTerm -> TCM TTerm) -> Pipeline
    forall a b. (a -> b) -> a -> b
    $ (TTerm -> TCM TTerm) -> EvaluationStrategy -> TTerm -> TCM TTerm
    forall a b. a -> b -> a
    const TTerm -> TCM TTerm
    simplifyTTerm
          , [Char]
    -> Int
    -> [Char]
    -> (EvaluationStrategy -> TTerm -> TCM TTerm)
    -> Pipeline
    compilerPass [Char]
    "erase"  (Int
    30 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    v) [Char]
    "erasure"            ((EvaluationStrategy -> TTerm -> TCM TTerm) -> Pipeline)
    -> (EvaluationStrategy -> TTerm -> TCM TTerm) -> Pipeline
    forall a b. (a -> b) -> a -> b
    $ QName -> EvaluationStrategy -> TTerm -> TCM TTerm
    eraseTerms QName
    q
          , [Char]
    -> Int
    -> [Char]
    -> (EvaluationStrategy -> TTerm -> TCM TTerm)
    -> Pipeline
    compilerPass [Char]
    "uncase" (Int
    30 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    v) [Char]
    "uncase"             ((EvaluationStrategy -> TTerm -> TCM TTerm) -> Pipeline)
    -> (EvaluationStrategy -> TTerm -> TCM TTerm) -> Pipeline
    forall a b. (a -> b) -> a -> b
    $ (TTerm -> TCM TTerm) -> EvaluationStrategy -> TTerm -> TCM TTerm
    forall a b. a -> b -> a
    const TTerm -> TCM TTerm
    forall (m :: * -> *). Monad m => TTerm -> m TTerm
    caseToSeq
          , [Char]
    -> Int
    -> [Char]
    -> (EvaluationStrategy -> TTerm -> TCM TTerm)
    -> Pipeline
    compilerPass [Char]
    "aspat"  (Int
    30 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    v) [Char]
    "@-pattern recovery" ((EvaluationStrategy -> TTerm -> TCM TTerm) -> Pipeline)
    -> (EvaluationStrategy -> TTerm -> TCM TTerm) -> Pipeline
    forall a b. (a -> b) -> a -> b
    $ (TTerm -> TCM TTerm) -> EvaluationStrategy -> TTerm -> TCM TTerm
    forall a b. a -> b -> a
    const TTerm -> TCM TTerm
    forall (m :: * -> *). Monad m => TTerm -> m TTerm
    recoverAsPatterns
          ]
        , [Char]
    -> Int
    -> [Char]
    -> (EvaluationStrategy -> TTerm -> TCM 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 -> TCM TTerm) -> Pipeline)
    -> (EvaluationStrategy -> TTerm -> TCM TTerm) -> Pipeline
    forall a b. (a -> b) -> a -> b
    $ (TTerm -> TCM TTerm) -> EvaluationStrategy -> TTerm -> TCM TTerm
    forall a b. a -> b -> a
    const (QName -> TTerm -> TCM TTerm
    detectIdentityFunctions QName
    q)
        ]

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

    runCompilerPass :: EvaluationStrategy -> QName -> CompilerPass -> TTerm -> TCM TTerm
    runCompilerPass :: EvaluationStrategy -> QName -> CompilerPass -> TTerm -> TCM TTerm
    runCompilerPass EvaluationStrategy
    eval QName
    q CompilerPass
    p TTerm
    t = do
      t' <- CompilerPass -> EvaluationStrategy -> TTerm -> TCM TTerm
    passCode CompilerPass
    p EvaluationStrategy
    eval TTerm
    t
      let 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
    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 ]
      dbg $ if | t == t'   -> (<+> "(No effect)")
               | otherwise -> ($$ pbody t')
      return t'

    runFixedPoint :: Int -> EvaluationStrategy -> QName -> Pipeline -> TTerm -> TCM TTerm
    runFixedPoint :: Int
    -> EvaluationStrategy -> QName -> Pipeline -> TTerm -> TCM TTerm
    runFixedPoint Int
    n EvaluationStrategy
    eval QName
    q Pipeline
    pipeline = Int -> TTerm -> TCM TTerm
    go Int
    1
      where
        go :: Int -> TTerm -> TCM 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 -> TCM TTerm
    forall a. a -> TCMT IO a
    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
          t' <- EvaluationStrategy -> QName -> Pipeline -> TTerm -> TCM TTerm
    runPipeline EvaluationStrategy
    eval QName
    q Pipeline
    pipeline TTerm
    t
          if | t == t'   -> do
                reportSLn "treeless.opt.loop" 30 $ "++ Optimisation loop terminating after " ++ show i ++ " iterations"
                return t'
             | otherwise -> go (i + 1) t'

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

    alwaysInline :: QName -> TCM Bool
    alwaysInline :: QName -> TCMT IO Bool
    alwaysInline QName
    q = do
      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
      pure $ case 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

    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 a. [a] -> 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 :: CCConfig -> CC.CompiledClauses -> TCM C.TTerm
    casetreeTop :: CCConfig -> CompiledClauses -> TCM TTerm
    casetreeTop CCConfig
    cfg CompiledClauses
    cc = (CC TTerm -> CCEnv -> TCM TTerm) -> CCEnv -> CC TTerm -> TCM TTerm
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip CC TTerm -> CCEnv -> TCM TTerm
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT (CCConfig -> CCEnv
    initCCEnv CCConfig
    cfg) (CC TTerm -> TCM TTerm) -> CC TTerm -> TCM TTerm
    forall a b. (a -> b) -> a -> b
    $ do
      let a :: Int
    a = CompiledClauses -> Int
    commonArity CompiledClauses
    cc
      TCMT IO () -> ReaderT CCEnv TCM ()
    forall (m :: * -> *) a. Monad m => m a -> ReaderT CCEnv m a
    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 a. [a] -> 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 a. a -> ReaderT CCEnv TCM a
    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 a. [a] -> 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.
          v <- TCM Term -> ReaderT CCEnv TCM Term
    forall (m :: * -> *) a. Monad m => m a -> ReaderT CCEnv m a
    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)
          cxt <- asks ccCxt
          v' <- substTerm v
          reportS "treeless.convert.casetree" 40 $
            [ "-- casetree, calling substTerm:"
            , "--   cxt =" <+> prettyPure cxt
            , "--   v   =" <+> prettyPure v
            , "--   v'  =" <+> prettyPure v'
            ]
          return 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__
        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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Map QName a -> f (Map QName 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
          -- re #3733 TODO: revise when compiling --cubical
          conBrs <- ([(QName, WithArity CompiledClauses)]
     -> Map QName (WithArity CompiledClauses))
    -> ReaderT CCEnv TCM [(QName, WithArity CompiledClauses)]
    -> ReaderT CCEnv TCM (Map QName (WithArity CompiledClauses))
    forall a b. (a -> b) -> ReaderT CCEnv TCM a -> ReaderT CCEnv TCM b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [(QName, WithArity CompiledClauses)]
    -> Map QName (WithArity CompiledClauses)
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList (ReaderT CCEnv TCM [(QName, WithArity CompiledClauses)]
     -> ReaderT CCEnv TCM (Map QName (WithArity CompiledClauses)))
    -> ReaderT CCEnv TCM [(QName, WithArity CompiledClauses)]
    -> ReaderT CCEnv TCM (Map QName (WithArity CompiledClauses))
    forall a b. (a -> b) -> a -> b
    $ ((QName, WithArity CompiledClauses) -> ReaderT CCEnv TCM Bool)
    -> [(QName, WithArity CompiledClauses)]
    -> ReaderT CCEnv TCM [(QName, WithArity CompiledClauses)]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM (QName -> ReaderT CCEnv TCM Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isConstructor (QName -> ReaderT CCEnv TCM Bool)
    -> ((QName, WithArity CompiledClauses) -> QName)
    -> (QName, WithArity CompiledClauses)
    -> ReaderT CCEnv TCM Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (QName, WithArity CompiledClauses) -> QName
    forall a b. (a, b) -> a
    fst) (Map QName (WithArity CompiledClauses)
    -> [(QName, WithArity CompiledClauses)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map QName (WithArity CompiledClauses)
    conBrs)
                        -- We can treat eta-matches as regular matches here.
          let 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.null conBrs' && Map.null litBrs then do
            -- there are no branches, just return default
            updateCatchall catchall fromCatchall
          else do
            -- Get the type of the scrutinee.
            caseTy <-
              case (Map.keys conBrs', Map.keys litBrs) of
                ([QName]
    cs, []) -> TCM CaseType -> ReaderT CCEnv TCM CaseType
    forall (m :: * -> *) a. Monad m => m a -> ReaderT CCEnv m a
    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
    forall {m :: * -> *}. HasConstInfo m => [QName] -> m CaseType
    go [QName]
    cs
                  where
                  go :: [QName] -> m CaseType
    go (QName
    c:[QName]
    cs) = QName -> m QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    canonicalName QName
    c m QName -> (QName -> m Definition) -> m Definition
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo m Definition -> (Definition -> Defn) -> m Defn
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> Definition -> Defn
    theDef m Defn -> (Defn -> m CaseType) -> m CaseType
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                    Constructor{QName
    conData :: QName
    conData :: Defn -> QName
    conData} ->
                      CaseType -> m CaseType
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CaseType -> m CaseType) -> CaseType -> m CaseType
    forall a b. (a -> b) -> a -> b
    $ QName -> CaseType
    C.CTData QName
    conData
                    Defn
    _ -> [QName] -> m CaseType
    go [QName]
    cs
                  go [] = m CaseType
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                ([], LitChar   Char
    _ : [Literal]
    _) -> CaseType -> ReaderT CCEnv TCM CaseType
    forall a. a -> ReaderT CCEnv TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return CaseType
    C.CTChar
                ([], LitString Text
    _ : [Literal]
    _) -> CaseType -> ReaderT CCEnv TCM CaseType
    forall a. a -> ReaderT CCEnv TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return CaseType
    C.CTString
                ([], LitFloat  Double
    _ : [Literal]
    _) -> CaseType -> ReaderT CCEnv TCM CaseType
    forall a. a -> ReaderT CCEnv TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return CaseType
    C.CTFloat
                ([], LitQName  QName
    _ : [Literal]
    _) -> CaseType -> ReaderT CCEnv TCM CaseType
    forall a. a -> ReaderT CCEnv TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return CaseType
    C.CTQName
                ([QName], [Literal])
    _ -> ReaderT CCEnv TCM CaseType
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            updateCatchall catchall $ do
              x <- asks (lookupLevel n . ccCxt)
              def <- fromCatchall
              let caseInfo = C.CaseInfo
                    { caseType :: CaseType
    caseType   = CaseType
    caseTy
                    , caseLazy :: Bool
    caseLazy   = Bool
    lazy
                    , caseErased :: Erased
    caseErased = Erased -> Maybe Erased -> Erased
    forall a. a -> Maybe a -> a
    fromMaybe Erased
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Erased -> Erased) -> Maybe Erased -> Erased
    forall a b. (a -> b) -> a -> b
    $
                                   Quantity -> Maybe Erased
    erasedFromQuantity (ArgInfo -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity ArgInfo
    i)
                    }
              C.TCase x caseInfo def <$> do
                br1 <- conAlts n conBrs'
                br2 <- litAlts n litBrs
                return (br1 ++ 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 a. Ord a => [a] -> a
    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 a. [a] -> 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 a. [a] -> 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
      def <- CompiledClauses -> CC TTerm
    casetree CompiledClauses
    cc
      cxt <- asks ccCxt
      reportS "treeless.convert.lambdas" 40 $
        [ "-- updateCatchall:"
        , "--   cxt =" <+> prettyPure cxt
        , "--   def =" <+> prettyPure def
        ]
      local (\ CCEnv
    e -> CCEnv
    e { ccCatchall = Just 0, ccCxt = shift 1 cxt }) $ do
        C.mkLet def <$> 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
      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 a. [a] -> 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 diff >= 1 then createLambdas diff cont else do
        let diff' = -Int
    diff
        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`.
           --
           drop diff' <$> asks ccCxt
        local (\ CCEnv
    e -> CCEnv
    e { ccCxt = cxt }) $ do
          reportS "treeless.convert.lambdas" 40 $
            [ "-- withContextSize:"
            , "--   n   =" <+> prettyPure n
            , "--   diff=" <+> prettyPure diff
            , "--   cxt =" <+> prettyPure cxt
            ]
          cont <&> (`C.mkTApp` map C.TVar (downFrom 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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (Int
    diff Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    1) ReaderT CCEnv TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      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
      local (\ CCEnv
    e -> CCEnv
    e { ccCxt = cxt }) $ do
        reportS "treeless.convert.lambdas" 40 $
          [ "-- createLambdas:"
          , "--   diff =" <+> prettyPure diff
          , "--   cxt  =" <+> prettyPure cxt
          ]
        -- Prepend diff lambdas
        cont <&> \ 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. HasCallStack => [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
      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 a. [a] -> 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 diff <= 0 then cont -- no new lambdas needed
      else do
        createLambdas diff $ do
          asks ccCatchall >>= \case
            Just Int
    catchall -> do
              cxt <- (CCEnv -> [Int]) -> ReaderT CCEnv TCM [Int]
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks CCEnv -> [Int]
    ccCxt
              reportS "treeless.convert.lambdas" 40 $
                [ "lambdasUpTo: n =" <+> (text . show) n
                , "  diff         =" <+> (text . show) n
                , "  catchall     =" <+> prettyPure catchall
                , "  ccCxt        =" <+> prettyPure 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
              local (\CCEnv
    e -> CCEnv
    e { ccCatchall = Just 0
                             , ccCxt = shift 1 cxt }) $ do
                let 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
                C.mkLet (C.mkTApp (C.TVar $ catchall + diff) catchallArgs)
                  <$> 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
      c' <- TCM QName -> ReaderT CCEnv TCM QName
    forall (m :: * -> *) a. Monad m => m a -> ReaderT CCEnv m a
    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
      replaceVar x n $ do
        branch (C.TACon c' n) 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 a. [a] -> 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 a.
    (CCEnv -> CCEnv) -> ReaderT CCEnv TCM a -> ReaderT CCEnv TCM a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (\CCEnv
    e -> CCEnv
    e { ccCxt = upd (ccCxt e) , ccCatchall = (+ n) <$> ccCatchall 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 = TCM TTerm -> CC TTerm
    forall (m :: * -> *) a. Monad m => m a -> ReaderT CCEnv m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM TTerm -> CC TTerm) -> TCM 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 c IsRecord{} _ind 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)
      reportSDoc "treeless.convert.mkRecord" 60 $ vcat
        [ text "record constructor fields: xs      = " <+> (text . show) xs
        , text "to be filled with content: keys fs = " <+> (text . show) (Map.keys fs)
        ]
      -- Convert the constructor
      let (args :: [C.TTerm]) = for xs $ \ 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
      return $ C.mkTApp (C.TCon c) 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 a b.
    ReaderT CCEnv TCM a
    -> (a -> ReaderT CCEnv TCM b) -> ReaderT CCEnv TCM b
    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
          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] -> 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
          C.mkTApp (C.TVar ind') <$> substArgs 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 a.
    (CCEnv -> CCEnv) -> ReaderT CCEnv TCM a -> ReaderT CCEnv TCM a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (\CCEnv
    e -> CCEnv
    e { ccCxt = 0 : shift 1 (ccCxt 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 a. a -> ReaderT CCEnv TCM a
    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 a. a -> ReaderT CCEnv TCM a
    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
            c' <- TCM QName -> ReaderT CCEnv TCM QName
    forall (m :: * -> *) a. Monad m => m a -> ReaderT CCEnv m a
    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
            C.mkTApp (C.TCon c') <$> substArgs args
        I.Pi Dom Type
    _ Abs Type
    _ -> TTerm -> CC TTerm
    forall a. a -> ReaderT CCEnv TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    C.TUnit
        I.Sort Sort
    _  -> TTerm -> CC TTerm
    forall a. a -> ReaderT CCEnv TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    C.TSort
        I.MetaV MetaId
    x Elims
    _ -> TTerm -> CC TTerm
    forall a. a -> ReaderT CCEnv TCM a
    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 a. a -> ReaderT CCEnv TCM a
    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 (m :: * -> *) a. Monad m => m a -> ReaderT CCEnv m a
    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
      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 static then normalise v else pure v
    normaliseStatic Term
    v = Term -> ReaderT CCEnv TCM Term
    forall a. a -> ReaderT CCEnv TCM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    v

    -- | 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
      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 def of
        Function{} -> () () -> TCM TTerm -> TCMT IO ()
    forall a b. a -> TCMT IO b -> TCMT IO a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ EvaluationStrategy -> QName -> TCM TTerm
    toTreeless' EvaluationStrategy
    eval QName
    q
        Defn
    _          -> () -> TCMT IO ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    maybeInlineDef :: I.QName -> I.Args -> CC C.TTerm
    maybeInlineDef :: QName -> [Arg Term] -> CC TTerm
    maybeInlineDef QName
    q [Arg Term]
    vs = do
      eval <- (CCEnv -> EvaluationStrategy)
    -> ReaderT CCEnv TCM EvaluationStrategy
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks CCEnv -> EvaluationStrategy
    ccEvaluation
      ifM (lift $ alwaysInline q) (doinline eval) $ do
        lift $ cacheTreeless eval q
        def <- lift $ getConstInfo q
        case theDef def of
          fun :: Defn
    fun@Function{}
            | Defn
    fun Defn -> Lens' Defn Bool -> Bool
    forall o i. o -> Lens' o i -> i
    ^. (Bool -> f Bool) -> Defn -> f Defn
    Lens' Defn Bool
    funInline -> EvaluationStrategy -> CC TTerm
    doinline EvaluationStrategy
    eval
            | Bool
    otherwise -> do
            -- If ArgUsage hasn't been computed yet, we assume all arguments are used.
            used <- TCM [ArgUsage] -> ReaderT CCEnv TCM [ArgUsage]
    forall (m :: * -> *) a. Monad m => m a -> ReaderT CCEnv m a
    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
            su <- asks ccSubstUnused
            let substUsed Arg Term
    arg ArgUsage
    used
                  | ArgUsage
    used ArgUsage -> ArgUsage -> Bool
    forall a. Eq a => a -> a -> Bool
    == ArgUsage
    ArgUnused Bool -> Bool -> Bool
    && CCSubst
    su CCSubst -> CCSubst -> Bool
    forall a. Eq a => a -> a -> Bool
    == CCSubst
    EraseUnused
                  = TTerm -> CC TTerm
    forall a. a -> ReaderT CCEnv TCM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    C.TErased
                  | Bool
    otherwise
                  = Arg Term -> CC TTerm
    substArg Arg Term
    arg
            C.mkTApp (C.TDef q) <$> zipWithM substUsed vs (used ++ repeat 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 a b.
    ReaderT CCEnv TCM (a -> b)
    -> ReaderT CCEnv TCM a -> ReaderT CCEnv TCM b
    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 = TCM TTerm -> t TCM TTerm
    forall (m :: * -> *) a. Monad m => m a -> t m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM TTerm -> t TCM TTerm) -> TCM TTerm -> t TCM TTerm
    forall a b. (a -> b) -> a -> b
    $ EvaluationStrategy -> QName -> TCM 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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [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 a. a -> ReaderT CCEnv TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    C.TErased