Compare commits

..

1 Commits

Author SHA1 Message Date
Leonardo de Moura
7786813bef chore: remove dead code at Structure.lean 2024-04-27 15:54:12 -07:00
603 changed files with 2193 additions and 8320 deletions

View File

@@ -11,7 +11,7 @@ assignees: ''
* [ ] Put an X between the brackets on this line if you have done all of the following:
* Check that your issue is not already [filed](https://github.com/leanprover/lean4/issues).
* Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
* Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.
### Description

View File

@@ -54,10 +54,7 @@ jobs:
with:
script: |
const quick = ${{ steps.set-quick.outputs.quick }};
console.log(`quick: ${quick}`);
// use large runners outside PRs where available (original repo)
// disabled for now as this mostly just speeds up the test suite which is not a bottleneck
// let large = ${{ github.event_name != 'pull_request' && github.repository == 'leanprover/lean4' }} ? "-large" : "";
console.log(`quick: ${quick}`)
let matrix = [
{
// portable release build: use channel with older glibc (2.27)

View File

@@ -126,11 +126,11 @@ jobs:
if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
echo "The merge base of this PR coincides with the nightly release"
BATTERIES_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/batteries.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
STD_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/std4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
if [[ -n "$BATTERIES_REMOTE_TAGS" ]]; then
echo "... and Batteries has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
if [[ -n "$STD_REMOTE_TAGS" ]]; then
echo "... and Std has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE=""
if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
@@ -140,8 +140,8 @@ jobs:
MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
fi
else
echo "... but Batteries does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE="- ❗ Batteries CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Batteries CI should run now."
echo "... but Std does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE="- ❗ Std CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Std CI should run now."
fi
else
@@ -151,7 +151,7 @@ jobs:
git -C lean4.git fetch origin nightly-with-mathlib
NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "origin/nightly-with-mathlib")"
MESSAGE="- ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`."
MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`."
fi
if [[ -n "$MESSAGE" ]]; then
@@ -223,27 +223,27 @@ jobs:
description: description,
});
# We next automatically create a Batteries branch using this toolchain.
# Batteries doesn't itself have a mechanism to report results of CI from this branch back to Lean
# Instead this is taken care of by Mathlib CI, which will fail if Batteries fails.
# We next automatically create a Std branch using this toolchain.
# Std doesn't itself have a mechanism to report results of CI from this branch back to Lean
# Instead this is taken care of by Mathlib CI, which will fail if Std fails.
- name: Cleanup workspace
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
run: |
sudo rm -rf ./*
# Checkout the Batteries repository with all branches
- name: Checkout Batteries repository
# Checkout the Std repository with all branches
- name: Checkout Std repository
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
uses: actions/checkout@v3
with:
repository: leanprover-community/batteries
repository: leanprover/std4
token: ${{ secrets.MATHLIB4_BOT }}
ref: nightly-testing
fetch-depth: 0 # This ensures we check out all tags and branches.
- name: Check if tag exists
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
id: check_batteries_tag
id: check_std_tag
run: |
git config user.name "leanprover-community-mathlib4-bot"
git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
@@ -251,7 +251,7 @@ jobs:
if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
else
echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Batteries. Falling back to 'nightly-testing'."
echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Std. Falling back to 'nightly-testing'."
BASE=nightly-testing
fi
@@ -268,7 +268,7 @@ jobs:
else
echo "Branch already exists, pushing an empty commit."
git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
# The Batteries `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
# The Std `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
# (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
@@ -321,7 +321,7 @@ jobs:
git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain
git add lean-toolchain
sed -i "s/require batteries from git \"https:\/\/github.com\/leanprover-community\/batteries\" @ \".\+\"/require batteries from git \"https:\/\/github.com\/leanprover-community\/batteries\" @ \"nightly-testing-${MOST_RECENT_NIGHTLY}\"/" lakefile.lean
sed -i "s/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \".\+\"/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \"nightly-testing-${MOST_RECENT_NIGHTLY}\"/" lakefile.lean
git add lakefile.lean
git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
else

View File

@@ -22,4 +22,4 @@ Please read our [Contribution Guidelines](CONTRIBUTING.md) first.
# Building from Source
See [Building Lean](https://lean-lang.org/lean4/doc/make/index.html) (documentation source: [doc/make/index.md](doc/make/index.md)).
See [Building Lean](https://lean-lang.org/lean4/doc/make/index.html).

View File

@@ -8,10 +8,7 @@ This file contains work-in-progress notes for the upcoming release, as well as p
Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
of each version.
v4.9.0 (development in progress)
---------
v4.8.0
v4.8.0 (development in progress)
---------
* **Executables configured with `supportInterpreter := true` on Windows should now be run via `lake exe` to function properly.**
@@ -88,8 +85,6 @@ v4.8.0
[#3798](https://github.com/leanprover/lean4/pull/3798) and
[#3978](https://github.com/leanprover/lean4/pull/3978).
* Hovers for terms in `match` expressions in the Infoview now reliably show the correct term.
* Added `@[induction_eliminator]` and `@[cases_eliminator]` attributes to be able to define custom eliminators
for the `induction` and `cases` tactics, replacing the `@[eliminator]` attribute.
Gives custom eliminators for `Nat` so that `induction` and `cases` put goal states into terms of `0` and `n + 1`

View File

@@ -1,4 +1,4 @@
open Batteries
open Std
open Lean
inductive BoolExpr where

View File

@@ -84,12 +84,10 @@ gh workflow run update-stage0.yml
Leaving stage0 updates to the CI automation is preferable, but should you need
to do it locally, you can use `make update-stage0-commit` in `build/release` to
update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to
update from another stage. This command will automatically stage the updated files
and introduce a commit,so make sure to commit your work before that.
update from another stage.
If you rebased the branch (either onto a newer version of `master`, or fixing
up some commits prior to the stage0 update, recreate the stage0 update commits.
The script `script/rebase-stage0.sh` can be used for that.
This command will automatically stage the updated files and introduce a commit,
so make sure to commit your work before that.
The CI should prevent PRs with changes to stage0 (besides `stdlib_flags.h`)
from entering `master` through the (squashing!) merge queue, and label such PRs
@@ -97,7 +95,6 @@ with the `changes-stage0` label. Such PRs should have a cleaned up history,
with separate stage0 update commits; then coordinate with the admins to merge
your PR using rebase merge, bypassing the merge queue.
## Further Bootstrapping Complications
As written above, changes in meta code in the current stage usually will only

View File

@@ -53,59 +53,10 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
Its runtime value is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number (`lean_box`/`lean_unbox`).
* A universe `Sort u`, type constructor `... → Sort u`, or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
* Any other type is represented by `lean_object *`.
Its runtime value is a pointer to an object of a subtype of `lean_object` (see the "Inductive types" section below) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
Its runtime value is a pointer to an object of a subtype of `lean_object` (see respective declarations in `lean.h`) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
Example: the runtime value of `u : Unit` is always `lean_box(0)`.
#### Inductive types
For inductive types which are in the fallback `lean_object *` case above and not trivial constructors, the type is stored as a `lean_ctor_object`, and `lean_is_ctor` will return true. A `lean_ctor_object` stores the constructor index in the header, and the fields are stored in the `m_objs` portion of the object.
The memory order of the fields is derived from the types and order of the fields in the declaration. They are ordered as follows:
* Non-scalar fields stored as `lean_object *`
* Fields of type `USize`
* Other scalar fields, in decreasing order by size
Within each group the fields are ordered in declaration order. **Warning**: Trivial wrapper types still count toward a field being treated as non-scalar for this purpose.
* To access fields of the first kind, use `lean_ctor_get(val, i)` to get the `i`th non-scalar field.
* To access `USize` fields, use `lean_ctor_get_usize(val, n+i)` to get the `i`th usize field and `n` is the total number of fields of the first kind.
* To access other scalar fields, use `lean_ctor_get_uintN(val, off)` or `lean_ctor_get_usize(val, off)` as appropriate. Here `off` is the byte offset of the field in the structure, starting at `n*sizeof(void*)` where `n` is the number of fields of the first two kinds.
For example, a structure such as
```lean
structure S where
ptr_1 : Array Nat
usize_1 : USize
sc64_1 : UInt64
ptr_2 : { x : UInt64 // x > 0 } -- wrappers don't count as scalars
sc64_2 : Float -- `Float` is 64 bit
sc8_1 : Bool
sc16_1 : UInt16
sc8_2 : UInt8
sc64_3 : UInt64
usize_2 : USize
ptr_3 : Char -- trivial wrapper around `UInt32`
sc32_1 : UInt32
sc16_2 : UInt16
```
would get re-sorted into the following memory order:
* `S.ptr_1` - `lean_ctor_get(val, 0)`
* `S.ptr_2` - `lean_ctor_get(val, 1)`
* `S.ptr_3` - `lean_ctor_get(val, 2)`
* `S.usize_1` - `lean_ctor_get_usize(val, 3)`
* `S.usize_2` - `lean_ctor_get_usize(val, 4)`
* `S.sc64_1` - `lean_ctor_get_uint64(val, sizeof(void*)*5)`
* `S.sc64_2` - `lean_ctor_get_float(val, sizeof(void*)*5 + 8)`
* `S.sc64_3` - `lean_ctor_get_uint64(val, sizeof(void*)*5 + 16)`
* `S.sc32_1` - `lean_ctor_get_uint32(val, sizeof(void*)*5 + 24)`
* `S.sc16_1` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 28)`
* `S.sc16_2` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 30)`
* `S.sc8_1` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 32)`
* `S.sc8_2` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 33)`
### Borrowing
By default, all `lean_object *` parameters of an `@[extern]` function are considered *owned*, i.e. the external code is passed a "virtual RC token" and is responsible for passing this token along to another consuming function (exactly once) or freeing it via `lean_dec`.

View File

@@ -50,13 +50,13 @@ We'll use `v4.6.0` as the intended release version as a running example.
- Toolchain bump PR
- Create and push the tag
- Merge the tag into `stable`
- [Batteries](https://github.com/leanprover-community/batteries)
- [Std](https://github.com/leanprover-community/std4)
- No dependencies
- Toolchain bump PR
- Create and push the tag
- Merge the tag into `stable`
- [ProofWidgets4](https://github.com/leanprover-community/ProofWidgets4)
- Dependencies: `Batteries`
- Dependencies: `Std`
- Note on versions and branches:
- `ProofWidgets` uses a sequential version tagging scheme, e.g. `v0.0.29`,
which does not refer to the toolchain being used.
@@ -65,7 +65,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
- Toolchain bump PR
- Create and push the tag, following the version convention of the repository
- [Aesop](https://github.com/leanprover-community/aesop)
- Dependencies: `Batteries`
- Dependencies: `Std`
- Toolchain bump PR including updated Lake manifest
- Create and push the tag
- Merge the tag into `stable`
@@ -79,7 +79,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
- Create and push the tag
- There is no `stable` branch; skip this step
- [Mathlib](https://github.com/leanprover-community/mathlib4)
- Dependencies: `Aesop`, `ProofWidgets4`, `lean4checker`, `Batteries`, `doc-gen4`, `import-graph`
- Dependencies: `Aesop`, `ProofWidgets4`, `lean4checker`, `Std`, `doc-gen4`, `import-graph`
- Toolchain bump PR notes:
- In addition to updating the `lean-toolchain` and `lakefile.lean`,
in `.github/workflows/build.yml.in` in the `lean4checker` section update the line
@@ -123,8 +123,8 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
- Decide which nightly release you want to turn into a release candidate.
We will use `nightly-2024-02-29` in this example.
- It is essential that Batteries and Mathlib already have reviewed branches compatible with this nightly.
- Check that both Batteries and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29`
- It is essential that Std and Mathlib already have reviewed branches compatible with this nightly.
- Check that both Std and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29`
in their `lean-toolchain`.
- The steps required to reach that state are beyond the scope of this checklist, but see below!
- Create the release branch from this nightly tag:
@@ -182,7 +182,7 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
- We do this for the same list of repositories as for stable releases, see above.
As above, there are dependencies between these, and so the process above is iterative.
It greatly helps if you can merge the `bump/v4.7.0` PRs yourself!
- For Batteries/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag
- For Std/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag
`nightly-testing-2024-02-29` with date corresponding to the nightly used for the release
(create it if not), and then on the `nightly-testing` branch `git reset --hard master`, and force push.
- Make an announcement!
@@ -204,7 +204,7 @@ In particular, updating the downstream repositories is significantly more work
# Preparing `bump/v4.7.0` branches
While not part of the release process per se,
this is a brief summary of the work that goes into updating Batteries/Aesop/Mathlib to new versions.
this is a brief summary of the work that goes into updating Std/Aesop/Mathlib to new versions.
Please read https://leanprover-community.github.io/contribute/tags_and_branches.html

View File

@@ -15,7 +15,7 @@ data type containing several important pieces of information. First and foremost
current player, and it has a random generator.
-/
open Batteries (HashMap)
open Std (HashMap)
abbrev TileIndex := Nat × Nat -- a 2D index
inductive TileState where

View File

@@ -180,7 +180,7 @@ rec {
update-stage0 =
let cTree = symlinkJoin { name = "cs"; paths = [ Init.cTree Lean.cTree ]; }; in
writeShellScriptBin "update-stage0" ''
CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"}
CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/update-stage0"}
'';
update-stage0-commit = writeShellScriptBin "update-stage0-commit" ''
set -euo pipefail

View File

@@ -1,2 +0,0 @@
This directory contains various scripts that are *not* meant to be called
directly, but through other scripts or makefiles.

View File

@@ -1,19 +0,0 @@
#!/usr/bin/env bash
# Script internal to `./script/rebase-stage0.sh`
# Determine OS type for sed in-place editing
SED_CMD=("sed" "-i")
if [[ "$OSTYPE" == "darwin"* ]]
then
# macOS requires an empty string argument with -i for in-place editing
SED_CMD=("sed" "-i" "")
fi
if [ "$STAGE0_WITH_NIX" = true ]
then
"${SED_CMD[@]}" '/chore: update stage0/ s,.*,x nix run .#update-stage0-commit,' "$1"
else
"${SED_CMD[@]}" '/chore: update stage0/ s,.*,x make -j32 -C build/release update-stage0 \&\& git commit -m "chore: update stage0",' "$1"
fi

View File

@@ -1,24 +0,0 @@
#!/usr/bin/env bash
# This script rebases onto the given branch/commit, and updates
# all `chore: update stage0` commits along the way.
# Whether to use nix or make to update stage0
if [ "$1" = "-nix" ]
then
export STAGE0_WITH_NIX=true
shift
fi
# Check if an argument is provided
if [ "$#" -eq 0 ]; then
echo "Usage: $0 [-nix] <options to git rebase -i>"
exit 1
fi
REPO_ROOT=$(git rev-parse --show-toplevel)
# Run git rebase in interactive mode, but automatically edit the todo list
# using the defined GIT_SEQUENCE_EDITOR command
GIT_SEQUENCE_EDITOR="$REPO_ROOT/script/lib/rebase-editor.sh" git rebase -i "$@"

View File

@@ -9,7 +9,7 @@ endif()
include(ExternalProject)
project(LEAN CXX C)
set(LEAN_VERSION_MAJOR 4)
set(LEAN_VERSION_MINOR 9)
set(LEAN_VERSION_MINOR 8)
set(LEAN_VERSION_PATCH 0)
set(LEAN_VERSION_IS_RELEASE 0) # This number is 1 in the release revision, and 0 otherwise.
set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -315,12 +315,6 @@ endif()
string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
# in local builds, link executables and not just dynlibs against C++ stdlib as well,
# which is required for e.g. asan
if(NOT LEAN_STANDALONE)
string(APPEND CMAKE_EXE_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
endif()
# flags for user binaries = flags for toolchain binaries + Lake
string(APPEND LEANC_STATIC_LINKER_FLAGS " ${TOOLCHAIN_STATIC_LINKER_FLAGS} -lLake")
@@ -591,7 +585,7 @@ endif()
if(PREV_STAGE)
add_custom_target(update-stage0
COMMAND bash -c 'CSRCS=${CMAKE_BINARY_DIR}/lib/temp script/lib/update-stage0'
COMMAND bash -c 'CSRCS=${CMAKE_BINARY_DIR}/lib/temp script/update-stage0'
DEPENDS make_stdlib
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/..")

View File

@@ -63,16 +63,3 @@ theorem ite_some_none_eq_none [Decidable P] :
@[simp] theorem ite_some_none_eq_some [Decidable P] :
(if P then some x else none) = some y P x = y := by
split <;> simp_all
-- This is not marked as `simp` as it is already handled by `dite_eq_right_iff`.
theorem dite_some_none_eq_none [Decidable P] {x : P α} :
(if h : P then some (x h) else none) = none ¬P := by
simp only [dite_eq_right_iff]
rfl
@[simp] theorem dite_some_none_eq_some [Decidable P] {x : P α} {y : α} :
(if h : P then some (x h) else none) = some y h : P, x h = y := by
by_cases h : P <;> simp only [h, dite_cond_eq_true, dite_cond_eq_false, Option.some.injEq,
false_iff, not_exists]
case pos => exact fun h_eq Exists.intro h h_eq, fun h_exists => h_exists.2
case neg => exact fun h_false _ h_false

View File

@@ -1114,6 +1114,9 @@ theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a := by
cases a
exact rfl
instance {α : Type u} {p : α Prop} {a : α} (h : p a) : Inhabited {x // p x} where
default := a, h
instance {α : Type u} {p : α Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
fun a, h₁ b, h₂ =>
if h : a = b then isTrue (by subst h; exact rfl)

View File

@@ -31,7 +31,6 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
go (i : Nat) (acc : Array α) : Array α :=
if h : i < n then go (i+1) (acc.push (f i, h)) else acc
termination_by n - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
/-- The array `#[0, 1, ..., n - 1]`. -/
def range (n : Nat) : Array Nat :=
@@ -44,7 +43,7 @@ instance : EmptyCollection (Array α) := ⟨Array.empty⟩
instance : Inhabited (Array α) where
default := Array.empty
@[simp] def isEmpty (a : Array α) : Bool :=
def isEmpty (a : Array α) : Bool :=
a.size = 0
def singleton (v : α) : Array α :=
@@ -53,7 +52,7 @@ def singleton (v : α) : Array α :=
/-- Low-level version of `fget` which is as fast as a C array read.
`Fin` values are represented as tag pointers in the Lean runtime. Thus,
`fget` may be slightly slower than `uget`. -/
@[extern "lean_array_uget", simp]
@[extern "lean_array_uget"]
def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
a[i.toNat]
@@ -307,7 +306,6 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
else
pure r
termination_by as.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
map 0 (mkEmpty as.size)
@[inline]
@@ -380,7 +378,6 @@ def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
else
pure false
termination_by stop - j
decreasing_by simp_wf; decreasing_trivial_pre_omega
loop start
if h : stop as.size then
any stop h
@@ -466,7 +463,6 @@ def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
if p as[j] then some j else loop (j + 1)
else none
termination_by as.size - j
decreasing_by simp_wf; decreasing_trivial_pre_omega
loop 0
def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
@@ -561,7 +557,6 @@ def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : αα → Bool) (
else
true
termination_by a.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
@[inline] def isEqv (a b : Array α) (p : α α Bool) : Bool :=
if h : a.size = b.size then
@@ -666,7 +661,6 @@ def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size)
else indexOfAux a v (i+1)
else none
termination_by a.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
indexOfAux a v 0
@@ -709,7 +703,6 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
else
as
termination_by as.size
decreasing_by simp_wf; decreasing_trivial_pre_omega
def takeWhile (p : α Bool) (as : Array α) : Array α :=
let rec go (i : Nat) (r : Array α) : Array α :=
@@ -722,7 +715,6 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
else
r
termination_by as.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
go 0 #[]
/-- Remove the element at a given index from an array without bounds checks, using a `Fin` index.
@@ -733,15 +725,16 @@ def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
if h : i.val + 1 < a.size then
let a' := a.swap i.val + 1, h i
let i' : Fin a'.size := i.val + 1, by simp [a', h]
have : a'.size - i' < a.size - i := by
simp [a', Nat.sub_succ_lt_self _ _ i.isLt]
a'.feraseIdx i'
else
a.pop
termination_by a.size - i.val
decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt
theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
induction a, i using Array.feraseIdx.induct with
| @case1 a i h a' _ ih =>
| @case1 a i h a' _ _ ih =>
unfold feraseIdx
simp [h, a', ih]
| case2 a i h =>
@@ -770,7 +763,6 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
else
as
termination_by j.1
decreasing_by simp_wf; decreasing_trivial_pre_omega
let j := as.size
let as := as.push a
loop as j, size_push .. j.lt_succ_self
@@ -824,7 +816,6 @@ def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : N
else
true
termination_by as.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
/-- Return true iff `as` is a prefix of `bs`.
That is, `bs = as ++ t` for some `t : List α`.-/
@@ -846,7 +837,6 @@ private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
else
true
termination_by as.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
def allDiff [BEq α] (as : Array α) : Bool :=
allDiffAux as 0
@@ -862,7 +852,6 @@ def allDiff [BEq α] (as : Array α) : Bool :=
else
cs
termination_by as.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
@[inline] def zipWith (as : Array α) (bs : Array β) (f : α β γ) : Array γ :=
zipWithAux f as bs 0 #[]

View File

@@ -48,7 +48,6 @@ where
let b f as[i]
go (i+1) acc.val.push b, by simp [acc.property] hlt
termination_by as.size - i
decreasing_by decreasing_trivial_pre_omega
@[inline] private unsafe def mapMonoMImp [Monad m] (as : Array α) (f : α m α) : m (Array α) :=
go 0 as

View File

@@ -21,8 +21,6 @@ theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size)
subst heq
exact absurd (Nat.lt_of_lt_of_le high low) (Nat.lt_irrefl j)
termination_by a.size - i
decreasing_by decreasing_trivial_pre_omega
theorem eq_of_isEqv [DecidableEq α] (a b : Array α) : Array.isEqv a b (fun x y => x = y) a = b := by
simp [Array.isEqv]
@@ -39,7 +37,6 @@ theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) : Array.isEqvAux
case inl h => simp [h, isEqvAux_self a (i+1)]
case inr h => simp [h]
termination_by a.size - i
decreasing_by decreasing_trivial_pre_omega
theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (fun x y => x = y) = true := by
simp [isEqv, isEqvAux_self]

View File

@@ -21,13 +21,6 @@ namespace Array
attribute [simp] data_toArray uset
@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
@[simp] theorem toArray_data : (a : Array α) a.data.toArray = a
| l => ext' (data_toArray l)
@[simp] theorem data_length {l : Array α} : l.data.length = l.size := rfl
@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
@@ -138,7 +131,6 @@ where
simp [aux (i+1), map_eq_pure_bind]; rfl
· rw [List.drop_length_le (Nat.ge_of_not_lt _)]; rfl
termination_by arr.size - i
decreasing_by decreasing_trivial_pre_omega
@[simp] theorem map_data (f : α β) (arr : Array α) : (arr.map f).data = arr.data.map f := by
rw [map, mapM_eq_foldlM]
@@ -148,8 +140,7 @@ where
simp [H]
@[simp] theorem size_map (f : α β) (arr : Array α) : (arr.map f).size = arr.size := by
simp only [ data_length]
simp
simp [size]
@[simp] theorem pop_data (arr : Array α) : arr.pop.data = arr.data.dropLast := rfl
@@ -316,749 +307,5 @@ termination_by n - i
(ofFn f)[i] = f i, size_ofFn f h :=
getElem_ofFn_go _ _ _ (by simp) (by simp) nofun
/-- # mkArray -/
@[simp] theorem mkArray_data (n : Nat) (v : α) : (mkArray n v).data = List.replicate n v := rfl
@[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
(mkArray n v)[i] = v := by simp [Array.getElem_eq_data_get]
/-- # mem -/
theorem mem_data {a : α} {l : Array α} : a l.data a l := (mem_def _ _).symm
theorem not_mem_nil (a : α) : ¬ a #[] := nofun
/-- # get lemmas -/
theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] l := by
erw [Array.mem_def, getElem_eq_data_get]
apply List.get_mem
theorem getElem_fin_eq_data_get (a : Array α) (i : Fin _) : a[i] = a.data.get i := rfl
@[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
a[i] = a[i.toNat] := rfl
theorem getElem?_eq_getElem (a : Array α) (i : Nat) (h : i < a.size) : a[i]? = a[i] :=
getElem?_pos ..
theorem get?_len_le (a : Array α) (i : Nat) (h : a.size i) : a[i]? = none := by
simp [getElem?_neg, h]
theorem getElem_mem_data (a : Array α) (h : i < a.size) : a[i] a.data := by
simp only [getElem_eq_data_get, List.get_mem]
theorem getElem?_eq_data_get? (a : Array α) (i : Nat) : a[i]? = a.data.get? i := by
by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]; rfl
theorem get?_eq_data_get? (a : Array α) (i : Nat) : a.get? i = a.data.get? i :=
getElem?_eq_data_get? ..
theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
simp [get!_eq_getD]
@[simp] theorem back_eq_back? [Inhabited α] (a : Array α) : a.back = a.back?.getD default := by
simp [back, back?]
@[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
simp [back?, getElem?_eq_data_get?]
theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
theorem get?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
(a.push x)[i]? = some a[i] := by
rw [getElem?_pos, get_push_lt]
theorem get?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x := by
rw [getElem?_pos, get_push_eq]
theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]? := by
match Nat.lt_trichotomy i a.size with
| Or.inl g =>
have h1 : i < a.size + 1 := by omega
have h2 : i a.size := by omega
simp [getElem?, size_push, g, h1, h2, get_push_lt]
| Or.inr (Or.inl heq) =>
simp [heq, getElem?_pos, get_push_eq]
| Or.inr (Or.inr g) =>
simp only [getElem?, size_push]
have h1 : ¬ (i < a.size) := by omega
have h2 : ¬ (i < a.size + 1) := by omega
have h3 : i a.size := by omega
simp [h1, h2, h3]
@[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by
simp only [getElem?, Nat.lt_irrefl, dite_false]
@[simp] theorem data_set (a : Array α) (i v) : (a.set i v).data = a.data.set i.1 v := rfl
theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
(a.set i v)[i.1] = v := by
simp only [set, getElem_eq_data_get, List.get_set_eq]
theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
(a.set i v)[i.1]? = v := by simp [getElem?_pos, i.2]
@[simp] theorem get?_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α)
(h : i.1 j) : (a.set i v)[j]? = a[j]? := by
by_cases j < a.size <;> simp [getElem?_pos, getElem?_neg, *]
theorem get?_set (a : Array α) (i : Fin a.size) (j : Nat) (v : α) :
(a.set i v)[j]? = if i.1 = j then some v else a[j]? := by
if h : i.1 = j then subst j; simp [*] else simp [*]
theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v : α) :
(a.set i v)[j]'(by simp [*]) = if i = j then v else a[j] := by
if h : i.1 = j then subst j; simp [*] else simp [*]
@[simp] theorem get_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size)
(h : i.1 j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
simp only [set, getElem_eq_data_get, List.get_set_ne _ h]
theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
(setD a i v)[i] = v := by
simp at h
simp only [setD, h, dite_true, get_set, ite_true]
theorem set_set (a : Array α) (i : Fin a.size) (v v' : α) :
(a.set i v).set i, by simp [i.2] v' = a.set i v' := by simp [set, List.set_set]
private theorem fin_cast_val (e : n = n') (i : Fin n) : e i = i.1, e i.2 := by cases e; rfl
theorem swap_def (a : Array α) (i j : Fin a.size) :
a.swap i j = (a.set i (a.get j)).set j.1, by simp [j.2] (a.get i) := by
simp [swap, fin_cast_val]
theorem data_swap (a : Array α) (i j : Fin a.size) :
(a.swap i j).data = (a.data.set i (a.get j)).set j (a.get i) := by simp [swap_def]
theorem get?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]? =
if j = k then some a[i.1] else if i = k then some a[j.1] else a[k]? := by
simp [swap_def, get?_set, getElem_fin_eq_data_get]
@[simp] theorem swapAt_def (a : Array α) (i : Fin a.size) (v : α) :
a.swapAt i v = (a[i.1], a.set i v) := rfl
-- @[simp] -- FIXME: gives a weird linter error
theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
a.swapAt! i v = (a[i], a.set i, h v) := by simp [swapAt!, h]
@[simp] theorem data_pop (a : Array α) : a.pop.data = a.data.dropLast := by simp [pop]
@[simp] theorem pop_empty : (#[] : Array α).pop = #[] := rfl
@[simp] theorem pop_push (a : Array α) : (a.push x).pop = a := by simp [pop]
@[simp] theorem getElem_pop (a : Array α) (i : Nat) (hi : i < a.pop.size) :
a.pop[i] = a[i]'(Nat.lt_of_lt_of_le (a.size_pop hi) (Nat.sub_le _ _)) :=
List.get_dropLast ..
theorem eq_empty_of_size_eq_zero {as : Array α} (h : as.size = 0) : as = #[] := by
apply ext
· simp [h]
· intros; contradiction
theorem eq_push_pop_back_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.size 0) :
as = as.pop.push as.back := by
apply ext
· simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)]
· intros i h h'
if hlt : i < as.pop.size then
rw [get_push_lt (h:=hlt), getElem_pop]
else
have heq : i = as.pop.size :=
Nat.le_antisymm (size_pop .. Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt)
cases heq; rw [get_push_eq, back, size_pop, get!_eq_getD, getD, dif_pos h]; rfl
theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size 0) :
(bs : Array α) (c : α), as = bs.push c :=
let _ : Inhabited α := as[0]
as.pop, as.back, eq_push_pop_back_of_size_ne_zero h
theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
@[simp] theorem size_swap! (a : Array α) (i j) :
(a.swap! i j).size = a.size := by unfold swap!; split <;> (try split) <;> simp [size_swap]
@[simp] theorem size_reverse (a : Array α) : a.reverse.size = a.size := by
let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by
rw [reverse.loop]
if h : i < j then
have := reverse.termination h
simp [(go · (i+1) j-1, ·), h]
else simp [h]
termination_by j - i
simp only [reverse]; split <;> simp [go]
@[simp] theorem size_range {n : Nat} : (range n).size = n := by
unfold range
induction n with
| zero => simp [Nat.fold]
| succ k ih =>
rw [Nat.fold, flip]
simp only [mkEmpty_eq, size_push] at *
omega
@[simp] theorem reverse_data (a : Array α) : a.reverse.data = a.data.reverse := by
let rec go (as : Array α) (i j hj)
(h : i + j + 1 = a.size) (h₂ : as.size = a.size)
(H : k, as.data.get? k = if i k k j then a.data.get? k else a.data.reverse.get? k)
(k) : (reverse.loop as i j, hj).data.get? k = a.data.reverse.get? k := by
rw [reverse.loop]; dsimp; split <;> rename_i h₁
· have := reverse.termination h₁
match j with | j+1 => ?_
simp at *
rw [(go · (i+1) j)]
· rwa [Nat.add_right_comm i]
· simp [size_swap, h₂]
· intro k
rw [ getElem?_eq_data_get?, get?_swap]
simp [getElem?_eq_data_get?, getElem_eq_data_get, List.get?_eq_get, H, Nat.le_of_lt h₁]
split <;> rename_i h₂
· simp [ h₂, Nat.not_le.2 (Nat.lt_succ_self _)]
exact (List.get?_reverse' _ _ (Eq.trans (by simp_arith) h)).symm
split <;> rename_i h₃
· simp [ h₃, Nat.not_le.2 (Nat.lt_succ_self _)]
exact (List.get?_reverse' _ _ (Eq.trans (by simp_arith) h)).symm
simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
· rw [H]; split <;> rename_i h₂
· cases Nat.le_antisymm (Nat.not_lt.1 h₁) (Nat.le_trans h₂.1 h₂.2)
cases Nat.le_antisymm h₂.1 h₂.2
exact (List.get?_reverse' _ _ h).symm
· rfl
termination_by j - i
simp only [reverse]; split
· match a with | [] | [_] => rfl
· have := Nat.sub_add_cancel (Nat.le_of_not_le _)
refine List.ext <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
split; {rfl}; rename_i h
simp [ show k < _ + 1 _ from Nat.lt_succ (n := a.size - 1), this] at h
rw [List.get?_eq_none.2 _, List.get?_eq_none.2 (a.data.length_reverse _)]
/-! ### foldl / foldr -/
-- This proof is the pure version of `Array.SatisfiesM_foldlM`,
-- reproduced to avoid a dependency on `SatisfiesM`.
theorem foldl_induction
{as : Array α} (motive : Nat β Prop) {init : β} (h0 : motive 0 init) {f : β α β}
(hf : i : Fin as.size, b, motive i.1 b motive (i.1 + 1) (f b as[i])) :
motive as.size (as.foldl f init) := by
let rec go {i j b} (h₁ : j as.size) (h₂ : as.size i + j) (H : motive j b) :
(motive as.size) (foldlM.loop (m := Id) f as as.size (Nat.le_refl _) i j b) := by
unfold foldlM.loop; split
· next hj =>
split
· cases Nat.not_le_of_gt (by simp [hj]) h₂
· exact go hj (by rwa [Nat.succ_add] at h₂) (hf j, hj b H)
· next hj => exact Nat.le_antisymm h₁ (Nat.ge_of_not_lt hj) H
simpa [foldl, foldlM] using go (Nat.zero_le _) (Nat.le_refl _) h0
-- This proof is the pure version of `Array.SatisfiesM_foldrM`,
-- reproduced to avoid a dependency on `SatisfiesM`.
theorem foldr_induction
{as : Array α} (motive : Nat β Prop) {init : β} (h0 : motive as.size init) {f : α β β}
(hf : i : Fin as.size, b, motive (i.1 + 1) b motive i.1 (f as[i] b)) :
motive 0 (as.foldr f init) := by
let rec go {i b} (hi : i as.size) (H : motive i b) :
(motive 0) (foldrM.fold (m := Id) f as 0 i hi b) := by
unfold foldrM.fold; simp; split
· next hi => exact (hi H)
· next hi =>
split; {simp at hi}
· next i hi' =>
exact go _ (hf i, hi' b H)
simp [foldr, foldrM]; split; {exact go _ h0}
· next h => exact (Nat.eq_zero_of_not_pos h h0)
/-! ### map -/
@[simp] theorem mem_map {f : α β} {l : Array α} : b l.map f a, a l f a = b := by
simp only [mem_def, map_data, List.mem_map]
theorem mapM_eq_mapM_data [Monad m] [LawfulMonad m] (f : α m β) (arr : Array α) :
arr.mapM f = return mk ( arr.data.mapM f) := by
rw [mapM_eq_foldlM, foldlM_eq_foldlM_data, List.foldrM_reverse]
conv => rhs; rw [ List.reverse_reverse arr.data]
induction arr.data.reverse with
| nil => simp; rfl
| cons a l ih => simp [ih]; simp [map_eq_pure_bind, push]
theorem mapM_map_eq_foldl (as : Array α) (f : α β) (i) :
mapM.map (m := Id) f as i b = as.foldl (start := i) (fun r a => r.push (f a)) b := by
unfold mapM.map
split <;> rename_i h
· simp only [Id.bind_eq]
dsimp [foldl, Id.run, foldlM]
rw [mapM_map_eq_foldl, dif_pos (by omega), foldlM.loop, dif_pos h]
-- Calling `split` here gives a bad goal.
have : size as - i = Nat.succ (size as - i - 1) := by omega
rw [this]
simp [foldl, foldlM, Id.run, Nat.sub_add_eq]
· dsimp [foldl, Id.run, foldlM]
rw [dif_pos (by omega), foldlM.loop, dif_neg h]
rfl
termination_by as.size - i
theorem map_eq_foldl (as : Array α) (f : α β) :
as.map f = as.foldl (fun r a => r.push (f a)) #[] :=
mapM_map_eq_foldl _ _ _
theorem map_induction (as : Array α) (f : α β) (motive : Nat Prop) (h0 : motive 0)
(p : Fin as.size β Prop) (hs : i, motive i.1 p i (f as[i]) motive (i+1)) :
motive as.size
eq : (as.map f).size = as.size, i h, p i, h ((as.map f)[i]) := by
have t := foldl_induction (as := as) (β := Array β)
(motive := fun i arr => motive i arr.size = i i h2, p i arr[i.1])
(init := #[]) (f := fun r a => r.push (f a)) ?_ ?_
obtain m, eq, w := t
· refine m, by simpa [map_eq_foldl] using eq, ?_
intro i h
simp [eq] at w
specialize w i, h h
simpa [map_eq_foldl] using w
· exact h0, rfl, nofun
· intro i b m, eq, w
refine ?_, ?_, ?_
· exact (hs _ m).2
· simp_all
· intro j h
simp at h
by_cases h' : j < size b
· rw [get_push]
simp_all
· rw [get_push, dif_neg h']
simp only [show j = i by omega]
exact (hs _ m).1
theorem map_spec (as : Array α) (f : α β) (p : Fin as.size β Prop)
(hs : i, p i (f as[i])) :
eq : (as.map f).size = as.size, i h, p i, h ((as.map f)[i]) := by
simpa using map_induction as f (fun _ => True) trivial p (by simp_all)
@[simp] theorem getElem_map (f : α β) (as : Array α) (i : Nat) (h) :
((as.map f)[i]) = f (as[i]'(size_map .. h)) := by
have := map_spec as f (fun i b => b = f (as[i]))
simp only [implies_true, true_implies] at this
obtain eq, w := this
apply w
simp_all
/-! ### mapIdx -/
-- This could also be prove from `SatisfiesM_mapIdxM`.
theorem mapIdx_induction (as : Array α) (f : Fin as.size α β)
(motive : Nat Prop) (h0 : motive 0)
(p : Fin as.size β Prop)
(hs : i, motive i.1 p i (f i as[i]) motive (i + 1)) :
motive as.size eq : (Array.mapIdx as f).size = as.size,
i h, p i, h ((Array.mapIdx as f)[i]) := by
let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : i h h', p i, h bs[i]) (hm : motive j) :
let arr : Array β := Array.mapIdxM.map (m := Id) as f i j h bs
motive as.size eq : arr.size = as.size, i h, p i, h arr[i] := by
induction i generalizing j bs with simp [mapIdxM.map]
| zero =>
have := (Nat.zero_add _).symm.trans h
exact this hm, h₁ this, fun _ _ => h₂ ..
| succ i ih =>
apply @ih (bs.push (f j, by omega as[j])) (j + 1) (by omega) (by simp; omega)
· intro i i_lt h'
rw [get_push]
split
· apply h₂
· simp only [size_push] at h'
obtain rfl : i = j := by omega
apply (hs i, by omega hm).1
· exact (hs j, by omega hm).2
simp [mapIdx, mapIdxM]; exact go rfl nofun h0
theorem mapIdx_spec (as : Array α) (f : Fin as.size α β)
(p : Fin as.size β Prop) (hs : i, p i (f i as[i])) :
eq : (Array.mapIdx as f).size = as.size,
i h, p i, h ((Array.mapIdx as f)[i]) :=
(mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ => hs .., trivial).2
@[simp] theorem size_mapIdx (a : Array α) (f : Fin a.size α β) : (a.mapIdx f).size = a.size :=
(mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
Array.size_mapIdx _ _
@[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size α β) (i : Nat)
(h : i < (mapIdx a f).size) :
haveI : i < a.size := by simp_all
(a.mapIdx f)[i] = f i, this a[i] :=
(mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
/-! ### modify -/
@[simp] theorem size_modify (a : Array α) (i : Nat) (f : α α) : (a.modify i f).size = a.size := by
unfold modify modifyM Id.run
split <;> simp
theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
(arr.modify x f).get i, by simp [h] =
if x = i then f (arr.get i, h) else arr.get i, h := by
simp [modify, modifyM, Id.run]; split
· simp [get_set _ _ _ h]; split <;> simp [*]
· rw [if_neg (mt (by rintro rfl; exact h) _)]
/-! ### filter -/
@[simp] theorem filter_data (p : α Bool) (l : Array α) :
(l.filter p).data = l.data.filter p := by
dsimp only [filter]
rw [foldl_eq_foldl_data]
generalize l.data = l
suffices a, (List.foldl (fun r a => if p a = true then push r a else r) a l).data =
a.data ++ List.filter p l by
simpa using this #[]
induction l with simp
| cons => split <;> simp [*]
@[simp] theorem filter_filter (q) (l : Array α) :
filter p (filter q l) = filter (fun a => p a q a) l := by
apply ext'
simp only [filter_data, List.filter_filter]
@[simp] theorem mem_filter : x filter p as x as p x := by
simp only [mem_def, filter_data, List.mem_filter]
theorem mem_of_mem_filter {a : α} {l} (h : a filter p l) : a l :=
(mem_filter.mp h).1
/-! ### filterMap -/
@[simp] theorem filterMap_data (f : α Option β) (l : Array α) :
(l.filterMap f).data = l.data.filterMap f := by
dsimp only [filterMap, filterMapM]
rw [foldlM_eq_foldlM_data]
generalize l.data = l
have this : a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).data =
a.data ++ List.filterMap f l := ?_
exact this #[]
induction l
· simp_all [Id.run]
· simp_all [Id.run]
split <;> simp_all
@[simp] theorem mem_filterMap (f : α Option β) (l : Array α) {b : β} :
b filterMap f l a, a l f a = some b := by
simp only [mem_def, filterMap_data, List.mem_filterMap]
/-! ### empty -/
theorem size_empty : (#[] : Array α).size = 0 := rfl
theorem empty_data : (#[] : Array α).data = [] := rfl
/-! ### append -/
theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
@[simp] theorem mem_append {a : α} {s t : Array α} : a s ++ t a s a t := by
simp only [mem_def, append_data, List.mem_append]
theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
simp only [size, append_data, List.length_append]
theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
(as ++ bs)[i] = as[i] := by
simp only [getElem_eq_data_get]
have h' : i < (as.data ++ bs.data).length := by rwa [ data_length, append_data] at h
conv => rhs; rw [ List.get_append_left (bs:=bs.data) (h':=h')]
apply List.get_of_eq; rw [append_data]
theorem get_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size i)
(hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. h)) :
(as ++ bs)[i] = bs[i - as.size] := by
simp only [getElem_eq_data_get]
have h' : i < (as.data ++ bs.data).length := by rwa [ data_length, append_data] at h
conv => rhs; rw [ List.get_append_right (h':=h') (h:=Nat.not_lt_of_ge hle)]
apply List.get_of_eq; rw [append_data]
@[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
apply ext'; simp only [append_data, empty_data, List.append_nil]
@[simp] theorem nil_append (as : Array α) : #[] ++ as = as := by
apply ext'; simp only [append_data, empty_data, List.nil_append]
theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
apply ext'; simp only [append_data, List.append_assoc]
/-! ### extract -/
theorem extract_loop_zero (as bs : Array α) (start : Nat) : extract.loop as 0 start bs = bs := by
rw [extract.loop]; split <;> rfl
theorem extract_loop_succ (as bs : Array α) (size start : Nat) (h : start < as.size) :
extract.loop as (size+1) start bs = extract.loop as size (start+1) (bs.push as[start]) := by
rw [extract.loop, dif_pos h]; rfl
theorem extract_loop_of_ge (as bs : Array α) (size start : Nat) (h : start as.size) :
extract.loop as size start bs = bs := by
rw [extract.loop, dif_neg (Nat.not_lt_of_ge h)]
theorem extract_loop_eq_aux (as bs : Array α) (size start : Nat) :
extract.loop as size start bs = bs ++ extract.loop as size start #[] := by
induction size using Nat.recAux generalizing start bs with
| zero => rw [extract_loop_zero, extract_loop_zero, append_nil]
| succ size ih =>
if h : start < as.size then
rw [extract_loop_succ (h:=h), ih (bs.push _), push_eq_append_singleton]
rw [extract_loop_succ (h:=h), ih (#[].push _), push_eq_append_singleton, nil_append]
rw [append_assoc]
else
rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)]
rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)]
rw [append_nil]
theorem extract_loop_eq (as bs : Array α) (size start : Nat) (h : start + size as.size) :
extract.loop as size start bs = bs ++ as.extract start (start + size) := by
simp [extract]; rw [extract_loop_eq_aux, Nat.min_eq_left h, Nat.add_sub_cancel_left]
theorem size_extract_loop (as bs : Array α) (size start : Nat) :
(extract.loop as size start bs).size = bs.size + min size (as.size - start) := by
induction size using Nat.recAux generalizing start bs with
| zero => rw [extract_loop_zero, Nat.zero_min, Nat.add_zero]
| succ size ih =>
if h : start < as.size then
rw [extract_loop_succ (h:=h), ih, size_push, Nat.add_assoc, Nat.add_min_add_left,
Nat.sub_succ, Nat.one_add, Nat.one_add, Nat.succ_pred_eq_of_pos (Nat.sub_pos_of_lt h)]
else
have h := Nat.le_of_not_gt h
rw [extract_loop_of_ge (h:=h), Nat.sub_eq_zero_of_le h, Nat.min_zero, Nat.add_zero]
@[simp] theorem size_extract (as : Array α) (start stop : Nat) :
(as.extract start stop).size = min stop as.size - start := by
simp [extract]; rw [size_extract_loop, size_empty, Nat.zero_add, Nat.sub_min_sub_right,
Nat.min_assoc, Nat.min_self]
theorem get_extract_loop_lt_aux (as bs : Array α) (size start : Nat) (hlt : i < bs.size) :
i < (extract.loop as size start bs).size := by
rw [size_extract_loop]
apply Nat.lt_of_lt_of_le hlt
exact Nat.le_add_right ..
theorem get_extract_loop_lt (as bs : Array α) (size start : Nat) (hlt : i < bs.size)
(h := get_extract_loop_lt_aux as bs size start hlt) :
(extract.loop as size start bs)[i] = bs[i] := by
apply Eq.trans _ (get_append_left (bs:=extract.loop as size start #[]) hlt)
· rw [size_append]; exact Nat.lt_of_lt_of_le hlt (Nat.le_add_right ..)
· congr; rw [extract_loop_eq_aux]
theorem get_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge : i bs.size)
(h : i < (extract.loop as size start bs).size) : start + i - bs.size < as.size := by
have h : i < bs.size + (as.size - start) := by
apply Nat.lt_of_lt_of_le h
rw [size_extract_loop]
apply Nat.add_le_add_left
exact Nat.min_le_right ..
rw [Nat.add_sub_assoc hge]
apply Nat.add_lt_of_lt_sub'
exact Nat.sub_lt_left_of_lt_add hge h
theorem get_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i bs.size)
(h : i < (extract.loop as size start bs).size)
(h' := get_extract_loop_ge_aux as bs size start hge h) :
(extract.loop as size start bs)[i] = as[start + i - bs.size] := by
induction size using Nat.recAux generalizing start bs with
| zero =>
rw [size_extract_loop, Nat.zero_min, Nat.add_zero] at h
omega
| succ size ih =>
have : start < as.size := by
apply Nat.lt_of_le_of_lt (Nat.le_add_right start (i - bs.size))
rwa [ Nat.add_sub_assoc hge]
have : i < (extract.loop as size (start+1) (bs.push as[start])).size := by
rwa [ extract_loop_succ]
have heq : (extract.loop as (size+1) start bs)[i] =
(extract.loop as size (start+1) (bs.push as[start]))[i] := by
congr 1; rw [extract_loop_succ]
rw [heq]
if hi : bs.size = i then
cases hi
have h₁ : bs.size < (bs.push as[start]).size := by rw [size_push]; exact Nat.lt_succ_self ..
have h₂ : bs.size < (extract.loop as size (start+1) (bs.push as[start])).size := by
rw [size_extract_loop]; apply Nat.lt_of_lt_of_le h₁; exact Nat.le_add_right ..
have h : (extract.loop as size (start + 1) (push bs as[start]))[bs.size] = as[start] := by
rw [get_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
rw [h]; congr; rw [Nat.add_sub_cancel]
else
have hge : bs.size + 1 i := Nat.lt_of_le_of_ne hge hi
rw [ih (bs.push as[start]) (start+1) ((size_push ..).symm hge)]
congr 1; rw [size_push, Nat.add_right_comm, Nat.add_sub_add_right]
theorem get_extract_aux {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) :
start + i < as.size := by
rw [size_extract] at h; apply Nat.add_lt_of_lt_sub'; apply Nat.lt_of_lt_of_le h
apply Nat.sub_le_sub_right; apply Nat.min_le_right
@[simp] theorem get_extract {as : Array α} {start stop : Nat}
(h : i < (as.extract start stop).size) :
(as.extract start stop)[i] = as[start + i]'(get_extract_aux h) :=
show (extract.loop as (min stop as.size - start) start #[])[i]
= as[start + i]'(get_extract_aux h) by rw [get_extract_loop_ge]; rfl; exact Nat.zero_le _
@[simp] theorem extract_all (as : Array α) : as.extract 0 as.size = as := by
apply ext
· rw [size_extract, Nat.min_self, Nat.sub_zero]
· intros; rw [get_extract]; congr; rw [Nat.zero_add]
theorem extract_empty_of_stop_le_start (as : Array α) {start stop : Nat} (h : stop start) :
as.extract start stop = #[] := by
simp [extract]; rw [Nat.sub_min_sub_right, Nat.sub_eq_zero_of_le h, Nat.zero_min,
extract_loop_zero]
theorem extract_empty_of_size_le_start (as : Array α) {start stop : Nat} (h : as.size start) :
as.extract start stop = #[] := by
simp [extract]; rw [Nat.sub_min_sub_right, Nat.sub_eq_zero_of_le h, Nat.min_zero,
extract_loop_zero]
@[simp] theorem extract_empty (start stop : Nat) : (#[] : Array α).extract start stop = #[] :=
extract_empty_of_size_le_start _ (Nat.zero_le _)
/-! ### any -/
-- Auxiliary for `any_iff_exists`.
theorem anyM_loop_iff_exists (p : α Bool) (as : Array α) (start stop) (h : stop as.size) :
anyM.loop (m := Id) p as stop h start = true
i : Fin as.size, start i i < stop p as[i] = true := by
unfold anyM.loop
split <;> rename_i h₁
· dsimp
split <;> rename_i h₂
· simp only [true_iff]
refine start, by omega, by dsimp; omega, by dsimp; omega, h₂
· rw [anyM_loop_iff_exists]
constructor
· rintro i, ge, lt, h
have : start i := by rintro rfl; omega
exact i, by omega, lt, h
· rintro i, ge, lt, h
have : start i := by rintro rfl; erw [h] at h₂; simp_all
exact i, by omega, lt, h
· simp
omega
termination_by stop - start
-- This could also be proved from `SatisfiesM_anyM_iff_exists` in `Batteries.Data.Array.Init.Monadic`
theorem any_iff_exists (p : α Bool) (as : Array α) (start stop) :
any as p start stop i : Fin as.size, start i.1 i.1 < stop p as[i] := by
dsimp [any, anyM, Id.run]
split
· rw [anyM_loop_iff_exists]; rfl
· rw [anyM_loop_iff_exists]
constructor
· rintro i, ge, _, h
exact i, by omega, by omega, h
· rintro i, ge, _, h
exact i, by omega, by omega, h
theorem any_eq_true (p : α Bool) (as : Array α) :
any as p i : Fin as.size, p as[i] := by simp [any_iff_exists, Fin.isLt]
theorem any_def {p : α Bool} (as : Array α) : as.any p = as.data.any p := by
rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]; simp only [List.mem_iff_get]
exact fun i, h => _, i, rfl, h, fun _, i, rfl, h => i, h
/-! ### all -/
theorem all_eq_not_any_not (p : α Bool) (as : Array α) (start stop) :
all as p start stop = !(any as (!p ·) start stop) := by
dsimp [all, allM]
rfl
theorem all_iff_forall (p : α Bool) (as : Array α) (start stop) :
all as p start stop i : Fin as.size, start i.1 i.1 < stop p as[i] := by
rw [all_eq_not_any_not]
suffices ¬(any as (!p ·) start stop = true)
i : Fin as.size, start i.1 i.1 < stop p as[i] by
simp_all
rw [any_iff_exists]
simp
theorem all_eq_true (p : α Bool) (as : Array α) : all as p i : Fin as.size, p as[i] := by
simp [all_iff_forall, Fin.isLt]
theorem all_def {p : α Bool} (as : Array α) : as.all p = as.data.all p := by
rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_get]
constructor
· rintro w x r, rfl
rw [ getElem_eq_data_get]
apply w
· intro w i
exact w as[i] i, (getElem_eq_data_get as i.2).symm
theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p x, x l p x := by
simp only [all_def, List.all_eq_true, mem_def]
/-! ### contains -/
theorem contains_def [DecidableEq α] {a : α} {as : Array α} : as.contains a a as := by
rw [mem_def, contains, any_def, List.any_eq_true]; simp [and_comm]
instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a as) :=
decidable_of_iff _ contains_def
/-! ### swap -/
open Fin
@[simp] theorem get_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
by simp only [swap, fin_cast_val, get_eq_getElem, getElem_set_eq, getElem_fin]
@[simp] theorem get_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
if he : ((Array.size_set _ _ _).symm j).val = i.val then by
simp only [he, fin_cast_val, get_swap_right, getElem_fin]
else by
apply Eq.trans
· apply Array.get_set_ne
· simp only [size_set, Fin.isLt]
· assumption
· simp [get_set_ne]
@[simp] theorem get_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
(hi : p i) (hj : p j) : (a.swap i j)[p]'(a.size_swap .. |>.symm hp) = a[p] := by
apply Eq.trans
· have : ((a.size_set i (a.get j)).symm j).val = j.val := by simp only [fin_cast_val]
apply Array.get_set_ne
· simp only [this]
apply Ne.symm
· assumption
· apply Array.get_set_ne
· apply Ne.symm
· assumption
theorem get_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk: k < a.size) :
(a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i] else a[k] := by
split
· simp_all only [get_swap_left]
· split <;> simp_all
theorem get_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk' : k < (a.swap i j).size) :
(a.swap i j)[k] = if k = i then a[j] else if k = j then a[i] else a[k]'(by simp_all) := by
apply get_swap
@[simp] theorem swap_swap (a : Array α) {i j : Fin a.size} :
(a.swap i j).swap i.1, (a.size_swap ..).symm i.2 j.1, (a.size_swap ..).symm j.2 = a := by
apply ext
· simp only [size_swap]
· intros
simp only [get_swap']
split
· simp_all
· split <;> simp_all
theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i := by
apply ext
· simp only [size_swap]
· intros
simp only [get_swap']
split
· split <;> simp_all
· split <;> simp_all
end Array

View File

@@ -27,20 +27,13 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a <
cases as with | _ as =>
exact Nat.lt_trans (List.sizeOf_get ..) (by simp_arith)
@[simp] theorem sizeOf_getElem [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) :
sizeOf (as[i]'h) < sizeOf as := sizeOf_get _ _
/-- This tactic, added to the `decreasing_trivial` toolbox, proves that
`sizeOf arr[i] < sizeOf arr`, which is useful for well founded recursions
over a nested inductive like `inductive T | mk : Array T → T`. -/
macro "array_get_dec" : tactic =>
`(tactic| first
-- subsumed by simp
-- | with_reducible apply sizeOf_get
-- | with_reducible apply sizeOf_getElem
| (with_reducible apply Nat.lt_trans (sizeOf_get ..)); simp_arith
| (with_reducible apply Nat.lt_trans (sizeOf_getElem ..)); simp_arith
)
| apply sizeOf_get
| apply Nat.lt_trans (sizeOf_get ..); simp_arith)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_get_dec)
@@ -50,10 +43,9 @@ provided that `a ∈ arr` which is useful for well founded recursions over a nes
-- NB: This is analogue to tactic `sizeOf_list_dec`
macro "array_mem_dec" : tactic =>
`(tactic| first
| with_reducible apply Array.sizeOf_lt_of_mem; assumption; done
| with_reducible
apply Nat.lt_trans (Array.sizeOf_lt_of_mem ?h)
case' h => assumption
| apply Array.sizeOf_lt_of_mem; assumption; done
| apply Nat.lt_trans (Array.sizeOf_lt_of_mem ?h)
case' h => assumption
simp_arith)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_mem_dec)

View File

@@ -27,7 +27,6 @@ def qpartition (as : Array α) (lt : αα → Bool) (lo hi : Nat) : Nat ×
let as := as.swap! i hi
(i, as)
termination_by hi - j
decreasing_by all_goals simp_wf; decreasing_trivial_pre_omega
loop as lo lo
@[inline] partial def qsort (as : Array α) (lt : α α Bool) (low := 0) (high := as.size - 1) : Array α :=

View File

@@ -159,29 +159,4 @@ theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := b
theorem allOnes_sub_eq_not (x : BitVec w) : allOnes w - x = ~~~x := by
rw [ add_not_self x, BitVec.add_comm, add_sub_cancel]
/-! ### Negation -/
theorem bit_not_testBit (x : BitVec w) (i : Fin w) :
getLsb (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) i.val = !(getLsb x i.val) := by
apply iunfoldr_getLsb (fun _ => ()) i (by simp)
theorem bit_not_add_self (x : BitVec w) :
((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd + x = -1 := by
simp only [add_eq_adc]
apply iunfoldr_replace_snd (fun _ => false) (-1) false rfl
intro i; simp only [ BitVec.not, adcb, testBit_toNat]
rw [iunfoldr_replace_snd (fun _ => ()) (((iunfoldr (fun i c => (c, !(x.getLsb i)))) ()).snd)]
<;> simp [bit_not_testBit, negOne_eq_allOnes, getLsb_allOnes]
theorem bit_not_eq_not (x : BitVec w) :
((iunfoldr (fun i c => (c, !(x.getLsb i)))) ()).snd = ~~~ x := by
simp [allOnes_sub_eq_not, BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), negOne_eq_allOnes]
theorem bit_neg_eq_neg (x : BitVec w) : -x = (adc (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) (BitVec.ofNat w 1) false).snd:= by
simp only [ add_eq_adc]
rw [iunfoldr_replace_snd ((fun _ => ())) (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) _ rfl]
· rw [BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), sub_toAdd, BitVec.add_comm _ (-x)]
simp [ sub_toAdd, BitVec.sub_add_cancel]
· simp [bit_not_testBit x _]
end BitVec

View File

@@ -1,7 +1,7 @@
/-
Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joe Hendrix, Harun Khan
Authors: Joe Hendrix
-/
prelude
import Init.Data.BitVec.Lemmas
@@ -48,51 +48,6 @@ private theorem iunfoldr.eq_test
intro i
simp_all [truncate_succ]
theorem iunfoldr_getLsb' {f : Fin w α α × Bool} (state : Nat α)
(ind : (i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :
( i : Fin w, getLsb (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd)
(iunfoldr f (state 0)).fst = state w := by
unfold iunfoldr
simp
apply Fin.hIterate_elim
(fun j (p : α × BitVec j) => (hj : j w)
( i : Fin j, getLsb p.snd i.val = (f i.val, Nat.lt_of_lt_of_le i.isLt hj (state i.val)).snd)
p.fst = state j)
case hj => simp
case init =>
intro
apply And.intro
· intro i
have := Fin.size_pos i
contradiction
· rfl
case step =>
intro j s, v ih hj
apply And.intro
case left =>
intro i
simp only [getLsb_cons]
have hj2 : j.val w := by simp
cases (Nat.lt_or_eq_of_le (Nat.lt_succ.mp i.isLt)) with
| inl h3 => simp [if_neg, (Nat.ne_of_lt h3)]
exact (ih hj2).1 i.val, h3
| inr h3 => simp [h3, if_pos]
cases (Nat.eq_zero_or_pos j.val) with
| inl hj3 => congr
rw [ (ih hj2).2]
| inr hj3 => congr
exact (ih hj2).2
case right =>
simp
have hj2 : j.val w := by simp
rw [ ind j, (ih hj2).2]
theorem iunfoldr_getLsb {f : Fin w α α × Bool} (state : Nat α) (i : Fin w)
(ind : (i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :
getLsb (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd := by
exact (iunfoldr_getLsb' state ind).1 i
/--
Correctness theorem for `iunfoldr`.
-/
@@ -103,11 +58,4 @@ theorem iunfoldr_replace
iunfoldr f a = (state w, value) := by
simp [iunfoldr.eq_test state value a init step]
theorem iunfoldr_replace_snd
{f : Fin w α α × Bool} (state : Nat α) (value : BitVec w) (a : α)
(init : state 0 = a)
(step : (i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
(iunfoldr f a).snd = value := by
simp [iunfoldr.eq_test state value a init step]
end BitVec

View File

@@ -2,7 +2,6 @@
Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed,
-/
prelude
import Init.Data.Bool
@@ -104,13 +103,7 @@ theorem eq_of_getMsb_eq {x y : BitVec w}
have q := pred w - 1 - i, q_lt
simpa [q_lt, Nat.sub_sub_self, r] using q
-- This cannot be a `@[simp]` lemma, as it would be tried at every term.
theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp
@[simp] theorem toNat_zero_length (x : BitVec 0) : x.toNat = 0 := by simp [of_length_zero]
@[simp] theorem getLsb_zero_length (x : BitVec 0) : x.getLsb i = false := by simp [of_length_zero]
@[simp] theorem getMsb_zero_length (x : BitVec 0) : x.getMsb i = false := by simp [of_length_zero]
@[simp] theorem msb_zero_length (x : BitVec 0) : x.msb = false := by simp [BitVec.msb, of_length_zero]
@[simp] theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp
theorem eq_of_toFin_eq : {x y : BitVec w}, x.toFin = y.toFin x = y
| _, _, _, _, rfl => rfl
@@ -343,7 +336,7 @@ theorem nat_eq_toNat (x : BitVec w) (y : Nat)
@[simp] theorem getMsb_zeroExtend_add {x : BitVec w} (h : k i) :
(x.zeroExtend (w + k)).getMsb i = x.getMsb (i - k) := by
by_cases h : w = 0
· subst h; simp [of_length_zero]
· subst h; simp
simp only [getMsb, getLsb_zeroExtend]
by_cases h₁ : i < w + k <;> by_cases h₂ : i - k < w <;> by_cases h₃ : w + k - 1 - i < w + k
<;> simp [h₁, h₂, h₃]
@@ -901,15 +894,6 @@ theorem add_sub_cancel (x y : BitVec w) : x + y - y = x := by
rw [toNat_sub, toNat_add, Nat.mod_add_mod, Nat.add_assoc, Nat.add_sub_assoc y_toNat_le,
Nat.add_sub_cancel_left, Nat.add_mod_right, toNat_mod_cancel]
theorem sub_add_cancel (x y : BitVec w) : x - y + y = x := by
rw [sub_toAdd, BitVec.add_assoc, BitVec.add_comm _ y,
BitVec.add_assoc, sub_toAdd, add_sub_cancel]
theorem eq_sub_iff_add_eq {x y z : BitVec w} : x = z - y x + y = z := by
apply Iff.intro <;> intro h
· simp [h, sub_add_cancel]
· simp [h, add_sub_cancel]
theorem negOne_eq_allOnes : -1#w = allOnes w := by
apply eq_of_toNat_eq
if g : w = 0 then
@@ -919,13 +903,6 @@ theorem negOne_eq_allOnes : -1#w = allOnes w := by
have r : (2^w - 1) < 2^w := by omega
simp [Nat.mod_eq_of_lt q, Nat.mod_eq_of_lt r]
theorem neg_eq_not_add (x : BitVec w) : -x = ~~~x + 1 := by
apply eq_of_toNat_eq
simp only [toNat_neg, ofNat_eq_ofNat, toNat_add, toNat_not, toNat_ofNat, Nat.add_mod_mod]
congr
have hx : x.toNat < 2^w := x.isLt
rw [Nat.sub_sub, Nat.add_comm 1 x.toNat, Nat.sub_sub, Nat.sub_add_cancel (by omega)]
/-! ### mul -/
theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl

View File

@@ -12,7 +12,6 @@ import Init.Data.Nat.Linear
loop (x : α) (i : Nat) : α :=
if h : i < n then loop (f x i, h) (i+1) else x
termination_by n - i
decreasing_by decreasing_trivial_pre_omega
/-- Folds over `Fin n` from the right: `foldr 3 f x = f 0 (f 1 (f 2 x))`. -/
@[inline] def foldr (n) (f : Fin n α α) (init : α) : α := loop n, Nat.le_refl n init where

View File

@@ -23,7 +23,6 @@ def hIterateFrom (P : Nat → Sort _) {n} (f : ∀(i : Fin n), P i.val → P (i.
have p : i = n := (or_iff_left g).mp (Nat.eq_or_lt_of_le ubnd)
_root_.cast (congrArg P p) a
termination_by n - i
decreasing_by decreasing_trivial_pre_omega
/--
`hIterate` is a heterogenous iterative operation that applies a

View File

@@ -602,7 +602,6 @@ A version of `Fin.succRec` taking `i : Fin n` as the first argument. -/
@Fin.succRecOn (n + 1) i.succ motive zero succ = succ n i (Fin.succRecOn i zero succ) := by
cases i; rfl
/-- Define `motive i` by induction on `i : Fin (n + 1)` via induction on the underlying `Nat` value.
This function has two arguments: `zero` handles the base case on `motive 0`,
and `succ` defines the inductive step using `motive i.castSucc`.
@@ -611,12 +610,8 @@ and `succ` defines the inductive step using `motive i.castSucc`.
@[elab_as_elim] def induction {motive : Fin (n + 1) Sort _} (zero : motive 0)
(succ : i : Fin n, motive (castSucc i) motive i.succ) :
i : Fin (n + 1), motive i
| i, hi => go i hi
where
-- Use a curried function so that this is structurally recursive
go : (i : Nat) (hi : i < n + 1), motive i, hi
| 0, hi => by rwa [Fin.mk_zero]
| i+1, hi => succ i, Nat.lt_of_succ_lt_succ hi (go i (Nat.lt_of_succ_lt hi))
| 0, hi => by rwa [Fin.mk_zero]
| i+1, hi => succ i, Nat.lt_of_succ_lt_succ hi (induction zero succ i, Nat.lt_of_succ_lt hi)
@[simp] theorem induction_zero {motive : Fin (n + 1) Sort _} (zero : motive 0)
(hs : i : Fin n, motive (castSucc i) motive i.succ) :

View File

@@ -9,4 +9,3 @@ import Init.Data.List.BasicAux
import Init.Data.List.Control
import Init.Data.List.Lemmas
import Init.Data.List.Impl
import Init.Data.List.TakeDrop

View File

@@ -226,10 +226,9 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a <
over a nested inductive like `inductive T | mk : List T → T`. -/
macro "sizeOf_list_dec" : tactic =>
`(tactic| first
| with_reducible apply sizeOf_lt_of_mem; assumption; done
| with_reducible
apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
case' h => assumption
| apply sizeOf_lt_of_mem; assumption; done
| apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
case' h => assumption
simp_arith)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| sizeOf_list_dec)

File diff suppressed because it is too large Load Diff

View File

@@ -1,360 +0,0 @@
/-
Copyright (c) 2014 Parikshit Khanna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
-/
prelude
import Init.Data.List.Lemmas
import Init.Data.Nat.Lemmas
/-!
# Lemmas about `List.take`, `List.drop`, `List.zip` and `List.zipWith`.
These are in a separate file from most of the list lemmas
as they required importing more lemmas about natural numbers.
-/
namespace List
open Nat
/-! ### take -/
abbrev take_succ_cons := @take_cons_succ
@[simp] theorem length_take : (i : Nat) (l : List α), length (take i l) = min i (length l)
| 0, l => by simp [Nat.zero_min]
| succ n, [] => by simp [Nat.min_zero]
| succ n, _ :: l => by simp [Nat.succ_min_succ, length_take]
theorem length_take_le (n) (l : List α) : length (take n l) n := by simp [Nat.min_le_left]
theorem length_take_le' (n) (l : List α) : length (take n l) l.length :=
by simp [Nat.min_le_right]
theorem length_take_of_le (h : n length l) : length (take n l) = n := by simp [Nat.min_eq_left h]
theorem take_all_of_le {n} {l : List α} (h : length l n) : take n l = l :=
take_length_le h
@[simp]
theorem take_left : l₁ l₂ : List α, take (length l₁) (l₁ ++ l₂) = l₁
| [], _ => rfl
| a :: l₁, l₂ => congrArg (cons a) (take_left l₁ l₂)
theorem take_left' {l₁ l₂ : List α} {n} (h : length l₁ = n) : take n (l₁ ++ l₂) = l₁ := by
rw [ h]; apply take_left
theorem take_take : (n m) (l : List α), take n (take m l) = take (min n m) l
| n, 0, l => by rw [Nat.min_zero, take_zero, take_nil]
| 0, m, l => by rw [Nat.zero_min, take_zero, take_zero]
| succ n, succ m, nil => by simp only [take_nil]
| succ n, succ m, a :: l => by
simp only [take, succ_min_succ, take_take n m l]
theorem take_replicate (a : α) : n m : Nat, take n (replicate m a) = replicate (min n m) a
| n, 0 => by simp [Nat.min_zero]
| 0, m => by simp [Nat.zero_min]
| succ n, succ m => by simp [succ_min_succ, take_replicate]
theorem map_take (f : α β) :
(L : List α) (i : Nat), (L.take i).map f = (L.map f).take i
| [], i => by simp
| _, 0 => by simp
| h :: t, n + 1 => by dsimp; rw [map_take f t n]
/-- Taking the first `n` elements in `l₁ ++ l₂` is the same as appending the first `n` elements
of `l₁` to the first `n - l₁.length` elements of `l₂`. -/
theorem take_append_eq_append_take {l₁ l₂ : List α} {n : Nat} :
take n (l₁ ++ l₂) = take n l₁ ++ take (n - l₁.length) l₂ := by
induction l₁ generalizing n
· simp
· cases n
· simp [*]
· simp only [cons_append, take_cons_succ, length_cons, succ_eq_add_one, cons.injEq,
append_cancel_left_eq, true_and, *]
congr 1
omega
theorem take_append_of_le_length {l₁ l₂ : List α} {n : Nat} (h : n l₁.length) :
(l₁ ++ l₂).take n = l₁.take n := by
simp [take_append_eq_append_take, Nat.sub_eq_zero_of_le h]
/-- Taking the first `l₁.length + i` elements in `l₁ ++ l₂` is the same as appending the first
`i` elements of `l₂` to `l₁`. -/
theorem take_append {l₁ l₂ : List α} (i : Nat) :
take (l₁.length + i) (l₁ ++ l₂) = l₁ ++ take i l₂ := by
rw [take_append_eq_append_take, take_all_of_le (Nat.le_add_right _ _), Nat.add_sub_cancel_left]
/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
length `> i`. Version designed to rewrite from the big list to the small list. -/
theorem get_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
get L i, hi = get (L.take j) i, length_take .. Nat.lt_min.mpr hj, hi :=
get_of_eq (take_append_drop j L).symm _ get_append ..
/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
length `> i`. Version designed to rewrite from the small list to the big list. -/
theorem get_take' (L : List α) {j i} :
get (L.take j) i =
get L i.1, Nat.lt_of_lt_of_le i.2 (length_take_le' _ _) := by
let i, hi := i; rw [length_take, Nat.lt_min] at hi; rw [get_take L _ hi.1]
theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.get? m := by
induction n generalizing l m with
| zero =>
exact absurd h (Nat.not_lt_of_le m.zero_le)
| succ _ hn =>
cases l with
| nil => simp only [take_nil]
| cons hd tl =>
cases m
· simp only [get?, take]
· simpa only using hn (Nat.lt_of_succ_lt_succ h)
theorem get?_take_eq_none {l : List α} {n m : Nat} (h : n m) :
(l.take n).get? m = none :=
get?_eq_none.mpr <| Nat.le_trans (length_take_le _ _) h
theorem get?_take_eq_if {l : List α} {n m : Nat} :
(l.take n).get? m = if m < n then l.get? m else none := by
split
· next h => exact get?_take h
· next h => exact get?_take_eq_none (Nat.le_of_not_lt h)
@[simp]
theorem nth_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1)).get? n = l.get? n :=
get?_take (Nat.lt_succ_self n)
theorem take_succ {l : List α} {n : Nat} : l.take (n + 1) = l.take n ++ (l.get? n).toList := by
induction l generalizing n with
| nil =>
simp only [Option.toList, get?, take_nil, append_nil]
| cons hd tl hl =>
cases n
· simp only [Option.toList, get?, eq_self_iff_true, take, nil_append]
· simp only [hl, cons_append, get?, eq_self_iff_true, take]
@[simp]
theorem take_eq_nil_iff {l : List α} {k : Nat} : l.take k = [] l = [] k = 0 := by
cases l <;> cases k <;> simp [Nat.succ_ne_zero]
@[simp]
theorem take_eq_take :
{l : List α} {m n : Nat}, l.take m = l.take n min m l.length = min n l.length
| [], m, n => by simp [Nat.min_zero]
| _ :: xs, 0, 0 => by simp
| x :: xs, m + 1, 0 => by simp [Nat.zero_min, succ_min_succ]
| x :: xs, 0, n + 1 => by simp [Nat.zero_min, succ_min_succ]
| x :: xs, m + 1, n + 1 => by simp [succ_min_succ, take_eq_take]; omega
theorem take_add (l : List α) (m n : Nat) : l.take (m + n) = l.take m ++ (l.drop m).take n := by
suffices take (m + n) (take m l ++ drop m l) = take m l ++ take n (drop m l) by
rw [take_append_drop] at this
assumption
rw [take_append_eq_append_take, take_all_of_le, append_right_inj]
· simp only [take_eq_take, length_take, length_drop]
omega
apply Nat.le_trans (m := m)
· apply length_take_le
· apply Nat.le_add_right
theorem take_eq_nil_of_eq_nil : {as : List α} {i}, as = [] as.take i = []
| _, _, rfl => take_nil
theorem ne_nil_of_take_ne_nil {as : List α} {i : Nat} (h: as.take i []) : as [] :=
mt take_eq_nil_of_eq_nil h
theorem dropLast_eq_take (l : List α) : l.dropLast = l.take l.length.pred := by
cases l with
| nil => simp [dropLast]
| cons x l =>
induction l generalizing x with
| nil => simp [dropLast]
| cons hd tl hl => simp [dropLast, hl]
theorem dropLast_take {n : Nat} {l : List α} (h : n < l.length) :
(l.take n).dropLast = l.take n.pred := by
simp only [dropLast_eq_take, length_take, Nat.le_of_lt h, take_take, pred_le, Nat.min_eq_left]
theorem map_eq_append_split {f : α β} {l : List α} {s₁ s₂ : List β}
(h : map f l = s₁ ++ s₂) : l₁ l₂, l = l₁ ++ l₂ map f l₁ = s₁ map f l₂ = s₂ := by
have := h
rw [ take_append_drop (length s₁) l] at this
rw [map_append] at this
refine _, _, rfl, append_inj this ?_
rw [length_map, length_take, Nat.min_eq_left]
rw [ length_map l f, h, length_append]
apply Nat.le_add_right
/-! ### drop -/
@[simp]
theorem drop_eq_nil_iff_le {l : List α} {k : Nat} : l.drop k = [] l.length k := by
refine' fun h => _, drop_eq_nil_of_le
induction k generalizing l with
| zero =>
simp only [drop] at h
simp [h]
| succ k hk =>
cases l
· simp
· simp only [drop] at h
simpa [Nat.succ_le_succ_iff] using hk h
theorem drop_length_cons {l : List α} (h : l []) (a : α) :
(a :: l).drop l.length = [l.getLast h] := by
induction l generalizing a with
| nil =>
cases h rfl
| cons y l ih =>
simp only [drop, length]
by_cases h₁ : l = []
· simp [h₁]
rw [getLast_cons' _ h₁]
exact ih h₁ y
/-- Dropping the elements up to `n` in `l₁ ++ l₂` is the same as dropping the elements up to `n`
in `l₁`, dropping the elements up to `n - l₁.length` in `l₂`, and appending them. -/
theorem drop_append_eq_append_drop {l₁ l₂ : List α} {n : Nat} :
drop n (l₁ ++ l₂) = drop n l₁ ++ drop (n - l₁.length) l₂ := by
induction l₁ generalizing n
· simp
· cases n
· simp [*]
· simp only [cons_append, drop_succ_cons, length_cons, succ_eq_add_one, append_cancel_left_eq, *]
congr 1
omega
theorem drop_append_of_le_length {l₁ l₂ : List α} {n : Nat} (h : n l₁.length) :
(l₁ ++ l₂).drop n = l₁.drop n ++ l₂ := by
simp [drop_append_eq_append_drop, Nat.sub_eq_zero_of_le h]
/-- Dropping the elements up to `l₁.length + i` in `l₁ + l₂` is the same as dropping the elements
up to `i` in `l₂`. -/
@[simp]
theorem drop_append {l₁ l₂ : List α} (i : Nat) : drop (l₁.length + i) (l₁ ++ l₂) = drop i l₂ := by
rw [drop_append_eq_append_drop, drop_eq_nil_of_le] <;>
simp [Nat.add_sub_cancel_left, Nat.le_add_right]
theorem drop_sizeOf_le [SizeOf α] (l : List α) (n : Nat) : sizeOf (l.drop n) sizeOf l := by
induction l generalizing n with
| nil => rw [drop_nil]; apply Nat.le_refl
| cons _ _ lih =>
induction n with
| zero => apply Nat.le_refl
| succ n =>
exact Trans.trans (lih _) (Nat.le_add_left _ _)
theorem lt_length_drop (L : List α) {i j : Nat} (h : i + j < L.length) : j < (L.drop i).length := by
have A : i < L.length := Nat.lt_of_le_of_lt (Nat.le.intro rfl) h
rw [(take_append_drop i L).symm] at h
simpa only [Nat.le_of_lt A, Nat.min_eq_left, Nat.add_lt_add_iff_left, length_take,
length_append] using h
/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
dropping the first `i` elements. Version designed to rewrite from the big list to the small list. -/
theorem get_drop (L : List α) {i j : Nat} (h : i + j < L.length) :
get L i + j, h = get (L.drop i) j, lt_length_drop L h := by
have : i L.length := Nat.le_trans (Nat.le_add_right _ _) (Nat.le_of_lt h)
rw [get_of_eq (take_append_drop i L).symm i + j, h, get_append_right'] <;>
simp [Nat.min_eq_left this, Nat.add_sub_cancel_left, Nat.le_add_right]
/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/
theorem get_drop' (L : List α) {i j} :
get (L.drop i) j = get L i + j, by
rw [Nat.add_comm]
exact Nat.add_lt_of_lt_sub (length_drop i L j.2) := by
rw [get_drop]
@[simp]
theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) := by
ext
simp only [get?_eq_some, get_drop', Option.mem_def]
constructor <;> intro h, ha
· exact _, ha
· refine ?_, ha
rw [length_drop]
rw [Nat.add_comm] at h
apply Nat.lt_sub_of_add_lt h
@[simp] theorem drop_drop (n : Nat) : (m) (l : List α), drop n (drop m l) = drop (n + m) l
| m, [] => by simp
| 0, l => by simp
| m + 1, a :: l =>
calc
drop n (drop (m + 1) (a :: l)) = drop n (drop m l) := rfl
_ = drop (n + m) l := drop_drop n m l
_ = drop (n + (m + 1)) (a :: l) := rfl
theorem take_drop : (m n : Nat) (l : List α), take n (drop m l) = drop m (take (m + n) l)
| 0, _, _ => by simp
| _, _, [] => by simp
| _+1, _, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop ..
theorem drop_take : (m n : Nat) (l : List α), drop n (take m l) = take (m - n) (drop n l)
| 0, _, _ => by simp
| _, 0, _ => by simp
| _, _, [] => by simp
| m+1, n+1, h :: t => by
simp [take_succ_cons, drop_succ_cons, drop_take m n t]
congr 1
omega
theorem map_drop (f : α β) :
(L : List α) (i : Nat), (L.drop i).map f = (L.map f).drop i
| [], i => by simp
| L, 0 => by simp
| h :: t, n + 1 => by
dsimp
rw [map_drop f t]
theorem reverse_take {α} {xs : List α} (n : Nat) (h : n xs.length) :
xs.reverse.take n = (xs.drop (xs.length - n)).reverse := by
induction xs generalizing n <;>
simp only [reverse_cons, drop, reverse_nil, Nat.zero_sub, length, take_nil]
next xs_hd xs_tl xs_ih =>
cases Nat.lt_or_eq_of_le h with
| inl h' =>
have h' := Nat.le_of_succ_le_succ h'
rw [take_append_of_le_length, xs_ih _ h']
rw [show xs_tl.length + 1 - n = succ (xs_tl.length - n) from _, drop]
· rwa [succ_eq_add_one, Nat.sub_add_comm]
· rwa [length_reverse]
| inr h' =>
subst h'
rw [length, Nat.sub_self, drop]
suffices xs_tl.length + 1 = (xs_tl.reverse ++ [xs_hd]).length by
rw [this, take_length, reverse_cons]
rw [length_append, length_reverse]
rfl
@[simp]
theorem get_cons_drop : (l : List α) i, get l i :: drop (i + 1) l = drop i l
| _::_, 0, _ => rfl
| _::_, i+1, _ => get_cons_drop _ i, _
theorem drop_eq_get_cons {n} {l : List α} (h) : drop n l = get l n, h :: drop (n + 1) l :=
(get_cons_drop _ n, h).symm
theorem drop_eq_nil_of_eq_nil : {as : List α} {i}, as = [] as.drop i = []
| _, _, rfl => drop_nil
theorem ne_nil_of_drop_ne_nil {as : List α} {i : Nat} (h: as.drop i []) : as [] :=
mt drop_eq_nil_of_eq_nil h
/-! ### zipWith -/
@[simp] theorem length_zipWith (f : α β γ) (l₁ l₂) :
length (zipWith f l₁ l₂) = min (length l₁) (length l₂) := by
induction l₁ generalizing l₂ <;> cases l₂ <;>
simp_all [succ_min_succ, Nat.zero_min, Nat.min_zero]
/-! ### zip -/
@[simp] theorem length_zip (l₁ : List α) (l₂ : List β) :
length (zip l₁ l₂) = min (length l₁) (length l₂) := by
simp [zip]
end List

View File

@@ -402,12 +402,12 @@ theorem and_pow_two_identity {x : Nat} (lt : x < 2^n) : x &&& 2^n-1 = x := by
/-! ### lor -/
@[simp] theorem zero_or (x : Nat) : 0 ||| x = x := by
@[simp] theorem or_zero (x : Nat) : 0 ||| x = x := by
simp only [HOr.hOr, OrOp.or, lor]
unfold bitwise
simp [@eq_comm _ 0]
@[simp] theorem or_zero (x : Nat) : x ||| 0 = x := by
@[simp] theorem zero_or (x : Nat) : x ||| 0 = x := by
simp only [HOr.hOr, OrOp.or, lor]
unfold bitwise
simp [@eq_comm _ 0]

View File

@@ -24,51 +24,23 @@ instance : LT String :=
instance decLt (s₁ s₂ : @& String) : Decidable (s₁ < s₂) :=
List.hasDecidableLt s₁.data s₂.data
/--
Returns the length of a string in Unicode code points.
Examples:
* `"".length = 0`
* `"abc".length = 3`
* `"L∃∀N".length = 4`
-/
@[extern "lean_string_length"]
def length : (@& String) Nat
| s => s.length
/--
Pushes a character onto the end of a string.
The internal implementation uses dynamic arrays and will perform destructive updates
if the string is not shared.
Example: `"abc".push 'd' = "abcd"`
-/
/-- The internal implementation uses dynamic arrays and will perform destructive updates
if the String is not shared. -/
@[extern "lean_string_push"]
def push : String Char String
| s, c => s ++ [c]
/--
Appends two strings.
The internal implementation uses dynamic arrays and will perform destructive updates
if the string is not shared.
Example: `"abc".append "def" = "abcdef"`
-/
/-- The internal implementation uses dynamic arrays and will perform destructive updates
if the String is not shared. -/
@[extern "lean_string_append"]
def append : String (@& String) String
| a, b => a ++ b
/--
Converts a string to a list of characters.
Even though the logical model of strings is as a structure that wraps a list of characters,
this operation takes time and space linear in the length of the string, because the compiler
uses an optimized representation as dynamic arrays.
Example: `"abc".toList = ['a', 'b', 'c']`
-/
/-- O(n) in the runtime, where n is the length of the String -/
def toList (s : String) : List Char :=
s.data
@@ -87,17 +59,9 @@ def utf8GetAux : List Char → Pos → Pos → Char
| c::cs, i, p => if i = p then c else utf8GetAux cs (i + c) p
/--
Returns the character at position `p` of a string. If `p` is not a valid position,
returns `(default : Char)`.
See `utf8GetAux` for the reference implementation.
Examples:
* `"abc".get ⟨1⟩ = 'b'`
* `"abc".get ⟨3⟩ = (default : Char) = 'A'`
Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8
character. For example,`"L∃∀N".get ⟨2⟩ = (default : Char) = 'A'`.
Return character at position `p`. If `p` is not a valid position
returns `(default : Char)`.
See `utf8GetAux` for the reference implementation.
-/
@[extern "lean_string_utf8_get"]
def get (s : @& String) (p : @& Pos) : Char :=
@@ -108,30 +72,12 @@ def utf8GetAux? : List Char → Pos → Pos → Option Char
| [], _, _ => none
| c::cs, i, p => if i = p then c else utf8GetAux? cs (i + c) p
/--
Returns the character at position `p`. If `p` is not a valid position, returns `none`.
Examples:
* `"abc".get? ⟨1⟩ = some 'b'`
* `"abc".get? ⟨3⟩ = none`
Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8
character. For example, `"L∃∀N".get? ⟨2⟩ = none`
-/
@[extern "lean_string_utf8_get_opt"]
def get? : (@& String) (@& Pos) Option Char
| s, p => utf8GetAux? s 0 p
/--
Returns the character at position `p` of a string. If `p` is not a valid position,
returns `(default : Char)` and produces a panic error message.
Examples:
* `"abc".get! ⟨1⟩ = 'b'`
* `"abc".get! ⟨3⟩` panics
Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8 character. For example,
`"L∃∀N".get! ⟨2⟩` panics.
Similar to `get`, but produces a panic error message if `p` is not a valid `String.Pos`.
-/
@[extern "lean_string_utf8_get_bang"]
def get! (s : @& String) (p : @& Pos) : Char :=
@@ -143,48 +89,13 @@ def utf8SetAux (c' : Char) : List Char → Pos → Pos → List Char
| c::cs, i, p =>
if i = p then (c'::cs) else c::(utf8SetAux c' cs (i + c) p)
/--
Replaces the character at a specified position in a string with a new character. If the position
is invalid, the string is returned unchanged.
If both the replacement character and the replaced character are ASCII characters and the string
is not shared, destructive updates are used.
Examples:
* `"abc".set ⟨1⟩ 'B' = "aBc"`
* `"abc".set ⟨3⟩ 'D' = "abc"`
* `"L∃∀N".set ⟨4⟩ 'X' = "L∃XN"`
Because `'∃'` is a multi-byte character, the byte index `2` in `L∃∀N` is an invalid position,
so `"L∃∀N".set ⟨2⟩ 'X' = "L∃∀N"`.
-/
@[extern "lean_string_utf8_set"]
def set : String (@& Pos) Char String
| s, i, c => utf8SetAux c s 0 i
/--
Replaces the character at position `p` in the string `s` with the result of applying `f` to that character.
If `p` is an invalid position, the string is returned unchanged.
Examples:
* `abc.modify ⟨1⟩ Char.toUpper = "aBc"`
* `abc.modify ⟨3⟩ Char.toUpper = "abc"`
-/
def modify (s : String) (i : Pos) (f : Char Char) : String :=
s.set i <| f <| s.get i
/--
Returns the next position in a string after position `p`. If `p` is not a valid position or `p = s.endPos`,
the result is unspecified.
Examples:
* `"abc".next ⟨1⟩ = String.Pos.mk 2`
* `"L∃∀N".next ⟨1⟩ = String.Pos.mk 4`, since `'∃'` is a multi-byte UTF-8 character
Cases where the result is unspecified:
* `"abc".next ⟨3⟩`, since `3 = s.endPos`
* `"L∃∀N".next ⟨2⟩`, since `2` points into the middle of a multi-byte UTF-8 character
-/
@[extern "lean_string_utf8_next"]
def next (s : @& String) (p : @& Pos) : Pos :=
let c := get s p

View File

@@ -132,17 +132,13 @@ theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext)
cases i; rename_i s pos; simp [Iterator.next, Iterator.sizeOf_eq]; simp [Iterator.hasNext] at h
exact Nat.sub_lt_sub_left h (String.lt_next s pos)
macro_rules
| `(tactic| decreasing_trivial) =>
`(tactic| with_reducible apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption)
theorem Iterator.sizeOf_next_lt_of_atEnd (i : String.Iterator) (h : ¬ i.atEnd = true) : sizeOf i.next < sizeOf i :=
have h : i.hasNext := decide_eq_true <| Nat.gt_of_not_le <| mt decide_eq_true h
sizeOf_next_lt_of_hasNext i h
macro_rules
| `(tactic| decreasing_trivial) =>
`(tactic| with_reducible apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)
namespace Iterator

View File

@@ -1057,7 +1057,6 @@ where
else
Syntax.mkCApp (Name.mkStr2 "Array" ("mkArray" ++ toString xs.size)) args
termination_by xs.size - i
decreasing_by decreasing_trivial_pre_omega
instance [Quote α `term] : Quote (Array α) `term where
quote := quoteArray

View File

@@ -296,7 +296,7 @@ macro_rules | `($x - $y) => `(binop% HSub.hSub $x $y)
macro_rules | `($x * $y) => `(binop% HMul.hMul $x $y)
macro_rules | `($x / $y) => `(binop% HDiv.hDiv $x $y)
macro_rules | `($x % $y) => `(binop% HMod.hMod $x $y)
-- exponentiation should be considered a right action (#2854)
-- exponentiation should be considered a right action (#2220)
macro_rules | `($x ^ $y) => `(rightact% HPow.hPow $x $y)
macro_rules | `($x ++ $y) => `(binop% HAppend.hAppend $x $y)
macro_rules | `(- $x) => `(unop% Neg.neg $x)
@@ -687,27 +687,4 @@ syntax (name := checkSimp) "#check_simp " term "~>" term : command
-/
syntax (name := checkSimpFailure) "#check_simp " term "!~>" : command
/--
The `seal foo` command ensures that the definition of `foo` is sealed, meaning it is marked as `[irreducible]`.
This command is particularly useful in contexts where you want to prevent the reduction of `foo` in proofs.
In terms of functionality, `seal foo` is equivalent to `attribute [local irreducible] foo`.
This attribute specifies that `foo` should be treated as irreducible only within the local scope,
which helps in maintaining the desired abstraction level without affecting global settings.
-/
syntax "seal " (ppSpace ident)+ : command
/--
The `unseal foo` command ensures that the definition of `foo` is unsealed, meaning it is marked as `[semireducible]`, the
default reducibility setting. This command is useful when you need to allow some level of reduction of `foo` in proofs.
Functionally, `unseal foo` is equivalent to `attribute [local semireducible] foo`.
Applying this attribute makes `foo` semireducible only within the local scope.
-/
syntax "unseal " (ppSpace ident)+ : command
macro_rules
| `(seal $fs:ident*) => `(attribute [local irreducible] $fs:ident*)
| `(unseal $fs:ident*) => `(attribute [local semireducible] $fs:ident*)
end Parser

View File

@@ -68,7 +68,7 @@ abbrev map (f : Int → Int) (xs : Coeffs) : Coeffs := List.map f xs
/-- Shim for `.enum.find?`. -/
abbrev findIdx? (f : Int Bool) (xs : Coeffs) : Option Nat :=
-- List.findIdx? f xs
-- We could avoid `Batteries.Data.List.Basic` by using the less efficient:
-- We could avoid `Std.Data.List.Basic` by using the less efficient:
xs.enum.find? (f ·.2) |>.map (·.1)
/-- Shim for `IntList.bmod`. -/
abbrev bmod (x : Coeffs) (m : Nat) : Coeffs := IntList.bmod x m

View File

@@ -4372,7 +4372,7 @@ def defaultMaxRecDepth := 512
/-- The message to display on stack overflow. -/
def maxRecDepthErrorMessage : String :=
"maximum recursion depth has been reached\nuse `set_option maxRecDepth <num>` to increase limit\nuse `set_option diagnostics true` to get diagnostic information"
"maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)"
namespace Syntax

View File

@@ -625,13 +625,7 @@ partial def FS.removeDirAll (p : FilePath) : IO Unit := do
namespace Process
/-- Returns the current working directory of the calling process. -/
@[extern "lean_io_process_get_current_dir"] opaque getCurrentDir : IO FilePath
/-- Sets the current working directory of the calling process. -/
@[extern "lean_io_process_set_current_dir"] opaque setCurrentDir (path : @& FilePath) : IO Unit
/-- Returns the process ID of the calling process. -/
/-- Returns the process ID of the current process. -/
@[extern "lean_io_process_get_pid"] opaque getPID : BaseIO UInt32
inductive Stdio where

View File

@@ -368,7 +368,7 @@ for new reflexive relations.
Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different
reflexivity theorems (e.g., `Iff.rfl`).
-/
macro "rfl" : tactic => `(tactic| case' _ => fail "The rfl tactic failed. Possible reasons:
macro "rfl" : tactic => `(tactic| fail "The rfl tactic failed. Possible reasons:
- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
- The arguments of the relation are not equal.
Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.")
@@ -835,7 +835,7 @@ syntax (name := renameI) "rename_i" (ppSpace colGt binderIdent)+ : tactic
/--
`repeat tac` repeatedly applies `tac` to the main goal until it fails.
That is, if `tac` produces multiple subgoals, only subgoals up to the first failure will be visited.
The `Batteries` library provides `repeat'` which repeats separately in each subgoal.
The `Std` library provides `repeat'` which repeats separately in each subgoal.
-/
syntax "repeat " tacticSeq : tactic
macro_rules
@@ -1266,7 +1266,7 @@ Optional arguments passed via a configuration argument as `solve_by_elim (config
but it is often useful to change to `.reducible`,
so semireducible definitions will not be unfolded when trying to apply a lemma.
See also the doc-comment for `Lean.Meta.Tactic.Backtrack.BacktrackConfig` for the options
See also the doc-comment for `Std.Tactic.BacktrackConfig` for the options
`proc`, `suspend`, and `discharge` which allow further customization of `solve_by_elim`.
Both `apply_assumption` and `apply_rules` are implemented via these hooks.
-/

View File

@@ -25,16 +25,9 @@ syntax "decreasing_trivial" : tactic
macro_rules | `(tactic| decreasing_trivial) => `(tactic| (simp (config := { arith := true, failIfUnchanged := false })) <;> done)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| omega)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| assumption)
/--
Variant of `decreasing_trivial` that does not use `omega`, intended to be used in core modules
before `omega` is available.
-/
syntax "decreasing_trivial_pre_omega" : tactic
macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a
macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i
macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt; assumption) -- i-1 < i if i ≠ 0
macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a
macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i
macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt; assumption) -- i-1 < i if i ≠ 0
/-- Constructs a proof of decreasing along a well founded relation, by applying
lexicographic order lemmas and using `ts` to solve the base case. If it fails,

View File

@@ -66,13 +66,12 @@ builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
descr := "builtin and foreign functions"
getParam := fun _ stx => syntaxToExternAttrData stx
afterSet := fun declName _ => do
let env getEnv
if env.isProjectionFn declName || env.isConstructor declName then
if let some (.thmInfo ..) := env.find? declName then
-- We should not mark theorems as extern
return ()
let env ofExcept <| addExtern env declName
let mut env getEnv
if env.isProjectionFn declName || env.isConstructor declName then do
env ofExcept <| addExtern env declName
setEnv env
else
pure ()
}
@[export lean_get_extern_attr_data]

View File

@@ -9,10 +9,9 @@ import Lean.Compiler.IR.CompilerM
import Lean.Compiler.IR.LiveVars
namespace Lean.IR.ExplicitRC
/-!
Insert explicit RC instructions. So, it assumes the input code does not contain `inc` nor `dec` instructions.
This transformation is applied before lower level optimizations
that introduce the instructions `release` and `set`
/-! Insert explicit RC instructions. So, it assumes the input code does not contain `inc` nor `dec` instructions.
This transformation is applied before lower level optimizations
that introduce the instructions `release` and `set`
-/
structure VarInfo where

View File

@@ -9,238 +9,152 @@ import Lean.Compiler.IR.LiveVars
import Lean.Compiler.IR.Format
namespace Lean.IR.ResetReuse
/-!
Remark: the insertResetReuse transformation is applied before we have
inserted `inc/dec` instructions, and performed lower level optimizations
that introduce the instructions `release` and `set`.
/-! Remark: the insertResetReuse transformation is applied before we have
inserted `inc/dec` instructions, and performed lower level optimizations
that introduce the instructions `release` and `set`. -/
/-! Remark: the functions `S`, `D` and `R` defined here implement the
corresponding functions in the paper "Counting Immutable Beans"
Here are the main differences:
- We use the State monad to manage the generation of fresh variable names.
- Support for join points, and `uset` and `sset` instructions for unboxed data.
- `D` uses the auxiliary function `Dmain`.
- `Dmain` returns a pair `(b, found)` to avoid quadratic behavior when checking
the last occurrence of the variable `x`.
- Because we have join points in the actual implementation, a variable may be live even if it
does not occur in a function body. See example at `livevars.lean`.
-/
/-!
Remark: the functions `S`, `D` and `R` defined here implement the
corresponding functions in the paper "Counting Immutable Beans"
Here are the main differences:
- We use the State monad to manage the generation of fresh variable names.
- Support for join points, and `uset` and `sset` instructions for unboxed data.
- `D` uses the auxiliary function `Dmain`.
- `Dmain` returns a pair `(b, found)` to avoid quadratic behavior when checking
the last occurrence of the variable `x`.
- Because we have join points in the actual implementation, a variable may be live even if it
does not occur in a function body. See example at `livevars.lean`.
-/
private def mayReuse (c₁ c₂ : CtorInfo) (relaxedReuse : Bool) : Bool :=
private def mayReuse (c₁ c₂ : CtorInfo) : Bool :=
c₁.size == c₂.size && c₁.usize == c₂.usize && c₁.ssize == c₂.ssize &&
/- The following condition is a heuristic.
If `relaxedReuse := false`, then we don't want to reuse cells from
different constructors even when they are compatible
We don't want to reuse cells from different types even when they are compatible
because it produces counterintuitive behavior. -/
(relaxedReuse || c₁.name.getPrefix == c₂.name.getPrefix)
c₁.name.getPrefix == c₂.name.getPrefix
/--
Replace `ctor` applications with `reuse` applications if compatible.
`w` contains the "memory cell" being reused.
-/
private partial def S (w : VarId) (c : CtorInfo) (relaxedReuse : Bool) (b : FnBody) : FnBody :=
go b
where
go : FnBody FnBody
| .vdecl x t v@(.ctor c' ys) b =>
if mayReuse c c' relaxedReuse then
private partial def S (w : VarId) (c : CtorInfo) : FnBody FnBody
| FnBody.vdecl x t v@(Expr.ctor c' ys) b =>
if mayReuse c c' then
let updtCidx := c.cidx != c'.cidx
.vdecl x t (.reuse w c' updtCidx ys) b
FnBody.vdecl x t (Expr.reuse w c' updtCidx ys) b
else
.vdecl x t v (go b)
| .jdecl j ys v b =>
let v' := go v
if v == v' then
.jdecl j ys v (go b)
else
.jdecl j ys v' b
| .case tid x xType alts =>
.case tid x xType <| alts.map fun alt => alt.modifyBody go
FnBody.vdecl x t v (S w c b)
| FnBody.jdecl j ys v b =>
let v' := S w c v
if v == v' then FnBody.jdecl j ys v (S w c b)
else FnBody.jdecl j ys v' b
| FnBody.case tid x xType alts => FnBody.case tid x xType <| alts.map fun alt => alt.modifyBody (S w c)
| b =>
if b.isTerminal then
b
else
let (instr, b) := b.split
instr.setBody (go b)
structure Context where
lctx : LocalContext := {}
/--
Contains all variables in `cases` statements in the current path
and variables that are already in `reset` statements when we
invoke `R`.
We use this information to prevent double-reset in code such as
```
case x_i : obj of
Prod.mk →
case x_i : obj of
Prod.mk →
...
```
A variable can already be in a `reset` statement when we
invoke `R` because we execute it with and without `relaxedReuse`.
-/
alreadyFound : PHashSet VarId := {}
/--
If `relaxedReuse := true`, then allow memory cells from different
constructors to be reused. For example, we can reuse a `PSigma.mk`
to allocate a `Prod.mk`. To avoid counterintuitive behavior,
we first try `relaxedReuse := false`, and then `relaxedReuse := true`.
-/
relaxedReuse : Bool := false
if b.isTerminal then b
else let
(instr, b) := b.split
instr.setBody (S w c b)
/-- We use `Context` to track join points in scope. -/
abbrev M := ReaderT Context (StateT Index Id)
abbrev M := ReaderT LocalContext (StateT Index Id)
private def mkFresh : M VarId := do
let idx getModify fun n => n + 1
return { idx := idx }
let idx getModify (fun n => n + 1)
pure { idx := idx }
/--
Helper function for applying `S`. We only introduce a `reset` if we managed
to replace a `ctor` withe `reuse` in `b`.
-/
private def tryS (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody := do
let w mkFresh
let b' := S w c ( read).relaxedReuse b
if b == b' then
return b
else
return .vdecl w IRType.object (.reset c.size x) b'
let b' := S w c b
if b == b' then pure b
else pure $ FnBody.vdecl w IRType.object (Expr.reset c.size x) b'
private def Dfinalize (x : VarId) (c : CtorInfo) : FnBody × Bool M FnBody
| (b, true) => return b
| (b, true) => pure b
| (b, false) => tryS x c b
private def argsContainsVar (ys : Array Arg) (x : VarId) : Bool :=
ys.any fun arg => match arg with
| .var y => x == y
| _ => false
| Arg.var y => x == y
| _ => false
private def isCtorUsing (b : FnBody) (x : VarId) : Bool :=
match b with
| .vdecl _ _ (.ctor _ ys) _ => argsContainsVar ys x
| (FnBody.vdecl _ _ (Expr.ctor _ ys) _) => argsContainsVar ys x
| _ => false
/--
Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`,
and `flag == true` if `x` is live in `b`.
/-- Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`,
and `flag == true` if `x` is live in `b`.
Note that, in the function `D` defined in the paper, for each `let x := e; F`,
`D` checks whether `x` is live in `F` or not. This is great for clarity but it
is expensive: `O(n^2)` where `n` is the size of the function body. -/
private partial def Dmain (x : VarId) (c : CtorInfo) (e : FnBody) : M (FnBody × Bool) := do
match e with
| .case tid y yType alts =>
if e.hasLiveVar ( read).lctx x then
Note that, in the function `D` defined in the paper, for each `let x := e; F`,
`D` checks whether `x` is live in `F` or not. This is great for clarity but it
is expensive: `O(n^2)` where `n` is the size of the function body. -/
private partial def Dmain (x : VarId) (c : CtorInfo) : FnBody M (FnBody × Bool)
| e@(FnBody.case tid y yType alts) => do
let ctx read
if e.hasLiveVar ctx x then do
/- If `x` is live in `e`, we recursively process each branch. -/
let alts alts.mapM fun alt => alt.mmodifyBody fun b => Dmain x c b >>= Dfinalize x c
return (.case tid y yType alts, true)
else
return (e, false)
| .jdecl j ys v b =>
let (b, found) withReader (fun ctx => { ctx with lctx := ctx.lctx.addJP j ys v }) (Dmain x c b)
pure (FnBody.case tid y yType alts, true)
else pure (e, false)
| FnBody.jdecl j ys v b => do
let (b, found) withReader (fun ctx => ctx.addJP j ys v) (Dmain x c b)
let (v, _ /- found' -/) Dmain x c v
/- If `found' == true`, then `Dmain b` must also have returned `(b, true)` since
we assume the IR does not have dead join points. So, if `x` is live in `j` (i.e., `v`),
then it must also live in `b` since `j` is reachable from `b` with a `jmp`.
On the other hand, `x` may be live in `b` but dead in `j` (i.e., `v`). -/
return (.jdecl j ys v b, found)
| e =>
pure (FnBody.jdecl j ys v b, found)
| e => do
let ctx read
if e.isTerminal then
return (e, e.hasLiveVar ( read).lctx x)
pure (e, e.hasLiveVar ctx x)
else do
let (instr, b) := e.split
if isCtorUsing instr x then
/- If the scrutinee `x` (the one that is providing memory) is being
stored in a constructor, then reuse will probably not be able to reuse memory at runtime.
It may work only if the new cell is consumed, but we ignore this case. -/
return (e, true)
pure (e, true)
else
let (b, found) Dmain x c b
/- Remark: it is fine to use `hasFreeVar` instead of `hasLiveVar`
since `instr` is not a `FnBody.jmp` (it is not a terminal) nor
it is a `FnBody.jdecl`. -/
since `instr` is not a `FnBody.jmp` (it is not a terminal) nor it is a `FnBody.jdecl`. -/
if found || !instr.hasFreeVar x then
return (instr.setBody b, found)
pure (instr.setBody b, found)
else
let b tryS x c b
return (instr.setBody b, true)
pure (instr.setBody b, true)
private def D (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody :=
Dmain x c b >>= Dfinalize x c
partial def R (e : FnBody) : M FnBody := do
match e with
| .case tid x xType alts =>
let alreadyFound := ( read).alreadyFound.contains x
withReader (fun ctx => { ctx with alreadyFound := ctx.alreadyFound.insert x }) do
partial def R : FnBody M FnBody
| FnBody.case tid x xType alts => do
let alts alts.mapM fun alt => do
let alt alt.mmodifyBody R
match alt with
| .ctor c b =>
if c.isScalar || alreadyFound then
-- If `alreadyFound`, then we don't try to reuse memory cell to avoid
-- double reset.
return alt
else
.ctor c <$> D x c b
| _ => return alt
return .case tid x xType alts
| .jdecl j ys v b =>
| Alt.ctor c b =>
if c.isScalar then pure alt
else Alt.ctor c <$> D x c b
| _ => pure alt
pure $ FnBody.case tid x xType alts
| FnBody.jdecl j ys v b => do
let v R v
let b withReader (fun ctx => { ctx with lctx := ctx.lctx.addJP j ys v }) (R b)
return .jdecl j ys v b
| e =>
if e.isTerminal then
return e
else
let b withReader (fun ctx => ctx.addJP j ys v) (R b)
pure $ FnBody.jdecl j ys v b
| e => do
if e.isTerminal then pure e
else do
let (instr, b) := e.split
let b R b
return instr.setBody b
abbrev N := StateT (PHashSet VarId) Id
partial def collectResets (e : FnBody) : N Unit := do
match e with
| .case _ _ _ alts => alts.forM fun alt => collectResets alt.body
| .jdecl _ _ v b => collectResets v; collectResets b
| .vdecl _ _ (.reset _ x) b => modify fun s => s.insert x; collectResets b
| e => unless e.isTerminal do
let (_, b) := e.split
collectResets b
pure (instr.setBody b)
end ResetReuse
open ResetReuse
def Decl.insertResetReuseCore (d : Decl) (relaxedReuse : Bool) : Decl :=
def Decl.insertResetReuse (d : Decl) : Decl :=
match d with
| .fdecl (body := b) .. =>
| .fdecl (body := b) ..=>
let nextIndex := d.maxIndex + 1
-- First time we execute `insertResetReuseCore`, `relaxedReuse := false`.
let alreadyFound : PHashSet VarId := if relaxedReuse then (collectResets b *> get).run' {} else {}
let bNew := R b { relaxedReuse, alreadyFound } |>.run' nextIndex
let bNew := (R b {}).run' nextIndex
d.updateBody! bNew
| other => other
def Decl.insertResetReuse (d : Decl) : Decl :=
/-
We execute the reset/reuse algorithm twice. The first time, we only reuse memory cells
between identical constructor memory cells. That is, we do not reuse a `PSigma.mk` memory cell
when allocating a `Prod.mk` memory cell, even though they have the same layout. Recall
that the reset/reuse placement algorithm is a heuristic, and the first pass prevents reuses
that are unlikely to be useful at runtime. Then, we run the procedure again,
relaxing this restriction. If there are still opportunities for reuse, we will take advantage of them.
The second pass addresses issue #4089.
-/
d.insertResetReuseCore (relaxedReuse := false)
|>.insertResetReuseCore (relaxedReuse := true)
end Lean.IR

View File

@@ -13,25 +13,13 @@ import Lean.Elab.InfoTree.Types
import Lean.MonadEnv
namespace Lean
register_builtin_option diagnostics : Bool := {
defValue := false
group := "diagnostics"
descr := "collect diagnostic information"
}
register_builtin_option diagnostics.threshold : Nat := {
defValue := 20
group := "diagnostics"
descr := "only diagnostic counters above this threshold are reported by the definitional equality"
}
namespace Core
register_builtin_option maxHeartbeats : Nat := {
defValue := 200000
descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
}
namespace Core
builtin_initialize registerTraceClass `Kernel
def getMaxHeartbeats (opts : Options) : Nat :=
@@ -84,11 +72,6 @@ structure Context where
Recall that runtime exceptions are `maxRecDepth` or `maxHeartbeats`.
-/
catchRuntimeEx : Bool := false
/--
If `diag := true`, different parts of the system collect diagnostics.
Use the `set_option diag true` to set it to true.
-/
diag : Bool := false
deriving Nonempty
/-- CoreM is a monad for manipulating the Lean environment.
@@ -121,22 +104,7 @@ instance : MonadOptions CoreM where
getOptions := return ( read).options
instance : MonadWithOptions CoreM where
withOptions f x := do
let options := f ( read).options
let diag := diagnostics.get options
if Kernel.isDiagnosticsEnabled ( getEnv) != diag then
modifyEnv fun env => Kernel.enableDiag env diag
withReader
(fun ctx =>
{ ctx with
options
diag
maxRecDepth := maxRecDepth.get options })
x
-- Helper function for ensuring fields that depend on `options` have the correct value.
@[inline] private def withConsistentCtx (x : CoreM α) : CoreM α := do
withOptions id x
withOptions f x := withReader (fun ctx => { ctx with options := f ctx.options }) x
instance : AddMessageContext CoreM where
addMessageContext := addMessageContextPartial
@@ -224,7 +192,7 @@ def mkFreshUserName (n : Name) : CoreM Name :=
mkFreshNameImp n
@[inline] def CoreM.run (x : CoreM α) (ctx : Context) (s : State) : EIO Exception (α × State) :=
((withConsistentCtx x) ctx).run s
(x ctx).run s
@[inline] def CoreM.run' (x : CoreM α) (ctx : Context) (s : State) : EIO Exception α :=
Prod.fst <$> x.run ctx s
@@ -238,7 +206,7 @@ def mkFreshUserName (n : Name) : CoreM Name :=
instance [MetaEval α] : MetaEval (CoreM α) where
eval env opts x _ := do
let x : CoreM α := do try x finally printTraces
let (a, s) (withConsistentCtx x).toIO { fileName := "<CoreM>", fileMap := default, options := opts } { env := env }
let (a, s) x.toIO { maxRecDepth := maxRecDepth.get opts, options := opts, fileName := "<CoreM>", fileMap := default } { env := env }
MetaEval.eval s.env opts a (hideUnit := true)
-- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`
@@ -251,7 +219,7 @@ protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m
throw <| Exception.error .missing "elaboration interrupted"
def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do
let msg := s!"(deterministic) timeout at `{moduleName}`, maximum number of heartbeats ({max/1000}) has been reached\nuse `set_option {optionName} <num>` to set the limit\nuse `set_option {diagnostics.name} true` to get diagnostic information"
let msg := s!"(deterministic) timeout at '{moduleName}', maximum number of heartbeats ({max/1000}) has been reached (use 'set_option {optionName} <num>' to set the limit)"
throw <| Exception.error ( getRef) (MessageData.ofFormat (Std.Format.text msg))
def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat) : CoreM Unit := do
@@ -404,16 +372,9 @@ def addAndCompile (decl : Declaration) : CoreM Unit := do
addDecl decl;
compileDecl decl
def getDiag (opts : Options) : Bool :=
diagnostics.get opts
/-- Return `true` if diagnostic information collection is enabled. -/
def isDiagnosticsEnabled : CoreM Bool :=
return ( read).diag
def ImportM.runCoreM (x : CoreM α) : ImportM α := do
let ctx read
let (a, _) (withOptions (fun _ => ctx.opts) x).toIO { fileName := "<ImportM>", fileMap := default } { env := ctx.env }
let (a, _) x.toIO { options := ctx.opts, fileName := "<ImportM>", fileMap := default } { env := ctx.env }
return a
/-- Return `true` if the exception was generated by one our resource limits. -/

View File

@@ -92,7 +92,6 @@ def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β)) (targ
moveEntries (i+1) source target
else target
termination_by source.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
let bucketsNew : HashMapBucket α β :=

View File

@@ -84,7 +84,6 @@ def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (target : Has
else
target
termination_by source.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
let bucketsNew : HashSetBucket α :=

View File

@@ -135,11 +135,6 @@ structure TheoremVal extends ConstantVal where
all : List Name := [name]
deriving Inhabited, BEq
@[export lean_mk_theorem_val]
def mkTheoremValEx (name : Name) (levelParams : List Name) (type : Expr) (value : Expr) (all : List Name) : TheoremVal := {
name, levelParams, type, value, all
}
/-- Value for an opaque constant declaration `opaque x : t := e` -/
structure OpaqueVal extends ConstantVal where
value : Expr

View File

@@ -70,34 +70,30 @@ def kindOfBinderName (binderName : Name) : LocalDeclKind :=
else
.default
partial def quoteAutoTactic : Syntax CoreM Expr
| .ident _ _ val preresolved =>
return mkApp4 (.const ``Syntax.ident [])
(.const ``SourceInfo.none [])
(.app (.const ``String.toSubstring []) (mkStrLit (toString val)))
(toExpr val)
(toExpr preresolved)
partial def quoteAutoTactic : Syntax TermElabM Syntax
| stx@(.ident ..) => throwErrorAt stx "invalid auto tactic, identifier is not allowed"
| stx@(.node _ k args) => do
if stx.isAntiquot then
throwErrorAt stx "invalid auto tactic, antiquotation is not allowed"
else
let ty := .const ``Syntax []
let mut quotedArgs := mkApp (.const ``Array.empty [.zero]) ty
let mut quotedArgs `(Array.empty)
for arg in args do
if k == nullKind && (arg.isAntiquotSuffixSplice || arg.isAntiquotSplice) then
throwErrorAt arg "invalid auto tactic, antiquotation is not allowed"
else
let quotedArg quoteAutoTactic arg
quotedArgs := mkApp3 (.const ``Array.push [.zero]) ty quotedArgs quotedArg
return mkApp3 (.const ``Syntax.node []) (.const ``SourceInfo.none []) (toExpr k) quotedArgs
| .atom _ val => return .app (.const ``mkAtom []) (toExpr val)
quotedArgs `(Array.push $quotedArgs $quotedArg)
`(Syntax.node SourceInfo.none $(quote k) $quotedArgs)
| .atom _ val => `(mkAtom $(quote val))
| .missing => throwError "invalid auto tactic, tactic is missing"
def declareTacticSyntax (tactic : Syntax) : TermElabM Name :=
withFreshMacroScope do
let name MonadQuotation.addMacroScope `_auto
let type := Lean.mkConst `Lean.Syntax
let value quoteAutoTactic tactic
let tactic quoteAutoTactic tactic
let value elabTerm tactic type
let value instantiateMVars value
trace[Elab.autoParam] value
let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := .opaque,
safety := DefinitionSafety.safe }

View File

@@ -388,7 +388,7 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
return ( mkEqRec motive h ( mkEqSymm heq), none)
let motive mkMotive lhs expectedAbst
if badMotive?.isSome || !( isTypeCorrect motive) then
-- Before failing try to use `subst`
-- Before failing try tos use `subst`
if (isSubstCandidate lhs rhs <||> isSubstCandidate rhs lhs) then
withLocalIdentFor heqStx heq fun heqStx => do
let h instantiateMVars h
@@ -408,13 +408,7 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
| none =>
let h elabTerm hStx none
let hType inferType h
let mut hTypeAbst kabstract hType lhs
unless hTypeAbst.hasLooseBVars do
hTypeAbst kabstract hType rhs
unless hTypeAbst.hasLooseBVars do
throwError "invalid `▸` notation, the equality{indentExpr heq}\nhas type {indentExpr heqType}\nbut neither side of the equality is mentioned in the type{indentExpr hType}"
heq mkEqSymm heq
(lhs, rhs) := (rhs, lhs)
let hTypeAbst kabstract hType lhs
let motive mkMotive lhs hTypeAbst
unless ( isTypeCorrect motive) do
throwError "invalid `▸` notation, failed to compute motive for the substitution"

View File

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Meta.Diagnostics
import Lean.Elab.Open
import Lean.Elab.SetOption
import Lean.Elab.Eval
@@ -314,12 +313,8 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
@[builtin_term_elab «set_option»] def elabSetOption : TermElab := fun stx expectedType? => do
let options Elab.elabSetOption stx[1] stx[3]
withOptions (fun _ => options) do
try
elabTerm stx[5] expectedType?
finally
if stx[1].getId == `diagnostics then
reportDiag
withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
elabTerm stx[5] expectedType?
@[builtin_term_elab withAnnotateTerm] def elabWithAnnotateTerm : TermElab := fun stx expectedType? => do
match stx with

View File

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Gabriel Ebner
-/
prelude
import Lean.Meta.Diagnostics
import Lean.Elab.Binders
import Lean.Elab.SyntheticMVars
import Lean.Elab.SetOption
@@ -128,6 +127,19 @@ def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severit
let endPos := ref.getTailPos?.getD pos
mkMessageCore ctx.fileName ctx.fileMap msgData severity pos endPos
private def mkCoreContext (ctx : Context) (s : State) (heartbeats : Nat) : Core.Context :=
let scope := s.scopes.head!
{ fileName := ctx.fileName
fileMap := ctx.fileMap
options := scope.opts
currRecDepth := ctx.currRecDepth
maxRecDepth := s.maxRecDepth
ref := ctx.ref
currNamespace := scope.currNamespace
openDecls := scope.openDecls
initHeartbeats := heartbeats
currMacroScope := ctx.currMacroScope }
private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceState : TraceState) : MessageLog := Id.run do
if traceState.traces.isEmpty then return log
let mut traces : HashMap (String.Pos × String.Pos) (Array MessageData) :=
@@ -153,49 +165,31 @@ private def addTraceAsMessages : CommandElabM Unit := do
traceState.traces := {}
}
private def runCore (x : CoreM α) : CommandElabM α := do
def liftCoreM (x : CoreM α) : CommandElabM α := do
let s get
let ctx read
let heartbeats IO.getNumHeartbeats
let env := Kernel.resetDiag s.env
let scope := s.scopes.head!
let coreCtx : Core.Context := {
fileName := ctx.fileName
fileMap := ctx.fileMap
currRecDepth := ctx.currRecDepth
maxRecDepth := s.maxRecDepth
ref := ctx.ref
currNamespace := scope.currNamespace
openDecls := scope.openDecls
initHeartbeats := heartbeats
currMacroScope := ctx.currMacroScope
options := scope.opts
}
let x : EIO _ _ := x.run coreCtx {
env
ngen := s.ngen
nextMacroScope := s.nextMacroScope
infoState.enabled := s.infoState.enabled
traceState := s.traceState
}
let Eα := Except Exception α
let x : CoreM Eα := try let a x; pure <| Except.ok a catch ex => pure <| Except.error ex
let x : EIO Exception (Eα × Core.State) := (ReaderT.run x (mkCoreContext ctx s heartbeats)).run { env := s.env, ngen := s.ngen, traceState := s.traceState, messages := {}, infoState.enabled := s.infoState.enabled }
let (ea, coreS) liftM x
modify fun s => { s with
env := coreS.env
nextMacroScope := coreS.nextMacroScope
ngen := coreS.ngen
infoState.trees := s.infoState.trees.append coreS.infoState.trees
env := coreS.env
ngen := coreS.ngen
messages := s.messages ++ coreS.messages
traceState.traces := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref }
messages := s.messages ++ coreS.messages
infoState.trees := s.infoState.trees.append coreS.infoState.trees
}
return ea
def liftCoreM (x : CoreM α) : CommandElabM α := do
MonadExcept.ofExcept ( runCore (observing x))
match ea with
| Except.ok a => pure a
| Except.error e => throw e
private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : Message :=
let ref := getBetterRef ref ctx.macroStack
mkMessageAux ctx ref (toString err) MessageSeverity.error
@[inline] def liftEIO {α} (x : EIO Exception α) : CommandElabM α := liftM x
@[inline] def liftIO {α} (x : IO α) : CommandElabM α := do
let ctx read
IO.toEIO (fun (ex : IO.Error) => Exception.error ctx.ref ex.toString) x
@@ -275,7 +269,7 @@ private def elabCommandUsing (s : State) (stx : Syntax) : List (KeyedDeclsAttrib
(fun _ => do set s; elabCommandUsing s stx elabFns)
/-- Elaborate `x` with `stx` on the macro stack -/
def withMacroExpansion (beforeStx afterStx : Syntax) (x : CommandElabM α) : CommandElabM α :=
def withMacroExpansion {α} (beforeStx afterStx : Syntax) (x : CommandElabM α) : CommandElabM α :=
withInfoContext (mkInfo := pure <| .ofMacroExpansionInfo { stx := beforeStx, output := afterStx, lctx := .empty }) do
withReader (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x
@@ -408,6 +402,7 @@ def printExpr (e : Expr) : MetaM Unit := do
def liftTermElabM (x : TermElabM α) : CommandElabM α := do
let ctx read
let s get
let heartbeats IO.getNumHeartbeats
-- dbg_trace "heartbeats: {heartbeats}"
let scope := s.scopes.head!
-- We execute `x` with an empty message log. Thus, `x` cannot modify/view messages produced by previous commands.
@@ -416,9 +411,18 @@ def liftTermElabM (x : TermElabM α) : CommandElabM α := do
-- make sure `observing` below also catches runtime exceptions (like we do by default in
-- `CommandElabM`)
let _ := MonadAlwaysExcept.except (m := TermElabM)
let x : MetaM _ := (observing (try x finally Meta.reportDiag)).run (mkTermContext ctx s) { levelNames := scope.levelNames }
let x : CoreM _ := x.run mkMetaContext {}
let ((ea, _), _) runCore x
let x : MetaM _ := (observing x).run (mkTermContext ctx s) { levelNames := scope.levelNames }
let x : CoreM _ := x.run mkMetaContext {}
let x : EIO _ _ := x.run (mkCoreContext ctx s heartbeats) { env := s.env, ngen := s.ngen, nextMacroScope := s.nextMacroScope, infoState.enabled := s.infoState.enabled, traceState := s.traceState }
let (((ea, _), _), coreS) liftEIO x
modify fun s => { s with
env := coreS.env
nextMacroScope := coreS.nextMacroScope
ngen := coreS.ngen
infoState.trees := s.infoState.trees.append coreS.infoState.trees
traceState.traces := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref }
messages := s.messages ++ coreS.messages
}
MonadExcept.ofExcept ea
/--

View File

@@ -70,8 +70,6 @@ where
if localDecl.binderInfo.isExplicit then
if ( inferType x).isAppOf indVal.name then
rhs `($rhs ++ Format.line ++ $(mkIdent auxFunName):ident $a:ident max_prec)
else if ( isType x <||> isProof x) then
rhs `($rhs ++ Format.line ++ "_")
else
rhs `($rhs ++ Format.line ++ reprArg $a)
patterns := patterns.push ( `(@$(mkIdent ctorName):ident $ctorArgs:term*))

View File

@@ -96,7 +96,7 @@ Here are brief descriptions of each of the operator types:
- `rightact% f a b` elaborates `f a b` as a right action (the `b` operand "acts upon" the `a` operand).
Only `a` participates in the protocol since `b` can have an unrelated type.
This is used by `HPow` since, for example, there are both `Real -> Nat -> Real` and `Real -> Real -> Real`
exponentiation functions, and we prefer the former in the case of `x ^ 2`, but `binop%` would choose the latter. (#2854)
exponentiation functions, and we prefer the former in the case of `x ^ 2`, but `binop%` would choose the latter. (#2220)
- There are also `binrel%` and `binrel_no_prop%` (see the docstring for `elabBinRelCore`).
The elaborator works as follows:
@@ -273,33 +273,7 @@ where
match ( get).max? with
| none => modify fun s => { s with max? := type }
| some max =>
/-
Remark: Previously, we used `withNewMCtxDepth` to prevent metavariables in `max` and `type` from being assigned.
Reason: This is a heuristic procedure for introducing coercions in scenarios such as:
- Given `(n : Nat) (i : Int)`, elaborate `n = i`. The coercion must be inserted at `n`.
Consider the elaboration problem `(n + 0) + i`, where the type of term `0` is a metavariable.
We do not want it to be elaborated as `(Int.ofNat n + Int.ofNat (0 : Nat)) + i`; instead, we prefer the result to be `(Int.ofNat n + (0 : Int)) + i`.
Here is another example where we avoid assigning metavariables: `max := BitVec n` and `type := BitVec ?m`.
However, the combination `withNewMCtxDepth <| isDefEqGuarded max type` introduced performance issues in several
Mathlib files because `isDefEq` was spending a lot of time unfolding definitions in `max` and `type` before failing.
To address this issue, we allowed only reducible definitions to be unfolded during this check, using
`withNewMCtxDepth <| withReducible <| isDefEqGuarded max type`. This change fixed some performance issues but created new ones.
Lean was now spending time trying to use `hasCoe`, likely occurring in places where `withNewMCtxDepth <| isDefEqGuarded max type`
used to succeed but was now failing after we introduced `withReducible`.
We then considered using just `isDefEqGuarded max type` and changing the definition of `isUnknown`. In the new definition,
the else-case would be `| e => e.hasExprMVar` instead of `| _ => false`. However, we could not even compile this repo using
this configuration. The problem arises because some files require coercions even when `max` contains metavariables,
for example: `max := Option ?m` and `type := Name`.
As a result, rather than restricting reducibility, we decided to set `Meta.Config.isDefEqStuckEx := true`.
This means that if `isDefEq` encounters a subproblem `?m =?= a` where `?m` is non-assignable, it aborts the test
instead of unfolding definitions.
-/
unless ( withNewMCtxDepth <| withConfig (fun config => { config with isDefEqStuckEx := true }) <| isDefEqGuarded max type) do
unless ( withNewMCtxDepth <| isDefEqGuarded max type) do
if ( hasCoe type max) then
return ()
else if ( hasCoe max type) then
@@ -475,7 +449,7 @@ def elabOp : TermElab := fun stx expectedType? => do
- `binrel% R x y` elaborates `R x y` using the `binop%/...` expression trees in both `x` and `y`.
It is similar to how `binop% R x y` elaborates but with a significant difference:
it does not use the expected type when computing the types of the operands.
it does not use the expected type when computing the types of the operads.
- `binrel_no_prop% R x y` elaborates `R x y` like `binrel% R x y`, but if the resulting type for `x` and `y`
is `Prop` they are coerced to `Bool`.
This is used for relations such as `==` which do not support `Prop`, but we still want

View File

@@ -686,8 +686,8 @@ private def computeFixedIndexBitMask (numParams : Nat) (indType : InductiveType)
maskRef.modify fun mask => mask.set! i false
for x in xs[numParams:] do
let xType inferType x
let cond (e : Expr) := indFVars.any (fun indFVar => e.getAppFn == indFVar)
xType.forEachWhere (stopWhenVisited := true) cond fun e => do
let cond (e : Expr) := indFVars.any (fun indFVar => e.getAppFn == indFVar) && e.getAppNumArgs > numParams
xType.forEachWhere cond fun e => do
let eArgs := e.getAppArgs
for i in [numParams:eArgs.size] do
if i >= typeArgs.size then
@@ -695,19 +695,6 @@ private def computeFixedIndexBitMask (numParams : Nat) (indType : InductiveType)
else
unless eArgs[i]! == typeArgs[i]! do
maskRef.modify (resetMaskAt · i)
/-If an index is missing in the arguments of the inductive type, then it must be non-fixed.
Consider the following example:
```lean
inductive All {I : Type u} (P : I → Type v) : List I → Type (max u v) where
| cons : P x → All P xs → All P (x :: xs)
inductive Iμ {I : Type u} : I → Type (max u v) where
| mk : (i : I) → All Iμ [] → Iμ i
```
because `i` doesn't appear in `All Iμ []`, the index shouldn't be fixed.
-/
for i in [eArgs.size:arity] do
maskRef.modify (resetMaskAt · i)
go ctors
go indType.ctors

View File

@@ -102,10 +102,8 @@ def ContextInfo.runCoreM (info : ContextInfo) (x : CoreM α) : IO α := do
have been used in `lctx` and `info.mctx`.
-/
(·.1) <$>
(withOptions (fun _ => info.options) x).toIO
{ currNamespace := info.currNamespace, openDecls := info.openDecls
fileName := "<InfoTree>", fileMap := default }
{ env := info.env, ngen := info.ngen }
x.toIO { options := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls, fileName := "<InfoTree>", fileMap := default }
{ env := info.env, ngen := info.ngen }
def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do
(·.1) <$> info.runCoreM (x.run { lctx := lctx } { mctx := info.mctx })

View File

@@ -228,23 +228,20 @@ private def shouldUseSimpMatch (e : Expr) : MetaM Bool := do
throwThe Unit ()
return ( (find e).run) matches .error _
partial def mkEqnTypes (tryRefl : Bool) (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
let (_, eqnTypes) go mvarId |>.run { declNames } |>.run #[]
return eqnTypes
where
go (mvarId : MVarId) : ReaderT Context (StateRefT (Array Expr) MetaM) Unit := do
trace[Elab.definition.eqns] "mkEqnTypes step\n{MessageData.ofGoal mvarId}"
if tryRefl then
if ( tryURefl mvarId) then
saveEqn mvarId
return ()
if ( tryURefl mvarId) then
saveEqn mvarId
return ()
if let some mvarId expandRHS? mvarId then
return ( go mvarId)
-- The following `funext?` was producing an overapplied `lhs`. Possible refinement: only do it
-- if we want to apply `splitMatch` on the body of the lambda
/- if let some mvarId ← funext? mvarId then
-- The following `funext?` was producing an overapplied `lhs`. Possible refinement: only do it if we want to apply `splitMatch` on the body of the lambda
/- if let some mvarId ← funext? mvarId then
return (← go mvarId) -/
if ( shouldUseSimpMatch ( mvarId.getType')) then

View File

@@ -62,7 +62,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
let us := info.levelParams.map mkLevelParam
let target mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
let goal mkFreshExprSyntheticOpaqueMVar target
mkEqnTypes (tryRefl := true) #[info.declName] goal.mvarId!
mkEqnTypes #[info.declName] goal.mvarId!
let baseName := info.declName
let mut thmNames := #[]
for i in [: eqnTypes.size] do

View File

@@ -114,8 +114,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
let us := info.levelParams.map mkLevelParam
let target mkEq (mkAppN (Lean.mkConst declName us) xs) body
let goal mkFreshExprSyntheticOpaqueMVar target
withReducible do
mkEqnTypes (tryRefl := false) info.declNames goal.mvarId!
mkEqnTypes info.declNames goal.mvarId!
let mut thmNames := #[]
for i in [: eqnTypes.size] do
let type := eqnTypes[i]!

View File

@@ -821,9 +821,7 @@ partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do
| some r => reduce structNames r
| none => return e.updateProj! ( reduce structNames b)
| .app f .. =>
-- Recall that proposition fields are theorems. Thus, we must set transparency to .all
-- to ensure they are unfolded here
match ( withTransparency .all <| reduceProjOf? e structNames.contains) with
match ( reduceProjOf? e structNames.contains) with
| some r => reduce structNames r
| none =>
let f := f.getAppFn

View File

@@ -704,8 +704,8 @@ private def registerStructure (structName : Name) (infos : Array StructFieldInfo
subobject? :=
if info.kind == StructFieldKind.subobject then
match env.find? info.declName with
| some info =>
match info.type.getForallBody.getAppFn with
| some (ConstantInfo.defnInfo val) =>
match val.type.getForallBody.getAppFn with
| Expr.const parentName .. => some parentName
| _ => panic! "ill-formed structure"
| _ => panic! "ill-formed environment"

View File

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Meta.Diagnostics
import Lean.Meta.Tactic.Apply
import Lean.Meta.Tactic.Assumption
import Lean.Meta.Tactic.Contradiction
@@ -164,12 +163,8 @@ private def getOptRotation (stx : Syntax) : Nat :=
@[builtin_tactic Parser.Tactic.set_option] def elabSetOption : Tactic := fun stx => do
let options Elab.elabSetOption stx[1] stx[3]
withOptions (fun _ => options) do
try
evalTactic stx[5]
finally
if stx[1].getId == `diagnostics then
reportDiag
withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
evalTactic stx[5]
@[builtin_tactic Parser.Tactic.allGoals] def evalAllGoals : Tactic := fun stx => do
let mvarIds getGoals

View File

@@ -146,9 +146,7 @@ It tries to rewrite an expression using the elim and move lemmas.
On failure, it calls the splitting procedure heuristic.
-/
partial def upwardAndElim (up : SimpTheorems) (e : Expr) : SimpM Simp.Step := do
-- Remark: we set `wellBehavedDischarge := false` because `prove` may access arbitrary elements in the local context.
-- See comment at `Methods.wellBehavedDischarge`
let r withDischarger prove (wellBehavedDischarge := false) do
let r withDischarger prove do
Simp.rewrite? e up.post up.erased (tag := "squash") (rflOnly := false)
let r := r.getD { expr := e }
let r r.mkEqTrans ( splittingProcedure r.expr)

View File

@@ -666,6 +666,7 @@ open Lean Elab Tactic Parser.Tactic
def omegaTactic (cfg : OmegaConfig) : TacticM Unit := do
liftMetaFinishingTactic fun g => do
let g g.falseOrByContra
(useClassical := false) -- because all the hypotheses we can make use of are decidable
g.withContext do
let hyps := ( getLocalHyps).toList
trace[omega] "analyzing {hyps.length} hypotheses:\n{← hyps.mapM inferType}"

View File

@@ -15,6 +15,7 @@ import Lean.Elab.Tactic.Config
namespace Lean.Elab.Tactic
open Meta
open TSyntax.Compat
open Simp (UsedSimps)
declare_config_elab elabSimpConfigCore Meta.Simp.Config
declare_config_elab elabSimpConfigCtxCore Meta.Simp.ConfigCtx
@@ -326,7 +327,7 @@ If `stx` is the syntax of a `simp`, `simp_all` or `dsimp` tactic invocation, and
creates the syntax of an equivalent `simp only`, `simp_all only` or `dsimp only`
invocation.
-/
def mkSimpOnly (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Syntax := do
def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) : MetaM Syntax := do
let isSimpAll := stx.isOfKind ``Parser.Tactic.simpAll
let mut stx := stx
if stx[3].isNone then
@@ -378,7 +379,7 @@ def mkSimpOnly (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Syntax := do
let argsStx := if args.isEmpty then #[] else #[mkAtom "[", (mkAtom ",").mkSep args, mkAtom "]"]
return stx.setArg 4 (mkNullNode argsStx)
def traceSimpCall (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Unit := do
def traceSimpCall (stx : Syntax) (usedSimps : UsedSimps) : MetaM Unit := do
logInfoAt stx[0] m!"Try this: {← mkSimpOnly stx usedSimps}"
/--
@@ -395,7 +396,7 @@ For many tactics other than the simplifier,
one should use the `withLocation` tactic combinator
when working with a `location`.
-/
def simpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM Simp.Stats := do
def simpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM UsedSimps := do
match loc with
| Location.targets hyps simplifyTarget =>
withMainContext do
@@ -405,39 +406,33 @@ def simpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (discharge
withMainContext do
go ( ( getMainGoal).getNondepPropHyps) (simplifyTarget := true)
where
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.Stats := do
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM UsedSimps := do
let mvarId getMainGoal
let (result?, stats) simpGoal mvarId ctx (simprocs := simprocs) (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
let (result?, usedSimps) simpGoal mvarId ctx (simprocs := simprocs) (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
match result? with
| none => replaceMainGoal []
| some (_, mvarId) => replaceMainGoal [mvarId]
return stats
def withSimpDiagnostics (x : TacticM Simp.Diagnostics) : TacticM Unit := do
let stats x
Simp.reportDiag stats
return usedSimps
/-
"simp" (config)? (discharger)? (" only")? (" [" ((simpStar <|> simpErase <|> simpLemma),*,?) "]")?
(location)?
-/
@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do withSimpDiagnostics do
@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do
let { ctx, simprocs, dischargeWrapper } mkSimpContext stx (eraseLocal := false)
let stats dischargeWrapper.with fun discharge? =>
let usedSimps dischargeWrapper.with fun discharge? =>
simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
if tactic.simp.trace.get ( getOptions) then
traceSimpCall stx stats.usedTheorems
return stats.diag
traceSimpCall stx usedSimps
@[builtin_tactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => withMainContext do withSimpDiagnostics do
@[builtin_tactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => withMainContext do
let { ctx, simprocs, .. } mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
let (result?, stats) simpAll ( getMainGoal) ctx (simprocs := simprocs)
let (result?, usedSimps) simpAll ( getMainGoal) ctx (simprocs := simprocs)
match result? with
| none => replaceMainGoal []
| some mvarId => replaceMainGoal [mvarId]
if tactic.simp.trace.get ( getOptions) then
traceSimpCall stx stats.usedTheorems
return stats.diag
traceSimpCall stx usedSimps
def dsimpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (loc : Location) : TacticM Unit := do
match loc with
@@ -449,15 +444,14 @@ def dsimpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (loc : Lo
withMainContext do
go ( ( getMainGoal).getNondepPropHyps) (simplifyTarget := true)
where
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Unit := withSimpDiagnostics do
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Unit := do
let mvarId getMainGoal
let (result?, stats) dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
let (result?, usedSimps) dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
match result? with
| none => replaceMainGoal []
| some mvarId => replaceMainGoal [mvarId]
if tactic.simp.trace.get ( getOptions) then
mvarId.withContext <| traceSimpCall ( getRef) stats.usedTheorems
return stats.diag
mvarId.withContext <| traceSimpCall ( getRef) usedSimps
@[builtin_tactic Lean.Parser.Tactic.dsimp] def evalDSimp : Tactic := fun stx => do
let { ctx, simprocs, .. } withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)

View File

@@ -25,41 +25,39 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
@[builtin_tactic simpTrace] def evalSimpTrace : Tactic := fun stx =>
match stx with
| `(tactic|
simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do withSimpDiagnostics do
simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do
let stx if bang.isSome then
`(tactic| simp!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
else
`(tactic| simp%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
let { ctx, simprocs, dischargeWrapper } mkSimpContext stx (eraseLocal := false)
let stats dischargeWrapper.with fun discharge? =>
let usedSimps dischargeWrapper.with fun discharge? =>
simpLocation ctx (simprocs := simprocs) discharge? <|
(loc.map expandLocation).getD (.targets #[] true)
let stx mkSimpCallStx stx stats.usedTheorems
let stx mkSimpCallStx stx usedSimps
addSuggestion tk stx (origSpan? := getRef)
return stats.diag
| _ => throwUnsupportedSyntax
@[builtin_tactic simpAllTrace] def evalSimpAllTrace : Tactic := fun stx =>
match stx with
| `(tactic| simp_all?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?) => withSimpDiagnostics do
| `(tactic| simp_all?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?) => do
let stx if bang.isSome then
`(tactic| simp_all!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?)
else
`(tactic| simp_all%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?)
let { ctx, .. } mkSimpContext stx (eraseLocal := true)
(kind := .simpAll) (ignoreStarArg := true)
let (result?, stats) simpAll ( getMainGoal) ctx
let (result?, usedSimps) simpAll ( getMainGoal) ctx
match result? with
| none => replaceMainGoal []
| some mvarId => replaceMainGoal [mvarId]
let stx mkSimpCallStx stx stats.usedTheorems
let stx mkSimpCallStx stx usedSimps
addSuggestion tk stx (origSpan? := getRef)
return stats.diag
| _ => throwUnsupportedSyntax
/-- Implementation of `dsimp?`. -/
def dsimpLocation' (ctx : Simp.Context) (simprocs : SimprocsArray) (loc : Location) :
TacticM Simp.Stats := do
TacticM Simp.UsedSimps := do
match loc with
| Location.targets hyps simplifyTarget =>
withMainContext do
@@ -70,26 +68,25 @@ def dsimpLocation' (ctx : Simp.Context) (simprocs : SimprocsArray) (loc : Locati
go ( ( getMainGoal).getNondepPropHyps) (simplifyTarget := true)
where
/-- Implementation of `dsimp?`. -/
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.Stats := do
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.UsedSimps := do
let mvarId getMainGoal
let (result?, stats) dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget)
let (result?, usedSimps) dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget)
(fvarIdsToSimp := fvarIdsToSimp)
match result? with
| none => replaceMainGoal []
| some mvarId => replaceMainGoal [mvarId]
pure stats
pure usedSimps
@[builtin_tactic dsimpTrace] def evalDSimpTrace : Tactic := fun stx =>
match stx with
| `(tactic| dsimp?%$tk $[!%$bang]? $(config)? $[only%$o]? $[[$args,*]]? $(loc)?) => withSimpDiagnostics do
| `(tactic| dsimp?%$tk $[!%$bang]? $(config)? $[only%$o]? $[[$args,*]]? $(loc)?) => do
let stx if bang.isSome then
`(tactic| dsimp!%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
else
`(tactic| dsimp%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
let { ctx, simprocs, .. }
withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
let stats dsimpLocation' ctx simprocs <| (loc.map expandLocation).getD (.targets #[] true)
let stx mkSimpCallStx stx stats.usedTheorems
let usedSimps dsimpLocation' ctx simprocs <| (loc.map expandLocation).getD (.targets #[] true)
let stx mkSimpCallStx stx usedSimps
addSuggestion tk stx (origSpan? := getRef)
return stats.diag
| _ => throwUnsupportedSyntax

View File

@@ -31,7 +31,7 @@ deriving instance Repr for UseImplicitLambdaResult
@[builtin_tactic Lean.Parser.Tactic.simpa] def evalSimpa : Tactic := fun stx => do
match stx with
| `(tactic| simpa%$tk $[?%$squeeze]? $[!%$unfold]? $(cfg)? $(disch)? $[only%$only]?
$[[$args,*]]? $[using $usingArg]?) => Elab.Tactic.focus do withSimpDiagnostics do
$[[$args,*]]? $[using $usingArg]?) => Elab.Tactic.focus do
let stx `(tactic| simp $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]?)
let { ctx, simprocs, dischargeWrapper }
withMainContext <| mkSimpContext stx (eraseLocal := false)
@@ -39,13 +39,12 @@ deriving instance Repr for UseImplicitLambdaResult
-- TODO: have `simpa` fail if it doesn't use `simp`.
let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
dischargeWrapper.with fun discharge? => do
let (some (_, g), stats) simpGoal ( getMainGoal) ctx (simprocs := simprocs)
let (some (_, g), usedSimps) simpGoal ( getMainGoal) ctx (simprocs := simprocs)
(simplifyTarget := true) (discharge? := discharge?)
| if getLinterUnnecessarySimpa ( getOptions) then
logLint linter.unnecessarySimpa ( getRef) "try 'simp' instead of 'simpa'"
return {}
g.withContext do
let stats if let some stx := usingArg then
let usedSimps if let some stx := usingArg then
setGoals [g]
g.withContext do
let e Tactic.elabTerm stx none (mayPostpone := true)
@@ -53,8 +52,8 @@ deriving instance Repr for UseImplicitLambdaResult
pure (h, g)
else
( g.assert `h ( inferType e) e).intro1
let (result?, stats) simpGoal g ctx (simprocs := simprocs) (fvarIdsToSimp := #[h])
(simplifyTarget := false) (stats := stats) (discharge? := discharge?)
let (result?, usedSimps) simpGoal g ctx (simprocs := simprocs) (fvarIdsToSimp := #[h])
(simplifyTarget := false) (usedSimps := usedSimps) (discharge? := discharge?)
match result? with
| some (xs, g) =>
let h := match xs with | #[h] | #[] => h | _ => unreachable!
@@ -67,18 +66,18 @@ deriving instance Repr for UseImplicitLambdaResult
if ( getLCtx).getRoundtrippingUserName? h |>.isSome then
logLint linter.unnecessarySimpa ( getRef)
m!"try 'simp at {Expr.fvar h}' instead of 'simpa using {Expr.fvar h}'"
pure stats
pure usedSimps
else if let some ldecl := ( getLCtx).findFromUserName? `this then
if let (some (_, g), stats) simpGoal g ctx (simprocs := simprocs)
(fvarIdsToSimp := #[ldecl.fvarId]) (simplifyTarget := false) (stats := stats)
if let (some (_, g), usedSimps) simpGoal g ctx (simprocs := simprocs)
(fvarIdsToSimp := #[ldecl.fvarId]) (simplifyTarget := false) (usedSimps := usedSimps)
(discharge? := discharge?) then
g.assumption; pure stats
g.assumption; pure usedSimps
else
pure stats
pure usedSimps
else
g.assumption; pure stats
g.assumption; pure usedSimps
if tactic.simp.trace.get ( getOptions) || squeeze.isSome then
let stx match mkSimpOnly stx stats.usedTheorems with
let stx match mkSimpOnly stx usedSimps with
| `(tactic| simp $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]?) =>
if unfold.isSome then
`(tactic| simpa! $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
@@ -86,7 +85,6 @@ deriving instance Repr for UseImplicitLambdaResult
`(tactic| simpa $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
| _ => unreachable!
TryThis.addSuggestion tk stx (origSpan? := getRef)
return stats.diag
| _ => throwUnsupportedSyntax
end Lean.Elab.Tactic.Simpa

View File

@@ -901,55 +901,6 @@ builtin_initialize namespacesExt : SimplePersistentEnvExtension Name NameSSet
addEntryFn := fun s n => s.insert n
}
structure Kernel.Diagnostics where
/-- Number of times each declaration has been unfolded by the kernel. -/
unfoldCounter : PHashMap Name Nat := {}
/-- If `enabled = true`, kernel records declarations that have been unfolded. -/
enabled : Bool := false
deriving Inhabited
/--
Extension for storting diagnostic information.
Remark: We store kernel diagnostic information in an environment extension to simplify
the interface with the kernel implemented in C/C++. Thus, we can only track
declarations in methods, such as `addDecl`, which return a new environment.
`Kernel.isDefEq` and `Kernel.whnf` do not update the statistics. We claim
this is ok since these methods are mainly used for debugging.
-/
builtin_initialize diagExt : EnvExtension Kernel.Diagnostics
registerEnvExtension (pure {})
@[export lean_kernel_diag_is_enabled]
def Kernel.Diagnostics.isEnabled (d : Diagnostics) : Bool :=
d.enabled
/-- Enables/disables kernel diagnostics. -/
def Kernel.enableDiag (env : Environment) (flag : Bool) : Environment :=
diagExt.modifyState env fun s => { s with enabled := flag }
def Kernel.isDiagnosticsEnabled (env : Environment) : Bool :=
diagExt.getState env |>.enabled
def Kernel.resetDiag (env : Environment) : Environment :=
diagExt.modifyState env fun s => { s with unfoldCounter := {} }
@[export lean_kernel_record_unfold]
def Kernel.Diagnostics.recordUnfold (d : Diagnostics) (declName : Name) : Diagnostics :=
if d.enabled then
let cNew := if let some c := d.unfoldCounter.find? declName then c + 1 else 1
{ d with unfoldCounter := d.unfoldCounter.insert declName cNew }
else
d
@[export lean_kernel_get_diag]
def Kernel.getDiagnostics (env : Environment) : Diagnostics :=
diagExt.getState env
@[export lean_kernel_set_diag]
def Kernel.setDiagnostics (env : Environment) (diag : Diagnostics) : Environment :=
diagExt.setState env diag
namespace Environment
/-- Register a new namespace in the environment. -/

View File

@@ -49,4 +49,3 @@ import Lean.Meta.LazyDiscrTree
import Lean.Meta.LitValues
import Lean.Meta.CheckTactic
import Lean.Meta.Canonicalizer
import Lean.Meta.Diagnostics

View File

@@ -212,17 +212,7 @@ instance : Hashable InfoCacheKey :=
fun transparency, expr, nargs => mixHash (hash transparency) <| mixHash (hash expr) (hash nargs)
end InfoCacheKey
structure SynthInstanceCacheKey where
localInsts : LocalInstances
type : Expr
/--
Value of `synthPendingDepth` when instance was synthesized or failed to be synthesized.
See issue #2522.
-/
synthPendingDepth : Nat
deriving Hashable, BEq
abbrev SynthInstanceCache := PersistentHashMap SynthInstanceCacheKey (Option Expr)
abbrev SynthInstanceCache := PersistentHashMap (LocalInstances × Expr) (Option Expr)
abbrev InferTypeCache := PersistentExprStructMap Expr
abbrev FunInfoCache := PersistentHashMap InfoCacheKey FunInfo
@@ -276,15 +266,6 @@ structure PostponedEntry where
ctx? : Option DefEqContext
deriving Inhabited
structure Diagnostics where
/-- Number of times each declaration has been unfolded -/
unfoldCounter : PHashMap Name Nat := {}
/-- Number of times `f a =?= f b` heuristic has been used per function `f`. -/
heuristicCounter : PHashMap Name Nat := {}
/-- Number of times a TC instance is used. -/
instanceCounter : PHashMap Name Nat := {}
deriving Inhabited
/--
`MetaM` monad state.
-/
@@ -295,7 +276,6 @@ structure State where
zetaDeltaFVarIds : FVarIdSet := {}
/-- Array of postponed universe level constraints -/
postponed : PersistentArray PostponedEntry := {}
diag : Diagnostics := {}
deriving Inhabited
/--
@@ -333,12 +313,6 @@ structure Context where
progress processing universe constraints.
-/
univApprox : Bool := false
/--
`inTypeClassResolution := true` when `isDefEq` is invoked at `tryResolve` in the type class
resolution module. We don't use `isDefEqProjDelta` when performing TC resolution due to performance issues.
This is not a great solution, but a proper solution would require a more sophisticased caching mechanism.
-/
inTypeClassResolution : Bool := false
/--
The `MetaM` monad is a core component of Lean's metaprogramming framework, facilitating the
@@ -460,7 +434,7 @@ section Methods
variable [MonadControlT MetaM n] [Monad n]
@[inline] def modifyCache (f : Cache Cache) : MetaM Unit :=
modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache := f cache, zetaDeltaFVarIds, postponed, diag }
modify fun { mctx, cache, zetaDeltaFVarIds, postponed } => { mctx, cache := f cache, zetaDeltaFVarIds, postponed }
@[inline] def modifyInferTypeCache (f : InferTypeCache InferTypeCache) : MetaM Unit :=
modifyCache fun ic, c1, c2, c3, c4, c5, c6 => f ic, c1, c2, c3, c4, c5, c6
@@ -474,28 +448,6 @@ variable [MonadControlT MetaM n] [Monad n]
@[inline] def resetDefEqPermCaches : MetaM Unit :=
modifyDefEqPermCache fun _ => {}
@[inline] def modifyDiag (f : Diagnostics Diagnostics) : MetaM Unit := do
if ( isDiagnosticsEnabled) then
modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache, zetaDeltaFVarIds, postponed, diag := f diag }
/-- If diagnostics are enabled, record that `declName` has been unfolded. -/
def recordUnfold (declName : Name) : MetaM Unit := do
modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter } =>
let newC := if let some c := unfoldCounter.find? declName then c + 1 else 1
{ unfoldCounter := unfoldCounter.insert declName newC, heuristicCounter, instanceCounter }
/-- If diagnostics are enabled, record that heuristic for solving `f a =?= f b` has been used. -/
def recordDefEqHeuristic (declName : Name) : MetaM Unit := do
modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter } =>
let newC := if let some c := heuristicCounter.find? declName then c + 1 else 1
{ unfoldCounter, heuristicCounter := heuristicCounter.insert declName newC, instanceCounter }
/-- If diagnostics are enabled, record that instance `declName` was used during TC resolution. -/
def recordInstance (declName : Name) : MetaM Unit := do
modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter } =>
let newC := if let some c := instanceCounter.find? declName then c + 1 else 1
{ unfoldCounter, heuristicCounter, instanceCounter := instanceCounter.insert declName newC }
def getLocalInstances : MetaM LocalInstances :=
return ( read).localInstances

View File

@@ -1,90 +0,0 @@
/-
Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.PrettyPrinter
import Lean.Meta.Basic
import Lean.Meta.Instances
namespace Lean.Meta
def collectAboveThreshold [BEq α] [Hashable α] (counters : PHashMap α Nat) (threshold : Nat) (p : α Bool) (lt : α α Bool) : Array (α × Nat) := Id.run do
let mut r := #[]
for (declName, counter) in counters do
if counter > threshold then
if p declName then
r := r.push (declName, counter)
return r.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then lt d₁ d₂ else c₁ > c₂
def subCounters [BEq α] [Hashable α] (newCounters oldCounters : PHashMap α Nat) : PHashMap α Nat := Id.run do
let mut result := {}
for (a, counterNew) in newCounters do
if let some counterOld := oldCounters.find? a then
result := result.insert a (counterNew - counterOld)
else
result := result.insert a counterNew
return result
structure DiagSummary where
data : Array MessageData := #[]
max : Nat := 0
deriving Inhabited
def DiagSummary.isEmpty (s : DiagSummary) : Bool :=
s.data.isEmpty
def mkDiagSummary (counters : PHashMap Name Nat) (p : Name Bool := fun _ => true) : MetaM DiagSummary := do
let threshold := diagnostics.threshold.get ( getOptions)
let entries := collectAboveThreshold counters threshold p Name.lt
if entries.isEmpty then
return {}
else
let mut data := #[]
for (declName, counter) in entries do
data := data.push m!"{if data.isEmpty then " " else "\n"}{MessageData.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}"
return { data, max := entries[0]!.2 }
def mkDiagSummaryForUnfolded (counters : PHashMap Name Nat) (instances := false) : MetaM DiagSummary := do
let env getEnv
mkDiagSummary counters fun declName =>
getReducibilityStatusCore env declName matches .semireducible
&& isInstanceCore env declName == instances
def mkDiagSummaryForUnfoldedReducible (counters : PHashMap Name Nat) : MetaM DiagSummary := do
let env getEnv
mkDiagSummary counters fun declName =>
getReducibilityStatusCore env declName matches .reducible
def mkDiagSummaryForUsedInstances : MetaM DiagSummary := do
mkDiagSummary ( get).diag.instanceCounter
def appendSection (m : MessageData) (cls : Name) (header : String) (s : DiagSummary) : MessageData :=
if s.isEmpty then
m
else
let header := s!"{header} (max: {s.max}, num: {s.data.size}):"
m ++ .trace { cls } header s.data
def reportDiag : MetaM Unit := do
if ( isDiagnosticsEnabled) then
let unfoldCounter := ( get).diag.unfoldCounter
let unfoldDefault mkDiagSummaryForUnfolded unfoldCounter
let unfoldInstance mkDiagSummaryForUnfolded unfoldCounter (instances := true)
let unfoldReducible mkDiagSummaryForUnfoldedReducible unfoldCounter
let heu mkDiagSummary ( get).diag.heuristicCounter
let inst mkDiagSummaryForUsedInstances
let unfoldKernel mkDiagSummary (Kernel.getDiagnostics ( getEnv)).unfoldCounter
unless unfoldDefault.isEmpty && unfoldInstance.isEmpty && unfoldReducible.isEmpty && heu.isEmpty && inst.isEmpty do
let m := MessageData.nil
let m := appendSection m `reduction "unfolded declarations" unfoldDefault
let m := appendSection m `reduction "unfolded instances" unfoldInstance
let m := appendSection m `reduction "unfolded reducible declarations" unfoldReducible
let m := appendSection m `type_class "used instances" inst
let m := appendSection m `def_eq "heuristic for solving `f a =?= f b`" heu
let m := appendSection m `kernel "unfolded declarations" unfoldKernel
let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
logInfo m
end Lean.Meta

View File

@@ -10,18 +10,6 @@ import Lean.Util.OccursCheck
namespace Lean.Meta
register_builtin_option backward.isDefEq.lazyProjDelta : Bool := {
defValue := true
group := "backward compatibility"
descr := "use lazy delta reduction when solving unification constrains of the form `(f a).i =?= (g b).i`"
}
register_builtin_option backward.isDefEq.lazyWhnfCore : Bool := {
defValue := true
group := "backward compatibility"
descr := "specifies transparency mode when normalizing constraints of the form `(f a).i =?= s`, if `true` only reducible definitions and instances are unfolded when reducing `f a`. Otherwise, the default setting is used"
}
/--
Return `true` if `e` is of the form `fun (x_1 ... x_n) => ?m y_1 ... y_k)`, and `?m` is unassigned.
Remark: `n`, `k` may be 0.
@@ -120,9 +108,9 @@ private def isDefEqEta (a b : Expr) : MetaM LBool := do
let bType inferType b
let bType whnfD bType
match bType with
| .forallE n d _ c =>
| Expr.forallE n d _ c =>
let b' := mkLambda n c d (mkApp b (mkBVar 0))
toLBoolM <| Meta.isExprDefEqAux a b'
toLBoolM <| checkpointDefEq <| Meta.isExprDefEqAux a b'
| _ => return .undef
else
return .undef
@@ -346,12 +334,10 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
k
loop 0
/--
Auxiliary function for `isDefEqBinding` for handling binders `forall/fun`.
It accumulates the new free variables in `fvars`, and declare them at `lctx`.
We use the domain types of `e` to create the new free variables.
We store the domain types of `e₂` at `ds₂`.
-/
/-- Auxiliary function for `isDefEqBinding` for handling binders `forall/fun`.
It accumulates the new free variables in `fvars`, and declare them at `lctx`.
We use the domain types of `e₁` to create the new free variables.
We store the domain types of `e` at `ds₂`. -/
private partial def isDefEqBindingAux (lctx : LocalContext) (fvars : Array Expr) (e₁ e₂ : Expr) (ds₂ : Array Expr) : MetaM Bool :=
let process (n : Name) (d₁ d₂ b₁ b₂ : Expr) : MetaM Bool := do
let d₁ := d₁.instantiateRev fvars
@@ -388,34 +374,34 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
pure false
/--
Auxiliary method for solving constraints of the form `?m xs := v`.
It creates a lambda using `mkLambdaFVars ys v`, where `ys` is a superset of `xs`.
`ys` is often equal to `xs`. It is a bigger when there are let-declaration dependencies in `xs`.
For example, suppose we have `xs` of the form `#[a, c]` where
```
a : Nat
b : Nat := f a
c : b = a
```
In this scenario, the type of `?m` is `(x1 : Nat) -> (x2 : f x1 = x1) -> C[x1, x2]`,
and type of `v` is `C[a, c]`. Note that, `?m a c` is type correct since `f a = a` is definitionally equal
to the type of `c : b = a`, and the type of `?m a c` is equal to the type of `v`.
Note that `fun xs => v` is the term `fun (x1 : Nat) (x2 : b = x1) => v` which has type
`(x1 : Nat) -> (x2 : b = x1) -> C[x1, x2]` which is not definitionally equal to the type of `?m`,
and may not even be type correct.
The issue here is that we are not capturing the `let`-declarations.
Auxiliary method for solving constraints of the form `?m xs := v`.
It creates a lambda using `mkLambdaFVars ys v`, where `ys` is a superset of `xs`.
`ys` is often equal to `xs`. It is a bigger when there are let-declaration dependencies in `xs`.
For example, suppose we have `xs` of the form `#[a, c]` where
```
a : Nat
b : Nat := f a
c : b = a
```
In this scenario, the type of `?m` is `(x1 : Nat) -> (x2 : f x1 = x1) -> C[x1, x2]`,
and type of `v` is `C[a, c]`. Note that, `?m a c` is type correct since `f a = a` is definitionally equal
to the type of `c : b = a`, and the type of `?m a c` is equal to the type of `v`.
Note that `fun xs => v` is the term `fun (x1 : Nat) (x2 : b = x1) => v` which has type
`(x1 : Nat) -> (x2 : b = x1) -> C[x1, x2]` which is not definitionally equal to the type of `?m`,
and may not even be type correct.
The issue here is that we are not capturing the `let`-declarations.
This method collects let-declarations `y` occurring between `xs[0]` and `xs.back` s.t.
some `x` in `xs` depends on `y`.
`ys` is the `xs` with these extra let-declarations included.
This method collects let-declarations `y` occurring between `xs[0]` and `xs.back` s.t.
some `x` in `xs` depends on `y`.
`ys` is the `xs` with these extra let-declarations included.
In the example above, `ys` is `#[a, b, c]`, and `mkLambdaFVars ys v` produces
`fun a => let b := f a; fun (c : b = a) => v` which has a type definitionally equal to the type of `?m`.
In the example above, `ys` is `#[a, b, c]`, and `mkLambdaFVars ys v` produces
`fun a => let b := f a; fun (c : b = a) => v` which has a type definitionally equal to the type of `?m`.
Recall that the method `checkAssignment` ensures `v` does not contain offending `let`-declarations.
Recall that the method `checkAssignment` ensures `v` does not contain offending `let`-declarations.
This method assumes that for any `xs[i]` and `xs[j]` where `i < j`, we have that `index of xs[i]` < `index of xs[j]`.
where the index is the position in the local context.
This method assumes that for any `xs[i]` and `xs[j]` where `i < j`, we have that `index of xs[i]` < `index of xs[j]`.
where the index is the position in the local context.
-/
private partial def mkLambdaFVarsWithLetDeps (xs : Array Expr) (v : Expr) : MetaM (Option Expr) := do
if not ( hasLetDeclsInBetween) then
@@ -449,13 +435,13 @@ where
let rec visit (e : Expr) : MonadCacheT Expr Unit (ReaderT Nat (StateRefT FVarIdHashSet MetaM)) Unit :=
checkCache e fun _ => do
match e with
| .forallE _ d b _ => visit d; visit b
| .lam _ d b _ => visit d; visit b
| .letE _ t v b _ => visit t; visit v; visit b
| .app f a => visit f; visit a
| .mdata _ b => visit b
| .proj _ _ b => visit b
| .fvar fvarId =>
| Expr.forallE _ d b _ => visit d; visit b
| Expr.lam _ d b _ => visit d; visit b
| Expr.letE _ t v b _ => visit t; visit v; visit b
| Expr.app f a => visit f; visit a
| Expr.mdata _ b => visit b
| Expr.proj _ _ b => visit b
| Expr.fvar fvarId =>
let localDecl fvarId.getDecl
if localDecl.isLet && localDecl.index > ( read) then
modify fun s => s.insert localDecl.fvarId
@@ -848,18 +834,18 @@ mutual
return e
else checkCache e fun _ =>
match e with
| .mdata _ b => return e.updateMData! ( check b)
| .proj _ _ s => return e.updateProj! ( check s)
| .lam _ d b _ => return e.updateLambdaE! ( check d) ( check b)
| .forallE _ d b _ => return e.updateForallE! ( check d) ( check b)
| .letE _ t v b _ => return e.updateLet! ( check t) ( check v) ( check b)
| .bvar .. => return e
| .sort .. => return e
| .const .. => return e
| .lit .. => return e
| .fvar .. => checkFVar e
| .mvar .. => checkMVar e
| .app .. =>
| Expr.mdata _ b => return e.updateMData! ( check b)
| Expr.proj _ _ s => return e.updateProj! ( check s)
| Expr.lam _ d b _ => return e.updateLambdaE! ( check d) ( check b)
| Expr.forallE _ d b _ => return e.updateForallE! ( check d) ( check b)
| Expr.letE _ t v b _ => return e.updateLet! ( check t) ( check v) ( check b)
| Expr.bvar .. => return e
| Expr.sort .. => return e
| Expr.const .. => return e
| Expr.lit .. => return e
| Expr.fvar .. => checkFVar e
| Expr.mvar .. => checkMVar e
| Expr.app .. =>
try
checkApp e
catch ex => match ex with
@@ -904,24 +890,24 @@ partial def check
if !e.hasExprMVar && !e.hasFVar then
true
else match e with
| .mdata _ b => visit b
| .proj _ _ s => visit s
| .app f a => visit f && visit a
| .lam _ d b _ => visit d && visit b
| .forallE _ d b _ => visit d && visit b
| .letE _ t v b _ => visit t && visit v && visit b
| .bvar .. => true
| .sort .. => true
| .const .. => true
| .lit .. => true
| .fvar fvarId .. =>
| Expr.mdata _ b => visit b
| Expr.proj _ _ s => visit s
| Expr.app f a => visit f && visit a
| Expr.lam _ d b _ => visit d && visit b
| Expr.forallE _ d b _ => visit d && visit b
| Expr.letE _ t v b _ => visit t && visit v && visit b
| Expr.bvar .. => true
| Expr.sort .. => true
| Expr.const .. => true
| Expr.lit .. => true
| Expr.fvar fvarId .. =>
if mvarDecl.lctx.contains fvarId then true
else match lctx.find? fvarId with
| some (LocalDecl.ldecl ..) => false -- need expensive CheckAssignment.check
| _ =>
if fvars.any fun x => x.fvarId! == fvarId then true
else false -- We could throw an exception here, but we would have to use ExceptM. So, we let CheckAssignment.check do it
| .mvar mvarId' =>
| Expr.mvar mvarId' =>
match mctx.getExprAssignmentCore? mvarId' with
| some _ => false -- use CheckAssignment.check to instantiate
| none =>
@@ -1253,7 +1239,6 @@ private def tryHeuristic (t s : Expr) : MetaM Bool := do
unless t.hasExprMVar || s.hasExprMVar do
return false
withTraceNodeBefore `Meta.isDefEq.delta (return m!"{t} =?= {s}") do
recordDefEqHeuristic tFn.constName!
/-
We process arguments before universe levels to reduce a source of brittleness in the TC procedure.
@@ -1477,8 +1462,8 @@ private def expandDelayedAssigned? (t : Expr) : MetaM (Option Expr) := do
return some (mkAppRange (mkMVar mvarIdPending) fvars.size tArgs.size tArgs)
private def isAssignable : Expr MetaM Bool
| .mvar mvarId => do let b mvarId.isReadOnlyOrSyntheticOpaque; pure (!b)
| _ => pure false
| Expr.mvar mvarId => do let b mvarId.isReadOnlyOrSyntheticOpaque; pure (!b)
| _ => pure false
private def etaEq (t s : Expr) : Bool :=
match t.etaExpanded? with
@@ -1553,7 +1538,7 @@ private def isDefEqMVarSelf (mvar : Expr) (args₁ args₂ : Array Expr) : MetaM
Removes unnecessary let-decls (both true `let`s and `let_fun`s).
-/
private partial def consumeLet : Expr Expr
| e@(.letE _ _ _ b _) => if b.hasLooseBVars then e else consumeLet b
| e@(Expr.letE _ _ _ b _) => if b.hasLooseBVars then e else consumeLet b
| e =>
if let some (_, _, _, b) := e.letFun? then
if b.hasLooseBVars then e else consumeLet b
@@ -1723,10 +1708,11 @@ private partial def isDefEqQuickMVarMVar (t s : Expr) : MetaM LBool := do
end
@[inline] def whenUndefDo (x : MetaM LBool) (k : MetaM Bool) : MetaM Bool := do
match ( x) with
| .true => return true
| .false => return false
| .undef => k
let status x
match status with
| LBool.true => pure true
| LBool.false => pure false
| LBool.undef => k
@[specialize] private def unstuckMVar (e : Expr) (successK : Expr MetaM Bool) (failK : MetaM Bool): MetaM Bool := do
match ( getStuckMVar? e) with
@@ -1773,7 +1759,7 @@ private def isDefEqDeltaStep (t s : Expr) : MetaM DeltaStepResult := do
| .eq =>
-- Remark: if `t` and `s` are both some `f`-application, we use `tryHeuristic`
-- if `f` is not a projection. The projection case generates a performance regression.
if tInfo.name == sInfo.name then
if tInfo.name == sInfo.name && !( isProjectionFn tInfo.name) then
if t.isApp && s.isApp && ( tryHeuristic t s) then
return .eq
else
@@ -1817,13 +1803,8 @@ where
| _, _ => Meta.isExprDefEqAux t s
private def isDefEqProj : Expr Expr MetaM Bool
| .proj m i t, .proj n j s => do
if ( read).inTypeClassResolution then
-- See comment at `inTypeClassResolution`
pure (i == j && m == n) <&&> Meta.isExprDefEqAux t s
else if !backward.isDefEq.lazyProjDelta.get ( getOptions) then
pure (i == j && m == n) <&&> Meta.isExprDefEqAux t s
else if i == j && m == n then
| .proj m i t, .proj n j s =>
if i == j && m == n then
isDefEqProjDelta t s i
else
return false
@@ -1996,12 +1977,6 @@ private def cacheResult (keyInfo : DefEqCacheKeyInfo) (result : Bool) : MetaM Un
let key := ( instantiateMVars key.1, instantiateMVars key.2)
modifyDefEqTransientCache fun c => c.update mode key result
private def whnfCoreAtDefEq (e : Expr) : MetaM Expr := do
if backward.isDefEq.lazyWhnfCore.get ( getOptions) then
whnfCore e (config := { proj := .yesWithDeltaI })
else
whnfCore e
@[export lean_is_expr_def_eq]
partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecDepth do
withTraceNodeBefore `Meta.isDefEq (return m!"{t} =?= {s}") do
@@ -2014,7 +1989,7 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
we only want to unify negation (and not all other field operations as well).
Unifying the field instances slowed down unification: https://github.com/leanprover/lean4/issues/1986
Note that we use `proj := .yesWithDeltaI` to ensure `whnfAtMostI` is used to reduce the projection structure.
Note that ew use `proj := .yesWithDeltaI` to ensure `whnfAtMostI` is used to reduce the projection structure.
We added this refinement to address a performance issue in code such as
```
let val : Test := bar c1 key
@@ -2043,8 +2018,8 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
`whnfCore t (config := { proj := .yes })` which more conservative than `.yesWithDeltaI`,
and it only created performance issues when handling TC unification problems.
-/
let t' whnfCoreAtDefEq t
let s' whnfCoreAtDefEq s
let t' whnfCore t (config := { proj := .yesWithDeltaI })
let s' whnfCore s (config := { proj := .yesWithDeltaI })
if t != t' || s != s' then
isExprDefEqAuxImpl t' s'
else

View File

@@ -21,28 +21,27 @@ section ExprLens
open Lean.SubExpr
variable [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadError M]
variable {M} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadError M]
/-- Given a constructor index for Expr, runs `g` on the value of that subexpression and replaces it.
If the subexpression is under a binder it will instantiate and abstract the binder body correctly.
Mdata is ignored. An index of 3 is interpreted as the type of the expression. An index of 3 will throw since we can't replace types.
See also `Lean.Meta.transform`, `Lean.Meta.traverseChildren`. -/
private def lensCoord (g : Expr M Expr) (n : Nat) (e : Expr) : M Expr := do
match n, e with
| 0, .app f a => return e.updateApp! ( g f) a
| 1, .app f a => return e.updateApp! f ( g a)
| 0, .lam _ y b _ => return e.updateLambdaE! ( g y) b
| 1, .lam n y b c => withLocalDecl n c y fun x => do mkLambdaFVars #[x] <| g <| b.instantiateRev #[x]
| 0, .forallE _ y b _ => return e.updateForallE! ( g y) b
| 1, .forallE n y b c => withLocalDecl n c y fun x => do mkForallFVars #[x] <| g <| b.instantiateRev #[x]
| 0, .letE _ y a b _ => return e.updateLet! ( g y) a b
| 1, .letE _ y a b _ => return e.updateLet! y ( g a) b
| 2, .letE n y a b _ => withLetDecl n y a fun x => do mkLetFVars #[x] <| g <| b.instantiateRev #[x]
| 0, .proj _ _ b => e.updateProj! <$> g b
| n, .mdata _ a => e.updateMData! <$> lensCoord g n a
| 3, _ => throwError "Lensing on types is not supported"
| c, e => throwError "Invalid coordinate {c} for {e}"
private def lensCoord (g : Expr M Expr) : Nat Expr M Expr
| 0, e@(Expr.app f a) => return e.updateApp! ( g f) a
| 1, e@(Expr.app f a) => return e.updateApp! f ( g a)
| 0, e@(Expr.lam _ y b _) => return e.updateLambdaE! ( g y) b
| 1, (Expr.lam n y b c) => withLocalDecl n c y fun x => do mkLambdaFVars #[x] <| g <| b.instantiateRev #[x]
| 0, e@(Expr.forallE _ y b _) => return e.updateForallE! ( g y) b
| 1, (Expr.forallE n y b c) => withLocalDecl n c y fun x => do mkForallFVars #[x] <| g <| b.instantiateRev #[x]
| 0, e@(Expr.letE _ y a b _) => return e.updateLet! ( g y) a b
| 1, e@(Expr.letE _ y a b _) => return e.updateLet! y ( g a) b
| 2, (Expr.letE n y a b _) => withLetDecl n y a fun x => do mkLetFVars #[x] <| g <| b.instantiateRev #[x]
| 0, e@(Expr.proj _ _ b) => e.updateProj! <$> g b
| n, e@(Expr.mdata _ a) => e.updateMData! <$> lensCoord g n a
| 3, _ => throwError "Lensing on types is not supported"
| c, e => throwError "Invalid coordinate {c} for {e}"
private def lensAux (g : Expr M Expr) : List Nat Expr M Expr
| [], e => g e
@@ -57,21 +56,20 @@ def replaceSubexpr (replace : (subexpr : Expr) → M Expr) (p : Pos) (root : Exp
/-- Runs `k` on the given coordinate, including handling binders properly.
The subexpression value passed to `k` is not instantiated with respect to the
array of free variables. -/
private def viewCoordAux (k : Array Expr Expr M α) (fvars: Array Expr) (n : Nat) (e : Expr) : M α := do
match n, e with
| 3, _ => throwError "Internal: Types should be handled by viewAux"
| 0, .app f _ => k fvars f
| 1, .app _ a => k fvars a
| 0, .lam _ y _ _ => k fvars y
| 1, .lam n y b c => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
| 0, .forallE _ y _ _ => k fvars y
| 1, .forallE n y b c => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
| 0, .letE _ y _ _ _ => k fvars y
| 1, .letE _ _ a _ _ => k fvars a
| 2, .letE n y a b _ => withLetDecl n (y.instantiateRev fvars) (a.instantiateRev fvars) fun x => k (fvars.push x) b
| 0, .proj _ _ b => k fvars b
| n, .mdata _ a => viewCoordAux k fvars n a
| c, e => throwError "Invalid coordinate {c} for {e}"
private def viewCoordAux (k : Array Expr Expr M α) (fvars: Array Expr) : Nat Expr M α
| 3, _ => throwError "Internal: Types should be handled by viewAux"
| 0, (Expr.app f _) => k fvars f
| 1, (Expr.app _ a) => k fvars a
| 0, (Expr.lam _ y _ _) => k fvars y
| 1, (Expr.lam n y b c) => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
| 0, (Expr.forallE _ y _ _) => k fvars y
| 1, (Expr.forallE n y b c) => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
| 0, (Expr.letE _ y _ _ _) => k fvars y
| 1, (Expr.letE _ _ a _ _) => k fvars a
| 2, (Expr.letE n y a b _) => withLetDecl n (y.instantiateRev fvars) (a.instantiateRev fvars) fun x => k (fvars.push x) b
| 0, (Expr.proj _ _ b) => k fvars b
| n, (Expr.mdata _ a) => viewCoordAux k fvars n a
| c, e => throwError "Invalid coordinate {c} for {e}"
private def viewAux (k : Array Expr Expr M α) (fvars : Array Expr) : List Nat Expr M α
| [], e => k fvars <| e.instantiateRev fvars
@@ -121,24 +119,24 @@ open Lean.SubExpr
section ViewRaw
variable [Monad M] [MonadError M]
variable {M} [Monad M] [MonadError M]
/-- Get the raw subexpression without performing any instantiation. -/
private def viewCoordRaw (e : Expr) (n : Nat) : M Expr := do
match e, n with
| e, 3 => throwError "Can't viewRaw the type of {e}"
| .app f _, 0 => pure f
| .app _ a, 1 => pure a
| .lam _ y _ _, 0 => pure y
| .lam _ _ b _, 1 => pure b
| .forallE _ y _ _, 0 => pure y
| .forallE _ _ b _, 1 => pure b
| .letE _ y _ _ _, 0 => pure y
| .letE _ _ a _ _, 1 => pure a
| .letE _ _ _ b _, 2 => pure b
| .proj _ _ b, 0 => pure b
| .mdata _ a, n => viewCoordRaw a n
| e, c => throwError "Bad coordinate {c} for {e}"
private def viewCoordRaw: Expr Nat M Expr
| e , 3 => throwError "Can't viewRaw the type of {e}"
| (Expr.app f _) , 0 => pure f
| (Expr.app _ a) , 1 => pure a
| (Expr.lam _ y _ _) , 0 => pure y
| (Expr.lam _ _ b _) , 1 => pure b
| (Expr.forallE _ y _ _), 0 => pure y
| (Expr.forallE _ _ b _), 1 => pure b
| (Expr.letE _ y _ _ _) , 0 => pure y
| (Expr.letE _ _ a _ _) , 1 => pure a
| (Expr.letE _ _ _ b _) , 2 => pure b
| (Expr.proj _ _ b) , 0 => pure b
| (Expr.mdata _ a) , n => viewCoordRaw a n
| e , c => throwError "Bad coordinate {c} for {e}"
/-- Given a valid `SubExpr`, return the raw current expression without performing any instantiation.
If the given `SubExpr` has a type subexpression coordinate, then throw an error.
@@ -150,20 +148,21 @@ def viewSubexpr (p : Pos) (root : Expr) : M Expr :=
p.foldlM viewCoordRaw root
private def viewBindersCoord : Nat Expr Option (Name × Expr)
| 1, .lam n y _ _ => some (n, y)
| 1, .forallE n y _ _ => some (n, y)
| 2, .letE n y _ _ _ => some (n, y)
| _, _ => none
| 1, (Expr.lam n y _ _) => some (n, y)
| 1, (Expr.forallE n y _ _) => some (n, y)
| 2, (Expr.letE n y _ _ _) => some (n, y)
| _, _ => none
/-- `viewBinders p e` returns a list of all of the binders (name, type) above the given position `p` in the root expression `e` -/
def viewBinders (p : Pos) (root : Expr) : M (Array (Name × Expr)) := do
let (acc, _) p.foldlM (init := (#[], root)) fun (acc, e) c => do
let (acc, _) p.foldlM (fun (acc, e) c => do
let e₂ viewCoordRaw e c
let acc :=
match viewBindersCoord c e with
| none => acc
| some b => acc.push b
return (acc, e₂)
) (#[], root)
return acc
/-- Returns the number of binders above a given subexpr position. -/

View File

@@ -31,35 +31,6 @@ def elimOptParam (type : Expr) : CoreM Expr := do
else
return .continue
/-- Returns true if `e` occurs either in `t`, or in the type of a sub-expression of `t`.
Consider the following example:
```lean
inductive Tyₛ : Type (u+1)
| SPi : (T : Type u) -> (T -> Tyₛ) -> Tyₛ
inductive Tmₛ.{u} : Tyₛ.{u} -> Type (u+1)
| app : Tmₛ (.SPi T A) -> (arg : T) -> Tmₛ (A arg)```
```
When looking for fixed arguments in `Tmₛ.app`, if we only consider occurences in the term `Tmₛ (A arg)`,
`T` is considered non-fixed despite the fact that `A : T -> Tyₛ`.
This leads to an ill-typed injectivity theorem signature:
```lean
theorem Tmₛ.app.inj {T : Type u} {A : T → Tyₛ} {a : Tmₛ (Tyₛ.SPi T A)} {arg : T} {T_1 : Type u} {a_1 : Tmₛ (Tyₛ.SPi T_1 A)} :
Tmₛ.app a arg = Tmₛ.app a_1 arg →
T = T_1 ∧ HEq a a_1 := fun x => Tmₛ.noConfusion x fun T_eq A_eq a_eq arg_eq => eq_of_heq a_eq
```
Instead of checking the type of every subterm, we only need to check the type of free variables, since free variables introduced in
the constructor may only appear in the type of other free variables introduced after them.
-/
def occursOrInType (e : Expr) (t : Expr) : MetaM Bool := do
let_fun f (s : Expr) := do
if !s.isFVar then
return s == e
let ty inferType s
return s == e || e.occurs ty
return ( t.findM? f).isSome
private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useEq : Bool) : MetaM (Option Expr) := do
let us := ctorVal.levelParams.map mkLevelParam
let type elimOptParam ctorVal.type
@@ -87,7 +58,7 @@ private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useE
match ( whnf type) with
| Expr.forallE n d b _ =>
let arg1 := args1.get i, h
if occursOrInType arg1 resultType then
if arg1.occurs resultType then
mkArgs2 (i + 1) (b.instantiate1 arg1) (args2.push arg1) args2New
else
withLocalDecl n (if useEq then BinderInfo.default else BinderInfo.implicit) d fun arg2 =>

View File

@@ -217,11 +217,8 @@ def getGlobalInstancesIndex : CoreM (DiscrTree InstanceEntry) :=
def getErasedInstances : CoreM (PHashSet Name) :=
return Meta.instanceExtension.getState ( getEnv) |>.erased
def isInstanceCore (env : Environment) (declName : Name) : Bool :=
Meta.instanceExtension.getState env |>.instanceNames.contains declName
def isInstance (declName : Name) : CoreM Bool :=
return isInstanceCore ( getEnv) declName
return Meta.instanceExtension.getState ( getEnv) |>.instanceNames.contains declName
def getInstancePriority? (declName : Name) : CoreM (Option Nat) := do
let some entry := Meta.instanceExtension.getState ( getEnv) |>.instanceNames.find? declName | return none

View File

@@ -745,6 +745,7 @@ instance : Append (PreDiscrTree α) where
end PreDiscrTree
/-- Initial entry in lazy discrimination tree -/
@[reducible]
structure InitEntry (α : Type) where
/-- Return root key for an entry. -/
key : Key
@@ -977,13 +978,12 @@ def createImportedDiscrTree [Monad m] [MonadLog m] [AddMessageContext m] [MonadO
/-- Creates the core context used for initializing a tree using the current context. -/
private def createTreeCtx (ctx : Core.Context) : Core.Context := {
fileName := ctx.fileName
fileMap := ctx.fileMap
options := ctx.options
maxRecDepth := ctx.maxRecDepth
maxHeartbeats := 0
ref := ctx.ref
diag := getDiag ctx.options
fileName := ctx.fileName,
fileMap := ctx.fileMap,
options := ctx.options,
maxRecDepth := ctx.maxRecDepth,
maxHeartbeats := 0,
ref := ctx.ref,
}
def findImportMatches

View File

@@ -25,12 +25,6 @@ register_builtin_option synthInstance.maxSize : Nat := {
descr := "maximum number of instances used to construct a solution in the type class instance synthesis procedure"
}
register_builtin_option backward.synthInstance.canonInstances : Bool := {
defValue := true
group := "backward compatibility"
descr := "use optimization that relies on 'morally canonical' instances during type class resolution"
}
namespace SynthInstance
def getMaxHeartbeats (opts : Options) : Nat :=
@@ -362,9 +356,6 @@ private def mkLambdaFVars' (xs : Array Expr) (e : Expr) : MetaM Expr :=
If it succeeds, the result is a new updated metavariable context and a new list of subgoals.
A subgoal is created for each instance implicit parameter of `inst`. -/
def tryResolve (mvar : Expr) (inst : Instance) : MetaM (Option (MetavarContext × List Expr)) := do
if ( isDiagnosticsEnabled) then
if let .const declName _ := inst.val.getAppFn then
recordInstance declName
let mvarType inferType mvar
let lctx getLCtx
let localInsts getLocalInstances
@@ -425,7 +416,7 @@ private def mkAnswer (cNode : ConsumerNode) : MetaM Answer :=
def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
withMCtx cNode.mctx do
if cNode.size ( read).maxResultSize then
trace[Meta.synthInstance.answer] "{crossEmoji} {← instantiateMVars (← inferType cNode.mvar)}{Format.line}(size: {cNode.size} ≥ {(← read).maxResultSize})"
trace[Meta.synthInstance.answer] "{crossEmoji} {← instantiateMVars (← inferType cNode.mvar)}{Format.line}(size: {cNode.size} ≥ {(← read).maxResultSize})"
else
withTraceNode `Meta.synthInstance.answer
(fun _ => return m!"{checkEmoji} {← instantiateMVars (← inferType cNode.mvar)}") do
@@ -558,17 +549,16 @@ def generate : SynthM Unit := do
let mctx := gNode.mctx
let mvar := gNode.mvar
/- See comment at `typeHasMVars` -/
if backward.synthInstance.canonInstances.get ( getOptions) then
unless gNode.typeHasMVars do
if let some entry := ( get).tableEntries.find? key then
unless entry.answers.isEmpty do
/-
We already have an answer for this node, and since its type does not have metavariables,
we can skip other solutions because we assume instances are "morally canonical".
We have added this optimization to address issue #3996.
-/
modify fun s => { s with generatorStack := s.generatorStack.pop }
return
unless gNode.typeHasMVars do
if let some entry := ( get).tableEntries.find? key then
unless entry.answers.isEmpty do
/-
We already have an answer for this node, and since its type does not have metavariables,
we can skip other solutions because we assume instances are "morally canonical".
We have added this optimization to address issue #3996.
-/
modify fun s => { s with generatorStack := s.generatorStack.pop }
return
discard do withMCtx mctx do
withTraceNode `Meta.synthInstance
(return m!"{exceptOptionEmoji ·} apply {inst.val} to {← instantiateMVars (← inferType mvar)}") do
@@ -721,7 +711,6 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
(return m!"{exceptOptionEmoji ·} {← instantiateMVars type}") do
withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.instances,
foApprox := true, ctxApprox := true, constApprox := false, univApprox := false }) do
withReader (fun ctx => { ctx with inTypeClassResolution := true }) do
let localInsts getLocalInstances
let type instantiateMVars type
let type preprocess type
@@ -735,8 +724,7 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
unless defEq do
trace[Meta.synthInstance] "{crossEmoji} result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
return defEq
let cacheKey := { localInsts, type, synthPendingDepth := ( read).synthPendingDepth }
match s.cache.synthInstance.find? cacheKey with
match s.cache.synthInstance.find? (localInsts, type) with
| some result =>
trace[Meta.synthInstance] "result {result} (cached)"
if let some inst := result then
@@ -783,7 +771,7 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
pure (some result)
else
pure none
modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey result? }
modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert (localInsts, type) result? }
pure result?
/--

View File

@@ -160,7 +160,7 @@ An exception ID that indicates further speculation on candidate lemmas should st
and current results should be returned.
-/
private builtin_initialize abortSpeculationId : InternalExceptionId
registerInternalExceptionId `Lean.Meta.LibrarySearch.abortSpeculation
registerInternalExceptionId `Std.Tactic.LibrarySearch.abortSpeculation
/--
Called to abort speculative execution in library search.

View File

@@ -81,7 +81,6 @@ def Poly.add (e₁ e₂ : Poly) : Poly :=
else
{ val := r }
termination_by (e₁.size - i₁, e₂.size - i₂)
decreasing_by all_goals decreasing_with decreasing_trivial_pre_omega
go 0 0 #[]
def Poly.combine (d₁ : Int) (e₁ : Poly) (d₂ : Int) (e₂ : Poly) : Poly :=
@@ -109,7 +108,6 @@ def Poly.combine (d₁ : Int) (e₁ : Poly) (d₂ : Int) (e₂ : Poly) : Poly :=
else
{ val := r }
termination_by (e₁.size - i₁, e₂.size - i₂)
decreasing_by all_goals decreasing_with decreasing_trivial_pre_omega
go 0 0 #[]
def Poly.eval? (e : Poly) (a : Assignment) : Option Rat := Id.run do

View File

@@ -14,7 +14,6 @@ import Lean.Meta.Tactic.Simp.Simproc
import Lean.Meta.Tactic.Simp.BuiltinSimprocs
import Lean.Meta.Tactic.Simp.RegisterCommand
import Lean.Meta.Tactic.Simp.Attr
import Lean.Meta.Tactic.Simp.Diagnostics
namespace Lean

View File

@@ -275,7 +275,7 @@ def reduceLTLE (nm : Name) (arity : Nat) (isLT : Bool) (e : Expr) : SimpM Step :
applySimprocConst (mkConst ``True) ``Nat.Simproc.le_add_le #[x, yb, yo, leProof]
else
let finExpr := mkLENat (toExpr (xn - yn)) yb
let geProof mkOfDecideEqTrue (mkGENat x yo)
let geProof mkOfDecideEqTrue (mkGENat yo x)
applySimprocConst finExpr ``Nat.Simproc.le_add_ge #[x, yb, yo, geProof]
| .offset xb xo xn, .offset yb yo yn => do
if xn yn then

View File

@@ -1,48 +0,0 @@
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Meta.Diagnostics
import Lean.Meta.Tactic.Simp.Types
namespace Lean.Meta.Simp
def mkSimpDiagSummary (counters : PHashMap Origin Nat) (usedCounters? : Option (PHashMap Origin Nat) := none) : MetaM DiagSummary := do
let threshold := diagnostics.threshold.get ( getOptions)
let entries := collectAboveThreshold counters threshold (fun _ => true) (lt := (· < ·))
if entries.isEmpty then
return {}
else
let mut data := #[]
for (thmId, counter) in entries do
let key match thmId with
| .decl declName _ _ =>
if ( getEnv).contains declName then
pure m!"{MessageData.ofConst (← mkConstWithLevelParams declName)}"
else
pure m!"{declName} (builtin simproc)"
| .fvar fvarId => pure m!"{mkFVar fvarId}"
| _ => pure thmId.key
let usedMsg if let some usedCounters := usedCounters? then
if let some c := usedCounters.find? thmId then pure s!", succeeded: {c}" else pure s!" {crossEmoji}" -- not used
else
pure ""
data := data.push m!"{if data.isEmpty then " " else "\n"}{key} ↦ {counter}{usedMsg}"
return { data, max := entries[0]!.2 }
def reportDiag (diag : Simp.Diagnostics) : MetaM Unit := do
if ( isDiagnosticsEnabled) then
let used mkSimpDiagSummary diag.usedThmCounter
let tried mkSimpDiagSummary diag.triedThmCounter diag.usedThmCounter
let congr mkDiagSummary diag.congrThmCounter
unless used.isEmpty && tried.isEmpty && congr.isEmpty do
let m := MessageData.nil
let m := appendSection m `simp "used theorems" used
let m := appendSection m `simp "tried theorems" tried
let m := appendSection m `simp "tried congruence theorems" congr
let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
logInfo m
end Lean.Meta.Simp

View File

@@ -8,7 +8,6 @@ import Lean.Meta.Transform
import Lean.Meta.Tactic.Replace
import Lean.Meta.Tactic.UnifyEq
import Lean.Meta.Tactic.Simp.Rewrite
import Lean.Meta.Tactic.Simp.Diagnostics
import Lean.Meta.Match.Value
namespace Lean.Meta
@@ -244,26 +243,28 @@ def getSimpLetCase (n : Name) (t : Expr) (b : Expr) : MetaM SimpLetCase := do
/--
We use `withNewlemmas` whenever updating the local context.
We use `withFreshCache` because the local context affects `simp` rewrites
even when `contextual := false`.
For example, the `discharger` may inspect the current local context. The default
discharger does that when applying equational theorems, and the user may
use `(discharger := assumption)` or `(discharger := omega)`.
If the `wishFreshCache` introduces performance issues, we can design a better solution
for the default discharger which is used most of the time.
-/
def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := do
def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := withFreshCache do
if ( getConfig).contextual then
withFreshCache do
let mut s getSimpTheorems
let mut updated := false
for x in xs do
if ( isProof x) then
s s.addTheorem (.fvar x.fvarId!) x
updated := true
if updated then
withTheReader Context (fun ctx => { ctx with simpTheorems := s }) f
else
f
else if ( getMethods).wellBehavedDischarge then
-- See comment at `Methods.wellBehavedDischarge` to understand why
-- we don't have to reset the cache
f
let mut s getSimpTheorems
let mut updated := false
for x in xs do
if ( isProof x) then
s s.addTheorem (.fvar x.fvarId!) x
updated := true
if updated then
withTheReader Context (fun ctx => { ctx with simpTheorems := s }) f
else
f
else
withFreshCache do f
f
def simpProj (e : Expr) : SimpM Result := do
match ( reduceProj? e) with
@@ -518,7 +519,6 @@ def processCongrHypothesis (h : Expr) : SimpM Bool := do
/-- Try to rewrite `e` children using the given congruence theorem -/
def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Result) := withNewMCtxDepth do
recordCongrTheorem c.theoremName
trace[Debug.Meta.Tactic.simp.congr] "{c.theoremName}, {e}"
let thm mkConstWithFreshMVarLevels c.theoremName
let (xs, bis, type) forallMetaTelescopeReducing ( inferType thm)
@@ -652,75 +652,63 @@ where
trace[Meta.Tactic.simp.heads] "{repr e.toHeadIndex}"
simpLoop e
@[inline] def withSimpContext (ctx : Context) (x : MetaM α) : MetaM α :=
@[inline] def withSimpConfig (ctx : Context) (x : MetaM α) : MetaM α :=
withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible x
def main (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Result × Stats) := do
let ctx := { ctx with config := ( ctx.config.updateArith), lctxInitIndices := ( getLCtx).numIndices }
withSimpContext ctx do
let (r, s) simpMain e methods.toMethodsRef ctx |>.run { stats with }
trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
return (r, { s with })
where
simpMain (e : Expr) : SimpM Result := withCatchingRuntimeEx do
def main (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Result × UsedSimps) := do
let ctx := { ctx with config := ( ctx.config.updateArith) }
withSimpConfig ctx do withCatchingRuntimeEx do
try
withoutCatchingRuntimeEx <| simp e
withoutCatchingRuntimeEx do
let (r, s) simp e methods.toMethodsRef ctx |>.run { usedTheorems := usedSimps }
trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
return (r, s.usedTheorems)
catch ex =>
reportDiag ( get).diag
if ex.isRuntime then
throwNestedTacticEx `simp ex
else
throw ex
if ex.isRuntime then throwNestedTacticEx `simp ex else throw ex
def dsimpMain (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Expr × Stats) := do
withSimpContext ctx do
let (r, s) dsimpMain e methods.toMethodsRef ctx |>.run { stats with }
pure (r, { s with })
where
dsimpMain (e : Expr) : SimpM Expr := withCatchingRuntimeEx do
def dsimpMain (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Expr × UsedSimps) := do
withSimpConfig ctx do withCatchingRuntimeEx do
try
withoutCatchingRuntimeEx <| dsimp e
withoutCatchingRuntimeEx do
let (r, s) dsimp e methods.toMethodsRef ctx |>.run { usedTheorems := usedSimps }
pure (r, s.usedTheorems)
catch ex =>
reportDiag ( get).diag
if ex.isRuntime then
throwNestedTacticEx `simp ex
else
throw ex
if ex.isRuntime then throwNestedTacticEx `dsimp ex else throw ex
end Simp
open Simp (SimprocsArray Stats)
open Simp (UsedSimps SimprocsArray)
def simp (e : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
(stats : Stats := {}) : MetaM (Simp.Result × Stats) := do profileitM Exception "simp" ( getOptions) do
(usedSimps : UsedSimps := {}) : MetaM (Simp.Result × UsedSimps) := do profileitM Exception "simp" ( getOptions) do
match discharge? with
| none => Simp.main e ctx stats (methods := Simp.mkDefaultMethodsCore simprocs)
| some d => Simp.main e ctx stats (methods := Simp.mkMethods simprocs d (wellBehavedDischarge := false))
| none => Simp.main e ctx usedSimps (methods := Simp.mkDefaultMethodsCore simprocs)
| some d => Simp.main e ctx usedSimps (methods := Simp.mkMethods simprocs d)
def dsimp (e : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[])
(stats : Stats := {}) : MetaM (Expr × Stats) := do profileitM Exception "dsimp" ( getOptions) do
Simp.dsimpMain e ctx stats (methods := Simp.mkDefaultMethodsCore simprocs )
(usedSimps : UsedSimps := {}) : MetaM (Expr × UsedSimps) := do profileitM Exception "dsimp" ( getOptions) do
Simp.dsimpMain e ctx usedSimps (methods := Simp.mkDefaultMethodsCore simprocs )
/-- See `simpTarget`. This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
(mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option MVarId × Stats) := do
(mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
let target instantiateMVars ( mvarId.getType)
let (r, stats) simp target ctx simprocs discharge? stats
let (r, usedSimps) simp target ctx simprocs discharge? usedSimps
if mayCloseGoal && r.expr.isTrue then
match r.proof? with
| some proof => mvarId.assign ( mkOfEqTrue proof)
| none => mvarId.assign (mkConst ``True.intro)
return (none, stats)
return (none, usedSimps)
else
return ( applySimpResultToTarget mvarId target r, stats)
return ( applySimpResultToTarget mvarId target r, usedSimps)
/--
Simplify the given goal target (aka type). Return `none` if the goal was closed. Return `some mvarId'` otherwise,
where `mvarId'` is the simplified new goal. -/
def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
(mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option MVarId × Stats) :=
(mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) :=
mvarId.withContext do
mvarId.checkNotAssigned `simp
simpTargetCore mvarId ctx simprocs discharge? mayCloseGoal stats
simpTargetCore mvarId ctx simprocs discharge? mayCloseGoal usedSimps
/--
Apply the result `r` for `prop` (which is inhabited by `proof`). Return `none` if the goal was closed. Return `some (proof', prop')`
@@ -752,9 +740,9 @@ def applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result
This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
(mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option (Expr × Expr) × Stats) := do
let (r, stats) simp prop ctx simprocs discharge? stats
return ( applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal), stats)
(mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (Expr × Expr) × UsedSimps) := do
let (r, usedSimps) simp prop ctx simprocs discharge? usedSimps
return ( applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal), usedSimps)
def applySimpResultToLocalDeclCore (mvarId : MVarId) (fvarId : FVarId) (r : Option (Expr × Expr)) : MetaM (Option (FVarId × MVarId)) := do
match r with
@@ -785,99 +773,99 @@ def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Res
applySimpResultToLocalDeclCore mvarId fvarId ( applySimpResultToFVarId mvarId fvarId r mayCloseGoal)
def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
(mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option (FVarId × MVarId) × Stats) := do
(mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (FVarId × MVarId) × UsedSimps) := do
mvarId.withContext do
mvarId.checkNotAssigned `simp
let type instantiateMVars ( fvarId.getType)
let (r, stats) simpStep mvarId (mkFVar fvarId) type ctx simprocs discharge? mayCloseGoal stats
return ( applySimpResultToLocalDeclCore mvarId fvarId r, stats)
let (r, usedSimps) simpStep mvarId (mkFVar fvarId) type ctx simprocs discharge? mayCloseGoal usedSimps
return ( applySimpResultToLocalDeclCore mvarId fvarId r, usedSimps)
def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
(simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
(stats : Stats := {}) : MetaM (Option (Array FVarId × MVarId) × Stats) := do
(usedSimps : UsedSimps := {}) : MetaM (Option (Array FVarId × MVarId) × UsedSimps) := do
mvarId.withContext do
mvarId.checkNotAssigned `simp
let mut mvarIdNew := mvarId
let mut toAssert := #[]
let mut replaced := #[]
let mut stats := stats
let mut usedSimps := usedSimps
for fvarId in fvarIdsToSimp do
let localDecl fvarId.getDecl
let type instantiateMVars localDecl.type
let ctx := { ctx with simpTheorems := ctx.simpTheorems.eraseTheorem (.fvar localDecl.fvarId) }
let (r, stats') simp type ctx simprocs discharge? stats
stats := stats'
let (r, usedSimps') simp type ctx simprocs discharge? usedSimps
usedSimps := usedSimps'
match r.proof? with
| some _ => match ( applySimpResultToProp mvarIdNew (mkFVar fvarId) type r) with
| none => return (none, stats)
| none => return (none, usedSimps)
| some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
| none =>
if r.expr.isFalse then
mvarIdNew.assign ( mkFalseElim ( mvarIdNew.getType) (mkFVar fvarId))
return (none, stats)
return (none, usedSimps)
-- TODO: if there are no forwards dependencies we may consider using the same approach we used when `r.proof?` is a `some ...`
-- Reason: it introduces a `mkExpectedTypeHint`
mvarIdNew mvarIdNew.replaceLocalDeclDefEq fvarId r.expr
replaced := replaced.push fvarId
if simplifyTarget then
match ( simpTarget mvarIdNew ctx simprocs discharge? (stats := stats)) with
| (none, stats') => return (none, stats')
| (some mvarIdNew', stats') => mvarIdNew := mvarIdNew'; stats := stats'
match ( simpTarget mvarIdNew ctx simprocs discharge? (usedSimps := usedSimps)) with
| (none, usedSimps') => return (none, usedSimps')
| (some mvarIdNew', usedSimps') => mvarIdNew := mvarIdNew'; usedSimps := usedSimps'
let (fvarIdsNew, mvarIdNew') mvarIdNew.assertHypotheses toAssert
mvarIdNew := mvarIdNew'
let toClear := fvarIdsToSimp.filter fun fvarId => !replaced.contains fvarId
mvarIdNew mvarIdNew.tryClearMany toClear
if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
throwError "simp made no progress"
return (some (fvarIdsNew, mvarIdNew), stats)
return (some (fvarIdsNew, mvarIdNew), usedSimps)
def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
(stats : Stats := {}) : MetaM (TacticResultCNM × Stats) := mvarId.withContext do
(usedSimps : UsedSimps := {}) : MetaM (TacticResultCNM × UsedSimps) := mvarId.withContext do
let mut ctx := ctx
for h in ( getPropHyps) do
let localDecl h.getDecl
let proof := localDecl.toExpr
let simpTheorems ctx.simpTheorems.addTheorem (.fvar h) proof
ctx := { ctx with simpTheorems }
match ( simpTarget mvarId ctx simprocs discharge? (stats := stats)) with
| (none, stats) => return (TacticResultCNM.closed, stats)
| (some mvarId', stats') =>
match ( simpTarget mvarId ctx simprocs discharge? (usedSimps := usedSimps)) with
| (none, usedSimps) => return (TacticResultCNM.closed, usedSimps)
| (some mvarId', usedSimps') =>
if ( mvarId.getType) == ( mvarId'.getType) then
return (TacticResultCNM.noChange, stats)
return (TacticResultCNM.noChange, usedSimps)
else
return (TacticResultCNM.modified mvarId', stats')
return (TacticResultCNM.modified mvarId', usedSimps')
def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
(stats : Stats := {}) : MetaM (Option MVarId × Stats) := do
(usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
mvarId.withContext do
mvarId.checkNotAssigned `simp
let mut mvarIdNew := mvarId
let mut stats : Stats := stats
let mut usedSimps : UsedSimps := usedSimps
for fvarId in fvarIdsToSimp do
let type instantiateMVars ( fvarId.getType)
let (typeNew, stats') dsimp type ctx simprocs
stats := stats'
let (typeNew, usedSimps') dsimp type ctx simprocs
usedSimps := usedSimps'
if typeNew.isFalse then
mvarIdNew.assign ( mkFalseElim ( mvarIdNew.getType) (mkFVar fvarId))
return (none, stats)
return (none, usedSimps)
if typeNew != type then
mvarIdNew mvarIdNew.replaceLocalDeclDefEq fvarId typeNew
if simplifyTarget then
let target mvarIdNew.getType
let (targetNew, stats') dsimp target ctx simprocs stats
stats := stats'
let (targetNew, usedSimps') dsimp target ctx simprocs usedSimps
usedSimps := usedSimps'
if targetNew.isTrue then
mvarIdNew.assign (mkConst ``True.intro)
return (none, stats)
return (none, usedSimps)
if let some (_, lhs, rhs) := targetNew.consumeMData.eq? then
if ( withReducible <| isDefEq lhs rhs) then
mvarIdNew.assign ( mkEqRefl lhs)
return (none, stats)
return (none, usedSimps)
if target != targetNew then
mvarIdNew mvarIdNew.replaceTargetDefEq targetNew
pure () -- FIXME: bug in do notation if this is removed?
if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
throwError "dsimp made no progress"
return (some mvarIdNew, stats)
return (some mvarIdNew, usedSimps)
end Lean.Meta

View File

@@ -109,7 +109,6 @@ where
return false
private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do
recordTriedSimpTheorem thm.origin
let rec go (e : Expr) : SimpM (Option Result) := do
if ( isDefEq lhs e) then
unless ( synthesizeArgs thm.origin bis xs) do
@@ -407,7 +406,6 @@ def mkSEvalMethods : CoreM Methods := do
dpre := dpreDefault #[s]
dpost := dpostDefault #[s]
discharge? := dischargeGround
wellBehavedDischarge := true
}
def mkSEvalContext : CoreM Context := do
@@ -495,16 +493,10 @@ where
| .forallE _ d b _ => (d.isEq || d.isHEq || b.hasLooseBVar 0) && go b
| _ => e.isFalse
private def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do
let lctxInitIndices := ( readThe Simp.Context).lctxInitIndices
let contextual := ( getConfig).contextual
def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do
( getLCtx).findDeclRevM? fun localDecl => do
if localDecl.isImplementationDetail then
return none
-- The following test is needed to ensure `dischargeUsingAssumption?` is a
-- well-behaved discharger. See comment at `Methods.wellBehavedDischarge`
else if !contextual && localDecl.index >= lctxInitIndices then
return none
else if ( isDefEq e localDecl.type) then
return some localDecl.toExpr
else
@@ -553,17 +545,16 @@ def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
abbrev Discharge := Expr SimpM (Option Expr)
def mkMethods (s : SimprocsArray) (discharge? : Discharge) (wellBehavedDischarge : Bool) : Methods := {
def mkMethods (s : SimprocsArray) (discharge? : Discharge) : Methods := {
pre := preDefault s
post := postDefault s
dpre := dpreDefault s
dpost := dpostDefault s
discharge?
wellBehavedDischarge
discharge? := discharge?
}
def mkDefaultMethodsCore (simprocs : SimprocsArray) : Methods :=
mkMethods simprocs dischargeDefault? (wellBehavedDischarge := true)
mkMethods simprocs dischargeDefault?
def mkDefaultMethods : CoreM Methods := do
if simprocs.get ( getOptions) then

View File

@@ -10,7 +10,7 @@ import Lean.Meta.Tactic.Simp.Main
namespace Lean.Meta
open Simp (Stats SimprocsArray)
open Simp (UsedSimps SimprocsArray)
namespace SimpAll
@@ -24,13 +24,12 @@ structure Entry where
deriving Inhabited
structure State where
modified : Bool := false
mvarId : MVarId
entries : Array Entry := #[]
ctx : Simp.Context
simprocs : SimprocsArray
usedTheorems : Simp.UsedSimps := {}
diag : Simp.Diagnostics := {}
modified : Bool := false
mvarId : MVarId
entries : Array Entry := #[]
ctx : Simp.Context
simprocs : SimprocsArray
usedSimps : UsedSimps := {}
abbrev M := StateRefT State MetaM
@@ -63,8 +62,8 @@ private partial def loop : M Bool := do
-- We disable the current entry to prevent it to be simplified to `True`
let simpThmsWithoutEntry := ( getSimpTheorems).eraseTheorem entry.id
let ctx := { ctx with simpTheorems := simpThmsWithoutEntry }
let (r, stats) simpStep ( get).mvarId entry.proof entry.type ctx simprocs (stats := { ( get) with })
modify fun s => { s with usedTheorems := stats.usedTheorems, diag := stats.diag }
let (r, usedSimps) simpStep ( get).mvarId entry.proof entry.type ctx simprocs (usedSimps := ( get).usedSimps)
modify fun s => { s with usedSimps }
match r with
| none => return true -- closed the goal
| some (proofNew, typeNew) =>
@@ -103,8 +102,8 @@ private partial def loop : M Bool := do
}
-- simplify target
let mvarId := ( get).mvarId
let (r, stats) simpTarget mvarId ( get).ctx simprocs (stats := { ( get) with })
modify fun s => { s with usedTheorems := stats.usedTheorems, diag := stats.diag }
let (r, usedSimps) simpTarget mvarId ( get).ctx simprocs (usedSimps := ( get).usedSimps)
modify fun s => { s with usedSimps }
match r with
| none => return true
| some mvarIdNew =>
@@ -144,12 +143,12 @@ def main : M (Option MVarId) := do
end SimpAll
def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (stats : Stats := {}) : MetaM (Option MVarId × Stats) := do
def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
mvarId.withContext do
let (r, s) SimpAll.main.run { stats with mvarId, ctx, simprocs }
let (r, s) SimpAll.main.run { mvarId, ctx, usedSimps, simprocs }
if let .some mvarIdNew := r then
if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
throwError "simp_all made no progress"
return (r, { s with })
return (r, s.usedSimps)
end Lean.Meta

View File

@@ -50,9 +50,6 @@ def Origin.key : Origin → Name
instance : BEq Origin := (·.key == ·.key)
instance : Hashable Origin := (hash ·.key)
instance : LT Origin := (·.key.lt ·.key)
instance (a b : Origin) : Decidable (a < b) :=
inferInstanceAs (Decidable (a.key.lt b.key = true))
/-
Note: we want to use iota reduction when indexing instances. Otherwise,

View File

@@ -90,12 +90,6 @@ structure Context where
-/
parent? : Option Expr := none
dischargeDepth : UInt32 := 0
/--
Number of indices in the local context when starting `simp`.
We use this information to decide which assumptions we can use without
invalidating the cache.
-/
lctxInitIndices : Nat := 0
deriving Inhabited
def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
@@ -104,25 +98,11 @@ def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
-- We should use `PHashMap` because we backtrack the contents of `UsedSimps`
abbrev UsedSimps := PHashMap Origin Nat
structure Diagnostics where
/-- Number of times each simp theorem has been used/applied. -/
usedThmCounter : PHashMap Origin Nat := {}
/-- Number of times each simp theorem has been tried. -/
triedThmCounter : PHashMap Origin Nat := {}
/-- Number of times each congr theorem has been tried. -/
congrThmCounter : PHashMap Name Nat := {}
deriving Inhabited
structure State where
cache : Cache := {}
congrCache : CongrCache := {}
usedTheorems : UsedSimps := {}
numSteps : Nat := 0
diag : Diagnostics := {}
structure Stats where
usedTheorems : UsedSimps := {}
diag : Diagnostics := {}
private opaque MethodsRefPointed : NonemptyType.{0}
@@ -138,10 +118,6 @@ opaque simp (e : Expr) : SimpM Result
@[extern "lean_dsimp"]
opaque dsimp (e : Expr) : SimpM Expr
@[inline] def modifyDiag (f : Diagnostics Diagnostics) : SimpM Unit := do
if ( isDiagnosticsEnabled) then
modify fun { cache, congrCache, usedTheorems, numSteps, diag } => { cache, congrCache, usedTheorems, numSteps, diag := f diag }
/--
Result type for a simplification procedure. We have `pre` and `post` simplication procedures.
-/
@@ -254,18 +230,11 @@ structure Simprocs where
deriving Inhabited
structure Methods where
pre : Simproc := fun _ => return .continue
post : Simproc := fun e => return .done { expr := e }
dpre : DSimproc := fun _ => return .continue
dpost : DSimproc := fun e => return .done e
pre : Simproc := fun _ => return .continue
post : Simproc := fun e => return .done { expr := e }
dpre : DSimproc := fun _ => return .continue
dpost : DSimproc := fun e => return .done e
discharge? : Expr SimpM (Option Expr) := fun _ => return none
/--
`wellBehavedDischarge` must **not** be set to `true` IF `discharge?`
access local declarations with index >= `Context.lctxInitIndices` when
`contextual := false`.
Reason: it would prevent us from aggressively caching `simp` results.
-/
wellBehavedDischarge : Bool := true
deriving Inhabited
unsafe def Methods.toMethodsRefImpl (m : Methods) : MethodsRef :=
@@ -319,19 +288,10 @@ Save current cache, reset it, execute `x`, and then restore original cache.
modify fun s => { s with cache := {} }
try x finally modify fun s => { s with cache := cacheSaved }
@[inline] def withDischarger (discharge? : Expr SimpM (Option Expr)) (wellBehavedDischarge : Bool) (x : SimpM α) : SimpM α :=
withFreshCache <|
withReader (fun r => { MethodsRef.toMethods r with discharge?, wellBehavedDischarge }.toMethodsRef) x
def recordTriedSimpTheorem (thmId : Origin) : SimpM Unit := do
modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } =>
let cNew := if let some c := triedThmCounter.find? thmId then c + 1 else 1
{ usedThmCounter, triedThmCounter := triedThmCounter.insert thmId cNew, congrThmCounter }
@[inline] def withDischarger (discharge? : Expr SimpM (Option Expr)) (x : SimpM α) : SimpM α :=
withFreshCache <| withReader (fun r => { MethodsRef.toMethods r with discharge? }.toMethodsRef) x
def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } =>
let cNew := if let some c := usedThmCounter.find? thmId then c + 1 else 1
{ usedThmCounter := usedThmCounter.insert thmId cNew, triedThmCounter, congrThmCounter }
/-
If `thmId` is an equational theorem (e.g., `foo.eq_1`), we should record `foo` instead.
See issue #3547.
@@ -351,11 +311,6 @@ def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
let n := s.usedTheorems.size
{ s with usedTheorems := s.usedTheorems.insert thmId n }
def recordCongrTheorem (declName : Name) : SimpM Unit := do
modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } =>
let cNew := if let some c := congrThmCounter.find? declName then c + 1 else 1
{ congrThmCounter := congrThmCounter.insert declName cNew, triedThmCounter, usedThmCounter }
def Result.getProof (r : Result) : MetaM Expr := do
match r.proof? with
| some p => return p

View File

@@ -344,7 +344,7 @@ inductive ProjReductionKind where
| yesWithDelta
/--
Projections `s.i` are reduced at `whnfCore`, and `whnfAtMostI` is used at `s` during the process.
Recall that `whnfAtMostI` is like `whnf` but uses transparency at most `instances`.
Recall that `whnfAtMostII` is like `whnf` but uses transparency at most `instances`.
This option is stronger than `yes`, but weaker than `yesWithDelta`.
We use this option to ensure we reduce projections to prevent expensive defeq checks when unifying TC operations.
When unifying e.g. `(@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1`,
@@ -608,11 +608,10 @@ where
| .notMatcher =>
matchConstAux f' (fun _ => return e) fun cinfo lvls =>
match cinfo with
| .recInfo rec => reduceRec rec lvls e.getAppArgs (fun _ => return e) (fun e => do recordUnfold cinfo.name; go e)
| .quotInfo rec => reduceQuotRec rec e.getAppArgs (fun _ => return e) (fun e => do recordUnfold cinfo.name; go e)
| .recInfo rec => reduceRec rec lvls e.getAppArgs (fun _ => return e) go
| .quotInfo rec => reduceQuotRec rec e.getAppArgs (fun _ => return e) go
| c@(.defnInfo _) => do
if ( isAuxDef c.name) then
recordUnfold c.name
deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => return e) go
else
return e
@@ -707,7 +706,7 @@ mutual
| some e =>
match ( withReducibleAndInstances <| reduceProj? e.getAppFn) with
| none => return none
| some r => recordUnfold declName; return mkAppN r e.getAppArgs |>.headBeta
| some r => return mkAppN r e.getAppArgs |>.headBeta
| _ => return none
| _ => return none
@@ -730,9 +729,8 @@ mutual
if fInfo.levelParams.length != fLvls.length then
return none
else
let unfoldDefault (_ : Unit) : MetaM (Option Expr) := do
let unfoldDefault (_ : Unit) : MetaM (Option Expr) :=
if fInfo.hasValue then
recordUnfold fInfo.name
deltaBetaDefinition fInfo fLvls e.getAppRevArgs (fun _ => pure none) (fun e => pure (some e))
else
return none
@@ -780,13 +778,11 @@ mutual
Thus, we should keep `return some r` until Mathlib has been ported to Lean 3.
Note that the `Vector` example above does not even work in Lean 3.
-/
let some recArgPos getStructuralRecArgPos? fInfo.name
| recordUnfold fInfo.name; return some r
let some recArgPos getStructuralRecArgPos? fInfo.name | return some r
let numArgs := e.getAppNumArgs
if recArgPos >= numArgs then return none
let recArg := e.getArg! recArgPos numArgs
if !( isConstructorApp ( whnfMatcher recArg)) then return none
recordUnfold fInfo.name
return some r
| _ =>
if ( getMatcherInfo? fInfo.name).isSome then
@@ -804,7 +800,7 @@ mutual
unless cinfo.hasValue do return none
deltaDefinition cinfo lvls
(fun _ => pure none)
(fun e => do recordUnfold declName; pure (some e))
(fun e => pure (some e))
| _ => return none
end
@@ -837,11 +833,11 @@ def reduceRecMatcher? (e : Expr) : MetaM (Option Expr) := do
| .reduced e => return e
| _ => matchConstAux e.getAppFn (fun _ => pure none) fun cinfo lvls => do
match cinfo with
| .recInfo «rec» => reduceRec «rec» lvls e.getAppArgs (fun _ => pure none) (fun e => do recordUnfold cinfo.name; pure (some e))
| .quotInfo «rec» => reduceQuotRec «rec» e.getAppArgs (fun _ => pure none) (fun e => do recordUnfold cinfo.name; pure (some e))
| .recInfo «rec» => reduceRec «rec» lvls e.getAppArgs (fun _ => pure none) (fun e => pure (some e))
| .quotInfo «rec» => reduceQuotRec «rec» e.getAppArgs (fun _ => pure none) (fun e => pure (some e))
| c@(.defnInfo _) =>
if ( isAuxDef c.name) then
deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => pure none) (fun e => do recordUnfold c.name; pure (some e))
deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => pure none) (fun e => pure (some e))
else
return none
| _ => return none

View File

@@ -807,10 +807,6 @@ It is especially useful for avoiding parentheses with repeated applications.
Given `h : a = b` and `e : p a`, the term `h ▸ e` has type `p b`.
You can also view `h ▸ e` as a "type casting" operation
where you change the type of `e` by using `h`.
The macro tries both orientations of `h`. If the context provides an
expected type, it rewrites the expeced type, else it rewrites the type of e`.
See the Chapter "Quantifiers and Equality" in the manual
"Theorem Proving in Lean" for additional information.
-/
@@ -874,7 +870,7 @@ def matchExprElseAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (ho
def matchExprAlts (rhsParser : Parser) :=
leading_parser withPosition $
many (ppLine >> checkColGe "irrelevant" >> notFollowedBy (symbol "| " >> " _ ") "irrelevant" >> matchExprAlt rhsParser)
>> (ppLine >> checkColGe "else-alternative for `match_expr`, i.e., `| _ => ...`" >> matchExprElseAlt rhsParser)
>> (ppLine >> checkColGe "irrelevant" >> matchExprElseAlt rhsParser)
@[builtin_term_parser] def matchExpr := leading_parser:leadPrec
"match_expr " >> termParser >> " with" >> ppDedent (matchExprAlts termParser)

View File

@@ -13,10 +13,7 @@ import Lean.ParserCompiler
namespace Lean
def PPContext.runCoreM {α : Type} (ppCtx : PPContext) (x : CoreM α) : IO α :=
Prod.fst <$> x.toIO { options := ppCtx.opts, currNamespace := ppCtx.currNamespace
openDecls := ppCtx.openDecls
fileName := "<PrettyPrinter>", fileMap := default
diag := getDiag ppCtx.opts }
Prod.fst <$> x.toIO { options := ppCtx.opts, currNamespace := ppCtx.currNamespace, openDecls := ppCtx.openDecls, fileName := "<PrettyPrinter>", fileMap := default }
{ env := ppCtx.env, ngen := { namePrefix := `_pp_uniq } }
def PPContext.runMetaM {α : Type} (ppCtx : PPContext) (x : MetaM α) : IO α :=
@@ -51,9 +48,7 @@ def ppExprWithInfos (e : Expr) (optsPerPos : Delaborator.OptionsPerPos := {}) (d
@[export lean_pp_expr]
def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format :=
Prod.fst <$> ((withOptions (fun _ => opts) <| ppExpr e).run' { lctx := lctx } { mctx := mctx }).toIO
{ fileName := "<PrettyPrinter>", fileMap := default }
{ env := env }
Prod.fst <$> ((ppExpr e).run' { lctx := lctx } { mctx := mctx }).toIO { options := opts, fileName := "<PrettyPrinter>", fileMap := default } { env := env }
def ppTactic (stx : TSyntax `tactic) : CoreM Format := ppCategory `tactic stx

View File

@@ -257,22 +257,6 @@ private partial def withoutParentProjections (explicit : Bool) (d : DelabM α) :
else
d
-- TODO(kmill): make sure that we only strip projections so long as it doesn't change how it elaborates.
-- This affects `withoutParentProjections` as well.
/-- Strips parent projections from `s`. Assumes that the current SubExpr is the same as the one used when delaborating `s`. -/
private partial def stripParentProjections (s : Term) : DelabM Term :=
match s with
| `($x.$f:ident) => do
if let some field try parentProj? false ( getExpr) catch _ => pure none then
if f.getId == field then
withAppArg <| stripParentProjections x
else
return s
else
return s
| _ => return s
/--
In explicit mode, decides whether or not the applied function needs `@`,
where `numArgs` is the number of arguments actually supplied to `f`.
@@ -329,27 +313,6 @@ def delabAppExplicitCore (fieldNotation : Bool) (numArgs : Nat) (delabHead : (in
else
return Syntax.mkApp fnStx argStxs
/-- Records how a particular argument to a function is delaborated, in non-explicit mode. -/
inductive AppImplicitArg
/-- An argument to skip, like an implicit argument. -/
| skip
/-- A regular argument. -/
| regular (s : Term)
/-- It's a named argument. Named arguments inhibit applying unexpanders. -/
| named (s : TSyntax ``Parser.Term.namedArgument)
deriving Inhabited
/-- Whether unexpanding is allowed with this argument. -/
def AppImplicitArg.canUnexpand : AppImplicitArg Bool
| .regular .. | .skip => true
| .named .. => false
/-- If the argument has associated syntax, returns it. -/
def AppImplicitArg.syntax? : AppImplicitArg Option Syntax
| .skip => none
| .regular s => s
| .named s => s
/--
Delaborates a function application in the standard mode, where implicit arguments are generally not
included, unless `pp.analysis.namedArg` is set at that argument.
@@ -367,74 +330,76 @@ def delabAppImplicitCore (unexpand : Bool) (numArgs : Nat) (delabHead : Delab) (
appFieldNotationCandidate?
else
pure none
let (fnStx, args)
let (shouldUnexpand, fnStx, fieldIdx?, _, _, argStxs, argData)
withBoundedAppFnArgs numArgs
(do return (( delabHead), Array.mkEmpty numArgs))
(fun (fnStx, args) => do
let idx := args.size
let arg mkArg (numArgs - idx - 1) paramKinds[idx]!
return (fnStx, args.push arg))
-- App unexpanders
if pure unexpand <&&> getPPOption getPPNotation then
(do return (unexpand, delabHead, none, 0, paramKinds.toList, Array.mkEmpty numArgs, (Array.mkEmpty numArgs).push (unexpand, 0)))
(fun (shouldUnexpand, fnStx, fieldIdx?, idx, paramKinds, argStxs, argData) => do
/-
- `argStxs` is the accumulated array of arguments that should be pretty printed
- `argData` is a list of `Bool × Nat` used to figure out:
1. whether an unexpander could be used for the prefix up to this argument and
2. how many arguments we need to include after this one when annotating the result of unexpansion.
Argument `argStxs[i]` corresponds to `argData[i+1]`, with `argData[0]` being for the head itself.
-/
if some idx = field?.map Prod.fst then
-- This is the object for field notation.
let fieldObj withoutParentProjections (explicit := false) delab
return (false, fnStx, some argStxs.size, idx + 1, paramKinds.tailD [], argStxs.push fieldObj, argData.push (false, 1))
let (argUnexpandable, stx?) mkArgStx (numArgs - idx - 1) paramKinds
let shouldUnexpand := shouldUnexpand && argUnexpandable
let (argStxs, argData) :=
match stx?, argData.back with
-- By default, a pretty-printed argument accounts for just itself.
| some stx, _ => (argStxs.push stx, argData.push (shouldUnexpand, 1))
-- A non-pretty-printed argument is accounted for by the previous pretty printed one.
| none, (_, argCount) => (argStxs, argData.pop.push (shouldUnexpand, argCount + 1))
return (shouldUnexpand, fnStx, fieldIdx?, idx + 1, paramKinds.tailD [], argStxs, argData))
if let some fieldIdx := fieldIdx? then
-- Delaborate using field notation
let field := field?.get!.2
let obj := argStxs[fieldIdx]!
let mut head : Term `($obj.$(mkIdent field))
if fieldIdx == 0 then
-- If it's the first argument (after some implicit arguments), we can tag `obj.field` with a prefix of the application
-- including the implicit arguments immediately before and after `obj`.
head withBoundedAppFn (numArgs - argData[0]!.2 - argData[1]!.2) <| annotateTermInfo <| head
return Syntax.mkApp head (argStxs.eraseIdx fieldIdx)
if pure (argData.any Prod.fst) <&&> getPPOption getPPNotation then
-- Try using an app unexpander for a prefix of the arguments.
if let some stx (some <$> tryAppUnexpanders fnStx args) <|> pure none then
if let some stx (some <$> tryAppUnexpanders fnStx argStxs argData) <|> pure none then
return stx
let stx := Syntax.mkApp fnStx (args.filterMap (·.syntax?))
-- Structure instance notation
if pure (unexpand && args.all (·.canUnexpand)) <&&> getPPOption getPPStructureInstances then
let stx := Syntax.mkApp fnStx argStxs
if pure shouldUnexpand <&&> getPPOption getPPStructureInstances then
-- Try using the structure instance unexpander.
-- It only makes sense applying this to the entire application, since structure instances cannot themselves be applied.
if let some stx (some <$> unexpandStructureInstance stx) <|> pure none then
return stx
-- Field notation
if let some (fieldIdx, field) := field? then
if fieldIdx < args.size then
let obj? : Option Term do
let arg := args[fieldIdx]!
if let .regular s := arg then
withNaryArg fieldIdx <| some <$> stripParentProjections s
else
pure none
if let some obj := obj? then
let isFirst := args[0:fieldIdx].all (· matches .skip)
-- Clear the `obj` argument from `args`.
let args' := args.set! fieldIdx .skip
let mut head : Term `($obj.$(mkIdent field))
if isFirst then
-- If the object is the first argument (after some implicit arguments),
-- we can annotate `obj.field` with the prefix of the application
-- that includes all the implicit arguments immediately before and after `obj`.
let objArity := args'.findIdx? (fun a => !(a matches .skip)) |>.getD args'.size
head withBoundedAppFn (numArgs - objArity) <| annotateTermInfo <| head
return Syntax.mkApp head (args'.filterMap (·.syntax?))
-- Normal application
return stx
where
mkNamedArg (name : Name) : DelabM AppImplicitArg :=
return .named <| `(Parser.Term.namedArgument| ($(mkIdent name) := $( delab)))
mkNamedArg (name : Name) (argStx : Syntax) : DelabM (Bool × Option Syntax) :=
return (false, `(Parser.Term.namedArgument| ($(mkIdent name) := $argStx)))
/--
Delaborates the current argument.
The argument `remainingArgs` is the number of arguments in the application after this one.
If the argument should be pretty printed then it returns the syntax for that argument.
The boolean is `false` if an unexpander should not be used for the application due to this argument.
The argumnet `remainingArgs` is the number of arguments in the application after this one.
-/
mkArg (remainingArgs : Nat) (param : ParamKind) : DelabM AppImplicitArg := do
let arg getExpr
if getPPOption getPPAnalysisSkip then return .skip
else if getPPOption getPPAnalysisHole then return .regular ( `(_))
else if getPPOption getPPAnalysisNamedArg then
mkNamedArg param.name
else if param.defVal.isSome && remainingArgs == 0 && param.defVal.get! == arg then
-- Assumption: `useAppExplicit` has already detected whether it is ok to omit this argument
return .skip
else if param.bInfo.isExplicit then
return .regular ( delab)
else if pure (param.name == `motive) <&&> shouldShowMotive arg ( getOptions) then
mkNamedArg param.name
mkArgStx (remainingArgs : Nat) (paramKinds : List ParamKind) : DelabM (Bool × Option Syntax) := do
if getPPOption getPPAnalysisSkip then return (true, none)
else if getPPOption getPPAnalysisHole then return (true, `(_))
else
return .skip
let arg getExpr
let param :: _ := paramKinds | unreachable!
if getPPOption getPPAnalysisNamedArg then
mkNamedArg param.name ( delab)
else if param.defVal.isSome && remainingArgs == 0 && param.defVal.get! == arg then
-- Assumption: `useAppExplicit` has already detected whether it is ok to omit this argument
return (true, none)
else if param.bInfo.isExplicit then
return (true, delab)
else if pure (param.name == `motive) <&&> shouldShowMotive arg ( getOptions) then
mkNamedArg param.name ( delab)
else
return (true, none)
/--
Runs the given unexpanders, returning the resulting syntax if any are applicable, and otherwise fails.
-/
@@ -449,26 +414,23 @@ where
try applying an app unexpander using some prefix of the arguments, longest prefix first.
This function makes sure that the unexpanded syntax is annotated and given TermInfo so that it is hoverable in the InfoView.
-/
tryAppUnexpanders (fnStx : Term) (args : Array AppImplicitArg) : Delab := do
tryAppUnexpanders (fnStx : Term) (argStxs : Array Syntax) (argData : Array (Bool × Nat)) : Delab := do
let .const c _ := ( getExpr).getAppFn.consumeMData | unreachable!
let fs := appUnexpanderAttribute.getValues ( getEnv) c
if fs.isEmpty then failure
let rec go (i : Nat) (implicitArgs : Nat) (argStxs : Array Syntax) : DelabM Term := do
match i with
let rec go (prefixArgs : Nat) : DelabM Term := do
let (unexpand, argCount) := argData[prefixArgs]!
match prefixArgs with
| 0 =>
guard unexpand
let stx tryUnexpand fs fnStx
return Syntax.mkApp ( annotateTermInfo stx) (args.filterMap (·.syntax?))
| i' + 1 =>
if args[i']!.syntax?.isSome then
(do let stx tryUnexpand fs <| Syntax.mkApp fnStx argStxs
let argStxs' := args.extract i args.size |>.filterMap (·.syntax?)
return Syntax.mkApp ( annotateTermInfo stx) argStxs')
<|> withBoundedAppFn (implicitArgs + 1) (go i' 0 argStxs.pop)
else
go i' (implicitArgs + 1) argStxs
let maxUnexpand := args.findIdx? (!·.canUnexpand) |>.getD args.size
withBoundedAppFn (args.size - maxUnexpand) <|
go maxUnexpand 0 (args.extract 0 maxUnexpand |>.filterMap (·.syntax?))
return Syntax.mkApp ( annotateTermInfo stx) argStxs
| prefixArgs' + 1 =>
(do guard unexpand
let stx tryUnexpand fs <| Syntax.mkApp fnStx (argStxs.extract 0 prefixArgs)
return Syntax.mkApp ( annotateTermInfo stx) (argStxs.extract prefixArgs argStxs.size))
<|> withBoundedAppFn argCount (go prefixArgs')
go argStxs.size
/--
Returns true if an application should use explicit mode when delaborating.
@@ -567,57 +529,64 @@ def withOverApp (arity : Nat) (x : Delab) : Delab := do
/-- State for `delabAppMatch` and helpers. -/
structure AppMatchState where
info : MatcherInfo
/-- The `matcherTy` instantiated with universe levels and the matcher parameters, with a position at the type of
this application prefix. -/
matcherTy : SubExpr
/-- The motive, with the pi type version delaborated and the original expression version.
Once `AppMatchState` is complete, this is not `none`. -/
matcherTy : Expr
params : Array Expr := #[]
motive : Option (Term × Expr) := none
/-- Whether `pp.analysis.namedArg` was set for the motive argument. -/
motiveNamed : Bool := false
/-- The delaborated discriminants, without `h :` annotations. -/
discrs : Array Term := #[]
/-- The collection of names used for the `h :` discriminant annotations, in order.
Uniquified names are constructed after the first phase. -/
hNames? : Array (Option Name) := #[]
/-- Lambda subexpressions for each alternate. -/
alts : Array SubExpr := #[]
/-- For each match alternative, the names to use for the pattern variables.
Each ends with `hNames?.filterMap id` exactly. -/
varNames : Array (Array Name) := #[]
/-- The delaborated right-hand sides for each match alternative. -/
rhss : Array Term := #[]
-- additional arguments applied to the result of the `match` expression
moreArgs : Array Term := #[]
/--
Skips `numParams` binders, and execute `x varNames` where `varNames` contains the new binder names.
The `hNames` array is used for the last params.
Helper for `delabAppMatch`.
-/
private partial def skippingBinders {α} (numParams : Nat) (hNames : Array Name) (x : Array Name DelabM α) : DelabM α := do
loop 0 #[]
Extract arguments of motive applications from the matcher type.
For the example below: `#[#[`([])], #[`(a::as)]]` -/
private partial def delabPatterns (st : AppMatchState) : DelabM (Array (Array Term)) :=
withReader (fun ctx => { ctx with inPattern := true, optionsPerPos := {} }) do
let ty instantiateForall st.matcherTy st.params
-- need to reduce `let`s that are lifted into the matcher type
forallTelescopeReducing ty fun params _ => do
-- skip motive and discriminators
let alts := Array.ofSubarray params[1 + st.discrs.size:]
alts.mapIdxM fun idx alt => do
let ty inferType alt
-- TODO: this is a hack; we are accessing the expression out-of-sync with the position
-- Currently, we reset `optionsPerPos` at the beginning of `delabPatterns` to avoid
-- incorrectly considering annotations.
withTheReader SubExpr ({ · with expr := ty }) $
usingNames st.varNames[idx]! do
withAppFnArgs (pure #[]) (fun pats => do pure $ pats.push ( delab))
where
loop (i : Nat) (varNames : Array Name) : DelabM α := do
let rec visitLambda : DelabM α := do
let varName := ( getExpr).bindingName!.eraseMacroScopes
if numParams - hNames.size i then
-- It is an "h annotation", so use the one we have already chosen.
let varName := hNames[i + hNames.size - numParams]!
withBindingBody varName do
loop (i + 1) (varNames.push varName)
else if varNames.contains varName then
-- Pattern variables must not shadow each other, so ensure a unique name
let varName := ( getLCtx).getUnusedName varName
withBindingBody varName do
loop (i + 1) (varNames.push varName)
else
withBindingBodyUnusedName fun id => do
loop (i + 1) (varNames.push id.getId)
if i < numParams then
usingNames {α} (varNames : Array Name) (x : DelabM α) : DelabM α :=
usingNamesAux 0 varNames x
usingNamesAux {α} (i : Nat) (varNames : Array Name) (x : DelabM α) : DelabM α :=
if i < varNames.size then
withBindingBody varNames[i]! <| usingNamesAux (i+1) varNames x
else
x
/-- Skip `numParams` binders, and execute `x varNames` where `varNames` contains the new binder names. -/
private partial def skippingBinders {α} (numParams : Nat) (x : Array Name DelabM α) : DelabM α :=
loop numParams #[]
where
loop : Nat Array Name DelabM α
| 0, varNames => x varNames
| n+1, varNames => do
let rec visitLambda : DelabM α := do
let varName := ( getExpr).bindingName!.eraseMacroScopes
-- Pattern variables cannot shadow each other
if varNames.contains varName then
let varName := ( getLCtx).getUnusedName varName
withBindingBody varName do
loop n (varNames.push varName)
else
withBindingBodyUnusedName fun id => do
loop n (varNames.push id.getId)
let e getExpr
if e.isLambda then
visitLambda
else
-- Eta expand `e`
-- eta expand `e`
let e forallTelescopeReducing ( inferType e) fun xs _ => do
if xs.size == 1 && ( inferType xs[0]!).isConstOf ``Unit then
-- `e` might be a thunk create by the dependent pattern matching compiler, and `xs[0]` may not even be a pattern variable.
@@ -628,117 +597,75 @@ where
else
mkLambdaFVars xs (mkAppN e xs)
withTheReader SubExpr (fun ctx => { ctx with expr := e }) visitLambda
else x varNames
/--
Delaborates applications of "matchers" such as
```
List.map.match_1 : {α : Type _} →
(motive : List α → Sort _) →
(x : List α) → (Unit → motive List.nil) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
```
Delaborate applications of "matchers" such as
```
List.map.match_1 : {α : Type _} →
(motive : List α → Sort _) →
(x : List α) → (Unit → motive List.nil) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
```
-/
@[builtin_delab app]
partial def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMatch do
-- Check that this is a matcher, and then set up overapplication.
let Expr.const c us := ( getExpr).getAppFn | failure
let some info getMatcherInfo? c | failure
withOverApp info.arity do
-- First pass visiting the match application. Incrementally fills `AppMatchState`,
-- collecting information needed to delaborate the patterns and RHSs.
-- No need to visit the parameters themselves.
let st : AppMatchState withBoundedAppFnArgs (1 + info.numDiscrs + info.numAlts)
(do
let params := ( getExpr).getAppArgs
let matcherTy : SubExpr :=
{ expr := instantiateForall ( instantiateTypeLevelParams ( getConstInfo c) us) params
pos := ( getPos).pushType }
guard <| isDefEq matcherTy.expr ( inferType ( getExpr))
return { info, matcherTy })
(fun st => do
if st.motive.isNone then
-- A motive for match notation is a type, so need to delaborate the lambda motive as a pi type.
let lamMotive getExpr
let piMotive lambdaTelescope lamMotive fun xs body => mkForallFVars xs body
-- TODO: pp.analyze has not analyzed `piMotive`, only `lamMotive`
-- Thus the binder types won't have any annotations.
-- Though, by using the same position we can use the body annotations
let piStx withTheReader SubExpr (fun cfg => { cfg with expr := piMotive }) delab
let named getPPOption getPPAnalysisNamedArg
return { st with motive := (piStx, lamMotive), motiveNamed := named }
else if st.discrs.size < st.info.numDiscrs then
return { st with discrs := st.discrs.push ( delab) }
else if st.alts.size < st.info.numAlts then
return { st with alts := st.alts.push ( readThe SubExpr) }
def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMatch do
-- incrementally fill `AppMatchState` from arguments
let st withAppFnArgs
(do
let (Expr.const c us) getExpr | failure
let (some info) getMatcherInfo? c | failure
let matcherTy instantiateTypeLevelParams ( getConstInfo c) us
return { matcherTy, info : AppMatchState })
(fun st => do
if st.params.size < st.info.numParams then
return { st with params := st.params.push ( getExpr) }
else if st.motive.isNone then
-- store motive argument separately
let lamMotive getExpr
let piMotive lambdaTelescope lamMotive fun xs body => mkForallFVars xs body
-- TODO: pp.analyze has not analyzed `piMotive`, only `lamMotive`
-- Thus the binder types won't have any annotations
let piStx withTheReader SubExpr (fun cfg => { cfg with expr := piMotive }) delab
let named getPPOption getPPAnalysisNamedArg
return { st with motive := (piStx, lamMotive), motiveNamed := named }
else if st.discrs.size < st.info.numDiscrs then
let idx := st.discrs.size
let discr delab
if let some hName := st.info.discrInfos[idx]!.hName? then
-- TODO: we should check whether the corresponding binder name, matches `hName`.
-- If it does not we should pretty print this `match` as a regular application.
return { st with discrs := st.discrs.push ( `(matchDiscr| $(mkIdent hName) : $discr)) }
else
panic! "impossible, number of arguments does not match arity")
return { st with discrs := st.discrs.push ( `(matchDiscr| $discr:term)) }
else if st.rhss.size < st.info.altNumParams.size then
/- We save the variables names here to be able to implement safe_shadowing.
The pattern delaboration must use the names saved here. -/
let (varNames, rhs) skippingBinders st.info.altNumParams[st.rhss.size]! fun varNames => do
let rhs delab
return (varNames, rhs)
return { st with rhss := st.rhss.push rhs, varNames := st.varNames.push varNames }
else
return { st with moreArgs := st.moreArgs.push ( delab) })
-- Second pass, create names for the h parameters, come up with pattern variable names,
-- and delaborate the RHSs.
-- We need to create dummy variables for the `h :` annotation variables first because they
-- come *last* in each alternative.
let st withDummyBinders (st.info.discrInfos.map (·.hName?)) ( getExpr) fun hNames? => do
let hNames := hNames?.filterMap id
let mut st := {st with hNames? := hNames?}
for i in [0:st.alts.size] do
st withTheReader SubExpr (fun _ => st.alts[i]!) do
-- We save the variables names here to be able to implement safe shadowing.
-- The pattern delaboration must use the names saved here.
skippingBinders st.info.altNumParams[i]! hNames fun varNames => do
let rhs delab
return { st with rhss := st.rhss.push rhs, varNames := st.varNames.push varNames }
return st
if st.discrs.size < st.info.numDiscrs || st.rhss.size < st.info.altNumParams.size then
-- underapplied
failure
if st.rhss.isEmpty then
`(nomatch $(st.discrs),*)
else
-- Third pass, delaborate patterns.
-- Extracts arguments of motive applications from the matcher type.
-- For the example in the docstring, yields `#[#[([])], #[(a::as)]]`.
let pats withReader (fun ctx => { ctx with inPattern := true, subExpr := st.matcherTy }) do
-- Need to reduce since there can be `let`s that are lifted into the matcher type
forallTelescopeReducing ( getExpr) fun afterParams _ => do
-- Skip motive and discriminators
let alts := Array.ofSubarray afterParams[1 + st.discrs.size:]
-- Visit minor premises
alts.mapIdxM fun idx alt => do
let altTy inferType alt
withTheReader SubExpr (fun ctx =>
{ ctx with expr := altTy, pos := ctx.pos.pushNthBindingDomain (1 + st.discrs.size + idx) }) do
usingNames st.varNames[idx]! <|
withAppFnArgs (pure #[]) fun pats => return pats.push ( delab)
-- Finally, assemble
let discrs (st.hNames?.zip st.discrs).mapM fun (hName?, discr) =>
match hName? with
| none => `(matchDiscr| $discr:term)
| some hName => `(matchDiscr| $(mkIdent hName) : $discr)
match st.discrs, st.rhss with
| #[discr], #[] =>
let stx `(nomatch $discr)
return Syntax.mkApp stx st.moreArgs
| _, #[] => failure
| _, _ =>
let pats delabPatterns st
let stx do
let (piStx, lamMotive) := st.motive.get!
let opts getOptions
-- TODO: disable the match if other implicits are needed?
if pure st.motiveNamed <||> shouldShowMotive lamMotive opts then
`(match (motive := $piStx) $[$discrs:matchDiscr],* with $[| $pats,* => $st.rhss]*)
`(match (motive := $piStx) $[$st.discrs:matchDiscr],* with $[| $pats,* => $st.rhss]*)
else
`(match $[$discrs:matchDiscr],* with $[| $pats,* => $st.rhss]*)
where
/-- Adds hNames to the local context to reserve their names and runs `m` in that context. -/
withDummyBinders {α : Type} (hNames? : Array (Option Name)) (body : Expr)
(m : Array (Option Name) DelabM α) (acc : Array (Option Name) := #[]) : DelabM α := do
let i := acc.size
if i < hNames?.size then
if let some name := hNames?[i]! then
let n' getUnusedName name body
withLocalDecl n' .default (.sort levelZero) (kind := .implDetail) fun _ =>
withDummyBinders hNames? body m (acc.push n')
else
withDummyBinders hNames? body m (acc.push none)
else
m acc
usingNames {α} (varNames : Array Name) (x : DelabM α) (i : Nat := 0) : DelabM α :=
if i < varNames.size then
withBindingBody varNames[i]! <| usingNames varNames x (i+1)
else
x
`(match $[$st.discrs:matchDiscr],* with $[| $pats,* => $st.rhss]*)
return Syntax.mkApp stx st.moreArgs
/--
Delaborates applications of the form `letFun v (fun x => b)` as `let_fun x := v; b`.

View File

@@ -101,25 +101,15 @@ def fieldNotationCandidate? (f : Expr) (args : Array Expr) (useGeneralizedFieldN
-- It's not handled by any of the above.
return none
/--
Returns the field name of the projection if `e` is an application that is a projection to a parent structure.
If `explicit` is `true`, then requires that the structure have no parameters.
-/
def parentProj? (explicit : Bool) (e : Expr) : MetaM (Option Name) := do
unless e.isApp do return none
try
let .const c .. := e.getAppFn | failure
let (field, numParams, isParentProj) projInfo c
if isParentProj && (!explicit || numParams == 0) && e.getAppNumArgs == numParams + 1 then
return some field
else
return none
catch _ =>
return none
/--
Returns `true` if `e` is an application that is a projection to a parent structure.
If `explicit` is `true`, then requires that the structure have no parameters.
If `explicit` is `true`, then further requires that the structure have no parameters.
-/
def isParentProj (explicit : Bool) (e : Expr) : MetaM Bool := do
return ( parentProj? explicit e).isSome
unless e.isApp do return false
try
let .const c .. := e.getAppFn | failure
let (_, numParams, isParentProj) projInfo c
return isParentProj && (!explicit || numParams == 0) && e.getAppNumArgs == numParams + 1
catch _ =>
return false

View File

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
-/
prelude
import Lean.Attributes
import Lean.ScopedEnvExtension
namespace Lean
@@ -14,159 +13,36 @@ Reducibility status for a definition.
-/
inductive ReducibilityStatus where
| reducible | semireducible | irreducible
deriving Inhabited, Repr, BEq
deriving Inhabited, Repr
def ReducibilityStatus.toAttrString : ReducibilityStatus String
| .reducible => "[reducible]"
| .irreducible => "[irreducible]"
| .semireducible => "[semireducible]"
builtin_initialize reducibilityCoreExt : PersistentEnvExtension (Name × ReducibilityStatus) (Name × ReducibilityStatus) (NameMap ReducibilityStatus)
registerPersistentEnvExtension {
name := `reducibilityCore
mkInitial := pure {}
addImportedFn := fun _ _ => pure {}
addEntryFn := fun (s : NameMap ReducibilityStatus) (p : Name × ReducibilityStatus) => s.insert p.1 p.2
exportEntriesFn := fun m =>
let r : Array (Name × ReducibilityStatus) := m.fold (fun a n p => a.push (n, p)) #[]
r.qsort (fun a b => Name.quickLt a.1 b.1)
statsFn := fun s => "reducibility attribute core extension" ++ Format.line ++ "number of local entries: " ++ format s.size
}
builtin_initialize reducibilityExtraExt : SimpleScopedEnvExtension (Name × ReducibilityStatus) (SMap Name ReducibilityStatus)
registerSimpleScopedEnvExtension {
name := `reducibilityExtra
initial := {}
addEntry := fun d (declName, status) => d.insert declName status
finalizeImport := fun d => d.switch
}
/--
Environment extension for storing the reducibility attribute for definitions.
-/
builtin_initialize reducibilityAttrs : EnumAttributes ReducibilityStatus
registerEnumAttributes
[(`reducible, "reducible", ReducibilityStatus.reducible),
(`semireducible, "semireducible", ReducibilityStatus.semireducible),
(`irreducible, "irreducible", ReducibilityStatus.irreducible)]
@[export lean_get_reducibility_status]
def getReducibilityStatusCore (env : Environment) (declName : Name) : ReducibilityStatus :=
let m := reducibilityExtraExt.getState env
if let some status := m.find? declName then
status
else match env.getModuleIdxFor? declName with
| some modIdx =>
match (reducibilityCoreExt.getModuleEntries env modIdx).binSearch (declName, .semireducible) (fun a b => Name.quickLt a.1 b.1) with
| some (_, status) => status
| none => .semireducible
| none => (reducibilityCoreExt.getState env).find? declName |>.getD .semireducible
private def setReducibilityStatusCore (env : Environment) (declName : Name) (status : ReducibilityStatus) (attrKind : AttributeKind) (currNamespace : Name) : Environment :=
if attrKind matches .global then
match env.getModuleIdxFor? declName with
| some _ =>
-- Trying to set the attribute of a declaration defined in an imported module.
reducibilityExtraExt.addEntry env (declName, status)
| none =>
--
reducibilityCoreExt.addEntry env (declName, status)
else
-- `scoped` and `local` must be handled by `reducibilityExtraExt`
reducibilityExtraExt.addCore env (declName, status) attrKind currNamespace
private def getReducibilityStatusImp (env : Environment) (declName : Name) : ReducibilityStatus :=
match reducibilityAttrs.getValue env declName with
| some s => s
| none => ReducibilityStatus.semireducible
@[export lean_set_reducibility_status]
private def setReducibilityStatusImp (env : Environment) (declName : Name) (status : ReducibilityStatus) : Environment :=
setReducibilityStatusCore env declName status .global .anonymous
/-
TODO: it would be great if we could distinguish between the following two situations
1-
```
@[reducible] def foo := ...
```
2-
```
def foo := ...
...
attribute [reducible] foo
```
Reason: the second one is problematic if user has add simp theorems or TC instances that include `foo`.
Recall that the discrimination trees unfold `[reducible]` declarations while indexing new entries.
-/
register_builtin_option allowUnsafeReducibility : Bool := {
defValue := false
descr := "enables users to modify the reducibility settings for declarations even when such changes are deemed potentially hazardous. For example, `simp` and type class resolution maintain term indices where reducible declarations are expanded."
}
private def validate (declName : Name) (status : ReducibilityStatus) (attrKind : AttributeKind) : CoreM Unit := do
let suffix := "use `set_option allowUnsafeReducibility true` to override reducibility status validation"
unless allowUnsafeReducibility.get ( getOptions) do
match ( getConstInfo declName) with
| .defnInfo _ =>
let statusOld := getReducibilityStatusCore ( getEnv) declName
match attrKind with
| .scoped =>
throwError "failed to set reducibility status for `{declName}`, the `scoped` modifier is not recommended for this kind of attribute\n{suffix}"
| .global =>
if ( getEnv).getModuleIdxFor? declName matches some _ then
throwError "failed to set reducibility status, `{declName}` has not been defined in this file, consider using the `local` modifier\n{suffix}"
match status with
| .reducible =>
unless statusOld matches .semireducible do
throwError "failed to set `[reducible]`, `{declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`\n{suffix}"
| .irreducible =>
unless statusOld matches .semireducible do
throwError "failed to set `[irreducible]`, `{declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`\n{suffix}"
| .semireducible =>
throwError "failed to set `[semireducible]` for `{declName}`, declarations are `[semireducible]` by default\n{suffix}"
| .local =>
match status with
| .reducible =>
throwError "failed to set `[local reducible]` for `{declName}`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution\n{suffix}"
| .irreducible =>
unless statusOld matches .semireducible do
throwError "failed to set `[local irreducible]`, `{declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected\n{suffix}"
| .semireducible =>
unless statusOld matches .irreducible do
throwError "failed to set `[local semireducible]`, `{declName}` is currently `{statusOld.toAttrString}`, `[irreducible]` expected\n{suffix}"
| _ => throwError "failed to set reducibility status, `{declName}` is not a definition\n{suffix}"
private def addAttr (status : ReducibilityStatus) (declName : Name) (stx : Syntax) (attrKind : AttributeKind) : AttrM Unit := do
Attribute.Builtin.ensureNoArgs stx
validate declName status attrKind
let ns getCurrNamespace
modifyEnv fun env => setReducibilityStatusCore env declName status attrKind ns
builtin_initialize
registerBuiltinAttribute {
ref := by exact decl_name%
name := `irreducible
descr := "irreducible declaration"
add := addAttr .irreducible
applicationTime := .afterTypeChecking
}
builtin_initialize
registerBuiltinAttribute {
ref := by exact decl_name%
name := `reducible
descr := "reducible declaration"
add := addAttr .reducible
applicationTime := .afterTypeChecking
}
builtin_initialize
registerBuiltinAttribute {
ref := by exact decl_name%
name := `semireducible
descr := "semireducible declaration"
add := addAttr .semireducible
applicationTime := .afterTypeChecking
}
private def setReducibilityStatusImp (env : Environment) (declName : Name) (s : ReducibilityStatus) : Environment :=
match reducibilityAttrs.setValue env declName s with
| Except.ok env => env
| _ => env -- TODO(Leo): we should extend EnumAttributes.setValue in the future and ensure it never fails
/-- Return the reducibility attribute for the given declaration. -/
def getReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) : m ReducibilityStatus := do
return getReducibilityStatusCore ( getEnv) declName
return getReducibilityStatusImp ( getEnv) declName
/-- Set the reducibility attribute for the given declaration. -/
def setReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit := do
modifyEnv fun env => setReducibilityStatusCore env declName s .global .anonymous
modifyEnv fun env => setReducibilityStatusImp env declName s
/-- Set the given declaration as `[reducible]` -/
def setReducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := do
@@ -175,13 +51,13 @@ def setReducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := d
/-- Return `true` if the given declaration has been marked as `[reducible]`. -/
def isReducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
match ( getReducibilityStatus declName) with
| .reducible => return true
| ReducibilityStatus.reducible => return true
| _ => return false
/-- Return `true` if the given declaration has been marked as `[irreducible]` -/
def isIrreducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
match ( getReducibilityStatus declName) with
| .irreducible => return true
| ReducibilityStatus.irreducible => return true
| _ => return false
end Lean

View File

@@ -146,15 +146,11 @@ def ScopedEnvExtension.addLocalEntry (ext : ScopedEnvExtension α β σ) (env :
let top := { top with state := ext.descr.addEntry top.state b }
ext.ext.setState env { s with stateStack := top :: states }
def ScopedEnvExtension.addCore (env : Environment) (ext : ScopedEnvExtension α β σ) (b : β) (kind : AttributeKind) (namespaceName : Name) : Environment :=
match kind with
| AttributeKind.global => ext.addEntry env b
| AttributeKind.local => ext.addLocalEntry env b
| AttributeKind.scoped => ext.addScopedEntry env namespaceName b
def ScopedEnvExtension.add [Monad m] [MonadResolveName m] [MonadEnv m] (ext : ScopedEnvExtension α β σ) (b : β) (kind := AttributeKind.global) : m Unit := do
let ns getCurrNamespace
modifyEnv (ext.addCore · b kind ns)
match kind with
| AttributeKind.global => modifyEnv (ext.addEntry · b)
| AttributeKind.local => modifyEnv (ext.addLocalEntry · b)
| AttributeKind.scoped => modifyEnv (ext.addScopedEntry · ( getCurrNamespace) b)
def ScopedEnvExtension.getState [Inhabited σ] (ext : ScopedEnvExtension α β σ) (env : Environment) : σ :=
match ext.ext.getState env |>.stateStack with

View File

@@ -54,24 +54,24 @@ def push (p : Pos) (c : Nat) : Pos :=
variable {α : Type} [Inhabited α]
/-- Fold over the position starting at the root and heading to the leaf-/
partial def foldl (f : α Nat α) (init : α) (p : Pos) : α :=
if p.isRoot then init else f (foldl f init p.tail) p.head
partial def foldl (f : α Nat α) (a : α) (p : Pos) : α :=
if p.isRoot then a else f (foldl f a p.tail) p.head
/-- Fold over the position starting at the leaf and heading to the root-/
partial def foldr (f : Nat α α) (p : Pos) (init : α) : α :=
if p.isRoot then init else foldr f p.tail (f p.head init)
partial def foldr (f : Nat α α) (p : Pos) (a : α) : α :=
if p.isRoot then a else foldr f p.tail (f p.head a)
/-- monad-fold over the position starting at the root and heading to the leaf -/
partial def foldlM [Monad M] (f : α Nat M α) (init : α) (p : Pos) : M α :=
partial def foldlM [Monad M] (f : α Nat M α) (a : α) (p : Pos) : M α :=
have : Inhabited (M α) := inferInstance
if p.isRoot then pure init else do foldlM f init p.tail >>= (f · p.head)
if p.isRoot then pure a else do foldlM f a p.tail >>= (f · p.head)
/-- monad-fold over the position starting at the leaf and finishing at the root. -/
partial def foldrM [Monad M] (f : Nat α M α) (p : Pos) (init : α) : M α :=
if p.isRoot then pure init else f p.head init >>= foldrM f p.tail
partial def foldrM [Monad M] (f : Nat α M α) (p : Pos) (a : α) : M α :=
if p.isRoot then pure a else f p.head a >>= foldrM f p.tail
def depth (p : Pos) :=
p.foldr (init := 0) fun _ => Nat.succ
p.foldr (fun _ => Nat.succ) 0
/-- Returns true if `pred` is true for each coordinate in `p`.-/
def all (pred : Nat Bool) (p : Pos) : Bool :=
@@ -98,7 +98,6 @@ def pushLetBody (p : Pos) := p.push 2
def pushAppFn (p : Pos) := p.push 0
def pushAppArg (p : Pos) := p.push 1
def pushProj (p : Pos) := p.push 0
def pushType (p : Pos) := p.push Pos.typeCoord
def pushNaryFn (numArgs : Nat) (p : Pos) : Pos :=
p.asNat * (maxChildren ^ numArgs)
@@ -135,8 +134,8 @@ protected def fromString? : String → Except String Pos
protected def fromString! (s : String) : Pos :=
match Pos.fromString? s with
| .ok a => a
| .error e => panic! e
| Except.ok a => a
| Except.error e => panic! e
instance : Ord Pos := show Ord Nat by infer_instance
instance : DecidableEq Pos := show DecidableEq Nat by infer_instance
@@ -214,7 +213,7 @@ open SubExpr in
`SubExpr.Pos` argument for tracking subexpression position. -/
def Expr.traverseAppWithPos {M} [Monad M] (visit : Pos Expr M Expr) (p : Pos) (e : Expr) : M Expr :=
match e with
| .app f a =>
| Expr.app f a =>
e.updateApp!
<$> traverseAppWithPos visit p.pushAppFn f
<*> visit p.pushAppArg a

View File

@@ -172,12 +172,6 @@ instance : ToExpr FVarId where
toTypeExpr := mkConst ``FVarId
toExpr fvarId := mkApp (mkConst ``FVarId.mk) (toExpr fvarId.name)
instance : ToExpr Syntax.Preresolved where
toTypeExpr := .const ``Syntax.Preresolved []
toExpr
| .namespace ns => mkApp (.const ``Syntax.Preresolved.namespace []) (toExpr ns)
| .decl a ls => mkApp2 (.const ``Syntax.Preresolved.decl []) (toExpr a) (toExpr ls)
def Expr.toCtorIfLit : Expr Expr
| .lit (.natVal v) =>
if v == 0 then mkConst ``Nat.zero

View File

@@ -58,7 +58,7 @@ def checked (e : Expr) : ForEachM m Bool := do
return false
/-- `Expr.forEachWhere` (unsafe) implementation -/
unsafe def visit (p : Expr Bool) (f : Expr m Unit) (e : Expr) (stopWhenVisited : Bool := false) : m Unit := do
unsafe def visit (p : Expr Bool) (f : Expr m Unit) (e : Expr) : m Unit := do
go e |>.run' initCache
where
go (e : Expr) : StateRefT' ω State m Unit := do
@@ -66,8 +66,6 @@ where
if p e then
unless ( checked e) do
f e
if stopWhenVisited then
return ()
match e with
| .forallE _ d b _ => go d; go b
| .lam _ d b _ => go d; go b
@@ -80,11 +78,9 @@ where
end ForEachExprWhere
/--
`e.forEachWhere p f` applies `f` to each subterm that satisfies `p`.
If `stopWhenVisited` is `true`, the function doesn't visit subterms of terms
which satisfy `p`.
`e.forEachWhere p f` applies `f` to each subterm that satisfies `p`.
-/
@[implemented_by ForEachExprWhere.visit]
opaque Expr.forEachWhere {ω : Type} {m : Type Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (p : Expr Bool) (f : Expr m Unit) (e : Expr) (stopWhenVisited : Bool := false) : m Unit
opaque Expr.forEachWhere {ω : Type} {m : Type Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (p : Expr Bool) (f : Expr m Unit) (e : Expr) : m Unit
end Lean

Some files were not shown because too many files have changed in this diff Show More