{-# OPTIONS_HADDOCK hide #-}

{-# LANGUAGE CPP                     #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TemplateHaskell         #-}
{-# 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.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

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


------------------------------------------------------------------------------------
---------------- Forward translation: Modularized syntax to IPS  -------------------
------------------------------------------------------------------------------------

--------------------------------
------------- Top-level translate
--------------------------------

------ Top-level definition

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

translate' :: (InjF MCSig l l') => F.CTerm l -> MCTerm l'
translate' :: forall l l'. InjF MCSig l l' => CTerm l -> MCTerm l'
translate' = CxtS NoHole MCSig (K ()) l -> CxtS NoHole MCSig (K ()) l'
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *). CxtS h MCSig a l -> CxtS h MCSig a l'
injF (CxtS NoHole MCSig (K ()) l -> CxtS NoHole MCSig (K ()) l')
-> (CTerm l -> CxtS NoHole MCSig (K ()) l)
-> CTerm l
-> CxtS NoHole MCSig (K ()) 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

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

------ Default and standard cases

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

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

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

---------------------------------
-------------- Per-fragment Instances
---------------------------------

-------- Identifiers

-- 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 (Cxt NoHole (Sum CSig) (K ())) IdentL)
NatM
  Maybe
  (Cxt NoHole (Sum CSig) (K ()))
  (Ident (Cxt NoHole (Sum CSig) (K ())))
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.Ident String
s Int
_ Cxt NoHole (Sum CSig) (K ()) NodeInfoL
_)) = String -> MCTerm IdentL
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) j.
(Ident :<: f) =>
String -> Cxt h f a IdentL
Ident' String
s

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

-------- Declarations

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

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

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

-------- Labeled blocks

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) (Cxt NoHole (Sum CSig) (K ())) Any
-> GTranslateM Identity (Cxt NoHole (Sum CSig) (K ())) 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) (Cxt NoHole (Sum CSig) (K ())) Any
 -> GTranslateM Identity (Cxt NoHole (Sum CSig) (K ())) Any)
-> GTranslateM (MaybeT Identity) (Cxt NoHole (Sum CSig) (K ())) Any
-> GTranslateM Identity (Cxt NoHole (Sum CSig) (K ())) Any
forall a b. (a -> b) -> a -> b
$ TranslateM
  (MaybeT Identity)
  (Cxt NoHole (Sum CSig) (K ()))
  CStorageSpecifierL
  Any
-> GTranslateM (MaybeT Identity) (Cxt NoHole (Sum CSig) (K ())) Any
forall (f :: * -> *) l (m :: * -> *) t.
(DynCase f l, Alternative m) =>
TranslateM m f l t -> GTranslateM m f t
promoteTF (TranslateM
   (MaybeT Identity)
   (Cxt NoHole (Sum CSig) (K ()))
   CStorageSpecifierL
   Any
 -> GTranslateM
      (MaybeT Identity) (Cxt NoHole (Sum CSig) (K ())) Any)
-> TranslateM
     (MaybeT Identity)
     (Cxt NoHole (Sum CSig) (K ()))
     CStorageSpecifierL
     Any
-> GTranslateM (MaybeT Identity) (Cxt NoHole (Sum CSig) (K ())) Any
forall a b. (a -> b) -> a -> b
$ TranslateM
  Identity (Cxt NoHole (Sum CSig) (K ())) CStorageSpecifierL Any
-> TranslateM
     (MaybeT Identity)
     (Cxt NoHole (Sum CSig) (K ()))
     CStorageSpecifierL
     Any
forall (m :: * -> *) (f :: * -> *) l t.
Monad m =>
TranslateM m f l t -> TranslateM (MaybeT m) f l t
addFail TranslateM
  Identity (Cxt NoHole (Sum CSig) (K ())) CStorageSpecifierL Any
forall (m :: * -> *). Monad m => CTerm CStorageSpecifierL -> m Any
isStatic)
  where
    isStatic :: (Monad m) => F.CTerm F.CStorageSpecifierL -> m Any
    isStatic :: forall (m :: * -> *). Monad m => CTerm CStorageSpecifierL -> m Any
isStatic (CTerm CStorageSpecifierL
-> Maybe
     (CStorageSpecifier
        (Cxt NoHole (Sum CSig) (K ())) CStorageSpecifierL)
NatM
  Maybe
  (Cxt NoHole (Sum CSig) (K ()))
  (CStorageSpecifier (Cxt NoHole (Sum CSig) (K ())))
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CStatic Cxt NoHole (Sum CSig) (K ()) ()
_)) = Any -> m Any
forall a. a -> m a
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 CTerm CStorageSpecifierL
_                               = Any -> m Any
forall a. a -> m a
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

transMultiDec :: F.CTerm F.CDeclarationL -> MCTerm MultiLocalVarDeclL
transMultiDec :: CTerm CDeclarationL -> MCTerm MultiLocalVarDeclL
transMultiDec (CTerm CDeclarationL
-> Maybe
     (CDeclaration (Cxt NoHole (Sum CSig) (K ())) CDeclarationL)
NatM
  Maybe
  (Cxt NoHole (Sum CSig) (K ()))
  (CDeclaration (Cxt NoHole (Sum CSig) (K ())))
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CDecl Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
specs Cxt
  NoHole
  (Sum CSig)
  (K ())
  [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
single_decs Cxt NoHole (Sum CSig) (K ()) ()
_)) =
        Cxt NoHole (Sum MCSig) (K ()) MultiLocalVarDeclCommonAttrsL
-> Cxt NoHole (Sum MCSig) (K ()) [SingleLocalVarDeclL]
-> MCTerm MultiLocalVarDeclL
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) j.
(MultiLocalVarDecl :<: f) =>
Cxt h f a MultiLocalVarDeclCommonAttrsL
-> Cxt h f a [SingleLocalVarDeclL] -> Cxt h f a MultiLocalVarDeclL
MultiLocalVarDecl' (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> Cxt NoHole (Sum MCSig) (K ()) MultiLocalVarDeclCommonAttrsL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MCSig a [CDeclarationSpecifierL]
-> CxtS h MCSig a MultiLocalVarDeclCommonAttrsL
injF (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
 -> Cxt NoHole (Sum MCSig) (K ()) MultiLocalVarDeclCommonAttrsL)
-> CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> Cxt NoHole (Sum MCSig) (K ()) MultiLocalVarDeclCommonAttrsL
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
specs) ((CTerm
   (Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)
 -> MCTerm SingleLocalVarDeclL)
-> Cxt
     NoHole
     (Sum CSig)
     (K ())
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> Cxt NoHole (Sum 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)

instance {-# OVERLAPPING #-} Trans F.CCompoundBlockItem where
  trans :: forall l.
CCompoundBlockItem (Cxt NoHole (Sum CSig) (K ())) l -> MCTerm l
trans t :: CCompoundBlockItem (Cxt NoHole (Sum CSig) (K ())) l
t@(F.CBlockStmt CTerm CStatementL
_)    = CCompoundBlockItem (Cxt NoHole (Sum CSig) (K ())) l -> MCTerm l
forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: MCSig, f :-<: CSig) =>
f (Cxt NoHole (Sum CSig) (K ())) l -> MCTerm l
transDefault CCompoundBlockItem (Cxt NoHole (Sum CSig) (K ())) l
t
  trans t :: CCompoundBlockItem (Cxt NoHole (Sum CSig) (K ())) l
t@(F.CNestedFunDef CTerm CFunctionDefL
_) = CCompoundBlockItem (Cxt NoHole (Sum CSig) (K ())) l -> MCTerm l
forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: MCSig, f :-<: CSig) =>
f (Cxt NoHole (Sum CSig) (K ())) l -> MCTerm l
transDefault CCompoundBlockItem (Cxt NoHole (Sum CSig) (K ())) l
t
  trans t :: CCompoundBlockItem (Cxt NoHole (Sum CSig) (K ())) l
t@(F.CBlockDecl CTerm CDeclarationL
decl) =
    if CTerm CDeclarationL -> Bool
containsStatic CTerm CDeclarationL
decl then
      CCompoundBlockItem (Cxt NoHole (Sum CSig) (K ())) l -> MCTerm l
forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: MCSig, f :-<: CSig) =>
f (Cxt NoHole (Sum CSig) (K ())) l -> MCTerm l
transDefault CCompoundBlockItem (Cxt NoHole (Sum CSig) (K ())) l
t
    else
      MCTerm MultiLocalVarDeclL -> MCTerm l
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MCSig a MultiLocalVarDeclL -> CxtS h MCSig a l
injF (MCTerm MultiLocalVarDeclL -> MCTerm l)
-> MCTerm MultiLocalVarDeclL -> MCTerm l
forall a b. (a -> b) -> a -> b
$ CTerm CDeclarationL -> MCTerm MultiLocalVarDeclL
transMultiDec CTerm CDeclarationL
decl

-------- Assignments

transAssignOp :: F.CTerm F.CAssignOpL -> MCTerm AssignOpL
transAssignOp :: CTerm CAssignOpL -> MCTerm AssignOpL
transAssignOp (CTerm CAssignOpL
-> Maybe (CAssignOp (Cxt NoHole (Sum CSig) (K ())) CAssignOpL)
NatM
  Maybe
  (Cxt NoHole (Sum CSig) (K ()))
  (CAssignOp (Cxt NoHole (Sum CSig) (K ())))
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just CAssignOp (Cxt NoHole (Sum CSig) (K ())) CAssignOpL
F.CAssignOp) = MCTerm AssignOpL
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) j.
(AssignOpEquals :<: f) =>
Cxt h f a AssignOpL
AssignOpEquals'
transAssignOp 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'
forall h (a :: * -> *).
CxtS h MCSig a CAssignOpL -> CxtS h MCSig a AssignOpL
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 CTerm [CExpressionL]
args = Cxt NoHole (Sum MCSig) (K ()) [FunctionArgumentL]
-> MCTerm FunctionArgumentsL
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) j.
(FunctionArgumentList :<: f) =>
Cxt h f a [FunctionArgumentL] -> Cxt h f a FunctionArgumentsL
FunctionArgumentList' (Cxt NoHole (Sum MCSig) (K ()) [FunctionArgumentL]
 -> MCTerm FunctionArgumentsL)
-> Cxt NoHole (Sum 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]
-> Cxt NoHole (Sum 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 (Cxt NoHole (Sum MCSig) (K ()) PositionalArgExpL
-> Cxt NoHole (Sum MCSig) (K ()) FunctionArgumentL
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) j.
(PositionalArgument :<: f) =>
Cxt h f a PositionalArgExpL -> Cxt h f a FunctionArgumentL
PositionalArgument' (Cxt NoHole (Sum MCSig) (K ()) PositionalArgExpL
 -> Cxt NoHole (Sum MCSig) (K ()) FunctionArgumentL)
-> (Cxt NoHole (Sum CSig) (K ()) CExpressionL
    -> Cxt NoHole (Sum 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
-> Cxt NoHole (Sum MCSig) (K ()) PositionalArgExpL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MCSig a CExpressionL -> CxtS h MCSig a PositionalArgExpL
injF (CxtS NoHole MCSig (K ()) CExpressionL
 -> Cxt NoHole (Sum MCSig) (K ()) PositionalArgExpL)
-> (Cxt NoHole (Sum CSig) (K ()) CExpressionL
    -> CxtS NoHole MCSig (K ()) CExpressionL)
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
-> Cxt NoHole (Sum 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

-------- (Multiple categories)

instance {-# OVERLAPPING #-} Trans F.CExpression where
  trans :: forall l. CExpression (Cxt NoHole (Sum CSig) (K ())) l -> MCTerm l
trans t :: CExpression (Cxt NoHole (Sum CSig) (K ())) l
t@(F.CAssign CTerm CAssignOpL
op Cxt NoHole (Sum CSig) (K ()) CExpressionL
lhs Cxt NoHole (Sum CSig) (K ()) CExpressionL
rhs Cxt NoHole (Sum CSig) (K ()) ()
_) = CxtS NoHole MCSig (K ()) LhsL
-> MCTerm AssignOpL
-> CxtS NoHole MCSig (K ()) RhsL
-> CxtS NoHole MCSig (K ()) 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'
forall h (a :: * -> *).
CxtS h MCSig a CExpressionL -> CxtS h MCSig a LhsL
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
transAssignOp 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'
forall h (a :: * -> *).
CxtS h MCSig a CExpressionL -> CxtS h MCSig a RhsL
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 (Cxt NoHole (Sum CSig) (K ())) l
t@(F.CCall Cxt NoHole (Sum CSig) (K ()) CExpressionL
f CTerm [CExpressionL]
args Cxt NoHole (Sum CSig) (K ()) ()
_)       = CxtS NoHole MCSig (K ()) FunctionCallAttrsL
-> CxtS NoHole MCSig (K ()) FunctionExpL
-> MCTerm FunctionArgumentsL
-> CxtS NoHole MCSig (K ()) 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 h (f :: (* -> *) -> * -> *) (a :: * -> *) j.
(EmptyFunctionCallAttrs :<: f) =>
Cxt h f 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'
forall h (a :: * -> *).
CxtS h MCSig a CExpressionL -> CxtS h MCSig a FunctionExpL
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 CExpression (Cxt NoHole (Sum CSig) (K ())) l
t                          = CExpression (Cxt NoHole (Sum CSig) (K ())) l
-> CxtS NoHole MCSig (K ()) l
forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: MCSig, f :-<: CSig) =>
f (Cxt NoHole (Sum CSig) (K ())) l -> MCTerm l
transDefault CExpression (Cxt NoHole (Sum CSig) (K ())) l
t

-------- For-loops

transForInit :: F.CTerm (Either (Maybe F.CExpressionL) F.CDeclarationL) -> MCTerm CForInitL
transForInit :: CTerm (Either (Maybe CExpressionL) CDeclarationL)
-> MCTerm CForInitL
transForInit (Left' Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
Nothing')  = MCTerm CForInitL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CForInit :-<: fs, InjF fs CForInitL j) =>
CxtS h fs a j
iCForInitEmpty
transForInit (Left' (Just' Cxt NoHole (Sum CSig) (K ()) CExpressionL
e)) = CxtS NoHole MCSig (K ()) CExpressionL -> MCTerm CForInitL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CForInit :-<: fs, InjF fs CForInitL j) =>
CxtS h fs a CExpressionL -> CxtS h fs a j
iCForInitExp (CxtS NoHole MCSig (K ()) CExpressionL -> MCTerm CForInitL)
-> CxtS NoHole MCSig (K ()) CExpressionL -> MCTerm CForInitL
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
e
transForInit (Right' CTerm CDeclarationL
dec)      = MCTerm MultiLocalVarDeclL -> MCTerm CForInitL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CForInit :-<: fs, InjF fs CForInitL j) =>
CxtS h fs a MultiLocalVarDeclL -> CxtS h fs a j
iCForInitDecl (MCTerm MultiLocalVarDeclL -> MCTerm CForInitL)
-> MCTerm MultiLocalVarDeclL -> MCTerm CForInitL
forall a b. (a -> b) -> a -> b
$ CTerm CDeclarationL -> MCTerm MultiLocalVarDeclL
transMultiDec CTerm CDeclarationL
dec

instance {-# OVERLAPPING #-} Trans F.CStatement where
  trans :: forall l. CStatement (Cxt NoHole (Sum CSig) (K ())) l -> MCTerm l
trans t :: CStatement (Cxt NoHole (Sum CSig) (K ())) l
t@(F.CCompound CTerm [IdentL]
ids CTerm [CCompoundBlockItemL]
items Cxt NoHole (Sum CSig) (K ()) ()
_)        = CxtS NoHole MCSig (K ()) [IdentL]
-> CxtS NoHole MCSig (K ()) BlockL -> CxtS NoHole MCSig (K ()) 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) (Cxt NoHole (Sum MCSig) (K ()) [BlockItemL]
-> Cxt NoHole (Sum MCSig) (K ()) BlockEndL
-> CxtS NoHole MCSig (K ()) BlockL
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) j.
(Block :<: f) =>
Cxt h f a [BlockItemL] -> Cxt h f a BlockEndL -> Cxt h f a BlockL
Block' ((Cxt NoHole (Sum CSig) (K ()) CCompoundBlockItemL
 -> Cxt NoHole (Sum MCSig) (K ()) BlockItemL)
-> CTerm [CCompoundBlockItemL]
-> Cxt NoHole (Sum 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'
forall h (a :: * -> *).
CxtS h MCSig a CCompoundBlockItemL -> CxtS h MCSig a BlockItemL
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) Cxt NoHole (Sum MCSig) (K ()) BlockEndL
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) j.
(EmptyBlockEnd :<: f) =>
Cxt h f a BlockEndL
EmptyBlockEnd')
  trans t :: CStatement (Cxt NoHole (Sum CSig) (K ())) l
t@(F.CFor CTerm (Either (Maybe CExpressionL) CDeclarationL)
init Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
cond Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
update CTerm CStatementL
body Cxt NoHole (Sum CSig) (K ()) ()
_) = MCTerm CForInitL
-> CxtS NoHole MCSig (K ()) (Maybe CExpressionL)
-> CxtS NoHole MCSig (K ()) (Maybe CExpressionL)
-> CxtS NoHole MCSig (K ()) CStatementL
-> CxtS NoHole MCSig (K ()) l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CFor :-<: fs, InjF fs CStatementL j) =>
CxtS h fs a CForInitL
-> CxtS h fs a (Maybe CExpressionL)
-> CxtS h fs a (Maybe CExpressionL)
-> CxtS h fs a CStatementL
-> CxtS h fs a j
iCFor (CTerm (Either (Maybe CExpressionL) CDeclarationL)
-> MCTerm CForInitL
transForInit CTerm (Either (Maybe CExpressionL) CDeclarationL)
init) (Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
-> CxtS NoHole MCSig (K ()) (Maybe CExpressionL)
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
cond) (Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
-> CxtS NoHole MCSig (K ()) (Maybe CExpressionL)
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
update) (CTerm CStatementL -> CxtS NoHole MCSig (K ()) CStatementL
forall l. CTerm l -> MCTerm l
translate CTerm CStatementL
body)
  trans CStatement (Cxt NoHole (Sum CSig) (K ())) l
t                                  = CStatement (Cxt NoHole (Sum CSig) (K ())) l
-> CxtS NoHole MCSig (K ()) l
forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: MCSig, f :-<: CSig) =>
f (Cxt NoHole (Sum CSig) (K ())) l -> MCTerm l
transDefault CStatement (Cxt NoHole (Sum CSig) (K ())) l
t

-------- Function calls, declarations, and definitions

paramDeclFromId :: F.CTerm F.IdentL -> MCTerm FunctionParameterDeclL
paramDeclFromId :: CTerm IdentL -> MCTerm FunctionParameterDeclL
paramDeclFromId CTerm IdentL
n = Cxt NoHole (Sum MCSig) (K ()) FunctionParameterDeclAttrsL
-> Cxt NoHole (Sum MCSig) (K ()) (Maybe IdentL)
-> MCTerm FunctionParameterDeclL
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) j.
(PositionalParameterDeclOptionalIdent :<: f) =>
Cxt h f a FunctionParameterDeclAttrsL
-> Cxt h f a (Maybe IdentL) -> Cxt h f a FunctionParameterDeclL
PositionalParameterDeclOptionalIdent' (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
-> CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
-> CxtS NoHole MCSig (K ()) [CAttributeL]
-> Cxt NoHole (Sum 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 -> Cxt NoHole (Sum 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 -> Cxt NoHole (Sum MCSig) (K ()) (Maybe IdentL))
-> MCTerm IdentL -> Cxt NoHole (Sum 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 (Cxt NoHole (Sum CSig) (K ())) CDeclarationL)
NatM
  Maybe
  (Cxt NoHole (Sum CSig) (K ()))
  (CDeclaration (Cxt NoHole (Sum CSig) (K ())))
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
        (Cxt NoHole (Sum CSig) (K ())) CDeclarationSpecifierL)
NatM
  Maybe
  (Cxt NoHole (Sum CSig) (K ()))
  (CDeclarationSpecifier (Cxt NoHole (Sum CSig) (K ())))
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 (Cxt NoHole (Sum CSig) (K ())) CTypeSpecifierL)
NatM
  Maybe
  (Cxt NoHole (Sum CSig) (K ()))
  (CTypeSpecifier (Cxt NoHole (Sum CSig) (K ())))
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CVoidType Cxt NoHole (Sum CSig) (K ()) ()
_))))) Cxt
  NoHole
  (Sum CSig)
  (K ())
  [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
NilF' Cxt NoHole (Sum CSig) (K ()) ()
_)) = MCTerm FunctionParameterDeclL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CVoidArg :-<: fs, InjF fs CSpecialParamL j) =>
CxtS h fs a j
iCVoidArg

paramDeclFromDecl (CTerm CDeclarationL
-> Maybe
     (CDeclaration (Cxt NoHole (Sum CSig) (K ())) CDeclarationL)
NatM
  Maybe
  (Cxt NoHole (Sum CSig) (K ()))
  (CDeclaration (Cxt NoHole (Sum CSig) (K ())))
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CDecl Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
dss Cxt
  NoHole
  (Sum CSig)
  (K ())
  [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
inf Cxt NoHole (Sum CSig) (K ()) ()
_)) =
  case Cxt
  NoHole
  (Sum CSig)
  (K ())
  [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
inf of
    Cxt
  NoHole
  (Sum CSig)
  (K ())
  [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
NilF' -> Cxt NoHole (Sum MCSig) (K ()) FunctionParameterDeclAttrsL
-> Cxt NoHole (Sum MCSig) (K ()) (Maybe IdentL)
-> MCTerm FunctionParameterDeclL
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) j.
(PositionalParameterDeclOptionalIdent :<: f) =>
Cxt h f a FunctionParameterDeclAttrsL
-> Cxt h f a (Maybe IdentL) -> Cxt h f a FunctionParameterDeclL
PositionalParameterDeclOptionalIdent' (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
-> CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
-> CxtS NoHole MCSig (K ()) [CAttributeL]
-> Cxt NoHole (Sum 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 (Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) [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') Cxt NoHole (Sum 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 (Cxt NoHole (Sum CSig) (K ())) CDeclaratorL)
NatM
  Maybe
  (Cxt NoHole (Sum CSig) (K ()))
  (CDeclarator (Cxt NoHole (Sum CSig) (K ())))
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CDeclr Cxt NoHole (Sum CSig) (K ()) (Maybe IdentL)
nOpt Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
dds Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
asmNm Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs Cxt NoHole (Sum CSig) (K ()) ()
_))) Cxt NoHole (Sum CSig) (K ()) (Maybe CInitializerL)
Nothing' Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
Nothing')) ->
                Cxt NoHole (Sum MCSig) (K ()) FunctionParameterDeclAttrsL
-> Cxt NoHole (Sum MCSig) (K ()) (Maybe IdentL)
-> MCTerm FunctionParameterDeclL
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) j.
(PositionalParameterDeclOptionalIdent :<: f) =>
Cxt h f a FunctionParameterDeclAttrsL
-> Cxt h f a (Maybe IdentL) -> Cxt h f a FunctionParameterDeclL
PositionalParameterDeclOptionalIdent' (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
-> CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
-> CxtS NoHole MCSig (K ()) [CAttributeL]
-> Cxt NoHole (Sum 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 (Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) [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)
-> Cxt NoHole (Sum 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 :: forall l. CDeclarator (Cxt NoHole (Sum CSig) (K ())) l -> MCTerm l
trans t :: CDeclarator (Cxt NoHole (Sum CSig) (K ())) l
t@(F.CDeclr (Just' CTerm IdentL
n) (ConsF' (Cxt NoHole (Sum CSig) (K ()) CDerivedDeclaratorL
-> Maybe
     (CDerivedDeclarator
        (Cxt NoHole (Sum CSig) (K ())) CDerivedDeclaratorL)
NatM
  Maybe
  (Cxt NoHole (Sum CSig) (K ()))
  (CDerivedDeclarator (Cxt NoHole (Sum CSig) (K ())))
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CFunDeclr Cxt
  NoHole (Sum CSig) (K ()) (Either [IdentL] ([CDeclarationL], BoolL))
pars Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs1 Cxt NoHole (Sum CSig) (K ()) ()
_)) Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
dds) Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
asmNm Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs2 Cxt NoHole (Sum CSig) (K ()) ()
_) =
    CxtS NoHole MCSig (K ()) FunctionDeclAttrsL
-> MCTerm IdentL
-> CxtS NoHole MCSig (K ()) [FunctionParameterDeclL]
-> CxtS NoHole MCSig (K ()) 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' 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' Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
decls (BoolF' Bool
isVarArg)) -> [MCTerm FunctionParameterDeclL]
-> CxtS NoHole MCSig (K ()) [FunctionParameterDeclL]
forall l.
Typeable l =>
[Cxt NoHole (Sum MCSig) (K ()) l]
-> Cxt NoHole (Sum MCSig) (K ()) [l]
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 l.
Cxt NoHole (Sum CSig) (K ()) [l]
-> [Cxt NoHole (Sum CSig) (K ()) l]
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 CDeclarator (Cxt NoHole (Sum CSig) (K ())) l
t = CDeclarator (Cxt NoHole (Sum CSig) (K ())) l
-> CxtS NoHole MCSig (K ()) l
forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: MCSig, f :-<: CSig) =>
f (Cxt NoHole (Sum CSig) (K ())) l -> MCTerm l
transDefault CDeclarator (Cxt NoHole (Sum CSig) (K ())) 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 (Cxt NoHole (Sum CSig) (K ())) CDeclarationL)
NatM
  Maybe
  (Cxt NoHole (Sum CSig) (K ()))
  (CDeclaration (Cxt NoHole (Sum CSig) (K ())))
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
        (Cxt NoHole (Sum CSig) (K ())) CDeclarationSpecifierL)
NatM
  Maybe
  (Cxt NoHole (Sum CSig) (K ()))
  (CDeclarationSpecifier (Cxt NoHole (Sum CSig) (K ())))
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 (Cxt NoHole (Sum CSig) (K ())) CTypeSpecifierL)
NatM
  Maybe
  (Cxt NoHole (Sum CSig) (K ()))
  (CTypeSpecifier (Cxt NoHole (Sum CSig) (K ())))
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CVoidType Cxt NoHole (Sum CSig) (K ()) ()
_))))) Cxt
  NoHole
  (Sum CSig)
  (K ())
  [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
NilF' Cxt NoHole (Sum CSig) (K ()) ()
_)) = MCTerm FunctionParameterL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CVoidArg :-<: fs, InjF fs CSpecialParamL j) =>
CxtS h fs a j
iCVoidArg
paramFromDecl (CTerm CDeclarationL
-> Maybe
     (CDeclaration (Cxt NoHole (Sum CSig) (K ())) CDeclarationL)
NatM
  Maybe
  (Cxt NoHole (Sum CSig) (K ()))
  (CDeclaration (Cxt NoHole (Sum CSig) (K ())))
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CDecl Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
dss (SingletonF' (TripleF' Cxt NoHole (Sum CSig) (K ()) (Maybe CDeclaratorL)
declOpt Cxt NoHole (Sum CSig) (K ()) (Maybe CInitializerL)
Nothing' Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
Nothing')) Cxt NoHole (Sum CSig) (K ()) ()
_)) =
  case Cxt NoHole (Sum CSig) (K ()) (Maybe CDeclaratorL)
declOpt of
    Cxt NoHole (Sum CSig) (K ()) (Maybe CDeclaratorL)
Nothing' -> String -> MCTerm FunctionParameterL
forall a. HasCallStack => String -> a
error String
"Unnamed parameter in function definition"
    Just' (Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
-> Maybe (CDeclarator (Cxt NoHole (Sum CSig) (K ())) CDeclaratorL)
NatM
  Maybe
  (Cxt NoHole (Sum CSig) (K ()))
  (CDeclarator (Cxt NoHole (Sum CSig) (K ())))
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CDeclr (Just' CTerm IdentL
n) Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
dds Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
asmNm Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs Cxt NoHole (Sum CSig) (K ()) ()
_)) ->
                Cxt NoHole (Sum MCSig) (K ()) ParameterAttrsL
-> MCTerm IdentL -> MCTerm FunctionParameterL
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) j.
(PositionalParameter :<: f) =>
Cxt h f a ParameterAttrsL
-> Cxt h f a IdentL -> Cxt h f a FunctionParameterL
PositionalParameter' (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
-> CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
-> CxtS NoHole MCSig (K ()) [CAttributeL]
-> Cxt NoHole (Sum 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 (Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) [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 :: forall l. CFunctionDef (Cxt NoHole (Sum CSig) (K ())) l -> MCTerm l
trans (F.CFunDef Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
dss (Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
-> Maybe (CDeclarator (Cxt NoHole (Sum CSig) (K ())) CDeclaratorL)
NatM
  Maybe
  (Cxt NoHole (Sum CSig) (K ()))
  (CDeclarator (Cxt NoHole (Sum CSig) (K ())))
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CDeclr (Just' CTerm IdentL
n)
                                                  (ConsF' (Cxt NoHole (Sum CSig) (K ()) CDerivedDeclaratorL
-> Maybe
     (CDerivedDeclarator
        (Cxt NoHole (Sum CSig) (K ())) CDerivedDeclaratorL)
NatM
  Maybe
  (Cxt NoHole (Sum CSig) (K ()))
  (CDerivedDeclarator (Cxt NoHole (Sum CSig) (K ())))
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (F.CFunDeclr Cxt
  NoHole (Sum CSig) (K ()) (Either [IdentL] ([CDeclarationL], BoolL))
pars Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs1 Cxt NoHole (Sum CSig) (K ()) ()
_)) Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
dds)
                                                  Cxt NoHole (Sum CSig) (K ()) (Maybe CStringLiteralL)
asmNm Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
attrs2 Cxt NoHole (Sum CSig) (K ()) ()
_))
                   Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
oldStyleDecls CTerm CStatementL
body Cxt NoHole (Sum CSig) (K ()) ()
_) =
      CxtS NoHole MCSig (K ()) FunctionDefAttrsL
-> MCTerm IdentL
-> CxtS NoHole MCSig (K ()) [FunctionParameterL]
-> CxtS NoHole MCSig (K ()) FunctionBodyL
-> CxtS NoHole MCSig (K ()) 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 (Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
-> CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
forall l. CTerm l -> MCTerm l
translate Cxt NoHole (Sum CSig) (K ()) [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' 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' Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
decls (BoolF' Bool
isVarArg)) -> [MCTerm FunctionParameterL]
-> CxtS NoHole MCSig (K ()) [FunctionParameterL]
forall l.
Typeable l =>
[Cxt NoHole (Sum MCSig) (K ()) l]
-> Cxt NoHole (Sum MCSig) (K ()) [l]
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 l.
Cxt NoHole (Sum CSig) (K ()) [l]
-> [Cxt NoHole (Sum CSig) (K ()) l]
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'
forall h (a :: * -> *).
CxtS h MCSig a CStatementL -> CxtS h MCSig a FunctionBodyL
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)


------------------------------------------------------------------------------------
---------------- Reverse translation: IPS to modularized syntax  -------------------
------------------------------------------------------------------------------------


--------------------------------
------------- Top-level untranslate
--------------------------------

------ Class (contains top-level function on sigs)

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


------ Default and standard cases

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

untransError :: (HFunctor f, f :-<: MCSig) => f MCTerm l -> F.CTerm l
untransError :: forall (f :: (* -> *) -> * -> *) l.
(HFunctor f, f :-<: MCSig) =>
f (Cxt NoHole (Sum MCSig) (K ())) l -> CTerm l
untransError 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
$ String
"Cannot untranslate root node: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Cxt NoHole (Sum MCSig) (K ()) l -> String
forall a. Show a => a -> String
show (Cxt NoHole (Sum MCSig) (K ()) l -> String)
-> Cxt NoHole (Sum MCSig) (K ()) l -> String
forall a b. (a -> b) -> a -> b
$ f (Cxt NoHole (Sum MCSig) (K ())) l
-> Cxt NoHole (Sum MCSig) (K ()) l
f (Cxt NoHole (Sum MCSig) (K ())) :-> Cxt NoHole (Sum MCSig) (K ())
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)

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

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

instance {-# OVERLAPPABLE #-} (HFunctor f, f :-<: F.CSig) => Untrans f where
  untrans :: forall l. 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

------ Top level function on terms

-- Must define this after template Haskell block
untranslate :: MCTerm l -> F.CTerm l
untranslate :: Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
untranslate = Sum MCSig (Cxt NoHole (Sum MCSig) (K ())) l -> CTerm l
forall l. 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

--------------------------------
------------- Per-fragment instances
--------------------------------

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

-------- Identifiers

untransIdent :: MCTerm IdentL -> F.CTerm F.IdentL
untransIdent :: MCTerm IdentL -> CTerm IdentL
untransIdent (Ident' String
s) = String
-> Int -> Cxt NoHole (Sum CSig) (K ()) 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 Int
0 Cxt NoHole (Sum CSig) (K ()) NodeInfoL
dummyNodeInfo

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

-------- Declarations

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' Cxt NoHole (Sum MCSig) (K ()) LocalVarDeclAttrsL
attrs Cxt NoHole (Sum MCSig) (K ()) VarDeclBinderL
id Cxt NoHole (Sum 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 CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
decs CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
asmName CxtS NoHole MCSig (K ()) [CAttributeL]
cAttrs) = Cxt NoHole (Sum MCSig) (K ()) LocalVarDeclAttrsL
-> Maybe
     (CLocalVarAttrs (Cxt NoHole (Sum MCSig) (K ())) LocalVarDeclAttrsL)
NatM
  Maybe
  (Cxt NoHole (Sum MCSig) (K ()))
  (CLocalVarAttrs (Cxt NoHole (Sum MCSig) (K ())))
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project Cxt NoHole (Sum 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]
-> Cxt NoHole (Sum 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
$ Cxt NoHole (Sum 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 Cxt NoHole (Sum MCSig) (K ()) VarDeclBinderL
id) (CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
-> Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
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 ()) :-> Cxt NoHole (Sum CSig) (K ())
untranslate CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
asmName) (CxtS NoHole MCSig (K ()) [CAttributeL]
-> Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
untranslate CxtS NoHole MCSig (K ()) [CAttributeL]
cAttrs) Cxt NoHole (Sum 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 Cxt NoHole (Sum MCSig) (K ()) OptLocalVarInitL
init of
      Cxt NoHole (Sum MCSig) (K ()) OptLocalVarInitL
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' Cxt NoHole (Sum 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 ()) :-> Cxt NoHole (Sum CSig) (K ())
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
$ Cxt NoHole (Sum 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 Cxt NoHole (Sum MCSig) (K ()) LocalVarInitL
x

untransMultiDec :: MCTerm MultiLocalVarDeclL -> F.CTerm F.CDeclarationL
untransMultiDec :: MCTerm MultiLocalVarDeclL -> CTerm CDeclarationL
untransMultiDec (MultiLocalVarDecl' Cxt NoHole (Sum MCSig) (K ()) MultiLocalVarDeclCommonAttrsL
attrs Cxt NoHole (Sum MCSig) (K ()) [SingleLocalVarDeclL]
decls) = Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
-> Cxt
     NoHole
     (Sum CSig)
     (K ())
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> Cxt NoHole (Sum 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]
-> Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
untranslate (CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
 -> Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL])
-> CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
-> Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum 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 Cxt NoHole (Sum MCSig) (K ()) MultiLocalVarDeclCommonAttrsL
attrs) ((MCTerm SingleLocalVarDeclL
 -> CTerm
      (Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL))
-> Cxt NoHole (Sum 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 Cxt NoHole (Sum MCSig) (K ()) [SingleLocalVarDeclL]
decls) Cxt NoHole (Sum CSig) (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF

instance {-# OVERLAPPING #-} Untrans MultiLocalVarDeclIsCCompoundBlockItem where
  untrans :: forall l.
MultiLocalVarDeclIsCCompoundBlockItem
  (Cxt NoHole (Sum MCSig) (K ())) l
-> CTerm l
untrans (MultiLocalVarDeclIsCCompoundBlockItem MCTerm MultiLocalVarDeclL
dec) = CTerm CDeclarationL -> CxtS NoHole CSig (K ()) 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 -> CxtS NoHole CSig (K ()) l)
-> CTerm CDeclarationL -> CxtS NoHole CSig (K ()) l
forall a b. (a -> b) -> a -> b
$ MCTerm MultiLocalVarDeclL -> CTerm CDeclarationL
untransMultiDec MCTerm MultiLocalVarDeclL
dec

-------- Assignment

untransAssignOp :: MCTerm AssignOpL -> F.CTerm F.CAssignOpL
untransAssignOp :: MCTerm AssignOpL -> CTerm CAssignOpL
untransAssignOp MCTerm AssignOpL
AssignOpEquals' = CTerm CAssignOpL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CAssignOp :-<: fs, InjF fs CAssignOpL j) =>
CxtS h fs a j
F.iCAssignOp
untransAssignOp MCTerm AssignOpL
x               = CxtS NoHole MCSig (K ()) CAssignOpL -> CTerm CAssignOpL
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
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 :: forall l.
AssignIsCExpression (Cxt NoHole (Sum MCSig) (K ())) l -> CTerm l
untrans (AssignIsCExpression (Assign' CxtS NoHole MCSig (K ()) LhsL
lhs MCTerm AssignOpL
op CxtS NoHole MCSig (K ()) RhsL
rhs)) = CTerm CAssignOpL
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
-> Cxt NoHole (Sum CSig) (K ()) ()
-> CxtS NoHole CSig (K ()) 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
untransAssignOp MCTerm AssignOpL
op) (CxtS NoHole MCSig (K ()) CExpressionL
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
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 ()) :-> Cxt NoHole (Sum CSig) (K ())
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) Cxt NoHole (Sum CSig) (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF

-------- Labeled blocks

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

-------- For loops

untransForInit :: MCTerm CForInitL -> F.CTerm (Either (Maybe F.CExpressionL) F.CDeclarationL)
untransForInit :: MCTerm CForInitL
-> CTerm (Either (Maybe CExpressionL) CDeclarationL)
untransForInit (MCTerm CForInitL
-> Maybe (CForInit (Cxt NoHole (Sum MCSig) (K ())) CForInitL)
NatM
  Maybe
  (Cxt NoHole (Sum MCSig) (K ()))
  (CForInit (Cxt NoHole (Sum MCSig) (K ())))
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just CForInit (Cxt NoHole (Sum MCSig) (K ())) CForInitL
CForInitEmpty)      = Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
-> CTerm (Either (Maybe CExpressionL) CDeclarationL)
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' 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'
untransForInit (MCTerm CForInitL
-> Maybe (CForInit (Cxt NoHole (Sum MCSig) (K ())) CForInitL)
NatM
  Maybe
  (Cxt NoHole (Sum MCSig) (K ()))
  (CForInit (Cxt NoHole (Sum MCSig) (K ())))
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (CForInitExp  CxtS NoHole MCSig (K ()) CExpressionL
e))   = Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
-> CTerm (Either (Maybe CExpressionL) CDeclarationL)
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' (Cxt NoHole (Sum CSig) (K ()) CExpressionL
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
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 ()) CExpressionL
 -> Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL))
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
forall a b. (a -> b) -> a -> b
$ CxtS NoHole MCSig (K ()) CExpressionL
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
untranslate CxtS NoHole MCSig (K ()) CExpressionL
e)
untransForInit (MCTerm CForInitL
-> Maybe (CForInit (Cxt NoHole (Sum MCSig) (K ())) CForInitL)
NatM
  Maybe
  (Cxt NoHole (Sum MCSig) (K ()))
  (CForInit (Cxt NoHole (Sum MCSig) (K ())))
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (CForInitDecl MCTerm MultiLocalVarDeclL
dec)) = CTerm CDeclarationL
-> CTerm (Either (Maybe CExpressionL) CDeclarationL)
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' (CTerm CDeclarationL
 -> CTerm (Either (Maybe CExpressionL) CDeclarationL))
-> CTerm CDeclarationL
-> CTerm (Either (Maybe CExpressionL) CDeclarationL)
forall a b. (a -> b) -> a -> b
$ MCTerm MultiLocalVarDeclL -> CTerm CDeclarationL
untransMultiDec MCTerm MultiLocalVarDeclL
dec

instance {-# OVERLAPPING #-} Untrans CFor where
  untrans :: forall l. CFor (Cxt NoHole (Sum MCSig) (K ())) l -> CTerm l
untrans (CFor MCTerm CForInitL
init CxtS NoHole MCSig (K ()) (Maybe CExpressionL)
cond CxtS NoHole MCSig (K ()) (Maybe CExpressionL)
update CxtS NoHole MCSig (K ()) CStatementL
body) = CTerm (Either (Maybe CExpressionL) CDeclarationL)
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
-> CTerm CStatementL
-> Cxt NoHole (Sum CSig) (K ()) ()
-> CxtS NoHole CSig (K ()) l
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CStatement :-<: fs, InjF fs CStatementL j) =>
CxtS h fs a (Either (Maybe CExpressionL) CDeclarationL)
-> CxtS h fs a (Maybe CExpressionL)
-> CxtS h fs a (Maybe CExpressionL)
-> CxtS h fs a CStatementL
-> CxtS h fs a ()
-> CxtS h fs a j
F.iCFor (MCTerm CForInitL
-> CTerm (Either (Maybe CExpressionL) CDeclarationL)
untransForInit MCTerm CForInitL
init) (CxtS NoHole MCSig (K ()) (Maybe CExpressionL)
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
untranslate CxtS NoHole MCSig (K ()) (Maybe CExpressionL)
cond) (CxtS NoHole MCSig (K ()) (Maybe CExpressionL)
-> Cxt NoHole (Sum CSig) (K ()) (Maybe CExpressionL)
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
untranslate CxtS NoHole MCSig (K ()) (Maybe CExpressionL)
update) (CxtS NoHole MCSig (K ()) CStatementL -> CTerm CStatementL
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
untranslate CxtS NoHole MCSig (K ()) CStatementL
body) Cxt NoHole (Sum CSig) (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF

-------- Function calls, declarations, and definitions

untranslateArg :: MCTerm FunctionArgumentL -> F.CTerm F.CExpressionL
untranslateArg :: Cxt NoHole (Sum MCSig) (K ()) FunctionArgumentL
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
untranslateArg (PositionalArgument' Cxt NoHole (Sum MCSig) (K ()) PositionalArgExpL
a) = CxtS NoHole MCSig (K ()) CExpressionL
-> Cxt NoHole (Sum CSig) (K ()) CExpressionL
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
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
$ Cxt NoHole (Sum 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 Cxt NoHole (Sum MCSig) (K ()) PositionalArgExpL
a

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

instance {-# OVERLAPPING #-} Untrans FunctionDeclIsCDeclarator where
  untrans :: forall l.
FunctionDeclIsCDeclarator (Cxt NoHole (Sum MCSig) (K ())) l
-> CTerm l
untrans (FunctionDeclIsCDeclarator (FunctionDecl' (CFunDeclAttrs' CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
dds CxtS NoHole MCSig (K ()) [CAttributeL]
attrs1 CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
asmNm CxtS NoHole MCSig (K ()) [CAttributeL]
attrs2) MCTerm IdentL
n 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]
-> Cxt NoHole (Sum CSig) (K ()) ()
-> CxtS NoHole CSig (K ()) 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]
-> Cxt NoHole (Sum 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 ()) :-> Cxt NoHole (Sum CSig) (K ())
untranslate CxtS NoHole MCSig (K ()) [CAttributeL]
attrs1) Cxt NoHole (Sum 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 ()) :-> Cxt NoHole (Sum CSig) (K ())
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 ()) :-> Cxt NoHole (Sum CSig) (K ())
untranslate CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
asmNm) (CxtS NoHole MCSig (K ()) [CAttributeL]
-> Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
untranslate CxtS NoHole MCSig (K ()) [CAttributeL]
attrs2) Cxt NoHole (Sum 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 CxtS NoHole MCSig (K ()) [FunctionParameterDeclL]
t = let ([CTerm CDeclarationL]
ds, Bool
b) = [MCTerm FunctionParameterDeclL]
-> ([CTerm CDeclarationL], Bool) -> ([CTerm CDeclarationL], Bool)
go (CxtS NoHole MCSig (K ()) [FunctionParameterDeclL]
-> [MCTerm FunctionParameterDeclL]
forall l.
Cxt NoHole (Sum MCSig) (K ()) [l]
-> [Cxt NoHole (Sum MCSig) (K ()) l]
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]
-> Cxt NoHole (Sum 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 l.
Typeable l =>
[Cxt NoHole (Sum CSig) (K ()) l]
-> Cxt NoHole (Sum CSig) (K ()) [l]
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 -> Cxt NoHole (Sum CSig) (K ()) BoolL
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) j.
(BoolF :<: f) =>
Bool -> Cxt h f 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' (Cxt NoHole (Sum 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' CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
dss CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
NilF' CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
Nothing' CxtS NoHole MCSig (K ()) [CAttributeL]
NilF')) Cxt NoHole (Sum MCSig) (K ()) (Maybe IdentL)
Nothing') : [MCTerm FunctionParameterDeclL]
ps) ([CTerm CDeclarationL]
l, Bool
b) =
               [MCTerm FunctionParameterDeclL]
-> ([CTerm CDeclarationL], Bool) -> ([CTerm CDeclarationL], Bool)
go [MCTerm FunctionParameterDeclL]
ps (Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
-> Cxt
     NoHole
     (Sum CSig)
     (K ())
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> Cxt NoHole (Sum 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]
-> Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
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' Cxt NoHole (Sum 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' (Cxt NoHole (Sum 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' CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
dss CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
dds CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
asmNm CxtS NoHole MCSig (K ()) [CAttributeL]
attrs)) Cxt NoHole (Sum MCSig) (K ()) (Maybe IdentL)
nOpt) : [MCTerm FunctionParameterDeclL]
ps) ([CTerm CDeclarationL]
l, Bool
b) =
               [MCTerm FunctionParameterDeclL]
-> ([CTerm CDeclarationL], Bool) -> ([CTerm CDeclarationL], Bool)
go [MCTerm FunctionParameterDeclL]
ps ((Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
-> Cxt
     NoHole
     (Sum CSig)
     (K ())
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> Cxt NoHole (Sum 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]
-> Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
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]
-> Cxt NoHole (Sum 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)
-> Cxt NoHole (Sum 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 Cxt NoHole (Sum MCSig) (K ()) (Maybe IdentL)
nOpt) (CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
-> Cxt NoHole (Sum CSig) (K ()) [CDerivedDeclaratorL]
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
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 ()) :-> Cxt NoHole (Sum CSig) (K ())
untranslate CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
asmNm) (CxtS NoHole MCSig (K ()) [CAttributeL]
-> Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
untranslate CxtS NoHole MCSig (K ()) [CAttributeL]
attrs) Cxt NoHole (Sum 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')) Cxt NoHole (Sum 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'] ([], Bool
b) = ([Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
-> Cxt
     NoHole
     (Sum CSig)
     (K ())
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> Cxt NoHole (Sum 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
-> Cxt NoHole (Sum CSig) (K ()) [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
 -> Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL])
-> Cxt NoHole (Sum CSig) (K ()) CDeclarationSpecifierL
-> Cxt NoHole (Sum CSig) (K ()) [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 (Cxt NoHole (Sum 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 Cxt NoHole (Sum 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' Cxt NoHole (Sum 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'] ([CTerm CDeclarationL]
l, Bool
b) = ([CTerm CDeclarationL]
l, Bool
True)
          go [] ([CTerm CDeclarationL]
l, Bool
b) = ([CTerm CDeclarationL]
l, Bool
b)

instance {-# OVERLAPPING #-} Untrans FunctionDefIsCFunctionDef where
  untrans :: forall l.
FunctionDefIsCFunctionDef (Cxt NoHole (Sum MCSig) (K ())) l
-> CTerm l
untrans (FunctionDefIsCFunctionDef
              (FunctionDef' (CFunDefAttrs' CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
dss
                                           (CFunDeclAttrs' CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
dds CxtS NoHole MCSig (K ()) [CAttributeL]
attrs1 CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
asmNm CxtS NoHole MCSig (K ()) [CAttributeL]
attrs2)
                                           CxtS NoHole MCSig (K ()) [CDeclarationL]
oldStyleParams)
                            MCTerm IdentL
n CxtS NoHole MCSig (K ()) [FunctionParameterL]
params CxtS NoHole MCSig (K ()) FunctionBodyL
body)) =
      Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
-> Cxt NoHole (Sum CSig) (K ()) CDeclaratorL
-> Cxt NoHole (Sum CSig) (K ()) [CDeclarationL]
-> CTerm CStatementL
-> Cxt NoHole (Sum CSig) (K ()) ()
-> CxtS NoHole CSig (K ()) 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]
-> Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
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]
-> Cxt NoHole (Sum 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]
-> Cxt NoHole (Sum 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 ()) :-> Cxt NoHole (Sum CSig) (K ())
untranslate CxtS NoHole MCSig (K ()) [CAttributeL]
attrs1) Cxt NoHole (Sum 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 ()) :-> Cxt NoHole (Sum CSig) (K ())
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 ()) :-> Cxt NoHole (Sum CSig) (K ())
untranslate CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
asmNm) (CxtS NoHole MCSig (K ()) [CAttributeL]
-> Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
untranslate CxtS NoHole MCSig (K ()) [CAttributeL]
attrs2) Cxt NoHole (Sum 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 ()) :-> Cxt NoHole (Sum CSig) (K ())
untranslate CxtS NoHole MCSig (K ()) [CDeclarationL]
oldStyleParams) (CxtS NoHole MCSig (K ()) CStatementL -> CTerm CStatementL
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
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) Cxt NoHole (Sum 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 CxtS NoHole MCSig (K ()) [FunctionParameterL]
t = case CxtS NoHole MCSig (K ()) [FunctionParameterL]
-> [MCTerm FunctionParameterL]
forall l.
Cxt NoHole (Sum MCSig) (K ()) [l]
-> [Cxt NoHole (Sum MCSig) (K ()) l]
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]
-> Cxt NoHole (Sum 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 -> Cxt NoHole (Sum CSig) (K ()) BoolL
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) j.
(BoolF :<: f) =>
Bool -> Cxt h f 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)
forall h (a :: * -> *).
CxtS h MCSig a FunctionParameterL
-> Maybe (CxtS h MCSig a COldStyleParamL)
projF -> Just (COldStyleParam' MCTerm IdentL
_)) : [MCTerm FunctionParameterL]
_) -> 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 l.
Typeable l =>
[Cxt NoHole (Sum CSig) (K ()) l]
-> Cxt NoHole (Sum CSig) (K ()) [l]
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)
forall h (a :: * -> *).
CxtS h MCSig a FunctionParameterL
-> Maybe (CxtS h MCSig a CSpecialParamL)
projF -> Just CxtS NoHole MCSig (K ()) CSpecialParamL
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]
-> Cxt NoHole (Sum 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
$ Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
-> Cxt
     NoHole
     (Sum CSig)
     (K ())
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> Cxt NoHole (Sum 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
-> Cxt NoHole (Sum CSig) (K ()) [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
 -> Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL])
-> Cxt NoHole (Sum CSig) (K ()) CDeclarationSpecifierL
-> Cxt NoHole (Sum CSig) (K ()) [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 (Cxt NoHole (Sum 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 Cxt NoHole (Sum 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' Cxt NoHole (Sum CSig) (K ()) ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF) (Bool -> Cxt NoHole (Sum CSig) (K ()) BoolL
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) j.
(BoolF :<: f) =>
Bool -> Cxt h f a BoolL
BoolF' Bool
False))
                        [MCTerm FunctionParameterL]
ps -> let ([CTerm CDeclarationL]
ds, Bool
b) = [MCTerm FunctionParameterL]
-> ([CTerm CDeclarationL], Bool) -> ([CTerm CDeclarationL], Bool)
go (CxtS NoHole MCSig (K ()) [FunctionParameterL]
-> [MCTerm FunctionParameterL]
forall l.
Cxt NoHole (Sum MCSig) (K ()) [l]
-> [Cxt NoHole (Sum MCSig) (K ()) l]
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]
-> Cxt NoHole (Sum 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 l.
Typeable l =>
[Cxt NoHole (Sum CSig) (K ()) l]
-> Cxt NoHole (Sum CSig) (K ()) [l]
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 -> Cxt NoHole (Sum CSig) (K ()) BoolL
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) j.
(BoolF :<: f) =>
Bool -> Cxt h f 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' 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' (Cxt NoHole (Sum 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' CxtS NoHole MCSig (K ()) [CDeclarationSpecifierL]
dss CxtS NoHole MCSig (K ()) [CDerivedDeclaratorL]
dds CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
asmNm CxtS NoHole MCSig (K ()) [CAttributeL]
attrs)) MCTerm IdentL
n) : [MCTerm FunctionParameterL]
ps) ([CTerm CDeclarationL]
l, Bool
b) =
               [MCTerm FunctionParameterL]
-> ([CTerm CDeclarationL], Bool) -> ([CTerm CDeclarationL], Bool)
go [MCTerm FunctionParameterL]
ps ((Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
-> Cxt
     NoHole
     (Sum CSig)
     (K ())
     [(Maybe CDeclaratorL, Maybe CInitializerL, Maybe CExpressionL)]
-> Cxt NoHole (Sum 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]
-> Cxt NoHole (Sum CSig) (K ()) [CDeclarationSpecifierL]
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
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]
-> Cxt NoHole (Sum 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 ()) :-> Cxt NoHole (Sum CSig) (K ())
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 ()) :-> Cxt NoHole (Sum CSig) (K ())
untranslate CxtS NoHole MCSig (K ()) (Maybe CStringLiteralL)
asmNm) (CxtS NoHole MCSig (K ()) [CAttributeL]
-> Cxt NoHole (Sum CSig) (K ()) [CAttributeL]
Cxt NoHole (Sum MCSig) (K ()) :-> Cxt NoHole (Sum CSig) (K ())
untranslate CxtS NoHole MCSig (K ()) [CAttributeL]
attrs) Cxt NoHole (Sum 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')) Cxt NoHole (Sum 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'] ([CTerm CDeclarationL]
l, Bool
b) = ([CTerm CDeclarationL]
l, Bool
True)
          go [] ([CTerm CDeclarationL]
l, Bool
b) = ([CTerm CDeclarationL]
l, Bool
b)

#endif