{-# OPTIONS_HADDOCK hide #-}
{-# OPTIONS_GHC -fno-warn-missing-signatures #-}

{-# LANGUAGE CPP                   #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE ViewPatterns          #-}

module Cubix.Language.JavaScript.Parametric.Full.Types where

#ifndef ONLY_ONE_LANGUAGE
import qualified Data.Set as Set
import Data.Type.Equality ( (:~:)(..), gcastWith )

import Data.Comp.Multi ( (:<:), inject, project, Cxt, Term )
import Data.Comp.Multi.Derive ( derive, makeHFunctor, makeHTraversable, makeHFoldable,
                                    makeEqHF, makeShowHF, makeOrdHF )

import qualified Language.Haskell.TH as TH

import Data.Comp.Multi.Strategy.Classification (DynCase(..) )
import qualified Language.JavaScript.Parser.AST as JS
import Data.Comp.Trans ( runCompTrans, deriveMultiComp, withExcludedNames, standardExcludedNames, makeSumType )

import Cubix.Language.Info
import Cubix.Language.JavaScript.Parametric.Full.Names
import Cubix.Language.Parametric.Derive

-----------------------------------------------------------


do let excludedNames = Set.union standardExcludedNames (Set.fromList [''JS.JSCommaList, ''JS.JSCommaTrailingList])
   runCompTrans $ withExcludedNames excludedNames $ deriveMultiComp ''JS.JSAST

-----------------------------------------------------------


-- I'd prefer to have labels named "JSCommaListL" and "JSCommaList",
-- but the current implementation of comptrans will just use (JS.JSCommaList l) as a label

type JSCommaList l = JS.JSCommaList l
data JSCommaListF e l where
  JSLCons :: e (JSCommaList l) -> e JSAnnotL -> e l -> JSCommaListF e (JSCommaList l)
  JSLOne  :: e l -> JSCommaListF e (JSCommaList l)
  JSLNil  :: JSCommaListF e (JSCommaList t)

type JSCommaTrailingList l = JS.JSCommaTrailingList l
data JSCommaTrailingListF e l where
  JSCTLComma :: e (JSCommaList l) -> e JSAnnotL -> JSCommaTrailingListF e (JSCommaTrailingList l)
  JSCTLNone  :: e (JSCommaList l) -> JSCommaTrailingListF e (JSCommaTrailingList l)



instance {-# OVERLAPPING #-} (JSCommaListF :<: g, DynCase (Cxt h g a) l) => DynCase (Cxt h g a) (JSCommaList l) where
  dyncase :: Cxt h g a b -> Maybe (b :~: JSCommaList l)
dyncase (Cxt h g a b -> Maybe (JSCommaListF (Cxt h g a) b)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just JSLNil) = Maybe (b :~: JSCommaList l)
forall a. Maybe a
Nothing
  dyncase (Cxt h g a b -> Maybe (JSCommaListF (Cxt h g a) b)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (JSLOne x :: Cxt h g a l
x)) = do (l :~: l
p :: _ :~: l) <- Cxt h g a l -> Maybe (l :~: l)
forall (f :: * -> *) a b. DynCase f a => f b -> Maybe (b :~: a)
dyncase Cxt h g a l
x
                                            (b :~: JSCommaList l) -> Maybe (b :~: JSCommaList l)
forall (m :: * -> *) a. Monad m => a -> m a
return ((b :~: JSCommaList l) -> Maybe (b :~: JSCommaList l))
-> (b :~: JSCommaList l) -> Maybe (b :~: JSCommaList l)
forall a b. (a -> b) -> a -> b
$ (l :~: l)
-> ((l ~ l) => b :~: JSCommaList l) -> b :~: JSCommaList l
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith l :~: l
p (l ~ l) => b :~: JSCommaList l
forall k (a :: k). a :~: a
Refl
  dyncase (Cxt h g a b -> Maybe (JSCommaListF (Cxt h g a) b)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (JSLCons x :: Cxt h g a (JSCommaList l)
x _ _)) = Cxt h g a (JSCommaList l)
-> Maybe (JSCommaList l :~: JSCommaList l)
forall (f :: * -> *) a b. DynCase f a => f b -> Maybe (b :~: a)
dyncase Cxt h g a (JSCommaList l)
x
  dyncase _ = Maybe (b :~: JSCommaList l)
forall a. Maybe a
Nothing



instance (JSCommaTrailingListF :<: g, DynCase (Cxt h g a) (JSCommaList l)) => DynCase (Cxt h g a) (JSCommaTrailingList l) where
  dyncase :: Cxt h g a b -> Maybe (b :~: JSCommaTrailingList l)
dyncase (Cxt h g a b -> Maybe (JSCommaTrailingListF (Cxt h g a) b)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (JSCTLNone x :: Cxt h g a (JSCommaList l)
x)) = do (JSCommaList l :~: JSCommaList l
p :: _ :~: (JSCommaList l)) <- Cxt h g a (JSCommaList l)
-> Maybe (JSCommaList l :~: JSCommaList l)
forall (f :: * -> *) a b. DynCase f a => f b -> Maybe (b :~: a)
dyncase Cxt h g a (JSCommaList l)
x
                                               (b :~: JSCommaTrailingList l)
-> Maybe (b :~: JSCommaTrailingList l)
forall (m :: * -> *) a. Monad m => a -> m a
return ((b :~: JSCommaTrailingList l)
 -> Maybe (b :~: JSCommaTrailingList l))
-> (b :~: JSCommaTrailingList l)
-> Maybe (b :~: JSCommaTrailingList l)
forall a b. (a -> b) -> a -> b
$ (JSCommaList l :~: JSCommaList l)
-> ((JSCommaList l ~ JSCommaList l) => b :~: JSCommaTrailingList l)
-> b :~: JSCommaTrailingList l
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith JSCommaList l :~: JSCommaList l
p (JSCommaList l ~ JSCommaList l) => b :~: JSCommaTrailingList l
forall k (a :: k). a :~: a
Refl
  dyncase (Cxt h g a b -> Maybe (JSCommaTrailingListF (Cxt h g a) b)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (JSCTLComma x :: Cxt h g a (JSCommaList l)
x _)) = do (JSCommaList l :~: JSCommaList l
p :: _ :~: (JSCommaList l)) <- Cxt h g a (JSCommaList l)
-> Maybe (JSCommaList l :~: JSCommaList l)
forall (f :: * -> *) a b. DynCase f a => f b -> Maybe (b :~: a)
dyncase Cxt h g a (JSCommaList l)
x
                                                  (b :~: JSCommaTrailingList l)
-> Maybe (b :~: JSCommaTrailingList l)
forall (m :: * -> *) a. Monad m => a -> m a
return ((b :~: JSCommaTrailingList l)
 -> Maybe (b :~: JSCommaTrailingList l))
-> (b :~: JSCommaTrailingList l)
-> Maybe (b :~: JSCommaTrailingList l)
forall a b. (a -> b) -> a -> b
$ (JSCommaList l :~: JSCommaList l)
-> ((JSCommaList l ~ JSCommaList l) => b :~: JSCommaTrailingList l)
-> b :~: JSCommaTrailingList l
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith JSCommaList l :~: JSCommaList l
p (JSCommaList l ~ JSCommaList l) => b :~: JSCommaTrailingList l
forall k (a :: k). a :~: a
Refl
  dyncase _ = Maybe (b :~: JSCommaTrailingList l)
forall a. Maybe a
Nothing


riJSLCons :: (JSCommaListF :<: f) => Cxt h f a (JSCommaList l) -> Cxt h f a JSAnnotL -> Cxt h f a l -> Cxt h f a (JSCommaList l)
riJSLCons :: Cxt h f a (JSCommaList l)
-> Cxt h f a JSAnnotL -> Cxt h f a l -> Cxt h f a (JSCommaList l)
riJSLCons a :: Cxt h f a (JSCommaList l)
a b :: Cxt h f a JSAnnotL
b c :: Cxt h f a l
c = JSCommaListF (Cxt h f a) (JSCommaList l)
-> Cxt h f a (JSCommaList l)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (JSCommaListF (Cxt h f a) (JSCommaList l)
 -> Cxt h f a (JSCommaList l))
-> JSCommaListF (Cxt h f a) (JSCommaList l)
-> Cxt h f a (JSCommaList l)
forall a b. (a -> b) -> a -> b
$ Cxt h f a (JSCommaList l)
-> Cxt h f a JSAnnotL
-> Cxt h f a l
-> JSCommaListF (Cxt h f a) (JSCommaList l)
forall (e :: * -> *) l.
e (JSCommaList l)
-> e JSAnnotL -> e l -> JSCommaListF e (JSCommaList l)
JSLCons Cxt h f a (JSCommaList l)
a Cxt h f a JSAnnotL
b Cxt h f a l
c

riJSLOne :: (JSCommaListF :<: f) => Cxt h f a l -> Cxt h f a (JSCommaList l)
riJSLOne :: Cxt h f a l -> Cxt h f a (JSCommaList l)
riJSLOne = JSCommaListF (Cxt h f a) (JSCommaList l)
-> Cxt h f a (JSCommaList l)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (JSCommaListF (Cxt h f a) (JSCommaList l)
 -> Cxt h f a (JSCommaList l))
-> (Cxt h f a l -> JSCommaListF (Cxt h f a) (JSCommaList l))
-> Cxt h f a l
-> Cxt h f a (JSCommaList l)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cxt h f a l -> JSCommaListF (Cxt h f a) (JSCommaList l)
forall (e :: * -> *) l. e l -> JSCommaListF e (JSCommaList l)
JSLOne

riJSLNil :: (JSCommaListF :<: f) => Cxt h f a (JSCommaList l)
riJSLNil :: Cxt h f a (JSCommaList l)
riJSLNil = JSCommaListF (Cxt h f a) (JSCommaList l)
-> Cxt h f a (JSCommaList l)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject JSCommaListF (Cxt h f a) (JSCommaList l)
forall (e :: * -> *) t. JSCommaListF e (JSCommaList t)
JSLNil

riJSCTLComma :: (JSCommaTrailingListF :<: f) => Cxt h f a (JSCommaList l) -> Cxt h f a JSAnnotL -> Cxt h f a (JSCommaTrailingList l)
riJSCTLComma :: Cxt h f a (JSCommaList l)
-> Cxt h f a JSAnnotL -> Cxt h f a (JSCommaTrailingList l)
riJSCTLComma a :: Cxt h f a (JSCommaList l)
a b :: Cxt h f a JSAnnotL
b = JSCommaTrailingListF (Cxt h f a) (JSCommaTrailingList l)
-> Cxt h f a (JSCommaTrailingList l)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (JSCommaTrailingListF (Cxt h f a) (JSCommaTrailingList l)
 -> Cxt h f a (JSCommaTrailingList l))
-> JSCommaTrailingListF (Cxt h f a) (JSCommaTrailingList l)
-> Cxt h f a (JSCommaTrailingList l)
forall a b. (a -> b) -> a -> b
$ Cxt h f a (JSCommaList l)
-> Cxt h f a JSAnnotL
-> JSCommaTrailingListF (Cxt h f a) (JSCommaTrailingList l)
forall (e :: * -> *) l.
e (JSCommaList l)
-> e JSAnnotL -> JSCommaTrailingListF e (JSCommaTrailingList l)
JSCTLComma Cxt h f a (JSCommaList l)
a Cxt h f a JSAnnotL
b

riJSCTLNone :: (JSCommaTrailingListF :<: f) => Cxt h f a (JSCommaList l) -> Cxt h f a (JSCommaTrailingList l)
riJSCTLNone :: Cxt h f a (JSCommaList l) -> Cxt h f a (JSCommaTrailingList l)
riJSCTLNone = JSCommaTrailingListF (Cxt h f a) (JSCommaTrailingList l)
-> Cxt h f a (JSCommaTrailingList l)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (JSCommaTrailingListF (Cxt h f a) (JSCommaTrailingList l)
 -> Cxt h f a (JSCommaTrailingList l))
-> (Cxt h f a (JSCommaList l)
    -> JSCommaTrailingListF (Cxt h f a) (JSCommaTrailingList l))
-> Cxt h f a (JSCommaList l)
-> Cxt h f a (JSCommaTrailingList l)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cxt h f a (JSCommaList l)
-> JSCommaTrailingListF (Cxt h f a) (JSCommaTrailingList l)
forall (e :: * -> *) l.
e (JSCommaList l) -> JSCommaTrailingListF e (JSCommaTrailingList l)
JSCTLNone


-----------------------------------------------------------

do let specialSigNames = [''JSCommaListF, ''JSCommaTrailingListF]
   let jsSigNames = jsSigNamesBase ++ specialSigNames

   decs1 <- deriveAll newASTTypes
   decs2 <- derive [makeHFunctor, makeHTraversable, makeHFoldable, makeEqHF, makeShowHF,
                                makeOrdHF]
                   specialSigNames
   decs3 <- runCompTrans $ makeSumType "JSSig" jsSigNames

   return $ decs1 ++ decs2 ++ decs3

type JSTerm    = Term JSSig
type JSTermLab l = TermLab JSSig l

-- Phase restriction makes eliminating redundancy hard
jsSigNames :: [TH.Name]
jsSigNames :: [Name]
jsSigNames = [Name]
jsSigNamesBase [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [''JSCommaListF, ''JSCommaTrailingListF]

#endif