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

11520 commits

Author SHA1 Message Date
Leonardo de Moura
a3c0e2bb36 chore(frontends/lean/builtin_exprs): ensure old let notation is not accepted 2019-07-17 08:26:42 -07:00
Leonardo de Moura
0c4708ad28 chore(stage0): update 2019-07-16 09:07:39 -07:00
Leonardo de Moura
b2e1ff8b3e feat(library/init): use new "empty match" syntax 2019-07-15 16:25:14 -07:00
Leonardo de Moura
7d062dd961 feat(frontends/lean): add new "empty/no match" syntax to old parser 2019-07-15 16:18:44 -07:00
Leonardo de Moura
12346d344a feat(shell/lean): invoke new parser when --new-frontend is used 2019-07-15 13:57:05 -07:00
Leonardo de Moura
367f28e90b chore(library/init/lean/parser/module): export test function 2019-07-15 13:39:56 -07:00
Leonardo de Moura
4c3ea024bc chore(stage0): update 2019-07-15 09:46:39 -07:00
Leonardo de Moura
1b8c2200d5 chore(stage0): update 2019-07-11 16:45:09 -07:00
Leonardo de Moura
57e2f1be2a feat(library/init/lean/parser/term): builtin operators 2019-07-11 10:13:00 -07:00
Leonardo de Moura
c9cd693b8e feat(runtime/object): avoid recursion at mark_mt and mark_persistent 
Reason: potential stack overflows
 2019-07-10 11:27:49 -07:00
Leonardo de Moura
a85a98f1ec chore(stage0): update 2019-07-10 11:19:40 -07:00
Leonardo de Moura
022d22cac4 feat(library/compiler/extract_closed): fine grain extraction 
Motivation: increase reuse
 2019-07-10 11:14:20 -07:00
Leonardo de Moura
efa48d6762 chore(stage0): update 2019-07-10 11:11:53 -07:00
Leonardo de Moura
17cc34def5 feat(library/compiler/compiler): add option compiler.extract_closed 
It is useful when using `unsafeIO`
 2019-07-10 11:08:34 -07:00
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