twee-lib-2.4.2: An equational theorem prover
Safe HaskellSafe-Inferred
LanguageHaskell2010

Twee.Term

Description

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

Terms

data Term f Source #

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

Instances

Instances details
(Labelled f, Show f) => Show (Term f) Source # 
Instance details

Defined in Twee.Term

Methods

showsPrec :: Int -> Term f -> ShowS #

show :: Term f -> String #

showList :: [Term f] -> ShowS #

Eq (Term f) Source # 
Instance details

Defined in Twee.Term.Core

Methods

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

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

Ord (Term f) Source # 
Instance details

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) Source # 
Instance details

Defined in Twee.Pretty

Methods

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

pPrint :: Term f -> Doc #

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

Symbolic (Term f) Source # 
Instance details

Defined in Twee.Base

Associated Types

type ConstantOf (Term f) Source #

Methods

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

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

(Labelled f, Sized f, Weighted f) => Sized (Term f) Source # 
Instance details

Defined in Twee.KBO

Methods

size :: Term f -> Integer Source #

Build (Term f) Source # 
Instance details

Defined in Twee.Term

Associated Types

type BuildFun (Term f) Source #

Methods

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

f ~ g => Has (Rule f) (Term g) Source # 
Instance details

Defined in Twee.Rule

Methods

the :: Rule f -> Term g Source #

type ConstantOf (Term f) Source # 
Instance details

Defined in Twee.Base

type ConstantOf (Term f) = f
type BuildFun (Term f) Source # 
Instance details

Defined in Twee.Term

type BuildFun (Term f) = f

pattern Var :: Var -> Term f Source #

Matches a variable.

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

Matches a function application.

isApp :: Term f -> Bool Source #

Check if a term is a function application.

isVar :: Term f -> Bool Source #

Check if a term is a variable

singleton :: Term f -> TermList f Source #

Convert a term to a termlist.

len :: Term f -> Int Source #

Find the length of a term.

Termlists

data TermList f Source #

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

Instances details
(Labelled f, Show f) => Show (TermList f) Source # 
Instance details

Defined in Twee.Term

Methods

showsPrec :: Int -> TermList f -> ShowS #

show :: TermList f -> String #

showList :: [TermList f] -> ShowS #

Eq (TermList f) Source # 
Instance details

Defined in Twee.Term.Core

Methods

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

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

Ord (TermList f) Source # 
Instance details

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) Source # 
Instance details

Defined in Twee.Pretty

Symbolic (TermList f) Source # 
Instance details

Defined in Twee.Base

Associated Types

type ConstantOf (TermList f) Source #

(Labelled f, Sized f, Weighted f) => Sized (TermList f) Source # 
Instance details

Defined in Twee.KBO

Methods

size :: TermList f -> Integer Source #

Build (TermList f) Source # 
Instance details

Defined in Twee.Term

Associated Types

type BuildFun (TermList f) Source #

type ConstantOf (TermList f) Source # 
Instance details

Defined in Twee.Base

type ConstantOf (TermList f) = f
type BuildFun (TermList f) Source # 
Instance details

Defined in Twee.Term

type BuildFun (TermList f) = f

pattern Empty :: TermList f Source #

Matches the empty termlist.

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

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

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

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

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

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

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

empty :: forall f. TermList f Source #

The empty termlist.

unpack :: TermList f -> [Term f] Source #

Convert a termlist into an ordinary list of terms.

lenList :: TermList f -> Int Source #

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

Function symbols and variables

data Fun f Source #

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

Instances details
(Labelled f, Show f) => Show (Fun f) Source # 
Instance details

Defined in Twee.Term

Methods

showsPrec :: Int -> Fun f -> ShowS #

show :: Fun f -> String #

showList :: [Fun f] -> ShowS #

Eq (Fun f) Source # 
Instance details

Defined in Twee.Term.Core

Methods

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

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

Ord (Fun f) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

Defined in Twee.Base

(Labelled f, Sized f) => Sized (Fun f) Source # 
Instance details

Defined in Twee.KBO

Methods

size :: Fun f -> Integer Source #

(Weighted f, Labelled f) => Weighted (Fun f) Source # 
Instance details

Defined in Twee.KBO

Methods

argWeight :: Fun f -> Integer Source #

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

Construct a Fun from a function symbol.

fun_id :: Fun f -> Int Source #

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

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

The underlying function symbol of a Fun.

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

A pattern which extracts the fun_value from a Fun.

newtype Var Source #

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

Instances details
Enum Var Source # 
Instance details

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 Source # 
Instance details

Defined in Twee.Term.Core

Methods

showsPrec :: Int -> Var -> ShowS #

show :: Var -> String #

showList :: [Var] -> ShowS #

Eq Var Source # 
Instance details

Defined in Twee.Term.Core

Methods

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

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

Ord Var Source # 
Instance details

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 Source # 
Instance details

Defined in Twee.Pretty

class Labelled f where Source #

Minimal complete definition

Nothing

Methods

label :: f -> Label f Source #

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

Building terms

class Build a where Source #

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

The underlying type of function symbols.

Methods

builder :: a -> Builder (BuildFun a) Source #

Convert a value into a Builder.

Instances

Instances details
Build (Builder f) Source # 
Instance details

Defined in Twee.Term

Associated Types

type BuildFun (Builder f) Source #

Build (Term f) Source # 
Instance details

Defined in Twee.Term

Associated Types

type BuildFun (Term f) Source #

Methods

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

Build (TermList f) Source # 
Instance details

Defined in Twee.Term

Associated Types

type BuildFun (TermList f) Source #

Build a => Build [a] Source # 
Instance details

Defined in Twee.Term

Associated Types

type BuildFun [a] Source #

Methods

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

data Builder f Source #

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

Instances

Instances details
Monoid (Builder f) Source # 
Instance details

Defined in Twee.Term.Core

Methods

mempty :: Builder f #

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

mconcat :: [Builder f] -> Builder f #

Semigroup (Builder f) Source # 
Instance details

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) Source # 
Instance details

Defined in Twee.Term

Associated Types

type BuildFun (Builder f) Source #

type BuildFun (Builder f) Source # 
Instance details

Defined in Twee.Term

type BuildFun (Builder f) = f

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

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

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

Build a termlist.

con :: Fun f -> Builder f Source #

Build a constant (a function with no arguments).

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

Build a function application.

var :: Var -> Builder f Source #

Build a variable.

Access to subterms

children :: Term f -> TermList f Source #

Get the children (direct subterms) of a term.

properSubterms :: Term f -> [Term f] Source #

Find all proper subterms of a term.

subtermsList :: TermList f -> [Term f] Source #

Find all subterms of a termlist.

subterms :: Term f -> [Term f] Source #

Find all subterms of a term.

reverseSubtermsList :: TermList f -> [Term f] Source #

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

occurs :: Var -> Term f -> Bool Source #

Check if a variable occurs in a term.

isSubtermOf :: Term f -> Term f -> Bool Source #

Is a term a subterm of another one?

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

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

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

Index into a termlist.

Substitutions

class Substitution s where Source #

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

The underlying type of function symbols.

Methods

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

Apply the substitution to a variable.

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

Apply the substitution to a termlist.

Instances

Instances details
Substitution (Subst f) Source # 
Instance details

Defined in Twee.Term

Associated Types

type SubstFun (Subst f) Source #

Substitution (TriangleSubst f) Source # 
Instance details

Defined in Twee.Term

Associated Types

type SubstFun (TriangleSubst f) Source #

(Build a, v ~ Var) => Substitution (v -> a) Source # 
Instance details

Defined in Twee.Term

Associated Types

type SubstFun (v -> a) Source #

Methods

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

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

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

Apply a substitution to a term.

newtype Subst f Source #

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

Constructors

Subst 

Fields

Instances

Instances details
(Labelled f, Show f) => Show (Subst f) Source # 
Instance details

Defined in Twee.Term

Methods

showsPrec :: Int -> Subst f -> ShowS #

show :: Subst f -> String #

showList :: [Subst f] -> ShowS #

Eq (Subst f) Source # 
Instance details

Defined in Twee.Term

Methods

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

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

Ord (Subst f) Source # 
Instance details

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) Source # 
Instance details

Defined in Twee.Pretty

Symbolic (Subst f) Source # 
Instance details

Defined in Twee.Base

Associated Types

type ConstantOf (Subst f) Source #

Methods

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

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

Substitution (Subst f) Source # 
Instance details

Defined in Twee.Term

Associated Types

type SubstFun (Subst f) Source #

type ConstantOf (Subst f) Source # 
Instance details

Defined in Twee.Base

type ConstantOf (Subst f) = f
type SubstFun (Subst f) Source # 
Instance details

Defined in Twee.Term

type SubstFun (Subst f) = f

Constructing and querying substitutions

emptySubst :: Subst f Source #

The empty substitution.

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

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

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

Convert a substitution to a list of bindings.

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

Look up a variable in a substitution.

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

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

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

Add a new binding to a substitution.

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

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

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

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

retract :: Var -> Subst f -> Subst f Source #

Remove a binding from a substitution.

Other operations on substitutions

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

Fold a function over a substitution.

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

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

substDomain :: Subst f -> [Var] Source #

Compute the set of variables bound by a substitution.

substSize :: Subst f -> Int Source #

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

substCompatible :: Subst f -> Subst f -> Bool Source #

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

substUnion :: Subst f -> Subst f -> Subst f Source #

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

idempotent :: Subst f -> Bool Source #

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

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

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

canonicalise :: [TermList f] -> Subst f Source #

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

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

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

A variant of match which extends an existing substitution.

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

A variant of match which works on termlists.

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

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

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

A variant of match which works on lists of terms.

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

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

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

A variant of match which works on lists of termlists.

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

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

isInstanceOf :: Term f -> Term f -> Bool Source #

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

isVariantOf :: Term f -> Term f -> Bool Source #

Check if two terms are renamings of one another.

Unification

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

Unify two terms.

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

Unify two termlists.

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

Unify a collection of pairs of terms.

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

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

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

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

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

Unify two terms, starting from an existing substitution.

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

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

newtype TriangleSubst f Source #

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

Instances

Instances details
(Labelled f, Show f) => Show (TriangleSubst f) Source # 
Instance details

Defined in Twee.Term

Substitution (TriangleSubst f) Source # 
Instance details

Defined in Twee.Term

Associated Types

type SubstFun (TriangleSubst f) Source #

type SubstFun (TriangleSubst f) Source # 
Instance details

Defined in Twee.Term

type SubstFun (TriangleSubst f) = f

emptyTriangleSubst :: TriangleSubst f Source #

The empty triangle substitution.

close :: TriangleSubst f -> Subst f Source #

Iterate a triangle substitution to make it idempotent.

Positions in terms

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

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

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

Convert a path in a term into a position.

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

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

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

Miscellaneous functions

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

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

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

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

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

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

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

Map a function over the function symbols in a term.

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

Map a function over the function symbols in a termlist.

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

Compare the fun_values of two Funs.

Orphan instances

(Labelled f, Show f) => Show (Fun f) Source # 
Instance details

Methods

showsPrec :: Int -> Fun f -> ShowS #

show :: Fun f -> String #

showList :: [Fun f] -> ShowS #

(Labelled f, Show f) => Show (Term f) Source # 
Instance details

Methods

showsPrec :: Int -> Term f -> ShowS #

show :: Term f -> String #

showList :: [Term f] -> ShowS #

(Labelled f, Show f) => Show (TermList f) Source # 
Instance details

Methods

showsPrec :: Int -> TermList f -> ShowS #

show :: TermList f -> String #

showList :: [TermList f] -> ShowS #