blob: 43f006008de0ac958e72b0b4d6c3bcb75a0c2613 (
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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
|
Require Import Coq.Strings.Ascii Coq.Strings.String.
Require Import Coq.Numbers.BinNums.
Require Import Crypto.Util.Strings.Equality.
Require Crypto.Util.Pos.
Import BinPosDef.
Local Open Scope positive_scope.
Local Open Scope string_scope.
Fixpoint oct_string_of_pos' (p : positive) (rest : string) : string
:= match p with
| 1 => String "1" rest
| 2 => String "2" rest
| 3 => String "3" rest
| 4 => String "4" rest
| 5 => String "5" rest
| 6 => String "6" rest
| 7 => String "7" rest
| p'~0~0~0 => oct_string_of_pos' p' (String "0" rest)
| p'~0~0~1 => oct_string_of_pos' p' (String "1" rest)
| p'~0~1~0 => oct_string_of_pos' p' (String "2" rest)
| p'~0~1~1 => oct_string_of_pos' p' (String "3" rest)
| p'~1~0~0 => oct_string_of_pos' p' (String "4" rest)
| p'~1~0~1 => oct_string_of_pos' p' (String "5" rest)
| p'~1~1~0 => oct_string_of_pos' p' (String "6" rest)
| p'~1~1~1 => oct_string_of_pos' p' (String "7" rest)
end.
Definition oct_string_of_pos (p : positive) : string
:= String "0" (String "o" (oct_string_of_pos' p "")).
Local Notation default := 1.
Fixpoint pos_of_oct_string' (s : string) (rest : option positive)
: option positive
:= match s with
| "" => rest
| String ch s'
=> pos_of_oct_string'
s'
(if ascii_beq ch "0"
then match rest with
| Some p => Some (p~0~0~0)
| None => None
end
else if ascii_beq ch "1"
then match rest with
| Some p => Some (p~0~0~1)
| None => Some 1
end
else if ascii_beq ch "2"
then match rest with
| Some p => Some (p~0~1~0)
| None => Some 2
end
else if ascii_beq ch "3"
then match rest with
| Some p => Some (p~0~1~1)
| None => Some 3
end
else if ascii_beq ch "4"
then match rest with
| Some p => Some (p~1~0~0)
| None => Some 4
end
else if ascii_beq ch "5"
then match rest with
| Some p => Some (p~1~0~1)
| None => Some 5
end
else if ascii_beq ch "6"
then match rest with
| Some p => Some (p~1~1~0)
| None => Some 6
end
else if ascii_beq ch "7"
then match rest with
| Some p => Some (p~1~1~1)
| None => Some 7
end
else None)
end.
Definition pos_of_oct_string (s : string) : positive
:= match s with
| String s0 (String sb s)
=> if ascii_beq s0 "0"
then if ascii_beq sb "o"
then match pos_of_oct_string' s None with
| Some p => p
| None => default
end
else default
else default
| _ => default
end.
Fixpoint pos_oct_app (p q:positive) : positive :=
match q with
| 1 => p~0~0~1
| 2 => p~0~1~0
| 3 => p~0~1~1
| 4 => p~1~0~0
| 5 => p~1~0~1
| 6 => p~1~1~0
| 7 => p~1~1~1
| q~0~0~0 => (pos_oct_app p q)~0~0~0
| q~0~0~1 => (pos_oct_app p q)~0~0~1
| q~0~1~0 => (pos_oct_app p q)~0~1~0
| q~0~1~1 => (pos_oct_app p q)~0~1~1
| q~1~0~0 => (pos_oct_app p q)~1~0~0
| q~1~0~1 => (pos_oct_app p q)~1~0~1
| q~1~1~0 => (pos_oct_app p q)~1~1~0
| q~1~1~1 => (pos_oct_app p q)~1~1~1
end.
Fixpoint pos_of_oct_string_of_pos' (p : positive)
(base : option positive)
(rest : string)
: pos_of_oct_string' (oct_string_of_pos' p rest) base
= pos_of_oct_string' rest (match base with
| None => Some p
| Some v => Some (pos_oct_app v p)
end).
Proof.
do 3 try destruct p as [p|p|]; destruct base; try reflexivity;
cbn; rewrite pos_of_oct_string_of_pos'; reflexivity.
Qed.
Lemma pos_of_oct_string_of_pos (p : positive)
: pos_of_oct_string (oct_string_of_pos p) = p.
Proof.
cbn; rewrite pos_of_oct_string_of_pos'; reflexivity.
Qed.
Example oct_string_of_pos_1 : oct_string_of_pos 1 = "0o1" := eq_refl.
Example oct_string_of_pos_2 : oct_string_of_pos 2 = "0o2" := eq_refl.
Example oct_string_of_pos_3 : oct_string_of_pos 3 = "0o3" := eq_refl.
Example oct_string_of_pos_7 : oct_string_of_pos 7 = "0o7" := eq_refl.
Example oct_string_of_pos_8 : oct_string_of_pos 8 = "0o10" := eq_refl.
|
