Merge pull request #1085 from MetaCoq/fixes-for-funelim

Fixes for funelim

Makefile

@@ -12,7 +12,7 @@ ifeq '$(METACOQ_CONFIG)' 'local'
   export OCAMLPATH
 endif
 
-.PHONY: printconf all utils template-coq pcuic erasure safechecker-plugin install uninstall html clean mrproper .merlin test-suite translations quotation
+.PHONY: printconf all utils template-coq pcuic erasure install uninstall html clean mrproper safechecker-plugin .merlin test-suite translations quotation
 
 printconf:
 ifeq '$(METACOQ_CONFIG)' 'local'

common/theories/BasicAst.v

@@ -301,7 +301,7 @@ Proof.
 Qed.
 
 Lemma map_context_length {term term'} (f : term -> term') l : #|map_context f l| = #|l|.
-Proof. now unfold map_context; rewrite map_length. Qed.
+Proof. now unfold map_context; rewrite length_map. Qed.
 #[global] Hint Rewrite @map_context_length : len.
 
 Definition test_decl {term} (f : term -> bool) (d : context_decl term) : bool :=
@@ -343,7 +343,7 @@ Proof using Type.
 Qed.
 
 Lemma app_context_length {T} (Γ Γ' : list T) : #|Γ ,,, Γ'| = #|Γ'| + #|Γ|.
-Proof. unfold app_context. now rewrite app_length. Qed.
+Proof. unfold app_context. now rewrite length_app. Qed.
 #[global] Hint Rewrite @app_context_length : len.
 
 Lemma nth_error_app_context_ge {T} v Γ Γ' :
@@ -481,7 +481,7 @@ Section Contexts.
     mapi (fun k' d => map_decl (f (Nat.pred (length Γ) - k')) d) Γ.
   Proof using Type.
     unfold fold_context_k. rewrite rev_mapi. rewrite List.rev_involutive.
-    apply mapi_ext. intros. f_equal. now rewrite List.rev_length.
+    apply mapi_ext. intros. f_equal. now rewrite List.length_rev.
   Qed.
 
   Lemma mapi_context_fold f Γ :
@@ -503,17 +503,17 @@ Section Contexts.
 
   Lemma fold_context_k_length f Γ : length (fold_context_k f Γ) = length Γ.
   Proof using Type.
-    unfold fold_context_k. now rewrite !List.rev_length mapi_length List.rev_length.
+    unfold fold_context_k. now rewrite !List.length_rev mapi_length List.length_rev.
   Qed.
 
   Lemma fold_context_k_snoc0 f Γ d :
     fold_context_k f (d :: Γ) = fold_context_k f Γ ,, map_decl (f (length Γ)) d.
   Proof using Type.
     unfold fold_context_k.
     rewrite !rev_mapi !rev_involutive. unfold mapi; rewrite mapi_rec_eqn.
-    unfold snoc. f_equal. now rewrite Nat.sub_0_r List.rev_length.
+    unfold snoc. f_equal. now rewrite Nat.sub_0_r List.length_rev.
     rewrite mapi_rec_Sk. simpl. apply mapi_rec_ext. intros.
-    rewrite app_length !List.rev_length. simpl. f_equal. f_equal. lia.
+    rewrite length_app !List.length_rev. simpl. f_equal. f_equal. lia.
   Qed.
 
   Lemma fold_context_k_app f Γ Δ :
@@ -523,7 +523,7 @@ Section Contexts.
     unfold fold_context_k.
     rewrite List.rev_app_distr.
     rewrite mapi_app. rewrite <- List.rev_app_distr. f_equal. f_equal.
-    apply mapi_ext. intros. f_equal. rewrite List.rev_length. f_equal.
+    apply mapi_ext. intros. f_equal. rewrite List.length_rev. f_equal.
   Qed.
 
   Local Set Keyed Unification.
@@ -714,7 +714,7 @@ Section Contexts.
   Lemma forget_types_length (ctx : list (context_decl term)) :
     #|forget_types ctx| = #|ctx|.
   Proof using Type.
-    now rewrite /forget_types map_length.
+    now rewrite /forget_types length_map.
   Qed.
 
   Lemma map_decl_name_fold_context_k (f : nat -> term' -> term) ctx :

common/theories/Environment.v

@@ -185,7 +185,7 @@ Module Environment (T : Term).
     mapi (fun k' d => subst_decl s (Nat.pred #|Γ| - k' + k) d) Γ.
   Proof.
     unfold subst_context, fold_context_k. rewrite rev_mapi. rewrite List.rev_involutive.
-    apply mapi_ext. intros. f_equal. now rewrite List.rev_length.
+    apply mapi_ext. intros. f_equal. now rewrite List.length_rev.
   Qed.
 
   Lemma subst_context_snoc s k Γ d : subst_context s k (d :: Γ) = subst_context s k Γ ,, subst_decl s (#|Γ| + k) d.
@@ -204,7 +204,7 @@ Module Environment (T : Term).
 
   Lemma subst_instance_length u (ctx : context)
     : #|subst_instance u ctx| = #|ctx|.
-  Proof. unfold subst_instance, subst_instance_context, map_context. now rewrite map_length. Qed.
+  Proof. unfold subst_instance, subst_instance_context, map_context. now rewrite length_map. Qed.
   #[global] Hint Rewrite subst_instance_length : len.
 
   Definition set_binder_name (na : aname) (x : context_decl) : context_decl :=
@@ -245,7 +245,7 @@ Module Environment (T : Term).
   Proof.
     induction Γ' as [|[na [body|] ty] tl] in Γ |- *; cbn; eauto.
     - now rewrite IHtl subst_context_length.
-    - rewrite IHtl app_length. simpl. lia.
+    - rewrite IHtl length_app. simpl. lia.
   Qed.
   #[global] Hint Rewrite smash_context_length : len.
 
@@ -1001,7 +1001,7 @@ Module Environment (T : Term).
                             (ind.(ind_relevance))) ind.(ind_type)) l.
 
   Lemma arities_context_length l : #|arities_context l| = #|l|.
-  Proof. unfold arities_context. now rewrite rev_map_length. Qed.
+  Proof. unfold arities_context. now rewrite length_rev_map. Qed.
   #[global] Hint Rewrite arities_context_length : len.
 
   Definition map_mutual_inductive_body f m :=

common/theories/EnvironmentReflect.v

@@ -33,7 +33,7 @@ Module EnvironmentReflect (T : Term) (Import E : EnvironmentSig T) (Import TDec
     { intro H'; apply H; clear H; intros [c ?]; specialize (H' c).
       destruct H' as [decls H'].
       cbn [fst].
-      rewrite H' app_length Nat.add_sub skipn_all_app //. }
+      rewrite H' length_app Nat.add_sub skipn_all_app //. }
   Qed.
 
   Lemma strictly_extends_decls_partT (Σ Σ' : global_env)
@@ -43,7 +43,7 @@ Module EnvironmentReflect (T : Term) (Import E : EnvironmentSig T) (Import TDec
     { rewrite -H.
       eexists; symmetry; apply firstn_skipn. }
     { move => [Σ'' H'].
-      move: H. rewrite H' app_length Nat.add_sub skipn_all_app //. }
+      move: H. rewrite H' length_app Nat.add_sub skipn_all_app //. }
   Qed.
 
   Definition extendsb (Σ Σ' : global_env) : bool

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.

erasure-plugin/_PluginProject.in

@@ -112,12 +112,22 @@ src/eOptimizePropDiscr.mli
 src/eOptimizePropDiscr.ml
 src/optimizePropDiscr.mli
 src/optimizePropDiscr.ml
+src/eInlining.mli
+src/eInlining.ml
+src/eBeta.mli
+src/eBeta.ml
 src/eProgram.mli
 src/eProgram.ml
 src/eInlineProjections.mli
 src/eInlineProjections.ml
 src/eConstructorsAsBlocks.mli
 src/eConstructorsAsBlocks.ml
+src/eCoInductiveToInductive.mli
+src/eCoInductiveToInductive.ml
+src/eReorderCstrs.mli
+src/eReorderCstrs.ml
+src/eUnboxing.mli
+src/eUnboxing.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,98 @@ 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_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 =
+  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 lazy 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

@@ -58,12 +58,17 @@ ESpineView
 EPretty
 Extract
 EEtaExpanded
+EInlining
+EBeta
 ERemoveParams
 ErasureFunction
 ErasureFunctionProperties
 EOptimizePropDiscr
 EInlineProjections
 EConstructorsAsBlocks
+ECoInductiveToInductive
+EReorderCstrs
+EUnboxing
 EProgram
 OptimizePropDiscr