Twee.Term

Documentation

class Build f a | a -> f where

Minimal complete definition

builder

Methods

builder :: a -> Builder f

Instances

Build f a => Build f [a]

Methods

builder :: [a] -> Builder f

Build f (TermList f)

Methods

builder :: TermList f -> Builder f

Build f (Term f)

Methods

builder :: Term f -> Builder f

Build f (Builder f)

Methods

builder :: Builder f -> Builder f

build :: Build f a => a -> Term f

buildList :: Build f a => a -> TermList f

con :: Fun f -> Builder f

fun :: Build f a => Fun f -> a -> Builder f

var :: Var -> Builder f

listSubstList :: Subst f -> [(Var, TermList f)]

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

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

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

forMSubst_ :: Monad m => Subst f -> (Var -> TermList f -> m ()) -> m ()

class Substitution f s | s -> f where

Minimal complete definition

evalSubst

Methods

evalSubst :: s -> Var -> Builder f

Instances

Substitution f (TriangleSubst f)

Methods

evalSubst :: TriangleSubst f -> Var -> Builder f

Substitution f (Subst f)

Methods

evalSubst :: Subst f -> Var -> Builder f

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

Methods

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

subst :: Substitution f s => s -> Term f -> Builder f

substList :: Substitution f s => s -> TermList f -> Builder f

newtype Subst f

Constructors

Subst

Fields

• unSubst :: IntMap (TermList f)

Instances

Substitution f (Subst f)

Methods

evalSubst :: Subst f -> Var -> Builder f

Show (Subst f)

Methods

showsPrec :: Int -> Subst f -> ShowS

show :: Subst f -> String

showList :: [Subst f] -> ShowS

substSize :: Subst f -> Int

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

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

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

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

substCompose :: Substitution f s => Subst f -> s -> Subst f

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

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

idempotent :: Subst f -> Bool

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

close :: TriangleSubst f -> Subst f

canonicalise :: [TermList f] -> Subst f

emptySubst :: Subst f

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

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

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

newtype TriangleSubst f

Constructors

Triangle

Fields

• unTriangle :: Subst f

Instances

Substitution f (TriangleSubst f)

Methods

evalSubst :: TriangleSubst f -> Var -> Builder f

Show (TriangleSubst f)

Methods

showsPrec :: Int -> TriangleSubst f -> ShowS

show :: TriangleSubst f -> String

showList :: [TriangleSubst f] -> ShowS

substTri :: Subst f -> Var -> Builder f

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

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

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

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

children :: Term f -> TermList f

fromTermList :: TermList f -> [Term f]

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

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

len :: Term f -> Int

emitTerm :: Term f -> Builder f

bound :: Term f -> Int

boundList :: TermList f -> Int

occurs :: Var -> Term f -> Bool

occursList :: Var -> TermList f -> Bool

termListToList :: TermList f -> [Term f]

emptyTermList :: TermList f

subtermsList :: TermList f -> [Term f]

subterms :: Term f -> [Term f]

properSubtermsList :: TermList f -> [Term f]

properSubterms :: Term f -> [Term f]

isFun :: Term f -> Bool

isVar :: Term f -> Bool

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

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

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

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

class Numbered f where

Minimal complete definition

fromInt, toInt

Methods

fromInt :: Int -> f

toInt :: f -> Int

Instances

Numbered f => Numbered (Extended f)

Methods

fromInt :: Int -> Extended f

toInt :: Extended f -> Int

fromFun :: Numbered f => Fun f -> f

toFun :: Numbered f => f -> Fun f

pattern App :: forall f. Numbered f => f -> [Term f] -> Term f

app :: Numbered a => a -> [Term a] -> Term a

data Term f

Instances

Build f (Term f)

Methods

builder :: Term f -> Builder f

Eq (Term f)

Methods

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

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

Ord (Term f)

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

(Sized f, Numbered f) => Sized (Term f)

Methods

size :: Term f -> Int

Symbolic (Term f)

Associated Types

type ConstantOf (Term f) :: *

Methods

term :: Term f -> TermOf (Term f)

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

replace :: (TermListOf (Term f) -> BuilderOf (Term f)) -> Term f -> Term f

type ConstantOf (Term f)

type ConstantOf (Term f) = f

data TermList f

Instances

Build f (TermList f)

Methods

builder :: TermList f -> Builder f

Eq (TermList f)

Methods

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

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

Ord (TermList f)

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

(Sized f, Numbered f) => Sized (TermList f)

Methods

size :: TermList f -> Int

Symbolic (TermList f)

Associated Types

type ConstantOf (TermList f) :: *

Methods

term :: TermList f -> TermOf (TermList f)

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

replace :: (TermListOf (TermList f) -> BuilderOf (TermList f)) -> TermList f -> TermList f

type ConstantOf (TermList f)

type ConstantOf (TermList f) = f

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

lenList :: TermList f -> Int

pattern Empty :: forall f. TermList f

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

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

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

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

newtype Fun f

Constructors

MkFun Int

Instances

Eq (Fun f)

Methods

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

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

Show (Fun f)

Methods

showsPrec :: Int -> Fun f -> ShowS

show :: Fun f -> String

showList :: [Fun f] -> ShowS

(Numbered f, Minimal f) => Minimal (Fun f)

Methods

minimal :: Fun f

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

Methods

size :: Fun f -> Int

(Numbered f, Arity f) => Arity (Fun f)

Methods

arity :: Fun f -> Int

(Numbered f, Skolem f) => Skolem (Fun f)

Methods

skolem :: Var -> Fun f

newtype Var

Constructors

MkVar Int

Instances

Enum Var

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

Methods

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

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

Ord Var

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

Methods

showsPrec :: Int -> Var -> ShowS

show :: Var -> String

showList :: [Var] -> ShowS

pattern Var :: forall t. Var -> Term t

pattern Fun :: forall f. Fun f -> TermList f -> Term f

singleton :: Term f -> TermList f

data Builder f

Instances

Build f (Builder f)

Methods

builder :: Builder f -> Builder f

Monoid (Builder f)

Methods

mempty :: Builder f

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

mconcat :: [Builder f] -> Builder f

Orphan instances

(Ord f, Numbered f) => Ord (Fun f)

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

Methods

showsPrec :: Int -> Term f -> ShowS

show :: Term f -> String

showList :: [Term f] -> ShowS

Show (TermList f)

Methods

showsPrec :: Int -> TermList f -> ShowS

show :: TermList f -> String

showList :: [TermList f] -> ShowS