From 9b605afc7705b2f18f638b9f5ae18f8b37329e88 Mon Sep 17 00:00:00 2001
From: min-nguyen <minhnguyen1995@googlemail.com>
Date: Wed, 27 Sep 2023 10:36:21 +0100
Subject: [PATCH] Refactor fields of Graph-based EvalGaloisConnection

---
 src/EvalGraph.purs | 14 +++++++++-----
 test/Util.purs     | 19 +++++++++----------
 2 files changed, 18 insertions(+), 15 deletions(-)

diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs
index 7c76bb2db..9bcbb19b8 100644
--- a/src/EvalGraph.purs
+++ b/src/EvalGraph.purs
@@ -28,8 +28,8 @@ import GaloisConnection (GaloisConnection)
 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)
-import Lattice (Raw)
+import Graph.Slice (bwdSlice, fwdSlice, selectαs, select𝔹s, vertices)
+import Lattice (Raw, 𝔹, botOf)
 import Pretty (prettyP)
 import Primitive (string, intPair)
 import Util (type (×), check, error, orElse, successful, throw, with, (×))
@@ -175,9 +175,10 @@ eval_module γ = go D.empty
       go (γ' <+> γ'') (Module ds) αs
 
 type EvalGaloisConnection g a b = GaloisConnection a b
-   ( eα :: Expr Vertex
+   ( selecte𝔹 :: a -> Expr 𝔹
+   , selectv𝔹 :: b -> Val 𝔹
+   , runδv :: (Val 𝔹 -> Val 𝔹) -> b
    , g :: g
-   , vα :: Val Vertex
    )
 
 graphGC
@@ -194,7 +195,10 @@ graphGC { g, n, γα } e = do
          vα <- eval γα eα S.empty
          pure (eα × vα)
    let
+      selecte𝔹 αs = select𝔹s eα αs
+      selectv𝔹 αs = select𝔹s vα αs
+      runδv δv = selectαs (δv (botOf vα)) vα
       fwd αs = G.vertices (fwdSlice αs g') `intersection` vertices vα
       -- TODO: want (vertices eα `union` foldMap vertices γα) rather than sinks g' here?
       bwd αs = G.vertices (bwdSlice αs g') `intersection` sinks g'
-   pure { eα, g: g', vα, fwd, bwd }
+   pure { selecte𝔹, selectv𝔹, runδv, g: g', fwd, bwd }
diff --git a/test/Util.purs b/test/Util.purs
index 6263c1d23..825e59f7a 100644
--- a/test/Util.purs
+++ b/test/Util.purs
@@ -25,7 +25,6 @@ import EvalGraph (GraphConfig, graphGC)
 import Graph (sinks, vertices)
 import Graph.GraphImpl (GraphImpl)
 import Graph.Slice (bwdSliceDual, fwdSliceDual, fwdSliceDeMorgan) as G
-import Graph.Slice (selectαs, select𝔹s)
 import Heterogeneous.Mapping (hmap)
 import Lattice (botOf, topOf, erase, Raw)
 import Module (parse)
@@ -107,48 +106,48 @@ testGraph s gconfig { δv, bwd_expect, fwd_expect } = do
    -- | Backward
    tBwd1 <- preciseTime
    let
-      αs_out = selectαs (δv (botOf gc.vα)) gc.vα
+      αs_out = gc.runδv δv
       αs_in = gc.bwd αs_out
-      e𝔹 = select𝔹s gc.eα αs_in
+      e𝔹 = gc.selecte𝔹 αs_in
    tBwd2 <- preciseTime
    let s𝔹 = desugBwd e𝔹 s
 
    -- | De Morgan dual of backward
    tBwdDual1 <- preciseTime
    let
-      αs_out_dual = selectαs (δv (botOf gc.vα)) gc.vα
+      αs_out_dual = gc.runδv δv
       gbwd_dual = G.bwdSliceDual αs_out_dual gc.g
       αs_in_dual = sinks gbwd_dual
-      e𝔹_dual = select𝔹s gc.eα αs_in_dual
+      e𝔹_dual = gc.selecte𝔹 αs_in_dual
    tBwdDual2 <- preciseTime
 
    -- | Backward (all outputs selected)
    tBwdAll1 <- preciseTime
    let
-      αs_out_all = selectαs (topOf gc.vα) gc.vα
+      αs_out_all = gc.runδv topOf
       αs_in_all = gc.bwd αs_out_all
-      e𝔹_all = select𝔹s gc.eα αs_in_all
+      e𝔹_all = gc.selecte𝔹 αs_in_all
    tBwdAll2 <- preciseTime
 
    -- | Forward (round-tripping)
    tFwd1 <- preciseTime
    let
       αs_out' = gc.fwd αs_in
-      v𝔹 = select𝔹s gc.vα αs_out'
+      v𝔹 = gc.selectv𝔹 αs_out'
    tFwd2 <- preciseTime
 
    -- | De Morgan dual of forward
    tFwdDual1 <- preciseTime
    let
       gfwd_dual = G.fwdSliceDual αs_in gc.g
-      v𝔹_dual = select𝔹s gc.vα (vertices gfwd_dual)
+      v𝔹_dual = gc.selectv𝔹 (vertices gfwd_dual)
    tFwdDual2 <- preciseTime
 
    -- | Forward (round-tripping) using De Morgan dual
    tFwdAsDeMorgan1 <- preciseTime
    let
       gfwd_demorgan = G.fwdSliceDeMorgan αs_in gc.g
-      v𝔹_demorgan = select𝔹s gc.vα (vertices gfwd_demorgan) <#> not
+      v𝔹_demorgan = gc.selectv𝔹 (vertices gfwd_demorgan) <#> not
    tFwdAsDeMorgan2 <- preciseTime
 
    lift do