-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

-- | 'StatementF' functor datatype for Freer monad
--
-- This defines the AST of the syntactical constructs of
-- Indigo.
--
-- Despite being a part of the "front-end", this module is considered internal
-- implementation detail. It's not intended to be used by the end-user and hence
-- is not re-exported.
module Indigo.Frontend.Internal.Statement
  ( StatementF (..)

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

import Data.Kind qualified as Kind

import Lorentz.Entrypoints.Helpers (RequireSumType)
import Lorentz.Run qualified as L (Contract)
import Morley.Michelson.Typed.Haskell.Instr.Sum (CaseClauseParam(..), CtorField(..))
import Morley.Michelson.Untyped.Annotation (FieldAnn)
import Morley.Util.TypeLits (AppendSymbol)

import Indigo.Backend.Case (CaseCommonF)
import Indigo.Backend.Conditional (IfConstraint)
import Indigo.Backend.Lambda (LambdaKind(..), withLambdaKind)
import Indigo.Backend.Scope (RetExprs, RetOutStack, RetVars, ReturnableValue, ScopeCodeGen)
import Indigo.Common.Expr (Expr)
import Indigo.Common.Field (HasField)
import Indigo.Common.Object (IsObject)
import Indigo.Common.SIS (SomeIndigoState)
import Indigo.Common.Var (HasSideEffects, Var)
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 ()

  -- | Constructor wrapper which holds 'IndigoM' function
  -- among with the callstack of caller side.
  --
  -- The another option could be to add `HasCallStack` to 'Instr' constructor of 'Program'
  -- but this would have held only a 'CallStack' of separate primitive statement (unlike 'updateStorageField', etc).
  -- The idea is to be able to have correspondence between original Indigo code
  -- and the generated Michelson assembler and vice versa to perform quick navigation and analyze,
  -- so it's better to have call stack for non-primitive frontend statements.
  CalledFrom :: CallStack -> freer a -> StatementF freer a

  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
    :: DocItem di
    => (SubDoc -> di) -> freer () -> StatementF freer ()
  ContractGeneral :: freer () -> StatementF freer ()
  FinalizeParamCallingDoc
    :: (NiceParameterFull cp, RequireSumType cp, HasCallStack)
    => (Var cp -> freer ()) -> Expr cp -> StatementF freer ()

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

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

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