From 3ff3c3a5b512cb263865979398d6a87580833b39 Mon Sep 17 00:00:00 2001 From: min-nguyen Date: Wed, 27 Sep 2023 09:58:13 +0100 Subject: [PATCH 1/5] Remove redundant fields from Trace-based EvalGaloisConnection --- src/EvalBwd.purs | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/EvalBwd.purs b/src/EvalBwd.purs index 29798f332..0ad4101c9 100644 --- a/src/EvalBwd.purs +++ b/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 } From 4c1b0f922fe37f1d02ed6439e3e175d3ae02bd43 Mon Sep 17 00:00:00 2001 From: min-nguyen Date: Wed, 27 Sep 2023 10:00:42 +0100 Subject: [PATCH 2/5] Remove redundant GraphConfig field from Graph-Based EvalGaloisConnection --- src/EvalGraph.purs | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs index 9253198fe..7c76bb2db 100644 --- a/src/EvalGraph.purs +++ b/src/EvalGraph.purs @@ -175,8 +175,7 @@ eval_module γ = go D.empty go (γ' <+> γ'') (Module ds) αs type EvalGaloisConnection g a b = GaloisConnection a b - ( gconfig :: GraphConfig g - , eα :: Expr Vertex + ( eα :: Expr Vertex , g :: g , vα :: Val Vertex ) @@ -188,7 +187,7 @@ graphGC => GraphConfig g -> Raw Expr -> m (EvalGaloisConnection g (Set Vertex) (Set Vertex)) -graphGC gconfig@{ g, n, γα } e = do +graphGC { g, n, γα } e = do (g' × _) × eα × vα <- do runWithGraphAllocT (g × n) $ do eα <- alloc e @@ -198,4 +197,4 @@ graphGC gconfig@{ g, n, γα } e = do 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 { eα, g: g', vα, fwd, bwd } From 9b605afc7705b2f18f638b9f5ae18f8b37329e88 Mon Sep 17 00:00:00 2001 From: min-nguyen Date: Wed, 27 Sep 2023 10:36:21 +0100 Subject: [PATCH 3/5] 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 From 577fa5f423ad86dd6ca80fdd4b8f605dc52855c9 Mon Sep 17 00:00:00 2001 From: min-nguyen Date: Wed, 27 Sep 2023 10:40:35 +0100 Subject: [PATCH 4/5] Simplified Backward (all outputs selected) --- test/Util.purs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/test/Util.purs b/test/Util.purs index 825e59f7a..614514b07 100644 --- a/test/Util.purs +++ b/test/Util.purs @@ -124,9 +124,7 @@ testGraph s gconfig { δv, bwd_expect, fwd_expect } = do -- | Backward (all outputs selected) tBwdAll1 <- preciseTime let - αs_out_all = gc.runδv topOf - αs_in_all = gc.bwd αs_out_all - e𝔹_all = gc.selecte𝔹 αs_in_all + e𝔹_all = (gc.selecte𝔹 <<< gc.bwd <<< gc.runδv) topOf tBwdAll2 <- preciseTime -- | Forward (round-tripping) From d78c8e24f90b77f38f7e705af3b5b7e858660d74 Mon Sep 17 00:00:00 2001 From: min-nguyen Date: Wed, 27 Sep 2023 10:56:58 +0100 Subject: [PATCH 5/5] Specialise Graph.EvalGaloisConnection to use Set Vertex for domain + codomain --- src/EvalGraph.purs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs index 9bcbb19b8..eb860c77c 100644 --- a/src/EvalGraph.purs +++ b/src/EvalGraph.purs @@ -174,10 +174,10 @@ eval_module γ = go D.empty γ'' <- closeDefs (γ <+> γ') ρ αs go (γ' <+> γ'') (Module ds) αs -type EvalGaloisConnection g a b = GaloisConnection a b - ( selecte𝔹 :: a -> Expr 𝔹 - , selectv𝔹 :: b -> Val 𝔹 - , runδv :: (Val 𝔹 -> Val 𝔹) -> b +type EvalGaloisConnection g = GaloisConnection (Set Vertex) (Set Vertex) + ( selecte𝔹 :: Set Vertex -> Expr 𝔹 + , selectv𝔹 :: Set Vertex -> Val 𝔹 + , runδv :: (Val 𝔹 -> Val 𝔹) -> Set Vertex , g :: g ) @@ -187,7 +187,7 @@ graphGC => Graph g => GraphConfig g -> Raw Expr - -> m (EvalGaloisConnection g (Set Vertex) (Set Vertex)) + -> m (EvalGaloisConnection g) graphGC { g, n, γα } e = do (g' × _) × eα × vα <- do runWithGraphAllocT (g × n) $ do