git.iko.soy/Idris-dev
on ff01a4c help sign in
Idris-dev/src/Idris/Parser.hs
1884 lines 73 kB history raw
1{-|
2Module : Idris.Parser
3Description : Idris' parser.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving, PatternGuards #-}
9{-# OPTIONS_GHC -O0 #-}
10module Idris.Parser(module Idris.Parser,
11 module Idris.Parser.Expr,
12 module Idris.Parser.Data,
13 module Idris.Parser.Helpers,
14 module Idris.Parser.Ops) where
16import Idris.AbsSyntax hiding (namespace, params)
17import Idris.Core.Evaluate
18import Idris.Core.TT
19import Idris.Coverage
20import Idris.Delaborate
21import Idris.Docstrings hiding (Unchecked)
22import Idris.DSL
23import Idris.Elab.Term
24import Idris.Elab.Value
25import Idris.ElabDecls
26import Idris.Error
27import Idris.IBC
28import Idris.Imports
29import Idris.Output
30import Idris.Parser.Data
31import Idris.Parser.Expr
32import Idris.Parser.Helpers
33import Idris.Parser.Ops
34import Idris.Providers
35import Idris.Unlit
37import Util.DynamicLinker
38import qualified Util.Pretty as P
39import Util.System (readSource, writeSource)
41import Paths_idris
43import Prelude hiding (pi)
45import Control.Applicative hiding (Const)
46import Control.Monad
47import Control.Monad.State.Strict
48import qualified Data.ByteString.UTF8 as UTF8
49import Data.Char
50import Data.Foldable (asum)
51import Data.Function
52import Data.Generics.Uniplate.Data (descendM)
53import qualified Data.HashSet as HS
54import Data.List
55import qualified Data.List.Split as Spl
56import qualified Data.Map as M
57import Data.Maybe
58import Data.Monoid
59import Data.Ord
60import qualified Data.Set as S
61import qualified Data.Text as T
62import Debug.Trace
63import qualified System.Directory as Dir (makeAbsolute)
64import System.FilePath
65import System.IO
66import qualified Text.Parser.Char as Chr
67import Text.Parser.Expression
68import Text.Parser.LookAhead
69import qualified Text.Parser.Token as Tok
70import qualified Text.Parser.Token.Highlight as Hi
71import Text.PrettyPrint.ANSI.Leijen (Doc, plain)
72import qualified Text.PrettyPrint.ANSI.Leijen as ANSI
73import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,
74 stringLiteral, symbol, whiteSpace)
75import Text.Trifecta.Delta
77{-
79 grammar shortcut notation:
80 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)
81 RULE? = optional rule (i.e. RULE or nothing)
82 RULE* = repeated rule (i.e. RULE zero or more times)
83 RULE+ = repeated rule with at least one match (i.e. RULE one or more times)
84 RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)
85 RULE{n} = rule repeated n times
87-}
89{- * Main grammar -}
91{-| Parses module definition
94 ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;
96-}
97moduleHeader :: IdrisParser (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
98moduleHeader = try (do docs <- optional docComment
99 noArgs docs
100 reservedHL "module"
101 (i, ifc) <- identifier
102 option ';' (lchar ';')
103 let modName = moduleName i
104 return (fmap fst docs,
105 modName,
106 [(ifc, AnnNamespace (map T.pack modName) Nothing)]))
107 <|> try (do lchar '%'; reserved "unqualified"
108 return (Nothing, [], []))
109 <|> return (Nothing, moduleName "Main", [])
110 where moduleName x = case span (/='.') x of
111 (x, "") -> [x]
112 (x, '.':y) -> x : moduleName y
113 noArgs (Just (_, args)) | not (null args) = fail "Modules do not take arguments"
114 noArgs _ = return ()
116data ImportInfo = ImportInfo { import_reexport :: Bool
117 , import_path :: FilePath
118 , import_rename :: Maybe (String, FC)
119 , import_namespace :: [T.Text]
120 , import_location :: FC
121 , import_modname_location :: FC
122 }
124{-| Parses an import statement
127 Import ::= 'import' Identifier_t ';'?;
129 -}
130import_ :: IdrisParser ImportInfo
131import_ = do fc <- getFC
132 reservedHL "import"
133 reexport <- option False (do reservedHL "public"
134 return True)
135 (id, idfc) <- identifier
136 newName <- optional (do reservedHL "as"
137 identifier)
138 option ';' (lchar ';')
139 return $ ImportInfo reexport (toPath id)
140 (fmap (\(n, fc) -> (toPath n, fc)) newName)
141 (map T.pack $ ns id) fc idfc
142 <?> "import statement"
143 where ns = Spl.splitOn "."
144 toPath = foldl1' (</>) . ns
146{-| Parses program source
149 Prog ::= Decl* EOF;
151 -}
152prog :: SyntaxInfo -> IdrisParser [PDecl]
153prog syn = do whiteSpace
154 decls <- many (decl syn)
155 let c = concat decls
156 case maxline syn of
157 Nothing -> do notOpenBraces; eof
158 _ -> return ()
159 ist <- get
160 fc <- getFC
161 put ist { idris_parsedSpan = Just (FC (fc_fname fc) (0,0) (fc_end fc)),
162 ibc_write = IBCParsedRegion fc : ibc_write ist }
163 return c
165{-| Parses a top-level declaration
168Decl ::=
169 Decl'
170 | Using
171 | Params
172 | Mutual
173 | Namespace
174 | Interface
175 | Implementation
176 | DSL
177 | Directive
178 | Provider
179 | Transform
180 | Import!
181 | RunElabDecl
182 ;
184-}
185decl :: SyntaxInfo -> IdrisParser [PDecl]
186decl syn = try (externalDecl syn)
187 <|> internalDecl syn
188 <?> "declaration"
190internalDecl :: SyntaxInfo -> IdrisParser [PDecl]
191internalDecl syn
192 = do fc <- getFC
193 -- if we're after maxline, stop at the next type declaration
194 -- (so we get all cases of a definition to preserve totality
195 -- results, in particular).
196 let continue = case maxline syn of
197 Nothing -> True
198 Just l -> if fst (fc_end fc) > l
199 then mut_nesting syn /= 0
200 else True
201 -- What I'd really like to do here is explicitly save the
202 -- current state, then if reading ahead finds we've passed
203 -- the end of the definition, reset the state. But I've lost
204 -- patience with trying to find out how to do that from the
205 -- trifecta docs, so this does the job instead.
206 if continue then
207 do notEndBlock
208 declBody continue
209 else try (do notEndBlock
210 declBody continue)
211 <|> fail "End of readable input"
212 where declBody :: Bool -> IdrisParser [PDecl]
213 declBody b =
214 try (implementation True syn)
215 <|> try (openInterface syn)
216 <|> declBody' b
217 <|> using_ syn
218 <|> params syn
219 <|> mutual syn
220 <|> namespace syn
221 <|> interface_ syn
222 <|> do d <- dsl syn; return [d]
223 <|> directive syn
224 <|> provider syn
225 <|> transform syn
226 <|> do import_; fail "imports must be at top of file"
227 <?> "declaration"
228 declBody' :: Bool -> IdrisParser [PDecl]
229 declBody' cont = do d <- decl' syn
230 i <- get
231 let d' = fmap (debindApp syn . (desugar syn i)) d
232 if continue cont d'
233 then return [d']
234 else fail "End of readable input"
236 -- Keep going while we're still parsing clauses
237 continue False (PClauses _ _ _ _) = True
238 continue c _ = c
240{-| Parses a top-level declaration with possible syntax sugar
243Decl' ::=
244 Fixity
245 | FunDecl'
246 | Data
247 | Record
248 | SyntaxDecl
249 ;
251-}
252decl' :: SyntaxInfo -> IdrisParser PDecl
253decl' syn = fixity
254 <|> syntaxDecl syn
255 <|> fnDecl' syn
256 <|> data_ syn
257 <|> record syn
258 <|> runElabDecl syn
259 <?> "declaration"
261externalDecl :: SyntaxInfo -> IdrisParser [PDecl]
262externalDecl syn = do i <- get
263 notEndBlock
264 FC fn start _ <- getFC
265 decls <- declExtensions syn (syntaxRulesList $ syntax_rules i)
266 FC _ _ end <- getFC
267 let outerFC = FC fn start end
268 return $ map (mapPDeclFC (fixFC outerFC)
269 (fixFCH fn outerFC))
270 decls
271 where
272 -- | Fix non-highlighting FCs to prevent spurious error location reports
273 fixFC :: FC -> FC -> FC
274 fixFC outer inner | inner `fcIn` outer = inner
275 | otherwise = outer
276 -- | Fix highlighting FCs by obliterating them, to avoid spurious highlights
277 fixFCH fn outer inner | inner `fcIn` outer = inner
278 | otherwise = FileFC fn
280declExtensions :: SyntaxInfo -> [Syntax] -> IdrisParser [PDecl]
281declExtensions syn rules = declExtension syn [] (filter isDeclRule rules)
282 <?> "user-defined declaration"
283 where
284 isDeclRule (DeclRule _ _) = True
285 isDeclRule _ = False
287declExtension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax]
288 -> IdrisParser [PDecl]
289declExtension syn ns rules =
290 choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->
291 case head rs of -- can never be []
292 DeclRule (symb:_) _ -> try $ do
293 n <- extSymbol symb
294 declExtension syn (n : ns) [DeclRule ss t | (DeclRule (_:ss) t) <- rs]
295 -- If we have more than one Rule in this bucket, our grammar is
296 -- nondeterministic.
297 DeclRule [] dec -> let r = map (update (mapMaybe id ns)) dec in
298 return r
300 where
301 update :: [(Name, SynMatch)] -> PDecl -> PDecl
302 update ns = updateNs ns . fmap (updateRefs ns) . fmap (updateSynMatch ns)
304 updateRefs ns = mapPT newref
305 where
306 newref (PRef fc fcs n) = PRef fc fcs (updateB ns n)
307 newref t = t
309 -- Below is a lot of tedious boilerplate which updates any top level
310 -- names in the declaration. It will only change names which are bound in
311 -- the declaration (including method names in interfaces and field names in
312 -- record declarations, not including pattern variables)
313 updateB :: [(Name, SynMatch)] -> Name -> Name
314 updateB ns (NS n mods) = NS (updateB ns n) mods
315 updateB ns n = case lookup n ns of
316 Just (SynBind tfc t) -> t
317 _ -> n
319 updateNs :: [(Name, SynMatch)] -> PDecl -> PDecl
320 updateNs ns (PTy doc argdoc s fc o n fc' t)
321 = PTy doc argdoc s fc o (updateB ns n) fc' t
322 updateNs ns (PClauses fc o n cs)
323 = PClauses fc o (updateB ns n) (map (updateClause ns) cs)
324 updateNs ns (PCAF fc n t) = PCAF fc (updateB ns n) t
325 updateNs ns (PData ds cds s fc o dat)
326 = PData ds cds s fc o (updateData ns dat)
327 updateNs ns (PParams fc ps ds) = PParams fc ps (map (updateNs ns) ds)
328 updateNs ns (PNamespace s fc ds) = PNamespace s fc (map (updateNs ns) ds)
329 updateNs ns (PRecord doc syn fc o n fc' ps pdocs fields cname cdoc s)
330 = PRecord doc syn fc o (updateB ns n) fc' ps pdocs
331 (map (updateField ns) fields)
332 (updateRecCon ns cname)
333 cdoc
334 s
335 updateNs ns (PInterface docs s fc cs cn fc' ps pdocs pdets ds cname cdocs)
336 = PInterface docs s fc cs (updateB ns cn) fc' ps pdocs pdets
337 (map (updateNs ns) ds)
338 (updateRecCon ns cname)
339 cdocs
340 updateNs ns (PImplementation docs pdocs s fc cs pnames acc opts cn fc' ps pextra ity ni ds)
341 = PImplementation docs pdocs s fc cs pnames acc opts (updateB ns cn) fc'
342 ps pextra ity (fmap (updateB ns) ni)
343 (map (updateNs ns) ds)
344 updateNs ns (PMutual fc ds) = PMutual fc (map (updateNs ns) ds)
345 updateNs ns (PProvider docs s fc fc' pw n)
346 = PProvider docs s fc fc' pw (updateB ns n)
347 updateNs ns d = d
349 updateRecCon ns Nothing = Nothing
350 updateRecCon ns (Just (n, fc)) = Just (updateB ns n, fc)
352 updateField ns (m, p, t, doc) = (updateRecCon ns m, p, t, doc)
354 updateClause ns (PClause fc n t ts t' ds)
355 = PClause fc (updateB ns n) t ts t' (map (update ns) ds)
356 updateClause ns (PWith fc n t ts t' m ds)
357 = PWith fc (updateB ns n) t ts t' m (map (update ns) ds)
358 updateClause ns (PClauseR fc ts t ds)
359 = PClauseR fc ts t (map (update ns) ds)
360 updateClause ns (PWithR fc ts t m ds)
361 = PWithR fc ts t m (map (update ns) ds)
363 updateData ns (PDatadecl n fc t cs)
364 = PDatadecl (updateB ns n) fc t (map (updateCon ns) cs)
365 updateData ns (PLaterdecl n fc t)
366 = PLaterdecl (updateB ns n) fc t
368 updateCon ns (cd, ads, cn, fc, ty, fc', fns)
369 = (cd, ads, updateB ns cn, fc, ty, fc', fns)
371 ruleGroup [] [] = True
372 ruleGroup (s1:_) (s2:_) = s1 == s2
373 ruleGroup _ _ = False
375 extSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
376 extSymbol (Keyword n) = do fc <- reservedFC (show n)
377 highlightP fc AnnKeyword
378 return Nothing
379 extSymbol (Expr n) = do tm <- expr syn
380 return $ Just (n, SynTm tm)
381 extSymbol (SimpleExpr n) = do tm <- simpleExpr syn
382 return $ Just (n, SynTm tm)
383 extSymbol (Binding n) = do (b, fc) <- name
384 return $ Just (n, SynBind fc b)
385 extSymbol (Symbol s) = do fc <- symbolFC s
386 highlightP fc AnnKeyword
387 return Nothing
389{-| Parses a syntax extension declaration (and adds the rule to parser state)
392 SyntaxDecl ::= SyntaxRule;
394-}
395syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
396syntaxDecl syn = do s <- syntaxRule syn
397 i <- get
398 put (i `addSyntax` s)
399 fc <- getFC
400 return (PSyntax fc s)
402-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.
403addSyntax :: IState -> Syntax -> IState
404addSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
405 syntax_keywords = ks ++ ns,
406 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc }
407 where rs = syntax_rules i
408 ns = syntax_keywords i
409 ibc = ibc_write i
410 ks = map show (syntaxNames s)
412-- | Like 'addSyntax', but no effect on the IBC.
413addReplSyntax :: IState -> Syntax -> IState
414addReplSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
415 syntax_keywords = ks ++ ns }
416 where rs = syntax_rules i
417 ns = syntax_keywords i
418 ks = map show (syntaxNames s)
420{-| Parses a syntax extension declaration
423SyntaxRuleOpts ::= 'term' | 'pattern';
427SyntaxRule ::=
428 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
432SyntaxSym ::= '[' Name_t ']'
433 | '{' Name_t '}'
434 | Name_t
435 | StringLiteral_t
436 ;
438-}
439syntaxRule :: SyntaxInfo -> IdrisParser Syntax
440syntaxRule syn
441 = do sty <- try (do
442 pushIndent
443 sty <- option AnySyntax
444 (do reservedHL "term"; return TermSyntax
445 <|> do reservedHL "pattern"; return PatternSyntax)
446 reservedHL "syntax"
447 return sty)
448 syms <- some syntaxSym
449 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
450 let ns = mapMaybe getName syms
451 when (length ns /= length (nub ns))
452 $ unexpected "repeated variable in syntax rule"
453 lchar '='
454 tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]
455 terminator
456 return (Rule (mkSimple syms) tm sty)
457 <|> do reservedHL "decl"; reservedHL "syntax"
458 syms <- some syntaxSym
459 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
460 let ns = mapMaybe getName syms
461 when (length ns /= length (nub ns))
462 $ unexpected "repeated variable in syntax rule"
463 lchar '='
464 openBlock
465 dec <- some (decl syn)
466 closeBlock
467 return (DeclRule (mkSimple syms) (concat dec))
468 where
469 isExpr (Expr _) = True
470 isExpr _ = False
471 getName (Expr n) = Just n
472 getName _ = Nothing
473 -- Can't parse two full expressions (i.e. expressions with application) in a row
474 -- so change them both to a simple expression
475 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
476 mkSimple xs = mkSimple' xs
478 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
479 mkSimple es
480 -- Can't parse a full expression followed by operator like characters due to ambiguity
481 mkSimple' (Expr e : Symbol s : es)
482 | takeWhile (`elem` opChars) ts /= "" = SimpleExpr e : Symbol s : mkSimple' es
483 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s
484 mkSimple' (e : es) = e : mkSimple' es
485 mkSimple' [] = []
487 -- Prevent syntax variable capture by making all binders under syntax unique
488 -- (the ol' Common Lisp GENSYM approach)
489 uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
490 uniquifyBinders userNames = fixBind 0 []
491 where
492 fixBind :: Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
493 fixBind 0 rens (PRef fc hls n) | Just n' <- lookup n rens =
494 return $ PRef fc hls n'
495 fixBind 0 rens (PPatvar fc n) | Just n' <- lookup n rens =
496 return $ PPatvar fc n'
497 fixBind 0 rens (PLam fc n nfc ty body)
498 | n `elem` userNames = liftM2 (PLam fc n nfc)
499 (fixBind 0 rens ty)
500 (fixBind 0 rens body)
501 | otherwise =
502 do ty' <- fixBind 0 rens ty
503 n' <- gensym n
504 body' <- fixBind 0 ((n,n'):rens) body
505 return $ PLam fc n' nfc ty' body'
506 fixBind 0 rens (PPi plic n nfc argTy body)
507 | n `elem` userNames = liftM2 (PPi plic n nfc)
508 (fixBind 0 rens argTy)
509 (fixBind 0 rens body)
510 | otherwise =
511 do ty' <- fixBind 0 rens argTy
512 n' <- gensym n
513 body' <- fixBind 0 ((n,n'):rens) body
514 return $ (PPi plic n' nfc ty' body')
515 fixBind 0 rens (PLet fc n nfc ty val body)
516 | n `elem` userNames = liftM3 (PLet fc n nfc)
517 (fixBind 0 rens ty)
518 (fixBind 0 rens val)
519 (fixBind 0 rens body)
520 | otherwise =
521 do ty' <- fixBind 0 rens ty
522 val' <- fixBind 0 rens val
523 n' <- gensym n
524 body' <- fixBind 0 ((n,n'):rens) body
525 return $ PLet fc n' nfc ty' val' body'
526 fixBind 0 rens (PMatchApp fc n) | Just n' <- lookup n rens =
527 return $ PMatchApp fc n'
528 -- Also rename resolved quotations, to allow syntax rules to
529 -- have quoted references to their own bindings.
530 fixBind 0 rens (PQuoteName n True fc) | Just n' <- lookup n rens =
531 return $ PQuoteName n' True fc
533 -- Don't mess with quoted terms
534 fixBind q rens (PQuasiquote tm goal) =
535 flip PQuasiquote goal <$> fixBind (q + 1) rens tm
536 fixBind q rens (PUnquote tm) =
537 PUnquote <$> fixBind (q - 1) rens tm
539 fixBind q rens x = descendM (fixBind q rens) x
541 gensym :: Name -> IdrisParser Name
542 gensym n = do ist <- get
543 let idx = idris_name ist
544 put ist { idris_name = idx + 1 }
545 return $ sMN idx (show n)
547{-| Parses a syntax symbol (either binding variable, keyword or expression)
550SyntaxSym ::= '[' Name_t ']'
551 | '{' Name_t '}'
552 | Name_t
553 | StringLiteral_t
554 ;
556 -}
557syntaxSym :: IdrisParser SSymbol
558syntaxSym = try (do lchar '['; n <- fst <$> name; lchar ']'
559 return (Expr n))
560 <|> try (do lchar '{'; n <- fst <$> name; lchar '}'
561 return (Binding n))
562 <|> do n <- fst <$> iName []
563 return (Keyword n)
564 <|> do sym <- fmap fst stringLiteral
565 return (Symbol sym)
566 <?> "syntax symbol"
568{-| Parses a function declaration with possible syntax sugar
571 FunDecl ::= FunDecl';
573-}
574fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
575fnDecl syn = try (do notEndBlock
576 d <- fnDecl' syn
577 i <- get
578 let d' = fmap (desugar syn i) d
579 return [d']) <?> "function declaration"
581{-| Parses a function declaration
584 FunDecl' ::=
585 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
586 | Postulate
587 | Pattern
588 | CAF
589 ;
591-}
592fnDecl' :: SyntaxInfo -> IdrisParser PDecl
593fnDecl' syn = checkDeclFixity $
594 do (doc, argDocs, fc, opts', n, nfc, acc) <- try (do
595 pushIndent
596 (doc, argDocs) <- docstring syn
597 (opts, acc) <- fnOpts
598 (n_in, nfc) <- fnName
599 let n = expandNS syn n_in
600 fc <- getFC
601 lchar ':'
602 return (doc, argDocs, fc, opts, n, nfc, acc))
603 ty <- typeExpr (allowImp syn)
604 terminator
605 -- If it's a top level function, note the accessibility
606 -- rules
607 when (syn_toplevel syn) $ addAcc n acc
608 return (PTy doc argDocs syn fc opts' n nfc ty)
609 <|> postulate syn
610 <|> caf syn
611 <|> pattern syn
612 <?> "function declaration"
614{-| Parses a series of function and accessbility options
617FnOpts ::= FnOpt* Accessibility FnOpt*
619 -}
620fnOpts :: IdrisParser ([FnOpt], Accessibility)
621fnOpts = do
622 opts <- many fnOpt
623 acc <- accessibility
624 opts' <- many fnOpt
625 let allOpts = opts ++ opts'
626 let existingTotality = allOpts `intersect` [TotalFn, CoveringFn, PartialFn]
627 opts'' <- addDefaultTotality (nub existingTotality) allOpts
628 return (opts'', acc)
629 where prettyTot TotalFn = "total"
630 prettyTot PartialFn = "partial"
631 prettyTot CoveringFn = "covering"
632 addDefaultTotality [] opts = do
633 ist <- get
634 case default_total ist of
635 DefaultCheckingTotal -> return (TotalFn:opts)
636 DefaultCheckingCovering -> return (CoveringFn:opts)
637 DefaultCheckingPartial -> return opts -- Don't add partial so that --warn-partial still reports warnings if necessary
638 addDefaultTotality [tot] opts = return opts
639 -- Should really be a semantics error instead of a parser error
640 addDefaultTotality (tot1:tot2:tots) opts =
641 fail ("Conflicting totality modifiers specified " ++ prettyTot tot1 ++ " and " ++ prettyTot tot2)
644{-| Parses a function option
647FnOpt ::= 'total'
648 | 'partial'
649 | 'covering'
650 | 'implicit'
651 | '%' 'no_implicit'
652 | '%' 'assert_total'
653 | '%' 'error_handler'
654 | '%' 'reflection'
655 | '%' 'specialise' '[' NameTimesList? ']'
656 ;
660NameTimes ::= FnName Natural?;
664NameTimesList ::=
665 NameTimes
666 | NameTimes ',' NameTimesList
667 ;
669-}
670fnOpt :: IdrisParser FnOpt
671fnOpt = do reservedHL "total"; return TotalFn
672 <|> do reservedHL "partial"; return PartialFn
673 <|> do reservedHL "covering"; return CoveringFn
674 <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;
675 return $ CExport c
676 <|> do try (lchar '%' *> reserved "no_implicit");
677 return NoImplicit
678 <|> do try (lchar '%' *> reserved "inline");
679 return Inlinable
680 <|> do try (lchar '%' *> reserved "static");
681 return StaticFn
682 <|> do try (lchar '%' *> reserved "assert_total");
683 fc <- getFC
684 parserWarning fc Nothing (Msg "%assert_total is deprecated. Use the 'assert_total' function instead.")
685 return AssertTotal
686 <|> do try (lchar '%' *> reserved "error_handler");
687 return ErrorHandler
688 <|> do try (lchar '%' *> reserved "error_reverse");
689 return ErrorReverse
690 <|> do try (lchar '%' *> reserved "reflection");
691 return Reflection
692 <|> do try (lchar '%' *> reserved "hint");
693 return AutoHint
694 <|> do try (lchar '%' *> reserved "overlapping");
695 return OverlappingDictionary
696 <|> do lchar '%'; reserved "specialise";
697 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']';
698 return $ Specialise ns
699 <|> do reservedHL "implicit"; return Implicit
700 <?> "function modifier"
701 where nameTimes :: IdrisParser (Name, Maybe Int)
702 nameTimes = do n <- fst <$> fnName
703 t <- option Nothing (do reds <- fmap fst natural
704 return (Just (fromInteger reds)))
705 return (n, t)
707{-| Parses a postulate
710Postulate ::=
711 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
712 ;
714-}
715postulate :: SyntaxInfo -> IdrisParser PDecl
716postulate syn = do (doc, ext)
717 <- try $ do (doc, _) <- docstring syn
718 pushIndent
719 ext <- ppostDecl
720 return (doc, ext)
721 ist <- get
722 (opts, acc) <- fnOpts
723 (n_in, nfc) <- fnName
724 let n = expandNS syn n_in
725 lchar ':'
726 ty <- typeExpr (allowImp syn)
727 fc <- getFC
728 terminator
729 addAcc n acc
730 return (PPostulate ext doc syn fc nfc opts n ty)
731 <?> "postulate"
732 where ppostDecl = do fc <- reservedHL "postulate"; return False
733 <|> do lchar '%'; reserved "extern"; return True
735{-| Parses a using declaration
738Using ::=
739 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
740 ;
742 -}
743using_ :: SyntaxInfo -> IdrisParser [PDecl]
744using_ syn =
745 do reservedHL "using"
746 lchar '('; ns <- usingDeclList syn; lchar ')'
747 openBlock
748 let uvars = using syn
749 ds <- many (decl (syn { using = uvars ++ ns }))
750 closeBlock
751 return (concat ds)
752 <?> "using declaration"
754{-| Parses a parameters declaration
757Params ::=
758 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
759 ;
761-}
762params :: SyntaxInfo -> IdrisParser [PDecl]
763params syn =
764 do reservedHL "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
765 let ns' = [(n, ty) | (n, _, ty) <- ns]
766 openBlock
767 let pvars = syn_params syn
768 ds <- many (decl syn { syn_params = pvars ++ ns' })
769 closeBlock
770 fc <- getFC
771 return [PParams fc ns' (concat ds)]
772 <?> "parameters declaration"
774-- | Parses an open block
775openInterface :: SyntaxInfo -> IdrisParser [PDecl]
776openInterface syn =
777 do reservedHL "using"
778 reservedHL "implementation"
779 fc <- getFC
780 ns <- sepBy1 fnName (lchar ',')
782 openBlock
783 ds <- many (decl syn)
784 closeBlock
785 return [POpenInterfaces fc (map fst ns) (concat ds)]
786 <?> "open interface declaration"
792{-| Parses a mutual declaration (for mutually recursive functions)
795Mutual ::=
796 'mutual' OpenBlock Decl* CloseBlock
797 ;
799-}
800mutual :: SyntaxInfo -> IdrisParser [PDecl]
801mutual syn =
802 do reservedHL "mutual"
803 openBlock
804 let pvars = syn_params syn
805 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
806 closeBlock
807 fc <- getFC
808 return [PMutual fc (concat ds)]
809 <?> "mutual block"
811{-| Parses a namespace declaration
814Namespace ::=
815 'namespace' identifier OpenBlock Decl+ CloseBlock
816 ;
818-}
819namespace :: SyntaxInfo -> IdrisParser [PDecl]
820namespace syn =
821 do reservedHL "namespace"
822 (n, nfc) <- identifier
823 openBlock
824 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
825 closeBlock
826 return [PNamespace n nfc (concat ds)]
827 <?> "namespace declaration"
829{-| Parses a methods block (for implementations)
832 ImplementationBlock ::= 'where' OpenBlock FnDecl* CloseBlock
834-}
835implementationBlock :: SyntaxInfo -> IdrisParser [PDecl]
836implementationBlock syn = do reservedHL "where"
837 openBlock
838 ds <- many (fnDecl syn)
839 closeBlock
840 return (concat ds)
841 <?> "implementation block"
843{-| Parses a methods and implementations block (for interfaces)
846MethodOrImplementation ::=
847 FnDecl
848 | Implementation
849 ;
853InterfaceBlock ::=
854 'where' OpenBlock Constructor? MethodOrImplementation* CloseBlock
855 ;
857-}
858interfaceBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])
859interfaceBlock syn = do reservedHL "where"
860 openBlock
861 (cn, cd) <- option (Nothing, emptyDocstring) $
862 try (do (doc, _) <- option noDocs docComment
863 n <- constructor
864 return (Just n, doc))
865 ist <- get
866 let cd' = annotate syn ist cd
868 ds <- many (notEndBlock >> try (implementation True syn)
869 <|> do x <- data_ syn
870 return [x]
871 <|> fnDecl syn)
872 closeBlock
873 return (cn, cd', concat ds)
874 <?> "interface block"
875 where
876 constructor :: IdrisParser (Name, FC)
877 constructor = reservedHL "constructor" *> fnName
879 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)
880 annotate syn ist = annotCode $ tryFullExpr syn ist
882{-| Parses an interface declaration
885InterfaceArgument ::=
886 Name
887 | '(' Name ':' Expr ')'
888 ;
892Interface ::=
893 DocComment_t? Accessibility? 'interface' ConstraintList? Name InterfaceArgument* InterfaceBlock?
894 ;
896-}
897interface_ :: SyntaxInfo -> IdrisParser [PDecl]
898interface_ syn = do (doc, argDocs, acc)
899 <- try (do (doc, argDocs) <- docstring syn
900 acc <- accessibility
901 interfaceKeyword
902 return (doc, argDocs, acc))
903 fc <- getFC
904 cons <- constraintList syn
905 let cons' = [(c, ty) | (c, _, ty) <- cons]
906 (n_in, nfc) <- fnName
907 let n = expandNS syn n_in
908 cs <- many carg
909 fds <- option [(cn, NoFC) | (cn, _, _) <- cs] fundeps
910 (cn, cd, ds) <- option (Nothing, fst noDocs, []) (interfaceBlock syn)
911 accData acc n (concatMap declared ds)
912 return [PInterface doc syn fc cons' n nfc cs argDocs fds ds cn cd]
913 <?> "interface declaration"
914 where
915 fundeps :: IdrisParser [(Name, FC)]
916 fundeps = do lchar '|'; sepBy name (lchar ',')
918 interfaceKeyword :: IdrisParser ()
919 interfaceKeyword = reservedHL "interface"
920 <|> do reservedHL "class"
921 fc <- getFC
922 parserWarning fc Nothing (Msg "The 'class' keyword is deprecated. Use 'interface' instead.")
924 carg :: IdrisParser (Name, FC, PTerm)
925 carg = do lchar '('; (i, ifc) <- name; lchar ':'; ty <- expr syn; lchar ')'
926 return (i, ifc, ty)
927 <|> do (i, ifc) <- name
928 fc <- getFC
929 return (i, ifc, PType fc)
931{-| Parses an interface implementation declaration
934 Implementation ::=
935 DocComment_t? 'implementation' ImplementationName? ConstraintList? Name SimpleExpr* ImplementationBlock?
936 ;
940ImplementationName ::= '[' Name ']';
942-}
943implementation :: Bool -> SyntaxInfo -> IdrisParser [PDecl]
944implementation kwopt syn
945 = do ist <- get
946 (doc, argDocs) <- docstring syn
947 (opts, acc) <- fnOpts
948 if kwopt then optional implementationKeyword
949 else do implementationKeyword
950 return (Just ())
952 fc <- getFC
953 en <- optional implementationName
954 cs <- constraintList syn
955 let cs' = [(c, ty) | (c, _, ty) <- cs]
956 (cn, cnfc) <- fnName
957 args <- many (simpleExpr syn)
958 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)
959 let t = bindList (PPi constraint) cs sc
960 pnames <- implementationUsing
961 ds <- implementationBlock syn
962 return [PImplementation doc argDocs syn fc cs' pnames acc opts cn cnfc args [] t en ds]
963 <?> "implementation declaration"
964 where implementationName :: IdrisParser Name
965 implementationName = do lchar '['; n_in <- fst <$> fnName; lchar ']'
966 let n = expandNS syn n_in
967 return n
968 <?> "implementation name"
969 implementationKeyword :: IdrisParser ()
970 implementationKeyword = reservedHL "implementation"
971 <|> do reservedHL "instance"
972 fc <- getFC
973 parserWarning fc Nothing (Msg "The 'instance' keyword is deprecated. Use 'implementation' (or omit it) instead.")
975 implementationUsing :: IdrisParser [Name]
976 implementationUsing = do reservedHL "using"
977 ns <- sepBy1 fnName (lchar ',')
978 return (map fst ns)
979 <|> return []
981-- | Parse a docstring
982docstring :: SyntaxInfo
983 -> IdrisParser (Docstring (Either Err PTerm),
984 [(Name,Docstring (Either Err PTerm))])
985docstring syn = do (doc, argDocs) <- option noDocs docComment
986 ist <- get
987 let doc' = annotCode (tryFullExpr syn ist) doc
988 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
989 | (n, d) <- argDocs ]
990 return (doc', argDocs')
993{-| Parses a using declaration list
996UsingDeclList ::=
997 UsingDeclList'
998 | NameList TypeSig
999 ;
1003UsingDeclList' ::=
1004 UsingDecl
1005 | UsingDecl ',' UsingDeclList'
1010NameList ::=
1011 Name
1012 | Name ',' NameList
1016usingDeclList :: SyntaxInfo -> IdrisParser [Using]
1017usingDeclList syn
1018 = try (sepBy1 (usingDecl syn) (lchar ','))
1019 <|> do ns <- sepBy1 (fst <$> name) (lchar ',')
1020 lchar ':'
1021 t <- typeExpr (disallowImp syn)
1022 return (map (\x -> UImplicit x t) ns)
1023 <?> "using declaration list"
1025{-| Parses a using declaration
1028UsingDecl ::=
1029 FnName TypeSig
1030 | FnName FnName+
1034usingDecl :: SyntaxInfo -> IdrisParser Using
1035usingDecl syn = try (do x <- fst <$> fnName
1036 lchar ':'
1037 t <- typeExpr (disallowImp syn)
1038 return (UImplicit x t))
1039 <|> do c <- fst <$> fnName
1040 xs <- many (fst <$> fnName)
1041 return (UConstraint c xs)
1042 <?> "using declaration"
1044{-| Parse a clause with patterns
1047Pattern ::= Clause;
1050pattern :: SyntaxInfo -> IdrisParser PDecl
1051pattern syn = do fc <- getFC
1052 clause <- clause syn
1053 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
1054 <?> "pattern"
1056{-| Parse a constant applicative form declaration
1059CAF ::= 'let' FnName '=' Expr Terminator;
1062caf :: SyntaxInfo -> IdrisParser PDecl
1063caf syn = do reservedHL "let"
1064 n_in <- fst <$> fnName; let n = expandNS syn n_in
1065 pushIndent
1066 lchar '='
1067 t <- indented $ expr syn
1068 terminator
1069 fc <- getFC
1070 return (PCAF fc n t)
1071 <?> "constant applicative form declaration"
1073{-| Parse an argument expression
1076ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
1079argExpr :: SyntaxInfo -> IdrisParser PTerm
1080argExpr syn = let syn' = syn { inPattern = True } in
1081 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
1082 <?> "argument expression"
1084{-| Parse a right hand side of a function
1087RHS ::= '=' Expr
1088 | '?=' RHSName? Expr
1089 | Impossible
1094RHSName ::= '{' FnName '}';
1097rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
1098rhs syn n = do lchar '='
1099 indentPropHolds gtProp
1100 expr syn
1101 <|> do symbol "?=";
1102 fc <- getFC
1103 name <- option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";
1104 return n)
1105 r <- expr syn
1106 return (addLet fc name r)
1107 <|> impossible
1108 <?> "function right hand side"
1109 where mkN :: Name -> Name
1110 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
1111 then sUN "infix_op_lemma_1"
1112 else sUN (str x++"_lemma_1")
1113 mkN (NS x n) = NS (mkN x) n
1114 n' :: Name
1115 n' = mkN n
1116 addLet :: FC -> Name -> PTerm -> PTerm
1117 addLet fc nm (PLet fc' n nfc ty val r) = PLet fc' n nfc ty val (addLet fc nm r)
1118 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
1119 where addLetC (l, r) = (l, addLet fc nm r)
1120 addLet fc nm r = (PLet fc (sUN "value") NoFC Placeholder r (PMetavar NoFC nm))
1122{-|Parses a function clause
1125RHSOrWithBlock ::= RHS WhereOrTerminator
1126 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
1131Clause ::= WExpr+ RHSOrWithBlock
1132 | SimpleExpr '<==' FnName RHS WhereOrTerminator
1133 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
1134 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
1139ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
1143WhereOrTerminator ::= WhereBlock | Terminator;
1146clause :: SyntaxInfo -> IdrisParser PClause
1147clause syn
1148 = do wargs <- try (do pushIndent; some (wExpr syn))
1149 fc <- getFC
1150 ist <- get
1151 n <- case lastParse ist of
1152 Just t -> return t
1153 Nothing -> fail "Invalid clause"
1154 (do r <- rhs syn n
1155 let ctxt = tt_ctxt ist
1156 let wsyn = syn { syn_namespace = [], syn_toplevel = False }
1157 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1158 popIndent
1159 return x,
1160 do terminator
1161 return ([], [])]
1162 return $ PClauseR fc wargs r wheres) <|> (do
1163 popIndent
1164 reservedHL "with"
1165 wval <- simpleExpr syn
1166 pn <- optProof
1167 openBlock
1168 ds <- some $ fnDecl syn
1169 let withs = concat ds
1170 closeBlock
1171 return $ PWithR fc wargs wval pn withs)
1172 <|> do ty <- try (do pushIndent
1173 ty <- simpleExpr syn
1174 symbol "<=="
1175 return ty)
1176 fc <- getFC
1177 n_in <- fst <$> fnName; let n = expandNS syn n_in
1178 r <- rhs syn n
1179 ist <- get
1180 let ctxt = tt_ctxt ist
1181 let wsyn = syn { syn_namespace = [] }
1182 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1183 popIndent
1184 return x,
1185 do terminator
1186 return ([], [])]
1187 let capp = PLet fc (sMN 0 "match") NoFC
1188 ty
1189 (PMatchApp fc n)
1190 (PRef fc [] (sMN 0 "match"))
1191 ist <- get
1192 put (ist { lastParse = Just n })
1193 return $ PClause fc n capp [] r wheres
1194 <|> do (l, op, nfc) <- try (do
1195 pushIndent
1196 l <- argExpr syn
1197 (op, nfc) <- operatorFC
1198 when (op == "=" || op == "?=" ) $
1199 fail "infix clause definition with \"=\" and \"?=\" not supported "
1200 return (l, op, nfc))
1201 let n = expandNS syn (sUN op)
1202 r <- argExpr syn
1203 fc <- getFC
1204 wargs <- many (wExpr syn)
1205 (do rs <- rhs syn n
1206 let wsyn = syn { syn_namespace = [] }
1207 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1208 popIndent
1209 return x,
1210 do terminator
1211 return ([], [])]
1212 ist <- get
1213 let capp = PApp fc (PRef nfc [nfc] n) [pexp l, pexp r]
1214 put (ist { lastParse = Just n })
1215 return $ PClause fc n capp wargs rs wheres) <|> (do
1216 popIndent
1217 reservedHL "with"
1218 wval <- bracketed syn
1219 pn <- optProof
1220 openBlock
1221 ds <- some $ fnDecl syn
1222 closeBlock
1223 ist <- get
1224 let capp = PApp fc (PRef fc [] n) [pexp l, pexp r]
1225 let withs = map (fillLHSD n capp wargs) $ concat ds
1226 put (ist { lastParse = Just n })
1227 return $ PWith fc n capp wargs wval pn withs)
1228 <|> do pushIndent
1229 (n_in, nfc) <- fnName; let n = expandNS syn n_in
1230 fc <- getFC
1231 args <- many (try (implicitArg (syn { inPattern = True } ))
1232 <|> try (constraintArg (syn { inPattern = True }))
1233 <|> (fmap pexp (argExpr syn)))
1234 wargs <- many (wExpr syn)
1235 let capp = PApp fc (PRef nfc [nfc] n) args
1236 (do r <- rhs syn n
1237 ist <- get
1238 let ctxt = tt_ctxt ist
1239 let wsyn = syn { syn_namespace = [] }
1240 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1241 popIndent
1242 return x,
1243 do terminator
1244 return ([], [])]
1245 ist <- get
1246 put (ist { lastParse = Just n })
1247 return $ PClause fc n capp wargs r wheres) <|> (do
1248 reservedHL "with"
1249 ist <- get
1250 put (ist { lastParse = Just n })
1251 wval <- bracketed syn
1252 pn <- optProof
1253 openBlock
1254 ds <- some $ fnDecl syn
1255 let withs = map (fillLHSD n capp wargs) $ concat ds
1256 closeBlock
1257 popIndent
1258 return $ PWith fc n capp wargs wval pn withs)
1259 <?> "function clause"
1260 where
1261 optProof = option Nothing (do reservedHL "proof"
1262 n <- fnName
1263 return (Just n))
1265 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
1266 fillLHS n capp owargs (PClauseR fc wargs v ws)
1267 = PClause fc n capp (owargs ++ wargs) v ws
1268 fillLHS n capp owargs (PWithR fc wargs v pn ws)
1269 = PWith fc n capp (owargs ++ wargs) v pn
1270 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1271 fillLHS _ _ _ c = c
1273 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
1274 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1275 fillLHSD n c a x = x
1277{-| Parses with pattern
1280WExpr ::= '|' Expr';
1283wExpr :: SyntaxInfo -> IdrisParser PTerm
1284wExpr syn = do lchar '|'
1285 expr' (syn { inPattern = True })
1286 <?> "with pattern"
1288{-| Parses a where block
1291WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
1294whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
1295whereBlock n syn
1296 = do reservedHL "where"
1297 ds <- indentedBlock1 (decl syn)
1298 let dns = concatMap (concatMap declared) ds
1299 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1300 <?> "where block"
1302{-|Parses a code generation target language name
1305Codegen ::= 'C'
1306 | 'Java'
1307 | 'JavaScript'
1308 | 'Node'
1309 | 'LLVM'
1310 | 'Bytecode'
1314codegen_ :: IdrisParser Codegen
1315codegen_ = do n <- fst <$> identifier
1316 return (Via IBCFormat (map toLower n))
1317 <|> do reserved "Bytecode"; return Bytecode
1318 <?> "code generation language"
1320{-|Parses a compiler directive
1322StringList ::=
1323 String
1324 | String ',' StringList
1329Directive ::= '%' Directive';
1333Directive' ::= 'lib' CodeGen String_t
1334 | 'link' CodeGen String_t
1335 | 'flag' CodeGen String_t
1336 | 'include' CodeGen String_t
1337 | 'hide' Name
1338 | 'freeze' Name
1339 | 'thaw' Name
1340 | 'access' Accessibility
1341 | 'default' Totality
1342 | 'logging' Natural
1343 | 'dynamic' StringList
1344 | 'name' Name NameList
1345 | 'error_handlers' Name NameList
1346 | 'language' 'TypeProviders'
1347 | 'language' 'ErrorReflection'
1348 | 'deprecated' Name String
1349 | 'fragile' Name Reason
1353directive :: SyntaxInfo -> IdrisParser [PDecl]
1354directive syn = do try (lchar '%' *> reserved "lib")
1355 cgn <- codegen_
1356 lib <- fmap fst stringLiteral
1357 return [PDirective (DLib cgn lib)]
1358 <|> do try (lchar '%' *> reserved "link")
1359 cgn <- codegen_; obj <- fst <$> stringLiteral
1360 return [PDirective (DLink cgn obj)]
1361 <|> do try (lchar '%' *> reserved "flag")
1362 cgn <- codegen_; flag <- fst <$> stringLiteral
1363 return [PDirective (DFlag cgn flag)]
1364 <|> do try (lchar '%' *> reserved "include")
1365 cgn <- codegen_
1366 hdr <- fst <$> stringLiteral
1367 return [PDirective (DInclude cgn hdr)]
1368 <|> do try (lchar '%' *> reserved "hide"); n <- fst <$> fnName
1369 return [PDirective (DHide n)]
1370 <|> do try (lchar '%' *> reserved "freeze"); n <- fst <$> iName []
1371 return [PDirective (DFreeze n)]
1372 <|> do try (lchar '%' *> reserved "thaw"); n <- fst <$> iName []
1373 return [PDirective (DThaw n)]
1374 -- injectivity assertins are intended for debugging purposes
1375 -- only, and won't be documented/could be removed at any point
1376 <|> do try (lchar '%' *> reserved "assert_injective"); n <- fst <$> fnName
1377 return [PDirective (DInjective n)]
1378 -- Assert totality of something after definition. This is
1379 -- here as a debugging aid, so commented out...
1380-- <|> do try (lchar '%' *> reserved "assert_set_total"); n <- fst <$> fnName
1381-- return [PDirective (DSetTotal n)]
1382 <|> do try (lchar '%' *> reserved "access")
1383 acc <- accessibility
1384 ist <- get
1385 put ist { default_access = acc }
1386 return [PDirective (DAccess acc)]
1387 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1388 i <- get
1389 put (i { default_total = tot } )
1390 return [PDirective (DDefault tot)]
1391 <|> do try (lchar '%' *> reserved "logging")
1392 i <- fst <$> natural
1393 return [PDirective (DLogging i)]
1394 <|> do try (lchar '%' *> reserved "dynamic")
1395 libs <- sepBy1 (fmap fst stringLiteral) (lchar ',')
1396 return [PDirective (DDynamicLibs libs)]
1397 <|> do try (lchar '%' *> reserved "name")
1398 (ty, tyFC) <- fnName
1399 ns <- sepBy1 name (lchar ',')
1400 return [PDirective (DNameHint ty tyFC ns)]
1401 <|> do try (lchar '%' *> reserved "error_handlers")
1402 (fn, nfc) <- fnName
1403 (arg, afc) <- fnName
1404 ns <- sepBy1 name (lchar ',')
1405 return [PDirective (DErrorHandlers fn nfc arg afc ns) ]
1406 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1407 return [PDirective (DLanguage ext)]
1408 <|> do try (lchar '%' *> reserved "deprecate")
1409 n <- fst <$> fnName
1410 alt <- option "" (fst <$> stringLiteral)
1411 return [PDirective (DDeprecate n alt)]
1412 <|> do try (lchar '%' *> reserved "fragile")
1413 n <- fst <$> fnName
1414 alt <- option "" (fst <$> stringLiteral)
1415 return [PDirective (DFragile n alt)]
1416 <|> do fc <- getFC
1417 try (lchar '%' *> reserved "used")
1418 fn <- fst <$> fnName
1419 arg <- fst <$> iName []
1420 return [PDirective (DUsed fc fn arg)]
1421 <|> do try (lchar '%' *> reserved "auto_implicits")
1422 b <- on_off
1423 return [PDirective (DAutoImplicits b)]
1424 <?> "directive"
1425 where on_off = do reserved "on"; return True
1426 <|> do reserved "off"; return False
1428pLangExt :: IdrisParser LanguageExt
1429pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1430 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1432{-| Parses a totality
1435Totality ::= 'partial' | 'total' | 'covering'
1439totality :: IdrisParser DefaultTotality
1440totality
1441 = do reservedHL "total"; return DefaultCheckingTotal
1442 <|> do reservedHL "partial"; return DefaultCheckingPartial
1443 <|> do reservedHL "covering"; return DefaultCheckingCovering
1445{-| Parses a type provider
1448Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1449ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1451 -}
1452provider :: SyntaxInfo -> IdrisParser [PDecl]
1453provider syn = do doc <- try (do (doc, _) <- docstring syn
1454 fc1 <- getFC
1455 lchar '%'
1456 fc2 <- reservedFC "provide"
1457 highlightP (spanFC fc1 fc2) AnnKeyword
1458 return doc)
1459 provideTerm doc <|> providePostulate doc
1460 <?> "type provider"
1461 where provideTerm doc =
1462 do lchar '('; (n, nfc) <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1463 fc <- getFC
1464 reservedHL "with"
1465 e <- expr syn <?> "provider expression"
1466 return [PProvider doc syn fc nfc (ProvTerm t e) n]
1467 providePostulate doc =
1468 do reservedHL "postulate"
1469 (n, nfc) <- fnName
1470 fc <- getFC
1471 reservedHL "with"
1472 e <- expr syn <?> "provider expression"
1473 return [PProvider doc syn fc nfc (ProvPostulate e) n]
1475{-| Parses a transform
1478Transform ::= '%' 'transform' Expr '==>' Expr
1481transform :: SyntaxInfo -> IdrisParser [PDecl]
1482transform syn = do try (lchar '%' *> reserved "transform")
1483 -- leave it unchecked, until we work out what this should
1484 -- actually mean...
1485-- safety <- option True (do reserved "unsafe"
1486-- return False)
1487 l <- expr syn
1488 fc <- getFC
1489 symbol "==>"
1490 r <- expr syn
1491 return [PTransform fc False l r]
1492 <?> "transform"
1494{-| Parses a top-level reflected elaborator script
1497RunElabDecl ::= '%' 'runElab' Expr
1500runElabDecl :: SyntaxInfo -> IdrisParser PDecl
1501runElabDecl syn =
1502 do kwFC <- try (do fc <- getFC
1503 lchar '%'
1504 fc' <- reservedFC "runElab"
1505 return (spanFC fc fc'))
1506 script <- expr syn <?> "elaborator script"
1507 highlightP kwFC AnnKeyword
1508 return $ PRunElabDecl kwFC script (syn_namespace syn)
1509 <?> "top-level elaborator script"
1511{- * Loading and parsing -}
1512{-| Parses an expression from input -}
1513parseExpr :: IState -> String -> Result PTerm
1514parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1516{-| Parses a constant form input -}
1517parseConst :: IState -> String -> Result Const
1518parseConst st = runparser (fmap fst constant) st "(input)"
1520{-| Parses a tactic from input -}
1521parseTactic :: IState -> String -> Result PTactic
1522parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1524{-| Parses a do-step from input (used in the elab shell) -}
1525parseElabShellStep :: IState -> String -> Result (Either ElabShellCmd PDo)
1526parseElabShellStep ist = runparser (fmap Right (do_ defaultSyntax) <|> fmap Left elabShellCmd) ist "(input)"
1527 where elabShellCmd = char ':' >>
1528 (reserved "qed" >> pure EQED ) <|>
1529 (reserved "abandon" >> pure EAbandon ) <|>
1530 (reserved "undo" >> pure EUndo ) <|>
1531 (reserved "state" >> pure EProofState) <|>
1532 (reserved "term" >> pure EProofTerm ) <|>
1533 (expressionTactic ["e", "eval"] EEval ) <|>
1534 (expressionTactic ["t", "type"] ECheck) <|>
1535 (expressionTactic ["search"] ESearch ) <|>
1536 (do reserved "doc"
1537 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)
1538 eof
1539 return (EDocStr doc))
1540 <?> "elab command"
1541 expressionTactic cmds tactic =
1542 do asum (map reserved cmds)
1543 t <- spaced (expr defaultSyntax)
1544 i <- get
1545 return $ tactic (desugar defaultSyntax i t)
1546 spaced parser = indentPropHolds gtProp *> parser
1548-- | Parse module header and imports
1549parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Delta)
1550parseImports fname input
1551 = do i <- getIState
1552 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1553 Failure (ErrInfo err _) -> fail (show err)
1554 Success (x, annots, i) ->
1555 do putIState i
1556 fname' <- runIO $ Dir.makeAbsolute fname
1557 sendHighlighting $ addPath annots fname'
1558 return x
1559 where imports :: IdrisParser ((Maybe (Docstring ()), [String],
1560 [ImportInfo],
1561 Maybe Delta),
1562 [(FC, OutputAnnotation)], IState)
1563 imports = do whiteSpace
1564 (mdoc, mname, annots) <- moduleHeader
1565 ps_exp <- many import_
1566 mrk <- mark
1567 isEof <- lookAheadMatches eof
1568 let mrk' = if isEof
1569 then Nothing
1570 else Just mrk
1571 i <- get
1572 -- add Builtins and Prelude, unless options say
1573 -- not to
1574 let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp
1575 return ((mdoc, mname, ps, mrk'), annots, i)
1577 imp m = ImportInfo False (toPath m)
1578 Nothing [] NoFC NoFC
1579 ns = Spl.splitOn "."
1580 toPath = foldl1' (</>) . ns
1582 addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]
1583 addPath [] _ = []
1584 addPath ((fc, AnnNamespace ns Nothing) : annots) path =
1585 (fc, AnnNamespace ns (Just path)) : addPath annots path
1586 addPath (annot:annots) path = annot : addPath annots path
1588-- | There should be a better way of doing this...
1589findFC :: Doc -> (FC, String)
1590findFC x = let s = show (plain x) in findFC' s
1591 where findFC' s = case span (/= ':') s of
1592 -- Horrid kludge to prevent crashes on Windows
1593 (prefix, ':':'\\':rest) ->
1594 case findFC' rest of
1595 (NoFC, msg) -> (NoFC, msg)
1596 (FileFC f, msg) -> (FileFC (prefix ++ ":\\" ++ f), msg)
1597 (FC f start end, msg) -> (FC (prefix ++ ":\\" ++ f) start end, msg)
1598 (failname, ':':rest) -> case span isDigit rest of
1599 (line, ':':rest') -> case span isDigit rest' of
1600 (col, ':':msg) -> let pos = (read line, read col) in
1601 (FC failname pos pos, msg)
1603-- | Check if the coloring matches the options and corrects if necessary
1604fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1605fixColour False doc = ANSI.plain doc
1606fixColour True doc = doc
1608-- | A program is a list of declarations, possibly with associated
1609-- documentation strings.
1610parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1611 Idris [PDecl]
1612parseProg syn fname input mrk
1613 = do i <- getIState
1614 case runparser mainProg i fname input of
1615 Failure (ErrInfo doc _) -> do -- FIXME: Get error location from trifecta
1616 -- this can't be the solution!
1617 -- Issue #1575 on the issue tracker.
1618 -- https://github.com/idris-lang/Idris-dev/issues/1575
1619 let (fc, msg) = findFC doc
1620 i <- getIState
1621 case idris_outputmode i of
1622 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1623 IdeMode n h -> iWarn fc (P.text msg)
1624 putIState (i { errSpan = Just fc })
1625 return []
1626 Success (x, i) -> do putIState i
1627 reportParserWarnings
1628 return $ collect x
1629 where mainProg :: IdrisParser ([PDecl], IState)
1630 mainProg = case mrk of
1631 Nothing -> do i <- get; return ([], i)
1632 Just mrk -> do
1633 release mrk
1634 ds <- prog syn
1635 i' <- get
1636 return (ds, i')
1638{-| Load idris module and show error if something wrong happens -}
1639loadModule :: FilePath -> IBCPhase -> Idris (Maybe String)
1640loadModule f phase
1641 = idrisCatch (loadModule' f phase)
1642 (\e -> do setErrSpan (getErrSpan e)
1643 ist <- getIState
1644 iWarn (getErrSpan e) $ pprintErr ist e
1645 return Nothing)
1647{-| Load idris module -}
1648loadModule' :: FilePath -> IBCPhase -> Idris (Maybe String)
1649loadModule' f phase
1650 = do i <- getIState
1651 let file = takeWhile (/= ' ') f
1652 ibcsd <- valIBCSubDir i
1653 ids <- allImportDirs
1654 fp <- findImport ids ibcsd file
1655 if file `elem` imported i
1656 then do logParser 1 $ "Already read " ++ file
1657 return Nothing
1658 else do putIState (i { imported = file : imported i })
1659 case fp of
1660 IDR fn -> loadSource False fn Nothing
1661 LIDR fn -> loadSource True fn Nothing
1662 IBC fn src ->
1663 idrisCatch (loadIBC True phase fn)
1664 (\c -> do logParser 1 $ fn ++ " failed " ++ pshow i c
1665 case src of
1666 IDR sfn -> loadSource False sfn Nothing
1667 LIDR sfn -> loadSource True sfn Nothing)
1668 return $ Just file
1670{-| Load idris code from file -}
1671loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()
1672loadFromIFile reexp phase i@(IBC fn src) maxline
1673 = do logParser 1 $ "Skipping " ++ getSrcFile i
1674 idrisCatch (loadIBC reexp phase fn)
1675 (\err -> ierror $ LoadingFailed fn err)
1676 where
1677 getSrcFile (IDR fn) = fn
1678 getSrcFile (LIDR fn) = fn
1679 getSrcFile (IBC f src) = getSrcFile src
1681loadFromIFile _ _ (IDR fn) maxline = loadSource' False fn maxline
1682loadFromIFile _ _ (LIDR fn) maxline = loadSource' True fn maxline
1684{-| Load idris source code and show error if something wrong happens -}
1685loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1686loadSource' lidr r maxline
1687 = idrisCatch (loadSource lidr r maxline)
1688 (\e -> do setErrSpan (getErrSpan e)
1689 ist <- getIState
1690 case e of
1691 At f e' -> iWarn f (pprintErr ist e')
1692 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1694{-| Load Idris source code-}
1695loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1696loadSource lidr f toline
1697 = do logParser 1 ("Reading " ++ f)
1698 i <- getIState
1699 let def_total = default_total i
1700 file_in <- runIO $ readSource f
1701 file <- if lidr then tclift $ unlit f file_in else return file_in
1702 (mdocs, mname, imports_in, pos) <- parseImports f file
1703 ai <- getAutoImports
1704 let imports = map (\n -> ImportInfo True n Nothing [] NoFC NoFC) ai ++ imports_in
1705 ids <- allImportDirs
1706 ibcsd <- valIBCSubDir i
1707 mapM_ (\(re, f, ns, nfc) ->
1708 do fp <- findImport ids ibcsd f
1709 case fp of
1710 LIDR fn -> ifail $ "No ibc for " ++ f
1711 IDR fn -> ifail $ "No ibc for " ++ f
1712 IBC fn src ->
1713 do loadIBC True IBC_Building fn
1714 let srcFn = case src of
1715 IDR fn -> Just fn
1716 LIDR fn -> Just fn
1717 _ -> Nothing
1718 srcFnAbs <- case srcFn of
1719 Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)
1720 Nothing -> return Nothing
1721 sendHighlighting [(nfc, AnnNamespace ns srcFnAbs)])
1722 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]
1723 reportParserWarnings
1724 sendParserHighlighting
1726 -- process and check module aliases
1727 let modAliases = M.fromList
1728 [ (prep alias, prep realName)
1729 | ImportInfo { import_reexport = reexport
1730 , import_path = realName
1731 , import_rename = Just (alias, _)
1732 , import_location = fc } <- imports
1734 prep = map T.pack . reverse . Spl.splitOn [pathSeparator]
1735 aliasNames = [ (alias, fc)
1736 | ImportInfo { import_rename = Just (alias, _)
1737 , import_location = fc } <- imports
1739 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1740 case map head . filter ((/= 1) . length) $ histogram of
1741 [] -> logParser 3 $ "Module aliases: " ++ show (M.toList modAliases)
1742 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1744 i <- getIState
1745 putIState (i { default_access = Private, module_aliases = modAliases })
1746 clearIBC -- start a new .ibc file
1747 -- record package info in .ibc
1748 imps <- allImportDirs
1749 mapM_ addIBC (map IBCImportDir imps)
1750 mapM_ (addIBC . IBCImport)
1751 [ (reexport, realName)
1752 | ImportInfo { import_reexport = reexport
1753 , import_path = realName
1754 } <- imports
1756 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1757 maxline = toline }
1758 ist <- getIState
1759 -- Save the span from parsing the module header, because
1760 -- an empty program parse might obliterate it.
1761 let oldSpan = idris_parsedSpan ist
1762 ds' <- parseProg syntax f file pos
1764 case (ds', oldSpan) of
1765 ([], Just fc) ->
1766 -- If no program elements were parsed, we dind't
1767 -- get a loaded region in the IBC file. That
1768 -- means we need to add it back.
1769 do ist <- getIState
1770 putIState ist { idris_parsedSpan = oldSpan
1771 , ibc_write = IBCParsedRegion fc :
1772 ibc_write ist
1774 _ -> return ()
1775 sendParserHighlighting
1777 -- Parsing done, now process declarations
1779 let ds = namespaces mname ds'
1780 logParser 3 (show $ showDecls verbosePPOption ds)
1781 i <- getIState
1782 logLvl 10 (show (toAlist (idris_implicits i)))
1783 logLvl 3 (show (idris_infixes i))
1784 -- Now add all the declarations to the context
1785 v <- verbose
1786 when v $ iputStrLn $ "Type checking " ++ f
1787 -- we totality check after every Mutual block, so if
1788 -- anything is a single definition, wrap it in a
1789 -- mutual block on its own
1790 elabDecls (toplevelWith f) (map toMutual ds)
1791 i <- getIState
1792 -- simplify every definition do give the totality checker
1793 -- a better chance
1794 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1795 ctxt' <-
1796 do ctxt <- getContext
1797 tclift $ simplifyCasedef n (getErasureInfo i) ctxt
1798 setContext ctxt')
1799 (map snd (idris_totcheck i))
1800 -- build size change graph from simplified definitions
1801 logLvl 1 "Totality checking"
1802 i <- getIState
1803 mapM_ buildSCG (idris_totcheck i)
1804 mapM_ checkDeclTotality (idris_totcheck i)
1805 mapM_ verifyTotality (idris_totcheck i)
1807 -- Redo totality check for deferred names
1808 let deftots = idris_defertotcheck i
1809 logLvl 2 $ "Totality checking " ++ show deftots
1810 mapM_ (\x -> do tot <- getTotality x
1811 case tot of
1812 Total _ ->
1813 do let opts = case lookupCtxtExact x (idris_flags i) of
1814 Just os -> os
1815 Nothing -> []
1816 when (AssertTotal `notElem` opts) $
1817 setTotality x Unchecked
1818 _ -> return ()) (map snd deftots)
1819 mapM_ buildSCG deftots
1820 mapM_ checkDeclTotality deftots
1822 logLvl 1 ("Finished " ++ f)
1823 ibcsd <- valIBCSubDir i
1824 logLvl 1 "Universe checking"
1825 iucheck
1826 let ibc = ibcPathNoFallback ibcsd f
1827 i <- getIState
1828 addHides (hide_list i)
1830 -- Save module documentation if applicable
1831 i <- getIState
1832 case mdocs of
1833 Nothing -> return ()
1834 Just docs -> addModDoc syntax mname docs
1837 -- Finally, write an ibc and highlights if checking was successful
1838 ok <- noErrors
1839 when ok $
1840 do idrisCatch (do writeIBC f ibc; clearIBC)
1841 (\c -> return ()) -- failure is harmless
1842 hl <- getDumpHighlighting
1843 when hl $
1844 idrisCatch (writeHighlights f)
1845 (const $ return ()) -- failure is harmless
1846 clearHighlights
1847 i <- getIState
1848 putIState (i { default_total = def_total,
1849 hide_list = emptyContext })
1850 return ()
1851 where
1852 namespaces :: [String] -> [PDecl] -> [PDecl]
1853 namespaces [] ds = ds
1854 namespaces (x:xs) ds = [PNamespace x NoFC (namespaces xs ds)]
1856 toMutual :: PDecl -> PDecl
1857 toMutual m@(PMutual _ d) = m
1858 toMutual (PNamespace x fc ds) = PNamespace x fc (map toMutual ds)
1859 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1860 case x of
1861 PClauses{} -> r
1862 PInterface{} -> r
1863 PData{} -> r
1864 PImplementation{} -> r
1865 _ -> x
1867 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1868 addModDoc syn mname docs =
1869 do ist <- getIState
1870 docs' <- elabDocTerms (toplevelWith f) (parsedDocs ist)
1871 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1872 putIState ist { idris_moduledocs = modDocs' }
1873 addIBC (IBCModDocs docName)
1874 where
1875 docName = NS modDocName (map T.pack (reverse mname))
1876 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1878{-| Adds names to hide list -}
1879addHides :: Ctxt Accessibility -> Idris ()
1880addHides xs = do i <- getIState
1881 let defh = default_access i
1882 mapM_ doHide (toAlist xs)
1883 where doHide (n, a) = do setAccessibility n a
1884 addIBC (IBCAccess n a)