* Closes#2962
* Depends on #2963
* In Isabelle/HOL comments cannot appear in internal syntax. All
comments inside a Juvix definition are moved outside: to before the
definition or before the earliest function clause.
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
* Closes#2894
* Closes#2895
* The translation of pattern matching on records is a bit tricky because
one cannot pattern match on records in Isabelle, except in top patterns
of function clauses. We thus need to translate into nested pattern
matching and record projections. Named patterns can be translated with a
similar technique and are also handled in this PR.
Checklist
---------
- [x] record creation
- [x] record projections
- [x] record update
- [x] top-level record patterns
- [x] nested record patterns
- [x] named patterns
- [x] remove redundant pattern matching clauses
- [x] remove redundant single-branch pattern matches
The `anoma-bytearray-{to, from}-anoma-contents` are intended to be used
to convert to/from atoms representing `ByteArrays`. These builtins are
required temporarily until Anoma Node makes ByteArray representation
uniform across all of its APIs.
We represent ByteArrays in nock as a cell:
```
[size contents]
```
Where `size` is the size of the ByteArray and `contents` is an Atom
representing the bytes in LSB ordering.
The `size` is required in general because the encoding of ByteArrays to
Atoms is ambiguous. For example the ByteArrays [0x01; 0x00] and [0x01]
are represented by `1`.
Some Anoma ByteArrays like keys and signatures are represented using on
the `contents` atom because the size is constant.
Users of Anoma APIs have to strip / add size information from ByteArrays
depending on where the data is used. The new builtins provide this
facility.
These builtins are temporary because it's been agreed with Anoma
engineering team to change the Anoma APIs to make the ByteArray
representation uniform, i.e always represent ByteArrays using `[size
content]`. When this is implemented in Anoma Node we can remove these
builtins.
```
builtin anoma-bytearray-to-anoma-contents
axiom toAnomaContents : ByteArray -> Nat;
builtin anoma-bytearray-from-anoma-contents
axiom fromAnomaContents :
-- | The size of the ByteArray
Nat
-- | The contents of the ByteArray
-> Nat
-- | The resulting ByteArray
-> ByteArray;
```
This PR updates:
- [x] Package version
- [x] Smoke test
- [x] Changelog
We can't merge this until the stdlib submodule pointer is fixed-up to
point to stdlib main.
* Specialization has become less effective after recent changes to the
codebase. This PR fixes issues with specialization.
* Closes#2939
* Closes#2945
Checklist
---------
- [X] Preserve pragmas for letrec and lambda in Stored Core
- [x] Remove the assumption that all type variables are at the front
(closes#2945)
- [x] Allow specialization when the argument is a constructor
application
- [x] Make renaming adjust pragmas
- [x] Allow pragmas for fields in record definitions (closes#2939)
- [x] Update standard library pragmas
- [x] Fix JuvixTree printing
This PR adds support for ByteArray in the Anoma cryptographic functions.
```
builtin anoma-sign
axiom anomaSign : {A : Type} -> A -> ByteArray -> ByteArray;
builtin anoma-verify-with-message
axiom anomaVerifyWithMessage : {A : Type} -> ByteArray -> ByteArray -> Maybe A;
builtin anoma-sign-detached
axiom anomaSignDetached : {A : Type} -> A -> ByteArray -> ByteArray;
builtin anoma-verify-detached
axiom anomaVerifyDetached : {A : Type} -> ByteArray -> A -> ByteArray -> Bool;
```
The Anoma / Hoon Stdlib function `length` needs to be exposed as a
StdlibFunction because a ByteArray stores its length and the value
returned by `anomaSign` is not a fixed length.
This PR adds support for a builtin `ByteArray` type and associated
functions for constructing a `ByteArray` from a list of bytes and a
function to query the size of the `ByteArray`. It is only available in
the Anoma backend.
In Core / Tree, ByteArray constant is stored using a Haskell ByteString.
In Anoma the ByteArray is stored as a cell where the head is the length
of the ByteArray and the tail is an integer is an integer formed by
concatenating the bytes in the array using little-endian byte ordering.
The Nock for constructing a `ByteArray` uses the `length`, `add`,
`folder` and `lsh` functions from the Anoma hoon stdlib. See the [code
comment](fa068a30e7/src/Juvix/Compiler/Nockma/StdlibFunction.hs (L37))
for more details.
Example:
```
module test082;
import Stdlib.Prelude open;
import Stdlib.Debug.Trace open;
builtin bytearray
axiom ByteArray : Type;
builtin bytearray-from-list-byte
axiom mkByteArray : List Byte -> ByteArray;
builtin bytearray-size
axiom size : ByteArray -> Nat;
bs0 : ByteArray := mkByteArray [];
bs1 : ByteArray := mkByteArray [0x0; 0x0; 0x0];
bs2 : ByteArray := mkByteArray [0x1; 0x0; 0x0; 0x0];
bs3 : ByteArray := mkByteArray [0x2; 0x1];
bs4 : ByteArray := mkByteArray [0x100];
main : ByteArray :=
trace (size bs0)
>-> trace bs0
>-> trace (size bs1)
>-> trace bs1
>-> trace (size bs2)
>-> trace bs2
>-> trace (size bs3)
>-> trace bs3
>-> trace (size bs4)
>-> bs4;
```
Output using `tests/Anoma/Compilation/positive/test082.juvix`
```
$ juvix compile anoma -g test082.juvix
$ juvix dev nockma run test082.pretty.nockma
0
[0 0]
3
[3 0]
4
[4 1]
2
[2 258]
1
[1 0]
```
1. Refactors css theme to only use variables as source for colors to
make it easier to define themes. In order to define a theme, the
following variables need to be defined (these variables have been taken
mostly from the catppuchin theme):
```
/* Code */
--ju-inductive: var(--ctp-green);
--ju-constructor: var(--ctp-mauve);
--ju-function: var(--ctp-yellow);
--ju-module: var(--ctp-lavender);
--ju-axiom: var(--ctp-red);
--ju-string: var(--ctp-flamingo);
--ju-keyword: var(--ctp-sky);
--ju-delimiter: var(--ctp-overlay2);
--ju-var: var(--ctp-text);
--ju-fixity: var(--ctp-sapphire);
--ju-comment: var(--ctp-rosewater);
--ju-judoc: var(--ctp-teal);
--ju-number: var(--ctp-peach);
/* Text */
--ju-text: var(--ctp-text);
--ju-subtext1: var(--ctp-subtext1);
--ju-subtext0: var(--ctp-subtext0);
/* Overlay */
--ju-overlay0: var(--ctp-overlay0);
--ju-overlay1: var(--ctp-overlay1);
--ju-overlay2: var(--ctp-overlay2);
/* Surface */
--ju-surface0: var(--ctp-surface0);
--ju-surface1: var(--ctp-surface1);
--ju-surface2: var(--ctp-surface2);
/* Panes */
--ju-base: var(--ctp-base);
--ju-mantle: var(--ctp-mantle);
--ju-crust: var(--ctp-mantle);
/* Theme */
--ju-main: var(--ctp-maroon);
--ju-main-link: var(--ctp-maroon);
--ju-main-link-visited: var(--ctp-flamingo);
--ju-warning: var(--ctp-red);
```
2. When changing theme, the judoc documentation will also use that
theme, as opposed to only the source code.
3. Added highlighting for module names.
4. When hovering a juvix code element (axiom, constructor, inductive,
etc.), the underline will be of the correct color for the kind. Before
it was always a fixed color.
This PR adds `Byte` as a builtin with builtin functions for equality,
`byte-from-nat` and `byte-to-nat`. The standard library is updated to
include this definition with instances for `FromNatural`, `Show` and
`Eq` traits.
The `FromNatural` trait means that you can assign `Byte` values using
non-negative numeric literals.
You can use byte literals in jvc files by adding the u8 suffix to a
numeric value. For example, 1u8 represents a byte literal.
Arithmetic is not supported as the intention is for this type to be used
to construct ByteArrays of data where isn't not appropriate to modify
using arithmetic operations. We may add a separate `UInt8` type in the
future which supports arithmetic.
The Byte is supported in the native, rust and Anoma backend. Byte is not
supported in the Cairo backend because `byte-from-nat` cannot be
defined.
The primitive builtin ops for `Byte` are called `OpUInt8ToInt` and
`OpUInt8FromInt`, named because these ops work on integers and in future
we may reuse these for a separate unsigned 8-bit integer type that
supports arithmetic.
Part of:
* https://github.com/anoma/juvix/issues/2865
This PR adds `FromNatural` to package-base. The change is backwards
compatible for existing Juvix code so we don't need to make a new
version of package-base. The new trait is unused, it will be integrated
in subsequent PRs.
### `FromNatural` trait
The `FromNatural` trait has the following definition.
```
trait
type FromNatural A :=
mkFromNatural {
builtin from-nat
fromNat : Nat -> A
};
```
### `Natural` trait changes
The `Natural` trait is changed to remove its `fromNat` field and add a
new instance field for `FromNatural A`.
### juvix-stdlib changes
`FromNatural` instances are added for `Int` and `Field` in the standard
library.
## Rationale
The `FromNatural` trait will be used for the Bytes type.
We want the following properties for Byte:
1. Values of the Bytes type should be assignable from a non-negative
numeric literal.
2. We don't want to implement + and * for Bytes.
Currently, in order for a type to have property 1. it must have an
instance of `Natural` so property 2. can't be satisfied.
To solve this we split the `from-nat` builtin from the `Natural` trait
into a new trait `FromNatural`.
1. When the flatparse scanner fails and we fallback to megaparsec, a
warning is issued.
2. The flatparse scanner has been fixed so it is not confused when a
name starts with `import`.
This PR addresses a bug/missing case present since v0.6.2, introduced
specifically by
- PR #2779,
That PR involves detecting imports in Juvix files before type checking,
and that's the issue.
Detecting/scanning imports is done by running a flat parser (which
ignores the Juvix Markdown structure) and when it fails, it runs a
Megaparser parse. So, for simplicity,
we could just continue using the same Megaparser as before for Juvix
Markdown files.
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
- Closes#2923
This pr fixes a bug where all fields were assigned to be explicit
arguments in the NameSignature Builder. A single line change was enough
to fix it.
```diff
- RecordStatementField RecordField {..} -> addSymbol @s Explicit Nothing _fieldName _fieldType
+ RecordStatementField RecordField {..} -> addSymbol @s (fromIsImplicitField _fieldIsImplicit) Nothing _fieldName _fieldType
```
I've also added a compilation test for instance fields.
1. Adds the `--log-level LOG_LEVEL` flag to the CLI. This flag can be
given `error`, `warn`, `info`, `progress`, `debug` as argument to filter
the logged messages.
2. Removes the `--only-errors` flag.
3. Adds the `--ide-end-error-char CHAR`, which receives a character as
an argument, which is appended to the end of error messages. This is
handy to facilitate parsing of errors messages from the ide. This
functionality was previously embeded in the old `--only-errors` flag.
* 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>
Since it is common to want to assign a named argument a variable of the
same name, we add special syntax for it. E.g.
```
f (fieldA : A) (fieldB : B) : S :=
mkS@{
fieldC := fieldA; -- normal named argument
fieldA; -- pun
fieldB -- pun
};
```
- Closes#2668
This pr migrates the old named application syntax to the new one. In
order to migrate a juvix file to the new syntax it suffices to run the
formatter.
After the next release, we should completely remove the support for the
old syntax.
## Other changes
I've improved Scope negative tests. Previously, when a negative test
failed, you could only see the title of the test and the message
"Incorrect Error", as well as the Haskell file and line where the test
is defined.
This is extremely incovenient because you have to go to the haskell test
file, go to the line where the error is defined, look at the name of the
file and then visit that file. Moreover, you need to manually run the
scoper on that file to see the error that was returned.
I've fixed that and it now shows all relevant information. Example:
I've implemented this only using the `Generic` instance for the
`ScoperError` type, so doing something similar for the rest of negative
tests should be straightforward.
This pr explores the option to implement error handling in Juvix à la
mtl. It adds the following as a test:
1. `MonadError` trait.
2. `MonadTrans` trait.
3. `ExceptT` monad transformer and its `Functor`, `Monad`, `MonadTrans`,
`MonadError` instances.
- Syntax for #2804.
- ⚠️ Depends on #2869.
This pr introduces:
1. front-end support (parsing, printing, typechecking) for boolean side
conditions for branches of case expressions.
2. Now `if` is a reserved keyword.
3. Multiway `if` is allowed to have only the `else` branch. I've also
refactored the parser to be simpler.
Example:
```
multiCaseBr : Nat :=
case 1 of
| zero
| if 0 < 0 := 3
| else := 4
| suc (suc n)
| if 0 < 0 := 3
| else := n
| suc n if 0 < 0 := 3;
```
The side if branches must satisfy the following.
1. There must be at least one `if` branch.
4. The `else` branch is optional. If present, it must be the last.
Future work:
1. Translate side if conditions to Core and extend the exhaustiveness
algorithm.
5. Add side if conditions to function clauses.
* Closes#2703
* Adds [peephole
optimization](https://en.wikipedia.org/wiki/Peephole_optimization) of
Cairo assembly.
* Adds a transformation framework for the CASM IR.
* Adds `--transforms`, `--run` and `--no-print` options to the `dev casm
read` command.
* Closes#2829
* Adds a transformation which converts `br` to `if` when the variable
branched on was assigned in the previous instruction. The transformation
itself doesn't check liveness and doesn't remove the assignment. Dead
code elimination should be run afterwards to remove the assignment.
* For Cairo, it only makes sense to convert `br` to `if` for equality
comparisons against zero. The assignment before `br` will always become
dead after converting `br` to `if`, because we convert to SSA before.
This PR adds support for the `anoma{encode, decode, sign, verify,
signDetached, verifyDetached}` functions to the Core evaluator.
## Encoding / Decoding
The serialization of values to `ByteString` for `anomaEncode` reuses the
Stored Core serialization. The Stored Core `Node` is extended to include
closures.
Anoma expects encoding of bytes as little-endian integers. In general
`ByteString -> Integer` is ambiguous because two `ByteString`s that
differ only by zero padding will map to the same integer. So we must
encode the length of the ByteString in the encoded integer alongside the
ByteString data so when it is decoded we can pad appropriately. We use
the same length encoding scheme that is used by Nockma jam.
## Verify
The Core evaluator implementation of `anomaVerify` crashes if the
verification fails. This matches the behaviour of Anoma node.
### `jvc` Support
You can now use `anoma-*` functions within `.jvc` core files.
* Closes https://github.com/anoma/juvix/issues/2808
- This PR adds a temporary compiler error for when the bug #2247
happens. We do not have plans to fix this bug until we move the
typechecker to Core, so it makes sense to add a better error message.
