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