Data.Equality.Analysis.Monadic

Like Analysis but for Analysis that are only well-defined within an (effectful) context. Mostly used with the monadic operations representM, addM, mergeM, and rebuildM.

This effectful Analysis could almost be trivially defined in terms of the other, through a "contextful" domain and by means of the _classes Traversal.

However, that would require an instance of Eq for the monadic domain, which is usually unnattainable.

Therefore, we do need this class for monadic Analysis.

Documentation

class (Monad m, Eq domain) => AnalysisM (m :: Type -> Type) domain (l :: Type -> Type) where

An e-class analysis with domain domain defined for a language l, whose operations are only well-defined within some effectful context.

The domain is the type of the domain of the e-class analysis, that is, the type of the data stored in an e-class according to this e-class analysis

Minimal complete definition

makeA, joinA

Methods

makeA :: l domain -> m domain

When a new e-node is added into a new, singleton e-class, construct a new value of the domain to be associated with the new e-class, by accessing the associated data of the node's children

The argument is the e-node term populated with its children data

joinA :: domain -> domain -> m domain

When e-classes c1 c2 are being merged into c, join d_c1 and d_c2 into a new value d_c to be associated with the new e-class c

modifyA

Arguments

:: ClassId

Id of class c whose new data d_c triggered the modify call

-> EGraph domain l

E-graph where class c being modified exists

-> m (EGraph domain l)

E-graph resulting from the modification

Optionally modify the e-class c (based on d_c), typically by adding an e-node to c. Modify should be idempotent if no other changes occur to the e-class, i.e., modify(modify(c)) = modify(c)

Instances

Monad m => AnalysisM m () l

The simplest analysis that defines the domain to be () and does nothing otherwise

Defined in Data.Equality.Analysis.Monadic

Methods

makeA :: l () -> m ()

joinA :: () -> () -> m ()

modifyA :: ClassId -> EGraph () l -> m (EGraph () l)