{-# OPTIONS_HADDOCK hide #-}
{-# OPTIONS_GHC -freduction-depth=200 #-}
{-# LANGUAGE CPP                      #-}
{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE GADTs                    #-}
{-# LANGUAGE KindSignatures           #-}
{-# LANGUAGE MultiParamTypeClasses    #-}
{-# LANGUAGE PartialTypeSignatures    #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE TemplateHaskell          #-}
{-# LANGUAGE TypeApplications         #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE UndecidableInstances     #-}
{-# LANGUAGE ViewPatterns             #-}

#ifdef ONLY_ONE_LANGUAGE
module Cubix.Language.Java.Parametric.Common.Trans () where
#else
module Cubix.Language.Java.Parametric.Common.Trans (
    translate
  , untranslate
  ) where

import Data.List( (\\) )
import Data.Maybe ( fromJust )
import Data.Proxy
import Data.Typeable ( Typeable )
import Language.Haskell.TH.Syntax ( Type(ConT), Exp(VarE) )

import Data.Comp.Multi ( unTerm , inject, project, HFunctor, hfmap, (:-<:), All, Sum, caseCxt )

import Cubix.Language.Java.Parametric.Common.Types
import qualified Cubix.Language.Java.Parametric.Full as F
import Cubix.Language.Parametric.Derive
import Cubix.Language.Parametric.InjF
import Cubix.Language.Parametric.Syntax

-- Problem: Some parts of the translation can tear down multiple layers. A VarDeclID
-- is only translated when its parent VarDecl is translated. It's nonsense to just be asked
-- to translate a VarDeclID on its own.
-- 
-- I did want to be able to avoid writing cases that throw errors,
-- while being able to have the type system know that the translation is total.
-- Inspired by how you'd write a hand-traversal to do this, I think the approach to doing this is to have
-- a type-level set of labels at which you can apply the transformation. A translation instance for VarDecl might take the form
--
-- instance (Trans (IdentL :@: ls)) => Trans (IdentL :@: VarDeclL :@: ls) where....
--
-- I think Haskell could do this if it had AC-matching (errr....AC+idempotent) in its typeclass resolver. That would let it infer
-- a fixpoint for the set of labels at which you could apply the translation.
--
-- Overall, this sounds quite infeasible without ACI-matching. At the very least, it seems painful, especially if
-- you have to hand-write the set of applicable labels


translate :: F.JavaTerm l -> MJavaTerm l
translate :: JavaTerm l -> MJavaTerm l
translate = Sum JavaSig JavaTerm l -> MJavaTerm l
forall (f :: (* -> *) -> * -> *) l.
Trans f =>
f JavaTerm l -> MJavaTerm l
trans (Sum JavaSig JavaTerm l -> MJavaTerm l)
-> (JavaTerm l -> Sum JavaSig JavaTerm l)
-> JavaTerm l
-> MJavaTerm l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JavaTerm l -> Sum JavaSig JavaTerm l
forall (f :: (* -> *) -> * -> *) t. HFix f t -> f (HFix f) t
unTerm

translate' :: (InjF MJavaSig l l') => F.JavaTerm l -> MJavaTerm l'
translate' :: JavaTerm l -> MJavaTerm l'
translate' = CxtS NoHole MJavaSig (K ()) l -> MJavaTerm l'
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MJavaSig (K ()) l -> MJavaTerm l')
-> (JavaTerm l -> CxtS NoHole MJavaSig (K ()) l)
-> JavaTerm l
-> MJavaTerm l'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JavaTerm l -> CxtS NoHole MJavaSig (K ()) l
forall l. JavaTerm l -> MJavaTerm l
translate

class Trans f where
  trans :: f F.JavaTerm l -> MJavaTerm l

instance {-# OVERLAPPING #-} (All Trans fs) => Trans (Sum fs) where
  trans :: Sum fs JavaTerm l -> MJavaTerm l
trans = Proxy Trans
-> (forall (f :: (* -> *) -> * -> *).
    Trans f =>
    f JavaTerm l -> MJavaTerm l)
-> Sum fs JavaTerm l
-> MJavaTerm l
forall (cxt :: ((* -> *) -> * -> *) -> Constraint)
       (fs :: [(* -> *) -> * -> *]) (a :: * -> *) e b.
All cxt fs =>
Proxy cxt
-> (forall (f :: (* -> *) -> * -> *). cxt f => f a e -> b)
-> Sum fs a e
-> b
caseCxt (Proxy Trans
forall k (t :: k). Proxy t
Proxy @Trans) forall (f :: (* -> *) -> * -> *).
Trans f =>
f JavaTerm l -> MJavaTerm l
forall (f :: (* -> *) -> * -> *) l.
Trans f =>
f JavaTerm l -> MJavaTerm l
trans

transDefault :: (HFunctor f, f :-<: MJavaSig, f :-<: F.JavaSig) => f F.JavaTerm l -> MJavaTerm l
transDefault :: f JavaTerm l -> MJavaTerm l
transDefault = f (Cxt NoHole (Sum MJavaSig) (K ())) l -> MJavaTerm l
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (f (Cxt NoHole (Sum MJavaSig) (K ())) l -> MJavaTerm l)
-> (f JavaTerm l -> f (Cxt NoHole (Sum MJavaSig) (K ())) l)
-> f JavaTerm l
-> MJavaTerm l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall l. JavaTerm l -> MJavaTerm l)
-> f JavaTerm :-> f (Cxt NoHole (Sum MJavaSig) (K ()))
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap forall l. JavaTerm l -> MJavaTerm l
translate

instance {-# OVERLAPPABLE #-} (HFunctor f, f :-<: MJavaSig, f :-<: F.JavaSig) => Trans f where
  trans :: f JavaTerm l -> MJavaTerm l
trans = f JavaTerm l -> MJavaTerm l
forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: MJavaSig, f :-<: JavaSig) =>
f JavaTerm l -> MJavaTerm l
transDefault

transIdent :: F.JavaTerm F.IdentL -> MJavaTerm IdentL
transIdent :: JavaTerm IdentL -> MJavaTerm IdentL
transIdent (JavaTerm IdentL -> Maybe (Ident JavaTerm IdentL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.Ident s :: String
s)) = String -> MJavaTerm IdentL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(Ident :-<: fs, All HFunctor fs) =>
String -> CxtS h fs a IdentL
Ident' String
s

-- Clone of transIdent because type-safe pattern match
instance Trans F.Ident where
  trans :: Ident JavaTerm l -> MJavaTerm l
trans (F.Ident n :: String
n) = String -> MJavaTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(Ident :-<: fs, InjF fs IdentL j) =>
String -> CxtS h fs a j
iIdent String
n

splitVarDeclId :: F.JavaTerm F.VarDeclIdL -> (Int, MJavaTerm IdentL)
splitVarDeclId :: JavaTerm VarDeclIdL -> (Int, MJavaTerm IdentL)
splitVarDeclId (JavaTerm VarDeclIdL -> Maybe (VarDeclId JavaTerm VarDeclIdL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.VarId ident :: JavaTerm IdentL
ident))      = (0, JavaTerm IdentL -> MJavaTerm IdentL
transIdent JavaTerm IdentL
ident)
splitVarDeclId (JavaTerm VarDeclIdL -> Maybe (VarDeclId JavaTerm VarDeclIdL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.VarDeclArray sub :: JavaTerm VarDeclIdL
sub)) = (Int
dim Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1, MJavaTerm IdentL
id)
  where
    (dim :: Int
dim, id :: MJavaTerm IdentL
id) = JavaTerm VarDeclIdL -> (Int, MJavaTerm IdentL)
splitVarDeclId JavaTerm VarDeclIdL
sub
                                                          

transSingleDecl :: F.JavaTerm F.VarDeclL -> MJavaTerm SingleLocalVarDeclL
transSingleDecl :: JavaTerm VarDeclL -> MJavaTerm SingleLocalVarDeclL
transSingleDecl (JavaTerm VarDeclL -> Maybe (VarDecl JavaTerm VarDeclL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.VarDecl vid :: JavaTerm VarDeclIdL
vid init :: Cxt NoHole (Sum JavaSig) (K ()) (Maybe VarInitL)
init)) = CxtS NoHole MJavaSig (K ()) LocalVarDeclAttrsL
-> CxtS NoHole MJavaSig (K ()) VarDeclBinderL
-> CxtS NoHole MJavaSig (K ()) OptLocalVarInitL
-> MJavaTerm SingleLocalVarDeclL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(SingleLocalVarDecl :-<: fs, All HFunctor fs) =>
CxtS h fs a LocalVarDeclAttrsL
-> CxtS h fs a VarDeclBinderL
-> CxtS h fs a OptLocalVarInitL
-> CxtS h fs a SingleLocalVarDeclL
SingleLocalVarDecl' (Int -> CxtS NoHole MJavaSig (K ()) LocalVarDeclAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(ArrayDimVarDeclAttrs :-<: fs, InjF fs LocalVarDeclAttrsL j) =>
Int -> CxtS h fs a j
iArrayDimVarDeclAttrs Int
dim) (MJavaTerm IdentL -> CxtS NoHole MJavaSig (K ()) VarDeclBinderL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF MJavaTerm IdentL
id) CxtS NoHole MJavaSig (K ()) OptLocalVarInitL
optInit
  where
    (dim :: Int
dim, id :: MJavaTerm IdentL
id) = JavaTerm VarDeclIdL -> (Int, MJavaTerm IdentL)
splitVarDeclId JavaTerm VarDeclIdL
vid

    optInit :: MJavaTerm OptLocalVarInitL
    optInit :: CxtS NoHole MJavaSig (K ()) OptLocalVarInitL
optInit = case Cxt NoHole (Sum JavaSig) (K ()) (Maybe VarInitL)
init of
      Just' x :: Cxt NoHole (Sum JavaSig) (K ()) VarInitL
x  -> CxtS NoHole MJavaSig (K ()) LocalVarInitL
-> CxtS NoHole MJavaSig (K ()) OptLocalVarInitL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(OptLocalVarInit :-<: fs, All HFunctor fs) =>
CxtS h fs a LocalVarInitL -> CxtS h fs a OptLocalVarInitL
JustLocalVarInit' (CxtS NoHole MJavaSig (K ()) LocalVarInitL
 -> CxtS NoHole MJavaSig (K ()) OptLocalVarInitL)
-> CxtS NoHole MJavaSig (K ()) LocalVarInitL
-> CxtS NoHole MJavaSig (K ()) OptLocalVarInitL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MJavaSig (K ()) VarInitL
-> CxtS NoHole MJavaSig (K ()) LocalVarInitL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MJavaSig (K ()) VarInitL
 -> CxtS NoHole MJavaSig (K ()) LocalVarInitL)
-> CxtS NoHole MJavaSig (K ()) VarInitL
-> CxtS NoHole MJavaSig (K ()) LocalVarInitL
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum JavaSig) (K ()) VarInitL
-> CxtS NoHole MJavaSig (K ()) VarInitL
forall l. JavaTerm l -> MJavaTerm l
translate Cxt NoHole (Sum JavaSig) (K ()) VarInitL
x
      Nothing' -> CxtS NoHole MJavaSig (K ()) OptLocalVarInitL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(OptLocalVarInit :-<: fs, All HFunctor fs) =>
CxtS h fs a OptLocalVarInitL
NoLocalVarInit'
                                                                                                                   

instance {-# OVERLAPPING #-} Trans F.BlockStmt where
  trans :: BlockStmt JavaTerm l -> MJavaTerm l
trans t :: BlockStmt JavaTerm l
t@(F.BlockStmt _)              = BlockStmt JavaTerm l -> MJavaTerm l
forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: MJavaSig, f :-<: JavaSig) =>
f JavaTerm l -> MJavaTerm l
transDefault BlockStmt JavaTerm l
t
  trans t :: BlockStmt JavaTerm l
t@(F.LocalClass _)             = BlockStmt JavaTerm l -> MJavaTerm l
forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: MJavaSig, f :-<: JavaSig) =>
f JavaTerm l -> MJavaTerm l
transDefault BlockStmt JavaTerm l
t
  trans t :: BlockStmt JavaTerm l
t@(F.LocalVars mods :: JavaTerm [ModifierL]
mods typ :: JavaTerm TypeL
typ decls :: JavaTerm [VarDeclL]
decls) = CxtS NoHole MJavaSig (K ()) MultiLocalVarDeclCommonAttrsL
-> CxtS NoHole MJavaSig (K ()) [SingleLocalVarDeclL] -> MJavaTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(MultiLocalVarDecl :-<: fs, InjF fs MultiLocalVarDeclL j) =>
CxtS h fs a MultiLocalVarDeclCommonAttrsL
-> CxtS h fs a [SingleLocalVarDeclL] -> CxtS h fs a j
iMultiLocalVarDecl (CxtS NoHole MJavaSig (K ()) ([ModifierL], TypeL)
-> CxtS NoHole MJavaSig (K ()) MultiLocalVarDeclCommonAttrsL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MJavaSig (K ()) ([ModifierL], TypeL)
 -> CxtS NoHole MJavaSig (K ()) MultiLocalVarDeclCommonAttrsL)
-> CxtS NoHole MJavaSig (K ()) ([ModifierL], TypeL)
-> CxtS NoHole MJavaSig (K ()) MultiLocalVarDeclCommonAttrsL
forall a b. (a -> b) -> a -> b
$ JavaTerm ([ModifierL], TypeL)
-> CxtS NoHole MJavaSig (K ()) ([ModifierL], TypeL)
forall l. JavaTerm l -> MJavaTerm l
translate (JavaTerm [ModifierL]
-> JavaTerm TypeL -> JavaTerm ([ModifierL], TypeL)
forall (f :: (* -> *) -> * -> *) i j h (a :: * -> *).
(PairF :<: f, Typeable i, Typeable j) =>
Cxt h f a i -> Cxt h f a j -> Cxt h f a (i, j)
riPairF JavaTerm [ModifierL]
mods JavaTerm TypeL
typ)) (CxtS NoHole MJavaSig (K ()) [SingleLocalVarDeclL] -> MJavaTerm l)
-> CxtS NoHole MJavaSig (K ()) [SingleLocalVarDeclL] -> MJavaTerm l
forall a b. (a -> b) -> a -> b
$ (JavaTerm VarDeclL -> MJavaTerm SingleLocalVarDeclL)
-> JavaTerm [VarDeclL]
-> CxtS NoHole MJavaSig (K ()) [SingleLocalVarDeclL]
forall (f :: * -> *) (h :: * -> *) (g :: * -> *) b a.
(InsertF f h, ExtractF f g, Functor f, Typeable b) =>
(g a -> h b) -> g (f a) -> h (f b)
mapF JavaTerm VarDeclL -> MJavaTerm SingleLocalVarDeclL
transSingleDecl JavaTerm [VarDeclL]
decls

transOp :: F.JavaTerm F.AssignOpL -> MJavaTerm AssignOpL
transOp :: JavaTerm AssignOpL -> MJavaTerm AssignOpL
transOp (JavaTerm AssignOpL -> Maybe (AssignOp JavaTerm AssignOpL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> (Just F.EqualA)) = MJavaTerm AssignOpL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(AssignOpEquals :-<: fs, All HFunctor fs) =>
CxtS h fs a AssignOpL
AssignOpEquals'
transOp x :: JavaTerm AssignOpL
x                            = CxtS NoHole MJavaSig (K ()) AssignOpL -> MJavaTerm AssignOpL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MJavaSig (K ()) AssignOpL -> MJavaTerm AssignOpL)
-> CxtS NoHole MJavaSig (K ()) AssignOpL -> MJavaTerm AssignOpL
forall a b. (a -> b) -> a -> b
$ JavaTerm AssignOpL -> CxtS NoHole MJavaSig (K ()) AssignOpL
forall l. JavaTerm l -> MJavaTerm l
translate JavaTerm AssignOpL
x

instance {-# OVERLAPPING #-} Trans F.Exp where
  trans :: Exp JavaTerm l -> MJavaTerm l
trans t :: Exp JavaTerm l
t@(F.Assign lhs :: JavaTerm LhsL
lhs op :: JavaTerm AssignOpL
op rhs :: JavaTerm ExpL
rhs) = CxtS NoHole MJavaSig (K ()) LhsL
-> MJavaTerm AssignOpL
-> CxtS NoHole MJavaSig (K ()) RhsL
-> MJavaTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(Assign :-<: fs, InjF fs AssignL j) =>
CxtS h fs a LhsL
-> CxtS h fs a AssignOpL -> CxtS h fs a RhsL -> CxtS h fs a j
iAssign (CxtS NoHole MJavaSig (K ()) LhsL
-> CxtS NoHole MJavaSig (K ()) LhsL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MJavaSig (K ()) LhsL
 -> CxtS NoHole MJavaSig (K ()) LhsL)
-> CxtS NoHole MJavaSig (K ()) LhsL
-> CxtS NoHole MJavaSig (K ()) LhsL
forall a b. (a -> b) -> a -> b
$ JavaTerm LhsL -> CxtS NoHole MJavaSig (K ()) LhsL
forall l. JavaTerm l -> MJavaTerm l
translate JavaTerm LhsL
lhs) (JavaTerm AssignOpL -> MJavaTerm AssignOpL
transOp JavaTerm AssignOpL
op) (CxtS NoHole MJavaSig (K ()) ExpL
-> CxtS NoHole MJavaSig (K ()) RhsL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MJavaSig (K ()) ExpL
 -> CxtS NoHole MJavaSig (K ()) RhsL)
-> CxtS NoHole MJavaSig (K ()) ExpL
-> CxtS NoHole MJavaSig (K ()) RhsL
forall a b. (a -> b) -> a -> b
$ JavaTerm ExpL -> CxtS NoHole MJavaSig (K ()) ExpL
forall l. JavaTerm l -> MJavaTerm l
translate JavaTerm ExpL
rhs)
  trans t :: Exp JavaTerm l
t                       = Exp JavaTerm l -> MJavaTerm l
forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: MJavaSig, f :-<: JavaSig) =>
f JavaTerm l -> MJavaTerm l
transDefault Exp JavaTerm l
t

instance {-# OVERLAPPING #-} Trans F.MethodInvocation where
  trans :: MethodInvocation JavaTerm l -> MJavaTerm l
trans (F.MethodCall nam :: JavaTerm NameL
nam args :: JavaTerm [ExpL]
args) = CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
-> CxtS NoHole MJavaSig (K ()) FunctionExpL
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
-> MJavaTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(FunctionCall :-<: fs, InjF fs FunctionCallL j) =>
CxtS h fs a FunctionCallAttrsL
-> CxtS h fs a FunctionExpL
-> CxtS h fs a FunctionArgumentsL
-> CxtS h fs a j
iFunctionCall (CxtS NoHole MJavaSig (K ()) [RefTypeL]
-> CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(JavaTypeArgs :-<: fs, InjF fs FunctionCallAttrsL j) =>
CxtS h fs a [RefTypeL] -> CxtS h fs a j
iJavaTypeArgs CxtS NoHole MJavaSig (K ()) [RefTypeL]
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) l.
(ListF :<: f, Typeable l) =>
Cxt h f a [l]
riNilF)
                                                CxtS NoHole MJavaSig (K ()) FunctionExpL
f
                                                (CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(FunctionArgumentList :-<: fs, All HFunctor fs) =>
CxtS h fs a [FunctionArgumentL] -> CxtS h fs a FunctionArgumentsL
FunctionArgumentList' (CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
 -> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL)
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a [l] -> Cxt h f a [l]
ConsF' (CxtS NoHole MJavaSig (K ()) ReceiverL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(ReceiverArg :-<: fs, All HFunctor fs) =>
CxtS h fs a ReceiverL -> CxtS h fs a FunctionArgumentL
ReceiverArg' CxtS NoHole MJavaSig (K ()) ReceiverL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(JavaReceiver :-<: fs, InjF fs ReceiverL j) =>
CxtS h fs a j
iImplicitReceiver)
                                                                                ((JavaTerm ExpL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> JavaTerm [ExpL]
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
forall (f :: * -> *) (h :: * -> *) (g :: * -> *) b a.
(InsertF f h, ExtractF f g, Functor f, Typeable b) =>
(g a -> h b) -> g (f a) -> h (f b)
mapF (CxtS NoHole MJavaSig (K ()) ExpL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MJavaSig (K ()) ExpL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> (JavaTerm ExpL -> CxtS NoHole MJavaSig (K ()) ExpL)
-> JavaTerm ExpL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JavaTerm ExpL -> CxtS NoHole MJavaSig (K ()) ExpL
forall l. JavaTerm l -> MJavaTerm l
translate) JavaTerm [ExpL]
args))
    where
      f :: CxtS NoHole MJavaSig (K ()) FunctionExpL
f = case JavaTerm NameL
nam of
            (JavaTerm NameL -> Maybe (Name JavaTerm NameL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.Name (SingletonF' n :: JavaTerm IdentL
n))) -> MJavaTerm IdentL -> CxtS NoHole MJavaSig (K ()) FunctionExpL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (MJavaTerm IdentL -> CxtS NoHole MJavaSig (K ()) FunctionExpL)
-> MJavaTerm IdentL -> CxtS NoHole MJavaSig (K ()) FunctionExpL
forall a b. (a -> b) -> a -> b
$ JavaTerm IdentL -> MJavaTerm IdentL
transIdent JavaTerm IdentL
n
            _                                          -> CxtS NoHole MJavaSig (K ()) NameL
-> CxtS NoHole MJavaSig (K ()) FunctionExpL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MJavaSig (K ()) NameL
 -> CxtS NoHole MJavaSig (K ()) FunctionExpL)
-> CxtS NoHole MJavaSig (K ()) NameL
-> CxtS NoHole MJavaSig (K ()) FunctionExpL
forall a b. (a -> b) -> a -> b
$ JavaTerm NameL -> CxtS NoHole MJavaSig (K ()) NameL
forall l. JavaTerm l -> MJavaTerm l
translate JavaTerm NameL
nam
  trans (F.PrimaryMethodCall e :: JavaTerm ExpL
e targs :: JavaTerm [RefTypeL]
targs n :: JavaTerm IdentL
n args :: JavaTerm [ExpL]
args) = CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
-> CxtS NoHole MJavaSig (K ()) FunctionExpL
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
-> MJavaTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(FunctionCall :-<: fs, InjF fs FunctionCallL j) =>
CxtS h fs a FunctionCallAttrsL
-> CxtS h fs a FunctionExpL
-> CxtS h fs a FunctionArgumentsL
-> CxtS h fs a j
iFunctionCall (CxtS NoHole MJavaSig (K ()) [RefTypeL]
-> CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(JavaTypeArgs :-<: fs, InjF fs FunctionCallAttrsL j) =>
CxtS h fs a [RefTypeL] -> CxtS h fs a j
iJavaTypeArgs (CxtS NoHole MJavaSig (K ()) [RefTypeL]
 -> CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL)
-> CxtS NoHole MJavaSig (K ()) [RefTypeL]
-> CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
forall a b. (a -> b) -> a -> b
$ JavaTerm [RefTypeL] -> CxtS NoHole MJavaSig (K ()) [RefTypeL]
forall l. JavaTerm l -> MJavaTerm l
translate JavaTerm [RefTypeL]
targs)
                                                             (MJavaTerm IdentL -> CxtS NoHole MJavaSig (K ()) FunctionExpL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (MJavaTerm IdentL -> CxtS NoHole MJavaSig (K ()) FunctionExpL)
-> MJavaTerm IdentL -> CxtS NoHole MJavaSig (K ()) FunctionExpL
forall a b. (a -> b) -> a -> b
$ JavaTerm IdentL -> MJavaTerm IdentL
transIdent JavaTerm IdentL
n)
                                                             (CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(FunctionArgumentList :-<: fs, All HFunctor fs) =>
CxtS h fs a [FunctionArgumentL] -> CxtS h fs a FunctionArgumentsL
FunctionArgumentList' (CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
 -> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL)
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a [l] -> Cxt h f a [l]
ConsF' (CxtS NoHole MJavaSig (K ()) ReceiverL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(ReceiverArg :-<: fs, All HFunctor fs) =>
CxtS h fs a ReceiverL -> CxtS h fs a FunctionArgumentL
ReceiverArg' (CxtS NoHole MJavaSig (K ()) ReceiverL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> CxtS NoHole MJavaSig (K ()) ReceiverL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MJavaSig (K ()) ExpL
-> CxtS NoHole MJavaSig (K ()) ReceiverL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(JavaReceiver :-<: fs, InjF fs ReceiverL j) =>
CxtS h fs a ExpL -> CxtS h fs a j
iPrimaryReceiver (CxtS NoHole MJavaSig (K ()) ExpL
 -> CxtS NoHole MJavaSig (K ()) ReceiverL)
-> CxtS NoHole MJavaSig (K ()) ExpL
-> CxtS NoHole MJavaSig (K ()) ReceiverL
forall a b. (a -> b) -> a -> b
$ JavaTerm ExpL -> CxtS NoHole MJavaSig (K ()) ExpL
forall l. JavaTerm l -> MJavaTerm l
translate JavaTerm ExpL
e)
                                                                                                             ((JavaTerm ExpL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> JavaTerm [ExpL]
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
forall (f :: * -> *) (h :: * -> *) (g :: * -> *) b a.
(InsertF f h, ExtractF f g, Functor f, Typeable b) =>
(g a -> h b) -> g (f a) -> h (f b)
mapF (CxtS NoHole MJavaSig (K ()) ExpL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MJavaSig (K ()) ExpL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> (JavaTerm ExpL -> CxtS NoHole MJavaSig (K ()) ExpL)
-> JavaTerm ExpL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JavaTerm ExpL -> CxtS NoHole MJavaSig (K ()) ExpL
forall l. JavaTerm l -> MJavaTerm l
translate) JavaTerm [ExpL]
args))
  trans (F.SuperMethodCall targs :: JavaTerm [RefTypeL]
targs n :: JavaTerm IdentL
n args :: JavaTerm [ExpL]
args)     = CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
-> CxtS NoHole MJavaSig (K ()) FunctionExpL
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
-> MJavaTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(FunctionCall :-<: fs, InjF fs FunctionCallL j) =>
CxtS h fs a FunctionCallAttrsL
-> CxtS h fs a FunctionExpL
-> CxtS h fs a FunctionArgumentsL
-> CxtS h fs a j
iFunctionCall (CxtS NoHole MJavaSig (K ()) [RefTypeL]
-> CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(JavaTypeArgs :-<: fs, InjF fs FunctionCallAttrsL j) =>
CxtS h fs a [RefTypeL] -> CxtS h fs a j
iJavaTypeArgs (CxtS NoHole MJavaSig (K ()) [RefTypeL]
 -> CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL)
-> CxtS NoHole MJavaSig (K ()) [RefTypeL]
-> CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
forall a b. (a -> b) -> a -> b
$ JavaTerm [RefTypeL] -> CxtS NoHole MJavaSig (K ()) [RefTypeL]
forall l. JavaTerm l -> MJavaTerm l
translate JavaTerm [RefTypeL]
targs)
                                                             (MJavaTerm IdentL -> CxtS NoHole MJavaSig (K ()) FunctionExpL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (MJavaTerm IdentL -> CxtS NoHole MJavaSig (K ()) FunctionExpL)
-> MJavaTerm IdentL -> CxtS NoHole MJavaSig (K ()) FunctionExpL
forall a b. (a -> b) -> a -> b
$ JavaTerm IdentL -> MJavaTerm IdentL
transIdent JavaTerm IdentL
n)
                                                             (CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(FunctionArgumentList :-<: fs, All HFunctor fs) =>
CxtS h fs a [FunctionArgumentL] -> CxtS h fs a FunctionArgumentsL
FunctionArgumentList' (CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
 -> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL)
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a [l] -> Cxt h f a [l]
ConsF' (CxtS NoHole MJavaSig (K ()) ReceiverL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(ReceiverArg :-<: fs, All HFunctor fs) =>
CxtS h fs a ReceiverL -> CxtS h fs a FunctionArgumentL
ReceiverArg' (CxtS NoHole MJavaSig (K ()) ReceiverL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> CxtS NoHole MJavaSig (K ()) ReceiverL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MJavaSig (K ()) ReceiverL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(JavaReceiver :-<: fs, InjF fs ReceiverL j) =>
CxtS h fs a j
iSuperReceiver)
                                                                                             ((JavaTerm ExpL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> JavaTerm [ExpL]
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
forall (f :: * -> *) (h :: * -> *) (g :: * -> *) b a.
(InsertF f h, ExtractF f g, Functor f, Typeable b) =>
(g a -> h b) -> g (f a) -> h (f b)
mapF (CxtS NoHole MJavaSig (K ()) ExpL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MJavaSig (K ()) ExpL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> (JavaTerm ExpL -> CxtS NoHole MJavaSig (K ()) ExpL)
-> JavaTerm ExpL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JavaTerm ExpL -> CxtS NoHole MJavaSig (K ()) ExpL
forall l. JavaTerm l -> MJavaTerm l
translate) JavaTerm [ExpL]
args))
  trans (F.ClassMethodCall typ :: JavaTerm NameL
typ targs :: JavaTerm [RefTypeL]
targs n :: JavaTerm IdentL
n args :: JavaTerm [ExpL]
args) = CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
-> CxtS NoHole MJavaSig (K ()) FunctionExpL
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
-> MJavaTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(FunctionCall :-<: fs, InjF fs FunctionCallL j) =>
CxtS h fs a FunctionCallAttrsL
-> CxtS h fs a FunctionExpL
-> CxtS h fs a FunctionArgumentsL
-> CxtS h fs a j
iFunctionCall (CxtS NoHole MJavaSig (K ()) [RefTypeL]
-> CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(JavaTypeArgs :-<: fs, InjF fs FunctionCallAttrsL j) =>
CxtS h fs a [RefTypeL] -> CxtS h fs a j
iJavaTypeArgs (CxtS NoHole MJavaSig (K ()) [RefTypeL]
 -> CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL)
-> CxtS NoHole MJavaSig (K ()) [RefTypeL]
-> CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
forall a b. (a -> b) -> a -> b
$ JavaTerm [RefTypeL] -> CxtS NoHole MJavaSig (K ()) [RefTypeL]
forall l. JavaTerm l -> MJavaTerm l
translate JavaTerm [RefTypeL]
targs)
                                                             (MJavaTerm IdentL -> CxtS NoHole MJavaSig (K ()) FunctionExpL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (MJavaTerm IdentL -> CxtS NoHole MJavaSig (K ()) FunctionExpL)
-> MJavaTerm IdentL -> CxtS NoHole MJavaSig (K ()) FunctionExpL
forall a b. (a -> b) -> a -> b
$ JavaTerm IdentL -> MJavaTerm IdentL
transIdent JavaTerm IdentL
n)
                                                             (CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(FunctionArgumentList :-<: fs, All HFunctor fs) =>
CxtS h fs a [FunctionArgumentL] -> CxtS h fs a FunctionArgumentsL
FunctionArgumentList' (CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
 -> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL)
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a [l] -> Cxt h f a [l]
ConsF' (CxtS NoHole MJavaSig (K ()) ReceiverL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(ReceiverArg :-<: fs, All HFunctor fs) =>
CxtS h fs a ReceiverL -> CxtS h fs a FunctionArgumentL
ReceiverArg' (CxtS NoHole MJavaSig (K ()) ReceiverL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> CxtS NoHole MJavaSig (K ()) ReceiverL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MJavaSig (K ()) NameL
-> CxtS NoHole MJavaSig (K ()) ReceiverL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(JavaReceiver :-<: fs, InjF fs ReceiverL j) =>
CxtS h fs a NameL -> CxtS h fs a j
iClassSuperReceiver (CxtS NoHole MJavaSig (K ()) NameL
 -> CxtS NoHole MJavaSig (K ()) ReceiverL)
-> CxtS NoHole MJavaSig (K ()) NameL
-> CxtS NoHole MJavaSig (K ()) ReceiverL
forall a b. (a -> b) -> a -> b
$ JavaTerm NameL -> CxtS NoHole MJavaSig (K ()) NameL
forall l. JavaTerm l -> MJavaTerm l
translate JavaTerm NameL
typ)
                                                                                             ((JavaTerm ExpL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> JavaTerm [ExpL]
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
forall (f :: * -> *) (h :: * -> *) (g :: * -> *) b a.
(InsertF f h, ExtractF f g, Functor f, Typeable b) =>
(g a -> h b) -> g (f a) -> h (f b)
mapF (CxtS NoHole MJavaSig (K ()) ExpL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MJavaSig (K ()) ExpL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> (JavaTerm ExpL -> CxtS NoHole MJavaSig (K ()) ExpL)
-> JavaTerm ExpL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JavaTerm ExpL -> CxtS NoHole MJavaSig (K ()) ExpL
forall l. JavaTerm l -> MJavaTerm l
translate) JavaTerm [ExpL]
args))
  trans (F.TypeMethodCall  typ :: JavaTerm NameL
typ targs :: JavaTerm [RefTypeL]
targs n :: JavaTerm IdentL
n args :: JavaTerm [ExpL]
args) = CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
-> CxtS NoHole MJavaSig (K ()) FunctionExpL
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
-> MJavaTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(FunctionCall :-<: fs, InjF fs FunctionCallL j) =>
CxtS h fs a FunctionCallAttrsL
-> CxtS h fs a FunctionExpL
-> CxtS h fs a FunctionArgumentsL
-> CxtS h fs a j
iFunctionCall (CxtS NoHole MJavaSig (K ()) [RefTypeL]
-> CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(JavaTypeArgs :-<: fs, InjF fs FunctionCallAttrsL j) =>
CxtS h fs a [RefTypeL] -> CxtS h fs a j
iJavaTypeArgs (CxtS NoHole MJavaSig (K ()) [RefTypeL]
 -> CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL)
-> CxtS NoHole MJavaSig (K ()) [RefTypeL]
-> CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
forall a b. (a -> b) -> a -> b
$ JavaTerm [RefTypeL] -> CxtS NoHole MJavaSig (K ()) [RefTypeL]
forall l. JavaTerm l -> MJavaTerm l
translate JavaTerm [RefTypeL]
targs)
                                                             (MJavaTerm IdentL -> CxtS NoHole MJavaSig (K ()) FunctionExpL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (MJavaTerm IdentL -> CxtS NoHole MJavaSig (K ()) FunctionExpL)
-> MJavaTerm IdentL -> CxtS NoHole MJavaSig (K ()) FunctionExpL
forall a b. (a -> b) -> a -> b
$ JavaTerm IdentL -> MJavaTerm IdentL
transIdent JavaTerm IdentL
n)
                                                             (CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(FunctionArgumentList :-<: fs, All HFunctor fs) =>
CxtS h fs a [FunctionArgumentL] -> CxtS h fs a FunctionArgumentsL
FunctionArgumentList' (CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
 -> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL)
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a [l] -> Cxt h f a [l]
ConsF' (CxtS NoHole MJavaSig (K ()) ReceiverL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(ReceiverArg :-<: fs, All HFunctor fs) =>
CxtS h fs a ReceiverL -> CxtS h fs a FunctionArgumentL
ReceiverArg' (CxtS NoHole MJavaSig (K ()) ReceiverL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> CxtS NoHole MJavaSig (K ()) ReceiverL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MJavaSig (K ()) NameL
-> CxtS NoHole MJavaSig (K ()) ReceiverL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(JavaReceiver :-<: fs, InjF fs ReceiverL j) =>
CxtS h fs a NameL -> CxtS h fs a j
iTypeReceiver (CxtS NoHole MJavaSig (K ()) NameL
 -> CxtS NoHole MJavaSig (K ()) ReceiverL)
-> CxtS NoHole MJavaSig (K ()) NameL
-> CxtS NoHole MJavaSig (K ()) ReceiverL
forall a b. (a -> b) -> a -> b
$ JavaTerm NameL -> CxtS NoHole MJavaSig (K ()) NameL
forall l. JavaTerm l -> MJavaTerm l
translate JavaTerm NameL
typ)
                                                                                                             ((JavaTerm ExpL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> JavaTerm [ExpL]
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
forall (f :: * -> *) (h :: * -> *) (g :: * -> *) b a.
(InsertF f h, ExtractF f g, Functor f, Typeable b) =>
(g a -> h b) -> g (f a) -> h (f b)
mapF (CxtS NoHole MJavaSig (K ()) ExpL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MJavaSig (K ()) ExpL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> (JavaTerm ExpL -> CxtS NoHole MJavaSig (K ()) ExpL)
-> JavaTerm ExpL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JavaTerm ExpL -> CxtS NoHole MJavaSig (K ()) ExpL
forall l. JavaTerm l -> MJavaTerm l
translate) JavaTerm [ExpL]
args))

transBlock :: F.JavaTerm F.BlockL -> MJavaTerm BlockL
transBlock :: JavaTerm BlockL -> MJavaTerm BlockL
transBlock (JavaTerm BlockL -> Maybe (Block JavaTerm BlockL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.Block stmts :: Cxt NoHole (Sum JavaSig) (K ()) [BlockStmtL]
stmts)) = CxtS NoHole MJavaSig (K ()) [BlockItemL]
-> CxtS NoHole MJavaSig (K ()) BlockEndL -> MJavaTerm BlockL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(Block :-<: fs, All HFunctor fs) =>
CxtS h fs a [BlockItemL]
-> CxtS h fs a BlockEndL -> CxtS h fs a BlockL
Block' ((Cxt NoHole (Sum JavaSig) (K ()) BlockStmtL
 -> Cxt NoHole (Sum MJavaSig) (K ()) BlockItemL)
-> Cxt NoHole (Sum JavaSig) (K ()) [BlockStmtL]
-> CxtS NoHole MJavaSig (K ()) [BlockItemL]
forall (f :: * -> *) (h :: * -> *) (g :: * -> *) b a.
(InsertF f h, ExtractF f g, Functor f, Typeable b) =>
(g a -> h b) -> g (f a) -> h (f b)
mapF (CxtS NoHole MJavaSig (K ()) BlockStmtL
-> Cxt NoHole (Sum MJavaSig) (K ()) BlockItemL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF(CxtS NoHole MJavaSig (K ()) BlockStmtL
 -> Cxt NoHole (Sum MJavaSig) (K ()) BlockItemL)
-> (Cxt NoHole (Sum JavaSig) (K ()) BlockStmtL
    -> CxtS NoHole MJavaSig (K ()) BlockStmtL)
-> Cxt NoHole (Sum JavaSig) (K ()) BlockStmtL
-> Cxt NoHole (Sum MJavaSig) (K ()) BlockItemL
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cxt NoHole (Sum JavaSig) (K ()) BlockStmtL
-> CxtS NoHole MJavaSig (K ()) BlockStmtL
forall l. JavaTerm l -> MJavaTerm l
translate) Cxt NoHole (Sum JavaSig) (K ()) [BlockStmtL]
stmts) CxtS NoHole MJavaSig (K ()) BlockEndL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(EmptyBlockEnd :-<: fs, All HFunctor fs) =>
CxtS h fs a BlockEndL
EmptyBlockEnd'

instance {-# OVERLAPPING #-} Trans F.Block where
  trans :: Block JavaTerm l -> MJavaTerm l
trans b :: Block JavaTerm l
b@(F.Block _) = MJavaTerm BlockL -> MJavaTerm l
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (MJavaTerm BlockL -> MJavaTerm l)
-> MJavaTerm BlockL -> MJavaTerm l
forall a b. (a -> b) -> a -> b
$ JavaTerm BlockL -> MJavaTerm BlockL
transBlock (JavaTerm BlockL -> MJavaTerm BlockL)
-> JavaTerm BlockL -> MJavaTerm BlockL
forall a b. (a -> b) -> a -> b
$ Block JavaTerm l -> Cxt NoHole (Sum JavaSig) (K ()) l
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject Block JavaTerm l
b

transParamDecl :: F.JavaTerm F.FormalParamL -> MJavaTerm FunctionParameterDeclL
transParamDecl :: JavaTerm FormalParamL -> MJavaTerm FunctionParameterDeclL
transParamDecl (JavaTerm FormalParamL -> Maybe (FormalParam JavaTerm FormalParamL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.FormalParam mods :: JavaTerm [ModifierL]
mods tp :: JavaTerm TypeL
tp isVarargs :: Bool
isVarargs vid :: JavaTerm VarDeclIdL
vid)) =
    if Bool
isVarargs then
      CxtS NoHole MJavaSig (K ()) JavaParamAttrsL
-> MJavaTerm IdentL -> MJavaTerm FunctionParameterDeclL
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 NoHole MJavaSig (K ()) JavaParamAttrsL
attrs MJavaTerm IdentL
n
    else
      CxtS NoHole MJavaSig (K ()) FunctionParameterDeclAttrsL
-> MJavaTerm IdentL -> MJavaTerm FunctionParameterDeclL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(PositionalParameterDeclWithIdent :-<: fs,
 InjF fs FunctionParameterDeclL j) =>
CxtS h fs a FunctionParameterDeclAttrsL
-> CxtS h fs a IdentL -> CxtS h fs a j
iPositionalParameterDeclWithIdent (CxtS NoHole MJavaSig (K ()) JavaParamAttrsL
-> CxtS NoHole MJavaSig (K ()) FunctionParameterDeclAttrsL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF CxtS NoHole MJavaSig (K ()) JavaParamAttrsL
attrs) MJavaTerm IdentL
n
  where
    (dim :: Int
dim, n :: MJavaTerm IdentL
n) = JavaTerm VarDeclIdL -> (Int, MJavaTerm IdentL)
splitVarDeclId JavaTerm VarDeclIdL
vid

    attrs :: MJavaTerm JavaParamAttrsL
    attrs :: CxtS NoHole MJavaSig (K ()) JavaParamAttrsL
attrs = CxtS NoHole MJavaSig (K ()) [ModifierL]
-> CxtS NoHole MJavaSig (K ()) TypeL
-> Int
-> CxtS NoHole MJavaSig (K ()) 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 (JavaTerm [ModifierL] -> CxtS NoHole MJavaSig (K ()) [ModifierL]
forall l. JavaTerm l -> MJavaTerm l
translate JavaTerm [ModifierL]
mods) (JavaTerm TypeL -> CxtS NoHole MJavaSig (K ()) TypeL
forall l. JavaTerm l -> MJavaTerm l
translate JavaTerm TypeL
tp) Int
dim


-- Yes, this is almost copy+paste of the previous function. It's
-- not obvious how to share code effectively between them. Basically, the issue
-- is that the ParameterDecl/Parameter type hierarchy is identical for Java, but we've
-- split them because they're in general different (i.e.: in C)
transParam :: F.JavaTerm F.FormalParamL -> MJavaTerm FunctionParameterL
transParam :: JavaTerm FormalParamL -> MJavaTerm FunctionParameterL
transParam (JavaTerm FormalParamL -> Maybe (FormalParam JavaTerm FormalParamL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.FormalParam mods :: JavaTerm [ModifierL]
mods tp :: JavaTerm TypeL
tp isVarargs :: Bool
isVarargs vid :: JavaTerm VarDeclIdL
vid)) =
    if Bool
isVarargs then
      CxtS NoHole MJavaSig (K ()) JavaParamAttrsL
-> MJavaTerm IdentL -> MJavaTerm FunctionParameterL
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 NoHole MJavaSig (K ()) JavaParamAttrsL
attrs MJavaTerm IdentL
n
    else
      CxtS NoHole MJavaSig (K ()) ParameterAttrsL
-> MJavaTerm IdentL -> MJavaTerm FunctionParameterL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(PositionalParameter :-<: fs, InjF fs FunctionParameterL j) =>
CxtS h fs a ParameterAttrsL -> CxtS h fs a IdentL -> CxtS h fs a j
iPositionalParameter (CxtS NoHole MJavaSig (K ()) JavaParamAttrsL
-> CxtS NoHole MJavaSig (K ()) ParameterAttrsL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF CxtS NoHole MJavaSig (K ()) JavaParamAttrsL
attrs) MJavaTerm IdentL
n
  where
    (dim :: Int
dim, n :: MJavaTerm IdentL
n) = JavaTerm VarDeclIdL -> (Int, MJavaTerm IdentL)
splitVarDeclId JavaTerm VarDeclIdL
vid

    attrs :: MJavaTerm JavaParamAttrsL
    attrs :: CxtS NoHole MJavaSig (K ()) JavaParamAttrsL
attrs = CxtS NoHole MJavaSig (K ()) [ModifierL]
-> CxtS NoHole MJavaSig (K ()) TypeL
-> Int
-> CxtS NoHole MJavaSig (K ()) 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 (JavaTerm [ModifierL] -> CxtS NoHole MJavaSig (K ()) [ModifierL]
forall l. JavaTerm l -> MJavaTerm l
translate JavaTerm [ModifierL]
mods) (JavaTerm TypeL -> CxtS NoHole MJavaSig (K ()) TypeL
forall l. JavaTerm l -> MJavaTerm l
translate JavaTerm TypeL
tp) Int
dim

-- The Nothing' field is for default methods; Java 8 only
instance {-# OVERLAPPING #-} Trans F.MemberDecl where
  trans :: MemberDecl JavaTerm l -> MJavaTerm l
trans (F.MethodDecl mods :: JavaTerm [ModifierL]
mods tparams :: JavaTerm [TypeParamL]
tparams typ :: JavaTerm (Maybe TypeL)
typ n :: JavaTerm IdentL
n params :: JavaTerm [FormalParamL]
params ex :: JavaTerm [RefTypeL]
ex Nothing' body :: JavaTerm MethodBodyL
body) =
      case JavaTerm MethodBodyL -> Maybe (MethodBody JavaTerm MethodBodyL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project JavaTerm MethodBodyL
body of
        Just (F.MethodBody Nothing') -> CxtS NoHole MJavaSig (K ()) FunctionDeclAttrsL
-> MJavaTerm IdentL
-> CxtS NoHole MJavaSig (K ()) [FunctionParameterDeclL]
-> MJavaTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(FunctionDecl :-<: fs, InjF fs FunctionDeclL j) =>
CxtS h fs a FunctionDeclAttrsL
-> CxtS h fs a IdentL
-> CxtS h fs a [FunctionParameterDeclL]
-> CxtS h fs a j
iFunctionDecl (CxtS NoHole MJavaSig (K ()) JavaMethodDeclAttrsL
-> CxtS NoHole MJavaSig (K ()) FunctionDeclAttrsL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF CxtS NoHole MJavaSig (K ()) JavaMethodDeclAttrsL
attrs) (JavaTerm IdentL -> MJavaTerm IdentL
transIdent JavaTerm IdentL
n) (MJavaTerm FunctionParameterDeclL
-> CxtS NoHole MJavaSig (K ()) [FunctionParameterDeclL]
-> CxtS NoHole MJavaSig (K ()) [FunctionParameterDeclL]
forall l.
Typeable l =>
MJavaTerm l -> MJavaTerm [l] -> MJavaTerm [l]
addUnlessStatic MJavaTerm FunctionParameterDeclL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(SelfParameterDecl :-<: fs, All HFunctor fs) =>
CxtS h fs a FunctionParameterDeclL
SelfParameterDecl' (CxtS NoHole MJavaSig (K ()) [FunctionParameterDeclL]
 -> CxtS NoHole MJavaSig (K ()) [FunctionParameterDeclL])
-> CxtS NoHole MJavaSig (K ()) [FunctionParameterDeclL]
-> CxtS NoHole MJavaSig (K ()) [FunctionParameterDeclL]
forall a b. (a -> b) -> a -> b
$ (JavaTerm FormalParamL -> MJavaTerm FunctionParameterDeclL)
-> JavaTerm [FormalParamL]
-> CxtS NoHole MJavaSig (K ()) [FunctionParameterDeclL]
forall (f :: * -> *) (h :: * -> *) (g :: * -> *) b a.
(InsertF f h, ExtractF f g, Functor f, Typeable b) =>
(g a -> h b) -> g (f a) -> h (f b)
mapF JavaTerm FormalParamL -> MJavaTerm FunctionParameterDeclL
transParamDecl JavaTerm [FormalParamL]
params)
        Just (F.MethodBody (Just' b :: JavaTerm BlockL
b)) -> CxtS NoHole MJavaSig (K ()) FunctionDefAttrsL
-> MJavaTerm IdentL
-> CxtS NoHole MJavaSig (K ()) [FunctionParameterL]
-> CxtS NoHole MJavaSig (K ()) FunctionBodyL
-> MJavaTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(FunctionDef :-<: fs, InjF fs FunctionDefL j) =>
CxtS h fs a FunctionDefAttrsL
-> CxtS h fs a IdentL
-> CxtS h fs a [FunctionParameterL]
-> CxtS h fs a FunctionBodyL
-> CxtS h fs a j
iFunctionDef  (CxtS NoHole MJavaSig (K ()) JavaMethodDeclAttrsL
-> CxtS NoHole MJavaSig (K ()) FunctionDefAttrsL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF CxtS NoHole MJavaSig (K ()) JavaMethodDeclAttrsL
attrs) (JavaTerm IdentL -> MJavaTerm IdentL
transIdent JavaTerm IdentL
n) (MJavaTerm FunctionParameterL
-> CxtS NoHole MJavaSig (K ()) [FunctionParameterL]
-> CxtS NoHole MJavaSig (K ()) [FunctionParameterL]
forall l.
Typeable l =>
MJavaTerm l -> MJavaTerm [l] -> MJavaTerm [l]
addUnlessStatic MJavaTerm FunctionParameterL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(SelfParameter :-<: fs, All HFunctor fs) =>
CxtS h fs a FunctionParameterL
SelfParameter' (CxtS NoHole MJavaSig (K ()) [FunctionParameterL]
 -> CxtS NoHole MJavaSig (K ()) [FunctionParameterL])
-> CxtS NoHole MJavaSig (K ()) [FunctionParameterL]
-> CxtS NoHole MJavaSig (K ()) [FunctionParameterL]
forall a b. (a -> b) -> a -> b
$ (JavaTerm FormalParamL -> MJavaTerm FunctionParameterL)
-> JavaTerm [FormalParamL]
-> CxtS NoHole MJavaSig (K ()) [FunctionParameterL]
forall (f :: * -> *) (h :: * -> *) (g :: * -> *) b a.
(InsertF f h, ExtractF f g, Functor f, Typeable b) =>
(g a -> h b) -> g (f a) -> h (f b)
mapF JavaTerm FormalParamL -> MJavaTerm FunctionParameterL
transParam JavaTerm [FormalParamL]
params) (MJavaTerm BlockL -> CxtS NoHole MJavaSig (K ()) FunctionBodyL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (MJavaTerm BlockL -> CxtS NoHole MJavaSig (K ()) FunctionBodyL)
-> MJavaTerm BlockL -> CxtS NoHole MJavaSig (K ()) FunctionBodyL
forall a b. (a -> b) -> a -> b
$ JavaTerm BlockL -> MJavaTerm BlockL
transBlock JavaTerm BlockL
b)
    where
      attrs :: MJavaTerm JavaMethodDeclAttrsL
      attrs :: CxtS NoHole MJavaSig (K ()) JavaMethodDeclAttrsL
attrs = CxtS NoHole MJavaSig (K ()) [ModifierL]
-> CxtS NoHole MJavaSig (K ()) [TypeParamL]
-> CxtS NoHole MJavaSig (K ()) (Maybe TypeL)
-> CxtS NoHole MJavaSig (K ()) [RefTypeL]
-> CxtS NoHole MJavaSig (K ()) 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 (JavaTerm [ModifierL] -> CxtS NoHole MJavaSig (K ()) [ModifierL]
forall l. JavaTerm l -> MJavaTerm l
translate JavaTerm [ModifierL]
mods) (JavaTerm [TypeParamL] -> CxtS NoHole MJavaSig (K ()) [TypeParamL]
forall l. JavaTerm l -> MJavaTerm l
translate JavaTerm [TypeParamL]
tparams) (JavaTerm (Maybe TypeL) -> CxtS NoHole MJavaSig (K ()) (Maybe TypeL)
forall l. JavaTerm l -> MJavaTerm l
translate JavaTerm (Maybe TypeL)
typ) (JavaTerm [RefTypeL] -> CxtS NoHole MJavaSig (K ()) [RefTypeL]
forall l. JavaTerm l -> MJavaTerm l
translate JavaTerm [RefTypeL]
ex)

      addUnlessStatic :: Typeable l => MJavaTerm l -> MJavaTerm [l] -> MJavaTerm [l]
      addUnlessStatic :: MJavaTerm l -> MJavaTerm [l] -> MJavaTerm [l]
addUnlessStatic x :: MJavaTerm l
x l :: MJavaTerm [l]
l = if CxtS NoHole JavaSig (K ()) ModifierL
-> [CxtS NoHole JavaSig (K ()) ModifierL] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem CxtS NoHole JavaSig (K ()) ModifierL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(Modifier :-<: fs, InjF fs ModifierL j) =>
CxtS h fs a j
F.iStatic (JavaTerm [ModifierL] -> [CxtS NoHole JavaSig (K ()) ModifierL]
forall (f :: * -> *) (e :: * -> *) l.
ExtractF f e =>
e (f l) -> f (e l)
extractF JavaTerm [ModifierL]
mods) then
                              MJavaTerm [l]
l
                            else
                              MJavaTerm l -> MJavaTerm [l] -> MJavaTerm [l]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a [l] -> Cxt h f a [l]
ConsF' MJavaTerm l
x MJavaTerm [l]
l

  trans t :: MemberDecl JavaTerm l
t = MemberDecl JavaTerm l -> MJavaTerm l
forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: MJavaSig, f :-<: JavaSig) =>
f JavaTerm l -> MJavaTerm l
transDefault MemberDecl JavaTerm l
t

instance {-# OVERLAPPING #-} Trans F.MethodBody where
  trans :: MethodBody JavaTerm l -> MJavaTerm l
trans = String -> MethodBody JavaTerm l -> MJavaTerm l
forall a. HasCallStack => String -> a
error "MethodBody found not within MethodDecl"

untranslate :: MJavaTerm l -> F.JavaTerm l
untranslate :: MJavaTerm l -> JavaTerm l
untranslate = Sum MJavaSig (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
forall (f :: (* -> *) -> * -> *) l.
Untrans f =>
f (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
untrans (Sum MJavaSig (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l)
-> (MJavaTerm l
    -> Sum MJavaSig (Cxt NoHole (Sum MJavaSig) (K ())) l)
-> MJavaTerm l
-> JavaTerm l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MJavaTerm l -> Sum MJavaSig (Cxt NoHole (Sum MJavaSig) (K ())) l
forall (f :: (* -> *) -> * -> *) t. HFix f t -> f (HFix f) t
unTerm

class Untrans f where
  untrans :: f MJavaTerm l -> F.JavaTerm l

instance {-# OVERLAPPING #-} (All Untrans fs) => Untrans (Sum fs) where
  untrans :: Sum fs (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
untrans = Proxy Untrans
-> (forall (f :: (* -> *) -> * -> *).
    Untrans f =>
    f (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l)
-> Sum fs (Cxt NoHole (Sum MJavaSig) (K ())) l
-> JavaTerm l
forall (cxt :: ((* -> *) -> * -> *) -> Constraint)
       (fs :: [(* -> *) -> * -> *]) (a :: * -> *) e b.
All cxt fs =>
Proxy cxt
-> (forall (f :: (* -> *) -> * -> *). cxt f => f a e -> b)
-> Sum fs a e
-> b
caseCxt (Proxy Untrans
forall k (t :: k). Proxy t
Proxy @Untrans) forall (f :: (* -> *) -> * -> *).
Untrans f =>
f (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
forall (f :: (* -> *) -> * -> *) l.
Untrans f =>
f (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
untrans

untransDefault :: (HFunctor f, f :-<: F.JavaSig) => f MJavaTerm l -> F.JavaTerm l
untransDefault :: f (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
untransDefault = f JavaTerm l -> JavaTerm l
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (f JavaTerm l -> JavaTerm l)
-> (f (Cxt NoHole (Sum MJavaSig) (K ())) l -> f JavaTerm l)
-> f (Cxt NoHole (Sum MJavaSig) (K ())) l
-> JavaTerm l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm)
-> f (Cxt NoHole (Sum MJavaSig) (K ())) :-> f JavaTerm
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate

instance {-# OVERLAPPABLE #-} (HFunctor f, f :-<: F.JavaSig) => Untrans f where
  untrans :: f (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
untrans = f (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: JavaSig) =>
f (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
untransDefault

untransIdent :: MJavaTerm IdentL -> F.JavaTerm F.IdentL
untransIdent :: MJavaTerm IdentL -> JavaTerm IdentL
untransIdent (Ident' s :: String
s) = String -> JavaTerm IdentL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(Ident :-<: fs, InjF fs IdentL j) =>
String -> CxtS h fs a j
F.iIdent String
s

instance {-# OVERLAPPING #-} Untrans IdentIsIdent where
  untrans :: IdentIsIdent (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
untrans (IdentIsIdent n :: MJavaTerm IdentL
n) = MJavaTerm IdentL -> JavaTerm IdentL
untransIdent MJavaTerm IdentL
n

combineVarDeclId :: Int -> MJavaTerm IdentL -> F.JavaTerm F.VarDeclIdL
combineVarDeclId :: Int -> MJavaTerm IdentL -> JavaTerm VarDeclIdL
combineVarDeclId 0 id :: MJavaTerm IdentL
id = JavaTerm IdentL -> JavaTerm VarDeclIdL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(VarDeclId :-<: fs, InjF fs VarDeclIdL j) =>
CxtS h fs a IdentL -> CxtS h fs a j
F.iVarId (JavaTerm IdentL -> JavaTerm VarDeclIdL)
-> JavaTerm IdentL -> JavaTerm VarDeclIdL
forall a b. (a -> b) -> a -> b
$ MJavaTerm IdentL -> JavaTerm IdentL
untransIdent MJavaTerm IdentL
id
combineVarDeclId n :: Int
n id :: MJavaTerm IdentL
id = JavaTerm VarDeclIdL -> JavaTerm VarDeclIdL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(VarDeclId :-<: fs, InjF fs VarDeclIdL j) =>
CxtS h fs a VarDeclIdL -> CxtS h fs a j
F.iVarDeclArray (Int -> MJavaTerm IdentL -> JavaTerm VarDeclIdL
combineVarDeclId (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) MJavaTerm IdentL
id)

untransSingleDecl :: MJavaTerm SingleLocalVarDeclL -> F.JavaTerm F.VarDeclL
untransSingleDecl :: MJavaTerm SingleLocalVarDeclL -> JavaTerm VarDeclL
untransSingleDecl (SingleLocalVarDecl' attrs :: CxtS NoHole MJavaSig (K ()) LocalVarDeclAttrsL
attrs id :: CxtS NoHole MJavaSig (K ()) VarDeclBinderL
id optInit :: CxtS NoHole MJavaSig (K ()) OptLocalVarInitL
optInit) = JavaTerm VarDeclIdL
-> Cxt NoHole (Sum JavaSig) (K ()) (Maybe VarInitL)
-> JavaTerm VarDeclL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(VarDecl :-<: fs, InjF fs VarDeclL j) =>
CxtS h fs a VarDeclIdL
-> CxtS h fs a (Maybe VarInitL) -> CxtS h fs a j
F.iVarDecl JavaTerm VarDeclIdL
vid Cxt NoHole (Sum JavaSig) (K ()) (Maybe VarInitL)
vinit
  where
    (CxtS NoHole MJavaSig (K ()) LocalVarDeclAttrsL
-> Maybe
     (ArrayDimVarDeclAttrs
        (Cxt NoHole (Sum MJavaSig) (K ())) LocalVarDeclAttrsL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (ArrayDimVarDeclAttrs dim)) = CxtS NoHole MJavaSig (K ()) LocalVarDeclAttrsL
attrs
    vid :: JavaTerm VarDeclIdL
vid = Int -> MJavaTerm IdentL -> JavaTerm VarDeclIdL
combineVarDeclId Int
dim (MJavaTerm IdentL -> JavaTerm VarDeclIdL)
-> MJavaTerm IdentL -> JavaTerm VarDeclIdL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MJavaSig (K ()) VarDeclBinderL -> MJavaTerm IdentL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF CxtS NoHole MJavaSig (K ()) VarDeclBinderL
id

    vinit :: F.JavaTerm (Maybe F.VarInitL)
    vinit :: Cxt NoHole (Sum JavaSig) (K ()) (Maybe VarInitL)
vinit = case CxtS NoHole MJavaSig (K ()) OptLocalVarInitL
optInit of
      JustLocalVarInit' e :: CxtS NoHole MJavaSig (K ()) LocalVarInitL
e -> Cxt NoHole (Sum JavaSig) (K ()) VarInitL
-> Cxt NoHole (Sum JavaSig) (K ()) (Maybe VarInitL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a (Maybe l)
Just' (Cxt NoHole (Sum JavaSig) (K ()) VarInitL
 -> Cxt NoHole (Sum JavaSig) (K ()) (Maybe VarInitL))
-> Cxt NoHole (Sum JavaSig) (K ()) VarInitL
-> Cxt NoHole (Sum JavaSig) (K ()) (Maybe VarInitL)
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MJavaSig (K ()) VarInitL
-> Cxt NoHole (Sum JavaSig) (K ()) VarInitL
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate (CxtS NoHole MJavaSig (K ()) VarInitL
 -> Cxt NoHole (Sum JavaSig) (K ()) VarInitL)
-> CxtS NoHole MJavaSig (K ()) VarInitL
-> Cxt NoHole (Sum JavaSig) (K ()) VarInitL
forall a b. (a -> b) -> a -> b
$ Maybe (CxtS NoHole MJavaSig (K ()) VarInitL)
-> CxtS NoHole MJavaSig (K ()) VarInitL
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (CxtS NoHole MJavaSig (K ()) VarInitL)
 -> CxtS NoHole MJavaSig (K ()) VarInitL)
-> Maybe (CxtS NoHole MJavaSig (K ()) VarInitL)
-> CxtS NoHole MJavaSig (K ()) VarInitL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MJavaSig (K ()) LocalVarInitL
-> Maybe (CxtS NoHole MJavaSig (K ()) VarInitL)
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> Maybe (CxtS h fs a l)
projF (CxtS NoHole MJavaSig (K ()) LocalVarInitL
e :: MJavaTerm LocalVarInitL)
      NoLocalVarInit'     -> Cxt NoHole (Sum JavaSig) (K ()) (Maybe VarInitL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a (Maybe l)
Nothing'
    

instance {-# OVERLAPPING #-} Untrans MultiLocalVarDeclIsBlockStmt where
  untrans :: MultiLocalVarDeclIsBlockStmt (Cxt NoHole (Sum MJavaSig) (K ())) l
-> JavaTerm l
untrans (MultiLocalVarDeclIsBlockStmt (MultiLocalVarDecl' attrs :: CxtS NoHole MJavaSig (K ()) MultiLocalVarDeclCommonAttrsL
attrs decls :: CxtS NoHole MJavaSig (K ()) [SingleLocalVarDeclL]
decls)) = JavaTerm [ModifierL]
-> JavaTerm TypeL -> JavaTerm [VarDeclL] -> JavaTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(BlockStmt :-<: fs, InjF fs BlockStmtL j) =>
CxtS h fs a [ModifierL]
-> CxtS h fs a TypeL -> CxtS h fs a [VarDeclL] -> CxtS h fs a j
F.iLocalVars (CxtS NoHole MJavaSig (K ()) [ModifierL] -> JavaTerm [ModifierL]
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) [ModifierL]
mods) (CxtS NoHole MJavaSig (K ()) TypeL -> JavaTerm TypeL
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) TypeL
typ) (JavaTerm [VarDeclL] -> JavaTerm l)
-> JavaTerm [VarDeclL] -> JavaTerm l
forall a b. (a -> b) -> a -> b
$ (MJavaTerm SingleLocalVarDeclL -> JavaTerm VarDeclL)
-> CxtS NoHole MJavaSig (K ()) [SingleLocalVarDeclL]
-> JavaTerm [VarDeclL]
forall (f :: * -> *) (h :: * -> *) (g :: * -> *) b a.
(InsertF f h, ExtractF f g, Functor f, Typeable b) =>
(g a -> h b) -> g (f a) -> h (f b)
mapF MJavaTerm SingleLocalVarDeclL -> JavaTerm VarDeclL
untransSingleDecl CxtS NoHole MJavaSig (K ()) [SingleLocalVarDeclL]
decls
    where
      (mods :: CxtS NoHole MJavaSig (K ()) [ModifierL]
mods, typ :: CxtS NoHole MJavaSig (K ()) TypeL
typ) = CxtS NoHole MJavaSig (K ()) ([ModifierL], TypeL)
-> (CxtS NoHole MJavaSig (K ()) [ModifierL],
    CxtS NoHole MJavaSig (K ()) TypeL)
forall (f :: * -> * -> *) (e :: * -> *) l l'.
ExtractF2 f e =>
e (f l l') -> f (e l) (e l')
extractF2 (CxtS NoHole MJavaSig (K ()) ([ModifierL], TypeL)
 -> (CxtS NoHole MJavaSig (K ()) [ModifierL],
     CxtS NoHole MJavaSig (K ()) TypeL))
-> CxtS NoHole MJavaSig (K ()) ([ModifierL], TypeL)
-> (CxtS NoHole MJavaSig (K ()) [ModifierL],
    CxtS NoHole MJavaSig (K ()) TypeL)
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MJavaSig (K ()) MultiLocalVarDeclCommonAttrsL
-> CxtS NoHole MJavaSig (K ()) ([ModifierL], TypeL)
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF CxtS NoHole MJavaSig (K ()) MultiLocalVarDeclCommonAttrsL
attrs

untransOp :: MJavaTerm AssignOpL -> F.JavaTerm F.AssignOpL
untransOp :: MJavaTerm AssignOpL -> JavaTerm AssignOpL
untransOp AssignOpEquals' = JavaTerm AssignOpL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(AssignOp :-<: fs, InjF fs AssignOpL j) =>
CxtS h fs a j
F.iEqualA
untransOp x :: MJavaTerm AssignOpL
x               = CxtS NoHole MJavaSig (K ()) AssignOpL -> JavaTerm AssignOpL
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate (CxtS NoHole MJavaSig (K ()) AssignOpL -> JavaTerm AssignOpL)
-> CxtS NoHole MJavaSig (K ()) AssignOpL -> JavaTerm AssignOpL
forall a b. (a -> b) -> a -> b
$ MJavaTerm AssignOpL -> CxtS NoHole MJavaSig (K ()) AssignOpL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF MJavaTerm AssignOpL
x

instance {-# OVERLAPPING #-} Untrans AssignIsExp where
  untrans :: AssignIsExp (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
untrans (AssignIsExp (Assign' lhs :: CxtS NoHole MJavaSig (K ()) LhsL
lhs op :: MJavaTerm AssignOpL
op rhs :: CxtS NoHole MJavaSig (K ()) RhsL
rhs)) = JavaTerm LhsL -> JavaTerm AssignOpL -> JavaTerm ExpL -> JavaTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(Exp :-<: fs, InjF fs ExpL j) =>
CxtS h fs a LhsL
-> CxtS h fs a AssignOpL -> CxtS h fs a ExpL -> CxtS h fs a j
F.iAssign (CxtS NoHole MJavaSig (K ()) LhsL -> JavaTerm LhsL
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate (CxtS NoHole MJavaSig (K ()) LhsL -> JavaTerm LhsL)
-> CxtS NoHole MJavaSig (K ()) LhsL -> JavaTerm LhsL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MJavaSig (K ()) LhsL
-> CxtS NoHole MJavaSig (K ()) LhsL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF CxtS NoHole MJavaSig (K ()) LhsL
lhs) (MJavaTerm AssignOpL -> JavaTerm AssignOpL
untransOp MJavaTerm AssignOpL
op) (CxtS NoHole MJavaSig (K ()) ExpL -> JavaTerm ExpL
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate (CxtS NoHole MJavaSig (K ()) ExpL -> JavaTerm ExpL)
-> CxtS NoHole MJavaSig (K ()) ExpL -> JavaTerm ExpL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MJavaSig (K ()) RhsL
-> CxtS NoHole MJavaSig (K ()) ExpL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF CxtS NoHole MJavaSig (K ()) RhsL
rhs)

untransBlock :: MJavaTerm BlockL -> F.JavaTerm F.BlockL
untransBlock :: MJavaTerm BlockL -> JavaTerm BlockL
untransBlock (Block' items :: CxtS NoHole MJavaSig (K ()) [BlockItemL]
items _) = Cxt NoHole (Sum JavaSig) (K ()) [BlockStmtL] -> JavaTerm BlockL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(Block :-<: fs, InjF fs BlockL j) =>
CxtS h fs a [BlockStmtL] -> CxtS h fs a j
F.iBlock (Cxt NoHole (Sum JavaSig) (K ()) [BlockStmtL] -> JavaTerm BlockL)
-> Cxt NoHole (Sum JavaSig) (K ()) [BlockStmtL] -> JavaTerm BlockL
forall a b. (a -> b) -> a -> b
$ (Cxt NoHole (Sum MJavaSig) (K ()) BlockItemL
 -> Cxt NoHole (Sum JavaSig) (K ()) BlockStmtL)
-> CxtS NoHole MJavaSig (K ()) [BlockItemL]
-> Cxt NoHole (Sum JavaSig) (K ()) [BlockStmtL]
forall (f :: * -> *) (h :: * -> *) (g :: * -> *) b a.
(InsertF f h, ExtractF f g, Functor f, Typeable b) =>
(g a -> h b) -> g (f a) -> h (f b)
mapF (CxtS NoHole MJavaSig (K ()) BlockStmtL
-> Cxt NoHole (Sum JavaSig) (K ()) BlockStmtL
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate(CxtS NoHole MJavaSig (K ()) BlockStmtL
 -> Cxt NoHole (Sum JavaSig) (K ()) BlockStmtL)
-> (Cxt NoHole (Sum MJavaSig) (K ()) BlockItemL
    -> CxtS NoHole MJavaSig (K ()) BlockStmtL)
-> Cxt NoHole (Sum MJavaSig) (K ()) BlockItemL
-> Cxt NoHole (Sum JavaSig) (K ()) BlockStmtL
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cxt NoHole (Sum MJavaSig) (K ()) BlockItemL
-> CxtS NoHole MJavaSig (K ()) BlockStmtL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF) CxtS NoHole MJavaSig (K ()) [BlockItemL]
items

instance {-# OVERLAPPING #-} Untrans BlockIsBlock where
  untrans :: BlockIsBlock (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
untrans (BlockIsBlock b :: MJavaTerm BlockL
b) = MJavaTerm BlockL -> JavaTerm BlockL
untransBlock MJavaTerm BlockL
b

instance {-# OVERLAPPING #-} Untrans FunctionCallIsMethodInvocation where
  untrans :: FunctionCallIsMethodInvocation (Cxt NoHole (Sum MJavaSig) (K ())) l
-> JavaTerm l
untrans (FunctionCallIsMethodInvocation (FunctionCall' (CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
-> Maybe
     (JavaTypeArgs
        (Cxt NoHole (Sum MJavaSig) (K ())) FunctionCallAttrsL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (JavaTypeArgs targs :: CxtS NoHole MJavaSig (K ()) [RefTypeL]
targs))
                                                         (FunctionIdent' n :: MJavaTerm IdentL
n)
                                                         (FunctionArgumentList' (ConsF' (ReceiverArg' rec :: CxtS NoHole MJavaSig (K ()) ReceiverL
rec) args :: CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
args)))) =
      case CxtS NoHole MJavaSig (K ()) ReceiverL
-> Maybe
     (JavaReceiver (Cxt NoHole (Sum MJavaSig) (K ())) ReceiverL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project CxtS NoHole MJavaSig (K ()) ReceiverL
rec of
        Just ImplicitReceiver -> case CxtS NoHole MJavaSig (K ()) [RefTypeL]
targs of
          NilF' -> JavaTerm NameL -> JavaTerm [ExpL] -> JavaTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(MethodInvocation :-<: fs, InjF fs MethodInvocationL j) =>
CxtS h fs a NameL -> CxtS h fs a [ExpL] -> CxtS h fs a j
F.iMethodCall (Cxt NoHole (Sum JavaSig) (K ()) [IdentL] -> JavaTerm NameL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(Name :-<: fs, InjF fs NameL j) =>
CxtS h fs a [IdentL] -> CxtS h fs a j
F.iName (Cxt NoHole (Sum JavaSig) (K ()) [IdentL] -> JavaTerm NameL)
-> Cxt NoHole (Sum JavaSig) (K ()) [IdentL] -> JavaTerm NameL
forall a b. (a -> b) -> a -> b
$ JavaTerm IdentL -> Cxt NoHole (Sum JavaSig) (K ()) [IdentL]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a [l]
SingletonF' JavaTerm IdentL
n') JavaTerm [ExpL]
args'
          _     -> String -> JavaTerm l
forall a. HasCallStack => String -> a
error "Illegal Java term constructed: type args passed to implicit receiver"
        Just (PrimaryReceiver e :: CxtS NoHole MJavaSig (K ()) ExpL
e)    -> JavaTerm ExpL
-> JavaTerm [RefTypeL]
-> JavaTerm IdentL
-> JavaTerm [ExpL]
-> JavaTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(MethodInvocation :-<: fs, InjF fs MethodInvocationL j) =>
CxtS h fs a ExpL
-> CxtS h fs a [RefTypeL]
-> CxtS h fs a IdentL
-> CxtS h fs a [ExpL]
-> CxtS h fs a j
F.iPrimaryMethodCall (CxtS NoHole MJavaSig (K ()) ExpL -> JavaTerm ExpL
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) ExpL
e) (CxtS NoHole MJavaSig (K ()) [RefTypeL] -> JavaTerm [RefTypeL]
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) [RefTypeL]
targs) JavaTerm IdentL
n' JavaTerm [ExpL]
args'
        Just SuperReceiver          -> JavaTerm [RefTypeL]
-> JavaTerm IdentL -> JavaTerm [ExpL] -> JavaTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(MethodInvocation :-<: fs, InjF fs MethodInvocationL j) =>
CxtS h fs a [RefTypeL]
-> CxtS h fs a IdentL -> CxtS h fs a [ExpL] -> CxtS h fs a j
F.iSuperMethodCall                   (CxtS NoHole MJavaSig (K ()) [RefTypeL] -> JavaTerm [RefTypeL]
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) [RefTypeL]
targs) JavaTerm IdentL
n' JavaTerm [ExpL]
args'
        Just (ClassSuperReceiver c :: CxtS NoHole MJavaSig (K ()) NameL
c) -> JavaTerm NameL
-> JavaTerm [RefTypeL]
-> JavaTerm IdentL
-> JavaTerm [ExpL]
-> JavaTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(MethodInvocation :-<: fs, InjF fs MethodInvocationL j) =>
CxtS h fs a NameL
-> CxtS h fs a [RefTypeL]
-> CxtS h fs a IdentL
-> CxtS h fs a [ExpL]
-> CxtS h fs a j
F.iClassMethodCall (CxtS NoHole MJavaSig (K ()) NameL -> JavaTerm NameL
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) NameL
c)   (CxtS NoHole MJavaSig (K ()) [RefTypeL] -> JavaTerm [RefTypeL]
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) [RefTypeL]
targs) JavaTerm IdentL
n' JavaTerm [ExpL]
args'
        Just (TypeReceiver c :: CxtS NoHole MJavaSig (K ()) NameL
c)       -> JavaTerm NameL
-> JavaTerm [RefTypeL]
-> JavaTerm IdentL
-> JavaTerm [ExpL]
-> JavaTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(MethodInvocation :-<: fs, InjF fs MethodInvocationL j) =>
CxtS h fs a NameL
-> CxtS h fs a [RefTypeL]
-> CxtS h fs a IdentL
-> CxtS h fs a [ExpL]
-> CxtS h fs a j
F.iTypeMethodCall  (CxtS NoHole MJavaSig (K ()) NameL -> JavaTerm NameL
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) NameL
c)   (CxtS NoHole MJavaSig (K ()) [RefTypeL] -> JavaTerm [RefTypeL]
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) [RefTypeL]
targs) JavaTerm IdentL
n' JavaTerm [ExpL]
args'
    where
      n' :: JavaTerm IdentL
n' = MJavaTerm IdentL -> JavaTerm IdentL
untransIdent MJavaTerm IdentL
n
      args' :: JavaTerm [ExpL]
args' = (Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
 -> JavaTerm ExpL)
-> CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
-> JavaTerm [ExpL]
forall (f :: * -> *) (h :: * -> *) (g :: * -> *) b a.
(InsertF f h, ExtractF f g, Functor f, Typeable b) =>
(g a -> h b) -> g (f a) -> h (f b)
mapF (CxtS NoHole MJavaSig (K ()) ExpL -> JavaTerm ExpL
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate(CxtS NoHole MJavaSig (K ()) ExpL -> JavaTerm ExpL)
-> (Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
    -> CxtS NoHole MJavaSig (K ()) ExpL)
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
-> JavaTerm ExpL
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
-> CxtS NoHole MJavaSig (K ()) ExpL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF) CxtS NoHole MJavaSig (K ()) [FunctionArgumentL]
args

untransParamDecl :: MJavaTerm FunctionParameterDeclL -> F.JavaTerm F.FormalParamL
untransParamDecl :: MJavaTerm FunctionParameterDeclL -> JavaTerm FormalParamL
untransParamDecl (MJavaTerm FunctionParameterDeclL
-> Maybe (CxtS NoHole MJavaSig (K ()) JavaVarargsParamL)
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> Maybe (CxtS h fs a l)
projF -> Just (JavaVarargsParam'               (JavaParamAttrs' mods :: CxtS NoHole MJavaSig (K ()) [ModifierL]
mods tp :: CxtS NoHole MJavaSig (K ()) TypeL
tp dim :: Int
dim) n :: MJavaTerm IdentL
n)) = JavaTerm [ModifierL]
-> JavaTerm TypeL
-> Bool
-> JavaTerm VarDeclIdL
-> JavaTerm FormalParamL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(FormalParam :-<: fs, InjF fs FormalParamL j) =>
CxtS h fs a [ModifierL]
-> CxtS h fs a TypeL
-> Bool
-> CxtS h fs a VarDeclIdL
-> CxtS h fs a j
F.iFormalParam (CxtS NoHole MJavaSig (K ()) [ModifierL] -> JavaTerm [ModifierL]
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) [ModifierL]
mods) (CxtS NoHole MJavaSig (K ()) TypeL -> JavaTerm TypeL
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) TypeL
tp) Bool
True  (Int -> MJavaTerm IdentL -> JavaTerm VarDeclIdL
combineVarDeclId Int
dim MJavaTerm IdentL
n)
untransParamDecl (PositionalParameterDeclWithIdent' (CxtS NoHole MJavaSig (K ()) FunctionParameterDeclAttrsL
-> CxtS NoHole MJavaSig (K ()) JavaParamAttrsL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF -> JavaParamAttrs' mods :: CxtS NoHole MJavaSig (K ()) [ModifierL]
mods tp :: CxtS NoHole MJavaSig (K ()) TypeL
tp dim :: Int
dim) n :: MJavaTerm IdentL
n)  = JavaTerm [ModifierL]
-> JavaTerm TypeL
-> Bool
-> JavaTerm VarDeclIdL
-> JavaTerm FormalParamL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(FormalParam :-<: fs, InjF fs FormalParamL j) =>
CxtS h fs a [ModifierL]
-> CxtS h fs a TypeL
-> Bool
-> CxtS h fs a VarDeclIdL
-> CxtS h fs a j
F.iFormalParam (CxtS NoHole MJavaSig (K ()) [ModifierL] -> JavaTerm [ModifierL]
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) [ModifierL]
mods) (CxtS NoHole MJavaSig (K ()) TypeL -> JavaTerm TypeL
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) TypeL
tp) Bool
False (Int -> MJavaTerm IdentL -> JavaTerm VarDeclIdL
combineVarDeclId Int
dim MJavaTerm IdentL
n)

untransParam :: MJavaTerm FunctionParameterL -> F.JavaTerm F.FormalParamL
untransParam :: MJavaTerm FunctionParameterL -> JavaTerm FormalParamL
untransParam (MJavaTerm FunctionParameterL
-> Maybe (CxtS NoHole MJavaSig (K ()) JavaVarargsParamL)
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> Maybe (CxtS h fs a l)
projF -> Just (JavaVarargsParam'  (JavaParamAttrs' mods :: CxtS NoHole MJavaSig (K ()) [ModifierL]
mods tp :: CxtS NoHole MJavaSig (K ()) TypeL
tp dim :: Int
dim) n :: MJavaTerm IdentL
n)) = JavaTerm [ModifierL]
-> JavaTerm TypeL
-> Bool
-> JavaTerm VarDeclIdL
-> JavaTerm FormalParamL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(FormalParam :-<: fs, InjF fs FormalParamL j) =>
CxtS h fs a [ModifierL]
-> CxtS h fs a TypeL
-> Bool
-> CxtS h fs a VarDeclIdL
-> CxtS h fs a j
F.iFormalParam (CxtS NoHole MJavaSig (K ()) [ModifierL] -> JavaTerm [ModifierL]
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) [ModifierL]
mods) (CxtS NoHole MJavaSig (K ()) TypeL -> JavaTerm TypeL
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) TypeL
tp) Bool
True  (Int -> MJavaTerm IdentL -> JavaTerm VarDeclIdL
combineVarDeclId Int
dim MJavaTerm IdentL
n)
untransParam (PositionalParameter' (CxtS NoHole MJavaSig (K ()) ParameterAttrsL
-> CxtS NoHole MJavaSig (K ()) JavaParamAttrsL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF -> JavaParamAttrs' mods :: CxtS NoHole MJavaSig (K ()) [ModifierL]
mods tp :: CxtS NoHole MJavaSig (K ()) TypeL
tp dim :: Int
dim) n :: MJavaTerm IdentL
n)  = JavaTerm [ModifierL]
-> JavaTerm TypeL
-> Bool
-> JavaTerm VarDeclIdL
-> JavaTerm FormalParamL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(FormalParam :-<: fs, InjF fs FormalParamL j) =>
CxtS h fs a [ModifierL]
-> CxtS h fs a TypeL
-> Bool
-> CxtS h fs a VarDeclIdL
-> CxtS h fs a j
F.iFormalParam (CxtS NoHole MJavaSig (K ()) [ModifierL] -> JavaTerm [ModifierL]
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) [ModifierL]
mods) (CxtS NoHole MJavaSig (K ()) TypeL -> JavaTerm TypeL
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) TypeL
tp) Bool
False (Int -> MJavaTerm IdentL -> JavaTerm VarDeclIdL
combineVarDeclId Int
dim MJavaTerm IdentL
n)


instance {-# OVERLAPPING #-} Untrans FunctionDeclIsMemberDecl where
  untrans :: FunctionDeclIsMemberDecl (Cxt NoHole (Sum MJavaSig) (K ())) l
-> JavaTerm l
untrans (FunctionDeclIsMemberDecl (FunctionDecl' (CxtS NoHole MJavaSig (K ()) FunctionDeclAttrsL
-> Maybe
     (JavaMethodDeclAttrsIsFunctionDeclAttrs
        (Cxt NoHole (Sum MJavaSig) (K ())) FunctionDeclAttrsL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (JavaMethodDeclAttrsIsFunctionDeclAttrs (JavaMethodDeclAttrs' mods :: CxtS NoHole MJavaSig (K ()) [ModifierL]
mods tparams :: CxtS NoHole MJavaSig (K ()) [TypeParamL]
tparams tp :: CxtS NoHole MJavaSig (K ()) (Maybe TypeL)
tp ex :: CxtS NoHole MJavaSig (K ()) [RefTypeL]
ex)))
                                                   n :: MJavaTerm IdentL
n
                                                   params :: CxtS NoHole MJavaSig (K ()) [FunctionParameterDeclL]
params))
           = JavaTerm [ModifierL]
-> JavaTerm [TypeParamL]
-> JavaTerm (Maybe TypeL)
-> JavaTerm IdentL
-> JavaTerm [FormalParamL]
-> JavaTerm [RefTypeL]
-> CxtS NoHole JavaSig (K ()) (Maybe ExpL)
-> JavaTerm MethodBodyL
-> JavaTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(MemberDecl :-<: fs, InjF fs MemberDeclL j) =>
CxtS h fs a [ModifierL]
-> CxtS h fs a [TypeParamL]
-> CxtS h fs a (Maybe TypeL)
-> CxtS h fs a IdentL
-> CxtS h fs a [FormalParamL]
-> CxtS h fs a [RefTypeL]
-> CxtS h fs a (Maybe ExpL)
-> CxtS h fs a MethodBodyL
-> CxtS h fs a j
F.iMethodDecl (CxtS NoHole MJavaSig (K ()) [ModifierL] -> JavaTerm [ModifierL]
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) [ModifierL]
mods)
                           (CxtS NoHole MJavaSig (K ()) [TypeParamL] -> JavaTerm [TypeParamL]
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) [TypeParamL]
tparams)
                           (CxtS NoHole MJavaSig (K ()) (Maybe TypeL) -> JavaTerm (Maybe TypeL)
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) (Maybe TypeL)
tp)
                           (MJavaTerm IdentL -> JavaTerm IdentL
untransIdent MJavaTerm IdentL
n)
                           ([JavaTerm FormalParamL] -> JavaTerm [FormalParamL]
forall (f :: * -> *) (e :: * -> *) l.
(InsertF f e, Typeable l) =>
f (e l) -> e (f l)
insertF ([JavaTerm FormalParamL] -> JavaTerm [FormalParamL])
-> [JavaTerm FormalParamL] -> JavaTerm [FormalParamL]
forall a b. (a -> b) -> a -> b
$ (MJavaTerm FunctionParameterDeclL -> JavaTerm FormalParamL)
-> [MJavaTerm FunctionParameterDeclL] -> [JavaTerm FormalParamL]
forall a b. (a -> b) -> [a] -> [b]
map MJavaTerm FunctionParameterDeclL -> JavaTerm FormalParamL
untransParamDecl ((MJavaTerm FunctionParameterDeclL -> Bool)
-> [MJavaTerm FunctionParameterDeclL]
-> [MJavaTerm FunctionParameterDeclL]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (MJavaTerm FunctionParameterDeclL
-> MJavaTerm FunctionParameterDeclL -> Bool
forall a. Eq a => a -> a -> Bool
== MJavaTerm FunctionParameterDeclL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(SelfParameterDecl :-<: fs, All HFunctor fs) =>
CxtS h fs a FunctionParameterDeclL
SelfParameterDecl') ([MJavaTerm FunctionParameterDeclL]
 -> [MJavaTerm FunctionParameterDeclL])
-> [MJavaTerm FunctionParameterDeclL]
-> [MJavaTerm FunctionParameterDeclL]
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MJavaSig (K ()) [FunctionParameterDeclL]
-> [MJavaTerm FunctionParameterDeclL]
forall (f :: * -> *) (e :: * -> *) l.
ExtractF f e =>
e (f l) -> f (e l)
extractF CxtS NoHole MJavaSig (K ()) [FunctionParameterDeclL]
params))
                           (CxtS NoHole MJavaSig (K ()) [RefTypeL] -> JavaTerm [RefTypeL]
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) [RefTypeL]
ex)
                           CxtS NoHole JavaSig (K ()) (Maybe ExpL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a (Maybe l)
Nothing'
                           (Cxt NoHole (Sum JavaSig) (K ()) (Maybe BlockL)
-> JavaTerm MethodBodyL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(MethodBody :-<: fs, InjF fs MethodBodyL j) =>
CxtS h fs a (Maybe BlockL) -> CxtS h fs a j
F.iMethodBody Cxt NoHole (Sum JavaSig) (K ()) (Maybe BlockL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a (Maybe l)
Nothing')

instance {-# OVERLAPPING #-} Untrans FunctionDefIsMemberDecl where
  untrans :: FunctionDefIsMemberDecl (Cxt NoHole (Sum MJavaSig) (K ())) l
-> JavaTerm l
untrans (FunctionDefIsMemberDecl (FunctionDef' (CxtS NoHole MJavaSig (K ()) FunctionDefAttrsL
-> Maybe
     (JavaMethodDeclAttrsIsFunctionDefAttrs
        (Cxt NoHole (Sum MJavaSig) (K ())) FunctionDefAttrsL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (JavaMethodDeclAttrsIsFunctionDefAttrs (JavaMethodDeclAttrs' mods :: CxtS NoHole MJavaSig (K ()) [ModifierL]
mods tparams :: CxtS NoHole MJavaSig (K ()) [TypeParamL]
tparams tp :: CxtS NoHole MJavaSig (K ()) (Maybe TypeL)
tp ex :: CxtS NoHole MJavaSig (K ()) [RefTypeL]
ex)))
                                                  n :: MJavaTerm IdentL
n
                                                  params :: CxtS NoHole MJavaSig (K ()) [FunctionParameterL]
params
                                                  body :: CxtS NoHole MJavaSig (K ()) FunctionBodyL
body))
           = JavaTerm [ModifierL]
-> JavaTerm [TypeParamL]
-> JavaTerm (Maybe TypeL)
-> JavaTerm IdentL
-> JavaTerm [FormalParamL]
-> JavaTerm [RefTypeL]
-> CxtS NoHole JavaSig (K ()) (Maybe ExpL)
-> JavaTerm MethodBodyL
-> JavaTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(MemberDecl :-<: fs, InjF fs MemberDeclL j) =>
CxtS h fs a [ModifierL]
-> CxtS h fs a [TypeParamL]
-> CxtS h fs a (Maybe TypeL)
-> CxtS h fs a IdentL
-> CxtS h fs a [FormalParamL]
-> CxtS h fs a [RefTypeL]
-> CxtS h fs a (Maybe ExpL)
-> CxtS h fs a MethodBodyL
-> CxtS h fs a j
F.iMethodDecl (CxtS NoHole MJavaSig (K ()) [ModifierL] -> JavaTerm [ModifierL]
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) [ModifierL]
mods)
                           (CxtS NoHole MJavaSig (K ()) [TypeParamL] -> JavaTerm [TypeParamL]
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) [TypeParamL]
tparams)
                           (CxtS NoHole MJavaSig (K ()) (Maybe TypeL) -> JavaTerm (Maybe TypeL)
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) (Maybe TypeL)
tp)
                           (MJavaTerm IdentL -> JavaTerm IdentL
untransIdent MJavaTerm IdentL
n)
                           ([JavaTerm FormalParamL] -> JavaTerm [FormalParamL]
forall (f :: * -> *) (e :: * -> *) l.
(InsertF f e, Typeable l) =>
f (e l) -> e (f l)
insertF ([JavaTerm FormalParamL] -> JavaTerm [FormalParamL])
-> [JavaTerm FormalParamL] -> JavaTerm [FormalParamL]
forall a b. (a -> b) -> a -> b
$ (MJavaTerm FunctionParameterL -> JavaTerm FormalParamL)
-> [MJavaTerm FunctionParameterL] -> [JavaTerm FormalParamL]
forall a b. (a -> b) -> [a] -> [b]
map MJavaTerm FunctionParameterL -> JavaTerm FormalParamL
untransParam ((MJavaTerm FunctionParameterL -> Bool)
-> [MJavaTerm FunctionParameterL] -> [MJavaTerm FunctionParameterL]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (MJavaTerm FunctionParameterL
-> MJavaTerm FunctionParameterL -> Bool
forall a. Eq a => a -> a -> Bool
== MJavaTerm FunctionParameterL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(SelfParameter :-<: fs, All HFunctor fs) =>
CxtS h fs a FunctionParameterL
SelfParameter') ([MJavaTerm FunctionParameterL] -> [MJavaTerm FunctionParameterL])
-> [MJavaTerm FunctionParameterL] -> [MJavaTerm FunctionParameterL]
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MJavaSig (K ()) [FunctionParameterL]
-> [MJavaTerm FunctionParameterL]
forall (f :: * -> *) (e :: * -> *) l.
ExtractF f e =>
e (f l) -> f (e l)
extractF CxtS NoHole MJavaSig (K ()) [FunctionParameterL]
params))
                           (CxtS NoHole MJavaSig (K ()) [RefTypeL] -> JavaTerm [RefTypeL]
Cxt NoHole (Sum MJavaSig) (K ()) :-> JavaTerm
untranslate CxtS NoHole MJavaSig (K ()) [RefTypeL]
ex)
                           CxtS NoHole JavaSig (K ()) (Maybe ExpL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a (Maybe l)
Nothing'
                           (Cxt NoHole (Sum JavaSig) (K ()) (Maybe BlockL)
-> JavaTerm MethodBodyL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(MethodBody :-<: fs, InjF fs MethodBodyL j) =>
CxtS h fs a (Maybe BlockL) -> CxtS h fs a j
F.iMethodBody (JavaTerm BlockL -> Cxt NoHole (Sum JavaSig) (K ()) (Maybe BlockL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a (Maybe l)
Just' (MJavaTerm BlockL -> JavaTerm BlockL
untransBlock (MJavaTerm BlockL -> JavaTerm BlockL)
-> MJavaTerm BlockL -> JavaTerm BlockL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MJavaSig (K ()) FunctionBodyL -> MJavaTerm BlockL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF CxtS NoHole MJavaSig (K ()) FunctionBodyL
body)))

untransError :: (HFunctor f, f :-<: MJavaSig) => f MJavaTerm l -> F.JavaTerm l
untransError :: f (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
untransError t :: f (Cxt NoHole (Sum MJavaSig) (K ())) l
t = String -> JavaTerm l
forall a. HasCallStack => String -> a
error (String -> JavaTerm l) -> String -> JavaTerm l
forall a b. (a -> b) -> a -> b
$ "Cannot untranslate root node: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (MJavaTerm l -> String
forall a. Show a => a -> String
show (MJavaTerm l -> String) -> MJavaTerm l -> String
forall a b. (a -> b) -> a -> b
$ (f (Cxt NoHole (Sum MJavaSig) (K ())) l -> MJavaTerm l
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject f (Cxt NoHole (Sum MJavaSig) (K ())) l
t :: MJavaTerm _))

do ipsNames <- sumToNames ''MJavaSig
   modNames <- sumToNames ''F.JavaSig
   let targTs = map ConT $ (ipsNames \\ modNames) \\ [ ''BlockIsBlock, ''AssignIsExp, ''MultiLocalVarDeclIsBlockStmt, ''IdentIsIdent
                                                     , ''FunctionCallIsMethodInvocation, ''FunctionDeclIsMemberDecl, ''FunctionDefIsMemberDecl]
   return $ makeDefaultInstances targTs ''Untrans 'untrans (VarE 'untransError)



#endif