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

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

-- | Backend machinery for cases.

module Indigo.Backend.Case
  ( caseRec
  , entryCaseRec
  , entryCaseSimpleRec

  , IndigoCaseClauseL
  , IndigoClause (..)
  , CaseCommonF
  ) where

import Data.Vinyl.Core (RMap(..))
import Fmt (pretty)
import Util.Type (type (++))
import Util.TypeLits (AppendSymbol)

import Indigo.Backend.Prelude
import Indigo.Backend.Scope
import Indigo.Internal hiding ((<>))
import Indigo.Lorentz
import qualified Lorentz.ADT as L
import qualified Lorentz.Entrypoints.Doc as L
import qualified Lorentz.Instr as L
import Michelson.Typed.Haskell.Instr.Sum
  (CaseClauseParam(..), CaseClauses, CtorField(..), InstrCaseC)

-- | This type is analogous to the 'CaseClauseL' type but instead of wrapping a Lorentz
-- instruction, this wraps an Indigo value with the same input/output types.
data IndigoCaseClauseL ret (param :: CaseClauseParam) where
  OneFieldIndigoCaseClauseL
    :: (forall inp .
         MetaData inp
      -> CaseClauseL inp (RetOutStack ret ++ inp) ('CaseClauseParam ctor ('OneField x)))
    -> IndigoCaseClauseL ret ('CaseClauseParam ctor ('OneField x))

data IndigoClause x ret where
  IndigoClause
    :: ( KnownValue x
       , ScopeCodeGen retBr
       , ret ~ RetExprs retBr
       , RetOutStack ret ~ RetOutStack retBr
       )
    => Var x
    -- ^ Variable for the clause input value (available to its code block)
    -> (forall inp. SomeIndigoState (x : inp))
    -- ^ Clause code block
    -> retBr
    -- ^ Clause return value(s)
    -> IndigoClause x ret

instance
  (name ~ AppendSymbol "c" ctor, KnownValue x)
  =>
    CaseArrow
      name
      (IndigoClause x ret)
      (IndigoCaseClauseL ret ('CaseClauseParam ctor ('OneField x)))
  where
    (/->) _ (IndigoClause varCase sIndSt (ret :: retBr)) =
      OneFieldIndigoCaseClauseL $ \md@MetaData{..} -> case sIndSt of
        (SomeIndigoState body :: SomeIndigoState (x : inp)) ->
          -- Create a reference to the top of stack
          case body (pushRefMd varCase md) of
            SomeGenCode bodyCd ->
              CaseClauseL $
                auxiliaryHook md ("case branch against " <> pretty varCase) $
                  -- Compute returning expressions and clean up everything
                  compileScope @retBr (\stk -> MetaData stk mdObjects mdHooks) bodyCd ret #
                  -- Remove @x@ from the stack too
                  liftClear @retBr @inp @(x : inp) L.drop

-- | This constraint is shared by all @case*@ functions.
-- Including some outside this module.
type CaseCommonF f dt ret clauses =
  ( InstrCaseC dt
  , RMap (CaseClauses dt)
  , clauses ~ Rec (f ret) (CaseClauses dt)
  , ScopeCodeGen ret
  )

-- | This constraint is shared by all backend @case*@ functions.
type CaseCommon dt ret clauses = CaseCommonF IndigoCaseClauseL dt ret clauses

-- | A case statement for indigo. See examples for a sample usage.
caseRec
  :: forall dt inp ret clauses . CaseCommon dt ret clauses
  => Expr dt
  -> clauses
  -> RetVars ret
  -- ^ Variable(s) that will be assigned to the resulting value(s)
  -> IndigoState inp (RetOutStack ret ++ inp)
caseRec g cls vars = IndigoState $ \md ->
  let cdG = gcCode $ usingIndigoState md (compileExpr g) in
  finalizeStatement @ret (mdStack md) vars $ stmtHook md (condStmtPretty @ret vars "caseRec" g) $
    exprHook md (pretty g) cdG #
    L.case_ (toCaseClauseL md cls)

-- | 'case_' for pattern-matching on parameter.
entryCaseRec
  :: forall dt entrypointKind inp ret clauses .
  ( CaseCommon dt ret clauses
  , DocumentEntrypoints entrypointKind dt
  )
  => Proxy entrypointKind
  -> Expr dt
  -> clauses
  -> RetVars ret
  -- ^ Variable(s) that will be assigned to the resulting value(s)
  -> IndigoState inp (RetOutStack ret ++ inp)
entryCaseRec proxy g cls vars = IndigoState $ \md ->
  let cdG = gcCode $ usingIndigoState md (compileExpr g) in
  finalizeStatement @ret (mdStack md) vars $ stmtHook md (condStmtPretty @ret vars "entryCaseRec" g) $
    exprHook md (pretty g) cdG #
    L.entryCase_ proxy (toCaseClauseL md cls)

-- | 'entryCase_' for contracts with flat parameter.
entryCaseSimpleRec
  :: forall dt inp ret clauses .
     ( CaseCommon dt ret clauses
     , DocumentEntrypoints PlainEntrypointsKind dt
     , NiceParameterFull dt
     , RequireFlatParamEps dt
     )
  => Expr dt
  -> clauses
  -> RetVars ret
  -- ^ Variable(s) that will be assigned to the resulting value(s)
  -> IndigoState inp (RetOutStack ret ++ inp)
entryCaseSimpleRec g cls vars = IndigoState $ \md ->
  let cdG = gcCode $ usingIndigoState md (compileExpr g) in
  finalizeStatement @ret (mdStack md) vars $ stmtHook md (condStmtPretty @ret vars "entryCaseSimpleRec" g) $
    exprHook md (pretty g) cdG #
    L.entryCaseSimple_ (toCaseClauseL md cls)

toCaseClauseL
  :: forall inp ret cs .
     MetaData inp
  -> Rec (IndigoCaseClauseL ret) cs
  -> Rec (CaseClauseL inp (RetOutStack ret ++ inp)) cs
toCaseClauseL _ RNil = RNil
toCaseClauseL md (OneFieldIndigoCaseClauseL fn :& rest) = fn md :& toCaseClauseL md rest