git.iko.soy/Idris-dev
on 3a8d9db help sign in
Idris-dev/src/Idris/Parser.hs
1747 lines 71 kB history raw
1{-# LANGUAGE PatternGuards, ScopedTypeVariables #-}
2-- | Parse the full Idris language.
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 Idris.Providers
15import Paths_idris
17import Util.DynamicLinker
19import Core.CoreParser
20import Core.TT
21import Core.Evaluate
23import Text.Parsec
24import Text.Parsec.Error
25import Text.Parsec.Expr
26import Text.Parsec.Language
27import Text.Parsec.String
28import qualified Text.Parsec.Token as PTok
30import Data.List
31import Data.List.Split(splitOn)
32import Control.Monad.State
33import Control.Monad.Error
34import Debug.Trace
35import Data.Maybe
36import System.FilePath
38type TokenParser a = PTok.TokenParser a
40type IParser = GenParser Char IState
42lexer :: TokenParser IState
43lexer = idrisLexer
45whiteSpace = PTok.whiteSpace lexer
46lexeme = PTok.lexeme lexer
47symbol = PTok.symbol lexer
48natural = PTok.natural lexer
49parens = PTok.parens lexer
50semi = PTok.semi lexer
51comma = PTok.comma lexer
52identifier = PTok.identifier lexer
53reserved = PTok.reserved lexer
54operator = PTok.operator lexer
55reservedOp = PTok.reservedOp lexer
56integer = PTok.integer lexer
57float = PTok.float lexer
58strlit = PTok.stringLiteral lexer
59chlit = PTok.charLiteral lexer
60lchar = lexeme.char
62fixErrorMsg :: String -> [String] -> String
63fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)
65-- Loading modules
67loadModule :: FilePath -> Idris String
68loadModule f
69 = idrisCatch (do i <- getIState
70 let file = takeWhile (/= ' ') f
71 ibcsd <- valIBCSubDir i
72 ids <- allImportDirs
73 fp <- liftIO $ findImport ids ibcsd file
74 if file `elem` imported i
75 then iLOG $ "Already read " ++ file
76 else do putIState (i { imported = file : imported i })
77 case fp of
78 IDR fn -> loadSource False fn
79 LIDR fn -> loadSource True fn
80 IBC fn src ->
81 idrisCatch (loadIBC fn)
82 (\c -> do iLOG $ fn ++ " failed " ++ show c
83 case src of
84 IDR sfn -> loadSource False sfn
85 LIDR sfn -> loadSource True sfn)
86 let (dir, fh) = splitFileName file
87 return (dropExtension fh))
88 (\e -> do let msg = show e
89 setErrLine (getErrLine msg)
90 iputStrLn msg
91 return "")
93loadFromIFile :: IFileType -> Idris ()
94loadFromIFile i@(IBC fn src)
95 = do iLOG $ "Skipping " ++ getSrcFile i
96 idrisCatch (loadIBC fn)
97 (\c -> do fail $ fn ++ " failed " ++ show c)
98-- loadFromIFile src)
99 where
100 getSrcFile (IDR fn) = fn
101 getSrcFile (LIDR fn) = fn
102 getSrcFile (IBC f src) = getSrcFile src
104loadFromIFile (IDR fn) = loadSource' False fn
105loadFromIFile (LIDR fn) = loadSource' True fn
107loadSource' lidr r
108 = idrisCatch (loadSource lidr r)
109 (\e -> do let msg = show e
110 setErrLine (getErrLine msg)
111 iputStrLn msg)
113loadSource :: Bool -> FilePath -> Idris ()
114loadSource lidr f
115 = do iLOG ("Reading " ++ f)
116 i <- getIState
117 let def_total = default_total i
118 file_in <- liftIO $ readFile f
119 file <- if lidr then tclift $ unlit f file_in else return file_in
120 (mname, modules, rest, pos) <- parseImports f file
121 i <- getIState
122 putIState (i { default_access = Hidden })
123-- mapM_ loadModule modules
124 clearIBC -- start a new .ibc file
125 mapM_ (addIBC . IBCImport) modules
126 ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
127 f rest pos
128 unless (null ds') $ do
129 let ds = namespaces mname ds'
130 logLvl 3 (dumpDecls ds)
131 i <- getIState
132 logLvl 10 (show (toAlist (idris_implicits i)))
133 logLvl 3 (show (idris_infixes i))
134 -- Now add all the declarations to the context
135 v <- verbose
136 when v $ iputStrLn $ "Type checking " ++ f
137 elabDecls toplevel ds
138 i <- getIState
139 -- simplify every definition do give the totality checker
140 -- a better chance
141 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
142 updateContext (simplifyCasedef n))
143 (map snd (idris_totcheck i))
144 -- build size change graph from simplified definitions
145 iLOG "Totality checking"
146 i <- getIState
147 mapM_ buildSCG (idris_totcheck i)
148 mapM_ checkDeclTotality (idris_totcheck i)
149 iLOG ("Finished " ++ f)
150 ibcsd <- valIBCSubDir i
151 iLOG "Universe checking"
152 iucheck
153 let ibc = ibcPathNoFallback ibcsd f
154 i <- getIState
155 addHides (hide_list i)
156 ok <- noErrors
157 when ok $
158 idrisCatch (do writeIBC f ibc; clearIBC)
159 (\c -> return ()) -- failure is harmless
160 i <- getIState
161 putIState (i { default_total = def_total,
162 hide_list = [] })
163 return ()
164 return ()
165 where
166 namespaces [] ds = ds
167 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
169addHides :: [(Name, Maybe Accessibility)] -> Idris ()
170addHides xs = do i <- getIState
171 let defh = default_access i
172 let (hs, as) = partition isNothing xs
173 unless (null as) $
174 mapM_ doHide
175 (map (\ (n, _) -> (n, defh)) hs ++
176 map (\ (n, Just a) -> (n, a)) as)
177 where isNothing (_, Nothing) = True
178 isNothing _ = False
180 doHide (n, a) = do setAccessibility n a
181 addIBC (IBCAccess n a)
183parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"
184parseTac i = runParser (do t <- pTactic defaultSyntax
185 eof
186 return t) i "(proof)"
188parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)
189parseImports fname input
190 = do i <- getIState
191 case runParser (do whiteSpace
192 mname <- pHeader
193 ps <- many pImport
194 rest <- getInput
195 pos <- getPosition
196 return ((mname, ps, rest, pos), i)) i fname input of
197 Left err -> fail (show err)
198 Right (x, i) -> do -- Discard state updates (there should be
199 -- none anyway)
200 return x
202pHeader :: IParser [String]
203pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')
204 return (parseName i))
205 <|> return []
206 where parseName x = case span (/='.') x of
207 (x, "") -> [x]
208 (x, '.':y) -> x : parseName y
210pushIndent :: IParser ()
211pushIndent = do pos <- getPosition
212 ist <- getState
213 setState (ist { indent_stack = sourceColumn pos :
214 indent_stack ist })
216lastIndent :: IParser Int
217lastIndent = do ist <- getState
218 case indent_stack ist of
219 (x : xs) -> return x
220 _ -> return 1
222indent :: IParser Int
223indent = liftM sourceColumn getPosition
225popIndent :: IParser ()
226popIndent = do ist <- getState
227 let (x : xs) = indent_stack ist
228 setState (ist { indent_stack = xs })
230openBlock :: IParser ()
231openBlock = do lchar '{'
232 ist <- getState
233 setState (ist { brace_stack = Nothing : brace_stack ist })
234 <|> do ist <- getState
235 lvl' <- indent
236 -- if we're not indented further, it's an empty block, so
237 -- increment lvl to ensure we get to the end
238 let lvl = case brace_stack ist of
239 Just lvl_old : _ ->
240 if lvl' <= lvl_old then lvl_old+1
241 else lvl'
242 [] -> if lvl' == 1 then 2 else lvl'
243 _ -> lvl'
244 setState (ist { brace_stack = Just lvl : brace_stack ist })
246closeBlock :: IParser ()
247closeBlock = do ist <- getState
248 bs <- case brace_stack ist of
249 [] -> eof >> return []
250 Nothing : xs -> (lchar '}' >> return xs) <|> (eof >> return [])
251 Just lvl : xs -> (do i <- indent
252 inp <- getInput
253-- trace (show (take 10 inp, i, lvl)) $
254 if i >= lvl && take 1 inp /= ")"
255 then fail "Not end of block"
256 else return xs) <|> (eof >> return [])
257 setState (ist { brace_stack = bs })
259pTerminator = do lchar ';'; popIndent
260 <|> do c <- indent; l <- lastIndent
261 if c <= l
262 then popIndent
263 else fail "Not a terminator"
264 <|> do i <- getInput
265 if "}" `isPrefixOf` i || ")" `isPrefixOf` i
266 then popIndent
267 else fail "Not a terminator"
268 <|> lookAhead eof
270pBarTerminator
271 = do lchar '|'; return ()
272 <|> do c <- indent; l <- lastIndent
273 unless (c <= l) $ fail "Not a terminator"
274 <|> lookAhead eof
276pKeepTerminator
277 = do lchar ';'; return ()
278 <|> do c <- indent; l <- lastIndent
279 unless (c <= l) $ fail "Not a terminator"
280 <|> do i <- getInput
281 let h = take 1 i
282 unless (h `elem` ["}", ")", "|"]) $ fail "Not a terminator"
283 <|> lookAhead eof
285notEndApp = do c <- indent; l <- lastIndent
286 i <- getInput
287 when (c <= l) $ fail "Terminator"
289notEndBlock = do ist <- getState
290 case brace_stack ist of
291 Just lvl : xs -> do i <- indent
292 inp <- getInput
293 when (i < lvl || ")" `isPrefixOf` inp) $ fail "End of block"
294 _ -> return ()
296-- | Use Parsec's internal state to construct a source code position
297pfc :: IParser FC
298pfc = do s <- getPosition
299 let (dir, file) = splitFileName (sourceName s)
300 let f = if dir == addTrailingPathSeparator "." then file else sourceName s
301 return $ FC f (sourceLine s)
303pImport :: IParser String
304pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')
305 return (toPath f)
306 where toPath n = foldl1' (</>) $ splitOn "." n
308-- | A program is a list of declarations, possibly with associated
309-- documentation strings.
310parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos ->
311 Idris [PDecl]
312parseProg syn fname input pos
313 = do i <- getIState
314 case runParser (do setPosition pos
315 whiteSpace
316 ps <- many (pDecl syn)
317 eof
318 i' <- getState
319 return (concat ps, i')) i fname input of
320 Left err -> do iputStrLn (show err)
321 let errl = sourceLine (errorPos err)
322 i <- getIState
323 putIState (i { errLine = Just errl })
324 return []
325 Right (x, i) -> do putIState i
326 return (collect x)
328-- | Collect 'PClauses' with the same function name
329collect :: [PDecl] -> [PDecl]
330collect (c@(PClauses _ o _ _) : ds)
331 = clauses (cname c) [] (c : ds)
332 where clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)
333 | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds
334 clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds)
335 | n == n' = clauses j (PWith fc' n' l ws r (collect w) : acc) ds
336 clauses (Just n) acc xs = PClauses (getfc c) o n (reverse acc) : collect xs
337 clauses Nothing acc (x:xs) = collect xs
338 clauses Nothing acc [] = []
340 cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n
341 cname (PClauses fc _ _ [PWith _ n _ _ _ _]) = Just n
342 cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing
343 cname (PClauses fc _ _ [PWithR _ _ _ _]) = Nothing
344 getfc (PClauses fc _ _ _) = fc
346collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
347collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds
348collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds
349collect (PClass doc f s cs n ps ds : ds')
350 = PClass doc f s cs n ps (collect ds) : collect ds'
351collect (PInstance f s cs n ps t en ds : ds')
352 = PInstance f s cs n ps t en (collect ds) : collect ds'
353collect (d : ds) = d : collect ds
354collect [] = []
356pFullExpr :: SyntaxInfo -> IParser PTerm
357pFullExpr syn
358 = do x <- pExpr syn; eof;
359 i <- getState
360 return $ desugar syn i x
362-- | Parse a top-level declaration
363pDecl :: SyntaxInfo -> IParser [PDecl]
364pDecl syn = do notEndBlock
365 pDeclBody where
366 pDeclBody
367 = do d <- pDecl' syn
368 i <- getState
369 let d' = fmap (desugar syn i) d
370 return [d']
371 <|> pUsing syn
372 <|> pParams syn
373 <|> pMutual syn
374 <|> pNamespace syn
375 <|> pClass syn
376 <|> pInstance syn
377 <|> do d <- pDSL syn; return [d]
378 <|> pDirective syn
379 <|> try (pProvider syn)
380 <|> pTransform syn
381 <|> try (do reserved "import"; fp <- identifier
382 fail "imports must be at the top of file")
384pFunDecl :: SyntaxInfo -> IParser [PDecl]
385pFunDecl syn
386 = try (do notEndBlock
387 d <- pFunDecl' syn
388 i <- getState
389 let d' = fmap (desugar syn i) d
390 return [d'])
392--------- Top Level Declarations ---------
394pDecl' :: SyntaxInfo -> IParser PDecl
395pDecl' syn
396 = try pFixity
397 <|> try (pFunDecl' syn)
398 <|> try (pData syn)
399 <|> try (pRecord syn)
400 <|> try (pSyntaxDecl syn)
402pSyntaxDecl :: SyntaxInfo -> IParser PDecl
403pSyntaxDecl syn
404 = do s <- pSyntaxRule syn
405 i <- getState
406 let rs = syntax_rules i
407 let ns = syntax_keywords i
408 let ibc = ibc_write i
409 let ks = map show (names s)
410 setState (i { syntax_rules = s : rs,
411 syntax_keywords = ks ++ ns,
412 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc
413 })
414 fc <- pfc
415 return (PSyntax fc s)
416 where
417 names (Rule syms _ _) = mapMaybe ename syms
418 ename (Keyword n) = Just n
419 ename _ = Nothing
421pSyntaxRule :: SyntaxInfo -> IParser Syntax
422pSyntaxRule syn
423 = do pushIndent
424 sty <- option AnySyntax (do reserved "term"; return TermSyntax
425 <|> do reserved "pattern"; return PatternSyntax)
426 reserved "syntax"
427 syms <- many1 pSynSym
428 when (all expr syms) $ fail "No keywords in syntax rule"
429 let ns = mapMaybe name syms
430 when (length ns /= length (nub ns))
431 $ fail "Repeated variable in syntax rule"
432 lchar '='
433 tm <- pTExpr (impOK syn)
434 pTerminator
435 return (Rule (mkSimple syms) tm sty)
436 where
437 expr (Expr _) = True
438 expr _ = False
439 name (Expr n) = Just n
440 name _ = Nothing
442 -- Can't parse two full expressions (i.e. expressions with application) in a row
443 -- so change them both to a simple expression
445 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
446 mkSimple xs = mkSimple' xs
448 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
449 mkSimple es
450 mkSimple' (e : es) = e : mkSimple' es
451 mkSimple' [] = []
453pSynSym :: IParser SSymbol
454pSynSym = try (do lchar '['; n <- pName; lchar ']'
455 return (Expr n))
456 <|> try (do lchar '{'; n <- pName; lchar '}'
457 return (Binding n))
458 <|> do n <- iName []
459 return (Keyword n)
460 <|> do sym <- strlit
461 return (Symbol sym)
463pFunDecl' :: SyntaxInfo -> IParser PDecl
464pFunDecl' syn = try (do doc <- option "" (pDocComment '|')
465 pushIndent
466 ist <- getState
467 let initOpts = if default_total ist
468 then [TotalFn]
469 else []
470 opts <- pFnOpts initOpts
471 acc <- pAccessibility
472 opts' <- pFnOpts opts
473 n_in <- pfName
474 let n = expandNS syn n_in
475 fc <- pfc
476 ty <- pTSig (impOK syn)
477 pTerminator
478-- ty' <- implicit syn n ty
479 addAcc n acc
480 return (PTy doc syn fc opts' n ty))
481 <|> try (pPostulate syn)
482 <|> try (pPattern syn)
483 <|> try (pCAF syn)
485pPostulate :: SyntaxInfo -> IParser PDecl
486pPostulate syn = do doc <- option "" (pDocComment '|')
487 pushIndent
488 reserved "postulate"
489 ist <- getState
490 let initOpts = if default_total ist
491 then [TotalFn]
492 else []
493 opts <- pFnOpts initOpts
494 acc <- pAccessibility
495 opts' <- pFnOpts opts
496 n_in <- pfName
497 let n = expandNS syn n_in
498 ty <- pTSig (impOK syn)
499 fc <- pfc
500 pTerminator
501 addAcc n acc
502 return (PPostulate doc syn fc opts' n ty)
505pUsing :: SyntaxInfo -> IParser [PDecl]
506pUsing syn =
507 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
508 openBlock
509 let uvars = using syn
510 ds <- many1 (pDecl (syn { using = uvars ++ ns }))
511 closeBlock
512 return (concat ds)
514pParams :: SyntaxInfo -> IParser [PDecl]
515pParams syn =
516 do reserved "parameters"; lchar '('; ns <- tyDeclList syn; lchar ')'
517 openBlock
518 let pvars = syn_params syn
519 ds <- many1 (pDecl syn { syn_params = pvars ++ ns })
520 closeBlock
521 fc <- pfc
522 return [PParams fc ns (concat ds)]
524pMutual :: SyntaxInfo -> IParser [PDecl]
525pMutual syn =
526 do reserved "mutual"
527 openBlock
528 let pvars = syn_params syn
529 ds <- many1 (pDecl syn)
530 closeBlock
531 fc <- pfc
532 return [PMutual fc (concat ds)]
534pNamespace :: SyntaxInfo -> IParser [PDecl]
535pNamespace syn =
536 do reserved "namespace"; n <- identifier;
537 openBlock
538 ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
539 closeBlock
540 return [PNamespace n (concat ds)]
542--------- Fixity ---------
544pFixity :: IParser PDecl
545pFixity = do pushIndent
546 f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
547 pTerminator
548 let prec = fromInteger i
549 istate <- getState
550 let infixes = idris_infixes istate
551 let fs = map (Fix (f prec)) ops
552 let redecls = map (alreadyDeclared infixes) fs
553 let ill = filter (not . checkValidity) redecls
554 if null ill
555 then do setState (istate { idris_infixes = nub $ sort (fs ++ infixes)
556 , ibc_write = map IBCFix fs ++ ibc_write istate
557 })
558 fc <- pfc
559 return (PFix fc (f prec) ops)
560 else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
561 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
562 where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
563 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
565 checkValidity :: (FixDecl, [FixDecl]) -> Bool
566 checkValidity (f, fs) = all (== f) fs
568 extractName :: FixDecl -> String
569 extractName (Fix _ n) = n
571fixity :: IParser (Int -> Fixity)
572fixity = try (do reserved "infixl"; return Infixl)
573 <|> try (do reserved "infixr"; return Infixr)
574 <|> try (do reserved "infix"; return InfixN)
575 <|> try (do reserved "prefix"; return PrefixN)
577--------- Type classes ---------
579pClass :: SyntaxInfo -> IParser [PDecl]
580pClass syn = do doc <- option "" (pDocComment '|')
581 acc <- pAccessibility
582 reserved "class"; fc <- pfc; cons <- pConstList syn; n_in <- pName
583 let n = expandNS syn n_in
584 cs <- many carg
585 reserved "where"; openBlock
586 ds <- many $ pFunDecl syn
587 closeBlock
588 let allDs = concat ds
589 accData acc n (concatMap declared allDs)
590 return [PClass doc syn fc cons n cs allDs]
591 where
592 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'
593 return (i, ty)
594 <|> do i <- pName;
595 return (i, PType)
597pInstance :: SyntaxInfo -> IParser [PDecl]
598pInstance syn = do reserved "instance"; fc <- pfc
599 en <- option Nothing
600 (do lchar '['; n_in <- pfName; lchar ']'
601 let n = expandNS syn n_in
602 return (Just n))
603 cs <- pConstList syn
604 cn <- pName
605 args <- many (pSimpleExpr syn)
606 let sc = PApp fc (PRef fc cn) (map pexp args)
607 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
608 reserved "where"; openBlock
609 ds <- many $ pFunDecl syn
610 closeBlock
611 return [PInstance syn fc cs cn args t en (concat ds)]
613--------- Expressions ---------
615pExpr syn = do i <- getState
616 buildExpressionParser (table (idris_infixes i)) (pExpr' syn)
618pExpr' :: SyntaxInfo -> IParser PTerm
619pExpr' syn
620 = try (pExtExpr syn)
621 <|> pNoExtExpr syn
623pExtExpr :: SyntaxInfo -> IParser PTerm
624pExtExpr syn = do i <- getState
625 pExtensions syn (syntax_rules i)
627pSimpleExtExpr :: SyntaxInfo -> IParser PTerm
628pSimpleExtExpr syn = do i <- getState
629 pExtensions syn (filter simple (syntax_rules i))
630 where
631 simple (Rule (Expr x:xs) _ _) = False
632 simple (Rule (SimpleExpr x:xs) _ _) = False
633 simple (Rule [Keyword _] _ _) = True
634 simple (Rule [Symbol _] _ _) = True
635 simple (Rule (_:xs) _ _) = case last xs of
636 Keyword _ -> True
637 Symbol _ -> True
638 _ -> False
639 simple _ = False
641pNoExtExpr syn =
642 try (pApp syn)
643 <|> try (pMatchApp syn)
644 <|> try (pUnifyLog syn)
645 <|> pRecordType syn
646 <|> try (pSimpleExpr syn)
647 <|> pLambda syn
648 <|> pQuoteGoal syn
649 <|> pLet syn
650 <|> pRewriteTerm syn
651 <|> pPi syn
652 <|> pDoBlock syn
654pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
655pExtensions syn rules = choice (map (try . pExt syn) (filter valid rules))
656 where
657 valid (Rule _ _ AnySyntax) = True
658 valid (Rule _ _ PatternSyntax) = inPattern syn
659 valid (Rule _ _ TermSyntax) = not (inPattern syn)
662data SynMatch = SynTm PTerm | SynBind Name
664pExt :: SyntaxInfo -> Syntax -> IParser PTerm
665pExt syn (Rule ssym ptm _)
666 = do smap <- mapM pSymbol ssym
667 let ns = mapMaybe id smap
668 return (update ns ptm) -- updated with smap
669 where
670 pSymbol (Keyword n) = do reserved (show n); return Nothing
671 pSymbol (Expr n) = do tm <- pExpr syn
672 return $ Just (n, SynTm tm)
673 pSymbol (SimpleExpr n) = do tm <- pSimpleExpr syn
674 return $ Just (n, SynTm tm)
675 pSymbol (Binding n) = do b <- pName
676 return $ Just (n, SynBind b)
677 pSymbol (Symbol s) = do symbol s
678 return Nothing
679 dropn n [] = []
680 dropn n ((x,t) : xs) | n == x = xs
681 | otherwise = (x,t):dropn n xs
683 updateB ns n = case lookup n ns of
684 Just (SynBind t) -> t
685 _ -> n
687 update ns (PRef fc n) = case lookup n ns of
688 Just (SynTm t) -> t
689 _ -> PRef fc n
690 update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)
691 update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc)
692 update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)
693 (update (dropn n ns) sc)
694 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
695 update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)
696 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)
697 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)
698 update ns (PAlternative a as) = PAlternative a (map (update ns) as)
699 update ns (PHidden t) = PHidden (update ns t)
700 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
701 where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
702 upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds
703 upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)
704 : upd (dropn n ns) ds
705 upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t)
706 : upd ns ds
707 upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)
708 : upd ns ds
709 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
710 update ns t = t
712pName = do i <- getState
713 iName (syntax_keywords i)
714 <|> do reserved "instance"
715 i <- getState
716 UN n <- iName (syntax_keywords i)
717 return (UN ('@':n))
719-- | Parser for an operator in function position, i.e. enclosed by `()', with an
720-- optional namespace.
721pOpFront = maybeWithNS pOpFrontNoNS False []
722 where pOpFrontNoNS = do lchar '('; o <- operator; lchar ')'; return o
724pfName = try pOpFront
725 <|> pName
727pTotality :: IParser Bool
728pTotality
729 = do reserved "total"; return True
730 <|> do reserved "partial"; return False
732pAccessibility' :: IParser Accessibility
733pAccessibility'
734 = do reserved "public"; return Public
735 <|> do reserved "abstract"; return Frozen
736 <|> do reserved "private"; return Hidden
738pAccessibility :: IParser (Maybe Accessibility)
739pAccessibility
740 = do acc <- pAccessibility'; return (Just acc)
741 <|> return Nothing
743pFnOpts :: [FnOpt] -> IParser [FnOpt]
744pFnOpts opts
745 = do reserved "total"; pFnOpts (TotalFn : opts)
746 <|> do reserved "partial"; pFnOpts (PartialFn : (opts \\ [TotalFn]))
747 <|> try (do lchar '%'; reserved "export"; c <- strlit;
748 pFnOpts (CExport c : opts))
749 <|> try (do lchar '%'; reserved "assert_total";
750 pFnOpts (AssertTotal : opts))
751 <|> try (do lchar '%'; reserved "reflection";
752 pFnOpts (Reflection : opts))
753 <|> do lchar '%'; reserved "specialise";
754 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
755 pFnOpts (Specialise ns : opts)
756 <|> do reserved "implicit"; pFnOpts (Implicit : opts)
757 <|> return opts
758 where nameTimes = do n <- pfName
759 t <- option Nothing (do reds <- natural
760 return (Just (fromInteger reds)))
761 return (n, t)
763addAcc :: Name -> Maybe Accessibility -> IParser ()
764addAcc n a = do i <- getState
765 setState (i { hide_list = (n, a) : hide_list i })
767pCaseExpr syn = do
768 reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
769 openBlock
770 pushIndent
771 opts <- many1 (do notEndBlock
772 x <- pCaseOpt syn
773 pKeepTerminator
774 return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
775 popIndent
776 closeBlock
777 return (PCase fc scr opts)
779pProofExpr syn = do
780 reserved "proof"; lchar '{'
781 ts <- endBy (pTactic syn) (lchar ';')
782 lchar '}'
783 return (PProof ts)
785pTacticsExpr syn = do
786 reserved "tactics"; lchar '{'
787 ts <- endBy (pTactic syn) (lchar ';')
788 lchar '}'
789 return (PTactics ts)
791pSimpleExpr syn =
792 try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t)
793 <|> do lchar '?'; x <- pName; return (PMetavar x)
794 <|> do lchar '%'; fc <- pfc; reserved "instance"; return (PResolveTC fc)
795 <|> do reserved "refl"; fc <- pfc;
796 tm <- option Placeholder (do lchar '{'; t <- pExpr syn; lchar '}';
797 return t)
798 return (PRefl fc tm)
799-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)
800 <|> pProofExpr syn
801 <|> pTacticsExpr syn
802 <|> pCaseExpr syn
803 <|> try (do x <- pfName
804 fc <- pfc
805 return (PRef fc x))
806 <|> try (pList syn)
807 <|> try (pComprehension syn)
808 <|> try (pAlt syn)
809 <|> try (pIdiom syn)
810 <|> try (do lchar '('
811 bracketed (noImp syn))
812 <|> try (do c <- pConstant
813 fc <- pfc
814 return (modifyConst syn fc (PConstant c)))
815 <|> do reserved "Type"; return PType
816 <|> try (do symbol "()"
817 fc <- pfc
818 return (PTrue fc))
819 <|> try (do symbol "_|_"
820 fc <- pfc
821 return (PFalse fc))
822 <|> do lchar '_'; return Placeholder
823 <|> pSimpleExtExpr syn
825bracketed syn =
826 try (pPair syn)
827 <|> try (do e <- pExpr syn; lchar ')'; return e)
828-- <|> try (do reserved "typed"
829-- e <- pExpr syn; symbol ":"; t <- pExpr syn; lchar ')'
830-- return (PTyped e t))
831 <|> try (do fc <- pfc; o <- operator; e <- pExpr syn; lchar ')'
832 return $ PLam (MN 1000 "ARG") Placeholder
833 (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),
834 pexp e]))
835 <|> try (do fc <- pfc; e <- pSimpleExpr syn; o <- operator; lchar ')'
836 return $ PLam (MN 1000 "ARG") Placeholder
837 (PApp fc (PRef fc (UN o)) [pexp e,
838 pexp (PRef fc (MN 1000 "ARG"))]))
840pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
841pCaseOpt syn = do lhs <- pExpr (syn { inPattern = True })
842 symbol "=>"; rhs <- pExpr syn
843 return (lhs, rhs)
845-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
846-- big integer, otherwise try fromInteger and the constants as alternatives.
847-- a better solution would be to fix fromInteger to work with Integer, as the
848-- name suggests, rather than Int
850modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
851modifyConst syn fc (PConstant (BI x))
852 | not (inPattern syn)
853 = PAlternative False
854 (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI (fromInteger x)))]
855 : consts)
856 | otherwise = PAlternative False consts
857 where
858 consts = [ PConstant (BI x)
859 , PConstant (I (fromInteger x))
860 , PConstant (B8 (fromInteger x))
861 , PConstant (B16 (fromInteger x))
862 , PConstant (B32 (fromInteger x))
863 , PConstant (B64 (fromInteger x))
864 ]
865modifyConst syn fc x = x
868pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']'
869 return (mkList fc xs)
870 where
871 mkList fc [] = PRef fc (UN "Nil")
872 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
874pPair syn = try (do l <- pExpr syn
875 fc <- pfc
876 rest <- restTuple
877 case rest of
878 [] -> return l
879 [Left r] -> return (PPair fc l r)
880 [Right r] -> return (PDPair fc l Placeholder r))
881 <|> try (do x <- ntuple
882 lchar ')'
883 return x)
884 <|> do ln <- pName; lchar ':'
885 lty <- pExpr syn
886 reservedOp "**"
887 fc <- pfc
888 r <- pExpr syn
889 lchar ')'
890 return (PDPair fc (PRef fc ln) lty r)
891 where
892 restTuple = do lchar ')'; return []
893 <|> do lchar ','
894 r <- pExpr syn
895 lchar ')'
896 return [Left r]
897 <|> do reservedOp "**"
898 r <- pExpr syn
899 lchar ')'
900 return [Right r]
901 ntuple = try (do l <- pExpr syn; fc <- pfc; lchar ','
902 rest <- ntuple
903 return (PPair fc l rest))
904 <|> (do l <- pExpr syn; fc <- pfc; lchar ','
905 r <- pExpr syn
906 return (PPair fc l r))
908pAlt syn = do symbol "(|"; alts <- sepBy1 (pExpr' syn) (lchar ','); symbol "|)"
909 return (PAlternative False alts)
911pHSimpleExpr syn
912 = do lchar '.'
913 e <- pSimpleExpr syn
914 return $ PHidden e
915 <|> pSimpleExpr syn
917pMatchApp syn = do ty <- pSimpleExpr syn
918 symbol "<=="
919 fc <- pfc
920 f <- pfName
921 return (PLet (MN 0 "match")
922 ty
923 (PMatchApp fc f)
924 (PRef fc (MN 0 "match")))
926pUnifyLog syn = do lchar '%'; reserved "unifyLog";
927 tm <- pSimpleExpr syn
928 return (PUnifyLog tm)
930pApp syn = do f <- reserved "mkForeign"
931 fc <- pfc
932 fn <- pArg syn
933 args <- many (do notEndApp; pArg syn)
934 i <- getState
935 -- mkForeign f args ==>
936 -- liftPrimIO (\w => mkForeignPrim f args w)
937 let ap = PApp fc (PRef fc (UN "liftPrimIO"))
938 [pexp (PLam (MN 0 "w")
939 Placeholder
940 (PApp fc (PRef fc (UN "mkForeignPrim"))
941 (fn : args ++
942 [pexp (PRef fc (MN 0 "w"))])))]
943 return (dslify i ap)
945 <|> do f <- pSimpleExpr syn
946 fc <- pfc
947 args <- many1 (do notEndApp
948 pArg syn)
949 i <- getState
950 return (dslify i $ PApp fc f args)
951 where
952 dslify i (PApp fc (PRef _ f) [a])
953 | [d] <- lookupCtxt f (idris_dsls i)
954 = desugar (syn { dsl_info = d }) i (getTm a)
955 dslify i t = t
957pArg :: SyntaxInfo -> IParser PArg
958pArg syn = try (pImplicitArg syn)
959 <|> try (pConstraintArg syn)
960 <|> do e <- pSimpleExpr syn
961 return (pexp e)
963pImplicitArg syn = do lchar '{'
964 n <- pName
965 fc <- pfc
966 v <- option (PRef fc n) (do lchar '='
967 pExpr syn)
968 lchar '}'
969 return (pimp n v)
971pConstraintArg syn = do symbol "@{"
972 e <- pExpr syn
973 symbol "}"
974 return (pconst e)
976pRecordType syn
977 = do reserved "record"
978 lchar '{'
979 fields <- sepBy1 pFieldType (lchar ',')
980 lchar '}'
981 fc <- pfc
982 rec <- option Nothing (do e <- pSimpleExpr syn
983 return (Just e))
984 case rec of
985 Nothing ->
986 return (PLam (MN 0 "fldx") Placeholder
987 (applyAll fc fields (PRef fc (MN 0 "fldx"))))
988 Just v -> return (applyAll fc fields v)
989 where pFieldType = do n <- pfName
990 lchar '='
991 e <- pExpr syn
992 return (n, e)
993 applyAll fc [] x = x
994 applyAll fc ((n, e) : es) x
995 = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])
997mkType (UN n) = UN ("set_" ++ n)
998mkType (MN 0 n) = MN 0 ("set_" ++ n)
999mkType (NS n s) = NS (mkType n) s
1001noImp syn = syn { implicitAllowed = False }
1002impOK syn = syn { implicitAllowed = True }
1004pTSig syn = do lchar ':'; pTExpr syn
1006pTExpr syn = do cs <- if implicitAllowed syn then pConstList syn else return []
1007 sc <- pExpr syn
1008 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
1010pLambda syn = do lchar '\\'
1011 try (do xt <- tyOptDeclList syn
1012 symbol "=>"
1013 sc <- pExpr syn
1014 return (bindList PLam xt sc)
1015 <|> (do ps <- sepBy (do fc <- pfc
1016 e <- pSimpleExpr syn
1017 return (fc, e)) (lchar ',')
1018 symbol "=>"
1019 sc <- pExpr syn
1020 return (pmList (zip [0..] ps) sc)))
1021 where pmList [] sc = sc
1022 pmList ((i, (fc, x)) : xs) sc
1023 = PLam (MN i "lamp") Placeholder
1024 (PCase fc (PRef fc (MN i "lamp"))
1025 [(x, pmList xs sc)])
1027pRewriteTerm syn =
1028 do reserved "rewrite"
1029 fc <- pfc
1030 prf <- pExpr syn
1031 giving <- option Nothing
1032 (do symbol "==>"; tm <- pExpr' syn
1033 return (Just tm))
1034 reserved "in"; sc <- pExpr syn
1035 return (PRewrite fc
1036 (PApp fc (PRef fc (UN "sym")) [pexp prf]) sc
1037 giving)
1039pLet syn = try (do reserved "let"; n <- pName;
1040 ty <- option Placeholder (do lchar ':'; pExpr' syn)
1041 lchar '='
1042 v <- pExpr syn
1043 reserved "in"; sc <- pExpr syn
1044 return (PLet n ty v sc))
1045 <|> (do reserved "let"; fc <- pfc; pat <- pExpr' (syn { inPattern = True } )
1046 symbol "="; v <- pExpr syn
1047 reserved "in"; sc <- pExpr syn
1048 return (PCase fc v [(pat, sc)]))
1050pQuoteGoal syn = do reserved "quoteGoal"; n <- pName;
1051 reserved "by"
1052 r <- pExpr syn
1053 reserved "in"
1054 fc <- pfc
1055 sc <- pExpr syn
1056 return (PGoal fc r n sc)
1058pPi syn =
1059 try (do lazy <- if implicitAllowed syn -- laziness is top level only
1060 then option False (do lchar '|'; return True)
1061 else return False
1062 st <- pStatic
1063 lchar '('; xt <- tyDeclList syn; lchar ')'
1064 doc <- option "" (pDocComment '^')
1065 symbol "->"
1066 sc <- pExpr syn
1067 return (bindList (PPi (Exp lazy st doc)) xt sc))
1068 <|> try (if implicitAllowed syn
1069 then do lazy <- option False (do lchar '|'
1070 return True)
1071 st <- pStatic
1072 lchar '{'
1073 xt <- tyDeclList syn
1074 lchar '}'
1075 symbol "->"
1076 sc <- pExpr syn
1077 return (bindList (PPi (Imp lazy st "")) xt sc)
1078 else fail "No implicit arguments allowed here")
1079 <|> try (do lchar '{'
1080 reserved "auto"
1081 xt <- tyDeclList syn
1082 lchar '}'
1083 symbol "->"
1084 sc <- pExpr syn
1085 return (bindList (PPi
1086 (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))
1087 <|> try (do lchar '{'
1088 reserved "default"
1089 script <- pSimpleExpr syn
1090 xt <- tyDeclList syn
1091 lchar '}'
1092 symbol "->"
1093 sc <- pExpr syn
1094 return (bindList (PPi (TacImp False Dynamic script "")) xt sc))
1095 <|> do --lazy <- option False (do lchar '|'; return True)
1096 lchar '{'
1097 reserved "static"
1098 lchar '}'
1099 t <- pExpr' syn
1100 symbol "->"
1101 sc <- pExpr syn
1102 return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)
1104pConstList :: SyntaxInfo -> IParser [PTerm]
1105pConstList syn = try (do lchar '('
1106 tys <- sepBy1 (pExpr' (noImp syn)) (lchar ',')
1107 lchar ')'
1108 reservedOp "=>"
1109 return tys)
1110 <|> try (do t <- pExpr (noImp syn)
1111 reservedOp "=>"
1112 return [t])
1113 <|> return []
1115usingDeclList syn
1116 = try (sepBy1 (usingDecl syn) (lchar ','))
1117 <|> do ns <- sepBy1 pName (lchar ',')
1118 t <- pTSig (noImp syn)
1119 return (map (\x -> UImplicit x t) ns)
1121usingDecl syn = try (do x <- pfName
1122 t <- pTSig (noImp syn)
1123 return (UImplicit x t))
1124 <|> do c <- pfName
1125 xs <- many1 pfName
1126 return (UConstraint c xs)
1128tyDeclList syn = try (sepBy1 (do x <- pfName
1129 t <- pTSig (noImp syn)
1130 return (x,t))
1131 (lchar ','))
1132 <|> do ns <- sepBy1 pName (lchar ',')
1133 t <- pTSig (noImp syn)
1134 return (map (\x -> (x, t)) ns)
1136tyOptDeclList syn = sepBy1 (do x <- pNameOrPlaceholder
1137 t <- option Placeholder (do lchar ':'
1138 pExpr syn)
1139 return (x,t))
1140 (lchar ',')
1141 where pNameOrPlaceholder = pfName
1142 <|> do symbol "_"
1143 return (MN 0 "underscore")
1145bindList b [] sc = sc
1146bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
1148pComprehension syn
1149 = do lchar '['
1150 fc <- pfc
1151 pat <- pExpr syn
1152 lchar '|'
1153 qs <- sepBy1 (pDo syn) (lchar ',')
1154 lchar ']'
1155 return (PDoBlock (map addGuard qs ++
1156 [DoExp fc (PApp fc (PRef fc (UN "return"))
1157 [pexp pat])]))
1158 where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
1159 [pexp e])
1160 addGuard x = x
1162pDoBlock syn
1163 = do reserved "do"
1164 openBlock
1165 pushIndent
1166 ds <- many1 (do notEndBlock
1167 x <- pDo syn
1168 pKeepTerminator
1169 return x)
1170 popIndent
1171 closeBlock
1172 return (PDoBlock ds)
1174pDo syn
1175 = try (do reserved "let"
1176 i <- pName;
1177 ty <- option Placeholder (do lchar ':'
1178 pExpr' syn)
1179 reservedOp "="
1180 fc <- pfc
1181 e <- pExpr syn
1182 return (DoLet fc i ty e))
1183 <|> try (do reserved "let"
1184 i <- pExpr' syn
1185 reservedOp "="
1186 fc <- pfc
1187 sc <- pExpr syn
1188 return (DoLetP fc i sc))
1189 <|> try (do i <- pName
1190 symbol "<-"
1191 fc <- pfc
1192 e <- pExpr syn;
1193 return (DoBind fc i e))
1194 <|> try (do i <- pExpr' syn
1195 symbol "<-"
1196 fc <- pfc
1197 e <- pExpr syn;
1198 return (DoBindP fc i e))
1199 <|> try (do e <- pExpr syn
1200 fc <- pfc
1201 return (DoExp fc e))
1203pIdiom syn
1204 = do symbol "[|"
1205 fc <- pfc
1206 e <- pExpr syn
1207 symbol "|]"
1208 return (PIdiom fc e)
1210pConstant :: IParser Const
1211pConstant = do reserved "Integer";return (AType (ATInt ITBig))
1212 <|> do reserved "Int"; return (AType (ATInt ITNative))
1213 <|> do reserved "Char"; return (AType (ATInt ITChar))
1214 <|> do reserved "Float"; return (AType ATFloat)
1215 <|> do reserved "String"; return StrType
1216 <|> do reserved "Ptr"; return PtrType
1217 <|> do reserved "Bits8"; return (AType (ATInt (ITFixed IT8)))
1218 <|> do reserved "Bits16"; return (AType (ATInt (ITFixed IT16)))
1219 <|> do reserved "Bits32"; return (AType (ATInt (ITFixed IT32)))
1220 <|> do reserved "Bits64"; return (AType (ATInt (ITFixed IT64)))
1221 <|> do reserved "Bits8x16"; return (AType (ATInt (ITVec IT8 16)))
1222 <|> do reserved "Bits16x8"; return (AType (ATInt (ITVec IT16 8)))
1223 <|> do reserved "Bits32x4"; return (AType (ATInt (ITVec IT32 4)))
1224 <|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2)))
1225 <|> try (do f <- float; return $ Fl f)
1226 <|> try (do i <- natural; return $ BI i)
1227 <|> try (do s <- strlit; return $ Str s)
1228 <|> try (do c <- chlit; return $ Ch c)
1230pStatic :: IParser Static
1231pStatic = do lchar '['
1232 reserved "static"
1233 lchar ']';
1234 return Static
1235 <|> return Dynamic
1237table fixes
1238 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
1239 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]
1240 ++ toTable (reverse fixes) ++
1241 [[backtick],
1242 [binary "=" PEq AssocLeft],
1243 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
1245toTable fs = map (map toBin)
1246 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
1247 where toBin (Fix (PrefixN _) op) = prefix op
1248 (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
1249 toBin (Fix f op)
1250 = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
1251 assoc (Infixl _) = AssocLeft
1252 assoc (Infixr _) = AssocRight
1253 assoc (InfixN _) = AssocNone
1255binary name f = Infix (do fc <- pfc
1256 reservedOp name
1257 doc <- option "" (pDocComment '^')
1258 return (f fc))
1259prefix name f = Prefix (do reservedOp name
1260 fc <- pfc;
1261 return (f fc))
1262backtick = Infix (do lchar '`'; n <- pfName
1263 lchar '`'
1264 fc <- pfc
1265 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
1267--------- Data declarations ---------
1269-- (works for classes too - 'abstract' means the data/class is visible but members not)
1270accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()
1271accData (Just Frozen) n ns = do addAcc n (Just Frozen)
1272 mapM_ (\n -> addAcc n (Just Hidden)) ns
1273accData a n ns = do addAcc n a
1274 mapM_ (`addAcc` a) ns
1276pRecord :: SyntaxInfo -> IParser PDecl
1277pRecord syn = do doc <- option "" (pDocComment '|')
1278 acc <- pAccessibility
1279 reserved "record"
1280 fc <- pfc
1281 tyn_in <- pfName
1282 ty <- pTSig (impOK syn)
1283 let tyn = expandNS syn tyn_in
1284 reserved "where"
1285 openBlock
1286 pushIndent
1287 (cdoc, cn, cty, _) <- pConstructor syn
1288 pKeepTerminator
1289 popIndent
1290 closeBlock
1291 accData acc tyn [cn]
1292 let rsyn = syn { syn_namespace = show (nsroot tyn) :
1293 syn_namespace syn }
1294 let fns = getRecNames rsyn cty
1295 mapM_ (\n -> addAcc n acc) fns
1296 return $ PRecord doc rsyn fc tyn ty cdoc cn cty
1297 where
1298 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
1299 ++ getRecNames syn sc
1300 getRecNames _ _ = []
1302 toFreeze (Just Frozen) = Just Hidden
1303 toFreeze x = x
1305pDataI = do reserved "data"; return False
1306 <|> do reserved "codata"; return True
1308pData :: SyntaxInfo -> IParser PDecl
1309pData syn = try (do doc <- option "" (pDocComment '|')
1310 acc <- pAccessibility
1311 co <- pDataI
1312 fc <- pfc
1313 tyn_in <- pfName
1314 ty <- pTSig (impOK syn)
1315 let tyn = expandNS syn tyn_in
1316 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1317 reserved "where"
1318 openBlock
1319 pushIndent
1320 cons <- many (do notEndBlock
1321 c <- pConstructor syn
1322 pKeepTerminator
1323 return c) -- (lchar '|')
1324 popIndent
1325 closeBlock
1326 accData acc tyn (map (\ (_, n, _, _) -> n) cons)
1327 return $ PData doc syn fc co (PDatadecl tyn ty cons)))
1328 <|> try (do doc <- option "" (pDocComment '|')
1329 pushIndent
1330 acc <- pAccessibility
1331 co <- pDataI
1332 fc <- pfc
1333 tyn_in <- pfName
1334 args <- many pName
1335 let ty = bindArgs (map (const PType) args) PType
1336 let tyn = expandNS syn tyn_in
1337 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1338 try (lchar '=') <|> do reserved "where"
1339 let kw = (if co then "co" else "") ++ "data "
1340 let n = show tyn_in ++ " "
1341 let s = kw ++ n
1342 let as = concat (intersperse " " $ map show args) ++ " "
1343 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
1344 let ss = concat (intersperse " -> " $ map (const "Type") args)
1345 let fix1 = s ++ as ++ " = ..."
1346 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
1347 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
1348 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
1350 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
1351 pTerminator
1352 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
1353 cons' <- mapM (\ (doc, x, cargs, cfc) ->
1354 do let cty = bindArgs cargs conty
1355 return (doc, x, cty, cfc)) cons
1356 accData acc tyn (map (\ (_, n, _, _) -> n) cons')
1357 return $ PData doc syn fc co (PDatadecl tyn ty cons')))
1358 where
1359 mkPApp fc t [] = t
1360 mkPApp fc t xs = PApp fc t (map pexp xs)
1362bindArgs :: [PTerm] -> PTerm -> PTerm
1363bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
1365pConstructor :: SyntaxInfo -> IParser (String, Name, PTerm, FC)
1366pConstructor syn
1367 = do doc <- option "" (pDocComment '|')
1368 cn_in <- pfName; fc <- pfc
1369 let cn = expandNS syn cn_in
1370 ty <- pTSig (impOK syn)
1371-- ty' <- implicit syn cn ty
1372 return (doc, cn, ty, fc)
1375pSimpleCon :: SyntaxInfo -> IParser (String, Name, [PTerm], FC)
1376pSimpleCon syn
1377 = do cn_in <- pfName
1378 let cn = expandNS syn cn_in
1379 fc <- pfc
1380 args <- many (do notEndApp
1381 pSimpleExpr syn)
1382 doc <- option "" (pDocComment '^')
1383 return (doc, cn, args, fc)
1385--------- DSL syntax overloading ---------
1387pDSL :: SyntaxInfo -> IParser PDecl
1388pDSL syn = do reserved "dsl"
1389 n <- pfName
1390 openBlock
1391 pushIndent
1392 bs <- many1 (do notEndBlock
1393 b <- pOverload syn
1394 pKeepTerminator
1395 return b)
1396 popIndent; closeBlock
1397 let dsl = mkDSL bs (dsl_info syn)
1398 checkDSL dsl
1399 i <- getState
1400 setState (i { idris_dsls = addDef n dsl (idris_dsls i) })
1401 return (PDSL n dsl)
1402 where mkDSL bs dsl = let var = lookup "variable" bs
1403 first = lookup "index_first" bs
1404 next = lookup "index_next" bs
1405 leto = lookup "let" bs
1406 lambda = lookup "lambda" bs in
1407 initDSL { dsl_var = var,
1408 index_first = first,
1409 index_next = next,
1410 dsl_lambda = lambda,
1411 dsl_let = leto }
1413checkDSL :: DSL -> IParser ()
1414checkDSL dsl = return ()
1416pOverload :: SyntaxInfo -> IParser (String, PTerm)
1417pOverload syn = do o <- identifier <|> do reserved "let"
1418 return "let"
1419 if o `notElem` overloadable
1420 then fail $ show o ++ " is not an overloading"
1421 else do
1422 lchar '='
1423 t <- pExpr syn
1424 return (o, t)
1425 where overloadable = ["let","lambda","index_first","index_next","variable"]
1427--------- Pattern match clauses ---------
1429pPattern :: SyntaxInfo -> IParser PDecl
1430pPattern syn = do fc <- pfc
1431 clause <- pClause syn
1432 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
1434pCAF :: SyntaxInfo -> IParser PDecl
1435pCAF syn = do reserved "let"
1436 n_in <- pfName; let n = expandNS syn n_in
1437 lchar '='
1438 t <- pExpr syn
1439 pTerminator
1440 fc <- pfc
1441 return (PCAF fc n t)
1443pArgExpr syn = let syn' = syn { inPattern = True } in
1444 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
1446pRHS :: SyntaxInfo -> Name -> IParser PTerm
1447pRHS syn n = do lchar '='; pExpr syn
1448 <|> do symbol "?=";
1449 name <- option n' (do symbol "{"; n <- pfName; symbol "}";
1450 return n)
1451 rhs <- pExpr syn
1452 return (addLet name rhs)
1453 <|> do reserved "impossible"; return PImpossible
1454 where mkN (UN x) = UN (x++"_lemma_1")
1455 mkN (NS x n) = NS (mkN x) n
1456 n' = mkN n
1458 addLet nm (PLet n ty val rhs) = PLet n ty val (addLet nm rhs)
1459 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
1460 where addLetC (l, r) = (l, addLet nm r)
1461 addLet nm rhs = (PLet (UN "value") Placeholder rhs (PMetavar nm))
1463pClause :: SyntaxInfo -> IParser PClause
1464pClause syn
1465 = try (do pushIndent
1466 n_in <- pfName; let n = expandNS syn n_in
1467 cargs <- many (pConstraintArg syn)
1468 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1469 fc <- pfc
1470 args <- many (try (pImplicitArg (syn { inPattern = True } ))
1471 <|> (fmap pexp (pArgExpr syn)))
1472 wargs <- many (pWExpr syn)
1473 rhs <- pRHS syn n
1474 ist <- getState
1475 let ctxt = tt_ctxt ist
1476 let wsyn = syn { syn_namespace = [] }
1477 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1478 popIndent
1479 return x,
1480 do pTerminator
1481 return ([], [])]
1482 let capp = PApp fc (PRef fc n)
1483 (iargs ++ cargs ++ args)
1484 ist <- getState
1485 setState (ist { lastParse = Just n })
1486 return $ PClause fc n capp wargs rhs wheres)
1487 <|> try (do pushIndent
1488 ty <- pSimpleExpr syn
1489 symbol "<=="
1490 fc <- pfc
1491 n_in <- pfName; let n = expandNS syn n_in
1492 rhs <- pRHS syn n
1493 ist <- getState
1494 let ctxt = tt_ctxt ist
1495 let wsyn = syn { syn_namespace = [] }
1496 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1497 popIndent
1498 return x,
1499 do pTerminator
1500 return ([], [])]
1501 let capp = PLet (MN 0 "match")
1502 ty
1503 (PMatchApp fc n)
1504 (PRef fc (MN 0 "match"))
1505 ist <- getState
1506 setState (ist { lastParse = Just n })
1507 return $ PClause fc n capp [] rhs wheres)
1508 <|> try (do pushIndent
1509 wargs <- many1 (pWExpr syn)
1510 ist <- getState
1511 n <- case lastParse ist of
1512 Just t -> return t
1513 Nothing -> fail "Invalid clause"
1514 fc <- pfc
1515 rhs <- pRHS syn n
1516 let ctxt = tt_ctxt ist
1517 let wsyn = syn { syn_namespace = [] }
1518 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1519 popIndent
1520 return x,
1521 do pTerminator
1522 return ([], [])]
1523 return $ PClauseR fc wargs rhs wheres)
1525 <|> try (do pushIndent
1526 n_in <- pfName; let n = expandNS syn n_in
1527 cargs <- many (pConstraintArg syn)
1528 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1529 fc <- pfc
1530 args <- many (try (pImplicitArg (syn { inPattern = True } ))
1531 <|> (fmap pexp (pArgExpr syn)))
1532 wargs <- many (pWExpr syn)
1533 let capp = PApp fc (PRef fc n)
1534 (iargs ++ cargs ++ args)
1535 ist <- getState
1536 setState (ist { lastParse = Just n })
1537 reserved "with"
1538 wval <- pSimpleExpr syn
1539 openBlock
1540 ds <- many1 $ pFunDecl syn
1541 let withs = map (fillLHSD n capp wargs) $ concat ds
1542 closeBlock
1543 popIndent
1544 return $ PWith fc n capp wargs wval withs)
1546 <|> try (do wargs <- many1 (pWExpr syn)
1547 fc <- pfc
1548 reserved "with"
1549 wval <- pSimpleExpr syn
1550 openBlock
1551 ds <- many1 $ pFunDecl syn
1552 let withs = concat ds
1553 closeBlock
1554 return $ PWithR fc wargs wval withs)
1556 <|> do pushIndent
1557 l <- pArgExpr syn
1558 op <- operator
1559 let n = expandNS syn (UN op)
1560 r <- pArgExpr syn
1561 fc <- pfc
1562 wargs <- many (pWExpr syn)
1563 rhs <- pRHS syn n
1564 let wsyn = syn { syn_namespace = [] }
1565 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1566 popIndent
1567 return x,
1568 do pTerminator
1569 return ([], [])]
1570 ist <- getState
1571 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1572 setState (ist { lastParse = Just n })
1573 return $ PClause fc n capp wargs rhs wheres
1575 <|> do l <- pArgExpr syn
1576 op <- operator
1577 let n = expandNS syn (UN op)
1578 r <- pArgExpr syn
1579 fc <- pfc
1580 wargs <- many (pWExpr syn)
1581 reserved "with"
1582 wval <- pSimpleExpr syn
1583 openBlock
1584 ds <- many1 $ pFunDecl syn
1585 closeBlock
1586 ist <- getState
1587 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1588 let withs = map (fillLHSD n capp wargs) $ concat ds
1589 setState (ist { lastParse = Just n })
1590 return $ PWith fc n capp wargs wval withs
1591 where
1592 fillLHS n capp owargs (PClauseR fc wargs v ws)
1593 = PClause fc n capp (owargs ++ wargs) v ws
1594 fillLHS n capp owargs (PWithR fc wargs v ws)
1595 = PWith fc n capp (owargs ++ wargs) v
1596 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1597 fillLHS _ _ _ c = c
1599 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1600 fillLHSD n c a x = x
1602pWExpr :: SyntaxInfo -> IParser PTerm
1603pWExpr syn = do lchar '|'
1604 pExpr' syn
1606pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
1607pWhereblock n syn
1608 = do reserved "where"; openBlock
1609 ds <- many1 $ pDecl syn
1610 let dns = concatMap (concatMap declared) ds
1611 closeBlock
1612 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1614pCodegen :: IParser Codegen
1615pCodegen = try (do reserved "C"; return ViaC)
1616 <|> try (do reserved "Java"; return ViaJava)
1617 <|> try (do reserved "JavaScript"; return ViaJavaScript)
1618 <|> try (do reserved "Node"; return ViaNode)
1619 <|> try (do reserved "LLVM"; return ViaLLVM)
1620 <|> try (do reserved "Bytecode"; return Bytecode)
1622pDirective :: SyntaxInfo -> IParser [PDecl]
1623pDirective syn = try (do lchar '%'; reserved "lib"; cgn <- pCodegen; lib <- strlit;
1624 return [PDirective (do addLib cgn lib
1625 addIBC (IBCLib cgn lib))])
1626 <|> try (do lchar '%'; reserved "link"; cgn <- pCodegen; obj <- strlit;
1627 return [PDirective (do dirs <- allImportDirs
1628 o <- liftIO $ findInPath dirs obj
1629 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
1630 addObjectFile cgn o)])
1631 <|> try (do lchar '%'; reserved "flag"; cgn <- pCodegen;
1632 flag <- strlit
1633 return [PDirective (do addIBC (IBCCGFlag cgn flag)
1634 addFlag cgn flag)])
1635 <|> try (do lchar '%'; reserved "include"; cgn <- pCodegen; hdr <- strlit;
1636 return [PDirective (do addHdr cgn hdr
1637 addIBC (IBCHeader cgn hdr))])
1638 <|> try (do lchar '%'; reserved "hide"; n <- iName []
1639 return [PDirective (do setAccessibility n Hidden
1640 addIBC (IBCAccess n Hidden))])
1641 <|> try (do lchar '%'; reserved "freeze"; n <- iName []
1642 return [PDirective (do setAccessibility n Frozen
1643 addIBC (IBCAccess n Frozen))])
1644 <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'
1645 return [PDirective (do i <- getIState
1646 putIState (i { default_access = acc }))])
1647 <|> try (do lchar '%'; reserved "default"; tot <- pTotality
1648 i <- getState
1649 setState (i { default_total = tot } )
1650 return [PDirective (do i <- getIState
1651 putIState (i { default_total = tot }))])
1652 <|> try (do lchar '%'; reserved "logging"; i <- natural;
1653 return [PDirective (setLogLevel (fromInteger i))])
1654 <|> try (do lchar '%'; reserved "dynamic"; libs <- sepBy1 strlit (lchar ',');
1655 return [PDirective (do added <- addDyLib libs
1656 case added of
1657 Left lib -> addIBC (IBCDyLib (lib_name lib))
1658 Right msg ->
1659 fail $ msg)])
1660 <|> try (do lchar '%'; reserved "language"; ext <- reserved "TypeProviders";
1661 return [PDirective (addLangExt TypeProviders)])
1663pProvider :: SyntaxInfo -> IParser [PDecl]
1664pProvider syn = do lchar '%'; reserved "provide";
1665 lchar '('; n <- pfName; t <- pTSig syn; lchar ')'
1666 fc <- pfc
1667 reserved "with"
1668 e <- pExpr syn
1669 return [PProvider syn fc n t e]
1671pTransform :: SyntaxInfo -> IParser [PDecl]
1672pTransform syn = do lchar '%'; reserved "transform";
1673 -- leave it unchecked, until we work out what this should
1674 -- actually mean...
1675-- safety <- option True (do reserved "unsafe"
1676-- return False)
1677 lhs <- pExpr syn
1678 fc <- pfc
1679 symbol "==>"
1680 rhs <- pExpr syn
1681 return [PTransform fc False lhs rhs]
1683pTactic :: SyntaxInfo -> IParser PTactic
1684pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
1685 return $ Intro ns
1686 <|> do reserved "intros"; return Intros
1687 <|> try (do reserved "refine"; n <- pName
1688 imps <- many1 imp
1689 return $ Refine n imps)
1690 <|> do reserved "refine"; n <- pName
1691 i <- getState
1692 return $ Refine n []
1693 <|> do reserved "mrefine"; n <- pName
1694 i <- getState
1695 return $ MatchRefine n
1696 <|> do reserved "rewrite"; t <- pExpr syn;
1697 i <- getState
1698 return $ Rewrite (desugar syn i t)
1699 <|> do reserved "equiv"; t <- pExpr syn;
1700 i <- getState
1701 return $ Equiv (desugar syn i t)
1702 <|> try (do reserved "let"; n <- pName; lchar ':';
1703 ty <- pExpr' syn; lchar '='; t <- pExpr syn;
1704 i <- getState
1705 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
1706 <|> try (do reserved "let"; n <- pName; lchar '=';
1707 t <- pExpr syn;
1708 i <- getState
1709 return $ LetTac n (desugar syn i t))
1710 <|> do reserved "focus"; n <- pName
1711 return $ Focus n
1712 <|> do reserved "exact"; t <- pExpr syn;
1713 i <- getState
1714 return $ Exact (desugar syn i t)
1715 <|> do reserved "applyTactic"; t <- pExpr syn;
1716 i <- getState
1717 return $ ApplyTactic (desugar syn i t)
1718 <|> do reserved "reflect"; t <- pExpr syn;
1719 i <- getState
1720 return $ Reflect (desugar syn i t)
1721 <|> do reserved "fill"; t <- pExpr syn;
1722 i <- getState
1723 return $ Fill (desugar syn i t)
1724 <|> do reserved "try"; t <- pTactic syn;
1725 lchar '|';
1726 t1 <- pTactic syn
1727 return $ Try t t1
1728 <|> do lchar '{'
1729 t <- pTactic syn;
1730 lchar ';';
1731 t1 <- pTactic syn;
1732 lchar '}'
1733 return $ TSeq t t1
1734 <|> do reserved "compute"; return Compute
1735 <|> do reserved "trivial"; return Trivial
1736 <|> do reserved "solve"; return Solve
1737 <|> do reserved "attack"; return Attack
1738 <|> do reserved "state"; return ProofState
1739 <|> do reserved "term"; return ProofTerm
1740 <|> do reserved "undo"; return Undo
1741 <|> do reserved "qed"; return Qed
1742 <|> do reserved "abandon"; return Abandon
1743 <|> do lchar ':'; reserved "q"; return Abandon
1744 where
1745 imp = do lchar '?'; return False
1746 <|> do lchar '_'; return True