git.iko.soy/Idris-dev
on cfd6dbc help sign in
Idris-dev/src/Idris/Parser.hs
1451 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 fds <- option (map fst cs) fundeps
616 ds <- option [] (classBlock syn)
617 accData acc n (concatMap declared ds)
618 return [PClass doc syn fc cons n cs argDocs fds ds]
619 <?> "type-class declaration"
620 where
621 fundeps :: IdrisParser [Name]
622 fundeps = do lchar '|'; sepBy name (lchar ',')
624 carg :: IdrisParser (Name, PTerm)
625 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
626 return (i, ty)
627 <|> do i <- name;
628 return (i, PType)
630{- | Parses a type class instance declaration
633 Instance ::=
634 DocComment_t? 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
635 ;
639InstanceName ::= '[' Name ']';
641-}
642instance_ :: SyntaxInfo -> IdrisParser [PDecl]
643instance_ syn = do (doc, argDocs)
644 <- try (docstring syn <* reserved "instance")
645 fc <- getFC
646 en <- optional instanceName
647 cs <- constraintList syn
648 cn <- fnName
649 args <- many (simpleExpr syn)
650 let sc = PApp fc (PRef fc cn) (map pexp args)
651 let t = bindList (PPi constraint) cs sc
652 ds <- option [] (instanceBlock syn)
653 return [PInstance doc argDocs syn fc cs cn args t en ds]
654 <?> "instance declaration"
655 where instanceName :: IdrisParser Name
656 instanceName = do lchar '['; n_in <- fnName; lchar ']'
657 let n = expandNS syn n_in
658 return n
659 <?> "instance name"
662-- | Parse a docstring
663docstring :: SyntaxInfo
664 -> IdrisParser (Docstring (Either Err PTerm),
665 [(Name,Docstring (Either Err PTerm))])
666docstring syn = do (doc, argDocs) <- option noDocs docComment
667 ist <- get
668 let doc' = annotCode (tryFullExpr syn ist) doc
669 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
670 | (n, d) <- argDocs ]
671 return (doc', argDocs')
674{- | Parses a using declaration list
677UsingDeclList ::=
678 UsingDeclList'
679 | NameList TypeSig
680 ;
684UsingDeclList' ::=
685 UsingDecl
686 | UsingDecl ',' UsingDeclList'
687 ;
691NameList ::=
692 Name
693 | Name ',' NameList
694 ;
696-}
697usingDeclList :: SyntaxInfo -> IdrisParser [Using]
698usingDeclList syn
699 = try (sepBy1 (usingDecl syn) (lchar ','))
700 <|> do ns <- sepBy1 name (lchar ',')
701 lchar ':'
702 t <- typeExpr (disallowImp syn)
703 return (map (\x -> UImplicit x t) ns)
704 <?> "using declaration list"
706{- |Parses a using declaration
709UsingDecl ::=
710 FnName TypeSig
711 | FnName FnName+
712 ;
714-}
715usingDecl :: SyntaxInfo -> IdrisParser Using
716usingDecl syn = try (do x <- fnName
717 lchar ':'
718 t <- typeExpr (disallowImp syn)
719 return (UImplicit x t))
720 <|> do c <- fnName
721 xs <- some fnName
722 return (UConstraint c xs)
723 <?> "using declaration"
725{- | Parse a clause with patterns
728Pattern ::= Clause;
730-}
731pattern :: SyntaxInfo -> IdrisParser PDecl
732pattern syn = do fc <- getFC
733 clause <- clause syn
734 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
735 <?> "pattern"
737{- | Parse a constant applicative form declaration
740CAF ::= 'let' FnName '=' Expr Terminator;
742-}
743caf :: SyntaxInfo -> IdrisParser PDecl
744caf syn = do reserved "let"
745 n_in <- fnName; let n = expandNS syn n_in
746 lchar '='
747 t <- expr syn
748 terminator
749 fc <- getFC
750 return (PCAF fc n t)
751 <?> "constant applicative form declaration"
753{- | Parse an argument expression
756ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
758-}
759argExpr :: SyntaxInfo -> IdrisParser PTerm
760argExpr syn = let syn' = syn { inPattern = True } in
761 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
762 <?> "argument expression"
764{- | Parse a right hand side of a function
767RHS ::= '=' Expr
768 | '?=' RHSName? Expr
769 | 'impossible'
770 ;
774RHSName ::= '{' FnName '}';
776-}
777rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
778rhs syn n = do lchar '='; expr syn
779 <|> do symbol "?=";
780 fc <- getFC
781 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
782 return n)
783 r <- expr syn
784 return (addLet fc name r)
785 <|> do reserved "impossible"; return PImpossible
786 <?> "function right hand side"
787 where mkN :: Name -> Name
788 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
789 then sUN "infix_op_lemma_1"
790 else sUN (str x++"_lemma_1")
791 mkN (NS x n) = NS (mkN x) n
792 n' :: Name
793 n' = mkN n
794 addLet :: FC -> Name -> PTerm -> PTerm
795 addLet fc nm (PLet fc' n ty val r) = PLet fc' n ty val (addLet fc nm r)
796 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
797 where addLetC (l, r) = (l, addLet fc nm r)
798 addLet fc nm r = (PLet fc (sUN "value") Placeholder r (PMetavar nm))
800{- |Parses a function clause
803RHSOrWithBlock ::= RHS WhereOrTerminator
804 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
805 ;
809Clause ::= WExpr+ RHSOrWithBlock
810 | SimpleExpr '<==' FnName RHS WhereOrTerminator
811 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
812 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
813 ;
817ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
821WhereOrTerminator ::= WhereBlock | Terminator;
823-}
824clause :: SyntaxInfo -> IdrisParser PClause
825clause syn
826 = do wargs <- try (do pushIndent; some (wExpr syn))
827 fc <- getFC
828 ist <- get
829 n <- case lastParse ist of
830 Just t -> return t
831 Nothing -> fail "Invalid clause"
832 (do r <- rhs syn n
833 let ctxt = tt_ctxt ist
834 let wsyn = syn { syn_namespace = [] }
835 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
836 popIndent
837 return x,
838 do terminator
839 return ([], [])]
840 return $ PClauseR fc wargs r wheres) <|> (do
841 popIndent
842 reserved "with"
843 wval <- simpleExpr syn
844 pn <- optProof
845 openBlock
846 ds <- some $ fnDecl syn
847 let withs = concat ds
848 closeBlock
849 return $ PWithR fc wargs wval pn withs)
850 <|> do ty <- try (do pushIndent
851 ty <- simpleExpr syn
852 symbol "<=="
853 return ty)
854 fc <- getFC
855 n_in <- fnName; let n = expandNS syn n_in
856 r <- rhs syn n
857 ist <- get
858 let ctxt = tt_ctxt ist
859 let wsyn = syn { syn_namespace = [] }
860 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
861 popIndent
862 return x,
863 do terminator
864 return ([], [])]
865 let capp = PLet fc (sMN 0 "match")
866 ty
867 (PMatchApp fc n)
868 (PRef fc (sMN 0 "match"))
869 ist <- get
870 put (ist { lastParse = Just n })
871 return $ PClause fc n capp [] r wheres
872 <|> do (l, op) <- try (do
873 pushIndent
874 l <- argExpr syn
875 op <- operator
876 when (op == "=" || op == "?=" ) $
877 fail "infix clause definition with \"=\" and \"?=\" not supported "
878 return (l, op))
879 let n = expandNS syn (sUN op)
880 r <- argExpr syn
881 fc <- getFC
882 wargs <- many (wExpr syn)
883 (do rs <- rhs syn n
884 let wsyn = syn { syn_namespace = [] }
885 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
886 popIndent
887 return x,
888 do terminator
889 return ([], [])]
890 ist <- get
891 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
892 put (ist { lastParse = Just n })
893 return $ PClause fc n capp wargs rs wheres) <|> (do
894 popIndent
895 reserved "with"
896 wval <- bracketed syn
897 pn <- optProof
898 openBlock
899 ds <- some $ fnDecl syn
900 closeBlock
901 ist <- get
902 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
903 let withs = map (fillLHSD n capp wargs) $ concat ds
904 put (ist { lastParse = Just n })
905 return $ PWith fc n capp wargs wval pn withs)
906 <|> do pushIndent
907 n_in <- fnName; let n = expandNS syn n_in
908 cargs <- many (constraintArg syn)
909 fc <- getFC
910 args <- many (try (implicitArg (syn { inPattern = True } ))
911 <|> (fmap pexp (argExpr syn)))
912 wargs <- many (wExpr syn)
913 let capp = PApp fc (PRef fc n)
914 (cargs ++ args)
915 (do r <- rhs syn n
916 ist <- get
917 let ctxt = tt_ctxt ist
918 let wsyn = syn { syn_namespace = [] }
919 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
920 popIndent
921 return x,
922 do terminator
923 return ([], [])]
924 ist <- get
925 put (ist { lastParse = Just n })
926 return $ PClause fc n capp wargs r wheres) <|> (do
927 reserved "with"
928 ist <- get
929 put (ist { lastParse = Just n })
930 wval <- bracketed syn
931 pn <- optProof
932 openBlock
933 ds <- some $ fnDecl syn
934 let withs = map (fillLHSD n capp wargs) $ concat ds
935 closeBlock
936 popIndent
937 return $ PWith fc n capp wargs wval pn withs)
938 <?> "function clause"
939 where
940 optProof = option Nothing (do reserved "proof"
941 n <- fnName
942 return (Just n))
944 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
945 fillLHS n capp owargs (PClauseR fc wargs v ws)
946 = PClause fc n capp (owargs ++ wargs) v ws
947 fillLHS n capp owargs (PWithR fc wargs v pn ws)
948 = PWith fc n capp (owargs ++ wargs) v pn
949 (map (fillLHSD n capp (owargs ++ wargs)) ws)
950 fillLHS _ _ _ c = c
952 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
953 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
954 fillLHSD n c a x = x
956{-| Parses with pattern
959WExpr ::= '|' Expr';
961-}
962wExpr :: SyntaxInfo -> IdrisParser PTerm
963wExpr syn = do lchar '|'
964 expr' (syn { inPattern = True })
965 <?> "with pattern"
967{- | Parses a where block
970WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
972-}
973whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
974whereBlock n syn
975 = do reserved "where"
976 ds <- indentedBlock1 (decl syn)
977 let dns = concatMap (concatMap declared) ds
978 return (concat ds, map (\x -> (x, decoration syn x)) dns)
979 <?> "where block"
981{- |Parses a code generation target language name
984Codegen ::= 'C'
985 | 'Java'
986 | 'JavaScript'
987 | 'Node'
988 | 'LLVM'
989 | 'Bytecode'
990 ;
992-}
993codegen_ :: IdrisParser Codegen
994codegen_ = do n <- identifier; return (Via (map toLower n))
995 <|> do reserved "Bytecode"; return Bytecode
996 <?> "code generation language"
998{- |Parses a compiler directive
1000StringList ::=
1001 String
1002 | String ',' StringList
1007Directive ::= '%' Directive';
1011Directive' ::= 'lib' CodeGen String_t
1012 | 'link' CodeGen String_t
1013 | 'flag' CodeGen String_t
1014 | 'include' CodeGen String_t
1015 | 'hide' Name
1016 | 'freeze' Name
1017 | 'access' Accessibility
1018 | 'default' Totality
1019 | 'logging' Natural
1020 | 'dynamic' StringList
1021 | 'name' Name NameList
1022 | 'error_handlers' Name NameList
1023 | 'language' 'TypeProviders'
1024 | 'language' 'ErrorReflection'
1028directive :: SyntaxInfo -> IdrisParser [PDecl]
1029directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
1030 return [PDirective (do addLib cgn lib
1031 addIBC (IBCLib cgn lib))]
1032 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
1033 return [PDirective (do dirs <- allImportDirs
1034 o <- liftIO $ findInPath dirs obj
1035 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
1036 addObjectFile cgn o)]
1037 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
1038 flag <- stringLiteral
1039 return [PDirective (do addIBC (IBCCGFlag cgn flag)
1040 addFlag cgn flag)]
1041 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
1042 return [PDirective (do addHdr cgn hdr
1043 addIBC (IBCHeader cgn hdr))]
1044 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
1045 return [PDirective (do setAccessibility n Hidden
1046 addIBC (IBCAccess n Hidden))]
1047 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
1048 return [PDirective (do setAccessibility n Frozen
1049 addIBC (IBCAccess n Frozen))]
1050 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1051 return [PDirective (do i <- get
1052 put(i { default_access = acc }))]
1053 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1054 i <- get
1055 put (i { default_total = tot } )
1056 return [PDirective (do i <- get
1057 put(i { default_total = tot }))]
1058 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
1059 return [PDirective (setLogLevel (fromInteger i))]
1060 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
1061 return [PDirective (do added <- addDyLib libs
1062 case added of
1063 Left lib -> addIBC (IBCDyLib (lib_name lib))
1064 Right msg ->
1065 fail $ msg)]
1066 <|> do try (lchar '%' *> reserved "name")
1067 ty <- fnName
1068 ns <- sepBy1 name (lchar ',')
1069 return [PDirective (do ty' <- disambiguate ty
1070 mapM_ (addNameHint ty') ns
1071 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1072 <|> do try (lchar '%' *> reserved "error_handlers")
1073 fn <- fnName
1074 arg <- fnName
1075 ns <- sepBy1 name (lchar ',')
1076 return [PDirective (do fn' <- disambiguate fn
1077 ns' <- mapM disambiguate ns
1078 addFunctionErrorHandlers fn' arg ns'
1079 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]
1080 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1081 return [PDirective (addLangExt ext)]
1082 <|> do fc <- getFC
1083 try (lchar '%' *> reserved "used")
1084 fn <- fnName
1085 arg <- iName []
1086 return [PDirective (addUsedName fc fn arg)]
1088 <?> "directive"
1089 where disambiguate :: Name -> Idris Name
1090 disambiguate n = do i <- getIState
1091 case lookupCtxtName n (idris_implicits i) of
1092 [(n', _)] -> return n'
1093 [] -> throwError (NoSuchVariable n)
1094 more -> throwError (CantResolveAlts (map fst more))
1096pLangExt :: IdrisParser LanguageExt
1097pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1098 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1100{- | Parses a totality
1103Totality ::= 'partial' | 'total'
1107totality :: IdrisParser Bool
1108totality
1109 = do reserved "total"; return True
1110 <|> do reserved "partial"; return False
1112{- | Parses a type provider
1115Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1116ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1118 -}
1119provider :: SyntaxInfo -> IdrisParser [PDecl]
1120provider syn = do doc <- try (do (doc, _) <- docstring syn
1121 lchar '%'
1122 reserved "provide"
1123 return doc)
1124 provideTerm doc <|> providePostulate doc
1125 <?> "type provider"
1126 where provideTerm doc =
1127 do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1128 fc <- getFC
1129 reserved "with"
1130 e <- expr syn <?> "provider expression"
1131 return [PProvider doc syn fc (ProvTerm t e) n]
1132 providePostulate doc =
1133 do reserved "postulate"
1134 n <- fnName
1135 fc <- getFC
1136 reserved "with"
1137 e <- expr syn <?> "provider expression"
1138 return [PProvider doc syn fc (ProvPostulate e) n]
1140{- | Parses a transform
1143Transform ::= '%' 'transform' Expr '==>' Expr
1146transform :: SyntaxInfo -> IdrisParser [PDecl]
1147transform syn = do try (lchar '%' *> reserved "transform")
1148 -- leave it unchecked, until we work out what this should
1149 -- actually mean...
1150-- safety <- option True (do reserved "unsafe"
1151-- return False)
1152 l <- expr syn
1153 fc <- getFC
1154 symbol "==>"
1155 r <- expr syn
1156 return [PTransform fc False l r]
1157 <?> "transform"
1160{- * Loading and parsing -}
1161{- | Parses an expression from input -}
1162parseExpr :: IState -> String -> Result PTerm
1163parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1165{- | Parses a constant form input -}
1166parseConst :: IState -> String -> Result Const
1167parseConst st = runparser constant st "(input)"
1169{- | Parses a tactic from input -}
1170parseTactic :: IState -> String -> Result PTactic
1171parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1173-- | Parse module header and imports
1174parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta)
1175parseImports fname input
1176 = do i <- getIState
1177 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1178 Failure err -> fail (show err)
1179 Success (x, i) -> do putIState i
1180 return x
1181 where imports :: IdrisParser ((Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta), IState)
1182 imports = do whiteSpace
1183 (mdoc, mname) <- moduleHeader
1184 ps <- many import_
1185 mrk <- mark
1186 isEof <- lookAheadMatches eof
1187 let mrk' = if isEof
1188 then Nothing
1189 else Just mrk
1190 i <- get
1191 return ((mdoc, mname, ps, mrk'), i)
1193-- | There should be a better way of doing this...
1194findFC :: Doc -> (FC, String)
1195findFC x = let s = show (plain x) in
1196 case span (/= ':') s of
1197 (failname, ':':rest) -> case span isDigit rest of
1198 (line, ':':rest') -> case span isDigit rest' of
1199 (col, ':':msg) -> let pos = (read line, read col) in
1200 (FC failname pos pos, msg)
1202-- | Check if the coloring matches the options and corrects if necessary
1203fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1204fixColour False doc = ANSI.plain doc
1205fixColour True doc = doc
1207-- | A program is a list of declarations, possibly with associated
1208-- documentation strings.
1209parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1210 Idris [PDecl]
1211parseProg syn fname input mrk
1212 = do i <- getIState
1213 case runparser mainProg i fname input of
1214 Failure doc -> do -- FIXME: Get error location from trifecta
1215 -- this can't be the solution!
1216 -- Issue #1575 on the issue tracker.
1217 -- https://github.com/idris-lang/Idris-dev/issues/1575
1218 let (fc, msg) = findFC doc
1219 i <- getIState
1220 case idris_outputmode i of
1221 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1222 IdeMode n h -> iWarn fc (P.text msg)
1223 putIState (i { errSpan = Just fc })
1224 return []
1225 Success (x, i) -> do putIState i
1226 reportParserWarnings
1227 return $ collect x
1228 where mainProg :: IdrisParser ([PDecl], IState)
1229 mainProg = case mrk of
1230 Nothing -> do i <- get; return ([], i)
1231 Just mrk -> do
1232 release mrk
1233 ds <- prog syn
1234 i' <- get
1235 return (ds, i')
1237{- | Load idris module and show error if something wrong happens -}
1238loadModule :: FilePath -> Idris (Maybe String)
1239loadModule f
1240 = idrisCatch (loadModule' f)
1241 (\e -> do setErrSpan (getErrSpan e)
1242 ist <- getIState
1243 iWarn (getErrSpan e) $ pprintErr ist e
1244 return Nothing)
1246{- | Load idris module -}
1247loadModule' :: FilePath -> Idris (Maybe String)
1248loadModule' f
1249 = do i <- getIState
1250 let file = takeWhile (/= ' ') f
1251 ibcsd <- valIBCSubDir i
1252 ids <- allImportDirs
1253 fp <- findImport ids ibcsd file
1254 if file `elem` imported i
1255 then do iLOG $ "Already read " ++ file
1256 return Nothing
1257 else do putIState (i { imported = file : imported i })
1258 case fp of
1259 IDR fn -> loadSource False fn Nothing
1260 LIDR fn -> loadSource True fn Nothing
1261 IBC fn src ->
1262 idrisCatch (loadIBC True fn)
1263 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1264 case src of
1265 IDR sfn -> loadSource False sfn Nothing
1266 LIDR sfn -> loadSource True sfn Nothing)
1267 return $ Just file
1269{- | Load idris code from file -}
1270loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()
1271loadFromIFile reexp i@(IBC fn src) maxline
1272 = do iLOG $ "Skipping " ++ getSrcFile i
1273 idrisCatch (loadIBC reexp fn)
1274 (\err -> ierror $ LoadingFailed fn err)
1275 where
1276 getSrcFile (IDR fn) = fn
1277 getSrcFile (LIDR fn) = fn
1278 getSrcFile (IBC f src) = getSrcFile src
1280loadFromIFile _ (IDR fn) maxline = loadSource' False fn maxline
1281loadFromIFile _ (LIDR fn) maxline = loadSource' True fn maxline
1283{-| Load idris source code and show error if something wrong happens -}
1284loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1285loadSource' lidr r maxline
1286 = idrisCatch (loadSource lidr r maxline)
1287 (\e -> do setErrSpan (getErrSpan e)
1288 ist <- getIState
1289 case e of
1290 At f e' -> iWarn f (pprintErr ist e')
1291 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1293{- | Load Idris source code-}
1294loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1295loadSource lidr f toline
1296 = do iLOG ("Reading " ++ f)
1297 i <- getIState
1298 let def_total = default_total i
1299 file_in <- runIO $ readFile f
1300 file <- if lidr then tclift $ unlit f file_in else return file_in
1301 (mdocs, mname, imports_in, pos) <- parseImports f file
1302 ai <- getAutoImports
1303 let imports = map (\n -> (True, n, Just n, emptyFC)) ai ++ imports_in
1304 ids <- allImportDirs
1305 ibcsd <- valIBCSubDir i
1306 mapM_ (\(re, f) ->
1307 do fp <- findImport ids ibcsd f
1308 case fp of
1309 LIDR fn -> ifail $ "No ibc for " ++ f
1310 IDR fn -> ifail $ "No ibc for " ++ f
1311 IBC fn src -> loadIBC True fn)
1312 [(re, fn) | (re, fn, _, _) <- imports]
1313 reportParserWarnings
1315 -- process and check module aliases
1316 let modAliases = M.fromList
1317 [(prep alias, prep realName) | (reexport, realName, Just alias, fc) <- imports]
1318 prep = map T.pack . reverse . Spl.splitOn "/"
1319 aliasNames = [(alias, fc) | (_, _, Just alias, fc) <- imports]
1320 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1321 case map head . filter ((/= 1) . length) $ histogram of
1322 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1323 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1325 i <- getIState
1326 putIState (i { default_access = Hidden, module_aliases = modAliases })
1327 clearIBC -- start a new .ibc file
1328 -- record package info in .ibc
1329 imps <- allImportDirs
1330 mapM_ addIBC (map IBCImportDir imps)
1331 mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports]
1332 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1333 maxline = toline }
1334 ist <- getIState
1335 -- Save the span from parsing the module header, because
1336 -- an empty program parse might obliterate it.
1337 let oldSpan = idris_parsedSpan ist
1338 ds' <- parseProg syntax f file pos
1340 case (ds', oldSpan) of
1341 ([], Just fc) ->
1342 -- If no program elements were parsed, we dind't
1343 -- get a loaded region in the IBC file. That
1344 -- means we need to add it back.
1345 do ist <- getIState
1346 putIState ist { idris_parsedSpan = oldSpan
1347 , ibc_write = IBCParsedRegion fc :
1348 ibc_write ist
1350 _ -> return ()
1352 -- Parsing done, now process declarations
1354 let ds = namespaces mname ds'
1355 logLvl 3 (show $ showDecls verbosePPOption ds)
1356 i <- getIState
1357 logLvl 10 (show (toAlist (idris_implicits i)))
1358 logLvl 3 (show (idris_infixes i))
1359 -- Now add all the declarations to the context
1360 v <- verbose
1361 when v $ iputStrLn $ "Type checking " ++ f
1362 -- we totality check after every Mutual block, so if
1363 -- anything is a single definition, wrap it in a
1364 -- mutual block on its own
1365 elabDecls toplevel (map toMutual ds)
1366 i <- getIState
1367 -- simplify every definition do give the totality checker
1368 -- a better chance
1369 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1370 updateContext (simplifyCasedef n $ getErasureInfo i))
1371 (map snd (idris_totcheck i))
1372 -- build size change graph from simplified definitions
1373 iLOG "Totality checking"
1374 i <- getIState
1375 mapM_ buildSCG (idris_totcheck i)
1376 mapM_ checkDeclTotality (idris_totcheck i)
1378 -- Redo totality check for deferred names
1379 let deftots = idris_defertotcheck i
1380 iLOG $ "Totality checking " ++ show deftots
1381 mapM_ (\x -> do tot <- getTotality x
1382 case tot of
1383 Total _ -> setTotality x Unchecked
1384 _ -> return ()) (map snd deftots)
1385 mapM_ buildSCG deftots
1386 mapM_ checkDeclTotality deftots
1388 iLOG ("Finished " ++ f)
1389 ibcsd <- valIBCSubDir i
1390 iLOG "Universe checking"
1391 iucheck
1392 let ibc = ibcPathNoFallback ibcsd f
1393 i <- getIState
1394 addHides (hide_list i)
1396 -- Save module documentation if applicable
1397 i <- getIState
1398 case mdocs of
1399 Nothing -> return ()
1400 Just docs -> addModDoc syntax mname docs
1403 -- Finally, write an ibc if checking was successful
1404 ok <- noErrors
1405 when ok $
1406 idrisCatch (do writeIBC f ibc; clearIBC)
1407 (\c -> return ()) -- failure is harmless
1408 i <- getIState
1409 putIState (i { default_total = def_total,
1410 hide_list = [] })
1411 return ()
1412 where
1413 namespaces :: [String] -> [PDecl] -> [PDecl]
1414 namespaces [] ds = ds
1415 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1417 toMutual :: PDecl -> PDecl
1418 toMutual m@(PMutual _ d) = m
1419 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1420 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1421 case x of
1422 PClauses{} -> r
1423 PClass{} -> r
1424 PInstance{} -> r
1425 _ -> x
1427 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1428 addModDoc syn mname docs =
1429 do ist <- getIState
1430 docs' <- elabDocTerms recinfo (parsedDocs ist)
1431 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1432 putIState ist { idris_moduledocs = modDocs' }
1433 addIBC (IBCModDocs docName)
1434 where
1435 docName = NS modDocName (map T.pack (reverse mname))
1436 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1438{- | Adds names to hide list -}
1439addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1440addHides xs = do i <- getIState
1441 let defh = default_access i
1442 let (hs, as) = partition isNothing xs
1443 unless (null as) $
1444 mapM_ doHide
1445 (map (\ (n, _) -> (n, defh)) hs ++
1446 map (\ (n, Just a) -> (n, a)) as)
1447 where isNothing (_, Nothing) = True
1448 isNothing _ = False
1450 doHide (n, a) = do setAccessibility n a
1451 addIBC (IBCAccess n a)