Nockma compile (#2570)

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 cb3659e08e/test/Nockma/Compile/Asm/Positive.hs We currently skip some because either: 1. They are too slow to run in the current evaluator (due to arithmetic operations using the unjetted nock code from the anoma nock stdlib). 2. They trace data types like lists and booleans which are represented differently by the asm interpreter and the nock interpreter 3. 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. --------- Co-authored-by: Paul Cadman <git@paulcadman.dev> Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
2024-10-05 20:47:36 +03:00 · 2024-01-17 11:15:38 +01:00 · 2024-01-17 11:15:38 +01:00 · 73364f4887
commit 73364f4887
parent 517897930f
64 changed files with 2212 additions and 232 deletions
--- a/app/App.hs
+++ b/app/App.hs
@ -190,18 +190,17 @@ runPipeline input_ p = do
    Right res -> return (snd res ^. pipelineResult)

 runPipelineHtml :: (Members '[App, Embed IO, TaggedLock] r) => Bool -> AppPath File -> Sem r (InternalTypedResult, [InternalTypedResult])
-runPipelineHtml bNonRecursive input_ =
-  if
-      | bNonRecursive -> do
-          r <- runPipeline input_ upToInternalTyped
-          return (r, [])
-      | otherwise -> do
-          args <- askArgs
-          entry <- getEntryPoint' args input_
-          r <- runPipelineHtmlEither entry
-          case r of
-            Left err -> exitJuvixError err
-            Right res -> return res
+runPipelineHtml bNonRecursive input_
+  | bNonRecursive = do
+      r <- runPipeline input_ upToInternalTyped
+      return (r, [])
+  | otherwise = do
+      args <- askArgs
+      entry <- getEntryPoint' args input_
+      r <- runPipelineHtmlEither entry
+      case r of
+        Left err -> exitJuvixError err
+        Right res -> return res

 runPipelineEntry :: (Members '[App, Embed IO, TaggedLock] r) => EntryPoint -> Sem (PipelineEff r) a -> Sem r a
 runPipelineEntry entry p = do
--- a/app/Commands/Compile.hs
+++ b/app/Commands/Compile.hs
@ -25,12 +25,13 @@ runCommand opts@CompileOptions {..} = do
    TargetVampIR -> Compile.runVampIRPipeline arg
    TargetCore -> writeCoreFile arg
    TargetAsm -> Compile.runAsmPipeline arg
+    TargetNockma -> Compile.runNockmaPipeline arg

 writeCoreFile :: (Members '[Embed IO, App, TaggedLock] r) => Compile.PipelineArg -> Sem r ()
 writeCoreFile pa@Compile.PipelineArg {..} = do
  entryPoint <- Compile.getEntry pa
  coreFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
-  r <- runReader entryPoint $ runError @JuvixError $ Core.toStored _pipelineArgModule
+  r <- runReader entryPoint . runError @JuvixError $ Core.toStored _pipelineArgModule
  case r of
    Left e -> exitJuvixError e
    Right md ->
--- a/app/Commands/Dev/Asm/Compile.hs
+++ b/app/Commands/Dev/Asm/Compile.hs
@ -6,43 +6,58 @@ import Commands.Extra.Compile qualified as Compile
 import Juvix.Compiler.Asm.Translation.FromSource qualified as Asm
 import Juvix.Compiler.Backend qualified as Backend
 import Juvix.Compiler.Backend.C qualified as C
+import Juvix.Compiler.Nockma.Pretty qualified as Nockma

 runCommand :: forall r. (Members '[Embed IO, App, TaggedLock] r) => AsmCompileOptions -> Sem r ()
 runCommand opts = do
  file <- getFile
-  ep <- getEntryPoint (AppPath (preFileFromAbs file) True)
-  tgt <- getTarget (opts ^. compileTarget)
-  let entryPoint :: EntryPoint
-      entryPoint =
-        ep
-          { _entryPointTarget = tgt,
-            _entryPointDebug = opts ^. compileDebug
-          }
  s <- readFile (toFilePath file)
  case Asm.runParser (toFilePath file) s of
    Left err -> exitJuvixError (JuvixError err)
    Right tab -> do
-      case run $ runReader entryPoint $ runError $ asmToMiniC tab of
-        Left err -> exitJuvixError err
-        Right C.MiniCResult {..} -> do
-          buildDir <- askBuildDir
-          ensureDir buildDir
-          cFile <- inputCFile file
-          embed @IO (writeFile (toFilePath cFile) _resultCCode)
-          outfile <- Compile.outputFile opts file
-          Compile.runCommand
-            opts
-              { _compileInputFile = Just (AppPath (preFileFromAbs cFile) False),
-                _compileOutputFile = Just (AppPath (preFileFromAbs outfile) False)
+      ep <- getEntryPoint (AppPath (preFileFromAbs file) True)
+      tgt <- getTarget (opts ^. compileTarget)
+      let entryPoint :: EntryPoint
+          entryPoint =
+            ep
+              { _entryPointTarget = tgt,
+                _entryPointDebug = opts ^. compileDebug
              }
+      case opts ^. compileTarget of
+        TargetNockma -> do
+          c <-
+            runReader entryPoint (runError (asmToNockma tab))
+              >>= either exitJuvixError return
+          let outputCell = Nockma.TermCell c
+              outputText = Nockma.ppPrintOpts nockmaOpts outputCell
+          outfile <- Compile.outputFile opts file
+          embed @IO (writeFileEnsureLn (toFilePath outfile) outputText)
+        _ -> do
+          case run $ runReader entryPoint $ runError $ asmToMiniC tab of
+            Left err -> exitJuvixError err
+            Right C.MiniCResult {..} -> do
+              buildDir <- askBuildDir
+              ensureDir buildDir
+              cFile <- inputCFile file
+              embed @IO $ writeFileEnsureLn (toFilePath cFile) _resultCCode
+              outfile <- Compile.outputFile opts file
+              Compile.runCommand
+                opts
+                  { _compileInputFile = Just (AppPath (preFileFromAbs cFile) False),
+                    _compileOutputFile = Just (AppPath (preFileFromAbs outfile) False)
+                  }
  where
    getFile :: Sem r (Path Abs File)
    getFile = getMainFile (opts ^. compileInputFile)

+    nockmaOpts :: Nockma.Options
+    nockmaOpts = Nockma.defaultOptions {Nockma._optIgnoreHints = not (opts ^. compileNockmaUsePrettySymbols)}
+
    getTarget :: CompileTarget -> Sem r Backend.Target
    getTarget = \case
      TargetWasm32Wasi -> return Backend.TargetCWasm32Wasi
      TargetNative64 -> return Backend.TargetCNative64
+      TargetNockma -> return Backend.TargetNockma
      TargetGeb -> exitMsg (ExitFailure 1) "error: GEB target not supported for JuvixAsm"
      TargetVampIR -> exitMsg (ExitFailure 1) "error: VampIR target not supported for JuvixAsm"
      TargetCore -> exitMsg (ExitFailure 1) "error: JuvixCore target not supported for JuvixAsm"
--- a/app/Commands/Dev/Asm/Compile/Options.hs
+++ b/app/Commands/Dev/Asm/Compile/Options.hs
@ -14,7 +14,8 @@ asmSupportedTargets :: NonEmpty CompileTarget
 asmSupportedTargets =
  NonEmpty.fromList
    [ TargetWasm32Wasi,
-      TargetNative64
+      TargetNative64,
+      TargetNockma
    ]

 parseAsmCompileOptions :: Parser AsmCompileOptions
--- a/app/Commands/Dev/Core/Compile.hs
+++ b/app/Commands/Dev/Core/Compile.hs
@ -19,6 +19,7 @@ runCommand opts = do
    TargetVampIR -> runVampIRPipeline arg
    TargetCore -> return ()
    TargetAsm -> runAsmPipeline arg
+    TargetNockma -> runNockmaPipeline arg
  where
    getFile :: Sem r (Path Abs File)
    getFile = getMainFile (opts ^. compileInputFile)
--- a/app/Commands/Dev/Core/Compile/Base.hs
+++ b/app/Commands/Dev/Core/Compile/Base.hs
@ -9,6 +9,7 @@ import Juvix.Compiler.Backend.C qualified as C
 import Juvix.Compiler.Backend.Geb qualified as Geb
 import Juvix.Compiler.Backend.VampIR.Translation qualified as VampIR
 import Juvix.Compiler.Core.Data.Module qualified as Core
+import Juvix.Compiler.Nockma.Pretty qualified as Nockma
 import System.FilePath (takeBaseName)

 data PipelineArg = PipelineArg
@ -37,6 +38,7 @@ getEntry PipelineArg {..} = do
      TargetVampIR -> Backend.TargetVampIR
      TargetCore -> Backend.TargetCore
      TargetAsm -> Backend.TargetAsm
+      TargetNockma -> Backend.TargetNockma

    defaultOptLevel :: Int
    defaultOptLevel
@ -74,15 +76,14 @@ runGebPipeline ::
 runGebPipeline pa@PipelineArg {..} = do
  entryPoint <- getEntry pa
  gebFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
-  let spec =
-        if
-            | _pipelineArgOptions ^. compileTerm -> Geb.OnlyTerm
-            | otherwise ->
-                Geb.LispPackage
-                  Geb.LispPackageSpec
-                    { _lispPackageName = fromString $ takeBaseName $ toFilePath gebFile,
-                      _lispPackageEntry = "*entry*"
-                    }
+  let spec
+        | _pipelineArgOptions ^. compileTerm = Geb.OnlyTerm
+        | otherwise =
+            Geb.LispPackage
+              Geb.LispPackageSpec
+                { _lispPackageName = fromString $ takeBaseName $ toFilePath gebFile,
+                  _lispPackageEntry = "*entry*"
+                }
  Geb.Result {..} <- getRight (run (runReader entryPoint (runError (coreToGeb spec _pipelineArgModule :: Sem '[Error JuvixError, Reader EntryPoint] Geb.Result))))
  embed @IO (writeFile (toFilePath gebFile) _resultCode)

@ -101,7 +102,24 @@ runAsmPipeline :: (Members '[Embed IO, App, TaggedLock] r) => PipelineArg -> Sem
 runAsmPipeline pa@PipelineArg {..} = do
  entryPoint <- getEntry pa
  asmFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
-  r <- runReader entryPoint $ runError @JuvixError (coreToAsm _pipelineArgModule)
+  r <-
+    runReader entryPoint
+      . runError @JuvixError
+      . coreToAsm
+      $ _pipelineArgModule
  tab' <- getRight r
  let code = Asm.ppPrint tab' tab'
  embed @IO (writeFile (toFilePath asmFile) code)
+
+runNockmaPipeline :: (Members '[Embed IO, App, TaggedLock] r) => PipelineArg -> Sem r ()
+runNockmaPipeline pa@PipelineArg {..} = do
+  entryPoint <- getEntry pa
+  nockmaFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
+  r <-
+    runReader entryPoint
+      . runError @JuvixError
+      . coreToNockma
+      $ _pipelineArgModule
+  tab' <- getRight r
+  let code = Nockma.ppSerialize tab'
+  embed @IO (writeFile (toFilePath nockmaFile) code)
--- a/app/Commands/Dev/Nockma.hs
+++ b/app/Commands/Dev/Nockma.hs
@ -1,9 +1,11 @@
 module Commands.Dev.Nockma where

 import Commands.Base
+import Commands.Dev.Nockma.Eval as FromAsm
 import Commands.Dev.Nockma.Options
 import Commands.Dev.Nockma.Repl as Repl

 runCommand :: forall r. (Members '[Embed IO, App] r) => NockmaCommand -> Sem r ()
 runCommand = \case
  NockmaRepl opts -> Repl.runCommand opts
+  NockmaEval opts -> FromAsm.runCommand opts
--- a/app/Commands/Dev/Nockma/Eval.hs
+++ b/app/Commands/Dev/Nockma/Eval.hs
@ -0,0 +1,29 @@
+module Commands.Dev.Nockma.Eval where
+
+import Commands.Base hiding (Atom)
+import Commands.Dev.Nockma.Eval.Options
+import Juvix.Compiler.Nockma.Pretty
+import Juvix.Compiler.Nockma.Translation.FromAsm
+import Juvix.Compiler.Nockma.Translation.FromSource qualified as Nockma
+
+runCommand :: forall r. (Members '[Embed IO, App] r) => NockmaEvalOptions -> Sem r ()
+runCommand opts = do
+  afile <- fromAppPathFile file
+  parsedTerm <- Nockma.parseTermFile (toFilePath afile)
+  case parsedTerm of
+    Left err -> exitJuvixError (JuvixError err)
+    Right (TermCell c) -> do
+      res <- runOutputSem @(Term Natural) (say . ppTrace) (evalCompiledNock' (c ^. cellLeft) (c ^. cellRight))
+      ret <- getReturn res
+      putStrLn (ppPrint ret)
+    Right TermAtom {} -> exitFailMsg "Expected nockma input to be a cell"
+  where
+    file :: AppPath File
+    file = opts ^. nockmaEvalFile
+
+    getReturn :: Term Natural -> Sem r (Term Natural)
+    getReturn res =
+      let valStack = getStack ValueStack res
+       in case valStack of
+            TermCell c -> return (c ^. cellLeft)
+            TermAtom {} -> exitFailMsg "Program does not return a value"
--- a/app/Commands/Dev/Nockma/Eval/Options.hs
+++ b/app/Commands/Dev/Nockma/Eval/Options.hs
@ -0,0 +1,15 @@
+module Commands.Dev.Nockma.Eval.Options where
+
+import CommonOptions
+
+newtype NockmaEvalOptions = NockmaEvalOptions
+  { _nockmaEvalFile :: AppPath File
+  }
+  deriving stock (Data)
+
+makeLenses ''NockmaEvalOptions
+
+parseNockmaEvalOptions :: Parser NockmaEvalOptions
+parseNockmaEvalOptions = do
+  _nockmaEvalFile <- parseInputFile FileExtNockma
+  pure NockmaEvalOptions {..}
--- a/app/Commands/Dev/Nockma/Options.hs
+++ b/app/Commands/Dev/Nockma/Options.hs
@ -1,20 +1,36 @@
 module Commands.Dev.Nockma.Options where

+import Commands.Dev.Nockma.Eval.Options
 import Commands.Dev.Nockma.Repl.Options
 import CommonOptions

 data NockmaCommand
  = NockmaRepl NockmaReplOptions
+  | NockmaEval NockmaEvalOptions
  deriving stock (Data)

 parseNockmaCommand :: Parser NockmaCommand
-parseNockmaCommand = hsubparser commandRepl
+parseNockmaCommand =
+  hsubparser $
+    mconcat
+      [ commandRepl,
+        commandFromAsm
+      ]
  where
+    commandFromAsm :: Mod CommandFields NockmaCommand
+    commandFromAsm = command "eval" fromAsmInfo
+      where
+        fromAsmInfo :: ParserInfo NockmaCommand
+        fromAsmInfo =
+          info
+            (NockmaEval <$> parseNockmaEvalOptions)
+            (progDesc "Evaluate a nockma file. The file should contain a single nockma cell: [subject formula]")
+
    commandRepl :: Mod CommandFields NockmaCommand
    commandRepl = command "repl" replInfo
-
-    replInfo :: ParserInfo NockmaCommand
-    replInfo =
-      info
-        (NockmaRepl <$> parseNockmaReplOptions)
-        (progDesc "Run the nockma repl")
+      where
+        replInfo :: ParserInfo NockmaCommand
+        replInfo =
+          info
+            (NockmaRepl <$> parseNockmaReplOptions)
+            (progDesc "Run the nockma repl")
--- a/app/Commands/Dev/Nockma/Repl.hs
+++ b/app/Commands/Dev/Nockma/Repl.hs
@ -10,9 +10,9 @@ import Data.String.Interpolate (__i)
 import Juvix.Compiler.Nockma.Evaluator (NockEvalError, evalRepl, fromReplTerm, programAssignments)
 import Juvix.Compiler.Nockma.Language
 import Juvix.Compiler.Nockma.Pretty (ppPrint)
+import Juvix.Compiler.Nockma.Pretty qualified as Nockma
 import Juvix.Compiler.Nockma.Translation.FromSource (parseProgramFile, parseReplStatement, parseReplText, parseText)
 import Juvix.Parser.Error
-import Juvix.Prelude.Pretty
 import System.Console.Haskeline
 import System.Console.Repline qualified as Repline
 import Prelude (read)
@ -102,11 +102,6 @@ getProgram = State.gets (^. replStateProgram)
 readProgram :: FilePath -> Repl (Program Natural)
 readProgram s = fromMegaParsecError <$> parseProgramFile s

-fromMegaParsecError :: Either MegaparsecError a -> a
-fromMegaParsecError = \case
-  Left e -> error (prettyText e)
-  Right a -> a
-
 direction' :: String -> Repl ()
 direction' s = Repline.dontCrash $ do
  let n = read s :: Natural
@ -136,11 +131,12 @@ evalStatement = \case
  ReplStatementExpression t -> do
    s <- getStack
    prog <- getProgram
-    let et =
-          run
-            . runError @(ErrNockNatural Natural)
-            . runError @NockEvalError
-            $ evalRepl prog s t
+    et <-
+      liftIO
+        $ runM
+          . runError @(ErrNockNatural Natural)
+          . runError @NockEvalError
+        $ evalRepl (putStrLn . Nockma.ppTrace) prog s t
    case et of
      Left e -> error (show e)
      Right ev -> case ev of
--- a/app/Commands/Dev/Nockma/Repl/Options.hs
+++ b/app/Commands/Dev/Nockma/Repl/Options.hs
@ -9,5 +9,5 @@ newtype NockmaReplOptions = NockmaReplOptions

 parseNockmaReplOptions :: Parser NockmaReplOptions
 parseNockmaReplOptions = do
-  _nockmaReplOptionsStackFile <- optional (parseInputFile FileExtNock)
+  _nockmaReplOptionsStackFile <- optional (parseInputFile FileExtNockma)
  pure NockmaReplOptions {..}
--- a/app/Commands/Extra/Compile.hs
+++ b/app/Commands/Extra/Compile.hs
@ -29,23 +29,27 @@ runCompile inputFile o = do
  case o ^. compileTarget of
    TargetWasm32Wasi -> runError (clangWasmWasiCompile inputFile o)
    TargetNative64 -> runError (clangNativeCompile inputFile o)
-    TargetGeb -> return $ Right ()
-    TargetVampIR -> return $ Right ()
-    TargetCore -> return $ Right ()
-    TargetAsm -> return $ Right ()
+    TargetGeb -> return (Right ())
+    TargetVampIR -> return (Right ())
+    TargetCore -> return (Right ())
+    TargetAsm -> return (Right ())
+    TargetNockma -> return (Right ())

 prepareRuntime :: forall r. (Members '[App, Embed IO] r) => Path Abs Dir -> CompileOptions -> Sem r ()
 prepareRuntime buildDir o = do
  mapM_ writeHeader headersDir
  case o ^. compileTarget of
-    TargetWasm32Wasi | o ^. compileDebug -> writeRuntime wasiDebugRuntime
+    TargetWasm32Wasi
+      | o ^. compileDebug -> writeRuntime wasiDebugRuntime
    TargetWasm32Wasi -> writeRuntime wasiReleaseRuntime
-    TargetNative64 | o ^. compileDebug -> writeRuntime nativeDebugRuntime
+    TargetNative64
+      | o ^. compileDebug -> writeRuntime nativeDebugRuntime
    TargetNative64 -> writeRuntime nativeReleaseRuntime
    TargetGeb -> return ()
    TargetVampIR -> return ()
    TargetCore -> return ()
    TargetAsm -> return ()
+    TargetNockma -> return ()
  where
    wasiReleaseRuntime :: BS.ByteString
    wasiReleaseRuntime = $(FE.makeRelativeToProject "runtime/_build.wasm32-wasi/libjuvix.a" >>= FE.embedFile)
@ -84,28 +88,27 @@ outputFile opts inputFile =
      invokeDir <- askInvokeDir
      let baseOutputFile = invokeDir <//> filename inputFile
      return $ case opts ^. compileTarget of
-        TargetNative64 ->
-          if
-              | opts ^. compileCOutput -> replaceExtension' cFileExt inputFile
-              | opts ^. compilePreprocess -> addExtension' cFileExt (addExtension' ".out" (removeExtension' inputFile))
-              | opts ^. compileAssembly -> replaceExtension' ".s" inputFile
-              | otherwise -> removeExtension' baseOutputFile
-        TargetWasm32Wasi ->
-          if
-              | opts ^. compileCOutput -> replaceExtension' cFileExt inputFile
-              | opts ^. compilePreprocess -> addExtension' cFileExt (addExtension' ".out" (removeExtension' inputFile))
-              | opts ^. compileAssembly -> replaceExtension' ".wat" inputFile
-              | otherwise -> replaceExtension' ".wasm" baseOutputFile
-        TargetGeb ->
-          if
-              | opts ^. compileTerm -> replaceExtension' juvixGebFileExt inputFile
-              | otherwise -> replaceExtension' lispFileExt baseOutputFile
+        TargetNative64
+          | opts ^. compileCOutput -> replaceExtension' cFileExt inputFile
+          | opts ^. compilePreprocess -> addExtension' cFileExt (addExtension' ".out" (removeExtension' inputFile))
+          | opts ^. compileAssembly -> replaceExtension' ".s" inputFile
+          | otherwise -> removeExtension' baseOutputFile
+        TargetWasm32Wasi
+          | opts ^. compileCOutput -> replaceExtension' cFileExt inputFile
+          | opts ^. compilePreprocess -> addExtension' cFileExt (addExtension' ".out" (removeExtension' inputFile))
+          | opts ^. compileAssembly -> replaceExtension' ".wat" inputFile
+          | otherwise -> replaceExtension' ".wasm" baseOutputFile
+        TargetGeb
+          | opts ^. compileTerm -> replaceExtension' juvixGebFileExt inputFile
+          | otherwise -> replaceExtension' lispFileExt baseOutputFile
        TargetVampIR ->
          replaceExtension' vampIRFileExt baseOutputFile
        TargetCore ->
          replaceExtension' juvixCoreFileExt baseOutputFile
        TargetAsm ->
          replaceExtension' juvixAsmFileExt baseOutputFile
+        TargetNockma ->
+          replaceExtension' nockmaFileExt baseOutputFile

 clangNativeCompile ::
  forall r.
--- a/app/Commands/Extra/Compile/Options.hs
+++ b/app/Commands/Extra/Compile/Options.hs
@ -11,6 +11,7 @@ data CompileTarget
  | TargetVampIR
  | TargetCore
  | TargetAsm
+  | TargetNockma
  deriving stock (Eq, Data, Bounded, Enum)

 instance Show CompileTarget where
@ -21,6 +22,7 @@ instance Show CompileTarget where
    TargetVampIR -> "vampir"
    TargetCore -> "core"
    TargetAsm -> "asm"
+    TargetNockma -> "nockma"

 data CompileOptions = CompileOptions
  { _compileDebug :: Bool,
@ -33,7 +35,8 @@ data CompileOptions = CompileOptions
    _compileTarget :: CompileTarget,
    _compileInputFile :: Maybe (AppPath File),
    _compileOptimizationLevel :: Maybe Int,
-    _compileInliningDepth :: Int
+    _compileInliningDepth :: Int,
+    _compileNockmaUsePrettySymbols :: Bool
  }
  deriving stock (Data)

@ -83,6 +86,11 @@ parseCompileOptions supportedTargets parserFile = do
              )
        | otherwise ->
            pure False
+  _compileNockmaUsePrettySymbols <-
+    switch
+      ( long "nockma-pretty"
+          <> help "Use names for op codes and paths in Nockma output (for target: nockma)"
+      )
  _compileUnsafe <-
    if
        | elem TargetVampIR supportedTargets ->
--- a/package.yaml
+++ b/package.yaml
@ -143,6 +143,7 @@ default-extensions:
  - NoFieldSelectors
  - NoImplicitPrelude
  - OverloadedStrings
+  - QuasiQuotes
  - RecordWildCards
  - TemplateHaskell
  - TypeFamilyDependencies
--- a/scripts/migrate-juvix-yaml.sh
+++ b/scripts/migrate-juvix-yaml.sh
--- a/scripts/nockma-stdlib-parser.sh
+++ b/scripts/nockma-stdlib-parser.sh
@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+#
+# Description:
+# A script that extracts the Nock locations of functions from comments in the the
+# anoma.hoon standard library:
+#
+# For example we want to extract the location "342" for the function dec.:
+# https://github.com/anoma/anoma/blob/9904ff81218c1a690027a481beb0b6d39e378a07/hoon/anoma.hoon#L12
+# ```
+# ++  dec  ::  +342
+# ```
+#
+# Usage:
+# chmod +x nockma-stdlib-parser.sh
+# ./nockma-stdlib-parser.sh < anoma.hoon
+
+# Use grep to find lines matching the pattern and awk to format the output
+# Reads from stdin
+grep -oP '\+\+  \K\w+\s+::\s+\+\d+' | awk '{gsub("::  \\+", ""); print}'
--- a/src/Juvix/Compiler/Asm/Data.hs
+++ b/src/Juvix/Compiler/Asm/Data.hs
@ -7,4 +7,4 @@ where

 import Juvix.Compiler.Asm.Data.InfoTable
 import Juvix.Compiler.Asm.Data.InfoTableBuilder
-import Juvix.Compiler.Asm.Data.Stack
+import Juvix.Compiler.Asm.Data.Stack hiding (empty)
--- a/src/Juvix/Compiler/Asm/Data/CallGraph.hs
+++ b/src/Juvix/Compiler/Asm/Data/CallGraph.hs
@ -3,7 +3,6 @@ module Juvix.Compiler.Asm.Data.CallGraph where
 import Data.HashSet qualified as HashSet
 import Juvix.Compiler.Asm.Data.InfoTable
 import Juvix.Compiler.Asm.Extra
-import Juvix.Compiler.Asm.Language

 -- | Call graph type
 type CallGraph = DependencyInfo Symbol
--- a/src/Juvix/Compiler/Asm/Data/InfoTable.hs
+++ b/src/Juvix/Compiler/Asm/Data/InfoTable.hs
@ -1,6 +1,7 @@
 module Juvix.Compiler.Asm.Data.InfoTable
  ( module Juvix.Compiler.Asm.Data.InfoTable,
    module Juvix.Compiler.Asm.Language.Rep,
+    module Juvix.Compiler.Asm.Language,
    module Juvix.Compiler.Asm.Language.Type,
  )
 where
--- a/src/Juvix/Compiler/Asm/Data/InfoTableBuilder.hs
+++ b/src/Juvix/Compiler/Asm/Data/InfoTableBuilder.hs
@ -2,7 +2,6 @@ module Juvix.Compiler.Asm.Data.InfoTableBuilder where

 import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Asm.Data.InfoTable
-import Juvix.Compiler.Asm.Language

 data IdentKind
  = IdentFun Symbol
@ -58,7 +57,7 @@ runInfoTableBuilder' bs =
      FreshTag -> do
        modify' (over stateNextUserTag (+ 1))
        s <- get
-        return (UserTag defaultModuleId (s ^. stateNextUserTag - 1))
+        return (UserTag (TagUser defaultModuleId (s ^. stateNextUserTag - 1)))
      RegisterFunction fi -> do
        modify' (over (stateInfoTable . infoFunctions) (HashMap.insert (fi ^. functionSymbol) fi))
        modify' (over stateIdents (HashMap.insert (fi ^. functionName) (IdentFun (fi ^. functionSymbol))))
--- a/src/Juvix/Compiler/Asm/Extra/Apply.hs
+++ b/src/Juvix/Compiler/Asm/Extra/Apply.hs
@ -5,7 +5,6 @@ import Data.HashMap.Strict qualified as HashMap
 import Data.Text.Encoding
 import Juvix.Compiler.Asm.Data.InfoTable
 import Juvix.Compiler.Asm.Data.InfoTableBuilder
-import Juvix.Compiler.Asm.Language
 import Juvix.Compiler.Asm.Translation.FromSource

 data ApplyBuiltins = ApplyBuiltins
--- a/src/Juvix/Compiler/Asm/Extra/Base.hs
+++ b/src/Juvix/Compiler/Asm/Extra/Base.hs
@ -1,7 +1,6 @@
 module Juvix.Compiler.Asm.Extra.Base where

 import Juvix.Compiler.Asm.Data.InfoTable
-import Juvix.Compiler.Asm.Language

 mkInstr :: Instruction -> Command
 mkInstr = Instr . CmdInstr emptyInfo
--- a/src/Juvix/Compiler/Asm/Extra/Memory.hs
+++ b/src/Juvix/Compiler/Asm/Extra/Memory.hs
@ -6,7 +6,6 @@ import Juvix.Compiler.Asm.Data.Stack (Stack)
 import Juvix.Compiler.Asm.Data.Stack qualified as Stack
 import Juvix.Compiler.Asm.Error
 import Juvix.Compiler.Asm.Extra.Type
-import Juvix.Compiler.Asm.Language
 import Juvix.Compiler.Asm.Pretty
 import Safe (atMay)

@ -100,8 +99,8 @@ getDirectRefType dr mem = case dr of
    topValueStack 0 mem
  ArgRef OffsetRef {..} ->
    getArgumentType _offsetRefOffset mem
-  TempRef OffsetRef {..} ->
-    bottomTempStack _offsetRefOffset mem
+  TempRef RefTemp {..} ->
+    bottomTempStack (_refTempOffsetRef ^. offsetRefOffset) mem

 getValueType' :: (Member (Error AsmError) r) => Maybe Location -> InfoTable -> Memory -> Value -> Sem r Type
 getValueType' loc tab mem = \case
--- a/src/Juvix/Compiler/Asm/Extra/Recursors.hs
+++ b/src/Juvix/Compiler/Asm/Extra/Recursors.hs
@ -10,7 +10,6 @@ import Juvix.Compiler.Asm.Error
 import Juvix.Compiler.Asm.Extra.Base
 import Juvix.Compiler.Asm.Extra.Memory
 import Juvix.Compiler.Asm.Extra.Type
-import Juvix.Compiler.Asm.Language
 import Juvix.Compiler.Asm.Pretty

 -- | Recursor signature. Contains read-only recursor parameters.
@ -24,6 +23,8 @@ data RecursorSig m r a = RecursorSig

 makeLenses ''RecursorSig

+-- | General recursor function. For most uses it is probably an overkill.
+-- Consider using `recurseS` if you only need stack height information.
 recurseFun :: (Member (Error AsmError) r) => RecursorSig Memory r a -> FunctionInfo -> Sem r [a]
 recurseFun sig fi = recurse sig (argumentsFromFunctionInfo fi) (fi ^. functionCode)

--- a/src/Juvix/Compiler/Asm/Extra/Type.hs
+++ b/src/Juvix/Compiler/Asm/Extra/Type.hs
@ -3,7 +3,6 @@ module Juvix.Compiler.Asm.Extra.Type where
 import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Asm.Data.InfoTable
 import Juvix.Compiler.Asm.Error
-import Juvix.Compiler.Asm.Language
 import Juvix.Compiler.Asm.Pretty

 mkTypeInteger :: Type
--- a/src/Juvix/Compiler/Asm/Interpreter.hs
+++ b/src/Juvix/Compiler/Asm/Interpreter.hs
@ -219,25 +219,27 @@ runCodeR infoTable funInfo = goCode (funInfo ^. functionCode) >> popLastValueSta
      ConstVoid -> return ValVoid
      Ref r -> getMemVal r

-    getMemVal :: (Member Runtime r) => MemValue -> Sem r Val
+    getMemVal :: forall r. (Member Runtime r) => MemValue -> Sem r Val
    getMemVal = \case
      DRef dr -> getDirectRef dr
      ConstrRef cr -> do
-        v <- getDirectRef (cr ^. fieldRef)
-        case v of
-          ValConstr ctr ->
-            if
-                | cr ^. fieldOffset < length (ctr ^. constrArgs) ->
-                    return $ (ctr ^. constrArgs) !! (cr ^. fieldOffset)
-                | otherwise ->
-                    runtimeError "invalid constructor field access"
-          _ -> runtimeError "invalid memory access: expected a constructor"
+        ctr <- getDirectRef (cr ^. fieldRef) >>= getConstr
+        if
+            | cr ^. fieldOffset < length (ctr ^. constrArgs) ->
+                return $ (ctr ^. constrArgs) !! (cr ^. fieldOffset)
+            | otherwise ->
+                runtimeError "invalid constructor field access"
+        where
+          getConstr :: Val -> Sem r Constr
+          getConstr = \case
+            ValConstr ctr -> return ctr
+            _ -> runtimeError "invalid memory access: expected a constructor"

    getDirectRef :: (Member Runtime r) => DirectRef -> Sem r Val
    getDirectRef = \case
      StackRef -> topValueStack
      ArgRef OffsetRef {..} -> readArg _offsetRefOffset
-      TempRef OffsetRef {..} -> readTemp _offsetRefOffset
+      TempRef r -> readTemp r

    popLastValueStack :: (Member Runtime r) => Sem r Val
    popLastValueStack = do
@ -248,30 +250,32 @@ runCodeR infoTable funInfo = goCode (funInfo ^. functionCode) >> popLastValueSta
        (runtimeError "value stack not empty on function return")
      return v

-    getCallDetails :: (Member Runtime r) => Maybe Location -> InstrCall -> Sem r (Code, Frame)
+    getCallDetails :: forall r. (Member Runtime r) => Maybe Location -> InstrCall -> Sem r (Code, Frame)
    getCallDetails loc InstrCall {..} = case _callType of
      CallFun sym -> do
        let fi = lookupFunInfo infoTable sym
-        when
-          (_callArgsNum /= fi ^. functionArgsNum)
+        unless
+          (_callArgsNum == fi ^. functionArgsNum)
          (runtimeError "invalid direct call: supplied arguments number not equal to expected arguments number")
        args <- replicateM (fi ^. functionArgsNum) popValueStack
        return (fi ^. functionCode, frameFromFunctionInfo loc fi args)
      CallClosure -> do
-        v <- popValueStack
-        case v of
-          ValClosure cl -> do
-            let fi = lookupFunInfo infoTable (cl ^. closureSymbol)
-                n = length (cl ^. closureArgs)
-            when
-              (n >= fi ^. functionArgsNum)
-              (runtimeError "invalid closure: too many arguments")
-            when
-              (_callArgsNum /= fi ^. functionArgsNum - n)
-              (runtimeError "invalid indirect call: supplied arguments number not equal to expected arguments number")
-            frm <- getCallFrame loc cl fi _callArgsNum
-            return (fi ^. functionCode, frm)
-          _ -> runtimeError "invalid indirect call: expected closure on top of value stack"
+        cl <- popValueStack >>= closureFromValue
+        let fi = lookupFunInfo infoTable (cl ^. closureSymbol)
+            clArgs = length (cl ^. closureArgs)
+        unless
+          (clArgs < fi ^. functionArgsNum)
+          (runtimeError "invalid closure: too many arguments")
+        unless
+          (clArgs + _callArgsNum == fi ^. functionArgsNum)
+          (runtimeError "invalid indirect call: supplied arguments number not equal to expected arguments number")
+        frm <- getCallFrame loc cl fi _callArgsNum
+        return (fi ^. functionCode, frm)
+        where
+          closureFromValue :: Val -> Sem r Closure
+          closureFromValue = \case
+            ValClosure cl -> return cl
+            _ -> runtimeError "invalid indirect call: expected closure on top of value stack"

    getCallFrame :: (Member Runtime r) => Maybe Location -> Closure -> FunctionInfo -> Int -> Sem r Frame
    getCallFrame loc cl fi argsNum = do
--- a/src/Juvix/Compiler/Asm/Interpreter/Runtime.hs
+++ b/src/Juvix/Compiler/Asm/Interpreter/Runtime.hs
@ -25,7 +25,7 @@ data Runtime m a where
  ReplaceFrame :: Frame -> Runtime m ()
  ReplaceTailFrame :: Frame -> Runtime m ()
  ReadArg :: Offset -> Runtime m Val
-  ReadTemp :: Offset -> Runtime m Val
+  ReadTemp :: RefTemp -> Runtime m Val
  PushTempStack :: Val -> Runtime m ()
  PopTempStack :: Runtime m ()
  LogMessage :: Text -> Runtime m ()
@ -79,13 +79,13 @@ runRuntime tab = runState (RuntimeState (CallStack []) emptyFrame [] Nothing tab
        return $
          fromMaybe
            (throwRuntimeError s "invalid argument area read")
-            (HashMap.lookup off (s ^. (runtimeFrame . frameArgs . argumentArea)))
-      ReadTemp off -> do
+            (HashMap.lookup off (s ^. runtimeFrame . frameArgs . argumentArea))
+      ReadTemp r -> do
        s <- get
        return $
          fromMaybe
            (throwRuntimeError s "invalid temporary stack read")
-            (Stack.nthFromBottom off (s ^. (runtimeFrame . frameTemp . temporaryStack)))
+            (Stack.nthFromBottom (r ^. refTempOffsetRef . offsetRefOffset) (s ^. runtimeFrame . frameTemp . temporaryStack))
      PushTempStack val ->
        modify' (over (runtimeFrame . frameTemp) (over temporaryStack (Stack.push val)))
      PopTempStack ->
--- a/src/Juvix/Compiler/Asm/Language.hs
+++ b/src/Juvix/Compiler/Asm/Language.hs
@ -50,7 +50,15 @@ data DirectRef
  | -- | TempRef references a value in the temporary stack (0-based offsets,
    --   counted from the *bottom* of the temporary stack). JVA code:
    --   'tmp[<offset>]'.
-    TempRef OffsetRef
+    TempRef RefTemp
+
+mkTempRef :: OffsetRef -> DirectRef
+mkTempRef o = TempRef (RefTemp o Nothing)
+
+data RefTemp = RefTemp
+  { _refTempOffsetRef :: OffsetRef,
+    _refTempTempHeight :: Maybe Int
+  }

 data OffsetRef = OffsetRef
  { _offsetRefOffset :: Offset,
@ -67,11 +75,14 @@ data Field = Field
    _fieldOffset :: Offset
  }

+makeLenses ''RefTemp
 makeLenses ''Field
 makeLenses ''OffsetRef

 -- | Function call type
-data CallType = CallFun Symbol | CallClosure
+data CallType
+  = CallFun Symbol
+  | CallClosure
  deriving stock (Eq)

 -- | `Instruction` is a single non-branching instruction, i.e., with no control
@ -156,6 +167,7 @@ data Instruction
  | -- | Pushes the top of the current value stack on top of the calling function
    -- value stack, discards the current activation frame, transfers control to
    -- the address at the top of the global call stack, and pops the call stack.
+    -- The return instruction can only appear in tail position in a function.
    -- JVA opcode: 'ret'.
    Return

--- a/src/Juvix/Compiler/Asm/Pipeline.hs
+++ b/src/Juvix/Compiler/Asm/Pipeline.hs
@ -7,7 +7,6 @@ where

 import Juvix.Compiler.Asm.Data.InfoTable
 import Juvix.Compiler.Asm.Extra
-import Juvix.Compiler.Asm.Language
 import Juvix.Compiler.Asm.Options
 import Juvix.Compiler.Asm.Transformation
 import Juvix.Compiler.Pipeline.EntryPoint
@ -17,5 +16,13 @@ import Juvix.Compiler.Pipeline.EntryPoint
 toReg' :: (Members '[Error AsmError, Reader Options] r) => InfoTable -> Sem r InfoTable
 toReg' = validate >=> filterUnreachable >=> computeStackUsage >=> computePrealloc

+-- | Perform transformations on JuvixAsm necessary before the translation to
+-- Nockma
+toNockma' :: (Members '[Error AsmError, Reader Options] r) => InfoTable -> Sem r InfoTable
+toNockma' = validate >=> computeApply >=> filterUnreachable >=> computeTempHeight
+
 toReg :: (Members '[Error JuvixError, Reader EntryPoint] r) => InfoTable -> Sem r InfoTable
 toReg = mapReader fromEntryPoint . mapError (JuvixError @AsmError) . toReg'
+
+toNockma :: (Members '[Error JuvixError, Reader EntryPoint] r) => InfoTable -> Sem r InfoTable
+toNockma = mapReader fromEntryPoint . mapError (JuvixError @AsmError) . toNockma'
--- a/src/Juvix/Compiler/Asm/Pretty.hs
+++ b/src/Juvix/Compiler/Asm/Pretty.hs
@ -9,7 +9,6 @@ import Juvix.Compiler.Asm.Data.InfoTable
 import Juvix.Compiler.Asm.Pretty.Base
 import Juvix.Compiler.Asm.Pretty.Options
 import Juvix.Data.PPOutput
-import Juvix.Prelude
 import Prettyprinter.Render.Terminal qualified as Ansi

 ppOutDefault :: (PrettyCode c) => InfoTable -> c -> AnsiText
--- a/src/Juvix/Compiler/Asm/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Asm/Pretty/Base.hs
@ -215,12 +215,14 @@ ppOffsetRef :: Text -> OffsetRef -> Sem r (Doc Ann)
 ppOffsetRef str OffsetRef {..} =
  return $ maybe (variable str <> lbracket <> integer _offsetRefOffset <> rbracket) variable _offsetRefName

+instance PrettyCode RefTemp where
+  ppCode = ppOffsetRef Str.tmp . (^. refTempOffsetRef)
+
 instance PrettyCode DirectRef where
-  ppCode :: DirectRef -> Sem r (Doc Ann)
  ppCode = \case
    StackRef -> return $ variable Str.dollar
    ArgRef roff -> ppOffsetRef Str.arg roff
-    TempRef roff -> ppOffsetRef Str.tmp roff
+    TempRef roff -> ppCode roff

 instance PrettyCode Field where
  ppCode :: (Member (Reader Options) r) => Field -> Sem r (Doc Ann)
@ -398,7 +400,7 @@ instance PrettyCode InfoTable where
        HashMap.filter
          ( \ii -> case ii ^. inductiveConstructors of
              BuiltinTag _ : _ -> False
-              UserTag _ _ : _ -> True
+              UserTag {} : _ -> True
              [] -> True
          )

--- a/src/Juvix/Compiler/Asm/Pretty/Options.hs
+++ b/src/Juvix/Compiler/Asm/Pretty/Options.hs
@ -2,7 +2,6 @@ module Juvix.Compiler.Asm.Pretty.Options where

 import Juvix.Compiler.Asm.Data.InfoTable
 import Juvix.Compiler.Core.Pretty.Options qualified as Core
-import Juvix.Prelude

 newtype Options = Options
  { _optInfoTable :: InfoTable
--- a/src/Juvix/Compiler/Asm/Transformation.hs
+++ b/src/Juvix/Compiler/Asm/Transformation.hs
@ -4,6 +4,7 @@ module Juvix.Compiler.Asm.Transformation
    module Juvix.Compiler.Asm.Transformation.Validate,
    module Juvix.Compiler.Asm.Transformation.Apply,
    module Juvix.Compiler.Asm.Transformation.FilterUnreachable,
+    module Juvix.Compiler.Asm.Transformation.TempHeight,
  )
 where

@ -11,4 +12,5 @@ import Juvix.Compiler.Asm.Transformation.Apply
 import Juvix.Compiler.Asm.Transformation.FilterUnreachable
 import Juvix.Compiler.Asm.Transformation.Prealloc
 import Juvix.Compiler.Asm.Transformation.StackUsage
+import Juvix.Compiler.Asm.Transformation.TempHeight
 import Juvix.Compiler.Asm.Transformation.Validate
--- a/src/Juvix/Compiler/Asm/Transformation/FilterUnreachable.hs
+++ b/src/Juvix/Compiler/Asm/Transformation/FilterUnreachable.hs
@ -4,7 +4,6 @@ import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Asm.Data.CallGraph
 import Juvix.Compiler.Asm.Data.InfoTable
 import Juvix.Compiler.Asm.Error
-import Juvix.Compiler.Asm.Language

 filterUnreachable :: (Member (Error AsmError) r) => InfoTable -> Sem r InfoTable
 filterUnreachable tab = do
--- a/src/Juvix/Compiler/Asm/Transformation/TempHeight.hs
+++ b/src/Juvix/Compiler/Asm/Transformation/TempHeight.hs
@ -0,0 +1,75 @@
+module Juvix.Compiler.Asm.Transformation.TempHeight where
+
+import Juvix.Compiler.Asm.Transformation.Base
+
+computeFunctionTempHeight ::
+  (Member (Error AsmError) r) =>
+  InfoTable ->
+  FunctionInfo ->
+  Sem r FunctionInfo
+computeFunctionTempHeight tab fi = do
+  ps :: [Command] <- recurseS sig (fi ^. functionCode)
+  return (set functionCode ps fi)
+  where
+    sig :: RecursorSig StackInfo r Command
+    sig =
+      RecursorSig
+        { _recursorInfoTable = tab,
+          _recurseInstr = goInstr,
+          _recurseBranch = goBranch,
+          _recurseCase = goCase,
+          _recurseSave = goSave
+        }
+
+    goInstr :: StackInfo -> CmdInstr -> Sem r Command
+    goInstr si cmd@(CmdInstr _ instr) = case instr of
+      Push (Ref (DRef (TempRef r))) ->
+        let h = si ^. stackInfoTempStackHeight
+            r' = set refTempTempHeight (Just h) r
+            instr' = Push (Ref (DRef (TempRef r')))
+         in return (Instr (set cmdInstrInstruction instr' cmd))
+      Push (Ref (ConstrRef field@Field {_fieldRef = TempRef r})) ->
+        let h = si ^. stackInfoTempStackHeight
+            r' = set refTempTempHeight (Just h) r
+            instr' =
+              Push
+                ( Ref
+                    ( ConstrRef
+                        field
+                          { _fieldRef = TempRef r'
+                          }
+                    )
+                )
+         in return (Instr (set cmdInstrInstruction instr' cmd))
+      _ -> return (Instr cmd)
+
+    goCase :: StackInfo -> CmdCase -> [Code] -> Maybe Code -> Sem r Command
+    goCase _ cmd brs mdef =
+      return
+        ( Case
+            cmd
+              { _cmdCaseBranches = branches',
+                _cmdCaseDefault = mdef
+              }
+        )
+      where
+        branches' :: [CaseBranch]
+        branches' =
+          [ set caseBranchCode newCode oldBr
+            | (oldBr, newCode) <- zipExact (cmd ^. cmdCaseBranches) brs
+          ]
+
+    goBranch :: StackInfo -> CmdBranch -> Code -> Code -> Sem r Command
+    goBranch _ cmd t f =
+      return
+        ( Branch
+            cmd
+              { _cmdBranchTrue = t,
+                _cmdBranchFalse = f
+              }
+        )
+    goSave :: StackInfo -> CmdSave -> Code -> Sem r Command
+    goSave _ cmd code = return (Save (set cmdSaveCode code cmd))
+
+computeTempHeight :: (Member (Error AsmError) r) => InfoTable -> Sem r InfoTable
+computeTempHeight tab = liftFunctionTransformation (computeFunctionTempHeight tab) tab
--- a/src/Juvix/Compiler/Asm/Translation/FromCore.hs
+++ b/src/Juvix/Compiler/Asm/Translation/FromCore.hs
@ -5,7 +5,6 @@ import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Asm.Data.InfoTable
 import Juvix.Compiler.Asm.Extra.Base
 import Juvix.Compiler.Asm.Extra.Type
-import Juvix.Compiler.Asm.Language
 import Juvix.Compiler.Core.Data.BinderList qualified as BL
 import Juvix.Compiler.Core.Data.Stripped.InfoTable qualified as Core
 import Juvix.Compiler.Core.Language.Stripped qualified as Core
@ -191,7 +190,7 @@ genCode infoTable fi =
            CmdSave
              { _cmdSaveInfo = emptyInfo,
                _cmdSaveIsTail = isTail,
-                _cmdSaveCode = DL.toList $ go isTail (tempSize + 1) (BL.cons (Ref (DRef (TempRef nameRef))) refs) _letBody,
+                _cmdSaveCode = DL.toList $ go isTail (tempSize + 1) (BL.cons (Ref (DRef (mkTempRef nameRef))) refs) _letBody,
                _cmdSaveName = Just name
              }
        )
@ -249,7 +248,7 @@ genCode infoTable fi =
                          (tempSize + 1)
                          ( BL.prepend
                              ( map
-                                  (Ref . ConstrRef . Field Nothing tag (TempRef (OffsetRef tempSize Nothing)))
+                                  (Ref . ConstrRef . Field Nothing tag (mkTempRef (OffsetRef tempSize Nothing)))
                                  (reverse [0 .. bindersNum - 1])
                              )
                              refs
--- a/src/Juvix/Compiler/Asm/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Asm/Translation/FromSource.hs
@ -12,7 +12,6 @@ import Juvix.Compiler.Asm.Data.InfoTable
 import Juvix.Compiler.Asm.Data.InfoTableBuilder
 import Juvix.Compiler.Asm.Extra.Base
 import Juvix.Compiler.Asm.Extra.Type
-import Juvix.Compiler.Asm.Language
 import Juvix.Compiler.Asm.Translation.FromSource.Lexer
 import Juvix.Parser.Error
 import Text.Megaparsec qualified as P
@ -384,7 +383,7 @@ parseSave loc isTail = do
  mn <- optional identifier
  tmpNum <- lift get
  let updateNames :: LocalNameMap -> LocalNameMap
-      updateNames mp = maybe mp (\n -> HashMap.insert n (TempRef (OffsetRef tmpNum (Just n))) mp) mn
+      updateNames mp = maybe mp (\n -> HashMap.insert n (mkTempRef (OffsetRef tmpNum (Just n))) mp) mn
  c <- braces (localS @Index (+ 1) $ localS updateNames parseCode)
  return $
    Save
@ -445,7 +444,7 @@ tempRef :: ParsecS r DirectRef
 tempRef = do
  kw kwTmp
  (off, _) <- brackets integer
-  return $ TempRef (OffsetRef (fromInteger off) Nothing)
+  return $ mkTempRef (OffsetRef (fromInteger off) Nothing)

 namedRef :: (Member (State LocalNameMap) r) => ParsecS r DirectRef
 namedRef = do
@ -530,7 +529,9 @@ instrCall = do
 parseCallType ::
  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
  ParsecS r CallType
-parseCallType = (kw kwDollar $> CallClosure) <|> (CallFun <$> funSymbol)
+parseCallType =
+  kw kwDollar $> CallClosure
+    <|> CallFun <$> funSymbol

 instrCallClosures :: ParsecS r InstrCallClosures
 instrCallClosures = do
--- a/src/Juvix/Compiler/Backend.hs
+++ b/src/Juvix/Compiler/Backend.hs
@ -10,6 +10,7 @@ data Target
  | TargetVampIR
  | TargetCore
  | TargetAsm
+  | TargetNockma
  deriving stock (Data, Eq, Show)

 data Limits = Limits
@ -72,6 +73,8 @@ getLimits tgt debug = case tgt of
    defaultLimits
  TargetAsm ->
    defaultLimits
+  TargetNockma ->
+    defaultLimits

 defaultLimits :: Limits
 defaultLimits =
--- a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
+++ b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
@ -102,7 +102,7 @@ runInfoTableBuilder' st =
      FreshTag -> do
        s <- get
        modify' (over builderStateNextTagId (+ 1))
-        return (UserTag (s ^. builderStateModule . moduleId) (s ^. builderStateNextTagId))
+        return (UserTag (TagUser (s ^. builderStateModule . moduleId) (s ^. builderStateNextTagId)))
      RegisterIdent idt ii -> do
        let sym = ii ^. identifierSymbol
            identKind = IdentFun (ii ^. identifierSymbol)
--- a/src/Juvix/Compiler/Core/Language/Base.hs
+++ b/src/Juvix/Compiler/Core/Language/Base.hs
@ -34,16 +34,29 @@ instance Pretty Symbol where
 instance Show Symbol where
  show = show . pretty

+defaultSymbol :: Word -> Symbol
+defaultSymbol = Symbol defaultModuleId
+
 uniqueName :: Text -> Symbol -> Text
 uniqueName txt sym = txt <> "_" <> show sym

+data TagUser = TagUser
+  { _tagUserModuleId :: ModuleId,
+    _tagUserWord :: Word
+  }
+  deriving stock (Eq, Generic, Ord, Show)
+
+instance Hashable TagUser
+
+instance Serialize TagUser
+
 -- | Tag of a constructor, uniquely identifying it. Tag values are consecutive
 -- and separate from symbol IDs. We might need fixed special tags in Core for
 -- common "builtin" constructors, e.g., unit, nat, so that the code generator
 -- can treat them specially.
 data Tag
  = BuiltinTag BuiltinDataTag
-  | UserTag ModuleId Word
+  | UserTag TagUser
  deriving stock (Eq, Generic, Ord, Show)

 instance Hashable Tag
@ -63,7 +76,7 @@ type Level = Int

 getUserTagId :: Tag -> Maybe Word
 getUserTagId = \case
-  UserTag _ u -> Just u
+  UserTag TagUser {..} -> Just _tagUserWord
  BuiltinTag {} -> Nothing

 -- | The first argument `bl` is the current binder level (the number of binders
@ -77,3 +90,4 @@ getBinderIndex :: Level -> Level -> Index
 getBinderIndex bl lvl = bl - lvl - 1

 makeLenses ''Symbol
+makeLenses ''TagUser
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@ -59,7 +59,7 @@ instance PrettyCode BuiltinDataTag where
 instance PrettyCode Tag where
  ppCode = \case
    BuiltinTag tag -> ppCode tag
-    UserTag mid tag -> return $ kwUnnamedConstr <> pretty tag <> "@" <> pretty mid
+    UserTag (TagUser mid tag) -> return $ kwUnnamedConstr <> pretty tag <> "@" <> pretty mid

 instance PrettyCode Primitive where
  ppCode = \case
--- a/src/Juvix/Compiler/Nockma/Evaluator.hs
+++ b/src/Juvix/Compiler/Nockma/Evaluator.hs
@ -6,6 +6,7 @@ where

 import Juvix.Compiler.Nockma.Evaluator.Error
 import Juvix.Compiler.Nockma.Language
+import Juvix.Compiler.Nockma.Pretty
 import Juvix.Prelude hiding (Atom, Path)

 asAtom :: (Member (Error NockEvalError) r) => Term a -> Sem r (Atom a)
@ -13,9 +14,9 @@ asAtom = \case
  TermAtom a -> return a
  TermCell {} -> throw ExpectedAtom

-asCell :: (Member (Error NockEvalError) r) => Term a -> Sem r (Cell a)
-asCell = \case
-  TermAtom {} -> throw ExpectedCell
+asCell :: (Member (Error NockEvalError) r) => Text -> Term a -> Sem r (Cell a)
+asCell msg = \case
+  TermAtom {} -> throw (ExpectedCell msg)
  TermCell c -> return c

 asBool :: (Member (Error NockEvalError) r, NockNatural a) => Term a -> Sem r Bool
@ -44,14 +45,14 @@ 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 @NockEvalError (error "")
    Just t -> return t

 setSubTerm :: (Member (Error NockEvalError) r) => Term a -> Path -> Term a -> Sem r (Term a)
 setSubTerm term pos repTerm =
  let (old, new) = setAndRemember (subTermT' pos) repTerm term
   in if
-          | isNothing (getFirst old) -> throw InvalidPath
+          | isNothing (getFirst old) -> throw @NockEvalError (error "")
          | otherwise -> return new

 parseCell :: forall r a. (Members '[Error NockEvalError, Error (ErrNockNatural a)] r, NockNatural a) => Cell a -> Sem r (ParsedCell a)
@ -83,19 +84,20 @@ programAssignments mprog =
 -- | The stack provided in the replExpression has priority
 evalRepl ::
  forall r a.
-  (Members '[Error NockEvalError, Error (ErrNockNatural a)] r, NockNatural a) =>
+  (PrettyCode a, Members '[Error NockEvalError, Error (ErrNockNatural a)] r, NockNatural a) =>
+  (Term a -> Sem r ()) ->
  Maybe (Program a) ->
  Maybe (Term a) ->
  ReplExpression a ->
  Sem r (Term a)
-evalRepl mprog defaultStack expr = do
+evalRepl handleTrace mprog defaultStack expr = do
  (mstack, t) <- case expr of
    ReplExpressionTerm tm -> return (defaultStack, tm)
    ReplExpressionWithStack w -> do
      t' <- fromReplTerm namedTerms (w ^. withStackStack)
      return (Just t', w ^. withStackTerm)
  stack <- maybe errNoStack return mstack
-  fromReplTerm namedTerms t >>= eval stack
+  fromReplTerm namedTerms t >>= runOutputSem @(Term a) handleTrace . eval stack
  where
    errNoStack :: Sem r x
    errNoStack = throw NoStack
@ -103,14 +105,9 @@ evalRepl mprog defaultStack expr = do
    namedTerms :: HashMap Text (Term a)
    namedTerms = programAssignments mprog

-eval ::
-  forall r a.
-  (Members '[Error NockEvalError, Error (ErrNockNatural a)] r, NockNatural a) =>
-  Term a ->
-  Term a ->
-  Sem r (Term a)
+eval :: forall r a. (PrettyCode a, Members '[Output (Term a), Error NockEvalError, Error (ErrNockNatural a)] r, NockNatural a) => Term a -> Term a -> Sem r (Term a)
 eval stack = \case
-  TermAtom {} -> throw ExpectedCell
+  TermAtom a -> throw (ExpectedCell ("eval " <> ppTrace a))
  TermCell c -> do
    pc <- parseCell c
    case pc of
@ -137,6 +134,7 @@ eval stack = \case
      OpCall -> goOpCall
      OpReplace -> goOpReplace
      OpHint -> goOpHint
+      OpTrace -> goOpTrace
      where
        goOpAddress :: Sem r (Term a)
        goOpAddress = asPath (c ^. operatorCellTerm) >>= subTerm stack
@ -149,41 +147,47 @@ eval stack = \case
          TermCell {} -> nockTrue
          TermAtom {} -> nockFalse

+        goOpTrace :: Sem r (Term a)
+        goOpTrace = do
+          Cell tr a <- asCell "OpTrace" (c ^. operatorCellTerm)
+          tr' <- eval stack tr
+          output tr'
+          eval stack a
+
        goOpHint :: Sem r (Term a)
        goOpHint = do
          -- Ignore the hint and evaluate
-          h <- asCell (c ^. operatorCellTerm)
+          h <- asCell "OpHint" (c ^. operatorCellTerm)
          eval stack (h ^. cellRight)

        goOpPush :: Sem r (Term a)
        goOpPush = do
-          cellTerm <- asCell (c ^. operatorCellTerm)
+          cellTerm <- asCell "OpPush" (c ^. operatorCellTerm)
          l <- eval stack (cellTerm ^. cellLeft)
          let s = TermCell Cell {_cellLeft = l, _cellRight = stack}
          eval s (cellTerm ^. cellRight)

        goOpReplace :: Sem r (Term a)
        goOpReplace = do
-          cellTerm <- asCell (c ^. operatorCellTerm)
-          rt1 <- asCell (cellTerm ^. cellLeft)
-          r <- asPath (rt1 ^. cellLeft)
-          let t1 = rt1 ^. cellRight
+          Cell rot1 t2 <- asCell "OpReplace 1" (c ^. operatorCellTerm)
+          Cell ro t1 <- asCell "OpReplace 2" rot1
+          r <- asPath ro
          t1' <- eval stack t1
-          t2' <- eval stack (cellTerm ^. cellRight)
+          t2' <- eval stack t2
          setSubTerm t2' r t1'

        goOpApply :: Sem r (Term a)
        goOpApply = do
-          cellTerm <- asCell (c ^. operatorCellTerm)
+          cellTerm <- asCell "OpApply" (c ^. operatorCellTerm)
          t1' <- eval stack (cellTerm ^. cellLeft)
          t2' <- eval stack (cellTerm ^. cellRight)
          eval t1' t2'

        goOpIf :: Sem r (Term a)
        goOpIf = do
-          cellTerm <- asCell (c ^. operatorCellTerm)
+          cellTerm <- asCell "OpIf 1" (c ^. operatorCellTerm)
          let t0 = cellTerm ^. cellLeft
-          Cell t1 t2 <- asCell (cellTerm ^. cellRight)
+          Cell t1 t2 <- asCell "OpIf 2" (cellTerm ^. cellRight)
          cond <- eval stack t0 >>= asBool
          if
              | cond -> eval stack t1
@ -194,7 +198,7 @@ eval stack = \case

        goOpEq :: Sem r (Term a)
        goOpEq = do
-          cellTerm <- asCell (c ^. operatorCellTerm)
+          cellTerm <- asCell "OpEq" (c ^. operatorCellTerm)
          l <- eval stack (cellTerm ^. cellLeft)
          r <- eval stack (cellTerm ^. cellRight)
          return . TermAtom $
@ -204,13 +208,13 @@ eval stack = \case

        goOpCall :: Sem r (Term a)
        goOpCall = do
-          cellTerm <- asCell (c ^. operatorCellTerm)
+          cellTerm <- asCell "OpCall" (c ^. operatorCellTerm)
          r <- asPath (cellTerm ^. cellLeft)
          t' <- eval stack (cellTerm ^. cellRight)
          subTerm t' r >>= eval t'

        goOpSequence :: Sem r (Term a)
        goOpSequence = do
-          cellTerm <- asCell (c ^. operatorCellTerm)
+          cellTerm <- asCell "OpSequence" (c ^. operatorCellTerm)
          t1' <- eval stack (cellTerm ^. cellLeft)
          eval t1' (cellTerm ^. cellRight)
--- a/src/Juvix/Compiler/Nockma/Evaluator/Error.hs
+++ b/src/Juvix/Compiler/Nockma/Evaluator/Error.hs
@ -4,9 +4,9 @@ import Juvix.Prelude hiding (Atom)
 import Juvix.Prelude.Pretty

 data NockEvalError
-  = InvalidPath
+  = InvalidPath Text
  | ExpectedAtom
-  | ExpectedCell
+  | ExpectedCell Text
  | NoStack
  | AssignmentNotFound Text
  deriving stock (Show)
--- a/src/Juvix/Compiler/Nockma/Language.hs
+++ b/src/Juvix/Compiler/Nockma/Language.hs
@ -1,7 +1,12 @@
-module Juvix.Compiler.Nockma.Language where
+module Juvix.Compiler.Nockma.Language
+  ( module Juvix.Compiler.Nockma.Language,
+    module Juvix.Compiler.Core.Language.Base,
+  )
+where

 import Data.HashMap.Strict qualified as HashMap
 import GHC.Base (Type)
+import Juvix.Compiler.Core.Language.Base (Symbol)
 import Juvix.Prelude hiding (Atom, Path)
 import Juvix.Prelude.Pretty

@ -72,6 +77,7 @@ data NockOp
  | OpCall
  | OpReplace
  | OpHint
+  | OpTrace
  deriving stock (Bounded, Enum, Eq, Generic)

 instance Hashable NockOp
@ -90,6 +96,7 @@ instance Pretty NockOp where
    OpCall -> "call"
    OpReplace -> "replace"
    OpHint -> "hint"
+    OpTrace -> "trace"

 atomOps :: HashMap Text NockOp
 atomOps = HashMap.fromList [(prettyText op, op) | op <- allElements]
@ -112,6 +119,14 @@ newtype EncodedPath = EncodedPath
  { _encodedPath :: Natural
  }

+-- | appends n R
+encodedPathAppendRightN :: Natural -> EncodedPath -> EncodedPath
+encodedPathAppendRightN n (EncodedPath p) = EncodedPath (f p)
+  where
+    -- equivalent to applying 2 * x + 1, n times
+    f :: Natural -> Natural
+    f x = (2 ^ n) * (x + 1) - 1
+
 data Direction
  = L
  | R
@ -154,6 +169,7 @@ serializeOp = \case
  OpCall -> 9
  OpReplace -> 10
  OpHint -> 11
+  OpTrace -> 100

 decodePath :: forall r. (Member Fail r) => EncodedPath -> Sem r Path
 decodePath ep = execOutputList (go (ep ^. encodedPath))
@ -212,6 +228,17 @@ data NockNaturalNaturalError
  | NaturalInvalidOp (Atom Natural)
  deriving stock (Show)

+nockTrueLiteral :: Term Natural
+nockTrueLiteral = OpQuote # (TermAtom (nockTrue @Natural))
+
+nockFalseLiteral :: Term Natural
+nockFalseLiteral = OpQuote # (TermAtom (nockFalse @Natural))
+
+nockBoolLiteral :: Bool -> Term Natural
+nockBoolLiteral b
+  | b = nockTrueLiteral
+  | otherwise = nockFalseLiteral
+
 instance NockNatural Natural where
  type ErrNockNatural Natural = NockNaturalNaturalError
  nockNatural a = return (a ^. atom)
@ -257,3 +284,9 @@ infixr 5 #

 (#) :: (IsNock x, IsNock y) => x -> y -> Term Natural
 a # b = TermCell (Cell (toNock a) (toNock b))
+
+instance Semigroup EncodedPath where
+  a <> b = encodePath (decodePath' a <> decodePath' b)
+
+instance Monoid EncodedPath where
+  mempty = encodePath []
--- a/src/Juvix/Compiler/Nockma/Pretty.hs
+++ b/src/Juvix/Compiler/Nockma/Pretty.hs
@ -24,5 +24,11 @@ ppTrace :: (PrettyCode c) => c -> Text
 ppTrace =
  Ansi.renderStrict . reAnnotateS stylize . layoutPretty defaultLayoutOptions . doc defaultOptions

+ppSerialize :: (PrettyCode c) => c -> Text
+ppSerialize = ppPrintOpts serializeOptions
+
 ppPrint :: (PrettyCode c) => c -> Text
-ppPrint = renderStrict . toTextStream . ppOutDefault
+ppPrint = ppPrintOpts defaultOptions
+
+ppPrintOpts :: (PrettyCode c) => Options -> c -> Text
+ppPrintOpts opts = renderStrict . toTextStream . ppOut opts
--- a/src/Juvix/Compiler/Nockma/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Nockma/Pretty/Base.hs
@ -26,6 +26,7 @@ instance (PrettyCode a, NockNatural a) => PrettyCode (Atom a) where
  ppCode atm@(Atom k h) = runFailDefaultM (annotate (AnnKind KNameFunction) <$> ppCode k)
    . failFromError @(ErrNockNatural a)
    $ do
+      whenM (asks (^. optIgnoreHints)) fail
      h' <- failMaybe (h ^. unIrrelevant)
      case h' of
        AtomHintOp -> nockOp atm >>= ppCode
@ -77,3 +78,8 @@ instance (PrettyCode a, NockNatural a) => PrettyCode (Term a) where
  ppCode = \case
    TermAtom t -> ppCode t
    TermCell c -> ppCode c
+
+instance (PrettyCode a, NockNatural a) => PrettyCode [Term a] where
+  ppCode ts = do
+    ts' <- mapM ppCode ts
+    return (braces (commaSep ts'))
--- a/src/Juvix/Compiler/Nockma/Pretty/Options.hs
+++ b/src/Juvix/Compiler/Nockma/Pretty/Options.hs
@ -10,17 +10,27 @@ data PrettyMode
 defaultOptions :: Options
 defaultOptions =
  Options
-    { _optPrettyMode = MinimizeDelimiters
+    { _optPrettyMode = MinimizeDelimiters,
+      _optIgnoreHints = False
    }

-newtype Options = Options
-  { _optPrettyMode :: PrettyMode
+data Options = Options
+  { _optPrettyMode :: PrettyMode,
+    _optIgnoreHints :: Bool
  }

+serializeOptions :: Options
+serializeOptions =
+  Options
+    { _optPrettyMode = MinimizeDelimiters,
+      _optIgnoreHints = True
+    }
+
 traceOptions :: Options
 traceOptions =
  Options
-    { _optPrettyMode = AllDelimiters
+    { _optPrettyMode = MinimizeDelimiters,
+      _optIgnoreHints = False
    }

 makeLenses ''Options
--- a/src/Juvix/Compiler/Nockma/Translation/FromAsm.hs
+++ b/src/Juvix/Compiler/Nockma/Translation/FromAsm.hs
--- a/src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs
+++ b/src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs
@ -7,23 +7,22 @@ import Juvix.Compiler.Nockma.Language qualified as N
 import Juvix.Parser.Error
 import Juvix.Prelude hiding (Atom, many, some)
 import Juvix.Prelude.Parsing hiding (runParser)
-import Juvix.Prelude.Pretty
 import Text.Megaparsec qualified as P
 import Text.Megaparsec.Char.Lexer qualified as L

 type Parser = Parsec Void Text

-fromMegaParsecError :: Either MegaparsecError a -> a
-fromMegaParsecError = \case
-  Left e -> error (prettyText e)
-  Right a -> a
-
 parseText :: Text -> Either MegaparsecError (N.Term Natural)
 parseText = runParser ""

 parseReplText :: Text -> Either MegaparsecError (N.ReplTerm Natural)
 parseReplText = runParserFor replTerm ""

+parseTermFile :: (MonadIO m) => FilePath -> m (Either MegaparsecError (N.Term Natural))
+parseTermFile fp = do
+  txt <- readFile fp
+  return (runParser fp txt)
+
 parseProgramFile :: (MonadIO m) => FilePath -> m (Either MegaparsecError (N.Program Natural))
 parseProgramFile fp = do
  txt <- readFile fp
--- a/src/Juvix/Compiler/Nockma/Translation/FromSource/QQ.hs
+++ b/src/Juvix/Compiler/Nockma/Translation/FromSource/QQ.hs
@ -7,6 +7,7 @@ where
 import Control.Monad.Fail qualified as M
 import Juvix.Compiler.Nockma.Language
 import Juvix.Compiler.Nockma.Translation.FromSource.Base
+import Juvix.Parser.Error (fromMegaParsecError)
 import Juvix.Prelude
 import Language.Haskell.TH.Quote
 import Language.Haskell.TH.Syntax
--- a/src/Juvix/Compiler/Pipeline.hs
+++ b/src/Juvix/Compiler/Pipeline.hs
@ -24,6 +24,8 @@ import Juvix.Compiler.Core qualified as Core
 import Juvix.Compiler.Core.Translation.Stripped.FromCore qualified as Stripped
 import Juvix.Compiler.Internal qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
+import Juvix.Compiler.Nockma.Language qualified as Nockma
+import Juvix.Compiler.Nockma.Translation.FromAsm qualified as Nockma
 import Juvix.Compiler.Pipeline.Artifacts
 import Juvix.Compiler.Pipeline.EntryPoint
 import Juvix.Compiler.Pipeline.Loader.PathResolver.Base
@ -148,6 +150,9 @@ storedCoreToVampIR' = Core.toVampIR' >=> return . VampIR.fromCore' False . Core.
 coreToAsm :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r Asm.InfoTable
 coreToAsm = Core.toStored >=> storedCoreToAsm

+coreToNockma :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r (Nockma.Cell Natural)
+coreToNockma = coreToAsm >=> asmToNockma
+
 coreToMiniC :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r C.MiniCResult
 coreToMiniC = coreToAsm >=> asmToMiniC

@ -164,6 +169,9 @@ coreToVampIR' = Core.toStored' >=> storedCoreToVampIR'
 -- Other workflows
 --------------------------------------------------------------------------------

+asmToNockma :: (Members '[Error JuvixError, Reader EntryPoint] r) => Asm.InfoTable -> Sem r (Nockma.Cell Natural)
+asmToNockma = Asm.toNockma >=> mapReader Nockma.fromEntryPoint . Nockma.fromAsmTable
+
 asmToMiniC :: (Members '[Error JuvixError, Reader EntryPoint] r) => Asm.InfoTable -> Sem r C.MiniCResult
 asmToMiniC = Asm.toReg >=> regToMiniC . Reg.fromAsm

@ -172,6 +180,9 @@ regToMiniC tab = do
  e <- ask
  return $ C.fromReg (Backend.getLimits (e ^. entryPointTarget) (e ^. entryPointDebug)) tab

+asmToNockma' :: (Members '[Error JuvixError, Reader Asm.Options, Reader Nockma.CompilerOptions] r) => Asm.InfoTable -> Sem r (Nockma.Cell Natural)
+asmToNockma' = mapError (JuvixError @Asm.AsmError) . Asm.toNockma' >=> Nockma.fromAsmTable
+
 asmToMiniC' :: (Members '[Error JuvixError, Reader Asm.Options] r) => Asm.InfoTable -> Sem r C.MiniCResult
 asmToMiniC' = mapError (JuvixError @Asm.AsmError) . Asm.toReg' >=> regToMiniC' . Reg.fromAsm

--- a/src/Juvix/Compiler/Reg/Translation/FromAsm.hs
+++ b/src/Juvix/Compiler/Reg/Translation/FromAsm.hs
@ -4,7 +4,6 @@ import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Asm.Data.InfoTable qualified as Asm
 import Juvix.Compiler.Asm.Error qualified as Asm
 import Juvix.Compiler.Asm.Extra.Recursors qualified as Asm
-import Juvix.Compiler.Asm.Language qualified as Asm
 import Juvix.Compiler.Reg.Data.InfoTable
 import Juvix.Compiler.Reg.Language

@ -174,7 +173,7 @@ fromAsmInstr funInfo tab si Asm.CmdInstr {..} =
    mkVar = \case
      Asm.StackRef -> VarRef VarGroupStack n
      Asm.ArgRef Asm.OffsetRef {..} -> VarRef VarGroupArgs _offsetRefOffset
-      Asm.TempRef Asm.OffsetRef {..} -> VarRef VarGroupTemp _offsetRefOffset
+      Asm.TempRef Asm.RefTemp {..} -> VarRef VarGroupTemp (_refTempOffsetRef ^. Asm.offsetRefOffset)

    mkPrealloc :: Asm.InstrPrealloc -> Instruction
    mkPrealloc Asm.InstrPrealloc {..} =
--- a/src/Juvix/Data/CodeAnn.hs
+++ b/src/Juvix/Data/CodeAnn.hs
@ -282,3 +282,6 @@ bracesIndent = braces . blockIndent

 blockIndent :: Doc Ann -> Doc Ann
 blockIndent d = hardline <> indent' d <> line
+
+commaSep :: (Foldable f) => f (Doc Ann) -> Doc Ann
+commaSep ts = mconcat (intersperse (delimiter "," <> " ") (toList ts))
--- a/src/Juvix/Data/FileExt.hs
+++ b/src/Juvix/Data/FileExt.hs
@ -23,7 +23,7 @@ data FileExt
  | FileExtMarkdown
  | FileExtHtml
  | FileExtCss
-  | FileExtNock
+  | FileExtNockma
  deriving stock (Eq)

 juvixFileExt :: (IsString a) => a
@ -71,8 +71,8 @@ cFileExt = ".c"
 cssFileExt :: (IsString a) => a
 cssFileExt = ".css"

-nockFileExt :: (IsString a) => a
-nockFileExt = ".nock"
+nockmaFileExt :: (IsString a) => a
+nockmaFileExt = ".nockma"

 fileExtToText :: FileExt -> Text
 fileExtToText = \case
@ -91,7 +91,7 @@ fileExtToText = \case
  FileExtMarkdown -> markdownFileExt
  FileExtHtml -> htmlFileExt
  FileExtCss -> cssFileExt
-  FileExtNock -> nockFileExt
+  FileExtNockma -> nockmaFileExt

 toMetavar :: FileExt -> String
 toMetavar = \case
@ -110,7 +110,7 @@ toMetavar = \case
  FileExtMarkdown -> "MARKDOWN_FILE"
  FileExtHtml -> "HTML_FILE"
  FileExtCss -> "CSS_FILE"
-  FileExtNock -> "NOCK_FILE"
+  FileExtNockma -> "NOCKMA_FILE"

 instance Show FileExt where
  show = Text.unpack . fileExtToText
@ -165,8 +165,8 @@ isHtmlFile = (== Just htmlFileExt) . fileExtension
 isCssFile :: Path b File -> Bool
 isCssFile = (== Just cssFileExt) . fileExtension

-isNockFile :: Path b File -> Bool
-isNockFile = (== Just nockFileExt) . fileExtension
+isNockmaFile :: Path b File -> Bool
+isNockmaFile = (== Just nockmaFileExt) . fileExtension

 toFileExt :: Path b File -> Maybe FileExt
 toFileExt p
@ -185,7 +185,7 @@ toFileExt p
  | isMarkdownFile p = Just FileExtMarkdown
  | isHtmlFile p = Just FileExtHtml
  | isCssFile p = Just FileExtCss
-  | isNockFile p = Just FileExtNock
+  | isNockmaFile p = Just FileExtNockma
  | otherwise = Nothing

 fileExtension' :: Path b File -> String
--- a/src/Juvix/Parser/Error.hs
+++ b/src/Juvix/Parser/Error.hs
@ -64,6 +64,12 @@ instance ToGenericError MegaparsecError where
    where
      i = getLoc e

+-- | Use only for debugging
+fromMegaParsecError :: Either MegaparsecError a -> a
+fromMegaParsecError = \case
+  Left e -> error (prettyText e)
+  Right a -> a
+
 newtype CommonmarkError = CommonmarkError
  { _commonMarkError :: MK.ParseError
  }
--- a/src/Juvix/Prelude/Base.hs
+++ b/src/Juvix/Prelude/Base.hs
@ -71,6 +71,7 @@ module Juvix.Prelude.Base
    module System.IO,
    module Text.Show,
    module Control.Monad.Catch,
+    module Control.Monad.Zip,
    Data,
    Text,
    pack,
@ -89,10 +90,11 @@ where

 import Control.Applicative
 import Control.Monad.Catch (MonadMask, MonadThrow, throwM)
-import Control.Monad.Extra hiding (fail, mconcatMapM, whileJustM)
+import Control.Monad.Extra hiding (fail, forM, mconcatMapM, whileJustM)
 import Control.Monad.Extra qualified as Monad
 import Control.Monad.Fix
 import Control.Monad.IO.Class (MonadIO (..))
+import Control.Monad.Zip
 import Data.Bifunctor hiding (first, second)
 import Data.Bitraversable
 import Data.Bool
@ -102,7 +104,7 @@ import Data.Char qualified as Char
 import Data.Data
 import Data.Either.Extra
 import Data.Eq
-import Data.Foldable hiding (minimum, minimumBy)
+import Data.Foldable hiding (foldr1, minimum, minimumBy)
 import Data.Function
 import Data.Functor
 import Data.Graph (Graph, SCC (..), Vertex, stronglyConnComp)
@ -115,7 +117,7 @@ import Data.Int
 import Data.IntMap.Strict (IntMap)
 import Data.IntMap.Strict qualified as IntMap
 import Data.IntSet (IntSet)
-import Data.List.Extra hiding (allSame, groupSortOn, head, last, mconcatMap)
+import Data.List.Extra hiding (allSame, foldr1, groupSortOn, head, last, mconcatMap, replicate)
 import Data.List.Extra qualified as List
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.List.NonEmpty.Extra
@ -127,7 +129,6 @@ import Data.List.NonEmpty.Extra
    maximumOn1,
    minimum1,
    minimumOn1,
-    nonEmpty,
    prependList,
    some1,
    (|:),
@ -142,6 +143,7 @@ import Data.Singletons hiding ((@@))
 import Data.Singletons.Sigma
 import Data.Singletons.TH (genSingletons, promoteOrdInstances, singOrdInstances)
 import Data.Stream (Stream)
+import Data.Stream qualified as Stream
 import Data.String
 import Data.Text (Text, pack, strip, unpack)
 import Data.Text qualified as Text
@ -280,12 +282,15 @@ allDifferent :: forall a. (Ord a) => [a] -> Bool
 allDifferent = null . findRepeated

 allSame :: forall t a. (Eq a, Foldable t) => t a -> Bool
-allSame t
-  | null t = True
-  | otherwise = all (== h) t
-  where
-    h :: a
-    h = foldr1 const t
+allSame t = case nonEmpty t of
+  Nothing -> True
+  Just (a :| as) -> all (== a) as
+
+nonEmpty :: (Foldable l) => l a -> Maybe (NonEmpty a)
+nonEmpty = NonEmpty.nonEmpty . toList
+
+foldr1 :: (a -> a -> a) -> NonEmpty a -> a
+foldr1 = List.foldr1

 sconcatMap :: (Semigroup c) => (a -> c) -> NonEmpty a -> c
 sconcatMap f = sconcat . fmap f
@ -297,9 +302,9 @@ mconcatMapM :: (Monad m, Monoid c, Foldable t) => (a -> m c) -> t a -> m c
 mconcatMapM f = Monad.mconcatMapM f . toList

 concatWith :: (Foldable t, Monoid a) => (a -> a -> a) -> t a -> a
-concatWith f ds
-  | null ds = mempty
-  | otherwise = foldr1 f ds
+concatWith f ds = case nonEmpty ds of
+  Nothing -> mempty
+  Just ds' -> foldr1 f ds'
 {-# INLINE concatWith #-}

 --------------------------------------------------------------------------------
@ -478,6 +483,9 @@ nubHashable = HashSet.toList . HashSet.fromList
 allElements :: (Bounded a, Enum a) => [a]
 allElements = [minBound .. maxBound]

+replicate :: (Integral n) => n -> a -> [a]
+replicate n a = List.replicate (fromIntegral n) a
+
 infixr 3 .&&.

 (.&&.) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
@ -568,3 +576,23 @@ indexedByHash getIx l = HashMap.fromList [(getIx i, i) | i <- toList l]

 hashMap :: (Foldable f, Hashable k) => f (k, v) -> HashMap k v
 hashMap = HashMap.fromList . toList
+
+runInputInfinite :: Stream i -> Sem (Input i ': r) a -> Sem r a
+runInputInfinite s =
+  evalState s
+    . reinterpret
+      ( \case
+          Input -> do
+            Stream.Cons i is <- get
+            put is
+            return i
+      )
+
+writeFileEnsureLn :: (MonadMask m, MonadIO m) => FilePath -> Text -> m ()
+writeFileEnsureLn p t =
+  let t' = case Text.unsnoc t of
+        Nothing -> t
+        Just (_, y) -> case y of
+          '\n' -> t
+          _ -> Text.snoc t '\n'
+   in writeFile p t'
--- a/src/Juvix/Prelude/Stream.hs
+++ b/src/Juvix/Prelude/Stream.hs
@ -3,6 +3,9 @@ module Juvix.Prelude.Stream where
 import Data.Stream qualified as Stream
 import Juvix.Prelude.Base

+allNaturals :: Stream Natural
+allNaturals = Stream.iterate succ 0
+
 allWords :: Stream Text
 allWords = pack . toList <$> allFiniteSequences ('a' :| ['b' .. 'z'])

@ -22,3 +25,6 @@ allFiniteSequences elems = build 0 []
          seq <- ofLength (n - 1)
          e <- elems
          return (pure e <> seq)
+
+runInputNaturals :: Sem (Input Natural ': r) a -> Sem r a
+runInputNaturals = runInputInfinite allNaturals
--- a/test/Asm/Run/Base.hs
+++ b/test/Asm/Run/Base.hs
@ -9,8 +9,23 @@ import Juvix.Compiler.Asm.Transformation.Validate
 import Juvix.Compiler.Asm.Translation.FromSource
 import Juvix.Data.PPOutput

+runAssertion :: Handle -> Symbol -> InfoTable -> IO ()
+runAssertion hout sym tab = do
+  r' <- doRun hout tab (lookupFunInfo tab sym)
+  case r' of
+    Left err -> do
+      hClose hout
+      assertFailure (show (pretty err))
+    Right value' -> do
+      case value' of
+        ValVoid -> return ()
+        _ -> hPutStrLn hout (ppPrint tab value')
+
 asmRunAssertion' :: InfoTable -> Path Abs File -> (String -> IO ()) -> Assertion
-asmRunAssertion' tab expectedFile step = do
+asmRunAssertion' = asmRunAssertionParam' runAssertion
+
+asmRunAssertionParam' :: (Handle -> Symbol -> InfoTable -> IO ()) -> InfoTable -> Path Abs File -> (String -> IO ()) -> Assertion
+asmRunAssertionParam' interpretFun tab expectedFile step = do
  step "Validate"
  case validate' tab of
    Just err -> assertFailure (show (pretty err))
@ -22,25 +37,20 @@ asmRunAssertion' tab expectedFile step = do
                let outputFile = dirPath <//> $(mkRelFile "out.out")
                hout <- openFile (toFilePath outputFile) WriteMode
                step "Interpret"
-                r' <- doRun hout tab (lookupFunInfo tab sym)
-                case r' of
-                  Left err -> do
-                    hClose hout
-                    assertFailure (show (pretty err))
-                  Right value' -> do
-                    case value' of
-                      ValVoid -> return ()
-                      _ -> hPutStrLn hout (ppPrint tab value')
-                    hClose hout
-                    actualOutput <- readFile (toFilePath outputFile)
-                    step "Compare expected and actual program output"
-                    expected <- readFile (toFilePath expectedFile)
-                    assertEqDiffText ("Check: RUN output = " <> toFilePath expectedFile) actualOutput expected
+                interpretFun hout sym tab
+                hClose hout
+                actualOutput <- readFile (toFilePath outputFile)
+                step "Compare expected and actual program output"
+                expected <- readFile (toFilePath expectedFile)
+                assertEqDiffText ("Check: RUN output = " <> toFilePath expectedFile) actualOutput expected
            )
        Nothing -> assertFailure "no 'main' function"

 asmRunAssertion :: Path Abs File -> Path Abs File -> (InfoTable -> Either AsmError InfoTable) -> (InfoTable -> Assertion) -> (String -> IO ()) -> Assertion
-asmRunAssertion mainFile expectedFile trans testTrans step = do
+asmRunAssertion = asmRunAssertionParam runAssertion
+
+asmRunAssertionParam :: (Handle -> Symbol -> InfoTable -> IO ()) -> Path Abs File -> Path Abs File -> (InfoTable -> Either AsmError InfoTable) -> (InfoTable -> Assertion) -> (String -> IO ()) -> Assertion
+asmRunAssertionParam interpretFun mainFile expectedFile trans testTrans step = do
  step "Parse"
  r <- parseFile mainFile
  case r of
@ -50,7 +60,7 @@ asmRunAssertion mainFile expectedFile trans testTrans step = do
        Left err -> assertFailure (show (pretty err))
        Right tab -> do
          testTrans tab
-          asmRunAssertion' tab expectedFile step
+          asmRunAssertionParam' interpretFun tab expectedFile step

 asmRunErrorAssertion :: Path Abs File -> (String -> IO ()) -> Assertion
 asmRunErrorAssertion mainFile step = do
--- a/test/Nockma.hs
+++ b/test/Nockma.hs
@ -1,8 +1,9 @@
 module Nockma where

 import Base
+import Nockma.Compile qualified as Compile
 import Nockma.Eval qualified as Eval
 import Nockma.Parse qualified as Parse

 allTests :: TestTree
-allTests = testGroup "Nockma tests" [Parse.allTests, Eval.allTests]
+allTests = testGroup "Nockma tests" [Parse.allTests, Eval.allTests, Compile.allTests]
--- a/test/Nockma/Compile.hs
+++ b/test/Nockma/Compile.hs
@ -0,0 +1,8 @@
+module Nockma.Compile where
+
+import Base
+import Nockma.Compile.Asm.Positive qualified as Asm
+import Nockma.Compile.Positive qualified as P
+
+allTests :: TestTree
+allTests = testGroup "Nockma compile" [P.allTests, Asm.allTests]
--- a/test/Nockma/Compile/Asm/Positive.hs
+++ b/test/Nockma/Compile/Asm/Positive.hs
@ -0,0 +1,86 @@
+module Nockma.Compile.Asm.Positive where
+
+import Asm.Run.Base
+import Asm.Run.Positive qualified as Asm
+import Base
+import Juvix.Compiler.Asm
+import Juvix.Compiler.Asm.Options qualified as Asm
+import Juvix.Compiler.Nockma.Language
+import Juvix.Compiler.Nockma.Pretty qualified as Nockma
+import Juvix.Compiler.Nockma.Translation.FromAsm
+import Juvix.Compiler.Nockma.Translation.FromAsm qualified as Nockma
+
+runNockmaAssertion :: Handle -> Symbol -> InfoTable -> IO ()
+runNockmaAssertion hout _main tab = do
+  Nockma.Cell nockSubject nockMain <-
+    runM
+      ( runReader
+          (Asm.makeOptions TargetNockma True)
+          $ runReader
+            (Nockma.CompilerOptions {_compilerOptionsEnableTrace = True})
+            (runErrorIO' @JuvixError (asmToNockma' tab))
+      )
+  res <- runM $ runOutputSem @(Term Natural) (embed . hPutStrLn hout . Nockma.ppPrint) (evalCompiledNock' nockSubject nockMain)
+  let ret = getReturn res
+  hPutStrLn hout (Nockma.ppPrint ret)
+  where
+    getReturn :: Term Natural -> Term Natural
+    getReturn res =
+      let valStack = getStack ValueStack res
+       in case valStack of
+            TermCell c -> c ^. cellLeft
+            TermAtom {} -> error "should be a cell"
+
+testDescr :: Asm.PosTest -> TestDescr
+testDescr Asm.PosTest {..} =
+  let tRoot = Asm.root <//> _relDir
+      file' = tRoot <//> _file
+      expected' = tRoot <//> _expectedFile
+   in TestDescr
+        { _testName = _name,
+          _testRoot = tRoot,
+          _testAssertion = Steps $ asmRunAssertionParam runNockmaAssertion file' expected' return (const (return ()))
+        }
+
+testsSlow :: [Int]
+testsSlow = [10, 11, 13, 17, 20, 23, 27, 28, 30, 32, 33, 34, 36]
+
+testsAdt :: [Int]
+testsAdt = [9, 15, 18, 25, 26, 29, 35]
+
+testsNegativeInteger :: [Int]
+testsNegativeInteger = [16, 31]
+
+testsHopeless :: [Int]
+testsHopeless =
+  [ 5,
+    6,
+    14,
+    24,
+    37
+  ]
+
+testsBugged :: [Int]
+testsBugged =
+  []
+
+testsToIgnore :: [Int]
+testsToIgnore = testsHopeless ++ testsBugged ++ testsSlow ++ testsAdt ++ testsNegativeInteger
+
+shouldRun :: Asm.PosTest -> Bool
+shouldRun Asm.PosTest {..} = testNum `notElem` map to3DigitString testsToIgnore
+  where
+    testNum :: String
+    testNum = take 3 (drop 4 _name)
+    to3DigitString :: Int -> String
+    to3DigitString n
+      | n < 10 = "00" ++ show n
+      | n < 100 = "0" ++ show n
+      | n < 1000 = show n
+      | otherwise = impossible
+
+allTests :: TestTree
+allTests =
+  testGroup
+    "Nockma Asm compile positive tests"
+    (map (mkTest . testDescr) (filter shouldRun Asm.tests))
--- a/test/Nockma/Compile/Positive.hs
+++ b/test/Nockma/Compile/Positive.hs
@ -0,0 +1,478 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+module Nockma.Compile.Positive where
+
+import Base hiding (Path)
+import Data.List.NonEmpty qualified as NonEmpty
+import Juvix.Compiler.Asm.Language qualified as Asm
+import Juvix.Compiler.Nockma.Evaluator
+import Juvix.Compiler.Nockma.Language
+import Juvix.Compiler.Nockma.Pretty
+import Juvix.Compiler.Nockma.Translation.FromAsm
+import Juvix.Compiler.Nockma.Translation.FromSource.QQ
+
+type Check = Sem '[Reader [Term Natural], Reader (Term Natural), Embed IO]
+
+data Test = Test
+  { _testName :: Text,
+    _testCheck :: Check (),
+    _testProgram :: Sem '[Compiler] ()
+  }
+
+makeLenses ''Test
+
+data FunctionName
+  = FunMain
+  | FunIncrement
+  | FunConst
+  | FunConst5
+  | FunCallInc
+  | FunAdd3
+  deriving stock (Eq, Bounded, Enum)
+
+sym :: (Enum a) => a -> FunctionId
+sym = UserFunction . Asm.defaultSymbol . fromIntegral . fromEnum
+
+debugProg :: Sem '[Compiler] () -> ([Term Natural], Term Natural)
+debugProg mkMain = run . runOutputList $ compileAndRunNock' opts exampleConstructors exampleFunctions mainFun
+  where
+    mainFun =
+      CompilerFunction
+        { _compilerFunctionName = sym FunMain,
+          _compilerFunctionArity = 0,
+          _compilerFunction = raiseUnder mkMain
+        }
+
+    opts = CompilerOptions {_compilerOptionsEnableTrace = True}
+
+isMain :: FunctionName -> Bool
+isMain = (== FunMain)
+
+functionArity' :: FunctionName -> Natural
+functionArity' = \case
+  FunMain -> 0
+  FunIncrement -> 1
+  FunConst -> 2
+  FunCallInc -> 1
+  FunConst5 -> 5
+  FunAdd3 -> 3
+
+functionCode :: (Members '[Compiler] r) => FunctionName -> Sem r ()
+functionCode = \case
+  FunMain -> impossible
+  FunIncrement -> do
+    push (OpInc # (OpAddress # pathToArg 0))
+    asmReturn
+  FunConst5 -> do
+    push (OpAddress # pathToArg 0)
+    asmReturn
+  FunConst -> do
+    push (OpAddress # pathToArg 0)
+    asmReturn
+  FunCallInc -> do
+    push (OpAddress # pathToArg 0)
+    callFun (sym FunIncrement) 1
+    asmReturn
+  FunAdd3 -> do
+    push (OpAddress # pathToArg 0)
+    push (OpAddress # pathToArg 1)
+    push (OpAddress # pathToArg 2)
+    add
+    add
+    asmReturn
+
+-- | NOTE that new constructors should be added to the end of the list or else
+-- the tests will fail.
+data ConstructorName
+  = ConstructorFalse
+  | ConstructorTrue
+  | ConstructorWrapper
+  | ConstructorPair
+  deriving stock (Eq, Bounded, Enum)
+
+constructorTag :: ConstructorName -> Asm.Tag
+constructorTag n = Asm.UserTag (Asm.TagUser defaultModuleId (fromIntegral (fromEnum n)))
+
+constructorArity :: ConstructorName -> Natural
+constructorArity = \case
+  ConstructorFalse -> 0
+  ConstructorTrue -> 0
+  ConstructorWrapper -> 1
+  ConstructorPair -> 2
+
+exampleConstructors :: ConstructorArities
+exampleConstructors =
+  hashMap $
+    [ (constructorTag n, constructorArity n)
+      | n <- allElements
+    ]
+      ++ [ (Asm.BuiltinTag Asm.TagTrue, 0),
+           (Asm.BuiltinTag Asm.TagFalse, 0)
+         ]
+
+exampleFunctions :: [CompilerFunction]
+exampleFunctions =
+  [ CompilerFunction (sym fun) (functionArity' fun) (functionCode fun)
+    | fun <- allElements,
+      not (isMain fun)
+  ]
+
+allTests :: TestTree
+allTests = testGroup "Nockma compile unit positive" (map mk tests)
+  where
+    mk :: Test -> TestTree
+    mk Test {..} = testCase (unpack _testName) $ do
+      let (traces, n) = debugProg _testProgram
+      runM (runReader n (runReader traces _testCheck))
+
+eqSubStack :: StackId -> Path -> Term Natural -> Check ()
+eqSubStack st subp expected = subStackPred st subp $
+  \n -> unless (n == expected) (err n)
+  where
+    err :: Term Natural -> Check ()
+    err n = do
+      let msg =
+            "Expected "
+              <> show st
+              <> ":\n"
+              <> ppTrace expected
+              <> "\nBut got:\n"
+              <> ppTrace n
+      assertFailure (unpack msg)
+
+eqTraces :: [Term Natural] -> Check ()
+eqTraces expected = do
+  ts <- ask
+  unless (ts == expected) (err ts)
+  where
+    err :: [Term Natural] -> Check ()
+    err ts = do
+      let msg =
+            "Expected traces:\n"
+              <> ppTrace expected
+              <> "\nBut got:\n"
+              <> ppTrace ts
+      assertFailure (unpack msg)
+
+subStackPred :: StackId -> Path -> (Term Natural -> Check ()) -> Check ()
+subStackPred st subp p = do
+  s <- getStack st <$> ask
+  case run (runError @NockEvalError (subTerm s subp)) of
+    Left {} -> assertFailure "Subterm path is not valid"
+    Right n -> p n
+
+eqStack :: StackId -> Term Natural -> Check ()
+eqStack st = eqSubStack st []
+
+unfoldTerm :: Term Natural -> NonEmpty (Term Natural)
+unfoldTerm t = case t of
+  TermAtom {} -> t :| []
+  TermCell Cell {..} -> _cellLeft NonEmpty.<| unfoldTerm _cellRight
+
+checkStackSize :: StackId -> Natural -> Check ()
+checkStackSize st stSize = subStackPred st ([] :: Path) $ \s -> do
+  let sl = NonEmpty.init (unfoldTerm s)
+      lenSl = fromIntegral (length sl)
+  unless (stSize == lenSl) (err lenSl)
+  where
+    err :: Natural -> Check ()
+    err n = do
+      let msg :: Text =
+            "Expected "
+              <> show st
+              <> "\nto have size: "
+              <> show stSize
+              <> "\nbut has size: "
+              <> show n
+      assertFailure (unpack msg)
+
+tests :: [Test]
+tests =
+  [ Test "push" (eqStack ValueStack [nock| [1 5 nil] |]) $ do
+      pushNat 5
+      pushNat 1,
+    Test "pop" (eqStack ValueStack [nock| [1 nil] |]) $ do
+      pushNat 1
+      pushNat 33
+      pop,
+    Test "increment" (eqStack ValueStack [nock| [3 nil] |]) $ do
+      pushNat 1
+      increment
+      increment,
+    Test "dec" (eqStack ValueStack [nock| [5 nil] |]) $ do
+      pushNat 6
+      dec,
+    Test "branch true" (eqStack ValueStack [nock| [5 nil] |]) $ do
+      push (nockBoolLiteral True)
+      branch (pushNat 5) (pushNat 666),
+    Test "branch false" (eqStack ValueStack [nock| [666 nil] |]) $ do
+      push (nockBoolLiteral False)
+      branch (pushNat 5) (pushNat 666),
+    Test "sub" (eqStack ValueStack [nock| [5 nil] |]) $ do
+      pushNat 3
+      pushNat 8
+      callStdlib StdlibSub,
+    Test "mul" (eqStack ValueStack [nock| [24 nil] |]) $ do
+      pushNat 8
+      pushNat 3
+      callStdlib StdlibMul,
+    Test "div" (eqStack ValueStack [nock| [3 nil] |]) $ do
+      pushNat 5
+      pushNat 15
+      callStdlib StdlibDiv,
+    Test "mod" (eqStack ValueStack [nock| [5 nil] |]) $ do
+      pushNat 10
+      pushNat 15
+      callStdlib StdlibMod,
+    Test "add" (eqStack ValueStack [nock| [5 nil] |]) $ do
+      pushNat 2
+      pushNat 3
+      add,
+    Test "pow2" (eqStack ValueStack [nock| [1 2 8 32 nil] |]) $ do
+      pushNat 5
+      pow2
+      pushNat 3
+      pow2
+      pushNat 1
+      pow2
+      pushNat 0
+      pow2,
+    Test "append rights" (eqStack ValueStack [nock| [95 3 nil] |]) $ do
+      push (OpQuote # toNock ([] :: Path))
+      pushNat 1
+      appendRights
+      push (OpQuote # toNock [L])
+      pushNat 5
+      appendRights,
+    Test "le less" (eqStack ValueStack [nock| [1 nil] |]) $ do
+      pushNat 2
+      pushNat 3
+      callStdlib StdlibLe,
+    Test "lt true" (eqStack ValueStack [nock| [0 nil] |]) $ do
+      pushNat 4
+      pushNat 3
+      callStdlib StdlibLt,
+    Test "lt eq" (eqStack ValueStack [nock| [1 nil] |]) $ do
+      pushNat 3
+      pushNat 3
+      callStdlib StdlibLt,
+    Test "le eq" (eqStack ValueStack [nock| [0 nil] |]) $ do
+      pushNat 3
+      pushNat 3
+      callStdlib StdlibLe,
+    Test "primitive eq true" (eqStack ValueStack [nock| [0 nil] |]) $ do
+      pushNat 4
+      pushNat 4
+      testEq,
+    Test "primitive eq false" (eqStack ValueStack [nock| [1 nil] |]) $ do
+      pushNat 4
+      pushNat 1
+      testEq,
+    Test
+      "save"
+      ( do
+          eqStack ValueStack [nock| [67 2 nil] |]
+          eqStack TempStack [nock| [77 nil] |]
+      )
+      $ do
+        pushNat 2
+        pushNat 3
+        save False (pushNat 77)
+        save True (pushNat 67),
+    Test "primitive increment" (eqStack ValueStack [nock| [5 nil] |]) $ do
+      pushNat 3
+      increment
+      increment,
+    Test "call increment" (eqStack ValueStack [nock| [5 nil] |]) $ do
+      pushNat 2
+      callEnum FunIncrement 1
+      callEnum FunIncrement 1
+      callEnum FunIncrement 1,
+    Test "call increment indirectly" (eqStack ValueStack [nock| [5 nil] |]) $ do
+      pushNat 2
+      callEnum FunIncrement 1
+      callEnum FunCallInc 1
+      callEnum FunIncrement 1,
+    Test
+      "push temp"
+      ( do
+          eqStack ValueStack [nock| [5 6 nil] |]
+          eqStack TempStack [nock| [6 5 nil] |]
+      )
+      $ do
+        pushNatOnto TempStack 5
+        pushNatOnto TempStack 6
+        pushTempRef 2 1
+        pushTempRef 2 0,
+    Test "push cell" (eqStack ValueStack [nock| [[1 2] nil] |]) $ do
+      push (OpQuote # (1 :: Natural) # (2 :: Natural)),
+    Test "push unit" (eqStack ValueStack [nock| [[0 nil nil] nil] |]) $ do
+      push constUnit,
+    Test "alloc nullary constructor" (eqStack ValueStack [nock| [[0 nil nil] nil] |]) $ do
+      allocConstr (constructorTag ConstructorFalse),
+    Test "alloc unary constructor" (eqStack ValueStack [nock| [[2 [[55 66] nil] nil] nil]|]) $ do
+      push (OpQuote # (55 :: Natural) # (66 :: Natural))
+      allocConstr (constructorTag ConstructorWrapper),
+    Test "alloc binary constructor" (eqStack ValueStack [nock| [[3 [9 7 nil] nil] nil] |]) $ do
+      pushNat 7
+      pushNat 9
+      allocConstr (constructorTag ConstructorPair),
+    Test
+      "alloc closure"
+      ( do
+          eqSubStack ValueStack (indexStack 0 ++ closurePath ClosureTotalArgsNum) [nock| 5 |]
+          eqSubStack ValueStack (indexStack 0 ++ closurePath ClosureArgsNum) [nock| 3 |]
+          eqSubStack ValueStack (indexStack 0 ++ closurePath ClosureArgs) [nock| [10 9 8 nil] |]
+          eqSubStack ValueStack (indexStack 1) [nock| 7 |]
+      )
+      $ do
+        pushNat 7
+        pushNat 8
+        pushNat 9
+        pushNat 10
+        allocClosure (sym FunConst5) 3,
+    Test
+      "alloc closure no args from value stack"
+      ( do
+          eqSubStack ValueStack (indexStack 0 ++ closurePath ClosureTotalArgsNum) [nock| 3 |]
+          eqSubStack ValueStack (indexStack 0 ++ closurePath ClosureArgsNum) [nock| 0 |]
+          eqSubStack ValueStack (indexStack 0 ++ closurePath ClosureArgs) [nock| nil |]
+          checkStackSize ValueStack 1
+      )
+      $ allocClosure (sym FunAdd3) 0,
+    Test
+      "extend closure"
+      ( do
+          eqSubStack ValueStack (indexStack 0 ++ closurePath ClosureTotalArgsNum) [nock| 5 |]
+          eqSubStack ValueStack (indexStack 0 ++ closurePath ClosureArgsNum) [nock| 3 |]
+          eqSubStack ValueStack (indexStack 0 ++ closurePath ClosureArgs) [nock| [10 9 8 nil] |]
+          eqSubStack ValueStack (indexStack 1) [nock| 7 |]
+      )
+      $ do
+        pushNat 7
+        pushNat 8
+        pushNat 9
+        pushNat 10
+        allocClosure (sym FunConst5) 1
+        extendClosure 2,
+    Test "alloc, extend and call closure" (eqStack ValueStack [nock| [6 nil] |]) $
+      do
+        pushNat 1
+        pushNat 2
+        pushNat 3
+        allocClosure (sym FunAdd3) 1
+        extendClosure 1
+        callHelper False Nothing 1,
+    Test "call closure" (eqStack ValueStack [nock| [110 nil] |]) $
+      do
+        pushNat 100
+        pushNat 110
+        allocClosure (sym FunConst) 1
+        callHelper False Nothing 1,
+    Test
+      "compute argsNum of a closure"
+      (eqStack ValueStack [nock| [2 7 nil] |])
+      $ do
+        pushNat 7
+        pushNat 8
+        pushNat 9
+        pushNat 10
+        allocClosure (sym FunConst5) 3
+        closureArgsNum,
+    Test
+      "save not tail"
+      ( do
+          eqStack ValueStack [nock| [17 nil] |]
+          eqStack TempStack [nock| nil |]
+      )
+      $ do
+        pushNat 10
+        save False $ do
+          pushNatOnto TempStack 7
+          addOn TempStack
+          moveTopFromTo TempStack ValueStack
+          pushNatOnto TempStack 9,
+    Test
+      "save tail"
+      ( do
+          eqStack ValueStack [nock| [17 nil] |]
+          eqStack TempStack [nock| [9 nil] |]
+      )
+      $ do
+        pushNat 10
+        save True $ do
+          pushNatOnto TempStack 7
+          addOn TempStack
+          moveTopFromTo TempStack ValueStack
+          pushNatOnto TempStack 9,
+    Test
+      "cmdCase: single branch"
+      (eqStack ValueStack [nock| [777 [2 [123 nil] nil] nil] |])
+      $ do
+        pushNat 123
+        allocConstr (constructorTag ConstructorWrapper)
+        caseCmd
+          Nothing
+          [ (constructorTag ConstructorWrapper, pushNat 777)
+          ],
+    Test
+      "cmdCase: default branch"
+      (eqStack ValueStack [nock| [5 nil] |])
+      $ do
+        pushNat 123
+        allocConstr (constructorTag ConstructorWrapper)
+        caseCmd
+          (Just (pop >> pushNat 5))
+          [ (constructorTag ConstructorFalse, pushNat 777)
+          ],
+    Test
+      "cmdCase: second branch"
+      (eqStack ValueStack [nock| [5 nil] |])
+      $ do
+        pushNat 123
+        allocConstr (constructorTag ConstructorWrapper)
+        caseCmd
+          (Just (pushNat 0))
+          [ (constructorTag ConstructorFalse, pushNat 0),
+            (constructorTag ConstructorWrapper, pop >> pushNat 5)
+          ],
+    Test
+      "cmdCase: case on builtin true"
+      (eqStack ValueStack [nock| [5 nil] |])
+      $ do
+        allocConstr (Asm.BuiltinTag Asm.TagTrue)
+        caseCmd
+          (Just (pushNat 0))
+          [ (Asm.BuiltinTag Asm.TagTrue, pop >> pushNat 5),
+            (Asm.BuiltinTag Asm.TagFalse, pushNat 0)
+          ],
+    Test
+      "cmdCase: case on builtin false"
+      (eqStack ValueStack [nock| [5 nil] |])
+      $ do
+        allocConstr (Asm.BuiltinTag Asm.TagFalse)
+        caseCmd
+          (Just (pushNat 0))
+          [ (Asm.BuiltinTag Asm.TagTrue, pushNat 0),
+            (Asm.BuiltinTag Asm.TagFalse, pop >> pushNat 5)
+          ],
+    Test
+      "push constructor field"
+      (eqStack TempStack [nock| [30 nil] |])
+      $ do
+        pushNat 10
+        pushNat 20
+        allocConstr (constructorTag ConstructorPair)
+        pushConstructorFieldOnto TempStack Asm.StackRef 0
+        pushConstructorFieldOnto TempStack Asm.StackRef 1
+        addOn TempStack,
+    Test
+      "trace"
+      ( do
+          eqStack ValueStack [nock| [10 nil] |]
+          eqTraces [[nock| 10 |]]
+      )
+      $ do
+        pushNat 10
+        traceTerm (OpAddress # topOfStack ValueStack)
+  ]
--- a/test/Nockma/Eval/Positive.hs
+++ b/test/Nockma/Eval/Positive.hs
@ -26,6 +26,7 @@ allTests = testGroup "Nockma eval unit positive" (map mk tests)
    mk Test {..} = testCase (unpack _testName) $ do
      let evalResult =
            run
+              . ignoreOutput @(Term Natural)
              . runError @(ErrNockNatural Natural)
              . runError @NockEvalError
              $ eval _testProgramSubject _testProgramFormula