git.iko.soy/Idris-dev
on 083fc70 help sign in
Idris-dev/src/Idris/Parser.hs
317 lines 11 kB history raw
1module Idris.Parser where
3import Idris.AbsSyntax
5import Core.CoreParser
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 Data.List
14import Control.Monad.State
15import Debug.Trace
17type TokenParser a = PTok.TokenParser a
19type IParser = GenParser Char IState
21lexer :: TokenParser IState
22lexer = PTok.makeTokenParser idrisDef
24whiteSpace= PTok.whiteSpace lexer
25lexeme = PTok.lexeme lexer
26symbol = PTok.symbol lexer
27natural = PTok.natural lexer
28parens = PTok.parens lexer
29semi = PTok.semi lexer
30comma = PTok.comma lexer
31identifier= PTok.identifier lexer
32reserved = PTok.reserved lexer
33operator = PTok.operator lexer
34reservedOp= PTok.reservedOp lexer
35integer = PTok.integer lexer
36float = PTok.float lexer
37strlit = PTok.stringLiteral lexer
38chlit = PTok.charLiteral lexer
39lchar = lexeme.char
41parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"
43parseProg :: SyntaxInfo -> String -> Idris [PDecl]
44parseProg syn fname
45 = do file <- lift $ readFile fname
46 i <- get
47 case (runParser (do ps <- many1 (pDecl syn)
48 eof
49 i' <- getState
50 return (concat ps, i')) i fname file) of
51 Left err -> fail (show err)
52 Right (x, i) -> do put i
53 return (collect x)
55-- Collect PClauses with the same function name
56collect :: [PDecl] -> [PDecl]
57collect (c@(PClauses _ [PClause n l r w]) : ds) = clauses n [] (c:ds)
58 where clauses n acc (PClauses _ [PClause n' l r w] : ds)
59 | n == n' = clauses n (PClause n' l r (collect w) : acc) ds
60 clauses n acc xs = PClauses n (reverse acc) : collect xs
61collect (PParams ns ps : ds) = PParams ns (collect ps) : (collect ds)
62collect (d : ds) = d : collect ds
63collect [] = []
65pFullExpr :: SyntaxInfo -> IParser PTerm
66pFullExpr syn
67 = do x <- pExpr syn; eof;
68 i <- getState
69 return (addImpl i x)
71pDecl :: SyntaxInfo -> IParser [PDecl]
72pDecl syn
73 = do d <- pDecl' syn
74 i <- getState
75 return [fmap (addImpl i) d]
76 <|> try (pUsing syn)
77 <|> try (pParams syn)
79pFunDecl :: SyntaxInfo -> IParser [PDecl]
80pFunDecl syn
81 = try (do d <- pFunDecl' syn
82 i <- getState
83 return [fmap (addImpl i) d])
85--------- Top Level Declarations ---------
87pDecl' :: SyntaxInfo -> IParser PDecl
88pDecl' syn
89 = try pFixity
90 <|> pFunDecl' syn
91 <|> try (pData syn)
93pFunDecl' :: SyntaxInfo -> IParser PDecl
94pFunDecl' syn = try (do n <- pfName; ty <- pTSig syn
95 lchar ';'
96 ty' <- implicit syn n ty
97 return (PTy n ty'))
98 <|> try (pPattern syn)
100pUsing :: SyntaxInfo -> IParser [PDecl]
101pUsing syn =
102 do reserved "using";
103 lchar '('
104 ns <- tyDeclList syn
105 lchar ')'
106 lchar '{'
107 let uvars = using syn
108 ds <- many1 (pDecl (syn { using = uvars ++ ns }))
109 lchar '}'
110 return (concat ds)
112pParams :: SyntaxInfo -> IParser [PDecl]
113pParams syn =
114 do reserved "params";
115 lchar '('
116 ns <- tyDeclList syn
117 lchar ')'
118 lchar '{'
119 let pvars = syn_params syn
120 ds <- many1 (pDecl syn { syn_params = pvars ++ ns })
121 lchar '}'
122 return [PParams ns (concat ds)]
124--------- Fixity ---------
126pFixity :: IParser PDecl
127pFixity = do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
128 lchar ';'
129 let prec = fromInteger i
130 istate <- getState
131 let fs = map (Fix (f prec)) ops
132 setState (istate {
133 idris_infixes = sort (fs ++ idris_infixes istate) })
134 return (PFix (f prec) ops)
136fixity :: IParser (Int -> Fixity)
137fixity = try (do reserved "infixl"; return Infixl)
138 <|> try (do reserved "infixr"; return Infixr)
139 <|> try (do reserved "infix"; return InfixN)
140 <|> try (do reserved "prefix"; return PrefixN)
142--------- Expressions ---------
144pExpr syn = do i <- getState
145 buildExpressionParser (table (idris_infixes i)) (pExpr' syn)
147pExpr' :: SyntaxInfo -> IParser PTerm
148pExpr' syn
149 = try (pApp syn)
150 <|> pSimpleExpr syn
151 <|> try (pLambda syn)
152 <|> try (pPi syn)
154pfName = try iName
155 <|> do lchar '('; o <- operator; lchar ')'; return (UN [o])
157pSimpleExpr syn =
158 try (do symbol "!["; t <- pTerm; lchar ']'
159 return $ PQuote t)
160 <|> try (do x <- pfName; return (PRef x))
161 <|> try (do lchar '_'; return Placeholder)
162 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)
163 <|> try (do c <- pConstant; return (PConstant c))
164 <|> try (do reserved "Set"; return PSet)
166pHSimpleExpr syn
167 = try (pSimpleExpr syn)
168 <|> do lchar '.'
169 e <- pSimpleExpr syn
170 return $ PHidden e
172pApp syn = do f <- pSimpleExpr syn
173 iargs <- many (pImplicitArg syn)
174 args <- many1 (pSimpleExpr syn)
175 return (PApp f (iargs ++ map PExp args))
177pImplicitArg syn = do lchar '{'; n <- iName
178 v <- option (PRef n) (do lchar '='; pExpr syn)
179 lchar '}'
180 return (PImp n v)
182pTSig syn = do lchar ':'
183 pExpr syn
185pLambda syn = do lchar '\\';
186 xt <- tyOptDeclList syn
187 symbol "=>"
188 sc <- pExpr syn
189 return (bindList PLam xt sc)
191pPi syn = do lchar '('; xt <- tyDeclList syn; lchar ')'
192 symbol "->"
193 sc <- pExpr syn
194 return (bindList (PPi Exp) xt sc)
195 <|> do lchar '{'; xt <- tyDeclList syn; lchar '}'
196 symbol "->"
197 sc <- pExpr syn
198 return (bindList (PPi Imp) xt sc)
200tyDeclList syn = sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))
201 (lchar ',')
203tyOptDeclList syn = sepBy1 (do x <- pfName; t <- option Placeholder (pTSig syn)
204 return (x,t))
205 (lchar ',')
207bindList b [] sc = sc
208bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
210pConstant :: IParser Const
211pConstant = do reserved "Int"; return IType
212 <|> do reserved "Char"; return ChType
213 <|> do reserved "Float"; return FlType
214 <|> do reserved "String"; return StrType
215 <|> do reserved "Ptr"; return PtrType
216 <|> try (do f <- float; return $ Fl f)
217 <|> try (do i <- natural; return $ I (fromInteger i))
219table fixes
220 = [[prefix "-" (\x -> PApp (PRef (UN ["-"])) [PExp (PConstant (I 0)), PExp x])]]
221 ++ toTable (reverse fixes) ++
222 [[binary "=" (\x y -> PApp (PRef (UN ["="])) [PExp x,PExp y]) AssocLeft],
223 [binary "->" (PPi Exp (MN 0 "X")) AssocRight]]
225toTable fs = map (map toBin)
226 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
227 where toBin (Fix (PrefixN _) op) = prefix op
228 (\x -> PApp (PRef (UN [op])) [PExp x])
229 toBin (Fix f op) = binary op
230 (\x y -> PApp (PRef (UN [op])) [PExp x,PExp y]) (assoc f)
231 assoc (Infixl _) = AssocLeft
232 assoc (Infixr _) = AssocRight
233 assoc (InfixN _) = AssocNone
235binary name f assoc = Infix (do { reservedOp name; return f }) assoc
236prefix name f = Prefix (do { reservedOp name; return f })
238--------- Data declarations ---------
240pData :: SyntaxInfo -> IParser PDecl
241pData syn = try (do reserved "data"; tyn <- pfName; ty <- pTSig syn
242 reserved "where"
243 ty' <- implicit syn tyn ty
244 cons <- sepBy1 (pConstructor syn) (lchar '|')
245 lchar ';'
246 return $ PData (PDatadecl tyn ty' cons))
247 <|> do reserved "data"; tyn <- pfName; args <- many iName
248 lchar '='
249 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
250 lchar ';'
251 let conty = mkPApp (PRef tyn) (map PRef args)
252 let ty = bindArgs (map (\a -> PSet) args) PSet
253 ty' <- implicit syn tyn ty
254 cons' <- mapM (\ (x, cargs) -> do let cty = bindArgs cargs conty
255 cty' <- implicit syn x cty
256 return (x, cty')) cons
257 return $ PData (PDatadecl tyn ty' cons')
259mkPApp t [] = t
260mkPApp t xs = PApp t (map PExp xs)
262bindArgs :: [PTerm] -> PTerm -> PTerm
263bindArgs [] t = t
264bindArgs (x:xs) t = PPi Exp (MN 0 "t") x (bindArgs xs t)
266pConstructor :: SyntaxInfo -> IParser (Name, PTerm)
267pConstructor syn
268 = do cn <- pfName; ty <- pTSig syn
269 ty' <- implicit syn cn ty
270 return (cn, ty')
272pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm])
273pSimpleCon syn
274 = do cn <- pfName
275 args <- many (pSimpleExpr syn)
276 return (cn, args)
278--------- Pattern match clauses ---------
280pPattern :: SyntaxInfo -> IParser PDecl
281pPattern syn = do clause <- pClause syn
282 return (PClauses (MN 2 "_") [clause]) -- collect together later
284pClause :: SyntaxInfo -> IParser PClause
285pClause syn
286 = try (do n <- pfName
287 iargs <- many (pImplicitArg syn)
288 args <- many (pHSimpleExpr syn)
289 lchar '='
290 rhs <- pExpr syn
291 wheres <- choice [pWhereblock syn, do lchar ';'; return []]
292 return $ PClause n (PApp (PRef n) (iargs ++ map PExp args)) rhs wheres)
293 <|> do l <- pSimpleExpr syn
294 op <- operator
295 let n = UN [op]
296 r <- pSimpleExpr syn
297 lchar '='
298 rhs <- pExpr syn
299 wheres <- choice [pWhereblock syn, do lchar ';'; return []]
300 return $ PClause n (PApp (PRef n) [PExp l,PExp r]) rhs wheres
302pWhereblock :: SyntaxInfo -> IParser [PDecl]
303pWhereblock syn = do reserved "where"; lchar '{'
304 ds <- many1 $ pFunDecl syn;
305 lchar '}';
306 return $ concat ds
308-- Dealing with implicit arguments
310implicit :: SyntaxInfo -> Name -> PTerm -> IParser PTerm
311implicit syn n ptm
312 = do i <- getState
313 let (tm', impdata) = implicitise syn i ptm
314 setState (i { idris_implicits = addDef n impdata (idris_implicits i) })
315 return tm'