git.iko.soy/Idris-dev
on d66da21 help sign in
Idris-dev/src/Idris/Parser.hs
1108 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 type classes and instances)
441 MethodsBlock ::= 'where' OpenBlock FnDecl* CloseBlock
442 -}
443methodsBlock :: SyntaxInfo -> IdrisParser [PDecl]
444methodsBlock syn = do reserved "where"
445 openBlock
446 ds <- many (fnDecl syn)
447 closeBlock
448 return (concat ds)
449 <?> "methods block"
451{- |Parses a type class declaration
453ClassArgument ::=
454 Name
455 | '(' Name ':' Expr ')'
456 ;
458Class ::=
459 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* MethodsBlock?
460 ;
461-}
462class_ :: SyntaxInfo -> IdrisParser [PDecl]
463class_ syn = do (doc, acc) <- try (do
464 doc <- option "" (docComment '|')
465 acc <- optional accessibility
466 return (doc, acc))
467 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- name
468 let n = expandNS syn n_in
469 cs <- many carg
470 ds <- option [] (methodsBlock syn)
471 accData acc n (concatMap declared ds)
472 return [PClass doc syn fc cons n cs ds]
473 <?> "type-class declaration"
474 where
475 carg :: IdrisParser (Name, PTerm)
476 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
477 return (i, ty)
478 <|> do i <- name;
479 return (i, PType)
481{- |Parses a type class instance declaration
483 Instance ::=
484 'instance' InstanceName? ConstraintList? Name SimpleExpr* MethodsBlock?
485 ;
487 InstanceName ::= '[' Name ']';
488-}
489instance_ :: SyntaxInfo -> IdrisParser [PDecl]
490instance_ syn = do reserved "instance"; fc <- getFC
491 en <- optional instanceName
492 cs <- constraintList syn
493 cn <- name
494 args <- many (simpleExpr syn)
495 let sc = PApp fc (PRef fc cn) (map pexp args)
496 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
497 ds <- option [] (methodsBlock syn)
498 return [PInstance syn fc cs cn args t en ds]
499 <?> "instance declaratioN"
500 where instanceName :: IdrisParser Name
501 instanceName = do lchar '['; n_in <- fnName; lchar ']'
502 let n = expandNS syn n_in
503 return n
504 <?> "instance name"
507{- | Parses a using declaration list
508UsingDeclList ::=
509 UsingDeclList'
510 | NameList TypeSig
511 ;
513UsingDeclList' ::=
514 UsingDecl
515 | UsingDecl ',' UsingDeclList'
516 ;
518NameList ::=
519 Name
520 | Name ',' NameList
521 ;
522-}
523usingDeclList :: SyntaxInfo -> IdrisParser [Using]
524usingDeclList syn
525 = try (sepBy1 (usingDecl syn) (lchar ','))
526 <|> do ns <- sepBy1 name (lchar ',')
527 lchar ':'
528 t <- typeExpr (disallowImp syn)
529 return (map (\x -> UImplicit x t) ns)
530 <?> "using declaration list"
532{- |Parses a using declaration
533UsingDecl ::=
534 FnName TypeSig
535 | FnName FnName+
536 ;
537-}
538usingDecl :: SyntaxInfo -> IdrisParser Using
539usingDecl syn = try (do x <- fnName
540 lchar ':'
541 t <- typeExpr (disallowImp syn)
542 return (UImplicit x t))
543 <|> do c <- fnName
544 xs <- some fnName
545 return (UConstraint c xs)
546 <?> "using declaration"
548{- | Parse a clause with patterns
549Pattern ::= Clause;
550-}
551pattern :: SyntaxInfo -> IdrisParser PDecl
552pattern syn = do fc <- getFC
553 clause <- clause syn
554 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
555 <?> "pattern"
557{- | Parse a constant applicative form declaration
558 CAF ::= 'let' FnName '=' Expr Terminator;
559-}
560caf :: SyntaxInfo -> IdrisParser PDecl
561caf syn = do reserved "let"
562 n_in <- fnName; let n = expandNS syn n_in
563 lchar '='
564 t <- expr syn
565 terminator
566 fc <- getFC
567 return (PCAF fc n t)
568 <?> "constant applicative form declaration"
570{- | Parse an argument expression
571 ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
572-}
573argExpr :: SyntaxInfo -> IdrisParser PTerm
574argExpr syn = let syn' = syn { inPattern = True } in
575 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
576 <?> "argument expression"
578{- | Parse a right hand side of a function
579RHS ::= '=' Expr
580 | '?=' RHSName? Expr
581 | 'impossible'
582 ;
584RHSName ::= '{' FnName '}';
585-}
586rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
587rhs syn n = do lchar '='; expr syn
588 <|> do symbol "?=";
589 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
590 return n)
591 r <- expr syn
592 return (addLet name r)
593 <|> do reserved "impossible"; return PImpossible
594 <?> "function right hand side"
595 where mkN :: Name -> Name
596 mkN (UN x) = UN (x++"_lemma_1")
597 mkN (NS x n) = NS (mkN x) n
598 n' :: Name
599 n' = mkN n
600 addLet :: Name -> PTerm -> PTerm
601 addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)
602 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
603 where addLetC (l, r) = (l, addLet nm r)
604 addLet nm r = (PLet (UN "value") Placeholder r (PMetavar nm))
606{- |Parses a function clause
607RHSOrWithBlock ::= RHS WhereOrTerminator
608 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
609 ;
610Clause ::= WExpr+ RHSOrWithBlock
611 | SimpleExpr '<==' FnName RHS WhereOrTerminator
612 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
613 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
614 ;
615ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
616WhereOrTerminator ::= WhereBlock | Terminator;
617-}
618clause :: SyntaxInfo -> IdrisParser PClause
619clause syn
620 = do wargs <- try (do pushIndent; some (wExpr syn))
621 fc <- getFC
622 ist <- get
623 n <- case lastParse ist of
624 Just t -> return t
625 Nothing -> fail "Invalid clause"
626 (do r <- rhs syn n
627 let ctxt = tt_ctxt ist
628 let wsyn = syn { syn_namespace = [] }
629 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
630 popIndent
631 return x,
632 do terminator
633 return ([], [])]
634 return $ PClauseR fc wargs r wheres) <|> (do
635 popIndent
636 reserved "with"
637 wval <- simpleExpr syn
638 openBlock
639 ds <- some $ fnDecl syn
640 let withs = concat ds
641 closeBlock
642 return $ PWithR fc wargs wval withs)
643 <|> do ty <- try (do pushIndent
644 ty <- simpleExpr syn
645 symbol "<=="
646 return ty)
647 fc <- getFC
648 n_in <- fnName; let n = expandNS syn n_in
649 r <- rhs syn n
650 ist <- get
651 let ctxt = tt_ctxt ist
652 let wsyn = syn { syn_namespace = [] }
653 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
654 popIndent
655 return x,
656 do terminator
657 return ([], [])]
658 let capp = PLet (MN 0 "match")
659 ty
660 (PMatchApp fc n)
661 (PRef fc (MN 0 "match"))
662 ist <- get
663 put (ist { lastParse = Just n })
664 return $ PClause fc n capp [] r wheres
665 <|> do (l, op) <- try (do
666 pushIndent
667 l <- argExpr syn
668 op <- operator
669 when (op == "=" || op == "?=" ) $
670 fail "infix clause definition with \"=\" and \"?=\" not supported "
671 return (l, op))
672 let n = expandNS syn (UN op)
673 r <- argExpr syn
674 fc <- getFC
675 wargs <- many (wExpr syn)
676 (do rs <- rhs syn n
677 let wsyn = syn { syn_namespace = [] }
678 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
679 popIndent
680 return x,
681 do terminator
682 return ([], [])]
683 ist <- get
684 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
685 put (ist { lastParse = Just n })
686 return $ PClause fc n capp wargs rs wheres) <|> (do
687 popIndent
688 reserved "with"
689 lchar '(' <?> "parenthesized expression"
690 wval <- bracketed syn
691 openBlock
692 ds <- some $ fnDecl syn
693 closeBlock
694 ist <- get
695 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
696 let withs = map (fillLHSD n capp wargs) $ concat ds
697 put (ist { lastParse = Just n })
698 return $ PWith fc n capp wargs wval withs)
699 <|> do pushIndent
700 n_in <- fnName; let n = expandNS syn n_in
701 cargs <- many (constraintArg syn)
702 fc <- getFC
703 args <- many (try (implicitArg (syn { inPattern = True } ))
704 <|> (fmap pexp (argExpr syn)))
705 wargs <- many (wExpr syn)
706 let capp = PApp fc (PRef fc n)
707 (cargs ++ args)
708 (do r <- rhs syn n
709 ist <- get
710 let ctxt = tt_ctxt ist
711 let wsyn = syn { syn_namespace = [] }
712 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
713 popIndent
714 return x,
715 do terminator
716 return ([], [])]
717 ist <- get
718 put (ist { lastParse = Just n })
719 return $ PClause fc n capp wargs r wheres) <|> (do
720 reserved "with"
721 ist <- get
722 put (ist { lastParse = Just n })
723 lchar '(' <?> "parenthesized expression"
724 wval <- bracketed syn
725 openBlock
726 ds <- some $ fnDecl syn
727 let withs = map (fillLHSD n capp wargs) $ concat ds
728 closeBlock
729 popIndent
730 return $ PWith fc n capp wargs wval withs)
731 <?> "function clause"
732 where
733 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
734 fillLHS n capp owargs (PClauseR fc wargs v ws)
735 = PClause fc n capp (owargs ++ wargs) v ws
736 fillLHS n capp owargs (PWithR fc wargs v ws)
737 = PWith fc n capp (owargs ++ wargs) v
738 (map (fillLHSD n capp (owargs ++ wargs)) ws)
739 fillLHS _ _ _ c = c
741 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
742 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
743 fillLHSD n c a x = x
745{- |Parses with pattern
746 WExpr ::= '|' Expr';
747-}
748wExpr :: SyntaxInfo -> IdrisParser PTerm
749wExpr syn = do lchar '|'
750 expr' syn
751 <?> "with pattern"
753{- |Parses a where block
754WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
755 -}
756whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
757whereBlock n syn
758 = do reserved "where"
759 ds <- indentedBlock1 (decl syn)
760 let dns = concatMap (concatMap declared) ds
761 return (concat ds, map (\x -> (x, decoration syn x)) dns)
762 <?> "where block"
764{- |Parses a code generation target language name
765Codegen ::= 'C'
766 | 'Java'
767 | 'JavaScript'
768 | 'Node'
769 | 'LLVM'
770 | 'Bytecode'
771 ;
772-}
773codegen_ :: IdrisParser Codegen
774codegen_ = do reserved "C"; return ViaC
775 <|> do reserved "Java"; return ViaJava
776 <|> do reserved "JavaScript"; return ViaJavaScript
777 <|> do reserved "Node"; return ViaNode
778 <|> do reserved "LLVM"; return ViaLLVM
779 <|> do reserved "Bytecode"; return Bytecode
780 <?> "code generation language"
782{- |Parses a compiler directive
783StringList ::=
784 String
785 | String ',' StringList
786 ;
788Directive ::= '%' Directive';
790Directive' ::= 'lib' CodeGen String_t
791 | 'link' CodeGen String_t
792 | 'flag' CodeGen String_t
793 | 'include' CodeGen String_t
794 | 'hide' Name
795 | 'freeze' Name
796 | 'access' Accessibility
797 | 'default' Totality
798 | 'logging' Natural
799 | 'dynamic' StringList
800 | 'name' Name NameList
801 | 'language' 'TypeProviders'
802 | 'language' 'ErrorReflection'
803 ;
804-}
805directive :: SyntaxInfo -> IdrisParser [PDecl]
806directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
807 return [PDirective (do addLib cgn lib
808 addIBC (IBCLib cgn lib))]
809 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
810 return [PDirective (do dirs <- allImportDirs
811 o <- liftIO $ findInPath dirs obj
812 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
813 addObjectFile cgn o)]
814 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
815 flag <- stringLiteral
816 return [PDirective (do addIBC (IBCCGFlag cgn flag)
817 addFlag cgn flag)]
818 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
819 return [PDirective (do addHdr cgn hdr
820 addIBC (IBCHeader cgn hdr))]
821 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
822 return [PDirective (do setAccessibility n Hidden
823 addIBC (IBCAccess n Hidden))]
824 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
825 return [PDirective (do setAccessibility n Frozen
826 addIBC (IBCAccess n Frozen))]
827 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
828 return [PDirective (do i <- get
829 put(i { default_access = acc }))]
830 <|> do try (lchar '%' *> reserved "default"); tot <- totality
831 i <- get
832 put (i { default_total = tot } )
833 return [PDirective (do i <- get
834 put(i { default_total = tot }))]
835 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
836 return [PDirective (setLogLevel (fromInteger i))]
837 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
838 return [PDirective (do added <- addDyLib libs
839 case added of
840 Left lib -> addIBC (IBCDyLib (lib_name lib))
841 Right msg ->
842 fail $ msg)]
843 <|> do try (lchar '%' *> reserved "name")
844 ty <- iName []
845 ns <- sepBy1 name (lchar ',')
846 return [PDirective
847 (do mapM_ (addNameHint ty) ns
848 mapM_ (\n -> addIBC (IBCNameHint (ty, n))) ns)]
849 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
850 return [PDirective (addLangExt ext)]
851 <?> "directive"
853pLangExt :: IdrisParser LanguageExt
854pLangExt = (reserved "TypeProviders" >> return TypeProviders)
855 <|> (reserved "ErrorReflection" >> return ErrorReflection)
857{- | Parses a totality
858Totality ::= 'partial' | 'total'
859-}
860totality :: IdrisParser Bool
861totality
862 = do reserved "total"; return True
863 <|> do reserved "partial"; return False
865{- | Parses a type provider
866Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;
867 -}
868provider :: SyntaxInfo -> IdrisParser [PDecl]
869provider syn = do try (lchar '%' *> reserved "provide");
870 lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
871 fc <- getFC
872 reserved "with"
873 e <- expr syn
874 return [PProvider syn fc n t e]
875 <?> "type provider"
877{- | Parses a transform
878Transform ::= '%' 'transform' Expr '==>' Expr
879-}
880transform :: SyntaxInfo -> IdrisParser [PDecl]
881transform syn = do try (lchar '%' *> reserved "transform")
882 -- leave it unchecked, until we work out what this should
883 -- actually mean...
884-- safety <- option True (do reserved "unsafe"
885-- return False)
886 l <- expr syn
887 fc <- getFC
888 symbol "==>"
889 r <- expr syn
890 return [PTransform fc False l r]
891 <?> "transform"
894{- * Loading and parsing -}
895{- | Parses an expression from input -}
896parseExpr :: IState -> String -> Result PTerm
897parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
899{- | Parses a tactic from input -}
900parseTactic :: IState -> String -> Result PTactic
901parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
903-- | Parse module header and imports
904parseImports :: FilePath -> String -> Idris ([String], [String], Maybe Delta)
905parseImports fname input
906 = do i <- getIState
907 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
908 Failure err -> fail (show err)
909 Success (x, i) -> do -- Discard state updates (there should be
910 -- none anyway)
911 return x
912 where imports :: IdrisParser (([String], [String], Maybe Delta), IState)
913 imports = do whiteSpace
914 mname <- moduleHeader
915 ps <- many import_
916 mrk <- mark
917 isEof <- lookAheadMatches eof
918 let mrk' = if isEof
919 then Nothing
920 else Just mrk
921 i <- get
922 return ((mname, ps, mrk'), i)
924-- | There should be a better way of doing this...
925findFC :: Doc -> (FC, String)
926findFC x = let s = show (plain x) in
927 case span (/= ':') s of
928 (failname, ':':rest) -> case span isDigit rest of
929 (line, ':':rest') -> (FC failname (read line) 0, drop 2 (dropWhile (/= ':') rest'))
931-- | A program is a list of declarations, possibly with associated
932-- documentation strings.
933parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
934 Idris [PDecl]
935parseProg syn fname input mrk
936 = do i <- getIState
937 case runparser mainProg i fname input of
938 Failure doc -> do -- FIXME: Get error location from trifecta
939 -- this can't be the solution!
940 let (fc, msg) = findFC doc
941 i <- getIState
942 case idris_outputmode i of
943 RawOutput -> ihputStrLn (idris_outh i) (show doc)
944 IdeSlave n -> ihWarn (idris_outh i) fc msg
945 putIState (i { errLine = Just (fc_line fc) }) -- Just errl })
946 return []
947 Success (x, i) -> do putIState i
948 return $ collect x
949 where mainProg :: IdrisParser ([PDecl], IState)
950 mainProg = case mrk of
951 Nothing -> do i <- get; return ([], i)
952 Just mrk -> do
953 release mrk
954 ds <- prog syn
955 i' <- get
956 return (ds, i')
958{- | Load idris module and show error if something wrong happens -}
959loadModule :: Handle -> FilePath -> Idris String
960loadModule outh f
961 = idrisCatch (loadModule' outh f)
962 (\e -> do setErrLine (getErrLine e)
963 ist <- getIState
964 msg <- showErr e
965 ihputStrLn outh msg
966 return "")
968{- | Load idris module -}
969loadModule' :: Handle -> FilePath -> Idris String
970loadModule' outh f
971 = do i <- getIState
972 let file = takeWhile (/= ' ') f
973 ibcsd <- valIBCSubDir i
974 ids <- allImportDirs
975 fp <- liftIO $ findImport ids ibcsd file
976 if file `elem` imported i
977 then iLOG $ "Already read " ++ file
978 else do putIState (i { imported = file : imported i })
979 case fp of
980 IDR fn -> loadSource outh False fn
981 LIDR fn -> loadSource outh True fn
982 IBC fn src ->
983 idrisCatch (loadIBC fn)
984 (\c -> do iLOG $ fn ++ " failed " ++ show c
985 case src of
986 IDR sfn -> loadSource outh False sfn
987 LIDR sfn -> loadSource outh True sfn)
988 let (dir, fh) = splitFileName file
989 return (dropExtension fh)
992{- | Load idris code from file -}
993loadFromIFile :: Handle -> IFileType -> Idris ()
994loadFromIFile h i@(IBC fn src)
995 = do iLOG $ "Skipping " ++ getSrcFile i
996 idrisCatch (loadIBC fn)
997 (\err -> ierror $ LoadingFailed fn err)
998 where
999 getSrcFile (IDR fn) = fn
1000 getSrcFile (LIDR fn) = fn
1001 getSrcFile (IBC f src) = getSrcFile src
1003loadFromIFile h (IDR fn) = loadSource' h False fn
1004loadFromIFile h (LIDR fn) = loadSource' h True fn
1006{-| Load idris source code and show error if something wrong happens -}
1007loadSource' :: Handle -> Bool -> FilePath -> Idris ()
1008loadSource' h lidr r
1009 = idrisCatch (loadSource h lidr r)
1010 (\e -> do setErrLine (getErrLine e)
1011 msg <- showErr e
1012 ihputStrLn h msg)
1014{- | Load Idris source code-}
1015loadSource :: Handle -> Bool -> FilePath -> Idris ()
1016loadSource h lidr f
1017 = do iLOG ("Reading " ++ f)
1018 i <- getIState
1019 let def_total = default_total i
1020 file_in <- runIO $ readFile f
1021 file <- if lidr then tclift $ unlit f file_in else return file_in
1022 (mname, modules, pos) <- parseImports f file
1023 i <- getIState
1024 putIState (i { default_access = Hidden })
1025 clearIBC -- start a new .ibc file
1026 mapM_ (addIBC . IBCImport) modules
1027 ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
1028 f file pos
1029 unless (null ds') $ do
1030 let ds = namespaces mname ds'
1031 logLvl 3 (showDecls True ds)
1032 i <- getIState
1033 logLvl 10 (show (toAlist (idris_implicits i)))
1034 logLvl 3 (show (idris_infixes i))
1035 -- Now add all the declarations to the context
1036 v <- verbose
1037 when v $ ihputStrLn h $ "Type checking " ++ f
1038 -- we totality check after every Mutual block, so if
1039 -- anything is a single definition, wrap it in a
1040 -- mutual block on its own
1041 elabDecls toplevel (map toMutual ds)
1042 i <- getIState
1043 -- simplify every definition do give the totality checker
1044 -- a better chance
1045 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1046 updateContext (simplifyCasedef n))
1047 (map snd (idris_totcheck i))
1048 -- build size change graph from simplified definitions
1049 iLOG "Totality checking"
1050 i <- getIState
1051 mapM_ buildSCG (idris_totcheck i)
1052 mapM_ checkDeclTotality (idris_totcheck i)
1054 -- Redo totality check for deferred names
1055 let deftots = idris_defertotcheck i
1056 iLOG $ "Totality checking " ++ show deftots
1057 mapM_ (\x -> do tot <- getTotality x
1058 case tot of
1059 Total _ -> setTotality x Unchecked
1060 _ -> return ()) (map snd deftots)
1061 mapM_ buildSCG deftots
1062 mapM_ checkDeclTotality deftots
1064 iLOG ("Finished " ++ f)
1065 ibcsd <- valIBCSubDir i
1066 iLOG "Universe checking"
1067 iucheck
1068 let ibc = ibcPathNoFallback ibcsd f
1069 i <- getIState
1070 addHides (hide_list i)
1071 ok <- noErrors
1072 when ok $
1073 idrisCatch (do writeIBC f ibc; clearIBC)
1074 (\c -> return ()) -- failure is harmless
1075 i <- getIState
1076 putIState (i { default_total = def_total,
1077 hide_list = [] })
1078 return ()
1079 return ()
1080 where
1081 namespaces :: [String] -> [PDecl] -> [PDecl]
1082 namespaces [] ds = ds
1083 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1085 toMutual :: PDecl -> PDecl
1086 toMutual m@(PMutual _ d) = m
1087 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1088 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1089 case x of
1090 PClauses _ _ _ _ -> r
1091 PClass _ _ _ _ _ _ _ -> r
1092 PInstance _ _ _ _ _ _ _ _ -> r
1093 _ -> x
1095{- | Adds names to hide list -}
1096addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1097addHides xs = do i <- getIState
1098 let defh = default_access i
1099 let (hs, as) = partition isNothing xs
1100 unless (null as) $
1101 mapM_ doHide
1102 (map (\ (n, _) -> (n, defh)) hs ++
1103 map (\ (n, Just a) -> (n, a)) as)
1104 where isNothing (_, Nothing) = True
1105 isNothing _ = False
1107 doHide (n, a) = do setAccessibility n a
1108 addIBC (IBCAccess n a)