Twee.Term.Core

Documentation

data Symbol

Constructors

Symbol

Fields

• isFun :: Bool
• index :: Int
• size :: Int

Instances

Show Symbol

Methods

showsPrec :: Int -> Symbol -> ShowS

show :: Symbol -> String

showList :: [Symbol] -> ShowS

toSymbol :: Int64 -> Symbol

fromSymbol :: Symbol -> Int64

data TermList f

Constructors

TermList

Fields

• low :: !Int
• high :: !Int
• array :: !ByteArray

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

data Term f

Constructors

Term

Fields

• root :: !Int64
• termlist :: !(TermList 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

Empty :: TermList f

Cons t ts :: Term f -> TermList f -> TermList f

ConsSym t ts :: Term f -> TermList f -> TermList f

UnsafeCons/UnsafeConsSym: like Cons and ConsSym but don't check

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

unsafePatHead :: TermList f -> Maybe (Term f, TermList f, TermList f)

patHead :: TermList f -> Maybe (Term f, TermList f, TermList f)

Var :: Var -> Term f

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

patRoot :: Int64 -> Either Var (Fun f)

patNext :: TermList f -> TermList f

singleton :: Term f -> TermList f

eqSameLength :: TermList f -> TermList f -> Bool

compareContents :: TermList f -> TermList f -> Ordering

newtype Builder f

Constructors

Builder

Fields

• unBuilder :: forall s. Builder1 s

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

type Builder1 s = State# s -> MutableByteArray# s -> Int# -> Int# -> (#State# s, Int##)

buildTermList :: Builder f -> TermList f

getArray :: (MutableByteArray s -> Builder1 s) -> Builder1 s

getSize :: (Int -> Builder1 s) -> Builder1 s

getIndex :: (Int -> Builder1 s) -> Builder1 s

putIndex :: Int -> Builder1 s

liftST :: ST s () -> Builder1 s

built :: Builder1 s

then_ :: Builder1 s -> Builder1 s -> Builder1 s

checked :: Int -> Builder1 s -> Builder1 s

emitSymbolBuilder :: Symbol -> Builder f -> Builder f

emitFun :: Fun f -> Builder f -> Builder f

emitVar :: Var -> Builder f

emitTermList :: TermList f -> Builder f