How to implement completion?

[ice1000]

trafficstars

As title. I'm quite unsure how to do this..

[imkiva]

We may need to implement aya-prover/aya-prover-proto#508 first because we should be able to provide completions on incomplete programs IMO

[imkiva]

But the biggest problem is that our parser currently cannot recover from parse errors like

def test => zero
def a =>  

So when vscode is trying to request completions in a, we can do nothing because parser produces no results :(

[ice1000]

@imkiva We can just define the syntax better to make these code parse

[ice1000]

@imkiva For example, we can make a "definition without body" a type error instead of a parse error

[re-xyr]

@imkiva For example, we can make a "definition without body" a type error instead of a parse error

This sounds very unlike a type error

[ice1000]

@imkiva For example, we can make a "definition without body" a type error instead of a parse error

This sounds very unlike a type error

It can be thrown as a type error and the users would see a syntax error

[re-xyr]

Btw how does Arend solve this?

[ice1000]

Btw how does Arend solve this?

Their JB plugin uses a different parser which is fault-tolerant (JB has a general framework for code completion).

[re-xyr]

Can we have some fault-tolerant parser?

[imkiva]

@ice1000 But this does not cover all cases and we need to change every pass in the compiler every time the syntax compromises.

[imkiva]

It seems ANTLR4 can recover: https://www.antlr.org/api/Java/org/antlr/v4/runtime/ANTLRErrorStrategy.html

[ice1000]

Can we have some fault-tolerant parser?

Idk if you could reuse GK

[ice1000]

It seems ANTLR4 can recover: https://www.antlr.org/api/Java/org/antlr/v4/runtime/ANTLRErrorStrategy.html

Is that easy to adapt in Aya?

[imkiva]

It seems ANTLR4 can recover: https://www.antlr.org/api/Java/org/antlr/v4/runtime/ANTLRErrorStrategy.html

Is that easy to adapt in Aya?

It's a little difficult. ANTLR does not have detailed documents on this.

[re-xyr]

I saw about tree-sitter. Is that any helpful for our case?

[ice1000]

@re-xyr It doesn't have a good Java rewrite/binding yet. JetBrains has a JNI-based binding, but I ain't sure if it's open sourced or "good" in any sense.

[ice1000]

It seems ANTLR4 can recover: https://www.antlr.org/api/Java/org/antlr/v4/runtime/ANTLRErrorStrategy.html

Is that easy to adapt in Aya?

It's a little difficult. ANTLR does not have detailed documents on this.

org.antlr.v4.runtime.Parser#setErrorHandler(ANTLRErrorStrategy handler)

[ice1000]

Quite easy.

[imkiva]

Quite easy.

I mean these magic functions not the API

[ice1000]

Maybe we can just look at the default implementation

[ice1000]

This is what I see. They're heavily documented

[re-xyr]

I don’t know much about incremental compiling. If we are to offer ide support, are we going to do that anyway? Is ANTLR a capable parser of that? How would we adapt our typechecking process for that?

[ice1000]

@re-xyr I have no idea. Probably we should only implement file-level incremental compilation as Agda to avoid the complications

[ice1000]

/cc @ShreckYe

[imkiva]

Our parsers are decoupled from base module now. Should we introduce a tree-sitter for LSP only?

[ice1000]

The problem is that there isn't a reliable tree-sitter implementation for JVM. IIRC fleet uses their own binding, which I consider reliable, but it's not open sourced