Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ByteVector.v Sprache: Coq

Original von: Coq^©

(************************************************************************)
(*         *   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 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.

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.