attempting duplicate parse fix

[jyoo980]

Changes from discussion https://github.com/jyoo980/silver/issues/12#issuecomment-748361453

[jyoo980]

After these changes, it's now resolving to a different error, where

Silicon 1.1-SNAPSHOT (f52b14f8+)
java.util.NoSuchElementException: None.get
Verification aborted exceptionally: java.util.NoSuchElementException: None.get

occurs when trying to verify

field elem: Int

inline predicate node(this: Ref)
{
    acc(this.elem)
}

[jyoo980]

I suspect it might be coming from here: https://github.com/jyoo980/silver/blob/master/src/main/scala/viper/silver/plugin/standard/inline/InlineRewrite.scala#L46

[jyoo980]

Wait, I'm dumb, that's not possible. That's only called in beforeVerify and we're not even getting to that stage yet

[ionathanch]

I think it's from type checking? Since that returns None atm

[alison-li]

The dreaded get that you taught me to avoid using :o

[jyoo980]

I hope it's typechecking.... and not something further downstream

[ionathanch]

Nope, typecheck in the termination plugin also returns None, must be something else

[ionathanch]

With my expert programming skills (Console.println) I have determined that the faulty get occurs somewhere during identifier resolution

[ionathanch]

Got it, you need this:

override def getSubnodes(): Seq[PNode] = Seq(idndef) ++ formalArgs ++ maybeBody

For PInlinePredicate, following what they do here: https://github.com/jyoo980/silver/blob/fix-parse-error/src/main/scala/viper/silver/parser/ParseAst.scala#L1208

[ionathanch]

There's a new error, but it looks like you just need to ~implement translateMemberSignature (...somehow, whatever that does)~ According to ParserPluginTemplate I guess you just need to call the super method super.translateMemberSignature(t)

[jyoo980]

That didn't seem to fix it, but I also caught another change in translateMember where we deviated from any of the others

[ionathanch]

Oh whoops calling the super is exactly the behaviour it used to have lmao. You do have to implement it, good luck

[jyoo980]

I actually think it might be something to do with typechecking. The error message says it's expecting a predicate, but our thing is an inline predicate right? Unless at the point where the error message occurs, it's already been converted

[ionathanch]

This is the error I'm getting:

Exception in thread "main" scala.NotImplementedError: an implementation is missing
    at scala.Predef$.$qmark$qmark$qmark(Predef.scala:288)
    at viper.silver.parser.PExtender.translateMemberSignature(ParseAst.scala:1101)
    at viper.silver.parser.PExtender.translateMemberSignature$(ParseAst.scala:1101)
    at viper.silver.plugin.standard.inline.PInlinePredicate.translateMemberSignature(InlinePredicatePASTExtension.scala:22)
    at viper.silver.parser.Translator.translateMemberSignature(Translator.scala:150)
        ...

Is yours something different?