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