TPDB.Data

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.)

Documentation

data Identifier

Constructors

Identifier

Fields

• _identifier_hash :: !Int
• name :: !String
• arity :: Int

Instances

Eq Identifier

Methods

(==) :: Identifier -> Identifier -> Bool

(/=) :: Identifier -> Identifier -> Bool

Ord Identifier

Methods

compare :: Identifier -> Identifier -> Ordering

(<) :: Identifier -> Identifier -> Bool

(<=) :: Identifier -> Identifier -> Bool

(>) :: Identifier -> Identifier -> Bool

(>=) :: Identifier -> Identifier -> Bool

max :: Identifier -> Identifier -> Identifier

min :: Identifier -> Identifier -> Identifier

Show Identifier

Methods

showsPrec :: Int -> Identifier -> ShowS

show :: Identifier -> String

showList :: [Identifier] -> ShowS

Hashable Identifier

Methods

hashWithSalt :: Int -> Identifier -> Int

hash :: Identifier -> Int

Reader Identifier

Methods

reader :: Parser Identifier

Reader (SRS Identifier)

Methods

reader :: Parser (SRS Identifier)

Reader v => Reader (Term v Identifier)

Methods

reader :: Parser (Term v Identifier)

Reader (TRS Identifier Identifier)

Methods

reader :: Parser (TRS Identifier Identifier)

mk :: Int -> String -> Identifier

data Funcsym

according to XTC spec

Constructors

Funcsym

Fields

• fs_name :: String

  should be Text

• fs_arity :: Int
• fs_theory :: Maybe Theory
• fs_replacementmap :: Maybe Replacementmap

Instances

Show Funcsym

Methods

showsPrec :: Int -> Funcsym -> ShowS

show :: Funcsym -> String

showList :: [Funcsym] -> ShowS

data Signature

Constructors

Signature [Funcsym]

HigherOrderSignature

Instances

Show Signature

Methods

showsPrec :: Int -> Signature -> ShowS

show :: Signature -> String

showList :: [Signature] -> ShowS

data Replacementmap

Constructors

Replacementmap [Int]

Instances

Show Replacementmap

Methods

showsPrec :: Int -> Replacementmap -> ShowS

show :: Replacementmap -> String

showList :: [Replacementmap] -> ShowS

data RS s r

Constructors

RS

Fields

• signature :: [s]

  better keep order in signature (?)

• rules :: [Rule r]
• separate :: Bool

  if True, write comma between rules

Instances

Functor (RS s)

Methods

fmap :: (a -> b) -> RS s a -> RS s b

(<$) :: a -> RS s b -> RS s a

Reader (SRS Identifier)

Methods

reader :: Parser (SRS Identifier)

Eq r => Eq (RS s r)

Methods

(==) :: RS s r -> RS s r -> Bool

(/=) :: RS s r -> RS s r -> Bool

Reader (TRS Identifier Identifier)

Methods

reader :: Parser (TRS Identifier Identifier)

strict_rules :: RS s t -> [(t, t)]

weak_rules :: RS s t -> [(t, t)]

equal_rules :: RS s t -> [(t, t)]

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

type SRS s = RS s [s]

data Problem v s

Constructors

Problem

Fields

• type_ :: Type
• trs :: TRS v s
• strategy :: Maybe Strategy
• full_signature :: Signature
• startterm :: Maybe Startterm
• attributes :: Attributes

data Type

Constructors

Termination

Complexity

Instances

Show Type

Methods

showsPrec :: Int -> Type -> ShowS

show :: Type -> String

showList :: [Type] -> ShowS

data Strategy

Constructors

Full

Innermost

Outermost

Instances

Show Strategy

Methods

showsPrec :: Int -> Strategy -> ShowS

show :: Strategy -> String

showList :: [Strategy] -> ShowS

data Theorydecl v s

this is modelled after https://www.lri.fr/~marche/tpdb/format.html

Constructors

Property Theory [s]

example: "(AC plus)"

Equations [Rule (Term v s)]

data Theory

Constructors

A

C

AC

Instances

Eq Theory

Methods

(==) :: Theory -> Theory -> Bool

(/=) :: Theory -> Theory -> Bool

Ord Theory

Methods

compare :: Theory -> Theory -> Ordering

(<) :: Theory -> Theory -> Bool

(<=) :: Theory -> Theory -> Bool

(>) :: Theory -> Theory -> Bool

(>=) :: Theory -> Theory -> Bool

max :: Theory -> Theory -> Theory

min :: Theory -> Theory -> Theory

Read Theory

Methods

readsPrec :: Int -> ReadS Theory

readList :: ReadS [Theory]

readPrec :: ReadPrec Theory

readListPrec :: ReadPrec [Theory]

Show Theory

Methods

showsPrec :: Int -> Theory -> ShowS

show :: Theory -> String

showList :: [Theory] -> ShowS

data Startterm

Constructors

Startterm_Constructor_based

Startterm_Full

Instances

Show Startterm

Methods

showsPrec :: Int -> Startterm -> ShowS

show :: Startterm -> String

showList :: [Startterm] -> ShowS

type TES = TRS Identifier Identifier

legacy stuff (used in matchbox)

type SES = SRS Identifier

mknullary :: String -> Identifier

mkunary :: String -> Identifier

from_strict_rules :: Bool -> [(t, t)] -> RS i t

with_rules :: RS s r1 -> [Rule r] -> RS s r

module TPDB.Data.Term

module TPDB.Data.Rule