{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}

module LibRISCV.Semantics.Utils where

import Control.Applicative
import Control.Monad.Freer
import LibRISCV.Effects.Decoding.Language
import LibRISCV.Effects.Expressions.Expr
import LibRISCV.Effects.Expressions.Language
import LibRISCV.Effects.Operations.Language
import qualified LibRISCV.Effects.Operations.Language as Op

-- TODO add newTypes for type safety
-- decode and read register
decodeAndReadIType :: forall v r. (Member (Decoding v) r, Member (Operations v) r) => Eff r (v, v, v)
decodeAndReadIType :: forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadIType = (v -> v -> v -> (v, v, v))
-> Eff r v -> Eff r v -> Eff r v -> Eff r (v, v, v)
forall (f :: * -> *) a b c d.
Applicative f =>
(a -> b -> c -> d) -> f a -> f b -> f c -> f d
liftA3 (,,) (Eff r v
forall v (effs :: [* -> *]). Member (Decoding v) effs => Eff effs v
decodeRS1 Eff r v -> (v -> Eff r v) -> Eff r v
forall a b. Eff r a -> (a -> Eff r b) -> Eff r b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= v -> Eff r v
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> Eff effs v
Op.readRegister) Eff r v
forall v (effs :: [* -> *]). Member (Decoding v) effs => Eff effs v
decodeRD Eff r v
forall v (effs :: [* -> *]). Member (Decoding v) effs => Eff effs v
decodeImmI

-- decode and read register
decodeAndReadBType :: forall v r. (Member (Decoding v) r, Member (Operations v) r) => Eff r (v, v, v)
decodeAndReadBType :: forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadBType = (v -> v -> v -> (v, v, v))
-> Eff r v -> Eff r v -> Eff r v -> Eff r (v, v, v)
forall (f :: * -> *) a b c d.
Applicative f =>
(a -> b -> c -> d) -> f a -> f b -> f c -> f d
liftA3 (,,) (Eff r v
forall v (effs :: [* -> *]). Member (Decoding v) effs => Eff effs v
decodeRS1 Eff r v -> (v -> Eff r v) -> Eff r v
forall a b. Eff r a -> (a -> Eff r b) -> Eff r b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= v -> Eff r v
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> Eff effs v
Op.readRegister) (Eff r v
forall v (effs :: [* -> *]). Member (Decoding v) effs => Eff effs v
decodeRS2 Eff r v -> (v -> Eff r v) -> Eff r v
forall a b. Eff r a -> (a -> Eff r b) -> Eff r b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= v -> Eff r v
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> Eff effs v
Op.readRegister) Eff r v
forall v (effs :: [* -> *]). Member (Decoding v) effs => Eff effs v
decodeImmB

-- decode and read register
decodeAndReadSType :: forall v r. (Member (Decoding v) r, Member (Operations v) r) => Eff r (v, v, v)
decodeAndReadSType :: forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadSType = (v -> v -> v -> (v, v, v))
-> Eff r v -> Eff r v -> Eff r v -> Eff r (v, v, v)
forall (f :: * -> *) a b c d.
Applicative f =>
(a -> b -> c -> d) -> f a -> f b -> f c -> f d
liftA3 (,,) (Eff r v
forall v (effs :: [* -> *]). Member (Decoding v) effs => Eff effs v
decodeRS1 Eff r v -> (v -> Eff r v) -> Eff r v
forall a b. Eff r a -> (a -> Eff r b) -> Eff r b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= v -> Eff r v
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> Eff effs v
Op.readRegister) (Eff r v
forall v (effs :: [* -> *]). Member (Decoding v) effs => Eff effs v
decodeRS2 Eff r v -> (v -> Eff r v) -> Eff r v
forall a b. Eff r a -> (a -> Eff r b) -> Eff r b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= v -> Eff r v
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> Eff effs v
Op.readRegister) Eff r v
forall v (effs :: [* -> *]). Member (Decoding v) effs => Eff effs v
decodeImmS

-- decode and read register
decodeAndReadRType :: forall v r. (Member (Decoding v) r, Member (Operations v) r) => Eff r (v, v, v)
decodeAndReadRType :: forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadRType = (v -> v -> v -> (v, v, v))
-> Eff r v -> Eff r v -> Eff r v -> Eff r (v, v, v)
forall (f :: * -> *) a b c d.
Applicative f =>
(a -> b -> c -> d) -> f a -> f b -> f c -> f d
liftA3 (,,) (Eff r v
forall v (effs :: [* -> *]). Member (Decoding v) effs => Eff effs v
decodeRS1 Eff r v -> (v -> Eff r v) -> Eff r v
forall a b. Eff r a -> (a -> Eff r b) -> Eff r b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= v -> Eff r v
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> Eff effs v
Op.readRegister) (Eff r v
forall v (effs :: [* -> *]). Member (Decoding v) effs => Eff effs v
decodeRS2 Eff r v -> (v -> Eff r v) -> Eff r v
forall a b. Eff r a -> (a -> Eff r b) -> Eff r b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= v -> Eff r v
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> Eff effs v
Op.readRegister) Eff r v
forall v (effs :: [* -> *]). Member (Decoding v) effs => Eff effs v
decodeRD

-- decode and read register
decodeJType :: forall v r. (Member (Decoding v) r, Member (Operations v) r) => Eff r (v, v)
decodeJType :: forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v)
decodeJType = (v -> v -> (v, v)) -> Eff r v -> Eff r v -> Eff r (v, v)
forall a b c. (a -> b -> c) -> Eff r a -> Eff r b -> Eff r c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,) Eff r v
forall v (effs :: [* -> *]). Member (Decoding v) effs => Eff effs v
decodeRD Eff r v
forall v (effs :: [* -> *]). Member (Decoding v) effs => Eff effs v
decodeImmJ

decodeUType :: forall v r. (Member (Decoding v) r, Member (Operations v) r) => Eff r (v, v)
decodeUType :: forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v)
decodeUType = (v -> v -> (v, v)) -> Eff r v -> Eff r v -> Eff r (v, v)
forall a b c. (a -> b -> c) -> Eff r a -> Eff r b -> Eff r c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,) Eff r v
forall v (effs :: [* -> *]). Member (Decoding v) effs => Eff effs v
decodeRD Eff r v
forall v (effs :: [* -> *]). Member (Decoding v) effs => Eff effs v
decodeImmU

-- | Write to a register in the register file. The function takes a register index and
-- a value which should be written to the register (represented as an 'Expr'). This function
-- is primarly useful to initialize special registers, e.g. setting the stack pointer to a
-- meaningful value at the very beginning of the free monad AST.
writeRegister :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => v -> Expr v -> Eff r ()
writeRegister :: forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
reg Expr v
e = Expr v -> Eff r v
forall v (effs :: [* -> *]).
Member (ExprEval v) effs =>
Expr v -> Eff effs v
eval Expr v
e Eff r v -> (v -> Eff r ()) -> Eff r ()
forall a b. Eff r a -> (a -> Eff r b) -> Eff r b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= v -> v -> Eff r ()
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> v -> Eff effs ()
Op.writeRegister v
reg

-- | Obtain the current value for a register in the register file. The functions takes a register
-- index (encapsulated in an 'Expr') and returns the value of this register.
readRegister :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => Expr v -> Eff r v
readRegister :: forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Expr v -> Eff r v
readRegister Expr v
e = Expr v -> Eff r v
forall v (effs :: [* -> *]).
Member (ExprEval v) effs =>
Expr v -> Eff effs v
eval Expr v
e Eff r v -> (v -> Eff r v) -> Eff r v
forall a b. Eff r a -> (a -> Eff r b) -> Eff r b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= v -> Eff r v
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> Eff effs v
Op.readRegister

-- | Change the current value of the /Program Counter/ (PC). The new value is the only function
-- argument and is represented as an 'Expr'.
writePC :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => Expr v -> Eff r ()
writePC :: forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Expr v -> Eff r ()
writePC Expr v
e = Expr v -> Eff r v
forall v (effs :: [* -> *]).
Member (ExprEval v) effs =>
Expr v -> Eff effs v
eval Expr v
e Eff r v -> (v -> Eff r ()) -> Eff r ()
forall a b. Eff r a -> (a -> Eff r b) -> Eff r b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= v -> Eff r ()
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> Eff effs ()
Op.writePC

-- | Load a fixed-size value from memory. The function takes two arguments: The 'Size' of the
-- value to load and the start address of the value in memory (represented as an 'Expr').
load :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => Size -> Expr v -> Eff r v
load :: forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Size -> Expr v -> Eff r v
load Size
s Expr v
e = Expr v -> Eff r v
forall v (effs :: [* -> *]).
Member (ExprEval v) effs =>
Expr v -> Eff effs v
eval Expr v
e Eff r v -> (v -> Eff r v) -> Eff r v
forall a b. Eff r a -> (a -> Eff r b) -> Eff r b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Size -> v -> Eff r v
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
Size -> v -> Eff effs v
Op.load Size
s

-- | Store a fixed-size value in memory. The arguments are: The 'Size' of the value, the start
-- address where the value should be stored, and the value itself. The latter two are encapuslated
-- in the 'Expr' abstraction.
store :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => Size -> Expr v -> Expr v -> Eff r ()
store :: forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Size -> Expr v -> Expr v -> Eff r ()
store Size
s Expr v
r Expr v
e = do
    v
reg <- Expr v -> Eff r v
forall v (effs :: [* -> *]).
Member (ExprEval v) effs =>
Expr v -> Eff effs v
eval Expr v
r
    v
v <- Expr v -> Eff r v
forall v (effs :: [* -> *]).
Member (ExprEval v) effs =>
Expr v -> Eff effs v
eval Expr v
e
    Size -> v -> v -> Eff r ()
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
Size -> v -> v -> Eff effs ()
Op.store Size
s v
reg v
v