From 5b1b34f0a56da57903e187c65bdf58b941cbe3ce Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 13 Apr 2023 14:23:44 +0200 Subject: [PATCH 01/12] Parsing of pragmas --- src/Juvix/Compiler/Concrete/Language.hs | 6 + src/Juvix/Compiler/Concrete/Pretty/Base.hs | 21 ++- src/Juvix/Compiler/Concrete/Print/Base.hs | 19 +- .../FromParsed/Analysis/Scoping.hs | 4 + .../Concrete/Translation/FromSource.hs | 162 +++++++++++------- src/Juvix/Compiler/Pragmas.hs | 64 +++++++ src/Juvix/Extra/Strings.hs | 6 + src/Juvix/Parser/Lexer.hs | 7 +- 8 files changed, 220 insertions(+), 69 deletions(-) create mode 100644 src/Juvix/Compiler/Pragmas.hs diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index 65f48d93c7..bf0afc935e 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -25,6 +25,7 @@ import Juvix.Compiler.Concrete.Data.PublicAnn import Juvix.Compiler.Concrete.Data.ScopedName (unqualifiedSymbol) import Juvix.Compiler.Concrete.Data.ScopedName qualified as S import Juvix.Compiler.Concrete.Data.VisibilityAnn +import Juvix.Compiler.Pragmas import Juvix.Data import Juvix.Data.Ape.Base as Ape import Juvix.Data.Fixity @@ -191,6 +192,7 @@ data TypeSignature (s :: Stage) = TypeSignature { _sigName :: FunctionName s, _sigType :: ExpressionType s, _sigDoc :: Maybe (Judoc s), + _sigPragmas :: Maybe Pragmas, _sigBuiltin :: Maybe (WithLoc BuiltinFunction), _sigBody :: Maybe (ExpressionType s), _sigTerminating :: Maybe KeywordRef @@ -209,6 +211,7 @@ deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Typ data AxiomDef (s :: Stage) = AxiomDef { _axiomKw :: KeywordRef, _axiomDoc :: Maybe (Judoc s), + _axiomPragmas :: Maybe Pragmas, _axiomName :: SymbolType s, _axiomBuiltin :: Maybe (WithLoc BuiltinAxiom), _axiomType :: ExpressionType s @@ -232,6 +235,7 @@ data InductiveConstructorDef (s :: Stage) = InductiveConstructorDef { _constructorPipe :: Irrelevant (Maybe KeywordRef), _constructorName :: InductiveConstructorName s, _constructorDoc :: Maybe (Judoc s), + _constructorPragmas :: Maybe Pragmas, _constructorType :: ExpressionType s } @@ -256,6 +260,7 @@ data InductiveDef (s :: Stage) = InductiveDef { _inductiveKw :: KeywordRef, _inductiveBuiltin :: Maybe (WithLoc BuiltinInductive), _inductiveDoc :: Maybe (Judoc s), + _inductivePragmas :: Maybe Pragmas, _inductiveName :: InductiveName s, _inductiveParameters :: [InductiveParameters s], _inductiveType :: Maybe (ExpressionType s), @@ -401,6 +406,7 @@ data Module (s :: Stage) (t :: ModuleIsTop) = Module { _moduleKw :: KeywordRef, _modulePath :: ModulePathType s t, _moduleDoc :: Maybe (Judoc s), + _modulePragmas :: Maybe Pragmas, _moduleBody :: [Statement s], _moduleKwEnd :: ModuleEndType t } diff --git a/src/Juvix/Compiler/Concrete/Pretty/Base.hs b/src/Juvix/Compiler/Concrete/Pretty/Base.hs index 890b242958..b494f68470 100644 --- a/src/Juvix/Compiler/Concrete/Pretty/Base.hs +++ b/src/Juvix/Compiler/Concrete/Pretty/Base.hs @@ -5,12 +5,14 @@ module Juvix.Compiler.Concrete.Pretty.Base ) where +import Data.ByteString.UTF8 qualified as BS import Data.List.NonEmpty.Extra qualified as NonEmpty import Juvix.Compiler.Concrete.Data.ScopedName (AbsModulePath, IsConcrete (..)) import Juvix.Compiler.Concrete.Data.ScopedName qualified as S import Juvix.Compiler.Concrete.Extra (unfoldApplication) import Juvix.Compiler.Concrete.Language import Juvix.Compiler.Concrete.Pretty.Options +import Juvix.Compiler.Pragmas import Juvix.Data.Ape import Juvix.Data.CodeAnn import Juvix.Extra.Strings qualified as Str @@ -173,8 +175,10 @@ instance (SingI s, SingI t) => PrettyCode (Module s t) where moduleBody' <- localIndent <$> ppCode _moduleBody modulePath' <- ppModulePathType _modulePath moduleDoc' <- mapM ppCode _moduleDoc + modulePragmas' <- mapM ppCode _modulePragmas return $ moduleDoc' + ?<> modulePragmas' ?<> kwModule <+> modulePath' <> kwSemicolon @@ -229,7 +233,8 @@ instance (SingI s) => PrettyCode (InductiveConstructorDef s) where constructorName' <- annDef _constructorName <$> ppSymbol _constructorName constructorType' <- ppExpression _constructorType doc' <- mapM ppCode _constructorDoc - return $ doc' ?<> hang' (constructorName' <+> kwColon <+> constructorType') + pragmas' <- mapM ppCode _constructorPragmas + return $ doc' ?<> pragmas' ?<> hang' (constructorName' <+> kwColon <+> constructorType') instance PrettyCode BuiltinInductive where ppCode i = return (kwBuiltin <+> keyword (prettyText i)) @@ -265,10 +270,11 @@ instance (SingI s) => PrettyCode (InductiveDef s) where ppCode :: forall r. (Members '[Reader Options] r) => InductiveDef s -> Sem r (Doc Ann) ppCode d@InductiveDef {..} = do doc' <- mapM ppCode _inductiveDoc + pragmas' <- mapM ppCode _inductivePragmas sig' <- ppInductiveSignature d inductiveConstructors' <- ppPipeBlock _inductiveConstructors return $ - doc' ?<> sig' + doc' ?<> pragmas' ?<> sig' <+> kwAssign <> line <> (indent' . align) inductiveConstructors' @@ -359,6 +365,11 @@ instance (SingI s) => PrettyCode (OpenModule s) where Public -> Just kwPublic NoPublic -> Nothing +instance PrettyCode Pragmas where + ppCode Pragmas {..} = + return $ + annotate (AnnComment) (pretty (Str.pragmasStart <> BS.toString _pragmasSource <> Str.pragmasEnd)) <> line + ppJudocStart :: Doc Ann ppJudocStart = pretty (Str.judocStart :: Text) @@ -405,8 +416,9 @@ instance (SingI s) => PrettyCode (TypeSignature s) where sigType' <- ppExpression _sigType builtin' <- traverse ppCode _sigBuiltin doc' <- mapM ppCode _sigDoc + pragmas' <- mapM ppCode _sigPragmas body' :: Maybe (Doc Ann) <- fmap ((kwAssign <>) . oneLineOrNext) <$> mapM ppExpression _sigBody - return $ doc' ?<> builtin' sigTerminating' <> hang' (sigName' <+> kwColon <> oneLineOrNext (sigType' <+?> body')) + return $ doc' ?<> pragmas' ?<> builtin' sigTerminating' <> hang' (sigName' <+> kwColon <> oneLineOrNext (sigType' <+?> body')) instance (SingI s) => PrettyCode (Function s) where ppCode a = case sing :: SStage s of @@ -504,9 +516,10 @@ instance (SingI s) => PrettyCode (AxiomDef s) where ppCode AxiomDef {..} = do axiomName' <- annDef _axiomName <$> ppSymbol _axiomName axiomDoc' <- mapM ppCode _axiomDoc + axiomPragmas' <- mapM ppCode _axiomPragmas axiomType' <- ppExpression _axiomType builtin' <- traverse ppCode _axiomBuiltin - return $ axiomDoc' ?<> builtin' hang' (kwAxiom <+> axiomName' <+> kwColon <+> axiomType') + return $ axiomDoc' ?<> axiomPragmas' ?<> builtin' hang' (kwAxiom <+> axiomName' <+> kwColon <+> axiomType') instance SingI s => PrettyCode (Import s) where ppCode :: forall r. Members '[Reader Options] r => Import s -> Sem r (Doc Ann) diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index cbd18e2995..bfcfdc8081 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -5,14 +5,17 @@ module Juvix.Compiler.Concrete.Print.Base ) where +import Data.ByteString.UTF8 qualified as BS import Data.List.NonEmpty.Extra qualified as NonEmpty import Juvix.Compiler.Concrete.Data.ScopedName qualified as S import Juvix.Compiler.Concrete.Language import Juvix.Compiler.Concrete.Pretty.Base qualified as P import Juvix.Compiler.Concrete.Pretty.Options +import Juvix.Compiler.Pragmas import Juvix.Data.CodeAnn (Ann, CodeAnn (..), ppStringLit) import Juvix.Data.Effect.ExactPrint import Juvix.Data.Keyword.All +import Juvix.Extra.Strings qualified as Str import Juvix.Prelude hiding ((<+>), (<+?>), (), (?<>)) import Juvix.Prelude.Pretty (annotate, pretty) @@ -61,7 +64,9 @@ instance SingI t => PrettyPrint (Module 'Scoped t) where let moduleBody' = localIndent (ppCode _moduleBody) modulePath' = ppModulePathType _modulePath moduleDoc' :: Sem r () = maybe (return ()) ppCode _moduleDoc + modulePragmas' :: Sem r () = maybe (return ()) ppCode _modulePragmas moduleDoc' + <> modulePragmas' <> ppCode _moduleKw <+> modulePath' <> ppCode kwSemicolon @@ -137,6 +142,11 @@ instance PrettyPrint OperatorSyntaxDef where instance PrettyPrint Expression where ppCode = ppMorpheme +instance PrettyPrint Pragmas where + ppCode Pragmas {..} = + noLoc (annotate (AnnComment) (pretty (Str.pragmasStart <> BS.toString _pragmasSource <> Str.pragmasEnd))) + <> line + instance PrettyPrint (Example 'Scoped) where ppCode e = noLoc P.ppJudocStart @@ -177,8 +187,10 @@ instance PrettyPrint (AxiomDef 'Scoped) where axiomName' <- P.annDef _axiomName <$> P.ppSymbol _axiomName let builtin' :: Maybe (Sem r ()) = (<> line) . (\x -> P.ppCode x >>= morpheme (getLoc x)) <$> _axiomBuiltin _axiomDoc' :: Maybe (Sem r ()) = ppCode <$> _axiomDoc + _axiomPragmas' :: Maybe (Sem r ()) = ppCode <$> _axiomPragmas axiom' = (<> line) . ppCode $ _axiomKw _axiomDoc' + ?<> _axiomPragmas' ?<> builtin' ?<> axiom' <> morpheme (getLoc _axiomName) axiomName' @@ -196,6 +208,7 @@ instance PrettyPrint (TypeSignature 'Scoped) where ppCode TypeSignature {..} = do let termin' :: Maybe (Sem r ()) = (<> line) . ppCode <$> _sigTerminating doc' :: Maybe (Sem r ()) = ppCode <$> _sigDoc + pragmas' :: Maybe (Sem r ()) = ppCode <$> _sigPragmas builtin' :: Maybe (Sem r ()) = (<> line) . ppCode <$> _sigBuiltin type' = ppCode _sigType name' = region (P.annDef _sigName) (ppCode _sigName) @@ -203,6 +216,7 @@ instance PrettyPrint (TypeSignature 'Scoped) where Nothing -> Nothing Just body -> Just (noLoc P.kwAssign <> oneLineOrNext (ppCode body)) doc' + ?<> pragmas' ?<> builtin' ?<> termin' ?<> ( name' @@ -311,7 +325,8 @@ instance PrettyPrint (InductiveConstructorDef 'Scoped) where let constructorName' = region (P.annDef _constructorName) (ppCode _constructorName) constructorType' = ppCode _constructorType doc' = ppCode <$> _constructorDoc - nest (pipeHelper <+> doc' ?<> constructorName' <+> noLoc P.kwColon <+> constructorType') + pragmas' = ppCode <$> _constructorPragmas + nest (pipeHelper <+> doc' ?<> pragmas' ?<> constructorName' <+> noLoc P.kwColon <+> constructorType') where -- we use this helper so that comments appear before the first optional pipe if the pipe was omitted pipeHelper :: Sem r () @@ -341,9 +356,11 @@ instance PrettyPrint (InductiveDef 'Scoped) where ppCode :: forall r. Members '[ExactPrint, Reader Options] r => InductiveDef 'Scoped -> Sem r () ppCode d@InductiveDef {..} = do let doc' = ppCode <$> _inductiveDoc + pragmas' = ppCode <$> _inductivePragmas constrs' = ppConstructorBlock _inductiveConstructors sig' = ppInductiveSignature d doc' + ?<> pragmas' ?<> sig' <+> noLoc P.kwAssign <> line diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index aa6a24569c..3d22aa7bfa 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -460,6 +460,7 @@ checkInductiveDef InductiveDef {..} = do InductiveDef { _inductiveName = inductiveName', _inductiveDoc = inductiveDoc', + _inductivePragmas = _inductivePragmas, _inductiveParameters = inductiveParameters', _inductiveType = inductiveType', _inductiveConstructors = inductiveConstructors', @@ -489,6 +490,7 @@ checkInductiveDef InductiveDef {..} = do { _constructorName = constructorName', _constructorType = constructorType', _constructorDoc = doc', + _constructorPragmas = _constructorPragmas, _constructorPipe } @@ -572,6 +574,7 @@ checkTopModule m@Module {..} = do { _modulePath = path', _moduleBody = body', _moduleDoc = doc', + _modulePragmas = _modulePragmas, _moduleKw, _moduleKwEnd } @@ -633,6 +636,7 @@ checkLocalModule Module {..} = do { _modulePath = _modulePath', _moduleBody = moduleBody', _moduleDoc = moduleDoc', + _modulePragmas = _modulePragmas, _moduleKw, _moduleKwEnd } diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 912ef1bf96..4c89808889 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -6,8 +6,10 @@ module Juvix.Compiler.Concrete.Translation.FromSource ) where +import Data.ByteString.UTF8 qualified as BS import Data.List.NonEmpty.Extra qualified as NonEmpty import Data.Singletons +import Data.Yaml import Juvix.Compiler.Concrete.Data.ParsedInfoTable import Juvix.Compiler.Concrete.Data.ParsedInfoTableBuilder import Juvix.Compiler.Concrete.Extra (MonadParsec (takeWhile1P)) @@ -17,12 +19,16 @@ import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.PathResolver import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context import Juvix.Compiler.Concrete.Translation.FromSource.Lexer hiding (symbol) import Juvix.Compiler.Pipeline.EntryPoint +import Juvix.Compiler.Pragmas +import Juvix.Extra.Strings qualified as Str import Juvix.Parser.Error import Juvix.Prelude import Juvix.Prelude.Pretty (Pretty, prettyText) type JudocStash = State (Maybe (Judoc 'Parsed)) +type PragmasStash = State (Maybe Pragmas) + fromSource :: (Members '[PathResolver, Files, Error JuvixError, NameIdGen] r) => EntryPoint -> @@ -65,8 +71,9 @@ expressionFromTextSource fp txt = mapError (JuvixError @ParserError) $ do runModuleParser :: Members '[Error ParserError, Files, PathResolver, NameIdGen, InfoTableBuilder] r => Path Abs File -> Text -> Sem r (Either ParserError (Module 'Parsed 'ModuleTop)) runModuleParser fileName input = do m <- - evalState (Nothing @(Judoc 'Parsed)) $ - P.runParserT topModuleDef (toFilePath fileName) input + evalState (Nothing @Pragmas) $ + evalState (Nothing @(Judoc 'Parsed)) $ + P.runParserT topModuleDef (toFilePath fileName) input case m of Left err -> return (Left (ErrMegaparsec (MegaparsecError err))) Right r -> registerModule r $> Right r @@ -79,8 +86,9 @@ runExpressionParser :: runExpressionParser fileName input = do m <- runParserInfoTableBuilder $ - evalState (Nothing @(Judoc 'Parsed)) $ - P.runParserT parseExpressionAtoms (toFilePath fileName) input + evalState (Nothing @Pragmas) $ + evalState (Nothing @(Judoc 'Parsed)) $ + P.runParserT parseExpressionAtoms (toFilePath fileName) input case m of (_, Left err) -> return (Left (ErrMegaparsec (MegaparsecError err))) (_, Right r) -> return (Right r) @@ -99,10 +107,11 @@ top :: top p = space >> p <* (optional (kw kwSemicolon) >> P.eof) topModuleDef :: - (Members '[Error ParserError, Files, PathResolver, InfoTableBuilder, JudocStash, NameIdGen] r) => + (Members '[Error ParserError, Files, PathResolver, InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Module 'Parsed 'ModuleTop) topModuleDef = do void (optional stashJudoc) + void (optional stashPragmas) m <- top moduleDef P.lift (checkPath (m ^. modulePath)) return m @@ -125,13 +134,13 @@ topModuleDef = do -- Symbols and names -------------------------------------------------------------------------------- -symbol :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r Symbol +symbol :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r Symbol symbol = uncurry (flip WithLoc) <$> identifierL -dottedSymbol :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (NonEmpty Symbol) +dottedSymbol :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (NonEmpty Symbol) dottedSymbol = fmap (uncurry (flip WithLoc)) <$> dottedIdentifier -name :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r Name +name :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r Name name = do parts <- dottedSymbol return $ case nonEmptyUnsnoc parts of @@ -141,19 +150,20 @@ name = do mkTopModulePath :: NonEmpty Symbol -> TopModulePath mkTopModulePath l = TopModulePath (NonEmpty.init l) (NonEmpty.last l) -symbolList :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (NonEmpty Symbol) +symbolList :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (NonEmpty Symbol) symbolList = braces (P.sepBy1 symbol (kw kwSemicolon)) -topModulePath :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r TopModulePath +topModulePath :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r TopModulePath topModulePath = mkTopModulePath <$> dottedSymbol -------------------------------------------------------------------------------- -- Top level statement -------------------------------------------------------------------------------- -statement :: (Members '[Files, Error ParserError, PathResolver, InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (Statement 'Parsed) +statement :: (Members '[Files, Error ParserError, PathResolver, InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Statement 'Parsed) statement = P.label "" $ do void (optional stashJudoc) + void (optional stashPragmas) (StatementOperator <$> operatorSyntaxDef) <|> (StatementOpenModule <$> openModule) <|> (StatementImport <$> import_) @@ -165,7 +175,24 @@ statement = P.label "" $ do <$> auxTypeSigFunClause ) -stashJudoc :: forall r. (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r () +stashPragmas :: forall r. (Members '[InfoTableBuilder, PragmasStash, NameIdGen] r) => ParsecS r () +stashPragmas = do + pragmas <- parsePragmas + P.lift (put (Just pragmas)) + return () + where + parsePragmas :: ParsecS r Pragmas + parsePragmas = do + void (P.chunk Str.pragmasStart) + off <- P.getOffset + str <- P.manyTill P.anySingle (P.chunk Str.pragmasEnd) + space + let bs = BS.fromString str + case decodeEither' bs of + Left err -> parseFailure off (prettyPrintParseException err) + Right pragmas -> return pragmas {_pragmasSource = bs} + +stashJudoc :: forall r. (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r () stashJudoc = do b <- judocBlocks many judocEmptyLine @@ -202,7 +229,7 @@ stashJudoc = do P.newline return ln -judocAtom :: forall r. (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (JudocAtom 'Parsed) +judocAtom :: forall r. (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (JudocAtom 'Parsed) judocAtom = JudocText <$> judocAtomText <|> JudocExpression <$> judocExpression @@ -219,17 +246,17 @@ judocAtom = judocText_ (P.char ';') return e -builtinInductive :: Members '[InfoTableBuilder, JudocStash, NameIdGen] r => ParsecS r (WithLoc BuiltinInductive) +builtinInductive :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (WithLoc BuiltinInductive) builtinInductive = builtinHelper -builtinFunction :: Members '[InfoTableBuilder, JudocStash, NameIdGen] r => ParsecS r (WithLoc BuiltinFunction) +builtinFunction :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (WithLoc BuiltinFunction) builtinFunction = builtinHelper -builtinAxiom :: Members '[InfoTableBuilder, JudocStash, NameIdGen] r => ParsecS r (WithLoc BuiltinAxiom) +builtinAxiom :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (WithLoc BuiltinAxiom) builtinAxiom = builtinHelper builtinHelper :: - (Members '[InfoTableBuilder, JudocStash, NameIdGen] r, Bounded a, Enum a, Pretty a) => + (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r, Bounded a, Enum a, Pretty a) => ParsecS r (WithLoc a) builtinHelper = P.choice @@ -237,17 +264,17 @@ builtinHelper = | a <- allElements ] -builtinInductiveDef :: Members '[InfoTableBuilder, JudocStash, NameIdGen] r => WithLoc BuiltinInductive -> ParsecS r (InductiveDef 'Parsed) +builtinInductiveDef :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => WithLoc BuiltinInductive -> ParsecS r (InductiveDef 'Parsed) builtinInductiveDef = inductiveDef . Just builtinAxiomDef :: - Members '[InfoTableBuilder, JudocStash, NameIdGen] r => + Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => WithLoc BuiltinAxiom -> ParsecS r (AxiomDef 'Parsed) builtinAxiomDef = axiomDef . Just builtinTypeSig :: - Members '[InfoTableBuilder, JudocStash, NameIdGen] r => + Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => WithLoc BuiltinFunction -> ParsecS r (TypeSignature 'Parsed) builtinTypeSig b = do @@ -255,7 +282,7 @@ builtinTypeSig b = do fun <- symbol typeSignature terminating fun (Just b) -builtinStatement :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (Statement 'Parsed) +builtinStatement :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Statement 'Parsed) builtinStatement = do void (kw kwBuiltin) (builtinInductive >>= fmap StatementInductive . builtinInductiveDef) @@ -266,10 +293,10 @@ builtinStatement = do -- Operator syntax declaration -------------------------------------------------------------------------------- -precedence :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r Precedence +precedence :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r Precedence precedence = PrecNat <$> (fst <$> decimal) -operatorSyntaxDef :: forall r. (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r OperatorSyntaxDef +operatorSyntaxDef :: forall r. (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r OperatorSyntaxDef operatorSyntaxDef = do (_fixityArity, _opKw) <- arity _fixityPrecedence <- precedence @@ -288,7 +315,7 @@ operatorSyntaxDef = do -- Import statement -------------------------------------------------------------------------------- -import_ :: Members '[Files, PathResolver, InfoTableBuilder, JudocStash, NameIdGen, Error ParserError] r => ParsecS r (Import 'Parsed) +import_ :: Members '[Files, PathResolver, InfoTableBuilder, PragmasStash, JudocStash, NameIdGen, Error ParserError] r => ParsecS r (Import 'Parsed) import_ = do _importKw <- kw kwImport _importModule <- topModulePath @@ -319,7 +346,7 @@ importedModule t = unlessM (moduleVisited t) go -- Expression -------------------------------------------------------------------------------- -expressionAtom :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (ExpressionAtom 'Parsed) +expressionAtom :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (ExpressionAtom 'Parsed) expressionAtom = P.label "" $ AtomLiteral <$> P.try literal @@ -335,7 +362,7 @@ expressionAtom = <|> braces (AtomBraces <$> withLoc parseExpressionAtoms) parseExpressionAtoms :: - (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => + (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (ExpressionAtoms 'Parsed) parseExpressionAtoms = do (_expressionAtoms, _expressionAtomsLoc) <- interval (P.some expressionAtom) @@ -345,34 +372,34 @@ parseExpressionAtoms = do -- Holes -------------------------------------------------------------------------------- -hole :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (HoleType 'Parsed) +hole :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (HoleType 'Parsed) hole = snd <$> interval (kw kwHole) -------------------------------------------------------------------------------- -- Literals -------------------------------------------------------------------------------- -literalInteger :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r LiteralLoc +literalInteger :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r LiteralLoc literalInteger = do (x, loc) <- integer return (WithLoc loc (LitInteger x)) -literalString :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r LiteralLoc +literalString :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r LiteralLoc literalString = do (x, loc) <- string return (WithLoc loc (LitString x)) -literal :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r LiteralLoc +literal :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r LiteralLoc literal = do l <- literalInteger <|> literalString P.lift (registerLiteral l) -letClause :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (LetClause 'Parsed) +letClause :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (LetClause 'Parsed) letClause = either LetTypeSig LetFunClause <$> auxTypeSigFunClause -letBlock :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (LetBlock 'Parsed) +letBlock :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (LetBlock 'Parsed) letBlock = do _letKw <- kw kwLet _letClauses <- P.sepEndBy1 letClause (kw kwSemicolon) @@ -380,7 +407,7 @@ letBlock = do _letExpression <- parseExpressionAtoms return LetBlock {..} -caseBranch :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (CaseBranch 'Parsed) +caseBranch :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (CaseBranch 'Parsed) caseBranch = do _caseBranchPipe <- kw kwPipe _caseBranchPattern <- parsePatternAtoms @@ -388,7 +415,7 @@ caseBranch = do _caseBranchExpression <- parseExpressionAtoms return CaseBranch {..} -case_ :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (Case 'Parsed) +case_ :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Case 'Parsed) case_ = do _caseKw <- kw kwCase _caseExpression <- parseExpressionAtoms @@ -400,7 +427,7 @@ case_ = do -- Universe expression -------------------------------------------------------------------------------- -universe :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r Universe +universe :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r Universe universe = do i <- snd <$> interval (kw kwType) uni <- optional decimal @@ -410,14 +437,20 @@ universe = do Just (lvl, i') -> Universe (Just lvl) (i <> i') ) -getJudoc :: (Members '[JudocStash, NameIdGen] r) => ParsecS r (Maybe (Judoc 'Parsed)) +getJudoc :: (Member JudocStash r) => ParsecS r (Maybe (Judoc 'Parsed)) getJudoc = P.lift $ do j <- get put (Nothing @(Judoc 'Parsed)) return j +getPragmas :: (Member PragmasStash r) => ParsecS r (Maybe Pragmas) +getPragmas = P.lift $ do + j <- get + put (Nothing @Pragmas) + return j + typeSignature :: - Members '[InfoTableBuilder, JudocStash, NameIdGen] r => + Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => Maybe KeywordRef -> Symbol -> Maybe (WithLoc BuiltinFunction) -> @@ -426,12 +459,13 @@ typeSignature _sigTerminating _sigName _sigBuiltin = do kw kwColon _sigType <- parseExpressionAtoms _sigDoc <- getJudoc + _sigPragmas <- getPragmas _sigBody <- optional (kw kwAssign >> parseExpressionAtoms) return TypeSignature {..} -- | Used to minimize the amount of required @P.try@s. auxTypeSigFunClause :: - (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => + (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Either (TypeSignature 'Parsed) (FunctionClause 'Parsed)) auxTypeSigFunClause = do terminating <- optional (kw kwTerminating) @@ -440,12 +474,13 @@ auxTypeSigFunClause = do <|> (Right <$> functionClause sym) axiomDef :: - Members '[InfoTableBuilder, JudocStash, NameIdGen] r => + Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => Maybe (WithLoc BuiltinAxiom) -> ParsecS r (AxiomDef 'Parsed) axiomDef _axiomBuiltin = do _axiomKw <- kw kwAxiom _axiomDoc <- getJudoc + _axiomPragmas <- getPragmas _axiomName <- symbol kw kwColon _axiomType <- parseExpressionAtoms @@ -455,17 +490,17 @@ axiomDef _axiomBuiltin = do -- Function expression -------------------------------------------------------------------------------- -implicitOpen :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r IsImplicit +implicitOpen :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r IsImplicit implicitOpen = lbrace $> Implicit <|> lparen $> Explicit -implicitClose :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => IsImplicit -> ParsecS r () +implicitClose :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => IsImplicit -> ParsecS r () implicitClose = \case Implicit -> rbrace Explicit -> rparen -functionParams :: forall r. (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (FunctionParameters 'Parsed) +functionParams :: forall r. (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (FunctionParameters 'Parsed) functionParams = do (_paramNames, _paramImplicit) <- P.try $ do impl <- implicitOpen @@ -481,7 +516,7 @@ functionParams = do (Just <$> symbol) <|> (Nothing <$ kw kwWildcard) -function :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (Function 'Parsed) +function :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Function 'Parsed) function = do _funParameters <- functionParams _funKw <- kw kwRightArrow @@ -492,14 +527,14 @@ function = do -- Lambda expression -------------------------------------------------------------------------------- -lambdaClause :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => Irrelevant (Maybe KeywordRef) -> ParsecS r (LambdaClause 'Parsed) +lambdaClause :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => Irrelevant (Maybe KeywordRef) -> ParsecS r (LambdaClause 'Parsed) lambdaClause _lambdaPipe = do _lambdaParameters <- P.some patternAtom kw kwAssign _lambdaBody <- parseExpressionAtoms return LambdaClause {..} -lambda :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (Lambda 'Parsed) +lambda :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Lambda 'Parsed) lambda = do _lambdaKw <- kw kwLambda _lambdaClauses <- braces (pipeSep1 lambdaClause) @@ -509,11 +544,12 @@ lambda = do -- Data type construction declaration ------------------------------------------------------------------------------- -inductiveDef :: Members '[InfoTableBuilder, JudocStash, NameIdGen] r => Maybe (WithLoc BuiltinInductive) -> ParsecS r (InductiveDef 'Parsed) +inductiveDef :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => Maybe (WithLoc BuiltinInductive) -> ParsecS r (InductiveDef 'Parsed) inductiveDef _inductiveBuiltin = do _inductivePositive <- isJust <$> optional (kw kwPositive) _inductiveKw <- kw kwInductive _inductiveDoc <- getJudoc + _inductivePragmas <- getPragmas _inductiveName <- symbol P. "" _inductiveParameters <- P.many inductiveParams @@ -527,39 +563,40 @@ inductiveDef _inductiveBuiltin = do P. "" return InductiveDef {..} -inductiveParams :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (InductiveParameters 'Parsed) +inductiveParams :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (InductiveParameters 'Parsed) inductiveParams = parens $ do _inductiveParametersNames <- some1 symbol kw kwColon _inductiveParametersType <- parseExpressionAtoms return InductiveParameters {..} -constructorDef :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => Irrelevant (Maybe KeywordRef) -> ParsecS r (InductiveConstructorDef 'Parsed) +constructorDef :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => Irrelevant (Maybe KeywordRef) -> ParsecS r (InductiveConstructorDef 'Parsed) constructorDef _constructorPipe = do _constructorDoc <- optional stashJudoc >> getJudoc + _constructorPragmas <- optional stashPragmas >> getPragmas _constructorName <- symbol P. "" _constructorType <- kw kwColon >> parseExpressionAtoms P. "" return InductiveConstructorDef {..} -wildcard :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r Wildcard +wildcard :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r Wildcard wildcard = Wildcard . snd <$> interval (kw kwWildcard) -------------------------------------------------------------------------------- -- Pattern section -------------------------------------------------------------------------------- -patternAtomAnon :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (PatternAtom 'Parsed) +patternAtomAnon :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (PatternAtom 'Parsed) patternAtomAnon = PatternAtomWildcard <$> wildcard <|> PatternAtomParens <$> parens parsePatternAtomsNested <|> PatternAtomBraces <$> braces parsePatternAtomsNested -patternAtomAt :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => SymbolType 'Parsed -> ParsecS r (PatternAtom 'Parsed) +patternAtomAt :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => SymbolType 'Parsed -> ParsecS r (PatternAtom 'Parsed) patternAtomAt s = kw kwAt >> PatternAtomAt . PatternBinding s <$> patternAtom -patternAtomNamed :: forall r. (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => Bool -> ParsecS r (PatternAtom 'Parsed) +patternAtomNamed :: forall r. (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => Bool -> ParsecS r (PatternAtom 'Parsed) patternAtomNamed nested = do off <- P.getOffset n <- name @@ -575,21 +612,21 @@ patternAtomNamed nested = do (not nested && t ^. withLocParam == "=") (parseFailure off "expected \":=\" instead of \"=\"") -patternAtomNested :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (PatternAtom 'Parsed) +patternAtomNested :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (PatternAtom 'Parsed) patternAtomNested = patternAtom' True -patternAtom :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (PatternAtom 'Parsed) +patternAtom :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (PatternAtom 'Parsed) patternAtom = patternAtom' False -patternAtom' :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => Bool -> ParsecS r (PatternAtom 'Parsed) +patternAtom' :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => Bool -> ParsecS r (PatternAtom 'Parsed) patternAtom' nested = P.label "" $ patternAtomNamed nested <|> patternAtomAnon -parsePatternAtoms :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (PatternAtoms 'Parsed) +parsePatternAtoms :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (PatternAtoms 'Parsed) parsePatternAtoms = do (_patternAtoms, _patternAtomsLoc) <- interval (P.some patternAtom) return PatternAtoms {..} -parsePatternAtomsNested :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (PatternAtoms 'Parsed) +parsePatternAtomsNested :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (PatternAtoms 'Parsed) parsePatternAtomsNested = do (_patternAtoms, _patternAtomsLoc) <- interval (P.some patternAtomNested) return PatternAtoms {..} @@ -598,7 +635,7 @@ parsePatternAtomsNested = do -- Function binding declaration -------------------------------------------------------------------------------- -functionClause :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => Symbol -> ParsecS r (FunctionClause 'Parsed) +functionClause :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => Symbol -> ParsecS r (FunctionClause 'Parsed) functionClause _clauseOwnerFunction = do _clausePatterns <- P.many patternAtom kw kwAssign @@ -609,15 +646,16 @@ functionClause _clauseOwnerFunction = do -- Module declaration -------------------------------------------------------------------------------- -pmodulePath :: forall t r. (SingI t, Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (ModulePathType 'Parsed t) +pmodulePath :: forall t r. (SingI t, Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (ModulePathType 'Parsed t) pmodulePath = case sing :: SModuleIsTop t of SModuleTop -> topModulePath SModuleLocal -> symbol -moduleDef :: forall t r. (SingI t, Members '[Error ParserError, Files, PathResolver, InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (Module 'Parsed t) +moduleDef :: forall t r. (SingI t, Members '[Error ParserError, Files, PathResolver, InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Module 'Parsed t) moduleDef = P.label "" $ do _moduleKw <- kw kwModule _moduleDoc <- getJudoc + _modulePragmas <- getPragmas _modulePath <- pmodulePath _moduleParameters <- many inductiveParams kw kwSemicolon @@ -631,7 +669,7 @@ moduleDef = P.label "" $ do SModuleTop -> void (optional (kw kwEnd >> kw kwSemicolon)) -- | An ExpressionAtom which is a valid expression on its own. -atomicExpression :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (ExpressionAtoms 'Parsed) +atomicExpression :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (ExpressionAtoms 'Parsed) atomicExpression = do (atom, loc) <- interval expressionAtom case atom of @@ -639,7 +677,7 @@ atomicExpression = do _ -> return () return $ ExpressionAtoms (NonEmpty.singleton atom) loc -openModule :: forall r. (Members '[Error ParserError, PathResolver, Files, InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (OpenModule 'Parsed) +openModule :: forall r. (Members '[Error ParserError, PathResolver, Files, InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (OpenModule 'Parsed) openModule = do _openModuleKw <- kw kwOpen _openModuleImportKw <- optional (kw kwImport) diff --git a/src/Juvix/Compiler/Pragmas.hs b/src/Juvix/Compiler/Pragmas.hs new file mode 100644 index 0000000000..285b0f2baa --- /dev/null +++ b/src/Juvix/Compiler/Pragmas.hs @@ -0,0 +1,64 @@ +module Juvix.Compiler.Pragmas where + +import Data.Aeson.BetterErrors +import Data.Yaml +import Juvix.Prelude hiding ((<|>)) + +data PragmaInline + = InlineNever + | InlineFullyApplied + | InlinePartiallyApplied {_pragmaInlineArgsNum :: Int} + deriving stock (Show, Eq, Ord) + +newtype PragmaUnroll = PragmaUnroll + { _pragmaUnrollDepth :: Int + } + deriving stock (Show, Eq, Ord) + +data Pragmas = Pragmas + { -- We keep the exact source of the pragma text. This is necessary, because + -- pragmas are supposed to be backwards-compatible. Unrecognised pragmas + -- should be ignored, but they still need to be printed out when + -- pretty-printing. Also, we probably don't want to impose pragma formatting + -- choices on the user. + _pragmasSource :: ByteString, + _pragmasInline :: Maybe PragmaInline, + _pragmasUnroll :: Maybe PragmaUnroll + } + deriving stock (Show, Eq, Ord) + +makeLenses ''PragmaUnroll +makeLenses ''Pragmas + +type PragmaError = Text + +instance FromJSON Pragmas where + parseJSON = toAesonParser id parsePragmas + where + parsePragmas :: Parse PragmaError Pragmas + parsePragmas = do + let _pragmasSource :: ByteString + _pragmasSource = "" + _pragmasInline <- keyMay "inline" parseInline + _pragmasUnroll <- keyMay "unroll" parseUnroll + return Pragmas {..} + + parseInline :: Parse PragmaError PragmaInline + parseInline = parseInlineArgsNum <|> parseInlineBool + where + parseInlineArgsNum :: Parse PragmaError PragmaInline + parseInlineArgsNum = do + _pragmaInlineArgsNum <- asIntegral + return $ InlinePartiallyApplied {..} + + parseInlineBool :: Parse PragmaError PragmaInline + parseInlineBool = do + b <- asBool + if + | b -> return InlineFullyApplied + | otherwise -> return InlineNever + + parseUnroll :: Parse PragmaError PragmaUnroll + parseUnroll = do + _pragmaUnrollDepth <- asIntegral + return PragmaUnroll {..} diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index d1d3304de3..7e4df675d7 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -14,6 +14,12 @@ judocStart = "---" judocExample :: (IsString s) => s judocExample = ">>>" +pragmasStart :: (IsString s) => s +pragmasStart = "{-#" + +pragmasEnd :: (IsString s) => s +pragmasEnd = "#-}" + end :: (IsString s) => s end = "end" diff --git a/src/Juvix/Parser/Lexer.hs b/src/Juvix/Parser/Lexer.hs index d4fb08ad71..27484ed9d1 100644 --- a/src/Juvix/Parser/Lexer.hs +++ b/src/Juvix/Parser/Lexer.hs @@ -25,7 +25,7 @@ space1 = void $ takeWhile1P (Just "white space (only spaces and newlines allowed isWhiteSpace = (`elem` [' ', '\n']) space' :: forall r. Bool -> ParsecS r [Comment] -space' judoc = do +space' special = do catMaybes <$> P.many ( hidden @@ -38,7 +38,7 @@ space' judoc = do lineComment = do let _commentType = CommentOneLine when - judoc + special (notFollowedBy (P.chunk Str.judocStart)) (_commentText, _commentInterval) <- interval $ do void (P.chunk "--") @@ -48,6 +48,9 @@ space' judoc = do blockComment :: ParsecS r Comment blockComment = do let _commentType = CommentBlock + when + special + (notFollowedBy (P.chunk Str.pragmasStart)) (_commentText, _commentInterval) <- interval $ do void (P.chunk "{-") pack <$> P.manyTill anySingle (P.chunk "-}") From 1cf58f66651ded73616e91871ac5a958556cb389 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 14 Apr 2023 11:25:26 +0200 Subject: [PATCH 02/12] fix highlighting --- .../Compiler/Concrete/Data/ParsedInfoTableBuilder.hs | 9 +++++++++ src/Juvix/Compiler/Concrete/Pretty/Base.hs | 4 ++-- src/Juvix/Compiler/Concrete/Print/Base.hs | 2 +- src/Juvix/Compiler/Concrete/Translation/FromSource.hs | 3 ++- .../Compiler/Concrete/Translation/FromSource/Lexer.hs | 7 +++++-- 5 files changed, 19 insertions(+), 6 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Data/ParsedInfoTableBuilder.hs b/src/Juvix/Compiler/Concrete/Data/ParsedInfoTableBuilder.hs index 2844f5a354..a9ebbfa9c3 100644 --- a/src/Juvix/Compiler/Concrete/Data/ParsedInfoTableBuilder.hs +++ b/src/Juvix/Compiler/Concrete/Data/ParsedInfoTableBuilder.hs @@ -3,6 +3,7 @@ module Juvix.Compiler.Concrete.Data.ParsedInfoTableBuilder registerLiteral, registerKeyword, registerJudocText, + registerPragmas, registerComment, registerModule, moduleVisited, @@ -46,6 +47,14 @@ registerJudocText i = _parsedTag = ParsedTagComment } +registerPragmas :: Member InfoTableBuilder r => Interval -> Sem r () +registerPragmas i = + registerItem + ParsedItem + { _parsedLoc = i, + _parsedTag = ParsedTagComment + } + registerLiteral :: Member InfoTableBuilder r => LiteralLoc -> Sem r LiteralLoc registerLiteral l = l diff --git a/src/Juvix/Compiler/Concrete/Pretty/Base.hs b/src/Juvix/Compiler/Concrete/Pretty/Base.hs index 6d64f2d338..fe96230521 100644 --- a/src/Juvix/Compiler/Concrete/Pretty/Base.hs +++ b/src/Juvix/Compiler/Concrete/Pretty/Base.hs @@ -368,7 +368,7 @@ instance (SingI s) => PrettyCode (OpenModule s) where instance PrettyCode Pragmas where ppCode Pragmas {..} = return $ - annotate (AnnComment) (pretty (Str.pragmasStart <> BS.toString _pragmasSource <> Str.pragmasEnd)) <> line + annotate AnnComment (pretty (Str.pragmasStart <> BS.toString _pragmasSource <> Str.pragmasEnd)) <> line ppJudocStart :: Doc Ann ppJudocStart = pretty (Str.judocStart :: Text) @@ -389,7 +389,7 @@ instance (SingI s) => PrettyCode (JudocBlock s) where instance (SingI s) => PrettyCode (JudocParagraphLine s) where ppCode (JudocParagraphLine atoms) = do atoms' <- mconcatMap ppCode atoms - let prefix = pretty (Str.judocStart :: Text) :: Doc Ann + let prefix = annotate AnnComment (pretty (Str.judocStart :: Text)) return (prefix <+> atoms') instance (SingI s) => PrettyCode (Judoc s) where diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index 4676bd4e74..847004ca1d 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -144,7 +144,7 @@ instance PrettyPrint Expression where instance PrettyPrint Pragmas where ppCode Pragmas {..} = - noLoc (annotate (AnnComment) (pretty (Str.pragmasStart <> BS.toString _pragmasSource <> Str.pragmasEnd))) + noLoc (annotate AnnComment (pretty (Str.pragmasStart <> BS.toString _pragmasSource <> Str.pragmasEnd))) <> line instance PrettyPrint (Example 'Scoped) where diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index eb3ef8df18..0285630044 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -178,7 +178,8 @@ statement = P.label "" $ do stashPragmas :: forall r. (Members '[InfoTableBuilder, PragmasStash, NameIdGen] r) => ParsecS r () stashPragmas = do - pragmas <- parsePragmas + (pragmas, i) <- interval parsePragmas + P.lift (registerPragmas i) P.lift (put (Just pragmas)) return () where diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource/Lexer.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource/Lexer.hs index 0f0bfcc6ce..29a5972762 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource/Lexer.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource/Lexer.hs @@ -74,8 +74,11 @@ string = lexemeInterval string' judocExampleStart :: ParsecS r () judocExampleStart = P.chunk Str.judocExample >> hspace -judocStart :: ParsecS r () -judocStart = P.chunk Str.judocStart >> hspace +judocStart :: Member InfoTableBuilder r => ParsecS r () +judocStart = do + (_, i) <- interval (P.chunk Str.judocStart) + hspace + P.lift (registerJudocText i) judocEmptyLine :: (Members '[InfoTableBuilder] r) => ParsecS r () judocEmptyLine = lexeme (void (P.try (judocStart >> P.newline))) From 890b63ca55153e3e37afe06ca9d53a0a64a2e5ed Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 14 Apr 2023 12:36:50 +0200 Subject: [PATCH 03/12] pragma parsing tests --- src/Juvix/Compiler/Concrete/Pretty/Base.hs | 4 ++- test/Parsing/Negative.hs | 14 ++++++++++ test/Scope/Positive.hs | 6 ++++- tests/negative/PragmasFormat.juvix | 7 +++++ tests/negative/PragmasYAML.juvix | 7 +++++ tests/positive/Pragmas.juvix | 30 ++++++++++++++++++++++ 6 files changed, 66 insertions(+), 2 deletions(-) create mode 100644 tests/negative/PragmasFormat.juvix create mode 100644 tests/negative/PragmasYAML.juvix create mode 100644 tests/positive/Pragmas.juvix diff --git a/src/Juvix/Compiler/Concrete/Pretty/Base.hs b/src/Juvix/Compiler/Concrete/Pretty/Base.hs index fe96230521..766c1c0060 100644 --- a/src/Juvix/Compiler/Concrete/Pretty/Base.hs +++ b/src/Juvix/Compiler/Concrete/Pretty/Base.hs @@ -394,7 +394,9 @@ instance (SingI s) => PrettyCode (JudocParagraphLine s) where instance (SingI s) => PrettyCode (Judoc s) where ppCode :: forall r. (Members '[Reader Options] r) => Judoc s -> Sem r (Doc Ann) - ppCode (Judoc blocks) = mconcatMapM ppCode blocks + ppCode (Judoc blocks) = do + doc' <- vsep <$> mapM ppCode blocks + return $ doc' <> line instance (SingI s) => PrettyCode (JudocAtom s) where ppCode :: forall r. (Members '[Reader Options] r) => JudocAtom s -> Sem r (Doc Ann) diff --git a/test/Parsing/Negative.hs b/test/Parsing/Negative.hs index 8c31e4a81b..3b9bfa6aa6 100644 --- a/test/Parsing/Negative.hs +++ b/test/Parsing/Negative.hs @@ -57,6 +57,20 @@ parserErrorTests = "Tab character" $(mkRelDir ".") $(mkRelFile "Tab.juvix") + $ \case + ErrMegaparsec {} -> Nothing + _ -> wrongError, + negTest + "Pragmas YAML error" + $(mkRelDir ".") + $(mkRelFile "PragmasYAML.juvix") + $ \case + ErrMegaparsec {} -> Nothing + _ -> wrongError, + negTest + "Pragmas format error" + $(mkRelDir ".") + $(mkRelFile "PragmasFormat.juvix") $ \case ErrMegaparsec {} -> Nothing _ -> wrongError diff --git a/test/Scope/Positive.hs b/test/Scope/Positive.hs index 0e0f51cf9f..c55bbfdf84 100644 --- a/test/Scope/Positive.hs +++ b/test/Scope/Positive.hs @@ -224,5 +224,9 @@ tests = PosTest "Shadow imported symbol" $(mkRelDir "ImportShadow") - $(mkRelFile "Main.juvix") + $(mkRelFile "Main.juvix"), + PosTest + "Pragmas" + $(mkRelDir ".") + $(mkRelFile "Pragmas.juvix") ] diff --git a/tests/negative/PragmasFormat.juvix b/tests/negative/PragmasFormat.juvix new file mode 100644 index 0000000000..3e3ce48a79 --- /dev/null +++ b/tests/negative/PragmasFormat.juvix @@ -0,0 +1,7 @@ +module PragmasFormat; + +open import Stdlib.Prelude; + +{-# inline: Tre #-} +main : Nat; +main := 0; diff --git a/tests/negative/PragmasYAML.juvix b/tests/negative/PragmasYAML.juvix new file mode 100644 index 0000000000..6348f6cecc --- /dev/null +++ b/tests/negative/PragmasYAML.juvix @@ -0,0 +1,7 @@ +module PragmasYAML; + +open import Stdlib.Prelude; + +{-# inline: true, unroll: 500 #-} +main : Nat; +main := 0; diff --git a/tests/positive/Pragmas.juvix b/tests/positive/Pragmas.juvix new file mode 100644 index 0000000000..9aa26abdc5 --- /dev/null +++ b/tests/positive/Pragmas.juvix @@ -0,0 +1,30 @@ +module Pragmas; + +open import Stdlib.Prelude; + +{-# + unknownPragma: something + unroll: 100 + inline: false +#-} +f : Nat → Nat; +f x := x; + +{-# inline: true #-} +g : Nat → Nat; +g x := suc x; + +{- +Multiline highlighting +-} +--- Judoc comment 1 +--- Judoc comment 2 +{-# unroll: 0 #-} +terminating +h : Nat → Nat; +h x := x + 5; + +--- Judoc comment +{-# {inline: false, unroll: 10, unknownPragma: tratatata} #-} +main : Nat; +main := 0; From ca453cdc8924af92eb223c763a42a54ed8035aa3 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 14 Apr 2023 14:19:30 +0200 Subject: [PATCH 04/12] refactor & propagation of pragmas to Abstract --- src/Juvix/Compiler/Abstract/Language.hs | 15 ++-- .../Abstract/Translation/FromConcrete.hs | 72 ++++++++++++------- src/Juvix/Compiler/Concrete/Language.hs | 22 ++++-- src/Juvix/Compiler/Concrete/Pretty/Base.hs | 8 +-- src/Juvix/Compiler/Concrete/Print/Base.hs | 8 +-- .../Concrete/Translation/FromSource.hs | 15 ++-- src/Juvix/Data.hs | 4 ++ src/Juvix/{Compiler => Data}/Pragmas.hs | 32 ++++++--- src/Juvix/Data/WithSource.hs | 34 +++++++++ 9 files changed, 143 insertions(+), 67 deletions(-) rename src/Juvix/{Compiler => Data}/Pragmas.hs (70%) create mode 100644 src/Juvix/Data/WithSource.hs diff --git a/src/Juvix/Compiler/Abstract/Language.hs b/src/Juvix/Compiler/Abstract/Language.hs index f9a4de4862..836d41e239 100644 --- a/src/Juvix/Compiler/Abstract/Language.hs +++ b/src/Juvix/Compiler/Abstract/Language.hs @@ -30,7 +30,8 @@ type TopModuleName = Name data Module = Module { _moduleName :: Name, _moduleExamples :: [Example], - _moduleBody :: ModuleBody + _moduleBody :: ModuleBody, + _modulePragmas :: Pragmas } deriving stock (Eq, Show) @@ -59,7 +60,8 @@ data FunctionDef = FunctionDef _funDefExamples :: [Example], _funDefClauses :: NonEmpty FunctionClause, _funDefBuiltin :: Maybe BuiltinFunction, - _funDefTerminating :: Bool + _funDefTerminating :: Bool, + _funDefPragmas :: Pragmas } deriving stock (Eq, Show) @@ -194,21 +196,24 @@ data InductiveDef = InductiveDef _inductiveType :: Expression, _inductiveExamples :: [Example], _inductiveConstructors :: [InductiveConstructorDef], - _inductivePositive :: Bool + _inductivePositive :: Bool, + _inductivePragmas :: Pragmas } deriving stock (Eq, Show) data InductiveConstructorDef = InductiveConstructorDef { _constructorName :: ConstrName, _constructorExamples :: [Example], - _constructorType :: Expression + _constructorType :: Expression, + _constructorPragmas :: Pragmas } deriving stock (Eq, Show) data AxiomDef = AxiomDef { _axiomName :: AxiomName, _axiomBuiltin :: Maybe BuiltinAxiom, - _axiomType :: Expression + _axiomType :: Expression, + _axiomPragmas :: Pragmas } deriving stock (Eq, Show) diff --git a/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs b/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs index b9281b82f4..050b61cfd6 100644 --- a/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs @@ -29,30 +29,34 @@ unsupported msg = error $ msg <> "Scoped to Abstract: not yet supported" fromConcrete :: (Members '[Error JuvixError, Builtins, NameIdGen] r) => Scoper.ScoperResult -> Sem r AbstractResult fromConcrete _resultScoper = mapError (JuvixError @ScoperError) $ do - (_resultTable, _resultModules) <- runInfoTableBuilder (evalState (ModulesCache mempty) (mapM goTopModule ms)) + (_resultTable, _resultModules) <- + runInfoTableBuilder $ + runReader @Pragmas mempty $ + evalState (ModulesCache mempty) $ + mapM goTopModule ms let _resultExports = _resultScoper ^. Scoper.resultExports return AbstractResult {..} where ms = _resultScoper ^. Scoper.resultModules fromConcreteExpression :: (Members '[Error JuvixError, NameIdGen] r) => Scoper.Expression -> Sem r Abstract.Expression -fromConcreteExpression = mapError (JuvixError @ScoperError) . ignoreInfoTableBuilder . goExpression +fromConcreteExpression = mapError (JuvixError @ScoperError) . ignoreInfoTableBuilder . runReader @Pragmas mempty . goExpression goTopModule :: - (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, State ModulesCache] r) => + (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r) => Module 'Scoped 'ModuleTop -> Sem r Abstract.TopModule goTopModule = goModule goLocalModule :: - (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, State ModulesCache] r) => + (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r) => Module 'Scoped 'ModuleLocal -> Sem r Abstract.LocalModule goLocalModule = goModule goModule :: forall r t. - (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, State ModulesCache] r, SingI t) => + (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r, SingI t) => Module 'Scoped t -> Sem r Abstract.Module goModule m = case sing :: SModuleIsTop t of @@ -70,13 +74,15 @@ goModule m = case sing :: SModuleIsTop t of where goModule' :: Module 'Scoped t -> Sem r Abstract.Module goModule' Module {..} = do - body' <- goModuleBody _moduleBody + pragmas' <- goPragmas _modulePragmas + body' <- local (const pragmas') (goModuleBody _moduleBody) examples' <- goExamples _moduleDoc return Abstract.Module { _moduleName = name', _moduleBody = body', - _moduleExamples = examples' + _moduleExamples = examples', + _modulePragmas = pragmas' } where name' :: Abstract.Name @@ -84,6 +90,11 @@ goModule m = case sing :: SModuleIsTop t of SModuleTop -> goSymbol (S.topModulePathName _modulePath) SModuleLocal -> goSymbol _modulePath +goPragmas :: Member (Reader Pragmas) r => Maybe ParsedPragmas -> Sem r Pragmas +goPragmas p = do + p' <- ask + return $ p' <> maybe mempty (^. withSourceValue) p + goName :: S.Name -> Abstract.Name goName name = set Abstract.namePretty prettyStr (goSymbol (S.nameUnqualify name)) @@ -104,7 +115,7 @@ goSymbol s = goModuleBody :: forall r. - (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, State ModulesCache] r) => + (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r) => [Statement 'Scoped] -> Sem r Abstract.ModuleBody goModuleBody ss' = do @@ -138,7 +149,7 @@ goModuleBody ss' = do goStatement :: forall r. - (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, State ModulesCache] r) => + (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r) => Indexed (Statement 'Scoped) -> Sem r (Maybe (Indexed Abstract.Statement)) goStatement (Indexed idx s) = @@ -154,7 +165,7 @@ goStatement (Indexed idx s) = goOpenModule :: forall r. - (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, State ModulesCache] r) => + (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r) => OpenModule 'Scoped -> Sem r (Maybe Abstract.Statement) goOpenModule o @@ -167,7 +178,7 @@ goOpenModule o | otherwise = return Nothing goLetFunctionDef :: - (Members '[InfoTableBuilder, Error ScoperError] r) => + (Members '[InfoTableBuilder, Reader Pragmas, Error ScoperError] r) => TypeSignature 'Scoped -> [FunctionClause 'Scoped] -> Sem r Abstract.FunctionDef @@ -175,7 +186,7 @@ goLetFunctionDef = goFunctionDefHelper goFunctionDefHelper :: forall r. - (Members '[InfoTableBuilder, Error ScoperError] r) => + (Members '[InfoTableBuilder, Reader Pragmas, Error ScoperError] r) => TypeSignature 'Scoped -> [FunctionClause 'Scoped] -> Sem r Abstract.FunctionDef @@ -185,6 +196,7 @@ goFunctionDefHelper sig@TypeSignature {..} clauses = do _funDefBuiltin = (^. withLocParam) <$> _sigBuiltin _funDefTypeSig <- goExpression _sigType _funDefExamples <- goExamples _sigDoc + _funDefPragmas <- goPragmas _sigPragmas _funDefClauses <- case (_sigBody, nonEmpty clauses) of (Nothing, Nothing) -> throw (ErrLacksFunctionClause (LacksFunctionClause sig)) (Just {}, Just clauses') -> throw (ErrDuplicateFunctionClause (DuplicateFunctionClause sig (head clauses'))) @@ -204,7 +216,7 @@ goFunctionDefHelper sig@TypeSignature {..} clauses = do goTopFunctionDef :: forall r. - (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader Pragmas, Error ScoperError, Builtins, NameIdGen] r) => TypeSignature 'Scoped -> [FunctionClause 'Scoped] -> Sem r Abstract.FunctionDef @@ -215,7 +227,7 @@ goTopFunctionDef sig clauses = do goExamples :: forall r. - (Members '[Error ScoperError, InfoTableBuilder] r) => + (Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) => Maybe (Judoc 'Scoped) -> Sem r [Abstract.Example] goExamples = mapM goExample . maybe [] judocExamples @@ -230,7 +242,7 @@ goExamples = mapM goExample . maybe [] judocExamples } goFunctionClause :: - (Members '[Error ScoperError, InfoTableBuilder] r) => + (Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) => FunctionClause 'Scoped -> Sem r Abstract.FunctionClause goFunctionClause FunctionClause {..} = do @@ -244,7 +256,7 @@ goFunctionClause FunctionClause {..} = do } goInductiveParameters :: - (Members '[Error ScoperError, InfoTableBuilder] r) => + (Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) => InductiveParameters 'Scoped -> Sem r [Abstract.FunctionParameter] goInductiveParameters InductiveParameters {..} = do @@ -324,7 +336,7 @@ registerBuiltinAxiom d = \case BuiltinIntPrint -> registerIntPrint d goInductive :: - (Members '[InfoTableBuilder, Builtins, Error ScoperError] r) => + (Members '[InfoTableBuilder, Reader Pragmas, Builtins, Error ScoperError] r) => InductiveDef 'Scoped -> Sem r Abstract.InductiveDef goInductive ty@InductiveDef {..} = do @@ -332,6 +344,7 @@ goInductive ty@InductiveDef {..} = do _inductiveType' <- mapM goExpression _inductiveType _inductiveConstructors' <- mapM goConstructorDef _inductiveConstructors _inductiveExamples' <- goExamples _inductiveDoc + _inductivePragmas' <- goPragmas _inductivePragmas let loc = getLoc _inductiveName indDef = Abstract.InductiveDef @@ -341,7 +354,8 @@ goInductive ty@InductiveDef {..} = do _inductiveType = fromMaybe (Abstract.ExpressionUniverse (smallUniverse loc)) _inductiveType', _inductiveConstructors = toList _inductiveConstructors', _inductiveExamples = _inductiveExamples', - _inductivePositive = ty ^. inductivePositive + _inductivePositive = ty ^. inductivePositive, + _inductivePragmas = _inductivePragmas' } whenJust ((^. withLocParam) <$> _inductiveBuiltin) (registerBuiltinInductive indDef) inductiveInfo <- registerInductive indDef @@ -349,22 +363,24 @@ goInductive ty@InductiveDef {..} = do return (inductiveInfo ^. inductiveInfoDef) goConstructorDef :: - (Members [Error ScoperError, InfoTableBuilder] r) => + (Members [Error ScoperError, Reader Pragmas, InfoTableBuilder] r) => InductiveConstructorDef 'Scoped -> Sem r Abstract.InductiveConstructorDef goConstructorDef InductiveConstructorDef {..} = do ty' <- goExpression _constructorType examples' <- goExamples _constructorDoc + pragmas' <- goPragmas _constructorPragmas return Abstract.InductiveConstructorDef { _constructorType = ty', _constructorExamples = examples', - _constructorName = goSymbol _constructorName + _constructorName = goSymbol _constructorName, + _constructorPragmas = pragmas' } goExpression :: forall r. - (Members [Error ScoperError, InfoTableBuilder] r) => + (Members [Error ScoperError, Reader Pragmas, InfoTableBuilder] r) => Expression -> Sem r Abstract.Expression goExpression = \case @@ -432,7 +448,7 @@ goExpression = \case r' <- goExpression r return (Abstract.Application l'' r' Explicit) -goCase :: forall r. (Members '[Error ScoperError, InfoTableBuilder] r) => Case 'Scoped -> Sem r Abstract.Case +goCase :: forall r. (Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) => Case 'Scoped -> Sem r Abstract.Case goCase c = do _caseExpression <- goExpression (c ^. caseExpression) _caseBranches <- mapM goBranch (c ^. caseBranches) @@ -445,7 +461,7 @@ goCase c = do _caseBranchExpression <- goExpression (b ^. caseBranchExpression) return Abstract.CaseBranch {..} -goLambda :: forall r. (Members '[Error ScoperError, InfoTableBuilder] r) => Lambda 'Scoped -> Sem r Abstract.Lambda +goLambda :: forall r. (Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) => Lambda 'Scoped -> Sem r Abstract.Lambda goLambda l = Abstract.Lambda <$> mapM goClause (l ^. lambdaClauses) where goClause :: LambdaClause 'Scoped -> Sem r Abstract.LambdaClause @@ -457,7 +473,7 @@ goLambda l = Abstract.Lambda <$> mapM goClause (l ^. lambdaClauses) goUniverse :: Universe -> Universe goUniverse = id -goFunction :: (Members '[Error ScoperError, InfoTableBuilder] r) => Function 'Scoped -> Sem r Abstract.Function +goFunction :: (Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) => Function 'Scoped -> Sem r Abstract.Function goFunction f = do params <- goFunctionParameters (f ^. funParameters) ret <- goExpression (f ^. funReturn) @@ -466,7 +482,7 @@ goFunction f = do foldr (\param acc -> Abstract.ExpressionFunction $ Abstract.Function param acc) ret (NonEmpty.tail params) goFunctionParameters :: - (Members '[Error ScoperError, InfoTableBuilder] r) => + (Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) => FunctionParameters 'Scoped -> Sem r (NonEmpty Abstract.FunctionParameter) goFunctionParameters (FunctionParameters {..}) = do @@ -552,14 +568,16 @@ goPattern p = case p of PatternWildcard i -> return (Abstract.PatternWildcard i) PatternEmpty {} -> return Abstract.PatternEmpty -goAxiom :: (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r) => AxiomDef 'Scoped -> Sem r Abstract.AxiomDef +goAxiom :: (Members '[InfoTableBuilder, Reader Pragmas, Error ScoperError, Builtins, NameIdGen] r) => AxiomDef 'Scoped -> Sem r Abstract.AxiomDef goAxiom a = do _axiomType' <- goExpression (a ^. axiomType) + _axiomPragmas' <- goPragmas (a ^. axiomPragmas) let axiom = Abstract.AxiomDef { _axiomType = _axiomType', _axiomBuiltin = (^. withLocParam) <$> a ^. axiomBuiltin, - _axiomName = goSymbol (a ^. axiomName) + _axiomName = goSymbol (a ^. axiomName), + _axiomPragmas = _axiomPragmas' } whenJust (a ^. axiomBuiltin) (registerBuiltinAxiom axiom . (^. withLocParam)) registerAxiom' axiom diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index bf0afc935e..72152ed83b 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -25,7 +25,6 @@ import Juvix.Compiler.Concrete.Data.PublicAnn import Juvix.Compiler.Concrete.Data.ScopedName (unqualifiedSymbol) import Juvix.Compiler.Concrete.Data.ScopedName qualified as S import Juvix.Compiler.Concrete.Data.VisibilityAnn -import Juvix.Compiler.Pragmas import Juvix.Data import Juvix.Data.Ape.Base as Ape import Juvix.Data.Fixity @@ -108,6 +107,17 @@ type family ModuleEndType t = res | res -> t where ModuleEndType 'ModuleTop = () ModuleEndType 'ModuleLocal = KeywordRef +-------------------------------------------------------------------------------- +-- Pragmas +-------------------------------------------------------------------------------- + +-- We keep the exact source of the pragma text. This is necessary, because +-- pragmas are supposed to be backwards-compatible. Unrecognised pragmas +-- should be ignored, but they still need to be printed out when +-- pretty-printing. Also, we probably don't want to impose pragma formatting +-- choices on the user. +type ParsedPragmas = WithSource Pragmas + -------------------------------------------------------------------------------- -- Top level statement -------------------------------------------------------------------------------- @@ -192,7 +202,7 @@ data TypeSignature (s :: Stage) = TypeSignature { _sigName :: FunctionName s, _sigType :: ExpressionType s, _sigDoc :: Maybe (Judoc s), - _sigPragmas :: Maybe Pragmas, + _sigPragmas :: Maybe ParsedPragmas, _sigBuiltin :: Maybe (WithLoc BuiltinFunction), _sigBody :: Maybe (ExpressionType s), _sigTerminating :: Maybe KeywordRef @@ -211,7 +221,7 @@ deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Typ data AxiomDef (s :: Stage) = AxiomDef { _axiomKw :: KeywordRef, _axiomDoc :: Maybe (Judoc s), - _axiomPragmas :: Maybe Pragmas, + _axiomPragmas :: Maybe ParsedPragmas, _axiomName :: SymbolType s, _axiomBuiltin :: Maybe (WithLoc BuiltinAxiom), _axiomType :: ExpressionType s @@ -235,7 +245,7 @@ data InductiveConstructorDef (s :: Stage) = InductiveConstructorDef { _constructorPipe :: Irrelevant (Maybe KeywordRef), _constructorName :: InductiveConstructorName s, _constructorDoc :: Maybe (Judoc s), - _constructorPragmas :: Maybe Pragmas, + _constructorPragmas :: Maybe ParsedPragmas, _constructorType :: ExpressionType s } @@ -260,7 +270,7 @@ data InductiveDef (s :: Stage) = InductiveDef { _inductiveKw :: KeywordRef, _inductiveBuiltin :: Maybe (WithLoc BuiltinInductive), _inductiveDoc :: Maybe (Judoc s), - _inductivePragmas :: Maybe Pragmas, + _inductivePragmas :: Maybe ParsedPragmas, _inductiveName :: InductiveName s, _inductiveParameters :: [InductiveParameters s], _inductiveType :: Maybe (ExpressionType s), @@ -406,7 +416,7 @@ data Module (s :: Stage) (t :: ModuleIsTop) = Module { _moduleKw :: KeywordRef, _modulePath :: ModulePathType s t, _moduleDoc :: Maybe (Judoc s), - _modulePragmas :: Maybe Pragmas, + _modulePragmas :: Maybe ParsedPragmas, _moduleBody :: [Statement s], _moduleKwEnd :: ModuleEndType t } diff --git a/src/Juvix/Compiler/Concrete/Pretty/Base.hs b/src/Juvix/Compiler/Concrete/Pretty/Base.hs index 766c1c0060..60d26f2cf0 100644 --- a/src/Juvix/Compiler/Concrete/Pretty/Base.hs +++ b/src/Juvix/Compiler/Concrete/Pretty/Base.hs @@ -5,14 +5,12 @@ module Juvix.Compiler.Concrete.Pretty.Base ) where -import Data.ByteString.UTF8 qualified as BS import Data.List.NonEmpty.Extra qualified as NonEmpty import Juvix.Compiler.Concrete.Data.ScopedName (AbsModulePath, IsConcrete (..)) import Juvix.Compiler.Concrete.Data.ScopedName qualified as S import Juvix.Compiler.Concrete.Extra (unfoldApplication) import Juvix.Compiler.Concrete.Language import Juvix.Compiler.Concrete.Pretty.Options -import Juvix.Compiler.Pragmas import Juvix.Data.Ape import Juvix.Data.CodeAnn import Juvix.Extra.Strings qualified as Str @@ -365,10 +363,10 @@ instance (SingI s) => PrettyCode (OpenModule s) where Public -> Just kwPublic NoPublic -> Nothing -instance PrettyCode Pragmas where - ppCode Pragmas {..} = +instance PrettyCode ParsedPragmas where + ppCode pragma = return $ - annotate AnnComment (pretty (Str.pragmasStart <> BS.toString _pragmasSource <> Str.pragmasEnd)) <> line + annotate AnnComment (pretty (Str.pragmasStart <> pragma ^. withSourceText <> Str.pragmasEnd)) <> line ppJudocStart :: Doc Ann ppJudocStart = pretty (Str.judocStart :: Text) diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index 847004ca1d..5c3539319b 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -5,13 +5,11 @@ module Juvix.Compiler.Concrete.Print.Base ) where -import Data.ByteString.UTF8 qualified as BS import Data.List.NonEmpty.Extra qualified as NonEmpty import Juvix.Compiler.Concrete.Data.ScopedName qualified as S import Juvix.Compiler.Concrete.Language import Juvix.Compiler.Concrete.Pretty.Base qualified as P import Juvix.Compiler.Concrete.Pretty.Options -import Juvix.Compiler.Pragmas import Juvix.Data.CodeAnn (Ann, CodeAnn (..), ppStringLit) import Juvix.Data.Effect.ExactPrint import Juvix.Data.Keyword.All @@ -142,9 +140,9 @@ instance PrettyPrint OperatorSyntaxDef where instance PrettyPrint Expression where ppCode = ppMorpheme -instance PrettyPrint Pragmas where - ppCode Pragmas {..} = - noLoc (annotate AnnComment (pretty (Str.pragmasStart <> BS.toString _pragmasSource <> Str.pragmasEnd))) +instance PrettyPrint ParsedPragmas where + ppCode pragma = + noLoc (annotate AnnComment (pretty (Str.pragmasStart <> pragma ^. withSourceText <> Str.pragmasEnd))) <> line instance PrettyPrint (Example 'Scoped) where diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 0285630044..6592c6c2b4 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -19,7 +19,6 @@ import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.PathResolver import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context import Juvix.Compiler.Concrete.Translation.FromSource.Lexer hiding (symbol) import Juvix.Compiler.Pipeline.EntryPoint -import Juvix.Compiler.Pragmas import Juvix.Extra.Strings qualified as Str import Juvix.Parser.Error import Juvix.Prelude @@ -27,7 +26,7 @@ import Juvix.Prelude.Pretty (Pretty, prettyText) type JudocStash = State (Maybe (Judoc 'Parsed)) -type PragmasStash = State (Maybe Pragmas) +type PragmasStash = State (Maybe ParsedPragmas) fromSource :: (Members '[PathResolver, Files, Error JuvixError, NameIdGen] r) => @@ -71,7 +70,7 @@ expressionFromTextSource fp txt = mapError (JuvixError @ParserError) $ do runModuleParser :: Members '[Error ParserError, Files, PathResolver, NameIdGen, InfoTableBuilder] r => Path Abs File -> Text -> Sem r (Either ParserError (Module 'Parsed 'ModuleTop)) runModuleParser fileName input = do m <- - evalState (Nothing @Pragmas) $ + evalState (Nothing @ParsedPragmas) $ evalState (Nothing @(Judoc 'Parsed)) $ P.runParserT topModuleDef (toFilePath fileName) input case m of @@ -86,7 +85,7 @@ runExpressionParser :: runExpressionParser fileName input = do m <- runParserInfoTableBuilder $ - evalState (Nothing @Pragmas) $ + evalState (Nothing @ParsedPragmas) $ evalState (Nothing @(Judoc 'Parsed)) $ P.runParserT parseExpressionAtoms (toFilePath fileName) input case m of @@ -183,7 +182,7 @@ stashPragmas = do P.lift (put (Just pragmas)) return () where - parsePragmas :: ParsecS r Pragmas + parsePragmas :: ParsecS r ParsedPragmas parsePragmas = do void (P.chunk Str.pragmasStart) off <- P.getOffset @@ -192,7 +191,7 @@ stashPragmas = do let bs = BS.fromString str case decodeEither' bs of Left err -> parseFailure off (prettyPrintParseException err) - Right pragmas -> return pragmas {_pragmasSource = bs} + Right pragmas -> return $ WithSource (fromString str) pragmas stashJudoc :: forall r. (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r () stashJudoc = do @@ -445,10 +444,10 @@ getJudoc = P.lift $ do put (Nothing @(Judoc 'Parsed)) return j -getPragmas :: (Member PragmasStash r) => ParsecS r (Maybe Pragmas) +getPragmas :: (Member PragmasStash r) => ParsecS r (Maybe ParsedPragmas) getPragmas = P.lift $ do j <- get - put (Nothing @Pragmas) + put (Nothing @ParsedPragmas) return j typeSignature :: diff --git a/src/Juvix/Data.hs b/src/Juvix/Data.hs index 8a3a477653..825d0e2cf0 100644 --- a/src/Juvix/Data.hs +++ b/src/Juvix/Data.hs @@ -8,11 +8,13 @@ module Juvix.Data module Juvix.Data.NameId, module Juvix.Data.Comment, module Juvix.Data.Irrelevant, + module Juvix.Data.Pragmas, module Juvix.Data.Processed, module Juvix.Data.Uid, module Juvix.Data.Universe, module Juvix.Data.Wildcard, module Juvix.Data.WithLoc, + module Juvix.Data.WithSource, module Juvix.Data.DependencyInfo, ) where @@ -27,8 +29,10 @@ import Juvix.Data.Irrelevant import Juvix.Data.IsImplicit import Juvix.Data.Loc import Juvix.Data.NameId qualified +import Juvix.Data.Pragmas import Juvix.Data.Processed import Juvix.Data.Uid import Juvix.Data.Universe import Juvix.Data.Wildcard import Juvix.Data.WithLoc +import Juvix.Data.WithSource diff --git a/src/Juvix/Compiler/Pragmas.hs b/src/Juvix/Data/Pragmas.hs similarity index 70% rename from src/Juvix/Compiler/Pragmas.hs rename to src/Juvix/Data/Pragmas.hs index 285b0f2baa..3e255194e6 100644 --- a/src/Juvix/Compiler/Pragmas.hs +++ b/src/Juvix/Data/Pragmas.hs @@ -1,8 +1,8 @@ -module Juvix.Compiler.Pragmas where +module Juvix.Data.Pragmas where import Data.Aeson.BetterErrors import Data.Yaml -import Juvix.Prelude hiding ((<|>)) +import Juvix.Prelude.Base hiding ((<|>)) data PragmaInline = InlineNever @@ -16,13 +16,7 @@ newtype PragmaUnroll = PragmaUnroll deriving stock (Show, Eq, Ord) data Pragmas = Pragmas - { -- We keep the exact source of the pragma text. This is necessary, because - -- pragmas are supposed to be backwards-compatible. Unrecognised pragmas - -- should be ignored, but they still need to be printed out when - -- pretty-printing. Also, we probably don't want to impose pragma formatting - -- choices on the user. - _pragmasSource :: ByteString, - _pragmasInline :: Maybe PragmaInline, + { _pragmasInline :: Maybe PragmaInline, _pragmasUnroll :: Maybe PragmaUnroll } deriving stock (Show, Eq, Ord) @@ -37,8 +31,6 @@ instance FromJSON Pragmas where where parsePragmas :: Parse PragmaError Pragmas parsePragmas = do - let _pragmasSource :: ByteString - _pragmasSource = "" _pragmasInline <- keyMay "inline" parseInline _pragmasUnroll <- keyMay "unroll" parseUnroll return Pragmas {..} @@ -62,3 +54,21 @@ instance FromJSON Pragmas where parseUnroll = do _pragmaUnrollDepth <- asIntegral return PragmaUnroll {..} + +instance Semigroup Pragmas where + p1 <> p2 = + Pragmas + { _pragmasInline = maybeSecond (p1 ^. pragmasInline) (p2 ^. pragmasInline), + _pragmasUnroll = maybeSecond (p2 ^. pragmasUnroll) (p1 ^. pragmasUnroll) + } + where + maybeSecond :: Maybe a -> Maybe a -> Maybe a + maybeSecond x Nothing = x + maybeSecond _ x@Just {} = x + +instance Monoid Pragmas where + mempty = + Pragmas + { _pragmasInline = Nothing, + _pragmasUnroll = Nothing + } diff --git a/src/Juvix/Data/WithSource.hs b/src/Juvix/Data/WithSource.hs new file mode 100644 index 0000000000..360df8d253 --- /dev/null +++ b/src/Juvix/Data/WithSource.hs @@ -0,0 +1,34 @@ +module Juvix.Data.WithSource where + +import Juvix.Data.Fixity +import Juvix.Prelude.Base + +data WithSource a = WithSource + { _withSourceText :: Text, + _withSourceValue :: a + } + deriving stock (Show, Data) + +makeLenses ''WithSource + +instance (HasAtomicity a) => HasAtomicity (WithSource a) where + atomicity (WithSource _ a) = atomicity a + +instance (Hashable a) => Hashable (WithSource a) where + hashWithSalt a (WithSource _ p) = hashWithSalt a p + +instance (Eq a) => Eq (WithSource a) where + (==) = (==) `on` (^. withSourceValue) + +instance (Ord a) => Ord (WithSource a) where + compare = compare `on` (^. withSourceValue) + +instance Functor WithSource where + fmap = over withSourceValue + +instance Foldable WithSource where + foldMap f (WithSource _ a) = f a + foldr f b (WithSource _ a) = f a b + +instance Traversable WithSource where + traverse f (WithSource i a) = WithSource i <$> f a From 1d6fb415be4d478c7f7986bc633bfe1655c48264 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 14 Apr 2023 14:46:04 +0200 Subject: [PATCH 05/12] propagate pragmas to Internal --- .../Abstract/Translation/FromConcrete.hs | 7 ++++--- src/Juvix/Compiler/Internal/Extra.hs | 11 +++++++---- src/Juvix/Compiler/Internal/Language.hs | 15 ++++++++++----- .../Internal/Translation/FromAbstract.hs | 15 ++++++++++----- .../Analysis/ArityChecking/Checker.hs | 3 +++ .../Analysis/TypeChecking/Checker.hs | 6 ++++-- src/Juvix/Data/Pragmas.hs | 16 +++++++++++++--- 7 files changed, 51 insertions(+), 22 deletions(-) diff --git a/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs b/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs index 050b61cfd6..80a6d4d60e 100644 --- a/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs @@ -7,7 +7,6 @@ where import Data.HashMap.Strict qualified as HashMap import Data.List.NonEmpty qualified as NonEmpty import Juvix.Compiler.Abstract.Data.InfoTableBuilder -import Juvix.Compiler.Abstract.Language (FunctionDef (_funDefExamples)) import Juvix.Compiler.Abstract.Language qualified as Abstract import Juvix.Compiler.Abstract.Translation.FromConcrete.Data.Context import Juvix.Compiler.Builtins @@ -342,9 +341,11 @@ goInductive :: goInductive ty@InductiveDef {..} = do _inductiveParameters' <- concatMapM goInductiveParameters _inductiveParameters _inductiveType' <- mapM goExpression _inductiveType - _inductiveConstructors' <- mapM goConstructorDef _inductiveConstructors - _inductiveExamples' <- goExamples _inductiveDoc _inductivePragmas' <- goPragmas _inductivePragmas + _inductiveConstructors' <- + local (const _inductivePragmas') $ + mapM goConstructorDef _inductiveConstructors + _inductiveExamples' <- goExamples _inductiveDoc let loc = getLoc _inductiveName indDef = Abstract.InductiveDef diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs index bf5280f905..71e007b299 100644 --- a/src/Juvix/Compiler/Internal/Extra.hs +++ b/src/Juvix/Compiler/Internal/Extra.hs @@ -157,7 +157,8 @@ instance HasExpressions FunctionDef where _funDefType = ty', _funDefExamples = examples', _funDefName, - _funDefBuiltin + _funDefBuiltin, + _funDefPragmas } instance HasExpressions InductiveParameter where @@ -176,7 +177,8 @@ instance HasExpressions InductiveDef where _inductiveExamples = examples', _inductiveName, _inductiveBuiltin, - _inductivePositive + _inductivePositive, + _inductivePragmas } instance HasExpressions InductiveConstructorDef where @@ -190,7 +192,8 @@ instance HasExpressions InductiveConstructorDef where { _inductiveConstructorExamples = examples', _inductiveConstructorParameters = args', _inductiveConstructorReturnType = ret', - _inductiveConstructorName + _inductiveConstructorName, + _inductiveConstructorPragmas } fillHolesFunctionDef :: HashMap Hole Expression -> FunctionDef -> FunctionDef @@ -288,7 +291,7 @@ unfoldTypeAbsType t = case t of _ -> ([], t) foldExplicitApplication :: Expression -> [Expression] -> Expression -foldExplicitApplication f = foldApplication f . zip (repeat Explicit) +foldExplicitApplication f = foldApplication f . map (Explicit,) foldApplication :: Expression -> [(IsImplicit, Expression)] -> Expression foldApplication f = \case diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs index c6e9749243..f9ececf516 100644 --- a/src/Juvix/Compiler/Internal/Language.hs +++ b/src/Juvix/Compiler/Internal/Language.hs @@ -20,7 +20,8 @@ import Juvix.Prelude data Module = Module { _moduleName :: Name, _moduleExamples :: [Example], - _moduleBody :: ModuleBody + _moduleBody :: ModuleBody, + _modulePragmas :: Pragmas } deriving stock (Data) @@ -52,7 +53,8 @@ instance Hashable MutualBlock data AxiomDef = AxiomDef { _axiomName :: AxiomName, _axiomBuiltin :: Maybe BuiltinAxiom, - _axiomType :: Expression + _axiomType :: Expression, + _axiomPragmas :: Pragmas } deriving stock (Data) @@ -61,7 +63,8 @@ data FunctionDef = FunctionDef _funDefType :: Expression, _funDefExamples :: [Example], _funDefClauses :: NonEmpty FunctionClause, - _funDefBuiltin :: Maybe BuiltinFunction + _funDefBuiltin :: Maybe BuiltinFunction, + _funDefPragmas :: Pragmas } deriving stock (Eq, Generic, Data) @@ -249,7 +252,8 @@ data InductiveDef = InductiveDef _inductiveExamples :: [Example], _inductiveParameters :: [InductiveParameter], _inductiveConstructors :: [InductiveConstructorDef], - _inductivePositive :: Bool + _inductivePositive :: Bool, + _inductivePragmas :: Pragmas } deriving stock (Data) @@ -257,7 +261,8 @@ data InductiveConstructorDef = InductiveConstructorDef { _inductiveConstructorName :: ConstrName, _inductiveConstructorParameters :: [Expression], _inductiveConstructorExamples :: [Example], - _inductiveConstructorReturnType :: Expression + _inductiveConstructorReturnType :: Expression, + _inductiveConstructorPragmas :: Pragmas } deriving stock (Data) diff --git a/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs b/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs index d976b936d6..c77e63ef84 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs @@ -92,7 +92,8 @@ goModule m = do Module { _moduleName = m ^. Abstract.moduleName, _moduleExamples = examples', - _moduleBody = _moduleBody' + _moduleBody = _moduleBody', + _modulePragmas = m ^. Abstract.modulePragmas } where moduleFunctionDefs :: [Abstract.FunctionDef] @@ -173,7 +174,8 @@ goAxiomDef a = do AxiomDef { _axiomName = a ^. Abstract.axiomName, _axiomBuiltin = a ^. Abstract.axiomBuiltin, - _axiomType = _axiomType' + _axiomType = _axiomType', + _axiomPragmas = a ^. Abstract.axiomPragmas } goFunctionParameter :: Abstract.FunctionParameter -> Sem r FunctionParameter @@ -214,7 +216,8 @@ goFunctionDef f = do _funDefType = _funDefType', _funDefClauses = _funDefClauses', _funDefExamples = _funDefExamples', - _funDefBuiltin = f ^. Abstract.funDefBuiltin + _funDefBuiltin = f ^. Abstract.funDefBuiltin, + _funDefPragmas = f ^. Abstract.funDefPragmas } where _funDefName' :: Name @@ -413,7 +416,8 @@ goInductiveDef i _inductiveBuiltin = i ^. Abstract.inductiveBuiltin, _inductiveConstructors = inductiveConstructors', _inductiveExamples = examples', - _inductivePositive = i ^. Abstract.inductivePositive + _inductivePositive = i ^. Abstract.inductivePositive, + _inductivePragmas = i ^. Abstract.inductivePragmas } where goConstructorDef :: Abstract.InductiveConstructorDef -> Sem r InductiveConstructorDef @@ -425,7 +429,8 @@ goInductiveDef i { _inductiveConstructorName = c ^. Abstract.constructorName, _inductiveConstructorParameters = cParams, _inductiveConstructorExamples = examples', - _inductiveConstructorReturnType = cReturnType + _inductiveConstructorReturnType = cReturnType, + _inductiveConstructorPragmas = c ^. Abstract.constructorPragmas } goTypeApplication :: Abstract.Application -> Sem r Application diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs index d426aa9ba0..7a59501225 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs @@ -58,6 +58,7 @@ checkInductive d = do let _inductiveName = d ^. inductiveName _inductiveBuiltin = d ^. inductiveBuiltin _inductivePositive = d ^. inductivePositive + _inductivePragmas = d ^. inductivePragmas (localVars, _inductiveParameters) <- checkParameters (d ^. inductiveParameters) _inductiveExamples <- runReader localVars (mapM checkExample (d ^. inductiveExamples)) _inductiveConstructors <- runReader localVars (mapM checkConstructor (d ^. inductiveConstructors)) @@ -72,6 +73,7 @@ checkInductive d = do checkConstructor :: (Members '[Reader LocalVars, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => InductiveConstructorDef -> Sem r InductiveConstructorDef checkConstructor c = do let _inductiveConstructorName = c ^. inductiveConstructorName + _inductiveConstructorPragmas = c ^. inductiveConstructorPragmas _inductiveConstructorParameters <- mapM checkType (c ^. inductiveConstructorParameters) _inductiveConstructorExamples <- mapM checkExample (c ^. inductiveConstructorExamples) _inductiveConstructorReturnType <- checkType (c ^. inductiveConstructorReturnType) @@ -85,6 +87,7 @@ checkAxiom :: (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r checkAxiom a = do let _axiomName = a ^. axiomName _axiomBuiltin = a ^. axiomBuiltin + _axiomPragmas = a ^. axiomPragmas _axiomType <- withEmptyLocalVars (checkType (a ^. axiomType)) return AxiomDef {..} diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs index 478c24e43f..23741b9bcf 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs @@ -82,7 +82,8 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do _inductiveName, _inductiveBuiltin, _inductivePositive, - _inductiveParameters + _inductiveParameters, + _inductivePragmas } checkPositivity d return d @@ -106,7 +107,8 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do { _inductiveConstructorParameters = cty', _inductiveConstructorExamples = examples', _inductiveConstructorReturnType, - _inductiveConstructorName + _inductiveConstructorName, + _inductiveConstructorPragmas } registerConstructor c' return c' diff --git a/src/Juvix/Data/Pragmas.hs b/src/Juvix/Data/Pragmas.hs index 3e255194e6..6e56f0cd1f 100644 --- a/src/Juvix/Data/Pragmas.hs +++ b/src/Juvix/Data/Pragmas.hs @@ -8,22 +8,28 @@ data PragmaInline = InlineNever | InlineFullyApplied | InlinePartiallyApplied {_pragmaInlineArgsNum :: Int} - deriving stock (Show, Eq, Ord) + deriving stock (Show, Eq, Ord, Data, Generic) newtype PragmaUnroll = PragmaUnroll { _pragmaUnrollDepth :: Int } - deriving stock (Show, Eq, Ord) + deriving stock (Show, Eq, Ord, Data, Generic) data Pragmas = Pragmas { _pragmasInline :: Maybe PragmaInline, _pragmasUnroll :: Maybe PragmaUnroll } - deriving stock (Show, Eq, Ord) + deriving stock (Show, Eq, Ord, Data, Generic) makeLenses ''PragmaUnroll makeLenses ''Pragmas +instance Hashable PragmaInline + +instance Hashable PragmaUnroll + +instance Hashable Pragmas + type PragmaError = Text instance FromJSON Pragmas where @@ -55,6 +61,10 @@ instance FromJSON Pragmas where _pragmaUnrollDepth <- asIntegral return PragmaUnroll {..} +-- The Semigroup `<>` is used to propagate pragmas from an enclosing context. +-- For example, if `p1` are the pragmas declared for a module `M`, and `p2` the +-- pragmas declared for a function `f` inside `M`, then the actual pragmas for +-- `f` are `p1 <> p2`. instance Semigroup Pragmas where p1 <> p2 = Pragmas From a05a990145a2a15274a8e8606512f084c61fea36 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 14 Apr 2023 14:59:06 +0200 Subject: [PATCH 06/12] propagate pragmas to Core --- src/Juvix/Compiler/Core/Data/InfoTable.hs | 12 ++++++++---- src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs | 12 ++++++++---- src/Juvix/Compiler/Core/Translation/FromInternal.hs | 7 ++++++- src/Juvix/Compiler/Core/Translation/FromSource.hs | 12 ++++++++---- 4 files changed, 30 insertions(+), 13 deletions(-) diff --git a/src/Juvix/Compiler/Core/Data/InfoTable.hs b/src/Juvix/Compiler/Core/Data/InfoTable.hs index 921072f762..4b319e4be5 100644 --- a/src/Juvix/Compiler/Core/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Core/Data/InfoTable.hs @@ -63,7 +63,8 @@ data IdentifierInfo = IdentifierInfo -- | The number of lambdas in the identifier body _identifierArgsNum :: Int, _identifierIsExported :: Bool, - _identifierBuiltin :: Maybe BuiltinFunction + _identifierBuiltin :: Maybe BuiltinFunction, + _identifierPragmas :: Pragmas } data InductiveInfo = InductiveInfo @@ -74,7 +75,8 @@ data InductiveInfo = InductiveInfo _inductiveConstructors :: [Tag], _inductiveParams :: [ParameterInfo], _inductivePositive :: Bool, - _inductiveBuiltin :: Maybe BuiltinType + _inductiveBuiltin :: Maybe BuiltinType, + _inductivePragmas :: Pragmas } data ConstructorInfo = ConstructorInfo @@ -85,7 +87,8 @@ data ConstructorInfo = ConstructorInfo _constructorArgsNum :: Int, _constructorInductive :: Symbol, _constructorFixity :: Maybe Fixity, - _constructorBuiltin :: Maybe BuiltinConstructor + _constructorBuiltin :: Maybe BuiltinConstructor, + _constructorPragmas :: Pragmas } data ParameterInfo = ParameterInfo @@ -98,7 +101,8 @@ data ParameterInfo = ParameterInfo data AxiomInfo = AxiomInfo { _axiomName :: Text, _axiomLocation :: Maybe Location, - _axiomType :: Type + _axiomType :: Type, + _axiomPragmas :: Pragmas } makeLenses ''InfoTable diff --git a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs index 181b909b5c..d7068bd2e9 100644 --- a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs +++ b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs @@ -152,7 +152,8 @@ createBuiltinConstr sym tag nameTxt ty cblt = _constructorArgsNum = length (typeArgs ty), _constructorInductive = sym, _constructorFixity = Nothing, - _constructorBuiltin = cblt + _constructorBuiltin = cblt, + _constructorPragmas = mempty } builtinConstrs :: @@ -183,7 +184,8 @@ declareInductiveBuiltins indName blt ctrs = do _inductiveConstructors = map (^. constructorTag) constrs, _inductivePositive = True, _inductiveParams = [], - _inductiveBuiltin = blt + _inductiveBuiltin = blt, + _inductivePragmas = mempty } ) mapM_ (\ci -> registerConstructor (ci ^. constructorName) ci) constrs @@ -258,7 +260,8 @@ setupLiteralIntToNat mkNode = do _identifierArgsNum = 1, _identifierType = mkPi mempty (Binder "x" Nothing mkTypeInteger') ty, _identifierIsExported = False, - _identifierBuiltin = Nothing + _identifierBuiltin = Nothing, + _identifierPragmas = mempty } targetType :: Sem r Node @@ -292,7 +295,8 @@ setupLiteralIntToInt node = do _identifierArgsNum = 1, _identifierType = mkPi mempty (Binder "x" Nothing mkTypeInteger') ty, _identifierIsExported = False, - _identifierBuiltin = Nothing + _identifierBuiltin = Nothing, + _identifierPragmas = mempty } targetType :: Sem r Node diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index 97977d014d..bbd35530aa 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -126,6 +126,7 @@ goInductiveDef i = do _inductiveParams = params, _inductivePositive = i ^. Internal.inductivePositive, _inductiveBuiltin = fmap BuiltinTypeInductive (i ^. Internal.inductiveBuiltin), + _inductivePragmas = i ^. Internal.inductivePragmas, _inductiveName } idx = mkIdentIndex (i ^. Internal.inductiveName) @@ -156,6 +157,7 @@ goConstructor sym ctor = do _constructorInductive = sym, _constructorBuiltin = mblt, _constructorFixity = ctorName ^. nameFixity, + _constructorPragmas = ctor ^. Internal.inductiveConstructorPragmas, _constructorName } @@ -236,7 +238,8 @@ goFunctionDefIden (f, sym) = do -- body. This needs to be filled in later (in goFunctionDef). _identifierArgsNum = 0, _identifierIsExported = False, - _identifierBuiltin = f ^. Internal.funDefBuiltin + _identifierBuiltin = f ^. Internal.funDefBuiltin, + _identifierPragmas = f ^. Internal.funDefPragmas } case f ^. Internal.funDefBuiltin of Just b @@ -489,6 +492,7 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive _inductiveParams = [], _inductivePositive = False, _inductiveBuiltin = BuiltinTypeAxiom <$> ax, + _inductivePragmas = a ^. Internal.axiomPragmas, _inductiveName } registerInductive (mkIdentIndex (a ^. Internal.axiomName)) info @@ -586,6 +590,7 @@ goAxiomDef a = do _identifierArgsNum = 0, _identifierIsExported = False, _identifierBuiltin = Nothing, + _identifierPragmas = a ^. Internal.axiomPragmas, _identifierName } registerIdent (mkIdentIndex name) info diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs index df05cc8fa3..5eba39843f 100644 --- a/src/Juvix/Compiler/Core/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs @@ -57,7 +57,8 @@ setupMainFunction tab node = _identifierArgsNum = 0, _identifierType = mkDynamic', _identifierBuiltin = Nothing, - _identifierIsExported = True + _identifierIsExported = True, + _identifierPragmas = mempty } guardSymbolNotDefined :: @@ -153,7 +154,8 @@ statementDef = do _identifierType = ty, _identifierArgsNum = 0, _identifierIsExported = False, - _identifierBuiltin = Nothing + _identifierBuiltin = Nothing, + _identifierPragmas = mempty } lift $ registerIdent txt info void $ optional (parseDefinition sym ty) @@ -198,7 +200,8 @@ statementInductive = do _inductiveConstructors = [], _inductiveParams = [], _inductivePositive = True, - _inductiveBuiltin = Nothing + _inductiveBuiltin = Nothing, + _inductivePragmas = mempty } lift $ registerInductive txt ii ctrs <- braces $ P.sepEndBy (constrDecl sym) (kw kwSemicolon) @@ -225,7 +228,8 @@ constrDecl symInd = do _constructorType = ty, _constructorInductive = symInd, _constructorFixity = Nothing, - _constructorBuiltin = Nothing + _constructorBuiltin = Nothing, + _constructorPragmas = mempty } lift $ registerConstructor txt ci return ci From 7d891c2cee593a169b4104a68a28b5223d564d86 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 14 Apr 2023 15:11:57 +0200 Subject: [PATCH 07/12] fix compilation --- app/Commands/Repl.hs | 3 ++- .../Compiler/Core/Transformation/LambdaLetRecLifting.hs | 6 ++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/app/Commands/Repl.hs b/app/Commands/Repl.hs index 9d72582fb5..4b4486efbb 100644 --- a/app/Commands/Repl.hs +++ b/app/Commands/Repl.hs @@ -386,7 +386,8 @@ runTransformations shouldDisambiguate ts n = runCoreInfoTableBuilderArtifacts $ _identifierArgsNum = 0, _identifierType = Core.mkDynamic', _identifierIsExported = False, - _identifierBuiltin = Nothing + _identifierBuiltin = Nothing, + _identifierPragmas = mempty } Core.registerIdent name idenInfo return sym diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLetRecLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLetRecLifting.hs index aeb8f2f542..0308035077 100644 --- a/src/Juvix/Compiler/Core/Transformation/LambdaLetRecLifting.hs +++ b/src/Juvix/Compiler/Core/Transformation/LambdaLetRecLifting.hs @@ -67,7 +67,8 @@ lambdaLiftNode aboveBl top = _identifierType = ty, _identifierArgsNum = argsNum, _identifierIsExported = False, - _identifierBuiltin = Nothing + _identifierBuiltin = Nothing, + _identifierPragmas = mempty } registerIdentNode f fBody' let fApp = mkApps' (mkIdent (setInfoName name mempty) f) (map NVar allfreevars) @@ -138,7 +139,8 @@ lambdaLiftNode aboveBl top = _identifierType = topTy, _identifierArgsNum = argsNum, _identifierIsExported = False, - _identifierBuiltin = Nothing + _identifierBuiltin = Nothing, + _identifierPragmas = mempty } | ((sym, name), (itemBinder, (b, bty))) <- zipExact From 58a57e8c6accc6f7159a6f69803207eaca5af077 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Mon, 24 Apr 2023 12:10:44 +0200 Subject: [PATCH 08/12] unroll pragma --- .../Core/Transformation/UnrollRecursion.hs | 15 ++++++++++++++- test/BackendGeb/Compilation/Positive.hs | 7 ++++++- tests/Geb/positive/Compilation/out/test030.geb | 1 + tests/Geb/positive/Compilation/test030.juvix | 12 ++++++++++++ 4 files changed, 33 insertions(+), 2 deletions(-) create mode 100644 tests/Geb/positive/Compilation/out/test030.geb create mode 100644 tests/Geb/positive/Compilation/test030.juvix diff --git a/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs b/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs index ae024e3ce4..bfec100920 100644 --- a/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs +++ b/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs @@ -37,11 +37,24 @@ unrollRecursion tab = do unrollSCC :: Members '[InfoTableBuilder, State (HashMap Symbol Symbol), Reader CoreOptions] r => [Symbol] -> Sem r () unrollSCC syms = do - unrollLimit <- asks (^. optUnrollLimit) + unrollLimit <- computeUnrollLimit freshSyms <- genSyms unrollLimit syms forM_ syms (unroll unrollLimit freshSyms) modify (\mp -> foldr (mapSymbol unrollLimit freshSyms) mp syms) where + computeUnrollLimit :: Member (Reader CoreOptions) r => Sem r Int + computeUnrollLimit = do + defaultUnrollLimit <- asks (^. optUnrollLimit) + let lims = mapMaybe go syms + if + | null lims -> return defaultUnrollLimit + | otherwise -> return $ minimum lims + where + go :: Symbol -> Maybe Int + go sym = fmap (^. pragmaUnrollDepth) (ii ^. identifierPragmas . pragmasUnroll) + where + ii = lookupIdentifierInfo tab sym + mapSymbol :: Int -> HashMap (Indexed Symbol) Symbol -> Symbol -> HashMap Symbol Symbol -> HashMap Symbol Symbol mapSymbol unrollLimit freshSyms sym = HashMap.insert sym (fromJust $ HashMap.lookup (Indexed unrollLimit sym) freshSyms) diff --git a/test/BackendGeb/Compilation/Positive.hs b/test/BackendGeb/Compilation/Positive.hs index 5de31d5382..82459682ac 100644 --- a/test/BackendGeb/Compilation/Positive.hs +++ b/test/BackendGeb/Compilation/Positive.hs @@ -178,5 +178,10 @@ tests = "Test029: pattern matching on natural numbers" $(mkRelDir ".") $(mkRelFile "test029.juvix") - $(mkRelFile "out/test029.geb") + $(mkRelFile "out/test029.geb"), + PosTest + "Test030: recursion with unroll pragma" + $(mkRelDir ".") + $(mkRelFile "test030.juvix") + $(mkRelFile "out/test030.geb") ] diff --git a/tests/Geb/positive/Compilation/out/test030.geb b/tests/Geb/positive/Compilation/out/test030.geb new file mode 100644 index 0000000000..c3f407c095 --- /dev/null +++ b/tests/Geb/positive/Compilation/out/test030.geb @@ -0,0 +1 @@ +55 diff --git a/tests/Geb/positive/Compilation/test030.juvix b/tests/Geb/positive/Compilation/test030.juvix new file mode 100644 index 0000000000..1ca7d7df7d --- /dev/null +++ b/tests/Geb/positive/Compilation/test030.juvix @@ -0,0 +1,12 @@ +-- recursion with unroll pragma +module test013; + +open import Stdlib.Prelude; + +{-# unroll: 11 #-} +sum : Nat → Nat; +sum zero := 0; +sum (suc x) := suc x + sum x; + +main : Nat; +main := sum 10; From b7e41878f218148eb72730631cce66fdfe3bbd84 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Tue, 25 Apr 2023 12:08:07 +0200 Subject: [PATCH 09/12] fix formatting --- src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs | 2 +- src/Juvix/Compiler/Concrete/Language.hs | 3 ++- src/Juvix/Compiler/Concrete/Pretty/Base.hs | 2 +- src/Juvix/Compiler/Concrete/Print/Base.hs | 5 +---- src/Juvix/Compiler/Concrete/Translation/FromSource.hs | 6 +++--- tests/positive/Pragmas.juvix | 1 + 6 files changed, 9 insertions(+), 10 deletions(-) diff --git a/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs b/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs index e851998fed..f236c5154c 100644 --- a/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs @@ -92,7 +92,7 @@ goModule m = case sing :: SModuleIsTop t of goPragmas :: Member (Reader Pragmas) r => Maybe ParsedPragmas -> Sem r Pragmas goPragmas p = do p' <- ask - return $ p' <> maybe mempty (^. withSourceValue) p + return $ p' <> maybe mempty (^. withLocParam . withSourceValue) p goName :: S.Name -> Abstract.Name goName name = diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index 3fb16824f2..8088a636cf 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -116,7 +116,7 @@ type family ModuleEndType t = res | res -> t where -- should be ignored, but they still need to be printed out when -- pretty-printing. Also, we probably don't want to impose pragma formatting -- choices on the user. -type ParsedPragmas = WithSource Pragmas +type ParsedPragmas = WithLoc (WithSource Pragmas) -------------------------------------------------------------------------------- -- Top level statement @@ -1176,6 +1176,7 @@ getJudocLoc = fmap getLocSpan . nonEmpty . (^. block) instance SingI s => HasLoc (TypeSignature s) where getLoc TypeSignature {..} = (_sigDoc >>= getJudocLoc) + ?<> (getLoc <$> _sigPragmas) ?<> (getLoc <$> _sigBuiltin) ?<> (getLoc <$> _sigTerminating) ?<> (getLocExpressionType <$> _sigBody) diff --git a/src/Juvix/Compiler/Concrete/Pretty/Base.hs b/src/Juvix/Compiler/Concrete/Pretty/Base.hs index fcc59b3dbf..b2aa9d7983 100644 --- a/src/Juvix/Compiler/Concrete/Pretty/Base.hs +++ b/src/Juvix/Compiler/Concrete/Pretty/Base.hs @@ -368,7 +368,7 @@ instance (SingI s) => PrettyCode (OpenModule s) where Public -> Just kwPublic NoPublic -> Nothing -instance PrettyCode ParsedPragmas where +instance PrettyCode (WithSource Pragmas) where ppCode pragma = return $ annotate AnnComment (pretty (Str.pragmasStart <> pragma ^. withSourceText <> Str.pragmasEnd)) <> line diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index d5e08d8027..8b699b35c4 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -13,7 +13,6 @@ import Juvix.Compiler.Concrete.Pretty.Options import Juvix.Data.CodeAnn (Ann, CodeAnn (..), ppStringLit) import Juvix.Data.Effect.ExactPrint import Juvix.Data.Keyword.All -import Juvix.Extra.Strings qualified as Str import Juvix.Prelude hiding ((<+>), (<+?>), (), (?<>)) import Juvix.Prelude.Pretty (annotate, pretty) @@ -151,9 +150,7 @@ instance PrettyPrint Expression where ppCode = ppMorpheme instance PrettyPrint ParsedPragmas where - ppCode pragma = - noLoc (annotate AnnComment (pretty (Str.pragmasStart <> pragma ^. withSourceText <> Str.pragmasEnd))) - <> line + ppCode = ppMorpheme instance PrettyPrint (Example 'Scoped) where ppCode e = diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 43b0acea6b..a57e4179de 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -177,12 +177,12 @@ statement = P.label "" $ do stashPragmas :: forall r. (Members '[InfoTableBuilder, PragmasStash, NameIdGen] r) => ParsecS r () stashPragmas = do - (pragmas, i) <- interval parsePragmas - P.lift (registerPragmas i) + pragmas <- withLoc parsePragmas + P.lift (registerPragmas (getLoc pragmas)) P.lift (put (Just pragmas)) return () where - parsePragmas :: ParsecS r ParsedPragmas + parsePragmas :: ParsecS r (WithSource Pragmas) parsePragmas = do void (P.chunk Str.pragmasStart) off <- P.getOffset diff --git a/tests/positive/Pragmas.juvix b/tests/positive/Pragmas.juvix index 9aa26abdc5..1c5638394f 100644 --- a/tests/positive/Pragmas.juvix +++ b/tests/positive/Pragmas.juvix @@ -1,3 +1,4 @@ +{-# unknownPragma: 300 #-} module Pragmas; open import Stdlib.Prelude; From e99a37ad127345f363e6c376be29c3d259269057 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Tue, 25 Apr 2023 12:17:42 +0200 Subject: [PATCH 10/12] test axiom pragmas --- tests/positive/Pragmas.juvix | 3 +++ 1 file changed, 3 insertions(+) diff --git a/tests/positive/Pragmas.juvix b/tests/positive/Pragmas.juvix index 1c5638394f..5eb0f671f8 100644 --- a/tests/positive/Pragmas.juvix +++ b/tests/positive/Pragmas.juvix @@ -3,6 +3,9 @@ module Pragmas; open import Stdlib.Prelude; +{-# unknownPragma: 0 #-} +axiom a : Nat; + {-# unknownPragma: something unroll: 100 From 08b9b5d73330444567932332c1bd1b5f0be42342 Mon Sep 17 00:00:00 2001 From: janmasrovira Date: Tue, 25 Apr 2023 18:38:57 +0200 Subject: [PATCH 11/12] Small style adjustments (#2030) --- .../Abstract/Translation/FromConcrete.hs | 2 +- src/Juvix/Compiler/Concrete/Print/Base.hs | 4 ++-- .../Concrete/Translation/FromSource.hs | 1 - .../Core/Transformation/UnrollRecursion.hs | 6 ++---- src/Juvix/Data/Pragmas.hs | 19 ++++++++----------- src/Juvix/Parser/Lexer.hs | 1 + 6 files changed, 14 insertions(+), 19 deletions(-) diff --git a/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs b/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs index f236c5154c..23c93eabb9 100644 --- a/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs @@ -92,7 +92,7 @@ goModule m = case sing :: SModuleIsTop t of goPragmas :: Member (Reader Pragmas) r => Maybe ParsedPragmas -> Sem r Pragmas goPragmas p = do p' <- ask - return $ p' <> maybe mempty (^. withLocParam . withSourceValue) p + return $ p' <> p ^. _Just . withLocParam . withSourceValue goName :: S.Name -> Abstract.Name goName name = diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index 8b699b35c4..790949f134 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -60,8 +60,8 @@ instance SingI t => PrettyPrint (Module 'Scoped t) where ppCode Module {..} = do let moduleBody' = localIndent (ppCode _moduleBody) modulePath' = ppModulePathType _modulePath - moduleDoc' :: Sem r () = maybe (return ()) ppCode _moduleDoc - modulePragmas' :: Sem r () = maybe (return ()) ppCode _modulePragmas + moduleDoc' = whenJust _moduleDoc ppCode + modulePragmas' = whenJust _modulePragmas ppCode body' | null _moduleBody = ensureEmptyLine | otherwise = diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index a57e4179de..dd9e4db74e 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -180,7 +180,6 @@ stashPragmas = do pragmas <- withLoc parsePragmas P.lift (registerPragmas (getLoc pragmas)) P.lift (put (Just pragmas)) - return () where parsePragmas :: ParsecS r (WithSource Pragmas) parsePragmas = do diff --git a/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs b/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs index bfec100920..25a4668dd3 100644 --- a/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs +++ b/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs @@ -45,10 +45,8 @@ unrollRecursion tab = do computeUnrollLimit :: Member (Reader CoreOptions) r => Sem r Int computeUnrollLimit = do defaultUnrollLimit <- asks (^. optUnrollLimit) - let lims = mapMaybe go syms - if - | null lims -> return defaultUnrollLimit - | otherwise -> return $ minimum lims + let lims = nonEmpty (mapMaybe go syms) + return (maybe defaultUnrollLimit minimum1 lims) where go :: Symbol -> Maybe Int go sym = fmap (^. pragmaUnrollDepth) (ii ^. identifierPragmas . pragmasUnroll) diff --git a/src/Juvix/Data/Pragmas.hs b/src/Juvix/Data/Pragmas.hs index 6e56f0cd1f..4c317af0d7 100644 --- a/src/Juvix/Data/Pragmas.hs +++ b/src/Juvix/Data/Pragmas.hs @@ -1,8 +1,9 @@ module Juvix.Data.Pragmas where -import Data.Aeson.BetterErrors +import Data.Aeson.BetterErrors hiding ((<|>)) +import Data.Aeson.BetterErrors qualified as Aeson import Data.Yaml -import Juvix.Prelude.Base hiding ((<|>)) +import Juvix.Prelude.Base data PragmaInline = InlineNever @@ -42,12 +43,12 @@ instance FromJSON Pragmas where return Pragmas {..} parseInline :: Parse PragmaError PragmaInline - parseInline = parseInlineArgsNum <|> parseInlineBool + parseInline = parseInlineArgsNum Aeson.<|> parseInlineBool where parseInlineArgsNum :: Parse PragmaError PragmaInline parseInlineArgsNum = do _pragmaInlineArgsNum <- asIntegral - return $ InlinePartiallyApplied {..} + return InlinePartiallyApplied {..} parseInlineBool :: Parse PragmaError PragmaInline parseInlineBool = do @@ -61,20 +62,16 @@ instance FromJSON Pragmas where _pragmaUnrollDepth <- asIntegral return PragmaUnroll {..} --- The Semigroup `<>` is used to propagate pragmas from an enclosing context. +-- | The Semigroup `<>` is used to propagate pragmas from an enclosing context. -- For example, if `p1` are the pragmas declared for a module `M`, and `p2` the -- pragmas declared for a function `f` inside `M`, then the actual pragmas for -- `f` are `p1 <> p2`. instance Semigroup Pragmas where p1 <> p2 = Pragmas - { _pragmasInline = maybeSecond (p1 ^. pragmasInline) (p2 ^. pragmasInline), - _pragmasUnroll = maybeSecond (p2 ^. pragmasUnroll) (p1 ^. pragmasUnroll) + { _pragmasInline = p2 ^. pragmasInline <|> p1 ^. pragmasInline, + _pragmasUnroll = p1 ^. pragmasUnroll <|> p2 ^. pragmasUnroll } - where - maybeSecond :: Maybe a -> Maybe a -> Maybe a - maybeSecond x Nothing = x - maybeSecond _ x@Just {} = x instance Monoid Pragmas where mempty = diff --git a/src/Juvix/Parser/Lexer.hs b/src/Juvix/Parser/Lexer.hs index 8571a7feb9..33f03aaa37 100644 --- a/src/Juvix/Parser/Lexer.hs +++ b/src/Juvix/Parser/Lexer.hs @@ -38,6 +38,7 @@ hspace_ = void hspace spaceMsg :: String spaceMsg = "white space (only spaces and newlines allowed)" +-- | `special` is set when judoc comments or pragmas are supported space' :: forall e m. MonadParsec e Text m => Bool -> m (Maybe SpaceSpan) space' special = hidden $ From 1638988bf4744f1c31b97baec8f7e6388e971e09 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 26 Apr 2023 12:43:36 +0200 Subject: [PATCH 12/12] fix pragma priority --- src/Juvix/Data/Pragmas.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Juvix/Data/Pragmas.hs b/src/Juvix/Data/Pragmas.hs index 4c317af0d7..d1065bb26e 100644 --- a/src/Juvix/Data/Pragmas.hs +++ b/src/Juvix/Data/Pragmas.hs @@ -70,7 +70,7 @@ instance Semigroup Pragmas where p1 <> p2 = Pragmas { _pragmasInline = p2 ^. pragmasInline <|> p1 ^. pragmasInline, - _pragmasUnroll = p1 ^. pragmasUnroll <|> p2 ^. pragmasUnroll + _pragmasUnroll = p2 ^. pragmasUnroll <|> p1 ^. pragmasUnroll } instance Monoid Pragmas where