{-# OPTIONS_HADDOCK hide #-}

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}

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

import Data.List ( (\\) )

import Language.Haskell.TH.Syntax ( mkName )

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

import Cubix.Language.Info
import Cubix.Language.Lua.Parametric.Full.Types as L
import Cubix.Language.Parametric.Derive
import Cubix.Language.Parametric.InjF
import Cubix.Language.Parametric.Syntax hiding (ExpL)
import Cubix.Language.Parametric.Syntax qualified as P

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

data LuaLocalVarInit e l where
  LuaLocalVarInit :: e [ExpL] -> LuaLocalVarInit e LocalVarInitL

data LuaLhs e l where
  LuaLhs :: e [L.VarL] -> LuaLhs e LhsL

data LuaRhs e l where
  LuaRhs :: e [ExpL] -> LuaRhs e RhsL

data LuaBlockEnd e l where
  LuaBlockEnd :: e (Maybe [ExpL]) -> LuaBlockEnd e BlockEndL

data LuaSpecialFunArg e l where
  LuaTableArg             ::                   e L.TableL -> LuaSpecialFunArg e FunctionArgumentsL
  LuaStringArg            ::                   String     -> LuaSpecialFunArg e FunctionArgumentsL
  LuaReceiverAndTableArg  :: e L.PrefixExpL -> e L.TableL -> LuaSpecialFunArg e FunctionArgumentsL
  LuaReceiverAndStringArg :: e L.PrefixExpL -> String     -> LuaSpecialFunArg e FunctionArgumentsL

deriveAll [''LuaLocalVarInit, ''LuaLhs, ''LuaRhs, ''LuaBlockEnd, ''LuaSpecialFunArg]

createSortInclusionTypes
  [''P.IdentL, ''P.AssignL, ''P.BlockL, ''L.StatL,      ''P.SingleLocalVarDeclL, ''P.FunctionCallL, ''L.ExpL,              ''L.PrefixExpL,   ''L.PrefixExpL]
  [''L.NameL,  ''L.StatL, ''L.BlockL,   ''P.BlockItemL, ''L.StatL,               ''L.FunCallL,      ''P.PositionalArgExpL, ''P.FunctionExpL, ''ReceiverL]
deriveAllButSortInjection [''IdentIsName, ''AssignIsStat, ''BlockIsBlock, ''StatIsBlockItem, ''SingleLocalVarDeclIsStat,
           ''FunctionCallIsFunCall, ''ExpIsPositionalArgExp, ''PrefixExpIsFunctionExp, ''PrefixExpIsReceiver]
createSortInclusionInfers [ ''P.IdentL, ''P.AssignL, ''P.BlockL, ''L.StatL,      ''P.SingleLocalVarDeclL, ''P.FunctionCallL, ''L.ExpL,              ''L.PrefixExpL,   ''L.PrefixExpL
                          ] [
                            ''L.NameL,  ''L.StatL, ''L.BlockL,   ''P.BlockItemL, ''L.StatL,               ''L.FunCallL,      ''P.PositionalArgExpL, ''P.FunctionExpL, ''ReceiverL
                          ]


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

data LuaFunctionDefinedObjL
data LuaFunctionDefinedObj e l where
  LuaFunctionDefinedObj :: e [P.IdentL] -> LuaFunctionDefinedObj e LuaFunctionDefinedObjL

deriveAll [''LuaFunctionDefinedObj]

-- Use this for "fun"; use EmptyFunctionAttrs for "local fun"
data LuaFunctionAttrs e l where
  LuaFunctionAttrs :: e LuaFunctionDefinedObjL -> LuaFunctionAttrs e FunctionDefAttrsL

deriveAll [''LuaFunctionAttrs]

data LuaVarArgsParam :: Node where
  LuaVarArgsParam :: LuaVarArgsParam e FunctionParameterL

deriveAll [''LuaVarArgsParam]

-- When I did the deriveAll's on one line, I got a mysterious GHC crash


createSortInclusionTypes
  [''P.FunctionDefL, ''P.BlockL]
  [''L.StatL,        ''P.FunctionBodyL]
deriveAllButSortInjection [''FunctionDefIsStat, ''BlockIsFunctionBody]
createSortInclusionInfers
  [''P.FunctionDefL, ''P.BlockL]
  [''L.StatL,        ''P.FunctionBodyL]

-----------------------------------------------------------------------------------
---------------               Expressions                  ------------------------
-----------------------------------------------------------------------------------

createSortInclusionTypes
  [''P.ExpressionL, ''ExpL]
  [''ExpL,          ''P.ExpressionL]
deriveAllButSortInjection [''ExpressionIsExp, ''ExpIsExpression]
createSortInclusionInfers
  [''P.ExpressionL, ''ExpL]
  [''ExpL,          ''P.ExpressionL]

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

do let newLuaNodes =
         [ ''LuaLocalVarInit, ''LuaLhs, ''LuaRhs, ''LuaBlockEnd
         , ''LuaSpecialFunArg, ''LuaFunctionDefinedObj
         , ''LuaFunctionAttrs, ''LuaVarArgsParam
         ]
       luaSortInjections =
         [ ''IdentIsName, ''AssignIsStat
         , ''BlockIsBlock, ''StatIsBlockItem
         , ''SingleLocalVarDeclIsStat, ''FunctionCallIsFunCall
         , ''ExpIsPositionalArgExp, ''PrefixExpIsFunctionExp
         , ''PrefixExpIsReceiver, ''FunctionDefIsStat
         , ''BlockIsFunctionBody
         , ''ExpressionIsExp, ''ExpIsExpression
         ]
   let names =
         (luaSigNames \\ [mkName "Name", mkName "Block", mkName "FunArg", mkName "FunCall"]) ++
         newLuaNodes ++
         luaSortInjections ++
         [ ''OptLocalVarInit, ''SingleLocalVarDecl, ''P.Ident
         , ''AssignOpEquals, ''Assign, ''P.Block, ''P.TupleBinder
         , ''EmptyLocalVarDeclAttrs
         , ''FunctionCall, ''EmptyFunctionCallAttrs
         , ''FunctionArgumentList, ''PositionalArgument
         , ''ReceiverArg, ''FunctionIdent
         , ''FunctionDef, ''EmptyFunctionDefAttrs, ''SelfParameter
         , ''PositionalParameter, ''EmptyParameterAttrs
         , ''UnaryMinusOp, ''ComplementOp, ''LogicalNegationOp
         , ''ArithBinOp, ''DivOp, ''ModOp, ''IDivOp, ''ExpOp
         , ''BitwiseBinOp, ''LogicalBinOp, ''LogicalShrOp, ''ShlOp
         , ''RelationalBinOp
         , ''Operator
         ]
   runCompTrans $ makeSumType "MLuaSig" names

type instance InjectableSorts MLuaSig AssignL = '[StatL]
type instance InjectableSorts MLuaSig SingleLocalVarDeclL = '[StatL]

type MLuaTerm = Term MLuaSig
type MLuaTermLab = TermLab MLuaSig

type MLuaCxt h a = CxtS h MLuaSig a
type MLuaCxtA h a p = AnnCxtS p h MLuaSig a

type MLuaTermOptAnn a = AnnTerm (Maybe a) MLuaSig

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

instance InjF MLuaSig [ExpL] LocalVarInitL where
  injF :: forall h (a :: * -> *).
CxtS h MLuaSig a [ExpL] -> CxtS h MLuaSig a LocalVarInitL
injF = CxtS h MLuaSig a [ExpL] -> CxtS h MLuaSig a LocalVarInitL
forall h (fs :: Signature) (a :: * -> *) j.
(LuaLocalVarInit :-<: fs, InjF fs LocalVarInitL j) =>
CxtS h fs a [ExpL] -> CxtS h fs a j
iLuaLocalVarInit

  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MLuaSig :&: p) a LocalVarInitL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a [ExpL])
projF' (Cxt h (Sum MLuaSig :&: p) a LocalVarInitL
-> Maybe
     (LuaLocalVarInit (Cxt h (Sum MLuaSig :&: 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' -> (Just (LuaLocalVarInit Cxt h (Sum MLuaSig :&: p) a [ExpL]
x))) = Cxt h (Sum MLuaSig :&: p) a [ExpL]
-> Maybe (Cxt h (Sum MLuaSig :&: p) a [ExpL])
forall a. a -> Maybe a
Just Cxt h (Sum MLuaSig :&: p) a [ExpL]
x
  projF' Cxt h (Sum MLuaSig :&: p) a LocalVarInitL
_ = Maybe (Cxt h (Sum MLuaSig :&: p) a [ExpL])
forall a. Maybe a
Nothing

instance InjF MLuaSig [L.VarL] LhsL where
  injF :: forall h (a :: * -> *).
CxtS h MLuaSig a [VarL] -> CxtS h MLuaSig a LhsL
injF = CxtS h MLuaSig a [VarL] -> CxtS h MLuaSig a LhsL
forall h (fs :: Signature) (a :: * -> *) j.
(LuaLhs :-<: fs, InjF fs LhsL j) =>
CxtS h fs a [VarL] -> CxtS h fs a j
iLuaLhs

  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MLuaSig :&: p) a LhsL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a [VarL])
projF' (Cxt h (Sum MLuaSig :&: p) a LhsL
-> Maybe (LuaLhs (Cxt h (Sum MLuaSig :&: p) a) LhsL)
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 (LuaLhs Cxt h (Sum MLuaSig :&: p) a [VarL]
x))) = Cxt h (Sum MLuaSig :&: p) a [VarL]
-> Maybe (Cxt h (Sum MLuaSig :&: p) a [VarL])
forall a. a -> Maybe a
Just Cxt h (Sum MLuaSig :&: p) a [VarL]
x
  projF' Cxt h (Sum MLuaSig :&: p) a LhsL
_ = Maybe (Cxt h (Sum MLuaSig :&: p) a [VarL])
forall a. Maybe a
Nothing

instance InjF MLuaSig [ExpL] RhsL where
  injF :: forall h (a :: * -> *).
CxtS h MLuaSig a [ExpL] -> CxtS h MLuaSig a RhsL
injF = CxtS h MLuaSig a [ExpL] -> CxtS h MLuaSig a RhsL
forall h (fs :: Signature) (a :: * -> *) j.
(LuaRhs :-<: fs, InjF fs RhsL j) =>
CxtS h fs a [ExpL] -> CxtS h fs a j
iLuaRhs

  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MLuaSig :&: p) a RhsL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a [ExpL])
projF' (Cxt h (Sum MLuaSig :&: p) a RhsL
-> Maybe (LuaRhs (Cxt h (Sum MLuaSig :&: 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' -> (Just (LuaRhs Cxt h (Sum MLuaSig :&: p) a [ExpL]
x))) = Cxt h (Sum MLuaSig :&: p) a [ExpL]
-> Maybe (Cxt h (Sum MLuaSig :&: p) a [ExpL])
forall a. a -> Maybe a
Just Cxt h (Sum MLuaSig :&: p) a [ExpL]
x
  projF' Cxt h (Sum MLuaSig :&: p) a RhsL
_ = Maybe (Cxt h (Sum MLuaSig :&: p) a [ExpL])
forall a. Maybe a
Nothing

instance InjF MLuaSig (Maybe [ExpL]) BlockEndL where
  injF :: forall h (a :: * -> *).
CxtS h MLuaSig a (Maybe [ExpL]) -> CxtS h MLuaSig a BlockEndL
injF = CxtS h MLuaSig a (Maybe [ExpL]) -> CxtS h MLuaSig a BlockEndL
forall h (fs :: Signature) (a :: * -> *) j.
(LuaBlockEnd :-<: fs, InjF fs BlockEndL j) =>
CxtS h fs a (Maybe [ExpL]) -> CxtS h fs a j
iLuaBlockEnd

  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MLuaSig :&: p) a BlockEndL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a (Maybe [ExpL]))
projF' (Cxt h (Sum MLuaSig :&: p) a BlockEndL
-> Maybe (LuaBlockEnd (Cxt h (Sum MLuaSig :&: p) a) BlockEndL)
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 (LuaBlockEnd Cxt h (Sum MLuaSig :&: p) a (Maybe [ExpL])
x))) = Cxt h (Sum MLuaSig :&: p) a (Maybe [ExpL])
-> Maybe (Cxt h (Sum MLuaSig :&: p) a (Maybe [ExpL]))
forall a. a -> Maybe a
Just Cxt h (Sum MLuaSig :&: p) a (Maybe [ExpL])
x
  projF' Cxt h (Sum MLuaSig :&: p) a BlockEndL
_ = Maybe (Cxt h (Sum MLuaSig :&: p) a (Maybe [ExpL]))
forall a. Maybe a
Nothing

instance InjF MLuaSig AssignL BlockItemL where
  injF :: forall h (a :: * -> *).
CxtS h MLuaSig a AssignL -> CxtS h MLuaSig a BlockItemL
injF = CxtS h MLuaSig a AssignL -> CxtS h MLuaSig a BlockItemL
forall h (fs :: Signature) (a :: * -> *) j.
(AssignIsStat :-<: fs, InjF fs StatL j) =>
CxtS h fs a AssignL -> CxtS h fs a j
iAssignIsStat

  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MLuaSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a AssignL)
projF' Cxt h (Sum MLuaSig :&: p) a BlockItemL
t = do
    (MLuaCxtA h a p StatL
a :: MLuaCxtA h a p StatL) <- Cxt h (Sum MLuaSig :&: p) a BlockItemL
-> Maybe (MLuaCxtA h a p StatL)
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 MLuaSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a StatL)
projF' Cxt h (Sum MLuaSig :&: p) a BlockItemL
t
    MLuaCxtA h a p StatL -> Maybe (Cxt h (Sum MLuaSig :&: 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 MLuaSig :&: p) a StatL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a AssignL)
projF' MLuaCxtA h a p StatL
a


instance InjF MLuaSig SingleLocalVarDeclL BlockItemL where
  injF :: forall h (a :: * -> *).
CxtS h MLuaSig a SingleLocalVarDeclL -> CxtS h MLuaSig a BlockItemL
injF = CxtS h MLuaSig a SingleLocalVarDeclL -> CxtS h MLuaSig a BlockItemL
forall h (fs :: Signature) (a :: * -> *) j.
(SingleLocalVarDeclIsStat :-<: fs, InjF fs StatL j) =>
CxtS h fs a SingleLocalVarDeclL -> CxtS h fs a j
iSingleLocalVarDeclIsStat
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MLuaSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a SingleLocalVarDeclL)
projF' Cxt h (Sum MLuaSig :&: p) a BlockItemL
t = do
    (MLuaCxtA h a p StatL
a :: MLuaCxtA h a p StatL) <- Cxt h (Sum MLuaSig :&: p) a BlockItemL
-> Maybe (MLuaCxtA h a p StatL)
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 MLuaSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a StatL)
projF' Cxt h (Sum MLuaSig :&: p) a BlockItemL
t
    MLuaCxtA h a p StatL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a SingleLocalVarDeclL)
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 MLuaSig :&: p) a StatL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a SingleLocalVarDeclL)
projF' MLuaCxtA h a p StatL
a

instance InjF MLuaSig IdentL ExpL where
  injF :: forall h (a :: * -> *).
CxtS h MLuaSig a IdentL -> CxtS h MLuaSig a ExpL
injF = CxtS h MLuaSig a PrefixExpL -> CxtS h MLuaSig a ExpL
forall h (fs :: Signature) (a :: * -> *) j.
(Exp :-<: fs, InjF fs ExpL j) =>
CxtS h fs a PrefixExpL -> CxtS h fs a j
iPrefixExp (CxtS h MLuaSig a PrefixExpL -> CxtS h MLuaSig a ExpL)
-> (CxtS h MLuaSig a IdentL -> CxtS h MLuaSig a PrefixExpL)
-> CxtS h MLuaSig a IdentL
-> CxtS h MLuaSig a ExpL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtS h MLuaSig a VarL -> CxtS h MLuaSig a PrefixExpL
forall h (fs :: Signature) (a :: * -> *) j.
(PrefixExp :-<: fs, InjF fs PrefixExpL j) =>
CxtS h fs a VarL -> CxtS h fs a j
iPEVar (CxtS h MLuaSig a VarL -> CxtS h MLuaSig a PrefixExpL)
-> (CxtS h MLuaSig a IdentL -> CxtS h MLuaSig a VarL)
-> CxtS h MLuaSig a IdentL
-> CxtS h MLuaSig a PrefixExpL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtS h MLuaSig a NameL -> CxtS h MLuaSig a VarL
forall h (fs :: Signature) (a :: * -> *) j.
(Var :-<: fs, InjF fs VarL j) =>
CxtS h fs a NameL -> CxtS h fs a j
iVarName (CxtS h MLuaSig a NameL -> CxtS h MLuaSig a VarL)
-> (CxtS h MLuaSig a IdentL -> CxtS h MLuaSig a NameL)
-> CxtS h MLuaSig a IdentL
-> CxtS h MLuaSig a VarL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtS h MLuaSig a IdentL -> CxtS h MLuaSig a NameL
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 MLuaSig a IdentL -> CxtS h MLuaSig a NameL
injF
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MLuaSig :&: p) a ExpL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a IdentL)
projF' Cxt h (Sum MLuaSig :&: p) a ExpL
t = do
    PrefixExp Cxt h (Sum MLuaSig :&: p) a PrefixExpL
a <- Cxt h (Sum MLuaSig :&: p) a ExpL
-> Maybe (Exp (Cxt h (Sum MLuaSig :&: p) a) ExpL)
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 MLuaSig :&: p) a ExpL
t
    PEVar Cxt h (Sum MLuaSig :&: p) a VarL
b <- Cxt h (Sum MLuaSig :&: p) a PrefixExpL
-> Maybe (PrefixExp (Cxt h (Sum MLuaSig :&: p) a) PrefixExpL)
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 MLuaSig :&: p) a PrefixExpL
a
    VarName Cxt h (Sum MLuaSig :&: p) a NameL
c <- Cxt h (Sum MLuaSig :&: p) a VarL
-> Maybe (Var (Cxt h (Sum MLuaSig :&: p) a) VarL)
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 MLuaSig :&: p) a VarL
b
    Cxt h (Sum MLuaSig :&: p) a NameL
-> Maybe (Cxt h (Sum MLuaSig :&: 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 MLuaSig :&: p) a NameL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a IdentL)
projF' Cxt h (Sum MLuaSig :&: p) a NameL
c

instance InjF MLuaSig ExpL LocalVarInitL where
  injF :: forall h (a :: * -> *).
CxtS h MLuaSig a ExpL -> CxtS h MLuaSig a LocalVarInitL
injF CxtS h MLuaSig a ExpL
x = CxtS h MLuaSig a [ExpL] -> CxtS h MLuaSig a LocalVarInitL
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 MLuaSig a [ExpL] -> CxtS h MLuaSig a LocalVarInitL
injF (CxtS h MLuaSig a [ExpL] -> CxtS h MLuaSig a LocalVarInitL)
-> CxtS h MLuaSig a [ExpL] -> CxtS h MLuaSig a LocalVarInitL
forall a b. (a -> b) -> a -> b
$ [CxtS h MLuaSig a ExpL] -> CxtS h MLuaSig a [ExpL]
forall l.
Typeable l =>
[Cxt h (Sum MLuaSig) a l] -> Cxt h (Sum MLuaSig) a [l]
forall (f :: * -> *) (e :: * -> *) l.
(InsertF f e, Typeable l) =>
f (e l) -> e (f l)
insertF [CxtS h MLuaSig a ExpL
x]
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MLuaSig :&: p) a LocalVarInitL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a ExpL)
projF' Cxt h (Sum MLuaSig :&: p) a LocalVarInitL
t = do
    LuaLocalVarInit Cxt h (Sum MLuaSig :&: p) a [ExpL]
x <- Cxt h (Sum MLuaSig :&: p) a LocalVarInitL
-> Maybe
     (LuaLocalVarInit (Cxt h (Sum MLuaSig :&: 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 MLuaSig :&: p) a LocalVarInitL
t
    ConsF Cxt h (Sum MLuaSig :&: p) a l1
e Cxt h (Sum MLuaSig :&: p) a [l1]
rest <- Cxt h (Sum MLuaSig :&: p) a [ExpL]
-> Maybe (ListF (Cxt h (Sum MLuaSig :&: p) a) [ExpL])
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 MLuaSig :&: p) a [ExpL]
x
    ListF (Cxt h (Sum MLuaSig :&: p) a) [l1]
NilF <- Cxt h (Sum MLuaSig :&: p) a [l1]
-> Maybe (ListF (Cxt h (Sum MLuaSig :&: p) a) [l1])
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 MLuaSig :&: p) a [l1]
rest
    Cxt h (Sum MLuaSig :&: p) a ExpL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a ExpL)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Cxt h (Sum MLuaSig :&: p) a l1
Cxt h (Sum MLuaSig :&: p) a ExpL
e

instance {-# OVERLAPPING #-} InjF MLuaSig IdentL VarDeclBinderL where
  injF :: forall h (a :: * -> *).
CxtS h MLuaSig a IdentL -> CxtS h MLuaSig a VarDeclBinderL
injF CxtS h MLuaSig a IdentL
x = CxtS h MLuaSig a [IdentL] -> CxtS h MLuaSig a VarDeclBinderL
forall h (fs :: Signature) (a :: * -> *) j.
(TupleBinder :-<: fs, InjF fs VarDeclBinderL j) =>
CxtS h fs a [IdentL] -> CxtS h fs a j
iTupleBinder (CxtS h MLuaSig a [IdentL] -> CxtS h MLuaSig a VarDeclBinderL)
-> CxtS h MLuaSig a [IdentL] -> CxtS h MLuaSig a VarDeclBinderL
forall a b. (a -> b) -> a -> b
$ [CxtS h MLuaSig a IdentL] -> CxtS h MLuaSig a [IdentL]
forall l.
Typeable l =>
[Cxt h (Sum MLuaSig) a l] -> Cxt h (Sum MLuaSig) a [l]
forall (f :: * -> *) (e :: * -> *) l.
(InsertF f e, Typeable l) =>
f (e l) -> e (f l)
insertF [CxtS h MLuaSig a IdentL
x]

  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MLuaSig :&: p) a VarDeclBinderL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a IdentL)
projF' Cxt h (Sum MLuaSig :&: p) a VarDeclBinderL
t = do
    TupleBinder Cxt h (Sum MLuaSig :&: p) a [IdentL]
ns <- Cxt h (Sum MLuaSig :&: p) a VarDeclBinderL
-> Maybe (TupleBinder (Cxt h (Sum MLuaSig :&: p) a) VarDeclBinderL)
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 MLuaSig :&: p) a VarDeclBinderL
t
    ConsF Cxt h (Sum MLuaSig :&: p) a l1
n Cxt h (Sum MLuaSig :&: p) a [l1]
rest <- Cxt h (Sum MLuaSig :&: p) a [IdentL]
-> Maybe (ListF (Cxt h (Sum MLuaSig :&: 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 MLuaSig :&: p) a [IdentL]
ns
    ListF (Cxt h (Sum MLuaSig :&: p) a) [l1]
NilF <- Cxt h (Sum MLuaSig :&: p) a [l1]
-> Maybe (ListF (Cxt h (Sum MLuaSig :&: p) a) [l1])
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 MLuaSig :&: p) a [l1]
rest
    Cxt h (Sum MLuaSig :&: p) a IdentL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a IdentL)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Cxt h (Sum MLuaSig :&: p) a l1
Cxt h (Sum MLuaSig :&: p) a IdentL
n

instance InjF MLuaSig IdentL LhsL where
  injF :: forall h (a :: * -> *).
CxtS h MLuaSig a IdentL -> CxtS h MLuaSig a LhsL
injF CxtS h MLuaSig a IdentL
x = CxtS h MLuaSig a [VarL] -> CxtS h MLuaSig a LhsL
forall h (fs :: Signature) (a :: * -> *) j.
(LuaLhs :-<: fs, InjF fs LhsL j) =>
CxtS h fs a [VarL] -> CxtS h fs a j
iLuaLhs (CxtS h MLuaSig a [VarL] -> CxtS h MLuaSig a LhsL)
-> CxtS h MLuaSig a [VarL] -> CxtS h MLuaSig a LhsL
forall a b. (a -> b) -> a -> b
$ Cxt h (Sum MLuaSig) a VarL
-> CxtS h MLuaSig a [VarL] -> CxtS h MLuaSig a [VarL]
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' (CxtS h MLuaSig a NameL -> Cxt h (Sum MLuaSig) a VarL
forall h (fs :: Signature) (a :: * -> *) j.
(Var :-<: fs, InjF fs VarL j) =>
CxtS h fs a NameL -> CxtS h fs a j
iVarName (CxtS h MLuaSig a NameL -> Cxt h (Sum MLuaSig) a VarL)
-> CxtS h MLuaSig a NameL -> Cxt h (Sum MLuaSig) a VarL
forall a b. (a -> b) -> a -> b
$ CxtS h MLuaSig a IdentL -> CxtS h MLuaSig a NameL
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 MLuaSig a IdentL -> CxtS h MLuaSig a NameL
injF CxtS h MLuaSig a IdentL
x) CxtS h MLuaSig a [VarL]
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) l.
(ListF :<: f, Typeable l) =>
Cxt h f a [l]
riNilF
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MLuaSig :&: p) a LhsL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a IdentL)
projF' Cxt h (Sum MLuaSig :&: p) a LhsL
t = do
    LuaLhs Cxt h (Sum MLuaSig :&: p) a [VarL]
vs <- Cxt h (Sum MLuaSig :&: p) a LhsL
-> Maybe (LuaLhs (Cxt h (Sum MLuaSig :&: p) a) LhsL)
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 MLuaSig :&: p) a LhsL
t
    ConsF Cxt h (Sum MLuaSig :&: p) a l1
v Cxt h (Sum MLuaSig :&: p) a [l1]
rest <- Cxt h (Sum MLuaSig :&: p) a [VarL]
-> Maybe (ListF (Cxt h (Sum MLuaSig :&: p) a) [VarL])
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 MLuaSig :&: p) a [VarL]
vs
    ListF (Cxt h (Sum MLuaSig :&: p) a) [l1]
NilF <- Cxt h (Sum MLuaSig :&: p) a [l1]
-> Maybe (ListF (Cxt h (Sum MLuaSig :&: p) a) [l1])
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 MLuaSig :&: p) a [l1]
rest
    VarName Cxt h (Sum MLuaSig :&: p) a NameL
n <- Cxt h (Sum MLuaSig :&: p) a l1
-> Maybe (Var (Cxt h (Sum MLuaSig :&: p) a) l1)
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 MLuaSig :&: p) a l1
v
    Cxt h (Sum MLuaSig :&: p) a NameL
-> Maybe (Cxt h (Sum MLuaSig :&: 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 MLuaSig :&: p) a NameL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a IdentL)
projF' Cxt h (Sum MLuaSig :&: p) a NameL
n

instance InjF MLuaSig ExpL RhsL where
  injF :: forall h (a :: * -> *).
CxtS h MLuaSig a ExpL -> CxtS h MLuaSig a RhsL
injF CxtS h MLuaSig a ExpL
x = CxtS h MLuaSig a [ExpL] -> CxtS h MLuaSig a RhsL
forall h (fs :: Signature) (a :: * -> *) j.
(LuaRhs :-<: fs, InjF fs RhsL j) =>
CxtS h fs a [ExpL] -> CxtS h fs a j
iLuaRhs (CxtS h MLuaSig a [ExpL] -> CxtS h MLuaSig a RhsL)
-> CxtS h MLuaSig a [ExpL] -> CxtS h MLuaSig a RhsL
forall a b. (a -> b) -> a -> b
$ CxtS h MLuaSig a ExpL
-> CxtS h MLuaSig a [ExpL] -> CxtS h MLuaSig a [ExpL]
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' CxtS h MLuaSig a ExpL
x CxtS h MLuaSig a [ExpL]
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) l.
(ListF :<: f, Typeable l) =>
Cxt h f a [l]
riNilF
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MLuaSig :&: p) a RhsL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a ExpL)
projF' Cxt h (Sum MLuaSig :&: p) a RhsL
t = do
    LuaRhs Cxt h (Sum MLuaSig :&: p) a [ExpL]
es <- Cxt h (Sum MLuaSig :&: p) a RhsL
-> Maybe (LuaRhs (Cxt h (Sum MLuaSig :&: 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 MLuaSig :&: p) a RhsL
t
    ConsF Cxt h (Sum MLuaSig :&: p) a l1
e Cxt h (Sum MLuaSig :&: p) a [l1]
rest <- Cxt h (Sum MLuaSig :&: p) a [ExpL]
-> Maybe (ListF (Cxt h (Sum MLuaSig :&: p) a) [ExpL])
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 MLuaSig :&: p) a [ExpL]
es
    ListF (Cxt h (Sum MLuaSig :&: p) a) [l1]
NilF <- Cxt h (Sum MLuaSig :&: p) a [l1]
-> Maybe (ListF (Cxt h (Sum MLuaSig :&: p) a) [l1])
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 MLuaSig :&: p) a [l1]
rest
    Cxt h (Sum MLuaSig :&: p) a ExpL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a ExpL)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Cxt h (Sum MLuaSig :&: p) a l1
Cxt h (Sum MLuaSig :&: p) a ExpL
e

instance InjF MLuaSig IdentL PositionalArgExpL where
  injF :: forall h (a :: * -> *).
CxtS h MLuaSig a IdentL -> CxtS h MLuaSig a PositionalArgExpL
injF = CxtS h MLuaSig a PrefixExpL -> CxtS h MLuaSig a PositionalArgExpL
forall h (fs :: Signature) (a :: * -> *) j.
(Exp :-<: fs, InjF fs ExpL j) =>
CxtS h fs a PrefixExpL -> CxtS h fs a j
iPrefixExp (CxtS h MLuaSig a PrefixExpL -> CxtS h MLuaSig a PositionalArgExpL)
-> (CxtS h MLuaSig a IdentL -> CxtS h MLuaSig a PrefixExpL)
-> CxtS h MLuaSig a IdentL
-> CxtS h MLuaSig a PositionalArgExpL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtS h MLuaSig a VarL -> CxtS h MLuaSig a PrefixExpL
forall h (fs :: Signature) (a :: * -> *) j.
(PrefixExp :-<: fs, InjF fs PrefixExpL j) =>
CxtS h fs a VarL -> CxtS h fs a j
iPEVar (CxtS h MLuaSig a VarL -> CxtS h MLuaSig a PrefixExpL)
-> (CxtS h MLuaSig a IdentL -> CxtS h MLuaSig a VarL)
-> CxtS h MLuaSig a IdentL
-> CxtS h MLuaSig a PrefixExpL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtS h MLuaSig a NameL -> CxtS h MLuaSig a VarL
forall h (fs :: Signature) (a :: * -> *) j.
(Var :-<: fs, InjF fs VarL j) =>
CxtS h fs a NameL -> CxtS h fs a j
iVarName (CxtS h MLuaSig a NameL -> CxtS h MLuaSig a VarL)
-> (CxtS h MLuaSig a IdentL -> CxtS h MLuaSig a NameL)
-> CxtS h MLuaSig a IdentL
-> CxtS h MLuaSig a VarL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtS h MLuaSig a IdentL -> CxtS h MLuaSig a NameL
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 MLuaSig a IdentL -> CxtS h MLuaSig a NameL
injF

  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MLuaSig :&: p) a PositionalArgExpL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a IdentL)
projF' Cxt h (Sum MLuaSig :&: p) a PositionalArgExpL
x
   | Just (ExpIsPositionalArgExp Cxt h (Sum MLuaSig :&: p) a ExpL
e) <- Cxt h (Sum MLuaSig :&: p) a PositionalArgExpL
-> Maybe
     (ExpIsPositionalArgExp
        (Cxt h (Sum MLuaSig :&: 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 MLuaSig :&: p) a PositionalArgExpL
x
   , Just (PrefixExp Cxt h (Sum MLuaSig :&: p) a PrefixExpL
p) <- Cxt h (Sum MLuaSig :&: p) a ExpL
-> Maybe (Exp (Cxt h (Sum MLuaSig :&: p) a) ExpL)
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 MLuaSig :&: p) a ExpL
e
   , Just (PEVar Cxt h (Sum MLuaSig :&: p) a VarL
v) <- Cxt h (Sum MLuaSig :&: p) a PrefixExpL
-> Maybe (PrefixExp (Cxt h (Sum MLuaSig :&: p) a) PrefixExpL)
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 MLuaSig :&: p) a PrefixExpL
p
   , Just (VarName Cxt h (Sum MLuaSig :&: p) a NameL
n) <- Cxt h (Sum MLuaSig :&: p) a VarL
-> Maybe (Var (Cxt h (Sum MLuaSig :&: p) a) VarL)
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 MLuaSig :&: p) a VarL
v
   = Cxt h (Sum MLuaSig :&: p) a NameL
-> Maybe (Cxt h (Sum MLuaSig :&: 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 MLuaSig :&: p) a NameL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a IdentL)
projF' Cxt h (Sum MLuaSig :&: p) a NameL
n
  projF' Cxt h (Sum MLuaSig :&: p) a PositionalArgExpL
_ = Maybe (Cxt h (Sum MLuaSig :&: p) a IdentL)
forall a. Maybe a
Nothing

instance InjF MLuaSig IdentL FunctionExpL where
  injF :: forall h (a :: * -> *).
CxtS h MLuaSig a IdentL -> CxtS h MLuaSig a FunctionExpL
injF = CxtS h MLuaSig a IdentL -> CxtS h MLuaSig a FunctionExpL
forall h (fs :: Signature) (a :: * -> *) j.
(FunctionIdent :-<: fs, InjF fs FunctionExpL j) =>
CxtS h fs a IdentL -> CxtS h fs a j
iFunctionIdent

  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MLuaSig :&: p) a FunctionExpL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a IdentL)
projF' (Cxt h (Sum MLuaSig :&: p) a FunctionExpL
-> Maybe (FunctionIdent (Cxt h (Sum MLuaSig :&: 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' -> Just (FunctionIdent Cxt h (Sum MLuaSig :&: p) a IdentL
n)) = Cxt h (Sum MLuaSig :&: p) a IdentL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a IdentL)
forall a. a -> Maybe a
Just Cxt h (Sum MLuaSig :&: p) a IdentL
n
  projF' Cxt h (Sum MLuaSig :&: p) a FunctionExpL
x
    | Just (PrefixExpIsFunctionExp Cxt h (Sum MLuaSig :&: p) a PrefixExpL
p) <- Cxt h (Sum MLuaSig :&: p) a FunctionExpL
-> Maybe
     (PrefixExpIsFunctionExp (Cxt h (Sum MLuaSig :&: 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 MLuaSig :&: p) a FunctionExpL
x
    , Just (PEVar Cxt h (Sum MLuaSig :&: p) a VarL
v) <- Cxt h (Sum MLuaSig :&: p) a PrefixExpL
-> Maybe (PrefixExp (Cxt h (Sum MLuaSig :&: p) a) PrefixExpL)
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 MLuaSig :&: p) a PrefixExpL
p
    , Just (VarName Cxt h (Sum MLuaSig :&: p) a NameL
n) <- Cxt h (Sum MLuaSig :&: p) a VarL
-> Maybe (Var (Cxt h (Sum MLuaSig :&: p) a) VarL)
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 MLuaSig :&: p) a VarL
v
    = Cxt h (Sum MLuaSig :&: p) a NameL
-> Maybe (Cxt h (Sum MLuaSig :&: 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 MLuaSig :&: p) a NameL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a IdentL)
projF' Cxt h (Sum MLuaSig :&: p) a NameL
n
  projF' Cxt h (Sum MLuaSig :&: p) a FunctionExpL
_                                    = Maybe (Cxt h (Sum MLuaSig :&: p) a IdentL)
forall a. Maybe a
Nothing

instance InjF MLuaSig FunctionCallL RhsL where
  injF :: forall h (a :: * -> *).
CxtS h MLuaSig a FunctionCallL -> CxtS h MLuaSig a RhsL
injF CxtS h MLuaSig a FunctionCallL
x = CxtS h MLuaSig a [ExpL] -> CxtS h MLuaSig a RhsL
forall h (fs :: Signature) (a :: * -> *) j.
(LuaRhs :-<: fs, InjF fs RhsL j) =>
CxtS h fs a [ExpL] -> CxtS h fs a j
iLuaRhs (CxtS h MLuaSig a [ExpL] -> CxtS h MLuaSig a RhsL)
-> CxtS h MLuaSig a [ExpL] -> CxtS h MLuaSig a RhsL
forall a b. (a -> b) -> a -> b
$ [Cxt h (Sum MLuaSig) a ExpL] -> CxtS h MLuaSig a [ExpL]
forall l.
Typeable l =>
[Cxt h (Sum MLuaSig) a l] -> Cxt h (Sum MLuaSig) a [l]
forall (f :: * -> *) (e :: * -> *) l.
(InsertF f e, Typeable l) =>
f (e l) -> e (f l)
insertF [CxtS h MLuaSig a PrefixExpL -> Cxt h (Sum MLuaSig) a ExpL
forall h (fs :: Signature) (a :: * -> *) j.
(Exp :-<: fs, InjF fs ExpL j) =>
CxtS h fs a PrefixExpL -> CxtS h fs a j
iPrefixExp (CxtS h MLuaSig a PrefixExpL -> Cxt h (Sum MLuaSig) a ExpL)
-> CxtS h MLuaSig a PrefixExpL -> Cxt h (Sum MLuaSig) a ExpL
forall a b. (a -> b) -> a -> b
$ CxtS h MLuaSig a FunCallL -> CxtS h MLuaSig a PrefixExpL
forall h (fs :: Signature) (a :: * -> *) j.
(PrefixExp :-<: fs, InjF fs PrefixExpL j) =>
CxtS h fs a FunCallL -> CxtS h fs a j
iPEFunCall (CxtS h MLuaSig a FunCallL -> CxtS h MLuaSig a PrefixExpL)
-> CxtS h MLuaSig a FunCallL -> CxtS h MLuaSig a PrefixExpL
forall a b. (a -> b) -> a -> b
$ CxtS h MLuaSig a FunctionCallL -> CxtS h MLuaSig a FunCallL
forall h (fs :: Signature) (a :: * -> *) j.
(FunctionCallIsFunCall :-<: fs, InjF fs FunCallL j) =>
CxtS h fs a FunctionCallL -> CxtS h fs a j
iFunctionCallIsFunCall CxtS h MLuaSig a FunctionCallL
x]
  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MLuaSig :&: p) a RhsL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a FunctionCallL)
projF' Cxt h (Sum MLuaSig :&: p) a RhsL
f
   | Just (LuaRhs (SingletonFA' Cxt h (Sum MLuaSig :&: p) a ExpL
e)) <- Cxt h (Sum MLuaSig :&: p) a RhsL
-> Maybe (LuaRhs (Cxt h (Sum MLuaSig :&: 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 MLuaSig :&: p) a RhsL
f
   , Just (PrefixExp Cxt h (Sum MLuaSig :&: p) a PrefixExpL
c) <- Cxt h (Sum MLuaSig :&: p) a ExpL
-> Maybe (Exp (Cxt h (Sum MLuaSig :&: p) a) ExpL)
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 MLuaSig :&: p) a ExpL
e
   , Just (PEFunCall Cxt h (Sum MLuaSig :&: p) a FunCallL
b) <- Cxt h (Sum MLuaSig :&: p) a PrefixExpL
-> Maybe (PrefixExp (Cxt h (Sum MLuaSig :&: p) a) PrefixExpL)
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 MLuaSig :&: p) a PrefixExpL
c
   , Just (FunctionCallIsFunCall Cxt h (Sum MLuaSig :&: p) a FunctionCallL
a) <- Cxt h (Sum MLuaSig :&: p) a FunCallL
-> Maybe
     (FunctionCallIsFunCall (Cxt h (Sum MLuaSig :&: p) a) FunCallL)
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 MLuaSig :&: p) a FunCallL
b
   = Cxt h (Sum MLuaSig :&: p) a FunctionCallL
-> Maybe (Cxt h (Sum MLuaSig :&: p) a FunctionCallL)
forall a. a -> Maybe a
Just Cxt h (Sum MLuaSig :&: p) a FunctionCallL
a
  projF' Cxt h (Sum MLuaSig :&: p) a RhsL
_ = Maybe (Cxt h (Sum MLuaSig :&: p) a FunctionCallL)
forall a. Maybe a
Nothing