Safe Haskell	Safe-Inferred
Language	Haskell2010

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

data Type
- = Termination
- | Complexity
data RS s r = RS {
- signature :: [s]
- rules :: [Rule r]
- separate :: Bool
}
data Strategy
- = Full
- | Innermost
- | Outermost
class Ord (Var t) => Variables t where
- type Var t
- variables :: t -> Set (Var t)
type TES = TRS Identifier Identifier
data Funcsym = Funcsym {
- fs_name :: Text
- fs_arity :: Int
- fs_theory :: Maybe Theory
- fs_replacementmap :: Maybe Replacementmap
}
data Theory
- = A
- | C
- | AC
data Replacementmap = Replacementmap [Int]
data Signature
- = Signature [Funcsym]
- | HigherOrderSignature
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 Startterm
- = Startterm_Constructor_based
- | Startterm_Full
data Theorydecl v s
- = Property Theory [s]
- | Equations [Rule (Term v s)]
type SES = SRS 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 r -> [Rule r] -> RS s r
module TPDB.Data.Identifier
module TPDB.Data.Term
module TPDB.Data.Rule

Documentation

data Type Source #

Constructors

Termination
Complexity

Instances

Instances details

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

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

Instances details

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) 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, TermC v s) => Variables (TRS v s) Source #
Instance details Defined in TPDB.Data Associated Types type Var (TRS v s) 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 Strategy Source #

Constructors

Full
Innermost
Outermost

Instances

Instances details

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

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

Associated Types

type Var t Source #

Methods

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

Instances

Instances details

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

type TES = TRS Identifier Identifier Source #

legacy stuff (used in matchbox)

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

Instances details

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

data Theory Source #

Constructors

A
C
AC

Instances

Instances details

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

data Replacementmap Source #

Constructors

Replacementmap [Int]

Instances

Instances details

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

Instances details

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

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

type SRS s = RS s [s] Source #

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

Instances details

(TermC s r, 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 #

data Startterm Source #

Constructors

Startterm_Constructor_based
Startterm_Full

Instances

Instances details

Show Startterm Source #
Instance details Defined in TPDB.Data Methods showsPrec :: Int -> Startterm -> ShowS # show :: Startterm -> String # showList :: [Startterm] -> 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)]

type SES = SRS 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 r -> [Rule r] -> RS s r Source #

module TPDB.Data.Identifier

module TPDB.Data.Term

module TPDB.Data.Rule