Parsing a string

Stream: metaprogramming / tactics

[Jon Eugster]

I don't fully understand how parsing works and all, but can I somehow feed some String to a parser to get a new syntax object from it?

Concretely, I'm trying to modify an interpolated string before feeding it back to s!. I had hoped this would be cleaner than duplicating all of the backend of s!. Is that possible?

Here's a MWE:

import Lean

open Lean Elab Term

syntax:max "t!" interpolatedStr(term) : term

elab_rules : term
  | `(t! $interpStr) => withFreshMacroScope do
    let key : String := "…replace it with this {1+1}"
    -- TODO: try to parse `key` and feed it to `s!` below
    let modified : TSyntax `interpolatedStrKind := interpStr
    Term.elabTerm (← `(s! $modified)) none

#eval t!"starting with this {1+2}…"

[Jon Eugster]

I'd hope this could print …replace it with this 2 in the infoview.

[Adam Topaz]

I think docs#Lean.Parser.runParserCategory is useful for this?

[Kyle Miller]

There isn't too much code you need for processing an interpolatedStr(term). The idea is that the underlying Syntax is an array of strings or terms, and you can loop through them and do whatever processing you want, depending on which of the two it is.

If you want more examples, the first two functions in the Basic file in this message show some processing. That creates a separate term, but you could have the output be another interpolatedStrKind.

[Jon Eugster]

@Kyle Miller I indeed took your code there as inspiration:grinning_face_with_smiling_eyes: but I'd like to use .po files for the translation part. I have the creation of that .po file down fine, but now I need to parse it again to get the translations into lean. And that's where I thought the easiest would be to just re-parse the translated string as an interpolated string.

[Jon Eugster]

thanks @Adam Topaz, got it working :)

working example

import Lean

open Lean Elab Term Parser

syntax:max "t!" interpolatedStr(term) : term

/-- Parse a string as an interpolated string.

Modified from `Lean.Parser.runParserCategory`.
 -/
def runInterpolatedStrParser (env : Environment) (input : String) (fileName := "<input>") :
    Except String <| TSyntax `interpolatedStrKind :=
  let input := s!"\"{input}\""
  let p := interpolatedStrFn <| andthenFn whitespace (categoryParserFnImpl `term)
  let ictx := mkInputContext input fileName
  let s := p.run ictx { env, options := {} } (getTokenTable env) (mkParserState input)
  if s.hasError then
    Except.error (s.toErrorMsg ictx)
  else if input.atEnd s.pos then
    Except.ok ⟨s.stxStack.back⟩
  else
    Except.error ((s.mkError "end of input").toErrorMsg ictx)

elab_rules : term
  | `(t! $interpStr) => withFreshMacroScope do
    let key : String := "…replace it with this {1+1}"

    match runInterpolatedStrParser (← getEnv) key with
      | .ok modified =>
        Term.elabTerm (← `(s! $modified)) none
      | .error err =>
        logError s!"Could not parse translated string: {err}\n\ninput: {key}"
        Term.elabTerm (← `(s! $interpStr)) none

#eval t!"starting with this {1+2}…"