git.iko.soy/Idris-dev
on 0cb9b4e help sign in
Idris-dev/src/Idris/Parser.hs
1824 lines 70 kB history raw
1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
2{-# OPTIONS_GHC -O0 #-}
3module Idris.Parser(module Idris.Parser,
4 module Idris.Parser.Expr,
5 module Idris.Parser.Data,
6 module Idris.Parser.Helpers,
7 module Idris.Parser.Ops) 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.Parser.Helpers
39import Idris.Parser.Ops
40import Idris.Parser.Expr
41import Idris.Parser.Data
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 acc opts cn fc' ps ity ni ds)
341 = PInstance docs pdocs s fc cs acc opts (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)
506 (fixBind rens argTy)
507 (fixBind rens body)
508 | otherwise =
509 do ty' <- fixBind rens argTy
510 n' <- gensym n
511 body' <- fixBind ((n,n'):rens) body
512 return $ (PPi plic n' nfc ty' body')
513 fixBind rens (PLet fc n nfc ty val body)
514 | n `elem` userNames = liftM3 (PLet fc n nfc)
515 (fixBind rens ty)
516 (fixBind rens val)
517 (fixBind rens body)
518 | otherwise =
519 do ty' <- fixBind rens ty
520 val' <- fixBind rens val
521 n' <- gensym n
522 body' <- fixBind ((n,n'):rens) body
523 return $ PLet fc n' nfc ty' val' body'
524 fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =
525 return $ PMatchApp fc n'
526 -- Also rename resolved quotations, to allow syntax rules to
527 -- have quoted references to their own bindings.
528 fixBind rens (PQuoteName n True fc) | Just n' <- lookup n rens =
529 return $ PQuoteName n' True fc
530 fixBind rens x = descendM (fixBind rens) x
532 gensym :: Name -> IdrisParser Name
533 gensym n = do ist <- get
534 let idx = idris_name ist
535 put ist { idris_name = idx + 1 }
536 return $ sMN idx (show n)
538{- | Parses a syntax symbol (either binding variable, keyword or expression)
541SyntaxSym ::= '[' Name_t ']'
542 | '{' Name_t '}'
543 | Name_t
544 | StringLiteral_t
545 ;
547 -}
548syntaxSym :: IdrisParser SSymbol
549syntaxSym = try (do lchar '['; n <- fst <$> name; lchar ']'
550 return (Expr n))
551 <|> try (do lchar '{'; n <- fst <$> name; lchar '}'
552 return (Binding n))
553 <|> do n <- fst <$> iName []
554 return (Keyword n)
555 <|> do sym <- fmap fst stringLiteral
556 return (Symbol sym)
557 <?> "syntax symbol"
559{- | Parses a function declaration with possible syntax sugar
562 FunDecl ::= FunDecl';
564-}
565fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
566fnDecl syn = try (do notEndBlock
567 d <- fnDecl' syn
568 i <- get
569 let d' = fmap (desugar syn i) d
570 return [d']) <?> "function declaration"
572{-| Parses a function declaration
575 FunDecl' ::=
576 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
577 | Postulate
578 | Pattern
579 | CAF
580 ;
582-}
583fnDecl' :: SyntaxInfo -> IdrisParser PDecl
584fnDecl' syn = checkFixity $
585 do (doc, argDocs, fc, opts', n, nfc, acc) <- try (do
586 pushIndent
587 (doc, argDocs) <- docstring syn
588 ist <- get
589 let initOpts = if default_total ist
590 then [TotalFn]
591 else []
592 opts <- fnOpts initOpts
593 acc <- accessibility
594 opts' <- fnOpts opts
595 (n_in, nfc) <- fnName
596 let n = expandNS syn n_in
597 fc <- getFC
598 lchar ':'
599 return (doc, argDocs, fc, opts', n, nfc, acc))
600 ty <- typeExpr (allowImp syn)
601 terminator
602 addAcc n acc
603 return (PTy doc argDocs syn fc opts' n nfc ty)
604 <|> postulate syn
605 <|> caf syn
606 <|> pattern syn
607 <?> "function declaration"
608 where checkFixity :: IdrisParser PDecl -> IdrisParser PDecl
609 checkFixity p = do decl <- p
610 case getName decl of
611 Nothing -> return decl
612 Just n -> do fOk <- fixityOK n
613 unless fOk . fail $
614 "Missing fixity declaration for " ++ show n
615 return decl
616 getName (PTy _ _ _ _ _ n _ _) = Just n
617 getName _ = Nothing
618 fixityOK (NS n _) = fixityOK n
619 fixityOK (UN n) | all (flip elem opChars) (str n) =
620 do fixities <- fmap idris_infixes get
621 return . elem (str n) . map (\ (Fix _ op) -> op) $ fixities
622 | otherwise = return True
623 fixityOK _ = return True
625{-| Parses function options given initial options
628FnOpts ::= 'total'
629 | 'partial'
630 | 'covering'
631 | 'implicit'
632 | '%' 'no_implicit'
633 | '%' 'assert_total'
634 | '%' 'error_handler'
635 | '%' 'reflection'
636 | '%' 'specialise' '[' NameTimesList? ']'
637 ;
641NameTimes ::= FnName Natural?;
645NameTimesList ::=
646 NameTimes
647 | NameTimes ',' NameTimesList
648 ;
650-}
651-- FIXME: Check compatability for function options (i.e. partal/total)
652--
653-- Issue #1574 on the issue tracker.
654-- https://github.com/idris-lang/Idris-dev/issues/1574
655fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
656fnOpts opts
657 = do reservedHL "total"; fnOpts (TotalFn : opts)
658 <|> do reservedHL "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
659 <|> do reservedHL "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))
660 <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;
661 fnOpts (CExport c : opts)
662 <|> do try (lchar '%' *> reserved "no_implicit");
663 fnOpts (NoImplicit : opts)
664 <|> do try (lchar '%' *> reserved "inline");
665 fnOpts (Inlinable : opts)
666 <|> do try (lchar '%' *> reserved "assert_total");
667 fnOpts (AssertTotal : opts)
668 <|> do try (lchar '%' *> reserved "error_handler");
669 fnOpts (ErrorHandler : opts)
670 <|> do try (lchar '%' *> reserved "error_reverse");
671 fnOpts (ErrorReverse : opts)
672 <|> do try (lchar '%' *> reserved "reflection");
673 fnOpts (Reflection : opts)
674 <|> do try (lchar '%' *> reserved "hint");
675 fnOpts (AutoHint : opts)
676 <|> do lchar '%'; reserved "specialise";
677 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
678 fnOpts (Specialise ns : opts)
679 <|> do reservedHL "implicit"; fnOpts (Implicit : opts)
680 <|> return opts
681 <?> "function modifier"
682 where nameTimes :: IdrisParser (Name, Maybe Int)
683 nameTimes = do n <- fst <$> fnName
684 t <- option Nothing (do reds <- fmap fst natural
685 return (Just (fromInteger reds)))
686 return (n, t)
688{- | Parses a postulate
691Postulate ::=
692 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
693 ;
695-}
696postulate :: SyntaxInfo -> IdrisParser PDecl
697postulate syn = do (doc, ext)
698 <- try $ do (doc, _) <- docstring syn
699 pushIndent
700 ext <- ppostDecl
701 return (doc, ext)
702 ist <- get
703 let initOpts = if default_total ist
704 then [TotalFn]
705 else []
706 opts <- fnOpts initOpts
707 acc <- accessibility
708 opts' <- fnOpts opts
709 (n_in, nfc) <- fnName
710 let n = expandNS syn n_in
711 lchar ':'
712 ty <- typeExpr (allowImp syn)
713 fc <- getFC
714 terminator
715 addAcc n acc
716 return (PPostulate ext doc syn fc nfc opts' n ty)
717 <?> "postulate"
718 where ppostDecl = do fc <- reservedHL "postulate"; return False
719 <|> do lchar '%'; reserved "extern"; return True
720{- | Parses a using declaration
723Using ::=
724 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
725 ;
727 -}
728using_ :: SyntaxInfo -> IdrisParser [PDecl]
729using_ syn =
730 do reservedHL "using"
731 lchar '('; ns <- usingDeclList syn; lchar ')'
732 openBlock
733 let uvars = using syn
734 ds <- many (decl (syn { using = uvars ++ ns }))
735 closeBlock
736 return (concat ds)
737 <?> "using declaration"
739{- | Parses a parameters declaration
742Params ::=
743 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
744 ;
746 -}
747params :: SyntaxInfo -> IdrisParser [PDecl]
748params syn =
749 do reservedHL "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
750 let ns' = [(n, ty) | (n, _, ty) <- ns]
751 openBlock
752 let pvars = syn_params syn
753 ds <- many (decl syn { syn_params = pvars ++ ns' })
754 closeBlock
755 fc <- getFC
756 return [PParams fc ns' (concat ds)]
757 <?> "parameters declaration"
759{- | Parses a mutual declaration (for mutually recursive functions)
762Mutual ::=
763 'mutual' OpenBlock Decl* CloseBlock
764 ;
766-}
767mutual :: SyntaxInfo -> IdrisParser [PDecl]
768mutual syn =
769 do reservedHL "mutual"
770 openBlock
771 let pvars = syn_params syn
772 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
773 closeBlock
774 fc <- getFC
775 return [PMutual fc (concat ds)]
776 <?> "mutual block"
778{-| Parses a namespace declaration
781Namespace ::=
782 'namespace' identifier OpenBlock Decl+ CloseBlock
783 ;
785-}
786namespace :: SyntaxInfo -> IdrisParser [PDecl]
787namespace syn =
788 do reservedHL "namespace"
789 (n, nfc) <- identifier
790 openBlock
791 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
792 closeBlock
793 return [PNamespace n nfc (concat ds)]
794 <?> "namespace declaration"
796{- | Parses a methods block (for instances)
799 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
801-}
802instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
803instanceBlock syn = do reservedHL "where"
804 openBlock
805 ds <- many (fnDecl syn)
806 closeBlock
807 return (concat ds)
808 <?> "implementation block"
810{- | Parses a methods and instances block (for type classes)
813MethodOrInstance ::=
814 FnDecl
815 | Instance
816 ;
820ClassBlock ::=
821 'where' OpenBlock Constructor? MethodOrInstance* CloseBlock
822 ;
824-}
825classBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])
826classBlock syn = do reservedHL "where"
827 openBlock
828 (cn, cd) <- option (Nothing, emptyDocstring) $
829 try (do (doc, _) <- option noDocs docComment
830 n <- constructor
831 return (Just n, doc))
832 ist <- get
833 let cd' = annotate syn ist cd
835 ds <- many (notEndBlock >> try (instance_ True syn) <|> fnDecl syn)
836 closeBlock
837 return (cn, cd', concat ds)
838 <?> "class block"
840 where
841 constructor :: IdrisParser (Name, FC)
842 constructor = reservedHL "constructor" *> fnName
844 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)
845 annotate syn ist = annotCode $ tryFullExpr syn ist
847{-| Parses a type class declaration
850ClassArgument ::=
851 Name
852 | '(' Name ':' Expr ')'
853 ;
857Class ::=
858 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
859 ;
861-}
862class_ :: SyntaxInfo -> IdrisParser [PDecl]
863class_ syn = do (doc, argDocs, acc)
864 <- try (do (doc, argDocs) <- docstring syn
865 acc <- accessibility
866 classKeyword
867 return (doc, argDocs, acc))
868 fc <- getFC
869 cons <- constraintList syn
870 let cons' = [(c, ty) | (c, _, ty) <- cons]
871 (n_in, nfc) <- fnName
872 let n = expandNS syn n_in
873 cs <- many carg
874 fds <- option [(cn, NoFC) | (cn, _, _) <- cs] fundeps
875 (cn, cd, ds) <- option (Nothing, fst noDocs, []) (classBlock syn)
876 accData acc n (concatMap declared ds)
877 return [PClass doc syn fc cons' n nfc cs argDocs fds ds cn cd]
878 <?> "type-class declaration"
879 where
880 fundeps :: IdrisParser [(Name, FC)]
881 fundeps = do lchar '|'; sepBy name (lchar ',')
883 classKeyword :: IdrisParser ()
884 classKeyword = reservedHL "interface"
885 <|> do reservedHL "class"
886 fc <- getFC
887 parserWarning fc Nothing (Msg "The 'class' keyword is deprecated. Use 'interface' instead.")
889 carg :: IdrisParser (Name, FC, PTerm)
890 carg = do lchar '('; (i, ifc) <- name; lchar ':'; ty <- expr syn; lchar ')'
891 return (i, ifc, ty)
892 <|> do (i, ifc) <- name
893 fc <- getFC
894 return (i, ifc, PType fc)
896{- | Parses a type class instance declaration
899 Instance ::=
900 DocComment_t? 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
901 ;
905InstanceName ::= '[' Name ']';
907-}
908instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl]
909instance_ kwopt syn
910 = do ist <- get
911 let initOpts = if default_total ist
912 then [TotalFn]
913 else []
915 (doc, argDocs) <- docstring syn
916 opts <- fnOpts initOpts
917 acc <- accessibility
918 opts' <- fnOpts opts
920 if kwopt then optional instanceKeyword
921 else do instanceKeyword
922 return (Just ())
924 fc <- getFC
925 en <- optional instanceName
926 cs <- constraintList syn
927 let cs' = [(c, ty) | (c, _, ty) <- cs]
928 (cn, cnfc) <- fnName
929 args <- many (simpleExpr syn)
930 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)
931 let t = bindList (PPi constraint) cs sc
932 ds <- instanceBlock syn
933 return [PInstance doc argDocs syn fc cs' acc opts' cn cnfc args t en ds]
934 <?> "implementation declaration"
935 where instanceName :: IdrisParser Name
936 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'
937 let n = expandNS syn n_in
938 return n
939 <?> "implementation name"
940 instanceKeyword :: IdrisParser ()
941 instanceKeyword = reservedHL "implementation"
942 <|> do reservedHL "instance"
943 fc <- getFC
944 parserWarning fc Nothing (Msg "The 'instance' keyword is deprecated. Use 'implementation' (or omit it) instead.")
946-- | Parse a docstring
947docstring :: SyntaxInfo
948 -> IdrisParser (Docstring (Either Err PTerm),
949 [(Name,Docstring (Either Err PTerm))])
950docstring syn = do (doc, argDocs) <- option noDocs docComment
951 ist <- get
952 let doc' = annotCode (tryFullExpr syn ist) doc
953 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
954 | (n, d) <- argDocs ]
955 return (doc', argDocs')
958{- | Parses a using declaration list
961UsingDeclList ::=
962 UsingDeclList'
963 | NameList TypeSig
964 ;
968UsingDeclList' ::=
969 UsingDecl
970 | UsingDecl ',' UsingDeclList'
971 ;
975NameList ::=
976 Name
977 | Name ',' NameList
978 ;
980-}
981usingDeclList :: SyntaxInfo -> IdrisParser [Using]
982usingDeclList syn
983 = try (sepBy1 (usingDecl syn) (lchar ','))
984 <|> do ns <- sepBy1 (fst <$> name) (lchar ',')
985 lchar ':'
986 t <- typeExpr (disallowImp syn)
987 return (map (\x -> UImplicit x t) ns)
988 <?> "using declaration list"
990{- |Parses a using declaration
993UsingDecl ::=
994 FnName TypeSig
995 | FnName FnName+
996 ;
998-}
999usingDecl :: SyntaxInfo -> IdrisParser Using
1000usingDecl syn = try (do x <- fst <$> fnName
1001 lchar ':'
1002 t <- typeExpr (disallowImp syn)
1003 return (UImplicit x t))
1004 <|> do c <- fst <$> fnName
1005 xs <- some (fst <$> fnName)
1006 return (UConstraint c xs)
1007 <?> "using declaration"
1009{- | Parse a clause with patterns
1012Pattern ::= Clause;
1015pattern :: SyntaxInfo -> IdrisParser PDecl
1016pattern syn = do fc <- getFC
1017 clause <- clause syn
1018 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
1019 <?> "pattern"
1021{- | Parse a constant applicative form declaration
1024CAF ::= 'let' FnName '=' Expr Terminator;
1027caf :: SyntaxInfo -> IdrisParser PDecl
1028caf syn = do reservedHL "let"
1029 n_in <- fst <$> fnName; let n = expandNS syn n_in
1030 pushIndent
1031 lchar '='
1032 t <- indented $ expr syn
1033 terminator
1034 fc <- getFC
1035 return (PCAF fc n t)
1036 <?> "constant applicative form declaration"
1038{- | Parse an argument expression
1041ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
1044argExpr :: SyntaxInfo -> IdrisParser PTerm
1045argExpr syn = let syn' = syn { inPattern = True } in
1046 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
1047 <?> "argument expression"
1049{- | Parse a right hand side of a function
1052RHS ::= '=' Expr
1053 | '?=' RHSName? Expr
1054 | Impossible
1059RHSName ::= '{' FnName '}';
1062rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
1063rhs syn n = do lchar '='; expr syn
1064 <|> do symbol "?=";
1065 fc <- getFC
1066 name <- option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";
1067 return n)
1068 r <- expr syn
1069 return (addLet fc name r)
1070 <|> impossible
1071 <?> "function right hand side"
1072 where mkN :: Name -> Name
1073 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
1074 then sUN "infix_op_lemma_1"
1075 else sUN (str x++"_lemma_1")
1076 mkN (NS x n) = NS (mkN x) n
1077 n' :: Name
1078 n' = mkN n
1079 addLet :: FC -> Name -> PTerm -> PTerm
1080 addLet fc nm (PLet fc' n nfc ty val r) = PLet fc' n nfc ty val (addLet fc nm r)
1081 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
1082 where addLetC (l, r) = (l, addLet fc nm r)
1083 addLet fc nm r = (PLet fc (sUN "value") NoFC Placeholder r (PMetavar NoFC nm))
1085{- |Parses a function clause
1088RHSOrWithBlock ::= RHS WhereOrTerminator
1089 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
1094Clause ::= WExpr+ RHSOrWithBlock
1095 | SimpleExpr '<==' FnName RHS WhereOrTerminator
1096 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
1097 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
1102ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
1106WhereOrTerminator ::= WhereBlock | Terminator;
1109clause :: SyntaxInfo -> IdrisParser PClause
1110clause syn
1111 = do wargs <- try (do pushIndent; some (wExpr syn))
1112 fc <- getFC
1113 ist <- get
1114 n <- case lastParse ist of
1115 Just t -> return t
1116 Nothing -> fail "Invalid clause"
1117 (do r <- rhs syn n
1118 let ctxt = tt_ctxt ist
1119 let wsyn = syn { syn_namespace = [] }
1120 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1121 popIndent
1122 return x,
1123 do terminator
1124 return ([], [])]
1125 return $ PClauseR fc wargs r wheres) <|> (do
1126 popIndent
1127 reservedHL "with"
1128 wval <- simpleExpr syn
1129 pn <- optProof
1130 openBlock
1131 ds <- some $ fnDecl syn
1132 let withs = concat ds
1133 closeBlock
1134 return $ PWithR fc wargs wval pn withs)
1135 <|> do ty <- try (do pushIndent
1136 ty <- simpleExpr syn
1137 symbol "<=="
1138 return ty)
1139 fc <- getFC
1140 n_in <- fst <$> fnName; let n = expandNS syn n_in
1141 r <- rhs syn n
1142 ist <- get
1143 let ctxt = tt_ctxt ist
1144 let wsyn = syn { syn_namespace = [] }
1145 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1146 popIndent
1147 return x,
1148 do terminator
1149 return ([], [])]
1150 let capp = PLet fc (sMN 0 "match") NoFC
1151 ty
1152 (PMatchApp fc n)
1153 (PRef fc [] (sMN 0 "match"))
1154 ist <- get
1155 put (ist { lastParse = Just n })
1156 return $ PClause fc n capp [] r wheres
1157 <|> do (l, op, nfc) <- try (do
1158 pushIndent
1159 l <- argExpr syn
1160 (op, nfc) <- operatorFC
1161 when (op == "=" || op == "?=" ) $
1162 fail "infix clause definition with \"=\" and \"?=\" not supported "
1163 return (l, op, nfc))
1164 let n = expandNS syn (sUN op)
1165 r <- argExpr syn
1166 fc <- getFC
1167 wargs <- many (wExpr syn)
1168 (do rs <- rhs syn n
1169 let wsyn = syn { syn_namespace = [] }
1170 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1171 popIndent
1172 return x,
1173 do terminator
1174 return ([], [])]
1175 ist <- get
1176 let capp = PApp fc (PRef nfc [nfc] n) [pexp l, pexp r]
1177 put (ist { lastParse = Just n })
1178 return $ PClause fc n capp wargs rs wheres) <|> (do
1179 popIndent
1180 reservedHL "with"
1181 wval <- bracketed syn
1182 pn <- optProof
1183 openBlock
1184 ds <- some $ fnDecl syn
1185 closeBlock
1186 ist <- get
1187 let capp = PApp fc (PRef fc [] n) [pexp l, pexp r]
1188 let withs = map (fillLHSD n capp wargs) $ concat ds
1189 put (ist { lastParse = Just n })
1190 return $ PWith fc n capp wargs wval pn withs)
1191 <|> do pushIndent
1192 (n_in, nfc) <- fnName; let n = expandNS syn n_in
1193 cargs <- many (constraintArg syn)
1194 fc <- getFC
1195 args <- many (try (implicitArg (syn { inPattern = True } ))
1196 <|> (fmap pexp (argExpr syn)))
1197 wargs <- many (wExpr syn)
1198 let capp = PApp fc (PRef nfc [nfc] n)
1199 (cargs ++ args)
1200 (do r <- rhs syn n
1201 ist <- get
1202 let ctxt = tt_ctxt ist
1203 let wsyn = syn { syn_namespace = [] }
1204 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1205 popIndent
1206 return x,
1207 do terminator
1208 return ([], [])]
1209 ist <- get
1210 put (ist { lastParse = Just n })
1211 return $ PClause fc n capp wargs r wheres) <|> (do
1212 reservedHL "with"
1213 ist <- get
1214 put (ist { lastParse = Just n })
1215 wval <- bracketed syn
1216 pn <- optProof
1217 openBlock
1218 ds <- some $ fnDecl syn
1219 let withs = map (fillLHSD n capp wargs) $ concat ds
1220 closeBlock
1221 popIndent
1222 return $ PWith fc n capp wargs wval pn withs)
1223 <?> "function clause"
1224 where
1225 optProof = option Nothing (do reservedHL "proof"
1226 n <- fnName
1227 return (Just n))
1229 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
1230 fillLHS n capp owargs (PClauseR fc wargs v ws)
1231 = PClause fc n capp (owargs ++ wargs) v ws
1232 fillLHS n capp owargs (PWithR fc wargs v pn ws)
1233 = PWith fc n capp (owargs ++ wargs) v pn
1234 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1235 fillLHS _ _ _ c = c
1237 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
1238 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1239 fillLHSD n c a x = x
1241{-| Parses with pattern
1244WExpr ::= '|' Expr';
1247wExpr :: SyntaxInfo -> IdrisParser PTerm
1248wExpr syn = do lchar '|'
1249 expr' (syn { inPattern = True })
1250 <?> "with pattern"
1252{- | Parses a where block
1255WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
1258whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
1259whereBlock n syn
1260 = do reservedHL "where"
1261 ds <- indentedBlock1 (decl syn)
1262 let dns = concatMap (concatMap declared) ds
1263 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1264 <?> "where block"
1266{- |Parses a code generation target language name
1269Codegen ::= 'C'
1270 | 'Java'
1271 | 'JavaScript'
1272 | 'Node'
1273 | 'LLVM'
1274 | 'Bytecode'
1278codegen_ :: IdrisParser Codegen
1279codegen_ = do n <- fst <$> identifier
1280 return (Via (map toLower n))
1281 <|> do reserved "Bytecode"; return Bytecode
1282 <?> "code generation language"
1284{- |Parses a compiler directive
1286StringList ::=
1287 String
1288 | String ',' StringList
1293Directive ::= '%' Directive';
1297Directive' ::= 'lib' CodeGen String_t
1298 | 'link' CodeGen String_t
1299 | 'flag' CodeGen String_t
1300 | 'include' CodeGen String_t
1301 | 'hide' Name
1302 | 'freeze' Name
1303 | 'access' Accessibility
1304 | 'default' Totality
1305 | 'logging' Natural
1306 | 'dynamic' StringList
1307 | 'name' Name NameList
1308 | 'error_handlers' Name NameList
1309 | 'language' 'TypeProviders'
1310 | 'language' 'ErrorReflection'
1314directive :: SyntaxInfo -> IdrisParser [PDecl]
1315directive syn = do try (lchar '%' *> reserved "lib")
1316 cgn <- codegen_
1317 lib <- fmap fst stringLiteral
1318 return [PDirective (DLib cgn lib)]
1319 <|> do try (lchar '%' *> reserved "link")
1320 cgn <- codegen_; obj <- fst <$> stringLiteral
1321 return [PDirective (DLink cgn obj)]
1322 <|> do try (lchar '%' *> reserved "flag")
1323 cgn <- codegen_; flag <- fst <$> stringLiteral
1324 return [PDirective (DFlag cgn flag)]
1325 <|> do try (lchar '%' *> reserved "include")
1326 cgn <- codegen_
1327 hdr <- fst <$> stringLiteral
1328 return [PDirective (DInclude cgn hdr)]
1329 <|> do try (lchar '%' *> reserved "hide"); n <- fst <$> fnName
1330 return [PDirective (DHide n)]
1331 <|> do try (lchar '%' *> reserved "freeze"); n <- fst <$> iName []
1332 return [PDirective (DFreeze n)]
1333 <|> do try (lchar '%' *> reserved "access")
1334 acc <- accessibility
1335 ist <- get
1336 put ist { default_access = acc }
1337 return [PDirective (DAccess acc)]
1338 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1339 i <- get
1340 put (i { default_total = tot } )
1341 return [PDirective (DDefault tot)]
1342 <|> do try (lchar '%' *> reserved "logging")
1343 i <- fst <$> natural
1344 return [PDirective (DLogging i)]
1345 <|> do try (lchar '%' *> reserved "dynamic")
1346 libs <- sepBy1 (fmap fst stringLiteral) (lchar ',')
1347 return [PDirective (DDynamicLibs libs)]
1348 <|> do try (lchar '%' *> reserved "name")
1349 (ty, tyFC) <- fnName
1350 ns <- sepBy1 name (lchar ',')
1351 return [PDirective (DNameHint ty tyFC ns)]
1352 <|> do try (lchar '%' *> reserved "error_handlers")
1353 (fn, nfc) <- fnName
1354 (arg, afc) <- fnName
1355 ns <- sepBy1 name (lchar ',')
1356 return [PDirective (DErrorHandlers fn nfc arg afc ns) ]
1357 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1358 return [PDirective (DLanguage ext)]
1359 <|> do try (lchar '%' *> reserved "deprecate")
1360 n <- fst <$> fnName
1361 alt <- option "" (fst <$> stringLiteral)
1362 return [PDirective (DDeprecate n alt)]
1363 <|> do fc <- getFC
1364 try (lchar '%' *> reserved "used")
1365 fn <- fst <$> fnName
1366 arg <- fst <$> iName []
1367 return [PDirective (DUsed fc fn arg)]
1368 <|> do try (lchar '%' *> reserved "auto_implicits")
1369 b <- on_off
1370 return [PDirective (DAutoImplicits b)]
1371 <?> "directive"
1372 where on_off = do reserved "on"; return True
1373 <|> do reserved "off"; return False
1375pLangExt :: IdrisParser LanguageExt
1376pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1377 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1379{- | Parses a totality
1382Totality ::= 'partial' | 'total'
1386totality :: IdrisParser Bool
1387totality
1388 = do reservedHL "total"; return True
1389 <|> do reservedHL "partial"; return False
1391{- | Parses a type provider
1394Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1395ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1397 -}
1398provider :: SyntaxInfo -> IdrisParser [PDecl]
1399provider syn = do doc <- try (do (doc, _) <- docstring syn
1400 fc1 <- getFC
1401 lchar '%'
1402 fc2 <- reservedFC "provide"
1403 highlightP (spanFC fc1 fc2) AnnKeyword
1404 return doc)
1405 provideTerm doc <|> providePostulate doc
1406 <?> "type provider"
1407 where provideTerm doc =
1408 do lchar '('; (n, nfc) <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1409 fc <- getFC
1410 reservedHL "with"
1411 e <- expr syn <?> "provider expression"
1412 return [PProvider doc syn fc nfc (ProvTerm t e) n]
1413 providePostulate doc =
1414 do reservedHL "postulate"
1415 (n, nfc) <- fnName
1416 fc <- getFC
1417 reservedHL "with"
1418 e <- expr syn <?> "provider expression"
1419 return [PProvider doc syn fc nfc (ProvPostulate e) n]
1421{- | Parses a transform
1424Transform ::= '%' 'transform' Expr '==>' Expr
1427transform :: SyntaxInfo -> IdrisParser [PDecl]
1428transform syn = do try (lchar '%' *> reserved "transform")
1429 -- leave it unchecked, until we work out what this should
1430 -- actually mean...
1431-- safety <- option True (do reserved "unsafe"
1432-- return False)
1433 l <- expr syn
1434 fc <- getFC
1435 symbol "==>"
1436 r <- expr syn
1437 return [PTransform fc False l r]
1438 <?> "transform"
1440{- | Parses a top-level reflected elaborator script
1443RunElabDecl ::= '%' 'runElab' Expr
1446runElabDecl :: SyntaxInfo -> IdrisParser PDecl
1447runElabDecl syn =
1448 do kwFC <- try (do fc <- getFC
1449 lchar '%'
1450 fc' <- reservedFC "runElab"
1451 return (spanFC fc fc'))
1452 script <- expr syn <?> "elaborator script"
1453 highlightP kwFC AnnKeyword
1454 return $ PRunElabDecl kwFC script (syn_namespace syn)
1455 <?> "top-level elaborator script"
1457{- * Loading and parsing -}
1458{- | Parses an expression from input -}
1459parseExpr :: IState -> String -> Result PTerm
1460parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1462{- | Parses a constant form input -}
1463parseConst :: IState -> String -> Result Const
1464parseConst st = runparser (fmap fst constant) st "(input)"
1466{- | Parses a tactic from input -}
1467parseTactic :: IState -> String -> Result PTactic
1468parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1470{- | Parses a do-step from input (used in the elab shell) -}
1471parseElabShellStep :: IState -> String -> Result (Either ElabShellCmd PDo)
1472parseElabShellStep ist = runparser (fmap Right (do_ defaultSyntax) <|> fmap Left elabShellCmd) ist "(input)"
1473 where elabShellCmd = char ':' >>
1474 (reserved "qed" >> pure EQED ) <|>
1475 (reserved "abandon" >> pure EAbandon ) <|>
1476 (reserved "undo" >> pure EUndo ) <|>
1477 (reserved "state" >> pure EProofState) <|>
1478 (reserved "term" >> pure EProofTerm ) <|>
1479 (expressionTactic ["e", "eval"] EEval ) <|>
1480 (expressionTactic ["t", "type"] ECheck) <|>
1481 (expressionTactic ["search"] ESearch ) <|>
1482 (do reserved "doc"
1483 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)
1484 eof
1485 return (EDocStr doc))
1486 <?> "elab command"
1487 expressionTactic cmds tactic =
1488 do asum (map reserved cmds)
1489 t <- spaced (expr defaultSyntax)
1490 i <- get
1491 return $ tactic (desugar defaultSyntax i t)
1492 spaced parser = indentPropHolds gtProp *> parser
1494-- | Parse module header and imports
1495parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Delta)
1496parseImports fname input
1497 = do i <- getIState
1498 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1499 Failure err -> fail (show err)
1500 Success (x, annots, i) ->
1501 do putIState i
1502 fname' <- runIO $ Dir.makeAbsolute fname
1503 sendHighlighting $ addPath annots fname'
1504 return x
1505 where imports :: IdrisParser ((Maybe (Docstring ()), [String],
1506 [ImportInfo],
1507 Maybe Delta),
1508 [(FC, OutputAnnotation)], IState)
1509 imports = do whiteSpace
1510 (mdoc, mname, annots) <- moduleHeader
1511 ps_exp <- many import_
1512 mrk <- mark
1513 isEof <- lookAheadMatches eof
1514 let mrk' = if isEof
1515 then Nothing
1516 else Just mrk
1517 i <- get
1518 -- add Builtins and Prelude, unless options say
1519 -- not to
1520 let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp
1521 return ((mdoc, mname, ps, mrk'), annots, i)
1523 imp m = ImportInfo False (toPath m)
1524 Nothing [] NoFC NoFC
1525 ns = Spl.splitOn "."
1526 toPath = foldl1' (</>) . ns
1528 addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]
1529 addPath [] _ = []
1530 addPath ((fc, AnnNamespace ns Nothing) : annots) path =
1531 (fc, AnnNamespace ns (Just path)) : addPath annots path
1532 addPath (annot:annots) path = annot : addPath annots path
1534-- | There should be a better way of doing this...
1535findFC :: Doc -> (FC, String)
1536findFC x = let s = show (plain x) in findFC' s
1537 where findFC' s = case span (/= ':') s of
1538 -- Horrid kludge to prevent crashes on Windows
1539 (prefix, ':':'\\':rest) ->
1540 case findFC' rest of
1541 (NoFC, msg) -> (NoFC, msg)
1542 (FileFC f, msg) -> (FileFC (prefix ++ ":\\" ++ f), msg)
1543 (FC f start end, msg) -> (FC (prefix ++ ":\\" ++ f) start end, msg)
1544 (failname, ':':rest) -> case span isDigit rest of
1545 (line, ':':rest') -> case span isDigit rest' of
1546 (col, ':':msg) -> let pos = (read line, read col) in
1547 (FC failname pos pos, msg)
1549-- | Check if the coloring matches the options and corrects if necessary
1550fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1551fixColour False doc = ANSI.plain doc
1552fixColour True doc = doc
1554-- | A program is a list of declarations, possibly with associated
1555-- documentation strings.
1556parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1557 Idris [PDecl]
1558parseProg syn fname input mrk
1559 = do i <- getIState
1560 case runparser mainProg i fname input of
1561 Failure doc -> do -- FIXME: Get error location from trifecta
1562 -- this can't be the solution!
1563 -- Issue #1575 on the issue tracker.
1564 -- https://github.com/idris-lang/Idris-dev/issues/1575
1565 let (fc, msg) = findFC doc
1566 i <- getIState
1567 case idris_outputmode i of
1568 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1569 IdeMode n h -> iWarn fc (P.text msg)
1570 putIState (i { errSpan = Just fc })
1571 return []
1572 Success (x, i) -> do putIState i
1573 reportParserWarnings
1574 return $ collect x
1575 where mainProg :: IdrisParser ([PDecl], IState)
1576 mainProg = case mrk of
1577 Nothing -> do i <- get; return ([], i)
1578 Just mrk -> do
1579 release mrk
1580 ds <- prog syn
1581 i' <- get
1582 return (ds, i')
1584{- | Load idris module and show error if something wrong happens -}
1585loadModule :: FilePath -> IBCPhase -> Idris (Maybe String)
1586loadModule f phase
1587 = idrisCatch (loadModule' f phase)
1588 (\e -> do setErrSpan (getErrSpan e)
1589 ist <- getIState
1590 iWarn (getErrSpan e) $ pprintErr ist e
1591 return Nothing)
1593{- | Load idris module -}
1594loadModule' :: FilePath -> IBCPhase -> Idris (Maybe String)
1595loadModule' f phase
1596 = do i <- getIState
1597 let file = takeWhile (/= ' ') f
1598 ibcsd <- valIBCSubDir i
1599 ids <- allImportDirs
1600 fp <- findImport ids ibcsd file
1601 if file `elem` imported i
1602 then do logParser 1 $ "Already read " ++ file
1603 return Nothing
1604 else do putIState (i { imported = file : imported i })
1605 case fp of
1606 IDR fn -> loadSource False fn Nothing
1607 LIDR fn -> loadSource True fn Nothing
1608 IBC fn src ->
1609 idrisCatch (loadIBC True phase fn)
1610 (\c -> do logParser 1 $ fn ++ " failed " ++ pshow i c
1611 case src of
1612 IDR sfn -> loadSource False sfn Nothing
1613 LIDR sfn -> loadSource True sfn Nothing)
1614 return $ Just file
1616{- | Load idris code from file -}
1617loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()
1618loadFromIFile reexp phase i@(IBC fn src) maxline
1619 = do logParser 1 $ "Skipping " ++ getSrcFile i
1620 idrisCatch (loadIBC reexp phase fn)
1621 (\err -> ierror $ LoadingFailed fn err)
1622 where
1623 getSrcFile (IDR fn) = fn
1624 getSrcFile (LIDR fn) = fn
1625 getSrcFile (IBC f src) = getSrcFile src
1627loadFromIFile _ _ (IDR fn) maxline = loadSource' False fn maxline
1628loadFromIFile _ _ (LIDR fn) maxline = loadSource' True fn maxline
1630{-| Load idris source code and show error if something wrong happens -}
1631loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1632loadSource' lidr r maxline
1633 = idrisCatch (loadSource lidr r maxline)
1634 (\e -> do setErrSpan (getErrSpan e)
1635 ist <- getIState
1636 case e of
1637 At f e' -> iWarn f (pprintErr ist e')
1638 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1640{- | Load Idris source code-}
1641loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1642loadSource lidr f toline
1643 = do logParser 1 ("Reading " ++ f)
1644 i <- getIState
1645 let def_total = default_total i
1646 file_in <- runIO $ readSource f
1647 file <- if lidr then tclift $ unlit f file_in else return file_in
1648 (mdocs, mname, imports_in, pos) <- parseImports f file
1649 ai <- getAutoImports
1650 let imports = map (\n -> ImportInfo True n Nothing [] NoFC NoFC) ai ++ imports_in
1651 ids <- allImportDirs
1652 ibcsd <- valIBCSubDir i
1653 mapM_ (\(re, f, ns, nfc) ->
1654 do fp <- findImport ids ibcsd f
1655 case fp of
1656 LIDR fn -> ifail $ "No ibc for " ++ f
1657 IDR fn -> ifail $ "No ibc for " ++ f
1658 IBC fn src ->
1659 do loadIBC True IBC_Building fn
1660 let srcFn = case src of
1661 IDR fn -> Just fn
1662 LIDR fn -> Just fn
1663 _ -> Nothing
1664 srcFnAbs <- case srcFn of
1665 Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)
1666 Nothing -> return Nothing
1667 sendHighlighting [(nfc, AnnNamespace ns srcFnAbs)])
1668 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]
1669 reportParserWarnings
1670 sendParserHighlighting
1672 -- process and check module aliases
1673 let modAliases = M.fromList
1674 [ (prep alias, prep realName)
1675 | ImportInfo { import_reexport = reexport
1676 , import_path = realName
1677 , import_rename = Just (alias, _)
1678 , import_location = fc } <- imports
1680 prep = map T.pack . reverse . Spl.splitOn [pathSeparator]
1681 aliasNames = [ (alias, fc)
1682 | ImportInfo { import_rename = Just (alias, _)
1683 , import_location = fc } <- imports
1685 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1686 case map head . filter ((/= 1) . length) $ histogram of
1687 [] -> logParser 3 $ "Module aliases: " ++ show (M.toList modAliases)
1688 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1690 i <- getIState
1691 putIState (i { default_access = Private, module_aliases = modAliases })
1692 clearIBC -- start a new .ibc file
1693 -- record package info in .ibc
1694 imps <- allImportDirs
1695 mapM_ addIBC (map IBCImportDir imps)
1696 mapM_ (addIBC . IBCImport)
1697 [ (reexport, realName)
1698 | ImportInfo { import_reexport = reexport
1699 , import_path = realName
1700 } <- imports
1702 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1703 maxline = toline }
1704 ist <- getIState
1705 -- Save the span from parsing the module header, because
1706 -- an empty program parse might obliterate it.
1707 let oldSpan = idris_parsedSpan ist
1708 ds' <- parseProg syntax f file pos
1710 case (ds', oldSpan) of
1711 ([], Just fc) ->
1712 -- If no program elements were parsed, we dind't
1713 -- get a loaded region in the IBC file. That
1714 -- means we need to add it back.
1715 do ist <- getIState
1716 putIState ist { idris_parsedSpan = oldSpan
1717 , ibc_write = IBCParsedRegion fc :
1718 ibc_write ist
1720 _ -> return ()
1721 sendParserHighlighting
1723 -- Parsing done, now process declarations
1725 let ds = namespaces mname ds'
1726 logParser 3 (show $ showDecls verbosePPOption ds)
1727 i <- getIState
1728 logLvl 10 (show (toAlist (idris_implicits i)))
1729 logLvl 3 (show (idris_infixes i))
1730 -- Now add all the declarations to the context
1731 v <- verbose
1732 when v $ iputStrLn $ "Type checking " ++ f
1733 -- we totality check after every Mutual block, so if
1734 -- anything is a single definition, wrap it in a
1735 -- mutual block on its own
1736 elabDecls toplevel (map toMutual ds)
1737 i <- getIState
1738 -- simplify every definition do give the totality checker
1739 -- a better chance
1740 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1741 ctxt' <-
1742 do ctxt <- getContext
1743 tclift $ simplifyCasedef n (getErasureInfo i) ctxt
1744 setContext ctxt')
1745 (map snd (idris_totcheck i))
1746 -- build size change graph from simplified definitions
1747 logLvl 1 "Totality checking"
1748 i <- getIState
1749 mapM_ buildSCG (idris_totcheck i)
1750 mapM_ checkDeclTotality (idris_totcheck i)
1752 -- Redo totality check for deferred names
1753 let deftots = idris_defertotcheck i
1754 logLvl 1 $ "Totality checking " ++ show deftots
1755 mapM_ (\x -> do tot <- getTotality x
1756 case tot of
1757 Total _ -> setTotality x Unchecked
1758 _ -> return ()) (map snd deftots)
1759 mapM_ buildSCG deftots
1760 mapM_ checkDeclTotality deftots
1762 logLvl 1 ("Finished " ++ f)
1763 ibcsd <- valIBCSubDir i
1764 logLvl 1 "Universe checking"
1765 iucheck
1766 let ibc = ibcPathNoFallback ibcsd f
1767 i <- getIState
1768 addHides (hide_list i)
1770 -- Save module documentation if applicable
1771 i <- getIState
1772 case mdocs of
1773 Nothing -> return ()
1774 Just docs -> addModDoc syntax mname docs
1777 -- Finally, write an ibc and highlights if checking was successful
1778 ok <- noErrors
1779 when ok $
1780 do idrisCatch (do writeIBC f ibc; clearIBC)
1781 (\c -> return ()) -- failure is harmless
1782 hl <- getDumpHighlighting
1783 when hl $
1784 idrisCatch (writeHighlights f)
1785 (const $ return ()) -- failure is harmless
1786 clearHighlights
1787 i <- getIState
1788 putIState (i { default_total = def_total,
1789 hide_list = emptyContext })
1790 return ()
1791 where
1792 namespaces :: [String] -> [PDecl] -> [PDecl]
1793 namespaces [] ds = ds
1794 namespaces (x:xs) ds = [PNamespace x NoFC (namespaces xs ds)]
1796 toMutual :: PDecl -> PDecl
1797 toMutual m@(PMutual _ d) = m
1798 toMutual (PNamespace x fc ds) = PNamespace x fc (map toMutual ds)
1799 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1800 case x of
1801 PClauses{} -> r
1802 PClass{} -> r
1803 PData{} -> r
1804 PInstance{} -> r
1805 _ -> x
1807 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1808 addModDoc syn mname docs =
1809 do ist <- getIState
1810 docs' <- elabDocTerms recinfo (parsedDocs ist)
1811 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1812 putIState ist { idris_moduledocs = modDocs' }
1813 addIBC (IBCModDocs docName)
1814 where
1815 docName = NS modDocName (map T.pack (reverse mname))
1816 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1818{- | Adds names to hide list -}
1819addHides :: Ctxt Accessibility -> Idris ()
1820addHides xs = do i <- getIState
1821 let defh = default_access i
1822 mapM_ doHide (toAlist xs)
1823 where doHide (n, a) = do setAccessibility n a
1824 addIBC (IBCAccess n a)