{-# OPTIONS_HADDOCK hide #-}
{-# OPTIONS_GHC -freduction-depth=200 #-}

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

#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.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 :: forall l. JavaTerm l -> MJavaTerm l
translate = Sum JavaSig (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
forall l.
Sum JavaSig (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
forall (f :: Fragment) l.
Trans f =>
f (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
trans (Sum JavaSig (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l)
-> (JavaTerm l -> Sum JavaSig (Cxt NoHole (Sum JavaSig) (K ())) l)
-> JavaTerm l
-> MJavaTerm l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JavaTerm l -> Sum JavaSig (Cxt NoHole (Sum JavaSig) (K ())) l
forall (f :: Fragment) t. HFix f t -> f (HFix f) t
unTerm

translate' :: (InjF MJavaSig l l') => F.JavaTerm l -> MJavaTerm l'
translate' :: forall l l'. InjF MJavaSig l l' => JavaTerm l -> MJavaTerm l'
translate' = CxtS NoHole MJavaSig (K ()) l -> CxtS NoHole MJavaSig (K ()) l'
forall (fs :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *). CxtS h MJavaSig a l -> CxtS h MJavaSig a l'
injF (CxtS NoHole MJavaSig (K ()) l -> CxtS NoHole MJavaSig (K ()) l')
-> (JavaTerm l -> CxtS NoHole MJavaSig (K ()) l)
-> JavaTerm l
-> CxtS NoHole MJavaSig (K ()) 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 :: forall l. Sum fs (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
trans = forall (cxt :: Fragment -> Constraint) (fs :: [Fragment])
       (a :: * -> *) e b.
All cxt fs =>
(forall (f :: Fragment). cxt f => f a e -> b) -> Sum fs a e -> b
caseCxt @Trans f (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
forall l. f (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
forall (f :: Fragment).
Trans f =>
f (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
forall (f :: Fragment) l.
Trans f =>
f (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
trans

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

instance {-# OVERLAPPABLE #-} (HFunctor f, f :-<: MJavaSig, f :-<: F.JavaSig) => Trans f where
  trans :: forall l. f (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
trans = f (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
forall (f :: Fragment) l.
(HFunctor f, f :-<: MJavaSig, f :-<: JavaSig) =>
f (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
transDefault

transIdent :: F.JavaTerm F.IdentL -> MJavaTerm IdentL
transIdent :: JavaTerm IdentL -> MJavaTerm IdentL
transIdent (JavaTerm IdentL
-> Maybe (Ident (Cxt NoHole (Sum JavaSig) (K ())) IdentL)
NatM
  Maybe
  (Cxt NoHole (Sum JavaSig) (K ()))
  (Ident (Cxt NoHole (Sum JavaSig) (K ())))
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.Ident String
s)) = String -> MJavaTerm IdentL
forall h (f :: Fragment) (a :: * -> *) j.
(Ident :<: f) =>
String -> Cxt h f a IdentL
Ident' String
s

-- Clone of transIdent because type-safe pattern match
instance Trans F.Ident where
  trans :: forall l. Ident (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
trans (F.Ident String
n) = String -> CxtS NoHole MJavaSig (K ()) l
forall h (fs :: [Fragment]) (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 (Cxt NoHole (Sum JavaSig) (K ())) VarDeclIdL)
NatM
  Maybe
  (Cxt NoHole (Sum JavaSig) (K ()))
  (VarDeclId (Cxt NoHole (Sum JavaSig) (K ())))
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.VarId JavaTerm IdentL
ident))      = (Int
0, JavaTerm IdentL -> MJavaTerm IdentL
transIdent JavaTerm IdentL
ident)
splitVarDeclId (JavaTerm VarDeclIdL
-> Maybe (VarDeclId (Cxt NoHole (Sum JavaSig) (K ())) VarDeclIdL)
NatM
  Maybe
  (Cxt NoHole (Sum JavaSig) (K ()))
  (VarDeclId (Cxt NoHole (Sum JavaSig) (K ())))
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.VarDeclArray JavaTerm VarDeclIdL
sub)) = (Int
dim Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, MJavaTerm IdentL
id)
  where
    (Int
dim, 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 (Cxt NoHole (Sum JavaSig) (K ())) VarDeclL)
NatM
  Maybe
  (Cxt NoHole (Sum JavaSig) (K ()))
  (VarDecl (Cxt NoHole (Sum JavaSig) (K ())))
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.VarDecl JavaTerm VarDeclIdL
vid Cxt NoHole (Sum JavaSig) (K ()) (Maybe VarInitL)
init)) = Cxt NoHole (Sum MJavaSig) (K ()) LocalVarDeclAttrsL
-> Cxt NoHole (Sum MJavaSig) (K ()) VarDeclBinderL
-> Cxt NoHole (Sum MJavaSig) (K ()) OptLocalVarInitL
-> MJavaTerm SingleLocalVarDeclL
forall h (f :: Fragment) (a :: * -> *) j.
(SingleLocalVarDecl :<: f) =>
Cxt h f a LocalVarDeclAttrsL
-> Cxt h f a VarDeclBinderL
-> Cxt h f a OptLocalVarInitL
-> Cxt h f a SingleLocalVarDeclL
SingleLocalVarDecl' (Int -> Cxt NoHole (Sum MJavaSig) (K ()) LocalVarDeclAttrsL
forall h (fs :: [Fragment]) (a :: * -> *) j.
(ArrayDimVarDeclAttrs :-<: fs, InjF fs LocalVarDeclAttrsL j) =>
Int -> CxtS h fs a j
iArrayDimVarDeclAttrs Int
dim) (MJavaTerm IdentL -> Cxt NoHole (Sum MJavaSig) (K ()) VarDeclBinderL
forall (fs :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a IdentL -> CxtS h MJavaSig a VarDeclBinderL
injF MJavaTerm IdentL
id) Cxt NoHole (Sum MJavaSig) (K ()) OptLocalVarInitL
optInit
  where
    (Int
dim, MJavaTerm IdentL
id) = JavaTerm VarDeclIdL -> (Int, MJavaTerm IdentL)
splitVarDeclId JavaTerm VarDeclIdL
vid

    optInit :: MJavaTerm OptLocalVarInitL
    optInit :: Cxt NoHole (Sum MJavaSig) (K ()) OptLocalVarInitL
optInit = case Cxt NoHole (Sum JavaSig) (K ()) (Maybe VarInitL)
init of
      Just' Cxt NoHole (Sum JavaSig) (K ()) VarInitL
x  -> Cxt NoHole (Sum MJavaSig) (K ()) LocalVarInitL
-> Cxt NoHole (Sum MJavaSig) (K ()) OptLocalVarInitL
forall h (f :: Fragment) (a :: * -> *) j.
(OptLocalVarInit :<: f) =>
Cxt h f a LocalVarInitL -> Cxt h f a OptLocalVarInitL
JustLocalVarInit' (Cxt NoHole (Sum MJavaSig) (K ()) LocalVarInitL
 -> Cxt NoHole (Sum MJavaSig) (K ()) OptLocalVarInitL)
-> Cxt NoHole (Sum MJavaSig) (K ()) LocalVarInitL
-> Cxt NoHole (Sum MJavaSig) (K ()) OptLocalVarInitL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MJavaSig (K ()) VarInitL
-> Cxt NoHole (Sum MJavaSig) (K ()) LocalVarInitL
forall (fs :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a VarInitL -> CxtS h MJavaSig a LocalVarInitL
injF (CxtS NoHole MJavaSig (K ()) VarInitL
 -> Cxt NoHole (Sum MJavaSig) (K ()) LocalVarInitL)
-> CxtS NoHole MJavaSig (K ()) VarInitL
-> Cxt NoHole (Sum 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
      Cxt NoHole (Sum JavaSig) (K ()) (Maybe VarInitL)
Nothing' -> Cxt NoHole (Sum MJavaSig) (K ()) OptLocalVarInitL
forall h (f :: Fragment) (a :: * -> *) j.
(OptLocalVarInit :<: f) =>
Cxt h f a OptLocalVarInitL
NoLocalVarInit'
                                                                                                                   

instance {-# OVERLAPPING #-} Trans F.BlockStmt where
  trans :: forall l.
BlockStmt (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
trans t :: BlockStmt (Cxt NoHole (Sum JavaSig) (K ())) l
t@(F.BlockStmt JavaTerm StmtL
_)              = BlockStmt (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
forall (f :: Fragment) l.
(HFunctor f, f :-<: MJavaSig, f :-<: JavaSig) =>
f (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
transDefault BlockStmt (Cxt NoHole (Sum JavaSig) (K ())) l
t
  trans t :: BlockStmt (Cxt NoHole (Sum JavaSig) (K ())) l
t@(F.LocalClass JavaTerm ClassDeclL
_)             = BlockStmt (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
forall (f :: Fragment) l.
(HFunctor f, f :-<: MJavaSig, f :-<: JavaSig) =>
f (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
transDefault BlockStmt (Cxt NoHole (Sum JavaSig) (K ())) l
t
  trans t :: BlockStmt (Cxt NoHole (Sum JavaSig) (K ())) l
t@(F.LocalVars JavaTerm [ModifierL]
mods JavaTerm TypeL
typ JavaTerm [VarDeclL]
decls) = CxtS NoHole MJavaSig (K ()) MultiLocalVarDeclCommonAttrsL
-> CxtS NoHole MJavaSig (K ()) [SingleLocalVarDeclL] -> MJavaTerm l
forall h (fs :: [Fragment]) (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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a ([ModifierL], TypeL)
-> CxtS h MJavaSig a MultiLocalVarDeclCommonAttrsL
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 :: Fragment) 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 (Cxt NoHole (Sum JavaSig) (K ())) AssignOpL)
NatM
  Maybe
  (Cxt NoHole (Sum JavaSig) (K ()))
  (AssignOp (Cxt NoHole (Sum JavaSig) (K ())))
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> (Just AssignOp (Cxt NoHole (Sum JavaSig) (K ())) AssignOpL
F.EqualA)) = MJavaTerm AssignOpL
forall h (f :: Fragment) (a :: * -> *) j.
(AssignOpEquals :<: f) =>
Cxt h f a AssignOpL
AssignOpEquals'
transOp JavaTerm AssignOpL
x                            = CxtS NoHole MJavaSig (K ()) AssignOpL -> MJavaTerm AssignOpL
forall (fs :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a AssignOpL -> CxtS h MJavaSig a AssignOpL
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 :: forall l. Exp (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
trans t :: Exp (Cxt NoHole (Sum JavaSig) (K ())) l
t@(F.Assign JavaTerm LhsL
lhs JavaTerm AssignOpL
op JavaTerm ExpL
rhs) = CxtS NoHole MJavaSig (K ()) LhsL
-> MJavaTerm AssignOpL
-> CxtS NoHole MJavaSig (K ()) RhsL
-> CxtS NoHole MJavaSig (K ()) l
forall h (fs :: [Fragment]) (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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a LhsL -> CxtS h MJavaSig a LhsL
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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a ExpL -> CxtS h MJavaSig a RhsL
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 Exp (Cxt NoHole (Sum JavaSig) (K ())) l
t                       = Exp (Cxt NoHole (Sum JavaSig) (K ())) l
-> CxtS NoHole MJavaSig (K ()) l
forall (f :: Fragment) l.
(HFunctor f, f :-<: MJavaSig, f :-<: JavaSig) =>
f (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
transDefault Exp (Cxt NoHole (Sum JavaSig) (K ())) l
t

instance {-# OVERLAPPING #-} Trans F.MethodInvocation where
  trans :: forall l.
MethodInvocation (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
trans (F.MethodCall JavaTerm NameL
nam JavaTerm [ExpL]
args) = CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
-> CxtS NoHole MJavaSig (K ()) FunctionExpL
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
-> CxtS NoHole MJavaSig (K ()) l
forall h (fs :: [Fragment]) (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 :: [Fragment]) (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 :: Fragment) (a :: * -> *) l.
(ListF :<: f, Typeable l) =>
Cxt h f a [l]
riNilF)
                                                CxtS NoHole MJavaSig (K ()) FunctionExpL
f
                                                (Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall h (f :: Fragment) (a :: * -> *) j.
(FunctionArgumentList :<: f) =>
Cxt h f a [FunctionArgumentL] -> Cxt h f a FunctionArgumentsL
FunctionArgumentList' (Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
 -> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL)
-> Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall a b. (a -> b) -> a -> b
$ (JavaTerm ExpL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> JavaTerm [ExpL]
-> Cxt NoHole (Sum 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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a ExpL -> CxtS h MJavaSig a FunctionArgumentL
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 (Cxt NoHole (Sum JavaSig) (K ())) NameL)
NatM
  Maybe
  (Cxt NoHole (Sum JavaSig) (K ()))
  (Name (Cxt NoHole (Sum JavaSig) (K ())))
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.Name (SingletonF' JavaTerm IdentL
n))) -> MJavaTerm IdentL -> CxtS NoHole MJavaSig (K ()) FunctionExpL
forall (fs :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a IdentL -> CxtS h MJavaSig a FunctionExpL
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
            JavaTerm NameL
_                                          -> CxtS NoHole MJavaSig (K ()) NameL
-> CxtS NoHole MJavaSig (K ()) FunctionExpL
forall (fs :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a NameL -> CxtS h MJavaSig a FunctionExpL
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 JavaTerm ExpL
e JavaTerm [RefTypeL]
targs JavaTerm IdentL
n JavaTerm [ExpL]
args) = CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
-> CxtS NoHole MJavaSig (K ()) FunctionExpL
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
-> CxtS NoHole MJavaSig (K ()) l
forall h (fs :: [Fragment]) (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 :: [Fragment]) (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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a IdentL -> CxtS h MJavaSig a FunctionExpL
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)
                                                             (Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall h (f :: Fragment) (a :: * -> *) j.
(FunctionArgumentList :<: f) =>
Cxt h f a [FunctionArgumentL] -> Cxt h f a FunctionArgumentsL
FunctionArgumentList' (Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
 -> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL)
-> Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
-> Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
-> Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
forall (f :: Fragment) 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' (Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall h (f :: Fragment) (a :: * -> *) j.
(ReceiverArg :<: f) =>
Cxt h f a ReceiverL -> Cxt h f a FunctionArgumentL
ReceiverArg' (Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MJavaSig (K ()) ExpL
-> Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL
forall h (fs :: [Fragment]) (a :: * -> *) j.
(JavaReceiver :-<: fs, InjF fs ReceiverL j) =>
CxtS h fs a ExpL -> CxtS h fs a j
iPrimaryReceiver (CxtS NoHole MJavaSig (K ()) ExpL
 -> Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL)
-> CxtS NoHole MJavaSig (K ()) ExpL
-> Cxt NoHole (Sum 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]
-> Cxt NoHole (Sum 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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a ExpL -> CxtS h MJavaSig a FunctionArgumentL
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 JavaTerm [RefTypeL]
targs JavaTerm IdentL
n JavaTerm [ExpL]
args)     = CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
-> CxtS NoHole MJavaSig (K ()) FunctionExpL
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
-> CxtS NoHole MJavaSig (K ()) l
forall h (fs :: [Fragment]) (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 :: [Fragment]) (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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a IdentL -> CxtS h MJavaSig a FunctionExpL
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)
                                                             (Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall h (f :: Fragment) (a :: * -> *) j.
(FunctionArgumentList :<: f) =>
Cxt h f a [FunctionArgumentL] -> Cxt h f a FunctionArgumentsL
FunctionArgumentList' (Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
 -> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL)
-> Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
-> Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
-> Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
forall (f :: Fragment) 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' (Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall h (f :: Fragment) (a :: * -> *) j.
(ReceiverArg :<: f) =>
Cxt h f a ReceiverL -> Cxt h f a FunctionArgumentL
ReceiverArg' (Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL
forall h (fs :: [Fragment]) (a :: * -> *) j.
(JavaReceiver :-<: fs, InjF fs ReceiverL j) =>
CxtS h fs a j
iSuperReceiver)
                                                                                             ((JavaTerm ExpL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> JavaTerm [ExpL]
-> Cxt NoHole (Sum 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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a ExpL -> CxtS h MJavaSig a FunctionArgumentL
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 JavaTerm NameL
typ JavaTerm [RefTypeL]
targs JavaTerm IdentL
n JavaTerm [ExpL]
args) = CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
-> CxtS NoHole MJavaSig (K ()) FunctionExpL
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
-> CxtS NoHole MJavaSig (K ()) l
forall h (fs :: [Fragment]) (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 :: [Fragment]) (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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a IdentL -> CxtS h MJavaSig a FunctionExpL
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)
                                                             (Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall h (f :: Fragment) (a :: * -> *) j.
(FunctionArgumentList :<: f) =>
Cxt h f a [FunctionArgumentL] -> Cxt h f a FunctionArgumentsL
FunctionArgumentList' (Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
 -> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL)
-> Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
-> Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
-> Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
forall (f :: Fragment) 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' (Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall h (f :: Fragment) (a :: * -> *) j.
(ReceiverArg :<: f) =>
Cxt h f a ReceiverL -> Cxt h f a FunctionArgumentL
ReceiverArg' (Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MJavaSig (K ()) NameL
-> Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL
forall h (fs :: [Fragment]) (a :: * -> *) j.
(JavaReceiver :-<: fs, InjF fs ReceiverL j) =>
CxtS h fs a NameL -> CxtS h fs a j
iClassSuperReceiver (CxtS NoHole MJavaSig (K ()) NameL
 -> Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL)
-> CxtS NoHole MJavaSig (K ()) NameL
-> Cxt NoHole (Sum 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]
-> Cxt NoHole (Sum 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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a ExpL -> CxtS h MJavaSig a FunctionArgumentL
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  JavaTerm NameL
typ JavaTerm [RefTypeL]
targs JavaTerm IdentL
n JavaTerm [ExpL]
args) = CxtS NoHole MJavaSig (K ()) FunctionCallAttrsL
-> CxtS NoHole MJavaSig (K ()) FunctionExpL
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
-> CxtS NoHole MJavaSig (K ()) l
forall h (fs :: [Fragment]) (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 :: [Fragment]) (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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a IdentL -> CxtS h MJavaSig a FunctionExpL
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)
                                                             (Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall h (f :: Fragment) (a :: * -> *) j.
(FunctionArgumentList :<: f) =>
Cxt h f a [FunctionArgumentL] -> Cxt h f a FunctionArgumentsL
FunctionArgumentList' (Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
 -> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL)
-> Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
-> CxtS NoHole MJavaSig (K ()) FunctionArgumentsL
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
-> Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
-> Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
forall (f :: Fragment) 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' (Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall h (f :: Fragment) (a :: * -> *) j.
(ReceiverArg :<: f) =>
Cxt h f a ReceiverL -> Cxt h f a FunctionArgumentL
ReceiverArg' (Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL
 -> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL)
-> Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL
-> Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MJavaSig (K ()) NameL
-> Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL
forall h (fs :: [Fragment]) (a :: * -> *) j.
(JavaReceiver :-<: fs, InjF fs ReceiverL j) =>
CxtS h fs a NameL -> CxtS h fs a j
iTypeReceiver (CxtS NoHole MJavaSig (K ()) NameL
 -> Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL)
-> CxtS NoHole MJavaSig (K ()) NameL
-> Cxt NoHole (Sum 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]
-> Cxt NoHole (Sum 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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a ExpL -> CxtS h MJavaSig a FunctionArgumentL
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 (Cxt NoHole (Sum JavaSig) (K ())) BlockL)
NatM
  Maybe
  (Cxt NoHole (Sum JavaSig) (K ()))
  (Block (Cxt NoHole (Sum JavaSig) (K ())))
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.Block Cxt NoHole (Sum JavaSig) (K ()) [BlockStmtL]
stmts)) = Cxt NoHole (Sum MJavaSig) (K ()) [BlockItemL]
-> Cxt NoHole (Sum MJavaSig) (K ()) BlockEndL -> MJavaTerm BlockL
forall h (f :: Fragment) (a :: * -> *) j.
(Block :<: f) =>
Cxt h f a [BlockItemL] -> Cxt h f a BlockEndL -> Cxt h f a BlockL
Block' ((Cxt NoHole (Sum JavaSig) (K ()) BlockStmtL
 -> Cxt NoHole (Sum MJavaSig) (K ()) BlockItemL)
-> Cxt NoHole (Sum JavaSig) (K ()) [BlockStmtL]
-> Cxt NoHole (Sum 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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a BlockStmtL -> CxtS h MJavaSig a BlockItemL
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) Cxt NoHole (Sum MJavaSig) (K ()) BlockEndL
forall h (f :: Fragment) (a :: * -> *) j.
(EmptyBlockEnd :<: f) =>
Cxt h f a BlockEndL
EmptyBlockEnd'

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

transParamDecl :: F.JavaTerm F.FormalParamL -> MJavaTerm FunctionParameterDeclL
transParamDecl :: JavaTerm FormalParamL -> MJavaTerm FunctionParameterDeclL
transParamDecl (JavaTerm FormalParamL
-> Maybe
     (FormalParam (Cxt NoHole (Sum JavaSig) (K ())) FormalParamL)
NatM
  Maybe
  (Cxt NoHole (Sum JavaSig) (K ()))
  (FormalParam (Cxt NoHole (Sum JavaSig) (K ())))
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.FormalParam JavaTerm [ModifierL]
mods JavaTerm TypeL
tp Bool
isVarargs JavaTerm VarDeclIdL
vid)) =
    if Bool
isVarargs then
      CxtS NoHole MJavaSig (K ()) JavaParamAttrsL
-> MJavaTerm IdentL -> MJavaTerm FunctionParameterDeclL
forall h (fs :: [Fragment]) (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 :: [Fragment]) (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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a JavaParamAttrsL
-> CxtS h MJavaSig a FunctionParameterDeclAttrsL
injF CxtS NoHole MJavaSig (K ()) JavaParamAttrsL
attrs) MJavaTerm IdentL
n
  where
    (Int
dim, 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 :: [Fragment]) (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 (Cxt NoHole (Sum JavaSig) (K ())) FormalParamL)
NatM
  Maybe
  (Cxt NoHole (Sum JavaSig) (K ()))
  (FormalParam (Cxt NoHole (Sum JavaSig) (K ())))
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.FormalParam JavaTerm [ModifierL]
mods JavaTerm TypeL
tp Bool
isVarargs JavaTerm VarDeclIdL
vid)) =
    if Bool
isVarargs then
      CxtS NoHole MJavaSig (K ()) JavaParamAttrsL
-> MJavaTerm IdentL -> MJavaTerm FunctionParameterL
forall h (fs :: [Fragment]) (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 :: [Fragment]) (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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a JavaParamAttrsL
-> CxtS h MJavaSig a ParameterAttrsL
injF CxtS NoHole MJavaSig (K ()) JavaParamAttrsL
attrs) MJavaTerm IdentL
n
  where
    (Int
dim, 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 :: [Fragment]) (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 :: forall l.
MemberDecl (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
trans (F.MethodDecl JavaTerm [ModifierL]
mods JavaTerm [TypeParamL]
tparams JavaTerm (Maybe TypeL)
typ JavaTerm IdentL
n JavaTerm [FormalParamL]
params JavaTerm [RefTypeL]
ex Cxt NoHole (Sum JavaSig) (K ()) (Maybe ExpL)
Nothing' JavaTerm MethodBodyL
body) =
      case JavaTerm MethodBodyL
body of
        F.MethodBody' Cxt NoHole (Sum JavaSig) (K ()) (Maybe BlockL)
Nothing'  -> CxtS NoHole MJavaSig (K ()) FunctionDeclAttrsL
-> MJavaTerm IdentL
-> CxtS NoHole MJavaSig (K ()) [FunctionParameterDeclL]
-> MJavaTerm l
forall h (fs :: [Fragment]) (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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a JavaMethodDeclAttrsL
-> CxtS h MJavaSig a FunctionDeclAttrsL
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 h (f :: Fragment) (a :: * -> *) j.
(SelfParameterDecl :<: f) =>
Cxt h f 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)
        F.MethodBody' (Just' 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 :: [Fragment]) (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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a JavaMethodDeclAttrsL
-> CxtS h MJavaSig a FunctionDefAttrsL
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 h (f :: Fragment) (a :: * -> *) j.
(SelfParameter :<: f) =>
Cxt h f 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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MJavaSig a BlockL -> CxtS h MJavaSig a FunctionBodyL
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 :: [Fragment]) (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 :: forall l.
Typeable l =>
MJavaTerm l -> MJavaTerm [l] -> MJavaTerm [l]
addUnlessStatic MJavaTerm l
x MJavaTerm [l]
l = if CxtS NoHole JavaSig (K ()) ModifierL
-> [CxtS NoHole JavaSig (K ()) ModifierL] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem CxtS NoHole JavaSig (K ()) ModifierL
forall h (fs :: [Fragment]) (a :: * -> *) j.
(Modifier :-<: fs, InjF fs ModifierL j) =>
CxtS h fs a j
F.iStatic (JavaTerm [ModifierL] -> [CxtS NoHole JavaSig (K ()) ModifierL]
forall l.
Cxt NoHole (Sum JavaSig) (K ()) [l]
-> [Cxt NoHole (Sum JavaSig) (K ()) l]
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 :: Fragment) 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 MemberDecl (Cxt NoHole (Sum JavaSig) (K ())) l
t = MemberDecl (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
forall (f :: Fragment) l.
(HFunctor f, f :-<: MJavaSig, f :-<: JavaSig) =>
f (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
transDefault MemberDecl (Cxt NoHole (Sum JavaSig) (K ())) l
t

instance {-# OVERLAPPING #-} Trans F.MethodBody where
  trans :: forall l.
MethodBody (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
trans = String
-> MethodBody (Cxt NoHole (Sum JavaSig) (K ())) l -> MJavaTerm l
forall a. HasCallStack => String -> a
error String
"MethodBody found not within MethodDecl"

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

instance {-# OVERLAPPING #-} (All Untrans fs) => Untrans (Sum fs) where
  untrans :: forall l. Sum fs (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
untrans = forall (cxt :: Fragment -> Constraint) (fs :: [Fragment])
       (a :: * -> *) e b.
All cxt fs =>
(forall (f :: Fragment). cxt f => f a e -> b) -> Sum fs a e -> b
caseCxt @Untrans f (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
forall l. f (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
forall (f :: Fragment).
Untrans f =>
f (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
forall (f :: Fragment) l.
Untrans f =>
f (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
untrans
  
untransError :: (HFunctor f, f :-<: MJavaSig) => f MJavaTerm l -> F.JavaTerm l
untransError :: forall (f :: Fragment) l.
(HFunctor f, f :-<: MJavaSig) =>
f (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
untransError 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
$ String
"Cannot untranslate root node: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Cxt NoHole (Sum MJavaSig) (K ()) l -> String
forall a. Show a => a -> String
show (Cxt NoHole (Sum MJavaSig) (K ()) l -> String)
-> Cxt NoHole (Sum MJavaSig) (K ()) l -> String
forall a b. (a -> b) -> a -> b
$ f (Cxt NoHole (Sum MJavaSig) (K ())) l
-> Cxt NoHole (Sum MJavaSig) (K ()) l
f (Cxt NoHole (Sum MJavaSig) (K ()))
:-> Cxt NoHole (Sum MJavaSig) (K ())
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject f (Cxt NoHole (Sum MJavaSig) (K ())) l
t)

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)


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

instance {-# OVERLAPPABLE #-} (HFunctor f, f :-<: F.JavaSig) => Untrans f where
  untrans :: forall l. f (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
untrans = f (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
forall (f :: Fragment) 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' String
s) = String -> JavaTerm IdentL
forall h (fs :: [Fragment]) (a :: * -> *) j.
(Ident :-<: fs, InjF fs IdentL j) =>
String -> CxtS h fs a j
F.iIdent String
s

instance {-# OVERLAPPING #-} Untrans IdentIsIdent where
  untrans :: forall l.
IdentIsIdent (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
untrans (IdentIsIdent 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 Int
0 MJavaTerm IdentL
id = JavaTerm IdentL -> JavaTerm VarDeclIdL
forall h (fs :: [Fragment]) (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 Int
n MJavaTerm IdentL
id = JavaTerm VarDeclIdL -> JavaTerm VarDeclIdL
forall h (fs :: [Fragment]) (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
-Int
1) MJavaTerm IdentL
id)

untransSingleDecl :: MJavaTerm SingleLocalVarDeclL -> F.JavaTerm F.VarDeclL
untransSingleDecl :: MJavaTerm SingleLocalVarDeclL -> JavaTerm VarDeclL
untransSingleDecl (SingleLocalVarDecl' Cxt NoHole (Sum MJavaSig) (K ()) LocalVarDeclAttrsL
attrs Cxt NoHole (Sum MJavaSig) (K ()) VarDeclBinderL
id Cxt NoHole (Sum MJavaSig) (K ()) OptLocalVarInitL
optInit) = JavaTerm VarDeclIdL
-> Cxt NoHole (Sum JavaSig) (K ()) (Maybe VarInitL)
-> JavaTerm VarDeclL
forall h (fs :: [Fragment]) (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
    (Cxt NoHole (Sum MJavaSig) (K ()) LocalVarDeclAttrsL
-> Maybe
     (ArrayDimVarDeclAttrs
        (Cxt NoHole (Sum MJavaSig) (K ())) LocalVarDeclAttrsL)
NatM
  Maybe
  (Cxt NoHole (Sum MJavaSig) (K ()))
  (ArrayDimVarDeclAttrs (Cxt NoHole (Sum MJavaSig) (K ())))
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (ArrayDimVarDeclAttrs Int
dim)) = Cxt NoHole (Sum 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
$ Cxt NoHole (Sum MJavaSig) (K ()) VarDeclBinderL -> MJavaTerm IdentL
forall (fs :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF Cxt NoHole (Sum MJavaSig) (K ()) VarDeclBinderL
id

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

instance {-# OVERLAPPING #-} Untrans MultiLocalVarDeclIsBlockStmt where
  untrans :: forall l.
MultiLocalVarDeclIsBlockStmt (Cxt NoHole (Sum MJavaSig) (K ())) l
-> JavaTerm l
untrans (MultiLocalVarDeclIsBlockStmt (MultiLocalVarDecl' CxtS NoHole MJavaSig (K ()) MultiLocalVarDeclCommonAttrsL
attrs CxtS NoHole MJavaSig (K ()) [SingleLocalVarDeclL]
decls)) = JavaTerm [ModifierL]
-> JavaTerm TypeL
-> JavaTerm [VarDeclL]
-> CxtS NoHole JavaSig (K ()) l
forall h (fs :: [Fragment]) (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 ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) [ModifierL]
mods) (CxtS NoHole MJavaSig (K ()) TypeL -> JavaTerm TypeL
Cxt NoHole (Sum MJavaSig) (K ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) TypeL
typ) (JavaTerm [VarDeclL] -> CxtS NoHole JavaSig (K ()) l)
-> JavaTerm [VarDeclL] -> CxtS NoHole JavaSig (K ()) 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
      (CxtS NoHole MJavaSig (K ()) [ModifierL]
mods, CxtS NoHole MJavaSig (K ()) TypeL
typ) = CxtS NoHole MJavaSig (K ()) ([ModifierL], TypeL)
-> (CxtS NoHole MJavaSig (K ()) [ModifierL],
    CxtS NoHole MJavaSig (K ()) TypeL)
forall l l'.
Cxt NoHole (Sum MJavaSig) (K ()) (l, l')
-> (Cxt NoHole (Sum MJavaSig) (K ()) l,
    Cxt NoHole (Sum MJavaSig) (K ()) l')
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 :: [Fragment]) 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 MJavaTerm AssignOpL
AssignOpEquals' = JavaTerm AssignOpL
forall h (fs :: [Fragment]) (a :: * -> *) j.
(AssignOp :-<: fs, InjF fs AssignOpL j) =>
CxtS h fs a j
F.iEqualA
untransOp MJavaTerm AssignOpL
x               = CxtS NoHole MJavaSig (K ()) AssignOpL -> JavaTerm AssignOpL
Cxt NoHole (Sum MJavaSig) (K ())
:-> Cxt NoHole (Sum JavaSig) (K ())
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 :: [Fragment]) 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 :: forall l.
AssignIsExp (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
untrans (AssignIsExp (Assign' CxtS NoHole MJavaSig (K ()) LhsL
lhs MJavaTerm AssignOpL
op CxtS NoHole MJavaSig (K ()) RhsL
rhs)) = JavaTerm LhsL
-> JavaTerm AssignOpL
-> JavaTerm ExpL
-> CxtS NoHole JavaSig (K ()) l
forall h (fs :: [Fragment]) (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 ())
:-> Cxt NoHole (Sum JavaSig) (K ())
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 :: [Fragment]) 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 ())
:-> Cxt NoHole (Sum JavaSig) (K ())
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 :: [Fragment]) 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' Cxt NoHole (Sum MJavaSig) (K ()) [BlockItemL]
items Cxt NoHole (Sum MJavaSig) (K ()) BlockEndL
_) = Cxt NoHole (Sum JavaSig) (K ()) [BlockStmtL] -> JavaTerm BlockL
forall h (fs :: [Fragment]) (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)
-> Cxt NoHole (Sum 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 ())
:-> Cxt NoHole (Sum JavaSig) (K ())
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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF) Cxt NoHole (Sum MJavaSig) (K ()) [BlockItemL]
items

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

instance {-# OVERLAPPING #-} Untrans FunctionCallIsMethodInvocation where
  untrans :: forall l.
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)
NatM
  Maybe
  (Cxt NoHole (Sum MJavaSig) (K ()))
  (JavaTypeArgs (Cxt NoHole (Sum MJavaSig) (K ())))
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (JavaTypeArgs CxtS NoHole MJavaSig (K ()) [RefTypeL]
targs))
                                                         (FunctionIdent' MJavaTerm IdentL
n)
                                                         (FunctionArgumentList' Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
args))) =
      case Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
args of
        ConsF' (ReceiverArg' Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL
receiver) Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
nonReceiverArgs ->
            let args' :: JavaTerm [ExpL]
args' = (Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
 -> JavaTerm ExpL)
-> Cxt NoHole (Sum 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 ())
:-> Cxt NoHole (Sum JavaSig) (K ())
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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF) Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
nonReceiverArgs in
            case Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL
receiver of
                PrimaryReceiver' CxtS NoHole MJavaSig (K ()) ExpL
e    -> JavaTerm ExpL
-> JavaTerm [RefTypeL]
-> JavaTerm IdentL
-> JavaTerm [ExpL]
-> JavaTerm l
forall h (fs :: [Fragment]) (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 ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) ExpL
e) (CxtS NoHole MJavaSig (K ()) [RefTypeL] -> JavaTerm [RefTypeL]
Cxt NoHole (Sum MJavaSig) (K ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) [RefTypeL]
targs) JavaTerm IdentL
n' JavaTerm [ExpL]
args'
                Cxt NoHole (Sum MJavaSig) (K ()) ReceiverL
SuperReceiver'        -> JavaTerm [RefTypeL]
-> JavaTerm IdentL -> JavaTerm [ExpL] -> JavaTerm l
forall h (fs :: [Fragment]) (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 ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) [RefTypeL]
targs) JavaTerm IdentL
n' JavaTerm [ExpL]
args'
                ClassSuperReceiver' CxtS NoHole MJavaSig (K ()) NameL
c -> JavaTerm NameL
-> JavaTerm [RefTypeL]
-> JavaTerm IdentL
-> JavaTerm [ExpL]
-> JavaTerm l
forall h (fs :: [Fragment]) (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 ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) NameL
c)   (CxtS NoHole MJavaSig (K ()) [RefTypeL] -> JavaTerm [RefTypeL]
Cxt NoHole (Sum MJavaSig) (K ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) [RefTypeL]
targs) JavaTerm IdentL
n' JavaTerm [ExpL]
args'
                TypeReceiver' CxtS NoHole MJavaSig (K ()) NameL
c       -> JavaTerm NameL
-> JavaTerm [RefTypeL]
-> JavaTerm IdentL
-> JavaTerm [ExpL]
-> JavaTerm l
forall h (fs :: [Fragment]) (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 ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) NameL
c)   (CxtS NoHole MJavaSig (K ()) [RefTypeL] -> JavaTerm [RefTypeL]
Cxt NoHole (Sum MJavaSig) (K ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) [RefTypeL]
targs) JavaTerm IdentL
n' JavaTerm [ExpL]
args'

        Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
_ -> case CxtS NoHole MJavaSig (K ()) [RefTypeL]
targs of
                 CxtS NoHole MJavaSig (K ()) [RefTypeL]
NilF' -> JavaTerm NameL -> JavaTerm [ExpL] -> JavaTerm l
forall h (fs :: [Fragment]) (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 :: [Fragment]) (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 :: Fragment) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a [l]
SingletonF' JavaTerm IdentL
n') ((Cxt NoHole (Sum MJavaSig) (K ()) FunctionArgumentL
 -> JavaTerm ExpL)
-> Cxt NoHole (Sum 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 ())
:-> Cxt NoHole (Sum JavaSig) (K ())
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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF) Cxt NoHole (Sum MJavaSig) (K ()) [FunctionArgumentL]
args)
                 CxtS NoHole MJavaSig (K ()) [RefTypeL]
_     -> String -> JavaTerm l
forall a. HasCallStack => String -> a
error String
"Illegal Java term constructed: type args passed to implicit receiver"
    where
      n' :: JavaTerm IdentL
n' = MJavaTerm IdentL -> JavaTerm IdentL
untransIdent MJavaTerm IdentL
n


untransParamDecl :: MJavaTerm FunctionParameterDeclL -> F.JavaTerm F.FormalParamL
untransParamDecl :: MJavaTerm FunctionParameterDeclL -> JavaTerm FormalParamL
untransParamDecl (MJavaTerm FunctionParameterDeclL
-> Maybe (CxtS NoHole MJavaSig (K ()) JavaVarargsParamL)
forall (fs :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> Maybe (CxtS h fs a l)
forall h (a :: * -> *).
CxtS h MJavaSig a FunctionParameterDeclL
-> Maybe (CxtS h MJavaSig a JavaVarargsParamL)
projF -> Just (JavaVarargsParam'               (JavaParamAttrs' CxtS NoHole MJavaSig (K ()) [ModifierL]
mods CxtS NoHole MJavaSig (K ()) TypeL
tp Int
dim) MJavaTerm IdentL
n)) = JavaTerm [ModifierL]
-> JavaTerm TypeL
-> Bool
-> JavaTerm VarDeclIdL
-> JavaTerm FormalParamL
forall h (fs :: [Fragment]) (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 ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) [ModifierL]
mods) (CxtS NoHole MJavaSig (K ()) TypeL -> JavaTerm TypeL
Cxt NoHole (Sum MJavaSig) (K ())
:-> Cxt NoHole (Sum JavaSig) (K ())
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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF -> JavaParamAttrs' CxtS NoHole MJavaSig (K ()) [ModifierL]
mods CxtS NoHole MJavaSig (K ()) TypeL
tp Int
dim) MJavaTerm IdentL
n)  = JavaTerm [ModifierL]
-> JavaTerm TypeL
-> Bool
-> JavaTerm VarDeclIdL
-> JavaTerm FormalParamL
forall h (fs :: [Fragment]) (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 ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) [ModifierL]
mods) (CxtS NoHole MJavaSig (K ()) TypeL -> JavaTerm TypeL
Cxt NoHole (Sum MJavaSig) (K ())
:-> Cxt NoHole (Sum JavaSig) (K ())
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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> Maybe (CxtS h fs a l)
forall h (a :: * -> *).
CxtS h MJavaSig a FunctionParameterL
-> Maybe (CxtS h MJavaSig a JavaVarargsParamL)
projF -> Just (JavaVarargsParam'  (JavaParamAttrs' CxtS NoHole MJavaSig (K ()) [ModifierL]
mods CxtS NoHole MJavaSig (K ()) TypeL
tp Int
dim) MJavaTerm IdentL
n)) = JavaTerm [ModifierL]
-> JavaTerm TypeL
-> Bool
-> JavaTerm VarDeclIdL
-> JavaTerm FormalParamL
forall h (fs :: [Fragment]) (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 ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) [ModifierL]
mods) (CxtS NoHole MJavaSig (K ()) TypeL -> JavaTerm TypeL
Cxt NoHole (Sum MJavaSig) (K ())
:-> Cxt NoHole (Sum JavaSig) (K ())
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 :: [Fragment]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF -> JavaParamAttrs' CxtS NoHole MJavaSig (K ()) [ModifierL]
mods CxtS NoHole MJavaSig (K ()) TypeL
tp Int
dim) MJavaTerm IdentL
n)  = JavaTerm [ModifierL]
-> JavaTerm TypeL
-> Bool
-> JavaTerm VarDeclIdL
-> JavaTerm FormalParamL
forall h (fs :: [Fragment]) (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 ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) [ModifierL]
mods) (CxtS NoHole MJavaSig (K ()) TypeL -> JavaTerm TypeL
Cxt NoHole (Sum MJavaSig) (K ())
:-> Cxt NoHole (Sum JavaSig) (K ())
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 :: forall l.
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)
NatM
  Maybe
  (Cxt NoHole (Sum MJavaSig) (K ()))
  (JavaMethodDeclAttrsIsFunctionDeclAttrs
     (Cxt NoHole (Sum MJavaSig) (K ())))
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (JavaMethodDeclAttrsIsFunctionDeclAttrs (JavaMethodDeclAttrs' CxtS NoHole MJavaSig (K ()) [ModifierL]
mods CxtS NoHole MJavaSig (K ()) [TypeParamL]
tparams CxtS NoHole MJavaSig (K ()) (Maybe TypeL)
tp CxtS NoHole MJavaSig (K ()) [RefTypeL]
ex)))
                                                   MJavaTerm IdentL
n
                                                   CxtS NoHole MJavaSig (K ()) [FunctionParameterDeclL]
params))
           = JavaTerm [ModifierL]
-> JavaTerm [TypeParamL]
-> JavaTerm (Maybe TypeL)
-> JavaTerm IdentL
-> JavaTerm [FormalParamL]
-> JavaTerm [RefTypeL]
-> Cxt NoHole (Sum JavaSig) (K ()) (Maybe ExpL)
-> JavaTerm MethodBodyL
-> CxtS NoHole JavaSig (K ()) l
forall h (fs :: [Fragment]) (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 ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) [ModifierL]
mods)
                           (CxtS NoHole MJavaSig (K ()) [TypeParamL] -> JavaTerm [TypeParamL]
Cxt NoHole (Sum MJavaSig) (K ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) [TypeParamL]
tparams)
                           (CxtS NoHole MJavaSig (K ()) (Maybe TypeL) -> JavaTerm (Maybe TypeL)
Cxt NoHole (Sum MJavaSig) (K ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) (Maybe TypeL)
tp)
                           (MJavaTerm IdentL -> JavaTerm IdentL
untransIdent MJavaTerm IdentL
n)
                           ([JavaTerm FormalParamL] -> JavaTerm [FormalParamL]
forall l.
Typeable l =>
[Cxt NoHole (Sum JavaSig) (K ()) l]
-> Cxt NoHole (Sum JavaSig) (K ()) [l]
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 h (f :: Fragment) (a :: * -> *) j.
(SelfParameterDecl :<: f) =>
Cxt h f 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 l.
Cxt NoHole (Sum MJavaSig) (K ()) [l]
-> [Cxt NoHole (Sum MJavaSig) (K ()) l]
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 ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) [RefTypeL]
ex)
                           Cxt NoHole (Sum JavaSig) (K ()) (Maybe ExpL)
forall (f :: Fragment) 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 :: [Fragment]) (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 :: Fragment) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a (Maybe l)
Nothing')

instance {-# OVERLAPPING #-} Untrans FunctionDefIsMemberDecl where
  untrans :: forall l.
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)
NatM
  Maybe
  (Cxt NoHole (Sum MJavaSig) (K ()))
  (JavaMethodDeclAttrsIsFunctionDefAttrs
     (Cxt NoHole (Sum MJavaSig) (K ())))
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (JavaMethodDeclAttrsIsFunctionDefAttrs (JavaMethodDeclAttrs' CxtS NoHole MJavaSig (K ()) [ModifierL]
mods CxtS NoHole MJavaSig (K ()) [TypeParamL]
tparams CxtS NoHole MJavaSig (K ()) (Maybe TypeL)
tp CxtS NoHole MJavaSig (K ()) [RefTypeL]
ex)))
                                                  MJavaTerm IdentL
n
                                                  CxtS NoHole MJavaSig (K ()) [FunctionParameterL]
params
                                                  CxtS NoHole MJavaSig (K ()) FunctionBodyL
body))
           = JavaTerm [ModifierL]
-> JavaTerm [TypeParamL]
-> JavaTerm (Maybe TypeL)
-> JavaTerm IdentL
-> JavaTerm [FormalParamL]
-> JavaTerm [RefTypeL]
-> Cxt NoHole (Sum JavaSig) (K ()) (Maybe ExpL)
-> JavaTerm MethodBodyL
-> CxtS NoHole JavaSig (K ()) l
forall h (fs :: [Fragment]) (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 ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) [ModifierL]
mods)
                           (CxtS NoHole MJavaSig (K ()) [TypeParamL] -> JavaTerm [TypeParamL]
Cxt NoHole (Sum MJavaSig) (K ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) [TypeParamL]
tparams)
                           (CxtS NoHole MJavaSig (K ()) (Maybe TypeL) -> JavaTerm (Maybe TypeL)
Cxt NoHole (Sum MJavaSig) (K ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) (Maybe TypeL)
tp)
                           (MJavaTerm IdentL -> JavaTerm IdentL
untransIdent MJavaTerm IdentL
n)
                           ([JavaTerm FormalParamL] -> JavaTerm [FormalParamL]
forall l.
Typeable l =>
[Cxt NoHole (Sum JavaSig) (K ()) l]
-> Cxt NoHole (Sum JavaSig) (K ()) [l]
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 h (f :: Fragment) (a :: * -> *) j.
(SelfParameter :<: f) =>
Cxt h f 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 l.
Cxt NoHole (Sum MJavaSig) (K ()) [l]
-> [Cxt NoHole (Sum MJavaSig) (K ()) l]
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 ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate CxtS NoHole MJavaSig (K ()) [RefTypeL]
ex)
                           Cxt NoHole (Sum JavaSig) (K ()) (Maybe ExpL)
forall (f :: Fragment) 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 :: [Fragment]) (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 :: Fragment) 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 :: [Fragment]) 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)))

untranslate :: MJavaTerm l -> F.JavaTerm l
untranslate :: Cxt NoHole (Sum MJavaSig) (K ())
:-> Cxt NoHole (Sum JavaSig) (K ())
untranslate = Sum MJavaSig (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
forall l.
Sum MJavaSig (Cxt NoHole (Sum MJavaSig) (K ())) l -> JavaTerm l
forall (f :: Fragment) 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 :: Fragment) t. HFix f t -> f (HFix f) t
unTerm

#endif