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