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