Strings: add ByteVector

3 files changed, 61 insertions, 0 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 865e1eeb95..ada68f97d5 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -241,6 +241,8 @@ Standard Library
 - There are now conversions between `string` and `positive`, `Z`,
   `nat`, and `N` in binary, octal, and hex.
 
+- Added `ByteVector` type that can convert to and from [string].
+
 Display diffs between proof steps
 
 - `coqtop` and `coqide` can now highlight the differences between proof steps
diff --git a/theories/Strings/ByteVector.v b/theories/Strings/ByteVector.v
new file mode 100644
index 0000000000..16f26002d2
--- /dev/null
+++ b/theories/Strings/ByteVector.v
@@ -0,0 +1,56 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+Require Import Ascii Basics Bvector Psatz String Vector.
+Export VectorNotations.
+Open Scope program_scope.
+Open Scope string_scope.
+
+Definition ByteVector := Vector.t ascii.
+
+Definition ByteNil : ByteVector 0 := Vector.nil ascii.
+
+Definition little_endian_to_string {n : nat} (v : ByteVector n) : string :=
+  fold_right String v "".
+
+Definition to_string {n : nat} : ByteVector n -> string :=
+  little_endian_to_string ∘ rev.
+
+Fixpoint little_endian_of_string (s : string) : ByteVector (length s) :=
+  match s with
+  | "" => ByteNil
+  | String b s' => b :: little_endian_of_string s'
+  end.
+
+Definition of_string (s : string) : ByteVector (length s) :=
+  rev (little_endian_of_string s).
+
+Fixpoint to_Bvector {n : nat} (v : ByteVector n) : Bvector (n * 8) :=
+  match v with
+  | [] => []
+  | Ascii b0 b1 b2 b3 b4 b5 b6 b7::v' =>
+    b0::b1::b2::b3::b4::b5::b6::b7::to_Bvector v'
+  end.
+
+Fixpoint of_Bvector {n : nat} : Bvector (n * 8) -> ByteVector n :=
+  match n with
+  | 0 => fun _ => []
+  | S n' =>
+    fun v =>
+      let (b0, v1) := uncons v in
+      let (b1, v2) := uncons v1 in
+      let (b2, v3) := uncons v2 in
+      let (b3, v4) := uncons v3 in
+      let (b4, v5) := uncons v4 in
+      let (b5, v6) := uncons v5 in
+      let (b6, v7) := uncons v6 in
+      let (b7, v8) := uncons v7 in
+      Ascii b0 b1 b2 b3 b4 b5 b6 b7::of_Bvector v8
+  end.
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 390ca78c0e..4a2bddf35c 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -132,6 +132,9 @@ replace v (Fin.of_nat_lt H).
 Definition tl {A} := @caseS _ (fun n v => t A n) (fun h n t => t).
 Global Arguments tl {A} {n} v.
 
+(** Destruct a non empty vector *)
+Definition uncons {A} {n : nat} (v : t A (S n)) : A * t A n := (hd v, tl v).
+
 (** Remove last element of a non-empty vector *)
 Definition shiftout {A} := @rectS _ (fun n _ => t A n) (fun a => [])
   (fun h _ _ H => h :: H).