{-# OPTIONS_GHC -Wunused-imports #-}

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

import Prelude hiding ((!!))

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.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
  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 -> 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 :: 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

-- ** 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
    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.
    BuildPipeline -> CCConfig -> QName -> CompiledClauses -> TCM TTerm
ccToTreelessWith BuildPipeline
pl CCConfig
cfg QName
q CompiledClauses
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 ]
  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 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)
  [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
forall (m :: * -> *). MonadPretty m => QName -> 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 <- CCConfig -> CompiledClauses -> TCM TTerm
casetreeTop CCConfig
cfg 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 -> TCM TTerm
runPipeline EvaluationStrategy
eval QName
q (BuildPipeline
pl 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 (CCSubst
su CCSubst -> CCSubst -> Bool
forall a. Eq a => a -> a -> Bool
== CCSubst
EraseUnused Bool -> Bool -> Bool
&& ArgUsage
ArgUnused ArgUsage -> [ArgUsage] -> Bool
forall a. Eq a => a -> [a] -> 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 -> TCM TTerm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
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
  TTerm
t' <- CompilerPass -> EvaluationStrategy -> TTerm -> TCM 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 -> TCM TTerm
forall a. a -> TCMT IO a
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 -> 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
      TTerm
t' <- EvaluationStrategy -> QName -> Pipeline -> TTerm -> TCM 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 -> TCM TTerm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t'
         | Bool
otherwise -> Int -> TTerm -> TCM TTerm
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) TTerm
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
  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 a. a -> TCMT IO a
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

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.
      Term
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)
      [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 ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [TCMT IO Doc] -> 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 a. a -> ReaderT CCEnv TCM a
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)
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
      Map QName (WithArity CompiledClauses)
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' :: 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 (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__

        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 = 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)
                }
          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 a. a -> ReaderT CCEnv TCM a
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 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
  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 ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [TCMT IO Doc] -> 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 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 { ccCatchAll = Just 0, ccCxt = shift 1 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 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 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 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 = 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 ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [TCMT IO Doc] -> 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 (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f 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 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 = 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 ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [TCMT IO Doc] -> 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 (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f 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. 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
  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 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 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 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
>>= \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 ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [TCMT IO Doc] -> 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 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 { ccCatchAll = Just 0
                         , ccCxt = shift 1 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 (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
  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 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 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 (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f 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 -> TCM TTerm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm -> TCM TTerm) -> TTerm -> TCM 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 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
      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 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
        QName
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
        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 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
  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 a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
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
  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{} -> () () -> 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
  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 (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 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 (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
$ EvaluationStrategy -> QName -> TCMT IO ()
cacheTreeless EvaluationStrategy
eval QName
q
    Definition
def <- TCMT IO Definition -> ReaderT CCEnv TCM Definition
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 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' 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.
        [ArgUsage]
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
        CCSubst
su <- (CCEnv -> CCSubst) -> ReaderT CCEnv TCM CCSubst
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CCEnv -> CCSubst
ccSubstUnused
        let substUsed :: Arg Term -> ArgUsage -> CC TTerm
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
        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 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