Skip command if it doesn't parse

Stream: metaprogramming / tactics

[Eric Wieser]

Is it possible to write a nicer version of this?

import Lean

open Lean Elab Parser

def runParserCategoryOnLit (env : Environment) (catName : Name) (input : TSyntax `str) : MetaM Syntax := do
  let p := andthenFn whitespace (categoryParserFnImpl catName)
  -- replace the source with the unquoted versoin
  let .some pos := input.raw.getPos? | failure
  let pos := pos + ' '
  let map ← getFileMap
  let source := map.source.extract 0 pos ++ input.getString
  let ictx := {
    fileMap := ← getFileMap, fileName := ←getFileName,
    input := source }
  let s := p.run ictx { env, options := {} } (getTokenTable env) ({
      pos := pos
      cache := initCacheForInput source
  })
  if !s.allErrors.isEmpty  then
    throwError m!"{s.toErrorMsg ictx}"
  else if ictx.input.atEnd s.pos then
    return s.stxStack.back
  else
    let msg := (s.mkError "end of input").toErrorMsg ictx
    throwError m!"{msg}"

elab "try_parse_command" s:str : command => do
  let env ← getEnv
  let stx ← try
    Command.liftTermElabM <| runParserCategoryOnLit env `command s
  catch e =>
    Lean.logWarning m!"Skipping: {e.toMessageData}"
    return
  Command.elabCommand stx

-- works
try_parse_command "run_cmd Lean.logInfo \"nice\""

-- ignores the failure, as intended
try_parse_command "some_unimplemented_cmd"

-- error message is in the wrong position; can we drop the quotes?
try_parse_command "run_cmd Lean.logInfo \"oops\n\n\n\n\n\n\n\" + 'c' "

[Eric Wieser]

In particular, the \ escapes inside the string literal mess with the error positions

[Robin Arnez]

You'll have to write your own string decode functions:

import Lean
import Std

open Lean Elab Parser

partial def decodeStrLitWithPositionMapAux (s : String) (off : String.Pos) (i : String.Pos) (acc : String) :
    StateT (Array String.Pos) Option String := do
  let istart := i
  let c := s.get i
  let i := s.next i
  if c == '\x22' then -- '\"' except zulip doesn't like that
    modify fun posMap => posMap.push (off + istart)
    pure acc
  else if s.atEnd i then
    none
  else if c == '\\' then do
    if let some (c, i') := Syntax.decodeQuotedChar s i then
      modify fun posMap => posMap ++ Array.replicate c.utf8Size (off + istart)
      decodeStrLitWithPositionMapAux s off i' (acc.push c)
    else if let some i := Syntax.decodeStringGap s i then
      decodeStrLitWithPositionMapAux s off i acc
    else
      none
  else
    modify fun posMap => posMap ++ Array.replicate c.utf8Size (off + istart)
    decodeStrLitWithPositionMapAux s off i (acc.push c)

partial def decodeRawStrLitWithPositionMapAux (s : String) (off : String.Pos) (i : String.Pos) (num : Nat) : String × Array String.Pos :=
  let c := s.get i
  let i := s.next i
  if c == '#' then
    decodeRawStrLitWithPositionMapAux s off i (num + 1)
  else
    let str := s.extract i ⟨s.utf8ByteSize - (num + 1)⟩
    (str, (0...=str.utf8ByteSize).iter.map (fun n => off + i + ⟨n⟩) |>.toArray)

def decodeStrLitWithPositionMap (s : String) (off : String.Pos) : Option (String × Array String.Pos) :=
  if s.get 0 == 'r' then
    some <| decodeRawStrLitWithPositionMapAux s off ⟨1⟩ 0
  else
    (decodeStrLitWithPositionMapAux s off ⟨1⟩ "").run #[]

def Lean.TSyntax.getStringWithPositionMap (stx : StrLit) : String × Array String.Pos :=
  match stx.raw with
  | Syntax.node _ k args =>
    if h : k == strLitKind ∧ args.size = 1 then
      match args[0]'(Nat.lt_of_sub_eq_succ h.2) with
      | Syntax.atom info val => (decodeStrLitWithPositionMap val (info.getPos?.getD 0)).getD ("", #[])
      | _ => ("", #[])
    else
      ("", #[])
  | _ => ("", #[])

def Lean.Syntax.mapInfo (stx : Syntax) (f : SourceInfo → SourceInfo) : Syntax :=
  match stx with
  | .missing => .missing
  | .atom info val => .atom (f info) val
  | .ident info rawVal val pre => .ident (f info) rawVal val pre
  | .node info kind args => .node (f info) kind (args.map (·.mapInfo f))

def runParserCategoryOnLit (catName : Name) (input : TSyntax `str) : MetaM Syntax := do
  let pmctx : ParserModuleContext := { env := ← getEnv, options := ← getOptions, currNamespace := ← getCurrNamespace, openDecls := ← getOpenDecls }
  let p := andthenFn whitespace (categoryParserFnImpl catName)
  let map ← getFileMap
  let (str, posMap) := input.getStringWithPositionMap
  let ictx := {
    fileMap := FileMap.ofString str, fileName := ← getFileName,
    input := str }
  let s := p.run ictx pmctx (getTokenTable (← getEnv)) ({
      pos := 0
      cache := initCacheForInput str
  })
  let mapSubstring : Substring → Substring
    | ⟨_, startPos, endPos⟩ => ⟨map.source, posMap[startPos.byteIdx]!, posMap[endPos.byteIdx]!⟩
  if !s.allErrors.isEmpty then
    throwError m!"{s.toErrorMsg ictx}"
  else if ictx.input.atEnd s.pos then
    return s.stxStack.back.mapInfo fun
      | .original l p t e => .original (mapSubstring l) posMap[p.byteIdx]! (mapSubstring t) posMap[e.byteIdx]!
      | info => info
  else
    let msg := (s.mkError "end of input").toErrorMsg ictx
    throwError m!"{msg}"

elab "try_parse_command" s:str : command => do
  let stx ← try
    Command.liftTermElabM <| runParserCategoryOnLit `command s
  catch e =>
    Lean.logWarning m!"Skipping: {e.toMessageData}"
    return
  Command.elabCommand stx

[Edward van de Meent]

are you looking for something like #check_failure?

[Eric Wieser]

That doesn't work for parse failures

[Eric Wieser]

And #parse doesn't run the command when it succeeds

[Damiano Testa]

Maybe we could add a flag to #parse, to make it also run the command?

[Robin Arnez]

The purpose of #parse is testing parsing, not elaboration though, isn't it?

[Robin Arnez]

Anyways, what exactly do you need this for?

[Kyle Miller]

You can sidestep the escaping issue by using raw strings. Here's an implementation that requires raw strings then looks into the atom itself to figure out the size of the r###" prefix:

code

import Lean

open Lean Elab Parser

def runParserCategoryOnLit (env : Environment) (catName : Name) (input : TSyntax `str) : MetaM Syntax := do
  -- The string might be malformed; abort if it is.
  let some inputStr := input.raw.isStrLit? | throwUnsupportedSyntax
  -- Check that it is a raw string and determine the prefix size 'r###"'
  let rawVal := input.raw[0].getAtomVal
  unless rawVal.get 0 == 'r' do throwErrorAt input "expecting a raw string literal"
  let offset := rawVal.find (· == '"')
  let p := andthenFn whitespace (categoryParserFnImpl catName)
  -- replace the source with the unquoted versoin
  let .some pos := input.raw.getPos? | failure
  let pos := pos + offset + ' '
  let map ← getFileMap
  let source := map.source.extract 0 pos ++ input.getString
  let ictx := {
    fileMap := ← getFileMap, fileName := ←getFileName,
    input := source }
  let s := p.run ictx { env, options := {} } (getTokenTable env) ({
      pos := pos
      cache := initCacheForInput source
  })
  if !s.allErrors.isEmpty  then
    throwError m!"{s.toErrorMsg ictx}"
  else if ictx.input.atEnd s.pos then
    return s.stxStack.back
  else
    let msg := (s.mkError "end of input").toErrorMsg ictx
    throwError m!"{msg}"

elab "try_parse_command" s:str : command => do
  let env ← getEnv
  let stx ← try
    Command.liftTermElabM <| runParserCategoryOnLit env `command s
  catch e =>
    Lean.logWarning m!"Skipping: {e.toMessageData}"
    return
  Command.elabCommand stx
-- works
try_parse_command "run_cmd Lean.logInfo \"nice\""
-- ignores the failure, as intended
try_parse_command "some_unimplemented_cmd"
-- error message is in the wrong position; can we drop the quotes?
try_parse_command r###"run_cmd Lean.logInfo "oops\n\n\n\n\n\n\n" + 'c' "###

Example:

try_parse_command r###"run_cmd Lean.logInfo "oops\n\n\n\n\n\n\n" + 'c' "###
--                             ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~