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