Twee.Rule

Documentation

data Rule f

Constructors

Rule

Fields

• orientation :: Orientation f
• lhs :: Term f
• rhs :: Term f

Instances

Eq (Rule f)

Methods

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

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

Ord (Rule f)

Methods

compare :: Rule f -> Rule f -> Ordering

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

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

(>) :: Rule f -> Rule f -> Bool

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

max :: Rule f -> Rule f -> Rule f

min :: Rule f -> Rule f -> Rule f

Show (Rule f)

Methods

showsPrec :: Int -> Rule f -> ShowS

show :: Rule f -> String

showList :: [Rule f] -> ShowS

(Numbered f, PrettyTerm f) => Pretty (Rule f)

Methods

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

pPrint :: Rule f -> Doc

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

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

type ConstantOf (Rule f)

type ConstantOf (Rule f) = f

data Orientation f

Constructors

Oriented

WeaklyOriented [Term f]

Permutative [(Term f, Term f)]

Unoriented

Instances

Eq (Orientation f)

Methods

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

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

Ord (Orientation f)

Methods

compare :: Orientation f -> Orientation f -> Ordering

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

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

(>) :: Orientation f -> Orientation f -> Bool

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

max :: Orientation f -> Orientation f -> Orientation f

min :: Orientation f -> Orientation f -> Orientation f

Show (Orientation f)

Methods

showsPrec :: Int -> Orientation f -> ShowS

show :: Orientation f -> String

showList :: [Orientation f] -> ShowS

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

type ConstantOf (Orientation f)

type ConstantOf (Orientation f) = f

oriented :: Orientation f -> Bool

pPrintRule :: (Numbered f, PrettyTerm f) => Term f -> Term f -> Doc

data Equation f

Constructors

(Term f) :=: (Term f)

Instances

Eq (Equation f)

Methods

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

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

Ord (Equation f)

Methods

compare :: Equation f -> Equation f -> Ordering

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

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

(>) :: Equation f -> Equation f -> Bool

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

max :: Equation f -> Equation f -> Equation f

min :: Equation f -> Equation f -> Equation f

Show (Equation f)

Methods

showsPrec :: Int -> Equation f -> ShowS

show :: Equation f -> String

showList :: [Equation f] -> ShowS

(Numbered f, PrettyTerm f) => Pretty (Equation f)

Methods

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

pPrint :: Equation f -> Doc

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

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

Methods

size :: Equation f -> Int

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

type ConstantOf (Equation f)

type ConstantOf (Equation f) = f

type EquationOf a = Equation (ConstantOf a)

order :: Function f => Equation f -> Equation f

unorient :: Rule f -> Equation f

orient :: Function f => Equation f -> [Rule f]

rule :: Function f => Term f -> Term f -> Rule f

bothSides :: (Term f -> Term f') -> Equation f -> Equation f'

trivial :: Eq f => Equation f -> Bool

type Strategy f = Term f -> [Reduction f]

data Reduction f

Constructors

Step (Rule f) (Subst f)

Trans (Reduction f) (Reduction f)

Parallel [(Int, Reduction f)] (Term f)

Instances

Show (Reduction f)

Methods

showsPrec :: Int -> Reduction f -> ShowS

show :: Reduction f -> String

showList :: [Reduction f] -> ShowS

(Numbered f, PrettyTerm f) => Pretty (Reduction f)

Methods

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

pPrint :: Reduction f -> Doc

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

result :: Reduction f -> Term f

pPrintReduction :: (Numbered f, PrettyTerm f) => Reduction f -> Doc

steps :: Reduction f -> [(Rule f, Subst f)]

anywhere1 :: (Numbered f, PrettyTerm f) => Strategy f -> Reduction f -> Maybe (Reduction f)

normaliseWith :: (Numbered f, PrettyTerm f) => Strategy f -> Term f -> Reduction f

normalForms :: Function f => Strategy f -> [Term f] -> Set (Term f)

anywhere :: Strategy f -> Strategy f

nested :: Strategy f -> Strategy f

rewrite :: Function f => String -> (Rule f -> Subst f -> Bool) -> Frozen (Rule f) -> Strategy f

tryRule :: Function f => (Rule f -> Subst f -> Bool) -> Rule f -> Strategy f

simplifies :: Function f => Rule f -> Subst f -> Bool

reducesWith :: Function f => (Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool

reduces :: Function f => Rule f -> Subst f -> Bool

reducesInModel :: Function f => Model f -> Rule f -> Subst f -> Bool

reducesSkolem :: Function f => Rule f -> Subst f -> Bool

reducesSub :: Function f => Term f -> Rule f -> Subst f -> Bool