max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/library/init/lean/compiler/ir
History
Leonardo de Moura 680ee21161 feat(library/init/lean/compiler/ir): add unreachbranches.lean 
New optimization pass for eliminating unreachable branches that occur
very often when using `ExceptT` and `EState`.

The current commit implements an abstract interpreter for computing
an approximation of the kinds of values returned by a function.
TODO:
- Implement `FnBody.jmp`.
- Implement `interpDecl`
- Remove unreachable branches in `FnBody.case`
2019-10-02 19:57:43 -07:00
..
basic.lean chore(library/init/lean/compiler/ir/basic): remove unnecessary function 2019-10-02 16:50:37 -07:00
borrow.lean refactor(library/init/data/array): new name convention for Array functions 2019-10-01 16:46:05 -07:00
boxing.lean refactor(library/init/data/array): new name convention for Array functions 2019-10-01 16:46:05 -07:00
checker.lean feat(library/init/lean/compiler/ir): store scrutinee type at FnBody.case 2019-09-12 08:07:47 -07:00
compilerm.lean feat(library/init/lean/smap): implement SMap using PHashMap instead of RBMap 2019-09-20 14:22:03 -07:00
default.lean feat(library/init/lean/compiler/ir): add [unbox] attribute 2019-10-02 16:50:37 -07:00
elimdead.lean feat(library/init/lean/compiler/ir): store scrutinee type at FnBody.case 2019-09-12 08:07:47 -07:00
emitc.lean refactor(library/init/data/array): new name convention for Array functions 2019-10-01 16:46:05 -07:00
emitutil.lean feat(library/init): add more general modify: modifyGet 2019-09-16 15:14:02 -07:00
expandresetreuse.lean refactor(library/init/data/array): new name convention for Array functions 2019-10-01 16:46:05 -07:00
format.lean feat(library/init/lean/compiler/ir): add unreachbranches.lean 2019-10-02 19:57:43 -07:00
freevars.lean feat(library/init/lean/compiler/ir): store scrutinee type at FnBody.case 2019-09-12 08:07:47 -07:00
livevars.lean fix(library/init/lean/compiler/ir/livevars): bug at updateLiveVars 2019-10-02 16:50:37 -07:00
normids.lean feat(library/init): add more general modify: modifyGet 2019-09-16 15:14:02 -07:00
pushproj.lean refactor(library/init/data/array): new name convention for Array functions 2019-10-01 16:46:05 -07:00
rc.lean refactor(library/init/data/array): new name convention for Array functions 2019-10-01 16:46:05 -07:00
resetreuse.lean feat(library/init/lean/compiler/ir): store scrutinee type at FnBody.case 2019-09-12 08:07:47 -07:00
simpcase.lean refactor(library/init/data/array): new name convention for Array functions 2019-10-01 16:46:05 -07:00
unboxresult.lean fix(library/init/lean/compiler/ir/unboxresult): reject recursive types 2019-10-02 16:50:37 -07:00
unreachbranches.lean feat(library/init/lean/compiler/ir): add unreachbranches.lean 2019-10-02 19:57:43 -07:00