| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.ECTA.Internal.ECTA.Type
Synopsis
- data RecNodeId
- data Edge where
- InternedEdge {
- edgeId :: !Id
- uninternedEdge :: !UninternedEdge
- pattern Edge :: Symbol -> [Node] -> Edge
- InternedEdge {
- data UninternedEdge = UninternedEdge {
- uEdgeSymbol :: !Symbol
- uEdgeChildren :: ![Node]
- uEdgeEcs :: !EqConstraints
- mkEdge :: Symbol -> [Node] -> EqConstraints -> Edge
- emptyEdge :: Edge
- edgeChildren :: Edge -> [Node]
- edgeEcs :: Edge -> EqConstraints
- edgeSymbol :: Edge -> Symbol
- setChildren :: Edge -> [Node] -> Edge
- data Node where
- InternedNode !InternedNode
- EmptyNode
- InternedMu !InternedMu
- Rec !RecNodeId
- pattern Node :: [Edge] -> Node
- pattern Mu :: (Node -> Node) -> Node
- data InternedNode = MkInternedNode {
- internedNodeId :: !Id
- internedNodeEdges :: ![Edge]
- internedNodeNumNestedMu :: !Int
- internedNodeFree :: !(Set RecNodeId)
- data InternedMu = MkInternedMu {
- internedMuId :: !Id
- internedMuBody :: !Node
- internedMuShape :: !Node
- data UninternedNode
- = UninternedNode ![Edge]
- | UninternedEmptyNode
- | UninternedMu !(RecNodeId -> Node)
- data IntersectId
- pattern IntersectId :: Id -> Id -> IntersectId
- nodeIdentity :: Node -> Id
- numNestedMu :: Node -> Int
- substFree :: RecNodeId -> Node -> Node -> Node
- freeVars :: Node -> Set RecNodeId
- modifyNode :: Node -> ([Edge] -> [Edge]) -> Node
- createMu :: (Node -> Node) -> Node
Documentation
Constructors
| RecInt !Id | |
| RecUnint Int | Reference to an as-yet uninterned The NOTE: This is intentionally not an |
| RecDepth | Placeholder variable that we use only for depth calculations The invariant that this is used only for depth calculations, along with the observation that depth calculation
does not depend on the exact choice of variable, justifies subtituting any other variable for |
| RecIntersect IntersectId | Refer to Mu-node-to-be-constructed during intersection TODO: It is obviously not very elegant to have a constructor here specifically for one algorithm. Ideally, we
would parameterize |
Instances
| Eq RecNodeId Source # | |
| Ord RecNodeId Source # | |
| Show RecNodeId Source # | |
| Generic RecNodeId Source # | |
| Hashable RecNodeId Source # | |
Defined in Data.ECTA.Internal.ECTA.Type | |
| type Rep RecNodeId Source # | |
Defined in Data.ECTA.Internal.ECTA.Type type Rep RecNodeId = D1 ('MetaData "RecNodeId" "Data.ECTA.Internal.ECTA.Type" "ecta-1.0.0.3-GsgcdoZGkFZA4oJqDsbHRS" 'False) ((C1 ('MetaCons "RecInt" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Id)) :+: C1 ('MetaCons "RecUnint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))) :+: (C1 ('MetaCons "RecDepth" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RecIntersect" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IntersectId)))) | |
Constructors
| InternedEdge | |
Fields
| |
Instances
data UninternedEdge Source #
Constructors
| UninternedEdge | |
Fields
| |
Instances
edgeChildren :: Edge -> [Node] Source #
edgeEcs :: Edge -> EqConstraints Source #
edgeSymbol :: Edge -> Symbol Source #
Constructors
| InternedNode !InternedNode | |
| EmptyNode | |
| InternedMu !InternedMu | |
| Rec !RecNodeId |
Bundled Patterns
| pattern Node :: [Edge] -> Node | |
| pattern Mu :: (Node -> Node) -> Node | Pattern only a Mu constructor When we go underneath a Mu constructor, we need to bind the corresponding Rec node to something: that's why pattern
matching on An identity function foo (Mu f) = Mu f will run in O(1) time: foo (Mu f) = Mu f
-- { expand view patern }
foo node | Just f <- matchMu node = createMu f
-- { case for @InternedMu mu@ }
foo (InternedMu mu) | Just f <- matchMu (InternedMu m) = createMu f
-- { definition of matchMu }
foo (InternedMu mu) = let f = \n' ->
if | n' == Rec (RecUnint (numNestedMu (internedMuBody mu))) ->
internedMuShape mu
| n' == Rec RecDepth ->
internedMuShape mu
| otherwise ->
substFree (internedMuId mu) n' (internedMuBody mu)
in createMu f
-- { definition of createMu }
foo (InternedMu mu) = intern $ UninternedMu (f . Rec)At this point, |
Instances
data InternedNode Source #
Constructors
| MkInternedNode | |
Fields
| |
Instances
| Show InternedNode Source # | |
Defined in Data.ECTA.Internal.ECTA.Type Methods showsPrec :: Int -> InternedNode -> ShowS # show :: InternedNode -> String # showList :: [InternedNode] -> ShowS # | |
data InternedMu Source #
Constructors
| MkInternedMu | |
Fields
| |
Instances
| Show InternedMu Source # | |
Defined in Data.ECTA.Internal.ECTA.Type Methods showsPrec :: Int -> InternedMu -> ShowS # show :: InternedMu -> String # showList :: [InternedMu] -> ShowS # | |
data UninternedNode Source #
Constructors
| UninternedNode ![Edge] | |
| UninternedEmptyNode | |
| UninternedMu !(RecNodeId -> Node) | Recursive node The function should be parametric in the Id: substFree i (Rec j) (f i) == f j See |
Instances
| Eq UninternedNode Source # | |
Defined in Data.ECTA.Internal.ECTA.Type Methods (==) :: UninternedNode -> UninternedNode -> Bool # (/=) :: UninternedNode -> UninternedNode -> Bool # | |
| Hashable UninternedNode Source # | |
Defined in Data.ECTA.Internal.ECTA.Type | |
data IntersectId Source #
Context-free references to a Mu node introduced by intersect
Background: This is a generalization of the idea to be able to refer to the "immediately enclosing binder", and then
only deal with graphs with the property that we never need to refer past that enclosing binder. This too would allow
us to refer to a Mu node without knowing its Id, at the cost of requiring a substitution when we discover that
Id to return this into a RecInt. The generalization is that all we need to some way to refer to that Mu node
concretely, without Id, but we can: intersection introduces Mu whenever it encounters a Mu on the left or the
right, /and will then not introduce another Mu for that same intersection problem (at least, not in the same
scope). This means that the Id of the left and right operand will indeed uniquely identify the Mu node to be
constructed by intersect.
Furthermore, since we cache the free variables in a term, we have a cheap check to see if we need the Mu node at
all. This means that if the input graphs satisfy the property that there are references past Mu nodes, the output
should too: we will not introduce redundant Mu nodes.
NOTE: Although intersect has three cases in which it introduces Mu nodes (Mu in both operands, Mu in the left,
or Mu in the right), we don't need that distinction here: we just need to know the Id of the two operands, so
that if we see a call to intersect again with those same two operands (no matter what kind of nodes they are), we
can refer to the newly constructed Mu node.
Instances
pattern IntersectId :: Id -> Id -> IntersectId Source #
nodeIdentity :: Node -> Id Source #
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.
substFree :: RecNodeId -> Node -> Node -> Node Source #
Substitution
substFree i n will replace all occurrences of Rec (RecNodeId i) by n. We appeal to the uniqueness of node IDs
and assume that all occurrences of i must be free (in other words, that any occurrences of Mu will have a
different identifier.
Postcondition:
substFree i (Rec (RecNodeId i)) == id
freeVars :: Node -> Set RecNodeId Source #
Free variables in the term
O(1) in the size of the graph, provided that there are no unbounded Mu chains in the term.
O(log n)@ in the number of free variables in the graph, which we expect to be orders of magnitude smaller than the
size of the graph (indeed, we don't expect more than a handful).