Nockma compile (#2570)

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

## Juvix -> Nockma compilation

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

example.juvix
```
module example;

import Stdlib.Prelude open;

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

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

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

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

```
$ juvix compile -t nockma example.juvix
```

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

```
$ juvix dev nockma eval example.nockma
```

Alternatively you can compile JuvixAsm to Nockma:

```
$ juvix dev asm compile -t nockma example.jva
```

## Tests

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

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

## Next steps

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

---------

Co-authored-by: Paul Cadman <[email protected]>
Co-authored-by: Lukasz Czajka <[email protected]>

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

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 ->

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"

app/Commands/Dev/Asm/Compile/Options.hs

@@ -14,7 +14,8 @@ asmSupportedTargets :: NonEmpty CompileTarget
 asmSupportedTargets =
   NonEmpty.fromList
     [ TargetWasm32Wasi,
-      TargetNative64
+      TargetNative64,
+      TargetNockma
     ]
 
 parseAsmCompileOptions :: Parser AsmCompileOptions

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)

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)

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

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"

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 {..}

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")

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

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 {..}