git.iko.soy/Idris-dev
on 7e43af7 help sign in
Idris-dev/src/Idris/Parser.hs
1447 lines 52 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, Err)
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 ::= DocComment_t? '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 -- Can't parse a full expression followed by operator like characters due to ambiguity
295 mkSimple' (Expr e : Symbol s : es)
296 | takeWhile (`elem` opChars) ts /= "" && ts `notElem` invalidOperators = SimpleExpr e : Symbol s : mkSimple' es
297 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s
298 mkSimple' (e : es) = e : mkSimple' es
299 mkSimple' [] = []
302{- | Parses a syntax symbol (either binding variable, keyword or expression)
305SyntaxSym ::= '[' Name_t ']'
306 | '{' Name_t '}'
307 | Name_t
308 | StringLiteral_t
309 ;
311 -}
312syntaxSym :: IdrisParser SSymbol
313syntaxSym = try (do lchar '['; n <- name; lchar ']'
314 return (Expr n))
315 <|> try (do lchar '{'; n <- name; lchar '}'
316 return (Binding n))
317 <|> do n <- iName []
318 return (Keyword n)
319 <|> do sym <- stringLiteral
320 return (Symbol sym)
321 <?> "syntax symbol"
323{- | Parses a function declaration with possible syntax sugar
326 FunDecl ::= FunDecl';
328-}
329fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
330fnDecl syn = try (do notEndBlock
331 d <- fnDecl' syn
332 i <- get
333 let d' = fmap (desugar syn i) d
334 return [d']) <?> "function declaration"
336{-| Parses a function declaration
339 FunDecl' ::=
340 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
341 | Postulate
342 | Pattern
343 | CAF
344 ;
346-}
347fnDecl' :: SyntaxInfo -> IdrisParser PDecl
348fnDecl' syn = checkFixity $
349 do (doc, argDocs, fc, opts', n, acc) <- try (do
350 pushIndent
351 (doc, argDocs) <- docstring syn
352 ist <- get
353 let 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, _) <- docstring syn
459 pushIndent
460 reserved "postulate"
461 return doc
462 ist <- get
463 let initOpts = if default_total ist
464 then [TotalFn]
465 else []
466 opts <- fnOpts initOpts
467 acc <- optional accessibility
468 opts' <- fnOpts opts
469 n_in <- fnName
470 let n = expandNS syn n_in
471 lchar ':'
472 ty <- typeExpr (allowImp syn)
473 fc <- getFC
474 terminator
475 addAcc n acc
476 return (PPostulate doc syn fc opts' n ty)
477 <?> "postulate"
479{- | Parses a using declaration
482Using ::=
483 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
484 ;
486 -}
487using_ :: SyntaxInfo -> IdrisParser [PDecl]
488using_ syn =
489 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
490 openBlock
491 let uvars = using syn
492 ds <- many (decl (syn { using = uvars ++ ns }))
493 closeBlock
494 return (concat ds)
495 <?> "using declaration"
497{- | Parses a parameters declaration
500Params ::=
501 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
502 ;
504 -}
505params :: SyntaxInfo -> IdrisParser [PDecl]
506params syn =
507 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
508 openBlock
509 let pvars = syn_params syn
510 ds <- many (decl syn { syn_params = pvars ++ ns })
511 closeBlock
512 fc <- getFC
513 return [PParams fc ns (concat ds)]
514 <?> "parameters declaration"
516{- | Parses a mutual declaration (for mutually recursive functions)
519Mutual ::=
520 'mutual' OpenBlock Decl* CloseBlock
521 ;
523-}
524mutual :: SyntaxInfo -> IdrisParser [PDecl]
525mutual syn =
526 do reserved "mutual"
527 openBlock
528 let pvars = syn_params syn
529 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
530 closeBlock
531 fc <- getFC
532 return [PMutual fc (concat ds)]
533 <?> "mutual block"
535{-| Parses a namespace declaration
538Namespace ::=
539 'namespace' identifier OpenBlock Decl+ CloseBlock
540 ;
542-}
543namespace :: SyntaxInfo -> IdrisParser [PDecl]
544namespace syn =
545 do reserved "namespace"; n <- identifier;
546 openBlock
547 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
548 closeBlock
549 return [PNamespace n (concat ds)]
550 <?> "namespace declaration"
552{- | Parses a methods block (for instances)
555 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
557-}
558instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
559instanceBlock syn = do reserved "where"
560 openBlock
561 ds <- many (fnDecl syn)
562 closeBlock
563 return (concat ds)
564 <?> "instance block"
566{- | Parses a methods and instances block (for type classes)
569MethodOrInstance ::=
570 FnDecl
571 | Instance
572 ;
576ClassBlock ::=
577 'where' OpenBlock MethodOrInstance* CloseBlock
578 ;
580-}
581classBlock :: SyntaxInfo -> IdrisParser [PDecl]
582classBlock syn = do reserved "where"
583 openBlock
584 ds <- many (notEndBlock >> instance_ syn <|> fnDecl syn)
585 closeBlock
586 return (concat ds)
587 <?> "class block"
589{-| Parses a type class declaration
592ClassArgument ::=
593 Name
594 | '(' Name ':' Expr ')'
595 ;
599Class ::=
600 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
601 ;
603-}
604class_ :: SyntaxInfo -> IdrisParser [PDecl]
605class_ syn = do (doc, argDocs, acc)
606 <- try (do (doc, argDocs) <- docstring syn
607 acc <- optional accessibility
608 reserved "class"
609 return (doc, argDocs, acc))
610 fc <- getFC
611 cons <- constraintList syn
612 n_in <- fnName
613 let n = expandNS syn n_in
614 cs <- many carg
615 ds <- option [] (classBlock syn)
616 accData acc n (concatMap declared ds)
617 return [PClass doc syn fc cons n cs argDocs ds]
618 <?> "type-class declaration"
619 where
620 carg :: IdrisParser (Name, PTerm)
621 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
622 return (i, ty)
623 <|> do i <- name;
624 return (i, PType)
626{- | Parses a type class instance declaration
629 Instance ::=
630 DocComment_t? 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
631 ;
635InstanceName ::= '[' Name ']';
637-}
638instance_ :: SyntaxInfo -> IdrisParser [PDecl]
639instance_ syn = do (doc, argDocs)
640 <- try (docstring syn <* reserved "instance")
641 fc <- getFC
642 en <- optional instanceName
643 cs <- constraintList syn
644 cn <- fnName
645 args <- many (simpleExpr syn)
646 let sc = PApp fc (PRef fc cn) (map pexp args)
647 let t = bindList (PPi constraint) cs sc
648 ds <- option [] (instanceBlock syn)
649 return [PInstance doc argDocs syn fc cs cn args t en ds]
650 <?> "instance declaration"
651 where instanceName :: IdrisParser Name
652 instanceName = do lchar '['; n_in <- fnName; lchar ']'
653 let n = expandNS syn n_in
654 return n
655 <?> "instance name"
658-- | Parse a docstring
659docstring :: SyntaxInfo
660 -> IdrisParser (Docstring (Either Err PTerm),
661 [(Name,Docstring (Either Err PTerm))])
662docstring syn = do (doc, argDocs) <- option noDocs docComment
663 ist <- get
664 let doc' = annotCode (tryFullExpr syn ist) doc
665 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
666 | (n, d) <- argDocs ]
667 return (doc', argDocs')
670{- | Parses a using declaration list
673UsingDeclList ::=
674 UsingDeclList'
675 | NameList TypeSig
676 ;
680UsingDeclList' ::=
681 UsingDecl
682 | UsingDecl ',' UsingDeclList'
683 ;
687NameList ::=
688 Name
689 | Name ',' NameList
690 ;
692-}
693usingDeclList :: SyntaxInfo -> IdrisParser [Using]
694usingDeclList syn
695 = try (sepBy1 (usingDecl syn) (lchar ','))
696 <|> do ns <- sepBy1 name (lchar ',')
697 lchar ':'
698 t <- typeExpr (disallowImp syn)
699 return (map (\x -> UImplicit x t) ns)
700 <?> "using declaration list"
702{- |Parses a using declaration
705UsingDecl ::=
706 FnName TypeSig
707 | FnName FnName+
708 ;
710-}
711usingDecl :: SyntaxInfo -> IdrisParser Using
712usingDecl syn = try (do x <- fnName
713 lchar ':'
714 t <- typeExpr (disallowImp syn)
715 return (UImplicit x t))
716 <|> do c <- fnName
717 xs <- some fnName
718 return (UConstraint c xs)
719 <?> "using declaration"
721{- | Parse a clause with patterns
724Pattern ::= Clause;
726-}
727pattern :: SyntaxInfo -> IdrisParser PDecl
728pattern syn = do fc <- getFC
729 clause <- clause syn
730 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
731 <?> "pattern"
733{- | Parse a constant applicative form declaration
736CAF ::= 'let' FnName '=' Expr Terminator;
738-}
739caf :: SyntaxInfo -> IdrisParser PDecl
740caf syn = do reserved "let"
741 n_in <- fnName; let n = expandNS syn n_in
742 lchar '='
743 t <- expr syn
744 terminator
745 fc <- getFC
746 return (PCAF fc n t)
747 <?> "constant applicative form declaration"
749{- | Parse an argument expression
752ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
754-}
755argExpr :: SyntaxInfo -> IdrisParser PTerm
756argExpr syn = let syn' = syn { inPattern = True } in
757 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
758 <?> "argument expression"
760{- | Parse a right hand side of a function
763RHS ::= '=' Expr
764 | '?=' RHSName? Expr
765 | 'impossible'
766 ;
770RHSName ::= '{' FnName '}';
772-}
773rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
774rhs syn n = do lchar '='; expr syn
775 <|> do symbol "?=";
776 fc <- getFC
777 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
778 return n)
779 r <- expr syn
780 return (addLet fc name r)
781 <|> do reserved "impossible"; return PImpossible
782 <?> "function right hand side"
783 where mkN :: Name -> Name
784 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
785 then sUN "infix_op_lemma_1"
786 else sUN (str x++"_lemma_1")
787 mkN (NS x n) = NS (mkN x) n
788 n' :: Name
789 n' = mkN n
790 addLet :: FC -> Name -> PTerm -> PTerm
791 addLet fc nm (PLet fc' n ty val r) = PLet fc' n ty val (addLet fc nm r)
792 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
793 where addLetC (l, r) = (l, addLet fc nm r)
794 addLet fc nm r = (PLet fc (sUN "value") Placeholder r (PMetavar nm))
796{- |Parses a function clause
799RHSOrWithBlock ::= RHS WhereOrTerminator
800 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
801 ;
805Clause ::= WExpr+ RHSOrWithBlock
806 | SimpleExpr '<==' FnName RHS WhereOrTerminator
807 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
808 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
809 ;
813ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
817WhereOrTerminator ::= WhereBlock | Terminator;
819-}
820clause :: SyntaxInfo -> IdrisParser PClause
821clause syn
822 = do wargs <- try (do pushIndent; some (wExpr syn))
823 fc <- getFC
824 ist <- get
825 n <- case lastParse ist of
826 Just t -> return t
827 Nothing -> fail "Invalid clause"
828 (do r <- rhs syn n
829 let ctxt = tt_ctxt ist
830 let wsyn = syn { syn_namespace = [] }
831 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
832 popIndent
833 return x,
834 do terminator
835 return ([], [])]
836 return $ PClauseR fc wargs r wheres) <|> (do
837 popIndent
838 reserved "with"
839 wval <- simpleExpr syn
840 pn <- optProof
841 openBlock
842 ds <- some $ fnDecl syn
843 let withs = concat ds
844 closeBlock
845 return $ PWithR fc wargs wval pn withs)
846 <|> do ty <- try (do pushIndent
847 ty <- simpleExpr syn
848 symbol "<=="
849 return ty)
850 fc <- getFC
851 n_in <- fnName; let n = expandNS syn n_in
852 r <- rhs syn n
853 ist <- get
854 let ctxt = tt_ctxt ist
855 let wsyn = syn { syn_namespace = [] }
856 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
857 popIndent
858 return x,
859 do terminator
860 return ([], [])]
861 let capp = PLet fc (sMN 0 "match")
862 ty
863 (PMatchApp fc n)
864 (PRef fc (sMN 0 "match"))
865 ist <- get
866 put (ist { lastParse = Just n })
867 return $ PClause fc n capp [] r wheres
868 <|> do (l, op) <- try (do
869 pushIndent
870 l <- argExpr syn
871 op <- operator
872 when (op == "=" || op == "?=" ) $
873 fail "infix clause definition with \"=\" and \"?=\" not supported "
874 return (l, op))
875 let n = expandNS syn (sUN op)
876 r <- argExpr syn
877 fc <- getFC
878 wargs <- many (wExpr syn)
879 (do rs <- rhs syn n
880 let wsyn = syn { syn_namespace = [] }
881 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
882 popIndent
883 return x,
884 do terminator
885 return ([], [])]
886 ist <- get
887 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
888 put (ist { lastParse = Just n })
889 return $ PClause fc n capp wargs rs wheres) <|> (do
890 popIndent
891 reserved "with"
892 wval <- bracketed syn
893 pn <- optProof
894 openBlock
895 ds <- some $ fnDecl syn
896 closeBlock
897 ist <- get
898 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
899 let withs = map (fillLHSD n capp wargs) $ concat ds
900 put (ist { lastParse = Just n })
901 return $ PWith fc n capp wargs wval pn withs)
902 <|> do pushIndent
903 n_in <- fnName; let n = expandNS syn n_in
904 cargs <- many (constraintArg syn)
905 fc <- getFC
906 args <- many (try (implicitArg (syn { inPattern = True } ))
907 <|> (fmap pexp (argExpr syn)))
908 wargs <- many (wExpr syn)
909 let capp = PApp fc (PRef fc n)
910 (cargs ++ args)
911 (do r <- rhs syn n
912 ist <- get
913 let ctxt = tt_ctxt ist
914 let wsyn = syn { syn_namespace = [] }
915 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
916 popIndent
917 return x,
918 do terminator
919 return ([], [])]
920 ist <- get
921 put (ist { lastParse = Just n })
922 return $ PClause fc n capp wargs r wheres) <|> (do
923 reserved "with"
924 ist <- get
925 put (ist { lastParse = Just n })
926 wval <- bracketed syn
927 pn <- optProof
928 openBlock
929 ds <- some $ fnDecl syn
930 let withs = map (fillLHSD n capp wargs) $ concat ds
931 closeBlock
932 popIndent
933 return $ PWith fc n capp wargs wval pn withs)
934 <?> "function clause"
935 where
936 optProof = option Nothing (do reserved "proof"
937 n <- fnName
938 return (Just n))
940 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
941 fillLHS n capp owargs (PClauseR fc wargs v ws)
942 = PClause fc n capp (owargs ++ wargs) v ws
943 fillLHS n capp owargs (PWithR fc wargs v pn ws)
944 = PWith fc n capp (owargs ++ wargs) v pn
945 (map (fillLHSD n capp (owargs ++ wargs)) ws)
946 fillLHS _ _ _ c = c
948 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
949 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
950 fillLHSD n c a x = x
952{-| Parses with pattern
955WExpr ::= '|' Expr';
957-}
958wExpr :: SyntaxInfo -> IdrisParser PTerm
959wExpr syn = do lchar '|'
960 expr' (syn { inPattern = True })
961 <?> "with pattern"
963{- | Parses a where block
966WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
968-}
969whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
970whereBlock n syn
971 = do reserved "where"
972 ds <- indentedBlock1 (decl syn)
973 let dns = concatMap (concatMap declared) ds
974 return (concat ds, map (\x -> (x, decoration syn x)) dns)
975 <?> "where block"
977{- |Parses a code generation target language name
980Codegen ::= 'C'
981 | 'Java'
982 | 'JavaScript'
983 | 'Node'
984 | 'LLVM'
985 | 'Bytecode'
986 ;
988-}
989codegen_ :: IdrisParser Codegen
990codegen_ = do n <- identifier; return (Via (map toLower n))
991 <|> do reserved "Bytecode"; return Bytecode
992 <?> "code generation language"
994{- |Parses a compiler directive
996StringList ::=
997 String
998 | String ',' StringList
999 ;
1003Directive ::= '%' Directive';
1007Directive' ::= 'lib' CodeGen String_t
1008 | 'link' CodeGen String_t
1009 | 'flag' CodeGen String_t
1010 | 'include' CodeGen String_t
1011 | 'hide' Name
1012 | 'freeze' Name
1013 | 'access' Accessibility
1014 | 'default' Totality
1015 | 'logging' Natural
1016 | 'dynamic' StringList
1017 | 'name' Name NameList
1018 | 'error_handlers' Name NameList
1019 | 'language' 'TypeProviders'
1020 | 'language' 'ErrorReflection'
1024directive :: SyntaxInfo -> IdrisParser [PDecl]
1025directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
1026 return [PDirective (do addLib cgn lib
1027 addIBC (IBCLib cgn lib))]
1028 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
1029 return [PDirective (do dirs <- allImportDirs
1030 o <- liftIO $ findInPath dirs obj
1031 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
1032 addObjectFile cgn o)]
1033 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
1034 flag <- stringLiteral
1035 return [PDirective (do addIBC (IBCCGFlag cgn flag)
1036 addFlag cgn flag)]
1037 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
1038 return [PDirective (do addHdr cgn hdr
1039 addIBC (IBCHeader cgn hdr))]
1040 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
1041 return [PDirective (do setAccessibility n Hidden
1042 addIBC (IBCAccess n Hidden))]
1043 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
1044 return [PDirective (do setAccessibility n Frozen
1045 addIBC (IBCAccess n Frozen))]
1046 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1047 return [PDirective (do i <- get
1048 put(i { default_access = acc }))]
1049 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1050 i <- get
1051 put (i { default_total = tot } )
1052 return [PDirective (do i <- get
1053 put(i { default_total = tot }))]
1054 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
1055 return [PDirective (setLogLevel (fromInteger i))]
1056 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
1057 return [PDirective (do added <- addDyLib libs
1058 case added of
1059 Left lib -> addIBC (IBCDyLib (lib_name lib))
1060 Right msg ->
1061 fail $ msg)]
1062 <|> do try (lchar '%' *> reserved "name")
1063 ty <- fnName
1064 ns <- sepBy1 name (lchar ',')
1065 return [PDirective (do ty' <- disambiguate ty
1066 mapM_ (addNameHint ty') ns
1067 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1068 <|> do try (lchar '%' *> reserved "error_handlers")
1069 fn <- fnName
1070 arg <- fnName
1071 ns <- sepBy1 name (lchar ',')
1072 return [PDirective (do fn' <- disambiguate fn
1073 ns' <- mapM disambiguate ns
1074 addFunctionErrorHandlers fn' arg ns'
1075 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]
1076 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1077 return [PDirective (addLangExt ext)]
1078 <|> do fc <- getFC
1079 try (lchar '%' *> reserved "used")
1080 fn <- fnName
1081 arg <- iName []
1082 return [PDirective (addUsedName fc fn arg)]
1084 <?> "directive"
1085 where disambiguate :: Name -> Idris Name
1086 disambiguate n = do i <- getIState
1087 case lookupCtxtName n (idris_implicits i) of
1088 [(n', _)] -> return n'
1089 [] -> throwError (NoSuchVariable n)
1090 more -> throwError (CantResolveAlts (map fst more))
1092pLangExt :: IdrisParser LanguageExt
1093pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1094 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1096{- | Parses a totality
1099Totality ::= 'partial' | 'total'
1103totality :: IdrisParser Bool
1104totality
1105 = do reserved "total"; return True
1106 <|> do reserved "partial"; return False
1108{- | Parses a type provider
1111Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1112ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1114 -}
1115provider :: SyntaxInfo -> IdrisParser [PDecl]
1116provider syn = do doc <- try (do (doc, _) <- docstring syn
1117 lchar '%'
1118 reserved "provide"
1119 return doc)
1120 provideTerm doc <|> providePostulate doc
1121 <?> "type provider"
1122 where provideTerm doc =
1123 do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1124 fc <- getFC
1125 reserved "with"
1126 e <- expr syn <?> "provider expression"
1127 return [PProvider doc syn fc (ProvTerm t e) n]
1128 providePostulate doc =
1129 do reserved "postulate"
1130 n <- fnName
1131 fc <- getFC
1132 reserved "with"
1133 e <- expr syn <?> "provider expression"
1134 return [PProvider doc syn fc (ProvPostulate e) n]
1136{- | Parses a transform
1139Transform ::= '%' 'transform' Expr '==>' Expr
1142transform :: SyntaxInfo -> IdrisParser [PDecl]
1143transform syn = do try (lchar '%' *> reserved "transform")
1144 -- leave it unchecked, until we work out what this should
1145 -- actually mean...
1146-- safety <- option True (do reserved "unsafe"
1147-- return False)
1148 l <- expr syn
1149 fc <- getFC
1150 symbol "==>"
1151 r <- expr syn
1152 return [PTransform fc False l r]
1153 <?> "transform"
1156{- * Loading and parsing -}
1157{- | Parses an expression from input -}
1158parseExpr :: IState -> String -> Result PTerm
1159parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1161{- | Parses a constant form input -}
1162parseConst :: IState -> String -> Result Const
1163parseConst st = runparser constant st "(input)"
1165{- | Parses a tactic from input -}
1166parseTactic :: IState -> String -> Result PTactic
1167parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1169-- | Parse module header and imports
1170parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta)
1171parseImports fname input
1172 = do i <- getIState
1173 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1174 Failure err -> fail (show err)
1175 Success (x, i) -> do putIState i
1176 return x
1177 where imports :: IdrisParser ((Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta), IState)
1178 imports = do whiteSpace
1179 (mdoc, mname) <- moduleHeader
1180 ps <- many import_
1181 mrk <- mark
1182 isEof <- lookAheadMatches eof
1183 let mrk' = if isEof
1184 then Nothing
1185 else Just mrk
1186 i <- get
1187 return ((mdoc, mname, ps, mrk'), i)
1189-- | There should be a better way of doing this...
1190findFC :: Doc -> (FC, String)
1191findFC x = let s = show (plain x) in
1192 case span (/= ':') s of
1193 (failname, ':':rest) -> case span isDigit rest of
1194 (line, ':':rest') -> case span isDigit rest' of
1195 (col, ':':msg) -> let pos = (read line, read col) in
1196 (FC failname pos pos, msg)
1198-- | Check if the coloring matches the options and corrects if necessary
1199fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1200fixColour False doc = ANSI.plain doc
1201fixColour True doc = doc
1203-- | A program is a list of declarations, possibly with associated
1204-- documentation strings.
1205parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1206 Idris [PDecl]
1207parseProg syn fname input mrk
1208 = do i <- getIState
1209 case runparser mainProg i fname input of
1210 Failure doc -> do -- FIXME: Get error location from trifecta
1211 -- this can't be the solution!
1212 -- Issue #1575 on the issue tracker.
1213 -- https://github.com/idris-lang/Idris-dev/issues/1575
1214 let (fc, msg) = findFC doc
1215 i <- getIState
1216 case idris_outputmode i of
1217 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1218 IdeMode n h -> iWarn fc (P.text msg)
1219 putIState (i { errSpan = Just fc })
1220 return []
1221 Success (x, i) -> do putIState i
1222 reportParserWarnings
1223 return $ collect x
1224 where mainProg :: IdrisParser ([PDecl], IState)
1225 mainProg = case mrk of
1226 Nothing -> do i <- get; return ([], i)
1227 Just mrk -> do
1228 release mrk
1229 ds <- prog syn
1230 i' <- get
1231 return (ds, i')
1233{- | Load idris module and show error if something wrong happens -}
1234loadModule :: FilePath -> Idris (Maybe String)
1235loadModule f
1236 = idrisCatch (loadModule' f)
1237 (\e -> do setErrSpan (getErrSpan e)
1238 ist <- getIState
1239 iWarn (getErrSpan e) $ pprintErr ist e
1240 return Nothing)
1242{- | Load idris module -}
1243loadModule' :: FilePath -> Idris (Maybe String)
1244loadModule' f
1245 = do i <- getIState
1246 let file = takeWhile (/= ' ') f
1247 ibcsd <- valIBCSubDir i
1248 ids <- allImportDirs
1249 fp <- findImport ids ibcsd file
1250 if file `elem` imported i
1251 then do iLOG $ "Already read " ++ file
1252 return Nothing
1253 else do putIState (i { imported = file : imported i })
1254 case fp of
1255 IDR fn -> loadSource False fn Nothing
1256 LIDR fn -> loadSource True fn Nothing
1257 IBC fn src ->
1258 idrisCatch (loadIBC True fn)
1259 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1260 case src of
1261 IDR sfn -> loadSource False sfn Nothing
1262 LIDR sfn -> loadSource True sfn Nothing)
1263 return $ Just file
1265{- | Load idris code from file -}
1266loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()
1267loadFromIFile reexp i@(IBC fn src) maxline
1268 = do iLOG $ "Skipping " ++ getSrcFile i
1269 idrisCatch (loadIBC reexp fn)
1270 (\err -> ierror $ LoadingFailed fn err)
1271 where
1272 getSrcFile (IDR fn) = fn
1273 getSrcFile (LIDR fn) = fn
1274 getSrcFile (IBC f src) = getSrcFile src
1276loadFromIFile _ (IDR fn) maxline = loadSource' False fn maxline
1277loadFromIFile _ (LIDR fn) maxline = loadSource' True fn maxline
1279{-| Load idris source code and show error if something wrong happens -}
1280loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1281loadSource' lidr r maxline
1282 = idrisCatch (loadSource lidr r maxline)
1283 (\e -> do setErrSpan (getErrSpan e)
1284 ist <- getIState
1285 case e of
1286 At f e' -> iWarn f (pprintErr ist e')
1287 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1289{- | Load Idris source code-}
1290loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1291loadSource lidr f toline
1292 = do iLOG ("Reading " ++ f)
1293 i <- getIState
1294 let def_total = default_total i
1295 file_in <- runIO $ readFile f
1296 file <- if lidr then tclift $ unlit f file_in else return file_in
1297 (mdocs, mname, imports_in, pos) <- parseImports f file
1298 ai <- getAutoImports
1299 let imports = map (\n -> (True, n, Just n, emptyFC)) ai ++ imports_in
1300 ids <- allImportDirs
1301 ibcsd <- valIBCSubDir i
1302 mapM_ (\(re, f) ->
1303 do fp <- findImport ids ibcsd f
1304 case fp of
1305 LIDR fn -> ifail $ "No ibc for " ++ f
1306 IDR fn -> ifail $ "No ibc for " ++ f
1307 IBC fn src -> loadIBC True fn)
1308 [(re, fn) | (re, fn, _, _) <- imports]
1309 reportParserWarnings
1311 -- process and check module aliases
1312 let modAliases = M.fromList
1313 [(prep alias, prep realName) | (reexport, realName, Just alias, fc) <- imports]
1314 prep = map T.pack . reverse . Spl.splitOn "/"
1315 aliasNames = [(alias, fc) | (_, _, Just alias, fc) <- imports]
1316 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1317 case map head . filter ((/= 1) . length) $ histogram of
1318 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1319 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1321 i <- getIState
1322 putIState (i { default_access = Hidden, module_aliases = modAliases })
1323 clearIBC -- start a new .ibc file
1324 -- record package info in .ibc
1325 imps <- allImportDirs
1326 mapM_ addIBC (map IBCImportDir imps)
1327 mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports]
1328 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1329 maxline = toline }
1330 ist <- getIState
1331 -- Save the span from parsing the module header, because
1332 -- an empty program parse might obliterate it.
1333 let oldSpan = idris_parsedSpan ist
1334 ds' <- parseProg syntax f file pos
1336 case (ds', oldSpan) of
1337 ([], Just fc) ->
1338 -- If no program elements were parsed, we dind't
1339 -- get a loaded region in the IBC file. That
1340 -- means we need to add it back.
1341 do ist <- getIState
1342 putIState ist { idris_parsedSpan = oldSpan
1343 , ibc_write = IBCParsedRegion fc :
1344 ibc_write ist
1346 _ -> return ()
1348 -- Parsing done, now process declarations
1350 let ds = namespaces mname ds'
1351 logLvl 3 (show $ showDecls verbosePPOption ds)
1352 i <- getIState
1353 logLvl 10 (show (toAlist (idris_implicits i)))
1354 logLvl 3 (show (idris_infixes i))
1355 -- Now add all the declarations to the context
1356 v <- verbose
1357 when v $ iputStrLn $ "Type checking " ++ f
1358 -- we totality check after every Mutual block, so if
1359 -- anything is a single definition, wrap it in a
1360 -- mutual block on its own
1361 elabDecls toplevel (map toMutual ds)
1362 i <- getIState
1363 -- simplify every definition do give the totality checker
1364 -- a better chance
1365 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1366 updateContext (simplifyCasedef n $ getErasureInfo i))
1367 (map snd (idris_totcheck i))
1368 -- build size change graph from simplified definitions
1369 iLOG "Totality checking"
1370 i <- getIState
1371 mapM_ buildSCG (idris_totcheck i)
1372 mapM_ checkDeclTotality (idris_totcheck i)
1374 -- Redo totality check for deferred names
1375 let deftots = idris_defertotcheck i
1376 iLOG $ "Totality checking " ++ show deftots
1377 mapM_ (\x -> do tot <- getTotality x
1378 case tot of
1379 Total _ -> setTotality x Unchecked
1380 _ -> return ()) (map snd deftots)
1381 mapM_ buildSCG deftots
1382 mapM_ checkDeclTotality deftots
1384 iLOG ("Finished " ++ f)
1385 ibcsd <- valIBCSubDir i
1386 iLOG "Universe checking"
1387 iucheck
1388 let ibc = ibcPathNoFallback ibcsd f
1389 i <- getIState
1390 addHides (hide_list i)
1392 -- Save module documentation if applicable
1393 i <- getIState
1394 case mdocs of
1395 Nothing -> return ()
1396 Just docs -> addModDoc syntax mname docs
1399 -- Finally, write an ibc if checking was successful
1400 ok <- noErrors
1401 when ok $
1402 idrisCatch (do writeIBC f ibc; clearIBC)
1403 (\c -> return ()) -- failure is harmless
1404 i <- getIState
1405 putIState (i { default_total = def_total,
1406 hide_list = [] })
1407 return ()
1408 where
1409 namespaces :: [String] -> [PDecl] -> [PDecl]
1410 namespaces [] ds = ds
1411 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1413 toMutual :: PDecl -> PDecl
1414 toMutual m@(PMutual _ d) = m
1415 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1416 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1417 case x of
1418 PClauses{} -> r
1419 PClass{} -> r
1420 PInstance{} -> r
1421 _ -> x
1423 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1424 addModDoc syn mname docs =
1425 do ist <- getIState
1426 docs' <- elabDocTerms recinfo (parsedDocs ist)
1427 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1428 putIState ist { idris_moduledocs = modDocs' }
1429 addIBC (IBCModDocs docName)
1430 where
1431 docName = NS modDocName (map T.pack (reverse mname))
1432 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1434{- | Adds names to hide list -}
1435addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1436addHides xs = do i <- getIState
1437 let defh = default_access i
1438 let (hs, as) = partition isNothing xs
1439 unless (null as) $
1440 mapM_ doHide
1441 (map (\ (n, _) -> (n, defh)) hs ++
1442 map (\ (n, Just a) -> (n, a)) as)
1443 where isNothing (_, Nothing) = True
1444 isNothing _ = False
1446 doHide (n, a) = do setAccessibility n a
1447 addIBC (IBCAccess n a)