max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: allow separate handlers for literals and interpolations in expandInterpolatedStr (#6763)

Browse source 
This PR makes it possible to write custom interpolation notation which
treats interpolated `String`s specially.

Sometimes it is desirable for `let w := "world"; foo!"hello {w}"` and
`foo!"hello world"` to mean different things; for instance, if debugging
and wanting to show all interpolands with `repr`. The current approach
forces `hello` to also be rendered with `repr`, which is not desirable.

This doesn't modify any existing formatters.

Requested in [#lean4 > ✔ dbg_trace should use `Repr` instance @
💬](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.E2.9C.94.20dbg_trace.20should.20use.20.60Repr.60.20instance/near/495082575)

---------

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This commit is contained in:
Eric Wieser 2025-09-10 14:22:17 +01:00 • committed by GitHub
parent 0a6bd5c0c6
commit fbcad8f593
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 12 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/Init/Meta.lean
View file

@ -1518,26 +1518,33 @@ end Syntax
namespace TSyntax
def expandInterpolatedStrChunks (chunks : Array Syntax) (mkAppend : Syntax → Syntax → MacroM Syntax) (mkElem : Syntax → MacroM Syntax) : MacroM Syntax := do
def expandInterpolatedStrChunks (chunks : Array Syntax) (mkAppend : Syntax → Syntax → MacroM Syntax)
(mkElem : Syntax → MacroM Syntax) (mkLit : String → MacroM Syntax) : MacroM Syntax := do
let mut result := Syntax.missing
for elem in chunks do
let elem ← match elem.isInterpolatedStrLit? with
| none => withRef elem <| mkElem elem
| some str =>
if String.Internal.isEmpty str then continue
else withRef elem <| mkElem (Syntax.mkStrLit str)
else withRef elem <| mkLit str
if result.isMissing then
result := elem
else
result ← mkAppend result elem
if result.isMissing then
mkElem (Syntax.mkStrLit "")
mkLit ""
else
return result
open TSyntax.Compat in
def expandInterpolatedStr (interpStr : TSyntax interpolatedStrKind) (type : Term) (toTypeFn : Term) : MacroM Term := do
let r ← expandInterpolatedStrChunks interpStr.raw.getArgs (fun a b => `($a ++ $b)) (fun a => `($toTypeFn $a))
/-- Expand `interpStr` into a term of type `type` (which supports ` ++ `),
calling `ofInterpFn` on terms within `{}`,
and `ofLitFn` on the literals between the interpolations. -/
def expandInterpolatedStr (interpStr : TSyntax interpolatedStrKind) (type : Term) (ofInterpFn : Term) (ofLitFn : Term := ofInterpFn) : MacroM Term := do
let r ← expandInterpolatedStrChunks interpStr.raw.getArgs
(fun a b => `($a ++ $b))
(fun a => `($ofInterpFn $a))
(fun s => `($ofLitFn $(Syntax.mkStrLit s)))
`(($r : $type))
def getDocString (stx : TSyntax `Lean.Parser.Command.docComment) : String :=