mirror of
https://github.com/anoma/juvix.git
synced 2024-12-03 09:41:10 +03:00
83837b9c5f
* Closes #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 --------- - [x] Basic translation - [x] Polymorphism - [x] Arithmetic operators - [x] Numeric literals - [x] List literals - [x] Comparison operators - [x] Boolean operators - [x] `if` translated to Isabelle `if` - [x] `true` and `false` translated to Isabelle `True` and `False` - [x] `zero` and `suc` translated to Isabelle `0` and `Suc` - [x] `Maybe` translated to Isabelle `option` - [x] Pairs translated to Isabelle tuples - [x] Quote Isabelle identifier names (e.g. cannot begin with `_`) - [x] Rename variables to avoid clashes (in Isabelle/HOL pattern variables don't shadow function identifiers) - [x] Common stdlib functions (`map`, `filter`, etc) translated to corresponding Isabelle functions - [x] Multiple assignments in a single `let` - [x] CLI - [x] 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. --------- Co-authored-by: Paul Cadman <git@paulcadman.dev> |
||
|---|---|---|
| .. | ||
| Anoma | ||
| Asm | ||
| BackendMarkdown | ||
| Casm | ||
| Compilation | ||
| Core | ||
| Examples | ||
| Formatter | ||
| Internal | ||
| Isabelle | ||
| Nockma | ||
| Package | ||
| Parsing | ||
| Reg | ||
| Repl | ||
| Resolver | ||
| Runtime | ||
| Rust | ||
| Scope | ||
| Termination | ||
| Tree | ||
| Typecheck | ||
| VampIR | ||
| Anoma.hs | ||
| Asm.hs | ||
| BackendMarkdown.hs | ||
| Base.hs | ||
| Casm.hs | ||
| Compilation.hs | ||
| Core.hs | ||
| Examples.hs | ||
| Format.hs | ||
| Formatter.hs | ||
| Internal.hs | ||
| Isabelle.hs | ||
| Main.hs | ||
| Nockma.hs | ||
| Package.hs | ||
| Parsing.hs | ||
| Reg.hs | ||
| Repl.hs | ||
| Resolver.hs | ||
| Runtime.hs | ||
| Rust.hs | ||
| Scope.hs | ||
| Termination.hs | ||
| Tree.hs | ||
| Typecheck.hs | ||
| VampIR.hs | ||