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

L6 ANF from L6 CPS #10

Closed
wants to merge 82 commits into from
Closed

L6 ANF from L6 CPS #10

Changes from 1 commit
Commits
Show all changes
82 commits
Select commit Hold shift + click to select a range
577d81c
Rolled back compute_fEnv_fds since it only worked for known functions…
Sep 29, 2019
b1db5c8
Added benchmarks target to the benchmarks/Makefile, with benchmarks/b…
Oct 2, 2019
3f0c167
Added a README in the benchmarks folder documenting the use of timePhase
Oct 5, 2019
dfede3e
Name shadowing fix and removed Focus warnings
mzweav Oct 5, 2019
59fc45c
added 6 fun param version of code gen
mzweav Oct 16, 2019
8495334
CP in ANF
zoep Oct 16, 2019
d98fee7
Merge remote-tracking branch 'origin/zoe_lambda-lifting' into code_ge…
mzweav Oct 16, 2019
0d72a3b
Removed redundant files/parameterized function arguments
mzweav Oct 16, 2019
c79247c
Progress on generating printers: constructor names can be printed now
joom Oct 20, 2019
88dc9f9
More comments on printing
joom Oct 20, 2019
22bf94a
progress on proof
mzweav Oct 20, 2019
d17244e
Some progress on Eapp case
Oct 20, 2019
5973944
(stub of) Proof progressed to end of Eapp case
Oct 21, 2019
852630a
Fix repr_asgn_fun_entry for expected Hlenv_new'''_asgn_i
Oct 21, 2019
a58b2fe
progress on proof
mzweav Oct 21, 2019
2e4920e
Move glue code generation to a different module
joom Oct 22, 2019
48b01e3
Progress on glue code generation: printers and constructor name arrays
joom Oct 22, 2019
3efe0cc
Fixed bug in dead param elim that resulted in empty C file
zoep Oct 23, 2019
e149590
error support in L6 state
zoep Oct 23, 2019
63f0ade
Two different L6 pipelines (CPS and ANF)
zoep Oct 23, 2019
4ad4a14
solved merge conflit
zoep Oct 23, 2019
1b127e7
CP in code extraction
zoep Oct 23, 2019
91baba2
Progress using L1 constructor types in glue code generation
joom Oct 23, 2019
f75f70b
CP in code generation
zoep Oct 23, 2019
91a242c
C code generation for ANF
zoep Oct 24, 2019
dc3f271
Getting glue code generation ready for parametrized types, and moving…
joom Oct 25, 2019
3c655b4
WIP in GC with shadow stack
zoep Oct 25, 2019
1906f1c
Fixed some bus in shadow stack GC
zoep Oct 28, 2019
7b81584
CP before fix
zoep Oct 28, 2019
59288c3
Big fix in inline letapp in shrink reduction and beta contruction
zoep Oct 29, 2019
f2848e5
Added forgotten L4 to L6 ANF file.
zoep Oct 29, 2019
f5019a6
Plugin support for printing L6 for debugging purposes
zoep Oct 29, 2019
7e73dab
Plugin support for printing L6 for debugging purposes
zoep Oct 29, 2019
decd2c5
Bug fixes in C runtime with stack
zoep Oct 29, 2019
ddf84d6
Added letapp case n bstep eval
zoep Oct 29, 2019
d1d203c
Minor tweaks
zoep Oct 30, 2019
121c413
Minor tweaks
zoep Oct 30, 2019
3d22ebf
Patches in the Log Rel framework
zoep Oct 30, 2019
0dbee08
Notes in uncurry
zoep Oct 30, 2019
914f6f9
Updated closure util lemmas
zoep Oct 31, 2019
3665266
Replaced old closure conversion
zoep Oct 31, 2019
2540ace
Replaced old closure conversion
zoep Oct 31, 2019
488295b
Tweaks in semantics
zoep Oct 31, 2019
476dc6b
Added logical relation back to the build
zoep Oct 31, 2019
c6e06a5
Removed dependency resolution warnings and L6 and compcert. In comcer…
zoep Oct 31, 2019
3604fda
Fixed warnings in extraction
zoep Oct 31, 2019
52169c9
WIP in closure conv proof
zoep Nov 2, 2019
98e8137
Add hoare triples + lemmas for new state monad
john-ml Nov 2, 2019
3a5ed4b
WIP in closure conv proof
zoep Nov 3, 2019
ce3164b
Merge branch 'zoe-ANF' of github.com:PrincetonUniversity/certicoq int…
zoep Nov 3, 2019
5ca24bb
Done with the hard case of CC
zoep Nov 4, 2019
2f22f59
- Moved environment invariants for CC proof to different file to avoi…
zoep Nov 5, 2019
d6854ee
Cleanup
zoep Nov 5, 2019
d8a4f48
WIP in parameterizing CC proof with bounds (as opposed to showing the…
zoep Nov 5, 2019
76cf277
Progress in proofs
zoep Nov 7, 2019
9524e02
WIP correctness of inlining
john-ml Nov 8, 2019
1a9f409
Start app/letapp inlining cases
john-ml Nov 9, 2019
989bbbd
More tweaks in CC proof
zoep Nov 9, 2019
aa2882a
Merge branch 'zoe-ANF' of github.com:PrincetonUniversity/certicoq int…
zoep Nov 9, 2019
035b5f0
Updated hoisting proof
zoep Nov 11, 2019
3aec56d
Updated compat lemmas
zoep Nov 11, 2019
2749c03
Commented out alpha_conv proof currently (needs update for bounds and…
zoep Nov 11, 2019
6156092
Fixed compat lemmmas in hoisting proof
zoep Nov 11, 2019
a581928
Some cleanup in hoisting
zoep Nov 11, 2019
2f95636
Updated bound_stem
zoep Nov 12, 2019
1d7e8a3
CP
zoep Nov 12, 2019
2188e50
Correct print functions generated for monomorphic types
joom Nov 13, 2019
0d760bf
Merge remote-tracking branch 'remotes/origin/timing' into code_gen_opt
Nov 13, 2019
33aaf34
Rudimentary polymorphic print functions done, needs some cleanup
joom Nov 14, 2019
7d7f0c4
Compositionality experiments
zoep Nov 17, 2019
8a6507e
WIP in updating alpha_conv proof
zoep Nov 18, 2019
3fe127c
Polymorphic print functions + moved constructor generation to glue.v
joom Nov 18, 2019
7eb8d73
WIP in alpha_conv, and removed dead_param_elim from pipeline again
zoep Nov 18, 2019
202dd46
Removed alpha_conv from build for now
zoep Nov 18, 2019
0a9b683
WIP Inlining proof
john-ml Nov 18, 2019
a5931a1
Merge branch 'zoe-ANF' of https://github.com/PrincetonUniversity/cert…
john-ml Nov 18, 2019
69f3c04
Merge remote-tracking branch 'origin/code_gen_opt'
joom Nov 19, 2019
9a4ff61
Fix compile error and styling in L6_to_Clight.v
joom Nov 19, 2019
6b849fe
Finished with the Alpha_conv proof
zoep Nov 20, 2019
00413ea
Merged with Joomy
zoep Nov 20, 2019
8c73622
Fix after merge
zoep Nov 20, 2019
f4128c6
Some changes in tests etc after merge
joom Nov 26, 2019
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
Fix compile error and styling in L6_to_Clight.v
  • Loading branch information
@joom
joom committed Nov 19, 2019
commit 9a4ff61cdd063d8fad446b0b46fb03057838c2cf
Loading