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