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

Injectivity of inductive types revisited #3253

Merged
merged 60 commits into from
May 1, 2024
Merged

Injectivity of inductive types revisited #3253

Show file tree
Hide file tree
Changes from 40 commits
Commits
Show all changes
60 commits
Select commit Hold shift + click to select a range
ead4864
restrict injectivity of inductives based on a simpler but more restri…
nikswamy Mar 26, 2024
2c50dcd
a refinement of the injectivity constraint
nikswamy Mar 27, 2024
92f768a
retain equations on indices even if parameters are in a universe too …
nikswamy Mar 27, 2024
ac07d58
snap
nikswamy Apr 15, 2024
fb34777
restrict the universe of type-function parameters when enabling injec…
nikswamy Apr 16, 2024
773cdc3
snap
nikswamy Apr 16, 2024
df6fb0d
need to explicitly destruct Refl
nikswamy Apr 16, 2024
13cb2d3
another explicit Refl destruction
nikswamy Apr 16, 2024
3a4b518
snap
nikswamy Apr 16, 2024
007ff20
Merge remote-tracking branch 'origin/master' into nik_restrict_inject…
nikswamy Apr 17, 2024
2c6b4db
Merge branch 'master' into nik_restrict_injectivity
nikswamy Apr 17, 2024
1057ff2
Merge branch 'master' into nik_restrict_injectivity
nikswamy Apr 18, 2024
87e5d17
trying to simplify the handling of Tm_name
nikswamy Apr 18, 2024
bbdff51
merge master in
nikswamy Apr 18, 2024
84d1251
simplify a counterexample; add it to the test suite
nikswamy Apr 18, 2024
ce14d27
merge
nikswamy Apr 18, 2024
5c011d5
current check is not strict enough; can still break it using injectiv…
nikswamy Apr 19, 2024
35380d3
refactoring encoding of inductive type and datacon to prepare for a r…
nikswamy Apr 19, 2024
448857d
restrict injectivity for data constructor type parameters
nikswamy Apr 19, 2024
ab79318
a temporary compat in FStar.ModifiesGen
nikswamy Apr 19, 2024
e376ccc
for data constructors on types not injective on their params, add an …
nikswamy Apr 19, 2024
db285db
remove compat options in ModifiesGen
nikswamy Apr 19, 2024
2aec69e
Merge remote-tracking branch 'origin/master' into nik_restrict_inject…
nikswamy Apr 19, 2024
9d39962
revise the statement of inversion of data constructor typing to not r…
nikswamy Apr 20, 2024
0d6bb6a
Merge remote-tracking branch 'origin/master' into nik_restrict_inject…
nikswamy Apr 20, 2024
ec1ed9d
remove projector function altogether if it is not injective
nikswamy Apr 20, 2024
d1508c8
try, never injective on params
nikswamy Apr 20, 2024
8ac4ae5
disable compat:injectivity
nikswamy Apr 21, 2024
ae4521b
Merge remote-tracking branch 'origin/master' into nik_restrict_inject…
nikswamy Apr 22, 2024
0ac8a71
remove duplicated guards
nikswamy Apr 22, 2024
ba8cb90
revert disabling compat options
nikswamy Apr 22, 2024
95499af
Merge remote-tracking branch 'origin/master' into nik_restrict_inject…
nikswamy Apr 22, 2024
f97222b
revert disabling injectivity globally
nikswamy Apr 22, 2024
c117073
undo ulib changes
nikswamy Apr 22, 2024
2a31bd0
reverting Bug3186; cleaning up BugBoxInjectivity
nikswamy Apr 22, 2024
07b70f7
update a comment
nikswamy Apr 22, 2024
89b83ab
Don't generate spurious declarations that rely on a projector of a ty…
nikswamy Apr 22, 2024
34089dd
snap
nikswamy Apr 23, 2024
8715862
Merge remote-tracking branch 'origin/master' into nik_restrict_inject…
nikswamy Apr 23, 2024
46b6855
Merge branch 'nik_restrict_injectivity_wip' into nik_restrict_injecti…
nikswamy Apr 23, 2024
ab0ee5f
merging master in
nikswamy Apr 24, 2024
630aadd
try revise pretyping axiom
nikswamy Apr 24, 2024
600963d
temporary admits
nikswamy Apr 24, 2024
68ad9ab
weaken pretype axiom for non-injective types
nikswamy Apr 25, 2024
9979879
Revert "temporary admits"
nikswamy Apr 25, 2024
9885844
refactor to provide an environment to eq_tm and NBETerm.eq_t
nikswamy Apr 26, 2024
a3ca82c
revise equality of data constructors to return unknown if the type pa…
nikswamy Apr 26, 2024
03d1b17
adding an injective_type_params field to Sig_inductive and Sig_datacon
nikswamy Apr 27, 2024
42bba1e
compute injective_type_params flag in phase2 only
nikswamy Apr 27, 2024
e023a9c
merging master in
nikswamy Apr 27, 2024
bcbff7c
snap
nikswamy Apr 27, 2024
d950b26
tweak a test; we seemt to run out of stack a bit sooner on unembeddin…
nikswamy Apr 27, 2024
35f89bf
Merge remote-tracking branch 'origin/master' into nik_restrict_inject…
nikswamy Apr 28, 2024
18b55b2
rlimit bump & retry on Lib.Vec.Lemmas
nikswamy Apr 28, 2024
ed0e430
snap
nikswamy Apr 29, 2024
596cc5c
another test
nikswamy Apr 29, 2024
0d8be16
Merge remote-tracking branch 'origin/master' into nik_restrict_inject…
nikswamy Apr 30, 2024
b85bee9
eq_tm and eq_t disregard non-injective type parameters in equality te…
nikswamy Apr 30, 2024
3b730a9
merge master
nikswamy May 1, 2024
3849844
Fix test
mtzguido May 1, 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,466 changes: 2,277 additions & 2,189 deletions ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml
View file
Open in desktop

Large diffs are not rendered by default.

113 changes: 95 additions & 18 deletions ocaml/fstar-lib/generated/FStar_SMTEncoding_Term.ml
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Loading
Loading