Twee.Base

Documentation

class Symbolic a where

Minimal complete definition

term, termsDL, replace

Associated Types

type ConstantOf a

Methods

term :: a -> TermOf a

termsDL :: a -> DList (TermListOf a)

replace :: (TermListOf a -> BuilderOf a) -> a -> a

Instances

Symbolic a => Symbolic [a]

Associated Types

type ConstantOf [a] :: *

Methods

term :: [a] -> TermOf [a]

termsDL :: [a] -> DList (TermListOf [a])

replace :: (TermListOf [a] -> BuilderOf [a]) -> [a] -> [a]

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

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

Symbolic a => Symbolic (Labelled a)

Associated Types

type ConstantOf (Labelled a) :: *

Methods

term :: Labelled a -> TermOf (Labelled a)

termsDL :: Labelled a -> DList (TermListOf (Labelled a))

replace :: (TermListOf (Labelled a) -> BuilderOf (Labelled a)) -> Labelled a -> Labelled a

Symbolic (Equation f)

Associated Types

type ConstantOf (Equation f) :: *

Methods

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

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

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

Symbolic (Orientation f)

Associated Types

type ConstantOf (Orientation f) :: *

Methods

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

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

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

Symbolic (Rule f)

Associated Types

type ConstantOf (Rule f) :: *

Methods

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

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

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

Symbolic (CritInfo f)

Associated Types

type ConstantOf (CritInfo f) :: *

Methods

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

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

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

Symbolic a => Symbolic (Critical a)

Associated Types

type ConstantOf (Critical a) :: *

Methods

term :: Critical a -> TermOf (Critical a)

termsDL :: Critical a -> DList (TermListOf (Critical a))

replace :: (TermListOf (Critical a) -> BuilderOf (Critical a)) -> Critical a -> Critical a

Symbolic (CancellationRule f)

Associated Types

type ConstantOf (CancellationRule f) :: *

Methods

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

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

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

Symbolic a => Symbolic (Modelled a)

Associated Types

type ConstantOf (Modelled a) :: *

Methods

term :: Modelled a -> TermOf (Modelled a)

termsDL :: Modelled a -> DList (TermListOf (Modelled a))

replace :: (TermListOf (Modelled a) -> BuilderOf (Modelled a)) -> Modelled a -> Modelled a

((~) * (ConstantOf a) (ConstantOf b), Symbolic a, Symbolic b) => Symbolic (a, b)

Associated Types

type ConstantOf (a, b) :: *

Methods

term :: (a, b) -> TermOf (a, b)

termsDL :: (a, b) -> DList (TermListOf (a, b))

replace :: (TermListOf (a, b) -> BuilderOf (a, b)) -> (a, b) -> (a, b)

((~) * (ConstantOf a) (ConstantOf b), (~) * (ConstantOf a) (ConstantOf c), Symbolic a, Symbolic b, Symbolic c) => Symbolic (a, b, c)

Associated Types

type ConstantOf (a, b, c) :: *

Methods

term :: (a, b, c) -> TermOf (a, b, c)

termsDL :: (a, b, c) -> DList (TermListOf (a, b, c))

replace :: (TermListOf (a, b, c) -> BuilderOf (a, b, c)) -> (a, b, c) -> (a, b, c)

terms :: Symbolic a => a -> [TermListOf a]

subst :: (Symbolic a, Substitution (ConstantOf a) s) => s -> a -> a

type TermOf a = Term (ConstantOf a)

type TermListOf a = TermList (ConstantOf a)

type SubstOf a = Subst (ConstantOf a)

type BuilderOf a = Builder (ConstantOf a)

type FunOf a = Fun (ConstantOf a)

vars :: Symbolic a => a -> [Var]

isGround :: Symbolic a => a -> Bool

funs :: Symbolic a => a -> [FunOf a]

occ :: Symbolic a => FunOf a -> a -> Int

canonicalise :: Symbolic a => a -> a

class Minimal a where

Minimal complete definition

minimal

Methods

minimal :: a

Instances

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

Methods

minimal :: Fun f

Minimal (Extended f)

Methods

minimal :: Extended f

minimalTerm :: (Numbered f, Minimal f) => Term f

isMinimal :: (Numbered f, Minimal f) => Term f -> Bool

class Skolem f where

Minimal complete definition

skolem

Methods

skolem :: Var -> f

Instances

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

Methods

skolem :: Var -> Fun f

Skolem (Extended f)

Methods

skolem :: Var -> Extended f

class Arity f where

Minimal complete definition

arity

Methods

arity :: f -> Int

Instances

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

Methods

arity :: Fun f -> Int

Arity f => Arity (Extended f)

Methods

arity :: Extended f -> Int

class Sized a where

Minimal complete definition

size

Methods

size :: a -> Int

Instances

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

Methods

size :: Fun f -> Int

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

Methods

size :: Term f -> Int

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

Methods

size :: TermList f -> Int

Sized f => Sized (Extended f)

Methods

size :: Extended f -> Int

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

Methods

size :: Equation f -> Int

class Ord f => Ordered f where

Minimal complete definition

lessEq, lessIn

Methods

orientTerms :: Term f -> Term f -> Maybe Ordering

lessEq :: Term f -> Term f -> Bool

lessIn :: Model f -> Term f -> Term f -> Maybe Strictness

data Strictness

Constructors

Strict

Nonstrict

Instances

Eq Strictness

Methods

(==) :: Strictness -> Strictness -> Bool

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

Show Strictness

Methods

showsPrec :: Int -> Strictness -> ShowS

show :: Strictness -> String

showList :: [Strictness] -> ShowS

class (Numbered f, Ordered f, Arity f, Sized f, Minimal f, Skolem f, PrettyTerm f) => Function f

Instances

(Numbered f, Ordered f, Arity f, Sized f, Minimal f, Skolem f, PrettyTerm f) => Function f

data Extended f

Constructors

Minimal

Skolem Int

Function f

Instances

Functor Extended

Methods

fmap :: (a -> b) -> Extended a -> Extended b

(<$) :: a -> Extended b -> Extended a

Eq f => Eq (Extended f)

Methods

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

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

Ord f => Ord (Extended f)

Methods

compare :: Extended f -> Extended f -> Ordering

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

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

(>) :: Extended f -> Extended f -> Bool

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

max :: Extended f -> Extended f -> Extended f

min :: Extended f -> Extended f -> Extended f

Show f => Show (Extended f)

Methods

showsPrec :: Int -> Extended f -> ShowS

show :: Extended f -> String

showList :: [Extended f] -> ShowS

Pretty f => Pretty (Extended f)

Methods

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

pPrint :: Extended f -> Doc

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

Numbered f => Numbered (Extended f)

Methods

fromInt :: Int -> Extended f

toInt :: Extended f -> Int

PrettyTerm f => PrettyTerm (Extended f)

Methods

termStyle :: Extended f -> TermStyle

Minimal (Extended f)

Methods

minimal :: Extended f

Sized f => Sized (Extended f)

Methods

size :: Extended f -> Int

Arity f => Arity (Extended f)

Methods

arity :: Extended f -> Int

Skolem (Extended f)

Methods

skolem :: Var -> Extended f

extended :: Numbered f => TermList f -> Builder (Extended f)

unextended :: Numbered f => TermList (Extended f) -> Builder f

module Twee.Term

module Twee.Pretty