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