{-# 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
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