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