git.iko.soy/Idris-dev
on eac558e help sign in
Idris-dev/src/Idris/Parser.hs
1905 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 '='
1120 indentPropHolds gtProp
1121 expr syn
1122 <|> do symbol "?=";
1123 fc <- getFC
1124 name <- option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";
1125 return n)
1126 r <- expr syn
1127 return (addLet fc name r)
1128 <|> impossible
1129 <?> "function right hand side"
1130 where mkN :: Name -> Name
1131 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
1132 then sUN "infix_op_lemma_1"
1133 else sUN (str x++"_lemma_1")
1134 mkN (NS x n) = NS (mkN x) n
1135 n' :: Name
1136 n' = mkN n
1137 addLet :: FC -> Name -> PTerm -> PTerm
1138 addLet fc nm (PLet fc' n nfc ty val r) = PLet fc' n nfc ty val (addLet fc nm r)
1139 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
1140 where addLetC (l, r) = (l, addLet fc nm r)
1141 addLet fc nm r = (PLet fc (sUN "value") NoFC Placeholder r (PMetavar NoFC nm))
1143{-|Parses a function clause
1146RHSOrWithBlock ::= RHS WhereOrTerminator
1147 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
1152Clause ::= WExpr+ RHSOrWithBlock
1153 | SimpleExpr '<==' FnName RHS WhereOrTerminator
1154 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
1155 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
1160ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
1164WhereOrTerminator ::= WhereBlock | Terminator;
1167clause :: SyntaxInfo -> IdrisParser PClause
1168clause syn
1169 = do wargs <- try (do pushIndent; some (wExpr syn))
1170 fc <- getFC
1171 ist <- get
1172 n <- case lastParse ist of
1173 Just t -> return t
1174 Nothing -> fail "Invalid clause"
1175 (do r <- rhs syn n
1176 let ctxt = tt_ctxt ist
1177 let wsyn = syn { syn_namespace = [], syn_toplevel = False }
1178 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1179 popIndent
1180 return x,
1181 do terminator
1182 return ([], [])]
1183 return $ PClauseR fc wargs r wheres) <|> (do
1184 popIndent
1185 reservedHL "with"
1186 wval <- simpleExpr syn
1187 pn <- optProof
1188 openBlock
1189 ds <- some $ fnDecl syn
1190 let withs = concat ds
1191 closeBlock
1192 return $ PWithR fc wargs wval pn withs)
1193 <|> do ty <- try (do pushIndent
1194 ty <- simpleExpr syn
1195 symbol "<=="
1196 return ty)
1197 fc <- getFC
1198 n_in <- fst <$> fnName; let n = expandNS syn n_in
1199 r <- rhs syn n
1200 ist <- get
1201 let ctxt = tt_ctxt ist
1202 let wsyn = syn { syn_namespace = [] }
1203 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1204 popIndent
1205 return x,
1206 do terminator
1207 return ([], [])]
1208 let capp = PLet fc (sMN 0 "match") NoFC
1209 ty
1210 (PMatchApp fc n)
1211 (PRef fc [] (sMN 0 "match"))
1212 ist <- get
1213 put (ist { lastParse = Just n })
1214 return $ PClause fc n capp [] r wheres
1215 <|> do (l, op, nfc) <- try (do
1216 pushIndent
1217 l <- argExpr syn
1218 (op, nfc) <- operatorFC
1219 when (op == "=" || op == "?=" ) $
1220 fail "infix clause definition with \"=\" and \"?=\" not supported "
1221 return (l, op, nfc))
1222 let n = expandNS syn (sUN op)
1223 r <- argExpr syn
1224 fc <- getFC
1225 wargs <- many (wExpr syn)
1226 (do rs <- rhs syn n
1227 let wsyn = syn { syn_namespace = [] }
1228 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1229 popIndent
1230 return x,
1231 do terminator
1232 return ([], [])]
1233 ist <- get
1234 let capp = PApp fc (PRef nfc [nfc] n) [pexp l, pexp r]
1235 put (ist { lastParse = Just n })
1236 return $ PClause fc n capp wargs rs wheres) <|> (do
1237 popIndent
1238 reservedHL "with"
1239 wval <- bracketed syn
1240 pn <- optProof
1241 openBlock
1242 ds <- some $ fnDecl syn
1243 closeBlock
1244 ist <- get
1245 let capp = PApp fc (PRef fc [] n) [pexp l, pexp r]
1246 let withs = map (fillLHSD n capp wargs) $ concat ds
1247 put (ist { lastParse = Just n })
1248 return $ PWith fc n capp wargs wval pn withs)
1249 <|> do pushIndent
1250 (n_in, nfc) <- fnName; let n = expandNS syn n_in
1251 fc <- getFC
1252 args <- many (try (implicitArg (syn { inPattern = True } ))
1253 <|> try (constraintArg (syn { inPattern = True }))
1254 <|> (fmap pexp (argExpr syn)))
1255 wargs <- many (wExpr syn)
1256 let capp = PApp fc (PRef nfc [nfc] n) args
1257 (do r <- rhs syn n
1258 ist <- get
1259 let ctxt = tt_ctxt ist
1260 let wsyn = syn { syn_namespace = [] }
1261 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1262 popIndent
1263 return x,
1264 do terminator
1265 return ([], [])]
1266 ist <- get
1267 put (ist { lastParse = Just n })
1268 return $ PClause fc n capp wargs r wheres) <|> (do
1269 reservedHL "with"
1270 ist <- get
1271 put (ist { lastParse = Just n })
1272 wval <- bracketed syn
1273 pn <- optProof
1274 openBlock
1275 ds <- some $ fnDecl syn
1276 let withs = map (fillLHSD n capp wargs) $ concat ds
1277 closeBlock
1278 popIndent
1279 return $ PWith fc n capp wargs wval pn withs)
1280 <?> "function clause"
1281 where
1282 optProof = option Nothing (do reservedHL "proof"
1283 n <- fnName
1284 return (Just n))
1286 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
1287 fillLHS n capp owargs (PClauseR fc wargs v ws)
1288 = PClause fc n capp (owargs ++ wargs) v ws
1289 fillLHS n capp owargs (PWithR fc wargs v pn ws)
1290 = PWith fc n capp (owargs ++ wargs) v pn
1291 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1292 fillLHS _ _ _ c = c
1294 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
1295 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1296 fillLHSD n c a x = x
1298{-| Parses with pattern
1301WExpr ::= '|' Expr';
1304wExpr :: SyntaxInfo -> IdrisParser PTerm
1305wExpr syn = do lchar '|'
1306 expr' (syn { inPattern = True })
1307 <?> "with pattern"
1309{-| Parses a where block
1312WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
1315whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
1316whereBlock n syn
1317 = do reservedHL "where"
1318 ds <- indentedBlock1 (decl syn)
1319 let dns = concatMap (concatMap declared) ds
1320 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1321 <?> "where block"
1323{-|Parses a code generation target language name
1326Codegen ::= 'C'
1327 | 'Java'
1328 | 'JavaScript'
1329 | 'Node'
1330 | 'LLVM'
1331 | 'Bytecode'
1335codegen_ :: IdrisParser Codegen
1336codegen_ = do n <- fst <$> identifier
1337 return (Via IBCFormat (map toLower n))
1338 <|> do reserved "Bytecode"; return Bytecode
1339 <?> "code generation language"
1341{-|Parses a compiler directive
1343StringList ::=
1344 String
1345 | String ',' StringList
1350Directive ::= '%' Directive';
1354Directive' ::= 'lib' CodeGen String_t
1355 | 'link' CodeGen String_t
1356 | 'flag' CodeGen String_t
1357 | 'include' CodeGen String_t
1358 | 'hide' Name
1359 | 'freeze' Name
1360 | 'thaw' Name
1361 | 'access' Accessibility
1362 | 'default' Totality
1363 | 'logging' Natural
1364 | 'dynamic' StringList
1365 | 'name' Name NameList
1366 | 'error_handlers' Name NameList
1367 | 'language' 'TypeProviders'
1368 | 'language' 'ErrorReflection'
1369 | 'deprecated' Name String
1370 | 'fragile' Name Reason
1374directive :: SyntaxInfo -> IdrisParser [PDecl]
1375directive syn = do try (lchar '%' *> reserved "lib")
1376 cgn <- codegen_
1377 lib <- fmap fst stringLiteral
1378 return [PDirective (DLib cgn lib)]
1379 <|> do try (lchar '%' *> reserved "link")
1380 cgn <- codegen_; obj <- fst <$> stringLiteral
1381 return [PDirective (DLink cgn obj)]
1382 <|> do try (lchar '%' *> reserved "flag")
1383 cgn <- codegen_; flag <- fst <$> stringLiteral
1384 return [PDirective (DFlag cgn flag)]
1385 <|> do try (lchar '%' *> reserved "include")
1386 cgn <- codegen_
1387 hdr <- fst <$> stringLiteral
1388 return [PDirective (DInclude cgn hdr)]
1389 <|> do try (lchar '%' *> reserved "hide"); n <- fst <$> fnName
1390 return [PDirective (DHide n)]
1391 <|> do try (lchar '%' *> reserved "freeze"); n <- fst <$> iName []
1392 return [PDirective (DFreeze n)]
1393 <|> do try (lchar '%' *> reserved "thaw"); n <- fst <$> iName []
1394 return [PDirective (DThaw n)]
1395 -- injectivity assertins are intended for debugging purposes
1396 -- only, and won't be documented/could be removed at any point
1397 <|> do try (lchar '%' *> reserved "assert_injective"); n <- fst <$> fnName
1398 return [PDirective (DInjective n)]
1399 -- Assert totality of something after definition. This is
1400 -- here as a debugging aid, so commented out...
1401-- <|> do try (lchar '%' *> reserved "assert_set_total"); n <- fst <$> fnName
1402-- return [PDirective (DSetTotal n)]
1403 <|> do try (lchar '%' *> reserved "access")
1404 acc <- accessibility
1405 ist <- get
1406 put ist { default_access = acc }
1407 return [PDirective (DAccess acc)]
1408 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1409 i <- get
1410 put (i { default_total = tot } )
1411 return [PDirective (DDefault tot)]
1412 <|> do try (lchar '%' *> reserved "logging")
1413 i <- fst <$> natural
1414 return [PDirective (DLogging i)]
1415 <|> do try (lchar '%' *> reserved "dynamic")
1416 libs <- sepBy1 (fmap fst stringLiteral) (lchar ',')
1417 return [PDirective (DDynamicLibs libs)]
1418 <|> do try (lchar '%' *> reserved "name")
1419 (ty, tyFC) <- fnName
1420 ns <- sepBy1 name (lchar ',')
1421 return [PDirective (DNameHint ty tyFC ns)]
1422 <|> do try (lchar '%' *> reserved "error_handlers")
1423 (fn, nfc) <- fnName
1424 (arg, afc) <- fnName
1425 ns <- sepBy1 name (lchar ',')
1426 return [PDirective (DErrorHandlers fn nfc arg afc ns) ]
1427 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1428 return [PDirective (DLanguage ext)]
1429 <|> do try (lchar '%' *> reserved "deprecate")
1430 n <- fst <$> fnName
1431 alt <- option "" (fst <$> stringLiteral)
1432 return [PDirective (DDeprecate n alt)]
1433 <|> do try (lchar '%' *> reserved "fragile")
1434 n <- fst <$> fnName
1435 alt <- option "" (fst <$> stringLiteral)
1436 return [PDirective (DFragile n alt)]
1437 <|> do fc <- getFC
1438 try (lchar '%' *> reserved "used")
1439 fn <- fst <$> fnName
1440 arg <- fst <$> iName []
1441 return [PDirective (DUsed fc fn arg)]
1442 <|> do try (lchar '%' *> reserved "auto_implicits")
1443 b <- on_off
1444 return [PDirective (DAutoImplicits b)]
1445 <?> "directive"
1446 where on_off = do reserved "on"; return True
1447 <|> do reserved "off"; return False
1449pLangExt :: IdrisParser LanguageExt
1450pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1451 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1453{-| Parses a totality
1456Totality ::= 'partial' | 'total' | 'covering'
1460totality :: IdrisParser DefaultTotality
1461totality
1462 = do reservedHL "total"; return DefaultCheckingTotal
1463 <|> do reservedHL "partial"; return DefaultCheckingPartial
1464 <|> do reservedHL "covering"; return DefaultCheckingCovering
1466{-| Parses a type provider
1469Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1470ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1472 -}
1473provider :: SyntaxInfo -> IdrisParser [PDecl]
1474provider syn = do doc <- try (do (doc, _) <- docstring syn
1475 fc1 <- getFC
1476 lchar '%'
1477 fc2 <- reservedFC "provide"
1478 highlightP (spanFC fc1 fc2) AnnKeyword
1479 return doc)
1480 provideTerm doc <|> providePostulate doc
1481 <?> "type provider"
1482 where provideTerm doc =
1483 do lchar '('; (n, nfc) <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1484 fc <- getFC
1485 reservedHL "with"
1486 e <- expr syn <?> "provider expression"
1487 return [PProvider doc syn fc nfc (ProvTerm t e) n]
1488 providePostulate doc =
1489 do reservedHL "postulate"
1490 (n, nfc) <- fnName
1491 fc <- getFC
1492 reservedHL "with"
1493 e <- expr syn <?> "provider expression"
1494 return [PProvider doc syn fc nfc (ProvPostulate e) n]
1496{-| Parses a transform
1499Transform ::= '%' 'transform' Expr '==>' Expr
1502transform :: SyntaxInfo -> IdrisParser [PDecl]
1503transform syn = do try (lchar '%' *> reserved "transform")
1504 -- leave it unchecked, until we work out what this should
1505 -- actually mean...
1506-- safety <- option True (do reserved "unsafe"
1507-- return False)
1508 l <- expr syn
1509 fc <- getFC
1510 symbol "==>"
1511 r <- expr syn
1512 return [PTransform fc False l r]
1513 <?> "transform"
1515{-| Parses a top-level reflected elaborator script
1518RunElabDecl ::= '%' 'runElab' Expr
1521runElabDecl :: SyntaxInfo -> IdrisParser PDecl
1522runElabDecl syn =
1523 do kwFC <- try (do fc <- getFC
1524 lchar '%'
1525 fc' <- reservedFC "runElab"
1526 return (spanFC fc fc'))
1527 script <- expr syn <?> "elaborator script"
1528 highlightP kwFC AnnKeyword
1529 return $ PRunElabDecl kwFC script (syn_namespace syn)
1530 <?> "top-level elaborator script"
1532{- * Loading and parsing -}
1533{-| Parses an expression from input -}
1534parseExpr :: IState -> String -> Result PTerm
1535parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1537{-| Parses a constant form input -}
1538parseConst :: IState -> String -> Result Const
1539parseConst st = runparser (fmap fst constant) st "(input)"
1541{-| Parses a tactic from input -}
1542parseTactic :: IState -> String -> Result PTactic
1543parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1545{-| Parses a do-step from input (used in the elab shell) -}
1546parseElabShellStep :: IState -> String -> Result (Either ElabShellCmd PDo)
1547parseElabShellStep ist = runparser (fmap Right (do_ defaultSyntax) <|> fmap Left elabShellCmd) ist "(input)"
1548 where elabShellCmd = char ':' >>
1549 (reserved "qed" >> pure EQED ) <|>
1550 (reserved "abandon" >> pure EAbandon ) <|>
1551 (reserved "undo" >> pure EUndo ) <|>
1552 (reserved "state" >> pure EProofState) <|>
1553 (reserved "term" >> pure EProofTerm ) <|>
1554 (expressionTactic ["e", "eval"] EEval ) <|>
1555 (expressionTactic ["t", "type"] ECheck) <|>
1556 (expressionTactic ["search"] ESearch ) <|>
1557 (do reserved "doc"
1558 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)
1559 eof
1560 return (EDocStr doc))
1561 <?> "elab command"
1562 expressionTactic cmds tactic =
1563 do asum (map reserved cmds)
1564 t <- spaced (expr defaultSyntax)
1565 i <- get
1566 return $ tactic (desugar defaultSyntax i t)
1567 spaced parser = indentPropHolds gtProp *> parser
1569-- | Parse module header and imports
1570parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Delta)
1571parseImports fname input
1572 = do i <- getIState
1573 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1574 Failure (ErrInfo err _) -> fail (show err)
1575 Success (x, annots, i) ->
1576 do putIState i
1577 fname' <- runIO $ Dir.makeAbsolute fname
1578 sendHighlighting $ addPath annots fname'
1579 return x
1580 where imports :: IdrisParser ((Maybe (Docstring ()), [String],
1581 [ImportInfo],
1582 Maybe Delta),
1583 [(FC, OutputAnnotation)], IState)
1584 imports = do whiteSpace
1585 (mdoc, mname, annots) <- moduleHeader
1586 ps_exp <- many import_
1587 mrk <- mark
1588 isEof <- lookAheadMatches eof
1589 let mrk' = if isEof
1590 then Nothing
1591 else Just mrk
1592 i <- get
1593 -- add Builtins and Prelude, unless options say
1594 -- not to
1595 let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp
1596 return ((mdoc, mname, ps, mrk'), annots, i)
1598 imp m = ImportInfo False (toPath m)
1599 Nothing [] NoFC NoFC
1600 ns = Spl.splitOn "."
1601 toPath = foldl1' (</>) . ns
1603 addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]
1604 addPath [] _ = []
1605 addPath ((fc, AnnNamespace ns Nothing) : annots) path =
1606 (fc, AnnNamespace ns (Just path)) : addPath annots path
1607 addPath (annot:annots) path = annot : addPath annots path
1609-- | There should be a better way of doing this...
1610findFC :: Doc -> (FC, String)
1611findFC x = let s = show (plain x) in findFC' s
1612 where findFC' s = case span (/= ':') s of
1613 -- Horrid kludge to prevent crashes on Windows
1614 (prefix, ':':'\\':rest) ->
1615 case findFC' rest of
1616 (NoFC, msg) -> (NoFC, msg)
1617 (FileFC f, msg) -> (FileFC (prefix ++ ":\\" ++ f), msg)
1618 (FC f start end, msg) -> (FC (prefix ++ ":\\" ++ f) start end, msg)
1619 (failname, ':':rest) -> case span isDigit rest of
1620 (line, ':':rest') -> case span isDigit rest' of
1621 (col, ':':msg) -> let pos = (read line, read col) in
1622 (FC failname pos pos, msg)
1624-- | Check if the coloring matches the options and corrects if necessary
1625fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1626fixColour False doc = ANSI.plain doc
1627fixColour True doc = doc
1629-- | A program is a list of declarations, possibly with associated
1630-- documentation strings.
1631parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1632 Idris [PDecl]
1633parseProg syn fname input mrk
1634 = do i <- getIState
1635 case runparser mainProg i fname input of
1636 Failure (ErrInfo doc _) -> do -- FIXME: Get error location from trifecta
1637 -- this can't be the solution!
1638 -- Issue #1575 on the issue tracker.
1639 -- https://github.com/idris-lang/Idris-dev/issues/1575
1640 let (fc, msg) = findFC doc
1641 i <- getIState
1642 case idris_outputmode i of
1643 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1644 IdeMode n h -> iWarn fc (P.text msg)
1645 putIState (i { errSpan = Just fc })
1646 return []
1647 Success (x, i) -> do putIState i
1648 reportParserWarnings
1649 return $ collect x
1650 where mainProg :: IdrisParser ([PDecl], IState)
1651 mainProg = case mrk of
1652 Nothing -> do i <- get; return ([], i)
1653 Just mrk -> do
1654 release mrk
1655 ds <- prog syn
1656 i' <- get
1657 return (ds, i')
1659{-| Load idris module and show error if something wrong happens -}
1660loadModule :: FilePath -> IBCPhase -> Idris (Maybe String)
1661loadModule f phase
1662 = idrisCatch (loadModule' f phase)
1663 (\e -> do setErrSpan (getErrSpan e)
1664 ist <- getIState
1665 iWarn (getErrSpan e) $ pprintErr ist e
1666 return Nothing)
1668{-| Load idris module -}
1669loadModule' :: FilePath -> IBCPhase -> Idris (Maybe String)
1670loadModule' f phase
1671 = do i <- getIState
1672 let file = takeWhile (/= ' ') f
1673 ibcsd <- valIBCSubDir i
1674 ids <- allImportDirs
1675 fp <- findImport ids ibcsd file
1676 if file `elem` imported i
1677 then do logParser 1 $ "Already read " ++ file
1678 return Nothing
1679 else do putIState (i { imported = file : imported i })
1680 case fp of
1681 IDR fn -> loadSource False fn Nothing
1682 LIDR fn -> loadSource True fn Nothing
1683 IBC fn src ->
1684 idrisCatch (loadIBC True phase fn)
1685 (\c -> do logParser 1 $ fn ++ " failed " ++ pshow i c
1686 case src of
1687 IDR sfn -> loadSource False sfn Nothing
1688 LIDR sfn -> loadSource True sfn Nothing)
1689 return $ Just file
1691{-| Load idris code from file -}
1692loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()
1693loadFromIFile reexp phase i@(IBC fn src) maxline
1694 = do logParser 1 $ "Skipping " ++ getSrcFile i
1695 idrisCatch (loadIBC reexp phase fn)
1696 (\err -> ierror $ LoadingFailed fn err)
1697 where
1698 getSrcFile (IDR fn) = fn
1699 getSrcFile (LIDR fn) = fn
1700 getSrcFile (IBC f src) = getSrcFile src
1702loadFromIFile _ _ (IDR fn) maxline = loadSource' False fn maxline
1703loadFromIFile _ _ (LIDR fn) maxline = loadSource' True fn maxline
1705{-| Load idris source code and show error if something wrong happens -}
1706loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1707loadSource' lidr r maxline
1708 = idrisCatch (loadSource lidr r maxline)
1709 (\e -> do setErrSpan (getErrSpan e)
1710 ist <- getIState
1711 case e of
1712 At f e' -> iWarn f (pprintErr ist e')
1713 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1715{-| Load Idris source code-}
1716loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1717loadSource lidr f toline
1718 = do logParser 1 ("Reading " ++ f)
1719 i <- getIState
1720 let def_total = default_total i
1721 file_in <- runIO $ readSource f
1722 file <- if lidr then tclift $ unlit f file_in else return file_in
1723 (mdocs, mname, imports_in, pos) <- parseImports f file
1724 ai <- getAutoImports
1725 let imports = map (\n -> ImportInfo True n Nothing [] NoFC NoFC) ai ++ imports_in
1726 ids <- allImportDirs
1727 ibcsd <- valIBCSubDir i
1728 mapM_ (\(re, f, ns, nfc) ->
1729 do fp <- findImport ids ibcsd f
1730 case fp of
1731 LIDR fn -> ifail $ "No ibc for " ++ f
1732 IDR fn -> ifail $ "No ibc for " ++ f
1733 IBC fn src ->
1734 do loadIBC True IBC_Building fn
1735 let srcFn = case src of
1736 IDR fn -> Just fn
1737 LIDR fn -> Just fn
1738 _ -> Nothing
1739 srcFnAbs <- case srcFn of
1740 Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)
1741 Nothing -> return Nothing
1742 sendHighlighting [(nfc, AnnNamespace ns srcFnAbs)])
1743 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]
1744 reportParserWarnings
1745 sendParserHighlighting
1747 -- process and check module aliases
1748 let modAliases = M.fromList
1749 [ (prep alias, prep realName)
1750 | ImportInfo { import_reexport = reexport
1751 , import_path = realName
1752 , import_rename = Just (alias, _)
1753 , import_location = fc } <- imports
1755 prep = map T.pack . reverse . Spl.splitOn [pathSeparator]
1756 aliasNames = [ (alias, fc)
1757 | ImportInfo { import_rename = Just (alias, _)
1758 , import_location = fc } <- imports
1760 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1761 case map head . filter ((/= 1) . length) $ histogram of
1762 [] -> logParser 3 $ "Module aliases: " ++ show (M.toList modAliases)
1763 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1765 i <- getIState
1766 putIState (i { default_access = Private, module_aliases = modAliases })
1767 clearIBC -- start a new .ibc file
1768 -- record package info in .ibc
1769 imps <- allImportDirs
1770 mapM_ addIBC (map IBCImportDir imps)
1771 mapM_ (addIBC . IBCImport)
1772 [ (reexport, realName)
1773 | ImportInfo { import_reexport = reexport
1774 , import_path = realName
1775 } <- imports
1777 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1778 maxline = toline }
1779 ist <- getIState
1780 -- Save the span from parsing the module header, because
1781 -- an empty program parse might obliterate it.
1782 let oldSpan = idris_parsedSpan ist
1783 ds' <- parseProg syntax f file pos
1785 case (ds', oldSpan) of
1786 ([], Just fc) ->
1787 -- If no program elements were parsed, we dind't
1788 -- get a loaded region in the IBC file. That
1789 -- means we need to add it back.
1790 do ist <- getIState
1791 putIState ist { idris_parsedSpan = oldSpan
1792 , ibc_write = IBCParsedRegion fc :
1793 ibc_write ist
1795 _ -> return ()
1796 sendParserHighlighting
1798 -- Parsing done, now process declarations
1800 let ds = namespaces mname ds'
1801 logParser 3 (show $ showDecls verbosePPOption ds)
1802 i <- getIState
1803 logLvl 10 (show (toAlist (idris_implicits i)))
1804 logLvl 3 (show (idris_infixes i))
1805 -- Now add all the declarations to the context
1806 v <- verbose
1807 when v $ iputStrLn $ "Type checking " ++ f
1808 -- we totality check after every Mutual block, so if
1809 -- anything is a single definition, wrap it in a
1810 -- mutual block on its own
1811 elabDecls (toplevelWith f) (map toMutual ds)
1812 i <- getIState
1813 -- simplify every definition do give the totality checker
1814 -- a better chance
1815 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1816 ctxt' <-
1817 do ctxt <- getContext
1818 tclift $ simplifyCasedef n (getErasureInfo i) ctxt
1819 setContext ctxt')
1820 (map snd (idris_totcheck i))
1821 -- build size change graph from simplified definitions
1822 logLvl 1 "Totality checking"
1823 i <- getIState
1824 mapM_ buildSCG (idris_totcheck i)
1825 mapM_ checkDeclTotality (idris_totcheck i)
1826 mapM_ verifyTotality (idris_totcheck i)
1828 -- Redo totality check for deferred names
1829 let deftots = idris_defertotcheck i
1830 logLvl 2 $ "Totality checking " ++ show deftots
1831 mapM_ (\x -> do tot <- getTotality x
1832 case tot of
1833 Total _ ->
1834 do let opts = case lookupCtxtExact x (idris_flags i) of
1835 Just os -> os
1836 Nothing -> []
1837 when (AssertTotal `notElem` opts) $
1838 setTotality x Unchecked
1839 _ -> return ()) (map snd deftots)
1840 mapM_ buildSCG deftots
1841 mapM_ checkDeclTotality deftots
1843 logLvl 1 ("Finished " ++ f)
1844 ibcsd <- valIBCSubDir i
1845 logLvl 1 "Universe checking"
1846 iucheck
1847 let ibc = ibcPathNoFallback ibcsd f
1848 i <- getIState
1849 addHides (hide_list i)
1851 -- Save module documentation if applicable
1852 i <- getIState
1853 case mdocs of
1854 Nothing -> return ()
1855 Just docs -> addModDoc syntax mname docs
1858 -- Finally, write an ibc and highlights if checking was successful
1859 ok <- noErrors
1860 when ok $
1861 do idrisCatch (do writeIBC f ibc; clearIBC)
1862 (\c -> return ()) -- failure is harmless
1863 hl <- getDumpHighlighting
1864 when hl $
1865 idrisCatch (writeHighlights f)
1866 (const $ return ()) -- failure is harmless
1867 clearHighlights
1868 i <- getIState
1869 putIState (i { default_total = def_total,
1870 hide_list = emptyContext })
1871 return ()
1872 where
1873 namespaces :: [String] -> [PDecl] -> [PDecl]
1874 namespaces [] ds = ds
1875 namespaces (x:xs) ds = [PNamespace x NoFC (namespaces xs ds)]
1877 toMutual :: PDecl -> PDecl
1878 toMutual m@(PMutual _ d) = m
1879 toMutual (PNamespace x fc ds) = PNamespace x fc (map toMutual ds)
1880 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1881 case x of
1882 PClauses{} -> r
1883 PClass{} -> r
1884 PData{} -> r
1885 PInstance{} -> r
1886 _ -> x
1888 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1889 addModDoc syn mname docs =
1890 do ist <- getIState
1891 docs' <- elabDocTerms (toplevelWith f) (parsedDocs ist)
1892 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1893 putIState ist { idris_moduledocs = modDocs' }
1894 addIBC (IBCModDocs docName)
1895 where
1896 docName = NS modDocName (map T.pack (reverse mname))
1897 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1899{-| Adds names to hide list -}
1900addHides :: Ctxt Accessibility -> Idris ()
1901addHides xs = do i <- getIState
1902 let defh = default_access i
1903 mapM_ doHide (toAlist xs)
1904 where doHide (n, a) = do setAccessibility n a
1905 addIBC (IBCAccess n a)