Merge pull request #1059 from MetaCoq/reorder-constructors

mattam82 · web-flow · commit f9c62c5e4253 · 2024-02-21T19:19:04.000+01:00
Reorder constructors
diff --git a/erasure-plugin/_PluginProject.in b/erasure-plugin/_PluginProject.in
@@ -120,6 +120,8 @@ src/eConstructorsAsBlocks.mli
 src/eConstructorsAsBlocks.ml
 src/eCoInductiveToInductive.mli
 src/eCoInductiveToInductive.ml
+src/eReorderCstrs.mli
+src/eReorderCstrs.ml
 src/eTransform.mli
 src/eTransform.ml
 src/erasure0.mli
diff --git a/erasure-plugin/src/g_metacoq_erasure.mlg b/erasure-plugin/src/g_metacoq_erasure.mlg
@@ -63,7 +63,7 @@ let make_erasure_config config =
     enable_typed_erasure = config.typed;
     enable_fast_remove_params = config.fast;
     dearging_config = default_dearging_config;
-     }
+    inductives_mapping = [] }
 
 let time_opt config str fn arg =
   if config.time then
diff --git a/erasure-plugin/src/metacoq_erasure_plugin.mlpack b/erasure-plugin/src/metacoq_erasure_plugin.mlpack
@@ -65,6 +65,7 @@ EOptimizePropDiscr
 EInlineProjections
 EConstructorsAsBlocks
 ECoInductiveToInductive
+EReorderCstrs
 EProgram
 OptimizePropDiscr
 
diff --git a/erasure-plugin/theories/ETransform.v b/erasure-plugin/theories/ETransform.v
@@ -8,7 +8,8 @@ Set Warnings "-notation-overridden".
 From MetaCoq.PCUIC Require PCUICAst PCUICAstUtils PCUICProgram PCUICWeakeningEnvSN.
 Set Warnings "+notation-overridden".
 From MetaCoq.SafeChecker Require Import PCUICErrors PCUICWfEnv PCUICWfEnvImpl.
-From MetaCoq.Erasure Require EAstUtils ErasureCorrectness Extract EOptimizePropDiscr ERemoveParams EProgram.
+From MetaCoq.Erasure Require EAstUtils ErasureCorrectness Extract EOptimizePropDiscr
+  ERemoveParams EProgram.
 From MetaCoq.Erasure Require Import ErasureFunction ErasureFunctionProperties.
 From MetaCoq.TemplatePCUIC Require Import PCUICTransform.
 
@@ -1023,6 +1024,45 @@ Proof.
   eapply ECoInductiveToInductive.trust_cofix.
 Qed.
 
+From MetaCoq.Erasure Require Import EReorderCstrs.
+
+Axiom trust_reorder_cstrs_wf :
+  forall efl : EEnvFlags,
+  WcbvFlags ->
+  forall (m : inductives_mapping) (input : Transform.program E.global_context term),
+  wf_eprogram efl input -> wf_eprogram efl (reorder_program m input).
+Axiom trust_reorder_cstrs_pres :
+  forall (efl : EEnvFlags) (wfl : WcbvFlags) (m : inductives_mapping) (p : Transform.program E.global_context term)
+  (v : term),
+  wf_eprogram efl p ->
+  eval_eprogram wfl p v -> exists v' : term, eval_eprogram wfl (reorder_program m p) v' /\ v' = reorder m v.
+
+Program Definition reorder_cstrs_transformation (efl : EEnvFlags) (wfl : WcbvFlags) (m : inductives_mapping) :
+  Transform.t _ _ EAst.term EAst.term _ _
+    (eval_eprogram wfl) (eval_eprogram wfl) :=
+  {| name := "reoder inductive constructors ";
+    transform p _ := EReorderCstrs.reorder_program m p ;
+    pre p := wf_eprogram efl p ;
+    post p := wf_eprogram efl p ;
+    obseq p hp p' v v' := v' = EReorderCstrs.reorder m v |}.
+
+Next Obligation.
+  move=> efl wfl m. cbn. now apply trust_reorder_cstrs_wf.
+Qed.
+Next Obligation.
+  red. eapply trust_reorder_cstrs_pres.
+Qed.
+
+#[global]
+Axiom trust_reorder_cstrs_transformation_ext : forall (efl : EEnvFlags) (wfl : WcbvFlags) (m : inductives_mapping),
+  TransformExt.t (reorder_cstrs_transformation efl wfl m)
+    (fun p p' => extends p.1 p'.1) (fun p p' => extends p.1 p'.1).
+
+#[global]
+Axiom trust_reorder_cstrs_transformation_ext' : forall (efl : EEnvFlags) (wfl : WcbvFlags) (m : inductives_mapping),
+  TransformExt.t (reorder_cstrs_transformation efl wfl m)
+    extends_eprogram 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'
diff --git a/erasure-plugin/theories/Erasure.v b/erasure-plugin/theories/Erasure.v
@@ -34,7 +34,8 @@ Record erasure_configuration := {
   enable_cofix_to_fix : bool;
   enable_typed_erasure : bool;
   enable_fast_remove_params : bool;
-  dearging_config : dearging_config
+  dearging_config : dearging_config;
+  inductives_mapping : EReorderCstrs.inductives_mapping
   }.
 
 Definition default_dearging_config :=
@@ -47,14 +48,16 @@ Definition default_erasure_config :=
   {| enable_cofix_to_fix := true;
      dearging_config := default_dearging_config;
      enable_typed_erasure := true;
-     enable_fast_remove_params := true |}.
+     enable_fast_remove_params := true;
+     inductives_mapping := [] |}.
 
 (* This runs only the verified phases without the typed erasure and "fast" remove params *)
 Definition safe_erasure_config :=
   {| enable_cofix_to_fix := false;
      enable_typed_erasure := false;
      enable_fast_remove_params := false;
-     dearging_config := default_dearging_config |}.
+     dearging_config := default_dearging_config;
+     inductives_mapping := [] |}.
 
 Axiom assume_welltyped_template_program_expansion :
   forall p (wtp : ∥ wt_template_program_env p ∥),
@@ -89,7 +92,7 @@ Definition final_wcbv_flags := {|
   with_guarded_fix := false;
   with_constructor_as_block := true |}.
 
-Program Definition optional_cofix_to_fix_transform econf :=
+Program Definition optional_unsafe_transforms econf :=
   ETransform.optional_self_transform econf.(enable_cofix_to_fix)
     ((* Rebuild the efficient lookup table *)
     rebuild_wf_env_transform (efl := EConstructorsAsBlocks.switch_cstr_as_blocks
@@ -98,8 +101,8 @@ Program Definition optional_cofix_to_fix_transform econf :=
     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))
-    .
+      (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)).
 
 Program Definition verified_lambdabox_pipeline {guard : abstract_guard_impl}
   (efl := EWellformed.all_env_flags)
@@ -237,32 +240,26 @@ Program Definition verified_lambdabox_typed_pipeline {guard : abstract_guard_imp
    constructors_as_blocks_transformation
      (efl := EInlineProjections.disable_projections_env_flag (ERemoveParams.switch_no_params EWellformed.all_env_flags))
      (has_app := eq_refl) (has_pars := eq_refl) (has_rel := eq_refl) (has_box := eq_refl) (has_cstrblocks := eq_refl) ▷
-   ETransform.optional_self_transform econf.(enable_cofix_to_fix)
-    ((* 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 ▷
-    (* 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))
-.
+   optional_unsafe_transforms econf.
 
  (* At the end of erasure we get a well-formed program (well-scoped globally and localy), without
     parameters in inductive declarations. The constructor applications are also transformed to a first-order
     "block"  application, of the right length, and the evaluation relation does not need to consider guarded
     fixpoints or case analyses on propositional content. All fixpoint bodies start with a lambda as well.
     Finally, projections are inlined to cases, so no `tProj` remains. *)
 
- Import EGlobalEnv EWellformed.
+Import EGlobalEnv EWellformed.
+
+Next Obligation.
+  destruct H. split => //. sq.
+  now eapply ETransform.expanded_eprogram_env_expanded_eprogram_cstrs.
+Qed.
 
- Next Obligation.
-   destruct H. split => //. sq.
-   now eapply ETransform.expanded_eprogram_env_expanded_eprogram_cstrs.
- Qed.
- Next Obligation.
-  destruct H. destruct enable_cofix_to_fix => //.
-  Qed.
+Next Obligation.
+  unfold optional_unsafe_transforms. cbn.
+  unfold optional_self_transform. cbn.
+  destruct enable_cofix_to_fix => //.
+Qed.
 
 Local Obligation Tactic := intros; eauto.
 
@@ -340,7 +337,7 @@ Program Definition erasure_pipeline_fast {guard : abstract_guard_impl} (efl := E
   let efl := EInlineProjections.disable_projections_env_flag (ERemoveParams.switch_no_params EWellformed.all_env_flags) in
   rebuild_wf_env_transform (efl :=  efl) true false ▷
   constructors_as_blocks_transformation (efl := efl) (has_app := eq_refl) (has_pars := eq_refl) (has_rel := eq_refl) (has_box := eq_refl) (has_cstrblocks := eq_refl) ▷
-  optional_cofix_to_fix_transform econf.
+  optional_unsafe_transforms econf.
 Next Obligation.
   destruct H; split => //. now eapply ETransform.expanded_eprogram_env_expanded_eprogram_cstrs.
 Qed.
@@ -360,7 +357,7 @@ Next Obligation.
   cbn in H. split; cbn; intuition eauto.
 Qed.
 Next Obligation.
-  cbn in H. unfold optional_cofix_to_fix_transform. destruct enable_cofix_to_fix => //.
+  cbn in H. unfold optional_unsafe_transforms. destruct enable_cofix_to_fix => //.
 Qed.
 Next Obligation.
   cbn in H. split; cbn; intuition eauto.
@@ -401,10 +398,10 @@ Program Definition run_erase_program {guard : abstract_guard_impl} econf :=
   if econf.(enable_typed_erasure) then run (typed_erasure_pipeline econf)
   else if econf.(enable_fast_remove_params) then
     run (erasure_pipeline_fast econf)
-  else run (erasure_pipeline ▷ (optional_cofix_to_fix_transform econf)).
+  else run (erasure_pipeline ▷ (optional_unsafe_transforms econf)).
 Next Obligation.
 Proof.
-  unfold optional_cofix_to_fix_transform.
+  unfold optional_unsafe_transforms.
   destruct enable_cofix_to_fix => //.
 Qed.
 
@@ -423,7 +420,8 @@ Definition erasure_fast_config :=
   {| enable_cofix_to_fix := false;
      dearging_config := default_dearging_config;
      enable_typed_erasure := false;
-     enable_fast_remove_params := true |}.
+     enable_fast_remove_params := true;
+     inductives_mapping := [] |}.
 
 Program Definition erase_fast_and_print_template_program (p : Ast.Env.program) : string :=
   erase_and_print_template_program erasure_fast_config p.
@@ -432,7 +430,8 @@ Definition typed_erasure_config :=
   {| enable_cofix_to_fix := false;
       dearging_config := default_dearging_config;
       enable_typed_erasure := true;
-      enable_fast_remove_params := true |}.
+      enable_fast_remove_params := true;
+      inductives_mapping := [] |}.
 
 (* Parameterized by a configuration for dearging, allowing to, e.g., override masks. *)
 Program Definition typed_erase_and_print_template_program (p : Ast.Env.program)
diff --git a/erasure/_CoqProject.in b/erasure/_CoqProject.in
@@ -39,6 +39,7 @@ theories/EConstructorsAsBlocks.v
 theories/EWcbvEvalCstrsAsBlocksInd.v
 theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
 theories/ECoInductiveToInductive.v
+theories/EReorderCstrs.v
 theories/EImplementBox.v
 
 theories/Typed/Annotations.v
diff --git a/erasure/theories/EReorderCstrs.v b/erasure/theories/EReorderCstrs.v
@@ -0,0 +1,97 @@
+From Coq Require Import List String Arith Lia.
+Import ListNotations.
+From Equations Require Import Equations.
+Set Equations Transparent.
+
+From MetaCoq.PCUIC Require Import PCUICAstUtils.
+From MetaCoq.Utils Require Import MCList bytestring utils monad_utils.
+From MetaCoq.Erasure Require Import EPrimitive EAst ESpineView EEtaExpanded EInduction ERemoveParams Erasure EGlobalEnv.
+
+Import Kernames.
+Import MCMonadNotation.
+
+Definition inductive_mapping : Set := Kernames.inductive * (bytestring.string * list nat).
+Definition inductives_mapping := list inductive_mapping.
+
+Fixpoint lookup_inductive {A} (Σ : list (inductive × A)) (kn : inductive) {struct Σ} : option A :=
+    match Σ with
+    | [] => None
+    | d :: tl => if kn == d.1 then Some d.2 else lookup_inductive tl kn
+    end.
+
+Section Reorder.
+  Context (Σ : global_declarations).
+  Context (mapping : inductives_mapping).
+
+  Definition lookup_constructor_mapping i m :=
+    '(tyna, tags) <- lookup_inductive mapping i ;;
+    List.nth_error tags m.
+
+  Definition lookup_constructor_ordinal i m :=
+    match lookup_constructor_mapping i m with
+    | None => m
+    | Some m' => m'
+    end.
+
+  Definition reorder_list_opt {A} tags (brs : list A) : option (list A) :=
+    mapopt (nth_error brs) tags.
+
+  Definition reorder_list {A} tags (l : list A) :=
+    option_get l (reorder_list_opt tags l).
+
+  Definition reorder_branches (i : inductive) (brs : list (list BasicAst.name × term)) : list (list BasicAst.name × term) :=
+    match lookup_inductive mapping i with
+    | None => brs
+    | Some (tyna, tags) => reorder_list tags brs
+    end.
+
+  Equations reorder (t : term) : term :=
+    | tVar na => tVar na
+    | tLambda nm bod => tLambda nm (reorder bod)
+    | tLetIn nm dfn bod => tLetIn nm dfn bod
+    | tApp fn arg => tApp (reorder fn) (reorder arg)
+    | tConst nm => tConst nm
+    | tConstruct i m args => tConstruct i (lookup_constructor_ordinal i m) (map reorder args)
+    | tCase i mch brs => tCase i mch (reorder_branches i.1 (map (on_snd reorder) brs))
+    | tFix mfix idx => tFix (map (map_def reorder) mfix) idx
+    | tCoFix mfix idx => tCoFix (map (map_def reorder) mfix) idx
+    | tProj (Kernames.mkProjection ind i arg) bod =>
+      tProj (Kernames.mkProjection ind i (lookup_constructor_ordinal ind arg)) (reorder bod)
+    | tPrim p => tPrim (map_prim reorder p)
+    | tLazy t => tLazy (reorder t)
+    | tForce t => tForce (reorder t)
+    | tRel n => tRel n
+    | tBox => tBox
+    | tEvar ev args => tEvar ev (map reorder args).
+
+    Definition reorder_constant_decl cb :=
+      {| cst_body := option_map reorder cb.(cst_body) |}.
+
+    Definition reorder_one_ind kn i (oib : one_inductive_body) : one_inductive_body :=
+      match lookup_inductive mapping {| inductive_mind := kn; inductive_ind := i |} with
+      | None => oib
+      | Some (tyna, tags) =>
+        {| ind_name := oib.(ind_name);
+           ind_propositional := oib.(ind_propositional);
+           ind_kelim := oib.(ind_kelim);
+           ind_ctors := reorder_list tags oib.(ind_ctors);
+           ind_projs := reorder_list tags oib.(ind_projs) |}
+      end.
+
+    Definition reorder_inductive_decl kn idecl :=
+      {| ind_finite := idecl.(ind_finite); ind_npars := 0;
+         ind_bodies := mapi (reorder_one_ind kn) idecl.(ind_bodies) |}.
+
+    Definition reorder_decl d :=
+      match d.2 with
+      | ConstantDecl cb => (d.1, ConstantDecl (reorder_constant_decl cb))
+      | InductiveDecl idecl => (d.1, InductiveDecl (reorder_inductive_decl d.1 idecl))
+      end.
+
+    Definition reorder_env Σ :=
+      map (reorder_decl) Σ.
+
+End Reorder.
+
+Definition reorder_program mapping (p : program) : program :=
+  (reorder_env mapping p.1, reorder mapping p.2).
