Twee.Base

Useful operations on terms and similar. Also re-exports some generally useful modules such as Term and Pretty.

Re-exported functionality

module Twee.Term

module Twee.Pretty

The Symbolic typeclass

class Symbolic a where

Generalisation of term functionality to things that contain terms (e.g., rewrite rules and equations).

Minimal complete definition

termsDL, subst_

Associated Types

type ConstantOf a

Methods

termsDL :: a -> DList (TermListOf a)

Compute a DList of all terms which appear in the argument (used for e.g. computing free variables). See also terms.

subst_ :: (Var -> BuilderOf a) -> a -> a

Apply a substitution. When using the Symbolic type class, you can use subst instead.

Instances

Symbolic a => Symbolic [a]

Associated Types

type ConstantOf [a] :: *

Methods

termsDL :: [a] -> DList (TermListOf [a])

subst_ :: (Var -> BuilderOf [a]) -> [a] -> [a]

Symbolic a => Symbolic (Maybe a)

Associated Types

type ConstantOf (Maybe a) :: *

Methods

termsDL :: Maybe a -> DList (TermListOf (Maybe a))

subst_ :: (Var -> BuilderOf (Maybe a)) -> Maybe a -> Maybe a

Symbolic (Term f)

Associated Types

type ConstantOf (Term f) :: *

Methods

termsDL :: Term f -> DList (TermListOf (Term f))

subst_ :: (Var -> BuilderOf (Term f)) -> Term f -> Term f

Symbolic (TermList f)

Associated Types

type ConstantOf (TermList f) :: *

Methods

termsDL :: TermList f -> DList (TermListOf (TermList f))

subst_ :: (Var -> BuilderOf (TermList f)) -> TermList f -> TermList f

Symbolic (Subst f)

Associated Types

type ConstantOf (Subst f) :: *

Methods

termsDL :: Subst f -> DList (TermListOf (Subst f))

subst_ :: (Var -> BuilderOf (Subst f)) -> Subst f -> Subst f

Symbolic (Equation f)

Associated Types

type ConstantOf (Equation f) :: *

Methods

termsDL :: Equation f -> DList (TermListOf (Equation f))

subst_ :: (Var -> BuilderOf (Equation f)) -> Equation f -> Equation f

Symbolic (Derivation f)

Associated Types

type ConstantOf (Derivation f) :: *

Methods

termsDL :: Derivation f -> DList (TermListOf (Derivation f))

subst_ :: (Var -> BuilderOf (Derivation f)) -> Derivation f -> Derivation f

Symbolic (Resulting f)

Associated Types

type ConstantOf (Resulting f) :: *

Methods

termsDL :: Resulting f -> DList (TermListOf (Resulting f))

subst_ :: (Var -> BuilderOf (Resulting f)) -> Resulting f -> Resulting f

Symbolic (Reduction f)

Associated Types

type ConstantOf (Reduction f) :: *

Methods

termsDL :: Reduction f -> DList (TermListOf (Reduction f))

subst_ :: (Var -> BuilderOf (Reduction f)) -> Reduction f -> Reduction f

Symbolic (Orientation f)

Associated Types

type ConstantOf (Orientation f) :: *

Methods

termsDL :: Orientation f -> DList (TermListOf (Orientation f))

subst_ :: (Var -> BuilderOf (Orientation f)) -> Orientation f -> Orientation f

Symbolic (Rule f)

Associated Types

type ConstantOf (Rule f) :: *

Methods

termsDL :: Rule f -> DList (TermListOf (Rule f))

subst_ :: (Var -> BuilderOf (Rule f)) -> Rule f -> Rule f

Symbolic (CriticalPair f)

Associated Types

type ConstantOf (CriticalPair f) :: *

Methods

termsDL :: CriticalPair f -> DList (TermListOf (CriticalPair f))

subst_ :: (Var -> BuilderOf (CriticalPair f)) -> CriticalPair f -> CriticalPair f

PrettyTerm f => Symbolic (ActiveRule f)

Associated Types

type ConstantOf (ActiveRule f) :: *

Methods

termsDL :: ActiveRule f -> DList (TermListOf (ActiveRule f))

subst_ :: (Var -> BuilderOf (ActiveRule f)) -> ActiveRule f -> ActiveRule f

((~) * (ConstantOf a) (ConstantOf b), Symbolic a, Symbolic b) => Symbolic (a, b)

Associated Types

type ConstantOf (a, b) :: *

Methods

termsDL :: (a, b) -> DList (TermListOf (a, b))

subst_ :: (Var -> BuilderOf (a, b)) -> (a, b) -> (a, b)

((~) * (ConstantOf a) (ConstantOf b), (~) * (ConstantOf a) (ConstantOf c), Symbolic a, Symbolic b, Symbolic c) => Symbolic (a, b, c)

Associated Types

type ConstantOf (a, b, c) :: *

Methods

termsDL :: (a, b, c) -> DList (TermListOf (a, b, c))

subst_ :: (Var -> BuilderOf (a, b, c)) -> (a, b, c) -> (a, b, c)

subst :: (Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) => s -> a -> a

Apply a substitution.

terms :: Symbolic a => a -> [TermListOf a]

Find all terms occuring in the argument.

type TermOf a = Term (ConstantOf a)

A term compatible with a given Symbolic.

type TermListOf a = TermList (ConstantOf a)

A termlist compatible with a given Symbolic.

type SubstOf a = Subst (ConstantOf a)

A substitution compatible with a given Symbolic.

type TriangleSubstOf a = TriangleSubst (ConstantOf a)

A triangle substitution compatible with a given Symbolic.

type BuilderOf a = Builder (ConstantOf a)

A builder compatible with a given Symbolic.

type FunOf a = Fun (ConstantOf a)

The underlying type of function symbols of a given Symbolic.

vars :: Symbolic a => a -> [Var]

Find the variables occurring in the argument.

isGround :: Symbolic a => a -> Bool

Test if the argument is ground.

funs :: Symbolic a => a -> [FunOf a]

Find the function symbols occurring in the argument.

occ :: Symbolic a => FunOf a -> a -> Int

Count how many times a function symbol occurs in the argument.

occVar :: Symbolic a => Var -> a -> Int

Count how many times a variable occurs in the argument.

canonicalise :: Symbolic a => a -> a

Rename the argument so that variables are introduced in a canonical order (starting with V0, then V1 and so on).

renameAvoiding :: (Symbolic a, Symbolic b) => a -> b -> b

Rename the second argument so that it does not mention any variable which occurs in the first.

General-purpose functionality

newtype Id

Represents a unique identifier (e.g., for a rule).

Constructors

Id

Fields

• unId :: Int32

Instances

Bounded Id

Methods

minBound :: Id

maxBound :: Id

Enum Id

Methods

succ :: Id -> Id

pred :: Id -> Id

toEnum :: Int -> Id

fromEnum :: Id -> Int

enumFrom :: Id -> [Id]

enumFromThen :: Id -> Id -> [Id]

enumFromTo :: Id -> Id -> [Id]

enumFromThenTo :: Id -> Id -> Id -> [Id]

Eq Id

Methods

(==) :: Id -> Id -> Bool

(/=) :: Id -> Id -> Bool

Integral Id

Methods

quot :: Id -> Id -> Id

rem :: Id -> Id -> Id

div :: Id -> Id -> Id

mod :: Id -> Id -> Id

quotRem :: Id -> Id -> (Id, Id)

divMod :: Id -> Id -> (Id, Id)

toInteger :: Id -> Integer

Num Id

Methods

(+) :: Id -> Id -> Id

(-) :: Id -> Id -> Id

(*) :: Id -> Id -> Id

negate :: Id -> Id

abs :: Id -> Id

signum :: Id -> Id

fromInteger :: Integer -> Id

Ord Id

Methods

compare :: Id -> Id -> Ordering

(<) :: Id -> Id -> Bool

(<=) :: Id -> Id -> Bool

(>) :: Id -> Id -> Bool

(>=) :: Id -> Id -> Bool

max :: Id -> Id -> Id

min :: Id -> Id -> Id

Real Id

Methods

toRational :: Id -> Rational

Show Id

Methods

showsPrec :: Int -> Id -> ShowS

show :: Id -> String

showList :: [Id] -> ShowS

Pretty Id

Methods

pPrintPrec :: PrettyLevel -> Rational -> Id -> Doc

pPrint :: Id -> Doc

pPrintList :: PrettyLevel -> [Id] -> Doc

Has (ActiveRule f) Id

Methods

the :: ActiveRule f -> Id

class Has a b where

An instance Has a b indicates that a value of type a contains a value of type b which is somehow part of the meaning of the a.

A number of functions use Has constraints to work in a more general setting. For example, the functions in CP operate on rewrite rules, but actually accept any a satisfying Has a (Rule f).

Use taste when definining Has instances; don't do it willy-nilly.

Minimal complete definition

the

Methods

the :: a -> b

Get at the thing.

Instances

Has a a

Methods

the :: a -> a

Has (ActiveRule f) Depth

Methods

the :: ActiveRule f -> Depth

Has (ActiveRule f) RuleId

Methods

the :: ActiveRule f -> RuleId

Has (ActiveRule f) Id

Methods

the :: ActiveRule f -> Id

(~) * f g => Has (Rule f) (Term g)

Methods

the :: Rule f -> Term g

(~) * f g => Has (ActiveRule f) (Positions g)

Methods

the :: ActiveRule f -> Positions g

(~) * f g => Has (ActiveRule f) (Lemma g)

Methods

the :: ActiveRule f -> Lemma g

(~) * f g => Has (ActiveRule f) (Proof g)

Methods

the :: ActiveRule f -> Proof g

(~) * f g => Has (ActiveRule f) (Rule g)

Methods

the :: ActiveRule f -> Rule g

Typeclasses

class Minimal f where

Minimal complete definition

minimal

Methods

minimal :: Fun f

Instances

(Typeable * f, Ord f) => Minimal (Extended f)

Methods

minimal :: Fun (Extended f)

minimalTerm :: Minimal f => Term f

Build the minimal constant as a term.

isMinimal :: Minimal f => Term f -> Bool

Check if a term is the minimal constant.

erase :: (Symbolic a, ConstantOf a ~ f, Minimal f) => [Var] -> a -> a

Erase a given set of variables from the argument, replacing them with the minimal constant.

class Skolem f where

Construction of Skolem constants.

Minimal complete definition

skolem

Methods

skolem :: Var -> Fun f

Turn a variable into a Skolem constant.

Instances

(Typeable * f, Ord f) => Skolem (Extended f)

Methods

skolem :: Var -> Fun (Extended f)

class Arity f where

For types which have a notion of arity.

Minimal complete definition

arity

Methods

arity :: f -> Int

Measure the arity.

Instances

Arity f => Arity (Fun f)

Methods

arity :: Fun f -> Int

Arity f => Arity (Extended f)

Methods

arity :: Extended f -> Int

class Sized a where

For types which have a notion of size.

Minimal complete definition

size

Methods

size :: a -> Int

Compute the size.

Instances

Sized f => Sized (Fun f)

Methods

size :: Fun f -> Int

Sized f => Sized (Term f)

Methods

size :: Term f -> Int

Sized f => Sized (TermList f)

Methods

size :: TermList f -> Int

Sized f => Sized (Extended f)

Methods

size :: Extended f -> Int

Sized f => Sized (Equation f)

Methods

size :: Equation f -> Int

class Ord f => Ordered f where

Minimal complete definition

lessEq, lessIn

Methods

lessEq :: Term f -> Term f -> Bool

Return True if the first term is less than or equal to the second, in the term ordering.

lessIn :: Model f -> Term f -> Term f -> Maybe Strictness

Check if the first term is less than or equal to the second in the given model, and decide whether the inequality is strict or nonstrict.

lessThan :: Ordered f => Term f -> Term f -> Bool

Return True if the first argument is strictly less than the second, in the term ordering.

orientTerms :: Ordered f => Term f -> Term f -> Maybe Ordering

Return the direction in which the terms are oriented according to the term ordering, or Nothing if they cannot be oriented. A result of Just LT means that the first term is less than or equal to the second.

class EqualsBonus f where

A hack for encoding Horn clauses. See Score. The default implementation of hasEqualsBonus should work OK.

Methods

hasEqualsBonus :: f -> Bool

isEquals, isTrue, isFalse :: f -> Bool

Instances

EqualsBonus f => EqualsBonus (Fun f)

Methods

hasEqualsBonus :: Fun f -> Bool

isEquals :: Fun f -> Bool

isTrue :: Fun f -> Bool

isFalse :: Fun f -> Bool

EqualsBonus f => EqualsBonus (Extended f)

Methods

hasEqualsBonus :: Extended f -> Bool

isEquals :: Extended f -> Bool

isTrue :: Extended f -> Bool

isFalse :: Extended f -> Bool

data Strictness

Describes whether an inequality is strict or nonstrict.

Constructors

Strict

The first term is strictly less than the second.

Nonstrict

The first term is less than or equal to the second.

Instances

Eq Strictness

Methods

(==) :: Strictness -> Strictness -> Bool

(/=) :: Strictness -> Strictness -> Bool

Show Strictness

Methods

showsPrec :: Int -> Strictness -> ShowS

show :: Strictness -> String

showList :: [Strictness] -> ShowS

type Function f = (Ordered f, Arity f, Sized f, Minimal f, Skolem f, PrettyTerm f, EqualsBonus f)

The collection of constraints which the type of function symbols must satisfy in order to be used by twee.

data Extended f

A function symbol extended with a minimal constant and Skolem functions. Comes equipped with Minimal and Skolem instances.

Constructors

Minimal

The minimal constant.

Skolem Var

A Skolem function.

Function f

An ordinary function symbol.

Instances

Functor Extended

Methods

fmap :: (a -> b) -> Extended a -> Extended b

(<$) :: a -> Extended b -> Extended a

Eq f => Eq (Extended f)

Methods

(==) :: Extended f -> Extended f -> Bool

(/=) :: Extended f -> Extended f -> Bool

Ord f => Ord (Extended f)

Methods

compare :: Extended f -> Extended f -> Ordering

(<) :: Extended f -> Extended f -> Bool

(<=) :: Extended f -> Extended f -> Bool

(>) :: Extended f -> Extended f -> Bool

(>=) :: Extended f -> Extended f -> Bool

max :: Extended f -> Extended f -> Extended f

min :: Extended f -> Extended f -> Extended f

Show f => Show (Extended f)

Methods

showsPrec :: Int -> Extended f -> ShowS

show :: Extended f -> String

showList :: [Extended f] -> ShowS

Pretty f => Pretty (Extended f)

Methods

pPrintPrec :: PrettyLevel -> Rational -> Extended f -> Doc

pPrint :: Extended f -> Doc

pPrintList :: PrettyLevel -> [Extended f] -> Doc

PrettyTerm f => PrettyTerm (Extended f)

Methods

termStyle :: Extended f -> TermStyle

(Typeable * f, Ord f) => Minimal (Extended f)

Methods

minimal :: Fun (Extended f)

EqualsBonus f => EqualsBonus (Extended f)

Methods

hasEqualsBonus :: Extended f -> Bool

isEquals :: Extended f -> Bool

isTrue :: Extended f -> Bool

isFalse :: Extended f -> Bool

Sized f => Sized (Extended f)

Methods

size :: Extended f -> Int

Arity f => Arity (Extended f)

Methods

arity :: Extended f -> Int

(Typeable * f, Ord f) => Skolem (Extended f)

Methods

skolem :: Var -> Fun (Extended f)