git.iko.soy/Idris-dev
on 8e94d86 help sign in
Idris-dev/src/Core/CoreParser.hs
201 lines 7.1 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName,
4 idrisLexer, maybeWithNS) 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
126pDef :: CParser a (Name, RDef)
127pDef = try (do x <- iName []; lchar ':'; ty <- pTerm
128 lchar '='
129 tm <- pTerm
130 lchar ';'
131 return (x, RFunction (RawFun ty tm)))
132 <|> do x <- iName []; lchar ':'; ty <- pTerm; lchar ';'
133 return (x, RConst ty)
134 <|> do (x, d) <- pData; lchar ';'
135 return (x, RData d)
137app :: CParser a (Raw -> Raw -> Raw)
138app = do whiteSpace ; return RApp
140arrow :: CParser a (Raw -> Raw -> Raw)
141arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
143pTerm :: CParser a Raw
144pTerm = try (do chainl1 pNoApp app)
145 <|> pNoApp
147pNoApp :: CParser a Raw
148pNoApp = try (chainr1 pExp arrow)
149 <|> pExp
150pExp :: CParser a Raw
151pExp = do lchar '\\'; x <- iName []; lchar ':'; ty <- pTerm
152 symbol "=>";
153 sc <- pTerm
154 return (RBind x (Lam ty) sc)
155 <|> try (do lchar '?'; x <- iName []; lchar ':'; ty <- pTerm
156 lchar '.';
157 sc <- pTerm
158 return (RBind x (Hole ty) sc))
159 <|> try (do lchar '(';
160 x <- iName []; lchar ':'; ty <- pTerm
161 lchar ')';
162 symbol "->";
163 sc <- pTerm
164 return (RBind x (Pi ty) sc))
165 <|> try (do lchar '(';
166 t <- pTerm
167 lchar ')'
168 return t)
169 <|> try (do symbol "??";
170 x <- iName []; lchar ':'; ty <- pTerm
171 lchar '=';
172 val <- pTerm
173 sc <- pTerm
174 return (RBind x (Guess ty val) sc))
175 <|> try (do reserved "let";
176 x <- iName []; lchar ':'; ty <- pTerm
177 lchar '=';
178 val <- pTerm
179 reserved "in";
180 sc <- pTerm
181 return (RBind x (Let ty val) sc))
182 <|> try (do lchar '_';
183 x <- iName []; lchar ':'; ty <- pTerm
184 lchar '.';
185 sc <- pTerm
186 return (RBind x (PVar ty) sc))
187 <|> try (do reserved "Set"
188 return RSet)
189 <|> try (do x <- iName []
190 return (Var x))
192pData :: CParser a (Name, RawDatatype)
193pData = do reserved "data"; x <- iName []; lchar ':'; ty <- pTerm; reserved "where"
194 cs <- many pConstructor
195 return (x, RDatatype x ty cs)
197pConstructor :: CParser a (Name, Raw)
198pConstructor = do lchar '|'
199 c <- iName []; lchar ':'; ty <- pTerm
200 return (c, ty)