1-- | Eliminates case defaults by adding an alternative for all possible
2-- constructors. Literal cases are preserved as-is.
3module Agda.Compiler.Treeless.EliminateDefaults where
4
5import Control.Monad
6import qualified Data.List as List
7
8import Agda.Syntax.Treeless
9
10import Agda.TypeChecking.Monad
11import Agda.TypeChecking.Substitute
12
13import Agda.Compiler.Treeless.Subst () --instance only
14
15eliminateCaseDefaults :: TTerm -> TCM TTerm
16eliminateCaseDefaults = tr
17  where
18    tr :: TTerm -> TCM TTerm
19    tr = \case
20      TCase sc ct@CaseInfo{caseType = CTData _ qn} def alts
21        | not (isUnreachable def) -> do
22        dtCons <- defConstructors . theDef <$> getConstInfo qn
23        let missingCons = dtCons List.\\ map aCon alts
24        def <- tr def
25        newAlts <- forM missingCons $ \con -> do
26          Constructor {conArity = ar} <- theDef <$> getConstInfo con
27          return $ TACon con ar (TVar ar)
28
29        alts' <- (++ newAlts) <$> mapM (trAlt . raise 1) alts
30
31        return $ TLet def $ TCase (sc + 1) ct tUnreachable alts'
32      TCase sc ct def alts -> TCase sc ct <$> tr def <*> mapM trAlt alts
33
34      t@TVar{}    -> return t
35      t@TDef{}    -> return t
36      t@TCon{}    -> return t
37      t@TPrim{}   -> return t
38      t@TLit{}    -> return t
39      t@TUnit{}   -> return t
40      t@TSort{}   -> return t
41      t@TErased{} -> return t
42      t@TError{}  -> return t
43
44      TCoerce a               -> TCoerce <$> tr a
45      TLam b                  -> TLam <$> tr b
46      TApp a bs               -> TApp <$> tr a <*> mapM tr bs
47      TLet e b                -> TLet <$> tr e <*> tr b
48
49    trAlt :: TAlt -> TCM TAlt
50    trAlt = \case
51      TAGuard g b -> TAGuard <$> tr g <*> tr b
52      TACon q a b -> TACon q a <$> tr b
53      TALit l b   -> TALit l <$> tr b
54