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

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

#ifndef ONLY_ONE_LANGUAGE
import Data.List ( (\\) )
import Language.Haskell.TH ( mkName )

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

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

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

-- Lvalues
-- See https://docs.python.org/3/reference/simple_stmts.html#grammar-token-assignment_stmt

data PyLValueL


-- Python manual is not detailed enough to explain whether we can model augmented
-- and normal assignments with the generic Assign fragment. A more immediate issue though
-- is that they allow different LHSs. It looks like we could use Assign to model either, but
-- we use it to model normal assignments

data PyLhs e l where
  PyLhs :: e [PyLValueL] -> PyLhs e LhsL

data TupleLValue e l where
  TupleLValue :: e [PyLValueL] -> TupleLValue e PyLValueL

data ListLValue e l where
  ListLValue :: e [PyLValueL] -> ListLValue e PyLValueL

data DotLValue e l where
  DotLValue :: e Py.ExprL -> e P.IdentL -> DotLValue e PyLValueL

data StarLValue e l where
  StarLValue :: e PyLValueL -> StarLValue e PyLValueL

data SubscriptLValue e l where
  SubscriptLValue :: e Py.ExprL -> e Py.ExprL -> SubscriptLValue e PyLValueL

data SliceLValue e l where
  SliceLValue :: e Py.ExprL -> e [Py.SliceL] -> SliceLValue e PyLValueL

data ParenLValue e l where
  ParenLValue :: e PyLValueL -> ParenLValue e PyLValueL

deriveAll [''PyLhs, ''TupleLValue, ''ListLValue, ''DotLValue, ''StarLValue, ''SubscriptLValue, ''SliceLValue, ''ParenLValue]




data PyWith e l where
  PyWith :: e [PyWithBinderL] -> e [Py.StatementL] -> PyWith e Py.StatementL

data PyWithBinderL
data PyWithBinder e l where
  PyWithBinder :: e Py.ExprL -> e (Maybe PyLValueL) -> PyWithBinder e PyWithBinderL

-- Extracting out this sort for docstring support

data PyStringLitL
data PyStringLit (e :: * -> *) l where
  PyStrings :: [String] -> PyStringLit e PyStringLitL
  PyUnicodeStrings :: [String] -> PyStringLit e PyStringLitL
  PyByteStrings :: [String] -> PyStringLit e PyStringLitL

-- Supports docstrings
-- Note that only functions and modules have scopes in Python. Those are
-- also the only places that support docstrings
data PyBlockL
data PyBlock e l where
  PyBlock :: e (Maybe PyStringLitL) -> e BlockL -> PyBlock e PyBlockL

data PyClassL -- Creating a new sort, so can tell the CFG it's a suspended computation
data PyClass e l where
  PyClass :: e P.IdentL -> e [ArgumentL] -> e PyBlockL -> PyClass e PyClassL

-- Chained comparison
data PyCompL
data PyComp e l where
  PyBaseComp  :: e Py.OpL -> e Py.ExprL -> e Py.ExprL -> PyComp e PyCompL
  PyChainComp :: e Py.OpL -> e Py.ExprL -> e PyCompL -> PyComp e PyCompL


-- We want the invariant that expressions something on the left of an expression may not
-- depend on something to the right. The "x if y else z" notation violates this; we're reordering.
--
--
-- TODO: Python assignments violate this. In fact, they don't meet the spec of generic assignments
data PyCondExpr e l where
  PyCondExpr :: e Py.ExprL -- condition
             -> e Py.ExprL -- then
             -> e Py.ExprL -- else
             -> PyCondExpr e Py.ExprL

data PyComprehensionExpr e l where
  PyListComprehension :: e PyComprehensionL -> PyComprehensionExpr e Py.ExprL
  PyDictComprehension :: e PyComprehensionL -> PyComprehensionExpr e Py.ExprL
  PySetComprehension :: e PyComprehensionL -> PyComprehensionExpr e Py.ExprL

data PyComprehensionL

data PyComprehension e l where
  PyComprehensionFor :: Bool -> e [Py.ExprL] -> e Py.ExprL -> e PyComprehensionL -> PyComprehension e PyComprehensionL
  PyComprehensionIf  :: e Py.ExprL -> e PyComprehensionL -> PyComprehension e PyComprehensionL
  PyComprehensionBody :: e Py.ComprehensionExprL -> PyComprehension e PyComprehensionL

deriveAll [''PyWith, ''PyWithBinder, ''PyStringLit, ''PyBlock, ''PyClass, ''PyComp, ''PyCondExpr, ''PyComprehensionExpr, ''PyComprehension]

pattern PyBlock' :: (PyBlock :-<: fs, All HFunctor fs) => CxtS h fs a (Maybe PyStringLitL) -> CxtS h fs a BlockL -> CxtS h fs a PyBlockL
pattern $bPyBlock' :: CxtS h fs a (Maybe PyStringLitL)
-> CxtS h fs a BlockL -> CxtS h fs a PyBlockL
$mPyBlock' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(PyBlock :-<: fs, All HFunctor fs) =>
CxtS h fs a PyBlockL
-> (CxtS h fs a (Maybe PyStringLitL) -> CxtS h fs a BlockL -> r)
-> (Void# -> r)
-> r
PyBlock' docStr body <- (project -> Just (PyBlock docStr body)) where
  PyBlock' docStr :: CxtS h fs a (Maybe PyStringLitL)
docStr body :: CxtS h fs a BlockL
body = CxtS h fs a (Maybe PyStringLitL)
-> CxtS h fs a BlockL -> CxtS h fs a PyBlockL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(PyBlock :-<: fs, InjF fs PyBlockL j) =>
CxtS h fs a (Maybe PyStringLitL)
-> CxtS h fs a BlockL -> CxtS h fs a j
iPyBlock CxtS h fs a (Maybe PyStringLitL)
docStr CxtS h fs a BlockL
body

pattern PyChainComp' :: (PyComp :-<: fs, All HFunctor fs) => CxtS h fs a Py.OpL -> CxtS h fs a Py.ExprL -> CxtS h fs a PyCompL -> CxtS h fs a PyCompL
pattern $bPyChainComp' :: CxtS h fs a OpL
-> CxtS h fs a ExprL -> CxtS h fs a PyCompL -> CxtS h fs a PyCompL
$mPyChainComp' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(PyComp :-<: fs, All HFunctor fs) =>
CxtS h fs a PyCompL
-> (CxtS h fs a OpL
    -> CxtS h fs a ExprL -> CxtS h fs a PyCompL -> r)
-> (Void# -> r)
-> r
PyChainComp' op l r <- (project -> Just (PyChainComp op l r)) where
  PyChainComp' op :: CxtS h fs a OpL
op l :: CxtS h fs a ExprL
l r :: CxtS h fs a PyCompL
r = CxtS h fs a OpL
-> CxtS h fs a ExprL -> CxtS h fs a PyCompL -> CxtS h fs a PyCompL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(PyComp :-<: fs, InjF fs PyCompL j) =>
CxtS h fs a OpL
-> CxtS h fs a ExprL -> CxtS h fs a PyCompL -> CxtS h fs a j
iPyChainComp CxtS h fs a OpL
op CxtS h fs a ExprL
l CxtS h fs a PyCompL
r

pattern PyBaseComp' :: (PyComp :-<: fs, All HFunctor fs) => CxtS h fs a Py.OpL -> CxtS h fs a Py.ExprL -> CxtS h fs a Py.ExprL -> CxtS h fs a PyCompL
pattern $bPyBaseComp' :: CxtS h fs a OpL
-> CxtS h fs a ExprL -> CxtS h fs a ExprL -> CxtS h fs a PyCompL
$mPyBaseComp' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(PyComp :-<: fs, All HFunctor fs) =>
CxtS h fs a PyCompL
-> (CxtS h fs a OpL -> CxtS h fs a ExprL -> CxtS h fs a ExprL -> r)
-> (Void# -> r)
-> r
PyBaseComp' op l r <- (project -> Just (PyBaseComp op l r)) where
  PyBaseComp' op :: CxtS h fs a OpL
op l :: CxtS h fs a ExprL
l r :: CxtS h fs a ExprL
r = CxtS h fs a OpL
-> CxtS h fs a ExprL -> CxtS h fs a ExprL -> CxtS h fs a PyCompL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(PyComp :-<: fs, InjF fs PyCompL j) =>
CxtS h fs a OpL
-> CxtS h fs a ExprL -> CxtS h fs a ExprL -> CxtS h fs a j
iPyBaseComp CxtS h fs a OpL
op CxtS h fs a ExprL
l CxtS h fs a ExprL
r


createSortInclusionTypes [ ''P.IdentL,  ''P.AssignL,     ''Py.ExprL, ''Py.StatementL, ''PyCompL,  ''P.IdentL,  ''PyClassL
                         ] [
                           ''Py.IdentL, ''Py.StatementL, ''P.RhsL,   ''P.BlockItemL,  ''Py.ExprL, ''PyLValueL, ''Py.StatementL
                         ]
deriveAll [''IdentIsIdent, ''AssignIsStatement, ''ExprIsRhs, ''StatementIsBlockItem, ''PyCompIsExpr, ''IdentIsPyLValue, ''PyClassIsStatement]
createSortInclusionInfers [ ''P.IdentL,  ''P.AssignL,     ''Py.ExprL, ''Py.StatementL, ''PyCompL,  ''P.IdentL,  ''PyClassL
                          ] [
                            ''Py.IdentL, ''Py.StatementL, ''P.RhsL,   ''P.BlockItemL,  ''Py.ExprL, ''PyLValueL, ''Py.StatementL
                          ]

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


data PythonArg e l where
  PythonArgSplat   :: e Py.ExprL               -> PythonArg e FunctionArgumentL
  PythonArgKeyword :: e P.IdentL -> e Py.ExprL -> PythonArg e FunctionArgumentL
  PythonArgKWSplat :: e Py.ExprL               -> PythonArg e FunctionArgumentL

deriveAll [''PythonArg]

data PyFunDefAttrs e l where
  PyFunDefAttrs :: e (Maybe Py.ExprL) -> PyFunDefAttrs e FunctionDefAttrsL

-- Annotation, default
data PyParamAttrs e l where
  PyParamAttrs :: e (Maybe Py.ExprL) -> e (Maybe Py.ExprL) -> PyParamAttrs e ParameterAttrsL


data PythonParam e l where
  PythonParamVarArgs     :: e P.IdentL       -> e (Maybe Py.ExprL) -> PythonParam e FunctionParameterL
  PythonParamVarArgsKW   :: e P.IdentL       -> e (Maybe Py.ExprL) -> PythonParam e FunctionParameterL
  PythonParamUnpackTuple :: e Py.ParamTupleL -> e (Maybe Py.ExprL) -> PythonParam e FunctionParameterL
  PythonEndPosParam      ::                                           PythonParam e FunctionParameterL

deriveAll [''PyFunDefAttrs, ''PyParamAttrs, ''PythonParam]

pattern PyFunDefAttrs' :: (PyFunDefAttrs :-<: fs, All HFunctor fs) => CxtS h fs a (Maybe Py.ExprL) -> CxtS h fs a FunctionDefAttrsL
pattern $bPyFunDefAttrs' :: CxtS h fs a (Maybe ExprL) -> CxtS h fs a FunctionDefAttrsL
$mPyFunDefAttrs' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(PyFunDefAttrs :-<: fs, All HFunctor fs) =>
CxtS h fs a FunctionDefAttrsL
-> (CxtS h fs a (Maybe ExprL) -> r) -> (Void# -> r) -> r
PyFunDefAttrs' ann <- (project -> Just (PyFunDefAttrs ann)) where
  PyFunDefAttrs' ann :: CxtS h fs a (Maybe ExprL)
ann = CxtS h fs a (Maybe ExprL) -> CxtS h fs a FunctionDefAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(PyFunDefAttrs :-<: fs, InjF fs FunctionDefAttrsL j) =>
CxtS h fs a (Maybe ExprL) -> CxtS h fs a j
iPyFunDefAttrs CxtS h fs a (Maybe ExprL)
ann

pattern PyParamAttrs' :: (PyParamAttrs :-<: fs, All HFunctor fs) => CxtS h fs a (Maybe Py.ExprL) -> CxtS h fs a (Maybe Py.ExprL) -> CxtS h fs a ParameterAttrsL
pattern $bPyParamAttrs' :: CxtS h fs a (Maybe ExprL)
-> CxtS h fs a (Maybe ExprL) -> CxtS h fs a ParameterAttrsL
$mPyParamAttrs' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(PyParamAttrs :-<: fs, All HFunctor fs) =>
CxtS h fs a ParameterAttrsL
-> (CxtS h fs a (Maybe ExprL) -> CxtS h fs a (Maybe ExprL) -> r)
-> (Void# -> r)
-> r
PyParamAttrs' ann def <- (project -> Just (PyParamAttrs ann def)) where
  PyParamAttrs' ann :: CxtS h fs a (Maybe ExprL)
ann def :: CxtS h fs a (Maybe ExprL)
def = CxtS h fs a (Maybe ExprL)
-> CxtS h fs a (Maybe ExprL) -> CxtS h fs a ParameterAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(PyParamAttrs :-<: fs, InjF fs ParameterAttrsL j) =>
CxtS h fs a (Maybe ExprL)
-> CxtS h fs a (Maybe ExprL) -> CxtS h fs a j
iPyParamAttrs CxtS h fs a (Maybe ExprL)
ann CxtS h fs a (Maybe ExprL)
def

-- | FIXME: Python lets you call class/static methods through an instance.
-- I should probably model this similarly to how I do so for Java, or create a more interesting representation
-- that separates syntactic function definitions from their semantic values. Alternatively, since there's a deadline
-- and I only need a prototype, I can also just ignore this issue. I choose the latter.

createSortInclusionTypes [ ''P.FunctionCallL, ''Py.ExprL,       ''Py.ExprL,            ''Py.ExprL,    ''P.FunctionDefL, ''PyBlockL
                         ] [
                           ''Py.ExprL,        ''P.FunctionExpL, ''P.PositionalArgExpL, ''P.ReceiverL, ''Py.StatementL,  ''P.FunctionBodyL
                         ]
deriveAll [ ''FunctionCallIsExpr, ''ExprIsFunctionExp, ''ExprIsPositionalArgExp, ''ExprIsReceiver
          , ''FunctionDefIsStatement, ''PyBlockIsFunctionBody]
createSortInclusionInfers [ ''P.FunctionCallL, ''Py.ExprL,       ''Py.ExprL,            ''Py.ExprL,    ''P.FunctionDefL, ''PyBlockL
                          ] [
                            ''Py.ExprL,        ''P.FunctionExpL, ''P.PositionalArgExpL, ''P.ReceiverL, ''Py.StatementL,  ''P.FunctionBodyL
                          ]

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


do let pythonSortInjections = [ ''IdentIsIdent, ''AssignIsStatement, ''ExprIsRhs, ''StatementIsBlockItem, ''PyCompIsExpr
                              , ''IdentIsPyLValue, ''PyClassIsStatement
                              , ''FunctionCallIsExpr, ''ExprIsFunctionExp, ''ExprIsPositionalArgExp, ''ExprIsReceiver
                              , ''FunctionDefIsStatement, ''PyBlockIsFunctionBody]
   let names = (pythonSigNames \\ [mkName "Ident"])
                    ++ pythonSortInjections
                    ++ [ ''PyLhs, ''TupleLValue, ''ListLValue, ''DotLValue, ''StarLValue, ''SubscriptLValue, ''SliceLValue, ''ParenLValue]
                    ++ [ ''PyWith, ''PyWithBinder
                       , ''PythonArg, ''PyFunDefAttrs, ''PyParamAttrs, ''PythonParam
                       , ''PyStringLit, ''PyBlock, ''PyClass, ''PyComp, ''PyCondExpr
                       , ''PyComprehensionExpr, ''PyComprehension]
                    ++ [ ''P.Ident, ''AssignOpEquals, ''Assign, ''P.Block, ''EmptyBlockEnd
                       , ''P.FunctionCall, ''P.EmptyFunctionCallAttrs, ''FunctionIdent, ''FunctionArgumentList, ''PositionalArgument, ''ReceiverArg
                       , ''FunctionDef, ''PositionalParameter]

   sumDec <- runCompTrans $ makeSumType "MPythonSig" names
   return sumDec

type instance InjectableSorts MPythonSig AssignL = '[StatementL]

type MPythonTerm    = Term MPythonSig
type MPythonTermLab = TermLab MPythonSig

type MPythonCxt h a = CxtS h MPythonSig a

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

instance InjF MPythonSig [PyLValueL] LhsL where
  injF :: CxtS h MPythonSig a [PyLValueL] -> CxtS h MPythonSig a LhsL
injF = CxtS h MPythonSig a [PyLValueL] -> CxtS h MPythonSig a LhsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(PyLhs :-<: fs, InjF fs LhsL j) =>
CxtS h fs a [PyLValueL] -> CxtS h fs a j
iPyLhs
  projF' :: Cxt h (Sum MPythonSig :&: p) a LhsL
-> Maybe (Cxt h (Sum MPythonSig :&: p) a [PyLValueL])
projF' x :: Cxt h (Sum MPythonSig :&: p) a LhsL
x = do
    PyLhs ls :: Cxt h (Sum MPythonSig :&: p) a [PyLValueL]
ls <- Cxt h (Sum MPythonSig :&: p) a LhsL
-> Maybe (PyLhs (Cxt h (Sum MPythonSig :&: 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 MPythonSig :&: p) a LhsL
x
    Cxt h (Sum MPythonSig :&: p) a [PyLValueL]
-> Maybe (Cxt h (Sum MPythonSig :&: p) a [PyLValueL])
forall (m :: * -> *) a. Monad m => a -> m a
return Cxt h (Sum MPythonSig :&: p) a [PyLValueL]
ls

instance InjF MPythonSig P.IdentL Py.ExprL where
  injF :: CxtS h MPythonSig a IdentL -> CxtS h MPythonSig a ExprL
injF x :: CxtS h MPythonSig a IdentL
x = CxtS h MPythonSig a IdentL
-> CxtS h MPythonSig a () -> CxtS h MPythonSig a ExprL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(Expr :-<: fs, InjF fs ExprL j) =>
CxtS h fs a IdentL -> CxtS h fs a () -> CxtS h fs a j
Py.iVar (CxtS h MPythonSig a IdentL -> CxtS h MPythonSig 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 MPythonSig a IdentL
x) CxtS h MPythonSig a ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF
  projF' :: Cxt h (Sum MPythonSig :&: p) a ExprL
-> Maybe (Cxt h (Sum MPythonSig :&: p) a IdentL)
projF' x :: Cxt h (Sum MPythonSig :&: p) a ExprL
x
    | Just (Py.Var v :: Cxt h (Sum MPythonSig :&: p) a IdentL
v _) <- Cxt h (Sum MPythonSig :&: p) a ExprL
-> Maybe (Expr (Cxt h (Sum MPythonSig :&: p) a) ExprL)
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 MPythonSig :&: p) a ExprL
x
    , Just (IdentIsIdent i :: Cxt h (Sum MPythonSig :&: p) a IdentL
i) <- Cxt h (Sum MPythonSig :&: p) a IdentL
-> Maybe (IdentIsIdent (Cxt h (Sum MPythonSig :&: 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 MPythonSig :&: p) a IdentL
v
    = Cxt h (Sum MPythonSig :&: p) a IdentL
-> Maybe (Cxt h (Sum MPythonSig :&: p) a IdentL)
forall (m :: * -> *) a. Monad m => a -> m a
return Cxt h (Sum MPythonSig :&: p) a IdentL
i
  projF' _ = Maybe (Cxt h (Sum MPythonSig :&: p) a IdentL)
forall a. Maybe a
Nothing

instance InjF MPythonSig P.IdentL LhsL where
  injF :: CxtS h MPythonSig a IdentL -> CxtS h MPythonSig a LhsL
injF n :: CxtS h MPythonSig a IdentL
n = CxtS h MPythonSig a [PyLValueL] -> CxtS h MPythonSig a LhsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(PyLhs :-<: fs, InjF fs LhsL j) =>
CxtS h fs a [PyLValueL] -> CxtS h fs a j
iPyLhs (CxtS h MPythonSig a [PyLValueL] -> CxtS h MPythonSig a LhsL)
-> CxtS h MPythonSig a [PyLValueL] -> CxtS h MPythonSig a LhsL
forall a b. (a -> b) -> a -> b
$ [Cxt h (Sum MPythonSig) a PyLValueL]
-> CxtS h MPythonSig a [PyLValueL]
forall (f :: * -> *) (e :: * -> *) l.
(InsertF f e, Typeable l) =>
f (e l) -> e (f l)
insertF [CxtS h MPythonSig a IdentL -> Cxt h (Sum MPythonSig) a PyLValueL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF CxtS h MPythonSig a IdentL
n]
  projF' :: Cxt h (Sum MPythonSig :&: p) a LhsL
-> Maybe (Cxt h (Sum MPythonSig :&: p) a IdentL)
projF' t :: Cxt h (Sum MPythonSig :&: p) a LhsL
t
    | Just (PyLhs es :: Cxt h (Sum MPythonSig :&: p) a [PyLValueL]
es) <- Cxt h (Sum MPythonSig :&: p) a LhsL
-> Maybe (PyLhs (Cxt h (Sum MPythonSig :&: 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 MPythonSig :&: p) a LhsL
t
    , Just (ConsF e :: Cxt h (Sum MPythonSig :&: p) a l
e rest :: Cxt h (Sum MPythonSig :&: p) a [l]
rest) <- Cxt h (Sum MPythonSig :&: p) a [PyLValueL]
-> Maybe (ListF (Cxt h (Sum MPythonSig :&: p) a) [PyLValueL])
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 MPythonSig :&: p) a [PyLValueL]
es
    , Just NilF <- Cxt h (Sum MPythonSig :&: p) a [l]
-> Maybe (ListF (Cxt h (Sum MPythonSig :&: p) a) [l])
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 MPythonSig :&: p) a [l]
rest
    = Cxt h (Sum MPythonSig :&: p) a l
-> Maybe (Cxt h (Sum MPythonSig :&: 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 MPythonSig :&: p) a l
e
  projF' _ = Maybe (Cxt h (Sum MPythonSig :&: p) a IdentL)
forall a. Maybe a
Nothing

instance InjF MPythonSig AssignL BlockItemL where
  injF :: CxtS h MPythonSig a AssignL -> CxtS h MPythonSig a BlockItemL
injF = CxtS h MPythonSig a AssignL -> CxtS h MPythonSig a BlockItemL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(AssignIsStatement :-<: fs, InjF fs StatementL j) =>
CxtS h fs a AssignL -> CxtS h fs a j
iAssignIsStatement
  projF' :: Cxt h (Sum MPythonSig :&: p) a BlockItemL
-> Maybe (Cxt h (Sum MPythonSig :&: p) a AssignL)
projF' t :: Cxt h (Sum MPythonSig :&: p) a BlockItemL
t
    | Just (StatementIsBlockItem s :: Cxt h (Sum MPythonSig :&: p) a StatementL
s) <- Cxt h (Sum MPythonSig :&: p) a BlockItemL
-> Maybe
     (StatementIsBlockItem (Cxt h (Sum MPythonSig :&: 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 MPythonSig :&: p) a BlockItemL
t
    , Just (AssignIsStatement a :: Cxt h (Sum MPythonSig :&: p) a AssignL
a) <- Cxt h (Sum MPythonSig :&: p) a StatementL
-> Maybe
     (AssignIsStatement (Cxt h (Sum MPythonSig :&: p) a) StatementL)
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 MPythonSig :&: p) a StatementL
s
    = Cxt h (Sum MPythonSig :&: p) a AssignL
-> Maybe (Cxt h (Sum MPythonSig :&: p) a AssignL)
forall (m :: * -> *) a. Monad m => a -> m a
return Cxt h (Sum MPythonSig :&: p) a AssignL
a
  projF' _ = Maybe (Cxt h (Sum MPythonSig :&: p) a AssignL)
forall a. Maybe a
Nothing

instance InjF MPythonSig P.IdentL FunctionExpL where
  injF :: CxtS h MPythonSig a IdentL -> CxtS h MPythonSig a FunctionExpL
injF x :: CxtS h MPythonSig a IdentL
x = CxtS h MPythonSig a IdentL
-> CxtS h MPythonSig a () -> CxtS h MPythonSig a FunctionExpL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(Expr :-<: fs, InjF fs ExprL j) =>
CxtS h fs a IdentL -> CxtS h fs a () -> CxtS h fs a j
iVar (CxtS h MPythonSig a IdentL -> CxtS h MPythonSig 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 MPythonSig a IdentL
x) CxtS h MPythonSig a ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF

  projF' :: Cxt h (Sum MPythonSig :&: p) a FunctionExpL
-> Maybe (Cxt h (Sum MPythonSig :&: p) a IdentL)
projF' (Cxt h (Sum MPythonSig :&: p) a FunctionExpL
-> Maybe
     (FunctionIdent (Cxt h (Sum MPythonSig :&: 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 n :: Cxt h (Sum MPythonSig :&: p) a IdentL
n)) = Cxt h (Sum MPythonSig :&: p) a IdentL
-> Maybe (Cxt h (Sum MPythonSig :&: p) a IdentL)
forall a. a -> Maybe a
Just Cxt h (Sum MPythonSig :&: p) a IdentL
n
  projF' f :: Cxt h (Sum MPythonSig :&: p) a FunctionExpL
f
    | Just (ExprIsFunctionExp e :: Cxt h (Sum MPythonSig :&: p) a ExprL
e) <- Cxt h (Sum MPythonSig :&: p) a FunctionExpL
-> Maybe
     (ExprIsFunctionExp (Cxt h (Sum MPythonSig :&: 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 MPythonSig :&: p) a FunctionExpL
f
    , Just (Var v :: Cxt h (Sum MPythonSig :&: p) a IdentL
v _) <- Cxt h (Sum MPythonSig :&: p) a ExprL
-> Maybe (Expr (Cxt h (Sum MPythonSig :&: p) a) ExprL)
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 MPythonSig :&: p) a ExprL
e = Cxt h (Sum MPythonSig :&: p) a IdentL
-> Maybe (Cxt h (Sum MPythonSig :&: 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 MPythonSig :&: p) a IdentL
v
  projF' _                                    = Maybe (Cxt h (Sum MPythonSig :&: p) a IdentL)
forall a. Maybe a
Nothing

instance InjF MPythonSig P.IdentL PositionalArgExpL where
  injF :: CxtS h MPythonSig a IdentL -> CxtS h MPythonSig a PositionalArgExpL
injF = CxtS h MPythonSig a ExprL -> CxtS h MPythonSig a PositionalArgExpL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(ExprIsPositionalArgExp :-<: fs, InjF fs PositionalArgExpL j) =>
CxtS h fs a ExprL -> CxtS h fs a j
iExprIsPositionalArgExp (CxtS h MPythonSig a ExprL
 -> CxtS h MPythonSig a PositionalArgExpL)
-> (CxtS h MPythonSig a IdentL -> CxtS h MPythonSig a ExprL)
-> CxtS h MPythonSig a IdentL
-> CxtS h MPythonSig a PositionalArgExpL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtS h MPythonSig a IdentL -> CxtS h MPythonSig a ExprL
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
injF
  projF' :: Cxt h (Sum MPythonSig :&: p) a PositionalArgExpL
-> Maybe (Cxt h (Sum MPythonSig :&: p) a IdentL)
projF' t :: Cxt h (Sum MPythonSig :&: p) a PositionalArgExpL
t
   | Just (ExprIsPositionalArgExp e :: Cxt h (Sum MPythonSig :&: p) a ExprL
e) <- Cxt h (Sum MPythonSig :&: p) a PositionalArgExpL
-> Maybe
     (ExprIsPositionalArgExp
        (Cxt h (Sum MPythonSig :&: 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 MPythonSig :&: p) a PositionalArgExpL
t = Cxt h (Sum MPythonSig :&: p) a ExprL
-> Maybe (Cxt h (Sum MPythonSig :&: 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 MPythonSig :&: p) a ExprL
e
  projF' _ = Maybe (Cxt h (Sum MPythonSig :&: p) a IdentL)
forall a. Maybe a
Nothing

#endif