diff --git a/src/Desug.purs b/src/Desug.purs index 23d545f44..440d92d76 100644 --- a/src/Desug.purs +++ b/src/Desug.purs @@ -6,8 +6,8 @@ import Control.Monad.Error.Class (class MonadError) import Desugarable (desug, desugBwd) import Effect.Exception (Error) import Expr (Expr) -import GaloisConnection (GaloisConnection) -import Lattice (class BoundedJoinSemilattice, Raw, botOf) +import GaloisConnection (GaloisConnection(..)) +import Lattice (class BoundedJoinSemilattice, Raw) import SExpr (Expr) as S import Util (successful) @@ -19,8 +19,6 @@ desugGC -> m (GaloisConnection (S.Expr a) (Expr a)) desugGC s0 = do let - dom = botOf s0 - codom = botOf $ successful $ desug s0 fwd s = successful $ desug s bwd e = desugBwd e s0 - pure { dom, codom, fwd, bwd } + pure $ GC { fwd, bwd } diff --git a/src/EvalBwd.purs b/src/EvalBwd.purs index 1920573f5..d53ee8b1b 100644 --- a/src/EvalBwd.purs +++ b/src/EvalBwd.purs @@ -20,7 +20,7 @@ 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 GaloisConnection (GaloisConnection(..)) import Lattice (Raw, bot, botOf, expand, (∨)) import Partial.Unsafe (unsafePartial) import Trace (AppTrace(..), Trace(..), VarDef(..)) as T @@ -195,12 +195,15 @@ evalBwd' v (T.LetRec ρ t) = γ1' × ρ' × α' = closeDefsBwd γ2 evalBwd' _ _ = error absurd -traceGC :: forall a m. MonadError Error m => Ann a => Raw Env -> Raw Expr -> m (GaloisConnection (Env a × Expr a × a) (Val a)) +type TracedEval a = + { gc :: GaloisConnection (Env a × Expr a × a) (Val a) + , v :: Raw Val + } + +traceGC :: forall a m. MonadError Error m => Ann a => Raw Env -> Raw Expr -> m (TracedEval a) traceGC γ e = do t × v <- eval γ e bot let - dom = (botOf <$> γ) × botOf e × bot - codom = botOf v bwd v' = evalBwd γ e v' t fwd (γ' × e' × α) = snd $ fromRight $ runExcept $ eval γ' e' α - pure { dom, codom, fwd, bwd } + pure $ { gc: GC { fwd, bwd }, v } diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs index 42aadfa89..a43965ed0 100644 --- a/src/EvalGraph.purs +++ b/src/EvalGraph.purs @@ -23,7 +23,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 GaloisConnection (GaloisConnection(..)) import Graph (class Graph, Vertex, sinks) import Graph (vertices) as G import Graph.GraphWriter (class MonadGraphAlloc, alloc, new, runWithGraphAllocT) @@ -173,13 +173,21 @@ eval_module γ = go D.empty γ'' <- closeDefs (γ <+> γ') ρ αs go (γ' <+> γ'') (Module ds) αs +type GraphEval g = + { gc :: GaloisConnection (Set Vertex) (Set Vertex) + , γα :: Env Vertex + , eα :: Expr Vertex + , g :: g + , vα :: Val Vertex + } + graphGC :: forall g m . MonadError Error m => Graph g => GraphConfig g -> Raw Expr - -> m (GaloisConnection (Set Vertex) (Set Vertex) × Expr Vertex × g × Val Vertex) + -> m (GraphEval g) graphGC { g, n, γα } e = do (g' × _) × eα × vα <- do runWithGraphAllocT (g × n) $ do @@ -188,8 +196,6 @@ graphGC { g, n, γα } e = do pure (eα × vα) let -- TODO: want (vertices eα `union` foldMap vertices γα) rather than sinks g' here? - dom = sinks g' - codom = vertices vα - fwd αs = G.vertices (fwdSlice αs g') `intersection` codom - bwd αs = G.vertices (bwdSlice αs g') `intersection` dom - pure $ { dom, codom, fwd, bwd } × eα × g' × vα + fwd αs = G.vertices (fwdSlice αs g') `intersection` vertices vα + bwd αs = G.vertices (bwdSlice αs g') `intersection` sinks g' + pure { gc: GC { fwd, bwd }, γα, eα, g: g', vα } diff --git a/src/GaloisConnection.purs b/src/GaloisConnection.purs index 170388c41..4852541fb 100644 --- a/src/GaloisConnection.purs +++ b/src/GaloisConnection.purs @@ -1,25 +1,25 @@ module GaloisConnection where import Prelude -import Data.Function (identity) as F + +import Data.Newtype (class Newtype) import Lattice (class BooleanLattice, neg) import Util (Endo) --- a and b are posets, but we don't enforce that here. Use record rather than type class so we can extend with --- explicit value-level representation of domain/codomain. -type GaloisConnection a b = - { dom :: a - , codom :: b - , fwd :: a -> b - , bwd :: b -> a - } +newtype GaloisConnection a b = GC { fwd :: a -> b, bwd :: b -> a } + +derive instance Newtype (GaloisConnection a b) _ deMorgan :: forall a b. BooleanLattice a => BooleanLattice b => Endo (a -> b) 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 -dual gc = gc { dom = gc.codom, codom = gc.dom, fwd = deMorgan gc.bwd, bwd = deMorgan gc.fwd } +dual (GC { fwd, bwd }) = GC { fwd: deMorgan bwd, bwd: deMorgan fwd } + +instance Semigroupoid GaloisConnection where + compose (GC { fwd: fwd1, bwd: bwd1 }) (GC { fwd: fwd2, bwd: bwd2 }) = + GC { fwd: fwd1 <<< fwd2, bwd: bwd1 >>> bwd2 } -identity :: forall a. a -> GaloisConnection a a -identity a = { dom: a, codom: a, fwd: F.identity, bwd: F.identity } +instance Category GaloisConnection where + identity = GC { fwd: identity, bwd: identity } diff --git a/test/Util.purs b/test/Util.purs index 922986c54..3a716319f 100644 --- a/test/Util.purs +++ b/test/Util.purs @@ -22,10 +22,12 @@ import Effect.Class.Console (log) import Effect.Exception (Error) import EvalBwd (traceGC) import EvalGraph (GraphConfig, graphGC) -import Graph (sinks, vertices) +import Graph (sinks) +import Graph (vertices) as G import Graph.GraphImpl (GraphImpl) import Graph.Slice (bwdSliceDual, fwdSliceDual, fwdSliceDeMorgan) as G -import Graph.Slice (selectαs, select𝔹s) +import Graph.Slice (selectαs, select𝔹s, vertices) +import GaloisConnection (GaloisConnection(..)) import Heterogeneous.Mapping (hmap) import Lattice (Raw, botOf, erase) import Module (parse) @@ -66,18 +68,18 @@ testParse s = do testTrace :: Raw SE.Expr -> GraphConfig GraphImpl -> TestConfig -> MayFailT Aff TraceRow testTrace s { γα } { δv, bwd_expect, fwd_expect } = do -- | Desugaring Galois connections for Unit and Boolean type selections - desug <- desugGC s - desug𝔹 <- desugGC s + GC desug <- desugGC s + GC desug𝔹 <- desugGC s -- | Eval let e = desug.fwd s t_eval1 <- preciseTime - eval <- traceGC (erase <$> γα) e + { gc: GC eval, v } <- traceGC (erase <$> γα) e t_eval2 <- preciseTime -- | Backward t_bwd1 <- preciseTime - let γ𝔹 × e𝔹 × _ = eval.bwd (δv (botOf eval.codom)) + let γ𝔹 × e𝔹 × _ = eval.bwd (δv (botOf v)) t_bwd2 <- preciseTime let s𝔹 = desug𝔹.bwd e𝔹 @@ -88,13 +90,13 @@ testTrace s { γα } { δv, bwd_expect, fwd_expect } = do t_fwd2 <- preciseTime lift do - unless (isGraphical eval.codom) $ + unless (isGraphical v) $ log (prettyP v𝔹) -- | Check backward selections unless (null bwd_expect) $ checkPretty "Trace-based source selection" bwd_expect s𝔹 -- | Check round-trip selections - unless (isGraphical eval.codom) $ + unless (isGraphical v) $ checkPretty "Trace-based value" fwd_expect v𝔹 pure { tEval: tdiff t_eval1 t_eval2, tBwd: tdiff t_bwd1 t_bwd2, tFwd: tdiff t_fwd1 t_fwd2 } @@ -102,23 +104,23 @@ testTrace s { γα } { δv, bwd_expect, fwd_expect } = do testGraph :: Raw SE.Expr -> GraphConfig GraphImpl -> TestConfig -> MayFailT Aff GraphRow testGraph s gconfig { δv, bwd_expect, fwd_expect } = do -- | Desugaring Galois connections for Unit and Boolean type selections - gc_desug <- desugGC s - gc_desug𝔹 <- desugGC s + GC desug <- desugGC s + GC desug𝔹 <- desugGC s -- | Eval - let e = gc_desug.fwd s + let e = desug.fwd s t_eval1 <- preciseTime - gc × eα × g × vα <- graphGC gconfig e + { gc: GC eval, eα, g, vα } <- graphGC gconfig e t_eval2 <- preciseTime -- | Backward t_bwd1 <- preciseTime let αs_out = selectαs (δv (botOf vα)) vα - αs_in = gc.bwd αs_out + αs_in = eval.bwd αs_out e𝔹 = select𝔹s eα αs_in t_bwd2 <- preciseTime - let s𝔹 = gc_desug𝔹.bwd e𝔹 + let s𝔹 = desug𝔹.bwd e𝔹 -- | De Morgan dual of backward t_bwdDual1 <- preciseTime @@ -132,13 +134,13 @@ testGraph s gconfig { δv, bwd_expect, fwd_expect } = do -- | Backward (all outputs selected) t_bwdAll1 <- preciseTime let - e𝔹_all = select𝔹s eα $ gc.bwd $ gc.codom + e𝔹_all = select𝔹s eα $ eval.bwd (vertices vα) t_bwdAll2 <- preciseTime -- | Forward (round-tripping) t_fwd1 <- preciseTime let - αs_out' = gc.fwd αs_in + αs_out' = eval.fwd αs_in v𝔹 = select𝔹s vα αs_out' t_fwd2 <- preciseTime @@ -146,14 +148,14 @@ testGraph s gconfig { δv, bwd_expect, fwd_expect } = do t_fwdDual1 <- preciseTime let gfwd_dual = G.fwdSliceDual αs_in g - v𝔹_dual = select𝔹s vα (vertices gfwd_dual) + v𝔹_dual = select𝔹s vα (G.vertices gfwd_dual) t_fwdDual2 <- preciseTime -- | Forward (round-tripping) using De Morgan dual t_fwdAsDeMorgan1 <- preciseTime let gfwd_demorgan = G.fwdSliceDeMorgan αs_in g - v𝔹_demorgan = select𝔹s vα (vertices gfwd_demorgan) <#> not + v𝔹_demorgan = select𝔹s vα (G.vertices gfwd_demorgan) <#> not t_fwdAsDeMorgan2 <- preciseTime lift do