This PR avoids match splitter calculation from testing all quadratically
many pairs of alternatives for overlaps, by keeping track of possible
overlaps during matcher calculation, storing that information in the
`MatcherInfo`, and using that during matcher calculation.
This PR fixes fallout of the closure allocator changes in #10982. As far
as we know
this bug only meaningfully manifests in non default build configurations
without mimalloc such as:
`cmake --preset release -DUSE_MIMALLOC=OFF`
The issue is that I forgot to update the deallocation functions for
closures. However, this only
seems to matter if we disable mimalloc which is why this slipped through
testing.
This PR renames `Substring` to `Substring.Raw`.
This is to signify its status as a second-class citizen (not deprecated,
but no real plans for verification, like `String.Pos.Raw`) and to free
up the name `Substring` for a possible future type `String.Substring :
String -> Type` so that `s.Substring` is the type of substrings of `s`.
The functions `String.toSubstring` and `String.toSubstring'` will remain
for now for bootstrapping reasons.
This PR implements `grind_pattern` constraints. They are useful for
controlling theorem instantiation in `grind`. As an example, consider
the following two theorems:
```lean
theorem extract_empty {start stop : Nat} :
(#[] : Array α).extract start stop = #[] := …
theorem extract_extract {as : Array α} {i j k l : Nat} :
(as.extract i j).extract k l = as.extract (i + k) (min (i + l) j) := …
```
If both are used for theorem instantiation, an unbounded number of
instances is generated as soon as we add the term `#[].extract i j` to
the `grind` context.
We can now prevent this by adding a `grind_pattern` constraint to
`extract_extract`:
```lean
grind_pattern extract_extract => (as.extract i j).extract k l where
as =/= #[]
```
With this constraint, only one instance is generated, as expected:
```lean
/-- trace: [grind.ematch.instance] extract_empty: #[].extract i j = #[] -/
#guard_msgs (drop error, trace) in
set_option trace.grind.ematch.instance true in
example (as : Array Nat) (h : #[].extract i j = as) : False := by
grind only [= extract_empty, usr extract_extract]
```
This PR adds syntax for specifying `grind_pattern` constraints and
extends the `EMatchTheorem` object.
---
Note: We need a manual stage0 update because it affects the .olean
files.
This PR fixes name mangling to be unambiguous / injective by adding `00`
for disambiguation where necessary. Additionally, the inverse function,
`Lean.Name.unmangle` has been added which can be used to unmangle a
mangled identifier. This unmangler has been added to demonstrate the
injectivity but also to allow unmangling identifiers e.g. for debugging
purposes.
Closes#10724
This PR implements zero cost `BaseIO` by erasing the `IO.RealWorld`
parameter from argument lists and structures. This is a **major breaking
change for FFI**.
Concretely:
- `BaseIO` is defined in terms of `ST IO.RealWorld`
- `EIO` (and thus `IO`) is defined in terms of `EST IO.RealWorld`
- The opaque `Void` type is introduced and the trivial structure
optimization updated to account for it. Furthermore, arguments of type
`Void s` are removed from the argument lists of the C functions.
- `ST` is redefined as `Void s -> ST.Out s a` where `ST.Out` is a pair
of `Void s` and `a`
This together has the following major effects on our generated code:
- Functions that return `BaseIO`/`ST`/`EIO`/`IO`/`EST` now do not take
the dummy world parameter anymore. To account for this FFI code needs to
delete the dummy world parameter from the argument lists.
- Functions that return `BaseIO`/`ST` now return their wrapped value
directly. In particular `BaseIO UInt32` now returns a `uint32_t` instead
of a `lean_object*`. To account for this FFI code might have to change
the return type and does not need to call `lean_io_result_mk_ok` anymore
but can instead just `return` values right away (same with extracting
values from `BaseIO` computations.
- Functions that return `EIO`/`IO`/`EST` now only return the equivalent
of an `Except` node which reduces the allocation size. The
`lean_io_result_mk_ok`/`lean_io_result_mk_error` functions were updated
to account for this already so no change is required.
Besides improving performance by dropping allocation (sizes) we can now
also do fun new things such as:
```lean
@[extern "malloc"]
opaque malloc (size : USize) : BaseIO USize
```
This PR follows upon #10606 and creates equational theorems uniformly
from the unfold theorem, there is only one handler registered in
`registerGetEqnsFn`.
For now we keep `registerGetEqnsFn`, because it’s used by mathlib’s
`irreducible_def`, but I’d like to get rid of it in the long term,
relying only on `registerGetUnfoldEqnFn` for constructions that should
unfold differently.
This PR adds a new helper parser for implementing parsers that contain
hexadecimal numbers. We are going to use it to implement anchors in the
`grind` interactive mode.
This PR changes how Lean proves the equational theorems for structural
recursion. The core idea is to let-bind the `f` argument to `brecOn` and
rewriting `.brecOn` with an unfolding theorem. This means no extra case
split for the `.rec` in `.brecOn` is needed, and `simp` doesn't change
the `f` argument which can break the definitional equality with the
defined function. With this, we can prove the unfolding theorem first,
and derive the equational theorems from that, like for all other ways of
defining recursive functions.
Backs out the changes from #10415, the old strategy works well with the
new goals.
Fixes#5667Fixes#10431Fixes#10195Fixes#2962
This PR ensures that even if a type is marked as `irreducible` the
compiler can see through it in
order to discover functions hidden behind type aliases.
This PR adds infrastructure for the upcoming `grind` tactic mode, which
will be similar to the `conv` mode. The goal is to extend `grind` from a
terminal tactic into an interactive mode: `grind => …`.
It will serve as the foundation for `ungrind`, the process of converting
an expensive (and potentially fragile) `grind` proof into a robust
script. This mode will include tactics for expensive reasoning steps
such as cutsat model-based search, Gröbner basis computation,
E-matching, case splits, and more.
It will also provide robust, succinct references to facts and terms:
labels, structural matches, and anchors (e.g., `#abcd`).
This PR adds a docstring role for module names, called `module`. It also
improves the suggestions provided for code elements, making them more
relevant and proposing `lit`.
This PR implements module docstrings in Verso syntax, as well as adding
a number of improvements and fixes to Verso docstrings in general. In
particular, they now have language server support and are parsed at
parse time rather than elaboration time, so the snapshot's syntax tree
includes the parsed documentation.
