Strings without "

Stream: lean4

[Damiano Testa]

Dear All,

I would like to have a Try this that suggests replacing itself with a command.

I am able to get almost all the way there, except that there are some annoying quotations (") on the way! Here is a #mwe showing my problems.

import Std.Tactic.TryThis

open Lean Elab Command Term

syntax "writeMe" (ppSpace colGt str) : command

elab_rules : command
| `(command| writeMe $text:str) => liftTermElabM do
  let stx ← getRef
  let str ← elabTerm text none
  Std.Tactic.TryThis.addTermSuggestion stx str (origSpan? := stx)

writeMe "hello"  -- Try this: "hello"

These are the two issues that I am trying to solve.

1. Can the Try this: suggestion not print the quotations? I would like
   Try this: hello instead of Try this: "hello"

2. Can the input not have the quotations? I would like to type
   writeMe hello and get Try this: hello as a suggestion.

The strings that I am going to input will not contain any spaces, if that is relevant in any way.

A related thread but I would really like to have no syntax at all to introduce the strings.

Thanks!

[Damiano Testa]

To un #xy, I would like to achieve the following. When I want to add an import, I copy the relative path and I paste it. A code action suggests import [pasted code with `/` replaced by `.` and `.lean` removed].

Currently, I can make this work:

Mathlib/"Data/Nat/Basic.lean"  -- Try this: "import Mathlib.Data.Nat.Basic"

but I would like to not have to put in the double quotes in the input and then remove them from the output.

[Scott Morrison]

std4#215 might be helpful. It adds support for plain string suggestions (i.e. which not-already-parsed Syntax).

[Damiano Testa]

Scott, thanks! I'll take a look! From a very superficial glance at the description and the examples, this seems like it might address the Try this quotes. Of the two issues, I view this as the main one!

[Endor H]

If you want the input to not have the quotations you'll need to declare syntax for it, there's no way around that.
In your specific case you could define an importPath parser that takes slash-separated paths.

Regarding the output, one way to trick the TryThis tactic is declaring your own output syntax category with the syntax you want, though it's kind of a hack:

import Std.Tactic.TryThis

open Lean Elab Command Term PrettyPrinter Delaborator

namespace WriteMe
-- Unfortunately, the `.lean` part is not useful, since the `ident` parser is greedy
syntax importPath := sepBy1(ident, "/") (noWs ".lean")?
syntax "writeMe" (ppSpace colGt importPath) : command

declare_syntax_cat write_me_output_stx
syntax "import " ident : write_me_output_stx

elab_rules : command
| `(command| writeMe $[$parts]/*$[.lean]?) => liftTermElabM do
  let strParts := parts.map λs =>
    let s := s.getId.toString (escape := false)
    -- Remove the `.lean` suffix if any
    if s.endsWith ".lean" then s.dropRight 5 else s
  -- Concat the path parts with dots into a `Name`
  let name := strParts.foldl (fun (name : Name) part => name.str part) `Mathlib
  let stx ← getRef
  let replacement ← `(write_me_output_stx| import $(mkIdent name))
  Std.Tactic.TryThis.addSuggestion stx replacement (origSpan? := stx)
end WriteMe

writeMe Data/Nat/Basic.lean  -- Try this: import Mathlib.Data.Nat.Basic

Note that in the example I'm folding the parts into a Name directly, with Mathlib as the root, not into a string, since what you want to produce is actually a name in this case.

[Endor H]

Still, I agree this would be easier if the TryThis widget supported plain string suggestions.

[Endor H]

A more general workaround would be having a raw syntax category that accepted anything, but you'd probably need to declare a parser, a pretty printer, and maybe an elaborator/delaborator for it

[Endor H]

I'm not sure if anything like that already exists

[Damiano Testa]

I'm on mobile now, but thanks for the suggestions!

I had thought that maybe I could use Mathlib/ and .lean as markers for quoting the string. As for the conversion, I am using docs#Lean.moduleOfFileName to also make sure that the path exists. But these are details! I'll try out your suggestions!

[Endor H]

To have custom delimiters for a string you'd probably need a custom parser, similar to the idea of having a custom raw syntax category.

[Damiano Testa]

Honestly, I'm way beyond what I understand of parsing, but the thread linked to earlier already has a trick for that, I think.

[Endor H]

Hmm, I'm afraid the trick from that thread only works because what's between the delimiters is always an identifier, so it can use the identifier parser.
Honestly, I've only ever made a custom parser once, and it was quite an ordeal.

[Endor H]

I basically copied what's done in Lean.Parser.Basic.lean and Lean.Parser.Extra.lean where the built-in parsers are declared.
Maybe there's an easier way, but I wouldn't recommend unless necessary :laughing:

[Damiano Testa]

When I have something working, I'll post it here.

[Damiano Testa]

Thank you very much for your help! From what I can see on my phone, your approach basically should work for me! I might simply change a couple of details.

[Damiano Testa]

I have now what I wanted: a very tiny modification of @Endor H's suggestion: thank you very much!

import Std.Tactic.TryThis

open Lean Elab Command

namespace importMe

syntax importPath := sepBy1(ident, "/")
syntax "Mathlib" "/" (ppSpace colGt importPath) : command
declare_syntax_cat write_me_output_stx

syntax "import " ident : write_me_output_stx

def toSuggestion (root : String) (parts : Array (TSyntax `ident)) :
    TermElabM (TSyntax `write_me_output_stx) := do
  let strParts := parts.map fun s ↦ s.getId.toString (escape := false)
  -- Rebuild the path and interpret it as a `System.FilePath`.
  let path : System.FilePath := root ++ "/" ++ String.intercalate "/" strParts.toList
  let impS ← Lean.moduleNameOfFileName path none
  `(write_me_output_stx| import $(mkIdent impS))

elab_rules : command
| `(command| Mathlib/ $[$parts]/*) => liftTermElabM do
  let stx ← getRef
  let replacement ← toSuggestion "Mathlib" parts
  Std.Tactic.TryThis.addSuggestion stx replacement (origSpan? := stx)

end importMe

Mathlib/Data/Nat/Basic.lean  -- Try this: import Mathlib.Data.Nat.Basic

Mathlib/Not/A/Path.lean
/-
no such file or directory (error code: 2)
  file: Mathlib/Not/A/Path.lean
-/

[Patrick Massot]

Scott Morrison said:

std4#215 might be helpful. It adds support for plain string suggestions (i.e. which not-already-parsed Syntax).

This is great! However it now has a merge conflict.