tpdb-1.3.3: Data Type for Rewriting Systems

Safe HaskellSafe
LanguageHaskell98

TPDB.Data

Description

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

Synopsis

Documentation

data Funcsym Source #

according to XTC spec

Constructors

Funcsym 

Instances

data RS s r Source #

Constructors

RS 

Fields

Instances

Functor (RS s) Source # 

Methods

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

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

Reader (SRS Identifier) Source # 
Eq r => Eq (RS s r) Source # 

Methods

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

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

Reader (TRS Identifier Identifier) Source # 

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

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

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

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

type SRS s = RS s [s] Source #

data Type Source #

Constructors

Termination 
Complexity 

Instances

data Theorydecl v s Source #

Constructors

Property Theory [s]

example: "(AC plus)"

Equations [Rule (Term v s)] 

type TES = TRS Identifier Identifier Source #

legacy stuff (used in matchbox)

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

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