git.iko.soy/Idris-dev
on 0417eae help sign in
Idris-dev/src/Idris/Parser.hs
1530 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 <|> pRecordType 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)
882pRecordType syn
883 = do reserved "record"
884 lchar '{'
885 fields <- sepBy1 pFieldType (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 pFieldType = 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 (mkType n)) [pexp e, pexp x])
903mkType (UN n) = UN ("set_" ++ n)
904mkType (MN 0 n) = MN 0 ("set_" ++ n)
905mkType (NS n s) = NS (mkType 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 "Bits8"; return B8Type
1085 <|> do reserved "Bits16"; return B16Type
1086 <|> do reserved "Bits32"; return B32Type
1087 <|> do reserved "Bits64"; return B64Type
1088 <|> try (do f <- float; return $ Fl f)
1089-- <|> try (do i <- natural; lchar 'L'; return $ BI i)
1090 <|> try (do i <- natural; return $ I (fromInteger i))
1091 <|> try (do s <- strlit; return $ Str s)
1092 <|> try (do c <- chlit; return $ Ch c)
1094pStatic :: IParser Static
1095pStatic = do lchar '['
1096 reserved "static"
1097 lchar ']';
1098 return Static
1099 <|> return Dynamic
1101table fixes
1102 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
1103 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]
1104 ++ toTable (reverse fixes) ++
1105 [[backtick],
1106 [binary "=" PEq AssocLeft],
1107 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
1109toTable fs = map (map toBin)
1110 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
1111 where toBin (Fix (PrefixN _) op) = prefix op
1112 (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
1113 toBin (Fix f op)
1114 = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
1115 assoc (Infixl _) = AssocLeft
1116 assoc (Infixr _) = AssocRight
1117 assoc (InfixN _) = AssocNone
1119binary name f = Infix (do reservedOp name
1120 fc <- pfc;
1121 doc <- option "" (pDocComment '^')
1122 return (f fc))
1123prefix name f = Prefix (do reservedOp name
1124 fc <- pfc;
1125 return (f fc))
1126backtick = Infix (do lchar '`'; n <- pfName
1127 lchar '`'
1128 fc <- pfc
1129 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
1131--------- Data declarations ---------
1133-- (works for classes too - 'abstract' means the data/class is visible but members not)
1134accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()
1135accData (Just Frozen) n ns = do addAcc n (Just Frozen)
1136 mapM_ (\n -> addAcc n (Just Hidden)) ns
1137accData a n ns = do addAcc n a
1138 mapM_ (`addAcc` a) ns
1140pRecord :: SyntaxInfo -> IParser PDecl
1141pRecord syn = do doc <- option "" (pDocComment '|')
1142 acc <- pAccessibility
1143 reserved "record"
1144 fc <- pfc
1145 tyn_in <- pfName
1146 ty <- pTSig (impOK syn)
1147 let tyn = expandNS syn tyn_in
1148 reserved "where"
1149 openBlock
1150 pushIndent
1151 (cdoc, cn, cty, _) <- pConstructor syn
1152 pKeepTerminator
1153 popIndent
1154 closeBlock
1155 accData acc tyn [cn]
1156 let rsyn = syn { syn_namespace = show (nsroot tyn) :
1157 syn_namespace syn }
1158 let fns = getRecNames rsyn cty
1159 mapM_ (\n -> addAcc n acc) fns
1160 return $ PRecord doc rsyn fc tyn ty cdoc cn cty
1161 where
1162 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
1163 ++ getRecNames syn sc
1164 getRecNames _ _ = []
1166 toFreeze (Just Frozen) = Just Hidden
1167 toFreeze x = x
1169pDataI = do reserved "data"; return False
1170 <|> do reserved "codata"; return True
1172pData :: SyntaxInfo -> IParser PDecl
1173pData syn = try (do doc <- option "" (pDocComment '|')
1174 acc <- pAccessibility
1175 co <- pDataI
1176 fc <- pfc
1177 tyn_in <- pfName
1178 ty <- pTSig (impOK syn)
1179 let tyn = expandNS syn tyn_in
1180 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1181 reserved "where"
1182 openBlock
1183 pushIndent
1184 cons <- many (do notEndBlock
1185 c <- pConstructor syn
1186 pKeepTerminator
1187 return c) -- (lchar '|')
1188 popIndent
1189 closeBlock
1190 accData acc tyn (map (\ (_, n, _, _) -> n) cons)
1191 return $ PData doc syn fc co (PDatadecl tyn ty cons)))
1192 <|> try (do doc <- option "" (pDocComment '|')
1193 pushIndent
1194 acc <- pAccessibility
1195 co <- pDataI
1196 fc <- pfc
1197 tyn_in <- pfName
1198 args <- many pName
1199 let ty = bindArgs (map (const PType) args) PType
1200 let tyn = expandNS syn tyn_in
1201 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1202 try (lchar '=') <|> do reserved "where"
1203 let kw = (if co then "co" else "") ++ "data "
1204 let n = show tyn_in ++ " "
1205 let s = kw ++ n
1206 let as = concat (intersperse " " $ map show args) ++ " "
1207 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
1208 let ss = concat (intersperse " -> " $ map (const "Type") args)
1209 let fix1 = s ++ as ++ " = ..."
1210 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
1211 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
1212 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
1214 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
1215 pTerminator
1216 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
1217 cons' <- mapM (\ (doc, x, cargs, cfc) ->
1218 do let cty = bindArgs cargs conty
1219 return (doc, x, cty, cfc)) cons
1220 accData acc tyn (map (\ (_, n, _, _) -> n) cons')
1221 return $ PData doc syn fc co (PDatadecl tyn ty cons')))
1222 where
1223 mkPApp fc t [] = t
1224 mkPApp fc t xs = PApp fc t (map pexp xs)
1226bindArgs :: [PTerm] -> PTerm -> PTerm
1227bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
1229pConstructor :: SyntaxInfo -> IParser (String, Name, PTerm, FC)
1230pConstructor syn
1231 = do doc <- option "" (pDocComment '|')
1232 cn_in <- pfName; fc <- pfc
1233 let cn = expandNS syn cn_in
1234 ty <- pTSig (impOK syn)
1235-- ty' <- implicit syn cn ty
1236 return (doc, cn, ty, fc)
1239pSimpleCon :: SyntaxInfo -> IParser (String, Name, [PTerm], FC)
1240pSimpleCon syn
1241 = do cn_in <- pfName
1242 let cn = expandNS syn cn_in
1243 fc <- pfc
1244 args <- many (do notEndApp
1245 pSimpleExpr syn)
1246 doc <- option "" (pDocComment '^')
1247 return (doc, cn, args, fc)
1249--------- DSL syntax overloading ---------
1251pDSL :: SyntaxInfo -> IParser PDecl
1252pDSL syn = do reserved "dsl"
1253 n <- pfName
1254 openBlock
1255 pushIndent
1256 bs <- many1 (do notEndBlock
1257 b <- pOverload syn
1258 pKeepTerminator
1259 return b)
1260 popIndent; closeBlock
1261 let dsl = mkDSL bs (dsl_info syn)
1262 checkDSL dsl
1263 i <- getState
1264 setState (i { idris_dsls = addDef n dsl (idris_dsls i) })
1265 return (PDSL n dsl)
1266 where mkDSL bs dsl = let var = lookup "variable" bs
1267 first = lookup "index_first" bs
1268 next = lookup "index_next" bs
1269 leto = lookup "let" bs
1270 lambda = lookup "lambda" bs in
1271 initDSL { dsl_var = var,
1272 index_first = first,
1273 index_next = next,
1274 dsl_lambda = lambda,
1275 dsl_let = leto }
1277checkDSL :: DSL -> IParser ()
1278checkDSL dsl = return ()
1280pOverload :: SyntaxInfo -> IParser (String, PTerm)
1281pOverload syn = do o <- identifier <|> do reserved "let"
1282 return "let"
1283 if o `notElem` overloadable
1284 then fail $ show o ++ " is not an overloading"
1285 else do
1286 lchar '='
1287 t <- pExpr syn
1288 return (o, t)
1289 where overloadable = ["let","lambda","index_first","index_next","variable"]
1291--------- Pattern match clauses ---------
1293pPattern :: SyntaxInfo -> IParser PDecl
1294pPattern syn = do fc <- pfc
1295 clause <- pClause syn
1296 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
1298pCAF :: SyntaxInfo -> IParser PDecl
1299pCAF syn = do reserved "let"
1300 n_in <- pfName; let n = expandNS syn n_in
1301 lchar '='
1302 t <- pExpr syn
1303 pTerminator
1304 fc <- pfc
1305 return (PCAF fc n t)
1307pArgExpr syn = let syn' = syn { inPattern = True } in
1308 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
1310pRHS :: SyntaxInfo -> Name -> IParser PTerm
1311pRHS syn n = do lchar '='; pExpr syn
1312 <|> do symbol "?="; rhs <- pExpr syn;
1313 return (addLet rhs)
1314 <|> do reserved "impossible"; return PImpossible
1315 where mkN (UN x) = UN (x++"_lemma_1")
1316 mkN (NS x n) = NS (mkN x) n
1317 n' = mkN n
1319 addLet (PLet n ty val rhs) = PLet n ty val (addLet rhs)
1320 addLet (PCase fc t cs) = PCase fc t (map addLetC cs)
1321 where addLetC (l, r) = (l, addLet r)
1322 addLet rhs = (PLet (UN "value") Placeholder rhs (PMetavar n'))
1324pClause :: SyntaxInfo -> IParser PClause
1325pClause syn
1326 = try (do pushIndent
1327 n_in <- pfName; let n = expandNS syn n_in
1328 cargs <- many (pConstraintArg syn)
1329 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1330 fc <- pfc
1331 args <- many (pArgExpr syn)
1332 wargs <- many (pWExpr syn)
1333 rhs <- pRHS syn n
1334 ist <- getState
1335 let ctxt = tt_ctxt ist
1336 let wsyn = syn { syn_namespace = [] }
1337 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1338 popIndent
1339 return x,
1340 do pTerminator
1341 return ([], [])]
1342 let capp = PApp fc (PRef fc n)
1343 (iargs ++ cargs ++ map pexp args)
1344 ist <- getState
1345 setState (ist { lastParse = Just n })
1346 return $ PClause fc n capp wargs rhs wheres)
1347 <|> try (do pushIndent
1348 wargs <- many1 (pWExpr syn)
1349 ist <- getState
1350 n <- case lastParse ist of
1351 Just t -> return t
1352 Nothing -> fail "Invalid clause"
1353 fc <- pfc
1354 rhs <- pRHS syn n
1355 let ctxt = tt_ctxt ist
1356 let wsyn = syn { syn_namespace = [] }
1357 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1358 popIndent
1359 return x,
1360 do pTerminator
1361 return ([], [])]
1362 return $ PClauseR fc wargs rhs wheres)
1364 <|> try (do pushIndent
1365 n_in <- pfName; let n = expandNS syn n_in
1366 cargs <- many (pConstraintArg syn)
1367 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1368 fc <- pfc
1369 args <- many (pArgExpr syn)
1370 wargs <- many (pWExpr syn)
1371 let capp = PApp fc (PRef fc n)
1372 (iargs ++ cargs ++ map pexp args)
1373 ist <- getState
1374 setState (ist { lastParse = Just n })
1375 reserved "with"
1376 wval <- pSimpleExpr syn
1377 openBlock
1378 ds <- many1 $ pFunDecl syn
1379 let withs = map (fillLHSD n capp wargs) $ concat ds
1380 closeBlock
1381 popIndent
1382 return $ PWith fc n capp wargs wval withs)
1384 <|> try (do wargs <- many1 (pWExpr syn)
1385 fc <- pfc
1386 reserved "with"
1387 wval <- pSimpleExpr syn
1388 openBlock
1389 ds <- many1 $ pFunDecl syn
1390 let withs = concat ds
1391 closeBlock
1392 return $ PWithR fc wargs wval withs)
1394 <|> do pushIndent
1395 l <- pArgExpr syn
1396 op <- operator
1397 let n = expandNS syn (UN op)
1398 r <- pArgExpr syn
1399 fc <- pfc
1400 wargs <- many (pWExpr syn)
1401 rhs <- pRHS syn n
1402 let wsyn = syn { syn_namespace = [] }
1403 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1404 popIndent
1405 return x,
1406 do pTerminator
1407 return ([], [])]
1408 ist <- getState
1409 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1410 setState (ist { lastParse = Just n })
1411 return $ PClause fc n capp wargs rhs wheres
1413 <|> do l <- pArgExpr syn
1414 op <- operator
1415 let n = expandNS syn (UN op)
1416 r <- pArgExpr syn
1417 fc <- pfc
1418 wargs <- many (pWExpr syn)
1419 reserved "with"
1420 wval <- pSimpleExpr syn
1421 openBlock
1422 ds <- many1 $ pFunDecl syn
1423 closeBlock
1424 ist <- getState
1425 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1426 let withs = map (fillLHSD n capp wargs) $ concat ds
1427 setState (ist { lastParse = Just n })
1428 return $ PWith fc n capp wargs wval withs
1429 where
1430 fillLHS n capp owargs (PClauseR fc wargs v ws)
1431 = PClause fc n capp (owargs ++ wargs) v ws
1432 fillLHS n capp owargs (PWithR fc wargs v ws)
1433 = PWith fc n capp (owargs ++ wargs) v
1434 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1435 fillLHS _ _ _ c = c
1437 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1438 fillLHSD n c a x = x
1440pWExpr :: SyntaxInfo -> IParser PTerm
1441pWExpr syn = do lchar '|'
1442 pExpr' syn
1444pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
1445pWhereblock n syn
1446 = do reserved "where"; openBlock
1447 ds <- many1 $ pDecl syn
1448 let dns = concatMap (concatMap declared) ds
1449 closeBlock
1450 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1452pDirective :: IParser [PDecl]
1453pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;
1454 return [PDirective (do addLib lib
1455 addIBC (IBCLib lib))])
1456 <|> try (do lchar '%'; reserved "link"; obj <- strlit;
1457 return [PDirective (do datadir <- liftIO getDataDir
1458 o <- liftIO $ findInPath [".", datadir] obj
1459 addIBC (IBCObj o)
1460 addObjectFile o)])
1461 <|> try (do lchar '%'; reserved "include"; hdr <- strlit;
1462 return [PDirective (do addHdr hdr
1463 addIBC (IBCHeader hdr))])
1464 <|> try (do lchar '%'; reserved "hide"; n <- iName []
1465 return [PDirective (do setAccessibility n Hidden
1466 addIBC (IBCAccess n Hidden))])
1467 <|> try (do lchar '%'; reserved "freeze"; n <- iName []
1468 return [PDirective (do setAccessibility n Frozen
1469 addIBC (IBCAccess n Frozen))])
1470 <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'
1471 return [PDirective (do i <- getIState
1472 putIState (i { default_access = acc }))])
1473 <|> try (do lchar '%'; reserved "default"; tot <- pTotality
1474 i <- getState
1475 setState (i { default_total = tot } )
1476 return [PDirective (do i <- getIState
1477 putIState (i { default_total = tot }))])
1478 <|> try (do lchar '%'; reserved "logging"; i <- natural;
1479 return [PDirective (setLogLevel (fromInteger i))])
1481pTactic :: SyntaxInfo -> IParser PTactic
1482pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
1483 return $ Intro ns
1484 <|> do reserved "intros"; return Intros
1485 <|> try (do reserved "refine"; n <- pName
1486 imps <- many1 imp
1487 return $ Refine n imps)
1488 <|> do reserved "refine"; n <- pName
1489 i <- getState
1490 return $ Refine n []
1491 <|> do reserved "rewrite"; t <- pExpr syn;
1492 i <- getState
1493 return $ Rewrite (desugar syn i t)
1494 <|> try (do reserved "let"; n <- pName; lchar ':';
1495 ty <- pExpr' syn; lchar '='; t <- pExpr syn;
1496 i <- getState
1497 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
1498 <|> try (do reserved "let"; n <- pName; lchar '=';
1499 t <- pExpr syn;
1500 i <- getState
1501 return $ LetTac n (desugar syn i t))
1502 <|> do reserved "focus"; n <- pName
1503 return $ Focus n
1504 <|> do reserved "exact"; t <- pExpr syn;
1505 i <- getState
1506 return $ Exact (desugar syn i t)
1507 <|> do reserved "try"; t <- pTactic syn;
1508 lchar '|';
1509 t1 <- pTactic syn
1510 return $ Try t t1
1511 <|> do lchar '{'
1512 t <- pTactic syn;
1513 lchar ';';
1514 t1 <- pTactic syn;
1515 lchar '}'
1516 return $ TSeq t t1
1517 <|> do reserved "compute"; return Compute
1518 <|> do reserved "trivial"; return Trivial
1519 <|> do reserved "solve"; return Solve
1520 <|> do reserved "attack"; return Attack
1521 <|> do reserved "state"; return ProofState
1522 <|> do reserved "term"; return ProofTerm
1523 <|> do reserved "undo"; return Undo
1524 <|> do reserved "qed"; return Qed
1525 <|> do reserved "abandon"; return Abandon
1526 <|> do lchar ':'; reserved "q"; return Abandon
1527 where
1528 imp = do lchar '?'; return False
1529 <|> do lchar '_'; return True