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

Define a minimal subset of Module(Type) Declarations in template-coq #739

Draft
wants to merge 50 commits into
base: coq-8.16
Choose a base branch
from
Draft

Define a minimal subset of Module(Type) Declarations in template-coq #739

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
50 commits
Select commit Hold shift + click to select a range
511bcda
Update docker image version.
mattam82 Jun 14, 2022
f5e6231
Merge pull request #712 from MetaCoq/fix-8.14-ci
mattam82 Jun 14, 2022
1610c2d
Remove mutual inductiveness from whne def (#711)
arthur-adjedj Jun 14, 2022
74b9db2
Fill one admitted proof in Firstorder, remove dead code
mattam82 Jun 17, 2022
ffd483d
Merge pull request #715 from MetaCoq/clean-admits-8.14
mattam82 Jun 17, 2022
63906fb
Option to see constructors as block in EWcbvEval, needed for extracti…
yforster Jun 25, 2022
488ac9d
Replace all uses of `todo` and `Admitted` by axioms (#717)
yforster Jun 26, 2022
b6daf8c
Ensure constant constructors are declared in evaluation (#718)
mattam82 Jun 27, 2022
17b9492
Update readmes (#719)
mattam82 Jun 27, 2022
a247fa6
Fix README
mattam82 Jun 27, 2022
f8510b0
Remove warnings (#720)
yforster Jun 28, 2022
78b5df8
Constructor tactic example (#725)
mattam82 Jun 30, 2022
5b410f1
Constructors as blocks (#723)
mattam82 Jul 1, 2022
1f45662
[doc] Update erasure README.md for constructors-as-blocks
mattam82 Jul 1, 2022
7fde2fb
Update README.md and self_erasure file
mattam82 Jul 1, 2022
0102668
Update DOC.md and dependency graph
mattam82 Jul 1, 2022
d921719
Point to 8.14 branch in README
mattam82 Jul 1, 2022
58a3f1f
Revert "Option to see constructors as block in EWcbvEval, needed for …
mattam82 Jul 1, 2022
c97d948
Fixes after merge
mattam82 Jul 1, 2022
5d2f136
Merge pull request #727 from MetaCoq/merge-8.16-in-8.14
mattam82 Jul 1, 2022
c1dae3e
Release changes 8.14 (#732)
mattam82 Jul 5, 2022
c6426d9
add support for nix, like #705 but as branch in this repo (#706)
yforster Jul 6, 2022
314186f
Ewellformed islambda (#735)
mattam82 Jul 8, 2022
2320bd1
Constructors as blocks in the erasure pipeline (#736)
mattam82 Jul 12, 2022
836ec66
Use efficient maps in eta-expansion phase (#738)
mattam82 Jul 13, 2022
a9eb6f6
Write fixpoint attempt for on_module_decl (failed)
Jun 14, 2022
1e90089
Define on_module_decl
Jun 17, 2022
2845a4c
Define on_module_decl with induction principle
Jun 30, 2022
edd35a6
Proves on_global_env_impl
Jun 30, 2022
82f2002
Done EnvironmentTyping, needs cleanup
Jul 4, 2022
d3bba3b
Proves theorem in Typing.v
Jul 5, 2022
05aa36f
Defined check_wf_mod_body and friends
Jul 7, 2022
e490ade
Cleanup todos and prove wf and eta properties
Jul 13, 2022
8e2c7a4
Move to prop Qed'ed lemmas in type for cleaner extraction
mattam82 Jul 13, 2022
25646ca
Merge remote-tracking branch 'origin/coq-8.14' into global-env-tree
Jul 18, 2022
3a0f226
Finish proving EtaExpand.v and remove Prints
Jul 19, 2022
e1101bf
Extend print_env for module (type) declarations
Jul 20, 2022
be8b6e9
Before updating to coq-8.16
Dec 1, 2022
2ee944e
fixup this
Dec 1, 2022
a5fd721
Merge remote-tracking branch 'origin/coq-8.16' into global-env-tree
Dec 1, 2022
ab86056
Fix some proofs
Dec 3, 2022
53afd12
More fixes
Dec 3, 2022
e11975f
Don't know how to derive reflection??
Dec 3, 2022
8bbde7e
Refactor structure_field and prove ReflectAst.v
Dec 7, 2022
b4b4efa
Merge remote-tracking branch 'origin/coq-8.16' into global-env-tree
Dec 7, 2022
3887bfb
Merge remote-tracking branch 'origin/coq-8.16' into global-env-tree
Dec 23, 2022
e6974c5
Create no-module environment for pcuic
Dec 23, 2022
4c62462
TemplateToPcuic translation for modules
Jan 15, 2023
89b4c00
nested inductive types
Jan 17, 2023
58ce481
Define well-founded recursion on structure_field
Feb 2, 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
127 changes: 127 additions & 0 deletions .github/workflows/nix-action-default-macos.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,127 @@
jobs:
coq:
needs: []
runs-on: macos-latest
steps:
- name: Determine which commit to test
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
\ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\
\ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\
\ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
- name: Git checkout
uses: actions/checkout@v2
with:
fetch-depth: 0
ref: ${{ env.tested_commit }}
- name: Cachix install
uses: cachix/install-nix-action@v16
with:
nix_path: nixpkgs=channel:nixpkgs-unstable
- name: Cachix setup metacoq
uses: cachix/cachix-action@v10
with:
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
extraPullNames: coq, coq-community
name: metacoq
- id: stepCheck
name: Checking presence of CI target coq
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
\ bundle \"default\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
\ \"built:\" | sed \"s/.*/built/\")\n"
- if: steps.stepCheck.outputs.status == 'built'
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
--argstr job "coq"
equations:
needs: []
runs-on: macos-latest
steps:
- name: Determine which commit to test
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
\ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\
\ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\
\ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
- name: Git checkout
uses: actions/checkout@v2
with:
fetch-depth: 0
ref: ${{ env.tested_commit }}
- name: Cachix install
uses: cachix/install-nix-action@v16
with:
nix_path: nixpkgs=channel:nixpkgs-unstable
- name: Cachix setup metacoq
uses: cachix/cachix-action@v10
with:
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
extraPullNames: coq, coq-community
name: metacoq
- id: stepCheck
name: Checking presence of CI target equations
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
\ bundle \"default\" --argstr job \"equations\" \\\n --dry-run 2>&1 > /dev/null)\n\
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
\ \"built:\" | sed \"s/.*/built/\")\n"
- if: steps.stepCheck.outputs.status == 'built'
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
--argstr job "equations"
metacoq:
needs:
- equations
runs-on: macos-latest
steps:
- name: Determine which commit to test
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
\ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\
\ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\
\ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
- name: Git checkout
uses: actions/checkout@v2
with:
fetch-depth: 0
ref: ${{ env.tested_commit }}
- name: Cachix install
uses: cachix/install-nix-action@v16
with:
nix_path: nixpkgs=channel:nixpkgs-unstable
- name: Cachix setup metacoq
uses: cachix/cachix-action@v10
with:
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
extraPullNames: coq, coq-community
name: metacoq
- id: stepCheck
name: Checking presence of CI target metacoq
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
\ bundle \"default\" --argstr job \"metacoq\" \\\n --dry-run 2>&1 > /dev/null)\n\
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
\ \"built:\" | sed \"s/.*/built/\")\n"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: equations'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
--argstr job "equations"
- if: steps.stepCheck.outputs.status == 'built'
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
--argstr job "metacoq"
name: Nix CI for bundle default
'on':
pull_request:
paths:
- .github/workflows/**
pull_request_target:
types:
- opened
- synchronize
- reopened
push:
branches:
- master
127 changes: 127 additions & 0 deletions .github/workflows/nix-action-default-ubuntu.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,127 @@
jobs:
coq:
needs: []
runs-on: ubuntu-latest
steps:
- name: Determine which commit to test
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
\ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\
\ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\
\ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
- name: Git checkout
uses: actions/checkout@v2
with:
fetch-depth: 0
ref: ${{ env.tested_commit }}
- name: Cachix install
uses: cachix/install-nix-action@v16
with:
nix_path: nixpkgs=channel:nixpkgs-unstable
- name: Cachix setup metacoq
uses: cachix/cachix-action@v10
with:
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
extraPullNames: coq, coq-community
name: metacoq
- id: stepCheck
name: Checking presence of CI target coq
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
\ bundle \"default\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
\ \"built:\" | sed \"s/.*/built/\")\n"
- if: steps.stepCheck.outputs.status == 'built'
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
--argstr job "coq"
equations:
needs: []
runs-on: ubuntu-latest
steps:
- name: Determine which commit to test
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
\ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\
\ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\
\ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
- name: Git checkout
uses: actions/checkout@v2
with:
fetch-depth: 0
ref: ${{ env.tested_commit }}
- name: Cachix install
uses: cachix/install-nix-action@v16
with:
nix_path: nixpkgs=channel:nixpkgs-unstable
- name: Cachix setup metacoq
uses: cachix/cachix-action@v10
with:
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
extraPullNames: coq, coq-community
name: metacoq
- id: stepCheck
name: Checking presence of CI target equations
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
\ bundle \"default\" --argstr job \"equations\" \\\n --dry-run 2>&1 > /dev/null)\n\
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
\ \"built:\" | sed \"s/.*/built/\")\n"
- if: steps.stepCheck.outputs.status == 'built'
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
--argstr job "equations"
metacoq:
needs:
- equations
runs-on: ubuntu-latest
steps:
- name: Determine which commit to test
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
\ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\
\ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\
\ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
- name: Git checkout
uses: actions/checkout@v2
with:
fetch-depth: 0
ref: ${{ env.tested_commit }}
- name: Cachix install
uses: cachix/install-nix-action@v16
with:
nix_path: nixpkgs=channel:nixpkgs-unstable
- name: Cachix setup metacoq
uses: cachix/cachix-action@v10
with:
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
extraPullNames: coq, coq-community
name: metacoq
- id: stepCheck
name: Checking presence of CI target metacoq
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
\ bundle \"default\" --argstr job \"metacoq\" \\\n --dry-run 2>&1 > /dev/null)\n\
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
\ \"built:\" | sed \"s/.*/built/\")\n"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: equations'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
--argstr job "equations"
- if: steps.stepCheck.outputs.status == 'built'
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
--argstr job "metacoq"
name: Nix CI for bundle default
'on':
pull_request:
paths:
- .github/workflows/**
pull_request_target:
types:
- opened
- synchronize
- reopened
push:
branches:
- master
3 changes: 0 additions & 3 deletions erasure/theories/EConstructorsAsBlocks.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,6 @@ Section transform_blocks.
Hint Rewrite @map_InP_spec : transform_blocks.

Arguments eqb : simpl never.

Opaque transform_blocks_unfold_clause_1.
Opaque transform_blocks.
Opaque isEtaExp.
Expand Down Expand Up @@ -276,7 +275,6 @@ Section transform_blocks.
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 Nat.compare => //.
- f_equal. solve_all. move/andP: b => [] _ he. solve_all.
- rewrite csubst_mkApps.
Expand Down Expand Up @@ -357,7 +355,6 @@ Section transform_blocks.
rewrite forallb_rev forallb_skipn //.
now rewrite map_rev map_skipn.
Qed.

Lemma transform_blocks_fix_subst mfix : EGlobalEnv.fix_subst (map (map_def transform_blocks) mfix) = map transform_blocks (EGlobalEnv.fix_subst mfix).
Proof using Type.
unfold EGlobalEnv.fix_subst.
Expand Down
1 change: 0 additions & 1 deletion erasure/theories/EGenericMapEnv.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,6 @@ destruct (lookup_env Σ kn) eqn:hl.
- eapply lookup_env_gen_transform_env_Some in hl as [Σ' [ext wf' hl']] => /=.
rewrite hl'. f_equal.
eapply wellformed_gen_transform_decl_extends; eauto. auto.

- cbn. now eapply lookup_env_gen_transform_env_None in hl.
Qed.

Expand Down
3 changes: 1 addition & 2 deletions erasure/theories/EInlineProjections.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -378,7 +378,6 @@ Proof.
- eapply lookup_env_optimize_env_Some in hl as [Σ' [ext wf' hl']] => /=.
rewrite hl'. f_equal.
eapply wellformed_optimize_decl_extends; eauto. auto.

- cbn. now eapply lookup_env_optimize_env_None in hl.
Qed.

Expand Down Expand Up @@ -502,7 +501,7 @@ Proof.
eapply eval_wellformed in ev2; tea => //.
eapply eval_wellformed in ev1; tea => //.
econstructor; eauto.
rewrite -(optimize_csubst _ 1) //.
rewrite -(optimize_csubst _ 1) //.
apply IHev3. eapply wellformed_csubst => //.

- move/andP => [] clb0 clb1.
Expand Down
2 changes: 1 addition & 1 deletion erasure/theories/ELiftSubst.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,7 @@ Require Import PeanoNat.
Import Nat.

Lemma lift_rel_ge :
forall k n p, p <= n -> lift k p (tRel n) = tRel (k + n).
forall k n p, p <= n -> lift k p (tRel n) = tRel (k + n).
Proof.
intros; simpl in |- *.
now elim (leb_spec p n).
Expand Down
18 changes: 12 additions & 6 deletions erasure/theories/EWcbvEval.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -107,6 +107,8 @@ Section Wcbv.
Context {wfl : WcbvFlags}.
Context (Σ : global_declarations).
(* The local context is fixed: we are only doing weak reductions *)

Local Unset Elimination Schemes.

Local Unset Elimination Schemes.

Expand Down Expand Up @@ -217,7 +219,6 @@ Section Wcbv.
nth_error args (p.(proj_npars) + p.(proj_arg)) = Some a ->
eval a res ->
eval (tProj p discr) res

(** Proj *)
| eval_proj_block p cdecl discr args a res :
with_constructor_as_block = true ->
Expand Down Expand Up @@ -327,7 +328,6 @@ Defined.

Set Equations Transparent.
Section eval_rect.

Variables (wfl : WcbvFlags) (Σ : global_declarations) (P : forall x y, eval Σ x y → Type).

Equations All2_over {A B : Set} {P : A → B → Set} {l : list A} {l' : list B} :
Expand Down Expand Up @@ -697,6 +697,15 @@ Section Wcbv.
- repeat eexists; eauto.
- invs i. destruct args; invs H0. exists []. repeat econstructor.
Qed.

Lemma eval_Construct_inv ind c args e :
eval (tConstruct ind c args) e ->
∑ args', e = tConstruct ind c args' × All2 eval args args'.
Proof.
intros H. depind H.
- repeat eexists; eauto.
- invs i. destruct args; invs H0. exists []. repeat econstructor.
Qed.

Lemma eval_to_value e e' : eval e e' -> value e'.
Proof.
Expand Down Expand Up @@ -724,12 +733,10 @@ Section Wcbv.
+ rewrite -[tApp _ _](mkApps_app _ _ [a']).
eapply value_app. cbn; auto. econstructor; tea. cbn; len.
eapply All_app_inv; auto.

- econstructor 2; tea. now rewrite -(All2_length a).
clear -a iha. induction a. constructor.
destruct iha as [va' ih].
constructor. exact va'. now apply IHa.

- destruct (mkApps_elim f' [a']).
eapply value_mkApps_inv in IHev1 => //.
destruct IHev1 as [?|[]]; intuition subst.
Expand Down Expand Up @@ -1608,7 +1615,6 @@ Definition mk_env_flags has_ax has_pars tfl has_blocks :=
has_cstr_params := has_pars;
term_switches := tfl ;
cstr_as_blocks := has_blocks |}.

Global Hint Rewrite andb_true_r andb_false_r : simplifications.
Global Hint Rewrite orb_false_r orb_true_r : simplifications.

Expand Down Expand Up @@ -2017,7 +2023,7 @@ Proof.
eapply (eval_mkApps_Construct_inv _ _ _ [] _ hblock) in x as [? []]; auto. subst f''. depelim a1.
f_equal.
eapply eval_deterministic_all; tea.
eapply All2_impl; tea; cbn; eauto. now intros x y [].
eapply All2_impl; tea; cbn; eauto. now intros x y [].
Qed.

Lemma eval_construct_size {fl : WcbvFlags} [Σ kn c args e] :
Expand Down
1 change: 0 additions & 1 deletion erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,6 @@ Proof.
eapply qpres in hfix. depelim hfix. depelim i0. eapply nth_error_all in a; tea. now rewrite Nat.add_0_r in a.
assumption.
Qed.

#[export] Instance Qsubst_Qcofixs {etfl : ETermFlags} Q : Qpres Q -> Qcofix Q -> Qsubst Q -> Qcofixs Q.
Proof.
move=> qpres qfix; rewrite /Qsubst /Qfixs.
Expand Down
Loading