Copyright	(c) Fabricio Olivetti 2021 - 2024
License	BSD3
Maintainer	fabricio.olivetti@gmail.com
Stability	experimental
Portability
Safe Haskell	Safe-Inferred
Language	Haskell2010

Algorithm.EqSat.EqSatDB

Description

Pattern matching and rule application functions Heavily based on hegg (https:/github.comalt-romes/hegg by alt-romes)

Synopsis

type DB = Map (SRTree ()) IntTrie
data IntTrie = IntTrie {
- _keys :: Set EClassId
- _trie :: IntMap IntTrie
}
data Pattern
- = Fixed (SRTree Pattern)
- | VarPat Char
data Rule
- = Pattern :=> Pattern
- | Pattern :==: Pattern
- | Rule :| Condition
type Query = [Atom]
type Condition = Map ClassOrVar ClassOrVar -> EGraph -> Bool
type ClassOrVar = Either EClassId Int
data Atom = Atom ClassOrVar (SRTree ClassOrVar)
unFixPat :: Pattern -> SRTree Pattern
createDB :: EGraph -> DB
addToDB :: ENode -> EClassId -> State DB ()
trie :: EClassId -> IntMap IntTrie -> IntTrie
populate :: Maybe IntTrie -> [EClassId] -> Maybe IntTrie
canonizeMap :: (Map ClassOrVar ClassOrVar, ClassOrVar) -> EGraphST (Map ClassOrVar ClassOrVar, ClassOrVar)
applyMatch :: CostFun -> Rule -> (Map ClassOrVar ClassOrVar, ClassOrVar) -> EGraphST ()
applyMergeOnlyMatch :: CostFun -> Rule -> (Map ClassOrVar ClassOrVar, ClassOrVar) -> EGraphST ()
target :: Rule -> Pattern
source :: Rule -> Pattern
getConditions :: Rule -> [Condition]
classOfENode :: CostFun -> Map ClassOrVar ClassOrVar -> Pattern -> EGraphST (Maybe EClassId)
isConst :: EClassId -> EGraphST Bool
reprPrat :: CostFun -> Map ClassOrVar ClassOrVar -> Pattern -> EGraphST EClassId
isValidHeight :: (Map ClassOrVar ClassOrVar, ClassOrVar) -> EGraph -> Bool
isValidConditions :: Condition -> (Map ClassOrVar ClassOrVar, ClassOrVar) -> EGraph -> Bool
match :: DB -> Pattern -> [(Map ClassOrVar ClassOrVar, ClassOrVar)]
compileToQuery :: Pattern -> (Query, ClassOrVar)
getInt :: ClassOrVar -> Int
getElems :: SRTree a -> [a]
genericJoin :: DB -> Query -> [Map ClassOrVar ClassOrVar]
domainX :: DB -> ClassOrVar -> Query -> [ClassOrVar]
intersectAtoms :: ClassOrVar -> DB -> Query -> [EClassId]
intersectTries :: ClassOrVar -> Map ClassOrVar EClassId -> IntTrie -> [ClassOrVar] -> Maybe (Set EClassId)
updateVar :: ClassOrVar -> ClassOrVar -> Query -> Query
isDiffFrom :: Int -> ClassOrVar -> Bool
elemOfAtom :: ClassOrVar -> Atom -> Bool
orderedVars :: Query -> [ClassOrVar]

Documentation

type DB = Map (SRTree ()) IntTrie #

data IntTrie #

Constructors

IntTrie
Fields _keys :: Set EClassId _trie :: IntMap IntTrie

Instances

Instances details

Show IntTrie #
Instance details Defined in Algorithm.EqSat.EqSatDB Methods showsPrec :: Int -> IntTrie -> ShowS # show :: IntTrie -> String # showList :: [IntTrie] -> ShowS #

data Pattern #

Constructors

Fixed (SRTree Pattern)
VarPat Char

Instances

Instances details

IsString Pattern #
Instance details Defined in Algorithm.EqSat.EqSatDB Methods fromString :: String -> Pattern #
Floating Pattern #
Instance details Defined in Algorithm.EqSat.EqSatDB Methods pi :: Pattern # exp :: Pattern -> Pattern # log :: Pattern -> Pattern # sqrt :: Pattern -> Pattern # (**) :: Pattern -> Pattern -> Pattern # logBase :: Pattern -> Pattern -> Pattern # sin :: Pattern -> Pattern # cos :: Pattern -> Pattern # tan :: Pattern -> Pattern # asin :: Pattern -> Pattern # acos :: Pattern -> Pattern # atan :: Pattern -> Pattern # sinh :: Pattern -> Pattern # cosh :: Pattern -> Pattern # tanh :: Pattern -> Pattern # asinh :: Pattern -> Pattern # acosh :: Pattern -> Pattern # atanh :: Pattern -> Pattern # log1p :: Pattern -> Pattern # expm1 :: Pattern -> Pattern # log1pexp :: Pattern -> Pattern # log1mexp :: Pattern -> Pattern #
Num Pattern #
Instance details Defined in Algorithm.EqSat.EqSatDB Methods (+) :: Pattern -> Pattern -> Pattern # (-) :: Pattern -> Pattern -> Pattern # (*) :: Pattern -> Pattern -> Pattern # negate :: Pattern -> Pattern # abs :: Pattern -> Pattern # signum :: Pattern -> Pattern # fromInteger :: Integer -> Pattern #
Fractional Pattern #
Instance details Defined in Algorithm.EqSat.EqSatDB Methods (/) :: Pattern -> Pattern -> Pattern # recip :: Pattern -> Pattern # fromRational :: Rational -> Pattern #
Show Pattern #
Instance details Defined in Algorithm.EqSat.EqSatDB Methods showsPrec :: Int -> Pattern -> ShowS # show :: Pattern -> String # showList :: [Pattern] -> ShowS #

data Rule #

Constructors

Pattern :=> Pattern infix 3
Pattern :==: Pattern infix 3
Rule :\| Condition infixl 2

Instances

Instances details

Show Rule #
Instance details Defined in Algorithm.EqSat.EqSatDB Methods showsPrec :: Int -> Rule -> ShowS # show :: Rule -> String # showList :: [Rule] -> ShowS #

type Query = [Atom] #

type Condition = Map ClassOrVar ClassOrVar -> EGraph -> Bool #

type ClassOrVar = Either EClassId Int #

data Atom #

Constructors

Atom ClassOrVar (SRTree ClassOrVar)

Instances

Instances details

Show Atom #
Instance details Defined in Algorithm.EqSat.EqSatDB Methods showsPrec :: Int -> Atom -> ShowS # show :: Atom -> String # showList :: [Atom] -> ShowS #

unFixPat :: Pattern -> SRTree Pattern #

createDB :: EGraph -> DB #

createDB creates a database of patterns from an e-graph it simply calls addToDB for every pair (e-node, e-class id) from the e-graph.

addToDB :: ENode -> EClassId -> State DB () #

addToDB adds an e-node and e-class id to the database

trie :: EClassId -> IntMap IntTrie -> IntTrie #

Creates a singleton trie from an e-class id

populate :: Maybe IntTrie -> [EClassId] -> Maybe IntTrie #

Populates an IntTrie with a sequence of e-class ids

canonizeMap :: (Map ClassOrVar ClassOrVar, ClassOrVar) -> EGraphST (Map ClassOrVar ClassOrVar, ClassOrVar) #

applyMatch :: CostFun -> Rule -> (Map ClassOrVar ClassOrVar, ClassOrVar) -> EGraphST () #

applyMergeOnlyMatch :: CostFun -> Rule -> (Map ClassOrVar ClassOrVar, ClassOrVar) -> EGraphST () #

target :: Rule -> Pattern #

source :: Rule -> Pattern #

getConditions :: Rule -> [Condition] #

classOfENode :: CostFun -> Map ClassOrVar ClassOrVar -> Pattern -> EGraphST (Maybe EClassId) #

gets the e-node of the target of the rule TODO: add consts and modify

isConst :: EClassId -> EGraphST Bool #

reprPrat :: CostFun -> Map ClassOrVar ClassOrVar -> Pattern -> EGraphST EClassId #

adds the target of the rule into the e-graph

isValidHeight :: (Map ClassOrVar ClassOrVar, ClassOrVar) -> EGraph -> Bool #

isValidConditions :: Condition -> (Map ClassOrVar ClassOrVar, ClassOrVar) -> EGraph -> Bool #

returns True if the condition of a rule is valid for that match

match :: DB -> Pattern -> [(Map ClassOrVar ClassOrVar, ClassOrVar)] #

Returns the substitution rules for every match of the pattern source inside the e-graph.

compileToQuery :: Pattern -> (Query, ClassOrVar) #

Returns a Query (list of atoms) of a pattern

getInt :: ClassOrVar -> Int #

getElems :: SRTree a -> [a] #

returns the list of the children values

genericJoin :: DB -> Query -> [Map ClassOrVar ClassOrVar] #

Creates the substituion map for the pattern variables for each one of the matched subgraph

domainX :: DB -> ClassOrVar -> Query -> [ClassOrVar] #

returns the e-class id for a certain variable that matches the pattern described by the atoms

intersectAtoms :: ClassOrVar -> DB -> Query -> [EClassId] #

returns all e-class id that can matches this sequence of atoms

intersectTries :: ClassOrVar -> Map ClassOrVar EClassId -> IntTrie -> [ClassOrVar] -> Maybe (Set EClassId) #

searches for the intersection of e-class ids that matches each part of the query. Returns Nothing if the intersection is empty.

var is the current variable being investigated xs is the map of ids being investigated and their corresponding e-class id trie is the current trie of the pattern (i:ids) sequence of root : children of the atom to investigate

updateVar :: ClassOrVar -> ClassOrVar -> Query -> Query #

updates all occurrence of var with the new id x

isDiffFrom :: Int -> ClassOrVar -> Bool #

checks whether two ClassOrVar are different only check if it is a pattern variable, else returns true

elemOfAtom :: ClassOrVar -> Atom -> Bool #

checks if v is an element of an atom

orderedVars :: Query -> [ClassOrVar] #

sorts the variables in a query by the most frequently occurring