git.iko.soy/Idris-dev
on bbf672a help sign in
Idris-dev/src/Idris/Parser.hs
1415 lines 51 kB history raw
1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
2{-# OPTIONS_GHC -O0 #-}
3module Idris.Parser(module Idris.Parser,
4 module Idris.ParseExpr,
5 module Idris.ParseData,
6 module Idris.ParseHelpers,
7 module Idris.ParseOps) where
9import Prelude hiding (pi)
11import Text.Trifecta.Delta
12import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)
13import Text.Parser.LookAhead
14import Text.Parser.Expression
15import qualified Text.Parser.Token as Tok
16import qualified Text.Parser.Char as Chr
17import qualified Text.Parser.Token.Highlight as Hi
19import Text.PrettyPrint.ANSI.Leijen (Doc, plain)
20import qualified Text.PrettyPrint.ANSI.Leijen as ANSI
22import Idris.AbsSyntax hiding (namespace, params)
23import Idris.DSL
24import Idris.Imports
25import Idris.Delaborate
26import Idris.Error
27import Idris.Elab.Value
28import Idris.ElabDecls
29import Idris.ElabTerm
30import Idris.Coverage
31import Idris.IBC
32import Idris.Unlit
33import Idris.Providers
34import Idris.Output
36import Idris.ParseHelpers
37import Idris.ParseOps
38import Idris.ParseExpr
39import Idris.ParseData
41import Idris.Docstrings hiding (Unchecked)
43import Paths_idris
45import Util.DynamicLinker
46import qualified Util.Pretty as P
48import Idris.Core.TT
49import Idris.Core.Evaluate
51import Control.Applicative hiding (Const)
52import Control.Monad
53import Control.Monad.State.Strict
55import Data.Function
56import Data.Maybe
57import qualified Data.List.Split as Spl
58import Data.List
59import Data.Monoid
60import Data.Char
61import Data.Ord
62import qualified Data.Map as M
63import qualified Data.HashSet as HS
64import qualified Data.Text as T
65import qualified Data.ByteString.UTF8 as UTF8
66import qualified Data.Set as S
68import Debug.Trace
70import System.FilePath
71import System.IO
73{-
75 grammar shortcut notation:
76 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)
77 RULE? = optional rule (i.e. RULE or nothing)
78 RULE* = repeated rule (i.e. RULE zero or more times)
79 RULE+ = repeated rule with at least one match (i.e. RULE one or more times)
80 RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)
81 RULE{n} = rule repeated n times
83-}
85{- * Main grammar -}
87{- | Parses module definition
90 ModuleHeader ::= 'module' Identifier_t ';'?;
92-}
93moduleHeader :: IdrisParser (Maybe (Docstring ()), [String])
94moduleHeader = try (do docs <- optional docComment
95 noArgs docs
96 reserved "module"
97 i <- identifier
98 option ';' (lchar ';')
99 return (fmap fst docs, moduleName i))
100 <|> try (do lchar '%'; reserved "unqualified"
101 return (Nothing, []))
102 <|> return (Nothing, moduleName "Main")
103 where moduleName x = case span (/='.') x of
104 (x, "") -> [x]
105 (x, '.':y) -> x : moduleName y
106 noArgs (Just (_, args)) | not (null args) = fail "Modules do not take arguments"
107 noArgs _ = return ()
109{- | Parses an import statement
112 Import ::= 'import' Identifier_t ';'?;
114 -}
115import_ :: IdrisParser (Bool, String, Maybe String, FC)
116import_ = do fc <- getFC
117 reserved "import"
118 reexport <- option False (do reserved "public"; return True)
119 id <- identifier
120 newName <- optional (reserved "as" *> identifier)
121 option ';' (lchar ';')
122 return (reexport, toPath id, toPath <$> newName, fc)
123 <?> "import statement"
124 where toPath = foldl1' (</>) . Spl.splitOn "."
126{- | Parses program source
129 Prog ::= Decl* EOF;
131 -}
132prog :: SyntaxInfo -> IdrisParser [PDecl]
133prog syn = do whiteSpace
134 decls <- many (decl syn)
135 let c = (concat decls)
136 case maxline syn of
137 Nothing -> do notOpenBraces; eof
138 _ -> return ()
139 ist <- get
140 fc <- getFC
141 put ist { idris_parsedSpan = Just (FC (fc_fname fc) (0,0) (fc_end fc)),
142 ibc_write = IBCParsedRegion fc : ibc_write ist }
143 return c
145{-| Parses a top-level declaration
148Decl ::=
149 Decl'
150 | Using
151 | Params
152 | Mutual
153 | Namespace
154 | Class
155 | Instance
156 | DSL
157 | Directive
158 | Provider
159 | Transform
160 | Import!
161 ;
163-}
164decl :: SyntaxInfo -> IdrisParser [PDecl]
165decl syn = do fc <- getFC
166 -- if we're after maxline, stop here
167 let continue = case maxline syn of
168 Nothing -> True
169 Just l -> if fst (fc_end fc) > l
170 then mut_nesting syn /= 0
171 else True
172 if continue then do notEndBlock
173 declBody
174 else fail "End of readable input"
175 where declBody :: IdrisParser [PDecl]
176 declBody = declBody'
177 <|> using_ syn
178 <|> params syn
179 <|> mutual syn
180 <|> namespace syn
181 <|> class_ syn
182 <|> instance_ syn
183 <|> do d <- dsl syn; return [d]
184 <|> directive syn
185 <|> provider syn
186 <|> transform syn
187 <|> do import_; fail "imports must be at top of file"
188 <?> "declaration"
189 declBody' :: IdrisParser [PDecl]
190 declBody' = do d <- decl' syn
191 i <- get
192 let d' = fmap (debindApp syn . (desugar syn i)) d
193 return [d']
195{- | Parses a top-level declaration with possible syntax sugar
198Decl' ::=
199 Fixity
200 | FunDecl'
201 | Data
202 | Record
203 | SyntaxDecl
204 ;
206-}
207decl' :: SyntaxInfo -> IdrisParser PDecl
208decl' syn = fixity
209 <|> syntaxDecl syn
210 <|> fnDecl' syn
211 <|> data_ syn
212 <|> record syn
213 <?> "declaration"
215{- | Parses a syntax extension declaration (and adds the rule to parser state)
218 SyntaxDecl ::= SyntaxRule;
220-}
221syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
222syntaxDecl syn = do s <- syntaxRule syn
223 i <- get
224 put (i `addSyntax` s)
225 fc <- getFC
226 return (PSyntax fc s)
228-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.
229addSyntax :: IState -> Syntax -> IState
230addSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
231 syntax_keywords = ks ++ ns,
232 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc }
233 where rs = syntax_rules i
234 ns = syntax_keywords i
235 ibc = ibc_write i
236 ks = map show (syntaxNames s)
238-- | Like 'addSyntax', but no effect on the IBC.
239addReplSyntax :: IState -> Syntax -> IState
240addReplSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
241 syntax_keywords = ks ++ ns }
242 where rs = syntax_rules i
243 ns = syntax_keywords i
244 ks = map show (syntaxNames s)
246{- | Parses a syntax extension declaration
249SyntaxRuleOpts ::= 'term' | 'pattern';
253SyntaxRule ::=
254 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
258SyntaxSym ::= '[' Name_t ']'
259 | '{' Name_t '}'
260 | Name_t
261 | StringLiteral_t
262 ;
264-}
265syntaxRule :: SyntaxInfo -> IdrisParser Syntax
266syntaxRule syn
267 = do sty <- try (do
268 pushIndent
269 sty <- option AnySyntax (do reserved "term"; return TermSyntax
270 <|> do reserved "pattern"; return PatternSyntax)
271 reserved "syntax"
272 return sty)
273 syms <- some syntaxSym
274 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
275 let ns = mapMaybe getName syms
276 when (length ns /= length (nub ns))
277 $ unexpected "repeated variable in syntax rule"
278 lchar '='
279 tm <- typeExpr (allowImp syn)
280 terminator
281 return (Rule (mkSimple syms) tm sty)
282 where
283 isExpr (Expr _) = True
284 isExpr _ = False
285 getName (Expr n) = Just n
286 getName _ = Nothing
287 -- Can't parse two full expressions (i.e. expressions with application) in a row
288 -- so change them both to a simple expression
289 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
290 mkSimple xs = mkSimple' xs
292 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
293 mkSimple es
294 mkSimple' (e : es) = e : mkSimple' es
295 mkSimple' [] = []
298{- | Parses a syntax symbol (either binding variable, keyword or expression)
301SyntaxSym ::= '[' Name_t ']'
302 | '{' Name_t '}'
303 | Name_t
304 | StringLiteral_t
305 ;
307 -}
308syntaxSym :: IdrisParser SSymbol
309syntaxSym = try (do lchar '['; n <- name; lchar ']'
310 return (Expr n))
311 <|> try (do lchar '{'; n <- name; lchar '}'
312 return (Binding n))
313 <|> do n <- iName []
314 return (Keyword n)
315 <|> do sym <- stringLiteral
316 return (Symbol sym)
317 <?> "syntax symbol"
319{- | Parses a function declaration with possible syntax sugar
322 FunDecl ::= FunDecl';
324-}
325fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
326fnDecl syn = try (do notEndBlock
327 d <- fnDecl' syn
328 i <- get
329 let d' = fmap (desugar syn i) d
330 return [d']) <?> "function declaration"
332{-| Parses a function declaration
335 FunDecl' ::=
336 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
337 | Postulate
338 | Pattern
339 | CAF
340 ;
342-}
343fnDecl' :: SyntaxInfo -> IdrisParser PDecl
344fnDecl' syn = checkFixity $
345 do (doc, argDocs, fc, opts', n, acc) <- try (do
346 pushIndent
347 (doc, argDocs) <- option noDocs docComment
348 ist <- get
349 let doc' = annotCode (tryFullExpr syn ist) doc
350 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
351 | (n, d) <- argDocs ]
353 initOpts = if default_total ist
354 then [TotalFn]
355 else []
356 opts <- fnOpts initOpts
357 acc <- optional accessibility
358 opts' <- fnOpts opts
359 n_in <- fnName
360 let n = expandNS syn n_in
361 fc <- getFC
362 lchar ':'
363 return (doc', argDocs', fc, opts', n, acc))
364 ty <- typeExpr (allowImp syn)
365 terminator
366 addAcc n acc
367 return (PTy doc argDocs syn fc opts' n ty)
368 <|> postulate syn
369 <|> caf syn
370 <|> pattern syn
371 <?> "function declaration"
372 where checkFixity :: IdrisParser PDecl -> IdrisParser PDecl
373 checkFixity p = do decl <- p
374 case getName decl of
375 Nothing -> return decl
376 Just n -> do fOk <- fixityOK n
377 unless fOk . fail $
378 "Missing fixity declaration for " ++ show n
379 return decl
380 getName (PTy _ _ _ _ _ n _) = Just n
381 getName _ = Nothing
382 fixityOK (NS n _) = fixityOK n
383 fixityOK (UN n) | all (flip elem opChars) (str n) =
384 do fixities <- fmap idris_infixes get
385 return . elem (str n) . map (\ (Fix _ op) -> op) $ fixities
386 | otherwise = return True
387 fixityOK _ = return True
389{-| Parses function options given initial options
392FnOpts ::= 'total'
393 | 'partial'
394 | 'implicit'
395 | '%' 'no_implicit'
396 | '%' 'assert_total'
397 | '%' 'error_handler'
398 | '%' 'reflection'
399 | '%' 'specialise' '[' NameTimesList? ']'
400 ;
404NameTimes ::= FnName Natural?;
408NameTimesList ::=
409 NameTimes
410 | NameTimes ',' NameTimesList
411 ;
413-}
414-- FIXME: Check compatability for function options (i.e. partal/total)
415--
416-- Issue #1574 on the issue tracker.
417-- https://github.com/idris-lang/Idris-dev/issues/1574
418fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
419fnOpts opts
420 = do reserved "total"; fnOpts (TotalFn : opts)
421 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
422 <|> do reserved "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))
423 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;
424 fnOpts (CExport c : opts)
425 <|> do try (lchar '%' *> reserved "no_implicit");
426 fnOpts (NoImplicit : opts)
427 <|> do try (lchar '%' *> reserved "inline");
428 fnOpts (Inlinable : opts)
429 <|> do try (lchar '%' *> reserved "assert_total");
430 fnOpts (AssertTotal : opts)
431 <|> do try (lchar '%' *> reserved "error_handler");
432 fnOpts (ErrorHandler : opts)
433 <|> do try (lchar '%' *> reserved "error_reverse");
434 fnOpts (ErrorReverse : opts)
435 <|> do try (lchar '%' *> reserved "reflection");
436 fnOpts (Reflection : opts)
437 <|> do lchar '%'; reserved "specialise";
438 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
439 fnOpts (Specialise ns : opts)
440 <|> do reserved "implicit"; fnOpts (Implicit : opts)
441 <|> return opts
442 <?> "function modifier"
443 where nameTimes :: IdrisParser (Name, Maybe Int)
444 nameTimes = do n <- fnName
445 t <- option Nothing (do reds <- natural
446 return (Just (fromInteger reds)))
447 return (n, t)
449{- | Parses a postulate
452Postulate ::=
453 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
454 ;
456-}
457postulate :: SyntaxInfo -> IdrisParser PDecl
458postulate syn = do doc <- try $ do (doc, _) <- option noDocs docComment
459 ist <- get
460 let doc' = annotCode (tryFullExpr syn ist) doc
461 pushIndent
462 reserved "postulate"
463 return doc'
464 ist <- get
465 let initOpts = if default_total ist
466 then [TotalFn]
467 else []
468 opts <- fnOpts initOpts
469 acc <- optional accessibility
470 opts' <- fnOpts opts
471 n_in <- fnName
472 let n = expandNS syn n_in
473 lchar ':'
474 ty <- typeExpr (allowImp syn)
475 fc <- getFC
476 terminator
477 addAcc n acc
478 return (PPostulate doc syn fc opts' n ty)
479 <?> "postulate"
481{- | Parses a using declaration
484Using ::=
485 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
486 ;
488 -}
489using_ :: SyntaxInfo -> IdrisParser [PDecl]
490using_ syn =
491 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
492 openBlock
493 let uvars = using syn
494 ds <- many (decl (syn { using = uvars ++ ns }))
495 closeBlock
496 return (concat ds)
497 <?> "using declaration"
499{- | Parses a parameters declaration
502Params ::=
503 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
504 ;
506 -}
507params :: SyntaxInfo -> IdrisParser [PDecl]
508params syn =
509 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
510 openBlock
511 let pvars = syn_params syn
512 ds <- many (decl syn { syn_params = pvars ++ ns })
513 closeBlock
514 fc <- getFC
515 return [PParams fc ns (concat ds)]
516 <?> "parameters declaration"
518{- | Parses a mutual declaration (for mutually recursive functions)
521Mutual ::=
522 'mutual' OpenBlock Decl* CloseBlock
523 ;
525-}
526mutual :: SyntaxInfo -> IdrisParser [PDecl]
527mutual syn =
528 do reserved "mutual"
529 openBlock
530 let pvars = syn_params syn
531 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
532 closeBlock
533 fc <- getFC
534 return [PMutual fc (concat ds)]
535 <?> "mutual block"
537{-| Parses a namespace declaration
540Namespace ::=
541 'namespace' identifier OpenBlock Decl+ CloseBlock
542 ;
544-}
545namespace :: SyntaxInfo -> IdrisParser [PDecl]
546namespace syn =
547 do reserved "namespace"; n <- identifier;
548 openBlock
549 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
550 closeBlock
551 return [PNamespace n (concat ds)]
552 <?> "namespace declaration"
554{- | Parses a methods block (for instances)
557 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
559-}
560instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
561instanceBlock syn = do reserved "where"
562 openBlock
563 ds <- many (fnDecl syn)
564 closeBlock
565 return (concat ds)
566 <?> "instance block"
568{- | Parses a methods and instances block (for type classes)
571MethodOrInstance ::=
572 FnDecl
573 | Instance
574 ;
578ClassBlock ::=
579 'where' OpenBlock MethodOrInstance* CloseBlock
580 ;
582-}
583classBlock :: SyntaxInfo -> IdrisParser [PDecl]
584classBlock syn = do reserved "where"
585 openBlock
586 ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)
587 closeBlock
588 return (concat ds)
589 <?> "class block"
591{-| Parses a type class declaration
594ClassArgument ::=
595 Name
596 | '(' Name ':' Expr ')'
597 ;
601Class ::=
602 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
603 ;
605-}
606class_ :: SyntaxInfo -> IdrisParser [PDecl]
607class_ syn = do (doc, argDocs, acc) <- try (do
608 (doc, argDocs) <- option noDocs docComment
609 ist <- get
610 let doc' = annotCode (tryFullExpr syn ist) doc
611 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
612 | (n, d) <- argDocs ]
613 acc <- optional accessibility
614 return (doc', argDocs', acc))
615 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName
616 let n = expandNS syn n_in
617 cs <- many carg
618 ds <- option [] (classBlock syn)
619 accData acc n (concatMap declared ds)
620 return [PClass doc syn fc cons n cs argDocs ds]
621 <?> "type-class declaration"
622 where
623 carg :: IdrisParser (Name, PTerm)
624 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
625 return (i, ty)
626 <|> do i <- name;
627 return (i, PType)
629{- | Parses a type class instance declaration
632 Instance ::=
633 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
634 ;
638InstanceName ::= '[' Name ']';
640-}
641instance_ :: SyntaxInfo -> IdrisParser [PDecl]
642instance_ syn = do reserved "instance"; fc <- getFC
643 en <- optional instanceName
644 cs <- constraintList syn
645 cn <- fnName
646 args <- many (simpleExpr syn)
647 let sc = PApp fc (PRef fc cn) (map pexp args)
648 let t = bindList (PPi constraint) cs sc
649 ds <- option [] (instanceBlock syn)
650 return [PInstance syn fc cs cn args t en ds]
651 <?> "instance declaration"
652 where instanceName :: IdrisParser Name
653 instanceName = do lchar '['; n_in <- fnName; lchar ']'
654 let n = expandNS syn n_in
655 return n
656 <?> "instance name"
659{- | Parses a using declaration list
662UsingDeclList ::=
663 UsingDeclList'
664 | NameList TypeSig
665 ;
669UsingDeclList' ::=
670 UsingDecl
671 | UsingDecl ',' UsingDeclList'
672 ;
676NameList ::=
677 Name
678 | Name ',' NameList
679 ;
681-}
682usingDeclList :: SyntaxInfo -> IdrisParser [Using]
683usingDeclList syn
684 = try (sepBy1 (usingDecl syn) (lchar ','))
685 <|> do ns <- sepBy1 name (lchar ',')
686 lchar ':'
687 t <- typeExpr (disallowImp syn)
688 return (map (\x -> UImplicit x t) ns)
689 <?> "using declaration list"
691{- |Parses a using declaration
694UsingDecl ::=
695 FnName TypeSig
696 | FnName FnName+
697 ;
699-}
700usingDecl :: SyntaxInfo -> IdrisParser Using
701usingDecl syn = try (do x <- fnName
702 lchar ':'
703 t <- typeExpr (disallowImp syn)
704 return (UImplicit x t))
705 <|> do c <- fnName
706 xs <- some fnName
707 return (UConstraint c xs)
708 <?> "using declaration"
710{- | Parse a clause with patterns
713Pattern ::= Clause;
715-}
716pattern :: SyntaxInfo -> IdrisParser PDecl
717pattern syn = do fc <- getFC
718 clause <- clause syn
719 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
720 <?> "pattern"
722{- | Parse a constant applicative form declaration
725CAF ::= 'let' FnName '=' Expr Terminator;
727-}
728caf :: SyntaxInfo -> IdrisParser PDecl
729caf syn = do reserved "let"
730 n_in <- fnName; let n = expandNS syn n_in
731 lchar '='
732 t <- expr syn
733 terminator
734 fc <- getFC
735 return (PCAF fc n t)
736 <?> "constant applicative form declaration"
738{- | Parse an argument expression
741ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
743-}
744argExpr :: SyntaxInfo -> IdrisParser PTerm
745argExpr syn = let syn' = syn { inPattern = True } in
746 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
747 <?> "argument expression"
749{- | Parse a right hand side of a function
752RHS ::= '=' Expr
753 | '?=' RHSName? Expr
754 | 'impossible'
755 ;
759RHSName ::= '{' FnName '}';
761-}
762rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
763rhs syn n = do lchar '='; expr syn
764 <|> do symbol "?=";
765 fc <- getFC
766 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
767 return n)
768 r <- expr syn
769 return (addLet fc name r)
770 <|> do reserved "impossible"; return PImpossible
771 <?> "function right hand side"
772 where mkN :: Name -> Name
773 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
774 then sUN "infix_op_lemma_1"
775 else sUN (str x++"_lemma_1")
776 mkN (NS x n) = NS (mkN x) n
777 n' :: Name
778 n' = mkN n
779 addLet :: FC -> Name -> PTerm -> PTerm
780 addLet fc nm (PLet fc' n ty val r) = PLet fc' n ty val (addLet fc nm r)
781 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
782 where addLetC (l, r) = (l, addLet fc nm r)
783 addLet fc nm r = (PLet fc (sUN "value") Placeholder r (PMetavar nm))
785{- |Parses a function clause
788RHSOrWithBlock ::= RHS WhereOrTerminator
789 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
790 ;
794Clause ::= WExpr+ RHSOrWithBlock
795 | SimpleExpr '<==' FnName RHS WhereOrTerminator
796 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
797 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
798 ;
802ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
806WhereOrTerminator ::= WhereBlock | Terminator;
808-}
809clause :: SyntaxInfo -> IdrisParser PClause
810clause syn
811 = do wargs <- try (do pushIndent; some (wExpr syn))
812 fc <- getFC
813 ist <- get
814 n <- case lastParse ist of
815 Just t -> return t
816 Nothing -> fail "Invalid clause"
817 (do r <- rhs syn n
818 let ctxt = tt_ctxt ist
819 let wsyn = syn { syn_namespace = [] }
820 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
821 popIndent
822 return x,
823 do terminator
824 return ([], [])]
825 return $ PClauseR fc wargs r wheres) <|> (do
826 popIndent
827 reserved "with"
828 wval <- simpleExpr syn
829 pn <- optProof
830 openBlock
831 ds <- some $ fnDecl syn
832 let withs = concat ds
833 closeBlock
834 return $ PWithR fc wargs wval pn withs)
835 <|> do ty <- try (do pushIndent
836 ty <- simpleExpr syn
837 symbol "<=="
838 return ty)
839 fc <- getFC
840 n_in <- fnName; let n = expandNS syn n_in
841 r <- rhs syn n
842 ist <- get
843 let ctxt = tt_ctxt ist
844 let wsyn = syn { syn_namespace = [] }
845 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
846 popIndent
847 return x,
848 do terminator
849 return ([], [])]
850 let capp = PLet fc (sMN 0 "match")
851 ty
852 (PMatchApp fc n)
853 (PRef fc (sMN 0 "match"))
854 ist <- get
855 put (ist { lastParse = Just n })
856 return $ PClause fc n capp [] r wheres
857 <|> do (l, op) <- try (do
858 pushIndent
859 l <- argExpr syn
860 op <- operator
861 when (op == "=" || op == "?=" ) $
862 fail "infix clause definition with \"=\" and \"?=\" not supported "
863 return (l, op))
864 let n = expandNS syn (sUN op)
865 r <- argExpr syn
866 fc <- getFC
867 wargs <- many (wExpr syn)
868 (do rs <- rhs syn n
869 let wsyn = syn { syn_namespace = [] }
870 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
871 popIndent
872 return x,
873 do terminator
874 return ([], [])]
875 ist <- get
876 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
877 put (ist { lastParse = Just n })
878 return $ PClause fc n capp wargs rs wheres) <|> (do
879 popIndent
880 reserved "with"
881 wval <- bracketed syn
882 pn <- optProof
883 openBlock
884 ds <- some $ fnDecl syn
885 closeBlock
886 ist <- get
887 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
888 let withs = map (fillLHSD n capp wargs) $ concat ds
889 put (ist { lastParse = Just n })
890 return $ PWith fc n capp wargs wval pn withs)
891 <|> do pushIndent
892 n_in <- fnName; let n = expandNS syn n_in
893 cargs <- many (constraintArg syn)
894 fc <- getFC
895 args <- many (try (implicitArg (syn { inPattern = True } ))
896 <|> (fmap pexp (argExpr syn)))
897 wargs <- many (wExpr syn)
898 let capp = PApp fc (PRef fc n)
899 (cargs ++ args)
900 (do r <- rhs syn n
901 ist <- get
902 let ctxt = tt_ctxt ist
903 let wsyn = syn { syn_namespace = [] }
904 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
905 popIndent
906 return x,
907 do terminator
908 return ([], [])]
909 ist <- get
910 put (ist { lastParse = Just n })
911 return $ PClause fc n capp wargs r wheres) <|> (do
912 reserved "with"
913 ist <- get
914 put (ist { lastParse = Just n })
915 wval <- bracketed syn
916 pn <- optProof
917 openBlock
918 ds <- some $ fnDecl syn
919 let withs = map (fillLHSD n capp wargs) $ concat ds
920 closeBlock
921 popIndent
922 return $ PWith fc n capp wargs wval pn withs)
923 <?> "function clause"
924 where
925 optProof = option Nothing (do reserved "proof"
926 n <- fnName
927 return (Just n))
929 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
930 fillLHS n capp owargs (PClauseR fc wargs v ws)
931 = PClause fc n capp (owargs ++ wargs) v ws
932 fillLHS n capp owargs (PWithR fc wargs v pn ws)
933 = PWith fc n capp (owargs ++ wargs) v pn
934 (map (fillLHSD n capp (owargs ++ wargs)) ws)
935 fillLHS _ _ _ c = c
937 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
938 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
939 fillLHSD n c a x = x
941{-| Parses with pattern
944WExpr ::= '|' Expr';
946-}
947wExpr :: SyntaxInfo -> IdrisParser PTerm
948wExpr syn = do lchar '|'
949 expr' (syn { inPattern = True })
950 <?> "with pattern"
952{- | Parses a where block
955WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
957-}
958whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
959whereBlock n syn
960 = do reserved "where"
961 ds <- indentedBlock1 (decl syn)
962 let dns = concatMap (concatMap declared) ds
963 return (concat ds, map (\x -> (x, decoration syn x)) dns)
964 <?> "where block"
966{- |Parses a code generation target language name
969Codegen ::= 'C'
970 | 'Java'
971 | 'JavaScript'
972 | 'Node'
973 | 'LLVM'
974 | 'Bytecode'
975 ;
977-}
978codegen_ :: IdrisParser Codegen
979codegen_ = do n <- identifier; return (Via (map toLower n))
980 <|> do reserved "Bytecode"; return Bytecode
981 <?> "code generation language"
983{- |Parses a compiler directive
985StringList ::=
986 String
987 | String ',' StringList
988 ;
992Directive ::= '%' Directive';
996Directive' ::= 'lib' CodeGen String_t
997 | 'link' CodeGen String_t
998 | 'flag' CodeGen String_t
999 | 'include' CodeGen String_t
1000 | 'hide' Name
1001 | 'freeze' Name
1002 | 'access' Accessibility
1003 | 'default' Totality
1004 | 'logging' Natural
1005 | 'dynamic' StringList
1006 | 'name' Name NameList
1007 | 'error_handlers' Name NameList
1008 | 'language' 'TypeProviders'
1009 | 'language' 'ErrorReflection'
1013directive :: SyntaxInfo -> IdrisParser [PDecl]
1014directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
1015 return [PDirective (do addLib cgn lib
1016 addIBC (IBCLib cgn lib))]
1017 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
1018 return [PDirective (do dirs <- allImportDirs
1019 o <- liftIO $ findInPath dirs obj
1020 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
1021 addObjectFile cgn o)]
1022 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
1023 flag <- stringLiteral
1024 return [PDirective (do addIBC (IBCCGFlag cgn flag)
1025 addFlag cgn flag)]
1026 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
1027 return [PDirective (do addHdr cgn hdr
1028 addIBC (IBCHeader cgn hdr))]
1029 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
1030 return [PDirective (do setAccessibility n Hidden
1031 addIBC (IBCAccess n Hidden))]
1032 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
1033 return [PDirective (do setAccessibility n Frozen
1034 addIBC (IBCAccess n Frozen))]
1035 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1036 return [PDirective (do i <- get
1037 put(i { default_access = acc }))]
1038 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1039 i <- get
1040 put (i { default_total = tot } )
1041 return [PDirective (do i <- get
1042 put(i { default_total = tot }))]
1043 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
1044 return [PDirective (setLogLevel (fromInteger i))]
1045 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
1046 return [PDirective (do added <- addDyLib libs
1047 case added of
1048 Left lib -> addIBC (IBCDyLib (lib_name lib))
1049 Right msg ->
1050 fail $ msg)]
1051 <|> do try (lchar '%' *> reserved "name")
1052 ty <- fnName
1053 ns <- sepBy1 name (lchar ',')
1054 return [PDirective (do ty' <- disambiguate ty
1055 mapM_ (addNameHint ty') ns
1056 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1057 <|> do try (lchar '%' *> reserved "error_handlers")
1058 fn <- fnName
1059 arg <- fnName
1060 ns <- sepBy1 name (lchar ',')
1061 return [PDirective (do fn' <- disambiguate fn
1062 ns' <- mapM disambiguate ns
1063 addFunctionErrorHandlers fn' arg ns'
1064 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]
1065 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1066 return [PDirective (addLangExt ext)]
1067 <|> do fc <- getFC
1068 try (lchar '%' *> reserved "used")
1069 fn <- fnName
1070 arg <- iName []
1071 return [PDirective (addUsedName fc fn arg)]
1073 <?> "directive"
1074 where disambiguate :: Name -> Idris Name
1075 disambiguate n = do i <- getIState
1076 case lookupCtxtName n (idris_implicits i) of
1077 [(n', _)] -> return n'
1078 [] -> throwError (NoSuchVariable n)
1079 more -> throwError (CantResolveAlts (map fst more))
1081pLangExt :: IdrisParser LanguageExt
1082pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1083 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1085{- | Parses a totality
1088Totality ::= 'partial' | 'total'
1092totality :: IdrisParser Bool
1093totality
1094 = do reserved "total"; return True
1095 <|> do reserved "partial"; return False
1097{- | Parses a type provider
1100Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1101ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1103 -}
1104provider :: SyntaxInfo -> IdrisParser [PDecl]
1105provider syn = do try (lchar '%' *> reserved "provide");
1106 provideTerm <|> providePostulate
1107 <?> "type provider"
1108 where provideTerm = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1109 fc <- getFC
1110 reserved "with"
1111 e <- expr syn <?> "provider expression"
1112 return [PProvider syn fc (ProvTerm t e) n]
1113 providePostulate = do reserved "postulate"
1114 n <- fnName
1115 fc <- getFC
1116 reserved "with"
1117 e <- expr syn <?> "provider expression"
1118 return [PProvider syn fc (ProvPostulate e) n]
1120{- | Parses a transform
1123Transform ::= '%' 'transform' Expr '==>' Expr
1126transform :: SyntaxInfo -> IdrisParser [PDecl]
1127transform syn = do try (lchar '%' *> reserved "transform")
1128 -- leave it unchecked, until we work out what this should
1129 -- actually mean...
1130-- safety <- option True (do reserved "unsafe"
1131-- return False)
1132 l <- expr syn
1133 fc <- getFC
1134 symbol "==>"
1135 r <- expr syn
1136 return [PTransform fc False l r]
1137 <?> "transform"
1140{- * Loading and parsing -}
1141{- | Parses an expression from input -}
1142parseExpr :: IState -> String -> Result PTerm
1143parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1145{- | Parses a constant form input -}
1146parseConst :: IState -> String -> Result Const
1147parseConst st = runparser constant st "(input)"
1149{- | Parses a tactic from input -}
1150parseTactic :: IState -> String -> Result PTactic
1151parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1153-- | Parse module header and imports
1154parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta)
1155parseImports fname input
1156 = do i <- getIState
1157 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1158 Failure err -> fail (show err)
1159 Success (x, i) -> do putIState i
1160 return x
1161 where imports :: IdrisParser ((Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta), IState)
1162 imports = do whiteSpace
1163 (mdoc, mname) <- moduleHeader
1164 ps <- many import_
1165 mrk <- mark
1166 isEof <- lookAheadMatches eof
1167 let mrk' = if isEof
1168 then Nothing
1169 else Just mrk
1170 i <- get
1171 return ((mdoc, mname, ps, mrk'), i)
1173-- | There should be a better way of doing this...
1174findFC :: Doc -> (FC, String)
1175findFC x = let s = show (plain x) in
1176 case span (/= ':') s of
1177 (failname, ':':rest) -> case span isDigit rest of
1178 (line, ':':rest') -> case span isDigit rest' of
1179 (col, ':':msg) -> let pos = (read line, read col) in
1180 (FC failname pos pos, msg)
1182-- | Check if the coloring matches the options and corrects if necessary
1183fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1184fixColour False doc = ANSI.plain doc
1185fixColour True doc = doc
1187-- | A program is a list of declarations, possibly with associated
1188-- documentation strings.
1189parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1190 Idris [PDecl]
1191parseProg syn fname input mrk
1192 = do i <- getIState
1193 case runparser mainProg i fname input of
1194 Failure doc -> do -- FIXME: Get error location from trifecta
1195 -- this can't be the solution!
1196 -- Issue #1575 on the issue tracker.
1197 -- https://github.com/idris-lang/Idris-dev/issues/1575
1198 let (fc, msg) = findFC doc
1199 i <- getIState
1200 case idris_outputmode i of
1201 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1202 IdeMode n h -> iWarn fc (P.text msg)
1203 putIState (i { errSpan = Just fc })
1204 return []
1205 Success (x, i) -> do putIState i
1206 reportParserWarnings
1207 return $ collect x
1208 where mainProg :: IdrisParser ([PDecl], IState)
1209 mainProg = case mrk of
1210 Nothing -> do i <- get; return ([], i)
1211 Just mrk -> do
1212 release mrk
1213 ds <- prog syn
1214 i' <- get
1215 return (ds, i')
1217{- | Load idris module and show error if something wrong happens -}
1218loadModule :: FilePath -> Idris (Maybe String)
1219loadModule f
1220 = idrisCatch (loadModule' f)
1221 (\e -> do setErrSpan (getErrSpan e)
1222 ist <- getIState
1223 iWarn (getErrSpan e) $ pprintErr ist e
1224 return Nothing)
1226{- | Load idris module -}
1227loadModule' :: FilePath -> Idris (Maybe String)
1228loadModule' f
1229 = do i <- getIState
1230 let file = takeWhile (/= ' ') f
1231 ibcsd <- valIBCSubDir i
1232 ids <- allImportDirs
1233 fp <- findImport ids ibcsd file
1234 if file `elem` imported i
1235 then do iLOG $ "Already read " ++ file
1236 return Nothing
1237 else do putIState (i { imported = file : imported i })
1238 case fp of
1239 IDR fn -> loadSource False fn Nothing
1240 LIDR fn -> loadSource True fn Nothing
1241 IBC fn src ->
1242 idrisCatch (loadIBC True fn)
1243 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1244 case src of
1245 IDR sfn -> loadSource False sfn Nothing
1246 LIDR sfn -> loadSource True sfn Nothing)
1247 return $ Just file
1249{- | Load idris code from file -}
1250loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()
1251loadFromIFile reexp i@(IBC fn src) maxline
1252 = do iLOG $ "Skipping " ++ getSrcFile i
1253 idrisCatch (loadIBC reexp fn)
1254 (\err -> ierror $ LoadingFailed fn err)
1255 where
1256 getSrcFile (IDR fn) = fn
1257 getSrcFile (LIDR fn) = fn
1258 getSrcFile (IBC f src) = getSrcFile src
1260loadFromIFile _ (IDR fn) maxline = loadSource' False fn maxline
1261loadFromIFile _ (LIDR fn) maxline = loadSource' True fn maxline
1263{-| Load idris source code and show error if something wrong happens -}
1264loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1265loadSource' lidr r maxline
1266 = idrisCatch (loadSource lidr r maxline)
1267 (\e -> do setErrSpan (getErrSpan e)
1268 ist <- getIState
1269 case e of
1270 At f e' -> iWarn f (pprintErr ist e')
1271 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1273{- | Load Idris source code-}
1274loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1275loadSource lidr f toline
1276 = do iLOG ("Reading " ++ f)
1277 i <- getIState
1278 let def_total = default_total i
1279 file_in <- runIO $ readFile f
1280 file <- if lidr then tclift $ unlit f file_in else return file_in
1281 (mdocs, mname, imports_in, pos) <- parseImports f file
1282 ai <- getAutoImports
1283 let imports = map (\n -> (True, n, Just n, emptyFC)) ai ++ imports_in
1284 ids <- allImportDirs
1285 ibcsd <- valIBCSubDir i
1286 mapM_ (\(re, f) ->
1287 do fp <- findImport ids ibcsd f
1288 case fp of
1289 LIDR fn -> ifail $ "No ibc for " ++ f
1290 IDR fn -> ifail $ "No ibc for " ++ f
1291 IBC fn src -> loadIBC True fn)
1292 [(re, fn) | (re, fn, _, _) <- imports]
1293 reportParserWarnings
1295 -- process and check module aliases
1296 let modAliases = M.fromList
1297 [(prep alias, prep realName) | (reexport, realName, Just alias, fc) <- imports]
1298 prep = map T.pack . reverse . Spl.splitOn "/"
1299 aliasNames = [(alias, fc) | (_, _, Just alias, fc) <- imports]
1300 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1301 case map head . filter ((/= 1) . length) $ histogram of
1302 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1303 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1305 i <- getIState
1306 putIState (i { default_access = Hidden, module_aliases = modAliases })
1307 clearIBC -- start a new .ibc file
1308 -- record package info in .ibc
1309 imps <- allImportDirs
1310 mapM_ addIBC (map IBCImportDir imps)
1311 mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports]
1312 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1313 maxline = toline }
1314 ds' <- parseProg syntax f file pos
1316 -- Parsing done, now process declarations
1318 let ds = namespaces mname ds'
1319 logLvl 3 (show $ showDecls verbosePPOption ds)
1320 i <- getIState
1321 logLvl 10 (show (toAlist (idris_implicits i)))
1322 logLvl 3 (show (idris_infixes i))
1323 -- Now add all the declarations to the context
1324 v <- verbose
1325 when v $ iputStrLn $ "Type checking " ++ f
1326 -- we totality check after every Mutual block, so if
1327 -- anything is a single definition, wrap it in a
1328 -- mutual block on its own
1329 elabDecls toplevel (map toMutual ds)
1330 i <- getIState
1331 -- simplify every definition do give the totality checker
1332 -- a better chance
1333 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1334 updateContext (simplifyCasedef n $ getErasureInfo i))
1335 (map snd (idris_totcheck i))
1336 -- build size change graph from simplified definitions
1337 iLOG "Totality checking"
1338 i <- getIState
1339 mapM_ buildSCG (idris_totcheck i)
1340 mapM_ checkDeclTotality (idris_totcheck i)
1342 -- Redo totality check for deferred names
1343 let deftots = idris_defertotcheck i
1344 iLOG $ "Totality checking " ++ show deftots
1345 mapM_ (\x -> do tot <- getTotality x
1346 case tot of
1347 Total _ -> setTotality x Unchecked
1348 _ -> return ()) (map snd deftots)
1349 mapM_ buildSCG deftots
1350 mapM_ checkDeclTotality deftots
1352 iLOG ("Finished " ++ f)
1353 ibcsd <- valIBCSubDir i
1354 iLOG "Universe checking"
1355 iucheck
1356 let ibc = ibcPathNoFallback ibcsd f
1357 i <- getIState
1358 addHides (hide_list i)
1360 -- Save module documentation if applicable
1361 i <- getIState
1362 case mdocs of
1363 Nothing -> return ()
1364 Just docs -> addModDoc syntax mname docs
1367 -- Finally, write an ibc if checking was successful
1368 ok <- noErrors
1369 when ok $
1370 idrisCatch (do writeIBC f ibc; clearIBC)
1371 (\c -> return ()) -- failure is harmless
1372 i <- getIState
1373 putIState (i { default_total = def_total,
1374 hide_list = [] })
1375 return ()
1376 where
1377 namespaces :: [String] -> [PDecl] -> [PDecl]
1378 namespaces [] ds = ds
1379 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1381 toMutual :: PDecl -> PDecl
1382 toMutual m@(PMutual _ d) = m
1383 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1384 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1385 case x of
1386 PClauses _ _ _ _ -> r
1387 PClass _ _ _ _ _ _ _ _ -> r
1388 PInstance _ _ _ _ _ _ _ _ -> r
1389 _ -> x
1391 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1392 addModDoc syn mname docs =
1393 do ist <- getIState
1394 docs' <- elabDocTerms recinfo (parsedDocs ist)
1395 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1396 putIState ist { idris_moduledocs = modDocs' }
1397 addIBC (IBCModDocs docName)
1398 where
1399 docName = NS modDocName (map T.pack (reverse mname))
1400 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1402{- | Adds names to hide list -}
1403addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1404addHides xs = do i <- getIState
1405 let defh = default_access i
1406 let (hs, as) = partition isNothing xs
1407 unless (null as) $
1408 mapM_ doHide
1409 (map (\ (n, _) -> (n, defh)) hs ++
1410 map (\ (n, Just a) -> (n, a)) as)
1411 where isNothing (_, Nothing) = True
1412 isNothing _ = False
1414 doHide (n, a) = do setAccessibility n a
1415 addIBC (IBCAccess n a)