Safe Haskell | None |
---|---|
Language | Haskell2010 |
Representations of paths in an FTA, data structures for equality constraints over paths, algorithms for saturating these constraints
Synopsis
- data Path where
- unPath :: Path -> [Int]
- path :: [Int] -> Path
- class Pathable t t' | t -> t' where
- type Emptyable t'
- getPath :: Path -> t -> Emptyable t'
- getAllAtPath :: Path -> t -> [t']
- modifyAtPath :: (t' -> t') -> Path -> t -> t
- pathHeadUnsafe :: Path -> Int
- pathTailUnsafe :: Path -> Path
- isSubpath :: Path -> Path -> Bool
- isStrictSubpath :: Path -> Path -> Bool
- substSubpath :: Path -> Path -> Path -> Path
- smallestNonempty :: Vector PathTrie -> Int
- largestNonempty :: Vector PathTrie -> Int
- getMaxNonemptyIndex :: PathTrie -> Maybe Int
- data PathTrie
- isEmptyPathTrie :: PathTrie -> Bool
- isTerminalPathTrie :: PathTrie -> Bool
- toPathTrie :: [Path] -> PathTrie
- fromPathTrie :: PathTrie -> [Path]
- pathTrieDescend :: PathTrie -> Int -> PathTrie
- data PathEClass where
- PathEClass' {
- getPathTrie :: !PathTrie
- getOrigPaths :: [Path]
- pattern PathEClass :: [Path] -> PathEClass
- PathEClass' {
- unPathEClass :: PathEClass -> [Path]
- hasSubsumingMember :: PathEClass -> PathEClass -> Bool
- completedSubsumptionOrdering :: PathEClass -> PathEClass -> Ordering
- data EqConstraints where
- EqConstraints {
- getEclasses :: [PathEClass]
- EqContradiction
- pattern EmptyConstraints :: EqConstraints
- EqConstraints {
- rawMkEqConstraints :: [[Path]] -> EqConstraints
- unsafeGetEclasses :: EqConstraints -> [PathEClass]
- hasSubsumingMemberListBased :: [Path] -> [Path] -> Bool
- isContradicting :: [[Path]] -> Bool
- mkEqConstraints :: [[Path]] -> EqConstraints
- combineEqConstraints :: EqConstraints -> EqConstraints -> EqConstraints
- eqConstraintsDescend :: EqConstraints -> Int -> EqConstraints
- constraintsAreContradictory :: EqConstraints -> Bool
- constraintsImply :: EqConstraints -> EqConstraints -> Bool
- subsumptionOrderedEclasses :: EqConstraints -> Maybe [PathEClass]
- unsafeSubsumptionOrderedEclasses :: EqConstraints -> [PathEClass]
Documentation
class Pathable t t' | t -> t' where Source #
TODO: Should this be redone as a lens-library traversal? | TODO: I am unhappy about this Emptyable design; makes one question whether this should be a typeclass at all. (Terms/ECTAs differ in that there is always an ECTA Node that represents the value at a path)
getPath :: Path -> t -> Emptyable t' Source #
getAllAtPath :: Path -> t -> [t'] Source #
modifyAtPath :: (t' -> t') -> Path -> t -> t Source #
pathHeadUnsafe :: Path -> Int Source #
pathTailUnsafe :: Path -> Path Source #
substSubpath :: Path -> Path -> Path -> Path Source #
Read `substSubpath p1 p2 p3` as `[p1/p2]p3`
`substSubpath replacement toReplace target` takes toReplace
, a prefix of target,
and returns a new path in which toReplace
has been replaced by replacement
.
Undefined if toReplace is not a prefix of target
Instances
Eq PathTrie Source # | |
Ord PathTrie Source # | |
Defined in Data.ECTA.Internal.Paths | |
Show PathTrie Source # | |
Generic PathTrie Source # | |
Hashable PathTrie Source # | |
Defined in Data.ECTA.Internal.Paths | |
type Rep PathTrie Source # | |
Defined in Data.ECTA.Internal.Paths type Rep PathTrie = D1 ('MetaData "PathTrie" "Data.ECTA.Internal.Paths" "ecta-1.0.0.3-GsgcdoZGkFZA4oJqDsbHRS" 'False) ((C1 ('MetaCons "EmptyPathTrie" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TerminalPathTrie" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PathTrieSingleChild" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 PathTrie)) :+: C1 ('MetaCons "PathTrie" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Vector PathTrie))))) |
isEmptyPathTrie :: PathTrie -> Bool Source #
isTerminalPathTrie :: PathTrie -> Bool Source #
toPathTrie :: [Path] -> PathTrie Source #
Precondition: No path in the input is a subpath of another
fromPathTrie :: PathTrie -> [Path] Source #
data PathEClass Source #
PathEClass' | |
|
pattern PathEClass :: [Path] -> PathEClass | TODO: This pattern (and the caching of the original path list) is a temporary affair until we convert all clients of PathEclass to fully be based on tries |
Instances
unPathEClass :: PathEClass -> [Path] Source #
hasSubsumingMember :: PathEClass -> PathEClass -> Bool Source #
completedSubsumptionOrdering :: PathEClass -> PathEClass -> Ordering Source #
Extends the subsumption ordering to a total ordering by using the default lexicographic comparison for incomparable elements. | TODO: Optimization opportunity: Redundant work in the hasSubsumingMember calls
data EqConstraints Source #
EqConstraints | |
| |
EqContradiction |
pattern EmptyConstraints :: EqConstraints |
Instances
rawMkEqConstraints :: [[Path]] -> EqConstraints Source #
unsafeGetEclasses :: EqConstraints -> [PathEClass] Source #
isContradicting :: [[Path]] -> Bool Source #
The real contradiction condition is a cycle in the subsumption ordering. But, after congruence closure, this will reduce into a self-cycle in the subsumption ordering.
TODO; Prove this.
mkEqConstraints :: [[Path]] -> EqConstraints Source #
eqConstraintsDescend :: EqConstraints -> Int -> EqConstraints Source #
constraintsImply :: EqConstraints -> EqConstraints -> Bool Source #