    module Agda.TypeChecking.Rewriting.Clause where

    import Data.Maybe

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

    import Agda.TypeChecking.Monad

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

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

    -- | Get all the clauses of a definition and convert them to rewrite
    --   rules.
    getClausesAsRewriteRules :: (HasConstInfo m, MonadFresh NameId m) => QName -> m [RewriteRule]
    getClausesAsRewriteRules :: forall (m :: * -> *).
    (HasConstInfo m, MonadFresh NameId m) =>
    QName -> m [RewriteRule]
    getClausesAsRewriteRules QName
    f = do
      [Clause]
    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
      [(Int, Clause)]
    -> ((Int, Clause) -> m (Maybe RewriteRule)) -> m [RewriteRule]
    forall (m :: * -> *) a b.
    Monad m =>
    [a] -> (a -> m (Maybe b)) -> m [b]
    forMaybeM ([Int] -> [Clause] -> [(Int, Clause)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int
    1..] [Clause]
    cls) (((Int, Clause) -> m (Maybe RewriteRule)) -> m [RewriteRule])
    -> ((Int, Clause) -> m (Maybe RewriteRule)) -> m [RewriteRule]
    forall a b. (a -> b) -> a -> b
    $ \(Int
    i,Clause
    cl) -> do
        QName
    clname <- QName -> Int -> m QName
    forall (m :: * -> *).
    (HasConstInfo m, MonadFresh NameId m) =>
    QName -> Int -> m QName
    clauseQName QName
    f Int
    i
        Maybe RewriteRule -> m (Maybe RewriteRule)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe RewriteRule -> m (Maybe RewriteRule))
    -> Maybe RewriteRule -> m (Maybe RewriteRule)
    forall a b. (a -> b) -> a -> b
    $ QName -> QName -> Clause -> Maybe RewriteRule
    clauseToRewriteRule QName
    f QName
    clname Clause
    cl

    -- | 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)

    -- | @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 :: QName -> QName -> Clause -> Maybe RewriteRule
    clauseToRewriteRule :: QName -> QName -> Clause -> Maybe RewriteRule
    clauseToRewriteRule QName
    f QName
    q Clause
    cl = Clause -> Maybe Term
    clauseBody Clause
    cl Maybe Term -> (Term -> RewriteRule) -> Maybe RewriteRule
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \Term
    rhs -> RewriteRule :: QName
    -> Telescope
    -> QName
    -> PElims
    -> Term
    -> Type
    -> Bool
    -> RewriteRule
    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
      }

    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 (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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Named_ DeBruijnPattern -> DeBruijnPattern
    forall name a. Named name a -> a
    namedThing