Nockma compile #2570

janmasrovira · 2023-12-29T16:12:07Z

This PR is a snapshot of the current work on the JuvixAsm -> Nockma translation. The compilation of Juvix programs to Nockma now works so we decided to raise this PR now to avoid it getting too large.

Juvix -> Nockma compilation

You can compile a frontend Juvix file to Nockma as follows:

example.juvix

module example;

import Stdlib.Prelude open;

fib : Nat → Nat → Nat → Nat
  | zero x1 _ := x1
  | (suc n) x1 x2 := fib n x2 (x1 + x2);

fibonacci (n : Nat) : Nat := fib n 0 1;

sumList (xs : List Nat) : Nat :=
  for (acc := 0) (x in xs)
    acc + x;

main : Nat := fibonacci 9 + sumList [1; 2; 3; 4];

$ juvix compile -t nockma example.juvix

This will generate a file example.nockma which can be run using the nockma evaluator:

$ juvix dev nockma eval example.nockma

Alternatively you can compile JuvixAsm to Nockma:

$ juvix dev asm compile -t nockma example.jva

Tests

We compile an evaluate the JuvixAsm tests in https://github.com/anoma/juvix/blob/cb3659e08e552ee9ca40860077e39a4070cf3303/test/Nockma/Compile/Asm/Positive.hs

We currently skip some because either:

They are too slow to run in the current evaluator (due to arithmetic operations using the unjetted nock code from the anoma nock stdlib).
They trace data types like lists and booleans which are represented differently by the asm interpreter and the nock interpreter
They operate on raw negative numbers, nock only supports raw natural numbers

Next steps

On top of this PR we will work on improving the evaluator so that we can enable the slow compilation tests.

lukaszcz · 2024-01-12T12:15:01Z

I refactored the Nockma pipeline to fit more with how other pipelines are handled, moving the JuvixAsm transformations to the function toNockma in Juvix.Compiler.Asm.Pipeline, and adjusting Juvix.Compiler.Pipeline and other places accordingly.

I also removed the --nockma-debug option, because there already is a --debug option. To generate trace pseudo-Nockma instructions, use --debug or -g.

paulcadman · 2024-01-12T12:16:58Z

I refactored the Nockma pipeline to fit more with how other pipelines are handled, moving the JuvixAsm transformations to the function toNockma in Juvix.Compiler.Asm.Pipeline, and adjusting Juvix.Compiler.Pipeline and other places accordingly.

I also removed the --nockma-debug option, because there already is a --debug option. To generate trace pseudo-Nockma instructions, use --debug or -g.

Thanks!

lukaszcz · 2024-01-12T12:18:55Z

I think ultimately the --nockma-pretty option should also be removed in favour of having a separate "pseudo-nockma" target which supports readable names, debugging instructions, generally some inessential but convenient sugar over the actual Nock format. This target would then be serialized to actual Nockma, omitting the traces and translating names to numbers:

Nock serialization #2558.

lukaszcz · 2024-01-12T15:57:44Z

app/Commands/Dev/Core/Repl.hs

@@ -26,7 +26,7 @@ parseText = Core.runParser replPath defaultModuleId

 runRepl :: forall r. (Members '[Embed IO, App] r) => CoreReplOptions -> Core.InfoTable -> Sem r ()
 runRepl opts tab = do
-  embed (putStr "> ")
+  putStr "> "


I don't understand what happened here and why is it in this PR? We don't need embed anymore? This PR changes that all over the place - it should be separate PR doing this refactor.

Done - the PR was raised #2582

lukaszcz · 2024-01-12T15:58:41Z

app/Commands/Dev/Geb/Infer.hs

@@ -27,7 +27,6 @@ runCommand opts = do
            Geb.ppOut
              opts
              (tyMorph ^. Geb.typedMorphismObject)
-          embed $ putStrLn ""


Why removing newline here (not only embed)?

This change was moved to #2582

lukaszcz · 2024-01-12T15:59:48Z

app/Commands/Dev/Geb/Repl.hs

@@ -114,25 +114,25 @@ checkTypedMorphism gebMorphism = Repline.dontCrash $ do
    Right _ -> printError (error "Checking only works on typed Geb morphisms.")

 runReplCommand :: String -> Repl ()
-runReplCommand input =
+runReplCommand input_ =


Analogously with the input that somehow appeared in Prelude or somewhere in this PR and requires adjusting variable names all over the place. This is an unrelated (?) refactor.

This change was moved to #2582

scripts/nockma-stdlib-parser.sh

lukaszcz · 2024-01-12T16:14:00Z

src/Juvix/Compiler/Asm/Transformation/TempHeight.hs

+  FunctionInfo ->
+  Sem r FunctionInfo
+computeFunctionTempHeight tab fi = do
+  ps :: [Command] <- recurseFun sig fi


This can be done with the simplified recursor recurseS. You don't need full memory information & validity checking here -- just stack height info. I'll change it.

lukaszcz · 2024-01-12T16:16:37Z

src/Juvix/Compiler/Backend/Geb/Translation/FromSource.hs

-fromSource fileName input =
-  case runParser fileName input of
+fromSource fileName input' =
+  case runParser fileName input' of


These input name changes really should be in a separate PR, if possible. There's too many of them.

This change was moved to #2582

lukaszcz · 2024-01-12T16:17:04Z

src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs

@@ -288,7 +288,7 @@ goTopModule cs m = do
  htmlOpts <- ask @HtmlOptions
  runReader (htmlOpts {_htmlOptionsKind = HtmlDoc}) $ do
    fpath <- moduleDocPath m
-    Prelude.embed (putStrLn ("Writing " <> pack (toFilePath fpath)))
+    putStrLn ("Writing " <> pack (toFilePath fpath))


Same with removing embed

This change was moved to #2582

lukaszcz · 2024-01-12T16:17:47Z

src/Juvix/Compiler/Concrete/Translation/FromSource.hs

-      input <- getFileContents fileName
-      mp <- runModuleParser fileName input
+      input_ <- getFileContents fileName
+      mp <- runModuleParser fileName input_


Unrelated (?) name changes.

This change was moved to #2582

lukaszcz · 2024-01-12T16:19:49Z

src/Juvix/Compiler/Core/Translation/FromSource.hs

@@ -25,16 +25,16 @@ import Text.Megaparsec qualified as P
 -- | Note: only new symbols and tags that are not in the InfoTable already will be
 -- generated during parsing
 runParser :: Path Abs File -> ModuleId -> InfoTable -> Text -> Either MegaparsecError (InfoTable, Maybe Node)
-runParser fileName mid tab input =
+runParser fileName mid tab input_ =


Name change

This change was moved to #2582

lukaszcz · 2024-01-12T16:20:21Z

src/Juvix/Compiler/Nockma/Evaluator.hs

@@ -44,14 +45,15 @@ subTermT = go
 subTerm :: (Member (Error NockEvalError) r) => Term a -> Path -> Sem r (Term a)
 subTerm term pos = do
  case term ^? subTermT pos of
-    Nothing -> throw InvalidPath
+    -- Nothing -> throw (InvalidPath "subterm")


Remove comment

lukaszcz · 2024-01-12T17:13:04Z

src/Juvix/Compiler/Nockma/Translation/FromAsm.hs

+  }
+
+data StackId
+  = CurrentFunction


What do you need to store the current function for? "Current function" is never referenced in JuvixAsm - functions are always referenced by name.

lukaszcz · 2024-01-12T17:13:21Z

src/Juvix/Compiler/Nockma/Translation/FromAsm.hs

+  = CurrentFunction
+  | ValueStack
+  | TempStack
+  | AuxStack


What's an AuxStack, what do you store there?

lukaszcz · 2024-01-12T17:14:30Z

src/Juvix/Compiler/Nockma/Translation/FromAsm.hs

+  | ValueStack
+  | TempStack
+  | AuxStack
+  | FrameStack


Why do you save the frames in a frame stack? You should just discard them when calling a function and let Nock VM handle that. In fact, you have to discard them for tail recursion to work without leaking memory.

lukaszcz · 2024-01-12T17:50:12Z

src/Juvix/Compiler/Nockma/Translation/FromAsm.hs

+
+  -- Setup function to call with its arguments
+  -- given n, we compute [R..R] of length n
+  if


You're emulating a call stack on top of a Nock VM, so it's slow. You should not be handling the call stack explicitly -- Nock VM already does this and you should use it. Saving/restoring stack frames is not necessary.

A call should just change the Nock subject (transferring the arguments, etc) and evaluate the compiled function call with the new subject. The result of the evaluation should just be pushed on top of the value stack in the calling function.

The ret instruction is then just returns the top of the value stack. I perhaps should've made it more clear that in JuvixAsm ret can only appear in tail positions (like tcall).

For example,

push arg1 push arg2 call f; P;

should be translated to Nock similar to:

[Push arg1* [Push arg2* [Push ["replace subject with new one, with 2 arguments from top of the stack"; fetch & eval f] ["remove the 2nd & 3rd value from top of the value stack (the arguments) - that's one indexing and one replace in Nock"; P*] ] ] ]

where X* is the translation of X, and Push is the nock "push" combinator 8. Note that in the second branch of the final push (for P*) you get the original calling function's subject - that's why you can always avoid explicitly saving/restoring stack frames and let Nock VM handle this.

In fact, almost always the call in JuvixAsm will be like above with the pushes corresponding to the number of arguments. Then we can compile this to slightly better:

[Push [Push arg1* [Push arg2* ["replace subject with new one, with 2 arguments from top of the stack"; fetch & eval f] ] ] P* ]

(we could in fact always recreate the original call tree and avoid removing the arguments after call return).

It also seems merging the stacks as I initially intended (#2559) might lead to a simpler nock code for "replace subject with new one" (but it's a bit more difficult, because you need to keep track of the value/temporary stack heights). Though I'm not completely sure how much simpler.

It matters a lot here whether you generate 1 or 10 instructions for a common operation. This translates to roughly an order of magnitude difference in the running time of generated programs.

EDIT: JuvixAsm is actually a bit too low level. Translating the value stack explicitly was a bad idea of mine and it's unnecessary, because the value stack just represents an applicative structure which can be represented directly in Nock. It's possible, but cumbersome and unnecessary, to recover the applicative structure from JuvixAsm code. We should merge the current version, then refactor the JuvixCore -> JuvixAsm translation into JuvixCore -> JuvixTree -> JuvixAsm, where JuvixTree is like JuvixAsm except that instead of the value stack there is an applicative structure. Then adapt the Asm -> Nock translation to Tree -> Nock.

lukaszcz · 2024-01-12T18:01:06Z

src/Juvix/Compiler/Nockma/Translation/FromAsm.hs

+    -- push the constructor tag at the top
+    push (OpAddress # topOfStack ValueStack ++ constructorPath ConstructorTag)
+    push (constructorTagToTerm tag)
+    testEq


Why do you need to push the stack twice to test for equality, just to immediately replace the pushed values with the equality result? We have [= X Y] in nock, so just use [= [@ S] [K TagValue]]. That would make testing equality several times faster (or more, because slicing/replacement might not be so cheap in Nock VM).

We can't write this the way one writes Haskell, hoping that it'll somehow get optimized later. There's nothing that can optimize this -- we're generating the code and it's all common basic operations.

The trace op is only supported by the Juvix Nockma evaluator.

lukaszcz

Okay, there are still a few unrelated refactors, but let's merge it

janmasrovira added nock backend:nockma labels Dec 29, 2023

janmasrovira self-assigned this Dec 29, 2023

janmasrovira force-pushed the nockma-compile branch from d39022d to d5b4be3 Compare December 30, 2023 19:26

janmasrovira force-pushed the nockma-compile branch from e2579e9 to f54cb4b Compare January 9, 2024 16:41

janmasrovira added this to the 0.6.0 milestone Jan 10, 2024

janmasrovira force-pushed the nockma-compile branch 2 times, most recently from 8472c79 to d29e785 Compare January 10, 2024 16:56

paulcadman force-pushed the nockma-compile branch 2 times, most recently from bc5ad7c to cb3659e Compare January 11, 2024 12:07

janmasrovira assigned paulcadman Jan 11, 2024

paulcadman marked this pull request as ready for review January 11, 2024 12:20

lukaszcz reviewed Jan 12, 2024

View reviewed changes

scripts/nockma-stdlib-parser.sh Show resolved Hide resolved

lukaszcz reviewed Jan 12, 2024

View reviewed changes

paulcadman and others added 23 commits January 16, 2024 16:42

Replace trace stack with output effect

0a924d8

Add nockma test for trace op

101e4ae

Test builtin bool compilation

8a5db9b

Add nockma target as CLI backend

f74223d

Add nockma as asm target and add nockma eval command

72ae346

Fix eval tests

e889f83

Compile and evaluate Asm tests for Nockma

757a76f

Fix formatting

0b425a1

remove Data.Text.IO.writeFile and change .nock -> .nockma

e268e76

add nockma pipeline

07f6e07

fix .nockma file extension

97ee341

compute temp height and fix temporary stack ref

fb09253

fix taill calls

fe731f3

save tempstack wip

191f9c7

Save / restore the activation frame correctly

26f9a84

Refactor function paths

87b9a70

Disable emit of Nockma trace op by default

6e7c0a0

The trace op is only supported by the Juvix Nockma evaluator.

fix after merge

7fbcb3c

refactor Nockma pipeline

9010dc9

recategorise some nockma tests

d48086d

comments

6dbd954

use

346d9e0

Use readFile from Data.Text.IO.Utf8

0bf0a6f

paulcadman force-pushed the nockma-compile branch from 01de866 to 0bf0a6f Compare January 16, 2024 16:42

paulcadman added 2 commits January 16, 2024 16:50

Add description for nockma-stdlib-parser script

bd513b1

Remove comment

95118d1

lukaszcz approved these changes Jan 17, 2024

View reviewed changes

lukaszcz merged commit 73364f4 into main Jan 17, 2024
4 checks passed

lukaszcz deleted the nockma-compile branch January 17, 2024 10:15

paulcadman mentioned this pull request Jan 29, 2024

Translation from JuvixAsm to Nock #2559

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Nockma compile #2570

Nockma compile #2570

janmasrovira commented Dec 29, 2023 •

edited by paulcadman

Loading

lukaszcz commented Jan 12, 2024 •

edited

Loading

paulcadman commented Jan 12, 2024

lukaszcz commented Jan 12, 2024

lukaszcz Jan 12, 2024

paulcadman Jan 16, 2024 •

edited

Loading

lukaszcz Jan 12, 2024

paulcadman Jan 16, 2024

lukaszcz Jan 12, 2024

paulcadman Jan 16, 2024

lukaszcz Jan 12, 2024

lukaszcz Jan 12, 2024 •

edited

Loading

paulcadman Jan 16, 2024

lukaszcz Jan 12, 2024

paulcadman Jan 16, 2024

lukaszcz Jan 12, 2024

paulcadman Jan 16, 2024

lukaszcz Jan 12, 2024

paulcadman Jan 16, 2024

lukaszcz Jan 12, 2024

paulcadman Jan 16, 2024

lukaszcz Jan 12, 2024

lukaszcz Jan 12, 2024

lukaszcz Jan 12, 2024

lukaszcz Jan 12, 2024 •

edited

Loading

lukaszcz Jan 12, 2024

lukaszcz left a comment

Nockma compile #2570

Nockma compile #2570

Conversation

janmasrovira commented Dec 29, 2023 • edited by paulcadman Loading

Juvix -> Nockma compilation

Tests

Next steps

lukaszcz commented Jan 12, 2024 • edited Loading

paulcadman commented Jan 12, 2024

lukaszcz commented Jan 12, 2024

Choose a reason for hiding this comment

paulcadman Jan 16, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lukaszcz Jan 12, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lukaszcz Jan 12, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lukaszcz left a comment

Choose a reason for hiding this comment

janmasrovira commented Dec 29, 2023 •

edited by paulcadman

Loading

lukaszcz commented Jan 12, 2024 •

edited

Loading

paulcadman Jan 16, 2024 •

edited

Loading

lukaszcz Jan 12, 2024 •

edited

Loading

lukaszcz Jan 12, 2024 •

edited

Loading