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

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

import Data.Singletons (Sing)
import Data.Typeable ((:~:)(..), eqT)

import Indigo.Backend.Prelude
import Indigo.Frontend.Program (IndigoM)
import Indigo.Internal.Object
import Indigo.Internal.State
import Indigo.Lorentz
import Util.Peano

----------------------------------------------------------------------------
-- Utility for compatibility with Lorentz
----------------------------------------------------------------------------

-- | 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 (\'S (\'S \'Z)) \'[a, b, c] x@ is the same as:
-- @Var b -> Var a -> IndigoM x@
type family IndigoWithParams n inp a where
  IndigoWithParams 'Z _ a = IndigoM a
  IndigoWithParams ('S n) inp a = Var (At n inp) -> IndigoWithParams n inp a

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

-- | Converts an 'IndigoWithParams' to its form without input 'Var's, alongside
-- the 'MetaData' to use it with.
-- If there is an 'Ops' to the bottom of the stack it also assigns a 'Var' to it.
fromIndigoWithParams
  :: forall inp n a . (AreIndigoParams n inp, KnownValue a)
  => IndigoWithParams n inp a
  -> MetaData inp
  -> Sing n
  -> (IndigoM a, MetaData inp)
fromIndigoWithParams :: IndigoWithParams n inp a
-> MetaData inp -> Sing n -> (IndigoM a, MetaData inp)
fromIndigoWithParams code :: IndigoWithParams n inp a
code md :: MetaData inp
md = \case
  SZ -> (IndigoM a
IndigoWithParams n inp a
code, MetaData inp -> MetaData inp
forall (inp :: [*]). MetaData inp -> MetaData inp
assignVarToOps MetaData inp
md)
  SS n -> let (md2 :: MetaData inp
md2, var :: Var (At n1 inp)
var) = MetaData inp -> Sing n1 -> (MetaData inp, Var (At n1 inp))
forall a (n :: Nat) (inp :: [*]).
(KnownValue a, a ~ At n inp, RequireLongerThan inp n) =>
MetaData inp -> Sing n -> (MetaData inp, Var a)
withVarAt MetaData inp
md SingNat n1
Sing n1
n in IndigoWithParams n1 inp a
-> MetaData inp -> Sing n1 -> (IndigoM a, MetaData inp)
forall (inp :: [*]) (n :: Nat) a.
(AreIndigoParams n inp, KnownValue a) =>
IndigoWithParams n inp a
-> MetaData inp -> Sing n -> (IndigoM a, MetaData inp)
fromIndigoWithParams @inp (IndigoWithParams n inp a
Var (At n1 inp) -> IndigoWithParams n1 inp a
code Var (At n1 inp)
var) MetaData inp
md2 SingNat n1
Sing n1
n

-- | Assigns a variable to the 'Ops' list at the bottom of the stack iff there is
-- one and it does not have one already. Otherwise returns the same 'MetaData'.
assignVarToOps :: MetaData inp -> MetaData inp
assignVarToOps :: MetaData inp -> MetaData inp
assignVarToOps md :: MetaData inp
md@(MetaData stk :: StackVars inp
stk vRef :: RefId
vRef) = case StackVars inp
stk of
  RNil -> MetaData inp
md
  (_ :& RNil) -> MetaData '[r] -> MetaData '[r]
forall x. MetaData '[x] -> MetaData '[x]
assingVarIfOps MetaData inp
MetaData '[r]
md
  (x :: StkEl r
x :& xs :: Rec StkEl rs
xs) -> case MetaData rs -> MetaData rs
forall (inp :: [*]). MetaData inp -> MetaData inp
assignVarToOps (MetaData rs -> MetaData rs) -> MetaData rs -> MetaData rs
forall a b. (a -> b) -> a -> b
$ Rec StkEl rs -> RefId -> MetaData rs
forall (stk :: [*]). StackVars stk -> RefId -> MetaData stk
MetaData Rec StkEl rs
xs RefId
vRef of
    MetaData xs' :: Rec StkEl rs
xs' vRef' :: RefId
vRef' -> StackVars (r : rs) -> RefId -> MetaData (r : rs)
forall (stk :: [*]). StackVars stk -> RefId -> MetaData stk
MetaData (StkEl r
x StkEl r -> Rec StkEl rs -> StackVars (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
xs') RefId
vRef'

assingVarIfOps :: forall x. MetaData '[x] -> MetaData '[x]
assingVarIfOps :: MetaData '[x] -> MetaData '[x]
assingVarIfOps md :: MetaData '[x]
md@(MetaData stk :: StackVars '[x]
stk vRef :: RefId
vRef) = case StackVars '[x]
stk of
  (Ref _ :& RNil) -> MetaData '[x]
md
  ((NoRef :: StkEl x) :& RNil) -> case (Typeable x, Typeable Ops) => Maybe (x :~: Ops)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @x @Ops of
    Nothing -> MetaData '[x]
md
    Just Refl -> StackVars '[x] -> RefId -> MetaData '[x]
forall (stk :: [*]). StackVars stk -> RefId -> MetaData stk
MetaData (RefId -> StkEl x
forall a. KnownValue a => RefId -> StkEl a
Ref RefId
vRef StkEl x -> Rec StkEl '[] -> StackVars '[x]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl '[]
forall u (a :: u -> *). Rec a '[]
RNil) (RefId
vRef RefId -> RefId -> RefId
forall a. Num a => a -> a -> a
+ 1)