twee-lib-2.4.2: An equational theorem prover
Safe HaskellSafe-Inferred
LanguageHaskell2010

Twee.CP

Description

Critical pair generation.

Synopsis

Documentation

data Positions f Source #

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

Constructors

NilP 
ConsP !Int !(Positions f) 

Instances

Instances details
Show (Positions f) Source # 
Instance details

Defined in Twee.CP

data Positions2 f Source #

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

Constructors

ForwardsPos !(Positions f) 
BothPos !(Positions f) !(Positions f) 

Instances

Instances details
f ~ g => Has (Active f) (Positions2 g) Source # 
Instance details

Defined in Twee

Methods

the :: Active f -> Positions2 g Source #

positions :: Term f -> Positions f Source #

Calculate the set of positions for a term.

positionsRule :: Rule f -> Positions2 f Source #

Calculate the set of positions for a rule.

positionsChurch :: Positions f -> ChurchList Int Source #

data Overlap a f Source #

A critical overlap of one rule with another.

Constructors

Overlap 

Fields

Instances

Instances details
(Labelled f, Show a, Show f) => Show (Overlap a f) Source # 
Instance details

Defined in Twee.CP

Methods

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

show :: Overlap a f -> String #

showList :: [Overlap a f] -> ShowS #

data How Source #

Constructors

How 

Instances

Instances details
Show How Source # 
Instance details

Defined in Twee.CP

Methods

showsPrec :: Int -> How -> ShowS #

show :: How -> String #

showList :: [How] -> ShowS #

Serialize How Source # 
Instance details

Defined in Twee.CP

Methods

put :: Putter How #

get :: Get How #

Eq How Source # 
Instance details

Defined in Twee.CP

Methods

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

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

Ord How Source # 
Instance details

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 #

newtype Depth Source #

Represents the depth of a critical pair.

Constructors

Depth Int 

Instances

Instances details
Enum Depth Source # 
Instance details

Defined in Twee.CP

Num Depth Source # 
Instance details

Defined in Twee.CP

Integral Depth Source # 
Instance details

Defined in Twee.CP

Real Depth Source # 
Instance details

Defined in Twee.CP

Methods

toRational :: Depth -> Rational #

Show Depth Source # 
Instance details

Defined in Twee.CP

Methods

showsPrec :: Int -> Depth -> ShowS #

show :: Depth -> String #

showList :: [Depth] -> ShowS #

Eq Depth Source # 
Instance details

Defined in Twee.CP

Methods

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

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

Ord Depth Source # 
Instance details

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 Source # 
Instance details

Defined in Twee

Methods

the :: Active f -> Depth Source #

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] Source #

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) Source #

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

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

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

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) Source #

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

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

data Config Source #

The configuration for the critical pair weighting heuristic.

defaultConfig :: Config Source #

The default heuristic configuration.

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

Compute a score for a critical pair.

Higher-level handling of critical pairs.

data CriticalPair f Source #

A critical pair together with information about how it was derived

Constructors

CriticalPair 

Fields

Instances

Instances details
(Labelled f, PrettyTerm f) => Pretty (CriticalPair f) Source # 
Instance details

Defined in Twee.CP

Symbolic (CriticalPair f) Source # 
Instance details

Defined in Twee.CP

Associated Types

type ConstantOf (CriticalPair f) Source #

type ConstantOf (CriticalPair f) Source # 
Instance details

Defined in Twee.CP

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

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 Source #

Make a critical pair from two rules and an overlap.