git.iko.soy/Idris-dev
on bc8da8d help sign in
Idris-dev/src/Idris/Parser.hs
1831 lines 71 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 reservedHL "module"
89 (i, ifc) <- 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 <- getFC
120 reservedHL "import"
121 reexport <- P.option False (True <$ reservedHL "public")
122 (id, idfc) <- identifier
123 newName <- optional (do reservedHL "as"
124 identifier)
125 P.option ';' (lchar ';')
126 return $ ImportInfo reexport (toPath id)
127 (fmap (\(n, fc) -> (toPath n, fc)) newName)
128 (map T.pack $ ns id) fc idfc
129 <?> "import statement"
130 where ns = Spl.splitOn "."
131 toPath = foldl1' (</>) . ns
133{-| Parses program source
136 Prog ::= Decl* EOF;
138 -}
139prog :: SyntaxInfo -> IdrisParser [PDecl]
140prog syn = do whiteSpace
141 decls <- many (decl syn)
142 let c = concat decls
143 case maxline syn of
144 Nothing -> do notOpenBraces; P.eof
145 _ -> return ()
146 ist <- get
147 fc <- getFC
148 put ist { idris_parsedSpan = Just (FC (fc_fname fc) (0,0) (fc_end fc)),
149 ibc_write = IBCParsedRegion fc : ibc_write ist }
150 return c
152{-| Parses a top-level declaration
155Decl ::=
156 Decl'
157 | Using
158 | Params
159 | Mutual
160 | Namespace
161 | Interface
162 | Implementation
163 | DSL
164 | Directive
165 | Provider
166 | Transform
167 | Import!
168 | RunElabDecl
169 ;
171-}
172decl :: SyntaxInfo -> IdrisParser [PDecl]
173decl syn = P.try (externalDecl syn)
174 <|> internalDecl syn
175 <?> "declaration"
177internalDecl :: SyntaxInfo -> IdrisParser [PDecl]
178internalDecl syn
179 = do fc <- getFC
180 -- if we're after maxline, stop at the next type declaration
181 -- (so we get all cases of a definition to preserve totality
182 -- results, in particular).
183 let continue = case maxline syn of
184 Nothing -> True
185 Just l -> if fst (fc_end fc) > l
186 then mut_nesting syn /= 0
187 else True
188 -- What I'd really like to do here is explicitly save the
189 -- current state, then if reading ahead finds we've passed
190 -- the end of the definition, reset the state. But I've lost
191 -- patience with trying to find out how to do that from the
192 -- trifecta docs, so this does the job instead.
193 if continue then
194 do notEndBlock
195 declBody continue
196 else P.try (do notEndBlock
197 declBody continue)
198 <|> fail "End of readable input"
199 where declBody :: Bool -> IdrisParser [PDecl]
200 declBody b =
201 P.try (implementation True syn)
202 <|> P.try (openInterface syn)
203 <|> declBody' b
204 <|> using_ syn
205 <|> params syn
206 <|> mutual syn
207 <|> namespace syn
208 <|> interface_ syn
209 <|> do d <- dsl syn; return [d]
210 <|> directive syn
211 <|> provider syn
212 <|> transform syn
213 <|> do import_; fail "imports must be at top of file"
214 <?> "declaration"
215 declBody' :: Bool -> IdrisParser [PDecl]
216 declBody' cont = do d <- decl' syn
217 i <- get
218 let d' = fmap (debindApp syn . (desugar syn i)) d
219 if continue cont d'
220 then return [d']
221 else fail "End of readable input"
223 -- Keep going while we're still parsing clauses
224 continue False (PClauses _ _ _ _) = True
225 continue c _ = c
227{-| Parses a top-level declaration with possible syntax sugar
230Decl' ::=
231 Fixity
232 | FunDecl'
233 | Data
234 | Record
235 | SyntaxDecl
236 ;
238-}
239decl' :: SyntaxInfo -> IdrisParser PDecl
240decl' syn = fixity
241 <|> syntaxDecl syn
242 <|> fnDecl' syn
243 <|> data_ syn
244 <|> record syn
245 <|> runElabDecl syn
246 <?> "declaration"
248externalDecl :: SyntaxInfo -> IdrisParser [PDecl]
249externalDecl syn = do i <- get
250 notEndBlock
251 FC fn start _ <- getFC
252 decls <- declExtensions syn (syntaxRulesList $ syntax_rules i)
253 FC _ _ end <- getFC
254 let outerFC = FC fn start end
255 return $ map (mapPDeclFC (fixFC outerFC)
256 (fixFCH fn outerFC))
257 decls
258 where
259 -- | Fix non-highlighting FCs to prevent spurious error location reports
260 fixFC :: FC -> FC -> FC
261 fixFC outer inner | inner `fcIn` outer = inner
262 | otherwise = outer
263 -- | Fix highlighting FCs by obliterating them, to avoid spurious highlights
264 fixFCH fn outer inner | inner `fcIn` outer = inner
265 | otherwise = FileFC fn
267declExtensions :: SyntaxInfo -> [Syntax] -> IdrisParser [PDecl]
268declExtensions syn rules = declExtension syn [] (filter isDeclRule rules)
269 <?> "user-defined declaration"
270 where
271 isDeclRule (DeclRule _ _) = True
272 isDeclRule _ = False
274declExtension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax]
275 -> IdrisParser [PDecl]
276declExtension syn ns rules =
277 P.choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->
278 case head rs of -- can never be []
279 DeclRule (symb:_) _ -> P.try $ do
280 n <- extSymbol symb
281 declExtension syn (n : ns) [DeclRule ss t | (DeclRule (_:ss) t) <- rs]
282 -- If we have more than one Rule in this bucket, our grammar is
283 -- nondeterministic.
284 DeclRule [] dec -> let r = map (update (mapMaybe id ns)) dec in
285 return r
287 where
288 update :: [(Name, SynMatch)] -> PDecl -> PDecl
289 update ns = updateNs ns . fmap (updateRefs ns) . fmap (updateSynMatch ns)
291 updateRefs ns = mapPT newref
292 where
293 newref (PRef fc fcs n) = PRef fc fcs (updateB ns n)
294 newref t = t
296 -- Below is a lot of tedious boilerplate which updates any top level
297 -- names in the declaration. It will only change names which are bound in
298 -- the declaration (including method names in interfaces and field names in
299 -- record declarations, not including pattern variables)
300 updateB :: [(Name, SynMatch)] -> Name -> Name
301 updateB ns (NS n mods) = NS (updateB ns n) mods
302 updateB ns n = case lookup n ns of
303 Just (SynBind tfc t) -> t
304 _ -> n
306 updateNs :: [(Name, SynMatch)] -> PDecl -> PDecl
307 updateNs ns (PTy doc argdoc s fc o n fc' t)
308 = PTy doc argdoc s fc o (updateB ns n) fc' t
309 updateNs ns (PClauses fc o n cs)
310 = PClauses fc o (updateB ns n) (map (updateClause ns) cs)
311 updateNs ns (PCAF fc n t) = PCAF fc (updateB ns n) t
312 updateNs ns (PData ds cds s fc o dat)
313 = PData ds cds s fc o (updateData ns dat)
314 updateNs ns (PParams fc ps ds) = PParams fc ps (map (updateNs ns) ds)
315 updateNs ns (PNamespace s fc ds) = PNamespace s fc (map (updateNs ns) ds)
316 updateNs ns (PRecord doc syn fc o n fc' ps pdocs fields cname cdoc s)
317 = PRecord doc syn fc o (updateB ns n) fc' ps pdocs
318 (map (updateField ns) fields)
319 (updateRecCon ns cname)
320 cdoc
321 s
322 updateNs ns (PInterface docs s fc cs cn fc' ps pdocs pdets ds cname cdocs)
323 = PInterface docs s fc cs (updateB ns cn) fc' ps pdocs pdets
324 (map (updateNs ns) ds)
325 (updateRecCon ns cname)
326 cdocs
327 updateNs ns (PImplementation docs pdocs s fc cs pnames acc opts cn fc' ps pextra ity ni ds)
328 = PImplementation docs pdocs s fc cs pnames acc opts (updateB ns cn) fc'
329 ps pextra ity (fmap (updateB ns) ni)
330 (map (updateNs ns) ds)
331 updateNs ns (PMutual fc ds) = PMutual fc (map (updateNs ns) ds)
332 updateNs ns (PProvider docs s fc fc' pw n)
333 = PProvider docs s fc fc' pw (updateB ns n)
334 updateNs ns d = d
336 updateRecCon ns Nothing = Nothing
337 updateRecCon ns (Just (n, fc)) = Just (updateB ns n, fc)
339 updateField ns (m, p, t, doc) = (updateRecCon ns m, p, t, doc)
341 updateClause ns (PClause fc n t ts t' ds)
342 = PClause fc (updateB ns n) t ts t' (map (update ns) ds)
343 updateClause ns (PWith fc n t ts t' m ds)
344 = PWith fc (updateB ns n) t ts t' m (map (update ns) ds)
345 updateClause ns (PClauseR fc ts t ds)
346 = PClauseR fc ts t (map (update ns) ds)
347 updateClause ns (PWithR fc ts t m ds)
348 = PWithR fc ts t m (map (update ns) ds)
350 updateData ns (PDatadecl n fc t cs)
351 = PDatadecl (updateB ns n) fc t (map (updateCon ns) cs)
352 updateData ns (PLaterdecl n fc t)
353 = PLaterdecl (updateB ns n) fc t
355 updateCon ns (cd, ads, cn, fc, ty, fc', fns)
356 = (cd, ads, updateB ns cn, fc, ty, fc', fns)
358 ruleGroup [] [] = True
359 ruleGroup (s1:_) (s2:_) = s1 == s2
360 ruleGroup _ _ = False
362 extSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
363 extSymbol (Keyword n) = do fc <- reservedFC (show n)
364 highlightP fc AnnKeyword
365 return Nothing
366 extSymbol (Expr n) = do tm <- expr syn
367 return $ Just (n, SynTm tm)
368 extSymbol (SimpleExpr n) = do tm <- simpleExpr syn
369 return $ Just (n, SynTm tm)
370 extSymbol (Binding n) = do (b, fc) <- name
371 return $ Just (n, SynBind fc b)
372 extSymbol (Symbol s) = do fc <- symbolFC s
373 highlightP fc AnnKeyword
374 return Nothing
376{-| Parses a syntax extension declaration (and adds the rule to parser state)
379 SyntaxDecl ::= SyntaxRule;
381-}
382syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
383syntaxDecl syn = do s <- syntaxRule syn
384 i <- get
385 put (i `addSyntax` s)
386 fc <- getFC
387 return (PSyntax fc s)
389-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.
390addSyntax :: IState -> Syntax -> IState
391addSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
392 syntax_keywords = ks ++ ns,
393 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc }
394 where rs = syntax_rules i
395 ns = syntax_keywords i
396 ibc = ibc_write i
397 ks = map show (syntaxNames s)
399-- | Like 'addSyntax', but no effect on the IBC.
400addReplSyntax :: IState -> Syntax -> IState
401addReplSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
402 syntax_keywords = ks ++ ns }
403 where rs = syntax_rules i
404 ns = syntax_keywords i
405 ks = map show (syntaxNames s)
407{-| Parses a syntax extension declaration
410SyntaxRuleOpts ::= 'term' | 'pattern';
414SyntaxRule ::=
415 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
419SyntaxSym ::= '[' Name_t ']'
420 | '{' Name_t '}'
421 | Name_t
422 | StringLiteral_t
423 ;
425-}
426syntaxRule :: SyntaxInfo -> IdrisParser Syntax
427syntaxRule syn
428 = do sty <- P.try (do
429 pushIndent
430 sty <- P.option AnySyntax
431 (TermSyntax <$ reservedHL "term"
432 <|> PatternSyntax <$ reservedHL "pattern")
433 reservedHL "syntax"
434 return sty)
435 syms <- some syntaxSym
436 when (all isExpr syms) $ P.unexpected . P.Label . NonEmpty.fromList $ "missing keywords in syntax rule"
437 let ns = mapMaybe getName syms
438 when (length ns /= length (nub ns))
439 $ P.unexpected . P.Label . NonEmpty.fromList $ "repeated variable in syntax rule"
440 lchar '='
441 tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]
442 terminator
443 return (Rule (mkSimple syms) tm sty)
444 <|> do reservedHL "decl"; reservedHL "syntax"
445 syms <- some syntaxSym
446 when (all isExpr syms) $ P.unexpected . P.Label . NonEmpty.fromList $ "missing keywords in syntax rule"
447 let ns = mapMaybe getName syms
448 when (length ns /= length (nub ns))
449 $ P.unexpected . P.Label . NonEmpty.fromList $ "repeated variable in syntax rule"
450 lchar '='
451 openBlock
452 dec <- some (decl syn)
453 closeBlock
454 return (DeclRule (mkSimple syms) (concat dec))
455 where
456 isExpr (Expr _) = True
457 isExpr _ = False
458 getName (Expr n) = Just n
459 getName _ = Nothing
460 -- Can't parse two full expressions (i.e. expressions with application) in a row
461 -- so change them both to a simple expression
462 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
463 mkSimple xs = mkSimple' xs
465 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
466 mkSimple es
467 -- Can't parse a full expression followed by operator like characters due to ambiguity
468 mkSimple' (Expr e : Symbol s : es)
469 | takeWhile (`elem` opChars) ts /= "" = SimpleExpr e : Symbol s : mkSimple' es
470 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s
471 mkSimple' (e : es) = e : mkSimple' es
472 mkSimple' [] = []
474 -- Prevent syntax variable capture by making all binders under syntax unique
475 -- (the ol' Common Lisp GENSYM approach)
476 uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
477 uniquifyBinders userNames = fixBind 0 []
478 where
479 fixBind :: Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
480 fixBind 0 rens (PRef fc hls n) | Just n' <- lookup n rens =
481 return $ PRef fc hls n'
482 fixBind 0 rens (PPatvar fc n) | Just n' <- lookup n rens =
483 return $ PPatvar fc n'
484 fixBind 0 rens (PLam fc n nfc ty body)
485 | n `elem` userNames = liftM2 (PLam fc n nfc)
486 (fixBind 0 rens ty)
487 (fixBind 0 rens body)
488 | otherwise =
489 do ty' <- fixBind 0 rens ty
490 n' <- gensym n
491 body' <- fixBind 0 ((n,n'):rens) body
492 return $ PLam fc n' nfc ty' body'
493 fixBind 0 rens (PPi plic n nfc argTy body)
494 | n `elem` userNames = liftM2 (PPi plic n nfc)
495 (fixBind 0 rens argTy)
496 (fixBind 0 rens body)
497 | otherwise =
498 do ty' <- fixBind 0 rens argTy
499 n' <- gensym n
500 body' <- fixBind 0 ((n,n'):rens) body
501 return $ (PPi plic n' nfc ty' body')
502 fixBind 0 rens (PLet fc rig n nfc ty val body)
503 | n `elem` userNames = liftM3 (PLet fc rig n nfc)
504 (fixBind 0 rens ty)
505 (fixBind 0 rens val)
506 (fixBind 0 rens body)
507 | otherwise =
508 do ty' <- fixBind 0 rens ty
509 val' <- fixBind 0 rens val
510 n' <- gensym n
511 body' <- fixBind 0 ((n,n'):rens) body
512 return $ PLet fc rig n' nfc ty' val' body'
513 fixBind 0 rens (PMatchApp fc n) | Just n' <- lookup n rens =
514 return $ PMatchApp fc n'
515 -- Also rename resolved quotations, to allow syntax rules to
516 -- have quoted references to their own bindings.
517 fixBind 0 rens (PQuoteName n True fc) | Just n' <- lookup n rens =
518 return $ PQuoteName n' True fc
520 -- Don't mess with quoted terms
521 fixBind q rens (PQuasiquote tm goal) =
522 flip PQuasiquote goal <$> fixBind (q + 1) rens tm
523 fixBind q rens (PUnquote tm) =
524 PUnquote <$> fixBind (q - 1) rens tm
526 fixBind q rens x = descendM (fixBind q rens) x
528 gensym :: Name -> IdrisParser Name
529 gensym n = do ist <- get
530 let idx = idris_name ist
531 put ist { idris_name = idx + 1 }
532 return $ sMN idx (show n)
534{-| Parses a syntax symbol (either binding variable, keyword or expression)
537SyntaxSym ::= '[' Name_t ']'
538 | '{' Name_t '}'
539 | Name_t
540 | StringLiteral_t
541 ;
543 -}
544syntaxSym :: IdrisParser SSymbol
545syntaxSym = P.try (do lchar '['; n <- fst <$> name; lchar ']'
546 return (Expr n))
547 <|> P.try (do lchar '{'; n <- fst <$> name; lchar '}'
548 return (Binding n))
549 <|> do n <- fst <$> iName []
550 return (Keyword n)
551 <|> do sym <- fmap fst stringLiteral
552 return (Symbol sym)
553 <?> "syntax symbol"
555{-| Parses a function declaration with possible syntax sugar
558 FunDecl ::= FunDecl';
560-}
561fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
562fnDecl syn = P.try (do notEndBlock
563 d <- fnDecl' syn
564 i <- get
565 let d' = fmap (desugar syn i) d
566 return [d']) <?> "function declaration"
568{-| Parses a function declaration
571 FunDecl' ::=
572 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
573 | Postulate
574 | Pattern
575 | CAF
576 ;
578-}
579fnDecl' :: SyntaxInfo -> IdrisParser PDecl
580fnDecl' syn = (checkDeclFixity $
581 do (doc, argDocs, fc, opts', n, nfc, acc) <- P.try (do
582 pushIndent
583 (doc, argDocs) <- docstring syn
584 (opts, acc) <- fnOpts
585 (n_in, nfc) <- fnName
586 let n = expandNS syn n_in
587 fc <- getFC
588 lchar ':'
589 return (doc, argDocs, fc, opts, n, nfc, acc))
590 ty <- typeExpr (allowImp syn)
591 terminator
592 -- If it's a top level function, note the accessibility
593 -- rules
594 when (syn_toplevel syn) $ addAcc n acc
595 return (PTy doc argDocs syn fc opts' n nfc ty)
596 <|> postulate syn
597 <|> caf syn
598 <|> pattern syn)
599 <?> "function declaration"
601{-| Parses a series of function and accessbility options
604FnOpts ::= FnOpt* Accessibility FnOpt*
606 -}
607fnOpts :: IdrisParser ([FnOpt], Accessibility)
608fnOpts = do
609 opts <- many fnOpt
610 acc <- accessibility
611 opts' <- many fnOpt
612 let allOpts = opts ++ opts'
613 let existingTotality = allOpts `intersect` [TotalFn, CoveringFn, PartialFn]
614 opts'' <- addDefaultTotality (nub existingTotality) allOpts
615 return (opts'', acc)
616 where prettyTot TotalFn = "total"
617 prettyTot PartialFn = "partial"
618 prettyTot CoveringFn = "covering"
619 addDefaultTotality [] opts = do
620 ist <- get
621 case default_total ist of
622 DefaultCheckingTotal -> return (TotalFn:opts)
623 DefaultCheckingCovering -> return (CoveringFn:opts)
624 DefaultCheckingPartial -> return opts -- Don't add partial so that --warn-partial still reports warnings if necessary
625 addDefaultTotality [tot] opts = return opts
626 -- Should really be a semantics error instead of a parser error
627 addDefaultTotality (tot1:tot2:tots) opts =
628 fail ("Conflicting totality modifiers specified " ++ prettyTot tot1 ++ " and " ++ prettyTot tot2)
631{-| Parses a function option
634FnOpt ::= 'total'
635 | 'partial'
636 | 'covering'
637 | 'implicit'
638 | '%' 'no_implicit'
639 | '%' 'assert_total'
640 | '%' 'error_handler'
641 | '%' 'reflection'
642 | '%' 'specialise' '[' NameTimesList? ']'
643 ;
647NameTimes ::= FnName Natural?;
651NameTimesList ::=
652 NameTimes
653 | NameTimes ',' NameTimesList
654 ;
656-}
657fnOpt :: IdrisParser FnOpt
658fnOpt = do reservedHL "total"; return TotalFn
659 <|> PartialFn <$ reservedHL "partial"
660 <|> CoveringFn <$ reservedHL "covering"
661 <|> do P.try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;
662 return $ CExport c
663 <|> NoImplicit <$ P.try (lchar '%' *> reserved "no_implicit")
664 <|> Inlinable <$ P.try (lchar '%' *> reserved "inline")
665 <|> StaticFn <$ P.try (lchar '%' *> reserved "static")
666 <|> do P.try (lchar '%' *> reserved "assert_total");
667 fc <- getFC
668 parserWarning fc Nothing (Msg "%assert_total is deprecated. Use the 'assert_total' function instead.")
669 return AssertTotal
670 <|> ErrorHandler <$ P.try (lchar '%' *> reserved "error_handler")
671 <|> ErrorReverse <$ P.try (lchar '%' *> reserved "error_reverse")
672 <|> ErrorReduce <$ P.try (lchar '%' *> reserved "error_reduce")
673 <|> Reflection <$ P.try (lchar '%' *> reserved "reflection")
674 <|> AutoHint <$ P.try (lchar '%' *> reserved "hint")
675 <|> OverlappingDictionary <$ P.try (lchar '%' *> reserved "overlapping")
676 <|> do lchar '%'; reserved "specialise";
677 lchar '['; ns <- P.sepBy nameTimes (lchar ','); lchar ']';
678 return $ Specialise ns
679 <|> Implicit <$ reservedHL "implicit"
680 <?> "function modifier"
681 where nameTimes :: IdrisParser (Name, Maybe Int)
682 nameTimes = do n <- fst <$> fnName
683 t <- P.option Nothing (do reds <- fmap fst natural
684 return (Just (fromInteger reds)))
685 return (n, t)
687{-| Parses a postulate
690Postulate ::=
691 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
692 ;
694-}
695postulate :: SyntaxInfo -> IdrisParser PDecl
696postulate syn = do (doc, ext)
697 <- P.try $ do (doc, _) <- docstring syn
698 pushIndent
699 ext <- ppostDecl
700 return (doc, ext)
701 ist <- get
702 (opts, acc) <- fnOpts
703 (n_in, nfc) <- fnName
704 let n = expandNS syn n_in
705 lchar ':'
706 ty <- typeExpr (allowImp syn)
707 fc <- getFC
708 terminator
709 addAcc n acc
710 return (PPostulate ext doc syn fc nfc opts n ty)
711 <?> "postulate"
712 where ppostDecl = do fc <- reservedHL "postulate"; return False
713 <|> do lchar '%'; reserved "extern"; return True
715{-| Parses a using declaration
718Using ::=
719 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
720 ;
722 -}
723using_ :: SyntaxInfo -> IdrisParser [PDecl]
724using_ syn =
725 do reservedHL "using"
726 lchar '('; ns <- usingDeclList syn; lchar ')'
727 openBlock
728 let uvars = using syn
729 ds <- many (decl (syn { using = uvars ++ ns }))
730 closeBlock
731 return (concat ds)
732 <?> "using declaration"
734{-| Parses a parameters declaration
737Params ::=
738 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
739 ;
741-}
742params :: SyntaxInfo -> IdrisParser [PDecl]
743params syn =
744 do reservedHL "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
745 let ns' = [(n, ty) | (_, n, _, ty) <- ns]
746 openBlock
747 let pvars = syn_params syn
748 ds <- many (decl syn { syn_params = pvars ++ ns' })
749 closeBlock
750 fc <- getFC
751 return [PParams fc ns' (concat ds)]
752 <?> "parameters declaration"
754-- | Parses an open block
755openInterface :: SyntaxInfo -> IdrisParser [PDecl]
756openInterface syn =
757 do reservedHL "using"
758 reservedHL "implementation"
759 fc <- getFC
760 ns <- P.sepBy1 fnName (lchar ',')
762 openBlock
763 ds <- many (decl syn)
764 closeBlock
765 return [POpenInterfaces fc (map fst ns) (concat ds)]
766 <?> "open interface declaration"
772{-| Parses a mutual declaration (for mutually recursive functions)
775Mutual ::=
776 'mutual' OpenBlock Decl* CloseBlock
777 ;
779-}
780mutual :: SyntaxInfo -> IdrisParser [PDecl]
781mutual syn =
782 do reservedHL "mutual"
783 openBlock
784 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
785 closeBlock
786 fc <- getFC
787 return [PMutual fc (concat ds)]
788 <?> "mutual block"
790{-| Parses a namespace declaration
793Namespace ::=
794 'namespace' identifier OpenBlock Decl+ CloseBlock
795 ;
797-}
798namespace :: SyntaxInfo -> IdrisParser [PDecl]
799namespace syn =
800 do reservedHL "namespace"
801 (n, nfc) <- identifier
802 openBlock
803 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
804 closeBlock
805 return [PNamespace n nfc (concat ds)]
806 <?> "namespace declaration"
808{-| Parses a methods block (for implementations)
811 ImplementationBlock ::= 'where' OpenBlock FnDecl* CloseBlock
813-}
814implementationBlock :: SyntaxInfo -> IdrisParser [PDecl]
815implementationBlock syn = do reservedHL "where"
816 openBlock
817 ds <- many (fnDecl syn)
818 closeBlock
819 return (concat ds)
820 <?> "implementation block"
822{-| Parses a methods and implementations block (for interfaces)
825MethodOrImplementation ::=
826 FnDecl
827 | Implementation
828 ;
832InterfaceBlock ::=
833 'where' OpenBlock Constructor? MethodOrImplementation* CloseBlock
834 ;
836-}
837interfaceBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])
838interfaceBlock syn = do reservedHL "where"
839 openBlock
840 (cn, cd) <- P.option (Nothing, emptyDocstring) $
841 P.try (do (doc, _) <- P.option noDocs docComment
842 n <- constructor
843 return (Just n, doc))
844 ist <- get
845 let cd' = annotate syn ist cd
847 ds <- many (notEndBlock >> P.try (implementation True syn)
848 <|> do x <- data_ syn
849 return [x]
850 <|> fnDecl syn)
851 closeBlock
852 return (cn, cd', concat ds)
853 <?> "interface block"
854 where
855 constructor :: IdrisParser (Name, FC)
856 constructor = reservedHL "constructor" *> fnName
858 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)
859 annotate syn ist = annotCode $ tryFullExpr syn ist
861{-| Parses an interface declaration
864InterfaceArgument ::=
865 Name
866 | '(' Name ':' Expr ')'
867 ;
871Interface ::=
872 DocComment_t? Accessibility? 'interface' ConstraintList? Name InterfaceArgument* InterfaceBlock?
873 ;
875-}
876interface_ :: SyntaxInfo -> IdrisParser [PDecl]
877interface_ syn = do (doc, argDocs, acc)
878 <- P.try (do (doc, argDocs) <- docstring syn
879 acc <- accessibility
880 interfaceKeyword
881 return (doc, argDocs, acc))
882 fc <- getFC
883 cons <- constraintList syn
884 let cons' = [(c, ty) | (_, c, _, ty) <- cons]
885 (n_in, nfc) <- fnName
886 let n = expandNS syn n_in
887 cs <- many carg
888 fds <- P.option [(cn, NoFC) | (cn, _, _) <- cs] fundeps
889 (cn, cd, ds) <- P.option (Nothing, fst noDocs, []) (interfaceBlock syn)
890 accData acc n (concatMap declared ds)
891 return [PInterface doc syn fc cons' n nfc cs argDocs fds ds cn cd]
892 <?> "interface declaration"
893 where
894 fundeps :: IdrisParser [(Name, FC)]
895 fundeps = do lchar '|'; P.sepBy name (lchar ',')
897 interfaceKeyword :: IdrisParser ()
898 interfaceKeyword = reservedHL "interface"
899 <|> do reservedHL "class"
900 fc <- getFC
901 parserWarning fc Nothing (Msg "The 'class' keyword is deprecated. Use 'interface' instead.")
903 carg :: IdrisParser (Name, FC, PTerm)
904 carg = do lchar '('; (i, ifc) <- name; lchar ':'; ty <- expr syn; lchar ')'
905 return (i, ifc, ty)
906 <|> do (i, ifc) <- name
907 fc <- getFC
908 return (i, ifc, PType fc)
910{-| Parses an interface implementation declaration
913 Implementation ::=
914 DocComment_t? 'implementation' ImplementationName? ConstraintList? Name SimpleExpr* ImplementationBlock?
915 ;
919ImplementationName ::= '[' Name ']';
921-}
922implementation :: Bool -> SyntaxInfo -> IdrisParser [PDecl]
923implementation kwopt syn
924 = do ist <- get
925 (doc, argDocs) <- docstring syn
926 (opts, acc) <- fnOpts
927 if kwopt then optional implementationKeyword
928 else do implementationKeyword
929 return (Just ())
931 fc <- getFC
932 en <- optional implementationName
933 cs <- constraintList syn
934 let cs' = [(c, ty) | (_, c, _, ty) <- cs]
935 (cn, cnfc) <- fnName
936 args <- many (simpleExpr syn)
937 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)
938 let t = bindList (\r -> PPi constraint { pcount = r }) cs sc
939 pnames <- implementationUsing
940 ds <- implementationBlock syn
941 return [PImplementation doc argDocs syn fc cs' pnames acc opts cn cnfc args [] t en ds]
942 <?> "implementation declaration"
943 where implementationName :: IdrisParser Name
944 implementationName = do lchar '['; n_in <- fst <$> fnName; lchar ']'
945 let n = expandNS syn n_in
946 return n
947 <?> "implementation name"
948 implementationKeyword :: IdrisParser ()
949 implementationKeyword = reservedHL "implementation"
950 <|> do reservedHL "instance"
951 fc <- getFC
952 parserWarning fc Nothing (Msg "The 'instance' keyword is deprecated. Use 'implementation' (or omit it) instead.")
954 implementationUsing :: IdrisParser [Name]
955 implementationUsing = do reservedHL "using"
956 ns <- P.sepBy1 fnName (lchar ',')
957 return (map fst ns)
958 <|> return []
960-- | Parse a docstring
961docstring :: SyntaxInfo
962 -> IdrisParser (Docstring (Either Err PTerm),
963 [(Name,Docstring (Either Err PTerm))])
964docstring syn = do (doc, argDocs) <- P.option noDocs docComment
965 ist <- get
966 let doc' = annotCode (tryFullExpr syn ist) doc
967 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
968 | (n, d) <- argDocs ]
969 return (doc', argDocs')
972{-| Parses a using declaration list
975UsingDeclList ::=
976 UsingDeclList'
977 | NameList TypeSig
978 ;
982UsingDeclList' ::=
983 UsingDecl
984 | UsingDecl ',' UsingDeclList'
985 ;
989NameList ::=
990 Name
991 | Name ',' NameList
992 ;
994-}
995usingDeclList :: SyntaxInfo -> IdrisParser [Using]
996usingDeclList syn
997 = P.try (P.sepBy1 (usingDecl syn) (lchar ','))
998 <|> do ns <- P.sepBy1 (fst <$> name) (lchar ',')
999 lchar ':'
1000 t <- typeExpr (disallowImp syn)
1001 return (map (\x -> UImplicit x t) ns)
1002 <?> "using declaration list"
1004{-| Parses a using declaration
1007UsingDecl ::=
1008 FnName TypeSig
1009 | FnName FnName+
1013usingDecl :: SyntaxInfo -> IdrisParser Using
1014usingDecl syn = P.try (do x <- fst <$> fnName
1015 lchar ':'
1016 t <- typeExpr (disallowImp syn)
1017 return (UImplicit x t))
1018 <|> do c <- fst <$> fnName
1019 xs <- many (fst <$> fnName)
1020 return (UConstraint c xs)
1021 <?> "using declaration"
1023{-| Parse a clause with patterns
1026Pattern ::= Clause;
1029pattern :: SyntaxInfo -> IdrisParser PDecl
1030pattern syn = do fc <- getFC
1031 clause <- clause syn
1032 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
1033 <?> "pattern"
1035{-| Parse a constant applicative form declaration
1038CAF ::= 'let' FnName '=' Expr Terminator;
1041caf :: SyntaxInfo -> IdrisParser PDecl
1042caf syn = do reservedHL "let"
1043 n_in <- fst <$> fnName; let n = expandNS syn n_in
1044 pushIndent
1045 lchar '='
1046 t <- indented $ expr syn
1047 terminator
1048 fc <- getFC
1049 return (PCAF fc n t)
1050 <?> "constant applicative form declaration"
1052{-| Parse an argument expression
1055ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
1058argExpr :: SyntaxInfo -> IdrisParser PTerm
1059argExpr syn = let syn' = syn { inPattern = True } in
1060 P.try (hsimpleExpr syn') <|> simpleExternalExpr syn'
1061 <?> "argument expression"
1063{-| Parse a right hand side of a function
1066RHS ::= '=' Expr
1067 | '?=' RHSName? Expr
1068 | Impossible
1073RHSName ::= '{' FnName '}';
1076rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
1077rhs syn n = do lchar '='
1078 indentGt
1079 expr syn
1080 <|> do symbol "?=";
1081 fc <- getFC
1082 name <- P.option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";
1083 return n)
1084 r <- expr syn
1085 return (addLet fc name r)
1086 <|> impossible
1087 <?> "function right hand side"
1088 where mkN :: Name -> Name
1089 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
1090 then sUN "infix_op_lemma_1"
1091 else sUN (str x++"_lemma_1")
1092 mkN (NS x n) = NS (mkN x) n
1093 n' :: Name
1094 n' = mkN n
1095 addLet :: FC -> Name -> PTerm -> PTerm
1096 addLet fc nm (PLet fc' rig n nfc ty val r) = PLet fc' rig n nfc ty val (addLet fc nm r)
1097 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
1098 where addLetC (l, r) = (l, addLet fc nm r)
1099 addLet fc nm r = (PLet fc RigW (sUN "value") NoFC Placeholder r (PMetavar NoFC nm))
1101{-|Parses a function clause
1104RHSOrWithBlock ::= RHS WhereOrTerminator
1105 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
1110Clause ::= WExpr+ RHSOrWithBlock
1111 | SimpleExpr '<==' FnName RHS WhereOrTerminator
1112 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
1113 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
1118ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
1122WhereOrTerminator ::= WhereBlock | Terminator;
1125clause :: SyntaxInfo -> IdrisParser PClause
1126clause syn
1127 = do wargs <- P.try (do pushIndent; some (wExpr syn))
1128 fc <- getFC
1129 ist <- get
1130 n <- case lastParse ist of
1131 Just t -> return t
1132 Nothing -> fail "Invalid clause"
1133 (do r <- rhs syn n
1134 let wsyn = syn { syn_namespace = [], syn_toplevel = False }
1135 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1136 <|> ([], []) <$ terminator
1137 return $ PClauseR fc wargs r wheres) <|> (do
1138 popIndent
1139 reservedHL "with"
1140 wval <- simpleExpr syn
1141 pn <- optProof
1142 openBlock
1143 ds <- some $ fnDecl syn
1144 let withs = concat ds
1145 closeBlock
1146 return $ PWithR fc wargs wval pn withs)
1147 <|> do ty <- P.try (do pushIndent
1148 ty <- simpleExpr syn
1149 symbol "<=="
1150 return ty)
1151 fc <- getFC
1152 n_in <- fst <$> fnName; let n = expandNS syn n_in
1153 r <- rhs syn n
1154 let wsyn = syn { syn_namespace = [] }
1155 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1156 <|> ([], []) <$ terminator
1157 let capp = PLet fc RigW (sMN 0 "match") NoFC
1158 ty
1159 (PMatchApp fc n)
1160 (PRef fc [] (sMN 0 "match"))
1161 ist <- get
1162 put (ist { lastParse = Just n })
1163 return $ PClause fc n capp [] r wheres
1164 <|> do (l, op, nfc) <- P.try (do
1165 pushIndent
1166 l <- argExpr syn
1167 (op, nfc) <- symbolicOperatorFC
1168 when (op == "=" || op == "?=" ) $
1169 fail "infix clause definition with \"=\" and \"?=\" not supported "
1170 return (l, op, nfc))
1171 let n = expandNS syn (sUN op)
1172 r <- argExpr syn
1173 fc <- getFC
1174 wargs <- many (wExpr syn)
1175 (do rs <- rhs syn n
1176 let wsyn = syn { syn_namespace = [] }
1177 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1178 <|> ([], []) <$ terminator
1179 ist <- get
1180 let capp = PApp fc (PRef nfc [nfc] n) [pexp l, pexp r]
1181 put (ist { lastParse = Just n })
1182 return $ PClause fc n capp wargs rs wheres) <|> (do
1183 popIndent
1184 reservedHL "with"
1185 wval <- bracketed syn
1186 pn <- optProof
1187 openBlock
1188 ds <- some $ fnDecl syn
1189 closeBlock
1190 ist <- get
1191 let capp = PApp fc (PRef fc [] n) [pexp l, pexp r]
1192 let withs = map (fillLHSD n capp wargs) $ concat ds
1193 put (ist { lastParse = Just n })
1194 return $ PWith fc n capp wargs wval pn withs)
1195 <|> do pushIndent
1196 (n_in, nfc) <- fnName; let n = expandNS syn n_in
1197 fc <- getFC
1198 args <- many (P.try (implicitArg (syn { inPattern = True } ))
1199 <|> P.try (constraintArg (syn { inPattern = True }))
1200 <|> (fmap pexp (argExpr syn)))
1201 wargs <- many (wExpr syn)
1202 let capp = PApp fc (PRef nfc [nfc] n) args
1203 (do r <- rhs syn n
1204 let wsyn = syn { syn_namespace = [] }
1205 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1206 <|> ([], []) <$ terminator
1207 ist <- get
1208 put (ist { lastParse = Just n })
1209 return $ PClause fc n capp wargs r wheres) <|> (do
1210 reservedHL "with"
1211 ist <- get
1212 put (ist { lastParse = Just n })
1213 wval <- bracketed syn
1214 pn <- optProof
1215 openBlock
1216 ds <- some $ fnDecl syn
1217 let withs = map (fillLHSD n capp wargs) $ concat ds
1218 closeBlock
1219 popIndent
1220 return $ PWith fc n capp wargs wval pn withs)
1221 <?> "function clause"
1222 where
1223 optProof = P.option Nothing (do reservedHL "proof"
1224 n <- fnName
1225 return (Just n))
1227 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
1228 fillLHS n capp owargs (PClauseR fc wargs v ws)
1229 = PClause fc n capp (owargs ++ wargs) v ws
1230 fillLHS n capp owargs (PWithR fc wargs v pn ws)
1231 = PWith fc n capp (owargs ++ wargs) v pn
1232 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1233 fillLHS _ _ _ c = c
1235 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
1236 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1237 fillLHSD n c a x = x
1239{-| Parses with pattern
1242WExpr ::= '|' Expr';
1245wExpr :: SyntaxInfo -> IdrisParser PTerm
1246wExpr syn = do lchar '|'
1247 expr' (syn { inPattern = True })
1248 <?> "with pattern"
1250{-| Parses a where block
1253WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
1256whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
1257whereBlock n syn
1258 = do reservedHL "where"
1259 ds <- indentedBlock1 (decl syn)
1260 let dns = concatMap (concatMap declared) ds
1261 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1262 <?> "where block"
1264{-|Parses a code generation target language name
1267Codegen ::= 'C'
1268 | 'Java'
1269 | 'JavaScript'
1270 | 'Node'
1271 | 'LLVM'
1272 | 'Bytecode'
1276codegen_ :: IdrisParser Codegen
1277codegen_ = do n <- fst <$> identifier
1278 return (Via IBCFormat (map toLower n))
1279 <|> do reserved "Bytecode"; return Bytecode
1280 <?> "code generation language"
1282{-|Parses a compiler directive
1284StringList ::=
1285 String
1286 | String ',' StringList
1291Directive ::= '%' Directive';
1295Directive' ::= 'lib' CodeGen String_t
1296 | 'link' CodeGen String_t
1297 | 'flag' CodeGen String_t
1298 | 'include' CodeGen String_t
1299 | 'hide' Name
1300 | 'freeze' Name
1301 | 'thaw' Name
1302 | 'access' Accessibility
1303 | 'default' Totality
1304 | 'logging' Natural
1305 | 'dynamic' StringList
1306 | 'name' Name NameList
1307 | 'error_handlers' Name NameList
1308 | 'language' 'TypeProviders'
1309 | 'language' 'ErrorReflection'
1310 | 'deprecated' Name String
1311 | 'fragile' Name Reason
1315directive :: SyntaxInfo -> IdrisParser [PDecl]
1316directive syn = do P.try (lchar '%' *> reserved "lib")
1317 cgn <- codegen_
1318 lib <- fmap fst stringLiteral
1319 return [PDirective (DLib cgn lib)]
1320 <|> do P.try (lchar '%' *> reserved "link")
1321 cgn <- codegen_; obj <- fst <$> stringLiteral
1322 return [PDirective (DLink cgn obj)]
1323 <|> do P.try (lchar '%' *> reserved "flag")
1324 cgn <- codegen_; flag <- fst <$> stringLiteral
1325 return [PDirective (DFlag cgn flag)]
1326 <|> do P.try (lchar '%' *> reserved "include")
1327 cgn <- codegen_
1328 hdr <- fst <$> stringLiteral
1329 return [PDirective (DInclude cgn hdr)]
1330 <|> do P.try (lchar '%' *> reserved "hide"); n <- fst <$> fnName
1331 return [PDirective (DHide n)]
1332 <|> do P.try (lchar '%' *> reserved "freeze"); n <- fst <$> iName []
1333 return [PDirective (DFreeze n)]
1334 <|> do P.try (lchar '%' *> reserved "thaw"); n <- fst <$> iName []
1335 return [PDirective (DThaw n)]
1336 -- injectivity assertins are intended for debugging purposes
1337 -- only, and won't be documented/could be removed at any point
1338 <|> do P.try (lchar '%' *> reserved "assert_injective"); n <- fst <$> fnName
1339 return [PDirective (DInjective n)]
1340 -- Assert totality of something after definition. This is
1341 -- here as a debugging aid, so commented out...
1342-- <|> do P.try (lchar '%' *> reserved "assert_set_total"); n <- fst <$> fnName
1343-- return [PDirective (DSetTotal n)]
1344 <|> do P.try (lchar '%' *> reserved "access")
1345 acc <- accessibility
1346 ist <- get
1347 put ist { default_access = acc }
1348 return [PDirective (DAccess acc)]
1349 <|> do P.try (lchar '%' *> reserved "default"); tot <- totality
1350 i <- get
1351 put (i { default_total = tot } )
1352 return [PDirective (DDefault tot)]
1353 <|> do P.try (lchar '%' *> reserved "logging")
1354 i <- fst <$> natural
1355 return [PDirective (DLogging i)]
1356 <|> do P.try (lchar '%' *> reserved "dynamic")
1357 libs <- P.sepBy1 (fmap fst stringLiteral) (lchar ',')
1358 return [PDirective (DDynamicLibs libs)]
1359 <|> do P.try (lchar '%' *> reserved "name")
1360 (ty, tyFC) <- fnName
1361 ns <- P.sepBy1 name (lchar ',')
1362 return [PDirective (DNameHint ty tyFC ns)]
1363 <|> do P.try (lchar '%' *> reserved "error_handlers")
1364 (fn, nfc) <- fnName
1365 (arg, afc) <- fnName
1366 ns <- P.sepBy1 name (lchar ',')
1367 return [PDirective (DErrorHandlers fn nfc arg afc ns) ]
1368 <|> do P.try (lchar '%' *> reserved "language"); ext <- pLangExt;
1369 return [PDirective (DLanguage ext)]
1370 <|> do P.try (lchar '%' *> reserved "deprecate")
1371 n <- fst <$> fnName
1372 alt <- P.option "" (fst <$> stringLiteral)
1373 return [PDirective (DDeprecate n alt)]
1374 <|> do P.try (lchar '%' *> reserved "fragile")
1375 n <- fst <$> fnName
1376 alt <- P.option "" (fst <$> stringLiteral)
1377 return [PDirective (DFragile n alt)]
1378 <|> do fc <- getFC
1379 P.try (lchar '%' *> reserved "used")
1380 fn <- fst <$> fnName
1381 arg <- fst <$> iName []
1382 return [PDirective (DUsed fc fn arg)]
1383 <|> do P.try (lchar '%' *> reserved "auto_implicits")
1384 b <- on_off
1385 return [PDirective (DAutoImplicits b)]
1386 <?> "directive"
1387 where on_off = do reserved "on"; return True
1388 <|> do reserved "off"; return False
1390pLangExt :: IdrisParser LanguageExt
1391pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1392 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1393 <|> (reserved "UniquenessTypes" >> return UniquenessTypes)
1394 <|> (reserved "LinearTypes" >> return LinearTypes)
1395 <|> (reserved "DSLNotation" >> return DSLNotation)
1396 <|> (reserved "ElabReflection" >> return ElabReflection)
1397 <|> (reserved "FirstClassReflection" >> return FCReflection)
1399{-| Parses a totality
1402Totality ::= 'partial' | 'total' | 'covering'
1406totality :: IdrisParser DefaultTotality
1407totality
1408 = do reservedHL "total"; return DefaultCheckingTotal
1409 <|> do reservedHL "partial"; return DefaultCheckingPartial
1410 <|> do reservedHL "covering"; return DefaultCheckingCovering
1412{-| Parses a type provider
1415Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1416ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1418 -}
1419provider :: SyntaxInfo -> IdrisParser [PDecl]
1420provider syn = do doc <- P.try (do (doc, _) <- docstring syn
1421 fc1 <- getFC
1422 lchar '%'
1423 fc2 <- reservedFC "provide"
1424 highlightP (spanFC fc1 fc2) AnnKeyword
1425 return doc)
1426 provideTerm doc <|> providePostulate doc
1427 <?> "type provider"
1428 where provideTerm doc =
1429 do lchar '('; (n, nfc) <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1430 fc <- getFC
1431 reservedHL "with"
1432 e <- expr syn <?> "provider expression"
1433 return [PProvider doc syn fc nfc (ProvTerm t e) n]
1434 providePostulate doc =
1435 do reservedHL "postulate"
1436 (n, nfc) <- fnName
1437 fc <- getFC
1438 reservedHL "with"
1439 e <- expr syn <?> "provider expression"
1440 return [PProvider doc syn fc nfc (ProvPostulate e) n]
1442{-| Parses a transform
1445Transform ::= '%' 'transform' Expr '==>' Expr
1448transform :: SyntaxInfo -> IdrisParser [PDecl]
1449transform syn = do P.try (lchar '%' *> reserved "transform")
1450 -- leave it unchecked, until we work out what this should
1451 -- actually mean...
1452-- safety <- option True (do reserved "unsafe"
1453-- return False)
1454 l <- expr syn
1455 fc <- getFC
1456 symbol "==>"
1457 r <- expr syn
1458 return [PTransform fc False l r]
1459 <?> "transform"
1461{-| Parses a top-level reflected elaborator script
1464RunElabDecl ::= '%' 'runElab' Expr
1467runElabDecl :: SyntaxInfo -> IdrisParser PDecl
1468runElabDecl syn =
1469 do kwFC <- P.try (do fc <- getFC
1470 lchar '%'
1471 fc' <- reservedFC "runElab"
1472 return (spanFC fc fc'))
1473 script <- expr syn <?> "elaborator script"
1474 highlightP kwFC AnnKeyword
1475 return $ PRunElabDecl kwFC script (syn_namespace syn)
1476 <?> "top-level elaborator script"
1478{- * Loading and parsing -}
1479{-| Parses an expression from input -}
1480parseExpr :: IState -> String -> Either ParseError PTerm
1481parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1483{-| Parses a constant form input -}
1484parseConst :: IState -> String -> Either ParseError Const
1485parseConst st = runparser (fmap fst constant) st "(input)"
1487{-| Parses a tactic from input -}
1488parseTactic :: IState -> String -> Either ParseError PTactic
1489parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1491{-| Parses a do-step from input (used in the elab shell) -}
1492parseElabShellStep :: IState -> String -> Either ParseError (Either ElabShellCmd PDo)
1493parseElabShellStep ist = runparser (Right <$> do_ defaultSyntax <|> Left <$> elabShellCmd) ist "(input)"
1494 where elabShellCmd = char ':' >>
1495 (reserved "qed" >> pure EQED ) <|>
1496 (reserved "abandon" >> pure EAbandon ) <|>
1497 (reserved "undo" >> pure EUndo ) <|>
1498 (reserved "state" >> pure EProofState) <|>
1499 (reserved "term" >> pure EProofTerm ) <|>
1500 (expressionTactic ["e", "eval"] EEval ) <|>
1501 (expressionTactic ["t", "type"] ECheck) <|>
1502 (expressionTactic ["search"] ESearch ) <|>
1503 (do reserved "doc"
1504 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)
1505 P.eof
1506 return (EDocStr doc))
1507 <?> "elab command"
1508 expressionTactic cmds tactic =
1509 do asum (map reserved cmds)
1510 t <- spaced (expr defaultSyntax)
1511 i <- get
1512 return $ tactic (desugar defaultSyntax i t)
1513 spaced parser = indentGt *> parser
1515-- | Parse module header and imports
1516parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe ParseState)
1517parseImports fname input
1518 = do i <- getIState
1519 case runparser imports i fname input of
1520 Left err -> ifail . show . parseErrorDoc $ err
1521 Right (x, annots, i) ->
1522 do putIState i
1523 fname' <- runIO $ Dir.makeAbsolute fname
1524 sendHighlighting $ addPath annots fname'
1525 return x
1526 where imports :: IdrisParser ((Maybe (Docstring ()), [String],
1527 [ImportInfo],
1528 Maybe ParseState),
1529 [(FC, OutputAnnotation)], IState)
1530 imports = do optional shebang
1531 whiteSpace
1532 (mdoc, mname, annots) <- moduleHeader
1533 ps_exp <- many import_
1534 mrk <- P.getParserState
1535 isEof <- lookAheadMatches P.eof
1536 let mrk' = if isEof
1537 then Nothing
1538 else Just mrk
1539 i <- get
1540 -- add Builtins and Prelude, unless options say
1541 -- not to
1542 let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp
1543 return ((mdoc, mname, ps, mrk'), annots, i)
1545 addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]
1546 addPath [] _ = []
1547 addPath ((fc, AnnNamespace ns Nothing) : annots) path =
1548 (fc, AnnNamespace ns (Just path)) : addPath annots path
1549 addPath (annot:annots) path = annot : addPath annots path
1551 shebang :: IdrisParser ()
1552 shebang = string "#!" *> many (P.satisfy $ not . isEol) *> eol *> pure ()
1554-- | Check if the coloring matches the options and corrects if necessary
1555fixColour :: Bool -> PP.Doc -> PP.Doc
1556fixColour False doc = PP.plain doc
1557fixColour True doc = doc
1559-- | A program is a list of declarations, possibly with associated
1560-- documentation strings.
1561parseProg :: SyntaxInfo -> FilePath -> String -> Maybe ParseState -> Idris [PDecl]
1562parseProg syn fname input mrk
1563 = do i <- getIState
1564 case runparser mainProg i fname input of
1565 Left err -> do let fc = parseErrorFC err
1566 i <- getIState
1567 case idris_outputmode i of
1568 RawOutput h -> iputStrLn (show . fixColour (idris_colourRepl i) . parseErrorDoc $ err)
1569 IdeMode n h -> iWarn fc (Util.Pretty.text $ parseErrorMessage err)
1570 putIState (i { errSpan = Just fc })
1571 return []
1572 Right (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 P.setParserState 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 <- rankedImportDirs file
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 logParser 3 $ "loadFromIFile i" ++ show i
1621 idrisCatch (loadIBC reexp phase fn)
1622 (\err -> ierror $ LoadingFailed fn err)
1623 where
1624 getSrcFile (IDR fn) = fn
1625 getSrcFile (LIDR fn) = fn
1626 getSrcFile (IBC f src) = getSrcFile src
1628loadFromIFile _ _ (IDR fn) maxline = loadSource' False fn maxline
1629loadFromIFile _ _ (LIDR fn) maxline = loadSource' True fn maxline
1631{-| Load idris source code and show error if something wrong happens -}
1632loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1633loadSource' lidr r maxline
1634 = idrisCatch (loadSource lidr r maxline)
1635 (\e -> do setErrSpan (getErrSpan e)
1636 ist <- getIState
1637 case e of
1638 At f e' -> iWarn f (pprintErr ist e')
1639 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1641{-| Load Idris source code-}
1642loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1643loadSource lidr f toline
1644 = do logParser 1 ("Reading " ++ f)
1645 iReport 2 ("Reading " ++ f)
1646 i <- getIState
1647 let def_total = default_total i
1648 file_in <- runIO $ readSource f
1649 file <- if lidr then tclift $ unlit f file_in else return file_in
1650 (mdocs, mname, imports_in, pos) <- parseImports f file
1651 ai <- getAutoImports
1652 let imports = map (\n -> ImportInfo True n Nothing [] NoFC NoFC) ai ++ imports_in
1653 ids <- rankedImportDirs f
1654 ibcsd <- valIBCSubDir i
1655 mapM_ (\(re, f, ns, nfc) ->
1656 do fp <- findImport ids ibcsd f
1657 case fp of
1658 LIDR fn -> ifail $ "No ibc for " ++ f
1659 IDR fn -> ifail $ "No ibc for " ++ f
1660 IBC fn src ->
1661 do loadIBC True IBC_Building fn
1662 let srcFn = case src of
1663 IDR fn -> Just fn
1664 LIDR fn -> Just fn
1665 _ -> Nothing
1666 srcFnAbs <- case srcFn of
1667 Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)
1668 Nothing -> return Nothing
1669 sendHighlighting [(nfc, AnnNamespace ns srcFnAbs)])
1670 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]
1671 reportParserWarnings
1672 sendParserHighlighting
1674 -- process and check module aliases
1675 let modAliases = M.fromList
1676 [ (prep alias, prep realName)
1677 | ImportInfo { import_reexport = reexport
1678 , import_path = realName
1679 , import_rename = Just (alias, _)
1680 , import_location = fc } <- imports
1682 prep = map T.pack . reverse . Spl.splitOn [pathSeparator]
1683 aliasNames = [ (alias, fc)
1684 | ImportInfo { import_rename = Just (alias, _)
1685 , import_location = fc } <- imports
1687 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1688 case map head . filter ((/= 1) . length) $ histogram of
1689 [] -> logParser 3 $ "Module aliases: " ++ show (M.toList modAliases)
1690 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1692 i <- getIState
1693 putIState (i { default_access = Private, module_aliases = modAliases })
1694 clearIBC -- start a new .ibc file
1695 -- record package info in .ibc
1696 imps <- allImportDirs
1697 mapM_ addIBC (map IBCImportDir imps)
1698 mapM_ (addIBC . IBCImport)
1699 [ (reexport, realName)
1700 | ImportInfo { import_reexport = reexport
1701 , import_path = realName
1702 } <- imports
1704 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1705 maxline = toline }
1706 ist <- getIState
1707 -- Save the span from parsing the module header, because
1708 -- an empty program parse might obliterate it.
1709 let oldSpan = idris_parsedSpan ist
1710 ds' <- parseProg syntax f file pos
1712 case (ds', oldSpan) of
1713 ([], Just fc) ->
1714 -- If no program elements were parsed, we dind't
1715 -- get a loaded region in the IBC file. That
1716 -- means we need to add it back.
1717 do ist <- getIState
1718 putIState ist { idris_parsedSpan = oldSpan
1719 , ibc_write = IBCParsedRegion fc :
1720 ibc_write ist
1722 _ -> return ()
1723 sendParserHighlighting
1725 -- Parsing done, now process declarations
1727 let ds = namespaces mname ds'
1728 logParser 3 (show $ showDecls verbosePPOption ds)
1729 i <- getIState
1730 logLvl 10 (show (toAlist (idris_implicits i)))
1731 logLvl 3 (show (idris_infixes i))
1732 -- Now add all the declarations to the context
1733 iReport 1 $ "Type checking " ++ f
1734 -- we totality check after every Mutual block, so if
1735 -- anything is a single definition, wrap it in a
1736 -- mutual block on its own
1737 elabDecls (toplevelWith f) (map toMutual ds)
1738 i <- getIState
1739 -- simplify every definition do give the totality checker
1740 -- a better chance
1741 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1742 ctxt' <-
1743 do ctxt <- getContext
1744 tclift $ simplifyCasedef n [] [] (getErasureInfo i) ctxt
1745 setContext ctxt')
1746 (map snd (idris_totcheck i))
1747 -- build size change graph from simplified definitions
1748 iReport 3 $ "Totality checking " ++ f
1749 logLvl 1 $ "Totality checking " ++ f
1750 i <- getIState
1751 mapM_ buildSCG (idris_totcheck i)
1752 mapM_ checkDeclTotality (idris_totcheck i)
1753 mapM_ verifyTotality (idris_totcheck i)
1755 -- Redo totality check for deferred names
1756 let deftots = idris_defertotcheck i
1757 logLvl 2 $ "Totality checking " ++ show deftots
1758 mapM_ (\x -> do tot <- getTotality x
1759 case tot of
1760 Total _ ->
1761 do let opts = case lookupCtxtExact x (idris_flags i) of
1762 Just os -> os
1763 Nothing -> []
1764 when (AssertTotal `notElem` opts) $
1765 setTotality x Unchecked
1766 _ -> return ()) (map snd deftots)
1767 mapM_ buildSCG deftots
1768 mapM_ checkDeclTotality deftots
1770 logLvl 1 ("Finished " ++ f)
1771 ibcsd <- valIBCSubDir i
1772 logLvl 1 $ "Universe checking " ++ f
1773 iReport 3 $ "Universe checking " ++ f
1774 iucheck
1775 let ibc = ibcPathNoFallback ibcsd f
1776 i <- getIState
1777 addHides (hide_list i)
1779 -- Save module documentation if applicable
1780 i <- getIState
1781 case mdocs of
1782 Nothing -> return ()
1783 Just docs -> addModDoc syntax mname docs
1786 -- Finally, write an ibc and highlights if checking was successful
1787 ok <- noErrors
1788 when ok $
1789 do idrisCatch (do writeIBC f ibc; clearIBC)
1790 (\c -> return ()) -- failure is harmless
1791 hl <- getDumpHighlighting
1792 when hl $
1793 idrisCatch (writeHighlights f)
1794 (const $ return ()) -- failure is harmless
1795 clearHighlights
1796 i <- getIState
1797 putIState (i { default_total = def_total,
1798 hide_list = emptyContext })
1799 return ()
1800 where
1801 namespaces :: [String] -> [PDecl] -> [PDecl]
1802 namespaces [] ds = ds
1803 namespaces (x:xs) ds = [PNamespace x NoFC (namespaces xs ds)]
1805 toMutual :: PDecl -> PDecl
1806 toMutual m@(PMutual _ d) = m
1807 toMutual (PNamespace x fc ds) = PNamespace x fc (map toMutual ds)
1808 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1809 case x of
1810 PClauses{} -> r
1811 PInterface{} -> r
1812 PData{} -> r
1813 PImplementation{} -> r
1814 _ -> x
1816 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1817 addModDoc syn mname docs =
1818 do ist <- getIState
1819 docs' <- elabDocTerms (toplevelWith f) (parsedDocs ist)
1820 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1821 putIState ist { idris_moduledocs = modDocs' }
1822 addIBC (IBCModDocs docName)
1823 where
1824 docName = NS modDocName (map T.pack (reverse mname))
1825 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1827{-| Adds names to hide list -}
1828addHides :: Ctxt Accessibility -> Idris ()
1829addHides xs = mapM_ doHide (toAlist xs)
1830 where doHide (n, a) = do setAccessibility n a
1831 addIBC (IBCAccess n a)