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