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