git.iko.soy/Idris-dev
on 57aaa5e help sign in
Idris-dev/src/Idris/Parser.hs
1298 lines 45 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
41import qualified Util.Pretty as P
43import Idris.Core.TT
44import Idris.Core.Evaluate
46import Control.Applicative
47import Control.Monad
48import Control.Monad.Error (throwError, catchError)
49import Control.Monad.State.Strict
51import Data.Function
52import Data.Maybe
53import qualified Data.List.Split as Spl
54import Data.List
55import Data.Monoid
56import Data.Char
57import Data.Ord
58import qualified Data.Map as M
59import qualified Data.HashSet as HS
60import qualified Data.Text as T
61import qualified Data.ByteString.UTF8 as UTF8
62import qualified Data.Set as S
64import Debug.Trace
66import System.FilePath
67import System.IO
69{-
71 grammar shortcut notation:
72 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)
73 RULE? = optional rule (i.e. RULE or nothing)
74 RULE* = repeated rule (i.e. RULE zero or more times)
75 RULE+ = repeated rule with at least one match (i.e. RULE one or more times)
76 RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)
77 RULE{n} = rule repeated n times
79-}
81{- * Main grammar -}
83{- | Parses module definition
86 ModuleHeader ::= 'module' Identifier_t ';'?;
88-}
89moduleHeader :: IdrisParser [String]
90moduleHeader = try (do reserved "module"
91 i <- identifier
92 option ';' (lchar ';')
93 return (moduleName i))
94 <|> try (do lchar '%'; reserved "unqualified"
95 return [])
96 <|> return (moduleName "Main")
97 where moduleName x = case span (/='.') x of
98 (x, "") -> [x]
99 (x, '.':y) -> x : moduleName y
101{- | Parses an import statement
104 Import ::= 'import' Identifier_t ';'?;
106 -}
107import_ :: IdrisParser (String, Maybe String, FC)
108import_ = do fc <- getFC
109 reserved "import"
110 id <- identifier
111 newName <- optional (reserved "as" *> identifier)
112 option ';' (lchar ';')
113 return (toPath id, toPath <$> newName, fc)
114 <?> "import statement"
115 where toPath = foldl1' (</>) . Spl.splitOn "."
117{- | Parses program source
120 Prog ::= Decl* EOF;
122 -}
123prog :: SyntaxInfo -> IdrisParser [PDecl]
124prog syn = do whiteSpace
125 decls <- many (decl syn)
126 notOpenBraces
127 eof
128 let c = (concat decls)
129 return c
131{-| Parses a top-level declaration
134Decl ::=
135 Decl'
136 | Using
137 | Params
138 | Mutual
139 | Namespace
140 | Class
141 | Instance
142 | DSL
143 | Directive
144 | Provider
145 | Transform
146 | Import!
147 ;
149-}
150decl :: SyntaxInfo -> IdrisParser [PDecl]
151decl syn = do notEndBlock
152 declBody
153 where declBody :: IdrisParser [PDecl]
154 declBody = declBody'
155 <|> using_ syn
156 <|> params syn
157 <|> mutual syn
158 <|> namespace syn
159 <|> class_ syn
160 <|> instance_ syn
161 <|> do d <- dsl syn; return [d]
162 <|> directive syn
163 <|> provider syn
164 <|> transform syn
165 <|> do import_; fail "imports must be at top of file"
166 <?> "declaration"
167 declBody' :: IdrisParser [PDecl]
168 declBody' = do d <- decl' syn
169 i <- get
170 let d' = fmap (debindApp syn . (desugar syn i)) d
171 return [d']
173{- | Parses a top-level declaration with possible syntax sugar
176Decl' ::=
177 Fixity
178 | FunDecl'
179 | Data
180 | Record
181 | SyntaxDecl
182 ;
184-}
185decl' :: SyntaxInfo -> IdrisParser PDecl
186decl' syn = fixity
187 <|> syntaxDecl syn
188 <|> fnDecl' syn
189 <|> data_ syn
190 <|> record syn
191 <?> "declaration"
193{- | Parses a syntax extension declaration (and adds the rule to parser state)
196 SyntaxDecl ::= SyntaxRule;
198-}
199syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
200syntaxDecl syn = do s <- syntaxRule syn
201 i <- get
202 let rs = syntax_rules i
203 let ns = syntax_keywords i
204 let ibc = ibc_write i
205 let ks = map show (names s)
206 put (i { syntax_rules = s : rs,
207 syntax_keywords = ks ++ ns,
208 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc })
209 fc <- getFC
210 return (PSyntax fc s)
211 where names (Rule syms _ _) = mapMaybe ename syms
212 ename (Keyword n) = Just n
213 ename _ = Nothing
215{- | Parses a syntax extension declaration
218SyntaxRuleOpts ::= 'term' | 'pattern';
222SyntaxRule ::=
223 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
227SyntaxSym ::= '[' Name_t ']'
228 | '{' Name_t '}'
229 | Name_t
230 | StringLiteral_t
231 ;
233-}
234syntaxRule :: SyntaxInfo -> IdrisParser Syntax
235syntaxRule syn
236 = do sty <- try (do
237 pushIndent
238 sty <- option AnySyntax (do reserved "term"; return TermSyntax
239 <|> do reserved "pattern"; return PatternSyntax)
240 reserved "syntax"
241 return sty)
242 syms <- some syntaxSym
243 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
244 let ns = mapMaybe getName syms
245 when (length ns /= length (nub ns))
246 $ unexpected "repeated variable in syntax rule"
247 lchar '='
248 tm <- typeExpr (allowImp syn)
249 terminator
250 return (Rule (mkSimple syms) tm sty)
251 where
252 isExpr (Expr _) = True
253 isExpr _ = False
254 getName (Expr n) = Just n
255 getName _ = Nothing
256 -- Can't parse two full expressions (i.e. expressions with application) in a row
257 -- so change them both to a simple expression
258 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
259 mkSimple xs = mkSimple' xs
261 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
262 mkSimple es
263 mkSimple' (e : es) = e : mkSimple' es
264 mkSimple' [] = []
267{- | Parses a syntax symbol (either binding variable, keyword or expression)
270SyntaxSym ::= '[' Name_t ']'
271 | '{' Name_t '}'
272 | Name_t
273 | StringLiteral_t
274 ;
276 -}
277syntaxSym :: IdrisParser SSymbol
278syntaxSym = try (do lchar '['; n <- name; lchar ']'
279 return (Expr n))
280 <|> try (do lchar '{'; n <- name; lchar '}'
281 return (Binding n))
282 <|> do n <- iName []
283 return (Keyword n)
284 <|> do sym <- stringLiteral
285 return (Symbol sym)
286 <?> "syntax symbol"
288{- | Parses a function declaration with possible syntax sugar
291 FunDecl ::= FunDecl';
293-}
294fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
295fnDecl syn = try (do notEndBlock
296 d <- fnDecl' syn
297 i <- get
298 let d' = fmap (desugar syn i) d
299 return [d']) <?> "function declaration"
301{-| Parses a function declaration
304 FunDecl' ::=
305 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
306 | Postulate
307 | Pattern
308 | CAF
309 ;
311-}
312fnDecl' :: SyntaxInfo -> IdrisParser PDecl
313fnDecl' syn = checkFixity $
314 do (doc, fc, opts', n, acc) <- try (do
315 doc <- option "" (docComment '|')
316 pushIndent
317 ist <- get
318 let initOpts = if default_total ist
319 then [TotalFn]
320 else []
321 opts <- fnOpts initOpts
322 acc <- optional accessibility
323 opts' <- fnOpts opts
324 n_in <- fnName
325 let n = expandNS syn n_in
326 fc <- getFC
327 lchar ':'
328 return (doc, fc, opts', n, acc))
329 ty <- typeExpr (allowImp syn)
330 terminator
331 addAcc n acc
332 return (PTy doc syn fc opts' n ty)
333 <|> postulate syn
334 <|> caf syn
335 <|> pattern syn
336 <?> "function declaration"
337 where checkFixity :: IdrisParser PDecl -> IdrisParser PDecl
338 checkFixity p = do decl <- p
339 case getName decl of
340 Nothing -> return decl
341 Just n -> do fOk <- fixityOK n
342 unless fOk . fail $
343 "Missing fixity declaration for " ++ show n
344 return decl
345 getName (PTy _ _ _ _ n _) = Just n
346 getName _ = Nothing
347 fixityOK (NS n _) = fixityOK n
348 fixityOK (UN n) | all (flip elem opChars) (str n) =
349 do fixities <- fmap idris_infixes get
350 return . elem (str n) . map (\ (Fix _ op) -> op) $ fixities
351 | otherwise = return True
352 fixityOK _ = return True
354{-| Parses function options given initial options
357FnOpts ::= 'total'
358 | 'partial'
359 | 'implicit'
360 | '%' 'assert_total'
361 | '%' 'error_handler'
362 | '%' 'reflection'
363 | '%' 'specialise' '[' NameTimesList? ']'
364 ;
368NameTimes ::= FnName Natural?;
372NameTimesList ::=
373 NameTimes
374 | NameTimes ',' NameTimesList
375 ;
377-}
378-- FIXME: Check compatability for function options (i.e. partal/total)
379fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
380fnOpts opts
381 = do reserved "total"; fnOpts (TotalFn : opts)
382 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
383 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;
384 fnOpts (CExport c : opts)
385 <|> do try (lchar '%' *> reserved "assert_total");
386 fnOpts (AssertTotal : opts)
387 <|> do try (lchar '%' *> reserved "error_handler");
388 fnOpts (ErrorHandler : opts)
389 <|> do try (lchar '%' *> reserved "error_reverse");
390 fnOpts (ErrorReverse : opts)
391 <|> do try (lchar '%' *> reserved "reflection");
392 fnOpts (Reflection : opts)
393 <|> do lchar '%'; reserved "specialise";
394 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
395 fnOpts (Specialise ns : opts)
396 <|> do reserved "implicit"; fnOpts (Implicit : opts)
397 <|> return opts
398 <?> "function modifier"
399 where nameTimes :: IdrisParser (Name, Maybe Int)
400 nameTimes = do n <- fnName
401 t <- option Nothing (do reds <- natural
402 return (Just (fromInteger reds)))
403 return (n, t)
405{- | Parses a postulate
408Postulate ::=
409 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
410 ;
412-}
413postulate :: SyntaxInfo -> IdrisParser PDecl
414postulate syn = do doc <- try $ do doc <- option "" (docComment '|')
415 pushIndent
416 reserved "postulate"
417 return doc
418 ist <- get
419 let initOpts = if default_total ist
420 then [TotalFn]
421 else []
422 opts <- fnOpts initOpts
423 acc <- optional accessibility
424 opts' <- fnOpts opts
425 n_in <- fnName
426 let n = expandNS syn n_in
427 lchar ':'
428 ty <- typeExpr (allowImp syn)
429 fc <- getFC
430 terminator
431 addAcc n acc
432 return (PPostulate doc syn fc opts' n ty)
433 <?> "postulate"
435{- | Parses a using declaration
438Using ::=
439 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
440 ;
442 -}
443using_ :: SyntaxInfo -> IdrisParser [PDecl]
444using_ syn =
445 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
446 openBlock
447 let uvars = using syn
448 ds <- many (decl (syn { using = uvars ++ ns }))
449 closeBlock
450 return (concat ds)
451 <?> "using declaration"
453{- | Parses a parameters declaration
456Params ::=
457 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
458 ;
460 -}
461params :: SyntaxInfo -> IdrisParser [PDecl]
462params syn =
463 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
464 openBlock
465 let pvars = syn_params syn
466 ds <- many (decl syn { syn_params = pvars ++ ns })
467 closeBlock
468 fc <- getFC
469 return [PParams fc ns (concat ds)]
470 <?> "parameters declaration"
472{- | Parses a mutual declaration (for mutually recursive functions)
475Mutual ::=
476 'mutual' OpenBlock Decl* CloseBlock
477 ;
479-}
480mutual :: SyntaxInfo -> IdrisParser [PDecl]
481mutual syn =
482 do reserved "mutual"
483 openBlock
484 let pvars = syn_params syn
485 ds <- many (decl syn)
486 closeBlock
487 fc <- getFC
488 return [PMutual fc (concat ds)]
489 <?> "mutual block"
491{-| Parses a namespace declaration
494Namespace ::=
495 'namespace' identifier OpenBlock Decl+ CloseBlock
496 ;
498-}
499namespace :: SyntaxInfo -> IdrisParser [PDecl]
500namespace syn =
501 do reserved "namespace"; n <- identifier;
502 openBlock
503 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
504 closeBlock
505 return [PNamespace n (concat ds)]
506 <?> "namespace declaration"
508{- | Parses a methods block (for instances)
511 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
513-}
514instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
515instanceBlock syn = do reserved "where"
516 openBlock
517 ds <- many (fnDecl syn)
518 closeBlock
519 return (concat ds)
520 <?> "instance block"
522{- | Parses a methods and instances block (for type classes)
525MethodOrInstance ::=
526 FnDecl
527 | Instance
528 ;
532ClassBlock ::=
533 'where' OpenBlock MethodOrInstance* CloseBlock
534 ;
536-}
537classBlock :: SyntaxInfo -> IdrisParser [PDecl]
538classBlock syn = do reserved "where"
539 openBlock
540 ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)
541 closeBlock
542 return (concat ds)
543 <?> "class block"
545{-| Parses a type class declaration
548ClassArgument ::=
549 Name
550 | '(' Name ':' Expr ')'
551 ;
555Class ::=
556 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
557 ;
559-}
560class_ :: SyntaxInfo -> IdrisParser [PDecl]
561class_ syn = do (doc, acc) <- try (do
562 doc <- option "" (docComment '|')
563 acc <- optional accessibility
564 return (doc, acc))
565 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName
566 let n = expandNS syn n_in
567 cs <- many carg
568 ds <- option [] (classBlock syn)
569 accData acc n (concatMap declared ds)
570 return [PClass doc syn fc cons n cs ds]
571 <?> "type-class declaration"
572 where
573 carg :: IdrisParser (Name, PTerm)
574 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
575 return (i, ty)
576 <|> do i <- name;
577 return (i, PType)
579{- | Parses a type class instance declaration
582 Instance ::=
583 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
584 ;
588InstanceName ::= '[' Name ']';
590-}
591instance_ :: SyntaxInfo -> IdrisParser [PDecl]
592instance_ syn = do reserved "instance"; fc <- getFC
593 en <- optional instanceName
594 cs <- constraintList syn
595 cn <- fnName
596 args <- many (simpleExpr syn)
597 let sc = PApp fc (PRef fc cn) (map pexp args)
598 let t = bindList (PPi constraint) (map (\x -> (sMN 0 "constraint", x)) cs) sc
599 ds <- option [] (instanceBlock syn)
600 return [PInstance syn fc cs cn args t en ds]
601 <?> "instance declaration"
602 where instanceName :: IdrisParser Name
603 instanceName = do lchar '['; n_in <- fnName; lchar ']'
604 let n = expandNS syn n_in
605 return n
606 <?> "instance name"
609{- | Parses a using declaration list
612UsingDeclList ::=
613 UsingDeclList'
614 | NameList TypeSig
615 ;
619UsingDeclList' ::=
620 UsingDecl
621 | UsingDecl ',' UsingDeclList'
622 ;
626NameList ::=
627 Name
628 | Name ',' NameList
629 ;
631-}
632usingDeclList :: SyntaxInfo -> IdrisParser [Using]
633usingDeclList syn
634 = try (sepBy1 (usingDecl syn) (lchar ','))
635 <|> do ns <- sepBy1 name (lchar ',')
636 lchar ':'
637 t <- typeExpr (disallowImp syn)
638 return (map (\x -> UImplicit x t) ns)
639 <?> "using declaration list"
641{- |Parses a using declaration
644UsingDecl ::=
645 FnName TypeSig
646 | FnName FnName+
647 ;
649-}
650usingDecl :: SyntaxInfo -> IdrisParser Using
651usingDecl syn = try (do x <- fnName
652 lchar ':'
653 t <- typeExpr (disallowImp syn)
654 return (UImplicit x t))
655 <|> do c <- fnName
656 xs <- some fnName
657 return (UConstraint c xs)
658 <?> "using declaration"
660{- | Parse a clause with patterns
663Pattern ::= Clause;
665-}
666pattern :: SyntaxInfo -> IdrisParser PDecl
667pattern syn = do fc <- getFC
668 clause <- clause syn
669 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
670 <?> "pattern"
672{- | Parse a constant applicative form declaration
675CAF ::= 'let' FnName '=' Expr Terminator;
677-}
678caf :: SyntaxInfo -> IdrisParser PDecl
679caf syn = do reserved "let"
680 n_in <- fnName; let n = expandNS syn n_in
681 lchar '='
682 t <- expr syn
683 terminator
684 fc <- getFC
685 return (PCAF fc n t)
686 <?> "constant applicative form declaration"
688{- | Parse an argument expression
691ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
693-}
694argExpr :: SyntaxInfo -> IdrisParser PTerm
695argExpr syn = let syn' = syn { inPattern = True } in
696 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
697 <?> "argument expression"
699{- | Parse a right hand side of a function
702RHS ::= '=' Expr
703 | '?=' RHSName? Expr
704 | 'impossible'
705 ;
709RHSName ::= '{' FnName '}';
711-}
712rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
713rhs syn n = do lchar '='; expr syn
714 <|> do symbol "?=";
715 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
716 return n)
717 r <- expr syn
718 return (addLet name r)
719 <|> do reserved "impossible"; return PImpossible
720 <?> "function right hand side"
721 where mkN :: Name -> Name
722 mkN (UN x) = sUN (str x++"_lemma_1")
723 mkN (NS x n) = NS (mkN x) n
724 n' :: Name
725 n' = mkN n
726 addLet :: Name -> PTerm -> PTerm
727 addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)
728 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
729 where addLetC (l, r) = (l, addLet nm r)
730 addLet nm r = (PLet (sUN "value") Placeholder r (PMetavar nm))
732{- |Parses a function clause
735RHSOrWithBlock ::= RHS WhereOrTerminator
736 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
737 ;
741Clause ::= WExpr+ RHSOrWithBlock
742 | SimpleExpr '<==' FnName RHS WhereOrTerminator
743 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
744 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
745 ;
749ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
753WhereOrTerminator ::= WhereBlock | Terminator;
755-}
756clause :: SyntaxInfo -> IdrisParser PClause
757clause syn
758 = do wargs <- try (do pushIndent; some (wExpr syn))
759 fc <- getFC
760 ist <- get
761 n <- case lastParse ist of
762 Just t -> return t
763 Nothing -> fail "Invalid clause"
764 (do r <- rhs syn n
765 let ctxt = tt_ctxt ist
766 let wsyn = syn { syn_namespace = [] }
767 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
768 popIndent
769 return x,
770 do terminator
771 return ([], [])]
772 return $ PClauseR fc wargs r wheres) <|> (do
773 popIndent
774 reserved "with"
775 wval <- simpleExpr syn
776 openBlock
777 ds <- some $ fnDecl syn
778 let withs = concat ds
779 closeBlock
780 return $ PWithR fc wargs wval withs)
781 <|> do ty <- try (do pushIndent
782 ty <- simpleExpr syn
783 symbol "<=="
784 return ty)
785 fc <- getFC
786 n_in <- fnName; let n = expandNS syn n_in
787 r <- rhs syn n
788 ist <- get
789 let ctxt = tt_ctxt ist
790 let wsyn = syn { syn_namespace = [] }
791 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
792 popIndent
793 return x,
794 do terminator
795 return ([], [])]
796 let capp = PLet (sMN 0 "match")
797 ty
798 (PMatchApp fc n)
799 (PRef fc (sMN 0 "match"))
800 ist <- get
801 put (ist { lastParse = Just n })
802 return $ PClause fc n capp [] r wheres
803 <|> do (l, op) <- try (do
804 pushIndent
805 l <- argExpr syn
806 op <- operator
807 when (op == "=" || op == "?=" ) $
808 fail "infix clause definition with \"=\" and \"?=\" not supported "
809 return (l, op))
810 let n = expandNS syn (sUN op)
811 r <- argExpr syn
812 fc <- getFC
813 wargs <- many (wExpr syn)
814 (do rs <- rhs syn n
815 let wsyn = syn { syn_namespace = [] }
816 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
817 popIndent
818 return x,
819 do terminator
820 return ([], [])]
821 ist <- get
822 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
823 put (ist { lastParse = Just n })
824 return $ PClause fc n capp wargs rs wheres) <|> (do
825 popIndent
826 reserved "with"
827 lchar '(' <?> "parenthesized expression"
828 wval <- bracketed syn
829 openBlock
830 ds <- some $ fnDecl syn
831 closeBlock
832 ist <- get
833 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
834 let withs = map (fillLHSD n capp wargs) $ concat ds
835 put (ist { lastParse = Just n })
836 return $ PWith fc n capp wargs wval withs)
837 <|> do pushIndent
838 n_in <- fnName; let n = expandNS syn n_in
839 cargs <- many (constraintArg syn)
840 fc <- getFC
841 args <- many (try (implicitArg (syn { inPattern = True } ))
842 <|> (fmap pexp (argExpr syn)))
843 wargs <- many (wExpr syn)
844 let capp = PApp fc (PRef fc n)
845 (cargs ++ args)
846 (do r <- rhs syn n
847 ist <- get
848 let ctxt = tt_ctxt ist
849 let wsyn = syn { syn_namespace = [] }
850 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
851 popIndent
852 return x,
853 do terminator
854 return ([], [])]
855 ist <- get
856 put (ist { lastParse = Just n })
857 return $ PClause fc n capp wargs r wheres) <|> (do
858 reserved "with"
859 ist <- get
860 put (ist { lastParse = Just n })
861 lchar '(' <?> "parenthesized expression"
862 wval <- bracketed syn
863 openBlock
864 ds <- some $ fnDecl syn
865 let withs = map (fillLHSD n capp wargs) $ concat ds
866 closeBlock
867 popIndent
868 return $ PWith fc n capp wargs wval withs)
869 <?> "function clause"
870 where
871 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
872 fillLHS n capp owargs (PClauseR fc wargs v ws)
873 = PClause fc n capp (owargs ++ wargs) v ws
874 fillLHS n capp owargs (PWithR fc wargs v ws)
875 = PWith fc n capp (owargs ++ wargs) v
876 (map (fillLHSD n capp (owargs ++ wargs)) ws)
877 fillLHS _ _ _ c = c
879 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
880 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
881 fillLHSD n c a x = x
883{-| Parses with pattern
885@
886WExpr ::= '|' Expr';
888-}
889wExpr :: SyntaxInfo -> IdrisParser PTerm
890wExpr syn = do lchar '|'
891 expr' syn
892 <?> "with pattern"
894{- | Parses a where block
897WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
899-}
900whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
901whereBlock n syn
902 = do reserved "where"
903 ds <- indentedBlock1 (decl syn)
904 let dns = concatMap (concatMap declared) ds
905 return (concat ds, map (\x -> (x, decoration syn x)) dns)
906 <?> "where block"
908{- |Parses a code generation target language name
911Codegen ::= 'C'
912 | 'Java'
913 | 'JavaScript'
914 | 'Node'
915 | 'LLVM'
916 | 'Bytecode'
917 ;
919-}
920codegen_ :: IdrisParser Codegen
921codegen_ = do reserved "C"; return ViaC
922 <|> do reserved "Java"; return ViaJava
923 <|> do reserved "JavaScript"; return ViaJavaScript
924 <|> do reserved "Node"; return ViaNode
925 <|> do reserved "LLVM"; return ViaLLVM
926 <|> do reserved "Bytecode"; return Bytecode
927 <?> "code generation language"
929{- |Parses a compiler directive
931StringList ::=
932 String
933 | String ',' StringList
934 ;
938Directive ::= '%' Directive';
942Directive' ::= 'lib' CodeGen String_t
943 | 'link' CodeGen String_t
944 | 'flag' CodeGen String_t
945 | 'include' CodeGen String_t
946 | 'hide' Name
947 | 'freeze' Name
948 | 'access' Accessibility
949 | 'default' Totality
950 | 'logging' Natural
951 | 'dynamic' StringList
952 | 'name' Name NameList
953 | 'error_handlers' Name NameList
954 | 'language' 'TypeProviders'
955 | 'language' 'ErrorReflection'
956 ;
958-}
959directive :: SyntaxInfo -> IdrisParser [PDecl]
960directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
961 return [PDirective (do addLib cgn lib
962 addIBC (IBCLib cgn lib))]
963 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
964 return [PDirective (do dirs <- allImportDirs
965 o <- liftIO $ findInPath dirs obj
966 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
967 addObjectFile cgn o)]
968 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
969 flag <- stringLiteral
970 return [PDirective (do addIBC (IBCCGFlag cgn flag)
971 addFlag cgn flag)]
972 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
973 return [PDirective (do addHdr cgn hdr
974 addIBC (IBCHeader cgn hdr))]
975 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
976 return [PDirective (do setAccessibility n Hidden
977 addIBC (IBCAccess n Hidden))]
978 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
979 return [PDirective (do setAccessibility n Frozen
980 addIBC (IBCAccess n Frozen))]
981 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
982 return [PDirective (do i <- get
983 put(i { default_access = acc }))]
984 <|> do try (lchar '%' *> reserved "default"); tot <- totality
985 i <- get
986 put (i { default_total = tot } )
987 return [PDirective (do i <- get
988 put(i { default_total = tot }))]
989 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
990 return [PDirective (setLogLevel (fromInteger i))]
991 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
992 return [PDirective (do added <- addDyLib libs
993 case added of
994 Left lib -> addIBC (IBCDyLib (lib_name lib))
995 Right msg ->
996 fail $ msg)]
997 <|> do try (lchar '%' *> reserved "name")
998 ty <- iName []
999 ns <- sepBy1 name (lchar ',')
1000 return [PDirective (do ty' <- disambiguate ty
1001 mapM_ (addNameHint ty') ns
1002 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1003 <|> do try (lchar '%' *> reserved "error_handlers")
1004 fn <- iName []
1005 arg <- iName []
1006 ns <- sepBy1 name (lchar ',')
1007 return [PDirective (do fn' <- disambiguate fn
1008 ns' <- mapM disambiguate ns
1009 addFunctionErrorHandlers fn' arg ns'
1010 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]
1011 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1012 return [PDirective (addLangExt ext)]
1013 <?> "directive"
1014 where disambiguate :: Name -> Idris Name
1015 disambiguate n = do i <- getIState
1016 case lookupCtxtName n (idris_implicits i) of
1017 [(n', _)] -> return n'
1018 [] -> throwError (NoSuchVariable n)
1019 more -> throwError (CantResolveAlts (map (show . fst) more))
1021pLangExt :: IdrisParser LanguageExt
1022pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1023 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1025{- | Parses a totality
1028Totality ::= 'partial' | 'total'
1032totality :: IdrisParser Bool
1033totality
1034 = do reserved "total"; return True
1035 <|> do reserved "partial"; return False
1037{- | Parses a type provider
1040Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;
1042 -}
1043provider :: SyntaxInfo -> IdrisParser [PDecl]
1044provider syn = do try (lchar '%' *> reserved "provide");
1045 lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1046 fc <- getFC
1047 reserved "with"
1048 e <- expr syn
1049 return [PProvider syn fc n t e]
1050 <?> "type provider"
1052{- | Parses a transform
1055Transform ::= '%' 'transform' Expr '==>' Expr
1058transform :: SyntaxInfo -> IdrisParser [PDecl]
1059transform syn = do try (lchar '%' *> reserved "transform")
1060 -- leave it unchecked, until we work out what this should
1061 -- actually mean...
1062-- safety <- option True (do reserved "unsafe"
1063-- return False)
1064 l <- expr syn
1065 fc <- getFC
1066 symbol "==>"
1067 r <- expr syn
1068 return [PTransform fc False l r]
1069 <?> "transform"
1072{- * Loading and parsing -}
1073{- | Parses an expression from input -}
1074parseExpr :: IState -> String -> Result PTerm
1075parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1077{- | Parses a tactic from input -}
1078parseTactic :: IState -> String -> Result PTactic
1079parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1081-- | Parse module header and imports
1082parseImports :: FilePath -> String -> Idris ([String], [(String, Maybe String, FC)], Maybe Delta)
1083parseImports fname input
1084 = do i <- getIState
1085 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1086 Failure err -> fail (show err)
1087 Success (x, i) -> do -- Discard state updates (there should be
1088 -- none anyway)
1089 return x
1090 where imports :: IdrisParser (([String], [(String, Maybe String, FC)], Maybe Delta), IState)
1091 imports = do whiteSpace
1092 mname <- moduleHeader
1093 ps <- many import_
1094 mrk <- mark
1095 isEof <- lookAheadMatches eof
1096 let mrk' = if isEof
1097 then Nothing
1098 else Just mrk
1099 i <- get
1100 return ((mname, ps, mrk'), i)
1102-- | There should be a better way of doing this...
1103findFC :: Doc -> (FC, String)
1104findFC x = let s = show (plain x) in
1105 case span (/= ':') s of
1106 (failname, ':':rest) -> case span isDigit rest of
1107 (line, ':':rest') -> case span isDigit rest' of
1108 (col, ':':msg) -> (FC failname (read line) (read col), msg)
1110-- | A program is a list of declarations, possibly with associated
1111-- documentation strings.
1112parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1113 Idris [PDecl]
1114parseProg syn fname input mrk
1115 = do i <- getIState
1116 case runparser mainProg i fname input of
1117 Failure doc -> do -- FIXME: Get error location from trifecta
1118 -- this can't be the solution!
1119 let (fc, msg) = findFC doc
1120 i <- getIState
1121 case idris_outputmode i of
1122 RawOutput -> ihputStrLn (idris_outh i) (show doc)
1123 IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)
1124 putIState (i { errLine = Just (fc_line fc) }) -- Just errl })
1125 return []
1126 Success (x, i) -> do putIState i
1127 return $ collect x
1128 where mainProg :: IdrisParser ([PDecl], IState)
1129 mainProg = case mrk of
1130 Nothing -> do i <- get; return ([], i)
1131 Just mrk -> do
1132 release mrk
1133 ds <- prog syn
1134 i' <- get
1135 return (ds, i')
1137{- | Load idris module and show error if something wrong happens -}
1138loadModule :: Handle -> FilePath -> Idris String
1139loadModule outh f
1140 = idrisCatch (loadModule' outh f)
1141 (\e -> do setErrLine (getErrLine e)
1142 ist <- getIState
1143 msg <- showErr e
1144 ihputStrLn outh msg
1145 return "")
1147{- | Load idris module -}
1148loadModule' :: Handle -> FilePath -> Idris String
1149loadModule' outh f
1150 = do i <- getIState
1151 let file = takeWhile (/= ' ') f
1152 ibcsd <- valIBCSubDir i
1153 ids <- allImportDirs
1154 fp <- liftIO $ findImport ids ibcsd file
1155 if file `elem` imported i
1156 then iLOG $ "Already read " ++ file
1157 else do putIState (i { imported = file : imported i })
1158 case fp of
1159 IDR fn -> loadSource outh False fn
1160 LIDR fn -> loadSource outh True fn
1161 IBC fn src ->
1162 idrisCatch (loadIBC fn)
1163 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1164 case src of
1165 IDR sfn -> loadSource outh False sfn
1166 LIDR sfn -> loadSource outh True sfn)
1167 let (dir, fh) = splitFileName file
1168 return (dropExtension fh)
1171{- | Load idris code from file -}
1172loadFromIFile :: Handle -> IFileType -> Idris ()
1173loadFromIFile h i@(IBC fn src)
1174 = do iLOG $ "Skipping " ++ getSrcFile i
1175 idrisCatch (loadIBC fn)
1176 (\err -> ierror $ LoadingFailed fn err)
1177 where
1178 getSrcFile (IDR fn) = fn
1179 getSrcFile (LIDR fn) = fn
1180 getSrcFile (IBC f src) = getSrcFile src
1182loadFromIFile h (IDR fn) = loadSource' h False fn
1183loadFromIFile h (LIDR fn) = loadSource' h True fn
1185{-| Load idris source code and show error if something wrong happens -}
1186loadSource' :: Handle -> Bool -> FilePath -> Idris ()
1187loadSource' h lidr r
1188 = idrisCatch (loadSource h lidr r)
1189 (\e -> do setErrLine (getErrLine e)
1190 ist <- getIState
1191 ihRenderError h (pprintErr ist e))
1193{- | Load Idris source code-}
1194loadSource :: Handle -> Bool -> FilePath -> Idris ()
1195loadSource h lidr f
1196 = do iLOG ("Reading " ++ f)
1197 i <- getIState
1198 let def_total = default_total i
1199 file_in <- runIO $ readFile f
1200 file <- if lidr then tclift $ unlit f file_in else return file_in
1201 (mname, imports, pos) <- parseImports f file
1203 -- process and check module aliases
1204 let modAliases = M.fromList
1205 [(prep alias, prep realName) | (realName, Just alias, fc) <- imports]
1206 prep = map T.pack . reverse . Spl.splitOn "/"
1207 aliasNames = [(alias, fc) | (_, Just alias, fc) <- imports]
1208 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1209 case map head . filter ((/= 1) . length) $ histogram of
1210 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1211 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1213 i <- getIState
1214 putIState (i { default_access = Hidden, module_aliases = modAliases })
1215 clearIBC -- start a new .ibc file
1216 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]
1217 let syntax = defaultSyntax{ syn_namespace = reverse mname }
1218 ds' <- parseProg syntax f file pos
1219 unless (null ds') $ do
1220 let ds = namespaces mname ds'
1221 logLvl 3 (show $ showDecls True ds)
1222 i <- getIState
1223 logLvl 10 (show (toAlist (idris_implicits i)))
1224 logLvl 3 (show (idris_infixes i))
1225 -- Now add all the declarations to the context
1226 v <- verbose
1227 when v $ ihputStrLn h $ "Type checking " ++ f
1228 -- we totality check after every Mutual block, so if
1229 -- anything is a single definition, wrap it in a
1230 -- mutual block on its own
1231 elabDecls toplevel (map toMutual ds)
1232 i <- getIState
1233 -- simplify every definition do give the totality checker
1234 -- a better chance
1235 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1236 updateContext (simplifyCasedef n))
1237 (map snd (idris_totcheck i))
1238 -- build size change graph from simplified definitions
1239 iLOG "Totality checking"
1240 i <- getIState
1241 mapM_ buildSCG (idris_totcheck i)
1242 mapM_ checkDeclTotality (idris_totcheck i)
1244 -- Redo totality check for deferred names
1245 let deftots = idris_defertotcheck i
1246 iLOG $ "Totality checking " ++ show deftots
1247 mapM_ (\x -> do tot <- getTotality x
1248 case tot of
1249 Total _ -> setTotality x Unchecked
1250 _ -> return ()) (map snd deftots)
1251 mapM_ buildSCG deftots
1252 mapM_ checkDeclTotality deftots
1254 iLOG ("Finished " ++ f)
1255 ibcsd <- valIBCSubDir i
1256 iLOG "Universe checking"
1257 iucheck
1258 let ibc = ibcPathNoFallback ibcsd f
1259 i <- getIState
1260 addHides (hide_list i)
1261 ok <- noErrors
1262 when ok $
1263 idrisCatch (do writeIBC f ibc; clearIBC)
1264 (\c -> return ()) -- failure is harmless
1265 i <- getIState
1266 putIState (i { default_total = def_total,
1267 hide_list = [] })
1268 return ()
1269 return ()
1270 where
1271 namespaces :: [String] -> [PDecl] -> [PDecl]
1272 namespaces [] ds = ds
1273 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1275 toMutual :: PDecl -> PDecl
1276 toMutual m@(PMutual _ d) = m
1277 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1278 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1279 case x of
1280 PClauses _ _ _ _ -> r
1281 PClass _ _ _ _ _ _ _ -> r
1282 PInstance _ _ _ _ _ _ _ _ -> r
1283 _ -> x
1285{- | Adds names to hide list -}
1286addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1287addHides xs = do i <- getIState
1288 let defh = default_access i
1289 let (hs, as) = partition isNothing xs
1290 unless (null as) $
1291 mapM_ doHide
1292 (map (\ (n, _) -> (n, defh)) hs ++
1293 map (\ (n, Just a) -> (n, a)) as)
1294 where isNothing (_, Nothing) = True
1295 isNothing _ = False
1297 doHide (n, a) = do setAccessibility n a
1298 addIBC (IBCAccess n a)