print Isabelle comments

src/Juvix/Compiler/Backend/Isabelle/Language.hs

@@ -172,7 +172,8 @@ data Clause = Clause
 
 data Synonym = Synonym
   { _synonymName :: Name,
-    _synonymType :: Type
+    _synonymType :: Type,
+    _synonymComment :: Maybe Text
   }
 
 data Datatype = Datatype

src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs

@@ -31,6 +31,11 @@ ppParams = \case
     ps <- mapM ppCode params
     return $ Just $ parens (hsep (punctuate comma ps))
 
+ppComment :: Maybe Text -> Sem r (Doc Ann)
+ppComment = \case
+  Nothing -> return ""
+  Just c -> return $ "text {*" <> line <> pretty c <> line <> "*}" <> line
+
 instance PrettyCode Name where
   ppCode = return . prettyName False
 
@@ -190,18 +195,20 @@ instance PrettyCode Statement where
 
 instance PrettyCode Definition where
   ppCode Definition {..} = do
+    comment <- ppComment _definitionComment
     n <- ppCode _definitionName
     ty <- ppCodeQuoted _definitionType
     body <- ppCode _definitionBody
-    return $ kwDefinition <+> n <+> "::" <+> ty <+> kwWhere <> line <> indent' (dquotes (n <+> "=" <> oneLineOrNext body))
+    return $ comment <> kwDefinition <+> n <+> "::" <+> ty <+> kwWhere <> line <> indent' (dquotes (n <+> "=" <> oneLineOrNext body))
 
 instance PrettyCode Function where
   ppCode Function {..} = do
+    comment <- ppComment _functionComment
     n <- ppCode _functionName
     ty <- ppCodeQuoted _functionType
     cls <- mapM ppCode _functionClauses
     let cls' = punctuate (space <> kwPipe) $ map (dquotes . (n <+>)) (toList cls)
-    return $ kwFun <+> n <+> "::" <+> ty <+> kwWhere <> line <> indent' (vsep cls')
+    return $ comment <> kwFun <+> n <+> "::" <+> ty <+> kwWhere <> line <> indent' (vsep cls')
 
 instance PrettyCode Clause where
   ppCode Clause {..} = do
@@ -211,35 +218,40 @@ instance PrettyCode Clause where
 
 instance PrettyCode Synonym where
   ppCode Synonym {..} = do
+    comment <- ppComment _synonymComment
     n <- ppCode _synonymName
     ty <- ppCodeQuoted _synonymType
-    return $ kwTypeSynonym <+> n <+> "=" <> oneLineOrNext ty
+    return $ comment <> kwTypeSynonym <+> n <+> "=" <> oneLineOrNext ty
 
 instance PrettyCode Datatype where
   ppCode Datatype {..} = do
+    comment <- ppComment _datatypeComment
     n <- ppCode _datatypeName
     params <- ppParams _datatypeParams
     ctrs <- mapM ppCode _datatypeConstructors
-    return $ kwDatatype <+> params <?+> n <> line <> indent' ("=" <+> align (vsep (punctuate (space <> kwPipe) ctrs)))
+    return $ comment <> kwDatatype <+> params <?+> n <> line <> indent' ("=" <+> align (vsep (punctuate (space <> kwPipe) ctrs)))
 
 instance PrettyCode Constructor where
   ppCode Constructor {..} = do
+    comment <- ppComment _constructorComment
     n <- ppCode _constructorName
     tys <- mapM ppCodeQuoted _constructorArgTypes
-    return $ hsep (n : tys)
+    return $ comment <> hsep (n : tys)
 
 instance PrettyCode Record where
   ppCode Record {..} = do
+    comment <- ppComment _recordComment
     n <- ppCode _recordName
     params <- ppParams _recordParams
     fields <- mapM ppCode _recordFields
-    return $ kwRecord <+> params <?+> n <+> "=" <> line <> indent' (vsep fields)
+    return $ comment <> kwRecord <+> params <?+> n <+> "=" <> line <> indent' (vsep fields)
 
 instance PrettyCode RecordField where
   ppCode RecordField {..} = do
+    comment <- ppComment _recordFieldComment
     n <- ppCode _recordFieldName
     ty <- ppCodeQuoted _recordFieldType
-    return $ n <+> "::" <+> ty
+    return $ comment <> n <+> "::" <+> ty
 
 ppImports :: [Name] -> Sem r [Doc Ann]
 ppImports ns =

src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs

@@ -133,7 +133,8 @@ goModule onlyTypes infoTable Internal.Module {..} =
         StmtSynonym
           Synonym
             { _synonymName = name',
-              _synonymType = goType $ fromMaybe (error "unsupported axiomatic type") body
+              _synonymType = goType $ fromMaybe (error "unsupported axiomatic type") body,
+              _synonymComment = comment
             }
       _
         | isFunction argnames ty body ->

src/Juvix/Compiler/Concrete/Pretty.hs

@@ -5,6 +5,7 @@ module Juvix.Compiler.Concrete.Pretty
   )
 where
 
+import Juvix.Compiler.Concrete.Language.Base
 import Juvix.Compiler.Concrete.Pretty.Options
 import Juvix.Compiler.Concrete.Print (PrettyPrint, doc, docNoComments)
 import Juvix.Compiler.Concrete.Print qualified as Print
@@ -22,3 +23,6 @@ ppPrint = toAnsiText True . ppOutDefault
 
 ppTrace :: (PrettyPrint c) => c -> Text
 ppTrace = toAnsiText True . ppOut traceOptions
+
+ppPrintJudoc :: (SingI s) => Judoc s -> Text
+ppPrintJudoc = toAnsiText True . Print.ppOutJudoc

src/Juvix/Compiler/Concrete/Print.hs

@@ -5,6 +5,7 @@ module Juvix.Compiler.Concrete.Print
   )
 where
 
+import Juvix.Compiler.Concrete.Language.Base
 import Juvix.Compiler.Concrete.Pretty.Options
 import Juvix.Compiler.Concrete.Print.Base
 import Juvix.Data.Effect.ExactPrint
@@ -22,3 +23,6 @@ ppOut o cs = mkAnsiText . PPOutput . doc (project o) (Just cs)
 
 ppOutNoComments :: (CanonicalProjection a Options, PrettyPrint c) => a -> c -> AnsiText
 ppOutNoComments o = mkAnsiText . PPOutput . docNoLoc (project o)
+
+ppOutJudoc :: (SingI s) => Judoc s -> AnsiText
+ppOutJudoc = mkAnsiText . PPOutput . docJudoc

src/Juvix/Compiler/Concrete/Print/Base.hs

@@ -69,6 +69,13 @@ instance PrettyPrint KeywordRef where
           $ p
       )
 
+docJudoc :: (SingI s) => Judoc s -> Doc Ann
+docJudoc =
+  run
+    . execExactPrint Nothing
+    . runReader defaultOptions
+    . ppJudoc False
+
 docNoComments :: (PrettyPrint c) => Options -> c -> Doc Ann
 docNoComments = docHelper Nothing
 
@@ -966,21 +973,26 @@ instance (SingI s) => PrettyPrint (JudocLine s) where
         atoms' = mapM_ ppCode atoms
     start' <?+> atoms'
 
+ppJudoc :: forall s r. (SingI s, Members '[ExactPrint, Reader Options] r) => Bool -> Judoc s -> Sem r ()
+ppJudoc bJuvix (Judoc groups) = ppGroups groups <> if bJuvix then hardline else mempty
+  where
+    ppGroups :: NonEmpty (JudocGroup s) -> Sem r ()
+    ppGroups = \case
+      g :| [] -> ppCode g
+      g :| b : bs -> ppCode g <> groupSep <> ppGroups (b :| bs)
+        where
+          groupSep :: Sem r ()
+          groupSep = line <> extraLine
+          extraLine :: Sem r ()
+          extraLine = case (g, b) of
+            (JudocGroupLines {}, JudocGroupLines {}) -> delim <> line
+              where
+                delim = if bJuvix then ppCode Kw.delimJudocStart else mempty
+            _ -> return ()
+
 instance (SingI s) => PrettyPrint (Judoc s) where
   ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => Judoc s -> Sem r ()
-  ppCode (Judoc groups) = ppGroups groups <> hardline
-    where
-      ppGroups :: NonEmpty (JudocGroup s) -> Sem r ()
-      ppGroups = \case
-        g :| [] -> ppCode g
-        g :| b : bs -> ppCode g <> groupSep <> ppGroups (b :| bs)
-          where
-            groupSep :: Sem r ()
-            groupSep = line <> extraLine
-            extraLine :: Sem r ()
-            extraLine = case (g, b) of
-              (JudocGroupLines {}, JudocGroupLines {}) -> ppCode Kw.delimJudocStart <> line
-              _ -> return ()
+  ppCode = ppJudoc True
 
 instance (SingI s) => PrettyPrint (JudocBlockParagraph s) where
   ppCode p = do

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -383,7 +383,7 @@ goFunctionDef FunctionDef {..} = do
   _funDefBody <- goBody
   msig <- asks (^. S.infoNameSigs . at (_funDefName ^. Internal.nameId))
   _funDefArgsInfo <- maybe (return mempty) goNameSignature msig
-  let _funDefComment = fmap ppPrint _signDoc
+  let _funDefComment = fmap ppPrintJudoc _signDoc
       fun = Internal.FunctionDef {..}
   whenJust _signBuiltin (registerBuiltinFunction fun . (^. withLocParam))
   return fun
@@ -621,7 +621,7 @@ goInductive ty@InductiveDef {..} = do
             _inductivePragmas = _inductivePragmas',
             _inductivePositive = isJust (ty ^. inductivePositive),
             _inductiveTrait = isJust (ty ^. inductiveTrait),
-            _inductiveComment = fmap ppPrint _inductiveDoc
+            _inductiveComment = fmap ppPrintJudoc _inductiveDoc
           }
   whenJust ((^. withLocParam) <$> _inductiveBuiltin) (registerBuiltinInductive indDef)
   registerInductiveConstructors indDef
@@ -648,7 +648,7 @@ goConstructorDef retTy ConstructorDef {..} = do
         _inductiveConstructorName = goSymbol _constructorName,
         _inductiveConstructorIsRecord = isRhsRecord _constructorRhs,
         _inductiveConstructorPragmas = pragmas',
-        _inductiveConstructorComment = fmap ppPrint _constructorDoc
+        _inductiveConstructorComment = fmap ppPrintJudoc _constructorDoc
       }
   where
     goAdtType :: Concrete.RhsAdt 'Scoped -> Sem r Internal.Expression
@@ -1390,7 +1390,7 @@ goAxiom a = do
             _axiomBuiltin = (^. withLocParam) <$> a ^. axiomBuiltin,
             _axiomName = goSymbol (a ^. axiomName),
             _axiomPragmas = _axiomPragmas',
-            _axiomComment = fmap ppPrint (a ^. axiomDoc)
+            _axiomComment = fmap ppPrintJudoc (a ^. axiomDoc)
           }
   whenJust (a ^. axiomBuiltin) (registerBuiltinAxiom axiom . (^. withLocParam))
   return axiom