From 6c4cb92d0efd57e668d824cefbb0168c3e9f96a6 Mon Sep 17 00:00:00 2001
From: Roly Perera <roly.perera@dynamicaspects.org>
Date: Mon, 25 Sep 2023 16:36:01 +0100
Subject: [PATCH 01/18] =?UTF-8?q?=F0=9F=A7=A9=20[consolidate]:=20Minor=20t?=
 =?UTF-8?q?idyup.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/EvalGraph.purs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs
index 97ff05103..9011e1e71 100644
--- a/src/EvalGraph.purs
+++ b/src/EvalGraph.purs
@@ -175,7 +175,7 @@ eval_module γ = go D.empty
       γ'' <- closeDefs (γ <+> γ') ρ αs
       go (γ' <+> γ'') (Module ds) αs
 
-evalWithConfig :: forall g m a. MonadError Error m => Graph g => GraphConfig g -> Expr a -> m ((g × Int) × Expr Vertex × Val Vertex)
+evalWithConfig :: forall g m. MonadError Error m => Graph g => GraphConfig g -> Raw Expr -> m ((g × Int) × Expr Vertex × Val Vertex)
 evalWithConfig { g, n, γα } e =
    runWithGraphAllocT (g × n) $ do
       eα <- alloc e
@@ -189,9 +189,9 @@ graphGC
    => GraphConfig g
    -> Raw Expr
    -> m (GaloisConnection (Set Vertex) (Set Vertex))
-graphGC { g: g0, n, γα } e = do
-   (g × _) × vα × eα <- evalWithConfig { g: g0, n, γα } e
+graphGC { g, n, γα } e = do
+   (g' × _) × vα × eα <- evalWithConfig { g, n, γα } e
    pure $
-      { fwd: \αs -> G.vertices (fwdSlice αs g) `intersection` vertices vα
-      , bwd: \αs -> G.vertices (bwdSlice αs g) `intersection` vertices eα -- TODO: include γα
+      { fwd: \αs -> G.vertices (fwdSlice αs g') `intersection` vertices vα
+      , bwd: \αs -> G.vertices (bwdSlice αs g') `intersection` vertices eα -- TODO: include γα
       }

From 13b7088974a178b6fad4212e0aa4ff7f41c6f512 Mon Sep 17 00:00:00 2001
From: Roly Perera <roly.perera@dynamicaspects.org>
Date: Mon, 25 Sep 2023 17:10:51 +0100
Subject: [PATCH 02/18] =?UTF-8?q?=F0=9F=A7=A9=20[consolidate]:=20Simplify?=
 =?UTF-8?q?=20testTrace.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 test/Util.purs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/test/Util.purs b/test/Util.purs
index fd024b5d0..95b9df17a 100644
--- a/test/Util.purs
+++ b/test/Util.purs
@@ -67,9 +67,9 @@ testParse s = do
 
 testTrace :: Raw SE.Expr -> GraphConfig GraphImpl -> TestConfig -> MayFailT Aff TraceRow
 testTrace s { γα: γ } { δv, bwd_expect, fwd_expect } = do
-   let s𝔹 × γ𝔹 = (botOf s) × (botOf <$> γ)
+   let γ𝔹 = botOf <$> γ
    -- | Eval
-   e𝔹 <- desug s𝔹
+   e𝔹 <- desug s
    tEval1 <- preciseTime
    t × v𝔹 <- eval γ𝔹 e𝔹 bot
    tEval2 <- preciseTime
@@ -77,7 +77,7 @@ testTrace s { γα: γ } { δv, bwd_expect, fwd_expect } = do
    -- | Backward
    tBwd1 <- preciseTime
    let
-      v𝔹' = δv v𝔹
+      v𝔹' = δv (botOf v𝔹)
       { γ: γ𝔹', e: e𝔹' } = evalBwd (erase <$> γ𝔹) (erase e𝔹) v𝔹' t
    tBwd2 <- preciseTime
    let s𝔹' = desugBwd e𝔹' s

From a24fb2b9dd91bca754d2f84b62c41099253d5440 Mon Sep 17 00:00:00 2001
From: Roly Perera <roly.perera@dynamicaspects.org>
Date: Mon, 25 Sep 2023 17:11:51 +0100
Subject: [PATCH 03/18] =?UTF-8?q?=F0=9F=A7=A9=20[consolidate]:=20Simplify?=
 =?UTF-8?q?=20testTrace.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 test/Util.purs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/test/Util.purs b/test/Util.purs
index 95b9df17a..163986c79 100644
--- a/test/Util.purs
+++ b/test/Util.purs
@@ -69,16 +69,16 @@ testTrace :: Raw SE.Expr -> GraphConfig GraphImpl -> TestConfig -> MayFailT Aff
 testTrace s { γα: γ } { δv, bwd_expect, fwd_expect } = do
    let γ𝔹 = botOf <$> γ
    -- | Eval
-   e𝔹 <- desug s
+   e <- desug s
    tEval1 <- preciseTime
-   t × v𝔹 <- eval γ𝔹 e𝔹 bot
+   t × v𝔹 <- eval γ𝔹 e bot
    tEval2 <- preciseTime
 
    -- | Backward
    tBwd1 <- preciseTime
    let
       v𝔹' = δv (botOf v𝔹)
-      { γ: γ𝔹', e: e𝔹' } = evalBwd (erase <$> γ𝔹) (erase e𝔹) v𝔹' t
+      { γ: γ𝔹', e: e𝔹' } = evalBwd (erase <$> γ𝔹) e v𝔹' t
    tBwd2 <- preciseTime
    let s𝔹' = desugBwd e𝔹' s
 

From 41f91488dfe4a0f51f3b28c3203ea2a3772506b0 Mon Sep 17 00:00:00 2001
From: Roly Perera <roly.perera@dynamicaspects.org>
Date: Mon, 25 Sep 2023 17:14:40 +0100
Subject: [PATCH 04/18] =?UTF-8?q?=F0=9F=A7=A9=20[consolidate]:=20Simplify?=
 =?UTF-8?q?=20testTrace.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 test/Util.purs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/test/Util.purs b/test/Util.purs
index 163986c79..9d815b5e2 100644
--- a/test/Util.purs
+++ b/test/Util.purs
@@ -66,19 +66,19 @@ testParse s = do
          lift $ fail "not equal"
 
 testTrace :: Raw SE.Expr -> GraphConfig GraphImpl -> TestConfig -> MayFailT Aff TraceRow
-testTrace s { γα: γ } { δv, bwd_expect, fwd_expect } = do
-   let γ𝔹 = botOf <$> γ
+testTrace s { γα } { δv, bwd_expect, fwd_expect } = do
+   let γ = erase <$> γα
    -- | Eval
    e <- desug s
    tEval1 <- preciseTime
-   t × v𝔹 <- eval γ𝔹 e bot
+   t × v𝔹 <- eval γ e bot
    tEval2 <- preciseTime
 
    -- | Backward
    tBwd1 <- preciseTime
    let
       v𝔹' = δv (botOf v𝔹)
-      { γ: γ𝔹', e: e𝔹' } = evalBwd (erase <$> γ𝔹) e v𝔹' t
+      { γ: γ𝔹', e: e𝔹' } = evalBwd γ e v𝔹' t
    tBwd2 <- preciseTime
    let s𝔹' = desugBwd e𝔹' s
 

From ae0a6151fe4cac7fc307022ef1b7cd61d125d358 Mon Sep 17 00:00:00 2001
From: Roly Perera <roly.perera@dynamicaspects.org>
Date: Mon, 25 Sep 2023 17:16:53 +0100
Subject: [PATCH 05/18] =?UTF-8?q?=F0=9F=A7=A9=20[rename]:=20Clean=20up=20n?=
 =?UTF-8?q?ames.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 test/Util.purs | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/test/Util.purs b/test/Util.purs
index 9d815b5e2..bf8675dff 100644
--- a/test/Util.purs
+++ b/test/Util.purs
@@ -71,32 +71,32 @@ testTrace s { γα } { δv, bwd_expect, fwd_expect } = do
    -- | Eval
    e <- desug s
    tEval1 <- preciseTime
-   t × v𝔹 <- eval γ e bot
+   t × v <- eval γ e bot
    tEval2 <- preciseTime
 
    -- | Backward
    tBwd1 <- preciseTime
    let
-      v𝔹' = δv (botOf v𝔹)
-      { γ: γ𝔹', e: e𝔹' } = evalBwd γ e v𝔹' t
+      v𝔹 = δv (botOf v)
+      { γ: γ𝔹, e: e𝔹 } = evalBwd γ e v𝔹 t
    tBwd2 <- preciseTime
-   let s𝔹' = desugBwd e𝔹' s
+   let s𝔹' = desugBwd e𝔹 s
 
    -- | Forward (round-tripping)
-   e𝔹'' <- desug s𝔹'
+   e𝔹' <- desug s𝔹'
    tFwd1 <- preciseTime
-   _ × v𝔹'' <- eval γ𝔹' e𝔹'' top
+   _ × v𝔹' <- eval γ𝔹 e𝔹' top
    tFwd2 <- preciseTime
 
    lift do
-      unless (isGraphical v𝔹') $
-         log (prettyP v𝔹'')
+      unless (isGraphical v𝔹) $
+         log (prettyP v𝔹')
       -- | Check backward selections
       unless (null bwd_expect) $
          checkPretty "Trace-based source selection" bwd_expect s𝔹'
       -- | Check round-trip selections
-      unless (isGraphical v𝔹') $
-         checkPretty "Trace-based value" fwd_expect v𝔹''
+      unless (isGraphical v𝔹) $
+         checkPretty "Trace-based value" fwd_expect v𝔹'
 
    pure { tEval: tdiff tEval1 tEval2, tBwd: tdiff tBwd1 tBwd2, tFwd: tdiff tFwd1 tFwd2 }
 

From 04b73e0cf75e7e915fbc4faeae0945d6e4a62d70 Mon Sep 17 00:00:00 2001
From: Roly Perera <roly.perera@dynamicaspects.org>
Date: Mon, 25 Sep 2023 17:18:51 +0100
Subject: [PATCH 06/18] =?UTF-8?q?=F0=9F=A7=A9=20[modify-unused]:=20Extend?=
 =?UTF-8?q?=20GaloisConnection=20to=20GaloisConnectionTraced.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/EvalBwd.purs | 21 ++++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

diff --git a/src/EvalBwd.purs b/src/EvalBwd.purs
index 1330ea262..22942d2c8 100644
--- a/src/EvalBwd.purs
+++ b/src/EvalBwd.purs
@@ -21,7 +21,6 @@ import Dict (fromFoldable, singleton, toUnfoldable) as D
 import Effect.Exception (Error)
 import Eval (eval)
 import Expr (Cont(..), Elim(..), Expr(..), RecDefs, VarDef(..), bv)
-import GaloisConnection (GaloisConnection)
 import Lattice (Raw, bot, botOf, expand, (∨))
 import Partial.Unsafe (unsafePartial)
 import Trace (AppTrace(..), Trace(..), VarDef(..)) as T
@@ -201,8 +200,20 @@ evalBwd' v (T.LetRec ρ t) =
    γ1' × ρ' × α' = closeDefsBwd γ2
 evalBwd' _ _ = error absurd
 
-traceGC :: forall a m. MonadError Error m => Ann a => Raw Env -> Raw Expr -> Trace -> m (GaloisConnection (EvalBwdResult a) (Val a))
-traceGC γ e t = pure $
-   { fwd: \{ γ: γ', e: e', α } -> snd $ fromRight $ runExcept $ eval γ' e' α
-   , bwd: \v -> evalBwd γ e v t
+-- Haven't yet figured out how to extend record types.
+type GaloisConnectionTraced a b =
+   { γ :: Raw Env
+   , e :: Raw Expr
+   , t :: Trace
+   , v :: Raw Val
+   , fwd :: a -> b
+   , bwd :: b -> a
    }
+
+traceGC :: forall a m. MonadError Error m => Ann a => Raw Env -> Raw Expr -> m (GaloisConnectionTraced (EvalBwdResult a) (Val a))
+traceGC γ e = do
+   t × v <- eval γ e bot
+   let
+      bwd v' = evalBwd γ e v' t
+      fwd { γ: γ', e: e', α } = snd $ fromRight $ runExcept $ eval γ' e' α
+   pure { γ, e, t, v, fwd, bwd }

From dd077a481b2fff2a9e4a5599d14b21a7e875f4ad Mon Sep 17 00:00:00 2001
From: Roly Perera <roly.perera@dynamicaspects.org>
Date: Mon, 25 Sep 2023 17:23:16 +0100
Subject: [PATCH 07/18] =?UTF-8?q?=F0=9F=A7=A9=20[refactor]:=20Start=20usin?=
 =?UTF-8?q?g=20traceGC.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 test/Util.purs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/test/Util.purs b/test/Util.purs
index bf8675dff..acf1b3048 100644
--- a/test/Util.purs
+++ b/test/Util.purs
@@ -21,14 +21,14 @@ import Effect.Aff (Aff)
 import Effect.Class.Console (log)
 import Effect.Exception (Error)
 import Eval (eval)
-import EvalBwd (evalBwd)
+import EvalBwd (traceGC)
 import EvalGraph (GraphConfig, evalWithConfig)
 import Graph (sinks, sources, vertices)
 import Graph.GraphImpl (GraphImpl)
 import Graph.Slice (bwdSlice, fwdSlice, fwdSliceDeMorgan) as G
 import Graph.Slice (selectαs, select𝔹s)
 import Heterogeneous.Mapping (hmap)
-import Lattice (bot, botOf, topOf, erase, Raw)
+import Lattice (botOf, topOf, erase, Raw)
 import Module (parse)
 import Parse (program)
 import Pretty (class Pretty, prettyP)
@@ -71,14 +71,14 @@ testTrace s { γα } { δv, bwd_expect, fwd_expect } = do
    -- | Eval
    e <- desug s
    tEval1 <- preciseTime
-   t × v <- eval γ e bot
+   gc <- traceGC γ e
    tEval2 <- preciseTime
 
    -- | Backward
    tBwd1 <- preciseTime
    let
-      v𝔹 = δv (botOf v)
-      { γ: γ𝔹, e: e𝔹 } = evalBwd γ e v𝔹 t
+      v𝔹 = δv (botOf gc.v)
+      { γ: γ𝔹, e: e𝔹 } = gc.bwd v𝔹
    tBwd2 <- preciseTime
    let s𝔹' = desugBwd e𝔹 s
 

From f9de642a1c16882c1b76222f44a88436a3ce29dd Mon Sep 17 00:00:00 2001
From: Roly Perera <roly.perera@dynamicaspects.org>
Date: Mon, 25 Sep 2023 17:28:10 +0100
Subject: [PATCH 08/18] =?UTF-8?q?=F0=9F=A7=A9=20[refactor]:=20Plug=20in=20?=
 =?UTF-8?q?gc.fwd.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 test/Util.purs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/test/Util.purs b/test/Util.purs
index acf1b3048..835ef3689 100644
--- a/test/Util.purs
+++ b/test/Util.purs
@@ -20,7 +20,6 @@ import Desugarable (desug, desugBwd)
 import Effect.Aff (Aff)
 import Effect.Class.Console (log)
 import Effect.Exception (Error)
-import Eval (eval)
 import EvalBwd (traceGC)
 import EvalGraph (GraphConfig, evalWithConfig)
 import Graph (sinks, sources, vertices)
@@ -85,7 +84,7 @@ testTrace s { γα } { δv, bwd_expect, fwd_expect } = do
    -- | Forward (round-tripping)
    e𝔹' <- desug s𝔹'
    tFwd1 <- preciseTime
-   _ × v𝔹' <- eval γ𝔹 e𝔹' top
+   let v𝔹' = gc.fwd { γ: γ𝔹, e: e𝔹', α: top }
    tFwd2 <- preciseTime
 
    lift do

From c9e1f410d5b79011f1689cd1706bb051e0479a15 Mon Sep 17 00:00:00 2001
From: Roly Perera <roly.perera@dynamicaspects.org>
Date: Tue, 26 Sep 2023 05:55:03 +0100
Subject: [PATCH 09/18] =?UTF-8?q?=F0=9F=A7=A9=20[rename]:=20Drop=20prime.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 test/Util.purs | 20 +++++++++-----------
 1 file changed, 9 insertions(+), 11 deletions(-)

diff --git a/test/Util.purs b/test/Util.purs
index 835ef3689..d26842c70 100644
--- a/test/Util.purs
+++ b/test/Util.purs
@@ -75,27 +75,25 @@ testTrace s { γα } { δv, bwd_expect, fwd_expect } = do
 
    -- | Backward
    tBwd1 <- preciseTime
-   let
-      v𝔹 = δv (botOf gc.v)
-      { γ: γ𝔹, e: e𝔹 } = gc.bwd v𝔹
+   let { γ: γ𝔹, e: e𝔹 } = gc.bwd (δv (botOf gc.v))
    tBwd2 <- preciseTime
-   let s𝔹' = desugBwd e𝔹 s
+   let s𝔹 = desugBwd e𝔹 s
 
    -- | Forward (round-tripping)
-   e𝔹' <- desug s𝔹'
+   e𝔹' <- desug s𝔹
    tFwd1 <- preciseTime
-   let v𝔹' = gc.fwd { γ: γ𝔹, e: e𝔹', α: top }
+   let v𝔹 = gc.fwd { γ: γ𝔹, e: e𝔹', α: top }
    tFwd2 <- preciseTime
 
    lift do
-      unless (isGraphical v𝔹) $
-         log (prettyP v𝔹')
+      unless (isGraphical gc.v) $
+         log (prettyP v𝔹)
       -- | Check backward selections
       unless (null bwd_expect) $
-         checkPretty "Trace-based source selection" bwd_expect s𝔹'
+         checkPretty "Trace-based source selection" bwd_expect s𝔹
       -- | Check round-trip selections
-      unless (isGraphical v𝔹) $
-         checkPretty "Trace-based value" fwd_expect v𝔹'
+      unless (isGraphical gc.v) $
+         checkPretty "Trace-based value" fwd_expect v𝔹
 
    pure { tEval: tdiff tEval1 tEval2, tBwd: tdiff tBwd1 tBwd2, tFwd: tdiff tFwd1 tFwd2 }
 

From eee4f5cbb1d05bfebe860b18718aee197c3458c7 Mon Sep 17 00:00:00 2001
From: Roly Perera <roly.perera@dynamicaspects.org>
Date: Tue, 26 Sep 2023 06:00:11 +0100
Subject: [PATCH 10/18] =?UTF-8?q?=F0=9F=A7=A9=20[consolidate]:=20Inline.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 test/Util.purs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/test/Util.purs b/test/Util.purs
index d26842c70..4cf61fc44 100644
--- a/test/Util.purs
+++ b/test/Util.purs
@@ -66,11 +66,10 @@ testParse s = do
 
 testTrace :: Raw SE.Expr -> GraphConfig GraphImpl -> TestConfig -> MayFailT Aff TraceRow
 testTrace s { γα } { δv, bwd_expect, fwd_expect } = do
-   let γ = erase <$> γα
    -- | Eval
    e <- desug s
    tEval1 <- preciseTime
-   gc <- traceGC γ e
+   gc <- traceGC (erase <$> γα) e
    tEval2 <- preciseTime
 
    -- | Backward

From cb0b962b0ad88d94ba2aac77f677e2adf82b45d9 Mon Sep 17 00:00:00 2001
From: Roly Perera <roly.perera@dynamicaspects.org>
Date: Tue, 26 Sep 2023 06:23:30 +0100
Subject: [PATCH 11/18] =?UTF-8?q?=F0=9F=A7=A9=20[modify-unused]:=20Flesh?=
 =?UTF-8?q?=20out=20graph=20GC.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/EvalBwd.purs   |  6 +++---
 src/EvalGraph.purs | 24 ++++++++++++++++--------
 test/Util.purs     |  4 ++--
 3 files changed, 21 insertions(+), 13 deletions(-)

diff --git a/src/EvalBwd.purs b/src/EvalBwd.purs
index 22942d2c8..a59c768ae 100644
--- a/src/EvalBwd.purs
+++ b/src/EvalBwd.purs
@@ -200,8 +200,8 @@ evalBwd' v (T.LetRec ρ t) =
    γ1' × ρ' × α' = closeDefsBwd γ2
 evalBwd' _ _ = error absurd
 
--- Haven't yet figured out how to extend record types.
-type GaloisConnectionTraced a b =
+-- TODO: somehow extend GaloisConnection, e.g. by aggregation or row polymorphism.
+type EvalGaloisConnection a b =
    { γ :: Raw Env
    , e :: Raw Expr
    , t :: Trace
@@ -210,7 +210,7 @@ type GaloisConnectionTraced a b =
    , bwd :: b -> a
    }
 
-traceGC :: forall a m. MonadError Error m => Ann a => Raw Env -> Raw Expr -> m (GaloisConnectionTraced (EvalBwdResult a) (Val a))
+traceGC :: forall a m. MonadError Error m => Ann a => Raw Env -> Raw Expr -> m (EvalGaloisConnection (EvalBwdResult a) (Val a))
 traceGC γ e = do
    t × v <- eval γ e bot
    let
diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs
index 9011e1e71..c7a30933a 100644
--- a/src/EvalGraph.purs
+++ b/src/EvalGraph.purs
@@ -25,7 +25,6 @@ import DataType (checkArity, arity, consistentWith, dataTypeFor, showCtr)
 import Dict (disjointUnion, fromFoldable, empty, get, keys, lookup, singleton) as D
 import Effect.Exception (Error)
 import Expr (Cont(..), Elim(..), Expr(..), VarDef(..), RecDefs, Module(..), fv, asExpr)
-import GaloisConnection (GaloisConnection)
 import Graph (class Graph, Vertex)
 import Graph (vertices) as G
 import Graph.GraphWriter (class MonadGraphAlloc, alloc, new, runWithGraphAllocT)
@@ -182,16 +181,25 @@ evalWithConfig { g, n, γα } e =
       vα <- eval γα eα S.empty
       pure (eα × vα)
 
+type EvalGaloisConnection g a b =
+   { gconfig :: GraphConfig g
+   , eα :: Expr Vertex
+   , g :: g
+   , vα :: Val Vertex
+   , fwd :: a -> b
+   , bwd :: b -> a
+   }
+
 graphGC
    :: forall g m
     . MonadError Error m
    => Graph g
    => GraphConfig g
    -> Raw Expr
-   -> m (GaloisConnection (Set Vertex) (Set Vertex))
-graphGC { g, n, γα } e = do
-   (g' × _) × vα × eα <- evalWithConfig { g, n, γα } e
-   pure $
-      { fwd: \αs -> G.vertices (fwdSlice αs g') `intersection` vertices vα
-      , bwd: \αs -> G.vertices (bwdSlice αs g') `intersection` vertices eα -- TODO: include γα
-      }
+   -> m (EvalGaloisConnection g (Set Vertex) (Set Vertex))
+graphGC gconfig@{ g, n, γα } e = do
+   (g' × _) × eα × vα <- evalWithConfig { g, n, γα } e
+   let
+      fwd αs = G.vertices (fwdSlice αs g') `intersection` vertices vα
+      bwd αs = G.vertices (bwdSlice αs g') `intersection` vertices eα -- TODO: include γα
+   pure { gconfig, eα, g: g', vα, fwd, bwd }
diff --git a/test/Util.purs b/test/Util.purs
index 4cf61fc44..9211ec680 100644
--- a/test/Util.purs
+++ b/test/Util.purs
@@ -97,11 +97,11 @@ testTrace s { γα } { δv, bwd_expect, fwd_expect } = do
    pure { tEval: tdiff tEval1 tEval2, tBwd: tdiff tBwd1 tBwd2, tFwd: tdiff tFwd1 tFwd2 }
 
 testGraph :: Raw SE.Expr -> GraphConfig GraphImpl -> TestConfig -> MayFailT Aff GraphRow
-testGraph s gconf { δv, bwd_expect, fwd_expect } = do
+testGraph s gconfig { δv, bwd_expect, fwd_expect } = do
    -- | Eval
    e <- desug s
    tEval1 <- preciseTime
-   (g × _) × eα × vα <- evalWithConfig gconf e
+   (g × _) × eα × vα <- evalWithConfig gconfig e
    tEval2 <- preciseTime
 
    -- | Backward

From d981b19a52ae3d07a4ff904d1d9b0e1e4d8a1662 Mon Sep 17 00:00:00 2001
From: Roly Perera <roly.perera@dynamicaspects.org>
Date: Tue, 26 Sep 2023 06:32:13 +0100
Subject: [PATCH 12/18] =?UTF-8?q?=F0=9F=A7=A9=20[refactor]:=20Use=20graph?=
 =?UTF-8?q?=20GC.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 test/Util.purs | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/test/Util.purs b/test/Util.purs
index 9211ec680..1d5d886d7 100644
--- a/test/Util.purs
+++ b/test/Util.purs
@@ -21,7 +21,7 @@ import Effect.Aff (Aff)
 import Effect.Class.Console (log)
 import Effect.Exception (Error)
 import EvalBwd (traceGC)
-import EvalGraph (GraphConfig, evalWithConfig)
+import EvalGraph (GraphConfig, graphGC)
 import Graph (sinks, sources, vertices)
 import Graph.GraphImpl (GraphImpl)
 import Graph.Slice (bwdSlice, fwdSlice, fwdSliceDeMorgan) as G
@@ -33,7 +33,7 @@ import Parse (program)
 import Pretty (class Pretty, prettyP)
 import SExpr (Expr) as SE
 import Test.Spec.Assertions (fail)
-import Util (MayFailT, (×), successful)
+import Util (MayFailT, successful)
 import Val (Val(..), class Ann)
 
 type TestConfig =
@@ -101,16 +101,16 @@ testGraph s gconfig { δv, bwd_expect, fwd_expect } = do
    -- | Eval
    e <- desug s
    tEval1 <- preciseTime
-   (g × _) × eα × vα <- evalWithConfig gconfig e
+   gc <- graphGC gconfig e
    tEval2 <- preciseTime
 
    -- | Backward
    tBwd1 <- preciseTime
    let
-      αs_out = selectαs (δv (botOf vα)) vα
-      gbwd = G.bwdSlice αs_out g
+      αs_out = selectαs (δv (botOf gc.vα)) gc.vα
+      gbwd = G.bwdSlice αs_out gc.g
       αs_in = sinks gbwd
-      e𝔹 = select𝔹s eα αs_in
+      e𝔹 = select𝔹s gc.eα αs_in
    tBwd2 <- preciseTime
    let
       s𝔹 = desugBwd e𝔹 (erase s)
@@ -118,24 +118,24 @@ testGraph s gconfig { δv, bwd_expect, fwd_expect } = do
    -- | Backward (all outputs selected)
    tBwdAll1 <- preciseTime
    let
-      αs_out_all = selectαs (topOf vα) vα
-      gbwd_all = G.bwdSlice αs_out_all g
+      αs_out_all = selectαs (topOf gc.vα) gc.vα
+      gbwd_all = G.bwdSlice αs_out_all gc.g
       αs_in_all = sinks gbwd_all
-      e𝔹_all = select𝔹s eα αs_in_all
+      e𝔹_all = select𝔹s gc.eα αs_in_all
    tBwdAll2 <- preciseTime
 
    -- | Forward (round-tripping)
    tFwd1 <- preciseTime
    let
-      gfwd = G.fwdSlice αs_in g
-      v𝔹 = select𝔹s vα (vertices gfwd)
+      gfwd = G.fwdSlice αs_in gc.g
+      v𝔹 = select𝔹s gc.vα (vertices gfwd)
    tFwd2 <- preciseTime
 
    -- | Forward (round-tripping) using De Morgan dual
    tFwdDeMorgan1 <- preciseTime
    let
-      gfwd' = G.fwdSliceDeMorgan αs_in g
-      v𝔹' = select𝔹s vα (vertices gfwd') <#> not
+      gfwd' = G.fwdSliceDeMorgan αs_in gc.g
+      v𝔹' = select𝔹s gc.vα (vertices gfwd') <#> not
    tFwdDeMorgan2 <- preciseTime
 
    lift do

From f7bcca676618293fbceed941d1707a15b62a9442 Mon Sep 17 00:00:00 2001
From: Roly Perera <roly.perera@dynamicaspects.org>
Date: Tue, 26 Sep 2023 06:39:18 +0100
Subject: [PATCH 13/18] =?UTF-8?q?=F0=9F=A7=A9=20[consolidate]:=20Simplify?=
 =?UTF-8?q?=20testGraph.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/EvalGraph.purs | 5 +++--
 test/Util.purs     | 5 ++---
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs
index c7a30933a..06ef0bcaa 100644
--- a/src/EvalGraph.purs
+++ b/src/EvalGraph.purs
@@ -25,7 +25,7 @@ import DataType (checkArity, arity, consistentWith, dataTypeFor, showCtr)
 import Dict (disjointUnion, fromFoldable, empty, get, keys, lookup, singleton) as D
 import Effect.Exception (Error)
 import Expr (Cont(..), Elim(..), Expr(..), VarDef(..), RecDefs, Module(..), fv, asExpr)
-import Graph (class Graph, Vertex)
+import Graph (class Graph, Vertex, sinks)
 import Graph (vertices) as G
 import Graph.GraphWriter (class MonadGraphAlloc, alloc, new, runWithGraphAllocT)
 import Graph.Slice (bwdSlice, fwdSlice, vertices)
@@ -201,5 +201,6 @@ graphGC gconfig@{ g, n, γα } e = do
    (g' × _) × eα × vα <- evalWithConfig { g, n, γα } e
    let
       fwd αs = G.vertices (fwdSlice αs g') `intersection` vertices vα
-      bwd αs = G.vertices (bwdSlice αs g') `intersection` vertices eα -- TODO: include γα
+      -- TODO: (vertices eα `union` vertices γα) rather than sinks g'
+      bwd αs = G.vertices (bwdSlice αs g') `intersection` sinks g'
    pure { gconfig, eα, g: g', vα, fwd, bwd }
diff --git a/test/Util.purs b/test/Util.purs
index 1d5d886d7..55c903dfa 100644
--- a/test/Util.purs
+++ b/test/Util.purs
@@ -108,8 +108,7 @@ testGraph s gconfig { δv, bwd_expect, fwd_expect } = do
    tBwd1 <- preciseTime
    let
       αs_out = selectαs (δv (botOf gc.vα)) gc.vα
-      gbwd = G.bwdSlice αs_out gc.g
-      αs_in = sinks gbwd
+      αs_in = gc.bwd αs_out
       e𝔹 = select𝔹s gc.eα αs_in
    tBwd2 <- preciseTime
    let
@@ -146,7 +145,7 @@ testGraph s gconfig { δv, bwd_expect, fwd_expect } = do
       unless (isGraphical v𝔹) do
          checkPretty "Graph-based value" fwd_expect v𝔹
          checkPretty "Graph-based value (De Morgan)" fwd_expect v𝔹'
-      sources gbwd `shouldSatisfy "fwd ⚬ bwd round-tripping property"`
+      αs_out `shouldSatisfy "fwd ⚬ bwd round-tripping property"`
          (flip subset (sources gfwd))
       -- | To avoid unused variables when benchmarking
       unless false do

From d449e1bc12ea179044f58999212d4051a19b8819 Mon Sep 17 00:00:00 2001
From: Roly Perera <roly.perera@dynamicaspects.org>
Date: Tue, 26 Sep 2023 06:39:47 +0100
Subject: [PATCH 14/18] =?UTF-8?q?=F0=9F=A7=A9=20[consolidate]:=20Redundant?=
 =?UTF-8?q?=20erase.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 test/Util.purs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/Util.purs b/test/Util.purs
index 55c903dfa..0e756ec3c 100644
--- a/test/Util.purs
+++ b/test/Util.purs
@@ -112,7 +112,7 @@ testGraph s gconfig { δv, bwd_expect, fwd_expect } = do
       e𝔹 = select𝔹s gc.eα αs_in
    tBwd2 <- preciseTime
    let
-      s𝔹 = desugBwd e𝔹 (erase s)
+      s𝔹 = desugBwd e𝔹 s
 
    -- | Backward (all outputs selected)
    tBwdAll1 <- preciseTime

From fcec014b2ad2c1ba3e81d46dc34251a49e58a8b9 Mon Sep 17 00:00:00 2001
From: Roly Perera <roly.perera@dynamicaspects.org>
Date: Tue, 26 Sep 2023 06:41:34 +0100
Subject: [PATCH 15/18] =?UTF-8?q?=F0=9F=A7=A9=20[consolidate]:=20Simplify?=
 =?UTF-8?q?=20testGraph.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 test/Util.purs | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/test/Util.purs b/test/Util.purs
index 0e756ec3c..7a84492bb 100644
--- a/test/Util.purs
+++ b/test/Util.purs
@@ -22,9 +22,9 @@ import Effect.Class.Console (log)
 import Effect.Exception (Error)
 import EvalBwd (traceGC)
 import EvalGraph (GraphConfig, graphGC)
-import Graph (sinks, sources, vertices)
+import Graph (sources, vertices)
 import Graph.GraphImpl (GraphImpl)
-import Graph.Slice (bwdSlice, fwdSlice, fwdSliceDeMorgan) as G
+import Graph.Slice (fwdSlice, fwdSliceDeMorgan) as G
 import Graph.Slice (selectαs, select𝔹s)
 import Heterogeneous.Mapping (hmap)
 import Lattice (botOf, topOf, erase, Raw)
@@ -111,15 +111,13 @@ testGraph s gconfig { δv, bwd_expect, fwd_expect } = do
       αs_in = gc.bwd αs_out
       e𝔹 = select𝔹s gc.eα αs_in
    tBwd2 <- preciseTime
-   let
-      s𝔹 = desugBwd e𝔹 s
+   let s𝔹 = desugBwd e𝔹 s
 
    -- | Backward (all outputs selected)
    tBwdAll1 <- preciseTime
    let
       αs_out_all = selectαs (topOf gc.vα) gc.vα
-      gbwd_all = G.bwdSlice αs_out_all gc.g
-      αs_in_all = sinks gbwd_all
+      αs_in_all = gc.bwd αs_out_all
       e𝔹_all = select𝔹s gc.eα αs_in_all
    tBwdAll2 <- preciseTime
 

From 4a3e4fcf090cb68e47fb975ac23167f86cb4f72b Mon Sep 17 00:00:00 2001
From: Roly Perera <roly.perera@dynamicaspects.org>
Date: Tue, 26 Sep 2023 06:46:41 +0100
Subject: [PATCH 16/18] =?UTF-8?q?=F0=9F=A7=A9=20[consolidate]:=20Simplify?=
 =?UTF-8?q?=20testGraph.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 test/Util.purs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/test/Util.purs b/test/Util.purs
index 7a84492bb..24d52a5db 100644
--- a/test/Util.purs
+++ b/test/Util.purs
@@ -22,9 +22,9 @@ import Effect.Class.Console (log)
 import Effect.Exception (Error)
 import EvalBwd (traceGC)
 import EvalGraph (GraphConfig, graphGC)
-import Graph (sources, vertices)
+import Graph (vertices)
 import Graph.GraphImpl (GraphImpl)
-import Graph.Slice (fwdSlice, fwdSliceDeMorgan) as G
+import Graph.Slice (fwdSliceDeMorgan) as G
 import Graph.Slice (selectαs, select𝔹s)
 import Heterogeneous.Mapping (hmap)
 import Lattice (botOf, topOf, erase, Raw)
@@ -124,8 +124,8 @@ testGraph s gconfig { δv, bwd_expect, fwd_expect } = do
    -- | Forward (round-tripping)
    tFwd1 <- preciseTime
    let
-      gfwd = G.fwdSlice αs_in gc.g
-      v𝔹 = select𝔹s gc.vα (vertices gfwd)
+      αs_out' = gc.fwd αs_in
+      v𝔹 = select𝔹s gc.vα αs_out'
    tFwd2 <- preciseTime
 
    -- | Forward (round-tripping) using De Morgan dual
@@ -144,7 +144,7 @@ testGraph s gconfig { δv, bwd_expect, fwd_expect } = do
          checkPretty "Graph-based value" fwd_expect v𝔹
          checkPretty "Graph-based value (De Morgan)" fwd_expect v𝔹'
       αs_out `shouldSatisfy "fwd ⚬ bwd round-tripping property"`
-         (flip subset (sources gfwd))
+         (flip subset αs_out')
       -- | To avoid unused variables when benchmarking
       unless false do
          log ("BwdAll selected nodes: " <> show αs_out_all)

From 3b0ae2a4dd7bb224de67507bd8d4a03fa0d3af1e Mon Sep 17 00:00:00 2001
From: Roly Perera <roly.perera@dynamicaspects.org>
Date: Tue, 26 Sep 2023 07:04:27 +0100
Subject: [PATCH 17/18] =?UTF-8?q?=F0=9F=A7=A9=20[doc]=20:=20Note=20on=20fw?=
 =?UTF-8?q?dSliceDeMorgan,=20graph=20bwd.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/EvalGraph.purs   | 4 ++--
 src/Graph/Slice.purs | 1 +
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs
index 06ef0bcaa..8886da40c 100644
--- a/src/EvalGraph.purs
+++ b/src/EvalGraph.purs
@@ -16,7 +16,7 @@ import Control.Monad.Error.Class (class MonadError)
 import Data.Array (range, singleton) as A
 import Data.Either (Either(..))
 import Data.Exists (runExists)
-import Data.List (List(..), (:), length, snoc, unzip, zip)
+import Data.List (List(..), length, snoc, unzip, zip, (:))
 import Data.Set (Set, empty, insert, intersection, singleton, union)
 import Data.Set as S
 import Data.Traversable (sequence, traverse)
@@ -201,6 +201,6 @@ graphGC gconfig@{ g, n, γα } e = do
    (g' × _) × eα × vα <- evalWithConfig { g, n, γα } e
    let
       fwd αs = G.vertices (fwdSlice αs g') `intersection` vertices vα
-      -- TODO: (vertices eα `union` vertices γα) rather than sinks g'
+      -- TODO: want (vertices eα `union` foldMap vertices γα) rather than sinks g' here?
       bwd αs = G.vertices (bwdSlice αs g') `intersection` sinks g'
    pure { gconfig, eα, g: g', vα, fwd, bwd }
diff --git a/src/Graph/Slice.purs b/src/Graph/Slice.purs
index 601776e0c..24f3eb95a 100644
--- a/src/Graph/Slice.purs
+++ b/src/Graph/Slice.purs
@@ -27,6 +27,7 @@ bwdSlice αs0 g0 = fst $ runWithGraph $ tailRecM go (empty × L.fromFoldable αs
       extend α βs
       pure $ Loop ((visited # insert α) × (L.fromFoldable βs <> αs))
 
+-- Doesn't do the final negation.
 fwdSliceDeMorgan :: forall g. Graph g => Set Vertex -> g -> g
 fwdSliceDeMorgan αs_0 g_0 =
    bwdSlice (sinks g_0 `difference` αs_0) (op g_0)

From aa6d940e8af77562686ad0543ce122a9d620d48d Mon Sep 17 00:00:00 2001
From: Roly Perera <roly.perera@dynamicaspects.org>
Date: Tue, 26 Sep 2023 08:36:05 +0100
Subject: [PATCH 18/18] =?UTF-8?q?=F0=9F=A7=A9=20[consolidate]:=20Inline=20?=
 =?UTF-8?q?evalWithConfig.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/EvalGraph.purs | 14 +++++---------
 1 file changed, 5 insertions(+), 9 deletions(-)

diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs
index 8886da40c..8d14b310e 100644
--- a/src/EvalGraph.purs
+++ b/src/EvalGraph.purs
@@ -2,7 +2,6 @@ module EvalGraph
    ( GraphConfig
    , apply
    , eval
-   , evalWithConfig
    , eval_module
    , graphGC
    , match
@@ -174,13 +173,6 @@ eval_module γ = go D.empty
       γ'' <- closeDefs (γ <+> γ') ρ αs
       go (γ' <+> γ'') (Module ds) αs
 
-evalWithConfig :: forall g m. MonadError Error m => Graph g => GraphConfig g -> Raw Expr -> m ((g × Int) × Expr Vertex × Val Vertex)
-evalWithConfig { g, n, γα } e =
-   runWithGraphAllocT (g × n) $ do
-      eα <- alloc e
-      vα <- eval γα eα S.empty
-      pure (eα × vα)
-
 type EvalGaloisConnection g a b =
    { gconfig :: GraphConfig g
    , eα :: Expr Vertex
@@ -198,7 +190,11 @@ graphGC
    -> Raw Expr
    -> m (EvalGaloisConnection g (Set Vertex) (Set Vertex))
 graphGC gconfig@{ g, n, γα } e = do
-   (g' × _) × eα × vα <- evalWithConfig { g, n, γα } e
+   (g' × _) × eα × vα <- do
+      runWithGraphAllocT (g × n) $ do
+         eα <- alloc e
+         vα <- eval γα eα S.empty
+         pure (eα × vα)
    let
       fwd αs = G.vertices (fwdSlice αs g') `intersection` vertices vα
       -- TODO: want (vertices eα `union` foldMap vertices γα) rather than sinks g' here?