Translate Judoc comments to Isabelle/HOL (#2958)

* Closes #2891
2024-11-30 05:42:26 +03:00 · 2024-08-23 20:43:57 +02:00 · 2024-08-23 20:43:57 +02:00 · 9c980d152a
commit 9c980d152a
parent 2b4520c855
15 changed files with 154 additions and 51 deletions
--- a/src/Juvix/Compiler/Backend/Isabelle/Language.hs
+++ b/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
--- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
+++ b/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 =
--- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
+++ b/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,25 +120,28 @@ 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 ->
@ -144,14 +149,16 @@ goModule onlyTypes infoTable Internal.Module {..} =
              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
--- a/src/Juvix/Compiler/Concrete/Pretty.hs
+++ b/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
--- a/src/Juvix/Compiler/Concrete/Pretty/Options.hs
+++ b/src/Juvix/Compiler/Concrete/Pretty/Options.hs
@ -5,7 +5,10 @@ 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
@ -13,7 +16,8 @@ defaultOptions =
  Options
    { _optShowNameIds = False,
      _optInJudocBlock = False,
-      _optPrintPragmas = True
+      _optPrintPragmas = True,
+      _optJudoc = False
    }

 traceOptions :: Options
@ -21,7 +25,8 @@ traceOptions =
  Options
    { _optShowNameIds = True,
      _optInJudocBlock = False,
-      _optPrintPragmas = True
+      _optPrintPragmas = True,
+      _optJudoc = False
    }

 makeLenses ''Options
--- a/src/Juvix/Compiler/Concrete/Print.hs
+++ b/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}
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/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,7 +1033,12 @@ 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
@ -1036,7 +1046,10 @@ instance (SingI s) => PrettyPrint (JudocBlockParagraph s) where
    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 ()
--- a/src/Juvix/Compiler/Internal/Extra.hs
+++ b/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
      }
--- a/src/Juvix/Compiler/Internal/Extra/Base.hs
+++ b/src/Juvix/Compiler/Internal/Extra/Base.hs
@ -231,7 +231,8 @@ instance HasExpressions FunctionDef where
          _funDefCoercion,
          _funDefName,
          _funDefBuiltin,
-          _funDefPragmas
+          _funDefPragmas,
+          _funDefDocComment
        }

 instance HasExpressions MutualStatement where
@ -248,7 +249,8 @@ instance HasExpressions AxiomDef where
        { _axiomType = ty',
          _axiomName,
          _axiomBuiltin,
-          _axiomPragmas
+          _axiomPragmas,
+          _axiomDocComment
        }

 instance HasExpressions InductiveParameter where
@ -274,7 +276,8 @@ instance HasExpressions InductiveDef where
          _inductiveBuiltin,
          _inductivePositive,
          _inductiveTrait,
-          _inductivePragmas
+          _inductivePragmas,
+          _inductiveDocComment
        }

 instance HasExpressions ConstructorDef where
@ -285,7 +288,8 @@ instance HasExpressions ConstructorDef where
        { _inductiveConstructorType = ty',
          _inductiveConstructorName,
          _inductiveConstructorIsRecord,
-          _inductiveConstructorPragmas
+          _inductiveConstructorPragmas,
+          _inductiveConstructorDocComment
        }

 typeAbstraction :: IsImplicit -> Name -> FunctionParameter
@ -803,7 +807,8 @@ simpleFunDef funName ty body =
      _funDefArgsInfo = mempty,
      _funDefTerminating = False,
      _funDefBuiltin = Nothing,
-      _funDefBody = body
+      _funDefBody = body,
+      _funDefDocComment = Nothing
    }

 umapM :: (Monad m, HasExpressions expr) => (Expression -> m Expression) -> expr -> m expr
--- a/src/Juvix/Compiler/Internal/Extra/Clonable.hs
+++ b/src/Juvix/Compiler/Internal/Extra/Clonable.hs
@ -264,5 +264,6 @@ instance Clonable FunctionDef where
            _funDefInstance,
            _funDefCoercion,
            _funDefBuiltin,
-            _funDefPragmas
+            _funDefPragmas,
+            _funDefDocComment
          }
--- a/src/Juvix/Compiler/Internal/Language.hs
+++ b/src/Juvix/Compiler/Internal/Language.hs
@ -85,7 +85,8 @@ data AxiomDef = AxiomDef
  { _axiomName :: AxiomName,
    _axiomBuiltin :: Maybe BuiltinAxiom,
    _axiomType :: Expression,
-    _axiomPragmas :: Pragmas
+    _axiomPragmas :: Pragmas,
+    _axiomDocComment :: Maybe Text
  }
  deriving stock (Data, Generic)

@ -102,7 +103,8 @@ data FunctionDef = FunctionDef
    _funDefCoercion :: Bool,
    _funDefBuiltin :: Maybe BuiltinFunction,
    _funDefArgsInfo :: [ArgInfo],
-    _funDefPragmas :: Pragmas
+    _funDefPragmas :: Pragmas,
+    _funDefDocComment :: Maybe Text
  }
  deriving stock (Eq, Generic, Data)

@ -402,7 +404,8 @@ data InductiveDef = InductiveDef
    _inductiveConstructors :: [ConstructorDef],
    _inductivePositive :: Bool,
    _inductiveTrait :: Bool,
-    _inductivePragmas :: Pragmas
+    _inductivePragmas :: Pragmas,
+    _inductiveDocComment :: Maybe Text
  }
  deriving stock (Data)

@ -410,7 +413,8 @@ data ConstructorDef = ConstructorDef
  { _inductiveConstructorName :: ConstrName,
    _inductiveConstructorType :: Expression,
    _inductiveConstructorIsRecord :: Bool,
-    _inductiveConstructorPragmas :: Pragmas
+    _inductiveConstructorPragmas :: Pragmas,
+    _inductiveConstructorDocComment :: Maybe Text
  }
  deriving stock (Data)

--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@ -19,6 +19,7 @@ import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Extra qualified as Concrete
 import Juvix.Compiler.Concrete.Gen qualified as Gen
 import Juvix.Compiler.Concrete.Language qualified as Concrete
+import Juvix.Compiler.Concrete.Pretty
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error
 import Juvix.Compiler.Internal.Builtins
@ -378,7 +379,8 @@ goFunctionDef FunctionDef {..} = do
  _funDefBody <- goBody
  msig <- asks (^. S.infoNameSigs . at (_funDefName ^. Internal.nameId))
  _funDefArgsInfo <- maybe (return mempty) goNameSignature msig
-  let fun = Internal.FunctionDef {..}
+  let _funDefDocComment = fmap ppPrintJudoc _signDoc
+      fun = Internal.FunctionDef {..}
  whenJust _signBuiltin (checkBuiltinFunction fun . (^. withLocParam))
  return fun
  where
@ -622,7 +624,8 @@ goInductive ty@InductiveDef {..} = do
            _inductiveConstructors = toList _inductiveConstructors',
            _inductivePragmas = _inductivePragmas',
            _inductivePositive = isJust (ty ^. inductivePositive),
-            _inductiveTrait = isJust (ty ^. inductiveTrait)
+            _inductiveTrait = isJust (ty ^. inductiveTrait),
+            _inductiveDocComment = fmap ppPrintJudoc _inductiveDoc
          }
  whenJust ((^. withLocParam) <$> _inductiveBuiltin) (checkBuiltinInductive indDef)
  checkInductiveConstructors indDef
@ -648,7 +651,8 @@ goConstructorDef retTy ConstructorDef {..} = do
      { _inductiveConstructorType = ty',
        _inductiveConstructorName = goSymbol _constructorName,
        _inductiveConstructorIsRecord = isRhsRecord _constructorRhs,
-        _inductiveConstructorPragmas = pragmas'
+        _inductiveConstructorPragmas = pragmas',
+        _inductiveConstructorDocComment = fmap ppPrintJudoc _constructorDoc
      }
  where
    goAdtType :: Concrete.RhsAdt 'Scoped -> Sem r Internal.Expression
@ -1451,7 +1455,8 @@ goAxiom a = do
          { _axiomType = _axiomType',
            _axiomBuiltin = (^. withLocParam) <$> a ^. axiomBuiltin,
            _axiomName = goSymbol (a ^. axiomName),
-            _axiomPragmas = _axiomPragmas'
+            _axiomPragmas = _axiomPragmas',
+            _axiomDocComment = fmap ppPrintJudoc (a ^. axiomDoc)
          }
  whenJust (a ^. axiomBuiltin) (checkBuiltinAxiom axiom . (^. withLocParam))
  return axiom
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
@ -206,7 +206,8 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do
              _inductivePositive,
              _inductiveParameters,
              _inductiveTrait,
-              _inductivePragmas
+              _inductivePragmas,
+              _inductiveDocComment
            }
    checkPositivity (inductiveInfoFromInductiveDef d)
    return d
@ -229,7 +230,8 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do
              { _inductiveConstructorType = cty',
                _inductiveConstructorName,
                _inductiveConstructorIsRecord,
-                _inductiveConstructorPragmas
+                _inductiveConstructorPragmas,
+                _inductiveConstructorDocComment
              }
      registerConstructor c'
      return c'
@ -332,7 +334,8 @@ checkFunctionDef FunctionDef {..} = do
          _funDefInstance,
          _funDefCoercion,
          _funDefBuiltin,
-          _funDefPragmas
+          _funDefPragmas,
+          _funDefDocComment
        }
  when _funDefInstance $
    checkInstanceType funDef
--- a/tests/positive/Isabelle/Program.juvix
+++ b/tests/positive/Isabelle/Program.juvix
@ -67,6 +67,7 @@ push_back {A} (q : Queue A) (x : A) : Queue A :=
      | nil := queue (x :: nil) (qsnd q)
      | q' := queue q' (x :: qsnd q);

+--- Checks if the queue is empty
 is_empty {A} (q : Queue A) : Bool :=
    case qfst q of
      | nil :=
@ -87,7 +88,12 @@ funkcja (n : Nat) : Nat :=
    plusOne (n : Nat) : Nat := n + 1;
  in plusOne n + nat1 + nat2;

-type Either' A B := Left' A | Right' B;
+--- An Either' type
+type Either' A B :=
+  --- Left constructor
+  Left' A
+| --- Right constructor
+  Right' B;

 -- Records

--- a/tests/positive/Isabelle/isabelle/Program.thy
+++ b/tests/positive/Isabelle/isabelle/Program.thy
@ -51,6 +51,9 @@ fun bool_fun :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
 fun bool_fun' :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool" where
  "bool_fun' x y z = (x \<and> y \<or> z)"

+text \<open>
+A type of Queues
+\<close>
 datatype 'A Queue
  = queue "'A list" "'A list"

@ -74,6 +77,9 @@ fun push_back :: "'A Queue \<Rightarrow> 'A \<Rightarrow> 'A Queue" where
       [] \<Rightarrow> queue [x] (qsnd q) |
       q' \<Rightarrow> queue q' (x # qsnd q))"

+text \<open>
+Checks if the queue is empty
+\<close>
 fun is_empty :: "'A Queue \<Rightarrow> bool" where
  "is_empty q =
    (case qfst q of
@ -95,8 +101,13 @@ fun funkcja :: "nat \<Rightarrow> nat" where
                                  n' \<Rightarrow> n' + 1
     in plusOne n + nat1 + nat2)"

+text \<open>
+An Either' type
+\<close>
 datatype ('A, 'B) Either'
-  = Left' 'A |
+  = (* Left constructor *)
+    Left' 'A |
+    (* Right constructor *)
    Right' 'B

 fun bf :: "bool \<Rightarrow> bool \<Rightarrow> bool" where