← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Strings/Ascii.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Strings/Ascii.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(* $Id: Ascii.v 9245 2006-10-17 12:53:34Z notin $ *)
 
10
 
 
11
(** Contributed by Laurent Th�ry (INRIA);
 
12
    Adapted to Coq V8 by the Coq Development Team *)
 
13
 
 
14
Require Import Bool.
 
15
Require Import BinPos.
 
16
 
 
17
(** * Definition of ascii characters *)
 
18
 
 
19
(** Definition of ascii character as a 8 bits constructor *)
 
20
 
 
21
Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).
 
22
 
 
23
Delimit Scope char_scope with char.
 
24
Bind Scope char_scope with ascii.
 
25
 
 
26
Definition zero := Ascii false false false false false false false false.
 
27
 
 
28
Definition one := Ascii true false false false false false false false.
 
29
 
 
30
Definition app1 (f : bool -> bool) (a : ascii) :=
 
31
  match a with
 
32
    | Ascii a1 a2 a3 a4 a5 a6 a7 a8 =>
 
33
      Ascii (f a1) (f a2) (f a3) (f a4) (f a5) (f a6) (f a7) (f a8)
 
34
  end.
 
35
 
 
36
Definition app2 (f : bool -> bool -> bool) (a b : ascii) :=
 
37
  match a, b with
 
38
    | Ascii a1 a2 a3 a4 a5 a6 a7 a8, Ascii b1 b2 b3 b4 b5 b6 b7 b8 =>
 
39
      Ascii (f a1 b1) (f a2 b2) (f a3 b3) (f a4 b4) 
 
40
      (f a5 b5) (f a6 b6) (f a7 b7) (f a8 b8)
 
41
  end.
 
42
 
 
43
Definition shift (c : bool) (a : ascii) :=
 
44
  match a with
 
45
    | Ascii a1 a2 a3 a4 a5 a6 a7 a8 => Ascii c a1 a2 a3 a4 a5 a6 a7
 
46
  end.
 
47
 
 
48
(** Definition of a decidable function that is effective *)
 
49
 
 
50
Definition ascii_dec : forall a b : ascii, {a = b} + {a <> b}.
 
51
  decide equality; apply bool_dec.
 
52
Defined.
 
53
 
 
54
(** * Conversion between natural numbers modulo 256 and ascii characters *)
 
55
 
 
56
(** Auxillary function that turns a positive into an ascii by
 
57
   looking at the last n bits, ie z mod 2^n *)
 
58
 
 
59
Fixpoint ascii_of_pos_aux (res acc : ascii) (z : positive) 
 
60
  (n : nat) {struct n} : ascii :=
 
61
  match n with
 
62
    | O => res
 
63
    | S n1 =>
 
64
      match z with
 
65
        | xH => app2 orb res acc
 
66
        | xI z' => ascii_of_pos_aux (app2 orb res acc) (shift false acc) z' n1
 
67
        | xO z' => ascii_of_pos_aux res (shift false acc) z' n1
 
68
      end
 
69
  end.
 
70
 
 
71
 
 
72
(** Function that turns a positive into an ascii by
 
73
    looking at the last 8 bits, ie a mod 8 *)
 
74
 
 
75
Definition ascii_of_pos (a : positive) := ascii_of_pos_aux zero one a 8.
 
76
 
 
77
(** Function that turns a Peano number into an ascii by converting it
 
78
    to positive *)
 
79
 
 
80
Definition ascii_of_nat (a : nat) :=
 
81
  match a with
 
82
    | O => zero
 
83
    | S a' => ascii_of_pos (P_of_succ_nat a')
 
84
  end.
 
85
 
 
86
(** The opposite function *)
 
87
 
 
88
Definition nat_of_ascii (a : ascii) : nat :=
 
89
  let (a1, a2, a3, a4, a5, a6, a7, a8) := a in
 
90
    2 *
 
91
    (2 *
 
92
      (2 *
 
93
        (2 *
 
94
          (2 *
 
95
            (2 *
 
96
              (2 * (if a8 then 1 else 0)
 
97
                + (if a7 then 1 else 0))
 
98
              + (if a6 then 1 else 0))
 
99
            + (if a5 then 1 else 0))
 
100
          + (if a4 then 1 else 0))
 
101
        + (if a3 then 1 else 0))
 
102
      + (if a2 then 1 else 0))
 
103
    + (if a1 then 1 else 0).
 
104
 
 
105
Theorem ascii_nat_embedding : 
 
106
  forall a : ascii, ascii_of_nat (nat_of_ascii a) = a.
 
107
Proof.
 
108
  destruct a as [[|][|][|][|][|][|][|][|]]; compute; reflexivity.
 
109
Qed.
 
110
 
 
111
(** * Concrete syntax *)
 
112
 
 
113
(**
 
114
  Ascii characters can be represented in scope char_scope as follows:
 
115
  - ["c"]   represents itself if c is a character of code < 128,
 
116
  - [""""]  is an exception: it represents the ascii character 34
 
117
            (double quote),
 
118
  - ["nnn"] represents the ascii character of decimal code nnn.
 
119
 
 
120
  For instance, both ["065"] and ["A"] denote the character `uppercase
 
121
  A', and both ["034"] and [""""] denote the character `double quote'.
 
122
 
 
123
  Notice that the ascii characters of code >= 128 do not denote
 
124
  stand-alone utf8 characters so that only the notation "nnn" is
 
125
  available for them (unless your terminal is able to represent them,
 
126
  which is typically not the case in coqide). 
 
127
*)
 
128
 
 
129
Open Local Scope char_scope.
 
130
 
 
131
Example Space := " ".
 
132
Example DoubleQuote := """".
 
133
Example Beep := "007".