Safe Haskell	Safe
Language	Haskell98

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

type SES = SRS Identifier
type TES = TRS Identifier Identifier
data Startterm
- = Startterm_Constructor_based
- | Startterm_Full
data Theory
- = A
- | C
- | AC
data Theorydecl v s
- = Property Theory [s]
- | Equations [Rule (Term v s)]
data Strategy
- = Full
- | Innermost
- | Outermost
data Type
- = Termination
- | Complexity
data Problem v s = Problem {
- type_ :: Type
- trs :: TRS v s
- strategy :: Maybe Strategy
- full_signature :: Signature
- startterm :: Maybe Startterm
- attributes :: Attributes
}
type SRS s = RS s [s]
type TRS v s = RS s (Term v s)
data RS s r = RS {
- signature :: [s]
- rules :: [Rule r]
- separate :: Bool
}
data Replacementmap = Replacementmap [Int]
data Signature
- = Signature [Funcsym]
- | HigherOrderSignature
data Funcsym = Funcsym {
- fs_name :: Text
- fs_arity :: Int
- fs_theory :: Maybe Theory
- fs_replacementmap :: Maybe Replacementmap
}
class Ord (Var t) => Variables t where
- type Var t
- variables :: t -> Set (Var t)
data Identifier = Identifier {
- _identifier_hash :: !Int
- name :: !Text
- arity :: Int
}
mk :: Int -> Text -> Identifier
strict_rules :: RS s b -> [(b, b)]
weak_rules :: RS s b -> [(b, b)]
equal_rules :: RS s b -> [(b, b)]
mknullary :: Text -> Identifier
mkunary :: Text -> Identifier
from_strict_rules :: Bool -> [(t, t)] -> RS i t
with_rules :: RS s r1 -> [Rule r2] -> RS s r2
module TPDB.Data.Term
module TPDB.Data.Rule

Documentation

type SES = SRS Identifier Source #

type TES = TRS Identifier Identifier Source #

legacy stuff (used in matchbox)

data Startterm Source #

Constructors

Startterm_Constructor_based
Startterm_Full

Instances

Show Startterm Source #
Instance details Defined in TPDB.Data Methods showsPrec :: Int -> Startterm -> ShowS # show :: Startterm -> String # showList :: [Startterm] -> ShowS #

data Theory Source #

Constructors

A
C
AC

Instances

Eq Theory Source #
Instance details Defined in TPDB.Data Methods (==) :: Theory -> Theory -> Bool # (/=) :: Theory -> Theory -> Bool #
Ord Theory Source #
Instance details Defined in TPDB.Data 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 Source #
Instance details Defined in TPDB.Data Methods readsPrec :: Int -> ReadS Theory # readList :: ReadS [Theory] # readPrec :: ReadPrec Theory # readListPrec :: ReadPrec [Theory] #
Show Theory Source #
Instance details Defined in TPDB.Data Methods showsPrec :: Int -> Theory -> ShowS # show :: Theory -> String # showList :: [Theory] -> ShowS #

data Theorydecl v s Source #

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 Strategy Source #

Constructors

Full
Innermost
Outermost

Instances

Show Strategy Source #
Instance details Defined in TPDB.Data Methods showsPrec :: Int -> Strategy -> ShowS # show :: Strategy -> String # showList :: [Strategy] -> ShowS #

data Type Source #

Constructors

Termination
Complexity

Instances

Show Type Source #
Instance details Defined in TPDB.Data Methods showsPrec :: Int -> Type -> ShowS # show :: Type -> String # showList :: [Type] -> ShowS #

data Problem v s Source #

Constructors

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

Instances

(Pretty s, Pretty r, Variables (Term s r)) => Pretty (Problem s r) Source #
Instance details Defined in TPDB.Plain.Write Methods pretty :: Problem s r -> Doc ann # prettyList :: [Problem s r] -> Doc ann #

type SRS s = RS s [s] Source #

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

data RS s r Source #

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) Source #
Instance details Defined in TPDB.Data Methods fmap :: (a -> b) -> RS s a -> RS s b # (<$) :: a -> RS s b -> RS s a #
Variables (SRS s) Source #
Instance details Defined in TPDB.Data Associated Types type Var (SRS s) :: Type Source # Methods variables :: SRS s -> Set (Var (SRS s)) Source #
Reader (SRS Identifier) Source #
Instance details Defined in TPDB.Plain.Read Methods reader :: Parser (SRS Identifier) Source #
Eq r => Eq (RS s r) Source #
Instance details Defined in TPDB.Data Methods (==) :: RS s r -> RS s r -> Bool # (/=) :: RS s r -> RS s r -> Bool #
(Pretty s, PrettyTerm r, Variables (RS s r), Pretty (Var (RS s r))) => Pretty (RS s r) Source #
Instance details Defined in TPDB.Plain.Write Methods pretty :: RS s r -> Doc ann # prettyList :: [RS s r] -> Doc ann #
Ord v => Variables (TRS v s) Source #
Instance details Defined in TPDB.Data Associated Types type Var (TRS v s) :: Type Source # Methods variables :: TRS v s -> Set (Var (TRS v s)) Source #
Reader (TRS Identifier Identifier) Source #
Instance details Defined in TPDB.Plain.Read Methods reader :: Parser (TRS Identifier Identifier) Source #
XmlContent (TRS Identifier Symbol) Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: TRS Identifier Symbol -> [Node] Source # parseContents :: Cursor -> [TRS Identifier Symbol] Source #
type Var (SRS s) Source #
Instance details Defined in TPDB.Data type Var (SRS s) = Void
type Var (TRS v s) Source #
Instance details Defined in TPDB.Data type Var (TRS v s) = v

data Replacementmap Source #

Constructors

Replacementmap [Int]

Instances

Show Replacementmap Source #
Instance details Defined in TPDB.Data Methods showsPrec :: Int -> Replacementmap -> ShowS # show :: Replacementmap -> String # showList :: [Replacementmap] -> ShowS #

data Signature Source #

Constructors

Signature [Funcsym]
HigherOrderSignature

Instances

Show Signature Source #
Instance details Defined in TPDB.Data Methods showsPrec :: Int -> Signature -> ShowS # show :: Signature -> String # showList :: [Signature] -> ShowS #

data Funcsym Source #

according to XTC spec

Constructors

Funcsym
Fields fs_name :: Text fs_arity :: Int fs_theory :: Maybe Theory fs_replacementmap :: Maybe Replacementmap

Instances

Show Funcsym Source #
Instance details Defined in TPDB.Data Methods showsPrec :: Int -> Funcsym -> ShowS # show :: Funcsym -> String # showList :: [Funcsym] -> ShowS #

class Ord (Var t) => Variables t where Source #

Associated Types

type Var t Source #

Methods

variables :: t -> Set (Var t) Source #

Instances

Variables [c] Source #
Instance details Defined in TPDB.Data Associated Types type Var [c] :: Type Source # Methods variables :: [c] -> Set (Var [c]) Source #
Variables r => Variables (Rule r) Source #
Instance details Defined in TPDB.Data Associated Types type Var (Rule r) :: Type Source # Methods variables :: Rule r -> Set (Var (Rule r)) Source #
Variables (SRS s) Source #
Instance details Defined in TPDB.Data Associated Types type Var (SRS s) :: Type Source # Methods variables :: SRS s -> Set (Var (SRS s)) Source #
Ord v => Variables (Term v c) Source #
Instance details Defined in TPDB.Data Associated Types type Var (Term v c) :: Type Source # Methods variables :: Term v c -> Set (Var (Term v c)) Source #
Ord v => Variables (TRS v s) Source #
Instance details Defined in TPDB.Data Associated Types type Var (TRS v s) :: Type Source # Methods variables :: TRS v s -> Set (Var (TRS v s)) Source #

data Identifier Source #

Constructors

Identifier
Fields _identifier_hash :: !Int name :: !Text arity :: Int

Instances

Eq Identifier Source #
Instance details Defined in TPDB.Data Methods (==) :: Identifier -> Identifier -> Bool # (/=) :: Identifier -> Identifier -> Bool #
Ord Identifier Source #
Instance details Defined in TPDB.Data 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 Source #
Instance details Defined in TPDB.Data Methods showsPrec :: Int -> Identifier -> ShowS # show :: Identifier -> String # showList :: [Identifier] -> ShowS #
Hashable Identifier Source #
Instance details Defined in TPDB.Data Methods hashWithSalt :: Int -> Identifier -> Int # hash :: Identifier -> Int #
Pretty Identifier Source #
Instance details Defined in TPDB.Plain.Write Methods pretty :: Identifier -> Doc ann # prettyList :: [Identifier] -> Doc ann #
Reader Identifier Source #
Instance details Defined in TPDB.Plain.Read Methods reader :: Parser Identifier Source #
XmlContent Identifier Source #	FIXME: move to separate module
Instance details Defined in TPDB.Data.Xml Methods toContents :: Identifier -> [Node] Source # parseContents :: Cursor -> [Identifier] Source #
Reader (SRS Identifier) Source #
Instance details Defined in TPDB.Plain.Read Methods reader :: Parser (SRS Identifier) Source #
Reader v => Reader (Term v Identifier) Source #
Instance details Defined in TPDB.Plain.Read Methods reader :: Parser (Term v Identifier) Source #
Reader (TRS Identifier Identifier) Source #
Instance details Defined in TPDB.Plain.Read Methods reader :: Parser (TRS Identifier Identifier) Source #
XmlContent (TRS Identifier Symbol) Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: TRS Identifier Symbol -> [Node] Source # parseContents :: Cursor -> [TRS Identifier Symbol] Source #

mk :: Int -> Text -> Identifier Source #

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

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

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

mknullary :: Text -> Identifier Source #

mkunary :: Text -> Identifier Source #

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

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

module TPDB.Data.Term

module TPDB.Data.Rule