{-# 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_hash :: ! Int
, name :: ! T.Text
, arity :: Int
}
deriving ( Eq, Ord, Typeable )
instance Hashable Identifier where
hashWithSalt s i = hash (s, _identifier_hash i)
instance Show Identifier where show = T.unpack . name
mk :: Int -> T.Text -> Identifier
mk a n = Identifier { _identifier_hash = hash (a,n)
, arity = a, name = 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 = vars
instance Variables [c] where
type Var [c] = ()
variables _ = S.empty
data Funcsym = Funcsym
{ fs_name :: T.Text
, fs_arity :: Int
, fs_theory :: Maybe Theory
, fs_replacementmap :: Maybe Replacementmap
}
deriving (Show, Typeable)
data Signature = Signature [ Funcsym ]
| HigherOrderSignature
deriving (Show, Typeable)
data Replacementmap = Replacementmap [Int]
deriving (Show, Typeable)
data RS s r =
RS { signature :: [ s ]
, rules :: [ Rule r ]
, separate :: Bool
}
deriving ( Typeable )
instance Eq r => Eq (RS s r) where
(==) = (==) `on` rules
instance Functor (RS s) where
fmap f rs = rs { rules = map (fmap f) $ rules rs }
strict_rules sys =
do u <- rules sys ; guard $ strict u ; return ( lhs u, rhs u )
weak_rules sys =
do u <- rules sys ; guard $ weak u ; return ( lhs u, rhs u )
equal_rules sys =
do u <- rules sys ; guard $ equal u ; return ( lhs u, rhs 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 u =
S.unions [ variables (lhs u), variables (rhs u) ]
instance Ord v => Variables (TRS v s) where
type Var (TRS v s) = v
variables sys = S.unions $ map variables $ rules sys
instance Variables (SRS s) where
type Var (SRS s) = Void
variables sys = S.empty
data Problem v s =
Problem { type_ :: Type
, trs :: TRS v s
, strategy :: Maybe Strategy
, full_signature :: Signature
, startterm :: Maybe Startterm
, attributes :: Attributes
}
data Type = Termination | Complexity
deriving Show
data Strategy = Full | Innermost | Outermost
deriving Show
data Theorydecl v s
= Property Theory [ s ]
| Equations [ Rule (Term v s) ]
deriving Typeable
data Theory = A | C | AC
deriving (Eq, Ord, Read, Show, Typeable)
data Startterm =
Startterm_Constructor_based
| Startterm_Full
deriving Show
type TES = TRS Identifier Identifier
type SES = SRS Identifier
mknullary s = mk 0 s
mkunary s = mk 1 s
from_strict_rules :: Bool -> [(t,t)] -> RS i t
from_strict_rules sep rs =
RS { rules = map ( \ (l,r) ->
Rule { relation = Strict, top = False, lhs = l, rhs = r } ) rs
, separate = sep
}
with_rules sys rs = sys { rules = rs }