git.iko.soy/Idris-dev
on 8464bc4 help sign in
Idris-dev/src/Core/CoreParser.hs
210 lines 7.3 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName,
4 idrisLexer, maybeWithNS, pDocComment) where
6import Core.TT
8import Text.ParserCombinators.Parsec
9import Text.ParserCombinators.Parsec.Expr
10import Text.ParserCombinators.Parsec.Language
11import qualified Text.ParserCombinators.Parsec.Token as PTok
13import Control.Monad.State
14import Data.Char
15import Debug.Trace
17type TokenParser a = PTok.TokenParser a
19idrisDef = haskellDef {
20 opStart = iOpStart,
21 opLetter = iOpLetter,
22 identLetter = identLetter haskellDef <|> lchar '.',
23 reservedOpNames
24 = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],
25 reservedNames
26 = ["let", "in", "data", "codata", "record", "Set",
27 "do", "dsl", "import", "impossible",
28 "case", "of", "total", "partial", "mutual",
29 "infix", "infixl", "infixr",
30 "where", "with", "syntax", "proof", "postulate",
31 "using", "namespace", "class", "instance",
32 "public", "private", "abstract",
33 "Int", "Integer", "Float", "Char", "String", "Ptr"]
34 }
36iOpStart = oneOf ":!#$%&*+./<=>?@\\^|-~"
37iOpLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
38-- <|> letter
40idrisLexer :: TokenParser a
41idrisLexer = (PTok.makeTokenParser idrisDef) { PTok.whiteSpace = lexWS }
43lexer = idrisLexer
45-- Taken from Parsec source code
46lexWS = skipMany (simpleSpace <|> oneLineComment <|> multiLineComment <?> "")
47 where
49 simpleSpace = skipMany1 (satisfy isSpace)
50 oneLineComment = do try (string ("--"))
51 satisfy (/= '|')
52 skipMany (satisfy (/= '\n'))
53 return ()
54 multiLineComment = do try (string "{-")
55 satisfy (/= '|')
56 inCommentMulti
58 inCommentMulti
59 = do{ try (string "-}") ; return () }
60 <|> do{ multiLineComment ; inCommentMulti }
61 <|> do{ skipMany1 (noneOf startEnd) ; inCommentMulti }
62 <|> do{ oneOf startEnd ; inCommentMulti }
63 <?> "end of comment"
64 where
65 startEnd = "-}{"
67whiteSpace= PTok.whiteSpace lexer
68lexeme = PTok.lexeme lexer
69symbol = PTok.symbol lexer
70natural = PTok.natural lexer
71parens = PTok.parens lexer
72semi = PTok.semi lexer
73comma = PTok.comma lexer
74identifier= PTok.identifier lexer
75reserved = PTok.reserved lexer
76operator = PTok.operator lexer
77reservedOp= PTok.reservedOp lexer
78lchar = lexeme.char
80type CParser a = GenParser Char a
82parseFile = runParser pTestFile () "(input)"
83parseDef = runParser pDef () "(input)"
84parseTerm = runParser pTerm () "(input)"
86pTestFile :: CParser a RProgram
87pTestFile = do p <- many1 pDef ; eof
88 return p
90iName :: [String] -> CParser a Name
91iName bad = maybeWithNS identifier False bad
93-- Enhances a given parser to accept an optional namespace. All possible
94-- namespace prefixes are tried in ascending / descending order, and
95-- identifiers of a given list fail.
96maybeWithNS :: CParser a String -> Bool -> [String] -> CParser a Name
97maybeWithNS parser ascend bad = do
98 i <- option "" (lookAhead identifier)
99 when (i `elem` bad) $ fail "Reserved identifier"
100 let transf = if ascend then id else reverse
101 (x, xs) <- choice $ transf (parserNoNS : parsersNS i)
102 return $ mkName (x, xs)
103 where
104 parserNoNS = do x <- parser; return (x, "")
105 parserNS ns = do xs <- string ns; lchar '.'; x <- parser; return (x, xs)
106 parsersNS i = [try (parserNS ns) | ns <- (initsEndAt (=='.') i)]
108-- List of all initial segments in ascending order of a list. Every such
109-- initial segment ends right before an element satisfying the given
110-- condition.
111initsEndAt :: (a -> Bool) -> [a] -> [[a]]
112initsEndAt p [] = []
113initsEndAt p (x:xs) | p x = [] : x_inits_xs
114 | otherwise = x_inits_xs
115 where x_inits_xs = [x : cs | cs <- initsEndAt p xs]
117-- Create a `Name' from a pair of strings representing a base name and its
118-- namespace.
119mkName :: (String, String) -> Name
120mkName (n, "") = UN n
121mkName (n, ns) = NS (UN n) (reverse (parseNS ns))
122 where parseNS x = case span (/= '.') x of
123 (x, "") -> [x]
124 (x, '.':y) -> x : parseNS y
126pDocComment :: Char -> CParser a String
127pDocComment c
128 = do string "--"
129 char c
130 i <- getInput
131 let (doc, rest) = span (/='\n') i
132 setInput rest
133 return doc
135pDef :: CParser a (Name, RDef)
136pDef = try (do x <- iName []; lchar ':'; ty <- pTerm
137 lchar '='
138 tm <- pTerm
139 lchar ';'
140 return (x, RFunction (RawFun ty tm)))
141 <|> do x <- iName []; lchar ':'; ty <- pTerm; lchar ';'
142 return (x, RConst ty)
143 <|> do (x, d) <- pData; lchar ';'
144 return (x, RData d)
146app :: CParser a (Raw -> Raw -> Raw)
147app = do whiteSpace ; return RApp
149arrow :: CParser a (Raw -> Raw -> Raw)
150arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
152pTerm :: CParser a Raw
153pTerm = try (do chainl1 pNoApp app)
154 <|> pNoApp
156pNoApp :: CParser a Raw
157pNoApp = try (chainr1 pExp arrow)
158 <|> pExp
159pExp :: CParser a Raw
160pExp = do lchar '\\'; x <- iName []; lchar ':'; ty <- pTerm
161 symbol "=>";
162 sc <- pTerm
163 return (RBind x (Lam ty) sc)
164 <|> try (do lchar '?'; x <- iName []; lchar ':'; ty <- pTerm
165 lchar '.';
166 sc <- pTerm
167 return (RBind x (Hole ty) sc))
168 <|> try (do lchar '(';
169 x <- iName []; lchar ':'; ty <- pTerm
170 lchar ')';
171 symbol "->";
172 sc <- pTerm
173 return (RBind x (Pi ty) sc))
174 <|> try (do lchar '(';
175 t <- pTerm
176 lchar ')'
177 return t)
178 <|> try (do symbol "??";
179 x <- iName []; lchar ':'; ty <- pTerm
180 lchar '=';
181 val <- pTerm
182 sc <- pTerm
183 return (RBind x (Guess ty val) sc))
184 <|> try (do reserved "let";
185 x <- iName []; lchar ':'; ty <- pTerm
186 lchar '=';
187 val <- pTerm
188 reserved "in";
189 sc <- pTerm
190 return (RBind x (Let ty val) sc))
191 <|> try (do lchar '_';
192 x <- iName []; lchar ':'; ty <- pTerm
193 lchar '.';
194 sc <- pTerm
195 return (RBind x (PVar ty) sc))
196 <|> try (do reserved "Set"
197 return RSet)
198 <|> try (do x <- iName []
199 return (Var x))
201pData :: CParser a (Name, RawDatatype)
202pData = do reserved "data"; x <- iName []; lchar ':'; ty <- pTerm; reserved "where"
203 cs <- many pConstructor
204 return (x, RDatatype x ty cs)
206pConstructor :: CParser a (Name, Raw)
207pConstructor = do lchar '|'
208 c <- iName []; lchar ':'; ty <- pTerm
209 return (c, ty)