Add nockma evaluator

[paulcadman]

This PR adds an parser, pretty printer, evaluator, repl and quasi-quoter for Nock terms.

Parser / Pretty Printer

The parser and pretty printer handle both standard Nock terms and 'pretty' Nock terms (where op codes and paths can be named). Standard and pretty Nock forms can be mixed in the same term.

For example instead of [0 2] you can write [@ L].

See

juvix/src/Juvix/Compiler/Nockma/Language.hs

Line 79 in a6028b0

instance Pretty NockOp where

for the correspondence between pretty Nock and Nock operators.

In pretty Nock, paths are represented as strings of L (for head) and R (for tail) instead of the number encoding in standard nock. The character S is used to refer to the whole subject, i.e it is sugar for 1 in standard Nock.

See

juvix/src/Juvix/Compiler/Nockma/Language.hs

Line 177 in a6028b0

encodePath :: Path -> EncodedPath

for the correspondence between pretty Nock path and standard Nock position.

Quasi-quoter

A quasi-quoter is added so Nock terms can be included in the source, e.g [nock| [@ LL] |].

REPL

Launch the repl with juvix dev nockma repl.

A Nock [subject formula] cell is input as subject / formula , e.g:

nockma>  [1 0] / [@ L]
1

The subject can be set using :set-stack.

nockma> :set-stack [1 0]
nockma> [@ L]
1

The subject can be viewed using :get-stack.

nockma> :set-stack [1 0]
nockma> :get-stack
[1 0]

You can assign a Nock term to a variable and use it in another expression:

nockma> r := [@ L]
nockma> [1 0] / r
1

A list of assignments can be read from a file:

$ cat stack.nock
r := [@ L]
$ juvix dev nockma repl
nockma> :load stack.nock
nockma> [1 0] / r
1

• Closes Nock language and evaluator #2557

[lukaszcz]

This doesn't seem to be used anywhere. Is it used for compilation? I think it might be a pain to keep it up-to-date with the actual Nockma stdlib. Maybe a better solution is to have an extra instruction StdLibCall with an enum of functions and translate them to library calls only at serialization, and implement them directly in Haskell for the interpreter?