fix non-top comments

anoma · Aug 19, 2024 · d2e1752 · d2e1752
1 parent d368911
commit d2e1752
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 11 deletions.
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
@@ -31,11 +31,16 @@ ppParams = \case
     ps <- mapM ppCode params
     return $ Just $ parens (hsep (punctuate comma ps))
 
-ppJudocComment :: Maybe Text -> Sem r (Doc Ann)
-ppJudocComment = \case
+ppTextComment :: Maybe Text -> Sem r (Doc Ann)
+ppTextComment = \case
   Nothing -> return ""
   Just c -> return $ annotate AnnComment "text \\<open>" <> line <> annotate AnnComment (pretty c) <> line <> annotate AnnComment "\\<close>" <> line
 
+ppComment :: Maybe Text -> Sem r (Doc Ann)
+ppComment = \case
+  Nothing -> return ""
+  Just c -> return $ annotate AnnComment "(* " <> annotate AnnComment (pretty c) <> annotate AnnComment " *)" <> line
+
 instance PrettyCode Name where
   ppCode = return . prettyName False
 
@@ -195,15 +200,15 @@ instance PrettyCode Statement where
 
 instance PrettyCode Definition where
   ppCode Definition {..} = do
-    comment <- ppJudocComment _definitionComment
+    comment <- ppTextComment _definitionComment
     n <- ppCode _definitionName
     ty <- ppCodeQuoted _definitionType
     body <- ppCode _definitionBody
     return $ comment <> kwDefinition <+> n <+> "::" <+> ty <+> kwWhere <> line <> indent' (dquotes (n <+> "=" <> oneLineOrNext body))
 
 instance PrettyCode Function where
   ppCode Function {..} = do
-    comment <- ppJudocComment _functionComment
+    comment <- ppTextComment _functionComment
     n <- ppCode _functionName
     ty <- ppCodeQuoted _functionType
     cls <- mapM ppCode _functionClauses
@@ -218,37 +223,37 @@ instance PrettyCode Clause where
 
 instance PrettyCode Synonym where
   ppCode Synonym {..} = do
-    comment <- ppJudocComment _synonymComment
+    comment <- ppTextComment _synonymComment
     n <- ppCode _synonymName
     ty <- ppCodeQuoted _synonymType
     return $ comment <> kwTypeSynonym <+> n <+> "=" <> oneLineOrNext ty
 
 instance PrettyCode Datatype where
   ppCode Datatype {..} = do
-    comment <- ppJudocComment _datatypeComment
+    comment <- ppTextComment _datatypeComment
     n <- ppCode _datatypeName
     params <- ppParams _datatypeParams
     ctrs <- mapM ppCode _datatypeConstructors
     return $ comment <> kwDatatype <+> params <?+> n <> line <> indent' ("=" <+> align (vsep (punctuate (space <> kwPipe) ctrs)))
 
 instance PrettyCode Constructor where
   ppCode Constructor {..} = do
-    comment <- ppJudocComment _constructorComment
+    comment <- ppComment _constructorComment
     n <- ppCode _constructorName
     tys <- mapM ppCodeQuoted _constructorArgTypes
     return $ comment <> hsep (n : tys)
 
 instance PrettyCode Record where
   ppCode Record {..} = do
-    comment <- ppJudocComment _recordComment
+    comment <- ppTextComment _recordComment
     n <- ppCode _recordName
     params <- ppParams _recordParams
     fields <- mapM ppCode _recordFields
     return $ comment <> kwRecord <+> params <?+> n <+> "=" <> line <> indent' (vsep fields)
 
 instance PrettyCode RecordField where
   ppCode RecordField {..} = do
-    comment <- ppJudocComment _recordFieldComment
+    comment <- ppComment _recordFieldComment
     n <- ppCode _recordFieldName
     ty <- ppCodeQuoted _recordFieldType
     return $ comment <> n <+> "::" <+> ty

diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix
@@ -89,7 +89,11 @@ funkcja (n : Nat) : Nat :=
   in plusOne n + nat1 + nat2;
 
 --- An Either' type
-type Either' A B := Left' A | Right' B;
+type Either' A B :=
+  --- Left constructor
+  Left' A
+| --- Right constructor
+  Right' B;
 
 -- Records
 

diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy
@@ -105,7 +105,9 @@ 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