git.iko.soy/Idris-dev
on master help sign in
Namespace parsing improvements (for qualified operator names)
517acc1Edwin Brady
src/Core/CoreParser.hs+35−9
compare with master
unifiedsplit
@@ -1,6 +1,7 @@
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
2
2
3−module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName, idrisDef) where
3+module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName, idrisDef,
4+ maybeWithNS) where
4
5
5import Core.TT
6import Core.TT
6
7
@@ -60,15 +61,40 @@ pTestFile = do p <- many1 pDef ; eof
60 return p
61 return p
61
62
62iName :: [String] -> CParser a Name
63iName :: [String] -> CParser a Name
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
63−iName bad = do x <- identifier
71+ i <- option "" (lookAhead identifier)
64− when (x `elem` bad) $ fail "Reserved identifier"
72+ when (i `elem` bad) $ fail "Reserved identifier"
65− return $ mkNS (reverse (parseName x))
73+ let transf = if ascend then id else reverse
74+ (x, xs) <- choice $ transf (parserNoNS : parsersNS i)
75+ return $ mkName (x, xs)
66 where
76 where
67− mkNS [x] = UN x
77+ parserNoNS = do x <- parser; return (x, "")
68− mkNS (x:xs) = NS (UN x) xs
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))
69− parseName x = case span (/= '.') x of
95+ where parseNS x = case span (/= '.') x of
70− (x, "") -> [x]
96+ (x, "") -> [x]
71− (x, '.':y) -> x : parseName y
97+ (x, '.':y) -> x : parseNS y
72
98
73pDef :: CParser a (Name, RDef)
99pDef :: CParser a (Name, RDef)
74pDef = try (do x <- iName []; lchar ':'; ty <- pTerm
100pDef = try (do x <- iName []; lchar ':'; ty <- pTerm
src/IRTS/Defunctionalise.hsnew file+20
@@ -0,0 +1,20 @@
1+module IRTS.Defunctionalise where
2+
3+import IRTS.Lang
4+import Core.TT
5+
6+defunctionalise :: [(Name, LDecl)] -> [(Name, LDecl)]
7+defunctionalise defs = defs -- TODO!
8+
9+-- To defunctionalise:
10+--
11+-- 1 Create a data constructor for each function
12+-- 2 Create a data constructor for each underapplication of a function
13+-- 3 Convert underapplications to their corresponding constructors
14+-- 4 Create an EVAL function which calls the appropriate function for data constructors
15+-- created as part of step 1
16+-- 5 Create an APPLY function which adds an argument to each underapplication (or calls
17+-- APPLY again for an exact application)
18+-- 6 Wrap overapplications in chains of APPLY
19+
20+
src/Idris/Parser.hs+7−3
@@ -613,10 +613,14 @@ pName = do i <- getState
613 i <- getState
613 i <- getState
614 UN n <- iName (syntax_keywords i)
614 UN n <- iName (syntax_keywords i)
615 return (UN ('@':n))
615 return (UN ('@':n))
616−
617
616
618−pfName = try pName
617+-- Parser for an operator in function position, i.e. enclosed by `()', with an
618+-- optional namespace.
619+pOpFront = maybeWithNS pOpFrontNoNS False []
619− <|> do lchar '('; o <- operator; lchar ')'; return (UN o)
620+ where pOpFrontNoNS = do lchar '('; o <- operator; lchar ')'; return o
621+
622+pfName = try pOpFront
623+ <|> pName
620
624
621pAccessibility' :: IParser Accessibility
625pAccessibility' :: IParser Accessibility
622pAccessibility'
626pAccessibility'