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

import Data.Maybe

import Agda.Syntax.Treeless
import Agda.Syntax.Literal

import Agda.TypeChecking.Monad
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)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
String -> m (Maybe QName)
getBuiltinName String
builtinNat TCMT IO (Maybe QName -> BuiltinKit)
-> TCMT IO (Maybe QName) -> TCMT IO BuiltinKit
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> TCMT IO (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
String -> m (Maybe QName)
getBuiltinName String
builtinInteger
  TTerm -> TCM TTerm
forall a. a -> TCMT IO a
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 = \case
      TCase Int
sc CaseInfo
t TTerm
def [TAlt]
alts | CaseInfo -> CaseType
caseType CaseInfo
t CaseType -> [CaseType] -> Bool
forall a. Eq a => a -> [a] -> 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 a b. (a -> b -> b) -> b -> [a] -> b
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 Quantity
_ 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 = \case
            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__

      t :: TTerm
t@TVar{}    -> TTerm
t
      t :: TTerm
t@TDef{}    -> TTerm
t
      t :: TTerm
t@TCon{}    -> TTerm
t
      t :: TTerm
t@TPrim{}   -> TTerm
t
      t :: TTerm
t@TLit{}    -> TTerm
t
      t :: TTerm
t@TUnit{}   -> TTerm
t
      t :: TTerm
t@TSort{}   -> TTerm
t
      t :: TTerm
t@TErased{} -> TTerm
t
      t :: 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)

    -- TODO:: Defined but not used
    isCaseOn :: CaseType -> [BuiltinKit -> Maybe QName] -> Bool
isCaseOn (CTData Quantity
_ QName
dt) [BuiltinKit -> Maybe QName]
xs = QName
dt QName -> [QName] -> Bool
forall a. Eq a => a -> [a] -> 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 = \case
      LitNat Integer
_     -> TPrim
PEqI
      LitFloat Double
_   -> TPrim
PEqF
      LitString Text
_  -> TPrim
PEqS
      LitChar Char
_    -> TPrim
PEqC
      LitQName QName
_   -> TPrim
PEqQ
      Literal
_ -> TPrim
forall a. HasCallStack => a
__IMPOSSIBLE__