Skip to content

Commit

Permalink
Refactor fields of Graph-based EvalGaloisConnection
Browse files Browse the repository at this point in the history
  • Loading branch information
min-nguyen committed Sep 27, 2023
1 parent 4c1b0f9 commit 9b605af
Show file tree
Hide file tree
Showing 2 changed files with 18 additions and 15 deletions.
14 changes: 9 additions & 5 deletions src/EvalGraph.purs
Original file line number Diff line number Diff line change
Expand Up @@ -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, (×))
Expand Down Expand Up @@ -175,9 +175,10 @@ eval_module γ = go D.empty
go (γ' <+> γ'') (Module ds) αs

type EvalGaloisConnection g a b = GaloisConnection a b
( :: Expr Vertex
( selecte𝔹 :: a -> Expr 𝔹
, selectv𝔹 :: b -> Val 𝔹
, runδv :: (Val 𝔹 -> Val 𝔹) -> b
, g :: g
, :: Val Vertex
)

graphGC
Expand All @@ -194,7 +195,10 @@ graphGC { g, n, γα } e = do
<- 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 }
19 changes: 9 additions & 10 deletions test/Util.purs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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. α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. α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. α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. α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. (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. (vertices gfwd_demorgan) <#> not
v𝔹_demorgan = gc.selectv𝔹 (vertices gfwd_demorgan) <#> not
tFwdAsDeMorgan2 <- preciseTime

lift do
Expand Down

0 comments on commit 9b605af

Please sign in to comment.