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