{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeOperators         #-}

module Language.Expression.GeneralOp where

-- import           Data.Typeable

import           Data.Vinyl
-- import           Data.Vinyl.Functor
-- import           Data.Vinyl.TypeLevel

import           Language.Expression
import           Language.Expression.Pretty

data GeneralOp op t a where
  Op :: RMap as => op as r -> Rec t as -> GeneralOp op t r

class EvalOpAt k op where
  evalMany :: op as r -> Rec k as -> k r

-- class EqOpMany op where
--   liftEqMany
--     :: op as a -> op bs b

--     -> (forall xs. (AllConstrained Eq xs, RecApplicative xs) =>
--         Rec f xs -> Rec g xs -> Bool)

--     -> Rec f as -> Rec g bs -> Bool


class PrettyOp op where
  prettysPrecOp :: Pretty1 t => Int -> op as a -> Rec t as -> ShowS

instance HFunctor (GeneralOp op) where

instance HTraversable (GeneralOp op) where
  htraverse :: (forall (b :: u). t b -> f (t' b))
-> GeneralOp op t a -> f (GeneralOp op t' a)
htraverse forall (b :: u). t b -> f (t' b)
f = \case
    Op op as a
o Rec t as
args -> op as a -> Rec t' as -> GeneralOp op t' a
forall u k (as :: [u]) (op :: [u] -> k -> *) (r :: k)
       (t :: u -> *).
RMap as =>
op as r -> Rec t as -> GeneralOp op t r
Op op as a
o (Rec t' as -> GeneralOp op t' a)
-> f (Rec t' as) -> f (GeneralOp op t' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (b :: u). t b -> f (t' b)) -> Rec t as -> f (Rec t' as)
forall u (h :: * -> *) (f :: u -> *) (g :: u -> *) (rs :: [u]).
Applicative h =>
(forall (x :: u). f x -> h (g x)) -> Rec f rs -> h (Rec g rs)
rtraverse forall (b :: u). t b -> f (t' b)
f Rec t as
args


instance (EvalOpAt k op) => HFoldableAt k (GeneralOp op) where
  hfoldMap :: (forall (b :: k). t b -> k b) -> GeneralOp op t a -> k a
hfoldMap forall (b :: k). t b -> k b
f = \case
    Op op as a
o Rec t as
args -> op as a -> Rec k as -> k a
forall k (k :: k -> *) (op :: [k] -> k -> *) (as :: [k]) (r :: k).
EvalOpAt k op =>
op as r -> Rec k as -> k r
evalMany op as a
o ((forall (b :: k). t b -> k b) -> Rec t as -> Rec k as
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap forall (b :: k). t b -> k b
f Rec t as
args)


-- instance EqOpMany op => HEq (GeneralOp op) where
--   liftHEq le _ (Op o1 (xs :: Rec f as)) (Op o2 (ys :: Rec g bs)) =
--     liftEqMany o1 o2 liftEqAll xs ys

--     where
--       liftEqAll
--         :: (AllConstrained Eq xs, RecApplicative xs)
--         => Rec f xs -> Rec g xs -> Bool
--       liftEqAll (xs' :: Rec f xs) ys' =
--         let
--           eqList :: Rec (Lift (->) f (Lift (->) g (Const Bool))) xs
--           eqList = rpureConstrained (Proxy :: Proxy Eq)
--             (Lift $ \x -> Lift $ Const . le (==) x)
--         in and . recordToList $ eqList <<*>> xs' <<*>> ys'

instance PrettyOp op => Pretty2 (GeneralOp op) where
  prettys2Prec :: Int -> GeneralOp op t a -> ShowS
prettys2Prec Int
p = \case
    Op op as a
op Rec t as
args -> Int -> op as a -> Rec t as -> ShowS
forall u k (op :: [u] -> k -> *) (t :: u -> *) (as :: [u])
       (a :: k).
(PrettyOp op, Pretty1 t) =>
Int -> op as a -> Rec t as -> ShowS
prettysPrecOp Int
p op as a
op Rec t as
args