git.iko.soy/Idris-dev
on 60dbc48 help sign in
Idris-dev/src/Idris/Parser.hs
1529 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 lchar '%'; fc <- pfc; reserved "instance"; return (PResolveTC fc)
742 <|> do reserved "refl"; fc <- pfc;
743 tm <- option Placeholder (do lchar '{'; t <- pExpr syn; lchar '}';
744 return t)
745 return (PRefl fc tm)
746-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)
747 <|> pProofExpr syn
748 <|> pTacticsExpr syn
749 <|> pCaseExpr syn
750 <|> try (do x <- pfName
751 fc <- pfc
752 return (PRef fc x))
753 <|> try (do lchar '!'; x <- pfName
754 fc <- pfc
755 return (PInferRef fc x))
756 <|> try (pList syn)
757 <|> try (pAlt syn)
758 <|> try (pIdiom syn)
759 <|> try (do lchar '('
760 bracketed (noImp syn))
761 <|> try (do c <- pConstant
762 fc <- pfc
763 return (modifyConst syn fc (PConstant c)))
764 <|> do reserved "Type"; return PType
765 <|> try (do symbol "()"
766 fc <- pfc
767 return (PTrue fc))
768 <|> try (do symbol "_|_"
769 fc <- pfc
770 return (PFalse fc))
771 <|> do lchar '_'; return Placeholder
772 <|> pSimpleExtExpr syn
774bracketed syn =
775 try (pPair syn)
776 <|> try (do e <- pExpr syn; lchar ')'; return e)
777-- <|> try (do reserved "typed"
778-- e <- pExpr syn; symbol ":"; t <- pExpr syn; lchar ')'
779-- return (PTyped e t))
780 <|> try (do fc <- pfc; o <- operator; e <- pExpr syn; lchar ')'
781 return $ PLam (MN 1000 "ARG") Placeholder
782 (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),
783 pexp e]))
784 <|> try (do fc <- pfc; e <- pSimpleExpr syn; o <- operator; lchar ')'
785 return $ PLam (MN 1000 "ARG") Placeholder
786 (PApp fc (PRef fc (UN o)) [pexp e,
787 pexp (PRef fc (MN 1000 "ARG"))]))
789pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
790pCaseOpt syn = do lhs <- pExpr syn; symbol "=>"; rhs <- pExpr syn
791 return (lhs, rhs)
793modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
794modifyConst syn fc (PConstant (I x))
795 | not (inPattern syn)
796 = PAlternative False
797 [PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I x))],
798 PConstant (I x), PConstant (BI (toEnum x))]
799 | otherwise = PAlternative False
800 [PConstant (I x), PConstant (BI (toEnum x))]
801modifyConst syn fc x = x
803pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']'
804 return (mkList fc xs)
805 where
806 mkList fc [] = PRef fc (UN "Nil")
807 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
809pPair syn = try (do l <- pExpr syn
810 fc <- pfc
811 rest <- restTuple
812 case rest of
813 [] -> return l
814 [Left r] -> return (PPair fc l r)
815 [Right r] -> return (PDPair fc l Placeholder r))
816 <|> try (do x <- ntuple
817 lchar ')'
818 return x)
819 <|> do ln <- pName; lchar ':'
820 lty <- pExpr syn
821 reservedOp "**"
822 fc <- pfc
823 r <- pExpr syn
824 lchar ')'
825 return (PDPair fc (PRef fc ln) lty r)
826 where
827 restTuple = do lchar ')'; return []
828 <|> do lchar ','
829 r <- pExpr syn
830 lchar ')'
831 return [Left r]
832 <|> do reservedOp "**"
833 r <- pExpr syn
834 lchar ')'
835 return [Right r]
836 ntuple = try (do l <- pExpr syn; fc <- pfc; lchar ','
837 rest <- ntuple
838 return (PPair fc l rest))
839 <|> (do l <- pExpr syn; fc <- pfc; lchar ','
840 r <- pExpr syn
841 return (PPair fc l r))
843pAlt syn = do symbol "(|"; alts <- sepBy1 (pExpr' syn) (lchar ','); symbol "|)"
844 return (PAlternative False alts)
846pHSimpleExpr syn
847 = do lchar '.'
848 e <- pSimpleExpr syn
849 return $ PHidden e
850 <|> pSimpleExpr syn
852pApp syn = do f <- pSimpleExpr syn
853 fc <- pfc
854 args <- many1 (do notEndApp
855 pArg syn)
856 i <- getState
857 return (dslify i $ PApp fc f args)
858 where
859 dslify i (PApp fc (PRef _ f) [a])
860 | [d] <- lookupCtxt Nothing f (idris_dsls i)
861 = desugar (syn { dsl_info = d }) i (getTm a)
862 dslify i t = t
864pArg :: SyntaxInfo -> IParser PArg
865pArg syn = try (pImplicitArg syn)
866 <|> try (pConstraintArg syn)
867 <|> do e <- pSimpleExpr syn
868 return (pexp e)
870pImplicitArg syn = do lchar '{'
871 n <- pName
872 fc <- pfc
873 v <- option (PRef fc n) (do lchar '='
874 pExpr syn)
875 lchar '}'
876 return (pimp n v)
878pConstraintArg syn = do symbol "@{"
879 e <- pExpr syn
880 symbol "}"
881 return (pconst e)
883pRecordType syn
884 = do reserved "record"
885 lchar '{'
886 fields <- sepBy1 pFieldType (lchar ',')
887 lchar '}'
888 fc <- pfc
889 rec <- option Nothing (do e <- pSimpleExpr syn
890 return (Just e))
891 case rec of
892 Nothing ->
893 return (PLam (MN 0 "fldx") Placeholder
894 (applyAll fc fields (PRef fc (MN 0 "fldx"))))
895 Just v -> return (applyAll fc fields v)
896 where pFieldType = do n <- pfName
897 lchar '='
898 e <- pExpr syn
899 return (n, e)
900 applyAll fc [] x = x
901 applyAll fc ((n, e) : es) x
902 = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])
904mkType (UN n) = UN ("set_" ++ n)
905mkType (MN 0 n) = MN 0 ("set_" ++ n)
906mkType (NS n s) = NS (mkType n) s
908noImp syn = syn { implicitAllowed = False }
909impOK syn = syn { implicitAllowed = True }
911pTSig syn = do lchar ':'
912 cs <- if implicitAllowed syn then pConstList syn else return []
913 sc <- pExpr syn
914 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
916pLambda syn = do lchar '\\'
917 try (do xt <- tyOptDeclList syn
918 symbol "=>"
919 sc <- pExpr syn
920 return (bindList PLam xt sc)
921 <|> (do ps <- sepBy (do fc <- pfc
922 e <- pSimpleExpr syn
923 return (fc, e)) (lchar ',')
924 symbol "=>"
925 sc <- pExpr syn
926 return (pmList (zip [0..] ps) sc)))
927 where pmList [] sc = sc
928 pmList ((i, (fc, x)) : xs) sc
929 = PLam (MN i "lamp") Placeholder
930 (PCase fc (PRef fc (MN i "lamp"))
931 [(x, pmList xs sc)])
933pLet syn = try (do reserved "let"; n <- pName;
934 ty <- option Placeholder (do lchar ':'; pExpr' syn)
935 lchar '='
936 v <- pExpr syn
937 reserved "in"; sc <- pExpr syn
938 return (PLet n ty v sc))
939 <|> (do reserved "let"; fc <- pfc; pat <- pExpr' (syn { inPattern = True } )
940 symbol "="; v <- pExpr syn
941 reserved "in"; sc <- pExpr syn
942 return (PCase fc v [(pat, sc)]))
944pPi syn =
945 try (do lazy <- option False (do lchar '|'; return True)
946 st <- pStatic
947 lchar '('; xt <- tyDeclList syn; lchar ')'
948 doc <- option "" (pDocComment '^')
949 symbol "->"
950 sc <- pExpr syn
951 return (bindList (PPi (Exp lazy st doc)) xt sc))
952 <|> try (if implicitAllowed syn
953 then do lazy <- option False (do lchar '|'
954 return True)
955 st <- pStatic
956 lchar '{'
957 xt <- tyDeclList syn
958 lchar '}'
959 symbol "->"
960 sc <- pExpr syn
961 return (bindList (PPi (Imp lazy st "")) xt sc)
962 else fail "No implicit arguments allowed here")
963 <|> try (do lchar '{'
964 reserved "auto"
965 xt <- tyDeclList syn
966 lchar '}'
967 symbol "->"
968 sc <- pExpr syn
969 return (bindList (PPi
970 (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))
971 <|> try (do lchar '{'
972 reserved "default"
973 script <- pSimpleExpr syn
974 xt <- tyDeclList syn
975 lchar '}'
976 symbol "->"
977 sc <- pExpr syn
978 return (bindList (PPi (TacImp False Dynamic script "")) xt sc))
979 <|> do --lazy <- option False (do lchar '|'; return True)
980 lchar '{'
981 reserved "static"
982 lchar '}'
983 t <- pExpr' syn
984 symbol "->"
985 sc <- pExpr syn
986 return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)
988pConstList :: SyntaxInfo -> IParser [PTerm]
989pConstList syn = try (do lchar '('
990 tys <- sepBy1 (pExpr' (noImp syn)) (lchar ',')
991 lchar ')'
992 reservedOp "=>"
993 return tys)
994 <|> try (do t <- pExpr (noImp syn)
995 reservedOp "=>"
996 return [t])
997 <|> return []
999tyDeclList syn = try (sepBy1 (do x <- pfName
1000 t <- pTSig (noImp syn)
1001 return (x,t))
1002 (lchar ','))
1003 <|> do ns <- sepBy1 pName (lchar ',')
1004 t <- pTSig (noImp syn)
1005 return (map (\x -> (x, t)) ns)
1007tyOptDeclList syn = sepBy1 (do x <- pfName;
1008 t <- option Placeholder (do lchar ':'
1009 pExpr syn)
1010 return (x,t))
1011 (lchar ',')
1013bindList b [] sc = sc
1014bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
1016pComprehension syn
1017 = do lchar '['
1018 fc <- pfc
1019 pat <- pExpr syn
1020 lchar '|'
1021 qs <- sepBy1 (pDo syn) (lchar ',')
1022 lchar ']'
1023 return (PDoBlock (map addGuard qs ++
1024 [DoExp fc (PApp fc (PRef fc (UN "return"))
1025 [pexp pat])]))
1026 where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
1027 [pexp e])
1028 addGuard x = x
1030pDoBlock syn
1031 = do reserved "do"
1032 openBlock
1033 pushIndent
1034 ds <- many1 (do notEndBlock
1035 x <- pDo syn
1036 pKeepTerminator
1037 return x)
1038 popIndent
1039 closeBlock
1040 return (PDoBlock ds)
1042pDo syn
1043 = try (do reserved "let"
1044 i <- pName;
1045 ty <- option Placeholder (do lchar ':'
1046 pExpr' syn)
1047 reservedOp "="
1048 fc <- pfc
1049 e <- pExpr syn
1050 return (DoLet fc i ty e))
1051 <|> try (do reserved "let"
1052 i <- pExpr' syn
1053 reservedOp "="
1054 fc <- pfc
1055 sc <- pExpr syn
1056 return (DoLetP fc i sc))
1057 <|> try (do i <- pName
1058 symbol "<-"
1059 fc <- pfc
1060 e <- pExpr syn;
1061 return (DoBind fc i e))
1062 <|> try (do i <- pExpr' syn
1063 symbol "<-"
1064 fc <- pfc
1065 e <- pExpr syn;
1066 return (DoBindP fc i e))
1067 <|> try (do e <- pExpr syn
1068 fc <- pfc
1069 return (DoExp fc e))
1071pIdiom syn
1072 = do symbol "[|"
1073 fc <- pfc
1074 e <- pExpr syn
1075 symbol "|]"
1076 return (PIdiom fc e)
1078pConstant :: IParser Const
1079pConstant = do reserved "Integer";return BIType
1080 <|> do reserved "Int"; return IType
1081 <|> do reserved "Char"; return ChType
1082 <|> do reserved "Float"; return FlType
1083 <|> do reserved "String"; return StrType
1084 <|> do reserved "Ptr"; return PtrType
1085 <|> do reserved "Word8"; return W8Type
1086 <|> do reserved "Word16"; return W16Type
1087 <|> try (do f <- float; return $ Fl f)
1088-- <|> try (do i <- natural; lchar 'L'; return $ BI i)
1089 <|> try (do i <- natural; return $ I (fromInteger i))
1090 <|> try (do s <- strlit; return $ Str s)
1091 <|> try (do c <- chlit; return $ Ch c)
1093pStatic :: IParser Static
1094pStatic = do lchar '['
1095 reserved "static"
1096 lchar ']';
1097 return Static
1098 <|> return Dynamic
1100table fixes
1101 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
1102 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]
1103 ++ toTable (reverse fixes) ++
1104 [[backtick],
1105 [binary "=" PEq AssocLeft],
1106 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
1108toTable fs = map (map toBin)
1109 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
1110 where toBin (Fix (PrefixN _) op) = prefix op
1111 (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
1112 toBin (Fix f op)
1113 = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
1114 assoc (Infixl _) = AssocLeft
1115 assoc (Infixr _) = AssocRight
1116 assoc (InfixN _) = AssocNone
1118binary name f = Infix (do reservedOp name
1119 fc <- pfc;
1120 doc <- option "" (pDocComment '^')
1121 return (f fc))
1122prefix name f = Prefix (do reservedOp name
1123 fc <- pfc;
1124 return (f fc))
1125backtick = Infix (do lchar '`'; n <- pfName
1126 lchar '`'
1127 fc <- pfc
1128 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
1130--------- Data declarations ---------
1132-- (works for classes too - 'abstract' means the data/class is visible but members not)
1133accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()
1134accData (Just Frozen) n ns = do addAcc n (Just Frozen)
1135 mapM_ (\n -> addAcc n (Just Hidden)) ns
1136accData a n ns = do addAcc n a
1137 mapM_ (`addAcc` a) ns
1139pRecord :: SyntaxInfo -> IParser PDecl
1140pRecord syn = do doc <- option "" (pDocComment '|')
1141 acc <- pAccessibility
1142 reserved "record"
1143 fc <- pfc
1144 tyn_in <- pfName
1145 ty <- pTSig (impOK syn)
1146 let tyn = expandNS syn tyn_in
1147 reserved "where"
1148 openBlock
1149 pushIndent
1150 (cdoc, cn, cty, _) <- pConstructor syn
1151 pKeepTerminator
1152 popIndent
1153 closeBlock
1154 accData acc tyn [cn]
1155 let rsyn = syn { syn_namespace = show (nsroot tyn) :
1156 syn_namespace syn }
1157 let fns = getRecNames rsyn cty
1158 mapM_ (\n -> addAcc n acc) fns
1159 return $ PRecord doc rsyn fc tyn ty cdoc cn cty
1160 where
1161 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
1162 ++ getRecNames syn sc
1163 getRecNames _ _ = []
1165 toFreeze (Just Frozen) = Just Hidden
1166 toFreeze x = x
1168pDataI = do reserved "data"; return False
1169 <|> do reserved "codata"; return True
1171pData :: SyntaxInfo -> IParser PDecl
1172pData syn = try (do doc <- option "" (pDocComment '|')
1173 acc <- pAccessibility
1174 co <- pDataI
1175 fc <- pfc
1176 tyn_in <- pfName
1177 ty <- pTSig (impOK syn)
1178 let tyn = expandNS syn tyn_in
1179 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1180 reserved "where"
1181 openBlock
1182 pushIndent
1183 cons <- many (do notEndBlock
1184 c <- pConstructor syn
1185 pKeepTerminator
1186 return c) -- (lchar '|')
1187 popIndent
1188 closeBlock
1189 accData acc tyn (map (\ (_, n, _, _) -> n) cons)
1190 return $ PData doc syn fc co (PDatadecl tyn ty cons)))
1191 <|> try (do doc <- option "" (pDocComment '|')
1192 pushIndent
1193 acc <- pAccessibility
1194 co <- pDataI
1195 fc <- pfc
1196 tyn_in <- pfName
1197 args <- many pName
1198 let ty = bindArgs (map (const PType) args) PType
1199 let tyn = expandNS syn tyn_in
1200 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1201 try (lchar '=') <|> do reserved "where"
1202 let kw = (if co then "co" else "") ++ "data "
1203 let n = show tyn_in ++ " "
1204 let s = kw ++ n
1205 let as = concat (intersperse " " $ map show args) ++ " "
1206 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
1207 let ss = concat (intersperse " -> " $ map (const "Type") args)
1208 let fix1 = s ++ as ++ " = ..."
1209 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
1210 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
1211 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
1213 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
1214 pTerminator
1215 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
1216 cons' <- mapM (\ (doc, x, cargs, cfc) ->
1217 do let cty = bindArgs cargs conty
1218 return (doc, x, cty, cfc)) cons
1219 accData acc tyn (map (\ (_, n, _, _) -> n) cons')
1220 return $ PData doc syn fc co (PDatadecl tyn ty cons')))
1221 where
1222 mkPApp fc t [] = t
1223 mkPApp fc t xs = PApp fc t (map pexp xs)
1225bindArgs :: [PTerm] -> PTerm -> PTerm
1226bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
1228pConstructor :: SyntaxInfo -> IParser (String, Name, PTerm, FC)
1229pConstructor syn
1230 = do doc <- option "" (pDocComment '|')
1231 cn_in <- pfName; fc <- pfc
1232 let cn = expandNS syn cn_in
1233 ty <- pTSig (impOK syn)
1234-- ty' <- implicit syn cn ty
1235 return (doc, cn, ty, fc)
1238pSimpleCon :: SyntaxInfo -> IParser (String, Name, [PTerm], FC)
1239pSimpleCon syn
1240 = do cn_in <- pfName
1241 let cn = expandNS syn cn_in
1242 fc <- pfc
1243 args <- many (do notEndApp
1244 pSimpleExpr syn)
1245 doc <- option "" (pDocComment '^')
1246 return (doc, cn, args, fc)
1248--------- DSL syntax overloading ---------
1250pDSL :: SyntaxInfo -> IParser PDecl
1251pDSL syn = do reserved "dsl"
1252 n <- pfName
1253 openBlock
1254 pushIndent
1255 bs <- many1 (do notEndBlock
1256 b <- pOverload syn
1257 pKeepTerminator
1258 return b)
1259 popIndent; closeBlock
1260 let dsl = mkDSL bs (dsl_info syn)
1261 checkDSL dsl
1262 i <- getState
1263 setState (i { idris_dsls = addDef n dsl (idris_dsls i) })
1264 return (PDSL n dsl)
1265 where mkDSL bs dsl = let var = lookup "variable" bs
1266 first = lookup "index_first" bs
1267 next = lookup "index_next" bs
1268 leto = lookup "let" bs
1269 lambda = lookup "lambda" bs in
1270 initDSL { dsl_var = var,
1271 index_first = first,
1272 index_next = next,
1273 dsl_lambda = lambda,
1274 dsl_let = leto }
1276checkDSL :: DSL -> IParser ()
1277checkDSL dsl = return ()
1279pOverload :: SyntaxInfo -> IParser (String, PTerm)
1280pOverload syn = do o <- identifier <|> do reserved "let"
1281 return "let"
1282 if o `notElem` overloadable
1283 then fail $ show o ++ " is not an overloading"
1284 else do
1285 lchar '='
1286 t <- pExpr syn
1287 return (o, t)
1288 where overloadable = ["let","lambda","index_first","index_next","variable"]
1290--------- Pattern match clauses ---------
1292pPattern :: SyntaxInfo -> IParser PDecl
1293pPattern syn = do fc <- pfc
1294 clause <- pClause syn
1295 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
1297pCAF :: SyntaxInfo -> IParser PDecl
1298pCAF syn = do reserved "let"
1299 n_in <- pfName; let n = expandNS syn n_in
1300 lchar '='
1301 t <- pExpr syn
1302 pTerminator
1303 fc <- pfc
1304 return (PCAF fc n t)
1306pArgExpr syn = let syn' = syn { inPattern = True } in
1307 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
1309pRHS :: SyntaxInfo -> Name -> IParser PTerm
1310pRHS syn n = do lchar '='; pExpr syn
1311 <|> do symbol "?="; rhs <- pExpr syn;
1312 return (addLet rhs)
1313 <|> do reserved "impossible"; return PImpossible
1314 where mkN (UN x) = UN (x++"_lemma_1")
1315 mkN (NS x n) = NS (mkN x) n
1316 n' = mkN n
1318 addLet (PLet n ty val rhs) = PLet n ty val (addLet rhs)
1319 addLet (PCase fc t cs) = PCase fc t (map addLetC cs)
1320 where addLetC (l, r) = (l, addLet r)
1321 addLet rhs = (PLet (UN "value") Placeholder rhs (PMetavar n'))
1323pClause :: SyntaxInfo -> IParser PClause
1324pClause syn
1325 = try (do pushIndent
1326 n_in <- pfName; let n = expandNS syn n_in
1327 cargs <- many (pConstraintArg syn)
1328 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1329 fc <- pfc
1330 args <- many (pArgExpr syn)
1331 wargs <- many (pWExpr syn)
1332 rhs <- pRHS syn n
1333 ist <- getState
1334 let ctxt = tt_ctxt ist
1335 let wsyn = syn { syn_namespace = [] }
1336 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1337 popIndent
1338 return x,
1339 do pTerminator
1340 return ([], [])]
1341 let capp = PApp fc (PRef fc n)
1342 (iargs ++ cargs ++ map pexp args)
1343 ist <- getState
1344 setState (ist { lastParse = Just n })
1345 return $ PClause fc n capp wargs rhs wheres)
1346 <|> try (do pushIndent
1347 wargs <- many1 (pWExpr syn)
1348 ist <- getState
1349 n <- case lastParse ist of
1350 Just t -> return t
1351 Nothing -> fail "Invalid clause"
1352 fc <- pfc
1353 rhs <- pRHS syn n
1354 let ctxt = tt_ctxt ist
1355 let wsyn = syn { syn_namespace = [] }
1356 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1357 popIndent
1358 return x,
1359 do pTerminator
1360 return ([], [])]
1361 return $ PClauseR fc wargs rhs wheres)
1363 <|> try (do pushIndent
1364 n_in <- pfName; let n = expandNS syn n_in
1365 cargs <- many (pConstraintArg syn)
1366 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1367 fc <- pfc
1368 args <- many (pArgExpr syn)
1369 wargs <- many (pWExpr syn)
1370 let capp = PApp fc (PRef fc n)
1371 (iargs ++ cargs ++ map pexp args)
1372 ist <- getState
1373 setState (ist { lastParse = Just n })
1374 reserved "with"
1375 wval <- pSimpleExpr syn
1376 openBlock
1377 ds <- many1 $ pFunDecl syn
1378 let withs = map (fillLHSD n capp wargs) $ concat ds
1379 closeBlock
1380 popIndent
1381 return $ PWith fc n capp wargs wval withs)
1383 <|> try (do wargs <- many1 (pWExpr syn)
1384 fc <- pfc
1385 reserved "with"
1386 wval <- pSimpleExpr syn
1387 openBlock
1388 ds <- many1 $ pFunDecl syn
1389 let withs = concat ds
1390 closeBlock
1391 return $ PWithR fc wargs wval withs)
1393 <|> do pushIndent
1394 l <- pArgExpr syn
1395 op <- operator
1396 let n = expandNS syn (UN op)
1397 r <- pArgExpr syn
1398 fc <- pfc
1399 wargs <- many (pWExpr syn)
1400 rhs <- pRHS syn n
1401 let wsyn = syn { syn_namespace = [] }
1402 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1403 popIndent
1404 return x,
1405 do pTerminator
1406 return ([], [])]
1407 ist <- getState
1408 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1409 setState (ist { lastParse = Just n })
1410 return $ PClause fc n capp wargs rhs wheres
1412 <|> do l <- pArgExpr syn
1413 op <- operator
1414 let n = expandNS syn (UN op)
1415 r <- pArgExpr syn
1416 fc <- pfc
1417 wargs <- many (pWExpr syn)
1418 reserved "with"
1419 wval <- pSimpleExpr syn
1420 openBlock
1421 ds <- many1 $ pFunDecl syn
1422 closeBlock
1423 ist <- getState
1424 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1425 let withs = map (fillLHSD n capp wargs) $ concat ds
1426 setState (ist { lastParse = Just n })
1427 return $ PWith fc n capp wargs wval withs
1428 where
1429 fillLHS n capp owargs (PClauseR fc wargs v ws)
1430 = PClause fc n capp (owargs ++ wargs) v ws
1431 fillLHS n capp owargs (PWithR fc wargs v ws)
1432 = PWith fc n capp (owargs ++ wargs) v
1433 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1434 fillLHS _ _ _ c = c
1436 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1437 fillLHSD n c a x = x
1439pWExpr :: SyntaxInfo -> IParser PTerm
1440pWExpr syn = do lchar '|'
1441 pExpr' syn
1443pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
1444pWhereblock n syn
1445 = do reserved "where"; openBlock
1446 ds <- many1 $ pDecl syn
1447 let dns = concatMap (concatMap declared) ds
1448 closeBlock
1449 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1451pDirective :: IParser [PDecl]
1452pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;
1453 return [PDirective (do addLib lib
1454 addIBC (IBCLib lib))])
1455 <|> try (do lchar '%'; reserved "link"; obj <- strlit;
1456 return [PDirective (do datadir <- liftIO getDataDir
1457 o <- liftIO $ findInPath [".", datadir] obj
1458 addIBC (IBCObj o)
1459 addObjectFile o)])
1460 <|> try (do lchar '%'; reserved "include"; hdr <- strlit;
1461 return [PDirective (do addHdr hdr
1462 addIBC (IBCHeader hdr))])
1463 <|> try (do lchar '%'; reserved "hide"; n <- iName []
1464 return [PDirective (do setAccessibility n Hidden
1465 addIBC (IBCAccess n Hidden))])
1466 <|> try (do lchar '%'; reserved "freeze"; n <- iName []
1467 return [PDirective (do setAccessibility n Frozen
1468 addIBC (IBCAccess n Frozen))])
1469 <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'
1470 return [PDirective (do i <- getIState
1471 putIState (i { default_access = acc }))])
1472 <|> try (do lchar '%'; reserved "default"; tot <- pTotality
1473 i <- getState
1474 setState (i { default_total = tot } )
1475 return [PDirective (do i <- getIState
1476 putIState (i { default_total = tot }))])
1477 <|> try (do lchar '%'; reserved "logging"; i <- natural;
1478 return [PDirective (setLogLevel (fromInteger i))])
1480pTactic :: SyntaxInfo -> IParser PTactic
1481pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
1482 return $ Intro ns
1483 <|> do reserved "intros"; return Intros
1484 <|> try (do reserved "refine"; n <- pName
1485 imps <- many1 imp
1486 return $ Refine n imps)
1487 <|> do reserved "refine"; n <- pName
1488 i <- getState
1489 return $ Refine n []
1490 <|> do reserved "rewrite"; t <- pExpr syn;
1491 i <- getState
1492 return $ Rewrite (desugar syn i t)
1493 <|> try (do reserved "let"; n <- pName; lchar ':';
1494 ty <- pExpr' syn; lchar '='; t <- pExpr syn;
1495 i <- getState
1496 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
1497 <|> try (do reserved "let"; n <- pName; lchar '=';
1498 t <- pExpr syn;
1499 i <- getState
1500 return $ LetTac n (desugar syn i t))
1501 <|> do reserved "focus"; n <- pName
1502 return $ Focus n
1503 <|> do reserved "exact"; t <- pExpr syn;
1504 i <- getState
1505 return $ Exact (desugar syn i t)
1506 <|> do reserved "try"; t <- pTactic syn;
1507 lchar '|';
1508 t1 <- pTactic syn
1509 return $ Try t t1
1510 <|> do lchar '{'
1511 t <- pTactic syn;
1512 lchar ';';
1513 t1 <- pTactic syn;
1514 lchar '}'
1515 return $ TSeq t t1
1516 <|> do reserved "compute"; return Compute
1517 <|> do reserved "trivial"; return Trivial
1518 <|> do reserved "solve"; return Solve
1519 <|> do reserved "attack"; return Attack
1520 <|> do reserved "state"; return ProofState
1521 <|> do reserved "term"; return ProofTerm
1522 <|> do reserved "undo"; return Undo
1523 <|> do reserved "qed"; return Qed
1524 <|> do reserved "abandon"; return Abandon
1525 <|> do lchar ':'; reserved "q"; return Abandon
1526 where
1527 imp = do lchar '?'; return False
1528 <|> do lchar '_'; return True