path info message

src/Juvix/Compiler/Nockma/Highlight.hs

@@ -9,7 +9,7 @@ import Juvix.Compiler.Concrete.Data.Highlight (goFaceError, goFaceSemanticItem)
 import Juvix.Compiler.Nockma.Highlight.Base
 import Juvix.Compiler.Nockma.Highlight.Doc
 import Juvix.Compiler.Nockma.Highlight.Input
-import Juvix.Compiler.Nockma.Language
+import Juvix.Compiler.Nockma.Language as Nockma
 import Juvix.Data.CodeAnn
 import Juvix.Emacs.Render
 import Juvix.Emacs.SExp
@@ -25,7 +25,7 @@ buildProperties HighlightInput {..} =
         mapMaybe goFaceSemanticItem _highlightSemanticItems
           <> map goFaceError _highlightErrors,
       _propertiesGoto = [],
-      _propertiesInfo = map goInfoNockOp _highlightNockOps
+      _propertiesInfo = map goInfoNockOp _highlightNockOps <> map goInfoPath _highlightPaths
     }
 
 -- | Used in nockma-mode
@@ -60,15 +60,30 @@ withDocTable body =
       body
     ]
 
+goInfoPath :: WithLoc Nockma.Path -> WithLoc PropertyInfo
+goInfoPath = fmap toProperty
+  where
+    toProperty :: Nockma.Path -> PropertyInfo
+    toProperty p =
+      PropertyInfo
+        { _infoInfo = String txt,
+          _infoInit = format
+        }
+      where
+        (txt, format) = renderEmacs msg
+
+        msg :: Doc CodeAnn
+        msg =
+          ppCodeAnn p
+            <+> kwEquals
+            <+> pretty (encodePath p ^. encodedPath)
+
 goInfoNockOp :: WithLoc NockOp -> WithLoc PropertyInfo
 goInfoNockOp = fmap toProperty
   where
     toProperty :: NockOp -> PropertyInfo
     toProperty o =
       PropertyInfo
-        { _infoInfo = toInfo o,
+        { _infoInfo = Symbol (nockOpKey o),
           _infoInit = nil
         }
-
-    toInfo :: NockOp -> SExp
-    toInfo = Symbol . nockOpKey

src/Juvix/Compiler/Nockma/Highlight/Input.hs

@@ -1,12 +1,14 @@
 module Juvix.Compiler.Nockma.Highlight.Input where
 
 import Juvix.Compiler.Nockma.Language hiding (Path)
+import Juvix.Compiler.Nockma.Language qualified as Nockma
 import Juvix.Data.CodeAnn
 import Juvix.Prelude
 
 data HighlightInput = HighlightInput
   { _highlightSemanticItems :: [SemanticItem],
     _highlightNockOps :: [WithLoc NockOp],
+    _highlightPaths :: [WithLoc Nockma.Path],
     _highlightErrors :: [Interval]
   }
 
@@ -17,6 +19,7 @@ emptyHighlightInput =
   HighlightInput
     { _highlightSemanticItems = [],
       _highlightNockOps = [],
+      _highlightPaths = [],
       _highlightErrors = []
     }
 
@@ -25,19 +28,22 @@ filterInput absPth HighlightInput {..} =
   HighlightInput
     { _highlightSemanticItems = filterByLoc absPth _highlightSemanticItems,
       _highlightNockOps = filterByLoc absPth _highlightNockOps,
+      _highlightPaths = filterByLoc absPth _highlightPaths,
       _highlightErrors = _highlightErrors
     }
 
 data HighlightBuilder :: Effect where
   HighlightItem :: SemanticItem -> HighlightBuilder m ()
   HighlightNockOp :: WithLoc NockOp -> HighlightBuilder m ()
+  HighlightPath :: WithLoc Nockma.Path -> HighlightBuilder m ()
 
 makeSem ''HighlightBuilder
 
 ignoreHighlightBuilder :: Sem (HighlightBuilder ': r) a -> Sem r a
 ignoreHighlightBuilder = interpret $ \case
   HighlightItem {} -> return ()
   HighlightNockOp {} -> return ()
+  HighlightPath {} -> return ()
 
 execHighlightBuilder :: Sem (HighlightBuilder ': r) a -> Sem r (HighlightInput)
 execHighlightBuilder = fmap fst . runHighlightBuilder
@@ -46,3 +52,4 @@ runHighlightBuilder :: Sem (HighlightBuilder ': r) a -> Sem r (HighlightInput, a
 runHighlightBuilder = reinterpret (runState emptyHighlightInput) $ \case
   HighlightItem i -> modify (over highlightSemanticItems (i :))
   HighlightNockOp i -> modify (over highlightNockOps (i :))
+  HighlightPath i -> modify (over highlightPaths (i :))

src/Juvix/Compiler/Nockma/Language/Path.hs

@@ -1,5 +1,6 @@
 module Juvix.Compiler.Nockma.Language.Path where
 
+import Juvix.Data.CodeAnn
 import Juvix.Prelude hiding (Atom, Path)
 import Prelude (show)
 
@@ -56,3 +57,13 @@ instance Semigroup EncodedPath where
 
 instance Monoid EncodedPath where
   mempty = encodePath []
+
+instance PrettyCodeAnn Path where
+  ppCodeAnn = \case
+    [] -> annotate (AnnKind KNameInductive) "S"
+    ds -> mconcatMap ppCodeAnn ds
+
+instance PrettyCodeAnn Direction where
+  ppCodeAnn d = annotate (AnnKind KNameInductive) $ case d of
+    L -> "L"
+    R -> "R"

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

@@ -67,15 +67,10 @@ instance PrettyCode Natural where
   ppCode = return . pretty
 
 instance PrettyCode Path where
-  ppCode = \case
-    [] -> return "S"
-    ds -> mconcatMapM ppCode ds
+  ppCode = return . ppCodeAnn
 
 instance PrettyCode Direction where
-  ppCode =
-    return . \case
-      L -> annotate (AnnKind KNameAxiom) "L"
-      R -> annotate AnnKeyword "R"
+  ppCode = return . ppCodeAnn
 
 instance PrettyCode NockOp where
   ppCode =

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

@@ -214,9 +214,15 @@ direction :: Parser Direction
 direction = choice [directionSymbol (show lr) $> lr | lr <- allElements :: [Direction]]
 
 pPath :: Parser Path
-pPath =
-  directionSymbol "S" $> []
-    <|> NonEmpty.toList <$> some direction
+pPath = do
+  p <-
+    withLoc $
+      choice
+        [ directionSymbol "S" $> [],
+          NonEmpty.toList <$> some direction
+        ]
+  lift (highlightPath p)
+  return (p ^. withLocParam)
 
 atomNat :: Maybe Tag -> Parser (Atom Natural)
 atomNat mtag = do

src/Juvix/Emacs/Render.hs

@@ -1,4 +1,8 @@
-module Juvix.Emacs.Render (renderEmacs, nameKindFace) where
+module Juvix.Emacs.Render
+  ( renderEmacs,
+    nameKindFace,
+  )
+where
 
 import Data.Text qualified as Text
 import Juvix.Data.CodeAnn