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

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

import Control.Monad.Identity ( Identity(..) )

import Data.Monoid ( Any(..) )
import Data.Proxy
import Data.List( (\\) )
import Language.Haskell.TH.Syntax ( Type(ConT), Exp(VarE) )

import Data.Comp.Multi ( project, inject, unTerm, caseCxt, Sum, All, HFunctor(..), (:-<:) )
import Data.Comp.Multi.Strategic ( crushtdT, addFail, promoteTF )

import qualified Language.C as COrig

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

translate :: F.CTerm l -> MCTerm l
translate :: CTerm l -> MCTerm l
translate = Sum CSig CTerm l -> MCTerm l
forall (f :: (* -> *) -> * -> *) l.
Trans f =>
f CTerm l -> MCTerm l
trans (Sum CSig CTerm l -> MCTerm l)
-> (CTerm l -> Sum CSig CTerm l) -> CTerm l -> MCTerm l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CTerm l -> Sum CSig CTerm l
forall (f :: (* -> *) -> * -> *) t. HFix f t -> f (HFix f) t
unTerm

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

class Trans f where
  trans :: f F.CTerm l -> MCTerm l

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

transDefault :: (HFunctor f, f :-<: MCSig, f :-<: F.CSig) => f F.CTerm l -> MCTerm l
transDefault :: f CTerm l -> MCTerm l
transDefault = f (Cxt NoHole (Sum MCSig) (K ())) l -> MCTerm l
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (f (Cxt NoHole (Sum MCSig) (K ())) l -> MCTerm l)
-> (f CTerm l -> f (Cxt NoHole (Sum MCSig) (K ())) l)
-> f CTerm l
-> MCTerm l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall l. CTerm l -> MCTerm l)
-> f CTerm :-> f (Cxt NoHole (Sum MCSig) (K ()))
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap forall l. CTerm l -> MCTerm l
translate

instance {-# OVERLAPPABLE #-} (HFunctor f, f :-<: MCSig, f :-<: F.CSig) => Trans f where
  trans :: f CTerm l -> MCTerm l
trans = f CTerm l -> MCTerm l
forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: MCSig, f :-<: CSig) =>
f CTerm l -> MCTerm l
transDefault

-- Damn language-c mixing in annotations. We drop them for the pure tree
transIdent :: F.CTerm F.IdentL -> MCTerm IdentL
transIdent :: CTerm IdentL -> MCTerm IdentL
transIdent (CTerm IdentL -> Maybe (Ident CTerm IdentL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.Ident s :: String
s _ _)) = String -> MCTerm IdentL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(Ident :-<: fs, All HFunctor fs) =>
String -> CxtS h fs a IdentL
Ident' String
s

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

transSingleDec :: F.CTerm (Maybe F.CDeclaratorL, Maybe F.CInitializerL, Maybe F.CExpressionL) ->  MCTerm SingleLocalVarDeclL
transSingleDec :: CTerm (Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)
-> MCTerm SingleLocalVarDeclL
transSingleDec (CTerm (Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)
-> (Cxt NoHole (Sum CSig) (K ()) (Maybe CDeclaratorL),
    Cxt NoHole (Sum CSig) (K ()) (Maybe CInitializerL),
    Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL))
forall (f :: * -> * -> * -> *) (e :: * -> *) l l' l''.
ExtractF3 f e =>
e (f l l' l'') -> f (e l) (e l') (e l'')
extractF3 -> (declaratorOpt :: Cxt NoHole (Sum CSig) (K ()) (Maybe CDeclaratorL)
declaratorOpt, initOpt :: Cxt NoHole (Sum CSig) (K ()) (Maybe CInitializerL)
initOpt, bitFieldOpt :: Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
bitFieldOpt)) = ()
checkBitField () -> MCTerm SingleLocalVarDeclL -> MCTerm SingleLocalVarDeclL
forall a b. a -> b -> b
`seq` CxtS NoHole MCSig (K ()) LocalVarDeclAttrsL
-> CxtS NoHole MCSig (K ()) VarDeclBinderL
-> CxtS NoHole MCSig (K ()) OptLocalVarInitL
-> MCTerm SingleLocalVarDeclL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(SingleLocalVarDecl :-<: fs, All HFunctor fs) =>
CxtS h fs a LocalVarDeclAttrsL
-> CxtS h fs a VarDeclBinderL
-> CxtS h fs a OptLocalVarInitL
-> CxtS h fs a SingleLocalVarDeclL
SingleLocalVarDecl' CxtS NoHole MCSig (K ()) LocalVarDeclAttrsL
localOpts CxtS NoHole MCSig (K ()) VarDeclBinderL
id CxtS NoHole MCSig (K ()) OptLocalVarInitL
init
  where
    checkBitField :: ()
checkBitField = case Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
bitFieldOpt of
      Just' _  -> String -> ()
forall a. HasCallStack => String -> a
error "Attempting to translate bitfield var declaration as if it were a local decl"
      Nothing' -> ()

    (id :: CxtS NoHole MCSig (K ()) VarDeclBinderL
id, localOpts :: CxtS NoHole MCSig (K ()) LocalVarDeclAttrsL
localOpts) = case Cxt NoHole (Sum CSig) (K ()) (Maybe CDeclaratorL)
declaratorOpt of
      Just' (Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
-> Maybe (CDeclarator CTerm CDeclaratorL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CDeclr (Just' vid :: CTerm IdentL
vid) decls :: Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
decls asmName :: Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
asmName attrs :: Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs _)) -> (MCTerm IdentL -> CxtS NoHole MCSig (K ()) VarDeclBinderL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (MCTerm IdentL -> CxtS NoHole MCSig (K ()) VarDeclBinderL)
-> MCTerm IdentL -> CxtS NoHole MCSig (K ()) VarDeclBinderL
forall a b. (a -> b) -> a -> b
$ CTerm IdentL -> MCTerm IdentL
transIdent CTerm IdentL
vid, CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
-> CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
-> CxtS NoHole MCSig (K ()) [CAttributeL]
-> CxtS NoHole MCSig (K ()) LocalVarDeclAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CLocalVarAttrs :-<: fs, InjF fs LocalVarDeclAttrsL j) =>
CxtS h fs a [CDerivedDeclaratorL]
-> CxtS h fs a (Maybe CStringLiteralL)
-> CxtS h fs a [CAttributeL]
-> CxtS h fs a j
iCLocalVarAttrs (Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
-> CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
decls) (Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
-> CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
asmName) (Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
-> CxtS NoHole MCSig (K ()) [CAttributeL]
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs))
      _ -> String
-> (CxtS NoHole MCSig (K ()) VarDeclBinderL,
    CxtS NoHole MCSig (K ()) LocalVarDeclAttrsL)
forall a. HasCallStack => String -> a
error "Attempting to translate nameless bitfield var declaration as if it were a local decl"

    init :: CxtS NoHole MCSig (K ()) OptLocalVarInitL
init = case Cxt NoHole (Sum CSig) (K ()) (Maybe CInitializerL)
initOpt of
      Nothing' -> CxtS NoHole MCSig (K ()) OptLocalVarInitL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(OptLocalVarInit :-<: fs, All HFunctor fs) =>
CxtS h fs a OptLocalVarInitL
NoLocalVarInit'
      Just' x :: Cxt NoHole (Sum CSig) (K ()) CInitializerL
x  -> CxtS NoHole MCSig (K ()) LocalVarInitL
-> CxtS NoHole MCSig (K ()) OptLocalVarInitL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(OptLocalVarInit :-<: fs, All HFunctor fs) =>
CxtS h fs a LocalVarInitL -> CxtS h fs a OptLocalVarInitL
JustLocalVarInit' (CxtS NoHole MCSig (K ()) LocalVarInitL
 -> CxtS NoHole MCSig (K ()) OptLocalVarInitL)
-> CxtS NoHole MCSig (K ()) LocalVarInitL
-> CxtS NoHole MCSig (K ()) OptLocalVarInitL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MCSig (K ()) CInitializerL
-> CxtS NoHole MCSig (K ()) LocalVarInitL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MCSig (K ()) CInitializerL
 -> CxtS NoHole MCSig (K ()) LocalVarInitL)
-> CxtS NoHole MCSig (K ()) CInitializerL
-> CxtS NoHole MCSig (K ()) LocalVarInitL
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum CSig) (K ()) CInitializerL
-> CxtS NoHole MCSig (K ()) CInitializerL
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) CInitializerL
x

containsStatic :: F.CTerm F.CDeclarationL -> Bool
containsStatic :: CTerm CDeclarationL -> Bool
containsStatic = Any -> Bool
getAny (Any -> Bool)
-> (CTerm CDeclarationL -> Any) -> CTerm CDeclarationL -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity Any -> Any
forall a. Identity a -> a
runIdentity (Identity Any -> Any)
-> (CTerm CDeclarationL -> Identity Any)
-> CTerm CDeclarationL
-> Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GTranslateM (MaybeT Identity) CTerm Any
-> CTerm CDeclarationL -> Identity Any
forall (f :: (* -> *) -> * -> *) t (m :: * -> *).
(HFoldable f, Monoid t, Monad m) =>
GTranslateM (MaybeT m) (HFix f) t -> GTranslateM m (HFix f) t
crushtdT (GTranslateM (MaybeT Identity) CTerm Any
 -> CTerm CDeclarationL -> Identity Any)
-> GTranslateM (MaybeT Identity) CTerm Any
-> CTerm CDeclarationL
-> Identity Any
forall a b. (a -> b) -> a -> b
$ TranslateM (MaybeT Identity) CTerm CStorageSpecifierL Any
-> TranslateM (MaybeT Identity) CTerm l Any
forall (f :: * -> *) l (m :: * -> *) t.
(DynCase f l, Alternative m) =>
TranslateM m f l t -> GTranslateM m f t
promoteTF (TranslateM (MaybeT Identity) CTerm CStorageSpecifierL Any
 -> TranslateM (MaybeT Identity) CTerm l Any)
-> TranslateM (MaybeT Identity) CTerm CStorageSpecifierL Any
-> TranslateM (MaybeT Identity) CTerm l Any
forall a b. (a -> b) -> a -> b
$ TranslateM Identity CTerm CStorageSpecifierL Any
-> TranslateM (MaybeT Identity) CTerm CStorageSpecifierL Any
forall (m :: * -> *) (f :: * -> *) l t.
Monad m =>
TranslateM m f l t -> TranslateM (MaybeT m) f l t
addFail TranslateM Identity CTerm CStorageSpecifierL Any
forall (m :: * -> *). Monad m => CTerm CStorageSpecifierL -> m Any
isStatic)
  where
    isStatic :: (Monad m) => F.CTerm F.CStorageSpecifierL -> m Any
    isStatic :: CTerm CStorageSpecifierL -> m Any
isStatic (CTerm CStorageSpecifierL
-> Maybe (CStorageSpecifier CTerm CStorageSpecifierL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CStatic _)) = Any -> m Any
forall (m :: * -> *) a. Monad m => a -> m a
return (Any -> m Any) -> Any -> m Any
forall a b. (a -> b) -> a -> b
$ Bool -> Any
Any Bool
True
    isStatic _                               = Any -> m Any
forall (m :: * -> *) a. Monad m => a -> m a
return (Any -> m Any) -> Any -> m Any
forall a b. (a -> b) -> a -> b
$ Bool -> Any
Any Bool
False

instance {-# OVERLAPPING #-} Trans F.CCompoundBlockItem where
  trans :: CCompoundBlockItem CTerm l -> MCTerm l
trans t :: CCompoundBlockItem CTerm l
t@(F.CBlockStmt _)    = CCompoundBlockItem CTerm l -> MCTerm l
forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: MCSig, f :-<: CSig) =>
f CTerm l -> MCTerm l
transDefault CCompoundBlockItem CTerm l
t
  trans t :: CCompoundBlockItem CTerm l
t@(F.CNestedFunDef _) = CCompoundBlockItem CTerm l -> MCTerm l
forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: MCSig, f :-<: CSig) =>
f CTerm l -> MCTerm l
transDefault CCompoundBlockItem CTerm l
t
  trans t :: CCompoundBlockItem CTerm l
t@(F.CBlockDecl decl :: CTerm CDeclarationL
decl) =
    if CTerm CDeclarationL -> Bool
containsStatic CTerm CDeclarationL
decl then
      CCompoundBlockItem CTerm l -> MCTerm l
forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: MCSig, f :-<: CSig) =>
f CTerm l -> MCTerm l
transDefault CCompoundBlockItem CTerm l
t
    else
      CxtS NoHole MCSig (K ()) MultiLocalVarDeclL -> MCTerm l
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MCSig (K ()) MultiLocalVarDeclL -> MCTerm l)
-> CxtS NoHole MCSig (K ()) MultiLocalVarDeclL -> MCTerm l
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MCSig (K ()) MultiLocalVarDeclCommonAttrsL
-> CxtS NoHole MCSig (K ()) [SingleLocalVarDeclL]
-> CxtS NoHole MCSig (K ()) MultiLocalVarDeclL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(MultiLocalVarDecl :-<: fs, All HFunctor fs) =>
CxtS h fs a MultiLocalVarDeclCommonAttrsL
-> CxtS h fs a [SingleLocalVarDeclL]
-> CxtS h fs a MultiLocalVarDeclL
MultiLocalVarDecl' (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) MultiLocalVarDeclCommonAttrsL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
 -> CxtS NoHole MCSig (K ()) MultiLocalVarDeclCommonAttrsL)
-> CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) MultiLocalVarDeclCommonAttrsL
forall a b. (a -> b) -> a -> b
$ CTerm [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
forall l. CTerm l -> MCTerm l
translate CTerm [CDeclarationSpecifierL]
specs) ((CTerm
   (Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)
 -> MCTerm SingleLocalVarDeclL)
-> Cxt
     NoHole
     (Sum CSig)
     (K ())
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> CxtS NoHole MCSig (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 CTerm (Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)
-> MCTerm SingleLocalVarDeclL
transSingleDec Cxt
  NoHole
  (Sum CSig)
  (K ())
  [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
single_decs)
    where
      Just (F.CDecl specs single_decs _) = CTerm CDeclarationL -> Maybe (CDeclaration CTerm CDeclarationL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project CTerm CDeclarationL
decl

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

translateArgs :: F.CTerm [F.CExpressionL] -> MCTerm FunctionArgumentsL
translateArgs :: CTerm [CExpressionL] -> MCTerm FunctionArgumentsL
translateArgs args :: CTerm [CExpressionL]
args = CxtS NoHole MCSig (K ()) [FunctionArgumentL]
-> MCTerm FunctionArgumentsL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(FunctionArgumentList :-<: fs, All HFunctor fs) =>
CxtS h fs a [FunctionArgumentL] -> CxtS h fs a FunctionArgumentsL
FunctionArgumentList' (CxtS NoHole MCSig (K ()) [FunctionArgumentL]
 -> MCTerm FunctionArgumentsL)
-> CxtS NoHole MCSig (K ()) [FunctionArgumentL]
-> MCTerm FunctionArgumentsL
forall a b. (a -> b) -> a -> b
$ (Cxt NoHole (Sum CSig) (K ()) CExpressionL
 -> Cxt NoHole (Sum MCSig) (K ()) FunctionArgumentL)
-> CTerm [CExpressionL]
-> CxtS NoHole MCSig (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 MCSig (K ()) PositionalArgExpL
-> Cxt NoHole (Sum MCSig) (K ()) FunctionArgumentL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(PositionalArgument :-<: fs, All HFunctor fs) =>
CxtS h fs a PositionalArgExpL -> CxtS h fs a FunctionArgumentL
PositionalArgument' (CxtS NoHole MCSig (K ()) PositionalArgExpL
 -> Cxt NoHole (Sum MCSig) (K ()) FunctionArgumentL)
-> (Cxt NoHole (Sum CSig) (K ()) CExpressionL
    -> CxtS NoHole MCSig (K ()) PositionalArgExpL)
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
-> Cxt NoHole (Sum MCSig) (K ()) FunctionArgumentL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtS NoHole MCSig (K ()) CExpressionL
-> CxtS NoHole MCSig (K ()) PositionalArgExpL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MCSig (K ()) CExpressionL
 -> CxtS NoHole MCSig (K ()) PositionalArgExpL)
-> (Cxt NoHole (Sum CSig) (K ()) CExpressionL
    -> CxtS NoHole MCSig (K ()) CExpressionL)
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
-> CxtS NoHole MCSig (K ()) PositionalArgExpL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cxt NoHole (Sum CSig) (K ()) CExpressionL
-> CxtS NoHole MCSig (K ()) CExpressionL
forall l. CTerm l -> MCTerm l
translate) CTerm [CExpressionL]
args

instance {-# OVERLAPPING #-} Trans F.CExpression where
  trans :: CExpression CTerm l -> MCTerm l
trans t :: CExpression CTerm l
t@(F.CAssign op :: CTerm CAssignOpL
op lhs :: Cxt NoHole (Sum CSig) (K ()) CExpressionL
lhs rhs :: Cxt NoHole (Sum CSig) (K ()) CExpressionL
rhs _) = CxtS NoHole MCSig (K ()) LhsL
-> MCTerm AssignOpL -> CxtS NoHole MCSig (K ()) RhsL -> MCTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(Assign :-<: fs, InjF fs AssignL j) =>
CxtS h fs a LhsL
-> CxtS h fs a AssignOpL -> CxtS h fs a RhsL -> CxtS h fs a j
iAssign (CxtS NoHole MCSig (K ()) CExpressionL
-> CxtS NoHole MCSig (K ()) LhsL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MCSig (K ()) CExpressionL
 -> CxtS NoHole MCSig (K ()) LhsL)
-> CxtS NoHole MCSig (K ()) CExpressionL
-> CxtS NoHole MCSig (K ()) LhsL
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum CSig) (K ()) CExpressionL
-> CxtS NoHole MCSig (K ()) CExpressionL
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) CExpressionL
lhs) (CTerm CAssignOpL -> MCTerm AssignOpL
transOp CTerm CAssignOpL
op) (CxtS NoHole MCSig (K ()) CExpressionL
-> CxtS NoHole MCSig (K ()) RhsL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MCSig (K ()) CExpressionL
 -> CxtS NoHole MCSig (K ()) RhsL)
-> CxtS NoHole MCSig (K ()) CExpressionL
-> CxtS NoHole MCSig (K ()) RhsL
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum CSig) (K ()) CExpressionL
-> CxtS NoHole MCSig (K ()) CExpressionL
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) CExpressionL
rhs)
  trans t :: CExpression CTerm l
t@(F.CCall f :: Cxt NoHole (Sum CSig) (K ()) CExpressionL
f args :: CTerm [CExpressionL]
args _)       = CxtS NoHole MCSig (K ()) FunctionCallAttrsL
-> CxtS NoHole MCSig (K ()) FunctionExpL
-> MCTerm FunctionArgumentsL
-> MCTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(FunctionCall :-<: fs, InjF fs FunctionCallL j) =>
CxtS h fs a FunctionCallAttrsL
-> CxtS h fs a FunctionExpL
-> CxtS h fs a FunctionArgumentsL
-> CxtS h fs a j
iFunctionCall CxtS NoHole MCSig (K ()) FunctionCallAttrsL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(EmptyFunctionCallAttrs :-<: fs, All HFunctor fs) =>
CxtS h fs a FunctionCallAttrsL
EmptyFunctionCallAttrs' (CxtS NoHole MCSig (K ()) CExpressionL
-> CxtS NoHole MCSig (K ()) FunctionExpL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MCSig (K ()) CExpressionL
 -> CxtS NoHole MCSig (K ()) FunctionExpL)
-> CxtS NoHole MCSig (K ()) CExpressionL
-> CxtS NoHole MCSig (K ()) FunctionExpL
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum CSig) (K ()) CExpressionL
-> CxtS NoHole MCSig (K ()) CExpressionL
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) CExpressionL
f) (CTerm [CExpressionL] -> MCTerm FunctionArgumentsL
translateArgs CTerm [CExpressionL]
args)
  trans t :: CExpression CTerm l
t                          = CExpression CTerm l -> MCTerm l
forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: MCSig, f :-<: CSig) =>
f CTerm l -> MCTerm l
transDefault CExpression CTerm l
t

instance {-# OVERLAPPING #-} Trans F.CStatement where
  trans :: CStatement CTerm l -> MCTerm l
trans t :: CStatement CTerm l
t@(F.CCompound ids :: CTerm [IdentL]
ids items :: CTerm [CCompoundBlockItemL]
items _) = CxtS NoHole MCSig (K ()) [IdentL]
-> CxtS NoHole MCSig (K ()) BlockL -> MCTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CLabeledBlock :-<: fs, InjF fs CStatementL j) =>
CxtS h fs a [IdentL] -> CxtS h fs a BlockL -> CxtS h fs a j
iCLabeledBlock ((CTerm IdentL -> MCTerm IdentL)
-> CTerm [IdentL] -> CxtS NoHole MCSig (K ()) [IdentL]
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 CTerm IdentL -> MCTerm IdentL
transIdent CTerm [IdentL]
ids) (CxtS NoHole MCSig (K ()) [BlockItemL]
-> CxtS NoHole MCSig (K ()) BlockEndL
-> CxtS NoHole MCSig (K ()) BlockL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(Block :-<: fs, All HFunctor fs) =>
CxtS h fs a [BlockItemL]
-> CxtS h fs a BlockEndL -> CxtS h fs a BlockL
Block' ((Cxt NoHole (Sum CSig) (K ()) CCompoundBlockItemL
 -> Cxt NoHole (Sum MCSig) (K ()) BlockItemL)
-> CTerm [CCompoundBlockItemL]
-> CxtS NoHole MCSig (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 MCSig (K ()) CCompoundBlockItemL
-> Cxt NoHole (Sum MCSig) (K ()) BlockItemL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF(CxtS NoHole MCSig (K ()) CCompoundBlockItemL
 -> Cxt NoHole (Sum MCSig) (K ()) BlockItemL)
-> (Cxt NoHole (Sum CSig) (K ()) CCompoundBlockItemL
    -> CxtS NoHole MCSig (K ()) CCompoundBlockItemL)
-> Cxt NoHole (Sum CSig) (K ()) CCompoundBlockItemL
-> Cxt NoHole (Sum MCSig) (K ()) BlockItemL
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cxt NoHole (Sum CSig) (K ()) CCompoundBlockItemL
-> CxtS NoHole MCSig (K ()) CCompoundBlockItemL
forall l. CTerm l -> MCTerm l
translate) CTerm [CCompoundBlockItemL]
items) CxtS NoHole MCSig (K ()) BlockEndL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(EmptyBlockEnd :-<: fs, All HFunctor fs) =>
CxtS h fs a BlockEndL
EmptyBlockEnd')
  trans t :: CStatement CTerm l
t                           = CStatement CTerm l -> MCTerm l
forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: MCSig, f :-<: CSig) =>
f CTerm l -> MCTerm l
transDefault CStatement CTerm l
t

paramDeclFromId :: F.CTerm F.IdentL -> MCTerm FunctionParameterDeclL
paramDeclFromId :: CTerm IdentL -> MCTerm FunctionParameterDeclL
paramDeclFromId n :: CTerm IdentL
n = CxtS NoHole MCSig (K ()) FunctionParameterDeclAttrsL
-> CxtS NoHole MCSig (K ()) (Maybe IdentL)
-> MCTerm FunctionParameterDeclL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(PositionalParameterDeclOptionalIdent :-<: fs, All HFunctor fs) =>
CxtS h fs a FunctionParameterDeclAttrsL
-> CxtS h fs a (Maybe IdentL) -> CxtS h fs a FunctionParameterDeclL
PositionalParameterDeclOptionalIdent' (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
-> CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
-> CxtS NoHole MCSig (K ()) [CAttributeL]
-> CxtS NoHole MCSig (K ()) FunctionParameterDeclAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CFunParamAttrs :-<: fs, InjF fs CFunParamAttrsL j) =>
CxtS h fs a [CDeclarationSpecifierL]
-> CxtS h fs a [CDerivedDeclaratorL]
-> CxtS h fs a (Maybe CStringLiteralL)
-> CxtS h fs a [CAttributeL]
-> CxtS h fs a j
iCFunParamAttrs CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a [l]
NilF' CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a [l]
NilF' CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a (Maybe l)
Nothing' CxtS NoHole MCSig (K ()) [CAttributeL]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a [l]
NilF') (MCTerm IdentL -> CxtS NoHole MCSig (K ()) (Maybe IdentL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a (Maybe l)
Just' (MCTerm IdentL -> CxtS NoHole MCSig (K ()) (Maybe IdentL))
-> MCTerm IdentL -> CxtS NoHole MCSig (K ()) (Maybe IdentL)
forall a b. (a -> b) -> a -> b
$ CTerm IdentL -> MCTerm IdentL
transIdent CTerm IdentL
n)

paramDeclFromDecl :: F.CTerm F.CDeclarationL -> MCTerm FunctionParameterDeclL
paramDeclFromDecl :: CTerm CDeclarationL -> MCTerm FunctionParameterDeclL
paramDeclFromDecl (CTerm CDeclarationL -> Maybe (CDeclaration CTerm CDeclarationL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CDecl (SingletonF' (Cxt NoHole (Sum CSig) (K ()) CDeclarationSpecifierL
-> Maybe (CDeclarationSpecifier CTerm CDeclarationSpecifierL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CTypeSpec (Cxt NoHole (Sum CSig) (K ()) CTypeSpecifierL
-> Maybe (CTypeSpecifier CTerm CTypeSpecifierL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CVoidType _))))) NilF' _)) = MCTerm FunctionParameterDeclL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CVoidArg :-<: fs, InjF fs CSpecialParamL j) =>
CxtS h fs a j
iCVoidArg

paramDeclFromDecl (CTerm CDeclarationL -> Maybe (CDeclaration CTerm CDeclarationL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CDecl dss :: CTerm [CDeclarationSpecifierL]
dss inf :: Cxt
  NoHole
  (Sum CSig)
  (K ())
  [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
inf _)) =
  case Cxt
  NoHole
  (Sum CSig)
  (K ())
  [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
inf of
    NilF' -> CxtS NoHole MCSig (K ()) FunctionParameterDeclAttrsL
-> CxtS NoHole MCSig (K ()) (Maybe IdentL)
-> MCTerm FunctionParameterDeclL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(PositionalParameterDeclOptionalIdent :-<: fs, All HFunctor fs) =>
CxtS h fs a FunctionParameterDeclAttrsL
-> CxtS h fs a (Maybe IdentL) -> CxtS h fs a FunctionParameterDeclL
PositionalParameterDeclOptionalIdent' (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
-> CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
-> CxtS NoHole MCSig (K ()) [CAttributeL]
-> CxtS NoHole MCSig (K ()) FunctionParameterDeclAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CFunParamAttrs :-<: fs, InjF fs CFunParamAttrsL j) =>
CxtS h fs a [CDeclarationSpecifierL]
-> CxtS h fs a [CDerivedDeclaratorL]
-> CxtS h fs a (Maybe CStringLiteralL)
-> CxtS h fs a [CAttributeL]
-> CxtS h fs a j
iCFunParamAttrs (CTerm [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
forall l. CTerm l -> MCTerm l
translate CTerm [CDeclarationSpecifierL]
dss) CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a [l]
NilF' CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a (Maybe l)
Nothing' CxtS NoHole MCSig (K ()) [CAttributeL]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a [l]
NilF') CxtS NoHole MCSig (K ()) (Maybe IdentL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a (Maybe l)
Nothing'
    (SingletonF' (TripleF' (Just' (Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
-> Maybe (CDeclarator CTerm CDeclaratorL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CDeclr nOpt :: Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL)
nOpt dds :: Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
dds asmNm :: Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
asmNm attrs :: Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs _))) Nothing' Nothing')) ->
                CxtS NoHole MCSig (K ()) FunctionParameterDeclAttrsL
-> CxtS NoHole MCSig (K ()) (Maybe IdentL)
-> MCTerm FunctionParameterDeclL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(PositionalParameterDeclOptionalIdent :-<: fs, All HFunctor fs) =>
CxtS h fs a FunctionParameterDeclAttrsL
-> CxtS h fs a (Maybe IdentL) -> CxtS h fs a FunctionParameterDeclL
PositionalParameterDeclOptionalIdent' (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
-> CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
-> CxtS NoHole MCSig (K ()) [CAttributeL]
-> CxtS NoHole MCSig (K ()) FunctionParameterDeclAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CFunParamAttrs :-<: fs, InjF fs CFunParamAttrsL j) =>
CxtS h fs a [CDeclarationSpecifierL]
-> CxtS h fs a [CDerivedDeclaratorL]
-> CxtS h fs a (Maybe CStringLiteralL)
-> CxtS h fs a [CAttributeL]
-> CxtS h fs a j
iCFunParamAttrs (CTerm [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
forall l. CTerm l -> MCTerm l
translate CTerm [CDeclarationSpecifierL]
dss) (Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
-> CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
dds) (Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
-> CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
asmNm) (Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
-> CxtS NoHole MCSig (K ()) [CAttributeL]
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs)) ((CTerm IdentL -> MCTerm IdentL)
-> Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL)
-> CxtS NoHole MCSig (K ()) (Maybe IdentL)
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 CTerm IdentL -> MCTerm IdentL
transIdent Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL)
nOpt)

instance {-# OVERLAPPING #-} Trans F.CDeclarator where
  trans :: CDeclarator CTerm l -> MCTerm l
trans t :: CDeclarator CTerm l
t@(F.CDeclr (Just' n :: CTerm IdentL
n) (ConsF' (Cxt NoHole (Sum CSig) (K ()) CDerivedDeclaratorL
-> Maybe (CDerivedDeclarator CTerm CDerivedDeclaratorL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CFunDeclr pars :: Cxt
  NoHole (Sum CSig) (K ()) (Either [IdentL] ([CDeclarationL], BoolL))
pars attrs1 :: Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs1 _)) dds :: Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
dds) asmNm :: Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
asmNm attrs2 :: Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs2 _) =
    CxtS NoHole MCSig (K ()) FunctionDeclAttrsL
-> MCTerm IdentL
-> CxtS NoHole MCSig (K ()) [FunctionParameterDeclL]
-> MCTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(FunctionDecl :-<: fs, InjF fs FunctionDeclL j) =>
CxtS h fs a FunctionDeclAttrsL
-> CxtS h fs a IdentL
-> CxtS h fs a [FunctionParameterDeclL]
-> CxtS h fs a j
iFunctionDecl (CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
-> CxtS NoHole MCSig (K ()) [CAttributeL]
-> CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
-> CxtS NoHole MCSig (K ()) [CAttributeL]
-> CxtS NoHole MCSig (K ()) FunctionDeclAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CFunDeclAttrs :-<: fs, InjF fs FunctionDeclAttrsL j) =>
CxtS h fs a [CDerivedDeclaratorL]
-> CxtS h fs a [CAttributeL]
-> CxtS h fs a (Maybe CStringLiteralL)
-> CxtS h fs a [CAttributeL]
-> CxtS h fs a j
iCFunDeclAttrs (Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
-> CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
dds) (Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
-> CxtS NoHole MCSig (K ()) [CAttributeL]
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs1) (Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
-> CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
asmNm) (Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
-> CxtS NoHole MCSig (K ()) [CAttributeL]
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs2))
                  (CTerm IdentL -> MCTerm IdentL
transIdent CTerm IdentL
n)
                  (case Cxt
  NoHole (Sum CSig) (K ()) (Either [IdentL] ([CDeclarationL], BoolL))
pars of
                    Left' ps :: CTerm [IdentL]
ps                                -> (CTerm IdentL -> MCTerm FunctionParameterDeclL)
-> CTerm [IdentL]
-> CxtS NoHole MCSig (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 CTerm IdentL -> MCTerm FunctionParameterDeclL
paramDeclFromId CTerm [IdentL]
ps
                    Right' (PairF' decls :: Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
decls (BoolF' isVarArg :: Bool
isVarArg)) -> [MCTerm FunctionParameterDeclL]
-> CxtS NoHole MCSig (K ()) [FunctionParameterDeclL]
forall (f :: * -> *) (e :: * -> *) l.
(InsertF f e, Typeable l) =>
f (e l) -> e (f l)
insertF ([MCTerm FunctionParameterDeclL]
 -> CxtS NoHole MCSig (K ()) [FunctionParameterDeclL])
-> [MCTerm FunctionParameterDeclL]
-> CxtS NoHole MCSig (K ()) [FunctionParameterDeclL]
forall a b. (a -> b) -> a -> b
$ ((CTerm CDeclarationL -> MCTerm FunctionParameterDeclL)
-> [CTerm CDeclarationL] -> [MCTerm FunctionParameterDeclL]
forall a b. (a -> b) -> [a] -> [b]
map CTerm CDeclarationL -> MCTerm FunctionParameterDeclL
paramDeclFromDecl ([CTerm CDeclarationL] -> [MCTerm FunctionParameterDeclL])
-> [CTerm CDeclarationL] -> [MCTerm FunctionParameterDeclL]
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
-> [CTerm CDeclarationL]
forall (f :: * -> *) (e :: * -> *) l.
ExtractF f e =>
e (f l) -> f (e l)
extractF Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
decls) [MCTerm FunctionParameterDeclL]
-> [MCTerm FunctionParameterDeclL]
-> [MCTerm FunctionParameterDeclL]
forall a. [a] -> [a] -> [a]
++ (if Bool
isVarArg then [MCTerm FunctionParameterDeclL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CVarArgParam :-<: fs, InjF fs CSpecialParamL j) =>
CxtS h fs a j
iCVarArgParam] else []))
  trans t :: CDeclarator CTerm l
t = CDeclarator CTerm l -> MCTerm l
forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: MCSig, f :-<: CSig) =>
f CTerm l -> MCTerm l
transDefault CDeclarator CTerm l
t

-- Duplication is better than the wrong abstraction
-- Problem here is that I don't really know how to abstract these overlapping trees.
-- I think the solution is going to be some way to "partially merge" the param decl/param hierarchies
paramFromDecl :: F.CTerm F.CDeclarationL -> MCTerm FunctionParameterL
paramFromDecl :: CTerm CDeclarationL -> MCTerm FunctionParameterL
paramFromDecl (CTerm CDeclarationL -> Maybe (CDeclaration CTerm CDeclarationL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CDecl (SingletonF' (Cxt NoHole (Sum CSig) (K ()) CDeclarationSpecifierL
-> Maybe (CDeclarationSpecifier CTerm CDeclarationSpecifierL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CTypeSpec (Cxt NoHole (Sum CSig) (K ()) CTypeSpecifierL
-> Maybe (CTypeSpecifier CTerm CTypeSpecifierL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CVoidType _))))) NilF' _)) = MCTerm FunctionParameterL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CVoidArg :-<: fs, InjF fs CSpecialParamL j) =>
CxtS h fs a j
iCVoidArg
paramFromDecl (CTerm CDeclarationL -> Maybe (CDeclaration CTerm CDeclarationL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CDecl dss :: CTerm [CDeclarationSpecifierL]
dss (SingletonF' (TripleF' declOpt :: Cxt NoHole (Sum CSig) (K ()) (Maybe CDeclaratorL)
declOpt Nothing' Nothing')) _)) =
  case Cxt NoHole (Sum CSig) (K ()) (Maybe CDeclaratorL)
declOpt of
    Nothing' -> String -> MCTerm FunctionParameterL
forall a. HasCallStack => String -> a
error "Unnamed parameter in function definition"
    Just' (Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
-> Maybe (CDeclarator CTerm CDeclaratorL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CDeclr (Just' n :: CTerm IdentL
n) dds :: Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
dds asmNm :: Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
asmNm attrs :: Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs _)) ->
                CxtS NoHole MCSig (K ()) ParameterAttrsL
-> MCTerm IdentL -> MCTerm FunctionParameterL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(PositionalParameter :-<: fs, All HFunctor fs) =>
CxtS h fs a ParameterAttrsL
-> CxtS h fs a IdentL -> CxtS h fs a FunctionParameterL
PositionalParameter' (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
-> CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
-> CxtS NoHole MCSig (K ()) [CAttributeL]
-> CxtS NoHole MCSig (K ()) ParameterAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CFunParamAttrs :-<: fs, InjF fs CFunParamAttrsL j) =>
CxtS h fs a [CDeclarationSpecifierL]
-> CxtS h fs a [CDerivedDeclaratorL]
-> CxtS h fs a (Maybe CStringLiteralL)
-> CxtS h fs a [CAttributeL]
-> CxtS h fs a j
iCFunParamAttrs (CTerm [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
forall l. CTerm l -> MCTerm l
translate CTerm [CDeclarationSpecifierL]
dss) (Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
-> CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
dds) (Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
-> CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
asmNm) (Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
-> CxtS NoHole MCSig (K ()) [CAttributeL]
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs)) (CTerm IdentL -> MCTerm IdentL
transIdent CTerm IdentL
n)

instance {-# OVERLAPPING #-} Trans F.CFunctionDef where
  trans :: CFunctionDef CTerm l -> MCTerm l
trans (F.CFunDef dss :: CTerm [CDeclarationSpecifierL]
dss (Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
-> Maybe (CDeclarator CTerm CDeclaratorL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CDeclr (Just' n :: CTerm IdentL
n)
                                                  (ConsF' (Cxt NoHole (Sum CSig) (K ()) CDerivedDeclaratorL
-> Maybe (CDerivedDeclarator CTerm CDerivedDeclaratorL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CFunDeclr pars :: Cxt
  NoHole (Sum CSig) (K ()) (Either [IdentL] ([CDeclarationL], BoolL))
pars attrs1 :: Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs1 _)) dds :: Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
dds)
                                                  asmNm :: Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
asmNm attrs2 :: Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs2 _))
                   oldStyleDecls :: Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
oldStyleDecls body :: CTerm CStatementL
body _) =
      CxtS NoHole MCSig (K ()) FunctionDefAttrsL
-> MCTerm IdentL
-> CxtS NoHole MCSig (K ()) [FunctionParameterL]
-> CxtS NoHole MCSig (K ()) FunctionBodyL
-> MCTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(FunctionDef :-<: fs, InjF fs FunctionDefL j) =>
CxtS h fs a FunctionDefAttrsL
-> CxtS h fs a IdentL
-> CxtS h fs a [FunctionParameterL]
-> CxtS h fs a FunctionBodyL
-> CxtS h fs a j
iFunctionDef (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) FunctionDeclAttrsL
-> CxtS NoHole MCSig (K ()) [CDeclarationL]
-> CxtS NoHole MCSig (K ()) FunctionDefAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CFunDefAttrs :-<: fs, InjF fs FunctionDefAttrsL j) =>
CxtS h fs a [CDeclarationSpecifierL]
-> CxtS h fs a FunctionDeclAttrsL
-> CxtS h fs a [CDeclarationL]
-> CxtS h fs a j
iCFunDefAttrs (CTerm [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
forall l. CTerm l -> MCTerm l
translate CTerm [CDeclarationSpecifierL]
dss)
                                  (CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
-> CxtS NoHole MCSig (K ()) [CAttributeL]
-> CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
-> CxtS NoHole MCSig (K ()) [CAttributeL]
-> CxtS NoHole MCSig (K ()) FunctionDeclAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CFunDeclAttrs :-<: fs, InjF fs FunctionDeclAttrsL j) =>
CxtS h fs a [CDerivedDeclaratorL]
-> CxtS h fs a [CAttributeL]
-> CxtS h fs a (Maybe CStringLiteralL)
-> CxtS h fs a [CAttributeL]
-> CxtS h fs a j
iCFunDeclAttrs (Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
-> CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
dds)
                                                  (Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
-> CxtS NoHole MCSig (K ()) [CAttributeL]
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs1)
                                                  (Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
-> CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
asmNm)
                                                  (Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
-> CxtS NoHole MCSig (K ()) [CAttributeL]
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs2))
                                  (Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
-> CxtS NoHole MCSig (K ()) [CDeclarationL]
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
oldStyleDecls))
                   (CTerm IdentL -> MCTerm IdentL
transIdent CTerm IdentL
n)
                   (case Cxt
  NoHole (Sum CSig) (K ()) (Either [IdentL] ([CDeclarationL], BoolL))
pars of
                     Left' ps :: CTerm [IdentL]
ps -> (CTerm IdentL -> MCTerm FunctionParameterL)
-> CTerm [IdentL] -> CxtS NoHole MCSig (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 (MCTerm IdentL -> MCTerm FunctionParameterL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(COldStyleParam :-<: fs, InjF fs COldStyleParamL j) =>
CxtS h fs a IdentL -> CxtS h fs a j
iCOldStyleParam(MCTerm IdentL -> MCTerm FunctionParameterL)
-> (CTerm IdentL -> MCTerm IdentL)
-> CTerm IdentL
-> MCTerm FunctionParameterL
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CTerm IdentL -> MCTerm IdentL
transIdent) CTerm [IdentL]
ps
                     Right' (PairF' decls :: Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
decls (BoolF' isVarArg :: Bool
isVarArg)) -> [MCTerm FunctionParameterL]
-> CxtS NoHole MCSig (K ()) [FunctionParameterL]
forall (f :: * -> *) (e :: * -> *) l.
(InsertF f e, Typeable l) =>
f (e l) -> e (f l)
insertF ([MCTerm FunctionParameterL]
 -> CxtS NoHole MCSig (K ()) [FunctionParameterL])
-> [MCTerm FunctionParameterL]
-> CxtS NoHole MCSig (K ()) [FunctionParameterL]
forall a b. (a -> b) -> a -> b
$ ((CTerm CDeclarationL -> MCTerm FunctionParameterL)
-> [CTerm CDeclarationL] -> [MCTerm FunctionParameterL]
forall a b. (a -> b) -> [a] -> [b]
map CTerm CDeclarationL -> MCTerm FunctionParameterL
paramFromDecl ([CTerm CDeclarationL] -> [MCTerm FunctionParameterL])
-> [CTerm CDeclarationL] -> [MCTerm FunctionParameterL]
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
-> [CTerm CDeclarationL]
forall (f :: * -> *) (e :: * -> *) l.
ExtractF f e =>
e (f l) -> f (e l)
extractF Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
decls) [MCTerm FunctionParameterL]
-> [MCTerm FunctionParameterL] -> [MCTerm FunctionParameterL]
forall a. [a] -> [a] -> [a]
++ (if Bool
isVarArg then [MCTerm FunctionParameterL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CVarArgParam :-<: fs, InjF fs CSpecialParamL j) =>
CxtS h fs a j
iCVarArgParam] else []))
                   (CxtS NoHole MCSig (K ()) CStatementL
-> CxtS NoHole MCSig (K ()) FunctionBodyL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF (CxtS NoHole MCSig (K ()) CStatementL
 -> CxtS NoHole MCSig (K ()) FunctionBodyL)
-> CxtS NoHole MCSig (K ()) CStatementL
-> CxtS NoHole MCSig (K ()) FunctionBodyL
forall a b. (a -> b) -> a -> b
$ CTerm CStatementL -> CxtS NoHole MCSig (K ()) CStatementL
forall l. CTerm l -> MCTerm l
translate CTerm CStatementL
body)

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

class Untrans f where
  untrans :: f MCTerm l -> F.CTerm l

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

untransDefault :: (HFunctor f, f :-<: F.CSig) => f MCTerm l -> F.CTerm l
untransDefault :: f (Cxt NoHole (Sum MCSig) (K ())) l -> CTerm l
untransDefault = f CTerm l -> CTerm l
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (f CTerm l -> CTerm l)
-> (f (Cxt NoHole (Sum MCSig) (K ())) l -> f CTerm l)
-> f (Cxt NoHole (Sum MCSig) (K ())) l
-> CTerm l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Cxt NoHole (Sum MCSig) (K ()) :-> CTerm)
-> f (Cxt NoHole (Sum MCSig) (K ())) :-> f CTerm
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate

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

dummyNodeInfo :: F.CTerm F.NodeInfoL
dummyNodeInfo :: CTerm NodeInfoL
dummyNodeInfo = NodeInfo -> CTerm NodeInfoL
F.translateNodeInfo (NodeInfo -> CTerm NodeInfoL) -> NodeInfo -> CTerm NodeInfoL
forall a b. (a -> b) -> a -> b
$ Position -> NodeInfo
COrig.mkNodeInfoOnlyPos Position
COrig.nopos

untransIdent :: MCTerm IdentL -> F.CTerm F.IdentL
untransIdent :: MCTerm IdentL -> CTerm IdentL
untransIdent (Ident' s :: String
s) = String -> Int -> CTerm NodeInfoL -> CTerm IdentL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(Ident :-<: fs, InjF fs IdentL j) =>
String -> Int -> CxtS h fs a NodeInfoL -> CxtS h fs a j
F.iIdent String
s 0 CTerm NodeInfoL
dummyNodeInfo

instance {-# OVERLAPPING #-} Untrans IdentIsIdent where
  untrans :: IdentIsIdent (Cxt NoHole (Sum MCSig) (K ())) l -> CTerm l
untrans (IdentIsIdent n :: MCTerm IdentL
n) = MCTerm IdentL -> CTerm IdentL
untransIdent MCTerm IdentL
n

untransSingleDec :: MCTerm SingleLocalVarDeclL -> F.CTerm (Maybe F.CDeclaratorL, Maybe F.CInitializerL, Maybe F.CExpressionL)
untransSingleDec :: MCTerm SingleLocalVarDeclL
-> CTerm
     (Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)
untransSingleDec (SingleLocalVarDecl' attrs :: CxtS NoHole MCSig (K ()) LocalVarDeclAttrsL
attrs id :: CxtS NoHole MCSig (K ()) VarDeclBinderL
id init :: CxtS NoHole MCSig (K ()) OptLocalVarInitL
init) = Cxt NoHole (Sum CSig) (K ()) (Maybe CDeclaratorL)
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CInitializerL)
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
-> CTerm
     (Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)
forall (f :: (* -> *) -> * -> *) i j k h (a :: * -> *).
(TripleF :<: f, Typeable i, Typeable j, Typeable k) =>
Cxt h f a i -> Cxt h f a j -> Cxt h f a k -> Cxt h f a (i, j, k)
riTripleF (Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CDeclaratorL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a (Maybe l)
Just' Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
declarator) Cxt NoHole (Sum CSig) (K ()) (Maybe CInitializerL)
cinit Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a (Maybe l)
Nothing'
  where
    Just (CLocalVarAttrs decs asmName cAttrs) = CxtS NoHole MCSig (K ()) LocalVarDeclAttrsL
-> Maybe
     (CLocalVarAttrs (Cxt NoHole (Sum MCSig) (K ())) LocalVarDeclAttrsL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project CxtS NoHole MCSig (K ()) LocalVarDeclAttrsL
attrs

    declarator :: Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
declarator = Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL)
-> Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
-> Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
-> CxtS NoHole CSig (K ()) ()
-> Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CDeclarator :-<: fs, InjF fs CDeclaratorL j) =>
CxtS h fs a (Maybe IdentL)
-> CxtS h fs a [CDerivedDeclaratorL]
-> CxtS h fs a (Maybe CStringLiteralL)
-> CxtS h fs a [CAttributeL]
-> CxtS h fs a ()
-> CxtS h fs a j
F.iCDeclr (CTerm IdentL -> Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a (Maybe l)
Just' (CTerm IdentL -> Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL))
-> CTerm IdentL -> Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL)
forall a b. (a -> b) -> a -> b
$ MCTerm IdentL -> CTerm IdentL
untransIdent (MCTerm IdentL -> CTerm IdentL) -> MCTerm IdentL -> CTerm IdentL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MCSig (K ()) VarDeclBinderL -> MCTerm IdentL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF CxtS NoHole MCSig (K ()) VarDeclBinderL
id) (CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
-> Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
decs) (CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
asmName) (CxtS NoHole MCSig (K ()) [CAttributeL]
-> Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) [CAttributeL]
cAttrs) CxtS NoHole CSig (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF

    cinit :: Cxt NoHole (Sum CSig) (K ()) (Maybe CInitializerL)
cinit = case CxtS NoHole MCSig (K ()) OptLocalVarInitL
init of
      NoLocalVarInit'     -> Cxt NoHole (Sum CSig) (K ()) (Maybe CInitializerL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a (Maybe l)
Nothing'
      JustLocalVarInit' x :: CxtS NoHole MCSig (K ()) LocalVarInitL
x -> Cxt NoHole (Sum CSig) (K ()) CInitializerL
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CInitializerL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a (Maybe l)
Just' (Cxt NoHole (Sum CSig) (K ()) CInitializerL
 -> Cxt NoHole (Sum CSig) (K ()) (Maybe CInitializerL))
-> Cxt NoHole (Sum CSig) (K ()) CInitializerL
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CInitializerL)
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MCSig (K ()) CInitializerL
-> Cxt NoHole (Sum CSig) (K ()) CInitializerL
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate (CxtS NoHole MCSig (K ()) CInitializerL
 -> Cxt NoHole (Sum CSig) (K ()) CInitializerL)
-> CxtS NoHole MCSig (K ()) CInitializerL
-> Cxt NoHole (Sum CSig) (K ()) CInitializerL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MCSig (K ()) LocalVarInitL
-> CxtS NoHole MCSig (K ()) CInitializerL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF CxtS NoHole MCSig (K ()) LocalVarInitL
x

instance {-# OVERLAPPING #-} Untrans MultiLocalVarDeclIsCCompoundBlockItem where
  untrans :: MultiLocalVarDeclIsCCompoundBlockItem
  (Cxt NoHole (Sum MCSig) (K ())) l
-> CTerm l
untrans (MultiLocalVarDeclIsCCompoundBlockItem (MultiLocalVarDecl' attrs :: CxtS NoHole MCSig (K ()) MultiLocalVarDeclCommonAttrsL
attrs decls :: CxtS NoHole MCSig (K ()) [SingleLocalVarDeclL]
decls)) = CTerm l
decl
    where
      decl :: CTerm l
decl = CTerm CDeclarationL -> CTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CCompoundBlockItem :-<: fs, InjF fs CCompoundBlockItemL j) =>
CxtS h fs a CDeclarationL -> CxtS h fs a j
F.iCBlockDecl CTerm CDeclarationL
declaration
      declaration :: CTerm CDeclarationL
declaration = CTerm [CDeclarationSpecifierL]
-> Cxt
     NoHole
     (Sum CSig)
     (K ())
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> CxtS NoHole CSig (K ()) ()
-> CTerm CDeclarationL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CDeclaration :-<: fs, InjF fs CDeclarationL j) =>
CxtS h fs a [CDeclarationSpecifierL]
-> CxtS
     h
     fs
     a
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> CxtS h fs a ()
-> CxtS h fs a j
F.iCDecl (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> CTerm [CDeclarationSpecifierL]
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
 -> CTerm [CDeclarationSpecifierL])
-> CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> CTerm [CDeclarationSpecifierL]
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MCSig (K ()) MultiLocalVarDeclCommonAttrsL
-> CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF CxtS NoHole MCSig (K ()) MultiLocalVarDeclCommonAttrsL
attrs) ((MCTerm SingleLocalVarDeclL
 -> CTerm
      (Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL))
-> CxtS NoHole MCSig (K ()) [SingleLocalVarDeclL]
-> Cxt
     NoHole
     (Sum CSig)
     (K ())
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
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 MCTerm SingleLocalVarDeclL
-> CTerm
     (Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)
untransSingleDec CxtS NoHole MCSig (K ()) [SingleLocalVarDeclL]
decls) CxtS NoHole CSig (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF

untransOp :: MCTerm AssignOpL -> F.CTerm F.CAssignOpL
untransOp :: MCTerm AssignOpL -> CTerm CAssignOpL
untransOp AssignOpEquals' = CTerm CAssignOpL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CAssignOp :-<: fs, InjF fs CAssignOpL j) =>
CxtS h fs a j
F.iCAssignOp
untransOp x :: MCTerm AssignOpL
x               = CxtS NoHole MCSig (K ()) CAssignOpL -> CTerm CAssignOpL
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate (CxtS NoHole MCSig (K ()) CAssignOpL -> CTerm CAssignOpL)
-> CxtS NoHole MCSig (K ()) CAssignOpL -> CTerm CAssignOpL
forall a b. (a -> b) -> a -> b
$ MCTerm AssignOpL -> CxtS NoHole MCSig (K ()) CAssignOpL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF MCTerm AssignOpL
x

instance {-# OVERLAPPING #-} Untrans AssignIsCExpression where
  untrans :: AssignIsCExpression (Cxt NoHole (Sum MCSig) (K ())) l -> CTerm l
untrans (AssignIsCExpression (Assign' lhs :: CxtS NoHole MCSig (K ()) LhsL
lhs op :: MCTerm AssignOpL
op rhs :: CxtS NoHole MCSig (K ()) RhsL
rhs)) = CTerm CAssignOpL
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
-> CxtS NoHole CSig (K ()) ()
-> CTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CExpression :-<: fs, InjF fs CExpressionL j) =>
CxtS h fs a CAssignOpL
-> CxtS h fs a CExpressionL
-> CxtS h fs a CExpressionL
-> CxtS h fs a ()
-> CxtS h fs a j
F.iCAssign (MCTerm AssignOpL -> CTerm CAssignOpL
untransOp MCTerm AssignOpL
op) (CxtS NoHole MCSig (K ()) CExpressionL
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate (CxtS NoHole MCSig (K ()) CExpressionL
 -> Cxt NoHole (Sum CSig) (K ()) CExpressionL)
-> CxtS NoHole MCSig (K ()) CExpressionL
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MCSig (K ()) LhsL
-> CxtS NoHole MCSig (K ()) CExpressionL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF CxtS NoHole MCSig (K ()) LhsL
lhs)  (CxtS NoHole MCSig (K ()) CExpressionL
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate (CxtS NoHole MCSig (K ()) CExpressionL
 -> Cxt NoHole (Sum CSig) (K ()) CExpressionL)
-> CxtS NoHole MCSig (K ()) CExpressionL
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MCSig (K ()) RhsL
-> CxtS NoHole MCSig (K ()) CExpressionL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF CxtS NoHole MCSig (K ()) RhsL
rhs) CxtS NoHole CSig (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF

instance {-# OVERLAPPING #-} Untrans CLabeledBlock where
  untrans :: CLabeledBlock (Cxt NoHole (Sum MCSig) (K ())) l -> CTerm l
untrans (CLabeledBlock ids :: CxtS NoHole MCSig (K ()) [IdentL]
ids (Block' items :: CxtS NoHole MCSig (K ()) [BlockItemL]
items _)) = CTerm [IdentL]
-> CTerm [CCompoundBlockItemL]
-> CxtS NoHole CSig (K ()) ()
-> CTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CStatement :-<: fs, InjF fs CStatementL j) =>
CxtS h fs a [IdentL]
-> CxtS h fs a [CCompoundBlockItemL]
-> CxtS h fs a ()
-> CxtS h fs a j
F.iCCompound ((MCTerm IdentL -> CTerm IdentL)
-> CxtS NoHole MCSig (K ()) [IdentL] -> CTerm [IdentL]
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 MCTerm IdentL -> CTerm IdentL
untransIdent CxtS NoHole MCSig (K ()) [IdentL]
ids) ((Cxt NoHole (Sum MCSig) (K ()) BlockItemL
 -> Cxt NoHole (Sum CSig) (K ()) CCompoundBlockItemL)
-> CxtS NoHole MCSig (K ()) [BlockItemL]
-> CTerm [CCompoundBlockItemL]
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 MCSig (K ()) CCompoundBlockItemL
-> Cxt NoHole (Sum CSig) (K ()) CCompoundBlockItemL
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate(CxtS NoHole MCSig (K ()) CCompoundBlockItemL
 -> Cxt NoHole (Sum CSig) (K ()) CCompoundBlockItemL)
-> (Cxt NoHole (Sum MCSig) (K ()) BlockItemL
    -> CxtS NoHole MCSig (K ()) CCompoundBlockItemL)
-> Cxt NoHole (Sum MCSig) (K ()) BlockItemL
-> Cxt NoHole (Sum CSig) (K ()) CCompoundBlockItemL
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cxt NoHole (Sum MCSig) (K ()) BlockItemL
-> CxtS NoHole MCSig (K ()) CCompoundBlockItemL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF) CxtS NoHole MCSig (K ()) [BlockItemL]
items) CxtS NoHole CSig (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF

untranslateArg :: MCTerm FunctionArgumentL -> F.CTerm F.CExpressionL
untranslateArg :: Cxt NoHole (Sum MCSig) (K ()) FunctionArgumentL
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
untranslateArg (PositionalArgument' a :: CxtS NoHole MCSig (K ()) PositionalArgExpL
a) = CxtS NoHole MCSig (K ()) CExpressionL
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate (CxtS NoHole MCSig (K ()) CExpressionL
 -> Cxt NoHole (Sum CSig) (K ()) CExpressionL)
-> CxtS NoHole MCSig (K ()) CExpressionL
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MCSig (K ()) PositionalArgExpL
-> CxtS NoHole MCSig (K ()) CExpressionL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF CxtS NoHole MCSig (K ()) PositionalArgExpL
a

instance {-# OVERLAPPING #-} Untrans FunctionCallIsCExpression where
  untrans :: FunctionCallIsCExpression (Cxt NoHole (Sum MCSig) (K ())) l
-> CTerm l
untrans (FunctionCallIsCExpression (FunctionCall' EmptyFunctionCallAttrs' f :: CxtS NoHole MCSig (K ()) FunctionExpL
f (FunctionArgumentList' args :: CxtS NoHole MCSig (K ()) [FunctionArgumentL]
args))) = Cxt NoHole (Sum CSig) (K ()) CExpressionL
-> CTerm [CExpressionL] -> CxtS NoHole CSig (K ()) () -> CTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CExpression :-<: fs, InjF fs CExpressionL j) =>
CxtS h fs a CExpressionL
-> CxtS h fs a [CExpressionL] -> CxtS h fs a () -> CxtS h fs a j
F.iCCall (CxtS NoHole MCSig (K ()) CExpressionL
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate (CxtS NoHole MCSig (K ()) CExpressionL
 -> Cxt NoHole (Sum CSig) (K ()) CExpressionL)
-> CxtS NoHole MCSig (K ()) CExpressionL
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MCSig (K ()) FunctionExpL
-> CxtS NoHole MCSig (K ()) CExpressionL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF CxtS NoHole MCSig (K ()) FunctionExpL
f) ((Cxt NoHole (Sum MCSig) (K ()) FunctionArgumentL
 -> Cxt NoHole (Sum CSig) (K ()) CExpressionL)
-> CxtS NoHole MCSig (K ()) [FunctionArgumentL]
-> CTerm [CExpressionL]
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 Cxt NoHole (Sum MCSig) (K ()) FunctionArgumentL
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
untranslateArg CxtS NoHole MCSig (K ()) [FunctionArgumentL]
args) CxtS NoHole CSig (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF

instance {-# OVERLAPPING #-} Untrans FunctionDeclIsCDeclarator where
  untrans :: FunctionDeclIsCDeclarator (Cxt NoHole (Sum MCSig) (K ())) l
-> CTerm l
untrans (FunctionDeclIsCDeclarator (FunctionDecl' (CFunDeclAttrs' dds :: CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
dds attrs1 :: CxtS NoHole MCSig (K ()) [CAttributeL]
attrs1 asmNm :: CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
asmNm attrs2 :: CxtS NoHole MCSig (K ()) [CAttributeL]
attrs2) n :: MCTerm IdentL
n pars :: CxtS NoHole MCSig (K ()) [FunctionParameterDeclL]
pars)) =
      Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL)
-> Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
-> Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
-> CxtS NoHole CSig (K ()) ()
-> CTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CDeclarator :-<: fs, InjF fs CDeclaratorL j) =>
CxtS h fs a (Maybe IdentL)
-> CxtS h fs a [CDerivedDeclaratorL]
-> CxtS h fs a (Maybe CStringLiteralL)
-> CxtS h fs a [CAttributeL]
-> CxtS h fs a ()
-> CxtS h fs a j
F.iCDeclr (CTerm IdentL -> Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a (Maybe l)
Just' (CTerm IdentL -> Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL))
-> CTerm IdentL -> Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL)
forall a b. (a -> b) -> a -> b
$ MCTerm IdentL -> CTerm IdentL
untransIdent MCTerm IdentL
n) (Cxt NoHole (Sum CSig) (K ()) CDerivedDeclaratorL
-> Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
-> Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a [l] -> Cxt h f a [l]
ConsF' (Cxt
  NoHole (Sum CSig) (K ()) (Either [IdentL] ([CDeclarationL], BoolL))
-> Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
-> CxtS NoHole CSig (K ()) ()
-> Cxt NoHole (Sum CSig) (K ()) CDerivedDeclaratorL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CDerivedDeclarator :-<: fs, InjF fs CDerivedDeclaratorL j) =>
CxtS h fs a (Either [IdentL] ([CDeclarationL], BoolL))
-> CxtS h fs a [CAttributeL] -> CxtS h fs a () -> CxtS h fs a j
F.iCFunDeclr (Cxt NoHole (Sum CSig) (K ()) ([CDeclarationL], BoolL)
-> Cxt
     NoHole (Sum CSig) (K ()) (Either [IdentL] ([CDeclarationL], BoolL))
forall (f :: (* -> *) -> * -> *) l l' h (a :: * -> *).
(EitherF :<: f, Typeable l, Typeable l', HFunctor f) =>
Cxt h f a l' -> Cxt h f a (Either l l')
Right' (Cxt NoHole (Sum CSig) (K ()) ([CDeclarationL], BoolL)
 -> Cxt
      NoHole
      (Sum CSig)
      (K ())
      (Either [IdentL] ([CDeclarationL], BoolL)))
-> Cxt NoHole (Sum CSig) (K ()) ([CDeclarationL], BoolL)
-> Cxt
     NoHole (Sum CSig) (K ()) (Either [IdentL] ([CDeclarationL], BoolL))
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MCSig (K ()) [FunctionParameterDeclL]
-> Cxt NoHole (Sum CSig) (K ()) ([CDeclarationL], BoolL)
untransPars CxtS NoHole MCSig (K ()) [FunctionParameterDeclL]
pars) (CxtS NoHole MCSig (K ()) [CAttributeL]
-> Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) [CAttributeL]
attrs1) CxtS NoHole CSig (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF) (CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
-> Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
dds)) (CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
asmNm) (CxtS NoHole MCSig (K ()) [CAttributeL]
-> Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) [CAttributeL]
attrs2) CxtS NoHole CSig (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF
    where
      untransPars :: MCTerm [FunctionParameterDeclL] -> F.CTerm ([F.CDeclarationL], BoolL)
      untransPars :: CxtS NoHole MCSig (K ()) [FunctionParameterDeclL]
-> Cxt NoHole (Sum CSig) (K ()) ([CDeclarationL], BoolL)
untransPars t :: CxtS NoHole MCSig (K ()) [FunctionParameterDeclL]
t = let (ds :: [CTerm CDeclarationL]
ds, b :: Bool
b) = [MCTerm FunctionParameterDeclL]
-> ([CTerm CDeclarationL], Bool) -> ([CTerm CDeclarationL], Bool)
go (CxtS NoHole MCSig (K ()) [FunctionParameterDeclL]
-> [MCTerm FunctionParameterDeclL]
forall (f :: * -> *) (e :: * -> *) l.
ExtractF f e =>
e (f l) -> f (e l)
extractF CxtS NoHole MCSig (K ()) [FunctionParameterDeclL]
t) ([], Bool
False) in Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
-> CxtS NoHole CSig (K ()) BoolL
-> Cxt NoHole (Sum CSig) (K ()) ([CDeclarationL], BoolL)
forall (f :: (* -> *) -> * -> *) l l' h (a :: * -> *).
(PairF :<: f, Typeable l, Typeable l', HFunctor f) =>
Cxt h f a l -> Cxt h f a l' -> Cxt h f a (l, l')
PairF' ([CTerm CDeclarationL]
-> Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
forall (f :: * -> *) (e :: * -> *) l.
(InsertF f e, Typeable l) =>
f (e l) -> e (f l)
insertF ([CTerm CDeclarationL]
 -> Cxt NoHole (Sum CSig) (K ()) [CDeclarationL])
-> [CTerm CDeclarationL]
-> Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
forall a b. (a -> b) -> a -> b
$ [CTerm CDeclarationL] -> [CTerm CDeclarationL]
forall a. [a] -> [a]
reverse [CTerm CDeclarationL]
ds) (Bool -> CxtS NoHole CSig (K ()) BoolL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(BoolF :-<: fs, All HFunctor fs) =>
Bool -> CxtS h fs a BoolL
BoolF' Bool
b)
        where
          go :: [MCTerm FunctionParameterDeclL] -> ([F.CTerm F.CDeclarationL], Bool) -> ([F.CTerm F.CDeclarationL], Bool)
          go :: [MCTerm FunctionParameterDeclL]
-> ([CTerm CDeclarationL], Bool) -> ([CTerm CDeclarationL], Bool)
go ((PositionalParameterDeclOptionalIdent' (CxtS NoHole MCSig (K ()) FunctionParameterDeclAttrsL
-> CxtS NoHole MCSig (K ()) CFunParamAttrsL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF -> (CFunParamAttrs' dss :: CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
dss NilF' Nothing' NilF')) Nothing') : ps :: [MCTerm FunctionParameterDeclL]
ps) (l :: [CTerm CDeclarationL]
l, b :: Bool
b) =
               [MCTerm FunctionParameterDeclL]
-> ([CTerm CDeclarationL], Bool) -> ([CTerm CDeclarationL], Bool)
go [MCTerm FunctionParameterDeclL]
ps (CTerm [CDeclarationSpecifierL]
-> Cxt
     NoHole
     (Sum CSig)
     (K ())
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> CxtS NoHole CSig (K ()) ()
-> CTerm CDeclarationL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CDeclaration :-<: fs, InjF fs CDeclarationL j) =>
CxtS h fs a [CDeclarationSpecifierL]
-> CxtS
     h
     fs
     a
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> CxtS h fs a ()
-> CxtS h fs a j
F.iCDecl (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> CTerm [CDeclarationSpecifierL]
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
dss) Cxt
  NoHole
  (Sum CSig)
  (K ())
  [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a [l]
NilF' CxtS NoHole CSig (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF CTerm CDeclarationL
-> [CTerm CDeclarationL] -> [CTerm CDeclarationL]
forall a. a -> [a] -> [a]
: [CTerm CDeclarationL]
l, Bool
b)
          go ((PositionalParameterDeclOptionalIdent' (CxtS NoHole MCSig (K ()) FunctionParameterDeclAttrsL
-> CxtS NoHole MCSig (K ()) CFunParamAttrsL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF -> (CFunParamAttrs' dss :: CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
dss dds :: CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
dds asmNm :: CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
asmNm attrs :: CxtS NoHole MCSig (K ()) [CAttributeL]
attrs)) nOpt :: CxtS NoHole MCSig (K ()) (Maybe IdentL)
nOpt) : ps :: [MCTerm FunctionParameterDeclL]
ps) (l :: [CTerm CDeclarationL]
l, b :: Bool
b) =
               [MCTerm FunctionParameterDeclL]
-> ([CTerm CDeclarationL], Bool) -> ([CTerm CDeclarationL], Bool)
go [MCTerm FunctionParameterDeclL]
ps ((CTerm [CDeclarationSpecifierL]
-> Cxt
     NoHole
     (Sum CSig)
     (K ())
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> CxtS NoHole CSig (K ()) ()
-> CTerm CDeclarationL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CDeclaration :-<: fs, InjF fs CDeclarationL j) =>
CxtS h fs a [CDeclarationSpecifierL]
-> CxtS
     h
     fs
     a
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> CxtS h fs a ()
-> CxtS h fs a j
F.iCDecl (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> CTerm [CDeclarationSpecifierL]
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
dss) (CTerm (Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)
-> Cxt
     NoHole
     (Sum CSig)
     (K ())
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a [l]
SingletonF' (Cxt NoHole (Sum CSig) (K ()) (Maybe CDeclaratorL)
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CInitializerL)
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
-> CTerm
     (Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)
forall (f :: (* -> *) -> * -> *) i j k h (a :: * -> *).
(TripleF :<: f, Typeable i, Typeable j, Typeable k, HFunctor f) =>
Cxt h f a i -> Cxt h f a j -> Cxt h f a k -> Cxt h f a (i, j, k)
TripleF' (Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CDeclaratorL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a (Maybe l)
Just' (Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
 -> Cxt NoHole (Sum CSig) (K ()) (Maybe CDeclaratorL))
-> Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CDeclaratorL)
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL)
-> Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
-> Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
-> CxtS NoHole CSig (K ()) ()
-> Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CDeclarator :-<: fs, InjF fs CDeclaratorL j) =>
CxtS h fs a (Maybe IdentL)
-> CxtS h fs a [CDerivedDeclaratorL]
-> CxtS h fs a (Maybe CStringLiteralL)
-> CxtS h fs a [CAttributeL]
-> CxtS h fs a ()
-> CxtS h fs a j
F.iCDeclr ((MCTerm IdentL -> CTerm IdentL)
-> CxtS NoHole MCSig (K ()) (Maybe IdentL)
-> Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL)
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 MCTerm IdentL -> CTerm IdentL
untransIdent CxtS NoHole MCSig (K ()) (Maybe IdentL)
nOpt) (CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
-> Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
dds) (CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
asmNm) (CxtS NoHole MCSig (K ()) [CAttributeL]
-> Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) [CAttributeL]
attrs) CxtS NoHole CSig (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF) Cxt NoHole (Sum CSig) (K ()) (Maybe CInitializerL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a (Maybe l)
Nothing' Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a (Maybe l)
Nothing')) CxtS NoHole CSig (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF) CTerm CDeclarationL
-> [CTerm CDeclarationL] -> [CTerm CDeclarationL]
forall a. a -> [a] -> [a]
: [CTerm CDeclarationL]
l, Bool
b)
          go [MCTerm FunctionParameterDeclL
-> CxtS NoHole MCSig (K ()) CSpecialParamL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF -> CxtS NoHole MCSig (K ()) CSpecialParamL
CVoidArg'] ([], b :: Bool
b) = ([CTerm [CDeclarationSpecifierL]
-> Cxt
     NoHole
     (Sum CSig)
     (K ())
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> CxtS NoHole CSig (K ()) ()
-> CTerm CDeclarationL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CDeclaration :-<: fs, InjF fs CDeclarationL j) =>
CxtS h fs a [CDeclarationSpecifierL]
-> CxtS
     h
     fs
     a
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> CxtS h fs a ()
-> CxtS h fs a j
F.iCDecl (Cxt NoHole (Sum CSig) (K ()) CDeclarationSpecifierL
-> CTerm [CDeclarationSpecifierL]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a [l]
SingletonF' (Cxt NoHole (Sum CSig) (K ()) CDeclarationSpecifierL
 -> CTerm [CDeclarationSpecifierL])
-> Cxt NoHole (Sum CSig) (K ()) CDeclarationSpecifierL
-> CTerm [CDeclarationSpecifierL]
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum CSig) (K ()) CTypeSpecifierL
-> Cxt NoHole (Sum CSig) (K ()) CDeclarationSpecifierL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CDeclarationSpecifier :-<: fs,
 InjF fs CDeclarationSpecifierL j) =>
CxtS h fs a CTypeSpecifierL -> CxtS h fs a j
F.iCTypeSpec (CxtS NoHole CSig (K ()) ()
-> Cxt NoHole (Sum CSig) (K ()) CTypeSpecifierL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CTypeSpecifier :-<: fs, InjF fs CTypeSpecifierL j) =>
CxtS h fs a () -> CxtS h fs a j
F.iCVoidType CxtS NoHole CSig (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF)) Cxt
  NoHole
  (Sum CSig)
  (K ())
  [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a [l]
NilF' CxtS NoHole CSig (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF], Bool
False)
          go [MCTerm FunctionParameterDeclL
-> CxtS NoHole MCSig (K ()) CSpecialParamL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF -> CxtS NoHole MCSig (K ()) CSpecialParamL
CVarArgParam'] (l :: [CTerm CDeclarationL]
l, b :: Bool
b) = ([CTerm CDeclarationL]
l, Bool
True)
          go [] (l :: [CTerm CDeclarationL]
l, b :: Bool
b) = ([CTerm CDeclarationL]
l, Bool
b)

instance {-# OVERLAPPING #-} Untrans FunctionDefIsCFunctionDef where
  untrans :: FunctionDefIsCFunctionDef (Cxt NoHole (Sum MCSig) (K ())) l
-> CTerm l
untrans (FunctionDefIsCFunctionDef
              (FunctionDef' (CFunDefAttrs' dss :: CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
dss
                                           (CFunDeclAttrs' dds :: CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
dds attrs1 :: CxtS NoHole MCSig (K ()) [CAttributeL]
attrs1 asmNm :: CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
asmNm attrs2 :: CxtS NoHole MCSig (K ()) [CAttributeL]
attrs2)
                                           oldStyleParams :: CxtS NoHole MCSig (K ()) [CDeclarationL]
oldStyleParams)
                            n :: MCTerm IdentL
n params :: CxtS NoHole MCSig (K ()) [FunctionParameterL]
params body :: CxtS NoHole MCSig (K ()) FunctionBodyL
body)) =
      CTerm [CDeclarationSpecifierL]
-> Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
-> Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
-> CTerm CStatementL
-> CxtS NoHole CSig (K ()) ()
-> CTerm l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CFunctionDef :-<: fs, InjF fs CFunctionDefL j) =>
CxtS h fs a [CDeclarationSpecifierL]
-> CxtS h fs a CDeclaratorL
-> CxtS h fs a [CDeclarationL]
-> CxtS h fs a CStatementL
-> CxtS h fs a ()
-> CxtS h fs a j
F.iCFunDef (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> CTerm [CDeclarationSpecifierL]
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
dss)
                 (Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL)
-> Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
-> Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
-> CxtS NoHole CSig (K ()) ()
-> Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CDeclarator :-<: fs, InjF fs CDeclaratorL j) =>
CxtS h fs a (Maybe IdentL)
-> CxtS h fs a [CDerivedDeclaratorL]
-> CxtS h fs a (Maybe CStringLiteralL)
-> CxtS h fs a [CAttributeL]
-> CxtS h fs a ()
-> CxtS h fs a j
F.iCDeclr (CTerm IdentL -> Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a (Maybe l)
Just' (CTerm IdentL -> Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL))
-> CTerm IdentL -> Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL)
forall a b. (a -> b) -> a -> b
$ MCTerm IdentL -> CTerm IdentL
untransIdent MCTerm IdentL
n)
                            (Cxt NoHole (Sum CSig) (K ()) CDerivedDeclaratorL
-> Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
-> Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a [l] -> Cxt h f a [l]
ConsF' (Cxt
  NoHole (Sum CSig) (K ()) (Either [IdentL] ([CDeclarationL], BoolL))
-> Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
-> CxtS NoHole CSig (K ()) ()
-> Cxt NoHole (Sum CSig) (K ()) CDerivedDeclaratorL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CDerivedDeclarator :-<: fs, InjF fs CDerivedDeclaratorL j) =>
CxtS h fs a (Either [IdentL] ([CDeclarationL], BoolL))
-> CxtS h fs a [CAttributeL] -> CxtS h fs a () -> CxtS h fs a j
F.iCFunDeclr (CxtS NoHole MCSig (K ()) [FunctionParameterL]
-> Cxt
     NoHole (Sum CSig) (K ()) (Either [IdentL] ([CDeclarationL], BoolL))
untransPars CxtS NoHole MCSig (K ()) [FunctionParameterL]
params) (CxtS NoHole MCSig (K ()) [CAttributeL]
-> Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) [CAttributeL]
attrs1) CxtS NoHole CSig (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF)
                                    (CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
-> Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
dds))
                            (CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
asmNm) (CxtS NoHole MCSig (K ()) [CAttributeL]
-> Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) [CAttributeL]
attrs2) CxtS NoHole CSig (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF)
                 (CxtS NoHole MCSig (K ()) [CDeclarationL]
-> Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) [CDeclarationL]
oldStyleParams) (CxtS NoHole MCSig (K ()) CStatementL -> CTerm CStatementL
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate (CxtS NoHole MCSig (K ()) CStatementL -> CTerm CStatementL)
-> CxtS NoHole MCSig (K ()) CStatementL -> CTerm CStatementL
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MCSig (K ()) FunctionBodyL
-> CxtS NoHole MCSig (K ()) CStatementL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF CxtS NoHole MCSig (K ()) FunctionBodyL
body) CxtS NoHole CSig (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF
    where
      untransPars :: MCTerm [FunctionParameterL] -> F.CTerm (Either [F.IdentL] ([F.CDeclarationL], BoolL))
      untransPars :: CxtS NoHole MCSig (K ()) [FunctionParameterL]
-> Cxt
     NoHole (Sum CSig) (K ()) (Either [IdentL] ([CDeclarationL], BoolL))
untransPars t :: CxtS NoHole MCSig (K ()) [FunctionParameterL]
t = case CxtS NoHole MCSig (K ()) [FunctionParameterL]
-> [MCTerm FunctionParameterL]
forall (f :: * -> *) (e :: * -> *) l.
ExtractF f e =>
e (f l) -> f (e l)
extractF CxtS NoHole MCSig (K ()) [FunctionParameterL]
t of
                        [] -> Cxt NoHole (Sum CSig) (K ()) ([CDeclarationL], BoolL)
-> Cxt
     NoHole (Sum CSig) (K ()) (Either [IdentL] ([CDeclarationL], BoolL))
forall (f :: (* -> *) -> * -> *) l l' h (a :: * -> *).
(EitherF :<: f, Typeable l, Typeable l', HFunctor f) =>
Cxt h f a l' -> Cxt h f a (Either l l')
Right' (Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
-> CxtS NoHole CSig (K ()) BoolL
-> Cxt NoHole (Sum CSig) (K ()) ([CDeclarationL], BoolL)
forall (f :: (* -> *) -> * -> *) l l' h (a :: * -> *).
(PairF :<: f, Typeable l, Typeable l', HFunctor f) =>
Cxt h f a l -> Cxt h f a l' -> Cxt h f a (l, l')
PairF' Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a [l]
NilF' (Bool -> CxtS NoHole CSig (K ()) BoolL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(BoolF :-<: fs, All HFunctor fs) =>
Bool -> CxtS h fs a BoolL
BoolF' Bool
False))
                        ns :: [MCTerm FunctionParameterL]
ns@((MCTerm FunctionParameterL
-> Maybe (CxtS NoHole MCSig (K ()) COldStyleParamL)
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> Maybe (CxtS h fs a l)
projF -> Just (COldStyleParam' _)) : _) -> CTerm [IdentL]
-> Cxt
     NoHole (Sum CSig) (K ()) (Either [IdentL] ([CDeclarationL], BoolL))
forall (f :: (* -> *) -> * -> *) l l' h (a :: * -> *).
(EitherF :<: f, Typeable l, Typeable l', HFunctor f) =>
Cxt h f a l -> Cxt h f a (Either l l')
Left' ([CTerm IdentL] -> CTerm [IdentL]
forall (f :: * -> *) (e :: * -> *) l.
(InsertF f e, Typeable l) =>
f (e l) -> e (f l)
insertF ([CTerm IdentL] -> CTerm [IdentL])
-> [CTerm IdentL] -> CTerm [IdentL]
forall a b. (a -> b) -> a -> b
$ (MCTerm FunctionParameterL -> CTerm IdentL)
-> [MCTerm FunctionParameterL] -> [CTerm IdentL]
forall a b. (a -> b) -> [a] -> [b]
map MCTerm FunctionParameterL -> CTerm IdentL
untransOldStyle [MCTerm FunctionParameterL]
ns)
                        ns :: [MCTerm FunctionParameterL]
ns@([MCTerm FunctionParameterL
-> Maybe (CxtS NoHole MCSig (K ()) CSpecialParamL)
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> Maybe (CxtS h fs a l)
projF -> Just CVoidArg']) -> Cxt NoHole (Sum CSig) (K ()) ([CDeclarationL], BoolL)
-> Cxt
     NoHole (Sum CSig) (K ()) (Either [IdentL] ([CDeclarationL], BoolL))
forall (f :: (* -> *) -> * -> *) l l' h (a :: * -> *).
(EitherF :<: f, Typeable l, Typeable l', HFunctor f) =>
Cxt h f a l' -> Cxt h f a (Either l l')
Right' (Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
-> CxtS NoHole CSig (K ()) BoolL
-> Cxt NoHole (Sum CSig) (K ()) ([CDeclarationL], BoolL)
forall (f :: (* -> *) -> * -> *) l l' h (a :: * -> *).
(PairF :<: f, Typeable l, Typeable l', HFunctor f) =>
Cxt h f a l -> Cxt h f a l' -> Cxt h f a (l, l')
PairF' (CTerm CDeclarationL -> Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a [l]
SingletonF' (CTerm CDeclarationL
 -> Cxt NoHole (Sum CSig) (K ()) [CDeclarationL])
-> CTerm CDeclarationL
-> Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
forall a b. (a -> b) -> a -> b
$ CTerm [CDeclarationSpecifierL]
-> Cxt
     NoHole
     (Sum CSig)
     (K ())
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> CxtS NoHole CSig (K ()) ()
-> CTerm CDeclarationL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CDeclaration :-<: fs, InjF fs CDeclarationL j) =>
CxtS h fs a [CDeclarationSpecifierL]
-> CxtS
     h
     fs
     a
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> CxtS h fs a ()
-> CxtS h fs a j
F.iCDecl (Cxt NoHole (Sum CSig) (K ()) CDeclarationSpecifierL
-> CTerm [CDeclarationSpecifierL]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a [l]
SingletonF' (Cxt NoHole (Sum CSig) (K ()) CDeclarationSpecifierL
 -> CTerm [CDeclarationSpecifierL])
-> Cxt NoHole (Sum CSig) (K ()) CDeclarationSpecifierL
-> CTerm [CDeclarationSpecifierL]
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum CSig) (K ()) CTypeSpecifierL
-> Cxt NoHole (Sum CSig) (K ()) CDeclarationSpecifierL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CDeclarationSpecifier :-<: fs,
 InjF fs CDeclarationSpecifierL j) =>
CxtS h fs a CTypeSpecifierL -> CxtS h fs a j
F.iCTypeSpec (CxtS NoHole CSig (K ()) ()
-> Cxt NoHole (Sum CSig) (K ()) CTypeSpecifierL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CTypeSpecifier :-<: fs, InjF fs CTypeSpecifierL j) =>
CxtS h fs a () -> CxtS h fs a j
F.iCVoidType CxtS NoHole CSig (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF)) Cxt
  NoHole
  (Sum CSig)
  (K ())
  [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a [l]
NilF' CxtS NoHole CSig (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF) (Bool -> CxtS NoHole CSig (K ()) BoolL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(BoolF :-<: fs, All HFunctor fs) =>
Bool -> CxtS h fs a BoolL
BoolF' Bool
False))
                        ps :: [MCTerm FunctionParameterL]
ps -> let (ds :: [CTerm CDeclarationL]
ds, b :: Bool
b) = [MCTerm FunctionParameterL]
-> ([CTerm CDeclarationL], Bool) -> ([CTerm CDeclarationL], Bool)
go (CxtS NoHole MCSig (K ()) [FunctionParameterL]
-> [MCTerm FunctionParameterL]
forall (f :: * -> *) (e :: * -> *) l.
ExtractF f e =>
e (f l) -> f (e l)
extractF CxtS NoHole MCSig (K ()) [FunctionParameterL]
t) ([], Bool
False) in Cxt NoHole (Sum CSig) (K ()) ([CDeclarationL], BoolL)
-> Cxt
     NoHole (Sum CSig) (K ()) (Either [IdentL] ([CDeclarationL], BoolL))
forall (f :: (* -> *) -> * -> *) l l' h (a :: * -> *).
(EitherF :<: f, Typeable l, Typeable l', HFunctor f) =>
Cxt h f a l' -> Cxt h f a (Either l l')
Right' (Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
-> CxtS NoHole CSig (K ()) BoolL
-> Cxt NoHole (Sum CSig) (K ()) ([CDeclarationL], BoolL)
forall (f :: (* -> *) -> * -> *) l l' h (a :: * -> *).
(PairF :<: f, Typeable l, Typeable l', HFunctor f) =>
Cxt h f a l -> Cxt h f a l' -> Cxt h f a (l, l')
PairF' ([CTerm CDeclarationL]
-> Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
forall (f :: * -> *) (e :: * -> *) l.
(InsertF f e, Typeable l) =>
f (e l) -> e (f l)
insertF ([CTerm CDeclarationL]
 -> Cxt NoHole (Sum CSig) (K ()) [CDeclarationL])
-> [CTerm CDeclarationL]
-> Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
forall a b. (a -> b) -> a -> b
$ [CTerm CDeclarationL] -> [CTerm CDeclarationL]
forall a. [a] -> [a]
reverse [CTerm CDeclarationL]
ds) (Bool -> CxtS NoHole CSig (K ()) BoolL
forall (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(BoolF :-<: fs, All HFunctor fs) =>
Bool -> CxtS h fs a BoolL
BoolF' Bool
b))
        where
          untransOldStyle :: MCTerm FunctionParameterL -> F.CTerm F.IdentL
          untransOldStyle :: MCTerm FunctionParameterL -> CTerm IdentL
untransOldStyle (MCTerm FunctionParameterL
-> CxtS NoHole MCSig (K ()) COldStyleParamL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF -> COldStyleParam' n :: MCTerm IdentL
n) = MCTerm IdentL -> CTerm IdentL
untransIdent MCTerm IdentL
n

          go :: [MCTerm FunctionParameterL] -> ([F.CTerm F.CDeclarationL], Bool) -> ([F.CTerm F.CDeclarationL], Bool)
          go :: [MCTerm FunctionParameterL]
-> ([CTerm CDeclarationL], Bool) -> ([CTerm CDeclarationL], Bool)
go ((PositionalParameter' (CxtS NoHole MCSig (K ()) ParameterAttrsL
-> CxtS NoHole MCSig (K ()) CFunParamAttrsL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF -> (CFunParamAttrs' dss :: CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
dss dds :: CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
dds asmNm :: CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
asmNm attrs :: CxtS NoHole MCSig (K ()) [CAttributeL]
attrs)) n :: MCTerm IdentL
n) : ps :: [MCTerm FunctionParameterL]
ps) (l :: [CTerm CDeclarationL]
l, b :: Bool
b) =
               [MCTerm FunctionParameterL]
-> ([CTerm CDeclarationL], Bool) -> ([CTerm CDeclarationL], Bool)
go [MCTerm FunctionParameterL]
ps ((CTerm [CDeclarationSpecifierL]
-> Cxt
     NoHole
     (Sum CSig)
     (K ())
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> CxtS NoHole CSig (K ()) ()
-> CTerm CDeclarationL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CDeclaration :-<: fs, InjF fs CDeclarationL j) =>
CxtS h fs a [CDeclarationSpecifierL]
-> CxtS
     h
     fs
     a
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> CxtS h fs a ()
-> CxtS h fs a j
F.iCDecl (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> CTerm [CDeclarationSpecifierL]
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
dss) (CTerm (Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)
-> Cxt
     NoHole
     (Sum CSig)
     (K ())
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a [l]
SingletonF' (Cxt NoHole (Sum CSig) (K ()) (Maybe CDeclaratorL)
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CInitializerL)
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
-> CTerm
     (Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)
forall (f :: (* -> *) -> * -> *) i j k h (a :: * -> *).
(TripleF :<: f, Typeable i, Typeable j, Typeable k, HFunctor f) =>
Cxt h f a i -> Cxt h f a j -> Cxt h f a k -> Cxt h f a (i, j, k)
TripleF' (Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CDeclaratorL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a (Maybe l)
Just' (Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
 -> Cxt NoHole (Sum CSig) (K ()) (Maybe CDeclaratorL))
-> Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CDeclaratorL)
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL)
-> Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
-> Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
-> CxtS NoHole CSig (K ()) ()
-> Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CDeclarator :-<: fs, InjF fs CDeclaratorL j) =>
CxtS h fs a (Maybe IdentL)
-> CxtS h fs a [CDerivedDeclaratorL]
-> CxtS h fs a (Maybe CStringLiteralL)
-> CxtS h fs a [CAttributeL]
-> CxtS h fs a ()
-> CxtS h fs a j
F.iCDeclr (CTerm IdentL -> Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a (Maybe l)
Just' (CTerm IdentL -> Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL))
-> CTerm IdentL -> Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL)
forall a b. (a -> b) -> a -> b
$ MCTerm IdentL -> CTerm IdentL
untransIdent MCTerm IdentL
n) (CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
-> Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
dds) (CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
asmNm) (CxtS NoHole MCSig (K ()) [CAttributeL]
-> Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
Cxt NoHole (Sum MCSig) (K ()) :-> CTerm
untranslate CxtS NoHole MCSig (K ()) [CAttributeL]
attrs) CxtS NoHole CSig (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF) Cxt NoHole (Sum CSig) (K ()) (Maybe CInitializerL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a (Maybe l)
Nothing' Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a (Maybe l)
Nothing')) CxtS NoHole CSig (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF) CTerm CDeclarationL
-> [CTerm CDeclarationL] -> [CTerm CDeclarationL]
forall a. a -> [a] -> [a]
: [CTerm CDeclarationL]
l, Bool
b)
          go [MCTerm FunctionParameterL
-> CxtS NoHole MCSig (K ()) CSpecialParamL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> CxtS h fs a l
fromProjF -> CxtS NoHole MCSig (K ()) CSpecialParamL
CVarArgParam'] (l :: [CTerm CDeclarationL]
l, b :: Bool
b) = ([CTerm CDeclarationL]
l, Bool
True)
          go [] (l :: [CTerm CDeclarationL]
l, b :: Bool
b) = ([CTerm CDeclarationL]
l, Bool
b)

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

do ipsNames <- sumToNames ''MCSig
   modNames <- sumToNames ''F.CSig
   let targTs = map ConT $ (ipsNames \\ modNames) \\ [ ''CLabeledBlock, ''AssignIsCExpression, ''MultiLocalVarDeclIsCCompoundBlockItem, ''IdentIsIdent
                                                     , ''FunctionCallIsCExpression, ''FunctionDeclIsCDeclarator, ''FunctionDefIsCFunctionDef]
   return $ makeDefaultInstances targTs ''Untrans 'untrans (VarE 'untransError)

#endif