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 = TCM Clause -> tcm Clause
forall a. TCM a -> tcm a
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 [NamedArg DeBruijnPattern]
ps Maybe Term
_           Maybe (Arg Type)
Nothing  Bool
_ Maybe Bool
_ Maybe Bool
_ Maybe Bool
_ ExpandedEllipsis
_ Maybe ModuleName
_ -> Clause -> TCM Clause
forall a. a -> TCMT IO a
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
_ -> Clause -> TCM Clause
forall a. a -> TCMT IO a
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' <- Telescope -> TCMT IO (TelV Type) -> TCMT IO (TelV Type)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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' :: [NamedArg DeBruijnPattern]
ps'   = Int -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Subst a => Int -> a -> a
raise Int
n [NamedArg DeBruijnPattern]
ps [NamedArg DeBruijnPattern]
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. [a] -> [a] -> [a]
++ Telescope -> [NamedArg DeBruijnPattern]
forall a t. DeBruijn a => Tele (Dom t) -> [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 -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"term.clause.expand" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"etaExpandClause"
        , TCMT IO Doc
"  body    = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
ctel' (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
body)
        , TCMT IO Doc
"  xs      = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ([Arg ArgName] -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow [Arg ArgName]
xs)
        , TCMT IO Doc
"  new tel = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
ctel'
        ]
      Clause -> TCM Clause
forall a. a -> TCMT IO a
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
-> [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' (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 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 -> 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 a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ArgName -> ArgName) -> (ArgName, Type) -> (ArgName, Type)
forall b c d. (b -> c) -> (b, d) -> (c, d)
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 a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Def QName
d Elims
_    -> Maybe QName -> TCM (Maybe QName)
forall a. a -> TCMT IO a
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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe QName
forall a. Maybe a
Nothing