Twee.CP

Critical pair generation.

Documentation

data Positions f

The set of positions at which a term can have critical overlaps.

Constructors

NilP

ConsP !Int !(Positions f)

Instances

Show (Positions f)

Defined in Twee.CP

Methods

showsPrec :: Int -> Positions f -> ShowS

show :: Positions f -> String

showList :: [Positions f] -> ShowS

type PositionsOf a = Positions (ConstantOf a)

data Positions2 f

Like Positions but for an equation (one set of positions per term).

Constructors

ForwardsPos !(Positions f)

BothPos !(Positions f) !(Positions f)

Instances

f ~ g => Has (Active f) (Positions2 g)

Defined in Twee

Methods

the :: Active f -> Positions2 g

positions :: Term f -> Positions f

Calculate the set of positions for a term.

positionsRule :: Rule f -> Positions2 f

Calculate the set of positions for a rule.

positionsChurch :: Positions f -> ChurchList Int

data Overlap a f

A critical overlap of one rule with another.

Constructors

Overlap

Fields

• overlap_rule1 :: !a

  The rule which applies at the root.

• overlap_rule2 :: !a

  The rule which applies at some subterm.

• overlap_how :: !How

  The position in the critical term which is rewritten, together with the direction of the two rules.

• overlap_top :: !(Term f)

  The top term of the critical pair

• overlap_eqn :: !(Equation f)

  The critical pair itself.

Instances

(Labelled f, Show a, Show f) => Show (Overlap a f)

Defined in Twee.CP

Methods

showsPrec :: Int -> Overlap a f -> ShowS

show :: Overlap a f -> String

showList :: [Overlap a f] -> ShowS

data How

Constructors

How

Fields

• how_pos :: !Int
• how_dir1 :: !Direction
• how_dir2 :: !Direction

Instances

Show How

Defined in Twee.CP

Methods

showsPrec :: Int -> How -> ShowS

show :: How -> String

showList :: [How] -> ShowS

Serialize How

Defined in Twee.CP

Methods

put :: Putter How

get :: Get How

Eq How

Defined in Twee.CP

Methods

(==) :: How -> How -> Bool

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

Ord How

Defined in Twee.CP

Methods

compare :: How -> How -> Ordering

(<) :: How -> How -> Bool

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

(>) :: How -> How -> Bool

(>=) :: How -> How -> Bool

max :: How -> How -> How

min :: How -> How -> How

data Direction

Constructors

Forwards

Backwards

Instances

Enum Direction

Defined in Twee.CP

Methods

succ :: Direction -> Direction

pred :: Direction -> Direction

toEnum :: Int -> Direction

fromEnum :: Direction -> Int

enumFrom :: Direction -> [Direction]

enumFromThen :: Direction -> Direction -> [Direction]

enumFromTo :: Direction -> Direction -> [Direction]

enumFromThenTo :: Direction -> Direction -> Direction -> [Direction]

Show Direction

Defined in Twee.CP

Methods

showsPrec :: Int -> Direction -> ShowS

show :: Direction -> String

showList :: [Direction] -> ShowS

Eq Direction

Defined in Twee.CP

Methods

(==) :: Direction -> Direction -> Bool

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

Ord Direction

Defined in Twee.CP

Methods

compare :: Direction -> Direction -> Ordering

(<) :: Direction -> Direction -> Bool

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

(>) :: Direction -> Direction -> Bool

(>=) :: Direction -> Direction -> Bool

max :: Direction -> Direction -> Direction

min :: Direction -> Direction -> Direction

direct :: Rule f -> Direction -> Rule f

newtype Depth

Represents the depth of a critical pair.

Constructors

Depth Int

Instances

Enum Depth

Defined in Twee.CP

Methods

succ :: Depth -> Depth

pred :: Depth -> Depth

toEnum :: Int -> Depth

fromEnum :: Depth -> Int

enumFrom :: Depth -> [Depth]

enumFromThen :: Depth -> Depth -> [Depth]

enumFromTo :: Depth -> Depth -> [Depth]

enumFromThenTo :: Depth -> Depth -> Depth -> [Depth]

Num Depth

Defined in Twee.CP

Methods

(+) :: Depth -> Depth -> Depth

(-) :: Depth -> Depth -> Depth

(*) :: Depth -> Depth -> Depth

negate :: Depth -> Depth

abs :: Depth -> Depth

signum :: Depth -> Depth

fromInteger :: Integer -> Depth

Integral Depth

Defined in Twee.CP

Methods

quot :: Depth -> Depth -> Depth

rem :: Depth -> Depth -> Depth

div :: Depth -> Depth -> Depth

mod :: Depth -> Depth -> Depth

quotRem :: Depth -> Depth -> (Depth, Depth)

divMod :: Depth -> Depth -> (Depth, Depth)

toInteger :: Depth -> Integer

Real Depth

Defined in Twee.CP

Methods

toRational :: Depth -> Rational

Show Depth

Defined in Twee.CP

Methods

showsPrec :: Int -> Depth -> ShowS

show :: Depth -> String

showList :: [Depth] -> ShowS

Eq Depth

Defined in Twee.CP

Methods

(==) :: Depth -> Depth -> Bool

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

Ord Depth

Defined in Twee.CP

Methods

compare :: Depth -> Depth -> Ordering

(<) :: Depth -> Depth -> Bool

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

(>) :: Depth -> Depth -> Bool

(>=) :: Depth -> Depth -> Bool

max :: Depth -> Depth -> Depth

min :: Depth -> Depth -> Depth

Has (Active f) Depth

Defined in Twee

Methods

the :: Active f -> Depth

overlaps :: forall a b f. (Function f, Has a (Rule f), Has b (Rule f), Has b (Positions2 f)) => Index f a -> [b] -> b -> [Overlap b f]

Compute all overlaps of a rule with a set of rules.

overlapsChurch :: forall f a b. (Function f, Has a (Rule f), Has b (Rule f), Has b (Positions2 f)) => Index f a -> [b] -> b -> ChurchList (Overlap b f)

directions :: Rule f -> Positions2 f -> ChurchList (Direction, Positions f, Equation f)

asymmetricOverlaps :: (Function f, Has a (Rule f)) => Index f a -> b -> b -> Direction -> Direction -> Positions f -> Equation f -> Equation f -> ChurchList (Overlap b f)

overlapAt :: How -> a -> a -> Rule f -> Rule f -> Maybe (Overlap a f)

Create an overlap at a particular position in a term. Doesn't simplify the overlap.

overlapAt' :: How -> a -> a -> Equation f -> Equation f -> Maybe (Overlap a f)

simplifyOverlap :: (Function f, Has a (Rule f)) => Index f a -> Overlap b f -> Maybe (Overlap b f)

Simplify an overlap and remove it if it's trivial.

buildReplacePositionSub :: TriangleSubst f -> Int -> TermList f -> TermList f -> Term f

termSubst :: TriangleSubst f -> Term f -> Term f

data Config

The configuration for the critical pair weighting heuristic.

Constructors

Config

Fields

• cfg_lhsweight :: !Int
• cfg_rhsweight :: !Int
• cfg_funweight :: !Int
• cfg_varweight :: !Int
• cfg_depthweight :: !Int
• cfg_dupcost :: !Int
• cfg_dupfactor :: !Int

defaultConfig :: Config

The default heuristic configuration.

score :: Function f => Config -> Depth -> Overlap a f -> Int

Compute a score for a critical pair.

Higher-level handling of critical pairs.

data CriticalPair f

A critical pair together with information about how it was derived

Constructors

CriticalPair

Fields

• cp_eqn :: !(Equation f)

  The critical pair itself.

• cp_top :: !(Maybe (Term f))

  The critical term, if there is one. (Axioms do not have a critical term.)

• cp_proof :: !(Derivation f)

  A derivation of the critical pair from the axioms.

Instances

(Labelled f, PrettyTerm f) => Pretty (CriticalPair f)

Defined in Twee.CP

Methods

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

pPrint :: CriticalPair f -> Doc

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

Symbolic (CriticalPair f)

Defined in Twee.CP

Associated Types

type ConstantOf (CriticalPair f)

Methods

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

subst_ :: (Var -> BuilderOf (CriticalPair f)) -> CriticalPair f -> CriticalPair f

type ConstantOf (CriticalPair f)

Defined in Twee.CP

type ConstantOf (CriticalPair f) = f

split :: Function f => CriticalPair f -> [CriticalPair f]

Split a critical pair so that it can be turned into rules.

The resulting critical pairs have the property that no variable appears on the right that is not on the left.

makeCriticalPair :: (Function f, Has a (Rule f)) => Overlap a f -> CriticalPair f

Make a critical pair from two rules and an overlap.