max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
17038 commits 1 branch 0 tags 5.3 GiB
Commit graph

106 commits

Author SHA1 Message Date
Leonardo de Moura
295cabed2e chore(library/init): remove unnecessary notations 2019-07-11 10:27:16 -07:00
Leonardo de Moura
c00788a982 fix(library/init/lean/compiler/ir/emitcpp): header of big boxed functions 2019-07-08 21:52:01 -07:00
Leonardo de Moura
324a053f4c fix(library/init/lean/compiler/ir/resetreuse): bug at Dmain 2019-07-08 20:37:54 -07:00
Leonardo de Moura
1a81d60820 chore(frontends/lean/parser): simplify binder notation 
The `<ident> : <expr>` now requires explicit brackets.
 2019-07-08 08:54:19 -07:00
Leonardo de Moura
ea6eee516b chore(frontends/lean): use => instead of := in match-expressions 
Motivation: use same separator used in lambda expressions as in
other programming languages.
 2019-07-04 11:38:38 -07:00
Leonardo de Moura
92466272ed fix(library/init/lean/compiler/ir/emitcpp): incorrectly emitting unicode characters in the range [128, 255] 
For example, "·" was being stored as `\xb7` which is not the valid UTF8.
 2019-07-02 15:56:32 -07:00
Leonardo de Moura
a02443d23d chore(frontends/lean): fun x, e ==> fun x => e 2019-07-02 13:22:11 -07:00
Leonardo de Moura
6841e47aa4 chore(frontends/lean/builtin_exprs): remove support for (<infix>) and (<infix> <expr>) notations 
In Lean 4, we will support the more general

`a + ·` ==> `fun x, a + x`
`· + b` ==> `fun x, x + b`
`· + ·` ==> `fun x y, x + y`
`f · y` ==> `fun x, f a y`
`g · · b` ==> `fun x y, g x y b`
 2019-07-02 08:06:06 -07:00
Leonardo de Moura
91e1d30cf8 feat(frontends/lean/builtin_exprs): use ; in do-notation 2019-06-27 18:00:43 -07:00
Leonardo de Moura
ab487ea4ac feat(frontends/lean): allow ; instead of in in let-decls 2019-06-27 17:12:03 -07:00
Leonardo de Moura
f05df7c511 fix(library/init/lean/compiler/ir/simpcase): missing optimization 2019-06-26 19:07:07 -07:00
Leonardo de Moura
e00dc873a8 chore(library/pattern_attribute): [pattern] ==> [matchPattern] 2019-06-26 11:26:49 -07:00
Leonardo de Moura
7ca4607ef3 chore(library/init/lean): move name_mangling.lean to compiler directory 2019-06-26 07:05:23 -07:00
Leonardo de Moura
70a1589817 refactor(library/init/lean): move extern.lean to compiler subdirectory 2019-06-25 08:59:55 -07:00
Leonardo de Moura
45dc2cd49a feat(library/init/lean/compiler): [export] attribute in Lean 2019-06-24 15:48:12 -07:00
Leonardo de Moura
94bca2b9d8 chore(library/init): mimize use of notations 2019-06-24 15:48:11 -07:00
Leonardo de Moura
dda0e38802 chore(library/init): avoid local notation 2019-06-24 15:48:11 -07:00
Leonardo de Moura
bc9e460f62 fix(library/init/lean/compiler/ir): collectUsedDecls must take initialization functions into account 
Move builtin parser level to its own directory
 2019-06-21 13:34:42 -07:00
Leonardo de Moura
0b99a18f97 chore(library): use >> as notation for andthen 
We have other plans for `;`.
 2019-06-20 09:54:53 -07:00
Leonardo de Moura
f176a7963c feat(library/init/lean/compiler/ir/emitcpp): register arity 0 declarations 2019-06-07 17:15:16 -07:00
Leonardo de Moura
c3a7cc4617 feat(library/init/lean/compiler/ir/emitcpp): register functions 2019-06-07 15:34:55 -07:00
Leonardo de Moura
89ab07a4b0 refactor(library/init/lean/environment): more flexible PersistentEnvExtensionState 
The previous API was not flexible enough to implement the new
`AttributeManager` with all "bells and whistles" we want.
For example, the new `addImportedFn` field allows us to initialize
the state for the imported entries using a `Thunk`.
 2019-06-04 16:35:21 -07:00
Leonardo de Moura
0a08569b46 feat(library/init/lean/environment): remove lazy, add addImported field to PersistentEnvExtension 
It seems `lazy := false` is only going to be used in the attribute
manager. So, I remove it. I added a new field `addImported : Bool`
instead. An extension can specify whether `addEntryFn` is going to be
invoked or not for imported entries. `addImported := false` is useful for extensions such
as `protected`, and I will use it in the attribute manager too.
 2019-06-03 16:45:27 -07:00
Leonardo de Moura
8256a48cda fix(library/init/lean/compiler/ir/rc): uset live vars 2019-05-31 21:55:57 -07:00
Leonardo de Moura
d9cceec9eb feat(library/init/lean/compiler/ir/emitcpp): avoid unnecessary var decls 2019-05-30 09:36:28 -07:00
Leonardo de Moura
d9856889d6 chore(*): cleanup 2019-05-30 07:30:07 -07:00
Leonardo de Moura
0f43c2e2d9 feat(library/init/data/array/basic): efficient heterogeneous Array.map 
This commit also removes Array.hmap.
Motivation: I wanted to use Array.hmap as an example in the paper, but
I found it would be too distracting to explain why we had `Array.hmap`
and `Array.map`.

cc @kha
 2019-05-25 16:32:59 -07:00
Leonardo de Moura
4b896bc71c fix(library/init/lean/compiler/ir/rc): use updated ctx at addDecForAlt 
Compiler was introducing unnecessary `dec` operations
 2019-05-24 19:20:20 -07:00
Leonardo de Moura
3f26ec8777 fix(library/init/lean/compiler/ir/expandresetreuse): typo at consumed 2019-05-23 18:17:44 -07:00
Leonardo de Moura
7ef495a526 fix(library/init/lean/compiler/ir): use setTag at expandresetreuse 
This commit also adds the instruction `setTag`, and removes `release`.
 2019-05-23 17:41:14 -07:00
Leonardo de Moura
bf3575a316 feat(library/init/lean/compiler/ir): improve expandresetreuse 2019-05-23 17:23:50 -07:00
Leonardo de Moura
78fe0b901d fix(library/init/lean/compiler/ir/resetreuse): bug at D 2019-05-23 16:57:59 -07:00
Leonardo de Moura
506c354a76 feat(library/init/lean/compiler/ir): push projections more aggresively 
The implementation was not matching the C++ version
 2019-05-23 15:03:51 -07:00
Leonardo de Moura
7cb5c04f4f feat(library/init/lean/compiler/ir/expandresetreuse): first draft 2019-05-23 14:07:08 -07:00
Leonardo de Moura
c6c46df285 feat(library/init/lean/compiler/ir): develop expandresetreuse 2019-05-23 12:42:31 -07:00
Leonardo de Moura
f9f4e6c14b feat(library/init/lean/compiler/ir): add expandresetreuse 2019-05-23 08:58:16 -07:00
Leonardo de Moura
8ba7dd4cff feat(library/init/lean/compiler/ir): add del instruction for releasing memory 2019-05-23 08:01:15 -07:00
Leonardo de Moura
c6433460fb chore(library/init/lean/compiler/ir/format): naming consistency 2019-05-22 18:46:50 -07:00
Leonardo de Moura
013f0c9edb feat(library/init/lean/compiler/ir/rc): missing optimization 2019-05-22 18:46:43 -07:00
Leonardo de Moura
3e76e43843 fix(library/init/lean/compiler/ir/borrow): visit join point body 2019-05-22 17:31:56 -07:00
Leonardo de Moura
fe0141918a fix(library/init/lean/compiler/ir) bug at addDecAfterFullApp 2019-05-22 16:30:42 -07:00
Leonardo de Moura
568bd1c269 fix(library/init/lean/compiler/ir/borrow): do not perform borrow inference for @[export] declarations 2019-05-22 11:44:34 -07:00
Leonardo de Moura
a8f8df1475 chore(library/init/lean/compiler): add export.lean 2019-05-22 11:27:25 -07:00
Leonardo de Moura
2408d6dd80 fix(library/init/lean/compiler/ir/boxing): created boxed version for externs 2019-05-22 10:56:51 -07:00
Leonardo de Moura
99d2f9931d fix(library/init/lean/compiler/ir/resetreuse): typo 2019-05-22 08:45:29 -07:00
Leonardo de Moura
ef89945ea0 fix(library/init/lean/compiler/ir/emitcpp): tail call 
Implement fix used at 4d2837430a in the new IR compiler.
 2019-05-22 07:58:33 -07:00
Leonardo de Moura
64525116f5 fix(library/init/lean/compiler/ir): avoid compilation warning 2019-05-21 20:19:45 -07:00
Leonardo de Moura
c391bff33c fix(library/init/lean/compiler/ir/emitcpp): misssing condition 2019-05-21 20:09:27 -07:00
Leonardo de Moura
f1fbe5cd61 feat(library/compiler/ir): add boxed version for extern constants 2019-05-21 17:55:58 -07:00
Leonardo de Moura
d90cfe5a1c feat(library/init/lean/compiler/ir/boxing): generate boxed version 2019-05-21 17:35:43 -07:00