Safe Haskell | Safe-Inferred |
---|---|
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.
Higher-level 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.