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