diff options
| -rw-r--r-- | riscv/prelude.sail | 36 | ||||
| -rw-r--r-- | src/sail_lib.ml | 22 |
2 files changed, 56 insertions, 2 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 6a627d22..4b1dd7ea 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -3,10 +3,33 @@ default Order dec type bits ('n : Int) = vector('n, dec, bit) union option ('a : Type) = {None : unit, Some : 'a} -val spaces : nat <-> string -val opt_spaces : nat <-> string +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 spaces_forwards : unit -> string +function spaces_forwards () = " " +val spaces_backwards : string -> unit +function spaces_backwards s = () + +val spaces_matches_prefix = "spaces_matches_prefix" : string -> option((unit, nat)) + +val opt_spaces_forwards : unit -> string +function opt_spaces_forwards () = "" +val opt_spaces_backwards : string -> unit +function opt_spaces_backwards s = () + +val opt_spaces_matches_prefix = "opt_spaces_matches_prefix" : string -> option((unit, nat)) + +val def_spaces_forwards : unit -> string +function def_spaces_forwards () = " " +val def_spaces_backwards : string -> unit +function def_spaces_backwards s = () + +val def_spaces_matches_prefix = "opt_spaces_matches_prefix" : string -> option((unit, nat)) + + val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : forall 'n 'm. (atom('n), atom('m)) -> bool val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool @@ -20,6 +43,14 @@ val "eq_bit" : (bit, bit) -> bool val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool val eq_string = {ocaml: "eq_string", lem: "eq"} : (string, string) -> bool +val string_startswith = "string_startswith" : (string, string) -> bool +val string_drop = "string_drop" : (string, nat) -> string +val string_length = "string_length" : string -> nat +val string_append = "string_append" : (string, string) -> string +val maybe_int_of_prefix = "maybe_int_of_prefix" : string -> option((int, nat)) +val maybe_nat_of_prefix = "maybe_nat_of_prefix" : string -> option((nat, nat)) +val maybe_int_of_string = "maybe_int_of_string" : string -> option(int) + val eq_real = {ocaml: "eq_real", lem: "eq"} : (real, real) -> bool @@ -192,6 +223,7 @@ val sub_range = {ocaml: "sub_int", lem: "integerMinus"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) val sub_int = {ocaml: "sub_int", lem: "integerMinus"} : (int, int) -> int +val sub_nat = {ocaml: "sub_int", lem: "integerMinus"} : (nat, nat) -> nat val "sub_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 1f3d0bba..b4c5a8aa 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -622,3 +622,25 @@ let speculate_conditional_success () = true (* Return nanoseconds since epoch. Truncates to ocaml int but will be OK for next 100 years or so... *) let get_time_ns () = Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ())) +let rec n_leading_spaces s = + match String.length s with + | 0 -> 0 + | 1 -> begin match s with + | " " -> 1 + | _ -> 0 + end + | len -> begin match String.get s 0 with + | ' ' -> 1 + (n_leading_spaces (String.sub s 1 (len - 1))) + | _ -> 0 + end + + +let opt_spaces_matches_prefix s = + ZSome ((), n_leading_spaces s |> Big_int.of_int) + +let spaces_matches_prefix s = + let n = n_leading_spaces s in + match n with + | 0 -> ZNone () + | n -> ZSome ((), Big_int.of_int n) + |