{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}

-- | Supports writing 'Set algebra' expressions, using overloaded set operations, that can
--   be applied to a variety of Basic types (Set, List, Map, etc). Also supports
--   a mechanism to evaluate them efficiently, choosing datatype specific algorithms.
--   This mechanism uses run-time rewrite rules to get the best algorithm. If there are
--   no rewrite rules for a specific expression, falls back to a less efficient generic algorithm.
module Control.Iterate.SetAlgebra where

import Control.Iterate.BaseTypes (
  BaseRep (..),
  Basic (..),
  Embed (..),
  Iter (..),
  Sett (..),
  Single (..),
  fromPairs,
 )
import Control.Iterate.Collect (Collect, front, one, rear, runCollect, when)
import Control.Iterate.Exp (
  Exp (..),
  Query (..),
  -- semantic meaning functions for Query

  andD,
  andPD,
  chainD,
  -- Operations on Fun

  constant,
  first,
  nEgate,
  plus,
  projD,
  rngElem,
  rngFst,
  rngSnd,
  second,
 )
import qualified Data.Map.Strict as Map
import Data.MapExtras (
  disjointMapSetFold,
  intersectDomP,
  intersectDomPLeft,
  intersectMapSetFold,
  keysEqual,
  noKeys,
 )
import qualified Data.Set as Set
import Prelude hiding (lookup)

-- ===============================================================================

-- | Compile the (Exp (f k v)) to a Query iterator, and a BaseRep that indicates
--   how to materialize the iterator to the correct type. Recall the iterator
--   can be used to constuct many things using runCollect, but here we want
--   to materialize it to the same type as the (Exp (f k v)), i.e. (f k v).
compile :: Exp (f k v) -> (Query k v, BaseRep f k v)
compile :: forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile (Base BaseRep f k v
rep f k v
relation) = (forall (k :: * -> * -> *) k v.
(Iter k, Ord k) =>
BaseRep k k v -> k k v -> Query k v
BaseD BaseRep f k v
rep f k v
relation, BaseRep f k v
rep)
compile (Singleton k
d v
r) = (forall (k :: * -> * -> *) k v.
(Iter k, Ord k) =>
BaseRep k k v -> k k v -> Query k v
BaseD forall k v. Basic Single => BaseRep Single k v
SingleR (forall k v. k -> v -> Single k v
Single k
d v
r), forall k v. Basic Single => BaseRep Single k v
SingleR)
compile (SetSingleton k
d) = (forall (k :: * -> * -> *) k v.
(Iter k, Ord k) =>
BaseRep k k v -> k k v -> Query k v
BaseD forall k v. Basic Single => BaseRep Single k v
SingleR (forall k. k -> Single k ()
SetSingle k
d), forall k v. Basic Single => BaseRep Single k v
SingleR)
compile (Dom (Base BaseRep f k v
SetR f k v
rel)) = (forall (k :: * -> * -> *) k v.
(Iter k, Ord k) =>
BaseRep k k v -> k k v -> Query k v
BaseD forall k. Basic Sett => BaseRep Sett k ()
SetR f k v
rel, forall k. Basic Sett => BaseRep Sett k ()
SetR)
compile (Dom (Singleton k
k v
_v)) = (forall (k :: * -> * -> *) k v.
(Iter k, Ord k) =>
BaseRep k k v -> k k v -> Query k v
BaseD forall k. Basic Sett => BaseRep Sett k ()
SetR (forall k. Set k -> Sett k ()
Sett (forall a. a -> Set a
Set.singleton k
k)), forall k. Basic Sett => BaseRep Sett k ()
SetR)
compile (Dom (SetSingleton k
k)) = (forall (k :: * -> * -> *) k v.
(Iter k, Ord k) =>
BaseRep k k v -> k k v -> Query k v
BaseD forall k. Basic Sett => BaseRep Sett k ()
SetR (forall k. Set k -> Sett k ()
Sett (forall a. a -> Set a
Set.singleton k
k)), forall k. Basic Sett => BaseRep Sett k ()
SetR)
compile (Dom Exp (f k v)
x) = (forall k v u. Ord k => Query k v -> Fun (k -> v -> u) -> Query k u
projD (forall a b. (a, b) -> a
fst (forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (f k v)
x)) (forall c a b. Show c => c -> Fun (a -> b -> c)
constant ()), forall k. Basic Sett => BaseRep Sett k ()
SetR)
compile (Rng (Base BaseRep f k v
SetR f k v
_rel)) = (forall (k :: * -> * -> *) k v.
(Iter k, Ord k) =>
BaseRep k k v -> k k v -> Query k v
BaseD forall k. Basic Sett => BaseRep Sett k ()
SetR (forall k. Set k -> Sett k ()
Sett (forall a. a -> Set a
Set.singleton ())), forall k. Basic Sett => BaseRep Sett k ()
SetR)
compile (Rng (Singleton k
_k v
v)) = (forall (k :: * -> * -> *) k v.
(Iter k, Ord k) =>
BaseRep k k v -> k k v -> Query k v
BaseD forall k. Basic Sett => BaseRep Sett k ()
SetR (forall k. Set k -> Sett k ()
Sett (forall a. a -> Set a
Set.singleton v
v)), forall k. Basic Sett => BaseRep Sett k ()
SetR)
compile (Rng (SetSingleton k
_k)) = (forall (k :: * -> * -> *) k v.
(Iter k, Ord k) =>
BaseRep k k v -> k k v -> Query k v
BaseD forall k. Basic Sett => BaseRep Sett k ()
SetR (forall k. Set k -> Sett k ()
Sett (forall a. a -> Set a
Set.singleton ())), forall k. Basic Sett => BaseRep Sett k ()
SetR)
compile (Rng Exp (f k v)
f) = (forall (k :: * -> * -> *) k v.
(Iter k, Ord k) =>
BaseRep k k v -> k k v -> Query k v
BaseD forall k. Basic Sett => BaseRep Sett k ()
SetR (forall k (f :: * -> * -> *) v.
Ord k =>
BaseRep f k v -> Collect (k, v) -> f k v
materialize forall k. Basic Sett => BaseRep Sett k ()
SetR (forall {f :: * -> * -> *} {a} {a}.
Iter f =>
f a a -> Collect (a, ())
loop Query k v
query)), forall k. Basic Sett => BaseRep Sett k ()
SetR) -- We really ought to memoize this. It might be computed many times.
  where
    query :: Query k v
query = forall a b. (a, b) -> a
fst (forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (f k v)
f)
    loop :: f a a -> Collect (a, ())
loop f a a
x = do (a
_k, a
v, f a a
x2) <- forall (f :: * -> * -> *) a b.
Iter f =>
f a b -> Collect (a, b, f a b)
nxt f a a
x; forall t. t -> Collect t -> Collect t
front (a
v, ()) (f a a -> Collect (a, ())
loop f a a
x2)
compile (DRestrict Exp (g k ())
set Exp (f k v)
rel) = (forall k v u. Ord k => Query k v -> Fun (k -> v -> u) -> Query k u
projD (forall k v1 v2.
Ord k =>
Query k v1 -> Query k v2 -> Query k (v1, v2)
andD (forall a b. (a, b) -> a
fst (forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (g k ())
set)) Query k v
reld) forall x a b. Fun (x -> (a, b) -> b)
rngSnd, BaseRep f k v
rep)
  where
    (Query k v
reld, BaseRep f k v
rep) = forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (f k v)
rel
compile (DExclude Exp (g k ())
set Exp (f k v)
rel) = (forall k v k. Ord k => Query k v -> Query k k -> Query k v
DiffD Query k v
reld (forall a b. (a, b) -> a
fst (forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (g k ())
set)), BaseRep f k v
rep)
  where
    (Query k v
reld, BaseRep f k v
rep) = forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (f k v)
rel
compile (RRestrict Exp (f k v)
rel Exp (g v ())
set) =
  case (forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (f k v)
rel, forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (g v ())
set) of
    ((Query k v
reld, BaseRep f k v
rep), (BaseD BaseRep f v ()
_ f v ()
x, BaseRep g v ()
_)) -> (forall k v. Ord k => Query k v -> Fun (k -> v -> Bool) -> Query k v
GuardD Query k v
reld (forall rng (f :: * -> * -> *) v dom.
(Ord rng, Iter f) =>
f rng v -> Fun (dom -> rng -> Bool)
rngElem f v ()
x), BaseRep f k v
rep)
    ((Query k v
reld, BaseRep f k v
rep), (Query v ()
setd, BaseRep g v ()
_)) -> (forall k v w u.
(Ord k, Ord v) =>
Query k v -> Query v w -> Fun (k -> (v, w) -> u) -> Query k u
chainD Query k v
reld Query v ()
setd forall x a b. Fun (x -> (a, b) -> a)
rngFst, BaseRep f k v
rep)
compile (RExclude Exp (f k v)
rel Exp (g v ())
set) =
  case (forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (f k v)
rel, forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (g v ())
set) of
    ((Query k v
reld, BaseRep f k v
rep), (BaseD BaseRep f v ()
_ f v ()
x, BaseRep g v ()
_)) -> (forall k v. Ord k => Query k v -> Fun (k -> v -> Bool) -> Query k v
GuardD Query k v
reld (forall k v. Fun (k -> v -> Bool) -> Fun (k -> v -> Bool)
nEgate (forall rng (f :: * -> * -> *) v dom.
(Ord rng, Iter f) =>
f rng v -> Fun (dom -> rng -> Bool)
rngElem f v ()
x)), BaseRep f k v
rep)
    ((Query k v
reld, BaseRep f k v
rep), (Query v (), BaseRep g v ())
_) -> (forall k v. Ord k => Query k v -> Fun (k -> v -> Bool) -> Query k v
GuardD Query k v
reld (forall k v. Fun (k -> v -> Bool) -> Fun (k -> v -> Bool)
nEgate (forall rng (f :: * -> * -> *) v dom.
(Ord rng, Iter f) =>
f rng v -> Fun (dom -> rng -> Bool)
rngElem (forall t. Exp t -> t
compute Exp (g v ())
set))), BaseRep f k v
rep) -- This could be expensive
compile (UnionOverrideLeft Exp (f k v)
rel1 Exp (g k v)
rel2) = (forall k v.
Ord k =>
Query k v -> Query k v -> Fun (v -> v -> v) -> Query k v
OrD Query k v
rel1d (forall a b. (a, b) -> a
fst (forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (g k v)
rel2)) forall v s. Fun (v -> s -> v)
first, BaseRep f k v
rep) -- first uses value from rel1 to override value from rel2
  where
    (Query k v
rel1d, BaseRep f k v
rep) = forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (f k v)
rel1
compile (UnionOverrideRight Exp (f k v)
rel1 Exp (g k v)
rel2) = (forall k v.
Ord k =>
Query k v -> Query k v -> Fun (v -> v -> v) -> Query k v
OrD Query k v
rel1d (forall a b. (a, b) -> a
fst (forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (g k v)
rel2)) forall v s. Fun (v -> s -> s)
second, BaseRep f k v
rep) -- second uses value from rel2 to override value from rel1
  where
    (Query k v
rel1d, BaseRep f k v
rep) = forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (f k v)
rel1
compile (UnionPlus Exp (f k n)
rel1 Exp (g k n)
rel2) = (forall k v.
Ord k =>
Query k v -> Query k v -> Fun (v -> v -> v) -> Query k v
OrD Query k n
rel1d (forall a b. (a, b) -> a
fst (forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (g k n)
rel2)) forall t. Monoid t => Fun (t -> t -> t)
plus, BaseRep f k n
rep)
  where
    (Query k n
rel1d, BaseRep f k n
rep) = forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (f k n)
rel1
compile (Intersect Exp (f k v)
rel1 Exp (g k u)
rel2) = (forall k v1 u v.
Ord k =>
Query k v1 -> Query k u -> Fun (k -> (v1, u) -> v) -> Query k v
andPD (forall a b. (a, b) -> a
fst (forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (f k v)
rel1)) (forall a b. (a, b) -> a
fst (forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (g k u)
rel2)) (forall c a b. Show c => c -> Fun (a -> b -> c)
constant ()), forall k. Basic Sett => BaseRep Sett k ()
SetR)
compile (SetDiff Exp (f k v)
rel1 Exp (g k u)
rel2) = (forall k v k. Ord k => Query k v -> Query k k -> Query k v
DiffD Query k v
rel1d (forall a b. (a, b) -> a
fst (forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (g k u)
rel2)), BaseRep f k v
rep)
  where
    (Query k v
rel1d, BaseRep f k v
rep) = forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (f k v)
rel1

compileSubterm :: Exp a -> Exp (f k v) -> Query k v
compileSubterm :: forall a (f :: * -> * -> *) k v. Exp a -> Exp (f k v) -> Query k v
compileSubterm Exp a
_whole Exp (f k v)
sub = forall a b. (a, b) -> a
fst (forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (f k v)
sub)

-- ===========================================================================
-- The second part of the generic algorithm is to run the compiled code.
-- This involves materiaizing every sub-expression, and then applying generic
-- operations to the sub-expressions to get the answer.  Some Exp's (ones built
-- with (Base baserep value) are aready materialized, so they only need be
-- transformed to the target type. If the target type, is the same type as the real
-- 'value' stored in (Base baserep value). Then this is a no-op, if not use the
-- function (materialize :: Ord k => BaseRep f k v -> Collect (k, v) -> f k v) to
-- convert it.
-- ===========================================================================

run :: Ord k => (Query k v, BaseRep f k v) -> f k v
run :: forall k v (f :: * -> * -> *).
Ord k =>
(Query k v, BaseRep f k v) -> f k v
run (BaseD BaseRep f k v
SetR f k v
x, BaseRep f k v
SetR) = f k v
x -- If it is already data (BaseD)
run (BaseD BaseRep f k v
MapR f k v
x, BaseRep f k v
MapR) = f k v
x -- and in the right form (the BaseRep's match)
run (BaseD BaseRep f k v
SingleR f k v
x, BaseRep f k v
SingleR) = f k v
x -- just return the data
run (BaseD BaseRep f k v
ListR f k v
x, BaseRep f k v
ListR) = f k v
x -- if the forms do not match.
run (BaseD BaseRep f k v
_source f k v
x, BaseRep f k v
ListR) = forall k (f :: * -> * -> *) v.
Ord k =>
BaseRep f k v -> Collect (k, v) -> f k v
materialize forall k v. Basic List => BaseRep List k v
ListR (forall (f :: * -> * -> *) k v. Iter f => f k v -> Collect (k, v)
fifo f k v
x) -- use fifo, since the order matters for Lists.
run (BaseD BaseRep f k v
_source f k v
x, BaseRep f k v
target) = forall k (f :: * -> * -> *) v.
Ord k =>
BaseRep f k v -> Collect (k, v) -> f k v
materialize BaseRep f k v
target (forall (f :: * -> * -> *) k v. Iter f => f k v -> Collect (k, v)
lifo f k v
x) -- use lifo, for others
run (Query k v
other, BaseRep f k v
ListR) = forall k (f :: * -> * -> *) v.
Ord k =>
BaseRep f k v -> Collect (k, v) -> f k v
materialize forall k v. Basic List => BaseRep List k v
ListR (forall (f :: * -> * -> *) k v. Iter f => f k v -> Collect (k, v)
fifo Query k v
other) -- If it is a compound Iterator, for List, than materialize it using fifo
run (Query k v
other, BaseRep f k v
target) = forall k (f :: * -> * -> *) v.
Ord k =>
BaseRep f k v -> Collect (k, v) -> f k v
materialize BaseRep f k v
target (forall (f :: * -> * -> *) k v. Iter f => f k v -> Collect (k, v)
lifo Query k v
other) -- If it is a compund Iterator, for anything else than materialize it using lifo

testing :: Bool
testing :: Bool
testing = Bool
False

runBoolExp :: Exp Bool -> Bool
runBoolExp :: Exp Bool -> Bool
runBoolExp Exp Bool
e =
  if Bool
testing
    then forall a. HasCallStack => [Char] -> a
error ([Char]
"In Testing mode, SetAlgebra expression: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Exp Bool
e forall a. [a] -> [a] -> [a]
++ [Char]
" falls through to slow mode.")
    else Exp Bool -> Bool
runBool Exp Bool
e

runSetExp :: Ord k => Exp (f k v) -> f k v
runSetExp :: forall k (f :: * -> * -> *) v. Ord k => Exp (f k v) -> f k v
runSetExp Exp (f k v)
e =
  if Bool
testing
    then forall a. HasCallStack => [Char] -> a
error ([Char]
"In Testing mode, SetAlgebra expression: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Exp (f k v)
e forall a. [a] -> [a] -> [a]
++ [Char]
" falls through to slow mode.")
    else forall k v (f :: * -> * -> *).
Ord k =>
(Query k v, BaseRep f k v) -> f k v
run (forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (f k v)
e)

-- The following ar only for use in the SetAlgebra internal tests

runSet :: Ord k => Exp (f k v) -> f k v
runSet :: forall k (f :: * -> * -> *) v. Ord k => Exp (f k v) -> f k v
runSet Exp (f k v)
e = forall k v (f :: * -> * -> *).
Ord k =>
(Query k v, BaseRep f k v) -> f k v
run (forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (f k v)
e)

runBool :: Exp Bool -> Bool
runBool :: Exp Bool -> Bool
runBool (Elem k
k Exp (g k ())
v) = forall (f :: * -> * -> *) key b.
(Iter f, Ord key) =>
key -> f key b -> Bool
haskey k
k (forall t. Exp t -> t
compute Exp (g k ())
v)
runBool (NotElem k
k Exp (g k ())
set) = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (f :: * -> * -> *) key b.
(Iter f, Ord key) =>
key -> f key b -> Bool
haskey k
k (forall t. Exp t -> t
compute Exp (g k ())
set)
runBool (w :: Exp Bool
w@(KeyEqual Exp (f k v)
x Exp (g k u)
y)) = forall k (f :: * -> * -> *) (g :: * -> * -> *) b c.
(Ord k, Iter f, Iter g) =>
f k b -> g k c -> Bool
sameDomain (forall a (f :: * -> * -> *) k v. Exp a -> Exp (f k v) -> Query k v
compileSubterm Exp Bool
w Exp (f k v)
x) (forall a (f :: * -> * -> *) k v. Exp a -> Exp (f k v) -> Query k v
compileSubterm Exp Bool
w Exp (g k u)
y)
runBool (w :: Exp Bool
w@(Subset Exp (f k v)
x Exp (g k u)
y)) = forall tuple.
Collect tuple -> forall ans. ans -> (tuple -> ans -> ans) -> ans
runCollect (forall (f :: * -> * -> *) k v. Iter f => f k v -> Collect (k, v)
lifo Query k v
left) Bool
True (\(k
k, v
_v) Bool
ans -> forall (f :: * -> * -> *) key b.
(Iter f, Ord key) =>
key -> f key b -> Bool
haskey k
k Query k u
right Bool -> Bool -> Bool
&& Bool
ans)
  where
    left :: Query k v
left = forall a (f :: * -> * -> *) k v. Exp a -> Exp (f k v) -> Query k v
compileSubterm Exp Bool
w Exp (f k v)
x
    right :: Query k u
right = forall a (f :: * -> * -> *) k v. Exp a -> Exp (f k v) -> Query k v
compileSubterm Exp Bool
w Exp (g k u)
y

-- | cost O(min (size m) (size n) * log(max (size m) (size n))), BUT the constants are high, too slow except for small maps.
sameDomain :: (Ord k, Iter f, Iter g) => f k b -> g k c -> Bool
sameDomain :: forall k (f :: * -> * -> *) (g :: * -> * -> *) b c.
(Ord k, Iter f, Iter g) =>
f k b -> g k c -> Bool
sameDomain f k b
m g k c
n = forall {a} {f :: * -> * -> *} {f :: * -> * -> *} {b} {b}.
(Ord a, Iter f, Iter f) =>
Maybe (a, b, f a b) -> Maybe (a, b, f a b) -> Bool
loop (forall (f :: * -> * -> *) a b.
Iter f =>
f a b -> Maybe (a, b, f a b)
hasNxt f k b
m) (forall (f :: * -> * -> *) a b.
Iter f =>
f a b -> Maybe (a, b, f a b)
hasNxt g k c
n)
  where
    loop :: Maybe (a, b, f a b) -> Maybe (a, b, f a b) -> Bool
loop (Just (a
k1, b
_, f a b
nextm)) (Just (a
k2, b
_, f a b
nextn)) =
      case forall a. Ord a => a -> a -> Ordering
compare a
k1 a
k2 of
        Ordering
EQ -> Maybe (a, b, f a b) -> Maybe (a, b, f a b) -> Bool
loop (forall (f :: * -> * -> *) a b.
Iter f =>
f a b -> Maybe (a, b, f a b)
hasNxt f a b
nextm) (forall (f :: * -> * -> *) a b.
Iter f =>
f a b -> Maybe (a, b, f a b)
hasNxt f a b
nextn)
        Ordering
LT -> Bool
False
        Ordering
GT -> Bool
False
    loop Maybe (a, b, f a b)
Nothing Maybe (a, b, f a b)
Nothing = Bool
True
    loop Maybe (a, b, f a b)
_ Maybe (a, b, f a b)
_ = Bool
False

-- ==============================================================================================
-- The faster strategy involves applying (type-specific) rewrite rules using the
-- function (compute :: Exp t -> t), This pattern matches against the GADT constructors
-- so this allows runtime choice of type specific algortihms of Exp
-- Evaluate an (Exp t) into real data of type t. Try domain and type specific algorithms first,
-- and if those fail. Compile the formula as an iterator, then run the iterator to get an answer.
-- Here are some sample of the type specific algorithms we incorporate
--  x  ∈ (dom y)            haskey
--  x  ∉ (dom y)            not . haskey
-- x ∪ (singleton y)        addpair
-- (Set.singleton x) ⋪ y    removekey
-- (dom x) ⊆ (dom y)
-- ===============================================================================================

compute :: Exp t -> t
compute :: forall t. Exp t -> t
compute (Base BaseRep f k v
_rep f k v
relation) = f k v
relation
compute (Dom (Base BaseRep f k v
SetR f k v
rel)) = f k v
rel
compute (Dom (Base BaseRep f k v
MapR f k v
x)) = forall k. Set k -> Sett k ()
Sett (forall k a. Map k a -> Set k
Map.keysSet f k v
x)
compute (Dom (Singleton k
k v
_v)) = forall k. Set k -> Sett k ()
Sett (forall a. a -> Set a
Set.singleton k
k)
compute (Dom (SetSingleton k
k)) = forall k. Set k -> Sett k ()
Sett (forall a. a -> Set a
Set.singleton k
k)
compute (Dom (Base BaseRep f k v
_rep f k v
rel)) = forall k. Set k -> Sett k ()
Sett (forall (f :: * -> * -> *) k v. (Basic f, Ord k) => f k v -> Set k
domain f k v
rel)
-- (dom (Map(62)? ▷ (setSingleton _ )))
compute (Dom (RRestrict (Base BaseRep f k v
MapR f k v
xs) (SetSingleton k
v))) = forall k. Set k -> Sett k ()
Sett (forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' Set k -> k -> k -> Set k
accum forall a. Set a
Set.empty f k v
xs)
  where
    accum :: Set k -> k -> k -> Set k
accum Set k
ans k
k k
u = if k
u forall a. Eq a => a -> a -> Bool
== k
v then forall a. Ord a => a -> Set a -> Set a
Set.insert k
k Set k
ans else Set k
ans
compute (Dom (RRestrict (Base BaseRep f k v
MapR f k v
xs) (Base BaseRep f k v
SetR (Sett Set k
set)))) = forall k. Set k -> Sett k ()
Sett (forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' Set k -> k -> k -> Set k
accum forall a. Set a
Set.empty f k v
xs)
  where
    accum :: Set k -> k -> k -> Set k
accum Set k
ans k
k k
u = if forall a. Ord a => a -> Set a -> Bool
Set.member k
u Set k
set then forall a. Ord a => a -> Set a -> Set a
Set.insert k
k Set k
ans else Set k
ans
compute (Dom (RExclude (Base BaseRep f k v
MapR f k v
xs) (SetSingleton k
v))) = forall k. Set k -> Sett k ()
Sett (forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' Set k -> k -> k -> Set k
accum forall a. Set a
Set.empty f k v
xs)
  where
    accum :: Set k -> k -> k -> Set k
accum Set k
ans k
k k
u = if Bool -> Bool
not (k
u forall a. Eq a => a -> a -> Bool
== k
v) then forall a. Ord a => a -> Set a -> Set a
Set.insert k
k Set k
ans else Set k
ans
compute (Dom (RExclude (Base BaseRep f k v
MapR f k v
xs) (Base BaseRep f k v
SetR (Sett Set k
set)))) = forall k. Set k -> Sett k ()
Sett (forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' Set k -> k -> k -> Set k
accum forall a. Set a
Set.empty f k v
xs)
  where
    accum :: Set k -> k -> k -> Set k
accum Set k
ans k
k k
u = if Bool -> Bool
not (forall a. Ord a => a -> Set a -> Bool
Set.member k
u Set k
set) then forall a. Ord a => a -> Set a -> Set a
Set.insert k
k Set k
ans else Set k
ans
compute (Dom (DRestrict (SetSingleton k
v) (Base BaseRep f k v
MapR f k v
xs))) = forall k. Set k -> Sett k ()
Sett (forall k v ans.
Ord k =>
(k -> v -> ans -> ans) -> Map k v -> Set k -> ans -> ans
intersectMapSetFold forall {a} {p}. Ord a => a -> p -> Set a -> Set a
accum f k v
xs (forall a. a -> Set a
Set.singleton k
v) forall a. Set a
Set.empty)
  where
    accum :: a -> p -> Set a -> Set a
accum a
k p
_u Set a
ans = forall a. Ord a => a -> Set a -> Set a
Set.insert a
k Set a
ans
compute (Dom (DRestrict (Base BaseRep f k v
SetR (Sett Set k
set)) (Base BaseRep f k v
MapR f k v
xs))) = forall k. Set k -> Sett k ()
Sett (forall k v ans.
Ord k =>
(k -> v -> ans -> ans) -> Map k v -> Set k -> ans -> ans
intersectMapSetFold forall {a} {p}. Ord a => a -> p -> Set a -> Set a
accum f k v
xs Set k
set forall a. Set a
Set.empty)
  where
    accum :: a -> p -> Set a -> Set a
accum a
k p
_u Set a
ans = forall a. Ord a => a -> Set a -> Set a
Set.insert a
k Set a
ans
compute (Dom (DExclude (SetSingleton k
v) (Base BaseRep f k v
MapR f k v
xs))) = forall k. Set k -> Sett k ()
Sett (forall k v ans.
Ord k =>
(k -> v -> ans -> ans) -> Map k v -> Set k -> ans -> ans
disjointMapSetFold forall {a} {p}. Ord a => a -> p -> Set a -> Set a
accum f k v
xs (forall a. a -> Set a
Set.singleton k
v) forall a. Set a
Set.empty)
  where
    accum :: a -> p -> Set a -> Set a
accum a
k p
_u Set a
ans = forall a. Ord a => a -> Set a -> Set a
Set.insert a
k Set a
ans
compute (Dom (DExclude (Base BaseRep f k v
SetR (Sett Set k
set)) (Base BaseRep f k v
MapR f k v
xs))) = forall k. Set k -> Sett k ()
Sett (forall k v ans.
Ord k =>
(k -> v -> ans -> ans) -> Map k v -> Set k -> ans -> ans
disjointMapSetFold forall {a} {p}. Ord a => a -> p -> Set a -> Set a
accum f k v
xs Set k
set forall a. Set a
Set.empty)
  where
    accum :: a -> p -> Set a -> Set a
accum a
k p
_u Set a
ans = forall a. Ord a => a -> Set a -> Set a
Set.insert a
k Set a
ans
compute (Rng (Base BaseRep f k v
SetR f k v
_rel)) = forall k. Set k -> Sett k ()
Sett (forall a. a -> Set a
Set.singleton ())
compute (Rng (Singleton k
_k v
v)) = forall k. Set k -> Sett k ()
Sett (forall a. a -> Set a
Set.singleton v
v)
compute (Rng (SetSingleton k
_k)) = forall k. Set k -> Sett k ()
Sett (forall a. a -> Set a
Set.singleton ())
compute (Rng (Base BaseRep f k v
_rep f k v
rel)) = forall k. Set k -> Sett k ()
Sett (forall (f :: * -> * -> *) v k. (Basic f, Ord v) => f k v -> Set v
range f k v
rel)
compute (DRestrict (Base BaseRep f k v
SetR (Sett Set k
set)) (Base BaseRep f k v
MapR f k v
m)) = forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys f k v
m Set k
set
compute (DRestrict (SetSingleton k
k) (Base BaseRep f k v
MapR f k v
m)) = forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys f k v
m (forall a. a -> Set a
Set.singleton k
k)
compute (DRestrict (Singleton k
k v
_v) (Base BaseRep f k v
MapR f k v
m)) = forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys f k v
m (forall a. a -> Set a
Set.singleton k
k)
compute (DRestrict (Dom (Base BaseRep f k v
MapR f k v
x)) (Base BaseRep f k v
MapR f k v
y)) = forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection f k v
y f k v
x
-- This case inspired by set expression in EpochBoundary.hs
-- (dom (delegs ▷ Set.singleton hk) ◁ stake) in EpochBoundart.hs
-- ((dom (Map(62)? ▷ (setSingleton _ ))) ◁ Map(63)?) which has this structure
-- materialize MapR (do { (x,y,z) <- delegs `domEq` stake; when (y==hk); one(x,z) })
compute (DRestrict (Dom (RRestrict (Base BaseRep f k v
MapR f k v
delegs) (SetSingleton k
hk))) (Base BaseRep f k v
MapR f k v
stake)) =
  forall k v2 v1.
Ord k =>
(k -> v2 -> Bool) -> Map k v1 -> Map k v2 -> Map k v1
intersectDomPLeft (\k
_k k
v2 -> k
v2 forall a. Eq a => a -> a -> Bool
== k
hk) f k v
stake f k v
delegs
compute (DRestrict (Dom (RRestrict (Base BaseRep f k v
MapR f k v
delegs) (Base BaseRep f k v
_ f k v
rngf))) (Base BaseRep f k v
MapR f k v
stake)) =
  forall k v2 v1.
Ord k =>
(k -> v2 -> Bool) -> Map k v1 -> Map k v2 -> Map k v1
intersectDomPLeft (\k
_k k
v2 -> forall (f :: * -> * -> *) key b.
(Iter f, Ord key) =>
key -> f key b -> Bool
haskey k
v2 f k v
rngf) f k v
stake f k v
delegs
compute (DRestrict Exp (g k ())
set (Base BaseRep f k v
MapR f k v
ys)) = forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys f k v
ys Set k
set2 -- Pay the cost of materializing set to use O(n* log n) restictKeys
  where
    Sett Set k
Set k
set2 = forall k (f :: * -> * -> *) v.
Ord k =>
BaseRep f k v -> Collect (k, v) -> f k v
materialize forall k. Basic Sett => BaseRep Sett k ()
SetR (forall (f :: * -> * -> *) k v. Iter f => f k v -> Collect (k, v)
lifo (forall t. Exp t -> t
compute Exp (g k ())
set))
compute (DRestrict (Base BaseRep f k v
SetR (Sett Set k
s1)) (Base BaseRep f k v
SetR (Sett Set k
s2))) = forall k. Set k -> Sett k ()
Sett (forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set k
s1 Set k
s2)
compute (DRestrict (Base BaseRep f k v
SetR f k v
x1) (Base BaseRep f k v
rep f k v
x2)) = forall k (f :: * -> * -> *) v.
Ord k =>
BaseRep f k v -> Collect (k, v) -> f k v
materialize BaseRep f k v
rep forall a b. (a -> b) -> a -> b
$ do (k
x, v
_, v
z) <- f k v
x1 forall k (f :: * -> * -> *) (g :: * -> * -> *) b c.
(Ord k, Iter f, Iter g) =>
f k b -> g k c -> Collect (k, b, c)
`domEq` f k v
x2; forall t. t -> Collect t
one (k
x, v
z)
compute (DRestrict (Dom (Base BaseRep f k v
_ f k v
x1)) (Base BaseRep f k v
rep f k v
x2)) = forall k (f :: * -> * -> *) v.
Ord k =>
BaseRep f k v -> Collect (k, v) -> f k v
materialize BaseRep f k v
rep forall a b. (a -> b) -> a -> b
$ do (k
x, v
_, v
z) <- f k v
x1 forall k (f :: * -> * -> *) (g :: * -> * -> *) b c.
(Ord k, Iter f, Iter g) =>
f k b -> g k c -> Collect (k, b, c)
`domEq` f k v
x2; forall t. t -> Collect t
one (k
x, v
z)
compute (DRestrict (SetSingleton k
k) (Base BaseRep f k v
rep f k v
x2)) = forall k (f :: * -> * -> *) v.
Ord k =>
BaseRep f k v -> Collect (k, v) -> f k v
materialize BaseRep f k v
rep forall a b. (a -> b) -> a -> b
$ do (k
x, ()
_, v
z) <- (forall k. k -> Single k ()
SetSingle k
k) forall k (f :: * -> * -> *) (g :: * -> * -> *) b c.
(Ord k, Iter f, Iter g) =>
f k b -> g k c -> Collect (k, b, c)
`domEq` f k v
x2; forall t. t -> Collect t
one (k
x, v
z)
compute (DRestrict (Dom (Singleton k
k v
_)) (Base BaseRep f k v
rep f k v
x2)) = forall k (f :: * -> * -> *) v.
Ord k =>
BaseRep f k v -> Collect (k, v) -> f k v
materialize BaseRep f k v
rep forall a b. (a -> b) -> a -> b
$ do (k
x, ()
_, v
z) <- (forall k. k -> Single k ()
SetSingle k
k) forall k (f :: * -> * -> *) (g :: * -> * -> *) b c.
(Ord k, Iter f, Iter g) =>
f k b -> g k c -> Collect (k, b, c)
`domEq` f k v
x2; forall t. t -> Collect t
one (k
x, v
z)
compute (DRestrict (Rng (Singleton k
_ v
v)) (Base BaseRep f k v
rep f k v
x2)) = forall k (f :: * -> * -> *) v.
Ord k =>
BaseRep f k v -> Collect (k, v) -> f k v
materialize BaseRep f k v
rep forall a b. (a -> b) -> a -> b
$ do (v
x, ()
_, v
z) <- (forall k. k -> Single k ()
SetSingle v
v) forall k (f :: * -> * -> *) (g :: * -> * -> *) b c.
(Ord k, Iter f, Iter g) =>
f k b -> g k c -> Collect (k, b, c)
`domEq` f k v
x2; forall t. t -> Collect t
one (v
x, v
z)
compute (DExclude (SetSingleton k
n) (Base BaseRep f k v
MapR f k v
m)) = forall k a. Ord k => Map k a -> Set k -> Map k a
Map.withoutKeys f k v
m (forall a. a -> Set a
Set.singleton k
n)
compute (DExclude (Dom (Singleton k
n v
_v)) (Base BaseRep f k v
MapR f k v
m)) = forall k a. Ord k => Map k a -> Set k -> Map k a
Map.withoutKeys f k v
m (forall a. a -> Set a
Set.singleton k
n)
compute (DExclude (Rng (Singleton k
_n v
v)) (Base BaseRep f k v
MapR f k v
m)) = forall k a. Ord k => Map k a -> Set k -> Map k a
Map.withoutKeys f k v
m (forall a. a -> Set a
Set.singleton v
v)
compute (DExclude (Base BaseRep f k v
SetR (Sett Set k
x1)) (Base BaseRep f k v
MapR f k v
x2)) = forall k a. Ord k => Map k a -> Set k -> Map k a
Map.withoutKeys f k v
x2 Set k
x1
compute (DExclude (Dom (Base BaseRep f k v
MapR f k v
x1)) (Base BaseRep f k v
MapR f k v
x2)) = forall k a b. Ord k => Map k a -> Map k b -> Map k a
noKeys f k v
x2 f k v
x1
compute (RExclude (Base BaseRep f k v
MapR f k v
xs) (Base BaseRep f k v
SetR (Sett Set k
y))) = forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (\k
x -> Bool -> Bool
not (forall a. Ord a => a -> Set a -> Bool
Set.member k
x Set k
y)) f k v
xs
compute (RExclude (Base BaseRep f k v
MapR f k v
xs) (SetSingleton k
k)) = forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Eq a => a -> a -> Bool
== k
k)) f k v
xs
compute (RExclude (Base BaseRep f k v
_rep f k v
lhs) (Base BaseRep f k v
SetR (Sett Set k
rhs))) | forall a. Set a -> Bool
Set.null Set k
rhs = f k v
lhs
compute (RExclude (Base BaseRep f k v
_rep f k v
lhs) (Base BaseRep f k v
SingleR f k v
Single k v
Fail)) = f k v
lhs
compute (RExclude (Base BaseRep f k v
rep f k v
lhs) Exp (g v ())
y) =
  forall k (f :: * -> * -> *) v.
Ord k =>
BaseRep f k v -> Collect (k, v) -> f k v
materialize BaseRep f k v
rep forall a b. (a -> b) -> a -> b
$ do (k
a, v
b) <- forall (f :: * -> * -> *) k v. Iter f => f k v -> Collect (k, v)
lifo f k v
lhs; Bool -> Collect ()
when (Bool -> Bool
not (forall (f :: * -> * -> *) key b.
(Iter f, Ord key) =>
key -> f key b -> Bool
haskey v
b Query v ()
rhs)); forall t. t -> Collect t
one (k
a, v
b)
  where
    (Query v ()
rhs, BaseRep g v ()
_) = forall (f :: * -> * -> *) k v.
Exp (f k v) -> (Query k v, BaseRep f k v)
compile Exp (g v ())
y

-- (dom (Map(16)? ▷ (setSingleton _ )))
compute (RRestrict (Base BaseRep f k v
MapR f k v
xs) (SetSingleton k
k)) = forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (\k
x -> k
x forall a. Eq a => a -> a -> Bool
== k
k) f k v
xs
-- ((dom rewards' ◁ delegs) ▷ dom poolParams)  in LedgerState.hs
compute (RRestrict (DRestrict (Dom (Base BaseRep f k v
MapR f k v
x)) (Base BaseRep f k v
MapR f k v
y)) (Dom (Base BaseRep f k v
MapR f k v
z))) = forall k v2 v1.
Ord k =>
(k -> v2 -> Bool) -> Map k v1 -> Map k v2 -> Map k v2
intersectDomP (\k
_k k
v -> forall k a. Ord k => k -> Map k a -> Bool
Map.member k
v f k v
z) f k v
x f k v
y
compute (RRestrict (DRestrict (Dom (Base BaseRep f k v
_r1 f k v
stkcreds)) (Base BaseRep f k v
r2 f k v
delegs)) (Dom (Base BaseRep f k v
_r3 f k v
stpools))) =
  forall k (f :: * -> * -> *) v.
Ord k =>
BaseRep f k v -> Collect (k, v) -> f k v
materialize BaseRep f k v
r2 forall a b. (a -> b) -> a -> b
$ do (k
x, v
_, v
y) <- f k v
stkcreds forall k (f :: * -> * -> *) (g :: * -> * -> *) b c.
(Ord k, Iter f, Iter g) =>
f k b -> g k c -> Collect (k, b, c)
`domEq` f k v
delegs; v
y forall (f :: * -> * -> *) k v.
(Iter f, Ord k) =>
k -> f k v -> Collect ()
`element` f k v
stpools; forall t. t -> Collect t
one (k
x, v
y)
compute (Elem k
k (Dom (Base BaseRep f k v
_rep f k v
x))) = forall (f :: * -> * -> *) key b.
(Iter f, Ord key) =>
key -> f key b -> Bool
haskey k
k f k v
x
compute (Elem k
k (Base BaseRep f k v
_rep f k v
rel)) = forall (f :: * -> * -> *) key b.
(Iter f, Ord key) =>
key -> f key b -> Bool
haskey k
k f k v
rel
compute (Elem k
k (Dom (Singleton k
key v
_v))) = k
k forall a. Eq a => a -> a -> Bool
== k
key
compute (Elem k
k (Rng (Singleton k
_ v
key))) = k
k forall a. Eq a => a -> a -> Bool
== v
key
compute (Elem k
k (SetSingleton k
key)) = k
k forall a. Eq a => a -> a -> Bool
== k
key
compute (Elem k
k (UnionOverrideLeft (Base BaseRep f k v
SetR (Sett Set k
x)) (Base BaseRep f k v
SetR (Sett Set k
y)))) = (forall a. Ord a => a -> Set a -> Bool
Set.member k
k Set k
x Bool -> Bool -> Bool
|| forall a. Ord a => a -> Set a -> Bool
Set.member k
k Set k
y)
compute (Elem k
k (UnionOverrideRight (Base BaseRep f k v
SetR (Sett Set k
x)) (Base BaseRep f k v
SetR (Sett Set k
y)))) = (forall a. Ord a => a -> Set a -> Bool
Set.member k
k Set k
x Bool -> Bool -> Bool
|| forall a. Ord a => a -> Set a -> Bool
Set.member k
k Set k
y)
compute (Elem k
k (UnionPlus (Base BaseRep f k v
SetR (Sett Set k
x)) (Base BaseRep f k v
SetR (Sett Set k
y)))) = (forall a. Ord a => a -> Set a -> Bool
Set.member k
k Set k
x Bool -> Bool -> Bool
|| forall a. Ord a => a -> Set a -> Bool
Set.member k
k Set k
y)
compute (Elem k
k (Intersect (Base BaseRep f k v
SetR (Sett Set k
x)) (Base BaseRep f k v
SetR (Sett Set k
y)))) = (forall a. Ord a => a -> Set a -> Bool
Set.member k
k Set k
x Bool -> Bool -> Bool
&& forall a. Ord a => a -> Set a -> Bool
Set.member k
k Set k
y)
compute (Elem k
k (DRestrict Exp (g k ())
s1 Exp (f k v)
m1)) = forall t. Exp t -> t
compute (forall k (g :: * -> * -> *).
(Ord k, Iter g, Show k) =>
k -> Exp (g k ()) -> Exp Bool
Elem k
k Exp (g k ())
s1) Bool -> Bool -> Bool
&& forall t. Exp t -> t
compute (forall k (g :: * -> * -> *).
(Ord k, Iter g, Show k) =>
k -> Exp (g k ()) -> Exp Bool
Elem k
k Exp (f k v)
m1)
compute (Elem k
k (DExclude Exp (g k ())
s1 Exp (f k v)
m1)) = Bool -> Bool
not (forall t. Exp t -> t
compute (forall k (g :: * -> * -> *).
(Ord k, Iter g, Show k) =>
k -> Exp (g k ()) -> Exp Bool
Elem k
k Exp (g k ())
s1)) Bool -> Bool -> Bool
&& forall t. Exp t -> t
compute (forall k (g :: * -> * -> *).
(Ord k, Iter g, Show k) =>
k -> Exp (g k ()) -> Exp Bool
Elem k
k Exp (f k v)
m1)
compute (NotElem k
k (Dom (Base BaseRep f k v
_rep f k v
x))) = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (f :: * -> * -> *) key b.
(Iter f, Ord key) =>
key -> f key b -> Bool
haskey k
k f k v
x
compute (NotElem k
k (Base BaseRep f k v
_rep f k v
rel)) = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (f :: * -> * -> *) key b.
(Iter f, Ord key) =>
key -> f key b -> Bool
haskey k
k f k v
rel
compute (NotElem k
k (Dom (Singleton k
key v
_v))) = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ k
k forall a. Eq a => a -> a -> Bool
== k
key
compute (NotElem k
k (Rng (Singleton k
_ v
key))) = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ k
k forall a. Eq a => a -> a -> Bool
== v
key
compute (NotElem k
k (SetSingleton k
key)) = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ k
k forall a. Eq a => a -> a -> Bool
== k
key
compute (NotElem k
k (UnionOverrideLeft (Base BaseRep f k v
SetR (Sett Set k
x)) (Base BaseRep f k v
SetR (Sett Set k
y)))) = Bool -> Bool
not (forall a. Ord a => a -> Set a -> Bool
Set.member k
k Set k
x Bool -> Bool -> Bool
|| forall a. Ord a => a -> Set a -> Bool
Set.member k
k Set k
y)
compute (NotElem k
k (UnionOverrideRight (Base BaseRep f k v
SetR (Sett Set k
x)) (Base BaseRep f k v
SetR (Sett Set k
y)))) = Bool -> Bool
not (forall a. Ord a => a -> Set a -> Bool
Set.member k
k Set k
x Bool -> Bool -> Bool
|| forall a. Ord a => a -> Set a -> Bool
Set.member k
k Set k
y)
compute (NotElem k
k (UnionPlus (Base BaseRep f k v
SetR (Sett Set k
x)) (Base BaseRep f k v
SetR (Sett Set k
y)))) = Bool -> Bool
not (forall a. Ord a => a -> Set a -> Bool
Set.member k
k Set k
x Bool -> Bool -> Bool
|| forall a. Ord a => a -> Set a -> Bool
Set.member k
k Set k
y)
compute (NotElem k
k (Intersect (Base BaseRep f k v
SetR (Sett Set k
x)) (Base BaseRep f k v
SetR (Sett Set k
y)))) = Bool -> Bool
not (forall a. Ord a => a -> Set a -> Bool
Set.member k
k Set k
x Bool -> Bool -> Bool
&& forall a. Ord a => a -> Set a -> Bool
Set.member k
k Set k
y)
compute (Subset (Base BaseRep f k v
SetR (Sett Set k
x)) (Base BaseRep f k v
SetR (Sett Set k
y))) = forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set k
x Set k
y
compute (Subset (Base BaseRep f k v
SetR (Sett Set k
x)) (Base BaseRep f k v
MapR f k v
y)) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall k a. Ord k => k -> Map k a -> Bool
`Map.member` f k v
y) Set k
x
compute (Subset (Base BaseRep f k v
SetR (Sett Set k
x)) (Dom (Base BaseRep f k v
MapR f k v
y))) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall k a. Ord k => k -> Map k a -> Bool
`Map.member` f k v
y) Set k
x
compute (Subset (Base BaseRep f k v
MapR f k v
x) (Base BaseRep f k v
MapR f k v
y)) = forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey k -> v -> Bool -> Bool
accum Bool
True f k v
x
  where
    accum :: k -> v -> Bool -> Bool
accum k
k v
_a Bool
ans = forall k a. Ord k => k -> Map k a -> Bool
Map.member k
k f k v
y Bool -> Bool -> Bool
&& Bool
ans
compute (Subset (Dom (Base BaseRep f k v
MapR f k v
x)) (Dom (Base BaseRep f k v
MapR f k v
y))) = forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey k -> v -> Bool -> Bool
accum Bool
True f k v
x
  where
    accum :: k -> v -> Bool -> Bool
accum k
k v
_a Bool
ans = forall k a. Ord k => k -> Map k a -> Bool
Map.member k
k f k v
y Bool -> Bool -> Bool
&& Bool
ans
compute (Intersect (Base BaseRep f k v
SetR (Sett Set k
x)) (Base BaseRep f k v
SetR (Sett Set k
y))) = forall k. Set k -> Sett k ()
Sett (forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set k
x Set k
y)
compute (Intersect (Base BaseRep f k v
MapR f k v
x) (Base BaseRep f k v
MapR f k v
y)) = forall k. Set k -> Sett k ()
Sett (forall k a. Map k a -> Set k
Map.keysSet (forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection f k v
x f k v
y))
compute (SetDiff (Base BaseRep f k v
SetR (Sett Set k
x)) (Base BaseRep f k v
SetR (Sett Set k
y))) = forall k. Set k -> Sett k ()
Sett (forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set k
x Set k
y)
compute (SetDiff (Base BaseRep f k v
SetR (Sett Set k
x)) (Base BaseRep f k v
MapR f k v
y)) = forall k. Set k -> Sett k ()
Sett (forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\k
e -> Bool -> Bool
not (forall k a. Ord k => k -> Map k a -> Bool
Map.member k
e f k v
y)) Set k
x)
compute (SetDiff (Base BaseRep f k v
SetR (Sett Set k
x)) (Dom (Base BaseRep f k v
MapR f k v
y))) = forall k. Set k -> Sett k ()
Sett (forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\k
e -> Bool -> Bool
not (forall k a. Ord k => k -> Map k a -> Bool
Map.member k
e f k v
y)) Set k
x)
compute (SetDiff (Base BaseRep f k v
MapR f k v
x) (Dom (Base BaseRep f k v
MapR f k v
y))) = forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.difference f k v
x f k v
y
compute (SetDiff (Base BaseRep f k v
MapR f k v
x) (Base BaseRep f k v
MapR f k v
y)) = (forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.difference f k v
x f k v
y)
compute (SetDiff (Base BaseRep f k v
MapR f k v
x) (Base BaseRep f k v
SetR (Sett Set k
y))) = (forall k a. Ord k => Map k a -> Set k -> Map k a
Map.withoutKeys f k v
x Set k
y)
compute (UnionOverrideLeft (Base BaseRep f k v
_rep f k v
x) (Singleton k
k v
v)) = forall (f :: * -> * -> *) k v.
(Basic f, Ord k) =>
(k, v) -> f k v -> (v -> v -> v) -> f k v
addkv (k
k, v
v) f k v
x (\v
old v
_new -> v
old) -- The value on the left is preferred over the right, so 'addkv' chooses 'old'
compute (UnionOverrideLeft (Base BaseRep f k v
MapR f k v
d0) (Base BaseRep f k v
MapR f k v
d1)) = forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union f k v
d0 f k v
d1 -- 'Map.union' is left biased, just what we want.
compute (UnionOverrideLeft (Base BaseRep f k v
SetR (Sett Set k
x)) (Base BaseRep f k v
SetR (Sett Set k
y))) = forall k. Set k -> Sett k ()
Sett (forall a. Ord a => Set a -> Set a -> Set a
Set.union Set k
x Set k
y)
compute (UnionOverrideLeft (DExclude (SetSingleton k
k) (Base BaseRep f k v
MapR f k v
xs)) (Base BaseRep f k v
MapR f k v
ys)) = forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (forall k a. Ord k => k -> Map k a -> Map k a
Map.delete k
k f k v
xs) f k v
ys
compute (UnionOverrideLeft (DExclude (Base BaseRep f k v
SetR (Sett Set k
s1)) (Base BaseRep f k v
MapR f k v
m2)) (Base BaseRep f k v
MapR f k v
m3)) = forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (forall k a. Ord k => Map k a -> Set k -> Map k a
Map.withoutKeys f k v
m2 Set k
s1) f k v
m3
compute (UnionOverrideRight (Base BaseRep f k v
_rep f k v
x) (Singleton k
k v
v)) = forall (f :: * -> * -> *) k v.
(Basic f, Ord k) =>
(k, v) -> f k v -> (v -> v -> v) -> f k v
addkv (k
k, v
v) f k v
x (\v
_old v
new -> v
new) -- The value on the right is preferred over the left, so 'addkv' chooses 'new'
compute (UnionOverrideRight (Base BaseRep f k v
MapR f k v
d0) (Base BaseRep f k v
MapR f k v
d1)) = forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union f k v
d1 f k v
d0 -- we pass @d1@ as first argument, since 'Map.union' is left biased.
compute (UnionOverrideRight (Base BaseRep f k v
SetR (Sett Set k
x)) (Base BaseRep f k v
SetR (Sett Set k
y))) = forall k. Set k -> Sett k ()
Sett (forall a. Ord a => Set a -> Set a -> Set a
Set.union Set k
x Set k
y)
compute (UnionPlus (Base BaseRep f k v
MapR f k v
x) (Base BaseRep f k v
MapR f k v
y)) = forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Semigroup a => a -> a -> a
(<>) f k v
x f k v
y
compute (UnionPlus (Base BaseRep f k v
SetR (Sett Set k
x)) (Base BaseRep f k v
SetR (Sett Set k
y))) = forall k. Set k -> Sett k ()
Sett (forall a. Ord a => Set a -> Set a -> Set a
Set.union Set k
x Set k
y) -- Recall (Sett k):: f k (), so () <> () = ()
compute (Singleton k
k v
v) = forall k v. k -> v -> Single k v
Single k
k v
v
compute (SetSingleton k
k) = (forall k. k -> Single k ()
SetSingle k
k)
compute (KeyEqual (Base BaseRep f k v
MapR f k v
m) (Base BaseRep f k v
MapR f k v
n)) = forall k v1 v2. Ord k => Map k v1 -> Map k v2 -> Bool
keysEqual f k v
m f k v
n
compute (KeyEqual (Dom (Base BaseRep f k v
MapR f k v
m)) (Dom (Base BaseRep f k v
MapR f k v
n))) = forall k v1 v2. Ord k => Map k v1 -> Map k v2 -> Bool
keysEqual f k v
m f k v
n
compute (KeyEqual (Base BaseRep f k v
SetR (Sett Set k
m)) (Base BaseRep f k v
SetR (Sett Set k
n))) = Set k
n forall a. Eq a => a -> a -> Bool
== Set k
m
compute (KeyEqual (Base BaseRep f k v
MapR f k v
xs) (Base BaseRep f k v
SetR (Sett Set k
ys))) = forall k a. Map k a -> Set k
Map.keysSet f k v
xs forall a. Eq a => a -> a -> Bool
== Set k
ys
compute Exp t
x = forall t. Exp t -> t
computeSlow Exp t
x

eval :: Embed s t => Exp t -> s
eval :: forall s t. Embed s t => Exp t -> s
eval Exp t
x = forall concrete base. Embed concrete base => base -> concrete
fromBase (forall t. Exp t -> t
compute Exp t
x)

computeSlow :: Exp t -> t
computeSlow :: forall t. Exp t -> t
computeSlow (Base BaseRep f k v
_ f k v
t) = f k v
t
computeSlow (e :: Exp t
e@(Dom Exp (f k v)
_)) = forall k (f :: * -> * -> *) v. Ord k => Exp (f k v) -> f k v
runSetExp Exp t
e
computeSlow (e :: Exp t
e@(Rng Exp (f k v)
_)) = forall k (f :: * -> * -> *) v. Ord k => Exp (f k v) -> f k v
runSetExp Exp t
e
computeSlow (e :: Exp t
e@(DRestrict Exp (g k ())
_ Exp (f k v)
_)) = forall k (f :: * -> * -> *) v. Ord k => Exp (f k v) -> f k v
runSetExp Exp t
e
computeSlow (e :: Exp t
e@(DExclude Exp (g k ())
_ Exp (f k v)
_)) = forall k (f :: * -> * -> *) v. Ord k => Exp (f k v) -> f k v
runSetExp Exp t
e
computeSlow (e :: Exp t
e@(RExclude Exp (f k v)
_ Exp (g v ())
_)) = forall k (f :: * -> * -> *) v. Ord k => Exp (f k v) -> f k v
runSetExp Exp t
e
computeSlow (e :: Exp t
e@(RRestrict Exp (f k v)
_ Exp (g v ())
_)) = forall k (f :: * -> * -> *) v. Ord k => Exp (f k v) -> f k v
runSetExp Exp t
e
computeSlow (e :: Exp t
e@(Elem k
_ Exp (g k ())
_)) = Exp Bool -> Bool
runBoolExp Exp t
e
computeSlow (e :: Exp t
e@(NotElem k
_ Exp (g k ())
_)) = Exp Bool -> Bool
runBoolExp Exp t
e
computeSlow (e :: Exp t
e@(Subset Exp (f k v)
_ Exp (g k u)
_)) = Exp Bool -> Bool
runBoolExp Exp t
e
computeSlow (e :: Exp t
e@(Intersect Exp (f k v)
_ Exp (g k u)
_)) = forall k (f :: * -> * -> *) v. Ord k => Exp (f k v) -> f k v
runSetExp Exp t
e
computeSlow (e :: Exp t
e@(SetDiff Exp (f k v)
_ Exp (g k u)
_)) = forall k (f :: * -> * -> *) v. Ord k => Exp (f k v) -> f k v
runSetExp Exp t
e
computeSlow (e :: Exp t
e@(UnionOverrideLeft Exp (f k v)
_ Exp (g k v)
_)) = forall k (f :: * -> * -> *) v. Ord k => Exp (f k v) -> f k v
runSetExp Exp t
e
computeSlow (e :: Exp t
e@(UnionOverrideRight Exp (f k v)
_ Exp (g k v)
_)) = forall k (f :: * -> * -> *) v. Ord k => Exp (f k v) -> f k v
runSetExp Exp t
e
computeSlow (e :: Exp t
e@(UnionPlus Exp (f k n)
_ Exp (g k n)
_)) = forall k (f :: * -> * -> *) v. Ord k => Exp (f k v) -> f k v
runSetExp Exp t
e
computeSlow (Singleton k
k v
v) = forall k v. k -> v -> Single k v
Single k
k v
v
computeSlow (SetSingleton k
k) = (forall k. k -> Single k ()
SetSingle k
k)
computeSlow (e :: Exp t
e@(KeyEqual Exp (f k v)
_ Exp (g k u)
_)) = Exp Bool -> Bool
runBoolExp Exp t
e

-- ==========================================================================
-- The most basic operation of iteration, where (Iter f) is to use the 'nxt'
-- operator on (f k v) to create a (Collect k v). The two possible
-- ways to produce their elements are in LIFO or FIFO order.
-- ===========================================================================

lifo :: Iter f => f k v -> Collect (k, v)
lifo :: forall (f :: * -> * -> *) k v. Iter f => f k v -> Collect (k, v)
lifo f k v
x = do (k
k, v
v, f k v
x2) <- forall (f :: * -> * -> *) a b.
Iter f =>
f a b -> Collect (a, b, f a b)
nxt f k v
x; forall t. t -> Collect t -> Collect t
front (k
k, v
v) (forall (f :: * -> * -> *) k v. Iter f => f k v -> Collect (k, v)
lifo f k v
x2)

fifo :: Iter f => f k v -> Collect (k, v)
fifo :: forall (f :: * -> * -> *) k v. Iter f => f k v -> Collect (k, v)
fifo f k v
x = do (k
k, v
v, f k v
x2) <- forall (f :: * -> * -> *) a b.
Iter f =>
f a b -> Collect (a, b, f a b)
nxt f k v
x; forall t. Collect t -> t -> Collect t
rear (forall (f :: * -> * -> *) k v. Iter f => f k v -> Collect (k, v)
fifo f k v
x2) (k
k, v
v)

-- ================================================================================
-- A witness (BaseRep) can be used to specifiy how to build a specifc datatype from
-- a CONCRETE sequence of tuples (a [(k,v)]). This is a way to import a type from from
--  a list. But unlike 'materialize' an arbitray [(k,v)] may have duplicate keys,
--  so when that happens, use 'combine' to merge the associated values.
-- ================================================================================

addp :: (Ord k, Basic f) => (v -> v -> v) -> (k, v) -> f k v -> f k v
addp :: forall k (f :: * -> * -> *) v.
(Ord k, Basic f) =>
(v -> v -> v) -> (k, v) -> f k v -> f k v
addp v -> v -> v
combine (k
k, v
v) f k v
xs = forall (f :: * -> * -> *) k v.
(Basic f, Ord k) =>
(k, v) -> f k v -> (v -> v -> v) -> f k v
addkv (k
k, v
v) f k v
xs v -> v -> v
combine

-- | Turn a list of pairs into any 'Basic' type. The first argument is a 'BaseRep' which
--   chooses what Base type to construct.
-- The combine function comb = (\\ earlier later -> later) will let values
-- later in the list override ones earlier in the list, and comb =
-- (\\ earlier later -> earlier) will keep the value that appears first in the list
fromList :: Ord k => BaseRep f k v -> (v -> v -> v) -> [(k, v)] -> f k v
fromList :: forall k (f :: * -> * -> *) v.
Ord k =>
BaseRep f k v -> (v -> v -> v) -> [(k, v)] -> f k v
fromList BaseRep f k v
MapR v -> v -> v
combine [(k, v)]
xs = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith v -> v -> v
combine [(k, v)]
xs
fromList BaseRep f k v
ListR v -> v -> v
combine [(k, v)]
xs = forall k v. Ord k => (v -> v -> v) -> [(k, v)] -> List k v
fromPairs v -> v -> v
combine [(k, v)]
xs
fromList BaseRep f k v
SetR v -> v -> v
combine [(k, v)]
xs = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall k (f :: * -> * -> *) v.
(Ord k, Basic f) =>
(v -> v -> v) -> (k, v) -> f k v -> f k v
addp v -> v -> v
combine) (forall k. Set k -> Sett k ()
Sett (forall a. Set a
Set.empty)) [(k, v)]
xs
fromList BaseRep f k v
SingleR v -> v -> v
combine [(k, v)]
xs = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall k (f :: * -> * -> *) v.
(Ord k, Basic f) =>
(v -> v -> v) -> (k, v) -> f k v -> f k v
addp v -> v -> v
combine) forall k v. Single k v
Fail [(k, v)]
xs

-- =======================================================================================

-- | A witness (BaseRep) can be used to materialize a (Collect k v) into the type witnessed by the BaseRep.
-- Recall a (Collect k v) has no intrinsic type (it is just an ABSTRACT sequence of tuples), so
-- the witness describes how to turn them into the chosen datatype. Note that materialize is meant
-- to be applied to a collection built by iterating over a Query. This produces the keys in
-- ascending order, with no duplicate keys. So we do not need to specify how to merge duplicate values.
materialize :: Ord k => BaseRep f k v -> Collect (k, v) -> f k v
materialize :: forall k (f :: * -> * -> *) v.
Ord k =>
BaseRep f k v -> Collect (k, v) -> f k v
materialize BaseRep f k v
ListR Collect (k, v)
x = forall k v. Ord k => (v -> v -> v) -> [(k, v)] -> List k v
fromPairs (\v
l v
_r -> v
l) (forall tuple.
Collect tuple -> forall ans. ans -> (tuple -> ans -> ans) -> ans
runCollect Collect (k, v)
x [] (:))
materialize BaseRep f k v
MapR Collect (k, v)
x = forall tuple.
Collect tuple -> forall ans. ans -> (tuple -> ans -> ans) -> ans
runCollect Collect (k, v)
x forall k a. Map k a
Map.empty (\(k
k, v
v) f k v
ans -> forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
k v
v f k v
ans)
materialize BaseRep f k v
SetR Collect (k, v)
x = forall k. Set k -> Sett k ()
Sett (forall tuple.
Collect tuple -> forall ans. ans -> (tuple -> ans -> ans) -> ans
runCollect Collect (k, v)
x forall a. Set a
Set.empty (\(k
k, v
_) Set k
ans -> forall a. Ord a => a -> Set a -> Set a
Set.insert k
k Set k
ans))
materialize BaseRep f k v
SingleR Collect (k, v)
x = forall tuple.
Collect tuple -> forall ans. ans -> (tuple -> ans -> ans) -> ans
runCollect Collect (k, v)
x forall k v. Single k v
Fail (\(k
k, v
v) f k v
_ignore -> forall k v. k -> v -> Single k v
Single k
k v
v)

-- =========================================================================================
-- Now we make an iterator that collects triples, on the intersection
-- of the domain of the two Iter types 'f' and 'g'. An answer of (k,b,c) means that
-- (k,b) is in m::f k a, and (k,c) is in n::g k c. All the other possible triples
-- are skipped over.  This is an instance of a thing called a "Generic Join"
-- See https://arxiv.org/pdf/1310.3314.pdf  or  http://personales.dcc.uchile.cl/~pbarcelo/ngo.pdf
-- The number of tuples it touches is proportional to the size of the output (modulo log factors).
-- It's cost is unrelated to the size of its inputs (modulo log factors)
-- This is a very specific version of the AndD compound iterator. It is used in the function 'eval'
-- =========================================================================================

(⨝) :: (Ord k, Iter f, Iter g) => f k b -> g k c -> Collect (k, b, c)
⨝ :: forall k (f :: * -> * -> *) (g :: * -> * -> *) b c.
(Ord k, Iter f, Iter g) =>
f k b -> g k c -> Collect (k, b, c)
(⨝) = forall k (f :: * -> * -> *) (g :: * -> * -> *) b c.
(Ord k, Iter f, Iter g) =>
f k b -> g k c -> Collect (k, b, c)
domEq

domEq :: (Ord k, Iter f, Iter g) => f k b -> g k c -> Collect (k, b, c)
domEq :: forall k (f :: * -> * -> *) (g :: * -> * -> *) b c.
(Ord k, Iter f, Iter g) =>
f k b -> g k c -> Collect (k, b, c)
domEq f k b
m g k c
n = do
  (k, b, f k b)
triplem <- forall (f :: * -> * -> *) a b.
Iter f =>
f a b -> Collect (a, b, f a b)
nxt f k b
m
  (k, c, g k c)
triplen <- forall (f :: * -> * -> *) a b.
Iter f =>
f a b -> Collect (a, b, f a b)
nxt g k c
n
  let loop :: (k, b, f k b) -> (k, b, f k b) -> Collect (k, b, b)
loop (mt :: (k, b, f k b)
mt@(k
k1, b
b, f k b
nextm)) (nt :: (k, b, f k b)
nt@(k
k2, b
c, f k b
nextn)) =
        case forall a. Ord a => a -> a -> Ordering
compare k
k1 k
k2 of
          Ordering
EQ -> forall t. t -> Collect t -> Collect t
front (k
k1, b
b, b
c) (forall k (f :: * -> * -> *) (g :: * -> * -> *) b c.
(Ord k, Iter f, Iter g) =>
f k b -> g k c -> Collect (k, b, c)
domEq f k b
nextm f k b
nextn)
          Ordering
LT -> do (k, b, f k b)
mt' <- forall (f :: * -> * -> *) k b.
(Iter f, Ord k) =>
k -> f k b -> Collect (k, b, f k b)
lub k
k2 f k b
nextm; (k, b, f k b) -> (k, b, f k b) -> Collect (k, b, b)
loop (k, b, f k b)
mt' (k, b, f k b)
nt
          Ordering
GT -> do (k, b, f k b)
nt' <- forall (f :: * -> * -> *) k b.
(Iter f, Ord k) =>
k -> f k b -> Collect (k, b, f k b)
lub k
k1 f k b
nextn; (k, b, f k b) -> (k, b, f k b) -> Collect (k, b, b)
loop (k, b, f k b)
mt (k, b, f k b)
nt'
  forall {k} {f :: * -> * -> *} {f :: * -> * -> *} {b} {b}.
(Ord k, Iter f, Iter f) =>
(k, b, f k b) -> (k, b, f k b) -> Collect (k, b, b)
loop (k, b, f k b)
triplem (k, c, g k c)
triplen

-- This is included here for the benchmark tests. It is much slower because it does not use lub.

domEqSlow :: (Ord k, Iter f, Iter g) => f k b -> g k c -> Collect (k, b, c)
domEqSlow :: forall k (f :: * -> * -> *) (g :: * -> * -> *) b c.
(Ord k, Iter f, Iter g) =>
f k b -> g k c -> Collect (k, b, c)
domEqSlow f k b
m g k c
n = do
  (k, b, f k b)
triplem <- forall (f :: * -> * -> *) a b.
Iter f =>
f a b -> Collect (a, b, f a b)
nxt f k b
m
  (k, c, g k c)
triplen <- forall (f :: * -> * -> *) a b.
Iter f =>
f a b -> Collect (a, b, f a b)
nxt g k c
n
  let loop :: (a, b, f a b) -> (a, b, f a b) -> Collect (a, b, b)
loop (mt :: (a, b, f a b)
mt@(a
k1, b
b, f a b
nextm)) (nt :: (a, b, f a b)
nt@(a
k2, b
c, f a b
nextn)) =
        case forall a. Ord a => a -> a -> Ordering
compare a
k1 a
k2 of
          Ordering
EQ -> forall t. t -> Collect t -> Collect t
front (a
k1, b
b, b
c) (forall k (f :: * -> * -> *) (g :: * -> * -> *) b c.
(Ord k, Iter f, Iter g) =>
f k b -> g k c -> Collect (k, b, c)
domEqSlow f a b
nextm f a b
nextn)
          Ordering
LT -> do (a, b, f a b)
mt' <- forall (f :: * -> * -> *) a b.
Iter f =>
f a b -> Collect (a, b, f a b)
nxt f a b
nextm; (a, b, f a b) -> (a, b, f a b) -> Collect (a, b, b)
loop (a, b, f a b)
mt' (a, b, f a b)
nt
          Ordering
GT -> do (a, b, f a b)
nt' <- forall (f :: * -> * -> *) a b.
Iter f =>
f a b -> Collect (a, b, f a b)
nxt f a b
nextn; (a, b, f a b) -> (a, b, f a b) -> Collect (a, b, b)
loop (a, b, f a b)
mt (a, b, f a b)
nt'
  forall {k} {f :: * -> * -> *} {f :: * -> * -> *} {b} {b}.
(Ord k, Iter f, Iter f) =>
(k, b, f k b) -> (k, b, f k b) -> Collect (k, b, b)
loop (k, b, f k b)
triplem (k, c, g k c)
triplen

-- ================================================================================