-- | Eliminates case defaults by adding an alternative for all possible
-- constructors. Literal cases are preserved as-is.
module Agda.Compiler.Treeless.EliminateDefaults where

import Control.Monad
import qualified Data.List as List

import Agda.Syntax.Treeless

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute

import Agda.Compiler.Treeless.Subst () --instance only

eliminateCaseDefaults :: TTerm -> TCM TTerm
eliminateCaseDefaults :: TTerm -> TCM TTerm
eliminateCaseDefaults = TTerm -> TCM TTerm
tr
  where
    tr :: TTerm -> TCM TTerm
    tr :: TTerm -> TCM TTerm
tr = \case
      TCase Int
sc ct :: CaseInfo
ct@CaseInfo{caseType :: CaseInfo -> CaseType
caseType = CTData Quantity
_ QName
qn} TTerm
def [TAlt]
alts
        | Bool -> Bool
not (TTerm -> Bool
forall a. Unreachable a => a -> Bool
isUnreachable TTerm
def) -> do
        [QName]
dtCons <- Defn -> [QName]
defConstructors (Defn -> [QName]) -> (Definition -> Defn) -> Definition -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> [QName]) -> TCMT IO Definition -> TCMT IO [QName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qn
        let missingCons :: [QName]
missingCons = [QName]
dtCons [QName] -> [QName] -> [QName]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ (TAlt -> QName) -> [TAlt] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map TAlt -> QName
aCon [TAlt]
alts
        TTerm
def <- TTerm -> TCM TTerm
tr TTerm
def
        [TAlt]
newAlts <- [QName] -> (QName -> TCMT IO TAlt) -> TCMT IO [TAlt]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [QName]
missingCons ((QName -> TCMT IO TAlt) -> TCMT IO [TAlt])
-> (QName -> TCMT IO TAlt) -> TCMT IO [TAlt]
forall a b. (a -> b) -> a -> b
$ \QName
con -> do
          Constructor {conArity :: Defn -> Int
conArity = Int
ar} <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
con
          TAlt -> TCMT IO TAlt
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (TAlt -> TCMT IO TAlt) -> TAlt -> TCMT IO TAlt
forall a b. (a -> b) -> a -> b
$ QName -> Int -> TTerm -> TAlt
TACon QName
con Int
ar (Int -> TTerm
TVar Int
ar)

        [TAlt]
alts' <- ([TAlt] -> [TAlt] -> [TAlt]
forall a. [a] -> [a] -> [a]
++ [TAlt]
newAlts) ([TAlt] -> [TAlt]) -> TCMT IO [TAlt] -> TCMT IO [TAlt]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TAlt -> TCMT IO TAlt) -> [TAlt] -> TCMT IO [TAlt]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (TAlt -> TCMT IO TAlt
trAlt (TAlt -> TCMT IO TAlt) -> (TAlt -> TAlt) -> TAlt -> TCMT IO TAlt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> TAlt -> TAlt
forall a. Subst a => Int -> a -> a
raise Int
1) [TAlt]
alts

        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
$ TTerm -> TTerm -> TTerm
TLet TTerm
def (TTerm -> TTerm) -> TTerm -> TTerm
forall a b. (a -> b) -> a -> b
$ Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
TCase (Int
sc Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) CaseInfo
ct TTerm
tUnreachable [TAlt]
alts'
      TCase Int
sc CaseInfo
ct TTerm
def [TAlt]
alts -> Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
TCase Int
sc CaseInfo
ct (TTerm -> [TAlt] -> TTerm)
-> TCM TTerm -> TCMT IO ([TAlt] -> TTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCM TTerm
tr TTerm
def TCMT IO ([TAlt] -> TTerm) -> TCMT IO [TAlt] -> TCM TTerm
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
<*> (TAlt -> TCMT IO TAlt) -> [TAlt] -> TCMT IO [TAlt]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TAlt -> TCMT IO TAlt
trAlt [TAlt]
alts

      t :: TTerm
t@TVar{}    -> TTerm -> TCM TTerm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
      t :: TTerm
t@TDef{}    -> TTerm -> TCM TTerm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
      t :: TTerm
t@TCon{}    -> TTerm -> TCM TTerm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
      t :: TTerm
t@TPrim{}   -> TTerm -> TCM TTerm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
      t :: TTerm
t@TLit{}    -> TTerm -> TCM TTerm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
      t :: TTerm
t@TUnit{}   -> TTerm -> TCM TTerm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
      t :: TTerm
t@TSort{}   -> TTerm -> TCM TTerm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
      t :: TTerm
t@TErased{} -> TTerm -> TCM TTerm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
      t :: TTerm
t@TError{}  -> TTerm -> TCM TTerm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t

      TCoerce TTerm
a               -> TTerm -> TTerm
TCoerce (TTerm -> TTerm) -> TCM TTerm -> TCM TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCM TTerm
tr TTerm
a
      TLam TTerm
b                  -> TTerm -> TTerm
TLam (TTerm -> TTerm) -> TCM TTerm -> TCM TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCM TTerm
tr TTerm
b
      TApp TTerm
a Args
bs               -> TTerm -> Args -> TTerm
TApp (TTerm -> Args -> TTerm) -> TCM TTerm -> TCMT IO (Args -> TTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCM TTerm
tr TTerm
a TCMT IO (Args -> TTerm) -> TCMT IO Args -> TCM TTerm
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
<*> (TTerm -> TCM TTerm) -> Args -> TCMT IO Args
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TTerm -> TCM TTerm
tr Args
bs
      TLet TTerm
e TTerm
b                -> TTerm -> TTerm -> TTerm
TLet (TTerm -> TTerm -> TTerm) -> TCM TTerm -> TCMT IO (TTerm -> TTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCM TTerm
tr TTerm
e TCMT IO (TTerm -> TTerm) -> TCM TTerm -> TCM TTerm
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
<*> TTerm -> TCM TTerm
tr TTerm
b

    trAlt :: TAlt -> TCM TAlt
    trAlt :: TAlt -> TCMT IO TAlt
trAlt = \case
      TAGuard TTerm
g TTerm
b -> TTerm -> TTerm -> TAlt
TAGuard (TTerm -> TTerm -> TAlt) -> TCM TTerm -> TCMT IO (TTerm -> TAlt)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCM TTerm
tr TTerm
g TCMT IO (TTerm -> TAlt) -> TCM TTerm -> TCMT IO TAlt
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
<*> TTerm -> TCM TTerm
tr TTerm
b
      TACon QName
q Int
a TTerm
b -> QName -> Int -> TTerm -> TAlt
TACon QName
q Int
a (TTerm -> TAlt) -> TCM TTerm -> TCMT IO TAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCM TTerm
tr TTerm
b
      TALit Literal
l TTerm
b   -> Literal -> TTerm -> TAlt
TALit Literal
l (TTerm -> TAlt) -> TCM TTerm -> TCMT IO TAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCM TTerm
tr TTerm
b