{-# OPTIONS_HADDOCK hide #-}

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

-- |

module Cubix.Language.Java.Parametric.Common.Types where

#ifndef ONLY_ONE_LANGUAGE
import Data.List ( (\\) )

import Language.Haskell.TH.Syntax ( mkName )

import Data.Comp.Multi ( Node, Term, project', project, HFunctor, (:-<:), All, CxtS, AnnCxtS )
import Data.Comp.Trans ( makeSumType, runCompTrans )

import Cubix.Language.Info
import Cubix.Language.Java.Parametric.Full.Names
import Cubix.Language.Java.Parametric.Full.Types as J
import Cubix.Language.Parametric.Derive
import Cubix.Language.Parametric.InjF
import Cubix.Language.Parametric.Syntax hiding (ExpL)
import Cubix.Language.Parametric.Syntax qualified as P

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


-----------------------------------------------------------------------------------
---------------       Variable declarations and blocks     ------------------------
-----------------------------------------------------------------------------------

data ArrayDimVarDeclAttrs :: Node where
  ArrayDimVarDeclAttrs :: Int -> ArrayDimVarDeclAttrs e LocalVarDeclAttrsL


data ModifiersTypeIsMultiLocalVarDeclCommonAttrs e l where
  ModifiersTypeIsMultiLocalVarDeclCommonAttrs :: e ([ModifierL], TypeL) -> ModifiersTypeIsMultiLocalVarDeclCommonAttrs e MultiLocalVarDeclCommonAttrsL

deriveAll [''ArrayDimVarDeclAttrs, ''ModifiersTypeIsMultiLocalVarDeclCommonAttrs]

createSortInclusionTypes [ ''VarInitL,       ''MultiLocalVarDeclL, ''P.IdentL, ''P.BlockL, ''AssignL, ''ExpL, ''J.LhsL, ''BlockStmtL, ''J.AssignOpL
                         ] [
                           ''LocalVarInitL,  ''BlockStmtL,         ''J.IdentL, ''J.BlockL, ''ExpL,    ''RhsL, ''P.LhsL, ''BlockItemL, ''P.AssignOpL
                         ]
deriveAllButSortInjection [''VarInitIsLocalVarInit, ''MultiLocalVarDeclIsBlockStmt, ''IdentIsIdent, ''BlockIsBlock, ''AssignIsExp, ''ExpIsRhs,
           ''LhsIsLhs, ''BlockStmtIsBlockItem, ''AssignOpIsAssignOp]
createSortInclusionInfers [ ''VarInitL,       ''MultiLocalVarDeclL, ''P.IdentL, ''P.BlockL, ''AssignL, ''ExpL, ''J.LhsL, ''BlockStmtL, ''J.AssignOpL
                          ] [
                            ''LocalVarInitL,  ''BlockStmtL,         ''J.IdentL, ''J.BlockL, ''ExpL,    ''RhsL, ''P.LhsL, ''BlockItemL, ''P.AssignOpL
                          ]

-----------------------------------------------------------------------------------
---------------       Function calls, decls, defns         ------------------------
-----------------------------------------------------------------------------------

-- | NOTE: You can call a static method on an instance; then a primary receiver is substituting for
-- a type receiver
data JavaReceiver e l where
  PrimaryReceiver    :: e J.ExpL  -> JavaReceiver e P.ReceiverL
  SuperReceiver      ::              JavaReceiver e P.ReceiverL
  ClassSuperReceiver :: e J.NameL -> JavaReceiver e P.ReceiverL
  TypeReceiver       :: e J.NameL -> JavaReceiver e P.ReceiverL

data JavaTypeArgs e l where
  JavaTypeArgs :: e [J.RefTypeL] -> JavaTypeArgs e P.FunctionCallAttrsL

-- "void" is represented by Nothing
data JavaMethodDeclAttrsL
data JavaMethodDeclAttrs e l where
  JavaMethodDeclAttrs :: e [J.ModifierL] -> e [J.TypeParamL] -> e (Maybe J.TypeL) -> e [J.RefTypeL] -> JavaMethodDeclAttrs e JavaMethodDeclAttrsL

data JavaParamAttrsL
data JavaParamAttrs e l where
  JavaParamAttrs :: e [J.ModifierL] -> e J.TypeL -> Int -> JavaParamAttrs e JavaParamAttrsL

data JavaVarargsParamL
data JavaVarargsParam e l where
  JavaVarargsParam :: e JavaParamAttrsL -> e P.IdentL -> JavaVarargsParam e JavaVarargsParamL


deriveAll [''JavaReceiver, ''JavaTypeArgs, ''JavaMethodDeclAttrs, ''JavaParamAttrs, ''JavaVarargsParam]



createSortInclusionTypes [ ''P.FunctionCallL,     ''J.NameL,        ''J.ExpL,              ''P.FunctionDeclL, ''JavaMethodDeclAttrsL, ''JavaParamAttrsL,               ''JavaVarargsParamL
                         ] [
                           ''J.MethodInvocationL, ''P.FunctionExpL, ''P.PositionalArgExpL, ''J.MemberDeclL,   ''P.FunctionDeclAttrsL, ''P.FunctionParameterDeclAttrsL, ''FunctionParameterDeclL
                         ]
deriveAllButSortInjection [ ''FunctionCallIsMethodInvocation, ''NameIsFunctionExp, ''ExpIsPositionalArgExp, ''FunctionDeclIsMemberDecl
          , ''JavaMethodDeclAttrsIsFunctionDeclAttrs, ''JavaParamAttrsIsFunctionParameterDeclAttrs, ''JavaVarargsParamIsFunctionParameterDecl]
createSortInclusionInfers [ ''P.FunctionCallL,     ''J.NameL,        ''J.ExpL,              ''P.FunctionDeclL, ''JavaMethodDeclAttrsL, ''JavaParamAttrsL,               ''JavaVarargsParamL
                          ] [
                            ''J.MethodInvocationL, ''P.FunctionExpL, ''P.PositionalArgExpL, ''J.MemberDeclL,   ''P.FunctionDeclAttrsL, ''P.FunctionParameterDeclAttrsL, ''FunctionParameterDeclL
                          ]

createSortInclusionTypes [ ''P.FunctionDefL, ''JavaMethodDeclAttrsL, ''JavaParamAttrsL,   ''JavaVarargsParamL,    ''P.BlockL
                         ] [
                           ''J.MemberDeclL,  ''P.FunctionDefAttrsL,  ''P.ParameterAttrsL, ''P.FunctionParameterL, ''P.FunctionBodyL
                         ]
deriveAllButSortInjection [ ''FunctionDefIsMemberDecl, ''JavaMethodDeclAttrsIsFunctionDefAttrs, ''JavaParamAttrsIsParameterAttrs, ''JavaVarargsParamIsFunctionParameter, ''BlockIsFunctionBody]
createSortInclusionInfers [ ''P.FunctionDefL, ''JavaMethodDeclAttrsL, ''JavaParamAttrsL,   ''JavaVarargsParamL,    ''P.BlockL
                          ] [
                            ''J.MemberDeclL,  ''P.FunctionDefAttrsL,  ''P.ParameterAttrsL, ''P.FunctionParameterL, ''P.FunctionBodyL
                          ]

-----------------------------------------------------------------------------------
----------------------         Declaring the IPS           ------------------------
-----------------------------------------------------------------------------------


do let newJavaNodes       = [''ArrayDimVarDeclAttrs, ''JavaReceiver, ''JavaTypeArgs, ''JavaMethodDeclAttrs, ''JavaParamAttrs, ''JavaVarargsParam]
   let javaSortInjections = [''VarInitIsLocalVarInit, ''ModifiersTypeIsMultiLocalVarDeclCommonAttrs, ''IdentIsIdent, ''MultiLocalVarDeclIsBlockStmt,
                             ''BlockIsBlock, ''AssignIsExp, ''ExpIsRhs, ''LhsIsLhs, ''BlockStmtIsBlockItem, ''AssignOpIsAssignOp, ''IdentIsVarDeclBinder,
                             ''FunctionCallIsMethodInvocation, ''NameIsFunctionExp, ''ExpIsPositionalArgExp, ''FunctionDeclIsMemberDecl,
                             ''JavaMethodDeclAttrsIsFunctionDeclAttrs, ''JavaParamAttrsIsFunctionParameterDeclAttrs, ''JavaVarargsParamIsFunctionParameterDecl,
                             ''FunctionDefIsMemberDecl, ''JavaMethodDeclAttrsIsFunctionDefAttrs, ''JavaParamAttrsIsParameterAttrs, ''JavaVarargsParamIsFunctionParameter, ''BlockIsFunctionBody]
   let names = (javaSigNames \\ [mkName "Ident", mkName "Block", mkName "MethodInvocation", mkName "MethodBody"])
                             ++ javaSortInjections
                             ++ newJavaNodes
                             ++ [ ''OptLocalVarInit, ''SingleLocalVarDecl, ''MultiLocalVarDecl, ''P.Ident
                                , ''AssignOpEquals, ''Assign, ''P.Block, ''EmptyBlockEnd
                                , ''FunctionCall, ''FunctionIdent, ''FunctionArgumentList, ''ReceiverArg, ''PositionalArgument
                                , ''FunctionDecl, ''SelfParameterDecl, ''PositionalParameterDeclWithIdent
                                , ''FunctionDef, ''SelfParameter, ''PositionalParameter
                                ]
   sumDec <- runCompTrans $ makeSumType "MJavaSig" names
   return sumDec

type instance InjectableSorts MJavaSig MultiLocalVarDeclL = '[]

type MJavaTerm = Term MJavaSig
type MJavaTermLab = TermLab MJavaSig

type MJavaCxt h a = CxtS h MJavaSig a
type MJavaCxtA h a p = AnnCxtS p h MJavaSig a



-----------------------------------------------------------------------------------
----------------------         Sort injections             ------------------------
-----------------------------------------------------------------------------------

instance InjF MJavaSig ([ModifierL], TypeL) MultiLocalVarDeclCommonAttrsL where
  injF :: forall h (a :: * -> *).
CxtS h MJavaSig a ([ModifierL], TypeL)
-> CxtS h MJavaSig a MultiLocalVarDeclCommonAttrsL
injF = CxtS h MJavaSig a ([ModifierL], TypeL)
-> CxtS h MJavaSig a MultiLocalVarDeclCommonAttrsL
forall h (fs :: Signature) (a :: * -> *) j.
(ModifiersTypeIsMultiLocalVarDeclCommonAttrs :-<: fs,
 InjF fs MultiLocalVarDeclCommonAttrsL j) =>
CxtS h fs a ([ModifierL], TypeL) -> CxtS h fs a j
iModifiersTypeIsMultiLocalVarDeclCommonAttrs

  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a MultiLocalVarDeclCommonAttrsL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a ([ModifierL], TypeL))
projF' (Cxt h (Sum MJavaSig :&: p) a MultiLocalVarDeclCommonAttrsL
-> Maybe
     (ModifiersTypeIsMultiLocalVarDeclCommonAttrs
        (Cxt h (Sum MJavaSig :&: p) a) MultiLocalVarDeclCommonAttrsL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' -> Just (ModifiersTypeIsMultiLocalVarDeclCommonAttrs Cxt h (Sum MJavaSig :&: p) a ([ModifierL], TypeL)
x)) = Cxt h (Sum MJavaSig :&: p) a ([ModifierL], TypeL)
-> Maybe (Cxt h (Sum MJavaSig :&: p) a ([ModifierL], TypeL))
forall a. a -> Maybe a
Just Cxt h (Sum MJavaSig :&: p) a ([ModifierL], TypeL)
x
  projF' Cxt h (Sum MJavaSig :&: p) a MultiLocalVarDeclCommonAttrsL
_ = Maybe (Cxt h (Sum MJavaSig :&: p) a ([ModifierL], TypeL))
forall a. Maybe a
Nothing

instance InjF MJavaSig AssignL BlockItemL where
  injF :: forall h (a :: * -> *).
CxtS h MJavaSig a AssignL -> CxtS h MJavaSig a BlockItemL
injF = CxtS h MJavaSig a StmtL -> CxtS h MJavaSig a BlockItemL
forall h (fs :: Signature) (a :: * -> *) j.
(BlockStmt :-<: fs, InjF fs BlockStmtL j) =>
CxtS h fs a StmtL -> CxtS h fs a j
iBlockStmt (CxtS h MJavaSig a StmtL -> CxtS h MJavaSig a BlockItemL)
-> (CxtS h MJavaSig a AssignL -> CxtS h MJavaSig a StmtL)
-> CxtS h MJavaSig a AssignL
-> CxtS h MJavaSig a BlockItemL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtS h MJavaSig a ExpL -> CxtS h MJavaSig a StmtL
forall h (fs :: Signature) (a :: * -> *) j.
(Stmt :-<: fs, InjF fs StmtL j) =>
CxtS h fs a ExpL -> CxtS h fs a j
iExpStmt (CxtS h MJavaSig a ExpL -> CxtS h MJavaSig a StmtL)
-> (CxtS h MJavaSig a AssignL -> CxtS h MJavaSig a ExpL)
-> CxtS h MJavaSig a AssignL
-> CxtS h MJavaSig a StmtL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtS h MJavaSig a AssignL -> CxtS h MJavaSig a ExpL
forall h (fs :: Signature) (a :: * -> *) j.
(AssignIsExp :-<: fs, InjF fs ExpL j) =>
CxtS h fs a AssignL -> CxtS h fs a j
iAssignIsExp

  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a AssignL)
projF' Cxt h (Sum MJavaSig :&: p) a BlockItemL
t = do
    (MJavaCxtA h a p BlockStmtL
a :: MJavaCxtA _ _ _ BlockStmtL) <- Cxt h (Sum MJavaSig :&: p) a BlockItemL
-> Maybe (MJavaCxtA h a p BlockStmtL)
forall (fs :: Signature) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a BlockStmtL)
projF' Cxt h (Sum MJavaSig :&: p) a BlockItemL
t
    BlockStmt Cxt h (Sum MJavaSig :&: p) a StmtL
s <- MJavaCxtA h a p BlockStmtL
-> Maybe (BlockStmt (Cxt h (Sum MJavaSig :&: p) a) BlockStmtL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' MJavaCxtA h a p BlockStmtL
a
    ExpStmt Cxt h (Sum MJavaSig :&: p) a ExpL
e <- Cxt h (Sum MJavaSig :&: p) a StmtL
-> Maybe (Stmt (Cxt h (Sum MJavaSig :&: p) a) StmtL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MJavaSig :&: p) a StmtL
s
    Cxt h (Sum MJavaSig :&: p) a ExpL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a AssignL)
forall (fs :: Signature) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a ExpL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a AssignL)
projF'  Cxt h (Sum MJavaSig :&: p) a ExpL
e


instance InjF MJavaSig MultiLocalVarDeclL BlockItemL where
  injF :: forall h (a :: * -> *).
CxtS h MJavaSig a MultiLocalVarDeclL
-> CxtS h MJavaSig a BlockItemL
injF = CxtS h MJavaSig a MultiLocalVarDeclL
-> CxtS h MJavaSig a BlockItemL
forall h (fs :: Signature) (a :: * -> *) j.
(MultiLocalVarDeclIsBlockStmt :-<: fs, InjF fs BlockStmtL j) =>
CxtS h fs a MultiLocalVarDeclL -> CxtS h fs a j
iMultiLocalVarDeclIsBlockStmt
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a MultiLocalVarDeclL)
projF' Cxt h (Sum MJavaSig :&: p) a BlockItemL
t = do
    (MJavaCxtA h a p BlockStmtL
a :: MJavaCxtA _ _ _ BlockStmtL) <- Cxt h (Sum MJavaSig :&: p) a BlockItemL
-> Maybe (MJavaCxtA h a p BlockStmtL)
forall (fs :: Signature) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a BlockStmtL)
projF' Cxt h (Sum MJavaSig :&: p) a BlockItemL
t
    MJavaCxtA h a p BlockStmtL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a MultiLocalVarDeclL)
forall (fs :: Signature) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a BlockStmtL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a MultiLocalVarDeclL)
projF' MJavaCxtA h a p BlockStmtL
a

-- Generalizing to contexts takes more work
instance InjF MJavaSig P.IdentL P.LhsL where
  injF :: forall h (a :: * -> *).
CxtS h MJavaSig a IdentL -> CxtS h MJavaSig a LhsL
injF CxtS h MJavaSig a IdentL
n = CxtS h MJavaSig a NameL -> CxtS h MJavaSig a LhsL
forall h (fs :: Signature) (a :: * -> *) j.
(Lhs :-<: fs, InjF fs LhsL j) =>
CxtS h fs a NameL -> CxtS h fs a j
iNameLhs (CxtS h MJavaSig a NameL -> CxtS h MJavaSig a LhsL)
-> CxtS h MJavaSig a NameL -> CxtS h MJavaSig a LhsL
forall a b. (a -> b) -> a -> b
$ CxtS h MJavaSig a [IdentL] -> CxtS h MJavaSig a NameL
forall h (fs :: Signature) (a :: * -> *) j.
(Name :-<: fs, InjF fs NameL j) =>
CxtS h fs a [IdentL] -> CxtS h fs a j
iName (CxtS h MJavaSig a [IdentL] -> CxtS h MJavaSig a NameL)
-> CxtS h MJavaSig a [IdentL] -> CxtS h MJavaSig a NameL
forall a b. (a -> b) -> a -> b
$ [Cxt h (Sum MJavaSig) a IdentL] -> CxtS h MJavaSig a [IdentL]
forall l.
Typeable l =>
[Cxt h (Sum MJavaSig) a l] -> Cxt h (Sum MJavaSig) a [l]
forall (f :: * -> *) (e :: * -> *) l.
(InsertF f e, Typeable l) =>
f (e l) -> e (f l)
insertF [CxtS h MJavaSig a IdentL -> Cxt h (Sum MJavaSig) a IdentL
forall h (fs :: Signature) (a :: * -> *) j.
(IdentIsIdent :-<: fs, InjF fs IdentL j) =>
CxtS h fs a IdentL -> CxtS h fs a j
iIdentIsIdent CxtS h MJavaSig a IdentL
n]
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a LhsL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a IdentL)
projF' Cxt h (Sum MJavaSig :&: p) a LhsL
n = do
    LhsIsLhs Cxt h (Sum MJavaSig :&: p) a LhsL
l <- Cxt h (Sum MJavaSig :&: p) a LhsL
-> Maybe (LhsIsLhs (Cxt h (Sum MJavaSig :&: p) a) LhsL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MJavaSig :&: p) a LhsL
n
    NameLhs Cxt h (Sum MJavaSig :&: p) a NameL
i <- Cxt h (Sum MJavaSig :&: p) a LhsL
-> Maybe (Lhs (Cxt h (Sum MJavaSig :&: p) a) LhsL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MJavaSig :&: p) a LhsL
l
    Name Cxt h (Sum MJavaSig :&: p) a [IdentL]
is <- Cxt h (Sum MJavaSig :&: p) a NameL
-> Maybe (Name (Cxt h (Sum MJavaSig :&: p) a) NameL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MJavaSig :&: p) a NameL
i
    let (SingletonFA' Cxt h (Sum MJavaSig :&: p) a IdentL
r) = Cxt h (Sum MJavaSig :&: p) a [IdentL]
is
    Cxt h (Sum MJavaSig :&: p) a IdentL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a IdentL)
forall (fs :: Signature) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a IdentL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a IdentL)
projF' Cxt h (Sum MJavaSig :&: p) a IdentL
r

-- Generalizing to contexts takes more work
instance InjF MJavaSig P.IdentL ExpL where
  injF :: forall h (a :: * -> *).
CxtS h MJavaSig a IdentL -> CxtS h MJavaSig a ExpL
injF CxtS h MJavaSig a IdentL
x = CxtS h MJavaSig a NameL -> CxtS h MJavaSig a ExpL
forall h (fs :: Signature) (a :: * -> *) j.
(Exp :-<: fs, InjF fs ExpL j) =>
CxtS h fs a NameL -> CxtS h fs a j
iExpName (CxtS h MJavaSig a NameL -> CxtS h MJavaSig a ExpL)
-> CxtS h MJavaSig a NameL -> CxtS h MJavaSig a ExpL
forall a b. (a -> b) -> a -> b
$ CxtS h MJavaSig a [IdentL] -> CxtS h MJavaSig a NameL
forall h (fs :: Signature) (a :: * -> *) j.
(Name :-<: fs, InjF fs NameL j) =>
CxtS h fs a [IdentL] -> CxtS h fs a j
iName (CxtS h MJavaSig a [IdentL] -> CxtS h MJavaSig a NameL)
-> CxtS h MJavaSig a [IdentL] -> CxtS h MJavaSig a NameL
forall a b. (a -> b) -> a -> b
$ [Cxt h (Sum MJavaSig) a IdentL] -> CxtS h MJavaSig a [IdentL]
forall l.
Typeable l =>
[Cxt h (Sum MJavaSig) a l] -> Cxt h (Sum MJavaSig) a [l]
forall (f :: * -> *) (e :: * -> *) l.
(InsertF f e, Typeable l) =>
f (e l) -> e (f l)
insertF [CxtS h MJavaSig a IdentL -> Cxt h (Sum MJavaSig) a IdentL
forall (fs :: Signature) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a IdentL -> CxtS h MJavaSig a IdentL
injF CxtS h MJavaSig a IdentL
x]
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a ExpL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a IdentL)
projF' Cxt h (Sum MJavaSig :&: p) a ExpL
e = do
    ExpName Cxt h (Sum MJavaSig :&: p) a NameL
n <- Cxt h (Sum MJavaSig :&: p) a ExpL
-> Maybe (Exp (Cxt h (Sum MJavaSig :&: p) a) ExpL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MJavaSig :&: p) a ExpL
e
    Name Cxt h (Sum MJavaSig :&: p) a [IdentL]
is <- Cxt h (Sum MJavaSig :&: p) a NameL
-> Maybe (Name (Cxt h (Sum MJavaSig :&: p) a) NameL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MJavaSig :&: p) a NameL
n
    let (SingletonFA' Cxt h (Sum MJavaSig :&: p) a IdentL
i) = Cxt h (Sum MJavaSig :&: p) a [IdentL]
is
    Cxt h (Sum MJavaSig :&: p) a IdentL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a IdentL)
forall (fs :: Signature) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a IdentL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a IdentL)
projF' Cxt h (Sum MJavaSig :&: p) a IdentL
i

instance InjF MJavaSig ExpL LocalVarInitL where
  injF :: forall h (a :: * -> *).
CxtS h MJavaSig a ExpL -> CxtS h MJavaSig a LocalVarInitL
injF = CxtS h MJavaSig a ExpL -> CxtS h MJavaSig a LocalVarInitL
forall h (fs :: Signature) (a :: * -> *) j.
(VarInit :-<: fs, InjF fs VarInitL j) =>
CxtS h fs a ExpL -> CxtS h fs a j
iInitExp
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a LocalVarInitL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a ExpL)
projF' Cxt h (Sum MJavaSig :&: p) a LocalVarInitL
i = do
    VarInitIsLocalVarInit Cxt h (Sum MJavaSig :&: p) a VarInitL
v <- Cxt h (Sum MJavaSig :&: p) a LocalVarInitL
-> Maybe
     (VarInitIsLocalVarInit
        (Cxt h (Sum MJavaSig :&: p) a) LocalVarInitL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MJavaSig :&: p) a LocalVarInitL
i
    InitExp Cxt h (Sum MJavaSig :&: p) a ExpL
e <- Cxt h (Sum MJavaSig :&: p) a VarInitL
-> Maybe (VarInit (Cxt h (Sum MJavaSig :&: p) a) VarInitL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MJavaSig :&: p) a VarInitL
v
    Cxt h (Sum MJavaSig :&: p) a ExpL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a ExpL)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Cxt h (Sum MJavaSig :&: p) a ExpL
e

instance InjF MJavaSig StmtL BlockItemL where
  injF :: forall h (a :: * -> *).
CxtS h MJavaSig a StmtL -> CxtS h MJavaSig a BlockItemL
injF = CxtS h MJavaSig a StmtL -> CxtS h MJavaSig a BlockItemL
forall h (fs :: Signature) (a :: * -> *) j.
(BlockStmt :-<: fs, InjF fs BlockStmtL j) =>
CxtS h fs a StmtL -> CxtS h fs a j
iBlockStmt
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a StmtL)
projF' Cxt h (Sum MJavaSig :&: p) a BlockItemL
b = do
    BlockStmtIsBlockItem Cxt h (Sum MJavaSig :&: p) a BlockStmtL
c <- Cxt h (Sum MJavaSig :&: p) a BlockItemL
-> Maybe
     (BlockStmtIsBlockItem (Cxt h (Sum MJavaSig :&: p) a) BlockItemL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MJavaSig :&: p) a BlockItemL
b
    BlockStmt Cxt h (Sum MJavaSig :&: p) a StmtL
s <- Cxt h (Sum MJavaSig :&: p) a BlockStmtL
-> Maybe (BlockStmt (Cxt h (Sum MJavaSig :&: p) a) BlockStmtL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MJavaSig :&: p) a BlockStmtL
c
    Cxt h (Sum MJavaSig :&: p) a StmtL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a StmtL)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Cxt h (Sum MJavaSig :&: p) a StmtL
s

instance InjF MJavaSig P.BlockL StmtL where
  injF :: forall h (a :: * -> *).
CxtS h MJavaSig a BlockL -> CxtS h MJavaSig a StmtL
injF = CxtS h MJavaSig a BlockL -> CxtS h MJavaSig a StmtL
forall h (fs :: Signature) (a :: * -> *) j.
(Stmt :-<: fs, InjF fs StmtL j) =>
CxtS h fs a BlockL -> CxtS h fs a j
iStmtBlock (CxtS h MJavaSig a BlockL -> CxtS h MJavaSig a StmtL)
-> (CxtS h MJavaSig a BlockL -> CxtS h MJavaSig a BlockL)
-> CxtS h MJavaSig a BlockL
-> CxtS h MJavaSig a StmtL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtS h MJavaSig a BlockL -> CxtS h MJavaSig a BlockL
forall h (fs :: Signature) (a :: * -> *) j.
(BlockIsBlock :-<: fs, InjF fs BlockL j) =>
CxtS h fs a BlockL -> CxtS h fs a j
iBlockIsBlock
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a StmtL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a BlockL)
projF' Cxt h (Sum MJavaSig :&: p) a StmtL
b = do
    StmtBlock Cxt h (Sum MJavaSig :&: p) a BlockL
s <- Cxt h (Sum MJavaSig :&: p) a StmtL
-> Maybe (Stmt (Cxt h (Sum MJavaSig :&: p) a) StmtL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MJavaSig :&: p) a StmtL
b
    BlockIsBlock Cxt h (Sum MJavaSig :&: p) a BlockL
b <- Cxt h (Sum MJavaSig :&: p) a BlockL
-> Maybe (BlockIsBlock (Cxt h (Sum MJavaSig :&: p) a) BlockL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MJavaSig :&: p) a BlockL
s
    Cxt h (Sum MJavaSig :&: p) a BlockL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a BlockL)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Cxt h (Sum MJavaSig :&: p) a BlockL
b

instance InjF MJavaSig ExpL P.FunctionArgumentL where
  injF :: forall h (a :: * -> *).
CxtS h MJavaSig a ExpL -> CxtS h MJavaSig a FunctionArgumentL
injF = CxtS h MJavaSig a PositionalArgExpL
-> CxtS h MJavaSig a FunctionArgumentL
forall h (fs :: Signature) (a :: * -> *) j.
(PositionalArgument :-<: fs, InjF fs FunctionArgumentL j) =>
CxtS h fs a PositionalArgExpL -> CxtS h fs a j
iPositionalArgument (CxtS h MJavaSig a PositionalArgExpL
 -> CxtS h MJavaSig a FunctionArgumentL)
-> (CxtS h MJavaSig a ExpL -> CxtS h MJavaSig a PositionalArgExpL)
-> CxtS h MJavaSig a ExpL
-> CxtS h MJavaSig a FunctionArgumentL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtS h MJavaSig a ExpL -> CxtS h MJavaSig a PositionalArgExpL
forall (fs :: Signature) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a ExpL -> CxtS h MJavaSig a PositionalArgExpL
injF
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a FunctionArgumentL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a ExpL)
projF' Cxt h (Sum MJavaSig :&: p) a FunctionArgumentL
a = do
    PositionalArgument Cxt h (Sum MJavaSig :&: p) a PositionalArgExpL
p <- Cxt h (Sum MJavaSig :&: p) a FunctionArgumentL
-> Maybe
     (PositionalArgument
        (Cxt h (Sum MJavaSig :&: p) a) FunctionArgumentL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MJavaSig :&: p) a FunctionArgumentL
a
    Cxt h (Sum MJavaSig :&: p) a PositionalArgExpL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a ExpL)
forall (fs :: Signature) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a PositionalArgExpL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a ExpL)
projF' Cxt h (Sum MJavaSig :&: p) a PositionalArgExpL
p

instance InjF MJavaSig P.IdentL FunctionExpL where
  injF :: forall h (a :: * -> *).
CxtS h MJavaSig a IdentL -> CxtS h MJavaSig a FunctionExpL
injF = CxtS h MJavaSig a IdentL -> CxtS h MJavaSig a FunctionExpL
forall h (fs :: Signature) (a :: * -> *) j.
(FunctionIdent :-<: fs, InjF fs FunctionExpL j) =>
CxtS h fs a IdentL -> CxtS h fs a j
iFunctionIdent

  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a FunctionExpL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a IdentL)
projF' (Cxt h (Sum MJavaSig :&: p) a FunctionExpL
-> Maybe
     (FunctionIdent (Cxt h (Sum MJavaSig :&: p) a) FunctionExpL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' -> Just (FunctionIdent Cxt h (Sum MJavaSig :&: p) a IdentL
n)) = Cxt h (Sum MJavaSig :&: p) a IdentL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a IdentL)
forall a. a -> Maybe a
Just Cxt h (Sum MJavaSig :&: p) a IdentL
n
  projF' Cxt h (Sum MJavaSig :&: p) a FunctionExpL
_                                    = Maybe (Cxt h (Sum MJavaSig :&: p) a IdentL)
forall a. Maybe a
Nothing


instance InjF MJavaSig P.IdentL PositionalArgExpL where
  injF :: forall h (a :: * -> *).
CxtS h MJavaSig a IdentL -> CxtS h MJavaSig a PositionalArgExpL
injF CxtS h MJavaSig a IdentL
x = CxtS h MJavaSig a NameL -> CxtS h MJavaSig a PositionalArgExpL
forall h (fs :: Signature) (a :: * -> *) j.
(Exp :-<: fs, InjF fs ExpL j) =>
CxtS h fs a NameL -> CxtS h fs a j
iExpName (CxtS h MJavaSig a NameL -> CxtS h MJavaSig a PositionalArgExpL)
-> CxtS h MJavaSig a NameL -> CxtS h MJavaSig a PositionalArgExpL
forall a b. (a -> b) -> a -> b
$ CxtS h MJavaSig a [IdentL] -> CxtS h MJavaSig a NameL
forall h (fs :: Signature) (a :: * -> *) j.
(Name :-<: fs, InjF fs NameL j) =>
CxtS h fs a [IdentL] -> CxtS h fs a j
iName (CxtS h MJavaSig a [IdentL] -> CxtS h MJavaSig a NameL)
-> CxtS h MJavaSig a [IdentL] -> CxtS h MJavaSig a NameL
forall a b. (a -> b) -> a -> b
$ [Cxt h (Sum MJavaSig) a IdentL] -> CxtS h MJavaSig a [IdentL]
forall l.
Typeable l =>
[Cxt h (Sum MJavaSig) a l] -> Cxt h (Sum MJavaSig) a [l]
forall (f :: * -> *) (e :: * -> *) l.
(InsertF f e, Typeable l) =>
f (e l) -> e (f l)
insertF [CxtS h MJavaSig a IdentL -> Cxt h (Sum MJavaSig) a IdentL
forall (fs :: Signature) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a IdentL -> CxtS h MJavaSig a IdentL
injF CxtS h MJavaSig a IdentL
x]
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a PositionalArgExpL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a IdentL)
projF' Cxt h (Sum MJavaSig :&: p) a PositionalArgExpL
a
   | Just (ExpIsPositionalArgExp Cxt h (Sum MJavaSig :&: p) a ExpL
e) <- Cxt h (Sum MJavaSig :&: p) a PositionalArgExpL
-> Maybe
     (ExpIsPositionalArgExp
        (Cxt h (Sum MJavaSig :&: p) a) PositionalArgExpL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MJavaSig :&: p) a PositionalArgExpL
a
   , Just (ExpName Cxt h (Sum MJavaSig :&: p) a NameL
n) <- Cxt h (Sum MJavaSig :&: p) a ExpL
-> Maybe (Exp (Cxt h (Sum MJavaSig :&: p) a) ExpL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MJavaSig :&: p) a ExpL
e
   , Just (Name (SingletonFA' Cxt h (Sum MJavaSig :&: p) a IdentL
i)) <- Cxt h (Sum MJavaSig :&: p) a NameL
-> Maybe (Name (Cxt h (Sum MJavaSig :&: p) a) NameL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MJavaSig :&: p) a NameL
n = Cxt h (Sum MJavaSig :&: p) a IdentL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a IdentL)
forall (fs :: Signature) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a IdentL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a IdentL)
projF' Cxt h (Sum MJavaSig :&: p) a IdentL
i
  projF' Cxt h (Sum MJavaSig :&: p) a PositionalArgExpL
_ = Maybe (Cxt h (Sum MJavaSig :&: p) a IdentL)
forall a. Maybe a
Nothing

instance InjF MJavaSig FunctionCallL RhsL where
  injF :: forall h (a :: * -> *).
CxtS h MJavaSig a FunctionCallL -> CxtS h MJavaSig a RhsL
injF = CxtS h MJavaSig a MethodInvocationL -> CxtS h MJavaSig a RhsL
forall h (fs :: Signature) (a :: * -> *) j.
(Exp :-<: fs, InjF fs ExpL j) =>
CxtS h fs a MethodInvocationL -> CxtS h fs a j
iMethodInv (CxtS h MJavaSig a MethodInvocationL -> CxtS h MJavaSig a RhsL)
-> (CxtS h MJavaSig a FunctionCallL
    -> CxtS h MJavaSig a MethodInvocationL)
-> CxtS h MJavaSig a FunctionCallL
-> CxtS h MJavaSig a RhsL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtS h MJavaSig a FunctionCallL
-> CxtS h MJavaSig a MethodInvocationL
forall (fs :: Signature) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a FunctionCallL
-> CxtS h MJavaSig a MethodInvocationL
injF
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MJavaSig :&: p) a RhsL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a FunctionCallL)
projF' Cxt h (Sum MJavaSig :&: p) a RhsL
f
   | Just (ExpIsRhs Cxt h (Sum MJavaSig :&: p) a ExpL
e) <- Cxt h (Sum MJavaSig :&: p) a RhsL
-> Maybe (ExpIsRhs (Cxt h (Sum MJavaSig :&: p) a) RhsL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MJavaSig :&: p) a RhsL
f
   , Just (MethodInv Cxt h (Sum MJavaSig :&: p) a MethodInvocationL
c) <- Cxt h (Sum MJavaSig :&: p) a ExpL
-> Maybe (Exp (Cxt h (Sum MJavaSig :&: p) a) ExpL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MJavaSig :&: p) a ExpL
e
   , Just (FunctionCallIsMethodInvocation Cxt h (Sum MJavaSig :&: p) a FunctionCallL
b) <- Cxt h (Sum MJavaSig :&: p) a MethodInvocationL
-> Maybe
     (FunctionCallIsMethodInvocation
        (Cxt h (Sum MJavaSig :&: p) a) MethodInvocationL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MJavaSig :&: p) a MethodInvocationL
c
   = Cxt h (Sum MJavaSig :&: p) a FunctionCallL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a FunctionCallL)
forall a. a -> Maybe a
Just Cxt h (Sum MJavaSig :&: p) a FunctionCallL
b
  projF' Cxt h (Sum MJavaSig :&: p) a RhsL
_ = Maybe (Cxt h (Sum MJavaSig :&: p) a FunctionCallL)
forall a. Maybe a
Nothing


#endif