add to doc-string

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

src/Init/Data/String/Basic.lean

@@ -515,6 +515,12 @@ def replace (s pattern replacement : String) : String :=
       termination_by s.endPos.1 - pos.1
     loop "" 0 0
 
+/-- Return the beginning of the line that contains character `pos`. -/
+def findLineStart (s : String) (pos : String.Pos) : String.Pos :=
+  match s.revFindAux (· = '\n') pos with
+  | none => 0
+  | some n => ⟨n.byteIdx + 1⟩
+
 end String
 
 namespace Substring

src/Lean/Data/Position.lean

@@ -84,6 +84,26 @@ partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
       -- Can also happen with EOF errors, which are not strictly inside the file.
       ⟨lines.back, (pos - ps.back).byteIdx⟩
 
+/-- Convert a `Lean.Position` to a `String.Pos`. -/
+def ofPosition (text : FileMap) (pos : Position) : String.Pos :=
+  let colPos :=
+    if h : pos.line - 1 < text.positions.size then
+      text.positions.get ⟨pos.line - 1, h⟩
+    else if text.positions.isEmpty then
+      0
+    else
+      text.positions.back
+  String.Iterator.nextn ⟨text.source, colPos⟩ pos.column |>.pos
+
+/--
+Returns the position of the start of (1-based) line `line`.
+This gives the stame result as `map.ofPosition ⟨line, 0⟩`, but is more efficient.
+-/
+def lineStart (map : FileMap) (line : Nat) : String.Pos :=
+  if h : line - 1 < map.positions.size then
+    map.positions.get ⟨line - 1, h⟩
+  else map.positions.back?.getD 0
+
 end FileMap
 end Lean
 

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean

@@ -40,11 +40,7 @@ def Value.toExpr (v : Value) : Expr :=
   unless e.isAppOfArity declName arity do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
   let some v₂ ← fromExpr? e.appArg! | return .continue
-  let d ← mkDecide e
-  if op v₁.value v₂.value then
-    return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
-  else
-    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
+  evalPropStep e (op v₁.value v₂.value)
 
 /-
 The following code assumes users did not override the `Fin n` instances for the arithmetic operators.

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean

@@ -47,11 +47,7 @@ def toExpr (v : Int) : Expr :=
   unless e.isAppOfArity declName arity do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
   let some v₂ ← fromExpr? e.appArg! | return .continue
-  let d ← mkDecide e
-  if op v₁ v₂ then
-    return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
-  else
-    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
+  evalPropStep e (op v₁ v₂)
 
 /-
 The following code assumes users did not override the `Int` instances for the arithmetic operators.

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Meta.Offset
 import Lean.Meta.Tactic.Simp.Simproc
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Util
 
 namespace Nat
 open Lean Meta Simp
@@ -28,11 +29,7 @@ def fromExpr? (e : Expr) : SimpM (Option Nat) := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appFn!.appArg! | return .continue
   let some m ← fromExpr? e.appArg! | return .continue
-  let d ← mkDecide e
-  if op n m then
-    return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
-  else
-    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
+  evalPropStep e (op n m)
 
 builtin_simproc [simp, seval] reduceSucc (Nat.succ _) := reduceUnary ``Nat.succ 1 (· + 1)
 

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean

@@ -41,11 +41,7 @@ def $toExpr (v : Value) : Expr :=
   unless e.isAppOfArity declName arity do return .continue
   let some n ← ($fromExpr e.appFn!.appArg!) | return .continue
   let some m ← ($fromExpr e.appArg!) | return .continue
-  let d ← mkDecide e
-  if op n.value m.value then
-    return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
-  else
-    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
+  evalPropStep e (op n.value m.value)
 
 builtin_simproc [simp, seval] $(mkIdent `reduceAdd):ident ((_ + _ : $typeName)) := reduceBin ``HAdd.hAdd 6 (· + ·)
 builtin_simproc [simp, seval] $(mkIdent `reduceMul):ident ((_ * _ : $typeName)) := reduceBin ``HMul.hMul 6 (· * ·)

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Util.lean

@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Tactic.Simp.Simproc
+
+namespace Lean.Meta.Simp
+
+/--
+Let `result` be the result of evaluating proposition `p`, return a `.done` step where
+the resulting expression is `True`(`False`) if `result is `true`(`false`), and the
+proof is uses `Decidable p` and the auxiliary theorems `eq_true_of_decide`/`eq_false_of_decide`.
+-/
+def evalPropStep (p : Expr) (result : Bool) : SimpM Step := do
+  let d ← mkDecide p
+  if result then
+    return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[p, d.appArg!, (← mkEqRefl (mkConst ``true))] }
+  else
+    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[p, d.appArg!, (← mkEqRefl (mkConst ``false))] }
+
+end Lean.Meta.Simp

src/Lean/Syntax.lean

@@ -305,6 +305,10 @@ def getRange? (stx : Syntax) (canonicalOnly := false) : Option String.Range :=
   | some start, some stop => some { start, stop }
   | _,          _         => none
 
+/-- Returns a synthetic Syntax which has the specified `String.Range`. -/
+def ofRange (range : String.Range) (canonical := true) : Lean.Syntax :=
+  .atom (.synthetic range.start range.stop canonical) ""
+
 /--
 Represents a cursor into a syntax tree that can be read, written, and advanced down/up/left/right.
 Indices are allowed to be out-of-bound, in which case `cur` is `Syntax.missing`.