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

Using core typechecker for indexed effects unification solutions #2760

Merged
merged 163 commits into from
Nov 22, 2022
Merged

Using core typechecker for indexed effects unification solutions #2760

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
163 commits
Select commit Hold shift + click to select a range
fb4c558
wip, uvar kinds
aseemr Oct 7, 2022
f9a4291
merge with master
aseemr Oct 10, 2022
fc33397
snap
aseemr Oct 10, 2022
0ad14a9
don't create guard uvar when weakening or strengthening
aseemr Oct 10, 2022
41bdd9d
snap
aseemr Oct 10, 2022
df01d3b
solve guard uvars in rel
aseemr Oct 11, 2022
de0c0d0
snap
aseemr Oct 11, 2022
4858bd8
some debug logs
aseemr Oct 11, 2022
172fc1b
one guard uvar per uvar, setting in a helper function in Rel
aseemr Oct 11, 2022
4384560
propagation of guard uvar
aseemr Oct 11, 2022
ecaa8f3
cp
aseemr Oct 11, 2022
a802b54
set guard uvar even if no guard in core check
aseemr Oct 12, 2022
b96bd7c
handle a Tm_delayed in the UF graph in push_subst
aseemr Oct 12, 2022
22169a3
some more tweaks
aseemr Oct 12, 2022
e5c8b6a
snap
aseemr Oct 12, 2022
d06b1f1
merge with nik_memoize_tc
aseemr Oct 12, 2022
9300f6a
snap
aseemr Oct 12, 2022
0eeac0e
undo syntax subst
aseemr Oct 12, 2022
e7b81b7
split guard API
aseemr Oct 12, 2022
b89ba36
resolve implicits of tc abs guards before discharging smt guard
aseemr Oct 12, 2022
e0b4dff
snap
aseemr Oct 12, 2022
5709d4e
use propositional and for incorporating guard uvars in vc
aseemr Oct 13, 2022
ac5a64e
merge
aseemr Oct 13, 2022
72580e7
if guard uvars are not allowed, use allow untyped
aseemr Oct 13, 2022
17e60ef
snap
aseemr Oct 13, 2022
9871fef
strengthen lift vc with guards, rather than returning them
aseemr Oct 13, 2022
6df0654
don't restrict guard uvars, more cases of strengthening with guard uvars
aseemr Oct 13, 2022
2a08115
snap
aseemr Oct 13, 2022
906dbe0
don't core check allow untyped uvars
aseemr Oct 14, 2022
2bfa4aa
adding a meta core guard + some annotations in prims
aseemr Oct 14, 2022
9c07512
merge
aseemr Oct 17, 2022
47052a3
snap
aseemr Oct 17, 2022
36562d6
checking bind combinator kind
aseemr Oct 17, 2022
491a27f
snap
aseemr Oct 17, 2022
46a1e67
wip
aseemr Oct 18, 2022
6865c9e
wip
aseemr Oct 18, 2022
dbb8c1a
cp
aseemr Oct 18, 2022
ac63ff5
unmeta meta_core_guard in smt
aseemr Oct 18, 2022
ba20488
some restucturing to allow for standard and ad-hoc binds
aseemr Oct 18, 2022
20148d1
indexed effects binder kinds in Syntax
aseemr Oct 18, 2022
c993a82
snap
aseemr Oct 18, 2022
f4a3a5c
debugging steel semantics, cp
aseemr Oct 18, 2022
9330ab0
some tweak to guard uvars in phase1 and lax
aseemr Oct 18, 2022
df9f556
snap
aseemr Oct 18, 2022
9508741
support for substitutive polymonadic binds
aseemr Oct 18, 2022
58cc3a4
snap
aseemr Oct 18, 2022
cc974f2
enable uvar guards for returns
aseemr Oct 19, 2022
32e07c3
merge
aseemr Oct 19, 2022
e76237a
snap
aseemr Oct 19, 2022
1457238
validating subcomp shape
aseemr Oct 19, 2022
b6473df
cp
aseemr Oct 19, 2022
ae9e85a
notion of standard for subcomp
aseemr Oct 19, 2022
c6ba665
snap
aseemr Oct 19, 2022
defe229
standard polymonadic subcomp
aseemr Oct 19, 2022
ec94939
snap
aseemr Oct 19, 2022
206af93
checking standard lift
aseemr Oct 19, 2022
7749b28
substitutive lifts
aseemr Oct 19, 2022
fc3f178
snap
aseemr Oct 19, 2022
d3ec8b9
cp, substitutive ite
aseemr Oct 19, 2022
32074ef
tweaks for dependent effect signature
aseemr Oct 19, 2022
61c9a7e
merge
aseemr Oct 20, 2022
1e6d7ab
snap
aseemr Oct 20, 2022
baca82f
cp
aseemr Oct 20, 2022
d250996
merge with master
aseemr Oct 21, 2022
f481f11
syntax AST support for indexed effect parameters
aseemr Oct 21, 2022
f50d582
snap
aseemr Oct 21, 2022
32c3b92
wip, indexed effect params
aseemr Oct 21, 2022
60555df
cp
aseemr Oct 21, 2022
96fbdb4
small example with effect params
aseemr Oct 21, 2022
89b7f25
snap
aseemr Oct 21, 2022
8b140d3
bug
aseemr Oct 21, 2022
84681d3
effect params in action
aseemr Oct 21, 2022
4604b8e
snap
aseemr Oct 21, 2022
ebe76f2
more precise equality
aseemr Oct 21, 2022
952084f
snap
aseemr Oct 21, 2022
e56429c
marking mst/nmst effects with params
aseemr Oct 21, 2022
d5c4bb4
snap
aseemr Oct 21, 2022
c55eebe
merge
aseemr Oct 25, 2022
805e3cd
snap
aseemr Oct 25, 2022
a315b64
trying some order in logical goals
aseemr Oct 25, 2022
8eec407
phase1 for tac implicits, simplify away core guards in vc
aseemr Oct 25, 2022
f0b8cef
Revert "trying some order in logical goals"
aseemr Oct 25, 2022
2f16333
nit
aseemr Oct 26, 2022
27a8aa1
wip
aseemr Oct 26, 2022
7e44437
some tweaks to Lattice Spec to make it standard
aseemr Oct 26, 2022
d4cf107
fixing a nit in classifying a bind as standard
aseemr Oct 27, 2022
6617975
snap
aseemr Oct 27, 2022
b616e0c
standardized
aseemr Oct 27, 2022
8ad21b4
standardized
aseemr Oct 27, 2022
d1295ca
RW
aseemr Oct 27, 2022
8c1cca1
GTWP
aseemr Oct 27, 2022
22da5a6
ID1
aseemr Oct 27, 2022
30665ef
wip
aseemr Oct 27, 2022
cacc734
all indexed effect uvars as Strict
aseemr Oct 27, 2022
a8c448d
snap
aseemr Oct 27, 2022
a9f4622
merge
aseemr Oct 27, 2022
477e1c4
snap
aseemr Oct 27, 2022
27f5ac8
cp
aseemr Oct 27, 2022
269806f
nit
aseemr Oct 27, 2022
2c70aa8
some cleanup
aseemr Oct 27, 2022
efc3a25
snap
aseemr Oct 27, 2022
9723ac7
removing a couple of Allow_untypeds
aseemr Oct 27, 2022
c521eef
nit
aseemr Oct 27, 2022
11ca5ae
restore lowparse examples
aseemr Oct 28, 2022
22a581d
merge
aseemr Oct 28, 2022
f06dfd1
removing allow_informative_binders attr
aseemr Oct 28, 2022
b399126
tweaks
aseemr Oct 28, 2022
254b1c8
snap
aseemr Oct 28, 2022
b930036
a slightly modified #2659
aseemr Oct 28, 2022
4bdc747
removing an outdated comment
aseemr Oct 28, 2022
5f0c586
merge
aseemr Oct 31, 2022
2c15728
snap
aseemr Oct 31, 2022
46a1a21
merge
aseemr Nov 7, 2022
719930d
snap
aseemr Nov 7, 2022
a50c655
some nits
aseemr Nov 7, 2022
64ab649
merge
aseemr Nov 8, 2022
e48d19e
snap
aseemr Nov 8, 2022
e1f25bf
merge
aseemr Nov 9, 2022
3b1d65c
snap
aseemr Nov 9, 2022
4e1a768
create indexed effects uvars as Allow_untyped if compat pre core flag…
aseemr Nov 9, 2022
6689a8e
REVERT: temporarily disable CQueue
aseemr Nov 9, 2022
c0ca99c
update tests
aseemr Nov 9, 2022
f4f26a7
snap
aseemr Nov 9, 2022
c231f16
making NDS substitutive
aseemr Nov 9, 2022
cd70b06
nit
aseemr Nov 9, 2022
f226387
merge
aseemr Nov 11, 2022
64047a6
snap
aseemr Nov 11, 2022
47191a6
compat_pre_typed_indexed_effects
aseemr Nov 11, 2022
87ba592
Merge branch 'master' into _aseem_substitutive_indexed_effects
aseemr Nov 11, 2022
40a514d
merge
aseemr Nov 14, 2022
baec726
reset letrecs when calling tc from the tactics engine
aseemr Nov 14, 2022
3b7d2a0
Reenable CQueue
aseemr Nov 14, 2022
bbecbd7
snap
aseemr Nov 14, 2022
ff5a522
add binders to env in monadic app only if needed
aseemr Nov 15, 2022
f587b6d
merge
aseemr Nov 15, 2022
3c1f041
snap
aseemr Nov 15, 2022
88f1f5c
Merge branch 'master' into _aseem_substitutive_indexed_effects
aseemr Nov 16, 2022
9c63459
some cleanup in syntax and comments
aseemr Nov 16, 2022
5b67575
check that all effect parameters are upfront
aseemr Nov 16, 2022
0694274
some cleanup and comments in Rel
aseemr Nov 16, 2022
8e4182c
rel cp
aseemr Nov 16, 2022
d31c7fa
some comments in tc effect
aseemr Nov 16, 2022
445fa23
nits
aseemr Nov 16, 2022
f81208d
comments in tc util
aseemr Nov 16, 2022
041fa18
nits
aseemr Nov 16, 2022
e32e573
tests
aseemr Nov 16, 2022
61ea368
warning for ad hoc indexed effects combinators
aseemr Nov 16, 2022
80c3619
messed up guards
aseemr Nov 16, 2022
f4751e3
error messages again
aseemr Nov 16, 2022
48c6f38
Merge branch 'master' into _aseem_substitutive_indexed_effects
aseemr Nov 17, 2022
030bc19
checked file number + CHANGES
aseemr Nov 17, 2022
36a4e7e
suppress 352 for ulib/steel
aseemr Nov 17, 2022
352dd51
tweak subcomp in Sec2.IFC to resolve a warning
nikswamy Nov 17, 2022
f9449e2
Merge branch 'master' into _aseem_substitutive_indexed_effects
aseemr Nov 18, 2022
7db7e26
set range of autogenerated subcomp and ite combinators
aseemr Nov 18, 2022
08c7d7e
another kind of substitutive subcomp that allows for f and g indices …
aseemr Nov 18, 2022
8ae7d09
classifying and applying substitutive invariant subcomp
aseemr Nov 18, 2022
3203555
snap
aseemr Nov 18, 2022
996542c
support for substitutive invariant ite
aseemr Nov 18, 2022
2976f3e
nit to Sec1.GST
aseemr Nov 18, 2022
97e38d2
comment in syntax
aseemr Nov 18, 2022
e1c1a18
nits
aseemr Nov 18, 2022
be5fa34
Merge branch 'master' into _aseem_substitutive_indexed_effects
aseemr Nov 21, 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
Prev Previous commit
Next Next commit
propagation of guard uvar
  • Loading branch information
@aseemr
aseemr committed Oct 11, 2022
commit 4384560a83922fc7807a91396506857253e8f898
115 changes: 59 additions & 56 deletions src/ocaml-output/FStar_Tactics_Basic.ml
View file
Open in desktop

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

Loading