git.iko.soy/Idris-dev
on 611dd97 help sign in
Idris-dev/src/Idris/Parser.hs
1406 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 iucheck
112 i <- getIState
113 addHides (hide_list i)
114 ok <- noErrors
115 when ok $
116 idrisCatch (do writeIBC f ibc; clearIBC)
117 (\c -> return ()) -- failure is harmless
118 i <- getIState
119 putIState (i { hide_list = [] })
120 return ()
121 where
122 namespaces [] ds = ds
123 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
125addHides :: [(Name, Maybe Accessibility)] -> Idris ()
126addHides xs = do i <- getIState
127 let defh = default_access i
128 let (hs, as) = partition isNothing xs
129 unless (null as) $
130 mapM_ doHide
131 (map (\ (n, _) -> (n, defh)) hs ++
132 map (\ (n, Just a) -> (n, a)) as)
133 where isNothing (_, Nothing) = True
134 isNothing _ = False
136 doHide (n, a) = do setAccessibility n a
137 addIBC (IBCAccess n a)
139parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"
140parseTac i = runParser (do t <- pTactic defaultSyntax
141 eof
142 return t) i "(proof)"
144iShowError fname err = let ln = sourceLine (errorPos err)
145 clm = sourceColumn (errorPos err)
146 msg = map messageString (errorMessages err) in
147 fname ++ ":" ++ show ln ++ ":parse error"
148 ++ " at column " ++ show clm -- ++ " with error:\n\t" ++ show msg
150parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)
151parseImports fname input
152 = do i <- get
153 case runParser (do whiteSpace
154 mname <- pHeader
155 ps <- many pImport
156 rest <- getInput
157 pos <- getPosition
158 return ((mname, ps, rest, pos), i)) i fname input of
159 Left err -> fail (iShowError fname err)
160 Right (x, i) -> do put i
161 return x
163pHeader :: IParser [String]
164pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')
165 return (parseName i))
166 <|> return []
167 where parseName x = case span (/='.') x of
168 (x, "") -> [x]
169 (x, '.':y) -> x : parseName y
171pushIndent :: IParser ()
172pushIndent = do pos <- getPosition
173 ist <- getState
174 setState (ist { indent_stack = sourceColumn pos :
175 indent_stack ist })
177lastIndent :: IParser Int
178lastIndent = do ist <- getState
179 case indent_stack ist of
180 (x : xs) -> return x
181 _ -> return 1
183indent :: IParser Int
184indent = liftM sourceColumn getPosition
186popIndent :: IParser ()
187popIndent = do ist <- getState
188 let (x : xs) = indent_stack ist
189 setState (ist { indent_stack = xs })
191openBlock :: IParser ()
192openBlock = do lchar '{'
193 ist <- getState
194 setState (ist { brace_stack = Nothing : brace_stack ist })
195 <|> do ist <- getState
196 lvl <- indent
197 setState (ist { brace_stack = Just lvl : brace_stack ist })
199closeBlock :: IParser ()
200closeBlock = do ist <- getState
201 bs <- case brace_stack ist of
202 Nothing : xs -> do lchar '}'
203 return xs
204 Just lvl : xs -> do i <- indent
205 inp <- getInput
206-- trace (show (take 10 inp, i, lvl)) $
207 if i >= lvl && take 1 inp /= ")"
208 then fail "Not end of block"
209 else return xs
210 setState (ist { brace_stack = bs })
212pTerminator = do lchar ';'; popIndent
213 <|> do c <- indent; l <- lastIndent
214 if c <= l
215 then popIndent
216 else fail "Not a terminator"
217 <|> do i <- getInput
218 if "}" `isPrefixOf` i || ")" `isPrefixOf` i
219 then popIndent
220 else fail "Not a terminator"
221 <|> lookAhead eof
223pBarTerminator
224 = do lchar '|'; return ()
225 <|> do c <- indent; l <- lastIndent
226 unless (c <= l) $ fail "Not a terminator"
227 <|> lookAhead eof
229pKeepTerminator
230 = do lchar ';'; return ()
231 <|> do c <- indent; l <- lastIndent
232 unless (c <= l) $ fail "Not a terminator"
233 <|> do i <- getInput
234 let h = take 1 i
235 unless (h `elem` ["}", ")", "|"]) $ fail "Not a terminator"
236 <|> lookAhead eof
238notEndApp = do c <- indent; l <- lastIndent
239 i <- getInput
240 when (c <= l) $ fail "Terminator"
242notEndBlock = do ist <- getState
243 case brace_stack ist of
244 Just lvl : xs -> do i <- indent
245 inp <- getInput
246 when (i < lvl || ")" `isPrefixOf` inp) $ fail "End of block"
247 _ -> return ()
249pfc :: IParser FC
250pfc = do s <- getPosition
251 let (dir, file) = splitFileName (sourceName s)
252 let f = case dir of
253 "./" -> file
254 _ -> sourceName s
255 return $ FC f (sourceLine s)
257pImport :: IParser String
258pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')
259 return (map dot f)
260 where dot '.' = '/'
261 dot c = c
263parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl]
264parseProg syn fname input pos
265 = do i <- get
266 case runParser (do setPosition pos
267 whiteSpace
268 ps <- many (pDecl syn)
269 eof
270 i' <- getState
271 return (concat ps, i')) i fname input of
272 Left err -> fail (iShowError fname err)
273 Right (x, i) -> do put i
274 return (collect x)
276-- Collect PClauses with the same function name
278collect :: [PDecl] -> [PDecl]
279collect (c@(PClauses _ o _ _) : ds)
280 = clauses (cname c) [] (c : ds)
281 where clauses n acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)
282 | n == n' = clauses n (PClause fc' n' l ws r (collect w) : acc) ds
283 clauses n acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds)
284 | n == n' = clauses n (PWith fc' n' l ws r (collect w) : acc) ds
285 clauses n acc xs = PClauses (getfc c) o n (reverse acc) : collect xs
287 cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = n
288 cname (PClauses fc _ _ [PWith _ n _ _ _ _]) = n
289 getfc (PClauses fc _ _ _) = fc
291collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
292collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds
293collect (PClass f s cs n ps ds : ds') = PClass f s cs n ps (collect ds) : collect ds'
294collect (PInstance f s cs n ps t en ds : ds')
295 = PInstance f s cs n ps t en (collect ds) : collect ds'
296collect (d : ds) = d : collect ds
297collect [] = []
299pFullExpr :: SyntaxInfo -> IParser PTerm
300pFullExpr syn
301 = do x <- pExpr syn; eof;
302 i <- getState
303 return $ desugar syn i x
305pDecl :: SyntaxInfo -> IParser [PDecl]
306pDecl syn = do notEndBlock
307 pDeclBody where
308 pDeclBody
309 = do d <- pDecl' syn
310 i <- getState
311 let d' = fmap (desugar syn i) d
312 return [d']
313 <|> pUsing syn
314 <|> pParams syn
315 <|> pNamespace syn
316 <|> pClass syn
317 <|> pInstance syn
318 <|> do d <- pDSL syn; return [d]
319 <|> pDirective
320 <|> try (do reserved "import"; fp <- identifier
321 fail "imports must be at the top of file")
323pFunDecl :: SyntaxInfo -> IParser [PDecl]
324pFunDecl syn
325 = try (do notEndBlock
326 d <- pFunDecl' syn
327 i <- getState
328 let d' = fmap (desugar syn i) d
329 return [d'])
331--------- Top Level Declarations ---------
333pDecl' :: SyntaxInfo -> IParser PDecl
334pDecl' syn
335 = try pFixity
336 <|> pFunDecl' syn
337 <|> try (pData syn)
338 <|> try (pRecord syn)
339 <|> pSyntaxDecl syn
341pSyntaxDecl :: SyntaxInfo -> IParser PDecl
342pSyntaxDecl syn
343 = do s <- pSyntaxRule syn
344 i <- getState
345 let rs = syntax_rules i
346 let ns = syntax_keywords i
347 let ibc = ibc_write i
348 let ks = map show (names s)
349 setState (i { syntax_rules = s : rs,
350 syntax_keywords = ks ++ ns,
351 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc
352 })
353 fc <- pfc
354 return (PSyntax fc s)
355 where
356 names (Rule syms _ _) = mapMaybe ename syms
357 ename (Keyword n) = Just n
358 ename _ = Nothing
360pSyntaxRule :: SyntaxInfo -> IParser Syntax
361pSyntaxRule syn
362 = do pushIndent
363 sty <- option AnySyntax (do reserved "term"; return TermSyntax
364 <|> do reserved "pattern"; return PatternSyntax)
365 reserved "syntax"
366 syms <- many1 pSynSym
367 when (all expr syms) $ fail "No keywords in syntax rule"
368 let ns = mapMaybe name syms
369 when (length ns /= length (nub ns))
370 $ fail "Repeated variable in syntax rule"
371 lchar '='
372 tm <- pExpr (impOK syn)
373 pTerminator
374 return (Rule (mkSimple syms) tm sty)
375 where
376 expr (Expr _) = True
377 expr _ = False
378 name (Expr n) = Just n
379 name _ = Nothing
381 -- Can't parse two full expressions (i.e. expressions with application) in a row
382 -- so change the first to a simple expression
384 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
385 mkSimple xs = mkSimple' xs
387 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : mkSimple' (Expr e1 : es)
388 mkSimple' (e : es) = e : mkSimple' es
389 mkSimple' [] = []
391pSynSym :: IParser SSymbol
392pSynSym = try (do lchar '['; n <- pName; lchar ']'
393 return (Expr n))
394 <|> try (do lchar '{'; n <- pName; lchar '}'
395 return (Binding n))
396 <|> do n <- iName []
397 return (Keyword n)
398 <|> do sym <- strlit
399 return (Symbol sym)
401pFunDecl' :: SyntaxInfo -> IParser PDecl
402pFunDecl' syn = try (do pushIndent
403 opts <- pFnOpts
404 acc <- pAccessibility
405 opts' <- pFnOpts
406 n_in <- pfName
407 let n = expandNS syn n_in
408 ty <- pTSig (impOK syn)
409 fc <- pfc
410 pTerminator
411-- ty' <- implicit syn n ty
412 addAcc n acc
413 return (PTy syn fc (opts ++ opts') n ty))
414 <|> try (pPattern syn)
415 <|> try (pCAF syn)
417pUsing :: SyntaxInfo -> IParser [PDecl]
418pUsing syn =
419 do reserved "using"; lchar '('; ns <- tyDeclList syn; lchar ')'
420 openBlock
421 let uvars = using syn
422 ds <- many1 (pDecl (syn { using = uvars ++ ns }))
423 closeBlock
424 return (concat ds)
426pParams :: SyntaxInfo -> IParser [PDecl]
427pParams syn =
428 do reserved "params"; lchar '('; ns <- tyDeclList syn; lchar ')'
429 lchar '{'
430 let pvars = syn_params syn
431 ds <- many1 (pDecl syn { syn_params = pvars ++ ns })
432 lchar '}'
433 fc <- pfc
434 return [PParams fc ns (concat ds)]
436pNamespace :: SyntaxInfo -> IParser [PDecl]
437pNamespace syn =
438 do reserved "namespace"; n <- identifier;
439 openBlock
440 ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
441 closeBlock
442 return [PNamespace n (concat ds)]
444--------- Fixity ---------
446pFixity :: IParser PDecl
447pFixity = do pushIndent
448 f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
449 pTerminator
450 let prec = fromInteger i
451 istate <- getState
452 let fs = map (Fix (f prec)) ops
453 setState (istate {
454 idris_infixes = nub $ sort (fs ++ idris_infixes istate),
455 ibc_write = map IBCFix fs ++ ibc_write istate })
456 fc <- pfc
457 return (PFix fc (f prec) ops)
459fixity :: IParser (Int -> Fixity)
460fixity = try (do reserved "infixl"; return Infixl)
461 <|> try (do reserved "infixr"; return Infixr)
462 <|> try (do reserved "infix"; return InfixN)
463 <|> try (do reserved "prefix"; return PrefixN)
465--------- Type classes ---------
467pClass :: SyntaxInfo -> IParser [PDecl]
468pClass syn = do acc <- pAccessibility
469 reserved "class"; fc <- pfc; cons <- pConstList syn; n_in <- pName
470 let n = expandNS syn n_in
471 cs <- many1 carg
472 reserved "where"; openBlock
473 ds <- many $ pFunDecl syn
474 closeBlock
475 let allDs = concat ds
476 accData acc n (concatMap declared allDs)
477 return [PClass syn fc cons n cs allDs]
478 where
479 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'
480 return (i, ty)
481 <|> do i <- pName;
482 return (i, PSet)
484pInstance :: SyntaxInfo -> IParser [PDecl]
485pInstance syn = do reserved "instance"; fc <- pfc
486 en <- option Nothing
487 (do lchar '['; n_in <- pfName; lchar ']'
488 let n = expandNS syn n_in
489 return (Just n))
490 cs <- pConstList syn
491 cn <- pName
492 args <- many1 (pSimpleExpr syn)
493 let sc = PApp fc (PRef fc cn) (map pexp args)
494 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
495 reserved "where"; openBlock
496 ds <- many $ pFunDecl syn
497 closeBlock
498 return [PInstance syn fc cs cn args t en (concat ds)]
500--------- Expressions ---------
502pExpr syn = do i <- getState
503 buildExpressionParser (table (idris_infixes i)) (pExpr' syn)
505pExpr' :: SyntaxInfo -> IParser PTerm
506pExpr' syn
507 = try (pExtExpr syn)
508 <|> pNoExtExpr syn
510pExtExpr :: SyntaxInfo -> IParser PTerm
511pExtExpr syn = do i <- getState
512 pExtensions syn (syntax_rules i)
514pSimpleExtExpr :: SyntaxInfo -> IParser PTerm
515pSimpleExtExpr syn = do i <- getState
516 pExtensions syn (filter simple (syntax_rules i))
517 where
518 simple (Rule (Expr x:xs) _ _) = False
519 simple (Rule (SimpleExpr x:xs) _ _) = False
520 simple (Rule [Keyword _] _ _) = True
521 simple (Rule [Symbol _] _ _) = True
522 simple (Rule (_:xs) _ _) = case last xs of
523 Keyword _ -> True
524 Symbol _ -> True
525 _ -> False
526 simple _ = False
528pNoExtExpr syn =
529 try (pApp syn)
530 <|> pRecordSet syn
531 <|> try (pSimpleExpr syn)
532 <|> pLambda syn
533 <|> pLet syn
534 <|> pPi syn
535 <|> pDoBlock syn
536 <|> pComprehension syn
538pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
539pExtensions syn rules = choice (map (try . pExt syn) (filter valid rules))
540 where
541 valid (Rule _ _ AnySyntax) = True
542 valid (Rule _ _ PatternSyntax) = inPattern syn
543 valid (Rule _ _ TermSyntax) = not (inPattern syn)
546data SynMatch = SynTm PTerm | SynBind Name
548pExt :: SyntaxInfo -> Syntax -> IParser PTerm
549pExt syn (Rule ssym ptm _)
550 = do smap <- mapM pSymbol ssym
551 let ns = mapMaybe id smap
552 return (update ns ptm) -- updated with smap
553 where
554 pSymbol (Keyword n) = do reserved (show n); return Nothing
555 pSymbol (Expr n) = do tm <- pExpr syn
556 return $ Just (n, SynTm tm)
557 pSymbol (SimpleExpr n) = do tm <- pSimpleExpr syn
558 return $ Just (n, SynTm tm)
559 pSymbol (Binding n) = do b <- pName
560 return $ Just (n, SynBind b)
561 pSymbol (Symbol s) = do symbol s
562 return Nothing
563 dropn n [] = []
564 dropn n ((x,t) : xs) | n == x = xs
565 | otherwise = (x,t):dropn n xs
567 updateB ns n = case lookup n ns of
568 Just (SynBind t) -> t
569 _ -> n
571 update ns (PRef fc n) = case lookup n ns of
572 Just (SynTm t) -> t
573 _ -> PRef fc n
574 update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)
575 update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc)
576 update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)
577 (update (dropn n ns) sc)
578 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
579 update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)
580 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)
581 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)
582 update ns (PAlternative a as) = PAlternative a (map (update ns) as)
583 update ns (PHidden t) = PHidden (update ns t)
584 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
585 where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
586 upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds
587 upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)
588 : upd (dropn n ns) ds
589 upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t)
590 : upd ns ds
591 upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)
592 : upd ns ds
593 update ns t = t
595pName = do i <- getState
596 iName (syntax_keywords i)
597 <|> do reserved "instance"
598 i <- getState
599 UN n <- iName (syntax_keywords i)
600 return (UN ('@':n))
602-- Parser for an operator in function position, i.e. enclosed by `()', with an
603-- optional namespace.
604pOpFront = maybeWithNS pOpFrontNoNS False []
605 where pOpFrontNoNS = do lchar '('; o <- operator; lchar ')'; return o
607pfName = try pOpFront
608 <|> pName
610pAccessibility' :: IParser Accessibility
611pAccessibility'
612 = do reserved "public"; return Public
613 <|> do reserved "abstract"; return Frozen
614 <|> do reserved "private"; return Hidden
616pAccessibility :: IParser (Maybe Accessibility)
617pAccessibility
618 = do acc <- pAccessibility'; return (Just acc)
619 <|> return Nothing
621pFnOpts :: IParser [FnOpt]
622pFnOpts = do reserved "total"; xs <- pFnOpts; return (TotalFn : xs)
623 <|> try (do lchar '%'; reserved "export"; c <- strlit; xs <- pFnOpts
624 return (CExport c : xs))
625 <|> do lchar '%'; reserved "assert_total"; xs <- pFnOpts; return (AssertTotal : xs)
626 <|> do lchar '%'; reserved "specialise";
627 lchar '['; ns <- sepBy pfName (lchar ','); lchar ']'
628 xs <- pFnOpts
629 return (Specialise ns : xs)
630 <|> return []
632addAcc :: Name -> Maybe Accessibility -> IParser ()
633addAcc n a = do i <- getState
634 setState (i { hide_list = (n, a) : hide_list i })
636pCaseExpr syn = do
637 reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
638 openBlock
639 pushIndent
640 opts <- many1 (do notEndBlock
641 x <- pCaseOpt syn
642 pKeepTerminator
643 return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
644 popIndent
645 closeBlock
646 return (PCase fc scr opts)
648pProofExpr syn = do
649 reserved "proof"; lchar '{'
650 ts <- endBy (pTactic syn) (lchar ';')
651 lchar '}'
652 return (PProof ts)
654pTacticsExpr syn = do
655 reserved "tactics"; lchar '{'
656 ts <- endBy (pTactic syn) (lchar ';')
657 lchar '}'
658 return (PTactics ts)
660pSimpleExpr syn =
661 try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t)
662 <|> do lchar '?'; x <- pName; return (PMetavar x)
663 <|> do reserved "refl"; fc <- pfc; return (PRefl fc)
664-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)
665 <|> pProofExpr syn
666 <|> pTacticsExpr syn
667 <|> pCaseExpr syn
668 <|> try (do x <- pfName
669 fc <- pfc
670 return (PRef fc x))
671 <|> try (pList syn)
672 <|> try (pAlt syn)
673 <|> try (pIdiom syn)
674 <|> try (do lchar '('
675 bracketed (noImp syn))
676 <|> try (do c <- pConstant
677 fc <- pfc
678 return (modifyConst syn fc (PConstant c)))
679 <|> do reserved "Set"; return PSet
680 <|> try (do symbol "()"
681 fc <- pfc
682 return (PTrue fc))
683 <|> try (do symbol "_|_"
684 fc <- pfc
685 return (PFalse fc))
686 <|> do lchar '_'; return Placeholder
687 <|> pSimpleExtExpr syn
689bracketed syn =
690 try (pPair syn)
691 <|> try (do e <- pExpr syn; lchar ')'; return e)
692-- <|> try (do reserved "typed"
693-- e <- pExpr syn; symbol ":"; t <- pExpr syn; lchar ')'
694-- return (PTyped e t))
695 <|> try (do fc <- pfc; o <- operator; e <- pExpr syn; lchar ')'
696 return $ PLam (MN 0 "x") Placeholder
697 (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 0 "x")),
698 pexp e]))
699 <|> try (do fc <- pfc; e <- pSimpleExpr syn; o <- operator; lchar ')'
700 return $ PLam (MN 0 "x") Placeholder
701 (PApp fc (PRef fc (UN o)) [pexp e,
702 pexp (PRef fc (MN 0 "x"))]))
704pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
705pCaseOpt syn = do lhs <- pExpr syn; symbol "=>"; rhs <- pExpr syn
706 return (lhs, rhs)
708modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
709modifyConst syn fc (PConstant (I x))
710 | not (inPattern syn)
711 = PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I x))]
712 | otherwise = PConstant (I x)
713modifyConst syn fc x = x
715pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']'
716 return (mkList fc xs)
717 where
718 mkList fc [] = PRef fc (UN "Nil")
719 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
721pPair syn = try (do l <- pExpr syn
722 fc <- pfc
723 rest <- restTuple
724 case rest of
725 [] -> return l
726 [Left r] -> return (PPair fc l r)
727 [Right r] -> return (PDPair fc l Placeholder r))
728 <|> try (do x <- ntuple
729 lchar ')'
730 return x)
731 <|> do ln <- pName; lchar ':'
732 lty <- pExpr syn
733 reservedOp "**"
734 fc <- pfc
735 r <- pExpr syn
736 lchar ')'
737 return (PDPair fc (PRef fc ln) lty r)
738 where
739 restTuple = do lchar ')'; return []
740 <|> do lchar ','
741 r <- pExpr syn
742 lchar ')'
743 return [Left r]
744 <|> do reservedOp "**"
745 r <- pExpr syn
746 lchar ')'
747 return [Right r]
748 ntuple = try (do l <- pExpr syn; fc <- pfc; lchar ','
749 rest <- ntuple
750 return (PPair fc l rest))
751 <|> (do l <- pExpr syn; fc <- pfc; lchar ','
752 r <- pExpr syn
753 return (PPair fc l r))
755pAlt syn = do symbol "(|"; alts <- sepBy1 (pExpr' syn) (lchar ','); symbol "|)"
756 return (PAlternative False alts)
758pHSimpleExpr syn
759 = do lchar '.'
760 e <- pSimpleExpr syn
761 return $ PHidden e
762 <|> pSimpleExpr syn
764pApp syn = do f <- pSimpleExpr syn
765 fc <- pfc
766 args <- many1 (do notEndApp
767 pArg syn)
768 i <- getState
769 return (dslify i $ PApp fc f args)
770 where
771 dslify i (PApp fc (PRef _ f) [a])
772 | [d] <- lookupCtxt Nothing f (idris_dsls i)
773 = desugar (syn { dsl_info = d }) i (getTm a)
774 dslify i t = t
776pArg :: SyntaxInfo -> IParser PArg
777pArg syn = try (pImplicitArg syn)
778 <|> try (pConstraintArg syn)
779 <|> do e <- pSimpleExpr syn
780 return (pexp e)
782pImplicitArg syn = do lchar '{'
783 n <- pName
784 fc <- pfc
785 v <- option (PRef fc n) (do lchar '='
786 pExpr syn)
787 lchar '}'
788 return (pimp n v)
790pConstraintArg syn = do symbol "@{"
791 e <- pExpr syn
792 symbol "}"
793 return (pconst e)
795pRecordSet syn
796 = do reserved "record"
797 lchar '{'
798 fields <- sepBy1 pFieldSet (lchar ',')
799 lchar '}'
800 fc <- pfc
801 rec <- option Nothing (do e <- pSimpleExpr syn
802 return (Just e))
803 case rec of
804 Nothing ->
805 return (PLam (MN 0 "fldx") Placeholder
806 (applyAll fc fields (PRef fc (MN 0 "fldx"))))
807 Just v -> return (applyAll fc fields v)
808 where pFieldSet = do n <- pfName
809 lchar '='
810 e <- pExpr syn
811 return (n, e)
812 applyAll fc [] x = x
813 applyAll fc ((n, e) : es) x
814 = applyAll fc es (PApp fc (PRef fc (mkSet n)) [pexp e, pexp x])
816mkSet (UN n) = UN ("set_" ++ n)
817mkSet (MN 0 n) = MN 0 ("set_" ++ n)
818mkSet (NS n s) = NS (mkSet n) s
820noImp syn = syn { implicitAllowed = False }
821impOK syn = syn { implicitAllowed = True }
823pTSig syn = do lchar ':'
824 cs <- if implicitAllowed syn then pConstList syn else return []
825 sc <- pExpr syn
826 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
828pLambda syn = do lchar '\\'
829 try (do xt <- tyOptDeclList syn
830 symbol "=>"
831 sc <- pExpr syn
832 return (bindList PLam xt sc)
833 <|> (do ps <- sepBy (do fc <- pfc
834 e <- pSimpleExpr syn
835 return (fc, e)) (lchar ',')
836 symbol "=>"
837 sc <- pExpr syn
838 return (pmList (zip [0..] ps) sc)))
839 where pmList [] sc = sc
840 pmList ((i, (fc, x)) : xs) sc
841 = PLam (MN i "lamp") Placeholder
842 (PCase fc (PRef fc (MN i "lamp"))
843 [(x, pmList xs sc)])
845pLet syn = try (do reserved "let"; n <- pName;
846 ty <- option Placeholder (do lchar ':'; pExpr' syn)
847 lchar '='
848 v <- pExpr syn
849 reserved "in"; sc <- pExpr syn
850 return (PLet n ty v sc))
851 <|> (do reserved "let"; fc <- pfc; pat <- pExpr' (syn { inPattern = True } )
852 symbol "="; v <- pExpr syn
853 reserved "in"; sc <- pExpr syn
854 return (PCase fc v [(pat, sc)]))
856pPi syn =
857 try (do lazy <- option False (do lchar '|'; return True)
858 st <- pStatic
859 lchar '('; xt <- tyDeclList syn; lchar ')'
860 symbol "->"
861 sc <- pExpr syn
862 return (bindList (PPi (Exp lazy st)) xt sc))
863 <|> try (if implicitAllowed syn
864 then do lazy <- option False (do lchar '|'
865 return True)
866 st <- pStatic
867 lchar '{'
868 xt <- tyDeclList syn
869 lchar '}'
870 symbol "->"
871 sc <- pExpr syn
872 return (bindList (PPi (Imp lazy st)) xt sc)
873 else fail "No implicit arguments allowed here")
874 <|> try (do lchar '{'
875 reserved "auto"
876 xt <- tyDeclList syn
877 lchar '}'
878 symbol "->"
879 sc <- pExpr syn
880 return (bindList (PPi (TacImp False Dynamic (PTactics [Trivial]))) xt sc))
881 <|> try (do lchar '{'
882 reserved "default"
883 script <- pSimpleExpr syn
884 xt <- tyDeclList syn
885 lchar '}'
886 symbol "->"
887 sc <- pExpr syn
888 return (bindList (PPi (TacImp False Dynamic script)) xt sc))
889 <|> do --lazy <- option False (do lchar '|'; return True)
890 lchar '{'
891 reserved "static"
892 lchar '}'
893 t <- pExpr' syn
894 symbol "->"
895 sc <- pExpr syn
896 return (PPi (Exp False Static) (MN 42 "__pi_arg") t sc)
898pConstList :: SyntaxInfo -> IParser [PTerm]
899pConstList syn = try (do lchar '('
900 tys <- sepBy1 (pExpr' (noImp syn)) (lchar ',')
901 lchar ')'
902 reservedOp "=>"
903 return tys)
904 <|> try (do t <- pExpr (noImp syn)
905 reservedOp "=>"
906 return [t])
907 <|> return []
909tyDeclList syn = try (sepBy1 (do x <- pfName
910 t <- pTSig (noImp syn)
911 return (x,t))
912 (lchar ','))
913 <|> do ns <- sepBy1 pName (lchar ',')
914 t <- pTSig (noImp syn)
915 return (map (\x -> (x, t)) ns)
917tyOptDeclList syn = sepBy1 (do x <- pfName;
918 t <- option Placeholder (do lchar ':'
919 pExpr syn)
920 return (x,t))
921 (lchar ',')
923bindList b [] sc = sc
924bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
926pComprehension syn
927 = do lchar '['
928 fc <- pfc
929 pat <- pExpr syn
930 lchar '|'
931 qs <- sepBy1 (pDo syn) (lchar ',')
932 lchar ']'
933 return (PDoBlock (map addGuard qs ++
934 [DoExp fc (PApp fc (PRef fc (UN "return"))
935 [pexp pat])]))
936 where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
937 [pexp e])
938 addGuard x = x
940pDoBlock syn
941 = do reserved "do"
942 openBlock
943 pushIndent
944 ds <- many1 (do notEndBlock
945 x <- pDo syn
946 pKeepTerminator
947 return x)
948 popIndent
949 closeBlock
950 return (PDoBlock ds)
952pDo syn
953 = try (do reserved "let"
954 i <- pName;
955 ty <- option Placeholder (do lchar ':'
956 pExpr' syn)
957 reservedOp "="
958 fc <- pfc
959 e <- pExpr syn
960 return (DoLet fc i ty e))
961 <|> try (do reserved "let"
962 i <- pExpr' syn
963 reservedOp "="
964 fc <- pfc
965 sc <- pExpr syn
966 return (DoLetP fc i sc))
967 <|> try (do i <- pName
968 symbol "<-"
969 fc <- pfc
970 e <- pExpr syn;
971 return (DoBind fc i e))
972 <|> try (do i <- pExpr' syn
973 symbol "<-"
974 fc <- pfc
975 e <- pExpr syn;
976 return (DoBindP fc i e))
977 <|> try (do e <- pExpr syn
978 fc <- pfc
979 return (DoExp fc e))
981pIdiom syn
982 = do symbol "[|"
983 fc <- pfc
984 e <- pExpr syn
985 symbol "|]"
986 return (PIdiom fc e)
988pConstant :: IParser Const
989pConstant = do reserved "Integer";return BIType
990 <|> do reserved "Int"; return IType
991 <|> do reserved "Char"; return ChType
992 <|> do reserved "Float"; return FlType
993 <|> do reserved "String"; return StrType
994 <|> do reserved "Ptr"; return PtrType
995 <|> try (do f <- float; return $ Fl f)
996-- <|> try (do i <- natural; lchar 'L'; return $ BI i)
997 <|> try (do i <- natural; return $ I (fromInteger i))
998 <|> try (do s <- strlit; return $ Str s)
999 <|> try (do c <- chlit; return $ Ch c)
1001pStatic :: IParser Static
1002pStatic = do lchar '['
1003 reserved "static"
1004 lchar ']';
1005 return Static
1006 <|> return Dynamic
1008table fixes
1009 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
1010 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]
1011 ++ toTable (reverse fixes) ++
1012 [[backtick],
1013 [binary "=" PEq AssocLeft],
1014 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
1016toTable fs = map (map toBin)
1017 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
1018 where toBin (Fix (PrefixN _) op) = prefix op
1019 (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
1020 toBin (Fix f op)
1021 = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
1022 assoc (Infixl _) = AssocLeft
1023 assoc (Infixr _) = AssocRight
1024 assoc (InfixN _) = AssocNone
1026binary name f = Infix (do reservedOp name
1027 fc <- pfc;
1028 return (f fc))
1029prefix name f = Prefix (do reservedOp name
1030 fc <- pfc;
1031 return (f fc))
1032backtick = Infix (do lchar '`'; n <- pfName
1033 lchar '`'
1034 fc <- pfc
1035 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
1037--------- Data declarations ---------
1039-- (works for classes too - 'abstract' means the data/class is visible but members not)
1040accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()
1041accData (Just Frozen) n ns = do addAcc n (Just Frozen)
1042 mapM_ (\n -> addAcc n (Just Hidden)) ns
1043accData a n ns = do addAcc n a
1044 mapM_ (`addAcc` a) ns
1046pRecord :: SyntaxInfo -> IParser PDecl
1047pRecord syn = do acc <- pAccessibility
1048 reserved "record"
1049 fc <- pfc
1050 tyn_in <- pfName
1051 ty <- pTSig (impOK syn)
1052 let tyn = expandNS syn tyn_in
1053 reserved "where"
1054 openBlock
1055 pushIndent
1056 (cn, cty, _) <- pConstructor syn
1057 pKeepTerminator
1058 popIndent
1059 closeBlock
1060 accData acc tyn [cn]
1061 let rsyn = syn { syn_namespace = show (nsroot tyn) :
1062 syn_namespace syn }
1063 let fns = getRecNames rsyn cty
1064 mapM_ (\n -> addAcc n (toFreeze acc)) fns
1065 return $ PRecord rsyn fc tyn ty cn cty
1066 where
1067 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkSet n)]
1068 ++ getRecNames syn sc
1069 getRecNames _ _ = []
1071 toFreeze (Just Frozen) = Just Hidden
1072 toFreeze x = x
1074pData :: SyntaxInfo -> IParser PDecl
1075pData syn = try (do acc <- pAccessibility
1076 reserved "data"
1077 fc <- pfc
1078 tyn_in <- pfName
1079 ty <- pTSig (impOK syn)
1080 let tyn = expandNS syn tyn_in
1081 reserved "where"
1082 openBlock
1083 pushIndent
1084 cons <- many (do notEndBlock
1085 c <- pConstructor syn
1086 pKeepTerminator
1087 return c) -- (lchar '|')
1088 popIndent
1089 closeBlock
1090 accData acc tyn (map (\ (n, _, _) -> n) cons)
1091 return $ PData syn fc (PDatadecl tyn ty cons))
1092 <|> try (do pushIndent
1093 acc <- pAccessibility
1094 reserved "data"
1095 fc <- pfc
1096 tyn_in <- pfName
1097 args <- many pName
1098 let tyn = expandNS syn tyn_in
1099 lchar '='
1100 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
1101 pTerminator
1102 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
1103 let ty = bindArgs (map (const PSet) args) PSet
1104 cons' <- mapM (\ (x, cargs, cfc) ->
1105 do let cty = bindArgs cargs conty
1106 return (x, cty, cfc)) cons
1107 accData acc tyn (map (\ (n, _, _) -> n) cons')
1108 return $ PData syn fc (PDatadecl tyn ty cons'))
1109 where
1110 mkPApp fc t [] = t
1111 mkPApp fc t xs = PApp fc t (map pexp xs)
1113bindArgs :: [PTerm] -> PTerm -> PTerm
1114bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
1116pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)
1117pConstructor syn
1118 = do cn_in <- pfName; fc <- pfc
1119 let cn = expandNS syn cn_in
1120 ty <- pTSig (impOK syn)
1121-- ty' <- implicit syn cn ty
1122 return (cn, ty, fc)
1125pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm], FC)
1126pSimpleCon syn
1127 = do cn_in <- pfName
1128 let cn = expandNS syn cn_in
1129 fc <- pfc
1130 args <- many (do notEndApp
1131 pSimpleExpr syn)
1132 return (cn, args, fc)
1134--------- DSL syntax overloading ---------
1136pDSL :: SyntaxInfo -> IParser PDecl
1137pDSL syn = do reserved "dsl"
1138 n <- pfName
1139 openBlock
1140 pushIndent
1141 bs <- many1 (do notEndBlock
1142 b <- pOverload syn
1143 pKeepTerminator
1144 return b)
1145 popIndent; closeBlock
1146 let dsl = mkDSL bs (dsl_info syn)
1147 checkDSL dsl
1148 i <- getState
1149 setState (i { idris_dsls = addDef n dsl (idris_dsls i) })
1150 return (PDSL n dsl)
1151 where mkDSL bs dsl = let var = lookup "variable" bs
1152 first = lookup "index_first" bs
1153 next = lookup "index_next" bs
1154 leto = lookup "let" bs
1155 lambda = lookup "lambda" bs in
1156 initDSL { dsl_var = var,
1157 index_first = first,
1158 index_next = next,
1159 dsl_lambda = lambda,
1160 dsl_let = leto }
1162checkDSL :: DSL -> IParser ()
1163checkDSL dsl = return ()
1165pOverload :: SyntaxInfo -> IParser (String, PTerm)
1166pOverload syn = do o <- identifier <|> do reserved "let"
1167 return "let"
1168 if o `notElem` overloadable
1169 then fail $ show o ++ " is not an overloading"
1170 else do
1171 lchar '='
1172 t <- pExpr syn
1173 return (o, t)
1174 where overloadable = ["let","lambda","index_first","index_next","variable"]
1176--------- Pattern match clauses ---------
1178pPattern :: SyntaxInfo -> IParser PDecl
1179pPattern syn = do fc <- pfc
1180 clause <- pClause syn
1181 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
1183pCAF :: SyntaxInfo -> IParser PDecl
1184pCAF syn = do reserved "let"
1185 n_in <- pfName; let n = expandNS syn n_in
1186 lchar '='
1187 t <- pExpr syn
1188 pTerminator
1189 fc <- pfc
1190 return (PCAF fc n t)
1192pArgExpr syn = let syn' = syn { inPattern = True } in
1193 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
1195pRHS :: SyntaxInfo -> Name -> IParser PTerm
1196pRHS syn n = do lchar '='; pExpr syn
1197 <|> do symbol "?="; rhs <- pExpr syn;
1198 return (addLet rhs)
1199 <|> do reserved "impossible"; return PImpossible
1200 where mkN (UN x) = UN (x++"_lemma_1")
1201 mkN (NS x n) = NS (mkN x) n
1202 n' = mkN n
1204 addLet (PLet n ty val rhs) = PLet n ty val (addLet rhs)
1205 addLet (PCase fc t cs) = PCase fc t (map addLetC cs)
1206 where addLetC (l, r) = (l, addLet r)
1207 addLet rhs = (PLet (UN "value") Placeholder rhs (PMetavar n'))
1209pClause :: SyntaxInfo -> IParser PClause
1210pClause syn
1211 = try (do pushIndent
1212 n_in <- pfName; let n = expandNS syn n_in
1213 cargs <- many (pConstraintArg syn)
1214 iargs <- many (pImplicitArg syn)
1215 fc <- pfc
1216 args <- many (pArgExpr syn)
1217 wargs <- many (pWExpr syn)
1218 rhs <- pRHS syn n
1219 ist <- getState
1220 let ctxt = tt_ctxt ist
1221 let wsyn = syn { syn_namespace = [] }
1222 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1223 popIndent
1224 return x,
1225 do pTerminator
1226 return ([], [])]
1227 let capp = PApp fc (PRef fc n)
1228 (iargs ++ cargs ++ map pexp args)
1229 ist <- getState
1230 setState (ist { lastParse = Just n })
1231 return $ PClause fc n capp wargs rhs wheres)
1232 <|> try (do pushIndent
1233 wargs <- many1 (pWExpr syn)
1234 ist <- getState
1235 n <- case lastParse ist of
1236 Just t -> return t
1237 Nothing -> fail "Invalid clause"
1238 fc <- pfc
1239 rhs <- pRHS syn n
1240 let ctxt = tt_ctxt ist
1241 let wsyn = syn { syn_namespace = [] }
1242 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1243 popIndent
1244 return x,
1245 do pTerminator
1246 return ([], [])]
1247 return $ PClauseR fc wargs rhs wheres)
1249 <|> try (do pushIndent
1250 n_in <- pfName; let n = expandNS syn n_in
1251 cargs <- many (pConstraintArg syn)
1252 iargs <- many (pImplicitArg syn)
1253 fc <- pfc
1254 args <- many (pArgExpr syn)
1255 wargs <- many (pWExpr syn)
1256 let capp = PApp fc (PRef fc n)
1257 (iargs ++ cargs ++ map pexp args)
1258 ist <- getState
1259 setState (ist { lastParse = Just n })
1260 reserved "with"
1261 wval <- pSimpleExpr syn
1262 openBlock
1263 ds <- many1 $ pFunDecl syn
1264 let withs = map (fillLHSD n capp wargs) $ concat ds
1265 closeBlock
1266 popIndent
1267 return $ PWith fc n capp wargs wval withs)
1269 <|> try (do wargs <- many1 (pWExpr syn)
1270 fc <- pfc
1271 reserved "with"
1272 wval <- pSimpleExpr syn
1273 openBlock
1274 ds <- many1 $ pFunDecl syn
1275 let withs = concat ds
1276 closeBlock
1277 return $ PWithR fc wargs wval withs)
1279 <|> do pushIndent
1280 l <- pArgExpr syn
1281 op <- operator
1282 let n = expandNS syn (UN op)
1283 r <- pArgExpr syn
1284 fc <- pfc
1285 wargs <- many (pWExpr syn)
1286 rhs <- pRHS syn n
1287 let wsyn = syn { syn_namespace = [] }
1288 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1289 popIndent
1290 return x,
1291 do pTerminator
1292 return ([], [])]
1293 ist <- getState
1294 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1295 setState (ist { lastParse = Just n })
1296 return $ PClause fc n capp wargs rhs wheres
1298 <|> do l <- pArgExpr syn
1299 op <- operator
1300 let n = expandNS syn (UN op)
1301 r <- pArgExpr syn
1302 fc <- pfc
1303 wargs <- many (pWExpr syn)
1304 reserved "with"
1305 wval <- pSimpleExpr syn
1306 openBlock
1307 ds <- many1 $ pFunDecl syn
1308 closeBlock
1309 ist <- getState
1310 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1311 let withs = map (fillLHSD n capp wargs) $ concat ds
1312 setState (ist { lastParse = Just n })
1313 return $ PWith fc n capp wargs wval withs
1314 where
1315 fillLHS n capp owargs (PClauseR fc wargs v ws)
1316 = PClause fc n capp (owargs ++ wargs) v ws
1317 fillLHS n capp owargs (PWithR fc wargs v ws)
1318 = PWith fc n capp (owargs ++ wargs) v
1319 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1320 fillLHS _ _ _ c = c
1322 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1323 fillLHSD n c a x = x
1325pWExpr :: SyntaxInfo -> IParser PTerm
1326pWExpr syn = do lchar '|'
1327 pExpr' syn
1329pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
1330pWhereblock n syn
1331 = do reserved "where"; openBlock
1332 ds <- many1 $ pFunDecl syn
1333 let dns = concatMap (concatMap declared) ds
1334 closeBlock
1335 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1337pDirective :: IParser [PDecl]
1338pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;
1339 return [PDirective (do addLib lib
1340 addIBC (IBCLib lib))])
1341 <|> try (do lchar '%'; reserved "link"; obj <- strlit;
1342 return [PDirective (do datadir <- liftIO getDataDir
1343 o <- liftIO $ findInPath [".", datadir] obj
1344 addIBC (IBCObj o)
1345 addObjectFile o)])
1346 <|> try (do lchar '%'; reserved "include"; hdr <- strlit;
1347 return [PDirective (do addHdr hdr
1348 addIBC (IBCHeader hdr))])
1349 <|> try (do lchar '%'; reserved "hide"; n <- iName []
1350 return [PDirective (do setAccessibility n Hidden
1351 addIBC (IBCAccess n Hidden))])
1352 <|> try (do lchar '%'; reserved "freeze"; n <- iName []
1353 return [PDirective (do setAccessibility n Frozen
1354 addIBC (IBCAccess n Frozen))])
1355 <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'
1356 return [PDirective (do i <- getIState
1357 putIState (i { default_access = acc }))])
1358 <|> try (do lchar '%'; reserved "logging"; i <- natural;
1359 return [PDirective (setLogLevel (fromInteger i))])
1361pTactic :: SyntaxInfo -> IParser PTactic
1362pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
1363 return $ Intro ns
1364 <|> do reserved "intros"; return Intros
1365 <|> try (do reserved "refine"; n <- pName
1366 imps <- many1 imp
1367 return $ Refine n imps)
1368 <|> do reserved "refine"; n <- pName
1369 i <- getState
1370 return $ Refine n []
1371 <|> do reserved "rewrite"; t <- pExpr syn;
1372 i <- getState
1373 return $ Rewrite (desugar syn i t)
1374 <|> do reserved "let"; n <- pName; lchar '=';
1375 t <- pExpr syn;
1376 i <- getState
1377 return $ LetTac n (desugar syn i t)
1378 <|> do reserved "focus"; n <- pName
1379 return $ Focus n
1380 <|> do reserved "exact"; t <- pExpr syn;
1381 i <- getState
1382 return $ Exact (desugar syn i t)
1383 <|> do reserved "try"; t <- pTactic syn;
1384 lchar '|';
1385 t1 <- pTactic syn
1386 return $ Try t t1
1387 <|> do lchar '{'
1388 t <- pTactic syn;
1389 lchar ';';
1390 t1 <- pTactic syn;
1391 lchar '}'
1392 return $ TSeq t t1
1393 <|> do reserved "compute"; return Compute
1394 <|> do reserved "trivial"; return Trivial
1395 <|> do reserved "solve"; return Solve
1396 <|> do reserved "attack"; return Attack
1397 <|> do reserved "state"; return ProofState
1398 <|> do reserved "term"; return ProofTerm
1399 <|> do reserved "undo"; return Undo
1400 <|> do reserved "qed"; return Qed
1401 <|> do reserved "abandon"; return Abandon
1402 <|> do lchar ':'; reserved "q"; return Abandon
1403 where
1404 imp = do lchar '?'; return False
1405 <|> do lchar '_'; return True