git.iko.soy/Idris-dev
on ff0fbfa help sign in
Idris-dev/src/Idris/Parser.hs
1566 lines 62 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 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)
803modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
804modifyConst syn fc (PConstant (I x))
805 | not (inPattern syn)
806 = PAlternative False
807 [PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I x))],
808 PConstant (I x), PConstant (BI (toEnum x))]
809 | otherwise = PAlternative False
810 [PConstant (I x), PConstant (BI (toEnum x))]
811modifyConst syn fc x = x
813pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']'
814 return (mkList fc xs)
815 where
816 mkList fc [] = PRef fc (UN "Nil")
817 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
819pPair syn = try (do l <- pExpr syn
820 fc <- pfc
821 rest <- restTuple
822 case rest of
823 [] -> return l
824 [Left r] -> return (PPair fc l r)
825 [Right r] -> return (PDPair fc l Placeholder r))
826 <|> try (do x <- ntuple
827 lchar ')'
828 return x)
829 <|> do ln <- pName; lchar ':'
830 lty <- pExpr syn
831 reservedOp "**"
832 fc <- pfc
833 r <- pExpr syn
834 lchar ')'
835 return (PDPair fc (PRef fc ln) lty r)
836 where
837 restTuple = do lchar ')'; return []
838 <|> do lchar ','
839 r <- pExpr syn
840 lchar ')'
841 return [Left r]
842 <|> do reservedOp "**"
843 r <- pExpr syn
844 lchar ')'
845 return [Right r]
846 ntuple = try (do l <- pExpr syn; fc <- pfc; lchar ','
847 rest <- ntuple
848 return (PPair fc l rest))
849 <|> (do l <- pExpr syn; fc <- pfc; lchar ','
850 r <- pExpr syn
851 return (PPair fc l r))
853pAlt syn = do symbol "(|"; alts <- sepBy1 (pExpr' syn) (lchar ','); symbol "|)"
854 return (PAlternative False alts)
856pHSimpleExpr syn
857 = do lchar '.'
858 e <- pSimpleExpr syn
859 return $ PHidden e
860 <|> pSimpleExpr syn
862pApp syn = do f <- pSimpleExpr syn
863 fc <- pfc
864 args <- many1 (do notEndApp
865 pArg syn)
866 i <- getState
867 return (dslify i $ PApp fc f args)
868 where
869 dslify i (PApp fc (PRef _ f) [a])
870 | [d] <- lookupCtxt Nothing f (idris_dsls i)
871 = desugar (syn { dsl_info = d }) i (getTm a)
872 dslify i t = t
874pArg :: SyntaxInfo -> IParser PArg
875pArg syn = try (pImplicitArg syn)
876 <|> try (pConstraintArg syn)
877 <|> do e <- pSimpleExpr syn
878 return (pexp e)
880pImplicitArg syn = do lchar '{'
881 n <- pName
882 fc <- pfc
883 v <- option (PRef fc n) (do lchar '='
884 pExpr syn)
885 lchar '}'
886 return (pimp n v)
888pConstraintArg syn = do symbol "@{"
889 e <- pExpr syn
890 symbol "}"
891 return (pconst e)
893pRecordType syn
894 = do reserved "record"
895 lchar '{'
896 fields <- sepBy1 pFieldType (lchar ',')
897 lchar '}'
898 fc <- pfc
899 rec <- option Nothing (do e <- pSimpleExpr syn
900 return (Just e))
901 case rec of
902 Nothing ->
903 return (PLam (MN 0 "fldx") Placeholder
904 (applyAll fc fields (PRef fc (MN 0 "fldx"))))
905 Just v -> return (applyAll fc fields v)
906 where pFieldType = do n <- pfName
907 lchar '='
908 e <- pExpr syn
909 return (n, e)
910 applyAll fc [] x = x
911 applyAll fc ((n, e) : es) x
912 = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])
914mkType (UN n) = UN ("set_" ++ n)
915mkType (MN 0 n) = MN 0 ("set_" ++ n)
916mkType (NS n s) = NS (mkType n) s
918noImp syn = syn { implicitAllowed = False }
919impOK syn = syn { implicitAllowed = True }
921pTSig syn = do lchar ':'; pTExpr syn
923pTExpr syn = do cs <- if implicitAllowed syn then pConstList syn else return []
924 sc <- pExpr syn
925 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
927pLambda syn = do lchar '\\'
928 try (do xt <- tyOptDeclList syn
929 symbol "=>"
930 sc <- pExpr syn
931 return (bindList PLam xt sc)
932 <|> (do ps <- sepBy (do fc <- pfc
933 e <- pSimpleExpr syn
934 return (fc, e)) (lchar ',')
935 symbol "=>"
936 sc <- pExpr syn
937 return (pmList (zip [0..] ps) sc)))
938 where pmList [] sc = sc
939 pmList ((i, (fc, x)) : xs) sc
940 = PLam (MN i "lamp") Placeholder
941 (PCase fc (PRef fc (MN i "lamp"))
942 [(x, pmList xs sc)])
944pRewriteTerm syn =
945 do reserved "rewrite"
946 fc <- pfc
947 prf <- pExpr syn
948 reserved "in"; sc <- pExpr syn
949 return (PRewrite fc
950 (PApp fc (PRef fc (UN "sym")) [pexp prf]) sc)
952pLet syn = try (do reserved "let"; n <- pName;
953 ty <- option Placeholder (do lchar ':'; pExpr' syn)
954 lchar '='
955 v <- pExpr syn
956 reserved "in"; sc <- pExpr syn
957 return (PLet n ty v sc))
958 <|> (do reserved "let"; fc <- pfc; pat <- pExpr' (syn { inPattern = True } )
959 symbol "="; v <- pExpr syn
960 reserved "in"; sc <- pExpr syn
961 return (PCase fc v [(pat, sc)]))
963pPi syn =
964 try (do lazy <- option False (do lchar '|'; return True)
965 st <- pStatic
966 lchar '('; xt <- tyDeclList syn; lchar ')'
967 doc <- option "" (pDocComment '^')
968 symbol "->"
969 sc <- pExpr syn
970 return (bindList (PPi (Exp lazy st doc)) xt sc))
971 <|> try (if implicitAllowed syn
972 then do lazy <- option False (do lchar '|'
973 return True)
974 st <- pStatic
975 lchar '{'
976 xt <- tyDeclList syn
977 lchar '}'
978 symbol "->"
979 sc <- pExpr syn
980 return (bindList (PPi (Imp lazy st "")) xt sc)
981 else fail "No implicit arguments allowed here")
982 <|> try (do lchar '{'
983 reserved "auto"
984 xt <- tyDeclList syn
985 lchar '}'
986 symbol "->"
987 sc <- pExpr syn
988 return (bindList (PPi
989 (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))
990 <|> try (do lchar '{'
991 reserved "default"
992 script <- pSimpleExpr syn
993 xt <- tyDeclList syn
994 lchar '}'
995 symbol "->"
996 sc <- pExpr syn
997 return (bindList (PPi (TacImp False Dynamic script "")) xt sc))
998 <|> do --lazy <- option False (do lchar '|'; return True)
999 lchar '{'
1000 reserved "static"
1001 lchar '}'
1002 t <- pExpr' syn
1003 symbol "->"
1004 sc <- pExpr syn
1005 return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)
1007pConstList :: SyntaxInfo -> IParser [PTerm]
1008pConstList syn = try (do lchar '('
1009 tys <- sepBy1 (pExpr' (noImp syn)) (lchar ',')
1010 lchar ')'
1011 reservedOp "=>"
1012 return tys)
1013 <|> try (do t <- pExpr (noImp syn)
1014 reservedOp "=>"
1015 return [t])
1016 <|> return []
1018tyDeclList syn = try (sepBy1 (do x <- pfName
1019 t <- pTSig (noImp syn)
1020 return (x,t))
1021 (lchar ','))
1022 <|> do ns <- sepBy1 pName (lchar ',')
1023 t <- pTSig (noImp syn)
1024 return (map (\x -> (x, t)) ns)
1026tyOptDeclList syn = sepBy1 (do x <- pfName;
1027 t <- option Placeholder (do lchar ':'
1028 pExpr syn)
1029 return (x,t))
1030 (lchar ',')
1032bindList b [] sc = sc
1033bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
1035pComprehension syn
1036 = do lchar '['
1037 fc <- pfc
1038 pat <- pExpr syn
1039 lchar '|'
1040 qs <- sepBy1 (pDo syn) (lchar ',')
1041 lchar ']'
1042 return (PDoBlock (map addGuard qs ++
1043 [DoExp fc (PApp fc (PRef fc (UN "return"))
1044 [pexp pat])]))
1045 where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
1046 [pexp e])
1047 addGuard x = x
1049pDoBlock syn
1050 = do reserved "do"
1051 openBlock
1052 pushIndent
1053 ds <- many1 (do notEndBlock
1054 x <- pDo syn
1055 pKeepTerminator
1056 return x)
1057 popIndent
1058 closeBlock
1059 return (PDoBlock ds)
1061pDo syn
1062 = try (do reserved "let"
1063 i <- pName;
1064 ty <- option Placeholder (do lchar ':'
1065 pExpr' syn)
1066 reservedOp "="
1067 fc <- pfc
1068 e <- pExpr syn
1069 return (DoLet fc i ty e))
1070 <|> try (do reserved "let"
1071 i <- pExpr' syn
1072 reservedOp "="
1073 fc <- pfc
1074 sc <- pExpr syn
1075 return (DoLetP fc i sc))
1076 <|> try (do i <- pName
1077 symbol "<-"
1078 fc <- pfc
1079 e <- pExpr syn;
1080 return (DoBind fc i e))
1081 <|> try (do i <- pExpr' syn
1082 symbol "<-"
1083 fc <- pfc
1084 e <- pExpr syn;
1085 return (DoBindP fc i e))
1086 <|> try (do e <- pExpr syn
1087 fc <- pfc
1088 return (DoExp fc e))
1090pIdiom syn
1091 = do symbol "[|"
1092 fc <- pfc
1093 e <- pExpr syn
1094 symbol "|]"
1095 return (PIdiom fc e)
1097pConstant :: IParser Const
1098pConstant = do reserved "Integer";return BIType
1099 <|> do reserved "Int"; return IType
1100 <|> do reserved "Char"; return ChType
1101 <|> do reserved "Float"; return FlType
1102 <|> do reserved "String"; return StrType
1103 <|> do reserved "Ptr"; return PtrType
1104 <|> do reserved "Bits8"; return B8Type
1105 <|> do reserved "Bits16"; return B16Type
1106 <|> do reserved "Bits32"; return B32Type
1107 <|> do reserved "Bits64"; return B64Type
1108 <|> try (do f <- float; return $ Fl f)
1109-- <|> try (do i <- natural; lchar 'L'; return $ BI i)
1110 <|> try (do i <- natural; return $ I (fromInteger i))
1111 <|> try (do s <- strlit; return $ Str s)
1112 <|> try (do c <- chlit; return $ Ch c)
1114pStatic :: IParser Static
1115pStatic = do lchar '['
1116 reserved "static"
1117 lchar ']';
1118 return Static
1119 <|> return Dynamic
1121table fixes
1122 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
1123 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]
1124 ++ toTable (reverse fixes) ++
1125 [[backtick],
1126 [binary "=" PEq AssocLeft],
1127 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
1129toTable fs = map (map toBin)
1130 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
1131 where toBin (Fix (PrefixN _) op) = prefix op
1132 (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
1133 toBin (Fix f op)
1134 = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
1135 assoc (Infixl _) = AssocLeft
1136 assoc (Infixr _) = AssocRight
1137 assoc (InfixN _) = AssocNone
1139binary name f = Infix (do fc <- pfc
1140 reservedOp name
1141 doc <- option "" (pDocComment '^')
1142 return (f fc))
1143prefix name f = Prefix (do reservedOp name
1144 fc <- pfc;
1145 return (f fc))
1146backtick = Infix (do lchar '`'; n <- pfName
1147 lchar '`'
1148 fc <- pfc
1149 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
1151--------- Data declarations ---------
1153-- (works for classes too - 'abstract' means the data/class is visible but members not)
1154accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()
1155accData (Just Frozen) n ns = do addAcc n (Just Frozen)
1156 mapM_ (\n -> addAcc n (Just Hidden)) ns
1157accData a n ns = do addAcc n a
1158 mapM_ (`addAcc` a) ns
1160pRecord :: SyntaxInfo -> IParser PDecl
1161pRecord syn = do doc <- option "" (pDocComment '|')
1162 acc <- pAccessibility
1163 reserved "record"
1164 fc <- pfc
1165 tyn_in <- pfName
1166 ty <- pTSig (impOK syn)
1167 let tyn = expandNS syn tyn_in
1168 reserved "where"
1169 openBlock
1170 pushIndent
1171 (cdoc, cn, cty, _) <- pConstructor syn
1172 pKeepTerminator
1173 popIndent
1174 closeBlock
1175 accData acc tyn [cn]
1176 let rsyn = syn { syn_namespace = show (nsroot tyn) :
1177 syn_namespace syn }
1178 let fns = getRecNames rsyn cty
1179 mapM_ (\n -> addAcc n acc) fns
1180 return $ PRecord doc rsyn fc tyn ty cdoc cn cty
1181 where
1182 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
1183 ++ getRecNames syn sc
1184 getRecNames _ _ = []
1186 toFreeze (Just Frozen) = Just Hidden
1187 toFreeze x = x
1189pDataI = do reserved "data"; return False
1190 <|> do reserved "codata"; return True
1192pData :: SyntaxInfo -> IParser PDecl
1193pData syn = try (do doc <- option "" (pDocComment '|')
1194 acc <- pAccessibility
1195 co <- pDataI
1196 fc <- pfc
1197 tyn_in <- pfName
1198 ty <- pTSig (impOK syn)
1199 let tyn = expandNS syn tyn_in
1200 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1201 reserved "where"
1202 openBlock
1203 pushIndent
1204 cons <- many (do notEndBlock
1205 c <- pConstructor syn
1206 pKeepTerminator
1207 return c) -- (lchar '|')
1208 popIndent
1209 closeBlock
1210 accData acc tyn (map (\ (_, n, _, _) -> n) cons)
1211 return $ PData doc syn fc co (PDatadecl tyn ty cons)))
1212 <|> try (do doc <- option "" (pDocComment '|')
1213 pushIndent
1214 acc <- pAccessibility
1215 co <- pDataI
1216 fc <- pfc
1217 tyn_in <- pfName
1218 args <- many pName
1219 let ty = bindArgs (map (const PType) args) PType
1220 let tyn = expandNS syn tyn_in
1221 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1222 try (lchar '=') <|> do reserved "where"
1223 let kw = (if co then "co" else "") ++ "data "
1224 let n = show tyn_in ++ " "
1225 let s = kw ++ n
1226 let as = concat (intersperse " " $ map show args) ++ " "
1227 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
1228 let ss = concat (intersperse " -> " $ map (const "Type") args)
1229 let fix1 = s ++ as ++ " = ..."
1230 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
1231 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
1232 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
1234 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
1235 pTerminator
1236 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
1237 cons' <- mapM (\ (doc, x, cargs, cfc) ->
1238 do let cty = bindArgs cargs conty
1239 return (doc, x, cty, cfc)) cons
1240 accData acc tyn (map (\ (_, n, _, _) -> n) cons')
1241 return $ PData doc syn fc co (PDatadecl tyn ty cons')))
1242 where
1243 mkPApp fc t [] = t
1244 mkPApp fc t xs = PApp fc t (map pexp xs)
1246bindArgs :: [PTerm] -> PTerm -> PTerm
1247bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
1249pConstructor :: SyntaxInfo -> IParser (String, Name, PTerm, FC)
1250pConstructor syn
1251 = do doc <- option "" (pDocComment '|')
1252 cn_in <- pfName; fc <- pfc
1253 let cn = expandNS syn cn_in
1254 ty <- pTSig (impOK syn)
1255-- ty' <- implicit syn cn ty
1256 return (doc, cn, ty, fc)
1259pSimpleCon :: SyntaxInfo -> IParser (String, Name, [PTerm], FC)
1260pSimpleCon syn
1261 = do cn_in <- pfName
1262 let cn = expandNS syn cn_in
1263 fc <- pfc
1264 args <- many (do notEndApp
1265 pSimpleExpr syn)
1266 doc <- option "" (pDocComment '^')
1267 return (doc, cn, args, fc)
1269--------- DSL syntax overloading ---------
1271pDSL :: SyntaxInfo -> IParser PDecl
1272pDSL syn = do reserved "dsl"
1273 n <- pfName
1274 openBlock
1275 pushIndent
1276 bs <- many1 (do notEndBlock
1277 b <- pOverload syn
1278 pKeepTerminator
1279 return b)
1280 popIndent; closeBlock
1281 let dsl = mkDSL bs (dsl_info syn)
1282 checkDSL dsl
1283 i <- getState
1284 setState (i { idris_dsls = addDef n dsl (idris_dsls i) })
1285 return (PDSL n dsl)
1286 where mkDSL bs dsl = let var = lookup "variable" bs
1287 first = lookup "index_first" bs
1288 next = lookup "index_next" bs
1289 leto = lookup "let" bs
1290 lambda = lookup "lambda" bs in
1291 initDSL { dsl_var = var,
1292 index_first = first,
1293 index_next = next,
1294 dsl_lambda = lambda,
1295 dsl_let = leto }
1297checkDSL :: DSL -> IParser ()
1298checkDSL dsl = return ()
1300pOverload :: SyntaxInfo -> IParser (String, PTerm)
1301pOverload syn = do o <- identifier <|> do reserved "let"
1302 return "let"
1303 if o `notElem` overloadable
1304 then fail $ show o ++ " is not an overloading"
1305 else do
1306 lchar '='
1307 t <- pExpr syn
1308 return (o, t)
1309 where overloadable = ["let","lambda","index_first","index_next","variable"]
1311--------- Pattern match clauses ---------
1313pPattern :: SyntaxInfo -> IParser PDecl
1314pPattern syn = do fc <- pfc
1315 clause <- pClause syn
1316 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
1318pCAF :: SyntaxInfo -> IParser PDecl
1319pCAF syn = do reserved "let"
1320 n_in <- pfName; let n = expandNS syn n_in
1321 lchar '='
1322 t <- pExpr syn
1323 pTerminator
1324 fc <- pfc
1325 return (PCAF fc n t)
1327pArgExpr syn = let syn' = syn { inPattern = True } in
1328 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
1330pRHS :: SyntaxInfo -> Name -> IParser PTerm
1331pRHS syn n = do lchar '='; pExpr syn
1332 <|> do symbol "?="; rhs <- pExpr syn;
1333 return (addLet rhs)
1334 <|> do reserved "impossible"; return PImpossible
1335 where mkN (UN x) = UN (x++"_lemma_1")
1336 mkN (NS x n) = NS (mkN x) n
1337 n' = mkN n
1339 addLet (PLet n ty val rhs) = PLet n ty val (addLet rhs)
1340 addLet (PCase fc t cs) = PCase fc t (map addLetC cs)
1341 where addLetC (l, r) = (l, addLet r)
1342 addLet rhs = (PLet (UN "value") Placeholder rhs (PMetavar n'))
1344pClause :: SyntaxInfo -> IParser PClause
1345pClause syn
1346 = try (do pushIndent
1347 n_in <- pfName; let n = expandNS syn n_in
1348 cargs <- many (pConstraintArg syn)
1349 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1350 fc <- pfc
1351 args <- many (pArgExpr syn)
1352 wargs <- many (pWExpr syn)
1353 rhs <- pRHS syn n
1354 ist <- getState
1355 let ctxt = tt_ctxt ist
1356 let wsyn = syn { syn_namespace = [] }
1357 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1358 popIndent
1359 return x,
1360 do pTerminator
1361 return ([], [])]
1362 let capp = PApp fc (PRef fc n)
1363 (iargs ++ cargs ++ map pexp args)
1364 ist <- getState
1365 setState (ist { lastParse = Just n })
1366 return $ PClause fc n capp wargs rhs wheres)
1367 <|> try (do pushIndent
1368 wargs <- many1 (pWExpr syn)
1369 ist <- getState
1370 n <- case lastParse ist of
1371 Just t -> return t
1372 Nothing -> fail "Invalid clause"
1373 fc <- pfc
1374 rhs <- pRHS syn n
1375 let ctxt = tt_ctxt ist
1376 let wsyn = syn { syn_namespace = [] }
1377 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1378 popIndent
1379 return x,
1380 do pTerminator
1381 return ([], [])]
1382 return $ PClauseR fc wargs rhs wheres)
1384 <|> try (do pushIndent
1385 n_in <- pfName; let n = expandNS syn n_in
1386 cargs <- many (pConstraintArg syn)
1387 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1388 fc <- pfc
1389 args <- many (pArgExpr syn)
1390 wargs <- many (pWExpr syn)
1391 let capp = PApp fc (PRef fc n)
1392 (iargs ++ cargs ++ map pexp args)
1393 ist <- getState
1394 setState (ist { lastParse = Just n })
1395 reserved "with"
1396 wval <- pSimpleExpr syn
1397 openBlock
1398 ds <- many1 $ pFunDecl syn
1399 let withs = map (fillLHSD n capp wargs) $ concat ds
1400 closeBlock
1401 popIndent
1402 return $ PWith fc n capp wargs wval withs)
1404 <|> try (do wargs <- many1 (pWExpr syn)
1405 fc <- pfc
1406 reserved "with"
1407 wval <- pSimpleExpr syn
1408 openBlock
1409 ds <- many1 $ pFunDecl syn
1410 let withs = concat ds
1411 closeBlock
1412 return $ PWithR fc wargs wval withs)
1414 <|> do pushIndent
1415 l <- pArgExpr syn
1416 op <- operator
1417 let n = expandNS syn (UN op)
1418 r <- pArgExpr syn
1419 fc <- pfc
1420 wargs <- many (pWExpr syn)
1421 rhs <- pRHS syn n
1422 let wsyn = syn { syn_namespace = [] }
1423 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1424 popIndent
1425 return x,
1426 do pTerminator
1427 return ([], [])]
1428 ist <- getState
1429 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1430 setState (ist { lastParse = Just n })
1431 return $ PClause fc n capp wargs rhs wheres
1433 <|> do l <- pArgExpr syn
1434 op <- operator
1435 let n = expandNS syn (UN op)
1436 r <- pArgExpr syn
1437 fc <- pfc
1438 wargs <- many (pWExpr syn)
1439 reserved "with"
1440 wval <- pSimpleExpr syn
1441 openBlock
1442 ds <- many1 $ pFunDecl syn
1443 closeBlock
1444 ist <- getState
1445 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1446 let withs = map (fillLHSD n capp wargs) $ concat ds
1447 setState (ist { lastParse = Just n })
1448 return $ PWith fc n capp wargs wval withs
1449 where
1450 fillLHS n capp owargs (PClauseR fc wargs v ws)
1451 = PClause fc n capp (owargs ++ wargs) v ws
1452 fillLHS n capp owargs (PWithR fc wargs v ws)
1453 = PWith fc n capp (owargs ++ wargs) v
1454 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1455 fillLHS _ _ _ c = c
1457 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1458 fillLHSD n c a x = x
1460pWExpr :: SyntaxInfo -> IParser PTerm
1461pWExpr syn = do lchar '|'
1462 pExpr' syn
1464pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
1465pWhereblock n syn
1466 = do reserved "where"; openBlock
1467 ds <- many1 $ pDecl syn
1468 let dns = concatMap (concatMap declared) ds
1469 closeBlock
1470 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1472pDirective :: SyntaxInfo -> IParser [PDecl]
1473pDirective syn = try (do lchar '%'; reserved "lib"; lib <- strlit;
1474 return [PDirective (do addLib lib
1475 addIBC (IBCLib lib))])
1476 <|> try (do lchar '%'; reserved "link"; obj <- strlit;
1477 return [PDirective (do datadir <- liftIO getDataDir
1478 o <- liftIO $ findInPath [".", datadir] obj
1479 addIBC (IBCObj o)
1480 addObjectFile o)])
1481 <|> try (do lchar '%'; reserved "include"; hdr <- strlit;
1482 return [PDirective (do addHdr hdr
1483 addIBC (IBCHeader hdr))])
1484 <|> try (do lchar '%'; reserved "hide"; n <- iName []
1485 return [PDirective (do setAccessibility n Hidden
1486 addIBC (IBCAccess n Hidden))])
1487 <|> try (do lchar '%'; reserved "freeze"; n <- iName []
1488 return [PDirective (do setAccessibility n Frozen
1489 addIBC (IBCAccess n Frozen))])
1490 <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'
1491 return [PDirective (do i <- getIState
1492 putIState (i { default_access = acc }))])
1493 <|> try (do lchar '%'; reserved "default"; tot <- pTotality
1494 i <- getState
1495 setState (i { default_total = tot } )
1496 return [PDirective (do i <- getIState
1497 putIState (i { default_total = tot }))])
1498 <|> try (do lchar '%'; reserved "logging"; i <- natural;
1499 return [PDirective (setLogLevel (fromInteger i))])
1500 <|> try (do lchar '%'; reserved "dynamic"; lib <- strlit;
1501 return [PDirective (do addIBC (IBCDyLib lib)
1502 addDyLib lib)])
1503 <|> try (do lchar '%'; reserved "language"; ext <- reserved "TypeProviders";
1504 return [PDirective (addLangExt TypeProviders)])
1506pProvider :: SyntaxInfo -> IParser [PDecl]
1507pProvider syn = do lchar '%'; reserved "provide";
1508 lchar '('; n <- pfName; t <- pTSig syn; lchar ')'
1509 fc <- pfc
1510 reserved "with"
1511 e <- pExpr syn
1512 return [PProvider syn fc n t e]
1514pTactic :: SyntaxInfo -> IParser PTactic
1515pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
1516 return $ Intro ns
1517 <|> do reserved "intros"; return Intros
1518 <|> try (do reserved "refine"; n <- pName
1519 imps <- many1 imp
1520 return $ Refine n imps)
1521 <|> do reserved "refine"; n <- pName
1522 i <- getState
1523 return $ Refine n []
1524 <|> do reserved "rewrite"; t <- pExpr syn;
1525 i <- getState
1526 return $ Rewrite (desugar syn i t)
1527 <|> try (do reserved "let"; n <- pName; lchar ':';
1528 ty <- pExpr' syn; lchar '='; t <- pExpr syn;
1529 i <- getState
1530 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
1531 <|> try (do reserved "let"; n <- pName; lchar '=';
1532 t <- pExpr syn;
1533 i <- getState
1534 return $ LetTac n (desugar syn i t))
1535 <|> do reserved "focus"; n <- pName
1536 return $ Focus n
1537 <|> do reserved "exact"; t <- pExpr syn;
1538 i <- getState
1539 return $ Exact (desugar syn i t)
1540 <|> do reserved "reflect"; t <- pExpr syn;
1541 i <- getState
1542 return $ ReflectTac (desugar syn i t)
1543 <|> do reserved "try"; t <- pTactic syn;
1544 lchar '|';
1545 t1 <- pTactic syn
1546 return $ Try t t1
1547 <|> do lchar '{'
1548 t <- pTactic syn;
1549 lchar ';';
1550 t1 <- pTactic syn;
1551 lchar '}'
1552 return $ TSeq t t1
1553 <|> do reserved "compute"; return Compute
1554 <|> do reserved "trivial"; return Trivial
1555 <|> do reserved "solve"; return Solve
1556 <|> do reserved "attack"; return Attack
1557 <|> do reserved "state"; return ProofState
1558 <|> do reserved "term"; return ProofTerm
1559 <|> do reserved "undo"; return Undo
1560 <|> do reserved "qed"; return Qed
1561 <|> do reserved "abandon"; return Abandon
1562 <|> do lchar ':'; reserved "q"; return Abandon
1563 where
1564 imp = do lchar '?'; return False
1565 <|> do lchar '_'; return True