Benchmarking

src/EvalBwd.purs

@@ -202,10 +202,7 @@ evalBwd' v (T.LetRec ρ t) =
 evalBwd' _ _ = error absurd
 
 type EvalGaloisConnection a = GaloisConnection (EvalBwdResult a) (Val a)
-   ( γ :: Raw Env
-   , e :: Raw Expr
-   , t :: Trace
-   , v :: Raw Val
+   ( v :: Raw Val
    )
 
 traceGC :: forall a m. MonadError Error m => Ann a => Raw Env -> Raw Expr -> m (EvalGaloisConnection a)
@@ -214,4 +211,4 @@ traceGC γ e = do
    let
       bwd v' = evalBwd γ e v' t
       fwd { γ: γ', e: e', α } = snd $ fromRight $ runExcept $ eval γ' e' α
-   pure { γ, e, t, v, fwd, bwd }
+   pure { v, fwd, bwd }

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, (×))
@@ -174,11 +174,11 @@ eval_module γ = go D.empty
       γ'' <- closeDefs (γ <+> γ') ρ αs
       go (γ' <+> γ'') (Module ds) αs
 
-type EvalGaloisConnection g a b = GaloisConnection a b
-   ( gconfig :: GraphConfig g
-   , eα :: Expr Vertex
+type EvalGaloisConnection g = GaloisConnection (Set Vertex) (Set Vertex)
+   ( selecte𝔹 :: Set Vertex -> Expr 𝔹
+   , selectv𝔹 :: Set Vertex -> Val 𝔹
+   , runδv :: (Val 𝔹 -> Val 𝔹) -> Set Vertex
    , g :: g
-   , vα :: Val Vertex
    )
 
 graphGC
@@ -187,15 +187,18 @@ graphGC
    => Graph g
    => GraphConfig g
    -> Raw Expr
-   -> m (EvalGaloisConnection g (Set Vertex) (Set Vertex))
-graphGC gconfig@{ g, n, γα } e = do
+   -> m (EvalGaloisConnection g)
+graphGC { g, n, γα } e = do
    (g' × _) × eα × vα <- do
       runWithGraphAllocT (g × n) $ do
          eα <- alloc e
          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 { gconfig, eα, g: g', vα, fwd, bwd }
+   pure { selecte𝔹, selectv𝔹, runδv, g: g', fwd, bwd }

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,46 @@ 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_in_all = gc.bwd αs_out_all
-      e𝔹_all = select𝔹s gc.eα αs_in_all
+      e𝔹_all = (gc.selecte𝔹 <<< gc.bwd <<< gc.runδv) topOf
    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