Coq: more strings for RISC-V

2 files changed, 25 insertions, 6 deletions

diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v
index 8bd7f0a6..9ca9cb67 100644
--- a/lib/coq/Sail2_string.v
+++ b/lib/coq/Sail2_string.v
@@ -7,10 +7,29 @@ Definition string_startswith s expected :=
   let prefix := String.substring 0 (String.length expected) s in
   generic_eq prefix expected.
 
-Definition string_drop s n :=
-  let n := Z.to_nat n in
+Definition string_drop s (n : {n : Z & ArithFact (n >= 0)}) :=
+  let n := Z.to_nat (projT1 n) in
   String.substring n (String.length s - n) s.
 
-Definition string_length s := Z.of_nat (String.length s).
+Definition string_length s : {n : Z & ArithFact (n >= 0)} :=
+ build_ex (Z.of_nat (String.length s)).
 
-Definition string_append := String.append.
\ No newline at end of file
+Definition string_append := String.append.
+
+(* TODO: maybe_int_of_prefix, maybe_int_of_string *)
+
+Fixpoint n_leading_spaces (s:string) : nat :=
+  match s with
+  | EmptyString => 0
+  | String " " t => S (n_leading_spaces t)
+  | _ => 0
+  end.
+
+Definition opt_spc_matches_prefix s : option (unit * {n : Z & ArithFact (n >= 0)}) :=
+  Some (tt, build_ex (Z.of_nat (n_leading_spaces s))).
+
+Definition spc_matches_prefix s : option (unit * {n : Z & ArithFact (n >= 0)}) :=
+  match n_leading_spaces s with
+  | O => None
+  | S n => Some (tt, build_ex (Z.of_nat (S n)))
+  end.
\ No newline at end of file
diff --git a/riscv/riscv_extras.v b/riscv/riscv_extras.v
index a3cb3fb9..3f1fe7e0 100644
--- a/riscv/riscv_extras.v
+++ b/riscv/riscv_extras.v
@@ -124,9 +124,9 @@ Definition skip {rv e} (_:unit) : monad rv unit e := returnm tt.
 Definition elf_entry (_:unit) : Z := 0.
 (*declare ocaml target_rep function elf_entry := `Elf_loader.elf_entry`*)
 
-(*Definition print_bits msg bs := prerr_endline (msg ^ (string_of_bits bs))
+Definition print_bits {n} msg (bs : mword n) := prerr_endline (msg ++ (string_of_bits bs)).
 
-val get_time_ns : unit -> integer*)
+(*val get_time_ns : unit -> integer*)
 Definition get_time_ns (_:unit) : Z := 0.
 (*declare ocaml target_rep function get_time_ns := `(fun () -> Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ())))`*)