Remove module parameters (#1848)

src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs

@@ -69,8 +69,7 @@ goModule m = case sing :: SModuleIsTop t of
   SModuleLocal -> goModule' m
   where
     goModule' :: Module 'Scoped t -> Sem r Abstract.Module
-    goModule' Module {..}
+    goModule' Module {..} = do
-      | null _moduleParameters = do
       body' <- goModuleBody _moduleBody
       examples' <- goExamples _moduleDoc
       return
@@ -79,7 +78,6 @@ goModule m = case sing :: SModuleIsTop t of
             _moduleBody = body',
             _moduleExamples = examples'
           }
-      | otherwise = unsupported "Module parameters"
       where
         name' :: Abstract.Name
         name' = case sing :: SModuleIsTop t of

src/Juvix/Compiler/Concrete/Language.hs

@@ -398,7 +398,6 @@ type LocalModuleName s = SymbolType s
 data Module (s :: Stage) (t :: ModuleIsTop) = Module
   { _moduleKw :: KeywordRef,
     _modulePath :: ModulePathType s t,
-    _moduleParameters :: [InductiveParameters s],
     _moduleDoc :: Maybe (Judoc s),
     _moduleBody :: [Statement s]
   }
@@ -511,7 +510,6 @@ data OpenModule (s :: Stage) = OpenModule
   { _openModuleKw :: KeywordRef,
     _openModuleName :: ModuleRefType s,
     _openModuleImportKw :: Maybe KeywordRef,
-    _openParameters :: [ExpressionType s],
     _openUsingHiding :: Maybe UsingHiding,
     _openPublic :: PublicAnn
   }

src/Juvix/Compiler/Concrete/Pretty/Base.hs

@@ -208,13 +208,11 @@ instance (SingI s, SingI t) => PrettyCode (Module s t) where
   ppCode Module {..} = do
     moduleBody' <- indent' <$> ppCode _moduleBody
     modulePath' <- ppModulePathType _modulePath
-    moduleParameters' <- ppInductiveParameters _moduleParameters
     moduleDoc' <- mapM ppCode _moduleDoc
     return $
       moduleDoc'
         ?<> kwModule
         <+> modulePath'
-        <+?> moduleParameters'
           <> kwSemicolon
           <> line
           <> moduleBody'
@@ -368,18 +366,10 @@ instance (SingI s) => PrettyCode (OpenModule s) where
       SParsed -> ppCode _openModuleName
       SScoped -> ppCode _openModuleName
     openUsingHiding' <- mapM ppUsingHiding _openUsingHiding
-    openParameters' <- ppOpenParams
     importkw' <- mapM ppCode _openModuleImportKw
     let openPublic' = ppPublic
-    return $ kwOpen <+?> importkw' <+> openModuleName' <+?> openParameters' <+?> openUsingHiding' <+?> openPublic'
+    return $ kwOpen <+?> importkw' <+> openModuleName' <+?> openUsingHiding' <+?> openPublic'
     where
-      ppAtom' = case sing :: SStage s of
-        SParsed -> ppCodeAtom
-        SScoped -> ppCodeAtom
-      ppOpenParams :: Sem r (Maybe (Doc Ann))
-      ppOpenParams = case _openParameters of
-        [] -> return Nothing
-        _ -> Just . hsep <$> mapM ppAtom' _openParameters
       ppUsingHiding :: UsingHiding -> Sem r (Doc Ann)
       ppUsingHiding uh = do
         bracedList <-

src/Juvix/Compiler/Concrete/Print/Base.hs

@@ -252,7 +252,6 @@ instance PrettyPrint (OpenModule 'Scoped) where
   ppCode OpenModule {..} = do
     let name' = ppCode _openModuleName
         usingHiding' = ppCode <$> _openUsingHiding
-        openParameters' = hsep . fmap ppAtom <$> nonEmpty _openParameters
         importkw' = ppCode <$> _openModuleImportKw
         public' = case _openPublic of
           Public -> Just (noLoc P.kwPublic)
@@ -260,7 +259,6 @@ instance PrettyPrint (OpenModule 'Scoped) where
     ppCode _openModuleKw
       <+?> importkw'
       <+> name'
-      <+?> openParameters'
       <+?> usingHiding'
       <+?> public'
 

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs

@@ -533,7 +533,7 @@ checkTopModule ::
   (Members '[Error ScoperError, Reader ScopeParameters, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
   Module 'Parsed 'ModuleTop ->
   Sem r (ModuleRef'' 'S.NotConcrete 'ModuleTop)
-checkTopModule m@(Module _moduleKw path params doc body) = do
+checkTopModule m@(Module _moduleKw path doc body) = do
   r <- checkedModule
   modify (over (scoperModulesCache . cachedModules) (HashMap.insert path r))
   registerModule (r ^. moduleRefModule)
@@ -563,14 +563,12 @@ checkTopModule m@(Module _moduleKw path params doc body) = do
     checkedModule = do
       (s, (m', p)) <- runState iniScope $ do
         path' <- freshTopModulePath
-        localScope $
+        localScope $ do
-          withParams params $ \params' -> do
           (_moduleExportInfo, body') <- checkModuleBody body
           doc' <- mapM checkJudoc doc
           let _moduleRefModule =
                 Module
                   { _modulePath = path',
-                      _moduleParameters = params',
                     _moduleBody = body',
                     _moduleDoc = doc',
                     _moduleKw
@@ -604,20 +602,18 @@ checkLocalModule ::
   Module 'Parsed 'ModuleLocal ->
   Sem r (Module 'Scoped 'ModuleLocal)
 checkLocalModule Module {..} = do
-  (_moduleExportInfo, moduleBody', moduleParameters', moduleDoc') <-
+  (_moduleExportInfo, moduleBody', moduleDoc') <-
-    withScope $
+    withScope $ do
-      withParams _moduleParameters $ \p' -> do
       inheritScope
       (e, b) <- checkModuleBody _moduleBody
       doc' <- mapM checkJudoc _moduleDoc
-        return (e, b, p', doc')
+      return (e, b, doc')
   _modulePath' <- reserveSymbolOf S.KNameLocalModule _modulePath
   let moduleId = _modulePath' ^. S.nameId
       _moduleRefName = set S.nameConcrete () _modulePath'
       _moduleRefModule =
         Module
           { _modulePath = _modulePath',
-            _moduleParameters = moduleParameters',
             _moduleBody = moduleBody',
             _moduleDoc = moduleDoc',
             _moduleKw
@@ -710,13 +706,11 @@ checkOpenModuleNoImport OpenModule {..}
   | isJust _openModuleImportKw = error "unsupported: open import statement"
   | otherwise = do
       openModuleName'@(ModuleRef' (_ :&: moduleRef'')) <- lookupModuleSymbol _openModuleName
-      openParameters' <- mapM checkParseExpressionAtoms _openParameters
       mergeScope (alterScope (moduleRef'' ^. moduleExportInfo))
       registerName (moduleRef'' ^. moduleRefName)
       return
         OpenModule
           { _openModuleName = openModuleName',
-            _openParameters = openParameters',
             ..
           }
   where