git.iko.soy/Idris-dev
on da672ec help sign in
Idris-dev/src/Idris/Parser.hs
1784 lines 68 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 | RunElabDecl
183 ;
185-}
186decl :: SyntaxInfo -> IdrisParser [PDecl]
187decl syn = try (externalDecl syn)
188 <|> internalDecl syn
189 <?> "declaration"
191internalDecl :: SyntaxInfo -> IdrisParser [PDecl]
192internalDecl syn
193 = do fc <- getFC
194 -- if we're after maxline, stop at the next type declaration
195 -- (so we get all cases of a definition to preserve totality
196 -- results, in particular).
197 let continue = case maxline syn of
198 Nothing -> True
199 Just l -> if fst (fc_end fc) > l
200 then mut_nesting syn /= 0
201 else True
202 -- What I'd really like to do here is explicitly save the
203 -- current state, then if reading ahead finds we've passed
204 -- the end of the definition, reset the state. But I've lost
205 -- patience with trying to find out how to do that from the
206 -- trifecta docs, so this does the job instead.
207 if continue then
208 do notEndBlock
209 declBody continue
210 else try (do notEndBlock
211 declBody continue)
212 <|> fail "End of readable input"
213 where declBody :: Bool -> IdrisParser [PDecl]
214 declBody b = declBody' b
215 <|> using_ syn
216 <|> params syn
217 <|> mutual syn
218 <|> namespace syn
219 <|> class_ syn
220 <|> instance_ syn
221 <|> do d <- dsl syn; return [d]
222 <|> directive syn
223 <|> provider syn
224 <|> transform syn
225 <|> do import_; fail "imports must be at top of file"
226 <?> "declaration"
227 declBody' :: Bool -> IdrisParser [PDecl]
228 declBody' cont = do d <- decl' syn
229 i <- get
230 let d' = fmap (debindApp syn . (desugar syn i)) d
231 if continue cont d'
232 then return [d']
233 else fail "End of readable input"
235 -- Keep going while we're still parsing clauses
236 continue False (PClauses _ _ _ _) = True
237 continue c _ = c
239{- | Parses a top-level declaration with possible syntax sugar
242Decl' ::=
243 Fixity
244 | FunDecl'
245 | Data
246 | Record
247 | SyntaxDecl
248 ;
250-}
251decl' :: SyntaxInfo -> IdrisParser PDecl
252decl' syn = fixity
253 <|> syntaxDecl syn
254 <|> fnDecl' syn
255 <|> data_ syn
256 <|> record syn
257 <|> runElabDecl syn
258 <?> "declaration"
260externalDecl :: SyntaxInfo -> IdrisParser [PDecl]
261externalDecl syn = do i <- get
262 notEndBlock
263 FC fn start _ <- getFC
264 decls <- declExtensions syn (syntaxRulesList $ syntax_rules i)
265 FC _ _ end <- getFC
266 let outerFC = FC fn start end
267 return $ map (mapPDeclFC (fixFC outerFC)
268 (fixFCH fn outerFC))
269 decls
270 where
271 -- | Fix non-highlighting FCs to prevent spurious error location reports
272 fixFC :: FC -> FC -> FC
273 fixFC outer inner | inner `fcIn` outer = inner
274 | otherwise = outer
275 -- | Fix highlighting FCs by obliterating them, to avoid spurious highlights
276 fixFCH fn outer inner | inner `fcIn` outer = inner
277 | otherwise = FileFC fn
279declExtensions :: SyntaxInfo -> [Syntax] -> IdrisParser [PDecl]
280declExtensions syn rules = declExtension syn [] (filter isDeclRule rules)
281 <?> "user-defined declaration"
282 where
283 isDeclRule (DeclRule _ _) = True
284 isDeclRule _ = False
286declExtension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax]
287 -> IdrisParser [PDecl]
288declExtension syn ns rules =
289 choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->
290 case head rs of -- can never be []
291 DeclRule (symb:_) _ -> try $ do
292 n <- extSymbol symb
293 declExtension syn (n : ns) [DeclRule ss t | (DeclRule (_:ss) t) <- rs]
294 -- If we have more than one Rule in this bucket, our grammar is
295 -- nondeterministic.
296 DeclRule [] dec -> let r = map (update (mapMaybe id ns)) dec in
297 return r
299 where
300 update :: [(Name, SynMatch)] -> PDecl -> PDecl
301 update ns = updateNs ns . fmap (updateRefs ns) . fmap (updateSynMatch ns)
303 updateRefs ns = mapPT newref
304 where
305 newref (PRef fc fcs n) = PRef fc fcs (updateB ns n)
306 newref t = t
308 -- Below is a lot of tedious boilerplate which updates any top level
309 -- names in the declaration. It will only change names which are bound in
310 -- the declaration (including method names in classes and field names in
311 -- record declarations, not including pattern variables)
312 updateB :: [(Name, SynMatch)] -> Name -> Name
313 updateB ns (NS n mods) = NS (updateB ns n) mods
314 updateB ns n = case lookup n ns of
315 Just (SynBind tfc t) -> t
316 _ -> n
318 updateNs :: [(Name, SynMatch)] -> PDecl -> PDecl
319 updateNs ns (PTy doc argdoc s fc o n fc' t)
320 = PTy doc argdoc s fc o (updateB ns n) fc' t
321 updateNs ns (PClauses fc o n cs)
322 = PClauses fc o (updateB ns n) (map (updateClause ns) cs)
323 updateNs ns (PCAF fc n t) = PCAF fc (updateB ns n) t
324 updateNs ns (PData ds cds s fc o dat)
325 = PData ds cds s fc o (updateData ns dat)
326 updateNs ns (PParams fc ps ds) = PParams fc ps (map (updateNs ns) ds)
327 updateNs ns (PNamespace s fc ds) = PNamespace s fc (map (updateNs ns) ds)
328 updateNs ns (PRecord doc syn fc o n fc' ps pdocs fields cname cdoc s)
329 = PRecord doc syn fc o (updateB ns n) fc' ps pdocs
330 (map (updateField ns) fields)
331 (updateRecCon ns cname)
332 cdoc
333 s
334 updateNs ns (PClass docs s fc cs cn fc' ps pdocs pdets ds cname cdocs)
335 = PClass docs s fc cs (updateB ns cn) fc' ps pdocs pdets
336 (map (updateNs ns) ds)
337 (updateRecCon ns cname)
338 cdocs
339 updateNs ns (PInstance docs pdocs s fc cs cn fc' ps ity ni ds)
340 = PInstance docs pdocs s fc cs (updateB ns cn) fc'
341 ps ity (fmap (updateB ns) ni)
342 (map (updateNs ns) ds)
343 updateNs ns (PMutual fc ds) = PMutual fc (map (updateNs ns) ds)
344 updateNs ns (PProvider docs s fc fc' pw n)
345 = PProvider docs s fc fc' pw (updateB ns n)
346 updateNs ns d = d
348 updateRecCon ns Nothing = Nothing
349 updateRecCon ns (Just (n, fc)) = Just (updateB ns n, fc)
351 updateField ns (m, p, t, doc) = (updateRecCon ns m, p, t, doc)
353 updateClause ns (PClause fc n t ts t' ds)
354 = PClause fc (updateB ns n) t ts t' (map (update ns) ds)
355 updateClause ns (PWith fc n t ts t' m ds)
356 = PWith fc (updateB ns n) t ts t' m (map (update ns) ds)
357 updateClause ns (PClauseR fc ts t ds)
358 = PClauseR fc ts t (map (update ns) ds)
359 updateClause ns (PWithR fc ts t m ds)
360 = PWithR fc ts t m (map (update ns) ds)
362 updateData ns (PDatadecl n fc t cs)
363 = PDatadecl (updateB ns n) fc t (map (updateCon ns) cs)
364 updateData ns (PLaterdecl n fc t)
365 = PLaterdecl (updateB ns n) fc t
367 updateCon ns (cd, ads, cn, fc, ty, fc', fns)
368 = (cd, ads, updateB ns cn, fc, ty, fc', fns)
370 ruleGroup [] [] = True
371 ruleGroup (s1:_) (s2:_) = s1 == s2
372 ruleGroup _ _ = False
374 extSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
375 extSymbol (Keyword n) = do fc <- reservedFC (show n)
376 highlightP fc AnnKeyword
377 return Nothing
378 extSymbol (Expr n) = do tm <- expr syn
379 return $ Just (n, SynTm tm)
380 extSymbol (SimpleExpr n) = do tm <- simpleExpr syn
381 return $ Just (n, SynTm tm)
382 extSymbol (Binding n) = do (b, fc) <- name
383 return $ Just (n, SynBind fc b)
384 extSymbol (Symbol s) = do fc <- symbolFC s
385 highlightP fc AnnKeyword
386 return Nothing
388{- | Parses a syntax extension declaration (and adds the rule to parser state)
391 SyntaxDecl ::= SyntaxRule;
393-}
394syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
395syntaxDecl syn = do s <- syntaxRule syn
396 i <- get
397 put (i `addSyntax` s)
398 fc <- getFC
399 return (PSyntax fc s)
401-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.
402addSyntax :: IState -> Syntax -> IState
403addSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
404 syntax_keywords = ks ++ ns,
405 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc }
406 where rs = syntax_rules i
407 ns = syntax_keywords i
408 ibc = ibc_write i
409 ks = map show (syntaxNames s)
411-- | Like 'addSyntax', but no effect on the IBC.
412addReplSyntax :: IState -> Syntax -> IState
413addReplSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
414 syntax_keywords = ks ++ ns }
415 where rs = syntax_rules i
416 ns = syntax_keywords i
417 ks = map show (syntaxNames s)
419{- | Parses a syntax extension declaration
422SyntaxRuleOpts ::= 'term' | 'pattern';
426SyntaxRule ::=
427 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
431SyntaxSym ::= '[' Name_t ']'
432 | '{' Name_t '}'
433 | Name_t
434 | StringLiteral_t
435 ;
437-}
438syntaxRule :: SyntaxInfo -> IdrisParser Syntax
439syntaxRule syn
440 = do sty <- try (do
441 pushIndent
442 sty <- option AnySyntax
443 (do reservedHL "term"; return TermSyntax
444 <|> do reservedHL "pattern"; return PatternSyntax)
445 reservedHL "syntax"
446 return sty)
447 syms <- some syntaxSym
448 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
449 let ns = mapMaybe getName syms
450 when (length ns /= length (nub ns))
451 $ unexpected "repeated variable in syntax rule"
452 lchar '='
453 tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]
454 terminator
455 return (Rule (mkSimple syms) tm sty)
456 <|> do reservedHL "decl"; reservedHL "syntax"
457 syms <- some syntaxSym
458 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
459 let ns = mapMaybe getName syms
460 when (length ns /= length (nub ns))
461 $ unexpected "repeated variable in syntax rule"
462 lchar '='
463 openBlock
464 dec <- some (decl syn)
465 closeBlock
466 return (DeclRule (mkSimple syms) (concat dec))
467 where
468 isExpr (Expr _) = True
469 isExpr _ = False
470 getName (Expr n) = Just n
471 getName _ = Nothing
472 -- Can't parse two full expressions (i.e. expressions with application) in a row
473 -- so change them both to a simple expression
474 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
475 mkSimple xs = mkSimple' xs
477 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
478 mkSimple es
479 -- Can't parse a full expression followed by operator like characters due to ambiguity
480 mkSimple' (Expr e : Symbol s : es)
481 | takeWhile (`elem` opChars) ts /= "" = SimpleExpr e : Symbol s : mkSimple' es
482 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s
483 mkSimple' (e : es) = e : mkSimple' es
484 mkSimple' [] = []
486 -- Prevent syntax variable capture by making all binders under syntax unique
487 -- (the ol' Common Lisp GENSYM approach)
488 uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
489 uniquifyBinders userNames = fixBind []
490 where
491 fixBind :: [(Name, Name)] -> PTerm -> IdrisParser PTerm
492 fixBind rens (PRef fc hls n) | Just n' <- lookup n rens =
493 return $ PRef fc hls n'
494 fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =
495 return $ PPatvar fc n'
496 fixBind rens (PLam fc n nfc ty body)
497 | n `elem` userNames = liftM2 (PLam fc n nfc) (fixBind rens ty) (fixBind rens body)
498 | otherwise =
499 do ty' <- fixBind rens ty
500 n' <- gensym n
501 body' <- fixBind ((n,n'):rens) body
502 return $ PLam fc n' nfc ty' body'
503 fixBind rens (PPi plic n nfc argTy body)
504 | n `elem` userNames = liftM2 (PPi plic n nfc) (fixBind rens argTy) (fixBind rens body)
505 | otherwise =
506 do ty' <- fixBind rens argTy
507 n' <- gensym n
508 body' <- fixBind ((n,n'):rens) body
509 return $ (PPi plic n' nfc ty' body')
510 fixBind rens (PLet fc n nfc ty val body)
511 | n `elem` userNames = liftM3 (PLet fc n nfc)
512 (fixBind rens ty)
513 (fixBind rens val)
514 (fixBind rens body)
515 | otherwise =
516 do ty' <- fixBind rens ty
517 val' <- fixBind rens val
518 n' <- gensym n
519 body' <- fixBind ((n,n'):rens) body
520 return $ PLet fc n' nfc ty' val' body'
521 fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =
522 return $ PMatchApp fc n'
523 fixBind rens x = descendM (fixBind rens) x
525 gensym :: Name -> IdrisParser Name
526 gensym n = do ist <- get
527 let idx = idris_name ist
528 put ist { idris_name = idx + 1 }
529 return $ sMN idx (show n)
531{- | Parses a syntax symbol (either binding variable, keyword or expression)
534SyntaxSym ::= '[' Name_t ']'
535 | '{' Name_t '}'
536 | Name_t
537 | StringLiteral_t
538 ;
540 -}
541syntaxSym :: IdrisParser SSymbol
542syntaxSym = try (do lchar '['; n <- fst <$> name; lchar ']'
543 return (Expr n))
544 <|> try (do lchar '{'; n <- fst <$> name; lchar '}'
545 return (Binding n))
546 <|> do n <- fst <$> iName []
547 return (Keyword n)
548 <|> do sym <- fmap fst stringLiteral
549 return (Symbol sym)
550 <?> "syntax symbol"
552{- | Parses a function declaration with possible syntax sugar
555 FunDecl ::= FunDecl';
557-}
558fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
559fnDecl syn = try (do notEndBlock
560 d <- fnDecl' syn
561 i <- get
562 let d' = fmap (desugar syn i) d
563 return [d']) <?> "function declaration"
565{-| Parses a function declaration
568 FunDecl' ::=
569 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
570 | Postulate
571 | Pattern
572 | CAF
573 ;
575-}
576fnDecl' :: SyntaxInfo -> IdrisParser PDecl
577fnDecl' syn = checkFixity $
578 do (doc, argDocs, fc, opts', n, nfc, acc) <- try (do
579 pushIndent
580 (doc, argDocs) <- docstring syn
581 ist <- get
582 let initOpts = if default_total ist
583 then [TotalFn]
584 else []
585 opts <- fnOpts initOpts
586 acc <- optional accessibility
587 opts' <- fnOpts opts
588 (n_in, nfc) <- fnName
589 let n = expandNS syn n_in
590 fc <- getFC
591 lchar ':'
592 return (doc, argDocs, fc, opts', n, nfc, acc))
593 ty <- typeExpr (allowImp syn)
594 terminator
595 addAcc n acc
596 return (PTy doc argDocs syn fc opts' n nfc ty)
597 <|> postulate syn
598 <|> caf syn
599 <|> pattern syn
600 <?> "function declaration"
601 where checkFixity :: IdrisParser PDecl -> IdrisParser PDecl
602 checkFixity p = do decl <- p
603 case getName decl of
604 Nothing -> return decl
605 Just n -> do fOk <- fixityOK n
606 unless fOk . fail $
607 "Missing fixity declaration for " ++ show n
608 return decl
609 getName (PTy _ _ _ _ _ n _ _) = Just n
610 getName _ = Nothing
611 fixityOK (NS n _) = fixityOK n
612 fixityOK (UN n) | all (flip elem opChars) (str n) =
613 do fixities <- fmap idris_infixes get
614 return . elem (str n) . map (\ (Fix _ op) -> op) $ fixities
615 | otherwise = return True
616 fixityOK _ = return True
618{-| Parses function options given initial options
621FnOpts ::= 'total'
622 | 'partial'
623 | 'covering'
624 | 'implicit'
625 | '%' 'no_implicit'
626 | '%' 'assert_total'
627 | '%' 'error_handler'
628 | '%' 'reflection'
629 | '%' 'specialise' '[' NameTimesList? ']'
630 ;
634NameTimes ::= FnName Natural?;
638NameTimesList ::=
639 NameTimes
640 | NameTimes ',' NameTimesList
641 ;
643-}
644-- FIXME: Check compatability for function options (i.e. partal/total)
645--
646-- Issue #1574 on the issue tracker.
647-- https://github.com/idris-lang/Idris-dev/issues/1574
648fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
649fnOpts opts
650 = do reservedHL "total"; fnOpts (TotalFn : opts)
651 <|> do reservedHL "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
652 <|> do reservedHL "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))
653 <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;
654 fnOpts (CExport c : opts)
655 <|> do try (lchar '%' *> reserved "no_implicit");
656 fnOpts (NoImplicit : opts)
657 <|> do try (lchar '%' *> reserved "inline");
658 fnOpts (Inlinable : opts)
659 <|> do try (lchar '%' *> reserved "assert_total");
660 fnOpts (AssertTotal : opts)
661 <|> do try (lchar '%' *> reserved "error_handler");
662 fnOpts (ErrorHandler : opts)
663 <|> do try (lchar '%' *> reserved "error_reverse");
664 fnOpts (ErrorReverse : opts)
665 <|> do try (lchar '%' *> reserved "reflection");
666 fnOpts (Reflection : opts)
667 <|> do try (lchar '%' *> reserved "hint");
668 fnOpts (AutoHint : opts)
669 <|> do lchar '%'; reserved "specialise";
670 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
671 fnOpts (Specialise ns : opts)
672 <|> do reservedHL "implicit"; fnOpts (Implicit : opts)
673 <|> return opts
674 <?> "function modifier"
675 where nameTimes :: IdrisParser (Name, Maybe Int)
676 nameTimes = do n <- fst <$> fnName
677 t <- option Nothing (do reds <- fmap fst natural
678 return (Just (fromInteger reds)))
679 return (n, t)
681{- | Parses a postulate
684Postulate ::=
685 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
686 ;
688-}
689postulate :: SyntaxInfo -> IdrisParser PDecl
690postulate syn = do (doc, ext)
691 <- try $ do (doc, _) <- docstring syn
692 pushIndent
693 ext <- ppostDecl
694 return (doc, ext)
695 ist <- get
696 let initOpts = if default_total ist
697 then [TotalFn]
698 else []
699 opts <- fnOpts initOpts
700 acc <- optional accessibility
701 opts' <- fnOpts opts
702 (n_in, nfc) <- fnName
703 let n = expandNS syn n_in
704 lchar ':'
705 ty <- typeExpr (allowImp syn)
706 fc <- getFC
707 terminator
708 addAcc n acc
709 return (PPostulate ext doc syn fc nfc opts' n ty)
710 <?> "postulate"
711 where ppostDecl = do fc <- reservedHL "postulate"; return False
712 <|> do lchar '%'; reserved "extern"; return True
713{- | Parses a using declaration
716Using ::=
717 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
718 ;
720 -}
721using_ :: SyntaxInfo -> IdrisParser [PDecl]
722using_ syn =
723 do reservedHL "using"
724 lchar '('; ns <- usingDeclList syn; lchar ')'
725 openBlock
726 let uvars = using syn
727 ds <- many (decl (syn { using = uvars ++ ns }))
728 closeBlock
729 return (concat ds)
730 <?> "using declaration"
732{- | Parses a parameters declaration
735Params ::=
736 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
737 ;
739 -}
740params :: SyntaxInfo -> IdrisParser [PDecl]
741params syn =
742 do reservedHL "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
743 let ns' = [(n, ty) | (n, _, ty) <- ns]
744 openBlock
745 let pvars = syn_params syn
746 ds <- many (decl syn { syn_params = pvars ++ ns' })
747 closeBlock
748 fc <- getFC
749 return [PParams fc ns' (concat ds)]
750 <?> "parameters declaration"
752{- | Parses a mutual declaration (for mutually recursive functions)
755Mutual ::=
756 'mutual' OpenBlock Decl* CloseBlock
757 ;
759-}
760mutual :: SyntaxInfo -> IdrisParser [PDecl]
761mutual syn =
762 do reservedHL "mutual"
763 openBlock
764 let pvars = syn_params syn
765 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
766 closeBlock
767 fc <- getFC
768 return [PMutual fc (concat ds)]
769 <?> "mutual block"
771{-| Parses a namespace declaration
774Namespace ::=
775 'namespace' identifier OpenBlock Decl+ CloseBlock
776 ;
778-}
779namespace :: SyntaxInfo -> IdrisParser [PDecl]
780namespace syn =
781 do reservedHL "namespace"
782 (n, nfc) <- identifier
783 openBlock
784 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
785 closeBlock
786 return [PNamespace n nfc (concat ds)]
787 <?> "namespace declaration"
789{- | Parses a methods block (for instances)
792 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
794-}
795instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
796instanceBlock syn = do reservedHL "where"
797 openBlock
798 ds <- many (fnDecl syn)
799 closeBlock
800 return (concat ds)
801 <?> "instance block"
803{- | Parses a methods and instances block (for type classes)
806MethodOrInstance ::=
807 FnDecl
808 | Instance
809 ;
813ClassBlock ::=
814 'where' OpenBlock Constructor? MethodOrInstance* CloseBlock
815 ;
817-}
818classBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])
819classBlock syn = do reservedHL "where"
820 openBlock
821 (cn, cd) <- option (Nothing, emptyDocstring) $
822 try (do (doc, _) <- option noDocs docComment
823 n <- constructor
824 return (Just n, doc))
825 ist <- get
826 let cd' = annotate syn ist cd
828 ds <- many (notEndBlock >> instance_ syn <|> fnDecl syn)
829 closeBlock
830 return (cn, cd', concat ds)
831 <?> "class block"
833 where
834 constructor :: IdrisParser (Name, FC)
835 constructor = reservedHL "constructor" *> fnName
837 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)
838 annotate syn ist = annotCode $ tryFullExpr syn ist
840{-| Parses a type class declaration
843ClassArgument ::=
844 Name
845 | '(' Name ':' Expr ')'
846 ;
850Class ::=
851 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
852 ;
854-}
855class_ :: SyntaxInfo -> IdrisParser [PDecl]
856class_ syn = do (doc, argDocs, acc)
857 <- try (do (doc, argDocs) <- docstring syn
858 acc <- optional accessibility
859 reservedHL "class"
860 return (doc, argDocs, acc))
861 fc <- getFC
862 cons <- constraintList syn
863 let cons' = [(c, ty) | (c, _, ty) <- cons]
864 (n_in, nfc) <- fnName
865 let n = expandNS syn n_in
866 cs <- many carg
867 fds <- option [(cn, NoFC) | (cn, _, _) <- cs] fundeps
868 (cn, cd, ds) <- option (Nothing, fst noDocs, []) (classBlock syn)
869 accData acc n (concatMap declared ds)
870 return [PClass doc syn fc cons' n nfc cs argDocs fds ds cn cd]
871 <?> "type-class declaration"
872 where
873 fundeps :: IdrisParser [(Name, FC)]
874 fundeps = do lchar '|'; sepBy name (lchar ',')
876 carg :: IdrisParser (Name, FC, PTerm)
877 carg = do lchar '('; (i, ifc) <- name; lchar ':'; ty <- expr syn; lchar ')'
878 return (i, ifc, ty)
879 <|> do (i, ifc) <- name
880 fc <- getFC
881 return (i, ifc, PType fc)
883{- | Parses a type class instance declaration
886 Instance ::=
887 DocComment_t? 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
888 ;
892InstanceName ::= '[' Name ']';
894-}
895instance_ :: SyntaxInfo -> IdrisParser [PDecl]
896instance_ syn = do (doc, argDocs)
897 <- try (docstring syn <* reservedHL "instance")
898 fc <- getFC
899 en <- optional instanceName
900 cs <- constraintList syn
901 let cs' = [(c, ty) | (c, _, ty) <- cs]
902 (cn, cnfc) <- fnName
903 args <- many (simpleExpr syn)
904 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)
905 let t = bindList (PPi constraint) cs sc
906 ds <- option [] (instanceBlock syn)
907 return [PInstance doc argDocs syn fc cs' cn cnfc args t en ds]
908 <?> "instance declaration"
909 where instanceName :: IdrisParser Name
910 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'
911 let n = expandNS syn n_in
912 return n
913 <?> "instance name"
916-- | Parse a docstring
917docstring :: SyntaxInfo
918 -> IdrisParser (Docstring (Either Err PTerm),
919 [(Name,Docstring (Either Err PTerm))])
920docstring syn = do (doc, argDocs) <- option noDocs docComment
921 ist <- get
922 let doc' = annotCode (tryFullExpr syn ist) doc
923 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
924 | (n, d) <- argDocs ]
925 return (doc', argDocs')
928{- | Parses a using declaration list
931UsingDeclList ::=
932 UsingDeclList'
933 | NameList TypeSig
934 ;
938UsingDeclList' ::=
939 UsingDecl
940 | UsingDecl ',' UsingDeclList'
941 ;
945NameList ::=
946 Name
947 | Name ',' NameList
948 ;
950-}
951usingDeclList :: SyntaxInfo -> IdrisParser [Using]
952usingDeclList syn
953 = try (sepBy1 (usingDecl syn) (lchar ','))
954 <|> do ns <- sepBy1 (fst <$> name) (lchar ',')
955 lchar ':'
956 t <- typeExpr (disallowImp syn)
957 return (map (\x -> UImplicit x t) ns)
958 <?> "using declaration list"
960{- |Parses a using declaration
963UsingDecl ::=
964 FnName TypeSig
965 | FnName FnName+
966 ;
968-}
969usingDecl :: SyntaxInfo -> IdrisParser Using
970usingDecl syn = try (do x <- fst <$> fnName
971 lchar ':'
972 t <- typeExpr (disallowImp syn)
973 return (UImplicit x t))
974 <|> do c <- fst <$> fnName
975 xs <- some (fst <$> fnName)
976 return (UConstraint c xs)
977 <?> "using declaration"
979{- | Parse a clause with patterns
982Pattern ::= Clause;
984-}
985pattern :: SyntaxInfo -> IdrisParser PDecl
986pattern syn = do fc <- getFC
987 clause <- clause syn
988 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
989 <?> "pattern"
991{- | Parse a constant applicative form declaration
994CAF ::= 'let' FnName '=' Expr Terminator;
996-}
997caf :: SyntaxInfo -> IdrisParser PDecl
998caf syn = do reservedHL "let"
999 n_in <- fst <$> fnName; let n = expandNS syn n_in
1000 pushIndent
1001 lchar '='
1002 t <- indented $ expr syn
1003 terminator
1004 fc <- getFC
1005 return (PCAF fc n t)
1006 <?> "constant applicative form declaration"
1008{- | Parse an argument expression
1011ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
1014argExpr :: SyntaxInfo -> IdrisParser PTerm
1015argExpr syn = let syn' = syn { inPattern = True } in
1016 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
1017 <?> "argument expression"
1019{- | Parse a right hand side of a function
1022RHS ::= '=' Expr
1023 | '?=' RHSName? Expr
1024 | Impossible
1029RHSName ::= '{' FnName '}';
1032rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
1033rhs syn n = do lchar '='; expr syn
1034 <|> do symbol "?=";
1035 fc <- getFC
1036 name <- option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";
1037 return n)
1038 r <- expr syn
1039 return (addLet fc name r)
1040 <|> impossible
1041 <?> "function right hand side"
1042 where mkN :: Name -> Name
1043 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
1044 then sUN "infix_op_lemma_1"
1045 else sUN (str x++"_lemma_1")
1046 mkN (NS x n) = NS (mkN x) n
1047 n' :: Name
1048 n' = mkN n
1049 addLet :: FC -> Name -> PTerm -> PTerm
1050 addLet fc nm (PLet fc' n nfc ty val r) = PLet fc' n nfc ty val (addLet fc nm r)
1051 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
1052 where addLetC (l, r) = (l, addLet fc nm r)
1053 addLet fc nm r = (PLet fc (sUN "value") NoFC Placeholder r (PMetavar NoFC nm))
1055{- |Parses a function clause
1058RHSOrWithBlock ::= RHS WhereOrTerminator
1059 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
1064Clause ::= WExpr+ RHSOrWithBlock
1065 | SimpleExpr '<==' FnName RHS WhereOrTerminator
1066 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
1067 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
1072ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
1076WhereOrTerminator ::= WhereBlock | Terminator;
1079clause :: SyntaxInfo -> IdrisParser PClause
1080clause syn
1081 = do wargs <- try (do pushIndent; some (wExpr syn))
1082 fc <- getFC
1083 ist <- get
1084 n <- case lastParse ist of
1085 Just t -> return t
1086 Nothing -> fail "Invalid clause"
1087 (do r <- rhs syn n
1088 let ctxt = tt_ctxt ist
1089 let wsyn = syn { syn_namespace = [] }
1090 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1091 popIndent
1092 return x,
1093 do terminator
1094 return ([], [])]
1095 return $ PClauseR fc wargs r wheres) <|> (do
1096 popIndent
1097 reservedHL "with"
1098 wval <- simpleExpr syn
1099 pn <- optProof
1100 openBlock
1101 ds <- some $ fnDecl syn
1102 let withs = concat ds
1103 closeBlock
1104 return $ PWithR fc wargs wval pn withs)
1105 <|> do ty <- try (do pushIndent
1106 ty <- simpleExpr syn
1107 symbol "<=="
1108 return ty)
1109 fc <- getFC
1110 n_in <- fst <$> fnName; let n = expandNS syn n_in
1111 r <- rhs syn n
1112 ist <- get
1113 let ctxt = tt_ctxt ist
1114 let wsyn = syn { syn_namespace = [] }
1115 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1116 popIndent
1117 return x,
1118 do terminator
1119 return ([], [])]
1120 let capp = PLet fc (sMN 0 "match") NoFC
1121 ty
1122 (PMatchApp fc n)
1123 (PRef fc [] (sMN 0 "match"))
1124 ist <- get
1125 put (ist { lastParse = Just n })
1126 return $ PClause fc n capp [] r wheres
1127 <|> do (l, op, nfc) <- try (do
1128 pushIndent
1129 l <- argExpr syn
1130 (op, nfc) <- operatorFC
1131 when (op == "=" || op == "?=" ) $
1132 fail "infix clause definition with \"=\" and \"?=\" not supported "
1133 return (l, op, nfc))
1134 let n = expandNS syn (sUN op)
1135 r <- argExpr syn
1136 fc <- getFC
1137 wargs <- many (wExpr syn)
1138 (do rs <- rhs syn n
1139 let wsyn = syn { syn_namespace = [] }
1140 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1141 popIndent
1142 return x,
1143 do terminator
1144 return ([], [])]
1145 ist <- get
1146 let capp = PApp fc (PRef nfc [nfc] n) [pexp l, pexp r]
1147 put (ist { lastParse = Just n })
1148 return $ PClause fc n capp wargs rs wheres) <|> (do
1149 popIndent
1150 reservedHL "with"
1151 wval <- bracketed syn
1152 pn <- optProof
1153 openBlock
1154 ds <- some $ fnDecl syn
1155 closeBlock
1156 ist <- get
1157 let capp = PApp fc (PRef fc [] n) [pexp l, pexp r]
1158 let withs = map (fillLHSD n capp wargs) $ concat ds
1159 put (ist { lastParse = Just n })
1160 return $ PWith fc n capp wargs wval pn withs)
1161 <|> do pushIndent
1162 (n_in, nfc) <- fnName; let n = expandNS syn n_in
1163 cargs <- many (constraintArg syn)
1164 fc <- getFC
1165 args <- many (try (implicitArg (syn { inPattern = True } ))
1166 <|> (fmap pexp (argExpr syn)))
1167 wargs <- many (wExpr syn)
1168 let capp = PApp fc (PRef nfc [nfc] n)
1169 (cargs ++ args)
1170 (do r <- rhs syn n
1171 ist <- get
1172 let ctxt = tt_ctxt ist
1173 let wsyn = syn { syn_namespace = [] }
1174 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1175 popIndent
1176 return x,
1177 do terminator
1178 return ([], [])]
1179 ist <- get
1180 put (ist { lastParse = Just n })
1181 return $ PClause fc n capp wargs r wheres) <|> (do
1182 reservedHL "with"
1183 ist <- get
1184 put (ist { lastParse = Just n })
1185 wval <- bracketed syn
1186 pn <- optProof
1187 openBlock
1188 ds <- some $ fnDecl syn
1189 let withs = map (fillLHSD n capp wargs) $ concat ds
1190 closeBlock
1191 popIndent
1192 return $ PWith fc n capp wargs wval pn withs)
1193 <?> "function clause"
1194 where
1195 optProof = option Nothing (do reservedHL "proof"
1196 n <- fnName
1197 return (Just n))
1199 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
1200 fillLHS n capp owargs (PClauseR fc wargs v ws)
1201 = PClause fc n capp (owargs ++ wargs) v ws
1202 fillLHS n capp owargs (PWithR fc wargs v pn ws)
1203 = PWith fc n capp (owargs ++ wargs) v pn
1204 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1205 fillLHS _ _ _ c = c
1207 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
1208 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1209 fillLHSD n c a x = x
1211{-| Parses with pattern
1214WExpr ::= '|' Expr';
1217wExpr :: SyntaxInfo -> IdrisParser PTerm
1218wExpr syn = do lchar '|'
1219 expr' (syn { inPattern = True })
1220 <?> "with pattern"
1222{- | Parses a where block
1225WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
1228whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
1229whereBlock n syn
1230 = do reservedHL "where"
1231 ds <- indentedBlock1 (decl syn)
1232 let dns = concatMap (concatMap declared) ds
1233 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1234 <?> "where block"
1236{- |Parses a code generation target language name
1239Codegen ::= 'C'
1240 | 'Java'
1241 | 'JavaScript'
1242 | 'Node'
1243 | 'LLVM'
1244 | 'Bytecode'
1248codegen_ :: IdrisParser Codegen
1249codegen_ = do n <- fst <$> identifier
1250 return (Via (map toLower n))
1251 <|> do reserved "Bytecode"; return Bytecode
1252 <?> "code generation language"
1254{- |Parses a compiler directive
1256StringList ::=
1257 String
1258 | String ',' StringList
1263Directive ::= '%' Directive';
1267Directive' ::= 'lib' CodeGen String_t
1268 | 'link' CodeGen String_t
1269 | 'flag' CodeGen String_t
1270 | 'include' CodeGen String_t
1271 | 'hide' Name
1272 | 'freeze' Name
1273 | 'access' Accessibility
1274 | 'default' Totality
1275 | 'logging' Natural
1276 | 'dynamic' StringList
1277 | 'name' Name NameList
1278 | 'error_handlers' Name NameList
1279 | 'language' 'TypeProviders'
1280 | 'language' 'ErrorReflection'
1284directive :: SyntaxInfo -> IdrisParser [PDecl]
1285directive syn = do try (lchar '%' *> reserved "lib")
1286 cgn <- codegen_
1287 lib <- fmap fst stringLiteral
1288 return [PDirective (DLib cgn lib)]
1289 <|> do try (lchar '%' *> reserved "link")
1290 cgn <- codegen_; obj <- fst <$> stringLiteral
1291 return [PDirective (DLink cgn obj)]
1292 <|> do try (lchar '%' *> reserved "flag")
1293 cgn <- codegen_; flag <- fst <$> stringLiteral
1294 return [PDirective (DFlag cgn flag)]
1295 <|> do try (lchar '%' *> reserved "include")
1296 cgn <- codegen_
1297 hdr <- fst <$> stringLiteral
1298 return [PDirective (DInclude cgn hdr)]
1299 <|> do try (lchar '%' *> reserved "hide"); n <- fst <$> fnName
1300 return [PDirective (DHide n)]
1301 <|> do try (lchar '%' *> reserved "freeze"); n <- fst <$> iName []
1302 return [PDirective (DFreeze n)]
1303 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1304 return [PDirective (DAccess acc)]
1305 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1306 i <- get
1307 put (i { default_total = tot } )
1308 return [PDirective (DDefault tot)]
1309 <|> do try (lchar '%' *> reserved "logging")
1310 i <- fst <$> natural
1311 return [PDirective (DLogging i)]
1312 <|> do try (lchar '%' *> reserved "dynamic")
1313 libs <- sepBy1 (fmap fst stringLiteral) (lchar ',')
1314 return [PDirective (DDynamicLibs libs)]
1315 <|> do try (lchar '%' *> reserved "name")
1316 (ty, tyFC) <- fnName
1317 ns <- sepBy1 name (lchar ',')
1318 return [PDirective (DNameHint ty tyFC ns)]
1319 <|> do try (lchar '%' *> reserved "error_handlers")
1320 (fn, nfc) <- fnName
1321 (arg, afc) <- fnName
1322 ns <- sepBy1 name (lchar ',')
1323 return [PDirective (DErrorHandlers fn nfc arg afc ns) ]
1324 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1325 return [PDirective (DLanguage ext)]
1326 <|> do try (lchar '%' *> reserved "deprecate")
1327 n <- fst <$> fnName
1328 alt <- option "" (fst <$> stringLiteral)
1329 return [PDirective (DDeprecate n alt)]
1330 <|> do fc <- getFC
1331 try (lchar '%' *> reserved "used")
1332 fn <- fst <$> fnName
1333 arg <- fst <$> iName []
1334 return [PDirective (DUsed fc fn arg)]
1335 <?> "directive"
1337pLangExt :: IdrisParser LanguageExt
1338pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1339 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1341{- | Parses a totality
1344Totality ::= 'partial' | 'total'
1348totality :: IdrisParser Bool
1349totality
1350 = do reservedHL "total"; return True
1351 <|> do reservedHL "partial"; return False
1353{- | Parses a type provider
1356Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1357ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1359 -}
1360provider :: SyntaxInfo -> IdrisParser [PDecl]
1361provider syn = do doc <- try (do (doc, _) <- docstring syn
1362 fc1 <- getFC
1363 lchar '%'
1364 fc2 <- reservedFC "provide"
1365 highlightP (spanFC fc1 fc2) AnnKeyword
1366 return doc)
1367 provideTerm doc <|> providePostulate doc
1368 <?> "type provider"
1369 where provideTerm doc =
1370 do lchar '('; (n, nfc) <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1371 fc <- getFC
1372 reservedHL "with"
1373 e <- expr syn <?> "provider expression"
1374 return [PProvider doc syn fc nfc (ProvTerm t e) n]
1375 providePostulate doc =
1376 do reservedHL "postulate"
1377 (n, nfc) <- fnName
1378 fc <- getFC
1379 reservedHL "with"
1380 e <- expr syn <?> "provider expression"
1381 return [PProvider doc syn fc nfc (ProvPostulate e) n]
1383{- | Parses a transform
1386Transform ::= '%' 'transform' Expr '==>' Expr
1389transform :: SyntaxInfo -> IdrisParser [PDecl]
1390transform syn = do try (lchar '%' *> reserved "transform")
1391 -- leave it unchecked, until we work out what this should
1392 -- actually mean...
1393-- safety <- option True (do reserved "unsafe"
1394-- return False)
1395 l <- expr syn
1396 fc <- getFC
1397 symbol "==>"
1398 r <- expr syn
1399 return [PTransform fc False l r]
1400 <?> "transform"
1402{- | Parses a top-level reflected elaborator script
1405RunElabDecl ::= '%' 'runElab' Expr
1408runElabDecl :: SyntaxInfo -> IdrisParser PDecl
1409runElabDecl syn =
1410 do kwFC <- try (do fc <- getFC
1411 lchar '%'
1412 fc' <- reservedFC "runElab"
1413 return (spanFC fc fc'))
1414 script <- expr syn <?> "elaborator script"
1415 highlightP kwFC AnnKeyword
1416 return $ PRunElabDecl kwFC script (syn_namespace syn)
1417 <?> "top-level elaborator script"
1419{- * Loading and parsing -}
1420{- | Parses an expression from input -}
1421parseExpr :: IState -> String -> Result PTerm
1422parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1424{- | Parses a constant form input -}
1425parseConst :: IState -> String -> Result Const
1426parseConst st = runparser (fmap fst constant) st "(input)"
1428{- | Parses a tactic from input -}
1429parseTactic :: IState -> String -> Result PTactic
1430parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1432{- | Parses a do-step from input (used in the elab shell) -}
1433parseElabShellStep :: IState -> String -> Result (Either ElabShellCmd PDo)
1434parseElabShellStep ist = runparser (fmap Right (do_ defaultSyntax) <|> fmap Left elabShellCmd) ist "(input)"
1435 where elabShellCmd = char ':' >>
1436 (reserved "qed" >> pure EQED ) <|>
1437 (reserved "abandon" >> pure EAbandon ) <|>
1438 (reserved "undo" >> pure EUndo ) <|>
1439 (reserved "state" >> pure EProofState) <|>
1440 (reserved "term" >> pure EProofTerm ) <|>
1441 (expressionTactic ["e", "eval"] EEval ) <|>
1442 (expressionTactic ["t", "type"] ECheck) <|>
1443 (expressionTactic ["search"] ESearch ) <|>
1444 (do reserved "doc"
1445 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)
1446 eof
1447 return (EDocStr doc))
1448 <?> "elab command"
1449 expressionTactic cmds tactic =
1450 do asum (map reserved cmds)
1451 t <- spaced (expr defaultSyntax)
1452 i <- get
1453 return $ tactic (desugar defaultSyntax i t)
1454 spaced parser = indentPropHolds gtProp *> parser
1456-- | Parse module header and imports
1457parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Delta)
1458parseImports fname input
1459 = do i <- getIState
1460 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1461 Failure err -> fail (show err)
1462 Success (x, annots, i) ->
1463 do putIState i
1464 fname' <- runIO $ Dir.makeAbsolute fname
1465 sendHighlighting $ addPath annots fname'
1466 return x
1467 where imports :: IdrisParser ((Maybe (Docstring ()), [String],
1468 [ImportInfo],
1469 Maybe Delta),
1470 [(FC, OutputAnnotation)], IState)
1471 imports = do whiteSpace
1472 (mdoc, mname, annots) <- moduleHeader
1473 ps <- many import_
1474 mrk <- mark
1475 isEof <- lookAheadMatches eof
1476 let mrk' = if isEof
1477 then Nothing
1478 else Just mrk
1479 i <- get
1480 return ((mdoc, mname, ps, mrk'), annots, i)
1481 addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]
1482 addPath [] _ = []
1483 addPath ((fc, AnnNamespace ns Nothing) : annots) path =
1484 (fc, AnnNamespace ns (Just path)) : addPath annots path
1485 addPath (annot:annots) path = annot : addPath annots path
1487-- | There should be a better way of doing this...
1488findFC :: Doc -> (FC, String)
1489findFC x = let s = show (plain x) in findFC' s
1490 where findFC' s = case span (/= ':') s of
1491 -- Horrid kludge to prevent crashes on Windows
1492 (prefix, ':':'\\':rest) ->
1493 case findFC' rest of
1494 (NoFC, msg) -> (NoFC, msg)
1495 (FileFC f, msg) -> (FileFC (prefix ++ ":\\" ++ f), msg)
1496 (FC f start end, msg) -> (FC (prefix ++ ":\\" ++ f) start end, msg)
1497 (failname, ':':rest) -> case span isDigit rest of
1498 (line, ':':rest') -> case span isDigit rest' of
1499 (col, ':':msg) -> let pos = (read line, read col) in
1500 (FC failname pos pos, msg)
1502-- | Check if the coloring matches the options and corrects if necessary
1503fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1504fixColour False doc = ANSI.plain doc
1505fixColour True doc = doc
1507-- | A program is a list of declarations, possibly with associated
1508-- documentation strings.
1509parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1510 Idris [PDecl]
1511parseProg syn fname input mrk
1512 = do i <- getIState
1513 case runparser mainProg i fname input of
1514 Failure doc -> do -- FIXME: Get error location from trifecta
1515 -- this can't be the solution!
1516 -- Issue #1575 on the issue tracker.
1517 -- https://github.com/idris-lang/Idris-dev/issues/1575
1518 let (fc, msg) = findFC doc
1519 i <- getIState
1520 case idris_outputmode i of
1521 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1522 IdeMode n h -> iWarn fc (P.text msg)
1523 putIState (i { errSpan = Just fc })
1524 return []
1525 Success (x, i) -> do putIState i
1526 reportParserWarnings
1527 return $ collect x
1528 where mainProg :: IdrisParser ([PDecl], IState)
1529 mainProg = case mrk of
1530 Nothing -> do i <- get; return ([], i)
1531 Just mrk -> do
1532 release mrk
1533 ds <- prog syn
1534 i' <- get
1535 return (ds, i')
1537{- | Load idris module and show error if something wrong happens -}
1538loadModule :: FilePath -> Idris (Maybe String)
1539loadModule f
1540 = idrisCatch (loadModule' f)
1541 (\e -> do setErrSpan (getErrSpan e)
1542 ist <- getIState
1543 iWarn (getErrSpan e) $ pprintErr ist e
1544 return Nothing)
1546{- | Load idris module -}
1547loadModule' :: FilePath -> Idris (Maybe String)
1548loadModule' f
1549 = do i <- getIState
1550 let file = takeWhile (/= ' ') f
1551 ibcsd <- valIBCSubDir i
1552 ids <- allImportDirs
1553 fp <- findImport ids ibcsd file
1554 if file `elem` imported i
1555 then do logLvl 1 $ "Already read " ++ file
1556 return Nothing
1557 else do putIState (i { imported = file : imported i })
1558 case fp of
1559 IDR fn -> loadSource False fn Nothing
1560 LIDR fn -> loadSource True fn Nothing
1561 IBC fn src ->
1562 idrisCatch (loadIBC True fn)
1563 (\c -> do logLvl 1 $ fn ++ " failed " ++ pshow i c
1564 case src of
1565 IDR sfn -> loadSource False sfn Nothing
1566 LIDR sfn -> loadSource True sfn Nothing)
1567 return $ Just file
1569{- | Load idris code from file -}
1570loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()
1571loadFromIFile reexp i@(IBC fn src) maxline
1572 = do logLvl 1 $ "Skipping " ++ getSrcFile i
1573 idrisCatch (loadIBC reexp fn)
1574 (\err -> ierror $ LoadingFailed fn err)
1575 where
1576 getSrcFile (IDR fn) = fn
1577 getSrcFile (LIDR fn) = fn
1578 getSrcFile (IBC f src) = getSrcFile src
1580loadFromIFile _ (IDR fn) maxline = loadSource' False fn maxline
1581loadFromIFile _ (LIDR fn) maxline = loadSource' True fn maxline
1583{-| Load idris source code and show error if something wrong happens -}
1584loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1585loadSource' lidr r maxline
1586 = idrisCatch (loadSource lidr r maxline)
1587 (\e -> do setErrSpan (getErrSpan e)
1588 ist <- getIState
1589 case e of
1590 At f e' -> iWarn f (pprintErr ist e')
1591 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1593{- | Load Idris source code-}
1594loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1595loadSource lidr f toline
1596 = do logLvl 1 ("Reading " ++ f)
1597 i <- getIState
1598 let def_total = default_total i
1599 file_in <- runIO $ readSource f
1600 file <- if lidr then tclift $ unlit f file_in else return file_in
1601 (mdocs, mname, imports_in, pos) <- parseImports f file
1602 ai <- getAutoImports
1603 let imports = map (\n -> ImportInfo True n Nothing [] NoFC NoFC) ai ++ imports_in
1604 ids <- allImportDirs
1605 ibcsd <- valIBCSubDir i
1606 mapM_ (\(re, f, ns, nfc) ->
1607 do fp <- findImport ids ibcsd f
1608 case fp of
1609 LIDR fn -> ifail $ "No ibc for " ++ f
1610 IDR fn -> ifail $ "No ibc for " ++ f
1611 IBC fn src ->
1612 do loadIBC True fn
1613 let srcFn = case src of
1614 IDR fn -> Just fn
1615 LIDR fn -> Just fn
1616 _ -> Nothing
1617 srcFnAbs <- case srcFn of
1618 Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)
1619 Nothing -> return Nothing
1620 sendHighlighting [(nfc, AnnNamespace ns srcFnAbs)])
1621 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]
1622 reportParserWarnings
1623 sendParserHighlighting
1625 -- process and check module aliases
1626 let modAliases = M.fromList
1627 [ (prep alias, prep realName)
1628 | ImportInfo { import_reexport = reexport
1629 , import_path = realName
1630 , import_rename = Just (alias, _)
1631 , import_location = fc } <- imports
1633 prep = map T.pack . reverse . Spl.splitOn [pathSeparator]
1634 aliasNames = [ (alias, fc)
1635 | ImportInfo { import_rename = Just (alias, _)
1636 , import_location = fc } <- imports
1638 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1639 case map head . filter ((/= 1) . length) $ histogram of
1640 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1641 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1643 i <- getIState
1644 putIState (i { default_access = Hidden, module_aliases = modAliases })
1645 clearIBC -- start a new .ibc file
1646 -- record package info in .ibc
1647 imps <- allImportDirs
1648 mapM_ addIBC (map IBCImportDir imps)
1649 mapM_ (addIBC . IBCImport)
1650 [ (reexport, realName)
1651 | ImportInfo { import_reexport = reexport
1652 , import_path = realName
1653 } <- imports
1655 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1656 maxline = toline }
1657 ist <- getIState
1658 -- Save the span from parsing the module header, because
1659 -- an empty program parse might obliterate it.
1660 let oldSpan = idris_parsedSpan ist
1661 ds' <- parseProg syntax f file pos
1663 case (ds', oldSpan) of
1664 ([], Just fc) ->
1665 -- If no program elements were parsed, we dind't
1666 -- get a loaded region in the IBC file. That
1667 -- means we need to add it back.
1668 do ist <- getIState
1669 putIState ist { idris_parsedSpan = oldSpan
1670 , ibc_write = IBCParsedRegion fc :
1671 ibc_write ist
1673 _ -> return ()
1674 sendParserHighlighting
1676 -- Parsing done, now process declarations
1678 let ds = namespaces mname ds'
1679 logLvl 3 (show $ showDecls verbosePPOption ds)
1680 i <- getIState
1681 logLvl 10 (show (toAlist (idris_implicits i)))
1682 logLvl 3 (show (idris_infixes i))
1683 -- Now add all the declarations to the context
1684 v <- verbose
1685 when v $ iputStrLn $ "Type checking " ++ f
1686 -- we totality check after every Mutual block, so if
1687 -- anything is a single definition, wrap it in a
1688 -- mutual block on its own
1689 elabDecls toplevel (map toMutual ds)
1690 i <- getIState
1691 -- simplify every definition do give the totality checker
1692 -- a better chance
1693 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1694 ctxt' <-
1695 do ctxt <- getContext
1696 tclift $ simplifyCasedef n (getErasureInfo i) ctxt
1697 setContext ctxt')
1698 (map snd (idris_totcheck i))
1699 -- build size change graph from simplified definitions
1700 logLvl 1 "Totality checking"
1701 i <- getIState
1702 mapM_ buildSCG (idris_totcheck i)
1703 mapM_ checkDeclTotality (idris_totcheck i)
1705 -- Redo totality check for deferred names
1706 let deftots = idris_defertotcheck i
1707 logLvl 1 $ "Totality checking " ++ show deftots
1708 mapM_ (\x -> do tot <- getTotality x
1709 case tot of
1710 Total _ -> setTotality x Unchecked
1711 _ -> return ()) (map snd deftots)
1712 mapM_ buildSCG deftots
1713 mapM_ checkDeclTotality deftots
1715 logLvl 1 ("Finished " ++ f)
1716 ibcsd <- valIBCSubDir i
1717 logLvl 1 "Universe checking"
1718 iucheck
1719 let ibc = ibcPathNoFallback ibcsd f
1720 i <- getIState
1721 addHides (hide_list i)
1723 -- Save module documentation if applicable
1724 i <- getIState
1725 case mdocs of
1726 Nothing -> return ()
1727 Just docs -> addModDoc syntax mname docs
1730 -- Finally, write an ibc and highlights if checking was successful
1731 ok <- noErrors
1732 when ok $
1733 do idrisCatch (do writeIBC f ibc; clearIBC)
1734 (\c -> return ()) -- failure is harmless
1735 hl <- getDumpHighlighting
1736 when hl $
1737 idrisCatch (writeHighlights f)
1738 (const $ return ()) -- failure is harmless
1739 clearHighlights
1740 i <- getIState
1741 putIState (i { default_total = def_total,
1742 hide_list = [] })
1743 return ()
1744 where
1745 namespaces :: [String] -> [PDecl] -> [PDecl]
1746 namespaces [] ds = ds
1747 namespaces (x:xs) ds = [PNamespace x NoFC (namespaces xs ds)]
1749 toMutual :: PDecl -> PDecl
1750 toMutual m@(PMutual _ d) = m
1751 toMutual (PNamespace x fc ds) = PNamespace x fc (map toMutual ds)
1752 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1753 case x of
1754 PClauses{} -> r
1755 PClass{} -> r
1756 PData{} -> r
1757 PInstance{} -> r
1758 _ -> x
1760 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1761 addModDoc syn mname docs =
1762 do ist <- getIState
1763 docs' <- elabDocTerms recinfo (parsedDocs ist)
1764 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1765 putIState ist { idris_moduledocs = modDocs' }
1766 addIBC (IBCModDocs docName)
1767 where
1768 docName = NS modDocName (map T.pack (reverse mname))
1769 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1771{- | Adds names to hide list -}
1772addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1773addHides xs = do i <- getIState
1774 let defh = default_access i
1775 let (hs, as) = partition isNothing xs
1776 unless (null as) $
1777 mapM_ doHide
1778 (map (\ (n, _) -> (n, defh)) hs ++
1779 map (\ (n, Just a) -> (n, a)) as)
1780 where isNothing (_, Nothing) = True
1781 isNothing _ = False
1783 doHide (n, a) = do setAccessibility n a
1784 addIBC (IBCAccess n a)