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

29892 commits

This branch
This branch
All branches
Author SHA1 Message Date
Chris Lovett
3eeb064d83
fix: Clear Diagnostics when file is closed (#1591) 2022-10-07 17:28:15 -07:00
Leonardo de Moura
45974229d2 feat: reactivate extendJoinPointContext at mono phase 
closes #1686

cc @hargoniX
 2022-10-07 16:27:44 -07:00
Leonardo de Moura
15ad5254a1 chore: update stage0 2022-10-07 16:08:14 -07:00
Leonardo de Moura
9eb641e7da feat: reuse specialized functions between different compilation units 2022-10-07 16:07:17 -07:00
Leonardo de Moura
f11e44910b refactor: add Closure.lean 
This module will also be used by the lambda lifter.
 2022-10-07 15:56:10 -07:00
Leonardo de Moura
e7a36f32f1 refactor: add MonadScope class 
We are going to use it to implement the lambda lifting pass too.
 2022-10-07 14:59:59 -07:00
Leonardo de Moura
1b8e310ada fix: fixes #1674 2022-10-07 13:33:41 -07:00
Leonardo de Moura
5c74bc1324 fix: fixes #1705 2022-10-07 13:11:26 -07:00
David Renshaw
5c7cf76575 doc: fix link to initialization section in ffi section 
The current link goes to doc/dev#init, where there is nothing
about initialization. This PR fixes the link so that it points
to the initialization section lower down on the ffi page.
 2022-10-07 19:11:59 +02:00
David Renshaw
4fa1a496b3 doc: Lean USize maps to C++ size_t, not usize_t 
usize_t is not a standard C++ type.

See src/include/lean/lean.h for translations between USize and size_t.
 2022-10-07 17:51:58 +02:00
E.W.Ayers
d22916fdcd feat: improve expression diff 
Added recursion cases to the diff algorithm for projections and mdata.
Previously, these would be rendered as the entire expression being different but we can do better
by checking if the recursion args are the same.

With mdata, these are entirely ignored by the diff algorithm.
 2022-10-07 12:45:00 +02:00
Leonardo de Moura
5b1aac7b8f fix: avoid nontermination on non-utf8 input 
This is not a perfect solution, but ensures the non-termination does
not happen. The changes also make it easier to prove termination in
the future.

TODO: validate UTF8 input?

closes #1690
 2022-10-06 17:45:21 -07:00
Sebastian Ullrich
d417c0238a doc: normalize Init.Conv docs 2022-10-06 17:27:33 -07:00
Sebastian Ullrich
5b7e6661f9 chore: more RBMap cleanup 2022-10-06 17:26:43 -07:00
Sebastian Ullrich
6f4cea6dba feat: add rbmap_fbip benchmark 2022-10-06 17:26:43 -07:00
Leonardo de Moura
7dfc51ce7c chore: update stage0 2022-10-06 17:22:08 -07:00
Mario Carneiro
391aef5cd7 feat: automatic extension names 2022-10-06 17:19:30 -07:00
Ed Ayers
7fabdf95d6 refactor: diffTag → diffStatus 
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
 2022-10-06 13:06:31 -07:00
E.W.Ayers
506abff532 fix: replace highlight with diffTag 2022-10-06 13:06:31 -07:00
E.W.Ayers
7c8fcb3233 fix: rm instance TypeName String because it is unused 2022-10-06 11:00:43 -07:00
E.W.Ayers
7f8c45b6f3 feat: make CustomInfo use Dynamic instead of Json 
A little easier to use than the previous CustomInfo.
 2022-10-06 11:00:43 -07:00
Leonardo de Moura
9996686690 feat: display mono phase code 2022-10-06 07:48:59 -07:00
Leonardo de Moura
150022fe13 chore: update stage0 2022-10-06 07:42:24 -07:00
Leonardo de Moura
0577993d61 chore: fix tests 2022-10-06 07:41:48 -07:00
Leonardo de Moura
87caf6d38a fix: bug at toMonoType 2022-10-06 07:41:36 -07:00
Leonardo de Moura
e99ffefeda chore: update stage0 2022-10-06 07:27:47 -07:00
Leonardo de Moura
acd2836cb5 feat: add saveMono pass to normalize mono phase free variable ids 
Motivation: control .olean size
 2022-10-06 07:24:30 -07:00
Leonardo de Moura
d9fcfd71d9 fix: missing test 2022-10-06 07:18:27 -07:00
Leonardo de Moura
73ee2d92aa fix: constructor parameter validation for mono phase 2022-10-06 06:57:06 -07:00
Leonardo de Moura
faa30bccb2 feat: activate toMono compiler pass 
It increases the .olean sizes.
 2022-10-06 06:23:08 -07:00
Leonardo de Moura
80bf4f3334 fix: erase type (and type former) parameters occurrences at toMono 2022-10-06 06:23:08 -07:00
Leonardo de Moura
23182882d4 fix: erase universe levels at toMono 2022-10-06 06:23:08 -07:00
Leonardo de Moura
d409ad75b5 fix: bug at trivialStructToMono 2022-10-06 06:23:08 -07:00
Leonardo de Moura
08bfb7060d feat: add support for trivial structures, Decidable, and constructors at toMono 2022-10-06 05:33:13 -07:00
Leonardo de Moura
a0894dedbb feat: add phaseOut field to Pass 
We need it for passes that move the code from one phase to another.

See `toMono` pass.

cc @hargoniX
 2022-10-06 03:29:21 -07:00
Leonardo de Moura
b172ba8a34 feat: add toMono pass 
It has to activate by default yet.
 2022-10-05 10:39:41 -07:00
Leonardo de Moura
254e28bd99 chore: update stage0 2022-10-05 10:33:51 -07:00
Leonardo de Moura
e64e877e8f feat: add Decl.toMono skeleton 2022-10-05 10:33:01 -07:00
Leonardo de Moura
9f76da2b7f feat: add env extension for the mono phase 2022-10-05 10:31:52 -07:00
Leonardo de Moura
c6b3ebdd85 feat: detect trivial structures and add extension for storing mono phase types 2022-10-05 08:55:44 -07:00
Leonardo de Moura
00f6f83379 refactor: add BaseTypes.lean 2022-10-05 07:27:39 -07:00
Leonardo de Moura
ee59048bfb chore: remove dead declaration 
We have merged `lcErased` and `lcAny` in the new code generator.
 2022-10-05 05:17:31 -07:00
Leonardo de Moura
6288181656 chore: fix test 2022-10-05 05:01:42 -07:00
Leonardo de Moura
efc42efe49 chore: update stage0 2022-10-05 04:47:13 -07:00
Leonardo de Moura
913ca41129 refactor: merge lcAny and lcErased 
`lcErased` is a superset of `lcAny` anyway, and we didn't find ways of
using the distinction to generate better code.
 2022-10-05 04:46:52 -07:00
Leonardo de Moura
ebdbdc1043 chore: temporarily disable extendJoinPointContext 
see #1686
 2022-10-04 17:41:41 -07:00
Leonardo de Moura
f63734cba4 chore: unexpanders for Name.mkStr* and Array.mkArray* 
closes #1675
 2022-10-04 17:18:36 -07:00
Leonardo de Moura
e9d5dfc689 chore: closes #1683 2022-10-04 16:46:08 -07:00
Mario Carneiro
d56708c0e5
fix: handle multi namespace/section in foldingRange and documentSymbol (#1680) 2022-10-04 17:37:52 +00:00
Leonardo de Moura
ee603ab741 feat: sort refine new goals using the order they were created 
Potential problem: if elaboration of subterms is delayed the order the new metavariables are created may not match the order they
appear in the `.lean` file. We should tell users to prefer tagged goals.

closes #1682
 2022-10-04 06:54:14 -07:00