From 64beea53759777d3ea598040fc703b06a939dcd6 Mon Sep 17 00:00:00 2001
From: Robert Zhang <jiaxuanzhang066@gmail.com>
Date: Tue, 4 Jul 2023 10:19:30 -0700
Subject: [PATCH] read Ltac2 integer bits using bitwise right shift (#355)

* read Ltac2 integer bits using bitwise right shift

Now that Ltac2 [supports](https://github.com/coq/coq/pull/15637) integer
operations like the bitwise right shift (`Int.lsr`), we can use it
directly for converting an Ltac2 integer into a bool list representation
of its bits, obviating the original workaround.

* simplify int_to_bits_rec

* fix typo and elaborate on comment

* minor refactor in LiveParsing.v
---
 .gitignore                              |  2 ++
 LiveVerif/src/LiveVerif/LiveParsing.v   |  2 +-
 bedrock2/src/bedrock2/ident_to_string.v | 28 +++++++------------------
 3 files changed, 10 insertions(+), 22 deletions(-)

diff --git a/.gitignore b/.gitignore
index fe975fae..46dd803d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -31,6 +31,8 @@ Makefile.coq*
 /end2end/admits.txt
 /end2end/admits1perLine.txt
 
+.vscode
+
 # _CoqProject is generated by the Makefile
 _CoqProject
 
diff --git a/LiveVerif/src/LiveVerif/LiveParsing.v b/LiveVerif/src/LiveVerif/LiveParsing.v
index 724cdaed..5f16a058 100644
--- a/LiveVerif/src/LiveVerif/LiveParsing.v
+++ b/LiveVerif/src/LiveVerif/LiveParsing.v
@@ -12,7 +12,7 @@ Require Import Ltac2.Ltac2.
 
 Ltac2 exact_basename_string_of_ref_constr(c: constr) :=
   let ref := reference_of_constr c in
-  let s := ident_to_string.string_to_coq (Ident.to_string (List.last (Env.path ref))) in
+  let s := ident_to_coq (List.last (Env.path ref)) in
   exact $s.
 
 Ltac exact_basename_string_of_ref_constr :=
diff --git a/bedrock2/src/bedrock2/ident_to_string.v b/bedrock2/src/bedrock2/ident_to_string.v
index 04d202ae..8fe40e7a 100644
--- a/bedrock2/src/bedrock2/ident_to_string.v
+++ b/bedrock2/src/bedrock2/ident_to_string.v
@@ -1,29 +1,15 @@
 Require Import Coq.Strings.String.
 Require Import Ltac2.Ltac2.
-Require Ltac2.Option.
-
-(* Takes a list of powers instead of one power and dividing because
-   Ltac2 does not have integer division: https://github.com/coq/coq/issues/13802 *)
-Ltac2 rec int_to_bits_rec(powers: int list)(val: int) :=
-  match powers with
-  | p :: rest =>
-    if Int.le p val
-    then true :: int_to_bits_rec rest (Int.sub val p)
-    else false :: int_to_bits_rec rest val
-  | [] => []
-  end.
 
-(* [2^(n-1); ..., 2^0] *)
-Ltac2 rec powers_of_two(n: int) :=
-  if Int.equal n 1 then [1] else
-  let r := powers_of_two (Int.sub n 1) in
-  match r with
-  | h :: t => Int.mul 2 h :: r
-  | [] => []
-  end.
+(* Converts the lower i + 1 bits of an Ltac2 integer into a bool list
+  (lower bits to the left) where 0 is false and 1 is true *)
+Ltac2 rec int_to_bits_rec(val: int)(i: int) :=
+  if Int.lt i 0 then [] else
+    (Int.equal (Int.land (Int.lsr val i) 1) 1)
+      :: int_to_bits_rec val (Int.sub i 1).
 
 Ltac2 char_to_bits(c: char) :=
-  int_to_bits_rec (powers_of_two 8) (Char.to_int c).
+  int_to_bits_rec (Char.to_int c) 7.
 
 Ltac2 bool_to_coq(b: bool) :=
   if b then constr:(true) else constr:(false).