{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- Only because can't make overlapping in TH
{-# LANGUAGE OverlappingInstances #-}
-- |

module Cubix.Language.Parametric.Syntax.VarDecl (
    IdentL
  , Ident(..)

  , MultiLocalVarDeclCommonAttrsL
  , LocalVarInitL
  , IsOptional(..)
  , OptLocalVarInitL
  , OptLocalVarInit(..)
  , LocalVarDeclAttrsL
  , TupleBinder(..)
  , IdentIsVarDeclBinder(..)
  , EmptyLocalVarDeclAttrs(..)
  , VarDeclBinderL
  , SingleLocalVarDeclL
  , SingleLocalVarDecl(..)
  , EmptyMultiLocalVarDeclCommonAttrs
  , MultiLocalVarDeclL
  , MultiLocalVarDecl(..)

  , AssignOpL
  , AssignOpEquals(..)
  , LhsL
  , RhsL
  , AssignL
  , Assign(..)

  , BlockItemL
  , BlockEndL
  , EmptyBlockEnd(..)
  , BlockL
  , Block(..)
  , EmptyBlockItem(..)


  , pattern Ident'
  ,        iIdent

  , pattern JustLocalVarInit'
  ,        iJustLocalVarInit
  , pattern NoLocalVarInit'
  ,        iNoLocalVarInit

  , pattern EmptyLocalVarDeclAttrs'
  ,        iEmptyLocalVarDeclAttrs

  , pattern TupleBinder'
  ,        iTupleBinder
  , pattern IdentIsVarDeclBinder'
  ,        iIdentIsVarDeclBinder
  , pattern SingleLocalVarDecl'
  ,        iSingleLocalVarDecl

  , pattern EmptyMultiLocalVarDeclCommonAttrs'
  ,        iEmptyMultiLocalVarDeclCommonAttrs

  , pattern MultiLocalVarDecl'
  ,        iMultiLocalVarDecl

  , pattern AssignOpEquals'
  ,        iAssignOpEquals
  , pattern Assign'
  ,        iAssign
  , pattern EmptyBlockEnd'
  ,        iEmptyBlockEnd
  , pattern Block'
  ,        iBlock
  , pattern EmptyBlockItem'
  ,        iEmptyBlockItem
  ) where

import Data.Comp.Multi ( project, project', HFunctor, (:-<:), All, CxtS)
import Cubix.Language.Parametric.Derive
import Cubix.Language.Parametric.InjF

data IdentL
data Ident (e :: * -> *) l where
  Ident :: String -> Ident e IdentL

deriveAll [''Ident]

pattern Ident' :: (Ident :-<: fs, All HFunctor fs) => String -> CxtS h fs a IdentL
pattern $bIdent' :: String -> CxtS h fs a IdentL
$mIdent' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(Ident :-<: fs, All HFunctor fs) =>
CxtS h fs a IdentL -> (String -> r) -> (Void# -> r) -> r
Ident' s <- (project -> (Just (Ident s))) where
  Ident' s :: String
s = String -> CxtS h fs a IdentL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(Ident :-<: fs, InjF fs IdentL j) =>
String -> CxtS h fs a j
iIdent String
s

data MultiLocalVarDeclCommonAttrsL
data LocalVarInitL

data IsOptional = Optional | NotOptional


data OptLocalVarInitL

-- Machinery not yet ready for this kind of parameterization
--data OptLocalVarInit opt e l where
--  JustLocalVarInit :: e LocalVarInitL -> OptLocalVarInit opt e OptLocalVarInitL
--  NoLocalVarInit   :: OptLocalVarInit Optional e OptLocalVarInitL

data OptLocalVarInit e l where
  JustLocalVarInit :: e LocalVarInitL -> OptLocalVarInit e OptLocalVarInitL
  NoLocalVarInit   :: OptLocalVarInit e OptLocalVarInitL

deriveAll [''OptLocalVarInit]

pattern JustLocalVarInit' :: (OptLocalVarInit :-<: fs, All HFunctor fs) => CxtS h fs a LocalVarInitL -> CxtS h fs a OptLocalVarInitL
pattern $bJustLocalVarInit' :: CxtS h fs a LocalVarInitL -> CxtS h fs a OptLocalVarInitL
$mJustLocalVarInit' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(OptLocalVarInit :-<: fs, All HFunctor fs) =>
CxtS h fs a OptLocalVarInitL
-> (CxtS h fs a LocalVarInitL -> r) -> (Void# -> r) -> r
JustLocalVarInit' x <- (project -> Just (JustLocalVarInit x)) where
  JustLocalVarInit' x :: CxtS h fs a LocalVarInitL
x = CxtS h fs a LocalVarInitL -> CxtS h fs a OptLocalVarInitL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(OptLocalVarInit :-<: fs, InjF fs OptLocalVarInitL j) =>
CxtS h fs a LocalVarInitL -> CxtS h fs a j
iJustLocalVarInit CxtS h fs a LocalVarInitL
x

pattern NoLocalVarInit' :: (OptLocalVarInit :-<: fs, All HFunctor fs) => CxtS h fs a OptLocalVarInitL
pattern $bNoLocalVarInit' :: CxtS h fs a OptLocalVarInitL
$mNoLocalVarInit' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(OptLocalVarInit :-<: fs, All HFunctor fs) =>
CxtS h fs a OptLocalVarInitL -> (Void# -> r) -> (Void# -> r) -> r
NoLocalVarInit' <- (project -> Just NoLocalVarInit) where
  NoLocalVarInit' = CxtS h fs a OptLocalVarInitL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(OptLocalVarInit :-<: fs, InjF fs OptLocalVarInitL j) =>
CxtS h fs a j
iNoLocalVarInit

data LocalVarDeclAttrsL

-- Needs better name because may need to distinguish part of multi-decl from a standalone decl
------ That's a really hypothetical thing. Why, Jimmy, why

data EmptyLocalVarDeclAttrs (e :: * -> *) l where
  EmptyLocalVarDeclAttrs :: EmptyLocalVarDeclAttrs e LocalVarDeclAttrsL

deriveAll [''EmptyLocalVarDeclAttrs]

pattern EmptyLocalVarDeclAttrs' :: (EmptyLocalVarDeclAttrs :-<: fs, All HFunctor fs) => CxtS h fs a LocalVarDeclAttrsL
pattern $bEmptyLocalVarDeclAttrs' :: CxtS h fs a LocalVarDeclAttrsL
$mEmptyLocalVarDeclAttrs' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(EmptyLocalVarDeclAttrs :-<: fs, All HFunctor fs) =>
CxtS h fs a LocalVarDeclAttrsL -> (Void# -> r) -> (Void# -> r) -> r
EmptyLocalVarDeclAttrs' <- (project -> Just EmptyLocalVarDeclAttrs) where
  EmptyLocalVarDeclAttrs' = CxtS h fs a LocalVarDeclAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(EmptyLocalVarDeclAttrs :-<: fs, InjF fs LocalVarDeclAttrsL j) =>
CxtS h fs a j
iEmptyLocalVarDeclAttrs


data VarDeclBinderL
-- | Represents declaring a list of identifiers, where the list of identifiers
-- should be thought of a single entity being declared. Not to be used as the LHS of an assignment
--
-- This models the (x,y) = (1,2) pattern found in Haskell, or "local x,y" in Lua
data TupleBinder e l where
  TupleBinder :: e [IdentL] -> TupleBinder e VarDeclBinderL

deriveAll [''TupleBinder]

pattern TupleBinder' :: (TupleBinder :-<: fs, All HFunctor fs) => CxtS h fs a [IdentL] -> CxtS h fs a VarDeclBinderL
pattern $bTupleBinder' :: CxtS h fs a [IdentL] -> CxtS h fs a VarDeclBinderL
$mTupleBinder' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(TupleBinder :-<: fs, All HFunctor fs) =>
CxtS h fs a VarDeclBinderL
-> (CxtS h fs a [IdentL] -> r) -> (Void# -> r) -> r
TupleBinder' xs <- (project -> Just (TupleBinder xs)) where
  TupleBinder' xs :: CxtS h fs a [IdentL]
xs = CxtS h fs a [IdentL] -> CxtS h fs a VarDeclBinderL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(TupleBinder :-<: fs, InjF fs VarDeclBinderL j) =>
CxtS h fs a [IdentL] -> CxtS h fs a j
iTupleBinder CxtS h fs a [IdentL]
xs


instance (TupleBinder :-<: fs, All HFunctor fs) => InjF fs [IdentL] VarDeclBinderL where
  injF :: CxtS h fs a [IdentL] -> CxtS h fs a VarDeclBinderL
injF = CxtS h fs a [IdentL] -> CxtS h fs a VarDeclBinderL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(TupleBinder :-<: fs, InjF fs VarDeclBinderL j) =>
CxtS h fs a [IdentL] -> CxtS h fs a j
iTupleBinder

  projF' :: Cxt h (Sum fs :&: p) a VarDeclBinderL
-> Maybe (Cxt h (Sum fs :&: p) a [IdentL])
projF' (Cxt h (Sum fs :&: p) a VarDeclBinderL
-> Maybe (TupleBinder (Cxt h (Sum fs :&: 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' -> Just (TupleBinder ns :: Cxt h (Sum fs :&: p) a [IdentL]
ns)) = Cxt h (Sum fs :&: p) a [IdentL]
-> Maybe (Cxt h (Sum fs :&: p) a [IdentL])
forall a. a -> Maybe a
Just Cxt h (Sum fs :&: p) a [IdentL]
ns
  projF' _                                   = Maybe (Cxt h (Sum fs :&: p) a [IdentL])
forall a. Maybe a
Nothing

createSortInclusionType ''IdentL ''VarDeclBinderL
deriveAll [''IdentIsVarDeclBinder]
createSortInclusionInfer ''IdentL ''VarDeclBinderL

pattern IdentIsVarDeclBinder' :: (IdentIsVarDeclBinder :-<: fs, All HFunctor fs) => CxtS h fs a IdentL -> CxtS h fs a VarDeclBinderL
pattern $bIdentIsVarDeclBinder' :: CxtS h fs a IdentL -> CxtS h fs a VarDeclBinderL
$mIdentIsVarDeclBinder' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(IdentIsVarDeclBinder :-<: fs, All HFunctor fs) =>
CxtS h fs a VarDeclBinderL
-> (CxtS h fs a IdentL -> r) -> (Void# -> r) -> r
IdentIsVarDeclBinder' n <- (project -> Just (IdentIsVarDeclBinder n)) where
  IdentIsVarDeclBinder' n :: CxtS h fs a IdentL
n = CxtS h fs a IdentL -> CxtS h fs a VarDeclBinderL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(IdentIsVarDeclBinder :-<: fs, InjF fs VarDeclBinderL j) =>
CxtS h fs a IdentL -> CxtS h fs a j
iIdentIsVarDeclBinder CxtS h fs a IdentL
n


-- |
-- See MultiLocalVarDecl spec
--
-- If no LocalVarInit is present, then the declared variable is unitialized, and may not be referenced until another language
-- If a LocalVarInit is present, then it is executed immediately, before placing the variable in scope, and the result is stored
-- in the declared variable.
--
-- We assume this variable can only be referenced by something enclosed by the local block which contains
-- an identifier contained within the var binder, or at least by something assigned to some value derived from
-- such a reference.
--
-- This forbids a newly-declared variable from referring to itself (sorry Haskell)
-- This does not model C's "static" keyword
--
-- FIXME: So.....I wrote that variables declared without an initializer are unitialized, but that does not model Lua.
-- Luckily, I don't actually depend on this anywhere.
data SingleLocalVarDeclL
data SingleLocalVarDecl e l where
  SingleLocalVarDecl :: e LocalVarDeclAttrsL -> e VarDeclBinderL -> e OptLocalVarInitL -> SingleLocalVarDecl e SingleLocalVarDeclL

deriveAll [''SingleLocalVarDecl]

pattern SingleLocalVarDecl' ::
  ( SingleLocalVarDecl :-<: fs
  , All HFunctor fs
  ) => CxtS h fs a LocalVarDeclAttrsL
  -> CxtS h fs a VarDeclBinderL
  -> CxtS h fs a OptLocalVarInitL
  -> CxtS h fs a SingleLocalVarDeclL
pattern $bSingleLocalVarDecl' :: CxtS h fs a LocalVarDeclAttrsL
-> CxtS h fs a VarDeclBinderL
-> CxtS h fs a OptLocalVarInitL
-> CxtS h fs a SingleLocalVarDeclL
$mSingleLocalVarDecl' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(SingleLocalVarDecl :-<: fs, All HFunctor fs) =>
CxtS h fs a SingleLocalVarDeclL
-> (CxtS h fs a LocalVarDeclAttrsL
    -> CxtS h fs a VarDeclBinderL -> CxtS h fs a OptLocalVarInitL -> r)
-> (Void# -> r)
-> r
SingleLocalVarDecl' x y z <- (project -> (Just (SingleLocalVarDecl x y z))) where
  SingleLocalVarDecl' x :: CxtS h fs a LocalVarDeclAttrsL
x y :: CxtS h fs a VarDeclBinderL
y z :: CxtS h fs a OptLocalVarInitL
z = CxtS h fs a LocalVarDeclAttrsL
-> CxtS h fs a VarDeclBinderL
-> CxtS h fs a OptLocalVarInitL
-> CxtS h fs a SingleLocalVarDeclL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(SingleLocalVarDecl :-<: fs, InjF fs SingleLocalVarDeclL j) =>
CxtS h fs a LocalVarDeclAttrsL
-> CxtS h fs a VarDeclBinderL
-> CxtS h fs a OptLocalVarInitL
-> CxtS h fs a j
iSingleLocalVarDecl CxtS h fs a LocalVarDeclAttrsL
x CxtS h fs a VarDeclBinderL
y CxtS h fs a OptLocalVarInitL
z


data EmptyMultiLocalVarDeclCommonAttrs (e :: * -> *) l where
  EmptyMultiLocalVarDeclCommonAttrs :: EmptyMultiLocalVarDeclCommonAttrs e MultiLocalVarDeclCommonAttrsL

deriveAll [''EmptyMultiLocalVarDeclCommonAttrs]

pattern EmptyMultiLocalVarDeclCommonAttrs' :: (EmptyMultiLocalVarDeclCommonAttrs :-<: fs, All HFunctor fs) => CxtS h fs a MultiLocalVarDeclCommonAttrsL
pattern $bEmptyMultiLocalVarDeclCommonAttrs' :: CxtS h fs a MultiLocalVarDeclCommonAttrsL
$mEmptyMultiLocalVarDeclCommonAttrs' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(EmptyMultiLocalVarDeclCommonAttrs :-<: fs, All HFunctor fs) =>
CxtS h fs a MultiLocalVarDeclCommonAttrsL
-> (Void# -> r) -> (Void# -> r) -> r
EmptyMultiLocalVarDeclCommonAttrs' <- (project -> Just EmptyMultiLocalVarDeclCommonAttrs) where
  EmptyMultiLocalVarDeclCommonAttrs' = CxtS h fs a MultiLocalVarDeclCommonAttrsL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(EmptyMultiLocalVarDeclCommonAttrs :-<: fs,
 InjF fs MultiLocalVarDeclCommonAttrsL j) =>
CxtS h fs a j
iEmptyMultiLocalVarDeclCommonAttrs

-- | Informal spec:
--
-- There is a notion of variable scope. Executing a MultiLocalVarDecl statement places each local variable declared into scope.
-- Our intention is that MultiLocalVarDecl is only to be used for local declarations, although we have not yet found
-- a reason why it can't be used for top-level variable declarations as in C.
--
-- -- Multi local var decl
-- Each variable declaration has no effect save putting the variable into scope, and executing the initializer expression.
-- Initializer expressions, if present, are executed in left-to-right order. If the language has a notion of
-- an initialized variable, then all declarations for which an initializer is present will be considered initialized.
--
-- Executing a MultiLocalVarDecl will execute all contained SingleLocalVardecl
--
-- Note: C++ variable declarations cannot use this, because the declarations are effectful
-- FIXME: Does not really give a good account for space allocation (e.g.: references to local variables)
data MultiLocalVarDeclL
data MultiLocalVarDecl e l where
  MultiLocalVarDecl :: e MultiLocalVarDeclCommonAttrsL -> e [SingleLocalVarDeclL] -> MultiLocalVarDecl e MultiLocalVarDeclL


deriveAll [''MultiLocalVarDecl]

pattern MultiLocalVarDecl' ::
  ( MultiLocalVarDecl :-<: fs
  , All HFunctor fs
  ) => CxtS h fs a MultiLocalVarDeclCommonAttrsL
  -> CxtS h fs a [SingleLocalVarDeclL]
  -> CxtS h fs a MultiLocalVarDeclL
pattern $bMultiLocalVarDecl' :: CxtS h fs a MultiLocalVarDeclCommonAttrsL
-> CxtS h fs a [SingleLocalVarDeclL]
-> CxtS h fs a MultiLocalVarDeclL
$mMultiLocalVarDecl' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(MultiLocalVarDecl :-<: fs, All HFunctor fs) =>
CxtS h fs a MultiLocalVarDeclL
-> (CxtS h fs a MultiLocalVarDeclCommonAttrsL
    -> CxtS h fs a [SingleLocalVarDeclL] -> r)
-> (Void# -> r)
-> r
MultiLocalVarDecl' x y <- (project -> (Just (MultiLocalVarDecl x y))) where
  MultiLocalVarDecl' x :: CxtS h fs a MultiLocalVarDeclCommonAttrsL
x y :: CxtS h fs a [SingleLocalVarDeclL]
y = CxtS h fs a MultiLocalVarDeclCommonAttrsL
-> CxtS h fs a [SingleLocalVarDeclL]
-> CxtS h fs a MultiLocalVarDeclL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(MultiLocalVarDecl :-<: fs, InjF fs MultiLocalVarDeclL j) =>
CxtS h fs a MultiLocalVarDeclCommonAttrsL
-> CxtS h fs a [SingleLocalVarDeclL] -> CxtS h fs a j
iMultiLocalVarDecl CxtS h fs a MultiLocalVarDeclCommonAttrsL
x CxtS h fs a [SingleLocalVarDeclL]
y


-- |
-- See spec for assign
--
-- We assume that AssignOpEquals has, as its associated f_op, the function f(x,y)=(typeof x)y
-- where (typeof x)y denotes a type conversion from y to the type of x. We leave it unspecified what
-- exactly that means
data AssignOpL
data AssignOpEquals (e :: * -> *) l where
  AssignOpEquals :: AssignOpEquals e AssignOpL

deriveAll [''AssignOpEquals]

pattern AssignOpEquals' :: (AssignOpEquals :-<: fs, All HFunctor fs) => CxtS h fs a AssignOpL
pattern $bAssignOpEquals' :: CxtS h fs a AssignOpL
$mAssignOpEquals' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(AssignOpEquals :-<: fs, All HFunctor fs) =>
CxtS h fs a AssignOpL -> (Void# -> r) -> (Void# -> r) -> r
AssignOpEquals' <- (project -> Just AssignOpEquals) where
  AssignOpEquals' = CxtS h fs a AssignOpL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(AssignOpEquals :-<: fs, InjF fs AssignOpL j) =>
CxtS h fs a j
iAssignOpEquals

data LhsL
data RhsL

-- |
-- The Assign node must have semantics of the following form:
--
-- store(lhs',f_op(lhs', eval(rhs)))
--   where lhs' = evalToLoc(lhs)
--
-- where eval and evalToLoc are arbitrary evaluation function (potentially with side effects)
--
-- The lhs must be evaluated before the rhs.
--
--Note that C can contain arbitrary function calls in lvalues
--
-- If an assign may be used in an expression context, then the store takes effect before its return value, all effects
-- in eval(rhs) take effect before the return, and the return value is the value assigned to lhs
--
-- If the LHS is a variable, it will be considered initialized after execution of the Assign
--
-- FIXME: This spec should maybe contain something like "every var init can be a valid assign", because there
-- are restrictions on assignments, e.g.: C can assign between lvalues with partial overlap. This opens up a rabbit
-- hole of possible constraints we need to specify to avoid allowing transformations to create invalid programs
data AssignL
data Assign e l where
  Assign :: e LhsL -> e AssignOpL -> e RhsL -> Assign e AssignL

deriveAll [''Assign]

pattern Assign' :: (Assign :-<: fs, All HFunctor fs) => CxtS h fs a LhsL -> CxtS h fs a AssignOpL -> CxtS h fs a RhsL -> CxtS h fs a AssignL
pattern $bAssign' :: CxtS h fs a LhsL
-> CxtS h fs a AssignOpL -> CxtS h fs a RhsL -> CxtS h fs a AssignL
$mAssign' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(Assign :-<: fs, All HFunctor fs) =>
CxtS h fs a AssignL
-> (CxtS h fs a LhsL
    -> CxtS h fs a AssignOpL -> CxtS h fs a RhsL -> r)
-> (Void# -> r)
-> r
Assign' l o r <- (project -> Just (Assign l o r)) where
  Assign' l :: CxtS h fs a LhsL
l o :: CxtS h fs a AssignOpL
o r :: CxtS h fs a RhsL
r = CxtS h fs a LhsL
-> CxtS h fs a AssignOpL -> CxtS h fs a RhsL -> CxtS h fs a AssignL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(Assign :-<: fs, InjF fs AssignL j) =>
CxtS h fs a LhsL
-> CxtS h fs a AssignOpL -> CxtS h fs a RhsL -> CxtS h fs a j
iAssign CxtS h fs a LhsL
l CxtS h fs a AssignOpL
o CxtS h fs a RhsL
r


data BlockItemL
data BlockEndL
data BlockL

data EmptyBlockEnd (e :: * -> *) l where
  EmptyBlockEnd :: EmptyBlockEnd e BlockEndL

deriveAll [''EmptyBlockEnd]

pattern EmptyBlockEnd' :: (EmptyBlockEnd :-<: fs, All HFunctor fs) => CxtS h fs a BlockEndL
pattern $bEmptyBlockEnd' :: CxtS h fs a BlockEndL
$mEmptyBlockEnd' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(EmptyBlockEnd :-<: fs, All HFunctor fs) =>
CxtS h fs a BlockEndL -> (Void# -> r) -> (Void# -> r) -> r
EmptyBlockEnd' <- (project -> Just EmptyBlockEnd) where
  EmptyBlockEnd' = CxtS h fs a BlockEndL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(EmptyBlockEnd :-<: fs, InjF fs BlockEndL j) =>
CxtS h fs a j
iEmptyBlockEnd

-- | Block has the following semantics
-- * Any variable introduced by MultiLocalVarDecl may not be referenced outside of the items contained in this block.
-- * Beware that languages such as JavaScript have assignment constructs which do not obey this. We place
-- * no limitation on the visibilty of other kinds of declarations.
--
-- We are also using this to model function bodies in Python, though these
-- have the additional restriction of being nonempty
data Block e l where
  Block :: e [BlockItemL] -> e BlockEndL -> Block e BlockL

deriveAll [''Block]

pattern Block' :: (Block :-<: fs, All HFunctor fs) => CxtS h fs a [BlockItemL] -> CxtS h fs a BlockEndL -> CxtS h fs a BlockL
pattern $bBlock' :: CxtS h fs a [BlockItemL]
-> CxtS h fs a BlockEndL -> CxtS h fs a BlockL
$mBlock' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(Block :-<: fs, All HFunctor fs) =>
CxtS h fs a BlockL
-> (CxtS h fs a [BlockItemL] -> CxtS h fs a BlockEndL -> r)
-> (Void# -> r)
-> r
Block' xs e <- (project -> Just (Block xs e)) where
  Block' xs :: CxtS h fs a [BlockItemL]
xs e :: CxtS h fs a BlockEndL
e = CxtS h fs a [BlockItemL]
-> CxtS h fs a BlockEndL -> CxtS h fs a BlockL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(Block :-<: fs, InjF fs BlockL j) =>
CxtS h fs a [BlockItemL] -> CxtS h fs a BlockEndL -> CxtS h fs a j
iBlock CxtS h fs a [BlockItemL]
xs CxtS h fs a BlockEndL
e

-- | This is inserted at the end of blocks
-- so that there's a place to insert at the end of blocks,
-- and so that the sort of empty block-item lists can be correctly determined
--
-- This is a bit of a hack....but, it's actually kinda nice in some ways
data EmptyBlockItem (e :: * -> *) l where
  EmptyBlockItem :: EmptyBlockItem e BlockItemL

deriveAll [''EmptyBlockItem]

pattern EmptyBlockItem' :: (EmptyBlockItem :-<: fs, All HFunctor fs) => CxtS h fs a BlockItemL
pattern $bEmptyBlockItem' :: CxtS h fs a BlockItemL
$mEmptyBlockItem' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(EmptyBlockItem :-<: fs, All HFunctor fs) =>
CxtS h fs a BlockItemL -> (Void# -> r) -> (Void# -> r) -> r
EmptyBlockItem' <- (project -> Just EmptyBlockItem) where
  EmptyBlockItem' = CxtS h fs a BlockItemL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(EmptyBlockItem :-<: fs, InjF fs BlockItemL j) =>
CxtS h fs a j
iEmptyBlockItem