Add parser and printer for pretty nock syntax

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/Nockma/Evaluator.hs

@@ -8,13 +8,6 @@ import Juvix.Compiler.Nockma.Evaluator.Error
 import Juvix.Compiler.Nockma.Language
 import Juvix.Prelude hiding (Atom)
 
-type EncodedPosition = Natural
-
-data Direction = L | R
-  deriving stock (Show)
-
-type Position = [Direction]
-
 asAtom :: (Member (Error NockEvalError) r) => Term a -> Sem r (Atom a)
 asAtom = \case
   TermAtom a -> return a
@@ -30,24 +23,8 @@ asBool t = do
   a <- asAtom t
   return (a == nockTrue)
 
-asPosition :: (Members '[Error NockEvalError, Error (ErrNockNaturalDecoding a)] r, NockNatural a) => Term a -> Sem r Position
-asPosition = asAtom >=> nockNatural >=> decodePosition
-
-decodePosition :: forall r. (Member (Error NockEvalError) r) => EncodedPosition -> Sem r Position
-decodePosition ep = execOutputList (go ep)
-  where
-    go :: EncodedPosition -> Sem (Output Direction ': r) ()
-    go = \case
-      0 -> throw InvalidEncodedPosition
-      1 -> return ()
-      x ->
-        if
-            | even x -> do
-                go (x `div` 2)
-                output L
-            | otherwise -> do
-                go ((x - 1) `div` 2)
-                output R
+asPosition :: (Members '[Error NockEvalError, Error (ErrNockNatural a)] r, NockNatural a) => Term a -> Sem r Position
+asPosition = asAtom >=> nockPosition
 
 subTermT' :: Position -> Traversal (Term a) (Term a) (First (Term a)) (Term a)
 subTermT' pos f = subTermT pos (f . First . Just)
@@ -56,13 +33,13 @@ subTermT :: Position -> Traversal' (Term a) (Term a)
 subTermT = go
   where
     go :: Position -> (forall f. (Applicative f) => (Term a -> f (Term a)) -> Term a -> f (Term a))
-    go = \case
+    go p = case p ^. positionDirections of
       [] -> id
       d : ds -> \g t -> case t of
         TermAtom {} -> pure t
         TermCell c -> case d of
-          L -> (\l' -> TermCell (set cellLeft l' c)) <$> go ds g (c ^. cellLeft)
-          R -> (\r' -> TermCell (set cellRight r' c)) <$> go ds g (c ^. cellRight)
+          L -> (\l' -> TermCell (set cellLeft l' c)) <$> go (Position ds) g (c ^. cellLeft)
+          R -> (\r' -> TermCell (set cellRight r' c)) <$> go (Position ds) g (c ^. cellRight)
 
 subTerm :: (Member (Error NockEvalError) r) => Term a -> Position -> Sem r (Term a)
 subTerm term pos = do
@@ -77,39 +54,21 @@ setSubTerm term pos repTerm =
           | isNothing (getFirst old) -> throw InvalidPosition
           | otherwise -> return new
 
-parseCell :: forall r a. (Members '[Error NockEvalError, Error (ErrNockNaturalDecoding a)] r, NockNatural a) => Cell a -> Sem r (ParsedCell a)
+parseCell :: forall r a. (Members '[Error NockEvalError, Error (ErrNockNatural a)] r, NockNatural a) => Cell a -> Sem r (ParsedCell a)
 parseCell c = case c ^. cellLeft of
   TermAtom a -> ParsedOperatorCell <$> parseOperatorCell a (c ^. cellRight)
   TermCell l -> return (ParsedAutoConsCell (AutoConsCell l (c ^. cellRight)))
   where
     parseOperatorCell :: Atom a -> Term a -> Sem r (OperatorCell a)
     parseOperatorCell a t = do
-      op <- parseOperator a
+      op <- failWithError InvalidOpCode (nockOp a)
       return
         OperatorCell
           { _operatorCellOp = op,
             _operatorCellTerm = t
           }
 
-    parseOperator :: Atom a -> Sem r NockOp
-    parseOperator a = do
-      n <- nockNatural a
-      case n of
-        0 -> return OpAddress
-        1 -> return OpQuote
-        2 -> return OpApply
-        3 -> return OpIsCell
-        4 -> return OpInc
-        5 -> return OpEq
-        6 -> return OpIf
-        7 -> return OpSequence
-        8 -> return OpPush
-        9 -> return OpCall
-        10 -> return OpReplace
-        11 -> return OpHint
-        _ -> throw InvalidOpCode
-
-eval :: forall r a. (Members '[Error NockEvalError, Error (ErrNockNaturalDecoding a)] r, NockNatural a) => Term a -> Term a -> Sem r (Term a)
+eval :: forall r a. (Members '[Error NockEvalError, Error (ErrNockNatural a)] r, NockNatural a) => Term a -> Term a -> Sem r (Term a)
 eval stack = \case
   a@TermAtom {} -> return a
   TermCell c -> do

src/Juvix/Compiler/Nockma/Language.hs

@@ -1,7 +1,9 @@
 module Juvix.Compiler.Nockma.Language where
 
+import Data.HashMap.Strict qualified as HashMap
 import GHC.Base (Type)
 import Juvix.Prelude hiding (Atom)
+import Juvix.Prelude.Pretty
 
 data Term a
   = TermAtom (Atom a)
@@ -14,11 +16,17 @@ data Cell a = Cell
   }
   deriving stock (Show, Eq)
 
-newtype Atom a = Atom
-  { _atom :: a
+data Atom a = Atom
+  { _atom :: a,
+    _atomInfo :: Irrelevant (Maybe AtomHint)
   }
   deriving stock (Show, Eq)
 
+data AtomHint
+  = AtomHintOp
+  | AtomHintPosition
+  | AtomHintBool
+
 data NockOp
   = OpAddress
   | OpQuote
@@ -32,6 +40,27 @@ data NockOp
   | OpCall
   | OpReplace
   | OpHint
+  deriving stock (Bounded, Enum, Eq, Generic)
+
+instance Hashable NockOp
+
+instance Pretty NockOp where
+  pretty = \case
+    OpAddress -> "@"
+    OpQuote -> "quote"
+    OpApply -> "apply"
+    OpIsCell -> "isCell"
+    OpInc -> "suc"
+    OpEq -> "="
+    OpIf -> "if"
+    OpSequence -> "seq"
+    OpPush -> "push"
+    OpCall -> "call"
+    OpReplace -> "replace"
+    OpHint -> "hint"
+
+atomOps :: HashMap Text NockOp
+atomOps = HashMap.fromList [(prettyText op, op) | op <- allElements]
 
 data OperatorCell a = OperatorCell
   { _operatorCellOp :: NockOp,
@@ -47,21 +76,93 @@ data ParsedCell a
   = ParsedOperatorCell (OperatorCell a)
   | ParsedAutoConsCell (AutoConsCell a)
 
+type EncodedPosition = Natural
+
+data Direction = L | R
+  deriving stock (Show)
+
+newtype Position = Position {_positionDirections :: [Direction]}
+  deriving stock (Show)
+
 makeLenses ''Cell
 makeLenses ''Atom
 makeLenses ''OperatorCell
 makeLenses ''AutoConsCell
+makeLenses ''Position
+
+naturalNockOps :: HashMap Natural NockOp
+naturalNockOps = HashMap.fromList [(serializeOp op, op) | op <- allElements]
+
+nockOpsNatural :: HashMap NockOp Natural
+nockOpsNatural = HashMap.fromList (swap <$> HashMap.toList naturalNockOps)
+
+parseOp :: (Member Fail r) => Natural -> Sem r NockOp
+parseOp n = failMaybe (naturalNockOps ^. at n)
+
+serializeOp :: NockOp -> Natural
+serializeOp = \case
+  OpAddress -> 0
+  OpQuote -> 1
+  OpApply -> 2
+  OpIsCell -> 3
+  OpInc -> 4
+  OpEq -> 5
+  OpIf -> 6
+  OpSequence -> 7
+  OpPush -> 8
+  OpCall -> 9
+  OpReplace -> 10
+  OpHint -> 11
+
+decodePosition :: forall r. (Member Fail r) => EncodedPosition -> Sem r Position
+decodePosition ep = Position <$> execOutputList (go ep)
+  where
+    go :: EncodedPosition -> Sem (Output Direction ': r) ()
+    go = \case
+      0 -> fail
+      1 -> return ()
+      x ->
+        if
+            | even x -> do
+                go (x `div` 2)
+                output L
+            | otherwise -> do
+                go ((x - 1) `div` 2)
+                output R
 
 class (Eq a) => NockNatural a where
-  data ErrNockNaturalDecoding a :: Type
-  nockNatural :: (Member (Error (ErrNockNaturalDecoding a)) r) => Atom a -> Sem r Natural
+  type ErrNockNatural a :: Type
+  nockNatural :: (Member (Error (ErrNockNatural a)) r) => Atom a -> Sem r Natural
+  serializeNockOp :: NockOp -> a
+
+  errInvalidOp :: Atom a -> ErrNockNatural a
+
+  errInvalidPosition :: Atom a -> ErrNockNatural a
+
+  nockOp :: (Member (Error (ErrNockNatural a)) r) => Atom a -> Sem r NockOp
+  nockOp atm = do
+    n <- nockNatural atm
+    failWithError (errInvalidOp atm) (parseOp n)
+
+  nockPosition :: (Member (Error (ErrNockNatural a)) r) => Atom a -> Sem r Position
+  nockPosition atm = do
+    n <- nockNatural atm
+    failWithError (errInvalidPosition atm) (decodePosition n)
+
   nockTrue :: Atom a
   nockFalse :: Atom a
   nockSucc :: Atom a -> Atom a
 
+data NockNaturalNaturalError
+  = NaturalInvalidPosition (Atom Natural)
+  | NaturalInvalidOp (Atom Natural)
+
 instance NockNatural Natural where
-  data ErrNockNaturalDecoding Natural = Void
+  type ErrNockNatural Natural = NockNaturalNaturalError
   nockNatural a = return (a ^. atom)
-  nockTrue = Atom 0
-  nockFalse = Atom 1
+  nockTrue = Atom 0 (Irrelevant (Just AtomHintBool))
+  nockFalse = Atom 1 (Irrelevant (Just AtomHintBool))
   nockSucc = over atom succ
+  errInvalidOp atm = NaturalInvalidOp atm
+  errInvalidPosition atm = NaturalInvalidPosition atm
+  serializeNockOp = serializeOp

src/Juvix/Compiler/Nockma/Pretty.hs

@@ -11,7 +11,6 @@ import Juvix.Compiler.Nockma.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/Nockma/Pretty/Base.hs

@@ -22,13 +22,36 @@ class PrettyCode c where
 runPrettyCode :: (PrettyCode c) => Options -> c -> Doc Ann
 runPrettyCode opts = run . runReader opts . ppCode
 
-instance (PrettyCode a) => PrettyCode (Atom a) where
-  ppCode (Atom k) = annotate (AnnKind KNameFunction) <$> ppCode k
+instance (PrettyCode a, NockNatural a) => PrettyCode (Atom a) where
+  ppCode atm@(Atom k h) = runFailDefaultM (annotate (AnnKind KNameFunction) <$> ppCode k)
+    . failFromError @(ErrNockNatural a)
+    $ do
+      h' <- failMaybe (h ^. unIrrelevant)
+      case h' of
+        AtomHintOp -> nockOp atm >>= ppCode
+        AtomHintPosition -> nockPosition atm >>= ppCode
+        AtomHintBool
+          | atm == nockTrue -> return (annotate (AnnKind KNameInductive) "true")
+          | atm == nockFalse -> return (annotate (AnnKind KNameAxiom) "false")
+          | otherwise -> fail
 
 instance PrettyCode Natural where
   ppCode = return . pretty
 
-instance (PrettyCode a) => PrettyCode (Cell a) where
+instance PrettyCode Position where
+  ppCode p = mconcatMapM ppCode (p ^. positionDirections)
+
+instance PrettyCode Direction where
+  ppCode =
+    return . \case
+      L -> annotate (AnnKind KNameAxiom) "L"
+      R -> annotate AnnKeyword "R"
+
+instance PrettyCode NockOp where
+  ppCode =
+    return . annotate (AnnKind KNameFunction) . pretty
+
+instance (PrettyCode a, NockNatural a) => PrettyCode (Cell a) where
   ppCode c = do
     m <- asks (^. optPrettyMode)
     inside <- case m of
@@ -47,7 +70,7 @@ unfoldCell c = c ^. cellLeft :| go [] (c ^. cellRight)
       t@TermAtom {} -> reverse (t : acc)
       TermCell (Cell l r) -> go (l : acc) r
 
-instance (PrettyCode a) => PrettyCode (Term a) where
+instance (PrettyCode a, NockNatural a) => PrettyCode (Term a) where
   ppCode = \case
     TermAtom t -> ppCode t
     TermCell c -> ppCode c

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

@@ -1,5 +1,6 @@
 module Juvix.Compiler.Nockma.Translation.FromSource where
 
+import Data.HashMap.Internal.Strict qualified as HashMap
 import Juvix.Compiler.Nockma.Language qualified as N
 import Juvix.Parser.Error
 import Juvix.Prelude hiding (Atom, many, some)
@@ -17,11 +18,14 @@ runParser f input = case P.runParser term f input of
   Left err -> Left (MegaparsecError err)
   Right t -> Right t
 
+spaceConsumer :: Parser ()
+spaceConsumer = L.space space1 empty empty
+
 lexeme :: Parser a -> Parser a
 lexeme = L.lexeme spaceConsumer
-  where
-    spaceConsumer :: Parser ()
-    spaceConsumer = L.space space1 empty empty
+
+symbol :: Text -> Parser Text
+symbol = L.symbol spaceConsumer
 
 lsbracket :: Parser ()
 lsbracket = void (lexeme "[")
@@ -41,21 +45,31 @@ dottedNatural = lexeme $ do
     digit :: Parser Char
     digit = satisfy isDigit
 
-atom :: Parser (N.Term Natural)
-atom = N.TermAtom . N.Atom <$> dottedNatural
+atomOp :: Parser (N.Atom Natural)
+atomOp = do
+  op' <- choice [symbol opName $> op | (opName, op) <- HashMap.toList N.atomOps]
+  return (N.Atom (N.serializeNockOp op') (Irrelevant (Just N.AtomHintOp)))
+
+atomNat :: Parser (N.Atom Natural)
+atomNat = (\n -> N.Atom n (Irrelevant Nothing)) <$> dottedNatural
+
+atom :: Parser (N.Atom Natural)
+atom = atomOp <|> atomNat
 
-cell :: Parser (N.Term Natural)
+cell :: Parser (N.Cell Natural)
 cell = do
   lsbracket
   firstTerm <- term
   restTerms <- some term
   rsbracket
   return (buildCell firstTerm restTerms)
   where
-    buildCell :: N.Term Natural -> NonEmpty (N.Term Natural) -> N.Term Natural
+    buildCell :: N.Term Natural -> NonEmpty (N.Term Natural) -> N.Cell Natural
     buildCell h = \case
-      x :| [] -> N.TermCell (N.Cell h x)
-      y :| (w : ws) -> N.TermCell (N.Cell h (buildCell y (w :| ws)))
+      x :| [] -> N.Cell h x
+      y :| (w : ws) -> N.Cell h (N.TermCell (buildCell y (w :| ws)))
 
 term :: Parser (N.Term Natural)
-term = atom <|> cell
+term =
+  N.TermAtom <$> atom
+    <|> N.TermCell <$> cell