Twee.Term

Terms and substitutions.

Terms in twee are represented as arrays rather than as an algebraic data type. This module defines pattern synonyms (App, Var, Cons, Empty) which means that pattern matching on terms works just as normal. The pattern synonyms can not be used to create new terms; for that you have to use a builder interface (Build).

This module also provides:

• pattern synonyms for iterating through a term one symbol at a time (ConsSym);
• substitutions (Substitution, Subst, subst);
• unification (unify) and matching (match);
• miscellaneous useful functions on terms.

Terms

data Term f

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

Instances

(Labelled f, Show f) => Show (Term f)

Defined in Twee.Term

Methods

showsPrec :: Int -> Term f -> ShowS

show :: Term f -> String

showList :: [Term f] -> ShowS

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

(Labelled f, 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

Symbolic (Term f)

Defined in Twee.Base

Associated Types

type ConstantOf (Term f)

Methods

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

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

(Labelled f, Sized f, Weighted f) => Sized (Term f)

Defined in Twee.KBO

Methods

size :: Term f -> Integer

Build (Term f)

Defined in Twee.Term

Associated Types

type BuildFun (Term f)

Methods

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

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

Defined in Twee.Rule

Methods

the :: Rule f -> Term g

type ConstantOf (Term f)

Defined in Twee.Base

type ConstantOf (Term f) = f

type BuildFun (Term f)

Defined in Twee.Term

type BuildFun (Term f) = f

pattern Var :: Var -> Term f

Matches a variable.

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

Matches a function application.

isApp :: Term f -> Bool

Check if a term is a function application.

isVar :: Term f -> Bool

Check if a term is a variable

singleton :: Term f -> TermList f

Convert a term to a termlist.

len :: Term f -> Int

Find the length of a term.

Termlists

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

(Labelled f, Show f) => Show (TermList f)

Defined in Twee.Term

Methods

showsPrec :: Int -> TermList f -> ShowS

show :: TermList f -> String

showList :: [TermList f] -> ShowS

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

(Labelled f, 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

Symbolic (TermList f)

Defined in Twee.Base

Associated Types

type ConstantOf (TermList f)

Methods

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

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

(Labelled f, Sized f, Weighted f) => Sized (TermList f)

Defined in Twee.KBO

Methods

size :: TermList f -> Integer

Build (TermList f)

Defined in Twee.Term

Associated Types

type BuildFun (TermList f)

Methods

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

type ConstantOf (TermList f)

Defined in Twee.Base

type ConstantOf (TermList f) = f

type BuildFun (TermList f)

Defined in Twee.Term

type BuildFun (TermList f) = f

pattern Empty :: TermList f

Matches the empty termlist.

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

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

pattern ConsSym :: Term f -> TermList 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)]

hd :: TermList f -> Term f

tl :: TermList f -> TermList f

rest :: TermList f -> TermList f

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 UnsafeConsSym :: Term f -> TermList 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.

uhd :: TermList f -> Term f

utl :: TermList f -> TermList f

urest :: TermList f -> TermList f

empty :: forall f. TermList f

The empty termlist.

unpack :: TermList f -> [Term f]

Convert a termlist into an ordinary list of terms.

lenList :: TermList f -> Int

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

Function symbols and variables

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

(Labelled f, Show f) => Show (Fun f)

Defined in Twee.Term

Methods

showsPrec :: Int -> Fun f -> ShowS

show :: Fun f -> String

showList :: [Fun f] -> ShowS

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

(Pretty f, Labelled f) => Pretty (Fun f)

Defined in Twee.Pretty

Methods

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

pPrint :: Fun f -> Doc

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

(Labelled f, 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

(Labelled f, Sized f) => Sized (Fun f)

Defined in Twee.KBO

Methods

size :: Fun f -> Integer

(Weighted f, Labelled f) => Weighted (Fun f)

Defined in Twee.KBO

Methods

argWeight :: Fun f -> Integer

fun :: Labelled f => f -> Fun f

Construct a Fun from a function symbol.

fun_id :: Fun f -> Int

The unique number of a Fun. Must fit in 32 bits.

fun_value :: Labelled f => Fun f -> f

The underlying function symbol of a Fun.

pattern F :: Labelled f => Int -> f -> Fun f

A pattern which extracts the fun_value from a Fun.

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]

Show Var

Defined in Twee.Term.Core

Methods

showsPrec :: Int -> Var -> ShowS

show :: Var -> String

showList :: [Var] -> ShowS

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

Pretty Var

Defined in Twee.Pretty

Methods

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

pPrint :: Var -> Doc

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

class Labelled f where

Minimal complete definition

Nothing

Methods

label :: f -> Label f

default label :: (Ord f, Typeable f) => f -> Label f

Building terms

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 (Builder f)

Defined in Twee.Term

Associated Types

type BuildFun (Builder f)

Methods

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

Build (Term f)

Defined in Twee.Term

Associated Types

type BuildFun (Term f)

Methods

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

Build (TermList f)

Defined in Twee.Term

Associated Types

type BuildFun (TermList f)

Methods

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

Build a => Build [a]

Defined in Twee.Term

Associated Types

type BuildFun [a]

Methods

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

data Builder f

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

Instances

Monoid (Builder f)

Defined in Twee.Term.Core

Methods

mempty :: Builder f

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

mconcat :: [Builder f] -> Builder f

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

Build (Builder f)

Defined in Twee.Term

Associated Types

type BuildFun (Builder f)

Methods

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

type BuildFun (Builder f)

Defined in Twee.Term

type BuildFun (Builder f) = f

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.

Access to subterms

children :: Term f -> TermList f

Get the children (direct subterms) of a term.

properSubterms :: Term f -> [Term f]

Find all proper subterms of a term.

subtermsList :: TermList f -> [Term f]

Find all subterms of a termlist.

subterms :: Term f -> [Term f]

Find all subterms of a term.

reverseSubtermsList :: TermList f -> [Term f]

Find all subterms of a term, but in reverse order.

reverseSubterms :: Term f -> [Term f]

occurs :: Var -> Term f -> Bool

Check if a variable occurs in a term.

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

Is a term a subterm of another one?

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

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

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

Index into a termlist.

Substitutions

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 (Subst f)

Defined in Twee.Term

Associated Types

type SubstFun (Subst f)

Methods

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

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

Substitution (TriangleSubst f)

Defined in Twee.Term

Associated Types

type SubstFun (TriangleSubst f)

Methods

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

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

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

Defined in Twee.Term

Associated Types

type SubstFun (v -> a)

Methods

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

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

subst :: Substitution s => s -> Term (SubstFun s) -> Builder (SubstFun s)

Apply a substitution to a term.

newtype Subst f

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

Constructors

Subst

Fields

• unSubst :: IntMap (TermList f)

Instances

(Labelled f, Show f) => Show (Subst f)

Defined in Twee.Term

Methods

showsPrec :: Int -> Subst f -> ShowS

show :: Subst f -> String

showList :: [Subst f] -> ShowS

Eq (Subst f)

Defined in Twee.Term

Methods

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

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

Ord (Subst f)

Defined in Twee.Term

Methods

compare :: Subst f -> Subst f -> Ordering

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

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

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

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

max :: Subst f -> Subst f -> Subst f

min :: Subst f -> Subst f -> Subst f

(Labelled f, 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

Symbolic (Subst f)

Defined in Twee.Base

Associated Types

type ConstantOf (Subst f)

Methods

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

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

Substitution (Subst f)

Defined in Twee.Term

Associated Types

type SubstFun (Subst f)

Methods

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

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

type ConstantOf (Subst f)

Defined in Twee.Base

type ConstantOf (Subst f) = f

type SubstFun (Subst f)

Defined in Twee.Term

type SubstFun (Subst f) = f

Constructing and querying substitutions

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.

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

Convert a substitution to a list of bindings.

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

Look up a variable in a substitution.

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

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

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

Add a new binding to a substitution.

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

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

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

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

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

Remove a binding from a substitution.

Other operations on substitutions

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.

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.

canonicalise :: [TermList f] -> Subst f

Return a substitution which renames the variables of a list of terms to put them in a canonical order.

Matching

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.

matchMany :: [Term f] -> [Term f] -> Maybe (Subst f)

A variant of match which works on lists of terms.

matchManyIn :: Subst f -> [Term f] -> [Term f] -> Maybe (Subst f)

A variant of match which works on lists of terms, and extends an existing substitution.

matchManyList :: [TermList f] -> [TermList f] -> Maybe (Subst f)

A variant of match which works on lists of termlists.

matchManyListIn :: Subst f -> [TermList f] -> [TermList f] -> Maybe (Subst f)

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

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.

Unification

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

Unify two terms.

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

Unify two termlists.

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

Unify a collection of pairs of terms.

unifyManyTri :: [(Term f, Term f)] -> Maybe (TriangleSubst f)

Unify a collection of pairs of terms, returning a triangle substitution.

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

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

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

Unify two terms, starting from an existing substitution.

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)

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

(Labelled f, Show f) => 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)

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

emptyTriangleSubst :: TriangleSubst f

The empty triangle substitution.

close :: TriangleSubst f -> Subst f

Iterate a triangle substitution to make it idempotent.

Positions in terms

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.

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.

replace :: (Build a, BuildFun a ~ f) => Term f -> a -> TermList f -> Builder f

Miscellaneous functions

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.

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.

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

Compare the fun_values of two Funs.

Orphan instances

(Labelled f, Show f) => Show (Fun f)

Methods

showsPrec :: Int -> Fun f -> ShowS

show :: Fun f -> String

showList :: [Fun f] -> ShowS

(Labelled f, Show f) => Show (Term f)

Methods

showsPrec :: Int -> Term f -> ShowS

show :: Term f -> String

showList :: [Term f] -> ShowS

(Labelled f, Show f) => Show (TermList f)

Methods

showsPrec :: Int -> TermList f -> ShowS

show :: TermList f -> String

showList :: [TermList f] -> ShowS