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

11506 commits

Author SHA1 Message Date
Leonardo de Moura
228ddd5fdc chore(stage0): update 2019-07-09 16:39:32 -07:00
Leonardo de Moura
85d151a335 feat(library/compiler): use eta expansion at eager_lambda_lifting 2019-07-09 16:34:20 -07:00
Leonardo de Moura
bda0277468 chore(stage0): update 2019-07-09 14:22:10 -07:00
Leonardo de Moura
f1a2c83e8c feat(library/compiler/eager_lambda_lifting): do not pass closed terms as arguments to lifted decl 2019-07-09 14:06:14 -07:00
Leonardo de Moura
0f873b7ba2 fix(library/compiler/eager_lambda_lifting): collect type dependencies 2019-07-09 13:32:41 -07:00
Leonardo de Moura
ff0d184176 chore(stage0): update 2019-07-08 22:04:51 -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
dbc67242a1 chore(stage0): update 2019-07-08 17:40:30 -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
0fc9aa24bc chore(frontends/lean/parser): remove "binder collection" support 
This kind of notation will not be supported in the new builtin parser.
If users want they may define their own notation with this feature.
 2019-07-08 08:36:29 -07:00
Leonardo de Moura
8fa888878f chore(frontends/lean/parser): remove support for ⦃ binders 2019-07-07 08:37:49 -07:00
Leonardo de Moura
8944767f6c chore(frontends/lean): Π ==> ∀ 2019-07-07 08:13:40 -07:00
Sebastian Ullrich
9707672cc8 fix(runtime/mpz): fix and document size_t functions 2019-07-05 16:27:04 -07:00
Sebastian Ullrich
723e9cc430 chore(runtime/object): fix usize_to_nat name 2019-07-05 16:26:54 -07:00
Sebastian Ullrich
826a5ee16b chore(shell/lean): profile initialization time 2019-07-05 16:21:48 +02:00
Sebastian Ullrich
b41f4a517c chore(bin/leanc): set increased stack size on Windows 2019-07-05 11:24:15 +02:00
Sebastian Ullrich
26155442f1 fix(CMakeLists): cmake -E copy doesn't support wildcards on Windows 
I don't think we'll need archives other than .a if we don't support MSVC
 2019-07-05 11:24:15 +02:00
Sebastian Ullrich
2c9dce6eed fix(runtime/mpz): use size_t instead of unsigned long for Windows compatibility 2019-07-05 11:24:15 +02: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
bf1f62c115 chore(shell/CMakeLists): temporarily remove --output-sync 
@kha this option is only available is gnu make version >= 4.0.
 2019-07-04 10:28:51 -07:00
Sebastian Ullrich
4c650d23d4 chore(shell/CMakeLists): avoid overlapping make output 2019-07-03 08:30:18 -07:00
Leonardo de Moura
0bee94886e feat(frontends/lean/builtin_exprs): , from ==> from, and cleanup suffices 2019-07-02 17:22:50 -07:00
Leonardo de Moura
7ba9a5012a chore(frontends/lean/builtin_exprs): make sure have-expression is consistent with let-expression 2019-07-02 16:46:51 -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
e29bf35d15 chore(frontends/lean/builtin_exprs): remove hard coded (::) notation 2019-07-02 11:01:05 -07:00
Leonardo de Moura
39221adcd6 chore(frontends/lean/builtin_exprs): remove assume notation 2019-07-02 10:40:07 -07:00
Leonardo de Moura
300414e6e4 chore(frontends/lean): change explicit universe parameter notation in declarations 2019-07-02 08:57:08 -07:00
Leonardo de Moura
7cfbf94ca6 chore(frontends/lean/parser): comma separated universe levels 
Make sure old C++ parsers uses the new Lean4 syntax for explicit
universe levels.
 2019-07-02 08:21:16 -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
5691450b5b feat(library/init/lean/parser): term parser skeleton 2019-07-01 15:04:13 -07:00
Leonardo de Moura
531ef5d700 feat(library/init/lean/parser): universe level parser and bug fixes 2019-06-30 09:02:06 -07:00
Leonardo de Moura
4648be6451 feat(runtime/alloc): save memory using a smaller LEAN_OBJECT_SIZE_DELTA 2019-06-29 15:29:39 -07:00
Leonardo de Moura
a77c6f3917 chore(util/object_ref): style 2019-06-27 18:01:54 -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
557dd16864 chore(library,frontends/lean): remove old attribute manager 2019-06-27 14:01:34 -07:00
Leonardo de Moura
4e444a283d feat(library/class): switch to Lean implementation 2019-06-27 13:51:09 -07:00
Leonardo de Moura
7049f4a889 feat(library/init/lean/class): register attributes and export functions 2019-06-27 13:27:13 -07:00
Leonardo de Moura
8399e41a5b feat(library/class): simpler get_class function 
It does not depend on `type_context.h`, and we will used it as a
template to implement the Lean version.
 2019-06-27 10:42:14 -07:00
Leonardo de Moura
6727c1fa68 feat(library/compiler/specialize): switch to specExtension in Lean 2019-06-27 10:08:39 -07:00
Leonardo de Moura
235b4c02c1 feat(library/init/lean/compiler/specialize): implement specExtension in Lean 2019-06-27 09:58:19 -07:00
Leonardo de Moura
4bc0346c17 chore(library/init/lean/compiler): specializeattrs.lean ==> specialize.lean 2019-06-27 09:38:21 -07:00
Leonardo de Moura
3c0caee73b chore(library/compiler/specialize): cleanup 
Preparing to implement environment extension in Lean.
 2019-06-27 09:32:25 -07:00
Leonardo de Moura
cf6f6bc96d chore(stage0): update 2019-06-27 09:30:53 -07:00
Leonardo de Moura
dfa3b6d9af chore(frontends/lean): compilation warnings 2019-06-27 08:00:48 -07:00
Leonardo de Moura
9037595ead chore(stage0): update 2019-06-26 19:09:20 -07:00
Leonardo de Moura
bd58525080 chore(library/class): simplify 2019-06-26 16:51:36 -07:00
Leonardo de Moura
14f05d2001 feat(library/init/lean/compiler): register [implementedBy] attribute using new attribute manager 2019-06-26 15:55:51 -07:00
Leonardo de Moura
1f53c4fd33 feat(library/init/lean/eqncompiler): register [matchPattern] attribute using new attribute manager 2019-06-26 15:38:14 -07:00