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