-- | 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 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 BuiltinKit
kit = TTerm -> TTerm
tr
  where
    tr :: TTerm -> TTerm
    tr :: TTerm -> TTerm
tr TTerm
t = case TTerm
t of
      TCase Int
sc CaseInfo
t TTerm
def [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 Literal
l TTerm
body) 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 TAlt
_ TTerm
_ = TTerm
forall a. HasCallStack => a
__IMPOSSIBLE__
      TCase Int
sc t :: CaseInfo
t@CaseInfo{caseType :: CaseInfo -> CaseType
caseType = CTData QName
dt} TTerm
def [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 TAlt
a = case TAlt
a of
            TAGuard TTerm
g TTerm
b -> TTerm -> TTerm -> TAlt
TAGuard (TTerm -> TTerm
tr TTerm
g) (TTerm -> TTerm
tr TTerm
b)
            TACon QName
q Int
a TTerm
b -> QName -> Int -> TTerm -> TAlt
TACon QName
q Int
a (TTerm -> TTerm
tr TTerm
b)
            TALit Literal
l TTerm
b   -> Literal -> TTerm -> TAlt
TALit Literal
l (TTerm -> TTerm
tr TTerm
b)
      TCase Int
_ CaseInfo
_ TTerm
_ [TAlt]
_ -> 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 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)

    isCaseOn :: CaseType -> [BuiltinKit -> Maybe QName] -> Bool
isCaseOn (CTData QName
dt) [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 CaseType
_ [BuiltinKit -> Maybe QName]
_ = Bool
False

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