git.iko.soy/Idris-dev
on 54e4e41 help sign in
Idris-dev/src/Idris/Parser.hs
1600 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 lchar '='
838 t <- expr syn
839 terminator
840 fc <- getFC
841 return (PCAF fc n t)
842 <?> "constant applicative form declaration"
844{- | Parse an argument expression
847ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
849-}
850argExpr :: SyntaxInfo -> IdrisParser PTerm
851argExpr syn = let syn' = syn { inPattern = True } in
852 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
853 <?> "argument expression"
855{- | Parse a right hand side of a function
858RHS ::= '=' Expr
859 | '?=' RHSName? Expr
860 | Impossible
861 ;
865RHSName ::= '{' FnName '}';
867-}
868rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
869rhs syn n = do lchar '='; expr syn
870 <|> do symbol "?=";
871 fc <- getFC
872 name <- option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";
873 return n)
874 r <- expr syn
875 return (addLet fc name r)
876 <|> impossible
877 <?> "function right hand side"
878 where mkN :: Name -> Name
879 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
880 then sUN "infix_op_lemma_1"
881 else sUN (str x++"_lemma_1")
882 mkN (NS x n) = NS (mkN x) n
883 n' :: Name
884 n' = mkN n
885 addLet :: FC -> Name -> PTerm -> PTerm
886 addLet fc nm (PLet fc' n nfc ty val r) = PLet fc' n nfc ty val (addLet fc nm r)
887 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
888 where addLetC (l, r) = (l, addLet fc nm r)
889 addLet fc nm r = (PLet fc (sUN "value") NoFC Placeholder r (PMetavar NoFC nm))
891{- |Parses a function clause
894RHSOrWithBlock ::= RHS WhereOrTerminator
895 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
896 ;
900Clause ::= WExpr+ RHSOrWithBlock
901 | SimpleExpr '<==' FnName RHS WhereOrTerminator
902 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
903 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
904 ;
908ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
912WhereOrTerminator ::= WhereBlock | Terminator;
914-}
915clause :: SyntaxInfo -> IdrisParser PClause
916clause syn
917 = do wargs <- try (do pushIndent; some (wExpr syn))
918 fc <- getFC
919 ist <- get
920 n <- case lastParse ist of
921 Just t -> return t
922 Nothing -> fail "Invalid clause"
923 (do r <- rhs syn n
924 let ctxt = tt_ctxt ist
925 let wsyn = syn { syn_namespace = [] }
926 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
927 popIndent
928 return x,
929 do terminator
930 return ([], [])]
931 return $ PClauseR fc wargs r wheres) <|> (do
932 popIndent
933 reservedHL "with"
934 wval <- simpleExpr syn
935 pn <- optProof
936 openBlock
937 ds <- some $ fnDecl syn
938 let withs = concat ds
939 closeBlock
940 return $ PWithR fc wargs wval pn withs)
941 <|> do ty <- try (do pushIndent
942 ty <- simpleExpr syn
943 symbol "<=="
944 return ty)
945 fc <- getFC
946 n_in <- fst <$> fnName; let n = expandNS syn n_in
947 r <- rhs syn n
948 ist <- get
949 let ctxt = tt_ctxt ist
950 let wsyn = syn { syn_namespace = [] }
951 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
952 popIndent
953 return x,
954 do terminator
955 return ([], [])]
956 let capp = PLet fc (sMN 0 "match") NoFC
957 ty
958 (PMatchApp fc n)
959 (PRef fc [] (sMN 0 "match"))
960 ist <- get
961 put (ist { lastParse = Just n })
962 return $ PClause fc n capp [] r wheres
963 <|> do (l, op, nfc) <- try (do
964 pushIndent
965 l <- argExpr syn
966 (op, nfc) <- operatorFC
967 when (op == "=" || op == "?=" ) $
968 fail "infix clause definition with \"=\" and \"?=\" not supported "
969 return (l, op, nfc))
970 let n = expandNS syn (sUN op)
971 r <- argExpr syn
972 fc <- getFC
973 wargs <- many (wExpr syn)
974 (do rs <- rhs syn n
975 let wsyn = syn { syn_namespace = [] }
976 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
977 popIndent
978 return x,
979 do terminator
980 return ([], [])]
981 ist <- get
982 let capp = PApp fc (PRef nfc [nfc] n) [pexp l, pexp r]
983 put (ist { lastParse = Just n })
984 return $ PClause fc n capp wargs rs wheres) <|> (do
985 popIndent
986 reservedHL "with"
987 wval <- bracketed syn
988 pn <- optProof
989 openBlock
990 ds <- some $ fnDecl syn
991 closeBlock
992 ist <- get
993 let capp = PApp fc (PRef fc [] n) [pexp l, pexp r]
994 let withs = map (fillLHSD n capp wargs) $ concat ds
995 put (ist { lastParse = Just n })
996 return $ PWith fc n capp wargs wval pn withs)
997 <|> do pushIndent
998 (n_in, nfc) <- fnName; let n = expandNS syn n_in
999 cargs <- many (constraintArg syn)
1000 fc <- getFC
1001 args <- many (try (implicitArg (syn { inPattern = True } ))
1002 <|> (fmap pexp (argExpr syn)))
1003 wargs <- many (wExpr syn)
1004 let capp = PApp fc (PRef nfc [nfc] n)
1005 (cargs ++ args)
1006 (do r <- rhs syn n
1007 ist <- get
1008 let ctxt = tt_ctxt ist
1009 let wsyn = syn { syn_namespace = [] }
1010 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1011 popIndent
1012 return x,
1013 do terminator
1014 return ([], [])]
1015 ist <- get
1016 put (ist { lastParse = Just n })
1017 return $ PClause fc n capp wargs r wheres) <|> (do
1018 reservedHL "with"
1019 ist <- get
1020 put (ist { lastParse = Just n })
1021 wval <- bracketed syn
1022 pn <- optProof
1023 openBlock
1024 ds <- some $ fnDecl syn
1025 let withs = map (fillLHSD n capp wargs) $ concat ds
1026 closeBlock
1027 popIndent
1028 return $ PWith fc n capp wargs wval pn withs)
1029 <?> "function clause"
1030 where
1031 optProof = option Nothing (do reservedHL "proof"
1032 n <- fnName
1033 return (Just n))
1035 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
1036 fillLHS n capp owargs (PClauseR fc wargs v ws)
1037 = PClause fc n capp (owargs ++ wargs) v ws
1038 fillLHS n capp owargs (PWithR fc wargs v pn ws)
1039 = PWith fc n capp (owargs ++ wargs) v pn
1040 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1041 fillLHS _ _ _ c = c
1043 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
1044 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1045 fillLHSD n c a x = x
1047{-| Parses with pattern
1050WExpr ::= '|' Expr';
1053wExpr :: SyntaxInfo -> IdrisParser PTerm
1054wExpr syn = do lchar '|'
1055 expr' (syn { inPattern = True })
1056 <?> "with pattern"
1058{- | Parses a where block
1061WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
1064whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
1065whereBlock n syn
1066 = do reservedHL "where"
1067 ds <- indentedBlock1 (decl syn)
1068 let dns = concatMap (concatMap declared) ds
1069 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1070 <?> "where block"
1072{- |Parses a code generation target language name
1075Codegen ::= 'C'
1076 | 'Java'
1077 | 'JavaScript'
1078 | 'Node'
1079 | 'LLVM'
1080 | 'Bytecode'
1084codegen_ :: IdrisParser Codegen
1085codegen_ = do n <- fst <$> identifier
1086 return (Via (map toLower n))
1087 <|> do reserved "Bytecode"; return Bytecode
1088 <?> "code generation language"
1090{- |Parses a compiler directive
1092StringList ::=
1093 String
1094 | String ',' StringList
1099Directive ::= '%' Directive';
1103Directive' ::= 'lib' CodeGen String_t
1104 | 'link' CodeGen String_t
1105 | 'flag' CodeGen String_t
1106 | 'include' CodeGen String_t
1107 | 'hide' Name
1108 | 'freeze' Name
1109 | 'access' Accessibility
1110 | 'default' Totality
1111 | 'logging' Natural
1112 | 'dynamic' StringList
1113 | 'name' Name NameList
1114 | 'error_handlers' Name NameList
1115 | 'language' 'TypeProviders'
1116 | 'language' 'ErrorReflection'
1120directive :: SyntaxInfo -> IdrisParser [PDecl]
1121directive syn = do try (lchar '%' *> reserved "lib")
1122 cgn <- codegen_
1123 lib <- fmap fst stringLiteral
1124 return [PDirective (DLib cgn lib)]
1125 <|> do try (lchar '%' *> reserved "link")
1126 cgn <- codegen_; obj <- fst <$> stringLiteral
1127 return [PDirective (DLink cgn obj)]
1128 <|> do try (lchar '%' *> reserved "flag")
1129 cgn <- codegen_; flag <- fst <$> stringLiteral
1130 return [PDirective (DFlag cgn flag)]
1131 <|> do try (lchar '%' *> reserved "include")
1132 cgn <- codegen_
1133 hdr <- fst <$> stringLiteral
1134 return [PDirective (DInclude cgn hdr)]
1135 <|> do try (lchar '%' *> reserved "hide"); n <- fst <$> fnName
1136 return [PDirective (DHide n)]
1137 <|> do try (lchar '%' *> reserved "freeze"); n <- fst <$> iName []
1138 return [PDirective (DFreeze n)]
1139 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1140 return [PDirective (DAccess acc)]
1141 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1142 i <- get
1143 put (i { default_total = tot } )
1144 return [PDirective (DDefault tot)]
1145 <|> do try (lchar '%' *> reserved "logging")
1146 i <- fst <$> natural
1147 return [PDirective (DLogging i)]
1148 <|> do try (lchar '%' *> reserved "dynamic")
1149 libs <- sepBy1 (fmap fst stringLiteral) (lchar ',')
1150 return [PDirective (DDynamicLibs libs)]
1151 <|> do try (lchar '%' *> reserved "name")
1152 (ty, tyFC) <- fnName
1153 ns <- sepBy1 name (lchar ',')
1154 return [PDirective (DNameHint ty tyFC ns)]
1155 <|> do try (lchar '%' *> reserved "error_handlers")
1156 (fn, nfc) <- fnName
1157 (arg, afc) <- fnName
1158 ns <- sepBy1 name (lchar ',')
1159 return [PDirective (DErrorHandlers fn nfc arg afc ns) ]
1160 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1161 return [PDirective (DLanguage ext)]
1162 <|> do fc <- getFC
1163 try (lchar '%' *> reserved "used")
1164 fn <- fst <$> fnName
1165 arg <- fst <$> iName []
1166 return [PDirective (DUsed fc fn arg)]
1167 <?> "directive"
1169pLangExt :: IdrisParser LanguageExt
1170pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1171 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1173{- | Parses a totality
1176Totality ::= 'partial' | 'total'
1180totality :: IdrisParser Bool
1181totality
1182 = do reservedHL "total"; return True
1183 <|> do reservedHL "partial"; return False
1185{- | Parses a type provider
1188Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1189ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1191 -}
1192provider :: SyntaxInfo -> IdrisParser [PDecl]
1193provider syn = do doc <- try (do (doc, _) <- docstring syn
1194 fc1 <- getFC
1195 lchar '%'
1196 fc2 <- reservedFC "provide"
1197 highlightP (spanFC fc1 fc2) AnnKeyword
1198 return doc)
1199 provideTerm doc <|> providePostulate doc
1200 <?> "type provider"
1201 where provideTerm doc =
1202 do lchar '('; (n, nfc) <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1203 fc <- getFC
1204 reservedHL "with"
1205 e <- expr syn <?> "provider expression"
1206 return [PProvider doc syn fc nfc (ProvTerm t e) n]
1207 providePostulate doc =
1208 do reservedHL "postulate"
1209 (n, nfc) <- fnName
1210 fc <- getFC
1211 reservedHL "with"
1212 e <- expr syn <?> "provider expression"
1213 return [PProvider doc syn fc nfc (ProvPostulate e) n]
1215{- | Parses a transform
1218Transform ::= '%' 'transform' Expr '==>' Expr
1221transform :: SyntaxInfo -> IdrisParser [PDecl]
1222transform syn = do try (lchar '%' *> reserved "transform")
1223 -- leave it unchecked, until we work out what this should
1224 -- actually mean...
1225-- safety <- option True (do reserved "unsafe"
1226-- return False)
1227 l <- expr syn
1228 fc <- getFC
1229 symbol "==>"
1230 r <- expr syn
1231 return [PTransform fc False l r]
1232 <?> "transform"
1235{- * Loading and parsing -}
1236{- | Parses an expression from input -}
1237parseExpr :: IState -> String -> Result PTerm
1238parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1240{- | Parses a constant form input -}
1241parseConst :: IState -> String -> Result Const
1242parseConst st = runparser (fmap fst constant) st "(input)"
1244{- | Parses a tactic from input -}
1245parseTactic :: IState -> String -> Result PTactic
1246parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1248{- | Parses a do-step from input (used in the elab shell) -}
1249parseElabShellStep :: IState -> String -> Result (Either ElabShellCmd PDo)
1250parseElabShellStep ist = runparser (fmap Right (do_ defaultSyntax) <|> fmap Left elabShellCmd) ist "(input)"
1251 where elabShellCmd = char ':' >>
1252 (reserved "qed" >> pure EQED ) <|>
1253 (reserved "abandon" >> pure EAbandon ) <|>
1254 (reserved "undo" >> pure EUndo ) <|>
1255 (reserved "state" >> pure EProofState) <|>
1256 (reserved "term" >> pure EProofTerm ) <|>
1257 (expressionTactic ["e", "eval"] EEval ) <|>
1258 (expressionTactic ["t", "type"] ECheck) <|>
1259 (expressionTactic ["search"] ESearch ) <|>
1260 (do reserved "doc"
1261 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)
1262 eof
1263 return (EDocStr doc))
1264 <?> "elab command"
1265 expressionTactic cmds tactic =
1266 do asum (map reserved cmds)
1267 t <- spaced (expr defaultSyntax)
1268 i <- get
1269 return $ tactic (desugar defaultSyntax i t)
1270 spaced parser = indentPropHolds gtProp *> parser
1272-- | Parse module header and imports
1273parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Delta)
1274parseImports fname input
1275 = do i <- getIState
1276 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1277 Failure err -> fail (show err)
1278 Success (x, annots, i) ->
1279 do putIState i
1280 fname' <- runIO $ Dir.makeAbsolute fname
1281 sendHighlighting $ addPath annots fname'
1282 return x
1283 where imports :: IdrisParser ((Maybe (Docstring ()), [String],
1284 [ImportInfo],
1285 Maybe Delta),
1286 [(FC, OutputAnnotation)], IState)
1287 imports = do whiteSpace
1288 (mdoc, mname, annots) <- moduleHeader
1289 ps <- many import_
1290 mrk <- mark
1291 isEof <- lookAheadMatches eof
1292 let mrk' = if isEof
1293 then Nothing
1294 else Just mrk
1295 i <- get
1296 return ((mdoc, mname, ps, mrk'), annots, i)
1297 addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]
1298 addPath [] _ = []
1299 addPath ((fc, AnnNamespace ns Nothing) : annots) path =
1300 (fc, AnnNamespace ns (Just path)) : addPath annots path
1301 addPath (annot:annots) path = annot : addPath annots path
1303-- | There should be a better way of doing this...
1304findFC :: Doc -> (FC, String)
1305findFC x = let s = show (plain x) in findFC' s
1306 where findFC' s = case span (/= ':') s of
1307 -- Horrid kludge to prevent crashes on Windows
1308 (prefix, ':':'\\':rest) ->
1309 case findFC' rest of
1310 (NoFC, msg) -> (NoFC, msg)
1311 (FileFC f, msg) -> (FileFC (prefix ++ ":\\" ++ f), msg)
1312 (FC f start end, msg) -> (FC (prefix ++ ":\\" ++ f) start end, msg)
1313 (failname, ':':rest) -> case span isDigit rest of
1314 (line, ':':rest') -> case span isDigit rest' of
1315 (col, ':':msg) -> let pos = (read line, read col) in
1316 (FC failname pos pos, msg)
1318-- | Check if the coloring matches the options and corrects if necessary
1319fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1320fixColour False doc = ANSI.plain doc
1321fixColour True doc = doc
1323-- | A program is a list of declarations, possibly with associated
1324-- documentation strings.
1325parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1326 Idris [PDecl]
1327parseProg syn fname input mrk
1328 = do i <- getIState
1329 case runparser mainProg i fname input of
1330 Failure doc -> do -- FIXME: Get error location from trifecta
1331 -- this can't be the solution!
1332 -- Issue #1575 on the issue tracker.
1333 -- https://github.com/idris-lang/Idris-dev/issues/1575
1334 let (fc, msg) = findFC doc
1335 i <- getIState
1336 case idris_outputmode i of
1337 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1338 IdeMode n h -> iWarn fc (P.text msg)
1339 putIState (i { errSpan = Just fc })
1340 return []
1341 Success (x, i) -> do putIState i
1342 reportParserWarnings
1343 return $ collect x
1344 where mainProg :: IdrisParser ([PDecl], IState)
1345 mainProg = case mrk of
1346 Nothing -> do i <- get; return ([], i)
1347 Just mrk -> do
1348 release mrk
1349 ds <- prog syn
1350 i' <- get
1351 return (ds, i')
1353{- | Load idris module and show error if something wrong happens -}
1354loadModule :: FilePath -> Idris (Maybe String)
1355loadModule f
1356 = idrisCatch (loadModule' f)
1357 (\e -> do setErrSpan (getErrSpan e)
1358 ist <- getIState
1359 iWarn (getErrSpan e) $ pprintErr ist e
1360 return Nothing)
1362{- | Load idris module -}
1363loadModule' :: FilePath -> Idris (Maybe String)
1364loadModule' f
1365 = do i <- getIState
1366 let file = takeWhile (/= ' ') f
1367 ibcsd <- valIBCSubDir i
1368 ids <- allImportDirs
1369 fp <- findImport ids ibcsd file
1370 if file `elem` imported i
1371 then do logLvl 1 $ "Already read " ++ file
1372 return Nothing
1373 else do putIState (i { imported = file : imported i })
1374 case fp of
1375 IDR fn -> loadSource False fn Nothing
1376 LIDR fn -> loadSource True fn Nothing
1377 IBC fn src ->
1378 idrisCatch (loadIBC True fn)
1379 (\c -> do logLvl 1 $ fn ++ " failed " ++ pshow i c
1380 case src of
1381 IDR sfn -> loadSource False sfn Nothing
1382 LIDR sfn -> loadSource True sfn Nothing)
1383 return $ Just file
1385{- | Load idris code from file -}
1386loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()
1387loadFromIFile reexp i@(IBC fn src) maxline
1388 = do logLvl 1 $ "Skipping " ++ getSrcFile i
1389 idrisCatch (loadIBC reexp fn)
1390 (\err -> ierror $ LoadingFailed fn err)
1391 where
1392 getSrcFile (IDR fn) = fn
1393 getSrcFile (LIDR fn) = fn
1394 getSrcFile (IBC f src) = getSrcFile src
1396loadFromIFile _ (IDR fn) maxline = loadSource' False fn maxline
1397loadFromIFile _ (LIDR fn) maxline = loadSource' True fn maxline
1399{-| Load idris source code and show error if something wrong happens -}
1400loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1401loadSource' lidr r maxline
1402 = idrisCatch (loadSource lidr r maxline)
1403 (\e -> do setErrSpan (getErrSpan e)
1404 ist <- getIState
1405 case e of
1406 At f e' -> iWarn f (pprintErr ist e')
1407 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1409{- | Load Idris source code-}
1410loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1411loadSource lidr f toline
1412 = do logLvl 1 ("Reading " ++ f)
1413 i <- getIState
1414 let def_total = default_total i
1415 file_in <- runIO $ readSource f
1416 file <- if lidr then tclift $ unlit f file_in else return file_in
1417 (mdocs, mname, imports_in, pos) <- parseImports f file
1418 ai <- getAutoImports
1419 let imports = map (\n -> ImportInfo True n Nothing [] NoFC NoFC) ai ++ imports_in
1420 ids <- allImportDirs
1421 ibcsd <- valIBCSubDir i
1422 mapM_ (\(re, f, ns, nfc) ->
1423 do fp <- findImport ids ibcsd f
1424 case fp of
1425 LIDR fn -> ifail $ "No ibc for " ++ f
1426 IDR fn -> ifail $ "No ibc for " ++ f
1427 IBC fn src ->
1428 do loadIBC True fn
1429 let srcFn = case src of
1430 IDR fn -> Just fn
1431 LIDR fn -> Just fn
1432 _ -> Nothing
1433 srcFnAbs <- case srcFn of
1434 Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)
1435 Nothing -> return Nothing
1436 sendHighlighting [(nfc, AnnNamespace ns srcFnAbs)])
1437 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]
1438 reportParserWarnings
1439 sendParserHighlighting
1441 -- process and check module aliases
1442 let modAliases = M.fromList
1443 [ (prep alias, prep realName)
1444 | ImportInfo { import_reexport = reexport
1445 , import_path = realName
1446 , import_rename = Just (alias, _)
1447 , import_location = fc } <- imports
1449 prep = map T.pack . reverse . Spl.splitOn [pathSeparator]
1450 aliasNames = [ (alias, fc)
1451 | ImportInfo { import_rename = Just (alias, _)
1452 , import_location = fc } <- imports
1454 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1455 case map head . filter ((/= 1) . length) $ histogram of
1456 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1457 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1459 i <- getIState
1460 putIState (i { default_access = Hidden, module_aliases = modAliases })
1461 clearIBC -- start a new .ibc file
1462 -- record package info in .ibc
1463 imps <- allImportDirs
1464 mapM_ addIBC (map IBCImportDir imps)
1465 mapM_ (addIBC . IBCImport)
1466 [ (reexport, realName)
1467 | ImportInfo { import_reexport = reexport
1468 , import_path = realName
1469 } <- imports
1471 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1472 maxline = toline }
1473 ist <- getIState
1474 -- Save the span from parsing the module header, because
1475 -- an empty program parse might obliterate it.
1476 let oldSpan = idris_parsedSpan ist
1477 ds' <- parseProg syntax f file pos
1479 case (ds', oldSpan) of
1480 ([], Just fc) ->
1481 -- If no program elements were parsed, we dind't
1482 -- get a loaded region in the IBC file. That
1483 -- means we need to add it back.
1484 do ist <- getIState
1485 putIState ist { idris_parsedSpan = oldSpan
1486 , ibc_write = IBCParsedRegion fc :
1487 ibc_write ist
1489 _ -> return ()
1490 sendParserHighlighting
1492 -- Parsing done, now process declarations
1494 let ds = namespaces mname ds'
1495 logLvl 3 (show $ showDecls verbosePPOption ds)
1496 i <- getIState
1497 logLvl 10 (show (toAlist (idris_implicits i)))
1498 logLvl 3 (show (idris_infixes i))
1499 -- Now add all the declarations to the context
1500 v <- verbose
1501 when v $ iputStrLn $ "Type checking " ++ f
1502 -- we totality check after every Mutual block, so if
1503 -- anything is a single definition, wrap it in a
1504 -- mutual block on its own
1505 elabDecls toplevel (map toMutual ds)
1506 i <- getIState
1507 -- simplify every definition do give the totality checker
1508 -- a better chance
1509 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1510 ctxt' <-
1511 do ctxt <- getContext
1512 tclift $ simplifyCasedef n (getErasureInfo i) ctxt
1513 setContext ctxt')
1514 (map snd (idris_totcheck i))
1515 -- build size change graph from simplified definitions
1516 logLvl 1 "Totality checking"
1517 i <- getIState
1518 mapM_ buildSCG (idris_totcheck i)
1519 mapM_ checkDeclTotality (idris_totcheck i)
1521 -- Redo totality check for deferred names
1522 let deftots = idris_defertotcheck i
1523 logLvl 1 $ "Totality checking " ++ show deftots
1524 mapM_ (\x -> do tot <- getTotality x
1525 case tot of
1526 Total _ -> setTotality x Unchecked
1527 _ -> return ()) (map snd deftots)
1528 mapM_ buildSCG deftots
1529 mapM_ checkDeclTotality deftots
1531 logLvl 1 ("Finished " ++ f)
1532 ibcsd <- valIBCSubDir i
1533 logLvl 1 "Universe checking"
1534 iucheck
1535 let ibc = ibcPathNoFallback ibcsd f
1536 i <- getIState
1537 addHides (hide_list i)
1539 -- Save module documentation if applicable
1540 i <- getIState
1541 case mdocs of
1542 Nothing -> return ()
1543 Just docs -> addModDoc syntax mname docs
1546 -- Finally, write an ibc and highlights if checking was successful
1547 ok <- noErrors
1548 when ok $
1549 do idrisCatch (do writeIBC f ibc; clearIBC)
1550 (\c -> return ()) -- failure is harmless
1551 hl <- getDumpHighlighting
1552 when hl $
1553 idrisCatch (writeHighlights f)
1554 (const $ return ()) -- failure is harmless
1555 clearHighlights
1556 i <- getIState
1557 putIState (i { default_total = def_total,
1558 hide_list = [] })
1559 return ()
1560 where
1561 namespaces :: [String] -> [PDecl] -> [PDecl]
1562 namespaces [] ds = ds
1563 namespaces (x:xs) ds = [PNamespace x NoFC (namespaces xs ds)]
1565 toMutual :: PDecl -> PDecl
1566 toMutual m@(PMutual _ d) = m
1567 toMutual (PNamespace x fc ds) = PNamespace x fc (map toMutual ds)
1568 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1569 case x of
1570 PClauses{} -> r
1571 PClass{} -> r
1572 PData{} -> r
1573 PInstance{} -> r
1574 _ -> x
1576 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1577 addModDoc syn mname docs =
1578 do ist <- getIState
1579 docs' <- elabDocTerms recinfo (parsedDocs ist)
1580 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1581 putIState ist { idris_moduledocs = modDocs' }
1582 addIBC (IBCModDocs docName)
1583 where
1584 docName = NS modDocName (map T.pack (reverse mname))
1585 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1587{- | Adds names to hide list -}
1588addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1589addHides xs = do i <- getIState
1590 let defh = default_access i
1591 let (hs, as) = partition isNothing xs
1592 unless (null as) $
1593 mapM_ doHide
1594 (map (\ (n, _) -> (n, defh)) hs ++
1595 map (\ (n, Just a) -> (n, a)) as)
1596 where isNothing (_, Nothing) = True
1597 isNothing _ = False
1599 doHide (n, a) = do setAccessibility n a
1600 addIBC (IBCAccess n a)