git.iko.soy/Idris-dev
on 2b0224a help sign in
Idris-dev/src/Idris/Parser.hs
1553 lines 57 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 qualified System.Directory as Dir (makeAbsolute)
13import Text.Trifecta.Delta
14import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace, Err)
15import Text.Parser.LookAhead
16import Text.Parser.Expression
17import qualified Text.Parser.Token as Tok
18import qualified Text.Parser.Char as Chr
19import qualified Text.Parser.Token.Highlight as Hi
21import Text.PrettyPrint.ANSI.Leijen (Doc, plain)
22import qualified Text.PrettyPrint.ANSI.Leijen as ANSI
24import Idris.AbsSyntax hiding (namespace, params)
25import Idris.DSL
26import Idris.Imports
27import Idris.Delaborate
28import Idris.Error
29import Idris.Elab.Value
30import Idris.Elab.Term
31import Idris.ElabDecls
32import Idris.Coverage
33import Idris.IBC
34import Idris.Unlit
35import Idris.Providers
36import Idris.Output
38import Idris.ParseHelpers
39import Idris.ParseOps
40import Idris.ParseExpr
41import Idris.ParseData
43import Idris.Docstrings hiding (Unchecked)
45import Paths_idris
47import Util.DynamicLinker
48import Util.System (readSource, writeSource)
49import qualified Util.Pretty as P
51import Idris.Core.TT
52import Idris.Core.Evaluate
54import Control.Applicative hiding (Const)
55import Control.Monad
56import Control.Monad.State.Strict
58import Data.Function
59import Data.Maybe
60import qualified Data.List.Split as Spl
61import Data.List
62import Data.Monoid
63import Data.Char
64import Data.Ord
65import Data.Generics.Uniplate.Data (descendM)
66import qualified Data.Map as M
67import qualified Data.HashSet as HS
68import qualified Data.Text as T
69import qualified Data.ByteString.UTF8 as UTF8
70import qualified Data.Set as S
72import Debug.Trace
74import System.FilePath
75import System.IO
77{-
79 grammar shortcut notation:
80 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)
81 RULE? = optional rule (i.e. RULE or nothing)
82 RULE* = repeated rule (i.e. RULE zero or more times)
83 RULE+ = repeated rule with at least one match (i.e. RULE one or more times)
84 RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)
85 RULE{n} = rule repeated n times
87-}
89{- * Main grammar -}
91{- | Parses module definition
94 ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;
96-}
97moduleHeader :: IdrisParser (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
98moduleHeader = try (do docs <- optional docComment
99 noArgs docs
100 reserved "module"
101 (i, ifc) <- identifier
102 option ';' (lchar ';')
103 let modName = moduleName i
104 return (fmap fst docs,
105 modName,
106 [(ifc, AnnNamespace (map T.pack modName) Nothing)]))
107 <|> try (do lchar '%'; reserved "unqualified"
108 return (Nothing, [], []))
109 <|> return (Nothing, moduleName "Main", [])
110 where moduleName x = case span (/='.') x of
111 (x, "") -> [x]
112 (x, '.':y) -> x : moduleName y
113 noArgs (Just (_, args)) | not (null args) = fail "Modules do not take arguments"
114 noArgs _ = return ()
116data ImportInfo = ImportInfo { import_reexport :: Bool
117 , import_path :: FilePath
118 , import_rename :: Maybe (String, FC)
119 , import_namespace :: [T.Text]
120 , import_location :: FC
121 , import_modname_location :: FC
122 }
124{- | Parses an import statement
127 Import ::= 'import' Identifier_t ';'?;
129 -}
130import_ :: IdrisParser ImportInfo
131import_ = do fc <- getFC
132 reserved "import"
133 reexport <- option False (do reserved "public"; return True)
134 (id, idfc) <- identifier
135 newName <- optional (reserved "as" *> identifier)
136 option ';' (lchar ';')
137 return $ ImportInfo reexport (toPath id)
138 (fmap (\(n, fc) -> (toPath n, fc)) newName)
139 (map T.pack $ ns id) fc idfc
140 <?> "import statement"
141 where ns = Spl.splitOn "."
142 toPath = foldl1' (</>) . ns
144{- | Parses program source
147 Prog ::= Decl* EOF;
149 -}
150prog :: SyntaxInfo -> IdrisParser [PDecl]
151prog syn = do whiteSpace
152 decls <- many (decl syn)
153 let c = (concat decls)
154 case maxline syn of
155 Nothing -> do notOpenBraces; eof
156 _ -> return ()
157 ist <- get
158 fc <- getFC
159 put ist { idris_parsedSpan = Just (FC (fc_fname fc) (0,0) (fc_end fc)),
160 ibc_write = IBCParsedRegion fc : ibc_write ist }
161 return c
163{-| Parses a top-level declaration
166Decl ::=
167 Decl'
168 | Using
169 | Params
170 | Mutual
171 | Namespace
172 | Class
173 | Instance
174 | DSL
175 | Directive
176 | Provider
177 | Transform
178 | Import!
179 ;
181-}
182decl :: SyntaxInfo -> IdrisParser [PDecl]
183decl syn = do fc <- getFC
184 -- if we're after maxline, stop here
185 let continue = case maxline syn of
186 Nothing -> True
187 Just l -> if fst (fc_end fc) > l
188 then mut_nesting syn /= 0
189 else True
190 if continue then do notEndBlock
191 declBody
192 else fail "End of readable input"
193 where declBody :: IdrisParser [PDecl]
194 declBody = declBody'
195 <|> using_ syn
196 <|> params syn
197 <|> mutual syn
198 <|> namespace syn
199 <|> class_ syn
200 <|> instance_ syn
201 <|> do d <- dsl syn; return [d]
202 <|> directive syn
203 <|> provider syn
204 <|> transform syn
205 <|> do import_; fail "imports must be at top of file"
206 <?> "declaration"
207 declBody' :: IdrisParser [PDecl]
208 declBody' = do d <- decl' syn
209 i <- get
210 let d' = fmap (debindApp syn . (desugar syn i)) d
211 return [d']
213{- | Parses a top-level declaration with possible syntax sugar
216Decl' ::=
217 Fixity
218 | FunDecl'
219 | Data
220 | Record
221 | SyntaxDecl
222 ;
224-}
225decl' :: SyntaxInfo -> IdrisParser PDecl
226decl' syn = fixity
227 <|> syntaxDecl syn
228 <|> fnDecl' syn
229 <|> data_ syn
230 <|> record syn
231 <?> "declaration"
233{- | Parses a syntax extension declaration (and adds the rule to parser state)
236 SyntaxDecl ::= SyntaxRule;
238-}
239syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
240syntaxDecl syn = do s <- syntaxRule syn
241 i <- get
242 put (i `addSyntax` s)
243 fc <- getFC
244 return (PSyntax fc s)
246-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.
247addSyntax :: IState -> Syntax -> IState
248addSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
249 syntax_keywords = ks ++ ns,
250 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc }
251 where rs = syntax_rules i
252 ns = syntax_keywords i
253 ibc = ibc_write i
254 ks = map show (syntaxNames s)
256-- | Like 'addSyntax', but no effect on the IBC.
257addReplSyntax :: IState -> Syntax -> IState
258addReplSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
259 syntax_keywords = ks ++ ns }
260 where rs = syntax_rules i
261 ns = syntax_keywords i
262 ks = map show (syntaxNames s)
264{- | Parses a syntax extension declaration
267SyntaxRuleOpts ::= 'term' | 'pattern';
271SyntaxRule ::=
272 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
276SyntaxSym ::= '[' Name_t ']'
277 | '{' Name_t '}'
278 | Name_t
279 | StringLiteral_t
280 ;
282-}
283syntaxRule :: SyntaxInfo -> IdrisParser Syntax
284syntaxRule syn
285 = do sty <- try (do
286 pushIndent
287 sty <- option AnySyntax (do reserved "term"; return TermSyntax
288 <|> do reserved "pattern"; return PatternSyntax)
289 reserved "syntax"
290 return sty)
291 syms <- some syntaxSym
292 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
293 let ns = mapMaybe getName syms
294 when (length ns /= length (nub ns))
295 $ unexpected "repeated variable in syntax rule"
296 lchar '='
297 tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]
298 terminator
299 return (Rule (mkSimple syms) tm sty)
300 where
301 isExpr (Expr _) = True
302 isExpr _ = False
303 getName (Expr n) = Just n
304 getName _ = Nothing
305 -- Can't parse two full expressions (i.e. expressions with application) in a row
306 -- so change them both to a simple expression
307 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
308 mkSimple xs = mkSimple' xs
310 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
311 mkSimple es
312 -- Can't parse a full expression followed by operator like characters due to ambiguity
313 mkSimple' (Expr e : Symbol s : es)
314 | takeWhile (`elem` opChars) ts /= "" && ts `notElem` invalidOperators = SimpleExpr e : Symbol s : mkSimple' es
315 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s
316 mkSimple' (e : es) = e : mkSimple' es
317 mkSimple' [] = []
319 -- Prevent syntax variable capture by making all binders under syntax unique
320 -- (the ol' Common Lisp GENSYM approach)
321 uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
322 uniquifyBinders userNames = fixBind []
323 where
324 fixBind :: [(Name, Name)] -> PTerm -> IdrisParser PTerm
325 fixBind rens (PRef fc n) | Just n' <- lookup n rens =
326 return $ PRef fc n'
327 fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =
328 return $ PPatvar fc n'
329 fixBind rens (PLam fc n nfc ty body)
330 | n `elem` userNames = liftM2 (PLam fc n nfc) (fixBind rens ty) (fixBind rens body)
331 | otherwise =
332 do ty' <- fixBind rens ty
333 n' <- gensym n
334 body' <- fixBind ((n,n'):rens) body
335 return $ PLam fc n' nfc ty' body'
336 fixBind rens (PPi plic n nfc argTy body)
337 | n `elem` userNames = liftM2 (PPi plic n nfc) (fixBind rens argTy) (fixBind rens body)
338 | otherwise =
339 do ty' <- fixBind rens argTy
340 n' <- gensym n
341 body' <- fixBind ((n,n'):rens) body
342 return $ (PPi plic n' nfc ty' body')
343 fixBind rens (PLet fc n nfc ty val body)
344 | n `elem` userNames = liftM3 (PLet fc n nfc)
345 (fixBind rens ty)
346 (fixBind rens val)
347 (fixBind rens body)
348 | otherwise =
349 do ty' <- fixBind rens ty
350 val' <- fixBind rens val
351 n' <- gensym n
352 body' <- fixBind ((n,n'):rens) body
353 return $ PLet fc n' nfc ty' val' body'
354 fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =
355 return $ PMatchApp fc n'
356 fixBind rens x = descendM (fixBind rens) x
358 gensym :: Name -> IdrisParser Name
359 gensym n = do ist <- get
360 let idx = idris_name ist
361 put ist { idris_name = idx + 1 }
362 return $ sMN idx (show n)
364{- | Parses a syntax symbol (either binding variable, keyword or expression)
367SyntaxSym ::= '[' Name_t ']'
368 | '{' Name_t '}'
369 | Name_t
370 | StringLiteral_t
371 ;
373 -}
374syntaxSym :: IdrisParser SSymbol
375syntaxSym = try (do lchar '['; n <- fst <$> name; lchar ']'
376 return (Expr n))
377 <|> try (do lchar '{'; n <- fst <$> name; lchar '}'
378 return (Binding n))
379 <|> do n <- fst <$> iName []
380 return (Keyword n)
381 <|> do sym <- fmap fst stringLiteral
382 return (Symbol sym)
383 <?> "syntax symbol"
385{- | Parses a function declaration with possible syntax sugar
388 FunDecl ::= FunDecl';
390-}
391fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
392fnDecl syn = try (do notEndBlock
393 d <- fnDecl' syn
394 i <- get
395 let d' = fmap (desugar syn i) d
396 return [d']) <?> "function declaration"
398{-| Parses a function declaration
401 FunDecl' ::=
402 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
403 | Postulate
404 | Pattern
405 | CAF
406 ;
408-}
409fnDecl' :: SyntaxInfo -> IdrisParser PDecl
410fnDecl' syn = checkFixity $
411 do (doc, argDocs, fc, opts', n, nfc, acc) <- try (do
412 pushIndent
413 (doc, argDocs) <- docstring syn
414 ist <- get
415 let initOpts = if default_total ist
416 then [TotalFn]
417 else []
418 opts <- fnOpts initOpts
419 acc <- optional accessibility
420 opts' <- fnOpts opts
421 (n_in, nfc) <- fnName
422 let n = expandNS syn n_in
423 fc <- getFC
424 lchar ':'
425 return (doc, argDocs, fc, opts', n, nfc, acc))
426 ty <- typeExpr (allowImp syn)
427 terminator
428 addAcc n acc
429 return (PTy doc argDocs syn fc opts' n nfc ty)
430 <|> postulate syn
431 <|> caf syn
432 <|> pattern syn
433 <?> "function declaration"
434 where checkFixity :: IdrisParser PDecl -> IdrisParser PDecl
435 checkFixity p = do decl <- p
436 case getName decl of
437 Nothing -> return decl
438 Just n -> do fOk <- fixityOK n
439 unless fOk . fail $
440 "Missing fixity declaration for " ++ show n
441 return decl
442 getName (PTy _ _ _ _ _ n _ _) = Just n
443 getName _ = Nothing
444 fixityOK (NS n _) = fixityOK n
445 fixityOK (UN n) | all (flip elem opChars) (str n) =
446 do fixities <- fmap idris_infixes get
447 return . elem (str n) . map (\ (Fix _ op) -> op) $ fixities
448 | otherwise = return True
449 fixityOK _ = return True
451{-| Parses function options given initial options
454FnOpts ::= 'total'
455 | 'partial'
456 | 'covering'
457 | 'implicit'
458 | '%' 'no_implicit'
459 | '%' 'assert_total'
460 | '%' 'error_handler'
461 | '%' 'reflection'
462 | '%' 'specialise' '[' NameTimesList? ']'
463 ;
467NameTimes ::= FnName Natural?;
471NameTimesList ::=
472 NameTimes
473 | NameTimes ',' NameTimesList
474 ;
476-}
477-- FIXME: Check compatability for function options (i.e. partal/total)
478--
479-- Issue #1574 on the issue tracker.
480-- https://github.com/idris-lang/Idris-dev/issues/1574
481fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
482fnOpts opts
483 = do reserved "total"; fnOpts (TotalFn : opts)
484 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
485 <|> do reserved "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))
486 <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;
487 fnOpts (CExport c : opts)
488 <|> do try (lchar '%' *> reserved "no_implicit");
489 fnOpts (NoImplicit : opts)
490 <|> do try (lchar '%' *> reserved "inline");
491 fnOpts (Inlinable : opts)
492 <|> do try (lchar '%' *> reserved "assert_total");
493 fnOpts (AssertTotal : opts)
494 <|> do try (lchar '%' *> reserved "error_handler");
495 fnOpts (ErrorHandler : opts)
496 <|> do try (lchar '%' *> reserved "error_reverse");
497 fnOpts (ErrorReverse : opts)
498 <|> do try (lchar '%' *> reserved "reflection");
499 fnOpts (Reflection : opts)
500 <|> do try (lchar '%' *> reserved "hint");
501 fnOpts (AutoHint : opts)
502 <|> do lchar '%'; reserved "specialise";
503 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
504 fnOpts (Specialise ns : opts)
505 <|> do reserved "implicit"; fnOpts (Implicit : opts)
506 <|> return opts
507 <?> "function modifier"
508 where nameTimes :: IdrisParser (Name, Maybe Int)
509 nameTimes = do n <- fst <$> fnName
510 t <- option Nothing (do reds <- fmap fst natural
511 return (Just (fromInteger reds)))
512 return (n, t)
514{- | Parses a postulate
517Postulate ::=
518 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
519 ;
521-}
522postulate :: SyntaxInfo -> IdrisParser PDecl
523postulate syn = do (doc, ext)
524 <- try $ do (doc, _) <- docstring syn
525 pushIndent
526 ext <- ppostDecl
527 return (doc, ext)
528 ist <- get
529 let initOpts = if default_total ist
530 then [TotalFn]
531 else []
532 opts <- fnOpts initOpts
533 acc <- optional accessibility
534 opts' <- fnOpts opts
535 n_in <- fst <$> fnName
536 let n = expandNS syn n_in
537 lchar ':'
538 ty <- typeExpr (allowImp syn)
539 fc <- getFC
540 terminator
541 addAcc n acc
542 return (PPostulate ext doc syn fc opts' n ty)
543 <?> "postulate"
544 where ppostDecl = do reserved "postulate"; return False
545 <|> do lchar '%'; reserved "extern"; return True
546{- | Parses a using declaration
549Using ::=
550 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
551 ;
553 -}
554using_ :: SyntaxInfo -> IdrisParser [PDecl]
555using_ syn =
556 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
557 openBlock
558 let uvars = using syn
559 ds <- many (decl (syn { using = uvars ++ ns }))
560 closeBlock
561 return (concat ds)
562 <?> "using declaration"
564{- | Parses a parameters declaration
567Params ::=
568 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
569 ;
571 -}
572params :: SyntaxInfo -> IdrisParser [PDecl]
573params syn =
574 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
575 let ns' = [(n, ty) | (n, _, ty) <- ns]
576 openBlock
577 let pvars = syn_params syn
578 ds <- many (decl syn { syn_params = pvars ++ ns' })
579 closeBlock
580 fc <- getFC
581 return [PParams fc ns' (concat ds)]
582 <?> "parameters declaration"
584{- | Parses a mutual declaration (for mutually recursive functions)
587Mutual ::=
588 'mutual' OpenBlock Decl* CloseBlock
589 ;
591-}
592mutual :: SyntaxInfo -> IdrisParser [PDecl]
593mutual syn =
594 do reserved "mutual"
595 openBlock
596 let pvars = syn_params syn
597 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
598 closeBlock
599 fc <- getFC
600 return [PMutual fc (concat ds)]
601 <?> "mutual block"
603{-| Parses a namespace declaration
606Namespace ::=
607 'namespace' identifier OpenBlock Decl+ CloseBlock
608 ;
610-}
611namespace :: SyntaxInfo -> IdrisParser [PDecl]
612namespace syn =
613 do reserved "namespace"
614 (n, nfc) <- identifier
615 openBlock
616 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
617 closeBlock
618 return [PNamespace n nfc (concat ds)]
619 <?> "namespace declaration"
621{- | Parses a methods block (for instances)
624 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
626-}
627instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
628instanceBlock syn = do reserved "where"
629 openBlock
630 ds <- many (fnDecl syn)
631 closeBlock
632 return (concat ds)
633 <?> "instance block"
635{- | Parses a methods and instances block (for type classes)
638MethodOrInstance ::=
639 FnDecl
640 | Instance
641 ;
645ClassBlock ::=
646 'where' OpenBlock Constructor? MethodOrInstance* CloseBlock
647 ;
649-}
650classBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])
651classBlock syn = do reserved "where"
652 openBlock
653 (cn, cd) <- option (Nothing, emptyDocstring) $
654 try (do (doc, _) <- option noDocs docComment
655 n <- constructor
656 return (Just n, doc))
657 ist <- get
658 let cd' = annotate syn ist cd
660 ds <- many (notEndBlock >> instance_ syn <|> fnDecl syn)
661 closeBlock
662 return (cn, cd', concat ds)
663 <?> "class block"
665 where
666 constructor :: IdrisParser (Name, FC)
667 constructor = reserved "constructor" *> fnName
669 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)
670 annotate syn ist = annotCode $ tryFullExpr syn ist
672{-| Parses a type class declaration
675ClassArgument ::=
676 Name
677 | '(' Name ':' Expr ')'
678 ;
682Class ::=
683 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
684 ;
686-}
687class_ :: SyntaxInfo -> IdrisParser [PDecl]
688class_ syn = do (doc, argDocs, acc)
689 <- try (do (doc, argDocs) <- docstring syn
690 acc <- optional accessibility
691 reserved "class"
692 return (doc, argDocs, acc))
693 fc <- getFC
694 cons <- constraintList syn
695 let cons' = [(c, ty) | (c, _, ty) <- cons]
696 (n_in, nfc) <- fnName
697 let n = expandNS syn n_in
698 cs <- many carg
699 fds <- option [(cn, NoFC) | (cn, _, _) <- cs] fundeps
700 (cn, cd, ds) <- option (Nothing, fst noDocs, []) (classBlock syn)
701 accData acc n (concatMap declared ds)
702 return [PClass doc syn fc cons' n nfc cs argDocs fds ds cn cd]
703 <?> "type-class declaration"
704 where
705 fundeps :: IdrisParser [(Name, FC)]
706 fundeps = do lchar '|'; sepBy name (lchar ',')
708 carg :: IdrisParser (Name, FC, PTerm)
709 carg = do lchar '('; (i, ifc) <- name; lchar ':'; ty <- expr syn; lchar ')'
710 return (i, ifc, ty)
711 <|> do (i, ifc) <- name
712 fc <- getFC
713 return (i, ifc, PType fc)
715{- | Parses a type class instance declaration
718 Instance ::=
719 DocComment_t? 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
720 ;
724InstanceName ::= '[' Name ']';
726-}
727instance_ :: SyntaxInfo -> IdrisParser [PDecl]
728instance_ syn = do (doc, argDocs)
729 <- try (docstring syn <* reserved "instance")
730 fc <- getFC
731 en <- optional instanceName
732 cs <- constraintList syn
733 let cs' = [(c, ty) | (c, _, ty) <- cs]
734 (cn, cnfc) <- fnName
735 args <- many (simpleExpr syn)
736 let sc = PApp fc (PRef cnfc cn) (map pexp args)
737 let t = bindList (PPi constraint) cs sc
738 ds <- option [] (instanceBlock syn)
739 return [PInstance doc argDocs syn fc cs' cn cnfc args t en ds]
740 <?> "instance declaration"
741 where instanceName :: IdrisParser Name
742 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'
743 let n = expandNS syn n_in
744 return n
745 <?> "instance name"
748-- | Parse a docstring
749docstring :: SyntaxInfo
750 -> IdrisParser (Docstring (Either Err PTerm),
751 [(Name,Docstring (Either Err PTerm))])
752docstring syn = do (doc, argDocs) <- option noDocs docComment
753 ist <- get
754 let doc' = annotCode (tryFullExpr syn ist) doc
755 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
756 | (n, d) <- argDocs ]
757 return (doc', argDocs')
760{- | Parses a using declaration list
763UsingDeclList ::=
764 UsingDeclList'
765 | NameList TypeSig
766 ;
770UsingDeclList' ::=
771 UsingDecl
772 | UsingDecl ',' UsingDeclList'
773 ;
777NameList ::=
778 Name
779 | Name ',' NameList
780 ;
782-}
783usingDeclList :: SyntaxInfo -> IdrisParser [Using]
784usingDeclList syn
785 = try (sepBy1 (usingDecl syn) (lchar ','))
786 <|> do ns <- sepBy1 (fst <$> name) (lchar ',')
787 lchar ':'
788 t <- typeExpr (disallowImp syn)
789 return (map (\x -> UImplicit x t) ns)
790 <?> "using declaration list"
792{- |Parses a using declaration
795UsingDecl ::=
796 FnName TypeSig
797 | FnName FnName+
798 ;
800-}
801usingDecl :: SyntaxInfo -> IdrisParser Using
802usingDecl syn = try (do x <- fst <$> fnName
803 lchar ':'
804 t <- typeExpr (disallowImp syn)
805 return (UImplicit x t))
806 <|> do c <- fst <$> fnName
807 xs <- some (fst <$> fnName)
808 return (UConstraint c xs)
809 <?> "using declaration"
811{- | Parse a clause with patterns
814Pattern ::= Clause;
816-}
817pattern :: SyntaxInfo -> IdrisParser PDecl
818pattern syn = do fc <- getFC
819 clause <- clause syn
820 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
821 <?> "pattern"
823{- | Parse a constant applicative form declaration
826CAF ::= 'let' FnName '=' Expr Terminator;
828-}
829caf :: SyntaxInfo -> IdrisParser PDecl
830caf syn = do reserved "let"
831 n_in <- fst <$> fnName; let n = expandNS syn n_in
832 lchar '='
833 t <- expr syn
834 terminator
835 fc <- getFC
836 return (PCAF fc n t)
837 <?> "constant applicative form declaration"
839{- | Parse an argument expression
842ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
844-}
845argExpr :: SyntaxInfo -> IdrisParser PTerm
846argExpr syn = let syn' = syn { inPattern = True } in
847 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
848 <?> "argument expression"
850{- | Parse a right hand side of a function
853RHS ::= '=' Expr
854 | '?=' RHSName? Expr
855 | Impossible
856 ;
860RHSName ::= '{' FnName '}';
862-}
863rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
864rhs syn n = do lchar '='; expr syn
865 <|> do symbol "?=";
866 fc <- getFC
867 name <- option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";
868 return n)
869 r <- expr syn
870 return (addLet fc name r)
871 <|> impossible
872 <?> "function right hand side"
873 where mkN :: Name -> Name
874 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
875 then sUN "infix_op_lemma_1"
876 else sUN (str x++"_lemma_1")
877 mkN (NS x n) = NS (mkN x) n
878 n' :: Name
879 n' = mkN n
880 addLet :: FC -> Name -> PTerm -> PTerm
881 addLet fc nm (PLet fc' n nfc ty val r) = PLet fc' n nfc ty val (addLet fc nm r)
882 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
883 where addLetC (l, r) = (l, addLet fc nm r)
884 addLet fc nm r = (PLet fc (sUN "value") NoFC Placeholder r (PMetavar NoFC nm))
886{- |Parses a function clause
889RHSOrWithBlock ::= RHS WhereOrTerminator
890 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
891 ;
895Clause ::= WExpr+ RHSOrWithBlock
896 | SimpleExpr '<==' FnName RHS WhereOrTerminator
897 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
898 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
899 ;
903ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
907WhereOrTerminator ::= WhereBlock | Terminator;
909-}
910clause :: SyntaxInfo -> IdrisParser PClause
911clause syn
912 = do wargs <- try (do pushIndent; some (wExpr syn))
913 fc <- getFC
914 ist <- get
915 n <- case lastParse ist of
916 Just t -> return t
917 Nothing -> fail "Invalid clause"
918 (do r <- rhs syn n
919 let ctxt = tt_ctxt ist
920 let wsyn = syn { syn_namespace = [] }
921 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
922 popIndent
923 return x,
924 do terminator
925 return ([], [])]
926 return $ PClauseR fc wargs r wheres) <|> (do
927 popIndent
928 reserved "with"
929 wval <- simpleExpr syn
930 pn <- optProof
931 openBlock
932 ds <- some $ fnDecl syn
933 let withs = concat ds
934 closeBlock
935 return $ PWithR fc wargs wval pn withs)
936 <|> do ty <- try (do pushIndent
937 ty <- simpleExpr syn
938 symbol "<=="
939 return ty)
940 fc <- getFC
941 n_in <- fst <$> fnName; let n = expandNS syn n_in
942 r <- rhs syn n
943 ist <- get
944 let ctxt = tt_ctxt ist
945 let wsyn = syn { syn_namespace = [] }
946 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
947 popIndent
948 return x,
949 do terminator
950 return ([], [])]
951 let capp = PLet fc (sMN 0 "match") NoFC
952 ty
953 (PMatchApp fc n)
954 (PRef fc (sMN 0 "match"))
955 ist <- get
956 put (ist { lastParse = Just n })
957 return $ PClause fc n capp [] r wheres
958 <|> do (l, op, nfc) <- try (do
959 pushIndent
960 l <- argExpr syn
961 (op, nfc) <- operatorFC
962 when (op == "=" || op == "?=" ) $
963 fail "infix clause definition with \"=\" and \"?=\" not supported "
964 return (l, op, nfc))
965 let n = expandNS syn (sUN op)
966 r <- argExpr syn
967 fc <- getFC
968 wargs <- many (wExpr syn)
969 (do rs <- rhs syn n
970 let wsyn = syn { syn_namespace = [] }
971 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
972 popIndent
973 return x,
974 do terminator
975 return ([], [])]
976 ist <- get
977 let capp = PApp fc (PRef nfc n) [pexp l, pexp r]
978 put (ist { lastParse = Just n })
979 return $ PClause fc n capp wargs rs wheres) <|> (do
980 popIndent
981 reserved "with"
982 wval <- bracketed syn
983 pn <- optProof
984 openBlock
985 ds <- some $ fnDecl syn
986 closeBlock
987 ist <- get
988 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
989 let withs = map (fillLHSD n capp wargs) $ concat ds
990 put (ist { lastParse = Just n })
991 return $ PWith fc n capp wargs wval pn withs)
992 <|> do pushIndent
993 (n_in, nfc) <- fnName; let n = expandNS syn n_in
994 cargs <- many (constraintArg syn)
995 fc <- getFC
996 args <- many (try (implicitArg (syn { inPattern = True } ))
997 <|> (fmap pexp (argExpr syn)))
998 wargs <- many (wExpr syn)
999 let capp = PApp fc (PRef nfc n)
1000 (cargs ++ args)
1001 (do r <- rhs syn n
1002 ist <- get
1003 let ctxt = tt_ctxt ist
1004 let wsyn = syn { syn_namespace = [] }
1005 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1006 popIndent
1007 return x,
1008 do terminator
1009 return ([], [])]
1010 ist <- get
1011 put (ist { lastParse = Just n })
1012 return $ PClause fc n capp wargs r wheres) <|> (do
1013 reserved "with"
1014 ist <- get
1015 put (ist { lastParse = Just n })
1016 wval <- bracketed syn
1017 pn <- optProof
1018 openBlock
1019 ds <- some $ fnDecl syn
1020 let withs = map (fillLHSD n capp wargs) $ concat ds
1021 closeBlock
1022 popIndent
1023 return $ PWith fc n capp wargs wval pn withs)
1024 <?> "function clause"
1025 where
1026 optProof = option Nothing (do reserved "proof"
1027 n <- fnName
1028 return (Just n))
1030 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
1031 fillLHS n capp owargs (PClauseR fc wargs v ws)
1032 = PClause fc n capp (owargs ++ wargs) v ws
1033 fillLHS n capp owargs (PWithR fc wargs v pn ws)
1034 = PWith fc n capp (owargs ++ wargs) v pn
1035 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1036 fillLHS _ _ _ c = c
1038 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
1039 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1040 fillLHSD n c a x = x
1042{-| Parses with pattern
1045WExpr ::= '|' Expr';
1048wExpr :: SyntaxInfo -> IdrisParser PTerm
1049wExpr syn = do lchar '|'
1050 expr' (syn { inPattern = True })
1051 <?> "with pattern"
1053{- | Parses a where block
1056WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
1059whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
1060whereBlock n syn
1061 = do reserved "where"
1062 ds <- indentedBlock1 (decl syn)
1063 let dns = concatMap (concatMap declared) ds
1064 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1065 <?> "where block"
1067{- |Parses a code generation target language name
1070Codegen ::= 'C'
1071 | 'Java'
1072 | 'JavaScript'
1073 | 'Node'
1074 | 'LLVM'
1075 | 'Bytecode'
1079codegen_ :: IdrisParser Codegen
1080codegen_ = do n <- fst <$> identifier
1081 return (Via (map toLower n))
1082 <|> do reserved "Bytecode"; return Bytecode
1083 <?> "code generation language"
1085{- |Parses a compiler directive
1087StringList ::=
1088 String
1089 | String ',' StringList
1094Directive ::= '%' Directive';
1098Directive' ::= 'lib' CodeGen String_t
1099 | 'link' CodeGen String_t
1100 | 'flag' CodeGen String_t
1101 | 'include' CodeGen String_t
1102 | 'hide' Name
1103 | 'freeze' Name
1104 | 'access' Accessibility
1105 | 'default' Totality
1106 | 'logging' Natural
1107 | 'dynamic' StringList
1108 | 'name' Name NameList
1109 | 'error_handlers' Name NameList
1110 | 'language' 'TypeProviders'
1111 | 'language' 'ErrorReflection'
1115directive :: SyntaxInfo -> IdrisParser [PDecl]
1116directive syn = do try (lchar '%' *> reserved "lib")
1117 cgn <- codegen_
1118 lib <- fmap fst stringLiteral
1119 return [PDirective (DLib cgn lib)]
1120 <|> do try (lchar '%' *> reserved "link")
1121 cgn <- codegen_; obj <- fst <$> stringLiteral
1122 return [PDirective (DLink cgn obj)]
1123 <|> do try (lchar '%' *> reserved "flag")
1124 cgn <- codegen_; flag <- fst <$> stringLiteral
1125 return [PDirective (DFlag cgn flag)]
1126 <|> do try (lchar '%' *> reserved "include")
1127 cgn <- codegen_
1128 hdr <- fst <$> stringLiteral
1129 return [PDirective (DInclude cgn hdr)]
1130 <|> do try (lchar '%' *> reserved "hide"); n <- fst <$> fnName
1131 return [PDirective (DHide n)]
1132 <|> do try (lchar '%' *> reserved "freeze"); n <- fst <$> iName []
1133 return [PDirective (DFreeze n)]
1134 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1135 return [PDirective (DAccess acc)]
1136 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1137 i <- get
1138 put (i { default_total = tot } )
1139 return [PDirective (DDefault tot)]
1140 <|> do try (lchar '%' *> reserved "logging")
1141 i <- fst <$> natural
1142 return [PDirective (DLogging i)]
1143 <|> do try (lchar '%' *> reserved "dynamic")
1144 libs <- sepBy1 (fmap fst stringLiteral) (lchar ',')
1145 return [PDirective (DDynamicLibs libs)]
1146 <|> do try (lchar '%' *> reserved "name")
1147 ty <- fst <$> fnName
1148 ns <- sepBy1 (fst <$> name) (lchar ',')
1149 return [PDirective (DNameHint ty ns)]
1150 <|> do try (lchar '%' *> reserved "error_handlers")
1151 fn <- fst <$> fnName
1152 arg <- fst <$> fnName
1153 ns <- sepBy1 (fst <$> name) (lchar ',')
1154 return [PDirective (DErrorHandlers fn arg ns) ]
1155 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1156 return [PDirective (DLanguage ext)]
1157 <|> do fc <- getFC
1158 try (lchar '%' *> reserved "used")
1159 fn <- fst <$> fnName
1160 arg <- fst <$> iName []
1161 return [PDirective (DUsed fc fn arg)]
1162 <?> "directive"
1164pLangExt :: IdrisParser LanguageExt
1165pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1166 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1168{- | Parses a totality
1171Totality ::= 'partial' | 'total'
1175totality :: IdrisParser Bool
1176totality
1177 = do reserved "total"; return True
1178 <|> do reserved "partial"; return False
1180{- | Parses a type provider
1183Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1184ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1186 -}
1187provider :: SyntaxInfo -> IdrisParser [PDecl]
1188provider syn = do doc <- try (do (doc, _) <- docstring syn
1189 lchar '%'
1190 reserved "provide"
1191 return doc)
1192 provideTerm doc <|> providePostulate doc
1193 <?> "type provider"
1194 where provideTerm doc =
1195 do lchar '('; n <- fst <$> fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1196 fc <- getFC
1197 reserved "with"
1198 e <- expr syn <?> "provider expression"
1199 return [PProvider doc syn fc (ProvTerm t e) n]
1200 providePostulate doc =
1201 do reserved "postulate"
1202 n <- fst <$> fnName
1203 fc <- getFC
1204 reserved "with"
1205 e <- expr syn <?> "provider expression"
1206 return [PProvider doc syn fc (ProvPostulate e) n]
1208{- | Parses a transform
1211Transform ::= '%' 'transform' Expr '==>' Expr
1214transform :: SyntaxInfo -> IdrisParser [PDecl]
1215transform syn = do try (lchar '%' *> reserved "transform")
1216 -- leave it unchecked, until we work out what this should
1217 -- actually mean...
1218-- safety <- option True (do reserved "unsafe"
1219-- return False)
1220 l <- expr syn
1221 fc <- getFC
1222 symbol "==>"
1223 r <- expr syn
1224 return [PTransform fc False l r]
1225 <?> "transform"
1228{- * Loading and parsing -}
1229{- | Parses an expression from input -}
1230parseExpr :: IState -> String -> Result PTerm
1231parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1233{- | Parses a constant form input -}
1234parseConst :: IState -> String -> Result Const
1235parseConst st = runparser (fmap fst constant) st "(input)"
1237{- | Parses a tactic from input -}
1238parseTactic :: IState -> String -> Result PTactic
1239parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1241-- | Parse module header and imports
1242parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Delta)
1243parseImports fname input
1244 = do i <- getIState
1245 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1246 Failure err -> fail (show err)
1247 Success (x, annots, i) ->
1248 do putIState i
1249 fname' <- runIO $ Dir.makeAbsolute fname
1250 sendHighlighting $ addPath annots fname'
1251 return x
1252 where imports :: IdrisParser ((Maybe (Docstring ()), [String],
1253 [ImportInfo],
1254 Maybe Delta),
1255 [(FC, OutputAnnotation)], IState)
1256 imports = do whiteSpace
1257 (mdoc, mname, annots) <- moduleHeader
1258 ps <- many import_
1259 mrk <- mark
1260 isEof <- lookAheadMatches eof
1261 let mrk' = if isEof
1262 then Nothing
1263 else Just mrk
1264 i <- get
1265 return ((mdoc, mname, ps, mrk'), annots, i)
1266 addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]
1267 addPath [] _ = []
1268 addPath ((fc, AnnNamespace ns Nothing) : annots) path =
1269 (fc, AnnNamespace ns (Just path)) : addPath annots path
1270 addPath (annot:annots) path = annot : addPath annots path
1272-- | There should be a better way of doing this...
1273findFC :: Doc -> (FC, String)
1274findFC x = let s = show (plain x) in
1275 case span (/= ':') s of
1276 (failname, ':':rest) -> case span isDigit rest of
1277 (line, ':':rest') -> case span isDigit rest' of
1278 (col, ':':msg) -> let pos = (read line, read col) in
1279 (FC failname pos pos, msg)
1281-- | Check if the coloring matches the options and corrects if necessary
1282fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1283fixColour False doc = ANSI.plain doc
1284fixColour True doc = doc
1286-- | A program is a list of declarations, possibly with associated
1287-- documentation strings.
1288parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1289 Idris [PDecl]
1290parseProg syn fname input mrk
1291 = do i <- getIState
1292 case runparser mainProg i fname input of
1293 Failure doc -> do -- FIXME: Get error location from trifecta
1294 -- this can't be the solution!
1295 -- Issue #1575 on the issue tracker.
1296 -- https://github.com/idris-lang/Idris-dev/issues/1575
1297 let (fc, msg) = findFC doc
1298 i <- getIState
1299 case idris_outputmode i of
1300 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1301 IdeMode n h -> iWarn fc (P.text msg)
1302 putIState (i { errSpan = Just fc })
1303 return []
1304 Success (x, i) -> do putIState i
1305 reportParserWarnings
1306 return $ collect x
1307 where mainProg :: IdrisParser ([PDecl], IState)
1308 mainProg = case mrk of
1309 Nothing -> do i <- get; return ([], i)
1310 Just mrk -> do
1311 release mrk
1312 ds <- prog syn
1313 i' <- get
1314 return (ds, i')
1316{- | Load idris module and show error if something wrong happens -}
1317loadModule :: FilePath -> Idris (Maybe String)
1318loadModule f
1319 = idrisCatch (loadModule' f)
1320 (\e -> do setErrSpan (getErrSpan e)
1321 ist <- getIState
1322 iWarn (getErrSpan e) $ pprintErr ist e
1323 return Nothing)
1325{- | Load idris module -}
1326loadModule' :: FilePath -> Idris (Maybe String)
1327loadModule' f
1328 = do i <- getIState
1329 let file = takeWhile (/= ' ') f
1330 ibcsd <- valIBCSubDir i
1331 ids <- allImportDirs
1332 fp <- findImport ids ibcsd file
1333 if file `elem` imported i
1334 then do iLOG $ "Already read " ++ file
1335 return Nothing
1336 else do putIState (i { imported = file : imported i })
1337 case fp of
1338 IDR fn -> loadSource False fn Nothing
1339 LIDR fn -> loadSource True fn Nothing
1340 IBC fn src ->
1341 idrisCatch (loadIBC True fn)
1342 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1343 case src of
1344 IDR sfn -> loadSource False sfn Nothing
1345 LIDR sfn -> loadSource True sfn Nothing)
1346 return $ Just file
1348{- | Load idris code from file -}
1349loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()
1350loadFromIFile reexp i@(IBC fn src) maxline
1351 = do iLOG $ "Skipping " ++ getSrcFile i
1352 idrisCatch (loadIBC reexp fn)
1353 (\err -> ierror $ LoadingFailed fn err)
1354 where
1355 getSrcFile (IDR fn) = fn
1356 getSrcFile (LIDR fn) = fn
1357 getSrcFile (IBC f src) = getSrcFile src
1359loadFromIFile _ (IDR fn) maxline = loadSource' False fn maxline
1360loadFromIFile _ (LIDR fn) maxline = loadSource' True fn maxline
1362{-| Load idris source code and show error if something wrong happens -}
1363loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1364loadSource' lidr r maxline
1365 = idrisCatch (loadSource lidr r maxline)
1366 (\e -> do setErrSpan (getErrSpan e)
1367 ist <- getIState
1368 case e of
1369 At f e' -> iWarn f (pprintErr ist e')
1370 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1372{- | Load Idris source code-}
1373loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1374loadSource lidr f toline
1375 = do iLOG ("Reading " ++ f)
1376 i <- getIState
1377 let def_total = default_total i
1378 file_in <- runIO $ readSource f
1379 file <- if lidr then tclift $ unlit f file_in else return file_in
1380 (mdocs, mname, imports_in, pos) <- parseImports f file
1381 ai <- getAutoImports
1382 let imports = map (\n -> ImportInfo True n Nothing [] NoFC NoFC) ai ++ imports_in
1383 ids <- allImportDirs
1384 ibcsd <- valIBCSubDir i
1385 mapM_ (\(re, f, ns, nfc) ->
1386 do fp <- findImport ids ibcsd f
1387 case fp of
1388 LIDR fn -> ifail $ "No ibc for " ++ f
1389 IDR fn -> ifail $ "No ibc for " ++ f
1390 IBC fn src ->
1391 do loadIBC True fn
1392 let srcFn = case src of
1393 IDR fn -> Just fn
1394 LIDR fn -> Just fn
1395 _ -> Nothing
1396 srcFnAbs <- case srcFn of
1397 Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)
1398 Nothing -> return Nothing
1399 sendHighlighting [(nfc, AnnNamespace ns srcFnAbs)])
1400 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]
1401 reportParserWarnings
1403 -- process and check module aliases
1404 let modAliases = M.fromList
1405 [ (prep alias, prep realName)
1406 | ImportInfo { import_reexport = reexport
1407 , import_path = realName
1408 , import_rename = Just (alias, _)
1409 , import_location = fc } <- imports
1411 prep = map T.pack . reverse . Spl.splitOn [pathSeparator]
1412 aliasNames = [ (alias, fc)
1413 | ImportInfo { import_rename = Just (alias, _)
1414 , import_location = fc } <- imports
1416 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1417 case map head . filter ((/= 1) . length) $ histogram of
1418 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1419 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1421 i <- getIState
1422 putIState (i { default_access = Hidden, module_aliases = modAliases })
1423 clearIBC -- start a new .ibc file
1424 -- record package info in .ibc
1425 imps <- allImportDirs
1426 mapM_ addIBC (map IBCImportDir imps)
1427 mapM_ (addIBC . IBCImport)
1428 [ (reexport, realName)
1429 | ImportInfo { import_reexport = reexport
1430 , import_path = realName
1431 } <- imports
1433 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1434 maxline = toline }
1435 ist <- getIState
1436 -- Save the span from parsing the module header, because
1437 -- an empty program parse might obliterate it.
1438 let oldSpan = idris_parsedSpan ist
1439 ds' <- parseProg syntax f file pos
1441 case (ds', oldSpan) of
1442 ([], Just fc) ->
1443 -- If no program elements were parsed, we dind't
1444 -- get a loaded region in the IBC file. That
1445 -- means we need to add it back.
1446 do ist <- getIState
1447 putIState ist { idris_parsedSpan = oldSpan
1448 , ibc_write = IBCParsedRegion fc :
1449 ibc_write ist
1451 _ -> return ()
1453 -- Parsing done, now process declarations
1455 let ds = namespaces mname ds'
1456 logLvl 3 (show $ showDecls verbosePPOption ds)
1457 i <- getIState
1458 logLvl 10 (show (toAlist (idris_implicits i)))
1459 logLvl 3 (show (idris_infixes i))
1460 -- Now add all the declarations to the context
1461 v <- verbose
1462 when v $ iputStrLn $ "Type checking " ++ f
1463 -- we totality check after every Mutual block, so if
1464 -- anything is a single definition, wrap it in a
1465 -- mutual block on its own
1466 elabDecls toplevel (map toMutual ds)
1467 i <- getIState
1468 -- simplify every definition do give the totality checker
1469 -- a better chance
1470 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1471 updateContext (simplifyCasedef n $ getErasureInfo i))
1472 (map snd (idris_totcheck i))
1473 -- build size change graph from simplified definitions
1474 iLOG "Totality checking"
1475 i <- getIState
1476 mapM_ buildSCG (idris_totcheck i)
1477 mapM_ checkDeclTotality (idris_totcheck i)
1479 -- Redo totality check for deferred names
1480 let deftots = idris_defertotcheck i
1481 iLOG $ "Totality checking " ++ show deftots
1482 mapM_ (\x -> do tot <- getTotality x
1483 case tot of
1484 Total _ -> setTotality x Unchecked
1485 _ -> return ()) (map snd deftots)
1486 mapM_ buildSCG deftots
1487 mapM_ checkDeclTotality deftots
1489 iLOG ("Finished " ++ f)
1490 ibcsd <- valIBCSubDir i
1491 iLOG "Universe checking"
1492 iucheck
1493 let ibc = ibcPathNoFallback ibcsd f
1494 i <- getIState
1495 addHides (hide_list i)
1497 -- Save module documentation if applicable
1498 i <- getIState
1499 case mdocs of
1500 Nothing -> return ()
1501 Just docs -> addModDoc syntax mname docs
1504 -- Finally, write an ibc if checking was successful
1505 ok <- noErrors
1506 when ok $
1507 idrisCatch (do writeIBC f ibc; clearIBC)
1508 (\c -> return ()) -- failure is harmless
1509 i <- getIState
1510 putIState (i { default_total = def_total,
1511 hide_list = [] })
1512 return ()
1513 where
1514 namespaces :: [String] -> [PDecl] -> [PDecl]
1515 namespaces [] ds = ds
1516 namespaces (x:xs) ds = [PNamespace x NoFC (namespaces xs ds)]
1518 toMutual :: PDecl -> PDecl
1519 toMutual m@(PMutual _ d) = m
1520 toMutual (PNamespace x fc ds) = PNamespace x fc (map toMutual ds)
1521 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1522 case x of
1523 PClauses{} -> r
1524 PClass{} -> r
1525 PData{} -> r
1526 PInstance{} -> r
1527 _ -> x
1529 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1530 addModDoc syn mname docs =
1531 do ist <- getIState
1532 docs' <- elabDocTerms recinfo (parsedDocs ist)
1533 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1534 putIState ist { idris_moduledocs = modDocs' }
1535 addIBC (IBCModDocs docName)
1536 where
1537 docName = NS modDocName (map T.pack (reverse mname))
1538 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1540{- | Adds names to hide list -}
1541addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1542addHides xs = do i <- getIState
1543 let defh = default_access i
1544 let (hs, as) = partition isNothing xs
1545 unless (null as) $
1546 mapM_ doHide
1547 (map (\ (n, _) -> (n, defh)) hs ++
1548 map (\ (n, Just a) -> (n, a)) as)
1549 where isNothing (_, Nothing) = True
1550 isNothing _ = False
1552 doHide (n, a) = do setAccessibility n a
1553 addIBC (IBCAccess n a)