dbc607c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Decorating names for namespaces

dbc607cEdwin Brady15 years ago

src/Core/CoreParser.hs+6−1

compare with master

unifiedsplit

@@ -17,6 +17,7 @@ type TokenParser a = PTok.TokenParser a

17idrisDef = haskellDef {

18 opStart = iOpStart,

19 opLetter = iOpLetter,

20+ identLetter = identLetter haskellDef <|> lchar '.',

20 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],

21 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],

21 reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",

22 reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",

22 "do", "dsl", "import", -- "refl",

23 "do", "dsl", "import", -- "refl",

@@ -59,7 +60,11 @@ pTestFile = do p <- many1 pDef ; eof

59iName :: [String] -> CParser a Name

60iName :: [String] -> CParser a Name

60iName bad = do x <- identifier

61iName bad = do x <- identifier

61 when (x `elem` bad) $ fail "Reserved identifier"

62 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)

64pDef :: CParser a (Name, RDef)

69pDef :: CParser a (Name, RDef)

65pDef = try (do x <- iName []; lchar ':'; ty <- pTerm

70pDef = try (do x <- iName []; lchar ':'; ty <- pTerm

src/Idris/Parser.hs+1−11

@@ -399,6 +399,7 @@ pName = do i <- getState

399 i <- getState

400 UN n <- iName (syntax_keywords i)

401 return (UN ('@':n))

402+

402

403

403pfName = try pName

404pfName = try pName

404 <|> do lchar '('; o <- operator; lchar ')'; return (UN o)

405 <|> do lchar '('; o <- operator; lchar ')'; return (UN o)

@@ -643,13 +644,6 @@ pPattern syn = do clause <- pClause syn

643 fc <- pfc

644 fc <- pfc

644 return (PClauses fc False (MN 2 "_") [clause]) -- collect together later

645 return (PClauses fc False (MN 2 "_") [clause]) -- collect together later

645

646

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−

653pArgExpr syn = let syn' = syn { inPattern = True } in

647pArgExpr syn = let syn' = syn { inPattern = True } in

654 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'

648 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'

655

649

@@ -672,9 +666,6 @@ pClause syn

672 rhs <- pRHS syn n

666 rhs <- pRHS syn n

673 ist <- getState

667 ist <- getState

674 let ctxt = tt_ctxt ist

668 let ctxt = tt_ctxt ist

675− let wsyn = whereSyn n syn (map getTm iargs ++

676− map getTm cargs ++

677− args ++ wargs)

678 (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'

669 (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'

679 return ([], [])]

670 return ([], [])]

680 return $ PClause n (PApp fc (PRef fc n)

671 return $ PClause n (PApp fc (PRef fc n)

@@ -701,7 +692,6 @@ pClause syn

701 fc <- pfc

692 fc <- pfc

702 wargs <- many (pWExpr syn)

693 wargs <- many (pWExpr syn)

703 rhs <- pRHS syn n

694 rhs <- pRHS syn n

704− let wsyn = whereSyn n syn []

705 (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'

695 (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'

706 return ([], [])]

696 return ([], [])]

707 return $ PClause n (PApp fc (PRef fc n) [pexp l,pexp r])

697 return $ PClause n (PApp fc (PRef fc n) [pexp l,pexp r])