twee-lib-2.3.1: An equational theorem prover
Safe HaskellNone
LanguageHaskell2010

Twee.CP

Description

Critical pair generation.

Synopsis

Documentation

newtype Max Source #

Constructors

Max 

Fields

Instances

Instances details
Eq Max Source # 
Instance details

Defined in Twee.CP

Methods

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

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

Ord Max Source # 
Instance details

Defined in Twee.CP

Methods

compare :: Max -> Max -> Ordering #

(<) :: Max -> Max -> Bool #

(<=) :: Max -> Max -> Bool #

(>) :: Max -> Max -> Bool #

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

max :: Max -> Max -> Max #

min :: Max -> Max -> Max #

Show Max Source # 
Instance details

Defined in Twee.CP

Methods

showsPrec :: Int -> Max -> ShowS #

show :: Max -> String #

showList :: [Max] -> ShowS #

Has (ActiveRule f) Max Source # 
Instance details

Defined in Twee

Methods

the :: ActiveRule f -> Max Source #

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

f ~ g => Has (ActiveRule f) (Positions g) Source # 
Instance details

Defined in Twee

Methods

the :: ActiveRule f -> Positions g Source #

positions :: Term f -> Positions f Source #

Calculate the set of positions for a term.

positionsChurch :: Positions f -> ChurchList Int Source #

data Overlap f Source #

A critical overlap of one rule with another.

Constructors

Overlap 

Fields

Instances

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

Defined in Twee.CP

Methods

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

show :: Overlap f -> String #

showList :: [Overlap f] -> ShowS #

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

Eq Depth Source # 
Instance details

Defined in Twee.CP

Methods

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

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

Integral Depth Source # 
Instance details

Defined in Twee.CP

Num Depth Source # 
Instance details

Defined in Twee.CP

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 #

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 #

Has (ActiveRule f) Depth Source # 
Instance details

Defined in Twee

Methods

the :: ActiveRule f -> Depth Source #

overlaps :: forall a f. (Function f, Has a Id, Has a (Rule f), Has a (Positions f), Has a Depth) => Depth -> Index f a -> [a] -> a -> [(a, a, Overlap f)] Source #

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

overlapsChurch :: forall f a. (Function f, Has a (Rule f), Has a (Positions f), Has a Depth) => Depth -> Index f a -> [a] -> a -> ChurchList (a, a, Overlap f) Source #

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

overlapAt :: Int -> Depth -> Rule f -> Rule f -> Maybe (Overlap f) Source #

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

simplifyOverlap :: (Function f, Has a (Rule f)) => Index f a -> Overlap f -> Maybe (Overlap 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 -> Overlap 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 :: forall f a. (Has a (Rule f), Has a Id, Has a Max, Function f) => a -> a -> Overlap f -> CriticalPair f Source #

Make a critical pair from two rules and an overlap.

overlapProof :: forall a f. (Has a (Rule f), Has a Id) => a -> a -> Overlap f -> Derivation f Source #

Return a proof for a critical pair.