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

Jump to bottom

Fix the translation of cofix to fix #1070

Merged
merged 3 commits into from
Mar 28, 2024
Merged

Fix the translation of cofix to fix #1070

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
d704705
Fix the translation of cofix to fix to move the head constructors's l…
mattam82 Mar 21, 2024
f593f92
WIP correcting cofixpoint translation
mattam82 Mar 25, 2024
a3d9a14
Be more clever when forcing the body of a translated cofix
mattam82 Mar 25, 2024
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
54 changes: 44 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 @@ -696,9 +696,6 @@ Proof.
red. intros p p' pr pr' [? ?]. now rewrite /transform /=.
Qed.

Definition rebuild_wf_env {efl} (p : eprogram) (hwf : wf_eprogram efl p): eprogram_env :=
(GlobalContextMap.make p.1 (wf_glob_fresh p.1 (proj1 hwf)), p.2).

Definition preserves_expansion with_fix p :=
if with_fix then EEtaExpandedFix.expanded_eprogram p
else EEtaExpanded.expanded_eprogram_cstrs p.
Expand All @@ -707,6 +704,9 @@ Definition preserves_expansion_env with_fix p :=
if with_fix then EEtaExpandedFix.expanded_eprogram_env p
else EEtaExpanded.expanded_eprogram_env_cstrs p.

Definition rebuild_wf_env {efl} (p : eprogram) (hwf : wf_eprogram efl p): eprogram_env :=
(GlobalContextMap.make p.1 (wf_glob_fresh p.1 (proj1 hwf)), p.2).

Program Definition rebuild_wf_env_transform {fl : EWcbvEval.WcbvFlags} {efl} (with_exp with_fix : bool) :
Transform.t _ _ EAst.term EAst.term _ _ (eval_eprogram fl) (eval_eprogram_env fl) :=
{| name := "rebuilding environment lookup table";
Expand Down Expand Up @@ -736,6 +736,39 @@ Proof.
red. intros p p' pr pr' [? ?]. now rewrite /transform /=.
Qed.


Definition project_wf_env {efl} (p : eprogram_env) (hwf : wf_eprogram_env efl p): eprogram :=
(GlobalContextMap.global_decls p.1, p.2).

Program Definition project_wf_env_transform {fl : EWcbvEval.WcbvFlags} {efl} (with_exp with_fix : bool) :
Transform.t _ _ EAst.term EAst.term _ _ (eval_eprogram_env fl) (eval_eprogram fl) :=
{| name := "projecting environment declarations list";
pre p := wf_eprogram_env efl p /\ (with_exp -> preserves_expansion_env with_fix p);
transform p pre := project_wf_env p (proj1 pre);
post p := wf_eprogram efl p /\ (with_exp -> preserves_expansion with_fix p);
obseq p hp p' v v' := v = v' |}.
Next Obligation.
cbn. unfold preserves_expansion, preserves_expansion_env.
intros fl efl [] [] input [wf exp]; cbn; split => //.
Qed.
Next Obligation.
cbn. intros fl efl [] [] input v [] ev p'; exists v; split => //.
Qed.

#[global]
Instance project_wf_env_extends {fl : EWcbvEval.WcbvFlags} {efl : EEnvFlags} with_exp with_fix :
TransformExt.t (project_wf_env_transform with_exp with_fix) (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 project_wf_env_extends' {fl : EWcbvEval.WcbvFlags} {efl : EEnvFlags} with_exp with_fix :
TransformExt.t (project_wf_env_transform with_exp with_fix) extends_eprogram_env extends_eprogram.
Proof.
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}
(efl := all_env_flags):
Transform.t _ _ EAst.term EAst.term _ _ (eval_eprogram_env fl) (eval_eprogram fl) :=
Expand Down Expand Up @@ -975,12 +1008,12 @@ 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) :=
(eval_eprogram block_wcbv_flags) (eval_eprogram_env 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 |}.
pre p := wf_eprogram efl p ;
post p := wf_eprogram_env 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].
Expand All @@ -991,9 +1024,10 @@ Next Obligation.
eexists. split; [ | eauto].
econstructor.
cbn -[transform_blocks].
eapply ECoInductiveToInductive.trans_correct; cbn; eauto.
apply ECoInductiveToInductive.trust_cofix.
(* eapply ECoInductiveToInductive.trans_correct; cbn; eauto.
eapply wellformed_closed_env, wfe1.
Unshelve. all:eauto.
Unshelve. all:eauto. *)
Qed.

#[global]
Expand All @@ -1012,7 +1046,7 @@ 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.
extends_eprogram extends_eprogram_env.
Proof.
red. intros p p' pr pr' ext. rewrite /transform /=.
eapply ECoInductiveToInductive.trust_cofix.
Expand Down
7 changes: 3 additions & 4 deletions erasure-plugin/theories/Erasure.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -128,11 +128,10 @@ Program Definition optional_unsafe_transforms econf :=
let efl := EConstructorsAsBlocks.switch_cstr_as_blocks
(EInlineProjections.disable_projections_env_flag (ERemoveParams.switch_no_params EWellformed.all_env_flags)) in
ETransform.optional_self_transform passes.(cofix_to_lazy)
((* Rebuild the efficient lookup table *)
rebuild_wf_env_transform (efl := efl) false false ▷
(* Coinductives & cofixpoints are translated to inductive types and thunked fixpoints *)
((* Coinductives & cofixpoints are translated to inductive types and thunked fixpoints *)
coinductive_to_inductive_transformation efl
(has_app := eq_refl) (has_box := eq_refl) (has_rel := eq_refl) (has_pars := eq_refl) (has_cstrblocks := eq_refl)) ▷
(has_app := eq_refl) (has_box := eq_refl) (has_rel := eq_refl) (has_pars := eq_refl) (has_cstrblocks := eq_refl) ▷
project_wf_env_transform false false) ▷
ETransform.optional_self_transform passes.(reorder_constructors)
(reorder_cstrs_transformation efl final_wcbv_flags econf.(inductives_mapping)) ▷
ETransform.optional_self_transform passes.(unboxing)
Expand Down
Loading
Loading