Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
See EGraph
.
Synopsis
- newtype EClassId = EClassId {
- unEClassId :: Int
- newtype ENodeId = ENodeId {}
- type EAnalysis d f = f d -> d
- noAnalysis :: EAnalysis () f
- data EClassInfo d f = EClassInfo {
- eciData :: !d
- eciNodes :: !(Assoc ENodeId (f ()))
- eciParents :: !(IntLikeSet ENodeId)
- data EGraph d f
- type WorkItem = IntLikeSet EClassId
- type WorkList = Seq WorkItem
- type ClassReplacements = EquivFind EClassId
- data MergeResult a
- egClassSource :: EGraph d f -> Source EClassId
- egNodeSource :: EGraph d f -> Source ENodeId
- egEquivFind :: EGraph d f -> EquivFind EClassId
- egClassMap :: EGraph d f -> IntLikeMap EClassId (EClassInfo d f)
- egNodeAssoc :: EGraph d f -> Assoc ENodeId (f EClassId)
- egHashCons :: EGraph d f -> IntLikeMap ENodeId EClassId
- egClassSize :: EGraph d f -> Int
- egNodeSize :: EGraph d f -> Int
- egFindNode :: (Eq (f EClassId), Hashable (f EClassId)) => f EClassId -> EGraph d f -> Maybe EClassId
- egFindTerm :: (RecursiveWhole t f, Traversable f, Eq (f EClassId), Hashable (f EClassId)) => t -> EGraph d f -> Maybe EClassId
- egClassInfo :: EClassId -> EGraph d f -> Maybe (EClassInfo d f)
- egNew :: EGraph d f
- egClasses :: State (EGraph d f) (IntLikeSet EClassId)
- egCanonicalize :: Traversable f => f EClassId -> State (EGraph d f) (Either EClassId (f EClassId))
- egCanonicalizePartial :: Traversable f => f EClassId -> State (EGraph d f) (f EClassId)
- egAddTerm :: (RecursiveWhole t f, Traversable f, Eq (f EClassId), Hashable (f EClassId), Hashable (f ())) => EAnalysis d f -> t -> State (EGraph d f) (Changed, EClassId)
- egMerge :: (Semigroup d, Traversable f, Eq (f EClassId), Hashable (f EClassId), Eq (f ()), Hashable (f ())) => EClassId -> EClassId -> State (EGraph d f) (MergeResult EClassId)
- egMergeMany :: (Semigroup d, Traversable f, Eq (f EClassId), Hashable (f EClassId), Eq (f ()), Hashable (f ())) => WorkList -> State (EGraph d f) (MergeResult (ClassReplacements, IntLikeSet EClassId))
- egReanalyzeSubset :: (Eq d, Semigroup d, Functor f) => EAnalysis d f -> IntLikeSet EClassId -> State (EGraph d f) ()
- egReanalyze :: (Eq d, Semigroup d, Functor f) => EAnalysis d f -> State (EGraph d f) ()
Documentation
An opaque class id. Constructor exported for coercibility. Num instance for literals only.
Instances
Enum EClassId Source # | |
Num EClassId Source # | |
Show EClassId Source # | |
NFData EClassId Source # | |
Defined in Overeasy.EGraph | |
Eq EClassId Source # | |
Ord EClassId Source # | |
Defined in Overeasy.EGraph | |
Hashable EClassId Source # | |
Defined in Overeasy.EGraph |
An opaque node id Constructor exported for coercibility. Num instance for literals only.
Instances
Enum ENodeId Source # | |
Num ENodeId Source # | |
Show ENodeId Source # | |
NFData ENodeId Source # | |
Defined in Overeasy.EGraph | |
Eq ENodeId Source # | |
Ord ENodeId Source # | |
Hashable ENodeId Source # | |
Defined in Overeasy.EGraph |
type EAnalysis d f = f d -> d Source #
The definition of an EGraph
analysis.
d
must be a join semilattice.
This function must be monotonic.
noAnalysis :: EAnalysis () f Source #
A disabled analysis
data EClassInfo d f Source #
Info stored for every class: analysis data, class members (nodes), and parent nodes.
EClassInfo | |
|
Instances
An E-Graph implementation
Instances
type WorkItem = IntLikeSet EClassId Source #
A set of class ids to merge
type ClassReplacements = EquivFind EClassId Source #
An invertible multimap of new root class to the sets of old classes it subsumes Can be used to externally recanonicalize any structures that reference class ids after merges.
data MergeResult a Source #
Merging classes can result in a few outcomes:
MergeResultUnchanged | All classes already merged, no change |
MergeResultMissing !WorkItem | Some classes missing, returns first problematic worklist entry (note that not all classes in worklist item will be missing, only at least one from the set) |
MergeResultChanged !a | Some classes merged, returns root map or merged class id |
Instances
egClassMap :: EGraph d f -> IntLikeMap EClassId (EClassInfo d f) Source #
Map of class to info Invariant: Only contains root classes.
egNodeAssoc :: EGraph d f -> Assoc ENodeId (f EClassId) Source #
Assoc of node id to node structure Invariant: only contains canonical structures (with root classes).
egHashCons :: EGraph d f -> IntLikeMap ENodeId EClassId Source #
Map of node to class Invariant: only contains root classes.
egFindNode :: (Eq (f EClassId), Hashable (f EClassId)) => f EClassId -> EGraph d f -> Maybe EClassId Source #
Find the class of the given node, if it exists. Note that you may have to canonicalize first to find it!
egFindTerm :: (RecursiveWhole t f, Traversable f, Eq (f EClassId), Hashable (f EClassId)) => t -> EGraph d f -> Maybe EClassId Source #
Find the class of the given term, if it exists
egClassInfo :: EClassId -> EGraph d f -> Maybe (EClassInfo d f) Source #
Lookup info for the given EClass
egCanonicalize :: Traversable f => f EClassId -> State (EGraph d f) (Either EClassId (f EClassId)) Source #
Find the canonical form of a node. If any classes are missing, the first missing is returned.
egCanonicalizePartial :: Traversable f => f EClassId -> State (EGraph d f) (f EClassId) Source #
Find the canonical form of a node. If any classes are missing, simply skip them.
egAddTerm :: (RecursiveWhole t f, Traversable f, Eq (f EClassId), Hashable (f EClassId), Hashable (f ())) => EAnalysis d f -> t -> State (EGraph d f) (Changed, EClassId) Source #
Adds a term (recursively) to the graph. If already in the graph, returns ChangedNo
and existing class id. Otherwise
returns ChangedYes
and a new class id.
egMerge :: (Semigroup d, Traversable f, Eq (f EClassId), Hashable (f EClassId), Eq (f ()), Hashable (f ())) => EClassId -> EClassId -> State (EGraph d f) (MergeResult EClassId) Source #
Merges two classes:
Returns Nothing
if the classes are not found or if they're already equal.
Otherwise returns the class remapping.
Note that it's MUCH more efficient to accumulate a WorkList
and use egMergeMany
.
egMergeMany :: (Semigroup d, Traversable f, Eq (f EClassId), Hashable (f EClassId), Eq (f ()), Hashable (f ())) => WorkList -> State (EGraph d f) (MergeResult (ClassReplacements, IntLikeSet EClassId)) Source #
Merges many sets of classes.
Returns Nothing
if the classes are not found or if they're already equal.
Otherwise returns the class remapping (equiv map of root to set of leaf classes).
It is important to note that the leaf classes in the returned mapping have been
REMOVED from the egraph, so they cannot be used to lookup classes in the future.
Therefore, if you have any class ids stored externally, you'll want to (partially)
canonicalize with the returned mapping.
Also note that the analysis of a given class is going to be an UNDER-APPROXIMATION
of the true analysis value, because per-node analyses are not recomputed.
egReanalyzeSubset :: (Eq d, Semigroup d, Functor f) => EAnalysis d f -> IntLikeSet EClassId -> State (EGraph d f) () Source #
Reanalyze a subset of classes - touched roots from merging is sufficient to ensure complete reanalysis. (Note this is implemented in a simplistic way, just taking the fixed point of rounds of analysis. The number of rounds can be no more than the size of the given set.) It may be necessary to call this because merging may leave class analyses in an under-approximating state. This method gives you the true analysis by fixed point.