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

      -- Get the telescope to expand the clause with.
      TelV Telescope
tel0 Type
t' <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
ctel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel0
      let tel :: Telescope
tel  = ListTel -> Telescope
telFromList ListTel
ltel
      let n :: Int
n    = forall a. Sized a => a -> Int
size Telescope
tel
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n forall a. Eq a => a -> a -> Bool
== forall a. Sized a => a -> Int
size Telescope
tel0) 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 forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
ctel forall a. [a] -> [a] -> [a]
++ ListTel
ltel
          ps' :: [NamedArg DeBruijnPattern]
ps'   = forall a. Subst a => Int -> a -> a
raise Int
n [NamedArg DeBruijnPattern]
ps forall a. [a] -> [a] -> [a]
++ forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
tel
          body' :: Term
body' = forall a. Subst a => Int -> a -> a
raise Int
n Term
body forall t. Apply t => t -> Args -> t
`apply` forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
tel
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"term.clause.expand" Int
30 forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"etaExpandClause"
        , TCMT IO Doc
"  body    = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
ctel' (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
body)
        , TCMT IO Doc
"  xs      = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Pretty a => a -> ArgName
prettyShow [Arg ArgName]
xs)
        , TCMT IO Doc
"  new tel = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
ctel'
        ]
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range
-> Range
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
Clause Range
rl Range
rf Telescope
ctel' [NamedArg DeBruijnPattern]
ps' (forall a. a -> Maybe a
Just Term
body') (forall a. a -> Maybe a
Just (Arg Type
t 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 Maybe ModuleName
wm
  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 -> forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (forall a. Abs a -> ArgName
absName Abs Term
b) forall a. a -> [a] -> [a]
: Term -> [Arg ArgName]
peekLambdas (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       = forall a b. (a -> b) -> [a] -> [b]
map (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)
      | forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Arg ArgName
x Dom (ArgName, Type)
dom =
          -- set the ArgName of the dom
          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg ArgName
x) Dom (ArgName, Type)
dom forall a. a -> [a] -> [a]
: [Arg ArgName] -> ListTel -> ListTel
useNames [Arg ArgName]
xs ListTel
tel
      | Bool
otherwise =
          forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted Dom (ArgName, Type)
dom forall a. a -> [a] -> [a]
: [Arg ArgName] -> ListTel -> ListTel
useNames (Arg ArgName
xforall 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 = forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Def QName
d Elims
_    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just QName
d
  Lam ArgInfo
_ Abs Term
v    -> 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
v
  DontCare Term
v -> Term -> TCM (Maybe QName)
getDef Term
v
  Term
_          -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing