print register names like t0, t1, a0, s0, etc instead of x0, x1, etc

mit-plv · Mar 16, 2023 · 55c9cc8 · 55c9cc8
1 parent f193b6e
commit 55c9cc8
Show file tree

Hide file tree

Showing 5 changed files with 471 additions and 141 deletions.
diff --git a/src/riscv/Utility/InstructionCoercions.v b/src/riscv/Utility/InstructionCoercions.v
@@ -1,10 +1,14 @@
 Require Import riscv.Spec.Decode.
 
-Coercion IInstruction: InstructionI >-> Instruction.
-Coercion MInstruction: InstructionM >-> Instruction.
-Coercion I64Instruction: InstructionI64 >-> Instruction.
-Coercion M64Instruction: InstructionM64 >-> Instruction.
-Coercion CSRInstruction: InstructionCSR >-> Instruction.
+Coercion IInstruction   : InstructionI   >-> Instruction.
+Coercion MInstruction   : InstructionM   >-> Instruction.
+Coercion AInstruction   : InstructionA   >-> Instruction.
+Coercion FInstruction   : InstructionF   >-> Instruction.
+Coercion I64Instruction : InstructionI64 >-> Instruction.
+Coercion M64Instruction : InstructionM64 >-> Instruction.
+Coercion A64Instruction : InstructionA64 >-> Instruction.
+Coercion F64Instruction : InstructionF64 >-> Instruction.
+Coercion CSRInstruction : InstructionCSR >-> Instruction.
 
 (* separate notation to make sure coercions kick in *)
 Declare Scope ilist_scope.