{-# OPTIONS_HADDOCK hide #-}

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

-- | 

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

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

import Language.Haskell.TH ( mkName )

import Data.Comp.Multi ( Node, 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

deriveAllButSortInjection [''CDeclarationSpecifiersIsMultiLocalVarDeclCommonAttrs, ''CLocalVarAttrs]

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

  projF' :: forall h p (a :: * -> *).
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 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' Cxt h (Sum fs :&: p) a MultiLocalVarDeclCommonAttrsL
_                                                                          = 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
                         ]
deriveAllButSortInjection [''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]

-----------------------------------------------------------------------------------
------------------------       Control-flow     -----------------------------------
-----------------------------------------------------------------------------------

data CForInitL

data CForInit e l where
  CForInitEmpty ::                         CForInit e CForInitL
  CForInitExp   :: e CExpressionL       -> CForInit e CForInitL
  CForInitDecl  :: e MultiLocalVarDeclL -> CForInit e CForInitL

data CFor e l where
  CFor :: e CForInitL -> e (Maybe CExpressionL) -> e (Maybe CExpressionL) -> e CStatementL -> CFor e CStatementL

deriveAll [''CForInit, ''CFor]

-----------------------------------------------------------------------------------
---------------       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 :: Node 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]

data CVarArgParam :: Node where
  CVarArgParam :: CVarArgParam e CSpecialParamL

deriveAll [''CVarArgParam]

-- 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]

-- 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]

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

deriveAll [''CFunDefAttrs]

-- 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]

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
                         ]
deriveAllButSortInjection [ ''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 $mCInteger' :: forall {r} {fs :: Signature} {h} {a :: * -> *}.
(CInteger :-<: fs, CIntRepr :-<: fs, Flags :-<: fs,
 All HFunctor fs) =>
CxtS h fs a CIntegerL -> (Integer -> r) -> ((# #) -> r) -> r
$bCInteger' :: forall (fs :: Signature) h (a :: * -> *).
(CInteger :-<: fs, CIntRepr :-<: fs, Flags :-<: fs,
 All HFunctor fs) =>
Integer -> CxtS h fs a CIntegerL
CInteger' n <- (project -> Just (CInteger n _ _)) where
  CInteger' Integer
n = Integer
-> CxtS h fs a CIntReprL
-> CxtS h fs a FlagsL
-> CxtS h fs a CIntegerL
forall h (fs :: Signature) (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 :: Signature) (a :: * -> *) j.
(CIntRepr :-<: fs, InjF fs CIntReprL j) =>
CxtS h fs a j
iDecRepr (Integer -> CxtS h fs a FlagsL
forall h (fs :: Signature) (a :: * -> *) j.
(Flags :-<: fs, InjF fs FlagsL j) =>
Integer -> CxtS h fs a j
C.iFlags Integer
0)

-- Not a wide string
pattern CString' :: (CString :-<: fs, All HFunctor fs) => String -> CxtS h fs a CStringL
pattern $mCString' :: forall {r} {fs :: Signature} {h} {a :: * -> *}.
(CString :-<: fs, All HFunctor fs) =>
CxtS h fs a CStringL -> (String -> r) -> ((# #) -> r) -> r
$bCString' :: forall (fs :: Signature) h (a :: * -> *).
(CString :-<: fs, All HFunctor fs) =>
String -> CxtS h fs a CStringL
CString' s <- (project -> Just (CString s False)) where
  CString' String
s = String -> Bool -> CxtS h fs a CStringL
forall h (fs :: Signature) (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, ''CForInit, ''CFor]
   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 :: forall h (a :: * -> *).
CxtS h MCSig a AssignL -> CxtS h MCSig a BlockItemL
injF = CxtS h MCSig a CStatementL -> CxtS h MCSig a BlockItemL
forall h (fs :: Signature) (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 :: Signature) (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 :: Signature) (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 :: Signature) 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
. (CxtS w MCSig w AssignL -> CxtS w MCSig w CExpressionL
forall h (fs :: Signature) (a :: * -> *) j.
(AssignIsCExpression :-<: fs, InjF fs CExpressionL j) =>
CxtS h fs a AssignL -> CxtS h fs a j
forall {w} {w :: * -> *}.
CxtS w MCSig w AssignL -> CxtS w MCSig w CExpressionL
iAssignIsCExpression :: (MCCxt _ _) AssignL -> (MCCxt _ _) CExpressionL)
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MCSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MCSig :&: p) a AssignL)
projF' 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 :: Signature) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
forall h p (a :: * -> *).
Cxt h (Sum MCSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MCSig :&: p) a CCompoundBlockItemL)
projF' Cxt h (Sum MCSig :&: p) a BlockItemL
t
    CBlockStmt 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 Cxt h (Sum MCSig :&: p) a (Maybe CExpressionL)
me Cxt h (Sum MCSig :&: p) a ()
_ <- 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' 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 :: Signature) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
forall h p (a :: * -> *).
Cxt h (Sum MCSig :&: p) a CExpressionL
-> Maybe (Cxt h (Sum MCSig :&: p) a AssignL)
projF' Cxt h (Sum MCSig :&: p) a CExpressionL
e

instance InjF MCSig MultiLocalVarDeclL BlockItemL where
  injF :: forall h (a :: * -> *).
CxtS h MCSig a MultiLocalVarDeclL -> CxtS h MCSig a BlockItemL
injF = CxtS h MCSig a MultiLocalVarDeclL -> CxtS h MCSig a BlockItemL
forall h (fs :: Signature) (a :: * -> *) j.
(MultiLocalVarDeclIsCCompoundBlockItem :-<: fs,
 InjF fs CCompoundBlockItemL j) =>
CxtS h fs a MultiLocalVarDeclL -> CxtS h fs a j
iMultiLocalVarDeclIsCCompoundBlockItem
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MCSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MCSig :&: p) a MultiLocalVarDeclL)
projF' 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 :: Signature) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
forall h p (a :: * -> *).
Cxt h (Sum MCSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MCSig :&: p) a CCompoundBlockItemL)
projF' Cxt h (Sum MCSig :&: p) a BlockItemL
t
    MCCxtA h a p CCompoundBlockItemL
-> Maybe (Cxt h (Sum MCSig :&: p) a MultiLocalVarDeclL)
forall (fs :: Signature) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
forall h p (a :: * -> *).
Cxt h (Sum MCSig :&: p) a CCompoundBlockItemL
-> Maybe (Cxt h (Sum MCSig :&: p) a MultiLocalVarDeclL)
projF' MCCxtA h a p CCompoundBlockItemL
s

instance InjF MCSig P.IdentL LhsL where
  injF :: forall h (a :: * -> *).
CxtS h MCSig a IdentL -> CxtS h MCSig a LhsL
injF CxtS h MCSig a IdentL
n = CxtS h MCSig a IdentL -> CxtS h MCSig a () -> CxtS h MCSig a LhsL
forall h (fs :: Signature) (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 :: Signature) 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 IdentL
injF CxtS h MCSig a IdentL
n) CxtS h MCSig a ()
forall h (fs :: Signature) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MCSig :&: p) a LhsL
-> Maybe (Cxt h (Sum MCSig :&: p) a IdentL)
projF' 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 :: Signature) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
forall h p (a :: * -> *).
Cxt h (Sum MCSig :&: p) a LhsL
-> Maybe (Cxt h (Sum MCSig :&: p) a CExpressionL)
projF' Cxt h (Sum MCSig :&: p) a LhsL
n
    CVar Cxt h (Sum MCSig :&: p) a IdentL
y Cxt h (Sum MCSig :&: p) a ()
_ <- 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 :: Signature) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
forall h p (a :: * -> *).
Cxt h (Sum MCSig :&: p) a IdentL
-> Maybe (Cxt h (Sum MCSig :&: p) a IdentL)
projF' Cxt h (Sum MCSig :&: p) a IdentL
y

instance InjF MCSig P.IdentL CExpressionL where
  injF :: forall h (a :: * -> *).
CxtS h MCSig a IdentL -> CxtS h MCSig a CExpressionL
injF CxtS h MCSig a IdentL
n = CxtS h MCSig a IdentL
-> CxtS h MCSig a () -> CxtS h MCSig a CExpressionL
forall h (fs :: Signature) (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 :: Signature) 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 IdentL
injF CxtS h MCSig a IdentL
n) CxtS h MCSig a ()
forall h (fs :: Signature) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MCSig :&: p) a CExpressionL
-> Maybe (Cxt h (Sum MCSig :&: p) a IdentL)
projF' Cxt h (Sum MCSig :&: p) a CExpressionL
e = do
    CVar Cxt h (Sum MCSig :&: p) a IdentL
x Cxt h (Sum MCSig :&: p) a ()
_ <- 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 :: Signature) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
forall h p (a :: * -> *).
Cxt h (Sum MCSig :&: p) a IdentL
-> Maybe (Cxt h (Sum MCSig :&: p) a IdentL)
projF' Cxt h (Sum MCSig :&: p) a IdentL
x

instance InjF MCSig CStatementL BlockItemL where
  injF :: forall h (a :: * -> *).
CxtS h MCSig a CStatementL -> CxtS h MCSig a BlockItemL
injF = CxtS h MCSig a CStatementL -> CxtS h MCSig a BlockItemL
forall h (fs :: Signature) (a :: * -> *) j.
(CCompoundBlockItem :-<: fs, InjF fs CCompoundBlockItemL j) =>
CxtS h fs a CStatementL -> CxtS h fs a j
iCBlockStmt
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MCSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MCSig :&: p) a CStatementL)
projF' Cxt h (Sum MCSig :&: p) a BlockItemL
s = do
    CCompoundBlockItemIsBlockItem 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 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 a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Cxt h (Sum MCSig :&: p) a CStatementL
y

instance InjF MCSig CExpressionL LocalVarInitL where
  injF :: forall h (a :: * -> *).
CxtS h MCSig a CExpressionL -> CxtS h MCSig a LocalVarInitL
injF CxtS h MCSig a CExpressionL
x = CxtS h MCSig a CExpressionL
-> CxtS h MCSig a () -> CxtS h MCSig a LocalVarInitL
forall h (fs :: Signature) (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 :: Signature) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MCSig :&: p) a LocalVarInitL
-> Maybe (Cxt h (Sum MCSig :&: p) a CExpressionL)
projF' Cxt h (Sum MCSig :&: p) a LocalVarInitL
i = do
    CInitializerIsLocalVarInit 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 Cxt h (Sum MCSig :&: p) a CExpressionL
e Cxt h (Sum MCSig :&: p) a ()
_ <- 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 a. a -> Maybe a
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 :: forall h (a :: * -> *).
CxtS h MCSig a IdentL -> CxtS h MCSig a FunctionExpL
injF CxtS h MCSig a IdentL
x = CxtS h MCSig a IdentL
-> CxtS h MCSig a () -> CxtS h MCSig a FunctionExpL
forall h (fs :: Signature) (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 :: Signature) 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 IdentL
injF CxtS h MCSig a IdentL
x) CxtS h MCSig a ()
forall h (fs :: Signature) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF

  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MCSig :&: p) a FunctionExpL
-> Maybe (Cxt h (Sum MCSig :&: p) a IdentL)
projF' Cxt h (Sum MCSig :&: p) a FunctionExpL
f
   | Just (CExpressionIsFunctionExp 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 Cxt h (Sum MCSig :&: p) a IdentL
n Cxt h (Sum MCSig :&: p) a ()
_) <- 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 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' Cxt h (Sum MCSig :&: p) a FunctionExpL
_ = Maybe (Cxt h (Sum MCSig :&: p) a IdentL)
forall a. Maybe a
Nothing

instance InjF MCSig P.IdentL PositionalArgExpL where
  injF :: forall h (a :: * -> *).
CxtS h MCSig a IdentL -> CxtS h MCSig a PositionalArgExpL
injF CxtS h MCSig a IdentL
n = CxtS h MCSig a IdentL
-> CxtS h MCSig a () -> CxtS h MCSig a PositionalArgExpL
forall h (fs :: Signature) (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 :: Signature) 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 IdentL
injF CxtS h MCSig a IdentL
n) CxtS h MCSig a ()
forall h (fs :: Signature) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF

  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MCSig :&: p) a PositionalArgExpL
-> Maybe (Cxt h (Sum MCSig :&: p) a IdentL)
projF' Cxt h (Sum MCSig :&: p) a PositionalArgExpL
a
   | Just (CExpressionIsPositionalArgExp 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 Cxt h (Sum MCSig :&: p) a IdentL
n Cxt h (Sum MCSig :&: p) a ()
_) <- 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 :: Signature) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
forall h p (a :: * -> *).
Cxt h (Sum MCSig :&: p) a IdentL
-> Maybe (Cxt h (Sum MCSig :&: p) a IdentL)
projF' Cxt h (Sum MCSig :&: p) a IdentL
n
  projF' Cxt h (Sum MCSig :&: p) a PositionalArgExpL
_ = Maybe (Cxt h (Sum MCSig :&: p) a IdentL)
forall a. Maybe a
Nothing

instance InjF MCSig FunctionCallL RhsL where
  injF :: forall h (a :: * -> *).
CxtS h MCSig a FunctionCallL -> CxtS h MCSig a RhsL
injF = CxtS h MCSig a FunctionCallL -> CxtS h MCSig a RhsL
forall h (fs :: Signature) (a :: * -> *) j.
(FunctionCallIsCExpression :-<: fs, InjF fs CExpressionL j) =>
CxtS h fs a FunctionCallL -> CxtS h fs a j
iFunctionCallIsCExpression
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MCSig :&: p) a RhsL
-> Maybe (Cxt h (Sum MCSig :&: p) a FunctionCallL)
projF' Cxt h (Sum MCSig :&: p) a RhsL
f
   | Just (CExpressionIsRhs Cxt h (Sum MCSig :&: p) a CExpressionL
e) <- Cxt h (Sum MCSig :&: p) a RhsL
-> Maybe (CExpressionIsRhs (Cxt h (Sum MCSig :&: p) a) RhsL)
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 RhsL
f
   , Just (FunctionCallIsCExpression Cxt h (Sum MCSig :&: p) a FunctionCallL
c) <- Cxt h (Sum MCSig :&: p) a CExpressionL
-> Maybe
     (FunctionCallIsCExpression
        (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 FunctionCallL
-> Maybe (Cxt h (Sum MCSig :&: p) a FunctionCallL)
forall a. a -> Maybe a
Just Cxt h (Sum MCSig :&: p) a FunctionCallL
c
  projF' Cxt h (Sum MCSig :&: p) a RhsL
_ = Maybe (Cxt h (Sum MCSig :&: p) a FunctionCallL)
forall a. Maybe a
Nothing

#endif