diff --git a/examples/milestone/TicTacToe/CLI/TicTacToe.juvix b/examples/milestone/TicTacToe/CLI/TicTacToe.juvix index 216135e7a3..a610b04aaa 100644 --- 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 index 4829713397..fc3b191248 100644 --- 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 index b2aa9d7983..cb21b993c2 100644 --- 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 index cf9f81337d..52c1d5199e 100644 --- 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 index ead22d25ec..8ea473565b 100644 --- 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 index 30bd158273..dd5ee3ec83 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -244,6 +244,7 @@ statement = P.label "" $ 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 index 7106db09ee..73aaddb1ed 100644 --- 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 index e8904c8d2b..e5fcd92fbf 100644 --- 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 new file mode 100644 index 0000000000..5f4866f663 --- /dev/null +++ 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 new file mode 100644 index 0000000000..9df816462b --- /dev/null +++ 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 new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tests/positive/ImportShadow/Main.juvix b/tests/positive/ImportShadow/Main.juvix index b9de8939d8..3768259907 100644 --- 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 index 8db7db5708..1508272fcb 100644 --- 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 index 5eb0f671f8..10f0afdbff 100644 --- 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 index 8de326d531..fcbdd9f703 100644 --- 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 index b807efb776..7930b04033 100644 --- 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 index 6e50325e18..dbd9e55cce 100644 --- 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