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

{-# LANGUAGE CPP                   #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE UndecidableInstances  #-}

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, makeConstrNameHF, 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 :: forall b. Cxt h g a b -> Maybe (b :~: JSCommaList l)
dyncase (Cxt h g a b -> Maybe (JSCommaListF (Cxt h g a) b)
NatM Maybe (Cxt h g a) (JSCommaListF (Cxt h g a))
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just JSCommaListF (Cxt h g a) b
JSLNil) = Maybe (b :~: JSCommaList l)
forall a. Maybe a
Nothing
  dyncase (Cxt h g a b -> Maybe (JSCommaListF (Cxt h g a) b)
NatM Maybe (Cxt h g a) (JSCommaListF (Cxt h g a))
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (JSLOne Cxt h g a l
x)) = do (l :~: l
p :: _ :~: l) <- Cxt h g a l -> Maybe (l :~: l)
forall b. Cxt h g a b -> Maybe (b :~: l)
forall (f :: * -> *) a b. DynCase f a => f b -> Maybe (b :~: a)
dyncase Cxt h g a l
x
                                            return $ (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 b :~: b
b :~: JSCommaList l
(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)
NatM Maybe (Cxt h g a) (JSCommaListF (Cxt h g a))
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (JSLCons Cxt h g a (JSCommaList l)
x Cxt h g a JSAnnotL
_ Cxt h g a l
_)) = Cxt h g a b -> Maybe (b :~: JSCommaList l)
forall b. Cxt h g a b -> Maybe (b :~: JSCommaList l)
forall (f :: * -> *) a b. DynCase f a => f b -> Maybe (b :~: a)
dyncase Cxt h g a b
Cxt h g a (JSCommaList l)
x
  dyncase Cxt h g a b
_ = 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 :: forall b. Cxt h g a b -> Maybe (b :~: JSCommaTrailingList l)
dyncase (Cxt h g a b -> Maybe (JSCommaTrailingListF (Cxt h g a) b)
NatM Maybe (Cxt h g a) (JSCommaTrailingListF (Cxt h g a))
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (JSCTLNone 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 b. Cxt h g a b -> Maybe (b :~: JSCommaList l)
forall (f :: * -> *) a b. DynCase f a => f b -> Maybe (b :~: a)
dyncase Cxt h g a (JSCommaList l)
x
                                               return $ (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 b :~: b
b :~: JSCommaTrailingList l
(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)
NatM Maybe (Cxt h g a) (JSCommaTrailingListF (Cxt h g a))
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (JSCTLComma Cxt h g a (JSCommaList l)
x Cxt h g a JSAnnotL
_)) = do (JSCommaList l :~: JSCommaList l
p :: _ :~: (JSCommaList l)) <- Cxt h g a (JSCommaList l)
-> Maybe (JSCommaList l :~: JSCommaList l)
forall b. Cxt h g a b -> Maybe (b :~: JSCommaList l)
forall (f :: * -> *) a b. DynCase f a => f b -> Maybe (b :~: a)
dyncase Cxt h g a (JSCommaList l)
x
                                                  return $ (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 b :~: b
b :~: JSCommaTrailingList l
(JSCommaList l ~ JSCommaList l) => b :~: JSCommaTrailingList l
forall {k} (a :: k). a :~: a
Refl
  dyncase Cxt h g a b
_ = 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 :: forall (f :: Fragment) h (a :: * -> *) l.
(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)
a Cxt h f a JSAnnotL
b Cxt h f a l
c = JSCommaListF (Cxt h f a) (JSCommaList l)
-> Cxt h f a (JSCommaList l)
JSCommaListF (Cxt h f a) :-> Cxt h f a
forall (g :: Fragment) (f :: Fragment) 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 :: forall (f :: Fragment) h (a :: * -> *) l.
(JSCommaListF :<: f) =>
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)
JSCommaListF (Cxt h f a) :-> Cxt h f a
forall (g :: Fragment) (f :: Fragment) 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 :: forall (f :: Fragment) h (a :: * -> *) l.
(JSCommaListF :<: f) =>
Cxt h f a (JSCommaList l)
riJSLNil = JSCommaListF (Cxt h f a) (JSCommaList l)
-> Cxt h f a (JSCommaList l)
JSCommaListF (Cxt h f a) :-> Cxt h f a
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject JSCommaListF (Cxt h f a) (JSCommaList l)
forall (e :: * -> *) l. JSCommaListF e (JSCommaList l)
JSLNil

riJSCTLComma :: (JSCommaTrailingListF :<: f) => Cxt h f a (JSCommaList l) -> Cxt h f a JSAnnotL -> Cxt h f a (JSCommaTrailingList l)
riJSCTLComma :: forall (f :: Fragment) h (a :: * -> *) l.
(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)
a Cxt h f a JSAnnotL
b = JSCommaTrailingListF (Cxt h f a) (JSCommaTrailingList l)
-> Cxt h f a (JSCommaTrailingList l)
JSCommaTrailingListF (Cxt h f a) :-> Cxt h f a
forall (g :: Fragment) (f :: Fragment) 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 :: forall (f :: Fragment) h (a :: * -> *) l.
(JSCommaTrailingListF :<: f) =>
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)
JSCommaTrailingListF (Cxt h f a) :-> Cxt h f a
forall (g :: Fragment) (f :: Fragment) 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, makeConstrNameHF]
                   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