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