From b7307bd33a1c0fe7190fc4b34a9d3eca9beda565 Mon Sep 17 00:00:00 2001
From: Jon French
Date: Thu, 10 May 2018 13:05:43 +0100
Subject: hacky monomorphic bits-string-parser for now

---
 riscv/prelude.sail | 6 ++++--
 riscv/riscv.sail   | 2 +-
 2 files changed, 5 insertions(+), 3 deletions(-)

(limited to 'riscv')

diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 4b1dd7ea..153b41db 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -6,7 +6,10 @@ union option ('a : Type) = {None : unit, Some : 'a}
 val spaces : unit <-> string
 val opt_spaces : unit <-> string
 val def_spaces : unit <-> string
-val hex_bits : forall 'n. (atom('n), bits('n)) <-> string
+val hex_bits_12 : bits(12) <-> string
+
+val hex_bits_12_forwards = "string_of_bits" : bits(12) -> string
+val "hex_bits_12_matches_prefix" : string -> option((bits(12), nat))
 
 val spaces_forwards : unit -> string
 function spaces_forwards () = " "
@@ -37,7 +40,6 @@ val lt_atom = "lt" : forall 'n 'm. (atom('n), atom('m)) -> bool
 val gt_atom = "gt" : forall 'n 'm. (atom('n), atom('m)) -> bool
 
 val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
-
 val "eq_bit" : (bit, bit) -> bool
 
 val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index ed640ad3..8e734576 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -185,7 +185,7 @@ mapping operand_sep = {
 
 val itype_operands : (bits(12), regbits, regbits) <-> string
 mapping itype_operands = {
-  (imm, rs1, rd) <-> spaces() ^^ reg_name(rd) ^^ operand_sep() ^^ reg_name(rs1) ^^ operand_sep() ^^ hex_bits(12, imm)
+  (imm, rs1, rd) <-> spaces() ^^ reg_name(rd) ^^ operand_sep() ^^ reg_name(rs1) ^^ operand_sep() ^^ hex_bits_12(imm)
 }
 
 mapping clause assembly = ITYPE(imm, rs1, rd, RISCV_ADDI)  <-> "addi"  ^^ itype_operands(imm, rs1, rd)
-- 
cgit v1.2.3