From 33524358b3b1c314fe52efc5ed39f982a8d9fa57 Mon Sep 17 00:00:00 2001 From: min-nguyen Date: Wed, 27 Sep 2023 17:03:55 +0100 Subject: [PATCH] Revert EvalGraph.EvalGaloisConnection fields --- src/EvalGraph.purs | 16 ++++++---------- test/Util.purs | 19 ++++++++++--------- 2 files changed, 16 insertions(+), 19 deletions(-) diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs index c4f0f66ec..d2dd155a2 100644 --- a/src/EvalGraph.purs +++ b/src/EvalGraph.purs @@ -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 @@ -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, (×)) @@ -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 + , eα :: Expr Vertex , g :: g + , vα :: Val Vertex ) graphGC @@ -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 } diff --git a/test/Util.purs b/test/Util.purs index 1c7ad3b87..486739405 100644 --- a/test/Util.purs +++ b/test/Util.purs @@ -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) @@ -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.vα α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.vα (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.vα (vertices gfwd_demorgan) <#> not t_fwdAsDeMorgan2 <- preciseTime lift do