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 } diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs index 9253198fe..eb860c77c 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, (×)) @@ -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 } diff --git a/test/Util.purs b/test/Util.purs index 6263c1d23..614514b07 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,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