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