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

-- | 'StatementF' functor datatype for Freer monad

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

  , IfConstraint
  , IndigoMCaseClauseL (..)
  ) 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 :: (ex :~> x) => ex -> StatementF freer (Var x)
  SetVar :: (ex :~> x, IsObject x) => Var x -> ex -> StatementF freer ()
  VarModification
    :: (ey :~> y, IsObject x)
    => [y, x] :-> '[x]
    -> Var x
    -> ey
    -> StatementF freer ()
  SetField ::
    ( ex :~> ftype
    , IsObject dt
    , IsObject ftype
    , HasField dt fname ftype
    )
    => Var dt -> Label fname -> ex -> 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, ex :~> Bool)
     => ex
     -> freer a
     -> freer b
     -> StatementF freer (RetVars a)
  IfSome :: (IfConstraint a b, KnownValue x, ex :~> Maybe x)
     => ex
     -> (Var x -> freer a)
     -> freer b
     -> StatementF freer (RetVars a)
  IfRight
     :: (IfConstraint a b, KnownValue x, KnownValue y, ex :~> Either y x)
     => ex
     -> (Var x -> freer a)
     -> (Var y -> freer b)
     -> StatementF freer (RetVars a)
  IfCons
     :: (IfConstraint a b, KnownValue x, ex :~> (List x) )
     => ex
     -> (Var x -> Var (List x) -> freer a)
     -> freer b
     -> StatementF freer (RetVars a)
  Case :: CaseCommonF (IndigoMCaseClauseL freer) dt guard ret clauses
       => guard -> clauses
       -> StatementF freer (RetVars ret)
  EntryCase ::
    ( CaseCommonF (IndigoMCaseClauseL freer) dt guard ret clauses
    , DocumentEntryPoints entryPointKind dt
    )
    => Proxy entryPointKind
    -> guard
    -> clauses
    -> StatementF freer (RetVars ret)
  EntryCaseSimple ::
         ( CaseCommonF (IndigoMCaseClauseL freer) cp guard ret clauses
         , DocumentEntryPoints PlainEntryPointsKind cp
         , NiceParameterFull cp
         , RequireFlatParamEps cp
         )
      => guard
      -> clauses
      -> StatementF freer (RetVars ret)

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

  ContractName :: Text        -> freer () -> StatementF freer ()
  DocGroup     :: DocGrouping -> freer () -> StatementF freer ()
  ContractGeneral :: freer () -> StatementF freer ()
  FinalizeParamCallingDoc
    :: (ToExpr param, NiceParameterFull (ExprType param), RequireSumType (ExprType param), HasCallStack)
    => (Var (ExprType param) -> freer x) -> param -> StatementF freer x

  TransferTokens
    :: (exp :~> p, exm :~> Mutez, exc :~> ContractRef p, NiceParameter p, HasSideEffects)
    => exp -> exm -> exc -> StatementF freer ()
  SetDelegate :: (HasSideEffects, ex :~> Maybe KeyHash) => ex -> StatementF freer ()

  CreateContract ::
    ( IsObject st
    , exk :~> Maybe KeyHash, exm :~> Mutez, exs :~> st
    , NiceStorage st, NiceParameterFull param
    , HasSideEffects
    )
    => L.Contract param st
    -> exk
    -> exm
    -> exs
    -> StatementF freer (Var Address)
  ContractCalling ::
     ( HasEntryPointArg cp epRef epArg
     , ToTAddress cp addr
     , ToT addr ~ ToT Address
     , exAddr :~> addr
     , KnownValue epArg
     )
     => Proxy cp -> epRef -> exAddr -> StatementF freer (Var (Maybe (ContractRef epArg)))

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