git.iko.soy/Idris-dev
on master help sign in
Decorating names for namespaces
commitdbc607cc9365e1ca2db4304473c1089d67e1fcd8 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 18 Nov 2011, 13:56 (15 years ago) parente473c2e
2 files changed+7−12
compare with master
unifiedsplit
src/Core/CoreParser.hs+6−1 src/Idris/Parser.hs+1−11
src/Core/CoreParser.hs+6−1
@@ -17,6 +17,7 @@ type TokenParser a = PTok.TokenParser a
1717idrisDef = haskellDef {
1818 opStart = iOpStart,
1919 opLetter = iOpLetter,
20+ identLetter = identLetter haskellDef <|> lchar '.',
2021 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],
2122 reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",
2223 "do", "dsl", "import", -- "refl",
@@ -59,7 +60,11 @@ pTestFile = do p <- many1 pDef ; eof
5960iName :: [String] -> CParser a Name
6061iName bad = do x <- identifier
6162 when (x `elem` bad) $ fail "Reserved identifier"
62− return (UN x)
63+ return (parseName x)
64+ where
65+ parseName x = case span (/= '.') x of
66+ (x, "") -> UN x
67+ (x, '.':y) -> NS x (parseName y)
6368
6469pDef :: CParser a (Name, RDef)
6570pDef = try (do x <- iName []; lchar ':'; ty <- pTerm
src/Idris/Parser.hs+1−11
@@ -399,6 +399,7 @@ pName = do i <- getState
399399 i <- getState
400400 UN n <- iName (syntax_keywords i)
401401 return (UN ('@':n))
402+
402403
403404pfName = try pName
404405 <|> do lchar '('; o <- operator; lchar ')'; return (UN o)
@@ -643,13 +644,6 @@ pPattern syn = do clause <- pClause syn
643644 fc <- pfc
644645 return (PClauses fc False (MN 2 "_") [clause]) -- collect together later
645646
646−whereSyn :: Name -> SyntaxInfo -> [PTerm] -> SyntaxInfo
647−whereSyn n syn args = let ns = concatMap allNamesIn args
648− ni = no_imp syn in
649− syn { decoration = \x -> decorate n (decoration syn x),
650− no_imp = nub (ni ++ ns) }
651− where decorate n x = UN (show n ++ "_" ++ show x)
652−
653647pArgExpr syn = let syn' = syn { inPattern = True } in
654648 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
655649
@@ -672,9 +666,6 @@ pClause syn
672666 rhs <- pRHS syn n
673667 ist <- getState
674668 let ctxt = tt_ctxt ist
675− let wsyn = whereSyn n syn (map getTm iargs ++
676− map getTm cargs ++
677− args ++ wargs)
678669 (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'
679670 return ([], [])]
680671 return $ PClause n (PApp fc (PRef fc n)
@@ -701,7 +692,6 @@ pClause syn
701692 fc <- pfc
702693 wargs <- many (pWExpr syn)
703694 rhs <- pRHS syn n
704− let wsyn = whereSyn n syn []
705695 (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'
706696 return ([], [])]
707697 return $ PClause n (PApp fc (PRef fc n) [pexp l,pexp r])