Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: sint63Notation.v Sprache: Coq

Original von: Coq^©

From Coq
Require Import Int63.
Import ZArith.

Declare Scope uint_scope.
Declare Scope sint_scope.
Delimit Scope uint_scope with uint.
Delimit Scope sint_scope with sint.

Record uint := wrapu { unwrapu : int }.
Record sint := wraps { unwraps : int }.

Definition uof_Z (v : Z) := wrapu (of_Z v).
Definition uto_Z (v : uint) := to_Z (unwrapu v).

Definition sof_Z (v : Z) := wraps (of_Z (v mod (2 ^ 31))).
Definition as_signed (bw : Z) (v : Z) :=
(((2 ^ (bw - 1) + v) mod (2 ^ bw)) - 2 ^ (bw - 1))%Z.

Definition sto_Z (v : sint) := as_signed 31 (to_Z (unwraps v)).
Numeral Notation uint uof_Z uto_Z : uint_scope.
Numeral Notation sint sof_Z sto_Z : sint_scope.
Open Scope uint_scope.
Compute uof_Z 0.
Compute uof_Z 1.
Compute uof_Z (-1).
Check let v := 0 in v : uint.
Check let v := 1 in v : uint.
Check let v := -1 in v : uint.
Close Scope uint_scope.
Open Scope sint_scope.
Compute sof_Z 0.
Compute sof_Z 1.
Compute sof_Z (-1).
Check let v := 0 in v : sint.
Check let v := 1 in v : sint.
Check let v := -1 in v : sint.

¤ Dauer der Verarbeitung: 0.15 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.