{-# 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.BiMap (BiMap, Bimap)
import Data.List (sortBy)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Data.UMap (UnifiedView (..), View)
import Text.PrettyPrint.ANSI.Leijen (Doc, align, parens, text, vsep, (<+>))
import Prelude hiding (lookup)

-- ================================================================================================
-- 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) -- Note the use of BaseRep to witness what Base type.
  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 _ _)) = String
"Single(_ _)"
  show (Base BaseRep f k v
SingleR (SetSingle _)) = String
"SetSingle(_)"
  show (Base BaseRep f k v
rep f k v
_x) = BaseRep f k v -> String
forall a. Show a => a -> String
show BaseRep f k v
rep String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"?"
  show (Dom Exp (f k v)
x) = String
"(dom " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (f k v) -> String
forall a. Show a => a -> String
show Exp (f k v)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (Rng Exp (f k v)
x) = String
"(rng " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (f k v) -> String
forall a. Show a => a -> String
show Exp (f k v)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (DRestrict Exp (g k ())
x Exp (f k v)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (g k ()) -> String
forall a. Show a => a -> String
show Exp (g k ())
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ◁ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (f k v) -> String
forall a. Show a => a -> String
show Exp (f k v)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (DExclude Exp (g k ())
x Exp (f k v)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (g k ()) -> String
forall a. Show a => a -> String
show Exp (g k ())
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ⋪ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (f k v) -> String
forall a. Show a => a -> String
show Exp (f k v)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (RRestrict Exp (f k v)
x Exp (g v ())
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (f k v) -> String
forall a. Show a => a -> String
show Exp (f k v)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ▷ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (g v ()) -> String
forall a. Show a => a -> String
show Exp (g v ())
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (RExclude Exp (f k v)
x Exp (g v ())
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (f k v) -> String
forall a. Show a => a -> String
show Exp (f k v)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ⋫ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (g v ()) -> String
forall a. Show a => a -> String
show Exp (g v ())
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (Elem k
k Exp (g k ())
x) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ k -> String
forall a. Show a => a -> String
show k
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ∈ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (g k ()) -> String
forall a. Show a => a -> String
show Exp (g k ())
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (NotElem k
k Exp (g k ())
x) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ k -> String
forall a. Show a => a -> String
show k
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ∉ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (g k ()) -> String
forall a. Show a => a -> String
show Exp (g k ())
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (Intersect Exp (f k v)
x Exp (g k u)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (f k v) -> String
forall a. Show a => a -> String
show Exp (f k v)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ∩ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (g k u) -> String
forall a. Show a => a -> String
show Exp (g k u)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (SetDiff Exp (f k v)
x Exp (g k u)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (f k v) -> String
forall a. Show a => a -> String
show Exp (f k v)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ➖ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (g k u) -> String
forall a. Show a => a -> String
show Exp (g k u)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (Subset Exp (f k v)
x Exp (g k u)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (f k v) -> String
forall a. Show a => a -> String
show Exp (f k v)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ⊆ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (g k u) -> String
forall a. Show a => a -> String
show Exp (g k u)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (UnionOverrideLeft Exp (f k v)
x Exp (g k v)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (f k v) -> String
forall a. Show a => a -> String
show Exp (f k v)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ∪ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (g k v) -> String
forall a. Show a => a -> String
show Exp (g k v)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (UnionPlus Exp (f k n)
x Exp (g k n)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (f k n) -> String
forall a. Show a => a -> String
show Exp (f k n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ∪+ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (g k n) -> String
forall a. Show a => a -> String
show Exp (g k n)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (UnionOverrideRight Exp (f k v)
x Exp (g k v)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (f k v) -> String
forall a. Show a => a -> String
show Exp (f k v)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ⨃ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (g k v) -> String
forall a. Show a => a -> String
show Exp (g k v)
y String -> ShowS
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
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (f k v) -> String
forall a. Show a => a -> String
show Exp (f k v)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ≍ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp (g k u) -> String
forall a. Show a => a -> String
show Exp (g k u)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

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

-- | Basic types are those that can be embedded 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 = BaseRep Map k v -> Map k v -> Exp (Map k v)
forall k (f :: * -> * -> *) v.
(Ord k, Basic f, Iter f) =>
BaseRep f k v -> f k v -> Exp (f k v)
Base BaseRep Map k v
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 = BaseRep Sett k () -> Sett k () -> Exp (Sett k ())
forall k (f :: * -> * -> *) v.
(Ord k, Basic f, Iter f) =>
BaseRep f k v -> f k v -> Exp (f k v)
Base BaseRep Sett k ()
forall k. Basic Sett => BaseRep Sett k ()
SetR (Set k -> Sett k ()
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 = BaseRep List k v -> List k v -> Exp (List k v)
forall k (f :: * -> * -> *) v.
(Ord k, Basic f, Iter f) =>
BaseRep f k v -> f k v -> Exp (f k v)
Base BaseRep List k v
forall k v. Basic List => BaseRep List k v
ListR ([(k, v)] -> List k v
forall k v. Ord k => [(k, v)] -> List k v
UnSafeList (((k, v) -> (k, v) -> Ordering) -> [(k, v)] -> [(k, v)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\(k, v)
x (k, v)
y -> k -> k -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ((k, v) -> k
forall a b. (a, b) -> a
fst (k, v)
x) ((k, v) -> k
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 = BaseRep Single k v -> Single k v -> Exp (Single k v)
forall k (f :: * -> * -> *) v.
(Ord k, Basic f, Iter f) =>
BaseRep f k v -> f k v -> Exp (f k v)
Base BaseRep Single k v
forall k v. Basic Single => BaseRep Single k v
SingleR Single k v
x

instance (Ord k, Ord v) => HasExp (Bimap k v) (Bimap k v) where
  toExp :: Bimap k v -> Exp (Bimap k v)
toExp Bimap k v
x = BaseRep (BiMap v) k v -> Bimap k v -> Exp (Bimap k v)
forall k (f :: * -> * -> *) v.
(Ord k, Basic f, Iter f) =>
BaseRep f k v -> f k v -> Exp (f k v)
Base BaseRep (BiMap v) k v
forall v k. (Basic (BiMap v), Ord v) => BaseRep (BiMap v) k v
BiMapR Bimap k v
x

instance
  (UnifiedView coin cred pool ptr k v, Ord k, Monoid coin, Ord coin, Ord cred, Ord ptr, Ord pool) =>
  HasExp
    (View coin cred pool ptr k v)
    (View coin cred pool ptr k v)
  where
  toExp :: View coin cred pool ptr k v -> Exp (View coin cred pool ptr k v)
toExp View coin cred pool ptr k v
x = BaseRep (View coin cred pool ptr) k v
-> View coin cred pool ptr k v -> Exp (View coin cred pool ptr k v)
forall k (f :: * -> * -> *) v.
(Ord k, Basic f, Iter f) =>
BaseRep f k v -> f k v -> Exp (f k v)
Base (Tag coin cred pool ptr k v -> BaseRep (View coin cred pool ptr) k v
forall coin cred ptr pool k v.
(Monoid coin, Ord cred, Ord ptr, Ord coin, Ord pool) =>
Tag coin cred pool ptr k v -> BaseRep (View coin cred pool ptr) k v
ViewR Tag coin cred pool ptr k v
forall coin cred pool ptr k v.
UnifiedView coin cred pool ptr k v =>
Tag coin cred pool ptr k v
tag) View coin cred pool ptr k v
x

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

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

dom :: (Ord k, HasExp s (f k v)) => s -> Exp (Sett k ())
dom :: s -> Exp (Sett k ())
dom s
x = Exp (f k v) -> Exp (Sett k ())
forall k (f :: * -> * -> *) v.
Ord k =>
Exp (f k v) -> Exp (Sett k ())
Dom (s -> Exp (f k v)
forall s t. HasExp s t => s -> Exp t
toExp s
x)

rng :: (Ord k, Ord v) => HasExp s (f k v) => s -> Exp (Sett v ())
rng :: s -> Exp (Sett v ())
rng s
x = Exp (f k v) -> Exp (Sett v ())
forall k v (f :: * -> * -> *).
(Ord k, Ord v) =>
Exp (f k v) -> Exp (Sett v ())
Rng (s -> Exp (f k v)
forall s t. HasExp s t => s -> Exp t
toExp s
x)

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

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

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

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

(∈) :: (Show k, Ord k, Iter g, HasExp s (g k ())) => k -> s -> Exp Bool
∈ :: k -> s -> Exp Bool
(∈) k
x s
y = k -> Exp (g k ()) -> Exp Bool
forall k (g :: * -> * -> *).
(Ord k, Iter g, Show k) =>
k -> Exp (g k ()) -> Exp Bool
Elem k
x (s -> Exp (g k ())
forall s t. HasExp s t => s -> Exp t
toExp s
y)

(∉), notelem :: (Show k, Ord k, Iter g, HasExp s (g k ())) => k -> s -> Exp Bool
∉ :: k -> s -> Exp Bool
(∉) k
x s
y = k -> Exp (g k ()) -> Exp Bool
forall k (g :: * -> * -> *).
(Ord k, Iter g, Show k) =>
k -> Exp (g k ()) -> Exp Bool
NotElem k
x (s -> Exp (g k ())
forall s t. HasExp s t => s -> Exp t
toExp s
y)
notelem :: k -> s -> Exp Bool
notelem = k -> s -> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
(∉)

(∪), unionleft :: (Show k, Show v, Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) => s1 -> s2 -> Exp (f k v)
∪ :: s1 -> s2 -> Exp (f k v)
(∪) s1
x s2
y = Exp (f k v) -> Exp (g k v) -> Exp (f k v)
forall k v (k :: * -> * -> *) (n :: * -> * -> *).
(Show k, Show v, Ord k) =>
Exp (k k v) -> Exp (n k v) -> Exp (k k v)
UnionOverrideLeft (s1 -> Exp (f k v)
forall s t. HasExp s t => s -> Exp t
toExp s1
x) (s2 -> Exp (g k v)
forall s t. HasExp s t => s -> Exp t
toExp s2
y)
unionleft :: s1 -> s2 -> Exp (f k v)
unionleft = 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)
(∪)

(⨃), unionright :: (Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) => s1 -> s2 -> Exp (f k v)
⨃ :: s1 -> s2 -> Exp (f k v)
(⨃) s1
x s2
y = Exp (f k v) -> Exp (g k v) -> Exp (f k v)
forall f (g :: * -> * -> *) k (v :: * -> * -> *).
Ord f =>
Exp (g f k) -> Exp (v f k) -> Exp (g f k)
UnionOverrideRight (s1 -> Exp (f k v)
forall s t. HasExp s t => s -> Exp t
toExp s1
x) (s2 -> Exp (g k v)
forall s t. HasExp s t => s -> Exp t
toExp s2
y)
unionright :: s1 -> s2 -> Exp (f k v)
unionright = 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)
(⨃)

(∪+), unionplus :: (Ord k, Monoid n, HasExp s1 (f k n), HasExp s2 (g k n)) => s1 -> s2 -> Exp (f k n)
∪+ :: s1 -> s2 -> Exp (f k n)
(∪+) s1
x s2
y = Exp (f k n) -> Exp (g k n) -> Exp (f k n)
forall k n (f :: * -> * -> *) (g :: * -> * -> *).
(Ord k, Monoid n) =>
Exp (f k n) -> Exp (g k n) -> Exp (f k n)
UnionPlus (s1 -> Exp (f k n)
forall s t. HasExp s t => s -> Exp t
toExp s1
x) (s2 -> Exp (g k n)
forall s t. HasExp s t => s -> Exp t
toExp s2
y)
unionplus :: s1 -> s2 -> Exp (f k n)
unionplus = 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)
(∪+)

singleton :: (Ord k) => k -> v -> Exp (Single k v)
singleton :: k -> v -> Exp (Single k v)
singleton k
k v
v = k -> v -> Exp (Single k v)
forall k v. Ord k => k -> v -> Exp (Single k v)
Singleton k
k v
v

setSingleton :: (Ord k) => k -> Exp (Single k ())
setSingleton :: k -> Exp (Single k ())
setSingleton k
k = k -> Exp (Single k ())
forall v. Ord v => v -> Exp (Single v ())
SetSingleton k
k

(∩), intersect :: (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) => s1 -> s2 -> Exp (Sett k ())
∩ :: s1 -> s2 -> Exp (Sett k ())
(∩) s1
x s2
y = Exp (f k v) -> Exp (g k u) -> Exp (Sett k ())
forall k (f :: * -> * -> *) (g :: * -> * -> *) v u.
(Ord k, Iter f, Iter g) =>
Exp (f k v) -> Exp (g k u) -> Exp (Sett k ())
Intersect (s1 -> Exp (f k v)
forall s t. HasExp s t => s -> Exp t
toExp s1
x) (s2 -> Exp (g k u)
forall s t. HasExp s t => s -> Exp t
toExp s2
y)
intersect :: s1 -> s2 -> Exp (Sett k ())
intersect = 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 ())
(∩)

(⊆), subset :: (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) => s1 -> s2 -> Exp Bool
⊆ :: s1 -> s2 -> Exp Bool
(⊆) s1
x s2
y = Exp (f k v) -> Exp (g k u) -> Exp Bool
forall k (f :: * -> * -> *) (g :: * -> * -> *) v u.
(Ord k, Iter f, Iter g) =>
Exp (f k v) -> Exp (g k u) -> Exp Bool
Subset (s1 -> Exp (f k v)
forall s t. HasExp s t => s -> Exp t
toExp s1
x) (s2 -> Exp (g k u)
forall s t. HasExp s t => s -> Exp t
toExp s2
y)
subset :: s1 -> s2 -> Exp Bool
subset = 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
(⊆)

(➖), setdiff :: (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) => s1 -> s2 -> Exp (f k v)
➖ :: s1 -> s2 -> Exp (f k v)
(➖) s1
x s2
y = Exp (f k v) -> Exp (g k u) -> Exp (f k v)
forall k (f :: * -> * -> *) (g :: * -> * -> *) v u.
(Ord k, Iter f, Iter g) =>
Exp (f k v) -> Exp (g k u) -> Exp (f k v)
SetDiff (s1 -> Exp (f k v)
forall s t. HasExp s t => s -> Exp t
toExp s1
x) (s2 -> Exp (g k u)
forall s t. HasExp s t => s -> Exp t
toExp s2
y)
setdiff :: s1 -> s2 -> Exp (f k v)
setdiff = 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)
(➖)

(≍), keyeq :: (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) => s1 -> s2 -> Exp Bool
≍ :: s1 -> s2 -> Exp Bool
(≍) s1
x s2
y = Exp (f k v) -> Exp (g k u) -> Exp Bool
forall k (f :: * -> * -> *) (g :: * -> * -> *) v u.
(Ord k, Iter f, Iter g) =>
Exp (f k v) -> Exp (g k u) -> Exp Bool
KeyEqual (s1 -> Exp (f k v)
forall s t. HasExp s t => s -> Exp t
toExp s1
x) (s2 -> Exp (g k u)
forall s t. HasExp s t => s -> Exp t
toExp s2
y)
keyeq :: s1 -> s2 -> Exp Bool
keyeq = 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
(≍)

-- ==========================================================================================
-- 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) = Lam t -> String
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

-- 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 :: 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)) = (StringEnv -> Expr (w, x, y, z) t -> String
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, StringEnv -> Expr (w, x, y, z) t -> String
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, StringEnv -> Expr (w, x, y, z) t -> String
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, StringEnv -> Expr (w, x, y, z) t -> String
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 = Pat (d, c, b, a) a -> Expr (w, x, y, z) a -> StringEnv -> StringEnv
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
Expr (w, x, y, z) a
e1 (Pat (d, c, b, a) b -> Expr (w, x, y, z) b -> StringEnv -> StringEnv
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
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 = Pat (d, c, b, a) b -> Expr (w, x, y, z) b -> StringEnv -> StringEnv
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) (d, b) -> Expr (w, x, y, z) b
forall e a b. Expr e (a, b) -> Expr e b
SND Expr (w, x, y, z) t
Expr (w, x, y, z) (d, b)
e) (Pat (d, c, b, a) a -> Expr (w, x, y, z) a -> StringEnv -> StringEnv
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, c) -> Expr (w, x, y, z) a
forall e a b. Expr e (a, b) -> Expr e a
FST Expr (w, x, y, z) t
Expr (w, x, y, z) (a, c)
e) StringEnv
env)

showE :: StringEnv -> (Expr (a, b, c, d) t) -> String
showE :: 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
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ StringEnv -> Expr (a, b, c, d) a -> String
forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE StringEnv
e Expr (a, b, c, d) a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ StringEnv -> Expr (a, b, c, d) b -> String
forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE StringEnv
e Expr (a, b, c, d) b
b String -> ShowS
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) = StringEnv -> Expr (d, c, b, a) v -> String
forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE (Pat (d, c, b, a) s -> Expr (a, b, c, d) s -> StringEnv -> StringEnv
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
Expr (a, b, c, d) s
y (Pat (d, c, b, a) t -> Expr (a, b, c, d) t -> StringEnv -> StringEnv
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
Expr (a, b, c, d) t
x StringEnv
e)) Expr (d, c, b, a) v
expr
showE StringEnv
e (FST Expr (a, b, c, d) (t, b)
f) = String
"(fst " String -> ShowS
forall a. [a] -> [a] -> [a]
++ StringEnv -> Expr (a, b, c, d) (t, b) -> String
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
showE StringEnv
e (SND Expr (a, b, c, d) (a, t)
f) = String
"(snd " String -> ShowS
forall a. [a] -> [a] -> [a]
++ StringEnv -> Expr (a, b, c, d) (a, t) -> String
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 String -> ShowS
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
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ StringEnv -> Expr (a, b, c, d) a -> String
forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE StringEnv
e Expr (a, b, c, d) a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ StringEnv -> Lam (a -> b -> t) -> String
forall t. StringEnv -> Lam t -> String
showL StringEnv
e Lam (a -> b -> t)
oper String -> ShowS
forall a. [a] -> [a] -> [a]
++ StringEnv -> Expr (a, b, c, d) b -> String
forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE StringEnv
e Expr (a, b, c, d) b
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
showE StringEnv
e (HasKey Expr (a, b, c, d) k
k f k v
_datum) = String
"(haskey " String -> ShowS
forall a. [a] -> [a] -> [a]
++ StringEnv -> Expr (a, b, c, d) k -> String
forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE StringEnv
e Expr (a, b, c, d) k
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ?)"
showE StringEnv
e (Neg Expr (a, b, c, d) Bool
x) = String
"(not " String -> ShowS
forall a. [a] -> [a] -> [a]
++ StringEnv -> Expr (a, b, c, d) Bool -> String
forall a b c d t. StringEnv -> Expr (a, b, c, d) t -> String
showE StringEnv
e Expr (a, b, c, d) Bool
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
showE StringEnv
_ (Lit t
n) = t -> String
forall a. Show a => a -> String
show t
n

showL :: StringEnv -> Lam t -> String
showL :: 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
"\\ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ StringEnv -> Pat (d, c, b, a) t -> String
forall any t. StringEnv -> Pat any t -> String
showP StringEnv
e Pat (d, c, b, a) t
p1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ StringEnv -> Pat (d, c, b, a) s -> String
forall any t. StringEnv -> Pat any t -> String
showP StringEnv
e Pat (d, c, b, a) s
p2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ StringEnv -> Expr (d, c, b, a) v -> String
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 :: 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
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ StringEnv -> Pat (d, c, b, a) a -> String
forall any t. StringEnv -> Pat any t -> String
showP StringEnv
env Pat (d, c, b, a) a
p1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ StringEnv -> Pat (d, c, b, a) b -> String
forall any t. StringEnv -> Pat any t -> String
showP StringEnv
env Pat (d, c, b, a) b
p2 String -> ShowS
forall a. [a] -> [a] -> [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 = StringEnv -> Expr (a, b, c, d) t -> String
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

instance Show (Lam t) where
  show :: Lam t -> String
show Lam t
x = StringEnv -> Lam t -> String
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 :: Fun t -> t
apply (Fun Lam t
_e t
f) = t
f

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

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

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

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

constant :: Show c => c -> Fun (a -> b -> c)
constant :: c -> Fun (a -> b -> c)
constant c
c = Lam (a -> b -> c) -> (a -> b -> c) -> Fun (a -> b -> c)
forall t. Lam t -> t -> Fun t
Fun (Pat (a, b, Any, Any) a
-> Pat (a, b, Any, Any) b
-> Expr (a, b, Any, Any) c
-> Lam (a -> b -> c)
forall d c b a m a b.
Pat (d, c, b, a) m
-> Pat (d, c, b, a) a -> Expr (d, c, b, a) b -> Lam (m -> a -> b)
Lam Pat (a, b, Any, Any) a
forall d c b a. Pat (d, c, b, a) d
P1 Pat (a, b, Any, Any) b
forall d c b a. Pat (d, c, b, a) c
P2 (c -> Expr (a, b, Any, Any) c
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 :: f rng v -> Fun (dom -> rng -> Bool)
rngElem f rng v
realset = Lam (dom -> rng -> Bool)
-> (dom -> rng -> Bool) -> Fun (dom -> rng -> Bool)
forall t. Lam t -> t -> Fun t
Fun (Pat (dom, rng, Any, Any) dom
-> Pat (dom, rng, Any, Any) rng
-> Expr (dom, rng, Any, Any) Bool
-> Lam (dom -> rng -> Bool)
forall d c b a m a b.
Pat (d, c, b, a) m
-> Pat (d, c, b, a) a -> Expr (d, c, b, a) b -> Lam (m -> a -> b)
Lam Pat (dom, rng, Any, Any) dom
forall d c b a. Pat (d, c, b, a) d
P1 Pat (dom, rng, Any, Any) rng
forall d c b a. Pat (d, c, b, a) c
P2 (Expr (dom, rng, Any, Any) rng
-> f rng v -> Expr (dom, rng, Any, Any) Bool
forall (f :: * -> * -> *) k e a.
(Iter f, Ord k) =>
Expr e k -> f k a -> Expr e Bool
HasKey Expr (dom, rng, Any, Any) rng
forall d c b a. Expr (d, c, b, a) c
X2 f rng v
realset)) (\dom
_x rng
y -> rng -> f rng v -> Bool
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 :: f dom v -> Fun (dom -> rng -> Bool)
domElem f dom v
realset = Lam (dom -> rng -> Bool)
-> (dom -> rng -> Bool) -> Fun (dom -> rng -> Bool)
forall t. Lam t -> t -> Fun t
Fun (Pat (dom, rng, Any, Any) dom
-> Pat (dom, rng, Any, Any) rng
-> Expr (dom, rng, Any, Any) Bool
-> Lam (dom -> rng -> Bool)
forall d c b a m a b.
Pat (d, c, b, a) m
-> Pat (d, c, b, a) a -> Expr (d, c, b, a) b -> Lam (m -> a -> b)
Lam Pat (dom, rng, Any, Any) dom
forall d c b a. Pat (d, c, b, a) d
P1 Pat (dom, rng, Any, Any) rng
forall d c b a. Pat (d, c, b, a) c
P2 (Expr (dom, rng, Any, Any) dom
-> f dom v -> Expr (dom, rng, Any, Any) Bool
forall (f :: * -> * -> *) k e a.
(Iter f, Ord k) =>
Expr e k -> f k a -> Expr e Bool
HasKey Expr (dom, rng, Any, Any) dom
forall d c b a. Expr (d, c, b, a) d
X1 f dom v
realset)) (\dom
x rng
_y -> dom -> f dom v -> Bool
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 :: Fun (x -> (a, b) -> a)
rngFst = Lam (x -> (a, b) -> a)
-> (x -> (a, b) -> a) -> Fun (x -> (a, b) -> a)
forall t. Lam t -> t -> Fun t
Fun (Pat (x, a, b, a) x
-> Pat (x, a, b, a) (a, b)
-> Expr (x, a, b, a) a
-> Lam (x -> (a, b) -> a)
forall d c b a m a b.
Pat (d, c, b, a) m
-> Pat (d, c, b, a) a -> Expr (d, c, b, a) b -> Lam (m -> a -> b)
Lam Pat (x, a, b, a) x
forall d c b a. Pat (d, c, b, a) d
P1 (Pat (x, a, b, a) a -> Pat (x, a, b, a) b -> Pat (x, a, b, a) (a, b)
forall d c b a.
Pat (d, c, b, a) a -> Pat (d, c, b, a) b -> Pat (d, c, b, a) (a, b)
PPair Pat (x, a, b, a) a
forall d c b a. Pat (d, c, b, a) c
P2 Pat (x, a, b, a) b
forall d c b a. Pat (d, c, b, a) b
P3) Expr (x, a, b, a) a
forall d c b a. Expr (d, c, b, a) c
X2) (\x
_x (a
a, b
_b) -> a
a)

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

compose1 :: Fun (t1 -> t2 -> t3) -> Fun (t1 -> t4 -> t2) -> Fun (t1 -> t4 -> t3)
compose1 :: 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) = Lam (t1 -> t4 -> t3) -> (t1 -> t4 -> t3) -> Fun (t1 -> t4 -> t3)
forall t. Lam t -> t -> Fun t
Fun (Pat (t1, t4, Any, Any) t1
-> Pat (t1, t4, Any, Any) t4
-> Expr (t1, t4, Any, Any) t3
-> Lam (t1 -> t4 -> t3)
forall d c b a m a b.
Pat (d, c, b, a) m
-> Pat (d, c, b, a) a -> Expr (d, c, b, a) b -> Lam (m -> a -> b)
Lam Pat (t1, t4, Any, Any) t1
forall d c b a. Pat (d, c, b, a) d
P1 Pat (t1, t4, Any, Any) t4
forall d c b a. Pat (d, c, b, a) c
P2 (Lam (t1 -> t2 -> t3)
-> Expr (t1, t4, Any, Any) t1
-> Expr (t1, t4, Any, Any) t2
-> Expr (t1, t4, Any, Any) t3
forall a b c e.
Lam (a -> b -> c) -> Expr e a -> Expr e b -> Expr e c
Ap Lam (t1 -> t2 -> t3)
e1 Expr (t1, t4, Any, Any) t1
forall d c b a. Expr (d, c, b, a) d
X1 (Lam (t1 -> t4 -> t2)
-> Expr (t1, t4, Any, Any) t1
-> Expr (t1, t4, Any, Any) t4
-> Expr (t1, t4, Any, Any) t2
forall a b c e.
Lam (a -> b -> c) -> Expr e a -> Expr e b -> Expr e c
Ap Lam (t1 -> t4 -> t2)
e2 Expr (t1, t4, Any, Any) t1
forall d c b a. Expr (d, c, b, a) d
X1 Expr (t1, t4, Any, Any) t4
forall d c b a. Expr (d, c, b, a) 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 :: 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) = Lam (k -> (d, b) -> c)
-> (k -> (d, b) -> c) -> Fun (k -> (d, b) -> c)
forall t. Lam t -> t -> Fun t
Fun (Pat (k, d, b, d) k
-> Pat (k, d, b, d) (d, b)
-> Expr (k, d, b, d) c
-> Lam (k -> (d, b) -> c)
forall d c b a m a b.
Pat (d, c, b, a) m
-> Pat (d, c, b, a) a -> Expr (d, c, b, a) b -> Lam (m -> a -> b)
Lam Pat (k, d, b, d) k
forall d c b a. Pat (d, c, b, a) d
P1 (Pat (k, d, b, d) d -> Pat (k, d, b, d) b -> Pat (k, d, b, d) (d, b)
forall d c b a.
Pat (d, c, b, a) a -> Pat (d, c, b, a) b -> Pat (d, c, b, a) (a, b)
PPair Pat (k, d, b, d) d
forall d c b a. Pat (d, c, b, a) c
P2 Pat (k, d, b, d) b
forall d c b a. Pat (d, c, b, a) b
P3) (Lam (k -> (a, b) -> c)
-> Expr (k, d, b, d) k
-> Expr (k, d, b, d) (a, b)
-> Expr (k, d, b, d) c
forall a b c e.
Lam (a -> b -> c) -> Expr e a -> Expr e b -> Expr e c
Ap Lam (k -> (a, b) -> c)
m Expr (k, d, b, d) k
forall d c b a. Expr (d, c, b, a) d
X1 (Expr (k, d, b, d) a
-> Expr (k, d, b, d) b -> Expr (k, d, b, d) (a, b)
forall e a b. Expr e a -> Expr e b -> Expr e (a, b)
EPair (Lam (k -> d -> a)
-> Expr (k, d, b, d) k
-> Expr (k, d, b, d) d
-> Expr (k, d, b, d) a
forall a b c e.
Lam (a -> b -> c) -> Expr e a -> Expr e b -> Expr e c
Ap Lam (k -> d -> a)
g Expr (k, d, b, d) k
forall d c b a. Expr (d, c, b, a) d
X1 Expr (k, d, b, d) d
forall d c b a. Expr (d, c, b, a) c
X2) Expr (k, d, b, d) b
forall d c b a. Expr (d, c, b, a) 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 :: 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) = (Lam (k -> (a, d) -> c)
-> (k -> (a, d) -> c) -> Fun (k -> (a, d) -> c)
forall t. Lam t -> t -> Fun t
Fun (Pat (k, a, d, a) k
-> Pat (k, a, d, a) (a, d)
-> Expr (k, a, d, a) c
-> Lam (k -> (a, d) -> c)
forall d c b a m a b.
Pat (d, c, b, a) m
-> Pat (d, c, b, a) a -> Expr (d, c, b, a) b -> Lam (m -> a -> b)
Lam Pat (k, a, d, a) k
forall d c b a. Pat (d, c, b, a) d
P1 (Pat (k, a, d, a) a -> Pat (k, a, d, a) d -> Pat (k, a, d, a) (a, d)
forall d c b a.
Pat (d, c, b, a) a -> Pat (d, c, b, a) b -> Pat (d, c, b, a) (a, b)
PPair Pat (k, a, d, a) a
forall d c b a. Pat (d, c, b, a) c
P2 Pat (k, a, d, a) d
forall d c b a. Pat (d, c, b, a) b
P3) (Lam (k -> (a, b) -> c)
-> Expr (k, a, d, a) k
-> Expr (k, a, d, a) (a, b)
-> Expr (k, a, d, a) c
forall a b c e.
Lam (a -> b -> c) -> Expr e a -> Expr e b -> Expr e c
Ap Lam (k -> (a, b) -> c)
m Expr (k, a, d, a) k
forall d c b a. Expr (d, c, b, a) d
X1 (Expr (k, a, d, a) a
-> Expr (k, a, d, a) b -> Expr (k, a, d, a) (a, b)
forall e a b. Expr e a -> Expr e b -> Expr e (a, b)
EPair Expr (k, a, d, a) a
forall d c b a. Expr (d, c, b, a) c
X2 (Lam (k -> d -> b)
-> Expr (k, a, d, a) k
-> Expr (k, a, d, a) d
-> Expr (k, a, d, a) b
forall a b c e.
Lam (a -> b -> c) -> Expr e a -> Expr e b -> Expr e c
Ap Lam (k -> d -> b)
g Expr (k, a, d, a) k
forall d c b a. Expr (d, c, b, a) d
X1 Expr (k, a, d, a) d
forall d c b a. Expr (d, c, b, a) 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 :: 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) = Lam (k -> (a, c) -> d)
-> (k -> (a, c) -> d) -> Fun (k -> (a, c) -> d)
forall t. Lam t -> t -> Fun t
Fun (Pat (k, a, c, a) k
-> Pat (k, a, c, a) (a, c)
-> Expr (k, a, c, a) d
-> Lam (k -> (a, c) -> d)
forall d c b a m a b.
Pat (d, c, b, a) m
-> Pat (d, c, b, a) a -> Expr (d, c, b, a) b -> Lam (m -> a -> b)
Lam Pat (k, a, c, a) k
forall d c b a. Pat (d, c, b, a) d
P1 (Pat (k, a, c, a) a -> Pat (k, a, c, a) c -> Pat (k, a, c, a) (a, c)
forall d c b a.
Pat (d, c, b, a) a -> Pat (d, c, b, a) b -> Pat (d, c, b, a) (a, b)
PPair Pat (k, a, c, a) a
forall d c b a. Pat (d, c, b, a) c
P2 Pat (k, a, c, a) c
forall d c b a. Pat (d, c, b, a) b
P3) (Lam (k -> (a, b) -> d)
-> Expr (k, a, c, a) k
-> Expr (k, a, c, a) (a, b)
-> Expr (k, a, c, a) d
forall a b c e.
Lam (a -> b -> c) -> Expr e a -> Expr e b -> Expr e c
Ap Lam (k -> (a, b) -> d)
ef Expr (k, a, c, a) k
forall d c b a. Expr (d, c, b, a) d
X1 (Expr (k, a, c, a) a
-> Expr (k, a, c, a) b -> Expr (k, a, c, a) (a, b)
forall e a b. Expr e a -> Expr e b -> Expr e (a, b)
EPair Expr (k, a, c, a) a
forall d c b a. Expr (d, c, b, a) c
X2 (Lam (a -> c -> b)
-> Expr (k, a, c, a) a
-> Expr (k, a, c, a) c
-> Expr (k, a, c, a) b
forall a b c e.
Lam (a -> b -> c) -> Expr e a -> Expr e b -> Expr e c
Ap Lam (a -> c -> b)
eg Expr (k, a, c, a) a
forall d c b a. Expr (d, c, b, a) c
X2 Expr (k, a, c, a) c
forall d c b a. Expr (d, c, b, a) 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 :: Fun (k -> v -> Bool) -> Fun (k -> v -> Bool)
nEgate (Fun Lam (k -> v -> Bool)
ef k -> v -> Bool
f) = Lam (k -> v -> Bool) -> (k -> v -> Bool) -> Fun (k -> v -> Bool)
forall t. Lam t -> t -> Fun t
Fun (Pat (k, v, Any, Any) k
-> Pat (k, v, Any, Any) v
-> Expr (k, v, Any, Any) Bool
-> Lam (k -> v -> Bool)
forall d c b a m a b.
Pat (d, c, b, a) m
-> Pat (d, c, b, a) a -> Expr (d, c, b, a) b -> Lam (m -> a -> b)
Lam Pat (k, v, Any, Any) k
forall d c b a. Pat (d, c, b, a) d
P1 Pat (k, v, Any, Any) v
forall d c b a. Pat (d, c, b, a) c
P2 (Expr (k, v, Any, Any) Bool -> Expr (k, v, Any, Any) Bool
forall e. Expr e Bool -> Expr e Bool
Neg (Lam (k -> v -> Bool)
-> Expr (k, v, Any, Any) k
-> Expr (k, v, Any, Any) v
-> Expr (k, v, Any, Any) Bool
forall a b c e.
Lam (a -> b -> c) -> Expr e a -> Expr e b -> Expr e c
Ap Lam (k -> v -> Bool)
ef Expr (k, v, Any, Any) k
forall d c b a. Expr (d, c, b, a) d
X1 Expr (k, v, Any, Any) v
forall d c b a. Expr (d, c, b, a) c
X2))) (\k
x v
y -> Bool -> Bool
not (k -> v -> Bool
f k
x v
y))

always :: Fun (a -> b -> Bool)
always :: Fun (a -> b -> Bool)
always = Bool -> Fun (a -> b -> Bool)
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 :: 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) = Lam (a -> b -> Bool) -> (a -> b -> Bool) -> Fun (a -> b -> Bool)
forall t. Lam t -> t -> Fun t
Fun (Pat (a, b, Any, Any) a
-> Pat (a, b, Any, Any) b
-> Expr (a, b, Any, Any) Bool
-> Lam (a -> b -> Bool)
forall d c b a m a b.
Pat (d, c, b, a) m
-> Pat (d, c, b, a) a -> Expr (d, c, b, a) b -> Lam (m -> a -> b)
Lam Pat (a, b, Any, Any) a
forall d c b a. Pat (d, c, b, a) d
P1 Pat (a, b, Any, Any) b
forall d c b a. Pat (d, c, b, a) c
P2 (Lam (Bool -> Bool -> Bool)
-> Expr (a, b, Any, Any) Bool
-> Expr (a, b, Any, Any) Bool
-> Expr (a, b, Any, Any) Bool
forall a b c e.
Lam (a -> b -> c) -> Expr e a -> Expr e b -> Expr e c
Ap Lam (Bool -> Bool -> Bool)
Both (Lam (a -> b -> Bool)
-> Expr (a, b, Any, Any) a
-> Expr (a, b, Any, Any) b
-> Expr (a, b, Any, Any) Bool
forall a b c e.
Lam (a -> b -> c) -> Expr e a -> Expr e b -> Expr e c
Ap Lam (a -> b -> Bool)
ef Expr (a, b, Any, Any) a
forall d c b a. Expr (d, c, b, a) d
X1 Expr (a, b, Any, Any) b
forall d c b a. Expr (d, c, b, a) c
X2) (Lam (a -> b -> Bool)
-> Expr (a, b, Any, Any) a
-> Expr (a, b, Any, Any) b
-> Expr (a, b, Any, Any) Bool
forall a b c e.
Lam (a -> b -> c) -> Expr e a -> Expr e b -> Expr e c
Ap Lam (a -> b -> Bool)
ff Expr (a, b, Any, Any) a
forall d c b a. Expr (d, c, b, a) d
X1 Expr (a, b, Any, Any) b
forall d c b a. Expr (d, c, b, a) 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 :: (a -> b -> c) -> Fun (a -> b -> c)
lift a -> b -> c
f = Lam (a -> b -> c) -> (a -> b -> c) -> Fun (a -> b -> c)
forall t. Lam t -> t -> Fun t
Fun ((a -> b -> c) -> Lam (a -> b -> c)
forall a b c. (a -> b -> c) -> Lam (a -> 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 :: 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 -> Query k v -> Fun (k -> v -> u) -> Query k u
forall k v u. Ord k => Query k v -> Fun (k -> v -> u) -> Query k u
projD Query k v
f (Fun (k -> v -> u) -> Fun (k -> v -> v) -> Fun (k -> v -> u)
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 -> Query k v -> Query k w -> Fun (k -> (v, w) -> u) -> Query k u
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 (Fun (k -> v -> u) -> Fun (k -> v -> v) -> Fun (k -> v -> u)
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)
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 -> Query k v -> Query k u -> Fun (k -> (v, u) -> u) -> Query k u
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 (Fun (k -> v -> u)
-> Fun (k -> (v, u) -> v) -> Fun (k -> (v, u) -> u)
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) -> Query k v -> Fun (k -> v -> u) -> Query k u
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 :: 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 = Query k v
-> Query k v2 -> Fun (k -> (v, v2) -> (v1, v2)) -> Query k (v1, v2)
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 (Fun (k -> (v1, v2) -> (v1, v2))
-> Fun (k -> v -> v1) -> Fun (k -> (v, v2) -> (v1, v2))
forall k a b c d.
Fun (k -> (a, b) -> c)
-> Fun (k -> d -> a) -> Fun (k -> (d, b) -> c)
compSndL Fun (k -> (v1, v2) -> (v1, v2))
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 = Query k v1
-> Query k v -> Fun (k -> (v1, v) -> (v1, v2)) -> Query k (v1, v2)
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 (Fun (k -> (v1, v2) -> (v1, v2))
-> Fun (k -> v -> v2) -> Fun (k -> (v1, v) -> (v1, v2))
forall k a b c d.
Fun (k -> (a, b) -> c)
-> Fun (k -> d -> b) -> Fun (k -> (a, d) -> c)
compSndR Fun (k -> (v1, v2) -> (v1, v2))
forall v s. Fun (v -> s -> s)
second Fun (k -> v -> v2)
p)
andD Query k v1
f Query k v2
g = Query k v1 -> Query k v2 -> Query k (v1, v2)
forall k v w. Ord k => Query k v -> Query k w -> Query k (v, w)
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 :: 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 = Query k v -> Query k u -> Fun (k -> (v, u) -> v) -> Query k v
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 (Fun (k -> (v1, u) -> v)
-> Fun (k -> v -> v1) -> Fun (k -> (v, u) -> v)
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 = Query k v1 -> Query k u -> Fun (k -> (v1, u) -> v) -> Query k v
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 :: 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 = Query k v -> Query v v -> Fun (k -> (v, v) -> u) -> Query k u
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 (Fun (k -> (v, w) -> u)
-> Fun (v -> v -> w) -> Fun (k -> (v, v) -> u)
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 = Query k v -> Query v w -> Fun (k -> (v, w) -> u) -> Query k u
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 :: 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 = Query k v -> Fun (k -> v -> Bool) -> Query k v
forall k v. Ord k => Query k v -> Fun (k -> v -> Bool) -> Query k v
GuardD Query k v
q1 (Fun (k -> v -> Bool)
-> Fun (k -> v -> Bool) -> Fun (k -> v -> Bool)
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 = Query k v -> Fun (k -> v -> Bool) -> Query k v
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.

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

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

orQ ::
  (Ord k, HasQuery concrete1 k v, HasQuery concrete2 k v) =>
  concrete1 ->
  concrete2 ->
  Fun (v -> v -> v) ->
  Query k v
orQ :: concrete1 -> concrete2 -> Fun (v -> v -> v) -> Query k v
orQ concrete1
x concrete2
y Fun (v -> v -> v)
comb = Query k v -> Query k v -> Fun (v -> v -> v) -> Query k v
forall k v.
Ord k =>
Query k v -> Query k v -> Fun (v -> v -> v) -> Query k v
OrD (concrete1 -> Query k v
forall concrete k v. HasQuery concrete k v => concrete -> Query k v
query concrete1
x) (concrete2 -> Query k v
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 :: concrete1 -> concrete2 -> Fun (k -> (v, w) -> u) -> Query k u
chainQ concrete1
x concrete2
y Fun (k -> (v, w) -> u)
p = Query k v -> Query v w -> Fun (k -> (v, w) -> u) -> Query k u
forall k v w u.
(Ord k, Ord v) =>
Query k v -> Query v w -> Fun (k -> (v, w) -> u) -> Query k u
ChainD (concrete1 -> Query k v
forall concrete k v. HasQuery concrete k v => concrete -> Query k v
query concrete1
x) (concrete2 -> Query v w
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 :: concrete1 -> concrete2 -> Fun (k -> (v, u) -> w) -> Query k w
andPQ concrete1
x concrete2
y Fun (k -> (v, u) -> w)
p = Query k v -> Query k u -> Fun (k -> (v, u) -> w) -> Query k w
forall k v1 u v.
Ord k =>
Query k v1 -> Query k u -> Fun (k -> (v1, u) -> v) -> Query k v
AndPD (concrete1 -> Query k v
forall concrete k v. HasQuery concrete k v => concrete -> Query k v
query concrete1
x) (concrete2 -> Query k u
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 :: concrete -> Fun (k -> v -> Bool) -> Query k v
guardQ concrete
x Fun (k -> v -> Bool)
p = Query k v -> Fun (k -> v -> Bool) -> Query k v
forall k v. Ord k => Query k v -> Fun (k -> v -> Bool) -> Query k v
GuardD (concrete -> Query k v
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 :: concrete1 k v -> concrete2 k u -> Query k v
diffQ concrete1 k v
x concrete2 k u
y = Query k v -> Query k u -> Query k v
forall k v u. Ord k => Query k v -> Query k u -> Query k v
DiffD (concrete1 k v -> Query k v
forall concrete k v. HasQuery concrete k v => concrete -> Query k v
query concrete1 k v
x) (concrete2 k u -> Query k u
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 = BaseRep List k v -> List k v -> Query k v
forall (f :: * -> * -> *) k v.
(Iter f, Ord k) =>
BaseRep f k v -> f k v -> Query k v
BaseD BaseRep List k v
forall k v. Basic List => BaseRep List k v
ListR ((v -> v -> v) -> [(k, v)] -> List k v
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 = BaseRep Sett k () -> Sett k () -> Query k ()
forall (f :: * -> * -> *) k v.
(Iter f, Ord k) =>
BaseRep f k v -> f k v -> Query k v
BaseD BaseRep Sett k ()
forall k. Basic Sett => BaseRep Sett k ()
SetR (Set k -> Sett k ()
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 = BaseRep Map k v -> Map k v -> Query k v
forall (f :: * -> * -> *) k v.
(Iter f, Ord k) =>
BaseRep f k v -> f k v -> Query k v
BaseD BaseRep Map k v
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 = BaseRep Single k v -> Single k v -> Query k v
forall (f :: * -> * -> *) k v.
(Iter f, Ord k) =>
BaseRep f k v -> f k v -> Query k v
BaseD BaseRep Single k v
forall k v. Basic Single => BaseRep Single k v
SingleR Single k v
xs

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

instance
  (UnifiedView coin cred pool ptr k v, Monoid coin, Ord k, Ord coin, Ord cred, Ord ptr, Ord pool) =>
  HasQuery (View coin cred pool ptr k v) k v
  where
  query :: View coin cred pool ptr k v -> Query k v
query View coin cred pool ptr k v
xs = BaseRep (View coin cred pool ptr) k v
-> View coin cred pool ptr k v -> Query k v
forall (f :: * -> * -> *) k v.
(Iter f, Ord k) =>
BaseRep f k v -> f k v -> Query k v
BaseD (Tag coin cred pool ptr k v -> BaseRep (View coin cred pool ptr) k v
forall coin cred ptr pool k v.
(Monoid coin, Ord cred, Ord ptr, Ord coin, Ord pool) =>
Tag coin cred pool ptr k v -> BaseRep (View coin cred pool ptr) k v
ViewR Tag coin cred pool ptr k v
forall coin cred pool ptr k v.
UnifiedView coin cred pool ptr k v =>
Tag coin cred pool ptr k v
tag) View coin cred pool ptr k v
xs

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

ppQuery :: Query k v -> Doc
ppQuery :: Query k v -> Doc
ppQuery (BaseD BaseRep f k v
rep f k v
_f) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (BaseRep f k v -> String
forall a. Show a => a -> String
show BaseRep f k v
rep)
ppQuery (ProjectD Query k v
f Fun (k -> v -> v)
p) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Proj" Doc -> Doc -> Doc
<+> Doc -> Doc
align ([Doc] -> Doc
vsep [Query k v -> Doc
forall k v. Query k v -> Doc
ppQuery Query k v
f, String -> Doc
text (Fun (k -> v -> v) -> String
forall a. Show a => a -> String
show Fun (k -> v -> v)
p)])
ppQuery (AndD Query k v
f Query k w
g) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"And" Doc -> Doc -> Doc
<+> Doc -> Doc
align ([Doc] -> Doc
vsep [Query k v -> Doc
forall k v. Query k v -> Doc
ppQuery Query k v
f, Query k w -> Doc
forall k v. Query k v -> Doc
ppQuery Query k w
g])
ppQuery (ChainD Query k v
f Query v w
g Fun (k -> (v, w) -> v)
p) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Chain" Doc -> Doc -> Doc
<+> Doc -> Doc
align ([Doc] -> Doc
vsep [Query k v -> Doc
forall k v. Query k v -> Doc
ppQuery Query k v
f, Query v w -> Doc
forall k v. Query k v -> Doc
ppQuery Query v w
g, String -> Doc
text (Fun (k -> (v, w) -> v) -> String
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) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Or" Doc -> Doc -> Doc
<+> Doc -> Doc
align ([Doc] -> Doc
vsep [Query k v -> Doc
forall k v. Query k v -> Doc
ppQuery Query k v
f, Query k v -> Doc
forall k v. Query k v -> Doc
ppQuery Query k v
g, String -> Doc
text (Fun (v -> v -> v) -> String
forall a. Show a => a -> String
show Fun (v -> v -> v)
p)])
ppQuery (GuardD Query k v
f Fun (k -> v -> Bool)
p) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Guard" Doc -> Doc -> Doc
<+> Doc -> Doc
align ([Doc] -> Doc
vsep [Query k v -> Doc
forall k v. Query k v -> Doc
ppQuery Query k v
f, String -> Doc
text (Fun (k -> v -> Bool) -> String
forall a. Show a => a -> String
show Fun (k -> v -> Bool)
p)])
ppQuery (DiffD Query k v
f Query k u
g) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Diff" Doc -> Doc -> Doc
<+> Doc -> Doc
align ([Doc] -> Doc
vsep [Query k v -> Doc
forall k v. Query k v -> Doc
ppQuery Query k v
f, Query k u -> Doc
forall k v. Query k v -> Doc
ppQuery Query k u
g])
ppQuery (AndPD Query k v
f Query k u
g Fun (k -> (v, u) -> v)
p) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"AndP" Doc -> Doc -> Doc
<+> Doc -> Doc
align ([Doc] -> Doc
vsep [Query k v -> Doc
forall k v. Query k v -> Doc
ppQuery Query k v
f, Query k u -> Doc
forall k v. Query k v -> Doc
ppQuery Query k u
g, String -> Doc
text (Fun (k -> (v, u) -> v) -> String
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 = Doc -> String
forall a. Show a => a -> String
show (Query k v -> Doc
forall k v. Query k v -> Doc
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 :: 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) <- f a b -> Collect (a, b, f a b)
forall (f :: * -> * -> *) a b.
Iter f =>
f a b -> Collect (a, b, f a b)
nxt f a b
x; (a, b, Query a b) -> Collect (a, b, Query a b)
forall t. t -> Collect t
one (a
k, b
v, BaseRep f a b -> f a b -> Query a b
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) = (Query a v -> Collect (a, v, Query a v))
-> Fun (a -> v -> b) -> Query a v -> Collect (a, b, Query a b)
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 Query a v -> Collect (a, v, Query a v)
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 <- Query a v -> Collect (a, v, Query a v)
forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Query a v
f; (a, w, Query a w)
triple2 <- Query a w -> Collect (a, w, Query a w)
forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Query a w
g; (a, v, Query a v)
-> (a, w, Query a w) -> Collect (a, (v, w), Query a (v, w))
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 <- Query a v -> Collect (a, v, Query a v)
forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Query a v
f; (a, v, Query a v)
-> Query v w -> Fun (a -> (v, w) -> b) -> Collect (a, b, Query a b)
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 <- Query a v -> Collect (a, v, Query a v)
forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Query a v
f; (a, u, Query a u)
triple2 <- Query a u -> Collect (a, u, Query a u)
forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Query a u
g; (a, v, Query a v)
-> (a, u, Query a u)
-> Fun (a -> (v, u) -> b)
-> Collect (a, b, Query a b)
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) = (Query a b -> Collect (a, b, Query a b))
-> Query a b
-> Query a b
-> Fun (b -> b -> b)
-> Collect (a, b, Query a b)
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 a b -> Collect (a, b, Query a b)
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) = (Query a b -> Collect (a, b, Query a b))
-> Fun (a -> b -> Bool) -> Query a b -> Collect (a, b, Query a b)
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)
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 <- Query a b -> Collect (a, b, Query a b)
forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Query a b
f; (a, b, Query a b) -> Query a u -> Collect (a, b, Query a b)
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 :: 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) <- a -> f a b -> Collect (a, b, f a b)
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; (a, b, Query a b) -> Collect (a, b, Query a b)
forall t. t -> Collect t
one (a
k, b
v, BaseRep f a b -> f a b -> Query a b
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) = (Query a v -> Collect (a, v, Query a v))
-> Fun (a -> v -> b) -> Query a v -> Collect (a, b, Query a b)
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 (a -> Query a v -> Collect (a, v, Query a v)
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 <- a -> Query a v -> Collect (a, v, Query a v)
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 <- a -> Query a w -> Collect (a, w, Query a w)
forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
key Query a w
g; (a, v, Query a v)
-> (a, w, Query a w) -> Collect (a, (v, w), Query a (v, w))
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 <- a -> Query a v -> Collect (a, v, Query a v)
forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
key Query a v
f; (a, v, Query a v)
-> Query v w -> Fun (a -> (v, w) -> b) -> Collect (a, b, Query a b)
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 <- a -> Query a v -> Collect (a, v, Query a v)
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 <- a -> Query a u -> Collect (a, u, Query a u)
forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
key Query a u
g; (a, v, Query a v)
-> (a, u, Query a u)
-> Fun (a -> (v, u) -> b)
-> Collect (a, b, Query a b)
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) = (Query a b -> Collect (a, b, Query a b))
-> Query a b
-> Query a b
-> Fun (b -> b -> b)
-> Collect (a, b, Query a b)
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 (a -> Query a b -> Collect (a, b, Query a b)
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) = (Query a b -> Collect (a, b, Query a b))
-> Fun (a -> b -> Bool) -> Query a b -> Collect (a, b, Query a b)
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 (a -> Query a b -> Collect (a, b, Query a b)
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 <- a -> Query a b -> Collect (a, b, Query a b)
forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
key Query a b
f; (a, b, Query a b) -> Query a u -> Collect (a, b, Query a b)
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 :: Query a b -> Collect (a, b, Query a b)
nxt = Query a b -> Collect (a, b, Query a b)
forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery
  lub :: k -> Query k b -> Collect (k, b, Query k b)
lub = k -> Query k b -> Collect (k, b, Query k b)
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 :: (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; (k, u, Query k u) -> Collect (k, u, Query k u)
forall t. t -> Collect t
one (k
k, Fun (k -> v -> u) -> k -> v -> u
forall t. Fun t -> t
apply Fun (k -> v -> u)
p k
k v
v, Query k v -> Fun (k -> v -> u) -> Query k u
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 :: (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 a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
k1 a
k2 of
    Ordering
EQ -> (a, (b1, b2), Query a (b1, b2))
-> Collect (a, (b1, b2), Query a (b1, b2))
forall t. t -> Collect t
one (a
k1, (b1
v1, b2
v2), Query a b1 -> Query a b2 -> Query a (b1, b2)
forall k v w. Ord k => Query k v -> Query k w -> Query k (v, w)
AndD Query a b1
f1 Query a b2
g2)
    Ordering
LT -> do (a, b1, Query a b1)
ftrip' <- a -> Query a b1 -> Collect (a, b1, Query a b1)
forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
k2 Query a b1
f1; (a, b1, Query a b1)
-> (a, b2, Query a b2) -> Collect (a, (b1, b2), Query a (b1, b2))
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' <- a -> Query a b2 -> Collect (a, b2, Query a b2)
forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
k1 Query a b2
g2; (a, b1, Query a b1)
-> (a, b2, Query a b2) -> Collect (a, (b1, b2), Query a (b1, b2))
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 :: (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 b -> Query b w -> Maybe w
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 -> (a, u, Query a u) -> Collect (a, u, Query a u)
forall t. t -> Collect t
one (a
d, Fun (a -> (b, w) -> u) -> a -> (b, w) -> u
forall t. Fun t -> t
apply Fun (a -> (b, w) -> u)
comb a
d (b
r1, w
w), Query a b -> Query b w -> Fun (a -> (b, w) -> u) -> Query a u
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 <- Query a b -> Collect (a, b, Query a b)
forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Query a b
f1; (a, b, Query a b)
-> Query b w -> Fun (a -> (b, w) -> u) -> Collect (a, u, Query a u)
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 :: (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 a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
k1 a
k2 of
    Ordering
EQ -> (a, w, Query a w) -> Collect (a, w, Query a w)
forall t. t -> Collect t
one (a
k1, (Fun (a -> (b1, b2) -> w) -> a -> (b1, b2) -> w
forall t. Fun t -> t
apply Fun (a -> (b1, b2) -> w)
p a
k1 (b1
v1, b2
v2)), Query a b1 -> Query a b2 -> Fun (a -> (b1, b2) -> w) -> Query a w
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' <- a -> Query a b1 -> Collect (a, b1, Query a b1)
forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
k2 Query a b1
f1; (a, b1, Query a b1)
-> (a, b2, Query a b2)
-> Fun (a -> (b1, b2) -> w)
-> Collect (a, w, Query a w)
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' <- a -> Query a b2 -> Collect (a, b2, Query a b2)
forall a b. Ord a => a -> Query a b -> Collect (a, b, Query a b)
lubQuery a
k1 Query a b2
g2; (a, b1, Query a b1)
-> (a, b2, Query a b2)
-> Fun (a -> (b1, b2) -> w)
-> Collect (a, w, Query a w)
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 :: (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 (Collect (a, v, Query k v) -> Maybe (a, v, Query k v)
forall t. Collect t -> Maybe t
hasElem (Query k v -> Collect (a, v, Query k v)
next Query k v
f), Collect (a, v, Query k v) -> Maybe (a, v, Query k v)
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) -> Collect (a, v, Query k v)
forall t. Collect t
none
    (Just (a
k1, v
v1, Query k v
f1), Maybe (a, v, Query k v)
Nothing) -> (a, v, Query k v) -> Collect (a, v, Query k v)
forall t. t -> Collect t
one (a
k1, v
v1, Query k v -> Query k v -> Fun (v -> v -> v) -> Query k v
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)) -> (a, v, Query k v) -> Collect (a, v, Query k v)
forall t. t -> Collect t
one (a
k1, v
v1, Query k v -> Query k v -> Fun (v -> v -> v) -> Query k v
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 a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
k1 a
k2 of
        Ordering
EQ -> (a, v, Query k v) -> Collect (a, v, Query k v)
forall t. t -> Collect t
one (a
k1, Fun (v -> v -> v) -> v -> v -> v
forall t. Fun t -> t
apply Fun (v -> v -> v)
comb v
v1 v
v2, Query k v -> Query k v -> Fun (v -> v -> v) -> Query k v
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 -> (a, v, Query k v) -> Collect (a, v, Query k v)
forall t. t -> Collect t
one (a
k1, v
v1, Query k v -> Query k v -> Fun (v -> v -> v) -> Query k v
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 -> (a, v, Query k v) -> Collect (a, v, Query k v)
forall t. t -> Collect t
one (a
k2, v
v2, Query k v -> Query k v -> Fun (v -> v -> v) -> Query k v
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 :: (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 (Fun (a -> b -> Bool) -> a -> b -> Bool
forall t. Fun t -> t
apply Fun (a -> b -> Bool)
p a
k b
v) then (a, b, Query a b) -> Collect (a, b, Query a b)
forall t. t -> Collect t
one (a
k, b
v, Query a b -> Fun (a -> b -> Bool) -> Query a b
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 <- Query a b -> Collect (a, b, Query a b)
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 :: (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 Collect (k, u, Query k u) -> Maybe (k, u, Query k u)
forall t. Collect t -> Maybe t
hasElem (k -> Query k u -> Collect (k, u, Query k u)
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 -> (k, v, Query k v) -> Collect (k, v, Query k v)
forall t. t -> Collect t
one (k
k1, v
u1, Query k v -> Query k u -> Query k v
forall k v u. Ord k => Query k v -> Query k u -> 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 k -> k -> Ordering
forall a. Ord a => a -> a -> Ordering
compare k
k1 k
k2 of
      Ordering
EQ -> do (k, v, Query k v)
tup <- Query k v -> Collect (k, v, Query k v)
forall a b. Query a b -> Collect (a, b, Query a b)
nxtQuery Query k v
f1; (k, v, Query k v) -> Query k u -> Collect (k, v, Query k v)
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 -> (k, v, Query k v) -> Collect (k, v, Query k v)
forall t. t -> Collect t
one (k
k1, v
u1, Query k v -> Query k u -> Query k v
forall k v u. Ord k => Query k v -> Query k u -> Query k v
DiffD Query k v
f1 Query k u
g)
      Ordering
GT -> (k, v, Query k v) -> Collect (k, v, Query k v)
forall t. t -> Collect t
one (k
k1, v
u1, Query k v -> Query k u -> Query k v
forall k v u. Ord k => Query k v -> Query k u -> Query k v
DiffD Query k v
f1 Query k u
g) -- the hasElem guarantees k1 <= k2, so this case is dead code