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