Allow erasure evaluation to be called through a new ERASEcast construct

.nix/config.nix

@@ -49,17 +49,14 @@ with (import <nixpkgs> {}).lib;
   bundles.default = {
     ## You can override Rocq and other Rocq rocqPackages
     ## through the following attribute
-    rocqPackages.rocq-core.override.version = "master";
-    rocqPackages.coq-core.override.version = "master";
-
+    rocqPackages.rocq-core.override.version = "7bedc37a9fb4c7bd340349324104e672d29203be";
+    rocqPackages.coq-core.override.version = "7bedc37a9fb4c7bd340349324104e672d29203be";
+    coqPackages.coq.override.version = "7bedc37a9fb4c7bd340349324104e672d29203be";
     ## You can override Coq and other Coq coqPackages
     ## through the following attribute
     coqPackages.equations.override.version = "main";
-    coqPackages.coq.override.version = "master";
-
-    coqPackages.metarocq.override.version = "main";
-
-    coqPackages.ceres.override.version = "0.4.1";
+    coqPackages.metarocq.override.version = "#1173";
+    coqPackages.ceres.override.version = "master";
 
     ## In some cases, light overrides are not available/enough
     ## in which case you can use either

examples/erase-conv/fib.v

@@ -0,0 +1,30 @@
+From VerifiedExtraction Require Import Extraction.
+
+Set Verified Extraction Build Directory "_build".
+
+(* Set Debug "verified-extraction". *)
+
+Set Verified Extraction Timing.
+Set Verified Extraction Format.
+Set Verified Extraction Optimize.
+
+(* Definition foo := (@eq_refl bool false <<<: (false = negb true)). *)
+
+From Stdlib Require Import Arith.
+
+Fixpoint fib (n : nat) := 
+  match n with
+  | 0 => 0
+  | 1 => 1
+  | S (S n as m) => fib m + fib n
+  end.
+
+Time Definition fib2 := Eval compute in fib 2.
+(* Check (ltac2:(erase_nocheck (fib 2) fib2)). *)
+
+Definition longtest (x: unit) := 
+  let x := fib 30 in match x with 0 => tt | S _ => tt end.
+Time Definition fib23 := Eval vm_compute in longtest tt.
+(* 0.2s *)
+Time Definition efib23 := ltac2:(erase_forget (longtest tt)).
+(* 0.3s total, 0.09s runing time *)

lib/rocq_verified_extraction_plugin/lib/verified_extraction.mli

@@ -87,4 +87,6 @@ val extract :
 
 val eval_plugin : ?loc:Loc.t -> malfunction_command_args list -> Libnames.qualid -> unit
 
-val eval : ?loc:Loc.t -> malfunction_command_args list -> Libnames.qualid -> Constr.t
+val eval : ?loc:Loc.t -> malfunction_command_args list -> Libnames.qualid -> Constr.t
+
+val install_erase_conv : malfunction_compilation_function -> unit

plugin/plugin-bootstrap/Extraction.v

@@ -1,4 +1,9 @@
+(** The plugin loader *)
 From VerifiedExtraction Require Export Loader.
-From Malfunction Require Export PrintMli.
+(* From Malfunction Require Export PrintMli. *)
 
+(** Bindings to primitive type implementations. *)
 From VerifiedExtraction Require Export PrimInt63 PrimFloat PrimArray PrimString RocqMsgFFI.
+
+(** Ltac2 tactics using the erasure cast for reflexive proofs. *)
+From VerifiedExtraction Require Export Tactics.

plugin/plugin-bootstrap/Tactics.v

@@ -0,0 +1,80 @@
+From VerifiedExtraction Require Import Loader.
+From Ltac2 Require Import Ltac2.
+
+Inductive value_of {A} : A -> Type := 
+  | value_is a : value_of a.
+Definition get_value_of {A} {a : A} (c : value_of a) : A := 
+  let 'value_is a := c in a.
+
+Lemma value_of_eq {A} {a : A} (c : value_of a) : get_value_of c = a.
+Proof. destruct c. reflexivity. Defined. 
+
+(** Runs erasure evaluation only once, in the kernel (if paired with Std.exact). 
+  Beware that no check is performed that the cast is correct when using this in a tactic.
+  It will be checked at Qed-time only. *)
+Ltac2 erase_nocheck c v := 
+  let vty := Constr.type c in
+  let c := Constr.Unsafe.make (Constr.Unsafe.Cast constr:(@value_is $vty $v) Constr.Cast.erase constr:(@value_of $vty $c)) in
+  c.
+
+(** Runs erasure evaluation twice, first to find the value during elaboration, 
+    then to check in the kernel *)
+Ltac2 erase_compute c := 
+  let vty := Constr.type c in
+  let c := Constr.pretype preterm:(@value_is $vty _ <<<: @value_of $vty $c) in
+  c.
+
+(** Helper to extract the value from an `value_of` term and apply `value_of_eq` to 
+  produce an equality. *)
+Ltac2 show_value c :=
+  let ty := Constr.type c in
+  match Constr.Unsafe.kind ty with
+  | Constr.Unsafe.App _ args =>
+    let car := Array.get args 0 in
+    let computed := Array.get args 1 in
+    let term := constr:(@get_value_of $car $computed $c) in
+    let cres := eval hnf in $term in
+    Std.exact_no_check constr:(value_of_eq $c : $computed = $cres)
+  | _ => Control.throw (Invalid_argument None)
+  end.
+
+(** Wrappers and notations for the primitives. *)
+
+(** Use `erase_nocheck t v` to get a proof through erasure evaluation that `t` is equal to `v`. 
+  The evaluation will happen only when this proof is typechecked by the kernel.
+  If `v` is not a value, standard conversion will apply to convert it to `t`'s value found by erased evaluation. *)
+Ltac2 erase_nocheck0 t v := show_value (erase_nocheck t v).
+Ltac2 Notation "erase_nocheck" t(constr) v(constr) := erase_nocheck0 t v.
+
+(** Use `erase_compute t` to find out the value `v` through erasure evaluation and get a proof that `t` equals `v`. 
+  This requires running evaluation twice. I.e. if used in a proof it will run evaluation at the tactic call and again at 
+  qed time.
+*)
+Ltac2 erase_compute0 t := show_value (erase_compute t).
+Ltac2 Notation "erase_compute" t(constr) := erase_compute0 t.
+
+(** Just compute the value associated to `t` during elaboration and throw away the proof that it comes from `t`. 
+  This runs evaluation only once. *)
+Ltac2 erase_forget0 t := 
+  let vty := Constr.type t in
+  let c := Constr.pretype preterm:(@value_is $vty _ <<<: @value_of $vty $t) in
+  match Constr.Unsafe.kind_nocast c with 
+  | Constr.Unsafe.App _compute args => Std.exact_no_check (Array.get args 1)
+  | _ => Control.throw (Invalid_argument None)
+  end.
+Ltac2 Notation "erase_forget" t(constr) := erase_forget0 t.
+
+Ltac2 Notation "value_of" c(constr) := show_value c.
+
+(* Tests *)
+(*
+Definition foo (x : unit) := true.
+
+Definition test := ltac2:(erase_nocheck (foo tt) true).
+(* Check test : foo tt = true. *)
+
+Definition testevar := ltac2:(erase_compute (foo tt)).
+(* Check testevar : foo tt = true. *)
+
+Definition foo_tt_value := ltac2:(erase_forget (foo tt)).
+Check eq_refl : foo_tt_value = true. *)

plugin/plugin-bootstrap/_RocqProject

@@ -14,4 +14,5 @@ PrimString.v
 PrimArray.v
 OCamlFFI.v
 RocqMsgFFI.v
+Tactics.v
 Extraction.v

plugin/plugin-bootstrap/g_verified_extraction_malfunction.mlg

@@ -292,6 +292,8 @@ let compile_malfunction conf pt p =
 
 let extract = extract compile_malfunction
 
+let () = install_erase_conv compile_malfunction
+
 }
 
 VERNAC COMMAND EXTEND Malfunction_Verified_Extraction CLASSIFIED AS QUERY

plugin/plugin/g_verified_extraction_ocaml.mlg

@@ -79,6 +79,8 @@ let compile_malfunction conf pt p =
 
 let extract = extract compile_malfunction
 
+let () = install_erase_conv compile_malfunction
+
 }
 
 VERNAC COMMAND EXTEND Verified_Extraction CLASSIFIED AS QUERY