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

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

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

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

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

-- | Environment for treeless conversion.
data CCEnv = CCEnv
  { CCEnv -> [Int]
ccCxt         :: CCContext
    -- ^ Maps case tree de-bruijn indices to TTerm de-bruijn indices.
  , CCEnv -> Maybe Int
ccCatchAll    :: Maybe Int
    -- ^ TTerm de-bruijn index of the current catch all.
    -- If an inner case has no catch-all clause, we use the one from its parent.
  , CCEnv -> EvaluationStrategy
ccEvaluation  :: EvaluationStrategy
    -- ^ Which evaluation strategy does the backend assumes.
  , CCEnv -> CCSubst
ccSubstUnused :: CCSubst
    -- ^ Whether to erase unused arguments.
  }

type CCConfig  = (EvaluationStrategy, CCSubst)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

casetree :: CC.CompiledClauses -> CC C.TTerm
casetree :: CompiledClauses -> CC TTerm
casetree CompiledClauses
cc = do
  case CompiledClauses
cc of
    CC.Fail [Arg [Char]]
xs -> Int -> CC TTerm -> CC TTerm
withContextSize ([Arg [Char]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg [Char]]
xs) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
forall a b. (a -> b) -> a -> b
$ TTerm -> CC TTerm
forall a. a -> ReaderT CCEnv TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
C.tUnreachable
    CC.Done [Arg [Char]]
xs Term
v -> Int -> CC TTerm -> CC TTerm
withContextSize ([Arg [Char]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg [Char]]
xs) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
forall a b. (a -> b) -> a -> b
$ do
      -- Issue 2469: Body context size (`length xs`) may be smaller than current context size
      -- if some arguments are not used in the body.
      v <- TCM Term -> ReaderT CCEnv TCM Term
forall (m :: * -> *) a. Monad m => m a -> ReaderT CCEnv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (AllowedReductions -> TCM Term -> TCM Term
forall (m :: * -> *) a.
MonadTCEnv m =>
AllowedReductions -> m a -> m a
putAllowedReductions ([AllowedReduction] -> AllowedReductions
forall a. SmallSetElement a => [a] -> SmallSet a
SmallSet.fromList [AllowedReduction
ProjectionReductions, AllowedReduction
CopatternReductions]) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Term -> TCM Term
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Term
v)
      cxt <- asks ccCxt
      v' <- substTerm v
      reportS "treeless.convert.casetree" 40 $
        [ "-- casetree, calling substTerm:"
        , "--   cxt =" <+> prettyPure cxt
        , "--   v   =" <+> prettyPure v
        , "--   v'  =" <+> prettyPure v'
        ]
      return v'
    CC.Case Arg Int
_ (CC.Branches Bool
True Map QName (WithArity CompiledClauses)
_ Maybe (ConHead, WithArity CompiledClauses)
_ Map Literal CompiledClauses
_ Just{} Maybe Bool
_ Bool
_) -> CC TTerm
forall a. HasCallStack => a
__IMPOSSIBLE__
      -- 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
      conBrs <- ([(QName, WithArity CompiledClauses)]
 -> Map QName (WithArity CompiledClauses))
-> ReaderT CCEnv TCM [(QName, WithArity CompiledClauses)]
-> ReaderT CCEnv TCM (Map QName (WithArity CompiledClauses))
forall a b. (a -> b) -> ReaderT CCEnv TCM a -> ReaderT CCEnv TCM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(QName, WithArity CompiledClauses)]
-> Map QName (WithArity CompiledClauses)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (ReaderT CCEnv TCM [(QName, WithArity CompiledClauses)]
 -> ReaderT CCEnv TCM (Map QName (WithArity CompiledClauses)))
-> ReaderT CCEnv TCM [(QName, WithArity CompiledClauses)]
-> ReaderT CCEnv TCM (Map QName (WithArity CompiledClauses))
forall a b. (a -> b) -> a -> b
$ ((QName, WithArity CompiledClauses) -> ReaderT CCEnv TCM Bool)
-> [(QName, WithArity CompiledClauses)]
-> ReaderT CCEnv TCM [(QName, WithArity CompiledClauses)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (QName -> ReaderT CCEnv TCM Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isConstructor (QName -> ReaderT CCEnv TCM Bool)
-> ((QName, WithArity CompiledClauses) -> QName)
-> (QName, WithArity CompiledClauses)
-> ReaderT CCEnv TCM Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName, WithArity CompiledClauses) -> QName
forall a b. (a, b) -> a
fst) (Map QName (WithArity CompiledClauses)
-> [(QName, WithArity CompiledClauses)]
forall k a. Map k a -> [(k, a)]
Map.toList Map QName (WithArity CompiledClauses)
conBrs)
                    -- We can treat eta-matches as regular matches here.
      let conBrs' = Maybe (ConHead, WithArity CompiledClauses)
-> Map QName (WithArity CompiledClauses)
-> ((ConHead, WithArity CompiledClauses)
    -> Map QName (WithArity CompiledClauses))
-> Map QName (WithArity CompiledClauses)
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (ConHead, WithArity CompiledClauses)
etaBr Map QName (WithArity CompiledClauses)
conBrs (((ConHead, WithArity CompiledClauses)
  -> Map QName (WithArity CompiledClauses))
 -> Map QName (WithArity CompiledClauses))
-> ((ConHead, WithArity CompiledClauses)
    -> Map QName (WithArity CompiledClauses))
-> Map QName (WithArity CompiledClauses)
forall a b. (a -> b) -> a -> b
$ \ (ConHead
c, WithArity CompiledClauses
br) -> (WithArity CompiledClauses
 -> WithArity CompiledClauses -> WithArity CompiledClauses)
-> QName
-> WithArity CompiledClauses
-> Map QName (WithArity CompiledClauses)
-> Map QName (WithArity CompiledClauses)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (\ WithArity CompiledClauses
new WithArity CompiledClauses
old -> WithArity CompiledClauses
old) (ConHead -> QName
conName ConHead
c) WithArity CompiledClauses
br Map QName (WithArity CompiledClauses)
conBrs
      if Map.null conBrs' && Map.null litBrs then do
        -- there are no branches, just return default
        updateCatchAll catchAll fromCatchAll
      else do
        -- Get the type of the scrutinee.
        caseTy <-
          case (Map.keys conBrs', Map.keys litBrs) of
            ([QName]
cs, []) -> TCM CaseType -> ReaderT CCEnv TCM CaseType
forall (m :: * -> *) a. Monad m => m a -> ReaderT CCEnv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM CaseType -> ReaderT CCEnv TCM CaseType)
-> TCM CaseType -> ReaderT CCEnv TCM CaseType
forall a b. (a -> b) -> a -> b
$ [QName] -> TCM CaseType
forall {m :: * -> *}. HasConstInfo m => [QName] -> m CaseType
go [QName]
cs
              where
              go :: [QName] -> m CaseType
go (QName
c:[QName]
cs) = QName -> m QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
c m QName -> (QName -> m Definition) -> m Definition
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo m Definition -> (Definition -> Defn) -> m Defn
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Definition -> Defn
theDef m Defn -> (Defn -> m CaseType) -> m CaseType
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                Constructor{QName
conData :: QName
conData :: Defn -> QName
conData} ->
                  CaseType -> m CaseType
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (CaseType -> m CaseType) -> CaseType -> m CaseType
forall a b. (a -> b) -> a -> b
$ QName -> CaseType
C.CTData QName
conData
                Defn
_ -> [QName] -> m CaseType
go [QName]
cs
              go [] = m CaseType
forall a. HasCallStack => a
__IMPOSSIBLE__
            ([], LitChar   Char
_ : [Literal]
_) -> CaseType -> ReaderT CCEnv TCM CaseType
forall a. a -> ReaderT CCEnv TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return CaseType
C.CTChar
            ([], LitString Text
_ : [Literal]
_) -> CaseType -> ReaderT CCEnv TCM CaseType
forall a. a -> ReaderT CCEnv TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return CaseType
C.CTString
            ([], LitFloat  Double
_ : [Literal]
_) -> CaseType -> ReaderT CCEnv TCM CaseType
forall a. a -> ReaderT CCEnv TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return CaseType
C.CTFloat
            ([], LitQName  QName
_ : [Literal]
_) -> CaseType -> ReaderT CCEnv TCM CaseType
forall a. a -> ReaderT CCEnv TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return CaseType
C.CTQName
            ([QName], [Literal])
_ -> ReaderT CCEnv TCM CaseType
forall a. HasCallStack => a
__IMPOSSIBLE__

        updateCatchAll catchAll $ do
          x <- asks (lookupLevel n . ccCxt)
          def <- fromCatchAll
          let caseInfo = C.CaseInfo
                { caseType :: CaseType
caseType   = CaseType
caseTy
                , caseLazy :: Bool
caseLazy   = Bool
lazy
                , caseErased :: Erased
caseErased = Erased -> Maybe Erased -> Erased
forall a. a -> Maybe a -> a
fromMaybe Erased
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Erased -> Erased) -> Maybe Erased -> Erased
forall a b. (a -> b) -> a -> b
$
                               Quantity -> Maybe Erased
erasedFromQuantity (ArgInfo -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
i)
                }
          C.TCase x caseInfo def <$> do
            br1 <- conAlts n conBrs'
            br2 <- litAlts n litBrs
            return (br1 ++ br2)
  where
    -- normally, Agda should make sure that a pattern match is total,
    -- so we set the default to unreachable if no default has been provided.
    fromCatchAll :: CC C.TTerm
    fromCatchAll :: CC TTerm
fromCatchAll = (CCEnv -> TTerm) -> CC TTerm
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (TTerm -> (Int -> TTerm) -> Maybe Int -> TTerm
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TTerm
C.tUnreachable Int -> TTerm
C.TVar (Maybe Int -> TTerm) -> (CCEnv -> Maybe Int) -> CCEnv -> TTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CCEnv -> Maybe Int
ccCatchAll)

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


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

updateCatchAll :: Maybe CC.CompiledClauses -> (CC C.TTerm -> CC C.TTerm)
updateCatchAll :: Maybe CompiledClauses -> CC TTerm -> CC TTerm
updateCatchAll Maybe CompiledClauses
Nothing CC TTerm
cont = CC TTerm
cont
updateCatchAll (Just CompiledClauses
cc) CC TTerm
cont = do
  def <- CompiledClauses -> CC TTerm
casetree CompiledClauses
cc
  cxt <- asks ccCxt
  reportS "treeless.convert.lambdas" 40 $
    [ "-- updateCatchAll:"
    , "--   cxt =" <+> prettyPure cxt
    , "--   def =" <+> prettyPure def
    ]
  local (\ CCEnv
e -> CCEnv
e { ccCatchAll = Just 0, ccCxt = shift 1 cxt }) $ do
    C.mkLet def <$> cont

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

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

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

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

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

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

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

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


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


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


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

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

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

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

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

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

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

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

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

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