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

module TPDB.DP.Transform
  ( dp, mark, Marked
  , pattern Marked, pattern Original, pattern Auxiliary
  , isOriginal, isMarked, mark_top
  , defined
  ) 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 Mark = Orig
   | Mark
   | Aux -- ^ wat is this?
  deriving (Mark -> Mark -> Bool
(Mark -> Mark -> Bool) -> (Mark -> Mark -> Bool) -> Eq Mark
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Mark -> Mark -> Bool
== :: Mark -> Mark -> Bool
$c/= :: Mark -> Mark -> Bool
/= :: Mark -> Mark -> Bool
Eq, Eq Mark
Eq Mark =>
(Mark -> Mark -> Ordering)
-> (Mark -> Mark -> Bool)
-> (Mark -> Mark -> Bool)
-> (Mark -> Mark -> Bool)
-> (Mark -> Mark -> Bool)
-> (Mark -> Mark -> Mark)
-> (Mark -> Mark -> Mark)
-> Ord Mark
Mark -> Mark -> Bool
Mark -> Mark -> Ordering
Mark -> Mark -> Mark
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
$ccompare :: Mark -> Mark -> Ordering
compare :: Mark -> Mark -> Ordering
$c< :: Mark -> Mark -> Bool
< :: Mark -> Mark -> Bool
$c<= :: Mark -> Mark -> Bool
<= :: Mark -> Mark -> Bool
$c> :: Mark -> Mark -> Bool
> :: Mark -> Mark -> Bool
$c>= :: Mark -> Mark -> Bool
>= :: Mark -> Mark -> Bool
$cmax :: Mark -> Mark -> Mark
max :: Mark -> Mark -> Mark
$cmin :: Mark -> Mark -> Mark
min :: Mark -> Mark -> Mark
Ord, Int -> Mark -> ShowS
[Mark] -> ShowS
Mark -> String
(Int -> Mark -> ShowS)
-> (Mark -> String) -> ([Mark] -> ShowS) -> Show Mark
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Mark -> ShowS
showsPrec :: Int -> Mark -> ShowS
$cshow :: Mark -> String
show :: Mark -> String
$cshowList :: [Mark] -> ShowS
showList :: [Mark] -> ShowS
Show, (forall x. Mark -> Rep Mark x)
-> (forall x. Rep Mark x -> Mark) -> Generic Mark
forall x. Rep Mark x -> Mark
forall x. Mark -> Rep Mark x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Mark -> Rep Mark x
from :: forall x. Mark -> Rep Mark x
$cto :: forall x. Rep Mark x -> Mark
to :: forall x. Rep Mark x -> Mark
Generic)
instance Hashable Mark

data Marked a = Marked_Imp { forall a. Marked a -> a
contents :: !a
                       , forall a. Marked a -> Mark
mark :: !Mark
                       }
    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
$cshowsPrec :: forall a. Show a => Int -> Marked a -> ShowS
showsPrec :: Int -> Marked a -> ShowS
$cshow :: forall a. Show a => Marked a -> String
show :: Marked a -> String
$cshowList :: forall a. Show a => [Marked a] -> ShowS
showList :: [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
$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
/= :: 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
$ccompare :: forall a. Ord a => Marked a -> Marked a -> Ordering
compare :: Marked a -> Marked a -> Ordering
$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
>= :: Marked a -> Marked a -> Bool
$cmax :: forall a. Ord a => Marked a -> Marked a -> Marked a
max :: Marked a -> Marked a -> Marked a
$cmin :: forall a. Ord a => Marked a -> Marked a -> Marked a
min :: Marked a -> Marked a -> 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
$cfrom :: forall a x. Marked a -> Rep (Marked a) x
from :: forall x. Marked a -> Rep (Marked a) x
$cto :: forall a x. Rep (Marked a) x -> Marked a
to :: forall x. Rep (Marked a) x -> Marked a
Generic )

pattern $mMarked :: forall {r} {a}. Marked a -> (a -> r) -> ((# #) -> r) -> r
$bMarked :: forall {a}. a -> Marked a
Marked a = Marked_Imp { mark = Mark, contents = a }
pattern $mOriginal :: forall {r} {a}. Marked a -> (a -> r) -> ((# #) -> r) -> r
$bOriginal :: forall {a}. a -> Marked a
Original a = Marked_Imp { mark = Orig, contents = a }
pattern $mAuxiliary :: forall {r} {a}. Marked a -> (a -> r) -> ((# #) -> r) -> r
$bAuxiliary :: forall {a}. a -> Marked a
Auxiliary a = Marked_Imp { mark = Aux, contents = a }

isOriginal :: Marked a -> Bool
isOriginal Marked a
m = Marked a -> Mark
forall a. Marked a -> Mark
mark Marked a
m Mark -> Mark -> Bool
forall a. Eq a => a -> a -> Bool
== Mark
Orig
isMarked :: Marked a -> Bool
isMarked   Marked a
m = Marked a -> Mark
forall a. Marked a -> Mark
mark Marked a
m Mark -> Mark -> Bool
forall a. Eq a => a -> a -> Bool
== Mark
Mark

instance Hashable a => Hashable (Marked a) 

instance Pretty a => Pretty ( Marked a) where
   pretty :: forall ann. Marked a -> Doc ann
pretty Marked a
m = let p :: Doc ann
p = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Marked a -> a
forall a. Marked a -> a
contents Marked a
m) in case Marked a -> Mark
forall a. Marked a -> Mark
mark Marked a
m of
       Mark
Orig -> Doc ann
forall {ann}. Doc ann
p
       Mark
Mark -> Doc ann
forall {ann}. Doc ann
p Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"#"
       Mark
Aux -> Doc ann
forall {ann}. Doc ann
p

mark_top :: TermC v a => Term v a -> Term v (Marked a)
mark_top :: forall v a. TermC v a => 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 {t} {s} {v}. (t -> s) -> Term v t -> Term v s
tmap 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 a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return a
f

-- | compute the DP transformed system.

dp :: (Eq v, Ord s, TermC v s)
   => RS s (Term v s) 
   -> RS (Marked s) (Term v (Marked s))
dp :: forall v s.
(Eq v, Ord s, TermC v a) =>
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 { relation :: Relation
relation = Relation
Weak
                               , lhs :: Term v (Marked s)
lhs = (s -> Marked s) -> Term v s -> Term v (Marked s)
forall {t} {s} {v}. (t -> s) -> Term v t -> Term v s
tmap 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 {t} {s} {v}. (t -> s) -> Term v t -> Term v s
tmap 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
                               , original_variable :: Maybe Identifier
original_variable = Rule (Term v s) -> Maybe Identifier
forall a. Rule a -> Maybe Identifier
original_variable Rule (Term v s)
u
                               } )
           ([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 = S.fromList $ strict_subterms $ lhs u
                walk :: Term v s -> [Term v s]
walk Term v s
r = if  -- S.member r ssubs
                          Term v s -> Term v s -> Bool
forall v c. (TermC v a, Eq v, Eq c) => Term v c -> Term v c -> Bool
isStrictSubtermOf Term v s
r (Rule (Term v s) -> Term v s
forall a. Rule a -> a
lhs Rule (Term v s)
u)
                         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 a b. [a] -> (a -> [b]) -> [b]
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 a. a -> [a]
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 { relation :: Relation
relation = Relation
Strict
                          , lhs :: Term v (Marked s)
lhs = Term v s -> Term v (Marked s)
forall v a. TermC 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. TermC v a => Term v a -> Term v (Marked a)
mark_top Term v s
r 
                          , top :: Bool
top = Bool
True
                          , original_variable :: Maybe Identifier
original_variable = Rule (Term v s) -> Maybe Identifier
forall a. Rule a -> Maybe Identifier
original_variable Rule (Term v s)
u
                          }
   in 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 
         }