rv 0.0.0.0 → 0.0.1.0

raw patch · 4 files changed

+79/−6 lines, 4 filesdep +Findep +peanodep +wordsetup-changed

Dependencies added: Fin, peano, word

Files

• Setup.hs +0/−2
• rv.cabal +8/−4
• src/Data/RiscV/I.hs +61/−0
• src/Data/RiscV/Reg.hs +10/−0

@@ -1,2 +0,0 @@-import Distribution.Simple-main = defaultMain

@@ -1,5 +1,5 @@ name:                rv-version:             0.0.0.0+version:             0.0.1.0 synopsis:            RISC-V -- description: license:             BSD3@@ -13,11 +13,15 @@ cabal-version:       >=1.10  library-  hs-source-dirs:      .-  exposed-modules:     -  build-depends:       base >= 4.7 && < 5+  hs-source-dirs:      src+  exposed-modules:     Data.RiscV.Reg+                     , Data.RiscV.I+  build-depends:       Fin+                     , base >= 4.7 && < 5                      , base-unicode-symbols+                     , peano                      , util+                     , word   default-language:    Haskell2010   default-extensions:  UnicodeSyntax                      , LambdaCase

@@ -0,0 +1,61 @@+{-# LANGUAGE GADTs, DataKinds, TypeFamilies #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++module Data.RiscV.I where++import Prelude hiding (Word)+import Data.Fin (Fin)+import Data.Functor.Const+import Data.Peano+import Data.Word.General++import Data.RiscV.Reg++data Instruction+  = LUI Reg Word20+  | AUIPC Reg Word20+  | JAL Reg Word20+  | JALR Reg Reg Word12+  | RegImmed IMinor Reg Reg Word12+  | RegReg IOp Reg Reg Reg+  | Branch BranchCmp Reg Reg Word12+  | Load Reg LogNumBytes Signedness+  | Stor Reg LogNumBytes+  | Fence FenceSpec FenceSpec+  | IFence+  | Trap Bool+  | CsrOp CsrOp Reg Reg Csr+  | CsrOpI CsrOp Reg Word5 Csr++data BranchCmp = EQ | NE | LT | LTU | GE | GEU+  deriving (Eq, Show, Enum)++newtype LogNumBytes = LogNumBytes (Fin (Succ (Succ (Succ (Succ Zero)))))+  deriving (Eq, Ord, Show, Enum)++data IOp = ∀ op . IOp (Const (ISubminor op) op)++data IMinor = Add | Slt | Sltu | Xor | Or | And | Shl | Shr+  deriving (Eq, Show, Enum)++type family ISubminor (op :: IMinor) where+    ISubminor Add = Signedness+    ISubminor Shr = Signedness+    ISubminor _ = ()++newtype Signedness = Signedness Bool+  deriving (Eq)++data FenceSpec = FenceSpec+  { fenceI, fenceO, fenceR, fenceW :: Bool }+  deriving (Eq, Show)++newtype Csr = Csr Word12+  deriving (Eq, Ord)++data CsrOp = RW | RS | RC+  deriving (Eq, Show, Enum)++type Word5  = Word (Succ (Succ (Succ (Succ (Succ Zero)))))+type Word12 = Word (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))+type Word20 = Word (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))

@@ -0,0 +1,10 @@+{-# LANGUAGE DataKinds #-}++module Data.RiscV.Reg where++import Prelude hiding (Word)+import Data.Peano+import Data.Word.General++newtype Reg = Reg (Word (Succ (Succ (Succ (Succ (Succ Zero))))))+  deriving (Eq, Ord)