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

import qualified Data.List as List


import Agda.Syntax.Abstract.Name (QName)
import Agda.Syntax.Treeless
import Agda.Syntax.Literal

import Agda.TypeChecking.Substitute

import Agda.Compiler.Treeless.Subst

import Agda.Utils.Impossible

#include "undefined.h"



convertGuards :: TTerm -> TTerm
convertGuards = tr
  where
    tr t = case t of
      TCase sc t def alts ->
        if null otherAlts
          then
            def'
          else
            TCase sc t def' (fmap trAlt otherAlts)
        where
          (plusAlts, otherAlts) = splitAlts alts

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

          def' = foldr guardedAlt (tr def) plusAlts

          trAlt (TAGuard{}) = __IMPOSSIBLE__
          trAlt a = a { aBody = tr (aBody a) }

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

      TCoerce a               -> TCoerce (tr a)
      TLam b                  -> TLam (tr b)
      TApp a bs               -> TApp (tr a) (map tr bs)
      TLet e b                -> TLet (tr e) (tr b)

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