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

-- | 'StatementF' functor datatype for Freer monad

module Indigo.Frontend.Statement
  ( StatementF (..)

  , IfConstraint
  , IndigoMCaseClauseL (..)
  , LambdaKind (..)
  , withLambdaKind
  ) where

import qualified Data.Kind as Kind
import Util.TypeLits (AppendSymbol)

import Lorentz.Entrypoints.Helpers (RequireSumType)
import qualified Lorentz.Run as L (Contract)
import Michelson.Typed.Haskell.Instr.Sum (CaseClauseParam(..), CtorField(..))

import Indigo.Backend
import Indigo.Internal
import Indigo.Lorentz
import Indigo.Prelude

-- | Analogous datatype as IndigoCaseClauseL from Indigo.Backend.Case
data IndigoMCaseClauseL freer ret (param :: CaseClauseParam) where
    OneFieldIndigoMCaseClauseL
      :: ( name ~ (AppendSymbol "c" ctor)
         , KnownValue x
         , ScopeCodeGen retBr
         , ret ~ RetExprs retBr
         , RetOutStack ret ~ RetOutStack retBr
         )
      => Label name
      -> (Var x -> freer retBr)
      -> IndigoMCaseClauseL freer ret ('CaseClauseParam ctor ('OneField x))

-- | StatementF functor for Freer monad.
--
-- The constructors correspond to every Indigo statement that has expressions
-- (@'Expr' x@) in its signature.
--
-- The ones that don't take expressions are compiled directly to 'IndigoState'
-- (and kept in 'LiftIndigoState'), because they won't be taken into consideration
-- by an optimizer anyway.
--
-- One more detail about 'StatementF' is that it takes a @cont@ type parameter,
-- which is basically 'IndigoM' (freer monad), to avoid cyclic dependencies.
-- @cont@ is needed to support statements which have recursive structure
-- (like: @if@, @while@, @case@, etc).
data StatementF (freer :: Kind.Type -> Kind.Type) a where
  -- | Direct injection of IndigoState of statements
  -- which are not going to be analyzed by optimizer.
  LiftIndigoState :: (forall inp. SomeIndigoState inp) -> StatementF freer ()

  NewVar :: KnownValue x => Expr x -> StatementF freer (Var x)
  SetVar :: KnownValue x => Var x -> Expr x -> StatementF freer ()
  VarModification
    :: (IsObject x, KnownValue y)
    => [y, x] :-> '[x]
    -> Var x
    -> Expr y
    -> StatementF freer ()
  SetField ::
    ( IsObject dt
    , IsObject ftype
    , HasField dt fname ftype
    )
    => Var dt -> Label fname -> Expr ftype -> StatementF cont ()

  LambdaCall1
    :: LambdaKind st arg res extra
    -> String
    -> (Var arg -> freer res)
    -> Expr arg
    -> StatementF freer (RetVars res)

  Scope :: ScopeCodeGen a => freer a -> StatementF freer (RetVars a)
  If
    :: IfConstraint a b
    => Expr Bool
    -> freer a
    -> freer b
    -> StatementF freer (RetVars a)
  IfSome
    :: (IfConstraint a b, KnownValue x)
    => Expr (Maybe x)
    -> (Var x -> freer a)
    -> freer b
    -> StatementF freer (RetVars a)
  IfRight
    :: (IfConstraint a b, KnownValue x, KnownValue y)
    => Expr (Either y x)
    -> (Var x -> freer a)
    -> (Var y -> freer b)
    -> StatementF freer (RetVars a)
  IfCons
    :: (IfConstraint a b, KnownValue x)
    => Expr (List x)
    -> (Var x -> Var (List x) -> freer a)
    -> freer b
    -> StatementF freer (RetVars a)
  Case
    :: CaseCommonF (IndigoMCaseClauseL freer) dt ret clauses
    => Expr dt -> clauses
    -> StatementF freer (RetVars ret)
  EntryCase
    :: ( CaseCommonF (IndigoMCaseClauseL freer) dt ret clauses
       , DocumentEntrypoints entrypointKind dt
       )
    => Proxy entrypointKind
    -> Expr dt
    -> clauses
    -> StatementF freer (RetVars ret)
  EntryCaseSimple
    :: ( CaseCommonF (IndigoMCaseClauseL freer) cp ret clauses
       , DocumentEntrypoints PlainEntrypointsKind cp
       , NiceParameterFull cp
       , RequireFlatParamEps cp
       )
    => Expr cp
    -> clauses
    -> StatementF freer (RetVars ret)

  While :: Expr Bool -> freer () -> StatementF freer ()
  WhileLeft
    :: (KnownValue x, KnownValue y)
    => Expr (Either y x)
    -> (Var y -> freer ())
    -> StatementF freer (Var x)
  ForEach
    :: (IterOpHs a, KnownValue (IterOpElHs a))
    => Expr a
    -> (Var (IterOpElHs a) -> freer ())
    -> StatementF freer ()

  ContractName :: Text        -> freer () -> StatementF freer ()
  DocGroup     :: DocGrouping -> freer () -> StatementF freer ()
  ContractGeneral :: freer () -> StatementF freer ()
  FinalizeParamCallingDoc
    :: (NiceParameterFull cp, RequireSumType cp, HasCallStack)
    => (Var cp -> freer ()) -> Expr cp -> StatementF freer ()

  TransferTokens
    :: (NiceParameter p, HasSideEffects)
    => Expr p -> Expr Mutez -> Expr (ContractRef p) -> StatementF freer ()
  SetDelegate :: HasSideEffects => Expr (Maybe KeyHash) -> StatementF freer ()

  CreateContract
    :: ( IsObject st
       , NiceStorage st, NiceParameterFull param
       , HasSideEffects
       )
    => L.Contract param st
    -> Expr (Maybe KeyHash)
    -> Expr Mutez
    -> Expr st
    -> StatementF freer (Var Address)
  SelfCalling
    :: ( NiceParameterFull p
       , KnownValue (GetEntrypointArgCustom p mname)
       )
    => Proxy p
    -> EntrypointRef mname
    -> StatementF freer (Var (ContractRef (GetEntrypointArgCustom p mname)))
  ContractCalling
    :: ( HasEntrypointArg cp epRef epArg
       , ToTAddress cp addr
       , ToT addr ~ ToT Address
       , KnownValue epArg
       )
    => Proxy cp -> epRef -> Expr addr -> StatementF freer (Var (Maybe (ContractRef epArg)))

  -- Generic failing statements, hardly more than 'LiftIndigoState', but with the
  -- knowledge that they end in a failure.
  Fail
    :: ReturnableValue ret
    => Proxy ret
    -> (forall inp. SomeIndigoState inp)
    -> StatementF freer (RetVars ret)
  FailOver
    :: ReturnableValue ret
    => Proxy ret
    -> (forall inp. Expr a -> SomeIndigoState inp)
    -> Expr a
    -> StatementF freer (RetVars ret)