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