| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.ECTA
Description
Equality-constrained deterministic finite tree automata
Specialized to DAGs, plus at most one globally unique recursive node
Synopsis
- data Edge where
- mkEdge :: Symbol -> [Node] -> EqConstraints -> Edge
- edgeChildren :: Edge -> [Node]
- edgeSymbol :: Edge -> Symbol
- data Node where
- nodeEdges :: Node -> [Edge]
- numNestedMu :: Node -> Int
- createMu :: (Node -> Node) -> Node
- pathsMatching :: (Node -> Bool) -> Node -> [Path]
- mapNodes :: (Node -> Node) -> Node -> Node
- refold :: Node -> Node
- unfoldBounded :: Int -> Node -> Node
- crush :: forall m. Monoid m => (Node -> m) -> Node -> m
- onNormalNodes :: Monoid m => (Node -> m) -> Node -> m
- nodeCount :: Node -> Int
- edgeCount :: Node -> Int
- maxIndegree :: Node -> Int
- union :: [Node] -> Node
- intersect :: Node -> Node -> Node
- withoutRedundantEdges :: Node -> Node
- reducePartially :: Node -> Node
- type EnumerateM = StateT EnumerationState []
- runEnumerateM :: EnumerateM a -> EnumerationState -> [(a, EnumerationState)]
- enumerateFully :: EnumerateM ()
- getAllTerms :: Node -> [Term]
- getAllTruncatedTerms :: Node -> [Term]
- naiveDenotation :: Node -> [Term]
- toDot :: Node -> Graph
Documentation
Instances
edgeChildren :: Edge -> [Node] Source #
edgeSymbol :: Edge -> Symbol Source #
Constructors
| EmptyNode |
Instances
numNestedMu :: Node -> Int Source #
Maximum number of nested Mus in the term
@O(1) provided that there are no unbounded Mu chains in the term.
Operations
pathsMatching :: (Node -> Bool) -> Node -> [Path] Source #
Warning: Linear in number of paths, exponential in size of graph. Only use for very small graphs.
mapNodes :: (Node -> Node) -> Node -> Node Source #
Precondition: For all i, f (Rec i) is either a Rec node meant to represent the enclosing Mu, or contains no Rec node not beneath another Mu.
maxIndegree :: Node -> Int Source #
withoutRedundantEdges :: Node -> Node Source #
reducePartially :: Node -> Node Source #
Enumeration
type EnumerateM = StateT EnumerationState [] Source #
runEnumerateM :: EnumerateM a -> EnumerationState -> [(a, EnumerationState)] Source #
enumerateFully :: EnumerateM () Source #
getAllTerms :: Node -> [Term] Source #
getAllTruncatedTerms :: Node -> [Term] Source #
naiveDenotation :: Node -> [Term] Source #
Inefficient enumeration
For ECTAs with Mu nodes may produce an infinite list or may loop indefinitely, depending on the ECTAs. For example, for
createMu $ \r -> Node [Edge "f" [r], Edge "a" []]
it will produce
[ Term "a" [] , Term "f" [Term "a" []] , Term "f" [Term "f" [Term "a" []]] , ... ]
This happens to work currently because non-recursive edges are interned before recursive edges.
TODO: It would be much nicer if this did fair enumeration. It would avoid the beforementioned dependency on interning order, and it would give better enumeration for examples such as
Node [Edge "h" [
createMu $ \r -> Node [Edge "f" [r], Edge "a" []]
, createMu $ \r -> Node [Edge "g" [r], Edge "b" []]
]]This will currently produce
[ Term "h" [Term "a" [], Term "b" []] , Term "h" [Term "a" [], Term "g" [Term "b" []]] , Term "h" [Term "a" [], Term "g" [Term "g" [Term "b" []]]] , .. ]
where it always unfolds the second argument to h, never the first.