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.

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

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

src/Juvix/Compiler/Concrete/Data.hs

@@ -12,14 +12,18 @@ 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
 
 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

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])

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)

src/Juvix/Compiler/Concrete/Data/PublicAnn.hs

@@ -5,11 +5,16 @@ 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)
 
 instance Serialize PublicAnn
 
 instance NFData PublicAnn
+
+_Public :: Traversal' PublicAnn KeywordRef
+_Public f = \case
+  NoPublic -> pure NoPublic
+  Public (Irrelevant x) -> Public . Irrelevant <$> f x

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,15 +263,15 @@ 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)
   | StatementFunctionDef (FunctionDef s)
   | 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