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