-- | Data types for rewrite systems and termination problems.
-- A "bare" term rewrite system (list of rules and relative rules) is @TRS v s@.
-- A termination problem is @Problem v s@. This contains a rewrite system plus extra
-- information (strategy, theory, etc.)

{-# language DeriveDataTypeable,
    FlexibleInstances, FlexibleContexts,
    MultiParamTypeClasses, TypeFamilies
#-}

module TPDB.Data 

( module TPDB.Data
, module TPDB.Data.Term
, module TPDB.Data.Rule
)

where


import TPDB.Data.Term
import TPDB.Data.Rule
import TPDB.Data.Attributes

import Data.Typeable
import Control.Monad ( guard )

import Data.Void
import Data.Hashable
import Data.Function (on)
import qualified Data.Text as T
import qualified Data.Set as S

data Identifier =
     Identifier { Identifier -> Int
_identifier_hash :: !Int
                , Identifier -> Text
name :: !T.Text
                , Identifier -> Int
arity :: Int
                }
    deriving ( Identifier -> Identifier -> Bool
(Identifier -> Identifier -> Bool)
-> (Identifier -> Identifier -> Bool) -> Eq Identifier
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Identifier -> Identifier -> Bool
$c/= :: Identifier -> Identifier -> Bool
== :: Identifier -> Identifier -> Bool
$c== :: Identifier -> Identifier -> Bool
Eq, Eq Identifier
Eq Identifier
-> (Identifier -> Identifier -> Ordering)
-> (Identifier -> Identifier -> Bool)
-> (Identifier -> Identifier -> Bool)
-> (Identifier -> Identifier -> Bool)
-> (Identifier -> Identifier -> Bool)
-> (Identifier -> Identifier -> Identifier)
-> (Identifier -> Identifier -> Identifier)
-> Ord Identifier
Identifier -> Identifier -> Bool
Identifier -> Identifier -> Ordering
Identifier -> Identifier -> Identifier
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
min :: Identifier -> Identifier -> Identifier
$cmin :: Identifier -> Identifier -> Identifier
max :: Identifier -> Identifier -> Identifier
$cmax :: Identifier -> Identifier -> Identifier
>= :: Identifier -> Identifier -> Bool
$c>= :: Identifier -> Identifier -> Bool
> :: Identifier -> Identifier -> Bool
$c> :: Identifier -> Identifier -> Bool
<= :: Identifier -> Identifier -> Bool
$c<= :: Identifier -> Identifier -> Bool
< :: Identifier -> Identifier -> Bool
$c< :: Identifier -> Identifier -> Bool
compare :: Identifier -> Identifier -> Ordering
$ccompare :: Identifier -> Identifier -> Ordering
$cp1Ord :: Eq Identifier
Ord, Typeable )

instance Hashable Identifier where
    hashWithSalt :: Int -> Identifier -> Int
hashWithSalt Int
s Identifier
i = (Int, Int) -> Int
forall a. Hashable a => a -> Int
hash (Int
s, Identifier -> Int
_identifier_hash Identifier
i)

instance Show Identifier where show :: Identifier -> String
show = Text -> String
T.unpack (Text -> String) -> (Identifier -> Text) -> Identifier -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identifier -> Text
name

mk :: Int -> T.Text -> Identifier
mk :: Int -> Text -> Identifier
mk Int
a Text
n = Identifier :: Int -> Text -> Int -> Identifier
Identifier { _identifier_hash :: Int
_identifier_hash = (Int, Text) -> Int
forall a. Hashable a => a -> Int
hash (Int
a,Text
n)
                    , arity :: Int
arity = Int
a, name :: Text
name = Text
n }

class Ord (Var t) => Variables t where
  type Var t
  variables :: t -> S.Set (Var t)

instance Ord v => Variables (Term v c) where
  type Var (Term v c) = v
  variables :: Term v c -> Set (Var (Term v c))
variables = Term v c -> Set (Var (Term v c))
forall v c. Ord v => Term v c -> Set v
vars

instance Variables [c] where
  type Var [c] = ()
  variables :: [c] -> Set (Var [c])
variables [c]
_ = Set (Var [c])
forall a. Set a
S.empty

---------------------------------------------------------------------

-- | according to XTC spec
data Funcsym = Funcsym
  { Funcsym -> Text
fs_name :: T.Text
  , Funcsym -> Int
fs_arity :: Int
  , Funcsym -> Maybe Theory
fs_theory :: Maybe Theory
  , Funcsym -> Maybe Replacementmap
fs_replacementmap :: Maybe Replacementmap
  }
  deriving (Int -> Funcsym -> ShowS
[Funcsym] -> ShowS
Funcsym -> String
(Int -> Funcsym -> ShowS)
-> (Funcsym -> String) -> ([Funcsym] -> ShowS) -> Show Funcsym
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Funcsym] -> ShowS
$cshowList :: [Funcsym] -> ShowS
show :: Funcsym -> String
$cshow :: Funcsym -> String
showsPrec :: Int -> Funcsym -> ShowS
$cshowsPrec :: Int -> Funcsym -> ShowS
Show, Typeable)

data Signature = Signature [ Funcsym ]
               | HigherOrderSignature
  deriving (Int -> Signature -> ShowS
[Signature] -> ShowS
Signature -> String
(Int -> Signature -> ShowS)
-> (Signature -> String)
-> ([Signature] -> ShowS)
-> Show Signature
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Signature] -> ShowS
$cshowList :: [Signature] -> ShowS
show :: Signature -> String
$cshow :: Signature -> String
showsPrec :: Int -> Signature -> ShowS
$cshowsPrec :: Int -> Signature -> ShowS
Show, Typeable)

data Replacementmap = Replacementmap [Int]
  deriving (Int -> Replacementmap -> ShowS
[Replacementmap] -> ShowS
Replacementmap -> String
(Int -> Replacementmap -> ShowS)
-> (Replacementmap -> String)
-> ([Replacementmap] -> ShowS)
-> Show Replacementmap
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Replacementmap] -> ShowS
$cshowList :: [Replacementmap] -> ShowS
show :: Replacementmap -> String
$cshow :: Replacementmap -> String
showsPrec :: Int -> Replacementmap -> ShowS
$cshowsPrec :: Int -> Replacementmap -> ShowS
Show, Typeable)

---------------------------------------------------------------------


data RS s r =
     RS { RS s r -> [s]
signature :: [ s ] -- ^ better keep order in signature (?)
        , RS s r -> [Rule r]
rules :: [ Rule r ]
        , RS s r -> Bool
separate :: Bool -- ^ if True, write comma between rules
        }
   deriving ( Typeable )

instance Eq r => Eq (RS s r) where
    == :: RS s r -> RS s r -> Bool
(==) = [Rule r] -> [Rule r] -> Bool
forall a. Eq a => a -> a -> Bool
(==) ([Rule r] -> [Rule r] -> Bool)
-> (RS s r -> [Rule r]) -> RS s r -> RS s r -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` RS s r -> [Rule r]
forall s r. RS s r -> [Rule r]
rules

instance Functor (RS s) where
    fmap :: (a -> b) -> RS s a -> RS s b
fmap a -> b
f RS s a
rs = RS s a
rs { rules :: [Rule b]
rules = (Rule a -> Rule b) -> [Rule a] -> [Rule b]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> b) -> Rule a -> Rule b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) ([Rule a] -> [Rule b]) -> [Rule a] -> [Rule b]
forall a b. (a -> b) -> a -> b
$ RS s a -> [Rule a]
forall s r. RS s r -> [Rule r]
rules RS s a
rs }

strict_rules :: RS s b -> [(b, b)]
strict_rules RS s b
sys =
    do Rule b
u <- RS s b -> [Rule b]
forall s r. RS s r -> [Rule r]
rules RS s b
sys ; Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Rule b -> Bool
forall a. Rule a -> Bool
strict Rule b
u ; (b, b) -> [(b, b)]
forall (m :: * -> *) a. Monad m => a -> m a
return ( Rule b -> b
forall a. Rule a -> a
lhs Rule b
u, Rule b -> b
forall a. Rule a -> a
rhs Rule b
u )
weak_rules :: RS s b -> [(b, b)]
weak_rules RS s b
sys =
    do Rule b
u <- RS s b -> [Rule b]
forall s r. RS s r -> [Rule r]
rules RS s b
sys ; Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Rule b -> Bool
forall a. Rule a -> Bool
weak Rule b
u ; (b, b) -> [(b, b)]
forall (m :: * -> *) a. Monad m => a -> m a
return ( Rule b -> b
forall a. Rule a -> a
lhs Rule b
u, Rule b -> b
forall a. Rule a -> a
rhs Rule b
u )
equal_rules :: RS s b -> [(b, b)]
equal_rules RS s b
sys =
    do Rule b
u <- RS s b -> [Rule b]
forall s r. RS s r -> [Rule r]
rules RS s b
sys ; Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Rule b -> Bool
forall a. Rule a -> Bool
equal Rule b
u ; (b, b) -> [(b, b)]
forall (m :: * -> *) a. Monad m => a -> m a
return ( Rule b -> b
forall a. Rule a -> a
lhs Rule b
u, Rule b -> b
forall a. Rule a -> a
rhs Rule b
u )

type TRS v s = RS s ( Term v s )

type SRS s = RS s [ s ]

instance Variables r => Variables (Rule r) where
  type Var (Rule r) = Var r
  variables :: Rule r -> Set (Var (Rule r))
variables Rule r
u =
    [Set (Var r)] -> Set (Var r)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions [ r -> Set (Var r)
forall t. Variables t => t -> Set (Var t)
variables (Rule r -> r
forall a. Rule a -> a
lhs Rule r
u), r -> Set (Var r)
forall t. Variables t => t -> Set (Var t)
variables (Rule r -> r
forall a. Rule a -> a
rhs Rule r
u) ]

instance Ord v => Variables (TRS v s) where
  type Var (TRS v s) = v
  variables :: TRS v s -> Set (Var (TRS v s))
variables TRS v s
sys = [Set v] -> Set v
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set v] -> Set v) -> [Set v] -> Set v
forall a b. (a -> b) -> a -> b
$ (Rule (Term v s) -> Set v) -> [Rule (Term v s)] -> [Set v]
forall a b. (a -> b) -> [a] -> [b]
map Rule (Term v s) -> Set v
forall t. Variables t => t -> Set (Var t)
variables ([Rule (Term v s)] -> [Set v]) -> [Rule (Term v s)] -> [Set v]
forall a b. (a -> b) -> a -> b
$ TRS v s -> [Rule (Term v s)]
forall s r. RS s r -> [Rule r]
rules TRS v s
sys

instance Variables (SRS s) where
  type Var (SRS s) = Void
  variables :: SRS s -> Set (Var (SRS s))
variables SRS s
sys = Set (Var (SRS s))
forall a. Set a
S.empty

data Problem v s =
     Problem { Problem v s -> Type
type_ :: Type
             , Problem v s -> TRS v s
trs :: TRS v s
             , Problem v s -> Maybe Strategy
strategy :: Maybe Strategy
             , Problem v s -> Signature
full_signature :: Signature
             -- , metainformation :: Metainformation
             , Problem v s -> Maybe Startterm
startterm :: Maybe Startterm
             , Problem v s -> Attributes
attributes :: Attributes
             }

data Type = Termination | Complexity
     deriving Int -> Type -> ShowS
[Type] -> ShowS
Type -> String
(Int -> Type -> ShowS)
-> (Type -> String) -> ([Type] -> ShowS) -> Show Type
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Type] -> ShowS
$cshowList :: [Type] -> ShowS
show :: Type -> String
$cshow :: Type -> String
showsPrec :: Int -> Type -> ShowS
$cshowsPrec :: Int -> Type -> ShowS
Show

data Strategy = Full | Innermost | Outermost
     deriving Int -> Strategy -> ShowS
[Strategy] -> ShowS
Strategy -> String
(Int -> Strategy -> ShowS)
-> (Strategy -> String) -> ([Strategy] -> ShowS) -> Show Strategy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Strategy] -> ShowS
$cshowList :: [Strategy] -> ShowS
show :: Strategy -> String
$cshow :: Strategy -> String
showsPrec :: Int -> Strategy -> ShowS
$cshowsPrec :: Int -> Strategy -> ShowS
Show

-- | this is modelled after
-- https://www.lri.fr/~marche/tpdb/format.html
data Theorydecl v s
  = Property Theory [ s ] -- ^ example: "(AC plus)"
  | Equations [ Rule (Term v s) ]
    deriving Typeable

data Theory = A | C | AC
  deriving (Theory -> Theory -> Bool
(Theory -> Theory -> Bool)
-> (Theory -> Theory -> Bool) -> Eq Theory
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Theory -> Theory -> Bool
$c/= :: Theory -> Theory -> Bool
== :: Theory -> Theory -> Bool
$c== :: Theory -> Theory -> Bool
Eq, Eq Theory
Eq Theory
-> (Theory -> Theory -> Ordering)
-> (Theory -> Theory -> Bool)
-> (Theory -> Theory -> Bool)
-> (Theory -> Theory -> Bool)
-> (Theory -> Theory -> Bool)
-> (Theory -> Theory -> Theory)
-> (Theory -> Theory -> Theory)
-> Ord Theory
Theory -> Theory -> Bool
Theory -> Theory -> Ordering
Theory -> Theory -> Theory
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
min :: Theory -> Theory -> Theory
$cmin :: Theory -> Theory -> Theory
max :: Theory -> Theory -> Theory
$cmax :: Theory -> Theory -> Theory
>= :: Theory -> Theory -> Bool
$c>= :: Theory -> Theory -> Bool
> :: Theory -> Theory -> Bool
$c> :: Theory -> Theory -> Bool
<= :: Theory -> Theory -> Bool
$c<= :: Theory -> Theory -> Bool
< :: Theory -> Theory -> Bool
$c< :: Theory -> Theory -> Bool
compare :: Theory -> Theory -> Ordering
$ccompare :: Theory -> Theory -> Ordering
$cp1Ord :: Eq Theory
Ord, ReadPrec [Theory]
ReadPrec Theory
Int -> ReadS Theory
ReadS [Theory]
(Int -> ReadS Theory)
-> ReadS [Theory]
-> ReadPrec Theory
-> ReadPrec [Theory]
-> Read Theory
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Theory]
$creadListPrec :: ReadPrec [Theory]
readPrec :: ReadPrec Theory
$creadPrec :: ReadPrec Theory
readList :: ReadS [Theory]
$creadList :: ReadS [Theory]
readsPrec :: Int -> ReadS Theory
$creadsPrec :: Int -> ReadS Theory
Read, Int -> Theory -> ShowS
[Theory] -> ShowS
Theory -> String
(Int -> Theory -> ShowS)
-> (Theory -> String) -> ([Theory] -> ShowS) -> Show Theory
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Theory] -> ShowS
$cshowList :: [Theory] -> ShowS
show :: Theory -> String
$cshow :: Theory -> String
showsPrec :: Int -> Theory -> ShowS
$cshowsPrec :: Int -> Theory -> ShowS
Show, Typeable)

data Startterm =
       Startterm_Constructor_based
       | Startterm_Full
     deriving Int -> Startterm -> ShowS
[Startterm] -> ShowS
Startterm -> String
(Int -> Startterm -> ShowS)
-> (Startterm -> String)
-> ([Startterm] -> ShowS)
-> Show Startterm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Startterm] -> ShowS
$cshowList :: [Startterm] -> ShowS
show :: Startterm -> String
$cshow :: Startterm -> String
showsPrec :: Int -> Startterm -> ShowS
$cshowsPrec :: Int -> Startterm -> ShowS
Show

------------------------------------------------------

-- | legacy stuff (used in matchbox)

type TES = TRS Identifier Identifier
type SES = SRS Identifier

mknullary :: Text -> Identifier
mknullary Text
s = Int -> Text -> Identifier
mk Int
0 Text
s
mkunary :: Text -> Identifier
mkunary   Text
s = Int -> Text -> Identifier
mk Int
1 Text
s

from_strict_rules :: Bool -> [(t,t)] -> RS i t
from_strict_rules :: Bool -> [(t, t)] -> RS i t
from_strict_rules Bool
sep [(t, t)]
rs =
    RS :: forall s r. [s] -> [Rule r] -> Bool -> RS s r
RS { rules :: [Rule t]
rules = ((t, t) -> Rule t) -> [(t, t)] -> [Rule t]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (t
l,t
r) ->
             Rule :: forall a. a -> a -> Relation -> Bool -> Rule a
Rule { relation :: Relation
relation = Relation
Strict, top :: Bool
top = Bool
False, lhs :: t
lhs = t
l, rhs :: t
rhs = t
r } ) [(t, t)]
rs
       , separate :: Bool
separate = Bool
sep
       }

with_rules :: RS s r -> [Rule r] -> RS s r
with_rules RS s r
sys [Rule r]
rs = RS s r
sys { rules :: [Rule r]
rules = [Rule r]
rs }