    {-# OPTIONS_GHC -Wunused-imports #-}

    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.Monad.Pure
    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.Syntax.Common.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 :: PureTCM tcm => Clause -> tcm Clause
    etaExpandClause :: forall (tcm :: * -> *). PureTCM tcm => Clause -> tcm Clause
    etaExpandClause Clause
    clause = do
      case Clause
    clause of
        Clause Range
    _  Range
    _  Telescope
    ctel [NamedArg DeBruijnPattern]
    ps Maybe Term
    _           Maybe (Arg Type)
    Nothing  Catchall
    _ Maybe Bool
    _ Maybe Bool
    _ ExpandedEllipsis
    _ Maybe ModuleName
    _ -> Clause -> tcm Clause
    forall a. a -> tcm 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) Catchall
    _ Maybe Bool
    _ Maybe Bool
    _ ExpandedEllipsis
    _ Maybe ModuleName
    _ -> Clause -> tcm Clause
    forall a. a -> tcm 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) Catchall
    catchall Maybe Bool
    recursive Maybe Bool
    unreachable ExpandedEllipsis
    ell Maybe ModuleName
    wm -> do

          -- Get the telescope to expand the clause with.
          TelV tel0 t' <- Telescope -> tcm (TelV Type) -> tcm (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 (tcm (TelV Type) -> tcm (TelV Type))
    -> tcm (TelV Type) -> tcm (TelV Type)
    forall a b. (a -> b) -> a -> b
    $ Type -> tcm (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView (Type -> tcm (TelV Type)) -> Type -> tcm (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   = Term -> [Arg ArgName]
    peekLambdas Term
    body
          let 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  = ListTel -> Telescope
    telFromList ListTel
    ltel
          let n    = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel
          unless (n == size tel0) __IMPOSSIBLE__  -- useNames should not drop anything
          -- Join with lhs telescope, extend patterns and apply body.
          -- NB: no need to raise ctel!
          let 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'   = 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' = 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
          reportSDoc "term.clause.expand" 30 $ inTopContext $ vcat
            [ "etaExpandClause"
            , "  body    = " <+> addContext ctel' (prettyTCM body)
            , "  xs      = " <+> text (prettyShow xs)
            , "  new tel = " <+> prettyTCM ctel'
            ]
          return $ Clause rl rf ctel' ps' (Just body') (Just (t $> t')) catchall recursive unreachable ell 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