-- 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_ e t f = IndigoState $ \md ->
  let cde = gcCode $ runIndigoState (compileExpr e) md in
  let gc1 = runIndigoState t md in
  let gc2 = runIndigoState f md in
  finalizeStatement @a md (cde # L.if_ (compileScope gc1) (compileScope 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 e t f = IndigoState $ \md ->
  let cde = gcCode $ runIndigoState (compileExpr e) md in
  let (v, mdJust) = pushRefMd md in
  let gc1 = runIndigoState (t v) mdJust in
  let gc2 = runIndigoState f md in
  finalizeStatement @a md $
    cde #
    L.ifSome
      ( compileScope gc1 #
       -- after this we have stack (e1 & e2 .. & ek & x & inp)
       liftClear' @(ClassifyReturnValue a) @a @(x & inp) @inp L.drop
       -- this can be lifted together with glClear code, but let's leave it like this for now
      )
      (compileScope 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 e r l = IndigoState $ \md ->
  let
    cde = gcCode $ runIndigoState (compileExpr e) md
    (v, mdRight) = pushRefMd md
    (w, mdLeft) = pushRefMd md
    gc1 = runIndigoState (r v) mdRight
    gc2 = runIndigoState (l w) mdLeft
  in
    finalizeStatement @a md $
      cde #
      L.ifRight
        ( compileScope gc1 #
        -- after this we have stack (e1 & e2 .. & ek & x & inp)
        liftClear' @(ClassifyReturnValue a) @a @(x & inp) @inp L.drop
        -- this can be lifted together with glClear code, but let's leave it like this for now
        )
        ( compileScope gc2 #
        -- after this we have stack (e1 & e2 .. & ek & x & inp)
        liftClear' @(ClassifyReturnValue b) @b @(y & inp) @inp 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 e t f = IndigoState $ \md ->
  let
    cde = gcCode $ runIndigoState (compileExpr e) md
    (l, mdList) = pushRefMd md
    (v, mdVal) = pushRefMd mdList
    gc1 = runIndigoState (t v l) mdVal
    gc2 = runIndigoState f md
  in
    finalizeStatement @a md $
      cde #
      L.ifCons
        ( compileScope gc1 #
          liftClear' @(ClassifyReturnValue a) @a @(x & List x & inp) @inp (L.drop # L.drop)
        )
        (compileScope gc2)