module Agda.TypeChecking.Functions
( etaExpandClause
, getDef
) where
import Control.Arrow ( first )
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Level
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.Utils.Impossible
import Agda.Utils.Functor ( ($>) )
import Agda.Utils.Pretty ( prettyShow )
import Agda.Utils.Monad
import Agda.Utils.Size
etaExpandClause :: MonadTCM tcm => Clause -> tcm Clause
etaExpandClause :: Clause -> tcm Clause
etaExpandClause clause :: Clause
clause = TCM Clause -> tcm Clause
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Clause -> tcm Clause) -> TCM Clause -> tcm Clause
forall a b. (a -> b) -> a -> b
$ do
case Clause
clause of
Clause _ _ ctel :: Telescope
ctel ps :: NAPs
ps _ Nothing _ _ _ _ -> Clause -> TCM Clause
forall (m :: * -> *) a. Monad m => a -> m a
return Clause
clause
Clause _ _ ctel :: Telescope
ctel ps :: NAPs
ps Nothing (Just t :: Arg Type
t) _ _ _ _ -> Clause -> TCM Clause
forall (m :: * -> *) a. Monad m => a -> m a
return Clause
clause
Clause rl :: Range
rl rf :: Range
rf ctel :: Telescope
ctel ps :: NAPs
ps (Just body :: Term
body) (Just t :: Arg Type
t) catchall :: Bool
catchall recursive :: Maybe Bool
recursive unreachable :: Maybe Bool
unreachable ell :: ExpandedEllipsis
ell -> do
TelV tel0 :: Telescope
tel0 t' :: Type
t' <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Type -> TCMT IO (TelV Type)) -> Type -> TCMT IO (TelV Type)
forall a b. (a -> b) -> a -> b
$ Arg Type -> Type
forall e. Arg e -> e
unArg Arg Type
t
let xs :: [Arg ArgName]
xs = Term -> [Arg ArgName]
peekLambdas Term
body
let ltel :: ListTel
ltel = [Arg ArgName] -> ListTel -> ListTel
useNames [Arg ArgName]
xs (ListTel -> ListTel) -> ListTel -> ListTel
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel0
let tel :: Telescope
tel = ListTel -> Telescope
telFromList ListTel
ltel
let n :: Int
n = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel
Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel0) TCMT IO ()
forall a. HasCallStack => a
__IMPOSSIBLE__
let ctel' :: Telescope
ctel' = ListTel -> Telescope
telFromList (ListTel -> Telescope) -> ListTel -> Telescope
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
ctel ListTel -> ListTel -> ListTel
forall a. [a] -> [a] -> [a]
++ ListTel
ltel
ps' :: NAPs
ps' = Int -> NAPs -> NAPs
forall t a. Subst t a => Int -> a -> a
raise Int
n NAPs
ps NAPs -> NAPs -> NAPs
forall a. [a] -> [a] -> [a]
++ Telescope -> NAPs
forall a. DeBruijn a => Telescope -> [NamedArg a]
teleNamedArgs Telescope
tel
body' :: Term
body' = Int -> Term -> Term
forall t a. Subst t a => Int -> a -> a
raise Int
n Term
body Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` Telescope -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
tel
ArgName -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc "term.clause.expand" 30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
[ "etaExpandClause"
, " body = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
ctel' (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
body)
, " xs = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCM Doc
forall (m :: * -> *). Monad m => ArgName -> m Doc
text ([Arg ArgName] -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow [Arg ArgName]
xs)
, " new tel = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
ctel'
]
Clause -> TCM Clause
forall (m :: * -> *) a. Monad m => a -> m a
return (Clause -> TCM Clause) -> Clause -> TCM Clause
forall a b. (a -> b) -> a -> b
$ Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Clause
Clause Range
rl Range
rf Telescope
ctel' NAPs
ps' (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
body') (Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just (Arg Type
t Arg Type -> Type -> Arg Type
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Type
t')) Bool
catchall Maybe Bool
recursive Maybe Bool
unreachable ExpandedEllipsis
ell
where
peekLambdas :: Term -> [Arg ArgName]
peekLambdas :: Term -> [Arg ArgName]
peekLambdas v :: Term
v =
case Term
v of
Lam info :: ArgInfo
info b :: Abs Term
b -> ArgInfo -> ArgName -> Arg ArgName
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Abs Term -> ArgName
forall a. Abs a -> ArgName
absName Abs Term
b) Arg ArgName -> [Arg ArgName] -> [Arg ArgName]
forall a. a -> [a] -> [a]
: Term -> [Arg ArgName]
peekLambdas (Abs Term -> Term
forall a. Abs a -> a
unAbs Abs Term
b)
_ -> []
useNames :: [Arg ArgName] -> ListTel -> ListTel
useNames :: [Arg ArgName] -> ListTel -> ListTel
useNames [] tel :: ListTel
tel = (Dom (ArgName, Type) -> Dom (ArgName, Type)) -> ListTel -> ListTel
forall a b. (a -> b) -> [a] -> [b]
map (Origin -> Dom (ArgName, Type) -> Dom (ArgName, Type)
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted) ListTel
tel
useNames (_:_) [] = []
useNames (x :: Arg ArgName
x:xs :: [Arg ArgName]
xs) (dom :: Dom (ArgName, Type)
dom:tel :: ListTel
tel)
| Arg ArgName -> Dom (ArgName, Type) -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Arg ArgName
x Dom (ArgName, Type)
dom =
((ArgName, Type) -> (ArgName, Type))
-> Dom (ArgName, Type) -> Dom (ArgName, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ArgName -> ArgName) -> (ArgName, Type) -> (ArgName, Type)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((ArgName -> ArgName) -> (ArgName, Type) -> (ArgName, Type))
-> (ArgName -> ArgName) -> (ArgName, Type) -> (ArgName, Type)
forall a b. (a -> b) -> a -> b
$ ArgName -> ArgName -> ArgName
forall a b. a -> b -> a
const (ArgName -> ArgName -> ArgName) -> ArgName -> ArgName -> ArgName
forall a b. (a -> b) -> a -> b
$ Arg ArgName -> ArgName
forall e. Arg e -> e
unArg Arg ArgName
x) Dom (ArgName, Type)
dom Dom (ArgName, Type) -> ListTel -> ListTel
forall a. a -> [a] -> [a]
: [Arg ArgName] -> ListTel -> ListTel
useNames [Arg ArgName]
xs ListTel
tel
| Bool
otherwise =
Origin -> Dom (ArgName, Type) -> Dom (ArgName, Type)
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted Dom (ArgName, Type)
dom Dom (ArgName, Type) -> ListTel -> ListTel
forall a. a -> [a] -> [a]
: [Arg ArgName] -> ListTel -> ListTel
useNames (Arg ArgName
xArg ArgName -> [Arg ArgName] -> [Arg ArgName]
forall a. a -> [a] -> [a]
:[Arg ArgName]
xs) ListTel
tel
getDef :: Term -> TCM (Maybe QName)
getDef :: Term -> TCM (Maybe QName)
getDef t :: Term
t = Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
t TCMT IO Term -> (Term -> TCM (Maybe QName)) -> TCM (Maybe QName)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Def d :: QName
d _ -> Maybe QName -> TCM (Maybe QName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe QName -> TCM (Maybe QName))
-> Maybe QName -> TCM (Maybe QName)
forall a b. (a -> b) -> a -> b
$ QName -> Maybe QName
forall a. a -> Maybe a
Just QName
d
Lam _ v :: Abs Term
v -> Abs Term -> (Term -> TCM (Maybe QName)) -> TCM (Maybe QName)
forall t a (m :: * -> *) b.
(Subst t a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs Term
v Term -> TCM (Maybe QName)
getDef
Level v :: Level
v -> Term -> TCM (Maybe QName)
getDef (Term -> TCM (Maybe QName)) -> TCMT IO Term -> TCM (Maybe QName)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Level -> TCMT IO Term
forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
v
DontCare v :: Term
v -> Term -> TCM (Maybe QName)
getDef Term
v
_ -> Maybe QName -> TCM (Maybe QName)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe QName
forall a. Maybe a
Nothing