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

module Indigo.Compilation.Params
  ( IndigoWithParams
  , AreIndigoParams
  , fromIndigoWithParams
  , contractToIndigoWithParams
  ) where

import Data.Reflection (give)
import Data.Singletons (Sing, SingI(..))

import Indigo.Backend.Prelude
import Indigo.Frontend.Program (IndigoM, IndigoContract)
import Indigo.Internal.Var
import Indigo.Lorentz
import Util.Peano

-- | Type of a function with @n@ 'Var' arguments and @IndigoM a@ result.
--
-- Note that the arguments are the first @n@ elements of the @inp@ stack in
-- inverse order, for example:
-- @IndigoWithParams 2 [a, b, c] x@ is the same as:
-- @Var b -> Var a -> IndigoM x@
type IndigoWithParams n inp a = IndigoWithPeanoParams (ToPeano n) inp a

-- | Typeable and stack size constraints for the parameters of an 'IndigoWithParams'
-- and for converting to a 'Peano'
type AreIndigoParams n stk =
  ( AreIndigoPeanoParams (ToPeano n) stk
  , SingI (ToPeano n)
  )

-- | 'Peano' equivalent of 'IndigoWithParams'
type family IndigoWithPeanoParams n inp a where
  IndigoWithPeanoParams 'Z _ a = IndigoM a
  IndigoWithPeanoParams ('S n) inp a = Var (At n inp) -> IndigoWithPeanoParams n inp a

-- | Typeable and stack size constraints for the parameters of an 'IndigoWithPeanoParams'.
type family AreIndigoPeanoParams n stk :: Constraint where
  AreIndigoPeanoParams 'Z _ = (() :: Constraint)
  AreIndigoPeanoParams ('S n) stk =
    (KnownValue (At n stk), RequireLongerThan stk n, AreIndigoPeanoParams n stk)

-- | Converts an 'IndigoWithParams' to its form without input 'Var's, alongside
-- the 'StackVars' to use it with and the first available (unassingned) 'RefId'.
fromIndigoWithParams
  :: forall n a inp.
     (AreIndigoParams n inp, KnownValue a, Default (StackVars inp))
  => IndigoWithParams n inp a
  -> (IndigoM a, StackVars inp, RefId)
fromIndigoWithParams :: IndigoWithParams n inp a -> (IndigoM a, StackVars inp, RefId)
fromIndigoWithParams code :: IndigoWithParams n inp a
code = RefId
-> StackVars inp
-> IndigoWithParams n inp a
-> Sing (ToPeano n)
-> (IndigoM a, StackVars inp, RefId)
forall (inp :: [*]) (n :: Nat) a.
(AreIndigoPeanoParams n inp, KnownValue a) =>
RefId
-> StackVars inp
-> IndigoWithPeanoParams n inp a
-> Sing n
-> (IndigoM a, StackVars inp, RefId)
fromIndigoWithPeanoParams RefId
forall a. Bounded a => a
minBound StackVars inp
forall a. Default a => a
def IndigoWithParams n inp a
code (SingI (ToPeano n) => Sing (ToPeano n)
forall k (a :: k). SingI a => Sing a
sing @(ToPeano n))

-- | 'Peano' version of 'fromIndigoWithParams'
fromIndigoWithPeanoParams
  :: forall inp n a. (AreIndigoPeanoParams n inp, KnownValue a)
  => RefId
  -> StackVars inp
  -> IndigoWithPeanoParams n inp a
  -> Sing n
  -> (IndigoM a, StackVars inp, RefId)
fromIndigoWithPeanoParams :: RefId
-> StackVars inp
-> IndigoWithPeanoParams n inp a
-> Sing n
-> (IndigoM a, StackVars inp, RefId)
fromIndigoWithPeanoParams ref :: RefId
ref md :: StackVars inp
md code :: IndigoWithPeanoParams n inp a
code = \case
  SZ -> (IndigoM a
IndigoWithPeanoParams n inp a
code, StackVars inp
md, RefId
ref)
  SS n -> let var :: Var (At n1 inp)
var = RefId -> Var (At n1 inp)
forall k (a :: k). RefId -> Var a
Var RefId
ref in
    RefId
-> StackVars inp
-> IndigoWithPeanoParams n1 inp a
-> Sing n1
-> (IndigoM a, StackVars inp, RefId)
forall (inp :: [*]) (n :: Nat) a.
(AreIndigoPeanoParams n inp, KnownValue a) =>
RefId
-> StackVars inp
-> IndigoWithPeanoParams n inp a
-> Sing n
-> (IndigoM a, StackVars inp, RefId)
fromIndigoWithPeanoParams @inp (RefId
ref RefId -> RefId -> RefId
forall a. Num a => a -> a -> a
+ 1) (Var (At n1 inp) -> StackVars inp -> Sing n1 -> StackVars inp
forall a (n :: Nat) (inp :: [*]).
(KnownValue a, a ~ At n inp, RequireLongerThan inp n) =>
Var a -> StackVars inp -> Sing n -> StackVars inp
assignVarAt Var (At n1 inp)
var StackVars inp
md Sing n1
SingNat n1
n) (IndigoWithPeanoParams n inp a
Var (At n1 inp) -> IndigoWithPeanoParams n1 inp a
code Var (At n1 inp)
var) Sing n1
SingNat n1
n

-- | Converts an 'IndigoContract' to the equivalent 'IndigoM' with the storage,
-- parameter and ops list as arguments.
contractToIndigoWithParams
  :: forall param st . KnownValue st
  => IndigoContract param st
  -> IndigoWithParams 3 '[param, st, Ops] ()
contractToIndigoWithParams :: IndigoContract param st -> IndigoWithParams 3 '[param, st, Ops] ()
contractToIndigoWithParams code :: IndigoContract param st
code = \varOps :: Var Ops
varOps varSt :: Var st
varSt varParam :: Var param
varParam ->
  (Var Ops
-> (Given (Var Ops) => Var param -> IndigoM ())
-> Var param
-> IndigoM ()
forall a r. a -> (Given a => r) -> r
give Var Ops
varOps ((Given (Var Ops) => Var param -> IndigoM ())
 -> Var param -> IndigoM ())
-> (Given (Var Ops) => Var param -> IndigoM ())
-> Var param
-> IndigoM ()
forall a b. (a -> b) -> a -> b
$ Var st
-> (Given (Var st) => Var param -> IndigoM ())
-> Var param
-> IndigoM ()
forall a r. a -> (Given a => r) -> r
give Var st
varSt IndigoContract param st
Given (Var st) => Var param -> IndigoM ()
code) Var param
varParam