-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

-- | This module implements the ability to put
-- Indigo computations on the stack as a lambda and execute them.
module Indigo.Backend.Lambda
  ( LambdaPure1
  , createLambdaPure1
  , CreateLambdaPure1C
  , executeLambdaPure1
  , ExecuteLambdaPure1C
  , initMetaDataPure

  , Lambda1
  , createLambda1
  , CreateLambda1C
  , executeLambda1
  , ExecuteLambda1C
  , initMetaData

  , LambdaEff1
  , createLambdaEff1
  , CreateLambdaEff1C
  , executeLambdaEff1
  , ExecuteLambdaEff1C
  , initMetaDataEff

  , Lambda1Generic
  , LambdaExecutor
  , LambdaCreator
  ) where

import Data.Constraint (Dict(..))

import Indigo.Backend.Prelude
import Indigo.Backend.Scope
import Indigo.Backend.Var
import Indigo.Internal
import Indigo.Lorentz
import qualified Lorentz.Instr as L
import Lorentz.Zip (ZipInstr, ZippedStack)
import Util.Type (type (++), KnownList, listOfTypesConcatAssociativityAxiom)

----------------------------------------------------------------------------
-- Pure lambdas
----------------------------------------------------------------------------

type LambdaPure1 arg res = Lambda1Generic '[] arg res

type CreateLambdaPure1C arg res = CreateLambda1CGeneric '[] arg res

-- | Create a lambda, that takes only one argument, from the given computation.
-- The lambda is not allowed to modify storage and emit operations.
createLambdaPure1
  :: forall res arg inp out . CreateLambdaPure1C arg res
  => LambdaCreator '[] arg res inp out
createLambdaPure1 :: LambdaCreator '[] arg res inp out
createLambdaPure1 = (Var arg, MetaData (arg & '[]))
-> LambdaCreator '[] arg res inp out
forall arg res (extra :: [*]) (inp :: [*]) (out :: [*]).
CreateLambda1CGeneric extra arg res =>
(Var arg, MetaData (arg & extra))
-> (Var arg -> IndigoState (arg & extra) out res)
-> IndigoState
     inp
     (Lambda1Generic extra arg res & inp)
     (Var (Lambda1Generic extra arg res))
createLambda1Generic (Var arg, MetaData (arg & '[]))
forall arg. KnownValue arg => (Var arg, MetaData '[arg])
initMetaDataPure

type ExecuteLambdaPure1C arg res = ExecuteLambda1CGeneric '[] arg res

-- | Execute a lambda, which accepts only one argument, on passed expression.
executeLambdaPure1
  :: forall res arg inp . ExecuteLambdaPure1C arg res
  => LambdaExecutor '[] arg res inp
executeLambdaPure1 :: LambdaExecutor '[] arg res inp
executeLambdaPure1 = IndigoState inp ('[] ++ inp) () -> LambdaExecutor '[] arg res inp
forall res arg (extra :: [*]) (inp :: [*]).
ExecuteLambda1CGeneric extra arg res =>
IndigoState inp (extra ++ inp) ()
-> Var (Lambda1Generic extra arg res)
-> Expr arg
-> IndigoState inp (RetOutStack res ++ inp) (RetVars res)
executeLambda1Generic @res (() -> IndigoState inp inp ()
forall a (inp :: [*]). a -> IndigoState inp inp a
return ())

initMetaDataPure :: KnownValue arg => (Var arg, MetaData '[arg])
initMetaDataPure :: (Var arg, MetaData '[arg])
initMetaDataPure = let v :: IndigoObjectF f arg
v = RefId -> IndigoObjectF f arg
forall a (f :: Symbol -> *).
KnownValue a =>
RefId -> IndigoObjectF f a
Cell 0 in (Var arg
forall (f :: Symbol -> *). IndigoObjectF f arg
v, StackVars '[arg] -> RefId -> MetaData '[arg]
forall (stk :: [*]). StackVars stk -> RefId -> MetaData stk
MetaData (RefId -> StkEl arg
forall a. KnownValue a => RefId -> StkEl a
Ref 0 StkEl arg -> Rec StkEl '[] -> StackVars '[arg]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl '[]
forall u (a :: u -> *). Rec a '[]
RNil) 1)

----------------------------------------------------------------------------
-- Impure lambda (modifying storage only)
----------------------------------------------------------------------------

type Lambda1 st arg res = Lambda1Generic '[st] arg res

type CreateLambda1C st arg res = (KnownValue st, CreateLambda1CGeneric '[st] arg res)

-- | Create a lambda, that takes only one argument, from the given computation.
-- The lambda is not allowed to emit operations.
createLambda1
  :: forall st res arg inp out . CreateLambda1C st arg res
  => LambdaCreator '[st] arg res inp out
createLambda1 :: LambdaCreator '[st] arg res inp out
createLambda1 = (Var arg, MetaData (arg & '[st]))
-> LambdaCreator '[st] arg res inp out
forall arg res (extra :: [*]) (inp :: [*]) (out :: [*]).
CreateLambda1CGeneric extra arg res =>
(Var arg, MetaData (arg & extra))
-> (Var arg -> IndigoState (arg & extra) out res)
-> IndigoState
     inp
     (Lambda1Generic extra arg res & inp)
     (Var (Lambda1Generic extra arg res))
createLambda1Generic (Var arg, MetaData (arg & '[st]))
forall arg st.
(KnownValue arg, KnownValue st) =>
(Var arg, MetaData '[arg, st])
initMetaData

type ExecuteLambda1C st arg res =
  ( IsObject st
  , HasStorage st
  , ExecuteLambda1CGeneric '[st] arg res
  )

-- | Execute a lambda that accepts only one argument on the given expression.
executeLambda1
  :: forall st res arg inp . ExecuteLambda1C st arg res
  => LambdaExecutor '[st] arg res inp
executeLambda1 :: LambdaExecutor '[st] arg res inp
executeLambda1 =
  IndigoState inp ('[st] ++ inp) ()
-> LambdaExecutor '[st] arg res inp
forall res arg (extra :: [*]) (inp :: [*]).
ExecuteLambda1CGeneric extra arg res =>
IndigoState inp (extra ++ inp) ()
-> Var (Lambda1Generic extra arg res)
-> Expr arg
-> IndigoState inp (RetOutStack res ++ inp) (RetVars res)
executeLambda1Generic @res
    -- TODO this @compileExpr (V (storageVar @st))@ call materialises the whole decomposed storage.
    -- This is pretty expensive operation and it has to be fixed:
    -- we have to materialise only fields used in the lambda
    ((MetaData inp -> GenCode inp (st & inp) ())
-> IndigoState inp ('[st] ++ inp) ()
forall (inp :: [*]) (out :: [*]) a.
(MetaData inp -> GenCode inp out a) -> IndigoState inp out a
IndigoState ((MetaData inp -> GenCode inp (st & inp) ())
 -> IndigoState inp ('[st] ++ inp) ())
-> (MetaData inp -> GenCode inp (st & inp) ())
-> IndigoState inp ('[st] ++ inp) ()
forall a b. (a -> b) -> a -> b
$ \md :: MetaData inp
md ->
      let GenCode _ newMd :: MetaData (st & inp)
newMd alloc :: inp :-> (st & inp)
alloc _ = MetaData inp
-> IndigoState inp (st & inp) () -> GenCode inp (st & inp) ()
forall (inp :: [*]) (out :: [*]) a.
MetaData inp -> IndigoState inp out a -> GenCode inp out a
usingIndigoState MetaData inp
md (IndigoState inp (st & inp) () -> GenCode inp (st & inp) ())
-> IndigoState inp (st & inp) () -> GenCode inp (st & inp) ()
forall a b. (a -> b) -> a -> b
$ Expr st -> IndigoState inp (st & inp) ()
forall a (inp :: [*]). Expr a -> IndigoState inp (a & inp) ()
compileExpr (Var st -> Expr st
forall a. KnownValue a => Var a -> Expr a
V (HasStorage st => Var st
forall st. HasStorage st => Var st
storageVar @st)) in
      let GenCode _ _ cleanup :: (st & inp) :-> (st & inp)
cleanup _   = MetaData (st & inp)
-> IndigoState (st & inp) (st & inp) ()
-> GenCode (st & inp) (st & inp) ()
forall (inp :: [*]) (out :: [*]) a.
MetaData inp -> IndigoState inp out a -> GenCode inp out a
usingIndigoState MetaData (st & inp)
newMd (IndigoState (st & inp) (st & inp) (Var st)
forall x (inp :: [*]).
KnownValue x =>
IndigoState (x & inp) (x & inp) (Var x)
makeTopVar IndigoState (st & inp) (st & inp) (Var st)
-> (Var st -> IndigoState (st & inp) (st & inp) ())
-> IndigoState (st & inp) (st & inp) ()
forall (inp :: [*]) (out :: [*]) (out1 :: [*]) a b.
IndigoState inp out a
-> (a -> IndigoState out out1 b) -> IndigoState inp out1 b
>>= (Var st -> Expr st -> IndigoState (st & inp) (st & inp) ()
forall a (inp :: [*]). Var a -> Expr a -> IndigoState inp inp ()
setVar (HasStorage st => Var st
forall st. HasStorage st => Var st
storageVar @st) (Expr st -> IndigoState (st & inp) (st & inp) ())
-> (Var st -> Expr st)
-> Var st
-> IndigoState (st & inp) (st & inp) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var st -> Expr st
forall a. KnownValue a => Var a -> Expr a
V)) in
      ()
-> MetaData (st & inp)
-> (inp :-> (st & inp))
-> ((st & inp) :-> inp)
-> GenCode inp (st & inp) ()
forall (inp :: [*]) (out :: [*]) a.
a
-> MetaData out
-> (inp :-> out)
-> (out :-> inp)
-> GenCode inp out a
GenCode () MetaData (st & inp)
newMd inp :-> (st & inp)
alloc ((st & inp) :-> (st & inp)
cleanup ((st & inp) :-> (st & inp))
-> ((st & inp) :-> inp) -> (st & inp) :-> inp
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (st & inp) :-> inp
forall a (s :: [*]). (a & s) :-> s
L.drop)
    )

initMetaData :: (KnownValue arg, KnownValue st) => (Var arg, MetaData '[arg, st])
initMetaData :: (Var arg, MetaData '[arg, st])
initMetaData =
  -- This numeration is intentional.
  -- We have to provide HasStorage for a lambda.
  -- To avoid excessive 'given' calls with new indexes,
  -- we just refer to storage variable with the same index.
  let argm :: IndigoObjectF f arg
argm = RefId -> IndigoObjectF f arg
forall a (f :: Symbol -> *).
KnownValue a =>
RefId -> IndigoObjectF f a
Cell 2 in
  (Var arg
forall (f :: Symbol -> *). IndigoObjectF f arg
argm, StackVars '[arg, st] -> RefId -> MetaData '[arg, st]
forall (stk :: [*]). StackVars stk -> RefId -> MetaData stk
MetaData (RefId -> StkEl arg
forall a. KnownValue a => RefId -> StkEl a
Ref 2 StkEl arg -> Rec StkEl '[st] -> StackVars '[arg, st]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& RefId -> StkEl st
forall a. KnownValue a => RefId -> StkEl a
Ref 1 StkEl st -> Rec StkEl '[] -> Rec StkEl '[st]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl '[]
forall u (a :: u -> *). Rec a '[]
RNil) 3)

----------------------------------------------------------------------------
-- Lambda with side effects (might emit operations)
----------------------------------------------------------------------------

type LambdaEff1 st arg res = Lambda1Generic '[st, Ops] arg res

type CreateLambdaEff1C st arg res = (KnownValue st, CreateLambda1CGeneric '[st, Ops] arg res)

-- | Create a lambda, that takes only one argument, from the given computation,
-- and return a variable referring to this lambda.
-- The lambda is allowed to modify storage and emit operations.
createLambdaEff1
  :: forall st res arg inp out . CreateLambdaEff1C st arg res
  => LambdaCreator '[st, Ops] arg res inp out
createLambdaEff1 :: LambdaCreator '[st, Ops] arg res inp out
createLambdaEff1 = (Var arg, MetaData (arg & '[st, Ops]))
-> LambdaCreator '[st, Ops] arg res inp out
forall arg res (extra :: [*]) (inp :: [*]) (out :: [*]).
CreateLambda1CGeneric extra arg res =>
(Var arg, MetaData (arg & extra))
-> (Var arg -> IndigoState (arg & extra) out res)
-> IndigoState
     inp
     (Lambda1Generic extra arg res & inp)
     (Var (Lambda1Generic extra arg res))
createLambda1Generic (Var arg, MetaData (arg & '[st, Ops]))
forall arg st.
(KnownValue arg, KnownValue st) =>
(Var arg, MetaData '[arg, st, Ops])
initMetaDataEff

type ExecuteLambdaEff1C st arg res =
  ( HasStorage st
  , HasSideEffects
  , IsObject st
  , ExecuteLambda1CGeneric '[st, Ops] arg res
  )

-- | Execute a lambda that accepts only one argument on the given expression.
-- Also updates the storage and operations with the values returned from the lambda.
executeLambdaEff1
  :: forall st res arg inp . ExecuteLambdaEff1C st arg res
  => LambdaExecutor '[st, Ops] arg res inp
executeLambdaEff1 :: LambdaExecutor '[st, Ops] arg res inp
executeLambdaEff1 =
  IndigoState inp ('[st, Ops] ++ inp) ()
-> LambdaExecutor '[st, Ops] arg res inp
forall res arg (extra :: [*]) (inp :: [*]).
ExecuteLambda1CGeneric extra arg res =>
IndigoState inp (extra ++ inp) ()
-> Var (Lambda1Generic extra arg res)
-> Expr arg
-> IndigoState inp (RetOutStack res ++ inp) (RetVars res)
executeLambda1Generic @res
    -- TODO this @compileExpr (V (storageVar @st))@ call materialises the whole decomposed storage.
    -- This is pretty expensive operation and it has to be fixed:
    -- we have to materialise only fields used in the lambda
    ((MetaData inp -> GenCode inp (st & (Ops & inp)) ())
-> IndigoState inp ('[st, Ops] ++ inp) ()
forall (inp :: [*]) (out :: [*]) a.
(MetaData inp -> GenCode inp out a) -> IndigoState inp out a
IndigoState ((MetaData inp -> GenCode inp (st & (Ops & inp)) ())
 -> IndigoState inp ('[st, Ops] ++ inp) ())
-> (MetaData inp -> GenCode inp (st & (Ops & inp)) ())
-> IndigoState inp ('[st, Ops] ++ inp) ()
forall a b. (a -> b) -> a -> b
$ \md :: MetaData inp
md ->
      let GenCode _ newMd :: MetaData (st & (Ops & inp))
newMd alloc :: inp :-> (st & (Ops & inp))
alloc _ =
              MetaData inp
-> IndigoState inp (st & (Ops & inp)) ()
-> GenCode inp (st & (Ops & inp)) ()
forall (inp :: [*]) (out :: [*]) a.
MetaData inp -> IndigoState inp out a -> GenCode inp out a
usingIndigoState MetaData inp
md (do
                  Expr Ops -> IndigoState inp (Ops & inp) ()
forall a (inp :: [*]). Expr a -> IndigoState inp (a & inp) ()
compileExpr (Var Ops -> Expr Ops
forall a. KnownValue a => Var a -> Expr a
V Var Ops
HasSideEffects => Var Ops
operationsVar)
                  Expr st -> IndigoState (Ops & inp) (st & (Ops & inp)) ()
forall a (inp :: [*]). Expr a -> IndigoState inp (a & inp) ()
compileExpr (Var st -> Expr st
forall a. KnownValue a => Var a -> Expr a
V (HasStorage st => Var st
forall st. HasStorage st => Var st
storageVar @st))) in
      let (newStoreVar :: Var st
newStoreVar, newMdStore :: MetaData (st & (Ops & inp))
newMdStore) = MetaData (Ops & inp) -> (Var st, MetaData (st & (Ops & inp)))
forall x (stk :: [*]).
KnownValue x =>
MetaData stk -> (Var x, MetaData (x & stk))
pushRefMd (MetaData inp -> MetaData (Ops & inp)
forall a (inp :: [*]).
KnownValue a =>
MetaData inp -> MetaData (a & inp)
pushNoRefMd MetaData inp
md) in
      let (newOpsVar :: Var Ops
newOpsVar, newMdOps :: MetaData (Ops & inp)
newMdOps) = MetaData inp -> (Var Ops, MetaData (Ops & inp))
forall x (stk :: [*]).
KnownValue x =>
MetaData stk -> (Var x, MetaData (x & stk))
pushRefMd MetaData inp
md in
      let cleanup :: (st & (Ops & inp)) :-> inp
cleanup =
            GenCode (st & (Ops & inp)) (st & (Ops & inp)) ()
-> (st & (Ops & inp)) :-> (st & (Ops & inp))
forall (inp :: [*]) (out :: [*]) a.
GenCode inp out a -> inp :-> out
gcCode (MetaData (st & (Ops & inp))
-> IndigoState (st & (Ops & inp)) (st & (Ops & inp)) ()
-> GenCode (st & (Ops & inp)) (st & (Ops & inp)) ()
forall (inp :: [*]) (out :: [*]) a.
MetaData inp -> IndigoState inp out a -> GenCode inp out a
usingIndigoState MetaData (st & (Ops & inp))
newMdStore (IndigoState (st & (Ops & inp)) (st & (Ops & inp)) ()
 -> GenCode (st & (Ops & inp)) (st & (Ops & inp)) ())
-> IndigoState (st & (Ops & inp)) (st & (Ops & inp)) ()
-> GenCode (st & (Ops & inp)) (st & (Ops & inp)) ()
forall a b. (a -> b) -> a -> b
$ Var st
-> Expr st -> IndigoState (st & (Ops & inp)) (st & (Ops & inp)) ()
forall a (inp :: [*]). Var a -> Expr a -> IndigoState inp inp ()
setVar (HasStorage st => Var st
forall st. HasStorage st => Var st
storageVar @st) (Var st -> Expr st
forall a. KnownValue a => Var a -> Expr a
V Var st
newStoreVar)) ((st & (Ops & inp)) :-> (st & (Ops & inp)))
-> ((st & (Ops & inp)) :-> (Ops & inp))
-> (st & (Ops & inp)) :-> (Ops & inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
            (st & (Ops & inp)) :-> (Ops & inp)
forall a (s :: [*]). (a & s) :-> s
L.drop ((st & (Ops & inp)) :-> (Ops & inp))
-> ((Ops & inp) :-> (Ops & inp))
-> (st & (Ops & inp)) :-> (Ops & inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
            GenCode (Ops & inp) (Ops & inp) () -> (Ops & inp) :-> (Ops & inp)
forall (inp :: [*]) (out :: [*]) a.
GenCode inp out a -> inp :-> out
gcCode (MetaData (Ops & inp)
-> IndigoState (Ops & inp) (Ops & inp) ()
-> GenCode (Ops & inp) (Ops & inp) ()
forall (inp :: [*]) (out :: [*]) a.
MetaData inp -> IndigoState inp out a -> GenCode inp out a
usingIndigoState MetaData (Ops & inp)
newMdOps (IndigoState (Ops & inp) (Ops & inp) ()
 -> GenCode (Ops & inp) (Ops & inp) ())
-> IndigoState (Ops & inp) (Ops & inp) ()
-> GenCode (Ops & inp) (Ops & inp) ()
forall a b. (a -> b) -> a -> b
$ Var Ops -> Expr Ops -> IndigoState (Ops & inp) (Ops & inp) ()
forall a (inp :: [*]). Var a -> Expr a -> IndigoState inp inp ()
setVar Var Ops
HasSideEffects => Var Ops
operationsVar (Var Ops -> Expr Ops
forall a. KnownValue a => Var a -> Expr a
V Var Ops
newOpsVar)) ((st & (Ops & inp)) :-> (Ops & inp))
-> ((Ops & inp) :-> inp) -> (st & (Ops & inp)) :-> inp
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
            (Ops & inp) :-> inp
forall a (s :: [*]). (a & s) :-> s
L.drop
      in ()
-> MetaData (st & (Ops & inp))
-> (inp :-> (st & (Ops & inp)))
-> ((st & (Ops & inp)) :-> inp)
-> GenCode inp (st & (Ops & inp)) ()
forall (inp :: [*]) (out :: [*]) a.
a
-> MetaData out
-> (inp :-> out)
-> (out :-> inp)
-> GenCode inp out a
GenCode () MetaData (st & (Ops & inp))
newMd inp :-> (st & (Ops & inp))
alloc (st & (Ops & inp)) :-> inp
cleanup
    )

initMetaDataEff :: (KnownValue arg, KnownValue st) => (Var arg, MetaData '[arg, st, Ops])
initMetaDataEff :: (Var arg, MetaData '[arg, st, Ops])
initMetaDataEff =
  let argm :: IndigoObjectF f arg
argm = RefId -> IndigoObjectF f arg
forall a (f :: Symbol -> *).
KnownValue a =>
RefId -> IndigoObjectF f a
Cell 2 in
  (Var arg
forall (f :: Symbol -> *). IndigoObjectF f arg
argm, StackVars '[arg, st, Ops] -> RefId -> MetaData '[arg, st, Ops]
forall (stk :: [*]). StackVars stk -> RefId -> MetaData stk
MetaData (RefId -> StkEl arg
forall a. KnownValue a => RefId -> StkEl a
Ref 2 StkEl arg -> Rec StkEl '[st, Ops] -> StackVars '[arg, st, Ops]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& RefId -> StkEl st
forall a. KnownValue a => RefId -> StkEl a
Ref 1 StkEl st -> Rec StkEl '[Ops] -> Rec StkEl '[st, Ops]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& RefId -> StkEl Ops
forall a. KnownValue a => RefId -> StkEl a
Ref 0 StkEl Ops -> Rec StkEl '[] -> Rec StkEl '[Ops]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl '[]
forall u (a :: u -> *). Rec a '[]
RNil) 3)

----------------------------------------------------------------------------
-- Common lambda functionality
----------------------------------------------------------------------------

type Lambda1Generic extra arg res = (arg & extra) :-> (RetOutStack res ++ extra)

type CreateLambda1CGeneric extra arg res =
  ( ScopeCodeGen res, KnownValue arg, Typeable extra
  , ZipInstr (arg & extra)
  , KnownValue (ZippedStack (arg ': extra))
  , KnownValue (ZippedStack (RetOutStack res ++ extra))
  , ZipInstr (RetOutStack res ++ extra)
  , Typeable (RetOutStack res ++ extra)
  )

type LambdaCreator extra arg res inp out
  = (Var arg -> IndigoState (arg & extra) out res)
  -> IndigoState inp (Lambda1Generic extra arg res & inp) (Var (Lambda1Generic extra arg res))

-- | Create a lambda, that takes only one argument, from the given computation,
-- and return a variable referring to this lambda.
createLambda1Generic
  :: forall arg res extra inp out . CreateLambda1CGeneric extra arg res
  => (Var arg, MetaData (arg & extra))
  -> (Var arg -> IndigoState (arg & extra) out res)
  -> IndigoState inp (Lambda1Generic extra arg res & inp) (Var (Lambda1Generic extra arg res))
createLambda1Generic :: (Var arg, MetaData (arg & extra))
-> (Var arg -> IndigoState (arg & extra) out res)
-> IndigoState
     inp
     (Lambda1Generic extra arg res & inp)
     (Var (Lambda1Generic extra arg res))
createLambda1Generic (varArg :: Var arg
varArg, initMd :: MetaData (arg & extra)
initMd) act :: Var arg -> IndigoState (arg & extra) out res
act = (MetaData inp
 -> GenCode
      inp
      (Lambda1Generic extra arg res & inp)
      (Var (Lambda1Generic extra arg res)))
-> IndigoState
     inp
     (Lambda1Generic extra arg res & inp)
     (Var (Lambda1Generic extra arg res))
forall (inp :: [*]) (out :: [*]) a.
(MetaData inp -> GenCode inp out a) -> IndigoState inp out a
IndigoState ((MetaData inp
  -> GenCode
       inp
       (Lambda1Generic extra arg res & inp)
       (Var (Lambda1Generic extra arg res)))
 -> IndigoState
      inp
      (Lambda1Generic extra arg res & inp)
      (Var (Lambda1Generic extra arg res)))
-> (MetaData inp
    -> GenCode
         inp
         (Lambda1Generic extra arg res & inp)
         (Var (Lambda1Generic extra arg res)))
-> IndigoState
     inp
     (Lambda1Generic extra arg res & inp)
     (Var (Lambda1Generic extra arg res))
forall a b. (a -> b) -> a -> b
$ \md :: MetaData inp
md ->
  let gc :: GenCode (arg & extra) out res
gc = IndigoState (arg & extra) out res
-> MetaData (arg & extra) -> GenCode (arg & extra) out res
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState (Var arg -> IndigoState (arg & extra) out res
act Var arg
varArg) MetaData (arg & extra)
initMd in
  let (var :: Var (Lambda1Generic extra arg res)
var, md1 :: MetaData (Lambda1Generic extra arg res & inp)
md1) = MetaData inp
-> (Var (Lambda1Generic extra arg res),
    MetaData (Lambda1Generic extra arg res & inp))
forall x (stk :: [*]).
KnownValue x =>
MetaData stk -> (Var x, MetaData (x & stk))
pushRefMd MetaData inp
md in
  Var (Lambda1Generic extra arg res)
-> MetaData (Lambda1Generic extra arg res & inp)
-> (inp :-> (Lambda1Generic extra arg res & inp))
-> ((Lambda1Generic extra arg res & inp) :-> inp)
-> GenCode
     inp
     (Lambda1Generic extra arg res & inp)
     (Var (Lambda1Generic extra arg res))
forall (inp :: [*]) (out :: [*]) a.
a
-> MetaData out
-> (inp :-> out)
-> (out :-> inp)
-> GenCode inp out a
GenCode Var (Lambda1Generic extra arg res)
var MetaData (Lambda1Generic extra arg res & inp)
md1 (Lambda1Generic extra arg res
-> inp :-> (Lambda1Generic extra arg res & inp)
forall (i :: [*]) (o :: [*]) (s :: [*]).
ZipInstrs '[i, o] =>
(i :-> o) -> s :-> ((i :-> o) & s)
L.lambda (GenCode (arg & extra) out res
-> (arg & extra)
   :-> (RetOutStack' (ClassifyReturnValue res) res ++ (arg & extra))
forall ret (inp :: [*]) (xs :: [*]).
ScopeCodeGen ret =>
GenCode inp xs ret -> inp :-> (RetOutStack ret ++ inp)
compileScope GenCode (arg & extra) out res
gc ((arg & extra)
 :-> (RetOutStack' (ClassifyReturnValue res) res ++ (arg & extra)))
-> ((RetOutStack' (ClassifyReturnValue res) res ++ (arg & extra))
    :-> (RetOutStack' (ClassifyReturnValue res) res ++ extra))
-> Lambda1Generic extra arg res
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((arg & extra) :-> extra)
-> (RetOutStack' (ClassifyReturnValue res) res ++ (arg & extra))
   :-> (RetOutStack' (ClassifyReturnValue res) res ++ extra)
forall ret (inp :: [*]) (xs :: [*]).
ScopeCodeGen ret =>
(xs :-> inp)
-> (RetOutStack ret ++ xs) :-> (RetOutStack ret ++ inp)
liftClear @res @extra @(arg & extra) (arg & extra) :-> extra
forall a (s :: [*]). (a & s) :-> s
L.drop)) (Lambda1Generic extra arg res & inp) :-> inp
forall a (s :: [*]). (a & s) :-> s
L.drop


type ExecuteLambda1CGeneric extra arg res =
  ( ScopeCodeGen res, KnownValue arg
  , KnownValue ((arg & extra) :-> (RetOutStack res ++ extra))
  , KnownList extra
  , ZipInstr (arg & extra)
  , KnownList (RetOutStack res ++ extra)
  , ZipInstr (RetOutStack res ++ extra)
  , Typeable (RetOutStack res ++ extra)
  , KnownValue (ZippedStack (RetOutStack res ++ extra))
  )

type LambdaExecutor extra arg res inp
  = Var (Lambda1Generic extra arg res)
  -> Expr arg
  -> IndigoState inp (RetOutStack res ++ inp) (RetVars res)

-- | Execute a lambda that accepts only one argument on the given expression.
-- Also updates the storage and operations with the values returned from the lambda.
executeLambda1Generic
  :: forall res arg extra inp . ExecuteLambda1CGeneric extra arg res
  => IndigoState inp (extra ++ inp) ()
  -> Var (Lambda1Generic extra arg res)
  -> Expr arg
  -> IndigoState inp (RetOutStack res ++ inp) (RetVars res)
executeLambda1Generic :: IndigoState inp (extra ++ inp) ()
-> Var (Lambda1Generic extra arg res)
-> Expr arg
-> IndigoState inp (RetOutStack res ++ inp) (RetVars res)
executeLambda1Generic allocateCleanup :: IndigoState inp (extra ++ inp) ()
allocateCleanup varF :: Var (Lambda1Generic extra arg res)
varF argm :: Expr arg
argm = (MetaData inp
 -> GenCode inp (RetOutStack res ++ inp) (RetVars res))
-> IndigoState inp (RetOutStack res ++ inp) (RetVars res)
forall (inp :: [*]) (out :: [*]) a.
(MetaData inp -> GenCode inp out a) -> IndigoState inp out a
IndigoState ((MetaData inp
  -> GenCode inp (RetOutStack res ++ inp) (RetVars res))
 -> IndigoState inp (RetOutStack res ++ inp) (RetVars res))
-> (MetaData inp
    -> GenCode inp (RetOutStack res ++ inp) (RetVars res))
-> IndigoState inp (RetOutStack res ++ inp) (RetVars res)
forall a b. (a -> b) -> a -> b
$ \md :: MetaData inp
md ->
  let GenCode _ allocMd :: MetaData (extra ++ inp)
allocMd allocate :: inp :-> (extra ++ inp)
allocate cleanup :: (extra ++ inp) :-> inp
cleanup = IndigoState inp (extra ++ inp) ()
-> MetaData inp -> GenCode inp (extra ++ inp) ()
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState IndigoState inp (extra ++ inp) ()
allocateCleanup MetaData inp
md in
  let getArgs :: inp :-> (Lambda1Generic extra arg res & (arg & (extra ++ inp)))
getArgs =
        inp :-> (extra ++ inp)
allocate (inp :-> (extra ++ inp))
-> ((extra ++ inp)
    :-> (Lambda1Generic extra arg res & (arg & (extra ++ inp))))
-> inp :-> (Lambda1Generic extra arg res & (arg & (extra ++ inp)))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
        (GenCode
  (extra ++ inp)
  (Lambda1Generic extra arg res & (arg & (extra ++ inp)))
  ()
-> (extra ++ inp)
   :-> (Lambda1Generic extra arg res & (arg & (extra ++ inp)))
forall (inp :: [*]) (out :: [*]) a.
GenCode inp out a -> inp :-> out
gcCode (GenCode
   (extra ++ inp)
   (Lambda1Generic extra arg res & (arg & (extra ++ inp)))
   ()
 -> (extra ++ inp)
    :-> (Lambda1Generic extra arg res & (arg & (extra ++ inp))))
-> GenCode
     (extra ++ inp)
     (Lambda1Generic extra arg res & (arg & (extra ++ inp)))
     ()
-> (extra ++ inp)
   :-> (Lambda1Generic extra arg res & (arg & (extra ++ inp)))
forall a b. (a -> b) -> a -> b
$
          MetaData (extra ++ inp)
-> IndigoState
     (extra ++ inp)
     (Lambda1Generic extra arg res & (arg & (extra ++ inp)))
     ()
-> GenCode
     (extra ++ inp)
     (Lambda1Generic extra arg res & (arg & (extra ++ inp)))
     ()
forall (inp :: [*]) (out :: [*]) a.
MetaData inp -> IndigoState inp out a -> GenCode inp out a
usingIndigoState MetaData (extra ++ inp)
allocMd (IndigoState
   (extra ++ inp)
   (Lambda1Generic extra arg res & (arg & (extra ++ inp)))
   ()
 -> GenCode
      (extra ++ inp)
      (Lambda1Generic extra arg res & (arg & (extra ++ inp)))
      ())
-> IndigoState
     (extra ++ inp)
     (Lambda1Generic extra arg res & (arg & (extra ++ inp)))
     ()
-> GenCode
     (extra ++ inp)
     (Lambda1Generic extra arg res & (arg & (extra ++ inp)))
     ()
forall a b. (a -> b) -> a -> b
$ do
              Expr arg -> IndigoState (extra ++ inp) (arg & (extra ++ inp)) ()
forall a (inp :: [*]). Expr a -> IndigoState inp (a & inp) ()
compileExpr Expr arg
argm
              Expr (Lambda1Generic extra arg res)
-> IndigoState
     (arg & (extra ++ inp))
     (Lambda1Generic extra arg res & (arg & (extra ++ inp)))
     ()
forall a (inp :: [*]). Expr a -> IndigoState inp (a & inp) ()
compileExpr (Var (Lambda1Generic extra arg res)
-> Expr (Lambda1Generic extra arg res)
forall a. KnownValue a => Var a -> Expr a
V Var (Lambda1Generic extra arg res)
varF)) in
  case Dict (ConcatListOfTypesAssociativity (RetOutStack res) extra inp)
forall k (a :: [k]) (b :: [k]) (c :: [k]).
Dict (ConcatListOfTypesAssociativity a b c)
listOfTypesConcatAssociativityAxiom @(RetOutStack res) @extra @inp of
    Dict ->
      let code :: inp :-> (RetOutStack res ++ inp)
code = inp :-> (Lambda1Generic extra arg res & (arg & (extra ++ inp)))
getArgs (inp :-> (Lambda1Generic extra arg res & (arg & (extra ++ inp))))
-> ((Lambda1Generic extra arg res & (arg & (extra ++ inp)))
    :-> (RetOutStack res ++ (extra ++ inp)))
-> inp :-> (RetOutStack res ++ (extra ++ inp))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
                 Each
  '[KnownList, ZipInstr] '[arg & extra, RetOutStack res ++ extra] =>
(Lambda1Generic extra arg res : ((arg & extra) ++ inp))
:-> ((RetOutStack res ++ extra) ++ inp)
forall (i :: [*]) (o :: [*]) (s :: [*]).
Each '[KnownList, ZipInstr] '[i, o] =>
((i :-> o) : (i ++ s)) :-> (o ++ s)
L.execute @_ @_ @inp (inp :-> (RetOutStack res ++ (extra ++ inp)))
-> ((RetOutStack res ++ (extra ++ inp))
    :-> (RetOutStack res ++ inp))
-> inp :-> (RetOutStack res ++ inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
                 ((extra ++ inp) :-> inp)
-> (RetOutStack res ++ (extra ++ inp)) :-> (RetOutStack res ++ inp)
forall ret (inp :: [*]) (xs :: [*]).
ScopeCodeGen ret =>
(xs :-> inp)
-> (RetOutStack ret ++ xs) :-> (RetOutStack ret ++ inp)
liftClear @res (extra ++ inp) :-> inp
cleanup
      in MetaData inp
-> (inp :-> (RetOutStack res ++ inp))
-> GenCode inp (RetOutStack res ++ inp) (RetVars res)
forall ret (inp :: [*]).
ScopeCodeGen ret =>
MetaData inp
-> (inp :-> (RetOutStack ret ++ inp))
-> GenCode inp (RetOutStack ret ++ inp) (RetVars ret)
finalizeStatement @res MetaData inp
md inp :-> (RetOutStack res ++ inp)
code