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

Primitive flags #1033

Merged
merged 2 commits into from
Dec 22, 2023
Merged

Primitive flags #1033

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
c1414bf
Make EPrimitive universe polymorphic so it can apply to term types in…
mattam82 Dec 21, 2023
f526608
Add an EPrimitiveFlags to control the presence of ints/floats/arrays
mattam82 Dec 21, 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
2 changes: 2 additions & 0 deletions erasure/theories/EConstructorsAsBlocks.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,7 @@ Section transform_blocks.

End Def.

#[universes(polymorphic)]
Hint Rewrite @map_primIn_spec @map_InP_spec : transform_blocks.

Arguments eqb : simpl never.
Expand Down Expand Up @@ -428,6 +429,7 @@ Section transform_blocks.

End transform_blocks.

#[universes(polymorphic)]
Global Hint Rewrite @map_primIn_spec @map_InP_spec : transform_blocks.

Definition transform_blocks_constant_decl Σ cb :=
Expand Down
1 change: 1 addition & 0 deletions erasure/theories/EEtaExpanded.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,7 @@ Section isEtaExp.

End isEtaExp.

#[universes(polymorphic)]
Global Hint Rewrite @test_primIn_spec @forallb_InP_spec : isEtaExp.
Tactic Notation "simp_eta" "in" hyp(H) := simp isEtaExp in H; rewrite -?isEtaExp_equation_1 in H.
Ltac simp_eta := simp isEtaExp; rewrite -?isEtaExp_equation_1.
Expand Down
4 changes: 2 additions & 2 deletions erasure/theories/EEtaExpandedFix.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -334,7 +334,7 @@ Section isEtaExp.
Qed.

Hint Rewrite @forallb_InP_spec : isEtaExp.
Hint Rewrite @test_primIn_spec : isEtaExp.
#[universes(polymorphic)] Hint Rewrite @test_primIn_spec : isEtaExp.

Lemma isEtaExp_mkApps_nonnil Γ f v :
~~ isApp f -> v <> [] ->
Expand Down Expand Up @@ -773,7 +773,7 @@ Section isEtaExp.

End isEtaExp.
Global Hint Rewrite @forallb_InP_spec : isEtaExp.
Global Hint Rewrite @test_primIn_spec : isEtaExp.
#[universes(polymorphic)] Global Hint Rewrite @test_primIn_spec : isEtaExp.

Tactic Notation "simp_eta" "in" hyp(H) := simp isEtaExp in H; rewrite -?isEtaExp_equation_1 in H.
Ltac simp_eta := simp isEtaExp; rewrite -?isEtaExp_equation_1.
Expand Down
4 changes: 3 additions & 1 deletion erasure/theories/EImplementBox.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,7 @@ Section implement_box.

End Def.

#[universes(polymorphic)]
Hint Rewrite @map_primIn_spec @map_InP_spec : implement_box.

Arguments eqb : simpl never.
Expand Down Expand Up @@ -265,6 +266,7 @@ Section implement_box.

End implement_box.

#[universes(polymorphic)]
Global Hint Rewrite @map_primIn_spec @map_InP_spec : implement_box.

Definition implement_box_constant_decl cb :=
Expand Down Expand Up @@ -670,7 +672,7 @@ Proof.
rewrite lookup_constructor_implement_box; eauto.
eapply All2_All2_Set.
solve_all. now destruct b.
- intros H; depelim H; simp implement_box; repeat constructor.
- intros wf H; depelim H; simp implement_box; repeat constructor.
destruct a0. eapply All2_over_undep in a. eapply All2_All2_Set, All2_map.
cbn -[implement_box]. solve_all. now destruct H. now destruct a0.
- intros. destruct t; try solve [constructor; cbn in H, H0 |- *; try congruence].
Expand Down
9 changes: 5 additions & 4 deletions erasure/theories/EInlineProjections.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -166,7 +166,7 @@ Section optimize.
- len. rtoProp; solve_all. solve_all.
now eapply isLambda_optimize. solve_all.
- len. rtoProp; repeat solve_all.
- rewrite test_prim_map. solve_all.
- rewrite test_prim_map. rtoProp; intuition eauto; solve_all.
Qed.

Lemma optimize_csubst {a k b} n :
Expand Down Expand Up @@ -716,11 +716,12 @@ Proof.
rewrite optimize_mkApps !isConstructApp_mkApps !isPrimApp_mkApps.
destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //.
destruct v => /= //.
- depelim X; repeat constructor.
- intros; rtoProp; intuition eauto.
depelim X; repeat constructor.
eapply All2_over_undep in a.
eapply All2_Set_All2 in ev. eapply All2_All2_Set. primProp.
subst a0 a'; cbn in *. depelim H; cbn in *. intuition auto; solve_all.
primProp; depelim H; intuition eauto.
subst a0 a'; cbn in *. depelim H0; cbn in *. intuition auto; solve_all.
primProp; depelim H0; intuition eauto.
- destruct t => //.
all:constructor; eauto.
cbn [atom optimize] in i |- *.
Expand Down
Loading