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

import Prelude hiding ((!!))

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

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

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

import Agda.TypeChecking.CompiledClause as CC
import qualified Agda.TypeChecking.CompiledClause.Compile as CC
import Agda.TypeChecking.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.Utils.Pretty (prettyShow)
import qualified Agda.Utils.Pretty as P
import qualified Agda.Utils.SmallSet as SmallSet

import Agda.Utils.Impossible

prettyPure :: P.Pretty a => a -> TCM Doc
prettyPure :: forall a. Pretty a => a -> TCMT IO Doc
prettyPure = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 <- 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 = 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
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"treeless.convert" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"-- before clause compiler" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ (forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Clause]
cs)
  let mst :: Maybe SplitTree
mst = Defn -> Maybe SplitTree
funSplitTree forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
def
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"treeless.convert" Int
70 forall a b. (a -> b) -> a -> b
$
    forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe SplitTree
mst TCMT IO Doc
"-- not using split tree" forall a b. (a -> b) -> a -> b
$ \SplitTree
st ->
      TCMT IO Doc
"-- using split tree" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty SplitTree
st
  RunRecordPatternTranslation
-> [Clause] -> Maybe SplitTree -> TCM CompiledClauses
CC.compileClauses' RunRecordPatternTranslation
translate [Clause]
cs Maybe SplitTree
mst

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

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

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

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

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

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

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 :: Int -> QName -> Pipeline
compilerPipeline :: Int -> QName -> Pipeline
compilerPipeline Int
v QName
q =
  [Pipeline] -> Pipeline
Sequential
    -- Issue #4967: No simplification step before builtin translation! Simplification relies
    --              on either all or no builtins being translated. Since we might have inlined
    --              functions that have had the builtin translation applied, we need to apply it
    --              first.
    -- [ compilerPass "simpl"   (35 + v) "simplification"      $ const simplifyTTerm
    [ [Char]
-> Int
-> [Char]
-> (EvaluationStrategy -> TTerm -> TCM TTerm)
-> Pipeline
compilerPass [Char]
"builtin" (Int
30 forall a. Num a => a -> a -> a
+ Int
v) [Char]
"builtin translation" forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const TTerm -> TCM TTerm
translateBuiltins
    , Int -> Pipeline -> Pipeline
FixedPoint Int
5 forall a b. (a -> b) -> a -> b
$ [Pipeline] -> Pipeline
Sequential
      [ [Char]
-> Int
-> [Char]
-> (EvaluationStrategy -> TTerm -> TCM TTerm)
-> Pipeline
compilerPass [Char]
"simpl"  (Int
30 forall a. Num a => a -> a -> a
+ Int
v) [Char]
"simplification"     forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const TTerm -> TCM TTerm
simplifyTTerm
      , [Char]
-> Int
-> [Char]
-> (EvaluationStrategy -> TTerm -> TCM TTerm)
-> Pipeline
compilerPass [Char]
"erase"  (Int
30 forall a. Num a => a -> a -> a
+ Int
v) [Char]
"erasure"            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 forall a. Num a => a -> a -> a
+ Int
v) [Char]
"uncase"             forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall (m :: * -> *). Monad m => TTerm -> m TTerm
caseToSeq
      , [Char]
-> Int
-> [Char]
-> (EvaluationStrategy -> TTerm -> TCM TTerm)
-> Pipeline
compilerPass [Char]
"aspat"  (Int
30 forall a. Num a => a -> a -> a
+ Int
v) [Char]
"@-pattern recovery" forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall (m :: * -> *). Monad m => TTerm -> m TTerm
recoverAsPatterns
      ]
    , [Char]
-> Int
-> [Char]
-> (EvaluationStrategy -> TTerm -> TCM TTerm)
-> Pipeline
compilerPass [Char]
"id" (Int
30 forall a. Num a => a -> a -> a
+ Int
v) [Char]
"identity function detection" forall a b. (a -> b) -> a -> b
$ 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  -> forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (forall a b c. (a -> b -> c) -> b -> a -> c
flip 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   = forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc ([Char]
"treeless.opt." forall a. [a] -> [a] -> [a]
++ CompilerPass -> [Char]
passTag CompilerPass
p) (CompilerPass -> Int
passVerbosity CompilerPass
p) forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
f forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"-- " forall a. [a] -> [a] -> [a]
++ CompilerPass -> [Char]
passName CompilerPass
p)
      pbody :: TTerm -> TCMT IO Doc
pbody TTerm
b = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Pretty a => a -> [Char]
prettyShow QName
q) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=", forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> TCMT IO Doc
prettyPure TTerm
b ]
  (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO ()
dbg forall a b. (a -> b) -> a -> b
$ if | TTerm
t forall a. Eq a => a -> a -> Bool
== TTerm
t'   -> (forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"(No effect)")
           | Bool
otherwise -> (forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ TTerm -> TCMT IO Doc
pbody TTerm
t')
  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 forall a. Ord a => a -> a -> Bool
> Int
n = do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"treeless.opt.loop" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
"++ Optimisation loop reached maximum iterations (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
n forall a. [a] -> [a] -> [a]
++ [Char]
")"
      forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
    go Int
i TTerm
t = do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"treeless.opt.loop" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"++ Optimisation loop iteration " forall a. [a] -> [a] -> [a]
++ 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 forall a. Eq a => a -> a -> Bool
== TTerm
t'   -> do
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"treeless.opt.loop" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"++ Optimisation loop terminating after " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
i forall a. [a] -> [a] -> [a]
++ [Char]
" iterations"
            forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t'
         | Bool
otherwise -> Int -> TTerm -> TCM TTerm
go (Int
i forall a. Num a => a -> a -> a
+ Int
1) TTerm
t'

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

alwaysInline :: QName -> TCM Bool
alwaysInline :: QName -> TCM Bool
alwaysInline QName
q = do
  Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  forall (f :: * -> *) a. Applicative f => a -> f a
pure 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} -> (forall a. Maybe a -> Bool
isJust (Defn -> Maybe ExtLamInfo
funExtLam Defn
def) Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
recursive) Bool -> Bool -> Bool
|| forall a. Maybe a -> Bool
isJust (Defn -> Maybe QName
funWith Defn
def)
            where
              recursive :: Bool
recursive = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. a -> Maybe a -> a
fromMaybe Bool
True forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Bool
clauseRecursive) [Clause]
cs
    Defn
_ -> Bool
False

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

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

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

shift :: Int -> CCContext -> CCContext
shift :: Int -> [Int] -> [Int]
shift Int
n = forall a b. (a -> b) -> [a] -> [b]
map (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 = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ [Int]
xs 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 = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ [Int]
xs forall a. [a] -> Int -> Maybe a
!!! (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
xs forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- Int
l)

-- | Compile a case tree into nested case and record expressions.
casetreeTop :: EvaluationStrategy -> CC.CompiledClauses -> TCM C.TTerm
casetreeTop :: EvaluationStrategy -> CompiledClauses -> TCM TTerm
casetreeTop EvaluationStrategy
eval CompiledClauses
cc = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (EvaluationStrategy -> CCEnv
initCCEnv EvaluationStrategy
eval) forall a b. (a -> b) -> a -> b
$ do
  let a :: Int
a = CompiledClauses -> Int
commonArity CompiledClauses
cc
  forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"treeless.convert.arity" Int
40 forall a b. (a -> b) -> a -> b
$ [Char]
"-- common arity: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
a
  Int -> CC TTerm -> CC TTerm
lambdasUpTo Int
a 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 (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg [Char]]
xs) forall a b. (a -> b) -> a -> b
$ 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 (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg [Char]]
xs) 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 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall (m :: * -> *) a.
MonadTCEnv m =>
AllowedReductions -> m a -> m a
putAllowedReductions (forall a. SmallSetElement a => [a] -> SmallSet a
SmallSet.fromList [AllowedReduction
ProjectionReductions, AllowedReduction
CopatternReductions]) forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Term
v)
      [Int]
cxt <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CCEnv -> [Int]
ccCxt
      TTerm
v' <- Term -> CC TTerm
substTerm Term
v
      forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Int -> a -> m ()
reportS [Char]
"treeless.convert.casetree" Int
40 forall a b. (a -> b) -> a -> b
$
        [ TCMT IO Doc
"-- casetree, calling substTerm:"
        , TCMT IO Doc
"--   cxt =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a. Pretty a => a -> TCMT IO Doc
prettyPure [Int]
cxt
        , TCMT IO Doc
"--   v   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a. Pretty a => a -> TCMT IO Doc
prettyPure Term
v
        , TCMT IO Doc
"--   v'  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a. Pretty a => a -> TCMT IO Doc
prettyPure TTerm
v'
        ]
      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
_) -> 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 forall a b. (a -> b) -> a -> b
$ do
      Map QName TTerm -> CC TTerm
mkRecord forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse CompiledClauses -> CC TTerm
casetree (forall c. WithArity c -> c
CC.content 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 forall a. Num a => a -> a -> a
+ Int
1) forall a b. (a -> b) -> a -> b
$ do
      -- re #3733 TODO: revise when compiling --cubical
      Map QName (WithArity CompiledClauses)
conBrs <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isConstructor forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) (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' = forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (ConHead, WithArity CompiledClauses)
etaBr Map QName (WithArity CompiledClauses)
conBrs forall a b. (a -> b) -> a -> b
$ \ (ConHead
c, WithArity CompiledClauses
br) -> 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 forall k a. Map k a -> Bool
Map.null Map QName (WithArity CompiledClauses)
conBrs' Bool -> Bool -> 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 (forall k a. Map k a -> [k]
Map.keys Map QName (WithArity CompiledClauses)
conBrs', forall k a. Map k a -> [k]
Map.keys Map Literal CompiledClauses
litBrs) of
            ([QName]
cs, []) -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ [QName] -> TCMT IO CaseType
go [QName]
cs
              where
              go :: [QName] -> TCMT IO CaseType
go (QName
c:[QName]
cs) = forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> Definition -> Defn
theDef forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                Constructor{QName
conData :: Defn -> QName
conData :: QName
conData} ->
                  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Quantity -> QName -> CaseType
C.CTData (forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
i) QName
conData
                Defn
_ -> [QName] -> TCMT IO CaseType
go [QName]
cs
              go [] = forall a. HasCallStack => a
__IMPOSSIBLE__
            ([], LitChar   Char
_ : [Literal]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return CaseType
C.CTChar
            ([], LitString Text
_ : [Literal]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return CaseType
C.CTString
            ([], LitFloat  Double
_ : [Literal]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return CaseType
C.CTFloat
            ([], LitQName  QName
_ : [Literal]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return CaseType
C.CTQName
            ([QName], [Literal])
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

        Maybe CompiledClauses -> CC TTerm -> CC TTerm
updateCatchAll Maybe CompiledClauses
catchAll forall a b. (a -> b) -> a -> b
$ do
          Int
x <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Int -> [Int] -> Int
lookupLevel Int
n 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 }
          Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
C.TCase Int
x CaseInfo
caseInfo TTerm
def 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
            forall (m :: * -> *) a. Monad m => a -> m a
return ([TAlt]
br1 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 = forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (forall b a. b -> (a -> b) -> Maybe a -> b
maybe TTerm
C.tUnreachable Int -> TTerm
C.TVar 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 forall {a}. Int -> CompiledClauses' a -> [Int]
arities Int
0 CompiledClauses
cc of
    [] -> Int
0
    [Int]
as -> 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
_)) =
      forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Int -> WithArity (CompiledClauses' a) -> [Int]
wArities Int
cxt') (forall k a. Map k a -> [a]
Map.elems Map QName (WithArity (CompiledClauses' a))
cons) forall a. [a] -> [a] -> [a]
++
      forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Int -> WithArity (CompiledClauses' a) -> [Int]
wArities Int
cxt') forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (forall a. Maybe a -> [a]
maybeToList Maybe (ConHead, WithArity (CompiledClauses' a))
eta) forall a. [a] -> [a] -> [a]
++
      forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Int -> WithArity (CompiledClauses' a) -> [Int]
wArities Int
cxt' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. Int -> c -> WithArity c
WithArity Int
0) (forall k a. Map k a -> [a]
Map.elems Map Literal (CompiledClauses' a)
lits) forall a. [a] -> [a] -> [a]
++
      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' = forall a. Ord a => a -> a -> a
max (Int
x 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
_) = [forall a. Ord a => a -> a -> a
max Int
cxt (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg [Char]]
xs)]
    arities Int
cxt (Fail [Arg [Char]]
xs)   = [forall a. Ord a => a -> a -> a
max Int
cxt (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) = forall a b. (a -> b) -> [a] -> [b]
map (\ Int
x -> Int
x forall a. Num a => a -> a -> a
- Int
k forall a. Num a => a -> a -> a
+ Int
1) forall a b. (a -> b) -> a -> b
$ Int -> CompiledClauses' a -> [Int]
arities (Int
cxt forall a. Num a => a -> a -> a
- Int
1 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 <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CCEnv -> [Int]
ccCxt
  forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Int -> a -> m ()
reportS [Char]
"treeless.convert.lambdas" Int
40 forall a b. (a -> b) -> a -> b
$
    [ TCMT IO Doc
"-- updateCatchAll:"
    , TCMT IO Doc
"--   cxt =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a. Pretty a => a -> TCMT IO Doc
prettyPure [Int]
cxt
    , TCMT IO Doc
"--   def =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a. Pretty a => a -> TCMT IO Doc
prettyPure TTerm
def
    ]
  forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ CCEnv
e -> CCEnv
e { ccCatchAll :: Maybe Int
ccCatchAll = forall a. a -> Maybe a
Just Int
0, ccCxt :: [Int]
ccCxt = Int -> [Int] -> [Int]
shift Int
1 [Int]
cxt }) forall a b. (a -> b) -> a -> b
$ do
    TTerm -> TTerm -> TTerm
C.mkLet TTerm
def 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 <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (((Int
n forall a. Num a => a -> a -> a
-) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Int
length) forall b c a. (b -> c) -> (a -> b) -> a -> c
. CCEnv -> [Int]
ccCxt)
  if Int
diff 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`.
       --
       forall a. Int -> [a] -> [a]
drop Int
diff' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CCEnv -> [Int]
ccCxt
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ CCEnv
e -> CCEnv
e { ccCxt :: [Int]
ccCxt = [Int]
cxt }) forall a b. (a -> b) -> a -> b
$ do
      forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Int -> a -> m ()
reportS [Char]
"treeless.convert.lambdas" Int
40 forall a b. (a -> b) -> a -> b
$
        [ TCMT IO Doc
"-- withContextSize:"
        , TCMT IO Doc
"--   n   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a. Pretty a => a -> TCMT IO Doc
prettyPure Int
n
        , TCMT IO Doc
"--   diff=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a. Pretty a => a -> TCMT IO Doc
prettyPure Int
diff
        , TCMT IO Doc
"--   cxt =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a. Pretty a => a -> TCMT IO Doc
prettyPure [Int]
cxt
        ]
      CC TTerm
cont forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> (TTerm -> Args -> TTerm
`C.mkTApp` forall a b. (a -> b) -> [a] -> [b]
map Int -> TTerm
C.TVar (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
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
diff forall a. Ord a => a -> a -> Bool
>= Int
1) forall a. HasCallStack => a
__IMPOSSIBLE__
  [Int]
cxt <- ([Int
0 .. Int
diffforall a. Num a => a -> a -> a
-Int
1] forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Int] -> [Int]
shift Int
diff forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CCEnv -> [Int]
ccCxt
  forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ CCEnv
e -> CCEnv
e { ccCxt :: [Int]
ccCxt = [Int]
cxt }) forall a b. (a -> b) -> a -> b
$ do
    forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Int -> a -> m ()
reportS [Char]
"treeless.convert.lambdas" Int
40 forall a b. (a -> b) -> a -> b
$
      [ TCMT IO Doc
"-- createLambdas:"
      , TCMT IO Doc
"--   diff =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a. Pretty a => a -> TCMT IO Doc
prettyPure Int
diff
      , TCMT IO Doc
"--   cxt  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a. Pretty a => a -> TCMT IO Doc
prettyPure [Int]
cxt
      ]
    -- Prepend diff lambdas
    CC TTerm
cont forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ TTerm
t -> forall a. (a -> a) -> a -> [a]
List.iterate TTerm -> TTerm
C.TLam TTerm
t 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 <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (((Int
n forall a. Num a => a -> a -> a
-) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Int
length) forall b c a. (b -> c) -> (a -> b) -> a -> c
. CCEnv -> [Int]
ccCxt)

  if Int
diff 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 forall a b. (a -> b) -> a -> b
$ do
      forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CCEnv -> Maybe Int
ccCatchAll forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just Int
catchAll -> do
          [Int]
cxt <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CCEnv -> [Int]
ccCxt
          forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Int -> a -> m ()
reportS [Char]
"treeless.convert.lambdas" Int
40 forall a b. (a -> b) -> a -> b
$
            [ TCMT IO Doc
"lambdasUpTo: n =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) Int
n
            , TCMT IO Doc
"  diff         =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) Int
n
            , TCMT IO Doc
"  catchAll     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a. Pretty a => a -> TCMT IO Doc
prettyPure Int
catchAll
            , TCMT IO Doc
"  ccCxt        =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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
          forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\CCEnv
e -> CCEnv
e { ccCatchAll :: Maybe Int
ccCatchAll = forall a. a -> Maybe a
Just Int
0
                         , ccCxt :: [Int]
ccCxt = Int -> [Int] -> [Int]
shift Int
1 [Int]
cxt }) forall a b. (a -> b) -> a -> b
$ do
            let catchAllArgs :: Args
catchAllArgs = forall a b. (a -> b) -> [a] -> [b]
map Int -> TTerm
C.TVar forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> [a]
downFrom Int
diff
            TTerm -> TTerm -> TTerm
C.mkLet (TTerm -> Args -> TTerm
C.mkTApp (Int -> TTerm
C.TVar forall a b. (a -> b) -> a -> b
$ Int
catchAll forall a. Num a => a -> a -> a
+ Int
diff) Args
catchAllArgs)
              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 = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall k a. Map k a -> [(k, a)]
Map.toList Map QName (WithArity CompiledClauses)
br) forall a b. (a -> b) -> a -> b
$ \ (QName
c, CC.WithArity Int
n CompiledClauses
cc) -> do
  QName
c' <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
c
  forall a. Int -> Int -> CC a -> CC a
replaceVar Int
x Int
n 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 = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall k a. Map k a -> [(k, a)]
Map.toList Map Literal CompiledClauses
br) forall a b. (a -> b) -> a -> b
$ \ (Literal
l, CompiledClauses
cc) ->
  -- Issue1624: we need to drop the case scrutinee from the environment here!
  forall a. Int -> Int -> CC a -> CC a
replaceVar Int
x Int
0 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 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 forall a. [a] -> [a] -> [a]
++ [Int]
ixs forall a. [a] -> [a] -> [a]
++ Int -> [Int] -> [Int]
shift Int
n [Int]
zs
       where
         -- compute the de Bruijn index
         i :: Int
i = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
cxt forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- Int
x
         -- discard index i
         ([Int]
ys, Int
_:[Int]
zs) = 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 forall a. Num a => a -> a -> a
- Int
1)]
  forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\CCEnv
e -> CCEnv
e { ccCxt :: [Int]
ccCxt = [Int] -> [Int]
upd (CCEnv -> [Int]
ccCxt CCEnv
e) , ccCatchAll :: Maybe Int
ccCatchAll = (forall a. Num a => a -> a -> a
+Int
n) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CCEnv -> Maybe Int
ccCatchAll CCEnv
e }) 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 = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ do
  -- Get the name of the first field
  let p1 :: QName
p1 = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> a
headWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> QName
I.conName forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO ConHead
recConFromProj QName
p1)
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"treeless.convert.mkRecord" Int
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"record constructor fields: xs      = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) [Arg QName]
xs
    , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"to be filled with content: keys fs = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) (forall k a. Map k a -> [k]
Map.keys Map QName TTerm
fs)
    ]
  -- Convert the constructor
  let (Args
args :: [C.TTerm]) = forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Arg QName]
xs forall a b. (a -> b) -> a -> b
$ \ Arg QName
x -> forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ (forall e. Arg e -> e
unArg Arg QName
x) Map QName TTerm
fs
  forall (m :: * -> *) a. Monad m => a -> m a
return 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
  forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isProjection QName
q) forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ \ Projection
proj -> do
    -- Get the record type name @d@ from the projection.
    let d :: QName
d = forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ Projection -> Arg QName
projFromType Projection
proj
    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 -> CC Term
normaliseStatic Term
term forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ Term
term ->
  case Term -> Term
I.unSpine forall a b. (a -> b) -> a -> b
$ Term -> Term
etaContractErased Term
term of
    I.Var Int
ind Elims
es -> do
      Int
ind' <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Int -> [Int] -> Int
lookupIndex Int
ind forall b c a. (b -> c) -> (a -> b) -> a -> c
. CCEnv -> [Int]
ccCxt)
      let args :: [Arg Term]
args = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
I.allApplyElims Elims
es
      TTerm -> Args -> TTerm
C.mkTApp (Int -> TTerm
C.TVar Int
ind') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Term] -> CC Args
substArgs [Arg Term]
args
    I.Lam ArgInfo
_ Abs Term
ab ->
      TTerm -> TTerm
C.TLam forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\CCEnv
e -> CCEnv
e { ccCxt :: [Int]
ccCxt = Int
0 forall a. a -> [a] -> [a]
: Int -> [Int] -> [Int]
shift Int
1 (CCEnv -> [Int]
ccCxt CCEnv
e) })
          (Term -> CC TTerm
substTerm forall a b. (a -> b) -> a -> b
$ forall a. Abs a -> a
I.unAbs Abs Term
ab)
    I.Lit Literal
l -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Literal -> TTerm
C.TLit Literal
l
    I.Level Level
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
C.TUnit
    I.Def QName
q Elims
es -> do
      let args :: [Arg Term]
args = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ 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 = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
I.allApplyElims Elims
es
        QName
c' <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName forall a b. (a -> b) -> a -> b
$ ConHead -> QName
I.conName ConHead
c
        TTerm -> Args -> TTerm
C.mkTApp (QName -> TTerm
C.TCon QName
c') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Term] -> CC Args
substArgs [Arg Term]
args
    I.Pi Dom Type
_ Abs Type
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
C.TUnit
    I.Sort Sort
_  -> forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
C.TSort
    I.MetaV MetaId
x Elims
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ TError -> TTerm
C.TError forall a b. (a -> b) -> a -> b
$ [Char] -> TError
C.TMeta forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> [Char]
prettyShow MetaId
x
    I.DontCare Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
C.TErased
    I.Dummy{} -> 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 = 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 (forall a. LensModality a => a -> Bool
usableModality Arg Term
arg) -> 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 (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 (forall a. LensModality a => a -> Bool
usableModality Arg Term
arg) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
0 (Term -> Term
DontCare HasCallStack => Term
__DUMMY_TERM__) Term
u
          BinAppView
_ -> Either Term Term
done

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

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

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

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