Resurrect the cofix transform, adding a new axiom for the admitted pr… (

#1056)

* Resurrect the cofix transform, adding a new axiom for the admitted proofs.
Generalize `MetaCoq Erase` to take options allowing to optionally run this pass

* Minor fixes

* Fix metacoq_tour

* Fix quoting of cofix to make translation correct

erasure-plugin/_PluginProject.in

@@ -118,6 +118,8 @@ src/eInlineProjections.mli
 src/eInlineProjections.ml
 src/eConstructorsAsBlocks.mli
 src/eConstructorsAsBlocks.ml
+src/eCoInductiveToInductive.mli
+src/eCoInductiveToInductive.ml
 src/eTransform.mli
 src/eTransform.ml
 src/erasure0.mli

erasure-plugin/src/g_metacoq_erasure.mlg

@@ -9,6 +9,23 @@ open PeanoNat.Nat
 open Datatypes
 open Vernacextend
 open Tm_util
+open Erasure0
+
+open Stdarg
+open Pcoq.Prim
+open Ltac_plugin
+open Tacexpr
+open Tacinterp
+open Stdarg
+open Tacarg
+open Genredexpr
+
+type erasure_command_args =
+  | Unsafe
+  | Time
+  | Typed
+  | BypassQeds
+  | Fast
 
 let pr_char c = str (Char.escaped c)
 
@@ -25,49 +42,97 @@ let pr_char_list l =
   (* We allow utf8 encoding *)
   str (Caml_bytestring.caml_string_of_bytestring l)
 
-let check ~bypass ~fast ?(with_types=false) env evm c =
+type erasure_config =
+  { unsafe : bool;
+    time : bool;
+    typed : bool;
+    bypass_qeds : bool;
+    fast : bool;
+    }
+
+let default_config =
+  { unsafe = false;
+    time = false;
+    typed = false;
+    bypass_qeds = false;
+    fast = false }
+
+let make_erasure_config config =
+  let open Erasure0 in
+  { enable_cofix_to_fix = config.unsafe;
+    enable_typed_erasure = config.typed;
+    enable_fast_remove_params = config.fast;
+    dearging_config = default_dearging_config;
+     }
+
+let time_opt config str fn arg =
+  if config.time then
+    time str fn arg
+  else fn arg
+
+let check config env evm c =
   debug (fun () -> str"Quoting");
-  let term = time (str"Quoting") (Ast_quoter.quote_term_rec ~bypass env evm) (EConstr.to_constr evm c) in
-  let erase = time (str"Erasure")
-      (if fast then Erasure0.erase_fast_and_print_template_program
-       else
-       if with_types then
-        Erasure0.typed_erase_and_print_template_program
-       else Erasure0.erase_and_print_template_program)
-      term
+  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 erase =
+    time (str"Erasure") (Erasure0.erase_and_print_template_program erasure_config) term
   in
-  Feedback.msg_info (pr_char_list erase)
+  Feedback.msg_notice (pr_char_list erase)
+
+let interp_erase args env evm c =
+  let open Erasure0 in
+  let config =
+    let rec aux config = function
+      | [] -> config
+      | arg :: args ->
+        match arg with
+        | Unsafe -> aux {config with unsafe = true} args
+        | 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
+
+let help_msg : string =
+  "Usage:\n\
+To erase a Gallina definition named <gid> type:\n\
+   MetaCoq Erase <options> <gid>.\n\n\
+To show this help message type:\n\
+   MetaCoq Erase -help.\n\n\
+Valid options:\n\
+-typed       :  Run the typed erasure pipeline including a dearging phase. By default we run the pipeline without this phase.\n\
+-unsafe      :  Run also partially verified passes of the pipeline. This includes the cofix to fix translation.\n\
+-time        :  Time each compilation phase\n\
+-bypass-qeds :  Bypass the use of Qed and quote opaque proofs. Beware, this can result in large memory\n\
+                consumption due to reification of large proof terms.\n\
+                By default, we use the (trusted) Template-Coq quoting optimization that quotes every opaque term as an axiom.\n\
+                All these axioms should live in Prop so that erasure is not affected by the absence of their bodies.\n\
+-fast        : Enables an alternative implementation of the parameter stripping phase that uses accumulators\n\
+               instead of a view (see Erasure.ERemoveParams).\n\
+\n\
+See https://metacoq.github.io for more detailed information."
+
 }
 
+ARGUMENT EXTEND erase_args
+| [ "-unsafe" ] -> { Unsafe }
+| [ "-time" ] -> { Time }
+| [ "-typed" ] -> { Typed }
+| [ "-bypass-qeds" ] -> { BypassQeds }
+| [ "-fast" ] -> { Fast }
+END
+
 VERNAC COMMAND EXTEND MetaCoqErase CLASSIFIED AS QUERY
-| [ "MetaCoq" "Bypass" "Erase" constr(c) ] -> {
+| [ "MetaCoq" "Erase" erase_args_list(l) constr(c) ] -> {
     let env = Global.env () in
     let evm = Evd.from_env env in
     let (c, _) = Constrintern.interp_constr env evm c in
-    check ~bypass:true ~fast:false env evm c
+    interp_erase l env evm c
   }
-| [ "MetaCoq" "Bypass" "Typed" "Erase" constr(c) ] -> {
-    let env = Global.env () in
-    let evm = Evd.from_env env in
-    let (c, _) = Constrintern.interp_constr env evm c in
-    check ~bypass:true ~fast:false ~with_types:true env evm c
-  }
-| [ "MetaCoq" "Typed" "Erase" constr(c) ] -> {
-    let env = Global.env () in
-    let evm = Evd.from_env env in
-    let (c, _) = Constrintern.interp_constr env evm c in
-    check ~bypass:false ~fast:false ~with_types:true env evm c
-  }
-| [ "MetaCoq" "Erase" constr(c) ] -> {
-    let env = Global.env () in
-    let evm = Evd.from_env env in
-    let (c, _) = Constrintern.interp_constr env evm c in
-    check ~bypass:false ~fast:false env evm c
-  }
-| [ "MetaCoq" "Fast" "Erase" constr(c) ] -> {
-    let env = Global.env () in
-    let evm = Evd.from_env env in
-    let (c, _) = Constrintern.interp_constr env evm c in
-    check ~bypass:false ~fast:true env evm c
+| [ "MetaCoq" "Erase" "-help" ] -> {
+    Feedback.msg_notice (str help_msg)
   }
 END

erasure-plugin/src/metacoq_erasure_plugin.mlpack

@@ -64,6 +64,7 @@ ErasureFunctionProperties
 EOptimizePropDiscr
 EInlineProjections
 EConstructorsAsBlocks
+ECoInductiveToInductive
 EProgram
 OptimizePropDiscr
 

erasure-plugin/theories/ETransform.v

@@ -744,7 +744,7 @@ Qed.
 Program Definition remove_params_optimization {fl : EWcbvEval.WcbvFlags} {wcon : EWcbvEval.with_constructor_as_block = false}
   (efl := all_env_flags):
   Transform.t _ _ EAst.term EAst.term _ _ (eval_eprogram_env fl) (eval_eprogram fl) :=
-  {| name := "stripping constructor parameters";
+  {| name := "stripping constructor parameters (using a view)";
     transform p pre := ERemoveParams.strip_program p;
     pre p := wf_eprogram_env efl p /\ EEtaExpanded.expanded_eprogram_env_cstrs p;
     post p := wf_eprogram (switch_no_params efl) p /\ EEtaExpanded.expanded_eprogram_cstrs p;
@@ -789,7 +789,7 @@ Qed.
 Program Definition remove_params_fast_optimization {fl : EWcbvEval.WcbvFlags} {wcon : EWcbvEval.with_constructor_as_block = false}
   (efl := all_env_flags) :
   Transform.t _ _ EAst.term EAst.term _ _ (eval_eprogram_env fl) (eval_eprogram fl) :=
-  {| name := "stripping constructor parameters (faster?)";
+  {| name := "stripping constructor parameters (using accumulators)";
     transform p _ := (ERemoveParams.Fast.strip_env p.1, ERemoveParams.Fast.strip p.1 [] p.2);
     pre p := wf_eprogram_env efl p /\ EEtaExpanded.expanded_eprogram_env_cstrs p;
     post p := wf_eprogram (switch_no_params efl) p /\ EEtaExpanded.expanded_eprogram_cstrs p;
@@ -927,7 +927,7 @@ Qed.
 From MetaCoq.Erasure Require Import EConstructorsAsBlocks.
 
 Program Definition constructors_as_blocks_transformation {efl : EEnvFlags}
-  {has_app : has_tApp} {has_rel : has_tRel} {hasbox : has_tBox} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = false} :
+  {has_app : has_tApp} {has_rel : has_tRel} {has_box : has_tBox} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = false} :
   Transform.t _ _ EAst.term EAst.term _ _ (eval_eprogram_env target_wcbv_flags) (eval_eprogram block_wcbv_flags) :=
   {| name := "transforming to constuctors as blocks";
     transform p _ := EConstructorsAsBlocks.transform_blocks_program p ;
@@ -953,8 +953,8 @@ Qed.
 
 #[global]
 Instance constructors_as_blocks_extends (efl : EEnvFlags)
-  {has_app : has_tApp} {has_rel : has_tRel} {hasbox : has_tBox} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = false} :
-  TransformExt.t (constructors_as_blocks_transformation (has_app := has_app) (has_rel := has_rel) (hasbox := hasbox) (has_pars := has_pars) (has_cstrblocks := has_cstrblocks))
+  {has_app : has_tApp} {has_rel : has_tRel} {has_box : has_tBox} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = false} :
+  TransformExt.t (constructors_as_blocks_transformation (has_app := has_app) (has_rel := has_rel) (has_box := has_box) (has_pars := has_pars) (has_cstrblocks := has_cstrblocks))
   (fun p p' => extends p.1 p'.1) (fun p p' => extends p.1 p'.1).
 Proof.
   red. intros p p' pr pr' ext. rewrite /transform /=.
@@ -963,8 +963,8 @@ Qed.
 
 #[global]
 Instance constructors_as_blocks_extends' (efl : EEnvFlags)
-  {has_app : has_tApp} {has_rel : has_tRel} {hasbox : has_tBox} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = false} :
-  TransformExt.t (constructors_as_blocks_transformation (has_app := has_app) (has_rel := has_rel) (hasbox := hasbox) (has_pars := has_pars) (has_cstrblocks := has_cstrblocks))
+  {has_app : has_tApp} {has_rel : has_tRel} {has_box : has_tBox} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = false} :
+  TransformExt.t (constructors_as_blocks_transformation (has_app := has_app) (has_rel := has_rel) (has_box := has_box) (has_pars := has_pars) (has_cstrblocks := has_cstrblocks))
   extends_eprogram_env extends_eprogram.
 Proof.
   red. intros p p' pr pr' [ext eq]. rewrite /transform /=. split.
@@ -974,3 +974,97 @@ Proof.
   eapply transform_blocks_extends; eauto. apply pr. apply pr'.
 Qed.
 
+From MetaCoq.Erasure Require ECoInductiveToInductive.
+
+Program Definition coinductive_to_inductive_transformation (efl : EEnvFlags)
+  {has_app : has_tApp} {has_box : has_tBox} {has_rel : has_tRel} {has_pars : has_cstr_params = false}
+  {has_cstrblocks : cstr_as_blocks = true} :
+  Transform.t _ _ EAst.term EAst.term _ _
+    (eval_eprogram_env block_wcbv_flags) (eval_eprogram block_wcbv_flags) :=
+  {| name := "transforming co-inductive to inductive types";
+    transform p _ := ECoInductiveToInductive.trans_program p ;
+    pre p := wf_eprogram_env efl p ;
+    post p := wf_eprogram efl p ;
+    obseq p hp p' v v' := v' = ECoInductiveToInductive.trans p.1 v |}.
+
+Next Obligation.
+  move=> efl hasapp hasbox hasrel haspars hascstrs [Σ t] [wftp wft].
+  cbn in *. eapply ECoInductiveToInductive.trans_program_wf; eauto. split => //.
+Qed.
+Next Obligation.
+  red. move=> efl hasapp hasbox hasrel haspars hascstrs [Σ t] /= v [wfe1 wfe2] [ev].
+  eexists. split; [ | eauto].
+  econstructor.
+  cbn -[transform_blocks].
+  eapply ECoInductiveToInductive.trans_correct; cbn; eauto.
+  eapply wellformed_closed_env, wfe1.
+  Unshelve. all:eauto.
+Qed.
+
+#[global]
+Instance coinductive_to_inductive_transformation_ext (efl : EEnvFlags)
+  {has_app : has_tApp} {has_rel : has_tRel} {has_box : has_tBox} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = true} :
+  TransformExt.t (coinductive_to_inductive_transformation efl (has_app := has_app) (has_rel := has_rel)
+    (has_box := has_box) (has_pars := has_pars) (has_cstrblocks := has_cstrblocks))
+    (fun p p' => extends p.1 p'.1) (fun p p' => extends p.1 p'.1).
+Proof.
+  red. intros p p' pr pr' ext. rewrite /transform /=.
+  eapply ECoInductiveToInductive.trust_cofix.
+Qed.
+
+#[global]
+Instance coinductive_to_inductive_transformation_ext' (efl : EEnvFlags)
+  {has_app : has_tApp} {has_rel : has_tRel} {has_box : has_tBox} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = true} :
+  TransformExt.t (coinductive_to_inductive_transformation efl (has_app := has_app) (has_rel := has_rel)
+    (has_box := has_box) (has_pars := has_pars) (has_cstrblocks := has_cstrblocks))
+    extends_eprogram_env extends_eprogram.
+Proof.
+  red. intros p p' pr pr' ext. rewrite /transform /=.
+  eapply ECoInductiveToInductive.trust_cofix.
+Qed.
+
+Program Definition optional_transform {env env' term term' value value' eval eval'} (activate : bool)
+  (tr : Transform.t env env' term term' value value' eval eval') :
+  if activate then Transform.t env env' term term' value value' eval eval'
+  else Transform.t env env term term value value eval eval :=
+  if activate return if activate then Transform.t env env' term term' value value' eval eval'
+  else Transform.t env env term term value value eval eval
+  then tr
+  else
+  {| name := ("skipped " ^ tr.(name));
+     transform p pr := p;
+     pre := tr.(pre) ;
+     post := tr.(pre) ;
+     obseq p hp p' v v' := v' = v |}.
+Next Obligation.
+  intros. cbn. exact p.
+Defined.
+Next Obligation.
+ cbn. intros. red. intros. exists v. split => //.
+Defined.
+
+Program Definition optional_self_transform {env term eval} (activate : bool)
+  (tr : Transform.self_transform env term eval eval) :
+  Transform.self_transform env term eval eval :=
+  if activate return Transform.self_transform env term eval eval
+  then tr
+  else
+  {| name := ("skipped " ^ tr.(name));
+     transform p pr := p;
+     pre := tr.(pre) ;
+     post := tr.(pre) ;
+     obseq p hp p' v v' := v' = v |}.
+Next Obligation.
+  intros. cbn. exact p.
+Defined.
+Next Obligation.
+ cbn. intros. red. intros. exists v. split => //.
+Defined.
+
+#[global]
+Instance optional_self_transformation_ext {env term eval} activate tr extends :
+  TransformExt.t tr extends extends ->
+  TransformExt.t (@optional_self_transform env term eval activate tr) extends extends.
+Proof.
+  red; intros. destruct activate; cbn in * => //. now apply H.
+Qed.