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

Removing lex tuples, cf. #1916 #2218

Merged
merged 73 commits into from
Feb 9, 2021
Merged

Removing lex tuples, cf. #1916 #2218

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
73 commits
Select commit Hold shift + click to select a range
4040c48
make lex tuples for precedes
aseemr Dec 18, 2020
94750b3
parser changes to make lex tuples
aseemr Dec 18, 2020
c3064e9
axiom about lex tuples ordering
aseemr Dec 18, 2020
022073a
snap
aseemr Dec 18, 2020
33c70fe
encode_binders returns sorts encoding that is used in encoding subter…
aseemr Dec 18, 2020
429e2c2
snap
aseemr Dec 18, 2020
ff3745f
removing uses of lex
aseemr Dec 18, 2020
f010192
snap
aseemr Dec 18, 2020
2df95aa
trying out a precedes axiom for refinements
aseemr Dec 18, 2020
1d1fd84
removing the precedes axiom for every refinement type
aseemr Dec 19, 2020
b054283
weakening axiom for precedes
aseemr Dec 19, 2020
4a7d931
snap
aseemr Dec 19, 2020
6acd3c9
removing special casing for LexCons dataconstructor smt encoding
aseemr Dec 24, 2020
921a12f
removing smt encoding of lexcons
aseemr Dec 24, 2020
38964ce
removing lex ordering axiom from the encoding
aseemr Dec 24, 2020
6288099
nits
aseemr Dec 24, 2020
97281b3
changes in the parser AST to have a term list in decreases
aseemr Dec 24, 2020
60ef688
changes in the syntax to have a list of terms in the decreases cflag
aseemr Dec 24, 2020
c32baee
inline the lex ordering axiom for precedes when building the type env…
aseemr Dec 24, 2020
3df8677
propagating syntax changes for decreases to the typechecker
aseemr Dec 24, 2020
0cd2b73
nit
aseemr Dec 24, 2020
2883e04
change in the reflection API for decreases clauses
aseemr Dec 24, 2020
f6ac29f
changes in the ulib reflection library for decreases clause
aseemr Dec 24, 2020
6bd59e8
some cleanup
aseemr Dec 24, 2020
54ada4b
admitting a couple of ulib proofs, to be investigated more
aseemr Dec 24, 2020
5489932
snap
aseemr Dec 24, 2020
7f0cb99
merge with master
aseemr Dec 24, 2020
ad52bfb
snap
aseemr Dec 24, 2020
10fa725
introduce lex_eq for checking equality in lex tuples
aseemr Dec 28, 2020
98a0da3
change in the reflection API for comps
aseemr Dec 28, 2020
6e49931
snap
aseemr Dec 28, 2020
ebe256a
same length lex lists
aseemr Dec 28, 2020
37e2415
snap
aseemr Dec 28, 2020
fddef93
tweak to the parser (fixing regression in Huffman)
aseemr Dec 28, 2020
f64cfce
removing uses of lex tuples
aseemr Dec 28, 2020
5fc6611
adapting string printer examples
aseemr Dec 30, 2020
6be7c10
makefile tweak to add include paths to the emacs target
aseemr Dec 30, 2020
1f20c2b
handle empty decreases clauses
aseemr Dec 30, 2020
7905f6b
snap
aseemr Dec 30, 2020
9628b88
adding a new parser ast node LexList, to help with pretty printing
aseemr Dec 30, 2020
8a639c6
snap
aseemr Dec 30, 2020
a730abd
adding a test case for lex list pretty printing
aseemr Dec 30, 2020
5159aac
commenting a few bug reports testcases that refered to LexTop etc.
aseemr Dec 30, 2020
34ecb9e
accept pretty printing testcases (line number changes in prims)
aseemr Dec 30, 2020
bb35a08
use a different kremlin branch for CI
aseemr Dec 30, 2020
f6666fa
removing more LexCons
aseemr Jan 6, 2021
bd778d5
snap
aseemr Jan 6, 2021
a8946e2
merge with master
aseemr Feb 1, 2021
c147cb2
snap
aseemr Feb 1, 2021
3b3ca0d
some cleanup
aseemr Feb 1, 2021
3d9019a
nit
aseemr Feb 1, 2021
716ceb0
interactive tests
aseemr Feb 1, 2021
5b44c78
removing lex_eq
aseemr Feb 2, 2021
ccc7411
snap
aseemr Feb 2, 2021
ebfba47
tests
aseemr Feb 2, 2021
efd037d
Adding mk_eq3_no_univ
aseemr Feb 4, 2021
df8b0fe
Providing type arguments for eq3 when building precedes
aseemr Feb 4, 2021
c7120c3
snap
aseemr Feb 4, 2021
5801194
try unfolding of the eq3 type arguments in precedes
aseemr Feb 5, 2021
34581f8
snap
aseemr Feb 5, 2021
260bd70
Revert "try unfolding of the eq3 type arguments in precedes"
aseemr Feb 5, 2021
d8cb0c9
warning to the user, if the type equality in precedes may fail
aseemr Feb 5, 2021
0baf227
annotating two failing examples
aseemr Feb 5, 2021
2d20cee
tweaking the precedes eq3 warning a bit
aseemr Feb 5, 2021
79918c0
interactive tests
aseemr Feb 5, 2021
f3de5ce
some tweaks to Reflection.Derived
aseemr Feb 5, 2021
7fd073b
revert the interactive test
aseemr Feb 5, 2021
a33dbb0
removing an unnecessary call to norm for the recursive lb type in TcTerm
aseemr Feb 5, 2021
da29700
snap
aseemr Feb 5, 2021
7576468
Merge branch '_aseem_1916_no_lex_eq' of github.com:FStarLang/FStar in…
aseemr Feb 5, 2021
efa119d
Merge branch 'master' into _aseem_1916_no_lex_eq
aseemr Feb 9, 2021
064da0c
CHANGES.md
aseemr Feb 9, 2021
838844d
Kick CI
aseemr Feb 9, 2021
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
Prev Previous commit
Next Next commit
annotating two failing examples
  • Loading branch information
@aseemr
aseemr committed Feb 5, 2021
commit 0baf2277cd1e2c83ba71c4bc9659f1a84837a33a
2 changes: 1 addition & 1 deletion tests/bug-reports/Bug281.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ val sub_einc : nat -> Tot (exp)
let sub_einc x = EVar (x+1)

val esubst : s:sub -> e:exp -> Tot (r:exp{renaming s /\ EVar? e ==> EVar? r})
(decreases %[is_evar e; is_renaming s; 1;e])
(decreases %[(is_evar e) <: int; is_renaming s; 1;e])
val sub_elam : s:sub -> Tot (r:sub{renaming s ==> renaming r})
(decreases %[1;is_renaming s; 0; EVar 0])

Expand Down
2 changes: 1 addition & 1 deletion tests/bug-reports/Bug442.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ let rec lt l =
| hd :: tl -> ld hd + lt tl

val finish : #a:Type0 -> #t:Type0 -> rights : list (dList t) -> xs : a -> f : (a -> t -> a)
-> Tot a (decreases %[lt rights; 1])
-> Tot a (decreases %[(lt rights) <: int; 1])
val walk : #a:Type0 -> #t:Type0 -> rights : list (dList t) -> l : dList t -> xs : a -> f : (a -> t -> Tot a)
-> Tot a (decreases %[ld l + lt rights; 0])

Expand Down