1 files changed, 138 insertions, 0 deletions
diff --git a/src/Util/Strings/Octal.v b/src/Util/Strings/Octal.v
new file mode 100644
index 000000000..43f006008
--- /dev/null
+++ b/src/Util/Strings/Octal.v
@@ -0,0 +1,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.