search

dominique-unruh / scala-isabelle

A Scala library for controlling/interacting with Isabelle
https://dominique-unruh.github.io/scala-isabelle
MIT License
37 stars 7 forks source link

Call sledgehammer on open goal of existing theory in Java #13

Closed BookWood7th closed 7 months ago

BookWood7th commented 7 months ago

I'd like to use scala-isabelle to call sledgehammer/try on an open proof of an existing theory. To this end I've been trying to workout how the sledgehammer experiment in this repo could be transferred from Scala to Java. But I've found a few oddities like BooleanConverter, StringConverter, etc... not extending the Converter Class for their respective types.

Is there a way to call sledgehammer from Java?

dominique-unruh commented 7 months ago

There are some oddities where the type system of Scala and Java do not match.

First, note that it is easiest to access the converters via de.unruh.isabelle.mlvalue.Implicits.booleanConverter. Then you do not need to guess weird names like BooleanConverter$.

booleanConverter is a Converter<scala.Boolean>, except that scala.Boolean does not exist in Java. So Scala represents it as as Converter<Object> (which is not correct, of course).

(Note: With stringConverter, this problem should not occur since a Scala string is a Java string.See javap de.unruh.isabelle.mlvalue.StringConverter$.)

Possibly your problem is resolved by simply having some converters-aliases whose types are Java-compatible. I added javaBooleanConverter, javaIntConverter, etc. for the ones that do not match. (Pushed to the repository, but not yet in the binary snapshot because the CI is still running.)

If that (and maybe some type-casts) doesn't help, can you please post the code that fails to compile? (Translating the sledgehammer code to Java myself is beyond what I can do, unfortunately.)

BookWood7th commented 7 months ago

Thank you, these classes will be helpful.

I had missed the second Implicits class in my program. I'd only used the one in the pure package. Replacing all Boolean occurences with Object and then casting solved the issues I've been facing.