Fix bugs in the Nockma prettyprinter and parser (#2632)

This pr addresses a number of problems.

1. It fixes a bug where paths were annotated as operations rather than
paths in the parser.
2. It fixes a bug that happened when unfolding cells in the pretty
printer in order to minimize delimiters. It caused the stdlibcall hints
to be ignored for the unfolded arguments.
3. In order to properly test this, we can't ignore the hints for the Eq
instance, so I've changed that.
4. I've introduced the class NockmaEq for nockma semantic equality. This
is used in the evaluator as well as in the semantic tests.
5. I've added a bigger test. I found these bugs while working with this
file.

package.yaml

@@ -122,6 +122,7 @@ ghc-options:
   # Warnings
   - -Weverything
   - -Wno-all-missed-specialisations
+  - -Wno-missed-specialisations
   - -Wno-missing-export-lists
   - -Wno-missing-import-lists
   - -Wno-missing-kind-signatures

src/Juvix/Compiler/Nockma/Evaluator.hs

@@ -23,7 +23,7 @@ asCell = \case
 asBool :: (Members '[Reader EvalCtx, Error (NockEvalError a)] r, NockNatural a) => Term a -> Sem r Bool
 asBool t = do
   a <- asAtom t
-  return (a == nockTrue)
+  return (nockmaEq a nockTrue)
 
 asPath ::
   (Members '[Reader EvalCtx, Error (NockEvalError a), Error (ErrNockNatural a)] r, NockNatural a) =>
@@ -302,7 +302,7 @@ eval inistack initerm =
               r <- evalArg crumbEvalSecond stack (cellTerm ^. cellRight)
               return . TermAtom $
                 if
-                    | l == r -> nockTrue
+                    | nockmaEq l r -> nockTrue
                     | otherwise -> nockFalse
 
             goOpCall :: Sem r (Term a)

src/Juvix/Compiler/Nockma/Language.hs

@@ -53,31 +53,30 @@ data StdlibCall a = StdlibCall
   { _stdlibCallFunction :: StdlibFunction,
     _stdlibCallArgs :: Term a
   }
-
-deriving stock instance (Lift a) => Lift (StdlibCall a)
+  deriving stock (Show, Eq, Lift)
 
 data CellInfo a = CellInfo
-  { _cellInfoLoc :: Maybe Interval,
+  { _cellInfoLoc :: Irrelevant (Maybe Interval),
     _cellInfoCall :: Maybe (StdlibCall a)
   }
-  deriving stock (Lift)
+  deriving stock (Show, Eq, Lift)
 
 data Cell a = Cell'
   { _cellLeft :: Term a,
     _cellRight :: Term a,
-    _cellInfo :: Irrelevant (CellInfo a)
+    _cellInfo :: CellInfo a
   }
   deriving stock (Show, Eq, Lift)
 
 data AtomInfo = AtomInfo
   { _atomInfoHint :: Maybe AtomHint,
-    _atomInfoLoc :: Maybe Interval
+    _atomInfoLoc :: Irrelevant (Maybe Interval)
   }
   deriving stock (Show, Eq, Lift)
 
 data Atom a = Atom
   { _atom :: a,
-    _atomInfo :: Irrelevant AtomInfo
+    _atomInfo :: AtomInfo
   }
   deriving stock (Show, Eq, Lift)
 
@@ -176,7 +175,7 @@ makeLenses ''AtomInfo
 makeLenses ''CellInfo
 
 atomHint :: Lens' (Atom a) (Maybe AtomHint)
-atomHint = atomInfo . unIrrelevant . atomInfoHint
+atomHint = atomInfo . atomInfoHint
 
 termLoc :: Lens' (Term a) (Maybe Interval)
 termLoc f = \case
@@ -184,13 +183,13 @@ termLoc f = \case
   TermCell a -> TermCell <$> cellLoc f a
 
 cellLoc :: Lens' (Cell a) (Maybe Interval)
-cellLoc = cellInfo . unIrrelevant . cellInfoLoc
+cellLoc = cellInfo . cellInfoLoc . unIrrelevant
 
 cellCall :: Lens' (Cell a) (Maybe (StdlibCall a))
-cellCall = cellInfo . unIrrelevant . cellInfoCall
+cellCall = cellInfo . cellInfoCall
 
 atomLoc :: Lens' (Atom a) (Maybe Interval)
-atomLoc = atomInfo . unIrrelevant . atomInfoLoc
+atomLoc = atomInfo . atomInfoLoc . unIrrelevant
 
 naturalNockOps :: HashMap Natural NockOp
 naturalNockOps = HashMap.fromList [(serializeOp op, op) | op <- allElements]
@@ -217,7 +216,7 @@ serializeOp = \case
   OpHint -> 11
   OpTrace -> 100
 
-class (Eq a) => NockNatural a where
+class (NockmaEq a) => NockNatural a where
   type ErrNockNatural a :: Type
   nockNatural :: (Member (Error (ErrNockNatural a)) r) => Atom a -> Sem r Natural
   serializeNockOp :: NockOp -> a
@@ -267,11 +266,11 @@ nockBoolLiteral b
 instance NockNatural Natural where
   type ErrNockNatural Natural = NockNaturalNaturalError
   nockNatural a = return (a ^. atom)
-  nockTrue = Atom 0 (Irrelevant (atomHintInfo AtomHintBool))
-  nockFalse = Atom 1 (Irrelevant (atomHintInfo AtomHintBool))
-  nockNil = Atom 0 (Irrelevant (atomHintInfo AtomHintNil))
+  nockTrue = Atom 0 (atomHintInfo AtomHintBool)
+  nockFalse = Atom 1 (atomHintInfo AtomHintBool)
+  nockNil = Atom 0 (atomHintInfo AtomHintNil)
   nockSucc = over atom succ
-  nockVoid = Atom 0 (Irrelevant (atomHintInfo AtomHintVoid))
+  nockVoid = Atom 0 (atomHintInfo AtomHintVoid)
   errInvalidOp atm = NaturalInvalidOp atm
   errInvalidPath atm = NaturalInvalidPath atm
   serializeNockOp = serializeOp
@@ -299,7 +298,7 @@ instance IsNock Natural where
   toNock = TAtom
 
 instance IsNock NockOp where
-  toNock op = toNock (Atom (serializeOp op) (Irrelevant (atomHintInfo AtomHintOp)))
+  toNock op = toNock (Atom (serializeOp op) (atomHintInfo AtomHintOp))
 
 instance IsNock Bool where
   toNock = \case
@@ -307,7 +306,7 @@ instance IsNock Bool where
     True -> toNock (nockTrue @Natural)
 
 instance IsNock Path where
-  toNock pos = TermAtom (Atom (encodePath pos ^. encodedPath) (Irrelevant (atomHintInfo AtomHintPath)))
+  toNock pos = TermAtom (Atom (encodePath pos ^. encodedPath) (atomHintInfo AtomHintPath))
 
 instance IsNock EncodedPath where
   toNock = toNock . decodePath'
@@ -337,7 +336,7 @@ a >># b = TermCell (a >>#. b)
 pattern Cell :: Term a -> Term a -> Cell a
 pattern Cell {_cellLeft', _cellRight'} <- Cell' _cellLeft' _cellRight' _
   where
-    Cell a b = Cell' a b (Irrelevant emptyCellInfo)
+    Cell a b = Cell' a b emptyCellInfo
 
 {-# COMPLETE TCell, TAtom #-}
 
@@ -349,18 +348,43 @@ pattern TCell l r <- TermCell (Cell' l r _)
 pattern TAtom :: a -> Term a
 pattern TAtom a <- TermAtom (Atom a _)
   where
-    TAtom a = TermAtom (Atom a (Irrelevant emptyAtomInfo))
+    TAtom a = TermAtom (Atom a emptyAtomInfo)
 
 emptyCellInfo :: CellInfo a
 emptyCellInfo =
   CellInfo
     { _cellInfoCall = Nothing,
-      _cellInfoLoc = Nothing
+      _cellInfoLoc = Irrelevant Nothing
     }
 
 emptyAtomInfo :: AtomInfo
 emptyAtomInfo =
   AtomInfo
     { _atomInfoHint = Nothing,
-      _atomInfoLoc = Nothing
+      _atomInfoLoc = Irrelevant Nothing
     }
+
+class NockmaEq a where
+  nockmaEq :: a -> a -> Bool
+
+instance NockmaEq Natural where
+  nockmaEq a b = a == b
+
+instance (NockmaEq a) => NockmaEq [a] where
+  nockmaEq a b =
+    case zipExactMay a b of
+      Nothing -> False
+      Just z -> all (uncurry nockmaEq) z
+
+instance (NockmaEq a) => NockmaEq (Atom a) where
+  nockmaEq = nockmaEq `on` (^. atom)
+
+instance (NockmaEq a) => NockmaEq (Term a) where
+  nockmaEq = \cases
+    (TermAtom a) (TermAtom b) -> nockmaEq a b
+    (TermCell a) (TermCell b) -> nockmaEq a b
+    TermCell {} TermAtom {} -> False
+    TermAtom {} TermCell {} -> False
+
+instance (NockmaEq a) => NockmaEq (Cell a) where
+  nockmaEq (Cell l r) (Cell l' r') = nockmaEq l l' && nockmaEq r r'

src/Juvix/Compiler/Nockma/Pretty/Base.hs

@@ -33,8 +33,8 @@ instance (PrettyCode a, NockNatural a) => PrettyCode (Atom a) where
         AtomHintOp -> nockOp atm >>= ppCode
         AtomHintPath -> nockPath atm >>= ppCode
         AtomHintBool
-          | atm == nockTrue -> return (annotate (AnnKind KNameInductive) "true")
-          | atm == nockFalse -> return (annotate (AnnKind KNameAxiom) "false")
+          | nockmaEq atm nockTrue -> return (annotate (AnnKind KNameInductive) "true")
+          | nockmaEq atm nockFalse -> return (annotate (AnnKind KNameAxiom) "false")
           | otherwise -> fail
         AtomHintNil -> return (annotate (AnnKind KNameConstructor) "nil")
         AtomHintVoid -> return (annotate (AnnKind KNameAxiom) "void")
@@ -85,12 +85,14 @@ instance (PrettyCode a, NockNatural a) => PrettyCode (Cell a) where
     return (oneLineOrNextBrackets inside)
 
 unfoldCell :: Cell a -> NonEmpty (Term a)
-unfoldCell c = c ^. cellLeft :| go [] (c ^. cellRight)
+unfoldCell c = c ^. cellLeft :| reverse (go [] (c ^. cellRight))
   where
     go :: [Term a] -> Term a -> [Term a]
-    go acc = \case
-      t@TermAtom {} -> reverse (t : acc)
-      TermCell (Cell l r) -> go (l : acc) r
+    go acc t = case t of
+      TermAtom {} -> t : acc
+      TermCell (Cell' l r i) -> case i ^. cellInfoCall of
+        Nothing -> go (l : acc) r
+        Just {} -> t : acc
 
 instance (PrettyCode a, NockNatural a) => PrettyCode (Term a) where
   ppCode = \case

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

@@ -7,7 +7,7 @@ import Juvix.Compiler.Nockma.Language
 import Juvix.Extra.Strings qualified as Str
 import Juvix.Parser.Error
 import Juvix.Parser.Lexer (onlyInterval, withLoc)
-import Juvix.Prelude hiding (Atom, many, some)
+import Juvix.Prelude hiding (Atom, Path, many, some)
 import Juvix.Prelude.Parsing hiding (runParser)
 import Text.Megaparsec qualified as P
 import Text.Megaparsec.Char.Lexer qualified as L
@@ -82,22 +82,29 @@ atomOp = do
   let info =
         AtomInfo
           { _atomInfoHint = Just AtomHintOp,
-            _atomInfoLoc = Just loc
+            _atomInfoLoc = Irrelevant (Just loc)
           }
-  return (Atom (serializeNockOp op') (Irrelevant info))
+  return (Atom (serializeNockOp op') info)
 
-atomDirection :: Parser (Atom Natural)
-atomDirection = do
-  WithLoc loc dirs <-
-    withLoc $
-      symbol "S" $> []
-        <|> NonEmpty.toList <$> some (choice [symbol "L" $> L, symbol "R" $> R])
+atomPath :: Parser (Atom Natural)
+atomPath = do
+  WithLoc loc path <- withLoc pPath
   let info =
         AtomInfo
-          { _atomInfoHint = Just AtomHintOp,
-            _atomInfoLoc = Just loc
+          { _atomInfoHint = Just AtomHintPath,
+            _atomInfoLoc = Irrelevant (Just loc)
           }
-  return (Atom (serializePath dirs) (Irrelevant info))
+  return (Atom (serializePath path) info)
+
+direction :: Parser Direction
+direction =
+  symbol "L" $> L
+    <|> symbol "R" $> R
+
+pPath :: Parser Path
+pPath =
+  symbol "S" $> []
+    <|> NonEmpty.toList <$> some direction
 
 atomNat :: Parser (Atom Natural)
 atomNat = do
@@ -105,9 +112,9 @@ atomNat = do
   let info =
         AtomInfo
           { _atomInfoHint = Nothing,
-            _atomInfoLoc = Just loc
+            _atomInfoLoc = Irrelevant (Just loc)
           }
-  return (Atom n (Irrelevant info))
+  return (Atom n info)
 
 atomBool :: Parser (Atom Natural)
 atomBool =
@@ -131,7 +138,7 @@ patom :: Parser (Atom Natural)
 patom =
   atomOp
     <|> atomNat
-    <|> atomDirection
+    <|> atomPath
     <|> atomBool
     <|> atomNil
     <|> atomVoid
@@ -150,9 +157,9 @@ cell = do
       info =
         CellInfo
           { _cellInfoCall = c,
-            _cellInfoLoc = Just (lloc <> rloc)
+            _cellInfoLoc = Irrelevant (Just (lloc <> rloc))
           }
-  return (set cellInfo (Irrelevant info) r)
+  return (set cellInfo info r)
   where
     stdlibCall :: Parser (StdlibCall Natural)
     stdlibCall = do

test/Nockma/Compile/Tree/Positive.hs

@@ -37,7 +37,7 @@ runNockmaAssertion hout _main tab = do
     getReturn :: Term Natural -> Maybe (Term Natural)
     getReturn = \case
       TermAtom Nockma.Atom {..}
-        | _atomInfo ^. unIrrelevant . atomInfoHint == Just AtomHintVoid -> Nothing
+        | _atomInfo ^. atomInfoHint == Just AtomHintVoid -> Nothing
       t -> Just t
 
 testDescr :: Tree.PosTest -> TestDescr

test/Nockma/Eval/Positive.hs

@@ -42,7 +42,7 @@ allTests = testGroup "Nockma eval unit positive" (map mk tests)
 eqNock :: Term Natural -> Check ()
 eqNock expected = do
   actual <- ask
-  unless (expected == actual) (err actual)
+  unless (nockmaEq expected actual) (err actual)
   where
     err :: Term Natural -> Check ()
     err actual = do
@@ -56,7 +56,7 @@ eqNock expected = do
 eqTraces :: [Term Natural] -> Check ()
 eqTraces expected = do
   ts <- ask
-  unless (ts == expected) (err ts)
+  unless (nockmaEq ts expected) (err ts)
   where
     err :: [Term Natural] -> Check ()
     err ts = do

test/Nockma/Parse/Positive.hs

@@ -53,5 +53,6 @@ tests =
   [ PosTest "Identity" $(mkRelDir ".") $(mkRelFile "Identity.nock"),
     PosTest "Identity Pretty" $(mkRelDir ".") $(mkRelFile "IdentityPretty.pnock"),
     PosTest "StdlibCall" $(mkRelDir ".") $(mkRelFile "StdlibCall.pnock"),
-    PosTest "Stdlib" $(mkRelDir ".") $(mkRelFile "Stdlib.nock")
+    PosTest "Stdlib" $(mkRelDir ".") $(mkRelFile "Stdlib.nock"),
+    PosTest "Compiled Tree program" $(mkRelDir ".") $(mkRelFile "Compiled.pnock")
   ]