Fixes due to removal of useless -fast flag and change for reordering …

…of constructors, now verified

erasure-plugin/src/g_metacoq_erasure.mlg

@@ -25,7 +25,6 @@ type erasure_command_args =
   | Time
   | Typed
   | BypassQeds
-  | Fast
 
 let pr_char c = str (Char.escaped c)
 
@@ -46,24 +45,19 @@ type erasure_config =
   { unsafe : bool;
     time : bool;
     typed : bool;
-    bypass_qeds : bool;
-    fast : bool;
-    }
+    bypass_qeds : bool }
 
 let default_config =
   { unsafe = false;
     time = false;
     typed = false;
-    bypass_qeds = false;
-    fast = false }
+    bypass_qeds = false }
 
 let make_erasure_config config =
   let open Erasure0 in
   { enable_unsafe = if config.unsafe then all_unsafe_passes else no_unsafe_passes ;
     enable_typed_erasure = config.typed;
-    enable_fast_remove_params = config.fast;
     dearging_config = default_dearging_config;
-    inductives_mapping = [];
     inlined_constants = Kernames.KernameSet.empty }
 
 let time_opt config str fn arg =
@@ -76,8 +70,9 @@ let check config env evm c =
   let time str f arg = time_opt config str f arg in
   let term = time (str"Quoting") (Ast_quoter.quote_term_rec ~bypass:config.bypass_qeds env evm) (EConstr.to_constr evm c) in
   let erasure_config = make_erasure_config config in
+  let mapping = [] in
   let erase =
-    time (str"Erasure") (Erasure0.erase_and_print_template_program erasure_config) term
+    time (str"Erasure") (Erasure0.erase_and_print_template_program erasure_config mapping) term
   in
   Feedback.msg_notice (pr_char_list erase)
 
@@ -92,7 +87,6 @@ let interp_erase args env evm c =
         | Time -> aux {config with time = true} args
         | Typed -> aux {config with typed = true} args
         | BypassQeds -> aux {config with bypass_qeds = true} args
-        | Fast -> aux {config with fast = true} args
     in aux default_config args
   in
   check config env evm c
@@ -123,7 +117,6 @@ ARGUMENT EXTEND erase_args
 | [ "-time" ] -> { Time }
 | [ "-typed" ] -> { Typed }
 | [ "-bypass-qeds" ] -> { BypassQeds }
-| [ "-fast" ] -> { Fast }
 END
 
 VERNAC COMMAND EXTEND MetaCoqErase CLASSIFIED AS QUERY

test-suite/erasure_live_test.v

@@ -18,14 +18,11 @@ Unset MetaCoq Debug.
 #[local] Existing Instance config.extraction_checker_flags.
 
 Definition test (p : Ast.Env.program) : string :=
-  erase_and_print_template_program default_erasure_config p.
+  erase_and_print_template_program default_erasure_config [] p.
 
 Definition testty (p : Ast.Env.program) : string :=
   typed_erase_and_print_template_program p.
 
-Definition test_fast (p : Ast.Env.program) : string :=
-  erase_fast_and_print_template_program p.
-
 MetaCoq Quote Recursively Definition zero := 0.
 
 Definition zerocst := Eval lazy in test zero.
@@ -53,12 +50,7 @@ Definition singlelim := ((fun (X : Set) (x : X) (e : x = x) =>
 
 Definition erase {A} (a : A) : TemplateMonad unit :=
   aq <- tmQuoteRec a ;;
-  s <- tmEval lazy (erase_and_print_template_program default_erasure_config aq) ;;
-  tmMsg s.
-
-Definition erase_fast {A} (a : A) : TemplateMonad unit :=
-  aq <- tmQuoteRec a ;;
-  s <- tmEval lazy (erase_fast_and_print_template_program aq) ;;
+  s <- tmEval lazy (erase_and_print_template_program default_erasure_config [] aq) ;;
   tmMsg s.
 
 MetaCoq Run (erase 0).
@@ -80,7 +72,6 @@ Definition vplus0123 := (vplus v01 v23).
 Set MetaCoq Timing.
 
 Time MetaCoq Run (tmEval hnf vplus0123 >>= erase).
-Time MetaCoq Run (tmEval hnf vplus0123 >>= erase_fast).
 
 (** Cofix *)
 From Coq Require Import StreamMemo.
@@ -352,7 +343,7 @@ MetaCoq Quote Recursively Definition cbv_provedCopyx :=
 Definition ans_provedCopyx :=
   Eval lazy in (test cbv_provedCopyx).
 MetaCoq Quote Recursively Definition p_provedCopyx := provedCopyx. (* program *)
-Time Definition P_provedCopyx := Eval lazy in (test_fast cbv_provedCopyx).
+Time Definition P_provedCopyx := Eval lazy in (test cbv_provedCopyx).
 (* We don't run this one every time as it is really expensive *)
 (*Time Definition P_provedCopyxvm := Eval vm_compute in (test p_provedCopyx).*)