module Agda.Compiler.ToTreeless
( toTreeless
, closedTermToTreeless
) where
import Control.Arrow (first)
import Control.Monad.Reader
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Traversable (traverse)
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)
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
getCompiledClauses :: QName -> TCM CC.CompiledClauses
getCompiledClauses :: QName -> TCM CompiledClauses
getCompiledClauses q :: 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 "treeless.convert" 40 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ "-- 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. (Monad 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
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [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. (Monad 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 "treeless.convert" 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 "-- not using split tree" ((SplitTree -> TCM Doc) -> TCM Doc)
-> (SplitTree -> TCM Doc) -> TCM Doc
forall a b. (a -> b) -> a -> b
$ \st :: SplitTree
st ->
"-- 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. (Monad m, Pretty a) => a -> m Doc
pretty SplitTree
st
RunRecordPatternTranslation
-> [Clause] -> Maybe SplitTree -> TCM CompiledClauses
CC.compileClauses' RunRecordPatternTranslation
translate [Clause]
cs Maybe SplitTree
mst
toTreeless :: EvaluationStrategy -> QName -> TCM (Maybe C.TTerm)
toTreeless :: EvaluationStrategy -> QName -> TCM (Maybe TTerm)
toTreeless eval :: EvaluationStrategy
eval q :: 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' eval :: EvaluationStrategy
eval q :: 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)
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 "treeless.convert" 20 ("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)
EvaluationStrategy -> QName -> CompiledClauses -> TCMT IO TTerm
ccToTreeless EvaluationStrategy
eval QName
q CompiledClauses
cc
cacheTreeless :: EvaluationStrategy -> QName -> TCM ()
cacheTreeless :: EvaluationStrategy -> QName -> TCMT IO ()
cacheTreeless eval :: EvaluationStrategy
eval q :: 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
_ -> () -> 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 eval :: EvaluationStrategy
eval q :: QName
q cc :: CompiledClauses
cc = do
let pbody :: a -> TCM Doc
pbody b :: a
b = VerboseKey -> a -> TCM Doc
forall a. Pretty a => VerboseKey -> a -> TCM Doc
pbody' "" a
b
pbody' :: VerboseKey -> a -> TCM Doc
pbody' suf :: VerboseKey
suf b :: a
b = [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ VerboseKey -> TCM Doc
forall (m :: * -> *). Monad 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
<+> "=", VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ a -> TCM Doc
forall a. Pretty a => a -> TCM Doc
prettyPure a
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 20) (VerboseLevel -> TCMT IO VerboseLevel
forall (m :: * -> *) a. Monad m => a -> m a
return 0)
VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "treeless.convert" (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
$ "-- 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 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 "treeless.opt.converted" (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
$ "-- converted" 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
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
[Bool]
used <- QName -> TTerm -> TCM [Bool]
usedArguments QName
q TTerm
body
Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((Bool -> Bool) -> [Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Bool -> Bool
not [Bool]
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 "treeless.opt.unused" (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
$
"-- used args:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
hsep [ if Bool
u then VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text [Char
x] else "_" | (x :: Char
x, u :: Bool
u) <- VerboseKey -> [Bool] -> [(Char, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip ['a'..] [Bool]
used ] TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
VerboseKey -> TTerm -> TCM Doc
forall a. Pretty a => VerboseKey -> a -> TCM Doc
pbody' "[stripped]" ([Bool] -> TTerm -> TTerm
stripUnusedArguments [Bool]
used TTerm
body)
VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "treeless.opt.final" (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
forall a. Pretty a => a -> TCM Doc
pbody TTerm
body
QName -> TTerm -> TCMT IO ()
setTreeless QName
q TTerm
body
QName -> [Bool] -> TCMT IO ()
setCompiledArgUse QName
q [Bool]
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 tag :: VerboseKey
tag v :: VerboseLevel
v name :: VerboseKey
name code :: 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 v :: VerboseLevel
v q :: QName
q =
[Pipeline] -> Pipeline
Sequential
[ VerboseKey
-> VerboseLevel
-> VerboseKey
-> (EvaluationStrategy -> TTerm -> TCMT IO TTerm)
-> Pipeline
compilerPass "simpl" (35 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
v) "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 "builtin" (30 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
v) "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 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 "simpl" (30 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
v) "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 "erase" (30 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
v) "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 "uncase" (30 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
v) "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 "aspat" (30 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
v) "@-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 "id" (30 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
v) "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 eval :: EvaluationStrategy
eval q :: QName
q pipeline :: Pipeline
pipeline t :: TTerm
t = case Pipeline
pipeline of
SinglePass p :: CompilerPass
p -> EvaluationStrategy
-> QName -> CompilerPass -> TTerm -> TCMT IO TTerm
runCompilerPass EvaluationStrategy
eval QName
q CompilerPass
p TTerm
t
Sequential ps :: [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 n :: VerboseLevel
n p :: 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 eval :: EvaluationStrategy
eval q :: QName
q p :: CompilerPass
p t :: TTerm
t = do
TTerm
t' <- CompilerPass -> EvaluationStrategy -> TTerm -> TCMT IO TTerm
passCode CompilerPass
p EvaluationStrategy
eval TTerm
t
let dbg :: (m Doc -> TCM Doc) -> m ()
dbg f :: m Doc -> TCM Doc
f = VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc ("treeless.opt." VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ CompilerPass -> VerboseKey
passTag CompilerPass
p) (CompilerPass -> VerboseLevel
passVerbosity CompilerPass
p) (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ m Doc -> TCM Doc
f (m Doc -> TCM Doc) -> m Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> m Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text ("-- " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ CompilerPass -> VerboseKey
passName CompilerPass
p)
pbody :: a -> TCM Doc
pbody b :: a
b = [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ VerboseKey -> TCM Doc
forall (m :: * -> *). Monad 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
<+> "=", VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ a -> TCM Doc
forall a. Pretty a => a -> TCM Doc
prettyPure a
b ]
(TCM Doc -> TCM Doc) -> TCMT IO ()
forall (m :: * -> *) (m :: * -> *).
(MonadDebug m, Monad m) =>
(m Doc -> TCM Doc) -> m ()
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
<+> "(No effect)")
| Bool
otherwise -> (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
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 n :: VerboseLevel
n eval :: EvaluationStrategy
eval q :: QName
q pipeline :: Pipeline
pipeline = VerboseLevel -> TTerm -> TCMT IO TTerm
go 1
where
go :: VerboseLevel -> TTerm -> TCMT IO TTerm
go i :: VerboseLevel
i t :: 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 "treeless.opt.loop" 20 (VerboseKey -> TCMT IO ()) -> VerboseKey -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ "++ 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]
++ ")"
TTerm -> TCMT IO TTerm
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
go i :: VerboseLevel
i t :: TTerm
t = do
VerboseKey -> VerboseLevel -> VerboseKey -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "treeless.opt.loop" 30 (VerboseKey -> TCMT IO ()) -> VerboseKey -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ "++ 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 "treeless.opt.loop" 30 (VerboseKey -> TCMT IO ()) -> VerboseKey -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ "++ 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]
++ " 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
+ 1) TTerm
t'
closedTermToTreeless :: EvaluationStrategy -> I.Term -> TCM C.TTerm
closedTermToTreeless :: EvaluationStrategy -> Term -> TCMT IO TTerm
closedTermToTreeless eval :: EvaluationStrategy
eval t :: 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 q :: 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
Function{} -> Maybe ExtLamInfo -> Bool
forall a. Maybe a -> Bool
isJust (Defn -> Maybe ExtLamInfo
funExtLam Defn
def) Bool -> Bool -> Bool
|| Maybe QName -> Bool
forall a. Maybe a -> Bool
isJust (Defn -> Maybe QName
funWith Defn
def)
_ -> Bool
False
initCCEnv :: EvaluationStrategy -> CCEnv
initCCEnv :: EvaluationStrategy -> CCEnv
initCCEnv eval :: 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
}
data CCEnv = CCEnv
{ CCEnv -> CCContext
ccCxt :: CCContext
, CCEnv -> Maybe VerboseLevel
ccCatchAll :: Maybe Int
, CCEnv -> EvaluationStrategy
ccEvaluation :: EvaluationStrategy
}
type CCContext = [Int]
type CC = ReaderT CCEnv TCM
shift :: Int -> CCContext -> CCContext
shift :: VerboseLevel -> CCContext -> CCContext
shift n :: 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)
lookupIndex :: Int
-> CCContext
-> Int
lookupIndex :: VerboseLevel -> CCContext -> VerboseLevel
lookupIndex i :: VerboseLevel
i xs :: 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
lookupLevel :: Int
-> CCContext
-> Int
lookupLevel :: VerboseLevel -> CCContext -> VerboseLevel
lookupLevel l :: VerboseLevel
l xs :: 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
- 1 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
l)
casetreeTop :: EvaluationStrategy -> CC.CompiledClauses -> TCM C.TTerm
casetreeTop :: EvaluationStrategy -> CompiledClauses -> TCMT IO TTerm
casetreeTop eval :: EvaluationStrategy
eval cc :: 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 "treeless.convert.arity" 40 (VerboseKey -> TCMT IO ()) -> VerboseKey -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ "-- 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 cc :: CompiledClauses
cc = do
case CompiledClauses
cc of
CC.Fail -> TTerm -> CC TTerm
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
C.tUnreachable
CC.Done xs :: [Arg VerboseKey]
xs v :: 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
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)
Term -> CC TTerm
substTerm Term
v
CC.Case _ (CC.Branches True _ _ _ Just{} _ _) -> CC TTerm
forall a. HasCallStack => a
__IMPOSSIBLE__
CC.Case (Arg _ n :: VerboseLevel
n) (CC.Branches True conBrs :: Map QName (WithArity CompiledClauses)
conBrs _ _ Nothing _ _) -> 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 _ n :: VerboseLevel
n) (CC.Branches False conBrs :: Map QName (WithArity CompiledClauses)
conBrs etaBr :: Maybe (ConHead, WithArity CompiledClauses)
etaBr litBrs :: Map Literal CompiledClauses
litBrs catchAll :: Maybe CompiledClauses
catchAll _ lazy :: Bool
lazy) -> VerboseLevel -> CC TTerm -> CC TTerm
lambdasUpTo (VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ 1) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
forall a b. (a -> b) -> a -> b
$ do
let conBrs' :: Map QName (WithArity CompiledClauses)
conBrs' = Map QName (WithArity CompiledClauses)
-> Map QName (WithArity CompiledClauses)
-> Map QName (WithArity CompiledClauses)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map QName (WithArity CompiledClauses)
conBrs (Map QName (WithArity CompiledClauses)
-> Map QName (WithArity CompiledClauses))
-> Map QName (WithArity CompiledClauses)
-> Map QName (WithArity CompiledClauses)
forall a b. (a -> b) -> a -> b
$ [(QName, WithArity CompiledClauses)]
-> Map QName (WithArity CompiledClauses)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(QName, WithArity CompiledClauses)]
-> Map QName (WithArity CompiledClauses))
-> [(QName, WithArity CompiledClauses)]
-> Map QName (WithArity CompiledClauses)
forall a b. (a -> b) -> a -> b
$ ((ConHead, WithArity CompiledClauses)
-> (QName, WithArity CompiledClauses))
-> [(ConHead, WithArity CompiledClauses)]
-> [(QName, WithArity CompiledClauses)]
forall a b. (a -> b) -> [a] -> [b]
map ((ConHead -> QName)
-> (ConHead, WithArity CompiledClauses)
-> (QName, WithArity CompiledClauses)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ConHead -> QName
conName) ([(ConHead, WithArity CompiledClauses)]
-> [(QName, WithArity CompiledClauses)])
-> [(ConHead, WithArity CompiledClauses)]
-> [(QName, WithArity CompiledClauses)]
forall a b. (a -> b) -> a -> b
$ Maybe (ConHead, WithArity CompiledClauses)
-> [(ConHead, WithArity CompiledClauses)]
forall a. Maybe a -> [a]
maybeToList Maybe (ConHead, WithArity CompiledClauses)
etaBr
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
Maybe CompiledClauses -> CC TTerm -> CC TTerm
updateCatchAll Maybe CompiledClauses
catchAll CC TTerm
fromCatchAll
else do
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
((c :: QName
c:_), []) -> do
QName
c' <- TCM QName -> ReaderT CCEnv TCM QName
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (QName -> TCM QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
c)
QName
dtNm <- Defn -> QName
conData (Defn -> QName) -> (Definition -> Defn) -> Definition -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> QName)
-> ReaderT CCEnv TCM Definition -> ReaderT CCEnv TCM QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Definition -> ReaderT CCEnv TCM Definition
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c')
CaseType -> ReaderT CCEnv TCM CaseType
forall (m :: * -> *) a. Monad m => a -> m a
return (CaseType -> ReaderT CCEnv TCM CaseType)
-> CaseType -> ReaderT CCEnv TCM CaseType
forall a b. (a -> b) -> a -> b
$ QName -> CaseType
C.CTData QName
dtNm
([], (LitChar _ _):_) -> CaseType -> ReaderT CCEnv TCM CaseType
forall (m :: * -> *) a. Monad m => a -> m a
return CaseType
C.CTChar
([], (LitString _ _):_) -> CaseType -> ReaderT CCEnv TCM CaseType
forall (m :: * -> *) a. Monad m => a -> m a
return CaseType
C.CTString
([], (LitFloat _ _):_) -> CaseType -> ReaderT CCEnv TCM CaseType
forall (m :: * -> *) a. Monad m => a -> m a
return CaseType
C.CTFloat
([], (LitQName _ _):_) -> CaseType -> ReaderT CCEnv TCM CaseType
forall (m :: * -> *) a. Monad m => a -> m a
return CaseType
C.CTQName
_ -> 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 <- VerboseLevel -> CCContext -> VerboseLevel
lookupLevel VerboseLevel
n (CCContext -> VerboseLevel)
-> ReaderT CCEnv TCM CCContext -> ReaderT CCEnv TCM VerboseLevel
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
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
fromCatchAll :: CC C.TTerm
fromCatchAll :: CC TTerm
fromCatchAll = 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)
-> ReaderT CCEnv TCM (Maybe VerboseLevel) -> CC TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CCEnv -> Maybe VerboseLevel)
-> ReaderT CCEnv TCM (Maybe VerboseLevel)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CCEnv -> Maybe VerboseLevel
ccCatchAll
commonArity :: CC.CompiledClauses -> Int
commonArity :: CompiledClauses -> VerboseLevel
commonArity cc :: CompiledClauses
cc =
case VerboseLevel -> CompiledClauses -> CCContext
forall a. VerboseLevel -> CompiledClauses' a -> CCContext
arities 0 CompiledClauses
cc of
[] -> 0
as :: CCContext
as -> CCContext -> VerboseLevel
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum CCContext
as
where
arities :: VerboseLevel -> CompiledClauses' a -> CCContext
arities cxt :: VerboseLevel
cxt (Case (Arg _ x :: VerboseLevel
x) (Branches False cons :: Map QName (WithArity (CompiledClauses' a))
cons eta :: Maybe (ConHead, WithArity (CompiledClauses' a))
eta lits :: Map Literal (CompiledClauses' a)
lits def :: Maybe (CompiledClauses' a)
def _ _)) =
(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]
++
(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') (((ConHead, WithArity (CompiledClauses' a))
-> WithArity (CompiledClauses' a))
-> [(ConHead, WithArity (CompiledClauses' a))]
-> [WithArity (CompiledClauses' a)]
forall a b. (a -> b) -> [a] -> [b]
map (ConHead, WithArity (CompiledClauses' a))
-> WithArity (CompiledClauses' a)
forall a b. (a, b) -> b
snd ([(ConHead, WithArity (CompiledClauses' a))]
-> [WithArity (CompiledClauses' a)])
-> [(ConHead, WithArity (CompiledClauses' a))]
-> [WithArity (CompiledClauses' a)]
forall a b. (a -> b) -> a -> b
$ 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 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 c :: 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
+ 1) VerboseLevel
cxt
arities cxt :: VerboseLevel
cxt (Case _ Branches{projPatterns :: forall c. Case c -> Bool
projPatterns = Bool
True}) = [VerboseLevel
cxt]
arities cxt :: VerboseLevel
cxt (Done xs :: [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)]
arities _ Fail = []
wArities :: VerboseLevel -> WithArity (CompiledClauses' a) -> CCContext
wArities cxt :: VerboseLevel
cxt (WithArity k :: VerboseLevel
k c :: CompiledClauses' a
c) = (VerboseLevel -> VerboseLevel) -> CCContext -> CCContext
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: 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
+ 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
- 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 Nothing cont :: CC TTerm
cont = CC TTerm
cont
updateCatchAll (Just cc :: CompiledClauses
cc) cont :: CC TTerm
cont = do
TTerm
def <- CompiledClauses -> CC TTerm
casetree CompiledClauses
cc
(CCEnv -> CCEnv) -> CC TTerm -> CC TTerm
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\e :: CCEnv
e -> CCEnv
e { ccCatchAll :: Maybe VerboseLevel
ccCatchAll = VerboseLevel -> Maybe VerboseLevel
forall a. a -> Maybe a
Just 0, ccCxt :: CCContext
ccCxt = VerboseLevel -> CCContext -> CCContext
shift 1 (CCEnv -> CCContext
ccCxt CCEnv
e) }) (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
withContextSize :: Int -> CC C.TTerm -> CC C.TTerm
withContextSize :: VerboseLevel -> CC TTerm -> CC TTerm
withContextSize n :: VerboseLevel
n cont :: CC TTerm
cont = do
VerboseLevel
diff <- (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)
-> ReaderT CCEnv TCM CCContext -> ReaderT CCEnv TCM VerboseLevel
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
if VerboseLevel
diff VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= 0
then do
let diff' :: VerboseLevel
diff' = -VerboseLevel
diff
(CCEnv -> CCEnv) -> CC TTerm -> CC TTerm
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\e :: CCEnv
e -> CCEnv
e { ccCxt :: CCContext
ccCxt = VerboseLevel -> CCContext -> CCContext
shift VerboseLevel
diff (CCContext -> CCContext)
-> (CCContext -> CCContext) -> CCContext -> CCContext
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> CCContext -> CCContext
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
diff' (CCContext -> CCContext) -> CCContext -> CCContext
forall a b. (a -> b) -> a -> b
$ CCEnv -> CCContext
ccCxt CCEnv
e }) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
forall a b. (a -> b) -> a -> b
$
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'))
else do
(CCEnv -> CCEnv) -> CC TTerm -> CC TTerm
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\e :: CCEnv
e -> CCEnv
e { ccCxt :: CCContext
ccCxt = [0..(VerboseLevel
diff VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- 1)] CCContext -> CCContext -> CCContext
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> CCContext -> CCContext
shift VerboseLevel
diff (CCEnv -> CCContext
ccCxt CCEnv
e)}) (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
forall a b. (a -> b) -> a -> b
$ do
VerboseLevel -> TTerm -> TTerm
createLambdas VerboseLevel
diff (TTerm -> TTerm) -> CC TTerm -> CC TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
CC TTerm
cont
where createLambdas :: Int -> C.TTerm -> C.TTerm
createLambdas :: VerboseLevel -> TTerm -> TTerm
createLambdas 0 cont' :: TTerm
cont' = TTerm
cont'
createLambdas i :: VerboseLevel
i cont' :: TTerm
cont' | VerboseLevel
i VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> 0 = TTerm -> TTerm
C.TLam (VerboseLevel -> TTerm -> TTerm
createLambdas (VerboseLevel
i VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- 1) TTerm
cont')
createLambdas _ _ = TTerm
forall a. HasCallStack => a
__IMPOSSIBLE__
lambdasUpTo :: Int -> CC C.TTerm -> CC C.TTerm
lambdasUpTo :: VerboseLevel -> CC TTerm -> CC TTerm
lambdasUpTo n :: VerboseLevel
n cont :: CC TTerm
cont = do
VerboseLevel
diff <- (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)
-> ReaderT CCEnv TCM CCContext -> ReaderT CCEnv TCM VerboseLevel
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
if VerboseLevel
diff VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= 0 then CC TTerm
cont
else do
Maybe VerboseLevel
catchAll <- (CCEnv -> Maybe VerboseLevel)
-> ReaderT CCEnv TCM (Maybe VerboseLevel)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CCEnv -> Maybe VerboseLevel
ccCatchAll
VerboseLevel -> CC TTerm -> CC TTerm
withContextSize VerboseLevel
n (CC TTerm -> CC TTerm) -> CC TTerm -> CC TTerm
forall a b. (a -> b) -> a -> b
$ do
case Maybe VerboseLevel
catchAll of
Just catchAll' :: VerboseLevel
catchAll' -> do
(CCEnv -> CCEnv) -> CC TTerm -> CC TTerm
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\e :: CCEnv
e -> CCEnv
e { ccCatchAll :: Maybe VerboseLevel
ccCatchAll = VerboseLevel -> Maybe VerboseLevel
forall a. a -> Maybe a
Just 0
, ccCxt :: CCContext
ccCxt = VerboseLevel -> CCContext -> CCContext
shift 1 (CCEnv -> CCContext
ccCxt CCEnv
e)}) (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
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 x :: VerboseLevel
x br :: 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
$ \ (c :: QName
c, CC.WithArity n :: VerboseLevel
n cc :: 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 x :: VerboseLevel
x br :: 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
$ \ (l :: Literal
l, cc :: CompiledClauses
cc) ->
VerboseLevel
-> VerboseLevel -> ReaderT CCEnv TCM TAlt -> ReaderT CCEnv TCM TAlt
forall a. VerboseLevel -> VerboseLevel -> CC a -> CC a
replaceVar VerboseLevel
x 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 alt :: TTerm -> TAlt
alt cc :: 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
replaceVar :: Int -> Int -> CC a -> CC a
replaceVar :: VerboseLevel -> VerboseLevel -> CC a -> CC a
replaceVar x :: VerboseLevel
x n :: VerboseLevel
n cont :: CC a
cont = do
let upd :: CCContext -> CCContext
upd cxt :: 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
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
- 1 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
x
(ys :: CCContext
ys, _:zs :: CCContext
zs) = VerboseLevel -> CCContext -> (CCContext, CCContext)
forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt VerboseLevel
i CCContext
cxt
ixs :: CCContext
ixs = [0..(VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- 1)]
(CCEnv -> CCEnv) -> CC a -> CC a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\e :: 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
mkRecord :: Map QName C.TTerm -> CC C.TTerm
mkRecord :: Map QName TTerm -> CC TTerm
mkRecord fs :: 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
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
I.ConHead c :: QName
c _ind :: Induction
_ind xs :: [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 "treeless.convert.mkRecord" 60 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
[ VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text "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 :: * -> *). Monad 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 :: * -> *). Monad m => VerboseKey -> m Doc
text "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 :: * -> *). Monad 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)
]
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
$ \ x :: 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 q :: 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
$ \ proj :: Projection
proj -> do
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
substTerm :: I.Term -> CC C.TTerm
substTerm :: Term -> CC TTerm
substTerm term :: 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
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 ind :: VerboseLevel
ind es :: Elims
es -> do
VerboseLevel
ind' <- VerboseLevel -> CCContext -> VerboseLevel
lookupIndex VerboseLevel
ind (CCContext -> VerboseLevel)
-> ReaderT CCEnv TCM CCContext -> ReaderT CCEnv TCM VerboseLevel
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
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 _ ab :: 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 (\e :: CCEnv
e -> CCEnv
e { ccCxt :: CCContext
ccCxt = 0 VerboseLevel -> CCContext -> CCContext
forall a. a -> [a] -> [a]
: (VerboseLevel -> CCContext -> CCContext
shift 1 (CCContext -> CCContext) -> CCContext -> CCContext
forall a b. (a -> b) -> a -> b
$ 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 l :: 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 _ -> TTerm -> CC TTerm
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
C.TUnit
I.Def q :: QName
q es :: 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 c :: ConHead
c ci :: ConInfo
ci es :: 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 _ _ -> TTerm -> CC TTerm
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
C.TUnit
I.Sort _ -> TTerm -> CC TTerm
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
C.TSort
I.MetaV _ _ -> CC TTerm
forall a. HasCallStack => a
__IMPOSSIBLE__
I.DontCare _ -> TTerm -> CC TTerm
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
C.TErased
I.Dummy{} -> CC TTerm
forall a. HasCallStack => a
__IMPOSSIBLE__
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
etaErasedOnce :: Term -> Either Term Term
etaErasedOnce t :: Term
t =
case Term
t of
I.Lam _ (NoAbs _ v :: Term
v) ->
case Term -> BinAppView
binAppView Term
v of
App u :: Term
u arg :: 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
_ -> Either Term Term
forall b. Either Term b
done
I.Lam ai :: ArgInfo
ai (Abs _ v :: Term
v) | Bool -> Bool
not (ArgInfo -> Bool
forall a. LensModality a => a -> Bool
usableModality ArgInfo
ai) ->
case Term -> BinAppView
binAppView Term
v of
App u :: Term
u arg :: 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 -> Term -> Term -> Term
forall t a. Subst t a => VerboseLevel -> t -> a -> a
subst 0 (Term -> Term
DontCare Term
HasCallStack => Term
__DUMMY_TERM__) Term
u
_ -> Either Term Term
forall b. Either Term b
done
_ -> Either Term Term
forall b. Either Term b
done
where
done :: Either Term b
done = Term -> Either Term b
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 f :: QName
f es :: 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 v :: 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 q :: QName
q vs :: [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
[Bool]
used <- TCM [Bool] -> ReaderT CCEnv TCM [Bool]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM [Bool] -> ReaderT CCEnv TCM [Bool])
-> TCM [Bool] -> ReaderT CCEnv TCM [Bool]
forall a b. (a -> b) -> a -> b
$ QName -> TCM [Bool]
getCompiledArgUse QName
q
let substUsed :: Bool -> Arg Term -> CC TTerm
substUsed False _ = TTerm -> CC TTerm
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
C.TErased
substUsed True arg :: Arg Term
arg = 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
<$> [CC TTerm] -> ReaderT CCEnv TCM Args
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ Bool -> Arg Term -> CC TTerm
substUsed Bool
u Arg Term
arg | (arg :: Arg Term
arg, u :: Bool
u) <- [Arg Term] -> [Bool] -> [(Arg Term, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Arg Term]
vs ([Bool] -> [(Arg Term, Bool)]) -> [Bool] -> [(Arg Term, Bool)]
forall a b. (a -> b) -> a -> b
$ [Bool]
used [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Bool -> [Bool]
forall a. a -> [a]
repeat Bool
True ]
_ -> 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 eval :: 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 eval :: EvaluationStrategy
eval q :: 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 x :: 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