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

-- | 'StatementF' functor datatype for Freer monad

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

  , IfConstraint
  , IndigoMCaseClauseL (..)
  , CaseCommonF
  ) 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.Prelude
import Indigo.Lorentz
import Indigo.Internal
import Indigo.Backend

-- | Analogous datatype as IndigoCaseClauseL from Indigo.Backend.Case
data IndigoMCaseClauseL freer ret (param :: CaseClauseParam) where
    OneFieldIndigoMCaseClauseL
      :: ( CaseArrow name
                     (Var x -> IndigoAnyOut x ret)
                     (IndigoCaseClauseL ret ('CaseClauseParam ctor ('OneField x)))
         , 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 a) -> StatementF freer a

  NewVar :: KnownValue x => Expr x -> StatementF freer (Var x)
  SetVar :: 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 ()

  -- | Pure lambda
  LambdaPure1Call
    :: (ExecuteLambdaPure1C arg res, CreateLambdaPure1C arg res, Typeable res)
    => String
    -> (Var arg -> freer res)
    -> Expr arg
    -> StatementF freer (RetVars res)

  -- | "Default" lambda which can modify storage
  Lambda1Call
    :: (ExecuteLambda1C st arg res, CreateLambda1C st arg res, Typeable res)
    => Proxy st
    -> String
    -> (Var arg -> freer res)
    -> Expr arg
    -> StatementF freer (RetVars res)

  -- | Lambda which can modify storage and emit operations
  LambdaEff1Call
    :: (ExecuteLambdaEff1C st arg res, CreateLambdaEff1C st arg res, Typeable res)
    => Proxy st
    -> 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 x) -> Expr cp -> StatementF freer x

  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)
  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)))

  FailWith :: KnownValue a => Expr a -> StatementF freer r
  Assert :: IsError x => x -> Expr Bool -> StatementF freer ()
  FailCustom
    :: ( err ~ ErrorArg tag
       , CustomErrorHasDoc tag
       , NiceConstant err
       )
    => Label tag -> Expr err -> StatementF freer r