git.iko.soy/Idris-dev
on d773edd help sign in
Idris-dev/src/Idris/Parser.hs
1817 lines 72 kB history raw
1{-|
2Module : Idris.Parser
3Description : Idris' parser.
5License : BSD3
6Maintainer : The Idris Community.
7-}
9{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,
10 PatternGuards #-}
11{-# OPTIONS_GHC -O0 #-}
12-- FIXME: {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
13{-# OPTIONS_GHC -fwarn-unused-imports #-}
15module Idris.Parser(IdrisParser(..), ImportInfo(..), addReplSyntax, clearParserWarnings,
16 decl, fixColour, loadFromIFile, loadModule, name, opChars, parseElabShellStep, parseConst, parseExpr, parseImports, parseTactic,
17 runparser, ParseError, parseErrorDoc) where
19import Idris.AbsSyntax hiding (namespace, params)
20import Idris.Core.Evaluate
21import Idris.Core.TT
22import Idris.Delaborate
23import Idris.Docstrings hiding (Unchecked)
24import Idris.DSL
25import Idris.Elab.Value
26import Idris.ElabDecls
27import Idris.Error
28import Idris.IBC
29import Idris.Imports
30import Idris.Options
31import Idris.Output
32import Idris.Parser.Data
33import Idris.Parser.Expr
34import Idris.Parser.Helpers
35import Idris.Parser.Ops
36import Idris.Termination
37import Idris.Unlit
39import qualified Util.Pretty
40import Util.System (readSource)
42import Prelude hiding (pi)
44import Control.Applicative hiding (Const)
45import Control.Monad
46import Control.Monad.State.Strict
47import Data.Char
48import Data.Foldable (asum)
49import Data.Function
50import Data.Generics.Uniplate.Data (descendM)
51import Data.List
52import qualified Data.List.NonEmpty as NonEmpty
53import qualified Data.List.Split as Spl
54import qualified Data.Map as M
55import Data.Maybe
56import Data.Ord
57import qualified Data.Text as T
58import qualified System.Directory as Dir (makeAbsolute)
59import System.FilePath
60import Text.Megaparsec ((<?>))
61import qualified Text.Megaparsec as P
62import qualified Text.Megaparsec.Char as P
63import qualified Text.PrettyPrint.ANSI.Leijen as PP
65{-
67 grammar shortcut notation:
68 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)
69 RULE? = optional rule (i.e. RULE or nothing)
70 RULE* = repeated rule (i.e. RULE zero or more times)
71 RULE+ = repeated rule with at least one match (i.e. RULE one or more times)
72 RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)
73 RULE{n} = rule repeated n times
75-}
77{- * Main grammar -}
79{-| Parses module definition
82 ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;
84-}
85moduleHeader :: IdrisParser (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
86moduleHeader = P.try (do docs <- optional docComment
87 noArgs docs
88 keyword "module"
89 (i, ifc) <- withExtent identifier
90 P.option ';' (lchar ';')
91 let modName = moduleName i
92 return (fmap fst docs,
93 modName,
94 [(ifc, AnnNamespace (map T.pack modName) Nothing)]))
95 <|> P.try (do lchar '%'; reserved "unqualified"
96 return (Nothing, [], []))
97 <|> return (Nothing, moduleName "Main", [])
98 where moduleName x = case span (/='.') x of
99 (x, "") -> [x]
100 (x, '.':y) -> x : moduleName y
101 noArgs (Just (_, args)) | not (null args) = fail "Modules do not take arguments"
102 noArgs _ = return ()
104data ImportInfo = ImportInfo { import_reexport :: Bool
105 , import_path :: FilePath
106 , import_rename :: Maybe (String, FC)
107 , import_namespace :: [T.Text]
108 , import_location :: FC
109 , import_modname_location :: FC
110 }
112{-| Parses an import statement
115 Import ::= 'import' Identifier_t ';'?;
117 -}
118import_ :: IdrisParser ImportInfo
119import_ = do fc <- extent $ keyword "import"
120 reexport <- P.option False (True <$ keyword "public")
121 (id, idfc) <- withExtent identifier
122 newName <- optional (do keyword "as"
123 withExtent identifier)
124 P.option ';' (lchar ';')
125 return $ ImportInfo reexport (toPath id)
126 (fmap (\(n, fc) -> (toPath n, fc)) newName)
127 (map T.pack $ ns id) fc idfc
128 <?> "import statement"
129 where ns = Spl.splitOn "."
130 toPath = foldl1' (</>) . ns
132{-| Parses program source
135 Prog ::= Decl* EOF;
137 -}
138prog :: SyntaxInfo -> IdrisParser [PDecl]
139prog syn = do (decls, fc) <- withExtent $ do
140 whiteSpace
141 decls <- concat <$> many (decl syn)
142 case maxline syn of
143 Nothing -> do notOpenBraces; P.eof
144 _ -> return ()
145 return decls
146 ist <- get
147 put ist { idris_parsedSpan = Just (FC (fc_fname fc) (0,0) (fc_end fc)),
148 ibc_write = IBCParsedRegion fc : ibc_write ist }
149 return decls
151{-| Parses a top-level declaration
154Decl ::=
155 Decl'
156 | Using
157 | Params
158 | Mutual
159 | Namespace
160 | Interface
161 | Implementation
162 | DSL
163 | Directive
164 | Provider
165 | Transform
166 | Import!
167 | RunElabDecl
168 ;
170-}
171decl :: SyntaxInfo -> IdrisParser [PDecl]
172decl syn = P.try (externalDecl syn)
173 <|> internalDecl syn
174 <?> "declaration"
176internalDecl :: SyntaxInfo -> IdrisParser [PDecl]
177internalDecl syn
178 = do fc <- getFC
179 -- if we're after maxline, stop at the next type declaration
180 -- (so we get all cases of a definition to preserve totality
181 -- results, in particular).
182 let continue = case maxline syn of
183 Nothing -> True
184 Just l -> if fst (fc_end fc) > l
185 then mut_nesting syn /= 0
186 else True
187 -- What I'd really like to do here is explicitly save the
188 -- current state, then if reading ahead finds we've passed
189 -- the end of the definition, reset the state. But I've lost
190 -- patience with trying to find out how to do that from the
191 -- trifecta docs, so this does the job instead.
192 if continue then
193 do notEndBlock
194 declBody continue
195 else P.try (do notEndBlock
196 declBody continue)
197 <|> fail "End of readable input"
198 where declBody :: Bool -> IdrisParser [PDecl]
199 declBody b =
200 P.try (implementation syn)
201 <|> P.try (openInterface syn)
202 <|> declBody' b
203 <|> using_ syn
204 <|> params syn
205 <|> mutual syn
206 <|> namespace syn
207 <|> interface_ syn
208 <|> do d <- dsl syn; return [d]
209 <|> directive syn
210 <|> provider syn
211 <|> transform syn
212 <|> do import_; fail "imports must be at top of file"
213 <?> "declaration"
214 declBody' :: Bool -> IdrisParser [PDecl]
215 declBody' cont = do d <- decl' syn
216 i <- get
217 let d' = fmap (debindApp syn . (desugar syn i)) d
218 if continue cont d'
219 then return [d']
220 else fail "End of readable input"
222 -- Keep going while we're still parsing clauses
223 continue False (PClauses _ _ _ _) = True
224 continue c _ = c
226{-| Parses a top-level declaration with possible syntax sugar
229Decl' ::=
230 Fixity
231 | FunDecl'
232 | Data
233 | Record
234 | SyntaxDecl
235 ;
237-}
238decl' :: SyntaxInfo -> IdrisParser PDecl
239decl' syn = fixity
240 <|> syntaxDecl syn
241 <|> fnDecl' syn
242 <|> data_ syn
243 <|> record syn
244 <|> runElabDecl syn
245 <?> "declaration"
247externalDecl :: SyntaxInfo -> IdrisParser [PDecl]
248externalDecl syn = do i <- get
249 notEndBlock
250 (decls, fc@(FC fn _ _)) <- withExtent $ declExtensions syn (syntaxRulesList $ syntax_rules i)
251 return $ map (mapPDeclFC (fixFC fc) (fixFCH fn fc)) decls
252 where
253 -- | Fix non-highlighting FCs to prevent spurious error location reports
254 fixFC :: FC -> FC -> FC
255 fixFC outer inner | inner `fcIn` outer = inner
256 | otherwise = outer
257 -- | Fix highlighting FCs by obliterating them, to avoid spurious highlights
258 fixFCH fn outer inner | inner `fcIn` outer = inner
259 | otherwise = FileFC fn
261declExtensions :: SyntaxInfo -> [Syntax] -> IdrisParser [PDecl]
262declExtensions syn rules = declExtension syn [] (filter isDeclRule rules)
263 <?> "user-defined declaration"
264 where
265 isDeclRule (DeclRule _ _) = True
266 isDeclRule _ = False
268declExtension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax]
269 -> IdrisParser [PDecl]
270declExtension syn ns rules =
271 P.choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->
272 case head rs of -- can never be []
273 DeclRule (symb:_) _ -> P.try $ do
274 n <- extSymbol symb
275 declExtension syn (n : ns) [DeclRule ss t | (DeclRule (_:ss) t) <- rs]
276 -- If we have more than one Rule in this bucket, our grammar is
277 -- nondeterministic.
278 DeclRule [] dec -> let r = map (update (mapMaybe id ns)) dec in
279 return r
281 where
282 update :: [(Name, SynMatch)] -> PDecl -> PDecl
283 update ns = updateNs ns . fmap (updateRefs ns) . fmap (updateSynMatch ns)
285 updateRefs ns = mapPT newref
286 where
287 newref (PRef fc fcs n) = PRef fc fcs (updateB ns n)
288 newref t = t
290 -- Below is a lot of tedious boilerplate which updates any top level
291 -- names in the declaration. It will only change names which are bound in
292 -- the declaration (including method names in interfaces and field names in
293 -- record declarations, not including pattern variables)
294 updateB :: [(Name, SynMatch)] -> Name -> Name
295 updateB ns (NS n mods) = NS (updateB ns n) mods
296 updateB ns n = case lookup n ns of
297 Just (SynBind tfc t) -> t
298 _ -> n
300 updateNs :: [(Name, SynMatch)] -> PDecl -> PDecl
301 updateNs ns (PTy doc argdoc s fc o n fc' t)
302 = PTy doc argdoc s fc o (updateB ns n) fc' t
303 updateNs ns (PClauses fc o n cs)
304 = PClauses fc o (updateB ns n) (map (updateClause ns) cs)
305 updateNs ns (PCAF fc n t) = PCAF fc (updateB ns n) t
306 updateNs ns (PData ds cds s fc o dat)
307 = PData ds cds s fc o (updateData ns dat)
308 updateNs ns (PParams fc ps ds) = PParams fc ps (map (updateNs ns) ds)
309 updateNs ns (PNamespace s fc ds) = PNamespace s fc (map (updateNs ns) ds)
310 updateNs ns (PRecord doc syn fc o n fc' ps pdocs fields cname cdoc s)
311 = PRecord doc syn fc o (updateB ns n) fc' ps pdocs
312 (map (updateField ns) fields)
313 (updateRecCon ns cname)
314 cdoc
315 s
316 updateNs ns (PInterface docs s fc cs cn fc' ps pdocs pdets ds cname cdocs)
317 = PInterface docs s fc cs (updateB ns cn) fc' ps pdocs pdets
318 (map (updateNs ns) ds)
319 (updateRecCon ns cname)
320 cdocs
321 updateNs ns (PImplementation docs pdocs s fc cs pnames acc opts cn fc' ps pextra ity ni ds)
322 = PImplementation docs pdocs s fc cs pnames acc opts (updateB ns cn) fc'
323 ps pextra ity (fmap (updateB ns) ni)
324 (map (updateNs ns) ds)
325 updateNs ns (PMutual fc ds) = PMutual fc (map (updateNs ns) ds)
326 updateNs ns (PProvider docs s fc fc' pw n)
327 = PProvider docs s fc fc' pw (updateB ns n)
328 updateNs ns d = d
330 updateRecCon ns Nothing = Nothing
331 updateRecCon ns (Just (n, fc)) = Just (updateB ns n, fc)
333 updateField ns (m, p, t, doc) = (updateRecCon ns m, p, t, doc)
335 updateClause ns (PClause fc n t ts t' ds)
336 = PClause fc (updateB ns n) t ts t' (map (update ns) ds)
337 updateClause ns (PWith fc n t ts t' m ds)
338 = PWith fc (updateB ns n) t ts t' m (map (update ns) ds)
339 updateClause ns (PClauseR fc ts t ds)
340 = PClauseR fc ts t (map (update ns) ds)
341 updateClause ns (PWithR fc ts t m ds)
342 = PWithR fc ts t m (map (update ns) ds)
344 updateData ns (PDatadecl n fc t cs)
345 = PDatadecl (updateB ns n) fc t (map (updateCon ns) cs)
346 updateData ns (PLaterdecl n fc t)
347 = PLaterdecl (updateB ns n) fc t
349 updateCon ns (cd, ads, cn, fc, ty, fc', fns)
350 = (cd, ads, updateB ns cn, fc, ty, fc', fns)
352 ruleGroup [] [] = True
353 ruleGroup (s1:_) (s2:_) = s1 == s2
354 ruleGroup _ _ = False
356 extSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
357 extSymbol (Keyword n) = Nothing <$ keyword (show n)
358 extSymbol (Expr n) = do tm <- expr syn
359 return $ Just (n, SynTm tm)
360 extSymbol (SimpleExpr n) = do tm <- simpleExpr syn
361 return $ Just (n, SynTm tm)
362 extSymbol (Binding n) = do (b, fc) <- withExtent name
363 return $ Just (n, SynBind fc b)
364 extSymbol (Symbol s) = Nothing <$ highlight AnnKeyword (symbol s)
366{-| Parses a syntax extension declaration (and adds the rule to parser state)
369 SyntaxDecl ::= SyntaxRule;
371-}
372syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
373syntaxDecl syn = do (s, fc) <- withExtent $ syntaxRule syn
374 modify $ \i -> i `addSyntax` s
375 return (PSyntax fc s)
377-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.
378addSyntax :: IState -> Syntax -> IState
379addSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
380 syntax_keywords = ks ++ ns,
381 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc }
382 where rs = syntax_rules i
383 ns = syntax_keywords i
384 ibc = ibc_write i
385 ks = map show (syntaxNames s)
387-- | Like 'addSyntax', but no effect on the IBC.
388addReplSyntax :: IState -> Syntax -> IState
389addReplSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
390 syntax_keywords = ks ++ ns }
391 where rs = syntax_rules i
392 ns = syntax_keywords i
393 ks = map show (syntaxNames s)
395{-| Parses a syntax extension declaration
398SyntaxRuleOpts ::= 'term' | 'pattern';
402SyntaxRule ::=
403 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
407SyntaxSym ::= '[' Name_t ']'
408 | '{' Name_t '}'
409 | Name_t
410 | StringLiteral_t
411 ;
413-}
414syntaxRule :: SyntaxInfo -> IdrisParser Syntax
415syntaxRule syn
416 = do sty <- P.try (do
417 pushIndent
418 sty <- P.option AnySyntax
419 (TermSyntax <$ keyword "term"
420 <|> PatternSyntax <$ keyword "pattern")
421 keyword "syntax"
422 return sty)
423 syms <- some syntaxSym
424 when (all isExpr syms) $ P.unexpected . P.Label . NonEmpty.fromList $ "missing keywords in syntax rule"
425 let ns = mapMaybe getName syms
426 when (length ns /= length (nub ns))
427 $ P.unexpected . P.Label . NonEmpty.fromList $ "repeated variable in syntax rule"
428 lchar '='
429 tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]
430 terminator
431 return (Rule (mkSimple syms) tm sty)
432 <|> do keyword "decl"; keyword "syntax"
433 syms <- some syntaxSym
434 when (all isExpr syms) $ P.unexpected . P.Label . NonEmpty.fromList $ "missing keywords in syntax rule"
435 let ns = mapMaybe getName syms
436 when (length ns /= length (nub ns))
437 $ P.unexpected . P.Label . NonEmpty.fromList $ "repeated variable in syntax rule"
438 lchar '='
439 openBlock
440 dec <- some (decl syn)
441 closeBlock
442 return (DeclRule (mkSimple syms) (concat dec))
443 where
444 isExpr (Expr _) = True
445 isExpr _ = False
446 getName (Expr n) = Just n
447 getName _ = Nothing
448 -- Can't parse two full expressions (i.e. expressions with application) in a row
449 -- so change them both to a simple expression
450 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
451 mkSimple xs = mkSimple' xs
453 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
454 mkSimple es
455 -- Can't parse a full expression followed by operator like characters due to ambiguity
456 mkSimple' (Expr e : Symbol s : es)
457 | takeWhile (`elem` opChars) ts /= "" = SimpleExpr e : Symbol s : mkSimple' es
458 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s
459 mkSimple' (e : es) = e : mkSimple' es
460 mkSimple' [] = []
462 -- Prevent syntax variable capture by making all binders under syntax unique
463 -- (the ol' Common Lisp GENSYM approach)
464 uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
465 uniquifyBinders userNames = fixBind 0 []
466 where
467 fixBind :: Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
468 fixBind 0 rens (PRef fc hls n) | Just n' <- lookup n rens =
469 return $ PRef fc hls n'
470 fixBind 0 rens (PPatvar fc n) | Just n' <- lookup n rens =
471 return $ PPatvar fc n'
472 fixBind 0 rens (PLam fc n nfc ty body)
473 | n `elem` userNames = liftM2 (PLam fc n nfc)
474 (fixBind 0 rens ty)
475 (fixBind 0 rens body)
476 | otherwise =
477 do ty' <- fixBind 0 rens ty
478 n' <- gensym n
479 body' <- fixBind 0 ((n,n'):rens) body
480 return $ PLam fc n' nfc ty' body'
481 fixBind 0 rens (PPi plic n nfc argTy body)
482 | n `elem` userNames = liftM2 (PPi plic n nfc)
483 (fixBind 0 rens argTy)
484 (fixBind 0 rens body)
485 | otherwise =
486 do ty' <- fixBind 0 rens argTy
487 n' <- gensym n
488 body' <- fixBind 0 ((n,n'):rens) body
489 return $ (PPi plic n' nfc ty' body')
490 fixBind 0 rens (PLet fc rig n nfc ty val body)
491 | n `elem` userNames = liftM3 (PLet fc rig n nfc)
492 (fixBind 0 rens ty)
493 (fixBind 0 rens val)
494 (fixBind 0 rens body)
495 | otherwise =
496 do ty' <- fixBind 0 rens ty
497 val' <- fixBind 0 rens val
498 n' <- gensym n
499 body' <- fixBind 0 ((n,n'):rens) body
500 return $ PLet fc rig n' nfc ty' val' body'
501 fixBind 0 rens (PMatchApp fc n) | Just n' <- lookup n rens =
502 return $ PMatchApp fc n'
503 -- Also rename resolved quotations, to allow syntax rules to
504 -- have quoted references to their own bindings.
505 fixBind 0 rens (PQuoteName n True fc) | Just n' <- lookup n rens =
506 return $ PQuoteName n' True fc
508 -- Don't mess with quoted terms
509 fixBind q rens (PQuasiquote tm goal) =
510 flip PQuasiquote goal <$> fixBind (q + 1) rens tm
511 fixBind q rens (PUnquote tm) =
512 PUnquote <$> fixBind (q - 1) rens tm
514 fixBind q rens x = descendM (fixBind q rens) x
516 gensym :: Name -> IdrisParser Name
517 gensym n = do ist <- get
518 let idx = idris_name ist
519 put ist { idris_name = idx + 1 }
520 return $ sMN idx (show n)
522{-| Parses a syntax symbol (either binding variable, keyword or expression)
525SyntaxSym ::= '[' Name_t ']'
526 | '{' Name_t '}'
527 | Name_t
528 | StringLiteral_t
529 ;
531 -}
532syntaxSym :: IdrisParser SSymbol
533syntaxSym = P.try (do lchar '['; n <- name; lchar ']'
534 return (Expr n))
535 <|> P.try (do lchar '{'; n <- name; lchar '}'
536 return (Binding n))
537 <|> do n <- iName []
538 return (Keyword n)
539 <|> do sym <- stringLiteral
540 return (Symbol sym)
541 <?> "syntax symbol"
543{-| Parses a function declaration with possible syntax sugar
546 FunDecl ::= FunDecl';
548-}
549fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
550fnDecl syn = P.try (do notEndBlock
551 d <- fnDecl' syn
552 i <- get
553 let d' = fmap (desugar syn i) d
554 return [d']) <?> "function declaration"
556{-| Parses a function declaration
559 FunDecl' ::=
560 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
561 | Postulate
562 | Pattern
563 | CAF
564 ;
566-}
567fnDecl' :: SyntaxInfo -> IdrisParser PDecl
568fnDecl' syn = (checkDeclFixity $
569 do (doc, argDocs, fc, opts', n, nfc, acc) <- P.try (do
570 pushIndent
571 (doc, argDocs) <- docstring syn
572 (opts, acc) <- fnOpts
573 (n_in, nfc) <- withExtent fnName
574 let n = expandNS syn n_in
575 fc <- extent $ lchar ':'
576 return (doc, argDocs, fc, opts, n, nfc, acc))
577 ty <- typeExpr (allowImp syn)
578 terminator
579 -- If it's a top level function, note the accessibility
580 -- rules
581 when (syn_toplevel syn) $ addAcc n acc
582 return (PTy doc argDocs syn fc opts' n nfc ty)
583 <|> postulate syn
584 <|> caf syn
585 <|> pattern syn)
586 <?> "function declaration"
588{-| Parses a series of function and accessbility options
591FnOpts ::= FnOpt* Accessibility FnOpt*
593 -}
594fnOpts :: IdrisParser ([FnOpt], Accessibility)
595fnOpts = do
596 opts <- many fnOpt
597 acc <- accessibility
598 opts' <- many fnOpt
599 let allOpts = opts ++ opts'
600 let existingTotality = allOpts `intersect` [TotalFn, CoveringFn, PartialFn]
601 opts'' <- addDefaultTotality (nub existingTotality) allOpts
602 return (opts'', acc)
603 where prettyTot TotalFn = "total"
604 prettyTot PartialFn = "partial"
605 prettyTot CoveringFn = "covering"
606 addDefaultTotality [] opts = do
607 ist <- get
608 case default_total ist of
609 DefaultCheckingTotal -> return (TotalFn:opts)
610 DefaultCheckingCovering -> return (CoveringFn:opts)
611 DefaultCheckingPartial -> return opts -- Don't add partial so that --warn-partial still reports warnings if necessary
612 addDefaultTotality [tot] opts = return opts
613 -- Should really be a semantics error instead of a parser error
614 addDefaultTotality (tot1:tot2:tots) opts =
615 fail ("Conflicting totality modifiers specified " ++ prettyTot tot1 ++ " and " ++ prettyTot tot2)
618{-| Parses a function option
621FnOpt ::= 'total'
622 | 'partial'
623 | 'covering'
624 | 'implicit'
625 | '%' 'no_implicit'
626 | '%' 'assert_total'
627 | '%' 'error_handler'
628 | '%' 'reflection'
629 | '%' 'specialise' '[' NameTimesList? ']'
630 ;
634NameTimes ::= FnName Natural?;
638NameTimesList ::=
639 NameTimes
640 | NameTimes ',' NameTimesList
641 ;
643-}
644fnOpt :: IdrisParser FnOpt
645fnOpt = do keyword "total"; return TotalFn
646 <|> PartialFn <$ keyword "partial"
647 <|> CoveringFn <$ keyword "covering"
648 <|> do P.try (lchar '%' *> reserved "export"); c <- stringLiteral;
649 return $ CExport c
650 <|> NoImplicit <$ P.try (lchar '%' *> reserved "no_implicit")
651 <|> Inlinable <$ P.try (lchar '%' *> reserved "inline")
652 <|> StaticFn <$ P.try (lchar '%' *> reserved "static")
653 <|> do fc <- P.try $ extent $ lchar '%' *> reserved "assert_total"
654 parserWarning fc Nothing (Msg "%assert_total is deprecated. Use the 'assert_total' function instead.")
655 return AssertTotal
656 <|> ErrorHandler <$ P.try (lchar '%' *> reserved "error_handler")
657 <|> ErrorReverse <$ P.try (lchar '%' *> reserved "error_reverse")
658 <|> ErrorReduce <$ P.try (lchar '%' *> reserved "error_reduce")
659 <|> Reflection <$ P.try (lchar '%' *> reserved "reflection")
660 <|> AutoHint <$ P.try (lchar '%' *> reserved "hint")
661 <|> OverlappingDictionary <$ P.try (lchar '%' *> reserved "overlapping")
662 <|> do lchar '%'; reserved "specialise";
663 lchar '['; ns <- P.sepBy nameTimes (lchar ','); lchar ']';
664 return $ Specialise ns
665 <|> Implicit <$ keyword "implicit"
666 <?> "function modifier"
667 where nameTimes :: IdrisParser (Name, Maybe Int)
668 nameTimes = do n <- fnName
669 t <- P.option Nothing (do reds <- natural
670 return (Just (fromInteger reds)))
671 return (n, t)
673{-| Parses a postulate
676Postulate ::=
677 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
678 ;
680-}
681postulate :: SyntaxInfo -> IdrisParser PDecl
682postulate syn = do (doc, ext)
683 <- P.try $ do (doc, _) <- docstring syn
684 pushIndent
685 ext <- ppostDecl
686 return (doc, ext)
687 ist <- get
688 (opts, acc) <- fnOpts
689 (n_in, nfc) <- withExtent fnName
690 let n = expandNS syn n_in
691 lchar ':'
692 ty <- typeExpr (allowImp syn)
693 fc <- extent $ terminator
694 addAcc n acc
695 return (PPostulate ext doc syn fc nfc opts n ty)
696 <?> "postulate"
697 where ppostDecl = do fc <- keyword "postulate"; return False
698 <|> do lchar '%'; reserved "extern"; return True
700{-| Parses a using declaration
703Using ::=
704 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
705 ;
707 -}
708using_ :: SyntaxInfo -> IdrisParser [PDecl]
709using_ syn =
710 do keyword "using"
711 lchar '('; ns <- usingDeclList syn; lchar ')'
712 openBlock
713 let uvars = using syn
714 ds <- many (decl (syn { using = uvars ++ ns }))
715 closeBlock
716 return (concat ds)
717 <?> "using declaration"
719{-| Parses a parameters declaration
722Params ::=
723 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
724 ;
726-}
727params :: SyntaxInfo -> IdrisParser [PDecl]
728params syn =
729 do (ns, fc) <- withExtent $ do
730 keyword "parameters"
731 lchar '(' *> typeDeclList syn <* lchar ')'
732 let ns' = [(n, ty) | (_, n, _, ty) <- ns]
733 openBlock
734 let pvars = syn_params syn
735 ds <- many (decl syn { syn_params = pvars ++ ns' })
736 closeBlock
737 return [PParams fc ns' (concat ds)]
738 <?> "parameters declaration"
740-- | Parses an open block
741openInterface :: SyntaxInfo -> IdrisParser [PDecl]
742openInterface syn =
743 do (ns, fc) <- withExtent $ do
744 keyword "using"
745 keyword "implementation"
746 P.sepBy1 (withExtent fnName) (lchar ',')
748 openBlock
749 ds <- many (decl syn)
750 closeBlock
751 return [POpenInterfaces fc (map fst ns) (concat ds)]
752 <?> "open interface declaration"
758{-| Parses a mutual declaration (for mutually recursive functions)
761Mutual ::=
762 'mutual' OpenBlock Decl* CloseBlock
763 ;
765-}
766mutual :: SyntaxInfo -> IdrisParser [PDecl]
767mutual syn =
768 do fc <- extent $ keyword "mutual"
769 openBlock
770 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
771 closeBlock
772 return [PMutual fc (concat ds)]
773 <?> "mutual block"
775{-| Parses a namespace declaration
778Namespace ::=
779 'namespace' identifier OpenBlock Decl+ CloseBlock
780 ;
782-}
783namespace :: SyntaxInfo -> IdrisParser [PDecl]
784namespace syn =
785 do keyword "namespace"
786 (n, nfc) <- withExtent identifier
787 openBlock
788 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
789 closeBlock
790 return [PNamespace n nfc (concat ds)]
791 <?> "namespace declaration"
793{-| Parses a methods block (for implementations)
796 ImplementationBlock ::= 'where' OpenBlock FnDecl* CloseBlock
798-}
799implementationBlock :: SyntaxInfo -> IdrisParser [PDecl]
800implementationBlock syn = do keyword "where"
801 openBlock
802 ds <- many (fnDecl syn)
803 closeBlock
804 return (concat ds)
805 <?> "implementation block"
807{-| Parses a methods and implementations block (for interfaces)
810MethodOrImplementation ::=
811 FnDecl
812 | Implementation
813 ;
817InterfaceBlock ::=
818 'where' OpenBlock Constructor? MethodOrImplementation* CloseBlock
819 ;
821-}
822interfaceBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])
823interfaceBlock syn = do keyword "where"
824 openBlock
825 (cn, cd) <- P.option (Nothing, emptyDocstring) $
826 P.try (do (doc, _) <- P.option noDocs docComment
827 n <- constructor
828 return (Just n, doc))
829 ist <- get
830 let cd' = annotate syn ist cd
832 ds <- many (notEndBlock >> P.try (implementation syn)
833 <|> do x <- data_ syn
834 return [x]
835 <|> fnDecl syn)
836 closeBlock
837 return (cn, cd', concat ds)
838 <?> "interface block"
839 where
840 constructor :: IdrisParser (Name, FC)
841 constructor = keyword "constructor" *> withExtent fnName
843 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)
844 annotate syn ist = annotCode $ tryFullExpr syn ist
846{-| Parses an interface declaration
849InterfaceArgument ::=
850 Name
851 | '(' Name ':' Expr ')'
852 ;
856Interface ::=
857 DocComment_t? Accessibility? 'interface' ConstraintList? Name InterfaceArgument* InterfaceBlock?
858 ;
860-}
861interface_ :: SyntaxInfo -> IdrisParser [PDecl]
862interface_ syn = do (doc, argDocs, acc)
863 <- P.try (do (doc, argDocs) <- docstring syn
864 acc <- accessibility
865 interfaceKeyword
866 return (doc, argDocs, acc))
867 ((cons', n, nfc, cs, fds), fc) <- withExtent $ do
868 cons <- constraintList syn
869 let cons' = [(c, ty) | (_, c, _, ty) <- cons]
870 (n_in, nfc) <- withExtent fnName
871 let n = expandNS syn n_in
872 cs <- many carg
873 fds <- P.option [(cn, NoFC) | (cn, _, _) <- cs] fundeps
874 return (cons', n, nfc, cs, fds)
876 (cn, cd, ds) <- P.option (Nothing, fst noDocs, []) (interfaceBlock syn)
877 accData acc n (concatMap declared ds)
878 return [PInterface doc syn fc cons' n nfc cs argDocs fds ds cn cd]
879 <?> "interface declaration"
880 where
881 fundeps :: IdrisParser [(Name, FC)]
882 fundeps = do lchar '|'; P.sepBy (withExtent name) (lchar ',')
884 interfaceKeyword :: IdrisParser ()
885 interfaceKeyword = keyword "interface"
886 <|> do fc <- extent $ keyword "class"
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) <- withExtent name; lchar ':'; ty <- expr syn; lchar ')'
891 return (i, ifc, ty)
892 <|> do (i, ifc) <- withExtent name
893 return (i, ifc, PType ifc)
895{-| Parses an interface implementation declaration
898 Implementation ::=
899 DocComment_t? 'implementation' ImplementationName? ConstraintList? Name SimpleExpr* ImplementationBlock?
900 ;
904ImplementationName ::= '[' Name ']';
906-}
907implementation :: SyntaxInfo -> IdrisParser [PDecl]
908implementation syn = do (doc, argDocs) <- docstring syn
909 (opts, acc) <- fnOpts
910 optional implementationKeyword
912 ((en, cs, cs', cn, cnfc, args, pnames), fc) <- withExtent $ do
913 en <- optional implementationName
914 cs <- constraintList syn
915 let cs' = [(c, ty) | (_, c, _, ty) <- cs]
916 (cn, cnfc) <- withExtent fnName
917 args <- many (simpleExpr syn)
918 pnames <- implementationUsing
919 return (en, cs, cs', cn, cnfc, args, pnames)
921 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)
922 let t = bindList (\r -> PPi constraint { pcount = r }) cs sc
924 ds <- implementationBlock syn
925 return [PImplementation doc argDocs syn fc cs' pnames acc opts cn cnfc args [] t en ds]
926 <?> "implementation declaration"
927 where implementationName :: IdrisParser Name
928 implementationName = do lchar '['; n_in <- fnName; lchar ']'
929 let n = expandNS syn n_in
930 return n
931 <?> "implementation name"
932 implementationKeyword :: IdrisParser ()
933 implementationKeyword = keyword "implementation"
934 <|> do fc <- extent $ keyword "instance"
935 parserWarning fc Nothing (Msg "The 'instance' keyword is deprecated. Use 'implementation' (or omit it) instead.")
937 implementationUsing :: IdrisParser [Name]
938 implementationUsing = do keyword "using"
939 ns <- P.sepBy1 (withExtent fnName) (lchar ',')
940 return (map fst ns)
941 <|> return []
943-- | Parse a docstring
944docstring :: SyntaxInfo
945 -> IdrisParser (Docstring (Either Err PTerm),
946 [(Name,Docstring (Either Err PTerm))])
947docstring syn = do (doc, argDocs) <- P.option noDocs docComment
948 ist <- get
949 let doc' = annotCode (tryFullExpr syn ist) doc
950 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
951 | (n, d) <- argDocs ]
952 return (doc', argDocs')
955{-| Parses a using declaration list
958UsingDeclList ::=
959 UsingDeclList'
960 | NameList TypeSig
961 ;
965UsingDeclList' ::=
966 UsingDecl
967 | UsingDecl ',' UsingDeclList'
968 ;
972NameList ::=
973 Name
974 | Name ',' NameList
975 ;
977-}
978usingDeclList :: SyntaxInfo -> IdrisParser [Using]
979usingDeclList syn
980 = P.try (P.sepBy1 (usingDecl syn) (lchar ','))
981 <|> do ns <- P.sepBy1 name (lchar ',')
982 lchar ':'
983 t <- typeExpr (disallowImp syn)
984 return (map (\x -> UImplicit x t) ns)
985 <?> "using declaration list"
987{-| Parses a using declaration
990UsingDecl ::=
991 FnName TypeSig
992 | FnName FnName+
993 ;
995-}
996usingDecl :: SyntaxInfo -> IdrisParser Using
997usingDecl syn = P.try (do x <- fnName
998 lchar ':'
999 t <- typeExpr (disallowImp syn)
1000 return (UImplicit x t))
1001 <|> do c <- fnName
1002 xs <- many fnName
1003 return (UConstraint c xs)
1004 <?> "using declaration"
1006{-| Parse a clause with patterns
1009Pattern ::= Clause;
1012pattern :: SyntaxInfo -> IdrisParser PDecl
1013pattern syn = do (clause, fc) <- withExtent (clause syn)
1014 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
1015 <?> "pattern"
1017{-| Parse a constant applicative form declaration
1020CAF ::= 'let' FnName '=' Expr Terminator;
1023caf :: SyntaxInfo -> IdrisParser PDecl
1024caf syn = do keyword "let"
1025 (n, fc) <- withExtent (expandNS syn <$> fnName)
1026 pushIndent
1027 lchar '='
1028 t <- indented $ expr syn
1029 terminator
1030 return (PCAF fc n t)
1031 <?> "constant applicative form declaration"
1033{-| Parse an argument expression
1036ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
1039argExpr :: SyntaxInfo -> IdrisParser PTerm
1040argExpr syn = let syn' = syn { inPattern = True } in
1041 P.try (hsimpleExpr syn') <|> simpleExternalExpr syn'
1042 <?> "argument expression"
1044{-| Parse a right hand side of a function
1047RHS ::= '=' Expr
1048 | '?=' RHSName? Expr
1049 | Impossible
1054RHSName ::= '{' FnName '}';
1057rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
1058rhs syn n = do lchar '='
1059 indentGt
1060 expr syn
1061 <|> do symbol "?=";
1062 (name, fc) <- withExtent $ P.option n' (symbol "{" *> fnName <* symbol "}")
1063 r <- expr syn
1064 return (addLet fc name r)
1065 <|> impossible
1066 <?> "function right hand side"
1067 where mkN :: Name -> Name
1068 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
1069 then sUN "infix_op_lemma_1"
1070 else sUN (str x++"_lemma_1")
1071 mkN (NS x n) = NS (mkN x) n
1072 n' :: Name
1073 n' = mkN n
1074 addLet :: FC -> Name -> PTerm -> PTerm
1075 addLet fc nm (PLet fc' rig n nfc ty val r) = PLet fc' rig n nfc ty val (addLet fc nm r)
1076 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
1077 where addLetC (l, r) = (l, addLet fc nm r)
1078 addLet fc nm r = (PLet fc RigW (sUN "value") NoFC Placeholder r (PMetavar NoFC nm))
1080{-|Parses a function clause
1083RHSOrWithBlock ::= RHS WhereOrTerminator
1084 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
1089Clause ::= WExpr+ RHSOrWithBlock
1090 | SimpleExpr '<==' FnName RHS WhereOrTerminator
1091 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
1092 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
1097ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
1101WhereOrTerminator ::= WhereBlock | Terminator;
1104clause :: SyntaxInfo -> IdrisParser PClause
1105clause syn
1106 -- unnamed with or function clause (inside a with)
1107 = appExtent (do
1108 wargs <- P.try (do pushIndent; some (wExpr syn))
1109 ist <- get
1110 n <- case lastParse ist of
1111 Just t -> return t
1112 Nothing -> fail "Invalid clause"
1113 (do r <- rhs syn n
1114 let wsyn = syn { syn_namespace = [], syn_toplevel = False }
1115 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1116 <|> ([], []) <$ terminator
1117 return $ \fc -> PClauseR fc wargs r wheres) <|> (do
1118 popIndent
1119 keyword "with"
1120 wval <- simpleExpr syn
1121 pn <- optProof
1122 openBlock
1123 ds <- some $ fnDecl syn
1124 let withs = concat ds
1125 closeBlock
1126 return $ \fc -> PWithR fc wargs wval pn withs))
1127 -- <==
1128 <|> do ty <- P.try (do pushIndent
1129 ty <- simpleExpr syn
1130 symbol "<=="
1131 return ty)
1132 (n, fc) <- withExtent (expandNS syn <$> fnName)
1133 r <- rhs syn n
1134 let wsyn = syn { syn_namespace = [] }
1135 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1136 <|> ([], []) <$ terminator
1137 let capp = PLet fc RigW (sMN 0 "match") NoFC
1138 ty
1139 (PMatchApp fc n)
1140 (PRef fc [] (sMN 0 "match"))
1141 ist <- get
1142 put (ist { lastParse = Just n })
1143 return $ PClause fc n capp [] r wheres
1144 -- lhs application "with" clause or function clause
1145 <|> do pushIndent
1146 (n, nfc, capp, wargs) <- lhs
1147 modify $ \ist -> ist { lastParse = Just n }
1148 (do (rs, fc) <- withExtent (rhs syn n)
1149 let wsyn = syn { syn_namespace = [] }
1150 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1151 <|> ([], []) <$ terminator
1152 return $ PClause fc n capp wargs rs wheres) <|> (do
1153 popIndent
1154 ((wval, pn), fc) <- withExtent $ do
1155 keyword "with"
1156 wval <- bracketed syn
1157 pn <- optProof
1158 return (wval, pn)
1159 openBlock
1160 ds <- some $ fnDecl syn
1161 closeBlock
1162 let withs = map (fillLHSD n capp wargs) $ concat ds
1163 return $ PWith fc n capp wargs wval pn withs)
1164 <?> "function clause"
1165 where
1166 lhsInfixApp :: IdrisParser (Name, FC, [PArg], [PTerm])
1167 lhsInfixApp = do l <- argExpr syn
1168 (op, nfc) <- withExtent symbolicOperator
1169 when (op == "=" || op == "?=" ) $
1170 fail "infix clause definition with \"=\" and \"?=\" not supported "
1171 let n = expandNS syn (sUN op)
1172 r <- argExpr syn
1173 wargs <- many (wExpr syn)
1174 return (n, nfc, [pexp l, pexp r], wargs)
1176 lhsPrefixApp :: IdrisParser (Name, FC, [PArg], [PTerm])
1177 lhsPrefixApp = do (n, nfc) <- withExtent (expandNS syn <$> fnName)
1178 args <- many (P.try (implicitArg (syn { inPattern = True } ))
1179 <|> P.try (constraintArg (syn { inPattern = True }))
1180 <|> (fmap pexp (argExpr syn)))
1181 wargs <- many (wExpr syn)
1182 return (n, nfc, args, wargs)
1184 lhs :: IdrisParser (Name, FC, PTerm, [PTerm])
1185 lhs = do ((n, nfc, args, wargs), lhs_fc) <- withExtent (P.try lhsInfixApp <|> lhsPrefixApp)
1186 let capp = PApp lhs_fc (PRef nfc [nfc] n) args
1187 return (n, nfc, capp, wargs)
1189 optProof = P.option Nothing (do keyword "proof"
1190 n <- withExtent fnName
1191 return (Just n))
1193 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
1194 fillLHS n capp owargs (PClauseR fc wargs v ws)
1195 = PClause fc n capp (owargs ++ wargs) v ws
1196 fillLHS n capp owargs (PWithR fc wargs v pn ws)
1197 = PWith fc n capp (owargs ++ wargs) v pn
1198 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1199 fillLHS _ _ _ c = c
1201 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
1202 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1203 fillLHSD n c a x = x
1205{-| Parses with pattern
1208WExpr ::= '|' Expr';
1211wExpr :: SyntaxInfo -> IdrisParser PTerm
1212wExpr syn = do lchar '|'
1213 expr' (syn { inPattern = True })
1214 <?> "with pattern"
1216{-| Parses a where block
1219WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
1222whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
1223whereBlock n syn
1224 = do keyword "where"
1225 ds <- indentedBlock1 (decl syn)
1226 let dns = concatMap (concatMap declared) ds
1227 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1228 <?> "where block"
1230{-|Parses a code generation target language name
1233Codegen ::= 'C'
1234 | 'Java'
1235 | 'JavaScript'
1236 | 'Node'
1237 | 'LLVM'
1238 | 'Bytecode'
1242codegen_ :: IdrisParser Codegen
1243codegen_ = do n <- identifier
1244 return (Via IBCFormat (map toLower n))
1245 <|> do reserved "Bytecode"; return Bytecode
1246 <?> "code generation language"
1248{-|Parses a compiler directive
1250StringList ::=
1251 String
1252 | String ',' StringList
1257Directive ::= '%' Directive';
1261Directive' ::= 'lib' CodeGen String_t
1262 | 'link' CodeGen String_t
1263 | 'flag' CodeGen String_t
1264 | 'include' CodeGen String_t
1265 | 'hide' Name
1266 | 'freeze' Name
1267 | 'thaw' Name
1268 | 'access' Accessibility
1269 | 'default' Totality
1270 | 'logging' Natural
1271 | 'dynamic' StringList
1272 | 'name' Name NameList
1273 | 'error_handlers' Name NameList
1274 | 'language' 'TypeProviders'
1275 | 'language' 'ErrorReflection'
1276 | 'deprecated' Name String
1277 | 'fragile' Name Reason
1281directive :: SyntaxInfo -> IdrisParser [PDecl]
1282directive syn = do P.try (lchar '%' *> reserved "lib")
1283 cgn <- codegen_
1284 lib <- stringLiteral
1285 return [PDirective (DLib cgn lib)]
1286 <|> do P.try (lchar '%' *> reserved "link")
1287 cgn <- codegen_; obj <- stringLiteral
1288 return [PDirective (DLink cgn obj)]
1289 <|> do P.try (lchar '%' *> reserved "flag")
1290 cgn <- codegen_; flag <- stringLiteral
1291 return [PDirective (DFlag cgn flag)]
1292 <|> do P.try (lchar '%' *> reserved "include")
1293 cgn <- codegen_
1294 hdr <- stringLiteral
1295 return [PDirective (DInclude cgn hdr)]
1296 <|> do P.try (lchar '%' *> reserved "hide"); n <- fnName
1297 return [PDirective (DHide n)]
1298 <|> do P.try (lchar '%' *> reserved "freeze"); n <- iName []
1299 return [PDirective (DFreeze n)]
1300 <|> do P.try (lchar '%' *> reserved "thaw"); n <- iName []
1301 return [PDirective (DThaw n)]
1302 -- injectivity assertins are intended for debugging purposes
1303 -- only, and won't be documented/could be removed at any point
1304 <|> do P.try (lchar '%' *> reserved "assert_injective"); n <- fnName
1305 return [PDirective (DInjective n)]
1306 -- Assert totality of something after definition. This is
1307 -- here as a debugging aid, so commented out...
1308-- <|> do P.try (lchar '%' *> reserved "assert_set_total"); n <- fst <$> fnName
1309-- return [PDirective (DSetTotal n)]
1310 <|> do P.try (lchar '%' *> reserved "access")
1311 acc <- accessibility
1312 ist <- get
1313 put ist { default_access = acc }
1314 return [PDirective (DAccess acc)]
1315 <|> do P.try (lchar '%' *> reserved "default"); tot <- totality
1316 i <- get
1317 put (i { default_total = tot } )
1318 return [PDirective (DDefault tot)]
1319 <|> do P.try (lchar '%' *> reserved "logging")
1320 i <- natural
1321 return [PDirective (DLogging i)]
1322 <|> do P.try (lchar '%' *> reserved "dynamic")
1323 libs <- P.sepBy1 stringLiteral (lchar ',')
1324 return [PDirective (DDynamicLibs libs)]
1325 <|> do P.try (lchar '%' *> reserved "name")
1326 (ty, tyFC) <- withExtent fnName
1327 ns <- P.sepBy1 (withExtent name) (lchar ',')
1328 return [PDirective (DNameHint ty tyFC ns)]
1329 <|> do P.try (lchar '%' *> reserved "error_handlers")
1330 (fn, nfc) <- withExtent fnName
1331 (arg, afc) <- withExtent fnName
1332 ns <- P.sepBy1 (withExtent name) (lchar ',')
1333 return [PDirective (DErrorHandlers fn nfc arg afc ns) ]
1334 <|> do P.try (lchar '%' *> reserved "language"); ext <- pLangExt;
1335 return [PDirective (DLanguage ext)]
1336 <|> do P.try (lchar '%' *> reserved "deprecate")
1337 n <- fnName
1338 alt <- P.option "" stringLiteral
1339 return [PDirective (DDeprecate n alt)]
1340 <|> do P.try (lchar '%' *> reserved "fragile")
1341 n <- fnName
1342 alt <- P.option "" stringLiteral
1343 return [PDirective (DFragile n alt)]
1344 <|> do fc <- extent $ P.try (lchar '%' *> reserved "used")
1345 fn <- fnName
1346 arg <- iName []
1347 return [PDirective (DUsed fc fn arg)]
1348 <|> do P.try (lchar '%' *> reserved "auto_implicits")
1349 b <- on_off
1350 return [PDirective (DAutoImplicits b)]
1351 <?> "directive"
1352 where on_off = do reserved "on"; return True
1353 <|> do reserved "off"; return False
1355pLangExt :: IdrisParser LanguageExt
1356pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1357 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1358 <|> (reserved "UniquenessTypes" >> return UniquenessTypes)
1359 <|> (reserved "LinearTypes" >> return LinearTypes)
1360 <|> (reserved "DSLNotation" >> return DSLNotation)
1361 <|> (reserved "ElabReflection" >> return ElabReflection)
1362 <|> (reserved "FirstClassReflection" >> return FCReflection)
1364{-| Parses a totality
1367Totality ::= 'partial' | 'total' | 'covering'
1371totality :: IdrisParser DefaultTotality
1372totality
1373 = do keyword "total"; return DefaultCheckingTotal
1374 <|> do keyword "partial"; return DefaultCheckingPartial
1375 <|> do keyword "covering"; return DefaultCheckingCovering
1377{-| Parses a type provider
1380Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1381ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1383 -}
1384provider :: SyntaxInfo -> IdrisParser [PDecl]
1385provider syn = do doc <- P.try (do (doc, _) <- docstring syn
1386 highlight AnnKeyword $ lchar '%' *> reserved "provide"
1387 return doc)
1388 provideTerm doc <|> providePostulate doc
1389 <?> "type provider"
1390 where provideTerm doc =
1391 do lchar '('; (n, nfc) <- withExtent fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1392 keyword "with"
1393 (e, fc) <- withExtent (expr syn) <?> "provider expression"
1394 return [PProvider doc syn fc nfc (ProvTerm t e) n]
1395 providePostulate doc =
1396 do keyword "postulate"
1397 (n, nfc) <- withExtent fnName
1398 keyword "with"
1399 (e, fc) <- withExtent (expr syn) <?> "provider expression"
1400 return [PProvider doc syn fc nfc (ProvPostulate e) n]
1402{-| Parses a transform
1405Transform ::= '%' 'transform' Expr '==>' Expr
1408transform :: SyntaxInfo -> IdrisParser [PDecl]
1409transform syn = do P.try (lchar '%' *> reserved "transform")
1410 -- leave it unchecked, until we work out what this should
1411 -- actually mean...
1412-- safety <- option True (do reserved "unsafe"
1413-- return False)
1414 l <- expr syn
1415 fc <- extent $ symbol "==>"
1416 r <- expr syn
1417 return [PTransform fc False l r]
1418 <?> "transform"
1420{-| Parses a top-level reflected elaborator script
1423RunElabDecl ::= '%' 'runElab' Expr
1426runElabDecl :: SyntaxInfo -> IdrisParser PDecl
1427runElabDecl syn =
1428 do kwFC <- P.try (highlight AnnKeyword (extent $ lchar '%' *> reserved "runElab"))
1429 script <- expr syn <?> "elaborator script"
1430 return $ PRunElabDecl kwFC script (syn_namespace syn)
1431 <?> "top-level elaborator script"
1433{- * Loading and parsing -}
1434{-| Parses an expression from input -}
1435parseExpr :: IState -> String -> Either ParseError PTerm
1436parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1438{-| Parses a constant form input -}
1439parseConst :: IState -> String -> Either ParseError Const
1440parseConst st = runparser constant st "(input)"
1442{-| Parses a tactic from input -}
1443parseTactic :: IState -> String -> Either ParseError PTactic
1444parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1446{-| Parses a do-step from input (used in the elab shell) -}
1447parseElabShellStep :: IState -> String -> Either ParseError (Either ElabShellCmd PDo)
1448parseElabShellStep ist = runparser (Right <$> do_ defaultSyntax <|> Left <$> elabShellCmd) ist "(input)"
1449 where elabShellCmd = char ':' >>
1450 (reserved "qed" >> pure EQED ) <|>
1451 (reserved "abandon" >> pure EAbandon ) <|>
1452 (reserved "undo" >> pure EUndo ) <|>
1453 (reserved "state" >> pure EProofState) <|>
1454 (reserved "term" >> pure EProofTerm ) <|>
1455 (expressionTactic ["e", "eval"] EEval ) <|>
1456 (expressionTactic ["t", "type"] ECheck) <|>
1457 (expressionTactic ["search"] ESearch ) <|>
1458 (do reserved "doc"
1459 doc <- (Right <$> constant) <|> (Left <$> fnName)
1460 P.eof
1461 return (EDocStr doc))
1462 <?> "elab command"
1463 expressionTactic cmds tactic =
1464 do asum (map reserved cmds)
1465 t <- spaced (expr defaultSyntax)
1466 i <- get
1467 return $ tactic (desugar defaultSyntax i t)
1468 spaced parser = indentGt *> parser
1470-- | Parse module header and imports
1471parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark)
1472parseImports fname input
1473 = do i <- getIState
1474 case runparser imports i fname input of
1475 Left err -> ifail . show . parseErrorDoc $ err
1476 Right (x, annots, i) ->
1477 do putIState i
1478 fname' <- runIO $ Dir.makeAbsolute fname
1479 sendHighlighting $ addPath annots fname'
1480 return x
1481 where imports :: IdrisParser ((Maybe (Docstring ()), [String],
1482 [ImportInfo],
1483 Maybe Mark),
1484 [(FC, OutputAnnotation)], IState)
1485 imports = do optional shebang
1486 whiteSpace
1487 (mdoc, mname, annots) <- moduleHeader
1488 ps_exp <- many import_
1489 mrk <- mark
1490 isEof <- lookAheadMatches P.eof
1491 let mrk' = if isEof
1492 then Nothing
1493 else Just mrk
1494 i <- get
1495 -- add Builtins and Prelude, unless options say
1496 -- not to
1497 let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp
1498 return ((mdoc, mname, ps, mrk'), annots, i)
1500 addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]
1501 addPath [] _ = []
1502 addPath ((fc, AnnNamespace ns Nothing) : annots) path =
1503 (fc, AnnNamespace ns (Just path)) : addPath annots path
1504 addPath (annot:annots) path = annot : addPath annots path
1506 shebang :: IdrisParser ()
1507 shebang = string "#!" *> many (P.satisfy $ not . isEol) *> eol *> pure ()
1509-- | Check if the coloring matches the options and corrects if necessary
1510fixColour :: Bool -> PP.Doc -> PP.Doc
1511fixColour False doc = PP.plain doc
1512fixColour True doc = doc
1514-- | A program is a list of declarations, possibly with associated
1515-- documentation strings.
1516parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Mark -> Idris [PDecl]
1517parseProg syn fname input mrk
1518 = do i <- getIState
1519 case runparser mainProg i fname input of
1520 Left err -> do let fc = errorExtent err
1521 i <- getIState
1522 case idris_outputmode i of
1523 RawOutput h -> iputStrLn (show . fixColour (idris_colourRepl i) . parseErrorDoc $ err)
1524 IdeMode n h -> iWarn fc (Util.Pretty.text $ errorMessage err)
1525 putIState (i { errSpan = Just fc })
1526 return []
1527 Right (x, i) -> do putIState i
1528 reportParserWarnings
1529 return $ collect x
1530 where mainProg :: IdrisParser ([PDecl], IState)
1531 mainProg = case mrk of
1532 Nothing -> do i <- get; return ([], i)
1533 Just mrk -> do
1534 restore mrk
1535 ds <- prog syn
1536 i' <- get
1537 return (ds, i')
1539-- | Collect 'PClauses' with the same function name
1540collect :: [PDecl] -> [PDecl]
1541collect (c@(PClauses _ o _ _) : ds)
1542 = clauses (cname c) [] (c : ds)
1543 where clauses :: Maybe Name -> [PClause] -> [PDecl] -> [PDecl]
1544 clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)
1545 | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds
1546 clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r pn w] : ds)
1547 | n == n' = clauses j (PWith fc' n' l ws r pn (collect w) : acc) ds
1548 clauses (Just n) acc xs = PClauses (fcOf c) o n (reverse acc) : collect xs
1549 clauses Nothing acc (x:xs) = collect xs
1550 clauses Nothing acc [] = []
1552 cname :: PDecl -> Maybe Name
1553 cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n
1554 cname (PClauses fc _ _ [PWith _ n _ _ _ _ _]) = Just n
1555 cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing
1556 cname (PClauses fc _ _ [PWithR _ _ _ _ _]) = Nothing
1557 fcOf :: PDecl -> FC
1558 fcOf (PClauses fc _ _ _) = fc
1559collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
1560collect (POpenInterfaces f ns ps : ds) = POpenInterfaces f ns (collect ps) : collect ds
1561collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds
1562collect (PNamespace ns fc ps : ds) = PNamespace ns fc (collect ps) : collect ds
1563collect (PInterface doc f s cs n nfc ps pdocs fds ds cn cd : ds')
1564 = PInterface doc f s cs n nfc ps pdocs fds (collect ds) cn cd : collect ds'
1565collect (PImplementation doc argDocs f s cs pnames acc opts n nfc ps pextra t en ds : ds')
1566 = PImplementation doc argDocs f s cs pnames acc opts n nfc ps pextra t en (collect ds) : collect ds'
1567collect (d : ds) = d : collect ds
1568collect [] = []
1570{-| Load idris module and show error if something wrong happens -}
1571loadModule :: FilePath -> IBCPhase -> Idris (Maybe String)
1572loadModule f phase
1573 = idrisCatch (loadModule' f phase)
1574 (\e -> do setErrSpan (getErrSpan e)
1575 ist <- getIState
1576 iWarn (getErrSpan e) $ pprintErr ist e
1577 return Nothing)
1579{-| Load idris module -}
1580loadModule' :: FilePath -> IBCPhase -> Idris (Maybe String)
1581loadModule' f phase
1582 = do i <- getIState
1583 let file = takeWhile (/= ' ') f
1584 ibcsd <- valIBCSubDir i
1585 ids <- rankedImportDirs file
1586 fp <- findImport ids ibcsd file
1587 if file `elem` imported i
1588 then do logParser 1 $ "Already read " ++ file
1589 return Nothing
1590 else do putIState (i { imported = file : imported i })
1591 case fp of
1592 IDR fn -> loadSource False fn Nothing
1593 LIDR fn -> loadSource True fn Nothing
1594 IBC fn src ->
1595 idrisCatch (loadIBC True phase fn)
1596 (\c -> do logParser 1 $ fn ++ " failed " ++ pshow i c
1597 case src of
1598 IDR sfn -> loadSource False sfn Nothing
1599 LIDR sfn -> loadSource True sfn Nothing)
1600 return $ Just file
1602{-| Load idris code from file -}
1603loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()
1604loadFromIFile reexp phase i@(IBC fn src) maxline
1605 = do logParser 1 $ "Skipping " ++ getSrcFile i
1606 logParser 3 $ "loadFromIFile i" ++ show i
1607 idrisCatch (loadIBC reexp phase fn)
1608 (\err -> ierror $ LoadingFailed fn err)
1609 where
1610 getSrcFile (IDR fn) = fn
1611 getSrcFile (LIDR fn) = fn
1612 getSrcFile (IBC f src) = getSrcFile src
1614loadFromIFile _ _ (IDR fn) maxline = loadSource' False fn maxline
1615loadFromIFile _ _ (LIDR fn) maxline = loadSource' True fn maxline
1617{-| Load idris source code and show error if something wrong happens -}
1618loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1619loadSource' lidr r maxline
1620 = idrisCatch (loadSource lidr r maxline)
1621 (\e -> do setErrSpan (getErrSpan e)
1622 ist <- getIState
1623 case e of
1624 At f e' -> iWarn f (pprintErr ist e')
1625 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1627{-| Load Idris source code-}
1628loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1629loadSource lidr f toline
1630 = do logParser 1 ("Reading " ++ f)
1631 iReport 2 ("Reading " ++ f)
1632 i <- getIState
1633 let def_total = default_total i
1634 file_in <- runIO $ readSource f
1635 file <- if lidr then tclift $ unlit f file_in else return file_in
1636 (mdocs, mname, imports_in, pos) <- parseImports f file
1637 ai <- getAutoImports
1638 let imports = map (\n -> ImportInfo True n Nothing [] NoFC NoFC) ai ++ imports_in
1639 ids <- rankedImportDirs f
1640 ibcsd <- valIBCSubDir i
1641 mapM_ (\(re, f, ns, nfc) ->
1642 do fp <- findImport ids ibcsd f
1643 case fp of
1644 LIDR fn -> ifail $ "No ibc for " ++ f
1645 IDR fn -> ifail $ "No ibc for " ++ f
1646 IBC fn src ->
1647 do loadIBC True IBC_Building fn
1648 let srcFn = case src of
1649 IDR fn -> Just fn
1650 LIDR fn -> Just fn
1651 _ -> Nothing
1652 srcFnAbs <- case srcFn of
1653 Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)
1654 Nothing -> return Nothing
1655 sendHighlighting [(nfc, AnnNamespace ns srcFnAbs)])
1656 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]
1657 reportParserWarnings
1658 sendParserHighlighting
1660 -- process and check module aliases
1661 let modAliases = M.fromList
1662 [ (prep alias, prep realName)
1663 | ImportInfo { import_reexport = reexport
1664 , import_path = realName
1665 , import_rename = Just (alias, _)
1666 , import_location = fc } <- imports
1668 prep = map T.pack . reverse . Spl.splitOn [pathSeparator]
1669 aliasNames = [ (alias, fc)
1670 | ImportInfo { import_rename = Just (alias, fc)
1671 } <- imports
1673 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1674 case map head . filter ((/= 1) . length) $ histogram of
1675 [] -> logParser 3 $ "Module aliases: " ++ show (M.toList modAliases)
1676 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1678 i <- getIState
1679 putIState (i { default_access = Private, module_aliases = modAliases })
1680 clearIBC -- start a new .ibc file
1681 -- record package info in .ibc
1682 imps <- allImportDirs
1683 mapM_ addIBC (map IBCImportDir imps)
1684 mapM_ (addIBC . IBCImport)
1685 [ (reexport, realName)
1686 | ImportInfo { import_reexport = reexport
1687 , import_path = realName
1688 } <- imports
1690 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1691 maxline = toline }
1692 ist <- getIState
1693 -- Save the span from parsing the module header, because
1694 -- an empty program parse might obliterate it.
1695 let oldSpan = idris_parsedSpan ist
1696 ds' <- parseProg syntax f file pos
1698 case (ds', oldSpan) of
1699 ([], Just fc) ->
1700 -- If no program elements were parsed, we dind't
1701 -- get a loaded region in the IBC file. That
1702 -- means we need to add it back.
1703 do ist <- getIState
1704 putIState ist { idris_parsedSpan = oldSpan
1705 , ibc_write = IBCParsedRegion fc :
1706 ibc_write ist
1708 _ -> return ()
1709 sendParserHighlighting
1711 -- Parsing done, now process declarations
1713 let ds = namespaces mname ds'
1714 logParser 3 (show $ showDecls verbosePPOption ds)
1715 i <- getIState
1716 logLvl 10 (show (toAlist (idris_implicits i)))
1717 logLvl 3 (show (idris_infixes i))
1718 -- Now add all the declarations to the context
1719 iReport 1 $ "Type checking " ++ f
1720 -- we totality check after every Mutual block, so if
1721 -- anything is a single definition, wrap it in a
1722 -- mutual block on its own
1723 elabDecls (toplevelWith f) (map toMutual ds)
1724 i <- getIState
1725 -- simplify every definition do give the totality checker
1726 -- a better chance
1727 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1728 ctxt' <-
1729 do ctxt <- getContext
1730 tclift $ simplifyCasedef n [] [] (getErasureInfo i) ctxt
1731 setContext ctxt')
1732 (map snd (idris_totcheck i))
1733 -- build size change graph from simplified definitions
1734 iReport 3 $ "Totality checking " ++ f
1735 logLvl 1 $ "Totality checking " ++ f
1736 i <- getIState
1737 mapM_ buildSCG (idris_totcheck i)
1738 mapM_ checkDeclTotality (idris_totcheck i)
1739 mapM_ verifyTotality (idris_totcheck i)
1741 -- Redo totality check for deferred names
1742 let deftots = idris_defertotcheck i
1743 logLvl 2 $ "Totality checking " ++ show deftots
1744 mapM_ (\x -> do tot <- getTotality x
1745 case tot of
1746 Total _ ->
1747 do let opts = case lookupCtxtExact x (idris_flags i) of
1748 Just os -> os
1749 Nothing -> []
1750 when (AssertTotal `notElem` opts) $
1751 setTotality x Unchecked
1752 _ -> return ()) (map snd deftots)
1753 mapM_ buildSCG deftots
1754 mapM_ checkDeclTotality deftots
1756 logLvl 1 ("Finished " ++ f)
1757 ibcsd <- valIBCSubDir i
1758 logLvl 1 $ "Universe checking " ++ f
1759 iReport 3 $ "Universe checking " ++ f
1760 iucheck
1761 let ibc = ibcPathNoFallback ibcsd f
1762 i <- getIState
1763 addHides (hide_list i)
1765 -- Save module documentation if applicable
1766 i <- getIState
1767 case mdocs of
1768 Nothing -> return ()
1769 Just docs -> addModDoc syntax mname docs
1772 -- Finally, write an ibc and highlights if checking was successful
1773 ok <- noErrors
1774 when ok $
1775 do idrisCatch (do writeIBC f ibc; clearIBC)
1776 (\c -> return ()) -- failure is harmless
1777 hl <- getDumpHighlighting
1778 when hl $
1779 idrisCatch (writeHighlights f)
1780 (const $ return ()) -- failure is harmless
1781 clearHighlights
1782 i <- getIState
1783 putIState (i { default_total = def_total,
1784 hide_list = emptyContext })
1785 return ()
1786 where
1787 namespaces :: [String] -> [PDecl] -> [PDecl]
1788 namespaces [] ds = ds
1789 namespaces (x:xs) ds = [PNamespace x NoFC (namespaces xs ds)]
1791 toMutual :: PDecl -> PDecl
1792 toMutual m@(PMutual _ d) = m
1793 toMutual (PNamespace x fc ds) = PNamespace x fc (map toMutual ds)
1794 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1795 case x of
1796 PClauses{} -> r
1797 PInterface{} -> r
1798 PData{} -> r
1799 PImplementation{} -> r
1800 _ -> x
1802 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1803 addModDoc syn mname docs =
1804 do ist <- getIState
1805 docs' <- elabDocTerms (toplevelWith f) (parsedDocs ist)
1806 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1807 putIState ist { idris_moduledocs = modDocs' }
1808 addIBC (IBCModDocs docName)
1809 where
1810 docName = NS modDocName (map T.pack (reverse mname))
1811 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1813{-| Adds names to hide list -}
1814addHides :: Ctxt Accessibility -> Idris ()
1815addHides xs = mapM_ doHide (toAlist xs)
1816 where doHide (n, a) = do setAccessibility n a
1817 addIBC (IBCAccess n a)