{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE BlockArguments #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE QualifiedDo #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} module LibRISCV.Semantics.RV32_I.Default where import Control.Monad.Freer import LibRISCV.Effects.Decoding.Language (Decoding, decodeShamt) import LibRISCV.Effects.Expressions.Expr import LibRISCV.Effects.Expressions.Language (ExprEval) import LibRISCV.Effects.Logging.Language (LogInstructionFetch) import LibRISCV.Effects.Operations.Language (Operations (..)) import LibRISCV.Internal.Decoder.Opcodes (RV32_I (..)) import LibRISCV.Semantics.Utils instrSemantics :: forall v r. (Member (Operations v) r, Member LogInstructionFetch r, Member (Decoding v) r, Member (ExprEval v) r) => RV32_I -> Eff r () instrSemantics :: forall v (r :: [* -> *]). (Member (Operations v) r, Member LogInstructionFetch r, Member (Decoding v) r, Member (ExprEval v) r) => RV32_I -> Eff r () instrSemantics = \case RV32_I SLLI -> do (v r1, v rd, v _) <- forall v (r :: [* -> *]). (Member (Decoding v) r, Member (Operations v) r) => Eff r (v, v, v) decodeAndReadIType @v v shamt <- Eff r v forall v (effs :: [* -> *]). Member (Decoding v) effs => Eff effs v decodeShamt v -> Expr v -> Eff r () forall v (r :: [* -> *]). (Member (ExprEval v) r, Member (Operations v) r) => v -> Expr v -> Eff r () writeRegister v rd (Expr v -> Eff r ()) -> Expr v -> Eff r () forall a b. (a -> b) -> a -> b $ v r1 v -> v -> Expr v forall {a}. a -> a -> Expr a `lshlImm` v shamt RV32_I SRLI -> do (v r1, v rd, v _) <- forall v (r :: [* -> *]). (Member (Decoding v) r, Member (Operations v) r) => Eff r (v, v, v) decodeAndReadIType @v v shamt <- Eff r v forall v (effs :: [* -> *]). Member (Decoding v) effs => Eff effs v decodeShamt v -> Expr v -> Eff r () forall v (r :: [* -> *]). (Member (ExprEval v) r, Member (Operations v) r) => v -> Expr v -> Eff r () writeRegister v rd (Expr v -> Eff r ()) -> Expr v -> Eff r () forall a b. (a -> b) -> a -> b $ v r1 v -> v -> Expr v forall {a}. a -> a -> Expr a `lshrImm` v shamt RV32_I SRAI -> do (v r1, v rd, v _) <- forall v (r :: [* -> *]). (Member (Decoding v) r, Member (Operations v) r) => Eff r (v, v, v) decodeAndReadIType @v v shamt <- Eff r v forall v (effs :: [* -> *]). Member (Decoding v) effs => Eff effs v decodeShamt v -> Expr v -> Eff r () forall v (r :: [* -> *]). (Member (ExprEval v) r, Member (Operations v) r) => v -> Expr v -> Eff r () writeRegister v rd (Expr v -> Eff r ()) -> Expr v -> Eff r () forall a b. (a -> b) -> a -> b $ v r1 v -> v -> Expr v forall {a}. a -> a -> Expr a `ashrImm` v shamt