Coq: add some of string library

2 files changed, 17 insertions, 1 deletions

diff --git a/lib/coq/Makefile b/lib/coq/Makefile
index 97869e3c..99321aae 100644
--- a/lib/coq/Makefile
+++ b/lib/coq/Makefile
@@ -1,6 +1,6 @@
 BBV_DIR=../../../bbv/theories
 
-SRC=Sail2_prompt_monad.v  Sail2_prompt.v  Sail2_impl_base.v  Sail2_instr_kinds.v  Sail2_operators_bitlists.v  Sail2_operators_mwords.v  Sail2_operators.v  Sail2_values.v  Sail2_state_monad.v  Sail2_state.v
+SRC=Sail2_prompt_monad.v  Sail2_prompt.v  Sail2_impl_base.v  Sail2_instr_kinds.v  Sail2_operators_bitlists.v  Sail2_operators_mwords.v  Sail2_operators.v  Sail2_values.v  Sail2_state_monad.v  Sail2_state.v  Sail2_string.v
 
 COQ_LIBS = -R . Sail -R "$(BBV_DIR)" bbv
 
diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v
new file mode 100644
index 00000000..8bd7f0a6
--- /dev/null
+++ b/lib/coq/Sail2_string.v
@@ -0,0 +1,16 @@
+Require Import Sail2_values.
+
+Definition string_sub (s : string) (start : Z) (len : Z) : string :=
+  String.substring (Z.to_nat start) (Z.to_nat len) s.
+
+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
+  String.substring n (String.length s - n) s.
+
+Definition string_length s := Z.of_nat (String.length s).
+
+Definition string_append := String.append.
\ No newline at end of file