Unsafe inlining and beta-reduction transfomations

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

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

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.

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 ∥),
@@ -95,15 +98,18 @@ Definition final_wcbv_flags := {|
 Program Definition optional_unsafe_transforms econf :=
   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_cofix_to_fix)
+  ETransform.optional_self_transform econf.(enable_unsafe)
     ((* Rebuild the efficient lookup table *)
     rebuild_wf_env_transform (efl := efl) false false ▷
     (* Coinductives & cofixpoints are translated to inductive types and thunked fixpoints *)
     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) ▷
     rebuild_wf_env_transform (efl := efl) false false ▷
-    unbox_transformation efl final_wcbv_flags).
+    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)
@@ -258,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.
@@ -358,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.
@@ -403,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 :=
@@ -418,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

erasure/theories/EBeta.v

@@ -0,0 +1,120 @@
+From Coq Require Import List.
+From Coq Require Import String.
+From MetaCoq.Utils Require Import utils.
+From MetaCoq.Common Require Import BasicAst.
+From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils ELiftSubst EProgram.
+
+Definition map_subterms (f : term -> term) (t : term) : term :=
+  match t with
+  | tEvar n ts => tEvar n (map f ts)
+  | tLambda na body => tLambda na (f body)
+  | tLetIn na val body => tLetIn na (f val) (f body)
+  | tApp hd arg => tApp (f hd) (f arg)
+  | tCase p disc brs =>
+    tCase p (f disc) (map (on_snd f) brs)
+  | tProj p t => tProj p (f t)
+  | tFix def i => tFix (map (map_def f) def) i
+  | tCoFix def i => tCoFix (map (map_def f) def) i
+  | tPrim p => tPrim (map_prim f p)
+  | tLazy t => tLazy (f t)
+  | tForce t => tForce (f t)
+  | tConstruct ind n args => tConstruct ind n (map f args)
+  | t => t
+  end.
+
+Section betared.
+  Fixpoint decompose_lam (t : term) {struct t} : list name × term :=
+    match t with
+    | tLambda na B =>
+      let (ns, B0) := decompose_lam B in
+      (na :: ns, B0)
+    | _ => ([], t)
+    end.
+
+  Fixpoint beta_body (body : term) (args : list term) {struct args} : term :=
+    match args with
+    | [] => body
+    | a :: args =>
+        match body with
+        | tLambda na body => beta_body (body{0 := a}) args
+        | _ => mkApps body (a :: args)
+        end
+    end.
+
+  Fixpoint betared_aux (args : list term) (t : term) : term :=
+    match t with
+    | tApp hd arg => betared_aux (betared_aux [] arg :: args) hd
+    | tLambda na body =>
+      let b := betared_aux [] body in
+      beta_body (tLambda na b) args
+    | t => mkApps (map_subterms (betared_aux []) t) args
+    end.
+
+  Definition betared : term -> term := betared_aux [].
+
+  Definition betared_in_constant_body cst :=
+    {| cst_body := option_map betared (cst_body cst); |}.
+
+  Definition betared_in_decl d :=
+    match d with
+    | ConstantDecl cst => ConstantDecl (betared_in_constant_body cst)
+    | _ => d
+    end.
+
+End betared.
+
+Definition betared_env (Σ : global_declarations) : global_declarations :=
+  map (fun '(kn, decl) => (kn, betared_in_decl decl)) Σ.
+
+Definition betared_program (p : program) : program :=
+  (betared_env p.1, betared p.2).
+
+From MetaCoq.Erasure Require Import EProgram EWellformed EWcbvEval.
+From MetaCoq.Common Require Import Transform.
+
+Axiom trust_betared_wf :
+  forall efl : EEnvFlags,
+  WcbvFlags ->
+  forall (input : Transform.program _ term),
+  wf_eprogram efl input -> wf_eprogram efl (betared_program input).
+Axiom trust_betared_pres :
+  forall (efl : EEnvFlags) (wfl : WcbvFlags) (p : Transform.program _ term)
+  (v : term),
+  wf_eprogram efl p ->
+  eval_eprogram wfl p v ->
+  exists v' : term,
+  eval_eprogram wfl (betared_program p) v' /\ v' = betared v.
+
+Import Transform.
+
+Program Definition betared_transformation (efl : EEnvFlags) (wfl : WcbvFlags) :
+  Transform.t _ _ EAst.term EAst.term _ _
+    (eval_eprogram wfl) (eval_eprogram wfl) :=
+  {| name := "betared ";
+    transform p _ := betared_program p ;
+    pre p := wf_eprogram efl p ;
+    post p := wf_eprogram efl p ;
+    obseq p hp p' v v' := v' = betared v |}.
+
+Next Obligation.
+  now apply trust_betared_wf.
+Qed.
+Next Obligation.
+  now eapply trust_betared_pres.
+Qed.
+
+Import EProgram EGlobalEnv.
+
+#[global]
+Axiom betared_transformation_ext :
+  forall (efl : EEnvFlags) (wfl : WcbvFlags),
+  TransformExt.t (betared_transformation efl wfl)
+    (fun p p' => extends p.1 p'.1) (fun p p' => extends p.1 p'.1).
+
+#[global]
+Axiom betared_transformation_ext' :
+  forall (efl : EEnvFlags) (wfl : WcbvFlags),
+  TransformExt.t (betared_transformation efl wfl)
+    extends_eprogram extends_eprogram.
+
+

erasure/theories/EEnvMap.v

@@ -69,6 +69,19 @@ Module GlobalContextMap.
     rewrite (EnvMap.lookup_spec Σ.(global_decls)) //; apply Σ.
   Qed.
 
+  Definition lookup_constant Σ kn : option constant_body :=
+    decl <- lookup_env Σ kn;;
+    match decl with
+    | ConstantDecl cb => ret cb
+    | InductiveDecl _ => None
+    end.
+
+  Lemma lookup_constant_spec Σ kn : lookup_constant Σ kn = EGlobalEnv.lookup_constant Σ kn.
+  Proof.
+    rewrite /lookup_constant /EGlobalEnv.lookup_constant.
+    rewrite lookup_env_spec //.
+  Qed.
+
   Definition lookup_minductive Σ kn : option mutual_inductive_body :=
     decl <- lookup_env Σ kn;;
     match decl with