1 2module Agda.Compiler.ToTreeless 3 ( toTreeless 4 , closedTermToTreeless 5 ) where 6 7import Control.Arrow (first) 8import Control.Monad.Reader 9 10import Data.Maybe 11import Data.Map (Map) 12import qualified Data.Map as Map 13import qualified Data.List as List 14 15import Agda.Syntax.Common 16import Agda.Syntax.Internal as I 17import Agda.Syntax.Literal 18import qualified Agda.Syntax.Treeless as C 19import Agda.Syntax.Treeless (TTerm, EvaluationStrategy, ArgUsage(..)) 20 21import Agda.TypeChecking.CompiledClause as CC 22import qualified Agda.TypeChecking.CompiledClause.Compile as CC 23import Agda.TypeChecking.EtaContract (binAppView, BinAppView(..)) 24import Agda.TypeChecking.Monad as TCM 25import Agda.TypeChecking.Pretty 26import Agda.TypeChecking.Records (getRecordConstructor) 27import Agda.TypeChecking.Reduce 28import Agda.TypeChecking.Substitute 29 30import Agda.Compiler.Treeless.AsPatterns 31import Agda.Compiler.Treeless.Builtin 32import Agda.Compiler.Treeless.Erase 33import Agda.Compiler.Treeless.Identity 34import Agda.Compiler.Treeless.Simplify 35import Agda.Compiler.Treeless.Uncase 36import Agda.Compiler.Treeless.Unused 37 38import Agda.Utils.Function 39import Agda.Utils.Functor 40import Agda.Utils.Lens 41import Agda.Utils.List 42import Agda.Utils.Maybe 43import Agda.Utils.Monad 44import Agda.Utils.Pretty (prettyShow) 45import qualified Agda.Utils.Pretty as P 46import qualified Agda.Utils.SmallSet as SmallSet 47 48import Agda.Utils.Impossible 49 50prettyPure :: P.Pretty a => a -> TCM Doc 51prettyPure = return . P.pretty 52 53-- | Recompile clauses with forcing translation turned on. 54getCompiledClauses :: QName -> TCM CC.CompiledClauses 55getCompiledClauses q = do 56 def <- getConstInfo q 57 let cs = defClauses def 58 isProj | Function{ funProjection = proj } <- theDef def = isJust (projProper =<< proj) 59 | otherwise = False 60 translate | isProj = CC.DontRunRecordPatternTranslation 61 | otherwise = CC.RunRecordPatternTranslation 62 reportSDoc "treeless.convert" 40 $ "-- before clause compiler" $$ (pretty q <+> "=") <?> vcat (map pretty cs) 63 let mst = funSplitTree $ theDef def 64 reportSDoc "treeless.convert" 70 $ 65 caseMaybe mst "-- not using split tree" $ \st -> 66 "-- using split tree" $$ pretty st 67 CC.compileClauses' translate cs mst 68 69-- | Converts compiled clauses to treeless syntax. 70-- 71-- Note: Do not use any of the concrete names in the returned 72-- term for identification purposes! If you wish to do so, 73-- first apply the Agda.Compiler.Treeless.NormalizeNames 74-- transformation. 75toTreeless :: EvaluationStrategy -> QName -> TCM (Maybe C.TTerm) 76toTreeless eval q = ifM (alwaysInline q) (pure Nothing) $ Just <$> toTreeless' eval q 77 78toTreeless' :: EvaluationStrategy -> QName -> TCM C.TTerm 79toTreeless' eval q = 80 flip fromMaybeM (getTreeless q) $ verboseBracket "treeless.convert" 20 ("compiling " ++ prettyShow q) $ do 81 cc <- getCompiledClauses q 82 unlessM (alwaysInline q) $ setTreeless q (C.TDef q) 83 -- so recursive inlining doesn't loop, but not for always inlined 84 -- functions, since that would risk inlining to fail. 85 ccToTreeless eval q cc 86 87-- | Does not require the name to refer to a function. 88cacheTreeless :: EvaluationStrategy -> QName -> TCM () 89cacheTreeless eval q = do 90 def <- theDef <$> getConstInfo q 91 case def of 92 Function{} -> () <$ toTreeless' eval q 93 _ -> return () 94 95ccToTreeless :: EvaluationStrategy -> QName -> CC.CompiledClauses -> TCM C.TTerm 96ccToTreeless eval q cc = do 97 let pbody b = pbody' "" b 98 pbody' suf b = sep [ text (prettyShow q ++ suf) <+> "=", nest 2 $ prettyPure b ] 99 v <- ifM (alwaysInline q) (return 20) (return 0) 100 reportSDoc "treeless.convert" (30 + v) $ "-- compiled clauses of" <+> prettyTCM q $$ nest 2 (prettyPure cc) 101 body <- casetreeTop eval cc 102 reportSDoc "treeless.opt.converted" (30 + v) $ "-- converted" $$ pbody body 103 body <- runPipeline eval q (compilerPipeline v q) body 104 used <- usedArguments q body 105 when (ArgUnused `elem` used) $ 106 reportSDoc "treeless.opt.unused" (30 + v) $ 107 "-- used args:" <+> hsep [ if u == ArgUsed then text [x] else "_" | (x, u) <- zip ['a'..] used ] $$ 108 pbody' "[stripped]" (stripUnusedArguments used body) 109 reportSDoc "treeless.opt.final" (20 + v) $ pbody body 110 setTreeless q body 111 setCompiledArgUse q used 112 return body 113 114data Pipeline = FixedPoint Int Pipeline 115 | Sequential [Pipeline] 116 | SinglePass CompilerPass 117 118data CompilerPass = CompilerPass 119 { passTag :: String 120 , passVerbosity :: Int 121 , passName :: String 122 , passCode :: EvaluationStrategy -> TTerm -> TCM TTerm 123 } 124 125compilerPass :: String -> Int -> String -> (EvaluationStrategy -> TTerm -> TCM TTerm) -> Pipeline 126compilerPass tag v name code = SinglePass (CompilerPass tag v name code) 127 128compilerPipeline :: Int -> QName -> Pipeline 129compilerPipeline v q = 130 Sequential 131 -- Issue #4967: No simplification step before builtin translation! Simplification relies 132 -- on either all or no builtins being translated. Since we might have inlined 133 -- functions that have had the builtin translation applied, we need to apply it 134 -- first. 135 -- [ compilerPass "simpl" (35 + v) "simplification" $ const simplifyTTerm 136 [ compilerPass "builtin" (30 + v) "builtin translation" $ const translateBuiltins 137 , FixedPoint 5 $ Sequential 138 [ compilerPass "simpl" (30 + v) "simplification" $ const simplifyTTerm 139 , compilerPass "erase" (30 + v) "erasure" $ eraseTerms q 140 , compilerPass "uncase" (30 + v) "uncase" $ const caseToSeq 141 , compilerPass "aspat" (30 + v) "@-pattern recovery" $ const recoverAsPatterns 142 ] 143 , compilerPass "id" (30 + v) "identity function detection" $ const (detectIdentityFunctions q) 144 ] 145 146runPipeline :: EvaluationStrategy -> QName -> Pipeline -> TTerm -> TCM TTerm 147runPipeline eval q pipeline t = case pipeline of 148 SinglePass p -> runCompilerPass eval q p t 149 Sequential ps -> foldM (flip $ runPipeline eval q) t ps 150 FixedPoint n p -> runFixedPoint n eval q p t 151 152runCompilerPass :: EvaluationStrategy -> QName -> CompilerPass -> TTerm -> TCM TTerm 153runCompilerPass eval q p t = do 154 t' <- passCode p eval t 155 let dbg f = reportSDoc ("treeless.opt." ++ passTag p) (passVerbosity p) $ f $ text ("-- " ++ passName p) 156 pbody b = sep [ text (prettyShow q) <+> "=", nest 2 $ prettyPure b ] 157 dbg $ if | t == t' -> (<+> "(No effect)") 158 | otherwise -> ($$ pbody t') 159 return t' 160 161runFixedPoint :: Int -> EvaluationStrategy -> QName -> Pipeline -> TTerm -> TCM TTerm 162runFixedPoint n eval q pipeline = go 1 163 where 164 go i t | i > n = do 165 reportSLn "treeless.opt.loop" 20 $ "++ Optimisation loop reached maximum iterations (" ++ show n ++ ")" 166 return t 167 go i t = do 168 reportSLn "treeless.opt.loop" 30 $ "++ Optimisation loop iteration " ++ show i 169 t' <- runPipeline eval q pipeline t 170 if | t == t' -> do 171 reportSLn "treeless.opt.loop" 30 $ "++ Optimisation loop terminating after " ++ show i ++ " iterations" 172 return t' 173 | otherwise -> go (i + 1) t' 174 175closedTermToTreeless :: EvaluationStrategy -> I.Term -> TCM C.TTerm 176closedTermToTreeless eval t = do 177 substTerm t `runReaderT` initCCEnv eval 178 179alwaysInline :: QName -> TCM Bool 180alwaysInline q = do 181 def <- theDef <$> getConstInfo q 182 pure $ case def of -- always inline with functions and pattern lambdas 183 Function{funClauses = cs} -> (isJust (funExtLam def) && not recursive) || isJust (funWith def) 184 where 185 recursive = any (fromMaybe True . clauseRecursive) cs 186 _ -> False 187 188-- | Initial environment for expression generation. 189initCCEnv :: EvaluationStrategy -> CCEnv 190initCCEnv eval = CCEnv 191 { ccCxt = [] 192 , ccCatchAll = Nothing 193 , ccEvaluation = eval 194 } 195 196-- | Environment for naming of local variables. 197data CCEnv = CCEnv 198 { ccCxt :: CCContext -- ^ Maps case tree de-bruijn indices to TTerm de-bruijn indices 199 , ccCatchAll :: Maybe Int -- ^ TTerm de-bruijn index of the current catch all 200 -- If an inner case has no catch-all clause, we use the one from its parent. 201 , ccEvaluation :: EvaluationStrategy 202 } 203 204type CCContext = [Int] 205type CC = ReaderT CCEnv TCM 206 207shift :: Int -> CCContext -> CCContext 208shift n = map (+n) 209 210-- | Term variables are de Bruijn indices. 211lookupIndex :: Int -- ^ Case tree de bruijn index. 212 -> CCContext 213 -> Int -- ^ TTerm de bruijn index. 214lookupIndex i xs = fromMaybe __IMPOSSIBLE__ $ xs !!! i 215 216-- | Case variables are de Bruijn levels. 217lookupLevel :: Int -- ^ case tree de bruijn level 218 -> CCContext 219 -> Int -- ^ TTerm de bruijn index 220lookupLevel l xs = fromMaybe __IMPOSSIBLE__ $ xs !!! (length xs - 1 - l) 221 222-- | Compile a case tree into nested case and record expressions. 223casetreeTop :: EvaluationStrategy -> CC.CompiledClauses -> TCM C.TTerm 224casetreeTop eval cc = flip runReaderT (initCCEnv eval) $ do 225 let a = commonArity cc 226 lift $ reportSLn "treeless.convert.arity" 40 $ "-- common arity: " ++ show a 227 lambdasUpTo a $ casetree cc 228 229casetree :: CC.CompiledClauses -> CC C.TTerm 230casetree cc = do 231 case cc of 232 CC.Fail xs -> withContextSize (length xs) $ return C.tUnreachable 233 CC.Done xs v -> withContextSize (length xs) $ do 234 -- Issue 2469: Body context size (`length xs`) may be smaller than current context size 235 -- if some arguments are not used in the body. 236 v <- lift (putAllowedReductions (SmallSet.fromList [ProjectionReductions, CopatternReductions]) $ normalise v) 237 cxt <- asks ccCxt 238 v' <- substTerm v 239 reportS "treeless.convert.casetree" 40 $ 240 [ "-- casetree, calling substTerm:" 241 , "-- cxt =" <+> prettyPure cxt 242 , "-- v =" <+> prettyPure v 243 , "-- v' =" <+> prettyPure v' 244 ] 245 return v' 246 CC.Case _ (CC.Branches True _ _ _ Just{} _ _) -> __IMPOSSIBLE__ 247 -- Andreas, 2016-06-03, issue #1986: Ulf: "no catch-all for copatterns!" 248 -- lift $ do 249 -- typeError . GenericDocError =<< do 250 -- "Not yet implemented: compilation of copattern matching with catch-all clause" 251 CC.Case (Arg _ n) (CC.Branches True conBrs _ _ Nothing _ _) -> lambdasUpTo n $ do 252 mkRecord =<< traverse casetree (CC.content <$> conBrs) 253 CC.Case (Arg i n) (CC.Branches False conBrs etaBr litBrs catchAll _ lazy) -> lambdasUpTo (n + 1) $ do 254 -- We can treat eta-matches as regular matches here. 255 let conBrs' = Map.union conBrs $ Map.fromList $ map (first conName) $ maybeToList etaBr 256 if Map.null conBrs' && Map.null litBrs then do 257 -- there are no branches, just return default 258 updateCatchAll catchAll fromCatchAll 259 else do 260 -- Get the type of the scrutinee. 261 caseTy <- 262 case (Map.keys conBrs', Map.keys litBrs) of 263 (cs, []) -> lift $ go cs 264 where 265 go (c:cs) = canonicalName c >>= getConstInfo <&> theDef >>= \case 266 Constructor{conData} -> 267 return $ C.CTData (getQuantity i) conData 268 _ -> go cs 269 go [] = __IMPOSSIBLE__ 270 ([], LitChar _ : _) -> return C.CTChar 271 ([], LitString _ : _) -> return C.CTString 272 ([], LitFloat _ : _) -> return C.CTFloat 273 ([], LitQName _ : _) -> return C.CTQName 274 _ -> __IMPOSSIBLE__ 275 276 updateCatchAll catchAll $ do 277 x <- asks (lookupLevel n . ccCxt) 278 def <- fromCatchAll 279 let caseInfo = C.CaseInfo { caseType = caseTy, caseLazy = lazy } 280 C.TCase x caseInfo def <$> do 281 br1 <- conAlts n conBrs' 282 br2 <- litAlts n litBrs 283 return (br1 ++ br2) 284 where 285 -- normally, Agda should make sure that a pattern match is total, 286 -- so we set the default to unreachable if no default has been provided. 287 fromCatchAll :: CC C.TTerm 288 fromCatchAll = asks (maybe C.tUnreachable C.TVar . ccCatchAll) 289 290commonArity :: CC.CompiledClauses -> Int 291commonArity cc = 292 case arities 0 cc of 293 [] -> 0 294 as -> minimum as 295 where 296 arities cxt (Case (Arg _ x) (Branches False cons eta lits def _ _)) = 297 concatMap (wArities cxt') (Map.elems cons) ++ 298 concatMap ((wArities cxt') . snd) (maybeToList eta) ++ 299 concatMap (wArities cxt' . WithArity 0) (Map.elems lits) ++ 300 concat [ arities cxt' c | Just c <- [def] ] -- ?? 301 where cxt' = max (x + 1) cxt 302 arities cxt (Case _ Branches{projPatterns = True}) = [cxt] 303 arities cxt (Done xs _) = [max cxt (length xs)] 304 arities cxt (Fail xs) = [max cxt (length xs)] 305 306 307 wArities cxt (WithArity k c) = map (\ x -> x - k + 1) $ arities (cxt - 1 + k) c 308 309updateCatchAll :: Maybe CC.CompiledClauses -> (CC C.TTerm -> CC C.TTerm) 310updateCatchAll Nothing cont = cont 311updateCatchAll (Just cc) cont = do 312 def <- casetree cc 313 cxt <- asks ccCxt 314 reportS "treeless.convert.lambdas" 40 $ 315 [ "-- updateCatchAll:" 316 , "-- cxt =" <+> prettyPure cxt 317 , "-- def =" <+> prettyPure def 318 ] 319 local (\ e -> e { ccCatchAll = Just 0, ccCxt = shift 1 cxt }) $ do 320 C.mkLet def <$> cont 321 322-- | Shrinks or grows the context to the given size. 323-- Does not update the catchAll expression, the catchAll expression 324-- MUST NOT be used inside `cont`. 325withContextSize :: Int -> CC C.TTerm -> CC C.TTerm 326withContextSize n cont = do 327 diff <- asks (((n -) . length) . ccCxt) 328 if diff >= 1 then createLambdas diff cont else do 329 let diff' = -diff 330 cxt <- -- shift diff . 331 -- Andreas, 2021-04-10, issue #5288 332 -- The @shift diff@ is wrong, since we are returning to the original 333 -- context from @cont@, and then we would have to reverse 334 -- the effect of @shift diff@. 335 -- We need to make sure that the result of @cont@ make sense 336 -- in the **present** context, not the changed context 337 -- where it is constructed. 338 -- 339 -- Ulf, 2021-04-12, https://github.com/agda/agda/pull/5311/files#r611452551 340 -- 341 -- This looks correct, but I can't quite follow the explanation. Here's my understanding: 342 -- 343 -- We are building a `TTerm` case tree from `CompiledClauses`. In order 344 -- to be able to match we bind all variables we'll need in a top-level 345 -- lambda `λ a b c d → ..` (say). As we compute the `TTerm` we keep a 346 -- context (list) of `TTerm` deBruijn indices for each `CompiledClause` 347 -- variable. This is a renaming from the *source* context of the 348 -- `CompiledClause` to the *target* context of the `TTerm`. 349 -- 350 -- After some pattern matching we might have 351 -- ``` 352 -- λ a b c d → 353 -- case c of 354 -- e :: f → {cxt = [d, f, e, b, a]} 355 -- ``` 356 -- Now, what's causing the problems here is that `CompiledClauses` can be 357 -- underapplied, so you might have matched on a variable only to find 358 -- that in the catch-all the variable you matched on is bound in a lambda 359 -- in the right-hand side! Extending the example, we might have 360 -- `CompiledClauses` looking like this: 361 -- ``` 362 -- case 2 of 363 -- _::_ → done[d, f, e, b, a] ... 364 -- _ → done[b, a] (λ c d → ...) 365 -- ``` 366 -- When we get to the catch-all, the context will be `[d, c, b, a]` but 367 -- the right-hand side is only expecting `a` and `b` to be bound. What we 368 -- need to do is compile the right-hand side and then apply it to the 369 -- variables `c` and `d` that we already bound. This is what 370 -- `withContextSize` does. 371 -- 372 -- Crucially (and this is where the bug was), we are not changing the 373 -- target context, only the source context (we want a `TTerm` that makes 374 -- sense at this point). This means that the correct move is to drop the 375 -- entries for the additional source variables, but not change what 376 -- target variables the remaining source variables map to. Hence, `drop` 377 -- but no `shift`. 378 -- 379 drop diff' <$> asks ccCxt 380 local (\ e -> e { ccCxt = cxt }) $ do 381 reportS "treeless.convert.lambdas" 40 $ 382 [ "-- withContextSize:" 383 , "-- n =" <+> prettyPure n 384 , "-- diff=" <+> prettyPure diff 385 , "-- cxt =" <+> prettyPure cxt 386 ] 387 cont <&> (`C.mkTApp` map C.TVar (downFrom diff')) 388 389-- | Prepend the given positive number of lambdas. 390-- Does not update the catchAll expression, 391-- the catchAll expression must be updated separately (or not be used). 392createLambdas :: Int -> CC C.TTerm -> CC C.TTerm 393createLambdas diff cont = do 394 unless (diff >= 1) __IMPOSSIBLE__ 395 cxt <- ([0 .. diff-1] ++) . shift diff <$> asks ccCxt 396 local (\ e -> e { ccCxt = cxt }) $ do 397 reportS "treeless.convert.lambdas" 40 $ 398 [ "-- createLambdas:" 399 , "-- diff =" <+> prettyPure diff 400 , "-- cxt =" <+> prettyPure cxt 401 ] 402 -- Prepend diff lambdas 403 cont <&> \ t -> List.iterate C.TLam t !! diff 404 405-- | Adds lambdas until the context has at least the given size. 406-- Updates the catchAll expression to take the additional lambdas into account. 407lambdasUpTo :: Int -> CC C.TTerm -> CC C.TTerm 408lambdasUpTo n cont = do 409 diff <- asks (((n -) . length) . ccCxt) 410 411 if diff <= 0 then cont -- no new lambdas needed 412 else do 413 createLambdas diff $ do 414 asks ccCatchAll >>= \case 415 Just catchAll -> do 416 cxt <- asks ccCxt 417 reportS "treeless.convert.lambdas" 40 $ 418 [ "lambdasUpTo: n =" <+> (text . show) n 419 , " diff =" <+> (text . show) n 420 , " catchAll =" <+> prettyPure catchAll 421 , " ccCxt =" <+> prettyPure cxt 422 ] 423 -- the catch all doesn't know about the additional lambdas, so just directly 424 -- apply it again to the newly introduced lambda arguments. 425 -- we also bind the catch all to a let, to avoid code duplication 426 local (\e -> e { ccCatchAll = Just 0 427 , ccCxt = shift 1 cxt }) $ do 428 let catchAllArgs = map C.TVar $ downFrom diff 429 C.mkLet (C.mkTApp (C.TVar $ catchAll + diff) catchAllArgs) 430 <$> cont 431 Nothing -> cont 432 433conAlts :: Int -> Map QName (CC.WithArity CC.CompiledClauses) -> CC [C.TAlt] 434conAlts x br = forM (Map.toList br) $ \ (c, CC.WithArity n cc) -> do 435 c' <- lift $ canonicalName c 436 replaceVar x n $ do 437 branch (C.TACon c' n) cc 438 439litAlts :: Int -> Map Literal CC.CompiledClauses -> CC [C.TAlt] 440litAlts x br = forM (Map.toList br) $ \ (l, cc) -> 441 -- Issue1624: we need to drop the case scrutinee from the environment here! 442 replaceVar x 0 $ do 443 branch (C.TALit l ) cc 444 445branch :: (C.TTerm -> C.TAlt) -> CC.CompiledClauses -> CC C.TAlt 446branch alt cc = alt <$> casetree cc 447 448-- | Replace de Bruijn Level @x@ by @n@ new variables. 449replaceVar :: Int -> Int -> CC a -> CC a 450replaceVar x n cont = do 451 let upd cxt = shift n ys ++ ixs ++ shift n zs 452 where 453 -- compute the de Bruijn index 454 i = length cxt - 1 - x 455 -- discard index i 456 (ys, _:zs) = splitAt i cxt 457 -- compute the de-bruijn indexes of the newly inserted variables 458 ixs = [0..(n - 1)] 459 local (\e -> e { ccCxt = upd (ccCxt e) , ccCatchAll = (+n) <$> ccCatchAll e }) $ 460 cont 461 462 463-- | Precondition: Map not empty. 464mkRecord :: Map QName C.TTerm -> CC C.TTerm 465mkRecord fs = lift $ do 466 -- Get the name of the first field 467 let p1 = fst $ headWithDefault __IMPOSSIBLE__ $ Map.toList fs 468 -- Use the field name to get the record constructor and the field names. 469 I.ConHead c IsRecord{} _ind xs <- conSrcCon . theDef <$> (getConstInfo =<< canonicalName . I.conName =<< recConFromProj p1) 470 reportSDoc "treeless.convert.mkRecord" 60 $ vcat 471 [ text "record constructor fields: xs = " <+> (text . show) xs 472 , text "to be filled with content: keys fs = " <+> (text . show) (Map.keys fs) 473 ] 474 -- Convert the constructor 475 let (args :: [C.TTerm]) = for xs $ \ x -> Map.findWithDefault __IMPOSSIBLE__ (unArg x) fs 476 return $ C.mkTApp (C.TCon c) args 477 478 479recConFromProj :: QName -> TCM I.ConHead 480recConFromProj q = do 481 caseMaybeM (isProjection q) __IMPOSSIBLE__ $ \ proj -> do 482 let d = unArg $ projFromType proj 483 getRecordConstructor d 484 485 486-- | Translate the actual Agda terms, with an environment of all the bound variables 487-- from patternmatching. Agda terms are in de Bruijn indices, but the expected 488-- TTerm de bruijn indexes may differ. This is due to additional let-bindings 489-- introduced by the catch-all machinery, so we need to lookup casetree de bruijn 490-- indices in the environment as well. 491substTerm :: I.Term -> CC C.TTerm 492substTerm term = normaliseStatic term >>= \ term -> 493 case I.unSpine $ etaContractErased term of 494 I.Var ind es -> do 495 ind' <- asks (lookupIndex ind . ccCxt) 496 let args = fromMaybe __IMPOSSIBLE__ $ I.allApplyElims es 497 C.mkTApp (C.TVar ind') <$> substArgs args 498 I.Lam _ ab -> 499 C.TLam <$> 500 local (\e -> e { ccCxt = 0 : shift 1 (ccCxt e) }) 501 (substTerm $ I.unAbs ab) 502 I.Lit l -> return $ C.TLit l 503 I.Level _ -> return C.TUnit 504 I.Def q es -> do 505 let args = fromMaybe __IMPOSSIBLE__ $ I.allApplyElims es 506 maybeInlineDef q args 507 I.Con c ci es -> do 508 let args = fromMaybe __IMPOSSIBLE__ $ I.allApplyElims es 509 c' <- lift $ canonicalName $ I.conName c 510 C.mkTApp (C.TCon c') <$> substArgs args 511 I.Pi _ _ -> return C.TUnit 512 I.Sort _ -> return C.TSort 513 I.MetaV x _ -> return $ C.TError $ C.TMeta $ prettyShow x 514 I.DontCare _ -> return C.TErased 515 I.Dummy{} -> __IMPOSSIBLE__ 516 517-- Andreas, 2019-07-10, issue #3792 518-- | Eta-contract erased lambdas. 519-- 520-- Should also be fine for strict backends: 521-- 522-- * eta-contraction is semantics-preserving for total, effect-free languages. 523-- * should a user rely on thunking, better not used an erased abstraction! 524-- 525-- A live-or-death issue for the GHC 8.0 backend. Consider: 526-- @ 527-- foldl : ∀ {A} (B : Nat → Set) 528-- → (f : ∀ {@0 n} → B n → A → B (suc n)) 529-- → (z : B 0) 530-- → ∀ {@0 n} → Vec A n → B n 531-- foldl B f z (x ∷ xs) = foldl (λ n → B (suc n)) (λ{@0 x} → f {suc x}) (f z x) xs 532-- foldl B f z [] = z 533-- @ 534-- The hidden composition of @f@ with @suc@, term @(λ{@0 x} → f {suc x})@, 535-- can be eta-contracted to just @f@ by the compiler, since the first argument 536-- of @f@ is erased. 537-- 538-- GHC >= 8.2 seems to be able to do the optimization himself, but not 8.0. 539-- 540etaContractErased :: I.Term -> I.Term 541etaContractErased = trampoline etaErasedOnce 542 where 543 etaErasedOnce :: I.Term -> Either I.Term I.Term -- Left = done, Right = jump again 544 etaErasedOnce t = 545 case t of 546 547 -- If the abstraction is void, we don't have to strengthen. 548 I.Lam _ (NoAbs _ v) -> 549 case binAppView v of 550 -- If the body is an application ending with an erased argument, eta-reduce! 551 App u arg | not (usableModality arg) -> Right u 552 _ -> done 553 554 -- If the abstraction is non-void, only eta-contract if erased. 555 I.Lam ai (Abs _ v) | not (usableModality ai) -> 556 case binAppView v of 557 -- If the body is an application ending with an erased argument, eta-reduce! 558 -- We need to strengthen the function part then. 559 App u arg | not (usableModality arg) -> Right $ subst 0 (DontCare __DUMMY_TERM__) u 560 _ -> done 561 562 _ -> done 563 where 564 done = Left t 565 566normaliseStatic :: I.Term -> CC I.Term 567normaliseStatic v@(I.Def f es) = lift $ do 568 static <- isStaticFun . theDef <$> getConstInfo f 569 if static then normalise v else pure v 570normaliseStatic v = pure v 571 572maybeInlineDef :: I.QName -> I.Args -> CC C.TTerm 573maybeInlineDef q vs = do 574 eval <- asks ccEvaluation 575 ifM (lift $ alwaysInline q) (doinline eval) $ do 576 lift $ cacheTreeless eval q 577 def <- lift $ getConstInfo q 578 case theDef def of 579 fun@Function{} 580 | fun ^. funInline -> doinline eval 581 | otherwise -> do 582 -- If ArgUsage hasn't been computed yet, we assume all arguments are used. 583 used <- lift $ fromMaybe [] <$> getCompiledArgUse q 584 let substUsed _ ArgUnused = pure C.TErased 585 substUsed arg ArgUsed = substArg arg 586 C.mkTApp (C.TDef q) <$> zipWithM substUsed vs (used ++ repeat ArgUsed) 587 _ -> C.mkTApp (C.TDef q) <$> substArgs vs 588 where 589 doinline eval = C.mkTApp <$> inline eval q <*> substArgs vs 590 inline eval q = lift $ toTreeless' eval q 591 592substArgs :: [Arg I.Term] -> CC [C.TTerm] 593substArgs = traverse substArg 594 595substArg :: Arg I.Term -> CC C.TTerm 596substArg x | usableModality x = substTerm (unArg x) 597 | otherwise = return C.TErased 598