Translate function bodies to Isabelle/HOL

[lukaszcz]

• Closes Extend the Juvix-to-Isabelle translation with pure functions #2813

Implements a translation from Juvix functions to Isabelle/HOL functions. This extends the previous Juvix -> Isabelle translation which could handle only type signatures.

Checklist

• Basic translation
• Polymorphism
• Arithmetic operators
• Numeric literals
• List literals
• Comparison operators
• Boolean operators
• if translated to Isabelle if
• true and false translated to Isabelle True and False
• zero and suc translated to Isabelle 0 and Suc
• Maybe translated to Isabelle option
• Pairs translated to Isabelle tuples
• Quote Isabelle identifier names (e.g. cannot begin with _)
• Rename variables to avoid clashes (in Isabelle/HOL pattern variables don't shadow function identifiers)
• Common stdlib functions (map, filter, etc) translated to corresponding Isabelle functions
• Multiple assignments in a single let
• CLI
• Test
  • The test is very fragile, similar to the markdown test. It just compares the result of translation to Isabelle against a predefined expected output file.

Limitations

The translation is not designed to be completely correct under all circumstances. There are aspects of the Juvix language that cannot be straightforwardly translated to Isabelle/HOL, and these are not planned to ever be properly handled. There are other aspects that are difficult but not impossible to translate, and these are left for future work. Occasionally, the generated code may need manual adjustments to type-check in Isabelle/HOL.

In particular:

• Higher-rank polymorphism or functions on types cannot be translated as these features are not supported by Isabelle/HOL. Juvix programs using these features will not be correctly translated (the generated output may need manual adjustment).
• In cases where Juvix termination checking diverges from Isabelle/HOL termination checking, providing a termination proof manually may be necessary. Non-terminating Juvix functions cannot be automatically translated and need to be manually modelled in Isabelle/HOL in a different way (e.g. as relations).
• Comments (including judoc) are ignored. This is left for future work.
• Traits are not translated to Isabelle/HOL type classes / locales. This is left for future work.
• Mutually recursive functions are not correctly translated. This is left for future work.
• Record creation, update, field access and pattern matching are not correctly translated. This is left for future work.
• Named patterns are not correctly translated. This is left for future work.
• Side conditions in patterns are not supported. This is left for future work.
• If a Juvix function in the translated module has the same name as some function from the Isabelle/HOL standard library, there will be a name clash in the generated code.

[jonaprieto]

As I didn't see any task in the CI that could check the test, I did it myself and can tell that the output for tests/positive/Isabelle/isabelle/Program.juvix typechecks with Isabelle2023 yey. Please add Isabelle to the CI for macOSX; you probably want to use something like this.

On the other hand, I tested this translation with some examples from the Specs we are writing. I noticed that many fragments (using literals) now have a well-formed Isabelle term that they didn't have before, that's good. However, many examples are still not supported in the translation. So, even when I'm not asking to solve them in this PR, unless you want, let me mention some issues I find crucial.

• Axioms translation is not supported. However, the following axiom with a pragma should be easily translated, knowing that Isabelle has an undefined term that takes any type. I'd expect to write something like or simply nothing.

{-# isabelle-translation:
      term: undefined #-}
axiom !undefined : {A : Type} -> A;

• Translate a definition like the following.

B (A : Type) (a : A) : Type := Pair Type A;

• One major problem with using this translation is the support for imports. I know imports are not supported in future work (recursively processing all the imports and so on). However, even without full support for imports, something basic could work now. For example, support some form, such as the basic import X.Y.Z open, so it returns something like imports "X/Y/Z". Optionally, we can have a pragma or some fragment to state which imports use in the Isabelle output.

module X;

{-# isabelle-translation: "Anoma/Types/Message" -#}
import Lib.Message open;

Or something like this, and the output

theory X
imports Main
        "Anoma/Types/Message"
begin
...

[lukaszcz]

Please add Isabelle to the CI for macOSX; you probably want to use something like this.

We don't currently run the MacOS CI, because it doesn't work with RISC0. Let's defer adding Isabelle to the Linux CI for later, because I don't know how to reliably install Isabelle as a single command on Linux.

[lukaszcz]

• Axioms translation is not supported. However, the following axiom with a pragma should be easily translated, knowing that Isabelle has an undefined term that takes any type. I'd expect to write something like or simply nothing.

{-# isabelle-translation:
      term: undefined #-}
axiom !undefined : {A : Type} -> A;

I don't understand what's the problem with axioms. Axiom translation is supported. The above axiom is translated to:

definition !undefined :: 'A where
  "!undefined = undefined"

[lukaszcz]

But "!undefined" is not a valid Isabelle identifier name. I think it needs to begin with a letter. I'll improve the quoting.

[lukaszcz]

• Translate a definition like the following.

B (A : Type) (a : A) : Type := Pair Type A;

How do you want this to be translated, in principle? There is no Type in Isabelle/HOL. There are no universes.

[lukaszcz]

But "!undefined" is not a valid Isabelle identifier name. I think it needs to begin with a letter. I'll improve the quoting.

I improved the quoting

[lukaszcz]

• One major problem with using this translation is the support for imports. I know imports are not supported in future work (recursively processing all the imports and so on). However, even without full support for imports, something basic could work now. For example, support some form, such as the basic import X.Y.Z open, so it returns something like imports "X/Y/Z".

I added basic support for imports. All imports are now translated in the way you mentioned to Isabelle/HOL imports, except imports from Stdlib.

[lukaszcz]

• Translate a definition like the following.

B (A : Type) (a : A) : Type := Pair Type A;

How do you want this to be translated, in principle? There is no Type in Isabelle/HOL. There are no universes.

Perhaps this could be simulated with locales somehow, but this needs more fundamental work.

[jonaprieto]

:) Let's merge this. And, yes, I tested the last changes you made.

As a next step, we could start working on supporting comments, mutually recursive functions and type syn. definitions that use further defined other types, such as

A (B : Type) : Type := C B -> D B;
...
type C (X : Type) :=..
type D (X : Type) := ..

And yes, record manipulation. Of course, the rest you mentioned in the PR description would be nice to have.