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