Safe Haskell	None
Language	Haskell2010

Twee.Base

Documentation

class Symbolic a where Source #

Minimal complete definition

term, termsDL, replace

Associated Types

type ConstantOf a Source #

Methods

term :: a -> TermOf a Source #

termsDL :: a -> DList (TermListOf a) Source #

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

Instances

Symbolic a => Symbolic [a] Source #
Associated Types type ConstantOf [a] :: * Source # Methods term :: [a] -> TermOf [a] Source # termsDL :: [a] -> DList (TermListOf [a]) Source # replace :: (TermListOf [a] -> BuilderOf [a]) -> [a] -> [a] 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 #
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 #
Symbolic a => Symbolic (Labelled a) Source #
Associated Types type ConstantOf (Labelled a) :: * Source # Methods term :: Labelled a -> TermOf (Labelled a) Source # termsDL :: Labelled a -> DList (TermListOf (Labelled a)) Source # replace :: (TermListOf (Labelled a) -> BuilderOf (Labelled a)) -> Labelled a -> Labelled a Source #
Symbolic (Equation f) Source #
Associated Types type ConstantOf (Equation f) :: * Source # Methods term :: Equation f -> TermOf (Equation f) Source # termsDL :: Equation f -> DList (TermListOf (Equation f)) Source # replace :: (TermListOf (Equation f) -> BuilderOf (Equation f)) -> Equation f -> Equation f Source #
Symbolic (Orientation f) Source #
Associated Types type ConstantOf (Orientation f) :: * Source # Methods term :: Orientation f -> TermOf (Orientation f) Source # termsDL :: Orientation f -> DList (TermListOf (Orientation f)) Source # replace :: (TermListOf (Orientation f) -> BuilderOf (Orientation f)) -> Orientation f -> Orientation f Source #
Symbolic (Rule f) Source #
Associated Types type ConstantOf (Rule f) :: * Source # Methods term :: Rule f -> TermOf (Rule f) Source # termsDL :: Rule f -> DList (TermListOf (Rule f)) Source # replace :: (TermListOf (Rule f) -> BuilderOf (Rule f)) -> Rule f -> Rule f Source #
Symbolic (CritInfo f) Source #
Associated Types type ConstantOf (CritInfo f) :: * Source # Methods term :: CritInfo f -> TermOf (CritInfo f) Source # termsDL :: CritInfo f -> DList (TermListOf (CritInfo f)) Source # replace :: (TermListOf (CritInfo f) -> BuilderOf (CritInfo f)) -> CritInfo f -> CritInfo f Source #
Symbolic a => Symbolic (Critical a) Source #
Associated Types type ConstantOf (Critical a) :: * Source # Methods term :: Critical a -> TermOf (Critical a) Source # termsDL :: Critical a -> DList (TermListOf (Critical a)) Source # replace :: (TermListOf (Critical a) -> BuilderOf (Critical a)) -> Critical a -> Critical a Source #
Symbolic (CancellationRule f) Source #
Associated Types type ConstantOf (CancellationRule f) :: * Source # Methods term :: CancellationRule f -> TermOf (CancellationRule f) Source # termsDL :: CancellationRule f -> DList (TermListOf (CancellationRule f)) Source # replace :: (TermListOf (CancellationRule f) -> BuilderOf (CancellationRule f)) -> CancellationRule f -> CancellationRule f Source #
Symbolic a => Symbolic (Modelled a) Source #
Associated Types type ConstantOf (Modelled a) :: * Source # Methods term :: Modelled a -> TermOf (Modelled a) Source # termsDL :: Modelled a -> DList (TermListOf (Modelled a)) Source # replace :: (TermListOf (Modelled a) -> BuilderOf (Modelled a)) -> Modelled a -> Modelled a Source #
((~) * (ConstantOf a) (ConstantOf b), Symbolic a, Symbolic b) => Symbolic (a, b) Source #
Associated Types type ConstantOf (a, b) :: * Source # Methods term :: (a, b) -> TermOf (a, b) Source # termsDL :: (a, b) -> DList (TermListOf (a, b)) Source # replace :: (TermListOf (a, b) -> BuilderOf (a, b)) -> (a, b) -> (a, b) Source #
((~) * (ConstantOf a) (ConstantOf b), (~) * (ConstantOf a) (ConstantOf c), Symbolic a, Symbolic b, Symbolic c) => Symbolic (a, b, c) Source #
Associated Types type ConstantOf (a, b, c) :: * Source # Methods term :: (a, b, c) -> TermOf (a, b, c) Source # termsDL :: (a, b, c) -> DList (TermListOf (a, b, c)) Source # replace :: (TermListOf (a, b, c) -> BuilderOf (a, b, c)) -> (a, b, c) -> (a, b, c) Source #

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

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

type TermOf a = Term (ConstantOf a) Source #

type TermListOf a = TermList (ConstantOf a) Source #

type SubstOf a = Subst (ConstantOf a) Source #

type BuilderOf a = Builder (ConstantOf a) Source #

type FunOf a = Fun (ConstantOf a) Source #

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

isGround :: Symbolic a => a -> Bool Source #

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

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

canonicalise :: Symbolic a => a -> a Source #

class Minimal a where Source #

Minimal complete definition

minimal

Methods

minimal :: a Source #

Instances

(Numbered f, Minimal f) => Minimal (Fun f) Source #
Methods minimal :: Fun f Source #
Minimal (Extended f) Source #
Methods minimal :: Extended f Source #

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

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

class Skolem f where Source #

Minimal complete definition

skolem

Methods

skolem :: Var -> f Source #

Instances

(Numbered f, Skolem f) => Skolem (Fun f) Source #
Methods skolem :: Var -> Fun f Source #
Skolem (Extended f) Source #
Methods skolem :: Var -> Extended f Source #

class Arity f where Source #

Minimal complete definition

arity

Methods

arity :: f -> Int Source #

Instances

(Numbered f, Arity f) => Arity (Fun f) Source #
Methods arity :: Fun f -> Int Source #
Arity f => Arity (Extended f) Source #
Methods arity :: Extended f -> Int Source #

class Sized a where Source #

Minimal complete definition

size

Methods

size :: a -> Int Source #

Instances

(Sized f, Numbered f) => Sized (Fun f) Source #
Methods size :: Fun f -> Int Source #
(Sized f, Numbered f) => Sized (Term f) Source #
Methods size :: Term f -> Int Source #
(Sized f, Numbered f) => Sized (TermList f) Source #
Methods size :: TermList f -> Int Source #
Sized f => Sized (Extended f) Source #
Methods size :: Extended f -> Int Source #
(Numbered f, Sized f) => Sized (Equation f) Source #
Methods size :: Equation f -> Int Source #

class Ord f => Ordered f where Source #

Minimal complete definition

lessEq, lessIn

Methods

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

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

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

data Strictness Source #

Constructors

Strict
Nonstrict

Instances

Eq Strictness Source #
Methods (==) :: Strictness -> Strictness -> Bool # (/=) :: Strictness -> Strictness -> Bool #
Show Strictness Source #
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 Source #

Instances

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

data Extended f Source #

Constructors

Minimal
Skolem Int
Function f

Instances

Functor Extended Source #
Methods fmap :: (a -> b) -> Extended a -> Extended b # (<$) :: a -> Extended b -> Extended a #
Eq f => Eq (Extended f) Source #
Methods (==) :: Extended f -> Extended f -> Bool # (/=) :: Extended f -> Extended f -> Bool #
Ord f => Ord (Extended f) Source #
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) Source #
Methods showsPrec :: Int -> Extended f -> ShowS # show :: Extended f -> String # showList :: [Extended f] -> ShowS #
Pretty f => Pretty (Extended f) Source #
Methods pPrintPrec :: PrettyLevel -> Rational -> Extended f -> Doc # pPrint :: Extended f -> Doc # pPrintList :: PrettyLevel -> [Extended f] -> Doc #
Numbered f => Numbered (Extended f) Source #
Methods fromInt :: Int -> Extended f Source # toInt :: Extended f -> Int Source #
PrettyTerm f => PrettyTerm (Extended f) Source #
Methods termStyle :: Extended f -> TermStyle Source #
Minimal (Extended f) Source #
Methods minimal :: Extended f Source #
Sized f => Sized (Extended f) Source #
Methods size :: Extended f -> Int Source #
Arity f => Arity (Extended f) Source #
Methods arity :: Extended f -> Int Source #
Skolem (Extended f) Source #
Methods skolem :: Var -> Extended f Source #

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

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

module Twee.Term

module Twee.Pretty