Java AST in Lean4

Stream: lean4

[ohhaimark]

What's the laziest way I can get a Java AST in Lean4?

[Mario Carneiro]

Have a java parser and print out the ast in s expressions or json or something

[Mario Carneiro]

Or write a java parser yourself in lean 4

[Andrew Kent]

I'm not sure what the laziest way is per se, but if you are wanting to define some types to represent the AST, the Java Language Specification isn't the worst document to work from at least.

If you're wanting a parser... these ANTLR Java grammars might be a helpful starting point. I don't recall if in Java you have to interleave parsing with type checking and other analyses (like you do for C or C++)... hopefully not... since that is an absolute nightmare to get right.

[ohhaimark]

I'm trying out the lean4 syntax stuff, but I'm not sure how to solve something:

I have the following setup:

syntax "java" "{" java_file "}" : term
syntax (pkg_decl)? import_decl* ty_decl* : java_file
syntax ident ("." ident)* : q_name
syntax "package" q_name ";" : pkg_decl
syntax "import" (ident ".")+ ("*" <|> ident) ";" : import_decl
syntax "public" <|> "protected" <|> "private" <|> "abstract" <|> "static" <|> "final" : modifier
syntax modifier* "class" ident noWs (ty_params)? (ty_super)? class_body : ty_decl
syntax "<" (ident (ty_super)?),* ">" : ty_params
syntax "<" (ty_ref),* ">" : ty_args
syntax ("extends" ty_ref)? ("implements" ty_ref,*)? : ty_super
syntax q_name (ty_args)? : ty_ref
syntax "{" class_body_decl* "}" : class_body
syntax modifier* (field_decl <|> ctor_or_method_decl) : class_body_decl
syntax ty ident ("=" expr)? ";" : field_decl
syntax (ty_params)? (ty_ret)? ident params (ty_throws)? : ctor_or_method_decl
syntax "void" <|> ty : ty_ret
syntax "(" param,* ")" : params
syntax ty ident : param
syntax "throws" ty_ref,+ : ty_throws

def test := java {
  package org.stnreu001.csc2002s;
  import java.util.*;

  public class HelloWorld<A> extends Comparator<A> {
    public int x = 0;
    public HelloWorld() {
    }
  }
}

But I don't know how to get the parser to distinguish between methods and fields.

[Sebastian Ullrich]

<|> does not backtrack if the LHS has consumed input, so you'll want to split

syntax modifier* (field_decl <|> ctor_or_method_decl) : class_body_decl

into two rules:

syntax modifier* field_decl : class_body_decl
syntax modifier* ctor_or_method_decl : class_body_decl

optionally factoring out the common modifier* prefix using yet another syntax category

[ohhaimark]

Is there a syntax category for number literals in lean? Where can I discover what syntax categories already exist?

[Mario Carneiro]

num

[Mario Carneiro]

It's not actually a syntax category, it's a parser (alias)

[Mario Carneiro]

They are sort of scattered all over, but that one is declared in a block with several others at the top of Lean/Parser.lean

[ohhaimark]

How do parsers deal with the parsing of Function<A,Function<B,C>> so you don't have to do c++ style `Function<A,Function<B,C> >?

[Mario Carneiro]

You put a hack in so that >> counts as two > when needed

[Mario Carneiro]

and I guess, >>> counts as three > (since java has >>> too IIRC)

[Mario Carneiro]

For a lean 4 parser, I would suggest replacing ">" in the ty_args and ty_params rules with a custom parser that consumes a > character and doesn't use tokens

[Mac]

Mario Carneiro said:

For a lean 4 parser, I would suggest replacing ">" in the ty_args and ty_params rules with a custom parser that consumes a > character and doesn't use tokens

This is actually much more difficult to do than it sounds since parsers to run for syntax categories are selected based on their tokens and their is no way (that I know of to so) to say declare that a parser can eat any token that begins with a '>' . This means that if another parser that consumes the full token exists, the parser will likely choose that first. You may be able to get around this by having your parser having no declared firstToken and a very high priority.

[ohhaimark]

Yay, I caused a stack overflow. It happened when I added ty_array.

declare_syntax_cat java_file
syntax "java" "{" java_file "}" : term

declare_syntax_cat q_name
syntax ident ("." ident)* : q_name

declare_syntax_cat pkg_decl
syntax "package" q_name ";" : pkg_decl

declare_syntax_cat import_decl
syntax "import" (ident ".")+ ("*" <|> ident) ";" : import_decl

declare_syntax_cat ty_ref
declare_syntax_cat ty_args
syntax ident (ty_args)? : ty_ref
syntax "<" (ty_ref),* ">" : ty_args

declare_syntax_cat ty_prim
syntax "int" <|> "long" <|> "float" <|> "double" <|> "boolean" : ty_prim

declare_syntax_cat ty
declare_syntax_cat ty_array
syntax ty "[" "]" : ty_array

syntax ty_array : ty
syntax ty_prim : ty
syntax ty_ref : ty

declare_syntax_cat ty_ret
syntax "void" : ty_ret
syntax ty : ty_ret


syntax q_name (ty_args)? : ty_ref

declare_syntax_cat ty_super
syntax ("extends" ty_ref)? ("implements" ty_ref,*)? : ty_super

declare_syntax_cat mod_access
syntax "public" <|> "protected" <|> "private" : mod_access

declare_syntax_cat mod_class_method
syntax (mod_access)? "abstract"? "final"? : mod_class_method

declare_syntax_cat mod_static_method
syntax (mod_access)? "static" "final"? : mod_static_method

declare_syntax_cat mod_method
syntax mod_class_method : mod_method
syntax mod_static_method : mod_method

declare_syntax_cat mod_field
syntax (mod_access)? "static"? "final"? : mod_field

declare_syntax_cat mod_local_var
syntax "final"? : mod_field


declare_syntax_cat ty_params
syntax "<" (ident (ty_super)?),* ">" : ty_params

declare_syntax_cat lit
syntax num : lit

declare_syntax_cat expr
syntax lit : expr
syntax ident : expr

declare_syntax_cat var_decl
syntax ty ident ("=" expr)? ";" : var_decl

declare_syntax_cat field_decl
syntax mod_field var_decl : field_decl

declare_syntax_cat class_body_decl
syntax field_decl : class_body_decl

declare_syntax_cat class_body
syntax "{" class_body_decl* "}" : class_body

declare_syntax_cat param
syntax ty ident : param

declare_syntax_cat params
syntax "(" param,* ")" : params

declare_syntax_cat ty_throws
syntax "throws" ty_ref,+ : ty_throws

declare_syntax_cat local_var_decl
syntax mod_local_var var_decl : local_var_decl

declare_syntax_cat assign
syntax expr "=" expr ";" : assign

declare_syntax_cat stmt
declare_syntax_cat block
syntax "{" stmt* "}" : block
syntax block : stmt
syntax var_decl : stmt
syntax local_var_decl : stmt
syntax assign : stmt

declare_syntax_cat method_body
syntax ";" : method_body
syntax block : method_body

declare_syntax_cat method_decl
syntax mod_method (ty_params)? ty_ret ident params (ty_throws)? method_body : method_decl

declare_syntax_cat ctor_decl
syntax mod_class_method (ty_params)? (ty_ret)? ident params (ty_throws)? method_body : ctor_decl

declare_syntax_cat ty_decl
syntax mod_method "class" ident (ty_params)? (ty_super)? class_body : ty_decl

syntax (pkg_decl)? import_decl* ty_decl* : java_file

syntax field_decl : class_body_decl
syntax ctor_decl : class_body_decl
syntax method_decl : class_body_decl

syntax num : lit


def test := java {
  package org.stnreu001.csc2002s;
  import java.util.*;

  public class HelloWorld<A extends Object implements List<B> > extends Comparator<A>{
    public static final int x = 0;

    public static void main(String[] args) {

    }

    public void HelloWorld() throws Exception {
      int y = 3;
      y = 4;
    }
  }
}

[ohhaimark]

Ah, fixed

declare_syntax_cat ty_no_array
syntax ty_prim : ty_no_array
syntax ty_ref : ty_no_array

declare_syntax_cat ty
syntax ty_no_array ("[" "]")* : ty

[ohhaimark]

I don't have to interleave parsing and typechecking at least, but I need to be able to differentiate type names from expression names. Would it be possible to reuse Lean4's existing binders and unification to resolve names in context and propagate information when a name is used like a type?

[Mario Carneiro]

Mac said:

Mario Carneiro said:

For a lean 4 parser, I would suggest replacing ">" in the ty_args and ty_params rules with a custom parser that consumes a > character and doesn't use tokens

This is actually much more difficult to do than it sounds since parsers to run for syntax categories are selected based on their tokens and their is no way (that I know of to so) to say declare that a parser can eat any token that begins with a '>' . This means that if another parser that consumes the full token exists, the parser will likely choose that first. You may be able to get around this by having your parser having no declared firstToken and a very high priority.

You can say that your parser will eat tokens >, >>, >>>

[Mario Carneiro]

@ohhaimark Where in the grammar do you need to distinguish type names from expression names? I thought java didn't inherit this cursed feature from C++

[ohhaimark]

In distinguishing method calls from static method calls.

typenamenotfollowingjavaconventions.staticcall()
localvariableinscope.membercall()

[ohhaimark]

The java spec talks about having different levels of knowledge about a name in its grammar. AmbigiousName, TypeName, PackageOrTypeName, etc.

[Mario Carneiro]

It seems like you can still parse that without knowing which is which, just have an ambiguous production and determine the difference at typechecking time

[Sebastian Ullrich]

Mac said:

Mario Carneiro said:

For a lean 4 parser, I would suggest replacing ">" in the ty_args and ty_params rules with a custom parser that consumes a > character and doesn't use tokens

This is actually much more difficult to do than it sounds since parsers to run for syntax categories are selected based on their tokens and their is no way (that I know of to so) to say declare that a parser can eat any token that begins with a '>' .

I don't see the issue, there are no category parsers starting with > here

[Sebastian Ullrich]

@ohhaimark Btw, instead of a single-parser syntax category, you can also use

syntax ty := ty_no_array ("[" "]")*

[ohhaimark]

Yay

syntax q_name := ident ("." ident)*

syntax pkg_decl := "package" q_name ";"

syntax import_decl := "import" (ident ".")+ ("*" <|> ident) ";"

declare_syntax_cat ty_ref
declare_syntax_cat ty_args
syntax ident (ty_args)? : ty_ref
syntax "<" (ty_ref),* ">" : ty_args

syntax ty_prim := "int" <|> "long" <|> "float" <|> "double" <|> "boolean"

declare_syntax_cat ty_no_array
syntax ty_prim : ty_no_array
syntax ty_ref : ty_no_array

syntax ty := ty_no_array ("[" "]")*

declare_syntax_cat ty_ret
syntax "void" : ty_ret
syntax ty : ty_ret

syntax q_name (ty_args)? : ty_ref

syntax ty_super := ("extends" ty_ref)? ("implements" ty_ref,*)?

syntax mod_access := "public" <|> "protected" <|> "private"

syntax mod_class_method := (mod_access)? "abstract"? "final"?

syntax mod_static_method := (mod_access)? "static" "final"?

declare_syntax_cat mod_method
syntax mod_class_method : mod_method
syntax mod_static_method : mod_method

syntax mod_field := (mod_access)? "static"? "final"?

syntax mod_local_var := "final"?

syntax ty_params := "<" (ident (ty_super)?),* ">"

declare_syntax_cat lit
syntax num : lit

syntax param := ty ident
syntax params := "(" param,* ")"

declare_syntax_cat expr

syntax args := "(" expr,* ")"

syntax ident_or_invoke := (ty_args)? ident (args)?
syntax dot := ident_or_invoke ("." ident_or_invoke)*

syntax lit : expr
syntax dot : expr

syntax var_decl := ty ident ("=" expr)? ";"

syntax field_decl := mod_field var_decl

declare_syntax_cat class_body_decl
syntax field_decl : class_body_decl

declare_syntax_cat ty_throws
syntax "throws" ty_ref,+ : ty_throws

declare_syntax_cat method_body

declare_syntax_cat ctor_decl
syntax ctor_decl : class_body_decl
syntax mod_class_method (ty_params)? ident params (ty_throws)? method_body : ctor_decl

declare_syntax_cat method_decl
syntax method_decl : class_body_decl
syntax mod_method (ty_params)? ty_ret ident params (ty_throws)? method_body : method_decl

syntax class_body := "{" class_body_decl* "}"

syntax local_var_decl := mod_local_var var_decl

syntax assign := expr "=" expr ";"

declare_syntax_cat stmt
syntax block := "{" stmt* "}"
syntax block : stmt
syntax var_decl : stmt
syntax local_var_decl : stmt
syntax assign : stmt

syntax ";" : method_body
syntax block : method_body

syntax ty_decl := mod_method "class" ident (ty_params)? (ty_super)? class_body

syntax num : lit

syntax java_compilation_unit := (pkg_decl)? import_decl* ty_decl*

syntax "java" "{" java_compilation_unit "}" : term

I should probably start putting this in a Gist or something.

[ohhaimark]

def test := java {
  package org.stnreu001.csc2002s;
  import java.util.*;

  public class Test <A extends Object implements List<B> > extends Comparator<A>{
    public static final int x = 0;

    public static void main(String[] args) {
      List<Map<String,Double> > listOfMaps;
    }

    public void HelloWorld() throws Exception {
      final int y = 3;
      y = 4;
      y.x = f(y.z);
    }
  }
}

[ohhaimark]

Can precedence help a production rule that's left recursive? e.g.

...
syntax ident_or_invoke := (ty_args)? ident (args)?
declare_syntax_cat expr
syntax dot := expr "." ident_or_invoke
syntax dot : expr
syntax ident_or_invoke : expr

[Sebastian Ullrich]

No. A syntax rule must be syntactically left-recursive to be handled correctly.

syntax expr "." ident_or_invoke : expr

[ohhaimark]

Can macro_rules for translating to AST give you pretty printing?

[Sebastian Ullrich]

Not directly, if I understood your question correctly, but the parser itself can contain hints for Lean's built-in pretty printer https://github.com/leanprover/lean4/blob/aba0a479ec221ad2e31de09c6e71ce82a705ec38/src/Lean/Parser/Extra.lean#L63-L78
https://github.com/leanprover/lean4/blob/aba0a479ec221ad2e31de09c6e71ce82a705ec38/src/Init/Notation.lean#L143

[ohhaimark]

Whats happening here

syntax "lolol" : term

inductive testlol := | lol

macro_rules
  | `(lolol) => ``(testlol.lol)


def yee : testlol := lolol

#eval yee

failed to synthesize
  Lean.MetaEval testlol

[ohhaimark]

Oh lol, has nothing to do with the macro stuff.

[ohhaimark]

inductive testlol := | lol

#eval (testlol.lol)

[ohhaimark]

Also with https://github.com/leanprover/lean4/blob/aba0a479ec221ad2e31de09c6e71ce82a705ec38/src/Init/Notation.lean#L410-L414, I see that the trivial tactic can macro expand into various other tactics. Does that mean the macro expander is backtracking?

[Mario Carneiro]

Sebastian Ullrich said:

ohhaimark Btw, instead of a single-parser syntax category, you can also use

syntax ty := ty_no_array ("[" "]")*

I thought you said that ("a" "b")* was bad practice?

[ohhaimark]

@Mario Carneiro Why is there no MetaEval instance for the inductive definitions I make?

[Mario Carneiro]

because one hasn't been defined

[Mario Carneiro]

What is it you want to get out of evaluating the expression?

[Mario Carneiro]

If you want to print it then use deriving Repr and then #eval repr testlol.lol

[ohhaimark]

Is there a deriving mechanism for it?
I expect inductive definitions to evaluate to themselves.
Oh, so it's also the printed output?
Can you select arbitrary reductions to be used?

[Mario Carneiro]

You can evaluate expressions of type testlol, but let _ := testlol.lol; () isn't very useful, you presumably want to print it at the end or something

[ohhaimark]

So it's just defining how to pretty print?

[Mario Carneiro]

and for that you need deriving Repr or ToString (I forget if that has a deriving instance)

[Mario Carneiro]

yes

[Mario Carneiro]

You can define a printer yourself too

[Mario Carneiro]

Or just use the inductive as an intermediate type and construct some base type at the end like strings or tuples or something

[ohhaimark]

Can you have deriving for mutual inductive types?

[ohhaimark]

Nvm, I just didn't put enough deriving Reprs.

[ohhaimark]

How would I write a syntax extension that takes

def Flags := List Flag
   deriving Repr Flags

and produces something like

def Flags := List Flag
instance : Repr Flags := inferInstanceAs (Repr (List Flag))

or find something which doesn't require something like this in the first place.

[Mario Carneiro]

cc: @Sebastian Ullrich , can we get this in lean core? Mathlib wants this too

[Mac]

@Mario Carneiro Isn't tis the same problem as discussed in the previous inferInstance Zulip thread where @Sebastian Ullrich said that "Ah, well, the current API doesn't quite allow for that yet".

[Mario Carneiro]

yes, this is a syntax extension

[Mario Carneiro]

The API issue might have to do with needing to use terms instead of class names

[Mario Carneiro]

but for this basic example it could just be

def Flags := List Flag
   deriving Repr

[Leonardo de Moura]

@Mario Carneiro I added basic support for deriving at def. We can now write

def Boo := List (String × String)
  deriving BEq, Repr, DecidableEq

def M := ReaderT String (StateT Nat IO)
  deriving Monad, MonadState, MonadReader

It is very simple for now. It only supports

• Type "aliases".
• Classes with a prefix of outParams followed by one parameter.

[Mario Carneiro]

@Leonardo de Moura Thanks!

[Alcides Fonseca]

A completely different take is to use an existing Java parser (https://javaparser.org or https://spoon.gforge.inria.fr) and create a tool that translates the parsed instances of the Java AST to a similar Java AST in Lean.