hegg 0.2.0.0 → 0.3.0.0

raw patch · 24 files changed

+771/−265 lines, 24 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• CHANGELOG.md +31/−0
• README.md +90/−6
• hegg.cabal +5/−3
• src/Data/Equality/Analysis.hs +96/−18
• src/Data/Equality/Extraction.hs +7/−13
• src/Data/Equality/Graph.hs +72/−40
• src/Data/Equality/Graph/Classes.hs +5/−7
• src/Data/Equality/Graph/Classes.hs-boot +2/−2
• src/Data/Equality/Graph/Internal.hs +7/−8
• src/Data/Equality/Graph/Internal.hs-boot +3/−3
• src/Data/Equality/Graph/Lens.hs +7/−8
• src/Data/Equality/Graph/Monad.hs +8/−7
• src/Data/Equality/Language.hs +1/−3
• src/Data/Equality/Matching.hs +1/−2
• src/Data/Equality/Saturation.hs +25/−26
• src/Data/Equality/Saturation/Rewrites.hs +9/−3
• src/Data/Equality/Saturation/Scheduler.hs +21/−15
• test/Invariants.hs +7/−15
• test/Lambda.hs +123/−52
• test/SimpleSym.hs +25/−9
• test/Sym.hs +23/−25
• test/T1.hs +145/−0
• test/T2.hs +49/−0
• test/Test.hs +9/−0

@@ -1,5 +1,36 @@ # Revision history for hegg +## Unreleased++## 0.3.0.0 -- 2022-12-09++* A better `Analysis` tutorial in the README.++* Complete `Analysis` redesign.+    * The `Analysis` class now has two type parameters: a `domain` and a+        `language`, and no longer has an associated type family+    * The analysis no longer has any knowledge of the e-graph:+        * `makeA` now has type `l domain -> domain`, that is, to make a domain+            of a new node we only have to take into consideration the data of+            the sub-nodes of the new node.+        * `joinA` is unchanged.+        * `modifyA` now has type `EClass domain lang -> (EClass domain lang,+            [Fix lang])`. It takes an e-class and optionally modifies it,+            possibly by adding nodes to it. The return value is the modified+            e-class, and a list of expressions from the language to add to the+            e-class.+    * We can now compose analysis and create language-polymorphic analysis. Such+        two examples are the analysis with domain `()` which regardless of the+        language simply ignores the domain: `instance Analysis () l`; and the+        second example is the product of analysis, which composes two separate+        analysis into one: `instance (Analysis a l, Analysis b l) => Analysis+        (a,b) l`.+    * An `EGraph` now also has two type parameters instead of one (the latter is+      the language is the former the domain of the analysis).++* Allow customization of Schedulers through parameters (by accepting a scheduler+    rather than a proxy for it)+ ## 0.2.0.0 -- 2022-09-19  * Expose `runEqualitySaturation` to run equality saturation on existing e-graphs

@@ -96,14 +96,94 @@ can be read about e-class analysis in the [`Data.Equality.Analsysis`]() module and in the paper. -We could easily define constant folding (`2+2` being simplified to `4`) through-an `Analysis` instance, but for the sake of simplicity we'll simply define the-analysis data as `()` and always ignore it.+We can easily define constant folding (`2+2` being simplified to `4`) through+an `Analysis` instance. +An `Analysis` is defined over a `domain` and a `language`. To define constant+folding, we'll say the domain is `Maybe Double` to attach a value of that type to+each e-class, where `Nothing` indicates the e-class does not currently have a+constant value and `Just i` means the e-class has constant value `i`.+ ```hs-instance Analysis SymExpr where-  type Domain SymExpr = ()-  makeA _ _ = ()+instance Analysis (Maybe Double) SymExpr+  makeA = ...+  joinA = ...+  modifyA = ...+```++Let's now understand and implement the three methods of the analysis instance we want.++`makeA` is called when a new e-node is added to a new e-class, and constructs+for the new e-class a new value of the domain to be associated with it, always+by accessing the associated data of the node's children data.  Its type is `l+domain -> domain`, so note that the e-node's children associated data is+directly available in place of the actual children.++We want to associate constant data to the e-class, so we must find if the+e-node has a constant value or otherwise return `Nothing`:++```hs+makeA :: SymExpr (Maybe Double) -> Maybe Int+makeA = \case+  Const x -> Just x+  Symbol _ -> Nothing+  x :+: y -> (+) <$> x <*> y+  x :*: y -> (*) <$> x <*> y+  x :/: y -> (/) <$> x <*> y+```+ +`joinA` is called when e-classes c1 c2 are being merged into c. In this case, we+must join the e-class data from both classes to form the e-class data to be+associated with new e-class c. Its type is `domain -> domain -> domain`.  In our+case, to merge `Just _` with `Nothing` we simply take the `Just`, and if we+merge two e-classes with a constant value (that is, both are `Just`), then the+constant value is the same (or something went very wrong) and we just keep it.++```hs+joinA :: Maybe Double -> Maybe Double -> Maybe Double+joinA Nothing (Just x) = Just x+joinA (Just x) Nothing = Just x+joinA Nothing Nothing  = Nothing+joinA (Just x) (Just y) = if x == y then Just x else error "ouch, that shouldn't have happened"+```++Finally, `modifyA` describes how an e-class should (optionally) be modified+according to the e-class data and what new language expressions are to be added+to the e-class also w.r.t. the e-class data.+Its type is `EClass domain l -> (EClass domain l, [Fix l])`, where the argument+is the class to modify, the first element of the return tuple is the+(optionally) modified e-class and the second element is a list of the+expressions to represent and merge with this e-class.+For our example, if the e-class has a constant value associated to it, we want+to create a new e-class with that constant value and merge it to this e-class.++```hs+-- import Data.Equality.Graph.Lens ((^.), _data)+modifyA :: EClass (Maybe Double) SymExpr -> (EClass (Maybe Double) SymExpr, [Fix SymExpr])+modifyA c = case c^._data of+              Nothing -> (c, [])+              Just i  -> (c, [Fix (Const i)])+```++Modify is a bit trickier than the other methods, but it allows our e-graph to+change based on the e-class analysis data. Note that the method is optional and+there's a default implementation for it which doesn't change the e-class or adds+anything to it. Analysis data can be otherwise used, e.g., to inform rewrite+conditions.++By instancing this e-class analysis, all e-classes that have a constant value+associated to them will also have an e-node with a constant value. This is great+for our simple symbolic library because it means if we ever find e.g. an+expression equal to `3+1`, we'll also know it to be equal to `4`, which is a+better result than `3+1` (we've then successfully implemented constant folding).++If, otherwise, we didn't want to use an analysis, we could specify the analysis+domain as `()` which will make the analysis do nothing, because there's an+instance polymorphic over `lang` for `()` that looks like this:++```hs+instance Analysis () lang where+  makeA _ = ()   joinA _ _ = () ``` @@ -202,6 +282,10 @@ let expr = fst (equalitySaturation e1 rewrites cost) ``` And upon printing we'd see `expr = Symbol "x"`!++If we had instead `e2 = Fix (Fix (Fix (Symbol "x") :/: Fix (Symbol "x")) :+:+(Fix (Const 3))) -- (x/x)+3`, we'd get `expr = Const 4` because of our rewrite+rules put together with our constant folding!  This was a first introduction which skipped over some details but that tried to walk through fundamental concepts for using e-graphs and equality saturation

@@ -1,7 +1,7 @@ cabal-version:      2.4 name:               hegg-version:            0.2.0.0-Tested-With:        GHC ==9.4.1 || ==9.2.2 || ==9.0.2 || ==8.10.7+version:            0.3.0.0+Tested-With:        GHC ==9.4.2 || ==9.2.2 || ==9.0.2 || ==8.10.7 synopsis:           Fast equality saturation in Haskell  description:        Fast equality saturation and equality graphs based on "egg:@@ -107,7 +107,9 @@     type:             exitcode-stdio-1.0     hs-source-dirs:   test     main-is:          Test.hs-    other-modules:    Invariants, Sym, Lambda, SimpleSym+    other-modules:    Invariants, Sym, Lambda, SimpleSym,+                      T1, T2+     other-extensions: OverloadedStrings     build-depends:    base,                       hegg,

@@ -1,4 +1,8 @@ {-# LANGUAGE AllowAmbiguousTypes #-} -- joinA+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE MultiParamTypeClasses #-}@@ -23,41 +27,115 @@ module Data.Equality.Analysis where  import Data.Kind (Type)--import Data.Equality.Graph.Classes.Id-import Data.Equality.Graph.Nodes--import {-# SOURCE #-} Data.Equality.Graph.Internal (EGraph)+import Control.Arrow ((***)) --- | The e-class analysis defined for a language @l@.-class Eq (Domain l) => Analysis (l :: Type -> Type) where+import Data.Equality.Utils+import Data.Equality.Language+import Data.Equality.Graph.Classes -    -- | Domain of data stored in e-class according to e-class analysis-    type Domain l+-- | An e-class analysis with domain @domain@ defined for a language @l@.+--+-- 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+class Eq domain => Analysis domain (l :: Type -> Type) where      -- | 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, typically-    -- by accessing the associated data of n's children-    makeA :: ENode l -> EGraph l -> Domain l+    -- 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+    --+    -- === Example+    --+    -- @+    -- -- domain = Maybe Double+    -- makeA :: Expr (Maybe Double) -> Maybe Double+    -- makeA = \case+    --     BinOp Div e1 e2 -> liftA2 (/) e1 e2+    --     BinOp Sub e1 e2 -> liftA2 (-) e1 e2+    --     BinOp Mul e1 e2 -> liftA2 (*) e1 e2+    --     BinOp Add e1 e2 -> liftA2 (+) e1 e2+    --     Const x -> Just x+    --     Sym _ -> Nothing+    -- @+    makeA :: l domain -> 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-    joinA :: Domain l -> Domain l -> Domain l+    joinA :: domain -> domain -> domain -    -- | Optionaly modify the e-class c (based on d_c), typically by adding an+    -- | 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)     --+    -- The return value of the modify function is both the modified class and+    -- the expressions (in their fixed-point form) to add to this class. We+    -- can't manually add them because not only would it skip some of the+    -- internal steps of representing + merging, but also because it's+    -- impossible to add any expression with depth > 0 without access to the+    -- e-graph (since we must represent every sub-expression in the e-graph+    -- first).+    --+    -- That's why we must return the modified class and the expressions to add+    -- to this class.+    --     -- === Example     --     -- Pruning an e-class with a constant value of all its nodes except for the-    -- leaf values+    -- leaf values, and adding a constant value node     --     -- @     --  -- Prune all except leaf e-nodes-    --  modify (_class i._nodes %~ S.filter (null . children))+    --  modifyA cl =+    --    case cl^._data of+    --      Nothing -> (cl, [])+    --      Just d -> ((_nodes %~ S.filter (F.null .unNode)) cl, [Fix (Const d)])     -- @-    modifyA :: ClassId -> EGraph l -> EGraph l-    modifyA _ = id+    modifyA :: EClass domain l -> (EClass domain l, [Fix l])+    modifyA c = (c, [])     {-# INLINE modifyA #-}+++-- | The simplest analysis that defines the domain to be () and does nothing+-- otherwise+instance forall l. Analysis () l where+  makeA _ = ()+  joinA = (<>)+++-- This instance is not necessarily well behaved for any two analysis, so care+-- must be taken when using it.+--+-- A possible criterion is:+--+-- For any two analysis, where 'modifyA' is called @m1@ and @m2@ respectively,+-- this instance is well behaved if @m1@ and @m2@ commute.+--+-- That is, if @m1@ and @m2@ satisfy the following law:+-- @+-- m1 . m2 = m2 . m1+-- @+--+-- A simple criterion that should suffice for commutativity. If:+--  * The modify function only depends on the analysis value, and+--  * The modify function doesn't change the analysis value+-- Then any two such functions commute.+--+-- Note: there are weaker (or at least different) criteria for this instance to+-- be well behaved.+instance (Language l, Analysis a l, Analysis b l) => Analysis (a, b) l where++  makeA :: l (a, b) -> (a, b)+  makeA g = (makeA @a (fst <$> g), makeA @b (snd <$> g))++  joinA :: (a,b) -> (a,b) -> (a,b)+  joinA (x,y) = joinA @a @l x *** joinA @b @l y++  modifyA :: EClass (a, b) l -> (EClass (a, b) l, [Fix l])+  modifyA c =+    let (ca, la) = modifyA @a (c { eClassData = fst (eClassData c) })+        (cb, lb) = modifyA @b (c { eClassData = snd (eClassData c) })+     in ( EClass (eClassId c) (eClassNodes ca <> eClassNodes cb) (eClassData ca, eClassData cb) (eClassParents ca <> eClassParents cb)+        , la <> lb+        )

@@ -1,10 +1,4 @@-{-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE DeriveFunctor #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ViewPatterns #-} {-|    Given an e-graph representing expressions of our language, we might want to@@ -45,9 +39,9 @@ -- @ -- -- For a real example you might want to check out the source code of 'Data.Equality.Saturation.equalitySaturation''-extractBest :: forall lang cost+extractBest :: forall anl lang cost              . (Language lang, Ord cost)-            => EGraph lang            -- ^ The e-graph out of which we are extracting an expression+            => EGraph anl lang        -- ^ The e-graph out of which we are extracting an expression             -> CostFunction lang cost -- ^ The cost function to define /best/             -> ClassId                -- ^ The e-class from which we'll extract the expression             -> Fix lang               -- ^ The resulting /best/ expression, in its fixed point form.@@ -66,14 +60,14 @@   where      -- | Find the lowest cost of all e-classes in an e-graph in an extraction-    findCosts :: ClassIdMap (EClass lang) -> ClassIdMap (CostWithExpr lang cost) -> ClassIdMap (CostWithExpr lang cost)+    findCosts :: ClassIdMap (EClass anl lang) -> ClassIdMap (CostWithExpr lang cost) -> ClassIdMap (CostWithExpr lang cost)     findCosts eclasses current =        let (modified, updated) = IM.foldlWithKey f (False, current) eclasses            {-# INLINE f #-}-          f :: (Bool, ClassIdMap (CostWithExpr lang cost)) -> Int -> EClass lang -> (Bool, ClassIdMap (CostWithExpr lang cost))-          f = \acc@(_, beingUpdated) i' EClass{eClassNodes = nodes} ->+          f :: (Bool, ClassIdMap (CostWithExpr lang cost)) -> Int -> EClass anl lang -> (Bool, ClassIdMap (CostWithExpr lang cost))+          f acc@(_, beingUpdated) i' EClass{eClassNodes = nodes} =                 let                     currentCost = IM.lookup i' beingUpdated @@ -107,7 +101,7 @@     nodeTotalCost :: Traversable lang => ClassIdMap (CostWithExpr lang cost) -> ENode lang -> Maybe (CostWithExpr lang cost)     nodeTotalCost m (Node n) = do         expr <- traverse ((`IM.lookup` m) . flip find egr) n-        return $ CostWithExpr (cost ((fst . unCWE) <$> expr), (Fix $ (snd . unCWE) <$> expr))+        return $ CostWithExpr (cost (fst . unCWE <$> expr), Fix $ snd . unCWE <$> expr)     {-# INLINE nodeTotalCost #-} {-# INLINABLE extractBest #-} @@ -140,7 +134,7 @@ -- | Find the current best node and its cost in an equivalence class given only the class and the current extraction -- This is not necessarily the best node in the e-graph, only the best in the current extraction state findBest :: ClassId -> ClassIdMap (CostWithExpr lang a) -> Maybe (CostWithExpr lang a)-findBest i = IM.lookup i+findBest = IM.lookup {-# INLINE findBest #-}  newtype CostWithExpr lang a = CostWithExpr { unCWE :: (a, Fix lang) }

@@ -1,6 +1,5 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE BangPatterns #-}-{-# LANGUAGE TupleSections #-} -- {-# LANGUAGE ApplicativeDo #-} {-# LANGUAGE BlockArguments #-} {-# LANGUAGE FlexibleContexts #-}@@ -20,7 +19,7 @@     , emptyEGraph        -- ** Transformations-    , add, merge, rebuild+    , represent, add, merge, rebuild     -- , repair, repairAnal        -- ** Querying@@ -38,6 +37,10 @@ import Data.Bifunctor import Data.Containers.ListUtils +import Control.Monad+import Control.Monad.Trans.State+import Control.Exception (assert)+ import qualified Data.IntMap.Strict as IM import qualified Data.Set    as S @@ -51,18 +54,24 @@ import Data.Equality.Language import Data.Equality.Graph.Lens +import Data.Equality.Utils+ -- ROMES:TODO: join things built in paralell? -- instance Ord1 l => Semigroup (EGraph l) where --     (<>) eg1 eg2 = undefined -- not so easy -- instance Ord1 l => Monoid (EGraph l) where --     mempty = EGraph emptyUF mempty mempty mempty +-- | Represent an expression (in it's fixed point form) in an e-graph.+-- Returns the updated e-graph and the id from the e-class in which it was represented.+represent :: forall a l. (Analysis a l, Language l) => Fix l -> EGraph a l -> (ClassId, EGraph a l)+represent = cata (flip $ \e -> uncurry add . first Node . (`runState` e) . traverse (gets >=> \(x,e') -> x <$ put e'))  -- | Add an e-node to the e-graph -- -- If the e-node is already represented in this e-graph, the class-id of the -- class it's already represented in will be returned.-add :: forall l. Language l => ENode l -> EGraph l -> (ClassId, EGraph l)+add :: forall a l. (Analysis a l, Language l) => ENode l -> EGraph a l -> (ClassId, EGraph a l) add uncanon_e egr =     let !new_en = canonicalize uncanon_e egr @@ -76,7 +85,12 @@             (new_eclass_id, new_uf) = makeNewSet (unionFind egr)              -- New singleton e-class stores the e-node and its analysis data-            new_eclass       = EClass new_eclass_id (S.singleton new_en) (makeA new_en egr) mempty+            -- which is modified according to analysis+            --+            -- The modification also produces a list of expressions to+            -- represent and merge with this class, which we'll do before+            -- returning from this function+            (new_eclass, added_nodes) = modifyA $ EClass new_eclass_id (S.singleton new_en) (makeA @a ((\i -> egr^._class i._data @a) <$> unNode new_en)) mempty              -- TODO:Performance: All updates can be done to the map first? Parallelize?             --@@ -86,7 +100,7 @@             -- And add new e-class to existing e-classes             new_parents      = ((new_eclass_id, new_en) |:)             new_classes      = IM.insert new_eclass_id new_eclass $-                                    foldr  (IM.adjust ((_parents %~ new_parents)))+                                    foldr  (IM.adjust (_parents %~ new_parents))                                            (classes egr)                                            (unNode new_en) @@ -115,27 +129,30 @@             -- something else?             --             -- So in the end, we do need to addToWorklist to get correct results-            new_worklist     = (new_eclass_id, new_en):(worklist egr)+            new_worklist     = (new_eclass_id, new_en):worklist egr              -- Add the e-node's e-class id at the e-node's id             new_memo         = insertNM new_en new_eclass_id (memo egr) -         in ( new_eclass_id+            -- So we have our almost final e-graph. We just need to represent+            -- and merge in it all expressions which resulted from 'modifyA'+            -- above+            egr1             = egr { unionFind = new_uf+                                   , classes   = new_classes+                                   , worklist  = new_worklist+                                   , memo      = new_memo+                                   } -            , egr { unionFind = new_uf-                  , classes   = new_classes-                  , worklist  = new_worklist-                  , memo      = new_memo-                  }+            egr2             = foldr (representAndMerge new_eclass_id) egr1 added_nodes -                  -- Modify created node according to analysis-                  & modifyA new_eclass_id +         in ( new_eclass_id+            , egr2             ) {-# INLINABLE add #-}  -- | Merge 2 e-classes by id-merge :: forall l. Language l => ClassId -> ClassId -> EGraph l -> (ClassId, EGraph l)+merge :: forall a l. (Analysis a l, Language l) => ClassId -> ClassId -> EGraph a l -> (ClassId, EGraph a l) merge a b egr0 =    -- Use canonical ids@@ -159,22 +176,28 @@             -- Make leader the leader in the union find            (new_id, new_uf) = unionSets leader sub (unionFind egr0)+                                & first (\n -> assert (leader == n) n)             -- Update leader class with all e-nodes and parents from the            -- subsumed class-           updatedLeader = leader_class & _parents %~ (sub_class^._parents <>)-                                        & _nodes   %~ (sub_class^._nodes <>)-                                        & _data    .~ new_data-           new_data = joinA @l (leader_class^._data) (sub_class^._data)+           (updatedLeader, added_nodes) = leader_class+                                            & _parents %~ (sub_class^._parents <>)+                                            & _nodes   %~ (sub_class^._nodes <>)+                                            & _data    .~ new_data+                                            & modifyA +           new_data = joinA @a @l (leader_class^._data) (sub_class^._data)+            -- Update leader in classes so that it has all nodes and parents            -- from subsumed class, and delete the subsumed class-           new_classes = ((IM.insert leader updatedLeader) . (IM.delete sub)) (classes egr0)+           --+           -- Additionally modify the e-class according to the analysis+           new_classes = (IM.insert leader updatedLeader . IM.delete sub) (classes egr0)             -- Add all subsumed parents to worklist We can do this instead of            -- adding the new e-class itself to the worklist because it would end            -- up adding its parents anyway-           new_worklist = toListSL (sub_class^._parents) <> (worklist egr0)+           new_worklist = toListSL (sub_class^._parents) <> worklist egr0             -- If the new_data is different from the classes, the parents of the            -- class whose data is different from the merged must be put on the@@ -186,13 +209,13 @@              (if new_data /= (leader_class^._data)                 then toListSL (leader_class^._parents)                 else mempty) <>-             (analysisWorklist egr0)+             analysisWorklist egr0             -- ROMES:TODO: The code that makes the -1 * cos test pass when some other things are tweaked            -- new_memo = foldr (`insertNM` leader) (memo egr0) (sub_class^._nodes)             -- Build new e-graph-           new_egr = egr0+           egr1 = egr0              { unionFind = new_uf              , classes   = new_classes              -- , memo      = new_memo@@ -200,10 +223,9 @@              , analysisWorklist = new_analysis_worklist              } -             -- Modify according to analysis-             & modifyA new_id+           egr2 = foldr (representAndMerge leader) egr1 added_nodes -        in (new_id, new_egr)+        in (new_id, egr2) {-# INLINEABLE merge #-}              @@ -212,12 +234,12 @@ -- similar to other approaches in how it restores congruence; but it uniquely -- allows the client to choose when to restore invariants in the context of a -- larger algorithm like equality saturation.-rebuild :: Language l => EGraph l -> EGraph l+rebuild :: (Analysis a l, Language l) => EGraph a l -> EGraph a l rebuild (EGraph uf cls mm wl awl) =   -- empty worklists   -- repair deduplicated e-classes   let-    emptiedEgr = (EGraph uf cls mm mempty mempty)+    emptiedEgr = EGraph uf cls mm mempty mempty      wl'   = nubOrd $ bimap (`find` emptiedEgr) (`canonicalize` emptiedEgr) <$> wl     egr'  = foldr repair emptiedEgr wl'@@ -234,7 +256,7 @@ -- ROMES:TODO: find repair_id could be shared between repair and repairAnal?  -- | Repair a single worklist entry.-repair :: forall l. Language l => (ClassId, ENode l) -> EGraph l -> EGraph l+repair :: forall a l. (Analysis a l, Language l) => (ClassId, ENode l) -> EGraph a l -> EGraph a l repair (repair_id, node) egr =     -- TODO We're no longer deleting the uncanonicalized node, how much does it matter that the structure keeps growing?@@ -247,20 +269,25 @@ {-# INLINE repair #-}  -- | Repair a single analysis-worklist entry.-repairAnal :: forall l. Language l => (ClassId, ENode l) -> EGraph l -> EGraph l+repairAnal :: forall a l. (Analysis a l, Language l) => (ClassId, ENode l) -> EGraph a l -> EGraph a l repairAnal (repair_id, node) egr =     let-        c        = (egr^._classes) IM.! repair_id-        new_data = joinA @l (c^._data) (makeA node egr)+        c1                = (egr^._classes) IM.! repair_id+        new_data          = joinA @a @l (c1^._data) (makeA @a ((\i -> egr^._class i^._data @a) <$> unNode node))+        (c2, added_nodes) = modifyA (c1 & _data .~ new_data)     in     -- Take action if the new_data is different from the existing data-    if c^._data /= new_data+    if c1^._data /= new_data         -- Merge result is different from original class data, update class         -- with new_data-       then egr { analysisWorklist = toListSL (c^._parents) <> analysisWorklist egr-                }-                & _classes %~ (IM.adjust (_data .~ new_data) repair_id)-                & modifyA repair_id+       then+        let+            new_classes = IM.insert repair_id c2 (classes egr)+            egr1 = egr { analysisWorklist = toListSL (c1^._parents) <> analysisWorklist egr+                       , classes = new_classes+                       }+            egr2 = foldr (representAndMerge repair_id) egr1 added_nodes+         in egr2        else egr {-# INLINE repairAnal #-} @@ -272,17 +299,22 @@ -- that their e-class ids are represented by the same e-class canonical ids -- -- canonicalize(𝑓(𝑎,𝑏,𝑐,...)) = 𝑓((find 𝑎), (find 𝑏), (find 𝑐),...)-canonicalize :: Functor l => ENode l -> EGraph l -> ENode l+canonicalize :: Functor l => ENode l -> EGraph a l -> ENode l canonicalize (Node enode) eg = Node $ fmap (`find` eg) enode {-# INLINE canonicalize #-}  -- | Find the canonical representation of an e-class id in the e-graph -- Invariant: The e-class id always exists.-find :: ClassId -> EGraph l -> ClassId+find :: ClassId -> EGraph a l -> ClassId find cid = findRepr cid . unionFind {-# INLINE find #-}  -- | The empty e-graph. Nothing is represented in it yet.-emptyEGraph :: Language l => EGraph l+emptyEGraph :: Language l => EGraph a l emptyEGraph = EGraph emptyUF mempty mempty mempty mempty {-# INLINE emptyEGraph #-}++-- | 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+representAndMerge o f g = case represent f g of+                        (i, e) -> snd $ merge o i e

@@ -17,21 +17,19 @@  import Data.Equality.Utils.SizedList -import Data.Equality.Analysis- -- | An e-class (an equivalence class of terms) of a language @l@. -- -- Intuitively, an e-graph is a set of equivalence classes (e-classes). Each -- e-class is a set of e-nodes representing equivalent terms from a given -- language, and an e-node is a function symbol paired with a list of children -- e-classes.-data EClass l = EClass+data EClass analysis_domain language = EClass     { eClassId      :: {-# UNPACK #-} !ClassId -- ^ E-class identifier-    , eClassNodes   :: !(S.Set (ENode l))      -- ^ E-nodes in this class-    , eClassData    :: Domain l                -- ^ The analysis data associated with this eclass.-    , eClassParents :: !(SList (ClassId, ENode l))   -- ^ E-nodes which are parents of this e-class and their corresponding e-class ids.+    , eClassNodes   :: !(S.Set (ENode language))      -- ^ E-nodes in this class+    , eClassData    :: analysis_domain                       -- ^ The analysis data associated with this eclass.+    , eClassParents :: !(SList (ClassId, ENode language)) -- ^ E-nodes which are parents of this e-class and their corresponding e-class ids.     } -instance (Show (Domain l), Show1 l) => Show (EClass l) where+instance (Show a, Show1 l) => Show (EClass a l) where     show (EClass a b d (SList c _)) = "Id: " <> show a <> "\nNodes: " <> show b <> "\nParents: " <> show c <> "\nData: " <> show d 

@@ -4,5 +4,5 @@  import Data.Kind -type role EClass nominal-data EClass (l :: Type -> Type)+type role EClass representational nominal+data EClass a (l :: Type -> Type)

@@ -11,19 +11,18 @@ import Data.Equality.Graph.ReprUnionFind import Data.Equality.Graph.Classes import Data.Equality.Graph.Nodes-import Data.Equality.Analysis  -- | E-graph representing terms of language @l@. -- -- Intuitively, an e-graph is a set of equivalence classes (e-classes). Each e-class is a -- set of e-nodes representing equivalent terms from a given language, and an e-node is a function -- symbol paired with a list of children e-classes.-data EGraph l = EGraph-    { unionFind :: !ReprUnionFind           -- ^ Union find like structure to find canonical representation of an e-class id-    , classes   :: !(ClassIdMap (EClass l)) -- ^ Map canonical e-class ids to their e-classes-    , memo      :: !(Memo l)                -- ^ Hashcons maps all canonical e-nodes to their e-class ids-    , worklist  :: !(Worklist l)            -- ^ Worklist of e-class ids that need to be upward merged-    , analysisWorklist :: !(Worklist l)     -- ^ Like 'worklist' but for analysis repairing+data EGraph analysis language = EGraph+    { unionFind :: !ReprUnionFind              -- ^ Union find like structure to find canonical representation of an e-class id+    , classes   :: !(ClassIdMap (EClass analysis language)) -- ^ Map canonical e-class ids to their e-classes+    , memo      :: !(Memo language)            -- ^ Hashcons maps all canonical e-nodes to their e-class ids+    , worklist  :: !(Worklist language)        -- ^ Worklist of e-class ids that need to be upward merged+    , analysisWorklist :: !(Worklist language) -- ^ Like 'worklist' but for analysis repairing     }  -- | The hashcons 𝐻  is a map from e-nodes to e-class ids@@ -32,7 +31,7 @@ -- | Maintained worklist of e-class ids that need to be “upward merged” type Worklist l = [(ClassId, ENode l)] -instance (Show (Domain l), Show1 l) => Show (EGraph l) where+instance (Show a, Show1 l) => Show (EGraph a l) where     show (EGraph a b c d e) =         "UnionFind: " <> show a <>             "\n\nE-Classes: " <> show b <>

@@ -4,6 +4,6 @@  import Data.Kind -type EGraph :: (Type -> Type) -> Type-type role EGraph nominal-data EGraph l+type role EGraph representational nominal+type EGraph :: Type -> (Type -> Type) -> Type+data EGraph a l

@@ -20,7 +20,6 @@ import Data.Equality.Graph.Nodes import Data.Equality.Graph.Classes import Data.Equality.Graph.ReprUnionFind-import Data.Equality.Analysis  -- | A 'Lens'' as defined in other lenses libraries type Lens' s a = forall f. Functor f => (a -> f a) -> (s -> f s)@@ -39,7 +38,7 @@ -- | Lens for the e-class with the given id in an e-graph -- -- Calls 'error' when the e-class doesn't exist-_class :: ClassId -> Lens' (EGraph l) (EClass l)+_class :: ClassId -> Lens' (EGraph a l) (EClass a l) _class i afa s =     let canon_id = findRepr i (unionFind s)      in (\c' -> s { classes = IM.insert canon_id c' (classes s) }) <$> afa (classes s IM.! canon_id)@@ -47,27 +46,27 @@  -- | Lens for the memo of e-nodes in an e-graph, that is, a mapping from -- e-nodes to the e-class they're represented in-_memo :: Lens' (EGraph l) (NodeMap l ClassId)+_memo :: Lens' (EGraph a l) (NodeMap l ClassId) _memo afa egr = (\m1 -> egr {memo = m1}) <$> afa (memo egr) {-# INLINE _memo #-}  -- | Lens for the map of existing classes by id in an e-graph-_classes :: Lens' (EGraph l) (ClassIdMap (EClass l))+_classes :: Lens' (EGraph a l) (ClassIdMap (EClass a l)) _classes afa egr = (\m1 -> egr {classes = m1}) <$> afa (classes egr) {-# INLINE _classes #-}  -- | Lens for the 'Domain' of an e-class-_data :: Lens' (EClass l) (Domain l)+_data :: Lens' (EClass domain l) domain _data afa EClass{..} = (\d1 -> EClass eClassId eClassNodes d1 eClassParents) <$> afa eClassData {-# INLINE _data #-}  -- | Lens for the parent e-classes of an e-class-_parents :: Lens' (EClass l) (SList (ClassId, ENode l))-_parents afa EClass{..} = (\ps -> EClass eClassId eClassNodes eClassData ps) <$> afa eClassParents+_parents :: Lens' (EClass a l) (SList (ClassId, ENode l))+_parents afa EClass{..} = EClass eClassId eClassNodes eClassData <$> afa eClassParents {-# INLINE _parents #-}  -- | Lens for the e-nodes in an e-class-_nodes :: Lens' (EClass l) (S.Set (ENode l))+_nodes :: Lens' (EClass a l) (S.Set (ENode l)) _nodes afa EClass{..} = (\ns -> EClass eClassId ns eClassData eClassParents) <$> afa eClassNodes {-# INLINE _nodes #-} 

@@ -28,11 +28,12 @@  import Data.Equality.Utils (Fix, cata) +import Data.Equality.Analysis import Data.Equality.Graph (EGraph, ClassId, Language, ENode(..)) import qualified Data.Equality.Graph as EG  -- | E-graph stateful computation-type EGraphM s = State (EGraph s)+type EGraphM a l = State (EGraph a l)  -- | Run EGraph computation on an empty e-graph --@@ -43,18 +44,18 @@ --  id2 <- represent t2 --  merge id1 id2 -- @-egraph :: Language l => EGraphM l a -> (a, EGraph l)+egraph :: Language l => EGraphM anl l a -> (a, EGraph anl l) egraph = runEGraphM EG.emptyEGraph {-# INLINE egraph #-}  -- | Represent an expression (@Fix l@) in an e-graph by recursively -- representing sub expressions-represent :: Language l => Fix l -> EGraphM l ClassId+represent :: (Analysis anl l, Language l) => Fix l -> EGraphM anl l ClassId represent = cata $ sequence >=> add . Node {-# INLINE represent #-}  -- | Add an e-node to the e-graph-add :: Language l => ENode l -> EGraphM l ClassId+add :: (Analysis anl l, Language l) => ENode l -> EGraphM anl l ClassId add = StateT . fmap pure . EG.add {-# INLINE add #-} @@ -62,7 +63,7 @@ -- -- E-graph invariants may be broken by merging, and 'rebuild' should be used -- /eventually/ to restore them-merge :: Language l => ClassId -> ClassId -> EGraphM l ClassId+merge :: (Analysis anl l, Language l) => ClassId -> ClassId -> EGraphM anl l ClassId merge a b = StateT (pure <$> EG.merge a b) {-# INLINE merge #-} @@ -73,11 +74,11 @@ -- 'rebuild') -- -- The paper describing rebuilding in detail is https://arxiv.org/abs/2004.03082-rebuild :: Language l => EGraphM l ()+rebuild :: (Analysis anl l, Language l) => EGraphM anl l () rebuild = StateT (pure . ((),). EG.rebuild) {-# INLINE rebuild #-}  -- | Run 'EGraphM' computation on a given e-graph-runEGraphM :: EGraph l -> EGraphM l a -> (a, EGraph l)+runEGraphM :: EGraph anl l -> EGraphM anl l a -> (a, EGraph anl l) runEGraphM = flip runState {-# INLINE runEGraphM #-}

@@ -30,8 +30,6 @@  import Data.Functor.Classes -import Data.Equality.Analysis- -- | A 'Language' is the required constraint on /expressions/ that are to be -- represented in an e-graph. --@@ -40,5 +38,5 @@ -- e-graphs), note that it must satisfy the other class constraints. In -- particular an 'Data.Equality.Analysis.Analysis' must be defined for the -- language.-class (Analysis l, Traversable l, Ord1 l) => Language l where+class (Traversable l, Ord1 l) => Language l where 

@@ -1,4 +1,3 @@-{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE ScopedTypeVariables #-} {-|@@ -69,7 +68,7 @@      in mapMaybe f (genericJoin db q)  -- | Convert an e-graph into a database-eGraphToDatabase :: Language l => EGraph l -> Database l+eGraphToDatabase :: Language l => EGraph a l -> Database l eGraphToDatabase egr = foldrWithKeyNM' addENodeToDB (DB mempty) (egr^._memo)   where 

@@ -48,14 +48,13 @@ import Data.Bifunctor import Control.Monad -import Data.Proxy- import Data.Equality.Utils import Data.Equality.Graph.Nodes import Data.Equality.Graph.Lens import qualified Data.Equality.Graph as G import Data.Equality.Graph.Monad import Data.Equality.Language+import Data.Equality.Analysis import Data.Equality.Graph.Classes import Data.Equality.Matching import Data.Equality.Matching.Database@@ -65,33 +64,33 @@ import Data.Equality.Saturation.Scheduler  -- | Equality saturation with defaults-equalitySaturation :: forall l cost-                    . (Language l, Ord cost)+equalitySaturation :: forall a l cost+                    . (Analysis a l, Language l, Ord cost)                    => Fix l               -- ^ Expression to run equality saturation on-                   -> [Rewrite l]         -- ^ List of rewrite rules+                   -> [Rewrite a l]         -- ^ List of rewrite rules                    -> CostFunction l cost -- ^ Cost function to extract the best equivalent representation-                   -> (Fix l, EGraph l)   -- ^ Best equivalent expression and resulting e-graph-equalitySaturation = equalitySaturation' (Proxy @BackoffScheduler)+                   -> (Fix l, EGraph a l)   -- ^ Best equivalent expression and resulting e-graph+equalitySaturation = equalitySaturation' defaultBackoffScheduler   -- | Run equality saturation on an expression given a list of rewrites, and -- extract the best equivalent expression according to the given cost function -- -- This variant takes all arguments instead of using defaults-equalitySaturation' :: forall l schd cost-                    . (Language l, Scheduler schd, Ord cost)-                    => Proxy schd          -- ^ Proxy for the scheduler to use+equalitySaturation' :: forall a l schd cost+                    . (Analysis a l, Language l, Scheduler schd, Ord cost)+                    => schd                -- ^ Scheduler to use                     -> Fix l               -- ^ Expression to run equality saturation on-                    -> [Rewrite l]         -- ^ List of rewrite rules+                    -> [Rewrite a l]       -- ^ List of rewrite rules                     -> CostFunction l cost -- ^ Cost function to extract the best equivalent representation-                    -> (Fix l, EGraph l)   -- ^ Best equivalent expression and resulting e-graph-equalitySaturation' proxy expr rewrites cost = egraph $ do+                    -> (Fix l, EGraph a l)   -- ^ Best equivalent expression and resulting e-graph+equalitySaturation' schd expr rewrites cost = egraph $ do      -- Represent expression as an e-graph     origClass <- represent expr      -- Run equality saturation (by applying non-destructively all rewrites)-    runEqualitySaturation proxy rewrites+    runEqualitySaturation schd rewrites      -- Extract best solution from the e-class of the original expression     gets $ \g -> extractBest g cost origClass@@ -100,17 +99,17 @@  -- | Run equality saturation on an e-graph by non-destructively applying all -- given rewrite rules until saturation (using the given 'Scheduler')-runEqualitySaturation :: forall l schd-                       . (Language l, Scheduler schd)-                      => Proxy schd          -- ^ Proxy for the scheduler to use-                      -> [Rewrite l]         -- ^ List of rewrite rules-                      -> EGraphM l ()-runEqualitySaturation _ rewrites = runEqualitySaturation' 0 mempty where -- Start at iteration 0+runEqualitySaturation :: forall a l schd+                       . (Analysis a l, Language l, Scheduler schd)+                      => schd                -- ^ Scheduler to use+                      -> [Rewrite a l]       -- ^ List of rewrite rules+                      -> EGraphM a l ()+runEqualitySaturation schd rewrites = runEqualitySaturation' 0 mempty where -- Start at iteration 0    -- Take map each rewrite rule to stats on its usage so we can do   -- backoff scheduling. Each rewrite rule is assigned an integer   -- (corresponding to its position in the list of rewrite rules)-  runEqualitySaturation' :: Int -> IM.IntMap (Stat schd) -> EGraphM l ()+  runEqualitySaturation' :: Int -> IM.IntMap (Stat schd) -> EGraphM a l ()   runEqualitySaturation' 30 _ = return () -- Stop after X iterations   runEqualitySaturation' i stats = do @@ -140,7 +139,7 @@                 && IM.size afterClasses == IM.size beforeClasses)           (runEqualitySaturation' (i+1) newStats) -  matchWithScheduler :: Database l -> Int -> IM.IntMap (Stat schd) -> (Int, Rewrite l) -> ([(Rewrite l, Match)], IM.IntMap (Stat schd))+  matchWithScheduler :: Database l -> Int -> IM.IntMap (Stat schd) -> (Int, Rewrite a l) -> ([(Rewrite a l, Match)], IM.IntMap (Stat schd))   matchWithScheduler db i stats = \case       (rw_id, rw :| cnd) -> first (map (first (:| cnd))) $ matchWithScheduler db i stats (rw_id, rw)       (rw_id, lhs := rhs) -> do@@ -156,11 +155,11 @@                 let matches' = ematch db lhs -- Add rewrite to the e-match substitutions                  -- Backoff scheduler: update stats-                let newStats = updateStats @schd i rw_id x stats matches'+                let newStats = updateStats schd i rw_id x stats matches'                  (map (lhs := rhs,) matches', newStats) -  applyMatchesRhs :: (Rewrite l, Match) -> EGraphM l ()+  applyMatchesRhs :: (Rewrite a l, Match) -> EGraphM a l ()   applyMatchesRhs =       \case           (rw :| cond, m@(Match subst _)) -> do@@ -189,12 +188,12 @@               return ()    -- | Represent a pattern in the e-graph a pattern given substitions-  reprPat :: Subst -> l (Pattern l) -> EGraphM l ClassId+  reprPat :: Subst -> l (Pattern l) -> EGraphM a l ClassId   reprPat subst = add . Node <=< traverse \case       VariablePattern v ->           case IM.lookup v subst of               Nothing -> error "impossible: couldn't find v in subst?"               Just i  -> return i       NonVariablePattern p -> reprPat subst p- {-# INLINEABLE runEqualitySaturation #-}+

@@ -8,6 +8,8 @@ -} module Data.Equality.Saturation.Rewrites where +import Data.Functor.Classes+ import Data.Equality.Graph import Data.Equality.Matching import Data.Equality.Matching.Database@@ -31,8 +33,8 @@ -- -- See the definition of @is_not_zero@ in the documentation for -- 'RewriteCondition'-data Rewrite lang = !(Pattern lang) := !(Pattern lang)          -- ^ Trivial Rewrite-                  | !(Rewrite lang) :| !(RewriteCondition lang) -- ^ Conditional Rewrite+data Rewrite anl lang = !(Pattern lang) := !(Pattern lang)          -- ^ Trivial Rewrite+                      | !(Rewrite anl lang) :| !(RewriteCondition anl lang) -- ^ Conditional Rewrite infix 3 := infixl 2 :| @@ -48,5 +50,9 @@ --      Just class_id -> --          egr^._class class_id._data /= Just 0 -- @-type RewriteCondition lang = Subst -> EGraph lang -> Bool+type RewriteCondition anl lang = Subst -> EGraph anl lang -> Bool ++instance Show1 lang => Show (Rewrite anl lang) where+  show (rw :| _) = show rw <> " :| <cond>"+  show (lhs := rhs) = show lhs <> " := " <> show rhs

@@ -11,7 +11,7 @@  -} module Data.Equality.Saturation.Scheduler-    ( Scheduler(..), BackoffScheduler+    ( Scheduler(..), BackoffScheduler(..), defaultBackoffScheduler     ) where  import qualified Data.IntMap.Strict as IM@@ -21,10 +21,11 @@ -- being used based on statistics it defines and collects on applied rewrite -- rules. class Scheduler s where-    type Stat s+    data Stat s      -- | Scheduler: update stats-    updateStats :: Int                -- ^ Iteration we're in+    updateStats :: s                  -- ^ The scheduler itself+                -> Int                -- ^ Iteration we're in                 -> Int                -- ^ Index of rewrite rule we're updating                 -> Maybe (Stat s)     -- ^ Current stat for this rewrite rule (we already got it so no point in doing a lookup again)                 -> IM.IntMap (Stat s) -- ^ The current stats map@@ -46,11 +47,23 @@ -- taking an unfair amount of resources. -- -- Originaly in [egg](https://docs.rs/egg/0.6.0/egg/struct.BackoffScheduler.html)-data BackoffScheduler+data BackoffScheduler = BackoffScheduler+  { matchLimit :: {-# UNPACK #-} !Int+  , banLength  :: {-# UNPACK #-} !Int }++-- | The default 'BackoffScheduler'.+-- +-- The match limit is set to @1000@ and the ban length is set to @10@.+defaultBackoffScheduler :: BackoffScheduler+defaultBackoffScheduler = BackoffScheduler 1000 10+ instance Scheduler BackoffScheduler where-    type Stat BackoffScheduler = BoSchStat+    data Stat BackoffScheduler =+      BSS { bannedUntil :: {-# UNPACK #-} !Int+          , timesBanned :: {-# UNPACK #-} !Int+          } deriving Show -    updateStats i rw currentStat stats matches =+    updateStats bos i rw currentStat stats matches =          if total_len > threshold @@ -65,16 +78,13 @@           -- TODO: Overall difficult, and buggy at the moment.           total_len = sum (map (length . matchSubst) matches) -          defaultMatchLimit = 1000-          defaultBanLength  = 10-           bannedN = case currentStat of                       Nothing -> 0;                       Just (timesBanned -> n) -> n -          threshold = defaultMatchLimit * (2^bannedN)+          threshold = matchLimit bos * (2^bannedN) -          ban_length = defaultBanLength * (2^bannedN)+          ban_length = banLength bos * (2^bannedN)            updateBans = \case             Nothing -> Just (BSS (i + ban_length) 1)@@ -82,7 +92,3 @@      isBanned i s = i < bannedUntil s --data BoSchStat = BSS { bannedUntil :: {-# UNPACK #-} !Int-                     , timesBanned :: {-# UNPACK #-} !Int-                     } deriving Show

@@ -9,7 +9,6 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE RecordWildCards #-} module Invariants where  import Test.Tasty@@ -27,7 +26,6 @@ import Data.Equality.Graph.Monad as GM import Data.Equality.Graph.Lens import Data.Equality.Graph-import Data.Equality.Analysis import Data.Equality.Extraction import Data.Equality.Saturation import Data.Equality.Matching@@ -40,12 +38,6 @@ newtype SimpleExpr l = SE (Expr l)     deriving (Functor, Foldable, Traversable, Show1, Eq1, Ord1, Language) -instance Analysis SimpleExpr where-    type Domain SimpleExpr = ()-    makeA _ _ = ()-    joinA = (<>)-    modifyA _ = id- -- | When a rewrite of type "x":=c where x is a pattern variable and c is a -- constant is used in equality saturation of any expression, all e-classes -- should be merged into a single one, since all classes are equal to c and@@ -53,11 +45,11 @@ patFoldAllClasses :: forall l. (Language l, Num (Pattern l))                   => Fix l -> Integer -> Bool patFoldAllClasses expr i =-    case IM.toList $ (eg^._classes) of+    case IM.toList (eg^._classes) of         [_] -> True         _   -> False     where-        eg :: EGraph l+        eg :: EGraph () l         eg = snd $ equalitySaturation expr [VariablePattern 1:=fromInteger i] (error "Cost function shouldn't be used" :: CostFunction l Int)  -- | Test 'compileToQuery'.@@ -93,7 +85,7 @@  -- | 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 => Var -> EGraph () lang -> Bool ematchSingletonVar v eg =     let         db = eGraphToDatabase eg@@ -122,7 +114,7 @@ -- -- ROMES:TODO Should I rebuild it here? Then the property test is that after rebuilding ...HashConsInvariant hashConsInvariant :: forall l. Language l-                  => EGraph l -> Bool+                  => EGraph () l -> Bool hashConsInvariant eg =     all f (IM.toList (eg^._classes))     where@@ -134,7 +126,7 @@             Just i' -> i' == find i eg   benchSaturate :: forall l. Language l-              => [Rewrite l] -> (l Int -> Int) -> Fix l -> Bool+              => [Rewrite () l] -> (l Int -> Int) -> Fix l -> Bool benchSaturate rws cost expr =     equalitySaturation expr rws cost `seq` True @@ -142,12 +134,12 @@ -- ROMES:TODO: Property: Extract expression after equality saturation is always better or equal to the original expression  -- ROMES:TODO: Use action trick https://jaspervdj.be/posts/2015-03-13-practical-testing-in-haskell.html-instance Arbitrary (EGraph SimpleExpr) where+instance Arbitrary (EGraph () SimpleExpr) where     arbitrary = sized $ \n -> do         exps <- forM [0..n] $ const arbitrary         -- rws :: [Rewrite Expr] <- forM [0..n] $ const arbitrary         (ids, eg) <- return $ egraph $-            mapM represent exps+            mapM GM.represent exps         ids1 <- sublistOf ids         ids2 <- sublistOf ids         return $ snd $ runEGraphM eg $ do

@@ -1,4 +1,6 @@ {-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedStrings #-}@@ -8,9 +10,14 @@ {-# LANGUAGE DeriveTraversable #-} module Lambda where +import Data.String+ import Test.Tasty import Test.Tasty.HUnit +import Data.Maybe++import qualified Data.IntMap as IM import qualified Data.Set as S  import Control.Applicative ((<|>))@@ -19,26 +26,29 @@ import Data.Ord.Deriving import Text.Show.Deriving -import Data.Equality.Graph.Lens-import Data.Equality.Graph.Monad as GM import Data.Equality.Graph import Data.Equality.Extraction import Data.Equality.Analysis import Data.Equality.Saturation import Data.Equality.Matching+import Data.Equality.Matching.Database as D+import Data.Equality.Graph.Lens  data Lambda a-    = Bool Bool-    | Num Int-    | Var a+    = Bool !Bool+    | Num !Int+    | Symbol !String+    | Use a+    | Subst a a a+     | Add a a     | Eq a a+    | If a a a+     | App a a     | Lam a a     | Let a a a     | LFix a a-    | If a a a-    | Symbol String     deriving ( Eq, Ord, Functor              , Foldable, Traversable              )@@ -47,72 +57,109 @@ deriveOrd1 ''Lambda deriveShow1 ''Lambda -data Data = Data { free :: S.Set ClassId-                 , constant :: Maybe (Fix Lambda)-                 } deriving Eq--evalL :: EGraph Lambda -> Lambda ClassId -> Maybe (Fix Lambda)-evalL egr = \case-    Bool n -> Just (Fix $ Bool n)-    Num n  -> Just (Fix $ Num n)+evalL :: Lambda (Maybe (Lambda ())) -> Maybe (Lambda ())+evalL = \case+    Bool n -> Just (Bool n)+    Num n  -> Just (Num n)     Add a b -> do-        a' <- constant (egr^._class a._data) >>= num-        b' <- constant (egr^._class b._data) >>= num-        return (Fix $ Num $ a' + b')+        a' <- a >>= num+        b' <- b >>= num+        return (Num $ a' + b')     Eq  a b -> do-        a' <- constant (egr^._class a._data)-        b' <- constant (egr^._class b._data)-        return (Fix $ Bool $  a' == b')+        a' <- a+        b' <- b+        return (Bool $ a' == b')     _ -> Nothing   where-    num :: Fix Lambda -> Maybe Int+    num :: Lambda () -> Maybe Int     num = \case-        Fix (Num i) -> Just i+        Num i -> Just i         _ -> Nothing -instance Analysis Lambda where-    type Domain Lambda = Data+type FreeVars = S.Set String+-- the lambda evaluator analysis is a combined analysis of the free variable analysis and the constant folding analysis+type LA = (FreeVars, Maybe (Lambda ())) -    makeA n egr =-      let-          freeVs = case unNode n of-            Var x -> S.singleton x-            Let v a b ->-                free (egr^._class a._data) <> S.delete v (free (egr^._class b._data))-            Lam v a -> S.delete v (free (egr^._class a._data))-            LFix v a -> S.delete v (free (egr^._class a._data))-            _ -> mconcat (map (\i -> free $ egr^._class i._data) (children n))+-- Constant folding for lambda evaluator+instance Analysis (Maybe (Lambda ())) Lambda where+  makeA = evalL+  joinA = (<|>)+  modifyA c = case c^._data of+                Nothing -> (c, [])+                Just v  -> (c, [f v])+                  where+                    f = \case+                      Bool b -> Fix $ Bool b+                      Num i  -> Fix $ Num i+                      _ -> error "impossible, lambda () can't construct this"+                       -          cnst = evalL egr (unNode n)-       in-          Data freeVs cnst+-- Free variable analysis for lambda+instance Analysis FreeVars Lambda where+  makeA = \case+    Use x -> x+    Let v a b -> (b S.\\ v) <> a+    Lam v a -> a S.\\ v+    LFix v a -> a S.\\ v+    Bool _ -> mempty+    Num _  -> mempty+    Add a b -> a <> b+    Eq a b -> a <> b+    App a b -> a <> b+    If a b c -> a <> b <> c+    Symbol x -> S.singleton x+    Subst a b c -> b <> a <> c -    joinA (Data fv1 c1) (Data fv2 c2) =-        Data (fv1 `S.intersection` fv2) (c1 <|> c2)+  joinA = (<>) -    -- modifyA :: ClassId -> EGraph l -> EGraph l-    modifyA i egr = -        case constant (egr^._class i._data) of-          Nothing -> egr-          Just c -> snd $ runEGraphM egr $ do-            new_c <- represent c-            GM.merge i new_c  instance Language Lambda  instance Num (Fix Lambda) where     fromInteger = Fix . Num . fromInteger-    (+) = error "todo..."+    (+) a b = Fix $ Add a b     (-) = error "todo..."     (*) = error "todo..."     abs = error "todo..."     signum = error "todo..." -rules :: [Rewrite Lambda]+unsafeGetSubst :: Pattern Lambda -> D.Subst -> ClassId+unsafeGetSubst (NonVariablePattern _) _ = error "unsafeGetSubst: NonVariablePattern; expecting VariablePattern"+unsafeGetSubst (VariablePattern v) subst = case IM.lookup 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++isNotSameVar :: Pattern Lambda -> Pattern Lambda -> RewriteCondition LA Lambda+isNotSameVar v1 v2 subst egr = find (unsafeGetSubst v1 subst) egr /= find (unsafeGetSubst v2 subst) egr++rules :: [Rewrite LA Lambda] rules =     [ ifP trP "x" "y" := "x"     , ifP flP "x" "y" := "y"-    -- , ifP (pat $ eq (varP "x") "e" "then" "else") := "else" :| if ...+    -- , ifP (pat $ Eq (pat $ Use "x") "e") "then" "else" := "else" :| conditionEqual (pat $ Let "x" "e" "then") (pat $ Let "x" "e" "else")++    , pat (Add "x" "y") := pat (Add "y" "x")+    , pat (Add (pat $ Add "x" "y") "z") := pat (Add "x" $ pat $ Add "y" "z")+    , pat (Eq "x" "y") := pat (Eq "y" "x")++    -- substitution introduction+    , pat (LFix "v" "e") := pat (Let "v" (pat $ LFix "v" "e") "e")+    , pat (App (pat $ Lam "v" "body") "e") := pat (Let "v" "e" "body")++    -- substitution propagation+    , pat (Let "v" "e" (pat $ App "a" "b")) := pat (App (pat $ Let "v" "e" "a") (pat $ Let "v" "e" "b"))+    , pat (Let "v" "e" (pat $ Add "a" "b")) := pat (Add (pat $ Let "v" "e" "a") (pat $ Let "v" "e" "b"))+    , pat (Let "v" "e" (pat $ Eq "a" "b")) := pat (Eq (pat $ Let "v" "e" "a") (pat $ Let "v" "e" "b"))+    , pat (Let "v" "e" (pat $ If "a" "b" "c")) := pat (If (pat $ Let "v" "e" "a") (pat $ Let "v" "e" "b") (pat $ Let "v" "e" "c"))++    -- substitution elimination+    , pat (Let "v" "e" "c") := "c" :| isConst "c" -- let const+    , pat (Let "v1" "e" (pat $ Use "v1")) := "e" -- let var same+    , pat (Let "v1" "e" (pat $ Use "v2")) := "v2" :| isNotSameVar "v1" "v2" -- let var diff+    , pat (Let "v1" "e" (pat $ Lam "v1" "body")) := pat (Lam "v1" "body") -- let lam same     ]  rewrite :: Fix Lambda -> Fix Lambda@@ -125,18 +172,33 @@      , testCase "if fl" $         rewrite (ifL fl 1 2) @?= 2-    ] +    , testCase "lambda_under" $+      -- \x -> 4 + ((\y -> y) 4) = \x -> 8+        rewrite (lam "x" (4 + app (lam "y" (var "y")) 4)) @?= lam "x" 8 +    {-+       This test requires at least the ConditionEqual rewrite condition helper+       and possibly dynamic rewrites. It would also be better to improve+       rewrite conditions before continuing down this path. +       For the analysis patch, being able to define the analysis+       compositionally and without expressiveness problems is good enough. +    , testCase "lambda_compose_many" $+        rewrite (Fix (Let "compose" (lam "f" (lam "g" (lam "x" (app (var "f") (app (var "g") (var "x"))))))+                          (Fix $ Let "add1" (lam "y" (Fix $ Add (var "y") 1)) (app (app (var "compose") (var "add1"))+                                                                                   (app (app (var "compose") (var "add1"))+                                                                                        (app (app (var "compose") (var "add1"))+                                                                                             (var "add1"))))))) @?= lam "x" (Fix $ Add "x" 5)+                                                                                             -}+    ]+ ifP :: Pattern Lambda -> Pattern Lambda -> Pattern Lambda -> Pattern Lambda ifP a b c = pat (If a b c) trP, flP :: Pattern Lambda trP = pat (Bool True) flP = pat (Bool False)-varP :: Pattern Lambda -> Pattern Lambda-varP x = pat (Var x)  -- TODO: recursion-schemes extension in separate package ifL :: Fix Lambda -> Fix Lambda -> Fix Lambda -> Fix Lambda@@ -144,3 +206,12 @@ tr, fl :: Fix Lambda tr = Fix $ Bool True fl = Fix $ Bool False+lam :: Fix Lambda -> Fix Lambda -> Fix Lambda+lam i = Fix . Lam i+var :: Fix Lambda -> Fix Lambda+var = Fix . Use+app :: Fix Lambda -> Fix Lambda -> Fix Lambda+app x y = Fix $ App x y++instance IsString (Fix Lambda) where+  fromString = Fix . Symbol

@@ -1,5 +1,7 @@ {-# LANGUAGE LambdaCase #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE DeriveTraversable #-}@@ -17,6 +19,7 @@ import Data.Equality.Saturation import Data.Equality.Language import Data.Equality.Analysis+import Data.Equality.Graph.Lens ((^.), _data)  data SymExpr a = Const Double                | Symbol String@@ -31,13 +34,25 @@ deriveOrd1  ''SymExpr deriveShow1 ''SymExpr -instance Analysis SymExpr where-  type Domain SymExpr = ()-  makeA _ _ = ()-  joinA _ _ = ()- instance Language SymExpr +instance Analysis (Maybe Double) SymExpr where+  makeA = \case+    Const x -> Just x+    Symbol _ -> Nothing+    x :+: y -> (+) <$> x <*> y+    x :*: y -> (*) <$> x <*> y+    x :/: y -> (/) <$> x <*> y++  joinA Nothing (Just x) = Just x+  joinA (Just x) Nothing = Just x+  joinA Nothing Nothing  = Nothing+  joinA (Just x) (Just y) = if x == y then Just x else error "ouch, that shouldn't have happened"++  modifyA c = case c^._data of+                Nothing -> (c, [])+                Just i  -> (c, [Fix (Const i)])+ cost :: CostFunction SymExpr Int cost = \case   Const  _ -> 1@@ -46,20 +61,21 @@   c1 :*: c2 -> c1 + c2 + 3   c1 :/: c2 -> c1 + c2 + 4 -rewrites :: [Rewrite SymExpr]+rewrites :: [Rewrite (Maybe Double) SymExpr] rewrites =   [ pat (pat ("a" :*: "b") :/: "c") := pat ("a" :*: pat ("b" :/: "c"))   , pat ("x" :/: "x")               := pat (Const 1)-  , pat ("x" :*: (pat (Const 1)))   := "x"+  , pat ("x" :*: pat (Const 1))     := "x"   ]  rewrite :: Fix SymExpr -> Fix SymExpr rewrite e = fst (equalitySaturation e rewrites cost)  e1 :: Fix SymExpr-e1 = Fix (Fix (Fix (Symbol "x") :*: Fix (Const 2)) :/: (Fix (Const 2))) -- (x*2)/2+e1 = Fix (Fix (Fix (Symbol "x") :*: Fix (Const 2)) :/: Fix (Const 2)) -- (x*2)/2  simpleSymTests :: TestTree simpleSymTests = testGroup "Simple Sym"-    [ testCase "(a*2)/2 = a" $ rewrite e1 @?= Fix (Symbol "x")+    [ testCase "(a*2)/2 = a"  $ rewrite e1 @?= Fix (Symbol "x")+    , testCase "(x/x)+1) = 4" $ rewrite (Fix $ Fix (Const 3) :+: Fix (Fix (Symbol "x") :/: Fix (Symbol "x"))) @?= Fix (Const 4)     ]

@@ -1,4 +1,5 @@ {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE BangPatterns #-} {-# LANGUAGE OverloadedStrings #-}@@ -25,7 +26,6 @@ import Control.Applicative (liftA2) import Control.Monad (unless) -import Data.Equality.Graph.Monad as GM import Data.Equality.Graph.Lens import Data.Equality.Graph import Data.Equality.Extraction@@ -109,10 +109,9 @@  -- | Define analysis for the @Expr@ language over domain @Maybe Double@ for -- constant folding-instance Analysis Expr where-    type Domain Expr = Maybe Double+instance Analysis (Maybe Double) Expr where -    makeA (Node e) egr = evalConstant ((\c -> egr^._class c._data) <$> e)+    makeA = evalConstant      -- joinA = (<|>)     joinA ma mb = do@@ -124,17 +123,16 @@         !_ <- unless (a == b || (a == 0 && b == (-0)) || (a == (-0) && b == 0)) (error "Merged non-equal constants!")         return a -    modifyA i egr =-        case egr ^._class i._data of-          Nothing -> egr-          Just d  -> snd $ runEGraphM egr $ do+    modifyA cl = case cl^._data of+                 Nothing -> (cl, [])+                 Just d -> ((_nodes %~ S.filter (F.null .unNode)) cl, [Fix (Const d)]) -            -- Add constant as e-node-            new_c <- represent (Fix $ Const d)-            _     <- GM.merge i new_c+    --         -- Add constant as e-node+    --         new_c <- represent (Fix $ Const d)+    --         _     <- GM.merge i new_c -            -- Prune all except leaf e-nodes-            modify (_class i._nodes %~ S.filter (F.null . unNode))+    --         -- Prune all except leaf e-nodes+    --         modify (_class i._nodes %~ S.filter (F.null . unNode))   @@ -161,19 +159,19 @@       Nothing -> error "Searching for non existent bound var in conditional"       Just class_id -> class_id -is_not_zero :: Pattern Expr -> RewriteCondition Expr+is_not_zero :: Pattern Expr -> RewriteCondition (Maybe Double) Expr is_not_zero v subst egr =     egr^._class (unsafeGetSubst v subst)._data /= Just 0 -is_sym :: Pattern Expr -> RewriteCondition Expr+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_const :: Pattern Expr -> RewriteCondition Expr+is_const :: Pattern Expr -> RewriteCondition (Maybe Double) Expr is_const v subst egr =     isJust (egr^._class (unsafeGetSubst v subst)._data) -is_const_or_distinct_var :: Pattern Expr -> Pattern Expr -> RewriteCondition Expr+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@@ -181,7 +179,7 @@         && (isJust (egr^._class v'._data)             || any ((\case (Sym _) -> True; _ -> False) . unNode) (egr^._class v'._nodes)) -rewrites :: [Rewrite Expr]+rewrites :: [Rewrite (Maybe Double) Expr] rewrites =     [ "a"+"b" := "b"+"a" -- comm add     , "a"*"b" := "b"*"a" -- comm mul@@ -257,9 +255,9 @@ symTests :: TestTree symTests = testGroup "Symbolic"     [ testCase "(a*2)/2 = a (custom rules)" $-        fst (equalitySaturation (("a"*2)/2) [ ("x"*"y")/"z" := "x"*("y"/"z")-                                            , "y"/"y" := 1-                                            , "x"*1 := "x"] symCost) @?= "a"+        fst (equalitySaturation @(Maybe Double) (("a"*2)/2) [ ("x"*"y")/"z" := "x"*("y"/"z")+                                                            , "y"/"y" := 1+                                                            , "x"*1 := "x"] symCost) @?= "a"      , testCase "(a/2)*2 = a (all rules)" $         rewrite (("a"/2)*2) @?= "a"@@ -269,7 +267,7 @@      , testCase "x/y (custom rules)" $         -- without backoff scheduler this will loop forever-        fst (equalitySaturation+        fst (equalitySaturation @(Maybe Double)                 ("x"/"y")                  [ "x"/"y" := "x"*(1/"y")@@ -282,13 +280,13 @@         fst (equalitySaturation (0+1) rewrites symCost)   @?= 1      , testCase "b*(1/b) = 1 (custom rules)" $-        fst (equalitySaturation ("b"*(1/"b")) [ "a"*(1/"a") := 1 ] symCost) @?= 1+        fst (equalitySaturation @(Maybe Double) ("b"*(1/"b")) [ "a"*(1/"a") := 1 ] symCost) @?= 1      , testCase "1+1=2 (constant folding)" $-        fst (equalitySaturation (1+1) [] symCost) @?= 2+        fst (equalitySaturation @(Maybe Double) (1+1) [] symCost) @?= 2      , testCase "a*(2-1) (1 rule + constant folding)" $-        fst (equalitySaturation ("a" * (2-1)) ["x"*1:="x"] symCost) @?= "a"+        fst (equalitySaturation @(Maybe Double) ("a" * (2-1)) ["x"*1:="x"] symCost) @?= "a"      , testCase "1+a*(2-1) = 1+a (all + constant folding)" $         rewrite (1+("a"*(2-1))) @?= (1+"a")

@@ -0,0 +1,145 @@+{-# language DeriveTraversable #-}+{-# language LambdaCase #-}+{-# language TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE FlexibleInstances #-}+{-# OPTIONS_GHC -Wno-unused-matches #-}+module T1 (main) where++import Test.Tasty.HUnit+import Data.Eq.Deriving+import Data.Ord.Deriving+import Text.Show.Deriving++import Data.Equality.Graph+import Data.Equality.Matching+import Data.Equality.Saturation+import Data.Equality.Saturation.Scheduler++data TreeF a = VarF Int+             | ConstF Double+             | AddF a a+             | SubF a a+             | MulF a a+             | DivF a a+             | LogF a+               deriving (Functor, Foldable, Traversable)++deriveEq1 ''TreeF+deriveOrd1 ''TreeF+deriveShow1 ''TreeF++instance Num (Fix TreeF) where+  l + r = Fix $ AddF l r+  l - r = Fix $ SubF l r+  l * r = Fix $ MulF l r+  abs   = undefined++  negate t    = fromInteger (-1) * t+  signum t    = undefined+  fromInteger = Fix . ConstF . fromInteger++instance Fractional (Fix TreeF) where+    (/) a b = Fix (DivF a b)+    fromRational = Fix . ConstF . fromRational++instance Floating (Fix TreeF) where+  pi      = undefined+  exp     = undefined+  log     = Fix . LogF+  sqrt    = undefined+  sin     = undefined+  cos     = undefined+  tan     = undefined+  asin    = undefined+  acos    = undefined+  atan    = undefined+  sinh    = undefined+  cosh    = undefined+  tanh    = undefined+  asinh   = undefined+  acosh   = undefined+  atanh   = undefined++  l ** r      = undefined+  logBase l r = undefined++instance Num (Pattern TreeF) where+  l + r = NonVariablePattern $ AddF l r+  l - r = NonVariablePattern $ SubF l r+  l * r = NonVariablePattern $ MulF l r+  abs   = undefined++  negate t    = fromInteger (-1) * t+  signum t    = undefined+  fromInteger = NonVariablePattern . ConstF . fromInteger++instance Fractional (Pattern TreeF) where+    (/) a b = NonVariablePattern (DivF a b)+    fromRational = NonVariablePattern . ConstF . fromRational++instance Floating (Pattern TreeF) where+  pi      = undefined+  exp     = undefined+  log     = NonVariablePattern . LogF+  sqrt    = undefined+  sin     = undefined+  cos     = undefined+  tan     = undefined+  asin    = undefined+  acos    = undefined+  atan    = undefined+  sinh    = undefined+  cosh    = undefined+  tanh    = undefined+  asinh   = undefined+  acosh   = undefined+  atanh   = undefined++  l ** r      = undefined+  logBase l r = undefined++instance Language TreeF++cost :: CostFunction TreeF Int+cost = \case+  ConstF _ -> 5+  VarF _ -> 1+  AddF c1 c2 -> c1 + c2 + 2+  SubF c1 c2 -> c1 + c2 + 2+  MulF c1 c2 -> c1 + c2 + 4+  DivF c1 c2 -> c1 + c2 + 5+  LogF c -> c + 2++tmpRewrites :: [Rewrite () TreeF]+tmpRewrites = [+        "x" + "y" := "y" + "x"+      , "x" * "y" := "y" * "x"+      , "x" + ("y" + "z") := ("x" + "y") + "z"+      , "x" * ("y" * "z") := ("x" * "y") * "z"+      , "x" * ("y" / "z") := ("x" * "y") / "z"+      , "x" + 0 := "x"+      , "x" * 1 := "x"+      , "x" * 0 := 0+      , "x" / "x" := 1+      , ("x" * "y") + ("x" * "z") := "x" * ("y" + "z") +      , negate ("x" + "y") := negate "x" - "y"+      , 0 - "x" := negate "x"+      , log ("x" * "y") := log "x" + log "y"+      , log ("x" / "y") := log "x" - log "y"+      , log 1 := 0+    ]++rewriteTree :: Fix TreeF -> (Fix TreeF, EGraph () TreeF)+rewriteTree t = equalitySaturation' (BackoffScheduler 1000 15) t tmpRewrites cost++x, y :: Fix TreeF+x = Fix (VarF 0)+y = Fix (VarF 1)++main :: IO ()+main = do+  fst (rewriteTree ((log x) / (x * ((y / y) / y)))) @?= (Fix $ DivF (Fix $ LogF (Fix $ VarF 0)) (Fix $ DivF (Fix $ VarF 0) (Fix $ VarF 1)))+  pure ()+

@@ -0,0 +1,49 @@+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE OverloadedStrings #-}+module T2 where++-- Tests whether this saturates just like mwillsey claims that it does in egg!++import Prelude hiding (not)++import Test.Tasty.HUnit+import Data.Deriving+import Data.Equality.Matching+import Data.Equality.Language+import Data.Equality.Extraction+import Data.Equality.Saturation++data Lang a = And a a+            | Or a a+            | Not a+            | ToElim a+            | Sym Int+            deriving (Functor, Foldable, Traversable)++deriveEq1 ''Lang+deriveOrd1 ''Lang+deriveShow1 ''Lang++instance Language Lang++x, y :: Pattern Lang+x = "x"+y = "y"+not :: Pattern Lang -> Pattern Lang+not = pat . Not++rules :: [Rewrite () Lang]+rules =+  [ pat (x `And` y) := not (pat (not x `Or` not y))+  , pat (x `Or` y) := not (pat (not x `And` not y))+  , not (not x) := pat (ToElim x)+  , pat (ToElim x) := x+  ]++main :: IO ()+main = do+  fst (equalitySaturation (Fix $ (Fix $ Not $ Fix $ Sym 0) `And` (Fix $ Not $ Fix $ Sym 1)) rules depthCost) @?= Fix (Not $ Fix $ (Fix $ Sym 0) `Or` (Fix $ Sym 1))+  pure ()+

@@ -1,18 +1,27 @@+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE OverloadedStrings #-} import Test.Tasty+import Test.Tasty.HUnit +import Control.Exception+ -- import Data.Equality.Utils import Invariants import Sym import Lambda import SimpleSym +import qualified T1+import qualified T2+ tests :: TestTree tests = testGroup "Tests"   [ symTests   , lambdaTests   , simpleSymTests   , invariants+  , testCase "T1" (T1.main `catch` (\(e :: SomeException) -> assertFailure (show e)))+  , testCase "T2" (T2.main `catch` (\(e :: SomeException) -> assertFailure (show e)))   ]  main :: IO ()