git.iko.soy/Idris-dev
on 17c537f help sign in
Idris-dev/src/Idris/Parser.hs
1363 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 let rs = syntax_rules i
221 let ns = syntax_keywords i
222 let ibc = ibc_write i
223 let ks = map show (names s)
224 put (i { syntax_rules = s : rs,
225 syntax_keywords = ks ++ ns,
226 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc })
227 fc <- getFC
228 return (PSyntax fc s)
229 where names (Rule syms _ _) = mapMaybe ename syms
230 ename (Keyword n) = Just n
231 ename _ = Nothing
233{- | Parses a syntax extension declaration
236SyntaxRuleOpts ::= 'term' | 'pattern';
240SyntaxRule ::=
241 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
245SyntaxSym ::= '[' Name_t ']'
246 | '{' Name_t '}'
247 | Name_t
248 | StringLiteral_t
249 ;
251-}
252syntaxRule :: SyntaxInfo -> IdrisParser Syntax
253syntaxRule syn
254 = do sty <- try (do
255 pushIndent
256 sty <- option AnySyntax (do reserved "term"; return TermSyntax
257 <|> do reserved "pattern"; return PatternSyntax)
258 reserved "syntax"
259 return sty)
260 syms <- some syntaxSym
261 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
262 let ns = mapMaybe getName syms
263 when (length ns /= length (nub ns))
264 $ unexpected "repeated variable in syntax rule"
265 lchar '='
266 tm <- typeExpr (allowImp syn)
267 terminator
268 return (Rule (mkSimple syms) tm sty)
269 where
270 isExpr (Expr _) = True
271 isExpr _ = False
272 getName (Expr n) = Just n
273 getName _ = Nothing
274 -- Can't parse two full expressions (i.e. expressions with application) in a row
275 -- so change them both to a simple expression
276 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
277 mkSimple xs = mkSimple' xs
279 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
280 mkSimple es
281 mkSimple' (e : es) = e : mkSimple' es
282 mkSimple' [] = []
285{- | Parses a syntax symbol (either binding variable, keyword or expression)
288SyntaxSym ::= '[' Name_t ']'
289 | '{' Name_t '}'
290 | Name_t
291 | StringLiteral_t
292 ;
294 -}
295syntaxSym :: IdrisParser SSymbol
296syntaxSym = try (do lchar '['; n <- name; lchar ']'
297 return (Expr n))
298 <|> try (do lchar '{'; n <- name; lchar '}'
299 return (Binding n))
300 <|> do n <- iName []
301 return (Keyword n)
302 <|> do sym <- stringLiteral
303 return (Symbol sym)
304 <?> "syntax symbol"
306{- | Parses a function declaration with possible syntax sugar
309 FunDecl ::= FunDecl';
311-}
312fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
313fnDecl syn = try (do notEndBlock
314 d <- fnDecl' syn
315 i <- get
316 let d' = fmap (desugar syn i) d
317 return [d']) <?> "function declaration"
319{-| Parses a function declaration
322 FunDecl' ::=
323 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
324 | Postulate
325 | Pattern
326 | CAF
327 ;
329-}
330fnDecl' :: SyntaxInfo -> IdrisParser PDecl
331fnDecl' syn = checkFixity $
332 do (doc, argDocs, fc, opts', n, acc) <- try (do
333 pushIndent
334 (doc, argDocs) <- option noDocs docComment
335 ist <- get
336 let doc' = annotCode (tryFullExpr syn ist) doc
337 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
338 | (n, d) <- argDocs ]
340 initOpts = if default_total ist
341 then [TotalFn]
342 else []
343 opts <- fnOpts initOpts
344 acc <- optional accessibility
345 opts' <- fnOpts opts
346 n_in <- fnName
347 let n = expandNS syn n_in
348 fc <- getFC
349 lchar ':'
350 return (doc', argDocs', fc, opts', n, acc))
351 ty <- typeExpr (allowImp syn)
352 terminator
353 addAcc n acc
354 return (PTy doc argDocs syn fc opts' n ty)
355 <|> postulate syn
356 <|> caf syn
357 <|> pattern syn
358 <?> "function declaration"
359 where checkFixity :: IdrisParser PDecl -> IdrisParser PDecl
360 checkFixity p = do decl <- p
361 case getName decl of
362 Nothing -> return decl
363 Just n -> do fOk <- fixityOK n
364 unless fOk . fail $
365 "Missing fixity declaration for " ++ show n
366 return decl
367 getName (PTy _ _ _ _ _ n _) = Just n
368 getName _ = Nothing
369 fixityOK (NS n _) = fixityOK n
370 fixityOK (UN n) | all (flip elem opChars) (str n) =
371 do fixities <- fmap idris_infixes get
372 return . elem (str n) . map (\ (Fix _ op) -> op) $ fixities
373 | otherwise = return True
374 fixityOK _ = return True
376{-| Parses function options given initial options
379FnOpts ::= 'total'
380 | 'partial'
381 | 'implicit'
382 | '%' 'no_implicit'
383 | '%' 'assert_total'
384 | '%' 'error_handler'
385 | '%' 'reflection'
386 | '%' 'specialise' '[' NameTimesList? ']'
387 ;
391NameTimes ::= FnName Natural?;
395NameTimesList ::=
396 NameTimes
397 | NameTimes ',' NameTimesList
398 ;
400-}
401-- FIXME: Check compatability for function options (i.e. partal/total)
402fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
403fnOpts opts
404 = do reserved "total"; fnOpts (TotalFn : opts)
405 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
406 <|> do reserved "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))
407 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;
408 fnOpts (CExport c : opts)
409 <|> do try (lchar '%' *> reserved "no_implicit");
410 fnOpts (NoImplicit : opts)
411 <|> do try (lchar '%' *> reserved "assert_total");
412 fnOpts (AssertTotal : opts)
413 <|> do try (lchar '%' *> reserved "error_handler");
414 fnOpts (ErrorHandler : opts)
415 <|> do try (lchar '%' *> reserved "error_reverse");
416 fnOpts (ErrorReverse : opts)
417 <|> do try (lchar '%' *> reserved "reflection");
418 fnOpts (Reflection : opts)
419 <|> do lchar '%'; reserved "specialise";
420 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
421 fnOpts (Specialise ns : opts)
422 <|> do reserved "implicit"; fnOpts (Implicit : opts)
423 <|> return opts
424 <?> "function modifier"
425 where nameTimes :: IdrisParser (Name, Maybe Int)
426 nameTimes = do n <- fnName
427 t <- option Nothing (do reds <- natural
428 return (Just (fromInteger reds)))
429 return (n, t)
431{- | Parses a postulate
434Postulate ::=
435 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
436 ;
438-}
439postulate :: SyntaxInfo -> IdrisParser PDecl
440postulate syn = do doc <- try $ do (doc, _) <- option noDocs docComment
441 ist <- get
442 let doc' = annotCode (tryFullExpr syn ist) doc
443 pushIndent
444 reserved "postulate"
445 return doc'
446 ist <- get
447 let initOpts = if default_total ist
448 then [TotalFn]
449 else []
450 opts <- fnOpts initOpts
451 acc <- optional accessibility
452 opts' <- fnOpts opts
453 n_in <- fnName
454 let n = expandNS syn n_in
455 lchar ':'
456 ty <- typeExpr (allowImp syn)
457 fc <- getFC
458 terminator
459 addAcc n acc
460 return (PPostulate doc syn fc opts' n ty)
461 <?> "postulate"
463{- | Parses a using declaration
466Using ::=
467 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
468 ;
470 -}
471using_ :: SyntaxInfo -> IdrisParser [PDecl]
472using_ syn =
473 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
474 openBlock
475 let uvars = using syn
476 ds <- many (decl (syn { using = uvars ++ ns }))
477 closeBlock
478 return (concat ds)
479 <?> "using declaration"
481{- | Parses a parameters declaration
484Params ::=
485 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
486 ;
488 -}
489params :: SyntaxInfo -> IdrisParser [PDecl]
490params syn =
491 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
492 openBlock
493 let pvars = syn_params syn
494 ds <- many (decl syn { syn_params = pvars ++ ns })
495 closeBlock
496 fc <- getFC
497 return [PParams fc ns (concat ds)]
498 <?> "parameters declaration"
500{- | Parses a mutual declaration (for mutually recursive functions)
503Mutual ::=
504 'mutual' OpenBlock Decl* CloseBlock
505 ;
507-}
508mutual :: SyntaxInfo -> IdrisParser [PDecl]
509mutual syn =
510 do reserved "mutual"
511 openBlock
512 let pvars = syn_params syn
513 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
514 closeBlock
515 fc <- getFC
516 return [PMutual fc (concat ds)]
517 <?> "mutual block"
519{-| Parses a namespace declaration
522Namespace ::=
523 'namespace' identifier OpenBlock Decl+ CloseBlock
524 ;
526-}
527namespace :: SyntaxInfo -> IdrisParser [PDecl]
528namespace syn =
529 do reserved "namespace"; n <- identifier;
530 openBlock
531 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
532 closeBlock
533 return [PNamespace n (concat ds)]
534 <?> "namespace declaration"
536{- | Parses a methods block (for instances)
539 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
541-}
542instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
543instanceBlock syn = do reserved "where"
544 openBlock
545 ds <- many (fnDecl syn)
546 closeBlock
547 return (concat ds)
548 <?> "instance block"
550{- | Parses a methods and instances block (for type classes)
553MethodOrInstance ::=
554 FnDecl
555 | Instance
556 ;
560ClassBlock ::=
561 'where' OpenBlock MethodOrInstance* CloseBlock
562 ;
564-}
565classBlock :: SyntaxInfo -> IdrisParser [PDecl]
566classBlock syn = do reserved "where"
567 openBlock
568 ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)
569 closeBlock
570 return (concat ds)
571 <?> "class block"
573{-| Parses a type class declaration
576ClassArgument ::=
577 Name
578 | '(' Name ':' Expr ')'
579 ;
583Class ::=
584 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
585 ;
587-}
588class_ :: SyntaxInfo -> IdrisParser [PDecl]
589class_ syn = do (doc, argDocs, acc) <- try (do
590 (doc, argDocs) <- option noDocs docComment
591 ist <- get
592 let doc' = annotCode (tryFullExpr syn ist) doc
593 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
594 | (n, d) <- argDocs ]
595 acc <- optional accessibility
596 return (doc', argDocs', acc))
597 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName
598 let n = expandNS syn n_in
599 cs <- many carg
600 ds <- option [] (classBlock syn)
601 accData acc n (concatMap declared ds)
602 return [PClass doc syn fc cons n cs argDocs ds]
603 <?> "type-class declaration"
604 where
605 carg :: IdrisParser (Name, PTerm)
606 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
607 return (i, ty)
608 <|> do i <- name;
609 return (i, PType)
611{- | Parses a type class instance declaration
614 Instance ::=
615 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
616 ;
620InstanceName ::= '[' Name ']';
622-}
623instance_ :: SyntaxInfo -> IdrisParser [PDecl]
624instance_ syn = do reserved "instance"; fc <- getFC
625 en <- optional instanceName
626 cs <- constraintList syn
627 cn <- fnName
628 args <- many (simpleExpr syn)
629 let sc = PApp fc (PRef fc cn) (map pexp args)
630 let t = bindList (PPi constraint) (map (\x -> (sMN 0 "constraint", x)) cs) sc
631 ds <- option [] (instanceBlock syn)
632 return [PInstance syn fc cs cn args t en ds]
633 <?> "instance declaration"
634 where instanceName :: IdrisParser Name
635 instanceName = do lchar '['; n_in <- fnName; lchar ']'
636 let n = expandNS syn n_in
637 return n
638 <?> "instance name"
641{- | Parses a using declaration list
644UsingDeclList ::=
645 UsingDeclList'
646 | NameList TypeSig
647 ;
651UsingDeclList' ::=
652 UsingDecl
653 | UsingDecl ',' UsingDeclList'
654 ;
658NameList ::=
659 Name
660 | Name ',' NameList
661 ;
663-}
664usingDeclList :: SyntaxInfo -> IdrisParser [Using]
665usingDeclList syn
666 = try (sepBy1 (usingDecl syn) (lchar ','))
667 <|> do ns <- sepBy1 name (lchar ',')
668 lchar ':'
669 t <- typeExpr (disallowImp syn)
670 return (map (\x -> UImplicit x t) ns)
671 <?> "using declaration list"
673{- |Parses a using declaration
676UsingDecl ::=
677 FnName TypeSig
678 | FnName FnName+
679 ;
681-}
682usingDecl :: SyntaxInfo -> IdrisParser Using
683usingDecl syn = try (do x <- fnName
684 lchar ':'
685 t <- typeExpr (disallowImp syn)
686 return (UImplicit x t))
687 <|> do c <- fnName
688 xs <- some fnName
689 return (UConstraint c xs)
690 <?> "using declaration"
692{- | Parse a clause with patterns
695Pattern ::= Clause;
697-}
698pattern :: SyntaxInfo -> IdrisParser PDecl
699pattern syn = do fc <- getFC
700 clause <- clause syn
701 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
702 <?> "pattern"
704{- | Parse a constant applicative form declaration
707CAF ::= 'let' FnName '=' Expr Terminator;
709-}
710caf :: SyntaxInfo -> IdrisParser PDecl
711caf syn = do reserved "let"
712 n_in <- fnName; let n = expandNS syn n_in
713 lchar '='
714 t <- expr syn
715 terminator
716 fc <- getFC
717 return (PCAF fc n t)
718 <?> "constant applicative form declaration"
720{- | Parse an argument expression
723ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
725-}
726argExpr :: SyntaxInfo -> IdrisParser PTerm
727argExpr syn = let syn' = syn { inPattern = True } in
728 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
729 <?> "argument expression"
731{- | Parse a right hand side of a function
734RHS ::= '=' Expr
735 | '?=' RHSName? Expr
736 | 'impossible'
737 ;
741RHSName ::= '{' FnName '}';
743-}
744rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
745rhs syn n = do lchar '='; expr syn
746 <|> do symbol "?=";
747 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
748 return n)
749 r <- expr syn
750 return (addLet name r)
751 <|> do reserved "impossible"; return PImpossible
752 <?> "function right hand side"
753 where mkN :: Name -> Name
754 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
755 then sUN "infix_op_lemma_1"
756 else sUN (str x++"_lemma_1")
757 mkN (NS x n) = NS (mkN x) n
758 n' :: Name
759 n' = mkN n
760 addLet :: Name -> PTerm -> PTerm
761 addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)
762 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
763 where addLetC (l, r) = (l, addLet nm r)
764 addLet nm r = (PLet (sUN "value") Placeholder r (PMetavar nm))
766{- |Parses a function clause
769RHSOrWithBlock ::= RHS WhereOrTerminator
770 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
771 ;
775Clause ::= WExpr+ RHSOrWithBlock
776 | SimpleExpr '<==' FnName RHS WhereOrTerminator
777 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
778 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
779 ;
783ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
787WhereOrTerminator ::= WhereBlock | Terminator;
789-}
790clause :: SyntaxInfo -> IdrisParser PClause
791clause syn
792 = do wargs <- try (do pushIndent; some (wExpr syn))
793 fc <- getFC
794 ist <- get
795 n <- case lastParse ist of
796 Just t -> return t
797 Nothing -> fail "Invalid clause"
798 (do r <- rhs syn n
799 let ctxt = tt_ctxt ist
800 let wsyn = syn { syn_namespace = [] }
801 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
802 popIndent
803 return x,
804 do terminator
805 return ([], [])]
806 return $ PClauseR fc wargs r wheres) <|> (do
807 popIndent
808 reserved "with"
809 wval <- simpleExpr syn
810 openBlock
811 ds <- some $ fnDecl syn
812 let withs = concat ds
813 closeBlock
814 return $ PWithR fc wargs wval withs)
815 <|> do ty <- try (do pushIndent
816 ty <- simpleExpr syn
817 symbol "<=="
818 return ty)
819 fc <- getFC
820 n_in <- fnName; let n = expandNS syn n_in
821 r <- rhs syn n
822 ist <- get
823 let ctxt = tt_ctxt ist
824 let wsyn = syn { syn_namespace = [] }
825 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
826 popIndent
827 return x,
828 do terminator
829 return ([], [])]
830 let capp = PLet (sMN 0 "match")
831 ty
832 (PMatchApp fc n)
833 (PRef fc (sMN 0 "match"))
834 ist <- get
835 put (ist { lastParse = Just n })
836 return $ PClause fc n capp [] r wheres
837 <|> do (l, op) <- try (do
838 pushIndent
839 l <- argExpr syn
840 op <- operator
841 when (op == "=" || op == "?=" ) $
842 fail "infix clause definition with \"=\" and \"?=\" not supported "
843 return (l, op))
844 let n = expandNS syn (sUN op)
845 r <- argExpr syn
846 fc <- getFC
847 wargs <- many (wExpr syn)
848 (do rs <- rhs syn n
849 let wsyn = syn { syn_namespace = [] }
850 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
851 popIndent
852 return x,
853 do terminator
854 return ([], [])]
855 ist <- get
856 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
857 put (ist { lastParse = Just n })
858 return $ PClause fc n capp wargs rs wheres) <|> (do
859 popIndent
860 reserved "with"
861 wval <- bracketed syn
862 openBlock
863 ds <- some $ fnDecl syn
864 closeBlock
865 ist <- get
866 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
867 let withs = map (fillLHSD n capp wargs) $ concat ds
868 put (ist { lastParse = Just n })
869 return $ PWith fc n capp wargs wval withs)
870 <|> do pushIndent
871 n_in <- fnName; let n = expandNS syn n_in
872 cargs <- many (constraintArg syn)
873 fc <- getFC
874 args <- many (try (implicitArg (syn { inPattern = True } ))
875 <|> (fmap pexp (argExpr syn)))
876 wargs <- many (wExpr syn)
877 let capp = PApp fc (PRef fc n)
878 (cargs ++ args)
879 (do r <- rhs syn n
880 ist <- get
881 let ctxt = tt_ctxt ist
882 let wsyn = syn { syn_namespace = [] }
883 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
884 popIndent
885 return x,
886 do terminator
887 return ([], [])]
888 ist <- get
889 put (ist { lastParse = Just n })
890 return $ PClause fc n capp wargs r wheres) <|> (do
891 reserved "with"
892 ist <- get
893 put (ist { lastParse = Just n })
894 wval <- bracketed syn
895 openBlock
896 ds <- some $ fnDecl syn
897 let withs = map (fillLHSD n capp wargs) $ concat ds
898 closeBlock
899 popIndent
900 return $ PWith fc n capp wargs wval withs)
901 <?> "function clause"
902 where
903 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
904 fillLHS n capp owargs (PClauseR fc wargs v ws)
905 = PClause fc n capp (owargs ++ wargs) v ws
906 fillLHS n capp owargs (PWithR fc wargs v ws)
907 = PWith fc n capp (owargs ++ wargs) v
908 (map (fillLHSD n capp (owargs ++ wargs)) ws)
909 fillLHS _ _ _ c = c
911 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
912 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
913 fillLHSD n c a x = x
915{-| Parses with pattern
917@
918WExpr ::= '|' Expr';
920-}
921wExpr :: SyntaxInfo -> IdrisParser PTerm
922wExpr syn = do lchar '|'
923 expr' syn
924 <?> "with pattern"
926{- | Parses a where block
929WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
931-}
932whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
933whereBlock n syn
934 = do reserved "where"
935 ds <- indentedBlock1 (decl syn)
936 let dns = concatMap (concatMap declared) ds
937 return (concat ds, map (\x -> (x, decoration syn x)) dns)
938 <?> "where block"
940{- |Parses a code generation target language name
943Codegen ::= 'C'
944 | 'Java'
945 | 'JavaScript'
946 | 'Node'
947 | 'LLVM'
948 | 'Bytecode'
949 ;
951-}
952codegen_ :: IdrisParser Codegen
953codegen_ = do n <- identifier; return (Via (map toLower n))
954 <|> do reserved "Bytecode"; return Bytecode
955 <?> "code generation language"
957{- |Parses a compiler directive
959StringList ::=
960 String
961 | String ',' StringList
962 ;
966Directive ::= '%' Directive';
970Directive' ::= 'lib' CodeGen String_t
971 | 'link' CodeGen String_t
972 | 'flag' CodeGen String_t
973 | 'include' CodeGen String_t
974 | 'hide' Name
975 | 'freeze' Name
976 | 'access' Accessibility
977 | 'default' Totality
978 | 'logging' Natural
979 | 'dynamic' StringList
980 | 'name' Name NameList
981 | 'error_handlers' Name NameList
982 | 'language' 'TypeProviders'
983 | 'language' 'ErrorReflection'
984 ;
986-}
987directive :: SyntaxInfo -> IdrisParser [PDecl]
988directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
989 return [PDirective (do addLib cgn lib
990 addIBC (IBCLib cgn lib))]
991 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
992 return [PDirective (do dirs <- allImportDirs
993 o <- liftIO $ findInPath dirs obj
994 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
995 addObjectFile cgn o)]
996 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
997 flag <- stringLiteral
998 return [PDirective (do addIBC (IBCCGFlag cgn flag)
999 addFlag cgn flag)]
1000 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
1001 return [PDirective (do addHdr cgn hdr
1002 addIBC (IBCHeader cgn hdr))]
1003 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
1004 return [PDirective (do setAccessibility n Hidden
1005 addIBC (IBCAccess n Hidden))]
1006 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
1007 return [PDirective (do setAccessibility n Frozen
1008 addIBC (IBCAccess n Frozen))]
1009 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1010 return [PDirective (do i <- get
1011 put(i { default_access = acc }))]
1012 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1013 i <- get
1014 put (i { default_total = tot } )
1015 return [PDirective (do i <- get
1016 put(i { default_total = tot }))]
1017 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
1018 return [PDirective (setLogLevel (fromInteger i))]
1019 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
1020 return [PDirective (do added <- addDyLib libs
1021 case added of
1022 Left lib -> addIBC (IBCDyLib (lib_name lib))
1023 Right msg ->
1024 fail $ msg)]
1025 <|> do try (lchar '%' *> reserved "name")
1026 ty <- fnName
1027 ns <- sepBy1 name (lchar ',')
1028 return [PDirective (do ty' <- disambiguate ty
1029 mapM_ (addNameHint ty') ns
1030 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1031 <|> do try (lchar '%' *> reserved "error_handlers")
1032 fn <- fnName
1033 arg <- fnName
1034 ns <- sepBy1 name (lchar ',')
1035 return [PDirective (do fn' <- disambiguate fn
1036 ns' <- mapM disambiguate ns
1037 addFunctionErrorHandlers fn' arg ns'
1038 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]
1039 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1040 return [PDirective (addLangExt ext)]
1041 <?> "directive"
1042 where disambiguate :: Name -> Idris Name
1043 disambiguate n = do i <- getIState
1044 case lookupCtxtName n (idris_implicits i) of
1045 [(n', _)] -> return n'
1046 [] -> throwError (NoSuchVariable n)
1047 more -> throwError (CantResolveAlts (map fst more))
1049pLangExt :: IdrisParser LanguageExt
1050pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1051 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1053{- | Parses a totality
1056Totality ::= 'partial' | 'total'
1060totality :: IdrisParser Bool
1061totality
1062 = do reserved "total"; return True
1063 <|> do reserved "partial"; return False
1065{- | Parses a type provider
1068Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1069ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1071 -}
1072provider :: SyntaxInfo -> IdrisParser [PDecl]
1073provider syn = do try (lchar '%' *> reserved "provide");
1074 provideTerm <|> providePostulate
1075 <?> "type provider"
1076 where provideTerm = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1077 fc <- getFC
1078 reserved "with"
1079 e <- expr syn <?> "provider expression"
1080 return [PProvider syn fc (ProvTerm t e) n]
1081 providePostulate = do reserved "postulate"
1082 n <- fnName
1083 fc <- getFC
1084 reserved "with"
1085 e <- expr syn <?> "provider expression"
1086 return [PProvider syn fc (ProvPostulate e) n]
1088{- | Parses a transform
1091Transform ::= '%' 'transform' Expr '==>' Expr
1094transform :: SyntaxInfo -> IdrisParser [PDecl]
1095transform syn = do try (lchar '%' *> reserved "transform")
1096 -- leave it unchecked, until we work out what this should
1097 -- actually mean...
1098-- safety <- option True (do reserved "unsafe"
1099-- return False)
1100 l <- expr syn
1101 fc <- getFC
1102 symbol "==>"
1103 r <- expr syn
1104 return [PTransform fc False l r]
1105 <?> "transform"
1108{- * Loading and parsing -}
1109{- | Parses an expression from input -}
1110parseExpr :: IState -> String -> Result PTerm
1111parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1113{- | Parses a constant form input -}
1114parseConst :: IState -> String -> Result Const
1115parseConst st = runparser constant st "(input)"
1117{- | Parses a tactic from input -}
1118parseTactic :: IState -> String -> Result PTactic
1119parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1121-- | Parse module header and imports
1122parseImports :: FilePath -> String -> Idris ([String], [(String, Maybe String, FC)], Maybe Delta)
1123parseImports fname input
1124 = do i <- getIState
1125 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1126 Failure err -> fail (show err)
1127 Success (x, i) -> do putIState i
1128 return x
1129 where imports :: IdrisParser (([String], [(String, Maybe String, FC)], Maybe Delta), IState)
1130 imports = do whiteSpace
1131 mname <- moduleHeader
1132 ps <- many import_
1133 mrk <- mark
1134 isEof <- lookAheadMatches eof
1135 let mrk' = if isEof
1136 then Nothing
1137 else Just mrk
1138 i <- get
1139 return ((mname, ps, mrk'), i)
1141-- | There should be a better way of doing this...
1142findFC :: Doc -> (FC, String)
1143findFC x = let s = show (plain x) in
1144 case span (/= ':') s of
1145 (failname, ':':rest) -> case span isDigit rest of
1146 (line, ':':rest') -> case span isDigit rest' of
1147 (col, ':':msg) -> let pos = (read line, read col) in
1148 (FC failname pos pos, msg)
1150-- | Check if the coloring matches the options and corrects if necessary
1151fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1152fixColour False doc = ANSI.plain doc
1153fixColour True doc = doc
1155-- | A program is a list of declarations, possibly with associated
1156-- documentation strings.
1157parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1158 Idris [PDecl]
1159parseProg syn fname input mrk
1160 = do i <- getIState
1161 case runparser mainProg i fname input of
1162 Failure doc -> do -- FIXME: Get error location from trifecta
1163 -- this can't be the solution!
1164 let (fc, msg) = findFC doc
1165 i <- getIState
1166 case idris_outputmode i of
1167 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1168 IdeSlave n h -> iWarn fc (P.text msg)
1169 putIState (i { errSpan = Just fc })
1170 return []
1171 Success (x, i) -> do putIState i
1172 reportParserWarnings
1173 return $ collect x
1174 where mainProg :: IdrisParser ([PDecl], IState)
1175 mainProg = case mrk of
1176 Nothing -> do i <- get; return ([], i)
1177 Just mrk -> do
1178 release mrk
1179 ds <- prog syn
1180 i' <- get
1181 return (ds, i')
1183{- | Load idris module and show error if something wrong happens -}
1184loadModule :: FilePath -> Idris String
1185loadModule f
1186 = idrisCatch (loadModule' f)
1187 (\e -> do setErrSpan (getErrSpan e)
1188 ist <- getIState
1189 iWarn (getErrSpan e) $ pprintErr ist e
1190 return "")
1192{- | Load idris module -}
1193loadModule' :: FilePath -> Idris String
1194loadModule' f
1195 = do i <- getIState
1196 let file = takeWhile (/= ' ') f
1197 ibcsd <- valIBCSubDir i
1198 ids <- allImportDirs
1199 fp <- findImport ids ibcsd file
1200 if file `elem` imported i
1201 then iLOG $ "Already read " ++ file
1202 else do putIState (i { imported = file : imported i })
1203 case fp of
1204 IDR fn -> loadSource False fn Nothing
1205 LIDR fn -> loadSource True fn Nothing
1206 IBC fn src ->
1207 idrisCatch (loadIBC fn)
1208 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1209 case src of
1210 IDR sfn -> loadSource False sfn Nothing
1211 LIDR sfn -> loadSource True sfn Nothing)
1212 let (dir, fh) = splitFileName file
1213 return (dropExtension fh)
1216{- | Load idris code from file -}
1217loadFromIFile :: IFileType -> Maybe Int -> Idris ()
1218loadFromIFile i@(IBC fn src) maxline
1219 = do iLOG $ "Skipping " ++ getSrcFile i
1220 idrisCatch (loadIBC fn)
1221 (\err -> ierror $ LoadingFailed fn err)
1222 where
1223 getSrcFile (IDR fn) = fn
1224 getSrcFile (LIDR fn) = fn
1225 getSrcFile (IBC f src) = getSrcFile src
1227loadFromIFile (IDR fn) maxline = loadSource' False fn maxline
1228loadFromIFile (LIDR fn) maxline = loadSource' True fn maxline
1230{-| Load idris source code and show error if something wrong happens -}
1231loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1232loadSource' lidr r maxline
1233 = idrisCatch (loadSource lidr r maxline)
1234 (\e -> do setErrSpan (getErrSpan e)
1235 ist <- getIState
1236 case e of
1237 At f e' -> iWarn f (pprintErr ist e')
1238 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1240{- | Load Idris source code-}
1241loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1242loadSource lidr f toline
1243 = do iLOG ("Reading " ++ f)
1244 i <- getIState
1245 let def_total = default_total i
1246 file_in <- runIO $ readFile f
1247 file <- if lidr then tclift $ unlit f file_in else return file_in
1248 (mname, imports_in, pos) <- parseImports f file
1249 ai <- getAutoImports
1250 let imports = map (\n -> (n, Just n, emptyFC)) ai ++ imports_in
1251 ids <- allImportDirs
1252 ibcsd <- valIBCSubDir i
1253 mapM_ (\f -> do fp <- findImport ids ibcsd f
1254 case fp of
1255 LIDR fn -> ifail $ "No ibc for " ++ f
1256 IDR fn -> ifail $ "No ibc for " ++ f
1257 IBC fn src -> loadIBC fn)
1258 [fn | (fn, _, _) <- imports]
1259 reportParserWarnings
1261 -- process and check module aliases
1262 let modAliases = M.fromList
1263 [(prep alias, prep realName) | (realName, Just alias, fc) <- imports]
1264 prep = map T.pack . reverse . Spl.splitOn "/"
1265 aliasNames = [(alias, fc) | (_, Just alias, fc) <- imports]
1266 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1267 case map head . filter ((/= 1) . length) $ histogram of
1268 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1269 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1271 i <- getIState
1272 putIState (i { default_access = Hidden, module_aliases = modAliases })
1273 clearIBC -- start a new .ibc file
1274 -- record package info in .ibc
1275 imps <- allImportDirs
1276 mapM_ addIBC (map IBCImportDir imps)
1277 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]
1278 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1279 maxline = toline }
1280 ds' <- parseProg syntax f file pos
1282 -- Parsing done, now process declarations
1284 let ds = namespaces mname ds'
1285 logLvl 3 (show $ showDecls verbosePPOption ds)
1286 i <- getIState
1287 logLvl 10 (show (toAlist (idris_implicits i)))
1288 logLvl 3 (show (idris_infixes i))
1289 -- Now add all the declarations to the context
1290 v <- verbose
1291 when v $ iputStrLn $ "Type checking " ++ f
1292 -- we totality check after every Mutual block, so if
1293 -- anything is a single definition, wrap it in a
1294 -- mutual block on its own
1295 elabDecls toplevel (map toMutual ds)
1296 i <- getIState
1297 -- simplify every definition do give the totality checker
1298 -- a better chance
1299 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1300 updateContext (simplifyCasedef n $ getErasureInfo i))
1301 (map snd (idris_totcheck i))
1302 -- build size change graph from simplified definitions
1303 iLOG "Totality checking"
1304 i <- getIState
1305 mapM_ buildSCG (idris_totcheck i)
1306 mapM_ checkDeclTotality (idris_totcheck i)
1308 -- Redo totality check for deferred names
1309 let deftots = idris_defertotcheck i
1310 iLOG $ "Totality checking " ++ show deftots
1311 mapM_ (\x -> do tot <- getTotality x
1312 case tot of
1313 Total _ -> setTotality x Unchecked
1314 _ -> return ()) (map snd deftots)
1315 mapM_ buildSCG deftots
1316 mapM_ checkDeclTotality deftots
1318 iLOG ("Finished " ++ f)
1319 ibcsd <- valIBCSubDir i
1320 iLOG "Universe checking"
1321 iucheck
1322 let ibc = ibcPathNoFallback ibcsd f
1323 i <- getIState
1324 addHides (hide_list i)
1326 -- Finally, write an ibc if checking was successful
1327 ok <- noErrors
1328 when ok $
1329 idrisCatch (do writeIBC f ibc; clearIBC)
1330 (\c -> return ()) -- failure is harmless
1331 i <- getIState
1332 putIState (i { default_total = def_total,
1333 hide_list = [] })
1334 return ()
1335 where
1336 namespaces :: [String] -> [PDecl] -> [PDecl]
1337 namespaces [] ds = ds
1338 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1340 toMutual :: PDecl -> PDecl
1341 toMutual m@(PMutual _ d) = m
1342 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1343 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1344 case x of
1345 PClauses _ _ _ _ -> r
1346 PClass _ _ _ _ _ _ _ _ -> r
1347 PInstance _ _ _ _ _ _ _ _ -> r
1348 _ -> x
1350{- | Adds names to hide list -}
1351addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1352addHides xs = do i <- getIState
1353 let defh = default_access i
1354 let (hs, as) = partition isNothing xs
1355 unless (null as) $
1356 mapM_ doHide
1357 (map (\ (n, _) -> (n, defh)) hs ++
1358 map (\ (n, Just a) -> (n, a)) as)
1359 where isNothing (_, Nothing) = True
1360 isNothing _ = False
1362 doHide (n, a) = do setAccessibility n a
1363 addIBC (IBCAccess n a)