From ccc79730a7585a3ce952c27d347b194562f4f473 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 9 Apr 2018 14:08:39 -0400 Subject: Update number/string conversions To updated version of https://github.com/coq/coq/pull/6597 --- _CoqProject | 6 +- src/Util/Strings/Binary.v | 72 ------------- src/Util/Strings/BinaryString.v | 139 +++++++++++++++++++++++++ src/Util/Strings/Hex.v | 219 --------------------------------------- src/Util/Strings/HexString.v | 221 ++++++++++++++++++++++++++++++++++++++++ src/Util/Strings/Octal.v | 138 ------------------------- src/Util/Strings/OctalString.v | 171 +++++++++++++++++++++++++++++++ 7 files changed, 534 insertions(+), 432 deletions(-) delete mode 100644 src/Util/Strings/Binary.v create mode 100644 src/Util/Strings/BinaryString.v delete mode 100644 src/Util/Strings/Hex.v create mode 100644 src/Util/Strings/HexString.v delete mode 100644 src/Util/Strings/Octal.v create mode 100644 src/Util/Strings/OctalString.v diff --git a/_CoqProject b/_CoqProject index 31249c067..4e5f33519 100644 --- a/_CoqProject +++ b/_CoqProject @@ -6513,11 +6513,11 @@ src/Util/Sigma/Associativity.v src/Util/Sigma/Lift.v src/Util/Sigma/MapProjections.v src/Util/Strings/Ascii.v -src/Util/Strings/Binary.v +src/Util/Strings/BinaryString.v src/Util/Strings/Decimal.v src/Util/Strings/Equality.v -src/Util/Strings/Hex.v -src/Util/Strings/Octal.v +src/Util/Strings/HexString.v +src/Util/Strings/OctalString.v src/Util/Strings/String.v src/Util/Tactics/BreakMatch.v src/Util/Tactics/CacheTerm.v diff --git a/src/Util/Strings/Binary.v b/src/Util/Strings/Binary.v deleted file mode 100644 index 955c6c8f6..000000000 --- a/src/Util/Strings/Binary.v +++ /dev/null @@ -1,72 +0,0 @@ -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 bin_string_of_pos' (p : positive) (rest : string) : string - := match p with - | 1 => String "1" rest - | p'~0 => bin_string_of_pos' p' (String "0" rest) - | p'~1 => bin_string_of_pos' p' (String "1" rest) - end. -Definition bin_string_of_pos (p : positive) : string - := String "0" (String "b" (bin_string_of_pos' p "")). - -Local Notation default := 1. - -Fixpoint pos_of_bin_string' (s : string) (rest : option positive) - : option positive - := match s with - | "" => rest - | String ch s' - => pos_of_bin_string' - s' - (if ascii_beq ch "0" - then option_map xO rest - else if ascii_beq ch "1" - then match rest with - | Some p => Some (xI p) - | None => Some xH - end - else None) - end. -Definition pos_of_bin_string (s : string) : positive - := match s with - | String s0 (String sb s) - => if ascii_beq s0 "0" - then if ascii_beq sb "b" - then match pos_of_bin_string' s None with - | Some p => p - | None => default - end - else default - else default - | _ => default - end. - -Lemma pos_of_bin_string_of_pos' (p : positive) - (base : option positive) - (rest : string) - : pos_of_bin_string' (bin_string_of_pos' p rest) base - = pos_of_bin_string' rest (match base with - | None => Some p - | Some v => Some (Pos.app v p) - end). -Proof. - revert base rest; induction p, base; intros; try reflexivity; - cbn; rewrite IHp; reflexivity. -Qed. - -Lemma pos_of_bin_string_of_pos (p : positive) - : pos_of_bin_string (bin_string_of_pos p) = p. -Proof. - cbn; rewrite pos_of_bin_string_of_pos'; reflexivity. -Qed. - -Example bin_string_of_pos_1 : bin_string_of_pos 1 = "0b1" := eq_refl. -Example bin_string_of_pos_2 : bin_string_of_pos 2 = "0b10" := eq_refl. -Example bin_string_of_pos_3 : bin_string_of_pos 3 = "0b11" := eq_refl. diff --git a/src/Util/Strings/BinaryString.v b/src/Util/Strings/BinaryString.v new file mode 100644 index 000000000..26c18ed51 --- /dev/null +++ b/src/Util/Strings/BinaryString.v @@ -0,0 +1,139 @@ +Require Import Coq.Strings.Ascii Coq.Strings.String. +Require Import Coq.Numbers.BinNums. +Import BinNatDef. +Import BinIntDef. +Import BinPosDef. + +Local Open Scope positive_scope. +Local Open Scope string_scope. + +Definition ascii_to_digit (ch : ascii) : option N + := (if ascii_dec ch "0" then Some 0 + else if ascii_dec ch "1" then Some 1 + else None)%N. + +Fixpoint pos_bin_app (p q:positive) : positive := + match q with + | q~0 => (pos_bin_app p q)~0 + | q~1 => (pos_bin_app p q)~1 + | 1 => p~1 + end. + +Module Raw. + Fixpoint of_pos (p : positive) (rest : string) : string + := match p with + | 1 => String "1" rest + | p'~0 => of_pos p' (String "0" rest) + | p'~1 => of_pos p' (String "1" rest) + end. + + Fixpoint to_N (s : string) (rest : N) + : N + := match s with + | "" => rest + | String ch s' + => to_N + s' + match ascii_to_digit ch with + | Some v => N.add v (N.double rest) + | None => N0 + end + end. + + Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N) + : to_N (of_pos p rest) base + = to_N rest match base with + | N0 => N.pos p + | Npos v => Npos (pos_bin_app v p) + end. + Proof. + destruct p as [p|p|]; destruct base; try reflexivity; + cbn; rewrite to_N_of_pos; reflexivity. + Qed. +End Raw. + +Definition of_pos (p : positive) : string + := String "0" (String "b" (Raw.of_pos p "")). +Definition of_N (n : N) : string + := match n with + | N0 => "0b0" + | Npos p => of_pos p + end. +Definition of_Z (z : Z) : string + := match z with + | Zneg p => String "-" (of_pos p) + | Z0 => "0b0" + | Zpos p => of_pos p + end. +Definition of_nat (n : nat) : string + := of_N (N.of_nat n). + +Definition to_N (s : string) : N + := match s with + | String s0 (String sb s) + => if ascii_dec s0 "0" + then if ascii_dec sb "b" + then Raw.to_N s N0 + else N0 + else N0 + | _ => N0 + end. +Definition to_pos (s : string) : positive + := match to_N s with + | N0 => 1 + | Npos p => p + end. +Definition to_Z (s : string) : Z + := let '(is_neg, n) := match s with + | String s0 s' + => if ascii_dec s0 "-" + then (true, to_N s') + else (false, to_N s) + | EmptyString => (false, to_N s) + end in + match n with + | N0 => Z0 + | Npos p => if is_neg then Zneg p else Zpos p + end. +Definition to_nat (s : string) : nat + := N.to_nat (to_N s). + +Lemma to_N_of_N (n : N) + : to_N (of_N n) + = n. +Proof. + destruct n; [ reflexivity | apply Raw.to_N_of_pos ]. +Qed. + +Lemma Z_of_of_Z (z : Z) + : to_Z (of_Z z) + = z. +Proof. + cbv [of_Z to_Z]; destruct z as [|z|z]; cbn; + try reflexivity; + rewrite Raw.to_N_of_pos; cbn; reflexivity. +Qed. + +Lemma to_nat_of_nat (n : nat) + : to_nat (of_nat n) + = n. +Proof. + cbv [to_nat of_nat]; + rewrite to_N_of_N, Nnat.Nat2N.id; reflexivity. +Qed. + +Lemma to_pos_of_pos (p : positive) + : to_pos (of_pos p) + = p. +Proof. + cbv [of_pos to_pos to_N]; cbn; + rewrite Raw.to_N_of_pos; cbn; reflexivity. +Qed. + +Example of_pos_1 : of_pos 1 = "0b1" := eq_refl. +Example of_pos_2 : of_pos 2 = "0b10" := eq_refl. +Example of_pos_3 : of_pos 3 = "0b11" := eq_refl. +Example of_N_0 : of_N 0 = "0b0" := eq_refl. +Example of_Z_0 : of_Z 0 = "0b0" := eq_refl. +Example of_Z_m1 : of_Z (-1) = "-0b1" := eq_refl. +Example of_nat_0 : of_nat 0 = "0b0" := eq_refl. diff --git a/src/Util/Strings/Hex.v b/src/Util/Strings/Hex.v deleted file mode 100644 index 62919901a..000000000 --- a/src/Util/Strings/Hex.v +++ /dev/null @@ -1,219 +0,0 @@ -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 bool_scope. -Local Open Scope positive_scope. -Local Open Scope string_scope. - -Fixpoint hex_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 - | 8 => String "8" rest - | 9 => String "9" rest - | 10 => String "a" rest - | 11 => String "b" rest - | 12 => String "c" rest - | 13 => String "d" rest - | 14 => String "e" rest - | 15 => String "f" rest - | p'~0~0~0~0 => hex_string_of_pos' p' (String "0" rest) - | p'~0~0~0~1 => hex_string_of_pos' p' (String "1" rest) - | p'~0~0~1~0 => hex_string_of_pos' p' (String "2" rest) - | p'~0~0~1~1 => hex_string_of_pos' p' (String "3" rest) - | p'~0~1~0~0 => hex_string_of_pos' p' (String "4" rest) - | p'~0~1~0~1 => hex_string_of_pos' p' (String "5" rest) - | p'~0~1~1~0 => hex_string_of_pos' p' (String "6" rest) - | p'~0~1~1~1 => hex_string_of_pos' p' (String "7" rest) - | p'~1~0~0~0 => hex_string_of_pos' p' (String "8" rest) - | p'~1~0~0~1 => hex_string_of_pos' p' (String "9" rest) - | p'~1~0~1~0 => hex_string_of_pos' p' (String "a" rest) - | p'~1~0~1~1 => hex_string_of_pos' p' (String "b" rest) - | p'~1~1~0~0 => hex_string_of_pos' p' (String "c" rest) - | p'~1~1~0~1 => hex_string_of_pos' p' (String "d" rest) - | p'~1~1~1~0 => hex_string_of_pos' p' (String "e" rest) - | p'~1~1~1~1 => hex_string_of_pos' p' (String "f" rest) - end. -Definition hex_string_of_pos (p : positive) : string - := String "0" (String "x" (hex_string_of_pos' p "")). - -Local Notation default := 1. - -Fixpoint pos_of_hex_string' (s : string) (rest : option positive) - : option positive - := match s with - | "" => rest - | String ch s' - => pos_of_hex_string' - s' - (if ascii_beq ch "0" - then match rest with - | Some p => Some (p~0~0~0~0) - | None => None - end - else if ascii_beq ch "1" - then match rest with - | Some p => Some (p~0~0~0~1) - | None => Some 1 - end - else if ascii_beq ch "2" - then match rest with - | Some p => Some (p~0~0~1~0) - | None => Some 2 - end - else if ascii_beq ch "3" - then match rest with - | Some p => Some (p~0~0~1~1) - | None => Some 3 - end - else if ascii_beq ch "4" - then match rest with - | Some p => Some (p~0~1~0~0) - | None => Some 4 - end - else if ascii_beq ch "5" - then match rest with - | Some p => Some (p~0~1~0~1) - | None => Some 5 - end - else if ascii_beq ch "6" - then match rest with - | Some p => Some (p~0~1~1~0) - | None => Some 6 - end - else if ascii_beq ch "7" - then match rest with - | Some p => Some (p~0~1~1~1) - | None => Some 7 - end - else if ascii_beq ch "8" - then match rest with - | Some p => Some (p~1~0~0~0) - | None => Some 8 - end - else if ascii_beq ch "9" - then match rest with - | Some p => Some (p~1~0~0~1) - | None => Some 9 - end - else if ascii_beq ch "a" || ascii_beq ch "A" - then match rest with - | Some p => Some (p~1~0~1~0) - | None => Some 10 - end - else if ascii_beq ch "b" || ascii_beq ch "B" - then match rest with - | Some p => Some (p~1~0~1~1) - | None => Some 11 - end - else if ascii_beq ch "c" || ascii_beq ch "C" - then match rest with - | Some p => Some (p~1~1~0~0) - | None => Some 12 - end - else if ascii_beq ch "d" || ascii_beq ch "D" - then match rest with - | Some p => Some (p~1~1~0~1) - | None => Some 13 - end - else if ascii_beq ch "e" || ascii_beq ch "E" - then match rest with - | Some p => Some (p~1~1~1~0) - | None => Some 14 - end - else if ascii_beq ch "f" || ascii_beq ch "F" - then match rest with - | Some p => Some (p~1~1~1~1) - | None => Some 15 - end - else None) - end. -Definition pos_of_hex_string (s : string) : positive - := match s with - | String s0 (String sb s) - => if ascii_beq s0 "0" - then if ascii_beq sb "x" - then match pos_of_hex_string' s None with - | Some p => p - | None => default - end - else default - else default - | _ => default - end. - -Fixpoint pos_hex_app (p q:positive) : positive := - match q with - | 1 => p~0~0~0~1 - | 2 => p~0~0~1~0 - | 3 => p~0~0~1~1 - | 4 => p~0~1~0~0 - | 5 => p~0~1~0~1 - | 6 => p~0~1~1~0 - | 7 => p~0~1~1~1 - | 8 => p~1~0~0~0 - | 9 => p~1~0~0~1 - | 10 => p~1~0~1~0 - | 11 => p~1~0~1~1 - | 12 => p~1~1~0~0 - | 13 => p~1~1~0~1 - | 14 => p~1~1~1~0 - | 15 => p~1~1~1~1 - | q~0~0~0~0 => (pos_hex_app p q)~0~0~0~0 - | q~0~0~0~1 => (pos_hex_app p q)~0~0~0~1 - | q~0~0~1~0 => (pos_hex_app p q)~0~0~1~0 - | q~0~0~1~1 => (pos_hex_app p q)~0~0~1~1 - | q~0~1~0~0 => (pos_hex_app p q)~0~1~0~0 - | q~0~1~0~1 => (pos_hex_app p q)~0~1~0~1 - | q~0~1~1~0 => (pos_hex_app p q)~0~1~1~0 - | q~0~1~1~1 => (pos_hex_app p q)~0~1~1~1 - | q~1~0~0~0 => (pos_hex_app p q)~1~0~0~0 - | q~1~0~0~1 => (pos_hex_app p q)~1~0~0~1 - | q~1~0~1~0 => (pos_hex_app p q)~1~0~1~0 - | q~1~0~1~1 => (pos_hex_app p q)~1~0~1~1 - | q~1~1~0~0 => (pos_hex_app p q)~1~1~0~0 - | q~1~1~0~1 => (pos_hex_app p q)~1~1~0~1 - | q~1~1~1~0 => (pos_hex_app p q)~1~1~1~0 - | q~1~1~1~1 => (pos_hex_app p q)~1~1~1~1 - end. - -Fixpoint pos_of_hex_string_of_pos' (p : positive) - (base : option positive) - (rest : string) - : pos_of_hex_string' (hex_string_of_pos' p rest) base - = pos_of_hex_string' rest (match base with - | None => Some p - | Some v => Some (pos_hex_app v p) - end). -Proof. - do 4 try destruct p as [p|p|]; destruct base; try reflexivity; - cbn; rewrite pos_of_hex_string_of_pos'; reflexivity. -Qed. - -Lemma pos_of_hex_string_of_pos (p : positive) - : pos_of_hex_string (hex_string_of_pos p) = p. -Proof. - cbn; rewrite pos_of_hex_string_of_pos'; reflexivity. -Qed. - -Example hex_string_of_pos_1 : hex_string_of_pos 1 = "0x1" := eq_refl. -Example hex_string_of_pos_2 : hex_string_of_pos 2 = "0x2" := eq_refl. -Example hex_string_of_pos_3 : hex_string_of_pos 3 = "0x3" := eq_refl. -Example hex_string_of_pos_7 : hex_string_of_pos 7 = "0x7" := eq_refl. -Example hex_string_of_pos_8 : hex_string_of_pos 8 = "0x8" := eq_refl. -Example hex_string_of_pos_9 : hex_string_of_pos 9 = "0x9" := eq_refl. -Example hex_string_of_pos_10 : hex_string_of_pos 10 = "0xa" := eq_refl. -Example hex_string_of_pos_11 : hex_string_of_pos 11 = "0xb" := eq_refl. -Example hex_string_of_pos_12 : hex_string_of_pos 12 = "0xc" := eq_refl. -Example hex_string_of_pos_13 : hex_string_of_pos 13 = "0xd" := eq_refl. -Example hex_string_of_pos_14 : hex_string_of_pos 14 = "0xe" := eq_refl. -Example hex_string_of_pos_15 : hex_string_of_pos 15 = "0xf" := eq_refl. -Example hex_string_of_pos_16 : hex_string_of_pos 16 = "0x10" := eq_refl. diff --git a/src/Util/Strings/HexString.v b/src/Util/Strings/HexString.v new file mode 100644 index 000000000..a6c9b04d4 --- /dev/null +++ b/src/Util/Strings/HexString.v @@ -0,0 +1,221 @@ +Require Import Coq.Strings.Ascii Coq.Strings.String. +Require Import Coq.Numbers.BinNums. +Import BinNatDef. +Import BinIntDef. +Import BinPosDef. + +Local Open Scope positive_scope. +Local Open Scope string_scope. + +Local Notation "a || b" + := (if a then true else if b then true else false). +Definition ascii_to_digit (ch : ascii) : option N + := (if ascii_dec ch "0" then Some 0 + else if ascii_dec ch "1" then Some 1 + else if ascii_dec ch "2" then Some 2 + else if ascii_dec ch "3" then Some 3 + else if ascii_dec ch "4" then Some 4 + else if ascii_dec ch "5" then Some 5 + else if ascii_dec ch "6" then Some 6 + else if ascii_dec ch "7" then Some 7 + else if ascii_dec ch "8" then Some 8 + else if ascii_dec ch "9" then Some 9 + else if ascii_dec ch "a" || ascii_dec ch "A" then Some 10 + else if ascii_dec ch "b" || ascii_dec ch "B" then Some 11 + else if ascii_dec ch "c" || ascii_dec ch "C" then Some 12 + else if ascii_dec ch "d" || ascii_dec ch "D" then Some 13 + else if ascii_dec ch "e" || ascii_dec ch "E" then Some 14 + else if ascii_dec ch "f" || ascii_dec ch "F" then Some 15 + else None)%N. + +Fixpoint pos_hex_app (p q:positive) : positive := + match q with + | 1 => p~0~0~0~1 + | 2 => p~0~0~1~0 + | 3 => p~0~0~1~1 + | 4 => p~0~1~0~0 + | 5 => p~0~1~0~1 + | 6 => p~0~1~1~0 + | 7 => p~0~1~1~1 + | 8 => p~1~0~0~0 + | 9 => p~1~0~0~1 + | 10 => p~1~0~1~0 + | 11 => p~1~0~1~1 + | 12 => p~1~1~0~0 + | 13 => p~1~1~0~1 + | 14 => p~1~1~1~0 + | 15 => p~1~1~1~1 + | q~0~0~0~0 => (pos_hex_app p q)~0~0~0~0 + | q~0~0~0~1 => (pos_hex_app p q)~0~0~0~1 + | q~0~0~1~0 => (pos_hex_app p q)~0~0~1~0 + | q~0~0~1~1 => (pos_hex_app p q)~0~0~1~1 + | q~0~1~0~0 => (pos_hex_app p q)~0~1~0~0 + | q~0~1~0~1 => (pos_hex_app p q)~0~1~0~1 + | q~0~1~1~0 => (pos_hex_app p q)~0~1~1~0 + | q~0~1~1~1 => (pos_hex_app p q)~0~1~1~1 + | q~1~0~0~0 => (pos_hex_app p q)~1~0~0~0 + | q~1~0~0~1 => (pos_hex_app p q)~1~0~0~1 + | q~1~0~1~0 => (pos_hex_app p q)~1~0~1~0 + | q~1~0~1~1 => (pos_hex_app p q)~1~0~1~1 + | q~1~1~0~0 => (pos_hex_app p q)~1~1~0~0 + | q~1~1~0~1 => (pos_hex_app p q)~1~1~0~1 + | q~1~1~1~0 => (pos_hex_app p q)~1~1~1~0 + | q~1~1~1~1 => (pos_hex_app p q)~1~1~1~1 + end. + +Module Raw. + Fixpoint 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 + | 8 => String "8" rest + | 9 => String "9" rest + | 10 => String "a" rest + | 11 => String "b" rest + | 12 => String "c" rest + | 13 => String "d" rest + | 14 => String "e" rest + | 15 => String "f" rest + | p'~0~0~0~0 => of_pos p' (String "0" rest) + | p'~0~0~0~1 => of_pos p' (String "1" rest) + | p'~0~0~1~0 => of_pos p' (String "2" rest) + | p'~0~0~1~1 => of_pos p' (String "3" rest) + | p'~0~1~0~0 => of_pos p' (String "4" rest) + | p'~0~1~0~1 => of_pos p' (String "5" rest) + | p'~0~1~1~0 => of_pos p' (String "6" rest) + | p'~0~1~1~1 => of_pos p' (String "7" rest) + | p'~1~0~0~0 => of_pos p' (String "8" rest) + | p'~1~0~0~1 => of_pos p' (String "9" rest) + | p'~1~0~1~0 => of_pos p' (String "a" rest) + | p'~1~0~1~1 => of_pos p' (String "b" rest) + | p'~1~1~0~0 => of_pos p' (String "c" rest) + | p'~1~1~0~1 => of_pos p' (String "d" rest) + | p'~1~1~1~0 => of_pos p' (String "e" rest) + | p'~1~1~1~1 => of_pos p' (String "f" rest) + end. + + Fixpoint to_N (s : string) (rest : N) + : N + := match s with + | "" => rest + | String ch s' + => to_N + s' + match ascii_to_digit ch with + | Some v => N.add v (N.mul 16 rest) + | None => N0 + end + end. + + Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N) + : to_N (of_pos p rest) base + = to_N rest match base with + | N0 => N.pos p + | Npos v => Npos (pos_hex_app v p) + end. + Proof. + do 4 try destruct p as [p|p|]; destruct base; try reflexivity; + cbn; rewrite to_N_of_pos; reflexivity. + Qed. +End Raw. + +Definition of_pos (p : positive) : string + := String "0" (String "x" (Raw.of_pos p "")). +Definition of_N (n : N) : string + := match n with + | N0 => "0x0" + | Npos p => of_pos p + end. +Definition of_Z (z : Z) : string + := match z with + | Zneg p => String "-" (of_pos p) + | Z0 => "0x0" + | Zpos p => of_pos p + end. +Definition of_nat (n : nat) : string + := of_N (N.of_nat n). + +Definition to_N (s : string) : N + := match s with + | String s0 (String so s) + => if ascii_dec s0 "0" + then if ascii_dec so "x" + then Raw.to_N s N0 + else N0 + else N0 + | _ => N0 + end. +Definition to_pos (s : string) : positive + := match to_N s with + | N0 => 1 + | Npos p => p + end. +Definition to_Z (s : string) : Z + := let '(is_neg, n) := match s with + | String s0 s' + => if ascii_dec s0 "-" + then (true, to_N s') + else (false, to_N s) + | EmptyString => (false, to_N s) + end in + match n with + | N0 => Z0 + | Npos p => if is_neg then Zneg p else Zpos p + end. +Definition to_nat (s : string) : nat + := N.to_nat (to_N s). + +Lemma to_N_of_N (n : N) + : to_N (of_N n) + = n. +Proof. + destruct n; [ reflexivity | apply Raw.to_N_of_pos ]. +Qed. + +Lemma to_Z_of_Z (z : Z) + : to_Z (of_Z z) + = z. +Proof. + cbv [of_Z to_Z]; destruct z as [|z|z]; cbn; + try reflexivity; + rewrite Raw.to_N_of_pos; cbn; reflexivity. +Qed. + +Lemma to_nat_of_nat (n : nat) + : to_nat (of_nat n) + = n. +Proof. + cbv [to_nat of_nat]; + rewrite to_N_of_N, Nnat.Nat2N.id; reflexivity. +Qed. + +Lemma to_pos_of_pos (p : positive) + : to_pos (of_pos p) + = p. +Proof. + cbv [of_pos to_pos to_N]; cbn; + rewrite Raw.to_N_of_pos; cbn; reflexivity. +Qed. + +Example of_pos_1 : of_pos 1 = "0x1" := eq_refl. +Example of_pos_2 : of_pos 2 = "0x2" := eq_refl. +Example of_pos_3 : of_pos 3 = "0x3" := eq_refl. +Example of_pos_7 : of_pos 7 = "0x7" := eq_refl. +Example of_pos_8 : of_pos 8 = "0x8" := eq_refl. +Example of_pos_9 : of_pos 9 = "0x9" := eq_refl. +Example of_pos_10 : of_pos 10 = "0xa" := eq_refl. +Example of_pos_11 : of_pos 11 = "0xb" := eq_refl. +Example of_pos_12 : of_pos 12 = "0xc" := eq_refl. +Example of_pos_13 : of_pos 13 = "0xd" := eq_refl. +Example of_pos_14 : of_pos 14 = "0xe" := eq_refl. +Example of_pos_15 : of_pos 15 = "0xf" := eq_refl. +Example of_pos_16 : of_pos 16 = "0x10" := eq_refl. +Example of_N_0 : of_N 0 = "0x0" := eq_refl. +Example of_Z_0 : of_Z 0 = "0x0" := eq_refl. +Example of_Z_m1 : of_Z (-1) = "-0x1" := eq_refl. +Example of_nat_0 : of_nat 0 = "0x0" := eq_refl. diff --git a/src/Util/Strings/Octal.v b/src/Util/Strings/Octal.v deleted file mode 100644 index 43f006008..000000000 --- a/src/Util/Strings/Octal.v +++ /dev/null @@ -1,138 +0,0 @@ -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. diff --git a/src/Util/Strings/OctalString.v b/src/Util/Strings/OctalString.v new file mode 100644 index 000000000..e771ad592 --- /dev/null +++ b/src/Util/Strings/OctalString.v @@ -0,0 +1,171 @@ +Require Import Coq.Strings.Ascii Coq.Strings.String. +Require Import Coq.Numbers.BinNums. +Import BinNatDef. +Import BinIntDef. +Import BinPosDef. + +Local Open Scope positive_scope. +Local Open Scope string_scope. + +Definition ascii_to_digit (ch : ascii) : option N + := (if ascii_dec ch "0" then Some 0 + else if ascii_dec ch "1" then Some 1 + else if ascii_dec ch "2" then Some 2 + else if ascii_dec ch "3" then Some 3 + else if ascii_dec ch "4" then Some 4 + else if ascii_dec ch "5" then Some 5 + else if ascii_dec ch "6" then Some 6 + else if ascii_dec ch "7" then Some 7 + else None)%N. + +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. + +Module Raw. + Fixpoint 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 => of_pos p' (String "0" rest) + | p'~0~0~1 => of_pos p' (String "1" rest) + | p'~0~1~0 => of_pos p' (String "2" rest) + | p'~0~1~1 => of_pos p' (String "3" rest) + | p'~1~0~0 => of_pos p' (String "4" rest) + | p'~1~0~1 => of_pos p' (String "5" rest) + | p'~1~1~0 => of_pos p' (String "6" rest) + | p'~1~1~1 => of_pos p' (String "7" rest) + end. + + Fixpoint to_N (s : string) (rest : N) + : N + := match s with + | "" => rest + | String ch s' + => to_N + s' + match ascii_to_digit ch with + | Some v => N.add v (N.mul 8 rest) + | None => N0 + end + end. + + Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N) + : to_N (of_pos p rest) base + = to_N rest match base with + | N0 => N.pos p + | Npos v => Npos (pos_oct_app v p) + end. + Proof. + do 3 try destruct p as [p|p|]; destruct base; try reflexivity; + cbn; rewrite to_N_of_pos; reflexivity. + Qed. +End Raw. + +Definition of_pos (p : positive) : string + := String "0" (String "o" (Raw.of_pos p "")). +Definition of_N (n : N) : string + := match n with + | N0 => "0o0" + | Npos p => of_pos p + end. +Definition of_Z (z : Z) : string + := match z with + | Zneg p => String "-" (of_pos p) + | Z0 => "0o0" + | Zpos p => of_pos p + end. +Definition of_nat (n : nat) : string + := of_N (N.of_nat n). + +Definition to_N (s : string) : N + := match s with + | String s0 (String so s) + => if ascii_dec s0 "0" + then if ascii_dec so "o" + then Raw.to_N s N0 + else N0 + else N0 + | _ => N0 + end. +Definition to_pos (s : string) : positive + := match to_N s with + | N0 => 1 + | Npos p => p + end. +Definition to_Z (s : string) : Z + := let '(is_neg, n) := match s with + | String s0 s' + => if ascii_dec s0 "-" + then (true, to_N s') + else (false, to_N s) + | EmptyString => (false, to_N s) + end in + match n with + | N0 => Z0 + | Npos p => if is_neg then Zneg p else Zpos p + end. +Definition to_nat (s : string) : nat + := N.to_nat (to_N s). + +Lemma to_N_of_N (n : N) + : to_N (of_N n) + = n. +Proof. + destruct n; [ reflexivity | apply Raw.to_N_of_pos ]. +Qed. + +Lemma to_Z_of_Z (z : Z) + : to_Z (of_Z z) + = z. +Proof. + cbv [of_Z to_Z]; destruct z as [|z|z]; cbn; + try reflexivity; + rewrite Raw.to_N_of_pos; cbn; reflexivity. +Qed. + +Lemma to_nat_of_nat (n : nat) + : to_nat (of_nat n) + = n. +Proof. + cbv [to_nat of_nat]; + rewrite to_N_of_N, Nnat.Nat2N.id; reflexivity. +Qed. + +Lemma to_pos_of_pos (p : positive) + : to_pos (of_pos p) + = p. +Proof. + cbv [of_pos to_pos to_N]; cbn; + rewrite Raw.to_N_of_pos; cbn; reflexivity. +Qed. + +Example of_pos_1 : of_pos 1 = "0o1" := eq_refl. +Example of_pos_2 : of_pos 2 = "0o2" := eq_refl. +Example of_pos_3 : of_pos 3 = "0o3" := eq_refl. +Example of_pos_7 : of_pos 7 = "0o7" := eq_refl. +Example of_pos_8 : of_pos 8 = "0o10" := eq_refl. +Example of_N_0 : of_N 0 = "0o0" := eq_refl. +Example of_Z_0 : of_Z 0 = "0o0" := eq_refl. +Example of_Z_m1 : of_Z (-1) = "-0o1" := eq_refl. +Example of_nat_0 : of_nat 0 = "0o0" := eq_refl. -- cgit v1.2.3