1-- | Converts case matches on literals to if cascades with equality comparisons. 2module Agda.Compiler.Treeless.EliminateLiteralPatterns where 3 4import Data.Maybe 5 6import Agda.Syntax.Treeless 7import Agda.Syntax.Literal 8 9import Agda.TypeChecking.Monad 10import Agda.TypeChecking.Primitive 11 12import Agda.Utils.Impossible 13 14 15eliminateLiteralPatterns :: TTerm -> TCM TTerm 16eliminateLiteralPatterns t = do 17 kit <- BuiltinKit <$> getBuiltinName builtinNat <*> getBuiltinName builtinInteger 18 return $ transform kit t 19 20data BuiltinKit = BuiltinKit 21 { nat :: Maybe QName 22 , int :: Maybe QName 23 } 24 25transform :: BuiltinKit -> TTerm -> TTerm 26transform kit = tr 27 where 28 tr :: TTerm -> TTerm 29 tr = \case 30 TCase sc t def alts | caseType t `elem` [CTChar, CTString, CTQName, CTNat, CTInt, CTFloat] -> 31 foldr litAlt (tr def) alts 32 where 33 litAlt :: TAlt -> TTerm -> TTerm 34 litAlt (TALit l body) cont = 35 tIfThenElse 36 (tOp (eqFromLit l) (TLit l) (TVar sc)) 37 (tr body) 38 cont 39 litAlt _ _ = __IMPOSSIBLE__ 40 TCase sc t@CaseInfo{caseType = CTData _ dt} def alts -> 41 TCase sc t (tr def) (map trAlt alts) 42 where 43 trAlt = \case 44 TAGuard g b -> TAGuard (tr g) (tr b) 45 TACon q a b -> TACon q a (tr b) 46 TALit l b -> TALit l (tr b) 47 TCase _ _ _ _ -> __IMPOSSIBLE__ 48 49 t@TVar{} -> t 50 t@TDef{} -> t 51 t@TCon{} -> t 52 t@TPrim{} -> t 53 t@TLit{} -> t 54 t@TUnit{} -> t 55 t@TSort{} -> t 56 t@TErased{} -> t 57 t@TError{} -> t 58 59 TCoerce a -> TCoerce (tr a) 60 TLam b -> TLam (tr b) 61 TApp a bs -> TApp (tr a) (map tr bs) 62 TLet e b -> TLet (tr e) (tr b) 63 64 -- TODO:: Defined but not used 65 isCaseOn (CTData _ dt) xs = dt `elem` mapMaybe ($ kit) xs 66 isCaseOn _ _ = False 67 68 eqFromLit :: Literal -> TPrim 69 eqFromLit = \case 70 LitNat _ -> PEqI 71 LitFloat _ -> PEqF 72 LitString _ -> PEqS 73 LitChar _ -> PEqC 74 LitQName _ -> PEqQ 75 _ -> __IMPOSSIBLE__ 76