Benchmarking

[min-nguyen]

I've gone for something like this for the graph-based EvalGaloisConnection, where we abstract away the concrete vα and eα terms into functions that directly operate on them.

type EvalGaloisConnection g a b = GaloisConnection a b
   ( selecte𝔹 :: a -> Expr 𝔹
   , selectv𝔹 :: b -> Val 𝔹
   , runδv :: (Val 𝔹 -> Val 𝔹) -> b
   , g :: 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α
      bwd αs = G.vertices (bwdSlice αs g') `intersection` sinks g'
   pure { selecte𝔹, selectv𝔹, runδv, g: g', fwd, bwd }

This removes some repeated references to vα and eα in Test.Util. You can now also write something like:

  e <- desug s
  gc <- graphGC gconfig e

  let e𝔹_all = (gc.selecte𝔹 <<< gc.bwd <<< gc.runδv) topOf

I'm afraid we can't always write things compositionally like this though (sometimes we want the intermediate results, like αs_out). What are your thoughts?