1-- | Translates guard alternatives to if-then-else cascades.
2--
3-- The builtin translation must be run before this transformation.
4module Agda.Compiler.Treeless.GuardsToPrims ( convertGuards ) where
5
6import qualified Data.List as List
7
8import Agda.Syntax.Treeless
9
10import Agda.Utils.Impossible
11
12
13convertGuards :: TTerm -> TTerm
14convertGuards = tr
15  where
16    tr = \case
17      TCase sc t def alts ->
18        if null otherAlts
19          then
20            def'
21          else
22            TCase sc t def' (fmap trAlt otherAlts)
23        where
24          (plusAlts, otherAlts) = splitAlts alts
25
26          guardedAlt :: TAlt -> TTerm -> TTerm
27          guardedAlt (TAGuard g body) cont = tIfThenElse (tr g) (tr body) (tr cont)
28          guardedAlt _ _ = __IMPOSSIBLE__
29
30          def' = foldr guardedAlt (tr def) plusAlts
31
32          trAlt (TAGuard{}) = __IMPOSSIBLE__
33          trAlt a = a { aBody = tr (aBody a) }
34
35      t@TVar{}    -> t
36      t@TDef{}    -> t
37      t@TCon{}    -> t
38      t@TPrim{}   -> t
39      t@TLit{}    -> t
40      t@TUnit{}   -> t
41      t@TSort{}   -> t
42      t@TErased{} -> t
43      t@TError{}  -> t
44
45      TCoerce a               -> TCoerce (tr a)
46      TLam b                  -> TLam (tr b)
47      TApp a bs               -> TApp (tr a) (map tr bs)
48      TLet e b                -> TLet (tr e) (tr b)
49
50-- | Split alts into TAGuard alts and other alts.
51splitAlts :: [TAlt] -> ([TAlt], [TAlt])
52splitAlts = List.partition isGuardAlt
53  where isGuardAlt (TAGuard _ _) = True
54        isGuardAlt _ = False
55