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

{-# LANGUAGE InstanceSigs #-}

{- |
This module contains the core of Indigo language:
the 'IndigoState' monad, a datatype that represents its state.
It also includes some convenient functions to work with the state in IndigoM,
to provide rebindable syntax.

The 'IndigoState' monad implements the functionality of a symbolic interpreter.
During its execution Lorentz code is being generated.
-}

module Indigo.Internal.State
  ( -- * Indigo State
    IndigoState (..)
  , usingIndigoState
  , (>>=)
  , (=<<)
  , (>>)
  , (<$>)
  , return
  , iget
  , iput

  , RefId
  , StkEl (..)
  , StackVars
  , GenCode (..)
  , MetaData (..)
  , emptyMetadata
  , cleanGenCode
  , DefaultStack
  ) where

import qualified Data.Kind as Kind
import Data.Type.Equality (TestEquality(..))
import Data.Typeable (eqT)

import Indigo.Backend.Prelude
import Indigo.Lorentz
import qualified Lorentz.Instr as L

{-# ANN module ("HLint: ignore Reduce duplication" :: Text) #-}

----------------------------------------------------------------------------
-- Indigo State
----------------------------------------------------------------------------

-- | IndigoState monad. It's basically
-- [Control.Monad.Indexed.State](https://hackage.haskell.org/package/category-extras-0.53.5/docs/Control-Monad-Indexed-State.html)
-- , however this package is not in the used lts and it doesn't compile.
--
-- It takes as input a 'MetaData' (for the initial state) and returns a
-- 'GenCode' (for the resulting state and the generated Lorentz code).
--
-- IndigoState has to be used to write backend typed Lorentz code
-- from the corresponding frontend constructions.
newtype IndigoState inp out a =
  IndigoState {IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState :: MetaData inp -> GenCode inp out a}
  deriving stock a -> IndigoState inp out b -> IndigoState inp out a
(a -> b) -> IndigoState inp out a -> IndigoState inp out b
(forall a b.
 (a -> b) -> IndigoState inp out a -> IndigoState inp out b)
-> (forall a b.
    a -> IndigoState inp out b -> IndigoState inp out a)
-> Functor (IndigoState inp out)
forall (inp :: [*]) (out :: [*]) a b.
a -> IndigoState inp out b -> IndigoState inp out a
forall (inp :: [*]) (out :: [*]) a b.
(a -> b) -> IndigoState inp out a -> IndigoState inp out b
forall a b. a -> IndigoState inp out b -> IndigoState inp out a
forall a b.
(a -> b) -> IndigoState inp out a -> IndigoState inp out b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> IndigoState inp out b -> IndigoState inp out a
$c<$ :: forall (inp :: [*]) (out :: [*]) a b.
a -> IndigoState inp out b -> IndigoState inp out a
fmap :: (a -> b) -> IndigoState inp out a -> IndigoState inp out b
$cfmap :: forall (inp :: [*]) (out :: [*]) a b.
(a -> b) -> IndigoState inp out a -> IndigoState inp out b
Functor

usingIndigoState :: MetaData inp -> IndigoState inp out a -> GenCode inp out a
usingIndigoState :: MetaData inp -> IndigoState inp out a -> GenCode inp out a
usingIndigoState = (IndigoState inp out a -> MetaData inp -> GenCode inp out a)
-> MetaData inp -> IndigoState inp out a -> GenCode inp out a
forall a b c. (a -> b -> c) -> b -> a -> c
flip IndigoState inp out a -> MetaData inp -> GenCode inp out a
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState

-- | Return for rebindable syntax.
return :: a -> IndigoState inp inp a
return :: a -> IndigoState inp inp a
return a :: a
a = (MetaData inp -> GenCode inp inp a) -> IndigoState inp inp a
forall (inp :: [*]) (out :: [*]) a.
(MetaData inp -> GenCode inp out a) -> IndigoState inp out a
IndigoState ((MetaData inp -> GenCode inp inp a) -> IndigoState inp inp a)
-> (MetaData inp -> GenCode inp inp a) -> IndigoState inp inp a
forall a b. (a -> b) -> a -> b
$ \md :: MetaData inp
md -> a
-> MetaData inp
-> (inp :-> inp)
-> (inp :-> inp)
-> GenCode inp inp a
forall (inp :: [*]) (out :: [*]) a.
a
-> MetaData out
-> (inp :-> out)
-> (out :-> inp)
-> GenCode inp out a
GenCode a
a MetaData inp
md inp :-> inp
forall (s :: [*]). s :-> s
L.nop inp :-> inp
forall (s :: [*]). s :-> s
L.nop

-- | Bind for rebindable syntax.
--
-- It's basically like the bind for the 'State' monad, but it also composes the
-- generated code from @m a@ and @a -> m b@.
(>>=) :: forall inp out out1 a b . IndigoState inp out a -> (a -> IndigoState out out1 b) -> IndigoState inp out1 b
>>= :: IndigoState inp out a
-> (a -> IndigoState out out1 b) -> IndigoState inp out1 b
(>>=) m :: IndigoState inp out a
m f :: a -> IndigoState out out1 b
f = (MetaData inp -> GenCode inp out1 b) -> IndigoState inp out1 b
forall (inp :: [*]) (out :: [*]) a.
(MetaData inp -> GenCode inp out a) -> IndigoState inp out a
IndigoState ((MetaData inp -> GenCode inp out1 b) -> IndigoState inp out1 b)
-> (MetaData inp -> GenCode inp out1 b) -> IndigoState inp out1 b
forall a b. (a -> b) -> a -> b
$ \md :: MetaData inp
md ->
  let GenCode a :: a
a md1 :: MetaData out
md1 cd1 :: inp :-> out
cd1 cl1 :: out :-> inp
cl1 = IndigoState inp out a -> MetaData inp -> GenCode inp out a
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState IndigoState inp out a
m MetaData inp
md in
  let GenCode b :: b
b md2 :: MetaData out1
md2 cd2 :: out :-> out1
cd2 cl2 :: out1 :-> out
cl2 = IndigoState out out1 b -> MetaData out -> GenCode out out1 b
forall (inp :: [*]) (out :: [*]) a.
IndigoState inp out a -> MetaData inp -> GenCode inp out a
runIndigoState (a -> IndigoState out out1 b
f a
a) MetaData out
md1 in
  b
-> MetaData out1
-> (inp :-> out1)
-> (out1 :-> inp)
-> GenCode inp out1 b
forall (inp :: [*]) (out :: [*]) a.
a
-> MetaData out
-> (inp :-> out)
-> (out :-> inp)
-> GenCode inp out a
GenCode b
b MetaData out1
md2 (inp :-> out
cd1 (inp :-> out) -> (out :-> out1) -> inp :-> out1
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
## out :-> out1
cd2) (out1 :-> out
cl2 (out1 :-> out) -> (out :-> inp) -> out1 :-> inp
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
## out :-> inp
cl1)

(=<<) :: (a -> IndigoState out out1 b) -> IndigoState inp out a -> IndigoState inp out1 b
=<< :: (a -> IndigoState out out1 b)
-> IndigoState inp out a -> IndigoState inp out1 b
(=<<) = (IndigoState inp out a
 -> (a -> IndigoState out out1 b) -> IndigoState inp out1 b)
-> (a -> IndigoState out out1 b)
-> IndigoState inp out a
-> IndigoState inp out1 b
forall a b c. (a -> b -> c) -> b -> a -> c
flip IndigoState inp out a
-> (a -> IndigoState out out1 b) -> IndigoState inp out1 b
forall (inp :: [*]) (out :: [*]) (out1 :: [*]) a b.
IndigoState inp out a
-> (a -> IndigoState out out1 b) -> IndigoState inp out1 b
(>>=)

-- | Then for rebindable syntax.
(>>) :: IndigoState inp out a -> IndigoState out out1 b -> IndigoState inp out1 b
>> :: IndigoState inp out a
-> IndigoState out out1 b -> IndigoState inp out1 b
(>>) a :: IndigoState inp out a
a b :: IndigoState out out1 b
b = IndigoState inp out a
a IndigoState inp out a
-> (a -> IndigoState out out1 b) -> IndigoState inp out1 b
forall (inp :: [*]) (out :: [*]) (out1 :: [*]) a b.
IndigoState inp out a
-> (a -> IndigoState out out1 b) -> IndigoState inp out1 b
>>= IndigoState out out1 b -> a -> IndigoState out out1 b
forall a b. a -> b -> a
const IndigoState out out1 b
b

-- | Get current 'MetaData'.
iget :: IndigoState inp inp (MetaData inp)
iget :: IndigoState inp inp (MetaData inp)
iget = (MetaData inp -> GenCode inp inp (MetaData inp))
-> IndigoState inp inp (MetaData inp)
forall (inp :: [*]) (out :: [*]) a.
(MetaData inp -> GenCode inp out a) -> IndigoState inp out a
IndigoState ((MetaData inp -> GenCode inp inp (MetaData inp))
 -> IndigoState inp inp (MetaData inp))
-> (MetaData inp -> GenCode inp inp (MetaData inp))
-> IndigoState inp inp (MetaData inp)
forall a b. (a -> b) -> a -> b
$ \md :: MetaData inp
md -> MetaData inp
-> MetaData inp
-> (inp :-> inp)
-> (inp :-> inp)
-> GenCode inp inp (MetaData inp)
forall (inp :: [*]) (out :: [*]) a.
a
-> MetaData out
-> (inp :-> out)
-> (out :-> inp)
-> GenCode inp out a
GenCode MetaData inp
md MetaData inp
md inp :-> inp
forall (s :: [*]). s :-> s
L.nop inp :-> inp
forall (s :: [*]). s :-> s
L.nop

-- | Put new 'GenCode'.
iput :: GenCode inp out a -> IndigoState inp out a
iput :: GenCode inp out a -> IndigoState inp out a
iput gc :: GenCode inp out a
gc = (MetaData inp -> GenCode inp out a) -> IndigoState inp out a
forall (inp :: [*]) (out :: [*]) a.
(MetaData inp -> GenCode inp out a) -> IndigoState inp out a
IndigoState ((MetaData inp -> GenCode inp out a) -> IndigoState inp out a)
-> (MetaData inp -> GenCode inp out a) -> IndigoState inp out a
forall a b. (a -> b) -> a -> b
$ \_ -> GenCode inp out a
gc

----------------------------------------------------------------------------
-- Indigo stack and code gen primitives
----------------------------------------------------------------------------

-- | Reference id to a stack cell
newtype RefId = RefId Word
  deriving stock (Int -> RefId -> ShowS
[RefId] -> ShowS
RefId -> String
(Int -> RefId -> ShowS)
-> (RefId -> String) -> ([RefId] -> ShowS) -> Show RefId
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RefId] -> ShowS
$cshowList :: [RefId] -> ShowS
show :: RefId -> String
$cshow :: RefId -> String
showsPrec :: Int -> RefId -> ShowS
$cshowsPrec :: Int -> RefId -> ShowS
Show, (forall x. RefId -> Rep RefId x)
-> (forall x. Rep RefId x -> RefId) -> Generic RefId
forall x. Rep RefId x -> RefId
forall x. RefId -> Rep RefId x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep RefId x -> RefId
$cfrom :: forall x. RefId -> Rep RefId x
Generic)
  deriving newtype (RefId -> RefId -> Bool
(RefId -> RefId -> Bool) -> (RefId -> RefId -> Bool) -> Eq RefId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RefId -> RefId -> Bool
$c/= :: RefId -> RefId -> Bool
== :: RefId -> RefId -> Bool
$c== :: RefId -> RefId -> Bool
Eq, Eq RefId
Eq RefId =>
(RefId -> RefId -> Ordering)
-> (RefId -> RefId -> Bool)
-> (RefId -> RefId -> Bool)
-> (RefId -> RefId -> Bool)
-> (RefId -> RefId -> Bool)
-> (RefId -> RefId -> RefId)
-> (RefId -> RefId -> RefId)
-> Ord RefId
RefId -> RefId -> Bool
RefId -> RefId -> Ordering
RefId -> RefId -> RefId
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: RefId -> RefId -> RefId
$cmin :: RefId -> RefId -> RefId
max :: RefId -> RefId -> RefId
$cmax :: RefId -> RefId -> RefId
>= :: RefId -> RefId -> Bool
$c>= :: RefId -> RefId -> Bool
> :: RefId -> RefId -> Bool
$c> :: RefId -> RefId -> Bool
<= :: RefId -> RefId -> Bool
$c<= :: RefId -> RefId -> Bool
< :: RefId -> RefId -> Bool
$c< :: RefId -> RefId -> Bool
compare :: RefId -> RefId -> Ordering
$ccompare :: RefId -> RefId -> Ordering
$cp1Ord :: Eq RefId
Ord, Num RefId
Ord RefId
(Num RefId, Ord RefId) => (RefId -> Rational) -> Real RefId
RefId -> Rational
forall a. (Num a, Ord a) => (a -> Rational) -> Real a
toRational :: RefId -> Rational
$ctoRational :: RefId -> Rational
$cp2Real :: Ord RefId
$cp1Real :: Num RefId
Real, Integer -> RefId
RefId -> RefId
RefId -> RefId -> RefId
(RefId -> RefId -> RefId)
-> (RefId -> RefId -> RefId)
-> (RefId -> RefId -> RefId)
-> (RefId -> RefId)
-> (RefId -> RefId)
-> (RefId -> RefId)
-> (Integer -> RefId)
-> Num RefId
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> RefId
$cfromInteger :: Integer -> RefId
signum :: RefId -> RefId
$csignum :: RefId -> RefId
abs :: RefId -> RefId
$cabs :: RefId -> RefId
negate :: RefId -> RefId
$cnegate :: RefId -> RefId
* :: RefId -> RefId -> RefId
$c* :: RefId -> RefId -> RefId
- :: RefId -> RefId -> RefId
$c- :: RefId -> RefId -> RefId
+ :: RefId -> RefId -> RefId
$c+ :: RefId -> RefId -> RefId
Num)

-- | Stack element of the symbolic interpreter.
--
-- It holds either a reference index that refers to this element
-- or just 'NoRef', indicating that there are no references
-- to this element.
data StkEl a where
  NoRef :: KnownValue a => StkEl a
  Ref :: KnownValue a => RefId -> StkEl a

instance TestEquality StkEl where
  testEquality :: StkEl a -> StkEl b -> Maybe (a :~: b)
testEquality NoRef NoRef = Maybe (a :~: b)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT
  testEquality (Ref _) (Ref _) = Maybe (a :~: b)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT
  testEquality (Ref _) NoRef = Maybe (a :~: b)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT
  testEquality NoRef (Ref _) = Maybe (a :~: b)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT

-- | Stack of the symbolic interpreter.
type StackVars (stk :: [Kind.Type]) = Rec StkEl stk

-- | Initial state of 'IndigoState'.
data MetaData stk = MetaData
  { MetaData stk -> StackVars stk
mdStack :: StackVars stk
  -- ^ Stack of the symbolic interpreter.
  , MetaData stk -> RefId
mdRefCount :: RefId
  -- ^ Number of allocated variables.
  }

emptyMetadata :: MetaData '[]
emptyMetadata :: MetaData '[]
emptyMetadata = StackVars '[] -> RefId -> MetaData '[]
forall (stk :: [*]). StackVars stk -> RefId -> MetaData stk
MetaData StackVars '[]
forall u (a :: u -> *). Rec a '[]
RNil 0

type DefaultStack stk = Default (MetaData stk)

instance Default (MetaData '[]) where
  def :: MetaData '[]
def = MetaData '[]
emptyMetadata

instance (KnownValue x, Default (MetaData xs)) => Default (MetaData (x ': xs)) where
  def :: MetaData (x : xs)
def = StackVars (x : xs) -> RefId -> MetaData (x : xs)
forall (stk :: [*]). StackVars stk -> RefId -> MetaData stk
MetaData (StkEl x
forall a. KnownValue a => StkEl a
NoRef StkEl x -> Rec StkEl xs -> StackVars (x : xs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& MetaData xs -> Rec StkEl xs
forall (stk :: [*]). MetaData stk -> StackVars stk
mdStack MetaData xs
forall a. Default a => a
def) 0

-- | Resulting state of IndigoM.
data GenCode inp out a = GenCode
  { GenCode inp out a -> a
gcOut :: ~a
  -- ^ Interpreter output value
  , GenCode inp out a -> MetaData out
gcMeta :: ~(MetaData out)
  -- ^ Interpreter meta data.
  , GenCode inp out a -> inp :-> out
gcCode  :: inp :-> out
  -- ^ Generated Lorentz code.
  , GenCode inp out a -> out :-> inp
gcClear :: out :-> inp
  -- ^ Clearing Lorentz code.
  } deriving stock a -> GenCode inp out b -> GenCode inp out a
(a -> b) -> GenCode inp out a -> GenCode inp out b
(forall a b. (a -> b) -> GenCode inp out a -> GenCode inp out b)
-> (forall a b. a -> GenCode inp out b -> GenCode inp out a)
-> Functor (GenCode inp out)
forall (inp :: [*]) (out :: [*]) a b.
a -> GenCode inp out b -> GenCode inp out a
forall (inp :: [*]) (out :: [*]) a b.
(a -> b) -> GenCode inp out a -> GenCode inp out b
forall a b. a -> GenCode inp out b -> GenCode inp out a
forall a b. (a -> b) -> GenCode inp out a -> GenCode inp out b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> GenCode inp out b -> GenCode inp out a
$c<$ :: forall (inp :: [*]) (out :: [*]) a b.
a -> GenCode inp out b -> GenCode inp out a
fmap :: (a -> b) -> GenCode inp out a -> GenCode inp out b
$cfmap :: forall (inp :: [*]) (out :: [*]) a b.
(a -> b) -> GenCode inp out a -> GenCode inp out b
Functor

-- | Produces the generated Lorentz code that cleans after itself, leaving the
-- same stack as the input one
cleanGenCode :: GenCode inp out a -> inp :-> inp
cleanGenCode :: GenCode inp out a -> inp :-> inp
cleanGenCode GenCode {..} = inp :-> out
gcCode (inp :-> out) -> (out :-> inp) -> inp :-> inp
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
## out :-> inp
gcClear