From e43797f0a033e52b504bb597e008b7a734b0ef65 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 21 Jun 2024 15:02:30 +0200 Subject: [PATCH] Generalize import syntax (#2819) - Closes #2429 This pr introduces two enchancements to import statements: 1. They can have `using/hiding` list of symbols, with a behaviour analogous to the open statement. 2. They can be public. When an import is marked as public, a local module (or a series of nested local modules) is generated like this: ``` import A public; -- equivalent to import A; module A; open A public; end; ``` It is easier to understand when there is an alias. ``` import A as X.Y public; -- equivalent to import A; module X; module Y; open A public; end; end; ``` Public imports are allowed to be combined with `using/hiding` modifier and open statements with the expected behaviour. --- .../Backend/Html/Translation/FromTyped.hs | 19 +- .../Markdown/Translation/FromTyped/Source.hs | 3 +- src/Juvix/Compiler/Concrete/Data.hs | 4 + .../Compiler/Concrete/Data/IsOpenShort.hs | 10 + .../Concrete/Data/LocalModuleOrigin.hs | 12 + src/Juvix/Compiler/Concrete/Data/PublicAnn.hs | 7 +- src/Juvix/Compiler/Concrete/Language.hs | 121 +++-- src/Juvix/Compiler/Concrete/Print/Base.hs | 51 +- .../FromParsed/Analysis/Scoping.hs | 489 ++++++++++++------ .../Analysis/Scoping/Error/Types.hs | 4 +- .../Concrete/Translation/FromSource.hs | 51 +- src/Juvix/Compiler/Pipeline/Package/Loader.hs | 31 +- src/Juvix/Compiler/Pipeline/Repl.hs | 2 +- src/Juvix/Data/Effect/ExactPrint.hs | 8 + src/Juvix/Prelude/Base/Foundation.hs | 8 + test/Scope/Positive.hs | 6 +- tests/positive/DefaultValues.juvix | 55 -- tests/positive/Format.juvix | 9 + tests/positive/PublicImports/M.juvix | 3 + tests/positive/PublicImports/Main.juvix | 30 ++ tests/positive/PublicImports/Package.juvix | 5 + 21 files changed, 593 insertions(+), 335 deletions(-) create mode 100644 src/Juvix/Compiler/Concrete/Data/IsOpenShort.hs create mode 100644 src/Juvix/Compiler/Concrete/Data/LocalModuleOrigin.hs delete mode 100644 tests/positive/DefaultValues.juvix create mode 100644 tests/positive/PublicImports/M.juvix create mode 100644 tests/positive/PublicImports/Main.juvix create mode 100644 tests/positive/PublicImports/Package.juvix diff --git a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs index 1043150e44..16a3bc3f9a 100644 --- a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs @@ -486,7 +486,7 @@ goAlias def = do -- | local modules generated by inductive types should not show up. goLocalModule :: forall r. (Members '[Reader HtmlOptions] r) => Module 'Scoped 'ModuleLocal -> Sem r Html goLocalModule def = fmap (fromMaybe mempty) . runFail $ do - failWhen (def ^. moduleInductive) + failUnless (def ^. moduleOrigin == LocalModuleSource) sig' <- ppHelper (ppModuleHeader def) header' <- defHeader (def ^. modulePath) sig' (def ^. moduleDoc) body' <- @@ -498,13 +498,24 @@ goLocalModule def = fmap (fromMaybe mempty) . runFail $ do goImport :: forall r. (Members '[Reader HtmlOptions] r) => Import 'Scoped -> Sem r Html goImport op - | Just Public <- op ^? importOpen . _Just . openPublic = noDefHeader <$> ppCodeHtml defaultOptions op + | shouldBeDocumented = noDefHeader <$> ppCodeHtml defaultOptions op | otherwise = mempty + where + shouldBeDocumented :: Bool + shouldBeDocumented + | Just Public {} <- op ^? importOpen . _Just . openModulePublic = True + | Just Public {} <- op ^? importPublic = True + | otherwise = False -goOpen :: forall r. (Members '[Reader HtmlOptions] r) => OpenModule 'Scoped -> Sem r Html +goOpen :: forall r. (Members '[Reader HtmlOptions] r) => OpenModule 'Scoped 'OpenFull -> Sem r Html goOpen op - | Public <- op ^. openModuleParams . openPublic = noDefHeader <$> ppCodeHtml defaultOptions op + | shouldBeDocumented = noDefHeader <$> ppCodeHtml defaultOptions op | otherwise = mempty + where + shouldBeDocumented :: Bool + shouldBeDocumented + | Public {} <- op ^. openModulePublic = True + | otherwise = False goAxiom :: forall r. (Members '[Reader HtmlOptions] r) => AxiomDef 'Scoped -> Sem r Html goAxiom axiom = do diff --git a/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs b/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs index 247c72de25..b2e9822fd2 100644 --- a/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs +++ b/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs @@ -7,6 +7,7 @@ import Juvix.Compiler.Backend.Html.Data.Options qualified as HtmlRender import Juvix.Compiler.Backend.Html.Translation.FromTyped.Source qualified as HtmlRender import Juvix.Compiler.Backend.Markdown.Data.Types import Juvix.Compiler.Backend.Markdown.Error +import Juvix.Compiler.Concrete.Data.LocalModuleOrigin import Juvix.Compiler.Concrete.Language qualified as Concrete import Juvix.Compiler.Concrete.Pretty qualified as Concrete import Juvix.Prelude @@ -216,7 +217,7 @@ indModuleFilter = Concrete.StatementFunctionDef _ -> True Concrete.StatementImport _ -> True Concrete.StatementInductive _ -> True - Concrete.StatementModule o -> not (o ^. Concrete.moduleInductive) + Concrete.StatementModule o -> o ^. Concrete.moduleOrigin == LocalModuleSource Concrete.StatementOpenModule _ -> True Concrete.StatementAxiom _ -> True Concrete.StatementProjectionDef _ -> True diff --git a/src/Juvix/Compiler/Concrete/Data.hs b/src/Juvix/Compiler/Concrete/Data.hs index 510eaa2db4..dd842a64ff 100644 --- a/src/Juvix/Compiler/Concrete/Data.hs +++ b/src/Juvix/Compiler/Concrete/Data.hs @@ -12,6 +12,8 @@ module Juvix.Compiler.Concrete.Data module Juvix.Compiler.Concrete.Data.VisibilityAnn, module Juvix.Compiler.Concrete.Data.Literal, module Juvix.Compiler.Concrete.Data.NameRef, + module Juvix.Compiler.Concrete.Data.IsOpenShort, + module Juvix.Compiler.Concrete.Data.LocalModuleOrigin, module Juvix.Data.NameId, ) where @@ -19,7 +21,9 @@ where import Juvix.Compiler.Concrete.Data.Builtins import Juvix.Compiler.Concrete.Data.Highlight import Juvix.Compiler.Concrete.Data.InfoTableBuilder +import Juvix.Compiler.Concrete.Data.IsOpenShort import Juvix.Compiler.Concrete.Data.Literal +import Juvix.Compiler.Concrete.Data.LocalModuleOrigin import Juvix.Compiler.Concrete.Data.ModuleIsTop import Juvix.Compiler.Concrete.Data.Name import Juvix.Compiler.Concrete.Data.NameRef diff --git a/src/Juvix/Compiler/Concrete/Data/IsOpenShort.hs b/src/Juvix/Compiler/Concrete/Data/IsOpenShort.hs new file mode 100644 index 0000000000..4ef768b47b --- /dev/null +++ b/src/Juvix/Compiler/Concrete/Data/IsOpenShort.hs @@ -0,0 +1,10 @@ +module Juvix.Compiler.Concrete.Data.IsOpenShort where + +import Juvix.Prelude + +data IsOpenShort + = OpenFull + | OpenShort + deriving stock (Eq, Ord, Show, Generic, Data, Enum, Bounded) + +$(genSingletons [''IsOpenShort]) diff --git a/src/Juvix/Compiler/Concrete/Data/LocalModuleOrigin.hs b/src/Juvix/Compiler/Concrete/Data/LocalModuleOrigin.hs new file mode 100644 index 0000000000..39ef3f3635 --- /dev/null +++ b/src/Juvix/Compiler/Concrete/Data/LocalModuleOrigin.hs @@ -0,0 +1,12 @@ +module Juvix.Compiler.Concrete.Data.LocalModuleOrigin where + +import Juvix.Prelude + +data LocalModuleOrigin + = -- | The local module was in the source code + LocalModuleSource + | -- | The local module was inserted because of a type definition + LocalModuleType + | -- | The local module was inserted because of a public import + LocalModulePublicImport + deriving stock (Eq, Ord, Show, Generic, Data, Enum, Bounded) diff --git a/src/Juvix/Compiler/Concrete/Data/PublicAnn.hs b/src/Juvix/Compiler/Concrete/Data/PublicAnn.hs index 8ca4ae99f0..e28dd4f27b 100644 --- a/src/Juvix/Compiler/Concrete/Data/PublicAnn.hs +++ b/src/Juvix/Compiler/Concrete/Data/PublicAnn.hs @@ -5,7 +5,7 @@ import Juvix.Prelude data PublicAnn = -- | Explicit public annotation - Public + Public (Irrelevant KeywordRef) | -- | No annotation. Do not confuse this with 'not public' or 'private'. NoPublic deriving stock (Show, Eq, Ord, Generic) @@ -13,3 +13,8 @@ data PublicAnn instance Serialize PublicAnn instance NFData PublicAnn + +_Public :: Traversal' PublicAnn KeywordRef +_Public f = \case + NoPublic -> pure NoPublic + Public (Irrelevant x) -> Public . Irrelevant <$> f x diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index 1454d9295c..70b270b387 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -3,6 +3,8 @@ module Juvix.Compiler.Concrete.Language ( module Juvix.Compiler.Concrete.Language, module Juvix.Data.FixityInfo, + module Juvix.Compiler.Concrete.Data.IsOpenShort, + module Juvix.Compiler.Concrete.Data.LocalModuleOrigin, module Juvix.Data.IteratorInfo, module Juvix.Compiler.Concrete.Data.Name, module Juvix.Compiler.Concrete.Data.Stage, @@ -21,7 +23,9 @@ where import Data.Kind qualified as GHC import Juvix.Compiler.Backend.Markdown.Data.Types (Mk) import Juvix.Compiler.Concrete.Data.Builtins +import Juvix.Compiler.Concrete.Data.IsOpenShort import Juvix.Compiler.Concrete.Data.Literal +import Juvix.Compiler.Concrete.Data.LocalModuleOrigin import Juvix.Compiler.Concrete.Data.ModuleIsTop import Juvix.Compiler.Concrete.Data.Name import Juvix.Compiler.Concrete.Data.NameRef @@ -110,6 +114,11 @@ type family ModulePathType s t = res | res -> t s where ModulePathType 'Parsed 'ModuleLocal = Symbol ModulePathType 'Scoped 'ModuleLocal = S.Symbol +type OpenModuleNameType :: Stage -> IsOpenShort -> GHC.Type +type family OpenModuleNameType s short = res where + OpenModuleNameType s 'OpenFull = ModuleNameType s + OpenModuleNameType _ 'OpenShort = () + type ModuleNameType :: Stage -> GHC.Type type family ModuleNameType s = res | res -> s where ModuleNameType 'Parsed = Name @@ -118,7 +127,7 @@ type family ModuleNameType s = res | res -> s where type ModuleInductiveType :: ModuleIsTop -> GHC.Type type family ModuleInductiveType t = res | res -> t where ModuleInductiveType 'ModuleTop = () - ModuleInductiveType 'ModuleLocal = Bool + ModuleInductiveType 'ModuleLocal = LocalModuleOrigin type ModuleEndType :: ModuleIsTop -> GHC.Type type family ModuleEndType t = res | res -> t where @@ -254,7 +263,7 @@ data Definition (s :: Stage) data NonDefinition (s :: Stage) = NonDefinitionImport (Import s) | NonDefinitionModule (Module s 'ModuleLocal) - | NonDefinitionOpenModule (OpenModule s) + | NonDefinitionOpenModule (OpenModule s 'OpenFull) data Statement (s :: Stage) = StatementSyntax (SyntaxDef s) @@ -262,7 +271,7 @@ data Statement (s :: Stage) | StatementImport (Import s) | StatementInductive (InductiveDef s) | StatementModule (Module s 'ModuleLocal) - | StatementOpenModule (OpenModule s) + | StatementOpenModule (OpenModule s 'OpenFull) | StatementAxiom (AxiomDef s) | StatementProjectionDef (ProjectionDef s) @@ -301,7 +310,9 @@ data Import (s :: Stage) = Import { _importKw :: KeywordRef, _importModulePath :: ModulePathType s 'ModuleTop, _importAsName :: Maybe (ModulePathType s 'ModuleTop), - _importOpen :: Maybe (OpenModuleParams s) + _importUsingHiding :: Maybe (UsingHiding s), + _importPublic :: PublicAnn, + _importOpen :: Maybe (OpenModule s 'OpenShort) } deriving stock instance Show (Import 'Parsed) @@ -1185,7 +1196,7 @@ data Module (s :: Stage) (t :: ModuleIsTop) = Module _modulePragmas :: Maybe ParsedPragmas, _moduleBody :: [Statement s], _moduleKwEnd :: ModuleEndType t, - _moduleInductive :: ModuleInductiveType t, + _moduleOrigin :: ModuleInductiveType t, _moduleId :: ModuleIdType s, _moduleMarkdownInfo :: Maybe MarkdownInfo } @@ -1352,59 +1363,53 @@ getNameRefId = case sing :: S.SIsConcrete c of S.SConcrete -> (^. S.nameId) S.SNotConcrete -> (^. S.nameId) -data OpenModule (s :: Stage) = OpenModule - { _openModuleName :: ModuleNameType s, - _openModuleParams :: OpenModuleParams s +data OpenModule (s :: Stage) (short :: IsOpenShort) = OpenModule + { _openModuleKw :: KeywordRef, + _openModuleName :: OpenModuleNameType s short, + _openModuleUsingHiding :: Maybe (UsingHiding s), + _openModulePublic :: PublicAnn } deriving stock (Generic) -instance Serialize (OpenModule 'Scoped) - -instance NFData (OpenModule 'Scoped) +instance Serialize (OpenModule 'Scoped 'OpenFull) -instance Serialize (OpenModule 'Parsed) +instance Serialize (OpenModule 'Scoped 'OpenShort) -instance NFData (OpenModule 'Parsed) +instance NFData (OpenModule 'Scoped 'OpenFull) -deriving stock instance Show (OpenModule 'Parsed) +instance NFData (OpenModule 'Scoped 'OpenShort) -deriving stock instance Show (OpenModule 'Scoped) +instance Serialize (OpenModule 'Parsed 'OpenFull) -deriving stock instance Eq (OpenModule 'Parsed) +instance Serialize (OpenModule 'Parsed 'OpenShort) -deriving stock instance Eq (OpenModule 'Scoped) +instance NFData (OpenModule 'Parsed 'OpenShort) -deriving stock instance Ord (OpenModule 'Parsed) +instance NFData (OpenModule 'Parsed 'OpenFull) -deriving stock instance Ord (OpenModule 'Scoped) +deriving stock instance Show (OpenModule 'Parsed 'OpenShort) -data OpenModuleParams (s :: Stage) = OpenModuleParams - { _openModuleKw :: KeywordRef, - _openUsingHiding :: Maybe (UsingHiding s), - _openPublicKw :: Irrelevant (Maybe KeywordRef), - _openPublic :: PublicAnn - } - deriving stock (Generic) +deriving stock instance Show (OpenModule 'Parsed 'OpenFull) -instance Serialize (OpenModuleParams 'Scoped) +deriving stock instance Show (OpenModule 'Scoped 'OpenShort) -instance NFData (OpenModuleParams 'Scoped) +deriving stock instance Show (OpenModule 'Scoped 'OpenFull) -instance Serialize (OpenModuleParams 'Parsed) +deriving stock instance Eq (OpenModule 'Parsed 'OpenShort) -instance NFData (OpenModuleParams 'Parsed) +deriving stock instance Eq (OpenModule 'Parsed 'OpenFull) -deriving stock instance Show (OpenModuleParams 'Parsed) +deriving stock instance Eq (OpenModule 'Scoped 'OpenShort) -deriving stock instance Show (OpenModuleParams 'Scoped) +deriving stock instance Eq (OpenModule 'Scoped 'OpenFull) -deriving stock instance Eq (OpenModuleParams 'Parsed) +deriving stock instance Ord (OpenModule 'Parsed 'OpenShort) -deriving stock instance Eq (OpenModuleParams 'Scoped) +deriving stock instance Ord (OpenModule 'Parsed 'OpenFull) -deriving stock instance Ord (OpenModuleParams 'Parsed) +deriving stock instance Ord (OpenModule 'Scoped 'OpenShort) -deriving stock instance Ord (OpenModuleParams 'Scoped) +deriving stock instance Ord (OpenModule 'Scoped 'OpenFull) data ScopedIden = ScopedIden { _scopedIdenFinal :: S.Name, @@ -1645,7 +1650,7 @@ instance NFData PostfixApplication data LetStatement (s :: Stage) = LetFunctionDef (FunctionDef s) | LetAliasDef (AliasDef s) - | LetOpen (OpenModule s) + | LetOpen (OpenModule s 'OpenFull) deriving stock (Generic) instance Serialize (LetStatement 'Scoped) @@ -2509,7 +2514,6 @@ makeLenses ''AxiomDef makeLenses ''InductiveParameters makeLenses ''InductiveParametersRhs makeLenses ''OpenModule -makeLenses ''OpenModuleParams makeLenses ''PatternApp makeLenses ''PatternInfixApp makeLenses ''PatternPostfixApp @@ -2665,10 +2669,14 @@ instance HasLoc (InductiveDef s) where instance (SingI s) => HasLoc (AxiomDef s) where getLoc m = getLoc (m ^. axiomKw) <> getLocExpressionType (m ^. axiomType) -instance HasLoc (OpenModule 'Scoped) where - getLoc m = - getLoc (m ^. openModuleParams . openModuleKw) - <>? fmap getLoc (m ^. openModuleParams . openPublicKw . unIrrelevant) +getLocPublicAnn :: PublicAnn -> Maybe Interval +getLocPublicAnn p = getLoc <$> p ^? _Public + +instance HasLoc (OpenModule s short) where + getLoc OpenModule {..} = + getLoc _openModuleKw + <>? fmap getLoc _openModuleUsingHiding + <>? getLocPublicAnn _openModulePublic instance HasLoc (ProjectionDef s) where getLoc = getLoc . (^. projectionConstructor) @@ -2801,10 +2809,33 @@ getLocIdentifierType e = case sing :: SStage s of instance (SingI s) => HasLoc (Iterator s) where getLoc Iterator {..} = getLocIdentifierType _iteratorName <> getLocExpressionType _iteratorBody +instance HasLoc (HidingList s) where + getLoc HidingList {..} = + let rbra = _hidingBraces ^. unIrrelevant . _2 + in getLoc (_hidingKw ^. unIrrelevant) <> getLoc rbra + +instance HasLoc (UsingList s) where + getLoc UsingList {..} = + let rbra = _usingBraces ^. unIrrelevant . _2 + in getLoc (_usingKw ^. unIrrelevant) <> getLoc rbra + +instance HasLoc (UsingHiding s) where + getLoc = \case + Using u -> getLoc u + Hiding u -> getLoc u + instance (SingI s) => HasLoc (Import s) where - getLoc Import {..} = case sing :: SStage s of - SParsed -> getLoc _importKw - SScoped -> getLoc _importKw + getLoc Import {..} = + let sLoc = case sing :: SStage s of + SParsed -> + getLoc _importKw + <> getLoc _importModulePath + <>? (getLoc <$> _importOpen) + SScoped -> + getLoc _importKw + <> getLoc _importModulePath + <>? (getLoc <$> _importOpen) + in sLoc <>? fmap getLoc (_importPublic ^? _Public) instance (SingI s, SingI t) => HasLoc (Module s t) where getLoc m = case sing :: SStage s of diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index 85a3df187b..2fd4c1587d 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -41,6 +41,8 @@ import Juvix.Prelude.Pretty qualified as P --- * the last branch body of a `Top` case expresssion. data IsTop = Top | NotTop +type PrettyPrintingMaybe a = forall r. (Members '[ExactPrint, Reader Options] r) => a -> Maybe (Sem r ()) + type PrettyPrinting a = forall r. (Members '[ExactPrint, Reader Options] r) => a -> Sem r () class PrettyPrint a where @@ -449,12 +451,13 @@ instance (PrettyPrint a) => PrettyPrint [a] where encloseSep (ppCode @Text "[") (ppCode @Text "]") (ppCode @Text ", ") cs ppStatements :: forall s r. (SingI s, Members '[ExactPrint, Reader Options] r) => [Statement s] -> Sem r () -ppStatements ss = paragraphs (ppGroup <$> Concrete.groupStatements (filter (not . isInductiveModule) ss)) +ppStatements ss = paragraphs (ppGroup <$> Concrete.groupStatements (filter shouldBePrinted ss)) where - isInductiveModule :: Statement s -> Bool - isInductiveModule = \case - StatementModule m -> m ^. moduleInductive - _ -> False + shouldBePrinted :: Statement s -> Bool + shouldBePrinted = \case + StatementModule m -> m ^. moduleOrigin == LocalModuleSource + _ -> True + ppGroup :: NonEmpty (Statement s) -> Sem r () ppGroup = vsep . sepEndSemicolon . fmap ppCode @@ -1157,31 +1160,39 @@ instance PrettyPrint (ImportScan' a) where instance (SingI s) => PrettyPrint (Import s) where ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => Import s -> Sem r () ppCode i = do - let open' = ppOpenModuleHelper Nothing <$> (i ^. importOpen) + let open' = ppCode <$> (i ^. importOpen) + usingHiding' = ppCode <$> i ^. importUsingHiding + public' = ppCode <$> i ^? importPublic . _Public ppCode (i ^. importKw) <+> ppModulePathType (i ^. importModulePath) <+?> ppAlias <+?> open' + <+?> usingHiding' + <+?> public' where ppAlias :: Maybe (Sem r ()) ppAlias = case i ^. importAsName of Nothing -> Nothing Just as -> Just (ppCode Kw.kwAs <+> ppModulePathType as) -ppOpenModuleHelper :: (SingI s) => Maybe (ModuleNameType s) -> PrettyPrinting (OpenModuleParams s) -ppOpenModuleHelper modName OpenModuleParams {..} = do - let name' = ppModuleNameType <$> modName - usingHiding' = ppCode <$> _openUsingHiding - openkw = ppCode _openModuleKw - public' = ppCode <$> _openPublicKw ^. unIrrelevant - openkw - <+?> name' - <+?> usingHiding' - <+?> public' - -instance (SingI s) => PrettyPrint (OpenModule s) where - ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => OpenModule s -> Sem r () - ppCode OpenModule {..} = ppOpenModuleHelper (Just _openModuleName) _openModuleParams +instance (SingI s, SingI short) => PrettyPrint (OpenModule s short) where + ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => OpenModule s short -> Sem r () + ppCode OpenModule {..} = do + let name' :: Maybe (Sem r ()) = case sing :: SIsOpenShort short of + SOpenShort -> Nothing + SOpenFull -> Just (ppModuleNameType _openModuleName) + openkw = ppCode _openModuleKw + pub = ppPublicAnn _openModulePublic + usingHiding = ppCode <$> _openModuleUsingHiding + openkw + <+?> name' + <+?> usingHiding + <+?> pub + +ppPublicAnn :: PrettyPrintingMaybe PublicAnn +ppPublicAnn = \case + NoPublic -> Nothing + Public k -> Just (ppCode (k ^. unIrrelevant)) ppCodeAtom :: (HasAtomicity c, PrettyPrint c) => PrettyPrinting c ppCodeAtom c = do diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 6350e37d40..e51c910294 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -92,7 +92,7 @@ scopeCheckRepl :: forall r a b. (Members '[Error JuvixError, NameIdGen, Reader EntryPoint, State Scope, State ScoperState] r) => ( forall r'. - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader EntryPoint] r') => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader BindingStrategy, Reader EntryPoint] r') => a -> Sem r' b ) -> @@ -106,6 +106,7 @@ scopeCheckRepl check importTab tab a = mapError (JuvixError @ScoperError) $ do . runInfoTableBuilder tab . runReader iniScopeParameters . runReader tab' + . localBindings $ check a where tab' = computeCombinedInfoTable importTab @@ -147,8 +148,8 @@ scopeCheckImport = scopeCheckRepl checkImport scopeCheckOpenModule :: forall r. (Members '[Error JuvixError, InfoTableBuilder, Reader InfoTable, NameIdGen, State Scope, Reader ScopeParameters, State ScoperState] r) => - OpenModule 'Parsed -> - Sem r (OpenModule 'Scoped) + OpenModule 'Parsed 'OpenFull -> + Sem r (OpenModule 'Scoped 'OpenFull) scopeCheckOpenModule = mapError (JuvixError @ScoperError) . checkOpenModule freshVariable :: (Members '[NameIdGen, State ScoperSyntax, State Scope, State ScoperState] r) => Symbol -> Sem r S.Symbol @@ -445,15 +446,149 @@ bindFixitySymbol s = do return s' checkImport :: + forall r. + ( Members + '[ HighlightBuilder, + Error ScoperError, + State Scope, + Reader ScopeParameters, + State ScoperState, + InfoTableBuilder, + Reader InfoTable, + NameIdGen, + Reader BindingStrategy, + Reader EntryPoint + ] + r + ) => + Import 'Parsed -> + Sem r (Import 'Scoped) +checkImport i@Import {..} = case _importPublic of + NoPublic -> checkImportNoPublic i + Public {} -> checkImportPublic i + +checkImportPublic :: + forall r. + ( Members + '[ Error ScoperError, + State Scope, + Reader ScopeParameters, + State ScoperState, + InfoTableBuilder, + Reader InfoTable, + NameIdGen, + HighlightBuilder, + Reader BindingStrategy, + Reader EntryPoint + ] + r + ) => + Import 'Parsed -> + Sem r (Import 'Scoped) +checkImportPublic i@Import {..} = do + let outerImport = + Import + { _importKw, + _importModulePath, + _importAsName = Nothing, + _importUsingHiding = Nothing, + _importPublic = NoPublic, + _importOpen = Nothing + } + outerImport' <- checkImportNoPublic outerImport + let locMod :: Module 'Parsed 'ModuleLocal = + localModule (splitName outerOpenModuleName) + local' <- checkLocalModule locMod + let (innerModuleName', usingHiding') = extract local' + mouterOpen' :: Maybe (OpenModule 'Scoped 'OpenShort) <- + fmap (set openModuleName ()) <$> mapM checkOpenModule outerOpen + let asName' :: Maybe S.TopModulePath = do + topModule :: TopModulePath <- _importAsName + return (set nameConcrete topModule innerModuleName') + return + Import + { _importKw, + _importPublic, + _importModulePath = outerImport' ^. importModulePath, + _importAsName = asName', + _importOpen = mouterOpen', + _importUsingHiding = usingHiding' + } + where + gen :: forall a. Sem '[Reader Interval] a -> a + gen = run . runReader loc + + loc :: Interval + loc = getLoc i + + -- Extracts the name of the innermost module as well as the scoped UsingHiding of the inner open + extract :: Module 'Scoped 'ModuleLocal -> (S.Symbol, Maybe (UsingHiding 'Scoped)) + extract m = case m ^. moduleBody of + [StatementOpenModule OpenModule {..}] -> (m ^. modulePath, _openModuleUsingHiding) + [StatementModule inner] -> extract inner + _ -> error "impossible. When generating this module we always put a single statement" + + outerOpenModuleName :: Name + outerOpenModuleName = topModulePathToName (fromMaybe _importModulePath _importAsName) + + outerOpen :: Maybe (OpenModule 'Parsed 'OpenFull) + outerOpen = do + OpenModule {..} <- _importOpen + return + OpenModule + { _openModuleKw, + _openModulePublic, + _openModuleName = outerOpenModuleName, + _openModuleUsingHiding + } + + innerOpen :: OpenModule 'Parsed 'OpenFull + innerOpen = gen $ do + _openModuleKw <- G.kw G.kwOpen + let _openModuleName = topModulePathToName _importModulePath + pubKw <- Irrelevant <$> G.kw G.kwPublic + let + return + OpenModule + { _openModuleKw, + _openModuleUsingHiding = _importUsingHiding, + _openModulePublic = Public pubKw, + _openModuleName + } + + singletonModule :: Symbol -> Statement 'Parsed -> Module 'Parsed 'ModuleLocal + singletonModule modName stm = gen $ do + _moduleKw <- G.kw G.kwModule + _moduleKwEnd <- G.kw G.kwEnd + let _moduleId = () + _moduleBody = [stm] + return + Module + { _moduleDoc = Nothing, + _modulePragmas = Nothing, + _moduleOrigin = LocalModuleType, + _moduleMarkdownInfo = Nothing, + _modulePath = modName, + .. + } + + localModule :: ([Symbol], Symbol) -> Module 'Parsed 'ModuleLocal + localModule (qualf, m) = case qualf of + [] -> singletonModule m (StatementOpenModule innerOpen) + n : ns -> singletonModule n (StatementModule (localModule (ns, m))) + +checkImportNoPublic :: forall r. (Members '[Error ScoperError, State Scope, Reader ScopeParameters, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r) => Import 'Parsed -> Sem r (Import 'Scoped) -checkImport import_@Import {..} = do +checkImportNoPublic import_@Import {..} = do + eassert (_importPublic == NoPublic) smodule <- readScopeModule import_ let sname :: S.TopModulePath = smodule ^. scopedModulePath sname' :: S.Name = set S.nameConcrete (topModulePathToName _importModulePath) sname - cmodule = set scopedModuleName sname' smodule + scopedModule :: ScopedModule = set scopedModuleName sname' smodule + exportInfoOriginal = scopedModule ^. scopedModuleExportInfo importName :: S.TopModulePath = set S.nameConcrete _importModulePath sname synonymName :: Maybe S.TopModulePath = do synonym <- _importAsName @@ -462,16 +597,20 @@ checkImport import_@Import {..} = do qual' = do asName <- _importAsName return (set S.nameConcrete asName sname') - addModuleToScope cmodule registerName importName whenJust synonymName registerName - registerScoperModules cmodule - importOpen' <- mapM (checkImportOpenParams cmodule) _importOpen + registerScoperModules scopedModule + importOpen' <- mapM (checkOpenModuleShort scopedModule) _importOpen + usingHiding' <- mapM (checkUsingHiding importName exportInfoOriginal) _importUsingHiding + let exportInfoFiltered :: ExportInfo = filterExportInfo _importPublic usingHiding' exportInfoOriginal + filteredScopedModule = set scopedModuleExportInfo exportInfoFiltered scopedModule + addModuleToScope filteredScopedModule return Import { _importModulePath = sname, _importAsName = qual', _importOpen = importOpen', + _importUsingHiding = usingHiding', .. } where @@ -771,7 +910,7 @@ getModuleId path = do checkFixitySyntaxDef :: forall r. - (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, State ScoperSyntax, NameIdGen, Reader EntryPoint, InfoTableBuilder, Reader InfoTable] r) => + (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, State ScoperSyntax, NameIdGen, InfoTableBuilder, Reader InfoTable, Reader EntryPoint] r) => FixitySyntaxDef 'Parsed -> Sem r (FixitySyntaxDef 'Scoped) checkFixitySyntaxDef FixitySyntaxDef {..} = topBindings $ do @@ -1155,7 +1294,7 @@ checkTopModule m@Module {..} = checkedModule _moduleDoc = doc', _modulePragmas = _modulePragmas, _moduleKw, - _moduleInductive, + _moduleOrigin, _moduleKwEnd, _moduleId, _moduleMarkdownInfo @@ -1450,7 +1589,7 @@ checkSections sec = topBindings helper Module { _moduleDoc = Nothing, _modulePragmas = Nothing, - _moduleInductive = True, + _moduleOrigin = LocalModuleType, _moduleMarkdownInfo = Nothing, .. } @@ -1563,7 +1702,20 @@ reserveLocalModuleSymbol = checkLocalModule :: forall r. - (Members '[HighlightBuilder, Error ScoperError, State Scope, Reader ScopeParameters, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader EntryPoint, Reader BindingStrategy] r) => + ( Members + '[ HighlightBuilder, + Error ScoperError, + State Scope, + Reader ScopeParameters, + State ScoperState, + InfoTableBuilder, + Reader InfoTable, + NameIdGen, + Reader BindingStrategy, + Reader EntryPoint + ] + r + ) => Module 'Parsed 'ModuleLocal -> Sem r (Module 'Scoped 'ModuleLocal) checkLocalModule md@Module {..} = do @@ -1589,7 +1741,7 @@ checkLocalModule md@Module {..} = do _moduleMarkdownInfo = Nothing, _moduleId = _moduleId', _moduleKw, - _moduleInductive, + _moduleOrigin, _moduleKwEnd } smod = @@ -1666,121 +1818,121 @@ lookupModuleSymbol n = do NameUnqualified s -> ([], s) NameQualified (QualifiedName (SymbolPath p) s) -> (toList p, s) -checkImportOpenParams :: +checkOpenModuleShort :: forall r. (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r) => ScopedModule -> - OpenModuleParams 'Parsed -> - Sem r (OpenModuleParams 'Scoped) -checkImportOpenParams m p = - (^. openModuleParams) - <$> checkOpenModuleHelper - (Just m) - OpenModule - { _openModuleParams = p, - _openModuleName = m ^. scopedModuleName . S.nameConcrete - } + OpenModule 'Parsed 'OpenShort -> + Sem r (OpenModule 'Scoped 'OpenShort) +checkOpenModuleShort = checkOpenModuleHelper checkOpenModule :: forall r. (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r) => - OpenModule 'Parsed -> - Sem r (OpenModule 'Scoped) -checkOpenModule = checkOpenModuleHelper Nothing + OpenModule 'Parsed 'OpenFull -> + Sem r (OpenModule 'Scoped 'OpenFull) +checkOpenModule open@OpenModule {..} = do + m <- lookupModuleSymbol _openModuleName + checkOpenModuleHelper m open -checkOpenModuleHelper :: +checkUsingHiding :: forall r. - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r) => - Maybe ScopedModule -> - OpenModule 'Parsed -> - Sem r (OpenModule 'Scoped) -checkOpenModuleHelper importModuleHint OpenModule {..} = do - cmod <- case importModuleHint of - Nothing -> lookupModuleSymbol _openModuleName - Just m -> return m - let exportInfo = cmod ^. scopedModuleExportInfo - registerName (cmod ^. scopedModuleName) - - let checkUsingHiding :: UsingHiding 'Parsed -> Sem r (UsingHiding 'Scoped) - checkUsingHiding = \case - Hiding h -> Hiding <$> checkHidingList h - Using uh -> Using <$> checkUsingList uh - where - scopeSymbol :: forall (ns :: NameSpace). (SingI ns) => Sing ns -> Symbol -> Sem r S.Symbol - scopeSymbol _ s = do - let mentry :: Maybe (NameSpaceEntryType ns) - mentry = exportInfo ^. exportNameSpace . at s - err = - throw - ( ErrModuleDoesNotExportSymbol - ( ModuleDoesNotExportSymbol - { _moduleDoesNotExportSymbol = s, - _moduleDoesNotExportModule = cmod - } - ) - ) - entry <- maybe err return mentry - let scopedSym = entryToSymbol entry s - registerName scopedSym - return scopedSym - - checkHidingList :: HidingList 'Parsed -> Sem r (HidingList 'Scoped) - checkHidingList l = do - items' <- mapM checkHidingItem (l ^. hidingList) - return - HidingList - { _hidingKw = l ^. hidingKw, - _hidingBraces = l ^. hidingBraces, - _hidingList = items' + (Members '[Error ScoperError, InfoTableBuilder] r) => + S.TopModulePath -> + ExportInfo -> + UsingHiding 'Parsed -> + Sem r (UsingHiding 'Scoped) +checkUsingHiding modulepath exportInfo = \case + Hiding h -> Hiding <$> checkHidingList h + Using uh -> Using <$> checkUsingList uh + where + scopeSymbol :: forall (ns :: NameSpace). (SingI ns) => Sing ns -> Symbol -> Sem r S.Symbol + scopeSymbol _ s = do + let mentry :: Maybe (NameSpaceEntryType ns) + mentry = exportInfo ^. exportNameSpace . at s + err = + throw + . ErrModuleDoesNotExportSymbol + $ ModuleDoesNotExportSymbol + { _moduleDoesNotExportSymbol = s, + _moduleDoesNotExportModule = modulepath } + entry <- maybe err return mentry + let scopedSym = entryToSymbol entry s + registerName scopedSym + return scopedSym + + checkHidingList :: HidingList 'Parsed -> Sem r (HidingList 'Scoped) + checkHidingList l = do + items' <- mapM checkHidingItem (l ^. hidingList) + return + HidingList + { _hidingKw = l ^. hidingKw, + _hidingBraces = l ^. hidingBraces, + _hidingList = items' + } - checkUsingList :: UsingList 'Parsed -> Sem r (UsingList 'Scoped) - checkUsingList l = do - items' <- mapM checkUsingItem (l ^. usingList) - return - UsingList - { _usingKw = l ^. usingKw, - _usingBraces = l ^. usingBraces, - _usingList = items' - } + checkUsingList :: UsingList 'Parsed -> Sem r (UsingList 'Scoped) + checkUsingList l = do + items' <- mapM checkUsingItem (l ^. usingList) + return + UsingList + { _usingKw = l ^. usingKw, + _usingBraces = l ^. usingBraces, + _usingList = items' + } - checkHidingItem :: HidingItem 'Parsed -> Sem r (HidingItem 'Scoped) - checkHidingItem h = do - let s = h ^. hidingSymbol - scopedSym <- - if - | isJust (h ^. hidingModuleKw) -> scopeSymbol SNameSpaceModules s - | otherwise -> scopeSymbol SNameSpaceSymbols s - return - HidingItem - { _hidingSymbol = scopedSym, - _hidingModuleKw = h ^. hidingModuleKw - } + checkHidingItem :: HidingItem 'Parsed -> Sem r (HidingItem 'Scoped) + checkHidingItem h = do + let s = h ^. hidingSymbol + scopedSym <- + if + | isJust (h ^. hidingModuleKw) -> scopeSymbol SNameSpaceModules s + | otherwise -> scopeSymbol SNameSpaceSymbols s + return + HidingItem + { _hidingSymbol = scopedSym, + _hidingModuleKw = h ^. hidingModuleKw + } - checkUsingItem :: UsingItem 'Parsed -> Sem r (UsingItem 'Scoped) - checkUsingItem i = do - let s = i ^. usingSymbol - scopedSym <- - if - | isJust (i ^. usingModuleKw) -> scopeSymbol SNameSpaceModules s - | otherwise -> scopeSymbol SNameSpaceSymbols s - let scopedAs = do - c <- i ^. usingAs - return (set S.nameConcrete c scopedSym) - mapM_ registerName scopedAs - return - UsingItem - { _usingSymbol = scopedSym, - _usingAs = scopedAs, - _usingAsKw = i ^. usingAsKw, - _usingModuleKw = i ^. usingModuleKw - } - openParams' <- traverseOf openUsingHiding (mapM checkUsingHiding) _openModuleParams - mergeScope (alterScope (openParams' ^. openUsingHiding) exportInfo) + checkUsingItem :: UsingItem 'Parsed -> Sem r (UsingItem 'Scoped) + checkUsingItem i = do + let s = i ^. usingSymbol + scopedSym <- + if + | isJust (i ^. usingModuleKw) -> scopeSymbol SNameSpaceModules s + | otherwise -> scopeSymbol SNameSpaceSymbols s + let scopedAs = do + c <- i ^. usingAs + return (set S.nameConcrete c scopedSym) + mapM_ registerName scopedAs + return + UsingItem + { _usingSymbol = scopedSym, + _usingAs = scopedAs, + _usingAsKw = i ^. usingAsKw, + _usingModuleKw = i ^. usingModuleKw + } + +checkOpenModuleHelper :: + forall r short. + (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r, SingI short) => + ScopedModule -> + OpenModule 'Parsed short -> + Sem r (OpenModule 'Scoped short) +checkOpenModuleHelper openedModule OpenModule {..} = do + let exportInfo = openedModule ^. scopedModuleExportInfo + registerName (openedModule ^. scopedModuleName) + usingHiding' <- mapM (checkUsingHiding (openedModule ^. scopedModulePath) exportInfo) _openModuleUsingHiding + mergeScope (filterExportInfo _openModulePublic usingHiding' exportInfo) + let openName :: OpenModuleNameType 'Scoped short = case sing :: SIsOpenShort short of + SOpenFull -> openedModule ^. scopedModuleName + SOpenShort -> () return OpenModule - { _openModuleName = cmod ^. scopedModuleName, - _openModuleParams = openParams', + { _openModuleName = openName, + _openModuleUsingHiding = usingHiding', + _openModulePublic, .. } where @@ -1795,61 +1947,61 @@ checkOpenModuleHelper importModuleHint OpenModule {..} = do modify (over scopeNameSpace (HashMap.insertWith (<>) s (symbolInfoSingle entry))) - alterScope :: Maybe (UsingHiding 'Scoped) -> ExportInfo -> ExportInfo - alterScope openModif = alterEntries . filterScope - where - alterEntries :: ExportInfo -> ExportInfo - alterEntries nfo = - ExportInfo - { _exportSymbols = alterEntry <$> nfo ^. exportSymbols, - _exportModuleSymbols = alterEntry <$> nfo ^. exportModuleSymbols, - _exportFixitySymbols = alterEntry <$> nfo ^. exportFixitySymbols - } +filterExportInfo :: PublicAnn -> Maybe (UsingHiding 'Scoped) -> ExportInfo -> ExportInfo +filterExportInfo pub openModif = alterEntries . filterScope + where + alterEntries :: ExportInfo -> ExportInfo + alterEntries nfo = + ExportInfo + { _exportSymbols = alterEntry <$> nfo ^. exportSymbols, + _exportModuleSymbols = alterEntry <$> nfo ^. exportModuleSymbols, + _exportFixitySymbols = alterEntry <$> nfo ^. exportFixitySymbols + } - alterEntry :: (SingI ns) => NameSpaceEntryType ns -> NameSpaceEntryType ns - alterEntry = - over - nsEntry - ( set S.nameWhyInScope S.BecauseImportedOpened - . set S.nameVisibilityAnn (publicAnnToVis (_openModuleParams ^. openPublic)) - ) + alterEntry :: (SingI ns) => NameSpaceEntryType ns -> NameSpaceEntryType ns + alterEntry = + over + nsEntry + ( set S.nameWhyInScope S.BecauseImportedOpened + . set S.nameVisibilityAnn (publicAnnToVis pub) + ) - publicAnnToVis :: PublicAnn -> VisibilityAnn - publicAnnToVis = \case - Public -> VisPublic - NoPublic -> VisPrivate - - filterScope :: ExportInfo -> ExportInfo - filterScope = case openModif of - Just (Using l) -> - over exportSymbols (HashMap.fromList . mapMaybe inUsing . HashMap.toList) - . over exportModuleSymbols (HashMap.fromList . mapMaybe inUsing . HashMap.toList) - . over exportFixitySymbols (HashMap.fromList . mapMaybe inUsing . HashMap.toList) - where - inUsing :: - forall (ns :: NameSpace). - (SingI ns) => - (Symbol, NameSpaceEntryType ns) -> - Maybe (Symbol, NameSpaceEntryType ns) - inUsing (sym, e) = do - mayAs' <- u ^. at (e ^. nsEntry . S.nameId) - return (fromMaybe sym mayAs', e) - u :: HashMap NameId (Maybe Symbol) - u = - HashMap.fromList - [ (i ^. usingSymbol . S.nameId, i ^? usingAs . _Just . S.nameConcrete) - | i <- toList (l ^. usingList) - ] - Just (Hiding l) -> - over exportSymbols (HashMap.filter (not . inHiding)) - . over exportModuleSymbols (HashMap.filter (not . inHiding)) - . over exportFixitySymbols (HashMap.filter (not . inHiding)) - where - inHiding :: forall ns. (SingI ns) => NameSpaceEntryType ns -> Bool - inHiding e = HashSet.member (e ^. nsEntry . S.nameId) u - u :: HashSet NameId - u = HashSet.fromList (map (^. hidingSymbol . S.nameId) (toList (l ^. hidingList))) - Nothing -> id + publicAnnToVis :: PublicAnn -> VisibilityAnn + publicAnnToVis = \case + Public {} -> VisPublic + NoPublic -> VisPrivate + + filterScope :: ExportInfo -> ExportInfo + filterScope = case openModif of + Just (Using l) -> + over exportSymbols (HashMap.fromList . mapMaybe inUsing . HashMap.toList) + . over exportModuleSymbols (HashMap.fromList . mapMaybe inUsing . HashMap.toList) + . over exportFixitySymbols (HashMap.fromList . mapMaybe inUsing . HashMap.toList) + where + inUsing :: + forall (ns :: NameSpace). + (SingI ns) => + (Symbol, NameSpaceEntryType ns) -> + Maybe (Symbol, NameSpaceEntryType ns) + inUsing (sym, e) = do + mayAs' <- u ^. at (e ^. nsEntry . S.nameId) + return (fromMaybe sym mayAs', e) + u :: HashMap NameId (Maybe Symbol) + u = + HashMap.fromList + [ (i ^. usingSymbol . S.nameId, i ^? usingAs . _Just . S.nameConcrete) + | i <- toList (l ^. usingList) + ] + Just (Hiding l) -> + over exportSymbols (HashMap.filter (not . inHiding)) + . over exportModuleSymbols (HashMap.filter (not . inHiding)) + . over exportFixitySymbols (HashMap.filter (not . inHiding)) + where + inHiding :: forall ns. (SingI ns) => NameSpaceEntryType ns -> Bool + inHiding e = HashSet.member (e ^. nsEntry . S.nameId) u + u :: HashSet NameId + u = HashSet.fromList (map (^. hidingSymbol . S.nameId) (toList (l ^. hidingList))) + Nothing -> id checkAxiomDef :: (Members '[HighlightBuilder, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, Error ScoperError, State Scope, State ScoperState, NameIdGen, State ScoperSyntax, Reader BindingStrategy, Reader EntryPoint] r) => @@ -2571,7 +2723,10 @@ checkJudoc :: (Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader EntryPoint] r) => Judoc 'Parsed -> Sem r (Judoc 'Scoped) -checkJudoc (Judoc groups) = ignoreHighlightBuilder $ ignoreInfoTableBuilder $ Judoc <$> mapM checkJudocGroup groups +checkJudoc (Judoc groups) = + ignoreHighlightBuilder + . ignoreInfoTableBuilder + $ Judoc <$> mapM checkJudocGroup groups checkJudocGroup :: (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader EntryPoint] r) => diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs index dca9c637fd..ee0b28c3a6 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs @@ -14,7 +14,7 @@ import Juvix.Compiler.Concrete.Language import Juvix.Compiler.Concrete.Pretty.Options (Options, fromGenericOptions) import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Pretty import Juvix.Compiler.Concrete.Translation.ImportScanner.Base -import Juvix.Compiler.Store.Scoped.Language (FixitySymbolEntry, ModuleSymbolEntry, PreSymbolEntry, ScopedModule) +import Juvix.Compiler.Store.Scoped.Language (FixitySymbolEntry, ModuleSymbolEntry, PreSymbolEntry) import Juvix.Data.CodeAnn import Juvix.Prelude @@ -651,7 +651,7 @@ instance ToGenericError ConstructorExpectedLeftApplication where data ModuleDoesNotExportSymbol = ModuleDoesNotExportSymbol { _moduleDoesNotExportSymbol :: Symbol, - _moduleDoesNotExportModule :: ScopedModule + _moduleDoesNotExportModule :: S.TopModulePath } instance ToGenericError ModuleDoesNotExportSymbol where diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index ed7baa10b7..85705aa2cb 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -95,7 +95,7 @@ fromSource e = mapError (JuvixError @ParserError) $ do data ReplInput = ReplExpression (ExpressionAtoms 'Parsed) | ReplImport (Import 'Parsed) - | ReplOpenImport (OpenModule 'Parsed) + | ReplOpen (OpenModule 'Parsed 'OpenFull) expressionFromTextSource :: (Members '[Error JuvixError] r) => @@ -378,7 +378,7 @@ replInput :: forall r. (Members '[ParserResultBuilder, JudocStash, Error ParserE replInput = P.label "" $ ReplExpression <$> parseExpressionAtoms - <|> ReplOpenImport <$> openModule + <|> ReplOpen <$> openModule <|> ReplImport <$> import_ -------------------------------------------------------------------------------- @@ -791,7 +791,9 @@ import_ = do _importKw <- kw kwImport _importModulePath <- topModulePath _importAsName <- optional pasName - _importOpen <- optional popenModuleParams + _importUsingHiding <- optional usingOrHiding + _importPublic <- publicAnn + _importOpen <- optional openModule let i = Import {..} P.lift (registerImport i) return i @@ -1164,7 +1166,7 @@ multiwayIf :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => Pa multiwayIf = do _ifKw <- kw kwIf (Left <$> multiwayIf' _ifKw []) - <|> (return $ Right $ NameUnqualified $ WithLoc (getLoc _ifKw) (_ifKw ^. keywordRefKeyword . keywordAscii)) + <|> return (Right $ NameUnqualified $ WithLoc (getLoc _ifKw) (_ifKw ^. keywordRefKeyword . keywordAscii)) -------------------------------------------------------------------------------- -- Universe expression @@ -1601,9 +1603,9 @@ moduleDef = P.label "" $ do .. } where - _moduleInductive :: ModuleInductiveType t - _moduleInductive = case sing :: SModuleIsTop t of - SModuleLocal -> False + _moduleOrigin :: ModuleInductiveType t + _moduleOrigin = case sing :: SModuleIsTop t of + SModuleLocal -> LocalModuleSource SModuleTop -> () endModule :: ParsecS r (ModuleEndType t) @@ -1620,26 +1622,29 @@ atomicExpression = do _ -> return () return $ ExpressionAtoms (NonEmpty.singleton atom) (Irrelevant loc) -openModule :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (OpenModule 'Parsed) +publicAnn :: forall r. (Members '[ParserResultBuilder] r) => ParsecS r PublicAnn +publicAnn = maybe NoPublic (Public . Irrelevant) <$> optional (kw kwPublic) + +openModule :: + forall r (short :: IsOpenShort). + ( SingI short, + Members + '[ ParserResultBuilder, + PragmasStash, + JudocStash + ] + r + ) => + ParsecS r (OpenModule 'Parsed short) openModule = do _openModuleKw <- kw kwOpen - _openModuleName <- name - _openUsingHiding <- optional usingOrHiding - _openPublicKw <- Irrelevant <$> optional (kw kwPublic) - let _openPublic = maybe NoPublic (const Public) (_openPublicKw ^. unIrrelevant) - _openModuleParams = OpenModuleParams {..} + _openModuleName <- case sing :: SIsOpenShort short of + SOpenFull -> name + SOpenShort -> return () + _openModuleUsingHiding <- optional usingOrHiding + _openModulePublic <- publicAnn return OpenModule {..} --- TODO is there way to merge this with `openModule`? -popenModuleParams :: forall r. (Members '[Error ParserError, ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (OpenModuleParams 'Parsed) -popenModuleParams = do - _openModuleKw <- kw kwOpen - _openUsingHiding <- optional usingOrHiding - _openPublicKw <- Irrelevant <$> optional (kw kwPublic) - let _openPublic = maybe NoPublic (const Public) (_openPublicKw ^. unIrrelevant) - _openModuleParams = OpenModuleParams {..} - return OpenModuleParams {..} - usingOrHiding :: (Members '[ParserResultBuilder, JudocStash, PragmasStash] r) => ParsecS r (UsingHiding 'Parsed) usingOrHiding = Using <$> pusingList diff --git a/src/Juvix/Compiler/Pipeline/Package/Loader.hs b/src/Juvix/Compiler/Pipeline/Package/Loader.hs index ae6824a115..47875a5e51 100644 --- a/src/Juvix/Compiler/Pipeline/Package/Loader.hs +++ b/src/Juvix/Compiler/Pipeline/Package/Loader.hs @@ -71,7 +71,7 @@ toConcrete t p = run . runReader l $ do return Module { _moduleKwEnd = (), - _moduleInductive = (), + _moduleOrigin = (), _moduleDoc = Nothing, _modulePragmas = Nothing, _moduleMarkdownInfo = Nothing, @@ -108,21 +108,22 @@ toConcrete t p = run . runReader l $ do mkImport _importModulePath = do _openModuleKw <- kw kwOpen _importKw <- kw kwImport - return - ( StatementImport - Import - { _importOpen = - Just - OpenModuleParams - { _openUsingHiding = Nothing, - _openPublicKw = Irrelevant Nothing, - _openPublic = NoPublic, - .. - }, - _importAsName = Nothing, - .. + let openShort :: OpenModule 'Parsed 'OpenShort = + OpenModule + { _openModuleName = (), + _openModuleUsingHiding = Nothing, + _openModulePublic = NoPublic, + _openModuleKw } - ) + return $ + StatementImport + Import + { _importOpen = Just openShort, + _importPublic = NoPublic, + _importUsingHiding = Nothing, + _importAsName = Nothing, + .. + } mkStdlibImport :: (Member (Reader Interval) r) => Sem r (Statement 'Parsed) mkStdlibImport = do diff --git a/src/Juvix/Compiler/Pipeline/Repl.hs b/src/Juvix/Compiler/Pipeline/Repl.hs index da3fd9ca69..2b456a9e48 100644 --- a/src/Juvix/Compiler/Pipeline/Repl.hs +++ b/src/Juvix/Compiler/Pipeline/Repl.hs @@ -180,7 +180,7 @@ compileReplInputIO fp txt = do case p of Parser.ReplExpression e -> ReplPipelineResultNode <$> compileExpression e Parser.ReplImport i -> registerImport i $> ReplPipelineResultImport (i ^. importModulePath) - Parser.ReplOpenImport i -> return (ReplPipelineResultOpen (i ^. openModuleName)) + Parser.ReplOpen i -> return (ReplPipelineResultOpen (i ^. openModuleName)) runTransformations :: forall r. diff --git a/src/Juvix/Data/Effect/ExactPrint.hs b/src/Juvix/Data/Effect/ExactPrint.hs index 38d235b64d..ba56727293 100644 --- a/src/Juvix/Data/Effect/ExactPrint.hs +++ b/src/Juvix/Data/Effect/ExactPrint.hs @@ -34,6 +34,14 @@ infixr 7 Nothing -> b Just () -> (space <> b) +infixr 7 + +() :: (Members '[ExactPrint] r) => Maybe (Sem r ()) -> Maybe (Sem r ()) -> Maybe (Sem r ()) +a b = do + a' <- a + b' <- b + return (a' <+> b') + infixr 7 () :: (Members '[ExactPrint] r) => Maybe (Sem r ()) -> Sem r () -> Sem r () diff --git a/src/Juvix/Prelude/Base/Foundation.hs b/src/Juvix/Prelude/Base/Foundation.hs index 606cb33ed3..d856efa099 100644 --- a/src/Juvix/Prelude/Base/Foundation.hs +++ b/src/Juvix/Prelude/Base/Foundation.hs @@ -432,6 +432,14 @@ infixr 7 Nothing -> id Just a -> (a <+>) +infixr 7 ?<>? + +(?<>?) :: (Semigroup m) => Maybe m -> Maybe m -> Maybe m +a ?<>? b = do + a' <- a + b' <- b + return (a' <> b') + infixr 7 ?<> (?<>) :: (Semigroup m) => Maybe m -> m -> m diff --git a/test/Scope/Positive.hs b/test/Scope/Positive.hs index 643d33c49b..0705c4c8c8 100644 --- a/test/Scope/Positive.hs +++ b/test/Scope/Positive.hs @@ -241,5 +241,9 @@ tests = posTest "Visibility precedence" $(mkRelDir "VisibilityPrecendence") - $(mkRelFile "VisibilityPrecedence.juvix") + $(mkRelFile "VisibilityPrecedence.juvix"), + posTest + "Public import" + $(mkRelDir "PublicImports") + $(mkRelFile "Main.juvix") ] diff --git a/tests/positive/DefaultValues.juvix b/tests/positive/DefaultValues.juvix deleted file mode 100644 index bb3bacfae9..0000000000 --- a/tests/positive/DefaultValues.juvix +++ /dev/null @@ -1,55 +0,0 @@ -module DefaultValues; - -import Stdlib.Data.Product open; - -axiom A : Type; - -axiom B : Type; - -axiom C : Type; - -axiom D : Type; - -axiom a : A; - -axiom b : B; - -axiom c : C; - -axiom d : D; - -mk - {f1 : A := a} - {f2 : Type} - {f3 : C := c} - (x : f2) - : A × f2 × C := f1, x, f3; - -x1 : A × B × C := mk (x := b); - -mk2 - {f1 : A := a} - {f2 : Type} - {f3 : C := c} - (x : f2) - {f4 : D := d} - (y : f2) - : A × f2 × C := f1, x, f3; - -x2 : A × B × C := mk2 (x := b) (y := b); - -mk3 {A := Type} {f1 : D := d} : D := f1; - -x3 : D := mk3; - -mk4 {A := Type} {f1 f2 f3 : D := d} : _ := f3; - -x4 : D := mk4; - -mk5 {A := Type} {f1 f2 f3 : D := mk4} : _ := f3; - -x5 : D := mk5; - -rec1 {a1 : A := rec2 {a}} : A := rec2 {a1 := a1}; - -rec2 {a1 : A := rec1 {a}} : A := a1; diff --git a/tests/positive/Format.juvix b/tests/positive/Format.juvix index 8cf83508ed..af14283a82 100644 --- a/tests/positive/Format.juvix +++ b/tests/positive/Format.juvix @@ -416,4 +416,13 @@ fff {f7 : List Nat} : Nat := zero; +module PublicImports; + + module Inner; + import Stdlib.Prelude as X.Y.Z using {Nat} public; + end; + + axiom a : Inner.X.Y.Z.Nat; +end; + -- Comment at the end of a module diff --git a/tests/positive/PublicImports/M.juvix b/tests/positive/PublicImports/M.juvix new file mode 100644 index 0000000000..a5af704bdc --- /dev/null +++ b/tests/positive/PublicImports/M.juvix @@ -0,0 +1,3 @@ +module M; + +axiom MType : Type; diff --git a/tests/positive/PublicImports/Main.juvix b/tests/positive/PublicImports/Main.juvix new file mode 100644 index 0000000000..1318ce4242 --- /dev/null +++ b/tests/positive/PublicImports/Main.juvix @@ -0,0 +1,30 @@ +module Main; + +module Using; + + module Inner; + import M using {MType} public; + end; + + axiom x : Inner.M.MType; + +end; + +module Hiding; + module Inner; + import M hiding {MType} public; + end; + + module P; + module Inner; + module M; + axiom MType : Type; + end; + end; + end; + + open P; + + --- There would be an ambiguity error if the above hiding did nothing + axiom x : Inner.M.MType; +end; diff --git a/tests/positive/PublicImports/Package.juvix b/tests/positive/PublicImports/Package.juvix new file mode 100644 index 0000000000..5b60fc4da1 --- /dev/null +++ b/tests/positive/PublicImports/Package.juvix @@ -0,0 +1,5 @@ +module Package; + +import PackageDescription.Basic open; + +package : Package := basicPackage;