git.iko.soy/Idris-dev
on cb005bc help sign in
Idris-dev/src/Idris/Parser.hs
1408 lines 51 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 Text.Trifecta.Delta
12import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)
13import Text.Parser.LookAhead
14import Text.Parser.Expression
15import qualified Text.Parser.Token as Tok
16import qualified Text.Parser.Char as Chr
17import qualified Text.Parser.Token.Highlight as Hi
19import Text.PrettyPrint.ANSI.Leijen (Doc, plain)
20import qualified Text.PrettyPrint.ANSI.Leijen as ANSI
22import Idris.AbsSyntax hiding (namespace, params)
23import Idris.DSL
24import Idris.Imports
25import Idris.Delaborate
26import Idris.Error
27import Idris.Elab.Value
28import Idris.ElabDecls
29import Idris.ElabTerm
30import Idris.Coverage
31import Idris.IBC
32import Idris.Unlit
33import Idris.Providers
34import Idris.Output
36import Idris.ParseHelpers
37import Idris.ParseOps
38import Idris.ParseExpr
39import Idris.ParseData
41import Idris.Docstrings hiding (Unchecked)
43import Paths_idris
45import Util.DynamicLinker
46import qualified Util.Pretty as P
48import Idris.Core.TT
49import Idris.Core.Evaluate
51import Control.Applicative hiding (Const)
52import Control.Monad
53import Control.Monad.State.Strict
55import Data.Function
56import Data.Maybe
57import qualified Data.List.Split as Spl
58import Data.List
59import Data.Monoid
60import Data.Char
61import Data.Ord
62import qualified Data.Map as M
63import qualified Data.HashSet as HS
64import qualified Data.Text as T
65import qualified Data.ByteString.UTF8 as UTF8
66import qualified Data.Set as S
68import Debug.Trace
70import System.FilePath
71import System.IO
73{-
75 grammar shortcut notation:
76 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)
77 RULE? = optional rule (i.e. RULE or nothing)
78 RULE* = repeated rule (i.e. RULE zero or more times)
79 RULE+ = repeated rule with at least one match (i.e. RULE one or more times)
80 RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)
81 RULE{n} = rule repeated n times
83-}
85{- * Main grammar -}
87{- | Parses module definition
90 ModuleHeader ::= 'module' Identifier_t ';'?;
92-}
93moduleHeader :: IdrisParser (Maybe (Docstring ()), [String])
94moduleHeader = try (do docs <- optional docComment
95 noArgs docs
96 reserved "module"
97 i <- identifier
98 option ';' (lchar ';')
99 return (fmap fst docs, moduleName i))
100 <|> try (do lchar '%'; reserved "unqualified"
101 return (Nothing, []))
102 <|> return (Nothing, moduleName "Main")
103 where moduleName x = case span (/='.') x of
104 (x, "") -> [x]
105 (x, '.':y) -> x : moduleName y
106 noArgs (Just (_, args)) | not (null args) = fail "Modules do not take arguments"
107 noArgs _ = return ()
109{- | Parses an import statement
112 Import ::= 'import' Identifier_t ';'?;
114 -}
115import_ :: IdrisParser (Bool, String, Maybe String, FC)
116import_ = do fc <- getFC
117 reserved "import"
118 reexport <- option False (do reserved "public"; return True)
119 id <- identifier
120 newName <- optional (reserved "as" *> identifier)
121 option ';' (lchar ';')
122 return (reexport, toPath id, toPath <$> newName, fc)
123 <?> "import statement"
124 where toPath = foldl1' (</>) . Spl.splitOn "."
126{- | Parses program source
129 Prog ::= Decl* EOF;
131 -}
132prog :: SyntaxInfo -> IdrisParser [PDecl]
133prog syn = do whiteSpace
134 decls <- many (decl syn)
135 let c = (concat decls)
136 case maxline syn of
137 Nothing -> do notOpenBraces; eof
138 _ -> return ()
139 ist <- get
140 fc <- getFC
141 put ist { idris_parsedSpan = Just (FC (fc_fname fc) (0,0) (fc_end fc)),
142 ibc_write = IBCParsedRegion fc : ibc_write ist }
143 return c
145{-| Parses a top-level declaration
148Decl ::=
149 Decl'
150 | Using
151 | Params
152 | Mutual
153 | Namespace
154 | Class
155 | Instance
156 | DSL
157 | Directive
158 | Provider
159 | Transform
160 | Import!
161 ;
163-}
164decl :: SyntaxInfo -> IdrisParser [PDecl]
165decl syn = do fc <- getFC
166 -- if we're after maxline, stop here
167 let continue = case maxline syn of
168 Nothing -> True
169 Just l -> if fst (fc_end fc) > l
170 then mut_nesting syn /= 0
171 else True
172 if continue then do notEndBlock
173 declBody
174 else fail "End of readable input"
175 where declBody :: IdrisParser [PDecl]
176 declBody = declBody'
177 <|> using_ syn
178 <|> params syn
179 <|> mutual syn
180 <|> namespace syn
181 <|> class_ syn
182 <|> instance_ syn
183 <|> do d <- dsl syn; return [d]
184 <|> directive syn
185 <|> provider syn
186 <|> transform syn
187 <|> do import_; fail "imports must be at top of file"
188 <?> "declaration"
189 declBody' :: IdrisParser [PDecl]
190 declBody' = do d <- decl' syn
191 i <- get
192 let d' = fmap (debindApp syn . (desugar syn i)) d
193 return [d']
195{- | Parses a top-level declaration with possible syntax sugar
198Decl' ::=
199 Fixity
200 | FunDecl'
201 | Data
202 | Record
203 | SyntaxDecl
204 ;
206-}
207decl' :: SyntaxInfo -> IdrisParser PDecl
208decl' syn = fixity
209 <|> syntaxDecl syn
210 <|> fnDecl' syn
211 <|> data_ syn
212 <|> record syn
213 <?> "declaration"
215{- | Parses a syntax extension declaration (and adds the rule to parser state)
218 SyntaxDecl ::= SyntaxRule;
220-}
221syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
222syntaxDecl syn = do s <- syntaxRule syn
223 i <- get
224 put (i `addSyntax` s)
225 fc <- getFC
226 return (PSyntax fc s)
228-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.
229addSyntax :: IState -> Syntax -> IState
230addSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
231 syntax_keywords = ks ++ ns,
232 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc }
233 where rs = syntax_rules i
234 ns = syntax_keywords i
235 ibc = ibc_write i
236 ks = map show (syntaxNames s)
238-- | Like 'addSyntax', but no effect on the IBC.
239addReplSyntax :: IState -> Syntax -> IState
240addReplSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
241 syntax_keywords = ks ++ ns }
242 where rs = syntax_rules i
243 ns = syntax_keywords i
244 ks = map show (syntaxNames s)
246{- | Parses a syntax extension declaration
249SyntaxRuleOpts ::= 'term' | 'pattern';
253SyntaxRule ::=
254 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
258SyntaxSym ::= '[' Name_t ']'
259 | '{' Name_t '}'
260 | Name_t
261 | StringLiteral_t
262 ;
264-}
265syntaxRule :: SyntaxInfo -> IdrisParser Syntax
266syntaxRule syn
267 = do sty <- try (do
268 pushIndent
269 sty <- option AnySyntax (do reserved "term"; return TermSyntax
270 <|> do reserved "pattern"; return PatternSyntax)
271 reserved "syntax"
272 return sty)
273 syms <- some syntaxSym
274 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
275 let ns = mapMaybe getName syms
276 when (length ns /= length (nub ns))
277 $ unexpected "repeated variable in syntax rule"
278 lchar '='
279 tm <- typeExpr (allowImp syn)
280 terminator
281 return (Rule (mkSimple syms) tm sty)
282 where
283 isExpr (Expr _) = True
284 isExpr _ = False
285 getName (Expr n) = Just n
286 getName _ = Nothing
287 -- Can't parse two full expressions (i.e. expressions with application) in a row
288 -- so change them both to a simple expression
289 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
290 mkSimple xs = mkSimple' xs
292 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
293 mkSimple es
294 mkSimple' (e : es) = e : mkSimple' es
295 mkSimple' [] = []
298{- | Parses a syntax symbol (either binding variable, keyword or expression)
301SyntaxSym ::= '[' Name_t ']'
302 | '{' Name_t '}'
303 | Name_t
304 | StringLiteral_t
305 ;
307 -}
308syntaxSym :: IdrisParser SSymbol
309syntaxSym = try (do lchar '['; n <- name; lchar ']'
310 return (Expr n))
311 <|> try (do lchar '{'; n <- name; lchar '}'
312 return (Binding n))
313 <|> do n <- iName []
314 return (Keyword n)
315 <|> do sym <- stringLiteral
316 return (Symbol sym)
317 <?> "syntax symbol"
319{- | Parses a function declaration with possible syntax sugar
322 FunDecl ::= FunDecl';
324-}
325fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
326fnDecl syn = try (do notEndBlock
327 d <- fnDecl' syn
328 i <- get
329 let d' = fmap (desugar syn i) d
330 return [d']) <?> "function declaration"
332{-| Parses a function declaration
335 FunDecl' ::=
336 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
337 | Postulate
338 | Pattern
339 | CAF
340 ;
342-}
343fnDecl' :: SyntaxInfo -> IdrisParser PDecl
344fnDecl' syn = checkFixity $
345 do (doc, argDocs, fc, opts', n, acc) <- try (do
346 pushIndent
347 (doc, argDocs) <- option noDocs docComment
348 ist <- get
349 let doc' = annotCode (tryFullExpr syn ist) doc
350 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
351 | (n, d) <- argDocs ]
353 initOpts = if default_total ist
354 then [TotalFn]
355 else []
356 opts <- fnOpts initOpts
357 acc <- optional accessibility
358 opts' <- fnOpts opts
359 n_in <- fnName
360 let n = expandNS syn n_in
361 fc <- getFC
362 lchar ':'
363 return (doc', argDocs', fc, opts', n, acc))
364 ty <- typeExpr (allowImp syn)
365 terminator
366 addAcc n acc
367 return (PTy doc argDocs syn fc opts' n ty)
368 <|> postulate syn
369 <|> caf syn
370 <|> pattern syn
371 <?> "function declaration"
372 where checkFixity :: IdrisParser PDecl -> IdrisParser PDecl
373 checkFixity p = do decl <- p
374 case getName decl of
375 Nothing -> return decl
376 Just n -> do fOk <- fixityOK n
377 unless fOk . fail $
378 "Missing fixity declaration for " ++ show n
379 return decl
380 getName (PTy _ _ _ _ _ n _) = Just n
381 getName _ = Nothing
382 fixityOK (NS n _) = fixityOK n
383 fixityOK (UN n) | all (flip elem opChars) (str n) =
384 do fixities <- fmap idris_infixes get
385 return . elem (str n) . map (\ (Fix _ op) -> op) $ fixities
386 | otherwise = return True
387 fixityOK _ = return True
389{-| Parses function options given initial options
392FnOpts ::= 'total'
393 | 'partial'
394 | 'implicit'
395 | '%' 'no_implicit'
396 | '%' 'assert_total'
397 | '%' 'error_handler'
398 | '%' 'reflection'
399 | '%' 'specialise' '[' NameTimesList? ']'
400 ;
404NameTimes ::= FnName Natural?;
408NameTimesList ::=
409 NameTimes
410 | NameTimes ',' NameTimesList
411 ;
413-}
414-- FIXME: Check compatability for function options (i.e. partal/total)
415--
416-- Issue #1574 on the issue tracker.
417-- https://github.com/idris-lang/Idris-dev/issues/1574
418fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
419fnOpts opts
420 = do reserved "total"; fnOpts (TotalFn : opts)
421 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
422 <|> do reserved "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))
423 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;
424 fnOpts (CExport c : opts)
425 <|> do try (lchar '%' *> reserved "no_implicit");
426 fnOpts (NoImplicit : opts)
427 <|> do try (lchar '%' *> reserved "inline");
428 fnOpts (Inlinable : opts)
429 <|> do try (lchar '%' *> reserved "assert_total");
430 fnOpts (AssertTotal : opts)
431 <|> do try (lchar '%' *> reserved "error_handler");
432 fnOpts (ErrorHandler : opts)
433 <|> do try (lchar '%' *> reserved "error_reverse");
434 fnOpts (ErrorReverse : opts)
435 <|> do try (lchar '%' *> reserved "reflection");
436 fnOpts (Reflection : opts)
437 <|> do lchar '%'; reserved "specialise";
438 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
439 fnOpts (Specialise ns : opts)
440 <|> do reserved "implicit"; fnOpts (Implicit : opts)
441 <|> return opts
442 <?> "function modifier"
443 where nameTimes :: IdrisParser (Name, Maybe Int)
444 nameTimes = do n <- fnName
445 t <- option Nothing (do reds <- natural
446 return (Just (fromInteger reds)))
447 return (n, t)
449{- | Parses a postulate
452Postulate ::=
453 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
454 ;
456-}
457postulate :: SyntaxInfo -> IdrisParser PDecl
458postulate syn = do doc <- try $ do (doc, _) <- option noDocs docComment
459 ist <- get
460 let doc' = annotCode (tryFullExpr syn ist) doc
461 pushIndent
462 reserved "postulate"
463 return doc'
464 ist <- get
465 let initOpts = if default_total ist
466 then [TotalFn]
467 else []
468 opts <- fnOpts initOpts
469 acc <- optional accessibility
470 opts' <- fnOpts opts
471 n_in <- fnName
472 let n = expandNS syn n_in
473 lchar ':'
474 ty <- typeExpr (allowImp syn)
475 fc <- getFC
476 terminator
477 addAcc n acc
478 return (PPostulate doc syn fc opts' n ty)
479 <?> "postulate"
481{- | Parses a using declaration
484Using ::=
485 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
486 ;
488 -}
489using_ :: SyntaxInfo -> IdrisParser [PDecl]
490using_ syn =
491 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
492 openBlock
493 let uvars = using syn
494 ds <- many (decl (syn { using = uvars ++ ns }))
495 closeBlock
496 return (concat ds)
497 <?> "using declaration"
499{- | Parses a parameters declaration
502Params ::=
503 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
504 ;
506 -}
507params :: SyntaxInfo -> IdrisParser [PDecl]
508params syn =
509 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
510 openBlock
511 let pvars = syn_params syn
512 ds <- many (decl syn { syn_params = pvars ++ ns })
513 closeBlock
514 fc <- getFC
515 return [PParams fc ns (concat ds)]
516 <?> "parameters declaration"
518{- | Parses a mutual declaration (for mutually recursive functions)
521Mutual ::=
522 'mutual' OpenBlock Decl* CloseBlock
523 ;
525-}
526mutual :: SyntaxInfo -> IdrisParser [PDecl]
527mutual syn =
528 do reserved "mutual"
529 openBlock
530 let pvars = syn_params syn
531 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
532 closeBlock
533 fc <- getFC
534 return [PMutual fc (concat ds)]
535 <?> "mutual block"
537{-| Parses a namespace declaration
540Namespace ::=
541 'namespace' identifier OpenBlock Decl+ CloseBlock
542 ;
544-}
545namespace :: SyntaxInfo -> IdrisParser [PDecl]
546namespace syn =
547 do reserved "namespace"; n <- identifier;
548 openBlock
549 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
550 closeBlock
551 return [PNamespace n (concat ds)]
552 <?> "namespace declaration"
554{- | Parses a methods block (for instances)
557 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
559-}
560instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
561instanceBlock syn = do reserved "where"
562 openBlock
563 ds <- many (fnDecl syn)
564 closeBlock
565 return (concat ds)
566 <?> "instance block"
568{- | Parses a methods and instances block (for type classes)
571MethodOrInstance ::=
572 FnDecl
573 | Instance
574 ;
578ClassBlock ::=
579 'where' OpenBlock MethodOrInstance* CloseBlock
580 ;
582-}
583classBlock :: SyntaxInfo -> IdrisParser [PDecl]
584classBlock syn = do reserved "where"
585 openBlock
586 ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)
587 closeBlock
588 return (concat ds)
589 <?> "class block"
591{-| Parses a type class declaration
594ClassArgument ::=
595 Name
596 | '(' Name ':' Expr ')'
597 ;
601Class ::=
602 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
603 ;
605-}
606class_ :: SyntaxInfo -> IdrisParser [PDecl]
607class_ syn = do (doc, argDocs, acc) <- try (do
608 (doc, argDocs) <- option noDocs docComment
609 ist <- get
610 let doc' = annotCode (tryFullExpr syn ist) doc
611 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
612 | (n, d) <- argDocs ]
613 acc <- optional accessibility
614 return (doc', argDocs', acc))
615 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName
616 let n = expandNS syn n_in
617 cs <- many carg
618 ds <- option [] (classBlock syn)
619 accData acc n (concatMap declared ds)
620 return [PClass doc syn fc cons n cs argDocs ds]
621 <?> "type-class declaration"
622 where
623 carg :: IdrisParser (Name, PTerm)
624 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
625 return (i, ty)
626 <|> do i <- name;
627 return (i, PType)
629{- | Parses a type class instance declaration
632 Instance ::=
633 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
634 ;
638InstanceName ::= '[' Name ']';
640-}
641instance_ :: SyntaxInfo -> IdrisParser [PDecl]
642instance_ syn = do reserved "instance"; fc <- getFC
643 en <- optional instanceName
644 cs <- constraintList syn
645 cn <- fnName
646 args <- many (simpleExpr syn)
647 let sc = PApp fc (PRef fc cn) (map pexp args)
648 let t = bindList (PPi constraint) cs sc
649 ds <- option [] (instanceBlock syn)
650 return [PInstance syn fc cs cn args t en ds]
651 <?> "instance declaration"
652 where instanceName :: IdrisParser Name
653 instanceName = do lchar '['; n_in <- fnName; lchar ']'
654 let n = expandNS syn n_in
655 return n
656 <?> "instance name"
659{- | Parses a using declaration list
662UsingDeclList ::=
663 UsingDeclList'
664 | NameList TypeSig
665 ;
669UsingDeclList' ::=
670 UsingDecl
671 | UsingDecl ',' UsingDeclList'
672 ;
676NameList ::=
677 Name
678 | Name ',' NameList
679 ;
681-}
682usingDeclList :: SyntaxInfo -> IdrisParser [Using]
683usingDeclList syn
684 = try (sepBy1 (usingDecl syn) (lchar ','))
685 <|> do ns <- sepBy1 name (lchar ',')
686 lchar ':'
687 t <- typeExpr (disallowImp syn)
688 return (map (\x -> UImplicit x t) ns)
689 <?> "using declaration list"
691{- |Parses a using declaration
694UsingDecl ::=
695 FnName TypeSig
696 | FnName FnName+
697 ;
699-}
700usingDecl :: SyntaxInfo -> IdrisParser Using
701usingDecl syn = try (do x <- fnName
702 lchar ':'
703 t <- typeExpr (disallowImp syn)
704 return (UImplicit x t))
705 <|> do c <- fnName
706 xs <- some fnName
707 return (UConstraint c xs)
708 <?> "using declaration"
710{- | Parse a clause with patterns
713Pattern ::= Clause;
715-}
716pattern :: SyntaxInfo -> IdrisParser PDecl
717pattern syn = do fc <- getFC
718 clause <- clause syn
719 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
720 <?> "pattern"
722{- | Parse a constant applicative form declaration
725CAF ::= 'let' FnName '=' Expr Terminator;
727-}
728caf :: SyntaxInfo -> IdrisParser PDecl
729caf syn = do reserved "let"
730 n_in <- fnName; let n = expandNS syn n_in
731 lchar '='
732 t <- expr syn
733 terminator
734 fc <- getFC
735 return (PCAF fc n t)
736 <?> "constant applicative form declaration"
738{- | Parse an argument expression
741ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
743-}
744argExpr :: SyntaxInfo -> IdrisParser PTerm
745argExpr syn = let syn' = syn { inPattern = True } in
746 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
747 <?> "argument expression"
749{- | Parse a right hand side of a function
752RHS ::= '=' Expr
753 | '?=' RHSName? Expr
754 | 'impossible'
755 ;
759RHSName ::= '{' FnName '}';
761-}
762rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
763rhs syn n = do lchar '='; expr syn
764 <|> do symbol "?=";
765 fc <- getFC
766 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
767 return n)
768 r <- expr syn
769 return (addLet fc name r)
770 <|> do reserved "impossible"; return PImpossible
771 <?> "function right hand side"
772 where mkN :: Name -> Name
773 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
774 then sUN "infix_op_lemma_1"
775 else sUN (str x++"_lemma_1")
776 mkN (NS x n) = NS (mkN x) n
777 n' :: Name
778 n' = mkN n
779 addLet :: FC -> Name -> PTerm -> PTerm
780 addLet fc nm (PLet fc' n ty val r) = PLet fc' n ty val (addLet fc nm r)
781 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)
782 where addLetC (l, r) = (l, addLet fc nm r)
783 addLet fc nm r = (PLet fc (sUN "value") Placeholder r (PMetavar nm))
785{- |Parses a function clause
788RHSOrWithBlock ::= RHS WhereOrTerminator
789 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
790 ;
794Clause ::= WExpr+ RHSOrWithBlock
795 | SimpleExpr '<==' FnName RHS WhereOrTerminator
796 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
797 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
798 ;
802ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
806WhereOrTerminator ::= WhereBlock | Terminator;
808-}
809clause :: SyntaxInfo -> IdrisParser PClause
810clause syn
811 = do wargs <- try (do pushIndent; some (wExpr syn))
812 fc <- getFC
813 ist <- get
814 n <- case lastParse ist of
815 Just t -> return t
816 Nothing -> fail "Invalid clause"
817 (do r <- rhs syn n
818 let ctxt = tt_ctxt ist
819 let wsyn = syn { syn_namespace = [] }
820 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
821 popIndent
822 return x,
823 do terminator
824 return ([], [])]
825 return $ PClauseR fc wargs r wheres) <|> (do
826 popIndent
827 reserved "with"
828 wval <- simpleExpr syn
829 openBlock
830 ds <- some $ fnDecl syn
831 let withs = concat ds
832 closeBlock
833 return $ PWithR fc wargs wval withs)
834 <|> do ty <- try (do pushIndent
835 ty <- simpleExpr syn
836 symbol "<=="
837 return ty)
838 fc <- getFC
839 n_in <- fnName; let n = expandNS syn n_in
840 r <- rhs syn n
841 ist <- get
842 let ctxt = tt_ctxt ist
843 let wsyn = syn { syn_namespace = [] }
844 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
845 popIndent
846 return x,
847 do terminator
848 return ([], [])]
849 let capp = PLet fc (sMN 0 "match")
850 ty
851 (PMatchApp fc n)
852 (PRef fc (sMN 0 "match"))
853 ist <- get
854 put (ist { lastParse = Just n })
855 return $ PClause fc n capp [] r wheres
856 <|> do (l, op) <- try (do
857 pushIndent
858 l <- argExpr syn
859 op <- operator
860 when (op == "=" || op == "?=" ) $
861 fail "infix clause definition with \"=\" and \"?=\" not supported "
862 return (l, op))
863 let n = expandNS syn (sUN op)
864 r <- argExpr syn
865 fc <- getFC
866 wargs <- many (wExpr syn)
867 (do rs <- rhs syn n
868 let wsyn = syn { syn_namespace = [] }
869 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
870 popIndent
871 return x,
872 do terminator
873 return ([], [])]
874 ist <- get
875 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
876 put (ist { lastParse = Just n })
877 return $ PClause fc n capp wargs rs wheres) <|> (do
878 popIndent
879 reserved "with"
880 wval <- bracketed syn
881 openBlock
882 ds <- some $ fnDecl syn
883 closeBlock
884 ist <- get
885 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
886 let withs = map (fillLHSD n capp wargs) $ concat ds
887 put (ist { lastParse = Just n })
888 return $ PWith fc n capp wargs wval withs)
889 <|> do pushIndent
890 n_in <- fnName; let n = expandNS syn n_in
891 cargs <- many (constraintArg syn)
892 fc <- getFC
893 args <- many (try (implicitArg (syn { inPattern = True } ))
894 <|> (fmap pexp (argExpr syn)))
895 wargs <- many (wExpr syn)
896 let capp = PApp fc (PRef fc n)
897 (cargs ++ args)
898 (do r <- rhs syn n
899 ist <- get
900 let ctxt = tt_ctxt ist
901 let wsyn = syn { syn_namespace = [] }
902 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
903 popIndent
904 return x,
905 do terminator
906 return ([], [])]
907 ist <- get
908 put (ist { lastParse = Just n })
909 return $ PClause fc n capp wargs r wheres) <|> (do
910 reserved "with"
911 ist <- get
912 put (ist { lastParse = Just n })
913 wval <- bracketed syn
914 openBlock
915 ds <- some $ fnDecl syn
916 let withs = map (fillLHSD n capp wargs) $ concat ds
917 closeBlock
918 popIndent
919 return $ PWith fc n capp wargs wval withs)
920 <?> "function clause"
921 where
922 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
923 fillLHS n capp owargs (PClauseR fc wargs v ws)
924 = PClause fc n capp (owargs ++ wargs) v ws
925 fillLHS n capp owargs (PWithR fc wargs v ws)
926 = PWith fc n capp (owargs ++ wargs) v
927 (map (fillLHSD n capp (owargs ++ wargs)) ws)
928 fillLHS _ _ _ c = c
930 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
931 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
932 fillLHSD n c a x = x
934{-| Parses with pattern
937WExpr ::= '|' Expr';
939-}
940wExpr :: SyntaxInfo -> IdrisParser PTerm
941wExpr syn = do lchar '|'
942 expr' (syn { inPattern = True })
943 <?> "with pattern"
945{- | Parses a where block
948WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
950-}
951whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
952whereBlock n syn
953 = do reserved "where"
954 ds <- indentedBlock1 (decl syn)
955 let dns = concatMap (concatMap declared) ds
956 return (concat ds, map (\x -> (x, decoration syn x)) dns)
957 <?> "where block"
959{- |Parses a code generation target language name
962Codegen ::= 'C'
963 | 'Java'
964 | 'JavaScript'
965 | 'Node'
966 | 'LLVM'
967 | 'Bytecode'
968 ;
970-}
971codegen_ :: IdrisParser Codegen
972codegen_ = do n <- identifier; return (Via (map toLower n))
973 <|> do reserved "Bytecode"; return Bytecode
974 <?> "code generation language"
976{- |Parses a compiler directive
978StringList ::=
979 String
980 | String ',' StringList
981 ;
985Directive ::= '%' Directive';
989Directive' ::= 'lib' CodeGen String_t
990 | 'link' CodeGen String_t
991 | 'flag' CodeGen String_t
992 | 'include' CodeGen String_t
993 | 'hide' Name
994 | 'freeze' Name
995 | 'access' Accessibility
996 | 'default' Totality
997 | 'logging' Natural
998 | 'dynamic' StringList
999 | 'name' Name NameList
1000 | 'error_handlers' Name NameList
1001 | 'language' 'TypeProviders'
1002 | 'language' 'ErrorReflection'
1006directive :: SyntaxInfo -> IdrisParser [PDecl]
1007directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
1008 return [PDirective (do addLib cgn lib
1009 addIBC (IBCLib cgn lib))]
1010 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
1011 return [PDirective (do dirs <- allImportDirs
1012 o <- liftIO $ findInPath dirs obj
1013 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
1014 addObjectFile cgn o)]
1015 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
1016 flag <- stringLiteral
1017 return [PDirective (do addIBC (IBCCGFlag cgn flag)
1018 addFlag cgn flag)]
1019 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
1020 return [PDirective (do addHdr cgn hdr
1021 addIBC (IBCHeader cgn hdr))]
1022 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
1023 return [PDirective (do setAccessibility n Hidden
1024 addIBC (IBCAccess n Hidden))]
1025 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
1026 return [PDirective (do setAccessibility n Frozen
1027 addIBC (IBCAccess n Frozen))]
1028 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1029 return [PDirective (do i <- get
1030 put(i { default_access = acc }))]
1031 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1032 i <- get
1033 put (i { default_total = tot } )
1034 return [PDirective (do i <- get
1035 put(i { default_total = tot }))]
1036 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
1037 return [PDirective (setLogLevel (fromInteger i))]
1038 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
1039 return [PDirective (do added <- addDyLib libs
1040 case added of
1041 Left lib -> addIBC (IBCDyLib (lib_name lib))
1042 Right msg ->
1043 fail $ msg)]
1044 <|> do try (lchar '%' *> reserved "name")
1045 ty <- fnName
1046 ns <- sepBy1 name (lchar ',')
1047 return [PDirective (do ty' <- disambiguate ty
1048 mapM_ (addNameHint ty') ns
1049 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1050 <|> do try (lchar '%' *> reserved "error_handlers")
1051 fn <- fnName
1052 arg <- fnName
1053 ns <- sepBy1 name (lchar ',')
1054 return [PDirective (do fn' <- disambiguate fn
1055 ns' <- mapM disambiguate ns
1056 addFunctionErrorHandlers fn' arg ns'
1057 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]
1058 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1059 return [PDirective (addLangExt ext)]
1060 <|> do fc <- getFC
1061 try (lchar '%' *> reserved "used")
1062 fn <- fnName
1063 arg <- iName []
1064 return [PDirective (addUsedName fc fn arg)]
1066 <?> "directive"
1067 where disambiguate :: Name -> Idris Name
1068 disambiguate n = do i <- getIState
1069 case lookupCtxtName n (idris_implicits i) of
1070 [(n', _)] -> return n'
1071 [] -> throwError (NoSuchVariable n)
1072 more -> throwError (CantResolveAlts (map fst more))
1074pLangExt :: IdrisParser LanguageExt
1075pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1076 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1078{- | Parses a totality
1081Totality ::= 'partial' | 'total'
1085totality :: IdrisParser Bool
1086totality
1087 = do reserved "total"; return True
1088 <|> do reserved "partial"; return False
1090{- | Parses a type provider
1093Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1094ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1096 -}
1097provider :: SyntaxInfo -> IdrisParser [PDecl]
1098provider syn = do try (lchar '%' *> reserved "provide");
1099 provideTerm <|> providePostulate
1100 <?> "type provider"
1101 where provideTerm = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1102 fc <- getFC
1103 reserved "with"
1104 e <- expr syn <?> "provider expression"
1105 return [PProvider syn fc (ProvTerm t e) n]
1106 providePostulate = do reserved "postulate"
1107 n <- fnName
1108 fc <- getFC
1109 reserved "with"
1110 e <- expr syn <?> "provider expression"
1111 return [PProvider syn fc (ProvPostulate e) n]
1113{- | Parses a transform
1116Transform ::= '%' 'transform' Expr '==>' Expr
1119transform :: SyntaxInfo -> IdrisParser [PDecl]
1120transform syn = do try (lchar '%' *> reserved "transform")
1121 -- leave it unchecked, until we work out what this should
1122 -- actually mean...
1123-- safety <- option True (do reserved "unsafe"
1124-- return False)
1125 l <- expr syn
1126 fc <- getFC
1127 symbol "==>"
1128 r <- expr syn
1129 return [PTransform fc False l r]
1130 <?> "transform"
1133{- * Loading and parsing -}
1134{- | Parses an expression from input -}
1135parseExpr :: IState -> String -> Result PTerm
1136parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1138{- | Parses a constant form input -}
1139parseConst :: IState -> String -> Result Const
1140parseConst st = runparser constant st "(input)"
1142{- | Parses a tactic from input -}
1143parseTactic :: IState -> String -> Result PTactic
1144parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1146-- | Parse module header and imports
1147parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta)
1148parseImports fname input
1149 = do i <- getIState
1150 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1151 Failure err -> fail (show err)
1152 Success (x, i) -> do putIState i
1153 return x
1154 where imports :: IdrisParser ((Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta), IState)
1155 imports = do whiteSpace
1156 (mdoc, mname) <- moduleHeader
1157 ps <- many import_
1158 mrk <- mark
1159 isEof <- lookAheadMatches eof
1160 let mrk' = if isEof
1161 then Nothing
1162 else Just mrk
1163 i <- get
1164 return ((mdoc, mname, ps, mrk'), i)
1166-- | There should be a better way of doing this...
1167findFC :: Doc -> (FC, String)
1168findFC x = let s = show (plain x) in
1169 case span (/= ':') s of
1170 (failname, ':':rest) -> case span isDigit rest of
1171 (line, ':':rest') -> case span isDigit rest' of
1172 (col, ':':msg) -> let pos = (read line, read col) in
1173 (FC failname pos pos, msg)
1175-- | Check if the coloring matches the options and corrects if necessary
1176fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1177fixColour False doc = ANSI.plain doc
1178fixColour True doc = doc
1180-- | A program is a list of declarations, possibly with associated
1181-- documentation strings.
1182parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1183 Idris [PDecl]
1184parseProg syn fname input mrk
1185 = do i <- getIState
1186 case runparser mainProg i fname input of
1187 Failure doc -> do -- FIXME: Get error location from trifecta
1188 -- this can't be the solution!
1189 -- Issue #1575 on the issue tracker.
1190 -- https://github.com/idris-lang/Idris-dev/issues/1575
1191 let (fc, msg) = findFC doc
1192 i <- getIState
1193 case idris_outputmode i of
1194 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1195 IdeSlave n h -> iWarn fc (P.text msg)
1196 putIState (i { errSpan = Just fc })
1197 return []
1198 Success (x, i) -> do putIState i
1199 reportParserWarnings
1200 return $ collect x
1201 where mainProg :: IdrisParser ([PDecl], IState)
1202 mainProg = case mrk of
1203 Nothing -> do i <- get; return ([], i)
1204 Just mrk -> do
1205 release mrk
1206 ds <- prog syn
1207 i' <- get
1208 return (ds, i')
1210{- | Load idris module and show error if something wrong happens -}
1211loadModule :: FilePath -> Idris (Maybe String)
1212loadModule f
1213 = idrisCatch (loadModule' f)
1214 (\e -> do setErrSpan (getErrSpan e)
1215 ist <- getIState
1216 iWarn (getErrSpan e) $ pprintErr ist e
1217 return Nothing)
1219{- | Load idris module -}
1220loadModule' :: FilePath -> Idris (Maybe String)
1221loadModule' f
1222 = do i <- getIState
1223 let file = takeWhile (/= ' ') f
1224 ibcsd <- valIBCSubDir i
1225 ids <- allImportDirs
1226 fp <- findImport ids ibcsd file
1227 if file `elem` imported i
1228 then do iLOG $ "Already read " ++ file
1229 return Nothing
1230 else do putIState (i { imported = file : imported i })
1231 case fp of
1232 IDR fn -> loadSource False fn Nothing
1233 LIDR fn -> loadSource True fn Nothing
1234 IBC fn src ->
1235 idrisCatch (loadIBC True fn)
1236 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1237 case src of
1238 IDR sfn -> loadSource False sfn Nothing
1239 LIDR sfn -> loadSource True sfn Nothing)
1240 return $ Just file
1242{- | Load idris code from file -}
1243loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()
1244loadFromIFile reexp i@(IBC fn src) maxline
1245 = do iLOG $ "Skipping " ++ getSrcFile i
1246 idrisCatch (loadIBC reexp fn)
1247 (\err -> ierror $ LoadingFailed fn err)
1248 where
1249 getSrcFile (IDR fn) = fn
1250 getSrcFile (LIDR fn) = fn
1251 getSrcFile (IBC f src) = getSrcFile src
1253loadFromIFile _ (IDR fn) maxline = loadSource' False fn maxline
1254loadFromIFile _ (LIDR fn) maxline = loadSource' True fn maxline
1256{-| Load idris source code and show error if something wrong happens -}
1257loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1258loadSource' lidr r maxline
1259 = idrisCatch (loadSource lidr r maxline)
1260 (\e -> do setErrSpan (getErrSpan e)
1261 ist <- getIState
1262 case e of
1263 At f e' -> iWarn f (pprintErr ist e')
1264 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1266{- | Load Idris source code-}
1267loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1268loadSource lidr f toline
1269 = do iLOG ("Reading " ++ f)
1270 i <- getIState
1271 let def_total = default_total i
1272 file_in <- runIO $ readFile f
1273 file <- if lidr then tclift $ unlit f file_in else return file_in
1274 (mdocs, mname, imports_in, pos) <- parseImports f file
1275 ai <- getAutoImports
1276 let imports = map (\n -> (True, n, Just n, emptyFC)) ai ++ imports_in
1277 ids <- allImportDirs
1278 ibcsd <- valIBCSubDir i
1279 mapM_ (\(re, f) ->
1280 do fp <- findImport ids ibcsd f
1281 case fp of
1282 LIDR fn -> ifail $ "No ibc for " ++ f
1283 IDR fn -> ifail $ "No ibc for " ++ f
1284 IBC fn src -> loadIBC True fn)
1285 [(re, fn) | (re, fn, _, _) <- imports]
1286 reportParserWarnings
1288 -- process and check module aliases
1289 let modAliases = M.fromList
1290 [(prep alias, prep realName) | (reexport, realName, Just alias, fc) <- imports]
1291 prep = map T.pack . reverse . Spl.splitOn "/"
1292 aliasNames = [(alias, fc) | (_, _, Just alias, fc) <- imports]
1293 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1294 case map head . filter ((/= 1) . length) $ histogram of
1295 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1296 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1298 i <- getIState
1299 putIState (i { default_access = Hidden, module_aliases = modAliases })
1300 clearIBC -- start a new .ibc file
1301 -- record package info in .ibc
1302 imps <- allImportDirs
1303 mapM_ addIBC (map IBCImportDir imps)
1304 mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports]
1305 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1306 maxline = toline }
1307 ds' <- parseProg syntax f file pos
1309 -- Parsing done, now process declarations
1311 let ds = namespaces mname ds'
1312 logLvl 3 (show $ showDecls verbosePPOption ds)
1313 i <- getIState
1314 logLvl 10 (show (toAlist (idris_implicits i)))
1315 logLvl 3 (show (idris_infixes i))
1316 -- Now add all the declarations to the context
1317 v <- verbose
1318 when v $ iputStrLn $ "Type checking " ++ f
1319 -- we totality check after every Mutual block, so if
1320 -- anything is a single definition, wrap it in a
1321 -- mutual block on its own
1322 elabDecls toplevel (map toMutual ds)
1323 i <- getIState
1324 -- simplify every definition do give the totality checker
1325 -- a better chance
1326 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1327 updateContext (simplifyCasedef n $ getErasureInfo i))
1328 (map snd (idris_totcheck i))
1329 -- build size change graph from simplified definitions
1330 iLOG "Totality checking"
1331 i <- getIState
1332 mapM_ buildSCG (idris_totcheck i)
1333 mapM_ checkDeclTotality (idris_totcheck i)
1335 -- Redo totality check for deferred names
1336 let deftots = idris_defertotcheck i
1337 iLOG $ "Totality checking " ++ show deftots
1338 mapM_ (\x -> do tot <- getTotality x
1339 case tot of
1340 Total _ -> setTotality x Unchecked
1341 _ -> return ()) (map snd deftots)
1342 mapM_ buildSCG deftots
1343 mapM_ checkDeclTotality deftots
1345 iLOG ("Finished " ++ f)
1346 ibcsd <- valIBCSubDir i
1347 iLOG "Universe checking"
1348 iucheck
1349 let ibc = ibcPathNoFallback ibcsd f
1350 i <- getIState
1351 addHides (hide_list i)
1353 -- Save module documentation if applicable
1354 i <- getIState
1355 case mdocs of
1356 Nothing -> return ()
1357 Just docs -> addModDoc syntax mname docs
1360 -- Finally, write an ibc if checking was successful
1361 ok <- noErrors
1362 when ok $
1363 idrisCatch (do writeIBC f ibc; clearIBC)
1364 (\c -> return ()) -- failure is harmless
1365 i <- getIState
1366 putIState (i { default_total = def_total,
1367 hide_list = [] })
1368 return ()
1369 where
1370 namespaces :: [String] -> [PDecl] -> [PDecl]
1371 namespaces [] ds = ds
1372 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1374 toMutual :: PDecl -> PDecl
1375 toMutual m@(PMutual _ d) = m
1376 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1377 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1378 case x of
1379 PClauses _ _ _ _ -> r
1380 PClass _ _ _ _ _ _ _ _ -> r
1381 PInstance _ _ _ _ _ _ _ _ -> r
1382 _ -> x
1384 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
1385 addModDoc syn mname docs =
1386 do ist <- getIState
1387 docs' <- elabDocTerms recinfo (parsedDocs ist)
1388 let modDocs' = addDef docName docs' (idris_moduledocs ist)
1389 putIState ist { idris_moduledocs = modDocs' }
1390 addIBC (IBCModDocs docName)
1391 where
1392 docName = NS modDocName (map T.pack (reverse mname))
1393 parsedDocs ist = annotCode (tryFullExpr syn ist) docs
1395{- | Adds names to hide list -}
1396addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1397addHides xs = do i <- getIState
1398 let defh = default_access i
1399 let (hs, as) = partition isNothing xs
1400 unless (null as) $
1401 mapM_ doHide
1402 (map (\ (n, _) -> (n, defh)) hs ++
1403 map (\ (n, Just a) -> (n, a)) as)
1404 where isNothing (_, Nothing) = True
1405 isNothing _ = False
1407 doHide (n, a) = do setAccessibility n a
1408 addIBC (IBCAccess n a)