Skip to content

Commit

Permalink
Better naming/documentation of slicing functions again
Browse files Browse the repository at this point in the history
  • Loading branch information
Minh Nguyen committed Oct 31, 2023
1 parent c3907c5 commit 88d8045
Show file tree
Hide file tree
Showing 3 changed files with 19 additions and 17 deletions.
22 changes: 12 additions & 10 deletions src/Graph/Slice.purs
Original file line number Diff line number Diff line change
Expand Up @@ -28,8 +28,8 @@ bwdSlice αs0 g0 = fst $ runWithGraph $ tailRecM go (empty × L.fromFoldable αs
pure $ Loop ((visited # insert α) × (L.fromFoldable βs <> αs))

-- | 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)
bwdSliceDualAsFwdOp :: forall g. Graph g => Set Vertex -> g -> g
bwdSliceDualAsFwdOp αs0 g0 = fwdSlice αs0 (op g0)

-- | Forward slicing (▷_G)
fwdSlice :: forall g. Graph g => Set Vertex -> g -> g
Expand All @@ -45,15 +45,17 @@ fwdSlice αs0 g0 = fst $ runWithGraph $ tailRecM go (M.empty × inEdges g0 αs0)
else
pure $ Loop (M.insert α βs h × es)

-- | De Morgan dual of forward slicing (▷_G)° ≡ Backward slicing on the opposite graph (◁_{G_op})
fwdSliceDualAsBwdOp :: forall g. Graph g => Set Vertex -> g -> g
fwdSliceDualAsBwdOp αs0 g0 = bwdSlice αs0 (op g0)

fwdSliceDual :: forall g. Graph g => Set Vertex -> g -> g
fwdSliceDual αs0 g0 = fwdSlice (sinks g0 `difference` αs0) g0

-- | Forward slicing (▷_G) ≡ De Morgan dual of backward slicing on the opposite graph (◁_{G_op})°
-- Doesn't do the final negation..
-- Also doesn't do the final negation..
fwdSliceAsDeMorgan :: forall g. Graph g => Set Vertex -> g -> g
fwdSliceAsDeMorgan αs0 g0 =
bwdSlice (sinks g0 `difference` αs0) (op g0)

-- | De Morgan dual of forward slicing (▷_G)°
-- Doesn't do the final negation..
fwdSliceDual :: forall g. Graph g => Set Vertex -> g -> g
fwdSliceDual αs0 g0 = fwdSlice (sinks g0 `difference` αs0) g0

-- | De Morgan dual of forward slicing (▷_G)° ≡ Backward slicing on the opposite graph (◁_{G_op})
fwdSliceDualAsBwdOp :: forall g. Graph g => Set Vertex -> g -> g
fwdSliceDualAsBwdOp αs0 g0 = bwdSlice αs0 (op g0)
2 changes: 1 addition & 1 deletion test/Benchmark/Main.purs
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ import Util (type (×), definitely, (×))
main :: Effect Unit
main = launchAff_ do
let
iter = 10
iter = 1
arr = concat ([ bench_misc, bench_desugaring, bench_bwd, bench_graphics ] <#> ((#) (iter × true)))
outs <- sequence $ (\(str × row) -> (str × _) <$> row) <$> arr
logShow $ BenchAcc $ definitely "More than one benchmark" $ fromArray outs
Expand Down
12 changes: 6 additions & 6 deletions test/Util.purs
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ import Expr (ProgCxt)
import GaloisConnection (GaloisConnection(..))
import Graph (Vertex, selectαs, select𝔹s, sinks, vertices)
import Graph.GraphImpl (GraphImpl)
import Graph.Slice (bwdSliceDual, fwdSliceDualAsBwdOp, fwdSliceAsDeMorgan) as G
import Graph.Slice (bwdSliceDualAsFwdOp, fwdSliceDualAsBwdOp, fwdSliceAsDeMorgan) as G
import Lattice (Raw, 𝔹, botOf, erase, topOf)
import Module (File, initialConfig, open, parse)
import Parse (program)
Expand Down Expand Up @@ -144,18 +144,18 @@ testGraph s gconfig spec@{ δv } benchmarking = do
when benchmarking do
do
let αs = selectαs (δv (botOf vα)) vα
g' <- benchmark (method <> "-BwdDual") $ \_ -> pure (G.bwdSliceDual αs g)
when logging (logAs "BwdDual/input slice" (prettyP $ select𝔹s eα (sinks g')))
g' <- benchmark (method <> "-BwdDualAsFwdOp") $ \_ -> pure (G.bwdSliceDualAsFwdOp αs g)
when logging (logAs "BwdDualAsFwdOp/input slice" (prettyP $ select𝔹s eα (sinks g')))

do
let αs = vertices vα
αs' <- benchmark (method <> "-BwdAll") $ \_ -> pure (eval.bwd αs)
when logging (logAs "BwdAll/input slice" (prettyP $ select𝔹s eα αs'))

do
g' <- benchmark (method <> "-FwdDual") $ \_ -> pure (G.fwdSliceDualAsBwdOp αs_in g)
-- g'' <- benchmark (method <> "-FwdDual2") $ \_ -> pure (G.fwdDual αs_in g)
when logging (logAs "FwdDual/output slice" (prettyP $ select𝔹s vα (vertices g')))
g' <- benchmark (method <> "-FwdDualAsBwdOp") $ \_ -> pure (G.fwdSliceDualAsBwdOp αs_in g)
-- g'' <- benchmark (method <> "-FwdDual2") $ \_ -> pure (G.fwdSliceDual αs_in g)
when logging (logAs "FwdDualAsBwdOp/output slice" (prettyP $ select𝔹s vα (vertices g')))
-- when logging (logAs "FwdDual2/output slice" (prettyP $ select𝔹s vα (vertices g'') <#> not))
do
g' <- benchmark (method <> "-FwdAsDeMorgan") $ \_ -> pure (G.fwdSliceAsDeMorgan αs_in g)
Expand Down

0 comments on commit 88d8045

Please sign in to comment.