git.iko.soy/Idris-dev
on 031ffb4 help sign in
Idris-dev/src/Idris/Parser.hs
1651 lines 66 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 i
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 "")
93loadSource :: Bool -> FilePath -> Idris ()
94loadSource lidr f
95 = do iLOG ("Reading " ++ f)
96 i <- getIState
97 let def_total = default_total i
98 file_in <- liftIO $ readFile f
99 file <- if lidr then tclift $ unlit f file_in else return file_in
100 (mname, modules, rest, pos) <- parseImports f file
101 i <- getIState
102 putIState (i { default_access = Hidden })
103 mapM_ loadModule modules
104 clearIBC -- start a new .ibc file
105 mapM_ (addIBC . IBCImport) modules
106 ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
107 f rest pos
108 unless (null ds') $ do
109 let ds = namespaces mname ds'
110 logLvl 3 (dumpDecls ds)
111 i <- getIState
112 logLvl 10 (show (toAlist (idris_implicits i)))
113 logLvl 3 (show (idris_infixes i))
114 -- Now add all the declarations to the context
115 v <- verbose
116 when v $ iputStrLn $ "Type checking " ++ f
117 elabDecls toplevel ds
118 i <- getIState
119 -- simplify every definition do give the totality checker
120 -- a better chance
121 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
122 updateContext (simplifyCasedef n))
123 (map snd (idris_totcheck i))
124 -- build size change graph from simplified definitions
125 iLOG "Totality checking"
126 i <- getIState
127 mapM_ buildSCG (idris_totcheck i)
128 mapM_ checkDeclTotality (idris_totcheck i)
129 iLOG ("Finished " ++ f)
130 ibcsd <- valIBCSubDir i
131 let ibc = ibcPathNoFallback ibcsd f
132 iLOG "Universe checking"
133 iucheck
134 i <- getIState
135 addHides (hide_list i)
136 ok <- noErrors
137 when ok $
138 idrisCatch (do writeIBC f ibc; clearIBC)
139 (\c -> return ()) -- failure is harmless
140 i <- getIState
141 putIState (i { default_total = def_total,
142 hide_list = [] })
143 return ()
144 return ()
145 where
146 namespaces [] ds = ds
147 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
149addHides :: [(Name, Maybe Accessibility)] -> Idris ()
150addHides xs = do i <- getIState
151 let defh = default_access i
152 let (hs, as) = partition isNothing xs
153 unless (null as) $
154 mapM_ doHide
155 (map (\ (n, _) -> (n, defh)) hs ++
156 map (\ (n, Just a) -> (n, a)) as)
157 where isNothing (_, Nothing) = True
158 isNothing _ = False
160 doHide (n, a) = do setAccessibility n a
161 addIBC (IBCAccess n a)
163parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"
164parseTac i = runParser (do t <- pTactic defaultSyntax
165 eof
166 return t) i "(proof)"
168parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)
169parseImports fname input
170 = do i <- getIState
171 case runParser (do whiteSpace
172 mname <- pHeader
173 ps <- many pImport
174 rest <- getInput
175 pos <- getPosition
176 return ((mname, ps, rest, pos), i)) i fname input of
177 Left err -> fail (show err)
178 Right (x, i) -> do putIState i
179 return x
181pHeader :: IParser [String]
182pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')
183 return (parseName i))
184 <|> return []
185 where parseName x = case span (/='.') x of
186 (x, "") -> [x]
187 (x, '.':y) -> x : parseName y
189pushIndent :: IParser ()
190pushIndent = do pos <- getPosition
191 ist <- getState
192 setState (ist { indent_stack = sourceColumn pos :
193 indent_stack ist })
195lastIndent :: IParser Int
196lastIndent = do ist <- getState
197 case indent_stack ist of
198 (x : xs) -> return x
199 _ -> return 1
201indent :: IParser Int
202indent = liftM sourceColumn getPosition
204popIndent :: IParser ()
205popIndent = do ist <- getState
206 let (x : xs) = indent_stack ist
207 setState (ist { indent_stack = xs })
209openBlock :: IParser ()
210openBlock = do lchar '{'
211 ist <- getState
212 setState (ist { brace_stack = Nothing : brace_stack ist })
213 <|> do ist <- getState
214 lvl <- indent
215 setState (ist { brace_stack = Just lvl : brace_stack ist })
217closeBlock :: IParser ()
218closeBlock = do ist <- getState
219 bs <- case brace_stack ist of
220 [] -> eof >> return []
221 Nothing : xs -> (lchar '}' >> return xs) <|> (eof >> return [])
222 Just lvl : xs -> (do i <- indent
223 inp <- getInput
224-- trace (show (take 10 inp, i, lvl)) $
225 if i >= lvl && take 1 inp /= ")"
226 then fail "Not end of block"
227 else return xs) <|> (eof >> return [])
228 setState (ist { brace_stack = bs })
230pTerminator = do lchar ';'; popIndent
231 <|> do c <- indent; l <- lastIndent
232 if c <= l
233 then popIndent
234 else fail "Not a terminator"
235 <|> do i <- getInput
236 if "}" `isPrefixOf` i || ")" `isPrefixOf` i
237 then popIndent
238 else fail "Not a terminator"
239 <|> lookAhead eof
241pBarTerminator
242 = do lchar '|'; return ()
243 <|> do c <- indent; l <- lastIndent
244 unless (c <= l) $ fail "Not a terminator"
245 <|> lookAhead eof
247pKeepTerminator
248 = do lchar ';'; return ()
249 <|> do c <- indent; l <- lastIndent
250 unless (c <= l) $ fail "Not a terminator"
251 <|> do i <- getInput
252 let h = take 1 i
253 unless (h `elem` ["}", ")", "|"]) $ fail "Not a terminator"
254 <|> lookAhead eof
256notEndApp = do c <- indent; l <- lastIndent
257 i <- getInput
258 when (c <= l) $ fail "Terminator"
260notEndBlock = do ist <- getState
261 case brace_stack ist of
262 Just lvl : xs -> do i <- indent
263 inp <- getInput
264 when (i < lvl || ")" `isPrefixOf` inp) $ fail "End of block"
265 _ -> return ()
267-- | Use Parsec's internal state to construct a source code position
268pfc :: IParser FC
269pfc = do s <- getPosition
270 let (dir, file) = splitFileName (sourceName s)
271 let f = if dir == addTrailingPathSeparator "." then file else sourceName s
272 return $ FC f (sourceLine s)
274pImport :: IParser String
275pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')
276 return (toPath f)
277 where toPath n = foldl1' (</>) $ splitOn "." n
279-- | A program is a list of declarations, possibly with associated
280-- documentation strings.
281parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos ->
282 Idris [PDecl]
283parseProg syn fname input pos
284 = do i <- getIState
285 case runParser (do setPosition pos
286 whiteSpace
287 ps <- many (pDecl syn)
288 eof
289 i' <- getState
290 return (concat ps, i')) i fname input of
291 Left err -> do iputStrLn (show err)
292 return []
293 Right (x, i) -> do putIState i
294 return (collect x)
296-- | Collect 'PClauses' with the same function name
297collect :: [PDecl] -> [PDecl]
298collect (c@(PClauses _ o _ _) : ds)
299 = clauses (cname c) [] (c : ds)
300 where clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)
301 | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds
302 clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds)
303 | n == n' = clauses j (PWith fc' n' l ws r (collect w) : acc) ds
304 clauses (Just n) acc xs = PClauses (getfc c) o n (reverse acc) : collect xs
305 clauses Nothing acc (x:xs) = collect xs
306 clauses Nothing acc [] = []
308 cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n
309 cname (PClauses fc _ _ [PWith _ n _ _ _ _]) = Just n
310 cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing
311 cname (PClauses fc _ _ [PWithR _ _ _ _]) = Nothing
312 getfc (PClauses fc _ _ _) = fc
314collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
315collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds
316collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds
317collect (PClass doc f s cs n ps ds : ds')
318 = PClass doc f s cs n ps (collect ds) : collect ds'
319collect (PInstance f s cs n ps t en ds : ds')
320 = PInstance f s cs n ps t en (collect ds) : collect ds'
321collect (d : ds) = d : collect ds
322collect [] = []
324pFullExpr :: SyntaxInfo -> IParser PTerm
325pFullExpr syn
326 = do x <- pExpr syn; eof;
327 i <- getState
328 return $ desugar syn i x
330-- | Parse a top-level declaration
331pDecl :: SyntaxInfo -> IParser [PDecl]
332pDecl syn = do notEndBlock
333 pDeclBody where
334 pDeclBody
335 = do d <- pDecl' syn
336 i <- getState
337 let d' = fmap (desugar syn i) d
338 return [d']
339 <|> pUsing syn
340 <|> pParams syn
341 <|> pMutual syn
342 <|> pNamespace syn
343 <|> pClass syn
344 <|> pInstance syn
345 <|> do d <- pDSL syn; return [d]
346 <|> pDirective syn
347 <|> pProvider syn
348 <|> try (do reserved "import"; fp <- identifier
349 fail "imports must be at the top of file")
351pFunDecl :: SyntaxInfo -> IParser [PDecl]
352pFunDecl syn
353 = try (do notEndBlock
354 d <- pFunDecl' syn
355 i <- getState
356 let d' = fmap (desugar syn i) d
357 return [d'])
359--------- Top Level Declarations ---------
361pDecl' :: SyntaxInfo -> IParser PDecl
362pDecl' syn
363 = try pFixity
364 <|> try (pFunDecl' syn)
365 <|> try (pData syn)
366 <|> try (pRecord syn)
367 <|> try (pSyntaxDecl syn)
369pSyntaxDecl :: SyntaxInfo -> IParser PDecl
370pSyntaxDecl syn
371 = do s <- pSyntaxRule syn
372 i <- getState
373 let rs = syntax_rules i
374 let ns = syntax_keywords i
375 let ibc = ibc_write i
376 let ks = map show (names s)
377 setState (i { syntax_rules = s : rs,
378 syntax_keywords = ks ++ ns,
379 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc
380 })
381 fc <- pfc
382 return (PSyntax fc s)
383 where
384 names (Rule syms _ _) = mapMaybe ename syms
385 ename (Keyword n) = Just n
386 ename _ = Nothing
388pSyntaxRule :: SyntaxInfo -> IParser Syntax
389pSyntaxRule syn
390 = do pushIndent
391 sty <- option AnySyntax (do reserved "term"; return TermSyntax
392 <|> do reserved "pattern"; return PatternSyntax)
393 reserved "syntax"
394 syms <- many1 pSynSym
395 when (all expr syms) $ fail "No keywords in syntax rule"
396 let ns = mapMaybe name syms
397 when (length ns /= length (nub ns))
398 $ fail "Repeated variable in syntax rule"
399 lchar '='
400 tm <- pTExpr (impOK syn)
401 pTerminator
402 return (Rule (mkSimple syms) tm sty)
403 where
404 expr (Expr _) = True
405 expr _ = False
406 name (Expr n) = Just n
407 name _ = Nothing
409 -- Can't parse two full expressions (i.e. expressions with application) in a row
410 -- so change them both to a simple expression
412 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
413 mkSimple xs = mkSimple' xs
415 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
416 mkSimple es
417 mkSimple' (e : es) = e : mkSimple' es
418 mkSimple' [] = []
420pSynSym :: IParser SSymbol
421pSynSym = try (do lchar '['; n <- pName; lchar ']'
422 return (Expr n))
423 <|> try (do lchar '{'; n <- pName; lchar '}'
424 return (Binding n))
425 <|> do n <- iName []
426 return (Keyword n)
427 <|> do sym <- strlit
428 return (Symbol sym)
430pFunDecl' :: SyntaxInfo -> IParser PDecl
431pFunDecl' syn = try (do doc <- option "" (pDocComment '|')
432 pushIndent
433 ist <- getState
434 let initOpts = if default_total ist
435 then [TotalFn]
436 else []
437 opts <- pFnOpts initOpts
438 acc <- pAccessibility
439 opts' <- pFnOpts opts
440 n_in <- pfName
441 let n = expandNS syn n_in
442 fc <- pfc
443 ty <- pTSig (impOK syn)
444 pTerminator
445-- ty' <- implicit syn n ty
446 addAcc n acc
447 return (PTy doc syn fc opts' n ty))
448 <|> try (pPostulate syn)
449 <|> try (pPattern syn)
450 <|> try (pCAF syn)
452pPostulate :: SyntaxInfo -> IParser PDecl
453pPostulate syn = do doc <- option "" (pDocComment '|')
454 pushIndent
455 reserved "postulate"
456 ist <- getState
457 let initOpts = if default_total ist
458 then [TotalFn]
459 else []
460 opts <- pFnOpts initOpts
461 acc <- pAccessibility
462 opts' <- pFnOpts opts
463 n_in <- pfName
464 let n = expandNS syn n_in
465 ty <- pTSig (impOK syn)
466 fc <- pfc
467 pTerminator
468 addAcc n acc
469 return (PPostulate doc syn fc opts' n ty)
472pUsing :: SyntaxInfo -> IParser [PDecl]
473pUsing syn =
474 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
475 openBlock
476 let uvars = using syn
477 ds <- many1 (pDecl (syn { using = uvars ++ ns }))
478 closeBlock
479 return (concat ds)
481pParams :: SyntaxInfo -> IParser [PDecl]
482pParams syn =
483 do reserved "parameters"; lchar '('; ns <- tyDeclList syn; lchar ')'
484 openBlock
485 let pvars = syn_params syn
486 ds <- many1 (pDecl syn { syn_params = pvars ++ ns })
487 closeBlock
488 fc <- pfc
489 return [PParams fc ns (concat ds)]
491pMutual :: SyntaxInfo -> IParser [PDecl]
492pMutual syn =
493 do reserved "mutual"
494 openBlock
495 let pvars = syn_params syn
496 ds <- many1 (pDecl syn)
497 closeBlock
498 fc <- pfc
499 return [PMutual fc (concat ds)]
501pNamespace :: SyntaxInfo -> IParser [PDecl]
502pNamespace syn =
503 do reserved "namespace"; n <- identifier;
504 openBlock
505 ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
506 closeBlock
507 return [PNamespace n (concat ds)]
509--------- Fixity ---------
511pFixity :: IParser PDecl
512pFixity = do pushIndent
513 f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
514 pTerminator
515 let prec = fromInteger i
516 istate <- getState
517 let infixes = idris_infixes istate
518 let fs = map (Fix (f prec)) ops
519 let redecls = map (alreadyDeclared infixes) fs
520 let ill = filter (not . checkValidity) redecls
521 if null ill
522 then do setState (istate { idris_infixes = nub $ sort (fs ++ infixes)
523 , ibc_write = map IBCFix fs ++ ibc_write istate
524 })
525 fc <- pfc
526 return (PFix fc (f prec) ops)
527 else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
528 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
529 where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
530 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
532 checkValidity :: (FixDecl, [FixDecl]) -> Bool
533 checkValidity (f, fs) = all (== f) fs
535 extractName :: FixDecl -> String
536 extractName (Fix _ n) = n
538fixity :: IParser (Int -> Fixity)
539fixity = try (do reserved "infixl"; return Infixl)
540 <|> try (do reserved "infixr"; return Infixr)
541 <|> try (do reserved "infix"; return InfixN)
542 <|> try (do reserved "prefix"; return PrefixN)
544--------- Type classes ---------
546pClass :: SyntaxInfo -> IParser [PDecl]
547pClass syn = do doc <- option "" (pDocComment '|')
548 acc <- pAccessibility
549 reserved "class"; fc <- pfc; cons <- pConstList syn; n_in <- pName
550 let n = expandNS syn n_in
551 cs <- many carg
552 reserved "where"; openBlock
553 ds <- many $ pFunDecl syn
554 closeBlock
555 let allDs = concat ds
556 accData acc n (concatMap declared allDs)
557 return [PClass doc syn fc cons n cs allDs]
558 where
559 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'
560 return (i, ty)
561 <|> do i <- pName;
562 return (i, PType)
564pInstance :: SyntaxInfo -> IParser [PDecl]
565pInstance syn = do reserved "instance"; fc <- pfc
566 en <- option Nothing
567 (do lchar '['; n_in <- pfName; lchar ']'
568 let n = expandNS syn n_in
569 return (Just n))
570 cs <- pConstList syn
571 cn <- pName
572 args <- many (pSimpleExpr syn)
573 let sc = PApp fc (PRef fc cn) (map pexp args)
574 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
575 reserved "where"; openBlock
576 ds <- many $ pFunDecl syn
577 closeBlock
578 return [PInstance syn fc cs cn args t en (concat ds)]
580--------- Expressions ---------
582pExpr syn = do i <- getState
583 buildExpressionParser (table (idris_infixes i)) (pExpr' syn)
585pExpr' :: SyntaxInfo -> IParser PTerm
586pExpr' syn
587 = try (pExtExpr syn)
588 <|> pNoExtExpr syn
590pExtExpr :: SyntaxInfo -> IParser PTerm
591pExtExpr syn = do i <- getState
592 pExtensions syn (syntax_rules i)
594pSimpleExtExpr :: SyntaxInfo -> IParser PTerm
595pSimpleExtExpr syn = do i <- getState
596 pExtensions syn (filter simple (syntax_rules i))
597 where
598 simple (Rule (Expr x:xs) _ _) = False
599 simple (Rule (SimpleExpr x:xs) _ _) = False
600 simple (Rule [Keyword _] _ _) = True
601 simple (Rule [Symbol _] _ _) = True
602 simple (Rule (_:xs) _ _) = case last xs of
603 Keyword _ -> True
604 Symbol _ -> True
605 _ -> False
606 simple _ = False
608pNoExtExpr syn =
609 try (pApp syn)
610 <|> try (pMatchApp syn)
611 <|> try (pUnifyLog syn)
612 <|> pRecordType syn
613 <|> try (pSimpleExpr syn)
614 <|> pLambda syn
615 <|> pLet syn
616 <|> pRewriteTerm syn
617 <|> pPi syn
618 <|> pDoBlock syn
620pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
621pExtensions syn rules = choice (map (try . pExt syn) (filter valid rules))
622 where
623 valid (Rule _ _ AnySyntax) = True
624 valid (Rule _ _ PatternSyntax) = inPattern syn
625 valid (Rule _ _ TermSyntax) = not (inPattern syn)
628data SynMatch = SynTm PTerm | SynBind Name
630pExt :: SyntaxInfo -> Syntax -> IParser PTerm
631pExt syn (Rule ssym ptm _)
632 = do smap <- mapM pSymbol ssym
633 let ns = mapMaybe id smap
634 return (update ns ptm) -- updated with smap
635 where
636 pSymbol (Keyword n) = do reserved (show n); return Nothing
637 pSymbol (Expr n) = do tm <- pExpr syn
638 return $ Just (n, SynTm tm)
639 pSymbol (SimpleExpr n) = do tm <- pSimpleExpr syn
640 return $ Just (n, SynTm tm)
641 pSymbol (Binding n) = do b <- pName
642 return $ Just (n, SynBind b)
643 pSymbol (Symbol s) = do symbol s
644 return Nothing
645 dropn n [] = []
646 dropn n ((x,t) : xs) | n == x = xs
647 | otherwise = (x,t):dropn n xs
649 updateB ns n = case lookup n ns of
650 Just (SynBind t) -> t
651 _ -> n
653 update ns (PRef fc n) = case lookup n ns of
654 Just (SynTm t) -> t
655 _ -> PRef fc n
656 update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)
657 update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc)
658 update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)
659 (update (dropn n ns) sc)
660 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
661 update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)
662 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)
663 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)
664 update ns (PAlternative a as) = PAlternative a (map (update ns) as)
665 update ns (PHidden t) = PHidden (update ns t)
666 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
667 where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
668 upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds
669 upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)
670 : upd (dropn n ns) ds
671 upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t)
672 : upd ns ds
673 upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)
674 : upd ns ds
675 update ns t = t
677pName = do i <- getState
678 iName (syntax_keywords i)
679 <|> do reserved "instance"
680 i <- getState
681 UN n <- iName (syntax_keywords i)
682 return (UN ('@':n))
684-- | Parser for an operator in function position, i.e. enclosed by `()', with an
685-- optional namespace.
686pOpFront = maybeWithNS pOpFrontNoNS False []
687 where pOpFrontNoNS = do lchar '('; o <- operator; lchar ')'; return o
689pfName = try pOpFront
690 <|> pName
692pTotality :: IParser Bool
693pTotality
694 = do reserved "total"; return True
695 <|> do reserved "partial"; return False
697pAccessibility' :: IParser Accessibility
698pAccessibility'
699 = do reserved "public"; return Public
700 <|> do reserved "abstract"; return Frozen
701 <|> do reserved "private"; return Hidden
703pAccessibility :: IParser (Maybe Accessibility)
704pAccessibility
705 = do acc <- pAccessibility'; return (Just acc)
706 <|> return Nothing
708pFnOpts :: [FnOpt] -> IParser [FnOpt]
709pFnOpts opts
710 = do reserved "total"; pFnOpts (TotalFn : opts)
711 <|> do reserved "partial"; pFnOpts (PartialFn : (opts \\ [TotalFn]))
712 <|> try (do lchar '%'; reserved "export"; c <- strlit;
713 pFnOpts (CExport c : opts))
714 <|> do lchar '%'; reserved "assert_total"; pFnOpts (AssertTotal : opts)
715 <|> do lchar '%'; reserved "specialise";
716 lchar '['; ns <- sepBy pfName (lchar ','); lchar ']'
717 pFnOpts (Specialise ns : opts)
718 <|> do reserved "implicit"; pFnOpts (Implicit : opts)
719 <|> return opts
721addAcc :: Name -> Maybe Accessibility -> IParser ()
722addAcc n a = do i <- getState
723 setState (i { hide_list = (n, a) : hide_list i })
725pCaseExpr syn = do
726 reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
727 openBlock
728 pushIndent
729 opts <- many1 (do notEndBlock
730 x <- pCaseOpt syn
731 pKeepTerminator
732 return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
733 popIndent
734 closeBlock
735 return (PCase fc scr opts)
737pProofExpr syn = do
738 reserved "proof"; lchar '{'
739 ts <- endBy (pTactic syn) (lchar ';')
740 lchar '}'
741 return (PProof ts)
743pTacticsExpr syn = do
744 reserved "tactics"; lchar '{'
745 ts <- endBy (pTactic syn) (lchar ';')
746 lchar '}'
747 return (PTactics ts)
749pSimpleExpr syn =
750 try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t)
751 <|> do lchar '?'; x <- pName; return (PMetavar x)
752 <|> do lchar '%'; fc <- pfc; reserved "instance"; return (PResolveTC fc)
753 <|> do reserved "refl"; fc <- pfc;
754 tm <- option Placeholder (do lchar '{'; t <- pExpr syn; lchar '}';
755 return t)
756 return (PRefl fc tm)
757-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)
758 <|> pProofExpr syn
759 <|> pTacticsExpr syn
760 <|> pCaseExpr syn
761 <|> try (do x <- pfName
762 fc <- pfc
763 return (PRef fc x))
764 <|> try (do lchar '!'; x <- pfName
765 fc <- pfc
766 return (PInferRef fc x))
767 <|> try (pList syn)
768 <|> try (pComprehension syn)
769 <|> try (pAlt syn)
770 <|> try (pIdiom syn)
771 <|> try (do lchar '('
772 bracketed (noImp syn))
773 <|> try (do c <- pConstant
774 fc <- pfc
775 return (modifyConst syn fc (PConstant c)))
776 <|> do reserved "Type"; return PType
777 <|> try (do symbol "()"
778 fc <- pfc
779 return (PTrue fc))
780 <|> try (do symbol "_|_"
781 fc <- pfc
782 return (PFalse fc))
783 <|> do lchar '_'; return Placeholder
784 <|> pSimpleExtExpr syn
786bracketed syn =
787 try (pPair syn)
788 <|> try (do e <- pExpr syn; lchar ')'; return e)
789-- <|> try (do reserved "typed"
790-- e <- pExpr syn; symbol ":"; t <- pExpr syn; lchar ')'
791-- return (PTyped e t))
792 <|> try (do fc <- pfc; o <- operator; e <- pExpr syn; lchar ')'
793 return $ PLam (MN 1000 "ARG") Placeholder
794 (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),
795 pexp e]))
796 <|> try (do fc <- pfc; e <- pSimpleExpr syn; o <- operator; lchar ')'
797 return $ PLam (MN 1000 "ARG") Placeholder
798 (PApp fc (PRef fc (UN o)) [pexp e,
799 pexp (PRef fc (MN 1000 "ARG"))]))
801pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
802pCaseOpt syn = do lhs <- pExpr (syn { inPattern = True })
803 symbol "=>"; rhs <- pExpr syn
804 return (lhs, rhs)
806-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
807-- big integer, otherwise try fromInteger and the constants as alternatives.
808-- a better solution would be to fix fromInteger to work with Integer, as the
809-- name suggests, rather than Int
811modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
812modifyConst syn fc (PConstant (BI x))
813 | not (inPattern syn)
814 = PAlternative False
815 (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI (fromInteger x)))]
816 : consts)
817 | otherwise = PAlternative False consts
818 where
819 consts = [ PConstant (BI x)
820 , PConstant (I (fromInteger x))
821 , PConstant (B8 (fromInteger x))
822 , PConstant (B16 (fromInteger x))
823 , PConstant (B32 (fromInteger x))
824 , PConstant (B64 (fromInteger x))
825 ]
826modifyConst syn fc x = x
829pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']'
830 return (mkList fc xs)
831 where
832 mkList fc [] = PRef fc (UN "Nil")
833 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
835pPair syn = try (do l <- pExpr syn
836 fc <- pfc
837 rest <- restTuple
838 case rest of
839 [] -> return l
840 [Left r] -> return (PPair fc l r)
841 [Right r] -> return (PDPair fc l Placeholder r))
842 <|> try (do x <- ntuple
843 lchar ')'
844 return x)
845 <|> do ln <- pName; lchar ':'
846 lty <- pExpr syn
847 reservedOp "**"
848 fc <- pfc
849 r <- pExpr syn
850 lchar ')'
851 return (PDPair fc (PRef fc ln) lty r)
852 where
853 restTuple = do lchar ')'; return []
854 <|> do lchar ','
855 r <- pExpr syn
856 lchar ')'
857 return [Left r]
858 <|> do reservedOp "**"
859 r <- pExpr syn
860 lchar ')'
861 return [Right r]
862 ntuple = try (do l <- pExpr syn; fc <- pfc; lchar ','
863 rest <- ntuple
864 return (PPair fc l rest))
865 <|> (do l <- pExpr syn; fc <- pfc; lchar ','
866 r <- pExpr syn
867 return (PPair fc l r))
869pAlt syn = do symbol "(|"; alts <- sepBy1 (pExpr' syn) (lchar ','); symbol "|)"
870 return (PAlternative False alts)
872pHSimpleExpr syn
873 = do lchar '.'
874 e <- pSimpleExpr syn
875 return $ PHidden e
876 <|> pSimpleExpr syn
878pMatchApp syn = do ty <- pSimpleExpr syn
879 symbol "<=="
880 fc <- pfc
881 f <- pfName
882 return (PLet (MN 0 "match")
883 ty
884 (PMatchApp fc f)
885 (PRef fc (MN 0 "match")))
887pUnifyLog syn = do lchar '%'; reserved "unifyLog";
888 tm <- pSimpleExpr syn
889 return (PUnifyLog tm)
891pApp syn = do f <- pSimpleExpr syn
892 fc <- pfc
893 args <- many1 (do notEndApp
894 pArg syn)
895 i <- getState
896 return (dslify i $ PApp fc f args)
897 where
898 dslify i (PApp fc (PRef _ f) [a])
899 | [d] <- lookupCtxt f (idris_dsls i)
900 = desugar (syn { dsl_info = d }) i (getTm a)
901 dslify i t = t
903pArg :: SyntaxInfo -> IParser PArg
904pArg syn = try (pImplicitArg syn)
905 <|> try (pConstraintArg syn)
906 <|> do e <- pSimpleExpr syn
907 return (pexp e)
909pImplicitArg syn = do lchar '{'
910 n <- pName
911 fc <- pfc
912 v <- option (PRef fc n) (do lchar '='
913 pExpr syn)
914 lchar '}'
915 return (pimp n v)
917pConstraintArg syn = do symbol "@{"
918 e <- pExpr syn
919 symbol "}"
920 return (pconst e)
922pRecordType syn
923 = do reserved "record"
924 lchar '{'
925 fields <- sepBy1 pFieldType (lchar ',')
926 lchar '}'
927 fc <- pfc
928 rec <- option Nothing (do e <- pSimpleExpr syn
929 return (Just e))
930 case rec of
931 Nothing ->
932 return (PLam (MN 0 "fldx") Placeholder
933 (applyAll fc fields (PRef fc (MN 0 "fldx"))))
934 Just v -> return (applyAll fc fields v)
935 where pFieldType = do n <- pfName
936 lchar '='
937 e <- pExpr syn
938 return (n, e)
939 applyAll fc [] x = x
940 applyAll fc ((n, e) : es) x
941 = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])
943mkType (UN n) = UN ("set_" ++ n)
944mkType (MN 0 n) = MN 0 ("set_" ++ n)
945mkType (NS n s) = NS (mkType n) s
947noImp syn = syn { implicitAllowed = False }
948impOK syn = syn { implicitAllowed = True }
950pTSig syn = do lchar ':'; pTExpr syn
952pTExpr syn = do cs <- if implicitAllowed syn then pConstList syn else return []
953 sc <- pExpr syn
954 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
956pLambda syn = do lchar '\\'
957 try (do xt <- tyOptDeclList syn
958 symbol "=>"
959 sc <- pExpr syn
960 return (bindList PLam xt sc)
961 <|> (do ps <- sepBy (do fc <- pfc
962 e <- pSimpleExpr syn
963 return (fc, e)) (lchar ',')
964 symbol "=>"
965 sc <- pExpr syn
966 return (pmList (zip [0..] ps) sc)))
967 where pmList [] sc = sc
968 pmList ((i, (fc, x)) : xs) sc
969 = PLam (MN i "lamp") Placeholder
970 (PCase fc (PRef fc (MN i "lamp"))
971 [(x, pmList xs sc)])
973pRewriteTerm syn =
974 do reserved "rewrite"
975 fc <- pfc
976 prf <- pExpr syn
977 reserved "in"; sc <- pExpr syn
978 return (PRewrite fc
979 (PApp fc (PRef fc (UN "sym")) [pexp prf]) sc)
981pLet syn = try (do reserved "let"; n <- pName;
982 ty <- option Placeholder (do lchar ':'; pExpr' syn)
983 lchar '='
984 v <- pExpr syn
985 reserved "in"; sc <- pExpr syn
986 return (PLet n ty v sc))
987 <|> (do reserved "let"; fc <- pfc; pat <- pExpr' (syn { inPattern = True } )
988 symbol "="; v <- pExpr syn
989 reserved "in"; sc <- pExpr syn
990 return (PCase fc v [(pat, sc)]))
992pPi syn =
993 try (do lazy <- if implicitAllowed syn -- laziness is top level only
994 then option False (do lchar '|'; return True)
995 else return False
996 st <- pStatic
997 lchar '('; xt <- tyDeclList syn; lchar ')'
998 doc <- option "" (pDocComment '^')
999 symbol "->"
1000 sc <- pExpr syn
1001 return (bindList (PPi (Exp lazy st doc)) xt sc))
1002 <|> try (if implicitAllowed syn
1003 then do lazy <- option False (do lchar '|'
1004 return True)
1005 st <- pStatic
1006 lchar '{'
1007 xt <- tyDeclList syn
1008 lchar '}'
1009 symbol "->"
1010 sc <- pExpr syn
1011 return (bindList (PPi (Imp lazy st "")) xt sc)
1012 else fail "No implicit arguments allowed here")
1013 <|> try (do lchar '{'
1014 reserved "auto"
1015 xt <- tyDeclList syn
1016 lchar '}'
1017 symbol "->"
1018 sc <- pExpr syn
1019 return (bindList (PPi
1020 (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))
1021 <|> try (do lchar '{'
1022 reserved "default"
1023 script <- pSimpleExpr syn
1024 xt <- tyDeclList syn
1025 lchar '}'
1026 symbol "->"
1027 sc <- pExpr syn
1028 return (bindList (PPi (TacImp False Dynamic script "")) xt sc))
1029 <|> do --lazy <- option False (do lchar '|'; return True)
1030 lchar '{'
1031 reserved "static"
1032 lchar '}'
1033 t <- pExpr' syn
1034 symbol "->"
1035 sc <- pExpr syn
1036 return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)
1038pConstList :: SyntaxInfo -> IParser [PTerm]
1039pConstList syn = try (do lchar '('
1040 tys <- sepBy1 (pExpr' (noImp syn)) (lchar ',')
1041 lchar ')'
1042 reservedOp "=>"
1043 return tys)
1044 <|> try (do t <- pExpr (noImp syn)
1045 reservedOp "=>"
1046 return [t])
1047 <|> return []
1049usingDeclList syn
1050 = try (sepBy1 (usingDecl syn) (lchar ','))
1051 <|> do ns <- sepBy1 pName (lchar ',')
1052 t <- pTSig (noImp syn)
1053 return (map (\x -> UImplicit x t) ns)
1055usingDecl syn = try (do x <- pfName
1056 t <- pTSig (noImp syn)
1057 return (UImplicit x t))
1058 <|> do c <- pfName
1059 xs <- many1 pfName
1060 return (UConstraint c xs)
1062tyDeclList syn = try (sepBy1 (do x <- pfName
1063 t <- pTSig (noImp syn)
1064 return (x,t))
1065 (lchar ','))
1066 <|> do ns <- sepBy1 pName (lchar ',')
1067 t <- pTSig (noImp syn)
1068 return (map (\x -> (x, t)) ns)
1070tyOptDeclList syn = sepBy1 (do x <- pfName;
1071 t <- option Placeholder (do lchar ':'
1072 pExpr syn)
1073 return (x,t))
1074 (lchar ',')
1076bindList b [] sc = sc
1077bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
1079pComprehension syn
1080 = do lchar '['
1081 fc <- pfc
1082 pat <- pExpr syn
1083 lchar '|'
1084 qs <- sepBy1 (pDo syn) (lchar ',')
1085 lchar ']'
1086 return (PDoBlock (map addGuard qs ++
1087 [DoExp fc (PApp fc (PRef fc (UN "return"))
1088 [pexp pat])]))
1089 where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
1090 [pexp e])
1091 addGuard x = x
1093pDoBlock syn
1094 = do reserved "do"
1095 openBlock
1096 pushIndent
1097 ds <- many1 (do notEndBlock
1098 x <- pDo syn
1099 pKeepTerminator
1100 return x)
1101 popIndent
1102 closeBlock
1103 return (PDoBlock ds)
1105pDo syn
1106 = try (do reserved "let"
1107 i <- pName;
1108 ty <- option Placeholder (do lchar ':'
1109 pExpr' syn)
1110 reservedOp "="
1111 fc <- pfc
1112 e <- pExpr syn
1113 return (DoLet fc i ty e))
1114 <|> try (do reserved "let"
1115 i <- pExpr' syn
1116 reservedOp "="
1117 fc <- pfc
1118 sc <- pExpr syn
1119 return (DoLetP fc i sc))
1120 <|> try (do i <- pName
1121 symbol "<-"
1122 fc <- pfc
1123 e <- pExpr syn;
1124 return (DoBind fc i e))
1125 <|> try (do i <- pExpr' syn
1126 symbol "<-"
1127 fc <- pfc
1128 e <- pExpr syn;
1129 return (DoBindP fc i e))
1130 <|> try (do e <- pExpr syn
1131 fc <- pfc
1132 return (DoExp fc e))
1134pIdiom syn
1135 = do symbol "[|"
1136 fc <- pfc
1137 e <- pExpr syn
1138 symbol "|]"
1139 return (PIdiom fc e)
1141pConstant :: IParser Const
1142pConstant = do reserved "Integer";return BIType
1143 <|> do reserved "Int"; return IType
1144 <|> do reserved "Char"; return ChType
1145 <|> do reserved "Float"; return FlType
1146 <|> do reserved "String"; return StrType
1147 <|> do reserved "Ptr"; return PtrType
1148 <|> do reserved "Bits8"; return B8Type
1149 <|> do reserved "Bits16"; return B16Type
1150 <|> do reserved "Bits32"; return B32Type
1151 <|> do reserved "Bits64"; return B64Type
1152 <|> try (do f <- float; return $ Fl f)
1153 <|> try (do i <- natural; return $ BI i)
1154 <|> try (do s <- strlit; return $ Str s)
1155 <|> try (do c <- chlit; return $ Ch c)
1157pStatic :: IParser Static
1158pStatic = do lchar '['
1159 reserved "static"
1160 lchar ']';
1161 return Static
1162 <|> return Dynamic
1164table fixes
1165 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
1166 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]
1167 ++ toTable (reverse fixes) ++
1168 [[backtick],
1169 [binary "=" PEq AssocLeft],
1170 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
1172toTable fs = map (map toBin)
1173 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
1174 where toBin (Fix (PrefixN _) op) = prefix op
1175 (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
1176 toBin (Fix f op)
1177 = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
1178 assoc (Infixl _) = AssocLeft
1179 assoc (Infixr _) = AssocRight
1180 assoc (InfixN _) = AssocNone
1182binary name f = Infix (do fc <- pfc
1183 reservedOp name
1184 doc <- option "" (pDocComment '^')
1185 return (f fc))
1186prefix name f = Prefix (do reservedOp name
1187 fc <- pfc;
1188 return (f fc))
1189backtick = Infix (do lchar '`'; n <- pfName
1190 lchar '`'
1191 fc <- pfc
1192 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
1194--------- Data declarations ---------
1196-- (works for classes too - 'abstract' means the data/class is visible but members not)
1197accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()
1198accData (Just Frozen) n ns = do addAcc n (Just Frozen)
1199 mapM_ (\n -> addAcc n (Just Hidden)) ns
1200accData a n ns = do addAcc n a
1201 mapM_ (`addAcc` a) ns
1203pRecord :: SyntaxInfo -> IParser PDecl
1204pRecord syn = do doc <- option "" (pDocComment '|')
1205 acc <- pAccessibility
1206 reserved "record"
1207 fc <- pfc
1208 tyn_in <- pfName
1209 ty <- pTSig (impOK syn)
1210 let tyn = expandNS syn tyn_in
1211 reserved "where"
1212 openBlock
1213 pushIndent
1214 (cdoc, cn, cty, _) <- pConstructor syn
1215 pKeepTerminator
1216 popIndent
1217 closeBlock
1218 accData acc tyn [cn]
1219 let rsyn = syn { syn_namespace = show (nsroot tyn) :
1220 syn_namespace syn }
1221 let fns = getRecNames rsyn cty
1222 mapM_ (\n -> addAcc n acc) fns
1223 return $ PRecord doc rsyn fc tyn ty cdoc cn cty
1224 where
1225 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
1226 ++ getRecNames syn sc
1227 getRecNames _ _ = []
1229 toFreeze (Just Frozen) = Just Hidden
1230 toFreeze x = x
1232pDataI = do reserved "data"; return False
1233 <|> do reserved "codata"; return True
1235pData :: SyntaxInfo -> IParser PDecl
1236pData syn = try (do doc <- option "" (pDocComment '|')
1237 acc <- pAccessibility
1238 co <- pDataI
1239 fc <- pfc
1240 tyn_in <- pfName
1241 ty <- pTSig (impOK syn)
1242 let tyn = expandNS syn tyn_in
1243 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1244 reserved "where"
1245 openBlock
1246 pushIndent
1247 cons <- many (do notEndBlock
1248 c <- pConstructor syn
1249 pKeepTerminator
1250 return c) -- (lchar '|')
1251 popIndent
1252 closeBlock
1253 accData acc tyn (map (\ (_, n, _, _) -> n) cons)
1254 return $ PData doc syn fc co (PDatadecl tyn ty cons)))
1255 <|> try (do doc <- option "" (pDocComment '|')
1256 pushIndent
1257 acc <- pAccessibility
1258 co <- pDataI
1259 fc <- pfc
1260 tyn_in <- pfName
1261 args <- many pName
1262 let ty = bindArgs (map (const PType) args) PType
1263 let tyn = expandNS syn tyn_in
1264 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1265 try (lchar '=') <|> do reserved "where"
1266 let kw = (if co then "co" else "") ++ "data "
1267 let n = show tyn_in ++ " "
1268 let s = kw ++ n
1269 let as = concat (intersperse " " $ map show args) ++ " "
1270 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
1271 let ss = concat (intersperse " -> " $ map (const "Type") args)
1272 let fix1 = s ++ as ++ " = ..."
1273 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
1274 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
1275 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
1277 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
1278 pTerminator
1279 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
1280 cons' <- mapM (\ (doc, x, cargs, cfc) ->
1281 do let cty = bindArgs cargs conty
1282 return (doc, x, cty, cfc)) cons
1283 accData acc tyn (map (\ (_, n, _, _) -> n) cons')
1284 return $ PData doc syn fc co (PDatadecl tyn ty cons')))
1285 where
1286 mkPApp fc t [] = t
1287 mkPApp fc t xs = PApp fc t (map pexp xs)
1289bindArgs :: [PTerm] -> PTerm -> PTerm
1290bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
1292pConstructor :: SyntaxInfo -> IParser (String, Name, PTerm, FC)
1293pConstructor syn
1294 = do doc <- option "" (pDocComment '|')
1295 cn_in <- pfName; fc <- pfc
1296 let cn = expandNS syn cn_in
1297 ty <- pTSig (impOK syn)
1298-- ty' <- implicit syn cn ty
1299 return (doc, cn, ty, fc)
1302pSimpleCon :: SyntaxInfo -> IParser (String, Name, [PTerm], FC)
1303pSimpleCon syn
1304 = do cn_in <- pfName
1305 let cn = expandNS syn cn_in
1306 fc <- pfc
1307 args <- many (do notEndApp
1308 pSimpleExpr syn)
1309 doc <- option "" (pDocComment '^')
1310 return (doc, cn, args, fc)
1312--------- DSL syntax overloading ---------
1314pDSL :: SyntaxInfo -> IParser PDecl
1315pDSL syn = do reserved "dsl"
1316 n <- pfName
1317 openBlock
1318 pushIndent
1319 bs <- many1 (do notEndBlock
1320 b <- pOverload syn
1321 pKeepTerminator
1322 return b)
1323 popIndent; closeBlock
1324 let dsl = mkDSL bs (dsl_info syn)
1325 checkDSL dsl
1326 i <- getState
1327 setState (i { idris_dsls = addDef n dsl (idris_dsls i) })
1328 return (PDSL n dsl)
1329 where mkDSL bs dsl = let var = lookup "variable" bs
1330 first = lookup "index_first" bs
1331 next = lookup "index_next" bs
1332 leto = lookup "let" bs
1333 lambda = lookup "lambda" bs in
1334 initDSL { dsl_var = var,
1335 index_first = first,
1336 index_next = next,
1337 dsl_lambda = lambda,
1338 dsl_let = leto }
1340checkDSL :: DSL -> IParser ()
1341checkDSL dsl = return ()
1343pOverload :: SyntaxInfo -> IParser (String, PTerm)
1344pOverload syn = do o <- identifier <|> do reserved "let"
1345 return "let"
1346 if o `notElem` overloadable
1347 then fail $ show o ++ " is not an overloading"
1348 else do
1349 lchar '='
1350 t <- pExpr syn
1351 return (o, t)
1352 where overloadable = ["let","lambda","index_first","index_next","variable"]
1354--------- Pattern match clauses ---------
1356pPattern :: SyntaxInfo -> IParser PDecl
1357pPattern syn = do fc <- pfc
1358 clause <- pClause syn
1359 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
1361pCAF :: SyntaxInfo -> IParser PDecl
1362pCAF syn = do reserved "let"
1363 n_in <- pfName; let n = expandNS syn n_in
1364 lchar '='
1365 t <- pExpr syn
1366 pTerminator
1367 fc <- pfc
1368 return (PCAF fc n t)
1370pArgExpr syn = let syn' = syn { inPattern = True } in
1371 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
1373pRHS :: SyntaxInfo -> Name -> IParser PTerm
1374pRHS syn n = do lchar '='; pExpr syn
1375 <|> do symbol "?="; rhs <- pExpr syn;
1376 return (addLet rhs)
1377 <|> do reserved "impossible"; return PImpossible
1378 where mkN (UN x) = UN (x++"_lemma_1")
1379 mkN (NS x n) = NS (mkN x) n
1380 n' = mkN n
1382 addLet (PLet n ty val rhs) = PLet n ty val (addLet rhs)
1383 addLet (PCase fc t cs) = PCase fc t (map addLetC cs)
1384 where addLetC (l, r) = (l, addLet r)
1385 addLet rhs = (PLet (UN "value") Placeholder rhs (PMetavar n'))
1387pClause :: SyntaxInfo -> IParser PClause
1388pClause syn
1389 = try (do pushIndent
1390 n_in <- pfName; let n = expandNS syn n_in
1391 cargs <- many (pConstraintArg syn)
1392 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1393 fc <- pfc
1394 args <- many (try (pImplicitArg (syn { inPattern = True } ))
1395 <|> (fmap pexp (pArgExpr syn)))
1396 wargs <- many (pWExpr syn)
1397 rhs <- pRHS syn n
1398 ist <- getState
1399 let ctxt = tt_ctxt ist
1400 let wsyn = syn { syn_namespace = [] }
1401 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1402 popIndent
1403 return x,
1404 do pTerminator
1405 return ([], [])]
1406 let capp = PApp fc (PRef fc n)
1407 (iargs ++ cargs ++ args)
1408 ist <- getState
1409 setState (ist { lastParse = Just n })
1410 return $ PClause fc n capp wargs rhs wheres)
1411 <|> try (do pushIndent
1412 ty <- pSimpleExpr syn
1413 symbol "<=="
1414 fc <- pfc
1415 n_in <- pfName; let n = expandNS syn n_in
1416 rhs <- pRHS syn n
1417 ist <- getState
1418 let ctxt = tt_ctxt ist
1419 let wsyn = syn { syn_namespace = [] }
1420 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1421 popIndent
1422 return x,
1423 do pTerminator
1424 return ([], [])]
1425 let capp = PLet (MN 0 "match")
1426 ty
1427 (PMatchApp fc n)
1428 (PRef fc (MN 0 "match"))
1429 ist <- getState
1430 setState (ist { lastParse = Just n })
1431 return $ PClause fc n capp [] rhs wheres)
1432 <|> try (do pushIndent
1433 wargs <- many1 (pWExpr syn)
1434 ist <- getState
1435 n <- case lastParse ist of
1436 Just t -> return t
1437 Nothing -> fail "Invalid clause"
1438 fc <- pfc
1439 rhs <- pRHS syn n
1440 let ctxt = tt_ctxt ist
1441 let wsyn = syn { syn_namespace = [] }
1442 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1443 popIndent
1444 return x,
1445 do pTerminator
1446 return ([], [])]
1447 return $ PClauseR fc wargs rhs wheres)
1449 <|> try (do pushIndent
1450 n_in <- pfName; let n = expandNS syn n_in
1451 cargs <- many (pConstraintArg syn)
1452 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1453 fc <- pfc
1454 args <- many (try (pImplicitArg (syn { inPattern = True } ))
1455 <|> (fmap pexp (pArgExpr syn)))
1456 wargs <- many (pWExpr syn)
1457 let capp = PApp fc (PRef fc n)
1458 (iargs ++ cargs ++ args)
1459 ist <- getState
1460 setState (ist { lastParse = Just n })
1461 reserved "with"
1462 wval <- pSimpleExpr syn
1463 openBlock
1464 ds <- many1 $ pFunDecl syn
1465 let withs = map (fillLHSD n capp wargs) $ concat ds
1466 closeBlock
1467 popIndent
1468 return $ PWith fc n capp wargs wval withs)
1470 <|> try (do wargs <- many1 (pWExpr syn)
1471 fc <- pfc
1472 reserved "with"
1473 wval <- pSimpleExpr syn
1474 openBlock
1475 ds <- many1 $ pFunDecl syn
1476 let withs = concat ds
1477 closeBlock
1478 return $ PWithR fc wargs wval withs)
1480 <|> do pushIndent
1481 l <- pArgExpr syn
1482 op <- operator
1483 let n = expandNS syn (UN op)
1484 r <- pArgExpr syn
1485 fc <- pfc
1486 wargs <- many (pWExpr syn)
1487 rhs <- pRHS syn n
1488 let wsyn = syn { syn_namespace = [] }
1489 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1490 popIndent
1491 return x,
1492 do pTerminator
1493 return ([], [])]
1494 ist <- getState
1495 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1496 setState (ist { lastParse = Just n })
1497 return $ PClause fc n capp wargs rhs wheres
1499 <|> do l <- pArgExpr syn
1500 op <- operator
1501 let n = expandNS syn (UN op)
1502 r <- pArgExpr syn
1503 fc <- pfc
1504 wargs <- many (pWExpr syn)
1505 reserved "with"
1506 wval <- pSimpleExpr syn
1507 openBlock
1508 ds <- many1 $ pFunDecl syn
1509 closeBlock
1510 ist <- getState
1511 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1512 let withs = map (fillLHSD n capp wargs) $ concat ds
1513 setState (ist { lastParse = Just n })
1514 return $ PWith fc n capp wargs wval withs
1515 where
1516 fillLHS n capp owargs (PClauseR fc wargs v ws)
1517 = PClause fc n capp (owargs ++ wargs) v ws
1518 fillLHS n capp owargs (PWithR fc wargs v ws)
1519 = PWith fc n capp (owargs ++ wargs) v
1520 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1521 fillLHS _ _ _ c = c
1523 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1524 fillLHSD n c a x = x
1526pWExpr :: SyntaxInfo -> IParser PTerm
1527pWExpr syn = do lchar '|'
1528 pExpr' syn
1530pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
1531pWhereblock n syn
1532 = do reserved "where"; openBlock
1533 ds <- many1 $ pDecl syn
1534 let dns = concatMap (concatMap declared) ds
1535 closeBlock
1536 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1538pTarget :: IParser Target
1539pTarget = try (do reserved "C"; return ViaC)
1540 <|> try (do reserved "Java"; return ViaJava)
1541 <|> try (do reserved "JavaScript"; return ViaJavaScript)
1542 <|> try (do reserved "Node"; return ViaNode)
1543 <|> try (do reserved "Bytecode"; return Bytecode)
1545pDirective :: SyntaxInfo -> IParser [PDecl]
1546pDirective syn = try (do lchar '%'; reserved "lib"; tgt <- pTarget; lib <- strlit;
1547 return [PDirective (do addLib tgt lib
1548 addIBC (IBCLib tgt lib))])
1549 <|> try (do lchar '%'; reserved "link"; tgt <- pTarget; obj <- strlit;
1550 return [PDirective (do datadir <- liftIO getDataDir
1551 o <- liftIO $ findInPath [".", datadir] obj
1552 addIBC (IBCObj tgt o)
1553 addObjectFile tgt o)])
1554 <|> try (do lchar '%'; reserved "include"; tgt <- pTarget; hdr <- strlit;
1555 return [PDirective (do addHdr tgt hdr
1556 addIBC (IBCHeader tgt hdr))])
1557 <|> try (do lchar '%'; reserved "hide"; n <- iName []
1558 return [PDirective (do setAccessibility n Hidden
1559 addIBC (IBCAccess n Hidden))])
1560 <|> try (do lchar '%'; reserved "freeze"; n <- iName []
1561 return [PDirective (do setAccessibility n Frozen
1562 addIBC (IBCAccess n Frozen))])
1563 <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'
1564 return [PDirective (do i <- getIState
1565 putIState (i { default_access = acc }))])
1566 <|> try (do lchar '%'; reserved "default"; tot <- pTotality
1567 i <- getState
1568 setState (i { default_total = tot } )
1569 return [PDirective (do i <- getIState
1570 putIState (i { default_total = tot }))])
1571 <|> try (do lchar '%'; reserved "logging"; i <- natural;
1572 return [PDirective (setLogLevel (fromInteger i))])
1573 <|> try (do lchar '%'; reserved "dynamic"; libs <- sepBy1 strlit (lchar ',');
1574 return [PDirective (do added <- addDyLib libs
1575 case added of
1576 Left lib -> addIBC (IBCDyLib (lib_name lib))
1577 Right msg ->
1578 fail $ msg)])
1579 <|> try (do lchar '%'; reserved "language"; ext <- reserved "TypeProviders";
1580 return [PDirective (addLangExt TypeProviders)])
1582pProvider :: SyntaxInfo -> IParser [PDecl]
1583pProvider syn = do lchar '%'; reserved "provide";
1584 lchar '('; n <- pfName; t <- pTSig syn; lchar ')'
1585 fc <- pfc
1586 reserved "with"
1587 e <- pExpr syn
1588 return [PProvider syn fc n t e]
1590pTactic :: SyntaxInfo -> IParser PTactic
1591pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
1592 return $ Intro ns
1593 <|> do reserved "intros"; return Intros
1594 <|> try (do reserved "refine"; n <- pName
1595 imps <- many1 imp
1596 return $ Refine n imps)
1597 <|> do reserved "refine"; n <- pName
1598 i <- getState
1599 return $ Refine n []
1600 <|> do reserved "mrefine"; n <- pName
1601 i <- getState
1602 return $ MatchRefine n
1603 <|> do reserved "rewrite"; t <- pExpr syn;
1604 i <- getState
1605 return $ Rewrite (desugar syn i t)
1606 <|> try (do reserved "let"; n <- pName; lchar ':';
1607 ty <- pExpr' syn; lchar '='; t <- pExpr syn;
1608 i <- getState
1609 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
1610 <|> try (do reserved "let"; n <- pName; lchar '=';
1611 t <- pExpr syn;
1612 i <- getState
1613 return $ LetTac n (desugar syn i t))
1614 <|> do reserved "focus"; n <- pName
1615 return $ Focus n
1616 <|> do reserved "exact"; t <- pExpr syn;
1617 i <- getState
1618 return $ Exact (desugar syn i t)
1619 <|> do reserved "applyTactic"; t <- pExpr syn;
1620 i <- getState
1621 return $ ApplyTactic (desugar syn i t)
1622 <|> do reserved "reflect"; t <- pExpr syn;
1623 i <- getState
1624 return $ Reflect (desugar syn i t)
1625 <|> do reserved "fill"; t <- pExpr syn;
1626 i <- getState
1627 return $ Fill (desugar syn i t)
1628 <|> do reserved "try"; t <- pTactic syn;
1629 lchar '|';
1630 t1 <- pTactic syn
1631 return $ Try t t1
1632 <|> do lchar '{'
1633 t <- pTactic syn;
1634 lchar ';';
1635 t1 <- pTactic syn;
1636 lchar '}'
1637 return $ TSeq t t1
1638 <|> do reserved "compute"; return Compute
1639 <|> do reserved "trivial"; return Trivial
1640 <|> do reserved "solve"; return Solve
1641 <|> do reserved "attack"; return Attack
1642 <|> do reserved "state"; return ProofState
1643 <|> do reserved "term"; return ProofTerm
1644 <|> do reserved "undo"; return Undo
1645 <|> do reserved "qed"; return Qed
1646 <|> do reserved "abandon"; return Abandon
1647 <|> do lchar ':'; reserved "q"; return Abandon
1648 where
1649 imp = do lchar '?'; return False
1650 <|> do lchar '_'; return True