{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

-- | This module provides deep embeddings of three things
--   1) Exp is a deep embedding of expressions over Sets and Maps as a typed data structure.
--   2) Fun is a deep embedding of symbolic functions
--   3) Query is a deep embedding of queries over Sets and Maps. It can be thought of as
--      a low-level compiled form of Exp
module Control.Iterate.Exp where

import Control.Iterate.BaseTypes (
  BaseRep (..),
  Basic (..),
  Iter (..),
  List (..),
  Sett (..),
  Single (..),
  fromPairs,
 )
import Control.Iterate.Collect (Collect (..), hasElem, none, one)
import Data.List (sortBy)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Prettyprinter (Doc, align, parens, pretty, vsep, (<+>))
import Prelude hiding (lookup)

-- $Deep embedding

-- ================================================================================================
-- PART 1. Exp over sets and maps
-- ================================================================================================

-- | The self typed GADT: Exp, that encodes the shape of Set expressions. A deep embedding.
-- Exp is a typed Symbolic representation of queries we may ask. It allows us to introspect a query
-- The strategy is to
--
-- 1. Define Exp so all queries can be represented.
-- 2. Define smart constructors that "parse" the surface syntax, and build a typed Exp
-- 3. Write an evaluate function:  eval:: Exp t -> t
-- 4. "eval" can introspect the code and apply efficient domain and type specific translations
-- 5.  Use the (Iter f) class to evaluate some Exp that can benefit from its efficient nature.
data Exp t where
  Base :: (Ord k, Basic f, Iter f) => BaseRep f k v -> f k v -> Exp (f k v)
  Dom :: Ord k => Exp (f k v) -> Exp (Sett k ())
  Rng :: (Ord k, Ord v) => Exp (f k v) -> Exp (Sett v ())
  DRestrict :: (Ord k, Iter g) => Exp (g k ()) -> Exp (f k v) -> Exp (f k v)
  DExclude :: (Ord k, Iter g) => Exp (g k ()) -> Exp (f k v) -> Exp (f k v)
  RRestrict :: (Ord k, Iter g, Ord v) => Exp (f k v) -> Exp (g v ()) -> Exp (f k v)
  RExclude :: (Ord k, Iter g, Ord v) => Exp (f k v) -> Exp (g v ()) -> Exp (f k v)
  Elem :: (Ord k, Iter g, Show k) => k -> Exp (g k ()) -> Exp Bool
  NotElem :: (Ord k, Iter g, Show k) => k -> Exp (g k ()) -> Exp Bool
  Intersect :: (Ord k, Iter f, Iter g) => Exp (f k v) -> Exp (g k u) -> Exp (Sett k ())
  Subset :: (Ord k, Iter f, Iter g) => Exp (f k v) -> Exp (g k u) -> Exp Bool
  SetDiff :: (Ord k, Iter f, Iter g) => Exp (f k v) -> Exp (g k u) -> Exp (f k v)
  UnionOverrideLeft :: (Show k, Show v, Ord k) => Exp (f k v) -> Exp (g k v) -> Exp (f k v)
  -- If 'k' appears in both, then choose the 'v' from the left 'f'
  -- The (Show k, Show v) supports logging errors if there are duplicate keys.
  UnionPlus :: (Ord k, Monoid n) => Exp (f k n) -> Exp (g k n) -> Exp (f k n)
  UnionOverrideRight :: Ord k => Exp (f k v) -> Exp (g k v) -> Exp (f k v)
  -- If 'k' appears in both, then choose the 'v' from the right 'g'
  Singleton :: Ord k => k -> v -> Exp (Single k v)
  SetSingleton :: Ord k => k -> Exp (Single k ())
  KeyEqual :: (Ord k, Iter f, Iter g) => Exp (f k v) -> Exp (g k u) -> Exp Bool

instance Show (Exp t) where
  show :: Exp t -> String
show (Base BaseRep f k v
MapR f k v
_) = String
"Map?"
  show (Base BaseRep f k v
SetR f k v
_) = String
"Set?"
  show (Base BaseRep f k v
ListR f k v
_) = String
"List?"
  show (Base BaseRep f k v
SingleR (Single k
_ v
_)) = String
"Single(_ _)"
  show (Base BaseRep f k v
SingleR (SetSingle k
_)) = String
"SetSingle(_)"
  show (Base BaseRep f k v
rep f k v
_x) = forall a. Show a => a -> String
show BaseRep f k v
rep forall a. [a] -> [a] -> [a]
++ String
"?"
  show (Dom Exp (f k v)
x) = String
"(dom " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (f k v)
x forall a. [a] -> [a] -> [a]
++ String
")"
  show (Rng Exp (f k v)
x) = String
"(rng " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (f k v)
x forall a. [a] -> [a] -> [a]
++ String
")"
  show (DRestrict Exp (g k ())
x Exp (f k v)
y) = String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (g k ())
x forall a. [a] -> [a] -> [a]
++ String
" ◁ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (f k v)
y forall a. [a] -> [a] -> [a]
++ String
")"
  show (DExclude Exp (g k ())
x Exp (f k v)
y) = String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (g k ())
x forall a. [a] -> [a] -> [a]
++ String
" ⋪ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (f k v)
y forall a. [a] -> [a] -> [a]
++ String
")"
  show (RRestrict Exp (f k v)
x Exp (g v ())
y) = String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (f k v)
x forall a. [a] -> [a] -> [a]
++ String
" ▷ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (g v ())
y forall a. [a] -> [a] -> [a]
++ String
")"
  show (RExclude Exp (f k v)
x Exp (g v ())
y) = String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (f k v)
x forall a. [a] -> [a] -> [a]
++ String
" ⋫ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (g v ())
y forall a. [a] -> [a] -> [a]
++ String
")"
  show (Elem k
k Exp (g k ())
x) = String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show k
k forall a. [a] -> [a] -> [a]
++ String
" ∈ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (g k ())
x forall a. [a] -> [a] -> [a]
++ String
")"
  show (NotElem k
k Exp (g k ())
x) = String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show k
k forall a. [a] -> [a] -> [a]
++ String
" ∉ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (g k ())
x forall a. [a] -> [a] -> [a]
++ String
")"
  show (Intersect Exp (f k v)
x Exp (g k u)
y) = String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (f k v)
x forall a. [a] -> [a] -> [a]
++ String
" ∩ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (g k u)
y forall a. [a] -> [a] -> [a]
++ String
")"
  show (SetDiff Exp (f k v)
x Exp (g k u)
y) = String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (f k v)
x forall a. [a] -> [a] -> [a]
++ String
" ➖ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (g k u)
y forall a. [a] -> [a] -> [a]
++ String
")"
  show (Subset Exp (f k v)
x Exp (g k u)
y) = String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (f k v)
x forall a. [a] -> [a] -> [a]
++ String
" ⊆ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (g k u)
y forall a. [a] -> [a] -> [a]
++ String
")"
  show (UnionOverrideLeft Exp (f k v)
x Exp (g k v)
y) = String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (f k v)
x forall a. [a] -> [a] -> [a]
++ String
" ∪ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (g k v)
y forall a. [a] -> [a] -> [a]
++ String
")"
  show (UnionPlus Exp (f k n)
x Exp (g k n)
y) = String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (f k n)
x forall a. [a] -> [a] -> [a]
++ String
" ∪+ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (g k n)
y forall a. [a] -> [a] -> [a]
++ String
")"
  show (UnionOverrideRight Exp (f k v)
x Exp (g k v)
y) = String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (f k v)
x forall a. [a] -> [a] -> [a]
++ String
" ⨃ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (g k v)
y forall a. [a] -> [a] -> [a]
++ String
")"
  show (Singleton k
_ v
_) = String
"(singleton _ _ )"
  show (SetSingleton k
_) = String
"(setSingleton _ )"
  show (KeyEqual Exp (f k v)
x Exp (g k u)
y) = String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (f k v)
x forall a. [a] -> [a] -> [a]
++ String
" ≍ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Exp (g k u)
y forall a. [a] -> [a] -> [a]
++ String
")"

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

-- | Basic types are those that can be tranformed into Exp.
-- The HasExp class, encodes how to lift a Basic type into an Exp.
-- The function 'toExp' will build a typed Exp for that Basic type.
-- This will be really usefull in the smart constructors.
class HasExp s t | s -> t where
  toExp :: s -> Exp t

-- | The simplest Base type is one that is already an Exp
instance HasExp (Exp t) t where
  toExp :: Exp t -> Exp t
toExp Exp t
x = Exp t
x

instance Ord k => HasExp (Map k v) (Map k v) where
  toExp :: Map k v -> Exp (Map k v)
toExp Map k v
x = forall f (b :: * -> * -> *) c.
(Ord f, Basic b, Iter b) =>
BaseRep b f c -> b f c -> Exp (b f c)
Base forall k v. Basic Map => BaseRep Map k v
MapR Map k v
x

instance Ord k => HasExp (Set.Set k) (Sett k ()) where
  toExp :: Set k -> Exp (Sett k ())
toExp Set k
x = forall f (b :: * -> * -> *) c.
(Ord f, Basic b, Iter b) =>
BaseRep b f c -> b f c -> Exp (b f c)
Base forall k. Basic Sett => BaseRep Sett k ()
SetR (forall k. Set k -> Sett k ()
Sett Set k
x)

instance Ord k => HasExp [(k, v)] (List k v) where
  toExp :: [(k, v)] -> Exp (List k v)
toExp [(k, v)]
l = forall f (b :: * -> * -> *) c.
(Ord f, Basic b, Iter b) =>
BaseRep b f c -> b f c -> Exp (b f c)
Base forall k v. Basic List => BaseRep List k v
ListR (forall k v. Ord k => [(k, v)] -> List k v
UnSafeList (forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\(k, v)
x (k, v)
y -> forall a. Ord a => a -> a -> Ordering
compare (forall a b. (a, b) -> a
fst (k, v)
x) (forall a b. (a, b) -> a
fst (k, v)
y)) [(k, v)]
l))

instance Ord k => HasExp (Single k v) (Single k v) where
  toExp :: Single k v -> Exp (Single k v)
toExp Single k v
x = forall f (b :: * -> * -> *) c.
(Ord f, Basic b, Iter b) =>
BaseRep b f c -> b f c -> Exp (b f c)
Base forall k v. Basic Single => BaseRep Single k v
SingleR Single k v
x

type OrdAll coin cred pool ptr k = (Ord k, Ord coin, Ord cred, Ord ptr, Ord pool)

-- =========================================================================================
-- When we build an Exp, we want to make sure all Sets with one element become (SetSingleton x)
-- so we use these 'smart' constructors.

dRestrict :: (Ord k, Iter g) => Exp (g k ()) -> Exp (f k v) -> Exp (f k v)
dRestrict :: forall k (g :: * -> * -> *) (f :: * -> * -> *) v.
(Ord k, Iter g) =>
Exp (g k ()) -> Exp (f k v) -> Exp (f k v)
dRestrict (Base BaseRep f k v
SetR (Sett Set k
x)) Exp (f k v)
y | forall a. Set a -> Int
Set.size Set k
x forall a. Eq a => a -> a -> Bool
== Int
1 = forall k (g :: * -> * -> *) (f :: * -> * -> *) v.
(Ord k, Iter g) =>
Exp (g k ()) -> Exp (f k v) -> Exp (f k v)
DRestrict (forall f. Ord f => f -> Exp (Single f ())
SetSingleton (forall a. Int -> Set a -> a
Set.elemAt Int
0 Set k
x)) Exp (f k v)
y
dRestrict Exp (g k ())
x Exp (f k v)
y = forall k (g :: * -> * -> *) (f :: * -> * -> *) v.
(Ord k, Iter g) =>
Exp (g k ()) -> Exp (f k v) -> Exp (f k v)
DRestrict Exp (g k ())
x Exp (f k v)
y

rRestrict :: (Ord k, Iter g, Ord v) => Exp (f k v) -> Exp (g v ()) -> Exp (f k v)
rRestrict :: forall k (g :: * -> * -> *) v (f :: * -> * -> *).
(Ord k, Iter g, Ord v) =>
Exp (f k v) -> Exp (g v ()) -> Exp (f k v)
rRestrict Exp (f k v)
y (Base BaseRep f k v
SetR (Sett Set k
x)) | forall a. Set a -> Int
Set.size Set k
x forall a. Eq a => a -> a -> Bool
== Int
1 = forall k (g :: * -> * -> *) v (f :: * -> * -> *).
(Ord k, Iter g, Ord v) =>
Exp (f k v) -> Exp (g v ()) -> Exp (f k v)
RRestrict Exp (f k v)
y (forall f. Ord f => f -> Exp (Single f ())
SetSingleton (forall a. Int -> Set a -> a
Set.elemAt Int
0 Set k
x))
rRestrict Exp (f k v)
y Exp (g v ())
x = forall k (g :: * -> * -> *) v (f :: * -> * -> *).
(Ord k, Iter g, Ord v) =>
Exp (f k v) -> Exp (g v ()) -> Exp (f k v)
RRestrict Exp (f k v)
y Exp (g v ())
x

dExclude :: (Ord k, Iter g) => Exp (g k ()) -> Exp (f k v) -> Exp (f k v)
dExclude :: forall k (g :: * -> * -> *) (f :: * -> * -> *) v.
(Ord k, Iter g) =>
Exp (g k ()) -> Exp (f k v) -> Exp (f k v)
dExclude (Base BaseRep f k v
SetR (Sett Set k
x)) Exp (f k v)
y | forall a. Set a -> Int
Set.size Set k
x forall a. Eq a => a -> a -> Bool
== Int
1 = forall k (g :: * -> * -> *) (f :: * -> * -> *) v.
(Ord k, Iter g) =>
Exp (g k ()) -> Exp (f k v) -> Exp (f k v)
DExclude (forall f. Ord f => f -> Exp (Single f ())
SetSingleton (forall a. Int -> Set a -> a
Set.elemAt Int
0 Set k
x)) Exp (f k v)
y
dExclude Exp (g k ())
x Exp (f k v)
y = forall k (g :: * -> * -> *) (f :: * -> * -> *) v.
(Ord k, Iter g) =>
Exp (g k ()) -> Exp (f k v) -> Exp (f k v)
DExclude Exp (g k ())
x Exp (f k v)
y

rExclude :: (Ord k, Iter g, Ord v) => Exp (f k v) -> Exp (g v ()) -> Exp (f k v)
rExclude :: forall k (g :: * -> * -> *) v (f :: * -> * -> *).
(Ord k, Iter g, Ord v) =>
Exp (f k v) -> Exp (g v ()) -> Exp (f k v)
rExclude Exp (f k v)
y (Base BaseRep f k v
SetR (Sett Set k
x)) | forall a. Set a -> Int
Set.size Set k
x forall a. Eq a => a -> a -> Bool
== Int
1 = forall k (g :: * -> * -> *) v (f :: * -> * -> *).
(Ord k, Iter g, Ord v) =>
Exp (f k v) -> Exp (g v ()) -> Exp (f k v)
RExclude Exp (f k v)
y (forall f. Ord f => f -> Exp (Single f ())
SetSingleton (forall a. Int -> Set a -> a
Set.elemAt Int
0 Set k
x))
rExclude Exp (f k v)
y Exp (g v ())
x = forall k (g :: * -> * -> *) v (f :: * -> * -> *).
(Ord k, Iter g, Ord v) =>
Exp (f k v) -> Exp (g v ()) -> Exp (f k v)
RExclude Exp (f k v)
y Exp (g v ())
x

-- ==========================================================================================
-- Smart constructors build typed Exp with real values at the leaves (the Base constuctor)

-- setoperators

-- (⊆),
-- (∩),

-- | domain of a map or element type of a set.
dom :: (Ord k, HasExp s (f k v)) => s -> Exp (Sett k ())
dom :: forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom s
x = forall f (b :: * -> * -> *) c.
Ord f =>
Exp (b f c) -> Exp (Sett f ())
Dom (forall s t. HasExp s t => s -> Exp t
toExp s
x)

-- | range of a map or () for a set.
rng :: (Ord k, Ord v) => HasExp s (f k v) => s -> Exp (Sett v ())
rng :: forall k v s (f :: * -> * -> *).
(Ord k, Ord v, HasExp s (f k v)) =>
s -> Exp (Sett v ())
rng s
x = forall f b (c :: * -> * -> *).
(Ord f, Ord b) =>
Exp (c f b) -> Exp (Sett b ())
Rng (forall s t. HasExp s t => s -> Exp t
toExp s
x)

-- | domain restrict.
(◁), (<|), drestrict :: (Ord k, HasExp s1 (Sett k ()), HasExp s2 (f k v)) => s1 -> s2 -> Exp (f k v)
◁ :: forall k s1 s2 (f :: * -> * -> *) v.
(Ord k, HasExp s1 (Sett k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
(◁) s1
x s2
y = forall k (g :: * -> * -> *) (f :: * -> * -> *) v.
(Ord k, Iter g) =>
Exp (g k ()) -> Exp (f k v) -> Exp (f k v)
dRestrict (forall s t. HasExp s t => s -> Exp t
toExp s1
x) (forall s t. HasExp s t => s -> Exp t
toExp s2
y)
drestrict :: forall k s1 s2 (f :: * -> * -> *) v.
(Ord k, HasExp s1 (Sett k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
drestrict = forall k s1 s2 (f :: * -> * -> *) v.
(Ord k, HasExp s1 (Sett k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
(◁)
<| :: forall k s1 s2 (f :: * -> * -> *) v.
(Ord k, HasExp s1 (Sett k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
(<|) = forall k s1 s2 (f :: * -> * -> *) v.
(Ord k, HasExp s1 (Sett k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
drestrict

-- | domain exclude
(⋪), dexclude :: (Ord k, Iter g, HasExp s1 (g k ()), HasExp s2 (f k v)) => s1 -> s2 -> Exp (f k v)
⋪ :: forall k (g :: * -> * -> *) s1 s2 (f :: * -> * -> *) v.
(Ord k, Iter g, HasExp s1 (g k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
(⋪) s1
x s2
y = forall k (g :: * -> * -> *) (f :: * -> * -> *) v.
(Ord k, Iter g) =>
Exp (g k ()) -> Exp (f k v) -> Exp (f k v)
dExclude (forall s t. HasExp s t => s -> Exp t
toExp s1
x) (forall s t. HasExp s t => s -> Exp t
toExp s2
y)
dexclude :: forall k (g :: * -> * -> *) s1 s2 (f :: * -> * -> *) v.
(Ord k, Iter g, HasExp s1 (g k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
dexclude = forall k (g :: * -> * -> *) s1 s2 (f :: * -> * -> *) v.
(Ord k, Iter g, HasExp s1 (g k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
(⋪)

-- | range restrict
(▷)
  , (|>)
  , rrestrict ::
    (Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) => s1 -> s2 -> Exp (f k v)
▷ :: forall k (g :: * -> * -> *) v s1 (f :: * -> * -> *) s2.
(Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) =>
s1 -> s2 -> Exp (f k v)
(▷) s1
x s2
y = forall k (g :: * -> * -> *) v (f :: * -> * -> *).
(Ord k, Iter g, Ord v) =>
Exp (f k v) -> Exp (g v ()) -> Exp (f k v)
rRestrict (forall s t. HasExp s t => s -> Exp t
toExp s1
x) (forall s t. HasExp s t => s -> Exp t
toExp s2
y)
rrestrict :: forall k (g :: * -> * -> *) v s1 (f :: * -> * -> *) s2.
(Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) =>
s1 -> s2 -> Exp (f k v)
rrestrict = forall k (g :: * -> * -> *) v s1 (f :: * -> * -> *) s2.
(Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) =>
s1 -> s2 -> Exp (f k v)
(▷)
|> :: forall k (g :: * -> * -> *) v s1 (f :: * -> * -> *) s2.
(Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) =>
s1 -> s2 -> Exp (f k v)
(|>) = forall k (g :: * -> * -> *) v s1 (f :: * -> * -> *) s2.
(Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) =>
s1 -> s2 -> Exp (f k v)
(▷)

-- | range exclude
(⋫)
  , rexclude ::
    (Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) => s1 -> s2 -> Exp (f k v)
⋫ :: forall k (g :: * -> * -> *) v s1 (f :: * -> * -> *) s2.
(Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) =>
s1 -> s2 -> Exp (f k v)
(⋫) s1
x s2
y = forall k (g :: * -> * -> *) v (f :: * -> * -> *).
(Ord k, Iter g, Ord v) =>
Exp (f k v) -> Exp (g v ()) -> Exp (f k v)
rExclude (forall s t. HasExp s t => s -> Exp t
toExp s1
x) (forall s t. HasExp s t => s -> Exp t
toExp s2
y)
rexclude :: forall k (g :: * -> * -> *) v s1 (f :: * -> * -> *) s2.
(Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) =>
s1 -> s2 -> Exp (f k v)
rexclude = forall k (g :: * -> * -> *) v s1 (f :: * -> * -> *) s2.
(Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) =>
s1 -> s2 -> Exp (f k v)
(⋫)

-- | element of the domain
(∈) :: (Show k, Ord k, Iter g, HasExp s (g k ())) => k -> s -> Exp Bool
∈ :: forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
(∈) k
x s
y = forall f (b :: * -> * -> *).
(Ord f, Iter b, Show f) =>
f -> Exp (b f ()) -> Exp Bool
Elem k
x (forall s t. HasExp s t => s -> Exp t
toExp s
y)

-- | not an element of the domain
(∉), notelem :: (Show k, Ord k, Iter g, HasExp s (g k ())) => k -> s -> Exp Bool
∉ :: forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
(∉) k
x s
y = forall f (b :: * -> * -> *).
(Ord f, Iter b, Show f) =>
f -> Exp (b f ()) -> Exp Bool
NotElem k
x (forall s t. HasExp s t => s -> Exp t
toExp s
y)
notelem :: forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
notelem = forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
(∉)

-- | union two maps or sets. In the case of a map, keep the pair from the left, if the two have common keys.
(∪)
  , unionleft ::
    (Show k, Show v, Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) => s1 -> s2 -> Exp (f k v)
∪ :: forall k v s1 (f :: * -> * -> *) s2 (g :: * -> * -> *).
(Show k, Show v, Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) =>
s1 -> s2 -> Exp (f k v)
(∪) s1
x s2
y = forall f b (c :: * -> * -> *) (a :: * -> * -> *).
(Show f, Show b, Ord f) =>
Exp (c f b) -> Exp (a f b) -> Exp (c f b)
UnionOverrideLeft (forall s t. HasExp s t => s -> Exp t
toExp s1
x) (forall s t. HasExp s t => s -> Exp t
toExp s2
y)
unionleft :: forall k v s1 (f :: * -> * -> *) s2 (g :: * -> * -> *).
(Show k, Show v, Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) =>
s1 -> s2 -> Exp (f k v)
unionleft = forall k v s1 (f :: * -> * -> *) s2 (g :: * -> * -> *).
(Show k, Show v, Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) =>
s1 -> s2 -> Exp (f k v)
(∪)

-- | union two maps or sets. In the case of a map, keep the pair from the right, if the two have common keys.
(⨃), unionright :: (Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) => s1 -> s2 -> Exp (f k v)
⨃ :: forall k s1 (f :: * -> * -> *) v s2 (g :: * -> * -> *).
(Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) =>
s1 -> s2 -> Exp (f k v)
(⨃) s1
x s2
y = forall f (b :: * -> * -> *) c (a :: * -> * -> *).
Ord f =>
Exp (b f c) -> Exp (a f c) -> Exp (b f c)
UnionOverrideRight (forall s t. HasExp s t => s -> Exp t
toExp s1
x) (forall s t. HasExp s t => s -> Exp t
toExp s2
y)
unionright :: forall k s1 (f :: * -> * -> *) v s2 (g :: * -> * -> *).
(Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) =>
s1 -> s2 -> Exp (f k v)
unionright = forall k s1 (f :: * -> * -> *) v s2 (g :: * -> * -> *).
(Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) =>
s1 -> s2 -> Exp (f k v)
(⨃)

-- | union two maps or sets. In the case of a map, combine values with monoid (<>), if the two have common keys.
(∪+)
  , unionplus ::
    (Ord k, Monoid n, HasExp s1 (f k n), HasExp s2 (g k n)) => s1 -> s2 -> Exp (f k n)
∪+ :: forall k n s1 (f :: * -> * -> *) s2 (g :: * -> * -> *).
(Ord k, Monoid n, HasExp s1 (f k n), HasExp s2 (g k n)) =>
s1 -> s2 -> Exp (f k n)
(∪+) s1
x s2
y = forall f b (c :: * -> * -> *) (a :: * -> * -> *).
(Ord f, Monoid b) =>
Exp (c f b) -> Exp (a f b) -> Exp (c f b)
UnionPlus (forall s t. HasExp s t => s -> Exp t
toExp s1
x) (forall s t. HasExp s t => s -> Exp t
toExp s2
y)
unionplus :: forall k n s1 (f :: * -> * -> *) s2 (g :: * -> * -> *).
(Ord k, Monoid n, HasExp s1 (f k n), HasExp s2 (g k n)) =>
s1 -> s2 -> Exp (f k n)
unionplus = forall k n s1 (f :: * -> * -> *) s2 (g :: * -> * -> *).
(Ord k, Monoid n, HasExp s1 (f k n), HasExp s2 (g k n)) =>
s1 -> s2 -> Exp (f k n)
(∪+)

-- | create a singleton map.
singleton :: Ord k => k -> v -> Exp (Single k v)
singleton :: forall k v. Ord k => k -> v -> Exp (Single k v)
singleton k
k v
v = forall k v. Ord k => k -> v -> Exp (Single k v)
Singleton k
k v
v

-- | create a singleton set.
setSingleton :: Ord k => k -> Exp (Single k ())
setSingleton :: forall f. Ord f => f -> Exp (Single f ())
setSingleton k
k = forall f. Ord f => f -> Exp (Single f ())
SetSingleton k
k

-- | intersect two sets, or the intersection of the domain of two maps.
(∩)
  , intersect ::
    (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) => s1 -> s2 -> Exp (Sett k ())
∩ :: forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp (Sett k ())
(∩) s1
x s2
y = forall f (b :: * -> * -> *) (c :: * -> * -> *) a t.
(Ord f, Iter b, Iter c) =>
Exp (b f a) -> Exp (c f t) -> Exp (Sett f ())
Intersect (forall s t. HasExp s t => s -> Exp t
toExp s1
x) (forall s t. HasExp s t => s -> Exp t
toExp s2
y)
intersect :: forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp (Sett k ())
intersect = forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp (Sett k ())
(∩)

-- | @(subset x y)@. is the domain of @x@ a subset of the domain of @y@.
(⊆), subset :: (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) => s1 -> s2 -> Exp Bool
⊆ :: forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp Bool
(⊆) s1
x s2
y = forall f (b :: * -> * -> *) (c :: * -> * -> *) a t.
(Ord f, Iter b, Iter c) =>
Exp (b f a) -> Exp (c f t) -> Exp Bool
Subset (forall s t. HasExp s t => s -> Exp t
toExp s1
x) (forall s t. HasExp s t => s -> Exp t
toExp s2
y)
subset :: forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp Bool
subset = forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp Bool
(⊆)

-- | @(x ➖ y)@ Everything in @x@ except for those pairs in @x@ where the domain of @x@ is an element of the domain of @y@.
(➖)
  , setdiff ::
    (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) => s1 -> s2 -> Exp (f k v)
➖ :: forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp (f k v)
(➖) s1
x s2
y = forall f (b :: * -> * -> *) (c :: * -> * -> *) a t.
(Ord f, Iter b, Iter c) =>
Exp (b f a) -> Exp (c f t) -> Exp (b f a)
SetDiff (forall s t. HasExp s t => s -> Exp t
toExp s1
x) (forall s t. HasExp s t => s -> Exp t
toExp s2
y)
setdiff :: forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp (f k v)
setdiff = forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp (f k v)
(➖)

-- | Do two maps (or sets) have exactly the same domain.
(≍), keyeq :: (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) => s1 -> s2 -> Exp Bool
≍ :: forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp Bool
(≍) s1
x s2
y = forall f (b :: * -> * -> *) (c :: * -> * -> *) a t.
(Ord f, Iter b, Iter c) =>
Exp (b f a) -> Exp (c f t) -> Exp Bool
KeyEqual (forall s t. HasExp s t => s -> Exp t
toExp s1
x) (forall s t. HasExp s t => s -> Exp t
toExp s2
y)
keyeq :: forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp Bool
keyeq = forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp Bool
(≍)

-- ==========================================================================================
-- Part 2. Symbolic functions
-- ===========================================================================================

-- | An symbolic function Fun has two parts, a Lam that can be analyzed, and real function that can be applied
data Fun t = Fun (Lam t) t

-- | We can observe a Fun by showing the Lam part.
instance Show (Fun t) where
  show :: Fun t -> String
show (Fun Lam t
lam t
_fun) = forall a. Show a => a -> String
show Lam t
lam

-- | Symbolc functions (Fun) are data, that can be pattern matched over. They
-- 1) Represent a wide class of binary functions that are used in translating the SetAlgebra
-- 2) Turned into a String so they can be printed
-- 3) Turned into the function they represent.
-- 4) Composed into bigger functions
-- 5) Symbolically symplified
-- Here  we implement Symbolic Binary functions with upto 4 variables, which is enough for this use
-- =================================================================================================
data Pat env t where
  P1 :: Pat (d, c, b, a) d
  P2 :: Pat (d, c, b, a) c
  P3 :: Pat (d, c, b, a) b
  P4 :: Pat (d, c, b, a) a
  PPair :: Pat (d, c, b, a) a -> Pat (d, c, b, a) b -> Pat (d, c, b, a) (a, b)

data Expr env t where
  X1 :: Expr (d, c, b, a) d
  X2 :: Expr (d, c, b, a) c
  X3 :: Expr (d, c, b, a) b
  X4 :: Expr (d, c, b, a) a
  HasKey :: (Iter f, Ord k) => Expr e k -> (f k v) -> Expr e Bool
  Neg :: Expr e Bool -> Expr e Bool
  Ap :: Lam (a -> b -> c) -> Expr e a -> Expr e b -> Expr e c
  EPair :: Expr e a -> Expr e b -> Expr e (a, b)
  FST :: Expr e (a, b) -> Expr e a
  SND :: Expr e (a, b) -> Expr e b
  Lit :: Show t => t -> Expr env t

-- | A typed deep embedding of Haskell functions with type @t@.
--   Be carefull, no pattern P1, P2, P3, P4 should appear MORE THAN ONCE in a Lam.
data Lam t where
  Lam :: Pat (d, c, b, a) t -> Pat (d, c, b, a) s -> Expr (d, c, b, a) v -> Lam (t -> s -> v)
  Add :: Num n => Lam (n -> n -> n)
  Cat :: Monoid m => Lam (m -> m -> m)
  Eql :: Eq t => Lam (t -> t -> Bool)
  Both :: Lam (Bool -> Bool -> Bool)
  Lift :: (a -> b -> c) -> Lam (a -> b -> c) -- For use n the tests only!

-- ============= Printing in 𝜷-Normal Form =========================

type StringEnv = (String, String, String, String)

bindE :: Pat (a, b, c, d) t -> Expr (w, x, y, z) t -> StringEnv -> StringEnv
bindE :: forall a b c d t w x y z.
Pat (a, b, c, d) t -> Expr (w, x, y, z) t -> StringEnv -> StringEnv
bindE Pat (a, b, c, d) t
P1 Expr (w, x, y, z) t
v (e :: StringEnv
e@(String
_, String
c, String
b, String
a)) = (forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE StringEnv
e Expr (w, x, y, z) t
v, String
c, String
b, String
a)
bindE Pat (a, b, c, d) t
P2 Expr (w, x, y, z) t
v (e :: StringEnv
e@(String
d, String
_, String
b, String
a)) = (String
d, forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE StringEnv
e Expr (w, x, y, z) t
v, String
b, String
a)
bindE Pat (a, b, c, d) t
P3 Expr (w, x, y, z) t
v (e :: StringEnv
e@(String
d, String
c, String
_, String
a)) = (String
d, String
c, forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE StringEnv
e Expr (w, x, y, z) t
v, String
a)
bindE Pat (a, b, c, d) t
P4 Expr (w, x, y, z) t
v (e :: StringEnv
e@(String
d, String
c, String
b, String
_)) = (String
d, String
c, String
b, forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE StringEnv
e Expr (w, x, y, z) t
v)
bindE (PPair Pat (d, c, b, a) a
p1 Pat (d, c, b, a) b
p2) (EPair Expr (w, x, y, z) a
e1 Expr (w, x, y, z) b
e2) StringEnv
env = forall a b c d t w x y z.
Pat (a, b, c, d) t -> Expr (w, x, y, z) t -> StringEnv -> StringEnv
bindE Pat (d, c, b, a) a
p1 Expr (w, x, y, z) a
e1 (forall a b c d t w x y z.
Pat (a, b, c, d) t -> Expr (w, x, y, z) t -> StringEnv -> StringEnv
bindE Pat (d, c, b, a) b
p2 Expr (w, x, y, z) b
e2 StringEnv
env)
bindE (PPair Pat (d, c, b, a) a
p1 Pat (d, c, b, a) b
p2) Expr (w, x, y, z) t
e StringEnv
env = forall a b c d t w x y z.
Pat (a, b, c, d) t -> Expr (w, x, y, z) t -> StringEnv -> StringEnv
bindE Pat (d, c, b, a) b
p2 (forall e f b. Expr e (f, b) -> Expr e b
SND Expr (w, x, y, z) t
e) (forall a b c d t w x y z.
Pat (a, b, c, d) t -> Expr (w, x, y, z) t -> StringEnv -> StringEnv
bindE Pat (d, c, b, a) a
p1 (forall e a f. Expr e (a, f) -> Expr e a
FST Expr (w, x, y, z) t
e) StringEnv
env)

showE :: StringEnv -> (Expr (a, b, c, d) t) -> String
showE :: forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE (String
x, String
_, String
_, String
_) Expr (a, b, c, d) t
X1 = String
x
showE (String
_, String
y, String
_, String
_) Expr (a, b, c, d) t
X2 = String
y
showE (String
_, String
_, String
z, String
_) Expr (a, b, c, d) t
X3 = String
z
showE (String
_, String
_, String
_, String
w) Expr (a, b, c, d) t
X4 = String
w
showE StringEnv
e (EPair Expr (a, b, c, d) a
a Expr (a, b, c, d) b
b) = String
"(" forall a. [a] -> [a] -> [a]
++ forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE StringEnv
e Expr (a, b, c, d) a
a forall a. [a] -> [a] -> [a]
++ String
"," forall a. [a] -> [a] -> [a]
++ forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE StringEnv
e Expr (a, b, c, d) b
b forall a. [a] -> [a] -> [a]
++ String
")"
showE StringEnv
e (Ap (Lam Pat (d, c, b, a) t
p1 Pat (d, c, b, a) s
p2 Expr (d, c, b, a) v
expr) Expr (a, b, c, d) a
x Expr (a, b, c, d) b
y) = forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE (forall a b c d t w x y z.
Pat (a, b, c, d) t -> Expr (w, x, y, z) t -> StringEnv -> StringEnv
bindE Pat (d, c, b, a) s
p2 Expr (a, b, c, d) b
y (forall a b c d t w x y z.
Pat (a, b, c, d) t -> Expr (w, x, y, z) t -> StringEnv -> StringEnv
bindE Pat (d, c, b, a) t
p1 Expr (a, b, c, d) a
x StringEnv
e)) Expr (d, c, b, a) v
expr
showE StringEnv
e (FST Expr (a, b, c, d) (t, b)
f) = String
"(fst " forall a. [a] -> [a] -> [a]
++ forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE StringEnv
e Expr (a, b, c, d) (t, b)
f forall a. [a] -> [a] -> [a]
++ String
")"
showE StringEnv
e (SND Expr (a, b, c, d) (a, t)
f) = String
"(snd " forall a. [a] -> [a] -> [a]
++ forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE StringEnv
e Expr (a, b, c, d) (a, t)
f forall a. [a] -> [a] -> [a]
++ String
")"
showE StringEnv
e (Ap Lam (a -> b -> t)
oper Expr (a, b, c, d) a
a Expr (a, b, c, d) b
b) = String
"(" forall a. [a] -> [a] -> [a]
++ forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE StringEnv
e Expr (a, b, c, d) a
a forall a. [a] -> [a] -> [a]
++ forall t. StringEnv -> Lam t -> String
showL StringEnv
e Lam (a -> b -> t)
oper forall a. [a] -> [a] -> [a]
++ forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE StringEnv
e Expr (a, b, c, d) b
b forall a. [a] -> [a] -> [a]
++ String
")"
showE StringEnv
e (HasKey Expr (a, b, c, d) k
k f k v
_datum) = String
"(haskey " forall a. [a] -> [a] -> [a]
++ forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE StringEnv
e Expr (a, b, c, d) k
k forall a. [a] -> [a] -> [a]
++ String
" ?)"
showE StringEnv
e (Neg Expr (a, b, c, d) Bool
x) = String
"(not " forall a. [a] -> [a] -> [a]
++ forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE StringEnv
e Expr (a, b, c, d) Bool
x forall a. [a] -> [a] -> [a]
++ String
")"
showE StringEnv
_ (Lit t
n) = forall a. Show a => a -> String
show t
n

showL :: StringEnv -> Lam t -> String
showL :: forall t. StringEnv -> Lam t -> String
showL StringEnv
e (Lam Pat (d, c, b, a) t
p1 Pat (d, c, b, a) s
p2 Expr (d, c, b, a) v
expr) = String
"\\ " forall a. [a] -> [a] -> [a]
++ forall any t. StringEnv -> Pat any t -> String
showP StringEnv
e Pat (d, c, b, a) t
p1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall any t. StringEnv -> Pat any t -> String
showP StringEnv
e Pat (d, c, b, a) s
p2 forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE StringEnv
e Expr (d, c, b, a) v
expr
showL StringEnv
_e Lam t
Add = String
" + "
showL StringEnv
_e Lam t
Cat = String
" <> "
showL StringEnv
_e Lam t
Eql = String
" == "
showL StringEnv
_e Lam t
Both = String
" && "
showL StringEnv
_e (Lift a -> b -> c
_f) = String
"<lifted function>"

showP :: StringEnv -> (Pat any t) -> String
showP :: forall any t. StringEnv -> Pat any t -> String
showP (String
x, String
_, String
_, String
_) Pat any t
P1 = String
x
showP (String
_, String
y, String
_, String
_) Pat any t
P2 = String
y
showP (String
_, String
_, String
z, String
_) Pat any t
P3 = String
z
showP (String
_, String
_, String
_, String
w) Pat any t
P4 = String
w
showP StringEnv
env (PPair Pat (d, c, b, a) a
p1 Pat (d, c, b, a) b
p2) = String
"(" forall a. [a] -> [a] -> [a]
++ forall any t. StringEnv -> Pat any t -> String
showP StringEnv
env Pat (d, c, b, a) a
p1 forall a. [a] -> [a] -> [a]
++ String
"," forall a. [a] -> [a] -> [a]
++ forall any t. StringEnv -> Pat any t -> String
showP StringEnv
env Pat (d, c, b, a) b
p2 forall a. [a] -> [a] -> [a]
++ String
")"

-- turn an Expr into a String
instance Show (Expr (a, b, c, d) t) where
  show :: Expr (a, b, c, d) t -> String
show Expr (a, b, c, d) t
x = forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE (String
"X1", String
"X2", String
"X3", String
"X4") Expr (a, b, c, d) t
x

-- turn a @Lam@ into a String.
instance Show (Lam t) where
  show :: Lam t -> String
show Lam t
x = forall t. StringEnv -> Lam t -> String
showL (String
"X1", String
"X2", String
"X3", String
"X4") Lam t
x

-- ======================================================================================
-- Operations we use to manipulate Fun. Some simple ones, and some ways to compose them.
-- The great thing is the types completely decide what the operations do.
-- ======================================================================================

-- Used in projectStep, chainStep, andPStep, orStep and guardStep
apply :: Fun t -> t
apply :: forall t. Fun t -> t
apply (Fun Lam t
_e t
f) = t
f

-- Used in compile (UnionOverrideLeft case)
first :: Fun (v -> s -> v)
first :: forall v s. Fun (v -> s -> v)
first = forall t. Lam t -> t -> Fun t
Fun (forall f b c a t s v.
Pat (f, b, c, a) t
-> Pat (f, b, c, a) s -> Expr (f, b, c, a) v -> Lam (t -> s -> v)
Lam forall d f b c. Pat (d, f, b, c) d
P1 forall f c b c. Pat (f, c, b, c) c
P2 forall d f b c. Expr (d, f, b, c) d
X1) (\v
x s
_y -> v
x)

-- Used in compile (UnionOverrideRight case)
second :: Fun (v -> s -> s)
second :: forall v s. Fun (v -> s -> s)
second = forall t. Lam t -> t -> Fun t
Fun (forall f b c a t s v.
Pat (f, b, c, a) t
-> Pat (f, b, c, a) s -> Expr (f, b, c, a) v -> Lam (t -> s -> v)
Lam forall d f b c. Pat (d, f, b, c) d
P1 forall f c b c. Pat (f, c, b, c) c
P2 forall f c b c. Expr (f, c, b, c) c
X2) (\v
_x s
y -> s
y)

-- Used in compile (UnionPlus case)
plus :: Monoid t => Fun (t -> t -> t)
plus :: forall t. Monoid t => Fun (t -> t -> t)
plus = (forall t. Lam t -> t -> Fun t
Fun forall f. Monoid f => Lam (f -> f -> f)
Cat forall a. Semigroup a => a -> a -> a
(<>))

eql :: Eq t => Fun (t -> t -> Bool)
eql :: forall t. Eq t => Fun (t -> t -> Bool)
eql = (forall t. Lam t -> t -> Fun t
Fun forall f. Eq f => Lam (f -> f -> Bool)
Eql forall a. Eq a => a -> a -> Bool
(==))

constant :: Show c => c -> Fun (a -> b -> c)
constant :: forall c a b. Show c => c -> Fun (a -> b -> c)
constant c
c = forall t. Lam t -> t -> Fun t
Fun (forall f b c a t s v.
Pat (f, b, c, a) t
-> Pat (f, b, c, a) s -> Expr (f, b, c, a) v -> Lam (t -> s -> v)
Lam forall d f b c. Pat (d, f, b, c) d
P1 forall f c b c. Pat (f, c, b, c) c
P2 (forall t env. Show t => t -> Expr env t
Lit c
c)) (\a
_x b
_y -> c
c)

-- Used in compile (RExclude RRestrict cases)
rngElem :: (Ord rng, Iter f) => f rng v -> Fun (dom -> rng -> Bool)
rngElem :: forall rng (f :: * -> * -> *) v dom.
(Ord rng, Iter f) =>
f rng v -> Fun (dom -> rng -> Bool)
rngElem f rng v
realset = forall t. Lam t -> t -> Fun t
Fun (forall f b c a t s v.
Pat (f, b, c, a) t
-> Pat (f, b, c, a) s -> Expr (f, b, c, a) v -> Lam (t -> s -> v)
Lam forall d f b c. Pat (d, f, b, c) d
P1 forall f c b c. Pat (f, c, b, c) c
P2 (forall (f :: * -> * -> *) b e c.
(Iter f, Ord b) =>
Expr e b -> f b c -> Expr e Bool
HasKey forall f c b c. Expr (f, c, b, c) c
X2 f rng v
realset)) (\dom
_x rng
y -> forall (f :: * -> * -> *) key b.
(Iter f, Ord key) =>
key -> f key b -> Bool
haskey rng
y f rng v
realset) -- x is ignored and realset is supplied

domElem :: (Ord dom, Iter f) => f dom v -> Fun (dom -> rng -> Bool)
domElem :: forall dom (f :: * -> * -> *) v rng.
(Ord dom, Iter f) =>
f dom v -> Fun (dom -> rng -> Bool)
domElem f dom v
realset = forall t. Lam t -> t -> Fun t
Fun (forall f b c a t s v.
Pat (f, b, c, a) t
-> Pat (f, b, c, a) s -> Expr (f, b, c, a) v -> Lam (t -> s -> v)
Lam forall d f b c. Pat (d, f, b, c) d
P1 forall f c b c. Pat (f, c, b, c) c
P2 (forall (f :: * -> * -> *) b e c.
(Iter f, Ord b) =>
Expr e b -> f b c -> Expr e Bool
HasKey forall d f b c. Expr (d, f, b, c) d
X1 f dom v
realset)) (\dom
x rng
_y -> forall (f :: * -> * -> *) key b.
(Iter f, Ord key) =>
key -> f key b -> Bool
haskey dom
x f dom v
realset) -- y is ignored and realset is supplied

rngFst :: Fun (x -> (a, b) -> a)
rngFst :: forall x a b. Fun (x -> (a, b) -> a)
rngFst = forall t. Lam t -> t -> Fun t
Fun (forall f b c a t s v.
Pat (f, b, c, a) t
-> Pat (f, b, c, a) s -> Expr (f, b, c, a) v -> Lam (t -> s -> v)
Lam forall d f b c. Pat (d, f, b, c) d
P1 (forall f b c a.
Pat (f, b, c, a) a -> Pat (f, b, c, a) c -> Pat (f, b, c, a) (a, c)
PPair forall f c b c. Pat (f, c, b, c) c
P2 forall f b b c. Pat (f, b, b, c) b
P3) forall f c b c. Expr (f, c, b, c) c
X2) (\x
_x (a
a, b
_b) -> a
a)

rngSnd :: Fun (x -> (a, b) -> b)
rngSnd :: forall x a b. Fun (x -> (a, b) -> b)
rngSnd = forall t. Lam t -> t -> Fun t
Fun (forall f b c a t s v.
Pat (f, b, c, a) t
-> Pat (f, b, c, a) s -> Expr (f, b, c, a) v -> Lam (t -> s -> v)
Lam forall d f b c. Pat (d, f, b, c) d
P1 (forall f b c a.
Pat (f, b, c, a) a -> Pat (f, b, c, a) c -> Pat (f, b, c, a) (a, c)
PPair forall f c b c. Pat (f, c, b, c) c
P2 forall f b b c. Pat (f, b, b, c) b
P3) forall f b b c. Expr (f, b, b, c) b
X3) (\x
_x (a, b)
y -> forall a b. (a, b) -> b
snd (a, b)
y)

compose1 :: Fun (t1 -> t2 -> t3) -> Fun (t1 -> t4 -> t2) -> Fun (t1 -> t4 -> t3)
compose1 :: forall t1 t2 t3 t4.
Fun (t1 -> t2 -> t3)
-> Fun (t1 -> t4 -> t2) -> Fun (t1 -> t4 -> t3)
compose1 (Fun Lam (t1 -> t2 -> t3)
e1 t1 -> t2 -> t3
f1) (Fun Lam (t1 -> t4 -> t2)
e2 t1 -> t4 -> t2
f2) = forall t. Lam t -> t -> Fun t
Fun (forall f b c a t s v.
Pat (f, b, c, a) t
-> Pat (f, b, c, a) s -> Expr (f, b, c, a) v -> Lam (t -> s -> v)
Lam forall d f b c. Pat (d, f, b, c) d
P1 forall f c b c. Pat (f, c, b, c) c
P2 (forall f b c e.
Lam (f -> b -> c) -> Expr e f -> Expr e b -> Expr e c
Ap Lam (t1 -> t2 -> t3)
e1 forall d f b c. Expr (d, f, b, c) d
X1 (forall f b c e.
Lam (f -> b -> c) -> Expr e f -> Expr e b -> Expr e c
Ap Lam (t1 -> t4 -> t2)
e2 forall d f b c. Expr (d, f, b, c) d
X1 forall f c b c. Expr (f, c, b, c) c
X2))) (\t1
a t4
b -> t1 -> t2 -> t3
f1 t1
a (t1 -> t4 -> t2
f2 t1
a t4
b))

compSndL :: Fun (k -> (a, b) -> c) -> Fun (k -> d -> a) -> Fun (k -> (d, b) -> c)
compSndL :: forall k a b c d.
Fun (k -> (a, b) -> c)
-> Fun (k -> d -> a) -> Fun (k -> (d, b) -> c)
compSndL (Fun Lam (k -> (a, b) -> c)
m k -> (a, b) -> c
mf) (Fun Lam (k -> d -> a)
g k -> d -> a
mg) = forall t. Lam t -> t -> Fun t
Fun (forall f b c a t s v.
Pat (f, b, c, a) t
-> Pat (f, b, c, a) s -> Expr (f, b, c, a) v -> Lam (t -> s -> v)
Lam forall d f b c. Pat (d, f, b, c) d
P1 (forall f b c a.
Pat (f, b, c, a) a -> Pat (f, b, c, a) c -> Pat (f, b, c, a) (a, c)
PPair forall f c b c. Pat (f, c, b, c) c
P2 forall f b b c. Pat (f, b, b, c) b
P3) (forall f b c e.
Lam (f -> b -> c) -> Expr e f -> Expr e b -> Expr e c
Ap Lam (k -> (a, b) -> c)
m forall d f b c. Expr (d, f, b, c) d
X1 (forall e f b. Expr e f -> Expr e b -> Expr e (f, b)
EPair (forall f b c e.
Lam (f -> b -> c) -> Expr e f -> Expr e b -> Expr e c
Ap Lam (k -> d -> a)
g forall d f b c. Expr (d, f, b, c) d
X1 forall f c b c. Expr (f, c, b, c) c
X2) forall f b b c. Expr (f, b, b, c) b
X3))) (\k
x (d
a, b
b) -> k -> (a, b) -> c
mf k
x (k -> d -> a
mg k
x d
a, b
b))

compSndR :: Fun (k -> (a, b) -> c) -> Fun (k -> d -> b) -> Fun (k -> (a, d) -> c)
compSndR :: forall k a b c d.
Fun (k -> (a, b) -> c)
-> Fun (k -> d -> b) -> Fun (k -> (a, d) -> c)
compSndR (Fun Lam (k -> (a, b) -> c)
m k -> (a, b) -> c
mf) (Fun Lam (k -> d -> b)
g k -> d -> b
mg) = (forall t. Lam t -> t -> Fun t
Fun (forall f b c a t s v.
Pat (f, b, c, a) t
-> Pat (f, b, c, a) s -> Expr (f, b, c, a) v -> Lam (t -> s -> v)
Lam forall d f b c. Pat (d, f, b, c) d
P1 (forall f b c a.
Pat (f, b, c, a) a -> Pat (f, b, c, a) c -> Pat (f, b, c, a) (a, c)
PPair forall f c b c. Pat (f, c, b, c) c
P2 forall f b b c. Pat (f, b, b, c) b
P3) (forall f b c e.
Lam (f -> b -> c) -> Expr e f -> Expr e b -> Expr e c
Ap Lam (k -> (a, b) -> c)
m forall d f b c. Expr (d, f, b, c) d
X1 (forall e f b. Expr e f -> Expr e b -> Expr e (f, b)
EPair forall f c b c. Expr (f, c, b, c) c
X2 (forall f b c e.
Lam (f -> b -> c) -> Expr e f -> Expr e b -> Expr e c
Ap Lam (k -> d -> b)
g forall d f b c. Expr (d, f, b, c) d
X1 forall f b b c. Expr (f, b, b, c) b
X3)))) (\k
x (a
a, d
b) -> k -> (a, b) -> c
mf k
x (a
a, k -> d -> b
mg k
x d
b)))

compCurryR :: Fun (k -> (a, b) -> d) -> Fun (a -> c -> b) -> Fun (k -> (a, c) -> d)
compCurryR :: forall k a b d c.
Fun (k -> (a, b) -> d)
-> Fun (a -> c -> b) -> Fun (k -> (a, c) -> d)
compCurryR (Fun Lam (k -> (a, b) -> d)
ef k -> (a, b) -> d
f) (Fun Lam (a -> c -> b)
eg a -> c -> b
g) = forall t. Lam t -> t -> Fun t
Fun (forall f b c a t s v.
Pat (f, b, c, a) t
-> Pat (f, b, c, a) s -> Expr (f, b, c, a) v -> Lam (t -> s -> v)
Lam forall d f b c. Pat (d, f, b, c) d
P1 (forall f b c a.
Pat (f, b, c, a) a -> Pat (f, b, c, a) c -> Pat (f, b, c, a) (a, c)
PPair forall f c b c. Pat (f, c, b, c) c
P2 forall f b b c. Pat (f, b, b, c) b
P3) (forall f b c e.
Lam (f -> b -> c) -> Expr e f -> Expr e b -> Expr e c
Ap Lam (k -> (a, b) -> d)
ef forall d f b c. Expr (d, f, b, c) d
X1 (forall e f b. Expr e f -> Expr e b -> Expr e (f, b)
EPair forall f c b c. Expr (f, c, b, c) c
X2 (forall f b c e.
Lam (f -> b -> c) -> Expr e f -> Expr e b -> Expr e c
Ap Lam (a -> c -> b)
eg forall f c b c. Expr (f, c, b, c) c
X2 forall f b b c. Expr (f, b, b, c) b
X3)))) (\k
x (a
a, c
b) -> k -> (a, b) -> d
f k
x (a
a, a -> c -> b
g a
a c
b))

nEgate :: Fun (k -> v -> Bool) -> Fun (k -> v -> Bool)
nEgate :: forall k v. Fun (k -> v -> Bool) -> Fun (k -> v -> Bool)
nEgate (Fun Lam (k -> v -> Bool)
ef k -> v -> Bool
f) = forall t. Lam t -> t -> Fun t
Fun (forall f b c a t s v.
Pat (f, b, c, a) t
-> Pat (f, b, c, a) s -> Expr (f, b, c, a) v -> Lam (t -> s -> v)
Lam forall d f b c. Pat (d, f, b, c) d
P1 forall f c b c. Pat (f, c, b, c) c
P2 (forall e. Expr e Bool -> Expr e Bool
Neg (forall f b c e.
Lam (f -> b -> c) -> Expr e f -> Expr e b -> Expr e c
Ap Lam (k -> v -> Bool)
ef forall d f b c. Expr (d, f, b, c) d
X1 forall f c b c. Expr (f, c, b, c) c
X2))) (\k
x v
y -> Bool -> Bool
not (k -> v -> Bool
f k
x v
y))

always :: Fun (a -> b -> Bool)
always :: forall a b. Fun (a -> b -> Bool)
always = forall c a b. Show c => c -> Fun (a -> b -> c)
constant Bool
True

both :: Fun (a -> b -> Bool) -> Fun (a -> b -> Bool) -> Fun (a -> b -> Bool)
both :: forall a b.
Fun (a -> b -> Bool)
-> Fun (a -> b -> Bool) -> Fun (a -> b -> Bool)
both (Fun Lam (a -> b -> Bool)
ef a -> b -> Bool
e) (Fun Lam (a -> b -> Bool)
ff a -> b -> Bool
f) = forall t. Lam t -> t -> Fun t
Fun (forall f b c a t s v.
Pat (f, b, c, a) t
-> Pat (f, b, c, a) s -> Expr (f, b, c, a) v -> Lam (t -> s -> v)
Lam forall d f b c. Pat (d, f, b, c) d
P1 forall f c b c. Pat (f, c, b, c) c
P2 (forall f b c e.
Lam (f -> b -> c) -> Expr e f -> Expr e b -> Expr e c
Ap Lam (Bool -> Bool -> Bool)
Both (forall f b c e.
Lam (f -> b -> c) -> Expr e f -> Expr e b -> Expr e c
Ap Lam (a -> b -> Bool)
ef forall d f b c. Expr (d, f, b, c) d
X1 forall f c b c. Expr (f, c, b, c) c
X2) (forall f b c e.
Lam (f -> b -> c) -> Expr e f -> Expr e b -> Expr e c
Ap Lam (a -> b -> Bool)
ff forall d f b c. Expr (d, f, b, c) d
X1 forall f c b c. Expr (f, c, b, c) c
X2))) (\a
a b
b -> (a -> b -> Bool
e a
a b
b) Bool -> Bool -> Bool
&& (a -> b -> Bool
f a
a b
b))

lift :: (a -> b -> c) -> Fun (a -> b -> c) -- This is used in the tests, not good to use it elsewhere.
lift :: forall a b c. (a -> b -> c) -> Fun (a -> b -> c)
lift a -> b -> c
f = forall t. Lam t -> t -> Fun t
Fun (forall f b c. (f -> b -> c) -> Lam (f -> b -> c)
Lift a -> b -> c
f) a -> b -> c
f

-- ==============================================================
-- Part 3. Queries, a compiled form of Exp
-- ==============================================================

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

-- | Query is a single datatype that describes a low-level language that can be
-- used to build compound iterators, from other iterators.
data Query k v where
  BaseD :: (Iter f, Ord k) => BaseRep f k v -> f k v -> Query k v
  ProjectD :: Ord k => Query k v -> Fun (k -> v -> u) -> Query k u
  AndD :: Ord k => Query k v -> Query k w -> Query k (v, w)
  ChainD :: (Ord k, Ord v) => Query k v -> Query v w -> Fun (k -> (v, w) -> u) -> Query k u
  AndPD :: Ord k => Query k v -> Query k u -> Fun (k -> (v, u) -> w) -> Query k w
  OrD :: Ord k => Query k v -> Query k v -> Fun (v -> v -> v) -> Query k v
  GuardD :: Ord k => Query k v -> Fun (k -> v -> Bool) -> Query k v
  DiffD :: Ord k => Query k v -> Query k u -> Query k v

-- ======================================================================================
-- low-level smart constructors for Query. These apply semantic preserving rewrites when applicable
-- ======================================================================================

smart :: Bool
smart :: Bool
smart = Bool
True -- for debugging purposes, this can be set to False, in which case no rewrites occurr.

projD :: Ord k => Query k v -> Fun (k -> v -> u) -> Query k u
projD :: forall k v u. Ord k => Query k v -> Fun (k -> v -> u) -> Query k u
projD Query k v
x Fun (k -> v -> u)
y = case (Query k v
x, Fun (k -> v -> u)
y) of
  (ProjectD Query k v
f Fun (k -> v -> v)
p, Fun (k -> v -> u)
q) | Bool
smart -> forall k v u. Ord k => Query k v -> Fun (k -> v -> u) -> Query k u
projD Query k v
f (forall t1 t2 t3 t4.
Fun (t1 -> t2 -> t3)
-> Fun (t1 -> t4 -> t2) -> Fun (t1 -> t4 -> t3)
compose1 Fun (k -> v -> u)
q Fun (k -> v -> v)
p)
  (AndD Query k v
f Query k w
g, Fun (k -> v -> u)
q) | Bool
smart -> forall k v1 u v.
Ord k =>
Query k v1 -> Query k u -> Fun (k -> (v1, u) -> v) -> Query k v
andPD Query k v
f Query k w
g (forall t1 t2 t3 t4.
Fun (t1 -> t2 -> t3)
-> Fun (t1 -> t4 -> t2) -> Fun (t1 -> t4 -> t3)
compose1 Fun (k -> v -> u)
q forall v s. Fun (v -> s -> s)
second)
  (AndPD Query k v
f Query k u
g Fun (k -> (v, u) -> v)
p, Fun (k -> v -> u)
q) | Bool
smart -> forall k v1 u v.
Ord k =>
Query k v1 -> Query k u -> Fun (k -> (v1, u) -> v) -> Query k v
andPD Query k v
f Query k u
g (forall t1 t2 t3 t4.
Fun (t1 -> t2 -> t3)
-> Fun (t1 -> t4 -> t2) -> Fun (t1 -> t4 -> t3)
compose1 Fun (k -> v -> u)
q Fun (k -> (v, u) -> v)
p)
  (Query k v
f, Fun (k -> v -> u)
p) -> forall k v u. Ord k => Query k v -> Fun (k -> v -> u) -> Query k u
ProjectD Query k v
f Fun (k -> v -> u)
p

andD :: Ord k => Query k v1 -> Query k v2 -> Query k (v1, v2)
andD :: forall k v1 v2.
Ord k =>
Query k v1 -> Query k v2 -> Query k (v1, v2)
andD (ProjectD Query k v
f Fun (k -> v -> v1)
p) Query k v2
g | Bool
smart = forall k v1 u v.
Ord k =>
Query k v1 -> Query k u -> Fun (k -> (v1, u) -> v) -> Query k v
AndPD Query k v
f Query k v2
g (forall k a b c d.
Fun (k -> (a, b) -> c)
-> Fun (k -> d -> a) -> Fun (k -> (d, b) -> c)
compSndL forall v s. Fun (v -> s -> s)
second Fun (k -> v -> v1)
p)
andD Query k v1
f (ProjectD Query k v
g Fun (k -> v -> v2)
p) | Bool
smart = forall k v1 u v.
Ord k =>
Query k v1 -> Query k u -> Fun (k -> (v1, u) -> v) -> Query k v
AndPD Query k v1
f Query k v
g (forall k a b c d.
Fun (k -> (a, b) -> c)
-> Fun (k -> d -> b) -> Fun (k -> (a, d) -> c)
compSndR forall v s. Fun (v -> s -> s)
second Fun (k -> v -> v2)
p)
andD Query k v1
f Query k v2
g = forall k v1 v2.
Ord k =>
Query k v1 -> Query k v2 -> Query k (v1, v2)
AndD Query k v1
f Query k v2
g

andPD :: Ord k => Query k v1 -> Query k u -> Fun (k -> (v1, u) -> v) -> Query k v
andPD :: forall k v1 u v.
Ord k =>
Query k v1 -> Query k u -> Fun (k -> (v1, u) -> v) -> Query k v
andPD (ProjectD Query k v
f Fun (k -> v -> v1)
p) Query k u
g Fun (k -> (v1, u) -> v)
q | Bool
smart = forall k v1 u v.
Ord k =>
Query k v1 -> Query k u -> Fun (k -> (v1, u) -> v) -> Query k v
andPD Query k v
f Query k u
g (forall k a b c d.
Fun (k -> (a, b) -> c)
-> Fun (k -> d -> a) -> Fun (k -> (d, b) -> c)
compSndL Fun (k -> (v1, u) -> v)
q Fun (k -> v -> v1)
p)
andPD Query k v1
f Query k u
g Fun (k -> (v1, u) -> v)
p = forall k v1 u v.
Ord k =>
Query k v1 -> Query k u -> Fun (k -> (v1, u) -> v) -> Query k v
AndPD Query k v1
f Query k u
g Fun (k -> (v1, u) -> v)
p

chainD :: (Ord k, Ord v) => Query k v -> Query v w -> Fun (k -> (v, w) -> u) -> Query k u
chainD :: 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
f (ProjectD Query v v
g Fun (v -> v -> w)
p) Fun (k -> (v, w) -> u)
q | Bool
smart = 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
f Query v v
g (forall k a b d c.
Fun (k -> (a, b) -> d)
-> Fun (a -> c -> b) -> Fun (k -> (a, c) -> d)
compCurryR Fun (k -> (v, w) -> u)
q Fun (v -> v -> w)
p)
chainD Query k v
f Query v w
g Fun (k -> (v, w) -> u)
p = 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
f Query v w
g Fun (k -> (v, w) -> u)
p

guardD :: Ord k => Query k v -> Fun (k -> v -> Bool) -> Query k v
guardD :: forall k v. Ord k => Query k v -> Fun (k -> v -> Bool) -> Query k v
guardD (GuardD Query k v
q1 Fun (k -> v -> Bool)
test1) Fun (k -> v -> Bool)
test2 | Bool
smart = forall k v. Ord k => Query k v -> Fun (k -> v -> Bool) -> Query k v
GuardD Query k v
q1 (forall a b.
Fun (a -> b -> Bool)
-> Fun (a -> b -> Bool) -> Fun (a -> b -> Bool)
both Fun (k -> v -> Bool)
test1 Fun (k -> v -> Bool)
test2)
guardD Query k v
qry Fun (k -> v -> Bool)
test = forall k v. Ord k => Query k v -> Fun (k -> v -> Bool) -> Query k v
GuardD Query k v
qry Fun (k -> v -> Bool)
test

-- =======================================================================================
-- Finally we make high-level smart constructors for Query, so we can lift un-embedded Base types
-- into Queries, so programmers don't need to know about List and Sett and other anomalies.
-- Note that these high-level smart constructors are in 1-to-1 correspondance with the low-level
-- ones, except the low-level ones take Querys, and the high-level ones just take data, lift the
-- data to Query, and then apply the low-level smart constructors.

-- Create a projection Query
projectQ :: (Ord k, HasQuery c k v) => c -> Fun (k -> v -> u) -> Query k u
projectQ :: forall k c v u.
(Ord k, HasQuery c k v) =>
c -> Fun (k -> v -> u) -> Query k u
projectQ c
q Fun (k -> v -> u)
fun = forall k v u. Ord k => Query k v -> Fun (k -> v -> u) -> Query k u
ProjectD (forall concrete k v. HasQuery concrete k v => concrete -> Query k v
query c
q) Fun (k -> v -> u)
fun

-- Conjoin two Querys
andQ ::
  (Ord k, HasQuery concrete1 k v, HasQuery concrete2 k w) => concrete1 -> concrete2 -> Query k (v, w)
andQ :: forall k concrete1 v concrete2 w.
(Ord k, HasQuery concrete1 k v, HasQuery concrete2 k w) =>
concrete1 -> concrete2 -> Query k (v, w)
andQ concrete1
x concrete2
y = forall k v1 v2.
Ord k =>
Query k v1 -> Query k v2 -> Query k (v1, v2)
AndD (forall concrete k v. HasQuery concrete k v => concrete -> Query k v
query concrete1
x) (forall concrete k v. HasQuery concrete k v => concrete -> Query k v
query concrete2
y)

-- Disjoin two Queries
orQ ::
  (Ord k, HasQuery concrete1 k v, HasQuery concrete2 k v) =>
  concrete1 ->
  concrete2 ->
  Fun (v -> v -> v) ->
  Query k v
orQ :: forall k concrete1 v concrete2.
(Ord k, HasQuery concrete1 k v, HasQuery concrete2 k v) =>
concrete1 -> concrete2 -> Fun (v -> v -> v) -> Query k v
orQ concrete1
x concrete2
y Fun (v -> v -> v)
comb = forall k v.
Ord k =>
Query k v -> Query k v -> Fun (v -> v -> v) -> Query k v
OrD (forall concrete k v. HasQuery concrete k v => concrete -> Query k v
query concrete1
x) (forall concrete k v. HasQuery concrete k v => concrete -> Query k v
query concrete2
y) Fun (v -> v -> v)
comb

chainQ ::
  (Ord k, Ord v, HasQuery concrete1 k v, HasQuery concrete2 v w) =>
  concrete1 ->
  concrete2 ->
  Fun (k -> (v, w) -> u) ->
  Query k u
chainQ :: forall k v concrete1 concrete2 w u.
(Ord k, Ord v, HasQuery concrete1 k v, HasQuery concrete2 v w) =>
concrete1 -> concrete2 -> Fun (k -> (v, w) -> u) -> Query k u
chainQ concrete1
x concrete2
y Fun (k -> (v, w) -> u)
p = forall k v w u.
(Ord k, Ord v) =>
Query k v -> Query v w -> Fun (k -> (v, w) -> u) -> Query k u
ChainD (forall concrete k v. HasQuery concrete k v => concrete -> Query k v
query concrete1
x) (forall concrete k v. HasQuery concrete k v => concrete -> Query k v
query concrete2
y) Fun (k -> (v, w) -> u)
p

andPQ ::
  (Ord k, HasQuery concrete1 k v, HasQuery concrete2 k u) =>
  concrete1 ->
  concrete2 ->
  Fun (k -> (v, u) -> w) ->
  Query k w
andPQ :: forall k concrete1 v concrete2 u w.
(Ord k, HasQuery concrete1 k v, HasQuery concrete2 k u) =>
concrete1 -> concrete2 -> Fun (k -> (v, u) -> w) -> Query k w
andPQ concrete1
x concrete2
y Fun (k -> (v, u) -> w)
p = forall k v1 u v.
Ord k =>
Query k v1 -> Query k u -> Fun (k -> (v1, u) -> v) -> Query k v
AndPD (forall concrete k v. HasQuery concrete k v => concrete -> Query k v
query concrete1
x) (forall concrete k v. HasQuery concrete k v => concrete -> Query k v
query concrete2
y) Fun (k -> (v, u) -> w)
p

guardQ ::
  (Ord k, HasQuery concrete k v) =>
  concrete ->
  Fun (k -> v -> Bool) ->
  Query k v
guardQ :: forall k concrete v.
(Ord k, HasQuery concrete k v) =>
concrete -> Fun (k -> v -> Bool) -> Query k v
guardQ concrete
x Fun (k -> v -> Bool)
p = forall k v. Ord k => Query k v -> Fun (k -> v -> Bool) -> Query k v
GuardD (forall concrete k v. HasQuery concrete k v => concrete -> Query k v
query concrete
x) Fun (k -> v -> Bool)
p

-- Don't know why this won't type check
-- diffQ :: (Ord k, HasQuery concrete1 k v, HasQuery concrete2 k u) => concrete1 -> concrete2 -> Query k v
-- diffQ = \ x y -> DiffD (query x) (query y)
diffQ ::
  forall k v u concrete1 concrete2.
  (Ord k, HasQuery (concrete1 k v) k v, HasQuery (concrete2 k u) k u) =>
  (concrete1 k v) ->
  (concrete2 k u) ->
  Query k v
diffQ :: forall k v u (concrete1 :: * -> * -> *) (concrete2 :: * -> * -> *).
(Ord k, HasQuery (concrete1 k v) k v,
 HasQuery (concrete2 k u) k u) =>
concrete1 k v -> concrete2 k u -> Query k v
diffQ concrete1 k v
x concrete2 k u
y = forall k v f. Ord k => Query k v -> Query k f -> Query k v
DiffD (forall concrete k v. HasQuery concrete k v => concrete -> Query k v
query concrete1 k v
x) (forall concrete k v. HasQuery concrete k v => concrete -> Query k v
query @(concrete2 k u) @k @u concrete2 k u
y)

class HasQuery concrete k v where
  query :: concrete -> Query k v

instance HasQuery (Query k v) k v where
  query :: Query k v -> Query k v
query Query k v
xs = Query k v
xs

instance Ord k => HasQuery [(k, v)] k v where
  query :: [(k, v)] -> Query k v
query [(k, v)]
xs = forall (f :: * -> * -> *) k v.
(Iter f, Ord k) =>
BaseRep f k v -> f k v -> Query k v
BaseD forall k v. Basic List => BaseRep List k v
ListR (forall k v. Ord k => (v -> v -> v) -> [(k, v)] -> List k v
fromPairs (\v
l v
_r -> v
l) [(k, v)]
xs)

instance Ord k => HasQuery (Set.Set k) k () where
  query :: Set k -> Query k ()
query Set k
xs = forall (f :: * -> * -> *) k v.
(Iter f, Ord k) =>
BaseRep f k v -> f k v -> Query k v
BaseD forall k. Basic Sett => BaseRep Sett k ()
SetR (forall k. Set k -> Sett k ()
Sett Set k
xs)

instance Ord k => HasQuery (Map.Map k v) k v where
  query :: Map k v -> Query k v
query Map k v
xs = forall (f :: * -> * -> *) k v.
(Iter f, Ord k) =>
BaseRep f k v -> f k v -> Query k v
BaseD forall k v. Basic Map => BaseRep Map k v
MapR Map k v
xs

instance Ord k => HasQuery (Single k v) k v where
  query :: Single k v -> Query k v
query Single k v
xs = forall (f :: * -> * -> *) k v.
(Iter f, Ord k) =>
BaseRep f k v -> f k v -> Query k v
BaseD forall k v. Basic Single => BaseRep Single k v
SingleR Single k v
xs

-- =================================================
-- Show Instance of Query

ppQuery :: Query k v -> Doc a
ppQuery :: forall k v a. Query k v -> Doc a
ppQuery (BaseD BaseRep f k v
rep f k v
_f) = forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Show a => a -> String
show BaseRep f k v
rep)
ppQuery (ProjectD Query k v
f Fun (k -> v -> v)
p) = forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"Proj" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall ann. [Doc ann] -> Doc ann
vsep [forall k v a. Query k v -> Doc a
ppQuery Query k v
f, forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Show a => a -> String
show Fun (k -> v -> v)
p)])
ppQuery (AndD Query k v
f Query k w
g) = forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"And" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall ann. [Doc ann] -> Doc ann
vsep [forall k v a. Query k v -> Doc a
ppQuery Query k v
f, forall k v a. Query k v -> Doc a
ppQuery Query k w
g])
ppQuery (ChainD Query k v
f Query v w
g Fun (k -> (v, w) -> v)
p) = forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"Chain" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall ann. [Doc ann] -> Doc ann
vsep [forall k v a. Query k v -> Doc a
ppQuery Query k v
f, forall k v a. Query k v -> Doc a
ppQuery Query v w
g, forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Show a => a -> String
show Fun (k -> (v, w) -> v)
p)])
ppQuery (OrD Query k v
f Query k v
g Fun (v -> v -> v)
p) = forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"Or" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall ann. [Doc ann] -> Doc ann
vsep [forall k v a. Query k v -> Doc a
ppQuery Query k v
f, forall k v a. Query k v -> Doc a
ppQuery Query k v
g, forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Show a => a -> String
show Fun (v -> v -> v)
p)])
ppQuery (GuardD Query k v
f Fun (k -> v -> Bool)
p) = forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"Guard" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall ann. [Doc ann] -> Doc ann
vsep [forall k v a. Query k v -> Doc a
ppQuery Query k v
f, forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Show a => a -> String
show Fun (k -> v -> Bool)
p)])
ppQuery (DiffD Query k v
f Query k u
g) = forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"Diff" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall ann. [Doc ann] -> Doc ann
vsep [forall k v a. Query k v -> Doc a
ppQuery Query k v
f, forall k v a. Query k v -> Doc a
ppQuery Query k u
g])
ppQuery (AndPD Query k v
f Query k u
g Fun (k -> (v, u) -> v)
p) = forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"AndP" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall ann. [Doc ann] -> Doc ann
vsep [forall k v a. Query k v -> Doc a
ppQuery Query k v
f, forall k v a. Query k v -> Doc a
ppQuery Query k u
g, forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Show a => a -> String
show Fun (k -> (v, u) -> v)
p)])

instance Show (Query k v) where
  show :: Query k v -> String
show Query k v
x = forall a. Show a => a -> String
show (forall k v a. Query k v -> Doc a
ppQuery Query k v
x)

-- =================================================
-- An instance of Iter can be made for Query.

nxtQuery :: Query a b -> Collect (a, b, Query a b)
nxtQuery :: forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery (BaseD BaseRep f a b
rep f a b
x) = do (a
k, b
v, f a b
x2) <- forall (f :: * -> * -> *) a b.
Iter f =>
f a b -> Collect (a, b, f a b)
nxt f a b
x; forall t. t -> Collect t
one (a
k, b
v, forall (f :: * -> * -> *) k v.
(Iter f, Ord k) =>
BaseRep f k v -> f k v -> Query k v
BaseD BaseRep f a b
rep f a b
x2)
nxtQuery (ProjectD Query a v
x Fun (a -> v -> b)
p) = forall k t v u.
Ord k =>
(t -> Collect (k, v, Query k v))
-> Fun (k -> v -> u) -> t -> Collect (k, u, Query k u)
projStep forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Fun (a -> v -> b)
p Query a v
x
nxtQuery (AndD Query a v
f Query a w
g) = do (a, v, Query a v)
triple1 <- forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Query a v
f; (a, w, Query a w)
triple2 <- forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Query a w
g; forall a b1 b2.
Ord a =>
(a, b1, Query a b1)
-> (a, b2, Query a b2) -> Collect (a, (b1, b2), Query a (b1, b2))
andStep (a, v, Query a v)
triple1 (a, w, Query a w)
triple2
nxtQuery (ChainD Query a v
f Query v w
g Fun (a -> (v, w) -> b)
p) = do (a, v, Query a v)
trip <- forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Query a v
f; forall b a w u.
(Ord b, Ord a) =>
(a, b, Query a b)
-> Query b w -> Fun (a -> (b, w) -> u) -> Collect (a, u, Query a u)
chainStep (a, v, Query a v)
trip Query v w
g Fun (a -> (v, w) -> b)
p
nxtQuery (AndPD Query a v
f Query a u
g Fun (a -> (v, u) -> b)
p) = do (a, v, Query a v)
triple1 <- forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Query a v
f; (a, u, Query a u)
triple2 <- forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Query a u
g; forall a b1 b2 w.
Ord a =>
(a, b1, Query a b1)
-> (a, b2, Query a b2)
-> Fun (a -> (b1, b2) -> w)
-> Collect (a, w, Query a w)
andPstep (a, v, Query a v)
triple1 (a, u, Query a u)
triple2 Fun (a -> (v, u) -> b)
p
nxtQuery (OrD Query a b
f Query a b
g Fun (b -> b -> b)
comb) = forall k a v.
(Ord k, Ord a) =>
(Query k v -> Collect (a, v, Query k v))
-> Query k v
-> Query k v
-> Fun (v -> v -> v)
-> Collect (a, v, Query k v)
orStep forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Query a b
f Query a b
g Fun (b -> b -> b)
comb
nxtQuery (GuardD Query a b
f Fun (a -> b -> Bool)
p) = forall a b.
Ord a =>
(Query a b -> Collect (a, b, Query a b))
-> Fun (a -> b -> Bool) -> Query a b -> Collect (a, b, Query a b)
guardStep forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Fun (a -> b -> Bool)
p Query a b
f
nxtQuery (DiffD Query a b
f Query a u
g) = do (a, b, Query a b)
trip <- forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Query a b
f; forall k v u.
Ord k =>
(k, v, Query k v) -> Query k u -> Collect (k, v, Query k v)
diffStep (a, b, Query a b)
trip Query a u
g

lubQuery :: Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery :: forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
key (BaseD BaseRep f a b
rep f a b
x) = do (a
k, b
v, f a b
x2) <- forall (f :: * -> * -> *) k b.
(Iter f, Ord k) =>
k -> f k b -> Collect (k, b, f k b)
lub a
key f a b
x; forall t. t -> Collect t
one (a
k, b
v, forall (f :: * -> * -> *) k v.
(Iter f, Ord k) =>
BaseRep f k v -> f k v -> Query k v
BaseD BaseRep f a b
rep f a b
x2)
lubQuery a
key (ProjectD Query a v
x Fun (a -> v -> b)
p) = forall k t v u.
Ord k =>
(t -> Collect (k, v, Query k v))
-> Fun (k -> v -> u) -> t -> Collect (k, u, Query k u)
projStep (forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
key) Fun (a -> v -> b)
p Query a v
x
lubQuery a
key (AndD Query a v
f Query a w
g) = do (a, v, Query a v)
triple1 <- forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
key Query a v
f; (a, w, Query a w)
triple2 <- forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
key Query a w
g; forall a b1 b2.
Ord a =>
(a, b1, Query a b1)
-> (a, b2, Query a b2) -> Collect (a, (b1, b2), Query a (b1, b2))
andStep (a, v, Query a v)
triple1 (a, w, Query a w)
triple2
lubQuery a
key (ChainD Query a v
f Query v w
g Fun (a -> (v, w) -> b)
p) = do (a, v, Query a v)
trip <- forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
key Query a v
f; forall b a w u.
(Ord b, Ord a) =>
(a, b, Query a b)
-> Query b w -> Fun (a -> (b, w) -> u) -> Collect (a, u, Query a u)
chainStep (a, v, Query a v)
trip Query v w
g Fun (a -> (v, w) -> b)
p
lubQuery a
key (AndPD Query a v
f Query a u
g Fun (a -> (v, u) -> b)
p) = do (a, v, Query a v)
triple1 <- forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
key Query a v
f; (a, u, Query a u)
triple2 <- forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
key Query a u
g; forall a b1 b2 w.
Ord a =>
(a, b1, Query a b1)
-> (a, b2, Query a b2)
-> Fun (a -> (b1, b2) -> w)
-> Collect (a, w, Query a w)
andPstep (a, v, Query a v)
triple1 (a, u, Query a u)
triple2 Fun (a -> (v, u) -> b)
p
lubQuery a
key (OrD Query a b
f Query a b
g Fun (b -> b -> b)
comb) = forall k a v.
(Ord k, Ord a) =>
(Query k v -> Collect (a, v, Query k v))
-> Query k v
-> Query k v
-> Fun (v -> v -> v)
-> Collect (a, v, Query k v)
orStep (forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
key) Query a b
f Query a b
g Fun (b -> b -> b)
comb
lubQuery a
key (GuardD Query a b
f Fun (a -> b -> Bool)
p) = forall a b.
Ord a =>
(Query a b -> Collect (a, b, Query a b))
-> Fun (a -> b -> Bool) -> Query a b -> Collect (a, b, Query a b)
guardStep (forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
key) Fun (a -> b -> Bool)
p Query a b
f
lubQuery a
key (DiffD Query a b
f Query a u
g) = do (a, b, Query a b)
trip <- forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
key Query a b
f; forall k v u.
Ord k =>
(k, v, Query k v) -> Query k u -> Collect (k, v, Query k v)
diffStep (a, b, Query a b)
trip Query a u
g

instance Iter Query where
  nxt :: forall a b. Query a b -> Collect (a, b, Query a b)
nxt = forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery
  lub :: forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lub = forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery

-- ==============================================================================================
-- To make the Iter instance for Query, we need semantic operators for each of the constructors
-- of Query. These semantic operators are "step" functions for each constructor.
-- ==============================================================================================

-- ==== Project ====
projStep ::
  Ord k =>
  (t -> Collect (k, v, Query k v)) ->
  Fun (k -> v -> u) ->
  t ->
  Collect (k, u, Query k u)
projStep :: forall k t v u.
Ord k =>
(t -> Collect (k, v, Query k v))
-> Fun (k -> v -> u) -> t -> Collect (k, u, Query k u)
projStep t -> Collect (k, v, Query k v)
next Fun (k -> v -> u)
p t
f = do (k
k, v
v, Query k v
f') <- t -> Collect (k, v, Query k v)
next t
f; forall t. t -> Collect t
one (k
k, forall t. Fun t -> t
apply Fun (k -> v -> u)
p k
k v
v, forall k v u. Ord k => Query k v -> Fun (k -> v -> u) -> Query k u
ProjectD Query k v
f' Fun (k -> v -> u)
p)

-- ===== And = ====
andStep ::
  Ord a =>
  (a, b1, Query a b1) ->
  (a, b2, Query a b2) ->
  Collect (a, (b1, b2), Query a (b1, b2))
andStep :: forall a b1 b2.
Ord a =>
(a, b1, Query a b1)
-> (a, b2, Query a b2) -> Collect (a, (b1, b2), Query a (b1, b2))
andStep (ftrip :: (a, b1, Query a b1)
ftrip@(a
k1, b1
v1, Query a b1
f1)) (gtrip :: (a, b2, Query a b2)
gtrip@(a
k2, b2
v2, Query a b2
g2)) =
  case forall a. Ord a => a -> a -> Ordering
compare a
k1 a
k2 of
    Ordering
EQ -> forall t. t -> Collect t
one (a
k1, (b1
v1, b2
v2), forall k v1 v2.
Ord k =>
Query k v1 -> Query k v2 -> Query k (v1, v2)
AndD Query a b1
f1 Query a b2
g2)
    Ordering
LT -> do (a, b1, Query a b1)
ftrip' <- forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
k2 Query a b1
f1; forall a b1 b2.
Ord a =>
(a, b1, Query a b1)
-> (a, b2, Query a b2) -> Collect (a, (b1, b2), Query a (b1, b2))
andStep (a, b1, Query a b1)
ftrip' (a, b2, Query a b2)
gtrip
    Ordering
GT -> do (a, b2, Query a b2)
gtrip' <- forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
k1 Query a b2
g2; forall a b1 b2.
Ord a =>
(a, b1, Query a b1)
-> (a, b2, Query a b2) -> Collect (a, (b1, b2), Query a (b1, b2))
andStep (a, b1, Query a b1)
ftrip (a, b2, Query a b2)
gtrip'

-- ==== Chain ====
chainStep ::
  (Ord b, Ord a) =>
  (a, b, Query a b) ->
  Query b w ->
  Fun (a -> (b, w) -> u) ->
  Collect (a, u, Query a u)
chainStep :: forall b a w u.
(Ord b, Ord a) =>
(a, b, Query a b)
-> Query b w -> Fun (a -> (b, w) -> u) -> Collect (a, u, Query a u)
chainStep (a
d, b
r1, Query a b
f1) Query b w
g Fun (a -> (b, w) -> u)
comb =
  case forall (f :: * -> * -> *) key rng.
(Iter f, Ord key) =>
key -> f key rng -> Maybe rng
lookup b
r1 Query b w
g of -- recall that the values 'r1' from f, are not iterated in ascending order, only the keys 'd' are ascending
    Just w
w -> forall t. t -> Collect t
one (a
d, forall t. Fun t -> t
apply Fun (a -> (b, w) -> u)
comb a
d (b
r1, w
w), 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 a b
f1 Query b w
g Fun (a -> (b, w) -> u)
comb)
    Maybe w
Nothing -> do (a, b, Query a b)
trip <- forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Query a b
f1; forall b a w u.
(Ord b, Ord a) =>
(a, b, Query a b)
-> Query b w -> Fun (a -> (b, w) -> u) -> Collect (a, u, Query a u)
chainStep (a, b, Query a b)
trip Query b w
g Fun (a -> (b, w) -> u)
comb

-- ==== And with Projection ====
andPstep ::
  Ord a =>
  (a, b1, Query a b1) ->
  (a, b2, Query a b2) ->
  Fun (a -> (b1, b2) -> w) ->
  Collect (a, w, Query a w)
andPstep :: forall a b1 b2 w.
Ord a =>
(a, b1, Query a b1)
-> (a, b2, Query a b2)
-> Fun (a -> (b1, b2) -> w)
-> Collect (a, w, Query a w)
andPstep (ftrip :: (a, b1, Query a b1)
ftrip@(a
k1, b1
v1, Query a b1
f1)) (gtrip :: (a, b2, Query a b2)
gtrip@(a
k2, b2
v2, Query a b2
g2)) Fun (a -> (b1, b2) -> w)
p =
  case forall a. Ord a => a -> a -> Ordering
compare a
k1 a
k2 of
    Ordering
EQ -> forall t. t -> Collect t
one (a
k1, (forall t. Fun t -> t
apply Fun (a -> (b1, b2) -> w)
p a
k1 (b1
v1, b2
v2)), forall k v1 u v.
Ord k =>
Query k v1 -> Query k u -> Fun (k -> (v1, u) -> v) -> Query k v
AndPD Query a b1
f1 Query a b2
g2 Fun (a -> (b1, b2) -> w)
p)
    Ordering
LT -> do (a, b1, Query a b1)
ftrip' <- forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
k2 Query a b1
f1; forall a b1 b2 w.
Ord a =>
(a, b1, Query a b1)
-> (a, b2, Query a b2)
-> Fun (a -> (b1, b2) -> w)
-> Collect (a, w, Query a w)
andPstep (a, b1, Query a b1)
ftrip' (a, b2, Query a b2)
gtrip Fun (a -> (b1, b2) -> w)
p
    Ordering
GT -> do (a, b2, Query a b2)
gtrip' <- forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
k1 Query a b2
g2; forall a b1 b2 w.
Ord a =>
(a, b1, Query a b1)
-> (a, b2, Query a b2)
-> Fun (a -> (b1, b2) -> w)
-> Collect (a, w, Query a w)
andPstep (a, b1, Query a b1)
ftrip (a, b2, Query a b2)
gtrip' Fun (a -> (b1, b2) -> w)
p

-- ==== Or with combine ====
orStep ::
  (Ord k, Ord a) =>
  (Query k v -> Collect (a, v, Query k v)) ->
  Query k v ->
  Query k v ->
  Fun (v -> v -> v) ->
  Collect (a, v, Query k v)
orStep :: forall k a v.
(Ord k, Ord a) =>
(Query k v -> Collect (a, v, Query k v))
-> Query k v
-> Query k v
-> Fun (v -> v -> v)
-> Collect (a, v, Query k v)
orStep Query k v -> Collect (a, v, Query k v)
next Query k v
f Query k v
g Fun (v -> v -> v)
comb =
  case (forall t. Collect t -> Maybe t
hasElem (Query k v -> Collect (a, v, Query k v)
next Query k v
f), forall t. Collect t -> Maybe t
hasElem (Query k v -> Collect (a, v, Query k v)
next Query k v
g)) of -- We have to be careful, because if only one has a nxt, there is still an answer
    (Maybe (a, v, Query k v)
Nothing, Maybe (a, v, Query k v)
Nothing) -> forall t. Collect t
none
    (Just (a
k1, v
v1, Query k v
f1), Maybe (a, v, Query k v)
Nothing) -> forall t. t -> Collect t
one (a
k1, v
v1, forall k v.
Ord k =>
Query k v -> Query k v -> Fun (v -> v -> v) -> Query k v
OrD Query k v
f1 Query k v
g Fun (v -> v -> v)
comb)
    (Maybe (a, v, Query k v)
Nothing, Just (a
k1, v
v1, Query k v
g1)) -> forall t. t -> Collect t
one (a
k1, v
v1, forall k v.
Ord k =>
Query k v -> Query k v -> Fun (v -> v -> v) -> Query k v
OrD Query k v
f Query k v
g1 Fun (v -> v -> v)
comb)
    (Just (a
k1, v
v1, Query k v
f1), Just (a
k2, v
v2, Query k v
g2)) ->
      case forall a. Ord a => a -> a -> Ordering
compare a
k1 a
k2 of
        Ordering
EQ -> forall t. t -> Collect t
one (a
k1, forall t. Fun t -> t
apply Fun (v -> v -> v)
comb v
v1 v
v2, forall k v.
Ord k =>
Query k v -> Query k v -> Fun (v -> v -> v) -> Query k v
OrD Query k v
f1 Query k v
g2 Fun (v -> v -> v)
comb)
        Ordering
LT -> forall t. t -> Collect t
one (a
k1, v
v1, forall k v.
Ord k =>
Query k v -> Query k v -> Fun (v -> v -> v) -> Query k v
OrD Query k v
f1 Query k v
g Fun (v -> v -> v)
comb)
        Ordering
GT -> forall t. t -> Collect t
one (a
k2, v
v2, forall k v.
Ord k =>
Query k v -> Query k v -> Fun (v -> v -> v) -> Query k v
OrD Query k v
f Query k v
g2 Fun (v -> v -> v)
comb)

-- ===== Guard =====
guardStep ::
  Ord a =>
  (Query a b -> Collect (a, b, Query a b)) ->
  Fun (a -> b -> Bool) ->
  Query a b ->
  Collect (a, b, Query a b)
guardStep :: forall a b.
Ord a =>
(Query a b -> Collect (a, b, Query a b))
-> Fun (a -> b -> Bool) -> Query a b -> Collect (a, b, Query a b)
guardStep Query a b -> Collect (a, b, Query a b)
next Fun (a -> b -> Bool)
p Query a b
f = do (a, b, Query a b)
triple <- Query a b -> Collect (a, b, Query a b)
next Query a b
f; (a, b, Query a b) -> Collect (a, b, Query a b)
loop (a, b, Query a b)
triple
  where
    loop :: (a, b, Query a b) -> Collect (a, b, Query a b)
loop (a
k, b
v, Query a b
f') = if (forall t. Fun t -> t
apply Fun (a -> b -> Bool)
p a
k b
v) then forall t. t -> Collect t
one (a
k, b
v, forall k v. Ord k => Query k v -> Fun (k -> v -> Bool) -> Query k v
GuardD Query a b
f' Fun (a -> b -> Bool)
p) else do (a, b, Query a b)
triple <- forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Query a b
f'; (a, b, Query a b) -> Collect (a, b, Query a b)
loop (a, b, Query a b)
triple

-- ===== Difference by key =====
diffStep :: Ord k => (k, v, Query k v) -> Query k u -> Collect (k, v, Query k v)
diffStep :: forall k v u.
Ord k =>
(k, v, Query k v) -> Query k u -> Collect (k, v, Query k v)
diffStep (k
k1, v
u1, Query k v
f1) Query k u
g =
  case forall t. Collect t -> Maybe t
hasElem (forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery k
k1 Query k u
g) of
    Maybe (k, u, Query k u)
Nothing -> forall t. t -> Collect t
one (k
k1, v
u1, forall k v f. Ord k => Query k v -> Query k f -> Query k v
DiffD Query k v
f1 Query k u
g) -- g has nothing to subtract
    Just (k
k2, u
_u2, Query k u
g2) -> case forall a. Ord a => a -> a -> Ordering
compare k
k1 k
k2 of
      Ordering
EQ -> do (k, v, Query k v)
tup <- forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Query k v
f1; forall k v u.
Ord k =>
(k, v, Query k v) -> Query k u -> Collect (k, v, Query k v)
diffStep (k, v, Query k v)
tup Query k u
g2
      Ordering
LT -> forall t. t -> Collect t
one (k
k1, v
u1, forall k v f. Ord k => Query k v -> Query k f -> Query k v
DiffD Query k v
f1 Query k u
g)
      Ordering
GT -> forall t. t -> Collect t
one (k
k1, v
u1, forall k v f. Ord k => Query k v -> Query k f -> Query k v
DiffD Query k v
f1 Query k u
g) -- the hasElem guarantees k1 <= k2, so this case is dead code