Updating parser from nightly-2022-03-11

Stream: lean4

[Josh Clune]

Hello,

I'm currently in the process of trying to update a parser in Lean4 from nightly-2022-03-11 to the current nightly (nightly-2022-08-22). I know that there have been quite a few changes in the past several months, but I'm struggling to identify what exactly needs to be done to get the parser working as it used to.

Here's a minimal(ish) example that does work how I intend it to in nightly-2022-03-11:

import Lean

open Lean
open Lean.Parser

declare_syntax_cat TPTP_file

declare_syntax_cat tff_type
declare_syntax_cat tff_atomic_type

syntax defined_type := "$" noWs ident
syntax defined_type : tff_atomic_type
syntax tff_atomic_type : tff_type

syntax tff_annotation := "," rawIdent

declare_syntax_cat TPTP_input
syntax "tff" "(" rawIdent "," &"type" "," rawIdent ":" tff_type tff_annotation ? ")" "." : TPTP_input

syntax TPTP_input* : TPTP_file

macro "BEGIN_TPTP" name:ident s:TPTP_file "END_TPTP" proof:term : command => do
  let (hyps : Array Syntax) ← s[0].getArgs.mapM fun input => do
    match input with
    | `(TPTP_input| tff($n:ident,type,$name:ident : $ty:tff_type $annotation:tff_annotation ?).) =>
      match ty with
      | `(tff_type| $ty:tff_atomic_type) => Macro.throwError s!"Successfully recognized {ty} as a tff_atomic_type"
      | `(tff_type| $ty) => Macro.throwError s!"Failed to recognize {ty} as a tff_atomic_type"
    | _ => Macro.throwError "Unreached code"
  Macro.throwError "Unreached code"

BEGIN_TPTP mytest -- Output: Successfully recognized (tff_atomic_type_ (defined_type "$" `tType)) as a tff_atomic_type
  tff(box_type, type, box: $tType).
END_TPTP
  by sorry

This code will successfully recognize $tType as what I call a tff_atomic_type. If I try to run the same code in the current nightly, the macro will fail to typecheck due to changes that have been made to the Syntax/TSyntax types. If I use TSyntax.Compat to resolve those type checking errors, then my macro will no longer recognize $tType as a tff_atomic_type. Here's the code (only two lines have been added: opening TSyntax.Compat and casting s to Syntax):

import Lean

open Lean
open Lean.Parser
open TSyntax.Compat

declare_syntax_cat TPTP_file

declare_syntax_cat tff_type
declare_syntax_cat tff_atomic_type

syntax defined_type := "$" noWs ident
syntax defined_type : tff_atomic_type
syntax tff_atomic_type : tff_type

syntax tff_annotation := "," rawIdent

declare_syntax_cat TPTP_input
syntax "tff" "(" rawIdent "," &"type" "," rawIdent ":" tff_type tff_annotation ? ")" "." : TPTP_input

syntax TPTP_input* : TPTP_file

macro "BEGIN_TPTP" name:ident s:TPTP_file "END_TPTP" proof:term : command => do
  let s : Syntax := s
  let (hyps : Array Syntax) ← s[0].getArgs.mapM fun input => do
    match input with
    | `(TPTP_input| tff($n:ident,type,$name:ident : $ty:tff_type $annotation:tff_annotation ?).) =>
      match ty with
      | `(tff_type| $ty:tff_atomic_type) => Macro.throwError s!"Successfully recognized {ty} as a tff_atomic_type"
      | `(tff_type| $ty) => Macro.throwError s!"Failed to recognize {ty} as a tff_atomic_type"
    | _ => Macro.throwError "Unreached code"
  Macro.throwError "Unreached code"

BEGIN_TPTP mytest -- Output: Failed to recognize (tff_type.pseudo.antiquot "$" [] `tType []) as a tff_atomic_type
  tff(box_type, type, box: $tType).
END_TPTP
  by sorry

Is the way I'm handling Syntax/TSyntax casting incorrect? Are there other things that I'm doing wrong that aren't resulting in a typechecking error but are causing the parser to not work as intended? More generally, is there any resource/document I could look at describing the parser changes that have been made since nightly-2022-03-11? Thanks!

[Sebastian Ullrich]

There are two relevant changes here: for TSyntax, it is sufficient to replace s[0] with s.raw[0]. The more fundamental change is that antiquotations are now allowed everywhere, which collides with your defined_type syntax.

[Sebastian Ullrich]

I suppose one simple workaround would be to just handle Lean antiquotations as if they were defined_types

      if ty.raw.isAntiquot then
        dbg_trace ty.raw.getAntiquotTerm.getId