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

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

-- | Conditional statements of Indigo language.

module Indigo.Backend.Conditional
  ( if_
  , ifSome
  , ifRight
  , ifCons
  , IfConstraint
  ) where

import qualified Data.Kind as Kind
import qualified GHC.TypeLits as Lit
import Util.Type (type (++))

import Indigo.Backend.Prelude
import Indigo.Backend.Scope
import Indigo.Internal
import Indigo.Lorentz
import qualified Lorentz.Instr as L
import qualified Lorentz.Macro as L

type family CompareBranchesResults (a :: Kind.Type) (b :: Kind.Type) :: Constraint where
  CompareBranchesResults x x = ()
  CompareBranchesResults x y = Lit.TypeError
      ('Lit.Text " Result types of if branches diverged: "
       'Lit.:<>: 'Lit.ShowType x 'Lit.:<>: ('Lit.Text " against ") 'Lit.:<>: 'Lit.ShowType y
      )

type IfConstraint a b =
  ( ScopeCodeGen a
  , ScopeCodeGen b
  , CompareBranchesResults (RetExprs a) (RetExprs b)
  -- These constraints below are implied by the one above, but GHC needs a proof
  , RetVars a ~ RetVars b
  , RetOutStack a ~ RetOutStack b
  )

-- | If statement. All variables created inside its branches will be released
-- after the execution leaves the scope in which they were created.
if_
  :: forall inp xs ys a b . IfConstraint a b
  => Expr Bool
  -> IndigoState inp xs a
  -> IndigoState inp ys b
  -> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
if_ :: Expr Bool
-> IndigoState inp xs a
-> IndigoState inp ys b
-> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
if_ e :: Expr Bool
e t :: IndigoState inp xs a
t f :: IndigoState inp ys b
f = (MetaData inp
 -> GenCode
      inp
      (RetOutStack' (ClassifyReturnValue b) b ++ inp)
      (RetVars' (ClassifyReturnValue b) b))
-> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
forall (inp :: [*]) (out :: [*]) a.
(MetaData inp -> GenCode inp out a) -> IndigoState inp out a
IndigoState ((MetaData inp
  -> GenCode
       inp
       (RetOutStack' (ClassifyReturnValue b) b ++ inp)
       (RetVars' (ClassifyReturnValue b) b))
 -> IndigoState inp (RetOutStack a ++ inp) (RetVars a))
-> (MetaData inp
    -> GenCode
         inp
         (RetOutStack' (ClassifyReturnValue b) b ++ inp)
         (RetVars' (ClassifyReturnValue b) b))
-> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
forall a b. (a -> b) -> a -> b
$ \md :: MetaData inp
md ->
  let cde :: inp :-> (Bool & inp)
cde = GenCode inp (Bool & inp) () -> inp :-> (Bool & inp)
forall (inp :: [*]) (out :: [*]) a.
GenCode inp out a -> inp :-> out
gcCode (GenCode inp (Bool & inp) () -> inp :-> (Bool & inp))
-> GenCode inp (Bool & inp) () -> inp :-> (Bool & inp)
forall a b. (a -> b) -> a -> b
$ IndigoState inp (Bool & inp) ()
-> MetaData inp -> GenCode inp (Bool & inp) ()
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState (Expr Bool -> IndigoState inp (Bool & inp) ()
forall a (inp :: [*]). Expr a -> IndigoState inp (a & inp) ()
compileExpr Expr Bool
e) MetaData inp
md in
  let gc1 :: GenCode inp xs a
gc1 = IndigoState inp xs a -> MetaData inp -> GenCode inp xs a
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState IndigoState inp xs a
t MetaData inp
md in
  let gc2 :: GenCode inp ys b
gc2 = IndigoState inp ys b -> MetaData inp -> GenCode inp ys b
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState IndigoState inp ys b
f MetaData inp
md in
  MetaData inp
-> (inp :-> (RetOutStack a ++ inp))
-> GenCode inp (RetOutStack a ++ inp) (RetVars a)
forall ret (inp :: [*]).
ScopeCodeGen ret =>
MetaData inp
-> (inp :-> (RetOutStack ret ++ inp))
-> GenCode inp (RetOutStack ret ++ inp) (RetVars ret)
finalizeStatement @a MetaData inp
md (inp :-> (Bool & inp)
cde (inp :-> (Bool & inp))
-> ((Bool & inp)
    :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp))
-> inp :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (inp :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp))
-> (inp :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp))
-> (Bool & inp) :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp)
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
L.if_ (GenCode inp xs a -> inp :-> (RetOutStack a ++ inp)
forall ret (inp :: [*]) (xs :: [*]).
ScopeCodeGen ret =>
GenCode inp xs ret -> inp :-> (RetOutStack ret ++ inp)
compileScope GenCode inp xs a
gc1) (GenCode inp ys b
-> inp :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp)
forall ret (inp :: [*]) (xs :: [*]).
ScopeCodeGen ret =>
GenCode inp xs ret -> inp :-> (RetOutStack ret ++ inp)
compileScope GenCode inp ys b
gc2))

-- | If which works like case for Maybe.
ifSome
  :: forall inp xs ys x a b . (IfConstraint a b, KnownValue x)
  => Expr (Maybe x)
  -> (Var x -> IndigoState (x & inp) xs a)
  -> IndigoState inp ys b
  -> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
ifSome :: Expr (Maybe x)
-> (Var x -> IndigoState (x & inp) xs a)
-> IndigoState inp ys b
-> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
ifSome e :: Expr (Maybe x)
e t :: Var x -> IndigoState (x & inp) xs a
t f :: IndigoState inp ys b
f = (MetaData inp
 -> GenCode
      inp
      (RetOutStack' (ClassifyReturnValue b) b ++ inp)
      (RetVars' (ClassifyReturnValue b) b))
-> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
forall (inp :: [*]) (out :: [*]) a.
(MetaData inp -> GenCode inp out a) -> IndigoState inp out a
IndigoState ((MetaData inp
  -> GenCode
       inp
       (RetOutStack' (ClassifyReturnValue b) b ++ inp)
       (RetVars' (ClassifyReturnValue b) b))
 -> IndigoState inp (RetOutStack a ++ inp) (RetVars a))
-> (MetaData inp
    -> GenCode
         inp
         (RetOutStack' (ClassifyReturnValue b) b ++ inp)
         (RetVars' (ClassifyReturnValue b) b))
-> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
forall a b. (a -> b) -> a -> b
$ \md :: MetaData inp
md ->
  let cde :: inp :-> (Maybe x & inp)
cde = GenCode inp (Maybe x & inp) () -> inp :-> (Maybe x & inp)
forall (inp :: [*]) (out :: [*]) a.
GenCode inp out a -> inp :-> out
gcCode (GenCode inp (Maybe x & inp) () -> inp :-> (Maybe x & inp))
-> GenCode inp (Maybe x & inp) () -> inp :-> (Maybe x & inp)
forall a b. (a -> b) -> a -> b
$ IndigoState inp (Maybe x & inp) ()
-> MetaData inp -> GenCode inp (Maybe x & inp) ()
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState (Expr (Maybe x) -> IndigoState inp (Maybe x & inp) ()
forall a (inp :: [*]). Expr a -> IndigoState inp (a & inp) ()
compileExpr Expr (Maybe x)
e) MetaData inp
md in
  let (v :: Var x
v, mdJust :: MetaData (x & inp)
mdJust) = MetaData inp -> (Var x, MetaData (x & inp))
forall x (stk :: [*]).
KnownValue x =>
MetaData stk -> (Var x, MetaData (x & stk))
pushRefMd MetaData inp
md in
  let gc1 :: GenCode (x & inp) xs a
gc1 = IndigoState (x & inp) xs a
-> MetaData (x & inp) -> GenCode (x & inp) xs a
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState (Var x -> IndigoState (x & inp) xs a
t Var x
v) MetaData (x & inp)
mdJust in
  let gc2 :: GenCode inp ys b
gc2 = IndigoState inp ys b -> MetaData inp -> GenCode inp ys b
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState IndigoState inp ys b
f MetaData inp
md in
  MetaData inp
-> (inp :-> (RetOutStack a ++ inp))
-> GenCode inp (RetOutStack a ++ inp) (RetVars a)
forall ret (inp :: [*]).
ScopeCodeGen ret =>
MetaData inp
-> (inp :-> (RetOutStack ret ++ inp))
-> GenCode inp (RetOutStack ret ++ inp) (RetVars ret)
finalizeStatement @a MetaData inp
md ((inp :-> (RetOutStack a ++ inp))
 -> GenCode
      inp
      (RetOutStack' (ClassifyReturnValue b) b ++ inp)
      (RetVars' (ClassifyReturnValue b) b))
-> (inp :-> (RetOutStack a ++ inp))
-> GenCode
     inp
     (RetOutStack' (ClassifyReturnValue b) b ++ inp)
     (RetVars' (ClassifyReturnValue b) b)
forall a b. (a -> b) -> a -> b
$
    inp :-> (Maybe x & inp)
cde (inp :-> (Maybe x & inp))
-> ((Maybe x & inp)
    :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp))
-> inp :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
    ((x & inp) :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp))
-> (inp :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp))
-> (Maybe x & inp)
   :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp)
forall a (s :: [*]) (s' :: [*]).
((a & s) :-> s') -> (s :-> s') -> (Maybe a & s) :-> s'
L.ifSome
      ( GenCode (x & inp) xs a
-> (x & inp) :-> (RetOutStack a ++ (x & inp))
forall ret (inp :: [*]) (xs :: [*]).
ScopeCodeGen ret =>
GenCode inp xs ret -> inp :-> (RetOutStack ret ++ inp)
compileScope GenCode (x & inp) xs a
gc1 ((x & inp)
 :-> (RetOutStack' (ClassifyReturnValue b) b ++ (x & inp)))
-> ((RetOutStack' (ClassifyReturnValue b) b ++ (x & inp))
    :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp))
-> (x & inp) :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
       -- after this we have stack (e1 & e2 .. & ek & x & inp)
       ((x & inp) :-> inp)
-> (RetOutStack a ++ (x & inp)) :-> (RetOutStack a ++ inp)
forall (retKind :: BranchRetKind) ret (xs :: [*]) (inp :: [*]).
ScopeCodeGen' retKind ret =>
(xs :-> inp)
-> (RetOutStack' retKind ret ++ xs)
   :-> (RetOutStack' retKind ret ++ inp)
liftClear' @(ClassifyReturnValue a) @a @(x & inp) @inp (x & inp) :-> inp
forall a (s :: [*]). (a & s) :-> s
L.drop
       -- this can be lifted together with glClear code, but let's leave it like this for now
      )
      (GenCode inp ys b
-> inp :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp)
forall ret (inp :: [*]) (xs :: [*]).
ScopeCodeGen ret =>
GenCode inp xs ret -> inp :-> (RetOutStack ret ++ inp)
compileScope GenCode inp ys b
gc2)

-- | If which works like case for Either.
ifRight
  :: forall inp xs ys x y a b . (IfConstraint a b, KnownValue x, KnownValue y)
  => Expr (Either y x)
  -> (Var x -> IndigoState (x & inp) xs a)
  -> (Var y -> IndigoState (y & inp) ys b)
  -> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
ifRight :: Expr (Either y x)
-> (Var x -> IndigoState (x & inp) xs a)
-> (Var y -> IndigoState (y & inp) ys b)
-> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
ifRight e :: Expr (Either y x)
e r :: Var x -> IndigoState (x & inp) xs a
r l :: Var y -> IndigoState (y & inp) ys b
l = (MetaData inp
 -> GenCode
      inp
      (RetOutStack' (ClassifyReturnValue b) b ++ inp)
      (RetVars' (ClassifyReturnValue b) b))
-> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
forall (inp :: [*]) (out :: [*]) a.
(MetaData inp -> GenCode inp out a) -> IndigoState inp out a
IndigoState ((MetaData inp
  -> GenCode
       inp
       (RetOutStack' (ClassifyReturnValue b) b ++ inp)
       (RetVars' (ClassifyReturnValue b) b))
 -> IndigoState inp (RetOutStack a ++ inp) (RetVars a))
-> (MetaData inp
    -> GenCode
         inp
         (RetOutStack' (ClassifyReturnValue b) b ++ inp)
         (RetVars' (ClassifyReturnValue b) b))
-> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
forall a b. (a -> b) -> a -> b
$ \md :: MetaData inp
md ->
  let
    cde :: inp :-> (Either y x & inp)
cde = GenCode inp (Either y x & inp) () -> inp :-> (Either y x & inp)
forall (inp :: [*]) (out :: [*]) a.
GenCode inp out a -> inp :-> out
gcCode (GenCode inp (Either y x & inp) () -> inp :-> (Either y x & inp))
-> GenCode inp (Either y x & inp) () -> inp :-> (Either y x & inp)
forall a b. (a -> b) -> a -> b
$ IndigoState inp (Either y x & inp) ()
-> MetaData inp -> GenCode inp (Either y x & inp) ()
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState (Expr (Either y x) -> IndigoState inp (Either y x & inp) ()
forall a (inp :: [*]). Expr a -> IndigoState inp (a & inp) ()
compileExpr Expr (Either y x)
e) MetaData inp
md
    (v :: Var x
v, mdRight :: MetaData (x & inp)
mdRight) = MetaData inp -> (Var x, MetaData (x & inp))
forall x (stk :: [*]).
KnownValue x =>
MetaData stk -> (Var x, MetaData (x & stk))
pushRefMd MetaData inp
md
    (w :: Var y
w, mdLeft :: MetaData (y & inp)
mdLeft) = MetaData inp -> (Var y, MetaData (y & inp))
forall x (stk :: [*]).
KnownValue x =>
MetaData stk -> (Var x, MetaData (x & stk))
pushRefMd MetaData inp
md
    gc1 :: GenCode (x & inp) xs a
gc1 = IndigoState (x & inp) xs a
-> MetaData (x & inp) -> GenCode (x & inp) xs a
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState (Var x -> IndigoState (x & inp) xs a
r Var x
v) MetaData (x & inp)
mdRight
    gc2 :: GenCode (y & inp) ys b
gc2 = IndigoState (y & inp) ys b
-> MetaData (y & inp) -> GenCode (y & inp) ys b
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState (Var y -> IndigoState (y & inp) ys b
l Var y
w) MetaData (y & inp)
mdLeft
  in
    MetaData inp
-> (inp :-> (RetOutStack a ++ inp))
-> GenCode inp (RetOutStack a ++ inp) (RetVars a)
forall ret (inp :: [*]).
ScopeCodeGen ret =>
MetaData inp
-> (inp :-> (RetOutStack ret ++ inp))
-> GenCode inp (RetOutStack ret ++ inp) (RetVars ret)
finalizeStatement @a MetaData inp
md ((inp :-> (RetOutStack a ++ inp))
 -> GenCode
      inp
      (RetOutStack' (ClassifyReturnValue b) b ++ inp)
      (RetVars' (ClassifyReturnValue b) b))
-> (inp :-> (RetOutStack a ++ inp))
-> GenCode
     inp
     (RetOutStack' (ClassifyReturnValue b) b ++ inp)
     (RetVars' (ClassifyReturnValue b) b)
forall a b. (a -> b) -> a -> b
$
      inp :-> (Either y x & inp)
cde (inp :-> (Either y x & inp))
-> ((Either y x & inp)
    :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp))
-> inp :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
      ((x & inp) :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp))
-> ((y & inp) :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp))
-> (Either y x & inp)
   :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp)
forall b (s :: [*]) (s' :: [*]) a.
((b & s) :-> s') -> ((a & s) :-> s') -> (Either a b & s) :-> s'
L.ifRight
        ( GenCode (x & inp) xs a
-> (x & inp) :-> (RetOutStack a ++ (x & inp))
forall ret (inp :: [*]) (xs :: [*]).
ScopeCodeGen ret =>
GenCode inp xs ret -> inp :-> (RetOutStack ret ++ inp)
compileScope GenCode (x & inp) xs a
gc1 ((x & inp)
 :-> (RetOutStack' (ClassifyReturnValue b) b ++ (x & inp)))
-> ((RetOutStack' (ClassifyReturnValue b) b ++ (x & inp))
    :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp))
-> (x & inp) :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
        -- after this we have stack (e1 & e2 .. & ek & x & inp)
        ((x & inp) :-> inp)
-> (RetOutStack a ++ (x & inp)) :-> (RetOutStack a ++ inp)
forall (retKind :: BranchRetKind) ret (xs :: [*]) (inp :: [*]).
ScopeCodeGen' retKind ret =>
(xs :-> inp)
-> (RetOutStack' retKind ret ++ xs)
   :-> (RetOutStack' retKind ret ++ inp)
liftClear' @(ClassifyReturnValue a) @a @(x & inp) @inp (x & inp) :-> inp
forall a (s :: [*]). (a & s) :-> s
L.drop
        -- this can be lifted together with glClear code, but let's leave it like this for now
        )
        ( GenCode (y & inp) ys b
-> (y & inp)
   :-> (RetOutStack' (ClassifyReturnValue b) b ++ (y & inp))
forall ret (inp :: [*]) (xs :: [*]).
ScopeCodeGen ret =>
GenCode inp xs ret -> inp :-> (RetOutStack ret ++ inp)
compileScope GenCode (y & inp) ys b
gc2 ((y & inp)
 :-> (RetOutStack' (ClassifyReturnValue b) b ++ (y & inp)))
-> ((RetOutStack' (ClassifyReturnValue b) b ++ (y & inp))
    :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp))
-> (y & inp) :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
        -- after this we have stack (e1 & e2 .. & ek & x & inp)
        ((y & inp) :-> inp)
-> (RetOutStack' (ClassifyReturnValue b) b ++ (y & inp))
   :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp)
forall (retKind :: BranchRetKind) ret (xs :: [*]) (inp :: [*]).
ScopeCodeGen' retKind ret =>
(xs :-> inp)
-> (RetOutStack' retKind ret ++ xs)
   :-> (RetOutStack' retKind ret ++ inp)
liftClear' @(ClassifyReturnValue b) @b @(y & inp) @inp (y & inp) :-> inp
forall a (s :: [*]). (a & s) :-> s
L.drop
        -- this can be lifted together with glClear code, but let's leave it like this for now
        )

ifCons
  :: forall inp xs ys x a b . (IfConstraint a b, KnownValue x)
  => Expr (List x)
  -> (Var x -> Var (List x) -> IndigoState (x & List x & inp) xs a)
  -> IndigoState inp ys b
  -> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
ifCons :: Expr (List x)
-> (Var x -> Var (List x) -> IndigoState (x & (List x & inp)) xs a)
-> IndigoState inp ys b
-> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
ifCons e :: Expr (List x)
e t :: Var x -> Var (List x) -> IndigoState (x & (List x & inp)) xs a
t f :: IndigoState inp ys b
f = (MetaData inp
 -> GenCode
      inp
      (RetOutStack' (ClassifyReturnValue b) b ++ inp)
      (RetVars' (ClassifyReturnValue b) b))
-> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
forall (inp :: [*]) (out :: [*]) a.
(MetaData inp -> GenCode inp out a) -> IndigoState inp out a
IndigoState ((MetaData inp
  -> GenCode
       inp
       (RetOutStack' (ClassifyReturnValue b) b ++ inp)
       (RetVars' (ClassifyReturnValue b) b))
 -> IndigoState inp (RetOutStack a ++ inp) (RetVars a))
-> (MetaData inp
    -> GenCode
         inp
         (RetOutStack' (ClassifyReturnValue b) b ++ inp)
         (RetVars' (ClassifyReturnValue b) b))
-> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
forall a b. (a -> b) -> a -> b
$ \md :: MetaData inp
md ->
  let
    cde :: inp :-> (List x & inp)
cde = GenCode inp (List x & inp) () -> inp :-> (List x & inp)
forall (inp :: [*]) (out :: [*]) a.
GenCode inp out a -> inp :-> out
gcCode (GenCode inp (List x & inp) () -> inp :-> (List x & inp))
-> GenCode inp (List x & inp) () -> inp :-> (List x & inp)
forall a b. (a -> b) -> a -> b
$ IndigoState inp (List x & inp) ()
-> MetaData inp -> GenCode inp (List x & inp) ()
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState (Expr (List x) -> IndigoState inp (List x & inp) ()
forall a (inp :: [*]). Expr a -> IndigoState inp (a & inp) ()
compileExpr Expr (List x)
e) MetaData inp
md
    (l :: Var (List x)
l, mdList :: MetaData (List x & inp)
mdList) = MetaData inp -> (Var (List x), MetaData (List x & inp))
forall x (stk :: [*]).
KnownValue x =>
MetaData stk -> (Var x, MetaData (x & stk))
pushRefMd MetaData inp
md
    (v :: Var x
v, mdVal :: MetaData (x & (List x & inp))
mdVal) = MetaData (List x & inp) -> (Var x, MetaData (x & (List x & inp)))
forall x (stk :: [*]).
KnownValue x =>
MetaData stk -> (Var x, MetaData (x & stk))
pushRefMd MetaData (List x & inp)
mdList
    gc1 :: GenCode (x & (List x & inp)) xs a
gc1 = IndigoState (x & (List x & inp)) xs a
-> MetaData (x & (List x & inp))
-> GenCode (x & (List x & inp)) xs a
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState (Var x -> Var (List x) -> IndigoState (x & (List x & inp)) xs a
t Var x
v Var (List x)
l) MetaData (x & (List x & inp))
mdVal
    gc2 :: GenCode inp ys b
gc2 = IndigoState inp ys b -> MetaData inp -> GenCode inp ys b
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState IndigoState inp ys b
f MetaData inp
md
  in
    MetaData inp
-> (inp :-> (RetOutStack a ++ inp))
-> GenCode inp (RetOutStack a ++ inp) (RetVars a)
forall ret (inp :: [*]).
ScopeCodeGen ret =>
MetaData inp
-> (inp :-> (RetOutStack ret ++ inp))
-> GenCode inp (RetOutStack ret ++ inp) (RetVars ret)
finalizeStatement @a MetaData inp
md ((inp :-> (RetOutStack a ++ inp))
 -> GenCode
      inp
      (RetOutStack' (ClassifyReturnValue b) b ++ inp)
      (RetVars' (ClassifyReturnValue b) b))
-> (inp :-> (RetOutStack a ++ inp))
-> GenCode
     inp
     (RetOutStack' (ClassifyReturnValue b) b ++ inp)
     (RetVars' (ClassifyReturnValue b) b)
forall a b. (a -> b) -> a -> b
$
      inp :-> (List x & inp)
cde (inp :-> (List x & inp))
-> ((List x & inp)
    :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp))
-> inp :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
      ((x & (List x & inp))
 :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp))
-> (inp :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp))
-> (List x & inp)
   :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp)
forall a (s :: [*]) (s' :: [*]).
((a & (List a & s)) :-> s') -> (s :-> s') -> (List a & s) :-> s'
L.ifCons
        ( GenCode (x & (List x & inp)) xs a
-> (x & (List x & inp)) :-> (RetOutStack a ++ (x & (List x & inp)))
forall ret (inp :: [*]) (xs :: [*]).
ScopeCodeGen ret =>
GenCode inp xs ret -> inp :-> (RetOutStack ret ++ inp)
compileScope GenCode (x & (List x & inp)) xs a
gc1 ((x & (List x & inp))
 :-> (RetOutStack' (ClassifyReturnValue b) b
      ++ (x & (List x & inp))))
-> ((RetOutStack' (ClassifyReturnValue b) b
     ++ (x & (List x & inp)))
    :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp))
-> (x & (List x & inp))
   :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
          ((x & (List x & inp)) :-> inp)
-> (RetOutStack a ++ (x & (List x & inp)))
   :-> (RetOutStack a ++ inp)
forall (retKind :: BranchRetKind) ret (xs :: [*]) (inp :: [*]).
ScopeCodeGen' retKind ret =>
(xs :-> inp)
-> (RetOutStack' retKind ret ++ xs)
   :-> (RetOutStack' retKind ret ++ inp)
liftClear' @(ClassifyReturnValue a) @a @(x & List x & inp) @inp ((x & (List x & inp)) :-> (List x & inp)
forall a (s :: [*]). (a & s) :-> s
L.drop ((x & (List x & inp)) :-> (List x & inp))
-> ((List x & inp) :-> inp) -> (x & (List x & inp)) :-> inp
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (List x & inp) :-> inp
forall a (s :: [*]). (a & s) :-> s
L.drop)
        )
        (GenCode inp ys b
-> inp :-> (RetOutStack' (ClassifyReturnValue b) b ++ inp)
forall ret (inp :: [*]) (xs :: [*]).
ScopeCodeGen ret =>
GenCode inp xs ret -> inp :-> (RetOutStack ret ++ inp)
compileScope GenCode inp ys b
gc2)