git.iko.soy/Idris-dev
on fb3160e help sign in
Idris-dev/src/Idris/Parser.hs
1244 lines 49 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.Parser where
5import Idris.AbsSyntax
6import Idris.DSL
7import Idris.Imports
8import Idris.Error
9import Idris.ElabDecls
10import Idris.ElabTerm
11import Idris.IBC
12import Idris.Unlit
13import Paths_idris
15import Core.CoreParser
16import Core.TT
17import Core.Evaluate
19import Text.ParserCombinators.Parsec
20import Text.ParserCombinators.Parsec.Error
21import Text.ParserCombinators.Parsec.Expr
22import Text.ParserCombinators.Parsec.Language
23import qualified Text.ParserCombinators.Parsec.Token as PTok
25import Data.List
26import Control.Monad.State
27import Debug.Trace
28import Data.Maybe
29import System.FilePath
31type TokenParser a = PTok.TokenParser a
33type IParser = GenParser Char IState
35lexer :: TokenParser IState
36lexer = PTok.makeTokenParser idrisDef
38whiteSpace= PTok.whiteSpace lexer
39lexeme = PTok.lexeme lexer
40symbol = PTok.symbol lexer
41natural = PTok.natural lexer
42parens = PTok.parens lexer
43semi = PTok.semi lexer
44comma = PTok.comma lexer
45identifier= PTok.identifier lexer
46reserved = PTok.reserved lexer
47operator = PTok.operator lexer
48reservedOp= PTok.reservedOp lexer
49integer = PTok.integer lexer
50float = PTok.float lexer
51strlit = PTok.stringLiteral lexer
52chlit = PTok.charLiteral lexer
53lchar = lexeme.char
55-- Loading modules
57loadModule :: FilePath -> Idris String
58loadModule f
59 = idrisCatch (do datadir <- liftIO $ getDataDir
60 fp <- liftIO $ findImport [".", datadir] f
61 i <- getIState
62 if (f `elem` imported i)
63 then iLOG $ "Already read " ++ f
64 else do putIState (i { imported = f : imported i })
65 case fp of
66 IDR fn -> loadSource False fn
67 LIDR fn -> loadSource True fn
68 IBC fn src ->
69 idrisCatch (loadIBC fn)
70 (\c -> do iLOG $ fn ++ " failed " ++ show c
71 case src of
72 IDR sfn -> loadSource False sfn
73 LIDR sfn -> loadSource True sfn)
74 let (dir, fh) = splitFileName f
75 return (dropExtension fh))
76 (\e -> do let msg = show e
77 setErrLine (getErrLine msg)
78 iputStrLn msg
79 return "")
81loadSource :: Bool -> FilePath -> Idris ()
82loadSource lidr f
83 = do iLOG ("Reading " ++ f)
84 file_in <- liftIO $ readFile f
85 file <- if lidr then tclift $ unlit f file_in else return file_in
86 (mname, modules, rest, pos) <- parseImports f file
87 i <- getIState
88 putIState (i { default_access = Hidden })
89 mapM_ loadModule modules
90 clearIBC -- start a new .ibc file
91 mapM_ (\m -> addIBC (IBCImport m)) modules
92 ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
93 f rest pos
94 let ds = namespaces mname ds'
95 logLvl 3 (dumpDecls ds)
96 i <- getIState
97 logLvl 10 (show (toAlist (idris_implicits i)))
98 logLvl 3 (show (idris_infixes i))
99 -- Now add all the declarations to the context
100 v <- verbose
101 when v $ iputStrLn $ "Type checking " ++ f
102 mapM_ (elabDecl toplevel) ds
103 iLOG ("Finished " ++ f)
104 let ibc = dropExtension f ++ ".ibc"
105 iucheck
106 i <- getIState
107 addHides (hide_list i)
108 ok <- noErrors
109 when ok $
110 idrisCatch (do writeIBC f ibc; clearIBC)
111 (\c -> return ()) -- failure is harmless
112 putIState (i { hide_list = [] })
113 return ()
114 where
115 namespaces [] ds = ds
116 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
118addHides :: [(Name, Maybe Accessibility)] -> Idris ()
119addHides xs = do i <- getIState
120 let defh = default_access i
121 let (hs, as) = partition isNothing xs
122 if null as then return ()
123 else mapM_ doHide
124 (map (\ (n, _) -> (n, defh)) hs ++
125 map (\ (n, Just a) -> (n, a)) as)
126 where isNothing (_, Nothing) = True
127 isNothing _ = False
129 doHide (n, a) = do setAccessibility n a
130 addIBC (IBCAccess n a)
132parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"
133parseTac i = runParser (do t <- pTactic defaultSyntax
134 eof
135 return t) i "(proof)"
137parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)
138parseImports fname input
139 = do i <- get
140 case (runParser (do mname <- pHeader
141 ps <- many pImport
142 rest <- getInput
143 pos <- getPosition
144 return ((mname, ps, rest, pos), i)) i fname input) of
145 Left err -> fail (ishow err)
146 Right (x, i) -> do put i
147 return x
148 where ishow err = let ln = sourceLine (errorPos err) in
149 fname ++ ":" ++ show ln ++ ":parse error"
150-- show (map messageString (errorMessages err))
152pHeader :: IParser [String]
153pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')
154 return (parseName i))
155 <|> return []
156 where parseName x = case span (/='.') x of
157 (x, "") -> [x]
158 (x, '.':y) -> x : parseName y
160push_indent :: IParser ()
161push_indent = do pos <- getPosition
162 ist <- getState
163 setState (ist { indent_stack = sourceColumn pos :
164 indent_stack ist })
166last_indent :: IParser Int
167last_indent = do ist <- getState
168 case indent_stack ist of
169 (x : xs) -> return x
170 _ -> return 1
172indent :: IParser Int
173indent = do pos <- getPosition
174 return (sourceColumn pos)
176pop_indent :: IParser ()
177pop_indent = do ist <- getState
178 let (x : xs) = indent_stack ist
179 setState (ist { indent_stack = xs })
181open_block :: IParser ()
182open_block = do lchar '{'
183 ist <- getState
184 setState (ist { brace_stack = Nothing : brace_stack ist })
185 <|> do ist <- getState
186 lvl <- indent
187 setState (ist { brace_stack = Just lvl : brace_stack ist })
189close_block :: IParser ()
190close_block = do ist <- getState
191 bs <- case brace_stack ist of
192 Nothing : xs -> do lchar '}'
193 return xs
194 Just lvl : xs -> do i <- indent
195 inp <- getInput
196-- trace (show (take 10 inp, i, lvl)) $
197 if (i >= lvl && take 1 inp /= ")")
198 then fail "Not end of block"
199 else return xs
200 setState (ist { brace_stack = bs })
202pTerminator = do lchar ';'; pop_indent
203 <|> do c <- indent; l <- last_indent
204 if (c <= l) then pop_indent
205 else fail "Not a terminator"
206 <|> do i <- getInput; if (take 1 i == "}" || take 1 i == ")") then pop_indent
207 else fail "Not a terminator"
208 <|> lookAhead eof
210pBarTerminator
211 = do lchar '|'; return ()
212 <|> do c <- indent; l <- last_indent
213 if (c <= l) then return ()
214 else fail "Not a terminator"
215 <|> lookAhead eof
217pKeepTerminator
218 = do lchar ';'; return ()
219 <|> do c <- indent; l <- last_indent
220 if (c <= l) then return ()
221 else fail "Not a terminator"
222 <|> do i <- getInput; let h = take 1 i
223 if (h == "}" || h == ")" || h == "|") then return ()
224 else fail "Not a terminator"
225 <|> lookAhead eof
227notEndApp = do c <- indent; l <- last_indent
228 i <- getInput
229 if (c <= l) then fail "Terminator"
230 else return ()
232notEndBlock = do ist <- getState
233 case brace_stack ist of
234 Just lvl : xs -> do i <- indent
235 inp <- getInput
236 if (i < lvl || take 1 inp == ")")
237 then fail "End of block"
238 else return ()
239 _ -> return ()
241pfc :: IParser FC
242pfc = do s <- getPosition
243 let (dir, file) = splitFileName (sourceName s)
244 let f = case dir of
245 "./" -> file
246 _ -> sourceName s
247 return $ FC f (sourceLine s)
249pImport :: IParser String
250pImport = do reserved "import"
251 f <- identifier
252 option ';' (lchar ';')
253 return (map dot f)
254 where dot '.' = '/'
255 dot c = c
257parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl]
258parseProg syn fname input pos
259 = do i <- get
260 case (runParser (do setPosition pos
261 whiteSpace
262 ps <- many (pDecl syn)
263 eof
264 i' <- getState
265 return (concat ps, i')) i fname input) of
266 Left err -> fail (ishow err)
267 Right (x, i) -> do put i
268 return (collect x)
269 where ishow err = let ln = sourceLine (errorPos err) in
270 fname ++ ":" ++ show ln ++ ":parse error"
271 ++ " at column " ++ show (sourceColumn (errorPos err))
272-- show (map messageString (errorMessages err))
274-- Collect PClauses with the same function name
276collect :: [PDecl] -> [PDecl]
277collect (c@(PClauses _ o _ _) : ds)
278 = clauses (cname c) [] (c : ds)
279 where clauses n acc (PClauses fc _ _ [PClause n' l ws r w] : ds)
280 | n == n' = clauses n (PClause n' l ws r (collect w) : acc) ds
281 clauses n acc (PClauses fc _ _ [PWith n' l ws r w] : ds)
282 | n == n' = clauses n (PWith n' l ws r (collect w) : acc) ds
283 clauses n acc xs = PClauses (getfc c) o n (reverse acc) : collect xs
285 cname (PClauses fc _ _ [PClause n _ _ _ _]) = n
286 cname (PClauses fc _ _ [PWith n _ _ _ _]) = n
287 getfc (PClauses fc _ _ _) = fc
289collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
290collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds
291collect (PClass f s cs n ps ds : ds') = PClass f s cs n ps (collect ds) : collect ds'
292collect (PInstance f s cs n ps t ds : ds')
293 = PInstance f s cs n ps t (collect ds) : collect ds'
294collect (d : ds) = d : collect ds
295collect [] = []
297pFullExpr :: SyntaxInfo -> IParser PTerm
298pFullExpr syn
299 = do x <- pExpr syn; eof;
300 i <- getState
301 return $ desugar syn i x
303pDecl :: SyntaxInfo -> IParser [PDecl]
304pDecl syn = do notEndBlock
305 pDeclBody where
306 pDeclBody
307 = do d <- pDecl' syn
308 i <- getState
309 let d' = fmap (desugar syn i) d
310 return [d']
311 <|> pUsing syn
312 <|> pParams syn
313 <|> pNamespace syn
314 <|> pClass syn
315 <|> pInstance syn
316 <|> do d <- pDSL syn; return [d]
317 <|> pDirective
318 <|> try (do reserved "import"
319 fp <- identifier
320 fail "imports must be at the top of file")
322pFunDecl :: SyntaxInfo -> IParser [PDecl]
323pFunDecl syn
324 = try (do notEndBlock
325 d <- pFunDecl' syn
326 i <- getState
327 let d' = fmap (desugar syn i) d
328 return [d'])
330--------- Top Level Declarations ---------
332pDecl' :: SyntaxInfo -> IParser PDecl
333pDecl' syn
334 = try pFixity
335 <|> pFunDecl' syn
336 <|> try (pData syn)
337 <|> try (pRecord syn)
338 <|> pSyntaxDecl syn
340pSyntaxDecl :: SyntaxInfo -> IParser PDecl
341pSyntaxDecl syn
342 = do s <- pSyntaxRule syn
343 i <- getState
344 let rs = syntax_rules i
345 let ns = syntax_keywords i
346 let ibc = ibc_write i
347 let ks = map show (names s)
348 setState (i { syntax_rules = s : rs,
349 syntax_keywords = ks ++ ns,
350 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc
351 })
352 fc <- pfc
353 return (PSyntax fc s)
354 where
355 names (Rule syms _ _) = mapMaybe ename syms
356 ename (Keyword n) = Just n
357 ename _ = Nothing
359pSyntaxRule :: SyntaxInfo -> IParser Syntax
360pSyntaxRule syn
361 = do push_indent
362 sty <- option AnySyntax (do reserved "term"; return TermSyntax
363 <|> do reserved "pattern"; return PatternSyntax)
364 reserved "syntax"
365 syms <- many1 pSynSym
366 when (all expr syms) $ fail "No keywords in syntax rule"
367 let ns = mapMaybe name syms
368 when (length ns /= length (nub ns))
369 $ fail "Repeated variable in syntax rule"
370 lchar '='
371 tm <- pExpr syn
372 pTerminator
373 return (Rule (mkSimple syms) tm sty)
374 where
375 expr (Expr _) = True
376 expr _ = False
377 name (Expr n) = Just n
378 name _ = Nothing
380 -- Can't parse two full expressions (i.e. expressions with application) in a row
381 -- so change the first to a simple expression
383 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
384 mkSimple xs = mkSimple' xs
386 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : mkSimple' (Expr e1 : es)
387 mkSimple' (e : es) = e : mkSimple' es
388 mkSimple' [] = []
390pSynSym :: IParser SSymbol
391pSynSym = try (do lchar '['; n <- pName; lchar ']'
392 return (Expr n))
393 <|> do n <- iName []
394 return (Keyword n)
395 <|> do sym <- strlit
396 return (Symbol sym)
398pFunDecl' :: SyntaxInfo -> IParser PDecl
399pFunDecl' syn = try (do push_indent
400 acc <- pAccessibility
401 n_in <- pfName
402 let n = expandNS syn n_in
403 ty <- pTSig syn
404 fc <- pfc
405 pTerminator
406-- ty' <- implicit syn n ty
407 addAcc n acc
408 return (PTy syn fc n ty))
409 <|> try (pPattern syn)
411pUsing :: SyntaxInfo -> IParser [PDecl]
412pUsing syn =
413 do reserved "using";
414 lchar '('
415 ns <- tyDeclList syn
416 lchar ')'
417 open_block
418 let uvars = using syn
419 ds <- many1 (pDecl (syn { using = uvars ++ ns }))
420 close_block
421 return (concat ds)
423pParams :: SyntaxInfo -> IParser [PDecl]
424pParams syn =
425 do reserved "params";
426 lchar '('
427 ns <- tyDeclList syn
428 lchar ')'
429 lchar '{'
430 let pvars = syn_params syn
431 ds <- many1 (pDecl syn { syn_params = pvars ++ ns })
432 lchar '}'
433 fc <- pfc
434 return [PParams fc ns (concat ds)]
436pNamespace :: SyntaxInfo -> IParser [PDecl]
437pNamespace syn =
438 do reserved "namespace";
439 n <- identifier
440 open_block
441 ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
442 close_block
443 return [PNamespace n (concat ds)]
445expandNS :: SyntaxInfo -> Name -> Name
446expandNS syn n@(NS _ _) = n
447expandNS syn n = case syn_namespace syn of
448 [] -> n
449 xs -> NS n xs
451--------- Fixity ---------
453pFixity :: IParser PDecl
454pFixity = do push_indent
455 f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
456 pTerminator
457 let prec = fromInteger i
458 istate <- getState
459 let fs = map (Fix (f prec)) ops
460 setState (istate {
461 idris_infixes = sort (fs ++ idris_infixes istate),
462 ibc_write = map IBCFix fs ++ ibc_write istate })
463 fc <- pfc
464 return (PFix fc (f prec) ops)
466fixity :: IParser (Int -> Fixity)
467fixity = try (do reserved "infixl"; return Infixl)
468 <|> try (do reserved "infixr"; return Infixr)
469 <|> try (do reserved "infix"; return InfixN)
470 <|> try (do reserved "prefix"; return PrefixN)
472--------- Tyoe classes ---------
474pClass :: SyntaxInfo -> IParser [PDecl]
475pClass syn = do acc <- pAccessibility
476 reserved "class"
477 fc <- pfc
478 cons <- pConstList syn
479 n_in <- pName; let n = expandNS syn n_in
480 cs <- many1 carg
481 reserved "where"; open_block
482 ds <- many1 $ pFunDecl syn
483 close_block
484 let allDs = concat ds
485 accData acc n (concatMap declared allDs)
486 return [PClass syn fc cons n cs allDs]
487 where
488 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'
489 return (i, ty)
490 <|> do i <- pName;
491 return (i, PSet)
493pInstance :: SyntaxInfo -> IParser [PDecl]
494pInstance syn = do reserved "instance"
495 fc <- pfc
496 cs <- pConstList syn
497 cn <- pName
498 args <- many1 (pSimpleExpr syn)
499 let sc = PApp fc (PRef fc cn) (map pexp args)
500 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
501 reserved "where"; open_block
502 ds <- many1 $ pFunDecl syn
503 close_block
504 return [PInstance syn fc cs cn args t (concat ds)]
506--------- Expressions ---------
508pExpr syn = do i <- getState
509 buildExpressionParser (table (idris_infixes i)) (pExpr' syn)
511pExpr' :: SyntaxInfo -> IParser PTerm
512pExpr' syn
513 = try (pExtExpr syn)
514 <|> pNoExtExpr syn
516pExtExpr :: SyntaxInfo -> IParser PTerm
517pExtExpr syn = do i <- getState
518 pExtensions syn (syntax_rules i)
520pSimpleExtExpr :: SyntaxInfo -> IParser PTerm
521pSimpleExtExpr syn = do i <- getState
522 pExtensions syn (filter simple (syntax_rules i))
523 where
524 simple (Rule (Expr x:xs) _ _) = False
525 simple (Rule (SimpleExpr x:xs) _ _) = False
526 simple (Rule [Keyword _] _ _) = True
527 simple (Rule [Symbol _] _ _) = True
528 simple (Rule (_:xs) _ _) = case (last xs) of
529 Keyword _ -> True
530 Symbol _ -> True
531 _ -> False
532 simple _ = False
534pNoExtExpr syn =
535 try (pApp syn)
536 <|> try (pSimpleExpr syn)
537 <|> pLambda syn
538 <|> pLet syn
539 <|> pPi syn
540 <|> pDoBlock syn
541 <|> pComprehension syn
543pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
544pExtensions syn rules = choice (map (\x -> try (pExt syn x)) (filter valid rules))
545 where
546 valid (Rule _ _ AnySyntax) = True
547 valid (Rule _ _ PatternSyntax) = inPattern syn
548 valid (Rule _ _ TermSyntax) = not (inPattern syn)
551pExt :: SyntaxInfo -> Syntax -> IParser PTerm
552pExt syn (Rule ssym ptm _)
553 = do smap <- mapM pSymbol ssym
554 let ns = mapMaybe id smap
555 return (update ns ptm) -- updated with smap
556 where
557 pSymbol (Keyword n) = do reserved (show n); return Nothing
558 pSymbol (Expr n) = do tm <- pExpr syn
559 return $ Just (n, tm)
560 pSymbol (SimpleExpr n) = do tm <- pSimpleExpr syn
561 return $ Just (n, tm)
562 pSymbol (Symbol s) = do symbol s
563 return Nothing
564 dropn n [] = []
565 dropn n ((x,t) : xs) | n == x = xs
566 | otherwise = (x,t):dropn n xs
568 update ns (PRef fc n) = case lookup n ns of
569 Just t -> t
570 _ -> PRef fc n
571 update ns (PLam n ty sc) = PLam n (update ns ty) (update (dropn n ns) sc)
572 update ns (PPi p n ty sc) = PPi p n (update ns ty) (update (dropn n ns) sc)
573 update ns (PLet n ty val sc) = PLet n (update ns ty) (update ns val)
574 (update (dropn n ns) sc)
575 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
576 update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)
577 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)
578 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)
579 update ns (PAlternative as) = PAlternative (map (update ns) as)
580 update ns (PHidden t) = PHidden (update ns t)
581 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
582 where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
583 upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds
584 upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)
585 : upd (dropn n ns) ds
586 upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t)
587 : upd ns ds
588 upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)
589 : upd ns ds
590 update ns t = t
592pName = do i <- getState
593 iName (syntax_keywords i)
594 <|> do reserved "instance"
595 i <- getState
596 UN n <- iName (syntax_keywords i)
597 return (UN ('@':n))
600pfName = try pName
601 <|> do lchar '('; o <- operator; lchar ')'; return (UN o)
603pAccessibility' :: IParser Accessibility
604pAccessibility'
605 = do reserved "public"; return Public
606 <|> do reserved "abstract"; return Frozen
607 <|> do reserved "private"; return Hidden
609pAccessibility :: IParser (Maybe Accessibility)
610pAccessibility
611 = do acc <- pAccessibility'; return (Just acc)
612 <|> return Nothing
614addAcc :: Name -> Maybe Accessibility -> IParser ()
615addAcc n a = do i <- getState
616 setState (i { hide_list = (n, a) : hide_list i })
618pSimpleExpr syn =
619 try (do symbol "!["; t <- pTerm; lchar ']'
620 return $ PQuote t)
621 <|> do lchar '?'; x <- pName; return (PMetavar x)
622 <|> do reserved "refl"; fc <- pfc; return (PRefl fc)
623-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)
624 <|> do reserved "proof"; lchar '{';
625 ts <- endBy (pTactic syn) (lchar ';')
626 lchar '}'
627 return (PProof ts)
628 <|> do reserved "tactics"; lchar '{';
629 ts <- endBy (pTactic syn) (lchar ';')
630 lchar '}'
631 return (PTactics ts)
632 <|> do reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
633 open_block
634 push_indent
635 opts <- many1 (do notEndBlock
636 x <- pCaseOpt syn
637 pKeepTerminator
638 return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
639 pop_indent
640 close_block
641 return (PCase fc scr opts)
642 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))
643 <|> try (pList syn)
644 <|> try (pAlt syn)
645 <|> try (pIdiom syn)
646 <|> try (do lchar '('; bracketed syn)
647 <|> try (do c <- pConstant; fc <- pfc
648 return (modifyConst syn fc (PConstant c)))
649 <|> do reserved "Set"; return PSet
650 <|> try (do symbol "()"; fc <- pfc; return (PTrue fc))
651 <|> try (do symbol "_|_"; fc <- pfc; return (PFalse fc))
652 <|> do lchar '_'; return Placeholder
653 <|> pSimpleExtExpr syn
655bracketed syn =
656 try (pPair syn)
657 <|> try (do e <- pExpr syn; lchar ')'; return e)
658-- <|> try (do reserved "typed"
659-- e <- pExpr syn; symbol ":"; t <- pExpr syn; lchar ')'
660-- return (PTyped e t))
661 <|> try (do fc <- pfc; o <- operator; e <- pExpr syn; lchar ')'
662 return $ PLam (MN 0 "x") Placeholder
663 (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 0 "x")),
664 pexp e]))
665 <|> try (do fc <- pfc; e <- pSimpleExpr syn; o <- operator; lchar ')'
666 return $ PLam (MN 0 "x") Placeholder
667 (PApp fc (PRef fc (UN o)) [pexp e,
668 pexp (PRef fc (MN 0 "x"))]))
670pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
671pCaseOpt syn = do lhs <- pExpr syn; symbol "=>";
672 rhs <- pExpr syn
673 return (lhs, rhs)
675modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
676modifyConst syn fc (PConstant (I x))
677 | not (inPattern syn)
678 = PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I x))]
679modifyConst syn fc x = x
681pList syn = do lchar '['; fc <- pfc
682 xs <- sepBy (pExpr syn) (lchar ','); lchar ']'
683 return (mkList fc xs)
684 where
685 mkList fc [] = PRef fc (UN "Nil")
686 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
688pPair syn = try (do l <- pExpr syn
689 fc <- pfc
690 rest <- restTuple
691 case rest of
692 [] -> return l
693 [Left r] -> return (PPair fc l r)
694 [Right r] -> return (PDPair fc l Placeholder r))
695 <|> try (do x <- ntuple
696 lchar ')'
697 return x)
698 <|> do ln <- pName; lchar ':'; lty <- pExpr syn;
699 reservedOp "**";
700 fc <- pfc
701 r <- pExpr syn; lchar ')';
702 return (PDPair fc (PRef fc ln) lty r)
703 where
704 restTuple = do lchar ')'; return []
705 <|> do lchar ','
706 r <- pExpr syn
707 lchar ')'
708 return [Left r]
709 <|> do reservedOp "**"
710 r <- pExpr syn
711 lchar ')'
712 return [Right r]
713 ntuple = try (do l <- pExpr syn; fc <- pfc; lchar ','
714 rest <- ntuple
715 return (PPair fc l rest))
716 <|> (do l <- pExpr syn; fc <- pfc; lchar ','
717 r <- pExpr syn
718 return (PPair fc l r))
720pAlt syn = do symbol "(|";
721 alts <- sepBy1 (pExpr' syn) (lchar ',')
722 symbol "|)"
723 return (PAlternative alts)
725pHSimpleExpr syn
726 = do lchar '.'
727 e <- pSimpleExpr syn
728 return $ PHidden e
729 <|> pSimpleExpr syn
731pApp syn = do f <- pSimpleExpr syn
732 fc <- pfc
733 args <- many1 (do notEndApp
734 pArg syn)
735 i <- getState
736 return (dslify i $ PApp fc f args)
737 where
738 dslify i (PApp fc (PRef _ f) [a])
739 | [d] <- lookupCtxt Nothing f (idris_dsls i)
740 = desugar (syn { dsl_info = d }) i (getTm a)
741 dslify i t = t
743pArg :: SyntaxInfo -> IParser PArg
744pArg syn = try (pImplicitArg syn)
745 <|> try (pConstraintArg syn)
746 <|> do e <- pSimpleExpr syn
747 return (pexp e)
749pImplicitArg syn = do lchar '{'; n <- pName
750 fc <- pfc
751 v <- option (PRef fc n) (do lchar '='; pExpr syn)
752 lchar '}'
753 return (pimp n v)
755pConstraintArg syn = do symbol "@{"; e <- pExpr syn; symbol "}"
756 return (pconst e)
758pTSig syn = do lchar ':'
759 cs <- pConstList syn
760 sc <- pExpr syn
761 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
763pLambda syn = do lchar '\\'
764 (try (do xt <- tyOptDeclList syn
765 symbol "=>"
766 sc <- pExpr syn
767 return (bindList PLam xt sc))
768 <|> (do ps <- sepBy (do fc <- pfc
769 e <- pSimpleExpr syn
770 return (fc, e)) (lchar ',')
771 symbol "=>"
772 sc <- pExpr syn
773 return (pmList (zip [0..] ps) sc)))
774 where pmList [] sc = sc
775 pmList ((i, (fc, x)) : xs) sc
776 = PLam (MN i "lamp") Placeholder
777 (PCase fc (PRef fc (MN i "lamp"))
778 [(x, (pmList xs sc))])
780pLet syn = try (do reserved "let"; n <- pName;
781 ty <- option Placeholder (do lchar ':'; pExpr' syn)
782 lchar '='; v <- pExpr syn
783 reserved "in"; sc <- pExpr syn
784 return (PLet n ty v sc))
785 <|> (do reserved "let"; fc <- pfc; pat <- pExpr' syn
786 symbol "="; v <- pExpr syn
787 reserved "in"; sc <- pExpr syn
788 return (PCase fc v [(pat, sc)]))
790pPi syn =
791 try (do lazy <- option False (do lchar '|'; return True)
792 st <- pStatic
793 lchar '('; xt <- tyDeclList syn; lchar ')'
794 symbol "->"
795 sc <- pExpr syn
796 return (bindList (PPi (Exp lazy st)) xt sc))
797 <|> try (do lazy <- option False (do lchar '|'; return True)
798 st <- pStatic
799 lchar '{'; xt <- tyDeclList syn; lchar '}'
800 symbol "->"
801 sc <- pExpr syn
802 return (bindList (PPi (Imp lazy st)) xt sc))
803 <|> do --lazy <- option False (do lchar '|'; return True)
804 lchar '{'; reserved "static"; lchar '}'
805 t <- pExpr' syn
806 symbol "->"
807 sc <- pExpr syn
808 return (PPi (Exp False Static) (MN 42 "__pi_arg") t sc)
810pConstList :: SyntaxInfo -> IParser [PTerm]
811pConstList syn = try (do lchar '('
812 tys <- sepBy1 (pExpr' syn) (lchar ',')
813 lchar ')'
814 reservedOp "=>"
815 return tys)
816 <|> try (do t <- pExpr syn
817 reservedOp "=>"
818 return [t])
819 <|> return []
821tyDeclList syn = try (sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))
822 (lchar ','))
823 <|> do ns <- sepBy1 pName (lchar ',')
824 t <- pTSig syn
825 return (map (\x -> (x, t)) ns)
827tyOptDeclList syn = sepBy1 (do x <- pfName;
828 t <- option Placeholder (do lchar ':'
829 pExpr syn)
830 return (x,t))
831 (lchar ',')
833bindList b [] sc = sc
834bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
836pComprehension syn
837 = do lchar '['; fc <- pfc; pat <- pExpr syn; lchar '|';
838 qs <- sepBy1 (pDo syn) (lchar ','); lchar ']';
839 return (PDoBlock (map addGuard qs ++
840 [DoExp fc (PApp fc (PRef fc (UN "return"))
841 [pexp pat])]))
842 where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
843 [pexp e])
844 addGuard x = x
846pDoBlock syn
847 = do reserved "do"; open_block
848 push_indent
849 ds <- many1 (do notEndBlock
850 x <- pDo syn; pKeepTerminator; return x)
851 pop_indent
852 close_block
853 return (PDoBlock ds)
855pDo syn
856 = try (do reserved "let"; i <- pName;
857 ty <- option Placeholder (do lchar ':'; pExpr' syn)
858 reservedOp "="; fc <- pfc
859 e <- pExpr syn
860 return (DoLet fc i ty e))
861 <|> try (do reserved "let"; i <- pExpr' syn; reservedOp "="; fc <- pfc
862 sc <- pExpr syn
863 return (DoLetP fc i sc))
864 <|> try (do i <- pName; symbol "<-"; fc <- pfc
865 e <- pExpr syn;
866 return (DoBind fc i e))
867 <|> try (do i <- pExpr' syn; symbol "<-"; fc <- pfc
868 e <- pExpr syn;
869 return (DoBindP fc i e))
870 <|> try (do e <- pExpr syn; fc <- pfc
871 return (DoExp fc e))
873pIdiom syn
874 = do symbol "[|"; fc <- pfc; e <- pExpr syn; symbol "|]"
875 return (PIdiom fc e)
877pConstant :: IParser Const
878pConstant = do reserved "Integer";return BIType
879 <|> do reserved "Int"; return IType
880 <|> do reserved "Char"; return ChType
881 <|> do reserved "Float"; return FlType
882 <|> do reserved "String"; return StrType
883 <|> do reserved "Ptr"; return PtrType
884 <|> try (do f <- float; return $ Fl f)
885 <|> try (do i <- natural; lchar 'L'; return $ BI i)
886 <|> try (do i <- natural; return $ I (fromInteger i))
887 <|> try (do s <- strlit; return $ Str s)
888 <|> try (do c <- chlit; return $ Ch c)
890pStatic :: IParser Static
891pStatic = do lchar '['; reserved "static"; lchar ']';
892 return Static
893 <|> return Dynamic
895table fixes
896 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
897 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]
898 ++ toTable (reverse fixes) ++
899 [[binary "=" (\fc x y -> PEq fc x y) AssocLeft],
900 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
902toTable fs = map (map toBin)
903 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
904 where toBin (Fix (PrefixN _) op) = prefix op
905 (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
906 toBin (Fix f op)
907 = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
908 assoc (Infixl _) = AssocLeft
909 assoc (Infixr _) = AssocRight
910 assoc (InfixN _) = AssocNone
912binary name f assoc = Infix (do { reservedOp name; fc <- pfc;
913 return (f fc) }) assoc
914prefix name f = Prefix (do { reservedOp name; fc <- pfc;
915 return (f fc) })
917--------- Data declarations ---------
919-- (works for classes too - 'abstract' means the data/class is visible but members not)
920accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()
921accData (Just Frozen) n ns = do addAcc n (Just Frozen)
922 mapM_ (\n -> addAcc n (Just Hidden)) ns
923accData a n ns = do addAcc n a; mapM_ (\n -> addAcc n a) ns
925pRecord :: SyntaxInfo -> IParser PDecl
926pRecord syn = try (do acc <- pAccessibility
927 reserved "record"; fc <- pfc
928 tyn_in <- pfName; ty <- pTSig syn
929 let tyn = expandNS syn tyn_in
930 reserved "where"
931 (cn, cty, _) <- pConstructor syn
932 pTerminator
933 accData acc tyn [cn]
934 return $ PRecord syn fc tyn ty cn cty)
936pData :: SyntaxInfo -> IParser PDecl
937pData syn = try (do acc <- pAccessibility
938 reserved "data"; fc <- pfc
939 tyn_in <- pfName; ty <- pTSig syn
940 let tyn = expandNS syn tyn_in
941 reserved "where"
942 open_block
943 push_indent
944 cons <- many (do notEndBlock
945 c <- pConstructor syn
946 pKeepTerminator
947 return c) -- (lchar '|')
948 pop_indent
949 close_block
950 accData acc tyn (map (\ (n, _, _) -> n) cons)
951 return $ PData syn fc (PDatadecl tyn ty cons))
952 <|> try (do push_indent
953 acc <- pAccessibility
954 reserved "data"; fc <- pfc
955 tyn_in <- pfName; args <- many pName
956 let tyn = expandNS syn tyn_in
957 lchar '='
958 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
959 pTerminator
960 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
961 let ty = bindArgs (map (\a -> PSet) args) PSet
962 cons' <- mapM (\ (x, cargs, cfc) ->
963 do let cty = bindArgs cargs conty
964 return (x, cty, cfc)) cons
965 accData acc tyn (map (\ (n, _, _) -> n) cons')
966 return $ PData syn fc (PDatadecl tyn ty cons'))
967 where
968 mkPApp fc t [] = t
969 mkPApp fc t xs = PApp fc t (map pexp xs)
971bindArgs :: [PTerm] -> PTerm -> PTerm
972bindArgs [] t = t
973bindArgs (x:xs) t = PPi expl (MN 0 "t") x (bindArgs xs t)
975pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)
976pConstructor syn
977 = do cn_in <- pfName; fc <- pfc
978 let cn = expandNS syn cn_in
979 ty <- pTSig syn
980-- ty' <- implicit syn cn ty
981 return (cn, ty, fc)
983pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm], FC)
984pSimpleCon syn
985 = do cn_in <- pfName
986 let cn = expandNS syn cn_in
987 fc <- pfc
988 args <- many (do notEndApp
989 pSimpleExpr syn)
990 return (cn, args, fc)
992--------- DSL syntax overloading ---------
994pDSL :: SyntaxInfo -> IParser PDecl
995pDSL syn = do reserved "dsl"; n <- pfName
996 open_block; push_indent
997 bs <- many1 (do notEndBlock
998 b <- pOverload syn
999 pKeepTerminator
1000 return b)
1001 pop_indent; close_block
1002 let dsl = mkDSL bs (dsl_info syn)
1003 checkDSL dsl
1004 i <- getState
1005 setState (i { idris_dsls = addDef n dsl (idris_dsls i) })
1006 return (PDSL n dsl)
1007 where mkDSL bs dsl = let var = lookup "variable" bs
1008 first = lookup "index_first" bs
1009 next = lookup "index_next" bs
1010 leto = lookup "let" bs
1011 lambda = lookup "lambda" bs in
1012 initDSL { dsl_var = var,
1013 index_first = first,
1014 index_next = next,
1015 dsl_lambda = lambda,
1016 dsl_let = leto }
1018checkDSL :: DSL -> IParser ()
1019checkDSL dsl = return ()
1021pOverload :: SyntaxInfo -> IParser (String, PTerm)
1022pOverload syn = do o <- identifier <|> do reserved "let"; return "let"
1023 if (not (o `elem` overloadable))
1024 then fail $ show o ++ " is not an overloading"
1025 else do
1026 lchar '='
1027 t <- pExpr syn
1028 return (o, t)
1029 where overloadable = ["let","lambda","index_first","index_next","variable"]
1031--------- Pattern match clauses ---------
1033pPattern :: SyntaxInfo -> IParser PDecl
1034pPattern syn = do clause <- pClause syn
1035 fc <- pfc
1036 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
1038pArgExpr syn = let syn' = syn { inPattern = True } in
1039 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
1041pRHS :: SyntaxInfo -> Name -> IParser PTerm
1042pRHS syn n = do lchar '='; pExpr syn
1043 <|> do symbol "?="; rhs <- pExpr syn;
1044 return (PLet (UN "value") Placeholder rhs (PMetavar n'))
1045 <|> do reserved "impossible"; return PImpossible
1046 where mkN (UN x) = UN (x++"_lemma_1")
1047 mkN (NS x n) = NS (mkN x) n
1048 n' = mkN n
1050pClause :: SyntaxInfo -> IParser PClause
1051pClause syn
1052 = try (do push_indent
1053 n_in <- pfName; let n = expandNS syn n_in
1054 cargs <- many (pConstraintArg syn)
1055 iargs <- many (pImplicitArg syn)
1056 fc <- pfc
1057 args <- many (pArgExpr syn)
1058 wargs <- many (pWExpr syn)
1059 rhs <- pRHS syn n
1060 ist <- getState
1061 let ctxt = tt_ctxt ist
1062 let wsyn = syn { syn_namespace = [] }
1063 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1064 pop_indent
1065 return x,
1066 do pTerminator
1067 return ([], [])]
1068 let capp = PApp fc (PRef fc n)
1069 (iargs ++ cargs ++ map pexp args)
1070 ist <- getState
1071 setState (ist { lastParse = Just n })
1072 return $ PClause n capp wargs rhs wheres)
1073 <|> try (do push_indent
1074 wargs <- many1 (pWExpr syn)
1075 ist <- getState
1076 n <- case lastParse ist of
1077 Just t -> return t
1078 Nothing -> fail "Invalid clause"
1079 rhs <- pRHS syn n
1080 let ctxt = tt_ctxt ist
1081 let wsyn = syn { syn_namespace = [] }
1082 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1083 pop_indent
1084 return x,
1085 do pTerminator
1086 return ([], [])]
1087 return $ PClauseR wargs rhs wheres)
1089 <|> try (do push_indent
1090 n_in <- pfName; let n = expandNS syn n_in
1091 cargs <- many (pConstraintArg syn)
1092 iargs <- many (pImplicitArg syn)
1093 fc <- pfc
1094 args <- many (pArgExpr syn)
1095 wargs <- many (pWExpr syn)
1096 let capp = PApp fc (PRef fc n)
1097 (iargs ++ cargs ++ map pexp args)
1098 reserved "with"
1099 wval <- pSimpleExpr syn
1100 open_block
1101 ds <- many1 $ pFunDecl syn
1102 let withs = map (fillLHSD n capp wargs) $ concat ds
1103 close_block
1104 ist <- getState
1105 setState (ist { lastParse = Just n })
1106 pop_indent
1107 return $ PWith n capp wargs wval withs)
1109 <|> try (do wargs <- many1 (pWExpr syn)
1110 reserved "with"
1111 wval <- pSimpleExpr syn
1112 open_block
1113 ds <- many1 $ pFunDecl syn
1114 let withs = concat ds
1115 close_block
1116 return $ PWithR wargs wval withs)
1118 <|> do push_indent
1119 l <- pArgExpr syn
1120 op <- operator
1121 let n = expandNS syn (UN op)
1122 r <- pArgExpr syn
1123 fc <- pfc
1124 wargs <- many (pWExpr syn)
1125 rhs <- pRHS syn n
1126 let wsyn = syn { syn_namespace = [] }
1127 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1128 pop_indent
1129 return x,
1130 do pTerminator
1131 return ([], [])]
1132 ist <- getState
1133 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1134 setState (ist { lastParse = Just n })
1135 return $ PClause n capp wargs rhs wheres
1137 <|> do l <- pArgExpr syn
1138 op <- operator
1139 let n = expandNS syn (UN op)
1140 r <- pArgExpr syn
1141 fc <- pfc
1142 wargs <- many (pWExpr syn)
1143 reserved "with"
1144 wval <- pSimpleExpr syn
1145 open_block
1146 ds <- many1 $ pFunDecl syn
1147 close_block
1148 ist <- getState
1149 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1150 let withs = map (fillLHSD n capp wargs) $ concat ds
1151 setState (ist { lastParse = Just n })
1152 return $ PWith n capp wargs wval withs
1153 where
1154 fillLHS n capp owargs (PClauseR wargs v ws)
1155 = PClause n capp (owargs ++ wargs) v ws
1156 fillLHS n capp owargs (PWithR wargs v ws)
1157 = PWith n capp (owargs ++ wargs) v
1158 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1159 fillLHS _ _ _ c = c
1161 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1162 fillLHSD n c a x = x
1164pWExpr :: SyntaxInfo -> IParser PTerm
1165pWExpr syn = do lchar '|'; pExpr' syn
1167pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
1168pWhereblock n syn
1169 = do reserved "where"; open_block
1170 ds <- many1 $ pFunDecl syn
1171 let dns = concatMap (concatMap declared) ds
1172 close_block
1173 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1175pDirective :: IParser [PDecl]
1176pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;
1177 return [PDirective (do addLib lib
1178 addIBC (IBCLib lib))])
1179 <|> try (do lchar '%'; reserved "link"; obj <- strlit;
1180 return [PDirective (do datadir <- liftIO $ getDataDir
1181 o <- liftIO $ findInPath [".", datadir] obj
1182 addIBC (IBCObj o)
1183 addObjectFile o)])
1184 <|> try (do lchar '%'; reserved "include"; hdr <- strlit;
1185 return [PDirective (do addHdr hdr
1186 addIBC (IBCHeader hdr))])
1187 <|> try (do lchar '%'; reserved "hide"; n <- iName []
1188 return [PDirective (do setAccessibility n Hidden
1189 addIBC (IBCAccess n Hidden))])
1190 <|> try (do lchar '%'; reserved "freeze"; n <- iName []
1191 return [PDirective (do setAccessibility n Frozen
1192 addIBC (IBCAccess n Frozen))])
1193 <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'
1194 return [PDirective (do i <- getIState
1195 putIState (i { default_access = acc }))])
1196 <|> do lchar '%'; reserved "logging"; i <- natural;
1197 return [PDirective (setLogLevel (fromInteger i))]
1199pTactic :: SyntaxInfo -> IParser PTactic
1200pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
1201 return $ Intro ns
1202 <|> do reserved "intros"; return Intros
1203 <|> try (do reserved "refine"; n <- pName
1204 imps <- many1 imp
1205 return $ Refine n imps)
1206 <|> do reserved "refine"; n <- pName
1207 i <- getState
1208 return $ Refine n []
1209 <|> do reserved "rewrite"; t <- pExpr syn;
1210 i <- getState
1211 return $ Rewrite (desugar syn i t)
1212 <|> do reserved "let"; n <- pName; lchar '=';
1213 t <- pExpr syn;
1214 i <- getState
1215 return $ LetTac n (desugar syn i t)
1216 <|> do reserved "focus"; n <- pName
1217 return $ Focus n
1218 <|> do reserved "exact"; t <- pExpr syn;
1219 i <- getState
1220 return $ Exact (desugar syn i t)
1221 <|> do reserved "try"; t <- pTactic syn;
1222 lchar '|';
1223 t1 <- pTactic syn
1224 return $ Try t t1
1225 <|> do lchar '{'
1226 t <- pTactic syn;
1227 lchar ';';
1228 t1 <- pTactic syn;
1229 lchar '}'
1230 return $ TSeq t t1
1231 <|> do reserved "compute"; return Compute
1232 <|> do reserved "trivial"; return Trivial
1233 <|> do reserved "solve"; return Solve
1234 <|> do reserved "attack"; return Attack
1235 <|> do reserved "state"; return ProofState
1236 <|> do reserved "term"; return ProofTerm
1237 <|> do reserved "undo"; return Undo
1238 <|> do reserved "qed"; return Qed
1239 <|> do reserved "abandon"; return Abandon
1240 <|> do lchar ':'; reserved "q"; return Abandon
1241 where
1242 imp = do lchar '?'; return False
1243 <|> do lchar '_'; return True