git.iko.soy/Idris-dev
on d3badf2 help sign in
Idris-dev/src/Idris/Parser.hs
1830 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(..), moduleName, 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 Util.System (readSource)
41import Prelude hiding (pi)
43import Control.Applicative hiding (Const)
44import Control.Monad
45import Control.Monad.State.Strict
46import Data.Char
47import Data.Foldable (asum)
48import Data.Function
49import Data.Generics.Uniplate.Data (descendM)
50import Data.List
51import qualified Data.List.NonEmpty as NonEmpty
52import qualified Data.List.Split as Spl
53import qualified Data.Map as M
54import Data.Maybe
55import Data.Ord
56import qualified Data.Text as T
57import qualified System.Directory as Dir (makeAbsolute)
58import System.FilePath
59import Text.Megaparsec ((<?>))
60import qualified Text.Megaparsec as P
61import qualified Text.Megaparsec.Char as P
62import qualified Text.PrettyPrint.ANSI.Leijen as PP
64{-
66 grammar shortcut notation:
67 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)
68 RULE? = optional rule (i.e. RULE or nothing)
69 RULE* = repeated rule (i.e. RULE zero or more times)
70 RULE+ = repeated rule with at least one match (i.e. RULE one or more times)
71 RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)
72 RULE{n} = rule repeated n times
74-}
76{- * Main grammar -}
78{-| Parses module definition
81 ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;
83-}
86moduleName :: Parsing m => m Name
87moduleName = mkName [] . map T.pack <$> moduleNamePieces where
89 mkName :: [T.Text] -> [T.Text] -> Name
90 mkName ts [x] = if null ts then UN x else NS (UN x) ts
91 mkName ts (x:xs) = mkName (x : ts) xs
93moduleNamePieces :: Parsing m => m [String]
94moduleNamePieces = Spl.splitOn "." <$> identifier
96moduleHeader :: IdrisParser (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
97moduleHeader = P.try (do docs <- optional docComment
98 noArgs docs
99 keyword "module"
100 (modName, ifc) <- withExtent moduleNamePieces
101 P.option ';' (lchar ';')
102 return (fmap fst docs,
103 modName,
104 [(ifc, AnnNamespace (map T.pack modName) Nothing)]))
105 <|> P.try (do lchar '%'; reserved "unqualified"
106 return (Nothing, [], []))
107 <|> return (Nothing, ["Main"], [])
108 where noArgs (Just (_, args)) | not (null args) = fail "Modules do not take arguments"
109 noArgs _ = return ()
111data ImportInfo = ImportInfo { import_reexport :: Bool
112 , import_path :: FilePath
113 , import_rename :: Maybe (String, FC)
114 , import_namespace :: [T.Text]
115 , import_location :: FC
116 , import_modname_location :: FC
117 }
119{-| Parses an import statement
122 Import ::= 'import' Identifier_t ';'?;
124 -}
125import_ :: IdrisParser ImportInfo
126import_ = do fc <- extent $ keyword "import"
127 reexport <- P.option False (True <$ keyword "public")
128 (ns, idfc) <- withExtent moduleNamePieces
129 newName <- optional (do keyword "as"
130 withExtent identifier)
131 P.option ';' (lchar ';')
132 return $ ImportInfo reexport (toPath ns)
133 (fmap (\(n, fc) -> (toPath (Spl.splitOn "." n), fc)) newName)
134 (map T.pack ns) fc idfc
135 <?> "import statement"
136 where toPath = foldl1' (</>)
138{-| Parses program source
141 Prog ::= Decl* EOF;
143 -}
144prog :: SyntaxInfo -> IdrisParser [PDecl]
145prog syn = do (decls, fc) <- withExtent $ do
146 whiteSpace
147 decls <- concat <$> many (decl syn)
148 case maxline syn of
149 Nothing -> do notOpenBraces; P.eof
150 _ -> return ()
151 return decls
152 ist <- get
153 put ist { idris_parsedSpan = Just (FC (fc_fname fc) (0,0) (fc_end fc)),
154 ibc_write = IBCParsedRegion fc : ibc_write ist }
155 return decls
157{-| Parses a top-level declaration
160Decl ::=
161 Decl'
162 | Using
163 | Params
164 | Mutual
165 | Namespace
166 | Interface
167 | Implementation
168 | DSL
169 | Directive
170 | Provider
171 | Transform
172 | Import!
173 | RunElabDecl
174 ;
176-}
177decl :: SyntaxInfo -> IdrisParser [PDecl]
178decl syn = P.try (externalDecl syn)
179 <|> internalDecl syn
180 <?> "declaration"
182internalDecl :: SyntaxInfo -> IdrisParser [PDecl]
183internalDecl syn
184 = do fc <- getFC
185 -- if we're after maxline, stop at the next type declaration
186 -- (so we get all cases of a definition to preserve totality
187 -- results, in particular).
188 let continue = case maxline syn of
189 Nothing -> True
190 Just l -> if fst (fc_end fc) > l
191 then mut_nesting syn /= 0
192 else True
193 -- What I'd really like to do here is explicitly save the
194 -- current state, then if reading ahead finds we've passed
195 -- the end of the definition, reset the state. But I've lost
196 -- patience with trying to find out how to do that from the
197 -- trifecta docs, so this does the job instead.
198 if continue then
199 do notEndBlock
200 declBody continue
201 else P.try (do notEndBlock
202 declBody continue)
203 <|> fail "End of readable input"
204 where declBody :: Bool -> IdrisParser [PDecl]
205 declBody b =
206 P.try (implementation syn)
207 <|> P.try (openInterface syn)
208 <|> declBody' b
209 <|> using_ syn
210 <|> params syn
211 <|> mutual syn
212 <|> namespace syn
213 <|> interface_ syn
214 <|> do d <- dsl syn; return [d]
215 <|> directive syn
216 <|> provider syn
217 <|> transform syn
218 <|> do import_; fail "imports must be at top of file"
219 <?> "declaration"
220 declBody' :: Bool -> IdrisParser [PDecl]
221 declBody' cont = do d <- decl' syn
222 i <- get
223 let d' = fmap (debindApp syn . (desugar syn i)) d
224 if continue cont d'
225 then return [d']
226 else fail "End of readable input"
228 -- Keep going while we're still parsing clauses
229 continue False (PClauses _ _ _ _) = True
230 continue c _ = c
232{-| Parses a top-level declaration with possible syntax sugar
235Decl' ::=
236 Fixity
237 | FunDecl'
238 | Data
239 | Record
240 | SyntaxDecl
241 ;
243-}
244decl' :: SyntaxInfo -> IdrisParser PDecl
245decl' syn = fixity
246 <|> syntaxDecl syn
247 <|> fnDecl' syn
248 <|> data_ syn
249 <|> record syn
250 <|> runElabDecl syn
251 <?> "declaration"
253externalDecl :: SyntaxInfo -> IdrisParser [PDecl]
254externalDecl syn = do i <- get
255 notEndBlock
256 (decls, fc@(FC fn _ _)) <- withExtent $ declExtensions syn (syntaxRulesList $ syntax_rules i)
257 return $ map (mapPDeclFC (fixFC fc) (fixFCH fn fc)) 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) = Nothing <$ keyword (show n)
364 extSymbol (Expr n) = do tm <- expr syn
365 return $ Just (n, SynTm tm)
366 extSymbol (SimpleExpr n) = do tm <- simpleExpr syn
367 return $ Just (n, SynTm tm)
368 extSymbol (Binding n) = do (b, fc) <- withExtent name
369 return $ Just (n, SynBind fc b)
370 extSymbol (Symbol s) = Nothing <$ highlight AnnKeyword (symbol s)
372{-| Parses a syntax extension declaration (and adds the rule to parser state)
375 SyntaxDecl ::= SyntaxRule;
377-}
378syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
379syntaxDecl syn = do (s, fc) <- withExtent $ syntaxRule syn
380 modify $ \i -> i `addSyntax` s
381 return (PSyntax fc s)
383-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.
384addSyntax :: IState -> Syntax -> IState
385addSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
386 syntax_keywords = ks ++ ns,
387 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc }
388 where rs = syntax_rules i
389 ns = syntax_keywords i
390 ibc = ibc_write i
391 ks = map show (syntaxNames s)
393-- | Like 'addSyntax', but no effect on the IBC.
394addReplSyntax :: IState -> Syntax -> IState
395addReplSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
396 syntax_keywords = ks ++ ns }
397 where rs = syntax_rules i
398 ns = syntax_keywords i
399 ks = map show (syntaxNames s)
401{-| Parses a syntax extension declaration
404SyntaxRuleOpts ::= 'term' | 'pattern';
408SyntaxRule ::=
409 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
413SyntaxSym ::= '[' Name_t ']'
414 | '{' Name_t '}'
415 | Name_t
416 | StringLiteral_t
417 ;
419-}
420syntaxRule :: SyntaxInfo -> IdrisParser Syntax
421syntaxRule syn
422 = do sty <- P.try (do
423 pushIndent
424 sty <- P.option AnySyntax
425 (TermSyntax <$ keyword "term"
426 <|> PatternSyntax <$ keyword "pattern")
427 keyword "syntax"
428 return sty)
429 syms <- some syntaxSym
430 when (all isExpr syms) $ P.unexpected . P.Label . NonEmpty.fromList $ "missing keywords in syntax rule"
431 let ns = mapMaybe getName syms
432 when (length ns /= length (nub ns))
433 $ P.unexpected . P.Label . NonEmpty.fromList $ "repeated variable in syntax rule"
434 lchar '='
435 tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]
436 terminator
437 return (Rule (mkSimple syms) tm sty)
438 <|> do keyword "decl"; keyword "syntax"
439 syms <- some syntaxSym
440 when (all isExpr syms) $ P.unexpected . P.Label . NonEmpty.fromList $ "missing keywords in syntax rule"
441 let ns = mapMaybe getName syms
442 when (length ns /= length (nub ns))
443 $ P.unexpected . P.Label . NonEmpty.fromList $ "repeated variable in syntax rule"
444 lchar '='
445 openBlock
446 dec <- some (decl syn)
447 closeBlock
448 return (DeclRule (mkSimple syms) (concat dec))
449 where
450 isExpr (Expr _) = True
451 isExpr _ = False
452 getName (Expr n) = Just n
453 getName _ = Nothing
454 -- Can't parse two full expressions (i.e. expressions with application) in a row
455 -- so change them both to a simple expression
456 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
457 mkSimple xs = mkSimple' xs
459 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
460 mkSimple es
461 -- Can't parse a full expression followed by operator like characters due to ambiguity
462 mkSimple' (Expr e : Symbol s : es)
463 | takeWhile (`elem` opChars) ts /= "" = SimpleExpr e : Symbol s : mkSimple' es
464 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s
465 mkSimple' (e : es) = e : mkSimple' es
466 mkSimple' [] = []
468 -- Prevent syntax variable capture by making all binders under syntax unique
469 -- (the ol' Common Lisp GENSYM approach)
470 uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
471 uniquifyBinders userNames = fixBind 0 []
472 where
473 fixBind :: Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
474 fixBind 0 rens (PRef fc hls n) | Just n' <- lookup n rens =
475 return $ PRef fc hls n'
476 fixBind 0 rens (PPatvar fc n) | Just n' <- lookup n rens =
477 return $ PPatvar fc n'
478 fixBind 0 rens (PLam fc n nfc ty body)
479 | n `elem` userNames = liftM2 (PLam fc n nfc)
480 (fixBind 0 rens ty)
481 (fixBind 0 rens body)
482 | otherwise =
483 do ty' <- fixBind 0 rens ty
484 n' <- gensym n
485 body' <- fixBind 0 ((n,n'):rens) body
486 return $ PLam fc n' nfc ty' body'
487 fixBind 0 rens (PPi plic n nfc argTy body)
488 | n `elem` userNames = liftM2 (PPi plic n nfc)
489 (fixBind 0 rens argTy)
490 (fixBind 0 rens body)
491 | otherwise =
492 do ty' <- fixBind 0 rens argTy
493 n' <- gensym n
494 body' <- fixBind 0 ((n,n'):rens) body
495 return $ (PPi plic n' nfc ty' body')
496 fixBind 0 rens (PLet fc rig n nfc ty val body)
497 | n `elem` userNames = liftM3 (PLet fc rig n nfc)
498 (fixBind 0 rens ty)
499 (fixBind 0 rens val)
500 (fixBind 0 rens body)
501 | otherwise =
502 do ty' <- fixBind 0 rens ty
503 val' <- fixBind 0 rens val
504 n' <- gensym n
505 body' <- fixBind 0 ((n,n'):rens) body
506 return $ PLet fc rig n' nfc ty' val' body'
507 fixBind 0 rens (PMatchApp fc n) | Just n' <- lookup n rens =
508 return $ PMatchApp fc n'
509 -- Also rename resolved quotations, to allow syntax rules to
510 -- have quoted references to their own bindings.
511 fixBind 0 rens (PQuoteName n True fc) | Just n' <- lookup n rens =
512 return $ PQuoteName n' True fc
514 -- Don't mess with quoted terms
515 fixBind q rens (PQuasiquote tm goal) =
516 flip PQuasiquote goal <$> fixBind (q + 1) rens tm
517 fixBind q rens (PUnquote tm) =
518 PUnquote <$> fixBind (q - 1) rens tm
520 fixBind q rens x = descendM (fixBind q rens) x
522 gensym :: Name -> IdrisParser Name
523 gensym n = do ist <- get
524 let idx = idris_name ist
525 put ist { idris_name = idx + 1 }
526 return $ sMN idx (show n)
528{-| Parses a syntax symbol (either binding variable, keyword or expression)
531SyntaxSym ::= '[' Name_t ']'
532 | '{' Name_t '}'
533 | Name_t
534 | StringLiteral_t
535 ;
537 -}
538syntaxSym :: IdrisParser SSymbol
539syntaxSym = P.try (do lchar '['; n <- name; lchar ']'
540 return (Expr n))
541 <|> P.try (do lchar '{'; n <- name; lchar '}'
542 return (Binding n))
543 <|> do n <- iName []
544 return (Keyword n)
545 <|> do sym <- stringLiteral
546 return (Symbol sym)
547 <?> "syntax symbol"
549{-| Parses a function declaration with possible syntax sugar
552 FunDecl ::= FunDecl';
554-}
555fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
556fnDecl syn = P.try (do notEndBlock
557 d <- fnDecl' syn
558 i <- get
559 let d' = fmap (debindApp syn . desugar syn i) d
560 return [d']) <?> "function declaration"
562{-| Parses a function declaration
565 FunDecl' ::=
566 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
567 | Postulate
568 | Pattern
569 | CAF
570 ;
572-}
573fnDecl' :: SyntaxInfo -> IdrisParser PDecl
574fnDecl' syn = (checkDeclFixity $
575 do (doc, argDocs, fc, opts', n, nfc, acc) <- P.try (do
576 pushIndent
577 (doc, argDocs) <- docstring syn
578 (opts, acc) <- fnOpts
579 (n_in, nfc) <- withExtent fnName
580 let n = expandNS syn n_in
581 fc <- extent $ lchar ':'
582 return (doc, argDocs, fc, opts, n, nfc, acc))
583 ty <- typeExpr (allowImp syn)
584 terminator
585 -- If it's a top level function, note the accessibility
586 -- rules
587 when (syn_toplevel syn) $ addAcc n acc
588 return (PTy doc argDocs syn fc opts' n nfc ty)
589 <|> postulate syn
590 <|> caf syn
591 <|> pattern syn)
592 <?> "function declaration"
594{-| Parses a series of function and accessbility options
597FnOpts ::= FnOpt* Accessibility FnOpt*
599 -}
600fnOpts :: IdrisParser ([FnOpt], Accessibility)
601fnOpts = do
602 opts <- many fnOpt
603 acc <- accessibility
604 opts' <- many fnOpt
605 let allOpts = opts ++ opts'
606 let existingTotality = allOpts `intersect` [TotalFn, CoveringFn, PartialFn]
607 opts'' <- addDefaultTotality (nub existingTotality) allOpts
608 return (opts'', acc)
609 where prettyTot TotalFn = "total"
610 prettyTot PartialFn = "partial"
611 prettyTot CoveringFn = "covering"
612 addDefaultTotality [] opts = do
613 ist <- get
614 case default_total ist of
615 DefaultCheckingTotal -> return (TotalFn:opts)
616 DefaultCheckingCovering -> return (CoveringFn:opts)
617 DefaultCheckingPartial -> return opts -- Don't add partial so that --warn-partial still reports warnings if necessary
618 addDefaultTotality [tot] opts = return opts
619 -- Should really be a semantics error instead of a parser error
620 addDefaultTotality (tot1:tot2:tots) opts =
621 fail ("Conflicting totality modifiers specified " ++ prettyTot tot1 ++ " and " ++ prettyTot tot2)
624{-| Parses a function option
627FnOpt ::= 'total'
628 | 'partial'
629 | 'covering'
630 | 'implicit'
631 | '%' 'no_implicit'
632 | '%' 'assert_total'
633 | '%' 'error_handler'
634 | '%' 'reflection'
635 | '%' 'specialise' '[' NameTimesList? ']'
636 ;
640NameTimes ::= FnName Natural?;
644NameTimesList ::=
645 NameTimes
646 | NameTimes ',' NameTimesList
647 ;
649-}
650fnOpt :: IdrisParser FnOpt
651fnOpt = do keyword "total"; return TotalFn
652 <|> PartialFn <$ keyword "partial"
653 <|> CoveringFn <$ keyword "covering"
654 <|> do P.try (lchar '%' *> reserved "export"); c <- stringLiteral;
655 return $ CExport c
656 <|> NoImplicit <$ P.try (lchar '%' *> reserved "no_implicit")
657 <|> Inlinable <$ P.try (lchar '%' *> reserved "inline")
658 <|> StaticFn <$ P.try (lchar '%' *> reserved "static")
659 <|> ErrorHandler <$ P.try (lchar '%' *> reserved "error_handler")
660 <|> ErrorReverse <$ P.try (lchar '%' *> reserved "error_reverse")
661 <|> ErrorReduce <$ P.try (lchar '%' *> reserved "error_reduce")
662 <|> Reflection <$ P.try (lchar '%' *> reserved "reflection")
663 <|> AutoHint <$ P.try (lchar '%' *> reserved "hint")
664 <|> OverlappingDictionary <$ P.try (lchar '%' *> reserved "overlapping")
665 <|> do lchar '%'; reserved "specialise";
666 lchar '['; ns <- P.sepBy nameTimes (lchar ','); lchar ']';
667 return $ Specialise ns
668 <|> Implicit <$ keyword "implicit"
669 <?> "function modifier"
670 where nameTimes :: IdrisParser (Name, Maybe Int)
671 nameTimes = do n <- fnName
672 t <- P.option Nothing (do reds <- natural
673 return (Just (fromInteger reds)))
674 return (n, t)
676{-| Parses a postulate
679Postulate ::=
680 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
681 ;
683-}
684postulate :: SyntaxInfo -> IdrisParser PDecl
685postulate syn = do (doc, ext)
686 <- P.try $ do (doc, _) <- docstring syn
687 pushIndent
688 ext <- ppostDecl
689 return (doc, ext)
690 ist <- get
691 (opts, acc) <- fnOpts
692 (n_in, nfc) <- withExtent fnName
693 let n = expandNS syn n_in
694 lchar ':'
695 ty <- typeExpr (allowImp syn)
696 fc <- extent $ terminator
697 addAcc n acc
698 return (PPostulate ext doc syn fc nfc opts n ty)
699 <?> "postulate"
700 where ppostDecl = do fc <- keyword "postulate"; return False
701 <|> do lchar '%'; reserved "extern"; return True
703{-| Parses a using declaration
706Using ::=
707 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
708 ;
710 -}
711using_ :: SyntaxInfo -> IdrisParser [PDecl]
712using_ syn =
713 do keyword "using"
714 lchar '('; ns <- usingDeclList syn; lchar ')'
715 openBlock
716 let uvars = using syn
717 ds <- many (decl (syn { using = uvars ++ ns }))
718 closeBlock
719 return (concat ds)
720 <?> "using declaration"
722{-| Parses a parameters declaration
725Params ::=
726 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
727 ;
729-}
730params :: SyntaxInfo -> IdrisParser [PDecl]
731params syn =
732 do (ns, fc) <- withExtent $ do
733 keyword "parameters"
734 lchar '(' *> typeDeclList syn <* lchar ')'
735 let ns' = [(n, ty) | (_, n, _, ty) <- ns]
736 openBlock
737 let pvars = syn_params syn
738 ds <- many (decl syn { syn_params = pvars ++ ns' })
739 closeBlock
740 return [PParams fc ns' (concat ds)]
741 <?> "parameters declaration"
743-- | Parses an open block
744openInterface :: SyntaxInfo -> IdrisParser [PDecl]
745openInterface syn =
746 do (ns, fc) <- withExtent $ do
747 keyword "using"
748 keyword "implementation"
749 P.sepBy1 (withExtent fnName) (lchar ',')
751 openBlock
752 ds <- many (decl syn)
753 closeBlock
754 return [POpenInterfaces fc (map fst ns) (concat ds)]
755 <?> "open interface declaration"
761{-| Parses a mutual declaration (for mutually recursive functions)
764Mutual ::=
765 'mutual' OpenBlock Decl* CloseBlock
766 ;
768-}
769mutual :: SyntaxInfo -> IdrisParser [PDecl]
770mutual syn =
771 do fc <- extent $ keyword "mutual"
772 openBlock
773 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
774 closeBlock
775 return [PMutual fc (concat ds)]
776 <?> "mutual block"
778{-| Parses a namespace declaration
781Namespace ::=
782 'namespace' identifier OpenBlock Decl+ CloseBlock
783 ;
785-}
786namespace :: SyntaxInfo -> IdrisParser [PDecl]
787namespace syn =
788 do keyword "namespace"
789 (n, nfc) <- withExtent identifier
790 openBlock
791 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
792 closeBlock
793 return [PNamespace n nfc (concat ds)]
794 <?> "namespace declaration"
796{-| Parses a methods block (for implementations)
799 ImplementationBlock ::= 'where' OpenBlock FnDecl* CloseBlock
801-}
802implementationBlock :: SyntaxInfo -> IdrisParser [PDecl]
803implementationBlock syn = do keyword "where"
804 openBlock
805 ds <- many (fnDecl syn)
806 closeBlock
807 return (concat ds)
808 <?> "implementation block"
810{-| Parses a methods and implementations block (for interfaces)
813MethodOrImplementation ::=
814 FnDecl
815 | Implementation
816 ;
820InterfaceBlock ::=
821 'where' OpenBlock Constructor? MethodOrImplementation* CloseBlock
822 ;
824-}
825interfaceBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])
826interfaceBlock syn = do keyword "where"
827 openBlock
828 (cn, cd) <- P.option (Nothing, emptyDocstring) $
829 P.try (do (doc, _) <- P.option noDocs docComment
830 n <- constructor
831 return (Just n, doc))
832 ist <- get
833 let cd' = annotate syn ist cd
835 ds <- many (notEndBlock >> P.try (implementation syn)
836 <|> do x <- data_ syn
837 return [x]
838 <|> fnDecl syn)
839 closeBlock
840 return (cn, cd', concat ds)
841 <?> "interface block"
842 where
843 constructor :: IdrisParser (Name, FC)
844 constructor = keyword "constructor" *> withExtent fnName
846 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)
847 annotate syn ist = annotCode $ tryFullExpr syn ist
849{-| Parses an interface declaration
852InterfaceArgument ::=
853 Name
854 | '(' Name ':' Expr ')'
855 ;
859Interface ::=
860 DocComment_t? Accessibility? 'interface' ConstraintList? Name InterfaceArgument* InterfaceBlock?
861 ;
863-}
864interface_ :: SyntaxInfo -> IdrisParser [PDecl]
865interface_ syn = do (doc, argDocs, acc)
866 <- P.try (do (doc, argDocs) <- docstring syn
867 acc <- accessibility
868 interfaceKeyword
869 return (doc, argDocs, acc))
870 ((cons', n, nfc, cs, fds), fc) <- withExtent $ do
871 cons <- constraintList syn
872 let cons' = [(c, ty) | (_, c, _, ty) <- cons]
873 (n_in, nfc) <- withExtent fnName
874 let n = expandNS syn n_in
875 cs <- many carg
876 fds <- P.option [(cn, NoFC) | (cn, _, _) <- cs] fundeps
877 return (cons', n, nfc, cs, fds)
879 (cn, cd, ds) <- P.option (Nothing, fst noDocs, []) (interfaceBlock syn)
880 accData acc n (concatMap declared ds)
881 return [PInterface doc syn fc cons' n nfc cs argDocs fds ds cn cd]
882 <?> "interface declaration"
883 where
884 fundeps :: IdrisParser [(Name, FC)]
885 fundeps = do lchar '|'; P.sepBy (withExtent name) (lchar ',')
887 classWarning :: String
888 classWarning = "Use of a fragile keyword `class`. " ++
889 "`class` is provided for those coming from Haskell. " ++
890 "Please use `interface` instead, which is equivalent."
892 interfaceKeyword :: IdrisParser ()
893 interfaceKeyword = keyword "interface"
894 <|> do fc <- extent $ keyword "class"
895 parserWarning fc Nothing (Msg classWarning)
897 carg :: IdrisParser (Name, FC, PTerm)
898 carg = do lchar '('; (i, ifc) <- withExtent name; lchar ':'; ty <- expr syn; lchar ')'
899 return (i, ifc, ty)
900 <|> do (i, ifc) <- withExtent name
901 return (i, ifc, PType ifc)
903{-| Parses an interface implementation declaration
906 Implementation ::=
907 DocComment_t? 'implementation' ImplementationName? ConstraintList? Name SimpleExpr* ImplementationBlock?
908 ;
912ImplementationName ::= '[' Name ']';
914-}
915implementation :: SyntaxInfo -> IdrisParser [PDecl]
916implementation syn = do (doc, argDocs) <- docstring syn
917 (opts, acc) <- fnOpts
918 optional implementationKeyword
920 ((en, cs, cs', cn, cnfc, args, pnames), fc) <- withExtent $ do
921 en <- optional implementationName
922 cs <- constraintList syn
923 let cs' = [(c, ty) | (_, c, _, ty) <- cs]
924 (cn, cnfc) <- withExtent fnName
925 args <- many (simpleExpr syn)
926 pnames <- implementationUsing
927 return (en, cs, cs', cn, cnfc, args, pnames)
929 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)
930 let t = bindList (\r -> PPi constraint { pcount = r }) cs sc
932 ds <- implementationBlock syn
933 return [PImplementation doc argDocs syn fc cs' pnames acc opts cn cnfc args [] t en ds]
934 <?> "implementation declaration"
935 where implementationName :: IdrisParser Name
936 implementationName = do lchar '['; n_in <- fnName; lchar ']'
937 let n = expandNS syn n_in
938 return n
939 <?> "implementation name"
941 instanceWarning :: String
942 instanceWarning = "Use of fragile keyword `instance`. " ++
943 "`instance` is provided for those coming from Haskell. " ++
944 "Please use `implementation` (which is equivalent) instead, or omit it."
946 implementationKeyword :: IdrisParser ()
947 implementationKeyword = keyword "implementation"
948 <|> do fc <- extent $ keyword "instance"
949 parserWarning fc Nothing (Msg instanceWarning)
951 implementationUsing :: IdrisParser [Name]
952 implementationUsing = do keyword "using"
953 ns <- P.sepBy1 (withExtent fnName) (lchar ',')
954 return (map fst ns)
955 <|> return []
957-- | Parse a docstring
958docstring :: SyntaxInfo
959 -> IdrisParser (Docstring (Either Err PTerm),
960 [(Name,Docstring (Either Err PTerm))])
961docstring syn = do (doc, argDocs) <- P.option noDocs docComment
962 ist <- get
963 let doc' = annotCode (tryFullExpr syn ist) doc
964 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
965 | (n, d) <- argDocs ]
966 return (doc', argDocs')
969{-| Parses a using declaration list
972UsingDeclList ::=
973 UsingDeclList'
974 | NameList TypeSig
975 ;
979UsingDeclList' ::=
980 UsingDecl
981 | UsingDecl ',' UsingDeclList'
982 ;
986NameList ::=
987 Name
988 | Name ',' NameList
989 ;
991-}
992usingDeclList :: SyntaxInfo -> IdrisParser [Using]
993usingDeclList syn
994 = P.try (P.sepBy1 (usingDecl syn) (lchar ','))
995 <|> do ns <- P.sepBy1 name (lchar ',')
996 lchar ':'
997 t <- typeExpr (disallowImp syn)
998 return (map (\x -> UImplicit x t) ns)
999 <?> "using declaration list"
1001{-| Parses a using declaration
1004UsingDecl ::=
1005 FnName TypeSig
1006 | FnName FnName+
1010usingDecl :: SyntaxInfo -> IdrisParser Using
1011usingDecl syn = P.try (do x <- fnName
1012 lchar ':'
1013 t <- typeExpr (disallowImp syn)
1014 return (UImplicit x t))
1015 <|> do c <- fnName
1016 xs <- many fnName
1017 return (UConstraint c xs)
1018 <?> "using declaration"
1020{-| Parse a clause with patterns
1023Pattern ::= Clause;
1026pattern :: SyntaxInfo -> IdrisParser PDecl
1027pattern syn = do (clause, fc) <- withExtent (clause syn)
1028 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
1029 <?> "pattern"
1031{-| Parse a constant applicative form declaration
1034CAF ::= 'let' FnName '=' Expr Terminator;
1037caf :: SyntaxInfo -> IdrisParser PDecl
1038caf syn = do keyword "let"
1039 (n, fc) <- withExtent (expandNS syn <$> fnName)
1040 pushIndent
1041 lchar '='
1042 t <- indented $ expr syn
1043 terminator
1044 return (PCAF fc n t)
1045 <?> "constant applicative form declaration"
1047{-| Parse an argument expression
1050ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
1053argExpr :: SyntaxInfo -> IdrisParser PTerm
1054argExpr syn = let syn' = syn { inPattern = True } in
1055 P.try (hsimpleExpr syn') <|> simpleExternalExpr syn'
1056 <?> "argument expression"
1058{-| Parse a right hand side of a function
1061RHS ::= '=' Expr
1062 | '?=' RHSName? Expr
1063 | Impossible
1068RHSName ::= '{' FnName '}';
1071rhs :: SyntaxInfo -> Name -> IdrisParser (PTerm, FC)
1072rhs syn n = do lchar '='
1073 indentGt
1074 withExtent $ expr syn
1075 <|> do symbol "?=";
1076 (name, fc) <- withExtent $ P.option n' (symbol "{" *> fnName <* symbol "}")
1077 r <- expr syn
1078 return (addLet fc name r, fc)
1079 <|> withExtent impossible
1080 <?> "function right hand side"
1081 where mkN :: Name -> Name
1082 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
1083 then sUN "infix_op_lemma_1"
1084 else sUN (str x++"_lemma_1")
1085 mkN (NS x n) = NS (mkN x) n
1086 n' :: Name
1087 n' = mkN n
1088 addLet :: FC -> Name -> PTerm -> PTerm
1089 addLet fc nm (PLet fc' rig n nfc ty val r) = PLet fc' rig n nfc ty val (addLet fc nm r)
1090 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
1091 where addLetC (l, r) = (l, addLet fc nm r)
1092 addLet fc nm r = (PLet fc RigW (sUN "value") NoFC Placeholder r (PMetavar NoFC nm))
1094{-|Parses a function clause
1097RHSOrWithBlock ::= RHS WhereOrTerminator
1098 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
1103Clause ::= WExpr+ RHSOrWithBlock
1104 | SimpleExpr '<==' FnName RHS WhereOrTerminator
1105 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
1106 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
1111ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
1115WhereOrTerminator ::= WhereBlock | Terminator;
1118clause :: SyntaxInfo -> IdrisParser PClause
1119clause syn
1120 -- unnamed with or function clause (inside a with)
1121 = do wargs <- P.try (do pushIndent; some (wExpr syn))
1122 ist <- get
1123 n <- case lastParse ist of
1124 Just t -> return t
1125 Nothing -> fail "Invalid clause"
1126 (do (r, fc) <- rhs syn n
1127 let wsyn = syn { syn_namespace = [], syn_toplevel = False }
1128 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1129 <|> ([], []) <$ terminator
1130 return $ PClauseR fc wargs r wheres) <|> (do
1131 popIndent
1132 ((wval, pn), fc) <- withExtent $ do
1133 keyword "with"
1134 wval <- bracketed syn
1135 pn <- optProof
1136 return (wval, pn)
1137 openBlock
1138 ds <- some $ fnDecl syn
1139 let withs = concat ds
1140 closeBlock
1141 return $ PWithR fc wargs wval pn withs)
1142 -- <==
1143 <|> do ty <- P.try (do pushIndent
1144 ty <- simpleExpr syn
1145 symbol "<=="
1146 return ty)
1147 (n, fc) <- withExtent (expandNS syn <$> fnName)
1148 (r, _) <- rhs syn n
1149 let wsyn = syn { syn_namespace = [] }
1150 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1151 <|> ([], []) <$ terminator
1152 let capp = PLet fc RigW (sMN 0 "match") NoFC
1153 ty
1154 (PMatchApp fc n)
1155 (PRef fc [] (sMN 0 "match"))
1156 ist <- get
1157 put (ist { lastParse = Just n })
1158 return $ PClause fc n capp [] r wheres
1159 -- lhs application "with" clause or function clause
1160 <|> do pushIndent
1161 (n, nfc, capp, wargs) <- lhs
1162 modify $ \ist -> ist { lastParse = Just n }
1163 (do (rs, fc) <- rhs syn n
1164 let wsyn = syn { syn_namespace = [] }
1165 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1166 <|> ([], []) <$ terminator
1167 return $ PClause fc n capp wargs rs wheres) <|> (do
1168 popIndent
1169 ((wval, pn), fc) <- withExtent $ do
1170 keyword "with"
1171 wval <- bracketed syn
1172 pn <- optProof
1173 return (wval, pn)
1174 openBlock
1175 ds <- some $ fnDecl syn
1176 closeBlock
1177 let withs = map (fillLHSD n capp wargs) $ concat ds
1178 return $ PWith fc n capp wargs wval pn withs)
1179 <?> "function clause"
1180 where
1181 lhsInfixApp :: IdrisParser (Name, FC, [PArg], [PTerm])
1182 lhsInfixApp = do l <- argExpr syn
1183 (op, nfc) <- withExtent symbolicOperator
1184 when (op == "=" || op == "?=" ) $
1185 fail "infix clause definition with \"=\" and \"?=\" not supported "
1186 let n = expandNS syn (sUN op)
1187 r <- argExpr syn
1188 wargs <- many (wExpr syn)
1189 return (n, nfc, [pexp l, pexp r], wargs)
1191 lhsPrefixApp :: IdrisParser (Name, FC, [PArg], [PTerm])
1192 lhsPrefixApp = do (n, nfc) <- withExtent (expandNS syn <$> fnName)
1193 args <- many (P.try (implicitArg (syn { inPattern = True } ))
1194 <|> P.try (constraintArg (syn { inPattern = True }))
1195 <|> (fmap pexp (argExpr syn)))
1196 wargs <- many (wExpr syn)
1197 return (n, nfc, args, wargs)
1199 lhs :: IdrisParser (Name, FC, PTerm, [PTerm])
1200 lhs = do ((n, nfc, args, wargs), lhs_fc) <- withExtent (P.try lhsInfixApp <|> lhsPrefixApp)
1201 let capp = PApp lhs_fc (PRef nfc [nfc] n) args
1202 return (n, nfc, capp, wargs)
1204 optProof = P.option Nothing (do keyword "proof"
1205 n <- withExtent fnName
1206 return (Just n))
1208 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
1209 fillLHS n capp owargs (PClauseR fc wargs v ws)
1210 = PClause fc n capp (owargs ++ wargs) v ws
1211 fillLHS n capp owargs (PWithR fc wargs v pn ws)
1212 = PWith fc n capp (owargs ++ wargs) v pn
1213 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1214 fillLHS _ _ _ c = c
1216 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
1217 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1218 fillLHSD n c a x = x
1220{-| Parses with pattern
1223WExpr ::= '|' Expr';
1226wExpr :: SyntaxInfo -> IdrisParser PTerm
1227wExpr syn = do lchar '|'
1228 expr' (syn { inPattern = True })
1229 <?> "with pattern"
1231{-| Parses a where block
1234WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
1237whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
1238whereBlock n syn
1239 = do keyword "where"
1240 ds <- indentedBlock1 (decl syn)
1241 let dns = concatMap (concatMap declared) ds
1242 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1243 <?> "where block"
1245{-|Parses a code generation target language name
1248Codegen ::= 'C'
1249 | 'Java'
1250 | 'JavaScript'
1251 | 'Node'
1252 | 'LLVM'
1253 | 'Bytecode'
1257codegen_ :: IdrisParser Codegen
1258codegen_ = do n <- identifier
1259 return (Via IBCFormat (map toLower n))
1260 <|> do reserved "Bytecode"; return Bytecode
1261 <?> "code generation language"
1263{-|Parses a compiler directive
1265StringList ::=
1266 String
1267 | String ',' StringList
1272Directive ::= '%' Directive';
1276Directive' ::= 'lib' CodeGen String_t
1277 | 'link' CodeGen String_t
1278 | 'flag' CodeGen String_t
1279 | 'include' CodeGen String_t
1280 | 'hide' Name
1281 | 'freeze' Name
1282 | 'thaw' Name
1283 | 'access' Accessibility
1284 | 'default' Totality
1285 | 'logging' Natural
1286 | 'dynamic' StringList
1287 | 'name' Name NameList
1288 | 'error_handlers' Name NameList
1289 | 'language' 'TypeProviders'
1290 | 'language' 'ErrorReflection'
1291 | 'deprecated' Name String
1292 | 'fragile' Name Reason
1296directive :: SyntaxInfo -> IdrisParser [PDecl]
1297directive syn = do P.try (lchar '%' *> reserved "lib")
1298 cgn <- codegen_
1299 lib <- stringLiteral
1300 return [PDirective (DLib cgn lib)]
1301 <|> do P.try (lchar '%' *> reserved "link")
1302 cgn <- codegen_; obj <- stringLiteral
1303 return [PDirective (DLink cgn obj)]
1304 <|> do P.try (lchar '%' *> reserved "flag")
1305 cgn <- codegen_; flag <- stringLiteral
1306 return [PDirective (DFlag cgn flag)]
1307 <|> do P.try (lchar '%' *> reserved "include")
1308 cgn <- codegen_
1309 hdr <- stringLiteral
1310 return [PDirective (DInclude cgn hdr)]
1311 <|> do P.try (lchar '%' *> reserved "hide"); n <- fnName
1312 return [PDirective (DHide n)]
1313 <|> do P.try (lchar '%' *> reserved "freeze"); n <- iName []
1314 return [PDirective (DFreeze n)]
1315 <|> do P.try (lchar '%' *> reserved "thaw"); n <- iName []
1316 return [PDirective (DThaw n)]
1317 -- injectivity assertins are intended for debugging purposes
1318 -- only, and won't be documented/could be removed at any point
1319 <|> do P.try (lchar '%' *> reserved "assert_injective"); n <- fnName
1320 return [PDirective (DInjective n)]
1321 -- Assert totality of something after definition. This is
1322 -- here as a debugging aid, so commented out...
1323-- <|> do P.try (lchar '%' *> reserved "assert_set_total"); n <- fst <$> fnName
1324-- return [PDirective (DSetTotal n)]
1325 <|> do P.try (lchar '%' *> reserved "access")
1326 acc <- accessibility
1327 ist <- get
1328 put ist { default_access = acc }
1329 return [PDirective (DAccess acc)]
1330 <|> do P.try (lchar '%' *> reserved "default"); tot <- totality
1331 i <- get
1332 put (i { default_total = tot } )
1333 return [PDirective (DDefault tot)]
1334 <|> do P.try (lchar '%' *> reserved "logging")
1335 i <- natural
1336 return [PDirective (DLogging i)]
1337 <|> do P.try (lchar '%' *> reserved "dynamic")
1338 libs <- P.sepBy1 stringLiteral (lchar ',')
1339 return [PDirective (DDynamicLibs libs)]
1340 <|> do P.try (lchar '%' *> reserved "name")
1341 (ty, tyFC) <- withExtent fnName
1342 ns <- P.sepBy1 (withExtent name) (lchar ',')
1343 return [PDirective (DNameHint ty tyFC ns)]
1344 <|> do P.try (lchar '%' *> reserved "error_handlers")
1345 (fn, nfc) <- withExtent fnName
1346 (arg, afc) <- withExtent fnName
1347 ns <- P.sepBy1 (withExtent name) (lchar ',')
1348 return [PDirective (DErrorHandlers fn nfc arg afc ns) ]
1349 <|> do P.try (lchar '%' *> reserved "language"); ext <- pLangExt;
1350 return [PDirective (DLanguage ext)]
1351 <|> do P.try (lchar '%' *> reserved "deprecate")
1352 n <- fnName
1353 alt <- P.option "" stringLiteral
1354 return [PDirective (DDeprecate n alt)]
1355 <|> do P.try (lchar '%' *> reserved "fragile")
1356 n <- fnName
1357 alt <- P.option "" stringLiteral
1358 return [PDirective (DFragile n alt)]
1359 <|> do fc <- extent $ P.try (lchar '%' *> reserved "used")
1360 fn <- fnName
1361 arg <- iName []
1362 return [PDirective (DUsed fc fn arg)]
1363 <|> do P.try (lchar '%' *> reserved "auto_implicits")
1364 b <- on_off
1365 return [PDirective (DAutoImplicits b)]
1366 <?> "directive"
1367 where on_off = do reserved "on"; return True
1368 <|> do reserved "off"; return False
1370pLangExt :: IdrisParser LanguageExt
1371pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1372 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1373 <|> (reserved "UniquenessTypes" >> return UniquenessTypes)
1374 <|> (reserved "LinearTypes" >> return LinearTypes)
1375 <|> (reserved "DSLNotation" >> return DSLNotation)
1376 <|> (reserved "ElabReflection" >> return ElabReflection)
1377 <|> (reserved "FirstClassReflection" >> return FCReflection)
1379{-| Parses a totality
1382Totality ::= 'partial' | 'total' | 'covering'
1386totality :: IdrisParser DefaultTotality
1387totality
1388 = do keyword "total"; return DefaultCheckingTotal
1389 <|> do keyword "partial"; return DefaultCheckingPartial
1390 <|> do keyword "covering"; return DefaultCheckingCovering
1392{-| Parses a type provider
1395Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1396ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1398 -}
1399provider :: SyntaxInfo -> IdrisParser [PDecl]
1400provider syn = do doc <- P.try (do (doc, _) <- docstring syn
1401 highlight AnnKeyword $ lchar '%' *> reserved "provide"
1402 return doc)
1403 provideTerm doc <|> providePostulate doc
1404 <?> "type provider"
1405 where provideTerm doc =
1406 do lchar '('; (n, nfc) <- withExtent fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1407 keyword "with"
1408 (e, fc) <- withExtent (expr syn) <?> "provider expression"
1409 return [PProvider doc syn fc nfc (ProvTerm t e) n]
1410 providePostulate doc =
1411 do keyword "postulate"
1412 (n, nfc) <- withExtent fnName
1413 keyword "with"
1414 (e, fc) <- withExtent (expr syn) <?> "provider expression"
1415 return [PProvider doc syn fc nfc (ProvPostulate e) n]
1417{-| Parses a transform
1420Transform ::= '%' 'transform' Expr '==>' Expr
1423transform :: SyntaxInfo -> IdrisParser [PDecl]
1424transform syn = do P.try (lchar '%' *> reserved "transform")
1425 -- leave it unchecked, until we work out what this should
1426 -- actually mean...
1427-- safety <- option True (do reserved "unsafe"
1428-- return False)
1429 l <- expr syn
1430 fc <- extent $ symbol "==>"
1431 r <- expr syn
1432 return [PTransform fc False l r]
1433 <?> "transform"
1435{-| Parses a top-level reflected elaborator script
1438RunElabDecl ::= '%' 'runElab' Expr
1441runElabDecl :: SyntaxInfo -> IdrisParser PDecl
1442runElabDecl syn =
1443 do kwFC <- P.try (highlight AnnKeyword (extent $ lchar '%' *> reserved "runElab"))
1444 script <- expr syn <?> "elaborator script"
1445 return $ PRunElabDecl kwFC script (syn_namespace syn)
1446 <?> "top-level elaborator script"
1448{- * Loading and parsing -}
1449{-| Parses an expression from input -}
1450parseExpr :: IState -> String -> Either ParseError PTerm
1451parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1453{-| Parses a constant form input -}
1454parseConst :: IState -> String -> Either ParseError Const
1455parseConst st = runparser constant st "(input)"
1457{-| Parses a tactic from input -}
1458parseTactic :: IState -> String -> Either ParseError PTactic
1459parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1461{-| Parses a do-step from input (used in the elab shell) -}
1462parseElabShellStep :: IState -> String -> Either ParseError (Either ElabShellCmd PDo)
1463parseElabShellStep ist = runparser (Right <$> do_ defaultSyntax <|> Left <$> elabShellCmd) ist "(input)"
1464 where elabShellCmd = char ':' >>
1465 (reserved "qed" >> pure EQED ) <|>
1466 (reserved "abandon" >> pure EAbandon ) <|>
1467 (reserved "undo" >> pure EUndo ) <|>
1468 (reserved "state" >> pure EProofState) <|>
1469 (reserved "term" >> pure EProofTerm ) <|>
1470 (expressionTactic ["e", "eval"] EEval ) <|>
1471 (expressionTactic ["t", "type"] ECheck) <|>
1472 (expressionTactic ["search"] ESearch ) <|>
1473 (do reserved "doc"
1474 doc <- (Right <$> constant) <|> (Left <$> fnName)
1475 P.eof
1476 return (EDocStr doc))
1477 <?> "elab command"
1478 expressionTactic cmds tactic =
1479 do asum (map reserved cmds)
1480 t <- spaced (expr defaultSyntax)
1481 i <- get
1482 return $ tactic (desugar defaultSyntax i t)
1483 spaced parser = indentGt *> parser
1485-- | Parse module header and imports
1486parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark)
1487parseImports fname input
1488 = do i <- getIState
1489 case runparser imports i fname input of
1490 Left err -> formatMessage err >>= ifail . show
1491 Right (x, annots, i) ->
1492 do putIState i
1493 fname' <- runIO $ Dir.makeAbsolute fname
1494 sendHighlighting $ addPath annots fname'
1495 return x
1496 where imports :: IdrisParser ((Maybe (Docstring ()), [String],
1497 [ImportInfo],
1498 Maybe Mark),
1499 [(FC, OutputAnnotation)], IState)
1500 imports = do optional shebang
1501 whiteSpace
1502 (mdoc, mname, annots) <- moduleHeader
1503 ps_exp <- many import_
1504 mrk <- mark
1505 isEof <- lookAheadMatches P.eof
1506 let mrk' = if isEof
1507 then Nothing
1508 else Just mrk
1509 i <- get
1510 -- add Builtins and Prelude, unless options say
1511 -- not to
1512 let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp
1513 return ((mdoc, mname, ps, mrk'), annots, i)
1515 addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]
1516 addPath [] _ = []
1517 addPath ((fc, AnnNamespace ns Nothing) : annots) path =
1518 (fc, AnnNamespace ns (Just path)) : addPath annots path
1519 addPath (annot:annots) path = annot : addPath annots path
1521 shebang :: IdrisParser ()
1522 shebang = string "#!" *> many (P.satisfy $ not . isEol) *> eol *> pure ()
1524-- | Check if the coloring matches the options and corrects if necessary
1525fixColour :: Bool -> PP.Doc -> PP.Doc
1526fixColour False doc = PP.plain doc
1527fixColour True doc = doc
1529-- | A program is a list of declarations, possibly with associated
1530-- documentation strings.
1531parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Mark -> Idris [PDecl]
1532parseProg syn fname input mrk
1533 = do i <- getIState
1534 case runparser mainProg i fname input of
1535 Left err -> do emitWarning err
1536 i <- getIState
1537 putIState (i { errSpan = Just (messageExtent err) })
1538 return []
1539 Right (x, i) -> do putIState i
1540 reportParserWarnings
1541 return $ collect x
1542 where mainProg :: IdrisParser ([PDecl], IState)
1543 mainProg = case mrk of
1544 Nothing -> do i <- get; return ([], i)
1545 Just mrk -> do
1546 restore mrk
1547 ds <- prog syn
1548 i' <- get
1549 return (ds, i')
1551-- | Collect 'PClauses' with the same function name
1552collect :: [PDecl] -> [PDecl]
1553collect (c@(PClauses _ o _ _) : ds)
1554 = clauses (cname c) [] (c : ds)
1555 where clauses :: Maybe Name -> [PClause] -> [PDecl] -> [PDecl]
1556 clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)
1557 | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds
1558 clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r pn w] : ds)
1559 | n == n' = clauses j (PWith fc' n' l ws r pn (collect w) : acc) ds
1560 clauses (Just n) acc xs = PClauses (fcOf c) o n (reverse acc) : collect xs
1561 clauses Nothing acc (x:xs) = collect xs
1562 clauses Nothing acc [] = []
1564 cname :: PDecl -> Maybe Name
1565 cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n
1566 cname (PClauses fc _ _ [PWith _ n _ _ _ _ _]) = Just n
1567 cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing
1568 cname (PClauses fc _ _ [PWithR _ _ _ _ _]) = Nothing
1569 fcOf :: PDecl -> FC
1570 fcOf (PClauses fc _ _ _) = fc
1571collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
1572collect (POpenInterfaces f ns ps : ds) = POpenInterfaces f ns (collect ps) : collect ds
1573collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds
1574collect (PNamespace ns fc ps : ds) = PNamespace ns fc (collect ps) : collect ds
1575collect (PInterface doc f s cs n nfc ps pdocs fds ds cn cd : ds')
1576 = PInterface doc f s cs n nfc ps pdocs fds (collect ds) cn cd : collect ds'
1577collect (PImplementation doc argDocs f s cs pnames acc opts n nfc ps pextra t en ds : ds')
1578 = PImplementation doc argDocs f s cs pnames acc opts n nfc ps pextra t en (collect ds) : collect ds'
1579collect (d : ds) = d : collect ds
1580collect [] = []
1582{-| Load idris module and show error if something wrong happens -}
1583loadModule :: FilePath -> IBCPhase -> Idris (Maybe String)
1584loadModule f phase
1585 = idrisCatch (loadModule' f phase)
1586 (\e -> do setErrSpan (getErrSpan e)
1587 ist <- getIState
1588 iWarn (getErrSpan e) $ pprintErr ist e
1589 return Nothing)
1591{-| Load idris module -}
1592loadModule' :: FilePath -> IBCPhase -> Idris (Maybe String)
1593loadModule' f phase
1594 = do i <- getIState
1595 let file = takeWhile (/= ' ') f
1596 ibcsd <- valIBCSubDir i
1597 ids <- rankedImportDirs file
1598 fp <- findImport ids ibcsd file
1599 if file `elem` imported i
1600 then do logParser 1 $ "Already read " ++ file
1601 return Nothing
1602 else do putIState (i { imported = file : imported i })
1603 case fp of
1604 IDR fn -> loadSource False fn Nothing
1605 LIDR fn -> loadSource True fn Nothing
1606 IBC fn src ->
1607 idrisCatch (loadIBC True phase fn)
1608 (\c -> do logParser 1 $ fn ++ " failed " ++ pshow i c
1609 case src of
1610 IDR sfn -> loadSource False sfn Nothing
1611 LIDR sfn -> loadSource True sfn Nothing)
1612 return $ Just file
1614{-| Load idris code from file -}
1615loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()
1616loadFromIFile reexp phase i@(IBC fn src) maxline
1617 = do logParser 1 $ "Skipping " ++ getSrcFile i
1618 logParser 3 $ "loadFromIFile i" ++ show i
1619 idrisCatch (loadIBC reexp phase fn)
1620 (\err -> ierror $ LoadingFailed fn err)
1621 where
1622 getSrcFile (IDR fn) = fn
1623 getSrcFile (LIDR fn) = fn
1624 getSrcFile (IBC f src) = getSrcFile src
1626loadFromIFile _ _ (IDR fn) maxline = loadSource' False fn maxline
1627loadFromIFile _ _ (LIDR fn) maxline = loadSource' True fn maxline
1629{-| Load idris source code and show error if something wrong happens -}
1630loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1631loadSource' lidr r maxline
1632 = idrisCatch (loadSource lidr r maxline)
1633 (\e -> do setErrSpan (getErrSpan e)
1634 ist <- getIState
1635 case e of
1636 At f e' -> iWarn f (pprintErr ist e')
1637 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1639{-| Load Idris source code-}
1640loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1641loadSource lidr f toline
1642 = do logParser 1 ("Reading " ++ f)
1643 iReport 2 ("Reading " ++ f)
1644 i <- getIState
1645 let def_total = default_total i
1646 file_in <- runIO $ readSource f
1647 file <- if lidr then tclift $ unlit f file_in else return file_in
1648 (mdocs, mname, imports_in, pos) <- parseImports f file
1649 ai <- getAutoImports
1650 let imports = map (\n -> ImportInfo True n Nothing [] NoFC NoFC) ai ++ imports_in
1651 ids <- rankedImportDirs f
1652 ibcsd <- valIBCSubDir i
1653 mapM_ (\(re, f, ns, nfc) ->
1654 do fp <- findImport ids ibcsd f
1655 case fp of
1656 LIDR fn -> ifail $ "No ibc for " ++ f
1657 IDR fn -> ifail $ "No ibc for " ++ f
1658 IBC fn src ->
1659 do loadIBC True IBC_Building fn
1660 let srcFn = case src of
1661 IDR fn -> Just fn
1662 LIDR fn -> Just fn
1663 _ -> Nothing
1664 srcFnAbs <- case srcFn of
1665 Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)
1666 Nothing -> return Nothing
1667 sendHighlighting [(nfc, AnnNamespace ns srcFnAbs)])
1668 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]
1669 reportParserWarnings
1670 sendParserHighlighting
1672 -- process and check module aliases
1673 let modAliases = M.fromList
1674 [ (prep alias, prep realName)
1675 | ImportInfo { import_reexport = reexport
1676 , import_path = realName
1677 , import_rename = Just (alias, _)
1678 , import_location = fc } <- imports
1680 prep = map T.pack . reverse . Spl.splitOn [pathSeparator]
1681 aliasNames = [ (alias, fc)
1682 | ImportInfo { import_rename = Just (alias, fc)
1683 } <- imports
1685 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1686 case map head . filter ((/= 1) . length) $ histogram of
1687 [] -> logParser 3 $ "Module aliases: " ++ show (M.toList modAliases)
1688 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1690 i <- getIState
1691 putIState (i { default_access = Private, module_aliases = modAliases })
1692 clearIBC -- start a new .ibc file
1693 -- record package info in .ibc
1694 imps <- allImportDirs
1695 mapM_ addIBC (map IBCImportDir imps)
1696 mapM_ (addIBC . IBCImport)
1697 [ (reexport, realName)
1698 | ImportInfo { import_reexport = reexport
1699 , import_path = realName
1700 } <- imports
1702 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1703 maxline = toline }
1704 ist <- getIState
1705 -- Save the span from parsing the module header, because
1706 -- an empty program parse might obliterate it.
1707 let oldSpan = idris_parsedSpan ist
1708 ds' <- parseProg syntax f file pos
1710 case (ds', oldSpan) of
1711 ([], Just fc) ->
1712 -- If no program elements were parsed, we dind't
1713 -- get a loaded region in the IBC file. That
1714 -- means we need to add it back.
1715 do ist <- getIState
1716 putIState ist { idris_parsedSpan = oldSpan
1717 , ibc_write = IBCParsedRegion fc :
1718 ibc_write ist
1720 _ -> return ()
1721 sendParserHighlighting
1723 -- Parsing done, now process declarations
1725 let ds = namespaces mname ds'
1726 logParser 3 (show $ showDecls verbosePPOption ds)
1727 i <- getIState
1728 logLvl 10 (show (toAlist (idris_implicits i)))
1729 logLvl 3 (show (idris_infixes i))
1730 -- Now add all the declarations to the context
1731 iReport 1 $ "Type checking " ++ f
1732 -- we totality check after every Mutual block, so if
1733 -- anything is a single definition, wrap it in a
1734 -- mutual block on its own
1735 elabDecls (toplevelWith f) (map toMutual ds)
1736 i <- getIState
1737 -- simplify every definition do give the totality checker
1738 -- a better chance
1739 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1740 ctxt' <-
1741 do ctxt <- getContext
1742 tclift $ simplifyCasedef n [] [] (getErasureInfo i) ctxt
1743 setContext ctxt')
1744 (map snd (idris_totcheck i))
1745 -- build size change graph from simplified definitions
1746 iReport 3 $ "Totality checking " ++ f
1747 logLvl 1 $ "Totality checking " ++ f
1748 i <- getIState
1749 mapM_ buildSCG (idris_totcheck i)
1750 mapM_ checkDeclTotality (idris_totcheck i)
1751 mapM_ verifyTotality (idris_totcheck i)
1753 -- Redo totality check for deferred names
1754 let deftots = idris_defertotcheck i
1755 logLvl 2 $ "Totality checking " ++ show deftots
1756 mapM_ (\x -> do tot <- getTotality x
1757 case tot of
1758 Total _ ->
1759 do let opts = case lookupCtxtExact x (idris_flags i) of
1760 Just os -> os
1761 Nothing -> []
1762 when (AssertTotal `notElem` opts) $
1763 setTotality x Unchecked
1764 _ -> return ()) (map snd deftots)
1765 mapM_ buildSCG deftots
1766 mapM_ checkDeclTotality deftots
1768 logLvl 1 ("Finished " ++ f)
1769 ibcsd <- valIBCSubDir i
1770 logLvl 1 $ "Universe checking " ++ f
1771 iReport 3 $ "Universe checking " ++ f
1772 iucheck
1773 let ibc = ibcPathNoFallback ibcsd f
1774 i <- getIState
1775 addHides (hide_list i)
1777 -- Save module documentation if applicable
1778 i <- getIState
1779 case mdocs of
1780 Nothing -> return ()
1781 Just docs -> addModDoc syntax mname docs
1784 -- Finally, write an ibc and highlights if checking was successful
1785 ok <- noErrors
1786 when ok $
1787 do idrisCatch (do writeIBC f ibc; clearIBC)
1788 (\c -> return ()) -- failure is harmless
1789 hl <- getDumpHighlighting
1790 when hl $
1791 idrisCatch (writeHighlights f)
1792 (const $ return ()) -- failure is harmless
1793 clearHighlights
1794 i <- getIState
1795 putIState (i { default_total = def_total,
1796 hide_list = emptyContext })
1797 return ()
1798 where
1799 namespaces :: [String] -> [PDecl] -> [PDecl]
1800 namespaces [] ds = ds
1801 namespaces (x:xs) ds = [PNamespace x NoFC (namespaces xs ds)]
1803 toMutual :: PDecl -> PDecl
1804 toMutual m@(PMutual _ d) = m
1805 toMutual (PNamespace x fc ds) = PNamespace x fc (map toMutual ds)
1806 toMutual (POpenInterfaces f ns ds) = POpenInterfaces f ns (map toMutual ds)
1807 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1808 case x of
1809 PClauses{} -> r
1810 PInterface{} -> r
1811 PData{} -> r
1812 PImplementation{} -> r
1813 _ -> x
1815 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1816 addModDoc syn mname docs =
1817 do ist <- getIState
1818 docs' <- elabDocTerms (toplevelWith f) (parsedDocs ist)
1819 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1820 putIState ist { idris_moduledocs = modDocs' }
1821 addIBC (IBCModDocs docName)
1822 where
1823 docName = NS modDocName (map T.pack (reverse mname))
1824 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1826{-| Adds names to hide list -}
1827addHides :: Ctxt Accessibility -> Idris ()
1828addHides xs = mapM_ doHide (toAlist xs)
1829 where doHide (n, a) = do setAccessibility n a
1830 addIBC (IBCAccess n a)