Twee.Base

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

Re-exported functionality

data Builder f

A monoid for building terms. mempty represents the empty termlist, while mappend appends two termlists.

Instances

Semigroup (Builder f)

Defined in Twee.Term.Core

Methods

(<>) :: Builder f -> Builder f -> Builder f

sconcat :: NonEmpty (Builder f) -> Builder f

stimes :: Integral b => b -> Builder f -> Builder f

Monoid (Builder f)

Defined in Twee.Term.Core

Methods

mempty :: Builder f

mappend :: Builder f -> Builder f -> Builder f

mconcat :: [Builder f] -> Builder f

Build (Builder f)

Defined in Twee.Term

Associated Types

type BuildFun (Builder f) :: Type

Methods

builder :: Builder f -> Builder (BuildFun (Builder f))

type BuildFun (Builder f)

Defined in Twee.Term

type BuildFun (Builder f) = f

newtype Var

A variable.

Constructors

V

Fields

• var_id :: Int

  The variable's number. Don't use huge variable numbers: they will be truncated to 32 bits when stored in a term.

Instances

Enum Var

Defined in Twee.Term.Core

Methods

succ :: Var -> Var

pred :: Var -> Var

toEnum :: Int -> Var

fromEnum :: Var -> Int

enumFrom :: Var -> [Var]

enumFromThen :: Var -> Var -> [Var]

enumFromTo :: Var -> Var -> [Var]

enumFromThenTo :: Var -> Var -> Var -> [Var]

Eq Var

Defined in Twee.Term.Core

Methods

(==) :: Var -> Var -> Bool

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

Ord Var

Defined in Twee.Term.Core

Methods

compare :: Var -> Var -> Ordering

(<) :: Var -> Var -> Bool

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

(>) :: Var -> Var -> Bool

(>=) :: Var -> Var -> Bool

max :: Var -> Var -> Var

min :: Var -> Var -> Var

Show Var

Defined in Twee.Term.Core

Methods

showsPrec :: Int -> Var -> ShowS

show :: Var -> String

showList :: [Var] -> ShowS

Pretty Var

Defined in Twee.Pretty

Methods

pPrintPrec :: PrettyLevel -> Rational -> Var -> Doc

pPrint :: Var -> Doc

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

data Fun f

A function symbol. f is the underlying type of function symbols defined by the user; Fun f is an f together with an automatically-generated unique number.

Instances

Eq (Fun f)

Defined in Twee.Term.Core

Methods

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

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

Ord (Fun f)

Defined in Twee.Term.Core

Methods

compare :: Fun f -> Fun f -> Ordering

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

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

(>) :: Fun f -> Fun f -> Bool

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

max :: Fun f -> Fun f -> Fun f

min :: Fun f -> Fun f -> Fun f

Show (Fun f)

Defined in Twee.Term.Core

Methods

showsPrec :: Int -> Fun f -> ShowS

show :: Fun f -> String

showList :: [Fun f] -> ShowS

Pretty f => Pretty (Fun f)

Defined in Twee.Pretty

Methods

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

pPrint :: Fun f -> Doc

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

PrettyTerm f => PrettyTerm (Fun f)

Defined in Twee.Pretty

Methods

termStyle :: Fun f -> TermStyle

EqualsBonus f => EqualsBonus (Fun f)

Defined in Twee.Base

Methods

hasEqualsBonus :: Fun f -> Bool

isEquals :: Fun f -> Bool

isTrue :: Fun f -> Bool

isFalse :: Fun f -> Bool

Sized f => Sized (Fun f)

Defined in Twee.Base

Methods

size :: Fun f -> Int

Arity f => Arity (Fun f)

Defined in Twee.Base

Methods

arity :: Fun f -> Int

data Term f

Term f is a term whose function symbols have type f. It is either a Var or an App.

Instances

Eq (Term f)

Defined in Twee.Term.Core

Methods

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

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

Ord (Term f)

Defined in Twee.Term.Core

Methods

compare :: Term f -> Term f -> Ordering

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

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

(>) :: Term f -> Term f -> Bool

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

max :: Term f -> Term f -> Term f

min :: Term f -> Term f -> Term f

Show (Term f)

Defined in Twee.Term

Methods

showsPrec :: Int -> Term f -> ShowS

show :: Term f -> String

showList :: [Term f] -> ShowS

PrettyTerm f => Pretty (Term f)

Defined in Twee.Pretty

Methods

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

pPrint :: Term f -> Doc

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

Build (Term f)

Defined in Twee.Term

Associated Types

type BuildFun (Term f) :: Type

Methods

builder :: Term f -> Builder (BuildFun (Term f))

Sized f => Sized (Term f)

Defined in Twee.Base

Methods

size :: Term f -> Int

Symbolic (Term f)

Defined in Twee.Base

Associated Types

type ConstantOf (Term f) :: Type

Methods

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

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

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

Defined in Twee.Rule

Methods

the :: Rule f -> Term g

type BuildFun (Term f)

Defined in Twee.Term

type BuildFun (Term f) = f

type ConstantOf (Term f)

Defined in Twee.Base

type ConstantOf (Term f) = f

data TermList f

TermList f is a list of terms whose function symbols have type f. It is either a Cons or an Empty. You can turn it into a [Term f] with unpack.

Instances

Eq (TermList f)

Defined in Twee.Term.Core

Methods

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

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

Ord (TermList f)

Defined in Twee.Term.Core

Methods

compare :: TermList f -> TermList f -> Ordering

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

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

(>) :: TermList f -> TermList f -> Bool

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

max :: TermList f -> TermList f -> TermList f

min :: TermList f -> TermList f -> TermList f

Show (TermList f)

Defined in Twee.Term

Methods

showsPrec :: Int -> TermList f -> ShowS

show :: TermList f -> String

showList :: [TermList f] -> ShowS

PrettyTerm f => Pretty (TermList f)

Defined in Twee.Pretty

Methods

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

pPrint :: TermList f -> Doc

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

Build (TermList f)

Defined in Twee.Term

Associated Types

type BuildFun (TermList f) :: Type

Methods

builder :: TermList f -> Builder (BuildFun (TermList f))

Sized f => Sized (TermList f)

Defined in Twee.Base

Methods

size :: TermList f -> Int

Symbolic (TermList f)

Defined in Twee.Base

Associated Types

type ConstantOf (TermList f) :: Type

Methods

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

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

type BuildFun (TermList f)

Defined in Twee.Term

type BuildFun (TermList f) = f

type ConstantOf (TermList f)

Defined in Twee.Base

type ConstantOf (TermList f) = f

pattern App :: Fun f -> TermList f -> Term f

Matches a function application.

pattern Var :: Var -> Term f

Matches a variable.

pattern UnsafeConsSym :: Term f -> TermList f -> TermList f

Like ConsSym, but does not check that the termlist is non-empty. Use only if you are sure the termlist is non-empty.

pattern ConsSym :: Term f -> TermList f -> TermList f

Matches a non-empty termlist, unpacking it into head and everything except the root symbol of the head. Useful for iterating through terms one symbol at a time.

For example, if ts is the termlist [f(x,y), g(z)], then let ConsSym u us = ts results in the following bindings:

u  = f(x,y)
us = [x, y, g(z)]

pattern UnsafeCons :: Term f -> TermList f -> TermList f

Like Cons, but does not check that the termlist is non-empty. Use only if you are sure the termlist is non-empty.

pattern Cons :: Term f -> TermList f -> TermList f

Matches a non-empty termlist, unpacking it into head and tail.

pattern Empty :: TermList f

Matches the empty termlist.

at :: Int -> TermList f -> Term f

Index into a termlist.

lenList :: TermList f -> Int

The length of (number of symbols in) a termlist.

fun :: (Ord f, Typeable f) => f -> Fun f

Construct a Fun from a function symbol.

fun_value :: Fun f -> f

The underlying function symbol of a Fun.

singleton :: Term f -> TermList f

Convert a term to a termlist.

isSubtermOfList :: Term f -> TermList f -> Bool

Is a term contained as a subterm in a given termlist?

newtype TriangleSubst f

A triangle substitution is one in which variables can be defined in terms of each other, though not in a circular way.

The main use of triangle substitutions is in unification; unifyTri returns one. A triangle substitution can be converted to an ordinary substitution with close, or used directly using its Substitution instance.

Constructors

Triangle

Fields

• unTriangle :: Subst f

Instances

Show (TriangleSubst f)

Defined in Twee.Term

Methods

showsPrec :: Int -> TriangleSubst f -> ShowS

show :: TriangleSubst f -> String

showList :: [TriangleSubst f] -> ShowS

Substitution (TriangleSubst f)

Defined in Twee.Term

Associated Types

type SubstFun (TriangleSubst f) :: Type

Methods

evalSubst :: TriangleSubst f -> Var -> Builder (SubstFun (TriangleSubst f))

substList :: TriangleSubst f -> TermList (SubstFun (TriangleSubst f)) -> Builder (SubstFun (TriangleSubst f))

type SubstFun (TriangleSubst f)

Defined in Twee.Term

type SubstFun (TriangleSubst f) = f

newtype Subst f

A substitution which maps variables to terms of type Term f.

Constructors

Subst

Fields

• unSubst :: IntMap (TermList f)

Instances

Eq (Subst f)

Defined in Twee.Term

Methods

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

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

Show (Subst f)

Defined in Twee.Term

Methods

showsPrec :: Int -> Subst f -> ShowS

show :: Subst f -> String

showList :: [Subst f] -> ShowS

PrettyTerm f => Pretty (Subst f)

Defined in Twee.Pretty

Methods

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

pPrint :: Subst f -> Doc

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

Substitution (Subst f)

Defined in Twee.Term

Associated Types

type SubstFun (Subst f) :: Type

Methods

evalSubst :: Subst f -> Var -> Builder (SubstFun (Subst f))

substList :: Subst f -> TermList (SubstFun (Subst f)) -> Builder (SubstFun (Subst f))

Symbolic (Subst f)

Defined in Twee.Base

Associated Types

type ConstantOf (Subst f) :: Type

Methods

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

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

type SubstFun (Subst f)

Defined in Twee.Term

type SubstFun (Subst f) = f

type ConstantOf (Subst f)

Defined in Twee.Base

type ConstantOf (Subst f) = f

class Substitution s where

A class for values which act as substitutions.

Instances include Subst as well as functions from variables to terms.

Minimal complete definition

evalSubst

Associated Types

type SubstFun s

The underlying type of function symbols.

Methods

evalSubst :: s -> Var -> Builder (SubstFun s)

Apply the substitution to a variable.

substList :: s -> TermList (SubstFun s) -> Builder (SubstFun s)

Apply the substitution to a termlist.

Instances

Substitution (TriangleSubst f)

Defined in Twee.Term

Associated Types

type SubstFun (TriangleSubst f) :: Type

Methods

evalSubst :: TriangleSubst f -> Var -> Builder (SubstFun (TriangleSubst f))

substList :: TriangleSubst f -> TermList (SubstFun (TriangleSubst f)) -> Builder (SubstFun (TriangleSubst f))

Substitution (Subst f)

Defined in Twee.Term

Associated Types

type SubstFun (Subst f) :: Type

Methods

evalSubst :: Subst f -> Var -> Builder (SubstFun (Subst f))

substList :: Subst f -> TermList (SubstFun (Subst f)) -> Builder (SubstFun (Subst f))

(Build a, v ~ Var) => Substitution (v -> a)

Defined in Twee.Term

Associated Types

type SubstFun (v -> a) :: Type

Methods

evalSubst :: (v -> a) -> Var -> Builder (SubstFun (v -> a))

substList :: (v -> a) -> TermList (SubstFun (v -> a)) -> Builder (SubstFun (v -> a))

class Build a where

Instances of Build can be turned into terms using build or buildList, and turned into term builders using builder. Has instances for terms, termlists, builders, and Haskell lists.

Associated Types

type BuildFun a

The underlying type of function symbols.

Methods

builder :: a -> Builder (BuildFun a)

Convert a value into a Builder.

Instances

Build a => Build [a]

Defined in Twee.Term

Associated Types

type BuildFun [a] :: Type

Methods

builder :: [a] -> Builder (BuildFun [a])

Build (Builder f)

Defined in Twee.Term

Associated Types

type BuildFun (Builder f) :: Type

Methods

builder :: Builder f -> Builder (BuildFun (Builder f))

Build (Term f)

Defined in Twee.Term

Associated Types

type BuildFun (Term f) :: Type

Methods

builder :: Term f -> Builder (BuildFun (Term f))

Build (TermList f)

Defined in Twee.Term

Associated Types

type BuildFun (TermList f) :: Type

Methods

builder :: TermList f -> Builder (BuildFun (TermList f))

pattern F :: f -> Fun f

A pattern which extracts the fun_value from a Fun.

build :: Build a => a -> Term (BuildFun a)

Build a term. The given builder must produce exactly one term.

buildList :: Build a => a -> TermList (BuildFun a)

Build a termlist.

con :: Fun f -> Builder f

Build a constant (a function with no arguments).

app :: Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)

Build a function application.

var :: Var -> Builder f

Build a variable.

substToList :: Subst f -> [(Var, Term f)]

Convert a substitution to a list of bindings.

foldSubst :: (Var -> TermList f -> b -> b) -> b -> Subst f -> b

Fold a function over a substitution.

allSubst :: (Var -> TermList f -> Bool) -> Subst f -> Bool

Check if all bindings of a substitution satisfy a given property.

substDomain :: Subst f -> [Var]

Compute the set of variables bound by a substitution.

substSize :: Subst f -> Int

Return the highest-number variable in a substitution plus 1.

lookupList :: Var -> Subst f -> Maybe (TermList f)

Look up a variable in a substitution, returning a termlist.

extendList :: Var -> TermList f -> Subst f -> Maybe (Subst f)

Add a new binding to a substitution, giving a termlist.

retract :: Var -> Subst f -> Subst f

Remove a binding from a substitution.

unsafeExtendList :: Var -> TermList f -> Subst f -> Subst f

Add a new binding to a substitution. Overwrites any existing binding.

substCompose :: Substitution s => Subst (SubstFun s) -> s -> Subst (SubstFun s)

Compose two substitutions.

substCompatible :: Subst f -> Subst f -> Bool

Check if two substitutions are compatible (they do not send the same variable to different terms).

substUnion :: Subst f -> Subst f -> Subst f

Take the union of two substitutions. The substitutions must be compatible, which is not checked.

idempotent :: Subst f -> Bool

Check if a substitution is idempotent (applying it twice has the same effect as applying it once).

idempotentOn :: Subst f -> TermList f -> Bool

Check if a substitution has no effect on a given term.

close :: TriangleSubst f -> Subst f

Iterate a triangle substitution to make it idempotent.

emptySubst :: Subst f

The empty substitution.

listToSubst :: [(Var, Term f)] -> Maybe (Subst f)

Construct a substitution from a list. Returns Nothing if a variable is bound to several different terms.

match :: Term f -> Term f -> Maybe (Subst f)

match pat t matches the term t against the pattern pat.

matchIn :: Subst f -> Term f -> Term f -> Maybe (Subst f)

A variant of match which extends an existing substitution.

matchList :: TermList f -> TermList f -> Maybe (Subst f)

A variant of match which works on termlists.

matchListIn :: Subst f -> TermList f -> TermList f -> Maybe (Subst f)

A variant of match which works on termlists and extends an existing substitution.

unify :: Term f -> Term f -> Maybe (Subst f)

Unify two terms.

unifyList :: TermList f -> TermList f -> Maybe (Subst f)

Unify two termlists.

unifyTri :: Term f -> Term f -> Maybe (TriangleSubst f)

Unify two terms, returning a triangle substitution. This is slightly faster than unify.

unifyListTri :: TermList f -> TermList f -> Maybe (TriangleSubst f)

Unify two termlists, returning a triangle substitution. This is slightly faster than unify.

unifyListTriFrom :: TermList f -> TermList f -> TriangleSubst f -> Maybe (TriangleSubst f)

empty :: forall f. TermList f

The empty termlist.

children :: Term f -> TermList f

Get the children (direct subterms) of a term.

unpack :: TermList f -> [Term f]

Convert a termlist into an ordinary list of terms.

lookup :: Var -> Subst f -> Maybe (Term f)

Look up a variable in a substitution.

extend :: Var -> Term f -> Subst f -> Maybe (Subst f)

Add a new binding to a substitution.

len :: Term f -> Int

Find the length of a term.

bound :: Term f -> (Var, Var)

Return the lowest- and highest-numbered variables in a term.

boundList :: TermList f -> (Var, Var)

Return the lowest- and highest-numbered variables in a termlist.

boundLists :: [TermList f] -> (Var, Var)

Return the lowest- and highest-numbered variables in a list of termlists.

occurs :: Var -> Term f -> Bool

Check if a variable occurs in a term.

subtermsList :: TermList f -> [Term f]

Find all subterms of a termlist.

subterms :: Term f -> [Term f]

Find all subterms of a term.

properSubterms :: Term f -> [Term f]

Find all proper subterms of a term.

isApp :: Term f -> Bool

Check if a term is a function application.

isVar :: Term f -> Bool

Check if a term is a variable

isInstanceOf :: Term f -> Term f -> Bool

t `'isInstanceOf'\` pat checks if t is an instance of pat.

isVariantOf :: Term f -> Term f -> Bool

Check if two terms are renamings of one another.

isSubtermOf :: Term f -> Term f -> Bool

Is a term a subterm of another one?

mapFun :: (Fun f -> Fun g) -> Term f -> Builder g

Map a function over the function symbols in a term.

mapFunList :: (Fun f -> Fun g) -> TermList f -> Builder g

Map a function over the function symbols in a termlist.

replacePosition :: (Build a, BuildFun a ~ f) => Int -> a -> TermList f -> Builder f

Replace the term at a given position in a term with a different term.

replacePositionSub :: (Substitution sub, SubstFun sub ~ f) => sub -> Int -> TermList f -> TermList f -> Builder f

Replace the term at a given position in a term with a different term, while simultaneously applying a substitution. Useful for building critical pairs.

positionToPath :: Term f -> Int -> [Int]

Convert a position in a term, expressed as a single number, into a path.

pathToPosition :: Term f -> [Int] -> Int

Convert a path in a term into a position.

(<<) :: Ord f => Fun f -> Fun f -> Bool

Compare the fun_values of two Funs.

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).

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]

Defined in Twee.Base

Associated Types

type ConstantOf [a] :: Type

Methods

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

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

Symbolic a => Symbolic (Maybe a)

Defined in Twee.Base

Associated Types

type ConstantOf (Maybe a) :: Type

Methods

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

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

Symbolic (Term f)

Defined in Twee.Base

Associated Types

type ConstantOf (Term f) :: Type

Methods

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

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

Symbolic (TermList f)

Defined in Twee.Base

Associated Types

type ConstantOf (TermList f) :: Type

Methods

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

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

Symbolic (Subst f)

Defined in Twee.Base

Associated Types

type ConstantOf (Subst f) :: Type

Methods

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

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

Symbolic (Equation f)

Defined in Twee.Equation

Associated Types

type ConstantOf (Equation f) :: Type

Methods

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

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

Symbolic (Derivation f)

Defined in Twee.Proof

Associated Types

type ConstantOf (Derivation f) :: Type

Methods

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

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

Symbolic (Resulting f)

Defined in Twee.Rule

Associated Types

type ConstantOf (Resulting f) :: Type

Methods

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

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

Symbolic (Reduction f)

Defined in Twee.Rule

Associated Types

type ConstantOf (Reduction f) :: Type

Methods

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

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

Symbolic (Orientation f)

Defined in Twee.Rule

Associated Types

type ConstantOf (Orientation f) :: Type

Methods

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

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

Symbolic (Rule f)

Defined in Twee.Rule

Associated Types

type ConstantOf (Rule f) :: Type

Methods

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

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

Symbolic (CriticalPair f)

Defined in Twee.CP

Associated Types

type ConstantOf (CriticalPair f) :: Type

Methods

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

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

PrettyTerm f => Symbolic (ActiveRule f)

Defined in Twee

Associated Types

type ConstantOf (ActiveRule f) :: Type

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)

Defined in Twee.Base

Associated Types

type ConstantOf (a, b) :: Type

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)

Defined in Twee.Base

Associated Types

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

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

Defined in Twee.Base

Methods

minBound :: Id

maxBound :: Id

Enum Id

Defined in Twee.Base

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

Defined in Twee.Base

Methods

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

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

Integral Id

Defined in Twee.Base

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

Defined in Twee.Base

Methods

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

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

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

negate :: Id -> Id

abs :: Id -> Id

signum :: Id -> Id

fromInteger :: Integer -> Id

Ord Id

Defined in Twee.Base

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

Defined in Twee.Base

Methods

toRational :: Id -> Rational

Show Id

Defined in Twee.Base

Methods

showsPrec :: Int -> Id -> ShowS

show :: Id -> String

showList :: [Id] -> ShowS

Pretty Id

Defined in Twee.Base

Methods

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

pPrint :: Id -> Doc

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

Has (ActiveRule f) Id

Defined in Twee

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.

Methods

the :: a -> b

Get at the thing.

Instances

Has a a

Defined in Twee.Base

Methods

the :: a -> a

Has (ActiveRule f) Depth

Defined in Twee

Methods

the :: ActiveRule f -> Depth

Has (ActiveRule f) RuleId

Defined in Twee

Methods

the :: ActiveRule f -> RuleId

Has (ActiveRule f) Id

Defined in Twee

Methods

the :: ActiveRule f -> Id

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

Defined in Twee.Rule

Methods

the :: Rule f -> Term g

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

Defined in Twee

Methods

the :: ActiveRule f -> Positions g

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

Defined in Twee

Methods

the :: ActiveRule f -> Proof g

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

Defined in Twee

Methods

the :: ActiveRule f -> Rule g

Typeclasses

class Minimal f where

Methods

minimal :: Fun f

Instances

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

Defined in Twee.Base

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.

Methods

skolem :: Var -> Fun f

Turn a variable into a Skolem constant.

getSkolem :: Fun f -> Maybe Var

Instances

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

Defined in Twee.Base

Methods

skolem :: Var -> Fun (Extended f)

getSkolem :: Fun (Extended f) -> Maybe Var

class Arity f where

For types which have a notion of arity.

Methods

arity :: f -> Int

Measure the arity.

Instances

Arity f => Arity (Fun f)

Defined in Twee.Base

Methods

arity :: Fun f -> Int

Arity f => Arity (Extended f)

Defined in Twee.Base

Methods

arity :: Extended f -> Int

class Sized a where

For types which have a notion of size.

Methods

size :: a -> Int

Compute the size.

Instances

Sized f => Sized (Fun f)

Defined in Twee.Base

Methods

size :: Fun f -> Int

Sized f => Sized (Term f)

Defined in Twee.Base

Methods

size :: Term f -> Int

Sized f => Sized (TermList f)

Defined in Twee.Base

Methods

size :: TermList f -> Int

Sized f => Sized (Extended f)

Defined in Twee.Base

Methods

size :: Extended f -> Int

Sized f => Sized (Equation f)

Defined in Twee.Equation

Methods

size :: Equation f -> Int

class Ord f => Ordered f where

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.

Minimal complete definition

Nothing

Methods

hasEqualsBonus :: f -> Bool

isEquals :: f -> Bool

isTrue :: f -> Bool

isFalse :: f -> Bool

Instances

EqualsBonus f => EqualsBonus (Fun f)

Defined in Twee.Base

Methods

hasEqualsBonus :: Fun f -> Bool

isEquals :: Fun f -> Bool

isTrue :: Fun f -> Bool

isFalse :: Fun f -> Bool

EqualsBonus f => EqualsBonus (Extended f)

Defined in Twee.Base

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

Defined in Twee.Constraints

Methods

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

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

Show Strictness

Defined in Twee.Constraints

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 Extended and Skolem instances.

Constructors

Minimal

The minimal constant.

Skolem Var

A Skolem function.

Function f

An ordinary function symbol.

Instances

Functor Extended

Defined in Twee.Base

Methods

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

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

Eq f => Eq (Extended f)

Defined in Twee.Base

Methods

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

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

Ord f => Ord (Extended f)

Defined in Twee.Base

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)

Defined in Twee.Base

Methods

showsPrec :: Int -> Extended f -> ShowS

show :: Extended f -> String

showList :: [Extended f] -> ShowS

Pretty f => Pretty (Extended f)

Defined in Twee.Base

Methods

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

pPrint :: Extended f -> Doc

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

PrettyTerm f => PrettyTerm (Extended f)

Defined in Twee.Base

Methods

termStyle :: Extended f -> TermStyle

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

Defined in Twee.Base

Methods

minimal :: Fun (Extended f)

EqualsBonus f => EqualsBonus (Extended f)

Defined in Twee.Base

Methods

hasEqualsBonus :: Extended f -> Bool

isEquals :: Extended f -> Bool

isTrue :: Extended f -> Bool

isFalse :: Extended f -> Bool

Sized f => Sized (Extended f)

Defined in Twee.Base

Methods

size :: Extended f -> Int

Arity f => Arity (Extended f)

Defined in Twee.Base

Methods

arity :: Extended f -> Int

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

Defined in Twee.Base

Methods

skolem :: Var -> Fun (Extended f)

getSkolem :: Fun (Extended f) -> Maybe Var