From d9b19cccfd5063748a1734087f32ff1383799026 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 14 Feb 2024 07:47:52 +0100 Subject: [PATCH] =?UTF-8?q?Resurrect=20the=20cofix=20transform,=20adding?= =?UTF-8?q?=20a=20new=20axiom=20for=20the=20admitted=20pr=E2=80=A6=20(#105?= =?UTF-8?q?6)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * 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 | 2 + erasure-plugin/src/g_metacoq_erasure.mlg | 135 +- .../src/metacoq_erasure_plugin.mlpack | 1 + erasure-plugin/theories/ETransform.v | 108 +- erasure-plugin/theories/Erasure.v | 177 ++- erasure/_CoqProject.in | 1 + erasure/theories/ECoInductiveToInductive.v | 1158 +++++++++++++++++ examples/metacoq_tour.v | 2 +- template-coq/src/ast_quoter.ml | 6 +- template-coq/src/constr_quoter.ml | 6 +- template-coq/src/quoter.ml | 14 +- test-suite/erasure_live_test.v | 26 +- test-suite/erasure_test.v | 20 +- 13 files changed, 1532 insertions(+), 124 deletions(-) create mode 100644 erasure/theories/ECoInductiveToInductive.v diff --git a/erasure-plugin/_PluginProject.in b/erasure-plugin/_PluginProject.in index 089e2bba1..c4015c525 100644 --- a/erasure-plugin/_PluginProject.in +++ b/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 diff --git a/erasure-plugin/src/g_metacoq_erasure.mlg b/erasure-plugin/src/g_metacoq_erasure.mlg index be1defda1..5e61fde14 100644 --- a/erasure-plugin/src/g_metacoq_erasure.mlg +++ b/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 type:\n\ + MetaCoq Erase .\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 diff --git a/erasure-plugin/src/metacoq_erasure_plugin.mlpack b/erasure-plugin/src/metacoq_erasure_plugin.mlpack index a366f9564..485dad598 100644 --- a/erasure-plugin/src/metacoq_erasure_plugin.mlpack +++ b/erasure-plugin/src/metacoq_erasure_plugin.mlpack @@ -64,6 +64,7 @@ ErasureFunctionProperties EOptimizePropDiscr EInlineProjections EConstructorsAsBlocks +ECoInductiveToInductive EProgram OptimizePropDiscr diff --git a/erasure-plugin/theories/ETransform.v b/erasure-plugin/theories/ETransform.v index 717e7320f..1dfc50628 100644 --- a/erasure-plugin/theories/ETransform.v +++ b/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. \ No newline at end of file diff --git a/erasure-plugin/theories/Erasure.v b/erasure-plugin/theories/Erasure.v index e41c094fb..736cfabf0 100644 --- a/erasure-plugin/theories/Erasure.v +++ b/erasure-plugin/theories/Erasure.v @@ -32,6 +32,32 @@ Import EWcbvEval. Local Obligation Tactic := program_simpl. +Record erasure_configuration := { + enable_cofix_to_fix : bool; + enable_typed_erasure : bool; + enable_fast_remove_params : bool; + dearging_config : dearging_config + }. + +Definition default_dearging_config := + {| overridden_masks := fun _ => None; + do_trim_const_masks := true; + do_trim_ctor_masks := false |}. + +(* This runs the cofix -> fix translation which is not entirely verified yet *) +Definition default_erasure_config := + {| enable_cofix_to_fix := true; + dearging_config := default_dearging_config; + enable_typed_erasure := true; + enable_fast_remove_params := true |}. + +(* 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 |}. + Axiom assume_welltyped_template_program_expansion : forall p (wtp : ∥ wt_template_program_env p ∥), let p' := EtaExpand.eta_expand_program p in @@ -60,14 +86,35 @@ Next Obligation. apply assume_preservation_template_program_env_expansion in ev as [ev']; eauto. Qed. -Program Definition verified_lambdabox_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : - Transform.t _ _ EAst.term EAst.term _ _ - (EProgram.eval_eprogram_env {| with_prop_case := true; with_guarded_fix := true; with_constructor_as_block := false |}) - (EProgram.eval_eprogram {| with_prop_case := false; with_guarded_fix := false; with_constructor_as_block := true |}) := +Definition final_wcbv_flags := {| + with_prop_case := false; + with_guarded_fix := false; + with_constructor_as_block := true |}. + +Program Definition optional_cofix_to_fix_transform 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 + (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)) + . + +Program Definition verified_lambdabox_pipeline {guard : abstract_guard_impl} + (efl := EWellformed.all_env_flags) + : Transform.t _ _ EAst.term EAst.term _ _ + (* Standard evaluation, with cases on prop, guarded fixpoints, applied constructors *) + (EProgram.eval_eprogram_env default_wcbv_flags) + (* Target evaluation, with no more cases on prop, unguarded fixpoints, constructors as block *) + (EProgram.eval_eprogram final_wcbv_flags) := + (* Simulation of the guarded fixpoint rules with a single unguarded one: the only "stuck" fixpoints remaining are unapplied. This translation is a noop on terms and environments. *) - guarded_to_unguarded_fix (fl := {| with_prop_case := true; with_guarded_fix := true; with_constructor_as_block := false |}) (wcon := eq_refl) eq_refl ▷ + guarded_to_unguarded_fix (fl := default_wcbv_flags) (wcon := eq_refl) eq_refl ▷ (* Remove all constructor parameters *) remove_params_optimization (wcon := eq_refl) ▷ (* Rebuild the efficient lookup table *) @@ -83,7 +130,7 @@ Program Definition verified_lambdabox_pipeline {guard : abstract_guard_impl} (ef (* First-order constructor representation *) 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) (hasbox := eq_refl) (has_cstrblocks := eq_refl). + (has_app := eq_refl) (has_pars := eq_refl) (has_rel := eq_refl) (has_box := eq_refl) (has_cstrblocks := eq_refl). (* 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 @@ -98,12 +145,11 @@ Next Obligation. now eapply ETransform.expanded_eprogram_env_expanded_eprogram_cstrs. Qed. - Program Definition verified_erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : Transform.t _ _ PCUICAst.term EAst.term _ _ PCUICTransform.eval_pcuic_program - (EProgram.eval_eprogram {| with_prop_case := false; with_guarded_fix := false; with_constructor_as_block := true |}) := + (EProgram.eval_eprogram final_wcbv_flags) := (* a bunch of nonsense for normalization preconditions *) let K ty (T : ty -> _) p := let p := T p in @@ -133,14 +179,14 @@ Proof. Qed. Lemma verified_lambdabox_pipeline_extends {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : - TransformExt.t (verified_lambdabox_pipeline) (fun p p' => extends (EEnvMap.GlobalContextMap.global_decls p.1) + TransformExt.t verified_lambdabox_pipeline (fun p p' => extends (EEnvMap.GlobalContextMap.global_decls p.1) (EEnvMap.GlobalContextMap.global_decls p'.1)) (fun p p' => extends p.1 p'.1). Proof. unfold verified_lambdabox_pipeline. tc. Qed. Lemma verified_lambdabox_pipeline_extends' {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : - TransformExt.t (verified_lambdabox_pipeline) extends_eprogram_env extends_eprogram. + TransformExt.t verified_lambdabox_pipeline extends_eprogram_env extends_eprogram. Proof. unfold verified_lambdabox_pipeline. tc. Qed. @@ -169,15 +215,14 @@ Program Definition pre_erasure_pipeline {guard : abstract_guard_impl} (efl := EW Program Definition erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : Transform.t _ _ Ast.term EAst.term _ _ TemplateProgram.eval_template_program - (EProgram.eval_eprogram {| with_prop_case := false; with_guarded_fix := false; with_constructor_as_block := true |}) := + (EProgram.eval_eprogram final_wcbv_flags) := pre_erasure_pipeline ▷ verified_erasure_pipeline. - -Program Definition verified_lambdabox_typed_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : +Program Definition verified_lambdabox_typed_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) econf : Transform.t _ _ EAst.term EAst.term _ _ (EProgram.eval_eprogram_env {| with_prop_case := false; with_guarded_fix := true; with_constructor_as_block := false |}) - (EProgram.eval_eprogram {| with_prop_case := false; with_guarded_fix := false; with_constructor_as_block := true |}) := + (EProgram.eval_eprogram final_wcbv_flags) := (* Simulation of the guarded fixpoint rules with a single unguarded one: the only "stuck" fixpoints remaining are unapplied. This translation is a noop on terms and environments. *) @@ -193,7 +238,17 @@ Program Definition verified_lambdabox_typed_pipeline {guard : abstract_guard_imp (* First-order constructor representation *) 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) (hasbox := eq_refl) (has_cstrblocks := eq_refl). + (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)) +. (* 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 @@ -207,16 +262,19 @@ Program Definition verified_lambdabox_typed_pipeline {guard : abstract_guard_imp destruct H. split => //. sq. now eapply ETransform.expanded_eprogram_env_expanded_eprogram_cstrs. Qed. + Next Obligation. + destruct H. destruct enable_cofix_to_fix => //. + Qed. Local Obligation Tactic := intros; eauto. Program Definition verified_typed_erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) - (cf : dearging_config) : + econf : Transform.t _ _ PCUICAst.term EAst.term _ _ PCUICTransform.eval_pcuic_program - (EProgram.eval_eprogram {| with_prop_case := false; with_guarded_fix := false; with_constructor_as_block := true |}) := + (EProgram.eval_eprogram final_wcbv_flags) := (* a bunch of nonsense for normalization preconditions *) let K ty (T : ty -> _) p := let p := T p in @@ -230,10 +288,10 @@ Program Definition verified_typed_erasure_pipeline {guard : abstract_guard_impl} (* Remove match on box early for dearging *) remove_match_on_box_typed_transform (wcon := eq_refl) (hastrel := eq_refl) (hastbox := eq_refl) ▷ (* Check if the preconditions for dearging are valid, otherwise dearging will be the identity *) - dearging_checks_transform cf (hastrel := eq_refl) (hastbox := eq_refl) ▷ - dearging_transform cf ▷ + dearging_checks_transform econf.(dearging_config) (hastrel := eq_refl) (hastbox := eq_refl) ▷ + dearging_transform econf.(dearging_config) ▷ rebuild_wf_env_transform true true ▷ - verified_lambdabox_typed_pipeline. + verified_lambdabox_typed_pipeline econf. Next Obligation. cbn in H. split; cbn; intuition eauto. @@ -244,13 +302,13 @@ Program Definition verified_typed_erasure_pipeline {guard : abstract_guard_impl} Program Definition typed_erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) - cf : + econf : Transform.t _ _ Ast.term EAst.term _ _ TemplateProgram.eval_template_program - (EProgram.eval_eprogram {| with_prop_case := false; with_guarded_fix := false; with_constructor_as_block := true |}) := + (EProgram.eval_eprogram final_wcbv_flags) := pre_erasure_pipeline ▷ - verified_typed_erasure_pipeline cf. + verified_typed_erasure_pipeline 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 @@ -260,9 +318,7 @@ Program Definition typed_erasure_pipeline {guard : abstract_guard_impl} Import EGlobalEnv EWellformed. -Definition run_erase_program {guard : abstract_guard_impl} := run erasure_pipeline. - -Program Definition erasure_pipeline_fast {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) := +Program Definition erasure_pipeline_fast {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) econf := (* a bunch of nonsense for normalization preconditions *) let K ty (T : ty -> _) p := let p := T p in @@ -285,7 +341,8 @@ Program Definition erasure_pipeline_fast {guard : abstract_guard_impl} (efl := E inline_projections_optimization (fl := EWcbvEval.target_wcbv_flags) (wcon := eq_refl) (hastrel := eq_refl) (hastbox := eq_refl) ▷ 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) (hasbox := eq_refl) (has_cstrblocks := eq_refl). + 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. Next Obligation. destruct H; split => //. now eapply ETransform.expanded_eprogram_env_expanded_eprogram_cstrs. Qed. @@ -304,11 +361,15 @@ Qed. 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 => //. +Qed. Next Obligation. cbn in H. split; cbn; intuition eauto. Qed. -Definition run_erase_program_fast {guard : abstract_guard_impl} := run erasure_pipeline_fast. +Definition run_erase_program_fast {guard : abstract_guard_impl} (econf : erasure_configuration) := + run (erasure_pipeline_fast econf). Local Open Scope string_scope. @@ -337,34 +398,20 @@ Global Existing Instance fake_normalization. Axiom assume_that_we_only_erase_on_welltyped_programs : forall {cf : checker_flags}, forall (p : Ast.Env.program), squash (TemplateProgram.wt_template_program p). -Program Definition erase_and_print_template_program (p : Ast.Env.program) - : string := - let p' := run_erase_program p _ in - time "Pretty printing" EPretty.print_program p'. -Next Obligation. - split. - now eapply assume_that_we_only_erase_on_welltyped_programs. - cbv [PCUICWeakeningEnvSN.normalizationInAdjustUniversesIn]. - pose proof @PCUICSN.normalization. - split; typeclasses eauto. -Qed. - -Program Definition erase_fast_and_print_template_program (p : Ast.Env.program) - : string := - let p' := run_erase_program_fast p _ in - time "pretty-printing" EPretty.print_program p'. +(* This also optionally runs the cofix to fix translation *) +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)). Next Obligation. - split. - now eapply assume_that_we_only_erase_on_welltyped_programs. - cbv [PCUICWeakeningEnvSN.normalizationInAdjustUniversesIn]. - pose proof @PCUICSN.normalization. - split; typeclasses eauto. +Proof. + unfold optional_cofix_to_fix_transform. + destruct enable_cofix_to_fix => //. Qed. -(* Parameterized by a configuration for dearging, allowing to, e.g., override masks. *) -Program Definition typed_erase_and_print_template_program_gen (p : Ast.Env.program) cf - : string := - let p' := run (typed_erasure_pipeline cf) p _ in +Program Definition erase_and_print_template_program econf (p : Ast.Env.program) : string := + let p' := run_erase_program econf p _ in time "Pretty printing" EPretty.print_program p'. Next Obligation. split. @@ -374,12 +421,22 @@ Next Obligation. split; typeclasses eauto. Qed. -Definition default_dearging_config := - {| overridden_masks := fun _ => None; - do_trim_const_masks := true; - do_trim_ctor_masks := false |}. +Definition erasure_fast_config := + {| enable_cofix_to_fix := false; + dearging_config := default_dearging_config; + enable_typed_erasure := false; + enable_fast_remove_params := true |}. -Definition typed_erase_and_print_template_program (p : Ast.Env.program) - : string := - typed_erase_and_print_template_program_gen p default_dearging_config. +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; + dearging_config := default_dearging_config; + enable_typed_erasure := true; + enable_fast_remove_params := true |}. +(* Parameterized by a configuration for dearging, allowing to, e.g., override masks. *) +Program Definition typed_erase_and_print_template_program (p : Ast.Env.program) + : string := + erase_and_print_template_program typed_erasure_config p. diff --git a/erasure/_CoqProject.in b/erasure/_CoqProject.in index a4a94c374..e0be67b79 100644 --- a/erasure/_CoqProject.in +++ b/erasure/_CoqProject.in @@ -38,6 +38,7 @@ theories/EInlineProjections.v theories/EConstructorsAsBlocks.v theories/EWcbvEvalCstrsAsBlocksInd.v theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v +theories/ECoInductiveToInductive.v theories/EImplementBox.v theories/Typed/Annotations.v diff --git a/erasure/theories/ECoInductiveToInductive.v b/erasure/theories/ECoInductiveToInductive.v new file mode 100644 index 000000000..3132dd66c --- /dev/null +++ b/erasure/theories/ECoInductiveToInductive.v @@ -0,0 +1,1158 @@ +(* Distributed under the terms of the MIT license. *) +From Coq Require Import Utf8 Program. +From MetaCoq.Utils Require Import utils. +From MetaCoq.Common Require Import config Kernames. +From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils + PCUICReflect PCUICWeakeningEnvConv PCUICWeakeningEnvTyp + PCUICTyping PCUICInversion + PCUICSafeLemmata. (* for welltyped *) +From MetaCoq.SafeChecker Require Import PCUICWfEnvImpl. +From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils EDeps EExtends + EEtaExpanded + ELiftSubst ECSubst ESpineView EGlobalEnv EInduction EWellformed EWcbvEval Extract Prelim + EEnvMap EArities EProgram. + +Import MCList (map_InP, map_InP_elim, map_InP_spec). + +Local Open Scope string_scope. +Set Asymmetric Patterns. +Import MCMonadNotation. + +From Equations Require Import Equations. +Set Equations Transparent. +Local Set Keyed Unification. +Require Import ssreflect ssrbool. + +(** We assumes [Prop ... -> Tn -> C here + and we want to produce an expansion: + λ x0 .. xn (), t x0 xn () *) + Equations make_n_aux (n : nat) (t : term) (acc : list term) : term := + make_n_aux 0 t acc => tLambda + (nNamed "thunk") + (mkApps (lift0 1 t) (rev (tRel 0 :: map (lift0 1) acc))); + make_n_aux (S n) t acc => + tLambda + (nNamed (make_name "x" (S n))) + (make_n_aux n (lift0 1 t) (tRel 0 :: map (lift0 1) acc)). + + Definition make_n (n : nat) (t : term) := make_n_aux n t []. + + (* Eval compute in make_n 2 (tRel 0). *) + +End Thunk. + +Section trans. + Context (Σ : GlobalContextMap.t). + + Definition trans_cofix (d : def term) := + {| dname := d.(dname); + dbody := Thunk.make_n d.(rarg) d.(dbody); + rarg := d.(rarg) |}. + + Fixpoint trans (t : term) : term := + match t with + | tRel i => tRel i + | tEvar ev args => tEvar ev (List.map trans args) + | tLambda na M => tLambda na (trans M) + | tApp u v => tApp (trans u) (trans v) + | tLetIn na b b' => tLetIn na (trans b) (trans b') + | tCase ind c brs => + let brs' := List.map (on_snd trans) brs in + match GlobalContextMap.lookup_inductive_kind Σ (fst ind).(inductive_mind) with + | Some CoFinite => + tCase ind (Thunk.force (trans c)) brs' + | _ => tCase ind (trans c) brs' + end + | tProj p c => + match GlobalContextMap.lookup_inductive_kind Σ p.(proj_ind).(inductive_mind) with + | Some CoFinite => tProj p (Thunk.force (trans c)) + | _ => tProj p (trans c) + end + | tFix mfix idx => + let mfix' := List.map (map_def trans) mfix in + tFix mfix' idx + | tCoFix mfix idx => + let mfix' := List.map (map_def trans) mfix in + let mfix' := List.map trans_cofix mfix' in + match nth_error mfix' idx with + | Some d => Thunk.make_n d.(rarg) (tFix mfix' idx) + | None => tCoFix mfix' idx + end + | tBox => t + | tVar _ => t + | tConst _ => t + | tConstruct ind i args => + match GlobalContextMap.lookup_inductive_kind Σ ind.(inductive_mind) with + | Some CoFinite => Thunk.make (tConstruct ind i (map trans args)) + | _ => tConstruct ind i (map trans args) + end + | tPrim p => tPrim (map_prim trans p) + end. + + (* cofix succ x := match x with Stream x xs => Stream (x + 1) (succ xs) -> + + fix succ x := match x () with Stream x xs => fun () => Stream (x + 1) (succ xs) + + cofix ones := Stream 1 ones -> + fix ones := fun () => Stream 1 ones + *) + + Lemma trans_mkApps f l : trans (mkApps f l) = mkApps (trans f) (map trans l). + Proof using Type. + induction l using rev_ind; simpl; auto. + now rewrite mkApps_app /= IHl map_app /= mkApps_app /=. + Qed. + + Lemma map_repeat {A B} (f : A -> B) x n : map f (repeat x n) = repeat (f x) n. + Proof using Type. + now induction n; simpl; auto; rewrite IHn. + Qed. + + Lemma map_trans_repeat_box n : map trans (repeat tBox n) = repeat tBox n. + Proof using Type. by rewrite map_repeat. Qed. + + Import ECSubst. + + Lemma csubst_mkApps {a k f l} : csubst a k (mkApps f l) = mkApps (csubst a k f) (map (csubst a k) l). + Proof using Type. + induction l using rev_ind; simpl; auto. + rewrite mkApps_app /= IHl. + now rewrite -[EAst.tApp _ _](mkApps_app _ _ [_]) map_app. + Qed. + + Lemma csubst_closed t k x : closedn k x -> csubst t k x = x. + Proof using Type. + induction x in k |- * using EInduction.term_forall_list_ind; simpl; auto. + all:try solve [intros; f_equal; solve_all; eauto]. + intros Hn. eapply Nat.ltb_lt in Hn. + - destruct (Nat.compare_spec k n); try lia. reflexivity. + - move/andP => []. intros. f_equal; solve_all; eauto. + - move/andP => []. intros. f_equal; solve_all; eauto. + - move/andP => []. intros. f_equal; solve_all; eauto. + Qed. + + Lemma closed_trans t k : closedn k t -> closedn k (trans t). + Proof using Type. + induction t in k |- * using EInduction.term_forall_list_ind; simpl; auto; + intros; try easy; + rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length; + unfold test_def in *; + simpl closed in *; try solve [simpl subst; simpl closed; f_equal; auto; rtoProp; solve_all]; try easy. + - destruct GlobalContextMap.lookup_inductive_kind as [[]|] => /= //; solve_all. + rewrite -Nat.add_1_r. now eapply closedn_lift. + - move/andP: H => [] clt clargs. + destruct GlobalContextMap.lookup_inductive_kind as [[]|] => /= //; rtoProp; solve_all; solve_all. + - destruct GlobalContextMap.lookup_inductive_kind as [[]|] => /= //; rtoProp; solve_all; solve_all. + - solve_all. destruct nth_error eqn:hnth. + * apply trust_cofix. + * cbn. unfold trans_cofix. len. solve_all. + unfold test_def. cbn. apply trust_cofix. + - primProp. solve_all_k 6. + Qed. + + Lemma subst_csubst_comm l t k b : + forallb (closedn 0) l -> closed t -> + subst l 0 (csubst t (#|l| + k) b) = + csubst t k (subst l 0 b). + Proof using Type. + intros hl cl. + rewrite !closed_subst //. + rewrite distr_subst. f_equal. + symmetry. solve_all. + rewrite subst_closed //. + eapply closed_upwards; tea. lia. + Qed. + + Lemma substl_subst s t : + forallb (closedn 0) s -> + substl s t = subst s 0 t. + Proof using Type. + induction s in t |- *; cbn; auto. + intros _. now rewrite subst_empty. + move/andP=> []cla cls. + rewrite (subst_app_decomp [_]). + cbn. rewrite lift_closed //. + rewrite closed_subst //. now eapply IHs. + Qed. + + Lemma substl_csubst_comm l t k b : + forallb (closedn 0) l -> closed t -> + substl l (csubst t (#|l| + k) b) = + csubst t k (substl l b). + Proof using Type. + intros hl cl. + rewrite substl_subst //. + rewrite substl_subst //. + apply subst_csubst_comm => //. + Qed. + + Lemma trans_csubst a k b : + closed a -> + trans (ECSubst.csubst a k b) = ECSubst.csubst (trans a) k (trans b). + Proof using Type. + induction b in k |- * using EInduction.term_forall_list_ind; simpl; auto; + intros cl; try easy; + rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length; + unfold test_def in *; + simpl closed in *; try solve [simpl subst; simpl closed; f_equal; auto; rtoProp; solve_all]; try easy. + - destruct (k ?= n)%nat; auto. + - destruct GlobalContextMap.lookup_inductive_kind as [[]|] => /= //. + 1,3,4:f_equal; rewrite map_map_compose; solve_all. + unfold Thunk.make. f_equal. cbn. + rewrite !map_map_compose. f_equal; solve_all. + specialize (H k cl). rewrite H. + rewrite closed_subst. now apply closed_trans. + rewrite closed_subst. now apply closed_trans. + now rewrite commut_lift_subst_rec. + - destruct GlobalContextMap.lookup_inductive_kind as [[]|] => /= //. + all:f_equal; eauto; try (rewrite /on_snd map_map_compose; solve_all). + unfold Thunk.force. f_equal; eauto. + - destruct GlobalContextMap.lookup_inductive_kind as [[]|] => /= //. + all:f_equal; eauto; try (rewrite /on_snd map_map_compose; solve_all). + unfold Thunk.force. f_equal; eauto. + - f_equal. solve_all. + rewrite !nth_error_map. destruct nth_error eqn:hnth => //=. + 2:{ f_equal. rewrite map_map_compose. eapply map_ext_in => x hin. + rewrite /trans_cofix /map_def //=. f_equal. len. + rewrite /Thunk.make_n. apply trust_cofix. + } + apply trust_cofix. + Qed. + + Lemma trans_substl s t : + forallb (closedn 0) s -> + trans (substl s t) = substl (map trans s) (trans t). + Proof using Type. + induction s in t |- *; simpl; auto. + move/andP => [] cla cls. + rewrite IHs //. f_equal. + now rewrite trans_csubst. + Qed. + + Lemma trans_iota_red pars args br : + forallb (closedn 0) args -> + trans (EGlobalEnv.iota_red pars args br) = EGlobalEnv.iota_red pars (map trans args) (on_snd trans br). + Proof using Type. + intros cl. + unfold EGlobalEnv.iota_red. + rewrite trans_substl //. + rewrite forallb_rev forallb_skipn //. + now rewrite map_rev map_skipn. + Qed. + + Lemma trans_fix_subst mfix : EGlobalEnv.fix_subst (map (map_def trans) mfix) = map trans (EGlobalEnv.fix_subst mfix). + Proof using Type. + unfold EGlobalEnv.fix_subst. + rewrite map_length. + generalize #|mfix|. + induction n; simpl; auto. + f_equal; auto. + Qed. + + Lemma trans_cunfold_fix mfix idx n f : + forallb (closedn 0) (EGlobalEnv.fix_subst mfix) -> + cunfold_fix mfix idx = Some (n, f) -> + cunfold_fix (map (map_def trans) mfix) idx = Some (n, trans f). + Proof using Type. + intros hfix. + unfold cunfold_fix. + rewrite nth_error_map. + destruct nth_error. + intros [= <- <-] => /=. f_equal. + now rewrite trans_substl // trans_fix_subst. + discriminate. + Qed. + + Lemma trans_cunfold_cofix mfix idx n f : + forallb (closedn 0) (EGlobalEnv.cofix_subst mfix) -> + cunfold_cofix mfix idx = Some (n, f) -> + exists d, nth_error mfix idx = Some d /\ + cunfold_fix (map trans_cofix mfix) idx = Some (n, substl (fix_subst (map trans_cofix mfix)) (Thunk.make_n (rarg d) (dbody d))). + Proof using Type. + intros hcofix. + unfold cunfold_cofix, cunfold_fix. + rewrite nth_error_map. + destruct nth_error. + intros [= <- <-] => /=. f_equal. exists d. split => //. + discriminate. + Qed. + + Lemma trans_nth {n l d} : + trans (nth n l d) = nth n (map trans l) (trans d). + Proof using Type. + induction l in n |- *; destruct n; simpl; auto. + Qed. + +End trans. + +Lemma is_box_inv b : is_box b -> ∑ args, b = mkApps tBox args. +Proof. + unfold is_box, EAstUtils.head. + destruct decompose_app eqn:da. + simpl. destruct t => //. + eapply decompose_app_inv in da. subst. + eexists; eauto. +Qed. + +Import EWcbvEval. + +Notation "Σ ⊢ s ⇓ t" := (eval Σ s t) (at level 50, s, t at next level) : type_scope. + +Lemma eval_is_box {wfl:WcbvFlags} Σ t u : Σ ⊢ t ⇓ u -> is_box t -> u = EAst.tBox. +Proof. + intros ev; induction ev => //. + - rewrite is_box_tApp. + intros isb. intuition congruence. + - rewrite is_box_tApp. move/IHev1 => ?; solve_discr. + - rewrite is_box_tApp. move/IHev1 => ?; solve_discr. + - rewrite is_box_tApp. move/IHev1 => ?. subst => //. + - rewrite is_box_tApp. move/IHev1 => ?. subst. solve_discr. + - rewrite is_box_tApp. move/IHev1 => ?. subst. cbn in i. + destruct EWcbvEval.with_guarded_fix => //. + - destruct t => //. +Qed. + +Lemma isType_tSort {cf:checker_flags} {Σ : global_env_ext} {Γ l A} {wfΣ : wf Σ} : + Σ ;;; Γ |- tSort (sType (Universe.make l)) : A -> isType Σ Γ (tSort (sType (Universe.make l))). +Proof. + intros HT. + eapply inversion_Sort in HT as [l' [wfΓ Hs]]; auto. + eexists; econstructor; eauto. cbn. split; eauto. econstructor; eauto. +Qed. + +Lemma isType_it_mkProd {cf:checker_flags} {Σ : global_env_ext} {Γ na dom codom A} {wfΣ : wf Σ} : + Σ ;;; Γ |- tProd na dom codom : A -> + isType Σ Γ (tProd na dom codom). +Proof. + intros HT. + eapply inversion_Prod in HT as (? & ? & ? & ? & ?); auto. + eexists; cbn; econstructor; split; eauto. econstructor; eauto. +Qed. + +Definition trans_constant_decl Σ cb := + {| cst_body := option_map (trans Σ) cb.(cst_body) |}. + +Definition trans_decl Σ d := + match d with + | ConstantDecl cb => ConstantDecl (trans_constant_decl Σ cb) + | InductiveDecl idecl => d + end. + +Definition trans_env Σ := + map (on_snd (trans_decl Σ)) Σ.(GlobalContextMap.global_decls). + +Import EnvMap. + +Program Fixpoint trans_env' Σ : EnvMap.fresh_globals Σ -> global_context := + match Σ with + | [] => fun _ => [] + | hd :: tl => fun HΣ => + let Σg := GlobalContextMap.make tl (fresh_globals_cons_inv HΣ) in + on_snd (trans_decl Σg) hd :: trans_env' tl (fresh_globals_cons_inv HΣ) + end. + +Import EGlobalEnv EExtends. + +(* Lemma extends_is_propositional {Σ Σ'} : + wf_glob Σ' -> extends Σ Σ' -> + forall ind, + match inductive_isprop_and_pars Σ ind with + | Some b => inductive_isprop_and_pars Σ' ind = Some b + | None => inductive_isprop_and_pars Σ' ind = None + end. +Proof. + intros wf ex ind. + rewrite /inductive_isprop_and_pars. + destruct lookup_env eqn:lookup => //. + now rewrite (extends_lookup wf ex lookup). + +Qed. *) + +Lemma extends_inductive_isprop_and_pars {efl : EEnvFlags} {Σ Σ' ind} : extends Σ Σ' -> wf_glob Σ' -> + isSome (lookup_inductive Σ ind) -> + inductive_isprop_and_pars Σ ind = inductive_isprop_and_pars Σ' ind. +Proof. + intros ext wf; cbn. + unfold inductive_isprop_and_pars. cbn. + destruct lookup_env as [[]|] eqn:hl => //. + rewrite (extends_lookup wf ext hl). + destruct nth_error => //. +Qed. + +Lemma extends_lookup_inductive_kind {efl : EEnvFlags} {Σ Σ' ind} : extends Σ Σ' -> wf_glob Σ' -> + isSome (lookup_minductive Σ ind) -> + lookup_inductive_kind Σ ind = lookup_inductive_kind Σ' ind. +Proof. + intros ext wf. + unfold lookup_inductive_kind. cbn. + destruct lookup_env as [[]|] eqn:hl => //. + now rewrite (extends_lookup wf ext hl). +Qed. + +Lemma wellformed_trans_extends {wfl: EEnvFlags} {Σ : GlobalContextMap.t} t : + forall n, EWellformed.wellformed Σ n t -> + forall {Σ' : GlobalContextMap.t}, extends Σ Σ' -> wf_glob Σ' -> + trans Σ t = trans Σ' t. +Proof. + induction t using EInduction.term_forall_list_ind; cbn -[lookup_constant lookup_inductive + lookup_projection + lookup_constructor + GlobalContextMap.lookup_inductive_kind]; intros => //. + all:unfold wf_fix_gen in *; rtoProp; intuition auto. + all:try now f_equal; eauto; solve_all. + - rewrite !GlobalContextMap.lookup_inductive_kind_spec. + destruct lookup_constructor as [[[mdecl idecl] cdecl]|] eqn:hl => //. + destruct cstr_as_blocks. + { move/andP: H2 => [] hpars hargs. + assert (map (trans Σ) args = map (trans Σ') args) as -> by solve_all. + rewrite (extends_lookup_inductive_kind H0 H1) //. + apply lookup_constructor_lookup_inductive in hl. + unfold lookup_inductive in hl. + destruct lookup_minductive => //. } + { destruct args => // /=. + rewrite (extends_lookup_inductive_kind H0 H1) //. + apply lookup_constructor_lookup_inductive in hl. + unfold lookup_inductive in hl. + destruct lookup_minductive => //. } + - rewrite !GlobalContextMap.lookup_inductive_kind_spec. + destruct lookup_inductive as [[mdecl idecl]|] eqn:hl => //. + assert (map (on_snd (trans Σ)) l = map (on_snd (trans Σ')) l) as -> by solve_all. + rewrite (extends_lookup_inductive_kind H0 H1) //. + unfold lookup_inductive in hl. + destruct lookup_minductive => //. + rewrite (IHt _ H4 _ H0 H1) //. + - rewrite !GlobalContextMap.lookup_inductive_kind_spec. + destruct (lookup_projection) as [[[[mdecl idecl] cdecl] pdecl]|] eqn:hl => //. + eapply lookup_projection_lookup_constructor in hl. + eapply lookup_constructor_lookup_inductive in hl. + rewrite (extends_lookup_inductive_kind H0 H1) //. + unfold lookup_inductive in hl. + destruct lookup_minductive => //. + rewrite (IHt _ H2 _ H0 H1) //. + - apply trust_cofix. +Qed. + +Lemma wellformed_trans_decl_extends {wfl: EEnvFlags} {Σ : GlobalContextMap.t} t : + wf_global_decl Σ t -> + forall {Σ' : GlobalContextMap.t}, extends Σ Σ' -> wf_glob Σ' -> + trans_decl Σ t = trans_decl Σ' t. +Proof. + destruct t => /= //. + intros wf Σ' ext wf'. f_equal. unfold trans_constant_decl. f_equal. + destruct (cst_body c) => /= //. f_equal. + now eapply wellformed_trans_extends. +Qed. + +Lemma lookup_env_trans_env_Some {efl : EEnvFlags} {Σ : GlobalContextMap.t} kn d : + wf_glob Σ -> + GlobalContextMap.lookup_env Σ kn = Some d -> + ∑ Σ' : GlobalContextMap.t, + [× extends_prefix Σ' Σ, wf_global_decl Σ' d & + lookup_env (trans_env Σ) kn = Some (trans_decl Σ' d)]. +Proof. + rewrite GlobalContextMap.lookup_env_spec. + destruct Σ as [Σ map repr wf]. + induction Σ in map, repr, wf |- *; simpl; auto => //. + intros wfg. + case: eqb_specT => //. + - intros ->. cbn. intros [= <-]. + exists (GlobalContextMap.make Σ (fresh_globals_cons_inv wf)). split. + cbn. now exists [a]. now depelim wfg. + depelim wfg; eauto. + f_equal. symmetry. eapply wellformed_trans_decl_extends. cbn; auto. cbn. + now eapply extends_fresh. cbn. now constructor. + - intros _. + set (Σ' := GlobalContextMap.make Σ (fresh_globals_cons_inv wf)). + specialize (IHΣ (GlobalContextMap.map Σ') (GlobalContextMap.repr Σ') (GlobalContextMap.wf Σ')). + cbn in IHΣ. forward IHΣ. now depelim wfg. + intros hl. specialize (IHΣ hl) as [Σ'' [ext wfgd hl']]. + exists Σ''. split => //. + * destruct ext as [? ->]. + now exists (a :: x). + * rewrite -hl'. f_equal. + clear -wfg. + eapply map_ext_in => kn hin. unfold on_snd. f_equal. + symmetry. eapply wellformed_trans_decl_extends => //. cbn. + eapply lookup_env_In in hin. 2:now depelim wfg. + depelim wfg. eapply lookup_env_wellformed; tea. + cbn. destruct a. eapply extends_fresh. now depelim wfg. +Qed. + +Lemma lookup_env_map_snd Σ f kn : lookup_env (List.map (on_snd f) Σ) kn = option_map f (lookup_env Σ kn). +Proof. + induction Σ; cbn; auto. + case: eqb_spec => //. +Qed. + +Lemma lookup_env_trans_env_None {efl : EEnvFlags} {Σ : GlobalContextMap.t} kn : + GlobalContextMap.lookup_env Σ kn = None -> + lookup_env (trans_env Σ) kn = None. +Proof. + rewrite GlobalContextMap.lookup_env_spec. + destruct Σ as [Σ map repr wf]. + cbn. intros hl. rewrite lookup_env_map_snd hl //. +Qed. + +Lemma lookup_env_trans {efl : EEnvFlags} {Σ : GlobalContextMap.t} kn : + wf_glob Σ -> + lookup_env (trans_env Σ) kn = option_map (trans_decl Σ) (lookup_env Σ kn). +Proof. + intros wf. + rewrite -GlobalContextMap.lookup_env_spec. + destruct (GlobalContextMap.lookup_env Σ kn) eqn:hl. + - eapply lookup_env_trans_env_Some in hl as [Σ' [ext wf' hl']] => /= //. + rewrite hl'. f_equal. + eapply wellformed_trans_decl_extends; eauto. + now eapply extends_prefix_extends. + - cbn. now eapply lookup_env_trans_env_None in hl. +Qed. + +Lemma is_propositional_trans {efl : EEnvFlags} {Σ : GlobalContextMap.t} ind : + wf_glob Σ -> + inductive_isprop_and_pars Σ ind = inductive_isprop_and_pars (trans_env Σ) ind. +Proof. + rewrite /inductive_isprop_and_pars => wf. + rewrite /lookup_inductive /lookup_minductive. + rewrite (lookup_env_trans (inductive_mind ind) wf) //. + rewrite /GlobalContextMap.inductive_isprop_and_pars /GlobalContextMap.lookup_inductive + /GlobalContextMap.lookup_minductive. + destruct lookup_env as [[decl|]|] => //. +Qed. + +Lemma is_propositional_cstr_trans {efl : EEnvFlags} {Σ : GlobalContextMap.t} ind c : + wf_glob Σ -> + constructor_isprop_pars_decl Σ ind c = constructor_isprop_pars_decl (trans_env Σ) ind c. +Proof. + rewrite /constructor_isprop_pars_decl => wf. + rewrite /lookup_constructor /lookup_inductive /lookup_minductive. + rewrite (lookup_env_trans (inductive_mind ind) wf). + rewrite /GlobalContextMap.inductive_isprop_and_pars /GlobalContextMap.lookup_inductive + /GlobalContextMap.lookup_minductive. + destruct lookup_env as [[decl|]|] => //. +Qed. + + +Lemma closed_iota_red pars c args brs br : + forallb (closedn 0) args -> + nth_error brs c = Some br -> + #|skipn pars args| = #|br.1| -> + closedn #|br.1| br.2 -> + closed (iota_red pars args br). +Proof. + intros clargs hnth hskip clbr. + rewrite /iota_red. + eapply ECSubst.closed_substl => //. + now rewrite forallb_rev forallb_skipn. + now rewrite List.rev_length hskip Nat.add_0_r. +Qed. + +Lemma isFix_mkApps t l : isFix (mkApps t l) = isFix t && match l with [] => true | _ => false end. +Proof. + induction l using rev_ind; cbn. + - now rewrite andb_true_r. + - rewrite mkApps_app /=. now destruct l => /= //; rewrite andb_false_r. +Qed. + +Lemma lookup_constructor_trans {efl : EEnvFlags} {Σ : GlobalContextMap.t} {ind c} : + wf_glob Σ -> + lookup_constructor Σ ind c = lookup_constructor (trans_env Σ) ind c. +Proof. + intros wfΣ. rewrite /lookup_constructor /lookup_inductive /lookup_minductive. + rewrite lookup_env_trans // /=. destruct lookup_env => // /=. + destruct g => //. +Qed. + +Lemma constructor_isprop_pars_decl_inductive {Σ ind c} {prop pars cdecl} : + constructor_isprop_pars_decl Σ ind c = Some (prop, pars, cdecl) -> + inductive_isprop_and_pars Σ ind = Some (prop, pars). +Proof. + rewrite /constructor_isprop_pars_decl /inductive_isprop_and_pars /lookup_constructor. + destruct lookup_inductive as [[mdecl idecl]|]=> /= //. + destruct nth_error => //. congruence. +Qed. + +Lemma value_constructor_as_block {wfl : WcbvFlags} {Σ ind c args} : value Σ (tConstruct ind c args) -> + All (value Σ) args. +Proof. + intros h; depelim h. + - depelim a. cbn in i. destruct args => //. + - eauto. + - depelim v; solve_discr. +Qed. + +Lemma constructor_isprop_pars_decl_constructor {Σ ind c prop npars cdecl} : + constructor_isprop_pars_decl Σ ind c = Some (prop, npars, cdecl) -> + ∑ mdecl idecl, lookup_constructor Σ ind c = Some (mdecl, idecl, cdecl) /\ npars = ind_npars mdecl. +Proof. + rewrite /constructor_isprop_pars_decl. + destruct lookup_constructor as [[[mdecl idecl] cdecl']|] eqn:hl => //=. + intros [= <- <- <-]. + exists mdecl, idecl; split => //. +Qed. + +Lemma isLambda_make_n n t : isLambda (Thunk.make_n n t). +Proof. + induction n; cbn => //. +Qed. + +Lemma value_trans {efl : EEnvFlags} {fl : WcbvFlags} {hasc : cstr_as_blocks = true} {wcon : with_constructor_as_block = true} {Σ : GlobalContextMap.t} {c} : + has_tApp -> wf_glob Σ -> + wellformed Σ 0 c -> + value Σ c -> + value (trans_env Σ) (trans Σ c). +Proof. + intros hasapp wfg wf h. + revert c h wf. apply: Ee.value_values_ind. + - intros t; destruct t => //; cbn -[lookup_constructor GlobalContextMap.lookup_inductive_kind]. + all:try solve [intros; repeat constructor => //]. + destruct args => //. + move=> /andP[] wc. now rewrite wcon in wc. + move=> _ /andP [] hascof /andP[] /Nat.ltb_lt /nth_error_Some hnth hm. + destruct nth_error => //. + pose proof (isLambda_make_n (rarg d) (tFix (map trans_cofix mfix) idx)). + destruct Thunk.make_n => //. apply trust_cofix. + (* do 3 constructor. *) + - intros p pv IH wf. cbn. constructor. constructor 2. + cbn in wf. move/andP: wf => [hasp tp]. + primProp. depelim tp; depelim pv; depelim IH; constructor; cbn in *; rtoProp; intuition auto; solve_all. + - intros ind c mdecl idecl cdecl args wc hl harglen hargs ihargs. + simpl. rewrite hasc. move/andP => [] /andP[] hascstr _ /andP[] hpargs wfargs. + cbn -[GlobalContextMap.lookup_inductive_kind]. + destruct GlobalContextMap.lookup_inductive_kind as [[]|] eqn:hl' => //. + 1,3,4:eapply value_constructor; tea; [erewrite <-lookup_constructor_trans; tea|now len|solve_all]. + now do 2 constructor. + - intros f args vh harglen hargs ihargs. + rewrite wellformed_mkApps // => /andP[] wff wfargs. + rewrite trans_mkApps. + depelim vh. congruence. + cbn. + simpl in wff; move/andP: wff => [] hascof /andP[] /Nat.ltb_lt wfidx wffix. + apply nth_error_Some in wfidx. + destruct nth_error eqn:heq => //. + all: apply trust_cofix. +Qed. + +Ltac destruct_times := + match goal with + | [ H : pair _ _ |- _ ] => destruct H + | [ H : MCProd.and3 _ _ _ |- _ ] => destruct H + | [ H : MCProd.and4 _ _ _ _ |- _ ] => destruct H + | [ H : MCProd.and5 _ _ _ _ _ |- _ ] => destruct H + | [ H : MCProd.and6 _ _ _ _ _ _ |- _ ] => destruct H + | [ H : MCProd.and7 _ _ _ _ _ _ _ |- _ ] => destruct H + | [ H : MCProd.and8 _ _ _ _ _ _ _ _ |- _ ] => destruct H + | [ H : MCProd.and9 _ _ _ _ _ _ _ _ _ |- _ ] => destruct H + | [ H : MCProd.and10 _ _ _ _ _ _ _ _ _ _ |- _ ] => destruct H + end. + +From MetaCoq.Erasure Require Import EWcbvEvalCstrsAsBlocksInd. +Lemma trans_correct {efl : EEnvFlags} {fl} {wcon : with_constructor_as_block = true} + {wcb : cstr_as_blocks = true} + {Σ : GlobalContextMap.t} t v : + has_tApp -> + wf_glob Σ -> + closed_env Σ -> + @Ee.eval fl Σ t v -> + wellformed Σ 0 t -> + @Ee.eval fl (trans_env Σ) (trans Σ t) (trans Σ v). +Proof. + intros hasapp wfΣ clΣ ev wf. + revert t v wf ev. + eapply + (eval_preserve_mkApps_ind fl wcon (efl := efl) Σ _ + (wellformed Σ) (Qpres := Qpreserves_wellformed efl _ wfΣ)) => //; eauto; + intros; repeat destruct_times; try solve [econstructor; eauto 3]. + + - intros. eapply eval_wellformed in H; tea. + + - econstructor; eauto. + rewrite trans_csubst // in e. now eapply wellformed_closed. + + - rewrite trans_csubst // in e. now eapply wellformed_closed. + cbn. econstructor; eauto. + + - assert (forallb (wellformed Σ 0) args). + cbn -[lookup_constructor lookup_constructor_pars_args] in i2. + rewrite wcb in i2. move/and3P: i2 => [] _ _ hargs. + solve_all. + rewrite trans_iota_red // in e. + { solve_all. now eapply wellformed_closed. } + cbn -[lookup_constructor lookup_constructor_pars_args + GlobalContextMap.lookup_inductive_kind] in e0 |- *. + eapply eval_closed in H as evc => //. + 2:{ now eapply wellformed_closed. } + rewrite GlobalContextMap.lookup_inductive_kind_spec in e0 *. + destruct lookup_inductive_kind as [[]|] eqn:hl => //. + 1,3,4:eapply eval_iota_block; eauto; + [now rewrite -is_propositional_cstr_trans| + rewrite nth_error_map H2 //|now len| + try (cbn; rewrite -H4 !skipn_length map_length //)]. + eapply eval_iota_block. + 1,3,4: eauto. + + now rewrite -is_propositional_cstr_trans. + + rewrite nth_error_map H2 //. + + eapply eval_beta. eapply e0; eauto. + constructor; eauto. + rewrite closed_subst // simpl_subst_k //. + eapply Ee.eval_to_value in H. + eapply value_constructor_as_block in H. + eapply constructor_isprop_pars_decl_constructor in H1 as [mdecl [idecl [hl' hp]]]. + econstructor; eauto. + now erewrite <-lookup_constructor_trans. len. + now rewrite /cstr_arity. + instantiate (1 := map (trans Σ) args). + eapply All2_All2_Set. + eapply values_final. solve_all. + unshelve eapply value_trans; tea. + + now len. + + now len. + + exact e. + + - subst brs. + cbn -[lookup_constructor lookup_constructor_pars_args + GlobalContextMap.lookup_inductive_kind] in e0 |- *. + rewrite GlobalContextMap.lookup_inductive_kind_spec. + rewrite trans_substl ?map_repeat /= in e. + { now apply forallb_repeat. } + destruct lookup_inductive_kind as [[]|] eqn:hl => //. + 1,3,4:eapply eval_iota_sing; [eauto|eauto| + now rewrite -is_propositional_trans|reflexivity| + rewrite /= ?trans_substl //; simpl; eauto]. + eapply eval_iota_sing; eauto. + eapply eval_box; eauto. + rewrite -is_propositional_trans //. + reflexivity. + + - apply trust_cofix. + - apply trust_cofix. + - apply trust_cofix. + - apply trust_cofix. + - apply trust_cofix. + - apply trust_cofix. + - apply trust_cofix. + - apply trust_cofix. + - apply trust_cofix. + - apply trust_cofix. + - apply trust_cofix. + - apply trust_cofix. +Qed. +(* + - rewrite trans_mkApps in e1. + simpl in *. + eapply eval_closed in ev1 => //. + rewrite closedn_mkApps in ev1. + move: ev1 => /andP [] clfix clargs. + eapply Ee.eval_fix; eauto. + rewrite map_length. + eapply trans_cunfold_fix; tea. + eapply closed_fix_subst. tea. + rewrite trans_mkApps in IHev3. apply IHev3. + rewrite closedn_mkApps clargs. + eapply eval_closed in ev2; tas. rewrite ev2 /= !andb_true_r. + eapply closed_cunfold_fix; tea. + + - move/andP => [] clf cla. + eapply eval_closed in ev1 => //. + rewrite closedn_mkApps in ev1. + move: ev1 => /andP [] clfix clargs. + eapply eval_closed in ev2; tas. + rewrite trans_mkApps in IHev1 |- *. + simpl in *. eapply Ee.eval_fix_value. auto. auto. auto. + eapply trans_cunfold_fix; eauto. + eapply closed_fix_subst => //. + now rewrite map_length. + + - move/andP => [] clf cla. + eapply eval_closed in ev1 => //. + eapply eval_closed in ev2; tas. + simpl in *. eapply Ee.eval_fix'. auto. auto. + eapply trans_cunfold_fix; eauto. + eapply closed_fix_subst => //. + eapply IHev2; tea. eapply IHev3. + apply/andP; split => //. + eapply closed_cunfold_fix; tea. + + - move/andP => [] cd clbrs. specialize (IHev1 cd). + rewrite closedn_mkApps in IHev2. + move: (eval_closed _ clΣ _ _ cd ev1). + rewrite closedn_mkApps. + move/andP => [] clfix clargs. + forward IHev2. + { rewrite clargs clbrs !andb_true_r. + eapply closed_cunfold_cofix; tea. } + rewrite -> trans_mkApps in IHev1, IHev2. simpl. + rewrite GlobalContextMap.lookup_inductive_kind_spec in IHev2 |- *. + destruct EGlobalEnv.lookup_inductive_kind as [[]|] eqn:isp => //. + simpl in IHev1. + eapply Ee.eval_cofix_case. tea. + apply trans_cunfold_cofix; tea. eapply closed_cofix_subst; tea. + apply IHev2. + eapply Ee.eval_cofix_case; tea. + apply trans_cunfold_cofix; tea. eapply closed_cofix_subst; tea. + simpl in *. + eapply Ee.eval_cofix_case; tea. + apply trans_cunfold_cofix; tea. eapply closed_cofix_subst; tea. + eapply Ee.eval_cofix_case; tea. + apply trans_cunfold_cofix; tea. eapply closed_cofix_subst; tea. + + - intros cd. specialize (IHev1 cd). + move: (eval_closed _ clΣ _ _ cd ev1). + rewrite closedn_mkApps; move/andP => [] clfix clargs. forward IHev2. + { rewrite closedn_mkApps clargs andb_true_r. eapply closed_cunfold_cofix; tea. } + rewrite GlobalContextMap.inductive_isprop_and_pars_spec in IHev2 |- *. + destruct EGlobalEnv.inductive_isprop_and_pars as [[[] pars]|] eqn:isp; auto. + rewrite -> trans_mkApps in IHev1, IHev2. simpl in *. + econstructor; eauto. + apply trans_cunfold_cofix; tea. eapply closed_cofix_subst; tea. + rewrite -> trans_mkApps in IHev1, IHev2. simpl in *. + econstructor; eauto. + apply trans_cunfold_cofix; tea. eapply closed_cofix_subst; tea. + + - rewrite /declared_constant in isdecl. + move: (lookup_env_trans c wfΣ). + rewrite isdecl /= //. + intros hl. + econstructor; tea. cbn. rewrite e //. + apply IHev. + eapply lookup_env_closed in clΣ; tea. + move: clΣ. rewrite /closed_decl e //. + + - move=> cld. + eapply eval_closed in ev1; tea. + move: ev1; rewrite closedn_mkApps /= => clargs. + rewrite GlobalContextMap.inductive_isprop_and_pars_spec. + rewrite (constructor_isprop_pars_decl_inductive e1). + rewrite trans_mkApps in IHev1. + specialize (IHev1 cld). + eapply Ee.eval_proj; tea. + now rewrite -is_propositional_cstr_trans. + now len. rewrite nth_error_map e3 //. + eapply IHev2. + eapply nth_error_forallb in e3; tea. + + - congruence. + + - rewrite GlobalContextMap.inductive_isprop_and_pars_spec. + now rewrite e0. + + - move/andP=> [] clf cla. + rewrite trans_mkApps. + eapply eval_construct; tea. + rewrite -lookup_constructor_trans //. exact e0. + rewrite trans_mkApps in IHev1. now eapply IHev1. + now len. + now eapply IHev2. + + - congruence. + + - move/andP => [] clf cla. + specialize (IHev1 clf). specialize (IHev2 cla). + eapply Ee.eval_app_cong; eauto. + eapply Ee.eval_to_value in ev1. + destruct ev1; simpl in *; eauto. + * destruct t => //; rewrite trans_mkApps /=. + * destruct with_guarded_fix. + + move: i. + rewrite !negb_or. + rewrite trans_mkApps !isFixApp_mkApps !isConstructApp_mkApps !isPrimApp_mkApps. + destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //. + rewrite !andb_true_r. + rtoProp; intuition auto. + destruct v => /= //. + destruct v => /= //. + destruct v => /= //. + + move: i. + rewrite !negb_or. + rewrite trans_mkApps !isConstructApp_mkApps !isPrimApp_mkApps. + destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //. + destruct v => /= //. + - destruct t => //. + all:constructor; eauto. cbn [atom trans] in i |- *. + rewrite -lookup_constructor_trans //. destruct l => //. +Qed. +*) +From MetaCoq.Erasure Require Import EEtaExpanded. + +Lemma isLambda_trans Σ t : isLambda t -> isLambda (trans Σ t). +Proof. destruct t => //. Qed. +Lemma isBox_trans Σ t : isBox t -> isBox (trans Σ t). +Proof. destruct t => //. Qed. + +Lemma trans_expanded {Σ : GlobalContextMap.t} t : expanded Σ t -> expanded Σ (trans Σ t). +Proof. + induction 1 using expanded_ind. + all:try solve[constructor; eauto; solve_all]. + all:rewrite ?trans_mkApps. + - eapply expanded_mkApps_expanded => //. solve_all. + - cbn -[GlobalContextMap.lookup_inductive_kind]. + rewrite GlobalContextMap.lookup_inductive_kind_spec. + destruct lookup_inductive_kind as [[]|] => /= //. + 2-3:constructor; eauto; solve_all. + constructor; eauto; solve_all. cbn. + unfold Thunk.force. + eapply isEtaExp_expanded. + all:apply trust_cofix. + - apply trust_cofix. + - apply trust_cofix. + - apply trust_cofix. + - apply trust_cofix. +Qed. + (*cbn. + eapply isEtaExp_substl. eapply forallb_repeat => //. + destruct branches as [|[]]; cbn in heq; noconf heq. + cbn -[isEtaExp] in *. depelim H1. cbn in H1. + now eapply expanded_isEtaExp. + constructor; eauto; solve_all. + depelim H1. depelim H1. do 2 (constructor; intuition auto). + solve_all. + - cbn -[GlobalContextMap.inductive_isprop_and_pars]. + rewrite GlobalContextMap.inductive_isprop_and_pars_spec. + destruct inductive_isprop_and_pars as [[[|] _]|] => /= //. + constructor. all:constructor; auto. + - cbn. eapply expanded_tFix. solve_all. + rewrite isLambda_trans //. + - eapply expanded_tConstruct_app; tea. + now len. solve_all. +Qed. +*) +Lemma trans_expanded_irrel {efl : EEnvFlags} {Σ : GlobalContextMap.t} t : wf_glob Σ -> expanded Σ t -> expanded (trans_env Σ) t. +Proof. + intros wf; induction 1 using expanded_ind. + all:try solve[constructor; eauto; solve_all]. + eapply expanded_tConstruct_app. + destruct H as [[H ?] ?]. + split => //. split => //. red. + red in H. rewrite lookup_env_trans // /= H //. 1-2:eauto. auto. solve_all. +Qed. + +Lemma trans_expanded_decl {Σ : GlobalContextMap.t} t : expanded_decl Σ t -> expanded_decl Σ (trans_decl Σ t). +Proof. + destruct t as [[[]]|] => /= //. + unfold expanded_constant_decl => /=. + apply trans_expanded. +Qed. + +Lemma trans_expanded_decl_irrel {efl : EEnvFlags} {Σ : GlobalContextMap.t} t : wf_glob Σ -> expanded_decl Σ t -> expanded_decl (trans_env Σ) t. +Proof. + destruct t as [[[]]|] => /= //. + unfold expanded_constant_decl => /=. + apply trans_expanded_irrel. +Qed. + +Lemma trans_env_extends' {efl : EEnvFlags} {Σ Σ' : GlobalContextMap.t} : + extends_prefix Σ Σ' -> + wf_glob Σ' -> + List.map (on_snd (trans_decl Σ)) Σ.(GlobalContextMap.global_decls) = + List.map (on_snd (trans_decl Σ')) Σ.(GlobalContextMap.global_decls). +Proof. + intros ext. + destruct Σ as [Σ map repr wf]; cbn in *. + move=> wfΣ. + assert (extends_prefix Σ Σ); auto. now exists []. + assert (wf_glob Σ). + { eapply extends_wf_glob. exact ext. tea. } + revert H H0. + generalize Σ at 1 3 5 6. intros Σ''. + induction Σ'' => //. cbn. + intros hin wfg. depelim wfg. + f_equal. + 2:{ eapply IHΣ'' => //. destruct hin. exists (x ++ [(kn, d)]). rewrite -app_assoc /= //. } + unfold on_snd. cbn. f_equal. + eapply wellformed_trans_decl_extends => //. cbn. + eapply extends_wf_global_decl. 3:tea. + eapply extends_wf_glob; tea. eapply extends_prefix_extends; tea. + 2:{ eapply extends_wf_glob; tea. } + destruct hin. exists (x ++ [(kn, d)]). rewrite -app_assoc /= //. + cbn. eapply extends_prefix_extends; tea. +Qed. + +Lemma trans_env_eq {efl : EEnvFlags} (Σ : GlobalContextMap.t) : + wf_glob Σ -> trans_env Σ = trans_env' Σ.(GlobalContextMap.global_decls) Σ.(GlobalContextMap.wf). +Proof. + intros wf. + unfold trans_env. + destruct Σ; cbn. cbn in wf. + induction global_decls in map, repr, wf0, wf |- * => //. + cbn. f_equal. + destruct a as [kn d]; unfold on_snd; cbn. f_equal. symmetry. + eapply wellformed_trans_decl_extends => //. cbn. now depelim wf. cbn. + eapply extends_prefix_extends; tea. now exists [(kn, d)]. cbn. + set (Σg' := GlobalContextMap.make global_decls (fresh_globals_cons_inv wf0)). + erewrite <- (IHglobal_decls (GlobalContextMap.map Σg') (GlobalContextMap.repr Σg')). + 2:now depelim wf. + set (Σg := {| GlobalContextMap.global_decls := _ :: _ |}). + symmetry. eapply (trans_env_extends' (Σ := Σg') (Σ' := Σg)) => //. + cbn. now exists [a]. +Qed. + +Lemma trans_env_expanded {efl : EEnvFlags} {Σ : GlobalContextMap.t} : + wf_glob Σ -> expanded_global_env Σ -> expanded_global_env (trans_env Σ). +Proof. + unfold expanded_global_env; move=> wfg. + rewrite trans_env_eq //. + destruct Σ as [Σ map repr wf]. cbn in *. + clear map repr. + induction 1; cbn; constructor; auto. + cbn in IHexpanded_global_declarations. + unshelve eapply IHexpanded_global_declarations. now depelim wfg. cbn. + set (Σ' := GlobalContextMap.make _ _). + rewrite -(trans_env_eq Σ'). cbn. now depelim wfg. + eapply (trans_expanded_decl_irrel (Σ := Σ')). now depelim wfg. + now unshelve eapply (trans_expanded_decl (Σ:=Σ')). +Qed. + +Lemma trans_wellformed {efl : EEnvFlags} {Σ : GlobalContextMap.t} n t : + has_tBox -> has_tRel -> + wf_glob Σ -> EWellformed.wellformed Σ n t -> EWellformed.wellformed Σ n (trans Σ t). +Proof. + intros wfΣ hbox hrel. + induction t in n |- * using EInduction.term_forall_list_ind => //. + all:try solve [cbn; rtoProp; intuition auto; solve_all]. + all:apply trust_cofix. + (*- + cbn -[lookup_constructor]. intros. destruct cstr_as_blocks; rtoProp; repeat split; eauto. 2:solve_all. + 2: now destruct args; inv H0. len. eauto. + - cbn -[GlobalContextMap.inductive_isprop_and_pars lookup_inductive]. move/and3P => [] hasc /andP[]hs ht hbrs. + destruct GlobalContextMap.inductive_isprop_and_pars as [[[|] _]|] => /= //. + destruct l as [|[br n'] [|l']] eqn:eql; simpl. + all:rewrite ?hasc ?hs /= ?andb_true_r. + rewrite IHt //. + depelim X. cbn in hbrs. + rewrite andb_true_r in hbrs. + specialize (i _ hbrs). + eapply wellformed_substl => //. solve_all. eapply All_repeat => //. + now rewrite repeat_length. + cbn in hbrs; rtoProp; solve_all. depelim X; depelim X. solve_all. + do 2 depelim X. solve_all. + do 2 depelim X. solve_all. + rtoProp; solve_all. solve_all. + rtoProp; solve_all. solve_all. + - cbn -[GlobalContextMap.inductive_isprop_and_pars lookup_inductive]. move/andP => [] /andP[]hasc hs ht. + destruct GlobalContextMap.inductive_isprop_and_pars as [[[|] _]|] => /= //. + all:rewrite hasc hs /=; eauto. + - cbn. unfold wf_fix; rtoProp; intuition auto; solve_all. now eapply isLambda_trans. now len. + unfold test_def in *. len. eauto. + - cbn. unfold wf_fix; rtoProp; intuition auto; solve_all. now len. + unfold test_def in *. len. eauto. *) +Qed. + +Import EWellformed. + +Lemma trans_wellformed_irrel {efl : EEnvFlags} {Σ : GlobalContextMap.t} t : + wf_glob Σ -> + forall n, wellformed Σ n t -> wellformed (trans_env Σ) n t. +Proof. + intros wfΣ. induction t using EInduction.term_forall_list_ind; cbn => //. + all:try solve [intros; unfold wf_fix_gen in *; rtoProp; intuition eauto; solve_all]. + - rewrite lookup_env_trans //. + destruct lookup_env eqn:hl => // /=. + destruct g eqn:hg => /= //. subst g. + destruct (cst_body c) => //. + - rewrite lookup_env_trans //. + destruct lookup_env eqn:hl => // /=; intros; rtoProp; eauto. + destruct g eqn:hg => /= //; intros; rtoProp; eauto. + repeat split; eauto. destruct cstr_as_blocks; rtoProp; repeat split; len; eauto. 1: solve_all. + - rewrite lookup_env_trans //. + destruct lookup_env eqn:hl => // /=. + destruct g eqn:hg => /= //. subst g. + destruct nth_error => /= //. + intros; rtoProp; intuition auto; solve_all. + - rewrite lookup_env_trans //. + destruct lookup_env eqn:hl => // /=. + destruct g eqn:hg => /= //. + rewrite andb_false_r => //. + destruct nth_error => /= //. + all:intros; rtoProp; intuition auto; solve_all. +Qed. + +Lemma trans_wellformed_decl_irrel {efl : EEnvFlags} {Σ : GlobalContextMap.t} d : + wf_glob Σ -> + wf_global_decl Σ d -> wf_global_decl (trans_env Σ) d. +Proof. + intros wf; destruct d => /= //. + destruct (cst_body c) => /= //. + now eapply trans_wellformed_irrel. +Qed. + +Lemma trans_decl_wf {efl : EEnvFlags} {Σ : GlobalContextMap.t} : + has_tBox -> has_tRel -> wf_glob Σ -> + forall d, wf_global_decl Σ d -> wf_global_decl (trans_env Σ) (trans_decl Σ d). +Proof. + intros hasb hasr wf d. + intros hd. + eapply trans_wellformed_decl_irrel; tea. + move: hd. + destruct d => /= //. + destruct (cst_body c) => /= //. + now eapply trans_wellformed => //. +Qed. + +Lemma fresh_global_trans_env {Σ : GlobalContextMap.t} kn : + fresh_global kn Σ -> + fresh_global kn (trans_env Σ). +Proof. + destruct Σ as [Σ map repr wf]; cbn in *. + induction 1; cbn; constructor; auto. + now eapply Forall_map; cbn. +Qed. + +Lemma trans_env_wf {efl : EEnvFlags} {Σ : GlobalContextMap.t} : + has_tBox -> has_tRel -> + wf_glob Σ -> wf_glob (trans_env Σ). +Proof. + intros hasb hasrel. + intros wfg. rewrite trans_env_eq //. + destruct Σ as [Σ map repr wf]; cbn in *. + clear map repr. + induction wfg; cbn; constructor; auto. + - rewrite /= -(trans_env_eq (GlobalContextMap.make Σ (fresh_globals_cons_inv wf))) //. + eapply trans_decl_wf => //. + - rewrite /= -(trans_env_eq (GlobalContextMap.make Σ (fresh_globals_cons_inv wf))) //. + now eapply fresh_global_trans_env. +Qed. + +Definition trans_program (p : eprogram_env) := + (trans_env p.1, trans p.1 p.2). + +Definition trans_program_wf {efl} (p : eprogram_env) {hastbox : has_tBox} {hastrel : has_tRel} : + wf_eprogram_env efl p -> wf_eprogram efl (trans_program p). +Proof. + intros []; split. + now eapply trans_env_wf. + cbn. eapply trans_wellformed_irrel => //. now eapply trans_wellformed. +Qed. + +Definition trans_program_expanded {efl} (p : eprogram_env) : + wf_eprogram_env efl p -> + expanded_eprogram_env_cstrs p -> expanded_eprogram_cstrs (trans_program p). +Proof. + unfold expanded_eprogram_env_cstrs. + move=> [wfe wft] /andP[] etae etat. + apply/andP; split. + cbn. eapply expanded_global_env_isEtaExp_env, trans_env_expanded => //. + now eapply isEtaExp_env_expanded_global_env. + eapply expanded_isEtaExp. + eapply trans_expanded_irrel => //. + now apply trans_expanded, isEtaExp_expanded. +Qed. diff --git a/examples/metacoq_tour.v b/examples/metacoq_tour.v index 2f56ce470..3830aa3de 100644 --- a/examples/metacoq_tour.v +++ b/examples/metacoq_tour.v @@ -99,7 +99,7 @@ From MetaCoq.ErasurePlugin Require Import Erasure Loader. (** Running erasure live in Coq *) Definition test (p : Ast.Env.program) : string := - erase_and_print_template_program p. + erase_and_print_template_program default_erasure_config p. MetaCoq Quote Recursively Definition zero := 0. diff --git a/template-coq/src/ast_quoter.ml b/template-coq/src/ast_quoter.ml index eda51ba1d..bae47d447 100644 --- a/template-coq/src/ast_quoter.ml +++ b/template-coq/src/ast_quoter.ml @@ -258,16 +258,16 @@ struct let block = List.rev defs in Coq_tFix (block, b) - let mkCoFix (a,(ns,ts,ds)) = + let mkCoFix ((a,b),(ns,ts,ds)) = let mk_fun xs i = { dname = Array.get ns i ; dtype = Array.get ts i ; dbody = Array.get ds i ; - rarg = Datatypes.O } :: xs + rarg = Array.get a i } :: xs in let defs = List.fold_left mk_fun [] (seq 0 (Array.length ns)) in let block = List.rev defs in - Coq_tCoFix (block, a) + Coq_tCoFix (block, b) let mkCase (ind, npar, r) (univs, pars, pctx, pret) c brs = let info = { ci_ind = ind; ci_npar = npar; ci_relevance = r } in diff --git a/template-coq/src/constr_quoter.ml b/template-coq/src/constr_quoter.ml index 53e496b35..24c317e04 100644 --- a/template-coq/src/constr_quoter.ml +++ b/template-coq/src/constr_quoter.ml @@ -59,14 +59,14 @@ struct let mkConstruct (ind, i) u = constr_mkApp (tConstructor, [| ind ; i ; u |]) - let mkCoFix (a,(ns,ts,ds)) = + let mkCoFix ((a,b),(ns,ts,ds)) = let mk_fun xs i = constr_mkApp (tmkdef, [| Lazy.force tTerm ; Array.get ns i ; - Array.get ts i ; Array.get ds i ; Lazy.force tO |]) :: xs + Array.get ts i ; Array.get ds i ; Array.get a i |]) :: xs in let defs = List.fold_left mk_fun [] (seq 0 (Array.length ns)) in let block = to_coq_list (constr_mkAppl (tdef, [| tTerm |])) (List.rev defs) in - constr_mkApp (tCoFix, [| block ; a |]) + constr_mkApp (tCoFix, [| block ; b |]) let mkInd i u = constr_mkApp (tInd, [| i ; u |]) diff --git a/template-coq/src/quoter.ml b/template-coq/src/quoter.ml index bd7e5346f..8c1ba5692 100644 --- a/template-coq/src/quoter.ml +++ b/template-coq/src/quoter.ml @@ -82,7 +82,7 @@ sig t -> (quoted_aname array * t) list (* branches *) -> t val mkProj : quoted_proj -> t -> t val mkFix : (quoted_int array * quoted_int) * (quoted_aname array * t array * t array) -> t - val mkCoFix : quoted_int * (quoted_aname array * t array * t array) -> t + val mkCoFix : (quoted_int array * quoted_int) * (quoted_aname array * t array * t array) -> t val mkInt : quoted_int63 -> t val mkFloat : quoted_float64 -> t val mkArray : quoted_univ_level -> t array -> default:t -> ty:t -> t @@ -266,6 +266,12 @@ struct CArray.fold_left_map (fun acc t -> let (x, acc) = quote_term acc env sigma t in acc, x) acc ts in ts, acc + let cofixpoint_arities ts = + let cofix_arity t = + let ctx, _concl = Term.decompose_prod_assum t in + Context.Rel.nhyps ctx + in Array.map cofix_arity ts + let quote_term_remember (add_constant : KerName.t -> 'a -> 'a) (add_inductive : Names.inductive -> Declarations.mutual_inductive_body -> 'a -> 'a) = @@ -375,9 +381,11 @@ struct let a' = Array.map Q.quote_int a in let (b',decl'),acc = quote_recdecl acc env sigma b decl in (Q.mkFix ((a',b'),decl'), acc) - and quote_cofixpoint acc env sigma (a,decl) = + and quote_cofixpoint acc env sigma (a,(_, ts, _ as decl)) = + let arities = cofixpoint_arities ts in + let qarities = Array.map Q.quote_int arities in let (a',decl'),acc = quote_recdecl acc env sigma a decl in - (Q.mkCoFix (a',decl'), acc) + (Q.mkCoFix ((qarities,a'),decl'), acc) and quote_minductive_type (acc : 'a) env sigma (t : MutInd.t) mib = let uctx = get_abstract_inductive_universes mib.Declarations.mind_universes in let inst = UVars.UContext.instance uctx in diff --git a/test-suite/erasure_live_test.v b/test-suite/erasure_live_test.v index 57c9e17b3..c780c2996 100644 --- a/test-suite/erasure_live_test.v +++ b/test-suite/erasure_live_test.v @@ -18,7 +18,7 @@ Unset MetaCoq Debug. #[local] Existing Instance config.extraction_checker_flags. Definition test (p : Ast.Env.program) : string := - erase_and_print_template_program p. + erase_and_print_template_program default_erasure_config p. Definition testty (p : Ast.Env.program) : string := typed_erase_and_print_template_program p. @@ -51,7 +51,7 @@ Definition singlelim := ((fun (X : Set) (x : X) (e : x = x) => Definition erase {A} (a : A) : TemplateMonad unit := aq <- tmQuoteRec a ;; - s <- tmEval lazy (erase_and_print_template_program aq) ;; + s <- tmEval lazy (erase_and_print_template_program default_erasure_config aq) ;; tmMsg s. Definition erase_fast {A} (a : A) : TemplateMonad unit := @@ -80,6 +80,13 @@ Set MetaCoq Timing. Time MetaCoq Run (tmEval hnf vplus0123 >>= erase). Time MetaCoq Run (tmEval hnf vplus0123 >>= erase_fast). +(** Cofix *) +From Coq Require Import StreamMemo. + +MetaCoq Quote Recursively Definition memo := memo_make. + +Definition testmemo := Eval lazy in test memo. + (** Ackermann **) Fixpoint ack (n m:nat) {struct n} : nat := match n with @@ -350,7 +357,7 @@ Time Definition P_provedCopyx := Eval lazy in (test_fast cbv_provedCopyx). From MetaCoq.ErasurePlugin Require Import Loader. MetaCoq Erase provedCopyx. -MetaCoq Typed Erase provedCopyx. +MetaCoq Erase -time -typed -unsafe provedCopyx. (* From MetaCoq.Erasure.Typed Require Import CertifyingEta. MetaCoq Run (eta_expand_def @@ -360,6 +367,16 @@ provedCopy). *) Print P_provedCopyx. +From Coq Require Import Streams. + +CoFixpoint ones : Stream nat := Cons 1 ones. + +MetaCoq Erase ones. +MetaCoq Erase -unsafe ones. + +MetaCoq Erase -typed -time -unsafe (map S ones). + + (* 0.2s purely in the bytecode VM *) (*Time Definition P_provedCopyxvm' := Eval vm_compute in (test p_provedCopyx). *) (* Goal @@ -431,7 +448,7 @@ Proof. show_match. *) - +(* Debuggging From MetaCoq.Common Require Import Transform. From MetaCoq.Erasure.Typed Require Import ExtractionCorrectness. @@ -497,3 +514,4 @@ Import ETransform Optimize. MetaCoq Typed Erase provedCopyx. Eval lazy in testty cbv_provedCopyx. +*) \ No newline at end of file diff --git a/test-suite/erasure_test.v b/test-suite/erasure_test.v index 601963af6..ddea7abab 100644 --- a/test-suite/erasure_test.v +++ b/test-suite/erasure_test.v @@ -3,6 +3,8 @@ From MetaCoq.Template Require Import Loader. Set MetaCoq Timing. Local Open Scope string_scope. +MetaCoq Erase -help. + MetaCoq Erase nat. (* Environment is well-formed and Ind(Coq.Init.Datatypes.nat,0,[]) has type: ⧆ @@ -17,24 +19,26 @@ Environment is well-formed and Construct(Coq.Init.Datatypes.bool,0,0,[]) erases Construct(Coq.Init.Datatypes.bool,0,0) *) -MetaCoq Erase (exist _ 0 (eq_refl) : {x : nat | x = 0}). +MetaCoq Erase (exist (fun x => x = 0) 0 (eq_refl)). Definition test := (proj1_sig (exist (fun x => x = 0) 0 (eq_refl))). -MetaCoq Typed Erase test. +MetaCoq Erase -typed test. + +(** Cofix *) +From Coq Require Import StreamMemo. + +MetaCoq Quote Recursively Definition memo := memo_make. +MetaCoq Erase -typed -unsafe memo_make. -(* (* *) -(* Environment is well-formed and exist nat (fun x : nat => eq nat x O) O (eq_refl nat O):sig nat (fun x : nat => eq nat x O) erases to: *) -(* (fun f => f) (exist ∎ ∎ O ∎) *) -(* *) *) MetaCoq Erase (3 + 1). Universe i. -MetaCoq Fast Erase ((fun (X : Set) (x : X) => x) nat). +MetaCoq Erase ((fun (X : Set) (x : X) => x) nat). (** Check that optimization of singleton pattern-matchings work *) -MetaCoq Erase ((fun (X : Set) (x : X) (e : x = x) => +MetaCoq Erase ((fun (X : Set) (x : X) (e : x = x) => match e in eq _ x' return bool with | eq_refl => true end)).