{-# language OverloadedStrings #-}
{-# LANGUAGE DeriveGeneric #-}

module TPDB.DP.Transform  where

import TPDB.Data
import TPDB.Pretty

import qualified Data.Set as S
import Control.Monad ( guard, forM )

import Data.Hashable
import GHC.Generics

data Marked a = Original a | Marked a | Auxiliary a
    deriving ( Int -> Marked a -> ShowS
[Marked a] -> ShowS
Marked a -> String
(Int -> Marked a -> ShowS)
-> (Marked a -> String) -> ([Marked a] -> ShowS) -> Show (Marked a)
forall a. Show a => Int -> Marked a -> ShowS
forall a. Show a => [Marked a] -> ShowS
forall a. Show a => Marked a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Marked a] -> ShowS
$cshowList :: forall a. Show a => [Marked a] -> ShowS
show :: Marked a -> String
$cshow :: forall a. Show a => Marked a -> String
showsPrec :: Int -> Marked a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Marked a -> ShowS
Show, Marked a -> Marked a -> Bool
(Marked a -> Marked a -> Bool)
-> (Marked a -> Marked a -> Bool) -> Eq (Marked a)
forall a. Eq a => Marked a -> Marked a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Marked a -> Marked a -> Bool
$c/= :: forall a. Eq a => Marked a -> Marked a -> Bool
== :: Marked a -> Marked a -> Bool
$c== :: forall a. Eq a => Marked a -> Marked a -> Bool
Eq, Eq (Marked a)
Eq (Marked a)
-> (Marked a -> Marked a -> Ordering)
-> (Marked a -> Marked a -> Bool)
-> (Marked a -> Marked a -> Bool)
-> (Marked a -> Marked a -> Bool)
-> (Marked a -> Marked a -> Bool)
-> (Marked a -> Marked a -> Marked a)
-> (Marked a -> Marked a -> Marked a)
-> Ord (Marked a)
Marked a -> Marked a -> Bool
Marked a -> Marked a -> Ordering
Marked a -> Marked a -> Marked a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Marked a)
forall a. Ord a => Marked a -> Marked a -> Bool
forall a. Ord a => Marked a -> Marked a -> Ordering
forall a. Ord a => Marked a -> Marked a -> Marked a
min :: Marked a -> Marked a -> Marked a
$cmin :: forall a. Ord a => Marked a -> Marked a -> Marked a
max :: Marked a -> Marked a -> Marked a
$cmax :: forall a. Ord a => Marked a -> Marked a -> Marked a
>= :: Marked a -> Marked a -> Bool
$c>= :: forall a. Ord a => Marked a -> Marked a -> Bool
> :: Marked a -> Marked a -> Bool
$c> :: forall a. Ord a => Marked a -> Marked a -> Bool
<= :: Marked a -> Marked a -> Bool
$c<= :: forall a. Ord a => Marked a -> Marked a -> Bool
< :: Marked a -> Marked a -> Bool
$c< :: forall a. Ord a => Marked a -> Marked a -> Bool
compare :: Marked a -> Marked a -> Ordering
$ccompare :: forall a. Ord a => Marked a -> Marked a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Marked a)
Ord, (forall x. Marked a -> Rep (Marked a) x)
-> (forall x. Rep (Marked a) x -> Marked a) -> Generic (Marked a)
forall x. Rep (Marked a) x -> Marked a
forall x. Marked a -> Rep (Marked a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Marked a) x -> Marked a
forall a x. Marked a -> Rep (Marked a) x
$cto :: forall a x. Rep (Marked a) x -> Marked a
$cfrom :: forall a x. Marked a -> Rep (Marked a) x
Generic )

isOriginal :: Marked a -> Bool
isOriginal Marked a
m = case Marked a
m of Original {} -> Bool
True ; Marked a
_ -> Bool
False
isMarked :: Marked a -> Bool
isMarked   Marked a
m = case Marked a
m of Marked   {} -> Bool
True ; Marked a
_ -> Bool
False

instance Hashable a => Hashable (Marked a) 

instance Pretty a => Pretty ( Marked a) where
   pretty :: Marked a -> Doc ann
pretty Marked a
m = case Marked a
m of
       Original a
a -> a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
a
       Marked a
a -> a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
a Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"#"
       Auxiliary a
a -> a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
a

mark_top :: Term v a -> Term v (Marked a)
mark_top :: Term v a -> Term v (Marked a)
mark_top  (Node a
f [Term v a]
args) = 
          Marked a -> [Term v (Marked a)] -> Term v (Marked a)
forall v s. s -> [Term v s] -> Term v s
Node (a -> Marked a
forall a. a -> Marked a
Marked a
f) ([Term v (Marked a)] -> Term v (Marked a))
-> [Term v (Marked a)] -> Term v (Marked a)
forall a b. (a -> b) -> a -> b
$ (Term v a -> Term v (Marked a))
-> [Term v a] -> [Term v (Marked a)]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> Marked a) -> Term v a -> Term v (Marked a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Marked a
forall a. a -> Marked a
Original) [Term v a]
args

defined :: RS s (Term v a) -> Set a
defined RS s (Term v a)
s = [a] -> Set a
forall a. Ord a => [a] -> Set a
S.fromList ([a] -> Set a) -> [a] -> Set a
forall a b. (a -> b) -> a -> b
$ do 
                Rule (Term v a)
u <- RS s (Term v a) -> [Rule (Term v a)]
forall s r. RS s r -> [Rule r]
rules RS s (Term v a)
s
                let Node a
f [Term v a]
args = Rule (Term v a) -> Term v a
forall a. Rule a -> a
lhs Rule (Term v a)
u
                -- will raise exception if lhs is variable
                a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return a
f

-- | compute the DP transformed system.

dp :: (Ord v, Ord s) 
   => RS s (Term v s) 
   -> RS (Marked s) (Term v (Marked s))
dp :: RS s (Term v s) -> RS (Marked s) (Term v (Marked s))
dp RS s (Term v s)
s = 
   let os :: [Rule (Term v (Marked s))]
os = (Rule (Term v s) -> Rule (Term v (Marked s)))
-> [Rule (Term v s)] -> [Rule (Term v (Marked s))]
forall a b. (a -> b) -> [a] -> [b]
map ( \ Rule (Term v s)
u -> Rule :: forall a. a -> a -> Relation -> Bool -> Rule a
Rule { relation :: Relation
relation = Relation
Weak
                               , lhs :: Term v (Marked s)
lhs = (s -> Marked s) -> Term v s -> Term v (Marked s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap s -> Marked s
forall a. a -> Marked a
Original (Term v s -> Term v (Marked s)) -> Term v s -> Term v (Marked s)
forall a b. (a -> b) -> a -> b
$ Rule (Term v s) -> Term v s
forall a. Rule a -> a
lhs Rule (Term v s)
u  
                               , rhs :: Term v (Marked s)
rhs = (s -> Marked s) -> Term v s -> Term v (Marked s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap s -> Marked s
forall a. a -> Marked a
Original (Term v s -> Term v (Marked s)) -> Term v s -> Term v (Marked s)
forall a b. (a -> b) -> a -> b
$ Rule (Term v s) -> Term v s
forall a. Rule a -> a
rhs Rule (Term v s)
u  
                               , top :: Bool
top = Bool
False
                               } )
           ([Rule (Term v s)] -> [Rule (Term v (Marked s))])
-> [Rule (Term v s)] -> [Rule (Term v (Marked s))]
forall a b. (a -> b) -> a -> b
$ RS s (Term v s) -> [Rule (Term v s)]
forall s r. RS s r -> [Rule r]
rules RS s (Term v s)
s
       def :: Set s
def = RS s (Term v s) -> Set s
forall a s v. Ord a => RS s (Term v a) -> Set a
defined RS s (Term v s)
s
       us :: [Rule (Term v (Marked s))]
us = do 
            Rule (Term v s)
u <- RS s (Term v s) -> [Rule (Term v s)]
forall s r. RS s r -> [Rule r]
rules RS s (Term v s)
s
            let ssubs :: Set (Term v s)
ssubs = [Term v s] -> Set (Term v s)
forall a. Ord a => [a] -> Set a
S.fromList ([Term v s] -> Set (Term v s)) -> [Term v s] -> Set (Term v s)
forall a b. (a -> b) -> a -> b
$ Term v s -> [Term v s]
forall v c. Term v c -> [Term v c]
strict_subterms (Term v s -> [Term v s]) -> Term v s -> [Term v s]
forall a b. (a -> b) -> a -> b
$ Rule (Term v s) -> Term v s
forall a. Rule a -> a
lhs Rule (Term v s)
u
                walk :: Term v s -> [Term v s]
walk Term v s
r = if Term v s -> Set (Term v s) -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member Term v s
r Set (Term v s)
ssubs then [] else case Term v s
r of
                    -- will raise exception if rhs contains 
                    -- a variable that is not in lhs
                    Node s
f [Term v s]
args -> 
                        ( if s -> Set s -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member s
f Set s
def then (Term v s
r Term v s -> [Term v s] -> [Term v s]
forall a. a -> [a] -> [a]
:) else [Term v s] -> [Term v s]
forall a. a -> a
id )
                        ( [Term v s]
args [Term v s] -> (Term v s -> [Term v s]) -> [Term v s]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term v s -> [Term v s]
walk )
            Term v s
r <- Term v s -> [Term v s]
walk (Term v s -> [Term v s]) -> Term v s -> [Term v s]
forall a b. (a -> b) -> a -> b
$ Rule (Term v s) -> Term v s
forall a. Rule a -> a
rhs Rule (Term v s)
u
            Rule (Term v (Marked s)) -> [Rule (Term v (Marked s))]
forall (m :: * -> *) a. Monad m => a -> m a
return (Rule (Term v (Marked s)) -> [Rule (Term v (Marked s))])
-> Rule (Term v (Marked s)) -> [Rule (Term v (Marked s))]
forall a b. (a -> b) -> a -> b
$ Rule :: forall a. a -> a -> Relation -> Bool -> Rule a
Rule { relation :: Relation
relation = Relation
Strict
                          , lhs :: Term v (Marked s)
lhs = Term v s -> Term v (Marked s)
forall v a. Term v a -> Term v (Marked a)
mark_top (Term v s -> Term v (Marked s)) -> Term v s -> Term v (Marked s)
forall a b. (a -> b) -> a -> b
$ Rule (Term v s) -> Term v s
forall a. Rule a -> a
lhs Rule (Term v s)
u
                          , rhs :: Term v (Marked s)
rhs = Term v s -> Term v (Marked s)
forall v a. Term v a -> Term v (Marked a)
mark_top Term v s
r 
                          , top :: Bool
top = Bool
True
                          }
   in RS :: forall s r. [s] -> [Rule r] -> Bool -> RS s r
RS { signature :: [Marked s]
signature = (s -> Marked s) -> [s] -> [Marked s]
forall a b. (a -> b) -> [a] -> [b]
map s -> Marked s
forall a. a -> Marked a
Marked ( Set s -> [s]
forall a. Set a -> [a]
S.toList Set s
def )
                     [Marked s] -> [Marked s] -> [Marked s]
forall a. [a] -> [a] -> [a]
++ (s -> Marked s) -> [s] -> [Marked s]
forall a b. (a -> b) -> [a] -> [b]
map s -> Marked s
forall a. a -> Marked a
Original ( RS s (Term v s) -> [s]
forall s r. RS s r -> [s]
signature RS s (Term v s)
s )
         , rules :: [Rule (Term v (Marked s))]
rules = [Rule (Term v (Marked s))]
us [Rule (Term v (Marked s))]
-> [Rule (Term v (Marked s))] -> [Rule (Term v (Marked s))]
forall a. [a] -> [a] -> [a]
++ [Rule (Term v (Marked s))]
os
         , separate :: Bool
separate = RS s (Term v s) -> Bool
forall s r. RS s r -> Bool
separate RS s (Term v s)
s 
         }