{-# OPTIONS_HADDOCK hide #-}

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

-- |

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 ( 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 as P

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


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

data ArrayDimVarDeclAttrs (e :: * -> *) l 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
                         ]
deriveAll [''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
  ImplicitReceiver   ::              JavaReceiver e P.ReceiverL
  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]

pattern JavaMethodDeclAttrs' ::
  ( JavaMethodDeclAttrs :-<: fs
  , All HFunctor fs
  ) => CxtS h fs a [J.ModifierL]
  -> CxtS h fs a [J.TypeParamL]
  -> CxtS h fs a (Maybe J.TypeL)
  -> CxtS h fs a [J.RefTypeL]
  -> CxtS h fs a JavaMethodDeclAttrsL
pattern $bJavaMethodDeclAttrs' :: CxtS h fs a [ModifierL]
-> CxtS h fs a [TypeParamL]
-> CxtS h fs a (Maybe TypeL)
-> CxtS h fs a [RefTypeL]
-> CxtS h fs a JavaMethodDeclAttrsL
$mJavaMethodDeclAttrs' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(JavaMethodDeclAttrs :-<: fs, All HFunctor fs) =>
CxtS h fs a JavaMethodDeclAttrsL
-> (CxtS h fs a [ModifierL]
    -> CxtS h fs a [TypeParamL]
    -> CxtS h fs a (Maybe TypeL)
    -> CxtS h fs a [RefTypeL]
    -> r)
-> (Void# -> r)
-> r
JavaMethodDeclAttrs' mods tparams retTp exns <- (project -> Just (JavaMethodDeclAttrs mods tparams retTp exns)) where
  JavaMethodDeclAttrs' mods :: CxtS h fs a [ModifierL]
mods tparams :: CxtS h fs a [TypeParamL]
tparams retTp :: CxtS h fs a (Maybe TypeL)
retTp exns :: CxtS h fs a [RefTypeL]
exns = CxtS h fs a [ModifierL]
-> CxtS h fs a [TypeParamL]
-> CxtS h fs a (Maybe TypeL)
-> CxtS h fs a [RefTypeL]
-> CxtS h fs a JavaMethodDeclAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(JavaMethodDeclAttrs :-<: fs, InjF fs JavaMethodDeclAttrsL j) =>
CxtS h fs a [ModifierL]
-> CxtS h fs a [TypeParamL]
-> CxtS h fs a (Maybe TypeL)
-> CxtS h fs a [RefTypeL]
-> CxtS h fs a j
iJavaMethodDeclAttrs CxtS h fs a [ModifierL]
mods CxtS h fs a [TypeParamL]
tparams CxtS h fs a (Maybe TypeL)
retTp CxtS h fs a [RefTypeL]
exns

pattern JavaParamAttrs' ::
  ( JavaParamAttrs :-<: fs
  , All HFunctor fs
  ) => CxtS h fs a [J.ModifierL]
  -> CxtS h fs a J.TypeL
  -> Int
  -> CxtS h fs a JavaParamAttrsL
pattern $bJavaParamAttrs' :: CxtS h fs a [ModifierL]
-> CxtS h fs a TypeL -> Int -> CxtS h fs a JavaParamAttrsL
$mJavaParamAttrs' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(JavaParamAttrs :-<: fs, All HFunctor fs) =>
CxtS h fs a JavaParamAttrsL
-> (CxtS h fs a [ModifierL] -> CxtS h fs a TypeL -> Int -> r)
-> (Void# -> r)
-> r
JavaParamAttrs' mods tp dim <- (project -> Just (JavaParamAttrs mods tp dim)) where
  JavaParamAttrs' mods :: CxtS h fs a [ModifierL]
mods tp :: CxtS h fs a TypeL
tp dim :: Int
dim = CxtS h fs a [ModifierL]
-> CxtS h fs a TypeL -> Int -> CxtS h fs a JavaParamAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(JavaParamAttrs :-<: fs, InjF fs JavaParamAttrsL j) =>
CxtS h fs a [ModifierL]
-> CxtS h fs a TypeL -> Int -> CxtS h fs a j
iJavaParamAttrs CxtS h fs a [ModifierL]
mods CxtS h fs a TypeL
tp Int
dim

pattern JavaVarargsParam' ::
  ( JavaVarargsParam :-<: fs
  , All HFunctor fs
  ) => CxtS h fs a JavaParamAttrsL
  -> CxtS h fs a P.IdentL
  -> CxtS h fs a JavaVarargsParamL
pattern $bJavaVarargsParam' :: CxtS h fs a JavaParamAttrsL
-> CxtS h fs a IdentL -> CxtS h fs a JavaVarargsParamL
$mJavaVarargsParam' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(JavaVarargsParam :-<: fs, All HFunctor fs) =>
CxtS h fs a JavaVarargsParamL
-> (CxtS h fs a JavaParamAttrsL -> CxtS h fs a IdentL -> r)
-> (Void# -> r)
-> r
JavaVarargsParam' attrs n <- (project -> Just (JavaVarargsParam attrs n)) where
  JavaVarargsParam' attrs :: CxtS h fs a JavaParamAttrsL
attrs n :: CxtS h fs a IdentL
n = CxtS h fs a JavaParamAttrsL
-> CxtS h fs a IdentL -> CxtS h fs a JavaVarargsParamL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(JavaVarargsParam :-<: fs, InjF fs JavaVarargsParamL j) =>
CxtS h fs a JavaParamAttrsL -> CxtS h fs a IdentL -> CxtS h fs a j
iJavaVarargsParam CxtS h fs a JavaParamAttrsL
attrs CxtS h fs a IdentL
n

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
                         ]
deriveAll [ ''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
                         ]
deriveAll [ ''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 :: 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 :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(ModifiersTypeIsMultiLocalVarDeclCommonAttrs :-<: fs,
 InjF fs MultiLocalVarDeclCommonAttrsL j) =>
CxtS h fs a ([ModifierL], TypeL) -> CxtS h fs a j
iModifiersTypeIsMultiLocalVarDeclCommonAttrs

  projF' :: 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 x :: 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' _ = Maybe (Cxt h (Sum MJavaSig :&: p) a ([ModifierL], TypeL))
forall a. Maybe a
Nothing

instance InjF MJavaSig AssignL BlockItemL where
  injF :: CxtS h MJavaSig a AssignL -> CxtS h MJavaSig a BlockItemL
injF = CxtS h MJavaSig a StmtL -> CxtS h MJavaSig a BlockItemL
forall h (fs :: [(* -> *) -> * -> *]) (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 :: [(* -> *) -> * -> *]) (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 :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(AssignIsExp :-<: fs, InjF fs ExpL j) =>
CxtS h fs a AssignL -> CxtS h fs a j
iAssignIsExp

  projF' :: Cxt h (Sum MJavaSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a AssignL)
projF' t :: 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 :: [(* -> *) -> * -> *]) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
projF' Cxt h (Sum MJavaSig :&: p) a BlockItemL
t
    BlockStmt s :: 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 e :: 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 :: [(* -> *) -> * -> *]) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
projF'  Cxt h (Sum MJavaSig :&: p) a ExpL
e


instance InjF MJavaSig MultiLocalVarDeclL BlockItemL where
  injF :: CxtS h MJavaSig a MultiLocalVarDeclL
-> CxtS h MJavaSig a BlockItemL
injF = CxtS h MJavaSig a MultiLocalVarDeclL
-> CxtS h MJavaSig a BlockItemL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(MultiLocalVarDeclIsBlockStmt :-<: fs, InjF fs BlockStmtL j) =>
CxtS h fs a MultiLocalVarDeclL -> CxtS h fs a j
iMultiLocalVarDeclIsBlockStmt
  projF' :: Cxt h (Sum MJavaSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a MultiLocalVarDeclL)
projF' t :: 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 :: [(* -> *) -> * -> *]) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
projF' Cxt h (Sum MJavaSig :&: p) a BlockItemL
t
    MJavaCxtA h a p BlockStmtL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a MultiLocalVarDeclL)
forall (fs :: [(* -> *) -> * -> *]) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
projF' MJavaCxtA h a p BlockStmtL
a

-- Generalizing to contexts takes more work
instance InjF MJavaSig P.IdentL P.LhsL where
  injF :: CxtS h MJavaSig a IdentL -> CxtS h MJavaSig a LhsL
injF n :: CxtS h MJavaSig a IdentL
n = CxtS h MJavaSig a NameL -> CxtS h MJavaSig a LhsL
forall h (fs :: [(* -> *) -> * -> *]) (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 :: [(* -> *) -> * -> *]) (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 (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 :: [(* -> *) -> * -> *]) (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' :: Cxt h (Sum MJavaSig :&: p) a LhsL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a IdentL)
projF' n :: Cxt h (Sum MJavaSig :&: p) a LhsL
n = do
    LhsIsLhs l :: 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 i :: 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 is :: 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' r :: 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 :: [(* -> *) -> * -> *]) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
projF' Cxt h (Sum MJavaSig :&: p) a IdentL
r

-- Generalizing to contexts takes more work
instance InjF MJavaSig P.IdentL ExpL where
  injF :: CxtS h MJavaSig a IdentL -> CxtS h MJavaSig a ExpL
injF x :: CxtS h MJavaSig a IdentL
x = CxtS h MJavaSig a NameL -> CxtS h MJavaSig a ExpL
forall h (fs :: [(* -> *) -> * -> *]) (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 :: [(* -> *) -> * -> *]) (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 (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 :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF CxtS h MJavaSig a IdentL
x]
  projF' :: Cxt h (Sum MJavaSig :&: p) a ExpL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a IdentL)
projF' e :: Cxt h (Sum MJavaSig :&: p) a ExpL
e = do
    ExpName n :: 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 is :: 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' i :: 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 :: [(* -> *) -> * -> *]) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
projF' Cxt h (Sum MJavaSig :&: p) a IdentL
i

instance InjF MJavaSig ExpL LocalVarInitL where
  injF :: CxtS h MJavaSig a ExpL -> CxtS h MJavaSig a LocalVarInitL
injF = CxtS h MJavaSig a ExpL -> CxtS h MJavaSig a LocalVarInitL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(VarInit :-<: fs, InjF fs VarInitL j) =>
CxtS h fs a ExpL -> CxtS h fs a j
iInitExp
  projF' :: Cxt h (Sum MJavaSig :&: p) a LocalVarInitL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a ExpL)
projF' i :: Cxt h (Sum MJavaSig :&: p) a LocalVarInitL
i = do
    VarInitIsLocalVarInit v :: 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 e :: 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 (m :: * -> *) a. Monad m => a -> m a
return Cxt h (Sum MJavaSig :&: p) a ExpL
e

instance InjF MJavaSig StmtL BlockItemL where
  injF :: CxtS h MJavaSig a StmtL -> CxtS h MJavaSig a BlockItemL
injF = CxtS h MJavaSig a StmtL -> CxtS h MJavaSig a BlockItemL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(BlockStmt :-<: fs, InjF fs BlockStmtL j) =>
CxtS h fs a StmtL -> CxtS h fs a j
iBlockStmt
  projF' :: Cxt h (Sum MJavaSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a StmtL)
projF' b :: Cxt h (Sum MJavaSig :&: p) a BlockItemL
b = do
    BlockStmtIsBlockItem c :: 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 s :: 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 (m :: * -> *) a. Monad m => a -> m a
return Cxt h (Sum MJavaSig :&: p) a StmtL
s

instance InjF MJavaSig P.BlockL StmtL where
  injF :: CxtS h MJavaSig a BlockL -> CxtS h MJavaSig a StmtL
injF = CxtS h MJavaSig a BlockL -> CxtS h MJavaSig a StmtL
forall h (fs :: [(* -> *) -> * -> *]) (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 :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(BlockIsBlock :-<: fs, InjF fs BlockL j) =>
CxtS h fs a BlockL -> CxtS h fs a j
iBlockIsBlock
  projF' :: Cxt h (Sum MJavaSig :&: p) a StmtL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a BlockL)
projF' b :: Cxt h (Sum MJavaSig :&: p) a StmtL
b = do
    StmtBlock s :: 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 b :: 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 (m :: * -> *) a. Monad m => a -> m a
return Cxt h (Sum MJavaSig :&: p) a BlockL
b

instance InjF MJavaSig ExpL P.FunctionArgumentL where
  injF :: CxtS h MJavaSig a ExpL -> CxtS h MJavaSig a FunctionArgumentL
injF = CxtS h MJavaSig a PositionalArgExpL
-> CxtS h MJavaSig a FunctionArgumentL
forall h (fs :: [(* -> *) -> * -> *]) (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 :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF
  projF' :: Cxt h (Sum MJavaSig :&: p) a FunctionArgumentL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a ExpL)
projF' a :: Cxt h (Sum MJavaSig :&: p) a FunctionArgumentL
a = do
    PositionalArgument p :: 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 :: [(* -> *) -> * -> *]) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
projF' Cxt h (Sum MJavaSig :&: p) a PositionalArgExpL
p

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

  projF' :: 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 n :: 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' _                                    = Maybe (Cxt h (Sum MJavaSig :&: p) a IdentL)
forall a. Maybe a
Nothing


instance InjF MJavaSig P.IdentL PositionalArgExpL where
  injF :: CxtS h MJavaSig a IdentL -> CxtS h MJavaSig a PositionalArgExpL
injF x :: CxtS h MJavaSig a IdentL
x = CxtS h MJavaSig a NameL -> CxtS h MJavaSig a PositionalArgExpL
forall h (fs :: [(* -> *) -> * -> *]) (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 :: [(* -> *) -> * -> *]) (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 (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 :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF CxtS h MJavaSig a IdentL
x]
  projF' :: Cxt h (Sum MJavaSig :&: p) a PositionalArgExpL
-> Maybe (Cxt h (Sum MJavaSig :&: p) a IdentL)
projF' a :: Cxt h (Sum MJavaSig :&: p) a PositionalArgExpL
a
   | Just (ExpIsPositionalArgExp e :: 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 n :: 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' i :: 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 :: [(* -> *) -> * -> *]) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
projF' Cxt h (Sum MJavaSig :&: p) a IdentL
i
  projF' _ = Maybe (Cxt h (Sum MJavaSig :&: p) a IdentL)
forall a. Maybe a
Nothing


#endif