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


-- | Expand a clause to the maximal arity, by inserting variable
--   patterns and applying the body to variables.

--  Fixes issue #2376.
--  Replaces 'introHiddenLambdas'.
--  See, e.g., test/Succeed/SizedTypesExtendedLambda.agda.

--  This is used instead of special treatment of lambdas
--  (which was unsound: Issue #121)

etaExpandClause :: MonadTCM tcm => Clause -> tcm Clause
etaExpandClause :: Clause -> tcm Clause
etaExpandClause 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 Range
_  Range
_  Telescope
ctel NAPs
ps Maybe Term
_           Maybe (Arg Type)
Nothing  Bool
_ Maybe Bool
_ Maybe Bool
_ Maybe Bool
_ ExpandedEllipsis
_ -> Clause -> TCM Clause
forall (m :: * -> *) a. Monad m => a -> m a
return Clause
clause
    Clause Range
_  Range
_  Telescope
ctel NAPs
ps Maybe Term
Nothing     (Just Arg Type
t) Bool
_ Maybe Bool
_ Maybe Bool
_ Maybe Bool
_ ExpandedEllipsis
_ -> Clause -> TCM Clause
forall (m :: * -> *) a. Monad m => a -> m a
return Clause
clause
    Clause Range
rl Range
rf Telescope
ctel NAPs
ps (Just Term
body) (Just Arg Type
t) Bool
catchall Maybe Bool
exact Maybe Bool
recursive Maybe Bool
unreachable ExpandedEllipsis
ell -> do

      -- Get the telescope to expand the clause with.
      TelV Telescope
tel0 Type
t' <- Telescope -> TCMT IO (TelV Type) -> TCMT IO (TelV Type)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
ctel (TCMT IO (TelV Type) -> TCMT IO (TelV Type))
-> TCMT IO (TelV Type) -> TCMT IO (TelV Type)
forall a b. (a -> b) -> a -> b
$ 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

      -- If the rhs has lambdas, harvest the names of the bound variables.
      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__  -- useNames should not drop anything
      -- Join with lhs telescope, extend patterns and apply body.
      -- NB: no need to raise ctel!
      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 a. Subst 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 a. Subst 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 ArgName
"term.clause.expand" Int
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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCM Doc
"etaExpandClause"
        , TCM Doc
"  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' (Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
body)
        , TCM Doc
"  xs      = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ([Arg ArgName] -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow [Arg ArgName]
xs)
        , TCM Doc
"  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
-> 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
exact Maybe Bool
recursive Maybe Bool
unreachable ExpandedEllipsis
ell
  where
    -- Get all initial lambdas of the body.
    peekLambdas :: Term -> [Arg ArgName]
    peekLambdas :: Term -> [Arg ArgName]
peekLambdas Term
v =
      case Term
v of
        Lam ArgInfo
info 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)
        Term
_ -> []

    -- Use the names of the first argument, and set the Origin all other
    -- parts of the telescope to Inserted.
    -- The first list of arguments is a subset of the telescope.
    -- Thus, if compared pointwise, if the hiding does not match,
    -- it means we skipped an element of the telescope.
    useNames :: [Arg ArgName] -> ListTel -> ListTel
    useNames :: [Arg ArgName] -> ListTel -> ListTel
useNames []     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
    -- Andrea: we can have more Lam's than Pi's, because they might be for Path
    -- Andreas, 2017-03-24: the following case is not IMPOSSIBLE when positivity checking comes before termination checking, see examples/tactics/ac/AC.agda
    useNames (Arg ArgName
_:[Arg ArgName]
_)  []        = []
    useNames (Arg ArgName
x:[Arg ArgName]
xs) (Dom (ArgName, Type)
dom: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 =
          -- set the ArgName of the 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

-- | Get the name of defined symbol of the head normal form of a term.
--   Returns 'Nothing' if no such head exists.

getDef :: Term -> TCM (Maybe QName)
getDef :: Term -> TCM (Maybe QName)
getDef 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 QName
d Elims
_    -> 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 ArgInfo
_ Abs Term
v    -> Abs Term -> (Term -> TCM (Maybe QName)) -> TCM (Maybe QName)
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs Term
v Term -> TCM (Maybe QName)
getDef
  Level 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 Term
v -> Term -> TCM (Maybe QName)
getDef Term
v
  Term
_          -> Maybe QName -> TCM (Maybe QName)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe QName
forall a. Maybe a
Nothing