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.

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

PCUIC PHOAS #573

Open
wants to merge 147 commits into
base: coq-8.14
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
147 commits
Select commit Hold shift + click to select a range
dc339ff
Adapt to removal of first argument of PrivatePolymorphic in Coq #14727.
herbelin Oct 22, 2021
ea3719f
Simplification of PrivatePolymorphism solves the coq/coq#14903 issue.
herbelin Oct 22, 2021
75127a6
Fix reify/quote of predicate and branches binding name contexts (wron…
mattam82 Nov 25, 2021
129475b
Adapt to coq/coq#15294 (comparison is no longer extracted to int)
Lysxia Dec 11, 2021
f309b9e
Merge pull request #621 from Lysxia/overlay-15294
TheoWinterhalter Dec 14, 2021
cfa9984
adapt to #14137
Alizter Jan 4, 2022
d601c2f
adapt to coq/coq#15446
olaure01 Jan 7, 2022
35df3d3
Merge pull request #624 from Alizter/setoid-rewrite-type
ppedrot Jan 7, 2022
717d48c
Merge pull request #628 from olaure01/signatureT
mattam82 Jan 10, 2022
bf8375e
Adapt w.r.t. coq/coq#15442.
ppedrot Jan 10, 2022
edf5061
Merge pull request #630 from ppedrot/deprecate-program-naming-mode
ppedrot Jan 11, 2022
1368aec
Missing adaptation to coq/coq#15442.
ppedrot Jan 12, 2022
a44a2fd
Merge pull request #631 from ppedrot/deprecate-program-naming-mode-mi…
ppedrot Jan 12, 2022
06457c0
Merge branch 'coq-8.14'
mattam82 Jan 25, 2022
bdaec46
Fixes after merge
mattam82 Jan 25, 2022
b19ebf8
Try to make the safechecker run again
mattam82 Jan 27, 2022
cc26139
Make master compile some examples: universes are broken right now
mattam82 Jan 27, 2022
fc3a268
Finish updating master with 8.14 changes
mattam82 Jan 27, 2022
7bebcd6
Fix Extraction files requiring Ascii
mattam82 Jan 27, 2022
8f40d07
Fix build.yml to require coq.dev
mattam82 Jan 28, 2022
be3af83
Upate opam dependencies
mattam82 Jan 28, 2022
176add0
Call Coq's CList.filter_map
mattam82 Jan 28, 2022
eb780f4
Move filter_map to tm_util
mattam82 Jan 28, 2022
0ee5bc8
Merge pull request #635 from MetaCoq/master-merge-8.14
mattam82 Jan 28, 2022
a149fee
pass on pcuic syntax
MevenBertrand Jan 5, 2022
51b62f5
cleaning up the removal of ContextRelations
MevenBertrand Jan 7, 2022
21a0144
document Nicolas' refactoring
MevenBertrand Jan 11, 2022
430252b
finished pass on pcuic
MevenBertrand Jan 26, 2022
09d855e
pass on safechecker
MevenBertrand Jan 26, 2022
f495006
first batch of remarks by Théo
MevenBertrand Jan 27, 2022
393a5b7
qualifying import to pass opam build
MevenBertrand Jan 27, 2022
1413c65
removing useless notation
MevenBertrand Jan 28, 2022
cd3bc92
Merge pull request #625 from MetaCoq/filesdoc
MevenBertrand Jan 28, 2022
51ac3cb
adapt to coq/coq#15220
gares Nov 29, 2021
ec96734
Merge pull request #613 from gares/dynlink-w-findlib
ppedrot Feb 3, 2022
c69085d
Fix compilation of safechecker with findlib
gares Feb 7, 2022
7ffff46
export OCAMLPATH
gares Feb 8, 2022
4026e06
Avoid warning keeping template-coq/build around
gares Feb 8, 2022
0b893e2
META: safechecker depends on template
gares Feb 10, 2022
1e24c40
Merge pull request #640 from gares/fix-findlib
mattam82 Feb 10, 2022
96f5dee
Change the univ representation so that global universes are really re…
mattam82 Jan 27, 2022
6b9e43b
New global_env structure in template-coq/reification
mattam82 Feb 2, 2022
cdb0762
Adapt PCUIC to new global_env structure
mattam82 Feb 8, 2022
e406d57
Adapt Template -> PCUIC Correctness proof
mattam82 Feb 8, 2022
42d6c2b
Fix udecl definition (was not including set in global levels)
mattam82 Feb 9, 2022
56fc551
Adapted safe_checker to new global env
mattam82 Feb 9, 2022
caa1b86
Adapt erasure to new global env
mattam82 Feb 9, 2022
b182531
Adapted erasure to new environment representation
mattam82 Feb 9, 2022
ccc5499
Fix quoting
mattam82 Feb 9, 2022
bff9cc4
Disable quoting of the universe graph for now
mattam82 Feb 9, 2022
95387c7
Fix warnings in extraction, using `Stdlib` instead of `Pervasives`
mattam82 Feb 10, 2022
9209af0
Factorize Extraction files
mattam82 Feb 10, 2022
1ad0f14
Fix quoting of universe contexts/safecheck to use restricted graph
mattam82 Feb 10, 2022
4a153c0
Adapt test-suite to change in global_env
mattam82 Feb 10, 2022
9e99741
Remove deprecation and other warnings
mattam82 Feb 10, 2022
085c7c6
Try to fix weird type equality issue in ocaml 4.07.1
mattam82 Feb 10, 2022
07776b1
Minor fixes
mattam82 Feb 10, 2022
578f1c1
Guard .merlin target: only applies when extracted files have been pro…
mattam82 Feb 10, 2022
ff3336b
Fix configure script call
mattam82 Feb 11, 2022
8ee8f75
Fix template-coq Makefile requirerments for install target
mattam82 Feb 11, 2022
98bf5c2
Fix opam/findlib installation
mattam82 Feb 11, 2022
afc6d36
Fix safechecker
mattam82 Feb 11, 2022
ebb430d
Fix local builds of plugins
mattam82 Feb 11, 2022
5113744
Make the local build not interfer with the global one
mattam82 Feb 11, 2022
ed72148
No more -I ../template_coq needed
mattam82 Feb 11, 2022
f64d8ca
Make META a phony rule so it is properly regenerated for each plugni
mattam82 Feb 11, 2022
fb0a5a8
Remove _build directory, no longer needed
mattam82 Feb 11, 2022
15cc7dc
Fix the test-suite makefiles
mattam82 Feb 11, 2022
e9f2ee2
Fix examples Makefile
mattam82 Feb 11, 2022
2598ee4
No longer mkdir build
mattam82 Feb 11, 2022
2c38bc1
Fix translations
mattam82 Feb 11, 2022
b5e4809
Merge pull request #634 from MetaCoq/master-global-universes
mattam82 Feb 11, 2022
b077764
Update copyright notice in README
mattam82 Feb 11, 2022
8531d62
Merge pull request #599 from herbelin/master+adapt-coq-pr14727-rework…
ppedrot Feb 14, 2022
42fb30a
Add stdlib-shims dependency to compile with ocaml < 4.07
mattam82 Feb 16, 2022
5962851
Merge pull request #647 from MetaCoq/stdlib-shims-dep
mattam82 Feb 16, 2022
af51a04
Update the META files for the dependency on stdlib-shims as well
mattam82 Feb 16, 2022
b638bfe
Merge branch 'coq-8.14' into master-merge-8.14
mattam82 Feb 17, 2022
321f34d
Fix a typo
mattam82 Feb 16, 2022
f09c0db
Revert extraction of nat to int (not compatible with certicoq)
mattam82 Feb 17, 2022
804d9ee
Merge pull request #648 from MetaCoq/master-merge-8.14
mattam82 Feb 17, 2022
234a829
Adapt to coq/coq#15754 (#655)
proux01 Mar 16, 2022
f0a3a56
Adapt w.r.t. coq/coq#15837.
ppedrot Mar 21, 2022
9793d93
Merge pull request #668 from ppedrot/reduce-universe-footprint
ppedrot Mar 22, 2022
4845d2a
Adapt w.r.t. coq/coq#15856.
ppedrot Mar 25, 2022
72667aa
Merge pull request #670 from ppedrot/universes-rm-univ-of-sort
ppedrot Mar 28, 2022
1cf25d9
Adapt w.r.t. coq/coq#15863.
ppedrot Mar 29, 2022
90dbbcb
Merge pull request #673 from ppedrot/universes-rm-small-levels
ppedrot Mar 29, 2022
0914586
Adapt w.r.t. coq/coq#15871.
ppedrot Mar 30, 2022
d012c81
Merge pull request #674 from ppedrot/univ-cleanup-api
ppedrot Mar 31, 2022
374086a
Merge pull request #649 from MetaCoq/extraction-no-ascii
mattam82 Feb 17, 2022
7478e56
Merge pull request #652 from MetaCoq/remove-primitives
mattam82 Feb 18, 2022
38c93a4
Merge pull request #653 from MetaCoq/self-erasure
mattam82 Feb 18, 2022
e30240f
Merge pull request #654 from MetaCoq/parameter-stripping
mattam82 Mar 1, 2022
fa458d8
Parameter stripping integration (#656)
mattam82 Mar 2, 2022
8af7ac2
Generic EnvMap (#658)
mattam82 Mar 5, 2022
83b4f94
Clean erasure (#661)
mattam82 Mar 8, 2022
7bdd877
Abstract env for safetyping (#662)
tabareau Mar 15, 2022
9a18b38
Merge pull request #663 from MetaCoq/bytestring
mattam82 Mar 16, 2022
a75750c
Merge pull request #664 from kyoDralliam/fix-case-insensitive
mattam82 Mar 16, 2022
20f630e
Merge pull request #665 from kyoDralliam/fix-file-ambiguity
mattam82 Mar 17, 2022
9c66c7b
Merge pull request #667 from MetaCoq/hnf_ctor_types
mattam82 Mar 20, 2022
272c438
Add a relevance field to constant bodies (#666)
mattam82 Mar 21, 2022
4058bc6
Implement a `infer_univs` mode for mkInductive (#612)
mattam82 Mar 24, 2022
9169639
Abstract env check (#671)
tabareau Mar 28, 2022
00a137a
Eta expand fixpoints (#669)
mattam82 Mar 29, 2022
73203c8
Merge pull request #675 from MetaCoq/typing-wf-forall-decls
tabareau Mar 31, 2022
c2453fe
Reorganise Universes.v and have check_univs only alter level [exprs] …
yannl35133 Apr 1, 2022
7790324
Thread eta expansion everywhere (#676)
mattam82 Apr 1, 2022
0fcb5ba
Update .gitignore
mattam82 Apr 25, 2022
65f8e13
Missing links in PCUIC’s Readme
MevenBertrand Apr 4, 2022
a5b3a05
Erasure optimizations preserves wellformedness and expansion (#677)
mattam82 Apr 5, 2022
b63ce43
Merge pull request #678 from MetaCoq/eenvmap-in-optimize-prop-discr
mattam82 Apr 6, 2022
2266b98
Strict eta expanded constructors (#680)
mattam82 Apr 10, 2022
5d66647
Refinements of EWellformed and EWcbvEvalEtaInd (#681)
mattam82 Apr 13, 2022
1d6c6d3
Inline projections optimization (#683)
mattam82 Apr 13, 2022
1495a1e
Make safechecker compute (#682)
tabareau Apr 14, 2022
9244ffb
Merge pull request #684 from MetaCoq/erasure-cleanups
mattam82 Apr 16, 2022
3bbfbd9
Slightly faster erasure of global environments (#685)
mattam82 Apr 17, 2022
ef9a873
Merge pull request #686 from MetaCoq/hott-tests
mattam82 Apr 21, 2022
8d8f3bc
Use explicit records for projection names and declarations, add irrel…
mattam82 Apr 21, 2022
881d6df
Remove accidentaly commited file
mattam82 Apr 21, 2022
9392e04
Merge pull request #690 from MetaCoq/safeconversion-admit-free
mattam82 Apr 22, 2022
0daa598
add constraints between monomorphic sorts to udecl (#687)
kyoDralliam Apr 25, 2022
acd3b3c
Merge pull request #692 from MetaCoq/writing_cleanups
mattam82 Apr 25, 2022
bb38e92
Merge pull request #691 from MetaCoq/cleanup-all-erasure
mattam82 Apr 25, 2022
76ee01d
Fixes after merge of 8.14 changes
mattam82 Apr 25, 2022
cbac790
Merge pull request #694 from MetaCoq/master-8.14-merge
mattam82 Apr 25, 2022
9474d7c
Adapt w.r.t. coq/coq#15943.
ppedrot Apr 27, 2022
42dba86
Merge pull request #698 from ppedrot/cache-projection-relevance
ppedrot Apr 28, 2022
c104fb3
Merge coq-8.14 branch in master
mattam82 Jun 8, 2022
c35be57
Fixes after merge of 8.14 branch
mattam82 Jun 9, 2022
8b835e7
Fix build.yml
mattam82 Jun 9, 2022
7d16657
Fix `quick` target by setting universe checking in translation_utils.v
mattam82 Jun 9, 2022
dc7848b
Fix generous_packed
mattam82 Jun 9, 2022
ea94a7f
Update master status badge
mattam82 Jun 15, 2022
d98e388
Fix CI instructions
mattam82 Jun 15, 2022
290e3b2
Fix CI instructions
mattam82 Jun 15, 2022
4461fe7
Fill one admitted proof in Firstorder, remove dead code
mattam82 Jun 17, 2022
4c8b06d
Merge pull request #713 from MetaCoq/clean-admits
mattam82 Jun 17, 2022
daf3e47
Replace all uses of `todo` and `Admitted` by axioms (#717)
yforster Jun 26, 2022
29126ac
Ensure constant constructors are declared in evaluation (#718)
mattam82 Jun 27, 2022
ea2d0be
Update readmes (#719)
mattam82 Jun 27, 2022
8e541ec
Fix README
mattam82 Jun 27, 2022
f6d8e17
Remove warnings (#720)
yforster Jun 28, 2022
5a9c2aa
Add a PCUICPHOAS file implementing a PHOAS variant of the syntax
mattam82 Jul 12, 2021
f03ae80
Allow giving only one binder name and retriviing it in the phoas repr…
mattam82 Jun 29, 2022
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
Binary file removed dependency-graph/depgraph-2022-01-07.png
Binary file not shown.
2,479 changes: 0 additions & 2,479 deletions dependency-graph/depgraph-2022-01-07.svg

This file was deleted.

Large diffs are not rendered by default.

Binary file added dependency-graph/depgraph-2022-01-26.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
2,605 changes: 2,605 additions & 0 deletions dependency-graph/depgraph-2022-01-26.svg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
1 change: 1 addition & 0 deletions erasure/theories/ErasureCorrectness.v
Original file line number Diff line number Diff line change
@@ -19,6 +19,7 @@ From MetaCoq.PCUIC Require Import PCUICTyping PCUICGlobalEnv PCUICAst
PCUICOnFreeVars PCUICWellScopedCumulativity PCUICValidity
PCUICContexts PCUICEquality PCUICSpine
PCUICInductives.
Require Import PCUICTactics.

Require Import Equations.Prop.DepElim.
Require Import ssreflect.
2 changes: 1 addition & 1 deletion pcuic/theories/Bidirectional/BDUnique.v
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
From Coq Require Import Bool List Arith Lia.
From MetaCoq.Template Require Import config utils monad_utils.
From MetaCoq.PCUIC Require Import PCUICGlobalEnv PCUICAst PCUICAstUtils PCUICInduction PCUICLiftSubst PCUICTyping PCUICEquality PCUICArities PCUICInversion PCUICReduction PCUICSubstitution PCUICConversion PCUICCumulativity PCUICGeneration PCUICWfUniverses PCUICContextConversion PCUICContextSubst PCUICContexts PCUICSpine PCUICWfUniverses PCUICUnivSubst PCUICClosed PCUICInductives PCUICValidity PCUICInductiveInversion PCUICConfluence PCUICWellScopedCumulativity PCUICSR PCUICOnFreeVars PCUICClosedTyp.
From MetaCoq.PCUIC Require Import PCUICGlobalEnv PCUICAst PCUICAstUtils PCUICTactics PCUICInduction PCUICLiftSubst PCUICTyping PCUICEquality PCUICArities PCUICInversion PCUICReduction PCUICSubstitution PCUICConversion PCUICCumulativity PCUICGeneration PCUICWfUniverses PCUICContextConversion PCUICContextSubst PCUICContexts PCUICSpine PCUICWfUniverses PCUICUnivSubst PCUICClosed PCUICInductives PCUICValidity PCUICInductiveInversion PCUICConfluence PCUICWellScopedCumulativity PCUICSR PCUICOnFreeVars PCUICClosedTyp.
From MetaCoq.PCUIC Require Import BDEnvironmentTyping BDTyping BDToPCUIC BDFromPCUIC.

Require Import ssreflect ssrbool.
14 changes: 8 additions & 6 deletions pcuic/theories/README.md
Original file line number Diff line number Diff line change
@@ -8,8 +8,8 @@
| [PCUICOnOne] | Lemmas for the OnOne relation
| [PCUICPrimitive] | Definitions and lemmas for primitives datatypes
| [PCUICTactics] | Tactics used throughout the library
| [Extraction] | Setup to extract the development to OCaml
| [PCUICLoader] |
| [Extraction] | Setup to extract the development
| [PCUICLoader] | For plugins



@@ -281,8 +281,10 @@
| [TemplateToPCUICCorrectness] | Type preservation of the aformentioned translation |
| [PCUICToTemplate] | Translation from PCUIC syntax to Template-Coq syntax |
| [PCUICToTemplateCorrectness] | Type preservation of the aformentioned translation |
| [TemplateToPCUICWcbvEval] | The weak-head call-by-value evaluation strategy is preserved by the translation between Template Coq and PCUIC

[TemplateToPCUIC]: TemplateToPCUIC.v
[TemplateToPCUICCorrectness]: TemplateToPCUICCorrectness.v
[PCUICToTemplate]: PCUICToTemplate.v
[PCUICToTemplateCorrectness]: PCUICToTemplateCorrectness.v
[TemplateToPCUIC]: ./TemplateToPCUIC.v
[TemplateToPCUICCorrectness]: ./TemplateToPCUICCorrectness.v
[PCUICToTemplate]: ./PCUICToTemplate.v
[PCUICToTemplateCorrectness]: ./PCUICToTemplateCorrectness.v
[TemplateToPCUICWcbvEval]: ./TemplateToPCUICWcbvEval.v
2 changes: 1 addition & 1 deletion pcuic/theories/Typing/PCUICWeakeningTyp.v
Original file line number Diff line number Diff line change
@@ -56,7 +56,7 @@ Proof.
+ apply wf_local_app; auto.
apply All_local_env_fold in IH. apply IH.
+ apply weakening_renaming.
- intros [s Hs]; exists s. red.
- intros [s Hs]; exists s.
rewrite -/(lift_context #|Γ''| 0 Δ).
rewrite Nat.add_0_r !lift_rename.
eapply (Hs xpredT).
102 changes: 0 additions & 102 deletions pcuic/theories/todo.md

This file was deleted.

6 changes: 3 additions & 3 deletions safechecker/theories/PCUICSafeChecker.v
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
(* Distributed under the terms of the MIT license. *)
From MetaCoq.Template Require Import config utils uGraph.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTactics
PCUICLiftSubst PCUICUnivSubst PCUICSigmaCalculus PCUICTyping PCUICNormal PCUICSR
PCUICWeakeningEnvConv PCUICWeakeningEnvTyp
PCUICGeneration PCUICReflect PCUICEquality PCUICInversion PCUICValidity
@@ -1780,15 +1780,15 @@ Section CheckEnv.
eapply forallbP_cond; eauto. clear wfcs.
simpl; intros c wfc.
pose proof (check_leqb_universe_spec' G (global_ext_uctx Σ)).
forward H. apply wf_ext_global_uctx_invariants; auto.
forward H. eapply wf_ext_global_uctx_invariants; eauto.
forward H. apply wfΣ.
eapply forallbP_cond; eauto. simpl. intros x wfx.
specialize (H wfG x ind_sort). simpl.
destruct check_leqb_universe eqn:eq; constructor.
now simpl in H.
intro. simpl in H.
pose proof (check_leqb_universe_complete G (global_ext_uctx Σ)).
forward H1. apply wf_ext_global_uctx_invariants. now sq.
forward H1. eapply wf_ext_global_uctx_invariants. now sq.
forward H1. apply wfΣ.
specialize (H1 wfG x ind_sort). simpl in H1.
forward H1.
14 changes: 7 additions & 7 deletions safechecker/theories/PCUICSafeConversion.v
Original file line number Diff line number Diff line change
@@ -9,7 +9,7 @@ From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils
PCUICOnFreeVars PCUICWellScopedCumulativity
PCUICWeakeningEnvConv PCUICWeakeningEnvTyp
PCUICWeakeningConv PCUICWeakeningTyp
PCUICClosed PCUICClosedTyp PCUICEqualityDec.
PCUICClosed PCUICClosedTyp PCUICEqualityDec PCUICConvCumInversion.
From MetaCoq.SafeChecker Require Import PCUICErrors PCUICSafeReduce.

Require Import Equations.Prop.DepElim.
@@ -1279,8 +1279,8 @@ Section Conversion.
intros. eapply (check_eqb_universe_spec' G (global_ext_uctx Σ)).
all: auto.
+ pose proof heΣ. sq. eapply wf_ext_global_uctx_invariants.
assumption.
+ pose proof heΣ. sq. eapply global_ext_uctx_consistent; assumption.
eassumption.
+ pose proof heΣ. sq. eapply global_ext_uctx_consistent; eassumption.
Qed.

Arguments LevelSet.mem : simpl never.
@@ -1297,11 +1297,11 @@ Section Conversion.
destruct heΣ.
destruct leq; cbn.
- eapply check_eqb_universe_complete; eauto.
+ now apply wf_ext_global_uctx_invariants.
+ now apply global_ext_uctx_consistent.
+ now eapply wf_ext_global_uctx_invariants.
+ now eapply global_ext_uctx_consistent.
- eapply check_leqb_universe_complete; eauto.
+ now apply wf_ext_global_uctx_invariants.
+ now apply global_ext_uctx_consistent.
+ now eapply wf_ext_global_uctx_invariants.
+ now eapply global_ext_uctx_consistent.
Qed.

Lemma get_level_make l :
8 changes: 4 additions & 4 deletions safechecker/theories/PCUICSafeRetyping.v
Original file line number Diff line number Diff line change
@@ -5,7 +5,7 @@ From Equations Require Import Equations.

From Coq Require Import Bool String List Program.
From MetaCoq.Template Require Import config monad_utils utils uGraph.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICArities PCUICInduction
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTactics PCUICArities PCUICInduction
PCUICLiftSubst PCUICUnivSubst PCUICTyping PCUICGlobalEnv
PCUICWeakeningEnvConv PCUICWeakeningEnvTyp
PCUICReduction
@@ -15,7 +15,7 @@ From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICArities PCUICInduc
PCUICGeneration PCUICInversion PCUICValidity PCUICInductives PCUICInductiveInversion PCUICReduction
PCUICSpine PCUICSR PCUICCumulativity PCUICConversion PCUICConfluence PCUICArities
PCUICContexts PCUICContextConversion PCUICContextConversionTyp PCUICOnFreeVars
PCUICWellScopedCumulativity PCUICSafeLemmata PCUICSN.
PCUICWellScopedCumulativity PCUICSafeLemmata PCUICSN PCUICConvCumInversion.

From MetaCoq.PCUIC Require Import BDTyping BDToPCUIC BDFromPCUIC BDUnique.

@@ -201,7 +201,7 @@ Qed.
cbn in *.
sq.
destruct wf as [[? i]].
eapply infering_sort_infering in i ; eauto.
eapply infering_sort_infering in i; eauto.
Qed.

Program Definition infer_as_prod Γ T
@@ -549,7 +549,7 @@ Qed.
1: now eapply red_terms_equality_terms.
1: symmetry.
1: now eapply red_terms_equality_terms.
eapply alt_into_equality_terms ; tea.
eapply PCUICConvCumInversion.alt_into_equality_terms ; tea.
* fvs.
* eapply infering_ind_typing, validity, isType_open in X ; auto.
rewrite on_free_vars_mkApps in X.
18 changes: 9 additions & 9 deletions safechecker/theories/PCUICTypeChecker.v
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
(* Distributed under the terms of the MIT license. *)
From MetaCoq.Template Require Import config utils uGraph.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTactics
PCUICLiftSubst PCUICUnivSubst PCUICTyping PCUICNormal PCUICSR
PCUICGeneration PCUICReflect PCUICEquality PCUICInversion PCUICValidity
PCUICWeakeningEnvConv PCUICWeakeningEnvTyp
@@ -856,7 +856,7 @@ Section Typecheck.
rewrite /subst_instance_level.
split.
* destruct l.
-- now apply wf_ext_global_uctx_invariants.
-- now eapply wf_ext_global_uctx_invariants.
-- cbn in Hcs'.
forward Hcs'.
do 2 eexists.
@@ -867,9 +867,9 @@ Section Typecheck.
-- apply LevelSetFact.mem_2.
pattern (nth n u Level.lzero).
apply Forall_nth_def ; tea.
now apply LevelSetFact.mem_1, wf_ext_global_uctx_invariants.
now eapply LevelSetFact.mem_1, wf_ext_global_uctx_invariants.
* destruct l'.
-- now apply wf_ext_global_uctx_invariants.
-- now eapply wf_ext_global_uctx_invariants.
-- forward Hcs''.
do 2 eexists.
constructor.
@@ -879,7 +879,7 @@ Section Typecheck.
-- apply LevelSetFact.mem_2.
pattern (nth n u Level.lzero).
apply Forall_nth_def ; tea.
now apply LevelSetFact.mem_1, wf_ext_global_uctx_invariants.
now eapply LevelSetFact.mem_1, wf_ext_global_uctx_invariants.
Qed.

Equations check_consistent_instance uctx (wfg : ∥ global_uctx_invariants (global_ext_uctx (Σ.1, uctx)) ∥)
@@ -913,7 +913,7 @@ Section Typecheck.
destruct wfg as [wfg].
suff: (@check_constraints cf G (subst_instance_cstrs u cstrs)) by congruence.
eapply check_constraints_complete.
- now apply wf_ext_global_uctx_invariants.
- now eapply wf_ext_global_uctx_invariants.
- now apply wf_ext_consistent.
- auto.
- eapply nor.
@@ -1016,8 +1016,8 @@ Section Typecheck.
rewrite nor_check_univs in check.
specialize (check val sat).
now rewrite check.
* now apply wf_ext_global_uctx_invariants.
* now apply global_ext_uctx_consistent.
* now eapply wf_ext_global_uctx_invariants.
* now eapply global_ext_uctx_consistent.
Qed.
Next Obligation.
sq.
@@ -1972,7 +1972,7 @@ Section Typecheck.
etransitivity.
1: now symmetry ; eapply All2_firstn, red_terms_equality_terms.

eapply alt_into_equality_terms ; tea.
eapply PCUICConvCumInversion.alt_into_equality_terms ; tea.
- fvs.
- eapply Forall_forallb.
2: intros ? H ; apply H.
2 changes: 1 addition & 1 deletion safechecker/theories/PCUICWfEnv.v
Original file line number Diff line number Diff line change
@@ -43,7 +43,7 @@ Section GraphSpec.
intros HH.
refine (check_constraints_spec G (global_ext_uctx Σ) _ _ HG _ HH).
sq; now eapply wf_ext_global_uctx_invariants.
sq; now apply global_ext_uctx_consistent.
sq; now eapply global_ext_uctx_consistent.
Qed.

Lemma is_graph_of_uctx_levels (l : Level.t) :
32 changes: 18 additions & 14 deletions safechecker/theories/README.md
Original file line number Diff line number Diff line change
@@ -1,25 +1,29 @@
# Safe Checker

Implementation of a fuel-free, correct type checker for PCUIC.
Implementation of a fuel-free, correct and complete type checker for PCUIC.
It is suited for extraction which would remove the termination and
correctness proofs.


| File | Description |
|-----------------------|------------------------------------------------------|
| [PCUICSafeReduce] | Weak-head reduction machine |
| [PCUICSafeConversion] | Conversion checker |
| [PCUICSafeChecker] | Type inference and type checking |
| [PCUICSafeRetyping] | Fast type inference, assuming well-typedness |
| [SafeTemplateChecker] | |
| [Loader] | |
| [Extraction] | |
| [PCUICWfReduction] | Well-foundedness of the order used by the reduction machine
| [PCUICErrors] | Output types used by the different machines
| [PCUICSafeReduce] | Weak-head reduction machine
| [PCUICSafeConversion] | Conversion checker
| [PCUICWfEnv] | Helper properties for global environments and universes
| [PCUICTypeChecker] | Type inference and type checking
| [PCUICSafeRetyping] | Fast type inference, assuming well-typedness
| [PCUICSafeChecker] | Checking of global environments
| [SafeTemplateChecker] | Checking of Template Coq programs
| [Extraction] | Setup to extract the development
| [Loader] | For plugins

[PCUICSafeReduce]: PCUICSafeReduce.v
[PCUICSafeConversion]: PCUICSafeConversion.v
[PCUICSafeChecker]: PCUICSafeChecker.v
[PCUICTypeChecker]: PCUICSafeChecker.v
[PCUICSafeRetyping]: PCUICSafeRetyping.v
[PCUICSafeChecker]: PCUICSafeChecker.v
[SafeTemplateChecker]: SafeTemplateChecker.v
[Loader]: Loader.v
[Extraction]: Extraction.v

All of these are proven correct but not yet complete.
They are suited for extraction which would remove the termination and
correctness proofs.
[Extraction]: Extraction.v