{-# 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
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 ]
, RS s r -> [Rule r]
rules :: [ Rule r ]
, RS s r -> Bool
separate :: Bool
}
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
, 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
data Theorydecl v s
= Property Theory [ s ]
| 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
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 }