git.iko.soy/Idris-dev
on 4dddfaf help sign in
Idris-dev/src/Idris/Parser.hs
1684 lines 68 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 <|> try (pProvider syn)
348 <|> pTransform syn
349 <|> try (do reserved "import"; fp <- identifier
350 fail "imports must be at the top of file")
352pFunDecl :: SyntaxInfo -> IParser [PDecl]
353pFunDecl syn
354 = try (do notEndBlock
355 d <- pFunDecl' syn
356 i <- getState
357 let d' = fmap (desugar syn i) d
358 return [d'])
360--------- Top Level Declarations ---------
362pDecl' :: SyntaxInfo -> IParser PDecl
363pDecl' syn
364 = try pFixity
365 <|> try (pFunDecl' syn)
366 <|> try (pData syn)
367 <|> try (pRecord syn)
368 <|> try (pSyntaxDecl syn)
370pSyntaxDecl :: SyntaxInfo -> IParser PDecl
371pSyntaxDecl syn
372 = do s <- pSyntaxRule syn
373 i <- getState
374 let rs = syntax_rules i
375 let ns = syntax_keywords i
376 let ibc = ibc_write i
377 let ks = map show (names s)
378 setState (i { syntax_rules = s : rs,
379 syntax_keywords = ks ++ ns,
380 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc
381 })
382 fc <- pfc
383 return (PSyntax fc s)
384 where
385 names (Rule syms _ _) = mapMaybe ename syms
386 ename (Keyword n) = Just n
387 ename _ = Nothing
389pSyntaxRule :: SyntaxInfo -> IParser Syntax
390pSyntaxRule syn
391 = do pushIndent
392 sty <- option AnySyntax (do reserved "term"; return TermSyntax
393 <|> do reserved "pattern"; return PatternSyntax)
394 reserved "syntax"
395 syms <- many1 pSynSym
396 when (all expr syms) $ fail "No keywords in syntax rule"
397 let ns = mapMaybe name syms
398 when (length ns /= length (nub ns))
399 $ fail "Repeated variable in syntax rule"
400 lchar '='
401 tm <- pTExpr (impOK syn)
402 pTerminator
403 return (Rule (mkSimple syms) tm sty)
404 where
405 expr (Expr _) = True
406 expr _ = False
407 name (Expr n) = Just n
408 name _ = Nothing
410 -- Can't parse two full expressions (i.e. expressions with application) in a row
411 -- so change them both to a simple expression
413 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
414 mkSimple xs = mkSimple' xs
416 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
417 mkSimple es
418 mkSimple' (e : es) = e : mkSimple' es
419 mkSimple' [] = []
421pSynSym :: IParser SSymbol
422pSynSym = try (do lchar '['; n <- pName; lchar ']'
423 return (Expr n))
424 <|> try (do lchar '{'; n <- pName; lchar '}'
425 return (Binding n))
426 <|> do n <- iName []
427 return (Keyword n)
428 <|> do sym <- strlit
429 return (Symbol sym)
431pFunDecl' :: SyntaxInfo -> IParser PDecl
432pFunDecl' syn = try (do doc <- option "" (pDocComment '|')
433 pushIndent
434 ist <- getState
435 let initOpts = if default_total ist
436 then [TotalFn]
437 else []
438 opts <- pFnOpts initOpts
439 acc <- pAccessibility
440 opts' <- pFnOpts opts
441 n_in <- pfName
442 let n = expandNS syn n_in
443 fc <- pfc
444 ty <- pTSig (impOK syn)
445 pTerminator
446-- ty' <- implicit syn n ty
447 addAcc n acc
448 return (PTy doc syn fc opts' n ty))
449 <|> try (pPostulate syn)
450 <|> try (pPattern syn)
451 <|> try (pCAF syn)
453pPostulate :: SyntaxInfo -> IParser PDecl
454pPostulate syn = do doc <- option "" (pDocComment '|')
455 pushIndent
456 reserved "postulate"
457 ist <- getState
458 let initOpts = if default_total ist
459 then [TotalFn]
460 else []
461 opts <- pFnOpts initOpts
462 acc <- pAccessibility
463 opts' <- pFnOpts opts
464 n_in <- pfName
465 let n = expandNS syn n_in
466 ty <- pTSig (impOK syn)
467 fc <- pfc
468 pTerminator
469 addAcc n acc
470 return (PPostulate doc syn fc opts' n ty)
473pUsing :: SyntaxInfo -> IParser [PDecl]
474pUsing syn =
475 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
476 openBlock
477 let uvars = using syn
478 ds <- many1 (pDecl (syn { using = uvars ++ ns }))
479 closeBlock
480 return (concat ds)
482pParams :: SyntaxInfo -> IParser [PDecl]
483pParams syn =
484 do reserved "parameters"; lchar '('; ns <- tyDeclList syn; lchar ')'
485 openBlock
486 let pvars = syn_params syn
487 ds <- many1 (pDecl syn { syn_params = pvars ++ ns })
488 closeBlock
489 fc <- pfc
490 return [PParams fc ns (concat ds)]
492pMutual :: SyntaxInfo -> IParser [PDecl]
493pMutual syn =
494 do reserved "mutual"
495 openBlock
496 let pvars = syn_params syn
497 ds <- many1 (pDecl syn)
498 closeBlock
499 fc <- pfc
500 return [PMutual fc (concat ds)]
502pNamespace :: SyntaxInfo -> IParser [PDecl]
503pNamespace syn =
504 do reserved "namespace"; n <- identifier;
505 openBlock
506 ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
507 closeBlock
508 return [PNamespace n (concat ds)]
510--------- Fixity ---------
512pFixity :: IParser PDecl
513pFixity = do pushIndent
514 f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
515 pTerminator
516 let prec = fromInteger i
517 istate <- getState
518 let infixes = idris_infixes istate
519 let fs = map (Fix (f prec)) ops
520 let redecls = map (alreadyDeclared infixes) fs
521 let ill = filter (not . checkValidity) redecls
522 if null ill
523 then do setState (istate { idris_infixes = nub $ sort (fs ++ infixes)
524 , ibc_write = map IBCFix fs ++ ibc_write istate
525 })
526 fc <- pfc
527 return (PFix fc (f prec) ops)
528 else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
529 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
530 where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
531 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
533 checkValidity :: (FixDecl, [FixDecl]) -> Bool
534 checkValidity (f, fs) = all (== f) fs
536 extractName :: FixDecl -> String
537 extractName (Fix _ n) = n
539fixity :: IParser (Int -> Fixity)
540fixity = try (do reserved "infixl"; return Infixl)
541 <|> try (do reserved "infixr"; return Infixr)
542 <|> try (do reserved "infix"; return InfixN)
543 <|> try (do reserved "prefix"; return PrefixN)
545--------- Type classes ---------
547pClass :: SyntaxInfo -> IParser [PDecl]
548pClass syn = do doc <- option "" (pDocComment '|')
549 acc <- pAccessibility
550 reserved "class"; fc <- pfc; cons <- pConstList syn; n_in <- pName
551 let n = expandNS syn n_in
552 cs <- many carg
553 reserved "where"; openBlock
554 ds <- many $ pFunDecl syn
555 closeBlock
556 let allDs = concat ds
557 accData acc n (concatMap declared allDs)
558 return [PClass doc syn fc cons n cs allDs]
559 where
560 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'
561 return (i, ty)
562 <|> do i <- pName;
563 return (i, PType)
565pInstance :: SyntaxInfo -> IParser [PDecl]
566pInstance syn = do reserved "instance"; fc <- pfc
567 en <- option Nothing
568 (do lchar '['; n_in <- pfName; lchar ']'
569 let n = expandNS syn n_in
570 return (Just n))
571 cs <- pConstList syn
572 cn <- pName
573 args <- many (pSimpleExpr syn)
574 let sc = PApp fc (PRef fc cn) (map pexp args)
575 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
576 reserved "where"; openBlock
577 ds <- many $ pFunDecl syn
578 closeBlock
579 return [PInstance syn fc cs cn args t en (concat ds)]
581--------- Expressions ---------
583pExpr syn = do i <- getState
584 buildExpressionParser (table (idris_infixes i)) (pExpr' syn)
586pExpr' :: SyntaxInfo -> IParser PTerm
587pExpr' syn
588 = try (pExtExpr syn)
589 <|> pNoExtExpr syn
591pExtExpr :: SyntaxInfo -> IParser PTerm
592pExtExpr syn = do i <- getState
593 pExtensions syn (syntax_rules i)
595pSimpleExtExpr :: SyntaxInfo -> IParser PTerm
596pSimpleExtExpr syn = do i <- getState
597 pExtensions syn (filter simple (syntax_rules i))
598 where
599 simple (Rule (Expr x:xs) _ _) = False
600 simple (Rule (SimpleExpr x:xs) _ _) = False
601 simple (Rule [Keyword _] _ _) = True
602 simple (Rule [Symbol _] _ _) = True
603 simple (Rule (_:xs) _ _) = case last xs of
604 Keyword _ -> True
605 Symbol _ -> True
606 _ -> False
607 simple _ = False
609pNoExtExpr syn =
610 try (pApp syn)
611 <|> try (pMatchApp syn)
612 <|> try (pUnifyLog syn)
613 <|> pRecordType syn
614 <|> try (pSimpleExpr syn)
615 <|> pLambda syn
616 <|> pLet syn
617 <|> pRewriteTerm syn
618 <|> pPi syn
619 <|> pDoBlock syn
621pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
622pExtensions syn rules = choice (map (try . pExt syn) (filter valid rules))
623 where
624 valid (Rule _ _ AnySyntax) = True
625 valid (Rule _ _ PatternSyntax) = inPattern syn
626 valid (Rule _ _ TermSyntax) = not (inPattern syn)
629data SynMatch = SynTm PTerm | SynBind Name
631pExt :: SyntaxInfo -> Syntax -> IParser PTerm
632pExt syn (Rule ssym ptm _)
633 = do smap <- mapM pSymbol ssym
634 let ns = mapMaybe id smap
635 return (update ns ptm) -- updated with smap
636 where
637 pSymbol (Keyword n) = do reserved (show n); return Nothing
638 pSymbol (Expr n) = do tm <- pExpr syn
639 return $ Just (n, SynTm tm)
640 pSymbol (SimpleExpr n) = do tm <- pSimpleExpr syn
641 return $ Just (n, SynTm tm)
642 pSymbol (Binding n) = do b <- pName
643 return $ Just (n, SynBind b)
644 pSymbol (Symbol s) = do symbol s
645 return Nothing
646 dropn n [] = []
647 dropn n ((x,t) : xs) | n == x = xs
648 | otherwise = (x,t):dropn n xs
650 updateB ns n = case lookup n ns of
651 Just (SynBind t) -> t
652 _ -> n
654 update ns (PRef fc n) = case lookup n ns of
655 Just (SynTm t) -> t
656 _ -> PRef fc n
657 update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)
658 update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc)
659 update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)
660 (update (dropn n ns) sc)
661 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
662 update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)
663 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)
664 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)
665 update ns (PAlternative a as) = PAlternative a (map (update ns) as)
666 update ns (PHidden t) = PHidden (update ns t)
667 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
668 where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
669 upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds
670 upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)
671 : upd (dropn n ns) ds
672 upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t)
673 : upd ns ds
674 upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)
675 : upd ns ds
676 update ns t = t
678pName = do i <- getState
679 iName (syntax_keywords i)
680 <|> do reserved "instance"
681 i <- getState
682 UN n <- iName (syntax_keywords i)
683 return (UN ('@':n))
685-- | Parser for an operator in function position, i.e. enclosed by `()', with an
686-- optional namespace.
687pOpFront = maybeWithNS pOpFrontNoNS False []
688 where pOpFrontNoNS = do lchar '('; o <- operator; lchar ')'; return o
690pfName = try pOpFront
691 <|> pName
693pTotality :: IParser Bool
694pTotality
695 = do reserved "total"; return True
696 <|> do reserved "partial"; return False
698pAccessibility' :: IParser Accessibility
699pAccessibility'
700 = do reserved "public"; return Public
701 <|> do reserved "abstract"; return Frozen
702 <|> do reserved "private"; return Hidden
704pAccessibility :: IParser (Maybe Accessibility)
705pAccessibility
706 = do acc <- pAccessibility'; return (Just acc)
707 <|> return Nothing
709pFnOpts :: [FnOpt] -> IParser [FnOpt]
710pFnOpts opts
711 = do reserved "total"; pFnOpts (TotalFn : opts)
712 <|> do reserved "partial"; pFnOpts (PartialFn : (opts \\ [TotalFn]))
713 <|> try (do lchar '%'; reserved "export"; c <- strlit;
714 pFnOpts (CExport c : opts))
715 <|> try (do lchar '%'; reserved "assert_total";
716 pFnOpts (AssertTotal : opts))
717 <|> do lchar '%'; reserved "specialise";
718 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
719 pFnOpts (Specialise ns : opts)
720 <|> do reserved "implicit"; pFnOpts (Implicit : opts)
721 <|> return opts
722 where nameTimes = do n <- pfName
723 t <- option Nothing (do reds <- natural
724 return (Just (fromInteger reds)))
725 return (n, t)
727addAcc :: Name -> Maybe Accessibility -> IParser ()
728addAcc n a = do i <- getState
729 setState (i { hide_list = (n, a) : hide_list i })
731pCaseExpr syn = do
732 reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
733 openBlock
734 pushIndent
735 opts <- many1 (do notEndBlock
736 x <- pCaseOpt syn
737 pKeepTerminator
738 return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
739 popIndent
740 closeBlock
741 return (PCase fc scr opts)
743pProofExpr syn = do
744 reserved "proof"; lchar '{'
745 ts <- endBy (pTactic syn) (lchar ';')
746 lchar '}'
747 return (PProof ts)
749pTacticsExpr syn = do
750 reserved "tactics"; lchar '{'
751 ts <- endBy (pTactic syn) (lchar ';')
752 lchar '}'
753 return (PTactics ts)
755pSimpleExpr syn =
756 try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t)
757 <|> do lchar '?'; x <- pName; return (PMetavar x)
758 <|> do lchar '%'; fc <- pfc; reserved "instance"; return (PResolveTC fc)
759 <|> do reserved "refl"; fc <- pfc;
760 tm <- option Placeholder (do lchar '{'; t <- pExpr syn; lchar '}';
761 return t)
762 return (PRefl fc tm)
763-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)
764 <|> pProofExpr syn
765 <|> pTacticsExpr syn
766 <|> pCaseExpr syn
767 <|> try (do x <- pfName
768 fc <- pfc
769 return (PRef fc x))
770 <|> try (do lchar '!'; x <- pfName
771 fc <- pfc
772 return (PInferRef fc x))
773 <|> try (pList syn)
774 <|> try (pComprehension syn)
775 <|> try (pAlt syn)
776 <|> try (pIdiom syn)
777 <|> try (do lchar '('
778 bracketed (noImp syn))
779 <|> try (do c <- pConstant
780 fc <- pfc
781 return (modifyConst syn fc (PConstant c)))
782 <|> do reserved "Type"; return PType
783 <|> try (do symbol "()"
784 fc <- pfc
785 return (PTrue fc))
786 <|> try (do symbol "_|_"
787 fc <- pfc
788 return (PFalse fc))
789 <|> do lchar '_'; return Placeholder
790 <|> pSimpleExtExpr syn
792bracketed syn =
793 try (pPair syn)
794 <|> try (do e <- pExpr syn; lchar ')'; return e)
795-- <|> try (do reserved "typed"
796-- e <- pExpr syn; symbol ":"; t <- pExpr syn; lchar ')'
797-- return (PTyped e t))
798 <|> try (do fc <- pfc; o <- operator; e <- pExpr syn; lchar ')'
799 return $ PLam (MN 1000 "ARG") Placeholder
800 (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),
801 pexp e]))
802 <|> try (do fc <- pfc; e <- pSimpleExpr syn; o <- operator; lchar ')'
803 return $ PLam (MN 1000 "ARG") Placeholder
804 (PApp fc (PRef fc (UN o)) [pexp e,
805 pexp (PRef fc (MN 1000 "ARG"))]))
807pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
808pCaseOpt syn = do lhs <- pExpr (syn { inPattern = True })
809 symbol "=>"; rhs <- pExpr syn
810 return (lhs, rhs)
812-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
813-- big integer, otherwise try fromInteger and the constants as alternatives.
814-- a better solution would be to fix fromInteger to work with Integer, as the
815-- name suggests, rather than Int
817modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
818modifyConst syn fc (PConstant (BI x))
819 | not (inPattern syn)
820 = PAlternative False
821 (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI (fromInteger x)))]
822 : consts)
823 | otherwise = PAlternative False consts
824 where
825 consts = [ PConstant (BI x)
826 , PConstant (I (fromInteger x))
827 , PConstant (B8 (fromInteger x))
828 , PConstant (B16 (fromInteger x))
829 , PConstant (B32 (fromInteger x))
830 , PConstant (B64 (fromInteger x))
831 ]
832modifyConst syn fc x = x
835pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']'
836 return (mkList fc xs)
837 where
838 mkList fc [] = PRef fc (UN "Nil")
839 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
841pPair syn = try (do l <- pExpr syn
842 fc <- pfc
843 rest <- restTuple
844 case rest of
845 [] -> return l
846 [Left r] -> return (PPair fc l r)
847 [Right r] -> return (PDPair fc l Placeholder r))
848 <|> try (do x <- ntuple
849 lchar ')'
850 return x)
851 <|> do ln <- pName; lchar ':'
852 lty <- pExpr syn
853 reservedOp "**"
854 fc <- pfc
855 r <- pExpr syn
856 lchar ')'
857 return (PDPair fc (PRef fc ln) lty r)
858 where
859 restTuple = do lchar ')'; return []
860 <|> do lchar ','
861 r <- pExpr syn
862 lchar ')'
863 return [Left r]
864 <|> do reservedOp "**"
865 r <- pExpr syn
866 lchar ')'
867 return [Right r]
868 ntuple = try (do l <- pExpr syn; fc <- pfc; lchar ','
869 rest <- ntuple
870 return (PPair fc l rest))
871 <|> (do l <- pExpr syn; fc <- pfc; lchar ','
872 r <- pExpr syn
873 return (PPair fc l r))
875pAlt syn = do symbol "(|"; alts <- sepBy1 (pExpr' syn) (lchar ','); symbol "|)"
876 return (PAlternative False alts)
878pHSimpleExpr syn
879 = do lchar '.'
880 e <- pSimpleExpr syn
881 return $ PHidden e
882 <|> pSimpleExpr syn
884pMatchApp syn = do ty <- pSimpleExpr syn
885 symbol "<=="
886 fc <- pfc
887 f <- pfName
888 return (PLet (MN 0 "match")
889 ty
890 (PMatchApp fc f)
891 (PRef fc (MN 0 "match")))
893pUnifyLog syn = do lchar '%'; reserved "unifyLog";
894 tm <- pSimpleExpr syn
895 return (PUnifyLog tm)
897pApp syn = do f <- pSimpleExpr syn
898 fc <- pfc
899 args <- many1 (do notEndApp
900 pArg syn)
901 i <- getState
902 return (dslify i $ PApp fc f args)
903 where
904 dslify i (PApp fc (PRef _ f) [a])
905 | [d] <- lookupCtxt f (idris_dsls i)
906 = desugar (syn { dsl_info = d }) i (getTm a)
907 dslify i t = t
909pArg :: SyntaxInfo -> IParser PArg
910pArg syn = try (pImplicitArg syn)
911 <|> try (pConstraintArg syn)
912 <|> do e <- pSimpleExpr syn
913 return (pexp e)
915pImplicitArg syn = do lchar '{'
916 n <- pName
917 fc <- pfc
918 v <- option (PRef fc n) (do lchar '='
919 pExpr syn)
920 lchar '}'
921 return (pimp n v)
923pConstraintArg syn = do symbol "@{"
924 e <- pExpr syn
925 symbol "}"
926 return (pconst e)
928pRecordType syn
929 = do reserved "record"
930 lchar '{'
931 fields <- sepBy1 pFieldType (lchar ',')
932 lchar '}'
933 fc <- pfc
934 rec <- option Nothing (do e <- pSimpleExpr syn
935 return (Just e))
936 case rec of
937 Nothing ->
938 return (PLam (MN 0 "fldx") Placeholder
939 (applyAll fc fields (PRef fc (MN 0 "fldx"))))
940 Just v -> return (applyAll fc fields v)
941 where pFieldType = do n <- pfName
942 lchar '='
943 e <- pExpr syn
944 return (n, e)
945 applyAll fc [] x = x
946 applyAll fc ((n, e) : es) x
947 = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])
949mkType (UN n) = UN ("set_" ++ n)
950mkType (MN 0 n) = MN 0 ("set_" ++ n)
951mkType (NS n s) = NS (mkType n) s
953noImp syn = syn { implicitAllowed = False }
954impOK syn = syn { implicitAllowed = True }
956pTSig syn = do lchar ':'; pTExpr syn
958pTExpr syn = do cs <- if implicitAllowed syn then pConstList syn else return []
959 sc <- pExpr syn
960 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
962pLambda syn = do lchar '\\'
963 try (do xt <- tyOptDeclList syn
964 symbol "=>"
965 sc <- pExpr syn
966 return (bindList PLam xt sc)
967 <|> (do ps <- sepBy (do fc <- pfc
968 e <- pSimpleExpr syn
969 return (fc, e)) (lchar ',')
970 symbol "=>"
971 sc <- pExpr syn
972 return (pmList (zip [0..] ps) sc)))
973 where pmList [] sc = sc
974 pmList ((i, (fc, x)) : xs) sc
975 = PLam (MN i "lamp") Placeholder
976 (PCase fc (PRef fc (MN i "lamp"))
977 [(x, pmList xs sc)])
979pRewriteTerm syn =
980 do reserved "rewrite"
981 fc <- pfc
982 prf <- pExpr syn
983 giving <- option Nothing
984 (do symbol "==>"; tm <- pExpr' syn
985 return (Just tm))
986 reserved "in"; sc <- pExpr syn
987 return (PRewrite fc
988 (PApp fc (PRef fc (UN "sym")) [pexp prf]) sc
989 giving)
991pLet syn = try (do reserved "let"; n <- pName;
992 ty <- option Placeholder (do lchar ':'; pExpr' syn)
993 lchar '='
994 v <- pExpr syn
995 reserved "in"; sc <- pExpr syn
996 return (PLet n ty v sc))
997 <|> (do reserved "let"; fc <- pfc; pat <- pExpr' (syn { inPattern = True } )
998 symbol "="; v <- pExpr syn
999 reserved "in"; sc <- pExpr syn
1000 return (PCase fc v [(pat, sc)]))
1002pPi syn =
1003 try (do lazy <- if implicitAllowed syn -- laziness is top level only
1004 then option False (do lchar '|'; return True)
1005 else return False
1006 st <- pStatic
1007 lchar '('; xt <- tyDeclList syn; lchar ')'
1008 doc <- option "" (pDocComment '^')
1009 symbol "->"
1010 sc <- pExpr syn
1011 return (bindList (PPi (Exp lazy st doc)) xt sc))
1012 <|> try (if implicitAllowed syn
1013 then do lazy <- option False (do lchar '|'
1014 return True)
1015 st <- pStatic
1016 lchar '{'
1017 xt <- tyDeclList syn
1018 lchar '}'
1019 symbol "->"
1020 sc <- pExpr syn
1021 return (bindList (PPi (Imp lazy st "")) xt sc)
1022 else fail "No implicit arguments allowed here")
1023 <|> try (do lchar '{'
1024 reserved "auto"
1025 xt <- tyDeclList syn
1026 lchar '}'
1027 symbol "->"
1028 sc <- pExpr syn
1029 return (bindList (PPi
1030 (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))
1031 <|> try (do lchar '{'
1032 reserved "default"
1033 script <- pSimpleExpr syn
1034 xt <- tyDeclList syn
1035 lchar '}'
1036 symbol "->"
1037 sc <- pExpr syn
1038 return (bindList (PPi (TacImp False Dynamic script "")) xt sc))
1039 <|> do --lazy <- option False (do lchar '|'; return True)
1040 lchar '{'
1041 reserved "static"
1042 lchar '}'
1043 t <- pExpr' syn
1044 symbol "->"
1045 sc <- pExpr syn
1046 return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)
1048pConstList :: SyntaxInfo -> IParser [PTerm]
1049pConstList syn = try (do lchar '('
1050 tys <- sepBy1 (pExpr' (noImp syn)) (lchar ',')
1051 lchar ')'
1052 reservedOp "=>"
1053 return tys)
1054 <|> try (do t <- pExpr (noImp syn)
1055 reservedOp "=>"
1056 return [t])
1057 <|> return []
1059usingDeclList syn
1060 = try (sepBy1 (usingDecl syn) (lchar ','))
1061 <|> do ns <- sepBy1 pName (lchar ',')
1062 t <- pTSig (noImp syn)
1063 return (map (\x -> UImplicit x t) ns)
1065usingDecl syn = try (do x <- pfName
1066 t <- pTSig (noImp syn)
1067 return (UImplicit x t))
1068 <|> do c <- pfName
1069 xs <- many1 pfName
1070 return (UConstraint c xs)
1072tyDeclList syn = try (sepBy1 (do x <- pfName
1073 t <- pTSig (noImp syn)
1074 return (x,t))
1075 (lchar ','))
1076 <|> do ns <- sepBy1 pName (lchar ',')
1077 t <- pTSig (noImp syn)
1078 return (map (\x -> (x, t)) ns)
1080tyOptDeclList syn = sepBy1 (do x <- pfName;
1081 t <- option Placeholder (do lchar ':'
1082 pExpr syn)
1083 return (x,t))
1084 (lchar ',')
1086bindList b [] sc = sc
1087bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
1089pComprehension syn
1090 = do lchar '['
1091 fc <- pfc
1092 pat <- pExpr syn
1093 lchar '|'
1094 qs <- sepBy1 (pDo syn) (lchar ',')
1095 lchar ']'
1096 return (PDoBlock (map addGuard qs ++
1097 [DoExp fc (PApp fc (PRef fc (UN "return"))
1098 [pexp pat])]))
1099 where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
1100 [pexp e])
1101 addGuard x = x
1103pDoBlock syn
1104 = do reserved "do"
1105 openBlock
1106 pushIndent
1107 ds <- many1 (do notEndBlock
1108 x <- pDo syn
1109 pKeepTerminator
1110 return x)
1111 popIndent
1112 closeBlock
1113 return (PDoBlock ds)
1115pDo syn
1116 = try (do reserved "let"
1117 i <- pName;
1118 ty <- option Placeholder (do lchar ':'
1119 pExpr' syn)
1120 reservedOp "="
1121 fc <- pfc
1122 e <- pExpr syn
1123 return (DoLet fc i ty e))
1124 <|> try (do reserved "let"
1125 i <- pExpr' syn
1126 reservedOp "="
1127 fc <- pfc
1128 sc <- pExpr syn
1129 return (DoLetP fc i sc))
1130 <|> try (do i <- pName
1131 symbol "<-"
1132 fc <- pfc
1133 e <- pExpr syn;
1134 return (DoBind fc i e))
1135 <|> try (do i <- pExpr' syn
1136 symbol "<-"
1137 fc <- pfc
1138 e <- pExpr syn;
1139 return (DoBindP fc i e))
1140 <|> try (do e <- pExpr syn
1141 fc <- pfc
1142 return (DoExp fc e))
1144pIdiom syn
1145 = do symbol "[|"
1146 fc <- pfc
1147 e <- pExpr syn
1148 symbol "|]"
1149 return (PIdiom fc e)
1151pConstant :: IParser Const
1152pConstant = do reserved "Integer";return (AType (ATInt ITBig))
1153 <|> do reserved "Int"; return (AType (ATInt ITNative))
1154 <|> do reserved "Char"; return (AType (ATInt ITChar))
1155 <|> do reserved "Float"; return (AType ATFloat)
1156 <|> do reserved "String"; return StrType
1157 <|> do reserved "Ptr"; return PtrType
1158 <|> do reserved "Bits8"; return (AType (ATInt (ITFixed IT8)))
1159 <|> do reserved "Bits16"; return (AType (ATInt (ITFixed IT16)))
1160 <|> do reserved "Bits32"; return (AType (ATInt (ITFixed IT32)))
1161 <|> do reserved "Bits64"; return (AType (ATInt (ITFixed IT64)))
1162 <|> do reserved "Bits8x16"; return (AType (ATInt (ITVec IT8 16)))
1163 <|> do reserved "Bits16x8"; return (AType (ATInt (ITVec IT16 8)))
1164 <|> do reserved "Bits32x4"; return (AType (ATInt (ITVec IT32 4)))
1165 <|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2)))
1166 <|> try (do f <- float; return $ Fl f)
1167 <|> try (do i <- natural; return $ BI i)
1168 <|> try (do s <- strlit; return $ Str s)
1169 <|> try (do c <- chlit; return $ Ch c)
1171pStatic :: IParser Static
1172pStatic = do lchar '['
1173 reserved "static"
1174 lchar ']';
1175 return Static
1176 <|> return Dynamic
1178table fixes
1179 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
1180 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]
1181 ++ toTable (reverse fixes) ++
1182 [[backtick],
1183 [binary "=" PEq AssocLeft],
1184 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
1186toTable fs = map (map toBin)
1187 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
1188 where toBin (Fix (PrefixN _) op) = prefix op
1189 (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
1190 toBin (Fix f op)
1191 = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
1192 assoc (Infixl _) = AssocLeft
1193 assoc (Infixr _) = AssocRight
1194 assoc (InfixN _) = AssocNone
1196binary name f = Infix (do fc <- pfc
1197 reservedOp name
1198 doc <- option "" (pDocComment '^')
1199 return (f fc))
1200prefix name f = Prefix (do reservedOp name
1201 fc <- pfc;
1202 return (f fc))
1203backtick = Infix (do lchar '`'; n <- pfName
1204 lchar '`'
1205 fc <- pfc
1206 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
1208--------- Data declarations ---------
1210-- (works for classes too - 'abstract' means the data/class is visible but members not)
1211accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()
1212accData (Just Frozen) n ns = do addAcc n (Just Frozen)
1213 mapM_ (\n -> addAcc n (Just Hidden)) ns
1214accData a n ns = do addAcc n a
1215 mapM_ (`addAcc` a) ns
1217pRecord :: SyntaxInfo -> IParser PDecl
1218pRecord syn = do doc <- option "" (pDocComment '|')
1219 acc <- pAccessibility
1220 reserved "record"
1221 fc <- pfc
1222 tyn_in <- pfName
1223 ty <- pTSig (impOK syn)
1224 let tyn = expandNS syn tyn_in
1225 reserved "where"
1226 openBlock
1227 pushIndent
1228 (cdoc, cn, cty, _) <- pConstructor syn
1229 pKeepTerminator
1230 popIndent
1231 closeBlock
1232 accData acc tyn [cn]
1233 let rsyn = syn { syn_namespace = show (nsroot tyn) :
1234 syn_namespace syn }
1235 let fns = getRecNames rsyn cty
1236 mapM_ (\n -> addAcc n acc) fns
1237 return $ PRecord doc rsyn fc tyn ty cdoc cn cty
1238 where
1239 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
1240 ++ getRecNames syn sc
1241 getRecNames _ _ = []
1243 toFreeze (Just Frozen) = Just Hidden
1244 toFreeze x = x
1246pDataI = do reserved "data"; return False
1247 <|> do reserved "codata"; return True
1249pData :: SyntaxInfo -> IParser PDecl
1250pData syn = try (do doc <- option "" (pDocComment '|')
1251 acc <- pAccessibility
1252 co <- pDataI
1253 fc <- pfc
1254 tyn_in <- pfName
1255 ty <- pTSig (impOK syn)
1256 let tyn = expandNS syn tyn_in
1257 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1258 reserved "where"
1259 openBlock
1260 pushIndent
1261 cons <- many (do notEndBlock
1262 c <- pConstructor syn
1263 pKeepTerminator
1264 return c) -- (lchar '|')
1265 popIndent
1266 closeBlock
1267 accData acc tyn (map (\ (_, n, _, _) -> n) cons)
1268 return $ PData doc syn fc co (PDatadecl tyn ty cons)))
1269 <|> try (do doc <- option "" (pDocComment '|')
1270 pushIndent
1271 acc <- pAccessibility
1272 co <- pDataI
1273 fc <- pfc
1274 tyn_in <- pfName
1275 args <- many pName
1276 let ty = bindArgs (map (const PType) args) PType
1277 let tyn = expandNS syn tyn_in
1278 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1279 try (lchar '=') <|> do reserved "where"
1280 let kw = (if co then "co" else "") ++ "data "
1281 let n = show tyn_in ++ " "
1282 let s = kw ++ n
1283 let as = concat (intersperse " " $ map show args) ++ " "
1284 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
1285 let ss = concat (intersperse " -> " $ map (const "Type") args)
1286 let fix1 = s ++ as ++ " = ..."
1287 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
1288 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
1289 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
1291 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
1292 pTerminator
1293 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
1294 cons' <- mapM (\ (doc, x, cargs, cfc) ->
1295 do let cty = bindArgs cargs conty
1296 return (doc, x, cty, cfc)) cons
1297 accData acc tyn (map (\ (_, n, _, _) -> n) cons')
1298 return $ PData doc syn fc co (PDatadecl tyn ty cons')))
1299 where
1300 mkPApp fc t [] = t
1301 mkPApp fc t xs = PApp fc t (map pexp xs)
1303bindArgs :: [PTerm] -> PTerm -> PTerm
1304bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
1306pConstructor :: SyntaxInfo -> IParser (String, Name, PTerm, FC)
1307pConstructor syn
1308 = do doc <- option "" (pDocComment '|')
1309 cn_in <- pfName; fc <- pfc
1310 let cn = expandNS syn cn_in
1311 ty <- pTSig (impOK syn)
1312-- ty' <- implicit syn cn ty
1313 return (doc, cn, ty, fc)
1316pSimpleCon :: SyntaxInfo -> IParser (String, Name, [PTerm], FC)
1317pSimpleCon syn
1318 = do cn_in <- pfName
1319 let cn = expandNS syn cn_in
1320 fc <- pfc
1321 args <- many (do notEndApp
1322 pSimpleExpr syn)
1323 doc <- option "" (pDocComment '^')
1324 return (doc, cn, args, fc)
1326--------- DSL syntax overloading ---------
1328pDSL :: SyntaxInfo -> IParser PDecl
1329pDSL syn = do reserved "dsl"
1330 n <- pfName
1331 openBlock
1332 pushIndent
1333 bs <- many1 (do notEndBlock
1334 b <- pOverload syn
1335 pKeepTerminator
1336 return b)
1337 popIndent; closeBlock
1338 let dsl = mkDSL bs (dsl_info syn)
1339 checkDSL dsl
1340 i <- getState
1341 setState (i { idris_dsls = addDef n dsl (idris_dsls i) })
1342 return (PDSL n dsl)
1343 where mkDSL bs dsl = let var = lookup "variable" bs
1344 first = lookup "index_first" bs
1345 next = lookup "index_next" bs
1346 leto = lookup "let" bs
1347 lambda = lookup "lambda" bs in
1348 initDSL { dsl_var = var,
1349 index_first = first,
1350 index_next = next,
1351 dsl_lambda = lambda,
1352 dsl_let = leto }
1354checkDSL :: DSL -> IParser ()
1355checkDSL dsl = return ()
1357pOverload :: SyntaxInfo -> IParser (String, PTerm)
1358pOverload syn = do o <- identifier <|> do reserved "let"
1359 return "let"
1360 if o `notElem` overloadable
1361 then fail $ show o ++ " is not an overloading"
1362 else do
1363 lchar '='
1364 t <- pExpr syn
1365 return (o, t)
1366 where overloadable = ["let","lambda","index_first","index_next","variable"]
1368--------- Pattern match clauses ---------
1370pPattern :: SyntaxInfo -> IParser PDecl
1371pPattern syn = do fc <- pfc
1372 clause <- pClause syn
1373 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
1375pCAF :: SyntaxInfo -> IParser PDecl
1376pCAF syn = do reserved "let"
1377 n_in <- pfName; let n = expandNS syn n_in
1378 lchar '='
1379 t <- pExpr syn
1380 pTerminator
1381 fc <- pfc
1382 return (PCAF fc n t)
1384pArgExpr syn = let syn' = syn { inPattern = True } in
1385 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
1387pRHS :: SyntaxInfo -> Name -> IParser PTerm
1388pRHS syn n = do lchar '='; pExpr syn
1389 <|> do symbol "?=";
1390 name <- option n' (do symbol "{"; n <- pfName; symbol "}";
1391 return n)
1392 rhs <- pExpr syn
1393 return (addLet name rhs)
1394 <|> do reserved "impossible"; return PImpossible
1395 where mkN (UN x) = UN (x++"_lemma_1")
1396 mkN (NS x n) = NS (mkN x) n
1397 n' = mkN n
1399 addLet nm (PLet n ty val rhs) = PLet n ty val (addLet nm rhs)
1400 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
1401 where addLetC (l, r) = (l, addLet nm r)
1402 addLet nm rhs = (PLet (UN "value") Placeholder rhs (PMetavar nm))
1404pClause :: SyntaxInfo -> IParser PClause
1405pClause syn
1406 = try (do pushIndent
1407 n_in <- pfName; let n = expandNS syn n_in
1408 cargs <- many (pConstraintArg syn)
1409 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1410 fc <- pfc
1411 args <- many (try (pImplicitArg (syn { inPattern = True } ))
1412 <|> (fmap pexp (pArgExpr syn)))
1413 wargs <- many (pWExpr syn)
1414 rhs <- pRHS syn n
1415 ist <- getState
1416 let ctxt = tt_ctxt ist
1417 let wsyn = syn { syn_namespace = [] }
1418 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1419 popIndent
1420 return x,
1421 do pTerminator
1422 return ([], [])]
1423 let capp = PApp fc (PRef fc n)
1424 (iargs ++ cargs ++ args)
1425 ist <- getState
1426 setState (ist { lastParse = Just n })
1427 return $ PClause fc n capp wargs rhs wheres)
1428 <|> try (do pushIndent
1429 ty <- pSimpleExpr syn
1430 symbol "<=="
1431 fc <- pfc
1432 n_in <- pfName; let n = expandNS syn n_in
1433 rhs <- pRHS syn n
1434 ist <- getState
1435 let ctxt = tt_ctxt ist
1436 let wsyn = syn { syn_namespace = [] }
1437 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1438 popIndent
1439 return x,
1440 do pTerminator
1441 return ([], [])]
1442 let capp = PLet (MN 0 "match")
1443 ty
1444 (PMatchApp fc n)
1445 (PRef fc (MN 0 "match"))
1446 ist <- getState
1447 setState (ist { lastParse = Just n })
1448 return $ PClause fc n capp [] rhs wheres)
1449 <|> try (do pushIndent
1450 wargs <- many1 (pWExpr syn)
1451 ist <- getState
1452 n <- case lastParse ist of
1453 Just t -> return t
1454 Nothing -> fail "Invalid clause"
1455 fc <- pfc
1456 rhs <- pRHS syn n
1457 let ctxt = tt_ctxt ist
1458 let wsyn = syn { syn_namespace = [] }
1459 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1460 popIndent
1461 return x,
1462 do pTerminator
1463 return ([], [])]
1464 return $ PClauseR fc wargs rhs wheres)
1466 <|> try (do pushIndent
1467 n_in <- pfName; let n = expandNS syn n_in
1468 cargs <- many (pConstraintArg syn)
1469 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1470 fc <- pfc
1471 args <- many (try (pImplicitArg (syn { inPattern = True } ))
1472 <|> (fmap pexp (pArgExpr syn)))
1473 wargs <- many (pWExpr syn)
1474 let capp = PApp fc (PRef fc n)
1475 (iargs ++ cargs ++ args)
1476 ist <- getState
1477 setState (ist { lastParse = Just n })
1478 reserved "with"
1479 wval <- pSimpleExpr syn
1480 openBlock
1481 ds <- many1 $ pFunDecl syn
1482 let withs = map (fillLHSD n capp wargs) $ concat ds
1483 closeBlock
1484 popIndent
1485 return $ PWith fc n capp wargs wval withs)
1487 <|> try (do wargs <- many1 (pWExpr syn)
1488 fc <- pfc
1489 reserved "with"
1490 wval <- pSimpleExpr syn
1491 openBlock
1492 ds <- many1 $ pFunDecl syn
1493 let withs = concat ds
1494 closeBlock
1495 return $ PWithR fc wargs wval withs)
1497 <|> do pushIndent
1498 l <- pArgExpr syn
1499 op <- operator
1500 let n = expandNS syn (UN op)
1501 r <- pArgExpr syn
1502 fc <- pfc
1503 wargs <- many (pWExpr syn)
1504 rhs <- pRHS syn n
1505 let wsyn = syn { syn_namespace = [] }
1506 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1507 popIndent
1508 return x,
1509 do pTerminator
1510 return ([], [])]
1511 ist <- getState
1512 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1513 setState (ist { lastParse = Just n })
1514 return $ PClause fc n capp wargs rhs wheres
1516 <|> do l <- pArgExpr syn
1517 op <- operator
1518 let n = expandNS syn (UN op)
1519 r <- pArgExpr syn
1520 fc <- pfc
1521 wargs <- many (pWExpr syn)
1522 reserved "with"
1523 wval <- pSimpleExpr syn
1524 openBlock
1525 ds <- many1 $ pFunDecl syn
1526 closeBlock
1527 ist <- getState
1528 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1529 let withs = map (fillLHSD n capp wargs) $ concat ds
1530 setState (ist { lastParse = Just n })
1531 return $ PWith fc n capp wargs wval withs
1532 where
1533 fillLHS n capp owargs (PClauseR fc wargs v ws)
1534 = PClause fc n capp (owargs ++ wargs) v ws
1535 fillLHS n capp owargs (PWithR fc wargs v ws)
1536 = PWith fc n capp (owargs ++ wargs) v
1537 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1538 fillLHS _ _ _ c = c
1540 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1541 fillLHSD n c a x = x
1543pWExpr :: SyntaxInfo -> IParser PTerm
1544pWExpr syn = do lchar '|'
1545 pExpr' syn
1547pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
1548pWhereblock n syn
1549 = do reserved "where"; openBlock
1550 ds <- many1 $ pDecl syn
1551 let dns = concatMap (concatMap declared) ds
1552 closeBlock
1553 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1555pCodegen :: IParser Codegen
1556pCodegen = try (do reserved "C"; return ViaC)
1557 <|> try (do reserved "Java"; return ViaJava)
1558 <|> try (do reserved "JavaScript"; return ViaJavaScript)
1559 <|> try (do reserved "Node"; return ViaNode)
1560 <|> try (do reserved "LLVM"; return ViaLLVM)
1561 <|> try (do reserved "Bytecode"; return Bytecode)
1563pDirective :: SyntaxInfo -> IParser [PDecl]
1564pDirective syn = try (do lchar '%'; reserved "lib"; cgn <- pCodegen; lib <- strlit;
1565 return [PDirective (do addLib cgn lib
1566 addIBC (IBCLib cgn lib))])
1567 <|> try (do lchar '%'; reserved "link"; cgn <- pCodegen; obj <- strlit;
1568 return [PDirective (do datadir <- liftIO getDataDir
1569 o <- liftIO $ findInPath [".", datadir] obj
1570 addIBC (IBCObj cgn o)
1571 addObjectFile cgn o)])
1572 <|> try (do lchar '%'; reserved "include"; cgn <- pCodegen; hdr <- strlit;
1573 return [PDirective (do addHdr cgn hdr
1574 addIBC (IBCHeader cgn hdr))])
1575 <|> try (do lchar '%'; reserved "hide"; n <- iName []
1576 return [PDirective (do setAccessibility n Hidden
1577 addIBC (IBCAccess n Hidden))])
1578 <|> try (do lchar '%'; reserved "freeze"; n <- iName []
1579 return [PDirective (do setAccessibility n Frozen
1580 addIBC (IBCAccess n Frozen))])
1581 <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'
1582 return [PDirective (do i <- getIState
1583 putIState (i { default_access = acc }))])
1584 <|> try (do lchar '%'; reserved "default"; tot <- pTotality
1585 i <- getState
1586 setState (i { default_total = tot } )
1587 return [PDirective (do i <- getIState
1588 putIState (i { default_total = tot }))])
1589 <|> try (do lchar '%'; reserved "logging"; i <- natural;
1590 return [PDirective (setLogLevel (fromInteger i))])
1591 <|> try (do lchar '%'; reserved "dynamic"; libs <- sepBy1 strlit (lchar ',');
1592 return [PDirective (do added <- addDyLib libs
1593 case added of
1594 Left lib -> addIBC (IBCDyLib (lib_name lib))
1595 Right msg ->
1596 fail $ msg)])
1597 <|> try (do lchar '%'; reserved "language"; ext <- reserved "TypeProviders";
1598 return [PDirective (addLangExt TypeProviders)])
1600pProvider :: SyntaxInfo -> IParser [PDecl]
1601pProvider syn = do lchar '%'; reserved "provide";
1602 lchar '('; n <- pfName; t <- pTSig syn; lchar ')'
1603 fc <- pfc
1604 reserved "with"
1605 e <- pExpr syn
1606 return [PProvider syn fc n t e]
1608pTransform :: SyntaxInfo -> IParser [PDecl]
1609pTransform syn = do lchar '%'; reserved "transform";
1610 -- leave it unchecked, until we work out what this should
1611 -- actually mean...
1612-- safety <- option True (do reserved "unsafe"
1613-- return False)
1614 lhs <- pExpr syn
1615 fc <- pfc
1616 symbol "==>"
1617 rhs <- pExpr syn
1618 return [PTransform fc False lhs rhs]
1620pTactic :: SyntaxInfo -> IParser PTactic
1621pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
1622 return $ Intro ns
1623 <|> do reserved "intros"; return Intros
1624 <|> try (do reserved "refine"; n <- pName
1625 imps <- many1 imp
1626 return $ Refine n imps)
1627 <|> do reserved "refine"; n <- pName
1628 i <- getState
1629 return $ Refine n []
1630 <|> do reserved "mrefine"; n <- pName
1631 i <- getState
1632 return $ MatchRefine n
1633 <|> do reserved "rewrite"; t <- pExpr syn;
1634 i <- getState
1635 return $ Rewrite (desugar syn i t)
1636 <|> do reserved "equiv"; t <- pExpr syn;
1637 i <- getState
1638 return $ Equiv (desugar syn i t)
1639 <|> try (do reserved "let"; n <- pName; lchar ':';
1640 ty <- pExpr' syn; lchar '='; t <- pExpr syn;
1641 i <- getState
1642 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
1643 <|> try (do reserved "let"; n <- pName; lchar '=';
1644 t <- pExpr syn;
1645 i <- getState
1646 return $ LetTac n (desugar syn i t))
1647 <|> do reserved "focus"; n <- pName
1648 return $ Focus n
1649 <|> do reserved "exact"; t <- pExpr syn;
1650 i <- getState
1651 return $ Exact (desugar syn i t)
1652 <|> do reserved "applyTactic"; t <- pExpr syn;
1653 i <- getState
1654 return $ ApplyTactic (desugar syn i t)
1655 <|> do reserved "reflect"; t <- pExpr syn;
1656 i <- getState
1657 return $ Reflect (desugar syn i t)
1658 <|> do reserved "fill"; t <- pExpr syn;
1659 i <- getState
1660 return $ Fill (desugar syn i t)
1661 <|> do reserved "try"; t <- pTactic syn;
1662 lchar '|';
1663 t1 <- pTactic syn
1664 return $ Try t t1
1665 <|> do lchar '{'
1666 t <- pTactic syn;
1667 lchar ';';
1668 t1 <- pTactic syn;
1669 lchar '}'
1670 return $ TSeq t t1
1671 <|> do reserved "compute"; return Compute
1672 <|> do reserved "trivial"; return Trivial
1673 <|> do reserved "solve"; return Solve
1674 <|> do reserved "attack"; return Attack
1675 <|> do reserved "state"; return ProofState
1676 <|> do reserved "term"; return ProofTerm
1677 <|> do reserved "undo"; return Undo
1678 <|> do reserved "qed"; return Qed
1679 <|> do reserved "abandon"; return Abandon
1680 <|> do lchar ':'; reserved "q"; return Abandon
1681 where
1682 imp = do lchar '?'; return False
1683 <|> do lchar '_'; return True