Skip to content

Commit

Permalink
Revert EvalGraph.EvalGaloisConnection fields
Browse files Browse the repository at this point in the history
  • Loading branch information
min-nguyen committed Sep 27, 2023
1 parent d911ec1 commit 3352435
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 19 deletions.
16 changes: 6 additions & 10 deletions src/EvalGraph.purs
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,9 @@ module EvalGraph
, patternMismatch
) where

import BoolAlg (BoolAlg, powerset)
import Prelude hiding (apply, add)

import BoolAlg (BoolAlg, powerset)
import Bindings (varAnon)
import Control.Monad.Error.Class (class MonadError)
import Data.Array (range, singleton) as A
Expand All @@ -29,8 +29,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, selectαs, select𝔹s, vertices)
import Lattice (Raw, 𝔹, botOf)
import Graph.Slice (bwdSlice, fwdSlice, vertices)
import Lattice (Raw)
import Pretty (prettyP)
import Primitive (string, intPair)
import Util (type (×), check, error, orElse, successful, throw, with, (×))
Expand Down Expand Up @@ -178,10 +178,9 @@ eval_module γ = go D.empty
type EvalGaloisConnection g = GaloisConnection (Set Vertex) (Set Vertex)
( dom :: BoolAlg (Set Vertex)
, codom :: BoolAlg (Set Vertex)
, selecte𝔹 :: Set Vertex -> Expr 𝔹
, selectv𝔹 :: Set Vertex -> Val 𝔹
, runδv :: (Val 𝔹 -> Val 𝔹) -> Set Vertex
, :: Expr Vertex
, g :: g
, :: Val Vertex
)

graphGC
Expand All @@ -200,10 +199,7 @@ graphGC { g, n, γα } e = do
let
dom = powerset (sinks g')
codom = powerset (vertices vα)
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 { dom, codom, selecte𝔹, selectv𝔹, runδv, g: g', fwd, bwd }
pure { dom, codom, eα, g: g', vα, fwd, bwd }
19 changes: 10 additions & 9 deletions test/Util.purs
Original file line number Diff line number Diff line change
Expand Up @@ -25,9 +25,10 @@ import EvalBwd (traceGC)
import EvalGraph (GraphConfig, graphGC)
import Graph (sinks, vertices)
import Graph.GraphImpl (GraphImpl)
import Graph.Slice (selectαs, select𝔹s)
import Graph.Slice (bwdSliceDual, fwdSliceDual, fwdSliceDeMorgan) as G
import Heterogeneous.Mapping (hmap)
import Lattice (botOf, topOf, erase, Raw)
import Lattice (botOf, erase, Raw)
import Module (parse)
import Parse (program)
import Pretty (class Pretty, prettyP)
Expand Down Expand Up @@ -115,46 +116,46 @@ testGraph s gconfig { δv, bwd_expect, fwd_expect } = do
-- | Backward
t_bwd1 <- preciseTime
let
αs_out = gc.runδv δv
αs_out = selectαs (δv (botOf gc.vα)) gc.vα
αs_in = gc.bwd αs_out
e𝔹 = gc.selecte𝔹 αs_in
e𝔹 = select𝔹s (gc.eα) αs_in
t_bwd2 <- preciseTime
let s𝔹 = gc_desug𝔹.bwd e𝔹

-- | De Morgan dual of backward
t_bwdDual1 <- preciseTime
let
αs_out_dual = gc.runδv δv
αs_out_dual = selectαs (δv (botOf gc.vα)) gc.vα
gbwd_dual = G.bwdSliceDual αs_out_dual gc.g
αs_in_dual = sinks gbwd_dual
e𝔹_dual = gc.selecte𝔹 αs_in_dual
e𝔹_dual = select𝔹s (gc.eα) αs_in_dual
t_bwdDual2 <- preciseTime

-- | Backward (all outputs selected)
t_bwdAll1 <- preciseTime
let
e𝔹_all = (gc.selecte𝔹 <<< gc.bwd <<< gc.runδv) topOf
e𝔹_all = select𝔹s gc.eα $ gc.bwd $ gc.codom.top
t_bwdAll2 <- preciseTime

-- | Forward (round-tripping)
t_fwd1 <- preciseTime
let
αs_out' = gc.fwd αs_in
v𝔹 = gc.selectv𝔹 αs_out'
v𝔹 = select𝔹s gc. αs_out'
t_fwd2 <- preciseTime

-- | De Morgan dual of forward
t_fwdDual1 <- preciseTime
let
gfwd_dual = G.fwdSliceDual αs_in gc.g
v𝔹_dual = gc.selectv𝔹 (vertices gfwd_dual)
v𝔹_dual = select𝔹s gc. (vertices gfwd_dual)
t_fwdDual2 <- preciseTime

-- | Forward (round-tripping) using De Morgan dual
t_fwdAsDeMorgan1 <- preciseTime
let
gfwd_demorgan = G.fwdSliceDeMorgan αs_in gc.g
v𝔹_demorgan = gc.selectv𝔹 (vertices gfwd_demorgan) <#> not
v𝔹_demorgan = select𝔹s gc. (vertices gfwd_demorgan) <#> not
t_fwdAsDeMorgan2 <- preciseTime

lift do
Expand Down

0 comments on commit 3352435

Please sign in to comment.