git.iko.soy/Idris-dev
on cd8fe96 help sign in
Idris-dev/src/Idris/Parser.hs
1127 lines 42 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)
21import Idris.AbsSyntax
22import Idris.DSL
23import Idris.Imports
24import Idris.Error
25import Idris.ElabDecls
26import Idris.ElabTerm hiding (namespace, params)
27import Idris.Coverage
28import Idris.IBC
29import Idris.Unlit
30import Idris.Providers
32import Idris.ParseHelpers
33import Idris.ParseOps
34import Idris.ParseExpr
35import Idris.ParseData
37import Paths_idris
39import Util.DynamicLinker
41import Core.TT
42import Core.Evaluate
44import Control.Applicative
45import Control.Monad
46import Control.Monad.State.Strict
48import Data.Maybe
49import qualified Data.List.Split as Spl
50import Data.List
51import Data.Monoid
52import Data.Char
53import qualified Data.HashSet as HS
54import qualified Data.Text as T
55import qualified Data.ByteString.UTF8 as UTF8
57import Debug.Trace
59import System.FilePath
60import System.IO
62{-
63 grammar shortcut notation:
64 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)
65 RULE? = optional rule (i.e. RULE or nothing)
66 RULE* = repeated rule (i.e. RULE zero or more times)
67 RULE+ = repeated rule with at least one match (i.e. RULE one or more times)
68 RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)
69 RULE{n} = rule repeated n times
70-}
72{- * Main grammar -}
74{- | Parses module definition
75 ModuleHeader ::= 'module' Identifier_t ';'?;
76-}
77moduleHeader :: IdrisParser [String]
78moduleHeader = try (do reserved "module"
79 i <- identifier
80 option ';' (lchar ';')
81 return (moduleName i))
82 <|> return []
83 where moduleName x = case span (/='.') x of
84 (x, "") -> [x]
85 (x, '.':y) -> x : moduleName y
87{- | Parses an import statement
88 Import ::= 'import' Identifier_t ';'?;
89 -}
90import_ :: IdrisParser String
91import_ = do reserved "import"
92 id <- identifier
93 option ';' (lchar ';')
94 return (toPath id)
95 <?> "import statement"
96 where toPath f = foldl1' (</>) (Spl.splitOn "." f)
98{- | Parses program source
99 Prog ::= Decl* EOF;
100 -}
101prog :: SyntaxInfo -> IdrisParser [PDecl]
102prog syn = do whiteSpace
103 decls <- many (decl syn)
104 notOpenBraces
105 eof
106 let c = (concat decls)
107 return c
109{- | Parses a top-level declaration
110Decl ::=
111 Decl'
112 | Using
113 | Params
114 | Mutual
115 | Namespace
116 | Class
117 | Instance
118 | DSL
119 | Directive
120 | Provider
121 | Transform
122 | Import!
123 ;
124-}
125decl :: SyntaxInfo -> IdrisParser [PDecl]
126decl syn = do notEndBlock
127 declBody
128 where declBody :: IdrisParser [PDecl]
129 declBody = declBody'
130 <|> using_ syn
131 <|> params syn
132 <|> mutual syn
133 <|> namespace syn
134 <|> class_ syn
135 <|> instance_ syn
136 <|> do d <- dsl syn; return [d]
137 <|> directive syn
138 <|> provider syn
139 <|> transform syn
140 <|> do import_; fail "imports must be at top of file"
141 <?> "declaration"
142 declBody' :: IdrisParser [PDecl]
143 declBody' = do d <- decl' syn
144 i <- get
145 let d' = fmap (debindApp syn . (desugar syn i)) d
146 return [d']
148{- | Parses a top-level declaration with possible syntax sugar
149Decl' ::=
150 Fixity
151 | FunDecl'
152 | Data
153 | Record
154 | SyntaxDecl
155 ;
156-}
157decl' :: SyntaxInfo -> IdrisParser PDecl
158decl' syn = fixity
159 <|> syntaxDecl syn
160 <|> fnDecl' syn
161 <|> data_ syn
162 <|> record syn
163 <?> "declaration"
165{- | Parses a syntax extension declaration (and adds the rule to parser state)
166 SyntaxDecl ::= SyntaxRule;
167-}
168syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
169syntaxDecl syn = do s <- syntaxRule syn
170 i <- get
171 let rs = syntax_rules i
172 let ns = syntax_keywords i
173 let ibc = ibc_write i
174 let ks = map show (names s)
175 put (i { syntax_rules = s : rs,
176 syntax_keywords = ks ++ ns,
177 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc })
178 fc <- getFC
179 return (PSyntax fc s)
180 where names (Rule syms _ _) = mapMaybe ename syms
181 ename (Keyword n) = Just n
182 ename _ = Nothing
184{- | Parses a syntax extension declaration
185SyntaxRuleOpts ::= 'term' | 'pattern';
187SyntaxRule ::=
188 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
190SyntaxSym ::= '[' Name_t ']'
191 | '{' Name_t '}'
192 | Name_t
193 | StringLiteral_t
194 ;
195-}
196syntaxRule :: SyntaxInfo -> IdrisParser Syntax
197syntaxRule syn
198 = do sty <- try (do
199 pushIndent
200 sty <- option AnySyntax (do reserved "term"; return TermSyntax
201 <|> do reserved "pattern"; return PatternSyntax)
202 reserved "syntax"
203 return sty)
204 syms <- some syntaxSym
205 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
206 let ns = mapMaybe getName syms
207 when (length ns /= length (nub ns))
208 $ unexpected "repeated variable in syntax rule"
209 lchar '='
210 tm <- typeExpr (allowImp syn)
211 terminator
212 return (Rule (mkSimple syms) tm sty)
213 where
214 isExpr (Expr _) = True
215 isExpr _ = False
216 getName (Expr n) = Just n
217 getName _ = Nothing
218 -- Can't parse two full expressions (i.e. expressions with application) in a row
219 -- so change them both to a simple expression
220 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
221 mkSimple xs = mkSimple' xs
223 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
224 mkSimple es
225 mkSimple' (e : es) = e : mkSimple' es
226 mkSimple' [] = []
229{- | Parses a syntax symbol (either binding variable, keyword or expression)
230SyntaxSym ::= '[' Name_t ']'
231 | '{' Name_t '}'
232 | Name_t
233 | StringLiteral_t
234 ;
235 -}
236syntaxSym :: IdrisParser SSymbol
237syntaxSym = try (do lchar '['; n <- name; lchar ']'
238 return (Expr n))
239 <|> try (do lchar '{'; n <- name; lchar '}'
240 return (Binding n))
241 <|> do n <- iName []
242 return (Keyword n)
243 <|> do sym <- stringLiteral
244 return (Symbol sym)
245 <?> "syntax symbol"
247{- | Parses a function declaration with possible syntax sugar
248 FunDecl ::= FunDecl';
249-}
250fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
251fnDecl syn = try (do notEndBlock
252 d <- fnDecl' syn
253 i <- get
254 let d' = fmap (desugar syn i) d
255 return [d']) <?> "function declaration"
257{- Parses a function declaration
258 FunDecl' ::=
259 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
260 | Postulate
261 | Pattern
262 | CAF
263 ;
264-}
265fnDecl' :: SyntaxInfo -> IdrisParser PDecl
266fnDecl' syn = checkFixity $
267 do (doc, fc, opts', n, acc) <- try (do
268 doc <- option "" (docComment '|')
269 pushIndent
270 ist <- get
271 let initOpts = if default_total ist
272 then [TotalFn]
273 else []
274 opts <- fnOpts initOpts
275 acc <- optional accessibility
276 opts' <- fnOpts opts
277 n_in <- fnName
278 let n = expandNS syn n_in
279 fc <- getFC
280 lchar ':'
281 return (doc, fc, opts', n, acc))
282 ty <- typeExpr (allowImp syn)
283 terminator
284 addAcc n acc
285 return (PTy doc syn fc opts' n ty)
286 <|> postulate syn
287 <|> caf syn
288 <|> pattern syn
289 <?> "function declaration"
290 where checkFixity :: IdrisParser PDecl -> IdrisParser PDecl
291 checkFixity p = do decl <- p
292 case getName decl of
293 Nothing -> return decl
294 Just n -> do fOk <- fixityOK n
295 unless fOk . fail $
296 "Missing fixity declaration for " ++ show n
297 return decl
298 getName (PTy _ _ _ _ n _) = Just n
299 getName _ = Nothing
300 fixityOK (NS n _) = fixityOK n
301 fixityOK (UN n) | all (flip elem opChars) n =
302 do fixities <- fmap idris_infixes get
303 return . elem n . map (\ (Fix _ op) -> op) $ fixities
304 | otherwise = return True
305 fixityOK _ = return True
307{- Parses function options given initial options
308FnOpts ::= 'total'
309 | 'partial'
310 | 'implicit'
311 | '%' 'assert_total'
312 | '%' 'reflection'
313 | '%' 'specialise' '[' NameTimesList? ']'
314 ;
316NameTimes ::= FnName Natural?;
318NameTimesList ::=
319 NameTimes
320 | NameTimes ',' NameTimesList
321 ;
323-}
324-- FIXME: Check compatability for function options (i.e. partal/total)
325fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
326fnOpts opts
327 = do reserved "total"; fnOpts (TotalFn : opts)
328 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
329 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;
330 fnOpts (CExport c : opts)
331 <|> do try (lchar '%' *> reserved "assert_total");
332 fnOpts (AssertTotal : opts)
333 <|> do try (lchar '%' *> reserved "reflection");
334 fnOpts (Reflection : opts)
335 <|> do lchar '%'; reserved "specialise";
336 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
337 fnOpts (Specialise ns : opts)
338 <|> do reserved "implicit"; fnOpts (Implicit : opts)
339 <|> return opts
340 <?> "function modifier"
341 where nameTimes :: IdrisParser (Name, Maybe Int)
342 nameTimes = do n <- fnName
343 t <- option Nothing (do reds <- natural
344 return (Just (fromInteger reds)))
345 return (n, t)
347{- | Parses a postulate
349Postulate ::=
350 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
351 ;
352-}
353postulate :: SyntaxInfo -> IdrisParser PDecl
354postulate syn = do doc <- try $ do doc <- option "" (docComment '|')
355 pushIndent
356 reserved "postulate"
357 return doc
358 ist <- get
359 let initOpts = if default_total ist
360 then [TotalFn]
361 else []
362 opts <- fnOpts initOpts
363 acc <- optional accessibility
364 opts' <- fnOpts opts
365 n_in <- fnName
366 let n = expandNS syn n_in
367 lchar ':'
368 ty <- typeExpr (allowImp syn)
369 fc <- getFC
370 terminator
371 addAcc n acc
372 return (PPostulate doc syn fc opts' n ty)
373 <?> "postulate"
375{- | Parses a using declaration
377Using ::=
378 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
379 ;
380 -}
381using_ :: SyntaxInfo -> IdrisParser [PDecl]
382using_ syn =
383 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
384 openBlock
385 let uvars = using syn
386 ds <- many (decl (syn { using = uvars ++ ns }))
387 closeBlock
388 return (concat ds)
389 <?> "using declaration"
391{- | Parses a parameters declaration
393Params ::=
394 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
395 ;
396 -}
397params :: SyntaxInfo -> IdrisParser [PDecl]
398params syn =
399 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
400 openBlock
401 let pvars = syn_params syn
402 ds <- many (decl syn { syn_params = pvars ++ ns })
403 closeBlock
404 fc <- getFC
405 return [PParams fc ns (concat ds)]
406 <?> "parameters declaration"
408{- | Parses a mutual declaration (for mutually recursive functions)
410Mutual ::=
411 'mutual' OpenBlock Decl* CloseBlock
412 ;
413-}
414mutual :: SyntaxInfo -> IdrisParser [PDecl]
415mutual syn =
416 do reserved "mutual"
417 openBlock
418 let pvars = syn_params syn
419 ds <- many (decl syn)
420 closeBlock
421 fc <- getFC
422 return [PMutual fc (concat ds)]
423 <?> "mutual block"
425{- | Parses a namespace declaration
427Namespace ::=
428 'namespace' identifier OpenBlock Decl+ CloseBlock
429 ;
430-}
431namespace :: SyntaxInfo -> IdrisParser [PDecl]
432namespace syn =
433 do reserved "namespace"; n <- identifier;
434 openBlock
435 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
436 closeBlock
437 return [PNamespace n (concat ds)]
438 <?> "namespace declaration"
440{- |Parses a methods block (for instances)
441 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
442 -}
443instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
444instanceBlock syn = do reserved "where"
445 openBlock
446 ds <- many (fnDecl syn)
447 closeBlock
448 return (concat ds)
449 <?> "instance block"
451{- |Parses a methods and instances block (for type classes)
453MethodOrInstance ::=
454 FnDecl
455 | Instance
456 ;
458ClassBlock ::=
459 'where' OpenBlock MethodOrInstance* CloseBlock
460 ;
461-}
462classBlock :: SyntaxInfo -> IdrisParser [PDecl]
463classBlock syn = do reserved "where"
464 openBlock
465 ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)
466 closeBlock
467 return (concat ds)
468 <?> "class block"
470{- |Parses a type class declaration
472ClassArgument ::=
473 Name
474 | '(' Name ':' Expr ')'
475 ;
477Class ::=
478 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
479 ;
480-}
481class_ :: SyntaxInfo -> IdrisParser [PDecl]
482class_ syn = do (doc, acc) <- try (do
483 doc <- option "" (docComment '|')
484 acc <- optional accessibility
485 return (doc, acc))
486 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- name
487 let n = expandNS syn n_in
488 cs <- many carg
489 ds <- option [] (classBlock syn)
490 accData acc n (concatMap declared ds)
491 return [PClass doc syn fc cons n cs ds]
492 <?> "type-class declaration"
493 where
494 carg :: IdrisParser (Name, PTerm)
495 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
496 return (i, ty)
497 <|> do i <- name;
498 return (i, PType)
500{- |Parses a type class instance declaration
502 Instance ::=
503 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
504 ;
506 InstanceName ::= '[' Name ']';
507-}
508instance_ :: SyntaxInfo -> IdrisParser [PDecl]
509instance_ syn = do reserved "instance"; fc <- getFC
510 en <- optional instanceName
511 cs <- constraintList syn
512 cn <- name
513 args <- many (simpleExpr syn)
514 let sc = PApp fc (PRef fc cn) (map pexp args)
515 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
516 ds <- option [] (instanceBlock syn)
517 return [PInstance syn fc cs cn args t en ds]
518 <?> "instance declaration"
519 where instanceName :: IdrisParser Name
520 instanceName = do lchar '['; n_in <- fnName; lchar ']'
521 let n = expandNS syn n_in
522 return n
523 <?> "instance name"
526{- | Parses a using declaration list
527UsingDeclList ::=
528 UsingDeclList'
529 | NameList TypeSig
530 ;
532UsingDeclList' ::=
533 UsingDecl
534 | UsingDecl ',' UsingDeclList'
535 ;
537NameList ::=
538 Name
539 | Name ',' NameList
540 ;
541-}
542usingDeclList :: SyntaxInfo -> IdrisParser [Using]
543usingDeclList syn
544 = try (sepBy1 (usingDecl syn) (lchar ','))
545 <|> do ns <- sepBy1 name (lchar ',')
546 lchar ':'
547 t <- typeExpr (disallowImp syn)
548 return (map (\x -> UImplicit x t) ns)
549 <?> "using declaration list"
551{- |Parses a using declaration
552UsingDecl ::=
553 FnName TypeSig
554 | FnName FnName+
555 ;
556-}
557usingDecl :: SyntaxInfo -> IdrisParser Using
558usingDecl syn = try (do x <- fnName
559 lchar ':'
560 t <- typeExpr (disallowImp syn)
561 return (UImplicit x t))
562 <|> do c <- fnName
563 xs <- some fnName
564 return (UConstraint c xs)
565 <?> "using declaration"
567{- | Parse a clause with patterns
568Pattern ::= Clause;
569-}
570pattern :: SyntaxInfo -> IdrisParser PDecl
571pattern syn = do fc <- getFC
572 clause <- clause syn
573 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
574 <?> "pattern"
576{- | Parse a constant applicative form declaration
577 CAF ::= 'let' FnName '=' Expr Terminator;
578-}
579caf :: SyntaxInfo -> IdrisParser PDecl
580caf syn = do reserved "let"
581 n_in <- fnName; let n = expandNS syn n_in
582 lchar '='
583 t <- expr syn
584 terminator
585 fc <- getFC
586 return (PCAF fc n t)
587 <?> "constant applicative form declaration"
589{- | Parse an argument expression
590 ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
591-}
592argExpr :: SyntaxInfo -> IdrisParser PTerm
593argExpr syn = let syn' = syn { inPattern = True } in
594 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
595 <?> "argument expression"
597{- | Parse a right hand side of a function
598RHS ::= '=' Expr
599 | '?=' RHSName? Expr
600 | 'impossible'
601 ;
603RHSName ::= '{' FnName '}';
604-}
605rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
606rhs syn n = do lchar '='; expr syn
607 <|> do symbol "?=";
608 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
609 return n)
610 r <- expr syn
611 return (addLet name r)
612 <|> do reserved "impossible"; return PImpossible
613 <?> "function right hand side"
614 where mkN :: Name -> Name
615 mkN (UN x) = UN (x++"_lemma_1")
616 mkN (NS x n) = NS (mkN x) n
617 n' :: Name
618 n' = mkN n
619 addLet :: Name -> PTerm -> PTerm
620 addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)
621 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
622 where addLetC (l, r) = (l, addLet nm r)
623 addLet nm r = (PLet (UN "value") Placeholder r (PMetavar nm))
625{- |Parses a function clause
626RHSOrWithBlock ::= RHS WhereOrTerminator
627 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
628 ;
629Clause ::= WExpr+ RHSOrWithBlock
630 | SimpleExpr '<==' FnName RHS WhereOrTerminator
631 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
632 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
633 ;
634ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
635WhereOrTerminator ::= WhereBlock | Terminator;
636-}
637clause :: SyntaxInfo -> IdrisParser PClause
638clause syn
639 = do wargs <- try (do pushIndent; some (wExpr syn))
640 fc <- getFC
641 ist <- get
642 n <- case lastParse ist of
643 Just t -> return t
644 Nothing -> fail "Invalid clause"
645 (do r <- rhs syn n
646 let ctxt = tt_ctxt ist
647 let wsyn = syn { syn_namespace = [] }
648 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
649 popIndent
650 return x,
651 do terminator
652 return ([], [])]
653 return $ PClauseR fc wargs r wheres) <|> (do
654 popIndent
655 reserved "with"
656 wval <- simpleExpr syn
657 openBlock
658 ds <- some $ fnDecl syn
659 let withs = concat ds
660 closeBlock
661 return $ PWithR fc wargs wval withs)
662 <|> do ty <- try (do pushIndent
663 ty <- simpleExpr syn
664 symbol "<=="
665 return ty)
666 fc <- getFC
667 n_in <- fnName; let n = expandNS syn n_in
668 r <- rhs syn n
669 ist <- get
670 let ctxt = tt_ctxt ist
671 let wsyn = syn { syn_namespace = [] }
672 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
673 popIndent
674 return x,
675 do terminator
676 return ([], [])]
677 let capp = PLet (MN 0 "match")
678 ty
679 (PMatchApp fc n)
680 (PRef fc (MN 0 "match"))
681 ist <- get
682 put (ist { lastParse = Just n })
683 return $ PClause fc n capp [] r wheres
684 <|> do (l, op) <- try (do
685 pushIndent
686 l <- argExpr syn
687 op <- operator
688 when (op == "=" || op == "?=" ) $
689 fail "infix clause definition with \"=\" and \"?=\" not supported "
690 return (l, op))
691 let n = expandNS syn (UN op)
692 r <- argExpr syn
693 fc <- getFC
694 wargs <- many (wExpr syn)
695 (do rs <- rhs syn n
696 let wsyn = syn { syn_namespace = [] }
697 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
698 popIndent
699 return x,
700 do terminator
701 return ([], [])]
702 ist <- get
703 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
704 put (ist { lastParse = Just n })
705 return $ PClause fc n capp wargs rs wheres) <|> (do
706 popIndent
707 reserved "with"
708 lchar '(' <?> "parenthesized expression"
709 wval <- bracketed syn
710 openBlock
711 ds <- some $ fnDecl syn
712 closeBlock
713 ist <- get
714 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
715 let withs = map (fillLHSD n capp wargs) $ concat ds
716 put (ist { lastParse = Just n })
717 return $ PWith fc n capp wargs wval withs)
718 <|> do pushIndent
719 n_in <- fnName; let n = expandNS syn n_in
720 cargs <- many (constraintArg syn)
721 fc <- getFC
722 args <- many (try (implicitArg (syn { inPattern = True } ))
723 <|> (fmap pexp (argExpr syn)))
724 wargs <- many (wExpr syn)
725 let capp = PApp fc (PRef fc n)
726 (cargs ++ args)
727 (do r <- rhs syn n
728 ist <- get
729 let ctxt = tt_ctxt ist
730 let wsyn = syn { syn_namespace = [] }
731 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
732 popIndent
733 return x,
734 do terminator
735 return ([], [])]
736 ist <- get
737 put (ist { lastParse = Just n })
738 return $ PClause fc n capp wargs r wheres) <|> (do
739 reserved "with"
740 ist <- get
741 put (ist { lastParse = Just n })
742 lchar '(' <?> "parenthesized expression"
743 wval <- bracketed syn
744 openBlock
745 ds <- some $ fnDecl syn
746 let withs = map (fillLHSD n capp wargs) $ concat ds
747 closeBlock
748 popIndent
749 return $ PWith fc n capp wargs wval withs)
750 <?> "function clause"
751 where
752 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
753 fillLHS n capp owargs (PClauseR fc wargs v ws)
754 = PClause fc n capp (owargs ++ wargs) v ws
755 fillLHS n capp owargs (PWithR fc wargs v ws)
756 = PWith fc n capp (owargs ++ wargs) v
757 (map (fillLHSD n capp (owargs ++ wargs)) ws)
758 fillLHS _ _ _ c = c
760 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
761 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
762 fillLHSD n c a x = x
764{- |Parses with pattern
765 WExpr ::= '|' Expr';
766-}
767wExpr :: SyntaxInfo -> IdrisParser PTerm
768wExpr syn = do lchar '|'
769 expr' syn
770 <?> "with pattern"
772{- |Parses a where block
773WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
774 -}
775whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
776whereBlock n syn
777 = do reserved "where"
778 ds <- indentedBlock1 (decl syn)
779 let dns = concatMap (concatMap declared) ds
780 return (concat ds, map (\x -> (x, decoration syn x)) dns)
781 <?> "where block"
783{- |Parses a code generation target language name
784Codegen ::= 'C'
785 | 'Java'
786 | 'JavaScript'
787 | 'Node'
788 | 'LLVM'
789 | 'Bytecode'
790 ;
791-}
792codegen_ :: IdrisParser Codegen
793codegen_ = do reserved "C"; return ViaC
794 <|> do reserved "Java"; return ViaJava
795 <|> do reserved "JavaScript"; return ViaJavaScript
796 <|> do reserved "Node"; return ViaNode
797 <|> do reserved "LLVM"; return ViaLLVM
798 <|> do reserved "Bytecode"; return Bytecode
799 <?> "code generation language"
801{- |Parses a compiler directive
802StringList ::=
803 String
804 | String ',' StringList
805 ;
807Directive ::= '%' Directive';
809Directive' ::= 'lib' CodeGen String_t
810 | 'link' CodeGen String_t
811 | 'flag' CodeGen String_t
812 | 'include' CodeGen String_t
813 | 'hide' Name
814 | 'freeze' Name
815 | 'access' Accessibility
816 | 'default' Totality
817 | 'logging' Natural
818 | 'dynamic' StringList
819 | 'name' Name NameList
820 | 'language' 'TypeProviders'
821 | 'language' 'ErrorReflection'
822 ;
823-}
824directive :: SyntaxInfo -> IdrisParser [PDecl]
825directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
826 return [PDirective (do addLib cgn lib
827 addIBC (IBCLib cgn lib))]
828 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
829 return [PDirective (do dirs <- allImportDirs
830 o <- liftIO $ findInPath dirs obj
831 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
832 addObjectFile cgn o)]
833 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
834 flag <- stringLiteral
835 return [PDirective (do addIBC (IBCCGFlag cgn flag)
836 addFlag cgn flag)]
837 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
838 return [PDirective (do addHdr cgn hdr
839 addIBC (IBCHeader cgn hdr))]
840 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
841 return [PDirective (do setAccessibility n Hidden
842 addIBC (IBCAccess n Hidden))]
843 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
844 return [PDirective (do setAccessibility n Frozen
845 addIBC (IBCAccess n Frozen))]
846 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
847 return [PDirective (do i <- get
848 put(i { default_access = acc }))]
849 <|> do try (lchar '%' *> reserved "default"); tot <- totality
850 i <- get
851 put (i { default_total = tot } )
852 return [PDirective (do i <- get
853 put(i { default_total = tot }))]
854 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
855 return [PDirective (setLogLevel (fromInteger i))]
856 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
857 return [PDirective (do added <- addDyLib libs
858 case added of
859 Left lib -> addIBC (IBCDyLib (lib_name lib))
860 Right msg ->
861 fail $ msg)]
862 <|> do try (lchar '%' *> reserved "name")
863 ty <- iName []
864 ns <- sepBy1 name (lchar ',')
865 return [PDirective
866 (do mapM_ (addNameHint ty) ns
867 mapM_ (\n -> addIBC (IBCNameHint (ty, n))) ns)]
868 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
869 return [PDirective (addLangExt ext)]
870 <?> "directive"
872pLangExt :: IdrisParser LanguageExt
873pLangExt = (reserved "TypeProviders" >> return TypeProviders)
874 <|> (reserved "ErrorReflection" >> return ErrorReflection)
876{- | Parses a totality
877Totality ::= 'partial' | 'total'
878-}
879totality :: IdrisParser Bool
880totality
881 = do reserved "total"; return True
882 <|> do reserved "partial"; return False
884{- | Parses a type provider
885Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;
886 -}
887provider :: SyntaxInfo -> IdrisParser [PDecl]
888provider syn = do try (lchar '%' *> reserved "provide");
889 lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
890 fc <- getFC
891 reserved "with"
892 e <- expr syn
893 return [PProvider syn fc n t e]
894 <?> "type provider"
896{- | Parses a transform
897Transform ::= '%' 'transform' Expr '==>' Expr
898-}
899transform :: SyntaxInfo -> IdrisParser [PDecl]
900transform syn = do try (lchar '%' *> reserved "transform")
901 -- leave it unchecked, until we work out what this should
902 -- actually mean...
903-- safety <- option True (do reserved "unsafe"
904-- return False)
905 l <- expr syn
906 fc <- getFC
907 symbol "==>"
908 r <- expr syn
909 return [PTransform fc False l r]
910 <?> "transform"
913{- * Loading and parsing -}
914{- | Parses an expression from input -}
915parseExpr :: IState -> String -> Result PTerm
916parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
918{- | Parses a tactic from input -}
919parseTactic :: IState -> String -> Result PTactic
920parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
922-- | Parse module header and imports
923parseImports :: FilePath -> String -> Idris ([String], [String], Maybe Delta)
924parseImports fname input
925 = do i <- getIState
926 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
927 Failure err -> fail (show err)
928 Success (x, i) -> do -- Discard state updates (there should be
929 -- none anyway)
930 return x
931 where imports :: IdrisParser (([String], [String], Maybe Delta), IState)
932 imports = do whiteSpace
933 mname <- moduleHeader
934 ps <- many import_
935 mrk <- mark
936 isEof <- lookAheadMatches eof
937 let mrk' = if isEof
938 then Nothing
939 else Just mrk
940 i <- get
941 return ((mname, ps, mrk'), i)
943-- | There should be a better way of doing this...
944findFC :: Doc -> (FC, String)
945findFC x = let s = show (plain x) in
946 case span (/= ':') s of
947 (failname, ':':rest) -> case span isDigit rest of
948 (line, ':':rest') -> (FC failname (read line) 0, drop 2 (dropWhile (/= ':') rest'))
950-- | A program is a list of declarations, possibly with associated
951-- documentation strings.
952parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
953 Idris [PDecl]
954parseProg syn fname input mrk
955 = do i <- getIState
956 case runparser mainProg i fname input of
957 Failure doc -> do -- FIXME: Get error location from trifecta
958 -- this can't be the solution!
959 let (fc, msg) = findFC doc
960 i <- getIState
961 case idris_outputmode i of
962 RawOutput -> ihputStrLn (idris_outh i) (show doc)
963 IdeSlave n -> ihWarn (idris_outh i) fc msg
964 putIState (i { errLine = Just (fc_line fc) }) -- Just errl })
965 return []
966 Success (x, i) -> do putIState i
967 return $ collect x
968 where mainProg :: IdrisParser ([PDecl], IState)
969 mainProg = case mrk of
970 Nothing -> do i <- get; return ([], i)
971 Just mrk -> do
972 release mrk
973 ds <- prog syn
974 i' <- get
975 return (ds, i')
977{- | Load idris module and show error if something wrong happens -}
978loadModule :: Handle -> FilePath -> Idris String
979loadModule outh f
980 = idrisCatch (loadModule' outh f)
981 (\e -> do setErrLine (getErrLine e)
982 ist <- getIState
983 msg <- showErr e
984 ihputStrLn outh msg
985 return "")
987{- | Load idris module -}
988loadModule' :: Handle -> FilePath -> Idris String
989loadModule' outh f
990 = do i <- getIState
991 let file = takeWhile (/= ' ') f
992 ibcsd <- valIBCSubDir i
993 ids <- allImportDirs
994 fp <- liftIO $ findImport ids ibcsd file
995 if file `elem` imported i
996 then iLOG $ "Already read " ++ file
997 else do putIState (i { imported = file : imported i })
998 case fp of
999 IDR fn -> loadSource outh False fn
1000 LIDR fn -> loadSource outh True fn
1001 IBC fn src ->
1002 idrisCatch (loadIBC fn)
1003 (\c -> do iLOG $ fn ++ " failed " ++ show c
1004 case src of
1005 IDR sfn -> loadSource outh False sfn
1006 LIDR sfn -> loadSource outh True sfn)
1007 let (dir, fh) = splitFileName file
1008 return (dropExtension fh)
1011{- | Load idris code from file -}
1012loadFromIFile :: Handle -> IFileType -> Idris ()
1013loadFromIFile h i@(IBC fn src)
1014 = do iLOG $ "Skipping " ++ getSrcFile i
1015 idrisCatch (loadIBC fn)
1016 (\err -> ierror $ LoadingFailed fn err)
1017 where
1018 getSrcFile (IDR fn) = fn
1019 getSrcFile (LIDR fn) = fn
1020 getSrcFile (IBC f src) = getSrcFile src
1022loadFromIFile h (IDR fn) = loadSource' h False fn
1023loadFromIFile h (LIDR fn) = loadSource' h True fn
1025{-| Load idris source code and show error if something wrong happens -}
1026loadSource' :: Handle -> Bool -> FilePath -> Idris ()
1027loadSource' h lidr r
1028 = idrisCatch (loadSource h lidr r)
1029 (\e -> do setErrLine (getErrLine e)
1030 msg <- showErr e
1031 ihputStrLn h msg)
1033{- | Load Idris source code-}
1034loadSource :: Handle -> Bool -> FilePath -> Idris ()
1035loadSource h lidr f
1036 = do iLOG ("Reading " ++ f)
1037 i <- getIState
1038 let def_total = default_total i
1039 file_in <- runIO $ readFile f
1040 file <- if lidr then tclift $ unlit f file_in else return file_in
1041 (mname, modules, pos) <- parseImports f file
1042 i <- getIState
1043 putIState (i { default_access = Hidden })
1044 clearIBC -- start a new .ibc file
1045 mapM_ (addIBC . IBCImport) modules
1046 ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
1047 f file pos
1048 unless (null ds') $ do
1049 let ds = namespaces mname ds'
1050 logLvl 3 (showDecls True ds)
1051 i <- getIState
1052 logLvl 10 (show (toAlist (idris_implicits i)))
1053 logLvl 3 (show (idris_infixes i))
1054 -- Now add all the declarations to the context
1055 v <- verbose
1056 when v $ ihputStrLn h $ "Type checking " ++ f
1057 -- we totality check after every Mutual block, so if
1058 -- anything is a single definition, wrap it in a
1059 -- mutual block on its own
1060 elabDecls toplevel (map toMutual ds)
1061 i <- getIState
1062 -- simplify every definition do give the totality checker
1063 -- a better chance
1064 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1065 updateContext (simplifyCasedef n))
1066 (map snd (idris_totcheck i))
1067 -- build size change graph from simplified definitions
1068 iLOG "Totality checking"
1069 i <- getIState
1070 mapM_ buildSCG (idris_totcheck i)
1071 mapM_ checkDeclTotality (idris_totcheck i)
1073 -- Redo totality check for deferred names
1074 let deftots = idris_defertotcheck i
1075 iLOG $ "Totality checking " ++ show deftots
1076 mapM_ (\x -> do tot <- getTotality x
1077 case tot of
1078 Total _ -> setTotality x Unchecked
1079 _ -> return ()) (map snd deftots)
1080 mapM_ buildSCG deftots
1081 mapM_ checkDeclTotality deftots
1083 iLOG ("Finished " ++ f)
1084 ibcsd <- valIBCSubDir i
1085 iLOG "Universe checking"
1086 iucheck
1087 let ibc = ibcPathNoFallback ibcsd f
1088 i <- getIState
1089 addHides (hide_list i)
1090 ok <- noErrors
1091 when ok $
1092 idrisCatch (do writeIBC f ibc; clearIBC)
1093 (\c -> return ()) -- failure is harmless
1094 i <- getIState
1095 putIState (i { default_total = def_total,
1096 hide_list = [] })
1097 return ()
1098 return ()
1099 where
1100 namespaces :: [String] -> [PDecl] -> [PDecl]
1101 namespaces [] ds = ds
1102 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1104 toMutual :: PDecl -> PDecl
1105 toMutual m@(PMutual _ d) = m
1106 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1107 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1108 case x of
1109 PClauses _ _ _ _ -> r
1110 PClass _ _ _ _ _ _ _ -> r
1111 PInstance _ _ _ _ _ _ _ _ -> r
1112 _ -> x
1114{- | Adds names to hide list -}
1115addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1116addHides xs = do i <- getIState
1117 let defh = default_access i
1118 let (hs, as) = partition isNothing xs
1119 unless (null as) $
1120 mapM_ doHide
1121 (map (\ (n, _) -> (n, defh)) hs ++
1122 map (\ (n, Just a) -> (n, a)) as)
1123 where isNothing (_, Nothing) = True
1124 isNothing _ = False
1126 doHide (n, a) = do setAccessibility n a
1127 addIBC (IBCAccess n a)