-- | Converts case matches on literals to if cascades with equality comparisons.
module Agda.Compiler.Treeless.EliminateLiteralPatterns where

import Data.Maybe

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

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Primitive

import Agda.Utils.Impossible


eliminateLiteralPatterns :: TTerm -> TCM TTerm
eliminateLiteralPatterns :: TTerm -> TCM TTerm
eliminateLiteralPatterns t :: TTerm
t = do
  BuiltinKit
kit <- Maybe QName -> Maybe QName -> BuiltinKit
BuiltinKit (Maybe QName -> Maybe QName -> BuiltinKit)
-> TCMT IO (Maybe QName) -> TCMT IO (Maybe QName -> BuiltinKit)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> TCMT IO (Maybe QName)
getBuiltinName String
builtinNat TCMT IO (Maybe QName -> BuiltinKit)
-> TCMT IO (Maybe QName) -> TCMT IO BuiltinKit
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> TCMT IO (Maybe QName)
getBuiltinName String
builtinInteger
  TTerm -> TCM TTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm -> TCM TTerm) -> TTerm -> TCM TTerm
forall a b. (a -> b) -> a -> b
$ BuiltinKit -> TTerm -> TTerm
transform BuiltinKit
kit TTerm
t

data BuiltinKit = BuiltinKit
  { BuiltinKit -> Maybe QName
nat :: Maybe QName
  , BuiltinKit -> Maybe QName
int :: Maybe QName
  }

transform :: BuiltinKit -> TTerm -> TTerm
transform :: BuiltinKit -> TTerm -> TTerm
transform kit :: BuiltinKit
kit = TTerm -> TTerm
tr
  where
    tr :: TTerm -> TTerm
    tr :: TTerm -> TTerm
tr t :: TTerm
t = case TTerm
t of
      TCase sc :: Int
sc t :: CaseInfo
t def :: TTerm
def alts :: [TAlt]
alts | CaseInfo -> CaseType
caseType CaseInfo
t CaseType -> [CaseType] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CaseType
CTChar, CaseType
CTString, CaseType
CTQName, CaseType
CTNat, CaseType
CTInt, CaseType
CTFloat] ->
        (TAlt -> TTerm -> TTerm) -> TTerm -> [TAlt] -> TTerm
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TAlt -> TTerm -> TTerm
litAlt (TTerm -> TTerm
tr TTerm
def) [TAlt]
alts
        where
          litAlt :: TAlt -> TTerm -> TTerm
          litAlt :: TAlt -> TTerm -> TTerm
litAlt (TALit l :: Literal
l body :: TTerm
body) cont :: TTerm
cont =
            TTerm -> TTerm -> TTerm -> TTerm
tIfThenElse
              (TPrim -> TTerm -> TTerm -> TTerm
tOp (Literal -> TPrim
eqFromLit Literal
l) (Literal -> TTerm
TLit Literal
l) (Int -> TTerm
TVar Int
sc))
              (TTerm -> TTerm
tr TTerm
body)
              TTerm
cont
          litAlt _ _ = TTerm
forall a. HasCallStack => a
__IMPOSSIBLE__
      TCase sc :: Int
sc t :: CaseInfo
t@CaseInfo{caseType :: CaseInfo -> CaseType
caseType = CTData dt :: QName
dt} def :: TTerm
def alts :: [TAlt]
alts -> Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
TCase Int
sc CaseInfo
t (TTerm -> TTerm
tr TTerm
def) ((TAlt -> TAlt) -> [TAlt] -> [TAlt]
forall a b. (a -> b) -> [a] -> [b]
map TAlt -> TAlt
trAlt [TAlt]
alts)
        where
          trAlt :: TAlt -> TAlt
trAlt a :: TAlt
a = case TAlt
a of
            TAGuard g :: TTerm
g b :: TTerm
b -> TTerm -> TTerm -> TAlt
TAGuard (TTerm -> TTerm
tr TTerm
g) (TTerm -> TTerm
tr TTerm
b)
            TACon q :: QName
q a :: Int
a b :: TTerm
b -> QName -> Int -> TTerm -> TAlt
TACon QName
q Int
a (TTerm -> TTerm
tr TTerm
b)
            TALit l :: Literal
l b :: TTerm
b   -> Literal -> TTerm -> TAlt
TALit Literal
l (TTerm -> TTerm
tr TTerm
b)
      TCase _ _ _ _ -> TTerm
forall a. HasCallStack => a
__IMPOSSIBLE__

      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 a :: TTerm
a               -> TTerm -> TTerm
TCoerce (TTerm -> TTerm
tr TTerm
a)
      TLam b :: TTerm
b                  -> TTerm -> TTerm
TLam (TTerm -> TTerm
tr TTerm
b)
      TApp a :: TTerm
a bs :: 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 e :: TTerm
e b :: TTerm
b                -> TTerm -> TTerm -> TTerm
TLet (TTerm -> TTerm
tr TTerm
e) (TTerm -> TTerm
tr TTerm
b)

    isCaseOn :: CaseType -> [BuiltinKit -> Maybe QName] -> Bool
isCaseOn (CTData dt :: QName
dt) xs :: [BuiltinKit -> Maybe QName]
xs = QName
dt QName -> [QName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((BuiltinKit -> Maybe QName) -> Maybe QName)
-> [BuiltinKit -> Maybe QName] -> [QName]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((BuiltinKit -> Maybe QName) -> BuiltinKit -> Maybe QName
forall a b. (a -> b) -> a -> b
$ BuiltinKit
kit) [BuiltinKit -> Maybe QName]
xs
    isCaseOn _ _ = Bool
False

    eqFromLit :: Literal -> TPrim
    eqFromLit :: Literal -> TPrim
eqFromLit x :: Literal
x = case Literal
x of
      LitNat _ _     -> TPrim
PEqI
      LitFloat _ _   -> TPrim
PEqF
      LitString _ _  -> TPrim
PEqS
      LitChar _ _    -> TPrim
PEqC
      LitQName _ _   -> TPrim
PEqQ
      _              -> TPrim
forall a. HasCallStack => a
__IMPOSSIBLE__