git.iko.soy/Idris-dev
on 49fffbc help sign in
Idris-dev/src/Idris/Parser.hs
1435 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)
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 -- 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) <- option noDocs docComment
352 ist <- get
353 let doc' = annotCode (tryFullExpr syn ist) doc
354 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
355 | (n, d) <- argDocs ]
357 initOpts = if default_total ist
358 then [TotalFn]
359 else []
360 opts <- fnOpts initOpts
361 acc <- optional accessibility
362 opts' <- fnOpts opts
363 n_in <- fnName
364 let n = expandNS syn n_in
365 fc <- getFC
366 lchar ':'
367 return (doc', argDocs', fc, opts', n, acc))
368 ty <- typeExpr (allowImp syn)
369 terminator
370 addAcc n acc
371 return (PTy doc argDocs syn fc opts' n ty)
372 <|> postulate syn
373 <|> caf syn
374 <|> pattern syn
375 <?> "function declaration"
376 where checkFixity :: IdrisParser PDecl -> IdrisParser PDecl
377 checkFixity p = do decl <- p
378 case getName decl of
379 Nothing -> return decl
380 Just n -> do fOk <- fixityOK n
381 unless fOk . fail $
382 "Missing fixity declaration for " ++ show n
383 return decl
384 getName (PTy _ _ _ _ _ n _) = Just n
385 getName _ = Nothing
386 fixityOK (NS n _) = fixityOK n
387 fixityOK (UN n) | all (flip elem opChars) (str n) =
388 do fixities <- fmap idris_infixes get
389 return . elem (str n) . map (\ (Fix _ op) -> op) $ fixities
390 | otherwise = return True
391 fixityOK _ = return True
393{-| Parses function options given initial options
396FnOpts ::= 'total'
397 | 'partial'
398 | 'implicit'
399 | '%' 'no_implicit'
400 | '%' 'assert_total'
401 | '%' 'error_handler'
402 | '%' 'reflection'
403 | '%' 'specialise' '[' NameTimesList? ']'
404 ;
408NameTimes ::= FnName Natural?;
412NameTimesList ::=
413 NameTimes
414 | NameTimes ',' NameTimesList
415 ;
417-}
418-- FIXME: Check compatability for function options (i.e. partal/total)
419--
420-- Issue #1574 on the issue tracker.
421-- https://github.com/idris-lang/Idris-dev/issues/1574
422fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
423fnOpts opts
424 = do reserved "total"; fnOpts (TotalFn : opts)
425 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
426 <|> do reserved "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))
427 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;
428 fnOpts (CExport c : opts)
429 <|> do try (lchar '%' *> reserved "no_implicit");
430 fnOpts (NoImplicit : opts)
431 <|> do try (lchar '%' *> reserved "inline");
432 fnOpts (Inlinable : opts)
433 <|> do try (lchar '%' *> reserved "assert_total");
434 fnOpts (AssertTotal : opts)
435 <|> do try (lchar '%' *> reserved "error_handler");
436 fnOpts (ErrorHandler : opts)
437 <|> do try (lchar '%' *> reserved "error_reverse");
438 fnOpts (ErrorReverse : opts)
439 <|> do try (lchar '%' *> reserved "reflection");
440 fnOpts (Reflection : opts)
441 <|> do lchar '%'; reserved "specialise";
442 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
443 fnOpts (Specialise ns : opts)
444 <|> do reserved "implicit"; fnOpts (Implicit : opts)
445 <|> return opts
446 <?> "function modifier"
447 where nameTimes :: IdrisParser (Name, Maybe Int)
448 nameTimes = do n <- fnName
449 t <- option Nothing (do reds <- natural
450 return (Just (fromInteger reds)))
451 return (n, t)
453{- | Parses a postulate
456Postulate ::=
457 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
458 ;
460-}
461postulate :: SyntaxInfo -> IdrisParser PDecl
462postulate syn = do doc <- try $ do (doc, _) <- option noDocs docComment
463 ist <- get
464 let doc' = annotCode (tryFullExpr syn ist) doc
465 pushIndent
466 reserved "postulate"
467 return doc'
468 ist <- get
469 let initOpts = if default_total ist
470 then [TotalFn]
471 else []
472 opts <- fnOpts initOpts
473 acc <- optional accessibility
474 opts' <- fnOpts opts
475 n_in <- fnName
476 let n = expandNS syn n_in
477 lchar ':'
478 ty <- typeExpr (allowImp syn)
479 fc <- getFC
480 terminator
481 addAcc n acc
482 return (PPostulate doc syn fc opts' n ty)
483 <?> "postulate"
485{- | Parses a using declaration
488Using ::=
489 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
490 ;
492 -}
493using_ :: SyntaxInfo -> IdrisParser [PDecl]
494using_ syn =
495 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
496 openBlock
497 let uvars = using syn
498 ds <- many (decl (syn { using = uvars ++ ns }))
499 closeBlock
500 return (concat ds)
501 <?> "using declaration"
503{- | Parses a parameters declaration
506Params ::=
507 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
508 ;
510 -}
511params :: SyntaxInfo -> IdrisParser [PDecl]
512params syn =
513 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
514 openBlock
515 let pvars = syn_params syn
516 ds <- many (decl syn { syn_params = pvars ++ ns })
517 closeBlock
518 fc <- getFC
519 return [PParams fc ns (concat ds)]
520 <?> "parameters declaration"
522{- | Parses a mutual declaration (for mutually recursive functions)
525Mutual ::=
526 'mutual' OpenBlock Decl* CloseBlock
527 ;
529-}
530mutual :: SyntaxInfo -> IdrisParser [PDecl]
531mutual syn =
532 do reserved "mutual"
533 openBlock
534 let pvars = syn_params syn
535 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
536 closeBlock
537 fc <- getFC
538 return [PMutual fc (concat ds)]
539 <?> "mutual block"
541{-| Parses a namespace declaration
544Namespace ::=
545 'namespace' identifier OpenBlock Decl+ CloseBlock
546 ;
548-}
549namespace :: SyntaxInfo -> IdrisParser [PDecl]
550namespace syn =
551 do reserved "namespace"; n <- identifier;
552 openBlock
553 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
554 closeBlock
555 return [PNamespace n (concat ds)]
556 <?> "namespace declaration"
558{- | Parses a methods block (for instances)
561 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
563-}
564instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
565instanceBlock syn = do reserved "where"
566 openBlock
567 ds <- many (fnDecl syn)
568 closeBlock
569 return (concat ds)
570 <?> "instance block"
572{- | Parses a methods and instances block (for type classes)
575MethodOrInstance ::=
576 FnDecl
577 | Instance
578 ;
582ClassBlock ::=
583 'where' OpenBlock MethodOrInstance* CloseBlock
584 ;
586-}
587classBlock :: SyntaxInfo -> IdrisParser [PDecl]
588classBlock syn = do reserved "where"
589 openBlock
590 ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)
591 closeBlock
592 return (concat ds)
593 <?> "class block"
595{-| Parses a type class declaration
598ClassArgument ::=
599 Name
600 | '(' Name ':' Expr ')'
601 ;
605Class ::=
606 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
607 ;
609-}
610class_ :: SyntaxInfo -> IdrisParser [PDecl]
611class_ syn = do (doc, argDocs, acc) <- try (do
612 (doc, argDocs) <- option noDocs docComment
613 ist <- get
614 let doc' = annotCode (tryFullExpr syn ist) doc
615 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
616 | (n, d) <- argDocs ]
617 acc <- optional accessibility
618 return (doc', argDocs', acc))
619 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName
620 let n = expandNS syn n_in
621 cs <- many carg
622 ds <- option [] (classBlock syn)
623 accData acc n (concatMap declared ds)
624 return [PClass doc syn fc cons n cs argDocs ds]
625 <?> "type-class declaration"
626 where
627 carg :: IdrisParser (Name, PTerm)
628 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
629 return (i, ty)
630 <|> do i <- name;
631 return (i, PType)
633{- | Parses a type class instance declaration
636 Instance ::=
637 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
638 ;
642InstanceName ::= '[' Name ']';
644-}
645instance_ :: SyntaxInfo -> IdrisParser [PDecl]
646instance_ syn = do reserved "instance"; fc <- getFC
647 en <- optional instanceName
648 cs <- constraintList syn
649 cn <- fnName
650 args <- many (simpleExpr syn)
651 let sc = PApp fc (PRef fc cn) (map pexp args)
652 let t = bindList (PPi constraint) cs sc
653 ds <- option [] (instanceBlock syn)
654 return [PInstance syn fc cs cn args t en ds]
655 <?> "instance declaration"
656 where instanceName :: IdrisParser Name
657 instanceName = do lchar '['; n_in <- fnName; lchar ']'
658 let n = expandNS syn n_in
659 return n
660 <?> "instance name"
663{- | Parses a using declaration list
666UsingDeclList ::=
667 UsingDeclList'
668 | NameList TypeSig
669 ;
673UsingDeclList' ::=
674 UsingDecl
675 | UsingDecl ',' UsingDeclList'
676 ;
680NameList ::=
681 Name
682 | Name ',' NameList
683 ;
685-}
686usingDeclList :: SyntaxInfo -> IdrisParser [Using]
687usingDeclList syn
688 = try (sepBy1 (usingDecl syn) (lchar ','))
689 <|> do ns <- sepBy1 name (lchar ',')
690 lchar ':'
691 t <- typeExpr (disallowImp syn)
692 return (map (\x -> UImplicit x t) ns)
693 <?> "using declaration list"
695{- |Parses a using declaration
698UsingDecl ::=
699 FnName TypeSig
700 | FnName FnName+
701 ;
703-}
704usingDecl :: SyntaxInfo -> IdrisParser Using
705usingDecl syn = try (do x <- fnName
706 lchar ':'
707 t <- typeExpr (disallowImp syn)
708 return (UImplicit x t))
709 <|> do c <- fnName
710 xs <- some fnName
711 return (UConstraint c xs)
712 <?> "using declaration"
714{- | Parse a clause with patterns
717Pattern ::= Clause;
719-}
720pattern :: SyntaxInfo -> IdrisParser PDecl
721pattern syn = do fc <- getFC
722 clause <- clause syn
723 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
724 <?> "pattern"
726{- | Parse a constant applicative form declaration
729CAF ::= 'let' FnName '=' Expr Terminator;
731-}
732caf :: SyntaxInfo -> IdrisParser PDecl
733caf syn = do reserved "let"
734 n_in <- fnName; let n = expandNS syn n_in
735 lchar '='
736 t <- expr syn
737 terminator
738 fc <- getFC
739 return (PCAF fc n t)
740 <?> "constant applicative form declaration"
742{- | Parse an argument expression
745ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
747-}
748argExpr :: SyntaxInfo -> IdrisParser PTerm
749argExpr syn = let syn' = syn { inPattern = True } in
750 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
751 <?> "argument expression"
753{- | Parse a right hand side of a function
756RHS ::= '=' Expr
757 | '?=' RHSName? Expr
758 | 'impossible'
759 ;
763RHSName ::= '{' FnName '}';
765-}
766rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
767rhs syn n = do lchar '='; expr syn
768 <|> do symbol "?=";
769 fc <- getFC
770 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
771 return n)
772 r <- expr syn
773 return (addLet fc name r)
774 <|> do reserved "impossible"; return PImpossible
775 <?> "function right hand side"
776 where mkN :: Name -> Name
777 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
778 then sUN "infix_op_lemma_1"
779 else sUN (str x++"_lemma_1")
780 mkN (NS x n) = NS (mkN x) n
781 n' :: Name
782 n' = mkN n
783 addLet :: FC -> Name -> PTerm -> PTerm
784 addLet fc nm (PLet fc' n ty val r) = PLet fc' n ty val (addLet fc nm r)
785 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
786 where addLetC (l, r) = (l, addLet fc nm r)
787 addLet fc nm r = (PLet fc (sUN "value") Placeholder r (PMetavar nm))
789{- |Parses a function clause
792RHSOrWithBlock ::= RHS WhereOrTerminator
793 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
794 ;
798Clause ::= WExpr+ RHSOrWithBlock
799 | SimpleExpr '<==' FnName RHS WhereOrTerminator
800 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
801 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
802 ;
806ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
810WhereOrTerminator ::= WhereBlock | Terminator;
812-}
813clause :: SyntaxInfo -> IdrisParser PClause
814clause syn
815 = do wargs <- try (do pushIndent; some (wExpr syn))
816 fc <- getFC
817 ist <- get
818 n <- case lastParse ist of
819 Just t -> return t
820 Nothing -> fail "Invalid clause"
821 (do r <- rhs syn n
822 let ctxt = tt_ctxt ist
823 let wsyn = syn { syn_namespace = [] }
824 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
825 popIndent
826 return x,
827 do terminator
828 return ([], [])]
829 return $ PClauseR fc wargs r wheres) <|> (do
830 popIndent
831 reserved "with"
832 wval <- simpleExpr syn
833 pn <- optProof
834 openBlock
835 ds <- some $ fnDecl syn
836 let withs = concat ds
837 closeBlock
838 return $ PWithR fc wargs wval pn withs)
839 <|> do ty <- try (do pushIndent
840 ty <- simpleExpr syn
841 symbol "<=="
842 return ty)
843 fc <- getFC
844 n_in <- fnName; let n = expandNS syn n_in
845 r <- rhs syn n
846 ist <- get
847 let ctxt = tt_ctxt ist
848 let wsyn = syn { syn_namespace = [] }
849 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
850 popIndent
851 return x,
852 do terminator
853 return ([], [])]
854 let capp = PLet fc (sMN 0 "match")
855 ty
856 (PMatchApp fc n)
857 (PRef fc (sMN 0 "match"))
858 ist <- get
859 put (ist { lastParse = Just n })
860 return $ PClause fc n capp [] r wheres
861 <|> do (l, op) <- try (do
862 pushIndent
863 l <- argExpr syn
864 op <- operator
865 when (op == "=" || op == "?=" ) $
866 fail "infix clause definition with \"=\" and \"?=\" not supported "
867 return (l, op))
868 let n = expandNS syn (sUN op)
869 r <- argExpr syn
870 fc <- getFC
871 wargs <- many (wExpr syn)
872 (do rs <- rhs syn n
873 let wsyn = syn { syn_namespace = [] }
874 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
875 popIndent
876 return x,
877 do terminator
878 return ([], [])]
879 ist <- get
880 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
881 put (ist { lastParse = Just n })
882 return $ PClause fc n capp wargs rs wheres) <|> (do
883 popIndent
884 reserved "with"
885 wval <- bracketed syn
886 pn <- optProof
887 openBlock
888 ds <- some $ fnDecl syn
889 closeBlock
890 ist <- get
891 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
892 let withs = map (fillLHSD n capp wargs) $ concat ds
893 put (ist { lastParse = Just n })
894 return $ PWith fc n capp wargs wval pn withs)
895 <|> do pushIndent
896 n_in <- fnName; let n = expandNS syn n_in
897 cargs <- many (constraintArg syn)
898 fc <- getFC
899 args <- many (try (implicitArg (syn { inPattern = True } ))
900 <|> (fmap pexp (argExpr syn)))
901 wargs <- many (wExpr syn)
902 let capp = PApp fc (PRef fc n)
903 (cargs ++ args)
904 (do r <- rhs syn n
905 ist <- get
906 let ctxt = tt_ctxt ist
907 let wsyn = syn { syn_namespace = [] }
908 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
909 popIndent
910 return x,
911 do terminator
912 return ([], [])]
913 ist <- get
914 put (ist { lastParse = Just n })
915 return $ PClause fc n capp wargs r wheres) <|> (do
916 reserved "with"
917 ist <- get
918 put (ist { lastParse = Just n })
919 wval <- bracketed syn
920 pn <- optProof
921 openBlock
922 ds <- some $ fnDecl syn
923 let withs = map (fillLHSD n capp wargs) $ concat ds
924 closeBlock
925 popIndent
926 return $ PWith fc n capp wargs wval pn withs)
927 <?> "function clause"
928 where
929 optProof = option Nothing (do reserved "proof"
930 n <- fnName
931 return (Just n))
933 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
934 fillLHS n capp owargs (PClauseR fc wargs v ws)
935 = PClause fc n capp (owargs ++ wargs) v ws
936 fillLHS n capp owargs (PWithR fc wargs v pn ws)
937 = PWith fc n capp (owargs ++ wargs) v pn
938 (map (fillLHSD n capp (owargs ++ wargs)) ws)
939 fillLHS _ _ _ c = c
941 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
942 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
943 fillLHSD n c a x = x
945{-| Parses with pattern
948WExpr ::= '|' Expr';
950-}
951wExpr :: SyntaxInfo -> IdrisParser PTerm
952wExpr syn = do lchar '|'
953 expr' (syn { inPattern = True })
954 <?> "with pattern"
956{- | Parses a where block
959WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
961-}
962whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
963whereBlock n syn
964 = do reserved "where"
965 ds <- indentedBlock1 (decl syn)
966 let dns = concatMap (concatMap declared) ds
967 return (concat ds, map (\x -> (x, decoration syn x)) dns)
968 <?> "where block"
970{- |Parses a code generation target language name
973Codegen ::= 'C'
974 | 'Java'
975 | 'JavaScript'
976 | 'Node'
977 | 'LLVM'
978 | 'Bytecode'
979 ;
981-}
982codegen_ :: IdrisParser Codegen
983codegen_ = do n <- identifier; return (Via (map toLower n))
984 <|> do reserved "Bytecode"; return Bytecode
985 <?> "code generation language"
987{- |Parses a compiler directive
989StringList ::=
990 String
991 | String ',' StringList
992 ;
996Directive ::= '%' Directive';
1000Directive' ::= 'lib' CodeGen String_t
1001 | 'link' CodeGen String_t
1002 | 'flag' CodeGen String_t
1003 | 'include' CodeGen String_t
1004 | 'hide' Name
1005 | 'freeze' Name
1006 | 'access' Accessibility
1007 | 'default' Totality
1008 | 'logging' Natural
1009 | 'dynamic' StringList
1010 | 'name' Name NameList
1011 | 'error_handlers' Name NameList
1012 | 'language' 'TypeProviders'
1013 | 'language' 'ErrorReflection'
1017directive :: SyntaxInfo -> IdrisParser [PDecl]
1018directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
1019 return [PDirective (do addLib cgn lib
1020 addIBC (IBCLib cgn lib))]
1021 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
1022 return [PDirective (do dirs <- allImportDirs
1023 o <- liftIO $ findInPath dirs obj
1024 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
1025 addObjectFile cgn o)]
1026 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
1027 flag <- stringLiteral
1028 return [PDirective (do addIBC (IBCCGFlag cgn flag)
1029 addFlag cgn flag)]
1030 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
1031 return [PDirective (do addHdr cgn hdr
1032 addIBC (IBCHeader cgn hdr))]
1033 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
1034 return [PDirective (do setAccessibility n Hidden
1035 addIBC (IBCAccess n Hidden))]
1036 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
1037 return [PDirective (do setAccessibility n Frozen
1038 addIBC (IBCAccess n Frozen))]
1039 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1040 return [PDirective (do i <- get
1041 put(i { default_access = acc }))]
1042 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1043 i <- get
1044 put (i { default_total = tot } )
1045 return [PDirective (do i <- get
1046 put(i { default_total = tot }))]
1047 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
1048 return [PDirective (setLogLevel (fromInteger i))]
1049 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
1050 return [PDirective (do added <- addDyLib libs
1051 case added of
1052 Left lib -> addIBC (IBCDyLib (lib_name lib))
1053 Right msg ->
1054 fail $ msg)]
1055 <|> do try (lchar '%' *> reserved "name")
1056 ty <- fnName
1057 ns <- sepBy1 name (lchar ',')
1058 return [PDirective (do ty' <- disambiguate ty
1059 mapM_ (addNameHint ty') ns
1060 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1061 <|> do try (lchar '%' *> reserved "error_handlers")
1062 fn <- fnName
1063 arg <- fnName
1064 ns <- sepBy1 name (lchar ',')
1065 return [PDirective (do fn' <- disambiguate fn
1066 ns' <- mapM disambiguate ns
1067 addFunctionErrorHandlers fn' arg ns'
1068 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]
1069 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1070 return [PDirective (addLangExt ext)]
1071 <|> do fc <- getFC
1072 try (lchar '%' *> reserved "used")
1073 fn <- fnName
1074 arg <- iName []
1075 return [PDirective (addUsedName fc fn arg)]
1077 <?> "directive"
1078 where disambiguate :: Name -> Idris Name
1079 disambiguate n = do i <- getIState
1080 case lookupCtxtName n (idris_implicits i) of
1081 [(n', _)] -> return n'
1082 [] -> throwError (NoSuchVariable n)
1083 more -> throwError (CantResolveAlts (map fst more))
1085pLangExt :: IdrisParser LanguageExt
1086pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1087 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1089{- | Parses a totality
1092Totality ::= 'partial' | 'total'
1096totality :: IdrisParser Bool
1097totality
1098 = do reserved "total"; return True
1099 <|> do reserved "partial"; return False
1101{- | Parses a type provider
1104Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1105ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1107 -}
1108provider :: SyntaxInfo -> IdrisParser [PDecl]
1109provider syn = do try (lchar '%' *> reserved "provide");
1110 provideTerm <|> providePostulate
1111 <?> "type provider"
1112 where provideTerm = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1113 fc <- getFC
1114 reserved "with"
1115 e <- expr syn <?> "provider expression"
1116 return [PProvider syn fc (ProvTerm t e) n]
1117 providePostulate = do reserved "postulate"
1118 n <- fnName
1119 fc <- getFC
1120 reserved "with"
1121 e <- expr syn <?> "provider expression"
1122 return [PProvider syn fc (ProvPostulate e) n]
1124{- | Parses a transform
1127Transform ::= '%' 'transform' Expr '==>' Expr
1130transform :: SyntaxInfo -> IdrisParser [PDecl]
1131transform syn = do try (lchar '%' *> reserved "transform")
1132 -- leave it unchecked, until we work out what this should
1133 -- actually mean...
1134-- safety <- option True (do reserved "unsafe"
1135-- return False)
1136 l <- expr syn
1137 fc <- getFC
1138 symbol "==>"
1139 r <- expr syn
1140 return [PTransform fc False l r]
1141 <?> "transform"
1144{- * Loading and parsing -}
1145{- | Parses an expression from input -}
1146parseExpr :: IState -> String -> Result PTerm
1147parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1149{- | Parses a constant form input -}
1150parseConst :: IState -> String -> Result Const
1151parseConst st = runparser constant st "(input)"
1153{- | Parses a tactic from input -}
1154parseTactic :: IState -> String -> Result PTactic
1155parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1157-- | Parse module header and imports
1158parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta)
1159parseImports fname input
1160 = do i <- getIState
1161 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1162 Failure err -> fail (show err)
1163 Success (x, i) -> do putIState i
1164 return x
1165 where imports :: IdrisParser ((Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta), IState)
1166 imports = do whiteSpace
1167 (mdoc, mname) <- moduleHeader
1168 ps <- many import_
1169 mrk <- mark
1170 isEof <- lookAheadMatches eof
1171 let mrk' = if isEof
1172 then Nothing
1173 else Just mrk
1174 i <- get
1175 return ((mdoc, mname, ps, mrk'), i)
1177-- | There should be a better way of doing this...
1178findFC :: Doc -> (FC, String)
1179findFC x = let s = show (plain x) in
1180 case span (/= ':') s of
1181 (failname, ':':rest) -> case span isDigit rest of
1182 (line, ':':rest') -> case span isDigit rest' of
1183 (col, ':':msg) -> let pos = (read line, read col) in
1184 (FC failname pos pos, msg)
1186-- | Check if the coloring matches the options and corrects if necessary
1187fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1188fixColour False doc = ANSI.plain doc
1189fixColour True doc = doc
1191-- | A program is a list of declarations, possibly with associated
1192-- documentation strings.
1193parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1194 Idris [PDecl]
1195parseProg syn fname input mrk
1196 = do i <- getIState
1197 case runparser mainProg i fname input of
1198 Failure doc -> do -- FIXME: Get error location from trifecta
1199 -- this can't be the solution!
1200 -- Issue #1575 on the issue tracker.
1201 -- https://github.com/idris-lang/Idris-dev/issues/1575
1202 let (fc, msg) = findFC doc
1203 i <- getIState
1204 case idris_outputmode i of
1205 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1206 IdeMode n h -> iWarn fc (P.text msg)
1207 putIState (i { errSpan = Just fc })
1208 return []
1209 Success (x, i) -> do putIState i
1210 reportParserWarnings
1211 return $ collect x
1212 where mainProg :: IdrisParser ([PDecl], IState)
1213 mainProg = case mrk of
1214 Nothing -> do i <- get; return ([], i)
1215 Just mrk -> do
1216 release mrk
1217 ds <- prog syn
1218 i' <- get
1219 return (ds, i')
1221{- | Load idris module and show error if something wrong happens -}
1222loadModule :: FilePath -> Idris (Maybe String)
1223loadModule f
1224 = idrisCatch (loadModule' f)
1225 (\e -> do setErrSpan (getErrSpan e)
1226 ist <- getIState
1227 iWarn (getErrSpan e) $ pprintErr ist e
1228 return Nothing)
1230{- | Load idris module -}
1231loadModule' :: FilePath -> Idris (Maybe String)
1232loadModule' f
1233 = do i <- getIState
1234 let file = takeWhile (/= ' ') f
1235 ibcsd <- valIBCSubDir i
1236 ids <- allImportDirs
1237 fp <- findImport ids ibcsd file
1238 if file `elem` imported i
1239 then do iLOG $ "Already read " ++ file
1240 return Nothing
1241 else do putIState (i { imported = file : imported i })
1242 case fp of
1243 IDR fn -> loadSource False fn Nothing
1244 LIDR fn -> loadSource True fn Nothing
1245 IBC fn src ->
1246 idrisCatch (loadIBC True fn)
1247 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1248 case src of
1249 IDR sfn -> loadSource False sfn Nothing
1250 LIDR sfn -> loadSource True sfn Nothing)
1251 return $ Just file
1253{- | Load idris code from file -}
1254loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()
1255loadFromIFile reexp i@(IBC fn src) maxline
1256 = do iLOG $ "Skipping " ++ getSrcFile i
1257 idrisCatch (loadIBC reexp fn)
1258 (\err -> ierror $ LoadingFailed fn err)
1259 where
1260 getSrcFile (IDR fn) = fn
1261 getSrcFile (LIDR fn) = fn
1262 getSrcFile (IBC f src) = getSrcFile src
1264loadFromIFile _ (IDR fn) maxline = loadSource' False fn maxline
1265loadFromIFile _ (LIDR fn) maxline = loadSource' True fn maxline
1267{-| Load idris source code and show error if something wrong happens -}
1268loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1269loadSource' lidr r maxline
1270 = idrisCatch (loadSource lidr r maxline)
1271 (\e -> do setErrSpan (getErrSpan e)
1272 ist <- getIState
1273 case e of
1274 At f e' -> iWarn f (pprintErr ist e')
1275 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1277{- | Load Idris source code-}
1278loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1279loadSource lidr f toline
1280 = do iLOG ("Reading " ++ f)
1281 i <- getIState
1282 let def_total = default_total i
1283 file_in <- runIO $ readFile f
1284 file <- if lidr then tclift $ unlit f file_in else return file_in
1285 (mdocs, mname, imports_in, pos) <- parseImports f file
1286 ai <- getAutoImports
1287 let imports = map (\n -> (True, n, Just n, emptyFC)) ai ++ imports_in
1288 ids <- allImportDirs
1289 ibcsd <- valIBCSubDir i
1290 mapM_ (\(re, f) ->
1291 do fp <- findImport ids ibcsd f
1292 case fp of
1293 LIDR fn -> ifail $ "No ibc for " ++ f
1294 IDR fn -> ifail $ "No ibc for " ++ f
1295 IBC fn src -> loadIBC True fn)
1296 [(re, fn) | (re, fn, _, _) <- imports]
1297 reportParserWarnings
1299 -- process and check module aliases
1300 let modAliases = M.fromList
1301 [(prep alias, prep realName) | (reexport, realName, Just alias, fc) <- imports]
1302 prep = map T.pack . reverse . Spl.splitOn "/"
1303 aliasNames = [(alias, fc) | (_, _, Just alias, fc) <- imports]
1304 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1305 case map head . filter ((/= 1) . length) $ histogram of
1306 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1307 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1309 i <- getIState
1310 putIState (i { default_access = Hidden, module_aliases = modAliases })
1311 clearIBC -- start a new .ibc file
1312 -- record package info in .ibc
1313 imps <- allImportDirs
1314 mapM_ addIBC (map IBCImportDir imps)
1315 mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports]
1316 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1317 maxline = toline }
1318 ist <- getIState
1319 -- Save the span from parsing the module header, because
1320 -- an empty program parse might obliterate it.
1321 let oldSpan = idris_parsedSpan ist
1322 ds' <- parseProg syntax f file pos
1324 case (ds', oldSpan) of
1325 ([], Just fc) ->
1326 -- If no program elements were parsed, we dind't
1327 -- get a loaded region in the IBC file. That
1328 -- means we need to add it back.
1329 do ist <- getIState
1330 putIState ist { idris_parsedSpan = oldSpan
1331 , ibc_write = IBCParsedRegion fc :
1332 ibc_write ist
1334 _ -> return ()
1336 -- Parsing done, now process declarations
1338 let ds = namespaces mname ds'
1339 logLvl 3 (show $ showDecls verbosePPOption ds)
1340 i <- getIState
1341 logLvl 10 (show (toAlist (idris_implicits i)))
1342 logLvl 3 (show (idris_infixes i))
1343 -- Now add all the declarations to the context
1344 v <- verbose
1345 when v $ iputStrLn $ "Type checking " ++ f
1346 -- we totality check after every Mutual block, so if
1347 -- anything is a single definition, wrap it in a
1348 -- mutual block on its own
1349 elabDecls toplevel (map toMutual ds)
1350 i <- getIState
1351 -- simplify every definition do give the totality checker
1352 -- a better chance
1353 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1354 updateContext (simplifyCasedef n $ getErasureInfo i))
1355 (map snd (idris_totcheck i))
1356 -- build size change graph from simplified definitions
1357 iLOG "Totality checking"
1358 i <- getIState
1359 mapM_ buildSCG (idris_totcheck i)
1360 mapM_ checkDeclTotality (idris_totcheck i)
1362 -- Redo totality check for deferred names
1363 let deftots = idris_defertotcheck i
1364 iLOG $ "Totality checking " ++ show deftots
1365 mapM_ (\x -> do tot <- getTotality x
1366 case tot of
1367 Total _ -> setTotality x Unchecked
1368 _ -> return ()) (map snd deftots)
1369 mapM_ buildSCG deftots
1370 mapM_ checkDeclTotality deftots
1372 iLOG ("Finished " ++ f)
1373 ibcsd <- valIBCSubDir i
1374 iLOG "Universe checking"
1375 iucheck
1376 let ibc = ibcPathNoFallback ibcsd f
1377 i <- getIState
1378 addHides (hide_list i)
1380 -- Save module documentation if applicable
1381 i <- getIState
1382 case mdocs of
1383 Nothing -> return ()
1384 Just docs -> addModDoc syntax mname docs
1387 -- Finally, write an ibc if checking was successful
1388 ok <- noErrors
1389 when ok $
1390 idrisCatch (do writeIBC f ibc; clearIBC)
1391 (\c -> return ()) -- failure is harmless
1392 i <- getIState
1393 putIState (i { default_total = def_total,
1394 hide_list = [] })
1395 return ()
1396 where
1397 namespaces :: [String] -> [PDecl] -> [PDecl]
1398 namespaces [] ds = ds
1399 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1401 toMutual :: PDecl -> PDecl
1402 toMutual m@(PMutual _ d) = m
1403 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1404 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1405 case x of
1406 PClauses _ _ _ _ -> r
1407 PClass _ _ _ _ _ _ _ _ -> r
1408 PInstance _ _ _ _ _ _ _ _ -> r
1409 _ -> x
1411 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1412 addModDoc syn mname docs =
1413 do ist <- getIState
1414 docs' <- elabDocTerms recinfo (parsedDocs ist)
1415 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1416 putIState ist { idris_moduledocs = modDocs' }
1417 addIBC (IBCModDocs docName)
1418 where
1419 docName = NS modDocName (map T.pack (reverse mname))
1420 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1422{- | Adds names to hide list -}
1423addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1424addHides xs = do i <- getIState
1425 let defh = default_access i
1426 let (hs, as) = partition isNothing xs
1427 unless (null as) $
1428 mapM_ doHide
1429 (map (\ (n, _) -> (n, defh)) hs ++
1430 map (\ (n, Just a) -> (n, a)) as)
1431 where isNothing (_, Nothing) = True
1432 isNothing _ = False
1434 doHide (n, a) = do setAccessibility n a
1435 addIBC (IBCAccess n a)