From 22d9da46fb9b601d6447250ff25b00f0d3225067 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 14 Aug 2024 19:24:24 +0200 Subject: [PATCH] print Isabelle comments --- .../Compiler/Backend/Isabelle/Language.hs | 3 +- .../Compiler/Backend/Isabelle/Pretty/Base.hs | 26 +++++++++---- .../Backend/Isabelle/Translation/FromTyped.hs | 3 +- src/Juvix/Compiler/Concrete/Pretty.hs | 4 ++ src/Juvix/Compiler/Concrete/Print.hs | 4 ++ src/Juvix/Compiler/Concrete/Print/Base.hs | 38 ++++++++++++------- .../Internal/Translation/FromConcrete.hs | 8 ++-- 7 files changed, 60 insertions(+), 26 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Language.hs b/src/Juvix/Compiler/Backend/Isabelle/Language.hs index ec74cebf0b..a30a6d08a9 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Language.hs +++ b/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 diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs index 6e58abaa40..b8c9604bd7 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs +++ b/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 = diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index fa551dfe8a..d44d3753ba 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/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 -> diff --git a/src/Juvix/Compiler/Concrete/Pretty.hs b/src/Juvix/Compiler/Concrete/Pretty.hs index e4dbc78dc8..90abe94488 100644 --- 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 @@ -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 diff --git a/src/Juvix/Compiler/Concrete/Print.hs b/src/Juvix/Compiler/Concrete/Print.hs index 372eb00afe..1285cbbf3b 100644 --- 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 = mkAnsiText . PPOutput . docJudoc diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index 46efc48ca6..aaa24a6419 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/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 diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index e02a298620..df965b4c3e 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/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