aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Strings
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Strings')
-rw-r--r--theories/Strings/Ascii.v119
1 files changed, 65 insertions, 54 deletions
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index ba01f3d4c..38245f59e 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -10,8 +10,7 @@
(** Contributed by Laurent Théry (INRIA);
Adapted to Coq V8 by the Coq Development Team *)
-Require Import Bool.
-Require Import BinPos.
+Require Import Bool BinPos BinNat Nnat.
Declare ML Module "ascii_syntax_plugin".
(** * Definition of ascii characters *)
@@ -27,19 +26,6 @@ Definition zero := Ascii false false false false false false false false.
Definition one := Ascii true false false false false false false false.
-Definition app1 (f : bool -> bool) (a : ascii) :=
- match a with
- | Ascii a1 a2 a3 a4 a5 a6 a7 a8 =>
- Ascii (f a1) (f a2) (f a3) (f a4) (f a5) (f a6) (f a7) (f a8)
- end.
-
-Definition app2 (f : bool -> bool -> bool) (a b : ascii) :=
- match a, b with
- | Ascii a1 a2 a3 a4 a5 a6 a7 a8, Ascii b1 b2 b3 b4 b5 b6 b7 b8 =>
- Ascii (f a1 b1) (f a2 b2) (f a3 b3) (f a4 b4)
- (f a5 b5) (f a6 b6) (f a7 b7) (f a8 b8)
- end.
-
Definition shift (c : bool) (a : ascii) :=
match a with
| Ascii a1 a2 a3 a4 a5 a6 a7 a8 => Ascii c a1 a2 a3 a4 a5 a6 a7
@@ -54,53 +40,65 @@ Defined.
(** * Conversion between natural numbers modulo 256 and ascii characters *)
(** Auxillary function that turns a positive into an ascii by
- looking at the last n bits, ie z mod 2^n *)
-
-Fixpoint ascii_of_pos_aux (res acc : ascii) (z : positive)
- (n : nat) : ascii :=
+ looking at the last 8 bits, ie z mod 2^8 *)
+
+Definition ascii_of_pos : positive -> ascii :=
+ let loop := fix loop n p :=
+ match n with
+ | O => zero
+ | S n' =>
+ match p with
+ | xH => one
+ | xI p' => shift true (loop n' p')
+ | xO p' => shift false (loop n' p')
+ end
+ end
+ in loop 8.
+
+(** Conversion from [N] to [ascii] *)
+
+Definition ascii_of_N (n : N) :=
match n with
- | O => res
- | S n1 =>
- match z with
- | xH => app2 orb res acc
- | xI z' => ascii_of_pos_aux (app2 orb res acc) (shift false acc) z' n1
- | xO z' => ascii_of_pos_aux res (shift false acc) z' n1
- end
+ | N0 => zero
+ | Npos p => ascii_of_pos p
end.
+(** Same for [nat] *)
-(** Function that turns a positive into an ascii by
- looking at the last 8 bits, ie a mod 8 *)
+Definition ascii_of_nat (a : nat) := ascii_of_N (N_of_nat a).
-Definition ascii_of_pos (a : positive) := ascii_of_pos_aux zero one a 8.
+(** The opposite functions *)
-(** Function that turns a Peano number into an ascii by converting it
- to positive *)
+Local Open Scope list_scope.
-Definition ascii_of_nat (a : nat) :=
- match a with
- | O => zero
- | S a' => ascii_of_pos (P_of_succ_nat a')
- end.
+Fixpoint N_of_digits (l:list bool) : N :=
+ match l with
+ | nil => 0
+ | b :: l' => (if b then 1 else 0) + 2*(N_of_digits l')
+ end%N.
+
+Definition N_of_ascii (a : ascii) : N :=
+ let (a0,a1,a2,a3,a4,a5,a6,a7) := a in
+ N_of_digits (a0::a1::a2::a3::a4::a5::a6::a7::nil).
+
+Definition nat_of_ascii (a : ascii) : nat := nat_of_N (N_of_ascii a).
-(** The opposite function *)
-
-Definition nat_of_ascii (a : ascii) : nat :=
- let (a1, a2, a3, a4, a5, a6, a7, a8) := a in
- 2 *
- (2 *
- (2 *
- (2 *
- (2 *
- (2 *
- (2 * (if a8 then 1 else 0)
- + (if a7 then 1 else 0))
- + (if a6 then 1 else 0))
- + (if a5 then 1 else 0))
- + (if a4 then 1 else 0))
- + (if a3 then 1 else 0))
- + (if a2 then 1 else 0))
- + (if a1 then 1 else 0).
+(** Proofs that we have indeed opposite function (below 256) *)
+
+Theorem ascii_N_embedding :
+ forall a : ascii, ascii_of_N (N_of_ascii a) = a.
+Proof.
+ destruct a as [[|][|][|][|][|][|][|][|]]; vm_compute; reflexivity.
+Qed.
+
+Theorem N_ascii_embedding :
+ forall n:N, (n < 256)%N -> N_of_ascii (ascii_of_N n) = n.
+Proof.
+destruct n.
+reflexivity.
+do 8 (destruct p; [ | | intros; vm_compute; reflexivity ]);
+ intro H; vm_compute in H; destruct p; discriminate.
+Qed.
Theorem ascii_nat_embedding :
forall a : ascii, ascii_of_nat (nat_of_ascii a) = a.
@@ -108,6 +106,19 @@ Proof.
destruct a as [[|][|][|][|][|][|][|][|]]; compute; reflexivity.
Qed.
+Theorem nat_ascii_embedding :
+ forall n : nat, n < 256 -> nat_of_ascii (ascii_of_nat n) = n.
+Proof.
+ intros. unfold nat_of_ascii, ascii_of_nat.
+ rewrite N_ascii_embedding.
+ apply nat_of_N_of_nat.
+ unfold Nlt.
+ change 256%N with (N_of_nat 256).
+ rewrite <- N_of_nat_compare.
+ rewrite <- Compare_dec.nat_compare_lt. auto.
+Qed.
+
+
(** * Concrete syntax *)
(**