Modify open import syntax (#2098)

anoma · May 17, 2023 · a164083 · a164083
1 parent d135f74
commit a164083
Show file tree

Hide file tree

Showing 17 changed files with 124 additions and 35 deletions.
diff --git a/examples/milestone/TicTacToe/CLI/TicTacToe.juvix b/examples/milestone/TicTacToe/CLI/TicTacToe.juvix
@@ -5,9 +5,9 @@
 --- The module Logic.Game contains the game logic.
 module CLI.TicTacToe;
 
-open import Stdlib.Data.Nat.Ord;
-open import Stdlib.Prelude;
-open import Logic.Game;
+import Stdlib.Data.Nat.Ord open;
+import Stdlib.Prelude open;
+import Logic.Game open;
 
 --- A ;String; that prompts the user for their input
 prompt : GameState → String;

diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs
@@ -530,6 +530,9 @@ data SymbolEntry
   | EntryVariable (S.Name' ())
   deriving stock (Show)
 
+instance SingI t => CanonicalProjection (ModuleRef'' c t) (ModuleRef' c) where
+  project r = ModuleRef' (sing :&: r)
+
 -- | Symbols that a module exports
 newtype ExportInfo = ExportInfo
   { _exportSymbols :: HashMap Symbol SymbolEntry
@@ -540,6 +543,7 @@ data OpenModule (s :: Stage) = OpenModule
   { _openModuleKw :: KeywordRef,
     _openModuleName :: ModuleRefType s,
     _openModuleImportKw :: Maybe KeywordRef,
+    _openImportAsName :: Maybe (ModulePathType s 'ModuleTop),
     _openUsingHiding :: Maybe UsingHiding,
     _openPublic :: PublicAnn
   }
@@ -548,6 +552,7 @@ deriving stock instance
   ( Eq (IdentifierType s),
     Eq (SymbolType s),
     Eq (ModuleRefType s),
+    Eq (ModulePathType s 'ModuleTop),
     Eq (PatternType s),
     Eq (ExpressionType s)
   ) =>
@@ -557,6 +562,7 @@ deriving stock instance
   ( Ord (IdentifierType s),
     Ord (SymbolType s),
     Ord (PatternType s),
+    Ord (ModulePathType s 'ModuleTop),
     Ord (ModuleRefType s),
     Ord (ExpressionType s)
   ) =>
@@ -565,6 +571,7 @@ deriving stock instance
 deriving stock instance
   ( Show (IdentifierType s),
     Show (ModuleRefType s),
+    Show (ModulePathType s 'ModuleTop),
     Show (ExpressionType s)
   ) =>
   Show (OpenModule s)

diff --git a/src/Juvix/Compiler/Concrete/Pretty/Base.hs b/src/Juvix/Compiler/Concrete/Pretty/Base.hs
@@ -351,7 +351,20 @@ instance (SingI s) => PrettyCode (OpenModule s) where
     openUsingHiding' <- mapM ppUsingHiding _openUsingHiding
     importkw' <- mapM ppCode _openModuleImportKw
     let openPublic' = ppPublic
-    return $ kwOpen <+?> importkw' <+> openModuleName' <+?> openUsingHiding' <+?> openPublic'
+    alias' <- fmap (kwAs <+>) <$> mapM ppModulePathType _openImportAsName
+    return $ case importkw' of
+      Nothing ->
+        kwOpen
+          <+> openModuleName'
+          <+?> openUsingHiding'
+          <+?> openPublic'
+      Just importkw ->
+        importkw
+          <+> openModuleName'
+          <+?> alias'
+          <+> kwOpen
+          <+?> openUsingHiding'
+          <+?> openPublic'
     where
       ppUsingHiding :: UsingHiding -> Sem r (Doc Ann)
       ppUsingHiding uh = do

diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -283,14 +283,24 @@ instance PrettyPrint (OpenModule 'Scoped) where
     let name' = ppCode _openModuleName
         usingHiding' = ppCode <$> _openUsingHiding
         importkw' = ppCode <$> _openModuleImportKw
+        openkw = ppCode _openModuleKw
+        alias' = (noLoc P.kwAs <+>) . ppCode <$> _openImportAsName
         public' = case _openPublic of
           Public -> Just (noLoc P.kwPublic)
           NoPublic -> Nothing
-    ppCode _openModuleKw
-      <+?> importkw'
-      <+> name'
-      <+?> usingHiding'
-      <+?> public'
+    case importkw' of
+      Nothing -> do
+        openkw
+          <+> name'
+          <+?> usingHiding'
+          <+?> public'
+      Just importkw ->
+        importkw
+          <+> name'
+          <+?> alias'
+          <+> openkw
+          <+?> usingHiding'
+          <+?> public'
 
 instance PrettyPrint (FunctionClause 'Scoped) where
   ppCode :: forall r. Members '[ExactPrint, Reader Options] r => FunctionClause 'Scoped -> Sem r ()

diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -756,11 +756,31 @@ checkOpenImportModule ::
 checkOpenImportModule op
   | Just k <- op ^. openModuleImportKw =
       let import_ :: Import 'Parsed
-          import_ = Import k (moduleNameToTopModulePath (op ^. openModuleName)) Nothing
+          import_ =
+            Import
+              { _importKw = k,
+                _importModule = moduleNameToTopModulePath (op ^. openModuleName),
+                _importAsName = op ^. openImportAsName
+              }
        in do
-            void (checkImport import_)
-            scopedOpen <- checkOpenModule (set openModuleImportKw Nothing op)
-            return (set openModuleImportKw (Just k) scopedOpen)
+            import' <- checkImport import_
+            let topName :: S.TopModulePath = over S.nameConcrete moduleNameToTopModulePath (import' ^. importModule . moduleRefName)
+                op' =
+                  op
+                    { _openModuleImportKw = Nothing,
+                      _openImportAsName = Nothing,
+                      _openModuleName = maybe (op ^. openModuleName) topModulePathToName (op ^. openImportAsName)
+                    }
+            scopedOpen <- checkOpenModuleNoImport op'
+            return
+              scopedOpen
+                { _openModuleImportKw = Just k,
+                  _openModuleName = project (import' ^. importModule),
+                  _openImportAsName =
+                    if
+                        | Just asTxt <- (op ^. openImportAsName) -> Just (set S.nameConcrete asTxt topName)
+                        | otherwise -> Nothing
+                }
   | otherwise = impossible
 
 checkOpenModuleNoImport ::
@@ -777,6 +797,7 @@ checkOpenModuleNoImport OpenModule {..}
       return
         OpenModule
           { _openModuleName = openModuleName',
+            _openImportAsName = Nothing,
             ..
           }
   where

diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -244,6 +244,7 @@ statement = P.label "<top level statement>" $ do
   ms <-
     optional
       ( StatementOperator <$> operatorSyntaxDef
+          <|> P.try (StatementOpenModule <$> newOpenSyntax)
           <|> StatementOpenModule <$> openModule
           <|> StatementImport <$> import_
           <|> StatementInductive <$> inductiveDef Nothing
@@ -780,9 +781,28 @@ openModule = do
   _openParameters <- many atomicExpression
   _openUsingHiding <- optional usingOrHiding
   _openPublic <- maybe NoPublic (const Public) <$> optional (kw kwPublic)
-  return OpenModule {..}
-  where
-    usingOrHiding :: ParsecS r UsingHiding
-    usingOrHiding =
-      (kw kwUsing >> (Using <$> symbolList))
-        <|> (kw kwHiding >> (Hiding <$> symbolList))
+  return
+    OpenModule
+      { _openImportAsName = Nothing,
+        ..
+      }
+
+usingOrHiding :: (Members '[Error ParserError, InfoTableBuilder, JudocStash, NameIdGen, PragmasStash] r) => ParsecS r UsingHiding
+usingOrHiding =
+  (kw kwUsing >> (Using <$> symbolList))
+    <|> (kw kwHiding >> (Hiding <$> symbolList))
+
+newOpenSyntax :: forall r. (Members '[Error ParserError, PathResolver, Files, InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (OpenModule 'Parsed)
+newOpenSyntax = do
+  im <- import_
+  _openModuleKw <- kw kwOpen
+  _openParameters <- many atomicExpression
+  _openUsingHiding <- optional usingOrHiding
+  _openPublic <- maybe NoPublic (const Public) <$> optional (kw kwPublic)
+  let _openModuleName = topModulePathToName (im ^. importModule)
+      _openModuleImportKw = Just (im ^. importKw)
+      _openImportAsName = im ^. importAsName
+  return
+    OpenModule
+      { ..
+      }
diff --git a/test/Scope/Positive.hs b/test/Scope/Positive.hs
@@ -226,5 +226,9 @@ tests =
     PosTest
       "Pragmas"
       $(mkRelDir ".")
-      $(mkRelFile "Pragmas.juvix")
+      $(mkRelFile "Pragmas.juvix"),
+    PosTest
+      "Import as open"
+      $(mkRelDir "ImportAsOpen")
+      $(mkRelFile "Main.juvix")
   ]
diff --git a/tests/positive/Format.juvix b/tests/positive/Format.juvix
@@ -1,7 +1,7 @@
 module Format;
 
-open import Stdlib.Prelude hiding {,};
-open import Stdlib.Data.Nat.Ord;
+import Stdlib.Prelude open hiding {,};
+import Stdlib.Data.Nat.Ord open;
 
 terminating
 go : Nat → Nat → Nat;

diff --git a/tests/positive/ImportAsOpen/Main.juvix b/tests/positive/ImportAsOpen/Main.juvix
@@ -0,0 +1,9 @@
+module Main;
+
+import Other as O open;
+
+B : Type;
+B := A;
+
+B' : Type;
+B' := O.A;
diff --git a/tests/positive/ImportAsOpen/Other.juvix b/tests/positive/ImportAsOpen/Other.juvix
@@ -0,0 +1,3 @@
+module Other;
+
+axiom A : Type;
diff --git a/tests/positive/ImportAsOpen/juvix.yaml b/tests/positive/ImportAsOpen/juvix.yaml
diff --git a/tests/positive/ImportShadow/Main.juvix b/tests/positive/ImportShadow/Main.juvix
@@ -1,6 +1,6 @@
 module Main;
 
-open import Nat;
+import Nat open;
 
 type Unit :=
   | unit : Unit;
@@ -13,7 +13,9 @@ f :=
 f2 : Nat;
 f2 :=
   case suc zero
-    | suc is-zero := zero;
+    | suc is-zero := zero
+    | _ := zero;
 
 f3 : Nat → Nat;
 f3 (suc is-zero) := is-zero;
+f3 zero := zero;
diff --git a/tests/positive/Internal/Case.juvix b/tests/positive/Internal/Case.juvix
@@ -1,6 +1,6 @@
 module Case;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 isZero : Nat → Bool;
 isZero n :=

diff --git a/tests/positive/Pragmas.juvix b/tests/positive/Pragmas.juvix
@@ -1,7 +1,7 @@
 {-# unknownPragma: 300 #-}
 module Pragmas;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 {-# unknownPragma: 0 #-}
 axiom a : Nat;

diff --git a/tests/positive/SignatureWithBody.juvix b/tests/positive/SignatureWithBody.juvix
@@ -1,6 +1,6 @@
 module SignatureWithBody;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 isNull :
   {A : Type} → List A → Bool :=

diff --git a/tests/positive/Symbols.juvix b/tests/positive/Symbols.juvix
@@ -1,6 +1,6 @@
 module Symbols;
 
-open import Stdlib.Data.Nat;
+import Stdlib.Data.Nat open;
 
 ╘⑽╛ : Nat;
 ╘⑽╛ := suc 9;

diff --git a/tests/smoke/Commands/format.smoke.yaml b/tests/smoke/Commands/format.smoke.yaml
@@ -159,12 +159,12 @@ tests:
       - --stdin
       - format
       - positive/Format.juvix
-    stdin: 'module Format; open import Stdlib.Prelude; main : Nat; main := 5; '
+    stdin: 'module Format; import Stdlib.Prelude open; main : Nat; main := 5; '
     stdout:
       contains: |
         module Format;
 
-        open import Stdlib.Prelude;
+        import Stdlib.Prelude open;
 
         main : Nat;
         main := 5;
@@ -176,7 +176,7 @@ tests:
       - --stdin
       - format
       - positive/NonExistingFormat.juvix
-    stdin: 'module Format; open import Stdlib.Prelude; main : Nat; main := 5; '
+    stdin: 'module Format; import Stdlib.Prelude open; main : Nat; main := 5; '
     stderr:
       contains: |
         positive/NonExistingFormat.juvix" does not exist
@@ -188,7 +188,7 @@ tests:
       - --stdin
       - format
       - positive/Format.juvix
-    stdin: 'module OtherFormat; open import Stdlib.Prelude; main : Nat; main := 5; '
+    stdin: 'module OtherFormat; import Stdlib.Prelude open; main : Nat; main := 5; '
     stderr:
       contains: 'is defined in the file'
     exit-status: 1
@@ -198,12 +198,12 @@ tests:
       - juvix
       - --stdin
       - format
-    stdin: 'module OtherFormat; open import Stdlib.Prelude; main : Nat; main := 5; '
+    stdin: 'module OtherFormat; import Stdlib.Prelude open; main : Nat; main := 5; '
     stdout:
       contains: |
         module OtherFormat;
 
-        open import Stdlib.Prelude;
+        import Stdlib.Prelude open;
 
         main : Nat;
         main := 5;
@@ -213,7 +213,7 @@ tests:
     command:
       - juvix
       - format
-    stdin: 'module OtherFormat; open import Stdlib.Prelude; main : Nat; main := 5module OtherFormat; open import Stdlib.Prelude; main : Nat; main := 5;; '
+    stdin: 'module OtherFormat; import Stdlib.Prelude open; main : Nat; main := 5module OtherFormat; import Stdlib.Prelude open; main : Nat; main := 5;; '
     stdout:
       contains: juvix format error
     exit-status: 1