git.iko.soy/Idris-dev
on 2df4ef6 help sign in
Idris-dev/src/Idris/Parser.hs
1764 lines 67 kB history raw
1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
2{-# OPTIONS_GHC -O0 #-}
3module Idris.Parser(module Idris.Parser,
4 module Idris.ParseExpr,
5 module Idris.ParseData,
6 module Idris.ParseHelpers,
7 module Idris.ParseOps) 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.ParseHelpers
39import Idris.ParseOps
40import Idris.ParseExpr
41import Idris.ParseData
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 here
195 let continue = case maxline syn of
196 Nothing -> True
197 Just l -> if fst (fc_end fc) > l
198 then mut_nesting syn /= 0
199 else True
200 if continue then do notEndBlock
201 declBody
202 else fail "End of readable input"
203 where declBody :: IdrisParser [PDecl]
204 declBody = declBody'
205 <|> using_ syn
206 <|> params syn
207 <|> mutual syn
208 <|> namespace syn
209 <|> class_ syn
210 <|> instance_ syn
211 <|> do d <- dsl syn; return [d]
212 <|> directive syn
213 <|> provider syn
214 <|> transform syn
215 <|> do import_; fail "imports must be at top of file"
216 <?> "declaration"
217 declBody' :: IdrisParser [PDecl]
218 declBody' = do d <- decl' syn
219 i <- get
220 let d' = fmap (debindApp syn . (desugar syn i)) d
221 return [d']
223{- | Parses a top-level declaration with possible syntax sugar
226Decl' ::=
227 Fixity
228 | FunDecl'
229 | Data
230 | Record
231 | SyntaxDecl
232 ;
234-}
235decl' :: SyntaxInfo -> IdrisParser PDecl
236decl' syn = fixity
237 <|> syntaxDecl syn
238 <|> fnDecl' syn
239 <|> data_ syn
240 <|> record syn
241 <|> runElabDecl syn
242 <?> "declaration"
244externalDecl :: SyntaxInfo -> IdrisParser [PDecl]
245externalDecl syn = do i <- get
246 notEndBlock
247 FC fn start _ <- getFC
248 decls <- declExtensions syn (syntaxRulesList $ syntax_rules i)
249 FC _ _ end <- getFC
250 let outerFC = FC fn start end
251 return $ map (mapPDeclFC (fixFC outerFC)
252 (fixFCH fn outerFC))
253 decls
254 where
255 -- | Fix non-highlighting FCs to prevent spurious error location reports
256 fixFC :: FC -> FC -> FC
257 fixFC outer inner | inner `fcIn` outer = inner
258 | otherwise = outer
259 -- | Fix highlighting FCs by obliterating them, to avoid spurious highlights
260 fixFCH fn outer inner | inner `fcIn` outer = inner
261 | otherwise = FileFC fn
263declExtensions :: SyntaxInfo -> [Syntax] -> IdrisParser [PDecl]
264declExtensions syn rules = declExtension syn [] (filter isDeclRule rules)
265 <?> "user-defined declaration"
266 where
267 isDeclRule (DeclRule _ _) = True
268 isDeclRule _ = False
270declExtension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax]
271 -> IdrisParser [PDecl]
272declExtension syn ns rules =
273 choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->
274 case head rs of -- can never be []
275 DeclRule (symb:_) _ -> try $ do
276 n <- extSymbol symb
277 declExtension syn (n : ns) [DeclRule ss t | (DeclRule (_:ss) t) <- rs]
278 -- If we have more than one Rule in this bucket, our grammar is
279 -- nondeterministic.
280 DeclRule [] dec -> let r = map (update (mapMaybe id ns)) dec in
281 return r
283 where
284 update :: [(Name, SynMatch)] -> PDecl -> PDecl
285 update ns = updateNs ns . fmap (updateRefs ns) . fmap (updateSynMatch ns)
287 updateRefs ns = mapPT newref
288 where
289 newref (PRef fc fcs n) = PRef fc fcs (updateB ns n)
290 newref t = t
292 -- Below is a lot of tedious boilerplate which updates any top level
293 -- names in the declaration. It will only change names which are bound in
294 -- the declaration (including method names in classes and field names in
295 -- record declarations, not including pattern variables)
296 updateB :: [(Name, SynMatch)] -> Name -> Name
297 updateB ns (NS n mods) = NS (updateB ns n) mods
298 updateB ns n = case lookup n ns of
299 Just (SynBind tfc t) -> t
300 _ -> n
302 updateNs :: [(Name, SynMatch)] -> PDecl -> PDecl
303 updateNs ns (PTy doc argdoc s fc o n fc' t)
304 = PTy doc argdoc s fc o (updateB ns n) fc' t
305 updateNs ns (PClauses fc o n cs)
306 = PClauses fc o (updateB ns n) (map (updateClause ns) cs)
307 updateNs ns (PCAF fc n t) = PCAF fc (updateB ns n) t
308 updateNs ns (PData ds cds s fc o dat)
309 = PData ds cds s fc o (updateData ns dat)
310 updateNs ns (PParams fc ps ds) = PParams fc ps (map (updateNs ns) ds)
311 updateNs ns (PNamespace s fc ds) = PNamespace s fc (map (updateNs ns) ds)
312 updateNs ns (PRecord doc syn fc o n fc' ps pdocs fields cname cdoc s)
313 = PRecord doc syn fc o (updateB ns n) fc' ps pdocs
314 (map (updateField ns) fields)
315 (updateRecCon ns cname)
316 cdoc
317 s
318 updateNs ns (PClass docs s fc cs cn fc' ps pdocs pdets ds cname cdocs)
319 = PClass docs s fc cs (updateB ns cn) fc' ps pdocs pdets
320 (map (updateNs ns) ds)
321 (updateRecCon ns cname)
322 cdocs
323 updateNs ns (PInstance docs pdocs s fc cs cn fc' ps ity ni ds)
324 = PInstance docs pdocs s fc cs (updateB ns cn) fc'
325 ps ity (fmap (updateB ns) ni)
326 (map (updateNs ns) ds)
327 updateNs ns (PMutual fc ds) = PMutual fc (map (updateNs ns) ds)
328 updateNs ns (PProvider docs s fc fc' pw n)
329 = PProvider docs s fc fc' pw (updateB ns n)
330 updateNs ns d = d
332 updateRecCon ns Nothing = Nothing
333 updateRecCon ns (Just (n, fc)) = Just (updateB ns n, fc)
335 updateField ns (m, p, t, doc) = (updateRecCon ns m, p, t, doc)
337 updateClause ns (PClause fc n t ts t' ds)
338 = PClause fc (updateB ns n) t ts t' (map (update ns) ds)
339 updateClause ns (PWith fc n t ts t' m ds)
340 = PWith fc (updateB ns n) t ts t' m (map (update ns) ds)
341 updateClause ns (PClauseR fc ts t ds)
342 = PClauseR fc ts t (map (update ns) ds)
343 updateClause ns (PWithR fc ts t m ds)
344 = PWithR fc ts t m (map (update ns) ds)
346 updateData ns (PDatadecl n fc t cs)
347 = PDatadecl (updateB ns n) fc t (map (updateCon ns) cs)
348 updateData ns (PLaterdecl n fc t)
349 = PLaterdecl (updateB ns n) fc t
351 updateCon ns (cd, ads, cn, fc, ty, fc', fns)
352 = (cd, ads, updateB ns cn, fc, ty, fc', fns)
354 ruleGroup [] [] = True
355 ruleGroup (s1:_) (s2:_) = s1 == s2
356 ruleGroup _ _ = False
358 extSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
359 extSymbol (Keyword n) = do fc <- reservedFC (show n)
360 highlightP fc AnnKeyword
361 return Nothing
362 extSymbol (Expr n) = do tm <- expr syn
363 return $ Just (n, SynTm tm)
364 extSymbol (SimpleExpr n) = do tm <- simpleExpr syn
365 return $ Just (n, SynTm tm)
366 extSymbol (Binding n) = do (b, fc) <- name
367 return $ Just (n, SynBind fc b)
368 extSymbol (Symbol s) = do fc <- symbolFC s
369 highlightP fc AnnKeyword
370 return Nothing
372{- | Parses a syntax extension declaration (and adds the rule to parser state)
375 SyntaxDecl ::= SyntaxRule;
377-}
378syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
379syntaxDecl syn = do s <- syntaxRule syn
380 i <- get
381 put (i `addSyntax` s)
382 fc <- getFC
383 return (PSyntax fc s)
385-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.
386addSyntax :: IState -> Syntax -> IState
387addSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
388 syntax_keywords = ks ++ ns,
389 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc }
390 where rs = syntax_rules i
391 ns = syntax_keywords i
392 ibc = ibc_write i
393 ks = map show (syntaxNames s)
395-- | Like 'addSyntax', but no effect on the IBC.
396addReplSyntax :: IState -> Syntax -> IState
397addReplSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
398 syntax_keywords = ks ++ ns }
399 where rs = syntax_rules i
400 ns = syntax_keywords i
401 ks = map show (syntaxNames s)
403{- | Parses a syntax extension declaration
406SyntaxRuleOpts ::= 'term' | 'pattern';
410SyntaxRule ::=
411 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
415SyntaxSym ::= '[' Name_t ']'
416 | '{' Name_t '}'
417 | Name_t
418 | StringLiteral_t
419 ;
421-}
422syntaxRule :: SyntaxInfo -> IdrisParser Syntax
423syntaxRule syn
424 = do sty <- try (do
425 pushIndent
426 sty <- option AnySyntax
427 (do reservedHL "term"; return TermSyntax
428 <|> do reservedHL "pattern"; return PatternSyntax)
429 reservedHL "syntax"
430 return sty)
431 syms <- some syntaxSym
432 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
433 let ns = mapMaybe getName syms
434 when (length ns /= length (nub ns))
435 $ unexpected "repeated variable in syntax rule"
436 lchar '='
437 tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]
438 terminator
439 return (Rule (mkSimple syms) tm sty)
440 <|> do reservedHL "decl"; reservedHL "syntax"
441 syms <- some syntaxSym
442 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
443 let ns = mapMaybe getName syms
444 when (length ns /= length (nub ns))
445 $ unexpected "repeated variable in syntax rule"
446 lchar '='
447 openBlock
448 dec <- some (decl syn)
449 closeBlock
450 return (DeclRule (mkSimple syms) (concat dec))
451 where
452 isExpr (Expr _) = True
453 isExpr _ = False
454 getName (Expr n) = Just n
455 getName _ = Nothing
456 -- Can't parse two full expressions (i.e. expressions with application) in a row
457 -- so change them both to a simple expression
458 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
459 mkSimple xs = mkSimple' xs
461 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
462 mkSimple es
463 -- Can't parse a full expression followed by operator like characters due to ambiguity
464 mkSimple' (Expr e : Symbol s : es)
465 | takeWhile (`elem` opChars) ts /= "" = SimpleExpr e : Symbol s : mkSimple' es
466 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s
467 mkSimple' (e : es) = e : mkSimple' es
468 mkSimple' [] = []
470 -- Prevent syntax variable capture by making all binders under syntax unique
471 -- (the ol' Common Lisp GENSYM approach)
472 uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
473 uniquifyBinders userNames = fixBind []
474 where
475 fixBind :: [(Name, Name)] -> PTerm -> IdrisParser PTerm
476 fixBind rens (PRef fc hls n) | Just n' <- lookup n rens =
477 return $ PRef fc hls n'
478 fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =
479 return $ PPatvar fc n'
480 fixBind rens (PLam fc n nfc ty body)
481 | n `elem` userNames = liftM2 (PLam fc n nfc) (fixBind rens ty) (fixBind rens body)
482 | otherwise =
483 do ty' <- fixBind rens ty
484 n' <- gensym n
485 body' <- fixBind ((n,n'):rens) body
486 return $ PLam fc n' nfc ty' body'
487 fixBind rens (PPi plic n nfc argTy body)
488 | n `elem` userNames = liftM2 (PPi plic n nfc) (fixBind rens argTy) (fixBind rens body)
489 | otherwise =
490 do ty' <- fixBind rens argTy
491 n' <- gensym n
492 body' <- fixBind ((n,n'):rens) body
493 return $ (PPi plic n' nfc ty' body')
494 fixBind rens (PLet fc n nfc ty val body)
495 | n `elem` userNames = liftM3 (PLet fc n nfc)
496 (fixBind rens ty)
497 (fixBind rens val)
498 (fixBind rens body)
499 | otherwise =
500 do ty' <- fixBind rens ty
501 val' <- fixBind rens val
502 n' <- gensym n
503 body' <- fixBind ((n,n'):rens) body
504 return $ PLet fc n' nfc ty' val' body'
505 fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =
506 return $ PMatchApp fc n'
507 fixBind rens x = descendM (fixBind rens) x
509 gensym :: Name -> IdrisParser Name
510 gensym n = do ist <- get
511 let idx = idris_name ist
512 put ist { idris_name = idx + 1 }
513 return $ sMN idx (show n)
515{- | Parses a syntax symbol (either binding variable, keyword or expression)
518SyntaxSym ::= '[' Name_t ']'
519 | '{' Name_t '}'
520 | Name_t
521 | StringLiteral_t
522 ;
524 -}
525syntaxSym :: IdrisParser SSymbol
526syntaxSym = try (do lchar '['; n <- fst <$> name; lchar ']'
527 return (Expr n))
528 <|> try (do lchar '{'; n <- fst <$> name; lchar '}'
529 return (Binding n))
530 <|> do n <- fst <$> iName []
531 return (Keyword n)
532 <|> do sym <- fmap fst stringLiteral
533 return (Symbol sym)
534 <?> "syntax symbol"
536{- | Parses a function declaration with possible syntax sugar
539 FunDecl ::= FunDecl';
541-}
542fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
543fnDecl syn = try (do notEndBlock
544 d <- fnDecl' syn
545 i <- get
546 let d' = fmap (desugar syn i) d
547 return [d']) <?> "function declaration"
549{-| Parses a function declaration
552 FunDecl' ::=
553 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
554 | Postulate
555 | Pattern
556 | CAF
557 ;
559-}
560fnDecl' :: SyntaxInfo -> IdrisParser PDecl
561fnDecl' syn = checkFixity $
562 do (doc, argDocs, fc, opts', n, nfc, acc) <- try (do
563 pushIndent
564 (doc, argDocs) <- docstring syn
565 ist <- get
566 let initOpts = if default_total ist
567 then [TotalFn]
568 else []
569 opts <- fnOpts initOpts
570 acc <- optional accessibility
571 opts' <- fnOpts opts
572 (n_in, nfc) <- fnName
573 let n = expandNS syn n_in
574 fc <- getFC
575 lchar ':'
576 return (doc, argDocs, fc, opts', n, nfc, acc))
577 ty <- typeExpr (allowImp syn)
578 terminator
579 addAcc n acc
580 return (PTy doc argDocs syn fc opts' n nfc ty)
581 <|> postulate syn
582 <|> caf syn
583 <|> pattern syn
584 <?> "function declaration"
585 where checkFixity :: IdrisParser PDecl -> IdrisParser PDecl
586 checkFixity p = do decl <- p
587 case getName decl of
588 Nothing -> return decl
589 Just n -> do fOk <- fixityOK n
590 unless fOk . fail $
591 "Missing fixity declaration for " ++ show n
592 return decl
593 getName (PTy _ _ _ _ _ n _ _) = Just n
594 getName _ = Nothing
595 fixityOK (NS n _) = fixityOK n
596 fixityOK (UN n) | all (flip elem opChars) (str n) =
597 do fixities <- fmap idris_infixes get
598 return . elem (str n) . map (\ (Fix _ op) -> op) $ fixities
599 | otherwise = return True
600 fixityOK _ = return True
602{-| Parses function options given initial options
605FnOpts ::= 'total'
606 | 'partial'
607 | 'covering'
608 | 'implicit'
609 | '%' 'no_implicit'
610 | '%' 'assert_total'
611 | '%' 'error_handler'
612 | '%' 'reflection'
613 | '%' 'specialise' '[' NameTimesList? ']'
614 ;
618NameTimes ::= FnName Natural?;
622NameTimesList ::=
623 NameTimes
624 | NameTimes ',' NameTimesList
625 ;
627-}
628-- FIXME: Check compatability for function options (i.e. partal/total)
629--
630-- Issue #1574 on the issue tracker.
631-- https://github.com/idris-lang/Idris-dev/issues/1574
632fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
633fnOpts opts
634 = do reservedHL "total"; fnOpts (TotalFn : opts)
635 <|> do reservedHL "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
636 <|> do reservedHL "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))
637 <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;
638 fnOpts (CExport c : opts)
639 <|> do try (lchar '%' *> reserved "no_implicit");
640 fnOpts (NoImplicit : opts)
641 <|> do try (lchar '%' *> reserved "inline");
642 fnOpts (Inlinable : opts)
643 <|> do try (lchar '%' *> reserved "assert_total");
644 fnOpts (AssertTotal : opts)
645 <|> do try (lchar '%' *> reserved "error_handler");
646 fnOpts (ErrorHandler : opts)
647 <|> do try (lchar '%' *> reserved "error_reverse");
648 fnOpts (ErrorReverse : opts)
649 <|> do try (lchar '%' *> reserved "reflection");
650 fnOpts (Reflection : opts)
651 <|> do try (lchar '%' *> reserved "hint");
652 fnOpts (AutoHint : opts)
653 <|> do lchar '%'; reserved "specialise";
654 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
655 fnOpts (Specialise ns : opts)
656 <|> do reservedHL "implicit"; fnOpts (Implicit : opts)
657 <|> return opts
658 <?> "function modifier"
659 where nameTimes :: IdrisParser (Name, Maybe Int)
660 nameTimes = do n <- fst <$> fnName
661 t <- option Nothing (do reds <- fmap fst natural
662 return (Just (fromInteger reds)))
663 return (n, t)
665{- | Parses a postulate
668Postulate ::=
669 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
670 ;
672-}
673postulate :: SyntaxInfo -> IdrisParser PDecl
674postulate syn = do (doc, ext)
675 <- try $ do (doc, _) <- docstring syn
676 pushIndent
677 ext <- ppostDecl
678 return (doc, ext)
679 ist <- get
680 let initOpts = if default_total ist
681 then [TotalFn]
682 else []
683 opts <- fnOpts initOpts
684 acc <- optional accessibility
685 opts' <- fnOpts opts
686 (n_in, nfc) <- fnName
687 let n = expandNS syn n_in
688 lchar ':'
689 ty <- typeExpr (allowImp syn)
690 fc <- getFC
691 terminator
692 addAcc n acc
693 return (PPostulate ext doc syn fc nfc opts' n ty)
694 <?> "postulate"
695 where ppostDecl = do fc <- reservedHL "postulate"; return False
696 <|> do lchar '%'; reserved "extern"; return True
697{- | Parses a using declaration
700Using ::=
701 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
702 ;
704 -}
705using_ :: SyntaxInfo -> IdrisParser [PDecl]
706using_ syn =
707 do reservedHL "using"
708 lchar '('; ns <- usingDeclList syn; lchar ')'
709 openBlock
710 let uvars = using syn
711 ds <- many (decl (syn { using = uvars ++ ns }))
712 closeBlock
713 return (concat ds)
714 <?> "using declaration"
716{- | Parses a parameters declaration
719Params ::=
720 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
721 ;
723 -}
724params :: SyntaxInfo -> IdrisParser [PDecl]
725params syn =
726 do reservedHL "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
727 let ns' = [(n, ty) | (n, _, ty) <- ns]
728 openBlock
729 let pvars = syn_params syn
730 ds <- many (decl syn { syn_params = pvars ++ ns' })
731 closeBlock
732 fc <- getFC
733 return [PParams fc ns' (concat ds)]
734 <?> "parameters declaration"
736{- | Parses a mutual declaration (for mutually recursive functions)
739Mutual ::=
740 'mutual' OpenBlock Decl* CloseBlock
741 ;
743-}
744mutual :: SyntaxInfo -> IdrisParser [PDecl]
745mutual syn =
746 do reservedHL "mutual"
747 openBlock
748 let pvars = syn_params syn
749 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
750 closeBlock
751 fc <- getFC
752 return [PMutual fc (concat ds)]
753 <?> "mutual block"
755{-| Parses a namespace declaration
758Namespace ::=
759 'namespace' identifier OpenBlock Decl+ CloseBlock
760 ;
762-}
763namespace :: SyntaxInfo -> IdrisParser [PDecl]
764namespace syn =
765 do reservedHL "namespace"
766 (n, nfc) <- identifier
767 openBlock
768 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
769 closeBlock
770 return [PNamespace n nfc (concat ds)]
771 <?> "namespace declaration"
773{- | Parses a methods block (for instances)
776 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
778-}
779instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
780instanceBlock syn = do reservedHL "where"
781 openBlock
782 ds <- many (fnDecl syn)
783 closeBlock
784 return (concat ds)
785 <?> "instance block"
787{- | Parses a methods and instances block (for type classes)
790MethodOrInstance ::=
791 FnDecl
792 | Instance
793 ;
797ClassBlock ::=
798 'where' OpenBlock Constructor? MethodOrInstance* CloseBlock
799 ;
801-}
802classBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])
803classBlock syn = do reservedHL "where"
804 openBlock
805 (cn, cd) <- option (Nothing, emptyDocstring) $
806 try (do (doc, _) <- option noDocs docComment
807 n <- constructor
808 return (Just n, doc))
809 ist <- get
810 let cd' = annotate syn ist cd
812 ds <- many (notEndBlock >> instance_ syn <|> fnDecl syn)
813 closeBlock
814 return (cn, cd', concat ds)
815 <?> "class block"
817 where
818 constructor :: IdrisParser (Name, FC)
819 constructor = reservedHL "constructor" *> fnName
821 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)
822 annotate syn ist = annotCode $ tryFullExpr syn ist
824{-| Parses a type class declaration
827ClassArgument ::=
828 Name
829 | '(' Name ':' Expr ')'
830 ;
834Class ::=
835 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
836 ;
838-}
839class_ :: SyntaxInfo -> IdrisParser [PDecl]
840class_ syn = do (doc, argDocs, acc)
841 <- try (do (doc, argDocs) <- docstring syn
842 acc <- optional accessibility
843 reservedHL "class"
844 return (doc, argDocs, acc))
845 fc <- getFC
846 cons <- constraintList syn
847 let cons' = [(c, ty) | (c, _, ty) <- cons]
848 (n_in, nfc) <- fnName
849 let n = expandNS syn n_in
850 cs <- many carg
851 fds <- option [(cn, NoFC) | (cn, _, _) <- cs] fundeps
852 (cn, cd, ds) <- option (Nothing, fst noDocs, []) (classBlock syn)
853 accData acc n (concatMap declared ds)
854 return [PClass doc syn fc cons' n nfc cs argDocs fds ds cn cd]
855 <?> "type-class declaration"
856 where
857 fundeps :: IdrisParser [(Name, FC)]
858 fundeps = do lchar '|'; sepBy name (lchar ',')
860 carg :: IdrisParser (Name, FC, PTerm)
861 carg = do lchar '('; (i, ifc) <- name; lchar ':'; ty <- expr syn; lchar ')'
862 return (i, ifc, ty)
863 <|> do (i, ifc) <- name
864 fc <- getFC
865 return (i, ifc, PType fc)
867{- | Parses a type class instance declaration
870 Instance ::=
871 DocComment_t? 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
872 ;
876InstanceName ::= '[' Name ']';
878-}
879instance_ :: SyntaxInfo -> IdrisParser [PDecl]
880instance_ syn = do (doc, argDocs)
881 <- try (docstring syn <* reservedHL "instance")
882 fc <- getFC
883 en <- optional instanceName
884 cs <- constraintList syn
885 let cs' = [(c, ty) | (c, _, ty) <- cs]
886 (cn, cnfc) <- fnName
887 args <- many (simpleExpr syn)
888 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)
889 let t = bindList (PPi constraint) cs sc
890 ds <- option [] (instanceBlock syn)
891 return [PInstance doc argDocs syn fc cs' cn cnfc args t en ds]
892 <?> "instance declaration"
893 where instanceName :: IdrisParser Name
894 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'
895 let n = expandNS syn n_in
896 return n
897 <?> "instance name"
900-- | Parse a docstring
901docstring :: SyntaxInfo
902 -> IdrisParser (Docstring (Either Err PTerm),
903 [(Name,Docstring (Either Err PTerm))])
904docstring syn = do (doc, argDocs) <- option noDocs docComment
905 ist <- get
906 let doc' = annotCode (tryFullExpr syn ist) doc
907 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
908 | (n, d) <- argDocs ]
909 return (doc', argDocs')
912{- | Parses a using declaration list
915UsingDeclList ::=
916 UsingDeclList'
917 | NameList TypeSig
918 ;
922UsingDeclList' ::=
923 UsingDecl
924 | UsingDecl ',' UsingDeclList'
925 ;
929NameList ::=
930 Name
931 | Name ',' NameList
932 ;
934-}
935usingDeclList :: SyntaxInfo -> IdrisParser [Using]
936usingDeclList syn
937 = try (sepBy1 (usingDecl syn) (lchar ','))
938 <|> do ns <- sepBy1 (fst <$> name) (lchar ',')
939 lchar ':'
940 t <- typeExpr (disallowImp syn)
941 return (map (\x -> UImplicit x t) ns)
942 <?> "using declaration list"
944{- |Parses a using declaration
947UsingDecl ::=
948 FnName TypeSig
949 | FnName FnName+
950 ;
952-}
953usingDecl :: SyntaxInfo -> IdrisParser Using
954usingDecl syn = try (do x <- fst <$> fnName
955 lchar ':'
956 t <- typeExpr (disallowImp syn)
957 return (UImplicit x t))
958 <|> do c <- fst <$> fnName
959 xs <- some (fst <$> fnName)
960 return (UConstraint c xs)
961 <?> "using declaration"
963{- | Parse a clause with patterns
966Pattern ::= Clause;
968-}
969pattern :: SyntaxInfo -> IdrisParser PDecl
970pattern syn = do fc <- getFC
971 clause <- clause syn
972 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
973 <?> "pattern"
975{- | Parse a constant applicative form declaration
978CAF ::= 'let' FnName '=' Expr Terminator;
980-}
981caf :: SyntaxInfo -> IdrisParser PDecl
982caf syn = do reservedHL "let"
983 n_in <- fst <$> fnName; let n = expandNS syn n_in
984 pushIndent
985 lchar '='
986 t <- indented $ expr syn
987 terminator
988 fc <- getFC
989 return (PCAF fc n t)
990 <?> "constant applicative form declaration"
992{- | Parse an argument expression
995ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
997-}
998argExpr :: SyntaxInfo -> IdrisParser PTerm
999argExpr syn = let syn' = syn { inPattern = True } in
1000 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
1001 <?> "argument expression"
1003{- | Parse a right hand side of a function
1006RHS ::= '=' Expr
1007 | '?=' RHSName? Expr
1008 | Impossible
1013RHSName ::= '{' FnName '}';
1016rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
1017rhs syn n = do lchar '='; expr syn
1018 <|> do symbol "?=";
1019 fc <- getFC
1020 name <- option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";
1021 return n)
1022 r <- expr syn
1023 return (addLet fc name r)
1024 <|> impossible
1025 <?> "function right hand side"
1026 where mkN :: Name -> Name
1027 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
1028 then sUN "infix_op_lemma_1"
1029 else sUN (str x++"_lemma_1")
1030 mkN (NS x n) = NS (mkN x) n
1031 n' :: Name
1032 n' = mkN n
1033 addLet :: FC -> Name -> PTerm -> PTerm
1034 addLet fc nm (PLet fc' n nfc ty val r) = PLet fc' n nfc ty val (addLet fc nm r)
1035 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
1036 where addLetC (l, r) = (l, addLet fc nm r)
1037 addLet fc nm r = (PLet fc (sUN "value") NoFC Placeholder r (PMetavar NoFC nm))
1039{- |Parses a function clause
1042RHSOrWithBlock ::= RHS WhereOrTerminator
1043 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
1048Clause ::= WExpr+ RHSOrWithBlock
1049 | SimpleExpr '<==' FnName RHS WhereOrTerminator
1050 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
1051 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
1056ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
1060WhereOrTerminator ::= WhereBlock | Terminator;
1063clause :: SyntaxInfo -> IdrisParser PClause
1064clause syn
1065 = do wargs <- try (do pushIndent; some (wExpr syn))
1066 fc <- getFC
1067 ist <- get
1068 n <- case lastParse ist of
1069 Just t -> return t
1070 Nothing -> fail "Invalid clause"
1071 (do r <- rhs syn n
1072 let ctxt = tt_ctxt ist
1073 let wsyn = syn { syn_namespace = [] }
1074 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1075 popIndent
1076 return x,
1077 do terminator
1078 return ([], [])]
1079 return $ PClauseR fc wargs r wheres) <|> (do
1080 popIndent
1081 reservedHL "with"
1082 wval <- simpleExpr syn
1083 pn <- optProof
1084 openBlock
1085 ds <- some $ fnDecl syn
1086 let withs = concat ds
1087 closeBlock
1088 return $ PWithR fc wargs wval pn withs)
1089 <|> do ty <- try (do pushIndent
1090 ty <- simpleExpr syn
1091 symbol "<=="
1092 return ty)
1093 fc <- getFC
1094 n_in <- fst <$> fnName; let n = expandNS syn n_in
1095 r <- rhs syn n
1096 ist <- get
1097 let ctxt = tt_ctxt ist
1098 let wsyn = syn { syn_namespace = [] }
1099 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1100 popIndent
1101 return x,
1102 do terminator
1103 return ([], [])]
1104 let capp = PLet fc (sMN 0 "match") NoFC
1105 ty
1106 (PMatchApp fc n)
1107 (PRef fc [] (sMN 0 "match"))
1108 ist <- get
1109 put (ist { lastParse = Just n })
1110 return $ PClause fc n capp [] r wheres
1111 <|> do (l, op, nfc) <- try (do
1112 pushIndent
1113 l <- argExpr syn
1114 (op, nfc) <- operatorFC
1115 when (op == "=" || op == "?=" ) $
1116 fail "infix clause definition with \"=\" and \"?=\" not supported "
1117 return (l, op, nfc))
1118 let n = expandNS syn (sUN op)
1119 r <- argExpr syn
1120 fc <- getFC
1121 wargs <- many (wExpr syn)
1122 (do rs <- rhs syn n
1123 let wsyn = syn { syn_namespace = [] }
1124 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1125 popIndent
1126 return x,
1127 do terminator
1128 return ([], [])]
1129 ist <- get
1130 let capp = PApp fc (PRef nfc [nfc] n) [pexp l, pexp r]
1131 put (ist { lastParse = Just n })
1132 return $ PClause fc n capp wargs rs wheres) <|> (do
1133 popIndent
1134 reservedHL "with"
1135 wval <- bracketed syn
1136 pn <- optProof
1137 openBlock
1138 ds <- some $ fnDecl syn
1139 closeBlock
1140 ist <- get
1141 let capp = PApp fc (PRef fc [] n) [pexp l, pexp r]
1142 let withs = map (fillLHSD n capp wargs) $ concat ds
1143 put (ist { lastParse = Just n })
1144 return $ PWith fc n capp wargs wval pn withs)
1145 <|> do pushIndent
1146 (n_in, nfc) <- fnName; let n = expandNS syn n_in
1147 cargs <- many (constraintArg syn)
1148 fc <- getFC
1149 args <- many (try (implicitArg (syn { inPattern = True } ))
1150 <|> (fmap pexp (argExpr syn)))
1151 wargs <- many (wExpr syn)
1152 let capp = PApp fc (PRef nfc [nfc] n)
1153 (cargs ++ args)
1154 (do r <- rhs syn n
1155 ist <- get
1156 let ctxt = tt_ctxt ist
1157 let wsyn = syn { syn_namespace = [] }
1158 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1159 popIndent
1160 return x,
1161 do terminator
1162 return ([], [])]
1163 ist <- get
1164 put (ist { lastParse = Just n })
1165 return $ PClause fc n capp wargs r wheres) <|> (do
1166 reservedHL "with"
1167 ist <- get
1168 put (ist { lastParse = Just n })
1169 wval <- bracketed syn
1170 pn <- optProof
1171 openBlock
1172 ds <- some $ fnDecl syn
1173 let withs = map (fillLHSD n capp wargs) $ concat ds
1174 closeBlock
1175 popIndent
1176 return $ PWith fc n capp wargs wval pn withs)
1177 <?> "function clause"
1178 where
1179 optProof = option Nothing (do reservedHL "proof"
1180 n <- fnName
1181 return (Just n))
1183 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
1184 fillLHS n capp owargs (PClauseR fc wargs v ws)
1185 = PClause fc n capp (owargs ++ wargs) v ws
1186 fillLHS n capp owargs (PWithR fc wargs v pn ws)
1187 = PWith fc n capp (owargs ++ wargs) v pn
1188 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1189 fillLHS _ _ _ c = c
1191 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
1192 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1193 fillLHSD n c a x = x
1195{-| Parses with pattern
1198WExpr ::= '|' Expr';
1201wExpr :: SyntaxInfo -> IdrisParser PTerm
1202wExpr syn = do lchar '|'
1203 expr' (syn { inPattern = True })
1204 <?> "with pattern"
1206{- | Parses a where block
1209WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
1212whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
1213whereBlock n syn
1214 = do reservedHL "where"
1215 ds <- indentedBlock1 (decl syn)
1216 let dns = concatMap (concatMap declared) ds
1217 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1218 <?> "where block"
1220{- |Parses a code generation target language name
1223Codegen ::= 'C'
1224 | 'Java'
1225 | 'JavaScript'
1226 | 'Node'
1227 | 'LLVM'
1228 | 'Bytecode'
1232codegen_ :: IdrisParser Codegen
1233codegen_ = do n <- fst <$> identifier
1234 return (Via (map toLower n))
1235 <|> do reserved "Bytecode"; return Bytecode
1236 <?> "code generation language"
1238{- |Parses a compiler directive
1240StringList ::=
1241 String
1242 | String ',' StringList
1247Directive ::= '%' Directive';
1251Directive' ::= 'lib' CodeGen String_t
1252 | 'link' CodeGen String_t
1253 | 'flag' CodeGen String_t
1254 | 'include' CodeGen String_t
1255 | 'hide' Name
1256 | 'freeze' Name
1257 | 'access' Accessibility
1258 | 'default' Totality
1259 | 'logging' Natural
1260 | 'dynamic' StringList
1261 | 'name' Name NameList
1262 | 'error_handlers' Name NameList
1263 | 'language' 'TypeProviders'
1264 | 'language' 'ErrorReflection'
1268directive :: SyntaxInfo -> IdrisParser [PDecl]
1269directive syn = do try (lchar '%' *> reserved "lib")
1270 cgn <- codegen_
1271 lib <- fmap fst stringLiteral
1272 return [PDirective (DLib cgn lib)]
1273 <|> do try (lchar '%' *> reserved "link")
1274 cgn <- codegen_; obj <- fst <$> stringLiteral
1275 return [PDirective (DLink cgn obj)]
1276 <|> do try (lchar '%' *> reserved "flag")
1277 cgn <- codegen_; flag <- fst <$> stringLiteral
1278 return [PDirective (DFlag cgn flag)]
1279 <|> do try (lchar '%' *> reserved "include")
1280 cgn <- codegen_
1281 hdr <- fst <$> stringLiteral
1282 return [PDirective (DInclude cgn hdr)]
1283 <|> do try (lchar '%' *> reserved "hide"); n <- fst <$> fnName
1284 return [PDirective (DHide n)]
1285 <|> do try (lchar '%' *> reserved "freeze"); n <- fst <$> iName []
1286 return [PDirective (DFreeze n)]
1287 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1288 return [PDirective (DAccess acc)]
1289 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1290 i <- get
1291 put (i { default_total = tot } )
1292 return [PDirective (DDefault tot)]
1293 <|> do try (lchar '%' *> reserved "logging")
1294 i <- fst <$> natural
1295 return [PDirective (DLogging i)]
1296 <|> do try (lchar '%' *> reserved "dynamic")
1297 libs <- sepBy1 (fmap fst stringLiteral) (lchar ',')
1298 return [PDirective (DDynamicLibs libs)]
1299 <|> do try (lchar '%' *> reserved "name")
1300 (ty, tyFC) <- fnName
1301 ns <- sepBy1 name (lchar ',')
1302 return [PDirective (DNameHint ty tyFC ns)]
1303 <|> do try (lchar '%' *> reserved "error_handlers")
1304 (fn, nfc) <- fnName
1305 (arg, afc) <- fnName
1306 ns <- sepBy1 name (lchar ',')
1307 return [PDirective (DErrorHandlers fn nfc arg afc ns) ]
1308 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1309 return [PDirective (DLanguage ext)]
1310 <|> do fc <- getFC
1311 try (lchar '%' *> reserved "used")
1312 fn <- fst <$> fnName
1313 arg <- fst <$> iName []
1314 return [PDirective (DUsed fc fn arg)]
1315 <?> "directive"
1317pLangExt :: IdrisParser LanguageExt
1318pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1319 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1321{- | Parses a totality
1324Totality ::= 'partial' | 'total'
1328totality :: IdrisParser Bool
1329totality
1330 = do reservedHL "total"; return True
1331 <|> do reservedHL "partial"; return False
1333{- | Parses a type provider
1336Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1337ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1339 -}
1340provider :: SyntaxInfo -> IdrisParser [PDecl]
1341provider syn = do doc <- try (do (doc, _) <- docstring syn
1342 fc1 <- getFC
1343 lchar '%'
1344 fc2 <- reservedFC "provide"
1345 highlightP (spanFC fc1 fc2) AnnKeyword
1346 return doc)
1347 provideTerm doc <|> providePostulate doc
1348 <?> "type provider"
1349 where provideTerm doc =
1350 do lchar '('; (n, nfc) <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1351 fc <- getFC
1352 reservedHL "with"
1353 e <- expr syn <?> "provider expression"
1354 return [PProvider doc syn fc nfc (ProvTerm t e) n]
1355 providePostulate doc =
1356 do reservedHL "postulate"
1357 (n, nfc) <- fnName
1358 fc <- getFC
1359 reservedHL "with"
1360 e <- expr syn <?> "provider expression"
1361 return [PProvider doc syn fc nfc (ProvPostulate e) n]
1363{- | Parses a transform
1366Transform ::= '%' 'transform' Expr '==>' Expr
1369transform :: SyntaxInfo -> IdrisParser [PDecl]
1370transform syn = do try (lchar '%' *> reserved "transform")
1371 -- leave it unchecked, until we work out what this should
1372 -- actually mean...
1373-- safety <- option True (do reserved "unsafe"
1374-- return False)
1375 l <- expr syn
1376 fc <- getFC
1377 symbol "==>"
1378 r <- expr syn
1379 return [PTransform fc False l r]
1380 <?> "transform"
1382{- | Parses a top-level reflected elaborator script
1385RunElabDecl ::= '%' 'runElab' Expr
1388runElabDecl :: SyntaxInfo -> IdrisParser PDecl
1389runElabDecl syn =
1390 do kwFC <- try (do fc <- getFC
1391 lchar '%'
1392 fc' <- reservedFC "runElab"
1393 return (spanFC fc fc'))
1394 script <- expr syn <?> "elaborator script"
1395 highlightP kwFC AnnKeyword
1396 return $ PRunElabDecl kwFC script
1397 <?> "top-level elaborator script"
1399{- * Loading and parsing -}
1400{- | Parses an expression from input -}
1401parseExpr :: IState -> String -> Result PTerm
1402parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1404{- | Parses a constant form input -}
1405parseConst :: IState -> String -> Result Const
1406parseConst st = runparser (fmap fst constant) st "(input)"
1408{- | Parses a tactic from input -}
1409parseTactic :: IState -> String -> Result PTactic
1410parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1412{- | Parses a do-step from input (used in the elab shell) -}
1413parseElabShellStep :: IState -> String -> Result (Either ElabShellCmd PDo)
1414parseElabShellStep ist = runparser (fmap Right (do_ defaultSyntax) <|> fmap Left elabShellCmd) ist "(input)"
1415 where elabShellCmd = char ':' >>
1416 (reserved "qed" >> pure EQED ) <|>
1417 (reserved "abandon" >> pure EAbandon ) <|>
1418 (reserved "undo" >> pure EUndo ) <|>
1419 (reserved "state" >> pure EProofState) <|>
1420 (reserved "term" >> pure EProofTerm ) <|>
1421 (expressionTactic ["e", "eval"] EEval ) <|>
1422 (expressionTactic ["t", "type"] ECheck) <|>
1423 (expressionTactic ["search"] ESearch ) <|>
1424 (do reserved "doc"
1425 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)
1426 eof
1427 return (EDocStr doc))
1428 <?> "elab command"
1429 expressionTactic cmds tactic =
1430 do asum (map reserved cmds)
1431 t <- spaced (expr defaultSyntax)
1432 i <- get
1433 return $ tactic (desugar defaultSyntax i t)
1434 spaced parser = indentPropHolds gtProp *> parser
1436-- | Parse module header and imports
1437parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Delta)
1438parseImports fname input
1439 = do i <- getIState
1440 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1441 Failure err -> fail (show err)
1442 Success (x, annots, i) ->
1443 do putIState i
1444 fname' <- runIO $ Dir.makeAbsolute fname
1445 sendHighlighting $ addPath annots fname'
1446 return x
1447 where imports :: IdrisParser ((Maybe (Docstring ()), [String],
1448 [ImportInfo],
1449 Maybe Delta),
1450 [(FC, OutputAnnotation)], IState)
1451 imports = do whiteSpace
1452 (mdoc, mname, annots) <- moduleHeader
1453 ps <- many import_
1454 mrk <- mark
1455 isEof <- lookAheadMatches eof
1456 let mrk' = if isEof
1457 then Nothing
1458 else Just mrk
1459 i <- get
1460 return ((mdoc, mname, ps, mrk'), annots, i)
1461 addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]
1462 addPath [] _ = []
1463 addPath ((fc, AnnNamespace ns Nothing) : annots) path =
1464 (fc, AnnNamespace ns (Just path)) : addPath annots path
1465 addPath (annot:annots) path = annot : addPath annots path
1467-- | There should be a better way of doing this...
1468findFC :: Doc -> (FC, String)
1469findFC x = let s = show (plain x) in findFC' s
1470 where findFC' s = case span (/= ':') s of
1471 -- Horrid kludge to prevent crashes on Windows
1472 (prefix, ':':'\\':rest) ->
1473 case findFC' rest of
1474 (NoFC, msg) -> (NoFC, msg)
1475 (FileFC f, msg) -> (FileFC (prefix ++ ":\\" ++ f), msg)
1476 (FC f start end, msg) -> (FC (prefix ++ ":\\" ++ f) start end, msg)
1477 (failname, ':':rest) -> case span isDigit rest of
1478 (line, ':':rest') -> case span isDigit rest' of
1479 (col, ':':msg) -> let pos = (read line, read col) in
1480 (FC failname pos pos, msg)
1482-- | Check if the coloring matches the options and corrects if necessary
1483fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1484fixColour False doc = ANSI.plain doc
1485fixColour True doc = doc
1487-- | A program is a list of declarations, possibly with associated
1488-- documentation strings.
1489parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1490 Idris [PDecl]
1491parseProg syn fname input mrk
1492 = do i <- getIState
1493 case runparser mainProg i fname input of
1494 Failure doc -> do -- FIXME: Get error location from trifecta
1495 -- this can't be the solution!
1496 -- Issue #1575 on the issue tracker.
1497 -- https://github.com/idris-lang/Idris-dev/issues/1575
1498 let (fc, msg) = findFC doc
1499 i <- getIState
1500 case idris_outputmode i of
1501 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1502 IdeMode n h -> iWarn fc (P.text msg)
1503 putIState (i { errSpan = Just fc })
1504 return []
1505 Success (x, i) -> do putIState i
1506 reportParserWarnings
1507 return $ collect x
1508 where mainProg :: IdrisParser ([PDecl], IState)
1509 mainProg = case mrk of
1510 Nothing -> do i <- get; return ([], i)
1511 Just mrk -> do
1512 release mrk
1513 ds <- prog syn
1514 i' <- get
1515 return (ds, i')
1517{- | Load idris module and show error if something wrong happens -}
1518loadModule :: FilePath -> Idris (Maybe String)
1519loadModule f
1520 = idrisCatch (loadModule' f)
1521 (\e -> do setErrSpan (getErrSpan e)
1522 ist <- getIState
1523 iWarn (getErrSpan e) $ pprintErr ist e
1524 return Nothing)
1526{- | Load idris module -}
1527loadModule' :: FilePath -> Idris (Maybe String)
1528loadModule' f
1529 = do i <- getIState
1530 let file = takeWhile (/= ' ') f
1531 ibcsd <- valIBCSubDir i
1532 ids <- allImportDirs
1533 fp <- findImport ids ibcsd file
1534 if file `elem` imported i
1535 then do logLvl 1 $ "Already read " ++ file
1536 return Nothing
1537 else do putIState (i { imported = file : imported i })
1538 case fp of
1539 IDR fn -> loadSource False fn Nothing
1540 LIDR fn -> loadSource True fn Nothing
1541 IBC fn src ->
1542 idrisCatch (loadIBC True fn)
1543 (\c -> do logLvl 1 $ fn ++ " failed " ++ pshow i c
1544 case src of
1545 IDR sfn -> loadSource False sfn Nothing
1546 LIDR sfn -> loadSource True sfn Nothing)
1547 return $ Just file
1549{- | Load idris code from file -}
1550loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()
1551loadFromIFile reexp i@(IBC fn src) maxline
1552 = do logLvl 1 $ "Skipping " ++ getSrcFile i
1553 idrisCatch (loadIBC reexp fn)
1554 (\err -> ierror $ LoadingFailed fn err)
1555 where
1556 getSrcFile (IDR fn) = fn
1557 getSrcFile (LIDR fn) = fn
1558 getSrcFile (IBC f src) = getSrcFile src
1560loadFromIFile _ (IDR fn) maxline = loadSource' False fn maxline
1561loadFromIFile _ (LIDR fn) maxline = loadSource' True fn maxline
1563{-| Load idris source code and show error if something wrong happens -}
1564loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1565loadSource' lidr r maxline
1566 = idrisCatch (loadSource lidr r maxline)
1567 (\e -> do setErrSpan (getErrSpan e)
1568 ist <- getIState
1569 case e of
1570 At f e' -> iWarn f (pprintErr ist e')
1571 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1573{- | Load Idris source code-}
1574loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1575loadSource lidr f toline
1576 = do logLvl 1 ("Reading " ++ f)
1577 i <- getIState
1578 let def_total = default_total i
1579 file_in <- runIO $ readSource f
1580 file <- if lidr then tclift $ unlit f file_in else return file_in
1581 (mdocs, mname, imports_in, pos) <- parseImports f file
1582 ai <- getAutoImports
1583 let imports = map (\n -> ImportInfo True n Nothing [] NoFC NoFC) ai ++ imports_in
1584 ids <- allImportDirs
1585 ibcsd <- valIBCSubDir i
1586 mapM_ (\(re, f, ns, nfc) ->
1587 do fp <- findImport ids ibcsd f
1588 case fp of
1589 LIDR fn -> ifail $ "No ibc for " ++ f
1590 IDR fn -> ifail $ "No ibc for " ++ f
1591 IBC fn src ->
1592 do loadIBC True fn
1593 let srcFn = case src of
1594 IDR fn -> Just fn
1595 LIDR fn -> Just fn
1596 _ -> Nothing
1597 srcFnAbs <- case srcFn of
1598 Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)
1599 Nothing -> return Nothing
1600 sendHighlighting [(nfc, AnnNamespace ns srcFnAbs)])
1601 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]
1602 reportParserWarnings
1603 sendParserHighlighting
1605 -- process and check module aliases
1606 let modAliases = M.fromList
1607 [ (prep alias, prep realName)
1608 | ImportInfo { import_reexport = reexport
1609 , import_path = realName
1610 , import_rename = Just (alias, _)
1611 , import_location = fc } <- imports
1613 prep = map T.pack . reverse . Spl.splitOn [pathSeparator]
1614 aliasNames = [ (alias, fc)
1615 | ImportInfo { import_rename = Just (alias, _)
1616 , import_location = fc } <- imports
1618 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1619 case map head . filter ((/= 1) . length) $ histogram of
1620 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1621 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1623 i <- getIState
1624 putIState (i { default_access = Hidden, module_aliases = modAliases })
1625 clearIBC -- start a new .ibc file
1626 -- record package info in .ibc
1627 imps <- allImportDirs
1628 mapM_ addIBC (map IBCImportDir imps)
1629 mapM_ (addIBC . IBCImport)
1630 [ (reexport, realName)
1631 | ImportInfo { import_reexport = reexport
1632 , import_path = realName
1633 } <- imports
1635 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1636 maxline = toline }
1637 ist <- getIState
1638 -- Save the span from parsing the module header, because
1639 -- an empty program parse might obliterate it.
1640 let oldSpan = idris_parsedSpan ist
1641 ds' <- parseProg syntax f file pos
1643 case (ds', oldSpan) of
1644 ([], Just fc) ->
1645 -- If no program elements were parsed, we dind't
1646 -- get a loaded region in the IBC file. That
1647 -- means we need to add it back.
1648 do ist <- getIState
1649 putIState ist { idris_parsedSpan = oldSpan
1650 , ibc_write = IBCParsedRegion fc :
1651 ibc_write ist
1653 _ -> return ()
1654 sendParserHighlighting
1656 -- Parsing done, now process declarations
1658 let ds = namespaces mname ds'
1659 logLvl 3 (show $ showDecls verbosePPOption ds)
1660 i <- getIState
1661 logLvl 10 (show (toAlist (idris_implicits i)))
1662 logLvl 3 (show (idris_infixes i))
1663 -- Now add all the declarations to the context
1664 v <- verbose
1665 when v $ iputStrLn $ "Type checking " ++ f
1666 -- we totality check after every Mutual block, so if
1667 -- anything is a single definition, wrap it in a
1668 -- mutual block on its own
1669 elabDecls toplevel (map toMutual ds)
1670 i <- getIState
1671 -- simplify every definition do give the totality checker
1672 -- a better chance
1673 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1674 ctxt' <-
1675 do ctxt <- getContext
1676 tclift $ simplifyCasedef n (getErasureInfo i) ctxt
1677 setContext ctxt')
1678 (map snd (idris_totcheck i))
1679 -- build size change graph from simplified definitions
1680 logLvl 1 "Totality checking"
1681 i <- getIState
1682 mapM_ buildSCG (idris_totcheck i)
1683 mapM_ checkDeclTotality (idris_totcheck i)
1685 -- Redo totality check for deferred names
1686 let deftots = idris_defertotcheck i
1687 logLvl 1 $ "Totality checking " ++ show deftots
1688 mapM_ (\x -> do tot <- getTotality x
1689 case tot of
1690 Total _ -> setTotality x Unchecked
1691 _ -> return ()) (map snd deftots)
1692 mapM_ buildSCG deftots
1693 mapM_ checkDeclTotality deftots
1695 logLvl 1 ("Finished " ++ f)
1696 ibcsd <- valIBCSubDir i
1697 logLvl 1 "Universe checking"
1698 iucheck
1699 let ibc = ibcPathNoFallback ibcsd f
1700 i <- getIState
1701 addHides (hide_list i)
1703 -- Save module documentation if applicable
1704 i <- getIState
1705 case mdocs of
1706 Nothing -> return ()
1707 Just docs -> addModDoc syntax mname docs
1710 -- Finally, write an ibc and highlights if checking was successful
1711 ok <- noErrors
1712 when ok $
1713 do idrisCatch (do writeIBC f ibc; clearIBC)
1714 (\c -> return ()) -- failure is harmless
1715 hl <- getDumpHighlighting
1716 when hl $
1717 idrisCatch (writeHighlights f)
1718 (const $ return ()) -- failure is harmless
1719 clearHighlights
1720 i <- getIState
1721 putIState (i { default_total = def_total,
1722 hide_list = [] })
1723 return ()
1724 where
1725 namespaces :: [String] -> [PDecl] -> [PDecl]
1726 namespaces [] ds = ds
1727 namespaces (x:xs) ds = [PNamespace x NoFC (namespaces xs ds)]
1729 toMutual :: PDecl -> PDecl
1730 toMutual m@(PMutual _ d) = m
1731 toMutual (PNamespace x fc ds) = PNamespace x fc (map toMutual ds)
1732 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1733 case x of
1734 PClauses{} -> r
1735 PClass{} -> r
1736 PData{} -> r
1737 PInstance{} -> r
1738 _ -> x
1740 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1741 addModDoc syn mname docs =
1742 do ist <- getIState
1743 docs' <- elabDocTerms recinfo (parsedDocs ist)
1744 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1745 putIState ist { idris_moduledocs = modDocs' }
1746 addIBC (IBCModDocs docName)
1747 where
1748 docName = NS modDocName (map T.pack (reverse mname))
1749 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1751{- | Adds names to hide list -}
1752addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1753addHides xs = do i <- getIState
1754 let defh = default_access i
1755 let (hs, as) = partition isNothing xs
1756 unless (null as) $
1757 mapM_ doHide
1758 (map (\ (n, _) -> (n, defh)) hs ++
1759 map (\ (n, Just a) -> (n, a)) as)
1760 where isNothing (_, Nothing) = True
1761 isNothing _ = False
1763 doHide (n, a) = do setAccessibility n a
1764 addIBC (IBCAccess n a)