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

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

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

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

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

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

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

import Agda.Utils.Impossible

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

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

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

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

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

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

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

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

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

compilerPipeline :: Int -> QName -> Pipeline
compilerPipeline :: VerboseLevel -> QName -> Pipeline
compilerPipeline VerboseLevel
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
    [ VerboseKey
-> VerboseLevel
-> VerboseKey
-> (EvaluationStrategy -> TTerm -> TCMT IO TTerm)
-> Pipeline
compilerPass VerboseKey
"builtin" (VerboseLevel
30 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
v) VerboseKey
"builtin translation" ((EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline)
-> (EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline
forall a b. (a -> b) -> a -> b
$ (TTerm -> TCMT IO TTerm)
-> EvaluationStrategy -> TTerm -> TCMT IO TTerm
forall a b. a -> b -> a
const TTerm -> TCMT IO TTerm
translateBuiltins
    , VerboseLevel -> Pipeline -> Pipeline
FixedPoint VerboseLevel
5 (Pipeline -> Pipeline) -> Pipeline -> Pipeline
forall a b. (a -> b) -> a -> b
$ [Pipeline] -> Pipeline
Sequential
      [ VerboseKey
-> VerboseLevel
-> VerboseKey
-> (EvaluationStrategy -> TTerm -> TCMT IO TTerm)
-> Pipeline
compilerPass VerboseKey
"simpl"  (VerboseLevel
30 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
v) VerboseKey
"simplification"     ((EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline)
-> (EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline
forall a b. (a -> b) -> a -> b
$ (TTerm -> TCMT IO TTerm)
-> EvaluationStrategy -> TTerm -> TCMT IO TTerm
forall a b. a -> b -> a
const TTerm -> TCMT IO TTerm
simplifyTTerm
      , VerboseKey
-> VerboseLevel
-> VerboseKey
-> (EvaluationStrategy -> TTerm -> TCMT IO TTerm)
-> Pipeline
compilerPass VerboseKey
"erase"  (VerboseLevel
30 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
v) VerboseKey
"erasure"            ((EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline)
-> (EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline
forall a b. (a -> b) -> a -> b
$ QName -> EvaluationStrategy -> TTerm -> TCMT IO TTerm
eraseTerms QName
q
      , VerboseKey
-> VerboseLevel
-> VerboseKey
-> (EvaluationStrategy -> TTerm -> TCMT IO TTerm)
-> Pipeline
compilerPass VerboseKey
"uncase" (VerboseLevel
30 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
v) VerboseKey
"uncase"             ((EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline)
-> (EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline
forall a b. (a -> b) -> a -> b
$ (TTerm -> TCMT IO TTerm)
-> EvaluationStrategy -> TTerm -> TCMT IO TTerm
forall a b. a -> b -> a
const TTerm -> TCMT IO TTerm
forall (m :: * -> *). Monad m => TTerm -> m TTerm
caseToSeq
      , VerboseKey
-> VerboseLevel
-> VerboseKey
-> (EvaluationStrategy -> TTerm -> TCMT IO TTerm)
-> Pipeline
compilerPass VerboseKey
"aspat"  (VerboseLevel
30 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
v) VerboseKey
"@-pattern recovery" ((EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline)
-> (EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline
forall a b. (a -> b) -> a -> b
$ (TTerm -> TCMT IO TTerm)
-> EvaluationStrategy -> TTerm -> TCMT IO TTerm
forall a b. a -> b -> a
const TTerm -> TCMT IO TTerm
forall (m :: * -> *). Monad m => TTerm -> m TTerm
recoverAsPatterns
      ]
    , VerboseKey
-> VerboseLevel
-> VerboseKey
-> (EvaluationStrategy -> TTerm -> TCMT IO TTerm)
-> Pipeline
compilerPass VerboseKey
"id" (VerboseLevel
30 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
v) VerboseKey
"identity function detection" ((EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline)
-> (EvaluationStrategy -> TTerm -> TCMT IO TTerm) -> Pipeline
forall a b. (a -> b) -> a -> b
$ (TTerm -> TCMT IO TTerm)
-> EvaluationStrategy -> TTerm -> TCMT IO TTerm
forall a b. a -> b -> a
const (QName -> TTerm -> TCMT IO TTerm
detectIdentityFunctions QName
q)
    ]

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

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

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

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

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

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

-- | Environment for naming of local variables.
data CCEnv = CCEnv
  { CCEnv -> CCContext
ccCxt        :: CCContext  -- ^ Maps case tree de-bruijn indices to TTerm de-bruijn indices
  , CCEnv -> Maybe VerboseLevel
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 :: VerboseLevel -> CCContext -> CCContext
shift VerboseLevel
n = (VerboseLevel -> VerboseLevel) -> CCContext -> CCContext
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+VerboseLevel
n)

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

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

-- | Compile a case tree into nested case and record expressions.
casetreeTop :: EvaluationStrategy -> CC.CompiledClauses -> TCM C.TTerm
casetreeTop :: EvaluationStrategy -> CompiledClauses -> TCMT IO TTerm
casetreeTop EvaluationStrategy
eval CompiledClauses
cc = (CC TTerm -> CCEnv -> TCMT IO TTerm)
-> CCEnv -> CC TTerm -> TCMT IO TTerm
forall a b c. (a -> b -> c) -> b -> a -> c
flip CC TTerm -> CCEnv -> TCMT IO TTerm
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (EvaluationStrategy -> CCEnv
initCCEnv EvaluationStrategy
eval) (CC TTerm -> TCMT IO TTerm) -> CC TTerm -> TCMT IO TTerm
forall a b. (a -> b) -> a -> b
$ do
  let a :: VerboseLevel
a = CompiledClauses -> VerboseLevel
commonArity CompiledClauses
cc
  TCMT IO () -> ReaderT CCEnv TCM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO () -> ReaderT CCEnv TCM ())
-> TCMT IO () -> ReaderT CCEnv TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> VerboseKey -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"treeless.convert.arity" VerboseLevel
40 (VerboseKey -> TCMT IO ()) -> VerboseKey -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"-- common arity: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show VerboseLevel
a
  VerboseLevel -> CC TTerm -> CC TTerm
lambdasUpTo VerboseLevel
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 VerboseKey]
xs -> VerboseLevel -> CC TTerm -> CC TTerm
withContextSize ([Arg VerboseKey] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Arg VerboseKey]
xs) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
forall a b. (a -> b) -> a -> b
$ TTerm -> CC TTerm
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
C.tUnreachable
    CC.Done [Arg VerboseKey]
xs Term
v -> VerboseLevel -> CC TTerm -> CC TTerm
withContextSize ([Arg VerboseKey] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Arg VerboseKey]
xs) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
forall a b. (a -> b) -> a -> b
$ do
      -- Issue 2469: Body context size (`length xs`) may be smaller than current context size
      -- if some arguments are not used in the body.
      Term
v <- TCM Term -> ReaderT CCEnv TCM Term
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (AllowedReductions -> TCM Term -> TCM Term
forall (m :: * -> *) a.
MonadTCEnv m =>
AllowedReductions -> m a -> m a
putAllowedReductions ([AllowedReduction] -> AllowedReductions
forall a. SmallSetElement a => [a] -> SmallSet a
SmallSet.fromList [AllowedReduction
ProjectionReductions, AllowedReduction
CopatternReductions]) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Term -> TCM Term
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Term
v)
      CCContext
cxt <- (CCEnv -> CCContext) -> ReaderT CCEnv TCM CCContext
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CCEnv -> CCContext
ccCxt
      TTerm
v' <- Term -> CC TTerm
substTerm Term
v
      VerboseKey -> VerboseLevel -> [TCM Doc] -> ReaderT CCEnv TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
VerboseKey -> VerboseLevel -> a -> m ()
reportS VerboseKey
"treeless.convert.casetree" VerboseLevel
40 ([TCM Doc] -> ReaderT CCEnv TCM ())
-> [TCM Doc] -> ReaderT CCEnv TCM ()
forall a b. (a -> b) -> a -> b
$
        [ TCM Doc
"-- casetree, calling substTerm:"
        , TCM Doc
"--   cxt =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> CCContext -> TCM Doc
forall a. Pretty a => a -> TCM Doc
prettyPure CCContext
cxt
        , TCM Doc
"--   v   =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a. Pretty a => a -> TCM Doc
prettyPure Term
v
        , TCM Doc
"--   v'  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TTerm -> TCM Doc
forall a. Pretty a => a -> TCM Doc
prettyPure TTerm
v'
        ]
      TTerm -> CC TTerm
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
v'
    CC.Case Arg VerboseLevel
_ (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
_ VerboseLevel
n) (CC.Branches Bool
True Map QName (WithArity CompiledClauses)
conBrs Maybe (ConHead, WithArity CompiledClauses)
_ Map Literal CompiledClauses
_ Maybe CompiledClauses
Nothing Maybe Bool
_ Bool
_) -> VerboseLevel -> CC TTerm -> CC TTerm
lambdasUpTo VerboseLevel
n (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
forall a b. (a -> b) -> a -> b
$ do
      Map QName TTerm -> CC TTerm
mkRecord (Map QName TTerm -> CC TTerm)
-> ReaderT CCEnv TCM (Map QName TTerm) -> CC TTerm
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (CompiledClauses -> CC TTerm)
-> Map QName CompiledClauses -> ReaderT CCEnv TCM (Map QName TTerm)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse CompiledClauses -> CC TTerm
casetree (WithArity CompiledClauses -> CompiledClauses
forall c. WithArity c -> c
CC.content (WithArity CompiledClauses -> CompiledClauses)
-> Map QName (WithArity CompiledClauses)
-> Map QName CompiledClauses
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map QName (WithArity CompiledClauses)
conBrs)
    CC.Case (Arg ArgInfo
i VerboseLevel
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) -> VerboseLevel -> CC TTerm -> CC TTerm
lambdasUpTo (VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
1) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
forall a b. (a -> b) -> a -> b
$ do
                    -- We can treat eta-matches as regular matches here.
      let conBrs' :: Map QName (WithArity CompiledClauses)
conBrs' = Maybe (ConHead, WithArity CompiledClauses)
-> Map QName (WithArity CompiledClauses)
-> ((ConHead, WithArity CompiledClauses)
    -> Map QName (WithArity CompiledClauses))
-> Map QName (WithArity CompiledClauses)
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (ConHead, WithArity CompiledClauses)
etaBr Map QName (WithArity CompiledClauses)
conBrs (((ConHead, WithArity CompiledClauses)
  -> Map QName (WithArity CompiledClauses))
 -> Map QName (WithArity CompiledClauses))
-> ((ConHead, WithArity CompiledClauses)
    -> Map QName (WithArity CompiledClauses))
-> Map QName (WithArity CompiledClauses)
forall a b. (a -> b) -> a -> b
$ \ (ConHead
c, WithArity CompiledClauses
br) -> (WithArity CompiledClauses
 -> WithArity CompiledClauses -> WithArity CompiledClauses)
-> QName
-> WithArity CompiledClauses
-> Map QName (WithArity CompiledClauses)
-> Map QName (WithArity CompiledClauses)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (\ WithArity CompiledClauses
new WithArity CompiledClauses
old -> WithArity CompiledClauses
old) (ConHead -> QName
conName ConHead
c) WithArity CompiledClauses
br Map QName (WithArity CompiledClauses)
conBrs
      if Map QName (WithArity CompiledClauses) -> Bool
forall k a. Map k a -> Bool
Map.null Map QName (WithArity CompiledClauses)
conBrs' Bool -> Bool -> Bool
&& Map Literal CompiledClauses -> Bool
forall k a. Map k a -> Bool
Map.null Map Literal CompiledClauses
litBrs then do
        -- there are no branches, just return default
        Maybe CompiledClauses -> CC TTerm -> CC TTerm
updateCatchAll Maybe CompiledClauses
catchAll CC TTerm
fromCatchAll
      else do
        -- Get the type of the scrutinee.
        CaseType
caseTy <-
          case (Map QName (WithArity CompiledClauses) -> [QName]
forall k a. Map k a -> [k]
Map.keys Map QName (WithArity CompiledClauses)
conBrs', Map Literal CompiledClauses -> [Literal]
forall k a. Map k a -> [k]
Map.keys Map Literal CompiledClauses
litBrs) of
            ([QName]
cs, []) -> TCM CaseType -> ReaderT CCEnv TCM CaseType
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM CaseType -> ReaderT CCEnv TCM CaseType)
-> TCM CaseType -> ReaderT CCEnv TCM CaseType
forall a b. (a -> b) -> a -> b
$ [QName] -> TCM CaseType
go [QName]
cs
              where
              go :: [QName] -> TCM CaseType
go (QName
c:[QName]
cs) = QName -> TCM QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
c TCM QName -> (QName -> TCMT IO Definition) -> TCMT IO Definition
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo TCMT IO Definition -> (Definition -> Defn) -> TCMT IO Defn
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> Definition -> Defn
theDef TCMT IO Defn -> (Defn -> TCM CaseType) -> TCM CaseType
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                Constructor{QName
conData :: Defn -> QName
conData :: QName
conData} ->
                  CaseType -> TCM CaseType
forall (m :: * -> *) a. Monad m => a -> m a
return (CaseType -> TCM CaseType) -> CaseType -> TCM CaseType
forall a b. (a -> b) -> a -> b
$ Quantity -> QName -> CaseType
C.CTData (ArgInfo -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
i) QName
conData
                Defn
_ -> [QName] -> TCM CaseType
go [QName]
cs
              go [] = TCM CaseType
forall a. HasCallStack => a
__IMPOSSIBLE__
            ([], LitChar   Char
_ : [Literal]
_) -> CaseType -> ReaderT CCEnv TCM CaseType
forall (m :: * -> *) a. Monad m => a -> m a
return CaseType
C.CTChar
            ([], LitString Text
_ : [Literal]
_) -> CaseType -> ReaderT CCEnv TCM CaseType
forall (m :: * -> *) a. Monad m => a -> m a
return CaseType
C.CTString
            ([], LitFloat  Double
_ : [Literal]
_) -> CaseType -> ReaderT CCEnv TCM CaseType
forall (m :: * -> *) a. Monad m => a -> m a
return CaseType
C.CTFloat
            ([], LitQName  QName
_ : [Literal]
_) -> CaseType -> ReaderT CCEnv TCM CaseType
forall (m :: * -> *) a. Monad m => a -> m a
return CaseType
C.CTQName
            ([QName], [Literal])
_ -> ReaderT CCEnv TCM CaseType
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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


    wArities :: VerboseLevel -> WithArity (CompiledClauses' a) -> CCContext
wArities VerboseLevel
cxt (WithArity VerboseLevel
k CompiledClauses' a
c) = (VerboseLevel -> VerboseLevel) -> CCContext -> CCContext
forall a b. (a -> b) -> [a] -> [b]
map (\ VerboseLevel
x -> VerboseLevel
x VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
k VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
1) (CCContext -> CCContext) -> CCContext -> CCContext
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> CompiledClauses' a -> CCContext
arities (VerboseLevel
cxt VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
1 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
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
  CCContext
cxt <- (CCEnv -> CCContext) -> ReaderT CCEnv TCM CCContext
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CCEnv -> CCContext
ccCxt
  VerboseKey -> VerboseLevel -> [TCM Doc] -> ReaderT CCEnv TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
VerboseKey -> VerboseLevel -> a -> m ()
reportS VerboseKey
"treeless.convert.lambdas" VerboseLevel
40 ([TCM Doc] -> ReaderT CCEnv TCM ())
-> [TCM Doc] -> ReaderT CCEnv TCM ()
forall a b. (a -> b) -> a -> b
$
    [ TCM Doc
"-- updateCatchAll:"
    , TCM Doc
"--   cxt =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> CCContext -> TCM Doc
forall a. Pretty a => a -> TCM Doc
prettyPure CCContext
cxt
    , TCM Doc
"--   def =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TTerm -> TCM Doc
forall a. Pretty a => a -> TCM Doc
prettyPure TTerm
def
    ]
  (CCEnv -> CCEnv) -> CC TTerm -> CC TTerm
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ CCEnv
e -> CCEnv
e { ccCatchAll :: Maybe VerboseLevel
ccCatchAll = VerboseLevel -> Maybe VerboseLevel
forall a. a -> Maybe a
Just VerboseLevel
0, ccCxt :: CCContext
ccCxt = VerboseLevel -> CCContext -> CCContext
shift VerboseLevel
1 CCContext
cxt }) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
forall a b. (a -> b) -> a -> b
$ do
    TTerm -> TTerm -> TTerm
C.mkLet TTerm
def (TTerm -> TTerm) -> CC TTerm -> CC TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CC TTerm
cont

-- | Shrinks or grows the context to the given size.
-- Does not update the catchAll expression, the catchAll expression
-- MUST NOT be used inside `cont`.
withContextSize :: Int -> CC C.TTerm -> CC C.TTerm
withContextSize :: VerboseLevel -> CC TTerm -> CC TTerm
withContextSize VerboseLevel
n CC TTerm
cont = do
  VerboseLevel
diff <- (CCEnv -> VerboseLevel) -> ReaderT CCEnv TCM VerboseLevel
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (((VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-) (VerboseLevel -> VerboseLevel)
-> (CCContext -> VerboseLevel) -> CCContext -> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CCContext -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length) (CCContext -> VerboseLevel)
-> (CCEnv -> CCContext) -> CCEnv -> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CCEnv -> CCContext
ccCxt)
  if VerboseLevel
diff VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
>= VerboseLevel
1 then VerboseLevel -> CC TTerm -> CC TTerm
createLambdas VerboseLevel
diff CC TTerm
cont else do
    let diff' :: VerboseLevel
diff' = -VerboseLevel
diff
    CCContext
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`.
       --
       VerboseLevel -> CCContext -> CCContext
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
diff' (CCContext -> CCContext)
-> ReaderT CCEnv TCM CCContext -> ReaderT CCEnv TCM CCContext
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CCEnv -> CCContext) -> ReaderT CCEnv TCM CCContext
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CCEnv -> CCContext
ccCxt
    (CCEnv -> CCEnv) -> CC TTerm -> CC TTerm
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ CCEnv
e -> CCEnv
e { ccCxt :: CCContext
ccCxt = CCContext
cxt }) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
forall a b. (a -> b) -> a -> b
$ do
      VerboseKey -> VerboseLevel -> [TCM Doc] -> ReaderT CCEnv TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
VerboseKey -> VerboseLevel -> a -> m ()
reportS VerboseKey
"treeless.convert.lambdas" VerboseLevel
40 ([TCM Doc] -> ReaderT CCEnv TCM ())
-> [TCM Doc] -> ReaderT CCEnv TCM ()
forall a b. (a -> b) -> a -> b
$
        [ TCM Doc
"-- withContextSize:"
        , TCM Doc
"--   n   =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseLevel -> TCM Doc
forall a. Pretty a => a -> TCM Doc
prettyPure VerboseLevel
n
        , TCM Doc
"--   diff=" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseLevel -> TCM Doc
forall a. Pretty a => a -> TCM Doc
prettyPure VerboseLevel
diff
        , TCM Doc
"--   cxt =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> CCContext -> TCM Doc
forall a. Pretty a => a -> TCM Doc
prettyPure CCContext
cxt
        ]
      CC TTerm
cont CC TTerm -> (TTerm -> TTerm) -> CC TTerm
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> (TTerm -> Args -> TTerm
`C.mkTApp` (VerboseLevel -> TTerm) -> CCContext -> Args
forall a b. (a -> b) -> [a] -> [b]
map VerboseLevel -> TTerm
C.TVar (VerboseLevel -> CCContext
forall a. Integral a => a -> [a]
downFrom VerboseLevel
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 :: VerboseLevel -> CC TTerm -> CC TTerm
createLambdas VerboseLevel
diff CC TTerm
cont = do
  Bool -> ReaderT CCEnv TCM () -> ReaderT CCEnv TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (VerboseLevel
diff VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
>= VerboseLevel
1) ReaderT CCEnv TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
  CCContext
cxt <- ([VerboseLevel
0 .. VerboseLevel
diffVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-VerboseLevel
1] CCContext -> CCContext -> CCContext
forall a. [a] -> [a] -> [a]
++) (CCContext -> CCContext)
-> (CCContext -> CCContext) -> CCContext -> CCContext
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> CCContext -> CCContext
shift VerboseLevel
diff (CCContext -> CCContext)
-> ReaderT CCEnv TCM CCContext -> ReaderT CCEnv TCM CCContext
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CCEnv -> CCContext) -> ReaderT CCEnv TCM CCContext
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CCEnv -> CCContext
ccCxt
  (CCEnv -> CCEnv) -> CC TTerm -> CC TTerm
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ CCEnv
e -> CCEnv
e { ccCxt :: CCContext
ccCxt = CCContext
cxt }) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
forall a b. (a -> b) -> a -> b
$ do
    VerboseKey -> VerboseLevel -> [TCM Doc] -> ReaderT CCEnv TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
VerboseKey -> VerboseLevel -> a -> m ()
reportS VerboseKey
"treeless.convert.lambdas" VerboseLevel
40 ([TCM Doc] -> ReaderT CCEnv TCM ())
-> [TCM Doc] -> ReaderT CCEnv TCM ()
forall a b. (a -> b) -> a -> b
$
      [ TCM Doc
"-- createLambdas:"
      , TCM Doc
"--   diff =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseLevel -> TCM Doc
forall a. Pretty a => a -> TCM Doc
prettyPure VerboseLevel
diff
      , TCM Doc
"--   cxt  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> CCContext -> TCM Doc
forall a. Pretty a => a -> TCM Doc
prettyPure CCContext
cxt
      ]
    -- Prepend diff lambdas
    CC TTerm
cont CC TTerm -> (TTerm -> TTerm) -> CC TTerm
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ TTerm
t -> (TTerm -> TTerm) -> TTerm -> Args
forall a. (a -> a) -> a -> [a]
List.iterate TTerm -> TTerm
C.TLam TTerm
t Args -> VerboseLevel -> TTerm
forall a. [a] -> VerboseLevel -> a
!! VerboseLevel
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 :: VerboseLevel -> CC TTerm -> CC TTerm
lambdasUpTo VerboseLevel
n CC TTerm
cont = do
  VerboseLevel
diff <- (CCEnv -> VerboseLevel) -> ReaderT CCEnv TCM VerboseLevel
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (((VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-) (VerboseLevel -> VerboseLevel)
-> (CCContext -> VerboseLevel) -> CCContext -> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CCContext -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length) (CCContext -> VerboseLevel)
-> (CCEnv -> CCContext) -> CCEnv -> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CCEnv -> CCContext
ccCxt)

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

conAlts :: Int -> Map QName (CC.WithArity CC.CompiledClauses) -> CC [C.TAlt]
conAlts :: VerboseLevel
-> Map QName (WithArity CompiledClauses)
-> ReaderT CCEnv TCM [TAlt]
conAlts VerboseLevel
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 VerboseLevel
n CompiledClauses
cc) -> do
  QName
c' <- TCM QName -> ReaderT CCEnv TCM QName
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM QName -> ReaderT CCEnv TCM QName)
-> TCM QName -> ReaderT CCEnv TCM QName
forall a b. (a -> b) -> a -> b
$ QName -> TCM QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
c
  VerboseLevel
-> VerboseLevel -> ReaderT CCEnv TCM TAlt -> ReaderT CCEnv TCM TAlt
forall a. VerboseLevel -> VerboseLevel -> CC a -> CC a
replaceVar VerboseLevel
x VerboseLevel
n (ReaderT CCEnv TCM TAlt -> ReaderT CCEnv TCM TAlt)
-> ReaderT CCEnv TCM TAlt -> ReaderT CCEnv TCM TAlt
forall a b. (a -> b) -> a -> b
$ do
    (TTerm -> TAlt) -> CompiledClauses -> ReaderT CCEnv TCM TAlt
branch (QName -> VerboseLevel -> TTerm -> TAlt
C.TACon QName
c' VerboseLevel
n) CompiledClauses
cc

litAlts :: Int -> Map Literal CC.CompiledClauses -> CC [C.TAlt]
litAlts :: VerboseLevel
-> Map Literal CompiledClauses -> ReaderT CCEnv TCM [TAlt]
litAlts VerboseLevel
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!
  VerboseLevel
-> VerboseLevel -> ReaderT CCEnv TCM TAlt -> ReaderT CCEnv TCM TAlt
forall a. VerboseLevel -> VerboseLevel -> CC a -> CC a
replaceVar VerboseLevel
x VerboseLevel
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 :: VerboseLevel -> VerboseLevel -> CC a -> CC a
replaceVar VerboseLevel
x VerboseLevel
n CC a
cont = do
  let upd :: CCContext -> CCContext
upd CCContext
cxt = VerboseLevel -> CCContext -> CCContext
shift VerboseLevel
n CCContext
ys CCContext -> CCContext -> CCContext
forall a. [a] -> [a] -> [a]
++ CCContext
ixs CCContext -> CCContext -> CCContext
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> CCContext -> CCContext
shift VerboseLevel
n CCContext
zs
       where
         -- compute the de Bruijn index
         i :: VerboseLevel
i = CCContext -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length CCContext
cxt VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
1 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
x
         -- discard index i
         (CCContext
ys, VerboseLevel
_:CCContext
zs) = VerboseLevel -> CCContext -> (CCContext, CCContext)
forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt VerboseLevel
i CCContext
cxt
         -- compute the de-bruijn indexes of the newly inserted variables
         ixs :: CCContext
ixs = [VerboseLevel
0..(VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
1)]
  (CCEnv -> CCEnv) -> CC a -> CC a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\CCEnv
e -> CCEnv
e { ccCxt :: CCContext
ccCxt = CCContext -> CCContext
upd (CCEnv -> CCContext
ccCxt CCEnv
e) , ccCatchAll :: Maybe VerboseLevel
ccCatchAll = (VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+VerboseLevel
n) (VerboseLevel -> VerboseLevel)
-> Maybe VerboseLevel -> Maybe VerboseLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CCEnv -> Maybe VerboseLevel
ccCatchAll CCEnv
e }) (CC a -> CC a) -> CC a -> CC a
forall a b. (a -> b) -> a -> b
$
    CC a
cont


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


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


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

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

      -- If the abstraction is void, we don't have to strengthen.
      I.Lam ArgInfo
_ (NoAbs VerboseKey
_ 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 VerboseKey
_ 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
$ VerboseLevel -> SubstArg Term -> Term -> Term
forall a. Subst a => VerboseLevel -> SubstArg a -> a -> a
subst VerboseLevel
0 (Term -> Term
DontCare Term
HasCallStack => Term
__DUMMY_TERM__) Term
u
          BinAppView
_ -> Either Term Term
done

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

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

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

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

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