Leonardo de Moura
b20e208867
chore: pretty print LCNF cases result type
2022-10-09 20:13:17 -07:00
Leonardo de Moura
6f023a44ad
fix: let _x.i := _x.j simplification at LCNF simp
2022-10-09 18:38:28 -07:00
Leonardo de Moura
72d3840f0c
feat: add simpCast?
2022-10-09 18:29:12 -07:00
Leonardo de Moura
6c5475725e
feat: (lcCast _ _ g) a_1 ... a_n => g a_1 ... a_n if type correct
2022-10-09 17:45:15 -07:00
Leonardo de Moura
30bd019a7f
chore: simplify SimpValue.lean
2022-10-09 17:35:13 -07:00
Leonardo de Moura
54944819a0
feat: add simpCastCast?
2022-10-09 16:43:33 -07:00
Leonardo de Moura
cd303cd8e5
fix: do not apply simpAppApp? over cast
2022-10-09 16:43:10 -07:00
Leonardo de Moura
cf313d2101
chore: improve eqvTypes
2022-10-09 16:42:55 -07:00
Leonardo de Moura
43fe67c41a
chore: helper pass for debugging purposes
2022-10-09 16:41:54 -07:00
Leonardo de Moura
9feb4d8ab7
fix: do not generate code for [extern] functions
2022-10-09 15:35:29 -07:00
Leonardo de Moura
11fcdb7bf4
feat: add cast at exit points if necessary when inlining code
2022-10-09 13:01:10 -07:00
Leonardo de Moura
ef2d17120c
chore: fix note
2022-10-09 12:25:45 -07:00
Leonardo de Moura
cc09afc5e1
fix: type error introducing when inlining LCNF functions
...
This issue has been reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Annoying.20LCNF.20errors/near/303142516
2022-10-09 12:10:11 -07:00
Leonardo de Moura
f61ec4929f
chore: add low-level normExprCore
2022-10-09 12:10:11 -07:00
Leonardo de Moura
e81673366a
chore: remove leftover
2022-10-09 12:10:11 -07:00
Leonardo de Moura
613c8027d7
fix: missing instantiateParamsLevelParams
2022-10-09 12:10:11 -07:00
Leonardo de Moura
827ef94486
feat: add eqvTypes
2022-10-09 12:10:11 -07:00
Leonardo de Moura
c14d07fe2e
feat: include def/fun/jp resulting type in the LCNF pretty printer
2022-10-09 12:10:11 -07:00
Leonardo de Moura
eeb98d9cf4
refactor: rename FixedArgs => FixedParams
2022-10-09 12:10:11 -07:00
Leonardo de Moura
37a61568bc
feat: improve fixed parameter analyzer
2022-10-09 12:10:11 -07:00
Leonardo de Moura
8e6cb25cbf
chore: temporarily disable eager lambda lifting
...
We need a better heuristic for deciding which functions in instances
should be eagerly lambda lifted. Otherwise, it will have to keep
chasing which instances we have to annotate with `[inline]`.
2022-10-08 19:51:19 -07:00
Leonardo de Moura
1148392f45
fix: Closure.lean
2022-10-08 19:51:19 -07:00
Leonardo de Moura
2efb1dbdf1
doc: lambda lifting
2022-10-08 19:51:19 -07:00
Leonardo de Moura
b7d4fd03a3
feat: eager lambda lifting
2022-10-08 19:51:19 -07:00
Leonardo de Moura
878e72b2f9
feat: lambda lifting
2022-10-08 19:51:19 -07:00
Leonardo de Moura
3c90b2fd3e
feat: add Decl.save
2022-10-08 19:51:19 -07:00
Leonardo de Moura
56002e1b33
fix: fixes #1707
2022-10-08 07:58:56 -07:00
Leonardo de Moura
7874c03c27
chore: style
2022-10-08 07:49:27 -07:00
Leonardo de Moura
6bc4144409
fix: fixes #1549
2022-10-08 07:41:49 -07:00
Leonardo de Moura
e3ec468e3b
fix: fixes #1650
2022-10-07 19:00:23 -07:00
Leonardo de Moura
cf2ea445fe
fix: fixes #1681
2022-10-07 18:36:25 -07:00
Leonardo de Moura
79683c4bf6
chore: missing imports
2022-10-07 18:11:19 -07:00
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
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
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
Sebastian Ullrich
5b7e6661f9
chore: more RBMap cleanup
2022-10-06 17:26:43 -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
87caf6d38a
fix: bug at toMonoType
2022-10-06 07:41:36 -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
