Allow local modules to be forward referenced (#3275)

This pr makes a number of changes to the Scoper. The most important
change is that local modules can be forward referenced. Below I list all
the changes.

- Closes #3032 

# Referencing local modules
Local modules can now be forward referenced. However, there is one
restriction:
1. When forward referencing a local module. The symbols that come from
an `open public` are **not** yet in scope, so they can't be referenced.
E.g.
   ```
   -- at this point, P.p is in scope, but P.m is not

   module P;
     axiom p : Type;

     open M public;
   end;

   -- at this point, both P.p and P.m are in scope

   module M;
     axiom m : Type;
   end;
   ```

# Forward reference passed an import, open or module statement
The following example was not allowed but now it is.
```
axiom A : B;
import M;
module S;
end;
axiom B : Type;
```

# Changes in operators and iteratos
The semantics of operator and iterator definitions have changed
slightly. Before, when the scoper found `syntax operator , pair`, it
would remember in the state that when the `,` symbol is defined in the
current syntax block, it should have the fixity `pair`. These had some
implications.
1. It was not possible to reassign/overwrite a fixity.
1. The `,` symbol in the `syntax operator , pair` is not highlighted and
it doesn't support going to definition.
2. We required special checks to throw an error when we had duplicate
operator/iterator definitions. We also had a check for when a symbol
used in an operator/iterator statement was not defined in the same
syntax block.

The new behaviour is as follows.
1. When the scoper finds `syntax operator , pair`, the symbol `,` is
scoped using the regular scoping rules - so `,` must be in scope. Then,
the scoper modifies the fixity for `,` in the current scope.
2. It is now possible to overwrite the fixity of a symbol. So this would
be possible.
```
syntax operator , pair;
p1 : Pair Nat Nat := 1, 2;
syntax operator , none;
p2 : Pair Nat Nat := , 1 2;
``` 
6. It is now possible to have qualified names in syntax/iterator
definitions. E.g. `syntax operator Pair., pair`.

Because of point 1) we might encounter some breaking changes.
1. ```
   syntax operator mkpair none;
   syntax alias mkpair := ,;
   ```
This is now invalid because `mkpair` is not in scope in the `syntax
operator`
   statement, because aliases cannot be forward referenced.
2. A `syntax operator op fix` will now throw an ambiguity error if `op`
is both defined in this module and imported from somewhere else.
# Qualified fixities
It is now possible to reference fixities using qualified names. E.g.
```
syntax operator , Fixities.pair;
```
# Pending tasks

- [x] Add positive test for local module forward referencing.
- [x] Add positive test for fixity overwriting.
- [x] Add positive test for qualified fixity.
- [x] Add positive test for qualified operator.
- [x] Add negative tests for local module forward referencing
restrictions.
- [x] Fix printing of operators in Core.
- [x] Cleanup the code.

include/package/PackageDescription/V2.juvix

@@ -30,7 +30,7 @@ type SemVer :=
 --- A ;Dependency; defines a Juvix package dependency.
 type Dependency :=
   | --- A filesystem path to another Juvix Package.
-    path@{path : String}
+    path@{pathStr : String}
   | --- A ;git; repository containing a Juvix package at its root
     git@{
       -- A name for this dependency

src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs

@@ -459,14 +459,14 @@ goFixity def = do
 
     mkPrec :: Sem r Html
     mkPrec = case info ^. fixityPrecSame of
-      Just (txt :: S.Symbol) -> do
+      Just (txt :: ScopedIden) -> do
         d <- ppCodeHtml defaultOptions txt
         return (row $ toHtml ("Same precedence as " <> d))
       Nothing ->
         goPrec "Higher" (info ^. fixityPrecAbove)
           <> goPrec "Lower" (info ^. fixityPrecBelow)
         where
-          goPrec :: Html -> Maybe [S.Symbol] -> Sem r Html
+          goPrec :: Html -> Maybe [ScopedIden] -> Sem r Html
           goPrec above ls = do
             semicolon' <- semiSeparator
             case ls >>= nonEmpty of

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

@@ -18,15 +18,15 @@ data InfoTableBuilder :: Effect where
   RegisterName :: (HasLoc c) => Bool -> S.Name' c -> InfoTableBuilder m ()
   RegisterScopedIden :: Bool -> ScopedIden -> InfoTableBuilder m ()
   RegisterModuleDoc :: S.NameId -> Maybe (Judoc 'Scoped) -> InfoTableBuilder m ()
-  RegisterFixity :: FixityDef -> InfoTableBuilder m ()
+  RegisterFixityDef :: FixityDef -> InfoTableBuilder m ()
   RegisterPrecedence :: S.NameId -> S.NameId -> InfoTableBuilder m ()
   RegisterHighlightDoc :: S.NameId -> Maybe (Judoc 'Scoped) -> InfoTableBuilder m ()
   RegisterNameSig :: S.NameId -> NameSignature 'Scoped -> InfoTableBuilder m ()
   RegisterConstructorSig :: S.NameId -> RecordNameSignature 'Scoped -> InfoTableBuilder m ()
   RegisterParsedNameSig :: S.NameId -> NameSignature 'Parsed -> InfoTableBuilder m ()
   RegisterParsedConstructorSig :: S.NameId -> RecordNameSignature 'Parsed -> InfoTableBuilder m ()
   RegisterRecordInfo :: S.NameId -> RecordInfo -> InfoTableBuilder m ()
-  RegisterAlias :: S.NameId -> PreSymbolEntry -> InfoTableBuilder m ()
+  RegisterAlias :: S.NameId -> ScopedIden -> InfoTableBuilder m ()
   RegisterLocalModule :: ScopedModule -> InfoTableBuilder m ()
   GetBuilderInfoTable :: InfoTableBuilder m InfoTable
   GetBuiltinSymbol' :: Interval -> BuiltinPrim -> InfoTableBuilder m S.Symbol
@@ -68,9 +68,9 @@ runInfoTableBuilder ini = reinterpret (runState ini) $ \case
   RegisterName isTop n -> highlightName (S.anameFromName isTop n)
   RegisterScopedIden isTop n -> highlightName (anameFromScopedIden isTop n)
   RegisterModuleDoc uid doc -> highlightDoc uid doc
-  RegisterFixity f -> do
+  RegisterFixityDef f -> do
     let sid = f ^. fixityDefSymbol . S.nameId
-    modify (over infoFixities (HashMap.insert sid f))
+    modify (set (infoFixities . at sid) (Just f))
     case f ^. fixityDefFixity . fixityId of
       Just fid -> modify (over infoPrecedenceGraph (HashMap.alter (Just . fromMaybe mempty) fid))
       Nothing -> return ()

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

@@ -77,6 +77,7 @@ instance HasLoc SymbolPath where
 
 deriving newtype instance Hashable SymbolPath
 
+makePrisms ''Name
 makeLenses ''QualifiedName
 makeLenses ''SymbolPath
 

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

@@ -42,6 +42,18 @@ nameSpaceElemName = \case
   NameSpaceModules -> "module"
   NameSpaceFixities -> "fixity"
 
+nsEntry :: forall ns. (SingI ns) => Lens' (NameSpaceEntryType ns) S.Name
+nsEntry = case sing :: SNameSpace ns of
+  SNameSpaceModules -> moduleEntry
+  SNameSpaceSymbols -> preSymbolName
+  SNameSpaceFixities -> fixityEntry
+
+shouldExport :: (SingI ns) => NameSpaceEntryType ns -> Bool
+shouldExport ent = ent ^. nsEntry . S.nameVisibilityAnn == VisPublic
+
+forEachNameSpace :: (Monad m) => (forall (ns :: NameSpace). Sing ns -> m ()) -> m ()
+forEachNameSpace f = sequence_ [withSomeSing ns f | ns <- allElements]
+
 entryName :: forall ns. (SingI ns) => Lens' (NameSpaceEntryType ns) S.Name
 entryName = case sing :: SNameSpace ns of
   SNameSpaceSymbols -> \f -> \case

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

@@ -14,7 +14,4 @@ instance Serialize PublicAnn
 
 instance NFData PublicAnn
 
-_Public :: Traversal' PublicAnn KeywordRef
-_Public f = \case
-  NoPublic -> pure NoPublic
-  Public (Irrelevant x) -> Public . Irrelevant <$> f x
+makePrisms ''PublicAnn

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

@@ -11,36 +11,10 @@ import Juvix.Compiler.Concrete.Data.Scope.Base
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Store.Scoped.Data.InfoTable
-import Juvix.Compiler.Store.Scoped.Language
 import Juvix.Prelude
 
-nsEntry :: forall ns. (SingI ns) => Lens' (NameSpaceEntryType ns) S.Name
-nsEntry = case sing :: SNameSpace ns of
-  SNameSpaceModules -> moduleEntry
-  SNameSpaceSymbols -> preSymbolName
-  SNameSpaceFixities -> fixityEntry
-
-scopeNameSpace :: forall (ns :: NameSpace). (SingI ns) => Lens' Scope (HashMap Symbol (SymbolInfo ns))
-scopeNameSpace = case sing :: SNameSpace ns of
-  SNameSpaceSymbols -> scopeSymbols
-  SNameSpaceModules -> scopeModuleSymbols
-  SNameSpaceFixities -> scopeFixitySymbols
-
-scopeNameSpaceLocal :: forall (ns :: NameSpace). Sing ns -> Lens' Scope (HashMap Symbol S.Symbol)
-scopeNameSpaceLocal s = case s of
-  SNameSpaceSymbols -> scopeLocalSymbols
-  SNameSpaceModules -> scopeLocalModuleSymbols
-  SNameSpaceFixities -> scopeLocalFixitySymbols
-
-emptyScope :: S.AbsModulePath -> Scope
-emptyScope absPath =
-  Scope
-    { _scopePath = absPath,
-      _scopeSymbols = mempty,
-      _scopeModuleSymbols = mempty,
-      _scopeFixitySymbols = mempty,
-      _scopeTopModules = mempty,
-      _scopeLocalSymbols = mempty,
-      _scopeLocalModuleSymbols = mempty,
-      _scopeLocalFixitySymbols = mempty
-    }
+scopeReservedNameSpace :: forall (ns :: NameSpace). Sing ns -> Lens' Scope (HashMap Symbol S.Symbol)
+scopeReservedNameSpace s = case s of
+  SNameSpaceSymbols -> scopeReservedSymbols
+  SNameSpaceModules -> scopeReservedLocalModuleSymbols
+  SNameSpaceFixities -> scopeReservedFixitySymbols

src/Juvix/Compiler/Concrete/Data/Scope/Base.hs

@@ -27,24 +27,36 @@ data BindingStrategy
   | -- | Top binding does not allow shadowing. It may result in an ambiguous error
     BindingTop
 
+data InScope = InScope
+  { _inScopeSymbols :: HashMap Symbol (SymbolInfo 'NameSpaceSymbols),
+    -- | Local module symbols (excluding top modules associated with files)
+    _inScopeLocalModuleSymbols :: HashMap Symbol (SymbolInfo 'NameSpaceModules),
+    _inScopeFixitySymbols :: HashMap Symbol (SymbolInfo 'NameSpaceFixities)
+  }
+
+-- | Symbols that have been defined in the current scope level. Every symbol
+-- should map to itself. This is needed because we may query it with a
+-- symbol with a different location but we may want the location of the
+-- original symbol
+data Reserved = Reserved
+  { _reservedLocalSymbols :: HashMap Symbol S.Symbol,
+    _reservedLocalModuleSymbols :: HashMap Symbol S.Symbol,
+    _reservedLocalFixitySymbols :: HashMap Symbol S.Symbol
+  }
+
 data Scope = Scope
   { _scopePath :: S.AbsModulePath,
-    _scopeSymbols :: HashMap Symbol (SymbolInfo 'NameSpaceSymbols),
-    -- | Local module symbols (excluding top modules associated with files)
-    _scopeModuleSymbols :: HashMap Symbol (SymbolInfo 'NameSpaceModules),
-    _scopeFixitySymbols :: HashMap Symbol (SymbolInfo 'NameSpaceFixities),
+    _scopeFixities :: HashMap NameId Fixity,
+    _scopeIterators :: HashMap NameId IteratorInfo,
+    _scopeInScope :: InScope,
+    -- | The name id of the module containing this scope
+    _scopeModuleId :: NameId,
     -- | The map from S.NameId to Modules is needed because we support merging
     -- several imports under the same name. E.g.
     -- import A as X;
     -- import B as X;
-    _scopeTopModules :: HashMap TopModulePathKey (HashMap S.NameId ScopedModule),
-    -- | Symbols that have been defined in the current scope level. Every symbol
-    -- should map to itself. This is needed because we may query it with a
-    -- symbol with a different location but we may want the location of the
-    -- original symbol
-    _scopeLocalSymbols :: HashMap Symbol S.Symbol,
-    _scopeLocalModuleSymbols :: HashMap Symbol S.Symbol,
-    _scopeLocalFixitySymbols :: HashMap Symbol S.Symbol
+    _scopeImports :: HashMap TopModulePathKey (HashMap S.NameId ScopedModule),
+    _scopeReserved :: Reserved
   }
 
 newtype ModulesCache = ModulesCache
@@ -55,10 +67,24 @@ newtype ScopeParameters = ScopeParameters
   { _scopeImportedModules :: HashMap TopModulePathKey ScopedModule
   }
 
+data ModuleExportInfo = ModuleExportInfo
+  { -- | The name of the module
+    _moduleExportInfoModuleName :: S.Name,
+    _moduleExportInfo :: ExportInfo
+  }
+
+data ReservedModule = ReservedModule
+  { _reservedModuleName :: S.Name,
+    _reservedModuleReserved :: Reserved,
+    _reservedModuleStatements :: [Statement 'Parsed]
+  }
+
 data ScoperState = ScoperState
   { -- | Local and top modules currently in scope - used to look up qualified symbols
     _scoperModules :: HashMap S.NameId ScopedModule,
-    _scoperAlias :: HashMap S.NameId PreSymbolEntry,
+    _scoperReservedModules :: HashMap S.NameId ReservedModule,
+    _scoperExportInfo :: HashMap S.NameId ModuleExportInfo,
+    _scoperAlias :: HashMap S.NameId ScopedIden,
     _scoperNameSignatures :: HashMap S.NameId (NameSignature 'Parsed),
     -- | Indexed by the inductive type. This is used for record updates
     _scoperRecordFields :: HashMap S.NameId RecordInfo,
@@ -67,10 +93,8 @@ data ScoperState = ScoperState
     _scoperScopedConstructorFields :: HashMap S.NameId (RecordNameSignature 'Scoped)
   }
 
-data SymbolOperator = SymbolOperator
-  { _symbolOperatorUsed :: Bool,
-    _symbolOperatorFixity :: Fixity,
-    _symbolOperatorDef :: OperatorSyntaxDef 'Parsed
+newtype SymbolOperator = SymbolOperator
+  { _symbolOperatorDef :: OperatorSyntaxDef 'Parsed
   }
   deriving stock (Show)
 
@@ -89,21 +113,87 @@ newtype ScoperIterators = ScoperIterators
   }
   deriving newtype (Semigroup, Monoid)
 
-data ScoperSyntax = ScoperSyntax
-  { _scoperSyntaxOperators :: ScoperOperators,
-    _scoperSyntaxIterators :: ScoperIterators
-  }
-
-emptyScoperSyntax :: ScoperSyntax
-emptyScoperSyntax = ScoperSyntax mempty mempty
-
 makeLenses ''ScoperIterators
+makeLenses ''ModuleExportInfo
+makeLenses ''InScope
+makeLenses ''ReservedModule
 makeLenses ''SymbolOperator
 makeLenses ''SymbolIterator
 makeLenses ''SymbolInfo
 makeLenses ''Scope
 makeLenses ''ScoperOperators
-makeLenses ''ScoperSyntax
 makeLenses ''ScoperState
 makeLenses ''ScopeParameters
 makeLenses ''ModulesCache
+makeLenses ''Reserved
+
+scopedModuleToModuleExportInfo :: ScopedModule -> ModuleExportInfo
+scopedModuleToModuleExportInfo scoped =
+  ModuleExportInfo
+    { _moduleExportInfoModuleName = scoped ^. scopedModuleName,
+      _moduleExportInfo = scoped ^. scopedModuleExportInfo
+    }
+
+emptyReserved :: Reserved
+emptyReserved =
+  Reserved
+    { _reservedLocalSymbols = mempty,
+      _reservedLocalModuleSymbols = mempty,
+      _reservedLocalFixitySymbols = mempty
+    }
+
+emptyInScope :: InScope
+emptyInScope =
+  InScope
+    { _inScopeSymbols = mempty,
+      _inScopeLocalModuleSymbols = mempty,
+      _inScopeFixitySymbols = mempty
+    }
+
+emptyScopeTop :: NameId -> S.AbsModulePath -> Scope
+emptyScopeTop modId absPath =
+  Scope
+    { _scopePath = absPath,
+      _scopeFixities = mempty,
+      _scopeIterators = mempty,
+      _scopeModuleId = modId,
+      _scopeInScope = emptyInScope,
+      _scopeImports = mempty,
+      _scopeReserved = emptyReserved
+    }
+
+scopeNameSpaceI :: forall (ns :: NameSpace). (SingI ns) => Lens' Scope (HashMap Symbol (SymbolInfo ns))
+scopeNameSpaceI = scopeNameSpace sing
+
+scopeNameSpace :: forall (ns :: NameSpace). Sing ns -> Lens' Scope (HashMap Symbol (SymbolInfo ns))
+scopeNameSpace = \case
+  SNameSpaceSymbols -> scopeSymbols
+  SNameSpaceModules -> scopeModuleSymbols
+  SNameSpaceFixities -> scopeFixitySymbols
+
+reservedNameSpace ::
+  forall (ns :: NameSpace).
+  Sing ns ->
+  Lens' Reserved (HashMap Symbol S.Symbol)
+reservedNameSpace = \case
+  SNameSpaceSymbols -> reservedLocalSymbols
+  SNameSpaceModules -> reservedLocalModuleSymbols
+  SNameSpaceFixities -> reservedLocalFixitySymbols
+
+scopeSymbols :: Lens' Scope (HashMap Symbol (SymbolInfo 'NameSpaceSymbols))
+scopeSymbols = scopeInScope . inScopeSymbols
+
+scopeModuleSymbols :: Lens' Scope (HashMap Symbol (SymbolInfo 'NameSpaceModules))
+scopeModuleSymbols = scopeInScope . inScopeLocalModuleSymbols
+
+scopeFixitySymbols :: Lens' Scope (HashMap Symbol (SymbolInfo 'NameSpaceFixities))
+scopeFixitySymbols = scopeInScope . inScopeFixitySymbols
+
+scopeReservedSymbols :: Lens' Scope (HashMap Symbol S.Symbol)
+scopeReservedSymbols = scopeReserved . reservedLocalSymbols
+
+scopeReservedLocalModuleSymbols :: Lens' Scope (HashMap Symbol S.Symbol)
+scopeReservedLocalModuleSymbols = scopeReserved . reservedLocalModuleSymbols
+
+scopeReservedFixitySymbols :: Lens' Scope (HashMap Symbol S.Symbol)
+scopeReservedFixitySymbols = scopeReserved . reservedLocalFixitySymbols

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

@@ -1,5 +1,6 @@
 module Juvix.Compiler.Concrete.Data.VisibilityAnn where
 
+import Juvix.Data.CodeAnn
 import Juvix.Extra.Serialize
 import Juvix.Prelude
 
@@ -10,6 +11,12 @@ data VisibilityAnn
 
 instance Serialize VisibilityAnn
 
+instance PrettyCodeAnn VisibilityAnn where
+  ppCodeAnn k =
+    annotate AnnKeyword $ case k of
+      VisPublic -> "Public"
+      VisPrivate -> "Private"
+
 instance NFData VisibilityAnn
 
 instance Semigroup VisibilityAnn where

src/Juvix/Compiler/Concrete/Extra.hs

@@ -52,8 +52,8 @@ groupStatements = \case
       (StatementDeriving _, _) -> False
       (StatementSyntax _, StatementSyntax _) -> True
       (StatementSyntax (SyntaxFixity _), _) -> False
-      (StatementSyntax (SyntaxOperator o), s) -> definesSymbol (o ^. opSymbol) s
-      (StatementSyntax (SyntaxIterator i), s) -> definesSymbol (i ^. iterSymbol) s
+      (StatementSyntax (SyntaxOperator o), s) -> definesIdentifier (o ^. opSymbol) s
+      (StatementSyntax (SyntaxIterator i), s) -> definesIdentifier (i ^. iterSymbol) s
       (StatementSyntax (SyntaxAlias {}), _) -> False
       (StatementImport _, StatementImport _) -> True
       (StatementImport i, StatementOpenModule o) -> case sing :: SStage s of
@@ -70,6 +70,12 @@ groupStatements = \case
       (_, StatementFunctionDef {}) -> False
       (StatementProjectionDef {}, StatementProjectionDef {}) -> True
       (StatementProjectionDef {}, _) -> False
+
+    definesIdentifier :: IdentifierType s -> Statement s -> Bool
+    definesIdentifier i stm = maybe False (`definesSymbol` stm) $ case sing :: SStage s of
+      SParsed -> i ^? _NameUnqualified
+      SScoped -> i ^? scopedIdenSrcName . S.nameConcrete . _NameUnqualified
+
     definesSymbol :: Symbol -> Statement s -> Bool
     definesSymbol n s = case s of
       StatementInductive d -> n `elem` syms d

src/Juvix/Compiler/Concrete/Language.hs

@@ -40,8 +40,8 @@ statementLabel = \case
     goSyntax :: SyntaxDef s -> Maybe Text
     goSyntax = \case
       SyntaxFixity f -> Just (f ^. fixitySymbol . symbolTypeLabel)
-      SyntaxOperator f -> Just (f ^. opSymbol . symbolTypeLabel)
-      SyntaxIterator f -> Just (f ^. iterSymbol . symbolTypeLabel)
+      SyntaxOperator {} -> Nothing
+      SyntaxIterator {} -> Nothing
       SyntaxAlias f -> Just (f ^. aliasDefName . symbolTypeLabel)
 
 -- | Indexes top statements by label