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