blob: a1ffe69527ff4e2b6b3f52c5b39b77a0286a8a81 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
Require Import Coq.Lists.List.
Require Import Coq.Strings.String Coq.Strings.Byte Coq.Strings.Ascii.
Import ListNotations.
Set Printing Depth 100000.
Set Printing Width 1000.
Close Scope char_scope.
Close Scope string_scope.
Open Scope byte_scope.
Print byte_rect.
Print byte_rec.
Print byte_ind.
Check "000".
Check "a".
Check "127".
Fail Check "€".
Close Scope byte_scope.
Open Scope char_scope.
Check "000".
Check "a".
Check "127".
Fail Check "€".
Close Scope char_scope.
Open Scope string_scope.
Check "000".
Check "a".
Check "127".
Check "€".
Check String "001" EmptyString.
Close Scope string_scope.
Compute ascii_of_byte "a".
Compute byte_of_ascii "a".
Compute string_of_list_byte ("a"::nil)%byte.
Compute list_byte_of_string "a".
Local Open Scope byte_scope.
Compute List.fold_right
(fun n ls => match Byte.of_nat n with
| Some b => cons b ls
| None => ls
end)
nil
(List.seq 0 256).
Local Close Scope byte_scope.
Local Open Scope char_scope.
Compute List.map Ascii.ascii_of_nat (List.seq 0 256).
Local Close Scope char_scope.
(* Test numeral notations for parameterized inductives *)
Module Test2.
Notation string := (list Byte.byte).
Definition id_string := @id string.
String Notation string id_string id_string : list_scope.
Check "abc"%list.
End Test2.
(* Test the via ... using ... option *)
Module Test3.
Inductive I :=
| IO : I
| IS : I -> I.
Definition of_byte (x : Byte.byte) : I :=
let fix f n :=
match n with
| O => IO
| S n => IS (f n)
end in
f (Byte.to_nat x).
Definition to_byte (x : I) : option Byte.byte :=
let fix f i :=
match i with
| IO => O
| IS i => S (f i)
end in
Byte.of_nat (f x).
String Notation nat of_byte to_byte (via I mapping [O => IO, S => IS]) : nat_scope.
Check "000".
Check "001".
Check "002".
Check "255".
Fail Check "256".
End Test3.
(* Test overlapping string notations *)
Module Test4.
Notation string1 := (list Byte.byte).
Definition id_string1 := @id string1.
String Notation string1 id_string1 id_string1 : list_scope.
Notation string2 := (list Ascii.ascii).
Definition a2b := List.map byte_of_ascii.
Definition b2a := List.map ascii_of_byte.
String Notation string2 b2a a2b : list_scope.
Check "abc"%list.
Check ["a";"b";"c"]%char%list : string2.
Check ["a";"b";"c"]%byte%list : string1.
End Test4.
|
