jpm61704

module Search where

import Agda.Syntax.Parser
-- import Agda.Syntax.Abstract as Abstract
import Agda.Syntax.Concrete as Concrete
-- import Agda.Syntax.Translation.ConcreteToAbstract
import Agda.Syntax.Scope.Monad
import Agda.Utils.FileName

import Data.Text.Lazy as T

jpm61704

infix 5 _,_∶_

data Context : Set where
  ∅ : Context
  _,_∶_ : Context → Id → Expr → Context

infix 4 _∋_∶_

data _∋_∶_ : Context → Id → Expr → Set where

jpm61704

decodeRegister ∷ W5 → MBReg
decodeRegister reg = case reg of
    (W5 C C C C C) -> R0
    (W5 C C C C S) -> R1
    (W5 C C C S C) -> R2
    (W5 C C C S S) -> R3
    (W5 C C S C C) -> R4
    (W5 C C S C S) -> R5
    (W5 C C S S C) -> R6
    (W5 C C S S S) -> R7

jpm61704

data Instr = ADDI W12 W5 W3 W5 W7

           | FENCE W4 Bit Bit Bit Bit Bit Bit Bit Bit W5 W3 W5 W7
           | FENCEI W12 W5 W3 W5 W7
           | ECALL W12 W5 W3 W5 W7
           | EBREAK W12 W5 W3 W5 W7