String uninterpolation

Stream: Is there code for X?

[Leni Aniva]

Is there a function which undoes string interpolation?

For example, suppose I want to test a string (12, 14) is of the form ({a}, {b}) and a + 2 = b. I need to extract a and b and test the equality a + 2 = b.

[Eric Wieser]

Is the string intended to be valid lean syntax?

[Leni Aniva]

Eric Wieser said:

Is the string intended to be valid lean syntax?

No

[Jireh Loreaux]

Isn't that just parsing? It sounds like you need to write a small parser for the strings relevant to you.

[Leni Aniva]

Jireh Loreaux said:

Isn't that just parsing? It sounds like you need to write a small parser for the strings relevant to you.

is there not something similar to scanf?

[Kyle Miller]

There's Parsec:

import Std.Internal.Parsec.String

open Std.Internal.Parsec Std.Internal.Parsec.String

class Unrepr (α : Type) where
  parse : Parser α
export Unrepr (parse)

instance : Unrepr Nat where
  parse := digits

def parsePair : Parser (Nat × Nat) := do
  skipChar '('
  let a ← parse
  skipChar ','
  let b ← parse
  skipChar ')'
  return (a, b)

def parseString (p : Parser α) (s : String) : Except String α :=
  match (p <* eof) s.mkIterator with
  | .success _ res => .ok res
  | .error _ msg => .error msg

#eval parseString parsePair "(1,2)"
-- Except.ok (1, 2)

[Kyle Miller]

It shouldn't be too hard of a project to make "parsec strings" like p!"({Nat},{Nat})" that return a tuple with all the parsed values.

[Kyle Miller]

Or maybe p!"({a},{b})" could be a doElem that defines a and b.

[Kyle Miller]

I forgot to generalize parsePair:

def parsePair [Unrepr α] [Unrepr β] : Parser (α × β) := do
  skipChar '('
  let a ← parse
  skipChar ','
  let b ← parse
  skipChar ')'
  return (a, b)