sscanf macro

Stream: general

[Conor Bergin]

Is it be possible to write a macro like sscanf!"{String}: {Nat} - {Nat}" that would return an Option (String x Nat x Nat) the tuple type being the same as whatever was in the format string? Rust has a crate for this which I use a lot and I would like to have it in lean.

[Conor Bergin]

https://docs.rs/sscanf/latest/sscanf/

[Kyle Miller]

Yeah, you should be able to write such a macro without too much work. You could use interpStr to parse these curly brace strings in a general way, but you'd have to figure out how to encode parsing options somehow.

[Kyle Miller]

@Conor Bergin Here's a prototype:

code

import Lean

open Lean Elab

declare_syntax_cat parsecTerm
declare_syntax_cat parsecSpec

syntax (term)? (" : " parsecSpec)? : parsecTerm

syntax (name := parsecStr) "parsec!" interpolatedStr(parsecTerm) : term

syntax "r16" : parsecSpec

/-- Represents the data after the `:` in a `parsec!` string,
along with other incidental configuration. -/
structure ParsecSpec where
  /-- If not `none`, parse without including this character.
  This comes from the character immediately after the `}`. -/
  untilChar? : Option Char
  radix : Nat := 10

instance : Quote Char where
  quote c :=
    let digs := Nat.toDigits 16 c.toNat
    let digs := (List.replicate (4 - digs.length) '0') ++ digs
    let n := String.mk digs
    Syntax.mkLit charLitKind s!"'\\u{n}'"

instance : Quote ParsecSpec where
  quote spec := Unhygienic.run
    `(ParsecSpec.mk $(quote spec.untilChar?) $(quote spec.radix))

/-- Predicate for the character not being the one in `untilChar?`. -/
def ParsecSpec.notUntilChar (spec : ParsecSpec) (c : Char) : Bool :=
  spec.untilChar? |>.map (· != c) |>.getD true

/-- Class for associating parsers to types. -/
class ParsecParse (α : Type) where
  parse : ParsecSpec → Lean.Parsec α

instance : ParsecParse Nat where
  parse spec := do
    -- TODO: Should handle `spec.radix` in here.
    let chars ← Parsec.many1Chars (Parsec.satisfy fun c => c.isDigit && spec.notUntilChar c)
    return chars.toNat!

instance : ParsecParse String where
  parse spec := Parsec.manyChars (Parsec.satisfy spec.notUntilChar)

/-- Modify the `spec` given the contents of `specStx?`. -/
def processParsecSpec (specStx? : Option (TSyntax `parsecSpec)) (spec : ParsecSpec) :
    MacroM ParsecSpec :=
  match specStx? with
  | some specStx =>
    match specStx with
    | `(parsecSpec| r16) => return {spec with radix := 16}
    | _ => Macro.throwUnsupported
  | none => return spec

def processParsecTerm (term : TSyntax `parsecTerm) (untilChar? : Option Char) :
    MacroM (Term × ParsecSpec) := do
  match term with
  | `(parsecTerm| $[$ty?]? $[: $spec?]?) =>
    let spec ← processParsecSpec spec? {untilChar?}
    let ty ← if let some ty := ty? then pure ty else `(_)
    return (ty, spec)
  | _ => Macro.throwUnsupported

def mkTuple (xs : Array Term) : MacroM Term :=
  match xs with
  | #[] => `(())
  | #[x] => return x
  | _ => `(($(xs[0]!), $(xs[1:]),*))

def expandChunks (chunks : Array Syntax) : MacroM Term := withFreshMacroScope do
  -- Array of binder/parser pairs
  let mut parsers : List (Option Term × Term) := []
  let mut res : List Term := []
  let mut untilChar? : Option Char := none
  for j in [0:chunks.size] do
    -- Reverse order for `untilChar?` handling
    let i := chunks.size - 1 - j
    let elem := chunks[i]!
    match elem.isInterpolatedStrLit? with
      | none =>
        let n := mkIdentFrom elem (← MonadQuotation.addMacroScope (Name.appendIndexAfter `n i))
        let (ty, spec) ← processParsecTerm ⟨elem⟩ untilChar?
        parsers := (n, ← `((ParsecParse.parse $(quote spec) : Parsec $ty))) :: parsers
        res := n :: res
        untilChar? := none
      | some str =>
        if str.utf8ByteSize > 0 then
          parsers := (none, ← `(Parsec.skipString $(quote str))) :: parsers
        untilChar? := str.get? ⟨0⟩
  let res' ← `(pure $(← mkTuple res.toArray))
  parsers.foldrM (init := res') fun (binder?, parser) t => do
    if let some binder := binder? then
      `($parser >>= fun $binder => $t)
    else
      `($parser *> $t)

macro_rules
  | `(parsec! $str) => do
    let t ← expandChunks str.raw.getArgs
    return t

#check parsec!"{String}: {Nat} - {Nat}"
/-
do
  let n_1 ← ParsecParse.parse { untilChar? := some (Char.ofNat 58) }
  SeqRight.seqRight (Parsec.skipString ": ") fun x ↦ do
      let n_3 ← ParsecParse.parse { untilChar? := some (Char.ofNat 32) }
      SeqRight.seqRight (Parsec.skipString " - ") fun x ↦ do
          let n_5 ← ParsecParse.parse { untilChar? := none }
          pure (n_1, n_3, n_5) : Parsec (String × Nat × Nat)
-/

#eval (parsec!"{String}: {Nat} - {Nat}").run "entry1: 1 - 2"
/-
Except.ok ("entry1", 1, 2)
-/

-- This works too:
#eval (parsec!"{}: {} - {}" : Parsec (String × Nat × Nat)).run "entry1: 1 - 2"

[Kyle Miller]

A couple examples:

#eval (parsec!"{String}: {Nat} - {Nat}").run "entry1: 1 - 2"
/-
Except.ok ("entry1", 1, 2)
-/

-- This works too:
#eval (parsec!"{}: {} - {}" : Parsec (String × Nat × Nat)).run "entry1: 1 - 2"

[Kyle Miller]

This theoretically supports radix specifiers like {Nat : r16} but I didn't implement this part.

[Kyle Miller]

Here's an example of extensibility:

structure Color where
  (r g b : Nat)
  deriving Repr

instance : ParsecParse Color where
  parse _ := do
    let (r, g, b) ← parsec!"({},{},{})"
    return {r, g, b}

#eval (parsec!"color = {Color}").run "color = (1,2,3)"
/-
Except.ok { r := 1, g := 2, b := 3 }
-/

[Conor Bergin]

This looks great, I wasn't expecting a working prototype within an hour! I am still working through the macro docs so it'll take me a bit to understand all of this.