Compare commits

..

2 Commits

Author SHA1 Message Date
Leonardo de Moura
9a65c5a43b feat: compute number of anchor digits 2025-10-16 16:29:19 -07:00
Leonardo de Moura
a7ca25ab0a refactor: move truncateAnchors 2025-10-16 16:10:59 -07:00
1669 changed files with 4334 additions and 7905 deletions

View File

@@ -16,26 +16,14 @@ These comments explain the scripts' behavior, which repositories get special han
## Process
1. Run `script/release_checklist.py {version}` to check the current status
2. **CRITICAL: If preliminary lean4 checks fail, STOP immediately and alert the user**
- Check for: release branch exists, CMake version correct, tag exists, release page exists, release notes exist
- **IMPORTANT**: The release page is created AUTOMATICALLY by CI after pushing the tag - DO NOT create it manually
- Do NOT create any PRs or proceed with repository updates if these checks fail
3. Create a todo list tracking all repositories that need updates
4. **CRITICAL RULE: You can ONLY run `release_steps.py` for a repository if `release_checklist.py` explicitly says to do so**
- The checklist output will say "Run `script/release_steps.py {version} {repo_name}` to create it"
- If a repository shows "🟡 Dependencies not ready", you CANNOT create a PR for it yet
- You MUST rerun `release_checklist.py` before attempting to create PRs for any new repositories
5. For each repository that the checklist says needs updating:
2. Create a todo list tracking all repositories that need updates
3. For each repository that needs updating:
- Run `script/release_steps.py {version} {repo_name}` to create the PR
- Mark it complete when the PR is created
6. After creating PRs, notify the user which PRs need review and merging
7. **MANDATORY: Rerun `release_checklist.py` to check current status**
- Do this after creating each batch of PRs
- Do this after the user reports PRs have been merged
- NEVER assume a repository is ready without checking the checklist output
8. As PRs are merged and tagged, dependent repositories will become ready
9. Continue the cycle: run checklist → create PRs for ready repos → wait for merges → repeat
10. Continue until all repositories are updated and the release is complete
4. After creating PRs, notify the user which PRs need review and merging
5. Continuously rerun `script/release_checklist.py {version}` to check progress
6. As PRs are merged, dependent repositories will become ready - create PRs for those as well
7. Continue until all repositories are updated and the release is complete
## Important Notes

View File

@@ -11,8 +11,8 @@ jobs:
- uses: actions/checkout@v5
with:
ref: ${{ github.event.pull_request.head.sha }}
filter: blob:none
fetch-depth: 0
filter: tree:0
- name: Find base commit
if: github.event_name == 'pull_request'

View File

@@ -116,7 +116,6 @@ jobs:
# rerun the workflow run after setting the `release-ci`/`merge-ci` labels.
run: |
check_level=0
fast=false
if [[ -n "${{ steps.set-nightly.outputs.nightly }}" || -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
check_level=2
@@ -129,13 +128,9 @@ jobs:
elif echo "$labels" | grep -q "merge-ci"; then
check_level=1
fi
if echo "$labels" | grep -q "fast-ci"; then
fast=true
fi
fi
echo "check-level=$check_level" >> "$GITHUB_OUTPUT"
echo "fast=$fast" >> "$GITHUB_OUTPUT"
env:
GH_TOKEN: ${{ github.token }}
@@ -145,8 +140,7 @@ jobs:
with:
script: |
const level = ${{ steps.set-level.outputs.check-level }};
const fast = ${{ steps.set-level.outputs.fast }};
console.log(`level: ${level}, fast: ${fast}`);
console.log(`level: ${level}`);
// use large runners where available (original repo)
let large = ${{ github.repository == 'leanprover/lean4' }};
const isPr = "${{ github.event_name }}" == "pull_request";
@@ -171,8 +165,7 @@ jobs:
{
// portable release build: use channel with older glibc (2.26)
"name": "Linux release",
// usually not a bottleneck so make exclusive to `fast-ci`
"os": large && fast ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
"os": "ubuntu-latest",
"release": true,
// Special handling for release jobs. We want:
// 1. To run it in PRs so developers get PR toolchains (so secondary without tests is sufficient)
@@ -237,9 +230,10 @@ jobs:
{
"name": "macOS aarch64",
// standard GH runner only comes with 7GB so use large runner if possible when running tests
"os": large && (fast || level >= 1) ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
"os": large && level >= 1 ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
"CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
"release": true,
"test": true,
"shell": "bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-apple-darwin.tar.zst",
"prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
@@ -247,12 +241,11 @@ jobs:
"tar": "gtar", // https://github.com/actions/runner-images/issues/2619
// See "Linux release" for release job levels; Grove is not a concern here
"enabled": isPr || level != 1,
"test": level >= 1,
"secondary": level == 0,
},
{
"name": "Windows",
"os": large && (fast || level == 2) ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
"os": large && level == 2 ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
"release": true,
"enabled": level >= 2,
"test": true,
@@ -404,8 +397,6 @@ jobs:
with:
# needed for tagging
fetch-depth: 0
# Doesn't seem to be working when additionally fetching from lean4-nightly
#filter: tree:0
token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
- uses: actions/download-artifact@v5
with:

View File

@@ -48,17 +48,17 @@ jobs:
git -C lean4.git remote add origin https://github.com/${{ github.repository_owner }}/lean4.git
git -C lean4.git fetch -n origin master
git -C lean4.git fetch -n origin "${{ steps.workflow-info.outputs.sourceHeadSha }}"
# Create both the original tag and the SHA-suffixed tag
SHORT_SHA="${{ steps.workflow-info.outputs.sourceHeadSha }}"
SHORT_SHA="${SHORT_SHA:0:7}"
# Export the short SHA for use in subsequent steps
echo "SHORT_SHA=${SHORT_SHA}" >> "$GITHUB_ENV"
git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} "${{ steps.workflow-info.outputs.sourceHeadSha }}"
git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}" "${{ steps.workflow-info.outputs.sourceHeadSha }}"
git -C lean4.git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git
git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}"
@@ -200,7 +200,7 @@ jobs:
-H "Accept: application/vnd.github.v3+json" \
"https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
| jq -r '.[].name')"
if echo "$LABELS" | grep -q "^force-mathlib-ci$"; then
echo "force-mathlib-ci label detected, forcing CI despite issues"
MESSAGE="Forcing Mathlib CI because the \`force-mathlib-ci\` label is present, despite problem: $MESSAGE"
@@ -301,7 +301,7 @@ jobs:
-H "Accept: application/vnd.github.v3+json" \
"https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
| jq -r '.[].name')"
if echo "$LABELS" | grep -q "^force-manual-ci$"; then
echo "force-manual-ci label detected, forcing CI despite issues"
MESSAGE="Forcing reference manual CI because the \`force-manual-ci\` label is present, despite problem: $MESSAGE"
@@ -401,7 +401,6 @@ jobs:
token: ${{ secrets.MATHLIB4_BOT }}
ref: nightly-testing
fetch-depth: 0 # This ensures we check out all tags and branches.
filter: tree:0
- name: Check if tag exists
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
@@ -461,7 +460,6 @@ jobs:
token: ${{ secrets.MATHLIB4_BOT }}
ref: nightly-testing
fetch-depth: 0 # This ensures we check out all tags and branches.
filter: tree:0
- name: install elan
run: |
@@ -532,7 +530,6 @@ jobs:
token: ${{ secrets.MANUAL_PR_BOT }}
ref: nightly-testing
fetch-depth: 0 # This ensures we check out all tags and branches.
filter: tree:0
- name: Check if tag in reference manual exists
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'

View File

@@ -52,7 +52,7 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
Similarly, the signed integer types `Int8`, ..., `Int64`, `ISize` are also represented by the unsigned C types `uint8_t`, ..., `uint64_t`, `size_t`, respectively, because they have a trivial structure.
* `Nat` and `Int` are represented by `lean_object *`.
Their runtime values 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 or integer (`lean_box`/`lean_unbox`).
* A universe `Sort u`, type constructor `... → Sort u`, `Void α` 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)`
* 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.
@@ -141,8 +141,8 @@ void lean_initialize_runtime_module();
void lean_initialize();
char ** lean_setup_args(int argc, char ** argv);
lean_object * initialize_A_B(uint8_t builtin);
lean_object * initialize_C(uint8_t builtin);
lean_object * initialize_A_B(uint8_t builtin, lean_object *);
lean_object * initialize_C(uint8_t builtin, lean_object *);
...
argv = lean_setup_args(argc, argv); // if using process-related functionality
@@ -152,7 +152,7 @@ lean_initialize_runtime_module();
lean_object * res;
// use same default as for Lean executables
uint8_t builtin = 1;
res = initialize_A_B(builtin);
res = initialize_A_B(builtin, lean_io_mk_world());
if (lean_io_result_is_ok(res)) {
lean_dec_ref(res);
} else {
@@ -160,7 +160,7 @@ if (lean_io_result_is_ok(res)) {
lean_dec(res);
return ...; // do not access Lean declarations if initialization failed
}
res = initialize_C(builtin);
res = initialize_C(builtin, lean_io_mk_world());
if (lean_io_result_is_ok(res)) {
...

View File

@@ -57,19 +57,19 @@ def main (args : List String) : IO Unit := do
sec := "\n\n" ++ sec
if insertPos?.isNone then
sec := sec ++ "\n\n"
text := text.extract 0 insertPos ++ sec ++ text.extract insertPos text.rawEndPos
text := text.extract 0 insertPos ++ sec ++ text.extract insertPos text.endPos
-- prepend each import with `public `
for imp in imps.reverse do
let insertPos := imp.raw.getPos?.get!
let prfx := if doMeta then "public meta " else "public "
text := text.extract 0 insertPos ++ prfx ++ text.extract insertPos text.rawEndPos
text := text.extract 0 insertPos ++ prfx ++ text.extract insertPos text.endPos
-- insert `module` header
let mut initText := text.extract 0 startPos
if !initText.trim.isEmpty then
-- If there is a header comment, preserve it and put `module` in the line after
initText := initText.trimRight ++ "\n"
text := initText ++ "module\n\n" ++ text.extract startPos text.rawEndPos
text := initText ++ "module\n\n" ++ text.extract startPos text.endPos
IO.FS.writeFile path text

View File

@@ -563,14 +563,14 @@ def main (args : List String) : IO UInt32 := do
if remove.contains mod || seen.contains mod then
out := out ++ text.extract pos stx.raw.getPos?.get!
-- We use the end position of the syntax, but include whitespace up to the first newline
pos := text.findAux (· == '\n') text.rawEndPos stx.raw.getTailPos?.get! + 1
pos := text.findAux (· == '\n') text.endPos stx.raw.getTailPos?.get! + 1
seen := seen.insert mod
out := out ++ text.extract pos insertion
for mod in add do
if !seen.contains mod then
seen := seen.insert mod
out := out ++ s!"{mod}\n"
out := out ++ text.extract insertion text.rawEndPos
out := out ++ text.extract insertion text.endPos
IO.FS.writeFile path out
return count + 1

View File

@@ -13,15 +13,8 @@ What this script does:
- Checks that the release branch (releases/vX.Y.0) exists
- Verifies CMake version settings are correct
- Confirms the release tag exists
- Validates the release page exists on GitHub (created automatically by CI after tag push)
- Checks the release notes page on lean-lang.org (updated while bumping the `reference-manual` repository)
**IMPORTANT: If the release page doesn't exist, the script will skip checking
downstream repositories and the master branch configuration. The preliminary
infrastructure must be in place before the release process can proceed.**
**NOTE: The GitHub release page is created AUTOMATICALLY by CI after the tag is pushed.
DO NOT create it manually. Wait for CI to complete after pushing the tag.**
- Validates the release page exists on GitHub
- Checks the release notes page on lean-lang.org
2. For each downstream repository (batteries, mathlib4, etc.):
- Checks if dependencies are ready (e.g., mathlib4 depends on batteries)
@@ -129,39 +122,6 @@ def release_page_exists(repo_url, tag_name, github_token):
response = requests.get(api_url, headers=headers)
return response.status_code == 200
def get_tag_workflow_status(repo_url, tag_name, github_token):
"""Get the status of CI workflows running for a specific tag."""
api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/")
headers = {'Authorization': f'token {github_token}'} if github_token else {}
# Get workflow runs for the tag
# GitHub's workflow runs API uses the branch/tag name in the 'head_branch' field
api_url = f"{api_base}/actions/runs?event=push&head_branch={tag_name}"
response = requests.get(api_url, headers=headers)
if response.status_code != 200:
return None
data = response.json()
workflow_runs = data.get('workflow_runs', [])
if not workflow_runs:
return None
# Get the most recent workflow run for this tag
run = workflow_runs[0]
status = run.get('status')
conclusion = run.get('conclusion')
workflow_name = run.get('name', 'CI')
run_id = run.get('id')
return {
'status': status,
'conclusion': conclusion,
'workflow_name': workflow_name,
'run_id': run_id
}
def get_release_notes(tag_name):
"""Fetch release notes page title from lean-lang.org."""
# Strip -rcX suffix if present for the URL
@@ -170,17 +130,20 @@ def get_release_notes(tag_name):
try:
response = requests.get(reference_url)
response.raise_for_status() # Raise HTTPError for bad responses (4xx or 5xx)
# Extract title using regex
match = re.search(r"<title>(.*?)</title>", response.text, re.IGNORECASE | re.DOTALL)
if match:
return match.group(1).strip()
else:
print(f" ⚠️ Could not find <title> tag in {reference_url}")
return None
except requests.exceptions.RequestException:
except requests.exceptions.RequestException as e:
print(f" ❌ Error fetching release notes from {reference_url}: {e}")
return None
except Exception:
except Exception as e:
print(f" ❌ An unexpected error occurred while processing release notes: {e}")
return None
def get_branch_content(repo_url, branch, file_path, github_token):
@@ -549,57 +512,30 @@ def main():
print(f" ❌ Short commit hash {commit_hash[:SHORT_HASH_LENGTH]} is numeric and starts with 0, causing issues for version parsing. Try regenerating the last commit to get a new hash.")
lean4_success = False
release_page_ready = release_page_exists(lean_repo_url, toolchain, github_token)
if not release_page_ready:
print(f" ❌ Release page for {toolchain} does not exist (This will be created by CI.)")
# Check CI workflow status
workflow_status = get_tag_workflow_status(lean_repo_url, toolchain, github_token)
if workflow_status:
status = workflow_status['status']
conclusion = workflow_status['conclusion']
workflow_name = workflow_status['workflow_name']
run_id = workflow_status['run_id']
workflow_url = f"{lean_repo_url}/actions/runs/{run_id}"
if status == 'in_progress' or status == 'queued':
print(f" 🔄 {workflow_name} workflow is {status}: {workflow_url}")
elif status == 'completed':
if conclusion == 'success':
print(f"{workflow_name} workflow completed successfully: {workflow_url}")
elif conclusion == 'failure':
print(f"{workflow_name} workflow failed: {workflow_url}")
else:
print(f" ⚠️ {workflow_name} workflow completed with status: {conclusion}: {workflow_url}")
else:
print(f" {workflow_name} workflow status: {status}: {workflow_url}")
if not release_page_exists(lean_repo_url, toolchain, github_token):
print(f" ❌ Release page for {toolchain} does not exist")
lean4_success = False
else:
print(f" ✅ Release page for {toolchain} exists")
# Check the actual release notes page title (informational only - does not block)
# Check the actual release notes page title
actual_title = get_release_notes(toolchain)
expected_title_prefix = f"Lean {toolchain.lstrip('v')}" # e.g., "Lean 4.19.0" or "Lean 4.19.0-rc1"
base_tag = toolchain.split('-')[0]
release_notes_url = f"https://lean-lang.org/doc/reference/latest/releases/{base_tag}/"
if actual_title is None:
print(f" ⚠️ Release notes not found at {release_notes_url} (this will be fixed while updating the reference-manual repository)")
# Error already printed by get_release_notes
lean4_success = False
elif not actual_title.startswith(expected_title_prefix):
print(f" ⚠️ Release notes page title mismatch. Expected prefix '{expected_title_prefix}', got '{actual_title}'. Check {release_notes_url}")
# Construct URL for the error message (using the base tag)
base_tag = toolchain.split('-')[0]
check_url = f"https://lean-lang.org/doc/reference/latest/releases/{base_tag}/"
print(f" ❌ Release notes page title mismatch. Expected prefix '{expected_title_prefix}', got '{actual_title}'. Check {check_url}")
lean4_success = False
else:
print(f" ✅ Release notes page title looks good ('{actual_title}').")
repo_status["lean4"] = lean4_success
# If the release page doesn't exist, skip repository checks and master branch checks
# The preliminary infrastructure must be in place first
if not release_page_exists(lean_repo_url, toolchain, github_token):
print("\n⚠️ Release process blocked: preliminary Lean4 infrastructure incomplete.")
print(" Complete the steps above, then rerun this script to proceed with downstream repositories.")
return
# Load repositories and perform further checks
print("\nChecking repositories...")

View File

@@ -589,19 +589,8 @@ def execute_release_steps(repo, version, config):
# Clean lake cache for a fresh build
print(blue("Cleaning lake cache..."))
run_command("lake clean", cwd=repo_path)
# Check if downstream of Mathlib and get cache if so
mathlib_package_dir = repo_path / ".lake" / "packages" / "mathlib"
if mathlib_package_dir.exists():
print(blue("Project is downstream of Mathlib, fetching cache..."))
try:
run_command("lake exe cache get", cwd=repo_path, stream_output=True)
print(green("Cache fetched successfully"))
except subprocess.CalledProcessError as e:
print(yellow("Failed to fetch cache, continuing anyway..."))
print(yellow(f"Cache fetch error: {e}"))
run_command("rm -rf .lake", cwd=repo_path)
try:
run_command("lake build", cwd=repo_path, stream_output=True)
print(green("Build completed successfully"))

View File

@@ -10,7 +10,7 @@ endif()
include(ExternalProject)
project(LEAN CXX C)
set(LEAN_VERSION_MAJOR 4)
set(LEAN_VERSION_MINOR 26)
set(LEAN_VERSION_MINOR 25)
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'")

View File

@@ -27,7 +27,7 @@ failure occurred.
/--
Executes an action that might fail in the underlying monad `m`, returning `none` in case of failure.
-/
@[always_inline, inline, expose]
@[always_inline, inline]
def OptionT.run {m : Type u Type v} {α : Type u} (x : OptionT m α) : m (Option α) :=
x
@@ -69,7 +69,7 @@ instance {m : Type u → Type v} [Pure m] : Inhabited (OptionT m α) where
/--
Recovers from failures. Typically used via the `<|>` operator.
-/
@[always_inline, inline, expose] protected def orElse (x : OptionT m α) (y : Unit OptionT m α) : OptionT m α := OptionT.mk do
@[always_inline, inline] protected def orElse (x : OptionT m α) (y : Unit OptionT m α) : OptionT m α := OptionT.mk do
match ( x) with
| some a => pure (some a)
| _ => y ()
@@ -77,7 +77,7 @@ Recovers from failures. Typically used via the `<|>` operator.
/--
A recoverable failure.
-/
@[always_inline, inline, expose] protected def fail : OptionT m α := OptionT.mk do
@[always_inline, inline] protected def fail : OptionT m α := OptionT.mk do
pure none
instance : Alternative (OptionT m) where
@@ -90,7 +90,7 @@ Converts a computation from the underlying monad into one that could fail, even
This function is typically implicitly accessed via a `MonadLiftT` instance as part of [automatic
lifting](lean-manual://section/monad-lifting).
-/
@[always_inline, inline, expose] protected def lift (x : m α) : OptionT m α := OptionT.mk do
@[always_inline, inline] protected def lift (x : m α) : OptionT m α := OptionT.mk do
return some ( x)
instance : MonadLift m (OptionT m) := OptionT.lift
@@ -100,11 +100,11 @@ instance : MonadFunctor m (OptionT m) := ⟨fun f x => f x⟩
/--
Handles failures by treating them as exceptions of type `Unit`.
-/
@[always_inline, inline, expose] protected def tryCatch (x : OptionT m α) (handle : PUnit OptionT m α) : OptionT m α := OptionT.mk do
let some a x | handle
@[always_inline, inline] protected def tryCatch (x : OptionT m α) (handle : Unit OptionT m α) : OptionT m α := OptionT.mk do
let some a x | handle ()
pure <| some a
instance : MonadExceptOf PUnit (OptionT m) where
instance : MonadExceptOf Unit (OptionT m) where
throw := fun _ => OptionT.fail
tryCatch := OptionT.tryCatch

View File

@@ -256,19 +256,3 @@ theorem ByteArray.copySlice_eq_append {src : ByteArray} {srcOff : Nat} {dest : B
dest.extract 0 destOff ++ src.extract srcOff (srcOff +len) ++ dest.extract (destOff + min len (src.data.size - srcOff)) dest.data.size := by
ext1
simp [copySlice]
@[simp]
theorem ByteArray.data_set {as : ByteArray} {i : Nat} {h : i < as.size} {a : UInt8} :
(as.set i a h).data = as.data.set i a (by simpa) := by
simp [set]
theorem ByteArray.set_eq_push_extract_append_extract {as : ByteArray} {i : Nat} (h : i < as.size) {a : UInt8} :
as.set i a h = (as.extract 0 i).push a ++ as.extract (i + 1) as.size := by
ext1
simpa using Array.set_eq_push_extract_append_extract _
@[simp]
theorem ByteArray.append_toByteArray_singleton {as : ByteArray} {a : UInt8} :
as ++ [a].toByteArray = as.push a := by
ext1
simp

View File

@@ -170,7 +170,7 @@ private def spaceUptoLine : Format → Bool → Int → Nat → SpaceResult
| text s, flatten, _, _ =>
let p := String.Internal.posOf s '\n'
let off := String.Internal.offsetOfPos s p
{ foundLine := p != s.rawEndPos, foundFlattenedHardLine := flatten && p != s.rawEndPos, space := off }
{ foundLine := p != s.endPos, foundFlattenedHardLine := flatten && p != s.endPos, space := off }
| append f₁ f₂, flatten, m, w => merge w (spaceUptoLine f₁ flatten m w) (spaceUptoLine f₂ flatten m)
| nest n f, flatten, m, w => spaceUptoLine f flatten (m - n) w
| group f _, _, m, w => spaceUptoLine f true m w
@@ -264,14 +264,14 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
| nest n f => be w (gs' ({ i with f, indent := i.indent + n }::is))
| text s =>
let p := String.Internal.posOf s '\n'
if p == s.rawEndPos then
if p == s.endPos then
pushOutput s
endTags i.activeTags
be w (gs' is)
else
pushOutput (String.Internal.extract s {} p)
pushNewline i.indent.toNat
let is := { i with f := text (String.Internal.extract s (String.Internal.next s p) s.rawEndPos) }::is
let is := { i with f := text (String.Internal.extract s (String.Internal.next s p) s.endPos) }::is
-- after a hard line break, re-evaluate whether to flatten the remaining group
-- note that we shouldn't start flattening after a hard break outside a group
if g.fla == .disallow then
@@ -411,6 +411,7 @@ Renders a `Format` to a string.
* `column`: begin the first line wrap `column` characters earlier than usual
(this is useful when the output String will be printed starting at `column`)
-/
@[export lean_format_pretty]
def pretty (f : Format) (width : Nat := defWidth) (indent : Nat := 0) (column := 0) : String :=
let act : StateM State Unit := prettyM f width indent
State.out <| act (State.mk "" column) |>.snd

View File

@@ -313,7 +313,7 @@ the logical model.
Examples:
* `(7 : Int).natAbs = 7`
* `(0 : Int).natAbs = 0`
* `(-11 : Int).natAbs = 11`
* `((-11 : Int).natAbs = 11`
-/
@[extern "lean_nat_abs", expose]
def natAbs (m : @& Int) : Nat :=

View File

@@ -241,16 +241,6 @@ def IterStep.successor : IterStep α β → Option α
| .skip it => some it
| .done => none
@[simp]
theorem IterStep.successor_yield {it : α} {out : β} :
(IterStep.yield it out).successor = some it := rfl
@[simp]
theorem IterStep.successor_skip {it : α} : (IterStep.skip (β := β) it).successor = some it := rfl
@[simp]
theorem IterStep.successor_done : (IterStep.done (α := α) (β := β)).successor = none := rfl
/--
If present, applies `f` to the iterator of an `IterStep` and replaces the iterator
with the result of the application of `f`.
@@ -553,10 +543,6 @@ def Iter.IsPlausibleSuccessorOf {α : Type w} {β : Type w} [Iterator α Id β]
(it' it : Iter (α := α) β) : Prop :=
it'.toIterM.IsPlausibleSuccessorOf it.toIterM
theorem Iter.isPlausibleSuccessorOf_eq_invImage {α : Type w} {β : Type w} [Iterator α Id β] :
IsPlausibleSuccessorOf (α := α) (β := β) =
InvImage (IterM.IsPlausibleSuccessorOf (α := α) (β := β) (m := Id)) Iter.toIterM := rfl
theorem Iter.isPlausibleSuccessorOf_iff_exists {α : Type w} {β : Type w} [Iterator α Id β]
{it' it : Iter (α := α) β} :
it'.IsPlausibleSuccessorOf it step, step.successor = some it' it.IsPlausibleStep step := by
@@ -569,16 +555,6 @@ theorem Iter.isPlausibleSuccessorOf_iff_exists {α : Type w} {β : Type w} [Iter
exact step.mapIterator Iter.toIterM,
by cases step <;> simp_all [IterStep.successor, Iter.IsPlausibleStep]
theorem Iter.IsPlausibleStep.isPlausibleSuccessor_of_yield {α : Type w} {β : Type w}
[Iterator α Id β] {it' it : Iter (α := α) β} {out : β}
(h : it.IsPlausibleStep (.yield it' out)) : it'.IsPlausibleSuccessorOf it := by
simpa [isPlausibleSuccessorOf_iff_exists] using .yield it' out, by simp [h]
theorem Iter.IsPlausibleStep.isPlausibleSuccessor_of_skip {α : Type w} {β : Type w}
[Iterator α Id β] {it' it : Iter (α := α) β} (h : it.IsPlausibleStep (.skip it')) :
it'.IsPlausibleSuccessorOf it := by
simpa [isPlausibleSuccessorOf_iff_exists] using .skip it', by simp [h]
/--
Asserts that a certain iterator `it` could plausibly yield the value `out` after an arbitrary
number of steps.
@@ -680,10 +656,6 @@ Given this typeclass, termination proofs for well-founded recursion over an iter
class Finite (α : Type w) (m : Type w Type w') {β : Type w} [Iterator α m β] : Prop where
wf : WellFounded (IterM.IsPlausibleSuccessorOf (α := α) (m := m))
theorem Finite.wf_of_id {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] :
WellFounded (Iter.IsPlausibleSuccessorOf (α := α)) := by
simpa [Iter.isPlausibleSuccessorOf_eq_invImage] using InvImage.wf _ Finite.wf
/--
This type is a wrapper around `IterM` so that it becomes a useful termination measure for
recursion over finite iterators. See also `IterM.finitelyManySteps` and `Iter.finitelyManySteps`.
@@ -733,12 +705,6 @@ theorem IterM.TerminationMeasures.Finite.rel_of_skip
Rel it' it := by
exact .single _, rfl, h
theorem IterM.TerminationMeasures.Finite.rel_trans
{α : Type w} {m : Type w Type w'} {β : Type w} [Iterator α m β]
{it it' it'' : TerminationMeasures.Finite α m} :
it.Rel it' it'.Rel it'' it.Rel it'' :=
.trans
macro_rules | `(tactic| decreasing_trivial) => `(tactic|
first
| exact IterM.TerminationMeasures.Finite.rel_of_yield _

View File

@@ -94,7 +94,7 @@ it.filterMapWithPostcondition ---a'-----c'-------⊥
**Termination properties:**
* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is finite
* `Productive` instance: only if `it` is finite`
For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided. For example, if `f` never returns `none`, then

View File

@@ -202,59 +202,6 @@ def Iter.all {α β : Type w}
(p : β Bool) (it : Iter (α := α) β) : Bool :=
(it.allM (fun x => pure (f := Id) (p x))).run
@[inline]
def Iter.findSomeM? {α β : Type w} {γ : Type x} {m : Type x Type w'} [Monad m] [Iterator α Id β]
[IteratorLoop α Id m] [Finite α Id] (it : Iter (α := α) β) (f : β m (Option γ)) :
m (Option γ) :=
ForIn.forIn it none (fun x _ => do
match f x with
| none => return .yield none
| some fx => return .done (some fx))
@[inline]
def Iter.Partial.findSomeM? {α β : Type w} {γ : Type x} {m : Type x Type w'} [Monad m]
[Iterator α Id β] [IteratorLoopPartial α Id m] (it : Iter.Partial (α := α) β)
(f : β m (Option γ)) :
m (Option γ) :=
ForIn.forIn it none (fun x _ => do
match f x with
| none => return .yield none
| some fx => return .done (some fx))
@[inline]
def Iter.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
[IteratorLoop α Id Id] [Finite α Id] (it : Iter (α := α) β) (f : β Option γ) :
Option γ :=
Id.run (it.findSomeM? (pure <| f ·))
@[inline]
def Iter.Partial.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
[IteratorLoopPartial α Id Id] (it : Iter.Partial (α := α) β) (f : β Option γ) :
Option γ :=
Id.run (it.findSomeM? (pure <| f ·))
@[inline]
def Iter.findM? {α β : Type w} {m : Type w Type w'} [Monad m] [Iterator α Id β]
[IteratorLoop α Id m] [Finite α Id] (it : Iter (α := α) β) (f : β m (ULift Bool)) :
m (Option β) :=
it.findSomeM? (fun x => return if ( f x).down then some x else none)
@[inline]
def Iter.Partial.findM? {α β : Type w} {m : Type w Type w'} [Monad m] [Iterator α Id β]
[IteratorLoopPartial α Id m] (it : Iter.Partial (α := α) β) (f : β m (ULift Bool)) :
m (Option β) :=
it.findSomeM? (fun x => return if ( f x).down then some x else none)
@[inline]
def Iter.find? {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
[Finite α Id] (it : Iter (α := α) β) (f : β Bool) : Option β :=
Id.run (it.findM? (pure <| .up <| f ·))
@[inline]
def Iter.Partial.find? {α β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id]
(it : Iter.Partial (α := α) β) (f : β Bool) : Option β :=
Id.run (it.findM? (pure <| .up <| f ·))
@[always_inline, inline, expose, inherit_doc IterM.size]
def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSize α Id]
(it : Iter (α := α) β) : Nat :=

View File

@@ -579,60 +579,6 @@ def IterM.Partial.all {α β : Type w} {m : Type w → Type w'} [Monad m]
(p : β Bool) (it : IterM.Partial (α := α) m β) : m (ULift Bool) := do
it.allM (fun x => pure (.up (p x)))
@[inline]
def IterM.findSomeM? {α β γ : Type w} {m : Type w Type w'} [Monad m] [Iterator α m β]
[IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) (f : β m (Option γ)) :
m (Option γ) :=
ForIn.forIn it none (fun x _ => do
match f x with
| none => return .yield none
| some fx => return .done (some fx))
@[inline]
def IterM.Partial.findSomeM? {α β γ : Type w} {m : Type w Type w'} [Monad m] [Iterator α m β]
[IteratorLoopPartial α m m] (it : IterM.Partial (α := α) m β) (f : β m (Option γ)) :
m (Option γ) :=
ForIn.forIn it none (fun x _ => do
match f x with
| none => return .yield none
| some fx => return .done (some fx))
@[inline]
def IterM.findSome? {α β γ : Type w} {m : Type w Type w'} [Monad m] [Iterator α m β]
[IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) (f : β Option γ) :
m (Option γ) :=
it.findSomeM? (pure <| f ·)
@[inline]
def IterM.Partial.findSome? {α β γ : Type w} {m : Type w Type w'} [Monad m] [Iterator α m β]
[IteratorLoopPartial α m m] (it : IterM.Partial (α := α) m β) (f : β Option γ) :
m (Option γ) :=
it.findSomeM? (pure <| f ·)
@[inline]
def IterM.findM? {α β : Type w} {m : Type w Type w'} [Monad m] [Iterator α m β]
[IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) (f : β m (ULift Bool)) :
m (Option β) :=
it.findSomeM? (fun x => return if ( f x).down then some x else none)
@[inline]
def IterM.Partial.findM? {α β : Type w} {m : Type w Type w'} [Monad m] [Iterator α m β]
[IteratorLoopPartial α m m] (it : IterM.Partial (α := α) m β) (f : β m (ULift Bool)) :
m (Option β) :=
it.findSomeM? (fun x => return if ( f x).down then some x else none)
@[inline]
def IterM.find? {α β : Type w} {m : Type w Type w'} [Monad m] [Iterator α m β]
[IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) (f : β Bool) :
m (Option β) :=
it.findM? (pure <| .up <| f ·)
@[inline]
def IterM.Partial.find? {α β : Type w} {m : Type w Type w'} [Monad m] [Iterator α m β]
[IteratorLoopPartial α m m] (it : IterM.Partial (α := α) m β) (f : β Bool) :
m (Option β) :=
it.findM? (pure <| .up <| f ·)
section Size
/--

View File

@@ -726,170 +726,4 @@ theorem Iter.all_eq_not_any_not {α β : Type w} [Iterator α Id β]
· simp [ihs _]
· simp
theorem Iter.findSomeM?_eq_match_step {α β : Type w} {γ : Type x} {m : Type x Type w'} [Monad m]
[Iterator α Id β] [IteratorLoop α Id m] [LawfulMonad m] [Finite α Id] [LawfulIteratorLoop α Id m]
{it : Iter (α := α) β} {f : β m (Option γ)} :
it.findSomeM? f = (do
match it.step.val with
| .yield it' out =>
match f out with
| none => it'.findSomeM? f
| some fx => return (some fx)
| .skip it' => it'.findSomeM? f
| .done => return none) := by
rw [findSomeM?, forIn_eq_match_step]
cases it.step using PlausibleIterStep.casesOn
· simp only [bind_assoc]
apply bind_congr; intro fx
split <;> simp [findSomeM?]
· simp [findSomeM?]
· simp
theorem Iter.findSomeM?_toList {α β : Type w} {γ : Type x} {m : Type x Type w'} [Monad m]
[Iterator α Id β] [IteratorLoop α Id m] [IteratorCollect α Id Id]
[LawfulMonad m] [Finite α Id] [LawfulIteratorLoop α Id m] [LawfulIteratorCollect α Id Id]
{it : Iter (α := α) β} {f : β m (Option γ)} :
it.toList.findSomeM? f = it.findSomeM? f := by
induction it using Iter.inductSteps with | step it ihy ihs
rw [it.findSomeM?_eq_match_step, it.toList_eq_match_step]
cases it.step using PlausibleIterStep.casesOn
· simp only [List.findSomeM?_cons]
apply bind_congr; intro fx
split <;> simp [ihy _]
· simp [ihs _]
· simp
theorem Iter.findSome?_eq_findSomeM? {α β : Type w} {γ : Type x}
[Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id]
{it : Iter (α := α) β} {f : β Option γ} :
it.findSome? f = Id.run (it.findSomeM? (pure <| f ·)) :=
(rfl)
theorem Iter.findSome?_eq_findSome?_toIterM {α β γ : Type w}
[Iterator α Id β] [IteratorLoop α Id Id.{w}] [Finite α Id]
{it : Iter (α := α) β} {f : β Option γ} :
it.findSome? f = (it.toIterM.findSome? f).run :=
(rfl)
theorem Iter.findSome?_eq_match_step {α β : Type w} {γ : Type x}
[Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id]
[LawfulIteratorLoop α Id Id] {it : Iter (α := α) β} {f : β Option γ} :
it.findSome? f = (match it.step.val with
| .yield it' out =>
match f out with
| none => it'.findSome? f
| some fx => some fx
| .skip it' => it'.findSome? f
| .done => none) := by
rw [findSome?_eq_findSomeM?, findSomeM?_eq_match_step]
split
· simp only [pure_bind, findSome?_eq_findSomeM?]
split <;> simp
· simp [findSome?_eq_findSomeM?]
· simp
theorem Iter.findSome?_toList {α β : Type w} {γ : Type x}
[Iterator α Id β] [IteratorLoop α Id Id] [IteratorCollect α Id Id]
[Finite α Id] [LawfulIteratorLoop α Id Id] [LawfulIteratorCollect α Id Id]
{it : Iter (α := α) β} {f : β Option γ} :
it.toList.findSome? f = it.findSome? f := by
simp [findSome?_eq_findSomeM?, List.findSome?_eq_findSomeM?, findSomeM?_toList]
theorem Iter.findSomeM?_pure {α β : Type w} {γ : Type x} {m : Type x Type w'} [Monad m]
[Iterator α Id β] [IteratorLoop α Id m] [IteratorLoop α Id Id]
[LawfulMonad m] [Finite α Id] [LawfulIteratorLoop α Id m] [LawfulIteratorLoop α Id Id]
{it : Iter (α := α) β} {f : β Option γ} :
it.findSomeM? (pure <| f ·) = pure (f := m) (it.findSome? f) := by
letI : IteratorCollect α Id Id := .defaultImplementation
simp [ findSomeM?_toList, findSome?_toList, List.findSomeM?_pure]
theorem Iter.findM?_eq_findSomeM? {α β : Type w} {m : Type w Type w'} [Monad m]
[Iterator α Id β] [IteratorLoop α Id m] [Finite α Id]
{it : Iter (α := α) β} {f : β m (ULift Bool)} :
it.findM? f = it.findSomeM? (fun x => return if ( f x).down then some x else none) :=
(rfl)
theorem Iter.findM?_eq_match_step {α β : Type w} {m : Type w Type w'} [Monad m]
[Iterator α Id β] [IteratorLoop α Id m] [LawfulMonad m] [Finite α Id] [LawfulIteratorLoop α Id m]
{it : Iter (α := α) β} {f : β m (ULift Bool)} :
it.findM? f = (do
match it.step.val with
| .yield it' out =>
if ( f out).down then return (some out) else it'.findM? f
| .skip it' => it'.findM? f
| .done => return none) := by
rw [findM?_eq_findSomeM?, findSomeM?_eq_match_step]
split
· simp only [bind_assoc]
apply bind_congr; intro fx
split <;> simp [findM?_eq_findSomeM?]
· simp [findM?_eq_findSomeM?]
· simp
theorem Iter.findM?_toList {α β : Type} {m : Type Type w'} [Monad m]
[Iterator α Id β] [IteratorLoop α Id m] [IteratorCollect α Id Id]
[LawfulMonad m] [Finite α Id] [LawfulIteratorLoop α Id m] [LawfulIteratorCollect α Id Id]
{it : Iter (α := α) β} {f : β m Bool} :
it.toList.findM? f = it.findM? (.up <$> f ·) := by
simp [findM?_eq_findSomeM?, List.findM?_eq_findSomeM?, findSomeM?_toList]
theorem Iter.findM?_eq_findM?_toList {α β : Type} {m : Type Type w'} [Monad m]
[Iterator α Id β] [IteratorLoop α Id m] [IteratorCollect α Id Id]
[LawfulMonad m] [Finite α Id] [LawfulIteratorLoop α Id m] [LawfulIteratorCollect α Id Id]
{it : Iter (α := α) β} {f : β m (ULift Bool)} :
it.findM? f = it.toList.findM? (ULift.down <$> f ·) := by
simp [findM?_toList]
theorem Iter.find?_eq_findM? {α β : Type w} [Iterator α Id β]
[IteratorLoop α Id Id] [Finite α Id] {it : Iter (α := α) β} {f : β Bool} :
it.find? f = Id.run (it.findM? (pure <| .up <| f ·)) :=
(rfl)
theorem Iter.find?_eq_find?_toIterM {α β : Type w} [Iterator α Id β]
[IteratorLoop α Id Id] [Finite α Id] {it : Iter (α := α) β} {f : β Bool} :
it.find? f = (it.toIterM.find? f).run :=
(rfl)
theorem Iter.find?_eq_findSome? {α β : Type w} [Iterator α Id β]
[IteratorLoop α Id Id] [Finite α Id] {it : Iter (α := α) β} {f : β Bool} :
it.find? f = it.findSome? (fun x => if f x then some x else none) := by
simp [find?_eq_findM?, findSome?_eq_findSomeM?, findM?_eq_findSomeM?]
theorem Iter.find?_eq_match_step {α β : Type w}
[Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id] [LawfulIteratorLoop α Id Id]
{it : Iter (α := α) β} {f : β Bool} :
it.find? f = (match it.step.val with
| .yield it' out =>
if f out then some out else it'.find? f
| .skip it' => it'.find? f
| .done => none) := by
rw [find?_eq_findM?, findM?_eq_match_step]
split
· simp only [pure_bind]
split <;> simp [find?_eq_findM?]
· simp [find?_eq_findM?]
· simp
theorem Iter.find?_toList {α β : Type w}
[Iterator α Id β] [IteratorLoop α Id Id] [IteratorCollect α Id Id]
[Finite α Id] [LawfulIteratorLoop α Id Id] [LawfulIteratorCollect α Id Id]
{it : Iter (α := α) β} {f : β Bool} :
it.toList.find? f = it.find? f := by
simp [find?_eq_findSome?, List.find?_eq_findSome?_guard, findSome?_toList, Option.guard_def]
theorem Iter.findM?_pure {α β : Type w} {m : Type w Type w'} [Monad m]
[Iterator α Id β] [IteratorLoop α Id m] [IteratorLoop α Id Id]
[LawfulMonad m] [Finite α Id] [LawfulIteratorLoop α Id m] [LawfulIteratorLoop α Id Id]
{it : Iter (α := α) β} {f : β ULift Bool} :
it.findM? (pure (f := m) <| f ·) = pure (f := m) (it.find? (ULift.down <| f ·)) := by
induction it using Iter.inductSteps with | step it ihy ihs
rw [findM?_eq_match_step, find?_eq_match_step]
cases it.step using PlausibleIterStep.casesOn
· simp only [pure_bind]
split
· simp
· simp [ihy _]
· simp [ihs _]
· simp
end Std.Iterators

View File

@@ -514,126 +514,4 @@ theorem IterM.all_eq_not_any_not {α β : Type w} {m : Type w → Type w'} [Iter
· simp [ihs _]
· simp
theorem IterM.findSomeM?_eq_match_step {α β γ : Type w} {m : Type w Type w'} [Monad m]
[Iterator α m β] [IteratorLoop α m m] [LawfulMonad m] [Finite α m] [LawfulIteratorLoop α m m]
{it : IterM (α := α) m β} {f : β m (Option γ)} :
it.findSomeM? f = (do
match ( it.step).inflate.val with
| .yield it' out =>
match f out with
| none => it'.findSomeM? f
| some fx => return (some fx)
| .skip it' => it'.findSomeM? f
| .done => return none) := by
rw [findSomeM?, forIn_eq_match_step]
apply bind_congr; intro step
cases step.inflate using PlausibleIterStep.casesOn
· simp only [bind_assoc]
apply bind_congr; intro fx
split <;> simp [findSomeM?]
· simp [findSomeM?]
· simp
theorem IterM.findSome?_eq_findSomeM? {α β γ : Type w} {m : Type w Type w'} [Monad m]
[Iterator α m β] [IteratorLoop α m m] [Finite α m]
{it : IterM (α := α) m β} {f : β Option γ} :
it.findSome? f = it.findSomeM? (pure <| f ·) :=
(rfl)
theorem IterM.findSome?_eq_match_step {α β γ : Type w} {m : Type w Type w'} [Monad m]
[Iterator α m β] [IteratorLoop α m m] [LawfulMonad m] [Finite α m] [LawfulIteratorLoop α m m]
{it : IterM (α := α) m β} {f : β Option γ} :
it.findSome? f = (do
match ( it.step).inflate.val with
| .yield it' out =>
match f out with
| none => it'.findSome? f
| some fx => return (some fx)
| .skip it' => it'.findSome? f
| .done => return none) := by
rw [findSome?_eq_findSomeM?, findSomeM?_eq_match_step]
apply bind_congr; intro step
split <;> simp [findSome?_eq_findSomeM?]
theorem IterM.findSomeM?_pure {α β γ : Type w} {m : Type w Type w'} [Monad m]
[Iterator α m β] [IteratorLoop α m m]
[LawfulMonad m] [Finite α m] [LawfulIteratorLoop α m m]
{it : IterM (α := α) m β} {f : β Option γ} :
it.findSomeM? (pure <| f ·) = it.findSome? f := by
induction it using IterM.inductSteps with | step it ihy ihs
rw [findSomeM?_eq_match_step, findSome?_eq_match_step]
apply bind_congr; intro step
cases step.inflate using PlausibleIterStep.casesOn
· simp only [pure_bind]
split <;> simp [ihy _]
· simp [ihs _]
· simp
theorem IterM.findM?_eq_findSomeM? {α β : Type w} {m : Type w Type w'} [Monad m]
[Iterator α m β] [IteratorLoop α m m] [Finite α m]
{it : IterM (α := α) m β} {f : β m (ULift Bool)} :
it.findM? f = it.findSomeM? (fun x => return if ( f x).down then some x else none) :=
(rfl)
theorem IterM.findM?_eq_match_step {α β : Type w} {m : Type w Type w'} [Monad m]
[Iterator α m β] [IteratorLoop α m m] [LawfulMonad m] [Finite α m] [LawfulIteratorLoop α m m]
{it : IterM (α := α) m β} {f : β m (ULift Bool)} :
it.findM? f = (do
match ( it.step).inflate.val with
| .yield it' out =>
if ( f out).down then return (some out) else it'.findM? f
| .skip it' => it'.findM? f
| .done => return none) := by
rw [findM?_eq_findSomeM?, findSomeM?_eq_match_step]
apply bind_congr; intro step
split
· simp only [bind_assoc]
apply bind_congr; intro fx
split <;> simp [findM?_eq_findSomeM?]
· simp [findM?_eq_findSomeM?]
· simp
theorem IterM.find?_eq_findM? {α β : Type w} {m : Type w Type w'} [Monad m] [Iterator α m β]
[IteratorLoop α m m] [Finite α m] {it : IterM (α := α) m β} {f : β Bool} :
it.find? f = it.findM? (pure <| .up <| f ·) :=
(rfl)
theorem IterM.find?_eq_findSome? {α β : Type w} {m : Type w Type w'} [Monad m] [Iterator α m β]
[IteratorLoop α m m] [LawfulMonad m] [Finite α m] {it : IterM (α := α) m β} {f : β Bool} :
it.find? f = it.findSome? (fun x => if f x then some x else none) := by
simp [find?_eq_findM?, findSome?_eq_findSomeM?, findM?_eq_findSomeM?]
theorem IterM.find?_eq_match_step {α β : Type w} {m : Type w Type w'} [Monad m]
[Iterator α m β] [IteratorLoop α m m] [LawfulMonad m] [Finite α m] [LawfulIteratorLoop α m m]
{it : IterM (α := α) m β} {f : β Bool} :
it.find? f = (do
match ( it.step).inflate.val with
| .yield it' out =>
if f out then return (some out) else it'.find? f
| .skip it' => it'.find? f
| .done => return none) := by
rw [find?_eq_findM?, findM?_eq_match_step]
apply bind_congr; intro step
split
· simp only [pure_bind]
split <;> simp [find?_eq_findM?]
· simp [find?_eq_findM?]
· simp
theorem IterM.findM?_pure {α β : Type w} {m : Type w Type w'} [Monad m]
[Iterator α m β] [IteratorLoop α m m]
[LawfulMonad m] [Finite α m] [LawfulIteratorLoop α m m]
{it : IterM (α := α) m β} {f : β ULift Bool} :
it.findM? (pure (f := m) <| f ·) = it.find? (ULift.down <| f ·) := by
induction it using IterM.inductSteps with | step it ihy ihs
rw [findM?_eq_match_step, find?_eq_match_step]
apply bind_congr; intro step
cases step.inflate using PlausibleIterStep.casesOn
· simp only [pure_bind]
split
· simp
· simp [ihy _]
· simp [ihs _]
· simp
end Std.Iterators

View File

@@ -403,21 +403,6 @@ def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f
| some b => pure (some b)
| none => findSomeM? f as
@[simp, grind =]
theorem findSomeM?_nil [Monad m] {α : Type w} {β : Type u}
{f : α m (Option β)} :
([] : List α).findSomeM? f = pure none :=
(rfl)
@[grind =]
theorem findSomeM?_cons [Monad m] {α : Type w} {β : Type u}
{f : α m (Option β)} {a : α} {as : List α} :
(a::as).findSomeM? f = (do
match f a with
| some b => return some b
| none => as.findSomeM? f) :=
(rfl)
@[simp]
theorem findSomeM?_pure [Monad m] [LawfulMonad m] {f : α Option β} {as : List α} :
findSomeM? (m := m) (pure <| f ·) as = pure (as.findSome? f) := by
@@ -439,10 +424,6 @@ theorem findSomeM?_id (f : α → Id (Option β)) (as : List α) :
findSomeM? (m := Id) f as = as.findSome? f :=
findSomeM?_pure
theorem findSome?_eq_findSomeM? {f : α Option β} {as : List α} :
as.findSome? f = (as.findSomeM? (pure (f := Id) <| f ·)).run := by
simp
theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] {p : α m Bool} {as : List α} :
as.findM? p = as.findSomeM? fun a => return if ( p a) then some a else none := by
induction as with

View File

@@ -1023,19 +1023,6 @@ theorem ofScientific_def' :
· push_cast
rfl
/-!
# min and max
-/
@[grind =] protected theorem max_def {n m : Rat} : max n m = if n m then m else n := rfl
@[grind =] protected theorem min_def {n m : Rat} : min n m = if n m then n else m := rfl
/-!
# floor
-/
theorem floor_def (a : Rat) : a.floor = a.num / a.den := by
rw [Rat.floor]
split <;> simp_all

View File

@@ -16,6 +16,3 @@ public import Init.Data.String.Bootstrap
public import Init.Data.String.Slice
public import Init.Data.String.Pattern
public import Init.Data.String.Stream
public import Init.Data.String.PosRaw
public import Init.Data.String.Substring
public import Init.Data.String.TakeDrop

File diff suppressed because it is too large Load Diff

View File

@@ -134,19 +134,19 @@ public theorem String.utf8EncodeChar_eq_utf8EncodeCharFast : @utf8EncodeChar = @
cases Decidable.em (c.val 0x7ff) <;> simp [*]
cases Decidable.em (c.val 0xffff) <;> simp [*]
public theorem String.utf8EncodeChar_eq_singleton {c : Char} : c.utf8Size = 1
theorem String.utf8EncodeChar_eq_singleton {c : Char} : c.utf8Size = 1
String.utf8EncodeChar c = [c.val.toUInt8] := by
rw [ length_utf8EncodeChar]
fun_cases utf8EncodeChar
all_goals simp_all; try rfl
public theorem String.utf8EncodeChar_eq_cons_cons {c : Char} : c.utf8Size = 2
theorem String.utf8EncodeChar_eq_cons_cons {c : Char} : c.utf8Size = 2
String.utf8EncodeChar c = [(c.val >>> 6).toUInt8 &&& 0x1f ||| 0xc0, c.val.toUInt8 &&& 0x3f ||| 0x80] := by
rw [ length_utf8EncodeChar, utf8EncodeChar_eq_utf8EncodeCharFast]
fun_cases utf8EncodeCharFast
all_goals simp_all <;> (repeat' apply And.intro) <;> rfl
public theorem String.utf8EncodeChar_eq_cons_cons_cons {c : Char} : c.utf8Size = 3
theorem String.utf8EncodeChar_eq_cons_cons_cons {c : Char} : c.utf8Size = 3
String.utf8EncodeChar c =
[(c.val >>> 12).toUInt8 &&& 0x0f ||| 0xe0,
(c.val >>> 6).toUInt8 &&& 0x3f ||| 0x80,
@@ -155,7 +155,7 @@ public theorem String.utf8EncodeChar_eq_cons_cons_cons {c : Char} : c.utf8Size =
fun_cases utf8EncodeCharFast
all_goals simp_all <;> (repeat' apply And.intro) <;> rfl
public theorem String.utf8EncodeChar_eq_cons_cons_cons_cons {c : Char} : c.utf8Size = 4
theorem String.utf8EncodeChar_eq_cons_cons_cons_cons {c : Char} : c.utf8Size = 4
String.utf8EncodeChar c =
[(c.val >>> 18).toUInt8 &&& 0x07 ||| 0xf0,
(c.val >>> 12).toUInt8 &&& 0x3f ||| 0x80,
@@ -1464,8 +1464,7 @@ public theorem ByteArray.isUTF8FirstByte_getElem_zero_utf8EncodeChar_append {c :
public theorem ByteArray.isUTF8FirstByte_of_isSome_utf8DecodeChar? {b : ByteArray} {i : Nat}
(h : (utf8DecodeChar? b i).isSome) : (b[i]'(lt_size_of_isSome_utf8DecodeChar? h)).IsUTF8FirstByte := by
rw [utf8DecodeChar?_eq_utf8DecodeChar?_extract] at h
suffices ((b.extract i b.size)[0]'
(by simpa using lt_size_of_isSome_utf8DecodeChar? h)).IsUTF8FirstByte by
suffices ((b.extract i b.size)[0]'(lt_size_of_isSome_utf8DecodeChar? h)).IsUTF8FirstByte by
simpa [ByteArray.getElem_extract, Nat.add_zero] using this
obtain c, hc := Option.isSome_iff_exists.1 h
conv => congr; congr; rw [eq_of_utf8DecodeChar?_eq_some hc]

View File

@@ -9,24 +9,9 @@ prelude
import all Init.Data.ByteArray.Basic
public import Init.Data.String.Basic
import all Init.Data.String.Basic
public import Init.Data.String.Iterator
import all Init.Data.String.Iterator
public import Init.Data.String.Substring
public section
namespace Substring
/--
Returns an iterator into the underlying string, at the substring's starting position. The ending
position is discarded, so the iterator alone cannot be used to determine whether its current
position is within the original substring.
-/
@[inline] def toIterator : Substring String.Iterator
| s, b, _ => s, b
end Substring
namespace String
/--
@@ -63,7 +48,7 @@ abbrev validateUTF8 (a : ByteArray) : Bool :=
theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext) : sizeOf i.next < sizeOf i := by
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.Pos.Raw.lt_next s pos)
exact Nat.sub_lt_sub_left h (String.lt_next s pos)
macro_rules
| `(tactic| decreasing_trivial) =>
@@ -168,26 +153,26 @@ def crlfToLf (text : String) : String :=
go "" 0 0
where
go (acc : String) (accStop pos : String.Pos.Raw) : String :=
if h : pos.atEnd text then
if h : text.atEnd pos then
-- note: if accStop = 0 then acc is empty
if accStop = 0 then text else acc ++ accStop.extract text pos
if accStop = 0 then text else acc ++ text.extract accStop pos
else
let c := pos.get' text h
let pos' := pos.next' text h
if h' : ¬ pos'.atEnd text c == '\r' pos'.get text == '\n' then
let acc := acc ++ accStop.extract text pos
go acc pos' (pos'.next' text h'.1)
let c := text.get' pos h
let pos' := text.next' pos h
if h' : ¬ text.atEnd pos' c == '\r' text.get pos' == '\n' then
let acc := acc ++ text.extract accStop pos
go acc pos' (text.next' pos' h'.1)
else
go acc accStop pos'
termination_by text.utf8ByteSize - pos.byteIdx
decreasing_by
decreasing_with
change text.utf8ByteSize - ((pos.next text).next text).byteIdx < text.utf8ByteSize - pos.byteIdx
change text.utf8ByteSize - (text.next (text.next pos)).byteIdx < text.utf8ByteSize - pos.byteIdx
have k := Nat.gt_of_not_le <| mt decide_eq_true h
exact Nat.sub_lt_sub_left k (Nat.lt_trans (String.Pos.Raw.lt_next text pos) (String.Pos.Raw.lt_next _ _))
exact Nat.sub_lt_sub_left k (Nat.lt_trans (String.lt_next text pos) (String.lt_next _ _))
decreasing_with
change text.utf8ByteSize - (pos.next text).byteIdx < text.utf8ByteSize - pos.byteIdx
change text.utf8ByteSize - (text.next pos).byteIdx < text.utf8ByteSize - pos.byteIdx
have k := Nat.gt_of_not_le <| mt decide_eq_true h
exact Nat.sub_lt_sub_left k (String.Pos.Raw.lt_next _ _)
exact Nat.sub_lt_sub_left k (String.lt_next _ _)
end String

View File

@@ -1,206 +0,0 @@
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura, Mario Carneiro
-/
module
prelude
public import Init.Data.String.Basic
/-!
# `String.Iterator`
This file contains `String.Iterator`, an outgoing API to be replaced by the iterator framework in
a future release.
-/
public section
namespace String
/--
An iterator over the characters (Unicode code points) in a `String`. Typically created by
`String.iter`.
String iterators pair a string with a valid byte index. This allows efficient character-by-character
processing of strings while avoiding the need to manually ensure that byte indices are used with the
correct strings.
An iterator is *valid* if the position `i` is *valid* for the string `s`, meaning `0 ≤ i ≤ s.rawEndPos`
and `i` lies on a UTF8 byte boundary. If `i = s.rawEndPos`, the iterator is at the end of the string.
Most operations on iterators return unspecified values if the iterator is not valid. The functions
in the `String.Iterator` API rule out the creation of invalid iterators, with two exceptions:
- `Iterator.next iter` is invalid if `iter` is already at the end of the string (`iter.atEnd` is
`true`), and
- `Iterator.forward iter n`/`Iterator.nextn iter n` is invalid if `n` is strictly greater than the
number of remaining characters.
-/
structure Iterator where
/-- The string being iterated over. -/
s : String
/-- The current UTF-8 byte position in the string `s`.
This position is not guaranteed to be valid for the string. If the position is not valid, then the
current character is `(default : Char)`, similar to `String.get` on an invalid position.
-/
i : Pos.Raw
deriving DecidableEq, Inhabited
/-- Creates an iterator at the beginning of the string. -/
@[inline] def mkIterator (s : String) : Iterator :=
s, 0
@[inherit_doc mkIterator]
abbrev iter := mkIterator
/--
The size of a string iterator is the number of bytes remaining.
Recursive functions that iterate towards the end of a string will typically decrease this measure.
-/
instance : SizeOf String.Iterator where
sizeOf i := i.1.utf8ByteSize - i.2.byteIdx
theorem Iterator.sizeOf_eq (i : String.Iterator) : sizeOf i = i.1.utf8ByteSize - i.2.byteIdx :=
rfl
namespace Iterator
@[inline, inherit_doc Iterator.s]
def toString := Iterator.s
/--
The number of UTF-8 bytes remaining in the iterator.
-/
@[inline] def remainingBytes : Iterator Nat
| s, i => s.rawEndPos.byteIdx - i.byteIdx
@[inline, inherit_doc Iterator.i]
def pos := Iterator.i
/--
Gets the character at the iterator's current position.
A run-time bounds check is performed. Use `String.Iterator.curr'` to avoid redundant bounds checks.
If the position is invalid, returns `(default : Char)`.
-/
@[inline] def curr : Iterator Char
| s, i => i.get s
/--
Moves the iterator's position forward by one character, unconditionally.
It is only valid to call this function if the iterator is not at the end of the string (i.e.
if `Iterator.atEnd` is `false`); otherwise, the resulting iterator will be invalid.
-/
@[inline] def next : Iterator Iterator
| s, i => s, i.next s
/--
Moves the iterator's position backward by one character, unconditionally.
The position is not changed if the iterator is at the beginning of the string.
-/
@[inline] def prev : Iterator Iterator
| s, i => s, i.prev s
/--
Checks whether the iterator is past its string's last character.
-/
@[inline] def atEnd : Iterator Bool
| s, i => i.byteIdx s.rawEndPos.byteIdx
/--
Checks whether the iterator is at or before the string's last character.
-/
@[inline] def hasNext : Iterator Bool
| s, i => i.byteIdx < s.rawEndPos.byteIdx
/--
Checks whether the iterator is after the beginning of the string.
-/
@[inline] def hasPrev : Iterator Bool
| _, i => i.byteIdx > 0
/--
Gets the character at the iterator's current position.
The proof of `it.hasNext` ensures that there is, in fact, a character at the current position. This
function is faster that `String.Iterator.curr` due to avoiding a run-time bounds check.
-/
@[inline] def curr' (it : Iterator) (h : it.hasNext) : Char :=
match it with
| s, i => i.get' s (by simpa only [hasNext, rawEndPos, decide_eq_true_eq, Pos.Raw.atEnd, ge_iff_le, Nat.not_le] using h)
/--
Moves the iterator's position forward by one character, unconditionally.
The proof of `it.hasNext` ensures that there is, in fact, a position that's one character forwards.
This function is faster that `String.Iterator.next` due to avoiding a run-time bounds check.
-/
@[inline] def next' (it : Iterator) (h : it.hasNext) : Iterator :=
match it with
| s, i => s, i.next' s (by simpa only [hasNext, rawEndPos, decide_eq_true_eq, Pos.Raw.atEnd, ge_iff_le, Nat.not_le] using h)
/--
Replaces the current character in the string.
Does nothing if the iterator is at the end of the string. If both the replacement character and the
replaced character are 7-bit ASCII characters and the string is not shared, then it is updated
in-place and not copied.
-/
@[inline] def setCurr : Iterator Char Iterator
| s, i, c => i.set s c, i
/--
Moves the iterator's position to the end of the string, just past the last character.
-/
@[inline] def toEnd : Iterator Iterator
| s, _ => s, s.rawEndPos
/--
Extracts the substring between the positions of two iterators. The first iterator's position is the
start of the substring, and the second iterator's position is the end.
Returns the empty string if the iterators are for different strings, or if the position of the first
iterator is past the position of the second iterator.
-/
@[inline] def extract : Iterator Iterator String
| s₁, b, s₂, e =>
if s₁ s₂ || b > e then ""
else b.extract s₁ e
/--
Moves the iterator's position forward by the specified number of characters.
The resulting iterator is only valid if the number of characters to skip is less than or equal
to the number of characters left in the iterator.
-/
def forward : Iterator Nat Iterator
| it, 0 => it
| it, n+1 => forward it.next n
/--
The remaining characters in an iterator, as a string.
-/
@[inline] def remainingToString : Iterator String
| s, i => i.extract s s.rawEndPos
@[inherit_doc forward]
def nextn : Iterator Nat Iterator
| it, 0 => it
| it, i+1 => nextn it.next i
/--
Moves the iterator's position back by the specified number of characters, stopping at the beginning
of the string.
-/
def prevn : Iterator Nat Iterator
| it, 0 => it
| it, i+1 => prevn it.prev i
end Iterator
end String

View File

@@ -35,7 +35,7 @@ inductive SearchStep (s : Slice) where
-/
| rejected (startPos endPos : s.Pos)
/--
The subslice starting at {name}`startPos` and ending at {name}`endPos` matches the pattern.
The subslice starting at {name}`startPos` and ending at {name}`endPos` did not match the pattern.
-/
| matched (startPos endPos : s.Pos)
deriving Inhabited
@@ -70,7 +70,7 @@ class ForwardPattern (ρ : Type) where
Checks whether the slice starts with the pattern. If it does, the slice is returned with the
prefix removed; otherwise the result is {name}`none`.
-/
dropPrefix? : (s : Slice) ρ Option s.Pos
dropPrefix? : Slice ρ Option Slice
namespace Internal
@@ -83,10 +83,10 @@ where
go (curr : String.Pos.Raw) : Bool :=
if h : curr < len then
have hl := by
simp [Pos.Raw.le_iff, Pos.Raw.lt_iff] at h h1
simp [Pos.Raw.le_iff] at h h1
omega
have hr := by
simp [Pos.Raw.le_iff, Pos.Raw.lt_iff] at h h2
simp [Pos.Raw.le_iff] at h h2
omega
if lhs.getUTF8Byte (curr.offsetBy lstart) hl == rhs.getUTF8Byte (curr.offsetBy rstart) hr then
go curr.inc
@@ -96,9 +96,47 @@ where
true
termination_by len.byteIdx - curr.byteIdx
decreasing_by
simp [Pos.Raw.lt_iff] at h
simp at h
omega
variable {ρ : Type} {σ : Slice Type}
variable [ s, Std.Iterators.Iterator (σ s) Id (SearchStep s)]
variable [ s, Std.Iterators.Finite (σ s) Id]
/--
Tries to skip the {name}`searcher` until the next {name}`SearchStep.matched` and return it. If no
match is found until the end returns {name}`none`.
-/
@[inline]
def nextMatch (searcher : Std.Iter (α := σ s) (SearchStep s)) :
Option (Std.Iter (α := σ s) (SearchStep s) × s.Pos × s.Pos) :=
go searcher
where
go [ s, Std.Iterators.Finite (σ s) Id] (searcher : Std.Iter (α := σ s) (SearchStep s)) :
Option (Std.Iter (α := σ s) (SearchStep s) × s.Pos × s.Pos) :=
match searcher.step with
| .yield it (.matched startPos endPos) _ => some (it, startPos, endPos)
| .yield it (.rejected ..) _ | .skip it .. => go it
| .done .. => none
termination_by Std.Iterators.Iter.finitelyManySteps searcher
/--
Tries to skip the {name}`searcher` until the next {name}`SearchStep.rejected` and return it. If no
reject is found until the end returns {name}`none`.
-/
@[inline]
def nextReject (searcher : Std.Iter (α := σ s) (SearchStep s)) :
Option (Std.Iter (α := σ s) (SearchStep s) × s.Pos × s.Pos) :=
go searcher
where
go [ s, Std.Iterators.Finite (σ s) Id] (searcher : Std.Iter (α := σ s) (SearchStep s)) :
Option (Std.Iter (α := σ s) (SearchStep s) × s.Pos × s.Pos) :=
match searcher.step with
| .yield it (.rejected startPos endPos) _ => some (it, startPos, endPos)
| .yield it (.matched ..) _ | .skip it .. => go it
| .done .. => none
termination_by Std.Iterators.Iter.finitelyManySteps searcher
end Internal
namespace ForwardPattern
@@ -115,10 +153,10 @@ def defaultStartsWith (s : Slice) (pat : ρ) : Bool :=
| _ => false
@[specialize pat]
def defaultDropPrefix? (s : Slice) (pat : ρ) : Option s.Pos :=
def defaultDropPrefix? (s : Slice) (pat : ρ) : Option Slice :=
let searcher := ToForwardSearcher.toSearcher s pat
match searcher.step with
| .yield _ (.matched _ endPos) _ => some endPos
| .yield _ (.matched _ endPos) _ => some (s.replaceStart endPos)
| _ => none
@[always_inline, inline]
@@ -158,7 +196,7 @@ class BackwardPattern (ρ : Type) where
Checks whether the slice ends with the pattern. If it does, the slice is returned with the
suffix removed; otherwise the result is {name}`none`.
-/
dropSuffix? : (s : Slice) ρ Option s.Pos
dropSuffix? : Slice ρ Option Slice
namespace ToBackwardSearcher
@@ -174,10 +212,10 @@ def defaultEndsWith (s : Slice) (pat : ρ) : Bool :=
| _ => false
@[specialize pat]
def defaultDropSuffix? (s : Slice) (pat : ρ) : Option s.Pos :=
def defaultDropSuffix? (s : Slice) (pat : ρ) : Option Slice :=
let searcher := ToBackwardSearcher.toSearcher s pat
match searcher.step with
| .yield _ (.matched startPos _) _ => some startPos
| .yield _ (.matched startPos _) _ => some (s.replaceEnd startPos)
| _ => none
@[always_inline, inline]

View File

@@ -139,7 +139,7 @@ def finitenessRelation : Std.Iterators.FinitenessRelation (BackwardCharSearcher
· cases h
obtain _, h1, h2, _ := h'
have h3 := Pos.offset_prev_lt_offset (h := h1)
simp [Pos.ext_iff, String.Pos.Raw.ext_iff, String.Pos.Raw.lt_iff] at h2 h3
simp [Pos.ext_iff, String.Pos.Raw.ext_iff] at h2 h3
omega
· cases h'
· cases h

View File

@@ -141,7 +141,7 @@ def finitenessRelation : Std.Iterators.FinitenessRelation (BackwardCharPredSearc
· cases h
obtain _, h1, h2, _ := h'
have h3 := Pos.offset_prev_lt_offset (h := h1)
simp [Pos.ext_iff, String.Pos.Raw.ext_iff, String.Pos.Raw.lt_iff] at h2 h3
simp [Pos.ext_iff, String.Pos.Raw.ext_iff] at h2 h3
omega
· cases h'
· cases h

View File

@@ -105,10 +105,10 @@ instance (s : Slice) : Std.Iterators.Iterator (ForwardSliceSearcher s) Id (Searc
left
exists nextStackPos
have haux := lt_offset_findNextPos h1
simp only [String.Pos.Raw.lt_iff, proper.injEq, true_and, exists_and_left, exists_eq', and_true,
simp only [pos_lt_eq, proper.injEq, true_and, exists_and_left, exists_eq', and_true,
nextStackPos]
constructor
· simp [String.Pos.Raw.le_iff, String.Pos.Raw.lt_iff] at h haux
· simp [String.Pos.Raw.le_iff] at h haux
omega
· apply Pos.Raw.IsValidForSlice.le_utf8ByteSize
apply Pos.isValidForSlice
@@ -121,12 +121,12 @@ instance (s : Slice) : Std.Iterators.Iterator (ForwardSliceSearcher s) Id (Searc
have hiter := by
left
exists nextStackPos
simp only [Pos.Raw.byteIdx_inc, proper.injEq, true_and, exists_and_left,
exists_eq', and_true, nextStackPos, String.Pos.Raw.lt_iff]
simp only [pos_lt_eq, Pos.Raw.byteIdx_inc, proper.injEq, true_and, exists_and_left,
exists_eq', and_true, nextStackPos]
constructor
· simp [String.Pos.Raw.le_iff] at h
omega
· simp [String.Pos.Raw.le_iff, String.Pos.Raw.lt_iff] at h1
· simp [String.Pos.Raw.le_iff] at h1
omega
.deflate .yield .proper needle table nextStackPos 0 res, hiter
else
@@ -142,7 +142,7 @@ instance (s : Slice) : Std.Iterators.Iterator (ForwardSliceSearcher s) Id (Searc
.deflate .done, by simp
termination_by s.utf8ByteSize - currStackPos.byteIdx
decreasing_by
simp [String.Pos.Raw.lt_iff] at h1
simp at h1
omega
findNext stackPos stackPos needlePos (by simp)
@@ -177,7 +177,7 @@ private def finitenessRelation :
apply Prod.Lex.right'
· simp
· have haux := np.isValidForSlice.le_utf8ByteSize
simp [Slice.Pos.lt_iff, String.Pos.Raw.le_iff, String.Pos.Raw.lt_iff] at h1' haux
simp [Slice.Pos.lt_iff, String.Pos.Raw.le_iff] at h1' haux
omega
· apply Prod.Lex.left
simp [h']
@@ -187,7 +187,7 @@ private def finitenessRelation :
· rw [h3']
apply Prod.Lex.right'
· simp
· simp [String.Pos.Raw.le_iff, String.Pos.Raw.lt_iff] at h1' h2'
· simp [String.Pos.Raw.le_iff] at h1' h2'
omega
· apply Prod.Lex.left
simp [h']
@@ -218,9 +218,9 @@ def startsWith (s : Slice) (pat : Slice) : Bool :=
false
@[inline]
def dropPrefix? (s : Slice) (pat : Slice) : Option s.Pos :=
def dropPrefix? (s : Slice) (pat : Slice) : Option Slice :=
if startsWith s pat then
some <| s.pos! <| pat.rawEndPos.offsetBy s.startPos.offset
some <| s.replaceStart <| s.pos! <| pat.rawEndPos.offsetBy s.startPos.offset
else
none
@@ -254,9 +254,9 @@ def endsWith (s : Slice) (pat : Slice) : Bool :=
false
@[inline]
def dropSuffix? (s : Slice) (pat : Slice) : Option s.Pos :=
def dropSuffix? (s : Slice) (pat : Slice) : Option Slice :=
if endsWith s pat then
some <| s.pos! <| s.endPos.offset.unoffsetBy pat.rawEndPos
some <| s.replaceEnd <| s.pos! <| s.endPos.offset.unoffsetBy pat.rawEndPos
else
none

View File

@@ -1,353 +0,0 @@
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura, Mario Carneiro
-/
module
prelude
public import Init.Data.String.Bootstrap
public import Init.Data.ByteArray.Basic
/-!
# Arithmetic of `String.Pos.Raw`
This file contains basic theory about which does not actually need to know anything about strings
and therefore does not depend on `Init.Data.String.Decode`.
-/
public section
namespace String
attribute [ext] String.Pos.Raw
instance : HSub String.Pos.Raw String String.Pos.Raw where
hSub p s := { byteIdx := p.byteIdx - s.utf8ByteSize }
instance : HSub String.Pos.Raw Char String.Pos.Raw where
hSub p c := { byteIdx := p.byteIdx - c.utf8Size }
@[export lean_string_pos_sub]
def Pos.Internal.subImpl : String.Pos.Raw String.Pos.Raw String.Pos.Raw :=
fun p₁ p₂ => p₁.byteIdx - p₂.byteIdx
instance : HAdd String.Pos.Raw Char String.Pos.Raw where
hAdd p c := { byteIdx := p.byteIdx + c.utf8Size }
instance : HAdd Char String.Pos.Raw String.Pos.Raw where
hAdd c p := { byteIdx := c.utf8Size + p.byteIdx }
instance : HAdd String String.Pos.Raw String.Pos.Raw where
hAdd s p := { byteIdx := s.utf8ByteSize + p.byteIdx }
instance : HAdd String.Pos.Raw String String.Pos.Raw where
hAdd p s := { byteIdx := p.byteIdx + s.utf8ByteSize }
instance : LE String.Pos.Raw where
le p₁ p₂ := p₁.byteIdx p₂.byteIdx
instance : LT String.Pos.Raw where
lt p₁ p₂ := p₁.byteIdx < p₂.byteIdx
instance (p₁ p₂ : String.Pos.Raw) : Decidable (p₁ p₂) :=
inferInstanceAs (Decidable (p₁.byteIdx p₂.byteIdx))
instance (p₁ p₂ : String.Pos.Raw) : Decidable (p₁ < p₂) :=
inferInstanceAs (Decidable (p₁.byteIdx < p₂.byteIdx))
instance : Min String.Pos.Raw := minOfLe
instance : Max String.Pos.Raw := maxOfLe
@[simp]
theorem Pos.Raw.byteIdx_sub_char {p : Pos.Raw} {c : Char} : (p - c).byteIdx = p.byteIdx - c.utf8Size := rfl
@[simp]
theorem Pos.Raw.byteIdx_sub_string {p : Pos.Raw} {s : String} : (p - s).byteIdx = p.byteIdx - s.utf8ByteSize := rfl
@[simp]
theorem Pos.Raw.byteIdx_add_string {p : Pos.Raw} {s : String} : (p + s).byteIdx = p.byteIdx + s.utf8ByteSize := rfl
@[simp]
theorem Pos.Raw.byteIdx_string_add {s : String} {p : Pos.Raw} : (s + p).byteIdx = s.utf8ByteSize + p.byteIdx := rfl
@[simp]
theorem Pos.Raw.byteIdx_add_char {p : Pos.Raw} {c : Char} : (p + c).byteIdx = p.byteIdx + c.utf8Size := rfl
@[simp]
theorem Pos.Raw.byteIdx_char_add {c : Char} {p : Pos.Raw} : (c + p).byteIdx = c.utf8Size + p.byteIdx := rfl
theorem Pos.Raw.le_iff {i₁ i₂ : Pos.Raw} : i₁ i₂ i₁.byteIdx i₂.byteIdx := .rfl
theorem Pos.Raw.lt_iff {i₁ i₂ : Pos.Raw} : i₁ < i₂ i₁.byteIdx < i₂.byteIdx := .rfl
@[simp]
theorem Pos.Raw.byteIdx_zero : (0 : Pos.Raw).byteIdx = 0 := rfl
/--
Returns the size of the byte slice delineated by the positions `lo` and `hi`.
-/
@[expose, inline]
def Pos.Raw.byteDistance (lo hi : Pos.Raw) : Nat :=
hi.byteIdx - lo.byteIdx
theorem Pos.Raw.byteDistance_eq {lo hi : Pos.Raw} : lo.byteDistance hi = hi.byteIdx - lo.byteIdx :=
(rfl)
@[simp]
theorem rawEndPos_empty : "".rawEndPos = 0 := rfl
@[deprecated rawEndPos_empty (since := "2025-10-20")]
theorem endPos_empty : "".rawEndPos = 0 := rfl
/--
Accesses the indicated byte in the UTF-8 encoding of a string.
At runtime, this function is implemented by efficient, constant-time code.
-/
@[extern "lean_string_get_byte_fast", expose]
def getUTF8Byte (s : @& String) (p : Pos.Raw) (h : p < s.rawEndPos) : UInt8 :=
s.bytes[p.byteIdx]
@[deprecated getUTF8Byte (since := "2025-10-01"), extern "lean_string_get_byte_fast", expose]
abbrev getUtf8Byte (s : String) (p : Pos.Raw) (h : p < s.rawEndPos) : UInt8 :=
s.getUTF8Byte p h
protected theorem Pos.Raw.le_trans {a b c : Pos.Raw} : a b b c a c := by
simpa [le_iff] using Nat.le_trans
protected theorem Pos.Raw.lt_of_lt_of_le {a b c : Pos.Raw} : a < b b c a < c := by
simpa [le_iff, lt_iff] using Nat.lt_of_lt_of_le
/--
Offsets `p` by `offset` on the left. This is not an `HAdd` instance because it should be a
relatively rare operation, so we use a name to make accidental use less likely. To offset a position
by the size of a character character `c` or string `s`, you can use `c + p` resp. `s + p`.
This should be seen as an operation that converts relative positions into absolute positions.
See also `Pos.Raw.increaseBy`, which is an "advancing" operation.
-/
@[expose, inline]
def Pos.Raw.offsetBy (p : Pos.Raw) (offset : Pos.Raw) : Pos.Raw where
byteIdx := offset.byteIdx + p.byteIdx
@[simp]
theorem Pos.Raw.byteIdx_offsetBy {p : Pos.Raw} {offset : Pos.Raw} :
(p.offsetBy offset).byteIdx = offset.byteIdx + p.byteIdx := (rfl)
theorem Pos.Raw.offsetBy_assoc {p q r : Pos.Raw} :
(p.offsetBy q).offsetBy r = p.offsetBy (q.offsetBy r) := by
ext
simp [Nat.add_assoc]
@[simp]
theorem Pos.Raw.offsetBy_zero_left {p : Pos.Raw} : (0 : Pos.Raw).offsetBy p = p := by
ext
simp
/--
Decreases `p` by `offset`. This is not an `HSub` instance because it should be a relatively
rare operation, so we use a name to make accidental use less likely. To unoffset a position
by the size of a character `c` or string `s`, you can use `p - c` resp. `p - s`.
This should be seen as an operation that converts absolute positions into relative positions.
See also `Pos.Raw.decreaseBy`, which is an "unadvancing" operation.
-/
@[expose, inline]
def Pos.Raw.unoffsetBy (p : Pos.Raw) (offset : Pos.Raw) : Pos.Raw where
byteIdx := p.byteIdx - offset.byteIdx
@[simp]
theorem Pos.Raw.byteIdx_unoffsetBy {p : Pos.Raw} {offset : Pos.Raw} :
(p.unoffsetBy offset).byteIdx = p.byteIdx - offset.byteIdx := (rfl)
theorem Pos.Raw.offsetBy_unoffsetBy_of_le {p : Pos.Raw} {q : Pos.Raw} (h : q p) :
(p.unoffsetBy q).offsetBy q = p := by
ext
simp_all [le_iff]
@[simp]
theorem Pos.Raw.unoffsetBy_offsetBy {p q : Pos.Raw} : (p.offsetBy q).unoffsetBy q = p := by
ext
simp
@[simp]
theorem Pos.Raw.eq_zero_iff {p : Pos.Raw} : p = 0 p.byteIdx = 0 :=
Pos.Raw.ext_iff
/--
Advances `p` by `n` bytes. This is not an `HAdd` instance because it should be a relatively
rare operation, so we use a name to make accidental use less likely. To add the size of a
character `c` or string `s` to a raw position `p`, you can use `p + c` resp. `p + s`.
This should be seen as an "advance" or "skip".
See also `Pos.Raw.offsetBy`, which turns relative positions into absolute positions.
-/
@[expose, inline]
def Pos.Raw.increaseBy (p : Pos.Raw) (n : Nat) : Pos.Raw where
byteIdx := p.byteIdx + n
@[simp]
theorem Pos.Raw.byteIdx_increaseBy {p : Pos.Raw} {n : Nat} :
(p.increaseBy n).byteIdx = p.byteIdx + n := (rfl)
/--
Move the position `p` back by `n` bytes. This is not an `HSub` instance because it should be a
relatively rare operation, so we use a name to make accidental use less likely. To remove the size
of a character `c` or string `s` from a raw position `p`, you can use `p - c` resp. `p - s`.
This should be seen as the inverse of an "advance" or "skip".
See also `Pos.Raw.unoffsetBy`, which turns absolute positions into relative positions.
-/
@[expose, inline]
def Pos.Raw.decreaseBy (p : Pos.Raw) (n : Nat) : Pos.Raw where
byteIdx := p.byteIdx - n
@[simp]
theorem Pos.Raw.byteIdx_decreaseBy {p : Pos.Raw} {n : Nat} :
(p.decreaseBy n).byteIdx = p.byteIdx - n := (rfl)
theorem Pos.Raw.increaseBy_charUtf8Size {p : Pos.Raw} {c : Char} :
p.increaseBy c.utf8Size = p + c := by
simp [Pos.Raw.ext_iff]
/-- Increases the byte offset of the position by `1`. Not to be confused with `ValidPos.next`. -/
@[inline, expose]
def Pos.Raw.inc (p : Pos.Raw) : Pos.Raw :=
p.byteIdx + 1
@[simp]
theorem Pos.Raw.byteIdx_inc {p : Pos.Raw} : p.inc.byteIdx = p.byteIdx + 1 := (rfl)
/-- Decreases the byte offset of the position by `1`. Not to be confused with `ValidPos.prev`. -/
@[inline, expose]
def Pos.Raw.dec (p : Pos.Raw) : Pos.Raw :=
p.byteIdx - 1
@[simp]
theorem Pos.Raw.byteIdx_dec {p : Pos.Raw} : p.dec.byteIdx = p.byteIdx - 1 := (rfl)
@[simp]
theorem Pos.Raw.le_refl {p : Pos.Raw} : p p := by simp [le_iff]
theorem Pos.Raw.lt_inc {p : Pos.Raw} : p < p.inc := by simp [lt_iff]
theorem Pos.Raw.le_of_lt {p q : Pos.Raw} : p < q p q := by simpa [lt_iff, le_iff] using Nat.le_of_lt
theorem Pos.Raw.inc_le {p q : Pos.Raw} : p.inc q p < q := by simpa [lt_iff, le_iff] using Nat.succ_le
theorem Pos.Raw.lt_of_le_of_lt {a b c : Pos.Raw} : a b b < c a < c := by
simpa [le_iff, lt_iff] using Nat.lt_of_le_of_lt
theorem Pos.Raw.ne_of_lt {a b : Pos.Raw} : a < b a b := by
simpa [lt_iff, Pos.Raw.ext_iff] using Nat.ne_of_lt
@[deprecated Pos.Raw.lt_iff (since := "2025-10-10")]
theorem pos_lt_eq (p₁ p₂ : Pos.Raw) : (p₁ < p₂) = (p₁.1 < p₂.1) :=
propext Pos.Raw.lt_iff
@[deprecated Pos.Raw.byteIdx_add_char (since := "2025-10-10")]
theorem pos_add_char (p : Pos.Raw) (c : Char) : (p + c).byteIdx = p.byteIdx + c.utf8Size :=
Pos.Raw.byteIdx_add_char
protected theorem Pos.Raw.ne_zero_of_lt : {a b : Pos.Raw} a < b b 0
| _, _, hlt, rfl => Nat.not_lt_zero _ hlt
/--
Returns either `p₁` or `p₂`, whichever has the least byte index.
-/
protected abbrev Pos.Raw.min (p₁ p₂ : Pos.Raw) : Pos.Raw :=
{ byteIdx := p₁.byteIdx.min p₂.byteIdx }
@[export lean_string_pos_min]
def Pos.Raw.Internal.minImpl (p₁ p₂ : Pos.Raw) : Pos.Raw :=
Pos.Raw.min p₁ p₂
namespace Pos.Raw
theorem byteIdx_mk (n : Nat) : byteIdx n = n := rfl
@[simp] theorem mk_zero : 0 = (0 : Pos.Raw) := rfl
@[simp] theorem mk_byteIdx (p : Pos.Raw) : p.byteIdx = p := rfl
@[deprecated byteIdx_offsetBy (since := "2025-10-08")]
theorem add_byteIdx {p₁ p₂ : Pos.Raw} : (p₂.offsetBy p₁).byteIdx = p₁.byteIdx + p₂.byteIdx := by
simp
@[deprecated byteIdx_offsetBy (since := "2025-10-08")]
theorem add_eq {p₁ p₂ : Pos.Raw} : p₂.offsetBy p₁ = p₁.byteIdx + p₂.byteIdx := rfl
@[deprecated byteIdx_unoffsetBy (since := "2025-10-08")]
theorem sub_byteIdx (p₁ p₂ : Pos.Raw) : (p₁.unoffsetBy p₂).byteIdx = p₁.byteIdx - p₂.byteIdx := rfl
@[deprecated byteIdx_add_char (since := "2025-10-10")]
theorem addChar_byteIdx (p : Pos.Raw) (c : Char) : (p + c).byteIdx = p.byteIdx + c.utf8Size :=
byteIdx_add_char
theorem add_char_eq (p : Pos.Raw) (c : Char) : p + c = p.byteIdx + c.utf8Size := rfl
@[deprecated add_char_eq (since := "2025-10-10")]
theorem addChar_eq (p : Pos.Raw) (c : Char) : p + c = p.byteIdx + c.utf8Size :=
add_char_eq p c
theorem byteIdx_zero_add_char (c : Char) : ((0 : Pos.Raw) + c).byteIdx = c.utf8Size := by
simp only [byteIdx_add_char, byteIdx_zero, Nat.zero_add]
@[deprecated byteIdx_zero_add_char (since := "2025-10-10")]
theorem zero_addChar_byteIdx (c : Char) : ((0 : Pos.Raw) + c).byteIdx = c.utf8Size :=
byteIdx_zero_add_char c
theorem zero_add_char_eq (c : Char) : (0 : Pos.Raw) + c = c.utf8Size := by rw [ byteIdx_zero_add_char]
@[deprecated zero_add_char_eq (since := "2025-10-10")]
theorem zero_addChar_eq (c : Char) : (0 : Pos.Raw) + c = c.utf8Size :=
zero_add_char_eq c
theorem add_char_right_comm (p : Pos.Raw) (c₁ c₂ : Char) : p + c₁ + c₂ = p + c₂ + c₁ := by
simpa [Pos.Raw.ext_iff] using Nat.add_right_comm ..
@[deprecated add_char_right_comm (since := "2025-10-10")]
theorem addChar_right_comm (p : Pos.Raw) (c₁ c₂ : Char) : p + c₁ + c₂ = p + c₂ + c₁ :=
add_char_right_comm p c₁ c₂
theorem ne_of_gt {i₁ i₂ : Pos.Raw} (h : i₁ < i₂) : i₂ i₁ := (ne_of_lt h).symm
@[deprecated byteIdx_add_string (since := "2025-10-10")]
theorem byteIdx_addString (p : Pos.Raw) (s : String) :
(p + s).byteIdx = p.byteIdx + s.utf8ByteSize := byteIdx_add_string
@[deprecated byteIdx_addString (since := "2025-03-18")]
abbrev addString_byteIdx := @byteIdx_add_string
theorem addString_eq (p : Pos.Raw) (s : String) : p + s = p.byteIdx + s.utf8ByteSize := rfl
theorem byteIdx_zero_add_string (s : String) : ((0 : Pos.Raw) + s).byteIdx = s.utf8ByteSize := by
simp only [byteIdx_add_string, byteIdx_zero, Nat.zero_add]
@[deprecated byteIdx_zero_add_string (since := "2025-10-10")]
theorem byteIdx_zero_addString (s : String) : ((0 : Pos.Raw) + s).byteIdx = s.utf8ByteSize :=
byteIdx_zero_add_string s
@[deprecated byteIdx_zero_addString (since := "2025-03-18")]
abbrev zero_addString_byteIdx := @byteIdx_zero_add_string
theorem zero_add_string_eq (s : String) : (0 : Pos.Raw) + s = s.utf8ByteSize := by
rw [ byteIdx_zero_add_string]
@[deprecated zero_add_string_eq (since := "2025-10-10")]
theorem zero_addString_eq (s : String) : (0 : Pos.Raw) + s = s.utf8ByteSize :=
zero_add_string_eq s
@[simp] theorem mk_le_mk {i₁ i₂ : Nat} : Pos.Raw.mk i₁ Pos.Raw.mk i₂ i₁ i₂ := .rfl
@[simp] theorem mk_lt_mk {i₁ i₂ : Nat} : Pos.Raw.mk i₁ < Pos.Raw.mk i₂ i₁ < i₂ := .rfl
end Pos.Raw
end String

View File

@@ -6,8 +6,7 @@ Author: Leonardo de Moura, Mario Carneiro
module
prelude
public import Init.Data.String.Substring
public import Init.Data.String.Iterator
public import Init.Data.String.Basic
public section
@@ -40,7 +39,7 @@ Examples:
* `"0xff".toInt? = none`
-/
def String.toInt? (s : String) : Option Int := do
if s.front = '-' then do
if s.get 0 = '-' then do
let v (s.toSubstring.drop 1).toNat?;
pure <| - Int.ofNat v
else
@@ -68,7 +67,7 @@ Examples:
* `"0xff".isInt = false`
-/
def String.isInt (s : String) : Bool :=
if s.front = '-' then
if s.get 0 = '-' then
(s.toSubstring.drop 1).isNat
else
s.isNat

View File

@@ -112,8 +112,8 @@ Examples:
def startsWith [ForwardPattern ρ] (s : Slice) (pat : ρ) : Bool :=
ForwardPattern.startsWith s pat
inductive SplitIterator (ρ : Type) (s : Slice) [ToForwardSearcher ρ σ] where
| operating (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
inductive SplitIterator (ρ : Type) [ToForwardSearcher ρ σ] where
| operating (s : Slice) (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
| atEnd
deriving Inhabited
@@ -121,72 +121,33 @@ namespace SplitIterator
variable [ToForwardSearcher ρ σ]
inductive PlausibleStep
instance : Std.Iterators.Iterator (SplitIterator ρ s) Id Slice where
IsPlausibleStep
| .operating _ s, .yield .operating _ s' _ => s'.IsPlausibleSuccessorOf s
| .operating _ s, .yield .atEnd .. _ => True
| .operating _ s, .skip .operating _ s' => s'.IsPlausibleSuccessorOf s
| .operating _ s, .skip .atEnd .. => False
| .operating _ s, .done => True
| .atEnd, .yield .. => False
| .atEnd, .skip _ => False
| .atEnd, .done => True
step
| .operating currPos searcher =>
match h : searcher.step with
| .yield searcher' (.matched startPos endPos), hps =>
instance [Pure m] : Std.Iterators.Iterator (SplitIterator ρ) m Slice where
IsPlausibleStep := fun _ _ => True
step := fun iter =>
match iter with
| .operating s currPos searcher =>
match Internal.nextMatch searcher with
| some (searcher, startPos, endPos) =>
let slice := s.replaceStartEnd! currPos startPos
let nextIt := .operating endPos searcher'
pure (.deflate .yield nextIt slice, by simp [nextIt, hps.isPlausibleSuccessor_of_yield])
| .yield searcher' (.rejected ..), hps =>
pure (.deflate .skip .operating currPos searcher',
by simp [hps.isPlausibleSuccessor_of_yield])
| .skip searcher', hps =>
pure (.deflate .skip .operating currPos searcher',
by simp [hps.isPlausibleSuccessor_of_skip])
| .done, _ =>
let nextIt := .operating s endPos searcher
pure (.deflate .yield nextIt slice, by simp)
| none =>
let slice := s.replaceStart currPos
pure (.deflate .yield .atEnd slice, by simp)
| .atEnd => pure (.deflate .done, by simp)
| .atEnd => pure (.deflate .done, by simp)
private def toOption : SplitIterator ρ s Option (Std.Iter (α := σ s) (SearchStep s))
| .operating _ s => some s
| .atEnd => none
-- TODO: Finiteness after we have a notion of lawful searcher
private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
Std.Iterators.FinitenessRelation (SplitIterator ρ s) Id where
rel := InvImage (Option.lt Std.Iterators.Iter.IsPlausibleSuccessorOf)
(SplitIterator.toOption Std.Iterators.IterM.internalState)
wf := InvImage.wf _ (Option.wellFounded_lt Std.Iterators.Finite.wf_of_id)
subrelation {it it'} h := by
simp_wf
obtain step, h, h' := h
match step with
| .yield it'' out | .skip it'' =>
obtain rfl : it' = it'' := by simpa using h.symm
simp only [Std.Iterators.IterM.IsPlausibleStep, Std.Iterators.Iterator.IsPlausibleStep] at h'
revert h'
match it, it' with
| .operating _ searcher, .operating _ searcher' => simp [SplitIterator.toOption, Option.lt]
| .operating _ searcher, .atEnd => simp [SplitIterator.toOption, Option.lt]
| .atEnd, _ => simp
@[no_expose]
instance [Std.Iterators.Finite (σ s) Id] : Std.Iterators.Finite (SplitIterator ρ s) Id :=
.of_finitenessRelation finitenessRelation
instance [Monad n] : Std.Iterators.IteratorCollect (SplitIterator ρ s) Id n :=
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (SplitIterator ρ) m n :=
.defaultImplementation
instance [Monad n] : Std.Iterators.IteratorCollectPartial (SplitIterator ρ s) Id n :=
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollectPartial (SplitIterator ρ) m n :=
.defaultImplementation
instance [Monad n] : Std.Iterators.IteratorLoop (SplitIterator ρ s) Id n :=
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (SplitIterator ρ) m n :=
.defaultImplementation
instance [Monad n] : Std.Iterators.IteratorLoopPartial (SplitIterator ρ s) Id n :=
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (SplitIterator ρ) m n :=
.defaultImplementation
end SplitIterator
@@ -200,18 +161,18 @@ multiple subslices in a row match the pattern, the resulting list will contain e
This function is generic over all currently supported patterns.
Examples:
* {lean}`("coffee tea water".toSlice.split Char.isWhitespace).toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
* {lean}`("coffee tea water".toSlice.split ' ').toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
* {lean}`("coffee tea water".toSlice.split " tea ").toList == ["coffee".toSlice, "water".toSlice]`
* {lean}`("ababababa".toSlice.split "aba").toList == ["coffee".toSlice, "water".toSlice]`
* {lean}`("baaab".toSlice.split "aa").toList == ["b".toSlice, "ab".toSlice]`
* {lean}`("coffee tea water".toSlice.split Char.isWhitespace).allowNontermination.toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
* {lean}`("coffee tea water".toSlice.split ' ').allowNontermination.toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
* {lean}`("coffee tea water".toSlice.split " tea ").allowNontermination.toList == ["coffee".toSlice, "water".toSlice]`
* {lean}`("ababababa".toSlice.split "aba").allowNontermination.toList == ["coffee".toSlice, "water".toSlice]`
* {lean}`("baaab".toSlice.split "aa").allowNontermination.toList == ["b".toSlice, "ab".toSlice]`
-/
@[specialize pat]
def split [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Std.Iter (α := SplitIterator ρ s) Slice :=
{ internalState := .operating s.startPos (ToForwardSearcher.toSearcher s pat) }
def split [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Std.Iter (α := SplitIterator ρ) Slice :=
{ internalState := .operating s s.startPos (ToForwardSearcher.toSearcher s pat) }
inductive SplitInclusiveIterator (ρ : Type) (s : Slice) [ToForwardSearcher ρ σ] where
| operating (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
inductive SplitInclusiveIterator (ρ : Type) [ToForwardSearcher ρ σ] where
| operating (s : Slice) (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
| atEnd
deriving Inhabited
@@ -219,79 +180,40 @@ namespace SplitInclusiveIterator
variable [ToForwardSearcher ρ σ]
instance : Std.Iterators.Iterator (SplitInclusiveIterator ρ s) Id Slice where
IsPlausibleStep
| .operating _ s, .yield .operating _ s' _ => s'.IsPlausibleSuccessorOf s
| .operating _ s, .yield .atEnd .. _ => True
| .operating _ s, .skip .operating _ s' => s'.IsPlausibleSuccessorOf s
| .operating _ s, .skip .atEnd .. => False
| .operating _ s, .done => True
| .atEnd, .yield .. => False
| .atEnd, .skip _ => False
| .atEnd, .done => True
step
| .operating currPos searcher =>
match h : searcher.step with
| .yield searcher' (.matched _ endPos), hps =>
instance [Pure m] : Std.Iterators.Iterator (SplitInclusiveIterator ρ) m Slice where
IsPlausibleStep := fun _ _ => True
step := fun iter =>
match iter with
| .operating s currPos searcher =>
match Internal.nextMatch searcher with
| some (searcher, _, endPos) =>
let slice := s.replaceStartEnd! currPos endPos
let nextIt := .operating endPos searcher'
pure (.deflate .yield nextIt slice,
by simp [nextIt, hps.isPlausibleSuccessor_of_yield])
| .yield searcher' (.rejected ..), hps =>
pure (.deflate .skip .operating currPos searcher',
by simp [hps.isPlausibleSuccessor_of_yield])
| .skip searcher', hps =>
pure (.deflate .skip .operating currPos searcher',
by simp [hps.isPlausibleSuccessor_of_skip])
| .done, _ =>
let nextIt := .operating s endPos searcher
pure (.deflate .yield nextIt slice, by simp)
| none =>
if currPos != s.endPos then
let slice := s.replaceStart currPos
pure (.deflate .yield .atEnd slice, by simp)
else
pure (.deflate .done, by simp)
| .atEnd => pure (.deflate .done, by simp)
| .atEnd => pure (.deflate .done, by simp)
private def toOption : SplitInclusiveIterator ρ s Option (Std.Iter (α := σ s) (SearchStep s))
| .operating _ s => some s
| .atEnd => none
-- TODO: Finiteness after we have a notion of lawful searcher
private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
Std.Iterators.FinitenessRelation (SplitInclusiveIterator ρ s) Id where
rel := InvImage (Option.lt Std.Iterators.Iter.IsPlausibleSuccessorOf)
(SplitInclusiveIterator.toOption Std.Iterators.IterM.internalState)
wf := InvImage.wf _ (Option.wellFounded_lt Std.Iterators.Finite.wf_of_id)
subrelation {it it'} h := by
simp_wf
obtain step, h, h' := h
match step with
| .yield it'' out | .skip it'' =>
obtain rfl : it' = it'' := by simpa using h.symm
simp only [Std.Iterators.IterM.IsPlausibleStep, Std.Iterators.Iterator.IsPlausibleStep] at h'
revert h'
match it, it' with
| .operating _ searcher, .operating _ searcher' => simp [SplitInclusiveIterator.toOption, Option.lt]
| .operating _ searcher, .atEnd => simp [SplitInclusiveIterator.toOption, Option.lt]
| .atEnd, _ => simp
@[no_expose]
instance [Std.Iterators.Finite (σ s) Id] :
Std.Iterators.Finite (SplitInclusiveIterator ρ s) Id :=
.of_finitenessRelation finitenessRelation
instance [Monad n] {s} :
Std.Iterators.IteratorCollect (SplitInclusiveIterator ρ s) Id n :=
instance [Monad m] [Monad n] :
Std.Iterators.IteratorCollect (SplitInclusiveIterator ρ) m n :=
.defaultImplementation
instance [Monad n] {s} :
Std.Iterators.IteratorCollectPartial (SplitInclusiveIterator ρ s) Id n :=
instance [Monad m] [Monad n] :
Std.Iterators.IteratorCollectPartial (SplitInclusiveIterator ρ) m n :=
.defaultImplementation
instance [Monad n] {s} :
Std.Iterators.IteratorLoop (SplitInclusiveIterator ρ s) Id n :=
instance [Monad m] [Monad n] :
Std.Iterators.IteratorLoop (SplitInclusiveIterator ρ) m n :=
.defaultImplementation
instance [Monad n] {s} :
Std.Iterators.IteratorLoopPartial (SplitInclusiveIterator ρ s) Id n :=
instance [Monad m] [Monad n] :
Std.Iterators.IteratorLoopPartial (SplitInclusiveIterator ρ) m n :=
.defaultImplementation
end SplitInclusiveIterator
@@ -303,15 +225,15 @@ matched subslices are included at the end of each subslice.
This function is generic over all currently supported patterns.
Examples:
* {lean}`("coffee tea water".toSlice.splitInclusive Char.isWhitespace).toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`
* {lean}`("coffee tea water".toSlice.splitInclusive ' ').toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`
* {lean}`("coffee tea water".toSlice.splitInclusive " tea ").toList == ["coffee tea ".toSlice, "water".toSlice]`
* {lean}`("baaab".toSlice.splitInclusive "aa").toList == ["baa".toSlice, "ab".toSlice]`
* {lean}`("coffee tea water".toSlice.splitInclusive Char.isWhitespace).allowNontermination.toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`
* {lean}`("coffee tea water".toSlice.splitInclusive ' ').allowNontermination.toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`
* {lean}`("coffee tea water".toSlice.splitInclusive " tea ").allowNontermination.toList == ["coffee tea ".toSlice, "water".toSlice]`
* {lean}`("baaab".toSlice.splitInclusive "aa").allowNontermination.toList == ["baa".toSlice, "ab".toSlice]`
-/
@[specialize pat]
def splitInclusive [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) :
Std.Iter (α := SplitInclusiveIterator ρ s) Slice :=
{ internalState := .operating s.startPos (ToForwardSearcher.toSearcher s pat) }
Std.Iter (α := SplitInclusiveIterator ρ) Slice :=
{ internalState := .operating s s.startPos (ToForwardSearcher.toSearcher s pat) }
/--
If {name}`pat` matches a prefix of {name}`s`, returns the remainder. Returns {name}`none` otherwise.
@@ -329,7 +251,7 @@ Examples:
-/
@[inline]
def dropPrefix? [ForwardPattern ρ] (s : Slice) (pat : ρ) : Option Slice :=
(ForwardPattern.dropPrefix? s pat).map s.replaceStart
ForwardPattern.dropPrefix? s pat
/--
If {name}`pat` matches a prefix of {name}`s`, returns the remainder. Returns {name}`s` unmodified
@@ -435,18 +357,18 @@ Examples:
-/
@[inline]
partial def takeWhile [ForwardPattern ρ] (s : Slice) (pat : ρ) : Slice :=
go s.startPos
go s
where
@[specialize pat]
go (curr : s.Pos) : Slice :=
if let some nextCurr := ForwardPattern.dropPrefix? (s.replaceStart curr) pat then
if (s.replaceStart curr).startPos < nextCurr then
go (curr : Slice) : Slice :=
if let some nextCurr := dropPrefix? curr pat then
if curr.startInclusive.offset < nextCurr.startInclusive.offset then
-- TODO: need lawful patterns to show this terminates
go (Pos.ofReplaceStart nextCurr)
go nextCurr
else
s.replaceEnd curr
s.replaceEnd <| s.pos! <| curr.startInclusive.offset
else
s.replaceEnd curr
s.replaceEnd <| s.pos! <| curr.startInclusive.offset
/--
Finds the position of the first match of the pattern {name}`pat` in a slice {name}`true`. If there
@@ -462,7 +384,9 @@ Examples:
@[specialize pat]
def find? [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Option s.Pos :=
let searcher := ToForwardSearcher.toSearcher s pat
searcher.findSome? (fun | .matched startPos _ => some startPos | .rejected .. => none)
match Internal.nextMatch searcher with
| some (_, startPos, _) => some startPos
| none => none
/--
Checks whether a slice has a match of the pattern {name}`pat` anywhere.
@@ -477,7 +401,7 @@ Examples:
@[specialize pat]
def contains [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Bool :=
let searcher := ToForwardSearcher.toSearcher s pat
searcher.any (· matches .matched ..)
Internal.nextMatch searcher |>.isSome
/--
Checks whether a slice only consists of matches of the pattern {name}`pat` anywhere.
@@ -491,7 +415,6 @@ Examples:
* {lean}`"brown and orange".toSlice.all Char.isLower = false`
* {lean}`"aaaaaa".toSlice.all 'a' = true`
* {lean}`"aaaaaa".toSlice.all "aa" = true`
* {lean}`"aaaaaaa".toSlice.all "aa" = false`
-/
@[inline]
def all [ForwardPattern ρ] (s : Slice) (pat : ρ) : Bool :=
@@ -522,8 +445,8 @@ Examples:
def endsWith [BackwardPattern ρ] (s : Slice) (pat : ρ) : Bool :=
BackwardPattern.endsWith s pat
inductive RevSplitIterator (ρ : Type) (s : Slice) [ToBackwardSearcher ρ σ] where
| operating (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
inductive RevSplitIterator (ρ : Type) [ToBackwardSearcher ρ σ] where
| operating (s : Slice) (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
| atEnd
deriving Inhabited
@@ -531,74 +454,37 @@ namespace RevSplitIterator
variable [ToBackwardSearcher ρ σ]
instance [Pure m] : Std.Iterators.Iterator (RevSplitIterator ρ s) m Slice where
IsPlausibleStep
| .operating _ s, .yield .operating _ s' _ => s'.IsPlausibleSuccessorOf s
| .operating _ s, .yield .atEnd .. _ => True
| .operating _ s, .skip .operating _ s' => s'.IsPlausibleSuccessorOf s
| .operating _ s, .skip .atEnd .. => False
| .operating _ s, .done => True
| .atEnd, .yield .. => False
| .atEnd, .skip _ => False
| .atEnd, .done => True
step
| .operating currPos searcher =>
match h : searcher.step with
| .yield searcher' (.matched startPos endPos), hps =>
instance [Pure m] : Std.Iterators.Iterator (RevSplitIterator ρ) m Slice where
IsPlausibleStep := fun _ _ => True
step := fun iter =>
match iter with
| .operating s currPos searcher =>
match Internal.nextMatch searcher with
| some (searcher, startPos, endPos) =>
let slice := s.replaceStartEnd! endPos currPos
let nextIt := .operating startPos searcher'
pure (.deflate .yield nextIt slice, by simp [nextIt, hps.isPlausibleSuccessor_of_yield])
| .yield searcher' (.rejected ..), hps =>
pure (.deflate .skip .operating currPos searcher',
by simp [hps.isPlausibleSuccessor_of_yield])
| .skip searcher', hps =>
pure (.deflate .skip .operating currPos searcher',
by simp [hps.isPlausibleSuccessor_of_skip])
| .done, _ =>
let nextIt := .operating s startPos searcher
pure (.deflate .yield nextIt slice, by simp)
| none =>
if currPos s.startPos then
let slice := s.replaceEnd currPos
pure (.deflate .yield .atEnd slice, by simp)
else
pure (.deflate .done, by simp)
| .atEnd => pure (.deflate .done, by simp)
| .atEnd => pure (.deflate .done, by simp)
private def toOption : RevSplitIterator ρ s Option (Std.Iter (α := σ s) (SearchStep s))
| .operating _ s => some s
| .atEnd => none
-- TODO: Finiteness after we have a notion of lawful searcher
private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
Std.Iterators.FinitenessRelation (RevSplitIterator ρ s) Id where
rel := InvImage (Option.lt Std.Iterators.Iter.IsPlausibleSuccessorOf)
(RevSplitIterator.toOption Std.Iterators.IterM.internalState)
wf := InvImage.wf _ (Option.wellFounded_lt Std.Iterators.Finite.wf_of_id)
subrelation {it it'} h := by
simp_wf
obtain step, h, h' := h
match step with
| .yield it'' out | .skip it'' =>
obtain rfl : it' = it'' := by simpa using h.symm
simp only [Std.Iterators.IterM.IsPlausibleStep, Std.Iterators.Iterator.IsPlausibleStep] at h'
revert h'
match it, it' with
| .operating _ searcher, .operating _ searcher' => simp [RevSplitIterator.toOption, Option.lt]
| .operating _ searcher, .atEnd => simp [RevSplitIterator.toOption, Option.lt]
| .atEnd, _ => simp
@[no_expose]
instance [Std.Iterators.Finite (σ s) Id] : Std.Iterators.Finite (RevSplitIterator ρ s) Id :=
.of_finitenessRelation finitenessRelation
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (RevSplitIterator ρ s) m n :=
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (RevSplitIterator ρ) m n :=
.defaultImplementation
instance [Monad m] [Monad n] :
Std.Iterators.IteratorCollectPartial (RevSplitIterator ρ s) m n :=
Std.Iterators.IteratorCollectPartial (RevSplitIterator ρ) m n :=
.defaultImplementation
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (RevSplitIterator ρ s) m n :=
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (RevSplitIterator ρ) m n :=
.defaultImplementation
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RevSplitIterator ρ s) m n :=
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RevSplitIterator ρ) m n :=
.defaultImplementation
end RevSplitIterator
@@ -614,13 +500,13 @@ This function is generic over all currently supported patterns except
{name}`String`/{name}`String.Slice`.
Examples:
* {lean}`("coffee tea water".toSlice.revSplit Char.isWhitespace).toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]`
* {lean}`("coffee tea water".toSlice.revSplit ' ').toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]`
* {lean}`("coffee tea water".toSlice.revSplit Char.isWhitespace).allowNontermination.toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]`
* {lean}`("coffee tea water".toSlice.revSplit ' ').allowNontermination.toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]`
-/
@[specialize pat]
def revSplit [ToBackwardSearcher ρ σ] (s : Slice) (pat : ρ) :
Std.Iter (α := RevSplitIterator ρ s) Slice :=
{ internalState := .operating s.endPos (ToBackwardSearcher.toSearcher s pat) }
Std.Iter (α := RevSplitIterator ρ) Slice :=
{ internalState := .operating s s.endPos (ToBackwardSearcher.toSearcher s pat) }
/--
If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`none` otherwise.
@@ -638,7 +524,7 @@ Examples:
-/
@[inline]
def dropSuffix? [BackwardPattern ρ] (s : Slice) (pat : ρ) : Option Slice :=
(BackwardPattern.dropSuffix? s pat).map s.replaceEnd
BackwardPattern.dropSuffix? s pat
/--
If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`s` unmodified
@@ -743,18 +629,18 @@ Examples:
-/
@[inline]
partial def takeEndWhile [BackwardPattern ρ] (s : Slice) (pat : ρ) : Slice :=
go s.endPos
go s
where
@[specialize pat]
go (curr : s.Pos) : Slice :=
if let some nextCurr := BackwardPattern.dropSuffix? (s.replaceEnd curr) pat then
if nextCurr < (s.replaceEnd curr).endPos then
go (curr : Slice) : Slice :=
if let some nextCurr := dropSuffix? curr pat then
if nextCurr.endExclusive.offset < curr.endExclusive.offset then
-- TODO: need lawful patterns to show this terminates
go (Pos.ofReplaceEnd nextCurr)
go nextCurr
else
s.replaceStart curr
s.replaceStart <| s.pos! <| curr.endExclusive.offset
else
s.replaceStart curr
s.replaceStart <| s.pos! <| curr.endExclusive.offset
/--
Finds the position of the first match of the pattern {name}`pat` in a slice {name}`true`, starting
@@ -772,7 +658,9 @@ Examples:
@[specialize pat]
def revFind? [ToBackwardSearcher ρ σ] (s : Slice) (pat : ρ) : Option s.Pos :=
let searcher := ToBackwardSearcher.toSearcher s pat
searcher.findSome? (fun | .matched startPos _ => some startPos | .rejected .. => none)
match Internal.nextMatch searcher with
| some (_, startPos, _) => some startPos
| none => none
end BackwardPatternUsers
@@ -809,7 +697,7 @@ where
s1Curr == s1.rawEndPos && s2Curr == s2.rawEndPos
termination_by s1.endPos.offset.byteIdx - s1Curr.byteIdx
decreasing_by
simp [String.Pos.Raw.lt_iff] at h
simp at h
omega
structure PosIterator (s : Slice) where
@@ -947,7 +835,7 @@ private def finitenessRelation [Pure m] :
· cases h
obtain h1, h2, _ := h'
have h3 := Pos.offset_prev_lt_offset (h := h1)
simp [Pos.ext_iff, String.Pos.Raw.ext_iff, String.Pos.Raw.lt_iff] at h2 h3
simp [Pos.ext_iff, String.Pos.Raw.ext_iff] at h2 h3
omega
· cases h'
· cases h
@@ -1034,7 +922,7 @@ private def finitenessRelation [Pure m] :
clear h4
generalize it'.internalState.s = s at *
cases h2
simp [String.Pos.Raw.ext_iff, String.Pos.Raw.lt_iff] at h1 h3
simp [String.Pos.Raw.ext_iff] at h1 h3
omega
· cases h'
· cases h
@@ -1099,7 +987,7 @@ instance [Pure m] : Std.Iterators.Iterator RevByteIterator m UInt8 where
if h : offset 0 then
let nextOffset := offset.dec
have hbound := by
simp [String.Pos.Raw.le_iff, nextOffset, String.Pos.Raw.lt_iff] at h hinv
simp [String.Pos.Raw.le_iff, nextOffset] at h hinv
omega
have hinv := by
simp [String.Pos.Raw.le_iff, nextOffset] at hinv
@@ -1160,9 +1048,9 @@ Creates an iterator over all lines in {name}`s` with the line ending characters
stripped.
Examples:
* {lean}`"foo\r\nbar\n\nbaz\n".toSlice.lines.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]`
* {lean}`"foo\r\nbar\n\nbaz".toSlice.lines.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]`
* {lean}`"foo\r\nbar\n\nbaz\r".toSlice.lines.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz\r".toSlice]`
* {lean}`"foo\r\nbar\n\nbaz\n".toSlice.lines.allowNontermination.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]`
* {lean}`"foo\r\nbar\n\nbaz".toSlice.lines.allowNontermination.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]`
* {lean}`"foo\r\nbar\n\nbaz\r".toSlice.lines.allowNontermination.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz\r".toSlice]`
-/
def lines (s : Slice) :=
s.splitInclusive '\n' |>.map lines.lineMap

View File

@@ -12,6 +12,6 @@ public import Init.Data.Stream
public instance : Std.Stream Substring Char where
next? s :=
if s.startPos < s.stopPos then
some (s.startPos.get s.str, { s with startPos := s.startPos.next s.str })
some (s.str.get s.startPos, { s with startPos := s.str.next s.startPos })
else
none

View File

@@ -1,521 +0,0 @@
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura, Mario Carneiro
-/
module
prelude
public import Init.Data.String.Basic
/-!
# The `Substring` type
This file contains API for `Substring` type, which is a legacy API that will be replaced by the
safer variant `String.Slice`.
-/
public section
namespace Substring
/--
Checks whether a substring is empty.
A substring is empty if its start and end positions are the same.
-/
@[inline] def isEmpty (ss : Substring) : Bool :=
ss.bsize == 0
@[export lean_substring_isempty]
def Internal.isEmptyImpl (ss : Substring) : Bool :=
Substring.isEmpty ss
/--
Copies the region of the underlying string pointed to by a substring into a fresh string.
-/
@[inline] def toString : Substring String
| s, b, e => b.extract s e
@[export lean_substring_tostring]
def Internal.toStringImpl : Substring String :=
Substring.toString
/--
Returns the character at the given position in the substring.
The position is relative to the substring, rather than the underlying string, and no bounds checking
is performed with respect to the substring's end position. If the relative position is not a valid
position in the underlying string, the fallback value `(default : Char)`, which is `'A'`, is
returned. Does not panic.
-/
@[inline] def get : Substring String.Pos.Raw Char
| s, b, _, p => (p.offsetBy b).get s
@[export lean_substring_get]
def Internal.getImpl : Substring String.Pos.Raw Char :=
Substring.get
/--
Returns the next position in a substring after the given position. If the position is at the end of
the substring, it is returned unmodified.
Both the input position and the returned position are interpreted relative to the substring's start
position, not the underlying string.
-/
@[inline] def next : Substring String.Pos.Raw String.Pos.Raw
| s, b, e, p =>
let absP := p.offsetBy b
if absP = e then p else { byteIdx := (absP.next s).byteIdx - b.byteIdx }
theorem lt_next (s : Substring) (i : String.Pos.Raw) (h : i.1 < s.bsize) :
i.1 < (s.next i).1 := by
simp [next]; rw [if_neg ?a]
case a =>
refine mt (congrArg String.Pos.Raw.byteIdx) (Nat.ne_of_lt ?_)
exact (Nat.add_comm .. Nat.add_lt_of_lt_sub h :)
apply Nat.lt_sub_of_add_lt
rw [Nat.add_comm]; apply String.Pos.Raw.lt_next
/--
Returns the previous position in a substring, just prior to the given position. If the position is
at the beginning of the substring, it is returned unmodified.
Both the input position and the returned position are interpreted relative to the substring's start
position, not the underlying string.
-/
@[inline] def prev : Substring String.Pos.Raw String.Pos.Raw
| s, b, _, p =>
let absP := p.offsetBy b
if absP = b then p else { byteIdx := (absP.prev s).byteIdx - b.byteIdx }
@[export lean_substring_prev]
def Internal.prevImpl : Substring String.Pos.Raw String.Pos.Raw :=
Substring.prev
/--
Returns the position that's the specified number of characters forward from the given position in a
substring. If the end position of the substring is reached, it is returned.
Both the input position and the returned position are interpreted relative to the substring's start
position, not the underlying string.
-/
def nextn : Substring Nat String.Pos.Raw String.Pos.Raw
| _, 0, p => p
| ss, i+1, p => ss.nextn i (ss.next p)
/--
Returns the position that's the specified number of characters prior to the given position in a
substring. If the start position of the substring is reached, it is returned.
Both the input position and the returned position are interpreted relative to the substring's start
position, not the underlying string.
-/
def prevn : Substring Nat String.Pos.Raw String.Pos.Raw
| _, 0, p => p
| ss, i+1, p => ss.prevn i (ss.prev p)
/--
Returns the first character in the substring.
If the substring is empty, but the substring's start position is a valid position in the underlying
string, then the character at the start position is returned. If the substring's start position is
not a valid position in the string, the fallback value `(default : Char)`, which is `'A'`, is
returned. Does not panic.
-/
@[inline, expose] def front (s : Substring) : Char :=
s.get 0
@[export lean_substring_front]
def Internal.frontImpl : Substring Char :=
Substring.front
/--
Returns the substring-relative position of the first occurrence of `c` in `s`, or `s.bsize` if `c`
doesn't occur.
-/
@[inline] def posOf (s : Substring) (c : Char) : String.Pos.Raw :=
match s with
| s, b, e => { byteIdx := (String.posOfAux s c e b).byteIdx - b.byteIdx }
/--
Removes the specified number of characters (Unicode code points) from the beginning of a substring
by advancing its start position.
If the substring's end position is reached, the start position is not advanced past it.
-/
@[inline] def drop : Substring Nat Substring
| ss@s, b, e, n => s, (ss.nextn n 0).offsetBy b, e
@[export lean_substring_drop]
def Internal.dropImpl : Substring Nat Substring :=
Substring.drop
/--
Removes the specified number of characters (Unicode code points) from the end of a substring
by moving its end position towards its start position.
If the substring's start position is reached, the end position is not retracted past it.
-/
@[inline] def dropRight : Substring Nat Substring
| ss@s, b, _, n => s, b, (ss.prevn n ss.bsize).offsetBy b
/--
Retains only the specified number of characters (Unicode code points) at the beginning of a
substring, by moving its end position towards its start position.
If the substring's start position is reached, the end position is not retracted past it.
-/
@[inline] def take : Substring Nat Substring
| ss@s, b, _, n => s, b, (ss.nextn n 0).offsetBy b
/--
Retains only the specified number of characters (Unicode code points) at the end of a substring, by
moving its start position towards its end position.
If the substring's end position is reached, the start position is not advanced past it.
-/
@[inline] def takeRight : Substring Nat Substring
| ss@s, b, e, n => s, (ss.prevn n ss.bsize).offsetBy b, e
/--
Checks whether a position in a substring is precisely equal to its ending position.
The position is understood relative to the substring's starting position, rather than the underlying
string's starting position.
-/
@[inline] def atEnd : Substring String.Pos.Raw Bool
| _, b, e, p => p.offsetBy b == e
/--
Returns the region of the substring delimited by the provided start and stop positions, as a
substring. The positions are interpreted with respect to the substring's start position, rather than
the underlying string.
If the resulting substring is empty, then the resulting substring is a substring of the empty string
`""`. Otherwise, the underlying string is that of the input substring with the beginning and end
positions adjusted.
-/
@[inline] def extract : Substring String.Pos.Raw String.Pos.Raw Substring
| s, b, e, b', e' => if b' e' then "", 0, 0 else s, e.min (b'.offsetBy b), e.min (e'.offsetBy b)
@[export lean_substring_extract]
def Internal.extractImpl : Substring String.Pos.Raw String.Pos.Raw Substring :=
Substring.extract
/--
Splits a substring `s` on occurrences of the separator string `sep`. The default separator is `" "`.
When `sep` is empty, the result is `[s]`. When `sep` occurs in overlapping patterns, the first match
is taken. There will always be exactly `n+1` elements in the returned list if there were `n`
non-overlapping matches of `sep` in the string. The separators are not included in the returned
substrings, which are all substrings of `s`'s string.
-/
def splitOn (s : Substring) (sep : String := " ") : List Substring :=
if sep == "" then
[s]
else
let rec loop (b i j : String.Pos.Raw) (r : List Substring) : List Substring :=
if h : i.byteIdx < s.bsize then
have := Nat.sub_lt_sub_left h (lt_next s i h)
if s.get i == j.get sep then
let i := s.next i
let j := j.next sep
if j.atEnd sep then
loop i i 0 (s.extract b (i.unoffsetBy j) :: r)
else
loop b i j r
else
loop b (s.next i) 0 r
else
let r := if j.atEnd sep then
"".toSubstring :: s.extract b (i.unoffsetBy j) :: r
else
s.extract b i :: r
r.reverse
termination_by s.bsize - i.1
loop 0 0 0 []
/--
Folds a function over a substring from the left, accumulating a value starting with `init`. The
accumulated value is combined with each character in order, using `f`.
-/
@[inline] def foldl {α : Type u} (f : α Char α) (init : α) (s : Substring) : α :=
match s with
| s, b, e => String.foldlAux f s e b init
/--
Folds a function over a substring from the right, accumulating a value starting with `init`. The
accumulated value is combined with each character in reverse order, using `f`.
-/
@[inline] def foldr {α : Type u} (f : Char α α) (init : α) (s : Substring) : α :=
match s with
| s, b, e => String.foldrAux f init s e b
/--
Checks whether the Boolean predicate `p` returns `true` for any character in a substring.
Short-circuits at the first character for which `p` returns `true`.
-/
@[inline] def any (s : Substring) (p : Char Bool) : Bool :=
match s with
| s, b, e => String.anyAux s e p b
/--
Checks whether the Boolean predicate `p` returns `true` for every character in a substring.
Short-circuits at the first character for which `p` returns `false`.
-/
@[inline] def all (s : Substring) (p : Char Bool) : Bool :=
!s.any (fun c => !p c)
@[export lean_substring_all]
def Internal.allImpl (s : Substring) (p : Char Bool) : Bool :=
Substring.all s p
/--
Checks whether a substring contains the specified character.
-/
@[inline] def contains (s : Substring) (c : Char) : Bool :=
s.any (fun a => a == c)
@[specialize] def takeWhileAux (s : String) (stopPos : String.Pos.Raw) (p : Char Bool) (i : String.Pos.Raw) : String.Pos.Raw :=
if h : i < stopPos then
if p (i.get s) then
have := Nat.sub_lt_sub_left h (String.Pos.Raw.lt_next s i)
takeWhileAux s stopPos p (i.next s)
else i
else i
termination_by stopPos.1 - i.1
/--
Retains only the longest prefix of a substring in which a Boolean predicate returns `true` for all
characters by moving the substring's end position towards its start position.
-/
@[inline] def takeWhile : Substring (Char Bool) Substring
| s, b, e, p =>
let e := takeWhileAux s e p b;
s, b, e
@[export lean_substring_takewhile]
def Internal.takeWhileImpl : Substring (Char Bool) Substring :=
Substring.takeWhile
/--
Removes the longest prefix of a substring in which a Boolean predicate returns `true` for all
characters by moving the substring's start position. The start position is moved to the position of
the first character for which the predicate returns `false`, or to the substring's end position if
the predicate always returns `true`.
-/
@[inline] def dropWhile : Substring (Char Bool) Substring
| s, b, e, p =>
let b := takeWhileAux s e p b;
s, b, e
@[specialize] def takeRightWhileAux (s : String) (begPos : String.Pos.Raw) (p : Char Bool) (i : String.Pos.Raw) : String.Pos.Raw :=
if h : begPos < i then
have := String.Pos.Raw.prev_lt_of_pos s i <| mt (congrArg String.Pos.Raw.byteIdx) <|
Ne.symm <| Nat.ne_of_lt <| Nat.lt_of_le_of_lt (Nat.zero_le _) h
let i' := i.prev s
let c := i'.get s
if !p c then i
else takeRightWhileAux s begPos p i'
else i
termination_by i.1
/--
Retains only the longest suffix of a substring in which a Boolean predicate returns `true` for all
characters by moving the substring's start position towards its end position.
-/
@[inline] def takeRightWhile : Substring (Char Bool) Substring
| s, b, e, p =>
let b := takeRightWhileAux s b p e
s, b, e
/--
Removes the longest suffix of a substring in which a Boolean predicate returns `true` for all
characters by moving the substring's end position. The end position is moved just after the position
of the last character for which the predicate returns `false`, or to the substring's start position
if the predicate always returns `true`.
-/
@[inline] def dropRightWhile : Substring (Char Bool) Substring
| s, b, e, p =>
let e := takeRightWhileAux s b p e
s, b, e
/--
Removes leading whitespace from a substring by moving its start position to the first non-whitespace
character, or to its end position if there is no non-whitespace character.
“Whitespace” is defined as characters for which `Char.isWhitespace` returns `true`.
-/
@[inline] def trimLeft (s : Substring) : Substring :=
s.dropWhile Char.isWhitespace
/--
Removes trailing whitespace from a substring by moving its end position to the last non-whitespace
character, or to its start position if there is no non-whitespace character.
“Whitespace” is defined as characters for which `Char.isWhitespace` returns `true`.
-/
@[inline] def trimRight (s : Substring) : Substring :=
s.dropRightWhile Char.isWhitespace
/--
Removes leading and trailing whitespace from a substring by first moving its start position to the
first non-whitespace character, and then moving its end position to the last non-whitespace
character.
If the substring consists only of whitespace, then the resulting substring's start position is moved
to its end position.
“Whitespace” is defined as characters for which `Char.isWhitespace` returns `true`.
Examples:
* `" red green blue ".toSubstring.trim.toString = "red green blue"`
* `" red green blue ".toSubstring.trim.startPos = ⟨1⟩`
* `" red green blue ".toSubstring.trim.stopPos = ⟨15⟩`
* `" ".toSubstring.trim.startPos = ⟨5⟩`
-/
@[inline] def trim : Substring Substring
| s, b, e =>
let b := takeWhileAux s e Char.isWhitespace b
let e := takeRightWhileAux s b Char.isWhitespace e
s, b, e
/--
Checks whether the substring can be interpreted as the decimal representation of a natural number.
A substring can be interpreted as a decimal natural number if it is not empty and all the characters
in it are digits.
Use `Substring.toNat?` to convert such a substring to a natural number.
-/
@[inline] def isNat (s : Substring) : Bool :=
!s.isEmpty && s.all fun c => c.isDigit
/--
Checks whether the substring can be interpreted as the decimal representation of a natural number,
returning the number if it can.
A substring can be interpreted as a decimal natural number if it is not empty and all the characters
in it are digits.
Use `Substring.isNat` to check whether the substring is such a substring.
-/
def toNat? (s : Substring) : Option Nat :=
if s.isNat then
some <| s.foldl (fun n c => n*10 + (c.toNat - '0'.toNat)) 0
else
none
/--
Given a `Substring`, returns another one which has valid endpoints
and represents the same substring according to `Substring.toString`.
(Note, the substring may still be inverted, i.e. beginning greater than end.)
-/
def repair : Substring Substring
| s, b, e => s, if b.isValid s then b else s.rawEndPos, if e.isValid s then e else s.rawEndPos
/--
Checks whether two substrings represent equal strings. Usually accessed via the `==` operator.
Two substrings do not need to have the same underlying string or the same start and end positions;
instead, they are equal if they contain the same sequence of characters.
-/
def beq (ss1 ss2 : Substring) : Bool :=
let ss1 := ss1.repair
let ss2 := ss2.repair
ss1.bsize == ss2.bsize && String.Pos.Raw.substrEq ss1.str ss1.startPos ss2.str ss2.startPos ss1.bsize
@[export lean_substring_beq]
def Internal.beqImpl (ss1 ss2 : Substring) : Bool :=
Substring.beq ss1 ss2
instance hasBeq : BEq Substring := beq
/--
Checks whether two substrings have the same position and content.
The two substrings do not need to have the same underlying string for this check to succeed.
-/
def sameAs (ss1 ss2 : Substring) : Bool :=
ss1.startPos == ss2.startPos && ss1 == ss2
/--
Returns the longest common prefix of two substrings.
The returned substring uses the same underlying string as `s`.
-/
def commonPrefix (s t : Substring) : Substring :=
{ s with stopPos := loop s.startPos t.startPos }
where
/-- Returns the ending position of the common prefix, working up from `spos, tpos`. -/
loop spos tpos :=
if h : spos < s.stopPos tpos < t.stopPos then
if spos.get s.str == tpos.get t.str then
have := Nat.sub_lt_sub_left h.1 (String.Pos.Raw.lt_next s.str spos)
loop (spos.next s.str) (tpos.next t.str)
else
spos
else
spos
termination_by s.stopPos.byteIdx - spos.byteIdx
/--
Returns the longest common suffix of two substrings.
The returned substring uses the same underlying string as `s`.
-/
def commonSuffix (s t : Substring) : Substring :=
{ s with startPos := loop s.stopPos t.stopPos }
where
/-- Returns the starting position of the common prefix, working down from `spos, tpos`. -/
loop spos tpos :=
if h : s.startPos < spos t.startPos < tpos then
let spos' := spos.prev s.str
let tpos' := tpos.prev t.str
if spos'.get s.str == tpos'.get t.str then
have : spos' < spos := String.Pos.Raw.prev_lt_of_pos s.str spos (String.Pos.Raw.ne_zero_of_lt h.1)
loop spos' tpos'
else
spos
else
spos
termination_by spos.byteIdx
/--
If `pre` is a prefix of `s`, returns the remainder. Returns `none` otherwise.
The substring `pre` is a prefix of `s` if there exists a `t : Substring` such that
`s.toString = pre.toString ++ t.toString`. If so, the result is the substring of `s` without the
prefix.
-/
def dropPrefix? (s : Substring) (pre : Substring) : Option Substring :=
let t := s.commonPrefix pre
if t.bsize = pre.bsize then
some { s with startPos := t.stopPos }
else
none
/--
If `suff` is a suffix of `s`, returns the remainder. Returns `none` otherwise.
The substring `suff` is a suffix of `s` if there exists a `t : Substring` such that
`s.toString = t.toString ++ suff.toString`. If so, the result the substring of `s` without the
suffix.
-/
def dropSuffix? (s : Substring) (suff : Substring) : Option Substring :=
let t := s.commonSuffix suff
if t.bsize = suff.bsize then
some { s with stopPos := t.startPos }
else
none
@[simp] theorem prev_zero (s : Substring) : s.prev 0 = 0 := by simp [prev]
@[simp] theorem prevn_zero (s : Substring) : n, s.prevn n 0 = 0
| 0 => rfl
| n+1 => by simp [prevn, prevn_zero s n]
end Substring

View File

@@ -1,314 +0,0 @@
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura, Mario Carneiro
-/
module
prelude
public import Init.Data.String.Substring
/-!
# `String.take` and variants
This file contains the implementations of `String.take` and its variants. Currently, they are
implemented in terms of `Substring`; soon, they will be implemented in terms of `String.Slice`
instead.
-/
public section
namespace String
/--
Removes the specified number of characters (Unicode code points) from the start of the string.
If `n` is greater than `s.length`, returns `""`.
Examples:
* `"red green blue".drop 4 = "green blue"`
* `"red green blue".drop 10 = "blue"`
* `"red green blue".drop 50 = ""`
-/
@[inline] def drop (s : String) (n : Nat) : String :=
(s.toSubstring.drop n).toString
@[export lean_string_drop]
def Internal.dropImpl (s : String) (n : Nat) : String :=
String.drop s n
/--
Removes the specified number of characters (Unicode code points) from the end of the string.
If `n` is greater than `s.length`, returns `""`.
Examples:
* `"red green blue".dropRight 5 = "red green"`
* `"red green blue".dropRight 11 = "red"`
* `"red green blue".dropRight 50 = ""`
-/
@[inline] def dropRight (s : String) (n : Nat) : String :=
(s.toSubstring.dropRight n).toString
@[export lean_string_dropright]
def Internal.dropRightImpl (s : String) (n : Nat) : String :=
String.dropRight s n
/--
Creates a new string that contains the first `n` characters (Unicode code points) of `s`.
If `n` is greater than `s.length`, returns `s`.
Examples:
* `"red green blue".take 3 = "red"`
* `"red green blue".take 1 = "r"`
* `"red green blue".take 0 = ""`
* `"red green blue".take 100 = "red green blue"`
-/
@[inline] def take (s : String) (n : Nat) : String :=
(s.toSubstring.take n).toString
/--
Creates a new string that contains the last `n` characters (Unicode code points) of `s`.
If `n` is greater than `s.length`, returns `s`.
Examples:
* `"red green blue".takeRight 4 = "blue"`
* `"red green blue".takeRight 1 = "e"`
* `"red green blue".takeRight 0 = ""`
* `"red green blue".takeRight 100 = "red green blue"`
-/
@[inline] def takeRight (s : String) (n : Nat) : String :=
(s.toSubstring.takeRight n).toString
/--
Creates a new string that contains the longest prefix of `s` in which `p` returns `true` for all
characters.
Examples:
* `"red green blue".takeWhile (·.isLetter) = "red"`
* `"red green blue".takeWhile (· == 'r') = "r"`
* `"red green blue".takeWhile (· != 'n') = "red gree"`
* `"red green blue".takeWhile (fun _ => true) = "red green blue"`
-/
@[inline] def takeWhile (s : String) (p : Char Bool) : String :=
(s.toSubstring.takeWhile p).toString
/--
Creates a new string by removing the longest prefix from `s` in which `p` returns `true` for all
characters.
Examples:
* `"red green blue".dropWhile (·.isLetter) = " green blue"`
* `"red green blue".dropWhile (· == 'r') = "ed green blue"`
* `"red green blue".dropWhile (· != 'n') = "n blue"`
* `"red green blue".dropWhile (fun _ => true) = ""`
-/
@[inline] def dropWhile (s : String) (p : Char Bool) : String :=
(s.toSubstring.dropWhile p).toString
/--
Creates a new string that contains the longest suffix of `s` in which `p` returns `true` for all
characters.
Examples:
* `"red green blue".takeRightWhile (·.isLetter) = "blue"`
* `"red green blue".takeRightWhile (· == 'e') = "e"`
* `"red green blue".takeRightWhile (· != 'n') = " blue"`
* `"red green blue".takeRightWhile (fun _ => true) = "red green blue"`
-/
@[inline] def takeRightWhile (s : String) (p : Char Bool) : String :=
(s.toSubstring.takeRightWhile p).toString
/--
Creates a new string by removing the longest suffix from `s` in which `p` returns `true` for all
characters.
Examples:
* `"red green blue".dropRightWhile (·.isLetter) = "red green "`
* `"red green blue".dropRightWhile (· == 'e') = "red green blu"`
* `"red green blue".dropRightWhile (· != 'n') = "red green"`
* `"red green blue".dropRightWhile (fun _ => true) = ""`
-/
@[inline] def dropRightWhile (s : String) (p : Char Bool) : String :=
(s.toSubstring.dropRightWhile p).toString
/--
Checks whether the first string (`s`) begins with the second (`pre`).
`String.isPrefix` is a version that takes the potential prefix before the string.
Examples:
* `"red green blue".startsWith "red" = true`
* `"red green blue".startsWith "green" = false`
* `"red green blue".startsWith "" = true`
* `"red".startsWith "red" = true`
-/
@[inline] def startsWith (s pre : String) : Bool :=
s.toSubstring.take pre.length == pre.toSubstring
/--
Checks whether the first string (`s`) ends with the second (`post`).
Examples:
* `"red green blue".endsWith "blue" = true`
* `"red green blue".endsWith "green" = false`
* `"red green blue".endsWith "" = true`
* `"red".endsWith "red" = true`
-/
@[inline] def endsWith (s post : String) : Bool :=
s.toSubstring.takeRight post.length == post.toSubstring
/--
Removes trailing whitespace from a string.
“Whitespace” is defined as characters for which `Char.isWhitespace` returns `true`.
Examples:
* `"abc".trimRight = "abc"`
* `" abc".trimRight = " abc"`
* `"abc \t ".trimRight = "abc"`
* `" abc ".trimRight = " abc"`
* `"abc\ndef\n".trimRight = "abc\ndef"`
-/
@[inline] def trimRight (s : String) : String :=
s.toSubstring.trimRight.toString
/--
Removes leading whitespace from a string.
“Whitespace” is defined as characters for which `Char.isWhitespace` returns `true`.
Examples:
* `"abc".trimLeft = "abc"`
* `" abc".trimLeft = " abc"`
* `"abc \t ".trimLeft = "abc \t "`
* `" abc ".trimLeft = "abc "`
* `"abc\ndef\n".trimLeft = "abc\ndef\n"`
-/
@[inline] def trimLeft (s : String) : String :=
s.toSubstring.trimLeft.toString
/--
Removes leading and trailing whitespace from a string.
“Whitespace” is defined as characters for which `Char.isWhitespace` returns `true`.
Examples:
* `"abc".trim = "abc"`
* `" abc".trim = "abc"`
* `"abc \t ".trim = "abc"`
* `" abc ".trim = "abc"`
* `"abc\ndef\n".trim = "abc\ndef"`
-/
@[inline] def trim (s : String) : String :=
s.toSubstring.trim.toString
@[export lean_string_trim]
def Internal.trimImpl (s : String) : String :=
String.trim s
/--
Repeatedly increments a position in a string, as if by `String.next`, while the predicate `p`
returns `true` for the character at the position. Stops incrementing at the end of the string or
when `p` returns `false` for the current character.
Examples:
* `let s := " a "; s.get (s.nextWhile Char.isWhitespace 0) = 'a'`
* `let s := "a "; s.get (s.nextWhile Char.isWhitespace 0) = 'a'`
* `let s := "ba "; s.get (s.nextWhile Char.isWhitespace 0) = 'b'`
-/
@[inline] def Pos.Raw.nextWhile (s : String) (p : Char Bool) (i : String.Pos.Raw) : String.Pos.Raw :=
Substring.takeWhileAux s s.rawEndPos p i
@[deprecated Pos.Raw.nextWhile (since := "2025-10-10")]
abbrev nextWhile (s : String) (p : Char Bool) (i : String.Pos.Raw) : String.Pos.Raw :=
Pos.Raw.nextWhile s p i
@[export lean_string_nextwhile]
def Internal.nextWhileImpl (s : String) (p : Char Bool) (i : String.Pos.Raw) : String.Pos.Raw :=
i.nextWhile s p
/--
Repeatedly increments a position in a string, as if by `String.next`, while the predicate `p`
returns `false` for the character at the position. Stops incrementing at the end of the string or
when `p` returns `true` for the current character.
Examples:
* `let s := " a "; s.get (s.nextUntil Char.isWhitespace 0) = ' '`
* `let s := " a "; s.get (s.nextUntil Char.isLetter 0) = 'a'`
* `let s := "a "; s.get (s.nextUntil Char.isWhitespace 0) = ' '`
-/
@[inline] def Pos.Raw.nextUntil (s : String) (p : Char Bool) (i : String.Pos.Raw) : String.Pos.Raw :=
nextWhile s (fun c => !p c) i
@[deprecated Pos.Raw.nextUntil (since := "2025-10-10")]
def nextUntil (s : String) (p : Char Bool) (i : String.Pos.Raw) : String.Pos.Raw :=
i.nextUntil s p
/--
If `pre` is a prefix of `s`, returns the remainder. Returns `none` otherwise.
The string `pre` is a prefix of `s` if there exists a `t : String` such that `s = pre ++ t`. If so,
the result is `some t`.
Use `String.stripPrefix` to return the string unchanged when `pre` is not a prefix.
Examples:
* `"red green blue".dropPrefix? "red " = some "green blue"`
* `"red green blue".dropPrefix? "reed " = none`
* `"red green blue".dropPrefix? "" = some "red green blue"`
-/
def dropPrefix? (s : String) (pre : String) : Option Substring :=
s.toSubstring.dropPrefix? pre.toSubstring
/--
If `suff` is a suffix of `s`, returns the remainder. Returns `none` otherwise.
The string `suff` is a suffix of `s` if there exists a `t : String` such that `s = t ++ suff`. If so,
the result is `some t`.
Use `String.stripSuffix` to return the string unchanged when `suff` is not a suffix.
Examples:
* `"red green blue".dropSuffix? " blue" = some "red green"`
* `"red green blue".dropSuffix? " blu " = none`
* `"red green blue".dropSuffix? "" = some "red green blue"`
-/
def dropSuffix? (s : String) (suff : String) : Option Substring :=
s.toSubstring.dropSuffix? suff.toSubstring
/--
If `pre` is a prefix of `s`, returns the remainder. Returns `s` unmodified otherwise.
The string `pre` is a prefix of `s` if there exists a `t : String` such that `s = pre ++ t`. If so,
the result is `t`. Otherwise, it is `s`.
Use `String.dropPrefix?` to return `none` when `pre` is not a prefix.
Examples:
* `"red green blue".stripPrefix "red " = "green blue"`
* `"red green blue".stripPrefix "reed " = "red green blue"`
* `"red green blue".stripPrefix "" = "red green blue"`
-/
def stripPrefix (s : String) (pre : String) : String :=
s.dropPrefix? pre |>.map Substring.toString |>.getD s
/--
If `suff` is a suffix of `s`, returns the remainder. Returns `s` unmodified otherwise.
The string `suff` is a suffix of `s` if there exists a `t : String` such that `s = t ++ suff`. If so,
the result is `t`. Otherwise, it is `s`.
Use `String.dropSuffix?` to return `none` when `suff` is not a suffix.
Examples:
* `"red green blue".stripSuffix " blue" = "red green"`
* `"red green blue".stripSuffix " blu " = "red green blue"`
* `"red green blue".stripSuffix "" = "red green blue"`
-/
def stripSuffix (s : String) (suff : String) : String :=
s.dropSuffix? suff |>.map Substring.toString |>.getD s
end String

View File

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura and Sebastian Ullrich
module
prelude
public import Init.Data.String.Substring
public import Init.Data.String.Extra
/-!
Here we give the. implementation of `Name.toString`. There is also a private implementation in
@@ -37,7 +37,7 @@ private partial def needsNoEscapeAsciiRest (s : String) (i : Nat) : Bool :=
-- If you change this, also change the corresponding function in `Init.Meta`.
@[inline] private def needsNoEscape (s : String) (h : s.utf8ByteSize > 0) : Bool :=
needsNoEscapeAscii s h || isIdFirst s.front && (s.toSubstring.drop 1).all isIdRest
needsNoEscapeAscii s h || isIdFirst (s.get 0) && (s.toSubstring.drop 1).all isIdRest
-- If you change this, also change the corresponding function in `Init.Meta`.
@[inline] private def escape (s : String) : String :=

View File

@@ -17,32 +17,13 @@ when selecting patterns.
syntax grindLemmaMin := ppGroup("!" (Attr.grindMod ppSpace)? ident)
namespace Grind
declare_syntax_cat grind_filter (behavior := both)
syntax:max ident : grind_filter
syntax:max &"gen" " < " num : grind_filter
syntax:max &"gen" " = " num : grind_filter
syntax:max &"gen" " != " num : grind_filter
syntax:max &"gen" "" num : grind_filter
syntax:max &"gen" " <= " num : grind_filter
syntax:max &"gen" " > " num : grind_filter
syntax:max &"gen" "" num : grind_filter
syntax:max &"gen" " >= " num : grind_filter
syntax:max "(" grind_filter ")" : grind_filter
syntax:35 grind_filter:35 " && " grind_filter:36 : grind_filter
syntax:35 grind_filter:35 " || " grind_filter:36 : grind_filter
syntax:max "!" grind_filter:40 : grind_filter
syntax grindFilter := (colGt grind_filter)?
/-- `grind` is the syntax category for a "grind interactive tactic".
A `grind` tactic is a program which receives a `grind` goal. -/
declare_syntax_cat grind (behavior := both)
syntax grindStep := grind ("|" (colGt ppSpace grind_filter)?)?
syntax grindSeq1Indented := sepBy1IndentSemicolon(grindStep)
syntax grindSeqBracketed := "{" withoutPosition(sepByIndentSemicolon(grindStep)) "}"
syntax grindSeq1Indented := sepBy1IndentSemicolon(grind)
syntax grindSeqBracketed := "{" withoutPosition(sepByIndentSemicolon(grind)) "}"
syntax grindSeq := grindSeqBracketed <|> grindSeq1Indented
/-- `(grindSeq)` runs the `grindSeq` in sequence on the current list of targets.
@@ -66,41 +47,49 @@ syntax (name := «sorry») "sorry" : grind
syntax anchor := "#" noWs hexnum
syntax thm := anchor <|> grindLemma <|> grindLemmaMin
/--
Instantiates theorems using E-matching.
The `approx` modifier is just a marker for users to easily identify automatically generated `instantiate` tactics
that may have redundant arguments.
-/
syntax (name := instantiate) "instantiate" (&" only")? (&" approx")? (" [" withoutPosition(thm,*,?) "]")? : grind
/-- Instantiates theorems using E-matching. -/
syntax (name := instantiate) "instantiate" (colGt thm),* : grind
declare_syntax_cat show_filter (behavior := both)
syntax:max ident : show_filter
syntax:max &"gen" " < " num : show_filter
syntax:max &"gen" " = " num : show_filter
syntax:max &"gen" " != " num : show_filter
syntax:max &"gen" "" num : show_filter
syntax:max &"gen" " <= " num : show_filter
syntax:max &"gen" " > " num : show_filter
syntax:max &"gen" "" num : show_filter
syntax:max &"gen" " >= " num : show_filter
syntax:max "(" show_filter ")" : show_filter
syntax:35 show_filter:35 " && " show_filter:36 : show_filter
syntax:35 show_filter:35 " || " show_filter:36 : show_filter
syntax:max "!" show_filter:40 : show_filter
syntax showFilter := (colGt show_filter)?
-- **Note**: Should we rename the following tactics to `trace_`?
/-- Shows asserted facts. -/
syntax (name := showAsserted) "show_asserted" ppSpace grindFilter : grind
syntax (name := showAsserted) "show_asserted" ppSpace showFilter : grind
/-- Shows propositions known to be `True`. -/
syntax (name := showTrue) "show_true" ppSpace grindFilter : grind
syntax (name := showTrue) "show_true" ppSpace showFilter : grind
/-- Shows propositions known to be `False`. -/
syntax (name := showFalse) "show_false" ppSpace grindFilter : grind
syntax (name := showFalse) "show_false" ppSpace showFilter : grind
/-- Shows equivalence classes of terms. -/
syntax (name := showEqcs) "show_eqcs" ppSpace grindFilter : grind
syntax (name := showEqcs) "show_eqcs" ppSpace showFilter : grind
/-- Show case-split candidates. -/
syntax (name := showCases) "show_cases" ppSpace grindFilter : grind
syntax (name := showSplits) "show_splits" ppSpace showFilter : grind
/-- Show `grind` state. -/
syntax (name := «showState») "show_state" ppSpace grindFilter : grind
syntax (name := «showState») "show_state" ppSpace showFilter : grind
/-- Show active local theorems and their anchors for heuristic instantiation. -/
syntax (name := showLocalThms) "show_local_thms" : grind
/--
`show_term tac` runs `tac`, then displays the generated proof in the InfoView.
-/
syntax (name := showTerm) "show_term " grindSeq : grind
syntax (name := showThms) "show_thms" : grind
declare_syntax_cat grind_ref (behavior := both)
syntax:max anchor : grind_ref
syntax term : grind_ref
syntax (name := cases) "cases " grind_ref : grind
syntax (name := casesTrace) "cases?" grindFilter : grind
syntax (name := cases) "cases " grind_ref (" with " (colGt ident)+)? : grind
/-- `done` succeeds iff there are no remaining goals. -/
syntax (name := done) "done" : grind
@@ -108,9 +97,6 @@ syntax (name := done) "done" : grind
/-- `finish` tries to close the current goal using `grind`'s default strategy -/
syntax (name := finish) "finish" : grind
/-- `finish?` tries to close the current goal using `grind`'s default strategy and suggests a tactic script. -/
syntax (name := finishTrace) "finish?" : grind
syntax (name := «have») "have" letDecl : grind
/-- Executes the given tactic block to close the current goal. -/
@@ -157,10 +143,10 @@ macro:1 x:grind tk:" <;> " y:grind:2 : grind => `(grind|
all_goals $y:grind)
/-- `first | tac | ...` runs each `tac` until one succeeds, or else fails. -/
syntax (name := first) "first " withPosition((ppDedent(ppLine) colGe "(" grindSeq ")")+) : grind
syntax (name := first) "first " withPosition((ppDedent(ppLine) colGe "| " grindSeq)+) : grind
/-- `try tac` runs `tac` and succeeds even if `tac` failed. -/
macro "try " t:grindSeq : grind => `(grind| first ($t:grindSeq) (skip))
macro "try " t:grindSeq : grind => `(grind| first | $t | skip)
/-- `fail_if_success t` fails if the tactic `t` succeeds. -/
syntax (name := failIfSuccess) "fail_if_success " grindSeq : grind
@@ -180,7 +166,7 @@ The tactic `tac` should eventually fail, otherwise `repeat tac` will run indefin
syntax "repeat " grindSeq : grind
macro_rules
| `(grind| repeat $seq:grindSeq) => `(grind| first (($seq); repeat $seq:grindSeq) (skip))
| `(grind| repeat $seq) => `(grind| first | ($seq); repeat $seq | skip)
/-- `rename_i x_1 ... x_n` renames the last `n` inaccessible names using the given names. -/
syntax (name := renameI) "rename_i" (ppSpace colGt binderIdent)+ : grind
@@ -193,10 +179,5 @@ generated `grind` tactic scripts.
-/
syntax (name := exposeNames) "expose_names" : grind
/--
`set_option opt val in tacs` (the tactic) acts like `set_option opt val` at the command level,
but it sets the option only within the tactics `tacs`. -/
syntax (name := setOption) "set_option " (ident (noWs "." noWs ident)?) ppSpace optionValue " in " grindSeq : grind
end Grind
end Lean.Parser.Tactic

View File

@@ -11,7 +11,7 @@ public import Init.System.IO -- for `MonoBind` instance
import all Init.Control.Except -- for `MonoBind` instance
import all Init.Control.StateRef -- for `MonoBind` instance
import all Init.Control.Option -- for `MonoBind` instance
import all Init.System.ST -- for `MonoBind` instance
import all Init.System.IO -- for `MonoBind` instance
public section
@@ -921,17 +921,16 @@ theorem monotone_stateTRun [PartialOrder γ]
monotone (fun (x : γ) => StateT.run (f x) s) :=
monotone_apply s _ hmono
-- TODO: axiomatize these instances (ideally without `Nonempty ε`) when EIO and friends are opaque
noncomputable instance [Nonempty ε] : CCPO (EST ε σ α) :=
-- TODO: axiomatize these instances (ideally without `Nonempty ε`) when EIO is opaque
noncomputable instance [Nonempty ε] : CCPO (EIO ε α) :=
inferInstanceAs (CCPO ((s : _) FlatOrder (.error Classical.ofNonempty (Classical.choice s))))
noncomputable instance [Nonempty ε] : MonoBind (EST ε σ) where
noncomputable instance [Nonempty ε] : MonoBind (EIO ε) where
bind_mono_left {_ _ a₁ a₂ f} h₁₂ := by
intro s
specialize h₁₂ s
change FlatOrder.rel (a₁.bind f s) (a₂.bind f s)
simp only [EST.bind]
simp only [EStateM.bind]
generalize a₁ s = a₁ at h₁₂; generalize a₂ s = a₂ at h₁₂
cases h₁₂
· exact .bot
@@ -939,23 +938,11 @@ noncomputable instance [Nonempty ε] : MonoBind (EST ε σ) where
bind_mono_right {_ _ a f₁ f₂} h₁₂ := by
intro w
change FlatOrder.rel (a.bind f₁ w) (a.bind f₂ w)
simp only [EST.bind]
simp only [EStateM.bind]
split
· apply h₁₂
· exact .refl
noncomputable instance [Nonempty α] : CCPO (ST σ α) :=
inferInstanceAs (CCPO ((s : _) FlatOrder (.mk Classical.ofNonempty (Classical.choice s))))
noncomputable instance [Nonempty α] : CCPO (BaseIO α) :=
inferInstanceAs (CCPO (ST IO.RealWorld α))
noncomputable instance [Nonempty ε] : CCPO (EIO ε α) :=
inferInstanceAs (CCPO (EST ε IO.RealWorld α))
noncomputable instance [Nonempty ε] : MonoBind (EIO ε) :=
inferInstanceAs (MonoBind (EST ε IO.RealWorld))
end mono_bind
section implication_order

View File

@@ -1550,7 +1550,7 @@ def expandInterpolatedStr (interpStr : TSyntax interpolatedStrKind) (type : Term
def getDocString (stx : TSyntax `Lean.Parser.Command.docComment) : String :=
match stx.raw[1] with
| Syntax.atom _ val => String.Internal.extract val 0 (String.Pos.Raw.Internal.sub val.rawEndPos ⟨2⟩)
| Syntax.atom _ val => String.Internal.extract val 0 (String.Pos.Raw.Internal.sub val.endPos ⟨2⟩)
| _ => ""
end TSyntax

View File

@@ -23,16 +23,6 @@ use `PUnit` in the desugaring of `do` notation, or in the pattern match compiler
universe u v w
/-- Marker for information that has been erased by the code generator. -/
unsafe axiom lcErased : Type
/-- Marker for type dependency that has been erased by the code generator. -/
unsafe axiom lcAny : Type
/-- Internal representation of `Void` in the compiler. -/
unsafe axiom lcVoid : Type
/--
The identity function. `id` takes an implicit argument `α : Sort u`
(a type in any universe), and an argument `a : α`, and returns `a`.
@@ -145,6 +135,15 @@ It can be written as an empty tuple: `()`.
-/
@[match_pattern] abbrev Unit.unit : Unit := PUnit.unit
/-- Marker for information that has been erased by the code generator. -/
unsafe axiom lcErased : Type
/-- Marker for type dependency that has been erased by the code generator. -/
unsafe axiom lcAny : Type
/-- Internal representation of `IO.RealWorld` in the compiler. -/
unsafe axiom lcRealWorld : Type
/--
Auxiliary unsafe constant used by the Compiler when erasing proofs from code.
@@ -3442,7 +3441,7 @@ Character positions (counting the Unicode code points rather than bytes) are rep
`Nat`s. Indexing a `String` by a `String.Pos.Raw` takes constant time, while character positions need to
be translated internally to byte positions, which takes linear time.
A byte position `p` is *valid* for a string `s` if `0 ≤ p ≤ s.rawEndPos` and `p` lies on a UTF-8
A byte position `p` is *valid* for a string `s` if `0 ≤ p ≤ s.endPos` and `p` lies on a UTF-8
character boundary, see `String.Pos.IsValid`.
There is another type, `String.ValidPos`, which bundles the validity predicate. Using `String.ValidPos`
@@ -3502,10 +3501,10 @@ def String.utf8ByteSize (s : @& String) : Nat :=
/--
A UTF-8 byte position that points at the end of a string, just after the last character.
* `"abc".rawEndPos = ⟨3⟩`
* `"L∃∀N".rawEndPos = ⟨8⟩`
* `"abc".endPos = ⟨3⟩`
* `"L∃∀N".endPos = ⟨8⟩`
-/
@[inline] def String.rawEndPos (s : String) : String.Pos.Raw where
@[inline] def String.endPos (s : String) : String.Pos.Raw where
byteIdx := utf8ByteSize s
/--
@@ -3514,7 +3513,7 @@ Converts a `String` into a `Substring` that denotes the entire string.
@[inline] def String.toSubstring (s : String) : Substring where
str := s
startPos := {}
stopPos := s.rawEndPos
stopPos := s.endPos
/--
Converts a `String` into a `Substring` that denotes the entire string.
@@ -3704,7 +3703,7 @@ When thinking about `f` as potential side effects, `*>` evaluates first the left
argument for their side effects, discarding the value of the left argument and returning the value
of the right argument.
For most applications, `Applicative` or `Monad` should be used rather than `SeqRight` itself.
For most applications, `Applicative` or `Monad` should be used rather than `SeqLeft` itself.
-/
class SeqRight (f : Type u Type v) : Type (max (u+1) v) where
/--

View File

@@ -7,7 +7,6 @@ module
prelude
public import Init.Data.String.Basic
import Init.Data.String.Iterator
public section
@@ -78,8 +77,8 @@ There is no guarantee that two equivalent paths normalize to the same path.
def normalize (p : FilePath) : FilePath := Id.run do
let mut p := p
-- normalize drive letter
if isWindows && p.toString.length >= 2 && p.toString.front.isLower && String.Pos.Raw.get p.toString 1 == ':' then
p := p.toString.capitalize
if isWindows && p.toString.length >= 2 && (p.toString.get 0).isLower && p.toString.get 1 == ':' then
p := p.toString.set 0 (p.toString.get 0).toUpper
-- normalize separator
unless pathSeparators.length == 1 do
p := p.toString.map fun c => if pathSeparators.contains c then pathSeparator else c
@@ -130,7 +129,7 @@ If the path is that of the root directory or the root of a drive letter, `none`
Otherwise, the path's parent directory is returned.
-/
def parent (p : FilePath) : Option FilePath :=
let extractParentPath := FilePath.mk <$> String.Pos.Raw.extract p.toString {} <$> posOfLastSep p
let extractParentPath := FilePath.mk <$> p.toString.extract {} <$> posOfLastSep p
if p.isAbsolute then
let lengthOfRootDirectory := if pathSeparators.contains p.toString.front then 1 else 3
if p.toString.length == lengthOfRootDirectory then
@@ -138,7 +137,7 @@ def parent (p : FilePath) : Option FilePath :=
none
else if posOfLastSep p == some (String.Pos.Raw.mk (lengthOfRootDirectory - 1)) then
-- `p` is a direct child of the root
some String.Pos.Raw.extract p.toString 0 lengthOfRootDirectory
some p.toString.extract 0 lengthOfRootDirectory
else
-- `p` is an absolute path with at least two subdirectories
extractParentPath
@@ -154,7 +153,7 @@ directory.
-/
def fileName (p : FilePath) : Option String :=
let lastPart := match posOfLastSep p with
| some sepPos => String.Pos.Raw.extract p.toString (sepPos + '/') p.toString.rawEndPos
| some sepPos => p.toString.extract (sepPos + '/') p.toString.endPos
| none => p.toString
if lastPart.isEmpty || lastPart == "." || lastPart == ".." then none else some lastPart
@@ -174,7 +173,7 @@ def fileStem (p : FilePath) : Option String :=
p.fileName.map fun fname =>
match fname.revPosOf '.' with
| some 0 => fname
| some pos => String.Pos.Raw.extract fname 0 pos
| some pos => fname.extract 0 pos
| none => fname
/--
@@ -193,7 +192,7 @@ def extension (p : FilePath) : Option String :=
p.fileName.bind fun fname =>
match fname.revPosOf '.' with
| some 0 => none
| some pos => some <| String.Pos.Raw.extract fname (pos + '.') fname.rawEndPos
| some pos => some <| fname.extract (pos + '.') fname.endPos
| none => none
/--
@@ -273,7 +272,7 @@ Separates the entries in the `$PATH` (or `%PATH%`) environment variable by the c
platform-dependent separator character.
-/
def parse (s : String) : SearchPath :=
s.splitToList (fun c => SearchPath.separator == c) |>.map FilePath.mk
s.split (fun c => SearchPath.separator == c) |>.map FilePath.mk
/--
Joins a list of paths into a suitable value for the current platform's `$PATH` (or `%PATH%`)

View File

@@ -1,7 +1,7 @@
/-
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich, Mac Malone, Henrik Böving
Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich, Mac Malone
-/
module
@@ -9,13 +9,14 @@ prelude
public import Init.System.IOError
public import Init.System.FilePath
public import Init.Data.Ord.UInt
import Init.Data.String.TakeDrop
public import Init.Data.String.Extra
public section
open System
opaque IO.RealWorld.nonemptyType : NonemptyType.{0}
/--
A representation of “the real world” that's used in `IO` monads to ensure that `IO` actions are not
reordered.
@@ -25,18 +26,6 @@ reordered.
instance IO.RealWorld.instNonempty : Nonempty IO.RealWorld :=
by exact IO.RealWorld.nonemptyType.property
/--
An `IO` monad that cannot throw exceptions.
-/
@[expose] def BaseIO (α : Type) := ST IO.RealWorld α
instance : Monad BaseIO := inferInstanceAs (Monad (ST IO.RealWorld))
instance : MonadFinally BaseIO := inferInstanceAs (MonadFinally (ST IO.RealWorld))
@[always_inline, inline]
def BaseIO.map (f : α β) (x : BaseIO α) : BaseIO β :=
f <$> x
/--
A monad that can have side effects on the external world or throw exceptions of type `ε`.
@@ -50,7 +39,21 @@ A monad that can have side effects on the external world or throw exceptions of
def getWorld : IO (IO.RealWorld) := get
```
-/
@[expose] def EIO (ε : Type) (α : Type) : Type := EST ε IO.RealWorld α
@[expose] def EIO (ε : Type) : Type Type := EStateM ε IO.RealWorld
instance : Monad (EIO ε) := inferInstanceAs (Monad (EStateM ε IO.RealWorld))
instance : MonadFinally (EIO ε) := inferInstanceAs (MonadFinally (EStateM ε IO.RealWorld))
instance : MonadExceptOf ε (EIO ε) := inferInstanceAs (MonadExceptOf ε (EStateM ε IO.RealWorld))
instance : OrElse (EIO ε α) := MonadExcept.orElse
instance [Inhabited ε] : Inhabited (EIO ε α) := inferInstanceAs (Inhabited (EStateM ε IO.RealWorld α))
/--
An `IO` monad that cannot throw exceptions.
-/
@[expose] def BaseIO := EIO Empty
instance : Monad BaseIO := inferInstanceAs (Monad (EIO Empty))
instance : MonadFinally BaseIO := inferInstanceAs (MonadFinally (EIO Empty))
/--
Runs a `BaseIO` action, which cannot throw an exception, in any other `EIO` monad.
@@ -61,7 +64,7 @@ lifting](lean-manual://section/lifting-monads) rather being than called explicit
@[always_inline, inline]
def BaseIO.toEIO (act : BaseIO α) : EIO ε α :=
fun s => match act s with
| .mk a s => .ok a s
| EStateM.Result.ok a s => EStateM.Result.ok a s
instance : MonadLift BaseIO (EIO ε) := BaseIO.toEIO
@@ -72,8 +75,8 @@ action that returns an `Except` value.
@[always_inline, inline]
def EIO.toBaseIO (act : EIO ε α) : BaseIO (Except ε α) :=
fun s => match act s with
| .ok a s => .mk (.ok a) s
| .error ex s => .mk (.error ex) s
| EStateM.Result.ok a s => EStateM.Result.ok (Except.ok a) s
| EStateM.Result.error ex s => EStateM.Result.ok (Except.error ex) s
/--
Handles any exception that might be thrown by an `EIO ε` action, transforming it into an
@@ -82,25 +85,8 @@ exception-free `BaseIO` action.
@[always_inline, inline]
def EIO.catchExceptions (act : EIO ε α) (h : ε BaseIO α) : BaseIO α :=
fun s => match act s with
| .ok a s => .mk a s
| .error ex s => h ex s
instance : Monad (EIO ε) := inferInstanceAs (Monad (EST ε IO.RealWorld))
instance : MonadFinally (EIO ε) := inferInstanceAs (MonadFinally (EST ε IO.RealWorld))
instance : MonadExceptOf ε (EIO ε) := inferInstanceAs (MonadExceptOf ε (EST ε IO.RealWorld))
instance : OrElse (EIO ε α) := MonadExcept.orElse
instance [Inhabited ε] : Inhabited (EIO ε α) := inferInstanceAs (Inhabited (EST ε IO.RealWorld α))
@[always_inline, inline]
def EIO.map (f : α β) (x : EIO ε α) : EIO ε β :=
f <$> x
@[always_inline, inline]
protected def EIO.throw (e : ε) : EIO ε α := throw e
@[always_inline, inline]
protected def EIO.tryCatch (x : EIO ε α) (handle : ε EIO ε α) : EIO ε α :=
MonadExceptOf.tryCatch x handle
| EStateM.Result.ok a s => EStateM.Result.ok a s
| EStateM.Result.error ex s => h ex s
/--
Converts an `Except ε` action into an `EIO ε` action.
@@ -108,21 +94,11 @@ Converts an `Except ε` action into an `EIO ε` action.
If the `Except ε` action throws an exception, then the resulting `EIO ε` action throws the same
exception. Otherwise, the value is returned.
-/
@[always_inline, inline]
def EIO.ofExcept (e : Except ε α) : EIO ε α :=
match e with
| Except.ok a => pure a
| Except.error e => throw e
@[always_inline, inline]
def EIO.adapt (f : ε ε') (m : EIO ε α) : EIO ε' α :=
fun s => match m s with
| .ok a s => .ok a s
| .error e s => .error (f e) s
@[deprecated EIO.adapt (since := "2025-09-29"), always_inline, inline]
def EIO.adaptExcept (f : ε ε') (m : EIO ε α) : EIO ε' α := EIO.adapt f m
open IO (Error) in
/--
A monad that supports arbitrary side effects and throwing exceptions of type `IO.Error`.
@@ -143,7 +119,7 @@ Converts an `EIO ε` action into an `IO` action by translating any exceptions th
`IO.Error`s using `f`.
-/
@[inline] def EIO.toIO (f : ε IO.Error) (act : EIO ε α) : IO α :=
act.adapt f
act.adaptExcept f
/--
Converts an `EIO ε` action that might throw an exception of type `ε` into an exception-free `IO`
@@ -156,7 +132,7 @@ action that returns an `Except` value.
Runs an `IO` action in some other `EIO` monad, using `f` to translate `IO` exceptions.
-/
@[inline] def IO.toEIO (f : IO.Error ε) (act : IO α) : EIO ε α :=
act.adapt f
act.adaptExcept f
/- After we inline `EState.run'`, the closed term `((), ())` is generated, where the second `()`
represents the "initial world". We don't want to cache this closed term. So, we disable
@@ -176,8 +152,8 @@ duplicate, or delete calls to this function. The side effect may even be hoisted
causing the side effect to occur at initialization time, even if it would otherwise never be called.
-/
@[noinline] unsafe def unsafeBaseIO (fn : BaseIO α) : α :=
match fn (unsafeCast Unit.unit) with
| .mk a _ => a
match fn.run (unsafeCast Unit.unit) with
| EStateM.Result.ok a _ => a
/--
Executes arbitrary side effects in a pure context, with exceptions indicated via `Except`. This a
@@ -422,7 +398,7 @@ Pauses execution for the specified number of milliseconds.
-/
opaque sleep (ms : UInt32) : BaseIO Unit :=
-- TODO: add a proper primitive for IO.sleep
fun s => dbgSleep ms fun _ => .mk () s
fun s => dbgSleep ms fun _ => EStateM.Result.ok () s
/--
Runs `act` in a separate `Task`, with priority `prio`. Because `IO` actions may throw an exception
@@ -1631,10 +1607,7 @@ the `IO` monad.
-/
abbrev Ref (α : Type) := ST.Ref IO.RealWorld α
instance : MonadLift (ST IO.RealWorld) BaseIO where
monadLift mx := fun s =>
match mx s with
| .mk s a => .mk s a
instance : MonadLift (ST IO.RealWorld) BaseIO := id
/--
Creates a new mutable reference cell that contains `a`.

View File

@@ -251,7 +251,7 @@ def mkProtocolError : UInt32 → String → IO.Error :=
def mkTimeExpired : UInt32 String IO.Error :=
timeExpired
private def downCaseFirst (s : String) : String := s.decapitalize
private def downCaseFirst (s : String) : String := s.modify 0 Char.toLower
def fopenErrorToString (gist fn : String) (code : UInt32) : Option String String
| some details => downCaseFirst gist ++ " (error code: " ++ toString code ++ ", " ++ downCaseFirst details ++ ")\n file: " ++ fn

View File

@@ -12,112 +12,24 @@ public import Init.Control.Reader
public section
opaque Void.nonemptyType (σ : Type) : NonemptyType.{0}
/--
A restricted version of `IO` in which mutable state and exceptions are the only side effects.
@[expose] def Void (σ : Type) : Type := Void.nonemptyType σ |>.type
instance Void.instNonempty : Nonempty (Void σ) :=
by exact (Void.nonemptyType σ).property
@[extern "lean_void_mk"]
opaque Void.mk (x : σ) : Void σ
structure ST.Out (σ : Type) (α : Type) where
val : α
state : Void σ
It is possible to run `EST` computations in a non-monadic context using `runEST`.
-/
@[expose] def EST (ε : Type) (σ : Type) : Type Type := EStateM ε σ
/--
A restricted version of `IO` in which mutable state is the only side effect.
It is possible to run `ST` computations in a non-monadic context using `runST`.
-/
abbrev ST (σ : Type) (α : Type) := Void σ ST.Out σ α
abbrev ST (σ : Type) := EST Empty σ
namespace ST
@[always_inline, inline]
protected def pure (x : α) : ST σ α := fun s => .mk x s
@[always_inline, inline]
protected def bind (x : ST σ α) (f : α ST σ β) : ST σ β :=
fun s =>
match x s with
| .mk x s => f x s
end ST
instance (σ : Type) : Monad (ST σ) where
pure := ST.pure
bind := ST.bind
@[always_inline]
instance : MonadFinally (ST σ) where
tryFinally' x f := fun s =>
match x s with
| .mk x s =>
match f (some x) s with
| .mk y s => .mk (x, y) s
instance {σ : Type} {α : Type} [Inhabited α] : Inhabited (ST σ α) where
default := fun s => .mk default s
inductive EST.Out (ε : Type) (σ : Type) (α : Type) where
| ok : α Void σ EST.Out ε σ α
| error : ε Void σ EST.Out ε σ α
/--
A restricted version of `IO` in which mutable state and exceptions are the only side effects.
It is possible to run `EST` computations in a non-monadic context using `runEST`.
-/
@[expose] def EST (ε : Type) (σ : Type) (α : Type) : Type := Void σ EST.Out ε σ α
namespace EST
@[always_inline, inline]
protected def pure (a : α) : EST ε σ α := fun s => .ok a s
@[always_inline, inline]
protected def bind (x : EST ε σ α) (f : α EST ε σ β) : EST ε σ β :=
fun s => match x s with
| .ok a s => f a s
| .error e s => .error e s
@[always_inline, inline]
protected def throw (e : ε) : EST ε σ α := fun s => .error e s
@[always_inline, inline]
protected def tryCatch (x : EST ε σ α) (handle : ε EST ε σ α) : EST ε σ α :=
fun s => match x s with
| .ok a s => .ok a s
| .error e s => handle e s
end EST
instance (ε σ : Type) : Monad (EST ε σ) where
pure := EST.pure
bind := EST.bind
@[always_inline]
instance : MonadFinally (EST ε σ) where
tryFinally' x f := fun s =>
let r := x s
match r with
| .ok x s =>
match f (some x) s with
| .ok y s => .ok (x, y) s
| .error e s => .error e s
| .error e s =>
match f none s with
| .ok _ s => .error e s
| .error e s => .error e s
instance (ε σ : Type) : MonadExceptOf ε (EST ε σ) where
throw := EST.throw
tryCatch := EST.tryCatch
instance {ε σ : Type} {α : Type} [Inhabited ε] : Inhabited (EST ε σ α) where
default := fun s => .error default s
instance (ε σ : Type) : Monad (EST ε σ) := inferInstanceAs (Monad (EStateM _ _))
instance (ε σ : Type) : MonadExceptOf ε (EST ε σ) := inferInstanceAs (MonadExceptOf ε (EStateM _ _))
instance {ε σ : Type} {α : Type} [Inhabited ε] : Inhabited (EST ε σ α) := inferInstanceAs (Inhabited (EStateM _ _ _))
instance (σ : Type) : Monad (ST σ) := inferInstanceAs (Monad (EST _ _))
/--
An auxiliary class used to infer the “state” of `EST` and `ST` monads.
@@ -125,7 +37,6 @@ An auxiliary class used to infer the “state” of `EST` and `ST` monads.
class STWorld (σ : outParam Type) (m : Type Type)
instance {σ m n} [MonadLift m n] [STWorld σ m] : STWorld σ n :=
instance {σ} : STWorld σ (ST σ) :=
instance {ε σ} : STWorld σ (EST ε σ) :=
/--
@@ -133,22 +44,24 @@ Runs an `EST` computation, in which mutable state and exceptions are the only si
-/
@[noinline, nospecialize]
def runEST {ε α : Type} (x : (σ : Type) EST ε σ α) : Except ε α :=
match x Unit (Void.mk ()) with
| .ok a _ => Except.ok a
| .error ex _ => Except.error ex
match x Unit () with
| EStateM.Result.ok a _ => Except.ok a
| EStateM.Result.error ex _ => Except.error ex
/--
Runs an `ST` computation, in which mutable state via `ST.Ref` is the only side effect.
-/
@[noinline, nospecialize]
def runST {α : Type} (x : (σ : Type) ST σ α) : α :=
match x Unit (Void.mk ()) with
| .mk a _ => a
match x Unit () with
| EStateM.Result.ok a _ => a
| EStateM.Result.error ex _ => nomatch ex
@[always_inline]
instance {ε σ} : MonadLift (ST σ) (EST ε σ) := fun x s =>
match x s with
| .mk a s => .ok a s
| EStateM.Result.ok a s => EStateM.Result.ok a s
| EStateM.Result.error ex _ => nomatch ex
namespace ST

View File

@@ -8,7 +8,6 @@ module
prelude
public import Init.Data.String.Extra
public import Init.System.FilePath
import Init.Data.String.TakeDrop
public section
@@ -94,8 +93,8 @@ def pathToUri (fname : System.FilePath) : String := Id.run do
if System.Platform.isWindows then
-- normalize drive letter
-- lower-case drive letters seem to be preferred in URIs
if uri.length >= 2 && uri.front.isUpper && String.Pos.Raw.get uri 1 == ':' then
uri := uri.decapitalize
if uri.length >= 2 && (uri.get 0).isUpper && uri.get 1 == ':' then
uri := uri.set 0 (uri.get 0).toLower
uri := uri.map (fun c => if c == '\\' then '/' else c)
uri := uri.foldl (fun s c => s ++ UriEscape.uriEscapeAsciiChar c) ""
let result := if uri.startsWith "/" then "file://" ++ uri else "file:///" ++ uri
@@ -111,9 +110,9 @@ def fileUriToPath? (uri : String) : Option System.FilePath := Id.run do
p := p.dropWhile (λ c => c != '/') -- drop the hostname.
-- On Windows, the path "/c:/temp" needs to become "C:/temp"
if System.Platform.isWindows && p.length >= 2 &&
p.front == '/' && (String.Pos.Raw.get p 1).isAlpha && String.Pos.Raw.get p 2 == ':' then
p.get 0 == '/' && (p.get 1).isAlpha && p.get 2 == ':' then
-- see also `pathToUri`
p := String.Pos.Raw.modify (p.drop 1) 0 .toUpper
p := p.drop 1 |>.modify 0 .toUpper
some p
end Uri

View File

@@ -35,7 +35,7 @@ private def isNamespaceName : Name → Bool
private def registerNamePrefixes (env : Environment) (name : Name) : Environment :=
match name with
| .str _ s =>
if s.front == '_' then
if s.get 0 == '_' then
-- Do not register namespaces that only contain internal declarations.
env
else
@@ -96,17 +96,13 @@ def warnIfUsesSorry (decl : Declaration) : CoreM Unit := do
-- This case should not happen, but it ensures a warning will get logged no matter what.
logWarning <| .tagged `hasSorry m!"declaration uses 'sorry'"
builtin_initialize
registerTraceClass `addDecl
/--
Adds the given declaration to the environment's private scope, deriving a suitable presentation in
the public scope if under the module system and if the declaration is not private. If `forceExpose`
is true, exposes the declaration body, i.e. preserves the full representation in the public scope,
independently of `Environment.isExporting` and even for theorems.
-/
def addDecl (decl : Declaration) (forceExpose := false) : CoreM Unit :=
withTraceNode `addDecl (fun _ => return m!"adding declarations {decl.getNames}") do
def addDecl (decl : Declaration) (forceExpose := false) : CoreM Unit := do
-- register namespaces for newly added constants; this used to be done by the kernel itself
-- but that is incompatible with moving it to a separate task
-- NOTE: we do not use `getTopLevelNames` here so that inductive types are registered as
@@ -119,37 +115,26 @@ def addDecl (decl : Declaration) (forceExpose := false) : CoreM Unit :=
let (name, info, kind) match decl with
| .thmDecl thm =>
if !forceExpose && ( getEnv).header.isModule then
trace[addDecl] "exporting theorem {thm.name} as axiom"
exportedInfo? := some <| .axiomInfo { thm with isUnsafe := false }
pure (thm.name, .thmInfo thm, .thm)
| .defnDecl defn | .mutualDefnDecl [defn] =>
if !forceExpose && ( getEnv).header.isModule && !( getEnv).isExporting then
trace[addDecl] "exporting definition {defn.name} as axiom"
exportedInfo? := some <| .axiomInfo { defn with isUnsafe := defn.safety == .unsafe }
pure (defn.name, .defnInfo defn, .defn)
| .opaqueDecl op =>
if !forceExpose && ( getEnv).header.isModule && !( getEnv).isExporting then
trace[addDecl] "exporting opaque {op.name} as axiom"
exportedInfo? := some <| .axiomInfo { op with }
pure (op.name, .opaqueInfo op, .opaque)
| .axiomDecl ax => pure (ax.name, .axiomInfo ax, .axiom)
| _ =>
trace[addDecl] "no matching async adding rules, adding synchronously"
return ( doAdd)
| _ => return ( doAdd)
if decl.getTopLevelNames.all isPrivateName then
if ( ResolveName.backward.privateInPublic.getM) then
trace[addDecl] "private decl under `privateInPublic`, exporting as is"
exportedInfo? := some info
else
trace[addDecl] "not exporting private declaration at all"
exportedInfo? := none
if decl.getTopLevelNames.all isPrivateName && !( ResolveName.backward.privateInPublic.getM) then
exportedInfo? := none
else
-- preserve original constant kind in extension if different from exported one
if exportedInfo?.isSome then
modifyEnv (privateConstKindsExt.insert · name kind)
else
trace[addDecl] "no matching exporting rules, exporting as is"
exportedInfo? := some info
-- no environment extension changes to report after kernel checking; ensures we do not

View File

@@ -148,14 +148,11 @@ def throwAttrDeclNotOfExpectedType (attrName declName : Name) (givenType expecte
throwError m!"Cannot add attribute `[{attrName}]`: Declaration `{.ofConstName declName}` has type{indentExpr givenType}\n\
but `[{attrName}]` can only be added to declarations of type{indentExpr expectedType}"
def ensureAttrDeclIsPublic (attrName declName : Name) (attrKind : AttributeKind) : AttrM Unit := do
if ( getEnv).header.isModule && attrKind != .local then
withExporting do
checkPrivateInPublic declName
if !( hasConst declName) then
throwError m!"Cannot add attribute `[{attrName}]`: Declaration `{.ofConstName declName}` must be public"
def ensureAttrDeclIsPublic [MonadEnv m] (attrName declName : Name) (attrKind : AttributeKind) : m Unit := do
if ( getEnv).header.isModule && attrKind != .local && !(( getEnv).setExporting true).contains declName then
throwError m!"Cannot add attribute `[{attrName}]`: Declaration `{.ofConstName declName}` must be public"
def ensureAttrDeclIsMeta (attrName declName : Name) (attrKind : AttributeKind) : AttrM Unit := do
def ensureAttrDeclIsMeta [MonadEnv m] (attrName declName : Name) (attrKind : AttributeKind) : m Unit := do
if ( getEnv).header.isModule && !isMeta ( getEnv) declName then
throwError m!"Cannot add attribute `[{attrName}]`: Declaration `{.ofConstName declName}` must be marked as `meta`"
-- Make sure attributed decls can't refer to private meta imports, which is already checked for

View File

@@ -7,7 +7,6 @@ module
prelude
public import Lean.EnvExtension
import Init.Data.String.TakeDrop
public section

View File

@@ -13,7 +13,7 @@ public section
namespace Lean
private def isValidCppId (id : String) : Bool :=
let first := id.front;
let first := id.get 0;
first.isAlpha && (id.toSubstring.drop 1).all (fun c => c.isAlpha || c.isDigit || c == '_')
private def isValidCppName : Name Bool

View File

@@ -7,7 +7,7 @@ module
prelude
public import Lean.ProjFns
public import Lean.Attributes
public import Lean.Meta.Basic
public section

View File

@@ -51,9 +51,6 @@ instance : ToString JoinPointId := ⟨fun a => "block_" ++ toString a.idx⟩
- `tobject` an `object` or a `tagged` pointer
- `void` is used to identify uses of the state token from `BaseIO` which do no longer need
to be passed around etc. at this point in the pipeline.
- `struct` and `union` are used to return small values (e.g., `Option`, `Prod`, `Except`)
on the stack.
@@ -81,7 +78,6 @@ inductive IRType where
| union (leanTypeName : Name) (types : Array IRType) : IRType
-- TODO: Move this upwards after a stage0 update.
| tagged
| void
deriving Inhabited, BEq, Repr
namespace IRType
@@ -100,7 +96,6 @@ def isObj : IRType → Bool
| object => true
| tagged => true
| tobject => true
| void => true
| _ => false
def isPossibleRef : IRType Bool
@@ -115,13 +110,9 @@ def isErased : IRType → Bool
| erased => true
| _ => false
def isVoid : IRType Bool
| void => true
| _ => false
def boxed : IRType IRType
| object | float | float32 => object
| void | tagged | uint8 | uint16 => tagged
| tagged | uint8 | uint16 => tagged
| _ => tobject
end IRType

View File

@@ -39,7 +39,7 @@ private def N.mkFresh : N VarId :=
def requiresBoxedVersion (env : Environment) (decl : Decl) : Bool :=
let ps := decl.params
(ps.size > 0 && (decl.resultType.isScalar || ps.any (fun p => p.ty.isScalar || p.borrow || p.ty.isVoid) || isExtern env decl.name))
(ps.size > 0 && (decl.resultType.isScalar || ps.any (fun p => p.ty.isScalar || p.borrow) || isExtern env decl.name))
|| ps.size > closureMaxArgs
def mkBoxedVersionAux (decl : Decl) : N Decl := do

View File

@@ -15,7 +15,7 @@ public import Lean.Compiler.IR.Boxing
public section
namespace Lean.IR.EmitC
open ExplicitBoxing (isBoxedName)
open ExplicitBoxing (requiresBoxedVersion mkBoxedName isBoxedName)
def leanMainFn := "_lean_main"
@@ -65,7 +65,6 @@ def toCType : IRType → String
| IRType.tagged => "lean_object*"
| IRType.tobject => "lean_object*"
| IRType.erased => "lean_object*"
| IRType.void => "lean_object*"
| IRType.struct _ _ => panic! "not implemented yet"
| IRType.union _ _ => panic! "not implemented yet"
@@ -106,8 +105,6 @@ def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M U
emit (toCType decl.resultType ++ " " ++ cppBaseName)
unless ps.isEmpty do
emit "("
-- We omit void parameters, note that they are guaranteed not to occur in boxed functions
let ps := ps.filter (fun p => !p.ty.isVoid)
-- We omit erased parameters for extern constants
let ps := if isExternC env decl.name then ps.filter (fun p => !p.ty.isErased) else ps
if ps.size > closureMaxArgs && isBoxedName decl.name then
@@ -172,7 +169,7 @@ def emitMainFn : M Unit := do
/- We disable panic messages because they do not mesh well with extracted closed terms.
See issue #534. We can remove this workaround after we implement issue #467. -/
emitLn "lean_set_panic_messages(false);"
emitLn ("res = " ++ mkModuleInitializationFunctionName modName ++ "(1 /* builtin */);")
emitLn ("res = " ++ mkModuleInitializationFunctionName modName ++ "(1 /* builtin */, lean_io_mk_world());")
emitLn "lean_set_panic_messages(true);"
emitLns ["lean_io_mark_end_initialization();",
"if (lean_io_result_is_ok(res)) {",
@@ -187,9 +184,9 @@ def emitMainFn : M Unit := do
" n = lean_alloc_ctor(1,2,0); lean_ctor_set(n, 0, lean_mk_string(argv[i])); lean_ctor_set(n, 1, in);",
" in = n;",
"}"]
emitLn ("res = " ++ leanMainFn ++ "(in);")
emitLn ("res = " ++ leanMainFn ++ "(in, lean_io_mk_world());")
else
emitLn ("res = " ++ leanMainFn ++ "();")
emitLn ("res = " ++ leanMainFn ++ "(lean_io_mk_world());")
emitLn "}"
-- `IO _`
let retTy := env.find? `main |>.get! |>.type |>.getForallBody
@@ -412,8 +409,7 @@ def emitSimpleExternalCall (f : String) (ps : Array Param) (ys : Array Arg) : M
-- We must remove erased arguments to extern calls.
discard <| ys.size.foldM
(fun i _ (first : Bool) =>
let ty := ps[i]!.ty
if ty.isErased || ty.isVoid then
if ps[i]!.ty.isErased then
pure first
else do
unless first do emit ", "
@@ -433,11 +429,9 @@ def emitFullApp (z : VarId) (f : FunId) (ys : Array Arg) : M Unit := do
emitLhs z
let decl getDecl f
match decl with
| .fdecl (xs := ps) .. | .extern (xs := ps) (ext := { entries := [.opaque _], .. }) .. =>
| .fdecl .. | .extern _ _ _ { entries := [.opaque _], .. } =>
emitCName f
if ys.size > 0 then
let (ys, _) := ys.zip ps |>.filter (fun (_, p) => !p.ty.isVoid) |>.unzip
emit "("; emitArgs ys; emit ")"
if ys.size > 0 then emit "("; emitArgs ys; emit ")"
emitLn ";"
| Decl.extern _ ps _ extData => emitExternCall f ps extData ys
@@ -577,23 +571,22 @@ def emitTailCall (v : Expr) : M Unit :=
let ctx read
let ps := ctx.mainParams
if h : ps.size = ys.size then
let (ps, ys) := ps.zip ys |>.filter (fun (p, _) => !p.ty.isVoid) |>.unzip
if overwriteParam ps ys then
emitLn "{"
ps.size.forM fun i _ => do
let p := ps[i]
let y := ys[i]!
let y := ys[i]
unless paramEqArg p y do
emit (toCType p.ty); emit " _tmp_"; emit i; emit " = "; emitArg y; emitLn ";"
ps.size.forM fun i _ => do
let p := ps[i]
let y := ys[i]!
let y := ys[i]
unless paramEqArg p y do emit p.x; emit " = _tmp_"; emit i; emitLn ";"
emitLn "}"
else
ps.size.forM fun i _ => do
ys.size.forM fun i _ => do
let p := ps[i]
let y := ys[i]!
let y := ys[i]
unless paramEqArg p y do emit p.x; emit " = "; emitArg y; emitLn ";"
emitLn "goto _start;"
else
@@ -674,7 +667,6 @@ def emitDeclAux (d : Decl) : M Unit := do
emit "LEAN_EXPORT " -- make symbol visible to the interpreter
emit (toCType t); emit " ";
if xs.size > 0 then
let xs := xs.filter (fun p => !p.ty.isVoid)
emit baseName;
emit "(";
if xs.size > closureMaxArgs && isBoxedName d.name then
@@ -721,7 +713,7 @@ def emitDeclInit (d : Decl) : M Unit := do
if isIOUnitInitFn env n then
if isIOUnitBuiltinInitFn env n then
emit "if (builtin) {"
emit "res = "; emitCName n; emitLn "();"
emit "res = "; emitCName n; emitLn "(lean_io_mk_world());"
emitLn "if (lean_io_result_is_error(res)) return res;"
emitLn "lean_dec_ref(res);"
if isIOUnitBuiltinInitFn env n then
@@ -731,7 +723,7 @@ def emitDeclInit (d : Decl) : M Unit := do
| some initFn =>
if getBuiltinInitFnNameFor? env d.name |>.isSome then
emit "if (builtin) {"
emit "res = "; emitCName initFn; emitLn "();"
emit "res = "; emitCName initFn; emitLn "(lean_io_mk_world());"
emitLn "if (lean_io_result_is_error(res)) return res;"
emitCName n
if d.resultType.isScalar then
@@ -748,16 +740,16 @@ def emitDeclInit (d : Decl) : M Unit := do
def emitInitFn : M Unit := do
let env getEnv
let modName getModName
env.imports.forM fun imp => emitLn ("lean_object* " ++ mkModuleInitializationFunctionName imp.module ++ "(uint8_t builtin);")
env.imports.forM fun imp => emitLn ("lean_object* " ++ mkModuleInitializationFunctionName imp.module ++ "(uint8_t builtin, lean_object*);")
emitLns [
"static bool _G_initialized = false;",
"LEAN_EXPORT lean_object* " ++ mkModuleInitializationFunctionName modName ++ "(uint8_t builtin) {",
"LEAN_EXPORT lean_object* " ++ mkModuleInitializationFunctionName modName ++ "(uint8_t builtin, lean_object* w) {",
"lean_object * res;",
"if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));",
"_G_initialized = true;"
]
env.imports.forM fun imp => emitLns [
"res = " ++ mkModuleInitializationFunctionName imp.module ++ "(builtin);",
"res = " ++ mkModuleInitializationFunctionName imp.module ++ "(builtin, lean_io_mk_world());",
"if (lean_io_result_is_error(res)) return res;",
"lean_dec_ref(res);"]
let decls := getDecls env

View File

@@ -19,18 +19,6 @@ public section
open Lean.IR.ExplicitBoxing (isBoxedName)
namespace Lean.IR
/-
TODO: At the time of writing this our CI for LLVM is dysfunctional so this code is not actually
tested. When we get back to fixing it we need to account for changes made to the ABI in the mean
time. These changes can likely be done similar to the ones in EmitC:
- IO.RealWorld elimination:
- init functions don't take a real world parameter anymore
- parameters that are `void` are erased and do not appear in function signatures or call sites
anymore. This means in particular:
- function decls need to be fixed
- full applications need to be fixed
- tail calls need to be fixed
-/
def leanMainFn := "_lean_main"
@@ -337,7 +325,6 @@ def toLLVMType (t : IRType) : M llvmctx (LLVM.LLVMType llvmctx) := do
| IRType.tagged => do LLVM.pointerType ( LLVM.i8Type llvmctx)
| IRType.tobject => do LLVM.pointerType ( LLVM.i8Type llvmctx)
| IRType.erased => do LLVM.pointerType ( LLVM.i8Type llvmctx)
| IRType.void => do LLVM.pointerType ( LLVM.i8Type llvmctx)
| IRType.struct _ _ => panic! "not implemented yet"
| IRType.union _ _ => panic! "not implemented yet"

View File

@@ -66,7 +66,6 @@ private partial def formatIRType : IRType → Format
| IRType.uint64 => "u64"
| IRType.usize => "usize"
| IRType.erased => ""
| IRType.void => "void"
| IRType.object => "obj"
| IRType.tagged => "tagged"
| IRType.tobject => "tobj"

View File

@@ -14,8 +14,7 @@ public section
namespace Lean.IR
open Lean.Compiler (LCNF.Alt LCNF.Arg LCNF.Code LCNF.Decl LCNF.DeclValue LCNF.LCtx LCNF.LetDecl
LCNF.LetValue LCNF.LitValue LCNF.Param LCNF.getMonoDecl? LCNF.FVarSubst LCNF.MonadFVarSubst
LCNF.MonadFVarSubstState LCNF.addSubst LCNF.normLetValue LCNF.normFVar)
LCNF.LetValue LCNF.LitValue LCNF.Param LCNF.getMonoDecl?)
namespace ToIR
@@ -23,32 +22,14 @@ structure BuilderState where
vars : Std.HashMap FVarId Arg := {}
joinPoints : Std.HashMap FVarId JoinPointId := {}
nextId : Nat := 1
/--
We keep around a substitution here because we run a second trivial structure elimination when
converting to IR. This elimination is aware of the fact that `Void` is irrelevant while the first
one in LCNF isn't because LCNF is still pure. However, IR does not allow us to have bindings of
the form `let x := y` which might occur when for example projecting out of a trivial structure
where previously a binding would've been `let x := proj y i` and now becomes `let x := y`.
For this reason we carry around these kinds of bindings in this substitution and apply it whenever
we access an fvar in the conversion.
-/
subst : LCNF.FVarSubst := {}
abbrev M := StateRefT BuilderState CoreM
instance : LCNF.MonadFVarSubst M false where
getSubst := return ( get).subst
instance : LCNF.MonadFVarSubstState M where
modifySubst f := modify fun s => { s with subst := f s.subst }
def M.run (x : M α) : CoreM α := do
x.run' {}
def getFVarValue (fvarId : FVarId) : M Arg := do
match LCNF.normFVar fvarId with
| .fvar fvarId => return ( get).vars.get! fvarId
| .erased => return .erased
return ( get).vars.get! fvarId
def getJoinPointValue (fvarId : FVarId) : M JoinPointId := do
return ( get).joinPoints.get! fvarId
@@ -111,13 +92,10 @@ def lowerProj (base : VarId) (ctorInfo : CtorInfo) (field : CtorFieldInfo)
| .usize i => .expr (.uproj i base), .usize
| .scalar _ offset irType => .expr (.sproj (ctorInfo.size + ctorInfo.usize) offset base), irType
| .erased => .erased, .erased
| .void => .erased, .void
def lowerParam (p : LCNF.Param) : M Param := do
let x bindVar p.fvarId
let ty toIRType p.type
if ty.isVoid || ty.isErased then
Compiler.LCNF.addSubst p.fvarId .erased
return { x, borrow := p.borrow, ty }
mutual
@@ -133,61 +111,40 @@ partial def lowerCode (c : LCNF.Code) : M FnBody := do
let joinPointId getJoinPointValue fvarId
return .jmp joinPointId ( args.mapM lowerArg)
| .cases cases =>
if let some info hasTrivialStructure? cases.typeName then
assert! cases.alts.size == 1
let .alt ctorName ps k := cases.alts[0]! | unreachable!
assert! ctorName == info.ctorName
assert! info.fieldIdx < ps.size
for idx in 0...ps.size do
let p := ps[idx]!
if idx == info.fieldIdx then
LCNF.addSubst p.fvarId (.fvar cases.discr)
else
bindErased p.fvarId
lowerCode k
else
-- `casesOn` for inductive predicates should have already been expanded.
let .var varId := ( getFVarValue cases.discr) | unreachable!
return .case cases.typeName
varId
( nameToIRType cases.typeName)
( cases.alts.mapM (lowerAlt varId))
-- `casesOn` for inductive predicates should have already been expanded.
let .var varId := ( getFVarValue cases.discr) | unreachable!
return .case cases.typeName
varId
( nameToIRType cases.typeName)
( cases.alts.mapM (lowerAlt varId))
| .return fvarId =>
return .ret ( getFVarValue fvarId)
| .unreach .. => return .unreachable
| .fun .. => panic! "all local functions should be λ-lifted"
partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
let value LCNF.normLetValue decl.value
match value with
match decl.value with
| .lit litValue =>
let var bindVar decl.fvarId
let litValue, type := lowerLitValue litValue
return .vdecl var type (.lit litValue) ( lowerCode k)
| .proj typeName i fvarId =>
if let some info hasTrivialStructure? typeName then
if info.fieldIdx == i then
LCNF.addSubst decl.fvarId (.fvar fvarId)
else
bindErased decl.fvarId
lowerCode k
else
match ( getFVarValue fvarId) with
| .var varId =>
let some (.inductInfo { ctors := [ctorName], .. }) := ( Lean.getEnv).find? typeName
| panic! "projection of non-structure type"
let ctorInfo, fields getCtorLayout ctorName
let result, type := lowerProj varId ctorInfo fields[i]!
match result with
| .expr e =>
let var bindVar decl.fvarId
return .vdecl var type e ( lowerCode k)
| .erased =>
bindErased decl.fvarId
lowerCode k
match ( getFVarValue fvarId) with
| .var varId =>
let some (.inductInfo { ctors := [ctorName], .. }) := ( Lean.getEnv).find? typeName
| panic! "projection of non-structure type"
let ctorInfo, fields getCtorLayout ctorName
let result, type := lowerProj varId ctorInfo fields[i]!
match result with
| .expr e =>
let var bindVar decl.fvarId
return .vdecl var type e ( lowerCode k)
| .erased =>
bindErased decl.fvarId
lowerCode k
| .erased =>
bindErased decl.fvarId
lowerCode k
| .const name _ args =>
let irArgs args.mapM lowerArg
if let some decl findDecl name then
@@ -197,48 +154,43 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
let env Lean.getEnv
match env.find? name with
| some (.ctorInfo ctorVal) =>
if let some info hasTrivialStructure? ctorVal.induct then
let arg := args[info.numParams + info.fieldIdx]!
LCNF.addSubst decl.fvarId arg
lowerCode k
else
let type nameToIRType ctorVal.induct
if type.isScalar then
let var bindVar decl.fvarId
return .vdecl var type (.lit (.num ctorVal.cidx)) ( lowerCode k)
let type nameToIRType ctorVal.induct
if type.isScalar then
let var bindVar decl.fvarId
return .vdecl var type (.lit (.num ctorVal.cidx)) ( lowerCode k)
let ctorInfo, fields getCtorLayout name
let irArgs := irArgs.extract (start := ctorVal.numParams)
if irArgs.size != fields.size then
-- An overapplied constructor arises from compiler
-- transformations on unreachable code
return .unreachable
let ctorInfo, fields getCtorLayout name
let irArgs := irArgs.extract (start := ctorVal.numParams)
if irArgs.size != fields.size then
-- An overapplied constructor arises from compiler
-- transformations on unreachable code
return .unreachable
let objArgs : Array Arg do
let mut result : Array Arg := #[]
for h : i in *...fields.size do
match fields[i] with
| .object .. =>
result := result.push irArgs[i]!
| .usize .. | .scalar .. | .erased | .void => pure ()
pure result
let objVar bindVar decl.fvarId
let rec lowerNonObjectFields (_ : Unit) : M FnBody :=
let rec loop (i : Nat) : M FnBody := do
match irArgs[i]? with
| some (.var varId) =>
match fields[i]! with
| .usize usizeIdx =>
let k loop (i + 1)
return .uset objVar usizeIdx varId k
| .scalar _ offset argType =>
let k loop (i + 1)
return .sset objVar (ctorInfo.size + ctorInfo.usize) offset varId argType k
| .object .. | .erased | .void => loop (i + 1)
| some .erased => loop (i + 1)
| none => lowerCode k
loop 0
return .vdecl objVar ctorInfo.type (.ctor ctorInfo objArgs) ( lowerNonObjectFields ())
let objArgs : Array Arg do
let mut result : Array Arg := #[]
for h : i in *...fields.size do
match fields[i] with
| .object .. =>
result := result.push irArgs[i]!
| .usize .. | .scalar .. | .erased => pure ()
pure result
let objVar bindVar decl.fvarId
let rec lowerNonObjectFields (_ : Unit) : M FnBody :=
let rec loop (i : Nat) : M FnBody := do
match irArgs[i]? with
| some (.var varId) =>
match fields[i]! with
| .usize usizeIdx =>
let k loop (i + 1)
return .uset objVar usizeIdx varId k
| .scalar _ offset argType =>
let k loop (i + 1)
return .sset objVar (ctorInfo.size + ctorInfo.usize) offset varId argType k
| .object .. | .erased => loop (i + 1)
| some .erased => loop (i + 1)
| none => lowerCode k
loop 0
return .vdecl objVar ctorInfo.type (.ctor ctorInfo objArgs) ( lowerNonObjectFields ())
| some (.defnInfo ..) | some (.opaqueInfo ..) =>
mkFap name irArgs
| some (.axiomInfo ..) | .some (.quotInfo ..) | .some (.inductInfo ..) | .some (.thmInfo ..) =>

View File

@@ -14,9 +14,7 @@ public section
namespace Lean
namespace IR
open Lean.Compiler (LCNF.CacheExtension LCNF.isTypeFormerType LCNF.toLCNFType LCNF.toMonoType
LCNF.TrivialStructureInfo LCNF.getOtherDeclBaseType LCNF.getParamTypes LCNF.instantiateForall
LCNF.Irrelevant.hasTrivialStructure?)
open Lean.Compiler (LCNF.CacheExtension LCNF.isTypeFormerType LCNF.toLCNFType LCNF.toMonoType)
def irTypeForEnum (numCtors : Nat) : IRType :=
if numCtors == 1 then
@@ -33,23 +31,6 @@ def irTypeForEnum (numCtors : Nat) : IRType :=
builtin_initialize irTypeExt : LCNF.CacheExtension Name IRType
LCNF.CacheExtension.register
builtin_initialize trivialStructureInfoExt :
LCNF.CacheExtension Name (Option LCNF.TrivialStructureInfo)
LCNF.CacheExtension.register
/--
The idea of this function is the same as in `ToMono`, however the notion of "irrelevancy" has
changed because we now have the `void` type which can only be erased in impure context and thus at
earliest at the conversion from mono to IR.
-/
def hasTrivialStructure? (declName : Name) : CoreM (Option LCNF.TrivialStructureInfo) := do
let isVoidType type := do
let type Meta.whnfD type
return type matches .proj ``Subtype 0 (.app (.const ``Void.nonemptyType []) _)
let irrelevantType type :=
Meta.isProp type <||> Meta.isTypeFormerType type <||> isVoidType type
LCNF.Irrelevant.hasTrivialStructure? trivialStructureInfoExt irrelevantType declName
def nameToIRType (name : Name) : CoreM IRType := do
match ( irTypeExt.find? name) with
| some type => return type
@@ -70,7 +51,7 @@ where fillCache : CoreM IRType := do
-- `Int` is specified as an inductive type with two constructors that have relevant arguments,
-- but it has the same runtime representation as `Nat` and thus needs to be special-cased here.
| ``Int => return .tobject
| ``lcVoid => return .void
| ``lcRealWorld => return .tagged
| _ =>
let env Lean.getEnv
let some (.inductInfo inductiveVal) := env.find? name | return .tobject
@@ -102,13 +83,13 @@ private def isAnyProducingType (type : Lean.Expr) : Bool :=
| .forallE _ _ b _ => isAnyProducingType b
| _ => false
partial def toIRType (type : Lean.Expr) : CoreM IRType := do
def toIRType (type : Lean.Expr) : CoreM IRType := do
match type with
| .const name _ => visitApp name #[]
| .const name _ => nameToIRType name
| .app .. =>
-- All mono types are in headBeta form.
let .const name _ := type.getAppFn | unreachable!
visitApp name type.getAppArgs
nameToIRType name
| .forallE _ _ b _ =>
-- Type formers are erased, but can be used polymorphically as
-- an arrow type producing `lcAny`. The runtime representation of
@@ -120,28 +101,18 @@ partial def toIRType (type : Lean.Expr) : CoreM IRType := do
return .object
| .mdata _ b => toIRType b
| _ => unreachable!
where
visitApp (declName : Name) (args : Array Lean.Expr) : CoreM IRType := do
if let some info hasTrivialStructure? declName then
let ctorType LCNF.getOtherDeclBaseType info.ctorName []
let monoType LCNF.toMonoType (LCNF.getParamTypes ( LCNF.instantiateForall ctorType args[*...info.numParams]))[info.fieldIdx]!
toIRType monoType
else
nameToIRType declName
inductive CtorFieldInfo where
| erased
| object (i : Nat) (type : IRType)
| usize (i : Nat)
| scalar (sz : Nat) (offset : Nat) (type : IRType)
| void
deriving Inhabited
namespace CtorFieldInfo
def format : CtorFieldInfo Format
| erased => ""
| void => "void"
| object i type => f!"obj@{i}:{type}"
| usize i => f!"usize@{i}"
| scalar sz offset type => f!"scalar#{sz}@{offset}:{type}"
@@ -186,7 +157,6 @@ where fillCache := do
pure <| .object i irFieldType
| .usize => pure <| .usize 0
| .erased => .pure <| .erased
| .void => .pure <| .void
| .uint8 =>
has1BScalar := true
.pure <| .scalar 1 0 .uint8
@@ -213,7 +183,7 @@ where fillCache := do
| .usize _ => do
let i modifyGet fun nextIdx => (nextIdx, nextIdx + 1)
return .usize i
| .object .. | .scalar .. | .erased | .void => return field
| .object .. | .scalar .. | .erased => return field
let numUSize := nextIdx - numObjs
let adjustScalarsForSize (fields : Array CtorFieldInfo) (size : Nat) (nextOffset : Nat)
: Array CtorFieldInfo × Nat :=
@@ -225,7 +195,7 @@ where fillCache := do
return .scalar sz offset type
else
return field
| .object .. | .usize _ | .erased | .void => return field
| .object .. | .usize _ | .erased => return field
let mut nextOffset := 0
if has8BScalar then
fields, nextOffset := adjustScalarsForSize fields 8 nextOffset

View File

@@ -44,4 +44,3 @@ public import Lean.Compiler.LCNF.Closure
public import Lean.Compiler.LCNF.LambdaLifting
public import Lean.Compiler.LCNF.ReduceArity
public import Lean.Compiler.LCNF.Probing
public import Lean.Compiler.LCNF.Irrelevant

View File

@@ -1,71 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
module
prelude
public import Lean.Compiler.LCNF.CompilerM
import Lean.Compiler.LCNF.BaseTypes
import Lean.Compiler.LCNF.Util
namespace Lean.Compiler.LCNF
/--
Given a constructor, return a bitmask `m` s.t. `m[i]` is true if field `i` is
computationally relevant.
-/
def getRelevantCtorFields (ctorName : Name) (trivialType : Expr MetaM Bool) :
CoreM (Array Bool) := do
let .ctorInfo info getConstInfo ctorName | unreachable!
Meta.MetaM.run' do
Meta.forallTelescopeReducing info.type fun xs _ => do
let mut result := #[]
for x in xs[info.numParams...*] do
let type Meta.inferType x
result := result.push !( trivialType type)
return result
/--
We say a structure has a trivial structure if it has not builtin support in the runtime,
it has only one constructor, and this constructor has only one relevant field.
-/
public structure TrivialStructureInfo where
ctorName : Name
numParams : Nat
fieldIdx : Nat
deriving Inhabited, Repr
/--
Return `some fieldIdx` if `declName` is the name of an inductive datatype s.t.
- It does not have builtin support in the runtime.
- It has only one constructor.
- This constructor has only one computationally relevant field.
-/
public def Irrelevant.hasTrivialStructure?
(cacheExt : CacheExtension Name (Option TrivialStructureInfo))
(trivialType : Expr MetaM Bool) (declName : Name) : CoreM (Option TrivialStructureInfo) := do
match ( cacheExt.find? declName) with
| some info? => return info?
| none =>
let info? fillCache
cacheExt.insert declName info?
return info?
where fillCache : CoreM (Option TrivialStructureInfo) := do
if isRuntimeBuiltinType declName then return none
let .inductInfo info getConstInfo declName | return none
if info.isUnsafe || info.isRec then return none
let [ctorName] := info.ctors | return none
let ctorType getOtherDeclBaseType ctorName []
if ctorType.isErased then return none
let mask getRelevantCtorFields ctorName trivialType
let mut result := none
for h : i in *...mask.size do
if mask[i] then
if result.isSome then return none
result := some { ctorName, fieldIdx := i, numParams := info.numParams }
return result
end Lean.Compiler.LCNF

View File

@@ -133,13 +133,11 @@ def showDecl (phase : Phase) (declName : Name) : CoreM Format := do
let some decl getDeclAt? declName phase | return "<not-available>"
ppDecl' decl
@[export lean_lcnf_compile_decls]
def main (declNames : Array Name) : CoreM Unit := do
withTraceNode `Compiler (fun _ => return m!"compiling: {declNames}") do
CompilerM.run <| discard <| PassManager.run declNames
builtin_initialize
compileDeclsRef.set main
builtin_initialize
registerTraceClass `Compiler.init (inherited := true)
registerTraceClass `Compiler.test (inherited := true)

View File

@@ -8,14 +8,36 @@ module
prelude
public import Lean.Compiler.LCNF.Util
public import Lean.Compiler.LCNF.BaseTypes
public import Lean.Compiler.LCNF.CompilerM
public import Lean.Compiler.LCNF.Irrelevant
public section
namespace Lean.Compiler.LCNF
private builtin_initialize trivialStructureInfoExt : CacheExtension Name (Option TrivialStructureInfo)
/--
Given a constructor, return a bitmask `m` s.t. `m[i]` is true if field `i` is
computationally relevant.
-/
def getRelevantCtorFields (ctorName : Name) : CoreM (Array Bool) := do
let .ctorInfo info getConstInfo ctorName | unreachable!
Meta.MetaM.run' do
Meta.forallTelescopeReducing info.type fun xs _ => do
let mut result := #[]
for x in xs[info.numParams...*] do
let type Meta.inferType x
result := result.push !( Meta.isProp type <||> Meta.isTypeFormerType type)
return result
/--
We say a structure has a trivial structure if it has not builtin support in the runtime,
it has only one constructor, and this constructor has only one relevant field.
-/
structure TrivialStructureInfo where
ctorName : Name
numParams : Nat
fieldIdx : Nat
deriving Inhabited, Repr
builtin_initialize trivialStructureInfoExt : CacheExtension Name (Option TrivialStructureInfo)
CacheExtension.register
/--
@@ -25,8 +47,26 @@ Return `some fieldIdx` if `declName` is the name of an inductive datatype s.t.
- This constructor has only one computationally relevant field.
-/
def hasTrivialStructure? (declName : Name) : CoreM (Option TrivialStructureInfo) := do
let irrelevantType type := Meta.isProp type <||> Meta.isTypeFormerType type
Irrelevant.hasTrivialStructure? trivialStructureInfoExt irrelevantType declName
match ( trivialStructureInfoExt.find? declName) with
| some info? => return info?
| none =>
let info? fillCache
trivialStructureInfoExt.insert declName info?
return info?
where fillCache : CoreM (Option TrivialStructureInfo) := do
if isRuntimeBuiltinType declName then return none
let .inductInfo info getConstInfo declName | return none
if info.isUnsafe || info.isRec then return none
let [ctorName] := info.ctors | return none
let ctorType getOtherDeclBaseType ctorName []
if ctorType.isErased then return none
let mask getRelevantCtorFields ctorName
let mut result := none
for h : i in *...mask.size do
if mask[i] then
if result.isSome then return none
result := some { ctorName, fieldIdx := i, numParams := info.numParams }
return result
def getParamTypes (type : Expr) : Array Expr :=
go type #[]

View File

@@ -163,8 +163,8 @@ where
| .forallE .. => visitForall type #[]
| .app .. => type.withApp visitApp
| .fvar .. => visitApp type #[]
| .proj ``Subtype 0 (.app (.const ``Void.nonemptyType []) _) =>
return mkConst ``lcVoid
| .proj ``Subtype 0 (.const ``IO.RealWorld.nonemptyType []) =>
return mkConst ``lcRealWorld
| _ => return mkConst ``lcAny
whnfEta (type : Expr) : MetaM Expr := do
@@ -195,10 +195,6 @@ where
visitApp (f : Expr) (args : Array Expr) := do
let fNew match f with
| .const declName us =>
if ( getEnv).isExporting && isPrivateName declName then
-- This branch can happen under `backward.privateInPublic`; restore original behavior of
-- failing here, which is caught and ignored above by `observing`.
throwError "internal compiler error: private in public"
let .inductInfo _ getConstInfo declName | return anyExpr
pure <| .const declName us
| .fvar .. => pure f

View File

@@ -7,7 +7,7 @@ module
prelude
public import Lean.Data.Name
import Init.Data.String.Iterator
import Init.Data.String.Basic
public section

View File

@@ -684,25 +684,9 @@ def traceBlock (tag : String) (t : Task α) : CoreM α := do
profileitM Exception "blocked" ( getOptions) do
IO.wait t
/--
This ref exists to break a linking cycle that goes as follows:
- We start in `Environment.lean`, there we have functions referencing the compiler such as
`evalConst`
- This pulls in the entire compiler transitively as well as all of its dependents
- The compiler relies on things like WHNF to inspect types
- WHNF in turn imports Environment
On Windows this causes a large amount of symbols to be included in one DLL as everything that
imports the Environment instantly requires a large chunk of the Meta stack to be linked. This ref
breaks the cycle by making `compileDeclsImpl` a "dynamic" call through the ref that is not visible
to the linker. In the compiler there is a matching `builtin_initialize` to set this ref to the
actual implementation of compileDeclsRef.
-/
builtin_initialize compileDeclsRef : IO.Ref (Array Name CoreM Unit)
IO.mkRef (fun _ => throwError m!"call to compileDecls with uninitialized compileDeclsRef")
def compileDeclsImpl (declNames : Array Name) : CoreM Unit := do
( compileDeclsRef.get) declNames
-- Forward declaration
@[extern "lean_lcnf_compile_decls"]
opaque compileDeclsImpl (declNames : Array Name) : CoreM Unit
-- `ref?` is used for error reporting if available
partial def compileDecls (decls : Array Name) (logErrors := true) : CoreM Unit := do

View File

@@ -30,29 +30,29 @@ section Utils
if string.isEmpty then
#[]
else if string.length == 1 then
#[f none (String.Pos.Raw.get string 0) none]
#[f none (string.get 0) none]
else Id.run do
let mut result := Array.mkEmpty string.length
result := result.push <| f none (String.Pos.Raw.get string 0) (String.Pos.Raw.get string 1)
result := result.push <| f none (string.get 0) (string.get 1)
-- TODO: the following code is assuming all characters are ASCII
for i in [2:string.length] do
result := result.push <| f (String.Pos.Raw.get string i - 2) (String.Pos.Raw.get string i - 1) (String.Pos.Raw.get string i)
result.push <| f (String.Pos.Raw.get string string.length - 2) (String.Pos.Raw.get string string.length - 1) none
result := result.push <| f (string.get i - 2) (string.get i - 1) (string.get i)
result.push <| f (string.get string.length - 2) (string.get string.length - 1) none
private partial def containsInOrderLower (a b : String) : Bool := Id.run do
go 0 0
where
go (aPos bPos : String.Pos.Raw) : Bool :=
if ha : aPos.atEnd a then
if ha : a.atEnd aPos then
true
else if hb : bPos.atEnd b then
else if hb : b.atEnd bPos then
false
else
let ac := aPos.get' a ha
let bc := bPos.get' b hb
let bPos := bPos.next' b hb
let ac := a.get' aPos ha
let bc := b.get' bPos hb
let bPos := b.next' bPos hb
if ac.toLower == bc.toLower then
let aPos := aPos.next' a ha
let aPos := a.next' aPos ha
go aPos bPos
else
go aPos bPos
@@ -173,7 +173,7 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr
let mut matchScore := .awful
if allowMatch (String.Pos.Raw.get pattern patternIdx) (String.Pos.Raw.get word wordIdx) patternRoles[patternIdx]! wordRoles[wordIdx]! then
if allowMatch (pattern.get patternIdx) (word.get wordIdx) patternRoles[patternIdx]! wordRoles[wordIdx]! then
if patternIdx >= 1 then
let runLength := runLengths[getIdx (patternIdx - 1) (wordIdx - 1)]! + 1
runLengths := runLengths.set! (getIdx patternIdx wordIdx) runLength
@@ -248,7 +248,7 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr
matchResult (patternIdx wordIdx : Nat) (patternRole wordRole : CharRole) (consecutive : Score) : Int16 := Id.run do
let mut score : Int16 := 1
/- Case-sensitive equality or beginning of a segment in pattern and word. -/
if (String.Pos.Raw.get pattern patternIdx) == (String.Pos.Raw.get word wordIdx) || (patternRole matches CharRole.head && wordRole matches CharRole.head) then
if (pattern.get patternIdx) == (word.get wordIdx) || (patternRole matches CharRole.head && wordRole matches CharRole.head) then
score := score + 1
/- Matched end of word with end of pattern -/
if wordIdx == word.length - 1 && patternIdx == pattern.length - 1 then

View File

@@ -14,7 +14,6 @@ public import Std.Data.TreeMap.Raw.Basic
public import Init.Data.Ord.String
import Init.Data.Range.Polymorphic.Iterators
import Init.Data.Range.Polymorphic.Nat
import Init.Data.String.TakeDrop
public section

View File

@@ -8,7 +8,6 @@ module
prelude
public import Lean.Data.JsonRpc
import Init.Data.String.TakeDrop
public section

View File

@@ -109,12 +109,12 @@ instance : ToJson CompletionIdentifier where
instance : FromJson CompletionIdentifier where
fromJson?
| .str s =>
let c := s.front
let c := s.get 0
if c == 'c' then
let declName := String.Pos.Raw.extract s 1 s.rawEndPos |>.toName
let declName := s.extract 1 s.endPos |>.toName
.ok <| .const declName
else if c == 'f' then
let id := String.Pos.Raw.extract s 1 s.rawEndPos |>.toName
let id := s.extract 1 s.endPos |>.toName
.ok <| .fvar id
else
.error "Expected string with prefix `c` or `f` in `FromJson` instance of `CompletionIdentifier`."

View File

@@ -34,7 +34,7 @@ def utf16Length (s : String) : Nat :=
private def codepointPosToUtf16PosFromAux (s : String) : Nat Pos.Raw Nat Nat
| 0, _, utf16pos => utf16pos
| cp+1, utf8pos, utf16pos => codepointPosToUtf16PosFromAux s cp (utf8pos.next s) (utf16pos + csize16 (utf8pos.get s))
| cp+1, utf8pos, utf16pos => codepointPosToUtf16PosFromAux s cp (s.next utf8pos) (utf16pos + csize16 (s.get utf8pos))
/-- Computes the UTF-16 offset of the `n`-th Unicode codepoint
in the substring of `s` starting at UTF-8 offset `off`.
@@ -47,7 +47,7 @@ def codepointPosToUtf16Pos (s : String) (pos : Nat) : Nat :=
private partial def utf16PosToCodepointPosFromAux (s : String) : Nat Pos.Raw Nat Nat
| 0, _, cp => cp
| utf16pos, utf8pos, cp => utf16PosToCodepointPosFromAux s (utf16pos - csize16 (utf8pos.get s)) (utf8pos.next s) (cp + 1)
| utf16pos, utf8pos, cp => utf16PosToCodepointPosFromAux s (utf16pos - csize16 (s.get utf8pos)) (s.next utf8pos) (cp + 1)
/-- Computes the position of the Unicode codepoint at UTF-16 offset
`utf16pos` in the substring of `s` starting at UTF-8 offset `off`. -/
@@ -60,7 +60,7 @@ def utf16PosToCodepointPos (s : String) (pos : Nat) : Nat :=
/-- Starting at `utf8pos`, finds the UTF-8 offset of the `p`-th codepoint. -/
def codepointPosToUtf8PosFrom (s : String) : String.Pos.Raw Nat String.Pos.Raw
| utf8pos, 0 => utf8pos
| utf8pos, p+1 => codepointPosToUtf8PosFrom s (utf8pos.next s) p
| utf8pos, p+1 => codepointPosToUtf8PosFrom s (s.next utf8pos) p
end String
@@ -89,15 +89,15 @@ def leanPosToLspPos (text : FileMap) : Lean.Position → Lsp.Position
def utf8PosToLspPos (text : FileMap) (pos : String.Pos.Raw) : Lsp.Position :=
text.leanPosToLspPos (text.toPosition pos)
/-- Gets the LSP range from a `Lean.Syntax.Range`. -/
def utf8RangeToLspRange (text : FileMap) (range : Lean.Syntax.Range) : Lsp.Range :=
/-- Gets the LSP range from a `String.Range`. -/
def utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range :=
{ start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }
/-- Gets the LSP range of syntax `stx`. -/
def lspRangeOfStx? (text : FileMap) (stx : Syntax) (canonicalOnly := false) : Option Lsp.Range :=
text.utf8RangeToLspRange <$> stx.getRange? canonicalOnly
def lspRangeToUtf8Range (text : FileMap) (range : Lsp.Range) : Lean.Syntax.Range :=
def lspRangeToUtf8Range (text : FileMap) (range : Lsp.Range) : String.Range :=
{ start := text.lspPosToUtf8Pos range.start, stop := text.lspPosToUtf8Pos range.end }
end FileMap

View File

@@ -7,7 +7,6 @@ module
prelude
public import Init.Data.Ord.Basic
import Init.Data.String.TakeDrop
import Init.Data.Ord.String
import Init.Data.Ord.UInt
@@ -112,7 +111,7 @@ def hasNum : Name → Bool
/-- The frontend does not allow user declarations to start with `_` in any of its parts.
We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`). -/
def isInternal : Name Bool
| str p s => s.front == '_' || isInternal p
| str p s => s.get 0 == '_' || isInternal p
| num p _ => isInternal p
| _ => false
@@ -123,7 +122,7 @@ We use name parts starting with `_` internally to create auxiliary names (e.g.,
This function checks if any component of the name starts with `_`, or is numeric.
-/
def isInternalOrNum : Name Bool
| .str p s => s.front == '_' || isInternalOrNum p
| .str p s => s.get 0 == '_' || isInternalOrNum p
| .num _ _ => true
| _ => false

View File

@@ -8,7 +8,6 @@ module
prelude
public import Lean.Data.Json.FromToJson.Basic
public import Lean.ToExpr
import Init.Data.String.Iterator
public section
@@ -64,10 +63,10 @@ def getLine (fmap : FileMap) (x : Nat) : Nat :=
partial def ofString (s : String) : FileMap :=
let rec loop (i : String.Pos.Raw) (line : Nat) (ps : Array String.Pos.Raw) : FileMap :=
if i.atEnd s then { source := s, positions := ps.push i }
if s.atEnd i then { source := s, positions := ps.push i }
else
let c := i.get s
let i := i.next s
let c := s.get i
let i := s.next i
if c == '\n' then loop i (line+1) (ps.push i)
else loop i line ps
loop 0 1 #[0]
@@ -77,8 +76,8 @@ partial def toPosition (fmap : FileMap) (pos : String.Pos.Raw) : Position :=
| { source := str, positions := ps } =>
if ps.size >= 2 && pos <= ps.back! then
let rec toColumn (i : String.Pos.Raw) (c : Nat) : Nat :=
if i == pos || i.atEnd str then c
else toColumn (i.next str) (c+1)
if i == pos || str.atEnd i then c
else toColumn (str.next i) (c+1)
let rec loop (b e : Nat) :=
let posB := ps[b]!
if e == b + 1 then { line := fmap.getLine b, column := toColumn posB 0 }

View File

@@ -175,7 +175,7 @@ partial def matchPrefix (s : String) (t : Trie α) (i : String.Pos.Raw)
| node1 v c' t', i, res =>
let res := if v.isSome then v else res
if h : i < endByte then
let c := s.getUTF8Byte i (by simp [String.Pos.Raw.lt_iff]; omega)
let c := s.getUTF8Byte i (by simp; omega)
if c == c'
then loop t' (i + 1) res
else res
@@ -184,7 +184,7 @@ partial def matchPrefix (s : String) (t : Trie α) (i : String.Pos.Raw)
| node v cs ts, i, res =>
let res := if v.isSome then v else res
if h : i < endByte then
let c := s.getUTF8Byte i (by simp [String.Pos.Raw.lt_iff]; omega)
let c := s.getUTF8Byte i (by simp; omega)
match cs.findIdx? (· == c) with
| none => res
| some idx => loop ts[idx]! (i + 1) res

View File

@@ -38,7 +38,7 @@ def validateDocComment
for (start, stop, err) in errs do
-- Report errors at their actual location if possible
if let some pos := pos? then
let urlStx : Syntax := .atom (.synthetic (start.offsetBy pos) (stop.offsetBy pos)) (String.Pos.Raw.extract str start stop)
let urlStx : Syntax := .atom (.synthetic (start.offsetBy pos) (stop.offsetBy pos)) (str.extract start stop)
logErrorAt urlStx err
else
logError err
@@ -65,9 +65,9 @@ def parseVersoDocString
| throwErrorAt docComment m!"Documentation comment has no source location, cannot parse"
-- Skip trailing `-/`
let endPos := String.Pos.Raw.prev text.source <| endPos.prev text.source
let endPos := if endPos text.source.rawEndPos then endPos else text.source.rawEndPos
have endPos_valid : endPos text.source.rawEndPos := by
let endPos := text.source.prev <| text.source.prev endPos
let endPos := if endPos text.source.endPos then endPos else text.source.endPos
have endPos_valid : endPos text.source.endPos := by
unfold endPos
split <;> simp [*]

View File

@@ -210,11 +210,11 @@ def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array Module
def getDocStringText [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
match stx.raw[1] with
| Syntax.atom _ val =>
return String.Pos.Raw.extract val 0 (val.rawEndPos.unoffsetBy 2)
return val.extract 0 (val.endPos.unoffsetBy 2)
| Syntax.node _ `Lean.Parser.Command.versoCommentBody _ =>
match stx.raw[1][0] with
| Syntax.atom _ val =>
return String.Pos.Raw.extract val 0 (val.rawEndPos.unoffsetBy 2)
return val.extract 0 (val.endPos.unoffsetBy 2)
| _ =>
throwErrorAt stx "unexpected doc string{indentD stx}"
| _ =>

View File

@@ -154,7 +154,7 @@ partial def versoSyntaxToString' (stx : Syntax) : ReaderT Nat (StateM String) Un
out "\n"
let i read
let s := Syntax.decodeStrLit (atomString s) |>.getD ""
|>.splitToList (· == '\n')
|>.split (· == '\n')
|>.map ("".pushn ' ' i ++ · ) |> "\n".intercalate
out s
out <| "".pushn ' ' i

View File

@@ -8,8 +8,6 @@ module
prelude
public import Lean.Syntax
import Init.Data.String.TakeDrop
import Init.Data.String.Iterator
public section
@@ -102,7 +100,7 @@ environment variable. If this environment variable is not set, a manual root pro
built is used (typically this is the version corresponding to the current release). If no such root
is available, the latest version of the manual is used.
-/
def rewriteManualLinksCore (s : String) : BaseIO (Array (Lean.Syntax.Range × String) × String) := do
def rewriteManualLinksCore (s : String) : BaseIO (Array (String.Range × String) × String) := do
let scheme := "lean-manual://"
let mut out := ""
let mut errors := #[]
@@ -154,7 +152,7 @@ where
Returns `true` if `goal` is a prefix of the string at the position pointed to by `iter`.
-/
lookingAt (goal : String) (iter : String.Iterator) : Bool :=
String.Pos.Raw.substrEq iter.s iter.i goal 0 goal.rawEndPos.byteIdx
iter.s.substrEq iter.i goal 0 goal.endPos.byteIdx
/--
Rewrites Lean reference manual links in `docstring` to point at the reference manual.
@@ -171,7 +169,7 @@ The `lean-manual` URL scheme is used to link to the version of the Lean referenc
corresponds to this version of Lean. Errors occurred while processing the links in this documentation
comment:
"# ++
String.join (errs.toList.map (fun (s, e, msg) => s!" * ```{String.Pos.Raw.extract docString s e}```: {msg}\n\n"))
String.join (errs.toList.map (fun (s, e, msg) => s!" * ```{docString.extract s e}```: {msg}\n\n"))
return str ++ "\n\n" ++ errReport
return str
@@ -189,4 +187,4 @@ def validateBuiltinDocString (docString : String) : IO Unit := do
if !errs.isEmpty then
throw <| IO.userError <|
s!"Errors in builtin documentation comment:\n" ++
String.join (errs.toList.map fun (s, e, msg) => s!" * {repr <| String.Pos.Raw.extract docString s e}:\n {msg}\n")
String.join (errs.toList.map fun (s, e, msg) => s!" * {repr <| docString.extract s e}:\n {msg}\n")

View File

@@ -10,8 +10,6 @@ prelude
import Init.Data.Ord
public import Lean.DocString.Types
public import Init.Data.String.TakeDrop
import Init.Data.String.Iterator
set_option linter.missingDocs true

View File

@@ -1252,11 +1252,8 @@ inductive LValResolution where
The `baseName` is the base name of the type to search for in the parameter list. -/
| localRec (baseName : Name) (fvar : Expr)
private def mkLValError (e : Expr) (eType : Expr) (msg : MessageData) : MessageData :=
m!"{msg}{indentExpr e}\nhas type{indentExpr eType}"
private def throwLValErrorAt (ref : Syntax) (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α :=
throwErrorAt ref (mkLValError e eType msg)
throwErrorAt ref "{msg}{indentExpr e}\nhas type{indentExpr eType}"
private def throwLValError (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α := do
throwLValErrorAt ( getRef) e eType msg
@@ -1325,19 +1322,9 @@ where
| some (_, p2) => prodArity p2 + 1
private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM LValResolution := do
let throwInvalidFieldAt {α : Type} (ref : Syntax) (fieldName : String) (fullName : Name)
(declHint := Name.anonymous) : TermElabM α := do
let msg
-- ordering: put decl hint, if any, last
mkUnknownIdentifierMessage (declHint := declHint)
(mkLValError e eType
m!"Invalid field `{fieldName}`: The environment does not contain `{fullName}`")
-- HACK: Simulate previous embedding of tagged `mkUnknownIdentifierMessage`.
-- The "import unknown identifier" code action requires the tag to be present somewhere in the
-- message. But if it is at the root, the tag will also be shown to the user even though the
-- current help page does not address field notation, which should likely get its own help page
-- (if any).
throwErrorAt ref m!"{msg}{.nil}"
let throwInvalidFieldAt {α : Type} (ref : Syntax) (fieldName : String) (fullName : Name) : TermElabM α := do
throwLValErrorAt ref e eType <| mkUnknownIdentifierMessage (declHint := fullName)
m!"Invalid field `{fieldName}`: The environment does not contain `{fullName}`"
if eType.isForall then
match lval with
| LVal.fieldName _ fieldName suffix? fullRef =>
@@ -1403,9 +1390,6 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
if let some (baseStructName, fullName) findMethod? structName (.mkSimple fieldName) then
return LValResolution.const baseStructName structName fullName
throwInvalidFieldAt fullRef fieldName fullName
-- Suggest a potential unreachable private name as hint. This does not cover structure
-- inheritance, nor `import all`.
(declHint := (mkPrivateName env structName).mkStr fieldName)
| none, LVal.fieldName _ _ (some suffix) fullRef =>
-- This may be a function constant whose implicit arguments have already been filled in:
let c := e.getAppFn
@@ -1590,15 +1574,14 @@ where
/-- Adds the `TermInfo` for the field of a projection. See `Lean.Parser.Term.identProjKind`. -/
private def addProjTermInfo
(stx : Syntax)
(e : Expr)
(expectedType? : Option Expr := none)
(lctx? : Option LocalContext := none)
(elaborator : Name := Name.anonymous)
(isBinder force : Bool := false)
(isDisplayableTerm : Bool := false)
(stx : Syntax)
(e : Expr)
(expectedType? : Option Expr := none)
(lctx? : Option LocalContext := none)
(elaborator : Name := Name.anonymous)
(isBinder force : Bool := false)
: TermElabM Expr :=
addTermInfo (Syntax.node .none Parser.Term.identProjKind #[stx]) e expectedType? lctx? elaborator isBinder force isDisplayableTerm
addTermInfo (Syntax.node .none Parser.Term.identProjKind #[stx]) e expectedType? lctx? elaborator isBinder force
private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) (explicit ellipsis : Bool)
(f : Expr) (lvals : List LVal) : TermElabM Expr :=
@@ -1617,7 +1600,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
| LValResolution.projFn baseStructName structName fieldName =>
let f mkBaseProjections baseStructName structName f
let some info := getFieldInfo? ( getEnv) baseStructName fieldName | unreachable!
if ( isInaccessiblePrivateName info.projFn) then
if isInaccessiblePrivateName ( getEnv) info.projFn then
throwError "Field `{fieldName}` from structure `{structName}` is private"
let projFn mkConst info.projFn
let projFn addProjTermInfo lval.getRef projFn
@@ -1751,7 +1734,7 @@ where
match resultTypeFn with
| .const declName .. =>
let env getEnv
if ( isInaccessiblePrivateName declName) then
if isInaccessiblePrivateName env declName then
throwError "The private declaration `{.ofConstName declName}` is not accessible in the current context"
-- Recall that the namespace for private declarations is non-private.
let fullName := privateToUserName declName ++ id

View File

@@ -22,7 +22,7 @@ namespace Lean.Elab.Command
match stx[1] with
| Syntax.atom _ val =>
if getVersoModuleDocs ( getEnv) |>.isEmpty then
let doc := String.Pos.Raw.extract val 0 (val.rawEndPos.unoffsetBy 2)
let doc := val.extract 0 (val.endPos.unoffsetBy 2)
modifyEnv fun env => addMainModuleDoc env doc, range
else
throwError m!"Can't add Markdown-format module docs because there is already Verso-format content present."

View File

@@ -56,7 +56,7 @@ open Meta
(fun ival _ => do
match ival.ctors with
| [ctor] =>
if ( isInaccessiblePrivateName ctor) then
if isInaccessiblePrivateName ( getEnv) ctor then
throwError "Invalid `⟨...⟩` notation: Constructor for `{ival.name}` is marked as private"
let cinfo getConstInfoCtor ctor
let numExplicitFields forallTelescopeReducing cinfo.type fun xs _ => do

View File

@@ -164,7 +164,7 @@ private def getMVarFromUserName (ident : Syntax) : MetaM Expr := do
-- `by` switches from an exported to a private context, so we must disallow unassigned
-- metavariables in the goal in this case as they could otherwise leak private data back into
-- the exported context.
mkTacticMVar expectedType stx .term (delayOnMVars := ( getEnv).isExporting && !( backward.proofsInPublic.getM))
mkTacticMVar expectedType stx .term (delayOnMVars := ( getEnv).isExporting)
| none =>
tryPostpone
throwError ("invalid 'by' tactic, expected type has not been provided")

View File

@@ -159,7 +159,7 @@ def expandOptDocComment? [Monad m] [MonadError m] (optDocComment : Syntax) : m (
match optDocComment.getOptional? with
| none => return none
| some s => match s[1] with
| .atom _ val => return some (String.Pos.Raw.extract val 0 (val.rawEndPos.unoffsetBy 2))
| .atom _ val => return some (val.extract 0 (val.endPos.unoffsetBy 2))
| _ => throwErrorAt s "unexpected doc string{indentD s[1]}"
section Methods

View File

@@ -1204,12 +1204,12 @@ private def mkSuggestion
let some b, e := ref.getRange?
| pure m!""
let text getFileMap
let pre := String.Pos.Raw.extract text.source 0 b
let post := String.Pos.Raw.extract text.source e text.source.rawEndPos
let pre := text.source.extract 0 b
let post := text.source.extract e text.source.endPos
let edits := newStrings.map fun (s, _, _) =>
let lines := text.source.splitToList (· == '\n') |>.toArray
let lines := text.source.split (· == '\n') |>.toArray
let s' := pre ++ s ++ post
let lines' := s'.splitToList (· == '\n') |>.toArray
let lines' := s'.split (· == '\n') |>.toArray
let d := diff lines lines'
toMessageData <| Diff.linesToString <| d.filter (·.1 != Action.skip)
pure m!"\n\nHint: {hintTitle}\n{indentD <| m!"\n".joinSep edits.toList}"
@@ -1255,7 +1255,7 @@ public partial def elabInline (stx : TSyntax `inline) : DocM (Inline ElabInline)
catch | _ => pure ()
unless suggestions.isEmpty do
let text getFileMap
let str := String.Pos.Raw.extract text.source b e
let str := text.source.extract b e
let ss : Array (String × Option String × Option String)
suggestions.mapM fun {role, args, moreInfo} => do
pure {
@@ -1373,7 +1373,7 @@ public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline Ela
catch | _ => pure ()
unless suggestions.isEmpty do
let text getFileMap
let str := String.Pos.Raw.extract text.source b e
let str := text.source.extract b e
let ss : Array (String × Option String × Option String)
suggestions.mapM fun {name, args, moreInfo} => do
pure {

View File

@@ -122,7 +122,7 @@ private def onlyCode [Monad m] [MonadError m] (xs : TSyntaxArray `inline) : m St
else
throwError "Expected precisely 1 code argument"
private def strLitRange [Monad m] [MonadFileMap m] (s : StrLit) : m Lean.Syntax.Range := do
private def strLitRange [Monad m] [MonadFileMap m] (s : StrLit) : m String.Range := do
let pos := (s.raw.getPos? (canonicalOnly := true)).get!
let endPos := s.raw.getTailPos? true |>.get!
return pos, endPos
@@ -168,7 +168,7 @@ def name (full : Option Ident := none) (scope : DocScope := .local)
| none
let _, pos tk1.getRange?
let tailPos, _ tk2.getRange?
pure <| Syntax.mkStrLit (String.Pos.Raw.extract text.source pos tailPos) (info := .synthetic pos tailPos)
pure <| Syntax.mkStrLit (text.source.extract pos tailPos) (info := .synthetic pos tailPos)
if let some ref := ref? then
m!"Remove surrounding whitespace:".hint #[s.getString.trim] (ref? := some ref)
else pure m!""
@@ -264,7 +264,7 @@ def module (checked : flag true) (xs : TSyntaxArray `inline) : DocM (Inline Elab
let some e := tk2.getPos?
| pure none
pure <| some {
span? := some (Syntax.mkStrLit (String.Pos.Raw.extract ( getFileMap).source b e) (info := .synthetic b e)),
span? := some (Syntax.mkStrLit (( getFileMap).source.extract b e) (info := .synthetic b e)),
previewSpan? := some ref,
suggestion := "" : Meta.Hint.Suggestion
}
@@ -598,8 +598,8 @@ def given (type : Option StrLit := none) (typeIsMeta : flag false) («show» : f
let thisStr
if let some b, e := stx[0].getRange? then
if let some b', e' := stx[2][1].getRange? then
pure <| s!"{String.Pos.Raw.extract text.source b e} : {String.Pos.Raw.extract text.source b' e'}"
else pure <| String.Pos.Raw.extract text.source b e
pure <| s!"{text.source.extract b e} : {text.source.extract b' e'}"
else pure <| text.source.extract b e
else
failed := true
break
@@ -647,7 +647,7 @@ def lean (name : Option Ident := none) (error warning «show» : flag false) (co
-- TODO fallback for non-original syntax
let pos := code.raw.getPos? true |>.get!
let endPos := code.raw.getTailPos? true |>.get!
let endPos := if endPos text.source.rawEndPos then endPos else text.source.rawEndPos
let endPos := if endPos text.source.endPos then endPos else text.source.endPos
let ictx :=
mkInputContext text.source ( getFileName)
(endPos := endPos) (endPos_valid := by simp only [endPos]; split <;> simp [*])
@@ -673,8 +673,8 @@ def lean (name : Option Ident := none) (error warning «show» : flag false) (co
let mut output := #[]
for msg in cmdState.messages.toArray do
let b := text.ofPosition msg.pos
let e := msg.endPos |>.map text.ofPosition |>.getD (b.next text.source)
let msgStr := String.Pos.Raw.extract text.source b e
let e := msg.endPos |>.map text.ofPosition |>.getD (text.source.next b)
let msgStr := text.source.extract b e
let msgStx := Syntax.mkStrLit msgStr (info := .synthetic b e (canonical := true))
unless msg.isSilent do
if name.isSome then output := output.push (msg.severity, msg.data.toString)
@@ -719,7 +719,7 @@ where
(mkNullNode (#[name] ++ args)).getRange?
| _ => none
if let some b, e := range? then
let str := String.Pos.Raw.extract ( getFileMap).source b e
let str := ( getFileMap).source.extract b e
let str := if str.startsWith "kw?" then "kw" ++ str.drop 3 else str
let stx := Syntax.mkStrLit str (info := .synthetic b e (canonical := true))
let suggs := suggestions.map (fun (s : String) => {suggestion := str ++ s})

View File

@@ -330,7 +330,7 @@ private def withAtoms (cat : Name) (atoms : List String) : TermElabM (Array Name
private def kwImpl (cat : Ident := mkIdent .anonymous) (of : Ident := mkIdent .anonymous)
(suggest : Bool)
(s : StrLit) : TermElabM (Inline ElabInline) := do
let atoms := s.getString |>.splitToList (·.isWhitespace)
let atoms := s.getString |>.split (·.isWhitespace)
let env getEnv
let parsers := Lean.Parser.parserExtension.getState env
let cat' := cat.getId
@@ -413,7 +413,7 @@ where
(mkNullNode (#[name] ++ args)).getRange?
| _ => none
if let some b, e := range? then
let str := String.Pos.Raw.extract ( getFileMap).source b e
let str := ( getFileMap).source.extract b e
let str := if str.startsWith "kw?" then "kw" ++ str.drop 3 else str
let stx := Syntax.mkStrLit str (info := .synthetic b e (canonical := true))
let suggs := suggestions.map (fun (s : String) => {suggestion := str ++ s})
@@ -495,7 +495,7 @@ Suggests the `kw` role, if applicable.
-/
@[builtin_doc_code_suggestions]
public def suggestKw (code : StrLit) : DocM (Array CodeSuggestion) := do
let atoms := code.getString |>.splitToList (·.isWhitespace)
let atoms := code.getString |>.split (·.isWhitespace)
let env getEnv
let parsers := Lean.Parser.parserExtension.getState env
let cats := parsers.categories.toArray

View File

@@ -13,7 +13,7 @@ open Lean.Parser
public section
private def strLitRange [Monad m] [MonadFileMap m] (s : StrLit) : m Lean.Syntax.Range := do
private def strLitRange [Monad m] [MonadFileMap m] (s : StrLit) : m String.Range := do
let pos := (s.raw.getPos? (canonicalOnly := true)).get!
let endPos := s.raw.getTailPos? true |>.get!
return pos, endPos
@@ -25,7 +25,7 @@ def parseStrLit (p : ParserFn) (s : StrLit) : m Syntax := do
let text getFileMap
let env getEnv
let pos, endPos strLitRange s
let endPos := if endPos text.source.rawEndPos then endPos else text.source.rawEndPos
let endPos := if endPos text.source.endPos then endPos else text.source.endPos
let ictx :=
mkInputContext text.source ( getFileName)
(endPos := endPos) (endPos_valid := by simp only [endPos]; split <;> simp [*])
@@ -46,12 +46,12 @@ def parseQuotedStrLit (p : ParserFn) (strLit : StrLit) : m Syntax := do
let pos, _ strLitRange strLit
let pos do
let mut pos := pos
if pos.get text.source == 'r' then
pos := pos.next text.source
while pos.get text.source == '#' do
pos := pos.next text.source
if pos.get text.source == '"' then
pure <| pos.next text.source
if text.source.get pos == 'r' then
pos := text.source.next pos
while text.source.get pos == '#' do
pos := text.source.next pos
if text.source.get pos == '"' then
pure <| text.source.next pos
else
throwErrorAt strLit "Not a quoted string literal"
let str := strLit.getString
@@ -88,12 +88,12 @@ where
| .none => .none
nextn (str : String) (n : Nat) (p : String.Pos.Raw) : String.Pos.Raw :=
n.fold (init := p) fun _ _ _ => p.next str
n.fold (init := p) fun _ _ _ => str.next p
posIndex (str : String) (p : String.Pos.Raw) : Nat := Id.run do
let mut p := p
let mut n := 0
while p > 0 do
p := p.prev str
p := str.prev p
n := n + 1
return n
@@ -101,7 +101,7 @@ def parseStrLit' (p : ParserFn) (s : StrLit) : m (Syntax × Bool) := do
let text ← getFileMap
let env ← getEnv
let endPos := s.raw.getTailPos? true |>.get!
let endPos := if endPos ≤ text.source.rawEndPos then endPos else text.source.rawEndPos
let endPos := if endPos ≤ text.source.endPos then endPos else text.source.endPos
let ictx :=
mkInputContext text.source (← getFileName)
(endPos := endPos) (endPos_valid := by simp only [endPos]; split <;> simp [*])

View File

@@ -166,7 +166,7 @@ def WhitespaceMode.apply (mode : WhitespaceMode) (s : String) : String :=
match mode with
| .exact => s
| .normalized => s.replace "\n" " "
| .lax => String.intercalate " " <| (s.splitToList Char.isWhitespace).filter (!·.isEmpty)
| .lax => String.intercalate " " <| (s.split Char.isWhitespace).filter (!·.isEmpty)
/--
Applies a message ordering mode.
@@ -215,7 +215,7 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S
modify fun st => { st with messages := msgs }
let feedback :=
if guard_msgs.diff.get ( getOptions) then
let diff := Diff.diff (expected.splitToList (· == '\n')).toArray (res.splitToList (· == '\n')).toArray
let diff := Diff.diff (expected.split (· == '\n')).toArray (res.split (· == '\n')).toArray
Diff.linesToString diff
else res
logErrorAt tk m!"❌️ Docstring on `#guard_msgs` does not match generated message:\n\n{feedback}"

View File

@@ -16,7 +16,7 @@ open Lean
structure InlayHintLinkLocation where
module : Name
range : Lean.Syntax.Range
range : String.Range
structure InlayHintLabelPart where
value : String
@@ -32,7 +32,7 @@ inductive InlayHintKind where
| parameter
structure InlayHintTextEdit where
range : Lean.Syntax.Range
range : String.Range
newText : String
deriving BEq

View File

@@ -72,8 +72,6 @@ structure TermInfo extends ElabInfo where
expectedType? : Option Expr
expr : Expr
isBinder : Bool := false
/-- Whether `expr` should always be displayed in the language server, e.g. in hovers. -/
isDisplayableTerm : Bool := false
deriving Inhabited
/--

View File

@@ -366,7 +366,7 @@ private def expandWhereStructInst : Macro := fun whereStx => do
let endOfStructureTkInfo : SourceInfo :=
match structureStxTailInfo with
| some (SourceInfo.original _ _ trailing _) =>
let tokenPos := trailing.stopPos.prev trailing.str
let tokenPos := trailing.str.prev trailing.stopPos
let tokenEndPos := trailing.stopPos
.synthetic tokenPos tokenEndPos true
| _ => .none
@@ -1222,9 +1222,7 @@ where
assert! view.kind.isTheorem
let env getEnv
let async env.addConstAsync declId.declName .thm
(exportedKind? :=
guard (!isPrivateName declId.declName || ( ResolveName.backward.privateInPublic.getM)) *>
some .axiom)
(exportedKind? := guard (!isPrivateName declId.declName) *> some .axiom)
setEnv async.mainEnv
-- TODO: parallelize header elaboration as well? Would have to refactor auto implicits catch,

View File

@@ -15,7 +15,6 @@ import Lean.Elab.ComputedFields
import Lean.Meta.Constructions.CtorIdx
import Lean.Meta.Constructions.CtorElim
import Lean.Meta.IndPredBelow
import Lean.Meta.Injective
public section

View File

@@ -44,31 +44,31 @@ def State.mkEOIError (s : State) : State :=
{ s with error? := none, badModifier := false }
@[inline] def State.next (s : State) (input : String) (pos : String.Pos.Raw) : State :=
{ s with pos := pos.next input }
{ s with pos := input.next pos }
@[inline] def State.next' (s : State) (input : String) (pos : String.Pos.Raw) (h : ¬ pos.atEnd input) : State :=
{ s with pos := pos.next' input h }
@[inline] def State.next' (s : State) (input : String) (pos : String.Pos.Raw) (h : ¬ input.atEnd pos): State :=
{ s with pos := input.next' pos h }
partial def finishCommentBlock (nesting : Nat) : Parser := fun input s =>
let input := input
let i := s.pos
if h : i.atEnd input then eoi s
if h : input.atEnd i then eoi s
else
let curr := i.get' input h
let i := i.next' input h
let curr := input.get' i h
let i := input.next' i h
if curr == '-' then
if h : i.atEnd input then eoi s
if h : input.atEnd i then eoi s
else
let curr := i.get' input h
let curr := input.get' i h
if curr == '/' then -- "-/" end of comment
if nesting == 1 then s.next input i
else finishCommentBlock (nesting-1) input (s.next' input i h)
else
finishCommentBlock nesting input (s.next' input i h)
else if curr == '/' then
if h : i.atEnd input then eoi s
if h : input.atEnd i then eoi s
else
let curr := i.get' input h
let curr := input.get' i h
if curr == '-' then finishCommentBlock (nesting+1) input (s.next' input i h)
else finishCommentBlock nesting input (s.setPos i)
else finishCommentBlock nesting input (s.setPos i)
@@ -77,8 +77,8 @@ where
@[specialize] partial def takeUntil (p : Char Bool) : Parser := fun input s =>
let i := s.pos
if h : i.atEnd input then s
else if p (i.get' input h) then s
if h : input.atEnd i then s
else if p (input.get' i h) then s
else takeUntil p input (s.next' input i h)
@[inline] def takeWhile (p : Char Bool) : Parser :=
@@ -93,23 +93,23 @@ instance : AndThen Parser where
partial def whitespace : Parser := fun input s =>
let i := s.pos
if h : i.atEnd input then s
if h : input.atEnd i then s
else
let curr := i.get' input h
let curr := input.get' i h
if curr == '\t' then
s.mkError "tabs are not allowed; please configure your editor to expand them"
else if curr.isWhitespace then whitespace input (s.next input i)
else if curr == '-' then
let i := i.next' input h
let curr := i.get input
let i := input.next' i h
let curr := input.get i
if curr == '-' then andthen (takeUntil (fun c => c = '\n')) whitespace input (s.next input i)
else s
else if curr == '/' then
let i := i.next' input h
let curr := i.get input
let i := input.next' i h
let curr := input.get i
if curr == '-' then
let i := i.next input
let curr := i.get input
let i := input.next i
let curr := input.get i
if curr == '-' || curr == '!' then s -- "/--" and "/-!" doc comment are actual tokens
else andthen (finishCommentBlock 1) whitespace input (s.next input i)
else s
@@ -117,17 +117,17 @@ partial def whitespace : Parser := fun input s =>
@[inline] partial def keywordCore (k : String) (failure : Parser) (success : Parser) : Parser := fun input s =>
let rec @[specialize] go (i j : String.Pos.Raw) : State :=
if h₁ : i.atEnd k then
if h₁ : k.atEnd i then
success input <| whitespace input (s.setPos j)
else if h₂ : j.atEnd input then
else if h₂ : input.atEnd j then
failure input s
else
let curr₁ := i.get' k h₁
let curr₂ := j.get' input h₂
let curr₁ := k.get' i h₁
let curr₂ := input.get' j h₂
if curr₁ != curr₂ then
failure input s
else
go (i.next' k h₁) (j.next' input h₂)
go (k.next' i h₁) (input.next' j h₂)
go 0 s.pos
@[inline] def keyword (k : String) : Parser :=
@@ -135,13 +135,13 @@ partial def whitespace : Parser := fun input s =>
@[inline] def isIdCont : String State Bool := fun input s =>
let i := s.pos
let curr := i.get input
let curr := input.get i
if curr == '.' then
let i := i.next input
if h : i.atEnd input then
let i := input.next i
if h : input.atEnd i then
false
else
let curr := i.get' input h
let curr := input.get' i h
isIdFirst curr || isIdBeginEscape curr
else
false
@@ -162,19 +162,19 @@ partial def moduleIdent : Parser := fun input s =>
{s with isMeta := false, importAll := false, isExported := !s.isModule}
let rec parse (module : Name) (s : State) :=
let i := s.pos
if h : i.atEnd input then
if h : input.atEnd i then
s.mkEOIError
else
let curr := i.get' input h
let curr := input.get' i h
if isIdBeginEscape curr then
let startPart := i.next' input h
let startPart := input.next' i h
let s := takeUntil isIdEndEscape input (s.setPos startPart)
if h : s.pos.atEnd input then
if h : input.atEnd s.pos then
s.mkError "unterminated identifier escape"
else
let stopPart := s.pos
let s := s.next' input s.pos h
let module := .str module (String.Pos.Raw.extract input startPart stopPart)
let module := .str module (input.extract startPart stopPart)
if isIdCont input s then
let s := s.next input s.pos
parse module s
@@ -184,7 +184,7 @@ partial def moduleIdent : Parser := fun input s =>
let startPart := i
let s := takeWhile isIdRestFast input (s.next' input i h)
let stopPart := s.pos
let module := .str module (String.Pos.Raw.extract input startPart stopPart)
let module := .str module (input.extract startPart stopPart)
if isIdCont input s then
let s := s.next input s.pos
parse module s

View File

@@ -135,10 +135,7 @@ private def shouldGenCodeFor (preDef : PreDefinition) : Bool :=
!preDef.kind.isTheorem && !preDef.modifiers.isNoncomputable
private def compileDecl (decl : Declaration) : TermElabM Unit := do
Lean.compileDecl
-- `meta` should disregard `noncomputable section`
(logErrors := !( read).isNoncomputableSection || decl.getTopLevelNames.any (isMeta ( getEnv)))
decl
Lean.compileDecl (logErrors := !( read).isNoncomputableSection) decl
register_builtin_option diagnostics.threshold.proofSize : Nat := {
defValue := 16384

View File

@@ -26,7 +26,7 @@ This module finds lexicographic termination measures for well-founded recursion.
Starting with basic measures (`sizeOf xᵢ` for all parameters `xᵢ`), and complex measures
(e.g. `e₂ - e₁` if `e₁ < e₂` is found in the context of a recursive call) it tries all combinations
until it finds one where all proof obligations go through with the given tactic (`decreasing_by`),
until it finds one where all proof obligations go through with the given tactic (`decerasing_by`),
if given, or the default `decreasing_tactic`.
For mutual recursion, a single measure is not just one parameter, but one from each recursive

View File

@@ -1190,7 +1190,7 @@ private def elabStructInstView (s : StructInstView) (structName : Name) (structT
TermElabM Expr := withRef s.ref do
let env getEnv
let ctorVal := getStructureCtor env structName
if ( isInaccessiblePrivateName ctorVal.name) then
if isInaccessiblePrivateName env ctorVal.name then
throwError "invalid \{...} notation, constructor for `{.ofConstName structName}` is marked as private"
let { ctorFn, ctorFnType, structType, levels, params } mkCtorHeader ctorVal structType?
let (_, fields) expandFields structName s.fields (recover := ( read).errToSorry)

View File

@@ -87,8 +87,8 @@ def mkMissingFieldsHint (fields : Array (Name × Option Expr)) (stx : Syntax) :
let interveningLineEndPos? :=
if leaderLine + 1 (fileMap.utf8PosToLspPos view.closingPos).line then none else
let leaderLineEnd := findLineEnd fileMap.source view.leaderTailPos
let indentPos := (indent + 1).fold (init := leaderLineEnd) (fun _ _ p => p.next fileMap.source)
let interveningLineEnd := findLineEnd fileMap.source (leaderLineEnd.next fileMap.source)
let indentPos := (indent + 1).fold (init := leaderLineEnd) (fun _ _ p => fileMap.source.next p)
let interveningLineEnd := findLineEnd fileMap.source (fileMap.source.next leaderLineEnd)
let nextTwoLines := Substring.mk fileMap.source view.leaderTailPos interveningLineEnd
if nextTwoLines.all (·.isWhitespace) then some (min indentPos nextTwoLines.stopPos) else none
@@ -148,7 +148,7 @@ where
Counterpart of `String.findLineStart`.
-/
findLineEnd (s : String) (p : String.Pos.Raw) : String.Pos.Raw :=
s.findAux (· == '\n') s.rawEndPos p
s.findAux (· == '\n') s.endPos p
/--
Is the structure instance notation `stx` described by `view` using single-line styling?

View File

@@ -249,7 +249,7 @@ where
(s.front != '\'' || "''".isPrefixOf s) &&
s.front != '\"' &&
!(isIdBeginEscape s.front) &&
!(s.front == '`' && (s.rawEndPos == ⟨1⟩ || isIdFirst (String.Pos.Raw.get s ⟨1⟩) || isIdBeginEscape (String.Pos.Raw.get s ⟨1⟩))) &&
!(s.front == '`' && (s.endPos == ⟨1⟩ || isIdFirst (s.get ⟨1⟩) || isIdBeginEscape (s.get ⟨1⟩))) &&
!s.front.isDigit &&
!(s.any Char.isWhitespace)

View File

@@ -340,13 +340,6 @@ private def TacticMVarKind.maybeWithoutRecovery (kind : TacticMVarKind) (m : Tac
else
m
register_builtin_option backward.proofsInPublic : Bool := {
defValue := false
descr := "(module system) Do not abstract proofs used in the public scope into auxiliary \
theorems. Enabling this option may lead to failures or, when `backward.privateInPublic` and \
its `warn` sub-option are enabled, additional warnings from private accesses."
}
mutual
/--
@@ -359,7 +352,7 @@ mutual
partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) (kind : TacticMVarKind) (report := true) : TermElabM Unit := withoutAutoBoundImplicit do
let wasExporting := ( getEnv).isExporting
-- exit exporting context if entering proof
let isNoLongerExporting pure (wasExporting && !( backward.proofsInPublic.getM)) <&&> do
let isNoLongerExporting pure wasExporting <&&> do
mvarId.withContext do
isProp ( mvarId.getType)
instantiateMVarDeclMVars mvarId

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