noWs

Stream: metaprogramming / tactics

[Arthur Paulino]

Hi, I'm trying to write an elaborator for syntax like 0u1 and 1u1

My current code is as simple as this:

import Lean

open Lean Elab Meta

declare_syntax_cat primitive
syntax num noWs "u1" : primitive

def elabPrimitive : TSyntax `primitive → TermElabM Expr
  | `(primitive| $n:num u1) => sorry -- expected no space before
  | _ => throwUnsupportedSyntax

But if I delete the whitespace, it complains differently (but expectedly)

  | `(primitive| $n:numu1) => sorry -- unexpected token '$'; expected 'num', 'primitive' or numeral

Is there a workaround for this?

[Arthur Paulino]

Alternatively I'm using a dash:

...
syntax num noWs "-u1" : primitive

def elabPrimitive : TSyntax `primitive → TermElabM Expr
  | `(primitive| $n:num-u1) => sorry
...

But this is not ideal

[Edward van de Meent]

the best workaround might be to match witout a quotation... i.e. match on Syntax.node ...

[Edward van de Meent]

i.e. with something like   | ⟨.node info ``u1_primitive ts⟩ => sorry

[Eric Wieser]

This works:

import Lean

open Lean Elab Meta Parser Term

declare_syntax_cat primitive
@[primitive_parser]
def u1Parser := leading_parser num >> withAntiquot (mkAntiquot "noWs" `noWs) checkNoWsBefore >> "u1"

def elabPrimitive : TSyntax `primitive → TermElabM Expr
  | `(primitive| $n:num$t:noWs u1) => sorry -- expected no space before
  | _ => throwUnsupportedSyntax

#check `(primitive|1u1)
#check `(primitive|1 u1)

[Eric Wieser]

Should checkNoWsBefore include this mkAntiquot component in core?

[Arthur Paulino]

Edward van de Meent said:

i.e. with something like   | ⟨.node info ``u1_primitive ts⟩ => sorry

For the record, the anonymous constructor for TSyntax is not accepted here. I think it's missing the match-pattern tag or something

[Edward van de Meent]

that's odd... the following works on live:

import Lean

open Lean Elab Meta

declare_syntax_cat primitive
syntax num noWs "u1" : primitive

def elabPrimitive : TSyntax `primitive → TermElabM Expr
  | ⟨.node info ``primitive__U1 ts⟩ => sorry
  | _ => throwUnsupportedSyntax

[Arthur Paulino]

Ah, thanks. ``primitive__U1 fixed it

[Edward van de Meent]

yea, key is figuring out what the parser for your syntax is called

[Edward van de Meent]

apparently it's [category]_[CapitalizedSyntaxParts]_*

[Edward van de Meent]

or something along those lines

[Arthur Paulino]

I'm trying Edward's solution now because Eric's fails when trying

elab "⟪" p:primitive "⟫" : term => elabPrimitive p

#reduce ⟪1u1⟫
-- unexpected syntax
--   ⟪1u1⟫

But I'm struggling to get the Nat from info and ts like I would do with n.getNat

[Eric Wieser]

Cast the Syntax back into a TSyntax

[Arthur Paulino]

I have

  | ⟨.node info ``primitive__U1 ts⟩ =>
    let x : NumLit := ⟨Syntax.node info `num ts⟩
    dbg_trace x
    dbg_trace x.getNat
    mkAppM ``Primitive.u1 #[ToExpr.toExpr $ x.getNat % 2 == 0]

But

#reduce ⟪3u1⟫
-- (num (num "3") "u1")
-- 0

-- Primitive.u1 true

getNat should return 3 and the elaborated Primitive should be Primitive.u1 false

[Arthur Paulino]

Apparently it works with let x := mkNode numLitKind #[ts[0]![0]!], but idk what I'm doing at this point

[Eric Wieser]

I think you want let x : NumLit := ⟨ts[0]!⟩

[Arthur Paulino]

That works. Thanks again!

[Kyle Miller]

Edward van de Meent said:

yea, key is figuring out what the parser for your syntax is called

Better, name the syntax:

syntax (name := mySyntax) ...

[Arthur Paulino]

Thanks a lot everyone. This is the resulting code:

declare_syntax_cat primitive
syntax (name := primitiveU1) num noWs "u1" : primitive
syntax (name := primitiveU8) num noWs "u8" : primitive
syntax (name := primitiveU16) num noWs "u16" : primitive
syntax (name := primitiveU32) num noWs "u32" : primitive
syntax (name := primitiveU64) num noWs "u64" : primitive

def elabPrimitive : TSyntax `primitive → TermElabM Expr
  | ⟨.node _ ``primitiveU1 ts⟩ => mkPrimitive ts (· % 2 == 0) ``Primitive.u1
  | ⟨.node _ ``primitiveU8 ts⟩ => mkPrimitive ts UInt8.ofNat ``Primitive.u8
  | ⟨.node _ ``primitiveU16 ts⟩ => mkPrimitive ts UInt16.ofNat ``Primitive.u16
  | ⟨.node _ ``primitiveU32 ts⟩ => mkPrimitive ts UInt32.ofNat ``Primitive.u32
  | ⟨.node _ ``primitiveU64 ts⟩ => mkPrimitive ts UInt64.ofNat ``Primitive.u64
  | _ => throwUnsupportedSyntax
where mkPrimitive {α} [ToExpr α] ts (f : Nat → α) ctorName :=
  let n : NumLit := ⟨ts[0]!⟩
  mkAppM ctorName #[ToExpr.toExpr $ f n.getNat]