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

Unsafe and ewcbvevalnamed #1064

Merged
merged 2 commits into from
Mar 6, 2024
Merged

Unsafe and ewcbvevalnamed #1064

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c8946aa
WIP improving ewcbvevalnamed, needs to consider cofixes
mattam82 Mar 1, 2024
e8e5ede
Split unsafe passes, update EWcbvEvalNamed to be more parametric on f…
mattam82 Mar 6, 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
4 changes: 2 additions & 2 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ ifeq '$(METACOQ_CONFIG)' 'local'
export OCAMLPATH
endif

.PHONY: printconf all utils template-coq pcuic erasure install uninstall html clean mrproper .merlin test-suite translations quotation
.PHONY: printconf all utils template-coq pcuic erasure install uninstall html clean mrproper safechecker-plugin .merlin test-suite translations quotation

printconf:
ifeq '$(METACOQ_CONFIG)' 'local'
Expand All @@ -26,7 +26,7 @@ else
endif
endif

install: all
install: all
$(MAKE) -C utils install
$(MAKE) -C common install
$(MAKE) -C template-coq install
Expand Down
4 changes: 2 additions & 2 deletions erasure-plugin/src/g_metacoq_erasure.mlg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,12 +59,12 @@ let default_config =

let make_erasure_config config =
let open Erasure0 in
{ enable_unsafe = config.unsafe;
{ enable_unsafe = if config.unsafe then all_unsafe_passes else no_unsafe_passes ;
enable_typed_erasure = config.typed;
enable_fast_remove_params = config.fast;
dearging_config = default_dearging_config;
inductives_mapping = [];
inlining = Kernames.KernameSet.empty }
inlined_constants = Kernames.KernameSet.empty }

let time_opt config str fn arg =
if config.time then
Expand Down
98 changes: 73 additions & 25 deletions erasure-plugin/theories/Erasure.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,37 +30,65 @@ Import EWcbvEval.

Local Obligation Tactic := program_simpl.

Record unsafe_passes :=
{ fix_to_lazy : bool;
reorder_constructors : bool;
inlining : bool;
unboxing : bool;
betared : bool }.

Record erasure_configuration := {
enable_unsafe : bool;
enable_unsafe : unsafe_passes;
enable_typed_erasure : bool;
enable_fast_remove_params : bool;
dearging_config : dearging_config;
inductives_mapping : EReorderCstrs.inductives_mapping;
inlining : KernameSet.t
inlined_constants : KernameSet.t
}.

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 make_unsafe_passes b :=
{| fix_to_lazy := b;
reorder_constructors := b;
inlining := b;
unboxing := b;
betared := b |}.

Definition no_unsafe_passes := make_unsafe_passes false.
Definition all_unsafe_passes := make_unsafe_passes true.

(* This runs the cofix -> fix/lazy translation as well as inlining and
beta-redex simplification, which are not verified. It does not change
representation by reordering constructors or unboxing. *)

Definition default_unsafe_passes :=
{| fix_to_lazy := true;
reorder_constructors := false;
inlining := true;
unboxing := false;
betared := true |}.

Definition default_erasure_config :=
{| enable_unsafe := true;
{| enable_unsafe := default_unsafe_passes;
dearging_config := default_dearging_config;
enable_typed_erasure := true;
enable_fast_remove_params := true;
inductives_mapping := [];
inlining := KernameSet.empty |}.
inlined_constants := KernameSet.empty |}.

(* This runs only the verified phases without the typed erasure and "fast" remove params *)
Definition safe_erasure_config :=
{| enable_unsafe := false;
{| enable_unsafe := no_unsafe_passes;
enable_typed_erasure := false;
enable_fast_remove_params := false;
dearging_config := default_dearging_config;
inductives_mapping := [];
inlining := KernameSet.empty |}.
inlined_constants := KernameSet.empty |}.

Axiom assume_welltyped_template_program_expansion :
forall p (wtp : ∥ wt_template_program_env p ∥),
Expand Down Expand Up @@ -96,22 +124,40 @@ Definition final_wcbv_flags := {|
with_constructor_as_block := true |}.

Program Definition optional_unsafe_transforms econf :=
let passes := econf.(enable_unsafe) in
let efl := EConstructorsAsBlocks.switch_cstr_as_blocks
(EInlineProjections.disable_projections_env_flag (ERemoveParams.switch_no_params EWellformed.all_env_flags)) in
ETransform.optional_self_transform econf.(enable_unsafe)
ETransform.optional_self_transform passes.(fix_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 *)
coinductive_to_inductive_transformation efl
(has_app := eq_refl) (has_box := eq_refl) (has_rel := eq_refl) (has_pars := eq_refl) (has_cstrblocks := eq_refl) ▷
reorder_cstrs_transformation efl final_wcbv_flags econf.(inductives_mapping) ▷
rebuild_wf_env_transform (efl := efl) false false ▷
unbox_transformation efl final_wcbv_flags ▷
inline_transformation efl final_wcbv_flags econf.(inlining) ▷
forget_inlining_info_transformation efl final_wcbv_flags ▷
(* Heuristically do it twice for more beta-normal terms *)
betared_transformation efl final_wcbv_flags ▷
betared_transformation efl final_wcbv_flags).
(has_app := eq_refl) (has_box := eq_refl) (has_rel := eq_refl) (has_pars := eq_refl) (has_cstrblocks := eq_refl)) ▷
ETransform.optional_self_transform passes.(reorder_constructors)
(reorder_cstrs_transformation efl final_wcbv_flags econf.(inductives_mapping)) ▷
ETransform.optional_self_transform passes.(unboxing)
(rebuild_wf_env_transform (efl := efl) false false ▷
unbox_transformation efl final_wcbv_flags) ▷
ETransform.optional_self_transform passes.(inlining)
(inline_transformation efl final_wcbv_flags econf.(inlined_constants) ▷
forget_inlining_info_transformation efl final_wcbv_flags) ▷
(* Heuristically do it twice for more beta-normal terms *)
ETransform.optional_self_transform passes.(betared)
(betared_transformation efl final_wcbv_flags ▷
betared_transformation efl final_wcbv_flags).

Next Obligation.
destruct (enable_unsafe econf) as [[] [] [] [] []]; cbn in * => //; intuition auto.
Qed.
Next Obligation.
destruct (enable_unsafe econf) as [[] [] [] [] []]; cbn in * => //; intuition auto.
Qed.
Next Obligation.
destruct (enable_unsafe econf) as [[] [] [] [] []]; cbn in * => //; intuition auto.
Qed.
Next Obligation.
destruct (enable_unsafe econf) as [[] [] [] [] []]; cbn in * => //; intuition auto.
Qed.

Program Definition verified_lambdabox_pipeline {guard : abstract_guard_impl}
(efl := EWellformed.all_env_flags)
Expand Down Expand Up @@ -266,7 +312,7 @@ Qed.

Next Obligation.
unfold optional_unsafe_transforms. cbn.
destruct enable_unsafe => //.
destruct enable_unsafe as [[] ? ? ? ?]=> //.
Qed.

Local Obligation Tactic := intros; eauto.
Expand Down Expand Up @@ -365,7 +411,9 @@ Next Obligation.
cbn in H. split; cbn; intuition eauto.
Qed.
Next Obligation.
cbn in H. unfold optional_unsafe_transforms. destruct enable_unsafe => //.
cbn in H. unfold optional_unsafe_transforms.
cbn.
destruct enable_unsafe as [[] ? ? ? ?]=> //.
Qed.
Next Obligation.
cbn in H. split; cbn; intuition eauto.
Expand Down Expand Up @@ -409,8 +457,8 @@ Program Definition run_erase_program {guard : abstract_guard_impl} econf :=
else run (erasure_pipeline ▷ (optional_unsafe_transforms econf)).
Next Obligation.
Proof.
unfold optional_unsafe_transforms.
destruct enable_unsafe => //.
unfold optional_unsafe_transforms; cbn.
destruct enable_unsafe as [[] ? ? ? ?]=> //.
Qed.

Program Definition erase_and_print_template_program econf (p : Ast.Env.program) : string :=
Expand All @@ -425,23 +473,23 @@ Next Obligation.
Qed.

Definition erasure_fast_config :=
{| enable_unsafe := false;
{| enable_unsafe := no_unsafe_passes;
dearging_config := default_dearging_config;
enable_typed_erasure := false;
enable_fast_remove_params := true;
inductives_mapping := [];
inlining := KernameSet.empty |}.
inlined_constants := KernameSet.empty |}.

Program Definition erase_fast_and_print_template_program (p : Ast.Env.program) : string :=
erase_and_print_template_program erasure_fast_config p.

Definition typed_erasure_config :=
{| enable_unsafe := false;
{| enable_unsafe := no_unsafe_passes;
dearging_config := default_dearging_config;
enable_typed_erasure := true;
enable_fast_remove_params := true;
inductives_mapping := [];
inlining := KernameSet.empty |}.
inlined_constants := KernameSet.empty |}.

(* Parameterized by a configuration for dearging, allowing to, e.g., override masks. *)
Program Definition typed_erase_and_print_template_program (p : Ast.Env.program)
Expand Down
Loading
Loading