From 6db70f61afc878fcd80007cd9469752688f9f85a Mon Sep 17 00:00:00 2001 From: Roly Perera Date: Thu, 21 Sep 2023 13:47:04 +0100 Subject: [PATCH] =?UTF-8?q?=F0=9F=A7=A9=20[consolidate]:=20Minor=20tidy=20?= =?UTF-8?q?up.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/EvalGraph.purs | 24 +++++++++++------------- src/GaloisConnection.purs | 2 +- test/Util.purs | 2 +- 3 files changed, 13 insertions(+), 15 deletions(-) diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs index e065f089f..de664bb6f 100644 --- a/src/EvalGraph.purs +++ b/src/EvalGraph.purs @@ -183,16 +183,14 @@ evalWithConfig { g, n, γα } e = pure (eα × vα) graphGC :: forall g. Graph g => GraphConfig g -> Raw Expr -> String + GaloisConnection (Set Vertex) (Set Vertex) -graphGC { g: g0, n, γα } e = - let - Identity q = (runWithGraphAllocT (g0 × n) :: _ -> Identity _) $ do - eα <- alloc e - vα <- eval γα eα S.empty - pure (vα × eα) - in - do - (g × _) × vα × eα <- q - pure $ - { fwd: \αs -> G.vertices (fwdSlice αs g) `intersection` vertices vα - , bwd: \αs -> G.vertices (bwdSlice αs g) `intersection` vertices eα -- needs to include γα - } +graphGC { g: g0, n, γα } e = do + (g × _) × vα × eα <- q + pure $ + { fwd: \αs -> G.vertices (fwdSlice αs g) `intersection` vertices vα + , bwd: \αs -> G.vertices (bwdSlice αs g) `intersection` vertices eα -- needs to include γα + } + where + Identity q = (runWithGraphAllocT (g0 × n) :: _ -> Identity _) $ do + eα <- alloc e + vα <- eval γα eα S.empty + pure (vα × eα) diff --git a/src/GaloisConnection.purs b/src/GaloisConnection.purs index 8229dd613..df981f5a7 100644 --- a/src/GaloisConnection.purs +++ b/src/GaloisConnection.purs @@ -12,7 +12,7 @@ type GaloisConnection a b = } deMorgan :: forall a b. BooleanLattice a => BooleanLattice b => Endo (a -> b) -deMorgan f = neg >>> f >>> neg +deMorgan = (neg >>> _) >>> (_ >>> neg) -- Could unify deMorgan and dual but would need to reify notion of opposite category. dual :: forall a b. BooleanLattice a => BooleanLattice b => GaloisConnection a b -> GaloisConnection b a diff --git a/test/Util.purs b/test/Util.purs index a5583790a..759df25ce 100644 --- a/test/Util.purs +++ b/test/Util.purs @@ -106,7 +106,7 @@ testGraph s gconf { δv, bwd_expect, fwd_expect } = do -- | Eval e <- desug s tEval1 <- preciseTime - (g × _) × (eα × vα) <- evalWithConfig gconf e >>= except + (g × _) × eα × vα <- evalWithConfig gconf e >>= except tEval2 <- preciseTime -- | Backward