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.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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
  forall (m :: * -> *) a b.
Monad m =>
[a] -> (a -> m (Maybe b)) -> m [b]
forMaybeM (forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] [Clause]
cls) forall a b. (a -> b) -> a -> b
$ \(Int
i,Clause
cl) -> do
    QName
clname <- forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> Int -> m QName
clauseQName QName
f Int
i
    forall (m :: * -> *) a. Monad m => a -> m a
return 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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall (m :: * -> *).
MonadFresh NameId m =>
Range -> [Char] -> m Name
freshName forall a. Range' a
noRange (forall a. Pretty a => a -> [Char]
prettyShow a
n forall a. [a] -> [a] -> [a]
++ [Char]
"-clause" forall a. [a] -> [a] -> [a]
++ 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 | NAPs -> Bool
hasDefP (Clause -> NAPs
namedClausePats Clause
cl) = forall a. Maybe a
Nothing
clauseToRewriteRule QName
f QName
q Clause
cl = Clause -> Maybe Term
clauseBody Clause
cl forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \Term
rhs -> RewriteRule
  { rewName :: QName
rewName    = QName
q
  , rewContext :: Telescope
rewContext = Clause -> Telescope
clauseTel Clause
cl
  , rewHead :: QName
rewHead    = QName
f
  , rewPats :: PElims
rewPats    = forall a b. ToNLPat a b => a -> b
toNLPat forall a b. (a -> b) -> a -> b
$ Clause -> NAPs
namedClausePats Clause
cl
  , rewRHS :: Term
rewRHS     = Term
rhs
  , rewType :: Type
rewType    = forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__  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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 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 forall a b. (a -> b) -> a -> b
$ Term -> NLPat
PTerm Term
u
    ConP ConHead
c ConPatternInfo
_ NAPs
ps     -> NLPat -> Elim' NLPat
app forall a b. (a -> b) -> a -> b
$ QName -> PElims -> NLPat
PDef (ConHead -> QName
conName ConHead
c) forall a b. (a -> b) -> a -> b
$ forall a b. ToNLPat a b => a -> b
toNLPat NAPs
ps
    LitP PatternInfo
o Literal
l        -> NLPat -> Elim' NLPat
app forall a b. (a -> b) -> a -> b
$ Term -> NLPat
PTerm forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
l
    ProjP ProjOrigin
o QName
f       -> forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
f
    IApplyP PatternInfo
_ Term
u Term
v DBPatVar
x -> forall a. a -> a -> a -> Elim' a
IApply (Term -> NLPat
PTerm Term
u) (Term -> NLPat
PTerm Term
v) 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 forall a b. (a -> b) -> a -> b
$ QName -> PElims -> NLPat
PDef QName
f forall a b. (a -> b) -> a -> b
$ forall a b. ToNLPat a b => a -> b
toNLPat NAPs
ps

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

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