diff --git a/app/App.hs b/app/App.hs
index f73fbacb77..3980567030 100644
--- 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
diff --git a/app/Commands/Compile.hs b/app/Commands/Compile.hs
index 35a2fd2561..208e3e53df 100644
--- 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 ->
diff --git a/app/Commands/Dev/Asm/Compile.hs b/app/Commands/Dev/Asm/Compile.hs
index 5743893469..8fde8cdfde 100644
--- 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"
diff --git a/app/Commands/Dev/Asm/Compile/Options.hs b/app/Commands/Dev/Asm/Compile/Options.hs
index 81e14e9500..0c3d016c84 100644
--- 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
diff --git a/app/Commands/Dev/Core/Compile.hs b/app/Commands/Dev/Core/Compile.hs
index d4ad7d91e1..fab54bce3a 100644
--- 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)
diff --git a/app/Commands/Dev/Core/Compile/Base.hs b/app/Commands/Dev/Core/Compile/Base.hs
index 76c0d122c0..82d7319d50 100644
--- 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)
diff --git a/app/Commands/Dev/Nockma.hs b/app/Commands/Dev/Nockma.hs
index d45602f70d..3a241743aa 100644
--- 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
diff --git a/app/Commands/Dev/Nockma/Eval.hs b/app/Commands/Dev/Nockma/Eval.hs
new file mode 100644
index 0000000000..c48fe1769a
--- /dev/null
+++ 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"
diff --git a/app/Commands/Dev/Nockma/Eval/Options.hs b/app/Commands/Dev/Nockma/Eval/Options.hs
new file mode 100644
index 0000000000..942ab51981
--- /dev/null
+++ 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 {..}
diff --git a/app/Commands/Dev/Nockma/Options.hs b/app/Commands/Dev/Nockma/Options.hs
index 3720873bfa..ec8f41d3b2 100644
--- 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")
diff --git a/app/Commands/Dev/Nockma/Repl.hs b/app/Commands/Dev/Nockma/Repl.hs
index 05b8800953..bc19569424 100644
--- 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
diff --git a/app/Commands/Dev/Nockma/Repl/Options.hs b/app/Commands/Dev/Nockma/Repl/Options.hs
index 4ac9aac147..6695e67227 100644
--- 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 {..}
diff --git a/app/Commands/Extra/Compile.hs b/app/Commands/Extra/Compile.hs
index bcd52a02cd..c23a86422b 100644
--- 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.
diff --git a/app/Commands/Extra/Compile/Options.hs b/app/Commands/Extra/Compile/Options.hs
index 9de19acfe4..4c4892f6cc 100644
--- 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 ->
diff --git a/package.yaml b/package.yaml
index 39e30899d5..3bd92c1bc0 100644
--- a/package.yaml
+++ b/package.yaml
@@ -143,6 +143,7 @@ default-extensions:
   - NoFieldSelectors
   - NoImplicitPrelude
   - OverloadedStrings
+  - QuasiQuotes
   - RecordWildCards
   - TemplateHaskell
   - TypeFamilyDependencies
diff --git a/migrate-juvix-yaml.sh b/scripts/migrate-juvix-yaml.sh
similarity index 100%
rename from migrate-juvix-yaml.sh
rename to scripts/migrate-juvix-yaml.sh
diff --git a/scripts/nockma-stdlib-parser.sh b/scripts/nockma-stdlib-parser.sh
new file mode 100755
index 0000000000..c5c92107b9
--- /dev/null
+++ 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}'
diff --git a/src/Juvix/Compiler/Asm/Data.hs b/src/Juvix/Compiler/Asm/Data.hs
index 07f3c31734..83f5d27e07 100644
--- 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)
diff --git a/src/Juvix/Compiler/Asm/Data/CallGraph.hs b/src/Juvix/Compiler/Asm/Data/CallGraph.hs
index 3cf0ebddfe..43d19d4d4d 100644
--- 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
diff --git a/src/Juvix/Compiler/Asm/Data/InfoTable.hs b/src/Juvix/Compiler/Asm/Data/InfoTable.hs
index 2c957fe666..4d27792632 100644
--- 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
diff --git a/src/Juvix/Compiler/Asm/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Asm/Data/InfoTableBuilder.hs
index 64459f4c21..b2275b8e1d 100644
--- 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))))
diff --git a/src/Juvix/Compiler/Asm/Extra/Apply.hs b/src/Juvix/Compiler/Asm/Extra/Apply.hs
index 840867487d..39e0e4927c 100644
--- 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
diff --git a/src/Juvix/Compiler/Asm/Extra/Base.hs b/src/Juvix/Compiler/Asm/Extra/Base.hs
index 5d2e5d49a4..6c3b02421c 100644
--- 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
diff --git a/src/Juvix/Compiler/Asm/Extra/Memory.hs b/src/Juvix/Compiler/Asm/Extra/Memory.hs
index 22beba8f24..73f827ff66 100644
--- 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
diff --git a/src/Juvix/Compiler/Asm/Extra/Recursors.hs b/src/Juvix/Compiler/Asm/Extra/Recursors.hs
index dfef342226..3573bc4370 100644
--- 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)
 
diff --git a/src/Juvix/Compiler/Asm/Extra/Type.hs b/src/Juvix/Compiler/Asm/Extra/Type.hs
index 951cbc19bf..c2d4f81550 100644
--- 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
diff --git a/src/Juvix/Compiler/Asm/Interpreter.hs b/src/Juvix/Compiler/Asm/Interpreter.hs
index 8e4cbb66e4..29d0936952 100644
--- 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
diff --git a/src/Juvix/Compiler/Asm/Interpreter/Runtime.hs b/src/Juvix/Compiler/Asm/Interpreter/Runtime.hs
index 32bc1afe18..f183bbe8e2 100644
--- 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 ->
diff --git a/src/Juvix/Compiler/Asm/Language.hs b/src/Juvix/Compiler/Asm/Language.hs
index d78570ba44..c09f8c619d 100644
--- 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
 
diff --git a/src/Juvix/Compiler/Asm/Pipeline.hs b/src/Juvix/Compiler/Asm/Pipeline.hs
index 8603795415..66be53368d 100644
--- 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'
diff --git a/src/Juvix/Compiler/Asm/Pretty.hs b/src/Juvix/Compiler/Asm/Pretty.hs
index 9fa1d33f57..b3ba68bf02 100644
--- 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
diff --git a/src/Juvix/Compiler/Asm/Pretty/Base.hs b/src/Juvix/Compiler/Asm/Pretty/Base.hs
index dd426892f9..2e0856c305 100644
--- 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
           )
 
diff --git a/src/Juvix/Compiler/Asm/Pretty/Options.hs b/src/Juvix/Compiler/Asm/Pretty/Options.hs
index 5b9338e614..59bb554668 100644
--- 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
diff --git a/src/Juvix/Compiler/Asm/Transformation.hs b/src/Juvix/Compiler/Asm/Transformation.hs
index 2ae5c055b2..f1c6196166 100644
--- 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
diff --git a/src/Juvix/Compiler/Asm/Transformation/FilterUnreachable.hs b/src/Juvix/Compiler/Asm/Transformation/FilterUnreachable.hs
index 79a6d96932..30bcc0ca13 100644
--- 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
diff --git a/src/Juvix/Compiler/Asm/Transformation/TempHeight.hs b/src/Juvix/Compiler/Asm/Transformation/TempHeight.hs
new file mode 100644
index 0000000000..1eab2d8909
--- /dev/null
+++ 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
diff --git a/src/Juvix/Compiler/Asm/Translation/FromCore.hs b/src/Juvix/Compiler/Asm/Translation/FromCore.hs
index bc9587f497..c2907413ed 100644
--- 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
diff --git a/src/Juvix/Compiler/Asm/Translation/FromSource.hs b/src/Juvix/Compiler/Asm/Translation/FromSource.hs
index 62b62302fe..50b3e09bea 100644
--- 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
diff --git a/src/Juvix/Compiler/Backend.hs b/src/Juvix/Compiler/Backend.hs
index b505c21590..54e2e7f50b 100644
--- 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 =
diff --git a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
index 44443ca887..f09d6ee697 100644
--- 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)
diff --git a/src/Juvix/Compiler/Core/Language/Base.hs b/src/Juvix/Compiler/Core/Language/Base.hs
index 2ab80eb4c5..55bb26c078 100644
--- 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
diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index c13e56414a..5e9cd8d3e7 100644
--- 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
diff --git a/src/Juvix/Compiler/Nockma/Evaluator.hs b/src/Juvix/Compiler/Nockma/Evaluator.hs
index c331beeef9..2d38b3f1d0 100644
--- 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)
diff --git a/src/Juvix/Compiler/Nockma/Evaluator/Error.hs b/src/Juvix/Compiler/Nockma/Evaluator/Error.hs
index ef1f9ff9cf..2d04e39fda 100644
--- 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)
diff --git a/src/Juvix/Compiler/Nockma/Language.hs b/src/Juvix/Compiler/Nockma/Language.hs
index 523603a3af..cf284db813 100644
--- 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 []
diff --git a/src/Juvix/Compiler/Nockma/Pretty.hs b/src/Juvix/Compiler/Nockma/Pretty.hs
index 32a1c56e78..fc6730e79f 100644
--- 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
diff --git a/src/Juvix/Compiler/Nockma/Pretty/Base.hs b/src/Juvix/Compiler/Nockma/Pretty/Base.hs
index 926ce130ad..3d103210fd 100644
--- 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'))
diff --git a/src/Juvix/Compiler/Nockma/Pretty/Options.hs b/src/Juvix/Compiler/Nockma/Pretty/Options.hs
index 6b2ba92d63..0914bc67e6 100644
--- 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
diff --git a/src/Juvix/Compiler/Nockma/Translation/FromAsm.hs b/src/Juvix/Compiler/Nockma/Translation/FromAsm.hs
new file mode 100644
index 0000000000..f3719a51cd
--- /dev/null
+++ b/src/Juvix/Compiler/Nockma/Translation/FromAsm.hs
@@ -0,0 +1,1048 @@
+module Juvix.Compiler.Nockma.Translation.FromAsm where
+
+import Juvix.Compiler.Asm.Data.InfoTable qualified as Asm
+import Juvix.Compiler.Nockma.Evaluator
+import Juvix.Compiler.Nockma.Pretty
+import Juvix.Compiler.Nockma.Stdlib
+import Juvix.Compiler.Pipeline.EntryPoint
+import Juvix.Prelude hiding (Atom, Path)
+
+type UserFunctionId = Symbol
+
+data FunctionId
+  = UserFunction UserFunctionId
+  | BuiltinFunction BuiltinFunctionId
+  deriving stock (Generic, Eq)
+
+instance Hashable FunctionId
+
+data BuiltinFunctionId
+  = BuiltinPow2Go
+  | BuiltinPow2
+  | BuiltinAppendRights
+  deriving stock (Eq, Enum, Bounded, Generic)
+
+instance Hashable BuiltinFunctionId
+
+newtype CompilerOptions = CompilerOptions
+  {_compilerOptionsEnableTrace :: Bool}
+
+fromEntryPoint :: EntryPoint -> CompilerOptions
+fromEntryPoint EntryPoint {..} =
+  CompilerOptions
+    { _compilerOptionsEnableTrace = _entryPointDebug
+    }
+
+data FunctionInfo = FunctionInfo
+  { _functionInfoPath :: Path,
+    _functionInfoArity :: Natural
+  }
+
+data CompilerCtx = CompilerCtx
+  { _compilerFunctionInfos :: HashMap FunctionId FunctionInfo,
+    _compilerConstructorArities :: ConstructorArities,
+    _compilerOptions :: CompilerOptions
+  }
+
+type ConstructorArities = HashMap Asm.Tag Natural
+
+type Offset = Natural
+
+data CompilerFunction = CompilerFunction
+  { _compilerFunctionName :: FunctionId,
+    _compilerFunctionArity :: Natural,
+    _compilerFunction :: Sem '[Compiler, Reader CompilerCtx] ()
+  }
+
+data StackId
+  = CurrentFunction
+  | ValueStack
+  | TempStack
+  | AuxStack
+  | FrameStack
+  | StandardLibrary
+  | FunctionsLibrary
+  deriving stock (Enum, Bounded, Eq, Show)
+
+-- | A closure has the following structure:
+-- [code totalArgsNum argsNum args], where
+-- 1. code is code to run when fully applied.
+-- 2. totalArgsNum is the number of arguments that the function
+--     which created the closure expects.
+-- 3. argsNum is the number of arguments that have been applied to the closure.
+-- 4. args is the list of args that have been applied.
+--    The length of the list should be argsNum.
+data ClosurePathId
+  = ClosureCode
+  | ClosureTotalArgsNum
+  | ClosureArgsNum
+  | ClosureArgs
+  deriving stock (Bounded, Enum)
+
+pathFromEnum :: (Enum a) => a -> Path
+pathFromEnum = indexStack . fromIntegral . fromEnum
+
+closurePath :: ClosurePathId -> Path
+closurePath = pathFromEnum
+
+data ConstructorPathId
+  = ConstructorTag
+  | ConstructorArgs
+  deriving stock (Bounded, Enum)
+
+constructorPath :: ConstructorPathId -> Path
+constructorPath = pathFromEnum
+
+data ActivationFramePathId
+  = ActivationFrameValueStack
+  | ActivationFrameTempStack
+  | ActivationFrameAuxStack
+  deriving stock (Bounded, Enum)
+
+activationFramePath :: ActivationFramePathId -> Path
+activationFramePath = pathFromEnum
+
+data FunctionPathId
+  = FunctionCode
+  | FunctionArgs
+
+functionPath :: FunctionPathId -> Path
+functionPath = \case
+  FunctionCode -> [L]
+  FunctionArgs -> [R]
+
+data StdlibFunction
+  = StdlibDec
+  | StdlibAdd
+  | StdlibSub
+  | StdlibMul
+  | StdlibDiv
+  | StdlibMod
+  | StdlibLt
+  | StdlibLe
+
+stdlibNumArgs :: StdlibFunction -> Natural
+stdlibNumArgs = \case
+  StdlibDec -> 1
+  StdlibAdd -> 2
+  StdlibSub -> 2
+  StdlibMul -> 2
+  StdlibMod -> 2
+  StdlibDiv -> 2
+  StdlibLe -> 2
+  StdlibLt -> 2
+
+-- | The stdlib paths are obtained using scripts/nockma-stdlib-parser.sh
+stdlibPath :: StdlibFunction -> Path
+stdlibPath =
+  decodePath' . EncodedPath . \case
+    StdlibDec -> 342
+    StdlibAdd -> 20
+    StdlibSub -> 47
+    StdlibMul -> 4
+    StdlibDiv -> 170
+    StdlibMod -> 46
+    StdlibLe -> 84
+    StdlibLt -> 343
+
+numStacks :: (Integral a) => a
+numStacks = fromIntegral (length (allElements @StackId))
+
+data Compiler m a where
+  Verbatim :: Term Natural -> Compiler m ()
+  TraceTerm :: Term Natural -> Compiler m ()
+  PushOnto :: StackId -> Term Natural -> Compiler m ()
+  Crash :: Compiler m ()
+  PopNAndPushOnto :: StackId -> Natural -> Term Natural -> Compiler m ()
+  PopFromN :: Natural -> StackId -> Compiler m ()
+  TestEqOn :: StackId -> Compiler m ()
+  CallHelper :: Bool -> Maybe FunctionId -> Natural -> Compiler m ()
+  IncrementOn :: StackId -> Compiler m ()
+  Branch :: m () -> m () -> Compiler m ()
+  Save :: Bool -> m () -> Compiler m ()
+  CallStdlibOn :: StackId -> StdlibFunction -> Compiler m ()
+  AsmReturn :: Compiler m ()
+  GetConstructorArity :: Asm.Tag -> Compiler m Natural
+  GetFunctionArity :: FunctionId -> Compiler m Natural
+  GetFunctionPath :: FunctionId -> Compiler m Path
+
+stackPath :: StackId -> Path
+stackPath s = indexStack (fromIntegral (fromEnum s))
+
+indexStack :: Natural -> Path
+indexStack idx = replicate idx R ++ [L]
+
+indexInPath :: Path -> Natural -> Path
+indexInPath p idx = p ++ indexStack idx
+
+topOfStack :: StackId -> Path
+topOfStack s = indexInStack s 0
+
+indexInStack :: StackId -> Natural -> Path
+indexInStack s idx = stackPath s ++ indexStack idx
+
+pathToArgumentsArea :: Path
+pathToArgumentsArea = topOfStack CurrentFunction ++ functionPath FunctionArgs
+
+pathToArg :: Natural -> Path
+pathToArg = indexInPath pathToArgumentsArea
+
+-- | Construct a path rooted at he head of a named stack
+pathInStack :: StackId -> Path -> Path
+pathInStack s p = stackPath s ++ p
+
+makeSem ''Compiler
+makeLenses ''CompilerOptions
+makeLenses ''CompilerFunction
+makeLenses ''CompilerCtx
+makeLenses ''FunctionInfo
+
+termFromParts :: (Bounded p, Enum p) => (p -> Term Natural) -> Term Natural
+termFromParts f = remakeList [f pi | pi <- allElements]
+
+makeClosure :: (ClosurePathId -> Term Natural) -> Term Natural
+makeClosure = termFromParts
+
+makeConstructor :: (ConstructorPathId -> Term Natural) -> Term Natural
+makeConstructor = termFromParts
+
+makeActivationFrame :: (ActivationFramePathId -> Term Natural) -> Term Natural
+makeActivationFrame = termFromParts
+
+makeFunction :: (FunctionPathId -> Term Natural) -> Term Natural
+makeFunction f = f FunctionCode # f FunctionArgs
+
+foldTerms :: NonEmpty (Term Natural) -> Term Natural
+foldTerms = foldr1 (#)
+
+-- | Use `Asm.toNockma` before calling this function
+fromAsmTable :: (Members '[Error JuvixError, Reader CompilerOptions] r) => Asm.InfoTable -> Sem r (Cell Natural)
+fromAsmTable t = case t ^. Asm.infoMainFunction of
+  Just mainFun -> do
+    opts <- ask
+    return (fromAsm opts mainFun t)
+  Nothing -> throw @JuvixError (error "TODO")
+  where
+    fromAsm :: CompilerOptions -> Asm.Symbol -> Asm.InfoTable -> Cell Natural
+    fromAsm opts mainSym Asm.InfoTable {..} =
+      let funs = map compileFunction allFunctions
+          constrs :: ConstructorArities
+          constrs = fromIntegral . (^. Asm.constructorArgsNum) <$> _infoConstrs
+       in runCompilerWith opts constrs funs mainFun
+      where
+        mainFun :: CompilerFunction
+        mainFun =
+          CompilerFunction
+            { _compilerFunctionName = UserFunction mainSym,
+              _compilerFunctionArity = 0,
+              _compilerFunction = compile mainCode
+            }
+
+        mainCode :: Asm.Code
+        mainCode = _infoFunctions ^?! at mainSym . _Just . Asm.functionCode
+
+        allFunctions :: [Asm.FunctionInfo]
+        allFunctions = filter notMain (toList _infoFunctions)
+          where
+            notMain :: Asm.FunctionInfo -> Bool
+            notMain Asm.FunctionInfo {..} = _functionSymbol /= mainSym
+
+        compileFunction :: Asm.FunctionInfo -> CompilerFunction
+        compileFunction Asm.FunctionInfo {..} =
+          CompilerFunction
+            { _compilerFunctionName = UserFunction _functionSymbol,
+              _compilerFunctionArity = fromIntegral _functionArgsNum,
+              _compilerFunction = compile _functionCode
+            }
+
+fromOffsetRef :: Asm.OffsetRef -> Natural
+fromOffsetRef = fromIntegral . (^. Asm.offsetRefOffset)
+
+-- | Generic constructors are encoded as [tag args], where args is a
+-- nil terminated list.
+goConstructor :: Asm.Tag -> [Term Natural] -> Term Natural
+goConstructor t args = case t of
+  Asm.BuiltinTag b -> makeConstructor $ \case
+    ConstructorTag -> builtinTagToTerm b
+    ConstructorArgs -> remakeList []
+  Asm.UserTag tag ->
+    makeConstructor $ \case
+      ConstructorTag -> OpQuote # (fromIntegral (tag ^. Asm.tagUserWord) :: Natural)
+      ConstructorArgs -> remakeList args
+
+compile :: forall r. (Members '[Compiler] r) => Asm.Code -> Sem r ()
+compile = mapM_ goCommand
+  where
+    goCommand :: Asm.Command -> Sem r ()
+    goCommand = \case
+      Asm.Instr i -> goCmdInstr i
+      Asm.Branch b -> goBranch b
+      Asm.Case c -> goCase c
+      Asm.Save s -> goSave s
+
+    goSave :: Asm.CmdSave -> Sem r ()
+    goSave cmd = save (cmd ^. Asm.cmdSaveIsTail) (compile (cmd ^. Asm.cmdSaveCode))
+
+    goCase :: Asm.CmdCase -> Sem r ()
+    goCase c = do
+      let def = compile <$> c ^. Asm.cmdCaseDefault
+          branches =
+            [ (b ^. Asm.caseBranchTag, compile (b ^. Asm.caseBranchCode))
+              | b <- c ^. Asm.cmdCaseBranches
+            ]
+      caseCmd def branches
+
+    goBranch :: Asm.CmdBranch -> Sem r ()
+    goBranch Asm.CmdBranch {..} = branch (compile _cmdBranchTrue) (compile _cmdBranchFalse)
+
+    goBinop :: Asm.Opcode -> Sem r ()
+    goBinop o = case o of
+      Asm.IntAdd -> callStdlib StdlibAdd
+      Asm.IntSub -> callStdlib StdlibSub
+      Asm.IntMul -> callStdlib StdlibMul
+      Asm.IntDiv -> callStdlib StdlibDiv
+      Asm.IntMod -> callStdlib StdlibMod
+      Asm.IntLt -> callStdlib StdlibLt
+      Asm.IntLe -> callStdlib StdlibLe
+      Asm.ValEq -> testEq
+      Asm.StrConcat -> stringsErr
+
+    goPush :: Asm.Value -> Sem r ()
+    goPush = \case
+      Asm.ConstInt i
+        | i < 0 -> unsupported "negative numbers"
+        | otherwise -> pushNat (fromInteger i)
+      Asm.ConstBool i -> push (nockBoolLiteral i)
+      Asm.ConstString {} -> stringsErr
+      Asm.ConstUnit -> push constUnit
+      Asm.ConstVoid -> push constVoid
+      Asm.Ref r -> pushMemValue r
+      where
+        pushMemValue :: Asm.MemValue -> Sem r ()
+        pushMemValue = \case
+          Asm.DRef r -> pushDirectRef r
+          Asm.ConstrRef r ->
+            pushConstructorField
+              (r ^. Asm.fieldRef)
+              (fromIntegral (r ^. Asm.fieldOffset))
+
+    goAllocClosure :: Asm.InstrAllocClosure -> Sem r ()
+    goAllocClosure a = allocClosure (UserFunction (a ^. Asm.allocClosureFunSymbol)) (fromIntegral (a ^. Asm.allocClosureArgsNum))
+
+    goExtendClosure :: Asm.InstrExtendClosure -> Sem r ()
+    goExtendClosure a = extendClosure (fromIntegral (a ^. Asm.extendClosureArgsNum))
+
+    goCallHelper :: Bool -> Asm.InstrCall -> Sem r ()
+    goCallHelper isTail Asm.InstrCall {..} =
+      let funName = case _callType of
+            Asm.CallFun fun -> Just fun
+            Asm.CallClosure -> Nothing
+       in callHelper isTail (UserFunction <$> funName) (fromIntegral _callArgsNum)
+
+    goCall :: Asm.InstrCall -> Sem r ()
+    goCall = goCallHelper False
+
+    goTailCall :: Asm.InstrCall -> Sem r ()
+    goTailCall = goCallHelper True
+
+    goDump :: Sem r ()
+    goDump = do
+      dumpStack ValueStack
+      dumpStack AuxStack
+      dumpStack TempStack
+      dumpStack FrameStack
+
+    goTrace :: Sem r ()
+    goTrace = traceTerm (OpAddress # topOfStack ValueStack)
+
+    goCmdInstr :: Asm.CmdInstr -> Sem r ()
+    goCmdInstr Asm.CmdInstr {..} = case _cmdInstrInstruction of
+      Asm.Binop op -> goBinop op
+      Asm.Push p -> goPush p
+      Asm.Pop -> pop
+      Asm.Failure -> crash
+      Asm.AllocConstr i -> allocConstr i
+      Asm.AllocClosure c -> goAllocClosure c
+      Asm.ExtendClosure c -> goExtendClosure c
+      Asm.Call c -> goCall c
+      Asm.TailCall c -> goTailCall c
+      Asm.Return -> asmReturn
+      Asm.ArgsNum -> closureArgsNum
+      Asm.ValShow -> stringsErr
+      Asm.StrToInt -> stringsErr
+      Asm.Trace -> goTrace
+      Asm.Dump -> goDump
+      Asm.Prealloc {} -> impossible
+      Asm.CallClosures {} -> impossible
+      Asm.TailCallClosures {} -> impossible
+
+extendClosure :: (Members '[Compiler] r) => Natural -> Sem r ()
+extendClosure extraArgsNum = do
+  let pathToOldClosure = topOfStack ValueStack
+      oldArgs = OpAddress # pathToOldClosure ++ closurePath ClosureArgs
+      curArgsNum = OpAddress # pathToOldClosure ++ closurePath ClosureArgsNum
+      extraArgs = stackSliceAsList ValueStack 1 extraArgsNum
+  push (OpQuote # toNock ([] :: Path))
+  push (OpAddress # indexInStack ValueStack 1 ++ closurePath ClosureArgsNum)
+  appendRights
+  moveTopFromTo ValueStack AuxStack
+  -- valueStack: [oldclosure ..]
+  -- tempstack: [posOfArgsNil ..]
+  pushOnto AuxStack curArgsNum
+  pushNatOnto AuxStack extraArgsNum
+  addOn AuxStack
+  pushOnto AuxStack extraArgs
+  -- valueStack: [oldclosure ..]
+  -- tempstack: [xtraArgsList newArgsNum posOfArgsNil ..]
+  let xtraArgs = OpAddress # topOfStack AuxStack
+      newArgsNum = OpAddress # indexInStack AuxStack 1
+      posOfArgsNil = OpAddress # indexInStack AuxStack 2
+      newClosure = makeClosure $ \case
+        ClosureCode -> OpAddress # pathToOldClosure ++ closurePath ClosureCode
+        ClosureTotalArgsNum -> OpAddress # pathToOldClosure ++ closurePath ClosureTotalArgsNum
+        ClosureArgsNum -> newArgsNum
+        ClosureArgs -> replaceSubterm' oldArgs posOfArgsNil xtraArgs
+  pushOnto AuxStack newClosure
+  popN (1 + extraArgsNum)
+  moveTopFromTo AuxStack ValueStack
+  popFromN 3 AuxStack
+
+constUnit :: Term Natural
+constUnit = constVoid
+
+constVoid :: Term Natural
+constVoid = makeConstructor $ \case
+  ConstructorTag -> OpQuote # toNock (0 :: Natural)
+  ConstructorArgs -> remakeList []
+
+pushConstructorFieldOnto :: (Members '[Compiler] r) => StackId -> Asm.DirectRef -> Natural -> Sem r ()
+pushConstructorFieldOnto s refToConstr argIx =
+  let path = directRefPath refToConstr ++ constructorPath ConstructorArgs ++ indexStack argIx
+   in pushOnto s (OpAddress # path)
+
+pushConstructorField :: (Members '[Compiler] r) => Asm.DirectRef -> Natural -> Sem r ()
+pushConstructorField = pushConstructorFieldOnto ValueStack
+
+directRefPath :: Asm.DirectRef -> Path
+directRefPath = \case
+  Asm.StackRef -> topOfStack ValueStack
+  Asm.ArgRef a -> pathToArg (fromOffsetRef a)
+  Asm.TempRef Asm.RefTemp {..} -> tempRefPath (fromIntegral (fromJust _refTempTempHeight)) (fromOffsetRef _refTempOffsetRef)
+
+pushDirectRef :: (Members '[Compiler] r) => Asm.DirectRef -> Sem r ()
+pushDirectRef = push . (OpAddress #) . directRefPath
+
+tempRefPath :: Natural -> Natural -> Path
+tempRefPath tempHeight off = indexInStack TempStack (tempHeight - off - 1)
+
+pushTempRef :: (Members '[Compiler] r) => Natural -> Natural -> Sem r ()
+pushTempRef tempHeight = push . (OpAddress #) . tempRefPath tempHeight
+
+allocClosure :: (Members '[Compiler] r) => FunctionId -> Natural -> Sem r ()
+allocClosure funSym numArgs = do
+  funPath <- getFunctionPath funSym
+  funAri <- getFunctionArity funSym
+  pushOnto AuxStack (stackTake ValueStack numArgs)
+  let closure = makeClosure $ \case
+        ClosureCode -> OpAddress # funPath
+        ClosureTotalArgsNum -> OpQuote # toNock funAri
+        ClosureArgsNum -> OpQuote # toNock numArgs
+        ClosureArgs -> OpAddress # topOfStack AuxStack
+  popNAndPushOnto ValueStack numArgs closure
+  popFrom AuxStack
+
+closureArgsNum :: (Members '[Compiler] r) => Sem r ()
+closureArgsNum = do
+  let helper p = OpAddress # topOfStack ValueStack ++ closurePath p
+  sub (helper ClosureTotalArgsNum) (helper ClosureArgsNum) pop
+
+allocConstr :: (Members '[Compiler] r) => Asm.Tag -> Sem r ()
+allocConstr tag = do
+  numArgs <- getConstructorArity tag
+  let args = [OpAddress # indexInStack ValueStack (pred i) | i <- [1 .. numArgs]]
+      constr = goConstructor tag args
+  pushOnto AuxStack constr
+  popN numArgs
+  moveTopFromTo AuxStack ValueStack
+
+copyTopFromTo :: (Members '[Compiler] r) => StackId -> StackId -> Sem r ()
+copyTopFromTo from toStack = pushOnto toStack (OpAddress # topOfStack from)
+
+moveTopFromTo :: (Members '[Compiler] r) => StackId -> StackId -> Sem r ()
+moveTopFromTo from toStack = do
+  pushOnto toStack (OpAddress # topOfStack from)
+  popFrom from
+
+unsupported :: Text -> a
+unsupported thing = error ("The Nockma backend does not support " <> thing)
+
+stringsErr :: a
+stringsErr = unsupported "strings"
+
+-- | Computes a - b
+sub :: (Members '[Compiler] r) => Term Natural -> Term Natural -> Sem r () -> Sem r ()
+sub a b aux = do
+  pushOnto AuxStack b
+  pushOnto AuxStack a
+  aux
+  callStdlibOn AuxStack StdlibSub
+  moveTopFromTo AuxStack ValueStack
+
+seqTerms :: [Term Natural] -> Term Natural
+seqTerms = foldl' step (OpAddress # emptyPath) . reverse
+  where
+    step :: Term Natural -> Term Natural -> Term Natural
+    step acc t = OpSequence # t # acc
+
+makeEmptyList :: Term Natural
+makeEmptyList = makeList []
+
+makeList :: [Term Natural] -> Term Natural
+makeList ts = foldTerms (ts `prependList` pure (TermAtom nockNil))
+
+remakeList :: (Foldable l) => l (Term Natural) -> Term Natural
+remakeList ts = foldTerms (toList ts `prependList` pure (OpQuote # nockNil'))
+
+nockNil' :: Term Natural
+nockNil' = TermAtom nockNil
+
+initStack :: [Term Natural] -> Term Natural
+initStack defs = makeList (initSubStack <$> allElements)
+  where
+    initSubStack :: StackId -> Term Natural
+    initSubStack = \case
+      CurrentFunction -> nockNil'
+      ValueStack -> nockNil'
+      FrameStack -> nockNil'
+      TempStack -> nockNil'
+      AuxStack -> nockNil'
+      StandardLibrary -> stdlib
+      FunctionsLibrary -> makeList defs
+
+push :: (Members '[Compiler] r) => Term Natural -> Sem r ()
+push = pushOnto ValueStack
+
+execCompilerList :: (Member (Reader CompilerCtx) r) => Sem (Compiler ': r) a -> Sem r [Term Natural]
+execCompilerList = fmap fst . runCompilerList
+
+runCompilerList :: (Member (Reader CompilerCtx) r) => Sem (Compiler ': r) a -> Sem r ([Term Natural], a)
+runCompilerList sem = do
+  (ts, a) <- runOutputList (re sem)
+  return (ts, a)
+
+execCompiler :: (Member (Reader CompilerCtx) r) => Sem (Compiler ': r) a -> Sem r (Term Natural)
+execCompiler = fmap fst . runCompiler
+
+runCompiler :: (Member (Reader CompilerCtx) r) => Sem (Compiler ': r) a -> Sem r (Term Natural, a)
+runCompiler sem = do
+  (ts, a) <- runOutputList (re sem)
+  return (seqTerms ts, a)
+
+runCompilerWith :: CompilerOptions -> ConstructorArities -> [CompilerFunction] -> CompilerFunction -> Cell Natural
+runCompilerWith opts constrs libFuns mainFun =
+  let entryCommand :: (Members '[Compiler] r) => Sem r ()
+      entryCommand = callFun (mainFun ^. compilerFunctionName) 0
+      entryTerm =
+        seqTerms
+          . run
+          . runReader compilerCtx
+          . execOutputList
+          . re
+          $ entryCommand
+      compiledFuns :: NonEmpty (Term Natural)
+      compiledFuns =
+        makeFunction'
+          <$> ( run
+                  . runReader compilerCtx
+                  . mapM (execCompiler . (^. compilerFunction))
+                  $ allFuns
+              )
+      makeFunction' :: Term Natural -> Term Natural
+      makeFunction' c = makeFunction $ \case
+        FunctionCode -> c
+        FunctionArgs -> nockNil'
+   in Cell (initStack (toList compiledFuns)) entryTerm
+  where
+    allFuns :: NonEmpty CompilerFunction
+    allFuns = mainFun :| libFuns ++ (builtinFunction <$> allElements)
+
+    compilerCtx :: CompilerCtx
+    compilerCtx =
+      CompilerCtx
+        { _compilerFunctionInfos = functionInfos,
+          _compilerConstructorArities = constrs,
+          _compilerOptions = opts
+        }
+
+    functionInfos :: HashMap FunctionId FunctionInfo
+    functionInfos = hashMap (run (runInputNaturals (toList <$> userFunctions)))
+
+    userFunctions :: (Members '[Input Natural] r) => Sem r (NonEmpty (FunctionId, FunctionInfo))
+    userFunctions = forM allFuns $ \CompilerFunction {..} -> do
+      i <- input
+      return
+        ( _compilerFunctionName,
+          FunctionInfo
+            { _functionInfoPath = indexInStack FunctionsLibrary i,
+              _functionInfoArity = _compilerFunctionArity
+            }
+        )
+
+builtinFunction :: BuiltinFunctionId -> CompilerFunction
+builtinFunction = \case
+  BuiltinAppendRights ->
+    CompilerFunction
+      { _compilerFunctionName = BuiltinFunction BuiltinAppendRights,
+        _compilerFunctionArity = 2, -- args: n pos
+        _compilerFunction = do
+          push (OpAddress # pathToArg 0)
+          pow2
+          push (OpAddress # pathToArg 1)
+          pushNat 1
+          add
+          mul
+          dec
+          asmReturn
+      }
+  BuiltinPow2 ->
+    CompilerFunction
+      { _compilerFunctionName = BuiltinFunction BuiltinPow2,
+        _compilerFunctionArity = 1,
+        _compilerFunction = do
+          pushNat 1 -- acc
+          push (OpAddress # pathToArg 0)
+          callFun (BuiltinFunction BuiltinPow2Go) 2
+          asmReturn
+      }
+  BuiltinPow2Go ->
+    CompilerFunction
+      { _compilerFunctionName = BuiltinFunction BuiltinPow2Go,
+        _compilerFunctionArity = 2, -- args: n acc
+        _compilerFunction = do
+          push (OpAddress # pathToArg 1)
+          push (OpAddress # pathToArg 0)
+          copyTopFromTo ValueStack AuxStack
+          pushNat 0
+          testEq
+          let baseCase :: (Members '[Compiler] r) => Sem r ()
+              baseCase = popFrom AuxStack >> asmReturn
+              recCase :: (Members '[Compiler] r) => Sem r ()
+              recCase = do
+                pushNat 2
+                mul
+                moveTopFromTo AuxStack ValueStack
+                dec
+                callHelper True (Just (BuiltinFunction BuiltinPow2Go)) 2
+          branch baseCase recCase
+      }
+
+callEnum :: (Enum funId, Members '[Compiler] r) => funId -> Natural -> Sem r ()
+callEnum = callFun . UserFunction . Asm.defaultSymbol . fromIntegral . fromEnum
+
+callFun :: (Members '[Compiler] r) => FunctionId -> Natural -> Sem r ()
+callFun = callHelper False . Just
+
+tcallFun :: (Members '[Compiler] r) => FunctionId -> Natural -> Sem r ()
+tcallFun = callHelper True . Just
+
+getFunctionPath' :: (Members '[Reader CompilerCtx] r) => FunctionId -> Sem r Path
+getFunctionPath' funName = asks (^?! compilerFunctionInfos . at funName . _Just . functionInfoPath)
+
+-- | obj[relPath] := newVal
+-- relPath is relative to obj
+replaceSubterm :: Term Natural -> Path -> Term Natural -> Term Natural
+replaceSubterm obj relPath newVal = OpReplace # (relPath # newVal) # obj
+
+evaluated :: Term Natural -> Term Natural
+evaluated t = OpApply # (OpAddress # emptyPath) # t
+
+-- | The same as replaceSubterm but the path is a cell that is evaluated.
+-- i.e. replaceSubterm a p b = replaceSubterm' a (quote p) b
+replaceSubterm' :: Term Natural -> Term Natural -> Term Natural -> Term Natural
+replaceSubterm' obj relPath newVal =
+  evaluated $ (OpQuote # OpReplace) # ((relPath # (OpQuote # newVal)) # (OpQuote # obj))
+
+sre :: (Members '[Output (Term Natural), Reader CompilerCtx] r) => Sem (Compiler ': r) x -> Sem r x
+sre = subsume . re
+
+-- | funName is Nothing when we call a closure at the top of the stack
+callHelper' ::
+  (Members '[Output (Term Natural), Reader CompilerCtx] r) =>
+  Bool ->
+  Maybe FunctionId ->
+  Natural ->
+  Sem r ()
+callHelper' isTail funName funArgsNum = do
+  let isClosure = isNothing funName
+  -- 1. Obtain the path to the function
+  funPath <- maybe (return (topOfStack ValueStack)) getFunctionPath' funName
+
+  -- 2.
+  --   i. Take a copy of the value stack without the arguments to the function
+  --   ii. Push this copy to the call stack
+  let storeOnStack
+        | isTail = replaceOnStack
+        | otherwise = pushOnStack
+      numToPop
+        | isClosure = 1 + funArgsNum
+        | otherwise = funArgsNum
+
+  unless isTail $ do
+    let frame = makeActivationFrame $ \case
+          ActivationFrameValueStack -> stackPop ValueStack numToPop
+          ActivationFrameTempStack -> OpAddress # stackPath TempStack
+          ActivationFrameAuxStack -> OpAddress # stackPath AuxStack
+    output (pushOnStack FrameStack frame)
+
+  -- 3.
+  --  i. Take a copy of the function from the function library
+  --  ii. Replace its argument area with the arguments from the value stack
+  --  iii. Push this copy to the current function stack
+
+  -- Setup function to call with its arguments
+  -- given n, we compute [R..R] of length n
+  if
+      | isClosure -> sre $ do
+          push (OpQuote # toNock ([] :: Path))
+          push (OpAddress # indexInStack ValueStack 1 ++ closurePath ClosureArgsNum)
+          appendRights
+          moveTopFromTo ValueStack AuxStack
+          let closurepath = topOfStack ValueStack
+              posOfArgsNil = OpAddress # topOfStack AuxStack
+              oldArgs = OpAddress # closurepath ++ closurePath ClosureArgs
+              xtraArgs = stackSliceAsList ValueStack 1 funArgsNum
+              allArgs = replaceSubterm' oldArgs posOfArgsNil xtraArgs
+              funCode = OpAddress # closurepath ++ closurePath ClosureCode
+              funWithArgs = replaceSubterm funCode (functionPath FunctionArgs) allArgs
+          output (storeOnStack CurrentFunction funWithArgs)
+          popFrom AuxStack
+      | otherwise -> do
+          let funWithArgs = replaceSubterm (OpAddress # funPath) (functionPath FunctionArgs) (stackTake ValueStack funArgsNum)
+          output (storeOnStack CurrentFunction funWithArgs)
+
+  -- 4. Replace the value stack with nil
+  output (resetStack ValueStack)
+  output (resetStack TempStack)
+  output (resetStack AuxStack)
+
+  -- 5. Evaluate the function in the context of the whole nock stack
+  -- 6. See documentation for asmReturn'
+  output (OpCall # ((topOfStack CurrentFunction ++ functionPath FunctionCode) # (OpAddress # emptyPath)))
+
+asmReturn' :: (Members '[Output (Term Natural), Reader CompilerCtx] r) => Sem r ()
+asmReturn' = do
+  -- Restore the previous value stack (created in call'.2.). i.e copy the previous value stack
+  -- from the call stack and push the result (the head of the current value stack) to it.
+
+  output
+    ( replaceStack
+        ValueStack
+        ( (OpAddress # topOfStack ValueStack)
+            # (OpAddress # topOfStack FrameStack ++ activationFramePath ActivationFrameValueStack)
+        )
+    )
+
+  output
+    ( replaceStack
+        TempStack
+        (OpAddress # topOfStack FrameStack ++ activationFramePath ActivationFrameTempStack)
+    )
+
+  output
+    ( replaceStack
+        AuxStack
+        (OpAddress # topOfStack FrameStack ++ activationFramePath ActivationFrameAuxStack)
+    )
+
+  -- discard the 'activation' frame
+  sre $ do
+    popFrom FrameStack
+    popFrom CurrentFunction
+
+testEq :: (Members '[Compiler] r) => Sem r ()
+testEq = testEqOn ValueStack
+
+testEqOn' :: (Members '[Output (Term Natural)] r) => StackId -> Sem r ()
+testEqOn' s = output (replaceOnStackN 2 s (OpEq # stackSliceAsCell s 0 1))
+
+dumpStack :: (Members '[Compiler] r) => StackId -> Sem r ()
+dumpStack t = traceTerm (OpAddress # stackPath t)
+
+traceTerm' :: (Members '[Output (Term Natural)] r) => Term Natural -> Sem r ()
+traceTerm' t =
+  let iden = OpAddress # ([] :: Path)
+   in output (OpTrace # t # iden)
+
+incrementOn' :: (Members '[Output (Term Natural)] r) => StackId -> Sem r ()
+incrementOn' s = output (replaceOnStack s (OpInc # stackSliceAsCell s 0 0))
+
+callStdlib :: (Members '[Compiler] r) => StdlibFunction -> Sem r ()
+callStdlib = callStdlibOn ValueStack
+
+callStdlibOn' :: (Members '[Output (Term Natural)] r) => StackId -> StdlibFunction -> Sem r ()
+callStdlibOn' s f = do
+  let fNumArgs = stdlibNumArgs f
+      fPath = stdlibPath f
+      decodeFn = OpCall # (fPath # (OpAddress # stackPath StandardLibrary))
+      arguments = OpSequence # (OpAddress # [R]) # stdlibStackTake s fNumArgs
+      extractResult = (OpAddress # [L]) # (OpAddress # [R, R])
+      callFn = OpPush # (OpCall # [L] # (OpReplace # ([R, L] # arguments) # (OpAddress # [L]))) # extractResult
+
+  output (OpPush # decodeFn # callFn)
+  output (replaceTopStackN fNumArgs s)
+  where
+    stdlibStackTake :: StackId -> Natural -> Term Natural
+    stdlibStackTake sn n =
+      foldTerms
+        ( nonEmpty'
+            (take (fromIntegral n) [OpAddress # indexInStack sn i | i <- [0 ..]])
+        )
+
+save' ::
+  (Functor f, Members '[Output (Term Natural), Reader CompilerCtx] r) =>
+  Bool ->
+  m () ->
+  Sem (WithTactics Compiler f m r) (f ())
+save' isTail m = do
+  pushOntoH TempStack (OpAddress # topOfStack ValueStack)
+  popFromH ValueStack
+  runT m >>= raise . execCompilerList >>= mapM_ output >>= pureT
+  if
+      | isTail -> pureT ()
+      | otherwise -> popFromH TempStack
+
+builtinTagToTerm :: Asm.BuiltinDataTag -> Term Natural
+builtinTagToTerm = \case
+  Asm.TagTrue -> nockBoolLiteral True
+  Asm.TagFalse -> nockBoolLiteral False
+  Asm.TagReturn -> impossible
+  Asm.TagBind -> impossible
+  Asm.TagWrite -> impossible
+  Asm.TagReadLn -> impossible
+
+constructorTagToTerm :: Asm.Tag -> Term Natural
+constructorTagToTerm = \case
+  Asm.UserTag t -> OpQuote # toNock (fromIntegral (t ^. Asm.tagUserWord) :: Natural)
+  Asm.BuiltinTag b -> builtinTagToTerm b
+
+caseCmd ::
+  (Members '[Compiler] r) =>
+  Maybe (Sem r ()) ->
+  [(Asm.Tag, Sem r ())] ->
+  Sem r ()
+caseCmd defaultBranch = \case
+  [] -> sequence_ defaultBranch
+  (tag, b) : bs -> do
+    -- push the constructor tag at the top
+    push (OpAddress # topOfStack ValueStack ++ constructorPath ConstructorTag)
+    push (constructorTagToTerm tag)
+    testEq
+    branch b (caseCmd defaultBranch bs)
+
+branch' ::
+  (Functor f, Members '[Output (Term Natural), Reader CompilerCtx] r) =>
+  m () ->
+  m () ->
+  Sem (WithTactics Compiler f m r) (f ())
+branch' t f = do
+  termT <- runT t >>= raise . execCompiler . (pop >>)
+  termF <- runT f >>= raise . execCompiler . (pop >>)
+  (output >=> pureT) (OpIf # (OpAddress # topOfStack ValueStack) # termT # termF)
+
+getFunctionArity' :: (Members '[Reader CompilerCtx] r) => FunctionId -> Sem r Natural
+getFunctionArity' s = asks (^?! compilerFunctionInfos . at s . _Just . functionInfoArity)
+
+getConstructorArity' :: (Members '[Reader CompilerCtx] r) => Asm.Tag -> Sem r Natural
+getConstructorArity' tag = asks (^?! compilerConstructorArities . at tag . _Just)
+
+re :: (Member (Reader CompilerCtx) r) => Sem (Compiler ': r) a -> Sem (Output (Term Natural) ': r) a
+re = reinterpretH $ \case
+  PushOnto s n -> pushOntoH s n
+  PopFromN n s -> popFromNH n s
+  PopNAndPushOnto s n t -> popNAndPushOnto' s n t >>= pureT
+  Verbatim s -> outputT s
+  TraceTerm s -> whenM (asks (^. compilerOptions . compilerOptionsEnableTrace)) (traceTerm' s) >>= pureT
+  CallHelper isTail funName funArgsNum -> callHelper' isTail funName funArgsNum >>= pureT
+  IncrementOn s -> incrementOn' s >>= pureT
+  Branch t f -> branch' t f
+  Save isTail m -> save' isTail m
+  CallStdlibOn s f -> callStdlibOn' s f >>= pureT
+  AsmReturn -> asmReturn' >>= pureT
+  TestEqOn s -> testEqOn' s >>= pureT
+  GetConstructorArity s -> getConstructorArity' s >>= pureT
+  GetFunctionArity s -> getFunctionArity' s >>= pureT
+  GetFunctionPath s -> getFunctionPath' s >>= pureT
+  Crash -> outputT (OpAddress # OpAddress # OpAddress)
+
+outputT :: (Functor f, Member (Output (Term Natural)) r) => Term Natural -> Sem (WithTactics e f m r) (f ())
+outputT = output >=> pureT
+
+pushOntoH ::
+  (Functor f, Member (Output (Term Natural)) r) =>
+  StackId ->
+  Term Natural ->
+  Sem (WithTactics e f m r) (f ())
+pushOntoH s n = outputT (pushOnStack s n)
+
+popFromH ::
+  (Functor f, Member (Output (Term Natural)) r) =>
+  StackId ->
+  Sem (WithTactics e f m r) (f ())
+popFromH s = outputT (popStack s)
+
+popFromNH ::
+  (Functor f, Member (Output (Term Natural)) r) =>
+  Natural ->
+  StackId ->
+  Sem (WithTactics e f m r) (f ())
+popFromNH n s = outputT (popStackN n s)
+
+mul :: (Members '[Compiler] r) => Sem r ()
+mul = mulOn ValueStack
+
+mulOn :: (Members '[Compiler] r) => StackId -> Sem r ()
+mulOn s = callStdlibOn s StdlibMul
+
+addOn :: (Members '[Compiler] r) => StackId -> Sem r ()
+addOn s = callStdlibOn s StdlibAdd
+
+-- | arg order: push path >> push n
+appendRights :: (Members '[Compiler] r) => Sem r ()
+appendRights = callFun (BuiltinFunction BuiltinAppendRights) 2
+
+pow2 :: (Members '[Compiler] r) => Sem r ()
+pow2 = callFun (BuiltinFunction BuiltinPow2) 1
+
+add :: (Members '[Compiler] r) => Sem r ()
+add = addOn ValueStack
+
+dec :: (Members '[Compiler] r) => Sem r ()
+dec = callStdlib StdlibDec
+
+increment :: (Members '[Compiler] r) => Sem r ()
+increment = incrementOn ValueStack
+
+popFrom :: (Members '[Compiler] r) => StackId -> Sem r ()
+popFrom = popFromN 1
+
+popN :: (Members '[Compiler] r) => Natural -> Sem r ()
+popN n = popFromN n ValueStack
+
+pop :: (Members '[Compiler] r) => Sem r ()
+pop = popFrom ValueStack
+
+stackPop :: StackId -> Natural -> Term Natural
+stackPop s n = OpAddress # pathInStack s (replicate n R)
+
+stackTake :: StackId -> Natural -> Term Natural
+stackTake sn n = remakeList (take (fromIntegral n) [OpAddress # indexInStack sn i | i <- [0 ..]])
+
+stackSliceHelper :: StackId -> Natural -> Natural -> NonEmpty (Term Natural)
+stackSliceHelper sn fromIx toIx = fromMaybe err (nonEmpty [OpAddress # indexInStack sn i | i <- indices])
+  where
+    err :: a
+    err = error "impossible: empty slice"
+    indices
+      | fromIx <= toIx = [fromIx .. toIx]
+      | otherwise = impossible
+
+stackSliceAsCell :: StackId -> Natural -> Natural -> Term Natural
+stackSliceAsCell sn a b = foldTerms (stackSliceHelper sn a b)
+
+-- | Takes a slice of a stack. Both indices are inclusive
+stackSliceAsList :: StackId -> Natural -> Natural -> Term Natural
+stackSliceAsList sn fromIx toIx = remakeList (stackSliceHelper sn fromIx toIx)
+
+pushOnStack :: StackId -> Term Natural -> Term Natural
+pushOnStack sn t = OpPush # t # moveTopToStack
+  where
+    moveTopToStack :: Term Natural
+    moveTopToStack =
+      remakeList
+        [ let p = OpAddress # (R : stackPath s)
+           in if
+                  | sn == s -> (OpAddress # indexStack 0) # p
+                  | otherwise -> p
+          | s <- allElements
+        ]
+
+popNAndPushOnto' :: (Member (Output (Term Natural)) r) => StackId -> Natural -> Term Natural -> Sem r ()
+popNAndPushOnto' s num t = output (replaceOnStackN num s t)
+
+replaceOnStackN :: Natural -> StackId -> Term Natural -> Term Natural
+replaceOnStackN numToReplace s t = OpPush # t # replaceTopStackN numToReplace s
+
+replaceOnStack :: StackId -> Term Natural -> Term Natural
+replaceOnStack = replaceOnStackN 1
+
+popStack :: StackId -> Term Natural
+popStack = popStackN 1
+
+popStackN :: Natural -> StackId -> Term Natural
+popStackN n sn =
+  remakeList
+    [ let p = stackPath s
+          a
+            | sn == s = p ++ replicate n R
+            | otherwise = p
+       in OpAddress # a
+      | s <- allElements
+    ]
+
+replaceStack :: StackId -> Term Natural -> Term Natural
+replaceStack sn t =
+  remakeList
+    [ if
+          | sn == s -> t
+          | otherwise -> OpAddress # (stackPath s)
+      | s <- allElements
+    ]
+
+resetStack :: StackId -> Term Natural
+resetStack sn = replaceStack sn (OpQuote # nockNil')
+
+replaceTopStackN :: Natural -> StackId -> Term Natural
+replaceTopStackN n sn =
+  remakeList
+    [ let p = R : stackPath s
+       in if
+              | sn == s -> (OpAddress # indexStack 0) # (OpAddress # p ++ replicate n R)
+              | otherwise -> OpAddress # p
+      | s <- allElements
+    ]
+
+replaceTopStack :: StackId -> Term Natural
+replaceTopStack = replaceTopStackN 1
+
+pushNat :: (Member Compiler r) => Natural -> Sem r ()
+pushNat = pushNatOnto ValueStack
+
+pushNatOnto :: (Member Compiler r) => StackId -> Natural -> Sem r ()
+pushNatOnto s n = pushOnto s (OpQuote # toNock n)
+
+compileAndRunNock :: CompilerOptions -> ConstructorArities -> [CompilerFunction] -> CompilerFunction -> Term Natural
+compileAndRunNock opts constrs funs = run . ignoreOutput @(Term Natural) . compileAndRunNock' opts constrs funs
+
+compileAndRunNock' :: (Member (Output (Term Natural)) r) => CompilerOptions -> ConstructorArities -> [CompilerFunction] -> CompilerFunction -> Sem r (Term Natural)
+compileAndRunNock' opts constrs funs mainfun =
+  let Cell nockSubject t = runCompilerWith opts constrs funs mainfun
+   in evalCompiledNock' nockSubject t
+
+evalCompiledNock :: Term Natural -> Term Natural -> Term Natural
+evalCompiledNock stack = run . ignoreOutput @(Term Natural) . evalCompiledNock' stack
+
+evalCompiledNock' :: (Member (Output (Term Natural)) r) => Term Natural -> Term Natural -> Sem r (Term Natural)
+evalCompiledNock' stack mainTerm = do
+  evalT <-
+    runError @(ErrNockNatural Natural)
+      . runError @NockEvalError
+      $ eval stack mainTerm
+  case evalT of
+    Left e -> error (show e)
+    Right ev -> case ev of
+      Left e -> error (show e)
+      Right res -> return res
+
+-- | Used in testing and app
+getStack :: StackId -> Term Natural -> Term Natural
+getStack st m = fromRight' (run (runError @NockEvalError (subTerm m (stackPath st))))
diff --git a/src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs b/src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs
index 5b34a52db4..3f111b2f70 100644
--- 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
diff --git a/src/Juvix/Compiler/Nockma/Translation/FromSource/QQ.hs b/src/Juvix/Compiler/Nockma/Translation/FromSource/QQ.hs
index 5d6ffff438..a79a98312a 100644
--- 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
diff --git a/src/Juvix/Compiler/Pipeline.hs b/src/Juvix/Compiler/Pipeline.hs
index 6e1102875d..e7ccbd7c20 100644
--- 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
 
diff --git a/src/Juvix/Compiler/Reg/Translation/FromAsm.hs b/src/Juvix/Compiler/Reg/Translation/FromAsm.hs
index 2cac5e7ab4..611146db56 100644
--- 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 {..} =
diff --git a/src/Juvix/Data/CodeAnn.hs b/src/Juvix/Data/CodeAnn.hs
index 9ff390128e..298adb9897 100644
--- 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))
diff --git a/src/Juvix/Data/FileExt.hs b/src/Juvix/Data/FileExt.hs
index db94f7d870..1e938c54ae 100644
--- 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
diff --git a/src/Juvix/Parser/Error.hs b/src/Juvix/Parser/Error.hs
index 678e36f223..bd22670205 100644
--- 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
   }
diff --git a/src/Juvix/Prelude/Base.hs b/src/Juvix/Prelude/Base.hs
index 8f4e3050e4..36234af41d 100644
--- 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'
diff --git a/src/Juvix/Prelude/Stream.hs b/src/Juvix/Prelude/Stream.hs
index d300866863..bea8ada198 100644
--- 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
diff --git a/test/Asm/Run/Base.hs b/test/Asm/Run/Base.hs
index c85826efcb..7ce0ff927c 100644
--- 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
diff --git a/test/Nockma.hs b/test/Nockma.hs
index 8b3e3dd737..2ed58b755e 100644
--- 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]
diff --git a/test/Nockma/Compile.hs b/test/Nockma/Compile.hs
new file mode 100644
index 0000000000..88a56939be
--- /dev/null
+++ 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]
diff --git a/test/Nockma/Compile/Asm/Positive.hs b/test/Nockma/Compile/Asm/Positive.hs
new file mode 100644
index 0000000000..0317f7c18a
--- /dev/null
+++ 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))
diff --git a/test/Nockma/Compile/Positive.hs b/test/Nockma/Compile/Positive.hs
new file mode 100644
index 0000000000..6ad525c1b4
--- /dev/null
+++ 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)
+  ]
diff --git a/test/Nockma/Eval/Positive.hs b/test/Nockma/Eval/Positive.hs
index 8455c10466..f2fb036981 100644
--- 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