Twee

Documentation

data Twee f

Constructors

Twee

Fields

• maxSize :: Maybe Int
• labelledRules :: !(Indexes (Labelled (Modelled (Critical (Rule f)))))
• extraRules :: !(Indexes (Rule f))
• cancellationRules :: !(Index (Labelled (CancellationRule f)))
• goals :: [Set (Term f)]
• totalCPs :: Int
• processedCPs :: Int
• renormaliseAt :: Int
• minimumCPSetSize :: Int
• cpSplits :: Int
• queue :: !(Queue (Mix (Either1 FIFO Heap)) (Passive f))
• useGeneralSuperpositions :: Bool
• useGroundJoining :: Bool
• useConnectedness :: Bool
• useSetJoining :: Bool
• useSetJoiningForGoals :: Bool
• useCancellation :: Bool
• maxCancellationSize :: Maybe Int
• atomicCancellation :: Bool
• unifyConstantsInCancellation :: Bool
• useInterreduction :: Bool
• useUnsafeInterreduction :: Bool
• skipCompositeSuperpositions :: Bool
• tracing :: Bool
• moreTracing :: Bool
• lhsWeight :: Int
• rhsWeight :: Int
• joinStatistics :: Map JoinReason Int

Instances

Show f => Show (Twee f)

Methods

showsPrec :: Int -> Twee f -> ShowS

show :: Twee f -> String

showList :: [Twee f] -> ShowS

initialState :: Int -> Int -> Twee f

addGoals :: [Set (Term f)] -> Twee f -> Twee f

report :: Function f => Twee f -> String

enqueueM :: Function f => Passive f -> State (Twee f) ()

reenqueueM :: Function f => Passive f -> State (Twee f) ()

dequeueM :: Function f => State (Twee f) (Maybe (Passive f))

newLabelM :: State (Twee f) Label

data Modelled a

Constructors

Modelled

Fields

• model :: Model (ConstantOf a)
• positions :: [Int]
• modelled :: a

Instances

Eq a => Eq (Modelled a)

Methods

(==) :: Modelled a -> Modelled a -> Bool

(/=) :: Modelled a -> Modelled a -> Bool

Ord a => Ord (Modelled a)

Methods

compare :: Modelled a -> Modelled a -> Ordering

(<) :: Modelled a -> Modelled a -> Bool

(<=) :: Modelled a -> Modelled a -> Bool

(>) :: Modelled a -> Modelled a -> Bool

(>=) :: Modelled a -> Modelled a -> Bool

max :: Modelled a -> Modelled a -> Modelled a

min :: Modelled a -> Modelled a -> Modelled a

(Show a, Show (ConstantOf a)) => Show (Modelled a)

Methods

showsPrec :: Int -> Modelled a -> ShowS

show :: Modelled a -> String

showList :: [Modelled a] -> ShowS

(PrettyTerm (ConstantOf a), Pretty a) => Pretty (Modelled a)

Methods

pPrintPrec :: PrettyLevel -> Rational -> Modelled a -> Doc

pPrint :: Modelled a -> Doc

pPrintList :: PrettyLevel -> [Modelled a] -> Doc

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

Rated a => Rated (Modelled a)

Methods

rating :: Modelled a -> Int

maxRating :: Modelled a -> Int

type ConstantOf (Modelled a)

type ConstantOf (Modelled a) = ConstantOf a

rulesFor :: Function f => Int -> Twee f -> Frozen (Rule f)

easyRules :: Function f => Twee f -> Frozen (Rule f)

rules :: Function f => Twee f -> Frozen (Rule f)

allRules :: Function f => Twee f -> Frozen (Rule f)

normaliseQuickly :: Function f => Twee f -> Term f -> Reduction f

normalise :: Function f => Twee f -> Term f -> Reduction f

normaliseIn :: Function f => Twee f -> Model f -> Term f -> Reduction f

normaliseSub :: Function f => Twee f -> Term f -> Term f -> Reduction f

normaliseSkolem :: Function f => Twee f -> Term f -> Reduction f

reduceCP :: Function f => Twee f -> JoinStage -> (Term f -> Term f) -> Critical (Equation f) -> Either JoinReason (Critical (Equation f))

data JoinStage

Constructors

Initial

Simplification

Reducing

Subjoining

Instances

Eq JoinStage

Methods

(==) :: JoinStage -> JoinStage -> Bool

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

Ord JoinStage

Methods

compare :: JoinStage -> JoinStage -> Ordering

(<) :: JoinStage -> JoinStage -> Bool

(<=) :: JoinStage -> JoinStage -> Bool

(>) :: JoinStage -> JoinStage -> Bool

(>=) :: JoinStage -> JoinStage -> Bool

max :: JoinStage -> JoinStage -> JoinStage

min :: JoinStage -> JoinStage -> JoinStage

Show JoinStage

Methods

showsPrec :: Int -> JoinStage -> ShowS

show :: JoinStage -> String

showList :: [JoinStage] -> ShowS

Pretty JoinStage

Methods

pPrintPrec :: PrettyLevel -> Rational -> JoinStage -> Doc

pPrint :: JoinStage -> Doc

pPrintList :: PrettyLevel -> [JoinStage] -> Doc

data JoinReason

Constructors

Trivial JoinStage

Subsumed JoinStage

SetJoining

GroundJoined

Instances

Eq JoinReason

Methods

(==) :: JoinReason -> JoinReason -> Bool

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

Ord JoinReason

Methods

compare :: JoinReason -> JoinReason -> Ordering

(<) :: JoinReason -> JoinReason -> Bool

(<=) :: JoinReason -> JoinReason -> Bool

(>) :: JoinReason -> JoinReason -> Bool

(>=) :: JoinReason -> JoinReason -> Bool

max :: JoinReason -> JoinReason -> JoinReason

min :: JoinReason -> JoinReason -> JoinReason

Show JoinReason

Methods

showsPrec :: Int -> JoinReason -> ShowS

show :: JoinReason -> String

showList :: [JoinReason] -> ShowS

Pretty JoinReason

Methods

pPrintPrec :: PrettyLevel -> Rational -> JoinReason -> Doc

pPrint :: JoinReason -> Doc

pPrintList :: PrettyLevel -> [JoinReason] -> Doc

normaliseCPQuickly :: Function f => Twee f -> Critical (Equation f) -> Either JoinReason (Critical (Equation f))

normaliseCPReducing :: Function f => Twee f -> Critical (Equation f) -> Either JoinReason (Critical (Equation f))

normaliseCP :: Function f => Twee f -> Critical (Equation f) -> Either JoinReason (Critical (Equation f))

complete :: Function f => State (Twee f) ()

complete1 :: Function f => State (Twee f) Bool

renormaliseGoals :: Function f => State (Twee f) ()

normaliseCPs :: forall f. Function f => State (Twee f) ()

consider :: Function f => Int -> Label -> Label -> Critical (Equation f) -> State (Twee f) Bool

groundJoinableEq :: Function f => Twee f -> Equation f -> Bool

groundJoinable :: Function f => Twee f -> Critical (Equation f) -> Bool

groundJoin :: Function f => Twee f -> [Branch f] -> Critical (Equation f) -> Either (Model f) [Critical (Equation f)]

valid :: Function f => Model f -> Reduction f -> Bool

optimise :: a -> (a -> [a]) -> (a -> Bool) -> a

addRule :: Function f => Modelled (Critical (Rule f)) -> State (Twee f) Label

addExtraRule :: Function f => Rule f -> State (Twee f) ()

extraRuleSafe :: Function f => Twee f -> Rule f -> Bool

deleteRule :: Function f => Label -> Modelled (Critical (Rule f)) -> State (Twee f) ()

data Simplification f

Constructors

Simplify (Model f) (Modelled (Critical (Rule f)))

Reorient (Modelled (Critical (Rule f)))

Instances

Show f => Show (Simplification f)

Methods

showsPrec :: Int -> Simplification f -> ShowS

show :: Simplification f -> String

showList :: [Simplification f] -> ShowS

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

Methods

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

pPrint :: Simplification f -> Doc

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

interreduce :: Function f => Rule f -> State (Twee f) ()

reduceWith :: Function f => Twee f -> Label -> Rule f -> Modelled (Critical (Rule f)) -> Maybe (Simplification f)

simplifyRule :: Function f => Label -> Model f -> Modelled (Critical (Rule f)) -> State (Twee f) ()

newEquation :: Function f => Equation f -> State (Twee f) ()

noCritInfo :: Function f => CritInfo f

data CancellationRule f

Constructors

CancellationRule

Fields

• cr_unified :: [[Term f]]
• cr_rule :: !(Rule f)

Instances

Show (CancellationRule f)

Methods

showsPrec :: Int -> CancellationRule f -> ShowS

show :: CancellationRule f -> String

showList :: [CancellationRule f] -> ShowS

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

Methods

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

pPrint :: CancellationRule f -> Doc

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

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

type ConstantOf (CancellationRule f)

type ConstantOf (CancellationRule f) = f

toCancellationRule :: Function f => Twee f -> Rule f -> Maybe (CancellationRule f)

addCancellationRule :: Function f => Label -> Rule f -> Twee f -> Twee f

deleteCancellationRule :: Function f => Label -> Rule f -> Twee f -> Twee f

data Critical a

Constructors

Critical

Fields

• critInfo :: CritInfo (ConstantOf a)
• critical :: a

Instances

Eq a => Eq (Critical a)

Methods

(==) :: Critical a -> Critical a -> Bool

(/=) :: Critical a -> Critical a -> Bool

Ord a => Ord (Critical a)

Methods

compare :: Critical a -> Critical a -> Ordering

(<) :: Critical a -> Critical a -> Bool

(<=) :: Critical a -> Critical a -> Bool

(>) :: Critical a -> Critical a -> Bool

(>=) :: Critical a -> Critical a -> Bool

max :: Critical a -> Critical a -> Critical a

min :: Critical a -> Critical a -> Critical a

(Show a, Show (ConstantOf a)) => Show (Critical a)

Methods

showsPrec :: Int -> Critical a -> ShowS

show :: Critical a -> String

showList :: [Critical a] -> ShowS

(PrettyTerm (ConstantOf a), Pretty a) => Pretty (Critical a)

Methods

pPrintPrec :: PrettyLevel -> Rational -> Critical a -> Doc

pPrint :: Critical a -> Doc

pPrintList :: PrettyLevel -> [Critical a] -> Doc

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

Rated a => Rated (Critical a)

Methods

rating :: Critical a -> Int

maxRating :: Critical a -> Int

type ConstantOf (Critical a)

type ConstantOf (Critical a) = ConstantOf a

data CritInfo f

Constructors

CritInfo

Fields

• top :: Term f
• overlap :: Int

Instances

Show f => Show (CritInfo f)

Methods

showsPrec :: Int -> CritInfo f -> ShowS

show :: CritInfo f -> String

showList :: [CritInfo f] -> ShowS

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

type ConstantOf (CritInfo f)

type ConstantOf (CritInfo f) = f

data CPInfo

Constructors

CPInfo

Fields

• cpWeight :: !Int
• cpWeight2 :: !Int
• cpAge1 :: !Label
• cpAge2 :: !Label

Instances

Eq CPInfo

Methods

(==) :: CPInfo -> CPInfo -> Bool

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

Ord CPInfo

Methods

compare :: CPInfo -> CPInfo -> Ordering

(<) :: CPInfo -> CPInfo -> Bool

(<=) :: CPInfo -> CPInfo -> Bool

(>) :: CPInfo -> CPInfo -> Bool

(>=) :: CPInfo -> CPInfo -> Bool

max :: CPInfo -> CPInfo -> CPInfo

min :: CPInfo -> CPInfo -> CPInfo

Show CPInfo

Methods

showsPrec :: Int -> CPInfo -> ShowS

show :: CPInfo -> String

showList :: [CPInfo] -> ShowS

data CP f

Constructors

CP

Fields

• info :: !CPInfo
• cp :: !(Critical (Equation f))
• l1 :: !Label
• l2 :: !Label

Instances

Eq (CP f)

Methods

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

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

Ord (CP f)

Methods

compare :: CP f -> CP f -> Ordering

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

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

(>) :: CP f -> CP f -> Bool

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

max :: CP f -> CP f -> CP f

min :: CP f -> CP f -> CP f

Show f => Show (CP f)

Methods

showsPrec :: Int -> CP f -> ShowS

show :: CP f -> String

showList :: [CP f] -> ShowS

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

Methods

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

pPrint :: CP f -> Doc

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

Labels (CP f)

Methods

labels :: CP f -> [Label]

data CPs f

Constructors

CPs

Fields

• best :: !CPInfo
• label :: !Label
• lower :: !Label
• upper :: !Label
• count :: !Int
• from :: !(Labelled (Rule f))

Instances

Eq (CPs f)

Methods

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

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

Ord (CPs f)

Methods

compare :: CPs f -> CPs f -> Ordering

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

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

(>) :: CPs f -> CPs f -> Bool

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

max :: CPs f -> CPs f -> CPs f

min :: CPs f -> CPs f -> CPs f

Show (CPs f)

Methods

showsPrec :: Int -> CPs f -> ShowS

show :: CPs f -> String

showList :: [CPs f] -> ShowS

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

Methods

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

pPrint :: CPs f -> Doc

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

Labels (CPs f)

Methods

labels :: CPs f -> [Label]

data Passive f

Constructors

SingleCP !(CP f)

ManyCPs !(CPs f)

Instances

Eq (Passive f)

Methods

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

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

Ord (Passive f)

Methods

compare :: Passive f -> Passive f -> Ordering

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

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

(>) :: Passive f -> Passive f -> Bool

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

max :: Passive f -> Passive f -> Passive f

min :: Passive f -> Passive f -> Passive f

Show f => Show (Passive f)

Methods

showsPrec :: Int -> Passive f -> ShowS

show :: Passive f -> String

showList :: [Passive f] -> ShowS

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

Methods

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

pPrint :: Passive f -> Doc

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

Labels (Passive f)

Methods

labels :: Passive f -> [Label]

passiveCount :: Passive f -> Int

data InitialCP f

Constructors

InitialCP

Fields

• cpId :: (Term f, Label)
• cpOK :: Bool
• cpCP :: Labelled (Critical (Equation f))

criticalPairs :: Function f => Twee f -> Label -> Label -> Rule f -> [Labelled (Critical (Equation f))]

ruleOverlaps :: Twee f -> Term f -> [Int]

overlaps :: [Int] -> Term f -> Term f -> [(Subst f, Int)]

emitReplacement :: Int -> Term f -> TermList f -> Builder f

criticalPairs1 :: Function f => Twee f -> [Int] -> Rule f -> [Labelled (Rule f)] -> [Labelled (Critical (Equation f))]

queueCP :: Function f => (Passive f -> State (Twee f) ()) -> (Equation f -> Bool) -> Label -> Label -> Critical (Equation f) -> State (Twee f) ()

queueCPs :: (Function f, Ord a) => (Passive f -> State (Twee f) ()) -> Label -> Label -> (Label -> a) -> Labelled (Rule f) -> State (Twee f) ()

queueCPsSplit :: Function f => (Passive f -> State (Twee f) ()) -> Label -> Label -> Labelled (Rule f) -> State (Twee f) ()

toCPs :: Function f => Twee f -> Label -> Label -> Labelled (Rule f) -> [CP f]

toCP :: Function f => Twee f -> Label -> Label -> (Equation f -> Bool) -> Critical (Equation f) -> Maybe (CP f)

cancelledWeight :: Function f => Twee f -> (Equation f -> Bool) -> Equation f -> Int

bestCancellation :: Function f => Twee f -> (Equation f -> Bool) -> Equation f -> (Int, Equation f)

weight :: Function f => Twee f -> Equation f -> Int

weight' :: Function f => Twee f -> Equation f -> Int

cancellations :: Function f => Twee f -> (Equation f -> Bool) -> Equation f -> [Equation f]

data Event f

Constructors

NewRule (Rule f)

ExtraRule (Rule f)

NewCP (Passive f)

Reduce (Simplification f) (Rule f)

Consider (Critical (Equation f))

Joined (Critical (Equation f)) JoinReason

Delay (Critical (Equation f))

Cancel (Critical (Equation f)) (Equation f)

Discharge (Critical (Equation f)) (Model f)

NormaliseCPs (Twee f)

trace :: Function f => Twee f -> Event f -> a -> a

traceM :: Function f => Event f -> State (Twee f) ()

traceIf :: Bool -> Doc -> a -> a

Orphan instances

Rated a => Rated (Labelled a)

Methods

rating :: Labelled a -> Int

maxRating :: Labelled a -> Int

Rated (Rule f)

Methods

rating :: Rule f -> Int

maxRating :: Rule f -> Int