git.iko.soy/Idris-dev
on 04abcae help sign in
Idris-dev/src/Idris/Parser.hs
1865 lines 73 kB history raw
1{-|
2Module : Idris.Parser
3Description : Idris' parser.
5License : BSD3
6Maintainer : The Idris Community.
7-}
9{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,
10 PatternGuards #-}
11{-# OPTIONS_GHC -O0 #-}
12-- FIXME: {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
13{-# OPTIONS_GHC -fwarn-unused-imports #-}
15module Idris.Parser(IdrisParser(..), ImportInfo(..), moduleName, addReplSyntax, clearParserWarnings,
16 decl, fixColour, loadFromIFile, loadModule, name, opChars, parseElabShellStep, parseConst, parseExpr, parseImports, parseTactic,
17 runparser, ParseError, parseErrorDoc) where
19import Idris.AbsSyntax hiding (namespace, params)
20import Idris.Core.Evaluate
21import Idris.Core.TT
22import Idris.Delaborate
23import Idris.Docstrings hiding (Unchecked)
24import Idris.DSL
25import Idris.Elab.Value
26import Idris.ElabDecls
27import Idris.Error
28import Idris.IBC
29import Idris.Imports
30import Idris.Options
31import Idris.Output
32import Idris.Parser.Data
33import Idris.Parser.Expr
34import Idris.Parser.Helpers
35import Idris.Parser.Ops
36import Idris.Termination
37import Idris.Unlit
39import Util.System (readSource)
41import Prelude hiding (pi)
43import Control.Applicative hiding (Const)
44import Control.Monad
45import Control.Monad.State.Strict
46import Data.Char
47import Data.Foldable (asum)
48import Data.Function
49import Data.Generics.Uniplate.Data (descendM)
50import Data.List
51import qualified Data.List.NonEmpty as NonEmpty
52import qualified Data.List.Split as Spl
53import qualified Data.Map as M
54import Data.Maybe
55import Data.Ord
56import qualified Data.Set as S
57import qualified Data.Text as T
58import qualified System.Directory as Dir (doesFileExist, getModificationTime,
59 makeAbsolute)
60import System.FilePath
61import Text.Megaparsec ((<?>))
62import qualified Text.Megaparsec as P
63import qualified Text.PrettyPrint.ANSI.Leijen as PP
65{-
67 grammar shortcut notation:
68 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)
69 RULE? = optional rule (i.e. RULE or nothing)
70 RULE* = repeated rule (i.e. RULE zero or more times)
71 RULE+ = repeated rule with at least one match (i.e. RULE one or more times)
72 RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)
73 RULE{n} = rule repeated n times
75-}
77{- * Main grammar -}
79{-| Parses module definition
82 ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;
84-}
87moduleName :: Parsing m => m Name
88moduleName = mkName [] . map T.pack <$> moduleNamePieces where
90 mkName :: [T.Text] -> [T.Text] -> Name
91 mkName ts [x] = if null ts then UN x else NS (UN x) ts
92 mkName ts (x:xs) = mkName (x : ts) xs
94moduleNamePieces :: Parsing m => m [String]
95moduleNamePieces = Spl.splitOn "." <$> identifier
97moduleHeader :: IdrisParser (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
98moduleHeader = P.try (do docs <- optional docComment
99 noArgs docs
100 keyword "module"
101 (modName, ifc) <- withExtent moduleNamePieces
102 P.option ';' (lchar ';')
103 return (fmap fst docs,
104 modName,
105 [(ifc, AnnNamespace (map T.pack modName) Nothing)]))
106 <|> P.try (do lchar '%'; reserved "unqualified"
107 return (Nothing, [], []))
108 <|> return (Nothing, ["Main"], [])
109 where noArgs (Just (_, args)) | not (null args) = fail "Modules do not take arguments"
110 noArgs _ = return ()
112data ImportInfo = ImportInfo { import_reexport :: Bool
113 , import_path :: FilePath
114 , import_rename :: Maybe (String, FC)
115 , import_namespace :: [T.Text]
116 , import_location :: FC
117 , import_modname_location :: FC
118 }
120{-| Parses an import statement
123 Import ::= 'import' Identifier_t ';'?;
125 -}
126import_ :: IdrisParser ImportInfo
127import_ = do fc <- extent $ keyword "import"
128 reexport <- P.option False (True <$ keyword "public")
129 (ns, idfc) <- withExtent moduleNamePieces
130 newName <- optional (do keyword "as"
131 withExtent identifier)
132 P.option ';' (lchar ';')
133 return $ ImportInfo reexport (toPath ns)
134 (fmap (\(n, fc) -> (toPath (Spl.splitOn "." n), fc)) newName)
135 (map T.pack ns) fc idfc
136 <?> "import statement"
137 where toPath = foldl1' (</>)
139{-| Parses program source
142 Prog ::= Decl* EOF;
144 -}
145prog :: SyntaxInfo -> IdrisParser [PDecl]
146prog syn = do (decls, fc) <- withExtent $ do
147 whiteSpace
148 decls <- concat <$> many (decl syn)
149 case maxline syn of
150 Nothing -> do notOpenBraces; P.eof
151 _ -> return ()
152 return decls
153 ist <- get
154 put ist { idris_parsedSpan = Just (FC (fc_fname fc) (0,0) (fc_end fc)),
155 ibc_write = IBCParsedRegion fc : ibc_write ist }
156 return decls
158{-| Parses a top-level declaration
161Decl ::=
162 Decl'
163 | Using
164 | Params
165 | Mutual
166 | Namespace
167 | Interface
168 | Implementation
169 | DSL
170 | Directive
171 | Provider
172 | Transform
173 | Import!
174 | RunElabDecl
175 ;
177-}
178decl :: SyntaxInfo -> IdrisParser [PDecl]
179decl syn = P.try (externalDecl syn)
180 <|> internalDecl syn
181 <?> "declaration"
183internalDecl :: SyntaxInfo -> IdrisParser [PDecl]
184internalDecl syn
185 = do fc <- getFC
186 -- if we're after maxline, stop at the next type declaration
187 -- (so we get all cases of a definition to preserve totality
188 -- results, in particular).
189 let continue = case maxline syn of
190 Nothing -> True
191 Just l -> if fst (fc_end fc) > l
192 then mut_nesting syn /= 0
193 else True
194 -- What I'd really like to do here is explicitly save the
195 -- current state, then if reading ahead finds we've passed
196 -- the end of the definition, reset the state. But I've lost
197 -- patience with trying to find out how to do that from the
198 -- trifecta docs, so this does the job instead.
199 if continue then
200 do notEndBlock
201 declBody continue
202 else P.try (do notEndBlock
203 declBody continue)
204 <|> fail "End of readable input"
205 where declBody :: Bool -> IdrisParser [PDecl]
206 declBody b =
207 P.try (implementation syn)
208 <|> P.try (openInterface syn)
209 <|> declBody' b
210 <|> using_ syn
211 <|> params syn
212 <|> mutual syn
213 <|> namespace syn
214 <|> interface_ syn
215 <|> do d <- dsl syn; return [d]
216 <|> directive syn
217 <|> provider syn
218 <|> transform syn
219 <|> do import_; fail "imports must be at top of file"
220 <?> "declaration"
221 declBody' :: Bool -> IdrisParser [PDecl]
222 declBody' cont = do d <- decl' syn
223 i <- get
224 let d' = fmap (debindApp syn . (desugar syn i)) d
225 if continue cont d'
226 then return [d']
227 else fail "End of readable input"
229 -- Keep going while we're still parsing clauses
230 continue False (PClauses _ _ _ _) = True
231 continue c _ = c
233{-| Parses a top-level declaration with possible syntax sugar
236Decl' ::=
237 Fixity
238 | FunDecl'
239 | Data
240 | Record
241 | SyntaxDecl
242 ;
244-}
245decl' :: SyntaxInfo -> IdrisParser PDecl
246decl' syn = fixity
247 <|> syntaxDecl syn
248 <|> fnDecl' syn
249 <|> data_ syn
250 <|> record syn
251 <|> runElabDecl syn
252 <?> "declaration"
254externalDecl :: SyntaxInfo -> IdrisParser [PDecl]
255externalDecl syn = do i <- get
256 notEndBlock
257 (decls, fc@(FC fn _ _)) <- withExtent $ declExtensions syn (syntaxRulesList $ syntax_rules i)
258 return $ map (mapPDeclFC (fixFC fc) (fixFCH fn fc)) decls
259 where
260 -- | Fix non-highlighting FCs to prevent spurious error location reports
261 fixFC :: FC -> FC -> FC
262 fixFC outer inner | inner `fcIn` outer = inner
263 | otherwise = outer
264 -- | Fix highlighting FCs by obliterating them, to avoid spurious highlights
265 fixFCH fn outer inner | inner `fcIn` outer = inner
266 | otherwise = FileFC fn
268declExtensions :: SyntaxInfo -> [Syntax] -> IdrisParser [PDecl]
269declExtensions syn rules = declExtension syn [] (filter isDeclRule rules)
270 <?> "user-defined declaration"
271 where
272 isDeclRule (DeclRule _ _) = True
273 isDeclRule _ = False
275declExtension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax]
276 -> IdrisParser [PDecl]
277declExtension syn ns rules =
278 P.choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->
279 case head rs of -- can never be []
280 DeclRule (symb:_) _ -> P.try $ do
281 n <- extSymbol symb
282 declExtension syn (n : ns) [DeclRule ss t | (DeclRule (_:ss) t) <- rs]
283 -- If we have more than one Rule in this bucket, our grammar is
284 -- nondeterministic.
285 DeclRule [] dec -> let r = map (update (mapMaybe id ns)) dec in
286 return r
288 where
289 update :: [(Name, SynMatch)] -> PDecl -> PDecl
290 update ns = updateNs ns . fmap (updateRefs ns) . fmap (updateSynMatch ns)
292 updateRefs ns = mapPT newref
293 where
294 newref (PRef fc fcs n) = PRef fc fcs (updateB ns n)
295 newref t = t
297 -- Below is a lot of tedious boilerplate which updates any top level
298 -- names in the declaration. It will only change names which are bound in
299 -- the declaration (including method names in interfaces and field names in
300 -- record declarations, not including pattern variables)
301 updateB :: [(Name, SynMatch)] -> Name -> Name
302 updateB ns (NS n mods) = NS (updateB ns n) mods
303 updateB ns n = case lookup n ns of
304 Just (SynBind tfc t) -> t
305 _ -> n
307 updateNs :: [(Name, SynMatch)] -> PDecl -> PDecl
308 updateNs ns (PTy doc argdoc s fc o n fc' t)
309 = PTy doc argdoc s fc o (updateB ns n) fc' t
310 updateNs ns (PClauses fc o n cs)
311 = PClauses fc o (updateB ns n) (map (updateClause ns) cs)
312 updateNs ns (PCAF fc n t) = PCAF fc (updateB ns n) t
313 updateNs ns (PData ds cds s fc o dat)
314 = PData ds cds s fc o (updateData ns dat)
315 updateNs ns (PParams fc ps ds) = PParams fc ps (map (updateNs ns) ds)
316 updateNs ns (PNamespace s fc ds) = PNamespace s fc (map (updateNs ns) ds)
317 updateNs ns (PRecord doc syn fc o n fc' ps pdocs fields cname cdoc s)
318 = PRecord doc syn fc o (updateB ns n) fc' ps pdocs
319 (map (updateField ns) fields)
320 (updateRecCon ns cname)
321 cdoc
322 s
323 updateNs ns (PInterface docs s fc cs cn fc' ps pdocs pdets ds cname cdocs)
324 = PInterface docs s fc cs (updateB ns cn) fc' ps pdocs pdets
325 (map (updateNs ns) ds)
326 (updateRecCon ns cname)
327 cdocs
328 updateNs ns (PImplementation docs pdocs s fc cs pnames acc opts cn fc' ps pextra ity ni ds)
329 = PImplementation docs pdocs s fc cs pnames acc opts (updateB ns cn) fc'
330 ps pextra ity (fmap (updateB ns) ni)
331 (map (updateNs ns) ds)
332 updateNs ns (PMutual fc ds) = PMutual fc (map (updateNs ns) ds)
333 updateNs ns (PProvider docs s fc fc' pw n)
334 = PProvider docs s fc fc' pw (updateB ns n)
335 updateNs ns d = d
337 updateRecCon ns Nothing = Nothing
338 updateRecCon ns (Just (n, fc)) = Just (updateB ns n, fc)
340 updateField ns (m, p, t, doc) = (updateRecCon ns m, p, t, doc)
342 updateClause ns (PClause fc n t ts t' ds)
343 = PClause fc (updateB ns n) t ts t' (map (update ns) ds)
344 updateClause ns (PWith fc n t ts t' m ds)
345 = PWith fc (updateB ns n) t ts t' m (map (update ns) ds)
346 updateClause ns (PClauseR fc ts t ds)
347 = PClauseR fc ts t (map (update ns) ds)
348 updateClause ns (PWithR fc ts t m ds)
349 = PWithR fc ts t m (map (update ns) ds)
351 updateData ns (PDatadecl n fc t cs)
352 = PDatadecl (updateB ns n) fc t (map (updateCon ns) cs)
353 updateData ns (PLaterdecl n fc t)
354 = PLaterdecl (updateB ns n) fc t
356 updateCon ns (cd, ads, cn, fc, ty, fc', fns)
357 = (cd, ads, updateB ns cn, fc, ty, fc', fns)
359 ruleGroup [] [] = True
360 ruleGroup (s1:_) (s2:_) = s1 == s2
361 ruleGroup _ _ = False
363 extSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
364 extSymbol (Keyword n) = Nothing <$ keyword (show n)
365 extSymbol (Expr n) = do tm <- expr syn
366 return $ Just (n, SynTm tm)
367 extSymbol (SimpleExpr n) = do tm <- simpleExpr syn
368 return $ Just (n, SynTm tm)
369 extSymbol (Binding n) = do (b, fc) <- withExtent name
370 return $ Just (n, SynBind fc b)
371 extSymbol (Symbol s) = Nothing <$ highlight AnnKeyword (symbol s)
373{-| Parses a syntax extension declaration (and adds the rule to parser state)
376 SyntaxDecl ::= SyntaxRule;
378-}
379syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
380syntaxDecl syn = do (s, fc) <- withExtent $ syntaxRule syn
381 modify $ \i -> i `addSyntax` s
382 return (PSyntax fc s)
384-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.
385addSyntax :: IState -> Syntax -> IState
386addSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
387 syntax_keywords = ks ++ ns,
388 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc }
389 where rs = syntax_rules i
390 ns = syntax_keywords i
391 ibc = ibc_write i
392 ks = map show (syntaxNames s)
394-- | Like 'addSyntax', but no effect on the IBC.
395addReplSyntax :: IState -> Syntax -> IState
396addReplSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
397 syntax_keywords = ks ++ ns }
398 where rs = syntax_rules i
399 ns = syntax_keywords i
400 ks = map show (syntaxNames s)
402{-| Parses a syntax extension declaration
405SyntaxRuleOpts ::= 'term' | 'pattern';
409SyntaxRule ::=
410 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
414SyntaxSym ::= '[' Name_t ']'
415 | '{' Name_t '}'
416 | Name_t
417 | StringLiteral_t
418 ;
420-}
421syntaxRule :: SyntaxInfo -> IdrisParser Syntax
422syntaxRule syn
423 = do sty <- P.try (do
424 pushIndent
425 sty <- P.option AnySyntax
426 (TermSyntax <$ keyword "term"
427 <|> PatternSyntax <$ keyword "pattern")
428 keyword "syntax"
429 return sty)
430 syms <- some syntaxSym
431 when (all isExpr syms) $ P.unexpected . P.Label . NonEmpty.fromList $ "missing keywords in syntax rule"
432 let ns = mapMaybe getName syms
433 when (length ns /= length (nub ns))
434 $ P.unexpected . P.Label . NonEmpty.fromList $ "repeated variable in syntax rule"
435 lchar '='
436 tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]
437 terminator
438 return (Rule (mkSimple syms) tm sty)
439 <|> do keyword "decl"; keyword "syntax"
440 syms <- some syntaxSym
441 when (all isExpr syms) $ P.unexpected . P.Label . NonEmpty.fromList $ "missing keywords in syntax rule"
442 let ns = mapMaybe getName syms
443 when (length ns /= length (nub ns))
444 $ P.unexpected . P.Label . NonEmpty.fromList $ "repeated variable in syntax rule"
445 lchar '='
446 openBlock
447 dec <- some (decl syn)
448 closeBlock
449 return (DeclRule (mkSimple syms) (concat dec))
450 where
451 isExpr (Expr _) = True
452 isExpr _ = False
453 getName (Expr n) = Just n
454 getName _ = Nothing
455 -- Can't parse two full expressions (i.e. expressions with application) in a row
456 -- so change them both to a simple expression
457 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
458 mkSimple xs = mkSimple' xs
460 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
461 mkSimple es
462 -- Can't parse a full expression followed by operator like characters due to ambiguity
463 mkSimple' (Expr e : Symbol s : es)
464 | takeWhile (`elem` opChars) ts /= "" = SimpleExpr e : Symbol s : mkSimple' es
465 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s
466 mkSimple' (e : es) = e : mkSimple' es
467 mkSimple' [] = []
469 -- Prevent syntax variable capture by making all binders under syntax unique
470 -- (the ol' Common Lisp GENSYM approach)
471 uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
472 uniquifyBinders userNames = fixBind 0 []
473 where
474 fixBind :: Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
475 fixBind 0 rens (PRef fc hls n) | Just n' <- lookup n rens =
476 return $ PRef fc hls n'
477 fixBind 0 rens (PPatvar fc n) | Just n' <- lookup n rens =
478 return $ PPatvar fc n'
479 fixBind 0 rens (PLam fc n nfc ty body)
480 | n `elem` userNames = liftM2 (PLam fc n nfc)
481 (fixBind 0 rens ty)
482 (fixBind 0 rens body)
483 | otherwise =
484 do ty' <- fixBind 0 rens ty
485 n' <- gensym n
486 body' <- fixBind 0 ((n,n'):rens) body
487 return $ PLam fc n' nfc ty' body'
488 fixBind 0 rens (PPi plic n nfc argTy body)
489 | n `elem` userNames = liftM2 (PPi plic n nfc)
490 (fixBind 0 rens argTy)
491 (fixBind 0 rens body)
492 | otherwise =
493 do ty' <- fixBind 0 rens argTy
494 n' <- gensym n
495 body' <- fixBind 0 ((n,n'):rens) body
496 return $ (PPi plic n' nfc ty' body')
497 fixBind 0 rens (PLet fc rig n nfc ty val body)
498 | n `elem` userNames = liftM3 (PLet fc rig n nfc)
499 (fixBind 0 rens ty)
500 (fixBind 0 rens val)
501 (fixBind 0 rens body)
502 | otherwise =
503 do ty' <- fixBind 0 rens ty
504 val' <- fixBind 0 rens val
505 n' <- gensym n
506 body' <- fixBind 0 ((n,n'):rens) body
507 return $ PLet fc rig n' nfc ty' val' body'
508 fixBind 0 rens (PMatchApp fc n) | Just n' <- lookup n rens =
509 return $ PMatchApp fc n'
510 -- Also rename resolved quotations, to allow syntax rules to
511 -- have quoted references to their own bindings.
512 fixBind 0 rens (PQuoteName n True fc) | Just n' <- lookup n rens =
513 return $ PQuoteName n' True fc
515 -- Don't mess with quoted terms
516 fixBind q rens (PQuasiquote tm goal) =
517 flip PQuasiquote goal <$> fixBind (q + 1) rens tm
518 fixBind q rens (PUnquote tm) =
519 PUnquote <$> fixBind (q - 1) rens tm
521 fixBind q rens x = descendM (fixBind q rens) x
523 gensym :: Name -> IdrisParser Name
524 gensym n = do ist <- get
525 let idx = idris_name ist
526 put ist { idris_name = idx + 1 }
527 return $ sMN idx (show n)
529{-| Parses a syntax symbol (either binding variable, keyword or expression)
532SyntaxSym ::= '[' Name_t ']'
533 | '{' Name_t '}'
534 | Name_t
535 | StringLiteral_t
536 ;
538 -}
539syntaxSym :: IdrisParser SSymbol
540syntaxSym = P.try (do lchar '['; n <- name; lchar ']'
541 return (Expr n))
542 <|> P.try (do lchar '{'; n <- name; lchar '}'
543 return (Binding n))
544 <|> do n <- iName []
545 return (Keyword n)
546 <|> do sym <- stringLiteral
547 return (Symbol sym)
548 <?> "syntax symbol"
550{-| Parses a function declaration with possible syntax sugar
553 FunDecl ::= FunDecl';
555-}
556fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
557fnDecl syn = P.try (do notEndBlock
558 d <- fnDecl' syn
559 i <- get
560 let d' = fmap (debindApp syn . desugar syn i) d
561 return [d']) <?> "function declaration"
563{-| Parses a function declaration
566 FunDecl' ::=
567 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
568 | Postulate
569 | Pattern
570 | CAF
571 ;
573-}
574fnDecl' :: SyntaxInfo -> IdrisParser PDecl
575fnDecl' syn = (checkDeclFixity $
576 do (doc, argDocs, fc, opts', n, nfc, acc) <- P.try (do
577 pushIndent
578 (doc, argDocs) <- docstring syn
579 (opts, acc) <- fnOpts
580 (n_in, nfc) <- withExtent fnName
581 let n = expandNS syn n_in
582 fc <- extent $ lchar ':'
583 return (doc, argDocs, fc, opts, n, nfc, acc))
584 ty <- typeExpr (allowImp syn)
585 terminator
586 -- If it's a top level function, note the accessibility
587 -- rules
588 when (syn_toplevel syn) $ addAcc n acc
589 return (PTy doc argDocs syn fc opts' n nfc ty)
590 <|> postulate syn
591 <|> caf syn
592 <|> pattern syn)
593 <?> "function declaration"
595{-| Parses a series of function and accessbility options
598FnOpts ::= FnOpt* Accessibility FnOpt*
600 -}
601fnOpts :: IdrisParser ([FnOpt], Accessibility)
602fnOpts = do
603 opts <- many fnOpt
604 acc <- accessibility
605 opts' <- many fnOpt
606 let allOpts = opts ++ opts'
607 let existingTotality = allOpts `intersect` [TotalFn, CoveringFn, PartialFn]
608 opts'' <- addDefaultTotality (nub existingTotality) allOpts
609 return (opts'', acc)
610 where prettyTot TotalFn = "total"
611 prettyTot PartialFn = "partial"
612 prettyTot CoveringFn = "covering"
613 addDefaultTotality [] opts = do
614 ist <- get
615 case default_total ist of
616 DefaultCheckingTotal -> return (TotalFn:opts)
617 DefaultCheckingCovering -> return (CoveringFn:opts)
618 DefaultCheckingPartial -> return opts -- Don't add partial so that --warn-partial still reports warnings if necessary
619 addDefaultTotality [tot] opts = return opts
620 -- Should really be a semantics error instead of a parser error
621 addDefaultTotality (tot1:tot2:tots) opts =
622 fail ("Conflicting totality modifiers specified " ++ prettyTot tot1 ++ " and " ++ prettyTot tot2)
625{-| Parses a function option
628FnOpt ::= 'total'
629 | 'partial'
630 | 'covering'
631 | 'implicit'
632 | '%' 'no_implicit'
633 | '%' 'assert_total'
634 | '%' 'error_handler'
635 | '%' 'reflection'
636 | '%' 'specialise' '[' NameTimesList? ']'
637 ;
641NameTimes ::= FnName Natural?;
645NameTimesList ::=
646 NameTimes
647 | NameTimes ',' NameTimesList
648 ;
650-}
651fnOpt :: IdrisParser FnOpt
652fnOpt = do keyword "total"; return TotalFn
653 <|> PartialFn <$ keyword "partial"
654 <|> CoveringFn <$ keyword "covering"
655 <|> do P.try (lchar '%' *> reserved "export"); c <- stringLiteral;
656 return $ CExport c
657 <|> NoImplicit <$ P.try (lchar '%' *> reserved "no_implicit")
658 <|> Inlinable <$ P.try (lchar '%' *> reserved "inline")
659 <|> StaticFn <$ P.try (lchar '%' *> reserved "static")
660 <|> ErrorHandler <$ P.try (lchar '%' *> reserved "error_handler")
661 <|> ErrorReverse <$ P.try (lchar '%' *> reserved "error_reverse")
662 <|> ErrorReduce <$ P.try (lchar '%' *> reserved "error_reduce")
663 <|> Reflection <$ P.try (lchar '%' *> reserved "reflection")
664 <|> AutoHint <$ P.try (lchar '%' *> reserved "hint")
665 <|> OverlappingDictionary <$ P.try (lchar '%' *> reserved "overlapping")
666 <|> do lchar '%'; reserved "specialise";
667 lchar '['; ns <- P.sepBy nameTimes (lchar ','); lchar ']';
668 return $ Specialise ns
669 <|> Implicit <$ keyword "implicit"
670 <?> "function modifier"
671 where nameTimes :: IdrisParser (Name, Maybe Int)
672 nameTimes = do n <- fnName
673 t <- P.option Nothing (do reds <- natural
674 return (Just (fromInteger reds)))
675 return (n, t)
677{-| Parses a postulate
680Postulate ::=
681 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
682 ;
684-}
685postulate :: SyntaxInfo -> IdrisParser PDecl
686postulate syn = do (doc, ext)
687 <- P.try $ do (doc, _) <- docstring syn
688 pushIndent
689 ext <- ppostDecl
690 return (doc, ext)
691 ist <- get
692 (opts, acc) <- fnOpts
693 (n_in, nfc) <- withExtent fnName
694 let n = expandNS syn n_in
695 lchar ':'
696 ty <- typeExpr (allowImp syn)
697 fc <- extent $ terminator
698 addAcc n acc
699 return (PPostulate ext doc syn fc nfc opts n ty)
700 <?> "postulate"
701 where ppostDecl = do fc <- keyword "postulate"; return False
702 <|> do lchar '%'; reserved "extern"; return True
704{-| Parses a using declaration
707Using ::=
708 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
709 ;
711 -}
712using_ :: SyntaxInfo -> IdrisParser [PDecl]
713using_ syn =
714 do keyword "using"
715 lchar '('; ns <- usingDeclList syn; lchar ')'
716 openBlock
717 let uvars = using syn
718 ds <- many (decl (syn { using = uvars ++ ns }))
719 closeBlock
720 return (concat ds)
721 <?> "using declaration"
723{-| Parses a parameters declaration
726Params ::=
727 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
728 ;
730-}
731params :: SyntaxInfo -> IdrisParser [PDecl]
732params syn =
733 do (ns, fc) <- withExtent $ do
734 keyword "parameters"
735 lchar '(' *> typeDeclList syn <* lchar ')'
736 let ns' = [(n, ty) | (_, n, _, ty) <- ns]
737 openBlock
738 let pvars = syn_params syn
739 ds <- many (decl syn { syn_params = pvars ++ ns' })
740 closeBlock
741 return [PParams fc ns' (concat ds)]
742 <?> "parameters declaration"
744-- | Parses an open block
745openInterface :: SyntaxInfo -> IdrisParser [PDecl]
746openInterface syn =
747 do (ns, fc) <- withExtent $ do
748 keyword "using"
749 keyword "implementation"
750 P.sepBy1 (withExtent fnName) (lchar ',')
752 openBlock
753 ds <- many (decl syn)
754 closeBlock
755 return [POpenInterfaces fc (map fst ns) (concat ds)]
756 <?> "open interface declaration"
762{-| Parses a mutual declaration (for mutually recursive functions)
765Mutual ::=
766 'mutual' OpenBlock Decl* CloseBlock
767 ;
769-}
770mutual :: SyntaxInfo -> IdrisParser [PDecl]
771mutual syn =
772 do fc <- extent $ keyword "mutual"
773 openBlock
774 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
775 closeBlock
776 return [PMutual fc (concat ds)]
777 <?> "mutual block"
779{-| Parses a namespace declaration
782Namespace ::=
783 'namespace' identifier OpenBlock Decl+ CloseBlock
784 ;
786-}
787namespace :: SyntaxInfo -> IdrisParser [PDecl]
788namespace syn =
789 do keyword "namespace"
790 (n, nfc) <- withExtent identifier
791 openBlock
792 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
793 closeBlock
794 return [PNamespace n nfc (concat ds)]
795 <?> "namespace declaration"
797{-| Parses a methods block (for implementations)
800 ImplementationBlock ::= 'where' OpenBlock FnDecl* CloseBlock
802-}
803implementationBlock :: SyntaxInfo -> IdrisParser [PDecl]
804implementationBlock syn = do keyword "where"
805 openBlock
806 ds <- many (fnDecl syn)
807 closeBlock
808 return (concat ds)
809 <?> "implementation block"
811{-| Parses a methods and implementations block (for interfaces)
814MethodOrImplementation ::=
815 FnDecl
816 | Implementation
817 ;
821InterfaceBlock ::=
822 'where' OpenBlock Constructor? MethodOrImplementation* CloseBlock
823 ;
825-}
826interfaceBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])
827interfaceBlock syn = do keyword "where"
828 openBlock
829 (cn, cd) <- P.option (Nothing, emptyDocstring) $
830 P.try (do (doc, _) <- P.option noDocs docComment
831 n <- constructor
832 return (Just n, doc))
833 ist <- get
834 let cd' = annotate syn ist cd
836 ds <- many (notEndBlock >> P.try (implementation syn)
837 <|> do x <- data_ syn
838 return [x]
839 <|> fnDecl syn)
840 closeBlock
841 return (cn, cd', concat ds)
842 <?> "interface block"
843 where
844 constructor :: IdrisParser (Name, FC)
845 constructor = keyword "constructor" *> withExtent fnName
847 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)
848 annotate syn ist = annotCode $ tryFullExpr syn ist
850{-| Parses an interface declaration
853InterfaceArgument ::=
854 Name
855 | '(' Name ':' Expr ')'
856 ;
860Interface ::=
861 DocComment_t? Accessibility? 'interface' ConstraintList? Name InterfaceArgument* InterfaceBlock?
862 ;
864-}
865interface_ :: SyntaxInfo -> IdrisParser [PDecl]
866interface_ syn = do (doc, argDocs, acc)
867 <- P.try (do (doc, argDocs) <- docstring syn
868 acc <- accessibility
869 interfaceKeyword
870 return (doc, argDocs, acc))
871 ((cons', n, nfc, cs, fds), fc) <- withExtent $ do
872 cons <- constraintList syn
873 let cons' = [(c, ty) | (_, c, _, ty) <- cons]
874 (n_in, nfc) <- withExtent fnName
875 let n = expandNS syn n_in
876 cs <- many carg
877 fds <- P.option [(cn, NoFC) | (cn, _, _) <- cs] fundeps
878 return (cons', n, nfc, cs, fds)
880 (cn, cd, ds) <- P.option (Nothing, fst noDocs, []) (interfaceBlock syn)
881 accData acc n (concatMap declared ds)
882 return [PInterface doc syn fc cons' n nfc cs argDocs fds ds cn cd]
883 <?> "interface declaration"
884 where
885 fundeps :: IdrisParser [(Name, FC)]
886 fundeps = do lchar '|'; P.sepBy (withExtent name) (lchar ',')
888 classWarning :: String
889 classWarning = "Use of a fragile keyword `class`. " ++
890 "`class` is provided for those coming from Haskell. " ++
891 "Please use `interface` instead, which is equivalent."
893 interfaceKeyword :: IdrisParser ()
894 interfaceKeyword = keyword "interface"
895 <|> do fc <- extent $ keyword "class"
896 parserWarning fc Nothing (Msg classWarning)
898 carg :: IdrisParser (Name, FC, PTerm)
899 carg = do lchar '('; (i, ifc) <- withExtent name; lchar ':'; ty <- expr syn; lchar ')'
900 return (i, ifc, ty)
901 <|> do (i, ifc) <- withExtent name
902 return (i, ifc, PType ifc)
904{-| Parses an interface implementation declaration
907 Implementation ::=
908 DocComment_t? 'implementation' ImplementationName? ConstraintList? Name SimpleExpr* ImplementationBlock?
909 ;
913ImplementationName ::= '[' Name ']';
915-}
916implementation :: SyntaxInfo -> IdrisParser [PDecl]
917implementation syn = do (doc, argDocs) <- docstring syn
918 (opts, acc) <- fnOpts
919 optional implementationKeyword
921 ((en, cs, cs', cn, cnfc, args, pnames), fc) <- withExtent $ do
922 en <- optional implementationName
923 cs <- constraintList syn
924 let cs' = [(c, ty) | (_, c, _, ty) <- cs]
925 (cn, cnfc) <- withExtent fnName
926 args <- many (simpleExpr syn)
927 pnames <- implementationUsing
928 return (en, cs, cs', cn, cnfc, args, pnames)
930 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)
931 let t = bindList (\r -> PPi constraint { pcount = r }) cs sc
933 ds <- implementationBlock syn
934 return [PImplementation doc argDocs syn fc cs' pnames acc opts cn cnfc args [] t en ds]
935 <?> "implementation declaration"
936 where implementationName :: IdrisParser Name
937 implementationName = do lchar '['; n_in <- fnName; lchar ']'
938 let n = expandNS syn n_in
939 return n
940 <?> "implementation name"
942 instanceWarning :: String
943 instanceWarning = "Use of fragile keyword `instance`. " ++
944 "`instance` is provided for those coming from Haskell. " ++
945 "Please use `implementation` (which is equivalent) instead, or omit it."
947 implementationKeyword :: IdrisParser ()
948 implementationKeyword = keyword "implementation"
949 <|> do fc <- extent $ keyword "instance"
950 parserWarning fc Nothing (Msg instanceWarning)
952 implementationUsing :: IdrisParser [Name]
953 implementationUsing = do keyword "using"
954 ns <- P.sepBy1 (withExtent fnName) (lchar ',')
955 return (map fst ns)
956 <|> return []
958-- | Parse a docstring
959docstring :: SyntaxInfo
960 -> IdrisParser (Docstring (Either Err PTerm),
961 [(Name,Docstring (Either Err PTerm))])
962docstring syn = do (doc, argDocs) <- P.option noDocs docComment
963 ist <- get
964 let doc' = annotCode (tryFullExpr syn ist) doc
965 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
966 | (n, d) <- argDocs ]
967 return (doc', argDocs')
970{-| Parses a using declaration list
973UsingDeclList ::=
974 UsingDeclList'
975 | NameList TypeSig
976 ;
980UsingDeclList' ::=
981 UsingDecl
982 | UsingDecl ',' UsingDeclList'
983 ;
987NameList ::=
988 Name
989 | Name ',' NameList
990 ;
992-}
993usingDeclList :: SyntaxInfo -> IdrisParser [Using]
994usingDeclList syn
995 = P.try (P.sepBy1 (usingDecl syn) (lchar ','))
996 <|> do ns <- P.sepBy1 name (lchar ',')
997 lchar ':'
998 t <- typeExpr (disallowImp syn)
999 return (map (\x -> UImplicit x t) ns)
1000 <?> "using declaration list"
1002{-| Parses a using declaration
1005UsingDecl ::=
1006 FnName TypeSig
1007 | FnName FnName+
1011usingDecl :: SyntaxInfo -> IdrisParser Using
1012usingDecl syn = P.try (do x <- fnName
1013 lchar ':'
1014 t <- typeExpr (disallowImp syn)
1015 return (UImplicit x t))
1016 <|> do c <- fnName
1017 xs <- many fnName
1018 return (UConstraint c xs)
1019 <?> "using declaration"
1021{-| Parse a clause with patterns
1024Pattern ::= Clause;
1027pattern :: SyntaxInfo -> IdrisParser PDecl
1028pattern syn = do (clause, fc) <- withExtent (clause syn)
1029 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
1030 <?> "pattern"
1032{-| Parse a constant applicative form declaration
1035CAF ::= 'let' FnName '=' Expr Terminator;
1038caf :: SyntaxInfo -> IdrisParser PDecl
1039caf syn = do keyword "let"
1040 (n, fc) <- withExtent (expandNS syn <$> fnName)
1041 pushIndent
1042 lchar '='
1043 t <- indented $ expr syn
1044 terminator
1045 return (PCAF fc n t)
1046 <?> "constant applicative form declaration"
1048{-| Parse an argument expression
1051ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
1054argExpr :: SyntaxInfo -> IdrisParser PTerm
1055argExpr syn = let syn' = syn { inPattern = True } in
1056 P.try (hsimpleExpr syn') <|> simpleExternalExpr syn'
1057 <?> "argument expression"
1059{-| Parse a right hand side of a function
1062RHS ::= '=' Expr
1063 | '?=' RHSName? Expr
1064 | Impossible
1069RHSName ::= '{' FnName '}';
1072rhs :: SyntaxInfo -> Name -> IdrisParser (PTerm, FC)
1073rhs syn n = do lchar '='
1074 indentGt
1075 withExtent $ expr syn
1076 <|> do symbol "?=";
1077 (name, fc) <- withExtent $ P.option n' (symbol "{" *> fnName <* symbol "}")
1078 r <- expr syn
1079 return (addLet fc name r, fc)
1080 <|> withExtent impossible
1081 <?> "function right hand side"
1082 where mkN :: Name -> Name
1083 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
1084 then sUN "infix_op_lemma_1"
1085 else sUN (str x++"_lemma_1")
1086 mkN (NS x n) = NS (mkN x) n
1087 n' :: Name
1088 n' = mkN n
1089 addLet :: FC -> Name -> PTerm -> PTerm
1090 addLet fc nm (PLet fc' rig n nfc ty val r) = PLet fc' rig n nfc ty val (addLet fc nm r)
1091 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
1092 where addLetC (l, r) = (l, addLet fc nm r)
1093 addLet fc nm r = (PLet fc RigW (sUN "value") NoFC Placeholder r (PMetavar NoFC nm))
1095{-|Parses a function clause
1098RHSOrWithBlock ::= RHS WhereOrTerminator
1099 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
1104Clause ::= WExpr+ RHSOrWithBlock
1105 | SimpleExpr '<==' FnName RHS WhereOrTerminator
1106 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
1107 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
1112ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
1116WhereOrTerminator ::= WhereBlock | Terminator;
1119clause :: SyntaxInfo -> IdrisParser PClause
1120clause syn
1121 -- unnamed with or function clause (inside a with)
1122 = do wargs <- P.try (do pushIndent; some (wExpr syn))
1123 ist <- get
1124 n <- case lastParse ist of
1125 Just t -> return t
1126 Nothing -> fail "Invalid clause"
1127 (do (r, fc) <- rhs syn n
1128 let wsyn = syn { syn_namespace = [], syn_toplevel = False }
1129 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1130 <|> ([], []) <$ terminator
1131 return $ PClauseR fc wargs r wheres) <|> (do
1132 popIndent
1133 ((wval, pn), fc) <- withExtent $ do
1134 keyword "with"
1135 wval <- bracketed syn
1136 pn <- optProof
1137 return (wval, pn)
1138 openBlock
1139 ds <- some $ fnDecl syn
1140 let withs = concat ds
1141 closeBlock
1142 return $ PWithR fc wargs wval pn withs)
1143 -- <==
1144 <|> do ty <- P.try (do pushIndent
1145 ty <- simpleExpr syn
1146 symbol "<=="
1147 return ty)
1148 (n, fc) <- withExtent (expandNS syn <$> fnName)
1149 (r, _) <- rhs syn n
1150 let wsyn = syn { syn_namespace = [] }
1151 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1152 <|> ([], []) <$ terminator
1153 let capp = PLet fc RigW (sMN 0 "match") NoFC
1154 ty
1155 (PMatchApp fc n)
1156 (PRef fc [] (sMN 0 "match"))
1157 ist <- get
1158 put (ist { lastParse = Just n })
1159 return $ PClause fc n capp [] r wheres
1160 -- lhs application "with" clause or function clause
1161 <|> do pushIndent
1162 (n, nfc, capp, wargs) <- lhs
1163 modify $ \ist -> ist { lastParse = Just n }
1164 (do (rs, fc) <- rhs syn n
1165 let wsyn = syn { syn_namespace = [] }
1166 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1167 <|> ([], []) <$ terminator
1168 return $ PClause fc n capp wargs rs wheres) <|> (do
1169 popIndent
1170 ((wval, pn), fc) <- withExtent $ do
1171 keyword "with"
1172 wval <- bracketed syn
1173 pn <- optProof
1174 return (wval, pn)
1175 openBlock
1176 ds <- some $ fnDecl syn
1177 closeBlock
1178 let withs = map (fillLHSD n capp wargs) $ concat ds
1179 return $ PWith fc n capp wargs wval pn withs)
1180 <?> "function clause"
1181 where
1182 lhsInfixApp :: IdrisParser (Name, FC, [PArg], [PTerm])
1183 lhsInfixApp = do l <- argExpr syn
1184 (op, nfc) <- withExtent symbolicOperator
1185 when (op == "=" || op == "?=" ) $
1186 fail "infix clause definition with \"=\" and \"?=\" not supported "
1187 let n = expandNS syn (sUN op)
1188 r <- argExpr syn
1189 wargs <- many (wExpr syn)
1190 return (n, nfc, [pexp l, pexp r], wargs)
1192 lhsPrefixApp :: IdrisParser (Name, FC, [PArg], [PTerm])
1193 lhsPrefixApp = do (n, nfc) <- withExtent (expandNS syn <$> fnName)
1194 args <- many (P.try (implicitArg (syn { inPattern = True } ))
1195 <|> P.try (constraintArg (syn { inPattern = True }))
1196 <|> (fmap pexp (argExpr syn)))
1197 wargs <- many (wExpr syn)
1198 return (n, nfc, args, wargs)
1200 lhs :: IdrisParser (Name, FC, PTerm, [PTerm])
1201 lhs = do ((n, nfc, args, wargs), lhs_fc) <- withExtent (P.try lhsInfixApp <|> lhsPrefixApp)
1202 let capp = PApp lhs_fc (PRef nfc [nfc] n) args
1203 return (n, nfc, capp, wargs)
1205 optProof = P.option Nothing (do keyword "proof"
1206 n <- withExtent fnName
1207 return (Just n))
1209 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
1210 fillLHS n capp owargs (PClauseR fc wargs v ws)
1211 = PClause fc n capp (owargs ++ wargs) v ws
1212 fillLHS n capp owargs (PWithR fc wargs v pn ws)
1213 = PWith fc n capp (owargs ++ wargs) v pn
1214 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1215 fillLHS _ _ _ c = c
1217 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
1218 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1219 fillLHSD n c a x = x
1221{-| Parses with pattern
1224WExpr ::= '|' Expr';
1227wExpr :: SyntaxInfo -> IdrisParser PTerm
1228wExpr syn = do lchar '|'
1229 expr' (syn { inPattern = True })
1230 <?> "with pattern"
1232{-| Parses a where block
1235WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
1238whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
1239whereBlock n syn
1240 = do keyword "where"
1241 ds <- indentedBlock1 (decl syn)
1242 let dns = concatMap (concatMap declared) ds
1243 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1244 <?> "where block"
1246{-|Parses a code generation target language name
1249Codegen ::= 'C'
1250 | 'Java'
1251 | 'JavaScript'
1252 | 'Node'
1253 | 'LLVM'
1254 | 'Bytecode'
1258codegen_ :: IdrisParser Codegen
1259codegen_ = do n <- identifier
1260 return (Via IBCFormat (map toLower n))
1261 <|> do reserved "Bytecode"; return Bytecode
1262 <?> "code generation language"
1264{-|Parses a compiler directive
1266StringList ::=
1267 String
1268 | String ',' StringList
1273Directive ::= '%' Directive';
1277Directive' ::= 'lib' CodeGen String_t
1278 | 'link' CodeGen String_t
1279 | 'flag' CodeGen String_t
1280 | 'include' CodeGen String_t
1281 | 'hide' Name
1282 | 'freeze' Name
1283 | 'thaw' Name
1284 | 'access' Accessibility
1285 | 'default' Totality
1286 | 'logging' Natural
1287 | 'dynamic' StringList
1288 | 'name' Name NameList
1289 | 'error_handlers' Name NameList
1290 | 'language' 'TypeProviders'
1291 | 'language' 'ErrorReflection'
1292 | 'deprecated' Name String
1293 | 'fragile' Name Reason
1297directive :: SyntaxInfo -> IdrisParser [PDecl]
1298directive syn = do P.try (lchar '%' *> reserved "lib")
1299 cgn <- codegen_
1300 lib <- stringLiteral
1301 return [PDirective (DLib cgn lib)]
1302 <|> do P.try (lchar '%' *> reserved "link")
1303 cgn <- codegen_; obj <- stringLiteral
1304 return [PDirective (DLink cgn obj)]
1305 <|> do P.try (lchar '%' *> reserved "flag")
1306 cgn <- codegen_; flag <- stringLiteral
1307 return [PDirective (DFlag cgn flag)]
1308 <|> do P.try (lchar '%' *> reserved "include")
1309 cgn <- codegen_
1310 hdr <- stringLiteral
1311 return [PDirective (DInclude cgn hdr)]
1312 <|> do P.try (lchar '%' *> reserved "hide"); n <- fnName
1313 return [PDirective (DHide n)]
1314 <|> do P.try (lchar '%' *> reserved "freeze"); n <- iName []
1315 return [PDirective (DFreeze n)]
1316 <|> do P.try (lchar '%' *> reserved "thaw"); n <- iName []
1317 return [PDirective (DThaw n)]
1318 -- injectivity assertins are intended for debugging purposes
1319 -- only, and won't be documented/could be removed at any point
1320 <|> do P.try (lchar '%' *> reserved "assert_injective"); n <- fnName
1321 return [PDirective (DInjective n)]
1322 -- Assert totality of something after definition. This is
1323 -- here as a debugging aid, so commented out...
1324-- <|> do P.try (lchar '%' *> reserved "assert_set_total"); n <- fst <$> fnName
1325-- return [PDirective (DSetTotal n)]
1326 <|> do P.try (lchar '%' *> reserved "access")
1327 acc <- accessibility
1328 ist <- get
1329 put ist { default_access = acc }
1330 return [PDirective (DAccess acc)]
1331 <|> do P.try (lchar '%' *> reserved "default"); tot <- totality
1332 i <- get
1333 put (i { default_total = tot } )
1334 return [PDirective (DDefault tot)]
1335 <|> do P.try (lchar '%' *> reserved "logging")
1336 i <- natural
1337 return [PDirective (DLogging i)]
1338 <|> do P.try (lchar '%' *> reserved "dynamic")
1339 libs <- P.sepBy1 stringLiteral (lchar ',')
1340 return [PDirective (DDynamicLibs libs)]
1341 <|> do P.try (lchar '%' *> reserved "name")
1342 (ty, tyFC) <- withExtent fnName
1343 ns <- P.sepBy1 (withExtent name) (lchar ',')
1344 return [PDirective (DNameHint ty tyFC ns)]
1345 <|> do P.try (lchar '%' *> reserved "error_handlers")
1346 (fn, nfc) <- withExtent fnName
1347 (arg, afc) <- withExtent fnName
1348 ns <- P.sepBy1 (withExtent name) (lchar ',')
1349 return [PDirective (DErrorHandlers fn nfc arg afc ns) ]
1350 <|> do P.try (lchar '%' *> reserved "language"); ext <- pLangExt;
1351 return [PDirective (DLanguage ext)]
1352 <|> do P.try (lchar '%' *> reserved "deprecate")
1353 n <- fnName
1354 alt <- P.option "" stringLiteral
1355 return [PDirective (DDeprecate n alt)]
1356 <|> do P.try (lchar '%' *> reserved "fragile")
1357 n <- fnName
1358 alt <- P.option "" stringLiteral
1359 return [PDirective (DFragile n alt)]
1360 <|> do fc <- extent $ P.try (lchar '%' *> reserved "used")
1361 fn <- fnName
1362 arg <- iName []
1363 return [PDirective (DUsed fc fn arg)]
1364 <|> do P.try (lchar '%' *> reserved "auto_implicits")
1365 b <- on_off
1366 return [PDirective (DAutoImplicits b)]
1367 <?> "directive"
1368 where on_off = do reserved "on"; return True
1369 <|> do reserved "off"; return False
1371pLangExt :: IdrisParser LanguageExt
1372pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1373 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1374 <|> (reserved "UniquenessTypes" >> return UniquenessTypes)
1375 <|> (reserved "LinearTypes" >> return LinearTypes)
1376 <|> (reserved "DSLNotation" >> return DSLNotation)
1377 <|> (reserved "ElabReflection" >> return ElabReflection)
1378 <|> (reserved "FirstClassReflection" >> return FCReflection)
1380{-| Parses a totality
1383Totality ::= 'partial' | 'total' | 'covering'
1387totality :: IdrisParser DefaultTotality
1388totality
1389 = do keyword "total"; return DefaultCheckingTotal
1390 <|> do keyword "partial"; return DefaultCheckingPartial
1391 <|> do keyword "covering"; return DefaultCheckingCovering
1393{-| Parses a type provider
1396Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1397ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1399 -}
1400provider :: SyntaxInfo -> IdrisParser [PDecl]
1401provider syn = do doc <- P.try (do (doc, _) <- docstring syn
1402 highlight AnnKeyword $ lchar '%' *> reserved "provide"
1403 return doc)
1404 provideTerm doc <|> providePostulate doc
1405 <?> "type provider"
1406 where provideTerm doc =
1407 do lchar '('; (n, nfc) <- withExtent fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1408 keyword "with"
1409 (e, fc) <- withExtent (expr syn) <?> "provider expression"
1410 return [PProvider doc syn fc nfc (ProvTerm t e) n]
1411 providePostulate doc =
1412 do keyword "postulate"
1413 (n, nfc) <- withExtent fnName
1414 keyword "with"
1415 (e, fc) <- withExtent (expr syn) <?> "provider expression"
1416 return [PProvider doc syn fc nfc (ProvPostulate e) n]
1418{-| Parses a transform
1421Transform ::= '%' 'transform' Expr '==>' Expr
1424transform :: SyntaxInfo -> IdrisParser [PDecl]
1425transform syn = do P.try (lchar '%' *> reserved "transform")
1426 -- leave it unchecked, until we work out what this should
1427 -- actually mean...
1428-- safety <- option True (do reserved "unsafe"
1429-- return False)
1430 l <- expr syn
1431 fc <- extent $ symbol "==>"
1432 r <- expr syn
1433 return [PTransform fc False l r]
1434 <?> "transform"
1436{-| Parses a top-level reflected elaborator script
1439RunElabDecl ::= '%' 'runElab' Expr
1442runElabDecl :: SyntaxInfo -> IdrisParser PDecl
1443runElabDecl syn =
1444 do kwFC <- P.try (highlight AnnKeyword (extent $ lchar '%' *> reserved "runElab"))
1445 script <- expr syn <?> "elaborator script"
1446 return $ PRunElabDecl kwFC script (syn_namespace syn)
1447 <?> "top-level elaborator script"
1449{- * Loading and parsing -}
1450{-| Parses an expression from input -}
1451parseExpr :: IState -> String -> Either ParseError PTerm
1452parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1454{-| Parses a constant form input -}
1455parseConst :: IState -> String -> Either ParseError Const
1456parseConst st = runparser constant st "(input)"
1458{-| Parses a tactic from input -}
1459parseTactic :: IState -> String -> Either ParseError PTactic
1460parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1462{-| Parses a do-step from input (used in the elab shell) -}
1463parseElabShellStep :: IState -> String -> Either ParseError (Either ElabShellCmd PDo)
1464parseElabShellStep ist = runparser (Right <$> do_ defaultSyntax <|> Left <$> elabShellCmd) ist "(input)"
1465 where elabShellCmd = char ':' >>
1466 (reserved "qed" >> pure EQED ) <|>
1467 (reserved "abandon" >> pure EAbandon ) <|>
1468 (reserved "undo" >> pure EUndo ) <|>
1469 (reserved "state" >> pure EProofState) <|>
1470 (reserved "term" >> pure EProofTerm ) <|>
1471 (expressionTactic ["e", "eval"] EEval ) <|>
1472 (expressionTactic ["t", "type"] ECheck) <|>
1473 (expressionTactic ["search"] ESearch ) <|>
1474 (do reserved "doc"
1475 doc <- (Right <$> constant) <|> (Left <$> fnName)
1476 P.eof
1477 return (EDocStr doc))
1478 <?> "elab command"
1479 expressionTactic cmds tactic =
1480 do asum (map reserved cmds)
1481 t <- spaced (expr defaultSyntax)
1482 i <- get
1483 return $ tactic (desugar defaultSyntax i t)
1484 spaced parser = indentGt *> parser
1486-- | Parse module header and imports
1487parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark)
1488parseImports fname input
1489 = do i <- getIState
1490 case runparser imports i fname input of
1491 Left err -> formatMessage err >>= ifail . show
1492 Right (x, annots, i) ->
1493 do putIState i
1494 fname' <- runIO $ Dir.makeAbsolute fname
1495 sendHighlighting $ S.fromList $ addPath annots fname'
1496 return x
1497 where imports :: IdrisParser ((Maybe (Docstring ()), [String],
1498 [ImportInfo],
1499 Maybe Mark),
1500 [(FC, OutputAnnotation)], IState)
1501 imports = do optional shebang
1502 whiteSpace
1503 (mdoc, mname, annots) <- moduleHeader
1504 ps_exp <- many import_
1505 mrk <- mark
1506 isEof <- lookAheadMatches P.eof
1507 let mrk' = if isEof
1508 then Nothing
1509 else Just mrk
1510 i <- get
1511 -- add Builtins and Prelude, unless options say
1512 -- not to
1513 let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp
1514 return ((mdoc, mname, ps, mrk'), annots, i)
1516 addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC', OutputAnnotation)]
1517 addPath [] _ = []
1518 addPath ((fc, AnnNamespace ns Nothing) : annots) path =
1519 (FC' fc, AnnNamespace ns (Just path)) : addPath annots path
1520 addPath ((fc,annot):annots) path = (FC' fc, annot) : addPath annots path
1522 shebang :: IdrisParser ()
1523 shebang = string "#!" *> many (P.satisfy $ not . isEol) *> eol *> pure ()
1525-- | Check if the coloring matches the options and corrects if necessary
1526fixColour :: Bool -> PP.Doc -> PP.Doc
1527fixColour False doc = PP.plain doc
1528fixColour True doc = doc
1530-- | A program is a list of declarations, possibly with associated
1531-- documentation strings.
1532parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Mark -> Idris [PDecl]
1533parseProg syn fname input mrk
1534 = do i <- getIState
1535 case runparser mainProg i fname input of
1536 Left err -> do emitWarning err
1537 i <- getIState
1538 putIState (i { errSpan = Just (messageExtent err) })
1539 return []
1540 Right (x, i) -> do putIState i
1541 reportParserWarnings
1542 return $ collect x
1543 where mainProg :: IdrisParser ([PDecl], IState)
1544 mainProg = case mrk of
1545 Nothing -> do i <- get; return ([], i)
1546 Just mrk -> do
1547 restore mrk
1548 ds <- prog syn
1549 i' <- get
1550 return (ds, i')
1552-- | Collect 'PClauses' with the same function name
1553collect :: [PDecl] -> [PDecl]
1554collect (c@(PClauses _ o _ _) : ds)
1555 = clauses (cname c) [] (c : ds)
1556 where clauses :: Maybe Name -> [PClause] -> [PDecl] -> [PDecl]
1557 clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)
1558 | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds
1559 clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r pn w] : ds)
1560 | n == n' = clauses j (PWith fc' n' l ws r pn (collect w) : acc) ds
1561 clauses (Just n) acc xs = PClauses (fcOf c) o n (reverse acc) : collect xs
1562 clauses Nothing acc (x:xs) = collect xs
1563 clauses Nothing acc [] = []
1565 cname :: PDecl -> Maybe Name
1566 cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n
1567 cname (PClauses fc _ _ [PWith _ n _ _ _ _ _]) = Just n
1568 cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing
1569 cname (PClauses fc _ _ [PWithR _ _ _ _ _]) = Nothing
1570 fcOf :: PDecl -> FC
1571 fcOf (PClauses fc _ _ _) = fc
1572collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
1573collect (POpenInterfaces f ns ps : ds) = POpenInterfaces f ns (collect ps) : collect ds
1574collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds
1575collect (PNamespace ns fc ps : ds) = PNamespace ns fc (collect ps) : collect ds
1576collect (PInterface doc f s cs n nfc ps pdocs fds ds cn cd : ds')
1577 = PInterface doc f s cs n nfc ps pdocs fds (collect ds) cn cd : collect ds'
1578collect (PImplementation doc argDocs f s cs pnames acc opts n nfc ps pextra t en ds : ds')
1579 = PImplementation doc argDocs f s cs pnames acc opts n nfc ps pextra t en (collect ds) : collect ds'
1580collect (d : ds) = d : collect ds
1581collect [] = []
1583{-| Load idris module and show error if something wrong happens -}
1584loadModule :: FilePath -> IBCPhase -> Idris (Maybe String)
1585loadModule f phase
1586 = idrisCatch (loadModule' f phase)
1587 (\e -> do setErrSpan (getErrSpan e)
1588 ist <- getIState
1589 iWarn (getErrSpan e) $ pprintErr ist e
1590 return Nothing)
1592{-| Load idris module -}
1593loadModule' :: FilePath -> IBCPhase -> Idris (Maybe String)
1594loadModule' f phase
1595 = do i <- getIState
1596 let file = takeWhile (/= ' ') f
1597 ibcsd <- valIBCSubDir i
1598 ids <- rankedImportDirs file
1599 fp <- findImport ids ibcsd file
1600 if file `elem` imported i
1601 then do logParser 1 $ "Already read " ++ file
1602 return Nothing
1603 else do putIState (i { imported = file : imported i })
1604 case fp of
1605 IDR fn -> loadSource False fn Nothing
1606 LIDR fn -> loadSource True fn Nothing
1607 IBC fn src ->
1608 idrisCatch (loadIBC True phase fn)
1609 (\c -> do logParser 1 $ fn ++ " failed " ++ pshow i c
1610 case src of
1611 IDR sfn -> loadSource False sfn Nothing
1612 LIDR sfn -> loadSource True sfn Nothing)
1613 return $ Just file
1615{-| Load idris code from file -}
1616loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()
1617loadFromIFile reexp phase i@(IBC fn src) maxline
1618 = do logParser 1 $ "Skipping " ++ getSrcFile i
1619 logParser 3 $ "loadFromIFile i" ++ show i
1620 idrisCatch (loadIBC reexp phase fn)
1621 (\err -> ierror $ LoadingFailed fn err)
1622 where
1623 getSrcFile (IDR fn) = fn
1624 getSrcFile (LIDR fn) = fn
1625 getSrcFile (IBC f src) = getSrcFile src
1627loadFromIFile _ _ (IDR fn) maxline = loadSource' False fn maxline
1628loadFromIFile _ _ (LIDR fn) maxline = loadSource' True fn maxline
1630{-| Load idris source code and show error if something wrong happens -}
1631loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1632loadSource' lidr r maxline
1633 = idrisCatch (loadSource lidr r maxline)
1634 (\e -> do setErrSpan (getErrSpan e)
1635 ist <- getIState
1636 case e of
1637 At f e' -> iWarn f (pprintErr ist e')
1638 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1640{-| Load Idris source code-}
1641loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1642loadSource lidr f toline
1643 = do logParser 1 ("Reading " ++ f)
1644 iReport 2 ("Reading " ++ f)
1645 i <- getIState
1646 let def_total = default_total i
1647 file_in <- runIO $ readSource f
1648 file <- if lidr then tclift $ unlit f file_in else return file_in
1649 (mdocs, mname, imports_in, pos) <- parseImports f file
1650 ai <- getAutoImports
1651 let imports = map (\n -> ImportInfo True n Nothing [] NoFC NoFC) ai ++ imports_in
1652 ids <- rankedImportDirs f
1653 ibcsd <- valIBCSubDir i
1654 let ibc = ibcPathNoFallback ibcsd f
1655 impHashes <- idrisCatch (getImportHashes ibc)
1656 (\err -> return [])
1657 newHashes <- mapM (\ (_, f, _, _) ->
1658 do fp <- findImport ids ibcsd f
1659 case fp of
1660 IBC fn src ->
1661 idrisCatch (do hash <- getIBCHash fn
1662 return (Just (fn, hash)))
1663 (\err -> return Nothing)
1664 _ -> return Nothing)
1665 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]
1667 fmod <- liftIO $ Dir.getModificationTime f
1668 ibcexists <- liftIO $ Dir.doesFileExist ibc
1669 ibcmod <- if ibcexists
1670 then liftIO $ Dir.getModificationTime ibc
1671 else return fmod
1673 logParser 10 $ ibc ++ " " ++ show ibcmod
1674 logParser 10 $ f ++ " " ++ show fmod
1675 logParser 10 $ show impHashes ++ "\n" ++ show newHashes
1677 -- If the ibc is newer than the source, and the old import
1678 -- hashes are the same as the ones we've just read,
1679 -- quit and just load the IBC
1681 let needLoad = (ibcmod <= fmod) ||
1682 (sort impHashes /= sort (mapMaybe id newHashes))
1684 if not needLoad
1685 then pure ()
1686 else do
1687 iReport 1 $ "Type checking " ++ f
1688 mapM_ (\ (re, f, ns, nfc) ->
1689 do fp <- findImport ids ibcsd f
1690 case fp of
1691 LIDR fn -> ifail $ "No ibc for " ++ f
1692 IDR fn -> ifail $ "No ibc for " ++ f
1693 IBC fn src ->
1694 do loadIBC True IBC_Building fn
1695 let srcFn = case src of
1696 IDR fn -> Just fn
1697 LIDR fn -> Just fn
1698 _ -> Nothing
1699 srcFnAbs <- case srcFn of
1700 Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)
1701 Nothing -> return Nothing
1702 sendHighlighting $ S.fromList [(FC' nfc, AnnNamespace ns srcFnAbs)])
1703 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]
1704 reportParserWarnings
1705 sendParserHighlighting
1707 -- process and check module aliases
1708 let modAliases = M.fromList
1709 [ (prep alias, prep realName)
1710 | ImportInfo { import_reexport = reexport
1711 , import_path = realName
1712 , import_rename = Just (alias, _)
1713 , import_location = fc } <- imports
1715 prep = map T.pack . reverse . Spl.splitOn [pathSeparator]
1716 aliasNames = [ (alias, fc)
1717 | ImportInfo { import_rename = Just (alias, fc)
1718 } <- imports
1720 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1721 case map head . filter ((/= 1) . length) $ histogram of
1722 [] -> logParser 3 $ "Module aliases: " ++ show (M.toList modAliases)
1723 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1725 i <- getIState
1726 putIState (i { default_access = Private, module_aliases = modAliases })
1727 clearIBC -- start a new .ibc file
1728 mapM_ addIBC (map (\ (f, h) -> IBCImportHash f h)
1729 (mapMaybe id newHashes))
1730 -- record package info in .ibc
1731 imps <- allImportDirs
1732 mapM_ addIBC (map IBCImportDir imps)
1733 mapM_ (addIBC . IBCImport)
1734 [ (reexport, realName)
1735 | ImportInfo { import_reexport = reexport
1736 , import_path = realName
1737 } <- imports
1739 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1740 maxline = toline }
1741 ist <- getIState
1742 -- Save the span from parsing the module header, because
1743 -- an empty program parse might obliterate it.
1744 let oldSpan = idris_parsedSpan ist
1745 ds' <- parseProg syntax f file pos
1747 case (ds', oldSpan) of
1748 ([], Just fc) ->
1749 -- If no program elements were parsed, we dind't
1750 -- get a loaded region in the IBC file. That
1751 -- means we need to add it back.
1752 do ist <- getIState
1753 putIState ist { idris_parsedSpan = oldSpan
1754 , ibc_write = IBCParsedRegion fc :
1755 ibc_write ist
1757 _ -> return ()
1758 sendParserHighlighting
1760 -- Parsing done, now process declarations
1762 let ds = namespaces mname ds'
1763 logParser 3 (show $ showDecls verbosePPOption ds)
1764 i <- getIState
1765 logLvl 10 (show (toAlist (idris_implicits i)))
1766 logLvl 3 (show (idris_infixes i))
1767 -- Now add all the declarations to the context
1768 -- we totality check after every Mutual block, so if
1769 -- anything is a single definition, wrap it in a
1770 -- mutual block on its own
1771 elabDecls (toplevelWith f) (map toMutual ds)
1772 i <- getIState
1773 -- simplify every definition do give the totality checker
1774 -- a better chance
1775 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1776 ctxt' <-
1777 do ctxt <- getContext
1778 tclift $ simplifyCasedef n [] [] (getErasureInfo i) ctxt
1779 setContext ctxt')
1780 (map snd (idris_totcheck i))
1781 -- build size change graph from simplified definitions
1782 iReport 3 $ "Totality checking " ++ f
1783 logLvl 1 $ "Totality checking " ++ f
1784 i <- getIState
1785 mapM_ buildSCG (idris_totcheck i)
1786 mapM_ checkDeclTotality (idris_totcheck i)
1787 mapM_ verifyTotality (idris_totcheck i)
1789 -- Redo totality check for deferred names
1790 let deftots = idris_defertotcheck i
1791 logLvl 2 $ "Totality checking " ++ show deftots
1792 mapM_ (\x -> do tot <- getTotality x
1793 case tot of
1794 Total _ ->
1795 do let opts = case lookupCtxtExact x (idris_flags i) of
1796 Just os -> os
1797 Nothing -> []
1798 when (AssertTotal `notElem` opts) $
1799 setTotality x Unchecked
1800 _ -> return ()) (map snd deftots)
1801 mapM_ buildSCG deftots
1802 mapM_ checkDeclTotality deftots
1804 logLvl 1 ("Finished " ++ f)
1805 ibcsd <- valIBCSubDir i
1806 logLvl 1 $ "Universe checking " ++ f
1807 iReport 3 $ "Universe checking " ++ f
1808 iucheck
1809 i <- getIState
1810 addHides (hide_list i)
1812 -- Save module documentation if applicable
1813 i <- getIState
1814 case mdocs of
1815 Nothing -> return ()
1816 Just docs -> addModDoc syntax mname docs
1819 -- Finally, write an ibc and highlights if checking was successful
1820 ok <- noErrors
1821 when ok $
1822 do idrisCatch (do writeIBC f ibc; clearIBC)
1823 (\c -> return ()) -- failure is harmless
1824 hl <- getDumpHighlighting
1825 when hl $
1826 idrisCatch (writeHighlights f)
1827 (const $ return ()) -- failure is harmless
1828 clearHighlights
1829 i <- getIState
1830 putIState (i { default_total = def_total,
1831 hide_list = emptyContext })
1832 return ()
1833 where
1834 namespaces :: [String] -> [PDecl] -> [PDecl]
1835 namespaces [] ds = ds
1836 namespaces (x:xs) ds = [PNamespace x NoFC (namespaces xs ds)]
1838 toMutual :: PDecl -> PDecl
1839 toMutual m@(PMutual _ d) = m
1840 toMutual (PNamespace x fc ds) = PNamespace x fc (map toMutual ds)
1841 toMutual (POpenInterfaces f ns ds) = POpenInterfaces f ns (map toMutual ds)
1842 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1843 case x of
1844 PClauses{} -> r
1845 PInterface{} -> r
1846 PData{} -> r
1847 PImplementation{} -> r
1848 _ -> x
1850 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1851 addModDoc syn mname docs =
1852 do ist <- getIState
1853 docs' <- elabDocTerms (toplevelWith f) (parsedDocs ist)
1854 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1855 putIState ist { idris_moduledocs = modDocs' }
1856 addIBC (IBCModDocs docName)
1857 where
1858 docName = NS modDocName (map T.pack (reverse mname))
1859 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1861{-| Adds names to hide list -}
1862addHides :: Ctxt Accessibility -> Idris ()
1863addHides xs = mapM_ doHide (toAlist xs)
1864 where doHide (n, a) = do setAccessibility n a
1865 addIBC (IBCAccess n a)