git.iko.soy/Idris-dev
on 76ec3fe help sign in
Idris-dev/src/Idris/Parser.hs
1501 lines 55 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 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 (do addLib cgn lib
1081 addIBC (IBCLib cgn lib))]
1082 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
1083 return [PDirective (do dirs <- allImportDirs
1084 o <- liftIO $ findInPath dirs obj
1085 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
1086 addObjectFile cgn o)]
1087 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
1088 flag <- stringLiteral
1089 return [PDirective (do addIBC (IBCCGFlag cgn flag)
1090 addFlag cgn flag)]
1091 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
1092 return [PDirective (do addHdr cgn hdr
1093 addIBC (IBCHeader cgn hdr))]
1094 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
1095 return [PDirective (do setAccessibility n Hidden
1096 addIBC (IBCAccess n Hidden))]
1097 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
1098 return [PDirective (do setAccessibility n Frozen
1099 addIBC (IBCAccess n Frozen))]
1100 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1101 return [PDirective (do i <- get
1102 put(i { default_access = acc }))]
1103 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1104 i <- get
1105 put (i { default_total = tot } )
1106 return [PDirective (do i <- get
1107 put(i { default_total = tot }))]
1108 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
1109 return [PDirective (setLogLevel (fromInteger i))]
1110 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
1111 return [PDirective (do added <- addDyLib libs
1112 case added of
1113 Left lib -> addIBC (IBCDyLib (lib_name lib))
1114 Right msg ->
1115 fail $ msg)]
1116 <|> do try (lchar '%' *> reserved "name")
1117 ty <- fnName
1118 ns <- sepBy1 name (lchar ',')
1119 return [PDirective (do ty' <- disambiguate ty
1120 mapM_ (addNameHint ty') ns
1121 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1122 <|> do try (lchar '%' *> reserved "error_handlers")
1123 fn <- fnName
1124 arg <- fnName
1125 ns <- sepBy1 name (lchar ',')
1126 return [PDirective (do fn' <- disambiguate fn
1127 ns' <- mapM disambiguate ns
1128 addFunctionErrorHandlers fn' arg ns'
1129 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]
1130 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1131 return [PDirective (addLangExt ext)]
1132 <|> do fc <- getFC
1133 try (lchar '%' *> reserved "used")
1134 fn <- fnName
1135 arg <- iName []
1136 return [PDirective (addUsedName fc fn arg)]
1138 <?> "directive"
1139 where disambiguate :: Name -> Idris Name
1140 disambiguate n = do i <- getIState
1141 case lookupCtxtName n (idris_implicits i) of
1142 [(n', _)] -> return n'
1143 [] -> throwError (NoSuchVariable n)
1144 more -> throwError (CantResolveAlts (map fst more))
1146pLangExt :: IdrisParser LanguageExt
1147pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1148 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1150{- | Parses a totality
1153Totality ::= 'partial' | 'total'
1157totality :: IdrisParser Bool
1158totality
1159 = do reserved "total"; return True
1160 <|> do reserved "partial"; return False
1162{- | Parses a type provider
1165Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1166ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1168 -}
1169provider :: SyntaxInfo -> IdrisParser [PDecl]
1170provider syn = do doc <- try (do (doc, _) <- docstring syn
1171 lchar '%'
1172 reserved "provide"
1173 return doc)
1174 provideTerm doc <|> providePostulate doc
1175 <?> "type provider"
1176 where provideTerm doc =
1177 do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1178 fc <- getFC
1179 reserved "with"
1180 e <- expr syn <?> "provider expression"
1181 return [PProvider doc syn fc (ProvTerm t e) n]
1182 providePostulate doc =
1183 do reserved "postulate"
1184 n <- fnName
1185 fc <- getFC
1186 reserved "with"
1187 e <- expr syn <?> "provider expression"
1188 return [PProvider doc syn fc (ProvPostulate e) n]
1190{- | Parses a transform
1193Transform ::= '%' 'transform' Expr '==>' Expr
1196transform :: SyntaxInfo -> IdrisParser [PDecl]
1197transform syn = do try (lchar '%' *> reserved "transform")
1198 -- leave it unchecked, until we work out what this should
1199 -- actually mean...
1200-- safety <- option True (do reserved "unsafe"
1201-- return False)
1202 l <- expr syn
1203 fc <- getFC
1204 symbol "==>"
1205 r <- expr syn
1206 return [PTransform fc False l r]
1207 <?> "transform"
1210{- * Loading and parsing -}
1211{- | Parses an expression from input -}
1212parseExpr :: IState -> String -> Result PTerm
1213parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1215{- | Parses a constant form input -}
1216parseConst :: IState -> String -> Result Const
1217parseConst st = runparser constant st "(input)"
1219{- | Parses a tactic from input -}
1220parseTactic :: IState -> String -> Result PTactic
1221parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1223-- | Parse module header and imports
1224parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta)
1225parseImports fname input
1226 = do i <- getIState
1227 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1228 Failure err -> fail (show err)
1229 Success (x, i) -> do putIState i
1230 return x
1231 where imports :: IdrisParser ((Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta), IState)
1232 imports = do whiteSpace
1233 (mdoc, mname) <- moduleHeader
1234 ps <- many import_
1235 mrk <- mark
1236 isEof <- lookAheadMatches eof
1237 let mrk' = if isEof
1238 then Nothing
1239 else Just mrk
1240 i <- get
1241 return ((mdoc, mname, ps, mrk'), i)
1243-- | There should be a better way of doing this...
1244findFC :: Doc -> (FC, String)
1245findFC x = let s = show (plain x) in
1246 case span (/= ':') s of
1247 (failname, ':':rest) -> case span isDigit rest of
1248 (line, ':':rest') -> case span isDigit rest' of
1249 (col, ':':msg) -> let pos = (read line, read col) in
1250 (FC failname pos pos, msg)
1252-- | Check if the coloring matches the options and corrects if necessary
1253fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1254fixColour False doc = ANSI.plain doc
1255fixColour True doc = doc
1257-- | A program is a list of declarations, possibly with associated
1258-- documentation strings.
1259parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1260 Idris [PDecl]
1261parseProg syn fname input mrk
1262 = do i <- getIState
1263 case runparser mainProg i fname input of
1264 Failure doc -> do -- FIXME: Get error location from trifecta
1265 -- this can't be the solution!
1266 -- Issue #1575 on the issue tracker.
1267 -- https://github.com/idris-lang/Idris-dev/issues/1575
1268 let (fc, msg) = findFC doc
1269 i <- getIState
1270 case idris_outputmode i of
1271 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1272 IdeMode n h -> iWarn fc (P.text msg)
1273 putIState (i { errSpan = Just fc })
1274 return []
1275 Success (x, i) -> do putIState i
1276 reportParserWarnings
1277 return $ collect x
1278 where mainProg :: IdrisParser ([PDecl], IState)
1279 mainProg = case mrk of
1280 Nothing -> do i <- get; return ([], i)
1281 Just mrk -> do
1282 release mrk
1283 ds <- prog syn
1284 i' <- get
1285 return (ds, i')
1287{- | Load idris module and show error if something wrong happens -}
1288loadModule :: FilePath -> Idris (Maybe String)
1289loadModule f
1290 = idrisCatch (loadModule' f)
1291 (\e -> do setErrSpan (getErrSpan e)
1292 ist <- getIState
1293 iWarn (getErrSpan e) $ pprintErr ist e
1294 return Nothing)
1296{- | Load idris module -}
1297loadModule' :: FilePath -> Idris (Maybe String)
1298loadModule' f
1299 = do i <- getIState
1300 let file = takeWhile (/= ' ') f
1301 ibcsd <- valIBCSubDir i
1302 ids <- allImportDirs
1303 fp <- findImport ids ibcsd file
1304 if file `elem` imported i
1305 then do iLOG $ "Already read " ++ file
1306 return Nothing
1307 else do putIState (i { imported = file : imported i })
1308 case fp of
1309 IDR fn -> loadSource False fn Nothing
1310 LIDR fn -> loadSource True fn Nothing
1311 IBC fn src ->
1312 idrisCatch (loadIBC True fn)
1313 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1314 case src of
1315 IDR sfn -> loadSource False sfn Nothing
1316 LIDR sfn -> loadSource True sfn Nothing)
1317 return $ Just file
1319{- | Load idris code from file -}
1320loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()
1321loadFromIFile reexp i@(IBC fn src) maxline
1322 = do iLOG $ "Skipping " ++ getSrcFile i
1323 idrisCatch (loadIBC reexp fn)
1324 (\err -> ierror $ LoadingFailed fn err)
1325 where
1326 getSrcFile (IDR fn) = fn
1327 getSrcFile (LIDR fn) = fn
1328 getSrcFile (IBC f src) = getSrcFile src
1330loadFromIFile _ (IDR fn) maxline = loadSource' False fn maxline
1331loadFromIFile _ (LIDR fn) maxline = loadSource' True fn maxline
1333{-| Load idris source code and show error if something wrong happens -}
1334loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1335loadSource' lidr r maxline
1336 = idrisCatch (loadSource lidr r maxline)
1337 (\e -> do setErrSpan (getErrSpan e)
1338 ist <- getIState
1339 case e of
1340 At f e' -> iWarn f (pprintErr ist e')
1341 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1343{- | Load Idris source code-}
1344loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1345loadSource lidr f toline
1346 = do iLOG ("Reading " ++ f)
1347 i <- getIState
1348 let def_total = default_total i
1349 file_in <- runIO $ readSource f
1350 file <- if lidr then tclift $ unlit f file_in else return file_in
1351 (mdocs, mname, imports_in, pos) <- parseImports f file
1352 ai <- getAutoImports
1353 let imports = map (\n -> (True, n, Just n, emptyFC)) ai ++ imports_in
1354 ids <- allImportDirs
1355 ibcsd <- valIBCSubDir i
1356 mapM_ (\(re, f) ->
1357 do fp <- findImport ids ibcsd f
1358 case fp of
1359 LIDR fn -> ifail $ "No ibc for " ++ f
1360 IDR fn -> ifail $ "No ibc for " ++ f
1361 IBC fn src -> loadIBC True fn)
1362 [(re, fn) | (re, fn, _, _) <- imports]
1363 reportParserWarnings
1365 -- process and check module aliases
1366 let modAliases = M.fromList
1367 [(prep alias, prep realName) | (reexport, realName, Just alias, fc) <- imports]
1368 prep = map T.pack . reverse . Spl.splitOn "/"
1369 aliasNames = [(alias, fc) | (_, _, Just alias, fc) <- imports]
1370 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1371 case map head . filter ((/= 1) . length) $ histogram of
1372 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1373 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1375 i <- getIState
1376 putIState (i { default_access = Hidden, module_aliases = modAliases })
1377 clearIBC -- start a new .ibc file
1378 -- record package info in .ibc
1379 imps <- allImportDirs
1380 mapM_ addIBC (map IBCImportDir imps)
1381 mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports]
1382 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1383 maxline = toline }
1384 ist <- getIState
1385 -- Save the span from parsing the module header, because
1386 -- an empty program parse might obliterate it.
1387 let oldSpan = idris_parsedSpan ist
1388 ds' <- parseProg syntax f file pos
1390 case (ds', oldSpan) of
1391 ([], Just fc) ->
1392 -- If no program elements were parsed, we dind't
1393 -- get a loaded region in the IBC file. That
1394 -- means we need to add it back.
1395 do ist <- getIState
1396 putIState ist { idris_parsedSpan = oldSpan
1397 , ibc_write = IBCParsedRegion fc :
1398 ibc_write ist
1400 _ -> return ()
1402 -- Parsing done, now process declarations
1404 let ds = namespaces mname ds'
1405 logLvl 3 (show $ showDecls verbosePPOption ds)
1406 i <- getIState
1407 logLvl 10 (show (toAlist (idris_implicits i)))
1408 logLvl 3 (show (idris_infixes i))
1409 -- Now add all the declarations to the context
1410 v <- verbose
1411 when v $ iputStrLn $ "Type checking " ++ f
1412 -- we totality check after every Mutual block, so if
1413 -- anything is a single definition, wrap it in a
1414 -- mutual block on its own
1415 elabDecls toplevel (map toMutual ds)
1416 i <- getIState
1417 -- simplify every definition do give the totality checker
1418 -- a better chance
1419 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1420 updateContext (simplifyCasedef n $ getErasureInfo i))
1421 (map snd (idris_totcheck i))
1422 -- build size change graph from simplified definitions
1423 iLOG "Totality checking"
1424 i <- getIState
1425 mapM_ buildSCG (idris_totcheck i)
1426 mapM_ checkDeclTotality (idris_totcheck i)
1428 -- Redo totality check for deferred names
1429 let deftots = idris_defertotcheck i
1430 iLOG $ "Totality checking " ++ show deftots
1431 mapM_ (\x -> do tot <- getTotality x
1432 case tot of
1433 Total _ -> setTotality x Unchecked
1434 _ -> return ()) (map snd deftots)
1435 mapM_ buildSCG deftots
1436 mapM_ checkDeclTotality deftots
1438 iLOG ("Finished " ++ f)
1439 ibcsd <- valIBCSubDir i
1440 iLOG "Universe checking"
1441 iucheck
1442 let ibc = ibcPathNoFallback ibcsd f
1443 i <- getIState
1444 addHides (hide_list i)
1446 -- Save module documentation if applicable
1447 i <- getIState
1448 case mdocs of
1449 Nothing -> return ()
1450 Just docs -> addModDoc syntax mname docs
1453 -- Finally, write an ibc if checking was successful
1454 ok <- noErrors
1455 when ok $
1456 idrisCatch (do writeIBC f ibc; clearIBC)
1457 (\c -> return ()) -- failure is harmless
1458 i <- getIState
1459 putIState (i { default_total = def_total,
1460 hide_list = [] })
1461 return ()
1462 where
1463 namespaces :: [String] -> [PDecl] -> [PDecl]
1464 namespaces [] ds = ds
1465 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1467 toMutual :: PDecl -> PDecl
1468 toMutual m@(PMutual _ d) = m
1469 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1470 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1471 case x of
1472 PClauses{} -> r
1473 PClass{} -> r
1474 PInstance{} -> r
1475 _ -> x
1477 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1478 addModDoc syn mname docs =
1479 do ist <- getIState
1480 docs' <- elabDocTerms recinfo (parsedDocs ist)
1481 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1482 putIState ist { idris_moduledocs = modDocs' }
1483 addIBC (IBCModDocs docName)
1484 where
1485 docName = NS modDocName (map T.pack (reverse mname))
1486 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1488{- | Adds names to hide list -}
1489addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1490addHides xs = do i <- getIState
1491 let defh = default_access i
1492 let (hs, as) = partition isNothing xs
1493 unless (null as) $
1494 mapM_ doHide
1495 (map (\ (n, _) -> (n, defh)) hs ++
1496 map (\ (n, Just a) -> (n, a)) as)
1497 where isNothing (_, Nothing) = True
1498 isNothing _ = False
1500 doHide (n, a) = do setAccessibility n a
1501 addIBC (IBCAccess n a)