Safe Haskell | None |
---|---|
Language | Haskell2010 |
Critical pair generation.
Synopsis
- data Positions f
- type PositionsOf a = Positions (ConstantOf a)
- positions :: Term f -> Positions f
- positionsChurch :: Positions f -> ChurchList Int
- data Overlap f = Overlap {
- overlap_depth :: !Depth
- overlap_top :: !(Term f)
- overlap_inner :: !(Term f)
- overlap_pos :: !Int
- overlap_eqn :: !(Equation f)
- type OverlapOf a = Overlap (ConstantOf a)
- newtype Depth = Depth Int
- overlaps :: (Function f, Has a (Rule f), Has a (Positions f), Has a Depth) => Depth -> Index f a -> [a] -> a -> [(a, a, Overlap f)]
- 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)
- asymmetricOverlaps :: (Function f, Has a (Rule f), Has a Depth) => Index f a -> Depth -> Positions f -> Rule f -> Rule f -> ChurchList (Overlap f)
- overlapAt :: Int -> Depth -> Rule f -> Rule f -> Maybe (Overlap f)
- simplifyOverlap :: (Function f, Has a (Rule f)) => Index f a -> Overlap f -> Maybe (Overlap 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 -> Overlap f -> Int
- data CriticalPair f = CriticalPair {}
- split :: Function f => CriticalPair f -> [CriticalPair f]
- makeCriticalPair :: (Has a (Rule f), Has a (Proof f), Has a Id, Function f) => a -> a -> Overlap f -> Maybe (CriticalPair f)
- overlapProof :: forall a f. (Has a (Rule f), Has a (Proof f), Has a Id) => a -> a -> Overlap f -> Derivation f
Documentation
The set of positions at which a term can have critical overlaps.
type PositionsOf a = Positions (ConstantOf a) Source #
positionsChurch :: Positions f -> ChurchList Int Source #
A critical overlap of one rule with another.
Overlap | |
|
type OverlapOf a = Overlap (ConstantOf a) Source #
Represents the depth of a critical pair.
overlaps :: (Function f, 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.
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.
Higher-level handling of critical pairs.
data CriticalPair f Source #
A critical pair together with information about how it was derived
Instances
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) :: Type 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.