Safe Haskell	None
Language	Haskell2010

Twee.Term

Contents

Orphan instances

Documentation

class Build f a | a -> f where Source #

Minimal complete definition

builder

Methods

builder :: a -> Builder f Source #

Instances

Build f a => Build f [a] Source #
Methods builder :: [a] -> Builder f Source #
Build f (TermList f) Source #
Methods builder :: TermList f -> Builder f Source #
Build f (Term f) Source #
Methods builder :: Term f -> Builder f Source #
Build f (Builder f) Source #
Methods builder :: Builder f -> Builder f Source #

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

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

con :: Fun f -> Builder f Source #

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

var :: Var -> Builder f Source #

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

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

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

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

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

class Substitution f s | s -> f where Source #

Minimal complete definition

evalSubst

Methods

evalSubst :: s -> Var -> Builder f Source #

Instances

Substitution f (TriangleSubst f) Source #
Methods evalSubst :: TriangleSubst f -> Var -> Builder f Source #
Substitution f (Subst f) Source #
Methods evalSubst :: Subst f -> Var -> Builder f Source #
(Build f a, (~) * v Var) => Substitution f (v -> a) Source #
Methods evalSubst :: (v -> a) -> Var -> Builder f Source #

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

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

newtype Subst f Source #

Constructors

Subst
Fields unSubst :: IntMap (TermList f)

Instances

Substitution f (Subst f) Source #
Methods evalSubst :: Subst f -> Var -> Builder f Source #
Show (Subst f) Source #
Methods showsPrec :: Int -> Subst f -> ShowS # show :: Subst f -> String # showList :: [Subst f] -> ShowS #

substSize :: Subst f -> Int Source #

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

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

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

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

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

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

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

idempotent :: Subst f -> Bool Source #

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

close :: TriangleSubst f -> Subst f Source #

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

emptySubst :: Subst f Source #

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

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

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

newtype TriangleSubst f Source #

Constructors

Triangle
Fields unTriangle :: Subst f

Instances

Substitution f (TriangleSubst f) Source #
Methods evalSubst :: TriangleSubst f -> Var -> Builder f Source #
Show (TriangleSubst f) Source #
Methods showsPrec :: Int -> TriangleSubst f -> ShowS # show :: TriangleSubst f -> String # showList :: [TriangleSubst f] -> ShowS #

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

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

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

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

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

children :: Term f -> TermList f Source #

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

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

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

len :: Term f -> Int Source #

emitTerm :: Term f -> Builder f Source #

bound :: Term f -> Int Source #

boundList :: TermList f -> Int Source #

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

occursList :: Var -> TermList f -> Bool Source #

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

emptyTermList :: TermList f Source #

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

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

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

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

isFun :: Term f -> Bool Source #

isVar :: Term f -> Bool Source #

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

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

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

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

class Numbered f where Source #

Minimal complete definition

fromInt, toInt

Methods

fromInt :: Int -> f Source #

toInt :: f -> Int Source #

Instances

Numbered f => Numbered (Extended f) Source #
Methods fromInt :: Int -> Extended f Source # toInt :: Extended f -> Int Source #

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

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

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

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

data Term f Source #

Instances

Build f (Term f) Source #
Methods builder :: Term f -> Builder f Source #
Eq (Term f) Source #
Methods (==) :: Term f -> Term f -> Bool # (/=) :: Term f -> Term f -> Bool #
Ord (Term f) Source #
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) Source #
Methods size :: Term f -> Int Source #
Symbolic (Term f) Source #
Associated Types type ConstantOf (Term f) :: * Source # Methods term :: Term f -> TermOf (Term f) Source # termsDL :: Term f -> DList (TermListOf (Term f)) Source # replace :: (TermListOf (Term f) -> BuilderOf (Term f)) -> Term f -> Term f Source #
type ConstantOf (Term f) Source #
type ConstantOf (Term f) = f

data TermList f Source #

Instances

Build f (TermList f) Source #
Methods builder :: TermList f -> Builder f Source #
Eq (TermList f) Source #
Methods (==) :: TermList f -> TermList f -> Bool # (/=) :: TermList f -> TermList f -> Bool #
Ord (TermList f) Source #
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) Source #
Methods size :: TermList f -> Int Source #
Symbolic (TermList f) Source #
Associated Types type ConstantOf (TermList f) :: * Source # Methods term :: TermList f -> TermOf (TermList f) Source # termsDL :: TermList f -> DList (TermListOf (TermList f)) Source # replace :: (TermListOf (TermList f) -> BuilderOf (TermList f)) -> TermList f -> TermList f Source #
type ConstantOf (TermList f) Source #
type ConstantOf (TermList f) = f

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

lenList :: TermList f -> Int Source #

pattern Empty :: forall f. TermList f Source #

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

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

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

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

newtype Fun f Source #

Constructors

MkFun Int

Instances

Eq (Fun f) Source #
Methods (==) :: Fun f -> Fun f -> Bool # (/=) :: Fun f -> Fun f -> Bool #
Show (Fun f) Source #
Methods showsPrec :: Int -> Fun f -> ShowS # show :: Fun f -> String # showList :: [Fun f] -> ShowS #
(Numbered f, Minimal f) => Minimal (Fun f) Source #
Methods minimal :: Fun f Source #
(Sized f, Numbered f) => Sized (Fun f) Source #
Methods size :: Fun f -> Int Source #
(Numbered f, Arity f) => Arity (Fun f) Source #
Methods arity :: Fun f -> Int Source #
(Numbered f, Skolem f) => Skolem (Fun f) Source #
Methods skolem :: Var -> Fun f Source #

newtype Var Source #

Constructors

MkVar Int

Instances

Enum Var Source #
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 Source #
Methods (==) :: Var -> Var -> Bool # (/=) :: Var -> Var -> Bool #
Ord Var Source #
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 Source #
Methods showsPrec :: Int -> Var -> ShowS # show :: Var -> String # showList :: [Var] -> ShowS #

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

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

singleton :: Term f -> TermList f Source #

data Builder f Source #

Instances

Build f (Builder f) Source #
Methods builder :: Builder f -> Builder f Source #
Monoid (Builder f) Source #
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) Source #
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) Source #
Methods showsPrec :: Int -> Term f -> ShowS # show :: Term f -> String # showList :: [Term f] -> ShowS #
Show (TermList f) Source #
Methods showsPrec :: Int -> TermList f -> ShowS # show :: TermList f -> String # showList :: [TermList f] -> ShowS #