git.iko.soy/Idris-dev
on 008fb1f help sign in
Idris-dev/src/Idris/Parser.hs
1894 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 "error_reduce");
692 return ErrorReduce
693 <|> do try (lchar '%' *> reserved "reflection");
694 return Reflection
695 <|> do try (lchar '%' *> reserved "hint");
696 return AutoHint
697 <|> do try (lchar '%' *> reserved "overlapping");
698 return OverlappingDictionary
699 <|> do lchar '%'; reserved "specialise";
700 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']';
701 return $ Specialise ns
702 <|> do reservedHL "implicit"; return Implicit
703 <?> "function modifier"
704 where nameTimes :: IdrisParser (Name, Maybe Int)
705 nameTimes = do n <- fst <$> fnName
706 t <- option Nothing (do reds <- fmap fst natural
707 return (Just (fromInteger reds)))
708 return (n, t)
710{-| Parses a postulate
713Postulate ::=
714 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
715 ;
717-}
718postulate :: SyntaxInfo -> IdrisParser PDecl
719postulate syn = do (doc, ext)
720 <- try $ do (doc, _) <- docstring syn
721 pushIndent
722 ext <- ppostDecl
723 return (doc, ext)
724 ist <- get
725 (opts, acc) <- fnOpts
726 (n_in, nfc) <- fnName
727 let n = expandNS syn n_in
728 lchar ':'
729 ty <- typeExpr (allowImp syn)
730 fc <- getFC
731 terminator
732 addAcc n acc
733 return (PPostulate ext doc syn fc nfc opts n ty)
734 <?> "postulate"
735 where ppostDecl = do fc <- reservedHL "postulate"; return False
736 <|> do lchar '%'; reserved "extern"; return True
738{-| Parses a using declaration
741Using ::=
742 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
743 ;
745 -}
746using_ :: SyntaxInfo -> IdrisParser [PDecl]
747using_ syn =
748 do reservedHL "using"
749 lchar '('; ns <- usingDeclList syn; lchar ')'
750 openBlock
751 let uvars = using syn
752 ds <- many (decl (syn { using = uvars ++ ns }))
753 closeBlock
754 return (concat ds)
755 <?> "using declaration"
757{-| Parses a parameters declaration
760Params ::=
761 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
762 ;
764-}
765params :: SyntaxInfo -> IdrisParser [PDecl]
766params syn =
767 do reservedHL "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
768 let ns' = [(n, ty) | (_, n, _, ty) <- ns]
769 openBlock
770 let pvars = syn_params syn
771 ds <- many (decl syn { syn_params = pvars ++ ns' })
772 closeBlock
773 fc <- getFC
774 return [PParams fc ns' (concat ds)]
775 <?> "parameters declaration"
777-- | Parses an open block
778openInterface :: SyntaxInfo -> IdrisParser [PDecl]
779openInterface syn =
780 do reservedHL "using"
781 reservedHL "implementation"
782 fc <- getFC
783 ns <- sepBy1 fnName (lchar ',')
785 openBlock
786 ds <- many (decl syn)
787 closeBlock
788 return [POpenInterfaces fc (map fst ns) (concat ds)]
789 <?> "open interface declaration"
795{-| Parses a mutual declaration (for mutually recursive functions)
798Mutual ::=
799 'mutual' OpenBlock Decl* CloseBlock
800 ;
802-}
803mutual :: SyntaxInfo -> IdrisParser [PDecl]
804mutual syn =
805 do reservedHL "mutual"
806 openBlock
807 let pvars = syn_params syn
808 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
809 closeBlock
810 fc <- getFC
811 return [PMutual fc (concat ds)]
812 <?> "mutual block"
814{-| Parses a namespace declaration
817Namespace ::=
818 'namespace' identifier OpenBlock Decl+ CloseBlock
819 ;
821-}
822namespace :: SyntaxInfo -> IdrisParser [PDecl]
823namespace syn =
824 do reservedHL "namespace"
825 (n, nfc) <- identifier
826 openBlock
827 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
828 closeBlock
829 return [PNamespace n nfc (concat ds)]
830 <?> "namespace declaration"
832{-| Parses a methods block (for implementations)
835 ImplementationBlock ::= 'where' OpenBlock FnDecl* CloseBlock
837-}
838implementationBlock :: SyntaxInfo -> IdrisParser [PDecl]
839implementationBlock syn = do reservedHL "where"
840 openBlock
841 ds <- many (fnDecl syn)
842 closeBlock
843 return (concat ds)
844 <?> "implementation block"
846{-| Parses a methods and implementations block (for interfaces)
849MethodOrImplementation ::=
850 FnDecl
851 | Implementation
852 ;
856InterfaceBlock ::=
857 'where' OpenBlock Constructor? MethodOrImplementation* CloseBlock
858 ;
860-}
861interfaceBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])
862interfaceBlock syn = do reservedHL "where"
863 openBlock
864 (cn, cd) <- option (Nothing, emptyDocstring) $
865 try (do (doc, _) <- option noDocs docComment
866 n <- constructor
867 return (Just n, doc))
868 ist <- get
869 let cd' = annotate syn ist cd
871 ds <- many (notEndBlock >> try (implementation True syn)
872 <|> do x <- data_ syn
873 return [x]
874 <|> fnDecl syn)
875 closeBlock
876 return (cn, cd', concat ds)
877 <?> "interface block"
878 where
879 constructor :: IdrisParser (Name, FC)
880 constructor = reservedHL "constructor" *> fnName
882 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)
883 annotate syn ist = annotCode $ tryFullExpr syn ist
885{-| Parses an interface declaration
888InterfaceArgument ::=
889 Name
890 | '(' Name ':' Expr ')'
891 ;
895Interface ::=
896 DocComment_t? Accessibility? 'interface' ConstraintList? Name InterfaceArgument* InterfaceBlock?
897 ;
899-}
900interface_ :: SyntaxInfo -> IdrisParser [PDecl]
901interface_ syn = do (doc, argDocs, acc)
902 <- try (do (doc, argDocs) <- docstring syn
903 acc <- accessibility
904 interfaceKeyword
905 return (doc, argDocs, acc))
906 fc <- getFC
907 cons <- constraintList syn
908 let cons' = [(c, ty) | (_, c, _, ty) <- cons]
909 (n_in, nfc) <- fnName
910 let n = expandNS syn n_in
911 cs <- many carg
912 fds <- option [(cn, NoFC) | (cn, _, _) <- cs] fundeps
913 (cn, cd, ds) <- option (Nothing, fst noDocs, []) (interfaceBlock syn)
914 accData acc n (concatMap declared ds)
915 return [PInterface doc syn fc cons' n nfc cs argDocs fds ds cn cd]
916 <?> "interface declaration"
917 where
918 fundeps :: IdrisParser [(Name, FC)]
919 fundeps = do lchar '|'; sepBy name (lchar ',')
921 interfaceKeyword :: IdrisParser ()
922 interfaceKeyword = reservedHL "interface"
923 <|> do reservedHL "class"
924 fc <- getFC
925 parserWarning fc Nothing (Msg "The 'class' keyword is deprecated. Use 'interface' instead.")
927 carg :: IdrisParser (Name, FC, PTerm)
928 carg = do lchar '('; (i, ifc) <- name; lchar ':'; ty <- expr syn; lchar ')'
929 return (i, ifc, ty)
930 <|> do (i, ifc) <- name
931 fc <- getFC
932 return (i, ifc, PType fc)
934{-| Parses an interface implementation declaration
937 Implementation ::=
938 DocComment_t? 'implementation' ImplementationName? ConstraintList? Name SimpleExpr* ImplementationBlock?
939 ;
943ImplementationName ::= '[' Name ']';
945-}
946implementation :: Bool -> SyntaxInfo -> IdrisParser [PDecl]
947implementation kwopt syn
948 = do ist <- get
949 (doc, argDocs) <- docstring syn
950 (opts, acc) <- fnOpts
951 if kwopt then optional implementationKeyword
952 else do implementationKeyword
953 return (Just ())
955 fc <- getFC
956 en <- optional implementationName
957 cs <- constraintList syn
958 let cs' = [(c, ty) | (_, c, _, ty) <- cs]
959 (cn, cnfc) <- fnName
960 args <- many (simpleExpr syn)
961 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)
962 let t = bindList (\r -> PPi constraint { pcount = r }) cs sc
963 pnames <- implementationUsing
964 ds <- implementationBlock syn
965 return [PImplementation doc argDocs syn fc cs' pnames acc opts cn cnfc args [] t en ds]
966 <?> "implementation declaration"
967 where implementationName :: IdrisParser Name
968 implementationName = do lchar '['; n_in <- fst <$> fnName; lchar ']'
969 let n = expandNS syn n_in
970 return n
971 <?> "implementation name"
972 implementationKeyword :: IdrisParser ()
973 implementationKeyword = reservedHL "implementation"
974 <|> do reservedHL "instance"
975 fc <- getFC
976 parserWarning fc Nothing (Msg "The 'instance' keyword is deprecated. Use 'implementation' (or omit it) instead.")
978 implementationUsing :: IdrisParser [Name]
979 implementationUsing = do reservedHL "using"
980 ns <- sepBy1 fnName (lchar ',')
981 return (map fst ns)
982 <|> return []
984-- | Parse a docstring
985docstring :: SyntaxInfo
986 -> IdrisParser (Docstring (Either Err PTerm),
987 [(Name,Docstring (Either Err PTerm))])
988docstring syn = do (doc, argDocs) <- option noDocs docComment
989 ist <- get
990 let doc' = annotCode (tryFullExpr syn ist) doc
991 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
992 | (n, d) <- argDocs ]
993 return (doc', argDocs')
996{-| Parses a using declaration list
999UsingDeclList ::=
1000 UsingDeclList'
1001 | NameList TypeSig
1006UsingDeclList' ::=
1007 UsingDecl
1008 | UsingDecl ',' UsingDeclList'
1013NameList ::=
1014 Name
1015 | Name ',' NameList
1019usingDeclList :: SyntaxInfo -> IdrisParser [Using]
1020usingDeclList syn
1021 = try (sepBy1 (usingDecl syn) (lchar ','))
1022 <|> do ns <- sepBy1 (fst <$> name) (lchar ',')
1023 lchar ':'
1024 t <- typeExpr (disallowImp syn)
1025 return (map (\x -> UImplicit x t) ns)
1026 <?> "using declaration list"
1028{-| Parses a using declaration
1031UsingDecl ::=
1032 FnName TypeSig
1033 | FnName FnName+
1037usingDecl :: SyntaxInfo -> IdrisParser Using
1038usingDecl syn = try (do x <- fst <$> fnName
1039 lchar ':'
1040 t <- typeExpr (disallowImp syn)
1041 return (UImplicit x t))
1042 <|> do c <- fst <$> fnName
1043 xs <- many (fst <$> fnName)
1044 return (UConstraint c xs)
1045 <?> "using declaration"
1047{-| Parse a clause with patterns
1050Pattern ::= Clause;
1053pattern :: SyntaxInfo -> IdrisParser PDecl
1054pattern syn = do fc <- getFC
1055 clause <- clause syn
1056 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
1057 <?> "pattern"
1059{-| Parse a constant applicative form declaration
1062CAF ::= 'let' FnName '=' Expr Terminator;
1065caf :: SyntaxInfo -> IdrisParser PDecl
1066caf syn = do reservedHL "let"
1067 n_in <- fst <$> fnName; let n = expandNS syn n_in
1068 pushIndent
1069 lchar '='
1070 t <- indented $ expr syn
1071 terminator
1072 fc <- getFC
1073 return (PCAF fc n t)
1074 <?> "constant applicative form declaration"
1076{-| Parse an argument expression
1079ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
1082argExpr :: SyntaxInfo -> IdrisParser PTerm
1083argExpr syn = let syn' = syn { inPattern = True } in
1084 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
1085 <?> "argument expression"
1087{-| Parse a right hand side of a function
1090RHS ::= '=' Expr
1091 | '?=' RHSName? Expr
1092 | Impossible
1097RHSName ::= '{' FnName '}';
1100rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
1101rhs syn n = do lchar '='
1102 indentPropHolds gtProp
1103 expr syn
1104 <|> do symbol "?=";
1105 fc <- getFC
1106 name <- option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";
1107 return n)
1108 r <- expr syn
1109 return (addLet fc name r)
1110 <|> impossible
1111 <?> "function right hand side"
1112 where mkN :: Name -> Name
1113 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
1114 then sUN "infix_op_lemma_1"
1115 else sUN (str x++"_lemma_1")
1116 mkN (NS x n) = NS (mkN x) n
1117 n' :: Name
1118 n' = mkN n
1119 addLet :: FC -> Name -> PTerm -> PTerm
1120 addLet fc nm (PLet fc' n nfc ty val r) = PLet fc' n nfc ty val (addLet fc nm r)
1121 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
1122 where addLetC (l, r) = (l, addLet fc nm r)
1123 addLet fc nm r = (PLet fc (sUN "value") NoFC Placeholder r (PMetavar NoFC nm))
1125{-|Parses a function clause
1128RHSOrWithBlock ::= RHS WhereOrTerminator
1129 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
1134Clause ::= WExpr+ RHSOrWithBlock
1135 | SimpleExpr '<==' FnName RHS WhereOrTerminator
1136 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
1137 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
1142ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
1146WhereOrTerminator ::= WhereBlock | Terminator;
1149clause :: SyntaxInfo -> IdrisParser PClause
1150clause syn
1151 = do wargs <- try (do pushIndent; some (wExpr syn))
1152 fc <- getFC
1153 ist <- get
1154 n <- case lastParse ist of
1155 Just t -> return t
1156 Nothing -> fail "Invalid clause"
1157 (do r <- rhs syn n
1158 let ctxt = tt_ctxt ist
1159 let wsyn = syn { syn_namespace = [], syn_toplevel = False }
1160 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1161 popIndent
1162 return x,
1163 do terminator
1164 return ([], [])]
1165 return $ PClauseR fc wargs r wheres) <|> (do
1166 popIndent
1167 reservedHL "with"
1168 wval <- simpleExpr syn
1169 pn <- optProof
1170 openBlock
1171 ds <- some $ fnDecl syn
1172 let withs = concat ds
1173 closeBlock
1174 return $ PWithR fc wargs wval pn withs)
1175 <|> do ty <- try (do pushIndent
1176 ty <- simpleExpr syn
1177 symbol "<=="
1178 return ty)
1179 fc <- getFC
1180 n_in <- fst <$> fnName; let n = expandNS syn n_in
1181 r <- rhs syn n
1182 ist <- get
1183 let ctxt = tt_ctxt ist
1184 let wsyn = syn { syn_namespace = [] }
1185 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1186 popIndent
1187 return x,
1188 do terminator
1189 return ([], [])]
1190 let capp = PLet fc (sMN 0 "match") NoFC
1191 ty
1192 (PMatchApp fc n)
1193 (PRef fc [] (sMN 0 "match"))
1194 ist <- get
1195 put (ist { lastParse = Just n })
1196 return $ PClause fc n capp [] r wheres
1197 <|> do (l, op, nfc) <- try (do
1198 pushIndent
1199 l <- argExpr syn
1200 (op, nfc) <- operatorFC
1201 when (op == "=" || op == "?=" ) $
1202 fail "infix clause definition with \"=\" and \"?=\" not supported "
1203 return (l, op, nfc))
1204 let n = expandNS syn (sUN op)
1205 r <- argExpr syn
1206 fc <- getFC
1207 wargs <- many (wExpr syn)
1208 (do rs <- rhs syn n
1209 let wsyn = syn { syn_namespace = [] }
1210 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1211 popIndent
1212 return x,
1213 do terminator
1214 return ([], [])]
1215 ist <- get
1216 let capp = PApp fc (PRef nfc [nfc] n) [pexp l, pexp r]
1217 put (ist { lastParse = Just n })
1218 return $ PClause fc n capp wargs rs wheres) <|> (do
1219 popIndent
1220 reservedHL "with"
1221 wval <- bracketed syn
1222 pn <- optProof
1223 openBlock
1224 ds <- some $ fnDecl syn
1225 closeBlock
1226 ist <- get
1227 let capp = PApp fc (PRef fc [] n) [pexp l, pexp r]
1228 let withs = map (fillLHSD n capp wargs) $ concat ds
1229 put (ist { lastParse = Just n })
1230 return $ PWith fc n capp wargs wval pn withs)
1231 <|> do pushIndent
1232 (n_in, nfc) <- fnName; let n = expandNS syn n_in
1233 fc <- getFC
1234 args <- many (try (implicitArg (syn { inPattern = True } ))
1235 <|> try (constraintArg (syn { inPattern = True }))
1236 <|> (fmap pexp (argExpr syn)))
1237 wargs <- many (wExpr syn)
1238 let capp = PApp fc (PRef nfc [nfc] n) args
1239 (do r <- rhs syn n
1240 ist <- get
1241 let ctxt = tt_ctxt ist
1242 let wsyn = syn { syn_namespace = [] }
1243 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1244 popIndent
1245 return x,
1246 do terminator
1247 return ([], [])]
1248 ist <- get
1249 put (ist { lastParse = Just n })
1250 return $ PClause fc n capp wargs r wheres) <|> (do
1251 reservedHL "with"
1252 ist <- get
1253 put (ist { lastParse = Just n })
1254 wval <- bracketed syn
1255 pn <- optProof
1256 openBlock
1257 ds <- some $ fnDecl syn
1258 let withs = map (fillLHSD n capp wargs) $ concat ds
1259 closeBlock
1260 popIndent
1261 return $ PWith fc n capp wargs wval pn withs)
1262 <?> "function clause"
1263 where
1264 optProof = option Nothing (do reservedHL "proof"
1265 n <- fnName
1266 return (Just n))
1268 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
1269 fillLHS n capp owargs (PClauseR fc wargs v ws)
1270 = PClause fc n capp (owargs ++ wargs) v ws
1271 fillLHS n capp owargs (PWithR fc wargs v pn ws)
1272 = PWith fc n capp (owargs ++ wargs) v pn
1273 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1274 fillLHS _ _ _ c = c
1276 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
1277 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1278 fillLHSD n c a x = x
1280{-| Parses with pattern
1283WExpr ::= '|' Expr';
1286wExpr :: SyntaxInfo -> IdrisParser PTerm
1287wExpr syn = do lchar '|'
1288 expr' (syn { inPattern = True })
1289 <?> "with pattern"
1291{-| Parses a where block
1294WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
1297whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
1298whereBlock n syn
1299 = do reservedHL "where"
1300 ds <- indentedBlock1 (decl syn)
1301 let dns = concatMap (concatMap declared) ds
1302 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1303 <?> "where block"
1305{-|Parses a code generation target language name
1308Codegen ::= 'C'
1309 | 'Java'
1310 | 'JavaScript'
1311 | 'Node'
1312 | 'LLVM'
1313 | 'Bytecode'
1317codegen_ :: IdrisParser Codegen
1318codegen_ = do n <- fst <$> identifier
1319 return (Via IBCFormat (map toLower n))
1320 <|> do reserved "Bytecode"; return Bytecode
1321 <?> "code generation language"
1323{-|Parses a compiler directive
1325StringList ::=
1326 String
1327 | String ',' StringList
1332Directive ::= '%' Directive';
1336Directive' ::= 'lib' CodeGen String_t
1337 | 'link' CodeGen String_t
1338 | 'flag' CodeGen String_t
1339 | 'include' CodeGen String_t
1340 | 'hide' Name
1341 | 'freeze' Name
1342 | 'thaw' Name
1343 | 'access' Accessibility
1344 | 'default' Totality
1345 | 'logging' Natural
1346 | 'dynamic' StringList
1347 | 'name' Name NameList
1348 | 'error_handlers' Name NameList
1349 | 'language' 'TypeProviders'
1350 | 'language' 'ErrorReflection'
1351 | 'deprecated' Name String
1352 | 'fragile' Name Reason
1356directive :: SyntaxInfo -> IdrisParser [PDecl]
1357directive syn = do try (lchar '%' *> reserved "lib")
1358 cgn <- codegen_
1359 lib <- fmap fst stringLiteral
1360 return [PDirective (DLib cgn lib)]
1361 <|> do try (lchar '%' *> reserved "link")
1362 cgn <- codegen_; obj <- fst <$> stringLiteral
1363 return [PDirective (DLink cgn obj)]
1364 <|> do try (lchar '%' *> reserved "flag")
1365 cgn <- codegen_; flag <- fst <$> stringLiteral
1366 return [PDirective (DFlag cgn flag)]
1367 <|> do try (lchar '%' *> reserved "include")
1368 cgn <- codegen_
1369 hdr <- fst <$> stringLiteral
1370 return [PDirective (DInclude cgn hdr)]
1371 <|> do try (lchar '%' *> reserved "hide"); n <- fst <$> fnName
1372 return [PDirective (DHide n)]
1373 <|> do try (lchar '%' *> reserved "freeze"); n <- fst <$> iName []
1374 return [PDirective (DFreeze n)]
1375 <|> do try (lchar '%' *> reserved "thaw"); n <- fst <$> iName []
1376 return [PDirective (DThaw n)]
1377 -- injectivity assertins are intended for debugging purposes
1378 -- only, and won't be documented/could be removed at any point
1379 <|> do try (lchar '%' *> reserved "assert_injective"); n <- fst <$> fnName
1380 return [PDirective (DInjective n)]
1381 -- Assert totality of something after definition. This is
1382 -- here as a debugging aid, so commented out...
1383-- <|> do try (lchar '%' *> reserved "assert_set_total"); n <- fst <$> fnName
1384-- return [PDirective (DSetTotal n)]
1385 <|> do try (lchar '%' *> reserved "access")
1386 acc <- accessibility
1387 ist <- get
1388 put ist { default_access = acc }
1389 return [PDirective (DAccess acc)]
1390 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1391 i <- get
1392 put (i { default_total = tot } )
1393 return [PDirective (DDefault tot)]
1394 <|> do try (lchar '%' *> reserved "logging")
1395 i <- fst <$> natural
1396 return [PDirective (DLogging i)]
1397 <|> do try (lchar '%' *> reserved "dynamic")
1398 libs <- sepBy1 (fmap fst stringLiteral) (lchar ',')
1399 return [PDirective (DDynamicLibs libs)]
1400 <|> do try (lchar '%' *> reserved "name")
1401 (ty, tyFC) <- fnName
1402 ns <- sepBy1 name (lchar ',')
1403 return [PDirective (DNameHint ty tyFC ns)]
1404 <|> do try (lchar '%' *> reserved "error_handlers")
1405 (fn, nfc) <- fnName
1406 (arg, afc) <- fnName
1407 ns <- sepBy1 name (lchar ',')
1408 return [PDirective (DErrorHandlers fn nfc arg afc ns) ]
1409 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1410 return [PDirective (DLanguage ext)]
1411 <|> do try (lchar '%' *> reserved "deprecate")
1412 n <- fst <$> fnName
1413 alt <- option "" (fst <$> stringLiteral)
1414 return [PDirective (DDeprecate n alt)]
1415 <|> do try (lchar '%' *> reserved "fragile")
1416 n <- fst <$> fnName
1417 alt <- option "" (fst <$> stringLiteral)
1418 return [PDirective (DFragile n alt)]
1419 <|> do fc <- getFC
1420 try (lchar '%' *> reserved "used")
1421 fn <- fst <$> fnName
1422 arg <- fst <$> iName []
1423 return [PDirective (DUsed fc fn arg)]
1424 <|> do try (lchar '%' *> reserved "auto_implicits")
1425 b <- on_off
1426 return [PDirective (DAutoImplicits b)]
1427 <?> "directive"
1428 where on_off = do reserved "on"; return True
1429 <|> do reserved "off"; return False
1431pLangExt :: IdrisParser LanguageExt
1432pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1433 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1434 <|> (reserved "UniquenessTypes" >> return UniquenessTypes)
1435 <|> (reserved "LinearTypes" >> return LinearTypes)
1436 <|> (reserved "DSLNotation" >> return DSLNotation)
1437 <|> (reserved "ElabReflection" >> return ElabReflection)
1438 <|> (reserved "FirstClassReflection" >> return FCReflection)
1440{-| Parses a totality
1443Totality ::= 'partial' | 'total' | 'covering'
1447totality :: IdrisParser DefaultTotality
1448totality
1449 = do reservedHL "total"; return DefaultCheckingTotal
1450 <|> do reservedHL "partial"; return DefaultCheckingPartial
1451 <|> do reservedHL "covering"; return DefaultCheckingCovering
1453{-| Parses a type provider
1456Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1457ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1459 -}
1460provider :: SyntaxInfo -> IdrisParser [PDecl]
1461provider syn = do doc <- try (do (doc, _) <- docstring syn
1462 fc1 <- getFC
1463 lchar '%'
1464 fc2 <- reservedFC "provide"
1465 highlightP (spanFC fc1 fc2) AnnKeyword
1466 return doc)
1467 provideTerm doc <|> providePostulate doc
1468 <?> "type provider"
1469 where provideTerm doc =
1470 do lchar '('; (n, nfc) <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1471 fc <- getFC
1472 reservedHL "with"
1473 e <- expr syn <?> "provider expression"
1474 return [PProvider doc syn fc nfc (ProvTerm t e) n]
1475 providePostulate doc =
1476 do reservedHL "postulate"
1477 (n, nfc) <- fnName
1478 fc <- getFC
1479 reservedHL "with"
1480 e <- expr syn <?> "provider expression"
1481 return [PProvider doc syn fc nfc (ProvPostulate e) n]
1483{-| Parses a transform
1486Transform ::= '%' 'transform' Expr '==>' Expr
1489transform :: SyntaxInfo -> IdrisParser [PDecl]
1490transform syn = do try (lchar '%' *> reserved "transform")
1491 -- leave it unchecked, until we work out what this should
1492 -- actually mean...
1493-- safety <- option True (do reserved "unsafe"
1494-- return False)
1495 l <- expr syn
1496 fc <- getFC
1497 symbol "==>"
1498 r <- expr syn
1499 return [PTransform fc False l r]
1500 <?> "transform"
1502{-| Parses a top-level reflected elaborator script
1505RunElabDecl ::= '%' 'runElab' Expr
1508runElabDecl :: SyntaxInfo -> IdrisParser PDecl
1509runElabDecl syn =
1510 do kwFC <- try (do fc <- getFC
1511 lchar '%'
1512 fc' <- reservedFC "runElab"
1513 return (spanFC fc fc'))
1514 script <- expr syn <?> "elaborator script"
1515 highlightP kwFC AnnKeyword
1516 return $ PRunElabDecl kwFC script (syn_namespace syn)
1517 <?> "top-level elaborator script"
1519{- * Loading and parsing -}
1520{-| Parses an expression from input -}
1521parseExpr :: IState -> String -> Result PTerm
1522parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1524{-| Parses a constant form input -}
1525parseConst :: IState -> String -> Result Const
1526parseConst st = runparser (fmap fst constant) st "(input)"
1528{-| Parses a tactic from input -}
1529parseTactic :: IState -> String -> Result PTactic
1530parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1532{-| Parses a do-step from input (used in the elab shell) -}
1533parseElabShellStep :: IState -> String -> Result (Either ElabShellCmd PDo)
1534parseElabShellStep ist = runparser (fmap Right (do_ defaultSyntax) <|> fmap Left elabShellCmd) ist "(input)"
1535 where elabShellCmd = char ':' >>
1536 (reserved "qed" >> pure EQED ) <|>
1537 (reserved "abandon" >> pure EAbandon ) <|>
1538 (reserved "undo" >> pure EUndo ) <|>
1539 (reserved "state" >> pure EProofState) <|>
1540 (reserved "term" >> pure EProofTerm ) <|>
1541 (expressionTactic ["e", "eval"] EEval ) <|>
1542 (expressionTactic ["t", "type"] ECheck) <|>
1543 (expressionTactic ["search"] ESearch ) <|>
1544 (do reserved "doc"
1545 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)
1546 eof
1547 return (EDocStr doc))
1548 <?> "elab command"
1549 expressionTactic cmds tactic =
1550 do asum (map reserved cmds)
1551 t <- spaced (expr defaultSyntax)
1552 i <- get
1553 return $ tactic (desugar defaultSyntax i t)
1554 spaced parser = indentPropHolds gtProp *> parser
1556-- | Parse module header and imports
1557parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Delta)
1558parseImports fname input
1559 = do i <- getIState
1560 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1561 Failure (ErrInfo err _) -> fail (show err)
1562 Success (x, annots, i) ->
1563 do putIState i
1564 fname' <- runIO $ Dir.makeAbsolute fname
1565 sendHighlighting $ addPath annots fname'
1566 return x
1567 where imports :: IdrisParser ((Maybe (Docstring ()), [String],
1568 [ImportInfo],
1569 Maybe Delta),
1570 [(FC, OutputAnnotation)], IState)
1571 imports = do whiteSpace
1572 (mdoc, mname, annots) <- moduleHeader
1573 ps_exp <- many import_
1574 mrk <- mark
1575 isEof <- lookAheadMatches eof
1576 let mrk' = if isEof
1577 then Nothing
1578 else Just mrk
1579 i <- get
1580 -- add Builtins and Prelude, unless options say
1581 -- not to
1582 let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp
1583 return ((mdoc, mname, ps, mrk'), annots, i)
1585 imp m = ImportInfo False (toPath m)
1586 Nothing [] NoFC NoFC
1587 ns = Spl.splitOn "."
1588 toPath = foldl1' (</>) . ns
1590 addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]
1591 addPath [] _ = []
1592 addPath ((fc, AnnNamespace ns Nothing) : annots) path =
1593 (fc, AnnNamespace ns (Just path)) : addPath annots path
1594 addPath (annot:annots) path = annot : addPath annots path
1596-- | There should be a better way of doing this...
1597findFC :: Doc -> (FC, String)
1598findFC x = let s = show (plain x) in findFC' s
1599 where findFC' s = case span (/= ':') s of
1600 -- Horrid kludge to prevent crashes on Windows
1601 (prefix, ':':'\\':rest) ->
1602 case findFC' rest of
1603 (NoFC, msg) -> (NoFC, msg)
1604 (FileFC f, msg) -> (FileFC (prefix ++ ":\\" ++ f), msg)
1605 (FC f start end, msg) -> (FC (prefix ++ ":\\" ++ f) start end, msg)
1606 (failname, ':':rest) -> case span isDigit rest of
1607 (line, ':':rest') -> case span isDigit rest' of
1608 (col, ':':msg) -> let pos = (read line, read col) in
1609 (FC failname pos pos, msg)
1611-- | Check if the coloring matches the options and corrects if necessary
1612fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1613fixColour False doc = ANSI.plain doc
1614fixColour True doc = doc
1616-- | A program is a list of declarations, possibly with associated
1617-- documentation strings.
1618parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1619 Idris [PDecl]
1620parseProg syn fname input mrk
1621 = do i <- getIState
1622 case runparser mainProg i fname input of
1623 Failure (ErrInfo doc _) -> do -- FIXME: Get error location from trifecta
1624 -- this can't be the solution!
1625 -- Issue #1575 on the issue tracker.
1626 -- https://github.com/idris-lang/Idris-dev/issues/1575
1627 let (fc, msg) = findFC doc
1628 i <- getIState
1629 case idris_outputmode i of
1630 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1631 IdeMode n h -> iWarn fc (P.text msg)
1632 putIState (i { errSpan = Just fc })
1633 return []
1634 Success (x, i) -> do putIState i
1635 reportParserWarnings
1636 return $ collect x
1637 where mainProg :: IdrisParser ([PDecl], IState)
1638 mainProg = case mrk of
1639 Nothing -> do i <- get; return ([], i)
1640 Just mrk -> do
1641 release mrk
1642 ds <- prog syn
1643 i' <- get
1644 return (ds, i')
1646{-| Load idris module and show error if something wrong happens -}
1647loadModule :: FilePath -> IBCPhase -> Idris (Maybe String)
1648loadModule f phase
1649 = idrisCatch (loadModule' f phase)
1650 (\e -> do setErrSpan (getErrSpan e)
1651 ist <- getIState
1652 iWarn (getErrSpan e) $ pprintErr ist e
1653 return Nothing)
1655{-| Load idris module -}
1656loadModule' :: FilePath -> IBCPhase -> Idris (Maybe String)
1657loadModule' f phase
1658 = do i <- getIState
1659 let file = takeWhile (/= ' ') f
1660 ibcsd <- valIBCSubDir i
1661 ids <- allImportDirs
1662 fp <- findImport ids ibcsd file
1663 if file `elem` imported i
1664 then do logParser 1 $ "Already read " ++ file
1665 return Nothing
1666 else do putIState (i { imported = file : imported i })
1667 case fp of
1668 IDR fn -> loadSource False fn Nothing
1669 LIDR fn -> loadSource True fn Nothing
1670 IBC fn src ->
1671 idrisCatch (loadIBC True phase fn)
1672 (\c -> do logParser 1 $ fn ++ " failed " ++ pshow i c
1673 case src of
1674 IDR sfn -> loadSource False sfn Nothing
1675 LIDR sfn -> loadSource True sfn Nothing)
1676 return $ Just file
1678{-| Load idris code from file -}
1679loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()
1680loadFromIFile reexp phase i@(IBC fn src) maxline
1681 = do logParser 1 $ "Skipping " ++ getSrcFile i
1682 idrisCatch (loadIBC reexp phase fn)
1683 (\err -> ierror $ LoadingFailed fn err)
1684 where
1685 getSrcFile (IDR fn) = fn
1686 getSrcFile (LIDR fn) = fn
1687 getSrcFile (IBC f src) = getSrcFile src
1689loadFromIFile _ _ (IDR fn) maxline = loadSource' False fn maxline
1690loadFromIFile _ _ (LIDR fn) maxline = loadSource' True fn maxline
1692{-| Load idris source code and show error if something wrong happens -}
1693loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1694loadSource' lidr r maxline
1695 = idrisCatch (loadSource lidr r maxline)
1696 (\e -> do setErrSpan (getErrSpan e)
1697 ist <- getIState
1698 case e of
1699 At f e' -> iWarn f (pprintErr ist e')
1700 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1702{-| Load Idris source code-}
1703loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1704loadSource lidr f toline
1705 = do logParser 1 ("Reading " ++ f)
1706 iReport 2 ("Reading " ++ f)
1707 i <- getIState
1708 let def_total = default_total i
1709 file_in <- runIO $ readSource f
1710 file <- if lidr then tclift $ unlit f file_in else return file_in
1711 (mdocs, mname, imports_in, pos) <- parseImports f file
1712 ai <- getAutoImports
1713 let imports = map (\n -> ImportInfo True n Nothing [] NoFC NoFC) ai ++ imports_in
1714 ids <- allImportDirs
1715 ibcsd <- valIBCSubDir i
1716 mapM_ (\(re, f, ns, nfc) ->
1717 do fp <- findImport ids ibcsd f
1718 case fp of
1719 LIDR fn -> ifail $ "No ibc for " ++ f
1720 IDR fn -> ifail $ "No ibc for " ++ f
1721 IBC fn src ->
1722 do loadIBC True IBC_Building fn
1723 let srcFn = case src of
1724 IDR fn -> Just fn
1725 LIDR fn -> Just fn
1726 _ -> Nothing
1727 srcFnAbs <- case srcFn of
1728 Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)
1729 Nothing -> return Nothing
1730 sendHighlighting [(nfc, AnnNamespace ns srcFnAbs)])
1731 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]
1732 reportParserWarnings
1733 sendParserHighlighting
1735 -- process and check module aliases
1736 let modAliases = M.fromList
1737 [ (prep alias, prep realName)
1738 | ImportInfo { import_reexport = reexport
1739 , import_path = realName
1740 , import_rename = Just (alias, _)
1741 , import_location = fc } <- imports
1743 prep = map T.pack . reverse . Spl.splitOn [pathSeparator]
1744 aliasNames = [ (alias, fc)
1745 | ImportInfo { import_rename = Just (alias, _)
1746 , import_location = fc } <- imports
1748 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1749 case map head . filter ((/= 1) . length) $ histogram of
1750 [] -> logParser 3 $ "Module aliases: " ++ show (M.toList modAliases)
1751 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1753 i <- getIState
1754 putIState (i { default_access = Private, module_aliases = modAliases })
1755 clearIBC -- start a new .ibc file
1756 -- record package info in .ibc
1757 imps <- allImportDirs
1758 mapM_ addIBC (map IBCImportDir imps)
1759 mapM_ (addIBC . IBCImport)
1760 [ (reexport, realName)
1761 | ImportInfo { import_reexport = reexport
1762 , import_path = realName
1763 } <- imports
1765 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1766 maxline = toline }
1767 ist <- getIState
1768 -- Save the span from parsing the module header, because
1769 -- an empty program parse might obliterate it.
1770 let oldSpan = idris_parsedSpan ist
1771 ds' <- parseProg syntax f file pos
1773 case (ds', oldSpan) of
1774 ([], Just fc) ->
1775 -- If no program elements were parsed, we dind't
1776 -- get a loaded region in the IBC file. That
1777 -- means we need to add it back.
1778 do ist <- getIState
1779 putIState ist { idris_parsedSpan = oldSpan
1780 , ibc_write = IBCParsedRegion fc :
1781 ibc_write ist
1783 _ -> return ()
1784 sendParserHighlighting
1786 -- Parsing done, now process declarations
1788 let ds = namespaces mname ds'
1789 logParser 3 (show $ showDecls verbosePPOption ds)
1790 i <- getIState
1791 logLvl 10 (show (toAlist (idris_implicits i)))
1792 logLvl 3 (show (idris_infixes i))
1793 -- Now add all the declarations to the context
1794 iReport 1 $ "Type checking " ++ f
1795 -- we totality check after every Mutual block, so if
1796 -- anything is a single definition, wrap it in a
1797 -- mutual block on its own
1798 elabDecls (toplevelWith f) (map toMutual ds)
1799 i <- getIState
1800 -- simplify every definition do give the totality checker
1801 -- a better chance
1802 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1803 ctxt' <-
1804 do ctxt <- getContext
1805 tclift $ simplifyCasedef n [] [] (getErasureInfo i) ctxt
1806 setContext ctxt')
1807 (map snd (idris_totcheck i))
1808 -- build size change graph from simplified definitions
1809 iReport 3 $ "Totality checking " ++ f
1810 logLvl 1 $ "Totality checking " ++ f
1811 i <- getIState
1812 mapM_ buildSCG (idris_totcheck i)
1813 mapM_ checkDeclTotality (idris_totcheck i)
1814 mapM_ verifyTotality (idris_totcheck i)
1816 -- Redo totality check for deferred names
1817 let deftots = idris_defertotcheck i
1818 logLvl 2 $ "Totality checking " ++ show deftots
1819 mapM_ (\x -> do tot <- getTotality x
1820 case tot of
1821 Total _ ->
1822 do let opts = case lookupCtxtExact x (idris_flags i) of
1823 Just os -> os
1824 Nothing -> []
1825 when (AssertTotal `notElem` opts) $
1826 setTotality x Unchecked
1827 _ -> return ()) (map snd deftots)
1828 mapM_ buildSCG deftots
1829 mapM_ checkDeclTotality deftots
1831 logLvl 1 ("Finished " ++ f)
1832 ibcsd <- valIBCSubDir i
1833 logLvl 1 $ "Universe checking " ++ f
1834 iReport 3 $ "Universe checking " ++ f
1835 iucheck
1836 let ibc = ibcPathNoFallback ibcsd f
1837 i <- getIState
1838 addHides (hide_list i)
1840 -- Save module documentation if applicable
1841 i <- getIState
1842 case mdocs of
1843 Nothing -> return ()
1844 Just docs -> addModDoc syntax mname docs
1847 -- Finally, write an ibc and highlights if checking was successful
1848 ok <- noErrors
1849 when ok $
1850 do idrisCatch (do writeIBC f ibc; clearIBC)
1851 (\c -> return ()) -- failure is harmless
1852 hl <- getDumpHighlighting
1853 when hl $
1854 idrisCatch (writeHighlights f)
1855 (const $ return ()) -- failure is harmless
1856 clearHighlights
1857 i <- getIState
1858 putIState (i { default_total = def_total,
1859 hide_list = emptyContext })
1860 return ()
1861 where
1862 namespaces :: [String] -> [PDecl] -> [PDecl]
1863 namespaces [] ds = ds
1864 namespaces (x:xs) ds = [PNamespace x NoFC (namespaces xs ds)]
1866 toMutual :: PDecl -> PDecl
1867 toMutual m@(PMutual _ d) = m
1868 toMutual (PNamespace x fc ds) = PNamespace x fc (map toMutual ds)
1869 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1870 case x of
1871 PClauses{} -> r
1872 PInterface{} -> r
1873 PData{} -> r
1874 PImplementation{} -> r
1875 _ -> x
1877 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1878 addModDoc syn mname docs =
1879 do ist <- getIState
1880 docs' <- elabDocTerms (toplevelWith f) (parsedDocs ist)
1881 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1882 putIState ist { idris_moduledocs = modDocs' }
1883 addIBC (IBCModDocs docName)
1884 where
1885 docName = NS modDocName (map T.pack (reverse mname))
1886 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1888{-| Adds names to hide list -}
1889addHides :: Ctxt Accessibility -> Idris ()
1890addHides xs = do i <- getIState
1891 let defh = default_access i
1892 mapM_ doHide (toAlist xs)
1893 where doHide (n, a) = do setAccessibility n a
1894 addIBC (IBCAccess n a)