git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/src/Idris/Parser.hs
1378 lines 49 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.ElabDecls
28import Idris.ElabTerm
29import Idris.Coverage
30import Idris.IBC
31import Idris.Unlit
32import Idris.Providers
33import Idris.Output
35import Idris.ParseHelpers
36import Idris.ParseOps
37import Idris.ParseExpr
38import Idris.ParseData
40import Idris.Docstrings
42import Paths_idris
44import Util.DynamicLinker
45import qualified Util.Pretty as P
47import Idris.Core.TT
48import Idris.Core.Evaluate
50import Control.Applicative hiding (Const)
51import Control.Monad
52import Control.Monad.Error (throwError, catchError)
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 [String]
94moduleHeader = try (do noDocCommentHere "Modules cannot have documentation comments"
95 reserved "module"
96 i <- identifier
97 option ';' (lchar ';')
98 return (moduleName i))
99 <|> try (do lchar '%'; reserved "unqualified"
100 return [])
101 <|> return (moduleName "Main")
102 where moduleName x = case span (/='.') x of
103 (x, "") -> [x]
104 (x, '.':y) -> x : moduleName y
106{- | Parses an import statement
109 Import ::= 'import' Identifier_t ';'?;
111 -}
112import_ :: IdrisParser (String, Maybe String, FC)
113import_ = do fc <- getFC
114 reserved "import"
115 id <- identifier
116 newName <- optional (reserved "as" *> identifier)
117 option ';' (lchar ';')
118 return (toPath id, toPath <$> newName, fc)
119 <?> "import statement"
120 where toPath = foldl1' (</>) . Spl.splitOn "."
122{- | Parses program source
125 Prog ::= Decl* EOF;
127 -}
128prog :: SyntaxInfo -> IdrisParser [PDecl]
129prog syn = do whiteSpace
130 decls <- many (decl syn)
131 let c = (concat decls)
132 case maxline syn of
133 Nothing -> do notOpenBraces; eof
134 _ -> return ()
135 ist <- get
136 fc <- getFC
137 put ist { idris_parsedSpan = Just (FC (fc_fname fc) (0,0) (fc_end fc)),
138 ibc_write = IBCParsedRegion fc : ibc_write ist }
139 return c
141{-| Parses a top-level declaration
144Decl ::=
145 Decl'
146 | Using
147 | Params
148 | Mutual
149 | Namespace
150 | Class
151 | Instance
152 | DSL
153 | Directive
154 | Provider
155 | Transform
156 | Import!
157 ;
159-}
160decl :: SyntaxInfo -> IdrisParser [PDecl]
161decl syn = do fc <- getFC
162 -- if we're after maxline, stop here
163 let continue = case maxline syn of
164 Nothing -> True
165 Just l -> if fst (fc_end fc) > l
166 then mut_nesting syn /= 0
167 else True
168 if continue then do notEndBlock
169 declBody
170 else fail "End of readable input"
171 where declBody :: IdrisParser [PDecl]
172 declBody = declBody'
173 <|> using_ syn
174 <|> params syn
175 <|> mutual syn
176 <|> namespace syn
177 <|> class_ syn
178 <|> instance_ syn
179 <|> do d <- dsl syn; return [d]
180 <|> directive syn
181 <|> provider syn
182 <|> transform syn
183 <|> do import_; fail "imports must be at top of file"
184 <?> "declaration"
185 declBody' :: IdrisParser [PDecl]
186 declBody' = do d <- decl' syn
187 i <- get
188 let d' = fmap (debindApp syn . (desugar syn i)) d
189 return [d']
191{- | Parses a top-level declaration with possible syntax sugar
194Decl' ::=
195 Fixity
196 | FunDecl'
197 | Data
198 | Record
199 | SyntaxDecl
200 ;
202-}
203decl' :: SyntaxInfo -> IdrisParser PDecl
204decl' syn = fixity
205 <|> syntaxDecl syn
206 <|> fnDecl' syn
207 <|> data_ syn
208 <|> record syn
209 <?> "declaration"
211{- | Parses a syntax extension declaration (and adds the rule to parser state)
214 SyntaxDecl ::= SyntaxRule;
216-}
217syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
218syntaxDecl syn = do s <- syntaxRule syn
219 i <- get
220 put (i `addSyntax` s)
221 fc <- getFC
222 return (PSyntax fc s)
224-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.
225addSyntax :: IState -> Syntax -> IState
226addSyntax i s = i { syntax_rules = s : rs,
227 syntax_keywords = ks ++ ns,
228 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc }
229 where rs = syntax_rules i
230 ns = syntax_keywords i
231 ibc = ibc_write i
232 ks = map show (syntaxNames s)
234-- | Like 'addSyntax', but no effect on the IBC.
235addReplSyntax :: IState -> Syntax -> IState
236addReplSyntax i s = i { syntax_rules = s : rs,
237 syntax_keywords = ks ++ ns }
238 where rs = syntax_rules i
239 ns = syntax_keywords i
240 ks = map show (syntaxNames s)
242{- | Parses a syntax extension declaration
245SyntaxRuleOpts ::= 'term' | 'pattern';
249SyntaxRule ::=
250 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
254SyntaxSym ::= '[' Name_t ']'
255 | '{' Name_t '}'
256 | Name_t
257 | StringLiteral_t
258 ;
260-}
261syntaxRule :: SyntaxInfo -> IdrisParser Syntax
262syntaxRule syn
263 = do sty <- try (do
264 pushIndent
265 sty <- option AnySyntax (do reserved "term"; return TermSyntax
266 <|> do reserved "pattern"; return PatternSyntax)
267 reserved "syntax"
268 return sty)
269 syms <- some syntaxSym
270 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
271 let ns = mapMaybe getName syms
272 when (length ns /= length (nub ns))
273 $ unexpected "repeated variable in syntax rule"
274 lchar '='
275 tm <- typeExpr (allowImp syn)
276 terminator
277 return (Rule (mkSimple syms) tm sty)
278 where
279 isExpr (Expr _) = True
280 isExpr _ = False
281 getName (Expr n) = Just n
282 getName _ = Nothing
283 -- Can't parse two full expressions (i.e. expressions with application) in a row
284 -- so change them both to a simple expression
285 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
286 mkSimple xs = mkSimple' xs
288 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
289 mkSimple es
290 mkSimple' (e : es) = e : mkSimple' es
291 mkSimple' [] = []
294{- | Parses a syntax symbol (either binding variable, keyword or expression)
297SyntaxSym ::= '[' Name_t ']'
298 | '{' Name_t '}'
299 | Name_t
300 | StringLiteral_t
301 ;
303 -}
304syntaxSym :: IdrisParser SSymbol
305syntaxSym = try (do lchar '['; n <- name; lchar ']'
306 return (Expr n))
307 <|> try (do lchar '{'; n <- name; lchar '}'
308 return (Binding n))
309 <|> do n <- iName []
310 return (Keyword n)
311 <|> do sym <- stringLiteral
312 return (Symbol sym)
313 <?> "syntax symbol"
315{- | Parses a function declaration with possible syntax sugar
318 FunDecl ::= FunDecl';
320-}
321fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
322fnDecl syn = try (do notEndBlock
323 d <- fnDecl' syn
324 i <- get
325 let d' = fmap (desugar syn i) d
326 return [d']) <?> "function declaration"
328{-| Parses a function declaration
331 FunDecl' ::=
332 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
333 | Postulate
334 | Pattern
335 | CAF
336 ;
338-}
339fnDecl' :: SyntaxInfo -> IdrisParser PDecl
340fnDecl' syn = checkFixity $
341 do (doc, argDocs, fc, opts', n, acc) <- try (do
342 pushIndent
343 (doc, argDocs) <- option noDocs docComment
344 ist <- get
345 let doc' = annotCode (tryFullExpr syn ist) doc
346 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
347 | (n, d) <- argDocs ]
349 initOpts = if default_total ist
350 then [TotalFn]
351 else []
352 opts <- fnOpts initOpts
353 acc <- optional accessibility
354 opts' <- fnOpts opts
355 n_in <- fnName
356 let n = expandNS syn n_in
357 fc <- getFC
358 lchar ':'
359 return (doc', argDocs', fc, opts', n, acc))
360 ty <- typeExpr (allowImp syn)
361 terminator
362 addAcc n acc
363 return (PTy doc argDocs syn fc opts' n ty)
364 <|> postulate syn
365 <|> caf syn
366 <|> pattern syn
367 <?> "function declaration"
368 where checkFixity :: IdrisParser PDecl -> IdrisParser PDecl
369 checkFixity p = do decl <- p
370 case getName decl of
371 Nothing -> return decl
372 Just n -> do fOk <- fixityOK n
373 unless fOk . fail $
374 "Missing fixity declaration for " ++ show n
375 return decl
376 getName (PTy _ _ _ _ _ n _) = Just n
377 getName _ = Nothing
378 fixityOK (NS n _) = fixityOK n
379 fixityOK (UN n) | all (flip elem opChars) (str n) =
380 do fixities <- fmap idris_infixes get
381 return . elem (str n) . map (\ (Fix _ op) -> op) $ fixities
382 | otherwise = return True
383 fixityOK _ = return True
385{-| Parses function options given initial options
388FnOpts ::= 'total'
389 | 'partial'
390 | 'implicit'
391 | '%' 'no_implicit'
392 | '%' 'assert_total'
393 | '%' 'error_handler'
394 | '%' 'reflection'
395 | '%' 'specialise' '[' NameTimesList? ']'
396 ;
400NameTimes ::= FnName Natural?;
404NameTimesList ::=
405 NameTimes
406 | NameTimes ',' NameTimesList
407 ;
409-}
410-- FIXME: Check compatability for function options (i.e. partal/total)
411--
412-- Issue #1574 on the issue tracker.
413-- https://github.com/idris-lang/Idris-dev/issues/1574
414fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
415fnOpts opts
416 = do reserved "total"; fnOpts (TotalFn : opts)
417 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
418 <|> do reserved "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))
419 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;
420 fnOpts (CExport c : opts)
421 <|> do try (lchar '%' *> reserved "no_implicit");
422 fnOpts (NoImplicit : opts)
423 <|> do try (lchar '%' *> reserved "assert_total");
424 fnOpts (AssertTotal : opts)
425 <|> do try (lchar '%' *> reserved "error_handler");
426 fnOpts (ErrorHandler : opts)
427 <|> do try (lchar '%' *> reserved "error_reverse");
428 fnOpts (ErrorReverse : opts)
429 <|> do try (lchar '%' *> reserved "reflection");
430 fnOpts (Reflection : opts)
431 <|> do lchar '%'; reserved "specialise";
432 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
433 fnOpts (Specialise ns : opts)
434 <|> do reserved "implicit"; fnOpts (Implicit : opts)
435 <|> return opts
436 <?> "function modifier"
437 where nameTimes :: IdrisParser (Name, Maybe Int)
438 nameTimes = do n <- fnName
439 t <- option Nothing (do reds <- natural
440 return (Just (fromInteger reds)))
441 return (n, t)
443{- | Parses a postulate
446Postulate ::=
447 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
448 ;
450-}
451postulate :: SyntaxInfo -> IdrisParser PDecl
452postulate syn = do doc <- try $ do (doc, _) <- option noDocs docComment
453 ist <- get
454 let doc' = annotCode (tryFullExpr syn ist) doc
455 pushIndent
456 reserved "postulate"
457 return doc'
458 ist <- get
459 let initOpts = if default_total ist
460 then [TotalFn]
461 else []
462 opts <- fnOpts initOpts
463 acc <- optional accessibility
464 opts' <- fnOpts opts
465 n_in <- fnName
466 let n = expandNS syn n_in
467 lchar ':'
468 ty <- typeExpr (allowImp syn)
469 fc <- getFC
470 terminator
471 addAcc n acc
472 return (PPostulate doc syn fc opts' n ty)
473 <?> "postulate"
475{- | Parses a using declaration
478Using ::=
479 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
480 ;
482 -}
483using_ :: SyntaxInfo -> IdrisParser [PDecl]
484using_ syn =
485 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
486 openBlock
487 let uvars = using syn
488 ds <- many (decl (syn { using = uvars ++ ns }))
489 closeBlock
490 return (concat ds)
491 <?> "using declaration"
493{- | Parses a parameters declaration
496Params ::=
497 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
498 ;
500 -}
501params :: SyntaxInfo -> IdrisParser [PDecl]
502params syn =
503 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
504 openBlock
505 let pvars = syn_params syn
506 ds <- many (decl syn { syn_params = pvars ++ ns })
507 closeBlock
508 fc <- getFC
509 return [PParams fc ns (concat ds)]
510 <?> "parameters declaration"
512{- | Parses a mutual declaration (for mutually recursive functions)
515Mutual ::=
516 'mutual' OpenBlock Decl* CloseBlock
517 ;
519-}
520mutual :: SyntaxInfo -> IdrisParser [PDecl]
521mutual syn =
522 do reserved "mutual"
523 openBlock
524 let pvars = syn_params syn
525 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
526 closeBlock
527 fc <- getFC
528 return [PMutual fc (concat ds)]
529 <?> "mutual block"
531{-| Parses a namespace declaration
534Namespace ::=
535 'namespace' identifier OpenBlock Decl+ CloseBlock
536 ;
538-}
539namespace :: SyntaxInfo -> IdrisParser [PDecl]
540namespace syn =
541 do reserved "namespace"; n <- identifier;
542 openBlock
543 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
544 closeBlock
545 return [PNamespace n (concat ds)]
546 <?> "namespace declaration"
548{- | Parses a methods block (for instances)
551 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
553-}
554instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
555instanceBlock syn = do reserved "where"
556 openBlock
557 ds <- many (fnDecl syn)
558 closeBlock
559 return (concat ds)
560 <?> "instance block"
562{- | Parses a methods and instances block (for type classes)
565MethodOrInstance ::=
566 FnDecl
567 | Instance
568 ;
572ClassBlock ::=
573 'where' OpenBlock MethodOrInstance* CloseBlock
574 ;
576-}
577classBlock :: SyntaxInfo -> IdrisParser [PDecl]
578classBlock syn = do reserved "where"
579 openBlock
580 ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)
581 closeBlock
582 return (concat ds)
583 <?> "class block"
585{-| Parses a type class declaration
588ClassArgument ::=
589 Name
590 | '(' Name ':' Expr ')'
591 ;
595Class ::=
596 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
597 ;
599-}
600class_ :: SyntaxInfo -> IdrisParser [PDecl]
601class_ syn = do (doc, argDocs, acc) <- try (do
602 (doc, argDocs) <- option noDocs docComment
603 ist <- get
604 let doc' = annotCode (tryFullExpr syn ist) doc
605 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
606 | (n, d) <- argDocs ]
607 acc <- optional accessibility
608 return (doc', argDocs', acc))
609 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName
610 let n = expandNS syn n_in
611 cs <- many carg
612 ds <- option [] (classBlock syn)
613 accData acc n (concatMap declared ds)
614 return [PClass doc syn fc cons n cs argDocs ds]
615 <?> "type-class declaration"
616 where
617 carg :: IdrisParser (Name, PTerm)
618 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
619 return (i, ty)
620 <|> do i <- name;
621 return (i, PType)
623{- | Parses a type class instance declaration
626 Instance ::=
627 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
628 ;
632InstanceName ::= '[' Name ']';
634-}
635instance_ :: SyntaxInfo -> IdrisParser [PDecl]
636instance_ syn = do reserved "instance"; fc <- getFC
637 en <- optional instanceName
638 cs <- constraintList syn
639 cn <- fnName
640 args <- many (simpleExpr syn)
641 let sc = PApp fc (PRef fc cn) (map pexp args)
642 let t = bindList (PPi constraint)
643 (map (\x -> (sMN 0 "constraint", x)) cs) sc
644 ds <- option [] (instanceBlock syn)
645 return [PInstance syn fc cs cn args t en ds]
646 <?> "instance declaration"
647 where instanceName :: IdrisParser Name
648 instanceName = do lchar '['; n_in <- fnName; lchar ']'
649 let n = expandNS syn n_in
650 return n
651 <?> "instance name"
654{- | Parses a using declaration list
657UsingDeclList ::=
658 UsingDeclList'
659 | NameList TypeSig
660 ;
664UsingDeclList' ::=
665 UsingDecl
666 | UsingDecl ',' UsingDeclList'
667 ;
671NameList ::=
672 Name
673 | Name ',' NameList
674 ;
676-}
677usingDeclList :: SyntaxInfo -> IdrisParser [Using]
678usingDeclList syn
679 = try (sepBy1 (usingDecl syn) (lchar ','))
680 <|> do ns <- sepBy1 name (lchar ',')
681 lchar ':'
682 t <- typeExpr (disallowImp syn)
683 return (map (\x -> UImplicit x t) ns)
684 <?> "using declaration list"
686{- |Parses a using declaration
689UsingDecl ::=
690 FnName TypeSig
691 | FnName FnName+
692 ;
694-}
695usingDecl :: SyntaxInfo -> IdrisParser Using
696usingDecl syn = try (do x <- fnName
697 lchar ':'
698 t <- typeExpr (disallowImp syn)
699 return (UImplicit x t))
700 <|> do c <- fnName
701 xs <- some fnName
702 return (UConstraint c xs)
703 <?> "using declaration"
705{- | Parse a clause with patterns
708Pattern ::= Clause;
710-}
711pattern :: SyntaxInfo -> IdrisParser PDecl
712pattern syn = do fc <- getFC
713 clause <- clause syn
714 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
715 <?> "pattern"
717{- | Parse a constant applicative form declaration
720CAF ::= 'let' FnName '=' Expr Terminator;
722-}
723caf :: SyntaxInfo -> IdrisParser PDecl
724caf syn = do reserved "let"
725 n_in <- fnName; let n = expandNS syn n_in
726 lchar '='
727 t <- expr syn
728 terminator
729 fc <- getFC
730 return (PCAF fc n t)
731 <?> "constant applicative form declaration"
733{- | Parse an argument expression
736ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
738-}
739argExpr :: SyntaxInfo -> IdrisParser PTerm
740argExpr syn = let syn' = syn { inPattern = True } in
741 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
742 <?> "argument expression"
744{- | Parse a right hand side of a function
747RHS ::= '=' Expr
748 | '?=' RHSName? Expr
749 | 'impossible'
750 ;
754RHSName ::= '{' FnName '}';
756-}
757rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
758rhs syn n = do lchar '='; expr syn
759 <|> do symbol "?=";
760 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
761 return n)
762 r <- expr syn
763 return (addLet name r)
764 <|> do reserved "impossible"; return PImpossible
765 <?> "function right hand side"
766 where mkN :: Name -> Name
767 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
768 then sUN "infix_op_lemma_1"
769 else sUN (str x++"_lemma_1")
770 mkN (NS x n) = NS (mkN x) n
771 n' :: Name
772 n' = mkN n
773 addLet :: Name -> PTerm -> PTerm
774 addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)
775 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
776 where addLetC (l, r) = (l, addLet nm r)
777 addLet nm r = (PLet (sUN "value") Placeholder r (PMetavar nm))
779{- |Parses a function clause
782RHSOrWithBlock ::= RHS WhereOrTerminator
783 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
784 ;
788Clause ::= WExpr+ RHSOrWithBlock
789 | SimpleExpr '<==' FnName RHS WhereOrTerminator
790 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
791 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
792 ;
796ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
800WhereOrTerminator ::= WhereBlock | Terminator;
802-}
803clause :: SyntaxInfo -> IdrisParser PClause
804clause syn
805 = do wargs <- try (do pushIndent; some (wExpr syn))
806 fc <- getFC
807 ist <- get
808 n <- case lastParse ist of
809 Just t -> return t
810 Nothing -> fail "Invalid clause"
811 (do r <- rhs syn n
812 let ctxt = tt_ctxt ist
813 let wsyn = syn { syn_namespace = [] }
814 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
815 popIndent
816 return x,
817 do terminator
818 return ([], [])]
819 return $ PClauseR fc wargs r wheres) <|> (do
820 popIndent
821 reserved "with"
822 wval <- simpleExpr syn
823 openBlock
824 ds <- some $ fnDecl syn
825 let withs = concat ds
826 closeBlock
827 return $ PWithR fc wargs wval withs)
828 <|> do ty <- try (do pushIndent
829 ty <- simpleExpr syn
830 symbol "<=="
831 return ty)
832 fc <- getFC
833 n_in <- fnName; let n = expandNS syn n_in
834 r <- rhs syn n
835 ist <- get
836 let ctxt = tt_ctxt ist
837 let wsyn = syn { syn_namespace = [] }
838 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
839 popIndent
840 return x,
841 do terminator
842 return ([], [])]
843 let capp = PLet (sMN 0 "match")
844 ty
845 (PMatchApp fc n)
846 (PRef fc (sMN 0 "match"))
847 ist <- get
848 put (ist { lastParse = Just n })
849 return $ PClause fc n capp [] r wheres
850 <|> do (l, op) <- try (do
851 pushIndent
852 l <- argExpr syn
853 op <- operator
854 when (op == "=" || op == "?=" ) $
855 fail "infix clause definition with \"=\" and \"?=\" not supported "
856 return (l, op))
857 let n = expandNS syn (sUN op)
858 r <- argExpr syn
859 fc <- getFC
860 wargs <- many (wExpr syn)
861 (do rs <- rhs syn n
862 let wsyn = syn { syn_namespace = [] }
863 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
864 popIndent
865 return x,
866 do terminator
867 return ([], [])]
868 ist <- get
869 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
870 put (ist { lastParse = Just n })
871 return $ PClause fc n capp wargs rs wheres) <|> (do
872 popIndent
873 reserved "with"
874 wval <- bracketed syn
875 openBlock
876 ds <- some $ fnDecl syn
877 closeBlock
878 ist <- get
879 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
880 let withs = map (fillLHSD n capp wargs) $ concat ds
881 put (ist { lastParse = Just n })
882 return $ PWith fc n capp wargs wval withs)
883 <|> do pushIndent
884 n_in <- fnName; let n = expandNS syn n_in
885 cargs <- many (constraintArg syn)
886 fc <- getFC
887 args <- many (try (implicitArg (syn { inPattern = True } ))
888 <|> (fmap pexp (argExpr syn)))
889 wargs <- many (wExpr syn)
890 let capp = PApp fc (PRef fc n)
891 (cargs ++ args)
892 (do r <- rhs syn n
893 ist <- get
894 let ctxt = tt_ctxt ist
895 let wsyn = syn { syn_namespace = [] }
896 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
897 popIndent
898 return x,
899 do terminator
900 return ([], [])]
901 ist <- get
902 put (ist { lastParse = Just n })
903 return $ PClause fc n capp wargs r wheres) <|> (do
904 reserved "with"
905 ist <- get
906 put (ist { lastParse = Just n })
907 wval <- bracketed syn
908 openBlock
909 ds <- some $ fnDecl syn
910 let withs = map (fillLHSD n capp wargs) $ concat ds
911 closeBlock
912 popIndent
913 return $ PWith fc n capp wargs wval withs)
914 <?> "function clause"
915 where
916 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
917 fillLHS n capp owargs (PClauseR fc wargs v ws)
918 = PClause fc n capp (owargs ++ wargs) v ws
919 fillLHS n capp owargs (PWithR fc wargs v ws)
920 = PWith fc n capp (owargs ++ wargs) v
921 (map (fillLHSD n capp (owargs ++ wargs)) ws)
922 fillLHS _ _ _ c = c
924 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
925 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
926 fillLHSD n c a x = x
928{-| Parses with pattern
931WExpr ::= '|' Expr';
933-}
934wExpr :: SyntaxInfo -> IdrisParser PTerm
935wExpr syn = do lchar '|'
936 expr' syn
937 <?> "with pattern"
939{- | Parses a where block
942WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
944-}
945whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
946whereBlock n syn
947 = do reserved "where"
948 ds <- indentedBlock1 (decl syn)
949 let dns = concatMap (concatMap declared) ds
950 return (concat ds, map (\x -> (x, decoration syn x)) dns)
951 <?> "where block"
953{- |Parses a code generation target language name
956Codegen ::= 'C'
957 | 'Java'
958 | 'JavaScript'
959 | 'Node'
960 | 'LLVM'
961 | 'Bytecode'
962 ;
964-}
965codegen_ :: IdrisParser Codegen
966codegen_ = do n <- identifier; return (Via (map toLower n))
967 <|> do reserved "Bytecode"; return Bytecode
968 <?> "code generation language"
970{- |Parses a compiler directive
972StringList ::=
973 String
974 | String ',' StringList
975 ;
979Directive ::= '%' Directive';
983Directive' ::= 'lib' CodeGen String_t
984 | 'link' CodeGen String_t
985 | 'flag' CodeGen String_t
986 | 'include' CodeGen String_t
987 | 'hide' Name
988 | 'freeze' Name
989 | 'access' Accessibility
990 | 'default' Totality
991 | 'logging' Natural
992 | 'dynamic' StringList
993 | 'name' Name NameList
994 | 'error_handlers' Name NameList
995 | 'language' 'TypeProviders'
996 | 'language' 'ErrorReflection'
997 ;
999-}
1000directive :: SyntaxInfo -> IdrisParser [PDecl]
1001directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
1002 return [PDirective (do addLib cgn lib
1003 addIBC (IBCLib cgn lib))]
1004 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
1005 return [PDirective (do dirs <- allImportDirs
1006 o <- liftIO $ findInPath dirs obj
1007 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
1008 addObjectFile cgn o)]
1009 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
1010 flag <- stringLiteral
1011 return [PDirective (do addIBC (IBCCGFlag cgn flag)
1012 addFlag cgn flag)]
1013 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
1014 return [PDirective (do addHdr cgn hdr
1015 addIBC (IBCHeader cgn hdr))]
1016 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
1017 return [PDirective (do setAccessibility n Hidden
1018 addIBC (IBCAccess n Hidden))]
1019 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
1020 return [PDirective (do setAccessibility n Frozen
1021 addIBC (IBCAccess n Frozen))]
1022 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1023 return [PDirective (do i <- get
1024 put(i { default_access = acc }))]
1025 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1026 i <- get
1027 put (i { default_total = tot } )
1028 return [PDirective (do i <- get
1029 put(i { default_total = tot }))]
1030 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
1031 return [PDirective (setLogLevel (fromInteger i))]
1032 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
1033 return [PDirective (do added <- addDyLib libs
1034 case added of
1035 Left lib -> addIBC (IBCDyLib (lib_name lib))
1036 Right msg ->
1037 fail $ msg)]
1038 <|> do try (lchar '%' *> reserved "name")
1039 ty <- fnName
1040 ns <- sepBy1 name (lchar ',')
1041 return [PDirective (do ty' <- disambiguate ty
1042 mapM_ (addNameHint ty') ns
1043 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1044 <|> do try (lchar '%' *> reserved "error_handlers")
1045 fn <- fnName
1046 arg <- fnName
1047 ns <- sepBy1 name (lchar ',')
1048 return [PDirective (do fn' <- disambiguate fn
1049 ns' <- mapM disambiguate ns
1050 addFunctionErrorHandlers fn' arg ns'
1051 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]
1052 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1053 return [PDirective (addLangExt ext)]
1054 <?> "directive"
1055 where disambiguate :: Name -> Idris Name
1056 disambiguate n = do i <- getIState
1057 case lookupCtxtName n (idris_implicits i) of
1058 [(n', _)] -> return n'
1059 [] -> throwError (NoSuchVariable n)
1060 more -> throwError (CantResolveAlts (map fst more))
1062pLangExt :: IdrisParser LanguageExt
1063pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1064 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1066{- | Parses a totality
1069Totality ::= 'partial' | 'total'
1073totality :: IdrisParser Bool
1074totality
1075 = do reserved "total"; return True
1076 <|> do reserved "partial"; return False
1078{- | Parses a type provider
1081Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1082ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1084 -}
1085provider :: SyntaxInfo -> IdrisParser [PDecl]
1086provider syn = do try (lchar '%' *> reserved "provide");
1087 provideTerm <|> providePostulate
1088 <?> "type provider"
1089 where provideTerm = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1090 fc <- getFC
1091 reserved "with"
1092 e <- expr syn <?> "provider expression"
1093 return [PProvider syn fc (ProvTerm t e) n]
1094 providePostulate = do reserved "postulate"
1095 n <- fnName
1096 fc <- getFC
1097 reserved "with"
1098 e <- expr syn <?> "provider expression"
1099 return [PProvider syn fc (ProvPostulate e) n]
1101{- | Parses a transform
1104Transform ::= '%' 'transform' Expr '==>' Expr
1107transform :: SyntaxInfo -> IdrisParser [PDecl]
1108transform syn = do try (lchar '%' *> reserved "transform")
1109 -- leave it unchecked, until we work out what this should
1110 -- actually mean...
1111-- safety <- option True (do reserved "unsafe"
1112-- return False)
1113 l <- expr syn
1114 fc <- getFC
1115 symbol "==>"
1116 r <- expr syn
1117 return [PTransform fc False l r]
1118 <?> "transform"
1121{- * Loading and parsing -}
1122{- | Parses an expression from input -}
1123parseExpr :: IState -> String -> Result PTerm
1124parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1126{- | Parses a constant form input -}
1127parseConst :: IState -> String -> Result Const
1128parseConst st = runparser constant st "(input)"
1130{- | Parses a tactic from input -}
1131parseTactic :: IState -> String -> Result PTactic
1132parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1134-- | Parse module header and imports
1135parseImports :: FilePath -> String -> Idris ([String], [(String, Maybe String, FC)], Maybe Delta)
1136parseImports fname input
1137 = do i <- getIState
1138 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1139 Failure err -> fail (show err)
1140 Success (x, i) -> do putIState i
1141 return x
1142 where imports :: IdrisParser (([String], [(String, Maybe String, FC)], Maybe Delta), IState)
1143 imports = do whiteSpace
1144 mname <- moduleHeader
1145 ps <- many import_
1146 mrk <- mark
1147 isEof <- lookAheadMatches eof
1148 let mrk' = if isEof
1149 then Nothing
1150 else Just mrk
1151 i <- get
1152 return ((mname, ps, mrk'), i)
1154-- | There should be a better way of doing this...
1155findFC :: Doc -> (FC, String)
1156findFC x = let s = show (plain x) in
1157 case span (/= ':') s of
1158 (failname, ':':rest) -> case span isDigit rest of
1159 (line, ':':rest') -> case span isDigit rest' of
1160 (col, ':':msg) -> let pos = (read line, read col) in
1161 (FC failname pos pos, msg)
1163-- | Check if the coloring matches the options and corrects if necessary
1164fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1165fixColour False doc = ANSI.plain doc
1166fixColour True doc = doc
1168-- | A program is a list of declarations, possibly with associated
1169-- documentation strings.
1170parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1171 Idris [PDecl]
1172parseProg syn fname input mrk
1173 = do i <- getIState
1174 case runparser mainProg i fname input of
1175 Failure doc -> do -- FIXME: Get error location from trifecta
1176 -- this can't be the solution!
1177 -- Issue #1575 on the issue tracker.
1178 -- https://github.com/idris-lang/Idris-dev/issues/1575
1179 let (fc, msg) = findFC doc
1180 i <- getIState
1181 case idris_outputmode i of
1182 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1183 IdeSlave n h -> iWarn fc (P.text msg)
1184 putIState (i { errSpan = Just fc })
1185 return []
1186 Success (x, i) -> do putIState i
1187 reportParserWarnings
1188 return $ collect x
1189 where mainProg :: IdrisParser ([PDecl], IState)
1190 mainProg = case mrk of
1191 Nothing -> do i <- get; return ([], i)
1192 Just mrk -> do
1193 release mrk
1194 ds <- prog syn
1195 i' <- get
1196 return (ds, i')
1198{- | Load idris module and show error if something wrong happens -}
1199loadModule :: FilePath -> Idris String
1200loadModule f
1201 = idrisCatch (loadModule' f)
1202 (\e -> do setErrSpan (getErrSpan e)
1203 ist <- getIState
1204 iWarn (getErrSpan e) $ pprintErr ist e
1205 return "")
1207{- | Load idris module -}
1208loadModule' :: FilePath -> Idris String
1209loadModule' f
1210 = do i <- getIState
1211 let file = takeWhile (/= ' ') f
1212 ibcsd <- valIBCSubDir i
1213 ids <- allImportDirs
1214 fp <- findImport ids ibcsd file
1215 if file `elem` imported i
1216 then iLOG $ "Already read " ++ file
1217 else do putIState (i { imported = file : imported i })
1218 case fp of
1219 IDR fn -> loadSource False fn Nothing
1220 LIDR fn -> loadSource True fn Nothing
1221 IBC fn src ->
1222 idrisCatch (loadIBC fn)
1223 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1224 case src of
1225 IDR sfn -> loadSource False sfn Nothing
1226 LIDR sfn -> loadSource True sfn Nothing)
1227 let (dir, fh) = splitFileName file
1228 return (dropExtension fh)
1231{- | Load idris code from file -}
1232loadFromIFile :: IFileType -> Maybe Int -> Idris ()
1233loadFromIFile i@(IBC fn src) maxline
1234 = do iLOG $ "Skipping " ++ getSrcFile i
1235 idrisCatch (loadIBC fn)
1236 (\err -> ierror $ LoadingFailed fn err)
1237 where
1238 getSrcFile (IDR fn) = fn
1239 getSrcFile (LIDR fn) = fn
1240 getSrcFile (IBC f src) = getSrcFile src
1242loadFromIFile (IDR fn) maxline = loadSource' False fn maxline
1243loadFromIFile (LIDR fn) maxline = loadSource' True fn maxline
1245{-| Load idris source code and show error if something wrong happens -}
1246loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1247loadSource' lidr r maxline
1248 = idrisCatch (loadSource lidr r maxline)
1249 (\e -> do setErrSpan (getErrSpan e)
1250 ist <- getIState
1251 case e of
1252 At f e' -> iWarn f (pprintErr ist e')
1253 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1255{- | Load Idris source code-}
1256loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1257loadSource lidr f toline
1258 = do iLOG ("Reading " ++ f)
1259 i <- getIState
1260 let def_total = default_total i
1261 file_in <- runIO $ readFile f
1262 file <- if lidr then tclift $ unlit f file_in else return file_in
1263 (mname, imports_in, pos) <- parseImports f file
1264 ai <- getAutoImports
1265 let imports = map (\n -> (n, Just n, emptyFC)) ai ++ imports_in
1266 ids <- allImportDirs
1267 ibcsd <- valIBCSubDir i
1268 mapM_ (\f -> do fp <- findImport ids ibcsd f
1269 case fp of
1270 LIDR fn -> ifail $ "No ibc for " ++ f
1271 IDR fn -> ifail $ "No ibc for " ++ f
1272 IBC fn src -> loadIBC fn)
1273 [fn | (fn, _, _) <- imports]
1274 reportParserWarnings
1276 -- process and check module aliases
1277 let modAliases = M.fromList
1278 [(prep alias, prep realName) | (realName, Just alias, fc) <- imports]
1279 prep = map T.pack . reverse . Spl.splitOn "/"
1280 aliasNames = [(alias, fc) | (_, Just alias, fc) <- imports]
1281 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1282 case map head . filter ((/= 1) . length) $ histogram of
1283 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1284 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1286 i <- getIState
1287 putIState (i { default_access = Hidden, module_aliases = modAliases })
1288 clearIBC -- start a new .ibc file
1289 -- record package info in .ibc
1290 imps <- allImportDirs
1291 mapM_ addIBC (map IBCImportDir imps)
1292 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]
1293 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1294 maxline = toline }
1295 ds' <- parseProg syntax f file pos
1297 -- Parsing done, now process declarations
1299 let ds = namespaces mname ds'
1300 logLvl 3 (show $ showDecls verbosePPOption ds)
1301 i <- getIState
1302 logLvl 10 (show (toAlist (idris_implicits i)))
1303 logLvl 3 (show (idris_infixes i))
1304 -- Now add all the declarations to the context
1305 v <- verbose
1306 when v $ iputStrLn $ "Type checking " ++ f
1307 -- we totality check after every Mutual block, so if
1308 -- anything is a single definition, wrap it in a
1309 -- mutual block on its own
1310 elabDecls toplevel (map toMutual ds)
1311 i <- getIState
1312 -- simplify every definition do give the totality checker
1313 -- a better chance
1314 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1315 updateContext (simplifyCasedef n $ getErasureInfo i))
1316 (map snd (idris_totcheck i))
1317 -- build size change graph from simplified definitions
1318 iLOG "Totality checking"
1319 i <- getIState
1320 mapM_ buildSCG (idris_totcheck i)
1321 mapM_ checkDeclTotality (idris_totcheck i)
1323 -- Redo totality check for deferred names
1324 let deftots = idris_defertotcheck i
1325 iLOG $ "Totality checking " ++ show deftots
1326 mapM_ (\x -> do tot <- getTotality x
1327 case tot of
1328 Total _ -> setTotality x Unchecked
1329 _ -> return ()) (map snd deftots)
1330 mapM_ buildSCG deftots
1331 mapM_ checkDeclTotality deftots
1333 iLOG ("Finished " ++ f)
1334 ibcsd <- valIBCSubDir i
1335 iLOG "Universe checking"
1336 iucheck
1337 let ibc = ibcPathNoFallback ibcsd f
1338 i <- getIState
1339 addHides (hide_list i)
1341 -- Finally, write an ibc if checking was successful
1342 ok <- noErrors
1343 when ok $
1344 idrisCatch (do writeIBC f ibc; clearIBC)
1345 (\c -> return ()) -- failure is harmless
1346 i <- getIState
1347 putIState (i { default_total = def_total,
1348 hide_list = [] })
1349 return ()
1350 where
1351 namespaces :: [String] -> [PDecl] -> [PDecl]
1352 namespaces [] ds = ds
1353 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1355 toMutual :: PDecl -> PDecl
1356 toMutual m@(PMutual _ d) = m
1357 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1358 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1359 case x of
1360 PClauses _ _ _ _ -> r
1361 PClass _ _ _ _ _ _ _ _ -> r
1362 PInstance _ _ _ _ _ _ _ _ -> r
1363 _ -> x
1365{- | Adds names to hide list -}
1366addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1367addHides xs = do i <- getIState
1368 let defh = default_access i
1369 let (hs, as) = partition isNothing xs
1370 unless (null as) $
1371 mapM_ doHide
1372 (map (\ (n, _) -> (n, defh)) hs ++
1373 map (\ (n, Just a) -> (n, a)) as)
1374 where isNothing (_, Nothing) = True
1375 isNothing _ = False
1377 doHide (n, a) = do setAccessibility n a
1378 addIBC (IBCAccess n a)