From 3b60b6cc432a0e6b6156b6ec969f4fb28f67d1aa Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Wed, 28 Feb 2024 10:53:47 +0100
Subject: [PATCH 1/2] Implement a general Show typeclass in MetaCoq.Utils

---
 common/theories/Primitive.v                   | 15 -----
 erasure-plugin/theories/Erasure.v             |  2 +
 erasure/theories/EBeta.v                      | 12 ++--
 erasure/theories/EPretty.v                    |  4 +-
 pcuic/theories/utils/PCUICPretty.v            | 14 ++--
 template-coq/_PluginProject                   |  4 ++
 template-coq/_PluginProject.in                |  4 ++
 .../gen-src/metacoq_template_plugin.mlpack    |  2 +
 utils/_CoqProject                             |  1 +
 utils/theories/MCUtils.v                      |  3 +-
 utils/theories/Show.v                         | 64 +++++++++++++++++++
 11 files changed, 95 insertions(+), 30 deletions(-)
 create mode 100644 utils/theories/Show.v

diff --git a/common/theories/Primitive.v b/common/theories/Primitive.v
index c3de3770a..f8283f6fc 100644
--- a/common/theories/Primitive.v
+++ b/common/theories/Primitive.v
@@ -9,18 +9,3 @@ Variant prim_tag :=
   | primFloat
   | primArray.
 Derive NoConfusion EqDec for prim_tag.
-
-Definition string_of_prim_int (i:Uint63.int) : string :=
-  (* Better? DecimalString.NilZero.string_of_uint (BinNat.N.to_uint (BinInt.Z.to_N (Int63.to_Z i))). ? *)
-  string_of_Z (Uint63.to_Z i).
-
-Definition string_of_float (f : PrimFloat.float) : string :=
-  match Prim2SF f with
-  | S754_zero sign => if sign then "-0" else "0"
-  | S754_infinity sign => if sign then "-INFINITY" else "INFINITY"
-  | S754_nan => "NAN"
-  | S754_finite sign p z =>
-    let abs := "0x" ++ bytestring.String.of_string (Numbers.HexadecimalString.NilZero.string_of_uint (Pos.to_hex_uint p)) ++ "p" ++
-      bytestring.String.of_string (Numbers.DecimalString.NilZero.string_of_int (Z.to_int z))
-    in if sign then "-" ++ abs else abs
-  end.
\ No newline at end of file
diff --git a/erasure-plugin/theories/Erasure.v b/erasure-plugin/theories/Erasure.v
index f24a1d62c..261a273b2 100644
--- a/erasure-plugin/theories/Erasure.v
+++ b/erasure-plugin/theories/Erasure.v
@@ -109,6 +109,8 @@ Program Definition optional_unsafe_transforms econf :=
     unbox_transformation efl final_wcbv_flags ▷
     inline_transformation efl final_wcbv_flags econf.(inlining) ▷
     forget_inlining_info_transformation efl final_wcbv_flags ▷
+    (* Heuristically do it twice for more beta-normal terms *)
+    betared_transformation efl final_wcbv_flags ▷
     betared_transformation efl final_wcbv_flags).
 
 Program Definition verified_lambdabox_pipeline {guard : abstract_guard_impl}
diff --git a/erasure/theories/EBeta.v b/erasure/theories/EBeta.v
index 75adc987d..a4b9cd1cf 100644
--- a/erasure/theories/EBeta.v
+++ b/erasure/theories/EBeta.v
@@ -19,17 +19,13 @@ Definition map_subterms (f : term -> term) (t : term) : term :=
   | tLazy t => tLazy (f t)
   | tForce t => tForce (f t)
   | tConstruct ind n args => tConstruct ind n (map f args)
-  | t => t
+  | tRel n => tRel n
+  | tVar na => tVar na
+  | tConst kn => tConst kn
+  | tBox => tBox
   end.
 
 Section betared.
-  Fixpoint decompose_lam (t : term) {struct t} : list name × term :=
-    match t with
-    | tLambda na B =>
-      let (ns, B0) := decompose_lam B in
-      (na :: ns, B0)
-    | _ => ([], t)
-    end.
 
   Fixpoint beta_body (body : term) (args : list term) {struct args} : term :=
     match args with
diff --git a/erasure/theories/EPretty.v b/erasure/theories/EPretty.v
index 97e6a2081..9c99f2e64 100644
--- a/erasure/theories/EPretty.v
+++ b/erasure/theories/EPretty.v
@@ -86,8 +86,8 @@ Module PrintTermTree.
 
     Definition print_prim (soft : EAst.term -> Tree.t) (p : @prim_val EAst.term) : Tree.t :=
       match p.π2 return Tree.t with
-      | primIntModel f => "(int: " ^ Primitive.string_of_prim_int f ^ ")"
-      | primFloatModel f => "(float: " ^ Primitive.string_of_float f ^ ")"
+      | primIntModel f => "(int: " ^ show f ^ ")"
+      | primFloatModel f => "(float: " ^ show f ^ ")"
       | primArrayModel a => "(array:" ^ soft a.(array_default) ^ " , " ^ string_of_list soft a.(array_value) ^ ")"
       end.
 
diff --git a/pcuic/theories/utils/PCUICPretty.v b/pcuic/theories/utils/PCUICPretty.v
index 8a4ae2a42..94065d591 100644
--- a/pcuic/theories/utils/PCUICPretty.v
+++ b/pcuic/theories/utils/PCUICPretty.v
@@ -119,8 +119,8 @@ Module PrintTermTree.
 
     Definition print_prim (soft : term -> Tree.t) (p : prim_val) : Tree.t :=
       match p.π2 return Tree.t with
-      | primIntModel f => "(int: " ^ Primitive.string_of_prim_int f ^ ")"
-      | primFloatModel f => "(float: " ^ Primitive.string_of_float f ^ ")"
+      | primIntModel f => "(int: " ^ show f ^ ")"
+      | primFloatModel f => "(float: " ^ show f ^ ")"
       | primArrayModel a => "(array:" ^ string_of_list soft a.(array_value) ^ ")"
       end.
 
@@ -128,7 +128,7 @@ Module PrintTermTree.
       Context (print_term : list ident -> bool -> bool -> term -> t).
 
       Definition print_def {A} (f : A -> t) (g : A -> t) (def : def A) :=
-        string_of_name (binder_name (dname def)) ^ " { struct " ^ string_of_nat (rarg def) ^ " }" ^
+        string_of_name (binder_name (dname def)) ^ " { struct " ^ show (rarg def) ^ " }" ^
                     " : " ^ f (dtype def) ^ " := " ^ nl ^ g (dbody def).
 
       Definition print_defs Γ (defs : mfixpoint term) :=
@@ -344,5 +344,11 @@ Definition print_context Σ Γ Δ : string :=
 Definition print_env (short : bool) (prefix : nat) Σ :=
   Tree.to_string (PrintTermTree.print_env short prefix Σ).
 
+#[export] Instance show_env : Show global_env :=
+  fun Σ => print_env false (List.length Σ.(declarations)) Σ.
+
 Definition print_program (short : bool) (prefix : nat) (p : program) : string :=
-  Tree.to_string (PrintTermTree.print_program short prefix p).
\ No newline at end of file
+  Tree.to_string (PrintTermTree.print_program short prefix p).
+
+#[export] Instance show_program : Show program :=
+  fun p => print_program false (List.length p.1.(declarations)) p.
diff --git a/template-coq/_PluginProject b/template-coq/_PluginProject
index e8ff059f6..f23af2660 100644
--- a/template-coq/_PluginProject
+++ b/template-coq/_PluginProject
@@ -143,6 +143,10 @@ gen-src/mCRelations.ml
 gen-src/mCRelations.mli
 gen-src/mCString.ml
 gen-src/mCString.mli
+gen-src/sint63.mli
+gen-src/sint63.ml
+gen-src/show.mli
+gen-src/show.ml
 # gen-src/mCUint63.ml
 # gen-src/mCUint63.mli
 gen-src/mCUtils.ml
diff --git a/template-coq/_PluginProject.in b/template-coq/_PluginProject.in
index 1532dfeba..a86fea10d 100644
--- a/template-coq/_PluginProject.in
+++ b/template-coq/_PluginProject.in
@@ -141,6 +141,10 @@ gen-src/mCRelations.ml
 gen-src/mCRelations.mli
 gen-src/mCString.ml
 gen-src/mCString.mli
+gen-src/sint63.mli
+gen-src/sint63.ml
+gen-src/show.mli
+gen-src/show.ml
 # gen-src/mCUint63.ml
 # gen-src/mCUint63.mli
 gen-src/mCUtils.ml
diff --git a/template-coq/gen-src/metacoq_template_plugin.mlpack b/template-coq/gen-src/metacoq_template_plugin.mlpack
index 9886d3375..8895f7328 100644
--- a/template-coq/gen-src/metacoq_template_plugin.mlpack
+++ b/template-coq/gen-src/metacoq_template_plugin.mlpack
@@ -76,6 +76,8 @@ PrimFloat
 FloatOps
 DecimalString
 MCString
+Sint63
+Show
 MCUtils
 Signature
 All_Forall
diff --git a/utils/_CoqProject b/utils/_CoqProject
index 9f0b08c4e..600c73719 100644
--- a/utils/_CoqProject
+++ b/utils/_CoqProject
@@ -31,6 +31,7 @@ theories/MC_ExtrOCamlInt63.v
 theories/MC_ExtrOCamlZPosInt.v
 theories/ReflectEq.v
 theories/monad_utils.v
+theories/Show.v
 theories/utils.v
 
 # extra tactics
diff --git a/utils/theories/MCUtils.v b/utils/theories/MCUtils.v
index d066b02e4..15dba02bb 100644
--- a/utils/theories/MCUtils.v
+++ b/utils/theories/MCUtils.v
@@ -1,6 +1,6 @@
 From Coq Require Import Nat ZArith Bool.
 
-Require Export MCPrelude
+From MetaCoq.Utils Require Export MCPrelude
         MCReflect
         All_Forall
         MCArith
@@ -23,6 +23,7 @@ Require Export MCPrelude
         MCTactics.UniquePose
         ReflectEq
         bytestring
+        Show
 .
 
 Tactic Notation "destruct" "?" :=
diff --git a/utils/theories/Show.v b/utils/theories/Show.v
new file mode 100644
index 000000000..9f3f38704
--- /dev/null
+++ b/utils/theories/Show.v
@@ -0,0 +1,64 @@
+From Coq Require Import PArith Sint63 String Uint63 PrimFloat SpecFloat FloatOps.
+From MetaCoq.Utils Require Import bytestring MCString.
+
+Local Open Scope bs_scope.
+
+Class Show (A : Type) := show : A -> string.
+Global Hint Mode Show ! : typeclass_instances.
+
+#[export] Instance show_bytestring : Show string := fun x => x.
+
+#[export] Instance show_string : Show String.string := bytestring.String.of_string.
+
+Definition string_show {A} {show : Show A} : A -> String.string :=
+  fun a => bytestring.String.to_string (show a).
+
+#[export] Instance nat_show : Show nat := string_of_nat.
+
+Definition string_of_bool b := if (b : bool) then "true" else "false".
+
+#[export] Instance show_bool : Show bool := string_of_bool.
+#[export] Instance show_pair {A B} {showA : Show A} {showB : Show B}: Show (A * B) :=
+  { show '(x, y) := "(" ++ show x ++ ", " ++ show y ++ ")" }.
+
+#[export] Instance show_sum {A B} {showA : Show A} {showB : Show B}: Show (A + B) :=
+  { show x := match x with
+    | inl x => "(inl " ++ show x ++ ")"
+    | inr x => "(inr " ++ show x ++ ")"
+    end
+    }.
+
+Definition string_of_option {A} (fn : A -> string) (x : option A) : string :=
+  match x with
+  | None => "None"
+  | Some x => "(Some " ++ fn x ++ ")"
+  end.
+
+#[export] Instance show_option {A} {showA : Show A}: Show (option A) := string_of_option show.
+
+#[export] Instance show_list {A} {SA : Show A} : Show (list A) := string_of_list show.
+
+Import SpecFloat.
+Definition string_of_specfloat (f : SpecFloat.spec_float) :=
+  match f with
+  | S754_zero sign => if sign then "-0" else "0"
+  | S754_infinity sign => if sign then "-infinity" else "infinity"
+  | S754_nan => "nan"
+  | S754_finite sign p z =>
+  let num := string_of_positive p ++ "p" ++ string_of_Z z in
+  if sign then "-" ++ num else num
+  end.
+
+Definition string_of_prim_int (i:Uint63.int) : string :=
+  (* Better? DecimalString.NilZero.string_of_uint (BinNat.N.to_uint (BinInt.Z.to_N (Int63.to_Z i))). ? *)
+  string_of_Z (Uint63.to_Z i).
+
+Definition string_of_float (f : PrimFloat.float) : string :=
+  string_of_specfloat (FloatOps.Prim2SF f).
+
+#[export] Instance show_uint : Show PrimInt63.int := string_of_prim_int.
+#[export] Instance show_sint : Show int_wrapper := { show x := string_of_Z (Sint63.to_Z (x.(int_wrap))) }.
+#[export] Instance show_specfloat : Show SpecFloat.spec_float := string_of_specfloat.
+#[export] Instance show_float : Show PrimFloat.float := string_of_float.
+#[export] Instance show_positive : Show positive := string_of_positive.
+#[export] Instance show_Z : Show Z := string_of_Z.

From 4603eafe4e689f4e850286b862d4fb1f71788c2c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Wed, 28 Feb 2024 11:32:10 +0100
Subject: [PATCH 2/2] Fix dependencies of new template-coq plugin

---
 template-coq/_PluginProject                         | 6 ++----
 template-coq/_PluginProject.in                      | 6 ++----
 template-coq/gen-src/metacoq_template_plugin.mlpack | 2 --
 3 files changed, 4 insertions(+), 10 deletions(-)

diff --git a/template-coq/_PluginProject b/template-coq/_PluginProject
index f23af2660..cb59a88eb 100644
--- a/template-coq/_PluginProject
+++ b/template-coq/_PluginProject
@@ -68,8 +68,6 @@ gen-src/decidableType.ml
 gen-src/decidableType.mli
 gen-src/decimal.ml
 gen-src/decimal.mli
-gen-src/decimalString.ml
-gen-src/decimalString.mli
 gen-src/denoter.ml
 # gen-src/depElim.ml
 # gen-src/depElim.mli
@@ -103,8 +101,8 @@ gen-src/floatOps.ml
 gen-src/floatOps.mli
 gen-src/hexadecimal.ml
 gen-src/hexadecimal.mli
-gen-src/hexadecimalString.ml
-gen-src/hexadecimalString.mli
+# gen-src/hexadecimalString.ml
+# gen-src/hexadecimalString.mli
 gen-src/induction.ml
 gen-src/induction.mli
 # gen-src/init.ml
diff --git a/template-coq/_PluginProject.in b/template-coq/_PluginProject.in
index a86fea10d..110bb8575 100644
--- a/template-coq/_PluginProject.in
+++ b/template-coq/_PluginProject.in
@@ -66,8 +66,6 @@ gen-src/decidableType.ml
 gen-src/decidableType.mli
 gen-src/decimal.ml
 gen-src/decimal.mli
-gen-src/decimalString.ml
-gen-src/decimalString.mli
 gen-src/denoter.ml
 # gen-src/depElim.ml
 # gen-src/depElim.mli
@@ -101,8 +99,8 @@ gen-src/floatOps.ml
 gen-src/floatOps.mli
 gen-src/hexadecimal.ml
 gen-src/hexadecimal.mli
-gen-src/hexadecimalString.ml
-gen-src/hexadecimalString.mli
+# gen-src/hexadecimalString.ml
+# gen-src/hexadecimalString.mli
 gen-src/induction.ml
 gen-src/induction.mli
 # gen-src/init.ml
diff --git a/template-coq/gen-src/metacoq_template_plugin.mlpack b/template-coq/gen-src/metacoq_template_plugin.mlpack
index 8895f7328..aeeae114c 100644
--- a/template-coq/gen-src/metacoq_template_plugin.mlpack
+++ b/template-coq/gen-src/metacoq_template_plugin.mlpack
@@ -25,7 +25,6 @@ Caml_byte
 ByteCompare
 ByteCompareSpec
 String0
-HexadecimalString
 Orders
 OrdersAlt
 OrdersTac
@@ -74,7 +73,6 @@ Zpower
 SpecFloat
 PrimFloat
 FloatOps
-DecimalString
 MCString
 Sint63
 Show