Safe Haskell  SafeInferred 

Language  Haskell2010 
Critical pair generation.
Synopsis
 data Positions f
 type PositionsOf a = Positions (ConstantOf a)
 data Positions2 f
 = ForwardsPos !(Positions f)
  BothPos !(Positions f) !(Positions f)
 positions :: Term f > Positions f
 positionsRule :: Rule f > Positions2 f
 positionsChurch :: Positions f > ChurchList Int
 data Overlap a f = Overlap {
 overlap_rule1 :: !a
 overlap_rule2 :: !a
 overlap_how :: !How
 overlap_top :: !(Term f)
 overlap_eqn :: !(Equation f)
 data How = How {}
 data Direction
 direct :: Rule f > Direction > Rule f
 newtype Depth = Depth Int
 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]
 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)
 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)
 buildReplacePositionSub :: TriangleSubst f > Int > TermList f > TermList f > Term f
 termSubst :: TriangleSubst f > Term f > Term f
 data Config = Config {
 cfg_lhsweight :: !Int
 cfg_rhsweight :: !Int
 cfg_funweight :: !Int
 cfg_varweight :: !Int
 cfg_depthweight :: !Int
 cfg_dupcost :: !Int
 cfg_dupfactor :: !Int
 defaultConfig :: Config
 score :: Function f => Config > Depth > Overlap a f > Int
 data CriticalPair f = CriticalPair {}
 split :: Function f => CriticalPair f > [CriticalPair f]
 makeCriticalPair :: (Function f, Has a (Rule f)) => Overlap a f > CriticalPair f
Documentation
The set of positions at which a term can have critical overlaps.
type PositionsOf a = Positions (ConstantOf a) Source #
data Positions2 f Source #
Like Positions but for an equation (one set of positions per term).
ForwardsPos !(Positions f)  
BothPos !(Positions f) !(Positions f) 
positionsRule :: Rule f > Positions2 f Source #
Calculate the set of positions for a rule.
positionsChurch :: Positions f > ChurchList Int Source #
A critical overlap of one rule with another.
Overlap  

Instances
Enum Direction Source #  
Defined in Twee.CP succ :: Direction > Direction # pred :: Direction > Direction # fromEnum :: Direction > Int # enumFrom :: Direction > [Direction] # enumFromThen :: Direction > Direction > [Direction] # enumFromTo :: Direction > Direction > [Direction] # enumFromThenTo :: Direction > Direction > Direction > [Direction] #  
Show Direction Source #  
Eq Direction Source #  
Ord Direction Source #  
Defined in Twee.CP 
Represents the depth of a critical pair.
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.
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.
buildReplacePositionSub :: TriangleSubst f > Int > TermList f > TermList f > Term f Source #
The configuration for the critical pair weighting heuristic.
Config  

defaultConfig :: Config Source #
The default heuristic configuration.
score :: Function f => Config > Depth > Overlap a f > Int Source #
Compute a score for a critical pair.
Higherlevel handling of critical pairs.
data CriticalPair f Source #
A critical pair together with information about how it was derived
Instances
(Labelled f, PrettyTerm f) => Pretty (CriticalPair f) Source #  
Defined in Twee.CP pPrintPrec :: PrettyLevel > Rational > CriticalPair f > Doc # pPrint :: CriticalPair f > Doc # pPrintList :: PrettyLevel > [CriticalPair f] > Doc #  
Symbolic (CriticalPair f) Source #  
Defined in Twee.CP type ConstantOf (CriticalPair f) Source # termsDL :: CriticalPair f > DList (TermListOf (CriticalPair f)) Source # subst_ :: (Var > BuilderOf (CriticalPair f)) > CriticalPair f > CriticalPair f Source #  
type ConstantOf (CriticalPair f) Source #  
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.