Syntax to parse binary strings

Stream: new members

[Fady Adal]

Hello!

I am trying to embed a DSL to be able to write qubit states in string form (e.g. ∣0100⟩) and be able to translate them to kronecker products. Part of that means I want to have a syntax like the following:

syntax (name := qubits) "∣" ("0" <|> "1")+ "⟩" : term

But doing so tells me that "0" is an "invalid atom".

I know one compromise I can make it to have

syntax (name := qubits) "∣" char+ "⟩" : term
@[macro qubits] def qubitsImpl : Macro
  | `( ∣ $bits* ⟩ ) => do
    let bools ← bits.mapM fun bit =>
    match bit.getChar with
    | '0' => `(false)
    | '1' => `(true)
    | _ => Macro.throwError "Invalid qubit string"
    `([$bools,*])
  | _ => Macro.throwUnsupported

But this would make me have to specify qubits as ∣'0''0'⟩ which is too verbose. Similarly, if I use the num syntax ∣00⟩ is understood as just ∣0⟩.

I there a way to make a new syntax that parses binary strings, without having to resort to either num or char or in a way to addresses those hiccups I laid out?

Thank you so much

[Asei Inoue]

I'm interesed in this problem!

[Soundwave]

Fady Adal said:

Similarly, if I use the num syntax ∣00⟩ is understood as just ∣0⟩.

Is it?

image.png

Give me a moment

[Soundwave]

cf.:

elab (name := qubits) "∣" n:num "⟩" : term => do
  let bits := (n.raw.getArg 0).getAtomVal.data.map λc ↦
    match c with
    | '0' => false
    | '1' => true
    | _ => false -- You can handle this better but you get the idea
  Lean.Elab.Term.elabTerm (Lean.Quote.quote (k := `term) bits) none

def test := ∣00⟩

#eval test

[Soundwave]

The lesson is perhaps that TSyntax needs lots of love to be immensely useful.

[Fady Adal]

You're correct. I don't remember what I was doing wrong but I ended up figuring it out and forgot to update this thread. My solution for reference (which I think might be overcomplicating it):

syntax (name := kets) "∣" num "⟩" : term
@[macro kets] def ketsImpl : Macro
  | `(∣ $n ⟩ ) => do
    let digits := (n.raw.isLit? `num).get!.toList
    let qubits ← (digits.mapM fun d => do
        match d with
        | '0' => ``(ket0)
        | '1' => ``(ket1)
        | _   =>
          Macro.throwError s!"invalid qubit state: expected 0 or 1, got {d}")
    mkKronChain qubits
  | _ => Macro.throwUnsupported

[Soundwave]

Nope, looks good. I'm not super familiar with all the Syntax helpers myself. Don't need to check for being a num lit though, as it's the only thing you'll get from the num parser.

[Kyle Miller]

It's possible for it to not be a num lit. For example, in ∣⟩ the num will be Syntax.missing. It's best to throwUnsupportedSyntax if it's not actually a number literal.

There are also number literals that aren't decimal sequences, like for example you might come across ∣0x22⟩.

[Soundwave]

Curious. I didn't realize the parser could throw an error but elaboration could succeed... Good to know.

elab (name := qubits) "∣" n:num "⟩" : term => do
  let `($bits) := n
  dbg_trace "{bits}"
  if bits.raw matches Lean.Syntax.missing then
    Lean.Elab.Term.elabTerm (Lean.Quote.quote (k := `term) 2) none
  else
    let bits := (n.raw.getArg 0).getAtomVal.data.map λc ↦
      match c with
      | '0' => false
      | '1' => true
      | _ => false
    Lean.Elab.Term.elabTerm (Lean.Quote.quote (k := `term) bits) none

def test := ∣⟩ -- Error here...

#eval test -- ...but term is still elaborated!

[Soundwave]

Introduces another caveat to relying on TSyntax: missing will appear as a correctly typed default value.