{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Constrained.Univ where

import Constrained.List
import Control.Monad.Identity
import Data.Functor.Const
import Data.Kind
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Typeable

class FunctionLike fn where
  -- | The semantics of a function is given by `sem`
  sem :: fn as b -> FunTy as b

-- | Evidence that `fn` exists somewhere in `fnU`. To make it possible
-- for `fnU` to consist of a balanced tree of functions we need the `path`
-- to help GHC disambiguate instances of this class during solving.
class IsMember (fn :: [Type] -> Type -> Type) fnU (path :: [PathElem]) where
  -- | Inject a specific function symbol into a function
  -- universe.
  injectFn0 :: fn as b -> fnU as b

  extractFn0 :: fnU as b -> Maybe (fn as b)

type Member fn univ = IsMember fn univ (Path fn univ)

injectFn :: forall fn fnU as b. Member fn fnU => fn as b -> fnU as b
injectFn :: forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *)
       (path :: [PathElem]) (as :: [*]) b.
IsMember fn fnU path =>
fn as b -> fnU as b
injectFn0 @fn @fnU @(Path fn fnU)

extractFn :: forall fn fnU as b. Member fn fnU => fnU as b -> Maybe (fn as b)
extractFn :: forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fnU as b -> Maybe (fn as b)
extractFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *)
       (path :: [PathElem]) (as :: [*]) b.
IsMember fn fnU path =>
fnU as b -> Maybe (fn as b)
extractFn0 @fn @fnU @(Path fn fnU)

data PathElem = PFix | PLeft | PRight

------------------------------------------------------------------------
-- Fixpoints
------------------------------------------------------------------------

{-
On the most basic level what we are after is a first order representation of
typed functions. Furthermore, we need the representation to be compositional so
that you can plug-in your own functions into the universe.

That might sound like it's no problem, but the issue is with higher-order
functions. Consider:

data ListFn where
  MapFn :: _ '[a] b -> ListFn '[[a]] [b]

What should go in place of `_`? It turns out that you need to specify the global
function universe and make sure the global universe is the same everywhere.

data ListFn fn where
  MapFn :: fn '[a] b -> ListFn fn '[[a]] [b]

-}

newtype Fix (fn :: Univ -> Univ) (as :: [Type]) b = Fix (fn (Fix fn) as b)

deriving via (fn (Fix fn)) instance FunctionLike (fn (Fix fn)) => FunctionLike (Fix fn)
deriving via (fn (Fix fn) as b) instance Eq (fn (Fix fn) as b) => Eq (Fix fn as b)
deriving via (fn (Fix fn) as b) instance Show (fn (Fix fn) as b) => Show (Fix fn as b)

------------------------------------------------------------------------
-- Universes
------------------------------------------------------------------------

type Univ = [Type] -> Type -> Type

-- TODO: there are faster implementation of this
data
  Oneof
    fn
    fn'
    -- NOTE: everything needs to be quantified over the
    -- universe because otherwise it would be impossible
    -- to write higher-order functions (like `foldMap`).
    (fnU :: [Type] -> Type -> Type)
    (as :: [Type])
    b
  = OneofLeft !(fn fnU as b)
  | OneofRight !(fn' fnU as b)

-- | Build a balanced tree of `Oneof` from a list of function universes.
-- NOTE: it is important that this is a balanced tree as that reduces the amount of
-- overhead in `injectFn` and `extractFn` from `O(n)` to `O(log(n))`. Surprisingly,
-- we've observed this making more than 10% difference in runtime on some generation
-- tasks even though the list `as` is typically small (< 20 elements).
type family OneofL as where
  OneofL '[t] = t
  OneofL (t : ts) = Insert t (OneofL ts)

type family Insert a t where
  Insert a (Oneof fn fn') = Oneof fn' (Insert a fn)
  Insert a t = Oneof a t

-- | Compute the path to look up `fn` in `fnU`
type family MPath fn fnU :: Maybe [PathElem] where
  MPath fn fn = 'Just '[]
  MPath fn (Oneof fn' fn'' fnU) = Resolve (MPath fn (fn' fnU)) (MPath fn (fn'' fnU))
  MPath fn (Fix fn') = AddFix (MPath fn (fn' (Fix fn')))
  MPath _ _ = 'Nothing

type family AddFix mpath where
  AddFix ('Just path) = 'Just ('PFix ': path)
  AddFix 'Nothing = 'Nothing

type family Resolve a b where
  Resolve ('Just as) _ = 'Just ('PLeft ': as)
  Resolve _ ('Just bs) = 'Just ('PRight ': bs)
  Resolve _ _ = 'Nothing

type family FromJust m where
  FromJust ('Just a) = a

type family Path fn fn' where
  Path fn fn' = FromJust (MPath fn fn')

instance IsMember fn fn '[] where
  injectFn0 :: forall (as :: [*]) b. fn as b -> fn as b
injectFn0 = forall a. a -> a
id
  extractFn0 :: forall (as :: [*]) b. fn as b -> Maybe (fn as b)
extractFn0 = forall a. a -> Maybe a
Just

instance IsMember fn (fn' (Fix fn')) path => IsMember fn (Fix fn') ('PFix : path) where
  injectFn0 :: forall (as :: [*]) b. fn as b -> Fix fn' as b
injectFn0 fn as b
fn = forall (fn :: ([*] -> * -> *) -> [*] -> * -> *) (as :: [*]) b.
fn (Fix fn) as b -> Fix fn as b
Fix (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *)
       (path :: [PathElem]) (as :: [*]) b.
IsMember fn fnU path =>
fn as b -> fnU as b
injectFn0 @_ @_ @path fn as b
fn)
  extractFn0 :: forall (as :: [*]) b. Fix fn' as b -> Maybe (fn as b)
extractFn0 (Fix fn' (Fix fn') as b
fn) = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *)
       (path :: [PathElem]) (as :: [*]) b.
IsMember fn fnU path =>
fnU as b -> Maybe (fn as b)
extractFn0 @_ @_ @path fn' (Fix fn') as b
fn

instance IsMember fn (fn' fnU) path => IsMember fn (Oneof fn' fn'' fnU) ('PLeft : path) where
  injectFn0 :: forall (as :: [*]) b. fn as b -> Oneof fn' fn'' fnU as b
injectFn0 fn as b
fn = forall {k} (fn :: ([*] -> * -> *) -> [*] -> k -> *)
       (fn' :: ([*] -> * -> *) -> [*] -> k -> *) (fnU :: [*] -> * -> *)
       (as :: [*]) (b :: k).
fn fnU as b -> Oneof fn fn' fnU as b
OneofLeft (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *)
       (path :: [PathElem]) (as :: [*]) b.
IsMember fn fnU path =>
fn as b -> fnU as b
injectFn0 @_ @_ @path fn as b
fn)
  extractFn0 :: forall (as :: [*]) b. Oneof fn' fn'' fnU as b -> Maybe (fn as b)
extractFn0 (OneofLeft fn' fnU as b
fn) = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *)
       (path :: [PathElem]) (as :: [*]) b.
IsMember fn fnU path =>
fnU as b -> Maybe (fn as b)
extractFn0 @_ @_ @path fn' fnU as b
fn
  extractFn0 Oneof fn' fn'' fnU as b
_ = forall a. Maybe a
Nothing

instance IsMember fn (fn'' fnU) path => IsMember fn (Oneof fn' fn'' fnU) ('PRight : path) where
  injectFn0 :: forall (as :: [*]) b. fn as b -> Oneof fn' fn'' fnU as b
injectFn0 fn as b
fn = forall {k} (fn :: ([*] -> * -> *) -> [*] -> k -> *)
       (fn' :: ([*] -> * -> *) -> [*] -> k -> *) (fnU :: [*] -> * -> *)
       (as :: [*]) (b :: k).
fn' fnU as b -> Oneof fn fn' fnU as b
OneofRight (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *)
       (path :: [PathElem]) (as :: [*]) b.
IsMember fn fnU path =>
fn as b -> fnU as b
injectFn0 @_ @_ @path fn as b
fn)
  extractFn0 :: forall (as :: [*]) b. Oneof fn' fn'' fnU as b -> Maybe (fn as b)
extractFn0 (OneofRight fn'' fnU as b
fn) = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *)
       (path :: [PathElem]) (as :: [*]) b.
IsMember fn fnU path =>
fnU as b -> Maybe (fn as b)
extractFn0 @_ @_ @path fn'' fnU as b
fn
  extractFn0 Oneof fn' fn'' fnU as b
_ = forall a. Maybe a
Nothing

instance (FunctionLike (fn fnU), FunctionLike (fn' fnU)) => FunctionLike (Oneof fn fn' fnU) where
  sem :: forall (as :: [*]) b. Oneof fn fn' fnU as b -> FunTy as b
sem (OneofLeft fn fnU as b
f) = forall (fn :: [*] -> * -> *) (as :: [*]) b.
FunctionLike fn =>
fn as b -> FunTy as b
sem fn fnU as b
f
  sem (OneofRight fn' fnU as b
f) = forall (fn :: [*] -> * -> *) (as :: [*]) b.
FunctionLike fn =>
fn as b -> FunTy as b
sem fn' fnU as b
f

instance (Show (fn fnU as b), Show (fn' fnU as b)) => Show (Oneof fn fn' fnU as b) where
  show :: Oneof fn fn' fnU as b -> String
show (OneofLeft fn fnU as b
fn) = forall a. Show a => a -> String
show fn fnU as b
fn
  show (OneofRight fn' fnU as b
fn') = forall a. Show a => a -> String
show fn' fnU as b
fn'

instance (Eq (fn fnU as b), Eq (fn' fnU as b)) => Eq (Oneof fn fn' fnU as b) where
  OneofLeft fn fnU as b
fn == :: Oneof fn fn' fnU as b -> Oneof fn fn' fnU as b -> Bool
== OneofLeft fn fnU as b
fn' = fn fnU as b
fn forall a. Eq a => a -> a -> Bool
== fn fnU as b
fn'
  OneofRight fn' fnU as b
fn == OneofRight fn' fnU as b
fn' = fn' fnU as b
fn forall a. Eq a => a -> a -> Bool
== fn' fnU as b
fn'
  Oneof fn fn' fnU as b
_ == Oneof fn fn' fnU as b
_ = Bool
False

------------------------------------------------------------------------
-- Equality
------------------------------------------------------------------------

equalFn :: forall fn a. (Eq a, Member (EqFn fn) fn) => fn '[a, a] Bool
equalFn :: forall (fn :: [*] -> * -> *) a.
(Eq a, Member (EqFn fn) fn) =>
fn '[a, a] Bool
equalFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn (forall k (fn :: [*] -> * -> *). Eq k => EqFn fn '[k, k] Bool
Equal @_ @fn)

data EqFn (fn :: [Type] -> Type -> Type) as b where
  Equal :: Eq a => EqFn fn '[a, a] Bool

deriving instance Eq (EqFn fn as b)
deriving instance Show (EqFn fn as b)

instance FunctionLike (EqFn fn) where
  sem :: forall (as :: [*]) b. EqFn fn as b -> FunTy as b
sem EqFn fn as b
Equal = forall a. Eq a => a -> a -> Bool
(==)

------------------------------------------------------------------------
-- Booleans
------------------------------------------------------------------------

notFn :: forall fn. Member (BoolFn fn) fn => fn '[Bool] Bool
notFn :: forall (fn :: [*] -> * -> *).
Member (BoolFn fn) fn =>
fn '[Bool] Bool
notFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *). BoolFn fn '[Bool] Bool
Not @fn

orFn :: forall fn. Member (BoolFn fn) fn => fn '[Bool, Bool] Bool
orFn :: forall (fn :: [*] -> * -> *).
Member (BoolFn fn) fn =>
fn '[Bool, Bool] Bool
orFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *). BoolFn fn '[Bool, Bool] Bool
Or @fn

-- | Operations on Bool.
--   One might expect   And :: BoolFn fn '[Bool, Bool] Bool
--   But this is problematic because a Term like ( p x &&. q y ) has to solve for
--   x or y first, choose x, so once x is fixed, it might be impossible to solve for y
--   Luckily we can get conjuction by using Preds, in fact using Preds, the x and y
--   can even be the same variable.
--   Or can be problematic too (by using a form of DeMorgan's laws: x && y = not(not x || not y))
--   but while that is possible, there are many scenarios which can only be specified using Or.
--   If one inadvertantly uses a form of DeMorgan's laws, the worst that can happen is an ErrorSpec
--   is returned, and the user can reformulate using Preds. So Or is incomplete, but sound, when it works.
data BoolFn (fn :: [Type] -> Type -> Type) as b where
  Not :: BoolFn fn '[Bool] Bool
  Or :: BoolFn fn '[Bool, Bool] Bool

deriving instance Eq (BoolFn fn as b)
deriving instance Show (BoolFn fn as b)

instance FunctionLike (BoolFn fn) where
  sem :: forall (as :: [*]) b. BoolFn fn as b -> FunTy as b
sem BoolFn fn as b
Not = Bool -> Bool
not
  sem BoolFn fn as b
Or = Bool -> Bool -> Bool
(||)

------------------------------------------------------------------------
-- Pairs
------------------------------------------------------------------------

data Prod a b = Prod {forall a b. Prod a b -> a
prodFst :: a, forall a b. Prod a b -> b
prodSnd :: b}
  deriving (Prod a b -> Prod a b -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b. (Eq a, Eq b) => Prod a b -> Prod a b -> Bool
/= :: Prod a b -> Prod a b -> Bool
$c/= :: forall a b. (Eq a, Eq b) => Prod a b -> Prod a b -> Bool
== :: Prod a b -> Prod a b -> Bool
$c== :: forall a b. (Eq a, Eq b) => Prod a b -> Prod a b -> Bool
Eq, Prod a b -> Prod a b -> Bool
Prod a b -> Prod a b -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a} {b}. (Ord a, Ord b) => Eq (Prod a b)
forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Bool
forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Ordering
forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Prod a b
min :: Prod a b -> Prod a b -> Prod a b
$cmin :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Prod a b
max :: Prod a b -> Prod a b -> Prod a b
$cmax :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Prod a b
>= :: Prod a b -> Prod a b -> Bool
$c>= :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Bool
> :: Prod a b -> Prod a b -> Bool
$c> :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Bool
<= :: Prod a b -> Prod a b -> Bool
$c<= :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Bool
< :: Prod a b -> Prod a b -> Bool
$c< :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Bool
compare :: Prod a b -> Prod a b -> Ordering
$ccompare :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Ordering
Ord, Int -> Prod a b -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> Prod a b -> ShowS
forall a b. (Show a, Show b) => [Prod a b] -> ShowS
forall a b. (Show a, Show b) => Prod a b -> String
showList :: [Prod a b] -> ShowS
$cshowList :: forall a b. (Show a, Show b) => [Prod a b] -> ShowS
show :: Prod a b -> String
$cshow :: forall a b. (Show a, Show b) => Prod a b -> String
showsPrec :: Int -> Prod a b -> ShowS
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> Prod a b -> ShowS
Show)

fstFn :: forall fn a b. Member (PairFn fn) fn => fn '[Prod a b] a
fstFn :: forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[Prod a b] a
fstFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a k. PairFn fn '[Prod a k] a
Fst @fn

sndFn :: forall fn a b. Member (PairFn fn) fn => fn '[Prod a b] b
sndFn :: forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[Prod a b] b
sndFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) k b. PairFn fn '[Prod k b] b
Snd @fn

pairFn :: forall fn a b. Member (PairFn fn) fn => fn '[a, b] (Prod a b)
pairFn :: forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[a, b] (Prod a b)
pairFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) k v. PairFn fn '[k, v] (Prod k v)
Pair @fn

data PairFn (fn :: [Type] -> Type -> Type) args res where
  Pair :: PairFn fn '[a, b] (Prod a b)
  Fst :: PairFn fn '[Prod a b] a
  Snd :: PairFn fn '[Prod a b] b

deriving instance Show (PairFn fn args res)
deriving instance Eq (PairFn fn args res)

instance FunctionLike (PairFn fn) where
  sem :: forall (as :: [*]) b. PairFn fn as b -> FunTy as b
sem = \case
    PairFn fn as b
Pair -> forall a b. a -> b -> Prod a b
Prod
    PairFn fn as b
Fst -> forall a b. Prod a b -> a
prodFst
    PairFn fn as b
Snd -> forall a b. Prod a b -> b
prodSnd

type family ProdOver as where
  ProdOver '[] = ()
  ProdOver '[a] = a
  ProdOver (a : as) = Prod a (ProdOver as)

listToProd :: (ProdOver as -> r) -> List Identity as -> r
listToProd :: forall (as :: [*]) r. (ProdOver as -> r) -> List Identity as -> r
listToProd ProdOver as -> r
k List Identity as
Nil = ProdOver as -> r
k ()
listToProd ProdOver as -> r
k (Identity a
a :> List Identity as1
Nil) = ProdOver as -> r
k a
a
listToProd ProdOver as -> r
k (Identity a
a :> Identity a
b :> List Identity as1
as) = ProdOver as -> r
k (forall a b. a -> b -> Prod a b
Prod a
a (forall (as :: [*]) r. (ProdOver as -> r) -> List Identity as -> r
listToProd forall a. a -> a
id (Identity a
b forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Identity as1
as)))

prodToList :: forall as. TypeList as => ProdOver as -> List Identity as
prodToList :: forall (as :: [*]). TypeList as => ProdOver as -> List Identity as
prodToList = forall (ts :: [*]).
List (Const ()) ts -> ProdOver ts -> List Identity ts
go (forall (as :: [*]). TypeList as => List (Const ()) as
listShape @as)
  where
    go ::
      forall ts.
      List (Const ()) ts ->
      ProdOver ts ->
      List Identity ts
    go :: forall (ts :: [*]).
List (Const ()) ts -> ProdOver ts -> List Identity ts
go List (Const ()) ts
Nil ProdOver ts
_ = forall {k} (f :: k -> *). List f '[]
Nil
    go (Const () a
_ :> List (Const ()) as1
Nil) ProdOver ts
a = forall a. a -> Identity a
Identity ProdOver ts
a forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil
    go (Const () a
_ :> Const () a
ix :> List (Const ()) as1
ixs) (Prod a
a ProdOver (a : as1)
as) = forall a. a -> Identity a
Identity a
a forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall (ts :: [*]).
List (Const ()) ts -> ProdOver ts -> List Identity ts
go (Const () a
ix forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List (Const ()) as1
ixs) ProdOver (a : as1)
as

appendProd ::
  forall xs ys.
  (TypeList xs, TypeList ys) =>
  ProdOver xs ->
  ProdOver ys ->
  ProdOver (Append xs ys)
appendProd :: forall (xs :: [*]) (ys :: [*]).
(TypeList xs, TypeList ys) =>
ProdOver xs -> ProdOver ys -> ProdOver (Append xs ys)
appendProd ProdOver xs
xs ProdOver ys
ys = forall (as :: [*]) r. (ProdOver as -> r) -> List Identity as -> r
listToProd forall a. a -> a
id (forall {a} (f :: a -> *) (as :: [a]) (bs :: [a]).
List f as -> List f bs -> List f (Append as bs)
appendList @Identity @xs @ys (forall (as :: [*]). TypeList as => ProdOver as -> List Identity as
prodToList ProdOver xs
xs) (forall (as :: [*]). TypeList as => ProdOver as -> List Identity as
prodToList ProdOver ys
ys))

splitProd ::
  forall xs ys.
  (TypeList xs, TypeList ys) =>
  ProdOver (Append xs ys) ->
  Prod (ProdOver xs) (ProdOver ys)
splitProd :: forall (xs :: [*]) (ys :: [*]).
(TypeList xs, TypeList ys) =>
ProdOver (Append xs ys) -> Prod (ProdOver xs) (ProdOver ys)
splitProd = forall (as :: [*]) (bs :: [*]).
List (Const ()) as
-> List (Const ()) bs
-> ProdOver (Append as bs)
-> Prod (ProdOver as) (ProdOver bs)
go (forall (as :: [*]). TypeList as => List (Const ()) as
listShape @xs) (forall (as :: [*]). TypeList as => List (Const ()) as
listShape @ys)
  where
    go ::
      List (Const ()) as ->
      List (Const ()) bs ->
      ProdOver (Append as bs) ->
      Prod (ProdOver as) (ProdOver bs)
    go :: forall (as :: [*]) (bs :: [*]).
List (Const ()) as
-> List (Const ()) bs
-> ProdOver (Append as bs)
-> Prod (ProdOver as) (ProdOver bs)
go List (Const ()) as
Nil List (Const ()) bs
_ ProdOver (Append as bs)
p = forall a b. a -> b -> Prod a b
Prod () ProdOver (Append as bs)
p
    go (Const () a
_ :> List (Const ()) as1
Nil) List (Const ()) bs
Nil ProdOver (Append as bs)
p = forall a b. a -> b -> Prod a b
Prod ProdOver (Append as bs)
p ()
    go (Const () a
_ :> List (Const ()) as1
Nil) (Const () a
_ :> List (Const ()) as1
_) ProdOver (Append as bs)
p = ProdOver (Append as bs)
p
    go (Const () a
_ :> Const () a
a :> List (Const ()) as1
as) List (Const ()) bs
bs (Prod a
x ProdOver (a : Append as1 bs)
xs) = forall a b. a -> b -> Prod a b
Prod (forall a b. a -> b -> Prod a b
Prod a
x ProdOver (a : as1)
p0) ProdOver bs
p1
      where
        Prod ProdOver (a : as1)
p0 ProdOver bs
p1 = forall (as :: [*]) (bs :: [*]).
List (Const ()) as
-> List (Const ()) bs
-> ProdOver (Append as bs)
-> Prod (ProdOver as) (ProdOver bs)
go (Const () a
a forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List (Const ()) as1
as) List (Const ()) bs
bs ProdOver (a : Append as1 bs)
xs

------------------------------------------------------------------------
-- Sums
------------------------------------------------------------------------

data Sum a b
  = SumLeft a
  | SumRight b
  deriving (Sum a b -> Sum a b -> Bool
Sum a b -> Sum a b -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a} {b}. (Ord a, Ord b) => Eq (Sum a b)
forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Bool
forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Ordering
forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Sum a b
min :: Sum a b -> Sum a b -> Sum a b
$cmin :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Sum a b
max :: Sum a b -> Sum a b -> Sum a b
$cmax :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Sum a b
>= :: Sum a b -> Sum a b -> Bool
$c>= :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Bool
> :: Sum a b -> Sum a b -> Bool
$c> :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Bool
<= :: Sum a b -> Sum a b -> Bool
$c<= :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Bool
< :: Sum a b -> Sum a b -> Bool
$c< :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Bool
compare :: Sum a b -> Sum a b -> Ordering
$ccompare :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Ordering
Ord, Sum a b -> Sum a b -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b. (Eq a, Eq b) => Sum a b -> Sum a b -> Bool
/= :: Sum a b -> Sum a b -> Bool
$c/= :: forall a b. (Eq a, Eq b) => Sum a b -> Sum a b -> Bool
== :: Sum a b -> Sum a b -> Bool
$c== :: forall a b. (Eq a, Eq b) => Sum a b -> Sum a b -> Bool
Eq, Int -> Sum a b -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> Sum a b -> ShowS
forall a b. (Show a, Show b) => [Sum a b] -> ShowS
forall a b. (Show a, Show b) => Sum a b -> String
showList :: [Sum a b] -> ShowS
$cshowList :: forall a b. (Show a, Show b) => [Sum a b] -> ShowS
show :: Sum a b -> String
$cshow :: forall a b. (Show a, Show b) => Sum a b -> String
showsPrec :: Int -> Sum a b -> ShowS
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> Sum a b -> ShowS
Show)

injLeftFn :: forall fn a b. Member (SumFn fn) fn => fn '[a] (Sum a b)
injLeftFn :: forall (fn :: [*] -> * -> *) a b.
Member (SumFn fn) fn =>
fn '[a] (Sum a b)
injLeftFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn @(SumFn fn) @fn forall (fn :: [*] -> * -> *) k v. SumFn fn '[k] (Sum k v)
InjLeft

injRightFn :: forall fn a b. Member (SumFn fn) fn => fn '[b] (Sum a b)
injRightFn :: forall (fn :: [*] -> * -> *) a b.
Member (SumFn fn) fn =>
fn '[b] (Sum a b)
injRightFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn @(SumFn fn) @fn forall (fn :: [*] -> * -> *) k v. SumFn fn '[k] (Sum v k)
InjRight

data SumFn (fn :: [Type] -> Type -> Type) args res where
  InjLeft :: SumFn fn '[a] (Sum a b)
  InjRight :: SumFn fn '[b] (Sum a b)

deriving instance Show (SumFn fn args res)
deriving instance Eq (SumFn fn args res)

instance FunctionLike (SumFn fn) where
  sem :: forall (as :: [*]) b. SumFn fn as b -> FunTy as b
sem = \case
    SumFn fn as b
InjLeft -> forall a b. a -> Sum a b
SumLeft
    SumFn fn as b
InjRight -> forall a b. b -> Sum a b
SumRight

type family SumOver as where
  SumOver '[a] = a
  SumOver (a : as) = Sum a (SumOver as)

------------------------------------------------------------------------
-- Sets
------------------------------------------------------------------------

singletonFn :: forall fn a. (Member (SetFn fn) fn, Ord a) => fn '[a] (Set a)
singletonFn :: forall (fn :: [*] -> * -> *) a.
(Member (SetFn fn) fn, Ord a) =>
fn '[a] (Set a)
singletonFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn forall a b. (a -> b) -> a -> b
$ forall k (fn :: [*] -> * -> *). Ord k => SetFn fn '[k] (Set k)
Singleton @_ @fn

unionFn ::
  forall fn a. (Member (SetFn fn) fn, Ord a, Show a, Typeable a) => fn '[Set a, Set a] (Set a)
unionFn :: forall (fn :: [*] -> * -> *) a.
(Member (SetFn fn) fn, Ord a, Show a, Typeable a) =>
fn '[Set a, Set a] (Set a)
unionFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn forall a b. (a -> b) -> a -> b
$ forall k (fn :: [*] -> * -> *).
(Ord k, Show k, Typeable k) =>
SetFn fn '[Set k, Set k] (Set k)
Union @_ @fn

subsetFn ::
  forall fn a. (Member (SetFn fn) fn, Ord a, Show a, Typeable a) => fn '[Set a, Set a] Bool
subsetFn :: forall (fn :: [*] -> * -> *) a.
(Member (SetFn fn) fn, Ord a, Show a, Typeable a) =>
fn '[Set a, Set a] Bool
subsetFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn forall a b. (a -> b) -> a -> b
$ forall k (fn :: [*] -> * -> *).
(Ord k, Show k, Typeable k) =>
SetFn fn '[Set k, Set k] Bool
Subset @_ @fn

memberFn :: forall fn a. (Member (SetFn fn) fn, Ord a, Show a, Typeable a) => fn '[a, Set a] Bool
memberFn :: forall (fn :: [*] -> * -> *) a.
(Member (SetFn fn) fn, Ord a, Show a, Typeable a) =>
fn '[a, Set a] Bool
memberFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn forall a b. (a -> b) -> a -> b
$ forall k (fn :: [*] -> * -> *).
(Ord k, Show k, Typeable k) =>
SetFn fn '[k, Set k] Bool
Member @_ @fn

elemFn :: forall fn a. (Member (SetFn fn) fn, Eq a, Show a, Typeable a) => fn '[a, [a]] Bool
elemFn :: forall (fn :: [*] -> * -> *) a.
(Member (SetFn fn) fn, Eq a, Show a, Typeable a) =>
fn '[a, [a]] Bool
elemFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn forall a b. (a -> b) -> a -> b
$ forall k (fn :: [*] -> * -> *).
(Eq k, Show k, Typeable k) =>
SetFn fn '[k, [k]] Bool
Elem @_ @fn

disjointFn ::
  forall fn a. (Member (SetFn fn) fn, Ord a, Show a, Typeable a) => fn '[Set a, Set a] Bool
disjointFn :: forall (fn :: [*] -> * -> *) a.
(Member (SetFn fn) fn, Ord a, Show a, Typeable a) =>
fn '[Set a, Set a] Bool
disjointFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn forall a b. (a -> b) -> a -> b
$ forall k (fn :: [*] -> * -> *).
(Ord k, Show k, Typeable k) =>
SetFn fn '[Set k, Set k] Bool
Disjoint @_ @fn

fromListFn :: forall fn a. (Member (SetFn fn) fn, Ord a) => fn '[[a]] (Set a)
fromListFn :: forall (fn :: [*] -> * -> *) a.
(Member (SetFn fn) fn, Ord a) =>
fn '[[a]] (Set a)
fromListFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn forall a b. (a -> b) -> a -> b
$ forall k (fn :: [*] -> * -> *). Ord k => SetFn fn '[[k]] (Set k)
FromList @_ @fn

data SetFn (fn :: [Type] -> Type -> Type) args res where
  Subset :: (Ord a, Show a, Typeable a) => SetFn fn '[Set a, Set a] Bool
  Disjoint :: (Ord a, Show a, Typeable a) => SetFn fn '[Set a, Set a] Bool
  Member :: (Ord a, Show a, Typeable a) => SetFn fn '[a, Set a] Bool
  Singleton :: Ord a => SetFn fn '[a] (Set a)
  Union :: (Ord a, Show a, Typeable a) => SetFn fn '[Set a, Set a] (Set a)
  Elem :: (Eq a, Show a, Typeable a) => SetFn fn '[a, [a]] Bool
  FromList :: Ord a => SetFn fn '[[a]] (Set a)

deriving instance Show (SetFn fn args res)
deriving instance Eq (SetFn fn args res)

instance FunctionLike (SetFn fn) where
  sem :: forall (as :: [*]) b. SetFn fn as b -> FunTy as b
sem = \case
    SetFn fn as b
Subset -> forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf
    SetFn fn as b
Disjoint -> forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint
    SetFn fn as b
Member -> forall a. Ord a => a -> Set a -> Bool
Set.member
    SetFn fn as b
Singleton -> forall a. a -> Set a
Set.singleton
    SetFn fn as b
Union -> forall a. Semigroup a => a -> a -> a
(<>)
    SetFn fn as b
Elem -> forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem
    SetFn fn as b
FromList -> forall a. Ord a => [a] -> Set a
Set.fromList

------------------------------------------------------------------------
-- Maps
------------------------------------------------------------------------

data MapFn (fn :: [Type] -> Type -> Type) args res where
  Dom :: Ord k => MapFn fn '[Map k v] (Set k)
  Rng :: MapFn fn '[Map k v] [v]
  Lookup :: Ord k => MapFn fn '[k, Map k v] (Maybe v)

deriving instance Show (MapFn fn args res)
deriving instance Eq (MapFn fn args res)

instance FunctionLike (MapFn fn) where
  sem :: forall (as :: [*]) b. MapFn fn as b -> FunTy as b
sem = \case
    MapFn fn as b
Dom -> forall k a. Map k a -> Set k
Map.keysSet
    MapFn fn as b
Rng -> forall k a. Map k a -> [a]
Map.elems
    MapFn fn as b
Lookup -> forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup

domFn :: forall fn k v. (Member (MapFn fn) fn, Ord k) => fn '[Map k v] (Set k)
domFn :: forall (fn :: [*] -> * -> *) k v.
(Member (MapFn fn) fn, Ord k) =>
fn '[Map k v] (Set k)
domFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn forall a b. (a -> b) -> a -> b
$ forall k (fn :: [*] -> * -> *) v.
Ord k =>
MapFn fn '[Map k v] (Set k)
Dom @_ @fn

rngFn :: forall fn k v. Member (MapFn fn) fn => fn '[Map k v] [v]
rngFn :: forall (fn :: [*] -> * -> *) k v.
Member (MapFn fn) fn =>
fn '[Map k v] [v]
rngFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) k v. MapFn fn '[Map k v] [v]
Rng @fn

lookupFn :: forall fn k v. (Member (MapFn fn) fn, Ord k) => fn '[k, Map k v] (Maybe v)
lookupFn :: forall (fn :: [*] -> * -> *) k v.
(Member (MapFn fn) fn, Ord k) =>
fn '[k, Map k v] (Maybe v)
lookupFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn forall a b. (a -> b) -> a -> b
$ forall k (fn :: [*] -> * -> *) v.
Ord k =>
MapFn fn '[k, Map k v] (Maybe v)
Lookup @_ @fn