Parsing idents separated by coma

Stream: lean4

[Raúl Raja Martínez]

Hi, I'm trying to tell lean4 to parse parameters separated by coma to be valid syntax.
I tried different things to get this to work:

def foo (x: Nat, y:Nat) : Nat := x + y

I'd like the above notation to work and expand to

def foo (x: Nat) (y:Nat) : Nat := x + y

where each "," is expanded as ")(" but I seem unable to properly escape (, so it's not used as precedence for ops in my argument declaration.
Any help or direction on how I might accomplish this?, thanks!

[Alex Keizer]

Could you show what you've tried so far?

[Raúl Raja Martínez]

I tried variations of the following:

syntax term noWs "(" term,* ")" : term

macro_rules
  | `($f($args,*)) => `($f $args*)

syntax "func" ident noWs "(" ident,* ")" ":" ident "=" term : command

macro_rules
  | `(func $name($args,*) : $type = $body) => `(def $name $args* : $type := $body)

func fx() : Int = 1
func fy() : Int = 1
func fz() : Int = fx + fy

#eval fz() -- work, 2

func fxi(n: Int, y: Int) : Int = n + y -- fails, expected `(`
func fyi() : Int = 1 -- works
func fzi() : Int = fxi(1, 1) + fyi() -- fails fxi is not properly defined

#eval fzi()  -- 2

[Raúl Raja Martínez]

I started with a more naive approach with notation trying to make it as simple as possible:

notation "," => ")("

--fails expected ")"
def foo (n: Int, y: Int) : Int := n + y

But I realize I'm not capturing the idents and expanding them properly in the def parameter position. But it's the first that I came up with. I just started learning Lean.

Eventually, I ended up following the sources to a lower level place in the macro system where leadingParsers are used to parse and structure precedence with "(" and ")" but I'd like to avoid using that low-level infra if possible.

[Mario Carneiro]

while it is for sure possible to make this work, I would preface this by saying that you should probably just learn to love the lambda instead of reinventing binder syntax

[Mario Carneiro]

the approach that is the closest here is the one starting with func. The others hit the issue that binders aren't terms so notation and syntax ... : term aren't going to work

[Mario Carneiro]

The reason yours didn't work here is because

syntax "func" ident noWs "(" ident,* ")" ":" ident "=" term : command

says that you only accept a list of identifiers in parentheses, meaning that func bla(x,y,z): w = x + y works but not func bla(x: Int,y,z): w = x + y or func bla(x,y,z): List Nat = sorry

[Mario Carneiro]

import Lean

open Lean Parser Term
def explicitBinder' := leading_parser
  withoutPosition (many1 binderIdent >> binderType >>
    Parser.optional (binderTactic <|> binderDefault))

syntax "func" Parser.ident noWs "(" explicitBinder',* ")" ":" term:51 "=" term : command

def trExplicitBinder' (stx : TSyntax ``explicitBinder') : TSyntax ``bracketedBinder :=
  let args := #[mkAtom "("] ++ stx.raw.getArgs ++ #[mkAtom ")"]
  ⟨stx.raw.setKind ``explicitBinder |>.setArgs args⟩

macro_rules
  | `(func $name($args,*) : $type = $body) =>
    let args := args.getElems.map trExplicitBinder'
    `(def $name $args* : $type := $body)

macro f:term noWs "(" args:term,* ")" : term => `($f $args*)

func fx() : Int = 1
func fy() : Int = 1
func fz() : Int = fx + fy

#eval fz() -- 2

func fxi(n: Int, y: Int) : Int = n + y
func fyi() : Int = 1
func fzi() : Int = fxi(1, 1) + fyi()

#eval fzi()  -- 2

@Raúl Raja Martínez

[Mario Carneiro]

unfortunately translating binders is a bit annoying because of the way the parsers are defined, so I had to use the raw interface here and put the syntax together manually

[Raúl Raja Martínez]

Thanks @Mario Carneiro ! this helps a lot. I already like lean's syntax, the reasons I was doing this is because I'm porting a subset of pure kotlin to be embedded in lean and I'm attempting to map existing kotlin programs to be verified in lean similar to how we do in https://arrow-kt.io/docs/meta/analysis/ . Arrow analysis depends on a SMT solver backend to implement pre,post conditions on functions.

I'm hoping to use lean as backend for a tool that verifies certain properties of other langs such as termination and type refinements, etc. When I got started I realized lean's power to embed other syntax and thought it would be a good start.

I've also played with the idea of attempting to support the antlr g4 style syntax directly in Lean so foreign grammars in Antlr can import syntax in lean but that seems a bigger effort until I get more experience with Lean

[Mario Carneiro]

You might want to look at lean4-alloy, which contains a more or less complete C grammar encoded as a lean4 DSL. You could do something similar for kotlin