Add nockma evaluator (#2564)

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

## Parser / Pretty Printer

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

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

See
https://github.com/anoma/juvix/blob/a6028b0d92e2dff02329ab7f441bf48ccdeb3eb3/src/Juvix/Compiler/Nockma/Language.hs#L79
for the correspondence between pretty Nock and Nock operators.

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

See
https://github.com/anoma/juvix/blob/a6028b0d92e2dff02329ab7f441bf48ccdeb3eb3/src/Juvix/Compiler/Nockma/Language.hs#L177
for the correspondence between pretty Nock path and standard Nock
position.

## Quasi-quoter

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

## REPL

Launch the repl with `juvix dev nockma repl`.

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

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

The subject can be set using `:set-stack`.

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

The subject can be viewed using `:get-stack`.

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

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

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

A list of assignments can be read from a file:

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

* Closes #2557

---------

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>

app/Commands/Dev.hs

@@ -12,6 +12,7 @@ import Commands.Dev.Geb qualified as Geb
 import Commands.Dev.Highlight qualified as Highlight
 import Commands.Dev.Internal qualified as Internal
 import Commands.Dev.MigrateJuvixYaml qualified as MigrateJuvixYaml
+import Commands.Dev.Nockma qualified as Nockma
 import Commands.Dev.Options
 import Commands.Dev.Parse qualified as Parse
 import Commands.Dev.Runtime qualified as Runtime
@@ -33,3 +34,4 @@ runCommand = \case
   DisplayRoot opts -> DisplayRoot.runCommand opts
   JuvixDevRepl opts -> Repl.runCommand opts
   MigrateJuvixYaml opts -> runFilesIO $ MigrateJuvixYaml.runCommand opts
+  Nockma opts -> Nockma.runCommand opts

app/Commands/Dev/Nockma.hs

@@ -0,0 +1,9 @@
+module Commands.Dev.Nockma where
+
+import Commands.Base
+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

app/Commands/Dev/Nockma/Options.hs

@@ -0,0 +1,20 @@
+module Commands.Dev.Nockma.Options where
+
+import Commands.Dev.Nockma.Repl.Options
+import CommonOptions
+
+data NockmaCommand
+  = NockmaRepl NockmaReplOptions
+  deriving stock (Data)
+
+parseNockmaCommand :: Parser NockmaCommand
+parseNockmaCommand = hsubparser commandRepl
+  where
+    commandRepl :: Mod CommandFields NockmaCommand
+    commandRepl = command "repl" replInfo
+
+    replInfo :: ParserInfo NockmaCommand
+    replInfo =
+      info
+        (NockmaRepl <$> parseNockmaReplOptions)
+        (progDesc "Run the nockma repl")

app/Commands/Dev/Nockma/Repl.hs

@@ -0,0 +1,177 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+module Commands.Dev.Nockma.Repl where
+
+import Commands.Base hiding (Atom)
+import Commands.Dev.Nockma.Repl.Options
+import Control.Exception (throwIO)
+import Control.Monad.State.Strict qualified as State
+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.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)
+
+type ReplS = State.StateT ReplState IO
+
+data ReplState = ReplState
+  { _replStateProgram :: Maybe (Program Natural),
+    _replStateStack :: Maybe (Term Natural),
+    _replStateLoadedFile :: Maybe (FilePath)
+  }
+
+type Repl a = Repline.HaskelineT ReplS a
+
+makeLenses ''ReplState
+
+printHelpTxt :: Repl ()
+printHelpTxt = liftIO $ putStrLn helpTxt
+  where
+    helpTxt :: Text =
+      [__i|
+  EXPRESSION                      Evaluate a Nockma expression in the context of the current stack
+  STACK_EXPRESSION / EXPRESSION   Evaluate a Nockma EXPRESSION in the context of STACK_EXPRESSION
+  :load FILE                      Load a file containing Nockma assignments
+  :reload                         Reload the current file
+  :help                           Print help text and describe options
+  :set-stack EXPRESSION           Set the current stack
+  :get-stack                      Print the current stack
+  :dir       NATURAL              Convert a natural number representing a position into a sequence of L and Rs. S means the empty sequence
+  :quit                           Exit the REPL
+          |]
+
+quit :: String -> Repl ()
+quit _ = liftIO (throwIO Interrupt)
+
+printStack :: String -> Repl ()
+printStack _ = Repline.dontCrash $ do
+  stack <- getStack
+  case stack of
+    Nothing -> noStackErr
+    Just s -> liftIO (putStrLn (ppPrint s))
+
+noStackErr :: a
+noStackErr = error "no stack is set. Use :set-stack <TERM> to set a stack."
+
+setStack :: String -> Repl ()
+setStack s = Repline.dontCrash $ do
+  newStack <- readReplTerm s
+  State.modify (set replStateStack (Just newStack))
+
+loadFile :: String -> Repl ()
+loadFile s = Repline.dontCrash $ do
+  State.modify (set replStateLoadedFile (Just s))
+  prog <- readProgram s
+  State.modify (set replStateProgram (Just prog))
+
+reloadFile :: Repl ()
+reloadFile = Repline.dontCrash $ do
+  fp <- State.gets (^. replStateLoadedFile)
+  case fp of
+    Nothing -> error "no file loaded"
+    Just f -> do
+      prog <- readProgram f
+      State.modify (set replStateProgram (Just prog))
+
+options :: [(String, String -> Repl ())]
+options =
+  [ ("quit", quit),
+    ("get-stack", printStack),
+    ("set-stack", setStack),
+    ("load", loadFile),
+    ("reload", const reloadFile),
+    ("dir", direction')
+  ]
+
+banner :: Repline.MultiLine -> Repl String
+banner = \case
+  Repline.MultiLine -> return "... "
+  Repline.SingleLine -> return "nockma> "
+
+getStack :: Repl (Maybe (Term Natural))
+getStack = State.gets (^. replStateStack)
+
+getProgram :: Repl (Maybe (Program Natural))
+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
+      p = run (runFailDefault (error "invalid position") (decodePath (EncodedPath n)))
+  liftIO (putStrLn (ppPrint p))
+
+readTerm :: String -> Repl (Term Natural)
+readTerm s = return (fromMegaParsecError (parseText (strip (pack s))))
+
+readReplTerm :: String -> Repl (Term Natural)
+readReplTerm s = do
+  mprog <- getProgram
+  let t = run $ runError @NockEvalError (fromReplTerm (programAssignments mprog) (fromMegaParsecError (parseReplText (strip (pack s)))))
+  case t of
+    Left e -> error (show e)
+    Right tv -> return tv
+
+readStatement :: String -> Repl (ReplStatement Natural)
+readStatement s = return (fromMegaParsecError (parseReplStatement (strip (pack s))))
+
+evalStatement :: ReplStatement Natural -> Repl ()
+evalStatement = \case
+  ReplStatementAssignment as -> do
+    prog <- fromMaybe (Program []) <$> getProgram
+    let p' = over programStatements (++ [StatementAssignment as]) prog
+    State.modify (set replStateProgram (Just p'))
+  ReplStatementExpression t -> do
+    s <- getStack
+    prog <- getProgram
+    let et =
+          run
+            . runError @(ErrNockNatural Natural)
+            . runError @NockEvalError
+            $ evalRepl prog s t
+    case et of
+      Left e -> error (show e)
+      Right ev -> case ev of
+        Left e -> error (show e)
+        Right res -> liftIO (putStrLn (ppPrint res))
+
+replCommand :: String -> Repl ()
+replCommand input = Repline.dontCrash $ do
+  readStatement input >>= evalStatement
+
+replAction :: ReplS ()
+replAction =
+  Repline.evalReplOpts
+    Repline.ReplOpts
+      { prefix = Just ':',
+        command = replCommand,
+        initialiser = return (),
+        finaliser = return Repline.Exit,
+        multilineCommand = Just "multiline",
+        tabComplete = Repline.Word (\_ -> return []),
+        options,
+        banner
+      }
+
+runCommand :: forall r. (Members '[Embed IO, App] r) => NockmaReplOptions -> Sem r ()
+runCommand _ = embed . (`State.evalStateT` iniState) $ replAction
+  where
+    iniState :: ReplState
+    iniState =
+      ReplState
+        { _replStateStack = Nothing,
+          _replStateProgram = Nothing,
+          _replStateLoadedFile = Nothing
+        }

app/Commands/Dev/Nockma/Repl/Options.hs

@@ -0,0 +1,13 @@
+module Commands.Dev.Nockma.Repl.Options where
+
+import CommonOptions
+
+newtype NockmaReplOptions = NockmaReplOptions
+  { _nockmaReplOptionsStackFile :: Maybe (AppPath File)
+  }
+  deriving stock (Data)
+
+parseNockmaReplOptions :: Parser NockmaReplOptions
+parseNockmaReplOptions = do
+  _nockmaReplOptionsStackFile <- optional (parseInputFile FileExtNock)
+  pure NockmaReplOptions {..}

app/Commands/Dev/Options.hs

@@ -19,6 +19,7 @@ import Commands.Dev.Geb.Options
 import Commands.Dev.Highlight.Options
 import Commands.Dev.Internal.Options
 import Commands.Dev.MigrateJuvixYaml.Options
+import Commands.Dev.Nockma.Options
 import Commands.Dev.Parse.Options
 import Commands.Dev.Repl.Options
 import Commands.Dev.Runtime.Options
@@ -40,6 +41,7 @@ data DevCommand
   | Termination TerminationCommand
   | JuvixDevRepl ReplOptions
   | MigrateJuvixYaml MigrateJuvixYamlOptions
+  | Nockma NockmaCommand
   deriving stock (Data)
 
 parseDevCommand :: Parser DevCommand
@@ -57,7 +59,8 @@ parseDevCommand =
           commandShowRoot,
           commandTermination,
           commandJuvixDevRepl,
-          commandMigrateJuvixYaml
+          commandMigrateJuvixYaml,
+          commandNockma
         ]
     )
 
@@ -146,3 +149,10 @@ commandMigrateJuvixYaml =
     info
       (MigrateJuvixYaml <$> parseMigrateJuvixYaml)
       (progDesc "Migrate juvix.yaml to Package.juvix in the current project")
+
+commandNockma :: Mod CommandFields DevCommand
+commandNockma =
+  command "nockma" $
+    info
+      (Nockma <$> parseNockmaCommand)
+      (progDesc "Subcommands related to the nockma backend")

cntlines.sh

@@ -17,6 +17,7 @@ RUNTIME=$((RUNTIME_C+RUNTIME_VAMPIR+RUNTIME_JVA))
 BACKENDC=$(count src/Juvix/Compiler/Backend/C/)
 GEB=$(count src/Juvix/Compiler/Backend/Geb/)
 VAMPIR=$(count src/Juvix/Compiler/Backend/VampIR/)
+NOCK=$(count src/Juvix/Compiler/Nockma)
 REG=$(count src/Juvix/Compiler/Reg/)
 ASM=$(count src/Juvix/Compiler/Asm/)
 CORE=$(count src/Juvix/Compiler/Core/)
@@ -34,7 +35,7 @@ PRELUDE=$(count src/Juvix/Prelude/)
 STORE=$(count src/Juvix/Compiler/Store/)
 
 FRONT=$((CONCRETE + INTERNAL + BUILTINS + PIPELINE))
-BACK=$((BACKENDC + GEB + VAMPIR + REG + ASM + CORE))
+BACK=$((BACKENDC + GEB + VAMPIR + NOCK + REG + ASM + CORE))
 OTHER=$((APP + STORE + HTML + EXTRA + DATA + PRELUDE))
 TESTS=$(count test/)
 
@@ -49,6 +50,7 @@ echo "Middle and back end: $BACK LOC"
 echo "   VampIR backend: $VAMPIR LOC"
 echo "   GEB backend: $GEB LOC"
 echo "   C backend: $BACKENDC LOC"
+echo "   Nockma: $NOCK LOC"
 echo "   JuvixReg: $REG LOC"
 echo "   JuvixAsm: $ASM LOC"
 echo "   JuvixCore: $CORE LOC"

src/Juvix/Compiler/Backend/VampIR/Pretty/Base.hs

@@ -6,7 +6,6 @@ import Juvix.Compiler.Backend.VampIR.Language
 import Juvix.Compiler.Backend.VampIR.Pretty.Keywords
 import Juvix.Compiler.Backend.VampIR.Pretty.Options
 import Juvix.Data.CodeAnn
-import Juvix.Data.NameKind
 
 class PrettyCode c where
   ppCode :: (Member (Reader Options) r) => c -> Sem r (Doc Ann)

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs

@@ -28,7 +28,6 @@ import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context qualified as
 import Juvix.Compiler.Pipeline.EntryPoint
 import Juvix.Compiler.Store.Scoped.Language as Store
 import Juvix.Data.FixityInfo qualified as FI
-import Juvix.Data.NameKind
 import Juvix.Prelude hiding (scoped)
 
 scopeCheck ::

src/Juvix/Compiler/Internal/Pretty.hs

@@ -11,7 +11,6 @@ import Juvix.Compiler.Internal.Pretty.Options
 import Juvix.Data.PPOutput
 import Juvix.Prelude
 import Prettyprinter.Render.Terminal qualified as Ansi
-import Prettyprinter.Render.Text (renderStrict)
 
 ppOutDefault :: (PrettyCode c) => c -> AnsiText
 ppOutDefault = mkAnsiText . PPOutput . doc defaultOptions

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -34,7 +34,6 @@ import Juvix.Compiler.Store.Language qualified as Store
 import Juvix.Compiler.Store.Scoped.Data.InfoTable qualified as S
 import Juvix.Compiler.Store.Scoped.Language (createExportsTable)
 import Juvix.Compiler.Store.Scoped.Language qualified as S
-import Juvix.Data.NameKind
 import Juvix.Prelude
 import Safe (lastMay)