-- 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
    /-> :: Label name
-> (Var x -> IndigoAnyOut x ret)
-> IndigoCaseClauseL ret ('CaseClauseParam ctor ('OneField x))
(/->) _ ind :: Var x -> IndigoAnyOut x ret
ind =
      (forall (inp :: [*]).
 MetaData inp
 -> CaseClauseL
      inp (RetOutStack ret ++ inp) ('CaseClauseParam ctor ('OneField x)))
-> IndigoCaseClauseL ret ('CaseClauseParam ctor ('OneField x))
forall ret (ctor :: Symbol) x.
(forall (inp :: [*]).
 MetaData inp
 -> CaseClauseL
      inp (RetOutStack ret ++ inp) ('CaseClauseParam ctor ('OneField x)))
-> IndigoCaseClauseL ret ('CaseClauseParam ctor ('OneField x))
OneFieldIndigoCaseClauseL (\(MetaData inp
md :: MetaData inp) ->
        -- Create a reference to the top of stack
        let (varCase :: Var x
varCase, mdCaseBody :: MetaData (x & inp)
mdCaseBody) = MetaData inp -> (Var x, MetaData (x & inp))
forall x (stk :: [*]).
KnownValue x =>
MetaData stk -> (Var x, MetaData (x & stk))
pushRefMd MetaData inp
md in
        -- Pass the reference to the case body
        case Var x -> IndigoAnyOut x ret
ind Var x
varCase of
          IndigoAnyOut (SomeIndigoState body :: SomeIndigoState (x : inp) retBr) ->
            case MetaData (x & inp) -> SomeGenCode (x & inp) retBranch
body MetaData (x & inp)
mdCaseBody of
              SomeGenCode gc :: GenCode (x & inp) out retBranch
gc ->
                (AppendCtorField ('OneField x) inp
 :-> (RetOutStack' (ClassifyReturnValue retBranch) retBranch
      ++ inp))
-> CaseClauseL
     inp (RetOutStack ret ++ inp) ('CaseClauseParam ctor ('OneField x))
forall (x :: CtorField) (inp :: [*]) (out :: [*]) (ctor :: Symbol).
(AppendCtorField x inp :-> out)
-> CaseClauseL inp out ('CaseClauseParam ctor x)
CaseClauseL ((AppendCtorField ('OneField x) inp
  :-> (RetOutStack' (ClassifyReturnValue retBranch) retBranch
       ++ inp))
 -> CaseClauseL
      inp (RetOutStack ret ++ inp) ('CaseClauseParam ctor ('OneField x)))
-> (AppendCtorField ('OneField x) inp
    :-> (RetOutStack' (ClassifyReturnValue retBranch) retBranch
         ++ inp))
-> CaseClauseL
     inp (RetOutStack ret ++ inp) ('CaseClauseParam ctor ('OneField x))
forall a b. (a -> b) -> a -> b
$
                  -- Compute returning expressions and clean up everything
                  GenCode (x & inp) out retBranch
-> (x & inp)
   :-> (RetOutStack' (ClassifyReturnValue retBranch) retBranch
        ++ (x & inp))
forall ret (inp :: [*]) (xs :: [*]).
ScopeCodeGen ret =>
GenCode inp xs ret -> inp :-> (RetOutStack ret ++ inp)
compileScope GenCode (x & inp) out retBranch
gc ((x & inp)
 :-> (RetOutStack' (ClassifyReturnValue retBranch) retBranch
      ++ (x & inp)))
-> ((RetOutStack' (ClassifyReturnValue retBranch) retBranch
     ++ (x & inp))
    :-> (RetOutStack' (ClassifyReturnValue retBranch) retBranch
         ++ inp))
-> (x & inp)
   :-> (RetOutStack' (ClassifyReturnValue retBranch) retBranch ++ inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
                  -- Remove @x@ from the stack too
                  ((x & inp) :-> inp)
-> (RetOutStack' (ClassifyReturnValue retBranch) retBranch
    ++ (x & inp))
   :-> (RetOutStack' (ClassifyReturnValue retBranch) retBranch ++ inp)
forall (retKind :: BranchRetKind) ret (xs :: [*]) (inp :: [*]).
ScopeCodeGen' retKind ret =>
(xs :-> inp)
-> (RetOutStack' retKind ret ++ xs)
   :-> (RetOutStack' retKind ret ++ inp)
liftClear' @(ClassifyReturnValue retBr) @retBr @(x & inp) @inp (x & inp) :-> inp
forall a (s :: [*]). (a & s) :-> s
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 :: Expr dt
-> clauses
-> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret)
caseRec g :: Expr dt
g cls :: clauses
cls = (MetaData inp
 -> GenCode inp (RetOutStack ret ++ inp) (RetVars ret))
-> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret)
forall (inp :: [*]) (out :: [*]) a.
(MetaData inp -> GenCode inp out a) -> IndigoState inp out a
IndigoState ((MetaData inp
  -> GenCode inp (RetOutStack ret ++ inp) (RetVars ret))
 -> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret))
-> (MetaData inp
    -> GenCode inp (RetOutStack ret ++ inp) (RetVars ret))
-> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret)
forall a b. (a -> b) -> a -> b
$ \md :: MetaData inp
md ->
  let cdG :: inp :-> (dt & inp)
cdG = GenCode inp (dt & inp) () -> inp :-> (dt & inp)
forall (inp :: [*]) (out :: [*]) a.
GenCode inp out a -> inp :-> out
gcCode (GenCode inp (dt & inp) () -> inp :-> (dt & inp))
-> GenCode inp (dt & inp) () -> inp :-> (dt & inp)
forall a b. (a -> b) -> a -> b
$ IndigoState inp (dt & inp) ()
-> MetaData inp -> GenCode inp (dt & inp) ()
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState (Expr dt -> IndigoState inp (dt & inp) ()
forall a (inp :: [*]). Expr a -> IndigoState inp (a & inp) ()
compileExpr Expr dt
g) MetaData inp
md in
  MetaData inp
-> (inp :-> (RetOutStack ret ++ inp))
-> GenCode inp (RetOutStack ret ++ inp) (RetVars ret)
forall ret (inp :: [*]).
ScopeCodeGen ret =>
MetaData inp
-> (inp :-> (RetOutStack ret ++ inp))
-> GenCode inp (RetOutStack ret ++ inp) (RetVars ret)
finalizeStatement @ret MetaData inp
md (inp :-> (dt & inp)
cdG (inp :-> (dt & inp))
-> ((dt & inp) :-> (RetOutStack ret ++ inp))
-> inp :-> (RetOutStack ret ++ inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Rec (CaseClauseL inp (RetOutStack ret ++ inp)) (CaseClauses dt)
-> (dt & inp) :-> (RetOutStack ret ++ inp)
forall dt (out :: [*]) (inp :: [*]).
(InstrCaseC dt, RMap (CaseClauses dt)) =>
Rec (CaseClauseL inp out) (CaseClauses dt) -> (dt & inp) :-> out
L.case_ (MetaData inp
-> Rec (IndigoCaseClauseL ret) (CaseClauses dt)
-> Rec (CaseClauseL inp (RetOutStack ret ++ inp)) (CaseClauses dt)
forall (inp :: [*]) ret (cs :: [CaseClauseParam]).
MetaData inp
-> Rec (IndigoCaseClauseL ret) cs
-> Rec (CaseClauseL inp (RetOutStack ret ++ inp)) cs
toCaseClauseL MetaData inp
md clauses
Rec (IndigoCaseClauseL ret) (CaseClauses dt)
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 entrypointKind
-> Expr dt
-> clauses
-> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret)
entryCaseRec proxy :: Proxy entrypointKind
proxy g :: Expr dt
g cls :: clauses
cls = (MetaData inp
 -> GenCode inp (RetOutStack ret ++ inp) (RetVars ret))
-> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret)
forall (inp :: [*]) (out :: [*]) a.
(MetaData inp -> GenCode inp out a) -> IndigoState inp out a
IndigoState ((MetaData inp
  -> GenCode inp (RetOutStack ret ++ inp) (RetVars ret))
 -> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret))
-> (MetaData inp
    -> GenCode inp (RetOutStack ret ++ inp) (RetVars ret))
-> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret)
forall a b. (a -> b) -> a -> b
$ \md :: MetaData inp
md ->
  let cdG :: inp :-> (dt & inp)
cdG = GenCode inp (dt & inp) () -> inp :-> (dt & inp)
forall (inp :: [*]) (out :: [*]) a.
GenCode inp out a -> inp :-> out
gcCode (GenCode inp (dt & inp) () -> inp :-> (dt & inp))
-> GenCode inp (dt & inp) () -> inp :-> (dt & inp)
forall a b. (a -> b) -> a -> b
$ IndigoState inp (dt & inp) ()
-> MetaData inp -> GenCode inp (dt & inp) ()
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState (Expr dt -> IndigoState inp (dt & inp) ()
forall a (inp :: [*]). Expr a -> IndigoState inp (a & inp) ()
compileExpr Expr dt
g) MetaData inp
md in
  MetaData inp
-> (inp :-> (RetOutStack ret ++ inp))
-> GenCode inp (RetOutStack ret ++ inp) (RetVars ret)
forall ret (inp :: [*]).
ScopeCodeGen ret =>
MetaData inp
-> (inp :-> (RetOutStack ret ++ inp))
-> GenCode inp (RetOutStack ret ++ inp) (RetVars ret)
finalizeStatement @ret MetaData inp
md (inp :-> (dt & inp)
cdG (inp :-> (dt & inp))
-> ((dt & inp) :-> (RetOutStack ret ++ inp))
-> inp :-> (RetOutStack ret ++ inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Proxy entrypointKind
-> Rec (CaseClauseL inp (RetOutStack ret ++ inp)) (CaseClauses dt)
-> (dt & inp) :-> (RetOutStack ret ++ inp)
forall dt entrypointKind (out :: [*]) (inp :: [*]).
(InstrCaseC dt, RMap (CaseClauses dt),
 DocumentEntrypoints entrypointKind dt) =>
Proxy entrypointKind
-> Rec (CaseClauseL inp out) (CaseClauses dt) -> (dt & inp) :-> out
L.entryCase_ Proxy entrypointKind
proxy (MetaData inp
-> Rec (IndigoCaseClauseL ret) (CaseClauses dt)
-> Rec (CaseClauseL inp (RetOutStack ret ++ inp)) (CaseClauses dt)
forall (inp :: [*]) ret (cs :: [CaseClauseParam]).
MetaData inp
-> Rec (IndigoCaseClauseL ret) cs
-> Rec (CaseClauseL inp (RetOutStack ret ++ inp)) cs
toCaseClauseL MetaData inp
md clauses
Rec (IndigoCaseClauseL ret) (CaseClauses dt)
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 :: Expr cp
-> clauses
-> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret)
entryCaseSimpleRec g :: Expr cp
g cls :: clauses
cls = (MetaData inp
 -> GenCode inp (RetOutStack ret ++ inp) (RetVars ret))
-> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret)
forall (inp :: [*]) (out :: [*]) a.
(MetaData inp -> GenCode inp out a) -> IndigoState inp out a
IndigoState ((MetaData inp
  -> GenCode inp (RetOutStack ret ++ inp) (RetVars ret))
 -> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret))
-> (MetaData inp
    -> GenCode inp (RetOutStack ret ++ inp) (RetVars ret))
-> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret)
forall a b. (a -> b) -> a -> b
$ \md :: MetaData inp
md ->
  let cdG :: inp :-> (cp & inp)
cdG = GenCode inp (cp & inp) () -> inp :-> (cp & inp)
forall (inp :: [*]) (out :: [*]) a.
GenCode inp out a -> inp :-> out
gcCode (GenCode inp (cp & inp) () -> inp :-> (cp & inp))
-> GenCode inp (cp & inp) () -> inp :-> (cp & inp)
forall a b. (a -> b) -> a -> b
$ IndigoState inp (cp & inp) ()
-> MetaData inp -> GenCode inp (cp & inp) ()
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState (Expr cp -> IndigoState inp (cp & inp) ()
forall a (inp :: [*]). Expr a -> IndigoState inp (a & inp) ()
compileExpr Expr cp
g) MetaData inp
md in
  MetaData inp
-> (inp :-> (RetOutStack ret ++ inp))
-> GenCode inp (RetOutStack ret ++ inp) (RetVars ret)
forall ret (inp :: [*]).
ScopeCodeGen ret =>
MetaData inp
-> (inp :-> (RetOutStack ret ++ inp))
-> GenCode inp (RetOutStack ret ++ inp) (RetVars ret)
finalizeStatement @ret MetaData inp
md (inp :-> (cp & inp)
cdG (inp :-> (cp & inp))
-> ((cp & inp) :-> (RetOutStack ret ++ inp))
-> inp :-> (RetOutStack ret ++ inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Rec (CaseClauseL inp (RetOutStack ret ++ inp)) (CaseClauses cp)
-> (cp & inp) :-> (RetOutStack ret ++ inp)
forall cp (out :: [*]) (inp :: [*]).
(InstrCaseC cp, RMap (CaseClauses cp),
 DocumentEntrypoints PlainEntrypointsKind cp, NiceParameterFull cp,
 RequireFlatParamEps cp) =>
Rec (CaseClauseL inp out) (CaseClauses cp) -> (cp & inp) :-> out
L.entryCaseSimple_ (MetaData inp
-> Rec (IndigoCaseClauseL ret) (CaseClauses cp)
-> Rec (CaseClauseL inp (RetOutStack ret ++ inp)) (CaseClauses cp)
forall (inp :: [*]) ret (cs :: [CaseClauseParam]).
MetaData inp
-> Rec (IndigoCaseClauseL ret) cs
-> Rec (CaseClauseL inp (RetOutStack ret ++ inp)) cs
toCaseClauseL MetaData inp
md clauses
Rec (IndigoCaseClauseL ret) (CaseClauses cp)
cls))

toCaseClauseL
  :: forall inp ret cs .
     MetaData inp
  -> Rec (IndigoCaseClauseL ret) cs
  -> Rec (CaseClauseL inp (RetOutStack ret ++ inp)) cs
toCaseClauseL :: MetaData inp
-> Rec (IndigoCaseClauseL ret) cs
-> Rec (CaseClauseL inp (RetOutStack ret ++ inp)) cs
toCaseClauseL _ RNil = Rec (CaseClauseL inp (RetOutStack ret ++ inp)) cs
forall u (a :: u -> *). Rec a '[]
RNil
toCaseClauseL md :: MetaData inp
md (OneFieldIndigoCaseClauseL fn :: forall (inp :: [*]).
MetaData inp
-> CaseClauseL
     inp (RetOutStack ret ++ inp) ('CaseClauseParam ctor ('OneField x))
fn :& rest :: Rec (IndigoCaseClauseL ret) rs
rest) = MetaData inp
-> CaseClauseL
     inp (RetOutStack ret ++ inp) ('CaseClauseParam ctor ('OneField x))
forall (inp :: [*]).
MetaData inp
-> CaseClauseL
     inp (RetOutStack ret ++ inp) ('CaseClauseParam ctor ('OneField x))
fn MetaData inp
md CaseClauseL
  inp (RetOutStack ret ++ inp) ('CaseClauseParam ctor ('OneField x))
-> Rec (CaseClauseL inp (RetOutStack ret ++ inp)) rs
-> Rec
     (CaseClauseL inp (RetOutStack ret ++ inp))
     ('CaseClauseParam ctor ('OneField x) : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& MetaData inp
-> Rec (IndigoCaseClauseL ret) rs
-> Rec (CaseClauseL inp (RetOutStack ret ++ inp)) rs
forall (inp :: [*]) ret (cs :: [CaseClauseParam]).
MetaData inp
-> Rec (IndigoCaseClauseL ret) cs
-> Rec (CaseClauseL inp (RetOutStack ret ++ inp)) cs
toCaseClauseL MetaData inp
md Rec (IndigoCaseClauseL ret) rs
rest