Replicate builtin do syntax

Stream: new members

[Alex M]

Hi all. Trying to understand how to create intrusive DSL with Lean4. Want to create syntax that replicate 'do' builtin syntax into more lightweight 'mm'. My try was:

prelude
import Lean.Parser.Term

namespace Lean
namespace Parser

namespace Category
def mmElem : Category := {}
end Category

builtin_initialize registerBuiltinParserAttribute `builtin_mmElem_parser ``Category.mmElem
builtin_initialize registerBuiltinDynamicParserAttribute `mmElem_parser `mmElem

@[inline] def mmElemParser (rbp : Nat := 0) : Parser :=
  categoryParser `mmElem rbp

namespace Term

def mmSeqItem := leading_parser
  ppLine >> mmElemParser >> optional "; "
def mmSeqIndent := leading_parser
  many1Indent mmSeqItem
def mmSeqBracketed := leading_parser
  "{" >> withoutPosition (many1 mmSeqItem) >> ppLine >> "}"
@[builtin_doc] def mmSeq :=
  withAntiquot (mkAntiquot "mmSeq" decl_name% (isPseudoKind := true)) <|
    mmSeqBracketed <|> mmSeqIndent

attribute [run_builtin_parser_attribute_hooks] mmSeq
builtin_initialize register_parser_alias mmSeq

@[builtin_mmElem_parser] def mmReturn := leading_parser:leadPrec
  withPosition ("return" >> optional (ppSpace >> checkLineEq >> termParser))

@[builtin_term_parser] def «mm»  := leading_parser:argPrec
  ppAllowUngrouped >> "mm " >> mmSeq

@[builtin_term_parser] def termReturn := leading_parser:leadPrec
  withPosition ("return" >> optional (ppSpace >> checkLineEq >> termParser))

end Term
end Parser
end Lean

But that not worked with error "unknown attribute [builtin_mmElem_parser]" on latest Lean 4.13.0. Is that doable? Appreciate some guidance from knowledgeables here.

[Daniel Weber]

Have you read Metaprogramming in Lean? In particular https://leanprover-community.github.io/lean4-metaprogramming-book/main/08_dsls.html should be helpful. I don't think you're supposed to use the @[builtin_... attributes, those are for builtin parts of Lean itself

[Alex M]

Thank you for reply.

Ok, may be @[builtin.. attributes not for users, but if i get rid of failing attribute mm not considered anyway by Lean. That not worked:

prelude
import Lean.Parser.Term

namespace Lean
namespace Parser

namespace Category
def mmElem : Category := {}
end Category

builtin_initialize registerBuiltinParserAttribute `builtin_mmElem_parser ``Category.mmElem
builtin_initialize registerBuiltinDynamicParserAttribute `mmElem_parser `mmElem

@[inline] def mmElemParser (rbp : Nat := 0) : Parser :=
  categoryParser `mmElem rbp

namespace Term

def mmSeqItem := leading_parser
  ppLine >> mmElemParser >> optional "; "
def mmSeqIndent := leading_parser
  many1Indent mmSeqItem
def mmSeqBracketed := leading_parser
  "{" >> withoutPosition (many1 mmSeqItem) >> ppLine >> "}"
@[builtin_doc] def mmSeq :=
  withAntiquot (mkAntiquot "mmSeq" decl_name% (isPseudoKind := true)) <|
    mmSeqBracketed <|> mmSeqIndent

attribute [run_builtin_parser_attribute_hooks] mmSeq
builtin_initialize register_parser_alias mmSeq

@[builtin_term_parser] def «mm»  := leading_parser:argPrec
  ppAllowUngrouped >> "mm " >> mmSeq

end Term
end Parser
end Lean

def main : IO Unit := mm
  IO.println "Hello"

I will try Embedding DSLs By Elaboration approach, that was referenced by you, thanx.

[Daniel Weber]

You should also avoid using prelude and builtin_initialize

[Kyle Miller]

In particular, remove prelude and remove builtin_ everywhere, but there's an issue that these are low-level parsing facilities. Maybe the notation will work from within a module that imports this one.

[Kyle Miller]

In case it's helpful, a while back I made a little do-like notation of my own: https://gist.github.com/kmill/be21ca7017d4b1d2eadd47ded5168dd1

Here's a variant: https://gist.github.com/kmill/db96b331b9f86579d5dea8e17a49425f

Both of these use syntax instead of leading_parsers, which is a higher-level interface.

[Alex M]

@Kyle Miller Cool. Your code works as expected, second variant too (aside from checkMaxHeartbeats). That is exactly what example i needed. Thank you. My try apparently was in wrong direction.