Safe Haskell | Safe |
---|---|
Language | Haskell98 |
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.)
- data Identifier = Identifier {}
- mk :: Int -> String -> Identifier
- data Funcsym = Funcsym {}
- data Signature
- data Replacementmap = Replacementmap [Int]
- data RS s r = RS {}
- 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 = Problem {
- type_ :: Type
- trs :: TRS v s
- strategy :: Maybe Strategy
- full_signature :: Signature
- startterm :: Maybe Startterm
- attributes :: Attributes
- data Type
- data Strategy
- data Theorydecl v s
- data Theory
- data Startterm
- type TES = TRS Identifier Identifier
- 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
Documentation
data Identifier Source #
according to XTC spec
strict_rules :: RS s t -> [(t, t)] Source #
weak_rules :: RS s t -> [(t, t)] Source #
equal_rules :: RS s t -> [(t, t)] Source #
Problem | |
|
data Theorydecl v s Source #
this is modelled after https://www.lri.fr/~marche/tpdb/format.html
type TES = TRS Identifier Identifier Source #
legacy stuff (used in matchbox)
type SES = SRS Identifier Source #
mknullary :: String -> Identifier Source #
mkunary :: String -> Identifier Source #
from_strict_rules :: Bool -> [(t, t)] -> RS i t Source #
module TPDB.Data.Term
module TPDB.Data.Rule