Skip to content

Commit

Permalink
Add operation to create mapping in union find
Browse files Browse the repository at this point in the history
  • Loading branch information
alt-romes committed Jul 6, 2023
1 parent 8f645e5 commit dc6b280
Show file tree
Hide file tree
Showing 2 changed files with 35 additions and 3 deletions.
36 changes: 34 additions & 2 deletions src/Data/Equality/Graph.hs
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE MagicHash #-}
-- {-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE FlexibleContexts #-}
Expand All @@ -24,14 +25,19 @@ module Data.Equality.Graph
, find, canonicalize

-- * Functions on e-graphs
, emptyEGraph, newEClass
, emptyEGraph

-- ** Low-level operations
, newEClass, newPointerToClassId

-- * Re-exports
, module Data.Equality.Graph.Classes
, module Data.Equality.Graph.Nodes
, module Data.Equality.Language
) where

import GHC.Exts (Int(..), (+#), (<#), isTrue#)

-- ROMES:TODO: Is the E-Graph a Monad if the analysis data were the type arg? i.e. Monad (EGraph language)?

-- import GHC.Conc
Expand All @@ -52,6 +58,7 @@ import Data.Equality.Utils.SizedList

import Data.Equality.Graph.Internal
import Data.Equality.Graph.ReprUnionFind
import qualified Data.Equality.Utils.IntToIntMap as IIM
import Data.Equality.Graph.Classes
import Data.Equality.Graph.Nodes
import Data.Equality.Analysis
Expand Down Expand Up @@ -334,7 +341,32 @@ newEClass adata egr =
, classes = IM.insert new_eclass_id new_eclass (classes egr)
}
)
{-# INLINE newEClass #-}
{-# INLINEABLE newEClass #-}

-- | Create a mapping from some class-id that does not exist in the e-graph to
-- the given e-class id target. In practice, this basically creates an
-- alias from the a given class-id to the e-class id of the target
--
-- If, instead, you want to create a mapping from an existing class-id to another one, use 'merge'.
--
-- Under the hood, this operation will bump the union find counter for next-ids
-- to the given id+1 and add an entry to the union find from given id to the
-- given target id.
--
-- This means that all e-class ids up to the new pointer id will be considered to be in use.
--
-- INVARIANT: The given e-class pointer does not exist in the e-graph
newPointerToClassId :: ClassId -- ^ Given Id (pointer) that will point to the target
-> ClassId -- ^ The target id
-> EGraph a l -> EGraph a l
newPointerToClassId (I# pointer) (I# target) egr =
egr { unionFind = case unionFind egr of
RUF im _size ->
if isTrue# (pointer <# _size)
then error $ "newPointerToClassId: given pointer id (" ++ show (I# pointer) ++ ") already exists in the e-graph"
else RUF (IIM.insert pointer target im) (pointer +# 1#)
}
{-# INLINEABLE newPointerToClassId #-}

-- | Represent an expression (in fix-point form) and merge it with the e-class with the given id
representAndMerge :: (Analysis a l, Language l) => ClassId -> Fix l -> EGraph a l -> EGraph a l
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Equality/Graph/ReprUnionFind.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ Union-find-like data structure that defines equivalence classes of e-class ids.
-}
module Data.Equality.Graph.ReprUnionFind
( ReprUnionFind
( ReprUnionFind(..)
, emptyUF
, makeNewSet
, unionSets
Expand Down

0 comments on commit dc6b280

Please sign in to comment.