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

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

-- | High level statements of Indigo language.

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

  , IndigoCaseClauseL
  , CaseCommonF
  , CaseCommon
  , IndigoAnyOut (..)
  ) where

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

import Indigo.Backend.Prelude
import Indigo.Backend.Scope
import Indigo.Internal
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 IndigoAnyOut x ret = forall retBranch .
  ( ScopeCodeGen retBranch
  , RetOutStack ret ~ RetOutStack retBranch
  ) =>
  IndigoAnyOut (forall inp . SomeIndigoState (x : inp) retBranch)

instance
  ( name ~ AppendSymbol "c" ctor
  , KnownValue x
  )
  =>
    CaseArrow
      name
      (Var x -> IndigoAnyOut x ret)
      (IndigoCaseClauseL ret ('CaseClauseParam ctor ('OneField x)))
  where
    (/->) _ ind =
      OneFieldIndigoCaseClauseL (\(md :: MetaData inp) ->
        -- Create a reference to the top of stack
        let (varCase, mdCaseBody) = pushRefMd md in
        -- Pass the reference to the case body
        case ind varCase of
          IndigoAnyOut (SomeIndigoState body :: SomeIndigoState (x : inp) retBr) ->
            case body mdCaseBody of
              SomeGenCode gc ->
                CaseClauseL $
                  -- Compute returning expressions and clean up everything
                  compileScope gc #
                  -- Remove @x@ from the stack too
                  liftClear' @(ClassifyReturnValue retBr) @retBr @(x & inp) @inp L.drop
      )

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

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
  -> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret)
caseRec g cls = IndigoState $ \md ->
  let cdG = gcCode $ runIndigoState (compileExpr g) md in
  finalizeStatement @ret md (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
  -> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret)
entryCaseRec proxy g cls = IndigoState $ \md ->
  let cdG = gcCode $ runIndigoState (compileExpr g) md in
  finalizeStatement @ret md (cdG # L.entryCase_ proxy (toCaseClauseL md cls))

-- | 'entryCase_' for contracts with flat parameter.
entryCaseSimpleRec
  :: forall cp inp ret clauses .
     ( CaseCommon cp ret clauses
     , DocumentEntrypoints PlainEntrypointsKind cp
     , NiceParameterFull cp
     , RequireFlatParamEps cp
     )
  => Expr cp
  -> clauses
  -> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret)
entryCaseSimpleRec g cls = IndigoState $ \md ->
  let cdG = gcCode $ runIndigoState (compileExpr g) md in
  finalizeStatement @ret md (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