-- | Translates guard alternatives to if-then-else cascades.
--
-- The builtin translation must be run before this transformation.
module Agda.Compiler.Treeless.GuardsToPrims ( convertGuards ) where

import qualified Data.List as List

import Agda.Syntax.Treeless

import Agda.Utils.Impossible


convertGuards :: TTerm -> TTerm
convertGuards :: TTerm -> TTerm
convertGuards = TTerm -> TTerm
tr
  where
    tr :: TTerm -> TTerm
tr TTerm
t = case TTerm
t of
      TCase Int
sc CaseInfo
t TTerm
def [TAlt]
alts ->
        if [TAlt] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TAlt]
otherAlts
          then
            TTerm
def'
          else
            Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
TCase Int
sc CaseInfo
t TTerm
def' ((TAlt -> TAlt) -> [TAlt] -> [TAlt]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TAlt -> TAlt
trAlt [TAlt]
otherAlts)
        where
          ([TAlt]
plusAlts, [TAlt]
otherAlts) = [TAlt] -> ([TAlt], [TAlt])
splitAlts [TAlt]
alts

          guardedAlt :: TAlt -> TTerm -> TTerm
          guardedAlt :: TAlt -> TTerm -> TTerm
guardedAlt (TAGuard TTerm
g TTerm
body) TTerm
cont = TTerm -> TTerm -> TTerm -> TTerm
tIfThenElse (TTerm -> TTerm
tr TTerm
g) (TTerm -> TTerm
tr TTerm
body) (TTerm -> TTerm
tr TTerm
cont)
          guardedAlt TAlt
_ TTerm
_ = TTerm
forall a. HasCallStack => a
__IMPOSSIBLE__

          def' :: TTerm
def' = (TAlt -> TTerm -> TTerm) -> TTerm -> [TAlt] -> TTerm
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TAlt -> TTerm -> TTerm
guardedAlt (TTerm -> TTerm
tr TTerm
def) [TAlt]
plusAlts

          trAlt :: TAlt -> TAlt
trAlt (TAGuard{}) = TAlt
forall a. HasCallStack => a
__IMPOSSIBLE__
          trAlt TAlt
a = TAlt
a { aBody :: TTerm
aBody = TTerm -> TTerm
tr (TAlt -> TTerm
aBody TAlt
a) }

      TVar{}    -> TTerm
t
      TDef{}    -> TTerm
t
      TCon{}    -> TTerm
t
      TPrim{}   -> TTerm
t
      TLit{}    -> TTerm
t
      TUnit{}   -> TTerm
t
      TSort{}   -> TTerm
t
      TErased{} -> TTerm
t
      TError{}  -> TTerm
t

      TCoerce TTerm
a               -> TTerm -> TTerm
TCoerce (TTerm -> TTerm
tr TTerm
a)
      TLam TTerm
b                  -> TTerm -> TTerm
TLam (TTerm -> TTerm
tr TTerm
b)
      TApp TTerm
a Args
bs               -> TTerm -> Args -> TTerm
TApp (TTerm -> TTerm
tr TTerm
a) ((TTerm -> TTerm) -> Args -> Args
forall a b. (a -> b) -> [a] -> [b]
map TTerm -> TTerm
tr Args
bs)
      TLet TTerm
e TTerm
b                -> TTerm -> TTerm -> TTerm
TLet (TTerm -> TTerm
tr TTerm
e) (TTerm -> TTerm
tr TTerm
b)

-- | Split alts into TAGuard alts and other alts.
splitAlts :: [TAlt] -> ([TAlt], [TAlt])
splitAlts :: [TAlt] -> ([TAlt], [TAlt])
splitAlts = (TAlt -> Bool) -> [TAlt] -> ([TAlt], [TAlt])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition TAlt -> Bool
isGuardAlt
  where isGuardAlt :: TAlt -> Bool
isGuardAlt (TAGuard TTerm
_ TTerm
_) = Bool
True
        isGuardAlt TAlt
_ = Bool
False