diff --git a/src/EvalBwd.purs b/src/EvalBwd.purs index 1330ea262..a59c768ae 100644 --- a/src/EvalBwd.purs +++ b/src/EvalBwd.purs @@ -21,7 +21,6 @@ import Dict (fromFoldable, singleton, toUnfoldable) as D import Effect.Exception (Error) import Eval (eval) import Expr (Cont(..), Elim(..), Expr(..), RecDefs, VarDef(..), bv) -import GaloisConnection (GaloisConnection) import Lattice (Raw, bot, botOf, expand, (∨)) import Partial.Unsafe (unsafePartial) import Trace (AppTrace(..), Trace(..), VarDef(..)) as T @@ -201,8 +200,20 @@ evalBwd' v (T.LetRec ρ t) = γ1' × ρ' × α' = closeDefsBwd γ2 evalBwd' _ _ = error absurd -traceGC :: forall a m. MonadError Error m => Ann a => Raw Env -> Raw Expr -> Trace -> m (GaloisConnection (EvalBwdResult a) (Val a)) -traceGC γ e t = pure $ - { fwd: \{ γ: γ', e: e', α } -> snd $ fromRight $ runExcept $ eval γ' e' α - , bwd: \v -> evalBwd γ e v t +-- TODO: somehow extend GaloisConnection, e.g. by aggregation or row polymorphism. +type EvalGaloisConnection a b = + { γ :: Raw Env + , e :: Raw Expr + , t :: Trace + , v :: Raw Val + , fwd :: a -> b + , bwd :: b -> a } + +traceGC :: forall a m. MonadError Error m => Ann a => Raw Env -> Raw Expr -> m (EvalGaloisConnection (EvalBwdResult a) (Val a)) +traceGC γ e = do + t × v <- eval γ e bot + let + bwd v' = evalBwd γ e v' t + fwd { γ: γ', e: e', α } = snd $ fromRight $ runExcept $ eval γ' e' α + pure { γ, e, t, v, fwd, bwd } diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs index 97ff05103..8d14b310e 100644 --- a/src/EvalGraph.purs +++ b/src/EvalGraph.purs @@ -2,7 +2,6 @@ module EvalGraph ( GraphConfig , apply , eval - , evalWithConfig , eval_module , graphGC , match @@ -16,7 +15,7 @@ import Control.Monad.Error.Class (class MonadError) import Data.Array (range, singleton) as A import Data.Either (Either(..)) import Data.Exists (runExists) -import Data.List (List(..), (:), length, snoc, unzip, zip) +import Data.List (List(..), length, snoc, unzip, zip, (:)) import Data.Set (Set, empty, insert, intersection, singleton, union) import Data.Set as S import Data.Traversable (sequence, traverse) @@ -25,8 +24,7 @@ import DataType (checkArity, arity, consistentWith, dataTypeFor, showCtr) import Dict (disjointUnion, fromFoldable, empty, get, keys, lookup, singleton) as D import Effect.Exception (Error) import Expr (Cont(..), Elim(..), Expr(..), VarDef(..), RecDefs, Module(..), fv, asExpr) -import GaloisConnection (GaloisConnection) -import Graph (class Graph, Vertex) +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) @@ -175,12 +173,14 @@ eval_module γ = go D.empty γ'' <- closeDefs (γ <+> γ') ρ αs go (γ' <+> γ'') (Module ds) αs -evalWithConfig :: forall g m a. MonadError Error m => Graph g => GraphConfig g -> Expr a -> m ((g × Int) × Expr Vertex × Val Vertex) -evalWithConfig { g, n, γα } e = - runWithGraphAllocT (g × n) $ do - eα <- alloc e - vα <- eval γα eα S.empty - pure (eα × vα) +type EvalGaloisConnection g a b = + { gconfig :: GraphConfig g + , eα :: Expr Vertex + , g :: g + , vα :: Val Vertex + , fwd :: a -> b + , bwd :: b -> a + } graphGC :: forall g m @@ -188,10 +188,15 @@ graphGC => Graph g => GraphConfig g -> Raw Expr - -> m (GaloisConnection (Set Vertex) (Set Vertex)) -graphGC { g: g0, n, γα } e = do - (g × _) × vα × eα <- evalWithConfig { g: g0, n, γα } e - pure $ - { fwd: \αs -> G.vertices (fwdSlice αs g) `intersection` vertices vα - , bwd: \αs -> G.vertices (bwdSlice αs g) `intersection` vertices eα -- TODO: include γα - } + -> m (EvalGaloisConnection g (Set Vertex) (Set Vertex)) +graphGC gconfig@{ g, n, γα } e = do + (g' × _) × eα × vα <- do + runWithGraphAllocT (g × n) $ do + eα <- alloc e + vα <- eval γα eα S.empty + pure (eα × vα) + let + 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 } diff --git a/src/Graph/Slice.purs b/src/Graph/Slice.purs index 5a34451a9..99200ff77 100644 --- a/src/Graph/Slice.purs +++ b/src/Graph/Slice.purs @@ -28,6 +28,11 @@ bwdSlice αs0 g0 = fst $ runWithGraph $ tailRecM go (empty × L.fromFoldable αs extend α βs pure $ Loop ((visited # insert α) × (L.fromFoldable βs <> αs)) +-- Doesn't do the final negation.. +fwdSliceDeMorgan :: forall g. Graph g => Set Vertex -> g -> g +fwdSliceDeMorgan αs_0 g_0 = + bwdSlice (sinks g_0 `difference` αs_0) (op g_0) + -- | De Morgan dual of backward slicing (◁_G)° ≡ Forward slicing on the opposite graph (▷_{G_op}) bwdSliceDual :: forall g. Graph g => Set Vertex -> g -> g bwdSliceDual αs0 g0 = fwdSlice αs0 (op g0) diff --git a/test/Util.purs b/test/Util.purs index dee0486c2..6263c1d23 100644 --- a/test/Util.purs +++ b/test/Util.purs @@ -20,21 +20,20 @@ import Desugarable (desug, desugBwd) import Effect.Aff (Aff) import Effect.Class.Console (log) import Effect.Exception (Error) -import Eval (eval) -import EvalBwd (evalBwd) -import EvalGraph (GraphConfig, evalWithConfig) -import Graph (sinks, sources, vertices) +import EvalBwd (traceGC) +import EvalGraph (GraphConfig, graphGC) +import Graph (sinks, vertices) import Graph.GraphImpl (GraphImpl) -import Graph.Slice (bwdSlice, bwdSliceDual, fwdSlice, fwdSliceDual, fwdSliceAsDeMorgan) as G +import Graph.Slice (bwdSliceDual, fwdSliceDual, fwdSliceDeMorgan) as G import Graph.Slice (selectαs, select𝔹s) import Heterogeneous.Mapping (hmap) -import Lattice (bot, botOf, topOf, erase, Raw) +import Lattice (botOf, topOf, erase, Raw) import Module (parse) import Parse (program) import Pretty (class Pretty, prettyP) import SExpr (Expr) as SE import Test.Spec.Assertions (fail) -import Util (MayFailT, (×), successful) +import Util (MayFailT, successful) import Val (Val(..), class Ann) type TestConfig = @@ -66,96 +65,90 @@ testParse s = do lift $ fail "not equal" testTrace :: Raw SE.Expr -> GraphConfig GraphImpl -> TestConfig -> MayFailT Aff TraceRow -testTrace s { γα: γ } { δv, bwd_expect, fwd_expect } = do - let s𝔹 × γ𝔹 = (botOf s) × (botOf <$> γ) +testTrace s { γα } { δv, bwd_expect, fwd_expect } = do -- | Eval - e𝔹 <- desug s𝔹 + e <- desug s tEval1 <- preciseTime - t × v𝔹 <- eval γ𝔹 e𝔹 bot + gc <- traceGC (erase <$> γα) e tEval2 <- preciseTime -- | Backward tBwd1 <- preciseTime - let - v𝔹' = δv v𝔹 - { γ: γ𝔹', e: e𝔹' } = evalBwd (erase <$> γ𝔹) (erase e𝔹) v𝔹' t + let { γ: γ𝔹, e: e𝔹 } = gc.bwd (δv (botOf gc.v)) tBwd2 <- preciseTime - let s𝔹' = desugBwd e𝔹' s + let s𝔹 = desugBwd e𝔹 s -- | Forward (round-tripping) - e𝔹'' <- desug s𝔹' + e𝔹' <- desug s𝔹 tFwd1 <- preciseTime - _ × v𝔹'' <- eval γ𝔹' e𝔹'' top + let v𝔹 = gc.fwd { γ: γ𝔹, e: e𝔹', α: top } tFwd2 <- preciseTime lift do - unless (isGraphical v𝔹') $ - log (prettyP v𝔹'') + unless (isGraphical gc.v) $ + log (prettyP v𝔹) -- | Check backward selections unless (null bwd_expect) $ - checkPretty "Trace-based source selection" bwd_expect s𝔹' + checkPretty "Trace-based source selection" bwd_expect s𝔹 -- | Check round-trip selections - unless (isGraphical v𝔹') $ - checkPretty "Trace-based value" fwd_expect v𝔹'' + unless (isGraphical gc.v) $ + checkPretty "Trace-based value" fwd_expect v𝔹 pure { tEval: tdiff tEval1 tEval2, tBwd: tdiff tBwd1 tBwd2, tFwd: tdiff tFwd1 tFwd2 } testGraph :: Raw SE.Expr -> GraphConfig GraphImpl -> TestConfig -> MayFailT Aff GraphRow -testGraph s gconf { δv, bwd_expect, fwd_expect } = do +testGraph s gconfig { δv, bwd_expect, fwd_expect } = do -- | Eval e <- desug s tEval1 <- preciseTime - (g × _) × eα × vα <- evalWithConfig gconf e + gc <- graphGC gconfig e tEval2 <- preciseTime -- | Backward tBwd1 <- preciseTime let - αs_out = selectαs (δv (botOf vα)) vα - gbwd = G.bwdSlice αs_out g - αs_in = sinks gbwd - e𝔹 = select𝔹s eα αs_in + αs_out = selectαs (δv (botOf gc.vα)) gc.vα + αs_in = gc.bwd αs_out + e𝔹 = select𝔹s gc.eα αs_in tBwd2 <- preciseTime - let - s𝔹 = desugBwd e𝔹 (erase s) + let s𝔹 = desugBwd e𝔹 s -- | De Morgan dual of backward tBwdDual1 <- preciseTime let - αs_out_dual = selectαs (δv (botOf vα)) vα - gbwd_dual = G.bwdSliceDual αs_out_dual g + α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 = select𝔹s eα αs_in_dual + e𝔹_dual = select𝔹s gc.eα αs_in_dual tBwdDual2 <- preciseTime -- | Backward (all outputs selected) tBwdAll1 <- preciseTime let - αs_out_all = selectαs (topOf vα) vα - gbwd_all = G.bwdSlice αs_out_all g - αs_in_all = sinks gbwd_all - e𝔹_all = select𝔹s eα αs_in_all + α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 tBwdAll2 <- preciseTime -- | Forward (round-tripping) tFwd1 <- preciseTime let - gfwd = G.fwdSlice αs_in g - v𝔹 = select𝔹s vα (vertices gfwd) + αs_out' = gc.fwd αs_in + v𝔹 = select𝔹s gc.vα αs_out' tFwd2 <- preciseTime -- | De Morgan dual of forward tFwdDual1 <- preciseTime let - gfwd_dual = G.fwdSliceDual αs_in g - v𝔹_dual = select𝔹s vα (vertices gfwd_dual) + gfwd_dual = G.fwdSliceDual αs_in gc.g + v𝔹_dual = select𝔹s gc.vα (vertices gfwd_dual) tFwdDual2 <- preciseTime -- | Forward (round-tripping) using De Morgan dual tFwdAsDeMorgan1 <- preciseTime let - gfwd_demorgan = G.fwdSliceAsDeMorgan αs_in g - v𝔹_demorgan = select𝔹s vα (vertices gfwd_demorgan) <#> not + gfwd_demorgan = G.fwdSliceDeMorgan αs_in gc.g + v𝔹_demorgan = select𝔹s gc.vα (vertices gfwd_demorgan) <#> not tFwdAsDeMorgan2 <- preciseTime lift do @@ -166,8 +159,8 @@ testGraph s gconf { δv, bwd_expect, fwd_expect } = do unless (isGraphical v𝔹) do checkPretty "Graph-based value" fwd_expect v𝔹 checkPretty "Graph-based value (De Morgan)" fwd_expect v𝔹_demorgan - sources gbwd `shouldSatisfy "fwd ⚬ bwd round-tripping property"` - (flip subset (sources gfwd)) + αs_out `shouldSatisfy "fwd ⚬ bwd round-tripping property"` + (flip subset αs_out') -- | To avoid unused variables when benchmarking unless false do log (prettyP e𝔹_dual)