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 Theory
- = A
- | C
- | AC
data Theorydecl v s
- = Property Theory [s]
- | Equations [Rule (Term v s)]
data Type
- = Termination
- | Complexity
data RS s r = RS {
- signature :: [s]
- rules :: [Rule r]
- separate :: Bool
}
data Problem v s = Problem {
- type_ :: Type
- trs :: TRS v s
- strategy :: Maybe Strategy
- full_signature :: Signature
- startterm :: Maybe Startterm
- attributes :: Attributes
}
data Strategy
- = Full
- | Innermost
- | Outermost
class Ord (Var t) => Variables t where
- type Var t
- variables :: t -> Set (Var t)
type family 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 Replacementmap = Replacementmap [Int]
data Signature
- = Signature [Funcsym]
- | HigherOrderSignature
strict_rules :: RS s b -> [(b, b)]
weak_rules :: RS s b -> [(b, b)]
equal_rules :: RS s b -> [(b, b)]
type TRS v s = RS s (Term v s)
type SRS s = RS s [s]
data Startterm
- = Startterm_Constructor_based
- | Startterm_Full
type SES = SRS Identifier
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.Identifier
module TPDB.Data.Term
module TPDB.Data.Rule

Documentation

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 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 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)
Instance details Defined in TPDB.Data type Var (SRS s) = Void

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)
Instance details Defined in TPDB.Data type Var (TRS v s) = v

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 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 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)
Instance details Defined in TPDB.Data type Var (SRS s) = Void

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)
Instance details Defined in TPDB.Data type Var (Rule r) = Var r

Methods

variables :: Rule r -> Set (Var (Rule r)) Source #

Variables [c] Source #

Instance details

Defined in TPDB.Data

Associated Types

type Var [c]
Instance details Defined in TPDB.Data type Var [c] = ()

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)
Instance details Defined in TPDB.Data type Var (TRS v s) = v

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)
Instance details Defined in TPDB.Data type Var (Term v c) = v

Methods

variables :: Term v c -> Set (Var (Term v c)) Source #

type family Var t Source #

Instances

Instances details

type Var (SRS s) Source #
Instance details Defined in TPDB.Data type Var (SRS s) = Void
type Var (Rule r) Source #
Instance details Defined in TPDB.Data type Var (Rule r) = Var r
type Var [c] Source #
Instance details Defined in TPDB.Data type Var [c] = ()
type Var (TRS v s) Source #
Instance details Defined in TPDB.Data type Var (TRS v s) = v
type Var (Term v c) Source #
Instance details Defined in TPDB.Data type Var (Term v c) = v

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

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

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

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

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

type SRS s = RS s [s] Source #

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 #

type SES = SRS Identifier 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.Identifier

module TPDB.Data.Term

module TPDB.Data.Rule