-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | Machinery that provides the ability to return values from Indigo statements
-- (like @if@, @case@, @while@, etc).
-- You are allowed to return unit, one expression or a tuple of expressions.
-- For instance:
--
-- @
-- (a, b) <- if flag
--           then do
--                  anotherFlag <- newVar True
--                  return (5 +. var, anotherFlag ||. True)
--           else return (0, anotherVar)
-- @
-- is a valid construction.
-- Pay attention to the fact that @5 +. var@ has the type 'Expr' 'Integer',
-- but 0 is just an 'Integer' and @anotherFlag ||. True@ has type 'Expr' 'Bool',
-- but @anotherVar@ has type 'Var' 'Bool'; and this code will compile anyway.
-- This is done intentionally to avoid the burden of manually converting values
-- to expressions (or variables).
-- So you can write the same constructions as in a regular language.

module Indigo.Backend.Scope
  ( BranchRetKind (..)
  , ScopeCodeGen
  , ScopeCodeGen' (..)
  , ReturnableValue
  , ReturnableValue' (..)
  , RetOutStack
  , RetVars
  , RetExprs
  , ClassifyReturnValue
  , liftClear
  , compileScope
  , allocateVars
  , finalizeStatement

  -- Builder helpers for hooks
  , prettyAssign
  , condStmtPretty
  , prettyRet
  ) where

import Data.Kind qualified as Kind
import Fmt (Buildable(..), pretty)
import GHC.TypeLits qualified as Lit

import Indigo.Backend.Expr.Compilation (compileExpr)
import Indigo.Backend.Prelude
import Indigo.Common.Expr (Expr, ExprType, ToExpr, toExpr)
import Indigo.Common.State
import Indigo.Common.Var
import Indigo.Lorentz
import Lorentz.Instr qualified as L
import Morley.Util.Type (type (++))

-- | To avoid overlapping instances we need to somehow distinguish single values
-- from tuples, because the instances:
--
-- @
--   instance Something a
--   instance Something (a, b)
-- @
-- overlap and adding @&#x7b;-\# OVERLAPPING \#-&#x7d;@ doesn't rescue in some cases,
-- especially for type families defined in @Something@.
data BranchRetKind =
    Unit
  -- ^ If value is unit (don't return anything)
  | SingleVal
  -- ^ If it's a single value (not tuple)
  | Tuple
  -- ^ If it's tuple (we don't care how many elements are in)

-- | This type family returns a promoted value of type 'BranchRetKind'
-- or causes a compilation error if a tuple with too many elements is used.
type family ClassifyReturnValue (ret :: Kind.Type) where
  ClassifyReturnValue ()     = 'Unit
  ClassifyReturnValue (_, _) = 'Tuple
  -- These type errors are an attempt to make compilation errors clear
  -- in cases where one tries to return a tuple with more elements from a statement
  ClassifyReturnValue (_, _, _) = 'Tuple
  ClassifyReturnValue (_, _, _, _) =
    Lit.TypeError ('Lit.Text "Tuple with 4 elements is not supported yet as returning value")
  ClassifyReturnValue (_, _, _, _, _) =
    Lit.TypeError ('Lit.Text "Tuple with 5 elements is not supported yet as returning value")
  ClassifyReturnValue (_, _, _, _, _, _) =
    Lit.TypeError ('Lit.Text "Tuple with 6 elements is not supported yet as returning value")
  -- I hope nobody will try to return as a value tuples with more elements
  ClassifyReturnValue _      = 'SingleVal

-- | Class for values that can be returned from Indigo statements.
-- They include @()@ and tuples.
class ReturnableValue' (retKind :: BranchRetKind) (ret :: Kind.Type) where
  -- | Type family reflecting the top elements of stack produced by
  -- a statement returning the value.
  type family RetOutStack' retKind ret :: [Kind.Type]

  -- | Type family reflecting the returning value from a statement.
  type family RetVars' retKind ret :: Kind.Type

  -- | Tuple looking like @(Expr x, Expr y, ..)@ that corresponds
  -- to expressions returning from the scope.
  -- 'RetVars\'' and 'RetExprs\'' are twin types because
  -- the former just adds 'Var' over each expression of the latter.
  type family RetExprs' retKind ret :: Kind.Type

  -- | Allocate variables referring to result of the statement.
  -- Requires an allocator operating in a Monad.
  allocateVars'
    :: Monad m
    => (forall (x :: Kind.Type) . m (Var x))
    -> m (RetVars' retKind ret)

  -- | Push the variables referring to the result of the statement on top of
  -- the stack of the given 'StackVars'.
  assignVars'
    :: RetVars' retKind ret
    -> StackVars inp
    -> StackVars (RetOutStack' retKind ret ++ inp)

  -- | Pretty printing of statements like \"var := statement\"
  prettyAssign' :: RetVars' retKind ret -> Text -> Text

  -- | Prettify 'ret' value
  prettyRet' :: ret -> Text

-- | Type class which unions all related management of computations in a scope,
-- like in @if@ branch, in @case@ body, etc.
--
-- Particularly, it takes care of the computation of expressions returning
-- from a scope to leave it safely.
-- Basically, this type class encapsulates the generation of Lorentz code that looks like:
--
-- @
--   branch_code #
--     -- we get some arbitrary type of a stack here, lets call it @xs@
--   compute_returning_expressions #
--     -- we get type of stack [e1, e2, ... ek] ++ xs
--   cleanup_xs_to_inp
--     -- we get [e1, e2, e3, ..., ek] ++ inp
-- @
class ReturnableValue' retKind ret => ScopeCodeGen' (retKind :: BranchRetKind) (ret :: Kind.Type) where
  -- | Produces an Indigo computation that puts on the stack
  -- the evaluated returned expressions from the leaving scope.
  compileScopeReturn' :: ret -> IndigoState xs (RetOutStack' retKind ret ++ xs)

  -- | Drop the stack cells that were produced in the leaving scope,
  -- apart from ones corresponding to the returning expressions.
  liftClear' :: (xs :-> inp) -> (RetOutStack' retKind ret ++ xs :-> RetOutStack' retKind ret ++ inp)

  -- | Generate 'gcClear' for the whole statement
  genGcClear' :: (RetOutStack' retKind ret ++ inp) :-> inp

type RetOutStack ret = RetOutStack' (ClassifyReturnValue ret) ret
type RetVars ret = RetVars' (ClassifyReturnValue ret) ret
type RetExprs ret = RetExprs' (ClassifyReturnValue ret) ret
type ReturnableValue ret = ReturnableValue' (ClassifyReturnValue ret) ret
type ScopeCodeGen ret = ScopeCodeGen' (ClassifyReturnValue ret) ret

-- | Specific version of 'allocateVars\''
allocateVars
  :: forall ret m . (ReturnableValue ret, Monad m)
  => (forall (x :: Kind.Type) . m (Var x))
  -> m (RetVars ret)
allocateVars :: forall ret (m :: * -> *).
(ReturnableValue ret, Monad m) =>
(forall x. m (Var x)) -> m (RetVars ret)
allocateVars = forall (retKind :: BranchRetKind) ret (m :: * -> *).
(ReturnableValue' retKind ret, Monad m) =>
(forall x. m (Var x)) -> m (RetVars' retKind ret)
allocateVars' @(ClassifyReturnValue ret) @ret

-- | Specific version of 'liftClear\''
liftClear
  :: forall ret inp xs . ScopeCodeGen ret
  => (xs :-> inp)
  -> (RetOutStack ret ++ xs :-> RetOutStack ret ++ inp)
liftClear :: forall ret (inp :: [*]) (xs :: [*]).
ScopeCodeGen ret =>
(xs :-> inp)
-> (RetOutStack ret ++ xs) :-> (RetOutStack ret ++ inp)
liftClear = forall (retKind :: BranchRetKind) ret (xs :: [*]) (inp :: [*]).
ScopeCodeGen' retKind ret =>
(xs :-> inp)
-> (RetOutStack' retKind ret ++ xs)
   :-> (RetOutStack' retKind ret ++ inp)
liftClear' @(ClassifyReturnValue ret) @ret

prettyAssign :: forall ret . ReturnableValue ret => RetVars ret -> Text -> Text
prettyAssign :: forall ret. ReturnableValue ret => RetVars ret -> Text -> Text
prettyAssign = forall (retKind :: BranchRetKind) ret.
ReturnableValue' retKind ret =>
RetVars' retKind ret -> Text -> Text
prettyAssign' @(ClassifyReturnValue ret) @ret

prettyRet :: forall ret . ReturnableValue ret => ret -> Text
prettyRet :: forall ret. ReturnableValue ret => ret -> Text
prettyRet = forall (retKind :: BranchRetKind) ret.
ReturnableValue' retKind ret =>
ret -> Text
prettyRet' @(ClassifyReturnValue ret) @ret

condStmtPretty :: forall ret x . ReturnableValue ret => RetVars ret -> Text -> Expr x -> Text
condStmtPretty :: forall ret x.
ReturnableValue ret =>
RetVars ret -> Text -> Expr x -> Text
condStmtPretty RetVars ret
retVars Text
stmtName Expr x
ex = forall ret. ReturnableValue ret => RetVars ret -> Text -> Text
prettyAssign @ret RetVars ret
retVars (Text
stmtName Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Expr x -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty Expr x
ex Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")")

-- | Concatenate a scoped code, generation of returning expressions,
-- and clean up of redundant cells from the stack.
compileScope
  :: forall ret inp xs . ScopeCodeGen ret
  => (StackVars xs -> MetaData xs)
  -- ^ Partially applied constructor of 'MetaData' (without passed 'StackVars').
  -- 'compileScope' function is usually being called from another function
  -- which is in 'IndigoState' and, consequently, holding 'MetaData' with all fields.
  -> GenCode inp xs
  -- ^ Code (and clear) of a wrapping scope
  -> ret
  -- ^ Return value of a scope (either primitives or expressions or variables)
  -> (inp :-> RetOutStack ret ++ inp)
compileScope :: forall ret (inp :: [*]) (xs :: [*]).
ScopeCodeGen ret =>
(StackVars xs -> MetaData xs)
-> GenCode inp xs -> ret -> inp :-> (RetOutStack ret ++ inp)
compileScope StackVars xs -> MetaData xs
mdCr GenCode inp xs
innerGc ret
gcRet =
  let md :: MetaData xs
md = StackVars xs -> MetaData xs
mdCr (GenCode inp xs -> StackVars xs
forall (inp :: [*]) (out :: [*]). GenCode inp out -> StackVars out
gcStack GenCode inp xs
innerGc) in
  GenCode inp xs -> inp :-> xs
forall (inp :: [*]) (out :: [*]). GenCode inp out -> inp :-> out
gcCode GenCode inp xs
innerGc (inp :-> xs)
-> (xs :-> (RetOutStack' (ClassifyReturnValue ret) ret ++ xs))
-> inp :-> (RetOutStack' (ClassifyReturnValue ret) ret ++ xs)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  MetaData xs
-> Text
-> (xs :-> (RetOutStack' (ClassifyReturnValue ret) ret ++ xs))
-> xs :-> (RetOutStack' (ClassifyReturnValue ret) ret ++ xs)
forall (inp :: [*]) (out :: [*]) (any :: [*]).
MetaData any -> Text -> (inp :-> out) -> inp :-> out
auxiliaryHook MetaData xs
md (Text
"computation of returning values: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> ret -> Text
forall ret. ReturnableValue ret => ret -> Text
prettyRet ret
gcRet)
    (GenCode xs (RetOutStack' (ClassifyReturnValue ret) ret ++ xs)
-> xs :-> (RetOutStack' (ClassifyReturnValue ret) ret ++ xs)
forall (inp :: [*]) (out :: [*]). GenCode inp out -> inp :-> out
gcCode (GenCode xs (RetOutStack' (ClassifyReturnValue ret) ret ++ xs)
 -> xs :-> (RetOutStack' (ClassifyReturnValue ret) ret ++ xs))
-> GenCode xs (RetOutStack' (ClassifyReturnValue ret) ret ++ xs)
-> xs :-> (RetOutStack' (ClassifyReturnValue ret) ret ++ xs)
forall a b. (a -> b) -> a -> b
$ MetaData xs
-> IndigoState
     xs (RetOutStack' (ClassifyReturnValue ret) ret ++ xs)
-> GenCode xs (RetOutStack' (ClassifyReturnValue ret) ret ++ xs)
forall (inp :: [*]) (out :: [*]).
MetaData inp -> IndigoState inp out -> GenCode inp out
usingIndigoState MetaData xs
md (IndigoState xs (RetOutStack' (ClassifyReturnValue ret) ret ++ xs)
 -> GenCode xs (RetOutStack' (ClassifyReturnValue ret) ret ++ xs))
-> IndigoState
     xs (RetOutStack' (ClassifyReturnValue ret) ret ++ xs)
-> GenCode xs (RetOutStack' (ClassifyReturnValue ret) ret ++ xs)
forall a b. (a -> b) -> a -> b
$ forall (retKind :: BranchRetKind) ret (xs :: [*]).
ScopeCodeGen' retKind ret =>
ret -> IndigoState xs (RetOutStack' retKind ret ++ xs)
compileScopeReturn' @(ClassifyReturnValue ret) ret
gcRet) (inp :-> (RetOutStack' (ClassifyReturnValue ret) ret ++ xs))
-> ((RetOutStack' (ClassifyReturnValue ret) ret ++ xs)
    :-> (RetOutStack' (ClassifyReturnValue ret) ret ++ inp))
-> inp :-> (RetOutStack' (ClassifyReturnValue ret) ret ++ inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  MetaData xs
-> Text
-> ((RetOutStack' (ClassifyReturnValue ret) ret ++ xs)
    :-> (RetOutStack' (ClassifyReturnValue ret) ret ++ inp))
-> (RetOutStack' (ClassifyReturnValue ret) ret ++ xs)
   :-> (RetOutStack' (ClassifyReturnValue ret) ret ++ inp)
forall (inp :: [*]) (out :: [*]) (any :: [*]).
MetaData any -> Text -> (inp :-> out) -> inp :-> out
auxiliaryHook MetaData xs
md Text
"dropping cells from the stack allocated in the scope"
    (forall (retKind :: BranchRetKind) ret (xs :: [*]) (inp :: [*]).
ScopeCodeGen' retKind ret =>
(xs :-> inp)
-> (RetOutStack' retKind ret ++ xs)
   :-> (RetOutStack' retKind ret ++ inp)
liftClear' @(ClassifyReturnValue ret) @ret (GenCode inp xs -> xs :-> inp
forall (inp :: [*]) (out :: [*]). GenCode inp out -> out :-> inp
gcClear GenCode inp xs
innerGc))

-- | Push variables in the 'StackVars', referring to the generated expressions,
-- and generate 'gcClear' for the whole statement.
finalizeStatement
  :: forall ret inp . ScopeCodeGen ret
  => StackVars inp
  -> RetVars ret
  -> (inp :-> RetOutStack ret ++ inp)
  -> GenCode inp (RetOutStack ret ++ inp)
finalizeStatement :: forall ret (inp :: [*]).
ScopeCodeGen ret =>
StackVars inp
-> RetVars ret
-> (inp :-> (RetOutStack ret ++ inp))
-> GenCode inp (RetOutStack ret ++ inp)
finalizeStatement StackVars inp
md RetVars ret
vars inp :-> (RetOutStack ret ++ inp)
code =
  let newMd :: StackVars (RetOutStack ret ++ inp)
newMd = forall (retKind :: BranchRetKind) ret (inp :: [*]).
ReturnableValue' retKind ret =>
RetVars' retKind ret
-> StackVars inp -> StackVars (RetOutStack' retKind ret ++ inp)
assignVars' @(ClassifyReturnValue ret) @ret RetVars ret
vars StackVars inp
md in
  StackVars (RetOutStack ret ++ inp)
-> (inp :-> (RetOutStack ret ++ inp))
-> ((RetOutStack ret ++ inp) :-> inp)
-> GenCode inp (RetOutStack ret ++ inp)
forall (inp :: [*]) (out :: [*]).
StackVars out -> (inp :-> out) -> (out :-> inp) -> GenCode inp out
GenCode StackVars (RetOutStack ret ++ inp)
newMd inp :-> (RetOutStack ret ++ inp)
code (forall (retKind :: BranchRetKind) ret (inp :: [*]).
ScopeCodeGen' retKind ret =>
(RetOutStack' retKind ret ++ inp) :-> inp
genGcClear' @(ClassifyReturnValue ret) @ret)

-- Type instances for ScopeCodeGen'.
-- Perhaps, they could be implemented more succinctly
-- and expressed inductively via previous instances,
-- but I don't think it makes sense to spend a lot of time to shorten them.

type KnownValueExpr a = (KnownValue (ExprType a), ToExpr a)

instance ReturnableValue' 'Unit () where
  type RetOutStack' 'Unit () = '[]
  type RetVars' 'Unit () = ()
  type RetExprs' 'Unit () = ()
  allocateVars' :: forall (m :: * -> *).
Monad m =>
(forall x. m (Var x)) -> m (RetVars' 'Unit ())
allocateVars' forall x. m (Var x)
_ = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  assignVars' :: forall (inp :: [*]).
RetVars' 'Unit ()
-> StackVars inp -> StackVars (RetOutStack' 'Unit () ++ inp)
assignVars' RetVars' 'Unit ()
_ StackVars inp
md = StackVars inp
StackVars (RetOutStack' 'Unit () ++ inp)
md
  prettyAssign' :: RetVars' 'Unit () -> Text -> Text
prettyAssign' RetVars' 'Unit ()
_ Text
stmt = Text
stmt
  prettyRet' :: () -> Text
prettyRet' ()
_ = Text
"()"

instance ScopeCodeGen' 'Unit () where
  compileScopeReturn' :: forall (xs :: [*]).
() -> IndigoState xs (RetOutStack' 'Unit () ++ xs)
compileScopeReturn' ()
_ = IndigoState xs (RetOutStack' 'Unit () ++ xs)
forall (inp :: [*]). IndigoState inp inp
nopState
  liftClear' :: forall (xs :: [*]) (inp :: [*]).
(xs :-> inp)
-> (RetOutStack' 'Unit () ++ xs) :-> (RetOutStack' 'Unit () ++ inp)
liftClear' = (xs :-> inp)
-> (RetOutStack' 'Unit () ++ xs) :-> (RetOutStack' 'Unit () ++ inp)
forall a. a -> a
id
  genGcClear' :: forall (inp :: [*]). (RetOutStack' 'Unit () ++ inp) :-> inp
genGcClear' = (RetOutStack' 'Unit () ++ inp) :-> inp
forall (s :: [*]). s :-> s
L.nop

instance KnownValueExpr single => ReturnableValue' 'SingleVal single where
  type RetOutStack' 'SingleVal single = '[ExprType single]
  type RetVars' 'SingleVal single = Var (ExprType single)
  type RetExprs' 'SingleVal single = ExprType single
  allocateVars' :: forall (m :: * -> *).
Monad m =>
(forall x. m (Var x)) -> m (RetVars' 'SingleVal single)
allocateVars' forall x. m (Var x)
allocator = forall x. m (Var x)
allocator @(ExprType single)
  assignVars' :: forall (inp :: [*]).
RetVars' 'SingleVal single
-> StackVars inp
-> StackVars (RetOutStack' 'SingleVal single ++ inp)
assignVars' = RetVars' 'SingleVal single
-> StackVars inp
-> StackVars (RetOutStack' 'SingleVal single ++ inp)
forall a (inp :: [*]).
KnownValue a =>
Var a -> StackVars inp -> StackVars (a : inp)
pushRef
  prettyAssign' :: RetVars' 'SingleVal single -> Text -> Text
prettyAssign' RetVars' 'SingleVal single
retVars Text
stmt = Var (ExprType single) -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty Var (ExprType single)
RetVars' 'SingleVal single
retVars Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" := " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
stmt
  prettyRet' :: single -> Text
prettyRet' = Expr (ExprType single) -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty (Expr (ExprType single) -> Text)
-> (single -> Expr (ExprType single)) -> single -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. single -> Expr (ExprType single)
forall a. ToExpr a => a -> Expr (ExprType a)
toExpr

instance KnownValueExpr single => ScopeCodeGen' 'SingleVal single where
  compileScopeReturn' :: forall (xs :: [*]).
single -> IndigoState xs (RetOutStack' 'SingleVal single ++ xs)
compileScopeReturn' = single -> IndigoState xs (RetOutStack' 'SingleVal single ++ xs)
forall a (inp :: [*]).
ToExpr a =>
a -> IndigoState inp (ExprType a : inp)
compileToExpr
  liftClear' :: forall (xs :: [*]) (inp :: [*]).
(xs :-> inp)
-> (RetOutStack' 'SingleVal single ++ xs)
   :-> (RetOutStack' 'SingleVal single ++ inp)
liftClear' = (xs :-> inp)
-> (RetOutStack' 'SingleVal single ++ xs)
   :-> (RetOutStack' 'SingleVal single ++ inp)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip
  genGcClear' :: forall (inp :: [*]).
(RetOutStack' 'SingleVal single ++ inp) :-> inp
genGcClear' = (RetOutStack' 'SingleVal single ++ inp) :-> inp
forall a (s :: [*]). (a : s) :-> s
L.drop

instance ( KnownValueExpr x
         , KnownValueExpr y
         , Buildable (RetVars' 'Tuple (x, y))
         )
         => ReturnableValue' 'Tuple (x, y) where
  type RetOutStack' 'Tuple (x, y) = ExprType x ': '[ExprType y]
  type RetVars' 'Tuple (x, y) = (Var (ExprType x), Var (ExprType y))
  type RetExprs' 'Tuple (x, y) = (ExprType x, ExprType y)
  allocateVars' :: forall (m :: * -> *).
Monad m =>
(forall x. m (Var x)) -> m (RetVars' 'Tuple (x, y))
allocateVars' forall x. m (Var x)
allocator = (,) (Var (ExprType x)
 -> Var (ExprType y) -> (Var (ExprType x), Var (ExprType y)))
-> m (Var (ExprType x))
-> m (Var (ExprType y) -> (Var (ExprType x), Var (ExprType y)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Var (ExprType x))
forall x. m (Var x)
allocator m (Var (ExprType y) -> (Var (ExprType x), Var (ExprType y)))
-> m (Var (ExprType y)) -> m (Var (ExprType x), Var (ExprType y))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (Var (ExprType y))
forall x. m (Var x)
allocator
  assignVars' :: forall (inp :: [*]).
RetVars' 'Tuple (x, y)
-> StackVars inp -> StackVars (RetOutStack' 'Tuple (x, y) ++ inp)
assignVars' (Var (ExprType x)
var1, Var (ExprType y)
var2) StackVars inp
md = Var (ExprType x)
-> StackVars (ExprType y : inp)
-> StackVars (ExprType x : ExprType y : inp)
forall a (inp :: [*]).
KnownValue a =>
Var a -> StackVars inp -> StackVars (a : inp)
pushRef Var (ExprType x)
var1 (StackVars (ExprType y : inp)
 -> StackVars (ExprType x : ExprType y : inp))
-> StackVars (ExprType y : inp)
-> StackVars (ExprType x : ExprType y : inp)
forall a b. (a -> b) -> a -> b
$ Var (ExprType y) -> StackVars inp -> StackVars (ExprType y : inp)
forall a (inp :: [*]).
KnownValue a =>
Var a -> StackVars inp -> StackVars (a : inp)
pushRef Var (ExprType y)
var2 StackVars inp
md
  prettyAssign' :: RetVars' 'Tuple (x, y) -> Text -> Text
prettyAssign' RetVars' 'Tuple (x, y)
retVars Text
stmt = (Var (ExprType x), Var (ExprType y)) -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty (Var (ExprType x), Var (ExprType y))
RetVars' 'Tuple (x, y)
retVars Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" := " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
stmt
  prettyRet' :: (x, y) -> Text
prettyRet' (x
x, y
y) = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Expr (ExprType x) -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty (x -> Expr (ExprType x)
forall a. ToExpr a => a -> Expr (ExprType a)
toExpr x
x) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
", " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Expr (ExprType y) -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty (y -> Expr (ExprType y)
forall a. ToExpr a => a -> Expr (ExprType a)
toExpr y
y) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

instance (KnownValueExpr x
         , KnownValueExpr y
         , Buildable (RetVars' 'Tuple (x, y))
         ) => ScopeCodeGen' 'Tuple (x, y) where
  compileScopeReturn' :: forall (xs :: [*]).
(x, y) -> IndigoState xs (RetOutStack' 'Tuple (x, y) ++ xs)
compileScopeReturn' (x
e1, y
e2) = y -> IndigoState xs (ExprType' (Decide y) y : xs)
forall a (inp :: [*]).
ToExpr a =>
a -> IndigoState inp (ExprType a : inp)
compileToExpr y
e2 IndigoState xs (ExprType' (Decide y) y : xs)
-> IndigoState
     (ExprType' (Decide y) y : xs)
     (ExprType' (Decide x) x : ExprType' (Decide y) y : xs)
-> IndigoState
     xs (ExprType' (Decide x) x : ExprType' (Decide y) y : xs)
forall (inp :: [*]) (out :: [*]) (out1 :: [*]).
IndigoState inp out -> IndigoState out out1 -> IndigoState inp out1
>> x
-> IndigoState
     (ExprType' (Decide y) y : xs)
     (ExprType' (Decide x) x : ExprType' (Decide y) y : xs)
forall a (inp :: [*]).
ToExpr a =>
a -> IndigoState inp (ExprType a : inp)
compileToExpr x
e1
  liftClear' :: forall (xs :: [*]) (inp :: [*]).
(xs :-> inp)
-> (RetOutStack' 'Tuple (x, y) ++ xs)
   :-> (RetOutStack' 'Tuple (x, y) ++ inp)
liftClear' = forall (n :: Nat) (inp :: [*]) (out :: [*]) (s :: [*]) (s' :: [*]).
ConstraintDIPNLorentz (ToPeano n) inp out s s' =>
(s :-> s') -> inp :-> out
L.dipN @2
  genGcClear' :: forall (inp :: [*]). (RetOutStack' 'Tuple (x, y) ++ inp) :-> inp
genGcClear' = (ExprType' (Decide x) x : ExprType' (Decide y) y : inp)
:-> (ExprType' (Decide y) y : inp)
forall a (s :: [*]). (a : s) :-> s
L.drop ((ExprType' (Decide x) x : ExprType' (Decide y) y : inp)
 :-> (ExprType' (Decide y) y : inp))
-> ((ExprType' (Decide y) y : inp) :-> inp)
-> (ExprType' (Decide x) x : ExprType' (Decide y) y : inp) :-> inp
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (ExprType' (Decide y) y : inp) :-> inp
forall a (s :: [*]). (a : s) :-> s
L.drop

instance ( KnownValueExpr x
         , KnownValueExpr y
         , KnownValueExpr z
         , Buildable (RetVars' 'Tuple (x, y, z))
         ) => ReturnableValue' 'Tuple (x, y, z) where
  type RetOutStack' 'Tuple (x, y, z) = ExprType x ': ExprType y ': '[ExprType z]
  type RetVars' 'Tuple (x, y, z) = (Var (ExprType x), Var (ExprType y), Var (ExprType z))
  type RetExprs' 'Tuple (x, y, z) = (ExprType x, ExprType y, ExprType z)
  allocateVars' :: forall (m :: * -> *).
Monad m =>
(forall x. m (Var x)) -> m (RetVars' 'Tuple (x, y, z))
allocateVars' forall x. m (Var x)
allocator = (,,) (Var (ExprType x)
 -> Var (ExprType y)
 -> Var (ExprType z)
 -> (Var (ExprType x), Var (ExprType y), Var (ExprType z)))
-> m (Var (ExprType x))
-> m (Var (ExprType y)
      -> Var (ExprType z)
      -> (Var (ExprType x), Var (ExprType y), Var (ExprType z)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Var (ExprType x))
forall x. m (Var x)
allocator m (Var (ExprType y)
   -> Var (ExprType z)
   -> (Var (ExprType x), Var (ExprType y), Var (ExprType z)))
-> m (Var (ExprType y))
-> m (Var (ExprType z)
      -> (Var (ExprType x), Var (ExprType y), Var (ExprType z)))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (Var (ExprType y))
forall x. m (Var x)
allocator m (Var (ExprType z)
   -> (Var (ExprType x), Var (ExprType y), Var (ExprType z)))
-> m (Var (ExprType z))
-> m (Var (ExprType x), Var (ExprType y), Var (ExprType z))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (Var (ExprType z))
forall x. m (Var x)
allocator
  assignVars' :: forall (inp :: [*]).
RetVars' 'Tuple (x, y, z)
-> StackVars inp
-> StackVars (RetOutStack' 'Tuple (x, y, z) ++ inp)
assignVars' (Var (ExprType x)
var1, Var (ExprType y)
var2, Var (ExprType z)
var3) StackVars inp
md =
    Var (ExprType x)
-> StackVars (ExprType y : ExprType z : inp)
-> StackVars (ExprType x : ExprType y : ExprType z : inp)
forall a (inp :: [*]).
KnownValue a =>
Var a -> StackVars inp -> StackVars (a : inp)
pushRef Var (ExprType x)
var1 (StackVars (ExprType y : ExprType z : inp)
 -> StackVars (ExprType x : ExprType y : ExprType z : inp))
-> (StackVars (ExprType z : inp)
    -> StackVars (ExprType y : ExprType z : inp))
-> StackVars (ExprType z : inp)
-> StackVars (ExprType x : ExprType y : ExprType z : inp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var (ExprType y)
-> StackVars (ExprType z : inp)
-> StackVars (ExprType y : ExprType z : inp)
forall a (inp :: [*]).
KnownValue a =>
Var a -> StackVars inp -> StackVars (a : inp)
pushRef Var (ExprType y)
var2 (StackVars (ExprType z : inp)
 -> StackVars (ExprType x : ExprType y : ExprType z : inp))
-> StackVars (ExprType z : inp)
-> StackVars (ExprType x : ExprType y : ExprType z : inp)
forall a b. (a -> b) -> a -> b
$ Var (ExprType z) -> StackVars inp -> StackVars (ExprType z : inp)
forall a (inp :: [*]).
KnownValue a =>
Var a -> StackVars inp -> StackVars (a : inp)
pushRef Var (ExprType z)
var3 StackVars inp
md
  prettyAssign' :: RetVars' 'Tuple (x, y, z) -> Text -> Text
prettyAssign' RetVars' 'Tuple (x, y, z)
retVars Text
stmt = (Var (ExprType x), Var (ExprType y), Var (ExprType z)) -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty (Var (ExprType x), Var (ExprType y), Var (ExprType z))
RetVars' 'Tuple (x, y, z)
retVars Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" := " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
stmt
  prettyRet' :: (x, y, z) -> Text
prettyRet' (x
x, y
y, z
z) = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Expr (ExprType x) -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty (x -> Expr (ExprType x)
forall a. ToExpr a => a -> Expr (ExprType a)
toExpr x
x) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
", " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Expr (ExprType y) -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty (y -> Expr (ExprType y)
forall a. ToExpr a => a -> Expr (ExprType a)
toExpr y
y) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
", " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Expr (ExprType z) -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty (z -> Expr (ExprType z)
forall a. ToExpr a => a -> Expr (ExprType a)
toExpr z
z) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

instance (KnownValueExpr x
         , KnownValueExpr y
         , KnownValueExpr z
         , Buildable (RetVars' 'Tuple (x, y, z))
         ) => ScopeCodeGen' 'Tuple (x, y, z) where
  compileScopeReturn' :: forall (xs :: [*]).
(x, y, z) -> IndigoState xs (RetOutStack' 'Tuple (x, y, z) ++ xs)
compileScopeReturn' (x
e1, y
e2, z
e3) = z -> IndigoState xs (ExprType' (Decide z) z : xs)
forall a (inp :: [*]).
ToExpr a =>
a -> IndigoState inp (ExprType a : inp)
compileToExpr z
e3 IndigoState xs (ExprType' (Decide z) z : xs)
-> IndigoState
     (ExprType' (Decide z) z : xs)
     (ExprType' (Decide y) y : ExprType' (Decide z) z : xs)
-> IndigoState
     xs (ExprType' (Decide y) y : ExprType' (Decide z) z : xs)
forall (inp :: [*]) (out :: [*]) (out1 :: [*]).
IndigoState inp out -> IndigoState out out1 -> IndigoState inp out1
>> y
-> IndigoState
     (ExprType' (Decide z) z : xs)
     (ExprType' (Decide y) y : ExprType' (Decide z) z : xs)
forall a (inp :: [*]).
ToExpr a =>
a -> IndigoState inp (ExprType a : inp)
compileToExpr y
e2 IndigoState
  xs (ExprType' (Decide y) y : ExprType' (Decide z) z : xs)
-> IndigoState
     (ExprType' (Decide y) y : ExprType' (Decide z) z : xs)
     (ExprType' (Decide x) x
        : ExprType' (Decide y) y : ExprType' (Decide z) z : xs)
-> IndigoState
     xs
     (ExprType' (Decide x) x
        : ExprType' (Decide y) y : ExprType' (Decide z) z : xs)
forall (inp :: [*]) (out :: [*]) (out1 :: [*]).
IndigoState inp out -> IndigoState out out1 -> IndigoState inp out1
>> x
-> IndigoState
     (ExprType' (Decide y) y : ExprType' (Decide z) z : xs)
     (ExprType' (Decide x) x
        : ExprType' (Decide y) y : ExprType' (Decide z) z : xs)
forall a (inp :: [*]).
ToExpr a =>
a -> IndigoState inp (ExprType a : inp)
compileToExpr x
e1
  liftClear' :: forall (xs :: [*]) (inp :: [*]).
(xs :-> inp)
-> (RetOutStack' 'Tuple (x, y, z) ++ xs)
   :-> (RetOutStack' 'Tuple (x, y, z) ++ inp)
liftClear' = forall (n :: Nat) (inp :: [*]) (out :: [*]) (s :: [*]) (s' :: [*]).
ConstraintDIPNLorentz (ToPeano n) inp out s s' =>
(s :-> s') -> inp :-> out
L.dipN @3
  genGcClear' :: forall (inp :: [*]). (RetOutStack' 'Tuple (x, y, z) ++ inp) :-> inp
genGcClear' = (ExprType' (Decide x) x
   : ExprType' (Decide y) y : ExprType' (Decide z) z : inp)
:-> (ExprType' (Decide y) y : ExprType' (Decide z) z : inp)
forall a (s :: [*]). (a : s) :-> s
L.drop ((ExprType' (Decide x) x
    : ExprType' (Decide y) y : ExprType' (Decide z) z : inp)
 :-> (ExprType' (Decide y) y : ExprType' (Decide z) z : inp))
-> ((ExprType' (Decide y) y : ExprType' (Decide z) z : inp)
    :-> (ExprType' (Decide z) z : inp))
-> (ExprType' (Decide x) x
      : ExprType' (Decide y) y : ExprType' (Decide z) z : inp)
   :-> (ExprType' (Decide z) z : inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (ExprType' (Decide y) y : ExprType' (Decide z) z : inp)
:-> (ExprType' (Decide z) z : inp)
forall a (s :: [*]). (a : s) :-> s
L.drop ((ExprType' (Decide x) x
    : ExprType' (Decide y) y : ExprType' (Decide z) z : inp)
 :-> (ExprType' (Decide z) z : inp))
-> ((ExprType' (Decide z) z : inp) :-> inp)
-> (ExprType' (Decide x) x
      : ExprType' (Decide y) y : ExprType' (Decide z) z : inp)
   :-> inp
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (ExprType' (Decide z) z : inp) :-> inp
forall a (s :: [*]). (a : s) :-> s
L.drop

-- | Utility function to compile from an 'IsExpr'
compileToExpr :: ToExpr a => a -> IndigoState inp ((ExprType a) : inp)
compileToExpr :: forall a (inp :: [*]).
ToExpr a =>
a -> IndigoState inp (ExprType a : inp)
compileToExpr = Expr (ExprType' (Decide a) a)
-> IndigoState inp (ExprType' (Decide a) a : inp)
forall a (inp :: [*]). Expr a -> IndigoState inp (a : inp)
compileExpr (Expr (ExprType' (Decide a) a)
 -> IndigoState inp (ExprType' (Decide a) a : inp))
-> (a -> Expr (ExprType' (Decide a) a))
-> a
-> IndigoState inp (ExprType' (Decide a) a : inp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Expr (ExprType' (Decide a) a)
forall a. ToExpr a => a -> Expr (ExprType a)
toExpr