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