pretty

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

@@ -1,46 +1,31 @@
 module Juvix.Compiler.Nockma.Highlight.Doc (nockOpDoc) where
 
-import Juvix.Compiler.Nockma.Language
+import Juvix.Compiler.Nockma.Highlight.Doc.Base
+import Juvix.Compiler.Nockma.Highlight.Doc.Parser
+import Juvix.Compiler.Nockma.Highlight.Doc.Pretty ()
 import Juvix.Data.CodeAnn
+import Juvix.Prelude
 
-stack :: Doc CodeAnn
-stack = annotate (AnnKind KNameAxiom) "𝒮"
-
--- term1 :: Doc CodeAnn
--- term1 = annotate AnnJudoc "𝓉₁"
-
--- term2 :: Doc CodeAnn
--- term2 = annotate AnnLiteralString "𝓉₂"
-
--- term3 :: Doc CodeAnn
--- term3 = annotate AnnLiteralInteger "𝓉₃"
-
-path1 :: Doc CodeAnn
-path1 = annotate (AnnKind KNameFunction) "𝓅"
-
-evaluatesTo :: Doc CodeAnn
-evaluatesTo = annotate AnnKeyword "⇒"
-
-indexOp :: Doc CodeAnn
-indexOp = annotate AnnKeyword "!"
+example :: Rules
+example =
+  [rules|
+    t * t => t
+    ---
+    s * p => index(s; p)
+    |]
 
 nockOpDoc :: NockOp -> Doc CodeAnn
-nockOpDoc = \case
-  OpAddress ->
-    stack <> ","
-      <+> ppCodeAnn OpAddress
-      <+> path1
-      <+> evaluatesTo
-      <+> stack <> indexOp <> path1
-  OpQuote -> "OpQuote"
-  OpApply -> "OpApply"
-  OpIsCell -> "OpIsCell"
-  OpInc -> "OpInc"
-  OpEq -> "OpEq"
-  OpIf -> "OpIf"
-  OpSequence -> "OpSequence"
-  OpPush -> "OpPush"
-  OpCall -> "OpCall"
-  OpReplace -> "OpReplace"
-  OpHint -> "OpHint"
-  OpScry -> "OpScry"
+nockOpDoc n = ppCodeAnn $ case n of
+  OpAddress -> example
+  OpQuote -> example
+  OpApply -> example
+  OpIsCell -> example
+  OpInc -> example
+  OpEq -> example
+  OpIf -> example
+  OpSequence -> example
+  OpPush -> example
+  OpCall -> example
+  OpReplace -> example
+  OpHint -> example
+  OpScry -> example

src/Juvix/Compiler/Nockma/Highlight/Doc/Base.hs

@@ -7,36 +7,26 @@ where
 
 import Juvix.Compiler.Nockma.Language (NockOp (..))
 import Juvix.Data.Keyword.All
-  ( delimBracketL,
+  ( delimBraceL,
+    delimBraceR,
+    delimBracketL,
     delimBracketR,
     delimParenL,
     delimParenR,
     delimRule,
     delimSemicolon,
     kwAnd,
     kwDoubleArrowR,
+    kwExclamation,
     kwIndex,
+    kwMapsTo,
     kwNockmaLogicAnd,
     kwReplace,
     kwStar,
     kwSucc,
   )
 import Juvix.Prelude
 
-mytext :: Text
-mytext =
-  [__i|
-  s * [t1t2] => t' && s * t3 => t''
-  ---
-  s * [[t1t2]t3] => [t't'']
-  and
-  ---
-  s * [?t] => s!p
-  and
-  ---
-  t'2
-  |]
-
 data Symbol = Symbol
   { _symbolLetter :: Char,
     _symbolSubscript :: Maybe Natural,
@@ -60,7 +50,7 @@ data Atom
   | AtomSuccessor Successor
   deriving stock (Lift)
 
--- | Syntax: succ _successor
+-- | Syntax: succ(_successor)
 newtype Successor = Successor
   { _successor :: Term
   }
@@ -86,6 +76,7 @@ data Term
   | TermCell Cell
   deriving stock (Lift)
 
+-- | Syntax: [l r]
 data Cell = Cell
   { _cellLhs :: Term,
     _cellRhs :: Term

src/Juvix/Compiler/Nockma/Highlight/Doc/Parser/Base.hs

@@ -3,11 +3,10 @@ module Juvix.Compiler.Nockma.Highlight.Doc.Parser.Base where
 import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Nockma.Highlight.Doc.Base
 import Juvix.Compiler.Nockma.Language (atomOps)
+import Juvix.Parser.Error.Base
 import Juvix.Parser.Lexer
 import Juvix.Prelude
 import Juvix.Prelude.Parsing as P
-
-import Juvix.Parser.Error.Base
 import Text.Megaparsec.Char.Lexer (decimal)
 
 type Parse a = Parsec Void Text a
@@ -89,14 +88,16 @@ pPathSymbol = chunk "p" $> PathP
 pIndexAt :: Parse IndexAt
 pIndexAt = do
   kw kwIndex
-  _indexAtBase <- pTerm
-  _indexAtPath <- pPathSymbol
-  return IndexAt {..}
+  parens $ do
+    _indexAtBase <- pTerm
+    kw delimSemicolon
+    _indexAtPath <- pPathSymbol
+    return IndexAt {..}
 
 pSuccessor :: Parse Successor
 pSuccessor = do
   kw kwSucc
-  t <- pTerm
+  t <- parens pTerm
   return
     Successor
       { _successor = t
@@ -111,14 +112,14 @@ pOne = lexeme . void $ chunk "1"
 pAtom :: Parse Atom
 pAtom =
   choice
-    [ AtomSymbol <$> pSymbol,
-      AtomOperator <$> pNockOp,
-      AtomReplace <$> pReplace,
+    [ AtomReplace <$> pReplace,
       AtomIndex <$> pIndexAt,
       AtomStack <$ pStack,
+      AtomOperator <$> pNockOp,
+      AtomSuccessor <$> pSuccessor,
       AtomZero <$ pZero,
       AtomOne <$ pOne,
-      AtomSuccessor <$> pSuccessor
+      AtomSymbol <$> pSymbol
     ]
 
 pCell :: Parse Cell

src/Juvix/Compiler/Nockma/Highlight/Doc/Pretty.hs

@@ -0,0 +1,164 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+
+{-# HLINT ignore "Avoid restricted flags" #-}
+module Juvix.Compiler.Nockma.Highlight.Doc.Pretty () where
+
+import Data.HashMap.Strict qualified as HashMap
+import Data.Text qualified as Text
+import Juvix.Compiler.Nockma.Highlight.Doc.Base
+import Juvix.Data.CodeAnn
+import Juvix.Prelude
+
+data ColorCounter :: Effect where
+  GetColor :: Symbol -> ColorCounter m NameKind
+
+makeSem ''ColorCounter
+
+runColorCounter :: Sem (ColorCounter ': r) a -> Sem r a
+runColorCounter = reinterpret (evalState (mempty :: HashMap Symbol NameKind)) $ \case
+  GetColor sym -> do
+    tbl <- get @(HashMap Symbol NameKind)
+    let m = length tbl
+    case tbl ^. at sym of
+      Just c -> return c
+      Nothing -> do
+        let color = colorAt m
+        modify (HashMap.insert sym color)
+        return color
+    where
+      colorAt :: Int -> NameKind
+      colorAt i = colors !! (i `mod` n)
+
+      n :: Int
+      n
+        | notNull colors = length colors
+        | otherwise = impossibleError "there must be at least one color"
+
+      colors :: [NameKind]
+      colors =
+        [ KNameConstructor,
+          KNameInductive,
+          KNameFunction,
+          KNameTopModule
+        ]
+
+type PP a = a -> Sem '[ColorCounter] (Doc CodeAnn)
+
+instance PrettyCodeAnn Rules where
+  ppCodeAnn = run . runColorCounter . ppRules
+
+ppAtom :: PP Atom
+ppAtom = \case
+  AtomSymbol s -> ppSymbol s
+  AtomOperator n -> ppOperator n
+  AtomReplace r -> ppReplace r
+  AtomIndex i -> ppIndexAt i
+  AtomStack -> return ppStack
+  AtomZero -> return (annotate AnnKeyword "0")
+  AtomOne -> return (annotate AnnKeyword "1")
+  AtomSuccessor s -> ppSuccessor s
+
+ppSymbol :: PP Symbol
+ppSymbol s@Symbol {..} = do
+  c <- getColor s
+  let primes = Text.replicate (fromIntegral _symbolPrimes) "'"
+      sym =
+        Text.singleton _symbolLetter
+          <>? (unicodeSubscript <$> _symbolSubscript)
+          <> primes
+  return
+    . annotate (AnnKind c)
+    . pretty
+    $ sym
+
+ppOperator :: PP NockOp
+ppOperator = return . ppCodeAnn
+
+ppReplace :: PP Replace
+ppReplace Replace {..} = do
+  b' <- ppTerm _replaceBase
+  ix' <- ppPathSymbol _replacePath
+  by' <- ppTerm _replaceBy
+  return $
+    b'
+      <> ppCodeAnn delimBraceL
+      <> ix'
+      <+> ppCodeAnn kwMapsTo
+      <+> by'
+
+ppPathSymbol :: PP PathSymbol
+ppPathSymbol = \case
+  PathP -> return (annotate (AnnKind KNameAxiom) "p")
+
+ppIndexAt :: PP IndexAt
+ppIndexAt IndexAt {..} = do
+  b' <- ppTerm _indexAtBase
+  ix' <- ppPathSymbol _indexAtPath
+  return $
+    b' <+> ppCodeAnn kwExclamation <+> ix'
+
+ppStack :: Doc CodeAnn
+ppStack = annotate (AnnKind KNameLocal) "S"
+
+ppSuccessor :: PP Successor
+ppSuccessor Successor {..} = do
+  t' <- ppTerm _successor
+  return $
+    t' <+> "+" <+> "1"
+
+ppCell :: PP Cell
+ppCell Cell {..} = do
+  l <- ppTerm _cellLhs
+  r <- ppTerm _cellRhs
+  return $
+    ppCodeAnn delimBracketL
+      <> l
+      <+> r
+        <> ppCodeAnn delimBracketR
+
+ppTerm :: PP Term
+ppTerm = \case
+  TermAtom a -> ppAtom a
+  TermCell a -> ppCell a
+
+ppEvalRelation :: PP EvalRelation
+ppEvalRelation EvalRelation {..} = do
+  ctx' <- ppContext _evalContext
+  r' <- ppTerm _evalRhs
+  return $
+    ctx' <+> ppCodeAnn kwDoubleArrowR <+> r'
+
+ppContext :: PP Context
+ppContext Context {..} = do
+  l <- ppTerm _contextLhs
+  r <- ppTerm _contextRhs
+  return $
+    l <+> ppCodeAnn kwStar <+> r
+
+ppRule :: PP Rule
+ppRule Rule {..} = do
+  let sep_ r1 r2 = r1 <+> ppCodeAnn kwNockmaLogicAnd <+> r2
+  conds' <- concatWith sep_ <$> mapM ppEvalRelation _ruleConditions
+  let n = Text.length (toPlainText conds')
+      hrule = pretty (Text.replicate (max n 3) "-")
+  post' <- ppEvalRelation _rulePost
+  return $
+    conds'
+      <> hardline
+      <> hrule
+      <> hardline
+      <> post'
+
+ppRules :: PP Rules
+ppRules Rules {..} = do
+  rules' <- mapM ppRule _rules
+  return $
+    concatWith
+      ( \r1 r2 ->
+          r1
+            <> hardline
+            <> hardline
+            <> r2
+      )
+      rules'

src/Juvix/Data/CodeAnn.hs

@@ -70,6 +70,9 @@ instance HasAnsiBackend (Doc CodeAnn) where
   toAnsiDoc = fmap stylize
   toAnsiStream = fmap stylize . layoutPretty defaultLayoutOptions
 
+instance PrettyCodeAnn Keyword where
+  ppCodeAnn = annotate AnnKeyword . pretty
+
 simpleErrorCodeAnn :: (PrettyCodeAnn msg) => msg -> SimpleError
 simpleErrorCodeAnn = SimpleError . mkAnsiText . ppCodeAnn
 

src/Juvix/Data/Keyword/All.hs

@@ -17,7 +17,7 @@ kwSucc :: Keyword
 kwSucc = asciiKw Str.succ
 
 delimRule :: Keyword
-delimRule = mkDelim Str.replace
+delimRule = mkDelim Str.nockmaRule
 
 kwNockmaLogicAnd :: Keyword
 kwNockmaLogicAnd = asciiKw Str.nockmaLogicAnd

src/Juvix/Prelude/Base/Foundation.hs

@@ -815,3 +815,20 @@ mappendField t1 t2 = appendFieldWith t1 t2 (<>)
 
 appendFieldWith :: t -> t -> (f -> f -> f) -> Lens' t f -> f
 appendFieldWith t1 t2 joinfun l = joinfun (t1 ^. l) (t2 ^. l)
+
+unicodeSubscript :: Natural -> Text
+unicodeSubscript = pack . map toSubscript . show
+  where
+    toSubscript :: Char -> Char
+    toSubscript = \case
+      '0' -> '₀'
+      '1' -> '₁'
+      '2' -> '₂'
+      '3' -> '₃'
+      '4' -> '₄'
+      '5' -> '₅'
+      '6' -> '₆'
+      '7' -> '₇'
+      '8' -> '₈'
+      '9' -> '₉'
+      _ -> impossible