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 :: forall a. Pretty a => a -> TCMT IO Doc
prettyPure = Doc -> TCMT IO Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCMT IO Doc) -> (a -> Doc) -> a -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
forall a. Pretty a => a -> Doc
P.pretty

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

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

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

compilerPipeline :: Int -> QName -> Pipeline
compilerPipeline :: Int -> QName -> Pipeline
compilerPipeline Int
v QName
q =
  [Pipeline] -> Pipeline
Sequential
    -- Issue #4967: No simplification step before builtin translation! Simplification relies
    --              on either all or no builtins being translated. Since we might have inlined
    --              functions that have had the builtin translation applied, we need to apply it
    --              first.
    -- [ compilerPass "simpl"   (35 + v) "simplification"      $ const simplifyTTerm
    [ [Char]
-> Int
-> [Char]
-> (EvaluationStrategy -> TTerm -> TCMT IO TTerm)
-> Pipeline
compilerPass [Char]
"builtin" (Int
30 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
v) [Char]
"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
    , 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 -> TCMT IO TTerm)
-> Pipeline
compilerPass [Char]
"simpl"  (Int
30 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
v) [Char]
"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
      , [Char]
-> Int
-> [Char]
-> (EvaluationStrategy -> TTerm -> TCMT IO TTerm)
-> Pipeline
compilerPass [Char]
"erase"  (Int
30 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
v) [Char]
"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
      , [Char]
-> Int
-> [Char]
-> (EvaluationStrategy -> TTerm -> TCMT IO TTerm)
-> Pipeline
compilerPass [Char]
"uncase" (Int
30 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
v) [Char]
"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
      , [Char]
-> Int
-> [Char]
-> (EvaluationStrategy -> TTerm -> TCMT IO TTerm)
-> Pipeline
compilerPass [Char]
"aspat"  (Int
30 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
v) [Char]
"@-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
      ]
    , [Char]
-> Int
-> [Char]
-> (EvaluationStrategy -> TTerm -> TCMT IO 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 -> 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 Int
n Pipeline
p -> Int
-> EvaluationStrategy
-> QName
-> Pipeline
-> TTerm
-> TCMT IO TTerm
runFixedPoint Int
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 :: (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO ()
dbg TCMT IO Doc -> TCMT IO Doc
f   = [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc ([Char]
"treeless.opt." [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CompilerPass -> [Char]
passTag CompilerPass
p) (CompilerPass -> Int
passVerbosity CompilerPass
p) (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
f (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"-- " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CompilerPass -> [Char]
passName CompilerPass
p)
      pbody :: TTerm -> TCMT IO Doc
pbody TTerm
b = [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
q) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=", Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TTerm -> TCMT IO Doc
forall a. Pretty a => a -> TCMT IO Doc
prettyPure TTerm
b ]
  (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO ()
dbg ((TCMT IO Doc -> TCMT IO Doc) -> TCMT IO ())
-> (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ if | TTerm
t TTerm -> TTerm -> Bool
forall a. Eq a => a -> a -> Bool
== TTerm
t'   -> (TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"(No effect)")
           | Bool
otherwise -> (TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ TTerm -> TCMT IO Doc
pbody TTerm
t')
  TTerm -> TCMT IO TTerm
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t'

runFixedPoint :: Int -> EvaluationStrategy -> QName -> Pipeline -> TTerm -> TCM TTerm
runFixedPoint :: Int
-> EvaluationStrategy
-> QName
-> Pipeline
-> TTerm
-> TCMT IO TTerm
runFixedPoint Int
n EvaluationStrategy
eval QName
q Pipeline
pipeline = Int -> TTerm -> TCMT IO TTerm
go Int
1
  where
    go :: Int -> TTerm -> TCMT IO 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 -> TCMT IO TTerm
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
    go Int
i TTerm
t = do
      [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"treeless.opt.loop" Int
30 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"++ Optimisation loop iteration " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i
      TTerm
t' <- EvaluationStrategy -> QName -> Pipeline -> TTerm -> 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
            [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"treeless.opt.loop" Int
30 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"++ Optimisation loop terminating after " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" iterations"
            TTerm -> TCMT IO TTerm
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t'
         | Bool
otherwise -> Int -> TTerm -> TCMT IO TTerm
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
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
  { ccCxt :: [Int]
ccCxt        = []
  , ccCatchAll :: Maybe Int
ccCatchAll   = Maybe Int
forall a. Maybe a
Nothing
  , ccEvaluation :: EvaluationStrategy
ccEvaluation = EvaluationStrategy
eval
  }

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

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

shift :: Int -> CCContext -> CCContext
shift :: Int -> [Int] -> [Int]
shift Int
n = (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 (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 :: 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 :: Int
a = CompiledClauses -> Int
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
$ [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 (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 (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 (t :: * -> *) a. Foldable t => t a -> Int
length [Arg [Char]]
xs) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
forall a b. (a -> b) -> a -> b
$ do
      -- Issue 2469: Body context size (`length xs`) may be smaller than current context size
      -- if some arguments are not used in the body.
      Term
v <- TCM Term -> ReaderT CCEnv TCM Term
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (AllowedReductions -> TCM Term -> TCM Term
forall (m :: * -> *) a.
MonadTCEnv m =>
AllowedReductions -> m a -> m a
putAllowedReductions ([AllowedReduction] -> AllowedReductions
forall a. SmallSetElement a => [a] -> SmallSet a
SmallSet.fromList [AllowedReduction
ProjectionReductions, AllowedReduction
CopatternReductions]) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Term -> TCM Term
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Term
v)
      [Int]
cxt <- (CCEnv -> [Int]) -> ReaderT CCEnv TCM [Int]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CCEnv -> [Int]
ccCxt
      TTerm
v' <- Term -> CC TTerm
substTerm Term
v
      [Char] -> Int -> [TCMT IO Doc] -> ReaderT CCEnv TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Int -> a -> m ()
reportS [Char]
"treeless.convert.casetree" Int
40 ([TCMT IO Doc] -> ReaderT CCEnv TCM ())
-> [TCMT IO Doc] -> ReaderT CCEnv TCM ()
forall a b. (a -> b) -> a -> b
$
        [ TCMT IO Doc
"-- casetree, calling substTerm:"
        , TCMT IO Doc
"--   cxt =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Int] -> TCMT IO Doc
forall a. Pretty a => a -> TCMT IO Doc
prettyPure [Int]
cxt
        , TCMT IO Doc
"--   v   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a. Pretty a => a -> TCMT IO Doc
prettyPure Term
v
        , TCMT IO Doc
"--   v'  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TTerm -> TCMT IO Doc
forall a. Pretty a => a -> TCMT IO Doc
prettyPure TTerm
v'
        ]
      TTerm -> CC TTerm
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
v'
    CC.Case Arg Int
_ (CC.Branches Bool
True Map QName (WithArity CompiledClauses)
_ Maybe (ConHead, WithArity CompiledClauses)
_ Map Literal CompiledClauses
_ Just{} Maybe Bool
_ Bool
_) -> CC TTerm
forall a. HasCallStack => a
__IMPOSSIBLE__
      -- Andreas, 2016-06-03, issue #1986: Ulf: "no catch-all for copatterns!"
      -- lift $ do
      --   typeError . GenericDocError =<< do
      --     "Not yet implemented: compilation of copattern matching with catch-all clause"
    CC.Case (Arg ArgInfo
_ Int
n) (CC.Branches Bool
True Map QName (WithArity CompiledClauses)
conBrs Maybe (ConHead, WithArity CompiledClauses)
_ Map Literal CompiledClauses
_ Maybe CompiledClauses
Nothing Maybe Bool
_ Bool
_) -> Int -> CC TTerm -> CC TTerm
lambdasUpTo Int
n (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
forall a b. (a -> b) -> a -> b
$ do
      Map QName TTerm -> CC TTerm
mkRecord (Map QName TTerm -> CC TTerm)
-> ReaderT CCEnv TCM (Map QName TTerm) -> CC TTerm
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (CompiledClauses -> CC TTerm)
-> Map QName CompiledClauses -> ReaderT CCEnv TCM (Map QName TTerm)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
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
                    -- 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 -> TCMT IO QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
c TCMT IO 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
          Int
x <- (CCEnv -> Int) -> ReaderT CCEnv TCM Int
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Int -> [Int] -> Int
lookupLevel Int
n ([Int] -> Int) -> (CCEnv -> [Int]) -> CCEnv -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CCEnv -> [Int]
ccCxt)
          TTerm
def <- CC TTerm
fromCatchAll
          let caseInfo :: CaseInfo
caseInfo = C.CaseInfo { caseType :: CaseType
caseType = CaseType
caseTy, caseLazy :: Bool
caseLazy = Bool
lazy }
          Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
C.TCase Int
x CaseInfo
caseInfo TTerm
def ([TAlt] -> TTerm) -> ReaderT CCEnv TCM [TAlt] -> CC TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
            [TAlt]
br1 <- Int
-> Map QName (WithArity CompiledClauses)
-> ReaderT CCEnv TCM [TAlt]
conAlts Int
n Map QName (WithArity CompiledClauses)
conBrs'
            [TAlt]
br2 <- Int -> Map Literal CompiledClauses -> ReaderT CCEnv TCM [TAlt]
litAlts Int
n Map Literal CompiledClauses
litBrs
            [TAlt] -> ReaderT CCEnv TCM [TAlt]
forall (m :: * -> *) a. Monad m => a -> m a
return ([TAlt]
br1 [TAlt] -> [TAlt] -> [TAlt]
forall a. [a] -> [a] -> [a]
++ [TAlt]
br2)
  where
    -- normally, Agda should make sure that a pattern match is total,
    -- so we set the default to unreachable if no default has been provided.
    fromCatchAll :: CC C.TTerm
    fromCatchAll :: CC TTerm
fromCatchAll = (CCEnv -> TTerm) -> CC TTerm
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (TTerm -> (Int -> TTerm) -> Maybe Int -> TTerm
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TTerm
C.tUnreachable Int -> TTerm
C.TVar (Maybe Int -> TTerm) -> (CCEnv -> Maybe Int) -> CCEnv -> TTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CCEnv -> Maybe Int
ccCatchAll)

commonArity :: CC.CompiledClauses -> Int
commonArity :: CompiledClauses -> Int
commonArity CompiledClauses
cc =
  case Int -> CompiledClauses -> [Int]
forall {a}. Int -> CompiledClauses' a -> [Int]
arities Int
0 CompiledClauses
cc of
    [] -> Int
0
    [Int]
as -> [Int] -> Int
forall (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 (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 (t :: * -> *) a. Foldable t => t a -> Int
length [Arg [Char]]
xs)]


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

updateCatchAll :: Maybe CC.CompiledClauses -> (CC C.TTerm -> CC C.TTerm)
updateCatchAll :: Maybe CompiledClauses -> CC TTerm -> CC TTerm
updateCatchAll Maybe CompiledClauses
Nothing CC TTerm
cont = CC TTerm
cont
updateCatchAll (Just CompiledClauses
cc) CC TTerm
cont = do
  TTerm
def <- CompiledClauses -> CC TTerm
casetree CompiledClauses
cc
  [Int]
cxt <- (CCEnv -> [Int]) -> ReaderT CCEnv TCM [Int]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CCEnv -> [Int]
ccCxt
  [Char] -> Int -> [TCMT IO Doc] -> ReaderT CCEnv TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Int -> a -> m ()
reportS [Char]
"treeless.convert.lambdas" Int
40 ([TCMT IO Doc] -> ReaderT CCEnv TCM ())
-> [TCMT IO Doc] -> ReaderT CCEnv TCM ()
forall a b. (a -> b) -> a -> b
$
    [ TCMT IO Doc
"-- updateCatchAll:"
    , TCMT IO Doc
"--   cxt =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Int] -> TCMT IO Doc
forall a. Pretty a => a -> TCMT IO Doc
prettyPure [Int]
cxt
    , TCMT IO Doc
"--   def =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TTerm -> TCMT IO Doc
forall a. Pretty a => a -> TCMT IO Doc
prettyPure TTerm
def
    ]
  (CCEnv -> CCEnv) -> CC TTerm -> CC TTerm
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ CCEnv
e -> CCEnv
e { ccCatchAll :: Maybe Int
ccCatchAll = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
0, ccCxt :: [Int]
ccCxt = Int -> [Int] -> [Int]
shift Int
1 [Int]
cxt }) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
forall a b. (a -> b) -> a -> b
$ do
    TTerm -> TTerm -> TTerm
C.mkLet TTerm
def (TTerm -> TTerm) -> CC TTerm -> CC TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CC TTerm
cont

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

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

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

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

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

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

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

-- | Replace de Bruijn Level @x@ by @n@ new variables.
replaceVar :: Int -> Int -> CC a -> CC a
replaceVar :: forall a. Int -> Int -> CC a -> CC a
replaceVar Int
x Int
n CC a
cont = do
  let upd :: [Int] -> [Int]
upd [Int]
cxt = Int -> [Int] -> [Int]
shift Int
n [Int]
ys [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int]
ixs [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ Int -> [Int] -> [Int]
shift Int
n [Int]
zs
       where
         -- compute the de Bruijn index
         i :: Int
i = [Int] -> Int
forall (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 r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\CCEnv
e -> CCEnv
e { ccCxt :: [Int]
ccCxt = [Int] -> [Int]
upd (CCEnv -> [Int]
ccCxt CCEnv
e) , ccCatchAll :: Maybe Int
ccCatchAll = (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
n) (Int -> Int) -> Maybe Int -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CCEnv -> Maybe Int
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)
-> TCMT IO QName -> TCMT IO Definition
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName (QName -> TCMT IO QName)
-> (ConHead -> QName) -> ConHead -> TCMT IO QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> QName
I.conName (ConHead -> TCMT IO QName) -> TCMT IO ConHead -> TCMT IO QName
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO ConHead
recConFromProj QName
p1)
  [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"treeless.convert.mkRecord" Int
60 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"record constructor fields: xs      = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> ([Arg QName] -> [Char]) -> [Arg QName] -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Arg QName] -> [Char]
forall a. Show a => a -> [Char]
show) [Arg QName]
xs
    , [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"to be filled with content: keys fs = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> ([QName] -> [Char]) -> [QName] -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [QName] -> [Char]
forall a. Show a => a -> [Char]
show) (Map QName TTerm -> [QName]
forall k a. Map k a -> [k]
Map.keys Map QName TTerm
fs)
    ]
  -- Convert the constructor
  let (Args
args :: [C.TTerm]) = [Arg QName] -> (Arg QName -> TTerm) -> Args
forall (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 Int
ind Elims
es -> do
      Int
ind' <- (CCEnv -> Int) -> ReaderT CCEnv TCM Int
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Int -> [Int] -> Int
lookupIndex Int
ind ([Int] -> Int) -> (CCEnv -> [Int]) -> CCEnv -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CCEnv -> [Int]
ccCxt)
      let args :: [Arg Term]
args = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
I.allApplyElims Elims
es
      TTerm -> Args -> TTerm
C.mkTApp (Int -> TTerm
C.TVar Int
ind') (Args -> TTerm) -> ReaderT CCEnv TCM Args -> CC TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Term] -> ReaderT CCEnv TCM Args
substArgs [Arg Term]
args
    I.Lam ArgInfo
_ Abs Term
ab ->
      TTerm -> TTerm
C.TLam (TTerm -> TTerm) -> CC TTerm -> CC TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        (CCEnv -> CCEnv) -> CC TTerm -> CC TTerm
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\CCEnv
e -> CCEnv
e { ccCxt :: [Int]
ccCxt = Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: Int -> [Int] -> [Int]
shift Int
1 (CCEnv -> [Int]
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' <- TCMT IO QName -> ReaderT CCEnv TCM QName
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO QName -> ReaderT CCEnv TCM QName)
-> TCMT IO QName -> ReaderT CCEnv TCM QName
forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName (QName -> TCMT IO QName) -> QName -> TCMT IO 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
$ [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 (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 (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