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