How to write a Parser for lean

Stream: new members

[kishou yusa]

How can I create a new Parser to parse a comment likehere: https://github.com/leanprover/lean4/blob/fe0cb97c5d4d43393728ddd885415bc5bfb4b929/src/Lean/Parser/Term.lean#L14C5-L14C17.
I tried with my code here

declare_syntax_cat comment
declare_syntax_cat project_term
set_option trace.Elab.info true

partial def getCommentUntilTheEnd : ParserFn := fun c s =>
  let input := c.input
  let pos := s.pos
  if h : input.atEnd pos then s else
  let curr := input.get pos
  if curr == '\n' then s.next' input pos h else
  getCommentUntilTheEnd c (s.next' input pos h)

def commentBody : Parser := {
  fn := getCommentUntilTheEnd
  info := epsilonInfo
}


elab "begin_test" s:project_term* "end_test": command => pure ()
syntax comment_wrap := "/*" rawIdent "*/"
syntax comment_line := "//" commentBody
syntax comment_wrap : comment
syntax comment_line : comment
syntax comment : project_term


syntax basic_type := "int*" <|> "uint*" <|> "address" <|> "bool" <|> "string" <|> "bytes" <|> rawIdent "." rawIdent

begin_test
  /* hello */
  /* hello1 */
  // fsadfsdaf

end_test

but for the line syntax comment_line : comment it give error that don't know how to generate formatter for non-definition '{ info := epsilonInfo, fn := getCommentUntilTheEnd }'

[Alex J. Best]

I get loads of errors if I try and run your code in the web editor. Can you make a #mwe that works there with only one error (the one you want help with) to make it easier for others to answer your question

[kishou yusa]

Here is mwe

import Lean
import Lean.Parser.Term
import Lean.Parser.Attr
import Lean.Parser.Level

open Lean
open Lean.Parser
open Lean.Parser.Term

declare_syntax_cat comment
declare_syntax_cat project_term

set_option trace.Elab.info true


partial def getCommentUntilTheEnd : ParserFn := fun c s =>
  let input := c.input
  let pos := s.pos
  if h : input.atEnd pos then s else
  let curr := input.get pos
  if curr == '\n' then s.next' input pos h else
  getCommentUntilTheEnd c (s.next' input pos h)

def commentBody : Parser := {
  fn := getCommentUntilTheEnd
  info := epsilonInfo
}


elab "begin_test" s:project_term* "end_test": command => pure ()
syntax comment_wrap := "/*" rawIdent "*/"
syntax comment_line := "//" commentBody
syntax comment_wrap : comment
syntax comment_line : comment
syntax comment : project_term


syntax basic_type := "int*" <|> "uint*" <|> "address" <|> "bool" <|> "string" <|> "bytes" <|> rawIdent "." rawIdent

[kishou yusa]

ok I manage to solve the problem by adding formatter and parenthesizer, here is the final code:

partial def getCommentUntilTheEnd : ParserFn := fun c s =>
  let input := c.input
  let pos := s.pos
  if h : input.atEnd pos then s else
  let curr := input.get pos
  if curr == '\n' then s.next' input pos h else
  getCommentUntilTheEnd c (s.next' input pos h)

def commentBody : Parser := {
  fn    := getCommentUntilTheEnd
  info  := mkAtomicInfo "comment"
}

@[combinator_parenthesizer commentBody]
def commentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
@[combinator_formatter commentBody]
def commentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous

elab "begin_test" s:project_term* "end_test": command => pure ()
syntax comment_wrap := "/*" rawIdent "*/"
syntax comment_line := "//" commentBody
syntax comment_wrap : comment
syntax comment_line : comment
syntax comment : project_term

syntax basic_type := "int*" <|> "uint*" <|> "address" <|> "bool" <|> "string" <|> "bytes" <|> rawIdent "." rawIdent

but I don't understand why do I need to add those, I just take it from the commentBody of lean4