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