    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.TypeChecking.Rewriting.Clause where

    import Data.Maybe

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Pattern
    import Agda.Syntax.Position

    import Agda.TypeChecking.Monad

    import Agda.Utils.Functor
    import Agda.Utils.Impossible
    import Agda.Utils.Monad
    import Agda.Syntax.Common.Pretty

    ------------------------------------------------------------------------
    -- * Converting clauses to rewrite rules
    ------------------------------------------------------------------------

    {-# INLINABLE getClausesAsRewriteRules #-}
    -- | Get all the clauses of a definition and convert them to rewrite
    --   rules.
    getClausesAsRewriteRules :: (HasConstInfo m, ReadTCState m, MonadFresh NameId m) => QName -> m [RewriteRule]
    getClausesAsRewriteRules :: forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadFresh NameId m) =>
    QName -> m [RewriteRule]
    getClausesAsRewriteRules QName
    f = do
      cls <- Definition -> [Clause]
    defClauses (Definition -> [Clause]) -> m Definition -> m [Clause]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
      forMaybeM (zip [1..] cls) $ \(Int
    i,Clause
    cl) -> do
        clname <- QName -> Int -> m QName
    forall (m :: * -> *).
    (HasConstInfo m, MonadFresh NameId m) =>
    QName -> Int -> m QName
    clauseQName QName
    f Int
    i
        clauseToRewriteRule f clname cl

    {-# INLINABLE clauseQName #-}
    -- | Generate a sensible name for the given clause
    clauseQName :: (HasConstInfo m, MonadFresh NameId m) => QName -> Int -> m QName
    clauseQName :: forall (m :: * -> *).
    (HasConstInfo m, MonadFresh NameId m) =>
    QName -> Int -> m QName
    clauseQName QName
    f Int
    i = ModuleName -> Name -> QName
    QName (QName -> ModuleName
    qnameModule QName
    f) (Name -> QName) -> m Name -> m QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Name -> Int -> m Name
    forall {m :: * -> *} {a} {a}.
    (MonadFresh NameId m, Pretty a, Show a) =>
    a -> a -> m Name
    clauseName (QName -> Name
    qnameName QName
    f) Int
    i
      where
        clauseName :: a -> a -> m Name
    clauseName a
    n a
    i = Range -> [Char] -> m Name
    forall (m :: * -> *).
    MonadFresh NameId m =>
    Range -> [Char] -> m Name
    freshName Range
    forall a. Range' a
    noRange (a -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow a
    n [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "-clause" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ a -> [Char]
    forall a. Show a => a -> [Char]
    show a
    i)

    {-# INLINABLE clauseToRewriteRule #-}
    -- | @clauseToRewriteRule f q cl@ converts the clause @cl@ of the
    --   function @f@ to a rewrite rule with name @q@. Returns @Nothing@
    --   if @clauseBody cl@ is @Nothing@. Precondition: @clauseType cl@ is
    --   not @Nothing@.
    clauseToRewriteRule :: (MonadTCEnv m, ReadTCState m)
      => QName -> QName -> Clause -> m (Maybe RewriteRule)
    clauseToRewriteRule :: forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    QName -> QName -> Clause -> m (Maybe RewriteRule)
    clauseToRewriteRule QName
    f QName
    q Clause
    cl | NAPs -> Bool
    hasDefP (Clause -> NAPs
    namedClausePats Clause
    cl) = Maybe RewriteRule -> m (Maybe RewriteRule)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return  Maybe RewriteRule
    forall a. Maybe a
    Nothing
    clauseToRewriteRule QName
    f QName
    q Clause
    cl = do
      top <- TopLevelModuleName
    -> Maybe TopLevelModuleName -> TopLevelModuleName
    forall a. a -> Maybe a -> a
    fromMaybe TopLevelModuleName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe TopLevelModuleName -> TopLevelModuleName)
    -> m (Maybe TopLevelModuleName) -> m TopLevelModuleName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe TopLevelModuleName)
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    m (Maybe TopLevelModuleName)
    currentTopLevelModule
      return $ clauseBody cl <&> \Term
    rhs -> RewriteRule
        { rewName :: QName
    rewName    = QName
    q
        , rewContext :: Telescope
    rewContext = Clause -> Telescope
    clauseTel Clause
    cl
        , rewHead :: QName
    rewHead    = QName
    f
        , rewPats :: PElims
    rewPats    = NAPs -> PElims
    forall a b. ToNLPat a b => a -> b
    toNLPat (NAPs -> PElims) -> NAPs -> PElims
    forall a b. (a -> b) -> a -> b
    $ Clause -> NAPs
    namedClausePats Clause
    cl
        , rewRHS :: Term
    rewRHS     = Term
    rhs
        , rewType :: Type
    rewType    = Arg Type -> Type
    forall e. Arg e -> e
    unArg (Arg Type -> Type) -> Arg Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Arg Type -> Maybe (Arg Type) -> Arg Type
    forall a. a -> Maybe a -> a
    fromMaybe Arg Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__  (Maybe (Arg Type) -> Arg Type) -> Maybe (Arg Type) -> Arg Type
    forall a b. (a -> b) -> a -> b
    $ Clause -> Maybe (Arg Type)
    clauseType Clause
    cl
        , rewFromClause :: Bool
    rewFromClause = Bool
    True
        , rewTopModule :: TopLevelModuleName
    rewTopModule  = TopLevelModuleName
    top
        }

    class ToNLPat a b where
      toNLPat :: a -> b

      default toNLPat
        :: ( ToNLPat a' b', Functor f, a ~ f a', b ~ f b')
        => a -> b
      toNLPat = (a' -> b') -> f a' -> f b'
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a' -> b'
    forall a b. ToNLPat a b => a -> b
    toNLPat

    instance ToNLPat a b => ToNLPat [a] [b] where
    instance ToNLPat a b => ToNLPat (Dom a) (Dom b) where
    instance ToNLPat a b => ToNLPat (Elim' a) (Elim' b) where
    instance ToNLPat a b => ToNLPat (Abs a) (Abs b) where

    instance ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) where
      toNLPat :: Arg DeBruijnPattern -> Elim' NLPat
    toNLPat (Arg ArgInfo
    ai DeBruijnPattern
    p) = case DeBruijnPattern
    p of
        VarP PatternInfo
    _ DBPatVar
    x        -> NLPat -> Elim' NLPat
    app (NLPat -> Elim' NLPat) -> NLPat -> Elim' NLPat
    forall a b. (a -> b) -> a -> b
    $ Int -> [Arg Int] -> NLPat
    PVar (DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x) []
        DotP PatternInfo
    _ Term
    u        -> NLPat -> Elim' NLPat
    app (NLPat -> Elim' NLPat) -> NLPat -> Elim' NLPat
    forall a b. (a -> b) -> a -> b
    $ Term -> NLPat
    PTerm Term
    u
        ConP ConHead
    c ConPatternInfo
    _ NAPs
    ps     -> NLPat -> Elim' NLPat
    app (NLPat -> Elim' NLPat) -> NLPat -> Elim' NLPat
    forall a b. (a -> b) -> a -> b
    $ QName -> PElims -> NLPat
    PDef (ConHead -> QName
    conName ConHead
    c) (PElims -> NLPat) -> PElims -> NLPat
    forall a b. (a -> b) -> a -> b
    $ NAPs -> PElims
    forall a b. ToNLPat a b => a -> b
    toNLPat NAPs
    ps
        LitP PatternInfo
    o Literal
    l        -> NLPat -> Elim' NLPat
    app (NLPat -> Elim' NLPat) -> NLPat -> Elim' NLPat
    forall a b. (a -> b) -> a -> b
    $ Term -> NLPat
    PTerm (Term -> NLPat) -> Term -> NLPat
    forall a b. (a -> b) -> a -> b
    $ Literal -> Term
    Lit Literal
    l
        ProjP ProjOrigin
    o QName
    f       -> ProjOrigin -> QName -> Elim' NLPat
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    o QName
    f
        IApplyP PatternInfo
    _ Term
    u Term
    v DBPatVar
    x -> NLPat -> NLPat -> NLPat -> Elim' NLPat
    forall a. a -> a -> a -> Elim' a
    IApply (Term -> NLPat
    PTerm Term
    u) (Term -> NLPat
    PTerm Term
    v) (NLPat -> Elim' NLPat) -> NLPat -> Elim' NLPat
    forall a b. (a -> b) -> a -> b
    $ Int -> [Arg Int] -> NLPat
    PVar (DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x) []
        DefP PatternInfo
    _ QName
    f NAPs
    ps     -> NLPat -> Elim' NLPat
    app (NLPat -> Elim' NLPat) -> NLPat -> Elim' NLPat
    forall a b. (a -> b) -> a -> b
    $ QName -> PElims -> NLPat
    PDef QName
    f (PElims -> NLPat) -> PElims -> NLPat
    forall a b. (a -> b) -> a -> b
    $ NAPs -> PElims
    forall a b. ToNLPat a b => a -> b
    toNLPat NAPs
    ps

        where
          app :: NLPat -> Elim' NLPat
    app = Arg NLPat -> Elim' NLPat
    forall a. Arg a -> Elim' a
    Apply (Arg NLPat -> Elim' NLPat)
    -> (NLPat -> Arg NLPat) -> NLPat -> Elim' NLPat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ArgInfo -> NLPat -> Arg NLPat
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai

    instance ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) where
      toNLPat :: Arg (Named_ DeBruijnPattern) -> Elim' NLPat
    toNLPat = Arg DeBruijnPattern -> Elim' NLPat
    forall a b. ToNLPat a b => a -> b
    toNLPat (Arg DeBruijnPattern -> Elim' NLPat)
    -> (Arg (Named_ DeBruijnPattern) -> Arg DeBruijnPattern)
    -> Arg (Named_ DeBruijnPattern)
    -> Elim' NLPat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Named_ DeBruijnPattern -> DeBruijnPattern)
    -> Arg (Named_ DeBruijnPattern) -> Arg DeBruijnPattern
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Named_ DeBruijnPattern -> DeBruijnPattern
    forall name a. Named name a -> a
    namedThing