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