From 673d03e57fa26a0c370454905713759c69215f01 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 22 Mar 2024 02:18:40 +0000 Subject: [PATCH] chore: don't use String->Name coercion, which may be removed (#11556) Co-authored-by: Scott Morrison --- Mathlib/Lean/Name.lean | 1 + Mathlib/Tactic/ComputeDegree.lean | 2 +- Mathlib/Tactic/DeriveTraversable.lean | 22 +++++++++++----------- Mathlib/Tactic/FunProp/ToStd.lean | 2 +- Mathlib/Tactic/HelpCmd.lean | 2 +- Mathlib/Tactic/IntervalCases.lean | 2 +- Mathlib/Tactic/ProjectionNotation.lean | 4 ++-- Mathlib/Tactic/TFAE.lean | 2 +- Mathlib/Tactic/ToAdditive.lean | 3 ++- 9 files changed, 21 insertions(+), 19 deletions(-) diff --git a/Mathlib/Lean/Name.lean b/Mathlib/Lean/Name.lean index bd7d0f1d1f08d..a7b3a31b8f744 100644 --- a/Mathlib/Lean/Name.lean +++ b/Mathlib/Lean/Name.lean @@ -6,6 +6,7 @@ Authors: Scott Morrison import Std.Data.HashMap.Basic import Std.Lean.SMap import Std.Lean.Name +import Lean.Meta.Match.MatcherInfo /-! # Additional functions on `Lean.Name`. diff --git a/Mathlib/Tactic/ComputeDegree.lean b/Mathlib/Tactic/ComputeDegree.lean index b14e7ed66d3c7..78d7fbd799f63 100644 --- a/Mathlib/Tactic/ComputeDegree.lean +++ b/Mathlib/Tactic/ComputeDegree.lean @@ -271,7 +271,7 @@ def getCongrLemma (twoH : Name × Name × List Bool) (debug : Bool := false) : N | true, true => ``id | _ => ``id if debug then - let natr := if nam.getString == `trans then nam else nam.getString + let natr := if nam.getString == "trans" then nam.toString else nam.getString dbg_trace f!"congr lemma: '{natr}'" nam else diff --git a/Mathlib/Tactic/DeriveTraversable.lean b/Mathlib/Tactic/DeriveTraversable.lean index 0de1a84674d9c..7c51bbb5ccfa4 100644 --- a/Mathlib/Tactic/DeriveTraversable.lean +++ b/Mathlib/Tactic/DeriveTraversable.lean @@ -85,7 +85,7 @@ This is convenient to make a definition with equation lemmas. -/ def mkCasesOnMatch (type : Name) (levels : List Level) (params : List Expr) (motive : Expr) (indices : List Expr) (val : Expr) (rhss : (ctor : Name) → (fields : List FVarId) → TermElabM Expr) : TermElabM Expr := do - let matcherName ← getDeclName? >>= (fun n? => Lean.mkAuxName (n?.getD type ++ "match") 1) + let matcherName ← getDeclName? >>= (fun n? => Lean.mkAuxName (.mkStr (n?.getD type) "match") 1) let matchType ← generalizeTelescope (indices.concat val).toArray fun iargs => mkForallFVars iargs (motive.beta iargs) let iinfo ← getConstInfoInduct type @@ -158,8 +158,8 @@ def deriveFunctor (m : MVarId) : TermElabM Unit := do let d ← getConstInfo n let [m] ← run m <| evalTactic (← `(tactic| refine { map := @(?_) })) | failure let t ← m.getType >>= instantiateMVars - let n' := n ++ "map" - withDeclName n' <| withAuxDecl "map" t n' fun ad => do + let n' := .mkStr n "map" + withDeclName n' <| withAuxDecl (.mkSimple "map") t n' fun ad => do let m' := (← mkFreshExprSyntheticOpaqueMVar t).mvarId! mkMap n m' let e ← instantiateMVars (mkMVar m') @@ -285,7 +285,7 @@ def deriveLawfulFunctor (m : MVarId) : TermElabM Unit := do xs.forM fun ⟨mim, _, _⟩ => mim.withContext do if let (some (_, mim), _) ← - simpGoal mim (← rules [(``Functor.map_id, false)] [n ++ "map"] true) then + simpGoal mim (← rules [(``Functor.map_id, false)] [.mkStr n "map"] true) then mim.refl let (#[_, _, _, _, _, x], mcm) ← mcm.introN 6 | failure let (some mcm, _) ← dsimpGoal mcm (← rules [] [``Functor.map] false) | failure @@ -293,7 +293,7 @@ def deriveLawfulFunctor (m : MVarId) : TermElabM Unit := do xs.forM fun ⟨mcm, _, _⟩ => mcm.withContext do if let (some (_, mcm), _) ← - simpGoal mcm (← rules [(``Functor.map_comp_map, true)] [n ++ "map"] true) then + simpGoal mcm (← rules [(``Functor.map_comp_map, true)] [.mkStr n "map"] true) then mcm.refl /-- The deriving handler for `LawfulFunctor`. -/ @@ -399,8 +399,8 @@ def deriveTraversable (m : MVarId) : TermElabM Unit := do let d ← getConstInfo n let [m] ← run m <| evalTactic (← `(tactic| refine { traverse := @(?_) })) | failure let t ← m.getType >>= instantiateMVars - let n' := n ++ "traverse" - withDeclName n' <| withAuxDecl "traverse" t n' fun ad => do + let n' := .mkStr n "traverse" + withDeclName n' <| withAuxDecl (.mkSimple "traverse") t n' fun ad => do let m' := (← mkFreshExprSyntheticOpaqueMVar t).mvarId! mkTraverse n m' let e ← instantiateMVars (mkMVar m') @@ -472,12 +472,12 @@ def deriveLawfulTraversable (m : MVarId) : TermElabM Unit := do let .app (.app (.const ``LawfulTraversable _) F) _ ← m.getType >>= instantiateMVars | failure let some n := F.getAppFn.constName? | failure let [mit, mct, mtmi, mn] ← m.applyConst ``LawfulTraversable.mk | failure - let defEqns : MetaM Simp.Context := rules [] [n ++ "map", n ++ "traverse"] true + let defEqns : MetaM Simp.Context := rules [] [.mkStr n "map", .mkStr n "traverse"] true traversableLawStarter mit n defEqns fun _ _ m => m.refl traversableLawStarter mct n defEqns fun _ _ m => do - if let (some (_, m), _) ← - simpFunctorGoal m (← rules [] [n ++ "map", n ++ "traverse", ``Function.comp] true) then - m.refl + if let (some (_, m), _) ← simpFunctorGoal m + (← rules [] [.mkStr n "map", .mkStr n "traverse", ``Function.comp] true) then + m.refl traversableLawStarter mtmi n defEqns fun _ _ m => do if let (some (_, m), _) ← simpGoal m (← rules [(``Traversable.traverse_eq_map_id', false)] [] false) then diff --git a/Mathlib/Tactic/FunProp/ToStd.lean b/Mathlib/Tactic/FunProp/ToStd.lean index 77e6dc2e2382f..48480b70cd606 100644 --- a/Mathlib/Tactic/FunProp/ToStd.lean +++ b/Mathlib/Tactic/FunProp/ToStd.lean @@ -109,7 +109,7 @@ def mkUncurryFun (n : Nat) (f : Expr) : MetaM Expr := do do return (n ++ toString (← x.fvarId!.getUserName).eraseMacroScopes) let xProdType ← inferType (← mkProdElem xs) - withLocalDecl xProdName default xProdType λ xProd => do + withLocalDecl (.mkSimple xProdName) default xProdType λ xProd => do let xs' ← mkProdSplitElem xProd n mkLambdaFVars #[xProd] (← mkAppM' f xs').headBeta diff --git a/Mathlib/Tactic/HelpCmd.lean b/Mathlib/Tactic/HelpCmd.lean index 459df05d7eee7..6f39bf9837bca 100644 --- a/Mathlib/Tactic/HelpCmd.lean +++ b/Mathlib/Tactic/HelpCmd.lean @@ -66,7 +66,7 @@ private def elabHelpOption (id : Option Ident) : CommandElabM Unit := do | .ofNat val => s!"Nat := {repr val}" | .ofInt val => s!"Int := {repr val}" | .ofSyntax val => s!"Syntax := {repr val}" - if let some val := opts.find name then + if let some val := opts.find (.mkSimple name) then msg1 := s!"{msg1} (currently: {val})" msg := msg ++ .nest 2 (f!"option {name} : {msg1}" ++ .line ++ decl.descr) ++ .line ++ .line logInfo msg diff --git a/Mathlib/Tactic/IntervalCases.lean b/Mathlib/Tactic/IntervalCases.lean index 3b7437e51cab3..231217e805ddb 100644 --- a/Mathlib/Tactic/IntervalCases.lean +++ b/Mathlib/Tactic/IntervalCases.lean @@ -308,7 +308,7 @@ def intervalCases (g : MVarId) (e e' : Expr) (lbs ubs : Array Expr) (mustUseBoun let z := lo+i let rhs ← m.mkNumeral z let ty ← mkArrow (← mkEq e rhs) tgt - let goal ← mkFreshExprMVar ty .syntheticOpaque (appendTag tag (toString z)) + let goal ← mkFreshExprMVar ty .syntheticOpaque (appendTag tag (.mkSimple (toString z))) goals := goals.push { rhs, value := z, goal := goal.mvarId! } m.bisect g goals.toSubarray z1 z2 e1 e2 p1 p2 e pure goals diff --git a/Mathlib/Tactic/ProjectionNotation.lean b/Mathlib/Tactic/ProjectionNotation.lean index 40bfe646bddb3..f8b7cecd69cde 100644 --- a/Mathlib/Tactic/ProjectionNotation.lean +++ b/Mathlib/Tactic/ProjectionNotation.lean @@ -39,14 +39,14 @@ def mkExtendedFieldNotationUnexpander (f : Name) : CommandElabM Unit := do aux_def $(mkIdent <| Name.str f "unexpander") : Lean.PrettyPrinter.Unexpander := fun -- Having a zero-argument pattern prevents unnecessary parenthesization in output | `($$_ $$(x).$(mkIdent toA)) - | `($$_ $$x) => set_option hygiene false in `($$(x).$(mkIdent projName)) + | `($$_ $$x) => set_option hygiene false in `($$(x).$(mkIdent (.mkSimple projName))) | _ => throw ()) else elabCommand <| ← `(command| @[app_unexpander $(mkIdent f)] aux_def $(mkIdent <| Name.str f "unexpander") : Lean.PrettyPrinter.Unexpander := fun -- Having this zero-argument pattern prevents unnecessary parenthesization in output - | `($$_ $$x) => set_option hygiene false in `($$(x).$(mkIdent projName)) + | `($$_ $$x) => set_option hygiene false in `($$(x).$(mkIdent (.mkSimple projName))) | _ => throw ()) /-- diff --git a/Mathlib/Tactic/TFAE.lean b/Mathlib/Tactic/TFAE.lean index 4594db66cf4d4..25c31d51a1827 100644 --- a/Mathlib/Tactic/TFAE.lean +++ b/Mathlib/Tactic/TFAE.lean @@ -165,7 +165,7 @@ def mkTFAEHypName (i j : TSyntax `num) (arr : TSyntax ``impArrow) : MetaM Name : | `(impArrow| → ) => pure "to" | `(impArrow| ↔ ) => pure "iff" | _ => throwErrorAt arr "expected '←', '→', or '↔'" - return String.intercalate "_" ["tfae", s!"{i.getNat}", arr, s!"{j.getNat}"] + return .mkSimple <| String.intercalate "_" ["tfae", s!"{i.getNat}", arr, s!"{j.getNat}"] open Elab in /-- The core of `tfae_have`, which behaves like `haveLetCore` in `Mathlib.Tactic.Have`. -/ diff --git a/Mathlib/Tactic/ToAdditive.lean b/Mathlib/Tactic/ToAdditive.lean index 9b9a13c69a9f6..c6133d37169c0 100644 --- a/Mathlib/Tactic/ToAdditive.lean +++ b/Mathlib/Tactic/ToAdditive.lean @@ -1086,7 +1086,8 @@ def proceedFields (src tgt : Name) : CoreM Unit := do else return #[] aux fun declName ↦ do match (← getEnv).find? declName with - | some (ConstantInfo.inductInfo {ctors := ctors, ..}) => return ctors.toArray.map (·.getString) + | some (ConstantInfo.inductInfo {ctors := ctors, ..}) => + return ctors.toArray.map (.mkSimple ·.getString) | _ => pure #[] /-- Elaboration of the configuration options for `to_additive`. -/