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

{-# LANGUAGE InstanceSigs #-}

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

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

Functionally, it's the same as having Lorentz instruction that can access and
modify a 'StackVars', referring to values on the stack with a 'RefId'.
-}

module Indigo.Internal.State
  ( -- * Indigo State
    IndigoState (..)
  , usingIndigoState
  , (>>)
  , (<$>)
  , iput
  , nopState
  , assignTopVar
  , withObject
  , withObjectState
  , withStackVars

  , DecomposedObjects
  , MetaData (..)
  , replStkMd
  , alterStkMd
  , pushRefMd
  , pushNoRefMd
  , popNoRefMd

  , GenCode (..)
  , cleanGenCode
  ) where

import qualified Data.Map as M
import Data.Typeable ((:~:)(..), eqT)

import Indigo.Internal.Object
import Indigo.Internal.Var
import Indigo.Backend.Prelude
import Indigo.Lorentz
import qualified Lorentz.Instr as L
import Util.Peano

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

-- | IndigoState data type.
--
-- It takes as input a 'StackVars' (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.
--
-- It has no return type, IndigoState instruction may take one or more
-- "return variables", that they assign to values produced during their execution.
newtype IndigoState inp out = IndigoState {
    IndigoState inp out -> MetaData inp -> GenCode inp out
runIndigoState :: MetaData inp -> GenCode inp out
  }

-- | Inverse of 'runIndigoState' for utility.
usingIndigoState :: MetaData inp -> IndigoState inp out -> GenCode inp out
usingIndigoState :: MetaData inp -> IndigoState inp out -> GenCode inp out
usingIndigoState md :: MetaData inp
md act :: IndigoState inp out
act = IndigoState inp out -> MetaData inp -> GenCode inp out
forall (inp :: [*]) (out :: [*]).
IndigoState inp out -> MetaData inp -> GenCode inp out
runIndigoState IndigoState inp out
act MetaData inp
md

-- | Then for rebindable syntax.
(>>) :: IndigoState inp out -> IndigoState out out1 -> IndigoState inp out1
>> :: IndigoState inp out -> IndigoState out out1 -> IndigoState inp out1
(>>) a :: IndigoState inp out
a b :: IndigoState out out1
b = (MetaData inp -> GenCode inp out1) -> IndigoState inp out1
forall (inp :: [*]) (out :: [*]).
(MetaData inp -> GenCode inp out) -> IndigoState inp out
IndigoState ((MetaData inp -> GenCode inp out1) -> IndigoState inp out1)
-> (MetaData inp -> GenCode inp out1) -> IndigoState inp out1
forall a b. (a -> b) -> a -> b
$ \md :: MetaData inp
md ->
  let GenCode st1 :: StackVars out
st1 cd1 :: inp :-> out
cd1 cl1 :: out :-> inp
cl1 = IndigoState inp out -> MetaData inp -> GenCode inp out
forall (inp :: [*]) (out :: [*]).
IndigoState inp out -> MetaData inp -> GenCode inp out
runIndigoState IndigoState inp out
a MetaData inp
md in
  let GenCode st2 :: StackVars out1
st2 cd2 :: out :-> out1
cd2 cl2 :: out1 :-> out
cl2 = IndigoState out out1 -> MetaData out -> GenCode out out1
forall (inp :: [*]) (out :: [*]).
IndigoState inp out -> MetaData inp -> GenCode inp out
runIndigoState IndigoState out out1
b (MetaData inp -> StackVars out -> MetaData out
forall (inp :: [*]) (inp1 :: [*]).
MetaData inp -> StackVars inp1 -> MetaData inp1
replStkMd MetaData inp
md StackVars out
st1) in
  StackVars out1
-> (inp :-> out1) -> (out1 :-> inp) -> GenCode inp out1
forall (inp :: [*]) (out :: [*]).
StackVars out -> (inp :-> out) -> (out :-> inp) -> GenCode inp out
GenCode StackVars out1
st2 (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)

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

-- | The simplest 'IndigoState', it does not modify the stack, nor the produced
-- code.
nopState :: IndigoState inp inp
nopState :: IndigoState inp inp
nopState = (MetaData inp -> GenCode inp inp) -> IndigoState inp inp
forall (inp :: [*]) (out :: [*]).
(MetaData inp -> GenCode inp out) -> IndigoState inp out
IndigoState ((MetaData inp -> GenCode inp inp) -> IndigoState inp inp)
-> (MetaData inp -> GenCode inp inp) -> IndigoState inp inp
forall a b. (a -> b) -> a -> b
$ \md :: MetaData inp
md -> StackVars inp -> (inp :-> inp) -> (inp :-> inp) -> GenCode inp inp
forall (inp :: [*]) (out :: [*]).
StackVars out -> (inp :-> out) -> (out :-> inp) -> GenCode inp out
GenCode (MetaData inp -> StackVars inp
forall (inp :: [*]). MetaData inp -> StackVars inp
mdStack MetaData inp
md) inp :-> inp
forall (s :: [*]). s :-> s
L.nop inp :-> inp
forall (s :: [*]). s :-> s
L.nop

-- | Assigns a variable to reference the element on top of the stack.
assignTopVar :: KnownValue x => Var x -> IndigoState (x & inp) (x & inp)
assignTopVar :: Var x -> IndigoState (x & inp) (x & inp)
assignTopVar var :: Var x
var = (MetaData (x & inp) -> GenCode (x & inp) (x & inp))
-> IndigoState (x & inp) (x & inp)
forall (inp :: [*]) (out :: [*]).
(MetaData inp -> GenCode inp out) -> IndigoState inp out
IndigoState ((MetaData (x & inp) -> GenCode (x & inp) (x & inp))
 -> IndigoState (x & inp) (x & inp))
-> (MetaData (x & inp) -> GenCode (x & inp) (x & inp))
-> IndigoState (x & inp) (x & inp)
forall a b. (a -> b) -> a -> b
$ \md :: MetaData (x & inp)
md ->
  StackVars (x & inp)
-> ((x & inp) :-> (x & inp))
-> ((x & inp) :-> (x & inp))
-> GenCode (x & inp) (x & inp)
forall (inp :: [*]) (out :: [*]).
StackVars out -> (inp :-> out) -> (out :-> inp) -> GenCode inp out
GenCode (Var x -> StackVars (x & inp) -> Sing 'Z -> StackVars (x & inp)
forall a (n :: Peano) (inp :: [*]).
(KnownValue a, a ~ At n inp, RequireLongerThan inp n) =>
Var a -> StackVars inp -> Sing n -> StackVars inp
assignVarAt Var x
var (MetaData (x & inp) -> StackVars (x & inp)
forall (inp :: [*]). MetaData inp -> StackVars inp
mdStack MetaData (x & inp)
md) Sing 'Z
SingNat 'Z
SZ) (x & inp) :-> (x & inp)
forall (s :: [*]). s :-> s
L.nop (x & inp) :-> (x & inp)
forall (s :: [*]). s :-> s
L.nop

withObject
  :: forall a r .  KnownValue a
  => DecomposedObjects
  -> Var a
  -> (Object a -> r)
  -> r
withObject :: DecomposedObjects -> Var a -> (Object a -> r) -> r
withObject objs :: DecomposedObjects
objs (Var refId :: RefId
refId) f :: Object a -> r
f = case RefId -> DecomposedObjects -> Maybe SomeObject
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup RefId
refId DecomposedObjects
objs of
  Nothing -> Object a -> r
f (RefId -> Object a
forall a (f :: Symbol -> *).
KnownValue a =>
RefId -> IndigoObjectF f a
Cell RefId
refId)
  Just so :: SomeObject
so -> case SomeObject
so of
    SomeObject (Object a
obj :: Object a1) -> case (Typeable a, Typeable a) => Maybe (a :~: a)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @a1 of
      Just Refl -> Object a -> r
f Object a
Object a
obj
      Nothing ->
        Text -> r
forall a. HasCallStack => Text -> a
error (Text -> r) -> Text -> r
forall a b. (a -> b) -> a -> b
$ "unexpectedly SomeObject with by reference #" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RefId -> Text
forall b a. (Show a, IsString b) => a -> b
show RefId
refId Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> " has different type"

withObjectState
  :: forall a inp out . KnownValue a
  => Var a
  -> (Object a -> IndigoState inp out)
  -> IndigoState inp out
withObjectState :: Var a -> (Object a -> IndigoState inp out) -> IndigoState inp out
withObjectState v :: Var a
v f :: Object a -> IndigoState inp out
f = (MetaData inp -> GenCode inp out) -> IndigoState inp out
forall (inp :: [*]) (out :: [*]).
(MetaData inp -> GenCode inp out) -> IndigoState inp out
IndigoState ((MetaData inp -> GenCode inp out) -> IndigoState inp out)
-> (MetaData inp -> GenCode inp out) -> IndigoState inp out
forall a b. (a -> b) -> a -> b
$ \md :: MetaData inp
md -> MetaData inp -> IndigoState inp out -> GenCode inp out
forall (inp :: [*]) (out :: [*]).
MetaData inp -> IndigoState inp out -> GenCode inp out
usingIndigoState MetaData inp
md (DecomposedObjects
-> Var a
-> (Object a -> IndigoState inp out)
-> IndigoState inp out
forall a r.
KnownValue a =>
DecomposedObjects -> Var a -> (Object a -> r) -> r
withObject (MetaData inp -> DecomposedObjects
forall (inp :: [*]). MetaData inp -> DecomposedObjects
mdObjects MetaData inp
md) Var a
v Object a -> IndigoState inp out
f)

-- | Utility function to create 'IndigoState' that need access to the current 'StackVars'.
withStackVars :: (StackVars inp -> IndigoState inp out) -> IndigoState inp out
withStackVars :: (StackVars inp -> IndigoState inp out) -> IndigoState inp out
withStackVars fIs :: StackVars inp -> IndigoState inp out
fIs = (MetaData inp -> GenCode inp out) -> IndigoState inp out
forall (inp :: [*]) (out :: [*]).
(MetaData inp -> GenCode inp out) -> IndigoState inp out
IndigoState ((MetaData inp -> GenCode inp out) -> IndigoState inp out)
-> (MetaData inp -> GenCode inp out) -> IndigoState inp out
forall a b. (a -> b) -> a -> b
$ \md :: MetaData inp
md -> MetaData inp -> IndigoState inp out -> GenCode inp out
forall (inp :: [*]) (out :: [*]).
MetaData inp -> IndigoState inp out -> GenCode inp out
usingIndigoState MetaData inp
md (StackVars inp -> IndigoState inp out
fIs (StackVars inp -> IndigoState inp out)
-> StackVars inp -> IndigoState inp out
forall a b. (a -> b) -> a -> b
$ MetaData inp -> StackVars inp
forall (inp :: [*]). MetaData inp -> StackVars inp
mdStack MetaData inp
md)

----------------------------------------------------------------------------
-- MetaData primitives
----------------------------------------------------------------------------

type DecomposedObjects = Map RefId SomeObject

data MetaData inp = MetaData
  { MetaData inp -> StackVars inp
mdStack   :: StackVars inp
  , MetaData inp -> DecomposedObjects
mdObjects :: DecomposedObjects
  }

replStkMd :: MetaData inp -> StackVars inp1 -> MetaData inp1
replStkMd :: MetaData inp -> StackVars inp1 -> MetaData inp1
replStkMd md :: MetaData inp
md = MetaData inp -> (StackVars inp -> StackVars inp1) -> MetaData inp1
forall (inp :: [*]) (inp1 :: [*]).
MetaData inp -> (StackVars inp -> StackVars inp1) -> MetaData inp1
alterStkMd MetaData inp
md ((StackVars inp -> StackVars inp1) -> MetaData inp1)
-> (StackVars inp1 -> StackVars inp -> StackVars inp1)
-> StackVars inp1
-> MetaData inp1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StackVars inp1 -> StackVars inp -> StackVars inp1
forall a b. a -> b -> a
const

alterStkMd :: MetaData inp -> (StackVars inp -> StackVars inp1) -> MetaData inp1
alterStkMd :: MetaData inp -> (StackVars inp -> StackVars inp1) -> MetaData inp1
alterStkMd (MetaData stk :: StackVars inp
stk objs :: DecomposedObjects
objs) f :: StackVars inp -> StackVars inp1
f = StackVars inp1 -> DecomposedObjects -> MetaData inp1
forall (inp :: [*]).
StackVars inp -> DecomposedObjects -> MetaData inp
MetaData (StackVars inp -> StackVars inp1
f StackVars inp
stk) DecomposedObjects
objs

-- | 'pushRef' version for 'MetaData'
pushRefMd :: KnownValue a => Var a -> MetaData inp -> MetaData (a & inp)
pushRefMd :: Var a -> MetaData inp -> MetaData (a & inp)
pushRefMd var :: Var a
var md :: MetaData inp
md = MetaData inp
-> (StackVars inp -> StackVars (a & inp)) -> MetaData (a & inp)
forall (inp :: [*]) (inp1 :: [*]).
MetaData inp -> (StackVars inp -> StackVars inp1) -> MetaData inp1
alterStkMd MetaData inp
md (Var a -> StackVars inp -> StackVars (a & inp)
forall a (inp :: [*]).
KnownValue a =>
Var a -> StackVars inp -> StackVars (a & inp)
pushRef Var a
var)

-- | 'pushNoRef' version for 'MetaData'
pushNoRefMd :: KnownValue a => MetaData inp -> MetaData (a & inp)
pushNoRefMd :: MetaData inp -> MetaData (a & inp)
pushNoRefMd md :: MetaData inp
md = MetaData inp
-> (StackVars inp -> StackVars (a & inp)) -> MetaData (a & inp)
forall (inp :: [*]) (inp1 :: [*]).
MetaData inp -> (StackVars inp -> StackVars inp1) -> MetaData inp1
alterStkMd MetaData inp
md StackVars inp -> StackVars (a & inp)
forall a (inp :: [*]).
KnownValue a =>
StackVars inp -> StackVars (a & inp)
pushNoRef

-- | 'popNoRef' version for 'MetaData'
popNoRefMd :: MetaData (a & inp) -> MetaData inp
popNoRefMd :: MetaData (a & inp) -> MetaData inp
popNoRefMd md :: MetaData (a & inp)
md = MetaData (a & inp)
-> (StackVars (a & inp) -> StackVars inp) -> MetaData inp
forall (inp :: [*]) (inp1 :: [*]).
MetaData inp -> (StackVars inp -> StackVars inp1) -> MetaData inp1
alterStkMd MetaData (a & inp)
md StackVars (a & inp) -> StackVars inp
forall a (inp :: [*]). StackVars (a & inp) -> StackVars inp
popNoRef

----------------------------------------------------------------------------
-- Code generation primitives
----------------------------------------------------------------------------

-- | Resulting state of IndigoM.
data GenCode inp out = GenCode
  { GenCode inp out -> StackVars out
gcStack :: ~(StackVars out)
  -- ^ Stack of the symbolic interpreter.
  , GenCode inp out -> inp :-> out
gcCode  :: inp :-> out
  -- ^ Generated Lorentz code.
  , GenCode inp out -> out :-> inp
gcClear :: out :-> inp
  -- ^ Clearing Lorentz code.
  }

-- | Produces the generated Lorentz code that cleans after itself, leaving the
-- same stack as the input one
cleanGenCode :: GenCode inp out -> inp :-> inp
cleanGenCode :: GenCode inp out -> 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