[ Fixed #1388 ] If top-level module declarations are indented, we do

not allow trailing unindented ones.

Fixes issue introduced by commit f304322
which fixed #953.

src/full/Agda/Syntax/Concrete.hs

@@ -43,6 +43,7 @@ module Agda.Syntax.Concrete
   , Module
   , ThingWithFixity(..)
   , topLevelModuleName
+  , spanAllowedBeforeModule
     -- * Pattern tools
   , patternNames, patternQNames
     -- * Lenses
@@ -374,12 +375,29 @@ type Module = ([Pragma], [Declaration])
 -- | Computes the top-level module name.
 --
 -- Precondition: The 'Module' has to be well-formed.
+-- This means that there are only allowed declarations before the
+-- first module declaration, typically import declarations.
+-- See 'spanAllowedBeforeModule'.
 
 topLevelModuleName :: Module -> TopLevelModuleName
 topLevelModuleName (_, []) = __IMPOSSIBLE__
-topLevelModuleName (_, ds) = case last ds of
-  Module _ n _ _ -> toTopLevelModuleName n
-  _              -> __IMPOSSIBLE__
+topLevelModuleName (_, ds) = case spanAllowedBeforeModule ds of
+  (_, Module _ n _ _ : _) -> toTopLevelModuleName n
+  _ -> __IMPOSSIBLE__
+
+-- | Splits off allowed (= import) declarations before the first
+--   non-allowed declaration.
+--   After successful parsing, the first non-allowed declaration
+--   should be a module declaration.
+spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration])
+spanAllowedBeforeModule = span isAllowedBeforeModule
+  where
+    isAllowedBeforeModule (Pragma OptionsPragma{}) = True
+    isAllowedBeforeModule (Private _ ds) = all isAllowedBeforeModule ds
+    isAllowedBeforeModule Import{}       = True
+    isAllowedBeforeModule ModuleMacro{}  = True
+    isAllowedBeforeModule Open{}         = True
+    isAllowedBeforeModule _              = False
 
 {--------------------------------------------------------------------------
     Lenses

src/full/Agda/Syntax/Parser/Parser.y

@@ -1497,18 +1497,27 @@ takeOptionsPragmas = spanJust $ \ d -> case d of
   _                        -> Nothing
 
 -- | Insert a top-level module if there is none.
+--   Also fix-up for the case the declarations in the top-level module
+--   are not indented (this is allowed as a special case).
 figureOutTopLevelModule :: [Declaration] -> [Declaration]
 figureOutTopLevelModule ds =
-  case span isAllowedBeforeModule ds of
-    (ds0, Module r m tel ds1 : ds2) -> ds0 ++ [Module r m tel $ ds1 ++ ds2]
+  case spanAllowedBeforeModule ds of
+    -- Andreas 2016-02-01, issue #1388.
+    -- We need to distinguish two additional cases.
+    -- Case 1: Regular file layout: imports followed by one module. Nothing to do.
+    (ds0, [ Module{} ]) -> ds
+    -- Case 2: The declarations in the module are not indented.
+    -- This is allowed for the top level module, and thus rectified here.
+    (ds0, Module r m tel [] : ds2) -> ds0 ++ [Module r m tel ds2]
+    -- Case 3: There is a module with indented declarations,
+    -- followed by non-indented declarations.  This should be a
+    -- parse error and be reported later (see @toAbstract TopLevel{}@),
+    -- thus, we do not do anything here.
+    (ds0, Module r m tel ds1 : ds2) -> ds  -- Gives parse error in scope checker.
+    -- OLD code causing issue 1388:
+    -- (ds0, Module r m tel ds1 : ds2) -> ds0 ++ [Module r m tel $ ds1 ++ ds2]
+    -- Case 4: a top-level module declaration is missing.
     (ds0, ds1)                      -> ds0 ++ [Module (getRange ds1) (QName noName_) [] ds1]
-  where
-    isAllowedBeforeModule (Pragma OptionsPragma{}) = True
-    isAllowedBeforeModule (Private _ ds) = all isAllowedBeforeModule ds
-    isAllowedBeforeModule Import{}       = True
-    isAllowedBeforeModule ModuleMacro{}  = True
-    isAllowedBeforeModule Open{}         = True
-    isAllowedBeforeModule _              = False
 
 -- | Create a name from a string.
 

src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs

@@ -989,8 +989,15 @@ instance ToAbstract (TopLevel [C.Declaration]) TopLevelInfo where
     toAbstract (TopLevel file ds) =
       -- A file is a bunch of preliminary decls (imports etc.)
       -- plus a single module decl.
-      caseMaybe (initLast ds) __IMPOSSIBLE__ $
-        \ (outsideDecls, C.Module r m0 tel insideDecls) -> do
+      case C.spanAllowedBeforeModule ds of
+
+        -- If there are declarations after the top-level module
+        -- we have to report a parse error here.
+        (_, C.Module{} : d : _) -> traceCall (SetRange $ getRange d) $
+          genericError $ "No declarations allowed after top-level module."
+
+        -- Otherwise, proceed.
+        (outsideDecls, [ C.Module r m0 tel insideDecls ]) -> do
           -- If the module name is _ compute the name from the file path
           m <- if isNoName m0
                 then return $ C.QName $ C.Name noRange [Id $ stringToRawName $ rootName file]
@@ -1010,6 +1017,11 @@ instance ToAbstract (TopLevel [C.Declaration]) TopLevelInfo where
           outsideScope <- getScope
           return $ TopLevelInfo (outsideDecls ++ insideDecls) outsideScope insideScope
 
+        -- We already inserted the missing top-level module, see
+        -- 'Agda.Syntax.Parser.Parser.figureOutTopLevelModule',
+        -- thus, this case is impossible:
+        _ -> __IMPOSSIBLE__
+
 -- | runs Syntax.Concrete.Definitions.niceDeclarations on main module
 niceDecls :: [C.Declaration] -> ScopeM [NiceDeclaration]
 niceDecls ds = case runNice $ niceDeclarations ds of

test/Fail/Issue1388.agda

@@ -0,0 +1,7 @@
+-- Andreas, 2016-02-01, reported on 2014-12-08
+
+module Issue1388 where
+
+  indented = Set
+
+not-indented = Set  -- This should be a parse error.