@@ -72,10 +72,9 @@ loadSource f = do iLOG ("Reading " ++ f)
7272 file <- lift $ readFile f
7373 (mname, modules, rest, pos) <- parseImports f file
7474 mapM_ loadModule modules
75− ds' <- parseProg (defaultSyntax {syn_namespace = mname }) f rest pos
76− let ds = case mname of
77− [] -> ds'
78− (x:_) -> [PNamespace x ds']
75+ ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
76+ f rest pos
77+ let ds = namespaces mname ds'
7978 logLvl 3 (dumpDecls ds)
8079 i <- getIState
8180 logLvl 10 (show (toAlist (idris_implicits i)))
@@ -84,6 +83,9 @@ loadSource f = do iLOG ("Reading " ++ f)
8483 mapM_ (elabDecl toplevel) ds
8584 iLOG ("Finished " ++ f)
8685 return ()
86+ where
87+ namespaces [] ds = ds
88+ namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
8789
8890parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"
8991parseTac i = runParser (do t <- pTactic defaultSyntax
@@ -107,8 +109,11 @@ parseImports fname input
107109
108110pHeader :: IParser [String]
109111pHeader = try (do reserved "module"; i <- identifier; lchar ';'
110− return [i])
112+ return (parseName i))
111113 <|> return []
114+ where parseName x = case span (/='.') x of
115+ (x, "") -> [x]
116+ (x, '.':y) -> x : parseName y
112117
113118
114119pfc :: IParser FC
@@ -123,7 +128,9 @@ pImport :: IParser String
123128pImport = do reserved "import"
124129 f <- identifier
125130 lchar ';'
126− return f
131+ return (map dot f)
132+ where dot '.' = '/'
133+ dot c = c
127134
128135parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl]
129136parseProg syn fname input pos