Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Transform extends #1012

Closed
wants to merge 4 commits into from
Closed

Transform extends #1012

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
669ed18
separate extends and extends_eprogram
tabareau Nov 14, 2023
935e858
prove missing lemmas of the pipeline
tabareau Nov 14, 2023
df22914
remove generated files
tabareau Nov 14, 2023
a1880e5
Update .gitignore
tabareau Nov 14, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -296,6 +296,8 @@ test-suite/plugin-demo/Makefile.plugin


template-coq/Makefile.plugin-e
template-coq/_PluginProject
template-coq/_TemplateCoqProject
template-coq/Makefile.template-e
template-coq/src/g_template_coq.ml
pcuic/Makefile.plugin-e
Expand Down Expand Up @@ -379,6 +381,7 @@ template-pcuic/Makefile.local
template-pcuic/_CoqProject
template-pcuic/Makefile.templatepcuic
template-pcuic/Makefile.templatepcuic.conf
template-pcuic/metacoq-config

quotation/Makefile.local
quotation/_CoqProject
Expand Down
80 changes: 70 additions & 10 deletions erasure-plugin/theories/ETransform.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -347,9 +347,16 @@ Qed.

#[global]
Instance guarded_to_unguarded_fix_extends {fl : EWcbvEval.WcbvFlags} {wcon : EWcbvEval.with_constructor_as_block = false} {efl : EEnvFlags} (wguard : with_guarded_fix) :
TransformExt.t (guarded_to_unguarded_fix (wcon:=wcon) wguard) (fun p p' => extends p.1 p'.1) (fun p p' => extends p.1 p'.1).
Proof.
red. intros p p' pr pr' ?. now rewrite /transform /=.
Qed.

#[global]
Instance guarded_to_unguarded_fix_extends' {fl : EWcbvEval.WcbvFlags} {wcon : EWcbvEval.with_constructor_as_block = false} {efl : EEnvFlags} (wguard : with_guarded_fix) :
TransformExt.t (guarded_to_unguarded_fix (wcon:=wcon) wguard) extends_eprogram_env extends_eprogram_env.
Proof.
red. intros p p' pr pr' [ext eq]. now rewrite /transform /=.
red. intros p p' pr pr' [? ?]. now rewrite /transform /=.
Qed.

Definition rebuild_wf_env {efl} (p : eprogram) (hwf : wf_eprogram efl p): eprogram_env :=
Expand All @@ -371,9 +378,16 @@ Qed.

#[global]
Instance rebuild_wf_env_extends {fl : EWcbvEval.WcbvFlags} {efl : EEnvFlags} with_exp :
TransformExt.t (rebuild_wf_env_transform with_exp) (fun p p' => extends p.1 p'.1) (fun p p' => extends p.1 p'.1).
Proof.
red. intros p p' pr pr' ext. red. now rewrite /transform /=.
Qed.

#[global]
Instance rebuild_wf_env_extends' {fl : EWcbvEval.WcbvFlags} {efl : EEnvFlags} with_exp :
TransformExt.t (rebuild_wf_env_transform with_exp) extends_eprogram extends_eprogram_env.
Proof.
red. intros p p' pr pr' [ext eq]. now rewrite /transform /=.
red. intros p p' pr pr' [? ?]. now rewrite /transform /=.
Qed.

Program Definition remove_params_optimization {fl : EWcbvEval.WcbvFlags} {wcon : EWcbvEval.with_constructor_as_block = false}
Expand Down Expand Up @@ -404,12 +418,21 @@ Qed.

#[global]
Instance remove_params_extends {fl : EWcbvEval.WcbvFlags} {wcon : EWcbvEval.with_constructor_as_block = false}
(efl := all_env_flags):
TransformExt.t (remove_params_optimization (wcon:=wcon)) (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 /= /strip_program.
red. cbn -[strip_env strip]. eapply strip_extends_env => //. apply pr. apply pr'.
Qed.

#[global]
Instance remove_params_extends' {fl : EWcbvEval.WcbvFlags} {wcon : EWcbvEval.with_constructor_as_block = false}
(efl := all_env_flags):
TransformExt.t (remove_params_optimization (wcon:=wcon)) extends_eprogram_env extends_eprogram.
Proof.
red. intros p p' pr pr' [ext eq]. rewrite /transform /= /strip_program. rewrite eq.
red. cbn -[strip_env strip]. split. eapply strip_extends_env => //. apply pr. apply pr'.
eapply strip_extends => //. apply pr'. rewrite -eq. apply pr.
red. cbn -[strip_env strip]. split. eapply strip_extends_env => //. apply pr. apply pr'.
cbn -[strip_env strip]. eapply strip_extends => //. apply pr'. rewrite -eq. apply pr.
Qed.

Program Definition remove_params_fast_optimization {fl : EWcbvEval.WcbvFlags} {wcon : EWcbvEval.with_constructor_as_block = false}
Expand Down Expand Up @@ -444,11 +467,21 @@ Qed.

#[global]
Instance remove_params_fast_extends {fl : EWcbvEval.WcbvFlags} {wcon : EWcbvEval.with_constructor_as_block = false}
(efl := all_env_flags):
TransformExt.t (remove_params_fast_optimization (wcon:=wcon)) (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 /=.
rewrite -!ERemoveParams.Fast.strip_env_fast.
eapply strip_extends_env => //. apply pr. apply pr'.
Qed.

#[global]
Instance remove_params_fast_extends' {fl : EWcbvEval.WcbvFlags} {wcon : EWcbvEval.with_constructor_as_block = false}
(efl := all_env_flags):
TransformExt.t (remove_params_fast_optimization (wcon:=wcon)) extends_eprogram_env extends_eprogram.
Proof.
red. intros p p' pr pr' [ext eq]. rewrite /transform /=. rewrite eq.
rewrite -!ERemoveParams.Fast.strip_fast -!ERemoveParams.Fast.strip_env_fast.
rewrite -!ERemoveParams.Fast.strip_env_fast -!ERemoveParams.Fast.strip_fast.
split => /=. eapply strip_extends_env => //. apply pr. apply pr'.
eapply strip_extends => //. apply pr'. rewrite -eq. apply pr.
Qed.
Expand Down Expand Up @@ -480,9 +513,17 @@ Qed.

#[global]
Instance remove_match_on_box_extends {fl : WcbvFlags} {wcon : with_constructor_as_block = false} {efl : EEnvFlags} {hastrel : has_tRel} {hastbox : has_tBox} :
TransformExt.t (remove_match_on_box_trans (wcon:=wcon) (hastrel := hastrel) (hastbox := hastbox)) (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 /= /remove_match_on_box_program.
eapply remove_match_on_box_extends_env => //. apply pr. apply pr'.
Qed.

#[global]
Instance remove_match_on_box_extends' {fl : WcbvFlags} {wcon : with_constructor_as_block = false} {efl : EEnvFlags} {hastrel : has_tRel} {hastbox : has_tBox} :
TransformExt.t (remove_match_on_box_trans (wcon:=wcon) (hastrel := hastrel) (hastbox := hastbox)) extends_eprogram_env extends_eprogram.
Proof.
red. intros p p' pr pr' [ext eq]. rewrite /transform /= /remove_match_on_box_program; split => /=.
red. intros p p' pr pr' [ext eq]. rewrite /transform /= /remove_match_on_box_program. split.
eapply remove_match_on_box_extends_env => //. apply pr. apply pr'.
rewrite -eq.
eapply wellformed_remove_match_on_box_extends; eauto. apply pr. apply pr'.
Expand Down Expand Up @@ -514,11 +555,19 @@ Qed.

#[global]
Instance inline_projections_optimization_extends {fl : WcbvFlags} {wcon : EWcbvEval.with_constructor_as_block = false} (efl := switch_no_params all_env_flags)
{hastrel : has_tRel} {hastbox : has_tBox} :
TransformExt.t (inline_projections_optimization (wcon:=wcon) (hastrel := hastrel) (hastbox := hastbox)) (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 /= /optimize_program /=.
eapply optimize_extends_env => //. apply pr. apply pr'.
Qed.

#[global]
Instance inline_projections_optimization_extends' {fl : WcbvFlags} {wcon : EWcbvEval.with_constructor_as_block = false} (efl := switch_no_params all_env_flags)
{hastrel : has_tRel} {hastbox : has_tBox} :
TransformExt.t (inline_projections_optimization (wcon:=wcon) (hastrel := hastrel) (hastbox := hastbox)) extends_eprogram_env extends_eprogram.
Proof.
red. intros p p' pr pr' [ext eq]. rewrite /transform /= /optimize_program /=.
split => /=.
red. intros p p' pr pr' [ext eq]. rewrite /transform /= /optimize_program /=. split.
eapply optimize_extends_env => //. apply pr. apply pr'.
rewrite -eq.
eapply wellformed_optimize_extends; eauto. apply pr. apply pr'.
Expand Down Expand Up @@ -553,13 +602,24 @@ 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))
(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 transform_blocks_env_extends => //. apply pr. apply pr'.
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))
extends_eprogram_env extends_eprogram.
Proof.
red. intros p p' pr pr' [ext eq]. rewrite /transform /=.
split => //. eapply transform_blocks_env_extends => //. apply pr. apply pr'.
red. intros p p' pr pr' [ext eq]. rewrite /transform /=. split.
eapply transform_blocks_env_extends => //. apply pr. apply pr'.
unfold transform_blocks_program => /=.
rewrite -eq.
eapply transform_blocks_extends; eauto. apply pr. apply pr'.
Qed.

7 changes: 7 additions & 0 deletions erasure-plugin/theories/Erasure.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -131,6 +131,13 @@ 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)
(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.
Proof.
unfold verified_lambdabox_pipeline. tc.
Expand Down
Loading
Loading