git.iko.soy/Idris-dev
on 239c8ca help sign in
Idris-dev/src/Idris/Parser.hs
1601 lines 60 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.Foldable (asum)
66import Data.Generics.Uniplate.Data (descendM)
67import qualified Data.Map as M
68import qualified Data.HashSet as HS
69import qualified Data.Text as T
70import qualified Data.ByteString.UTF8 as UTF8
71import qualified Data.Set as S
73import Debug.Trace
75import System.FilePath
76import System.IO
78{-
80 grammar shortcut notation:
81 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)
82 RULE? = optional rule (i.e. RULE or nothing)
83 RULE* = repeated rule (i.e. RULE zero or more times)
84 RULE+ = repeated rule with at least one match (i.e. RULE one or more times)
85 RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)
86 RULE{n} = rule repeated n times
88-}
90{- * Main grammar -}
92{- | Parses module definition
95 ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;
97-}
98moduleHeader :: IdrisParser (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
99moduleHeader = try (do docs <- optional docComment
100 noArgs docs
101 reservedHL "module"
102 (i, ifc) <- identifier
103 option ';' (lchar ';')
104 let modName = moduleName i
105 return (fmap fst docs,
106 modName,
107 [(ifc, AnnNamespace (map T.pack modName) Nothing)]))
108 <|> try (do lchar '%'; reserved "unqualified"
109 return (Nothing, [], []))
110 <|> return (Nothing, moduleName "Main", [])
111 where moduleName x = case span (/='.') x of
112 (x, "") -> [x]
113 (x, '.':y) -> x : moduleName y
114 noArgs (Just (_, args)) | not (null args) = fail "Modules do not take arguments"
115 noArgs _ = return ()
117data ImportInfo = ImportInfo { import_reexport :: Bool
118 , import_path :: FilePath
119 , import_rename :: Maybe (String, FC)
120 , import_namespace :: [T.Text]
121 , import_location :: FC
122 , import_modname_location :: FC
123 }
125{- | Parses an import statement
128 Import ::= 'import' Identifier_t ';'?;
130 -}
131import_ :: IdrisParser ImportInfo
132import_ = do fc <- getFC
133 reservedHL "import"
134 reexport <- option False (do reservedHL "public"
135 return True)
136 (id, idfc) <- identifier
137 newName <- optional (do reservedHL "as"
138 identifier)
139 option ';' (lchar ';')
140 return $ ImportInfo reexport (toPath id)
141 (fmap (\(n, fc) -> (toPath n, fc)) newName)
142 (map T.pack $ ns id) fc idfc
143 <?> "import statement"
144 where ns = Spl.splitOn "."
145 toPath = foldl1' (</>) . ns
147{- | Parses program source
150 Prog ::= Decl* EOF;
152 -}
153prog :: SyntaxInfo -> IdrisParser [PDecl]
154prog syn = do whiteSpace
155 decls <- many (decl syn)
156 let c = (concat decls)
157 case maxline syn of
158 Nothing -> do notOpenBraces; eof
159 _ -> return ()
160 ist <- get
161 fc <- getFC
162 put ist { idris_parsedSpan = Just (FC (fc_fname fc) (0,0) (fc_end fc)),
163 ibc_write = IBCParsedRegion fc : ibc_write ist }
164 return c
166{-| Parses a top-level declaration
169Decl ::=
170 Decl'
171 | Using
172 | Params
173 | Mutual
174 | Namespace
175 | Class
176 | Instance
177 | DSL
178 | Directive
179 | Provider
180 | Transform
181 | Import!
182 ;
184-}
185decl :: SyntaxInfo -> IdrisParser [PDecl]
186decl syn = do fc <- getFC
187 -- if we're after maxline, stop here
188 let continue = case maxline syn of
189 Nothing -> True
190 Just l -> if fst (fc_end fc) > l
191 then mut_nesting syn /= 0
192 else True
193 if continue then do notEndBlock
194 declBody
195 else fail "End of readable input"
196 where declBody :: IdrisParser [PDecl]
197 declBody = declBody'
198 <|> using_ syn
199 <|> params syn
200 <|> mutual syn
201 <|> namespace syn
202 <|> class_ syn
203 <|> instance_ syn
204 <|> do d <- dsl syn; return [d]
205 <|> directive syn
206 <|> provider syn
207 <|> transform syn
208 <|> do import_; fail "imports must be at top of file"
209 <?> "declaration"
210 declBody' :: IdrisParser [PDecl]
211 declBody' = do d <- decl' syn
212 i <- get
213 let d' = fmap (debindApp syn . (desugar syn i)) d
214 return [d']
216{- | Parses a top-level declaration with possible syntax sugar
219Decl' ::=
220 Fixity
221 | FunDecl'
222 | Data
223 | Record
224 | SyntaxDecl
225 ;
227-}
228decl' :: SyntaxInfo -> IdrisParser PDecl
229decl' syn = fixity
230 <|> syntaxDecl syn
231 <|> fnDecl' syn
232 <|> data_ syn
233 <|> record syn
234 <?> "declaration"
236{- | Parses a syntax extension declaration (and adds the rule to parser state)
239 SyntaxDecl ::= SyntaxRule;
241-}
242syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
243syntaxDecl syn = do s <- syntaxRule syn
244 i <- get
245 put (i `addSyntax` s)
246 fc <- getFC
247 return (PSyntax fc s)
249-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.
250addSyntax :: IState -> Syntax -> IState
251addSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
252 syntax_keywords = ks ++ ns,
253 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc }
254 where rs = syntax_rules i
255 ns = syntax_keywords i
256 ibc = ibc_write i
257 ks = map show (syntaxNames s)
259-- | Like 'addSyntax', but no effect on the IBC.
260addReplSyntax :: IState -> Syntax -> IState
261addReplSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
262 syntax_keywords = ks ++ ns }
263 where rs = syntax_rules i
264 ns = syntax_keywords i
265 ks = map show (syntaxNames s)
267{- | Parses a syntax extension declaration
270SyntaxRuleOpts ::= 'term' | 'pattern';
274SyntaxRule ::=
275 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
279SyntaxSym ::= '[' Name_t ']'
280 | '{' Name_t '}'
281 | Name_t
282 | StringLiteral_t
283 ;
285-}
286syntaxRule :: SyntaxInfo -> IdrisParser Syntax
287syntaxRule syn
288 = do sty <- try (do
289 pushIndent
290 sty <- option AnySyntax
291 (do reservedHL "term"; return TermSyntax
292 <|> do reservedHL "pattern"; return PatternSyntax)
293 reservedHL "syntax"
294 return sty)
295 syms <- some syntaxSym
296 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
297 let ns = mapMaybe getName syms
298 when (length ns /= length (nub ns))
299 $ unexpected "repeated variable in syntax rule"
300 lchar '='
301 tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]
302 terminator
303 return (Rule (mkSimple syms) tm sty)
304 where
305 isExpr (Expr _) = True
306 isExpr _ = False
307 getName (Expr n) = Just n
308 getName _ = Nothing
309 -- Can't parse two full expressions (i.e. expressions with application) in a row
310 -- so change them both to a simple expression
311 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
312 mkSimple xs = mkSimple' xs
314 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
315 mkSimple es
316 -- Can't parse a full expression followed by operator like characters due to ambiguity
317 mkSimple' (Expr e : Symbol s : es)
318 | takeWhile (`elem` opChars) ts /= "" && ts `notElem` invalidOperators = SimpleExpr e : Symbol s : mkSimple' es
319 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s
320 mkSimple' (e : es) = e : mkSimple' es
321 mkSimple' [] = []
323 -- Prevent syntax variable capture by making all binders under syntax unique
324 -- (the ol' Common Lisp GENSYM approach)
325 uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
326 uniquifyBinders userNames = fixBind []
327 where
328 fixBind :: [(Name, Name)] -> PTerm -> IdrisParser PTerm
329 fixBind rens (PRef fc hls n) | Just n' <- lookup n rens =
330 return $ PRef fc hls n'
331 fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =
332 return $ PPatvar fc n'
333 fixBind rens (PLam fc n nfc ty body)
334 | n `elem` userNames = liftM2 (PLam fc n nfc) (fixBind rens ty) (fixBind rens body)
335 | otherwise =
336 do ty' <- fixBind rens ty
337 n' <- gensym n
338 body' <- fixBind ((n,n'):rens) body
339 return $ PLam fc n' nfc ty' body'
340 fixBind rens (PPi plic n nfc argTy body)
341 | n `elem` userNames = liftM2 (PPi plic n nfc) (fixBind rens argTy) (fixBind rens body)
342 | otherwise =
343 do ty' <- fixBind rens argTy
344 n' <- gensym n
345 body' <- fixBind ((n,n'):rens) body
346 return $ (PPi plic n' nfc ty' body')
347 fixBind rens (PLet fc n nfc ty val body)
348 | n `elem` userNames = liftM3 (PLet fc n nfc)
349 (fixBind rens ty)
350 (fixBind rens val)
351 (fixBind rens body)
352 | otherwise =
353 do ty' <- fixBind rens ty
354 val' <- fixBind rens val
355 n' <- gensym n
356 body' <- fixBind ((n,n'):rens) body
357 return $ PLet fc n' nfc ty' val' body'
358 fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =
359 return $ PMatchApp fc n'
360 fixBind rens x = descendM (fixBind rens) x
362 gensym :: Name -> IdrisParser Name
363 gensym n = do ist <- get
364 let idx = idris_name ist
365 put ist { idris_name = idx + 1 }
366 return $ sMN idx (show n)
368{- | Parses a syntax symbol (either binding variable, keyword or expression)
371SyntaxSym ::= '[' Name_t ']'
372 | '{' Name_t '}'
373 | Name_t
374 | StringLiteral_t
375 ;
377 -}
378syntaxSym :: IdrisParser SSymbol
379syntaxSym = try (do lchar '['; n <- fst <$> name; lchar ']'
380 return (Expr n))
381 <|> try (do lchar '{'; n <- fst <$> name; lchar '}'
382 return (Binding n))
383 <|> do n <- fst <$> iName []
384 return (Keyword n)
385 <|> do sym <- fmap fst stringLiteral
386 return (Symbol sym)
387 <?> "syntax symbol"
389{- | Parses a function declaration with possible syntax sugar
392 FunDecl ::= FunDecl';
394-}
395fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
396fnDecl syn = try (do notEndBlock
397 d <- fnDecl' syn
398 i <- get
399 let d' = fmap (desugar syn i) d
400 return [d']) <?> "function declaration"
402{-| Parses a function declaration
405 FunDecl' ::=
406 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
407 | Postulate
408 | Pattern
409 | CAF
410 ;
412-}
413fnDecl' :: SyntaxInfo -> IdrisParser PDecl
414fnDecl' syn = checkFixity $
415 do (doc, argDocs, fc, opts', n, nfc, acc) <- try (do
416 pushIndent
417 (doc, argDocs) <- docstring syn
418 ist <- get
419 let initOpts = if default_total ist
420 then [TotalFn]
421 else []
422 opts <- fnOpts initOpts
423 acc <- optional accessibility
424 opts' <- fnOpts opts
425 (n_in, nfc) <- fnName
426 let n = expandNS syn n_in
427 fc <- getFC
428 lchar ':'
429 return (doc, argDocs, fc, opts', n, nfc, acc))
430 ty <- typeExpr (allowImp syn)
431 terminator
432 addAcc n acc
433 return (PTy doc argDocs syn fc opts' n nfc ty)
434 <|> postulate syn
435 <|> caf syn
436 <|> pattern syn
437 <?> "function declaration"
438 where checkFixity :: IdrisParser PDecl -> IdrisParser PDecl
439 checkFixity p = do decl <- p
440 case getName decl of
441 Nothing -> return decl
442 Just n -> do fOk <- fixityOK n
443 unless fOk . fail $
444 "Missing fixity declaration for " ++ show n
445 return decl
446 getName (PTy _ _ _ _ _ n _ _) = Just n
447 getName _ = Nothing
448 fixityOK (NS n _) = fixityOK n
449 fixityOK (UN n) | all (flip elem opChars) (str n) =
450 do fixities <- fmap idris_infixes get
451 return . elem (str n) . map (\ (Fix _ op) -> op) $ fixities
452 | otherwise = return True
453 fixityOK _ = return True
455{-| Parses function options given initial options
458FnOpts ::= 'total'
459 | 'partial'
460 | 'covering'
461 | 'implicit'
462 | '%' 'no_implicit'
463 | '%' 'assert_total'
464 | '%' 'error_handler'
465 | '%' 'reflection'
466 | '%' 'specialise' '[' NameTimesList? ']'
467 ;
471NameTimes ::= FnName Natural?;
475NameTimesList ::=
476 NameTimes
477 | NameTimes ',' NameTimesList
478 ;
480-}
481-- FIXME: Check compatability for function options (i.e. partal/total)
482--
483-- Issue #1574 on the issue tracker.
484-- https://github.com/idris-lang/Idris-dev/issues/1574
485fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
486fnOpts opts
487 = do reservedHL "total"; fnOpts (TotalFn : opts)
488 <|> do reservedHL "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
489 <|> do reservedHL "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))
490 <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;
491 fnOpts (CExport c : opts)
492 <|> do try (lchar '%' *> reserved "no_implicit");
493 fnOpts (NoImplicit : opts)
494 <|> do try (lchar '%' *> reserved "inline");
495 fnOpts (Inlinable : opts)
496 <|> do try (lchar '%' *> reserved "assert_total");
497 fnOpts (AssertTotal : opts)
498 <|> do try (lchar '%' *> reserved "error_handler");
499 fnOpts (ErrorHandler : opts)
500 <|> do try (lchar '%' *> reserved "error_reverse");
501 fnOpts (ErrorReverse : opts)
502 <|> do try (lchar '%' *> reserved "reflection");
503 fnOpts (Reflection : opts)
504 <|> do try (lchar '%' *> reserved "hint");
505 fnOpts (AutoHint : opts)
506 <|> do lchar '%'; reserved "specialise";
507 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
508 fnOpts (Specialise ns : opts)
509 <|> do reservedHL "implicit"; fnOpts (Implicit : opts)
510 <|> return opts
511 <?> "function modifier"
512 where nameTimes :: IdrisParser (Name, Maybe Int)
513 nameTimes = do n <- fst <$> fnName
514 t <- option Nothing (do reds <- fmap fst natural
515 return (Just (fromInteger reds)))
516 return (n, t)
518{- | Parses a postulate
521Postulate ::=
522 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
523 ;
525-}
526postulate :: SyntaxInfo -> IdrisParser PDecl
527postulate syn = do (doc, ext)
528 <- try $ do (doc, _) <- docstring syn
529 pushIndent
530 ext <- ppostDecl
531 return (doc, ext)
532 ist <- get
533 let initOpts = if default_total ist
534 then [TotalFn]
535 else []
536 opts <- fnOpts initOpts
537 acc <- optional accessibility
538 opts' <- fnOpts opts
539 (n_in, nfc) <- fnName
540 let n = expandNS syn n_in
541 lchar ':'
542 ty <- typeExpr (allowImp syn)
543 fc <- getFC
544 terminator
545 addAcc n acc
546 return (PPostulate ext doc syn fc nfc opts' n ty)
547 <?> "postulate"
548 where ppostDecl = do fc <- reservedHL "postulate"; return False
549 <|> do lchar '%'; reserved "extern"; return True
550{- | Parses a using declaration
553Using ::=
554 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
555 ;
557 -}
558using_ :: SyntaxInfo -> IdrisParser [PDecl]
559using_ syn =
560 do reservedHL "using"
561 lchar '('; ns <- usingDeclList syn; lchar ')'
562 openBlock
563 let uvars = using syn
564 ds <- many (decl (syn { using = uvars ++ ns }))
565 closeBlock
566 return (concat ds)
567 <?> "using declaration"
569{- | Parses a parameters declaration
572Params ::=
573 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
574 ;
576 -}
577params :: SyntaxInfo -> IdrisParser [PDecl]
578params syn =
579 do reservedHL "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
580 let ns' = [(n, ty) | (n, _, ty) <- ns]
581 openBlock
582 let pvars = syn_params syn
583 ds <- many (decl syn { syn_params = pvars ++ ns' })
584 closeBlock
585 fc <- getFC
586 return [PParams fc ns' (concat ds)]
587 <?> "parameters declaration"
589{- | Parses a mutual declaration (for mutually recursive functions)
592Mutual ::=
593 'mutual' OpenBlock Decl* CloseBlock
594 ;
596-}
597mutual :: SyntaxInfo -> IdrisParser [PDecl]
598mutual syn =
599 do reservedHL "mutual"
600 openBlock
601 let pvars = syn_params syn
602 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
603 closeBlock
604 fc <- getFC
605 return [PMutual fc (concat ds)]
606 <?> "mutual block"
608{-| Parses a namespace declaration
611Namespace ::=
612 'namespace' identifier OpenBlock Decl+ CloseBlock
613 ;
615-}
616namespace :: SyntaxInfo -> IdrisParser [PDecl]
617namespace syn =
618 do reservedHL "namespace"
619 (n, nfc) <- identifier
620 openBlock
621 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
622 closeBlock
623 return [PNamespace n nfc (concat ds)]
624 <?> "namespace declaration"
626{- | Parses a methods block (for instances)
629 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
631-}
632instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
633instanceBlock syn = do reservedHL "where"
634 openBlock
635 ds <- many (fnDecl syn)
636 closeBlock
637 return (concat ds)
638 <?> "instance block"
640{- | Parses a methods and instances block (for type classes)
643MethodOrInstance ::=
644 FnDecl
645 | Instance
646 ;
650ClassBlock ::=
651 'where' OpenBlock Constructor? MethodOrInstance* CloseBlock
652 ;
654-}
655classBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])
656classBlock syn = do reservedHL "where"
657 openBlock
658 (cn, cd) <- option (Nothing, emptyDocstring) $
659 try (do (doc, _) <- option noDocs docComment
660 n <- constructor
661 return (Just n, doc))
662 ist <- get
663 let cd' = annotate syn ist cd
665 ds <- many (notEndBlock >> instance_ syn <|> fnDecl syn)
666 closeBlock
667 return (cn, cd', concat ds)
668 <?> "class block"
670 where
671 constructor :: IdrisParser (Name, FC)
672 constructor = reservedHL "constructor" *> fnName
674 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)
675 annotate syn ist = annotCode $ tryFullExpr syn ist
677{-| Parses a type class declaration
680ClassArgument ::=
681 Name
682 | '(' Name ':' Expr ')'
683 ;
687Class ::=
688 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
689 ;
691-}
692class_ :: SyntaxInfo -> IdrisParser [PDecl]
693class_ syn = do (doc, argDocs, acc)
694 <- try (do (doc, argDocs) <- docstring syn
695 acc <- optional accessibility
696 reservedHL "class"
697 return (doc, argDocs, acc))
698 fc <- getFC
699 cons <- constraintList syn
700 let cons' = [(c, ty) | (c, _, ty) <- cons]
701 (n_in, nfc) <- fnName
702 let n = expandNS syn n_in
703 cs <- many carg
704 fds <- option [(cn, NoFC) | (cn, _, _) <- cs] fundeps
705 (cn, cd, ds) <- option (Nothing, fst noDocs, []) (classBlock syn)
706 accData acc n (concatMap declared ds)
707 return [PClass doc syn fc cons' n nfc cs argDocs fds ds cn cd]
708 <?> "type-class declaration"
709 where
710 fundeps :: IdrisParser [(Name, FC)]
711 fundeps = do lchar '|'; sepBy name (lchar ',')
713 carg :: IdrisParser (Name, FC, PTerm)
714 carg = do lchar '('; (i, ifc) <- name; lchar ':'; ty <- expr syn; lchar ')'
715 return (i, ifc, ty)
716 <|> do (i, ifc) <- name
717 fc <- getFC
718 return (i, ifc, PType fc)
720{- | Parses a type class instance declaration
723 Instance ::=
724 DocComment_t? 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
725 ;
729InstanceName ::= '[' Name ']';
731-}
732instance_ :: SyntaxInfo -> IdrisParser [PDecl]
733instance_ syn = do (doc, argDocs)
734 <- try (docstring syn <* reservedHL "instance")
735 fc <- getFC
736 en <- optional instanceName
737 cs <- constraintList syn
738 let cs' = [(c, ty) | (c, _, ty) <- cs]
739 (cn, cnfc) <- fnName
740 args <- many (simpleExpr syn)
741 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)
742 let t = bindList (PPi constraint) cs sc
743 ds <- option [] (instanceBlock syn)
744 return [PInstance doc argDocs syn fc cs' cn cnfc args t en ds]
745 <?> "instance declaration"
746 where instanceName :: IdrisParser Name
747 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'
748 let n = expandNS syn n_in
749 return n
750 <?> "instance name"
753-- | Parse a docstring
754docstring :: SyntaxInfo
755 -> IdrisParser (Docstring (Either Err PTerm),
756 [(Name,Docstring (Either Err PTerm))])
757docstring syn = do (doc, argDocs) <- option noDocs docComment
758 ist <- get
759 let doc' = annotCode (tryFullExpr syn ist) doc
760 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
761 | (n, d) <- argDocs ]
762 return (doc', argDocs')
765{- | Parses a using declaration list
768UsingDeclList ::=
769 UsingDeclList'
770 | NameList TypeSig
771 ;
775UsingDeclList' ::=
776 UsingDecl
777 | UsingDecl ',' UsingDeclList'
778 ;
782NameList ::=
783 Name
784 | Name ',' NameList
785 ;
787-}
788usingDeclList :: SyntaxInfo -> IdrisParser [Using]
789usingDeclList syn
790 = try (sepBy1 (usingDecl syn) (lchar ','))
791 <|> do ns <- sepBy1 (fst <$> name) (lchar ',')
792 lchar ':'
793 t <- typeExpr (disallowImp syn)
794 return (map (\x -> UImplicit x t) ns)
795 <?> "using declaration list"
797{- |Parses a using declaration
800UsingDecl ::=
801 FnName TypeSig
802 | FnName FnName+
803 ;
805-}
806usingDecl :: SyntaxInfo -> IdrisParser Using
807usingDecl syn = try (do x <- fst <$> fnName
808 lchar ':'
809 t <- typeExpr (disallowImp syn)
810 return (UImplicit x t))
811 <|> do c <- fst <$> fnName
812 xs <- some (fst <$> fnName)
813 return (UConstraint c xs)
814 <?> "using declaration"
816{- | Parse a clause with patterns
819Pattern ::= Clause;
821-}
822pattern :: SyntaxInfo -> IdrisParser PDecl
823pattern syn = do fc <- getFC
824 clause <- clause syn
825 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
826 <?> "pattern"
828{- | Parse a constant applicative form declaration
831CAF ::= 'let' FnName '=' Expr Terminator;
833-}
834caf :: SyntaxInfo -> IdrisParser PDecl
835caf syn = do reservedHL "let"
836 n_in <- fst <$> fnName; let n = expandNS syn n_in
837 pushIndent
838 lchar '='
839 t <- indented $ expr syn
840 terminator
841 fc <- getFC
842 return (PCAF fc n t)
843 <?> "constant applicative form declaration"
845{- | Parse an argument expression
848ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
850-}
851argExpr :: SyntaxInfo -> IdrisParser PTerm
852argExpr syn = let syn' = syn { inPattern = True } in
853 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
854 <?> "argument expression"
856{- | Parse a right hand side of a function
859RHS ::= '=' Expr
860 | '?=' RHSName? Expr
861 | Impossible
862 ;
866RHSName ::= '{' FnName '}';
868-}
869rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
870rhs syn n = do lchar '='; expr syn
871 <|> do symbol "?=";
872 fc <- getFC
873 name <- option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";
874 return n)
875 r <- expr syn
876 return (addLet fc name r)
877 <|> impossible
878 <?> "function right hand side"
879 where mkN :: Name -> Name
880 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
881 then sUN "infix_op_lemma_1"
882 else sUN (str x++"_lemma_1")
883 mkN (NS x n) = NS (mkN x) n
884 n' :: Name
885 n' = mkN n
886 addLet :: FC -> Name -> PTerm -> PTerm
887 addLet fc nm (PLet fc' n nfc ty val r) = PLet fc' n nfc ty val (addLet fc nm r)
888 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
889 where addLetC (l, r) = (l, addLet fc nm r)
890 addLet fc nm r = (PLet fc (sUN "value") NoFC Placeholder r (PMetavar NoFC nm))
892{- |Parses a function clause
895RHSOrWithBlock ::= RHS WhereOrTerminator
896 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
897 ;
901Clause ::= WExpr+ RHSOrWithBlock
902 | SimpleExpr '<==' FnName RHS WhereOrTerminator
903 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
904 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
905 ;
909ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
913WhereOrTerminator ::= WhereBlock | Terminator;
915-}
916clause :: SyntaxInfo -> IdrisParser PClause
917clause syn
918 = do wargs <- try (do pushIndent; some (wExpr syn))
919 fc <- getFC
920 ist <- get
921 n <- case lastParse ist of
922 Just t -> return t
923 Nothing -> fail "Invalid clause"
924 (do r <- rhs syn n
925 let ctxt = tt_ctxt ist
926 let wsyn = syn { syn_namespace = [] }
927 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
928 popIndent
929 return x,
930 do terminator
931 return ([], [])]
932 return $ PClauseR fc wargs r wheres) <|> (do
933 popIndent
934 reservedHL "with"
935 wval <- simpleExpr syn
936 pn <- optProof
937 openBlock
938 ds <- some $ fnDecl syn
939 let withs = concat ds
940 closeBlock
941 return $ PWithR fc wargs wval pn withs)
942 <|> do ty <- try (do pushIndent
943 ty <- simpleExpr syn
944 symbol "<=="
945 return ty)
946 fc <- getFC
947 n_in <- fst <$> fnName; let n = expandNS syn n_in
948 r <- rhs syn n
949 ist <- get
950 let ctxt = tt_ctxt ist
951 let wsyn = syn { syn_namespace = [] }
952 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
953 popIndent
954 return x,
955 do terminator
956 return ([], [])]
957 let capp = PLet fc (sMN 0 "match") NoFC
958 ty
959 (PMatchApp fc n)
960 (PRef fc [] (sMN 0 "match"))
961 ist <- get
962 put (ist { lastParse = Just n })
963 return $ PClause fc n capp [] r wheres
964 <|> do (l, op, nfc) <- try (do
965 pushIndent
966 l <- argExpr syn
967 (op, nfc) <- operatorFC
968 when (op == "=" || op == "?=" ) $
969 fail "infix clause definition with \"=\" and \"?=\" not supported "
970 return (l, op, nfc))
971 let n = expandNS syn (sUN op)
972 r <- argExpr syn
973 fc <- getFC
974 wargs <- many (wExpr syn)
975 (do rs <- rhs syn n
976 let wsyn = syn { syn_namespace = [] }
977 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
978 popIndent
979 return x,
980 do terminator
981 return ([], [])]
982 ist <- get
983 let capp = PApp fc (PRef nfc [nfc] n) [pexp l, pexp r]
984 put (ist { lastParse = Just n })
985 return $ PClause fc n capp wargs rs wheres) <|> (do
986 popIndent
987 reservedHL "with"
988 wval <- bracketed syn
989 pn <- optProof
990 openBlock
991 ds <- some $ fnDecl syn
992 closeBlock
993 ist <- get
994 let capp = PApp fc (PRef fc [] n) [pexp l, pexp r]
995 let withs = map (fillLHSD n capp wargs) $ concat ds
996 put (ist { lastParse = Just n })
997 return $ PWith fc n capp wargs wval pn withs)
998 <|> do pushIndent
999 (n_in, nfc) <- fnName; let n = expandNS syn n_in
1000 cargs <- many (constraintArg syn)
1001 fc <- getFC
1002 args <- many (try (implicitArg (syn { inPattern = True } ))
1003 <|> (fmap pexp (argExpr syn)))
1004 wargs <- many (wExpr syn)
1005 let capp = PApp fc (PRef nfc [nfc] n)
1006 (cargs ++ args)
1007 (do r <- rhs syn n
1008 ist <- get
1009 let ctxt = tt_ctxt ist
1010 let wsyn = syn { syn_namespace = [] }
1011 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1012 popIndent
1013 return x,
1014 do terminator
1015 return ([], [])]
1016 ist <- get
1017 put (ist { lastParse = Just n })
1018 return $ PClause fc n capp wargs r wheres) <|> (do
1019 reservedHL "with"
1020 ist <- get
1021 put (ist { lastParse = Just n })
1022 wval <- bracketed syn
1023 pn <- optProof
1024 openBlock
1025 ds <- some $ fnDecl syn
1026 let withs = map (fillLHSD n capp wargs) $ concat ds
1027 closeBlock
1028 popIndent
1029 return $ PWith fc n capp wargs wval pn withs)
1030 <?> "function clause"
1031 where
1032 optProof = option Nothing (do reservedHL "proof"
1033 n <- fnName
1034 return (Just n))
1036 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
1037 fillLHS n capp owargs (PClauseR fc wargs v ws)
1038 = PClause fc n capp (owargs ++ wargs) v ws
1039 fillLHS n capp owargs (PWithR fc wargs v pn ws)
1040 = PWith fc n capp (owargs ++ wargs) v pn
1041 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1042 fillLHS _ _ _ c = c
1044 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
1045 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1046 fillLHSD n c a x = x
1048{-| Parses with pattern
1051WExpr ::= '|' Expr';
1054wExpr :: SyntaxInfo -> IdrisParser PTerm
1055wExpr syn = do lchar '|'
1056 expr' (syn { inPattern = True })
1057 <?> "with pattern"
1059{- | Parses a where block
1062WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
1065whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
1066whereBlock n syn
1067 = do reservedHL "where"
1068 ds <- indentedBlock1 (decl syn)
1069 let dns = concatMap (concatMap declared) ds
1070 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1071 <?> "where block"
1073{- |Parses a code generation target language name
1076Codegen ::= 'C'
1077 | 'Java'
1078 | 'JavaScript'
1079 | 'Node'
1080 | 'LLVM'
1081 | 'Bytecode'
1085codegen_ :: IdrisParser Codegen
1086codegen_ = do n <- fst <$> identifier
1087 return (Via (map toLower n))
1088 <|> do reserved "Bytecode"; return Bytecode
1089 <?> "code generation language"
1091{- |Parses a compiler directive
1093StringList ::=
1094 String
1095 | String ',' StringList
1100Directive ::= '%' Directive';
1104Directive' ::= 'lib' CodeGen String_t
1105 | 'link' CodeGen String_t
1106 | 'flag' CodeGen String_t
1107 | 'include' CodeGen String_t
1108 | 'hide' Name
1109 | 'freeze' Name
1110 | 'access' Accessibility
1111 | 'default' Totality
1112 | 'logging' Natural
1113 | 'dynamic' StringList
1114 | 'name' Name NameList
1115 | 'error_handlers' Name NameList
1116 | 'language' 'TypeProviders'
1117 | 'language' 'ErrorReflection'
1121directive :: SyntaxInfo -> IdrisParser [PDecl]
1122directive syn = do try (lchar '%' *> reserved "lib")
1123 cgn <- codegen_
1124 lib <- fmap fst stringLiteral
1125 return [PDirective (DLib cgn lib)]
1126 <|> do try (lchar '%' *> reserved "link")
1127 cgn <- codegen_; obj <- fst <$> stringLiteral
1128 return [PDirective (DLink cgn obj)]
1129 <|> do try (lchar '%' *> reserved "flag")
1130 cgn <- codegen_; flag <- fst <$> stringLiteral
1131 return [PDirective (DFlag cgn flag)]
1132 <|> do try (lchar '%' *> reserved "include")
1133 cgn <- codegen_
1134 hdr <- fst <$> stringLiteral
1135 return [PDirective (DInclude cgn hdr)]
1136 <|> do try (lchar '%' *> reserved "hide"); n <- fst <$> fnName
1137 return [PDirective (DHide n)]
1138 <|> do try (lchar '%' *> reserved "freeze"); n <- fst <$> iName []
1139 return [PDirective (DFreeze n)]
1140 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1141 return [PDirective (DAccess acc)]
1142 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1143 i <- get
1144 put (i { default_total = tot } )
1145 return [PDirective (DDefault tot)]
1146 <|> do try (lchar '%' *> reserved "logging")
1147 i <- fst <$> natural
1148 return [PDirective (DLogging i)]
1149 <|> do try (lchar '%' *> reserved "dynamic")
1150 libs <- sepBy1 (fmap fst stringLiteral) (lchar ',')
1151 return [PDirective (DDynamicLibs libs)]
1152 <|> do try (lchar '%' *> reserved "name")
1153 (ty, tyFC) <- fnName
1154 ns <- sepBy1 name (lchar ',')
1155 return [PDirective (DNameHint ty tyFC ns)]
1156 <|> do try (lchar '%' *> reserved "error_handlers")
1157 (fn, nfc) <- fnName
1158 (arg, afc) <- fnName
1159 ns <- sepBy1 name (lchar ',')
1160 return [PDirective (DErrorHandlers fn nfc arg afc ns) ]
1161 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1162 return [PDirective (DLanguage ext)]
1163 <|> do fc <- getFC
1164 try (lchar '%' *> reserved "used")
1165 fn <- fst <$> fnName
1166 arg <- fst <$> iName []
1167 return [PDirective (DUsed fc fn arg)]
1168 <?> "directive"
1170pLangExt :: IdrisParser LanguageExt
1171pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1172 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1174{- | Parses a totality
1177Totality ::= 'partial' | 'total'
1181totality :: IdrisParser Bool
1182totality
1183 = do reservedHL "total"; return True
1184 <|> do reservedHL "partial"; return False
1186{- | Parses a type provider
1189Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1190ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1192 -}
1193provider :: SyntaxInfo -> IdrisParser [PDecl]
1194provider syn = do doc <- try (do (doc, _) <- docstring syn
1195 fc1 <- getFC
1196 lchar '%'
1197 fc2 <- reservedFC "provide"
1198 highlightP (spanFC fc1 fc2) AnnKeyword
1199 return doc)
1200 provideTerm doc <|> providePostulate doc
1201 <?> "type provider"
1202 where provideTerm doc =
1203 do lchar '('; (n, nfc) <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1204 fc <- getFC
1205 reservedHL "with"
1206 e <- expr syn <?> "provider expression"
1207 return [PProvider doc syn fc nfc (ProvTerm t e) n]
1208 providePostulate doc =
1209 do reservedHL "postulate"
1210 (n, nfc) <- fnName
1211 fc <- getFC
1212 reservedHL "with"
1213 e <- expr syn <?> "provider expression"
1214 return [PProvider doc syn fc nfc (ProvPostulate e) n]
1216{- | Parses a transform
1219Transform ::= '%' 'transform' Expr '==>' Expr
1222transform :: SyntaxInfo -> IdrisParser [PDecl]
1223transform syn = do try (lchar '%' *> reserved "transform")
1224 -- leave it unchecked, until we work out what this should
1225 -- actually mean...
1226-- safety <- option True (do reserved "unsafe"
1227-- return False)
1228 l <- expr syn
1229 fc <- getFC
1230 symbol "==>"
1231 r <- expr syn
1232 return [PTransform fc False l r]
1233 <?> "transform"
1236{- * Loading and parsing -}
1237{- | Parses an expression from input -}
1238parseExpr :: IState -> String -> Result PTerm
1239parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1241{- | Parses a constant form input -}
1242parseConst :: IState -> String -> Result Const
1243parseConst st = runparser (fmap fst constant) st "(input)"
1245{- | Parses a tactic from input -}
1246parseTactic :: IState -> String -> Result PTactic
1247parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1249{- | Parses a do-step from input (used in the elab shell) -}
1250parseElabShellStep :: IState -> String -> Result (Either ElabShellCmd PDo)
1251parseElabShellStep ist = runparser (fmap Right (do_ defaultSyntax) <|> fmap Left elabShellCmd) ist "(input)"
1252 where elabShellCmd = char ':' >>
1253 (reserved "qed" >> pure EQED ) <|>
1254 (reserved "abandon" >> pure EAbandon ) <|>
1255 (reserved "undo" >> pure EUndo ) <|>
1256 (reserved "state" >> pure EProofState) <|>
1257 (reserved "term" >> pure EProofTerm ) <|>
1258 (expressionTactic ["e", "eval"] EEval ) <|>
1259 (expressionTactic ["t", "type"] ECheck) <|>
1260 (expressionTactic ["search"] ESearch ) <|>
1261 (do reserved "doc"
1262 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)
1263 eof
1264 return (EDocStr doc))
1265 <?> "elab command"
1266 expressionTactic cmds tactic =
1267 do asum (map reserved cmds)
1268 t <- spaced (expr defaultSyntax)
1269 i <- get
1270 return $ tactic (desugar defaultSyntax i t)
1271 spaced parser = indentPropHolds gtProp *> parser
1273-- | Parse module header and imports
1274parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Delta)
1275parseImports fname input
1276 = do i <- getIState
1277 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1278 Failure err -> fail (show err)
1279 Success (x, annots, i) ->
1280 do putIState i
1281 fname' <- runIO $ Dir.makeAbsolute fname
1282 sendHighlighting $ addPath annots fname'
1283 return x
1284 where imports :: IdrisParser ((Maybe (Docstring ()), [String],
1285 [ImportInfo],
1286 Maybe Delta),
1287 [(FC, OutputAnnotation)], IState)
1288 imports = do whiteSpace
1289 (mdoc, mname, annots) <- moduleHeader
1290 ps <- many import_
1291 mrk <- mark
1292 isEof <- lookAheadMatches eof
1293 let mrk' = if isEof
1294 then Nothing
1295 else Just mrk
1296 i <- get
1297 return ((mdoc, mname, ps, mrk'), annots, i)
1298 addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]
1299 addPath [] _ = []
1300 addPath ((fc, AnnNamespace ns Nothing) : annots) path =
1301 (fc, AnnNamespace ns (Just path)) : addPath annots path
1302 addPath (annot:annots) path = annot : addPath annots path
1304-- | There should be a better way of doing this...
1305findFC :: Doc -> (FC, String)
1306findFC x = let s = show (plain x) in findFC' s
1307 where findFC' s = case span (/= ':') s of
1308 -- Horrid kludge to prevent crashes on Windows
1309 (prefix, ':':'\\':rest) ->
1310 case findFC' rest of
1311 (NoFC, msg) -> (NoFC, msg)
1312 (FileFC f, msg) -> (FileFC (prefix ++ ":\\" ++ f), msg)
1313 (FC f start end, msg) -> (FC (prefix ++ ":\\" ++ f) start end, msg)
1314 (failname, ':':rest) -> case span isDigit rest of
1315 (line, ':':rest') -> case span isDigit rest' of
1316 (col, ':':msg) -> let pos = (read line, read col) in
1317 (FC failname pos pos, msg)
1319-- | Check if the coloring matches the options and corrects if necessary
1320fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1321fixColour False doc = ANSI.plain doc
1322fixColour True doc = doc
1324-- | A program is a list of declarations, possibly with associated
1325-- documentation strings.
1326parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1327 Idris [PDecl]
1328parseProg syn fname input mrk
1329 = do i <- getIState
1330 case runparser mainProg i fname input of
1331 Failure doc -> do -- FIXME: Get error location from trifecta
1332 -- this can't be the solution!
1333 -- Issue #1575 on the issue tracker.
1334 -- https://github.com/idris-lang/Idris-dev/issues/1575
1335 let (fc, msg) = findFC doc
1336 i <- getIState
1337 case idris_outputmode i of
1338 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1339 IdeMode n h -> iWarn fc (P.text msg)
1340 putIState (i { errSpan = Just fc })
1341 return []
1342 Success (x, i) -> do putIState i
1343 reportParserWarnings
1344 return $ collect x
1345 where mainProg :: IdrisParser ([PDecl], IState)
1346 mainProg = case mrk of
1347 Nothing -> do i <- get; return ([], i)
1348 Just mrk -> do
1349 release mrk
1350 ds <- prog syn
1351 i' <- get
1352 return (ds, i')
1354{- | Load idris module and show error if something wrong happens -}
1355loadModule :: FilePath -> Idris (Maybe String)
1356loadModule f
1357 = idrisCatch (loadModule' f)
1358 (\e -> do setErrSpan (getErrSpan e)
1359 ist <- getIState
1360 iWarn (getErrSpan e) $ pprintErr ist e
1361 return Nothing)
1363{- | Load idris module -}
1364loadModule' :: FilePath -> Idris (Maybe String)
1365loadModule' f
1366 = do i <- getIState
1367 let file = takeWhile (/= ' ') f
1368 ibcsd <- valIBCSubDir i
1369 ids <- allImportDirs
1370 fp <- findImport ids ibcsd file
1371 if file `elem` imported i
1372 then do logLvl 1 $ "Already read " ++ file
1373 return Nothing
1374 else do putIState (i { imported = file : imported i })
1375 case fp of
1376 IDR fn -> loadSource False fn Nothing
1377 LIDR fn -> loadSource True fn Nothing
1378 IBC fn src ->
1379 idrisCatch (loadIBC True fn)
1380 (\c -> do logLvl 1 $ fn ++ " failed " ++ pshow i c
1381 case src of
1382 IDR sfn -> loadSource False sfn Nothing
1383 LIDR sfn -> loadSource True sfn Nothing)
1384 return $ Just file
1386{- | Load idris code from file -}
1387loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()
1388loadFromIFile reexp i@(IBC fn src) maxline
1389 = do logLvl 1 $ "Skipping " ++ getSrcFile i
1390 idrisCatch (loadIBC reexp fn)
1391 (\err -> ierror $ LoadingFailed fn err)
1392 where
1393 getSrcFile (IDR fn) = fn
1394 getSrcFile (LIDR fn) = fn
1395 getSrcFile (IBC f src) = getSrcFile src
1397loadFromIFile _ (IDR fn) maxline = loadSource' False fn maxline
1398loadFromIFile _ (LIDR fn) maxline = loadSource' True fn maxline
1400{-| Load idris source code and show error if something wrong happens -}
1401loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1402loadSource' lidr r maxline
1403 = idrisCatch (loadSource lidr r maxline)
1404 (\e -> do setErrSpan (getErrSpan e)
1405 ist <- getIState
1406 case e of
1407 At f e' -> iWarn f (pprintErr ist e')
1408 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1410{- | Load Idris source code-}
1411loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1412loadSource lidr f toline
1413 = do logLvl 1 ("Reading " ++ f)
1414 i <- getIState
1415 let def_total = default_total i
1416 file_in <- runIO $ readSource f
1417 file <- if lidr then tclift $ unlit f file_in else return file_in
1418 (mdocs, mname, imports_in, pos) <- parseImports f file
1419 ai <- getAutoImports
1420 let imports = map (\n -> ImportInfo True n Nothing [] NoFC NoFC) ai ++ imports_in
1421 ids <- allImportDirs
1422 ibcsd <- valIBCSubDir i
1423 mapM_ (\(re, f, ns, nfc) ->
1424 do fp <- findImport ids ibcsd f
1425 case fp of
1426 LIDR fn -> ifail $ "No ibc for " ++ f
1427 IDR fn -> ifail $ "No ibc for " ++ f
1428 IBC fn src ->
1429 do loadIBC True fn
1430 let srcFn = case src of
1431 IDR fn -> Just fn
1432 LIDR fn -> Just fn
1433 _ -> Nothing
1434 srcFnAbs <- case srcFn of
1435 Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)
1436 Nothing -> return Nothing
1437 sendHighlighting [(nfc, AnnNamespace ns srcFnAbs)])
1438 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]
1439 reportParserWarnings
1440 sendParserHighlighting
1442 -- process and check module aliases
1443 let modAliases = M.fromList
1444 [ (prep alias, prep realName)
1445 | ImportInfo { import_reexport = reexport
1446 , import_path = realName
1447 , import_rename = Just (alias, _)
1448 , import_location = fc } <- imports
1450 prep = map T.pack . reverse . Spl.splitOn [pathSeparator]
1451 aliasNames = [ (alias, fc)
1452 | ImportInfo { import_rename = Just (alias, _)
1453 , import_location = fc } <- imports
1455 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1456 case map head . filter ((/= 1) . length) $ histogram of
1457 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1458 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1460 i <- getIState
1461 putIState (i { default_access = Hidden, module_aliases = modAliases })
1462 clearIBC -- start a new .ibc file
1463 -- record package info in .ibc
1464 imps <- allImportDirs
1465 mapM_ addIBC (map IBCImportDir imps)
1466 mapM_ (addIBC . IBCImport)
1467 [ (reexport, realName)
1468 | ImportInfo { import_reexport = reexport
1469 , import_path = realName
1470 } <- imports
1472 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1473 maxline = toline }
1474 ist <- getIState
1475 -- Save the span from parsing the module header, because
1476 -- an empty program parse might obliterate it.
1477 let oldSpan = idris_parsedSpan ist
1478 ds' <- parseProg syntax f file pos
1480 case (ds', oldSpan) of
1481 ([], Just fc) ->
1482 -- If no program elements were parsed, we dind't
1483 -- get a loaded region in the IBC file. That
1484 -- means we need to add it back.
1485 do ist <- getIState
1486 putIState ist { idris_parsedSpan = oldSpan
1487 , ibc_write = IBCParsedRegion fc :
1488 ibc_write ist
1490 _ -> return ()
1491 sendParserHighlighting
1493 -- Parsing done, now process declarations
1495 let ds = namespaces mname ds'
1496 logLvl 3 (show $ showDecls verbosePPOption ds)
1497 i <- getIState
1498 logLvl 10 (show (toAlist (idris_implicits i)))
1499 logLvl 3 (show (idris_infixes i))
1500 -- Now add all the declarations to the context
1501 v <- verbose
1502 when v $ iputStrLn $ "Type checking " ++ f
1503 -- we totality check after every Mutual block, so if
1504 -- anything is a single definition, wrap it in a
1505 -- mutual block on its own
1506 elabDecls toplevel (map toMutual ds)
1507 i <- getIState
1508 -- simplify every definition do give the totality checker
1509 -- a better chance
1510 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1511 ctxt' <-
1512 do ctxt <- getContext
1513 tclift $ simplifyCasedef n (getErasureInfo i) ctxt
1514 setContext ctxt')
1515 (map snd (idris_totcheck i))
1516 -- build size change graph from simplified definitions
1517 logLvl 1 "Totality checking"
1518 i <- getIState
1519 mapM_ buildSCG (idris_totcheck i)
1520 mapM_ checkDeclTotality (idris_totcheck i)
1522 -- Redo totality check for deferred names
1523 let deftots = idris_defertotcheck i
1524 logLvl 1 $ "Totality checking " ++ show deftots
1525 mapM_ (\x -> do tot <- getTotality x
1526 case tot of
1527 Total _ -> setTotality x Unchecked
1528 _ -> return ()) (map snd deftots)
1529 mapM_ buildSCG deftots
1530 mapM_ checkDeclTotality deftots
1532 logLvl 1 ("Finished " ++ f)
1533 ibcsd <- valIBCSubDir i
1534 logLvl 1 "Universe checking"
1535 iucheck
1536 let ibc = ibcPathNoFallback ibcsd f
1537 i <- getIState
1538 addHides (hide_list i)
1540 -- Save module documentation if applicable
1541 i <- getIState
1542 case mdocs of
1543 Nothing -> return ()
1544 Just docs -> addModDoc syntax mname docs
1547 -- Finally, write an ibc and highlights if checking was successful
1548 ok <- noErrors
1549 when ok $
1550 do idrisCatch (do writeIBC f ibc; clearIBC)
1551 (\c -> return ()) -- failure is harmless
1552 hl <- getDumpHighlighting
1553 when hl $
1554 idrisCatch (writeHighlights f)
1555 (const $ return ()) -- failure is harmless
1556 clearHighlights
1557 i <- getIState
1558 putIState (i { default_total = def_total,
1559 hide_list = [] })
1560 return ()
1561 where
1562 namespaces :: [String] -> [PDecl] -> [PDecl]
1563 namespaces [] ds = ds
1564 namespaces (x:xs) ds = [PNamespace x NoFC (namespaces xs ds)]
1566 toMutual :: PDecl -> PDecl
1567 toMutual m@(PMutual _ d) = m
1568 toMutual (PNamespace x fc ds) = PNamespace x fc (map toMutual ds)
1569 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1570 case x of
1571 PClauses{} -> r
1572 PClass{} -> r
1573 PData{} -> r
1574 PInstance{} -> r
1575 _ -> x
1577 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1578 addModDoc syn mname docs =
1579 do ist <- getIState
1580 docs' <- elabDocTerms recinfo (parsedDocs ist)
1581 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1582 putIState ist { idris_moduledocs = modDocs' }
1583 addIBC (IBCModDocs docName)
1584 where
1585 docName = NS modDocName (map T.pack (reverse mname))
1586 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1588{- | Adds names to hide list -}
1589addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1590addHides xs = do i <- getIState
1591 let defh = default_access i
1592 let (hs, as) = partition isNothing xs
1593 unless (null as) $
1594 mapM_ doHide
1595 (map (\ (n, _) -> (n, defh)) hs ++
1596 map (\ (n, Just a) -> (n, a)) as)
1597 where isNothing (_, Nothing) = True
1598 isNothing _ = False
1600 doHide (n, a) = do setAccessibility n a
1601 addIBC (IBCAccess n a)