Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Support Anoma serialisation primitives as Juvix builtin axioms #2764

Closed
paulcadman opened this issue May 3, 2024 · 0 comments · Fixed by #2775
Closed

Support Anoma serialisation primitives as Juvix builtin axioms #2764

paulcadman opened this issue May 3, 2024 · 0 comments · Fixed by #2775
Assignees
@paulcadman
Labels
anoma backend:nockma enhancement New feature or request pending-review
Milestone
0.6.2

Comments

@paulcadman
Copy link
Collaborator

paulcadman commented May 3, 2024 •
edited
Loading

The Anoma hoon stdlib now supports serialisation primitives:

  • jam - serialization from a noun to an atom
  • cue - deserialization from an atom to a noun, the inverse of jam.

We need to make these available as Juvix builtins, in the same way as we did for anomaGet.

Proposed builtins:

--- Encode a value
builtin anoma-encode
axiom anomaEncode : {A : Type} -> A -> Nat;

--- Decode a value
builtin anoma-decode
axiom anomaDecode : {A : Type} -> Nat -> A;
@paulcadman paulcadman added this to the 0.6.2 milestone May 3, 2024
@paulcadman paulcadman self-assigned this May 3, 2024
@paulcadman paulcadman changed the title Support Anoma serialisation primitives as Juvix builtin axioms. Support Anoma serialisation primitives as Juvix builtin axioms May 3, 2024
@paulcadman paulcadman mentioned this issue May 3, 2024
Merged
@paulcadman paulcadman mentioned this issue May 13, 2024
Merged
paulcadman added a commit that referenced this issue May 14, 2024
@paulcadman
Update Anoma nockma stdlib (#2765)
6d660f5 
This PR updates the Anoma nockma stdlib to the version in Anoma 0.13.0
obtained from:

*
https://github.com/anoma/anoma/blob/1bbaf664ad87eb14a9aaf0012ac822a67cbc1a8f/lib/nock.ex#L433

NB: As is documented in the code, the standard library paths are
obtained by running commands in the urbit dojo against the loaded
stdlib. For example to find the path to the `dec` function in the stdlib
run:

```
~zod:dojo> =>  anoma  !=(dec)
[9 342 0 31]
```

Part of:

* #2764
@paulcadman paulcadman linked a pull request May 14, 2024 that will close this issue
Add support for anoma-decode builtin #2775
Merged
paulcadman added a commit that referenced this issue May 15, 2024
@paulcadman
Add support for anoma-decode builtin (#2775)
52f8afd 
This PR adds support for the `anoma-decode` builtin

```
builtin anoma-decode
axiom anomaDecode : {A : Type} -> Nat -> A
```

Adds:
* An implementation of the `cue` function in Haskell
* Unit tests for `cue`
* A benchmark for `cue` applied to the Anoma / nockma stdlib

Benchmark results:

```
      cue (jam stdlib): OK
        36.0 ms ± 2.0 ms
```

Closes:
*  #2764
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@paulcadman paulcadman

Labels
anoma backend:nockma enhancement New feature or request pending-review
Projects
None yet
Milestone
0.6.2
Development

Successfully merging a pull request may close this issue.

Add support for anoma-decode builtin anoma/juvix
1 participant
@paulcadman