Commit graph

27 commits

Author SHA1 Message Date
Leonardo de Moura
514a5fddc6
refactor: DiscrTree (#11875)
This PR adds the directory `Meta/DiscrTree` and reorganizes the code
into different files. Motivation: we are going to have new functions for
retrieving simplification theorems for the new structural simplifier.
2026-01-02 19:53:45 +00:00
Henrik Böving
b8c53b1d29
chore: remove IR elim dead branches (#11576)
This PR removes the old ElimDeadBranches pass and shifts the new one
past lambda lifting.

The reason for dropping the old one is its general unsoundness and the
fact that we want to do refactorings on the IR part. The reason for
shifting the current pass past lambda lifting, is that its analysis is
imprecise in the presence of local function symbols. I experimented with
the exact placement for a while and it seems like it is optimal here.
Overall we observe a slight regression in the amount of C code
generated, likely because we don't propagate information into lambdas
before lifting them anymore. But generally measure a slight performance
improvement in general.
2025-12-11 10:39:02 +00:00
Joachim Breitner
63bd0b5e77
refactor: introduce Match.altInfos (#11256)
This PR replaces `MatcherInfo.numAltParams` with a more detailed data
structure that allows us, in particular, to distinguish between an
alternative for a constructor with a `Unit` field and the alternative
for a nullary constructor, where an artificial `Unit` argument is
introduced.
2025-11-19 15:09:17 +00:00
Sebastian Ullrich
428355cf02
chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Leonardo de Moura
8c4db341dd
chore: use ofConstName in error messages (#10121) 2025-08-25 23:20:36 +00:00
Sebastian Ullrich
ff1d3138bf
refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Paul Reichert
6e538c35dd
refactor: migrate all usages of old slice notation (#9000)
This PR replaces all usages of `[:]` slice notation in `src` with the
new `[...]` notation in production code, tests and comments. The
underlying implementation of the `Subarray` functions stays the same.

Notation cheat sheet:

* `*...*` is the doubly-unbounded range.
* `*...a` or `*...<a` contains all elements that are less than `a`.
* `*...=a` contains all elements that are less than or equal to `a`.
* `a...*` contains all elements that are greater than or equal to `a`.
* `a...b` or `a...<b` contains all elements that are greater than or
equal to `a` and less than `b`.
* `a...=b` contains all elements that are greater than or equal to `a`
and less than or equal to `b`.
* `a<...*` contains all elements that are greater than `a`.
* `a<...b` or `a<...<b` contains all elements that are greater than `a`
and less than `b`.
* `a<...=b` contains all elements that are greater than `a` and less
than or equal to `b`.

Benchmarks have shown that importing the iterator-backed parts of the
polymorphic slice library in `Init` impacts build performance. This PR
avoids this problem by separating those parts of the library that do not
rely on iterators from those those that do. Whereever the new slice
notation is used, only the iterator-independent files are imported.
2025-06-27 18:52:07 +00:00
Cameron Zwarich
9f65d0251a
chore: remove comments about missing functionality now implemented elsewhere (#8732) 2025-06-12 00:38:42 +00:00
Cameron Zwarich
c633725b3e
fix: add support for the init attribute to the new compiler (#8125)
This PR adds support for the `init` attribute to the new compiler.
2025-04-27 01:01:44 +00:00
Cameron Zwarich
bf1d253764
feat: add support for extern LCNF decls (#6429)
This PR adds support for extern LCNF decls, which is required for parity
with the existing code generator.
2024-12-20 21:20:56 +00:00
Leonardo de Moura
f790b1999f
fix: new code generator must generate code for opaque declarations that are not @[extern] (#6383)
This PR ensures the new code generator produces code for `opaque`
definitions that are not tagged as `@[extern]`.
Remark: This is the behavior of the old code generator.
2024-12-14 20:26:14 +00:00
Joachim Breitner
60096e7d15
refactor: more idiomatic syntax for if h: (#5567)
https://github.com/leanprover/lean4/pull/5552 introduced a fair number
of `if h:`, but the slightly preferred style is `if h :`, with a space,
so here goes a quick `sed`.
2024-10-01 15:23:54 +00:00
TomasPuverle
ddec5336e5
chore: switch obvious cases of array "bang"[]! indexing to rely on hypothesis (#5552)
Update certain uses of `arr[i]!` to use the "provably correct" version
`arr[i]`, in order to use "best practices".

Some motivation and discussion on
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lean.20compiler.2Felaborator.20development.20question/near/472934715)
2024-10-01 11:12:22 +00:00
Henrik Böving
23e49eb519 perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Mario Carneiro
dd5948d641 chore: snake-case attributes (part 1) 2022-10-19 09:28:08 -07:00
Leonardo de Moura
af99715a58 feat: store inline attribute at LCNF declarations
This commit also adds support for inheriting the inline attribute when
the compiler lambda lifts local functions from instances.
2022-10-13 02:06:35 -07:00
Leonardo de Moura
4c2c6931f4 feat: add flag at LCNF Decl indicating whether the original Lean declaration was declared using partial or unsafe 2022-09-30 19:28:05 -07:00
Leonardo de Moura
ba619be393 fix: apply macroInline again after inlineMatchers 2022-09-26 07:31:27 -07:00
Leonardo de Moura
7d583f9543 fix: convert _unsafe_rec to original name 2022-09-24 08:19:41 -07:00
Leonardo de Moura
e4f0f4b794 fix: shouldGenerateCode fix for axiom 2022-09-23 14:25:48 -07:00
Leonardo de Moura
c1b7accd12 refactor: LCNF local context
The previous implementation had a few issues:
- Function (and join point) declarations were being inserted into two different hashmaps.
- `borrow` information was not available for parameters.
- No proper erase functions.
2022-09-14 19:25:16 -07:00
Leonardo de Moura
9e5a818de5 fix: bug at LCNF toDecl 2022-09-14 15:23:34 -07:00
Leonardo de Moura
a40118c79d chore: disable eager applyCasesOnImplementedBy
It must be performed at phase 2.
We still want to perform the regular `[implementedBy]` replacements at
phase 1 since they affect code specialization.
2022-09-08 14:50:27 -07:00
Leonardo de Moura
07bdab45d2 feat: apply casesOn implementedBy replacements 2022-09-07 20:37:09 -07:00
Leonardo de Moura
ddab48a154 fix: erase dead variables 2022-08-31 20:43:13 -07:00
Sebastian Ullrich
e81ba951c6 fix: Core.transform API and uses 2022-08-25 19:07:42 -07:00
Leonardo de Moura
f2f3a72196 feat: add ToDecl.lean 2022-08-24 08:31:38 -07:00