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

812 commits

Author SHA1 Message Date
Leonardo de Moura
d212abb9ee feat(library/init/lean/syntax): export helper functions for creating syntax in C++ 2019-06-05 16:49:58 -07:00
Leonardo de Moura
df3b85490b feat(library/init/lean/position): add new FileMap 2019-06-05 15:58:53 -07:00
Leonardo de Moura
7909d86e5d feat(library/init/lean): Syntax objects with new SyntaxNodeKind and Substring, and arrays instead of lists 
We can use `SyntaxNodeKind.id : Nat` to implement maps from kind to
values using arrays.
 2019-06-05 15:35:51 -07:00
Leonardo de Moura
55626ba60d chore(library/init/lean): disable new frontend for now 
We are going to start making drastic changes in the parser,
elaborator, attributes, etc. Examples:
- No View objects. I am going to implement match_syntax.
- No RecT in the parser. I am going to implement parser extensions
using an approach similar to the one I used to implement environment
extensions.
- No Parsec. I will use an approach similar to the one used in the
experiment https://github.com/leanprover/lean4/tree/master/tests/playground/parser

It is easier to perform these changes with the new frontend disabled.
I will slowly re-active it as I apply the changes.

cc @kha
 2019-06-05 15:26:43 -07:00
Leonardo de Moura
642992eeca chore(library/init/lean/attributes): missing @[export] 2019-06-05 13:30:26 -07:00
Leonardo de Moura
fd9c8a4c82 feat(library/init/lean/attributes): add pushScope/popScope, missing APIs, and @[export] 2019-06-05 13:17:25 -07:00
Leonardo de Moura
2cb50f31bd chore(library/init/lean/environment): error message consistency 2019-06-05 09:16:10 -07:00
Leonardo de Moura
67a4ebbde6 feat(library/init/lean/attributes): low level attribute registration, and frontend attribute actions 
Remark: the attribute actions used by the frontend are all in IO.
These actions access attributes by name, and need access to the IO.ref
that contains all registered attributes in the system.
 2019-06-05 09:15:35 -07:00
Leonardo de Moura
583f38d1e5 feat(library/init/lean/attributes): attribute API for implementing the new frontend 2019-06-05 07:02:06 -07:00
Leonardo de Moura
c480f1f95c refactor(library/init/lean/environment): move scope management to attributes.lean 2019-06-04 16:50:29 -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
3bb8826bb4 feat(library/init/lean/environment): scope management skeleton 2019-06-04 15:20:07 -07:00
Leonardo de Moura
ca12439e25 feat(library/init/lean/environment): add persistent := true parameter to addEntry 2019-06-03 17:03:46 -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
90dc3356dc chore(library/init/lean/environment): remove unnecessary local instance 2019-06-03 16:24:36 -07:00
Leonardo de Moura
4a26f0028c chore(library/init/lean/environment): remove unnecessary function 2019-06-03 15:17:40 -07:00
Leonardo de Moura
ed1a433d52 feat(library/init/lean/modifiers): add privatePrefix 2019-06-03 10:33:40 -07:00
Leonardo de Moura
224195a1fb feat(library/init/lean/modifiers): environment extension for private declarations 2019-06-03 10:10:00 -07:00
Leonardo de Moura
cd73105dff refactor(kernel/environment,library/private,library/init/lean/environment): move main module name to header 2019-06-03 09:14:23 -07:00
Leonardo de Moura
483f1efc4d refactor(library/init/lean/environment): move fields that are rarely used to a separate structure, add setMainModuleName 2019-06-03 08:23:00 -07:00
Leonardo de Moura
6d39b8478f chore(library/init/lean/environment): remove dead field 2019-06-03 08:08:04 -07:00
Leonardo de Moura
8d913e382d feat(library/init/lean/compiler/constfolding): fold Nat.pow, UInt*.toNat and USize.toNat 2019-06-01 10:28:04 -07:00
Leonardo de Moura
c92fe75053 fix(library/init/lean/compiler/constfolding): Usize => USize 
Camel case auto-conversion bug.
 2019-06-01 09:42:22 -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