Safe Haskell | None |
---|---|
Language | Haskell2010 |
Critical pair generation.
Synopsis
- newtype Max = Max {}
- 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 :: 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)]
- 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 :: forall f a. (Has a (Rule f), Has a Id, Has a Max, Function f) => a -> a -> Overlap f -> CriticalPair f
- overlapProof :: forall a f. (Has a (Rule 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 :: 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.
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
(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 :: 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.