git.iko.soy/Idris-dev
on dbc607c help sign in
Idris-dev/src/Core/CoreParser.hs
144 lines 4.9 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName, idrisDef) where
5import Core.TT
7import Text.ParserCombinators.Parsec
8import Text.ParserCombinators.Parsec.Expr
9import Text.ParserCombinators.Parsec.Language
10import qualified Text.ParserCombinators.Parsec.Token as PTok
12import Control.Monad.State
13import Debug.Trace
15type TokenParser a = PTok.TokenParser a
17idrisDef = haskellDef {
18 opStart = iOpStart,
19 opLetter = iOpLetter,
20 identLetter = identLetter haskellDef <|> lchar '.',
21 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],
22 reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",
23 "do", "dsl", "import", -- "refl",
24 "infix", "infixl", "infixr", "prefix",
25 "where", "with", "forall", "syntax", "proof",
26 "using", "params", "namespace", "class", "instance",
27 "Int", "Integer", "Float", "Char", "String", "Ptr"]
28 }
30iOpStart = oneOf ":!#$%&*+./<=>?@\\^|-~"
31iOpLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
32-- <|> letter
34lexer :: TokenParser a
35lexer = PTok.makeTokenParser idrisDef
37whiteSpace= PTok.whiteSpace lexer
38lexeme = PTok.lexeme lexer
39symbol = PTok.symbol lexer
40natural = PTok.natural lexer
41parens = PTok.parens lexer
42semi = PTok.semi lexer
43comma = PTok.comma lexer
44identifier= PTok.identifier lexer
45reserved = PTok.reserved lexer
46operator = PTok.operator lexer
47reservedOp= PTok.reservedOp lexer
48lchar = lexeme.char
50type CParser a = GenParser Char a
52parseFile = runParser pTestFile () "(input)"
53parseDef = runParser pDef () "(input)"
54parseTerm = runParser pTerm () "(input)"
56pTestFile :: CParser a RProgram
57pTestFile = do p <- many1 pDef ; eof
58 return p
60iName :: [String] -> CParser a Name
61iName bad = do x <- identifier
62 when (x `elem` bad) $ fail "Reserved identifier"
63 return (parseName x)
64 where
65 parseName x = case span (/= '.') x of
66 (x, "") -> UN x
67 (x, '.':y) -> NS x (parseName y)
69pDef :: CParser a (Name, RDef)
70pDef = try (do x <- iName []; lchar ':'; ty <- pTerm
71 lchar '='
72 tm <- pTerm
73 lchar ';'
74 return (x, RFunction (RawFun ty tm)))
75 <|> do x <- iName []; lchar ':'; ty <- pTerm; lchar ';'
76 return (x, RConst ty)
77 <|> do (x, d) <- pData; lchar ';'
78 return (x, RData d)
80app :: CParser a (Raw -> Raw -> Raw)
81app = do whiteSpace ; return RApp
83arrow :: CParser a (Raw -> Raw -> Raw)
84arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
86pTerm :: CParser a Raw
87pTerm = try (do chainl1 pNoApp app)
88 <|> pNoApp
90pNoApp :: CParser a Raw
91pNoApp = try (chainr1 pExp arrow)
92 <|> pExp
93pExp :: CParser a Raw
94pExp = do lchar '\\'; x <- iName []; lchar ':'; ty <- pTerm
95 symbol "=>";
96 sc <- pTerm
97 return (RBind x (Lam ty) sc)
98 <|> try (do lchar '?'; x <- iName []; lchar ':'; ty <- pTerm
99 lchar '.';
100 sc <- pTerm
101 return (RBind x (Hole ty) sc))
102 <|> try (do lchar '(';
103 x <- iName []; lchar ':'; ty <- pTerm
104 lchar ')';
105 symbol "->";
106 sc <- pTerm
107 return (RBind x (Pi ty) sc))
108 <|> try (do lchar '(';
109 t <- pTerm
110 lchar ')'
111 return t)
112 <|> try (do symbol "??";
113 x <- iName []; lchar ':'; ty <- pTerm
114 lchar '=';
115 val <- pTerm
116 sc <- pTerm
117 return (RBind x (Guess ty val) sc))
118 <|> try (do reserved "let";
119 x <- iName []; lchar ':'; ty <- pTerm
120 lchar '=';
121 val <- pTerm
122 reserved "in";
123 sc <- pTerm
124 return (RBind x (Let ty val) sc))
125 <|> try (do lchar '_';
126 x <- iName []; lchar ':'; ty <- pTerm
127 lchar '.';
128 sc <- pTerm
129 return (RBind x (PVar ty) sc))
130 <|> try (do reserved "Set"; i <- option 0 natural
131 return (RSet (fromInteger i)))
132 <|> try (do x <- iName []
133 return (Var x))
135pData :: CParser a (Name, RawDatatype)
136pData = do reserved "data"; x <- iName []; lchar ':'; ty <- pTerm; reserved "where"
137 cs <- many pConstructor
138 return (x, RDatatype x ty cs)
140pConstructor :: CParser a (Name, Raw)
141pConstructor = do lchar '|'
142 c <- iName []; lchar ':'; ty <- pTerm
143 return (c, ty)