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