Fix bugs in the Nockma prettyprinter and parser

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,21 +175,21 @@ 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
   TermAtom a -> TermAtom <$> atomLoc f a
   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,15 +298,15 @@ 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
     False -> toNock (nockFalse @Natural)
     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,32 +82,39 @@ atomOp = do
   let info =
         AtomInfo
           { _atomInfoHint = Just AtomHintOp,
-            _atomInfoLoc = Just loc
+            _atomInfoLoc = Irrelevant (Just loc)
           }
-  return (Atom (serializeNockOp op') (Irrelevant info))
-
-atomDirection :: Parser (Atom Natural)
-atomDirection = do
-  WithLoc loc dirs <-
-    withLoc $
-      symbol "S" $> []
-        <|> NonEmpty.toList <$> some (choice [symbol "L" $> L, symbol "R" $> R])
+  return (Atom (serializeNockOp op') info)
+
+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
   WithLoc loc n <- withLoc dottedNatural
   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")
   ]