git.iko.soy/Idris-dev
on 8a3d348 help sign in
Idris-dev/src/Idris/Parser.hs
1500 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 try (lchar '%' *> reserved "hint");
483 fnOpts (AutoHint : opts)
484 <|> do lchar '%'; reserved "specialise";
485 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
486 fnOpts (Specialise ns : opts)
487 <|> do reserved "implicit"; fnOpts (Implicit : opts)
488 <|> return opts
489 <?> "function modifier"
490 where nameTimes :: IdrisParser (Name, Maybe Int)
491 nameTimes = do n <- fnName
492 t <- option Nothing (do reds <- natural
493 return (Just (fromInteger reds)))
494 return (n, t)
496{- | Parses a postulate
499Postulate ::=
500 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
501 ;
503-}
504postulate :: SyntaxInfo -> IdrisParser PDecl
505postulate syn = do (doc, ext)
506 <- try $ do (doc, _) <- docstring syn
507 pushIndent
508 ext <- ppostDecl
509 return (doc, ext)
510 ist <- get
511 let initOpts = if default_total ist
512 then [TotalFn]
513 else []
514 opts <- fnOpts initOpts
515 acc <- optional accessibility
516 opts' <- fnOpts opts
517 n_in <- fnName
518 let n = expandNS syn n_in
519 lchar ':'
520 ty <- typeExpr (allowImp syn)
521 fc <- getFC
522 terminator
523 addAcc n acc
524 return (PPostulate ext doc syn fc opts' n ty)
525 <?> "postulate"
526 where ppostDecl = do reserved "postulate"; return False
527 <|> do lchar '%'; reserved "extern"; return True
528{- | Parses a using declaration
531Using ::=
532 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
533 ;
535 -}
536using_ :: SyntaxInfo -> IdrisParser [PDecl]
537using_ syn =
538 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
539 openBlock
540 let uvars = using syn
541 ds <- many (decl (syn { using = uvars ++ ns }))
542 closeBlock
543 return (concat ds)
544 <?> "using declaration"
546{- | Parses a parameters declaration
549Params ::=
550 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
551 ;
553 -}
554params :: SyntaxInfo -> IdrisParser [PDecl]
555params syn =
556 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
557 openBlock
558 let pvars = syn_params syn
559 ds <- many (decl syn { syn_params = pvars ++ ns })
560 closeBlock
561 fc <- getFC
562 return [PParams fc ns (concat ds)]
563 <?> "parameters declaration"
565{- | Parses a mutual declaration (for mutually recursive functions)
568Mutual ::=
569 'mutual' OpenBlock Decl* CloseBlock
570 ;
572-}
573mutual :: SyntaxInfo -> IdrisParser [PDecl]
574mutual syn =
575 do reserved "mutual"
576 openBlock
577 let pvars = syn_params syn
578 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
579 closeBlock
580 fc <- getFC
581 return [PMutual fc (concat ds)]
582 <?> "mutual block"
584{-| Parses a namespace declaration
587Namespace ::=
588 'namespace' identifier OpenBlock Decl+ CloseBlock
589 ;
591-}
592namespace :: SyntaxInfo -> IdrisParser [PDecl]
593namespace syn =
594 do reserved "namespace"; n <- identifier;
595 openBlock
596 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
597 closeBlock
598 return [PNamespace n (concat ds)]
599 <?> "namespace declaration"
601{- | Parses a methods block (for instances)
604 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
606-}
607instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
608instanceBlock syn = do reserved "where"
609 openBlock
610 ds <- many (fnDecl syn)
611 closeBlock
612 return (concat ds)
613 <?> "instance block"
615{- | Parses a methods and instances block (for type classes)
618MethodOrInstance ::=
619 FnDecl
620 | Instance
621 ;
625ClassBlock ::=
626 'where' OpenBlock MethodOrInstance* CloseBlock
627 ;
629-}
630classBlock :: SyntaxInfo -> IdrisParser [PDecl]
631classBlock syn = do reserved "where"
632 openBlock
633 ds <- many (notEndBlock >> instance_ syn <|> fnDecl syn)
634 closeBlock
635 return (concat ds)
636 <?> "class block"
638{-| Parses a type class declaration
641ClassArgument ::=
642 Name
643 | '(' Name ':' Expr ')'
644 ;
648Class ::=
649 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
650 ;
652-}
653class_ :: SyntaxInfo -> IdrisParser [PDecl]
654class_ syn = do (doc, argDocs, acc)
655 <- try (do (doc, argDocs) <- docstring syn
656 acc <- optional accessibility
657 reserved "class"
658 return (doc, argDocs, acc))
659 fc <- getFC
660 cons <- constraintList syn
661 n_in <- fnName
662 let n = expandNS syn n_in
663 cs <- many carg
664 fds <- option (map fst cs) fundeps
665 ds <- option [] (classBlock syn)
666 accData acc n (concatMap declared ds)
667 return [PClass doc syn fc cons n cs argDocs fds ds]
668 <?> "type-class declaration"
669 where
670 fundeps :: IdrisParser [Name]
671 fundeps = do lchar '|'; sepBy name (lchar ',')
673 carg :: IdrisParser (Name, PTerm)
674 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
675 return (i, ty)
676 <|> do i <- name;
677 return (i, PType)
679{- | Parses a type class instance declaration
682 Instance ::=
683 DocComment_t? 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
684 ;
688InstanceName ::= '[' Name ']';
690-}
691instance_ :: SyntaxInfo -> IdrisParser [PDecl]
692instance_ syn = do (doc, argDocs)
693 <- try (docstring syn <* reserved "instance")
694 fc <- getFC
695 en <- optional instanceName
696 cs <- constraintList syn
697 cn <- fnName
698 args <- many (simpleExpr syn)
699 let sc = PApp fc (PRef fc cn) (map pexp args)
700 let t = bindList (PPi constraint) cs sc
701 ds <- option [] (instanceBlock syn)
702 return [PInstance doc argDocs syn fc cs cn args t en ds]
703 <?> "instance declaration"
704 where instanceName :: IdrisParser Name
705 instanceName = do lchar '['; n_in <- fnName; lchar ']'
706 let n = expandNS syn n_in
707 return n
708 <?> "instance name"
711-- | Parse a docstring
712docstring :: SyntaxInfo
713 -> IdrisParser (Docstring (Either Err PTerm),
714 [(Name,Docstring (Either Err PTerm))])
715docstring syn = do (doc, argDocs) <- option noDocs docComment
716 ist <- get
717 let doc' = annotCode (tryFullExpr syn ist) doc
718 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
719 | (n, d) <- argDocs ]
720 return (doc', argDocs')
723{- | Parses a using declaration list
726UsingDeclList ::=
727 UsingDeclList'
728 | NameList TypeSig
729 ;
733UsingDeclList' ::=
734 UsingDecl
735 | UsingDecl ',' UsingDeclList'
736 ;
740NameList ::=
741 Name
742 | Name ',' NameList
743 ;
745-}
746usingDeclList :: SyntaxInfo -> IdrisParser [Using]
747usingDeclList syn
748 = try (sepBy1 (usingDecl syn) (lchar ','))
749 <|> do ns <- sepBy1 name (lchar ',')
750 lchar ':'
751 t <- typeExpr (disallowImp syn)
752 return (map (\x -> UImplicit x t) ns)
753 <?> "using declaration list"
755{- |Parses a using declaration
758UsingDecl ::=
759 FnName TypeSig
760 | FnName FnName+
761 ;
763-}
764usingDecl :: SyntaxInfo -> IdrisParser Using
765usingDecl syn = try (do x <- fnName
766 lchar ':'
767 t <- typeExpr (disallowImp syn)
768 return (UImplicit x t))
769 <|> do c <- fnName
770 xs <- some fnName
771 return (UConstraint c xs)
772 <?> "using declaration"
774{- | Parse a clause with patterns
777Pattern ::= Clause;
779-}
780pattern :: SyntaxInfo -> IdrisParser PDecl
781pattern syn = do fc <- getFC
782 clause <- clause syn
783 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
784 <?> "pattern"
786{- | Parse a constant applicative form declaration
789CAF ::= 'let' FnName '=' Expr Terminator;
791-}
792caf :: SyntaxInfo -> IdrisParser PDecl
793caf syn = do reserved "let"
794 n_in <- fnName; let n = expandNS syn n_in
795 lchar '='
796 t <- expr syn
797 terminator
798 fc <- getFC
799 return (PCAF fc n t)
800 <?> "constant applicative form declaration"
802{- | Parse an argument expression
805ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
807-}
808argExpr :: SyntaxInfo -> IdrisParser PTerm
809argExpr syn = let syn' = syn { inPattern = True } in
810 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
811 <?> "argument expression"
813{- | Parse a right hand side of a function
816RHS ::= '=' Expr
817 | '?=' RHSName? Expr
818 | Impossible
819 ;
823RHSName ::= '{' FnName '}';
825-}
826rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
827rhs syn n = do lchar '='; expr syn
828 <|> do symbol "?=";
829 fc <- getFC
830 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
831 return n)
832 r <- expr syn
833 return (addLet fc name r)
834 <|> impossible
835 <?> "function right hand side"
836 where mkN :: Name -> Name
837 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
838 then sUN "infix_op_lemma_1"
839 else sUN (str x++"_lemma_1")
840 mkN (NS x n) = NS (mkN x) n
841 n' :: Name
842 n' = mkN n
843 addLet :: FC -> Name -> PTerm -> PTerm
844 addLet fc nm (PLet fc' n ty val r) = PLet fc' n ty val (addLet fc nm r)
845 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
846 where addLetC (l, r) = (l, addLet fc nm r)
847 addLet fc nm r = (PLet fc (sUN "value") Placeholder r (PMetavar nm))
849{- |Parses a function clause
852RHSOrWithBlock ::= RHS WhereOrTerminator
853 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
854 ;
858Clause ::= WExpr+ RHSOrWithBlock
859 | SimpleExpr '<==' FnName RHS WhereOrTerminator
860 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
861 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
862 ;
866ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
870WhereOrTerminator ::= WhereBlock | Terminator;
872-}
873clause :: SyntaxInfo -> IdrisParser PClause
874clause syn
875 = do wargs <- try (do pushIndent; some (wExpr syn))
876 fc <- getFC
877 ist <- get
878 n <- case lastParse ist of
879 Just t -> return t
880 Nothing -> fail "Invalid clause"
881 (do r <- rhs syn n
882 let ctxt = tt_ctxt ist
883 let wsyn = syn { syn_namespace = [] }
884 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
885 popIndent
886 return x,
887 do terminator
888 return ([], [])]
889 return $ PClauseR fc wargs r wheres) <|> (do
890 popIndent
891 reserved "with"
892 wval <- simpleExpr syn
893 pn <- optProof
894 openBlock
895 ds <- some $ fnDecl syn
896 let withs = concat ds
897 closeBlock
898 return $ PWithR fc wargs wval pn withs)
899 <|> do ty <- try (do pushIndent
900 ty <- simpleExpr syn
901 symbol "<=="
902 return ty)
903 fc <- getFC
904 n_in <- fnName; let n = expandNS syn n_in
905 r <- rhs syn n
906 ist <- get
907 let ctxt = tt_ctxt ist
908 let wsyn = syn { syn_namespace = [] }
909 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
910 popIndent
911 return x,
912 do terminator
913 return ([], [])]
914 let capp = PLet fc (sMN 0 "match")
915 ty
916 (PMatchApp fc n)
917 (PRef fc (sMN 0 "match"))
918 ist <- get
919 put (ist { lastParse = Just n })
920 return $ PClause fc n capp [] r wheres
921 <|> do (l, op) <- try (do
922 pushIndent
923 l <- argExpr syn
924 op <- operator
925 when (op == "=" || op == "?=" ) $
926 fail "infix clause definition with \"=\" and \"?=\" not supported "
927 return (l, op))
928 let n = expandNS syn (sUN op)
929 r <- argExpr syn
930 fc <- getFC
931 wargs <- many (wExpr syn)
932 (do rs <- rhs syn n
933 let wsyn = syn { syn_namespace = [] }
934 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
935 popIndent
936 return x,
937 do terminator
938 return ([], [])]
939 ist <- get
940 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
941 put (ist { lastParse = Just n })
942 return $ PClause fc n capp wargs rs wheres) <|> (do
943 popIndent
944 reserved "with"
945 wval <- bracketed syn
946 pn <- optProof
947 openBlock
948 ds <- some $ fnDecl syn
949 closeBlock
950 ist <- get
951 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
952 let withs = map (fillLHSD n capp wargs) $ concat ds
953 put (ist { lastParse = Just n })
954 return $ PWith fc n capp wargs wval pn withs)
955 <|> do pushIndent
956 n_in <- fnName; let n = expandNS syn n_in
957 cargs <- many (constraintArg syn)
958 fc <- getFC
959 args <- many (try (implicitArg (syn { inPattern = True } ))
960 <|> (fmap pexp (argExpr syn)))
961 wargs <- many (wExpr syn)
962 let capp = PApp fc (PRef fc n)
963 (cargs ++ args)
964 (do r <- rhs syn n
965 ist <- get
966 let ctxt = tt_ctxt ist
967 let wsyn = syn { syn_namespace = [] }
968 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
969 popIndent
970 return x,
971 do terminator
972 return ([], [])]
973 ist <- get
974 put (ist { lastParse = Just n })
975 return $ PClause fc n capp wargs r wheres) <|> (do
976 reserved "with"
977 ist <- get
978 put (ist { lastParse = Just n })
979 wval <- bracketed syn
980 pn <- optProof
981 openBlock
982 ds <- some $ fnDecl syn
983 let withs = map (fillLHSD n capp wargs) $ concat ds
984 closeBlock
985 popIndent
986 return $ PWith fc n capp wargs wval pn withs)
987 <?> "function clause"
988 where
989 optProof = option Nothing (do reserved "proof"
990 n <- fnName
991 return (Just n))
993 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
994 fillLHS n capp owargs (PClauseR fc wargs v ws)
995 = PClause fc n capp (owargs ++ wargs) v ws
996 fillLHS n capp owargs (PWithR fc wargs v pn ws)
997 = PWith fc n capp (owargs ++ wargs) v pn
998 (map (fillLHSD n capp (owargs ++ wargs)) ws)
999 fillLHS _ _ _ c = c
1001 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
1002 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1003 fillLHSD n c a x = x
1005{-| Parses with pattern
1008WExpr ::= '|' Expr';
1011wExpr :: SyntaxInfo -> IdrisParser PTerm
1012wExpr syn = do lchar '|'
1013 expr' (syn { inPattern = True })
1014 <?> "with pattern"
1016{- | Parses a where block
1019WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
1022whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
1023whereBlock n syn
1024 = do reserved "where"
1025 ds <- indentedBlock1 (decl syn)
1026 let dns = concatMap (concatMap declared) ds
1027 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1028 <?> "where block"
1030{- |Parses a code generation target language name
1033Codegen ::= 'C'
1034 | 'Java'
1035 | 'JavaScript'
1036 | 'Node'
1037 | 'LLVM'
1038 | 'Bytecode'
1042codegen_ :: IdrisParser Codegen
1043codegen_ = do n <- identifier; return (Via (map toLower n))
1044 <|> do reserved "Bytecode"; return Bytecode
1045 <?> "code generation language"
1047{- |Parses a compiler directive
1049StringList ::=
1050 String
1051 | String ',' StringList
1056Directive ::= '%' Directive';
1060Directive' ::= 'lib' CodeGen String_t
1061 | 'link' CodeGen String_t
1062 | 'flag' CodeGen String_t
1063 | 'include' CodeGen String_t
1064 | 'hide' Name
1065 | 'freeze' Name
1066 | 'access' Accessibility
1067 | 'default' Totality
1068 | 'logging' Natural
1069 | 'dynamic' StringList
1070 | 'name' Name NameList
1071 | 'error_handlers' Name NameList
1072 | 'language' 'TypeProviders'
1073 | 'language' 'ErrorReflection'
1077directive :: SyntaxInfo -> IdrisParser [PDecl]
1078directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
1079 return [PDirective (do addLib cgn lib
1080 addIBC (IBCLib cgn lib))]
1081 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
1082 return [PDirective (do dirs <- allImportDirs
1083 o <- liftIO $ findInPath dirs obj
1084 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
1085 addObjectFile cgn o)]
1086 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
1087 flag <- stringLiteral
1088 return [PDirective (do addIBC (IBCCGFlag cgn flag)
1089 addFlag cgn flag)]
1090 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
1091 return [PDirective (do addHdr cgn hdr
1092 addIBC (IBCHeader cgn hdr))]
1093 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
1094 return [PDirective (do setAccessibility n Hidden
1095 addIBC (IBCAccess n Hidden))]
1096 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
1097 return [PDirective (do setAccessibility n Frozen
1098 addIBC (IBCAccess n Frozen))]
1099 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1100 return [PDirective (do i <- get
1101 put(i { default_access = acc }))]
1102 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1103 i <- get
1104 put (i { default_total = tot } )
1105 return [PDirective (do i <- get
1106 put(i { default_total = tot }))]
1107 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
1108 return [PDirective (setLogLevel (fromInteger i))]
1109 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
1110 return [PDirective (do added <- addDyLib libs
1111 case added of
1112 Left lib -> addIBC (IBCDyLib (lib_name lib))
1113 Right msg ->
1114 fail $ msg)]
1115 <|> do try (lchar '%' *> reserved "name")
1116 ty <- fnName
1117 ns <- sepBy1 name (lchar ',')
1118 return [PDirective (do ty' <- disambiguate ty
1119 mapM_ (addNameHint ty') ns
1120 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1121 <|> do try (lchar '%' *> reserved "error_handlers")
1122 fn <- fnName
1123 arg <- fnName
1124 ns <- sepBy1 name (lchar ',')
1125 return [PDirective (do fn' <- disambiguate fn
1126 ns' <- mapM disambiguate ns
1127 addFunctionErrorHandlers fn' arg ns'
1128 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]
1129 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1130 return [PDirective (addLangExt ext)]
1131 <|> do fc <- getFC
1132 try (lchar '%' *> reserved "used")
1133 fn <- fnName
1134 arg <- iName []
1135 return [PDirective (addUsedName fc fn arg)]
1137 <?> "directive"
1138 where disambiguate :: Name -> Idris Name
1139 disambiguate n = do i <- getIState
1140 case lookupCtxtName n (idris_implicits i) of
1141 [(n', _)] -> return n'
1142 [] -> throwError (NoSuchVariable n)
1143 more -> throwError (CantResolveAlts (map fst more))
1145pLangExt :: IdrisParser LanguageExt
1146pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1147 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1149{- | Parses a totality
1152Totality ::= 'partial' | 'total'
1156totality :: IdrisParser Bool
1157totality
1158 = do reserved "total"; return True
1159 <|> do reserved "partial"; return False
1161{- | Parses a type provider
1164Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1165ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1167 -}
1168provider :: SyntaxInfo -> IdrisParser [PDecl]
1169provider syn = do doc <- try (do (doc, _) <- docstring syn
1170 lchar '%'
1171 reserved "provide"
1172 return doc)
1173 provideTerm doc <|> providePostulate doc
1174 <?> "type provider"
1175 where provideTerm doc =
1176 do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1177 fc <- getFC
1178 reserved "with"
1179 e <- expr syn <?> "provider expression"
1180 return [PProvider doc syn fc (ProvTerm t e) n]
1181 providePostulate doc =
1182 do reserved "postulate"
1183 n <- fnName
1184 fc <- getFC
1185 reserved "with"
1186 e <- expr syn <?> "provider expression"
1187 return [PProvider doc syn fc (ProvPostulate e) n]
1189{- | Parses a transform
1192Transform ::= '%' 'transform' Expr '==>' Expr
1195transform :: SyntaxInfo -> IdrisParser [PDecl]
1196transform syn = do try (lchar '%' *> reserved "transform")
1197 -- leave it unchecked, until we work out what this should
1198 -- actually mean...
1199-- safety <- option True (do reserved "unsafe"
1200-- return False)
1201 l <- expr syn
1202 fc <- getFC
1203 symbol "==>"
1204 r <- expr syn
1205 return [PTransform fc False l r]
1206 <?> "transform"
1209{- * Loading and parsing -}
1210{- | Parses an expression from input -}
1211parseExpr :: IState -> String -> Result PTerm
1212parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1214{- | Parses a constant form input -}
1215parseConst :: IState -> String -> Result Const
1216parseConst st = runparser constant st "(input)"
1218{- | Parses a tactic from input -}
1219parseTactic :: IState -> String -> Result PTactic
1220parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1222-- | Parse module header and imports
1223parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta)
1224parseImports fname input
1225 = do i <- getIState
1226 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1227 Failure err -> fail (show err)
1228 Success (x, i) -> do putIState i
1229 return x
1230 where imports :: IdrisParser ((Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta), IState)
1231 imports = do whiteSpace
1232 (mdoc, mname) <- moduleHeader
1233 ps <- many import_
1234 mrk <- mark
1235 isEof <- lookAheadMatches eof
1236 let mrk' = if isEof
1237 then Nothing
1238 else Just mrk
1239 i <- get
1240 return ((mdoc, mname, ps, mrk'), i)
1242-- | There should be a better way of doing this...
1243findFC :: Doc -> (FC, String)
1244findFC x = let s = show (plain x) in
1245 case span (/= ':') s of
1246 (failname, ':':rest) -> case span isDigit rest of
1247 (line, ':':rest') -> case span isDigit rest' of
1248 (col, ':':msg) -> let pos = (read line, read col) in
1249 (FC failname pos pos, msg)
1251-- | Check if the coloring matches the options and corrects if necessary
1252fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1253fixColour False doc = ANSI.plain doc
1254fixColour True doc = doc
1256-- | A program is a list of declarations, possibly with associated
1257-- documentation strings.
1258parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1259 Idris [PDecl]
1260parseProg syn fname input mrk
1261 = do i <- getIState
1262 case runparser mainProg i fname input of
1263 Failure doc -> do -- FIXME: Get error location from trifecta
1264 -- this can't be the solution!
1265 -- Issue #1575 on the issue tracker.
1266 -- https://github.com/idris-lang/Idris-dev/issues/1575
1267 let (fc, msg) = findFC doc
1268 i <- getIState
1269 case idris_outputmode i of
1270 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1271 IdeMode n h -> iWarn fc (P.text msg)
1272 putIState (i { errSpan = Just fc })
1273 return []
1274 Success (x, i) -> do putIState i
1275 reportParserWarnings
1276 return $ collect x
1277 where mainProg :: IdrisParser ([PDecl], IState)
1278 mainProg = case mrk of
1279 Nothing -> do i <- get; return ([], i)
1280 Just mrk -> do
1281 release mrk
1282 ds <- prog syn
1283 i' <- get
1284 return (ds, i')
1286{- | Load idris module and show error if something wrong happens -}
1287loadModule :: FilePath -> Idris (Maybe String)
1288loadModule f
1289 = idrisCatch (loadModule' f)
1290 (\e -> do setErrSpan (getErrSpan e)
1291 ist <- getIState
1292 iWarn (getErrSpan e) $ pprintErr ist e
1293 return Nothing)
1295{- | Load idris module -}
1296loadModule' :: FilePath -> Idris (Maybe String)
1297loadModule' f
1298 = do i <- getIState
1299 let file = takeWhile (/= ' ') f
1300 ibcsd <- valIBCSubDir i
1301 ids <- allImportDirs
1302 fp <- findImport ids ibcsd file
1303 if file `elem` imported i
1304 then do iLOG $ "Already read " ++ file
1305 return Nothing
1306 else do putIState (i { imported = file : imported i })
1307 case fp of
1308 IDR fn -> loadSource False fn Nothing
1309 LIDR fn -> loadSource True fn Nothing
1310 IBC fn src ->
1311 idrisCatch (loadIBC True fn)
1312 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1313 case src of
1314 IDR sfn -> loadSource False sfn Nothing
1315 LIDR sfn -> loadSource True sfn Nothing)
1316 return $ Just file
1318{- | Load idris code from file -}
1319loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()
1320loadFromIFile reexp i@(IBC fn src) maxline
1321 = do iLOG $ "Skipping " ++ getSrcFile i
1322 idrisCatch (loadIBC reexp fn)
1323 (\err -> ierror $ LoadingFailed fn err)
1324 where
1325 getSrcFile (IDR fn) = fn
1326 getSrcFile (LIDR fn) = fn
1327 getSrcFile (IBC f src) = getSrcFile src
1329loadFromIFile _ (IDR fn) maxline = loadSource' False fn maxline
1330loadFromIFile _ (LIDR fn) maxline = loadSource' True fn maxline
1332{-| Load idris source code and show error if something wrong happens -}
1333loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1334loadSource' lidr r maxline
1335 = idrisCatch (loadSource lidr r maxline)
1336 (\e -> do setErrSpan (getErrSpan e)
1337 ist <- getIState
1338 case e of
1339 At f e' -> iWarn f (pprintErr ist e')
1340 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1342{- | Load Idris source code-}
1343loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1344loadSource lidr f toline
1345 = do iLOG ("Reading " ++ f)
1346 i <- getIState
1347 let def_total = default_total i
1348 file_in <- runIO $ readFile f
1349 file <- if lidr then tclift $ unlit f file_in else return file_in
1350 (mdocs, mname, imports_in, pos) <- parseImports f file
1351 ai <- getAutoImports
1352 let imports = map (\n -> (True, n, Just n, emptyFC)) ai ++ imports_in
1353 ids <- allImportDirs
1354 ibcsd <- valIBCSubDir i
1355 mapM_ (\(re, f) ->
1356 do fp <- findImport ids ibcsd f
1357 case fp of
1358 LIDR fn -> ifail $ "No ibc for " ++ f
1359 IDR fn -> ifail $ "No ibc for " ++ f
1360 IBC fn src -> loadIBC True fn)
1361 [(re, fn) | (re, fn, _, _) <- imports]
1362 reportParserWarnings
1364 -- process and check module aliases
1365 let modAliases = M.fromList
1366 [(prep alias, prep realName) | (reexport, realName, Just alias, fc) <- imports]
1367 prep = map T.pack . reverse . Spl.splitOn "/"
1368 aliasNames = [(alias, fc) | (_, _, Just alias, fc) <- imports]
1369 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1370 case map head . filter ((/= 1) . length) $ histogram of
1371 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1372 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1374 i <- getIState
1375 putIState (i { default_access = Hidden, module_aliases = modAliases })
1376 clearIBC -- start a new .ibc file
1377 -- record package info in .ibc
1378 imps <- allImportDirs
1379 mapM_ addIBC (map IBCImportDir imps)
1380 mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports]
1381 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1382 maxline = toline }
1383 ist <- getIState
1384 -- Save the span from parsing the module header, because
1385 -- an empty program parse might obliterate it.
1386 let oldSpan = idris_parsedSpan ist
1387 ds' <- parseProg syntax f file pos
1389 case (ds', oldSpan) of
1390 ([], Just fc) ->
1391 -- If no program elements were parsed, we dind't
1392 -- get a loaded region in the IBC file. That
1393 -- means we need to add it back.
1394 do ist <- getIState
1395 putIState ist { idris_parsedSpan = oldSpan
1396 , ibc_write = IBCParsedRegion fc :
1397 ibc_write ist
1399 _ -> return ()
1401 -- Parsing done, now process declarations
1403 let ds = namespaces mname ds'
1404 logLvl 3 (show $ showDecls verbosePPOption ds)
1405 i <- getIState
1406 logLvl 10 (show (toAlist (idris_implicits i)))
1407 logLvl 3 (show (idris_infixes i))
1408 -- Now add all the declarations to the context
1409 v <- verbose
1410 when v $ iputStrLn $ "Type checking " ++ f
1411 -- we totality check after every Mutual block, so if
1412 -- anything is a single definition, wrap it in a
1413 -- mutual block on its own
1414 elabDecls toplevel (map toMutual ds)
1415 i <- getIState
1416 -- simplify every definition do give the totality checker
1417 -- a better chance
1418 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1419 updateContext (simplifyCasedef n $ getErasureInfo i))
1420 (map snd (idris_totcheck i))
1421 -- build size change graph from simplified definitions
1422 iLOG "Totality checking"
1423 i <- getIState
1424 mapM_ buildSCG (idris_totcheck i)
1425 mapM_ checkDeclTotality (idris_totcheck i)
1427 -- Redo totality check for deferred names
1428 let deftots = idris_defertotcheck i
1429 iLOG $ "Totality checking " ++ show deftots
1430 mapM_ (\x -> do tot <- getTotality x
1431 case tot of
1432 Total _ -> setTotality x Unchecked
1433 _ -> return ()) (map snd deftots)
1434 mapM_ buildSCG deftots
1435 mapM_ checkDeclTotality deftots
1437 iLOG ("Finished " ++ f)
1438 ibcsd <- valIBCSubDir i
1439 iLOG "Universe checking"
1440 iucheck
1441 let ibc = ibcPathNoFallback ibcsd f
1442 i <- getIState
1443 addHides (hide_list i)
1445 -- Save module documentation if applicable
1446 i <- getIState
1447 case mdocs of
1448 Nothing -> return ()
1449 Just docs -> addModDoc syntax mname docs
1452 -- Finally, write an ibc if checking was successful
1453 ok <- noErrors
1454 when ok $
1455 idrisCatch (do writeIBC f ibc; clearIBC)
1456 (\c -> return ()) -- failure is harmless
1457 i <- getIState
1458 putIState (i { default_total = def_total,
1459 hide_list = [] })
1460 return ()
1461 where
1462 namespaces :: [String] -> [PDecl] -> [PDecl]
1463 namespaces [] ds = ds
1464 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1466 toMutual :: PDecl -> PDecl
1467 toMutual m@(PMutual _ d) = m
1468 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1469 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1470 case x of
1471 PClauses{} -> r
1472 PClass{} -> r
1473 PInstance{} -> r
1474 _ -> x
1476 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1477 addModDoc syn mname docs =
1478 do ist <- getIState
1479 docs' <- elabDocTerms recinfo (parsedDocs ist)
1480 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1481 putIState ist { idris_moduledocs = modDocs' }
1482 addIBC (IBCModDocs docName)
1483 where
1484 docName = NS modDocName (map T.pack (reverse mname))
1485 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1487{- | Adds names to hide list -}
1488addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1489addHides xs = do i <- getIState
1490 let defh = default_access i
1491 let (hs, as) = partition isNothing xs
1492 unless (null as) $
1493 mapM_ doHide
1494 (map (\ (n, _) -> (n, defh)) hs ++
1495 map (\ (n, Just a) -> (n, a)) as)
1496 where isNothing (_, Nothing) = True
1497 isNothing _ = False
1499 doHide (n, a) = do setAccessibility n a
1500 addIBC (IBCAccess n a)