Merge pull request #1061 from MetaCoq/unsafe-inline-beta

Unsafe inline beta and unboxing transforms

Author: mattam82

erasure-plugin/_PluginProject.in

@@ -112,6 +112,10 @@ 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
@@ -122,6 +126,8 @@ 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

@@ -59,11 +59,12 @@ let default_config =
 
 let make_erasure_config config =
   let open Erasure0 in
-  { enable_cofix_to_fix = config.unsafe;
+  { enable_unsafe = config.unsafe;
     enable_typed_erasure = config.typed;
     enable_fast_remove_params = config.fast;
     dearging_config = default_dearging_config;
-    inductives_mapping = [] }
+    inductives_mapping = [];
+    inlining = Kernames.KernameSet.empty }
 
 let time_opt config str fn arg =
   if config.time then

erasure-plugin/src/metacoq_erasure_plugin.mlpack

@@ -58,6 +58,8 @@ ESpineView
 EPretty
 Extract
 EEtaExpanded
+EInlining
+EBeta
 ERemoveParams
 ErasureFunction
 ErasureFunctionProperties
@@ -66,6 +68,7 @@ EInlineProjections
 EConstructorsAsBlocks
 ECoInductiveToInductive
 EReorderCstrs
+EUnboxing
 EProgram
 OptimizePropDiscr
 

erasure-plugin/theories/ETransform.v

@@ -23,7 +23,6 @@ Definition build_wf_env_from_env {cf : checker_flags} (Σ : global_env_map) (wf
      wf_env_map_repr := Σ.(trans_env_repr);
  |}.
 
-
 Notation NormalizationIn_erase_pcuic_program_1 p
   := (@PCUICTyping.wf_ext config.extraction_checker_flags p -> PCUICSN.NormalizationIn (cf:=config.extraction_checker_flags) (no:=PCUICSN.extraction_normalizing) p)
        (only parsing).
@@ -601,11 +600,6 @@ Section Dearging.
 
 End Dearging.
 
-Definition extends_eprogram (p p' : eprogram) :=
-  extends p.1 p'.1 /\ p.2 = p'.2.
-
-Definition extends_eprogram_env (p p' : eprogram_env) :=
-  extends p.1 p'.1 /\ p.2 = p'.2.
 
 Section PCUICEnv. (* Locally reuse the short names for PCUIC environment handling *)
 Import PCUICAst.PCUICEnvironment.
@@ -1063,6 +1057,47 @@ Axiom trust_reorder_cstrs_transformation_ext' : forall (efl : EEnvFlags) (wfl :
   TransformExt.t (reorder_cstrs_transformation efl wfl m)
     extends_eprogram extends_eprogram.
 
+From MetaCoq.Erasure Require Import EUnboxing.
+
+Axiom trust_unboxing_wf :
+  forall efl : EEnvFlags,
+  WcbvFlags ->
+  forall (input : Transform.program _ term),
+  wf_eprogram_env efl input -> wf_eprogram efl (unbox_program input).
+Axiom trust_unboxing_pres :
+  forall (efl : EEnvFlags) (wfl : WcbvFlags) (p : Transform.program _ term)
+  (v : term),
+  wf_eprogram_env efl p ->
+  eval_eprogram_env wfl p v -> exists v' : term, eval_eprogram wfl (unbox_program p) v' /\ v' = unbox p.1 v.
+
+Program Definition unbox_transformation (efl : EEnvFlags) (wfl : WcbvFlags)  :
+  Transform.t _ _ EAst.term EAst.term _ _
+    (eval_eprogram_env wfl) (eval_eprogram wfl) :=
+  {| name := "unbox singleton constructors ";
+    transform p _ := EUnboxing.unbox_program p ;
+    pre p := wf_eprogram_env efl p ;
+    post p := wf_eprogram efl p ;
+    obseq p hp p' v v' := v' = unbox p.1 v |}.
+
+Next Obligation.
+  move=> efl wfl m. cbn. now apply trust_unboxing_wf.
+Qed.
+Next Obligation.
+  red. eapply trust_unboxing_pres.
+Qed.
+
+#[global]
+Axiom trust_unbox_transformation_ext :
+  forall (efl : EEnvFlags) (wfl : WcbvFlags),
+  TransformExt.t (unbox_transformation efl wfl)
+    (fun p p' => extends p.1 p'.1) (fun p p' => extends p.1 p'.1).
+
+#[global]
+Axiom trust_unbox_transformation_ext' :
+  forall (efl : EEnvFlags) (wfl : WcbvFlags),
+  TransformExt.t (unbox_transformation efl wfl)
+    extends_eprogram_env extends_eprogram.
+
 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'

erasure-plugin/theories/Erasure.v

@@ -6,7 +6,7 @@ From MetaCoq.Template Require Import EtaExpand TemplateProgram.
 From MetaCoq.PCUIC Require PCUICAst PCUICAstUtils PCUICProgram.
 From MetaCoq.SafeChecker Require Import PCUICErrors PCUICWfEnvImpl.
 From MetaCoq.Erasure Require EAstUtils ErasureFunction ErasureCorrectness EPretty Extract.
-From MetaCoq.Erasure Require Import EProgram.
+From MetaCoq.Erasure Require Import EProgram EInlining EBeta.
 From MetaCoq.ErasurePlugin Require Import ETransform.
 
 Import PCUICProgram.
@@ -31,11 +31,12 @@ Import EWcbvEval.
 Local Obligation Tactic := program_simpl.
 
 Record erasure_configuration := {
-  enable_cofix_to_fix : bool;
+  enable_unsafe : bool;
   enable_typed_erasure : bool;
   enable_fast_remove_params : bool;
   dearging_config : dearging_config;
-  inductives_mapping : EReorderCstrs.inductives_mapping
+  inductives_mapping : EReorderCstrs.inductives_mapping;
+  inlining : KernameSet.t
   }.
 
 Definition default_dearging_config :=
@@ -45,19 +46,21 @@ Definition default_dearging_config :=
 
 (* This runs the cofix -> fix translation which is not entirely verified yet *)
 Definition default_erasure_config :=
-  {| enable_cofix_to_fix := true;
+  {| enable_unsafe := true;
      dearging_config := default_dearging_config;
      enable_typed_erasure := true;
      enable_fast_remove_params := true;
-     inductives_mapping := [] |}.
+     inductives_mapping := [];
+     inlining := KernameSet.empty |}.
 
 (* This runs only the verified phases without the typed erasure and "fast" remove params *)
 Definition safe_erasure_config :=
-  {| enable_cofix_to_fix := false;
+  {| enable_unsafe := false;
      enable_typed_erasure := false;
      enable_fast_remove_params := false;
      dearging_config := default_dearging_config;
-     inductives_mapping := [] |}.
+     inductives_mapping := [];
+     inlining := KernameSet.empty |}.
 
 Axiom assume_welltyped_template_program_expansion :
   forall p (wtp : ∥ wt_template_program_env p ∥),
@@ -93,16 +96,20 @@ Definition final_wcbv_flags := {|
   with_constructor_as_block := true |}.
 
 Program Definition optional_unsafe_transforms econf :=
-  ETransform.optional_self_transform econf.(enable_cofix_to_fix)
+  let efl := EConstructorsAsBlocks.switch_cstr_as_blocks
+  (EInlineProjections.disable_projections_env_flag (ERemoveParams.switch_no_params EWellformed.all_env_flags)) in
+  ETransform.optional_self_transform econf.(enable_unsafe)
     ((* Rebuild the efficient lookup table *)
-    rebuild_wf_env_transform (efl := EConstructorsAsBlocks.switch_cstr_as_blocks
-      (EInlineProjections.disable_projections_env_flag (ERemoveParams.switch_no_params EWellformed.all_env_flags))) false false ▷
+    rebuild_wf_env_transform (efl := efl) false false ▷
     (* Coinductives & cofixpoints are translated to inductive types and thunked fixpoints *)
-    let efl := EConstructorsAsBlocks.switch_cstr_as_blocks
-      (EInlineProjections.disable_projections_env_flag (ERemoveParams.switch_no_params EWellformed.all_env_flags)) in
     coinductive_to_inductive_transformation efl
       (has_app := eq_refl) (has_box := eq_refl) (has_rel := eq_refl) (has_pars := eq_refl) (has_cstrblocks := eq_refl) ▷
-    reorder_cstrs_transformation efl final_wcbv_flags econf.(inductives_mapping)).
+    reorder_cstrs_transformation efl final_wcbv_flags econf.(inductives_mapping) ▷
+    rebuild_wf_env_transform (efl := efl) false false ▷
+    unbox_transformation efl final_wcbv_flags ▷
+    inline_transformation efl final_wcbv_flags econf.(inlining) ▷
+    forget_inlining_info_transformation efl final_wcbv_flags ▷
+    betared_transformation efl final_wcbv_flags).
 
 Program Definition verified_lambdabox_pipeline {guard : abstract_guard_impl}
   (efl := EWellformed.all_env_flags)
@@ -257,8 +264,7 @@ Qed.
 
 Next Obligation.
   unfold optional_unsafe_transforms. cbn.
-  unfold optional_self_transform. cbn.
-  destruct enable_cofix_to_fix => //.
+  destruct enable_unsafe => //.
 Qed.
 
 Local Obligation Tactic := intros; eauto.
@@ -357,7 +363,7 @@ Next Obligation.
   cbn in H. split; cbn; intuition eauto.
 Qed.
 Next Obligation.
-  cbn in H. unfold optional_unsafe_transforms. destruct enable_cofix_to_fix => //.
+  cbn in H. unfold optional_unsafe_transforms. destruct enable_unsafe => //.
 Qed.
 Next Obligation.
   cbn in H. split; cbn; intuition eauto.
@@ -402,7 +408,7 @@ Program Definition run_erase_program {guard : abstract_guard_impl} econf :=
 Next Obligation.
 Proof.
   unfold optional_unsafe_transforms.
-  destruct enable_cofix_to_fix => //.
+  destruct enable_unsafe => //.
 Qed.
 
 Program Definition erase_and_print_template_program econf (p : Ast.Env.program) : string :=
@@ -417,21 +423,23 @@ Next Obligation.
 Qed.
 
 Definition erasure_fast_config :=
-  {| enable_cofix_to_fix := false;
+  {| enable_unsafe := false;
      dearging_config := default_dearging_config;
      enable_typed_erasure := false;
      enable_fast_remove_params := true;
-     inductives_mapping := [] |}.
+     inductives_mapping := [];
+     inlining := KernameSet.empty |}.
 
 Program Definition erase_fast_and_print_template_program (p : Ast.Env.program) : string :=
   erase_and_print_template_program erasure_fast_config p.
 
 Definition typed_erasure_config :=
-  {| enable_cofix_to_fix := false;
+  {| enable_unsafe := false;
       dearging_config := default_dearging_config;
       enable_typed_erasure := true;
       enable_fast_remove_params := true;
-      inductives_mapping := [] |}.
+      inductives_mapping := [];
+      inlining := KernameSet.empty |}.
 
 (* Parameterized by a configuration for dearging, allowing to, e.g., override masks. *)
 Program Definition typed_erase_and_print_template_program (p : Ast.Env.program)

erasure-plugin/theories/ErasureCorrectness.v

@@ -5,10 +5,10 @@ From MetaCoq.Utils Require Import bytestring utils.
 From MetaCoq.PCUIC Require PCUICAst PCUICAstUtils PCUICProgram.
 From MetaCoq.PCUIC Require Import PCUICNormal.
 From MetaCoq.SafeChecker Require Import PCUICErrors PCUICWfEnvImpl.
-From MetaCoq.Erasure Require EAstUtils ErasureCorrectness EPretty Extract EConstructorsAsBlocks.
+From MetaCoq.Erasure Require EAstUtils ErasureCorrectness EPretty Extract EProgram EConstructorsAsBlocks.
 From MetaCoq.Erasure Require Import EWcbvEvalNamed ErasureFunction ErasureFunctionProperties.
 From MetaCoq.ErasurePlugin Require Import ETransform Erasure.
-Import PCUICProgram.
+Import EProgram PCUICProgram.
 Import PCUICTransform (template_to_pcuic_transform, pcuic_expand_lets_transform).
 
 (* This is the total erasure function +
@@ -1742,7 +1742,7 @@ Section PCUICErase.
       match goal with
       [ |- context [ @erase ?X_type ?X ?nin ?G (tApp _ _) ?wt ] ] =>
         unshelve epose proof (@erase_mkApps X_type X nin G t [u] wt (wt'_erase_pcuic_program (Σ, t) prf3 prf0))
-      end. 
+      end.
       assert (hargs : forall Σ : global_env_ext, Σ ∼_ext env -> ∥ All (welltyped Σ []) [u] ∥).
       { cbn; intros ? ->. do 2 constructor; auto. destruct prf4 as [[T HT]]. eexists; eapply HT. }
       specialize (H hargs).
@@ -2120,7 +2120,7 @@ Section pipeline_cond.
 
   Opaque compose.
 
-  Lemma verified_erasure_pipeline_lookup_env_in kn decl (efl := EInlineProjections.switch_no_params all_env_flags)  
+  Lemma verified_erasure_pipeline_lookup_env_in kn decl (efl := EInlineProjections.switch_no_params all_env_flags)
     {has_rel : has_tRel} {has_box : has_tBox} :
     EGlobalEnv.lookup_env Σ_t kn = Some decl ->
    exists decl',
@@ -2216,7 +2216,7 @@ Section pipeline_theorem.
   Let Σ_v := (transform verified_erasure_pipeline (Σ, v) (precond2 _ _ _ _ expΣ expt typing _ _ Heval)).1.
   Let v_t := compile_value_box (PCUICExpandLets.trans_global_env Σ) v [].
 
-  Lemma verified_erasure_pipeline_extends (efl := EInlineProjections.switch_no_params all_env_flags) 
+  Lemma verified_erasure_pipeline_extends (efl := EInlineProjections.switch_no_params all_env_flags)
    {has_rel : has_tRel} {has_box : has_tBox} :
    EGlobalEnv.extends Σ_v Σ_t.
   Proof.

erasure/_CoqProject.in

@@ -30,6 +30,8 @@ theories/ErasureFunction.v
 theories/ErasureFunctionProperties.v
 theories/EExtends.v
 theories/EOptimizePropDiscr.v
+theories/EInlining.v
+theories/EBeta.v
 theories/EEtaExpandedFix.v
 theories/EEtaExpanded.v
 theories/EProgram.v
@@ -39,6 +41,7 @@ theories/EConstructorsAsBlocks.v
 theories/EWcbvEvalCstrsAsBlocksInd.v
 theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
 theories/ECoInductiveToInductive.v
+theories/EUnboxing.v
 theories/EReorderCstrs.v
 theories/EImplementBox.v