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