git.iko.soy/Idris-dev
on 047be9e help sign in
Idris-dev/src/Idris/Parser.hs
1315 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 ds : ds')
300 = PInstance f s cs n ps t (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 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 cs <- pConstList syn
500 cn <- pName
501 args <- many1 (pSimpleExpr syn)
502 let sc = PApp fc (PRef fc cn) (map pexp args)
503 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
504 reserved "where"; open_block
505 ds <- many $ pFunDecl syn
506 close_block
507 return [PInstance syn fc cs cn args t (concat ds)]
509--------- Expressions ---------
511pExpr syn = do i <- getState
512 buildExpressionParser (table (idris_infixes i)) (pExpr' syn)
514pExpr' :: SyntaxInfo -> IParser PTerm
515pExpr' syn
516 = try (pExtExpr syn)
517 <|> pNoExtExpr syn
519pExtExpr :: SyntaxInfo -> IParser PTerm
520pExtExpr syn = do i <- getState
521 pExtensions syn (syntax_rules i)
523pSimpleExtExpr :: SyntaxInfo -> IParser PTerm
524pSimpleExtExpr syn = do i <- getState
525 pExtensions syn (filter simple (syntax_rules i))
526 where
527 simple (Rule (Expr x:xs) _ _) = False
528 simple (Rule (SimpleExpr x:xs) _ _) = False
529 simple (Rule [Keyword _] _ _) = True
530 simple (Rule [Symbol _] _ _) = True
531 simple (Rule (_:xs) _ _) = case (last xs) of
532 Keyword _ -> True
533 Symbol _ -> True
534 _ -> False
535 simple _ = False
537pNoExtExpr syn =
538 try (pApp syn)
539 <|> pRecordSet syn
540 <|> try (pSimpleExpr syn)
541 <|> pLambda syn
542 <|> pLet syn
543 <|> pPi syn
544 <|> pDoBlock syn
545 <|> pComprehension syn
547pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
548pExtensions syn rules = choice (map (\x -> try (pExt syn x)) (filter valid rules))
549 where
550 valid (Rule _ _ AnySyntax) = True
551 valid (Rule _ _ PatternSyntax) = inPattern syn
552 valid (Rule _ _ TermSyntax) = not (inPattern syn)
555pExt :: SyntaxInfo -> Syntax -> IParser PTerm
556pExt syn (Rule ssym ptm _)
557 = do smap <- mapM pSymbol ssym
558 let ns = mapMaybe id smap
559 return (update ns ptm) -- updated with smap
560 where
561 pSymbol (Keyword n) = do reserved (show n); return Nothing
562 pSymbol (Expr n) = do tm <- pExpr syn
563 return $ Just (n, tm)
564 pSymbol (SimpleExpr n) = do tm <- pSimpleExpr syn
565 return $ Just (n, tm)
566 pSymbol (Symbol s) = do symbol s
567 return Nothing
568 dropn n [] = []
569 dropn n ((x,t) : xs) | n == x = xs
570 | otherwise = (x,t):dropn n xs
572 update ns (PRef fc n) = case lookup n ns of
573 Just t -> t
574 _ -> PRef fc n
575 update ns (PLam n ty sc) = PLam n (update ns ty) (update (dropn n ns) sc)
576 update ns (PPi p n ty sc) = PPi p n (update ns ty) (update (dropn n ns) sc)
577 update ns (PLet n ty val sc) = PLet n (update ns ty) (update ns val)
578 (update (dropn n ns) sc)
579 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
580 update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)
581 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)
582 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)
583 update ns (PAlternative a as) = PAlternative a (map (update ns) as)
584 update ns (PHidden t) = PHidden (update ns t)
585 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
586 where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
587 upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds
588 upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)
589 : upd (dropn n ns) ds
590 upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t)
591 : upd ns ds
592 upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)
593 : upd ns ds
594 update ns t = t
596pName = do i <- getState
597 iName (syntax_keywords i)
598 <|> do reserved "instance"
599 i <- getState
600 UN n <- iName (syntax_keywords i)
601 return (UN ('@':n))
604pfName = try pName
605 <|> do lchar '('; o <- operator; lchar ')'; return (UN o)
607pAccessibility' :: IParser Accessibility
608pAccessibility'
609 = do reserved "public"; return Public
610 <|> do reserved "abstract"; return Frozen
611 <|> do reserved "private"; return Hidden
613pAccessibility :: IParser (Maybe Accessibility)
614pAccessibility
615 = do acc <- pAccessibility'; return (Just acc)
616 <|> return Nothing
618pFnOpts :: IParser [FnOpt]
619pFnOpts = do reserved "total"; xs <- pFnOpts; return (TotalFn : xs)
620 <|> do lchar '%'; reserved "assert_total"; xs <- pFnOpts; return (AssertTotal : xs)
621 <|> do lchar '%'; reserved "specialise";
622 lchar '['; ns <- sepBy pfName (lchar ','); lchar ']'
623 xs <- pFnOpts
624 return (Specialise ns : xs)
625 <|> return []
627addAcc :: Name -> Maybe Accessibility -> IParser ()
628addAcc n a = do i <- getState
629 setState (i { hide_list = (n, a) : hide_list i })
631pSimpleExpr syn =
632 try (do symbol "!["; t <- pTerm; lchar ']'
633 return $ PQuote t)
634 <|> do lchar '?'; x <- pName; return (PMetavar x)
635 <|> do reserved "refl"; fc <- pfc; return (PRefl fc)
636-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)
637 <|> do reserved "proof"; lchar '{';
638 ts <- endBy (pTactic syn) (lchar ';')
639 lchar '}'
640 return (PProof ts)
641 <|> do reserved "tactics"; lchar '{';
642 ts <- endBy (pTactic syn) (lchar ';')
643 lchar '}'
644 return (PTactics ts)
645 <|> do reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
646 open_block
647 push_indent
648 opts <- many1 (do notEndBlock
649 x <- pCaseOpt syn
650 pKeepTerminator
651 return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
652 pop_indent
653 close_block
654 return (PCase fc scr opts)
655 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))
656 <|> try (pList syn)
657 <|> try (pAlt syn)
658 <|> try (pIdiom syn)
659 <|> try (do lchar '('; bracketed syn)
660 <|> try (do c <- pConstant; fc <- pfc
661 return (modifyConst syn fc (PConstant c)))
662 <|> do reserved "Set"; return PSet
663-- <|> do symbol "*"; return PSet
664 <|> try (do symbol "()"; fc <- pfc; return (PTrue fc))
665 <|> try (do symbol "_|_"; fc <- pfc; return (PFalse fc))
666 <|> do lchar '_'; return Placeholder
667 <|> pSimpleExtExpr syn
669bracketed syn =
670 try (pPair syn)
671 <|> try (do e <- pExpr syn; lchar ')'; return e)
672-- <|> try (do reserved "typed"
673-- e <- pExpr syn; symbol ":"; t <- pExpr syn; lchar ')'
674-- return (PTyped e t))
675 <|> try (do fc <- pfc; o <- operator; e <- pExpr syn; lchar ')'
676 return $ PLam (MN 0 "x") Placeholder
677 (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 0 "x")),
678 pexp e]))
679 <|> try (do fc <- pfc; e <- pSimpleExpr syn; o <- operator; lchar ')'
680 return $ PLam (MN 0 "x") Placeholder
681 (PApp fc (PRef fc (UN o)) [pexp e,
682 pexp (PRef fc (MN 0 "x"))]))
684pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
685pCaseOpt syn = do lhs <- pExpr syn; symbol "=>";
686 rhs <- pExpr syn
687 return (lhs, rhs)
689modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
690modifyConst syn fc (PConstant (I x))
691 | not (inPattern syn)
692 = PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I x))]
693 | otherwise = PConstant (I x)
694modifyConst syn fc x = x
696pList syn = do lchar '['; fc <- pfc
697 xs <- sepBy (pExpr syn) (lchar ','); lchar ']'
698 return (mkList fc xs)
699 where
700 mkList fc [] = PRef fc (UN "Nil")
701 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
703pPair syn = try (do l <- pExpr syn
704 fc <- pfc
705 rest <- restTuple
706 case rest of
707 [] -> return l
708 [Left r] -> return (PPair fc l r)
709 [Right r] -> return (PDPair fc l Placeholder r))
710 <|> try (do x <- ntuple
711 lchar ')'
712 return x)
713 <|> do ln <- pName; lchar ':'; lty <- pExpr syn;
714 reservedOp "**";
715 fc <- pfc
716 r <- pExpr syn; lchar ')';
717 return (PDPair fc (PRef fc ln) lty r)
718 where
719 restTuple = do lchar ')'; return []
720 <|> do lchar ','
721 r <- pExpr syn
722 lchar ')'
723 return [Left r]
724 <|> do reservedOp "**"
725 r <- pExpr syn
726 lchar ')'
727 return [Right r]
728 ntuple = try (do l <- pExpr syn; fc <- pfc; lchar ','
729 rest <- ntuple
730 return (PPair fc l rest))
731 <|> (do l <- pExpr syn; fc <- pfc; lchar ','
732 r <- pExpr syn
733 return (PPair fc l r))
735pAlt syn = do symbol "(|";
736 alts <- sepBy1 (pExpr' syn) (lchar ',')
737 symbol "|)"
738 return (PAlternative False alts)
740pHSimpleExpr syn
741 = do lchar '.'
742 e <- pSimpleExpr syn
743 return $ PHidden e
744 <|> pSimpleExpr syn
746pApp syn = do f <- pSimpleExpr syn
747 fc <- pfc
748 args <- many1 (do notEndApp
749 pArg syn)
750 i <- getState
751 return (dslify i $ PApp fc f args)
752 where
753 dslify i (PApp fc (PRef _ f) [a])
754 | [d] <- lookupCtxt Nothing f (idris_dsls i)
755 = desugar (syn { dsl_info = d }) i (getTm a)
756 dslify i t = t
758pArg :: SyntaxInfo -> IParser PArg
759pArg syn = try (pImplicitArg syn)
760 <|> try (pConstraintArg syn)
761 <|> do e <- pSimpleExpr syn
762 return (pexp e)
764pImplicitArg syn = do lchar '{'; n <- pName
765 fc <- pfc
766 v <- option (PRef fc n) (do lchar '='; pExpr syn)
767 lchar '}'
768 return (pimp n v)
770pConstraintArg syn = do symbol "@{"; e <- pExpr syn; symbol "}"
771 return (pconst e)
773pRecordSet syn
774 = do reserved "record"
775 lchar '{'
776 fields <- sepBy1 pFieldSet (lchar ',')
777 lchar '}'
778 fc <- pfc
779 rec <- option Nothing (do e <- pSimpleExpr syn; return (Just e))
780 case rec of
781 Nothing ->
782 return (PLam (MN 0 "fldx") Placeholder
783 (applyAll fc fields (PRef fc (MN 0 "fldx"))))
784 Just v -> return (applyAll fc fields v)
785 where pFieldSet = do n <- pfName; lchar '='
786 e <- pExpr syn
787 return (n, e)
788 applyAll fc [] x = x
789 applyAll fc ((n, e) : es) x
790 = applyAll fc es (PApp fc (PRef fc (mkSet n)) [pexp e, pexp x])
792mkSet (UN n) = UN ("set_" ++ n)
793mkSet (MN 0 n) = MN 0 ("set_" ++ n)
794mkSet (NS n s) = NS (mkSet n) s
796pTSig syn = do lchar ':'
797 cs <- pConstList syn
798 sc <- pExpr syn
799 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
801pLambda syn = do lchar '\\'
802 (try (do xt <- tyOptDeclList syn
803 symbol "=>"
804 sc <- pExpr syn
805 return (bindList PLam xt sc))
806 <|> (do ps <- sepBy (do fc <- pfc
807 e <- pSimpleExpr syn
808 return (fc, e)) (lchar ',')
809 symbol "=>"
810 sc <- pExpr syn
811 return (pmList (zip [0..] ps) sc)))
812 where pmList [] sc = sc
813 pmList ((i, (fc, x)) : xs) sc
814 = PLam (MN i "lamp") Placeholder
815 (PCase fc (PRef fc (MN i "lamp"))
816 [(x, (pmList xs sc))])
818pLet syn = try (do reserved "let"; n <- pName;
819 ty <- option Placeholder (do lchar ':'; pExpr' syn)
820 lchar '='; v <- pExpr syn
821 reserved "in"; sc <- pExpr syn
822 return (PLet n ty v sc))
823 <|> (do reserved "let"; fc <- pfc; pat <- pExpr' syn
824 symbol "="; v <- pExpr syn
825 reserved "in"; sc <- pExpr syn
826 return (PCase fc v [(pat, sc)]))
828pPi syn =
829 try (do lazy <- option False (do lchar '|'; return True)
830 st <- pStatic
831 lchar '('; xt <- tyDeclList syn; lchar ')'
832 symbol "->"
833 sc <- pExpr syn
834 return (bindList (PPi (Exp lazy st)) xt sc))
835 <|> try (do lazy <- option False (do lchar '|'; return True)
836 st <- pStatic
837 lchar '{'; xt <- tyDeclList syn; lchar '}'
838 symbol "->"
839 sc <- pExpr syn
840 return (bindList (PPi (Imp lazy st)) xt sc))
841 <|> try (do lchar '{'; reserved "auto"
842 xt <- tyDeclList syn; lchar '}'
843 symbol "->"
844 sc <- pExpr syn
845 return (bindList (PPi (TacImp False Dynamic (PTactics [Trivial]))) xt sc))
846 <|> try (do lchar '{'; reserved "default"
847 script <- pSimpleExpr syn
848 xt <- tyDeclList syn; lchar '}'
849 symbol "->"
850 sc <- pExpr syn
851 return (bindList (PPi (TacImp False Dynamic script)) xt sc))
852 <|> do --lazy <- option False (do lchar '|'; return True)
853 lchar '{'; reserved "static"; lchar '}'
854 t <- pExpr' syn
855 symbol "->"
856 sc <- pExpr syn
857 return (PPi (Exp False Static) (MN 42 "__pi_arg") t sc)
859pConstList :: SyntaxInfo -> IParser [PTerm]
860pConstList syn = try (do lchar '('
861 tys <- sepBy1 (pExpr' syn) (lchar ',')
862 lchar ')'
863 reservedOp "=>"
864 return tys)
865 <|> try (do t <- pExpr syn
866 reservedOp "=>"
867 return [t])
868 <|> return []
870tyDeclList syn = try (sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))
871 (lchar ','))
872 <|> do ns <- sepBy1 pName (lchar ',')
873 t <- pTSig syn
874 return (map (\x -> (x, t)) ns)
876tyOptDeclList syn = sepBy1 (do x <- pfName;
877 t <- option Placeholder (do lchar ':'
878 pExpr syn)
879 return (x,t))
880 (lchar ',')
882bindList b [] sc = sc
883bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
885pComprehension syn
886 = do lchar '['; fc <- pfc; pat <- pExpr syn; lchar '|';
887 qs <- sepBy1 (pDo syn) (lchar ','); lchar ']';
888 return (PDoBlock (map addGuard qs ++
889 [DoExp fc (PApp fc (PRef fc (UN "return"))
890 [pexp pat])]))
891 where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
892 [pexp e])
893 addGuard x = x
895pDoBlock syn
896 = do reserved "do"; open_block
897 push_indent
898 ds <- many1 (do notEndBlock
899 x <- pDo syn; pKeepTerminator; return x)
900 pop_indent
901 close_block
902 return (PDoBlock ds)
904pDo syn
905 = try (do reserved "let"; i <- pName;
906 ty <- option Placeholder (do lchar ':'; pExpr' syn)
907 reservedOp "="; fc <- pfc
908 e <- pExpr syn
909 return (DoLet fc i ty e))
910 <|> try (do reserved "let"; i <- pExpr' syn; reservedOp "="; fc <- pfc
911 sc <- pExpr syn
912 return (DoLetP fc i sc))
913 <|> try (do i <- pName; symbol "<-"; fc <- pfc
914 e <- pExpr syn;
915 return (DoBind fc i e))
916 <|> try (do i <- pExpr' syn; symbol "<-"; fc <- pfc
917 e <- pExpr syn;
918 return (DoBindP fc i e))
919 <|> try (do e <- pExpr syn; fc <- pfc
920 return (DoExp fc e))
922pIdiom syn
923 = do symbol "[|"; fc <- pfc; e <- pExpr syn; symbol "|]"
924 return (PIdiom fc e)
926pConstant :: IParser Const
927pConstant = do reserved "Integer";return BIType
928 <|> do reserved "Int"; return IType
929 <|> do reserved "Char"; return ChType
930 <|> do reserved "Float"; return FlType
931 <|> do reserved "String"; return StrType
932 <|> do reserved "Ptr"; return PtrType
933 <|> try (do f <- float; return $ Fl f)
934-- <|> try (do i <- natural; lchar 'L'; return $ BI i)
935 <|> try (do i <- natural; return $ I (fromInteger i))
936 <|> try (do s <- strlit; return $ Str s)
937 <|> try (do c <- chlit; return $ Ch c)
939pStatic :: IParser Static
940pStatic = do lchar '['; reserved "static"; lchar ']';
941 return Static
942 <|> return Dynamic
944table fixes
945 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
946 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]
947 ++ toTable (reverse fixes) ++
948 [[backtick],
949 [binary "=" (\fc x y -> PEq fc x y) AssocLeft],
950 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
952toTable fs = map (map toBin)
953 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
954 where toBin (Fix (PrefixN _) op) = prefix op
955 (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
956 toBin (Fix f op)
957 = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
958 assoc (Infixl _) = AssocLeft
959 assoc (Infixr _) = AssocRight
960 assoc (InfixN _) = AssocNone
962binary name f assoc = Infix (do reservedOp name; fc <- pfc;
963 return (f fc)) assoc
964prefix name f = Prefix (do reservedOp name; fc <- pfc;
965 return (f fc))
966backtick = Infix (do lchar '`'; n <- pfName; lchar '`'
967 fc <- pfc
968 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
970--------- Data declarations ---------
972-- (works for classes too - 'abstract' means the data/class is visible but members not)
973accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()
974accData (Just Frozen) n ns = do addAcc n (Just Frozen)
975 mapM_ (\n -> addAcc n (Just Hidden)) ns
976accData a n ns = do addAcc n a; mapM_ (\n -> addAcc n a) ns
978pRecord :: SyntaxInfo -> IParser PDecl
979pRecord syn = do acc <- pAccessibility
980 reserved "record"; fc <- pfc
981 tyn_in <- pfName; ty <- pTSig syn
982 let tyn = expandNS syn tyn_in
983 reserved "where"
984 open_block
985 push_indent
986 (cn, cty, _) <- pConstructor syn
987 pKeepTerminator
988 pop_indent
989 close_block
990 accData acc tyn [cn]
991 let rsyn = syn { syn_namespace = show (nsroot tyn) :
992 syn_namespace syn }
993 let fns = getRecNames rsyn cty
994 mapM_ (\n -> addAcc n (toFreeze acc)) fns
995 return $ PRecord rsyn fc tyn ty cn cty
996 where
997 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkSet n)]
998 ++ getRecNames syn sc
999 getRecNames _ _ = []
1001 toFreeze (Just Frozen) = Just Hidden
1002 toFreeze x = x
1004pData :: SyntaxInfo -> IParser PDecl
1005pData syn = try (do acc <- pAccessibility
1006 reserved "data"; fc <- pfc
1007 tyn_in <- pfName; ty <- pTSig syn
1008 let tyn = expandNS syn tyn_in
1009 reserved "where"
1010 open_block
1011 push_indent
1012 cons <- many (do notEndBlock
1013 c <- pConstructor syn
1014 pKeepTerminator
1015 return c) -- (lchar '|')
1016 pop_indent
1017 close_block
1018 accData acc tyn (map (\ (n, _, _) -> n) cons)
1019 return $ PData syn fc (PDatadecl tyn ty cons))
1020 <|> try (do push_indent
1021 acc <- pAccessibility
1022 reserved "data"; fc <- pfc
1023 tyn_in <- pfName; args <- many pName
1024 let tyn = expandNS syn tyn_in
1025 lchar '='
1026 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
1027 pTerminator
1028 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
1029 let ty = bindArgs (map (\a -> PSet) args) PSet
1030 cons' <- mapM (\ (x, cargs, cfc) ->
1031 do let cty = bindArgs cargs conty
1032 return (x, cty, cfc)) cons
1033 accData acc tyn (map (\ (n, _, _) -> n) cons')
1034 return $ PData syn fc (PDatadecl tyn ty cons'))
1035 where
1036 mkPApp fc t [] = t
1037 mkPApp fc t xs = PApp fc t (map pexp xs)
1039bindArgs :: [PTerm] -> PTerm -> PTerm
1040bindArgs [] t = t
1041bindArgs (x:xs) t = PPi expl (MN 0 "t") x (bindArgs xs t)
1043pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)
1044pConstructor syn
1045 = do cn_in <- pfName; fc <- pfc
1046 let cn = expandNS syn cn_in
1047 ty <- pTSig syn
1048-- ty' <- implicit syn cn ty
1049 return (cn, ty, fc)
1052pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm], FC)
1053pSimpleCon syn
1054 = do cn_in <- pfName
1055 let cn = expandNS syn cn_in
1056 fc <- pfc
1057 args <- many (do notEndApp
1058 pSimpleExpr syn)
1059 return (cn, args, fc)
1061--------- DSL syntax overloading ---------
1063pDSL :: SyntaxInfo -> IParser PDecl
1064pDSL syn = do reserved "dsl"; n <- pfName
1065 open_block; push_indent
1066 bs <- many1 (do notEndBlock
1067 b <- pOverload syn
1068 pKeepTerminator
1069 return b)
1070 pop_indent; close_block
1071 let dsl = mkDSL bs (dsl_info syn)
1072 checkDSL dsl
1073 i <- getState
1074 setState (i { idris_dsls = addDef n dsl (idris_dsls i) })
1075 return (PDSL n dsl)
1076 where mkDSL bs dsl = let var = lookup "variable" bs
1077 first = lookup "index_first" bs
1078 next = lookup "index_next" bs
1079 leto = lookup "let" bs
1080 lambda = lookup "lambda" bs in
1081 initDSL { dsl_var = var,
1082 index_first = first,
1083 index_next = next,
1084 dsl_lambda = lambda,
1085 dsl_let = leto }
1087checkDSL :: DSL -> IParser ()
1088checkDSL dsl = return ()
1090pOverload :: SyntaxInfo -> IParser (String, PTerm)
1091pOverload syn = do o <- identifier <|> do reserved "let"; return "let"
1092 if (not (o `elem` overloadable))
1093 then fail $ show o ++ " is not an overloading"
1094 else do
1095 lchar '='
1096 t <- pExpr syn
1097 return (o, t)
1098 where overloadable = ["let","lambda","index_first","index_next","variable"]
1100--------- Pattern match clauses ---------
1102pPattern :: SyntaxInfo -> IParser PDecl
1103pPattern syn = do fc <- pfc
1104 clause <- pClause syn
1105 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
1107pArgExpr syn = let syn' = syn { inPattern = True } in
1108 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
1110pRHS :: SyntaxInfo -> Name -> IParser PTerm
1111pRHS syn n = do lchar '='; pExpr syn
1112 <|> do symbol "?="; rhs <- pExpr syn;
1113 return (PLet (UN "value") Placeholder rhs (PMetavar n'))
1114 <|> do reserved "impossible"; return PImpossible
1115 where mkN (UN x) = UN (x++"_lemma_1")
1116 mkN (NS x n) = NS (mkN x) n
1117 n' = mkN n
1119pClause :: SyntaxInfo -> IParser PClause
1120pClause syn
1121 = try (do push_indent
1122 n_in <- pfName; let n = expandNS syn n_in
1123 cargs <- many (pConstraintArg syn)
1124 iargs <- many (pImplicitArg syn)
1125 fc <- pfc
1126 args <- many (pArgExpr syn)
1127 wargs <- many (pWExpr syn)
1128 rhs <- pRHS syn n
1129 ist <- getState
1130 let ctxt = tt_ctxt ist
1131 let wsyn = syn { syn_namespace = [] }
1132 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1133 pop_indent
1134 return x,
1135 do pTerminator
1136 return ([], [])]
1137 let capp = PApp fc (PRef fc n)
1138 (iargs ++ cargs ++ map pexp args)
1139 ist <- getState
1140 setState (ist { lastParse = Just n })
1141 return $ PClause fc n capp wargs rhs wheres)
1142 <|> try (do push_indent
1143 wargs <- many1 (pWExpr syn)
1144 ist <- getState
1145 n <- case lastParse ist of
1146 Just t -> return t
1147 Nothing -> fail "Invalid clause"
1148 fc <- pfc
1149 rhs <- pRHS syn n
1150 let ctxt = tt_ctxt ist
1151 let wsyn = syn { syn_namespace = [] }
1152 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1153 pop_indent
1154 return x,
1155 do pTerminator
1156 return ([], [])]
1157 return $ PClauseR fc wargs rhs wheres)
1159 <|> try (do push_indent
1160 n_in <- pfName; let n = expandNS syn n_in
1161 cargs <- many (pConstraintArg syn)
1162 iargs <- many (pImplicitArg syn)
1163 fc <- pfc
1164 args <- many (pArgExpr syn)
1165 wargs <- many (pWExpr syn)
1166 let capp = PApp fc (PRef fc n)
1167 (iargs ++ cargs ++ map pexp args)
1168 reserved "with"
1169 wval <- pSimpleExpr syn
1170 open_block
1171 ds <- many1 $ pFunDecl syn
1172 let withs = map (fillLHSD n capp wargs) $ concat ds
1173 close_block
1174 ist <- getState
1175 setState (ist { lastParse = Just n })
1176 pop_indent
1177 return $ PWith fc n capp wargs wval withs)
1179 <|> try (do wargs <- many1 (pWExpr syn)
1180 fc <- pfc
1181 reserved "with"
1182 wval <- pSimpleExpr syn
1183 open_block
1184 ds <- many1 $ pFunDecl syn
1185 let withs = concat ds
1186 close_block
1187 return $ PWithR fc wargs wval withs)
1189 <|> do push_indent
1190 l <- pArgExpr syn
1191 op <- operator
1192 let n = expandNS syn (UN op)
1193 r <- pArgExpr syn
1194 fc <- pfc
1195 wargs <- many (pWExpr syn)
1196 rhs <- pRHS syn n
1197 let wsyn = syn { syn_namespace = [] }
1198 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1199 pop_indent
1200 return x,
1201 do pTerminator
1202 return ([], [])]
1203 ist <- getState
1204 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1205 setState (ist { lastParse = Just n })
1206 return $ PClause fc n capp wargs rhs wheres
1208 <|> do l <- pArgExpr syn
1209 op <- operator
1210 let n = expandNS syn (UN op)
1211 r <- pArgExpr syn
1212 fc <- pfc
1213 wargs <- many (pWExpr syn)
1214 reserved "with"
1215 wval <- pSimpleExpr syn
1216 open_block
1217 ds <- many1 $ pFunDecl syn
1218 close_block
1219 ist <- getState
1220 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1221 let withs = map (fillLHSD n capp wargs) $ concat ds
1222 setState (ist { lastParse = Just n })
1223 return $ PWith fc n capp wargs wval withs
1224 where
1225 fillLHS n capp owargs (PClauseR fc wargs v ws)
1226 = PClause fc n capp (owargs ++ wargs) v ws
1227 fillLHS n capp owargs (PWithR fc wargs v ws)
1228 = PWith fc n capp (owargs ++ wargs) v
1229 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1230 fillLHS _ _ _ c = c
1232 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1233 fillLHSD n c a x = x
1235pWExpr :: SyntaxInfo -> IParser PTerm
1236pWExpr syn = do lchar '|'; pExpr' syn
1238pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
1239pWhereblock n syn
1240 = do reserved "where"; open_block
1241 ds <- many1 $ pFunDecl syn
1242 let dns = concatMap (concatMap declared) ds
1243 close_block
1244 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1246pDirective :: IParser [PDecl]
1247pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;
1248 return [PDirective (do addLib lib
1249 addIBC (IBCLib lib))])
1250 <|> try (do lchar '%'; reserved "link"; obj <- strlit;
1251 return [PDirective (do datadir <- liftIO $ getDataDir
1252 o <- liftIO $ findInPath [".", datadir] obj
1253 addIBC (IBCObj o)
1254 addObjectFile o)])
1255 <|> try (do lchar '%'; reserved "include"; hdr <- strlit;
1256 return [PDirective (do addHdr hdr
1257 addIBC (IBCHeader hdr))])
1258 <|> try (do lchar '%'; reserved "hide"; n <- iName []
1259 return [PDirective (do setAccessibility n Hidden
1260 addIBC (IBCAccess n Hidden))])
1261 <|> try (do lchar '%'; reserved "freeze"; n <- iName []
1262 return [PDirective (do setAccessibility n Frozen
1263 addIBC (IBCAccess n Frozen))])
1264 <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'
1265 return [PDirective (do i <- getIState
1266 putIState (i { default_access = acc }))])
1267 <|> try (do lchar '%'; reserved "logging"; i <- natural;
1268 return [PDirective (setLogLevel (fromInteger i))])
1270pTactic :: SyntaxInfo -> IParser PTactic
1271pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
1272 return $ Intro ns
1273 <|> do reserved "intros"; return Intros
1274 <|> try (do reserved "refine"; n <- pName
1275 imps <- many1 imp
1276 return $ Refine n imps)
1277 <|> do reserved "refine"; n <- pName
1278 i <- getState
1279 return $ Refine n []
1280 <|> do reserved "rewrite"; t <- pExpr syn;
1281 i <- getState
1282 return $ Rewrite (desugar syn i t)
1283 <|> do reserved "let"; n <- pName; lchar '=';
1284 t <- pExpr syn;
1285 i <- getState
1286 return $ LetTac n (desugar syn i t)
1287 <|> do reserved "focus"; n <- pName
1288 return $ Focus n
1289 <|> do reserved "exact"; t <- pExpr syn;
1290 i <- getState
1291 return $ Exact (desugar syn i t)
1292 <|> do reserved "try"; t <- pTactic syn;
1293 lchar '|';
1294 t1 <- pTactic syn
1295 return $ Try t t1
1296 <|> do lchar '{'
1297 t <- pTactic syn;
1298 lchar ';';
1299 t1 <- pTactic syn;
1300 lchar '}'
1301 return $ TSeq t t1
1302 <|> do reserved "compute"; return Compute
1303 <|> do reserved "trivial"; return Trivial
1304 <|> do reserved "solve"; return Solve
1305 <|> do reserved "attack"; return Attack
1306 <|> do reserved "state"; return ProofState
1307 <|> do reserved "term"; return ProofTerm
1308 <|> do reserved "undo"; return Undo
1309 <|> do reserved "qed"; return Qed
1310 <|> do reserved "abandon"; return Abandon
1311 <|> do lchar ':'; reserved "q"; return Abandon
1312 where
1313 imp = do lchar '?'; return False
1314 <|> do lchar '_'; return True