hegg 0.5.0.0 → 0.6.0.0

raw patch · 15 files changed

+270/−122 lines, 15 filesdep ~containersdep ~transformersPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: containers, transformers

API changes (from Hackage documentation)

Files

• CHANGELOG.md +8/−0
• README.md +7/−0
• hegg.cabal +5/−5
• src/Data/Equality/Matching.hs +71/−23
• src/Data/Equality/Matching/Database.hs +62/−22
• src/Data/Equality/Matching/Pattern.hs +2/−5
• src/Data/Equality/Saturation.hs +22/−18
• src/Data/Equality/Saturation/Rewrites.hs +1/−1
• src/Data/Equality/Saturation/Scheduler.hs +2/−1
• src/Data/Equality/Utils.hs +0/−10
• test/Invariants.hs +13/−18
• test/Lambda.hs +5/−6
• test/Sym.hs +13/−13
• test/T32.hs +57/−0
• test/Test.hs +2/−0

@@ -2,6 +2,14 @@  ## Unreleased +## 0.6.0.0 -- 2024-07-13++* Fix a soundness bug that would cause equality saturation to be broken when+  `VariablePattern` was used explicitly with low numbers such as 1,2,3...+  This bug could also be triggered in the unlikely case when the hash of the+  given IsString variable instance collided with the Var Ids internally+  associated to NonVariablePatterns. Fixes #20 and #32.+ ## 0.5.0.0 -- 2023-10-31  * Change `'modifyA'` to instead operate over e-graphs, instead of being

@@ -303,3 +303,10 @@ open hegg-test.svg open hegg-test.eventlog.html ```++## Coverage++```+cabal test hegg-test --enable-coverage --enable-library-coverage+```+

@@ -1,7 +1,7 @@ cabal-version:      2.4 name:               hegg-version:            0.5.0.0-Tested-With:        GHC ==9.6.2 || ==9.4.5 || ==9.2.7 || ==8.10.7+version:            0.6.0.0+Tested-With:        GHC ==9.10.1 || ==9.8.4 || ==9.6.7 synopsis:           Fast equality saturation in Haskell  description:        Fast equality saturation and equality graphs based on "egg:@@ -101,8 +101,8 @@     -- LANGUAGE extensions used by modules in this package.     -- base-4.13, because foldMap' is used.     build-depends:    base         >= 4.13 && < 5,-                      transformers >= 0.4 && < 0.7,-                      containers   >= 0.4 && < 0.7+                      transformers >= 0.4 && < 0.8,+                      containers   >= 0.4 && < 0.8     if flag(vizdot)         build-depends: graphviz >= 2999.20 && < 2999.21,                        text@@ -118,7 +118,7 @@     hs-source-dirs:   test     main-is:          Test.hs     other-modules:    Invariants, Sym, Lambda, SimpleSym,-                      T1, T2, T3+                      T1, T2, T3, T32      other-extensions: OverloadedStrings     build-depends:    base,

@@ -10,7 +10,11 @@     ( ematch     , eGraphToDatabase     , Match(..)++    -- * Compiling a Pattern to a Query     , compileToQuery+    , VarsState(varNames), findVarName+    , userPatVars      , module Data.Equality.Matching.Pattern     )@@ -31,6 +35,7 @@ import Data.Equality.Graph.Lens import Data.Equality.Matching.Database import Data.Equality.Matching.Pattern+import Data.Coerce (coerce)  -- | Matching a pattern on an e-graph returns the e-class in which the pattern -- was matched and an e-class substitution for every 'VariablePattern' in the pattern.@@ -41,7 +46,8 @@  -- TODO: Perhaps e-graph could carry database and rebuild it on rebuild --- | Match a pattern against a 'Database', which can be gotten from an 'EGraph' with 'eGraphToDatabase'+-- | Match a pattern 'Query', gotten from 'compileToQuery' on a 'Pattern',+-- against a 'Database', which is built from an 'EGraph' with 'eGraphToDatabase'. -- -- Returns a list of matches, one 'Match' for each set of valid substitutions -- for all variables and the equivalence class in which the pattern was matched.@@ -50,21 +56,20 @@ -- could be constructed only once and shared accross matching. ematch :: Language l        => Database l-       -> Pattern l+       -> (Query l, Var {- query root var -})        -> [Match]-ematch db patr =+ematch db (q, root) =     let-        (q, root) = compileToQuery patr-         -- | Convert each substitution into a match by getting the class-id         -- where we matched from the subst         --         -- If the substitution is empty there is no match         f :: Subst -> Maybe Match-        f s = if IM.null s then Nothing-                           else case IM.lookup root s of-                                  Nothing -> error "how is root not in map?"-                                  Just found -> pure (Match s found)+        f s = if nullSubst s+                then Nothing+                else case lookupSubst root s of+                  Nothing -> error "how is root not in map?"+                  Just found -> pure (Match s found)       in mapMaybe f (genericJoin db q) @@ -97,24 +102,28 @@ -- | Auxiliary result in 'compileToQuery' algorithm data AuxResult lang = {-# UNPACK #-} !Var :~ [Atom lang] + -- | Compiles a 'Pattern' to a 'Query' and returns the query root variable with -- it. -- The root variable's substitutions are the e-classes where the pattern -- matched-compileToQuery :: (Traversable lang) => Pattern lang -> (Query lang, Var)-compileToQuery (VariablePattern x) = (SelectAllQuery x, x)-compileToQuery pa@(NonVariablePattern _) =+compileToQuery :: (Traversable lang) => Pattern lang -> ((Query lang, Var), VarsState)+compileToQuery (VariablePattern n) = flip runState emptyVarsState $ do+  v <- getVarName n+  return (SelectAllQuery v, v)+compileToQuery pa = -  let root :~ atoms = evalState (aux pa) 0-   in (Query (nubInt $ root:vars pa) atoms, root)+  let (root :~ atoms, varsState) = runState (aux pa) emptyVarsState+   in ((Query (nubVars $ root:userPatVars varsState) atoms, root), varsState)      where -        aux :: (Traversable lang) => Pattern lang -> State Int (AuxResult lang)-        aux (VariablePattern x) = return (x :~ []) -- from definition in relational e-matching paper (needed for as base case for recursion)+        aux :: (Traversable lang) => Pattern lang -> State VarsState (AuxResult lang)+        aux (VariablePattern x) = do+          v <- getVarName x+          return (v :~ []) -- from definition in relational e-matching paper (needed for as base case for recursion)         aux (NonVariablePattern p) = do-            v <- get-            modify' (+1)+            v <- nextVar             (toList -> auxs) <- traverse aux p             let boundVars = map (\(b :~ _) -> b) auxs                 atoms     = join $ map (\(_ :~ a) -> a) auxs@@ -128,9 +137,48 @@                     -- taking from the bound vars array                     subPatsToVars :: Traversable lang => lang (Pattern lang) -> [Var] -> State Int (lang Var)                     subPatsToVars p' boundVars = traverse (const $ (boundVars !!) <$> (get >>= \i -> modify' (+1) >> return i)) p'--        -- | Return distinct variables in a pattern-        vars :: Foldable lang => Pattern lang -> [Var]-        vars (VariablePattern x) = [x]-        vars (NonVariablePattern p) = nubInt $ join $ map vars $ toList p {-# INLINABLE compileToQuery #-}++--------------------------------------------------------------------------------+-- ** Vars utils for compileToQuery+--------------------------------------------------------------------------------++-- | Map user-given Variable names to internal 'Var's plus a counter+data VarsState = VarsState+  { varNames  :: !(M.Map String Var)+  , nextVarId :: !Int+  }++-- | An empty 'VarsState'+emptyVarsState :: VarsState+emptyVarsState = VarsState mempty 0++-- | Compute the next internal 'Var' from the current 'VarNameMap'+nextVar :: State VarsState Var+nextVar = do+  n <- gets nextVarId+  modify' (\vs -> vs{nextVarId = nextVarId vs +1})+  return (MatchVar n)++-- | Add a name to the 'VarNameMap' and get the resulting 'Var'.+getVarName :: String -> State VarsState Var+getVarName s = do+  vm <- gets varNames+  case M.lookup s vm of+    Nothing -> do+      n <- nextVar+      modify' (\vs -> vs{varNames = M.insert s n (varNames vs)})+      return n+    Just v ->+      return v++findVarName :: VarsState -> String -> Var+findVarName vs s = (varNames vs) M.! s++-- | Return the variables given in a pattern by a user, from the 'VarsState'+userPatVars :: VarsState -> [Var]+userPatVars = M.elems . varNames++-- | Deduplicate list of pattern Vars+nubVars :: [Var] -> [Var]+nubVars = coerce . nubInt . coerce

@@ -21,10 +21,15 @@   , Database(..)   , Query(..)   , IntTrie(..)-  , Subst-  , Var+  , Var(..)   , Atom(..)   , ClassIdOrVar(..)++    -- * Subst+  , Subst+  , lookupSubst+  , nullSubst+  , sizeSubst   ) where  import Data.List (sortBy)@@ -32,10 +37,10 @@ import Data.Maybe (mapMaybe) import Control.Monad -#if MIN_VERSION_base(4,20,0)-import Data.Foldable as F (toList, length)+#if !MIN_VERSION_base(4,20,0)+import Data.Foldable (foldl') #endif-import Data.Foldable as F (toList, foldl', length)+import qualified Data.Foldable as F (toList, length) import qualified Data.Map.Strict    as M import qualified Data.IntMap.Strict as IM import qualified Data.IntSet as IS@@ -43,6 +48,7 @@ import Data.Equality.Graph.Classes.Id import Data.Equality.Graph.Nodes import Data.Equality.Language+import Data.Coerce  -- | A variable in a query is identified by an 'Int'. -- This is much more efficient than using e.g. a 'String'.@@ -50,11 +56,8 @@ -- As a consequence, patterns also use 'Int' to represent a variable, but we -- can still have an 'Data.String.IsString' instance for variable patterns by hashing the -- string into a unique number.-type Var = Int---- | Mapping from 'Var' to 'ClassId'. In a 'Subst' there is only one--- substitution for each variable-type Subst = IM.IntMap ClassId+newtype Var = MatchVar { unsafeMatchVar :: Int }+  deriving (Show, Eq, Ord)  -- | A value which is either a 'ClassId' or a 'Var' data ClassIdOrVar = CClassId {-# UNPACK #-} !ClassId@@ -70,7 +73,9 @@  -- | A conjunctive query to be run on the database data Query lang-    = Query ![Var] ![Atom lang]+    = Query -- Q(x1,...,xk) <- R1(x11,...x1n), ..., Rn(xn1,...,xnn)+        ![Var] {- query head -}+        ![Atom lang] {- query body -}     | SelectAllQuery {-# UNPACK #-} !Var  -- | The relational representation of an e-graph, as described in section 3.1@@ -117,19 +122,18 @@  -- We want to match against ANYTHING, so we return a valid substitution for -- all existing e-class: get all relations and make a substition for each class in that relation, then join all substitutions across all classes-genericJoin (DB m) (SelectAllQuery x) = concatMap (map (IM.singleton x) . IS.toList . tkeys) (M.elems m)+genericJoin (DB m) (SelectAllQuery x) = concatMap (map (singleSubstVar x) . IS.toList . tkeys) (M.elems m)  -- This is the last variable, so we return a valid substitution for every -- possible value for the variable (hence, we prepend @x@ to each and make it -- its own substitution)--- ROMES:TODO: Start here. Map vars to indexs in an array and substitute in the resulting subst genericJoin d q@(Query _ atoms) = genericJoin' atoms (orderedVarsInQuery q)   where    genericJoin' :: [Atom l] -> [Var] -> [Subst]    genericJoin' atoms' = \case -     [] -> mempty <$> atoms'+     [] -> const emptySubst <$> atoms'       (!x):xs -> do @@ -138,7 +142,7 @@        -- Each valid sub-query assumes x -> x_in_D substitution        y <- genericJoin' (substitute x x_in_D atoms') xs -       return $! IM.insert x x_in_D y -- TODO: A bit contrieved, perhaps better to avoid map ?+       return $! insertSubstVar x x_in_D y     domainX :: Var -> [Atom l] -> [Int]    domainX x = IS.toList . intersectAtoms x d . filter (x `elemOfAtom`)@@ -170,11 +174,14 @@ -- described in the paper (such as batching) orderedVarsInQuery :: (Functor lang, Foldable lang) => Query lang -> [Var] orderedVarsInQuery (SelectAllQuery x) = [x]-orderedVarsInQuery (Query _ atoms) = IS.toList . IS.fromAscList $ sortBy (compare `on` varCost) $ mapMaybe toVar $ foldl' f mempty atoms+orderedVarsInQuery (Query _ atoms) = coerce . IS.toList . IS.fromAscList . coerce $+                                     sortBy (compare `on` varCost)                $+                                     mapMaybe toVar                               $+                                     foldl' f mempty atoms     where          f :: Foldable lang => [ClassIdOrVar] -> Atom lang -> [ClassIdOrVar]-        f s (Atom v (toList -> l)) = v:(l <> s)+        f s (Atom v (F.toList -> l)) = v:(l <> s)         {-# INLINE f #-}          -- First, prioritize variables that occur in many relations; second,@@ -214,7 +221,7 @@          -- If needed relation does exist, find intersection in it         -- Add list of found intersections to existing-        Just r  -> case intersectInTrie var mempty r (v:toList l) of+        Just r  -> case intersectInTrie var emptySubst r (v:F.toList l) of                      Nothing ->  error "intersectInTrie should return valid substitution for variable query"                      Just xs -> xs @@ -239,7 +246,7 @@ -- -- TODO: Really, a valid substitution is one which isn't empty... intersectInTrie :: Var -- ^ The variable whose domain we are looking for-                -> IM.IntMap ClassId -- ^ A mapping from variables that have been substituted+                -> Subst -- ^ A mapping from variables that have been substituted                 -> IntTrie  -- ^ The trie                 -> [ClassIdOrVar]  -- ^ The "query"                 -> Maybe IS.IntSet -- ^ The resulting domain for a valid substitution@@ -273,7 +280,7 @@     --      continue the recursion again to validate the assumption and     --      possibly find the domain of the variable we're looking for ahead     ---    CVar x:xs -> case IM.lookup x substs of+    CVar x:xs -> case lookupSubst x substs of         -- (2) or (4), we simply continue         Just varVal -> IM.lookup varVal m >>= \next -> intersectInTrie var substs next xs         -- (1) or (3)@@ -287,14 +294,14 @@             if all (isVarDifferentFrom x) xs               then trieKeys               else IM.foldrWithKey (\k ls (!acc) ->-               case intersectInTrie var (IM.insert x k substs) ls xs of+               case intersectInTrie var (insertSubstVar x k substs) ls xs of                    Nothing -> acc                    Just _  -> k `IS.insert` acc                          ) mempty m           -- (3)           -- else IS.unions $ IM.elems $ IM.mapMaybeWithKey (\k ls -> intersectInTrie var (IM.insert x k substs) ls xs) m           else IM.foldrWithKey (\k ls (!acc) ->-            case intersectInTrie var (IM.insert x k substs) ls xs of+            case intersectInTrie var (insertSubstVar x k substs) ls xs of                 Nothing -> acc                 Just rs -> rs <> acc) mempty m     where@@ -304,3 +311,36 @@       isVarDifferentFrom _ (CClassId _) = False       isVarDifferentFrom x (CVar     y) = x /= y       {-# INLINE isVarDifferentFrom #-}++--------------------------------------------------------------------------------+-- * Subst+--------------------------------------------------------------------------------++-- | Mapping from 'Var' to 'ClassId'. In a 'Subst' there is only one+-- substitution for each variable+newtype Subst = Subst (IM.IntMap ClassId)++-- | Insert a 'Var' in a 'Subst'+insertSubstVar :: Var -> ClassId -> Subst -> Subst+insertSubstVar (MatchVar k) v (Subst s) = Subst (IM.insert k v s)++-- | Make a singleton 'Var' in a 'Subst'+singleSubstVar :: Var -> ClassId -> Subst+singleSubstVar (MatchVar k) v = Subst (IM.singleton k v)++-- | Lookup a 'Var' in a 'Subst'+lookupSubst :: Var -> Subst -> Maybe ClassId+lookupSubst (MatchVar k) (Subst s) = IM.lookup k s++-- | An empty substitution+emptySubst :: Subst+emptySubst = Subst IM.empty++-- | Is the 'Subst' empty?+nullSubst :: Subst -> Bool+nullSubst (Subst s) = IM.null s++sizeSubst :: Subst -> Int+sizeSubst (Subst s) = IM.size s++

@@ -7,9 +7,6 @@  import Data.String -import Data.Equality.Utils-import Data.Equality.Matching.Database- -- | A pattern can be either a variable or an non-variable expression of -- patterns. --@@ -64,7 +61,7 @@ -- @ data Pattern lang     = NonVariablePattern (lang (Pattern lang))-    | VariablePattern Var -- ^ Should be a >0 positive number+    | VariablePattern String  -- | Synonym for 'NonVariablePattern'. --@@ -93,5 +90,5 @@     showsPrec d (NonVariablePattern x) = showsPrec d x  instance IsString (Pattern lang) where-    fromString = VariablePattern . hashString+    fromString = VariablePattern 

@@ -46,7 +46,6 @@  import qualified Data.IntMap.Strict as IM -import Data.Bifunctor import Control.Monad  import Data.Equality.Utils@@ -123,7 +122,9 @@       -- Read-only phase, invariants are preserved       -- With backoff scheduler       -- ROMES:TODO parMap with chunks-      let (!matches, newStats) = mconcat (fmap (\(rw_id,rw) -> first (map (rw,)) $ matchWithScheduler db i stats rw_id rw) (zip [1..] rewrites))+      let (!matches, newStats) = mconcat (fmap (\(rw_id,rw) ->+            let (ms, ss, vss) = matchWithScheduler db i stats rw_id rw+             in (map (\m -> (rw,m,vss)) ms, ss)) (zip [1..] rewrites))        -- Write-only phase, temporarily break invariants       forM_ matches applyMatchesRhs@@ -141,61 +142,64 @@                 && IM.size afterClasses == IM.size beforeClasses)           (runEqualitySaturation' (i+1) newStats) -  matchWithScheduler :: Database l -> Int -> IM.IntMap (Stat schd) -> Int -> Rewrite a l -> ([Match], IM.IntMap (Stat schd))+  matchWithScheduler :: Database l -> Int -> IM.IntMap (Stat schd) -> Int -> Rewrite a l+                     -> ([Match], IM.IntMap (Stat schd), VarsState {- the vars mapping resulting from compiling the query -})   matchWithScheduler db i stats rw_id = \case       rw  :| _ -> matchWithScheduler db i stats rw_id rw       lhs := _ -> do+          let (lhs_query, varsState) = compileToQuery lhs+           case IM.lookup rw_id stats of             -- If it's banned until some iteration, don't match this rule             -- against anything.-            Just s | isBanned @schd i s -> ([], stats)+            Just s | isBanned @schd i s -> ([], stats, varsState)              -- Otherwise, match and update stats             x -> do                  -- Match pattern-                let matches' = ematch db lhs -- Add rewrite to the e-match substitutions+                let matches' = ematch db lhs_query -- Add rewrite to the e-match substitutions                  -- Backoff scheduler: update stats                 let newStats = updateStats schd i rw_id x stats matches' -                (matches', newStats)+                (matches', newStats, varsState) -  applyMatchesRhs :: (Rewrite a l, Match) -> EGraphM a l ()+  applyMatchesRhs :: (Rewrite a l, Match, VarsState) -> EGraphM a l ()   applyMatchesRhs =       \case-          (rw :| cond, m@(Match subst _)) -> do+          (rw :| cond, m@(Match subst _), vss) -> do               -- If the rewrite condition is satisfied, applyMatchesRhs on the rewrite rule.               egr <- get-              when (cond subst egr) $-                 applyMatchesRhs (rw, m)+              when (cond vss subst egr) $+                 applyMatchesRhs (rw, m, vss) -          (_ := VariablePattern v, Match subst eclass) -> do+          (_ := VariablePattern v, Match subst eclass, vss) -> do               -- rhs is equal to a variable, simply merge class where lhs               -- pattern was found (@eclass@) and the eclass the pattern               -- variable matched (@lookup v subst@)-              case IM.lookup v subst of+              case lookupSubst (findVarName vss v) subst of                 Nothing -> error "impossible: couldn't find v in subst"                 Just n  -> do                     _ <- merge n eclass                     return () -          (_ := NonVariablePattern rhs, Match subst eclass) -> do+          (_ := NonVariablePattern rhs, Match subst eclass, vss) -> do               -- rhs is (at the top level) a non-variable pattern, so substitute               -- all pattern variables in the pattern and create a new e-node (and               -- e-class that represents it), then merge the e-class of the               -- substituted rhs with the class that matched the left hand side-              eclass' <- reprPat subst rhs+              eclass' <- reprPat vss subst rhs               _ <- merge eclass eclass'               return ()    -- | Represent a pattern in the e-graph a pattern given substitions-  reprPat :: Subst -> l (Pattern l) -> EGraphM a l ClassId-  reprPat subst = add . Node <=< traverse \case+  reprPat :: VarsState -> Subst -> l (Pattern l) -> EGraphM a l ClassId+  reprPat vss subst = add . Node <=< traverse \case       VariablePattern v ->-          case IM.lookup v subst of+          case lookupSubst (findVarName vss v) subst of               Nothing -> error "impossible: couldn't find v in subst?"               Just i  -> return i-      NonVariablePattern p -> reprPat subst p+      NonVariablePattern p -> reprPat vss subst p {-# INLINEABLE runEqualitySaturation #-} 

@@ -49,7 +49,7 @@ --      Just class_id -> --          egr^._class class_id._data /= Just 0 -- @-type RewriteCondition anl lang = Subst -> EGraph anl lang -> Bool+type RewriteCondition anl lang = VarsState -> Subst -> EGraph anl lang -> Bool   instance (∀ a. Show a => Show (lang a)) => Show (Rewrite anl lang) where

@@ -16,6 +16,7 @@  import qualified Data.IntMap.Strict as IM import Data.Equality.Matching+import Data.Equality.Matching.Database (sizeSubst)  -- | A 'Scheduler' determines whether a certain rewrite rule is banned from -- being used based on statistics it defines and collects on applied rewrite@@ -76,7 +77,7 @@         where            -- TODO: Overall difficult, and buggy at the moment.-          total_len = sum (map (length . matchSubst) matches)+          total_len = sum (map (sizeSubst . matchSubst) matches)            bannedN = case currentStat of                       Nothing -> 0;

@@ -9,7 +9,6 @@ #else import Data.Foldable #endif-import Data.Bits  -- import qualified Data.Set    as S -- import qualified Data.IntSet as IS@@ -35,15 +34,6 @@ cata :: Functor f => (f a -> a) -> (Fix f -> a) cata f = f . fmap (cata f) . unFix {-# INLINE cata #-}---- | Get the hash of a string.------ This util is currently used to generate an 'Int' used for the internal--- pattern variable representation from the external pattern variable--- representation ('String')-hashString :: String -> Int-hashString = foldl' (\h c -> 33*h `xor` fromEnum c) 5381-{-# INLINE hashString #-}  -- -- | We don't have the parallel package, so roll our own simple parMap -- parMap :: (a -> b) -> [a] -> [b]

@@ -16,7 +16,6 @@  import Control.Monad -import qualified Data.Containers.ListUtils as LU import qualified Data.Foldable as F import qualified Data.List   as L import qualified Data.IntSet as IS@@ -50,7 +49,7 @@         _   -> False     where         eg :: EGraph () l-        eg = snd $ equalitySaturation expr [VariablePattern 1:=fromInteger i] (error "Cost function shouldn't be used" :: CostFunction l Int)+        eg = snd $ equalitySaturation expr [VariablePattern "1":=fromInteger i] (error "Cost function shouldn't be used" :: CostFunction l Int)  -- | Test 'compileToQuery'. --@@ -60,14 +59,14 @@ -- The number of atoms should also match the number of non variable patterns -- since we should create an additional atom (with a new bound variable) for each.  testCompileToQuery :: Traversable lang => Pattern lang -> Bool-testCompileToQuery p = case fst $ compileToQuery p of-                         -- Handle special case for selectAll queries...-                         SelectAllQuery x -> [x] == vars p && numNonVarPatterns p == 0-                         q@(Query _ atoms)-                           | [] <- queryHeadVars q   -> False-                           | _:xs <- queryHeadVars q ->-                               L.sort xs == L.sort (vars p)-                                 && length atoms == numNonVarPatterns p+testCompileToQuery p = case compileToQuery p of+     -- Handle special case for selectAll queries...+     ((SelectAllQuery x, _), vss) -> [x] == userPatVars vss && numNonVarPatterns p == 0+     ((q@(Query _ atoms), _), vss)+       | _:xs <- queryHeadVars q ->+           L.sort xs == L.sort (userPatVars vss)+             && length atoms == numNonVarPatterns p+       | otherwise -> False     where         numNonVarPatterns :: Foldable lang => Pattern lang -> Int         numNonVarPatterns (VariablePattern _) = 0@@ -77,18 +76,14 @@         queryHeadVars (SelectAllQuery x) = [x]         queryHeadVars (Query qv _) = qv -        -- | Return distinct variables in a pattern-        vars :: Foldable lang => Pattern lang -> [Var]-        vars (VariablePattern x) = [x]-        vars (NonVariablePattern p') = LU.nubInt $ join $ map vars $ F.toList p'- -- | If we match a singleton variable pattern against an e-graph, we should get -- a match on all e-classes in the e-graph-ematchSingletonVar :: Language lang => Var -> EGraph () lang -> Bool+ematchSingletonVar :: Language lang => String -> EGraph () lang -> Bool ematchSingletonVar v eg =     let         db = eGraphToDatabase eg-        matches = IS.fromList $ map matchClassId $ ematch db (VariablePattern v)+        (q, _) = compileToQuery (VariablePattern v)+        matches = IS.fromList $ map matchClassId $ ematch db q         eclasses = IM.keysSet (classes eg)     in         matches == eclasses @@ -181,7 +176,7 @@ instance Arbitrary (Pattern SimpleExpr) where     arbitrary = sized p'       where-        p' 0 = VariablePattern <$> oneof (return <$> [1..16])+        p' 0 = VariablePattern <$> arbitrary         p' n = NonVariablePattern <$> resize (n `div` 2) arbitrary  newtype Name = Name { un :: String }

@@ -14,7 +14,6 @@  import Data.Maybe -import qualified Data.IntMap as IM import qualified Data.Set as S  import Control.Applicative ((<|>))@@ -111,17 +110,17 @@     abs = error "todo..."     signum = error "todo..." -unsafeGetSubst :: Pattern Lambda -> D.Subst -> ClassId-unsafeGetSubst (NonVariablePattern _) _ = error "unsafeGetSubst: NonVariablePattern; expecting VariablePattern"-unsafeGetSubst (VariablePattern v) subst = case IM.lookup v subst of+unsafeGetSubst :: Pattern Lambda -> VarsState -> D.Subst -> ClassId+unsafeGetSubst (NonVariablePattern _) _ _ = error "unsafeGetSubst: NonVariablePattern; expecting VariablePattern"+unsafeGetSubst (VariablePattern v) vss subst = case lookupSubst (findVarName vss v) subst of       Nothing -> error "Searching for non existent bound var in conditional"       Just class_id -> class_id  isConst :: Pattern Lambda -> RewriteCondition LA Lambda-isConst v subst egr = isJust $ snd $ egr^._class (unsafeGetSubst v subst)._data+isConst v vss subst egr = isJust $ snd $ egr^._class (unsafeGetSubst v vss subst)._data  isNotSameVar :: Pattern Lambda -> Pattern Lambda -> RewriteCondition LA Lambda-isNotSameVar v1 v2 subst egr = find (unsafeGetSubst v1 subst) egr /= find (unsafeGetSubst v2 subst) egr+isNotSameVar v1 v2 vss subst egr = find (unsafeGetSubst v1 vss subst) egr /= find (unsafeGetSubst v2 vss subst) egr  rules :: [Rewrite LA Lambda] rules =

@@ -14,7 +14,6 @@ import Test.Tasty import Test.Tasty.HUnit -import qualified Data.IntMap.Strict as IM import qualified Data.Set    as S import Data.String import Data.Maybe (isJust)@@ -148,28 +147,29 @@     Sym _ -> Nothing     Const x -> Just x     -unsafeGetSubst :: Pattern Expr -> Subst -> ClassId-unsafeGetSubst (NonVariablePattern _) _ = error "unsafeGetSubst: NonVariablePattern; expecting VariablePattern"-unsafeGetSubst (VariablePattern v) subst = case IM.lookup v subst of+unsafeGetSubst :: Pattern Expr -> VarsState -> Subst -> ClassId+unsafeGetSubst (NonVariablePattern _) _ _ = error "unsafeGetSubst: NonVariablePattern; expecting VariablePattern"+unsafeGetSubst (VariablePattern v) vss subst = case lookupSubst (findVarName vss v) subst of       Nothing -> error "Searching for non existent bound var in conditional"       Just class_id -> class_id +-- | TODO: This condition is incorrect. See #35 is_not_zero :: Pattern Expr -> RewriteCondition (Maybe Double) Expr-is_not_zero v subst egr =-    egr^._class (unsafeGetSubst v subst)._data /= Just 0+is_not_zero v vss subst egr =+    egr^._class (unsafeGetSubst v vss subst)._data /= Just 0  is_sym :: Pattern Expr -> RewriteCondition (Maybe Double) Expr-is_sym v subst egr =-    any ((\case (Sym _) -> True; _ -> False) . unNode) (egr^._class (unsafeGetSubst v subst)._nodes)+is_sym v vss subst egr =+    any ((\case (Sym _) -> True; _ -> False) . unNode) (egr^._class (unsafeGetSubst v vss subst)._nodes)  is_const :: Pattern Expr -> RewriteCondition (Maybe Double) Expr-is_const v subst egr =-    isJust (egr^._class (unsafeGetSubst v subst)._data)+is_const v vss subst egr =+    isJust (egr^._class (unsafeGetSubst v vss subst)._data)  is_const_or_distinct_var :: Pattern Expr -> Pattern Expr -> RewriteCondition (Maybe Double) Expr-is_const_or_distinct_var v w subst egr =-    let v' = unsafeGetSubst v subst-        w' = unsafeGetSubst w subst+is_const_or_distinct_var v w vss subst egr =+    let v' = unsafeGetSubst v vss subst+        w' = unsafeGetSubst w vss subst      in (eClassId (egr^._class v') /= eClassId (egr^._class w'))         && (isJust (egr^._class v'._data)             || any ((\case (Sym _) -> True; _ -> False) . unNode) (egr^._class v'._nodes))

@@ -0,0 +1,57 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE TypeApplications #-}+module T32 where++import Test.Tasty+import Test.Tasty.HUnit++import Data.Equality.Utils+import Data.Equality.Matching+import Data.Equality.Saturation+import Data.Equality.Graph+import qualified Data.Equality.Graph as EG+import Data.Equality.Saturation.Scheduler (defaultBackoffScheduler)+import Data.Equality.Graph.Monad++data SymExpr a = Symbol String+               | a :+: a+               deriving (Functor, Foldable, Traversable, Eq, Ord, Show)+infix 6 :+:++-- This test tests that using "VariablePattern 1, VariablePattern 2,+-- VariablePattern 3" in a rewrite rule succeeds, as opposed to using the+-- IsString instance for Pattern.+-- (Well, it tests that we can no longer screw up by writing the numbers+-- directly as well. Now the implementation transforms the strings into Ids+-- when compiling the pattern)+rewrites :: [Rewrite () SymExpr]+rewrites =+  [ pat (VariablePattern "1" :+: pat (VariablePattern "2" :+: VariablePattern "3")) := pat (pat (VariablePattern "1" :+: VariablePattern "2") :+: VariablePattern "3")+  ]++e1, e1' :: Fix SymExpr+e1 = Fix (Fix (Fix (Symbol "a") :+: Fix (Symbol "b")) :+: Fix (Symbol "c"))+e1' = Fix (Fix (Symbol "a") :+: Fix (Fix (Symbol "b") :+: Fix (Symbol "c")))++somePattern :: Pattern []+somePattern = NonVariablePattern [VariablePattern "0",VariablePattern "1"] ++-- Test basic associativity using pattern vars+testT32 :: TestTree+testT32 = testGroup "T32"+    [ testCase "basic associativity with VarPattern 1,2,3" $+        let+          (e1_id, eg0)  = EG.represent @() e1 emptyEGraph+          (e1'_id, eg1) = EG.represent @() e1' eg0+          ((), eg2)     = runEGraphM eg1 (runEqualitySaturation defaultBackoffScheduler rewrites)+          e1_canon      = EG.find e1_id eg2+          e1'_canon     = EG.find e1'_id eg2+         in e1_canon @?= e1'_canon+    -- , testCase "compiling pattern" $+    --     compileToQuery somePattern @?= Query ...+    ]

@@ -10,6 +10,7 @@ import Sym import Lambda import SimpleSym+import T32  import qualified T1 import qualified T2@@ -24,6 +25,7 @@   , testCase "T1" (T1.main `catch` (\(e :: SomeException) -> assertFailure (show e)))   , testCase "T2" (T2.main `catch` (\(e :: SomeException) -> assertFailure (show e)))   , testCase "T3" (T3.main `catch` (\(e :: SomeException) -> assertFailure (show e)))+  , testT32   ]  main :: IO ()