Merge branch 'master' into joachim/less-isNoConfusion

Author: nomeata

.github/workflows/grove.yml

@@ -51,7 +51,7 @@ jobs:
       - name: Fetch upstream invalidated facts
         if: ${{ steps.should-run.outputs.should-run == 'true' && steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: fetch-upstream
-        uses: TwoFx/grove-action/fetch-upstream@v0.4
+        uses: TwoFx/grove-action/fetch-upstream@v0.5
         with:
           artifact-name: grove-invalidated-facts
           base-ref: master
@@ -96,7 +96,7 @@ jobs:
       - name: Build
         if: ${{ steps.should-run.outputs.should-run == 'true' }}
         id: build
-        uses: TwoFx/grove-action/build@v0.4
+        uses: TwoFx/grove-action/build@v0.5
         with:
           project-path: doc/std/grove
           script-name: grove-stdlib

doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/StringsAndFormatting.lean

@@ -11,9 +11,41 @@ namespace GroveStdlib.Std.CoreTypesAndOperations
 
 namespace StringsAndFormatting
 
+open Lean Meta
+
+def introduction : Text where
+  id := "string-introduction"
+  content := Grove.Markdown.render [
+    .h1 "The Lean string library",
+    .text "The Lean standard library contains a fully-featured string library, centered around the types `String` and `String.Slice`.",
+    .text "`String` is defined as the subtype of `ByteArray` of valid UTF-8 strings. A `String.Slice` is a `String` together with a start and end position.",
+    .text "`String` is equivalent to `List Char`, but it has a more efficient runtime representation. While the logical model based on `ByteArray` is overwritten in the runtime, the runtime implementation is very similar to the logical model, with the main difference being that the length of a string in Unicode code points is cached in the runtime implementation.",
+    .text "We are considering removing this feature in the future (i.e., deprecating `String.length`), as the number of UTF-8 codepoints in a string is not particularly useful, and if needed it can be computed in linear time using `s.positions.count`."
+  ]
+
 def highLevelStringTypes : List Lean.Name :=
   [`String, `String.Slice, `String.Pos, `String.Slice.Pos]
 
+def creatingStringsAndSlices : Text where
+  id := "transforming-strings-and-slices"
+  content := Grove.Markdown.render [
+    .h2 "Transforming strings and slices",
+    .text "The Lean standard library contains a number of functions that take one or more strings and slices and return a string or a slice.",
+    .text "If possible, these functions should avoid allocating a new string, and return a slice of their input(s) instead.",
+    .text "Usually, for every operation `f`, there will be functions `String.f` and `String.Slice.f`, where `String.f s` is defined as `String.Slice.f s.toSlice`.",
+    .text "In particular, functions that transform strings and slices should live in the `String` and `String.Slice` namespaces even if they involve a `String.Pos`/`String.Slice.Pos` (like `String.sliceTo`), for reasons that will become clear shortly.",
+
+    .h3 "Transforming positions",
+    .text "Since positions on strings and slices are dependent on the string or slice, whenever users transform a string/slice, they will be interested in interpreting positions on the original string/slice as positions on the result, or vice versa.",
+    .text "Consequently, every operation that transforms a string or slice should come with a corresponding set of transformations between positions, usually in both directions, possibly with one of the directions being conditional.",
+    .text "For example, given a string `s` and a position `p` on `s`, we have the slice `s.sliceFrom p`, which is the slice from `p` to the end of `s`. A position on `s.sliceFrom p` can always be interpreted as a position on `s`. This is the \"backwards\" transformation. Conversely, a position `q` on `s` can be interpreted as a position on `s.sliceFrom p` as long as `p ≤ q`. This is the conditional forwards direction.",
+    .text "The convention for naming these transformations is that the forwards transformation should have the same name as the transformation on strings/slices, but it should be located in the `String.Pos` or `String.Slice.Pos` namespace, depending on the type of the starting position (so that dot notation is possible for the forward direction). The backwards transformation should have the same name as the operation on strings/slices, but with an `of` prefix, and live in the same namespace as the forwards transformation (so in general dot notation will not be available).",
+    .text "So, in the `sliceFrom` example, the forward direction would be called `String.Pos.sliceFrom`, while the backwards direction should be called `String.Pos.ofSliceFrom` (not `String.Slice.Pos.ofSliceFrom`).",
+    .text "If one of the directions is conditional, it should have a corresponding panicking operation that does not require a proof; in our example this would be `String.Pos.sliceFrom!`.",
+    .text "Sometimes there is a name clash for the panicking operations if the operation on strings is already panicking. For example, there are both `String.slice` and `String.slice!`. If the original operation is already panicking, we only provide panicking transformation operations. But now `String.Pos.slice!` could refer both to the panicking forwards transformation associated with `String.slice`, and also to the (only) forwards transformation associated with `String.slice!`. In this situation, we use an `orPanic` suffix to disambiguate. So the panicking forwards operation associated with `String.slice` is called `String.Pos.sliceOrPanic`, and the forwards operation associated with `String.slice!` is called `String.Pos.slice!`."
+  ]
+
+-- TODO: also include the `HAppend` instance(s)
 def sliceProducing : AssociationTable (β := Alias Lean.Name) .declaration
     [`String, `String.Slice,
      Alias.mk `String.Pos "string-pos-forwards" "String.Pos (forwards)",
@@ -23,16 +55,43 @@ def sliceProducing : AssociationTable (β := Alias Lean.Name) .declaration
      Alias.mk `String.Slice.Pos "string-slice-pos-backwards" "String.Slice.Pos (backwards)",
      Alias.mk `String.Slice.Pos "string-slice-pos-noproof" "String.Slice.Pos (no proof)"] where
   id := "slice-producing"
-  title := "String functions returning slices"
+  title := "String functions returning strings or slices"
   description := "Operations on strings and string slices that themselves return a new string slice."
   dataSources n := DataSource.definitionsInNamespace n.inner
 
+def sliceProducingComplete : Assertion where
+  widgetId := "slice-producing-complete"
+  title := "Slice-producing table is complete"
+  description := "All functions in the `String.**` namespace that return a string or a slice are covered in the table"
+  check := do
+    let mut ans := #[]
+    let covered := Std.HashSet.ofArray (← valuesInAssociationTable sliceProducing)
+    let pred : DataSource.DeclarationPredicate :=
+      DataSource.DeclarationPredicate.all [.isDefinition, .not .isDeprecated,
+        .notInNamespace `String.Pos.Raw, .notInNamespace `String.Legacy,
+        .not .isInstance]
+    let env ← getEnv
+    for name in ← declarationsMatching `String pred do
+      let some c := env.find? name | continue
+      if c.type.getForallBody.getUsedConstants.any (fun n => n == ``String || n == ``String.Slice) then
+        let success : Bool := name.toString ∈ covered
+        ans := ans.push {
+          assertionId := name.toString
+          description := s!"`{name}` should appear in the table."
+          passed := success
+          message := s!"`{name}` was{if success then "" else " not"} found in the table."
+        }
+    return ans
+
 end StringsAndFormatting
 
 open StringsAndFormatting
 
 def stringsAndFormatting : Node :=
   .section "strings-and-formatting" "Strings and formatting"
-    #[.associationTable sliceProducing]
+    #[.text introduction,
+      .text creatingStringsAndSlices,
+      .associationTable sliceProducing,
+      .assertion sliceProducingComplete]
 
 end GroveStdlib.Std.CoreTypesAndOperations

doc/std/grove/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": "backend",
    "scope": "",
-   "rev": "c19abde9101b29eb1e30d0d9d9e24ec2714f25b6",
+   "rev": "c580a425c9b7fa2aebaec2a1d8de16b2e2283c40",
    "name": "grove",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

src/Lean/Elab/App.lean

@@ -1314,6 +1314,16 @@ where
     | none => 0
     | some (_, p2) => prodArity p2 + 1
 
+/--
+For a fieldname `fieldName`, locate all the environment constants with that name
+-/
+private def reverseFieldLookup (env : Environment) (fieldName : String) :=
+  env.constants.fold (init := #[]) (fun accum name _ =>
+      match name with
+      | .str _ s => if s = fieldName && !name.isInternal then accum.push name else accum
+      | _ => accum)
+    |>.qsort (lt := Name.lt)
+
 private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM LValResolution := do
   match eType.getAppFn, lval with
   | .const structName _, LVal.fieldIdx ref idx =>
@@ -1379,11 +1389,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
       has function type{inlineExprTrailing eType}"
 
   | .mvar .., .fieldName _ fieldName _ _ =>
-    let possibleConstants := (← getEnv).constants.fold (fun accum name _ =>
-      match name with
-      | .str _ s => if s = fieldName && !name.isInternal then accum.push name else accum
-      | _ => accum) #[]
-    let hint := match possibleConstants with
+    let hint := match reverseFieldLookup (← getEnv) fieldName with
       | #[] => MessageData.nil
       | #[opt] => .hint' m!"Consider replacing the field projection `.{fieldName}` with a call to the function `{.ofConstName opt}`."
       | opts => .hint' m!"Consider replacing the field projection with a call to one of the following:\
@@ -1428,16 +1434,15 @@ where
           (suggestions.map fun suggestion => {
             preInfo? := .some s!"{e}.",
             suggestion := suggestion.getString!,
-            toCodeActionTitle? := .some (s!"Suggested replacement: {e}.{·}"),
+            toCodeActionTitle? := .some (s!"Change to {e}.{·}"),
             diffGranularity := .all,
           })
       else
         MessageData.hint (ref? := ref)
           m!"Perhaps you meant one of these in place of `{fullName}`:"
           (suggestions.map fun suggestion => {
             suggestion := suggestion.getString!,
-            toCodeActionTitle? := .some (s!"Suggested replacement: {e}.{·}"),
-            diffGranularity := .all,
+            toCodeActionTitle? := .some (s!"Change to {e}.{·}"),
             messageData? := .some m!"`{.ofConstName suggestion}`: {e}.{suggestion.getString!}",
           })
 
@@ -1765,8 +1770,17 @@ private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (expectedT
   withForallBody expectedType fun resultType => do
     go resultType expectedType #[]
 where
-  throwNoExpectedType :=
-    throwNamedError lean.invalidDottedIdent "Invalid dotted identifier notation: The expected type of `.{id}` could not be determined"
+  throwNoExpectedType := do
+    let hint ← match reverseFieldLookup (← getEnv) (id.getString!) with
+      | #[] => pure MessageData.nil
+      | suggestions =>
+        let oneOfThese := if h : suggestions.size = 1 then m!"`{.ofConstName suggestions[0]}" else m!"one of these"
+        m!"Using {oneOfThese} would be unambiguous:".hint (suggestions.map fun suggestion => {
+          suggestion := mkIdent suggestion
+          toCodeActionTitle? := .some (s!"Change to {·}")
+          messageData? := .some m!"`{.ofConstName suggestion}`",
+        })
+    throwNamedError lean.invalidDottedIdent (m!"Invalid dotted identifier notation: The expected type of `.{id}` could not be determined" ++ hint)
   /-- A weak version of forallTelescopeReducing that only uses whnfCore, to avoid unfolding definitions except by `unfoldDefinition?` below. -/
   withForallBody {α} (type : Expr) (k : Expr → TermElabM α) : TermElabM α := do
     let type ← whnfCoreUnfoldingAnnotations type

src/Lean/Elab/PatternVar.lean

@@ -67,35 +67,13 @@ private def throwCtorExpected {α} (ident : Option Syntax) : M α := do
 
   if candidates.size = 0 then
     throwError message
-  else if h : candidates.size = 1 then
-    throwError message ++ .hint' m!"`{candidates[0]}` is similar"
-  else
-    let sorted := candidates.qsort (·.toString < ·.toString)
-    let diff :=
-      if candidates.size > 10 then [m!" (or {candidates.size - 10} others)"]
-      else []
-    let suggestions : MessageData := .group <|
-      .joinSep ((sorted.extract 0 10 |>.toList |>.map (showName env)) ++ diff)
-        ("," ++ Format.line)
-    throwError message ++ .group (.hint' ("These are similar:" ++ .nestD (Format.line ++ suggestions)))
-where
-  -- Create some `MessageData` for a name that shows it without an `@`, but with the metadata that
-  -- makes infoview hovers and the like work. This technique only works because the names are known
-  -- to be global constants, so we don't need the local context.
-  showName (env : Environment) (n : Name) : MessageData :=
-    let params :=
-      env.constants.find?' n |>.map (·.levelParams.map Level.param) |>.getD []
-    .ofFormatWithInfos {
-      fmt := "'" ++ .tag 0 (format n) ++ "'",
-      infos :=
-        .ofList [(0, .ofTermInfo {
-          lctx := .empty,
-          expr := .const n params,
-          stx := .ident .none (toString n).toRawSubstring n [.decl n []],
-          elaborator := `Delab,
-          expectedType? := none
-        })] _
-    }
+  let oneOfThese := if h : candidates.size = 1 then m!"`{candidates[0]}`" else m!"one of these"
+  let hint ← m!"Using {oneOfThese} would be valid:".hint (ref? := idStx) (candidates.map fun candidate => {
+    suggestion := mkIdent candidate
+    toCodeActionTitle? := .some (s!"Change to {·}")
+    messageData? := .some m!"`{.ofConstName candidate}`",
+  })
+  throwError message ++ hint
 
 private def throwInvalidPattern {α} : M α :=
   throwError "Invalid pattern"

src/Lean/IdentifierSuggestion.lean

@@ -90,8 +90,7 @@ public def throwUnknownConstantWithSuggestions (constName : Name) : CoreM α :=
         let modified := modifySuggestion suggestion
         {
           suggestion := s!"{modified}",
-          toCodeActionTitle? := .some (s!"Suggested replacement: {·}"),
-          diffGranularity := .all,
-          -- messageData? := .some m!"replace `{.ofName rawId}` with `{.ofName modified}`",
+          toCodeActionTitle? := .some (s!"Change to {·}"),
+          messageData? := .some m!"`{.ofConstName suggestion}`",
         }) ref
   throwUnknownIdentifierAt (declHint := constName) ref (m!"Unknown constant `{.ofConstName constName}`" ++ hint)

src/Lean/Meta/Tactic/Try/Collect.lean

@@ -7,8 +7,6 @@ module
 prelude
 public import Init.Try
 public import Lean.Meta.Tactic.LibrarySearch
-public import Lean.Meta.Tactic.Grind.Cases
-public import Lean.Meta.Tactic.Grind.EMatchTheorem
 public import Lean.Meta.Tactic.FunIndCollect
 import Lean.Meta.Eqns
 public section

src/Lean/ProjFns.lean

@@ -36,13 +36,11 @@ def ProjectionFunctionInfo.fromClassEx (info : ProjectionFunctionInfo) : Bool :=
 
 builtin_initialize projectionFnInfoExt : MapDeclarationExtension ProjectionFunctionInfo ← mkMapDeclarationExtension
 
-@[export lean_add_projection_info]
 def addProjectionFnInfo (env : Environment) (projName : Name) (ctorName : Name) (numParams : Nat) (i : Nat) (fromClass : Bool) : Environment :=
   projectionFnInfoExt.insert env projName { ctorName, numParams, i, fromClass }
 
 namespace Environment
 
-@[export lean_get_projection_info]
 def getProjectionFnInfo? (env : Environment) (projName : Name) : Option ProjectionFunctionInfo :=
   projectionFnInfoExt.find? env projName