[scoper] add module not in scope error

src/MiniJuvix/Syntax/Concrete/Name.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 
 module MiniJuvix.Syntax.Concrete.Name where
@@ -26,18 +27,6 @@ instance HasLoc Symbol where
 instance Hashable Symbol where
   hashWithSalt i Symbol {..} = hashWithSalt i _symbolText
 
-data QualifiedName = QualifiedName
-  { qualifiedPath :: Path,
-    qualifiedSymbol :: Symbol
-  }
-  deriving stock (Show, Eq, Ord, Generic, Lift)
-
-instance HasLoc QualifiedName where
-  getLoc QualifiedName {..} =
-    getLoc qualifiedPath <> getLoc qualifiedSymbol
-
-instance Hashable QualifiedName
-
 data Name
   = NameQualified QualifiedName
   | NameUnqualified Symbol
@@ -53,11 +42,25 @@ newtype Path = Path
   }
   deriving stock (Show, Eq, Ord, Lift)
 
+data QualifiedName = QualifiedName
+  { _qualifiedPath :: Path,
+    _qualifiedSymbol :: Symbol
+  }
+  deriving stock (Show, Eq, Ord, Generic, Lift)
+
+instance HasLoc QualifiedName where
+  getLoc QualifiedName {..} =
+    getLoc _qualifiedPath <> getLoc _qualifiedSymbol
+
+instance Hashable QualifiedName
+
 instance HasLoc Path where
   getLoc (Path p) = getLoc (NonEmpty.head p) <> getLoc (NonEmpty.last p)
 
 deriving newtype instance Hashable Path
 
+makeLenses ''QualifiedName
+
 -- | A.B.C corresponds to TopModulePath [A,B] C
 data TopModulePath = TopModulePath
   { modulePathDir :: [Symbol],
@@ -86,5 +89,4 @@ topModulePathToFilePath' ext root mp = absPath
   toPath :: Symbol -> FilePath
   toPath Symbol{..} = unpack _symbolText
 
-
 instance Hashable TopModulePath

src/MiniJuvix/Syntax/Concrete/Scoped/Error.hs

@@ -20,10 +20,9 @@ data ScopeError
   | ErrMultipleDeclarations MultipleDeclarations
   | ErrLacksTypeSig LacksTypeSig
   | ErrImportCycle ImportCycle
-  | ErrOpenNotInScope QualifiedName
   | ErrSymNotInScope NotInScope
   | ErrQualSymNotInScope QualifiedName
-  | ErrModuleNotInScope Name
+  | ErrModuleNotInScope ModuleNotInScope
   | ErrBindGroup BindGroupConflict
   | ErrDuplicateFixity DuplicateFixity
   | ErrMultipleExport MultipleExportConflict
@@ -42,10 +41,9 @@ ppScopeError s = case s of
   ErrMultipleDeclarations e -> ppError e
   ErrLacksTypeSig e -> ppError e
   ErrImportCycle e -> ppError e
-  ErrOpenNotInScope {} -> undefined
   ErrSymNotInScope e -> ppError e
-  ErrQualSymNotInScope {} -> undefined
+  ErrQualSymNotInScope {} -> pretty (show s :: Text)
-  ErrModuleNotInScope {} -> undefined
+  ErrModuleNotInScope e -> ppError e
   ErrBindGroup e -> ppError e
   ErrDuplicateFixity e -> ppError e
   ErrMultipleExport e -> ppError e

src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Base.hs

@@ -112,8 +112,9 @@ instance PrettyError DuplicateFixity where
 
 instance PrettyError MultipleExportConflict where
   ppError MultipleExportConflict {..} =
-    "The symbol" <+> ppCode sym <+> "is exported multiple times in the module" <+> undefined
+    "The symbol" <+> highlight (ppCode _multipleExportSymbol) <+> "is exported multiple times in the module"
-    where
+      <+> ppCode _multipleExportModule
-     sym :: S.Symbol
+
-     sym = undefined
+instance PrettyError ModuleNotInScope where
-     e = NonEmpty.head _multipleExportEntries
+  ppError ModuleNotInScope {..} =
+    "The module" <+> ppCode _moduleNotInScopeName <+> "is not in scope"

src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs

@@ -6,6 +6,7 @@ module MiniJuvix.Syntax.Concrete.Scoped.Error.Types (
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Language
 import MiniJuvix.Syntax.Concrete.Scoped.Scope
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 
 data MultipleDeclarations = MultipleDeclarations {
   _multipleDeclEntry :: SymbolEntry,
@@ -38,13 +39,6 @@ newtype ImportCycle = ImportCycle {
   }
  deriving stock (Show)
 
-data NotInScope = NotInScope {
- _notInScopeSymbol :: Symbol,
- _notInScopeLocal :: LocalVars,
- _notInScopeScope :: Scope
- }
- deriving stock (Show)
-
 data BindGroupConflict = BindGroupConflict {
  _bindGroupFirst :: Symbol,
  _bindGroupSecond :: Symbol
@@ -57,7 +51,21 @@ data DuplicateFixity = DuplicateFixity {
  }
  deriving stock (Show)
 
-newtype MultipleExportConflict = MultipleExportConflict {
+data MultipleExportConflict = MultipleExportConflict {
+  _multipleExportModule :: S.AbsModulePath,
+  _multipleExportSymbol :: Symbol,
   _multipleExportEntries :: NonEmpty SymbolEntry
   }
  deriving stock (Show)
+
+data NotInScope = NotInScope {
+ _notInScopeSymbol :: Symbol,
+ _notInScopeLocal :: LocalVars,
+ _notInScopeScope :: Scope
+ }
+ deriving stock (Show)
+
+newtype ModuleNotInScope = ModuleNotInScope {
+  _moduleNotInScopeName :: Name
+  }
+ deriving stock (Show)

src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs

@@ -9,6 +9,7 @@ import MiniJuvix.Prelude
 import qualified Data.List.NonEmpty.Extra as NonEmpty
 import Prettyprinter hiding (braces, parens)
 import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ann
+import MiniJuvix.Syntax.Concrete.Scoped.Name (AbsModulePath)
 
 data Options = Options
   {
@@ -203,7 +204,9 @@ groupStatements = reverse . map reverse . uncurry cons . foldl' aux ([], [])
     (StatementImport _, StatementImport _) -> True
     (StatementImport i, StatementOpenModule o) -> case sing :: SStage s of
       SParsed -> True
-      SScoped -> S._nameId (modulePath (importModule i)) == S._nameId (openModuleName o)
+      SScoped ->
+        S._nameId (modulePath (importModule i)) ==
+        S._nameId (openModuleName o)
     (StatementImport _, _) -> False
     (StatementOpenModule {}, StatementOpenModule {}) -> True
     (StatementOpenModule {}, _) -> False
@@ -280,6 +283,12 @@ instance SingI s => PrettyCode (InductiveParameter s) where
 instance SingI s => PrettyCode [InductiveParameter s] where
   ppCode = fmap hsep . mapM ppCode
 
+instance PrettyCode AbsModulePath where
+  ppCode S.AbsModulePath {..} = do
+    absLocalPath' <- mapM ppCode absLocalPath
+    absTopModulePath' <- ppCode absTopModulePath
+    return $ dotted (absTopModulePath' : absLocalPath')
+
 ppInductiveParameters :: (SingI s, Members '[Reader Options] r)
     => [InductiveParameter s] -> Sem r (Maybe (Doc Ann))
 ppInductiveParameters ps
@@ -355,7 +364,7 @@ dotted = concatWith (surround kwDot)
 
 instance PrettyCode QualifiedName where
   ppCode QualifiedName {..} = do
-    let symbols = pathParts qualifiedPath NonEmpty.|> qualifiedSymbol
+    let symbols = pathParts _qualifiedPath NonEmpty.|> _qualifiedSymbol
     dotted <$> mapM ppSymbol symbols
 
 ppName :: forall s r. (SingI s, Members '[Reader Options] r) => NameType s -> Sem r (Doc Ann)
@@ -372,7 +381,7 @@ annDef nm = case sing :: SStage s of
   SParsed -> id
 
 annSDef :: S.Name' n -> Doc Ann -> Doc Ann
-annSDef nm = annotate (AnnDef (S.absTopModulePath (S._nameDefinedIn nm)) (S._nameId nm))
+annSDef S.Name' {..} = annotate (AnnDef (S.absTopModulePath _nameDefinedIn) _nameId)
 
 instance PrettyCode TopModulePath where
   ppCode TopModulePath {..} =
@@ -708,22 +717,22 @@ instance HasFixity (ExpressionAtoms 'Parsed) where
   getFixity = const Nothing
 
 pinfixFixity :: PatternInfixApp -> Fixity
-pinfixFixity (PatternInfixApp  _ op _) = case S._nameFixity op of
+pinfixFixity (PatternInfixApp  _ op _) = case op ^. S.nameFixity of
     S.NoFixity -> impossible
     S.SomeFixity s -> s
 
 ppostfixFixity :: PatternPostfixApp -> Fixity
-ppostfixFixity (PatternPostfixApp  _ op) = case S._nameFixity op of
+ppostfixFixity (PatternPostfixApp  _ op) = case op ^. S.nameFixity of
     S.NoFixity -> impossible
     S.SomeFixity s -> s
 
 infixFixity :: InfixApplication -> Fixity
-infixFixity (InfixApplication  _ op _) = case S._nameFixity op of
+infixFixity (InfixApplication  _ op _) = case op ^. S.nameFixity of
     S.NoFixity -> impossible
     S.SomeFixity s -> s
 
 postfixFixity :: PostfixApplication -> Fixity
-postfixFixity (PostfixApplication _ op) = case S._nameFixity op of
+postfixFixity (PostfixApplication _ op) = case op ^. S.nameFixity of
     S.NoFixity -> impossible
     S.SomeFixity s -> s
 

src/MiniJuvix/Syntax/Concrete/Scoped/Scope.hs

@@ -26,29 +26,10 @@ newtype SymbolInfo = SymbolInfo
 
 type SymbolEntry = S.Name' ()
 
--- data SymbolEntry = SymbolEntry
+-- data SymbolEntry' = SymbolEntry' {
---   { _symbolKind :: S.NameKind,
+--   _entryNameInfo :: NameInfo
---     _symbolDefinedIn :: S.AbsModulePath,
+
---     _symbolDefined :: Interval,
---     _symbolId :: S.NameId,
---     _symbolFixity :: S.NameFixity,
---     _symbolWhyInScope :: S.WhyInScope,
---     _symbolPublicAnn :: PublicAnn
 --   }
---   deriving stock (Show)
-
--- getSymbolKind :: SymbolEntry -> S.NameKind
--- getSymbolKind SymbolEntry {..} = fromSing _symbolKind
-
--- instance HasLoc SymbolEntry where
---   getLoc SymbolEntry {..} = case _symbolKind of
---     S.SKNameTopModule -> getLoc _symbolSymbol
---     S.SKNameAxiom -> getLoc _symbolSymbol
---     S.SKNameConstructor -> getLoc _symbolSymbol
---     S.SKNameInductive -> getLoc _symbolSymbol
---     S.SKNameFunction -> getLoc _symbolSymbol
---     S.SKNameLocal -> getLoc _symbolSymbol
---     S.SKNameLocalModule -> getLoc _symbolSymbol
 
 -- | Symbols that a module exports
 newtype ExportInfo = ExportInfo {

src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs

@@ -315,7 +315,7 @@ entryToSName :: s -> SymbolEntry -> S.Name' s
 entryToSName s S.Name' {..} = S.Name' {_nameConcrete = s, ..}
 
 -- | We gather all symbols which have been defined or marked to be public in the given scope.
-exportScope :: forall r. Members '[Error ScopeError] r => Scope -> Sem r ExportInfo
+exportScope :: forall r. Members '[State Scope, Error ScopeError] r => Scope -> Sem r ExportInfo
 exportScope Scope {..} = do
   _exportSymbols <- getExportSymbols
   return ExportInfo {..}
@@ -332,7 +332,8 @@ exportScope Scope {..} = do
           case filter shouldExport (toList _symbolInfo) of
             [] -> return Nothing
             [e] -> return $ Just (s, e)
-            (e:es) -> throw (ErrMultipleExport (MultipleExportConflict (e :| es)))
+            (e:es) -> throw (ErrMultipleExport
+                       (MultipleExportConflict _scopePath  s (e :| es)))
 
 readParseModule ::
   Members '[Error ScopeError, Reader ScopeParameters, Embed IO] r =>
@@ -542,7 +543,7 @@ lookupModuleSymbol n = do
     [x] -> return $ entryToSName n x
     _ -> throw (ErrAmbiguousModuleSym es)
   where
-  notInScope = throw (ErrModuleNotInScope n)
+  notInScope = throw (ErrModuleNotInScope (ModuleNotInScope n))
   (path, sym) = case n of
     NameUnqualified s -> ([], s)
     NameQualified (QualifiedName (Path p) s) -> (toList p, s)

test/Scope/Negative.hs

@@ -96,4 +96,11 @@ tests = [
       case er of
         ErrMultipleExport {} -> Nothing
         _ -> wrongError
+
+  ,  NegTest "Module not in scope"
+    "."
+   "ModuleNotInScope.mjuvix" $ \er ->
+      case er of
+        ErrModuleNotInScope {} -> Nothing
+        _ -> wrongError
   ]

tests/negative/ModuleNotInScope.mjuvix

@@ -0,0 +1,11 @@
+module ModuleNotInScope;
+
+    module A;
+    end;
+
+    axiom M : Type;
+
+    open M;
+
+
+end;