git.iko.soy/Idris-dev
on b4dbebd help sign in
Idris-dev/src/Idris/Parser.hs
1475 lines 53 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.Elab.Term
29import Idris.ElabDecls
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 Util.System (readSource, writeSource)
47import qualified Util.Pretty as P
49import Idris.Core.TT
50import Idris.Core.Evaluate
52import Control.Applicative hiding (Const)
53import Control.Monad
54import Control.Monad.State.Strict
56import Data.Function
57import Data.Maybe
58import qualified Data.List.Split as Spl
59import Data.List
60import Data.Monoid
61import Data.Char
62import Data.Ord
63import Data.Generics.Uniplate.Data (descendM)
64import qualified Data.Map as M
65import qualified Data.HashSet as HS
66import qualified Data.Text as T
67import qualified Data.ByteString.UTF8 as UTF8
68import qualified Data.Set as S
70import Debug.Trace
72import System.FilePath
73import System.IO
75{-
77 grammar shortcut notation:
78 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)
79 RULE? = optional rule (i.e. RULE or nothing)
80 RULE* = repeated rule (i.e. RULE zero or more times)
81 RULE+ = repeated rule with at least one match (i.e. RULE one or more times)
82 RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)
83 RULE{n} = rule repeated n times
85-}
87{- * Main grammar -}
89{- | Parses module definition
92 ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;
94-}
95moduleHeader :: IdrisParser (Maybe (Docstring ()), [String])
96moduleHeader = try (do docs <- optional docComment
97 noArgs docs
98 reserved "module"
99 i <- identifier
100 option ';' (lchar ';')
101 return (fmap fst docs, moduleName i))
102 <|> try (do lchar '%'; reserved "unqualified"
103 return (Nothing, []))
104 <|> return (Nothing, moduleName "Main")
105 where moduleName x = case span (/='.') x of
106 (x, "") -> [x]
107 (x, '.':y) -> x : moduleName y
108 noArgs (Just (_, args)) | not (null args) = fail "Modules do not take arguments"
109 noArgs _ = return ()
111{- | Parses an import statement
114 Import ::= 'import' Identifier_t ';'?;
116 -}
117import_ :: IdrisParser (Bool, String, Maybe String, FC)
118import_ = do fc <- getFC
119 reserved "import"
120 reexport <- option False (do reserved "public"; return True)
121 id <- identifier
122 newName <- optional (reserved "as" *> identifier)
123 option ';' (lchar ';')
124 return (reexport, toPath id, toPath <$> newName, fc)
125 <?> "import statement"
126 where toPath = foldl1' (</>) . Spl.splitOn "."
128{- | Parses program source
131 Prog ::= Decl* EOF;
133 -}
134prog :: SyntaxInfo -> IdrisParser [PDecl]
135prog syn = do whiteSpace
136 decls <- many (decl syn)
137 let c = (concat decls)
138 case maxline syn of
139 Nothing -> do notOpenBraces; eof
140 _ -> return ()
141 ist <- get
142 fc <- getFC
143 put ist { idris_parsedSpan = Just (FC (fc_fname fc) (0,0) (fc_end fc)),
144 ibc_write = IBCParsedRegion fc : ibc_write ist }
145 return c
147{-| Parses a top-level declaration
150Decl ::=
151 Decl'
152 | Using
153 | Params
154 | Mutual
155 | Namespace
156 | Class
157 | Instance
158 | DSL
159 | Directive
160 | Provider
161 | Transform
162 | Import!
163 ;
165-}
166decl :: SyntaxInfo -> IdrisParser [PDecl]
167decl syn = do fc <- getFC
168 -- if we're after maxline, stop here
169 let continue = case maxline syn of
170 Nothing -> True
171 Just l -> if fst (fc_end fc) > l
172 then mut_nesting syn /= 0
173 else True
174 if continue then do notEndBlock
175 declBody
176 else fail "End of readable input"
177 where declBody :: IdrisParser [PDecl]
178 declBody = declBody'
179 <|> using_ syn
180 <|> params syn
181 <|> mutual syn
182 <|> namespace syn
183 <|> class_ syn
184 <|> instance_ syn
185 <|> do d <- dsl syn; return [d]
186 <|> directive syn
187 <|> provider syn
188 <|> transform syn
189 <|> do import_; fail "imports must be at top of file"
190 <?> "declaration"
191 declBody' :: IdrisParser [PDecl]
192 declBody' = do d <- decl' syn
193 i <- get
194 let d' = fmap (debindApp syn . (desugar syn i)) d
195 return [d']
197{- | Parses a top-level declaration with possible syntax sugar
200Decl' ::=
201 Fixity
202 | FunDecl'
203 | Data
204 | Record
205 | SyntaxDecl
206 ;
208-}
209decl' :: SyntaxInfo -> IdrisParser PDecl
210decl' syn = fixity
211 <|> syntaxDecl syn
212 <|> fnDecl' syn
213 <|> data_ syn
214 <|> record syn
215 <?> "declaration"
217{- | Parses a syntax extension declaration (and adds the rule to parser state)
220 SyntaxDecl ::= SyntaxRule;
222-}
223syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
224syntaxDecl syn = do s <- syntaxRule syn
225 i <- get
226 put (i `addSyntax` s)
227 fc <- getFC
228 return (PSyntax fc s)
230-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.
231addSyntax :: IState -> Syntax -> IState
232addSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
233 syntax_keywords = ks ++ ns,
234 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc }
235 where rs = syntax_rules i
236 ns = syntax_keywords i
237 ibc = ibc_write i
238 ks = map show (syntaxNames s)
240-- | Like 'addSyntax', but no effect on the IBC.
241addReplSyntax :: IState -> Syntax -> IState
242addReplSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
243 syntax_keywords = ks ++ ns }
244 where rs = syntax_rules i
245 ns = syntax_keywords i
246 ks = map show (syntaxNames s)
248{- | Parses a syntax extension declaration
251SyntaxRuleOpts ::= 'term' | 'pattern';
255SyntaxRule ::=
256 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
260SyntaxSym ::= '[' Name_t ']'
261 | '{' Name_t '}'
262 | Name_t
263 | StringLiteral_t
264 ;
266-}
267syntaxRule :: SyntaxInfo -> IdrisParser Syntax
268syntaxRule syn
269 = do sty <- try (do
270 pushIndent
271 sty <- option AnySyntax (do reserved "term"; return TermSyntax
272 <|> do reserved "pattern"; return PatternSyntax)
273 reserved "syntax"
274 return sty)
275 syms <- some syntaxSym
276 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
277 let ns = mapMaybe getName syms
278 when (length ns /= length (nub ns))
279 $ unexpected "repeated variable in syntax rule"
280 lchar '='
281 tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]
282 terminator
283 return (Rule (mkSimple syms) tm sty)
284 where
285 isExpr (Expr _) = True
286 isExpr _ = False
287 getName (Expr n) = Just n
288 getName _ = Nothing
289 -- Can't parse two full expressions (i.e. expressions with application) in a row
290 -- so change them both to a simple expression
291 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
292 mkSimple xs = mkSimple' xs
294 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
295 mkSimple es
296 -- Can't parse a full expression followed by operator like characters due to ambiguity
297 mkSimple' (Expr e : Symbol s : es)
298 | takeWhile (`elem` opChars) ts /= "" && ts `notElem` invalidOperators = SimpleExpr e : Symbol s : mkSimple' es
299 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s
300 mkSimple' (e : es) = e : mkSimple' es
301 mkSimple' [] = []
303 -- Prevent syntax variable capture by making all binders under syntax unique
304 -- (the ol' Common Lisp GENSYM approach)
305 uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
306 uniquifyBinders userNames = fixBind []
307 where
308 fixBind :: [(Name, Name)] -> PTerm -> IdrisParser PTerm
309 fixBind rens (PRef fc n) | Just n' <- lookup n rens =
310 return $ PRef fc n'
311 fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =
312 return $ PPatvar fc n'
313 fixBind rens (PLam fc n ty body)
314 | n `elem` userNames = liftM2 (PLam fc n) (fixBind rens ty) (fixBind rens body)
315 | otherwise =
316 do ty' <- fixBind rens ty
317 n' <- gensym n
318 body' <- fixBind ((n,n'):rens) body
319 return $ PLam fc n' ty' body'
320 fixBind rens (PPi plic n argTy body)
321 | n `elem` userNames = liftM2 (PPi plic n) (fixBind rens argTy) (fixBind rens body)
322 | otherwise =
323 do ty' <- fixBind rens argTy
324 n' <- gensym n
325 body' <- fixBind ((n,n'):rens) body
326 return $ (PPi plic n' ty' body')
327 fixBind rens (PLet fc n ty val body)
328 | n `elem` userNames = liftM3 (PLet fc n)
329 (fixBind rens ty)
330 (fixBind rens val)
331 (fixBind rens body)
332 | otherwise =
333 do ty' <- fixBind rens ty
334 val' <- fixBind rens val
335 n' <- gensym n
336 body' <- fixBind ((n,n'):rens) body
337 return $ (PLet fc n' ty' val' body')
338 fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =
339 return $ PMatchApp fc n'
340 fixBind rens x = descendM (fixBind rens) x
342 gensym :: Name -> IdrisParser Name
343 gensym n = do ist <- get
344 let idx = idris_name ist
345 put ist { idris_name = idx + 1 }
346 return $ sMN idx (show n)
348{- | Parses a syntax symbol (either binding variable, keyword or expression)
351SyntaxSym ::= '[' Name_t ']'
352 | '{' Name_t '}'
353 | Name_t
354 | StringLiteral_t
355 ;
357 -}
358syntaxSym :: IdrisParser SSymbol
359syntaxSym = try (do lchar '['; n <- name; lchar ']'
360 return (Expr n))
361 <|> try (do lchar '{'; n <- name; lchar '}'
362 return (Binding n))
363 <|> do n <- iName []
364 return (Keyword n)
365 <|> do sym <- stringLiteral
366 return (Symbol sym)
367 <?> "syntax symbol"
369{- | Parses a function declaration with possible syntax sugar
372 FunDecl ::= FunDecl';
374-}
375fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
376fnDecl syn = try (do notEndBlock
377 d <- fnDecl' syn
378 i <- get
379 let d' = fmap (desugar syn i) d
380 return [d']) <?> "function declaration"
382{-| Parses a function declaration
385 FunDecl' ::=
386 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
387 | Postulate
388 | Pattern
389 | CAF
390 ;
392-}
393fnDecl' :: SyntaxInfo -> IdrisParser PDecl
394fnDecl' syn = checkFixity $
395 do (doc, argDocs, fc, opts', n, acc) <- try (do
396 pushIndent
397 (doc, argDocs) <- docstring syn
398 ist <- get
399 let initOpts = if default_total ist
400 then [TotalFn]
401 else []
402 opts <- fnOpts initOpts
403 acc <- optional accessibility
404 opts' <- fnOpts opts
405 n_in <- fnName
406 let n = expandNS syn n_in
407 fc <- getFC
408 lchar ':'
409 return (doc, argDocs, fc, opts', n, acc))
410 ty <- typeExpr (allowImp syn)
411 terminator
412 addAcc n acc
413 return (PTy doc argDocs syn fc opts' n ty)
414 <|> postulate syn
415 <|> caf syn
416 <|> pattern syn
417 <?> "function declaration"
418 where checkFixity :: IdrisParser PDecl -> IdrisParser PDecl
419 checkFixity p = do decl <- p
420 case getName decl of
421 Nothing -> return decl
422 Just n -> do fOk <- fixityOK n
423 unless fOk . fail $
424 "Missing fixity declaration for " ++ show n
425 return decl
426 getName (PTy _ _ _ _ _ n _) = Just n
427 getName _ = Nothing
428 fixityOK (NS n _) = fixityOK n
429 fixityOK (UN n) | all (flip elem opChars) (str n) =
430 do fixities <- fmap idris_infixes get
431 return . elem (str n) . map (\ (Fix _ op) -> op) $ fixities
432 | otherwise = return True
433 fixityOK _ = return True
435{-| Parses function options given initial options
438FnOpts ::= 'total'
439 | 'partial'
440 | 'implicit'
441 | '%' 'no_implicit'
442 | '%' 'assert_total'
443 | '%' 'error_handler'
444 | '%' 'reflection'
445 | '%' 'specialise' '[' NameTimesList? ']'
446 ;
450NameTimes ::= FnName Natural?;
454NameTimesList ::=
455 NameTimes
456 | NameTimes ',' NameTimesList
457 ;
459-}
460-- FIXME: Check compatability for function options (i.e. partal/total)
461--
462-- Issue #1574 on the issue tracker.
463-- https://github.com/idris-lang/Idris-dev/issues/1574
464fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
465fnOpts opts
466 = do reserved "total"; fnOpts (TotalFn : opts)
467 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
468 <|> do reserved "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))
469 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;
470 fnOpts (CExport c : opts)
471 <|> do try (lchar '%' *> reserved "no_implicit");
472 fnOpts (NoImplicit : opts)
473 <|> do try (lchar '%' *> reserved "inline");
474 fnOpts (Inlinable : opts)
475 <|> do try (lchar '%' *> reserved "assert_total");
476 fnOpts (AssertTotal : opts)
477 <|> do try (lchar '%' *> reserved "error_handler");
478 fnOpts (ErrorHandler : opts)
479 <|> do try (lchar '%' *> reserved "error_reverse");
480 fnOpts (ErrorReverse : opts)
481 <|> do try (lchar '%' *> reserved "reflection");
482 fnOpts (Reflection : opts)
483 <|> do try (lchar '%' *> reserved "hint");
484 fnOpts (AutoHint : opts)
485 <|> do lchar '%'; reserved "specialise";
486 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
487 fnOpts (Specialise ns : opts)
488 <|> do reserved "implicit"; fnOpts (Implicit : opts)
489 <|> return opts
490 <?> "function modifier"
491 where nameTimes :: IdrisParser (Name, Maybe Int)
492 nameTimes = do n <- fnName
493 t <- option Nothing (do reds <- natural
494 return (Just (fromInteger reds)))
495 return (n, t)
497{- | Parses a postulate
500Postulate ::=
501 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
502 ;
504-}
505postulate :: SyntaxInfo -> IdrisParser PDecl
506postulate syn = do (doc, ext)
507 <- try $ do (doc, _) <- docstring syn
508 pushIndent
509 ext <- ppostDecl
510 return (doc, ext)
511 ist <- get
512 let initOpts = if default_total ist
513 then [TotalFn]
514 else []
515 opts <- fnOpts initOpts
516 acc <- optional accessibility
517 opts' <- fnOpts opts
518 n_in <- fnName
519 let n = expandNS syn n_in
520 lchar ':'
521 ty <- typeExpr (allowImp syn)
522 fc <- getFC
523 terminator
524 addAcc n acc
525 return (PPostulate ext doc syn fc opts' n ty)
526 <?> "postulate"
527 where ppostDecl = do reserved "postulate"; return False
528 <|> do lchar '%'; reserved "extern"; return True
529{- | Parses a using declaration
532Using ::=
533 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
534 ;
536 -}
537using_ :: SyntaxInfo -> IdrisParser [PDecl]
538using_ syn =
539 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
540 openBlock
541 let uvars = using syn
542 ds <- many (decl (syn { using = uvars ++ ns }))
543 closeBlock
544 return (concat ds)
545 <?> "using declaration"
547{- | Parses a parameters declaration
550Params ::=
551 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
552 ;
554 -}
555params :: SyntaxInfo -> IdrisParser [PDecl]
556params syn =
557 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
558 openBlock
559 let pvars = syn_params syn
560 ds <- many (decl syn { syn_params = pvars ++ ns })
561 closeBlock
562 fc <- getFC
563 return [PParams fc ns (concat ds)]
564 <?> "parameters declaration"
566{- | Parses a mutual declaration (for mutually recursive functions)
569Mutual ::=
570 'mutual' OpenBlock Decl* CloseBlock
571 ;
573-}
574mutual :: SyntaxInfo -> IdrisParser [PDecl]
575mutual syn =
576 do reserved "mutual"
577 openBlock
578 let pvars = syn_params syn
579 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
580 closeBlock
581 fc <- getFC
582 return [PMutual fc (concat ds)]
583 <?> "mutual block"
585{-| Parses a namespace declaration
588Namespace ::=
589 'namespace' identifier OpenBlock Decl+ CloseBlock
590 ;
592-}
593namespace :: SyntaxInfo -> IdrisParser [PDecl]
594namespace syn =
595 do reserved "namespace"; n <- identifier;
596 openBlock
597 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
598 closeBlock
599 return [PNamespace n (concat ds)]
600 <?> "namespace declaration"
602{- | Parses a methods block (for instances)
605 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
607-}
608instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
609instanceBlock syn = do reserved "where"
610 openBlock
611 ds <- many (fnDecl syn)
612 closeBlock
613 return (concat ds)
614 <?> "instance block"
616{- | Parses a methods and instances block (for type classes)
619MethodOrInstance ::=
620 FnDecl
621 | Instance
622 ;
626ClassBlock ::=
627 'where' OpenBlock MethodOrInstance* CloseBlock
628 ;
630-}
631classBlock :: SyntaxInfo -> IdrisParser [PDecl]
632classBlock syn = do reserved "where"
633 openBlock
634 ds <- many (notEndBlock >> instance_ syn <|> fnDecl syn)
635 closeBlock
636 return (concat ds)
637 <?> "class block"
639{-| Parses a type class declaration
642ClassArgument ::=
643 Name
644 | '(' Name ':' Expr ')'
645 ;
649Class ::=
650 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
651 ;
653-}
654class_ :: SyntaxInfo -> IdrisParser [PDecl]
655class_ syn = do (doc, argDocs, acc)
656 <- try (do (doc, argDocs) <- docstring syn
657 acc <- optional accessibility
658 reserved "class"
659 return (doc, argDocs, acc))
660 fc <- getFC
661 cons <- constraintList syn
662 n_in <- fnName
663 let n = expandNS syn n_in
664 cs <- many carg
665 fds <- option (map fst cs) fundeps
666 ds <- option [] (classBlock syn)
667 accData acc n (concatMap declared ds)
668 return [PClass doc syn fc cons n cs argDocs fds ds]
669 <?> "type-class declaration"
670 where
671 fundeps :: IdrisParser [Name]
672 fundeps = do lchar '|'; sepBy name (lchar ',')
674 carg :: IdrisParser (Name, PTerm)
675 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
676 return (i, ty)
677 <|> do i <- name;
678 return (i, PType)
680{- | Parses a type class instance declaration
683 Instance ::=
684 DocComment_t? 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
685 ;
689InstanceName ::= '[' Name ']';
691-}
692instance_ :: SyntaxInfo -> IdrisParser [PDecl]
693instance_ syn = do (doc, argDocs)
694 <- try (docstring syn <* reserved "instance")
695 fc <- getFC
696 en <- optional instanceName
697 cs <- constraintList syn
698 cn <- fnName
699 args <- many (simpleExpr syn)
700 let sc = PApp fc (PRef fc cn) (map pexp args)
701 let t = bindList (PPi constraint) cs sc
702 ds <- option [] (instanceBlock syn)
703 return [PInstance doc argDocs syn fc cs cn args t en ds]
704 <?> "instance declaration"
705 where instanceName :: IdrisParser Name
706 instanceName = do lchar '['; n_in <- fnName; lchar ']'
707 let n = expandNS syn n_in
708 return n
709 <?> "instance name"
712-- | Parse a docstring
713docstring :: SyntaxInfo
714 -> IdrisParser (Docstring (Either Err PTerm),
715 [(Name,Docstring (Either Err PTerm))])
716docstring syn = do (doc, argDocs) <- option noDocs docComment
717 ist <- get
718 let doc' = annotCode (tryFullExpr syn ist) doc
719 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
720 | (n, d) <- argDocs ]
721 return (doc', argDocs')
724{- | Parses a using declaration list
727UsingDeclList ::=
728 UsingDeclList'
729 | NameList TypeSig
730 ;
734UsingDeclList' ::=
735 UsingDecl
736 | UsingDecl ',' UsingDeclList'
737 ;
741NameList ::=
742 Name
743 | Name ',' NameList
744 ;
746-}
747usingDeclList :: SyntaxInfo -> IdrisParser [Using]
748usingDeclList syn
749 = try (sepBy1 (usingDecl syn) (lchar ','))
750 <|> do ns <- sepBy1 name (lchar ',')
751 lchar ':'
752 t <- typeExpr (disallowImp syn)
753 return (map (\x -> UImplicit x t) ns)
754 <?> "using declaration list"
756{- |Parses a using declaration
759UsingDecl ::=
760 FnName TypeSig
761 | FnName FnName+
762 ;
764-}
765usingDecl :: SyntaxInfo -> IdrisParser Using
766usingDecl syn = try (do x <- fnName
767 lchar ':'
768 t <- typeExpr (disallowImp syn)
769 return (UImplicit x t))
770 <|> do c <- fnName
771 xs <- some fnName
772 return (UConstraint c xs)
773 <?> "using declaration"
775{- | Parse a clause with patterns
778Pattern ::= Clause;
780-}
781pattern :: SyntaxInfo -> IdrisParser PDecl
782pattern syn = do fc <- getFC
783 clause <- clause syn
784 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
785 <?> "pattern"
787{- | Parse a constant applicative form declaration
790CAF ::= 'let' FnName '=' Expr Terminator;
792-}
793caf :: SyntaxInfo -> IdrisParser PDecl
794caf syn = do reserved "let"
795 n_in <- fnName; let n = expandNS syn n_in
796 lchar '='
797 t <- expr syn
798 terminator
799 fc <- getFC
800 return (PCAF fc n t)
801 <?> "constant applicative form declaration"
803{- | Parse an argument expression
806ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
808-}
809argExpr :: SyntaxInfo -> IdrisParser PTerm
810argExpr syn = let syn' = syn { inPattern = True } in
811 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
812 <?> "argument expression"
814{- | Parse a right hand side of a function
817RHS ::= '=' Expr
818 | '?=' RHSName? Expr
819 | Impossible
820 ;
824RHSName ::= '{' FnName '}';
826-}
827rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
828rhs syn n = do lchar '='; expr syn
829 <|> do symbol "?=";
830 fc <- getFC
831 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
832 return n)
833 r <- expr syn
834 return (addLet fc name r)
835 <|> impossible
836 <?> "function right hand side"
837 where mkN :: Name -> Name
838 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
839 then sUN "infix_op_lemma_1"
840 else sUN (str x++"_lemma_1")
841 mkN (NS x n) = NS (mkN x) n
842 n' :: Name
843 n' = mkN n
844 addLet :: FC -> Name -> PTerm -> PTerm
845 addLet fc nm (PLet fc' n ty val r) = PLet fc' n ty val (addLet fc nm r)
846 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
847 where addLetC (l, r) = (l, addLet fc nm r)
848 addLet fc nm r = (PLet fc (sUN "value") Placeholder r (PMetavar nm))
850{- |Parses a function clause
853RHSOrWithBlock ::= RHS WhereOrTerminator
854 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
855 ;
859Clause ::= WExpr+ RHSOrWithBlock
860 | SimpleExpr '<==' FnName RHS WhereOrTerminator
861 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
862 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
863 ;
867ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
871WhereOrTerminator ::= WhereBlock | Terminator;
873-}
874clause :: SyntaxInfo -> IdrisParser PClause
875clause syn
876 = do wargs <- try (do pushIndent; some (wExpr syn))
877 fc <- getFC
878 ist <- get
879 n <- case lastParse ist of
880 Just t -> return t
881 Nothing -> fail "Invalid clause"
882 (do r <- rhs syn n
883 let ctxt = tt_ctxt ist
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 return $ PClauseR fc wargs r wheres) <|> (do
891 popIndent
892 reserved "with"
893 wval <- simpleExpr syn
894 pn <- optProof
895 openBlock
896 ds <- some $ fnDecl syn
897 let withs = concat ds
898 closeBlock
899 return $ PWithR fc wargs wval pn withs)
900 <|> do ty <- try (do pushIndent
901 ty <- simpleExpr syn
902 symbol "<=="
903 return ty)
904 fc <- getFC
905 n_in <- fnName; let n = expandNS syn n_in
906 r <- rhs syn n
907 ist <- get
908 let ctxt = tt_ctxt ist
909 let wsyn = syn { syn_namespace = [] }
910 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
911 popIndent
912 return x,
913 do terminator
914 return ([], [])]
915 let capp = PLet fc (sMN 0 "match")
916 ty
917 (PMatchApp fc n)
918 (PRef fc (sMN 0 "match"))
919 ist <- get
920 put (ist { lastParse = Just n })
921 return $ PClause fc n capp [] r wheres
922 <|> do (l, op) <- try (do
923 pushIndent
924 l <- argExpr syn
925 op <- operator
926 when (op == "=" || op == "?=" ) $
927 fail "infix clause definition with \"=\" and \"?=\" not supported "
928 return (l, op))
929 let n = expandNS syn (sUN op)
930 r <- argExpr syn
931 fc <- getFC
932 wargs <- many (wExpr syn)
933 (do rs <- rhs syn n
934 let wsyn = syn { syn_namespace = [] }
935 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
936 popIndent
937 return x,
938 do terminator
939 return ([], [])]
940 ist <- get
941 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
942 put (ist { lastParse = Just n })
943 return $ PClause fc n capp wargs rs wheres) <|> (do
944 popIndent
945 reserved "with"
946 wval <- bracketed syn
947 pn <- optProof
948 openBlock
949 ds <- some $ fnDecl syn
950 closeBlock
951 ist <- get
952 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
953 let withs = map (fillLHSD n capp wargs) $ concat ds
954 put (ist { lastParse = Just n })
955 return $ PWith fc n capp wargs wval pn withs)
956 <|> do pushIndent
957 n_in <- fnName; let n = expandNS syn n_in
958 cargs <- many (constraintArg syn)
959 fc <- getFC
960 args <- many (try (implicitArg (syn { inPattern = True } ))
961 <|> (fmap pexp (argExpr syn)))
962 wargs <- many (wExpr syn)
963 let capp = PApp fc (PRef fc n)
964 (cargs ++ args)
965 (do r <- rhs syn n
966 ist <- get
967 let ctxt = tt_ctxt ist
968 let wsyn = syn { syn_namespace = [] }
969 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
970 popIndent
971 return x,
972 do terminator
973 return ([], [])]
974 ist <- get
975 put (ist { lastParse = Just n })
976 return $ PClause fc n capp wargs r wheres) <|> (do
977 reserved "with"
978 ist <- get
979 put (ist { lastParse = Just n })
980 wval <- bracketed syn
981 pn <- optProof
982 openBlock
983 ds <- some $ fnDecl syn
984 let withs = map (fillLHSD n capp wargs) $ concat ds
985 closeBlock
986 popIndent
987 return $ PWith fc n capp wargs wval pn withs)
988 <?> "function clause"
989 where
990 optProof = option Nothing (do reserved "proof"
991 n <- fnName
992 return (Just n))
994 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
995 fillLHS n capp owargs (PClauseR fc wargs v ws)
996 = PClause fc n capp (owargs ++ wargs) v ws
997 fillLHS n capp owargs (PWithR fc wargs v pn ws)
998 = PWith fc n capp (owargs ++ wargs) v pn
999 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1000 fillLHS _ _ _ c = c
1002 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
1003 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1004 fillLHSD n c a x = x
1006{-| Parses with pattern
1009WExpr ::= '|' Expr';
1012wExpr :: SyntaxInfo -> IdrisParser PTerm
1013wExpr syn = do lchar '|'
1014 expr' (syn { inPattern = True })
1015 <?> "with pattern"
1017{- | Parses a where block
1020WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
1023whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
1024whereBlock n syn
1025 = do reserved "where"
1026 ds <- indentedBlock1 (decl syn)
1027 let dns = concatMap (concatMap declared) ds
1028 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1029 <?> "where block"
1031{- |Parses a code generation target language name
1034Codegen ::= 'C'
1035 | 'Java'
1036 | 'JavaScript'
1037 | 'Node'
1038 | 'LLVM'
1039 | 'Bytecode'
1043codegen_ :: IdrisParser Codegen
1044codegen_ = do n <- identifier; return (Via (map toLower n))
1045 <|> do reserved "Bytecode"; return Bytecode
1046 <?> "code generation language"
1048{- |Parses a compiler directive
1050StringList ::=
1051 String
1052 | String ',' StringList
1057Directive ::= '%' Directive';
1061Directive' ::= 'lib' CodeGen String_t
1062 | 'link' CodeGen String_t
1063 | 'flag' CodeGen String_t
1064 | 'include' CodeGen String_t
1065 | 'hide' Name
1066 | 'freeze' Name
1067 | 'access' Accessibility
1068 | 'default' Totality
1069 | 'logging' Natural
1070 | 'dynamic' StringList
1071 | 'name' Name NameList
1072 | 'error_handlers' Name NameList
1073 | 'language' 'TypeProviders'
1074 | 'language' 'ErrorReflection'
1078directive :: SyntaxInfo -> IdrisParser [PDecl]
1079directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
1080 return [PDirective (DLib cgn lib)]
1081 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
1082 return [PDirective (DLink cgn obj)]
1083 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_; flag <- stringLiteral
1084 return [PDirective (DFlag cgn flag)]
1085 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
1086 return [PDirective (DInclude cgn hdr)]
1087 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
1088 return [PDirective (DHide n)]
1089 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
1090 return [PDirective (DFreeze n)]
1091 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1092 return [PDirective (DAccess acc)]
1093 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1094 i <- get
1095 put (i { default_total = tot } )
1096 return [PDirective (DDefault tot)]
1097 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
1098 return [PDirective (DLogging i)]
1099 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
1100 return [PDirective (DDynamicLibs libs)]
1101 <|> do try (lchar '%' *> reserved "name")
1102 ty <- fnName
1103 ns <- sepBy1 name (lchar ',')
1104 return [PDirective (DNameHint ty ns)]
1105 <|> do try (lchar '%' *> reserved "error_handlers")
1106 fn <- fnName
1107 arg <- fnName
1108 ns <- sepBy1 name (lchar ',')
1109 return [PDirective (DErrorHandlers fn arg ns) ]
1110 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1111 return [PDirective (DLanguage ext)]
1112 <|> do fc <- getFC
1113 try (lchar '%' *> reserved "used")
1114 fn <- fnName
1115 arg <- iName []
1116 return [PDirective (DUsed fc fn arg)]
1117 <?> "directive"
1119pLangExt :: IdrisParser LanguageExt
1120pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1121 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1123{- | Parses a totality
1126Totality ::= 'partial' | 'total'
1130totality :: IdrisParser Bool
1131totality
1132 = do reserved "total"; return True
1133 <|> do reserved "partial"; return False
1135{- | Parses a type provider
1138Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1139ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1141 -}
1142provider :: SyntaxInfo -> IdrisParser [PDecl]
1143provider syn = do doc <- try (do (doc, _) <- docstring syn
1144 lchar '%'
1145 reserved "provide"
1146 return doc)
1147 provideTerm doc <|> providePostulate doc
1148 <?> "type provider"
1149 where provideTerm doc =
1150 do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1151 fc <- getFC
1152 reserved "with"
1153 e <- expr syn <?> "provider expression"
1154 return [PProvider doc syn fc (ProvTerm t e) n]
1155 providePostulate doc =
1156 do reserved "postulate"
1157 n <- fnName
1158 fc <- getFC
1159 reserved "with"
1160 e <- expr syn <?> "provider expression"
1161 return [PProvider doc syn fc (ProvPostulate e) n]
1163{- | Parses a transform
1166Transform ::= '%' 'transform' Expr '==>' Expr
1169transform :: SyntaxInfo -> IdrisParser [PDecl]
1170transform syn = do try (lchar '%' *> reserved "transform")
1171 -- leave it unchecked, until we work out what this should
1172 -- actually mean...
1173-- safety <- option True (do reserved "unsafe"
1174-- return False)
1175 l <- expr syn
1176 fc <- getFC
1177 symbol "==>"
1178 r <- expr syn
1179 return [PTransform fc False l r]
1180 <?> "transform"
1183{- * Loading and parsing -}
1184{- | Parses an expression from input -}
1185parseExpr :: IState -> String -> Result PTerm
1186parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1188{- | Parses a constant form input -}
1189parseConst :: IState -> String -> Result Const
1190parseConst st = runparser constant st "(input)"
1192{- | Parses a tactic from input -}
1193parseTactic :: IState -> String -> Result PTactic
1194parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1196-- | Parse module header and imports
1197parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta)
1198parseImports fname input
1199 = do i <- getIState
1200 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1201 Failure err -> fail (show err)
1202 Success (x, i) -> do putIState i
1203 return x
1204 where imports :: IdrisParser ((Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta), IState)
1205 imports = do whiteSpace
1206 (mdoc, mname) <- moduleHeader
1207 ps <- many import_
1208 mrk <- mark
1209 isEof <- lookAheadMatches eof
1210 let mrk' = if isEof
1211 then Nothing
1212 else Just mrk
1213 i <- get
1214 return ((mdoc, mname, ps, mrk'), i)
1216-- | There should be a better way of doing this...
1217findFC :: Doc -> (FC, String)
1218findFC x = let s = show (plain x) in
1219 case span (/= ':') s of
1220 (failname, ':':rest) -> case span isDigit rest of
1221 (line, ':':rest') -> case span isDigit rest' of
1222 (col, ':':msg) -> let pos = (read line, read col) in
1223 (FC failname pos pos, msg)
1225-- | Check if the coloring matches the options and corrects if necessary
1226fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1227fixColour False doc = ANSI.plain doc
1228fixColour True doc = doc
1230-- | A program is a list of declarations, possibly with associated
1231-- documentation strings.
1232parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1233 Idris [PDecl]
1234parseProg syn fname input mrk
1235 = do i <- getIState
1236 case runparser mainProg i fname input of
1237 Failure doc -> do -- FIXME: Get error location from trifecta
1238 -- this can't be the solution!
1239 -- Issue #1575 on the issue tracker.
1240 -- https://github.com/idris-lang/Idris-dev/issues/1575
1241 let (fc, msg) = findFC doc
1242 i <- getIState
1243 case idris_outputmode i of
1244 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1245 IdeMode n h -> iWarn fc (P.text msg)
1246 putIState (i { errSpan = Just fc })
1247 return []
1248 Success (x, i) -> do putIState i
1249 reportParserWarnings
1250 return $ collect x
1251 where mainProg :: IdrisParser ([PDecl], IState)
1252 mainProg = case mrk of
1253 Nothing -> do i <- get; return ([], i)
1254 Just mrk -> do
1255 release mrk
1256 ds <- prog syn
1257 i' <- get
1258 return (ds, i')
1260{- | Load idris module and show error if something wrong happens -}
1261loadModule :: FilePath -> Idris (Maybe String)
1262loadModule f
1263 = idrisCatch (loadModule' f)
1264 (\e -> do setErrSpan (getErrSpan e)
1265 ist <- getIState
1266 iWarn (getErrSpan e) $ pprintErr ist e
1267 return Nothing)
1269{- | Load idris module -}
1270loadModule' :: FilePath -> Idris (Maybe String)
1271loadModule' f
1272 = do i <- getIState
1273 let file = takeWhile (/= ' ') f
1274 ibcsd <- valIBCSubDir i
1275 ids <- allImportDirs
1276 fp <- findImport ids ibcsd file
1277 if file `elem` imported i
1278 then do iLOG $ "Already read " ++ file
1279 return Nothing
1280 else do putIState (i { imported = file : imported i })
1281 case fp of
1282 IDR fn -> loadSource False fn Nothing
1283 LIDR fn -> loadSource True fn Nothing
1284 IBC fn src ->
1285 idrisCatch (loadIBC True fn)
1286 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1287 case src of
1288 IDR sfn -> loadSource False sfn Nothing
1289 LIDR sfn -> loadSource True sfn Nothing)
1290 return $ Just file
1292{- | Load idris code from file -}
1293loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()
1294loadFromIFile reexp i@(IBC fn src) maxline
1295 = do iLOG $ "Skipping " ++ getSrcFile i
1296 idrisCatch (loadIBC reexp fn)
1297 (\err -> ierror $ LoadingFailed fn err)
1298 where
1299 getSrcFile (IDR fn) = fn
1300 getSrcFile (LIDR fn) = fn
1301 getSrcFile (IBC f src) = getSrcFile src
1303loadFromIFile _ (IDR fn) maxline = loadSource' False fn maxline
1304loadFromIFile _ (LIDR fn) maxline = loadSource' True fn maxline
1306{-| Load idris source code and show error if something wrong happens -}
1307loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1308loadSource' lidr r maxline
1309 = idrisCatch (loadSource lidr r maxline)
1310 (\e -> do setErrSpan (getErrSpan e)
1311 ist <- getIState
1312 case e of
1313 At f e' -> iWarn f (pprintErr ist e')
1314 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1316{- | Load Idris source code-}
1317loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1318loadSource lidr f toline
1319 = do iLOG ("Reading " ++ f)
1320 i <- getIState
1321 let def_total = default_total i
1322 file_in <- runIO $ readSource f
1323 file <- if lidr then tclift $ unlit f file_in else return file_in
1324 (mdocs, mname, imports_in, pos) <- parseImports f file
1325 ai <- getAutoImports
1326 let imports = map (\n -> (True, n, Just n, emptyFC)) ai ++ imports_in
1327 ids <- allImportDirs
1328 ibcsd <- valIBCSubDir i
1329 mapM_ (\(re, f) ->
1330 do fp <- findImport ids ibcsd f
1331 case fp of
1332 LIDR fn -> ifail $ "No ibc for " ++ f
1333 IDR fn -> ifail $ "No ibc for " ++ f
1334 IBC fn src -> loadIBC True fn)
1335 [(re, fn) | (re, fn, _, _) <- imports]
1336 reportParserWarnings
1338 -- process and check module aliases
1339 let modAliases = M.fromList
1340 [(prep alias, prep realName) | (reexport, realName, Just alias, fc) <- imports]
1341 prep = map T.pack . reverse . Spl.splitOn [pathSeparator]
1342 aliasNames = [(alias, fc) | (_, _, Just alias, fc) <- imports]
1343 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1344 case map head . filter ((/= 1) . length) $ histogram of
1345 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1346 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1348 i <- getIState
1349 putIState (i { default_access = Hidden, module_aliases = modAliases })
1350 clearIBC -- start a new .ibc file
1351 -- record package info in .ibc
1352 imps <- allImportDirs
1353 mapM_ addIBC (map IBCImportDir imps)
1354 mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports]
1355 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1356 maxline = toline }
1357 ist <- getIState
1358 -- Save the span from parsing the module header, because
1359 -- an empty program parse might obliterate it.
1360 let oldSpan = idris_parsedSpan ist
1361 ds' <- parseProg syntax f file pos
1363 case (ds', oldSpan) of
1364 ([], Just fc) ->
1365 -- If no program elements were parsed, we dind't
1366 -- get a loaded region in the IBC file. That
1367 -- means we need to add it back.
1368 do ist <- getIState
1369 putIState ist { idris_parsedSpan = oldSpan
1370 , ibc_write = IBCParsedRegion fc :
1371 ibc_write ist
1373 _ -> return ()
1375 -- Parsing done, now process declarations
1377 let ds = namespaces mname ds'
1378 logLvl 3 (show $ showDecls verbosePPOption ds)
1379 i <- getIState
1380 logLvl 10 (show (toAlist (idris_implicits i)))
1381 logLvl 3 (show (idris_infixes i))
1382 -- Now add all the declarations to the context
1383 v <- verbose
1384 when v $ iputStrLn $ "Type checking " ++ f
1385 -- we totality check after every Mutual block, so if
1386 -- anything is a single definition, wrap it in a
1387 -- mutual block on its own
1388 elabDecls toplevel (map toMutual ds)
1389 i <- getIState
1390 -- simplify every definition do give the totality checker
1391 -- a better chance
1392 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1393 updateContext (simplifyCasedef n $ getErasureInfo i))
1394 (map snd (idris_totcheck i))
1395 -- build size change graph from simplified definitions
1396 iLOG "Totality checking"
1397 i <- getIState
1398 mapM_ buildSCG (idris_totcheck i)
1399 mapM_ checkDeclTotality (idris_totcheck i)
1401 -- Redo totality check for deferred names
1402 let deftots = idris_defertotcheck i
1403 iLOG $ "Totality checking " ++ show deftots
1404 mapM_ (\x -> do tot <- getTotality x
1405 case tot of
1406 Total _ -> setTotality x Unchecked
1407 _ -> return ()) (map snd deftots)
1408 mapM_ buildSCG deftots
1409 mapM_ checkDeclTotality deftots
1411 iLOG ("Finished " ++ f)
1412 ibcsd <- valIBCSubDir i
1413 iLOG "Universe checking"
1414 iucheck
1415 let ibc = ibcPathNoFallback ibcsd f
1416 i <- getIState
1417 addHides (hide_list i)
1419 -- Save module documentation if applicable
1420 i <- getIState
1421 case mdocs of
1422 Nothing -> return ()
1423 Just docs -> addModDoc syntax mname docs
1426 -- Finally, write an ibc if checking was successful
1427 ok <- noErrors
1428 when ok $
1429 idrisCatch (do writeIBC f ibc; clearIBC)
1430 (\c -> return ()) -- failure is harmless
1431 i <- getIState
1432 putIState (i { default_total = def_total,
1433 hide_list = [] })
1434 return ()
1435 where
1436 namespaces :: [String] -> [PDecl] -> [PDecl]
1437 namespaces [] ds = ds
1438 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1440 toMutual :: PDecl -> PDecl
1441 toMutual m@(PMutual _ d) = m
1442 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1443 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1444 case x of
1445 PClauses{} -> r
1446 PClass{} -> r
1447 PData{} -> r
1448 PInstance{} -> r
1449 _ -> x
1451 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1452 addModDoc syn mname docs =
1453 do ist <- getIState
1454 docs' <- elabDocTerms recinfo (parsedDocs ist)
1455 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1456 putIState ist { idris_moduledocs = modDocs' }
1457 addIBC (IBCModDocs docName)
1458 where
1459 docName = NS modDocName (map T.pack (reverse mname))
1460 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1462{- | Adds names to hide list -}
1463addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1464addHides xs = do i <- getIState
1465 let defh = default_access i
1466 let (hs, as) = partition isNothing xs
1467 unless (null as) $
1468 mapM_ doHide
1469 (map (\ (n, _) -> (n, defh)) hs ++
1470 map (\ (n, Just a) -> (n, a)) as)
1471 where isNothing (_, Nothing) = True
1472 isNothing _ = False
1474 doHide (n, a) = do setAccessibility n a
1475 addIBC (IBCAccess n a)