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