Translate Judoc comments to Isabelle/HOL (#2958)

* Closes #2891

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

@@ -154,13 +154,15 @@ data Statement
 data Definition = Definition
   { _definitionName :: Name,
     _definitionType :: Type,
-    _definitionBody :: Expression
+    _definitionBody :: Expression,
+    _definitionDocComment :: Maybe Text
   }
 
 data Function = Function
   { _functionName :: Name,
     _functionType :: Type,
-    _functionClauses :: NonEmpty Clause
+    _functionClauses :: NonEmpty Clause,
+    _functionDocComment :: Maybe Text
   }
 
 data Clause = Clause
@@ -170,29 +172,34 @@ data Clause = Clause
 
 data Synonym = Synonym
   { _synonymName :: Name,
-    _synonymType :: Type
+    _synonymType :: Type,
+    _synonymDocComment :: Maybe Text
   }
 
 data Datatype = Datatype
   { _datatypeName :: Name,
     _datatypeParams :: [TypeVar],
-    _datatypeConstructors :: [Constructor]
+    _datatypeConstructors :: [Constructor],
+    _datatypeDocComment :: Maybe Text
   }
 
 data Constructor = Constructor
   { _constructorName :: Name,
-    _constructorArgTypes :: [Type]
+    _constructorArgTypes :: [Type],
+    _constructorDocComment :: Maybe Text
   }
 
 data Record = Record
   { _recordName :: Name,
     _recordParams :: [TypeVar],
-    _recordFields :: [RecordField]
+    _recordFields :: [RecordField],
+    _recordDocComment :: Maybe Text
   }
 
 data RecordField = RecordField
   { _recordFieldName :: Name,
-    _recordFieldType :: Type
+    _recordFieldType :: Type,
+    _recordFieldDocComment :: Maybe Text
   }
 
 makeLenses ''Definition

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

@@ -31,6 +31,26 @@ ppParams = \case
     ps <- mapM ppCode params
     return $ Just $ parens (hsep (punctuate comma ps))
 
+prettyTextComment :: Maybe Text -> Doc Ann
+prettyTextComment = \case
+  Nothing -> ""
+  Just c ->
+    annotate AnnComment "text \\<open>"
+      <> line
+      <> annotate AnnComment (pretty c)
+      <> line
+      <> annotate AnnComment "\\<close>"
+      <> line
+
+prettyComment :: Maybe Text -> Doc Ann
+prettyComment = \case
+  Nothing -> ""
+  Just c ->
+    annotate AnnComment "(* "
+      <> annotate AnnComment (pretty c)
+      <> annotate AnnComment " *)"
+      <> line
+
 instance PrettyCode Name where
   ppCode = return . prettyName False
 
@@ -190,18 +210,20 @@ instance PrettyCode Statement where
 
 instance PrettyCode Definition where
   ppCode Definition {..} = do
+    let comment = prettyTextComment _definitionDocComment
     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
+    let comment = prettyTextComment _functionDocComment
     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 +233,40 @@ instance PrettyCode Clause where
 
 instance PrettyCode Synonym where
   ppCode Synonym {..} = do
+    let comment = prettyTextComment _synonymDocComment
     n <- ppCode _synonymName
     ty <- ppCodeQuoted _synonymType
-    return $ kwTypeSynonym <+> n <+> "=" <> oneLineOrNext ty
+    return $ comment <> kwTypeSynonym <+> n <+> "=" <> oneLineOrNext ty
 
 instance PrettyCode Datatype where
   ppCode Datatype {..} = do
+    let comment = prettyTextComment _datatypeDocComment
     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
+    let comment = prettyComment _constructorDocComment
     n <- ppCode _constructorName
     tys <- mapM ppCodeQuoted _constructorArgTypes
-    return $ hsep (n : tys)
+    return $ comment <> hsep (n : tys)
 
 instance PrettyCode Record where
   ppCode Record {..} = do
+    let comment = prettyTextComment _recordDocComment
     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
+    let comment = prettyComment _recordFieldDocComment
     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

@@ -99,14 +99,16 @@ goModule onlyTypes infoTable Internal.Module {..} =
                 Record
                   { _recordName = _inductiveName,
                     _recordParams = params,
-                    _recordFields = map goRecordField tyargs
+                    _recordFields = map goRecordField tyargs,
+                    _recordDocComment = _inductiveDocComment
                   }
       | otherwise =
           StmtDatatype
             Datatype
               { _datatypeName = _inductiveName,
                 _datatypeParams = params,
-                _datatypeConstructors = map goConstructorDef _inductiveConstructors
+                _datatypeConstructors = map goConstructorDef _inductiveConstructors,
+                _datatypeDocComment = _inductiveDocComment
               }
       where
         params = map goInductiveParameter _inductiveParameters
@@ -118,40 +120,45 @@ goModule onlyTypes infoTable Internal.Module {..} =
     goRecordField Internal.FunctionParameter {..} =
       RecordField
         { _recordFieldName = fromMaybe (defaultName "_") _paramName,
-          _recordFieldType = goType _paramType
+          _recordFieldType = goType _paramType,
+          _recordFieldDocComment = Nothing
         }
 
     goConstructorDef :: Internal.ConstructorDef -> Constructor
     goConstructorDef Internal.ConstructorDef {..} =
       Constructor
         { _constructorName = _inductiveConstructorName,
-          _constructorArgTypes = tyargs
+          _constructorArgTypes = tyargs,
+          _constructorDocComment = _inductiveConstructorDocComment
         }
       where
         tyargs = map (goType . (^. Internal.paramType)) (fst $ Internal.unfoldFunType _inductiveConstructorType)
 
-    goDef :: Name -> Internal.Expression -> [Internal.ArgInfo] -> Maybe Internal.Expression -> Statement
-    goDef name ty argsInfo body = case ty of
+    goDef :: Name -> Internal.Expression -> [Internal.ArgInfo] -> Maybe Internal.Expression -> Maybe Text -> Statement
+    goDef name ty argsInfo body comment = case ty of
       Internal.ExpressionUniverse {} ->
         StmtSynonym
           Synonym
             { _synonymName = name',
-              _synonymType = goType $ fromMaybe (error "unsupported axiomatic type") body
+              _synonymType = goType $ fromMaybe (error "unsupported axiomatic type") body,
+              _synonymDocComment = comment
             }
       _
         | isFunction argnames ty body ->
             StmtFunction
               Function
                 { _functionName = name',
                   _functionType = goType ty,
-                  _functionClauses = goBody argnames ty body
+                  _functionClauses = goBody argnames ty body,
+                  _functionDocComment = comment
                 }
         | otherwise ->
             StmtDefinition
               Definition
                 { _definitionName = name',
                   _definitionType = goType ty,
-                  _definitionBody = maybe ExprUndefined goExpression' body
+                  _definitionBody = maybe ExprUndefined goExpression' body,
+                  _definitionDocComment = comment
                 }
       where
         argnames =
@@ -198,10 +205,10 @@ goModule onlyTypes infoTable Internal.Module {..} =
             (pats, nset', nmap') = goPatternArgs'' (filterTypeArgs 0 ty (toList _lambdaPatterns))
 
     goFunctionDef :: Internal.FunctionDef -> Statement
-    goFunctionDef Internal.FunctionDef {..} = goDef _funDefName _funDefType _funDefArgsInfo (Just _funDefBody)
+    goFunctionDef Internal.FunctionDef {..} = goDef _funDefName _funDefType _funDefArgsInfo (Just _funDefBody) _funDefDocComment
 
     goAxiomDef :: Internal.AxiomDef -> Statement
-    goAxiomDef Internal.AxiomDef {..} = goDef _axiomName _axiomType [] Nothing
+    goAxiomDef Internal.AxiomDef {..} = goDef _axiomName _axiomType [] Nothing _axiomDocComment
 
     goType :: Internal.Expression -> Type
     goType ty = case ty of

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
@@ -19,3 +20,6 @@ ppOut = Print.ppOutNoComments
 
 ppTrace :: (PrettyPrint c) => c -> Text
 ppTrace = toAnsiText True . ppOut traceOptions
+
+ppPrintJudoc :: (SingI s) => Judoc s -> Text
+ppPrintJudoc = toAnsiText False . Print.ppOutJudoc

src/Juvix/Compiler/Concrete/Pretty/Options.hs

@@ -5,23 +5,28 @@ import Juvix.Prelude
 data Options = Options
   { _optShowNameIds :: Bool,
     _optInJudocBlock :: Bool,
-    _optPrintPragmas :: Bool
+    _optPrintPragmas :: Bool,
+    -- | Whether to print judoc annotations without the judoc start string
+    -- (`---`), i.e., print the content of the judoc comments only.
+    _optJudoc :: Bool
   }
 
 defaultOptions :: Options
 defaultOptions =
   Options
     { _optShowNameIds = False,
       _optInJudocBlock = False,
-      _optPrintPragmas = True
+      _optPrintPragmas = True,
+      _optJudoc = False
     }
 
 traceOptions :: Options
 traceOptions =
   Options
     { _optShowNameIds = True,
       _optInJudocBlock = False,
-      _optPrintPragmas = True
+      _optPrintPragmas = True,
+      _optJudoc = False
     }
 
 makeLenses ''Options

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 = ppOutNoComments defaultOptions {_optJudoc = True}

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

@@ -1013,11 +1013,16 @@ instance (SingI s) => PrettyPrint (JudocLine s) where
   ppCode (JudocLine deli atoms) = do
     let start' :: Maybe (Sem r ()) = ppCode <$> deli
         atoms' = mapM_ ppCode atoms
-    start' <?+> atoms'
+    bJudoc <- asks (^. optJudoc)
+    if
+        | bJudoc -> atoms'
+        | otherwise -> start' <?+> atoms'
 
 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
+  ppCode (Judoc groups) = do
+    bJudoc <- asks (^. optJudoc)
+    ppGroups groups <> if bJudoc then mempty else hardline
     where
       ppGroups :: NonEmpty (JudocGroup s) -> Sem r ()
       ppGroups = \case
@@ -1028,15 +1033,23 @@ instance (SingI s) => PrettyPrint (Judoc s) where
             groupSep = line <> extraLine
             extraLine :: Sem r ()
             extraLine = case (g, b) of
-              (JudocGroupLines {}, JudocGroupLines {}) -> ppCode Kw.delimJudocStart <> line
+              (JudocGroupLines {}, JudocGroupLines {}) -> delim <> line
+                where
+                  delim :: Sem r ()
+                  delim = do
+                    bJudoc <- asks (^. optJudoc)
+                    if bJudoc then mempty else ppCode Kw.delimJudocStart
               _ -> return ()
 
 instance (SingI s) => PrettyPrint (JudocBlockParagraph s) where
   ppCode p = do
     let start' = ppCode (p ^. judocBlockParagraphStart)
         contents' = inJudocBlock (vsep2 (ppCode <$> p ^. judocBlockParagraphBlocks))
         endpar' = ppCode (p ^. judocBlockParagraphEnd)
-    start' <+> contents' <+> endpar'
+    bJudoc <- asks (^. optJudoc)
+    if
+        | bJudoc -> contents'
+        | otherwise -> start' <+> contents' <+> endpar'
 
 instance (SingI s) => PrettyPrint (JudocGroup s) where
   ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => JudocGroup s -> Sem r ()

src/Juvix/Compiler/Internal/Extra.hs

@@ -131,6 +131,7 @@ genFieldProjection kind _funDefName _funDefBuiltin mpragmas info fieldIx = do
             mpragmas,
         _funDefBody = body',
         _funDefType = foldFunType (inductiveArgs ++ [saturatedTy]) retTy,
+        _funDefDocComment = Nothing,
         _funDefName,
         _funDefBuiltin
       }