@@ -1,6 +1,7 @@
11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
22
3−module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName, idrisDef) where
3+module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName, idrisDef,
4+ maybeWithNS) where
45
56import Core.TT
67
@@ -60,15 +61,40 @@ pTestFile = do p <- many1 pDef ; eof
6061 return p
6162
6263iName :: [String] -> CParser a Name
63−iName bad = do x <- identifier
64− when (x `elem` bad) $ fail "Reserved identifier"
65− return $ mkNS (reverse (parseName x))
64+iName bad = maybeWithNS identifier False bad
65+
66+-- Enhances a given parser to accept an optional namespace. All possible
67+-- namespace prefixes are tried in ascending / descending order, and
68+-- identifiers of a given list fail.
69+maybeWithNS :: CParser a String -> Bool -> [String] -> CParser a Name
70+maybeWithNS parser ascend bad = do
71+ i <- option "" (lookAhead identifier)
72+ when (i `elem` bad) $ fail "Reserved identifier"
73+ let transf = if ascend then id else reverse
74+ (x, xs) <- choice $ transf (parserNoNS : parsersNS i)
75+ return $ mkName (x, xs)
6676 where
67− mkNS [x] = UN x
68− mkNS (x:xs) = NS (UN x) xs
69− parseName x = case span (/= '.') x of
70− (x, "") -> [x]
71− (x, '.':y) -> x : parseName y
77+ parserNoNS = do x <- parser; return (x, "")
78+ parserNS ns = do xs <- string ns; lchar '.'; x <- parser; return (x, xs)
79+ parsersNS i = [try (parserNS ns) | ns <- (initsEndAt (=='.') i)]
80+
81+-- List of all initial segments in ascending order of a list. Every such
82+-- initial segment ends right before an element satisfying the given
83+-- condition.
84+initsEndAt :: (a -> Bool) -> [a] -> [[a]]
85+initsEndAt p [] = []
86+initsEndAt p (x:xs) | p x = [] : x_inits_xs
87+ | otherwise = x_inits_xs
88+ where x_inits_xs = [x : cs | cs <- initsEndAt p xs]
89+
90+-- Create a `Name' from a pair of strings representing a base name and its
91+-- namespace.
92+mkName :: (String, String) -> Name
93+mkName (n, "") = UN n
94+mkName (n, ns) = NS (UN n) (reverse (parseNS ns))
95+ where parseNS x = case span (/= '.') x of
96+ (x, "") -> [x]
97+ (x, '.':y) -> x : parseNS y
7298
7399pDef :: CParser a (Name, RDef)
74100pDef = try (do x <- iName []; lchar ':'; ty <- pTerm