git.iko.soy/Idris-dev
on 321b8fd help sign in
Idris-dev/src/Idris/Parser.hs
1585 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
616 <|> pComprehension syn
618pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
619pExtensions syn rules = choice (map (try . pExt syn) (filter valid rules))
620 where
621 valid (Rule _ _ AnySyntax) = True
622 valid (Rule _ _ PatternSyntax) = inPattern syn
623 valid (Rule _ _ TermSyntax) = not (inPattern syn)
626data SynMatch = SynTm PTerm | SynBind Name
628pExt :: SyntaxInfo -> Syntax -> IParser PTerm
629pExt syn (Rule ssym ptm _)
630 = do smap <- mapM pSymbol ssym
631 let ns = mapMaybe id smap
632 return (update ns ptm) -- updated with smap
633 where
634 pSymbol (Keyword n) = do reserved (show n); return Nothing
635 pSymbol (Expr n) = do tm <- pExpr syn
636 return $ Just (n, SynTm tm)
637 pSymbol (SimpleExpr n) = do tm <- pSimpleExpr syn
638 return $ Just (n, SynTm tm)
639 pSymbol (Binding n) = do b <- pName
640 return $ Just (n, SynBind b)
641 pSymbol (Symbol s) = do symbol s
642 return Nothing
643 dropn n [] = []
644 dropn n ((x,t) : xs) | n == x = xs
645 | otherwise = (x,t):dropn n xs
647 updateB ns n = case lookup n ns of
648 Just (SynBind t) -> t
649 _ -> n
651 update ns (PRef fc n) = case lookup n ns of
652 Just (SynTm t) -> t
653 _ -> PRef fc n
654 update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)
655 update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc)
656 update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)
657 (update (dropn n ns) sc)
658 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
659 update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)
660 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)
661 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)
662 update ns (PAlternative a as) = PAlternative a (map (update ns) as)
663 update ns (PHidden t) = PHidden (update ns t)
664 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
665 where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
666 upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds
667 upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)
668 : upd (dropn n ns) ds
669 upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t)
670 : upd ns ds
671 upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)
672 : upd ns ds
673 update ns t = t
675pName = do i <- getState
676 iName (syntax_keywords i)
677 <|> do reserved "instance"
678 i <- getState
679 UN n <- iName (syntax_keywords i)
680 return (UN ('@':n))
682-- | Parser for an operator in function position, i.e. enclosed by `()', with an
683-- optional namespace.
684pOpFront = maybeWithNS pOpFrontNoNS False []
685 where pOpFrontNoNS = do lchar '('; o <- operator; lchar ')'; return o
687pfName = try pOpFront
688 <|> pName
690pTotality :: IParser Bool
691pTotality
692 = do reserved "total"; return True
693 <|> do reserved "partial"; return False
695pAccessibility' :: IParser Accessibility
696pAccessibility'
697 = do reserved "public"; return Public
698 <|> do reserved "abstract"; return Frozen
699 <|> do reserved "private"; return Hidden
701pAccessibility :: IParser (Maybe Accessibility)
702pAccessibility
703 = do acc <- pAccessibility'; return (Just acc)
704 <|> return Nothing
706pFnOpts :: [FnOpt] -> IParser [FnOpt]
707pFnOpts opts
708 = do reserved "total"; pFnOpts (TotalFn : opts)
709 <|> do reserved "partial"; pFnOpts (PartialFn : (opts \\ [TotalFn]))
710 <|> try (do lchar '%'; reserved "export"; c <- strlit;
711 pFnOpts (CExport c : opts))
712 <|> do lchar '%'; reserved "assert_total"; pFnOpts (AssertTotal : opts)
713 <|> do lchar '%'; reserved "specialise";
714 lchar '['; ns <- sepBy pfName (lchar ','); lchar ']'
715 pFnOpts (Specialise ns : opts)
716 <|> do reserved "implicit"; pFnOpts (Implicit : opts)
717 <|> return opts
719addAcc :: Name -> Maybe Accessibility -> IParser ()
720addAcc n a = do i <- getState
721 setState (i { hide_list = (n, a) : hide_list i })
723pCaseExpr syn = do
724 reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
725 openBlock
726 pushIndent
727 opts <- many1 (do notEndBlock
728 x <- pCaseOpt syn
729 pKeepTerminator
730 return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
731 popIndent
732 closeBlock
733 return (PCase fc scr opts)
735pProofExpr syn = do
736 reserved "proof"; lchar '{'
737 ts <- endBy (pTactic syn) (lchar ';')
738 lchar '}'
739 return (PProof ts)
741pTacticsExpr syn = do
742 reserved "tactics"; lchar '{'
743 ts <- endBy (pTactic syn) (lchar ';')
744 lchar '}'
745 return (PTactics ts)
747pSimpleExpr syn =
748 try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t)
749 <|> do lchar '?'; x <- pName; return (PMetavar x)
750 <|> do lchar '%'; fc <- pfc; reserved "instance"; return (PResolveTC fc)
751 <|> do reserved "refl"; fc <- pfc;
752 tm <- option Placeholder (do lchar '{'; t <- pExpr syn; lchar '}';
753 return t)
754 return (PRefl fc tm)
755-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)
756 <|> pProofExpr syn
757 <|> pTacticsExpr syn
758 <|> pCaseExpr syn
759 <|> try (do x <- pfName
760 fc <- pfc
761 return (PRef fc x))
762 <|> try (do lchar '!'; x <- pfName
763 fc <- pfc
764 return (PInferRef fc x))
765 <|> try (pList 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 Nothing 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 <- option False (do lchar '|'; return True)
979 st <- pStatic
980 lchar '('; xt <- tyDeclList syn; lchar ')'
981 doc <- option "" (pDocComment '^')
982 symbol "->"
983 sc <- pExpr syn
984 return (bindList (PPi (Exp lazy st doc)) xt sc))
985 <|> try (if implicitAllowed syn
986 then do lazy <- option False (do lchar '|'
987 return True)
988 st <- pStatic
989 lchar '{'
990 xt <- tyDeclList syn
991 lchar '}'
992 symbol "->"
993 sc <- pExpr syn
994 return (bindList (PPi (Imp lazy st "")) xt sc)
995 else fail "No implicit arguments allowed here")
996 <|> try (do lchar '{'
997 reserved "auto"
998 xt <- tyDeclList syn
999 lchar '}'
1000 symbol "->"
1001 sc <- pExpr syn
1002 return (bindList (PPi
1003 (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))
1004 <|> try (do lchar '{'
1005 reserved "default"
1006 script <- pSimpleExpr syn
1007 xt <- tyDeclList syn
1008 lchar '}'
1009 symbol "->"
1010 sc <- pExpr syn
1011 return (bindList (PPi (TacImp False Dynamic script "")) xt sc))
1012 <|> do --lazy <- option False (do lchar '|'; return True)
1013 lchar '{'
1014 reserved "static"
1015 lchar '}'
1016 t <- pExpr' syn
1017 symbol "->"
1018 sc <- pExpr syn
1019 return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)
1021pConstList :: SyntaxInfo -> IParser [PTerm]
1022pConstList syn = try (do lchar '('
1023 tys <- sepBy1 (pExpr' (noImp syn)) (lchar ',')
1024 lchar ')'
1025 reservedOp "=>"
1026 return tys)
1027 <|> try (do t <- pExpr (noImp syn)
1028 reservedOp "=>"
1029 return [t])
1030 <|> return []
1032tyDeclList syn = try (sepBy1 (do x <- pfName
1033 t <- pTSig (noImp syn)
1034 return (x,t))
1035 (lchar ','))
1036 <|> do ns <- sepBy1 pName (lchar ',')
1037 t <- pTSig (noImp syn)
1038 return (map (\x -> (x, t)) ns)
1040tyOptDeclList syn = sepBy1 (do x <- pfName;
1041 t <- option Placeholder (do lchar ':'
1042 pExpr syn)
1043 return (x,t))
1044 (lchar ',')
1046bindList b [] sc = sc
1047bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
1049pComprehension syn
1050 = do lchar '['
1051 fc <- pfc
1052 pat <- pExpr syn
1053 lchar '|'
1054 qs <- sepBy1 (pDo syn) (lchar ',')
1055 lchar ']'
1056 return (PDoBlock (map addGuard qs ++
1057 [DoExp fc (PApp fc (PRef fc (UN "return"))
1058 [pexp pat])]))
1059 where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
1060 [pexp e])
1061 addGuard x = x
1063pDoBlock syn
1064 = do reserved "do"
1065 openBlock
1066 pushIndent
1067 ds <- many1 (do notEndBlock
1068 x <- pDo syn
1069 pKeepTerminator
1070 return x)
1071 popIndent
1072 closeBlock
1073 return (PDoBlock ds)
1075pDo syn
1076 = try (do reserved "let"
1077 i <- pName;
1078 ty <- option Placeholder (do lchar ':'
1079 pExpr' syn)
1080 reservedOp "="
1081 fc <- pfc
1082 e <- pExpr syn
1083 return (DoLet fc i ty e))
1084 <|> try (do reserved "let"
1085 i <- pExpr' syn
1086 reservedOp "="
1087 fc <- pfc
1088 sc <- pExpr syn
1089 return (DoLetP fc i sc))
1090 <|> try (do i <- pName
1091 symbol "<-"
1092 fc <- pfc
1093 e <- pExpr syn;
1094 return (DoBind fc i e))
1095 <|> try (do i <- pExpr' syn
1096 symbol "<-"
1097 fc <- pfc
1098 e <- pExpr syn;
1099 return (DoBindP fc i e))
1100 <|> try (do e <- pExpr syn
1101 fc <- pfc
1102 return (DoExp fc e))
1104pIdiom syn
1105 = do symbol "[|"
1106 fc <- pfc
1107 e <- pExpr syn
1108 symbol "|]"
1109 return (PIdiom fc e)
1111pConstant :: IParser Const
1112pConstant = do reserved "Integer";return BIType
1113 <|> do reserved "Int"; return IType
1114 <|> do reserved "Char"; return ChType
1115 <|> do reserved "Float"; return FlType
1116 <|> do reserved "String"; return StrType
1117 <|> do reserved "Ptr"; return PtrType
1118 <|> do reserved "Bits8"; return B8Type
1119 <|> do reserved "Bits16"; return B16Type
1120 <|> do reserved "Bits32"; return B32Type
1121 <|> do reserved "Bits64"; return B64Type
1122 <|> try (do f <- float; return $ Fl f)
1123 <|> try (do i <- natural; return $ BI i)
1124 <|> try (do s <- strlit; return $ Str s)
1125 <|> try (do c <- chlit; return $ Ch c)
1127pStatic :: IParser Static
1128pStatic = do lchar '['
1129 reserved "static"
1130 lchar ']';
1131 return Static
1132 <|> return Dynamic
1134table fixes
1135 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
1136 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]
1137 ++ toTable (reverse fixes) ++
1138 [[backtick],
1139 [binary "=" PEq AssocLeft],
1140 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
1142toTable fs = map (map toBin)
1143 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
1144 where toBin (Fix (PrefixN _) op) = prefix op
1145 (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
1146 toBin (Fix f op)
1147 = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
1148 assoc (Infixl _) = AssocLeft
1149 assoc (Infixr _) = AssocRight
1150 assoc (InfixN _) = AssocNone
1152binary name f = Infix (do fc <- pfc
1153 reservedOp name
1154 doc <- option "" (pDocComment '^')
1155 return (f fc))
1156prefix name f = Prefix (do reservedOp name
1157 fc <- pfc;
1158 return (f fc))
1159backtick = Infix (do lchar '`'; n <- pfName
1160 lchar '`'
1161 fc <- pfc
1162 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
1164--------- Data declarations ---------
1166-- (works for classes too - 'abstract' means the data/class is visible but members not)
1167accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()
1168accData (Just Frozen) n ns = do addAcc n (Just Frozen)
1169 mapM_ (\n -> addAcc n (Just Hidden)) ns
1170accData a n ns = do addAcc n a
1171 mapM_ (`addAcc` a) ns
1173pRecord :: SyntaxInfo -> IParser PDecl
1174pRecord syn = do doc <- option "" (pDocComment '|')
1175 acc <- pAccessibility
1176 reserved "record"
1177 fc <- pfc
1178 tyn_in <- pfName
1179 ty <- pTSig (impOK syn)
1180 let tyn = expandNS syn tyn_in
1181 reserved "where"
1182 openBlock
1183 pushIndent
1184 (cdoc, cn, cty, _) <- pConstructor syn
1185 pKeepTerminator
1186 popIndent
1187 closeBlock
1188 accData acc tyn [cn]
1189 let rsyn = syn { syn_namespace = show (nsroot tyn) :
1190 syn_namespace syn }
1191 let fns = getRecNames rsyn cty
1192 mapM_ (\n -> addAcc n acc) fns
1193 return $ PRecord doc rsyn fc tyn ty cdoc cn cty
1194 where
1195 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
1196 ++ getRecNames syn sc
1197 getRecNames _ _ = []
1199 toFreeze (Just Frozen) = Just Hidden
1200 toFreeze x = x
1202pDataI = do reserved "data"; return False
1203 <|> do reserved "codata"; return True
1205pData :: SyntaxInfo -> IParser PDecl
1206pData syn = try (do doc <- option "" (pDocComment '|')
1207 acc <- pAccessibility
1208 co <- pDataI
1209 fc <- pfc
1210 tyn_in <- pfName
1211 ty <- pTSig (impOK syn)
1212 let tyn = expandNS syn tyn_in
1213 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1214 reserved "where"
1215 openBlock
1216 pushIndent
1217 cons <- many (do notEndBlock
1218 c <- pConstructor syn
1219 pKeepTerminator
1220 return c) -- (lchar '|')
1221 popIndent
1222 closeBlock
1223 accData acc tyn (map (\ (_, n, _, _) -> n) cons)
1224 return $ PData doc syn fc co (PDatadecl tyn ty cons)))
1225 <|> try (do doc <- option "" (pDocComment '|')
1226 pushIndent
1227 acc <- pAccessibility
1228 co <- pDataI
1229 fc <- pfc
1230 tyn_in <- pfName
1231 args <- many pName
1232 let ty = bindArgs (map (const PType) args) PType
1233 let tyn = expandNS syn tyn_in
1234 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1235 try (lchar '=') <|> do reserved "where"
1236 let kw = (if co then "co" else "") ++ "data "
1237 let n = show tyn_in ++ " "
1238 let s = kw ++ n
1239 let as = concat (intersperse " " $ map show args) ++ " "
1240 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
1241 let ss = concat (intersperse " -> " $ map (const "Type") args)
1242 let fix1 = s ++ as ++ " = ..."
1243 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
1244 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
1245 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
1247 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
1248 pTerminator
1249 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
1250 cons' <- mapM (\ (doc, x, cargs, cfc) ->
1251 do let cty = bindArgs cargs conty
1252 return (doc, x, cty, cfc)) cons
1253 accData acc tyn (map (\ (_, n, _, _) -> n) cons')
1254 return $ PData doc syn fc co (PDatadecl tyn ty cons')))
1255 where
1256 mkPApp fc t [] = t
1257 mkPApp fc t xs = PApp fc t (map pexp xs)
1259bindArgs :: [PTerm] -> PTerm -> PTerm
1260bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
1262pConstructor :: SyntaxInfo -> IParser (String, Name, PTerm, FC)
1263pConstructor syn
1264 = do doc <- option "" (pDocComment '|')
1265 cn_in <- pfName; fc <- pfc
1266 let cn = expandNS syn cn_in
1267 ty <- pTSig (impOK syn)
1268-- ty' <- implicit syn cn ty
1269 return (doc, cn, ty, fc)
1272pSimpleCon :: SyntaxInfo -> IParser (String, Name, [PTerm], FC)
1273pSimpleCon syn
1274 = do cn_in <- pfName
1275 let cn = expandNS syn cn_in
1276 fc <- pfc
1277 args <- many (do notEndApp
1278 pSimpleExpr syn)
1279 doc <- option "" (pDocComment '^')
1280 return (doc, cn, args, fc)
1282--------- DSL syntax overloading ---------
1284pDSL :: SyntaxInfo -> IParser PDecl
1285pDSL syn = do reserved "dsl"
1286 n <- pfName
1287 openBlock
1288 pushIndent
1289 bs <- many1 (do notEndBlock
1290 b <- pOverload syn
1291 pKeepTerminator
1292 return b)
1293 popIndent; closeBlock
1294 let dsl = mkDSL bs (dsl_info syn)
1295 checkDSL dsl
1296 i <- getState
1297 setState (i { idris_dsls = addDef n dsl (idris_dsls i) })
1298 return (PDSL n dsl)
1299 where mkDSL bs dsl = let var = lookup "variable" bs
1300 first = lookup "index_first" bs
1301 next = lookup "index_next" bs
1302 leto = lookup "let" bs
1303 lambda = lookup "lambda" bs in
1304 initDSL { dsl_var = var,
1305 index_first = first,
1306 index_next = next,
1307 dsl_lambda = lambda,
1308 dsl_let = leto }
1310checkDSL :: DSL -> IParser ()
1311checkDSL dsl = return ()
1313pOverload :: SyntaxInfo -> IParser (String, PTerm)
1314pOverload syn = do o <- identifier <|> do reserved "let"
1315 return "let"
1316 if o `notElem` overloadable
1317 then fail $ show o ++ " is not an overloading"
1318 else do
1319 lchar '='
1320 t <- pExpr syn
1321 return (o, t)
1322 where overloadable = ["let","lambda","index_first","index_next","variable"]
1324--------- Pattern match clauses ---------
1326pPattern :: SyntaxInfo -> IParser PDecl
1327pPattern syn = do fc <- pfc
1328 clause <- pClause syn
1329 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
1331pCAF :: SyntaxInfo -> IParser PDecl
1332pCAF syn = do reserved "let"
1333 n_in <- pfName; let n = expandNS syn n_in
1334 lchar '='
1335 t <- pExpr syn
1336 pTerminator
1337 fc <- pfc
1338 return (PCAF fc n t)
1340pArgExpr syn = let syn' = syn { inPattern = True } in
1341 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
1343pRHS :: SyntaxInfo -> Name -> IParser PTerm
1344pRHS syn n = do lchar '='; pExpr syn
1345 <|> do symbol "?="; rhs <- pExpr syn;
1346 return (addLet rhs)
1347 <|> do reserved "impossible"; return PImpossible
1348 where mkN (UN x) = UN (x++"_lemma_1")
1349 mkN (NS x n) = NS (mkN x) n
1350 n' = mkN n
1352 addLet (PLet n ty val rhs) = PLet n ty val (addLet rhs)
1353 addLet (PCase fc t cs) = PCase fc t (map addLetC cs)
1354 where addLetC (l, r) = (l, addLet r)
1355 addLet rhs = (PLet (UN "value") Placeholder rhs (PMetavar n'))
1357pClause :: SyntaxInfo -> IParser PClause
1358pClause syn
1359 = try (do pushIndent
1360 n_in <- pfName; let n = expandNS syn n_in
1361 cargs <- many (pConstraintArg syn)
1362 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1363 fc <- pfc
1364 args <- many (pArgExpr syn)
1365 wargs <- many (pWExpr syn)
1366 rhs <- pRHS syn n
1367 ist <- getState
1368 let ctxt = tt_ctxt ist
1369 let wsyn = syn { syn_namespace = [] }
1370 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1371 popIndent
1372 return x,
1373 do pTerminator
1374 return ([], [])]
1375 let capp = PApp fc (PRef fc n)
1376 (iargs ++ cargs ++ map pexp args)
1377 ist <- getState
1378 setState (ist { lastParse = Just n })
1379 return $ PClause fc n capp wargs rhs wheres)
1380 <|> try (do pushIndent
1381 wargs <- many1 (pWExpr syn)
1382 ist <- getState
1383 n <- case lastParse ist of
1384 Just t -> return t
1385 Nothing -> fail "Invalid clause"
1386 fc <- pfc
1387 rhs <- pRHS syn n
1388 let ctxt = tt_ctxt ist
1389 let wsyn = syn { syn_namespace = [] }
1390 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1391 popIndent
1392 return x,
1393 do pTerminator
1394 return ([], [])]
1395 return $ PClauseR fc wargs rhs wheres)
1397 <|> try (do pushIndent
1398 n_in <- pfName; let n = expandNS syn n_in
1399 cargs <- many (pConstraintArg syn)
1400 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1401 fc <- pfc
1402 args <- many (pArgExpr syn)
1403 wargs <- many (pWExpr syn)
1404 let capp = PApp fc (PRef fc n)
1405 (iargs ++ cargs ++ map pexp args)
1406 ist <- getState
1407 setState (ist { lastParse = Just n })
1408 reserved "with"
1409 wval <- pSimpleExpr syn
1410 openBlock
1411 ds <- many1 $ pFunDecl syn
1412 let withs = map (fillLHSD n capp wargs) $ concat ds
1413 closeBlock
1414 popIndent
1415 return $ PWith fc n capp wargs wval withs)
1417 <|> try (do wargs <- many1 (pWExpr syn)
1418 fc <- pfc
1419 reserved "with"
1420 wval <- pSimpleExpr syn
1421 openBlock
1422 ds <- many1 $ pFunDecl syn
1423 let withs = concat ds
1424 closeBlock
1425 return $ PWithR fc wargs wval withs)
1427 <|> do pushIndent
1428 l <- pArgExpr syn
1429 op <- operator
1430 let n = expandNS syn (UN op)
1431 r <- pArgExpr syn
1432 fc <- pfc
1433 wargs <- many (pWExpr syn)
1434 rhs <- pRHS syn n
1435 let wsyn = syn { syn_namespace = [] }
1436 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1437 popIndent
1438 return x,
1439 do pTerminator
1440 return ([], [])]
1441 ist <- getState
1442 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1443 setState (ist { lastParse = Just n })
1444 return $ PClause fc n capp wargs rhs wheres
1446 <|> do l <- pArgExpr syn
1447 op <- operator
1448 let n = expandNS syn (UN op)
1449 r <- pArgExpr syn
1450 fc <- pfc
1451 wargs <- many (pWExpr syn)
1452 reserved "with"
1453 wval <- pSimpleExpr syn
1454 openBlock
1455 ds <- many1 $ pFunDecl syn
1456 closeBlock
1457 ist <- getState
1458 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1459 let withs = map (fillLHSD n capp wargs) $ concat ds
1460 setState (ist { lastParse = Just n })
1461 return $ PWith fc n capp wargs wval withs
1462 where
1463 fillLHS n capp owargs (PClauseR fc wargs v ws)
1464 = PClause fc n capp (owargs ++ wargs) v ws
1465 fillLHS n capp owargs (PWithR fc wargs v ws)
1466 = PWith fc n capp (owargs ++ wargs) v
1467 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1468 fillLHS _ _ _ c = c
1470 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1471 fillLHSD n c a x = x
1473pWExpr :: SyntaxInfo -> IParser PTerm
1474pWExpr syn = do lchar '|'
1475 pExpr' syn
1477pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
1478pWhereblock n syn
1479 = do reserved "where"; openBlock
1480 ds <- many1 $ pDecl syn
1481 let dns = concatMap (concatMap declared) ds
1482 closeBlock
1483 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1485pDirective :: SyntaxInfo -> IParser [PDecl]
1486pDirective syn = try (do lchar '%'; reserved "lib"; lib <- strlit;
1487 return [PDirective (do addLib lib
1488 addIBC (IBCLib lib))])
1489 <|> try (do lchar '%'; reserved "link"; obj <- strlit;
1490 return [PDirective (do datadir <- liftIO getDataDir
1491 o <- liftIO $ findInPath [".", datadir] obj
1492 addIBC (IBCObj o)
1493 addObjectFile o)])
1494 <|> try (do lchar '%'; reserved "include"; hdr <- strlit;
1495 return [PDirective (do addHdr hdr
1496 addIBC (IBCHeader hdr))])
1497 <|> try (do lchar '%'; reserved "hide"; n <- iName []
1498 return [PDirective (do setAccessibility n Hidden
1499 addIBC (IBCAccess n Hidden))])
1500 <|> try (do lchar '%'; reserved "freeze"; n <- iName []
1501 return [PDirective (do setAccessibility n Frozen
1502 addIBC (IBCAccess n Frozen))])
1503 <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'
1504 return [PDirective (do i <- getIState
1505 putIState (i { default_access = acc }))])
1506 <|> try (do lchar '%'; reserved "default"; tot <- pTotality
1507 i <- getState
1508 setState (i { default_total = tot } )
1509 return [PDirective (do i <- getIState
1510 putIState (i { default_total = tot }))])
1511 <|> try (do lchar '%'; reserved "logging"; i <- natural;
1512 return [PDirective (setLogLevel (fromInteger i))])
1513 <|> try (do lchar '%'; reserved "dynamic"; lib <- strlit;
1514 return [PDirective (do addIBC (IBCDyLib lib)
1515 addDyLib lib)])
1516 <|> try (do lchar '%'; reserved "language"; ext <- reserved "TypeProviders";
1517 return [PDirective (addLangExt TypeProviders)])
1519pProvider :: SyntaxInfo -> IParser [PDecl]
1520pProvider syn = do lchar '%'; reserved "provide";
1521 lchar '('; n <- pfName; t <- pTSig syn; lchar ')'
1522 fc <- pfc
1523 reserved "with"
1524 e <- pExpr syn
1525 return [PProvider syn fc n t e]
1527pTactic :: SyntaxInfo -> IParser PTactic
1528pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
1529 return $ Intro ns
1530 <|> do reserved "intros"; return Intros
1531 <|> try (do reserved "refine"; n <- pName
1532 imps <- many1 imp
1533 return $ Refine n imps)
1534 <|> do reserved "refine"; n <- pName
1535 i <- getState
1536 return $ Refine n []
1537 <|> do reserved "rewrite"; t <- pExpr syn;
1538 i <- getState
1539 return $ Rewrite (desugar syn i t)
1540 <|> try (do reserved "let"; n <- pName; lchar ':';
1541 ty <- pExpr' syn; lchar '='; t <- pExpr syn;
1542 i <- getState
1543 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
1544 <|> try (do reserved "let"; n <- pName; lchar '=';
1545 t <- pExpr syn;
1546 i <- getState
1547 return $ LetTac n (desugar syn i t))
1548 <|> do reserved "focus"; n <- pName
1549 return $ Focus n
1550 <|> do reserved "exact"; t <- pExpr syn;
1551 i <- getState
1552 return $ Exact (desugar syn i t)
1553 <|> do reserved "applyTactic"; t <- pExpr syn;
1554 i <- getState
1555 return $ ApplyTactic (desugar syn i t)
1556 <|> do reserved "reflect"; t <- pExpr syn;
1557 i <- getState
1558 return $ Reflect (desugar syn i t)
1559 <|> do reserved "fill"; t <- pExpr syn;
1560 i <- getState
1561 return $ Fill (desugar syn i t)
1562 <|> do reserved "try"; t <- pTactic syn;
1563 lchar '|';
1564 t1 <- pTactic syn
1565 return $ Try t t1
1566 <|> do lchar '{'
1567 t <- pTactic syn;
1568 lchar ';';
1569 t1 <- pTactic syn;
1570 lchar '}'
1571 return $ TSeq t t1
1572 <|> do reserved "compute"; return Compute
1573 <|> do reserved "trivial"; return Trivial
1574 <|> do reserved "solve"; return Solve
1575 <|> do reserved "attack"; return Attack
1576 <|> do reserved "state"; return ProofState
1577 <|> do reserved "term"; return ProofTerm
1578 <|> do reserved "undo"; return Undo
1579 <|> do reserved "qed"; return Qed
1580 <|> do reserved "abandon"; return Abandon
1581 <|> do lchar ':'; reserved "q"; return Abandon
1582 where
1583 imp = do lchar '?'; return False
1584 <|> do lchar '_'; return True