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

-- | 

module Cubix.Language.C.Parametric.Common.Types where

#ifndef ONLY_ONE_LANGUAGE
import Data.List ( (\\) )

import Language.Haskell.TH ( mkName )

import Data.Comp.Multi ( HFunctor, Term, project', project, (:-<:), CxtS, All, AnnCxtS )
import Data.Comp.Trans ( runCompTrans, makeSumType )

import Cubix.Language.C.Parametric.Full.Names
import Cubix.Language.C.Parametric.Full.Types as C
import Cubix.Language.Info
import Cubix.Language.Parametric.Derive
import Cubix.Language.Parametric.InjF
import Cubix.Language.Parametric.Syntax as P

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


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

data CDeclarationSpecifiersIsMultiLocalVarDeclCommonAttrs e l where
  CDeclarationSpecifiersIsMultiLocalVarDeclCommonAttrs :: e [CDeclarationSpecifierL] -> CDeclarationSpecifiersIsMultiLocalVarDeclCommonAttrs e MultiLocalVarDeclCommonAttrsL 

data CLocalVarAttrs e l where
  CLocalVarAttrs :: e [CDerivedDeclaratorL] -> e (Maybe CStringLiteralL) -> e [CAttributeL] -> CLocalVarAttrs e LocalVarDeclAttrsL

deriveAll [''CDeclarationSpecifiersIsMultiLocalVarDeclCommonAttrs, ''CLocalVarAttrs]

instance ( CDeclarationSpecifiersIsMultiLocalVarDeclCommonAttrs :-<: fs
         , All HFunctor fs
         ) => InjF fs [CDeclarationSpecifierL] MultiLocalVarDeclCommonAttrsL where
  injF :: CxtS h fs a [CDeclarationSpecifierL]
-> CxtS h fs a MultiLocalVarDeclCommonAttrsL
injF = CxtS h fs a [CDeclarationSpecifierL]
-> CxtS h fs a MultiLocalVarDeclCommonAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CDeclarationSpecifiersIsMultiLocalVarDeclCommonAttrs :-<: fs,
 InjF fs MultiLocalVarDeclCommonAttrsL j) =>
CxtS h fs a [CDeclarationSpecifierL] -> CxtS h fs a j
iCDeclarationSpecifiersIsMultiLocalVarDeclCommonAttrs

  projF' :: Cxt h (Sum fs :&: p) a MultiLocalVarDeclCommonAttrsL
-> Maybe (Cxt h (Sum fs :&: p) a [CDeclarationSpecifierL])
projF' (Cxt h (Sum fs :&: p) a MultiLocalVarDeclCommonAttrsL
-> Maybe
     (CDeclarationSpecifiersIsMultiLocalVarDeclCommonAttrs
        (Cxt h (Sum fs :&: p) a) MultiLocalVarDeclCommonAttrsL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' -> Just (CDeclarationSpecifiersIsMultiLocalVarDeclCommonAttrs x :: Cxt h (Sum fs :&: p) a [CDeclarationSpecifierL]
x)) = Cxt h (Sum fs :&: p) a [CDeclarationSpecifierL]
-> Maybe (Cxt h (Sum fs :&: p) a [CDeclarationSpecifierL])
forall a. a -> Maybe a
Just Cxt h (Sum fs :&: p) a [CDeclarationSpecifierL]
x
  projF' _                                                                          = Maybe (Cxt h (Sum fs :&: p) a [CDeclarationSpecifierL])
forall a. Maybe a
Nothing

createSortInclusionTypes [  ''MultiLocalVarDeclL,  ''CInitializerL, ''P.IdentL, ''C.CExpressionL, ''C.CExpressionL, ''C.CAssignOpL, ''P.AssignL,      ''C.CCompoundBlockItemL
                         ] [''CCompoundBlockItemL, ''LocalVarInitL, ''C.IdentL, ''P.LhsL,         ''P.RhsL,         ''P.AssignOpL,  ''C.CExpressionL, ''P.BlockItemL
                         ]
deriveAll [''MultiLocalVarDeclIsCCompoundBlockItem, ''CInitializerIsLocalVarInit, ''IdentIsIdent, ''CExpressionIsLhs,
           ''CExpressionIsRhs, ''CAssignOpIsAssignOp, ''AssignIsCExpression, ''CCompoundBlockItemIsBlockItem]
createSortInclusionInfers [  ''MultiLocalVarDeclL,  ''CInitializerL, ''P.IdentL, ''C.CExpressionL, ''C.CExpressionL, ''C.CAssignOpL, ''P.AssignL,         ''C.CCompoundBlockItemL
                          ] [''CCompoundBlockItemL, ''LocalVarInitL, ''C.IdentL, ''P.LhsL,         ''P.RhsL,         ''P.AssignOpL,  ''C.CExpressionL,    ''P.BlockItemL
                          ]

data CLabeledBlock e l where
  CLabeledBlock :: e [P.IdentL] -> e BlockL -> CLabeledBlock e C.CStatementL

deriveAll [''CLabeledBlock]


-----------------------------------------------------------------------------------
---------------       Function calls, decls, defns         ------------------------
-----------------------------------------------------------------------------------


-- | Modeling note: The language-c AST crams a lot of different kind of declarations together into a single
--   node with too many options. We're breaking it apart so we can e.g.: assume variables have identifiers when
--   it's possible to make that assumption
--  On the other hand, I've learned that "int;" is a valid line of C (at least according to Clang).
--  However, language-c can't parse it.

-- It took me hours to go through language-c's representation of functions/fundecls and understand everything.
-- I now see that much of the complexity is from the spec and not from language-c, though language-c could
-- factor things to make it more clear (and use a tree structure instead of a list structure for the derived declarators, perhaps).
-- Oh, and also it would be nice if it used distinct sorts for parameter declarations, general declarations, and struct declarations;
-- would really clean a lot up.
--
-- Below is the relevant pieces of abstract syntax and my notes on them

{-
data CFunctionDef a
  = CFunDef
    [CDeclarationSpecifier a] -- leaf (though note that it has the type information)
    (CDeclarator a)           -- declarator
    [CDeclaration a]          -- params
    (CStatement a)            -- Is always a CCompound
    a


data CDeclarator a
  = CDeclr (Maybe Ident) [CDerivedDeclarator a] (Maybe (CStringLiteral a)) [CAttribute a] a -- Is a function iff the first CDerivedDeclarator is CFunDeclr

data CDerivedDeclarator a
  = CFunDeclr (Either [Ident] ([CDeclaration a],Bool)) [CAttribute a] a -- CAttribute is leaf. The bool represents varargs.
    -- ^ Function declarator @CFunDeclr declr (old-style-params | new-style-params) c-attrs@
  | ...

data CDeclaration a
  = CDecl
    [CDeclarationSpecifier a] -- leaf
    [(Maybe (CDeclarator a),  -- declarator (may be omitted)
      Maybe (CInitializer a), -- should be nothing for params and fundecls
      Maybe (CExpression a))] -- should be nothing for params and fundecls
    a                         -- annotation
    | ...
-}

-- Note: We totally gloss over how C function decls are multi-decls: there is a return type attached but it's attached
-- to many functions. This is also totally not required by the IPT transformation.

-- According to the C spec (and language-c), a parameter list is either "old-style" (just a list of identifiers),
-- or "new-style" (each parameter must have a type). language-c will fail to parse a declaration that mixes
-- old and new style parameters. Yet Clang accepts them, because why not. C++ apparently removed old-style
-- parameters, and requires a type specifier for all declarations; both Clang in C++ mode and MSVC++ reject old-style
-- parameters.
--
-- As a small sin, I'm going to declare old-style parameters to be just a special case of new-style ones.
-- It makes my life easier, and that appears to be how Clang models them anyway.
--
-- ....except that I just learned about the "int f(a,b) int a; int b; { ... }" syntax. Ahhhhhh! When presented with that,
-- now GCC does treat them differently. Also, those "int a; int b;" decls can come in the other order.
-- No way around this: there is a non-context-free/non-syntactic constraint in the C spec, a constraint
-- between the language-specific and general notions of parameters. At the end of the day: we don't
-- have a good story for handling these kinds of constraints, other than seeing just how far
-- we can get without handling them.
--
-- This syntax can be used in function definitions, but not function declarations. So, we will do the merger
-- as planned for function declarations.

-- |
-- Quoth the spec:
-- If the declarator includes a parameter type list, the declaration of each parameter shall
-- include an identifier, except for the special case of a parameter list consisting of a single
-- parameter of type void, in which case there shall not be an identifier. No declaration list
-- shall follow.
--
-- AHHHHHHHHHHHHH!
-- I'm going to include another argument type for this. Thankfully, the planned
-- design for IPT will not be willing to mess with functions that have non-positional arguments,
-- so we're safe here

-- In function decls, since we don't model that void isn't a type,
-- this becomes just a special case of a normal param, and we don't include it
data CSpecialParamL
data CVoidArg (e :: * -> *) l where
  CVoidArg :: CVoidArg e CSpecialParamL

-- NOTE: I don't derive these all on one line because GHC crashes
-- Try again after upgrading GHC?
deriveAll [''CVoidArg]

pattern CVoidArg' :: (CVoidArg :-<: fs, All HFunctor fs) => CxtS h fs a CSpecialParamL
pattern $bCVoidArg' :: CxtS h fs a CSpecialParamL
$mCVoidArg' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(CVoidArg :-<: fs, All HFunctor fs) =>
CxtS h fs a CSpecialParamL -> (Void# -> r) -> (Void# -> r) -> r
CVoidArg' <- (project -> Just CVoidArg) where
  CVoidArg' = CxtS h fs a CSpecialParamL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CVoidArg :-<: fs, InjF fs CSpecialParamL j) =>
CxtS h fs a j
iCVoidArg

data CVarArgParam (e :: * -> *) l where
  CVarArgParam :: CVarArgParam e CSpecialParamL

deriveAll [''CVarArgParam]

pattern CVarArgParam' :: (CVarArgParam :-<: fs, All HFunctor fs) => CxtS h fs a CSpecialParamL
pattern $bCVarArgParam' :: CxtS h fs a CSpecialParamL
$mCVarArgParam' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(CVarArgParam :-<: fs, All HFunctor fs) =>
CxtS h fs a CSpecialParamL -> (Void# -> r) -> (Void# -> r) -> r
CVarArgParam' <- (project -> Just CVarArgParam) where
  CVarArgParam' = CxtS h fs a CSpecialParamL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CVarArgParam :-<: fs, InjF fs CSpecialParamL j) =>
CxtS h fs a j
iCVarArgParam

-- These can be used in function definitions, but not function declarations
data COldStyleParamL
data COldStyleParam e l where
  COldStyleParam :: e P.IdentL -> COldStyleParam e COldStyleParamL

deriveAll [''COldStyleParam]

pattern COldStyleParam' :: (COldStyleParam :-<: fs, All HFunctor fs) => CxtS h fs a P.IdentL -> CxtS h fs a COldStyleParamL
pattern $bCOldStyleParam' :: CxtS h fs a IdentL -> CxtS h fs a COldStyleParamL
$mCOldStyleParam' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(COldStyleParam :-<: fs, All HFunctor fs) =>
CxtS h fs a COldStyleParamL
-> (CxtS h fs a IdentL -> r) -> (Void# -> r) -> r
COldStyleParam' n <- (project -> Just (COldStyleParam n)) where
  COldStyleParam' n :: CxtS h fs a IdentL
n = CxtS h fs a IdentL -> CxtS h fs a COldStyleParamL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(COldStyleParam :-<: fs, InjF fs COldStyleParamL j) =>
CxtS h fs a IdentL -> CxtS h fs a j
iCOldStyleParam CxtS h fs a IdentL
n

-- Contains both fields from the first CDerivedDeclarator  in the original abstract syntax, as well as the CDeclarator its
data CFunDeclAttrs e l where
  CFunDeclAttrs :: e [C.CDerivedDeclaratorL] -> e [C.CAttributeL] -> e (Maybe (C.CStringLiteralL)) -> e [C.CAttributeL] -> CFunDeclAttrs e FunctionDeclAttrsL

deriveAll [''CFunDeclAttrs]

pattern CFunDeclAttrs' ::
  ( CFunDeclAttrs :-<: fs
  , All HFunctor fs
  ) => CxtS h fs a [C.CDerivedDeclaratorL]
  -> CxtS h fs a [C.CAttributeL]
  -> CxtS h fs a (Maybe (C.CStringLiteralL))
  -> CxtS h fs a [C.CAttributeL]
  -> CxtS h fs a FunctionDeclAttrsL
pattern $bCFunDeclAttrs' :: 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 FunctionDeclAttrsL
$mCFunDeclAttrs' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(CFunDeclAttrs :-<: fs, All HFunctor fs) =>
CxtS h fs a FunctionDeclAttrsL
-> (CxtS h fs a [CDerivedDeclaratorL]
    -> CxtS h fs a [CAttributeL]
    -> CxtS h fs a (Maybe CStringLiteralL)
    -> CxtS h fs a [CAttributeL]
    -> r)
-> (Void# -> r)
-> r
CFunDeclAttrs' dds attrs1 asmNm attrs2 <- (project -> Just (CFunDeclAttrs dds attrs1 asmNm attrs2)) where
  CFunDeclAttrs' dds :: CxtS h fs a [CDerivedDeclaratorL]
dds attrs1 :: CxtS h fs a [CAttributeL]
attrs1 asmNm :: CxtS h fs a (Maybe CStringLiteralL)
asmNm attrs2 :: CxtS h fs a [CAttributeL]
attrs2 = 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 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 CxtS h fs a [CDerivedDeclaratorL]
dds CxtS h fs a [CAttributeL]
attrs1 CxtS h fs a (Maybe CStringLiteralL)
asmNm CxtS h fs a [CAttributeL]
attrs2

data CFunDefAttrs e l where
  CFunDefAttrs :: e [CDeclarationSpecifierL] -> e FunctionDeclAttrsL -> e [CDeclarationL] -> CFunDefAttrs e FunctionDefAttrsL

deriveAll [''CFunDefAttrs]

pattern CFunDefAttrs' ::
  ( CFunDefAttrs :-<: fs
  , All HFunctor fs
  ) => CxtS h fs a [CDeclarationSpecifierL]
  -> CxtS h fs a FunctionDeclAttrsL
  -> CxtS h fs a [CDeclarationL]
  -> CxtS h fs a FunctionDefAttrsL
pattern $bCFunDefAttrs' :: CxtS h fs a [CDeclarationSpecifierL]
-> CxtS h fs a FunctionDeclAttrsL
-> CxtS h fs a [CDeclarationL]
-> CxtS h fs a FunctionDefAttrsL
$mCFunDefAttrs' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(CFunDefAttrs :-<: fs, All HFunctor fs) =>
CxtS h fs a FunctionDefAttrsL
-> (CxtS h fs a [CDeclarationSpecifierL]
    -> CxtS h fs a FunctionDeclAttrsL
    -> CxtS h fs a [CDeclarationL]
    -> r)
-> (Void# -> r)
-> r
CFunDefAttrs' dss fda decls <- (project -> Just (CFunDefAttrs dss fda decls)) where
  CFunDefAttrs' dss :: CxtS h fs a [CDeclarationSpecifierL]
dss fda :: CxtS h fs a FunctionDeclAttrsL
fda decls :: CxtS h fs a [CDeclarationL]
decls = CxtS h fs a [CDeclarationSpecifierL]
-> CxtS h fs a FunctionDeclAttrsL
-> CxtS h fs a [CDeclarationL]
-> CxtS h fs a 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 CxtS h fs a [CDeclarationSpecifierL]
dss CxtS h fs a FunctionDeclAttrsL
fda CxtS h fs a [CDeclarationL]
decls

-- Modeling note: The only difference between parameters and parameter decls
-- is that identifiers are optional for decls. Sharing an attributes type
data CFunParamAttrsL
data CFunParamAttrs e l where
  CFunParamAttrs :: e [CDeclarationSpecifierL] -> e [CDerivedDeclaratorL] -> e (Maybe CStringLiteralL) -> e [CAttributeL] -> CFunParamAttrs e CFunParamAttrsL

deriveAll [''CFunParamAttrs]

pattern CFunParamAttrs' ::
  ( CFunParamAttrs :-<: fs
  , All HFunctor fs
  ) => 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 CFunParamAttrsL
pattern $bCFunParamAttrs' :: 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 CFunParamAttrsL
$mCFunParamAttrs' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(CFunParamAttrs :-<: fs, All HFunctor fs) =>
CxtS h fs a CFunParamAttrsL
-> (CxtS h fs a [CDeclarationSpecifierL]
    -> CxtS h fs a [CDerivedDeclaratorL]
    -> CxtS h fs a (Maybe CStringLiteralL)
    -> CxtS h fs a [CAttributeL]
    -> r)
-> (Void# -> r)
-> r
CFunParamAttrs' dss dds asmNm attrs <- (project -> Just (CFunParamAttrs dss dds asmNm attrs)) where
  CFunParamAttrs' dss :: CxtS h fs a [CDeclarationSpecifierL]
dss dds :: CxtS h fs a [CDerivedDeclaratorL]
dds asmNm :: CxtS h fs a (Maybe CStringLiteralL)
asmNm attrs :: CxtS h fs a [CAttributeL]
attrs = 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 CFunParamAttrsL
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 h fs a [CDeclarationSpecifierL]
dss CxtS h fs a [CDerivedDeclaratorL]
dds CxtS h fs a (Maybe CStringLiteralL)
asmNm CxtS h fs a [CAttributeL]
attrs

createSortInclusionTypes [  ''P.FunctionCallL, ''C.CExpressionL, ''C.CExpressionL,      ''P.FunctionDeclL, ''CFunParamAttrsL,               ''CSpecialParamL,           ''P.FunctionDefL,  ''CFunParamAttrsL,   ''CSpecialParamL,       ''COldStyleParamL,      ''C.CStatementL
                         ] [''C.CExpressionL,  ''P.FunctionExpL, ''P.PositionalArgExpL, ''C.CDeclaratorL,  ''P.FunctionParameterDeclAttrsL, ''P.FunctionParameterDeclL, ''C.CFunctionDefL, ''P.ParameterAttrsL, ''P.FunctionParameterL, ''P.FunctionParameterL, ''P.FunctionBodyL
                         ]
deriveAll [ ''FunctionCallIsCExpression, ''CExpressionIsFunctionExp, ''CExpressionIsPositionalArgExp
          , ''FunctionDeclIsCDeclarator, ''CFunParamAttrsIsFunctionParameterDeclAttrs, ''CSpecialParamIsFunctionParameterDecl
          , ''FunctionDefIsCFunctionDef, ''CFunParamAttrsIsParameterAttrs, ''CSpecialParamIsFunctionParameter, ''COldStyleParamIsFunctionParameter
          , ''CStatementIsFunctionBody]
createSortInclusionInfers [  ''P.FunctionCallL, ''C.CExpressionL, ''C.CExpressionL,      ''P.FunctionDeclL, ''CFunParamAttrsL,               ''CSpecialParamL,           ''P.FunctionDefL,  ''CFunParamAttrsL,   ''CSpecialParamL,       ''COldStyleParamL,      ''C.CStatementL
                          ] [''C.CExpressionL,  ''P.FunctionExpL, ''P.PositionalArgExpL, ''C.CDeclaratorL,  ''P.FunctionParameterDeclAttrsL, ''P.FunctionParameterDeclL, ''C.CFunctionDefL, ''P.ParameterAttrsL, ''P.FunctionParameterL, ''P.FunctionParameterL, ''P.FunctionBodyL
                          ]



pattern CInteger' ::
  ( CInteger :-<: fs
  , CIntRepr :-<: fs
  , Flags :-<: fs
  , All HFunctor fs
  ) => Integer -> CxtS h fs a CIntegerL
pattern $bCInteger' :: Integer -> CxtS h fs a CIntegerL
$mCInteger' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(CInteger :-<: fs, CIntRepr :-<: fs, Flags :-<: fs,
 All HFunctor fs) =>
CxtS h fs a CIntegerL -> (Integer -> r) -> (Void# -> r) -> r
CInteger' n <- (project -> Just (CInteger n _ _)) where
  CInteger' n :: Integer
n = Integer
-> CxtS h fs a CIntReprL
-> CxtS h fs a FlagsL
-> CxtS h fs a CIntegerL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CInteger :-<: fs, InjF fs CIntegerL j) =>
Integer
-> CxtS h fs a CIntReprL -> CxtS h fs a FlagsL -> CxtS h fs a j
iCInteger Integer
n CxtS h fs a CIntReprL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CIntRepr :-<: fs, InjF fs CIntReprL j) =>
CxtS h fs a j
iDecRepr (Integer -> CxtS h fs a FlagsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(Flags :-<: fs, InjF fs FlagsL j) =>
Integer -> CxtS h fs a j
C.iFlags 0)

-- Not a wide string
pattern CString' :: (CString :-<: fs, All HFunctor fs) => String -> CxtS h fs a CStringL
pattern $bCString' :: String -> CxtS h fs a CStringL
$mCString' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(CString :-<: fs, All HFunctor fs) =>
CxtS h fs a CStringL -> (String -> r) -> (Void# -> r) -> r
CString' s <- (project -> Just (CString s False)) where
  CString' s :: String
s = String -> Bool -> CxtS h fs a CStringL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CString :-<: fs, InjF fs CStringL j) =>
String -> Bool -> CxtS h fs a j
iCString String
s Bool
False

-----------------------------------------------------------------------------------
----------------------         Declaring the IPS           ------------------------
-----------------------------------------------------------------------------------

do let cSortInjections = [ ''CDeclarationSpecifiersIsMultiLocalVarDeclCommonAttrs, ''MultiLocalVarDeclIsCCompoundBlockItem
                         , ''CInitializerIsLocalVarInit, ''IdentIsIdent, ''CExpressionIsLhs
                         , ''CExpressionIsRhs, ''CAssignOpIsAssignOp, ''AssignIsCExpression, ''CCompoundBlockItemIsBlockItem, ''IdentIsVarDeclBinder
                         , ''FunctionCallIsCExpression, ''CExpressionIsFunctionExp, ''CExpressionIsPositionalArgExp
                         , ''FunctionDeclIsCDeclarator, ''CFunParamAttrsIsFunctionParameterDeclAttrs, ''CSpecialParamIsFunctionParameterDecl
                         , ''FunctionDefIsCFunctionDef, ''CFunParamAttrsIsParameterAttrs, ''CSpecialParamIsFunctionParameter, ''COldStyleParamIsFunctionParameter
                         , ''CStatementIsFunctionBody
                         ]
   let cNewNodes       = [''CLocalVarAttrs, ''CLabeledBlock, ''CVoidArg, ''CVarArgParam, ''COldStyleParam, ''CFunDeclAttrs, ''CFunDefAttrs, ''CFunParamAttrs]
   let names = (cSigNames \\ [mkName "Ident", mkName "CFunctionDef"])
                          ++ cSortInjections
                          ++ cNewNodes
                          ++ [ ''OptLocalVarInit, ''SingleLocalVarDecl, ''MultiLocalVarDecl, ''P.Ident, ''Assign
                             , ''AssignOpEquals, ''Block, ''EmptyBlockEnd
                             , ''FunctionCall, ''EmptyFunctionCallAttrs, ''FunctionArgumentList, ''PositionalArgument
                             , ''FunctionDecl, ''PositionalParameterDeclOptionalIdent
                             , ''FunctionDef, ''PositionalParameter
                             ]
   sumDec <- runCompTrans $ makeSumType "MCSig" names
   return sumDec

type instance InjectableSorts MCSig MultiLocalVarDeclL = '[CCompoundBlockItemL]

type MCTerm = Term MCSig
type MCTermLab = TermLab MCSig

type MCCxt h a = CxtS h MCSig a
type MCCxtA h a p = AnnCxtS p h MCSig a


-----------------------------------------------------------------------------------
----------------------         Sort injections             ------------------------
-----------------------------------------------------------------------------------

-- Some extra work needed to make this work on Context's
instance InjF MCSig AssignL BlockItemL where
  injF :: CxtS h MCSig a AssignL -> CxtS h MCSig a BlockItemL
injF = CxtS h MCSig a CStatementL -> CxtS h MCSig a BlockItemL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CCompoundBlockItem :-<: fs, InjF fs CCompoundBlockItemL j) =>
CxtS h fs a CStatementL -> CxtS h fs a j
C.iCBlockStmt (CxtS h MCSig a CStatementL -> CxtS h MCSig a BlockItemL)
-> (CxtS h MCSig a AssignL -> CxtS h MCSig a CStatementL)
-> CxtS h MCSig a AssignL
-> CxtS h MCSig a BlockItemL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((CxtS h MCSig a (Maybe CExpressionL)
 -> CxtS h MCSig a () -> CxtS h MCSig a CStatementL)
-> CxtS h MCSig a ()
-> CxtS h MCSig a (Maybe CExpressionL)
-> CxtS h MCSig a CStatementL
forall a b c. (a -> b -> c) -> b -> a -> c
flip CxtS h MCSig a (Maybe CExpressionL)
-> CxtS h MCSig a () -> CxtS h MCSig a CStatementL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CStatement :-<: fs, InjF fs CStatementL j) =>
CxtS h fs a (Maybe CExpressionL) -> CxtS h fs a () -> CxtS h fs a j
C.iCExpr CxtS h MCSig a ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF) (CxtS h MCSig a (Maybe CExpressionL) -> CxtS h MCSig a CStatementL)
-> (CxtS h MCSig a AssignL -> CxtS h MCSig a (Maybe CExpressionL))
-> CxtS h MCSig a AssignL
-> CxtS h MCSig a CStatementL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtS h MCSig a CExpressionL -> CxtS h MCSig a (Maybe CExpressionL)
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
(MaybeF :-<: fs, InjF fs (Maybe l) l', Typeable l) =>
CxtS h fs a l -> CxtS h fs a l'
iJustF (CxtS h MCSig a CExpressionL
 -> CxtS h MCSig a (Maybe CExpressionL))
-> (CxtS h MCSig a AssignL -> CxtS h MCSig a CExpressionL)
-> CxtS h MCSig a AssignL
-> CxtS h MCSig a (Maybe CExpressionL)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(AssignIsCExpression :-<: fs, InjF fs CExpressionL j) =>
CxtS h fs a AssignL -> CxtS h fs a j
forall _ (_ :: * -> *).
CxtS _ MCSig _ AssignL -> CxtS _ MCSig _ CExpressionL
iAssignIsCExpression :: (MCCxt _ _) AssignL -> (MCCxt _ _) CExpressionL)
  projF' :: Cxt h (Sum MCSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MCSig :&: p) a AssignL)
projF' t :: Cxt h (Sum MCSig :&: p) a BlockItemL
t = do
    (MCCxtA h a p CCompoundBlockItemL
b :: MCCxtA _ _ _ CCompoundBlockItemL) <- Cxt h (Sum MCSig :&: p) a BlockItemL
-> Maybe (MCCxtA h a p CCompoundBlockItemL)
forall (fs :: [(* -> *) -> * -> *]) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
projF' Cxt h (Sum MCSig :&: p) a BlockItemL
t
    CBlockStmt s :: Cxt h (Sum MCSig :&: p) a CStatementL
s <- MCCxtA h a p CCompoundBlockItemL
-> Maybe
     (CCompoundBlockItem
        (Cxt h (Sum MCSig :&: p) a) CCompoundBlockItemL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' MCCxtA h a p CCompoundBlockItemL
b
    CExpr me :: Cxt h (Sum MCSig :&: p) a (Maybe CExpressionL)
me _ <- Cxt h (Sum MCSig :&: p) a CStatementL
-> Maybe (CStatement (Cxt h (Sum MCSig :&: p) a) CStatementL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MCSig :&: p) a CStatementL
s
    let JustA' e :: Cxt h (Sum MCSig :&: p) a CExpressionL
e = Cxt h (Sum MCSig :&: p) a (Maybe CExpressionL)
me
    Cxt h (Sum MCSig :&: p) a CExpressionL
-> Maybe (Cxt h (Sum MCSig :&: p) a AssignL)
forall (fs :: [(* -> *) -> * -> *]) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
projF' Cxt h (Sum MCSig :&: p) a CExpressionL
e

instance InjF MCSig MultiLocalVarDeclL BlockItemL where
  injF :: CxtS h MCSig a MultiLocalVarDeclL -> CxtS h MCSig a BlockItemL
injF = CxtS h MCSig a MultiLocalVarDeclL -> CxtS h MCSig a BlockItemL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(MultiLocalVarDeclIsCCompoundBlockItem :-<: fs,
 InjF fs CCompoundBlockItemL j) =>
CxtS h fs a MultiLocalVarDeclL -> CxtS h fs a j
iMultiLocalVarDeclIsCCompoundBlockItem
  projF' :: Cxt h (Sum MCSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MCSig :&: p) a MultiLocalVarDeclL)
projF' t :: Cxt h (Sum MCSig :&: p) a BlockItemL
t = do
    (MCCxtA h a p CCompoundBlockItemL
s :: (MCCxtA _ _ _) CCompoundBlockItemL) <- Cxt h (Sum MCSig :&: p) a BlockItemL
-> Maybe (MCCxtA h a p CCompoundBlockItemL)
forall (fs :: [(* -> *) -> * -> *]) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
projF' Cxt h (Sum MCSig :&: p) a BlockItemL
t
    MCCxtA h a p CCompoundBlockItemL
-> Maybe (Cxt h (Sum MCSig :&: p) a MultiLocalVarDeclL)
forall (fs :: [(* -> *) -> * -> *]) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
projF' MCCxtA h a p CCompoundBlockItemL
s

instance InjF MCSig P.IdentL LhsL where
  injF :: CxtS h MCSig a IdentL -> CxtS h MCSig a LhsL
injF n :: CxtS h MCSig a IdentL
n = CxtS h MCSig a IdentL -> CxtS h MCSig a () -> CxtS h MCSig a LhsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CExpression :-<: fs, InjF fs CExpressionL j) =>
CxtS h fs a IdentL -> CxtS h fs a () -> CxtS h fs a j
iCVar (CxtS h MCSig a IdentL -> CxtS h MCSig a IdentL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF CxtS h MCSig a IdentL
n) CxtS h MCSig a ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF
  projF' :: Cxt h (Sum MCSig :&: p) a LhsL
-> Maybe (Cxt h (Sum MCSig :&: p) a IdentL)
projF' n :: Cxt h (Sum MCSig :&: p) a LhsL
n = do
    (MCCxtA h a p CExpressionL
x :: (MCCxtA _ _ _) CExpressionL) <- Cxt h (Sum MCSig :&: p) a LhsL -> Maybe (MCCxtA h a p CExpressionL)
forall (fs :: [(* -> *) -> * -> *]) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
projF' Cxt h (Sum MCSig :&: p) a LhsL
n
    CVar y :: Cxt h (Sum MCSig :&: p) a IdentL
y _ <- MCCxtA h a p CExpressionL
-> Maybe (CExpression (Cxt h (Sum MCSig :&: p) a) CExpressionL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' MCCxtA h a p CExpressionL
x
    Cxt h (Sum MCSig :&: p) a IdentL
-> Maybe (Cxt h (Sum MCSig :&: p) a IdentL)
forall (fs :: [(* -> *) -> * -> *]) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
projF' Cxt h (Sum MCSig :&: p) a IdentL
y

instance InjF MCSig P.IdentL CExpressionL where
  injF :: CxtS h MCSig a IdentL -> CxtS h MCSig a CExpressionL
injF n :: CxtS h MCSig a IdentL
n = CxtS h MCSig a IdentL
-> CxtS h MCSig a () -> CxtS h MCSig a CExpressionL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CExpression :-<: fs, InjF fs CExpressionL j) =>
CxtS h fs a IdentL -> CxtS h fs a () -> CxtS h fs a j
iCVar (CxtS h MCSig a IdentL -> CxtS h MCSig a IdentL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF CxtS h MCSig a IdentL
n) CxtS h MCSig a ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF
  projF' :: Cxt h (Sum MCSig :&: p) a CExpressionL
-> Maybe (Cxt h (Sum MCSig :&: p) a IdentL)
projF' e :: Cxt h (Sum MCSig :&: p) a CExpressionL
e = do
    CVar x :: Cxt h (Sum MCSig :&: p) a IdentL
x _ <- Cxt h (Sum MCSig :&: p) a CExpressionL
-> Maybe (CExpression (Cxt h (Sum MCSig :&: p) a) CExpressionL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MCSig :&: p) a CExpressionL
e
    Cxt h (Sum MCSig :&: p) a IdentL
-> Maybe (Cxt h (Sum MCSig :&: p) a IdentL)
forall (fs :: [(* -> *) -> * -> *]) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
projF' Cxt h (Sum MCSig :&: p) a IdentL
x

instance InjF MCSig CStatementL BlockItemL where
  injF :: CxtS h MCSig a CStatementL -> CxtS h MCSig a BlockItemL
injF = CxtS h MCSig a CStatementL -> CxtS h MCSig a BlockItemL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CCompoundBlockItem :-<: fs, InjF fs CCompoundBlockItemL j) =>
CxtS h fs a CStatementL -> CxtS h fs a j
iCBlockStmt
  projF' :: Cxt h (Sum MCSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MCSig :&: p) a CStatementL)
projF' s :: Cxt h (Sum MCSig :&: p) a BlockItemL
s = do
    CCompoundBlockItemIsBlockItem x :: Cxt h (Sum MCSig :&: p) a CCompoundBlockItemL
x <- Cxt h (Sum MCSig :&: p) a BlockItemL
-> Maybe
     (CCompoundBlockItemIsBlockItem
        (Cxt h (Sum MCSig :&: p) a) BlockItemL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MCSig :&: p) a BlockItemL
s
    CBlockStmt y :: Cxt h (Sum MCSig :&: p) a CStatementL
y <- Cxt h (Sum MCSig :&: p) a CCompoundBlockItemL
-> Maybe
     (CCompoundBlockItem
        (Cxt h (Sum MCSig :&: p) a) CCompoundBlockItemL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MCSig :&: p) a CCompoundBlockItemL
x
    Cxt h (Sum MCSig :&: p) a CStatementL
-> Maybe (Cxt h (Sum MCSig :&: p) a CStatementL)
forall (m :: * -> *) a. Monad m => a -> m a
return Cxt h (Sum MCSig :&: p) a CStatementL
y

instance InjF MCSig CExpressionL LocalVarInitL where
  injF :: CxtS h MCSig a CExpressionL -> CxtS h MCSig a LocalVarInitL
injF x :: CxtS h MCSig a CExpressionL
x = CxtS h MCSig a CExpressionL
-> CxtS h MCSig a () -> CxtS h MCSig a LocalVarInitL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CInitializer :-<: fs, InjF fs CInitializerL j) =>
CxtS h fs a CExpressionL -> CxtS h fs a () -> CxtS h fs a j
iCInitExpr CxtS h MCSig a CExpressionL
x CxtS h MCSig a ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF
  projF' :: Cxt h (Sum MCSig :&: p) a LocalVarInitL
-> Maybe (Cxt h (Sum MCSig :&: p) a CExpressionL)
projF' i :: Cxt h (Sum MCSig :&: p) a LocalVarInitL
i = do
    CInitializerIsLocalVarInit x :: Cxt h (Sum MCSig :&: p) a CInitializerL
x <- Cxt h (Sum MCSig :&: p) a LocalVarInitL
-> Maybe
     (CInitializerIsLocalVarInit
        (Cxt h (Sum MCSig :&: p) a) LocalVarInitL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MCSig :&: p) a LocalVarInitL
i
    CInitExpr e :: Cxt h (Sum MCSig :&: p) a CExpressionL
e _ <- Cxt h (Sum MCSig :&: p) a CInitializerL
-> Maybe (CInitializer (Cxt h (Sum MCSig :&: p) a) CInitializerL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MCSig :&: p) a CInitializerL
x
    Cxt h (Sum MCSig :&: p) a CExpressionL
-> Maybe (Cxt h (Sum MCSig :&: p) a CExpressionL)
forall (m :: * -> *) a. Monad m => a -> m a
return Cxt h (Sum MCSig :&: p) a CExpressionL
e

instance InjF MCSig P.IdentL FunctionExpL where
  injF :: CxtS h MCSig a IdentL -> CxtS h MCSig a FunctionExpL
injF x :: CxtS h MCSig a IdentL
x = CxtS h MCSig a IdentL
-> CxtS h MCSig a () -> CxtS h MCSig a FunctionExpL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CExpression :-<: fs, InjF fs CExpressionL j) =>
CxtS h fs a IdentL -> CxtS h fs a () -> CxtS h fs a j
iCVar (CxtS h MCSig a IdentL -> CxtS h MCSig a IdentL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF CxtS h MCSig a IdentL
x) CxtS h MCSig a ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF

  projF' :: Cxt h (Sum MCSig :&: p) a FunctionExpL
-> Maybe (Cxt h (Sum MCSig :&: p) a IdentL)
projF' f :: Cxt h (Sum MCSig :&: p) a FunctionExpL
f
   | Just (CExpressionIsFunctionExp e :: Cxt h (Sum MCSig :&: p) a CExpressionL
e) <- Cxt h (Sum MCSig :&: p) a FunctionExpL
-> Maybe
     (CExpressionIsFunctionExp (Cxt h (Sum MCSig :&: p) a) FunctionExpL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MCSig :&: p) a FunctionExpL
f
   , Just (CVar n :: Cxt h (Sum MCSig :&: p) a IdentL
n _) <- Cxt h (Sum MCSig :&: p) a CExpressionL
-> Maybe (CExpression (Cxt h (Sum MCSig :&: p) a) CExpressionL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MCSig :&: p) a CExpressionL
e
   , Just (IdentIsIdent i :: Cxt h (Sum MCSig :&: p) a IdentL
i) <- Cxt h (Sum MCSig :&: p) a IdentL
-> Maybe (IdentIsIdent (Cxt h (Sum MCSig :&: p) a) IdentL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MCSig :&: p) a IdentL
n
   = Cxt h (Sum MCSig :&: p) a IdentL
-> Maybe (Cxt h (Sum MCSig :&: p) a IdentL)
forall a. a -> Maybe a
Just Cxt h (Sum MCSig :&: p) a IdentL
i
  projF' _ = Maybe (Cxt h (Sum MCSig :&: p) a IdentL)
forall a. Maybe a
Nothing

instance InjF MCSig P.IdentL PositionalArgExpL where
  injF :: CxtS h MCSig a IdentL -> CxtS h MCSig a PositionalArgExpL
injF n :: CxtS h MCSig a IdentL
n = CxtS h MCSig a IdentL
-> CxtS h MCSig a () -> CxtS h MCSig a PositionalArgExpL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CExpression :-<: fs, InjF fs CExpressionL j) =>
CxtS h fs a IdentL -> CxtS h fs a () -> CxtS h fs a j
iCVar (CxtS h MCSig a IdentL -> CxtS h MCSig a IdentL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF CxtS h MCSig a IdentL
n) CxtS h MCSig a ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF

  projF' :: Cxt h (Sum MCSig :&: p) a PositionalArgExpL
-> Maybe (Cxt h (Sum MCSig :&: p) a IdentL)
projF' a :: Cxt h (Sum MCSig :&: p) a PositionalArgExpL
a
   | Just (CExpressionIsPositionalArgExp e :: Cxt h (Sum MCSig :&: p) a CExpressionL
e) <- Cxt h (Sum MCSig :&: p) a PositionalArgExpL
-> Maybe
     (CExpressionIsPositionalArgExp
        (Cxt h (Sum MCSig :&: p) a) PositionalArgExpL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MCSig :&: p) a PositionalArgExpL
a
   , Just (CVar n :: Cxt h (Sum MCSig :&: p) a IdentL
n _) <- Cxt h (Sum MCSig :&: p) a CExpressionL
-> Maybe (CExpression (Cxt h (Sum MCSig :&: p) a) CExpressionL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MCSig :&: p) a CExpressionL
e = Cxt h (Sum MCSig :&: p) a IdentL
-> Maybe (Cxt h (Sum MCSig :&: p) a IdentL)
forall (fs :: [(* -> *) -> * -> *]) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
projF' Cxt h (Sum MCSig :&: p) a IdentL
n
  projF' _ = Maybe (Cxt h (Sum MCSig :&: p) a IdentL)
forall a. Maybe a
Nothing

#endif