    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 (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 -> 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
    addContext Telescope
    ctel' (Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    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