git.iko.soy/Idris-dev
on cd8a233 help sign in
Idris-dev/src/Idris/Parser.hs
1329 lines 47 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)
20import qualified Text.PrettyPrint.ANSI.Leijen as ANSI
22import Idris.AbsSyntax hiding (namespace, params)
23import Idris.DSL
24import Idris.Imports
25import Idris.Delaborate
26import Idris.Error
27import Idris.ElabDecls
28import Idris.ElabTerm
29import Idris.Coverage
30import Idris.IBC
31import Idris.Unlit
32import Idris.Providers
33import Idris.Output
35import Idris.ParseHelpers
36import Idris.ParseOps
37import Idris.ParseExpr
38import Idris.ParseData
40import Idris.Docstrings
42import Paths_idris
44import Util.DynamicLinker
45import qualified Util.Pretty as P
47import Idris.Core.TT
48import Idris.Core.Evaluate
50import Control.Applicative
51import Control.Monad
52import Control.Monad.Error (throwError, catchError)
53import Control.Monad.State.Strict
55import Data.Function
56import Data.Maybe
57import qualified Data.List.Split as Spl
58import Data.List
59import Data.Monoid
60import Data.Char
61import Data.Ord
62import qualified Data.Map as M
63import qualified Data.HashSet as HS
64import qualified Data.Text as T
65import qualified Data.ByteString.UTF8 as UTF8
66import qualified Data.Set as S
68import Debug.Trace
70import System.FilePath
71import System.IO
73{-
75 grammar shortcut notation:
76 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)
77 RULE? = optional rule (i.e. RULE or nothing)
78 RULE* = repeated rule (i.e. RULE zero or more times)
79 RULE+ = repeated rule with at least one match (i.e. RULE one or more times)
80 RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)
81 RULE{n} = rule repeated n times
83-}
85{- * Main grammar -}
87{- | Parses module definition
90 ModuleHeader ::= 'module' Identifier_t ';'?;
92-}
93moduleHeader :: IdrisParser [String]
94moduleHeader = try (do noDocCommentHere "Modules cannot have documentation comments"
95 reserved "module"
96 i <- identifier
97 option ';' (lchar ';')
98 return (moduleName i))
99 <|> try (do lchar '%'; reserved "unqualified"
100 return [])
101 <|> return (moduleName "Main")
102 where moduleName x = case span (/='.') x of
103 (x, "") -> [x]
104 (x, '.':y) -> x : moduleName y
106{- | Parses an import statement
109 Import ::= 'import' Identifier_t ';'?;
111 -}
112import_ :: IdrisParser (String, Maybe String, FC)
113import_ = do fc <- getFC
114 reserved "import"
115 id <- identifier
116 newName <- optional (reserved "as" *> identifier)
117 option ';' (lchar ';')
118 return (toPath id, toPath <$> newName, fc)
119 <?> "import statement"
120 where toPath = foldl1' (</>) . Spl.splitOn "."
122{- | Parses program source
125 Prog ::= Decl* EOF;
127 -}
128prog :: SyntaxInfo -> IdrisParser [PDecl]
129prog syn = do whiteSpace
130 decls <- many (decl syn)
131 notOpenBraces
132 eof
133 let c = (concat decls)
134 return c
136{-| Parses a top-level declaration
139Decl ::=
140 Decl'
141 | Using
142 | Params
143 | Mutual
144 | Namespace
145 | Class
146 | Instance
147 | DSL
148 | Directive
149 | Provider
150 | Transform
151 | Import!
152 ;
154-}
155decl :: SyntaxInfo -> IdrisParser [PDecl]
156decl syn = do notEndBlock
157 declBody
158 where declBody :: IdrisParser [PDecl]
159 declBody = declBody'
160 <|> using_ syn
161 <|> params syn
162 <|> mutual syn
163 <|> namespace syn
164 <|> class_ syn
165 <|> instance_ syn
166 <|> do d <- dsl syn; return [d]
167 <|> directive syn
168 <|> provider syn
169 <|> transform syn
170 <|> do import_; fail "imports must be at top of file"
171 <?> "declaration"
172 declBody' :: IdrisParser [PDecl]
173 declBody' = do d <- decl' syn
174 i <- get
175 let d' = fmap (debindApp syn . (desugar syn i)) d
176 return [d']
178{- | Parses a top-level declaration with possible syntax sugar
181Decl' ::=
182 Fixity
183 | FunDecl'
184 | Data
185 | Record
186 | SyntaxDecl
187 ;
189-}
190decl' :: SyntaxInfo -> IdrisParser PDecl
191decl' syn = fixity
192 <|> syntaxDecl syn
193 <|> fnDecl' syn
194 <|> data_ syn
195 <|> record syn
196 <?> "declaration"
198{- | Parses a syntax extension declaration (and adds the rule to parser state)
201 SyntaxDecl ::= SyntaxRule;
203-}
204syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
205syntaxDecl syn = do s <- syntaxRule syn
206 i <- get
207 let rs = syntax_rules i
208 let ns = syntax_keywords i
209 let ibc = ibc_write i
210 let ks = map show (names s)
211 put (i { syntax_rules = s : rs,
212 syntax_keywords = ks ++ ns,
213 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc })
214 fc <- getFC
215 return (PSyntax fc s)
216 where names (Rule syms _ _) = mapMaybe ename syms
217 ename (Keyword n) = Just n
218 ename _ = Nothing
220{- | Parses a syntax extension declaration
223SyntaxRuleOpts ::= 'term' | 'pattern';
227SyntaxRule ::=
228 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
232SyntaxSym ::= '[' Name_t ']'
233 | '{' Name_t '}'
234 | Name_t
235 | StringLiteral_t
236 ;
238-}
239syntaxRule :: SyntaxInfo -> IdrisParser Syntax
240syntaxRule syn
241 = do sty <- try (do
242 pushIndent
243 sty <- option AnySyntax (do reserved "term"; return TermSyntax
244 <|> do reserved "pattern"; return PatternSyntax)
245 reserved "syntax"
246 return sty)
247 syms <- some syntaxSym
248 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
249 let ns = mapMaybe getName syms
250 when (length ns /= length (nub ns))
251 $ unexpected "repeated variable in syntax rule"
252 lchar '='
253 tm <- typeExpr (allowImp syn)
254 terminator
255 return (Rule (mkSimple syms) tm sty)
256 where
257 isExpr (Expr _) = True
258 isExpr _ = False
259 getName (Expr n) = Just n
260 getName _ = Nothing
261 -- Can't parse two full expressions (i.e. expressions with application) in a row
262 -- so change them both to a simple expression
263 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
264 mkSimple xs = mkSimple' xs
266 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
267 mkSimple es
268 mkSimple' (e : es) = e : mkSimple' es
269 mkSimple' [] = []
272{- | Parses a syntax symbol (either binding variable, keyword or expression)
275SyntaxSym ::= '[' Name_t ']'
276 | '{' Name_t '}'
277 | Name_t
278 | StringLiteral_t
279 ;
281 -}
282syntaxSym :: IdrisParser SSymbol
283syntaxSym = try (do lchar '['; n <- name; lchar ']'
284 return (Expr n))
285 <|> try (do lchar '{'; n <- name; lchar '}'
286 return (Binding n))
287 <|> do n <- iName []
288 return (Keyword n)
289 <|> do sym <- stringLiteral
290 return (Symbol sym)
291 <?> "syntax symbol"
293{- | Parses a function declaration with possible syntax sugar
296 FunDecl ::= FunDecl';
298-}
299fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
300fnDecl syn = try (do notEndBlock
301 d <- fnDecl' syn
302 i <- get
303 let d' = fmap (desugar syn i) d
304 return [d']) <?> "function declaration"
306{-| Parses a function declaration
309 FunDecl' ::=
310 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
311 | Postulate
312 | Pattern
313 | CAF
314 ;
316-}
317fnDecl' :: SyntaxInfo -> IdrisParser PDecl
318fnDecl' syn = checkFixity $
319 do (doc, fc, opts', n, acc) <- try (do
320 pushIndent
321 ist <- get
322 doc <- option noDocs docComment
323 ist <- get
324 let initOpts = if default_total ist
325 then [TotalFn]
326 else []
327 opts <- fnOpts initOpts
328 acc <- optional accessibility
329 opts' <- fnOpts opts
330 n_in <- fnName
331 let n = expandNS syn n_in
332 fc <- getFC
333 lchar ':'
334 return (doc, fc, opts', n, acc))
335 ty <- typeExpr (allowImp syn)
336 terminator
337 addAcc n acc
338 return (PTy (fst doc) (snd doc) syn fc opts' n ty)
339 <|> postulate syn
340 <|> caf syn
341 <|> pattern syn
342 <?> "function declaration"
343 where checkFixity :: IdrisParser PDecl -> IdrisParser PDecl
344 checkFixity p = do decl <- p
345 case getName decl of
346 Nothing -> return decl
347 Just n -> do fOk <- fixityOK n
348 unless fOk . fail $
349 "Missing fixity declaration for " ++ show n
350 return decl
351 getName (PTy _ _ _ _ _ n _) = Just n
352 getName _ = Nothing
353 fixityOK (NS n _) = fixityOK n
354 fixityOK (UN n) | all (flip elem opChars) (str n) =
355 do fixities <- fmap idris_infixes get
356 return . elem (str n) . map (\ (Fix _ op) -> op) $ fixities
357 | otherwise = return True
358 fixityOK _ = return True
360{-| Parses function options given initial options
363FnOpts ::= 'total'
364 | 'partial'
365 | 'implicit'
366 | '%' 'assert_total'
367 | '%' 'error_handler'
368 | '%' 'reflection'
369 | '%' 'specialise' '[' NameTimesList? ']'
370 ;
374NameTimes ::= FnName Natural?;
378NameTimesList ::=
379 NameTimes
380 | NameTimes ',' NameTimesList
381 ;
383-}
384-- FIXME: Check compatability for function options (i.e. partal/total)
385fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
386fnOpts opts
387 = do reserved "total"; fnOpts (TotalFn : opts)
388 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
389 <|> do reserved "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))
390 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;
391 fnOpts (CExport c : opts)
392 <|> do try (lchar '%' *> reserved "assert_total");
393 fnOpts (AssertTotal : opts)
394 <|> do try (lchar '%' *> reserved "error_handler");
395 fnOpts (ErrorHandler : opts)
396 <|> do try (lchar '%' *> reserved "error_reverse");
397 fnOpts (ErrorReverse : opts)
398 <|> do try (lchar '%' *> reserved "reflection");
399 fnOpts (Reflection : opts)
400 <|> do lchar '%'; reserved "specialise";
401 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
402 fnOpts (Specialise ns : opts)
403 <|> do reserved "implicit"; fnOpts (Implicit : opts)
404 <|> return opts
405 <?> "function modifier"
406 where nameTimes :: IdrisParser (Name, Maybe Int)
407 nameTimes = do n <- fnName
408 t <- option Nothing (do reds <- natural
409 return (Just (fromInteger reds)))
410 return (n, t)
412{- | Parses a postulate
415Postulate ::=
416 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
417 ;
419-}
420postulate :: SyntaxInfo -> IdrisParser PDecl
421postulate syn = do doc <- try $ do doc <- option noDocs docComment
422 pushIndent
423 reserved "postulate"
424 return doc
425 ist <- get
426 let initOpts = if default_total ist
427 then [TotalFn]
428 else []
429 opts <- fnOpts initOpts
430 acc <- optional accessibility
431 opts' <- fnOpts opts
432 n_in <- fnName
433 let n = expandNS syn n_in
434 lchar ':'
435 ty <- typeExpr (allowImp syn)
436 fc <- getFC
437 terminator
438 addAcc n acc
439 return (PPostulate (fst doc) syn fc opts' n ty)
440 <?> "postulate"
442{- | Parses a using declaration
445Using ::=
446 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
447 ;
449 -}
450using_ :: SyntaxInfo -> IdrisParser [PDecl]
451using_ syn =
452 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
453 openBlock
454 let uvars = using syn
455 ds <- many (decl (syn { using = uvars ++ ns }))
456 closeBlock
457 return (concat ds)
458 <?> "using declaration"
460{- | Parses a parameters declaration
463Params ::=
464 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
465 ;
467 -}
468params :: SyntaxInfo -> IdrisParser [PDecl]
469params syn =
470 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
471 openBlock
472 let pvars = syn_params syn
473 ds <- many (decl syn { syn_params = pvars ++ ns })
474 closeBlock
475 fc <- getFC
476 return [PParams fc ns (concat ds)]
477 <?> "parameters declaration"
479{- | Parses a mutual declaration (for mutually recursive functions)
482Mutual ::=
483 'mutual' OpenBlock Decl* CloseBlock
484 ;
486-}
487mutual :: SyntaxInfo -> IdrisParser [PDecl]
488mutual syn =
489 do reserved "mutual"
490 openBlock
491 let pvars = syn_params syn
492 ds <- many (decl syn)
493 closeBlock
494 fc <- getFC
495 return [PMutual fc (concat ds)]
496 <?> "mutual block"
498{-| Parses a namespace declaration
501Namespace ::=
502 'namespace' identifier OpenBlock Decl+ CloseBlock
503 ;
505-}
506namespace :: SyntaxInfo -> IdrisParser [PDecl]
507namespace syn =
508 do reserved "namespace"; n <- identifier;
509 openBlock
510 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
511 closeBlock
512 return [PNamespace n (concat ds)]
513 <?> "namespace declaration"
515{- | Parses a methods block (for instances)
518 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
520-}
521instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
522instanceBlock syn = do reserved "where"
523 openBlock
524 ds <- many (fnDecl syn)
525 closeBlock
526 return (concat ds)
527 <?> "instance block"
529{- | Parses a methods and instances block (for type classes)
532MethodOrInstance ::=
533 FnDecl
534 | Instance
535 ;
539ClassBlock ::=
540 'where' OpenBlock MethodOrInstance* CloseBlock
541 ;
543-}
544classBlock :: SyntaxInfo -> IdrisParser [PDecl]
545classBlock syn = do reserved "where"
546 openBlock
547 ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)
548 closeBlock
549 return (concat ds)
550 <?> "class block"
552{-| Parses a type class declaration
555ClassArgument ::=
556 Name
557 | '(' Name ':' Expr ')'
558 ;
562Class ::=
563 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
564 ;
566-}
567class_ :: SyntaxInfo -> IdrisParser [PDecl]
568class_ syn = do (doc, acc) <- try (do
569 doc <- option noDocs docComment
570 acc <- optional accessibility
571 return (doc, acc))
572 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName
573 let n = expandNS syn n_in
574 cs <- many carg
575 ds <- option [] (classBlock syn)
576 accData acc n (concatMap declared ds)
577 return [PClass (fst doc) syn fc cons n cs (snd doc) ds]
578 <?> "type-class declaration"
579 where
580 carg :: IdrisParser (Name, PTerm)
581 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
582 return (i, ty)
583 <|> do i <- name;
584 return (i, PType)
586{- | Parses a type class instance declaration
589 Instance ::=
590 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
591 ;
595InstanceName ::= '[' Name ']';
597-}
598instance_ :: SyntaxInfo -> IdrisParser [PDecl]
599instance_ syn = do reserved "instance"; fc <- getFC
600 en <- optional instanceName
601 cs <- constraintList syn
602 cn <- fnName
603 args <- many (simpleExpr syn)
604 let sc = PApp fc (PRef fc cn) (map pexp args)
605 let t = bindList (PPi constraint) (map (\x -> (sMN 0 "constraint", x)) cs) sc
606 ds <- option [] (instanceBlock syn)
607 return [PInstance syn fc cs cn args t en ds]
608 <?> "instance declaration"
609 where instanceName :: IdrisParser Name
610 instanceName = do lchar '['; n_in <- fnName; lchar ']'
611 let n = expandNS syn n_in
612 return n
613 <?> "instance name"
616{- | Parses a using declaration list
619UsingDeclList ::=
620 UsingDeclList'
621 | NameList TypeSig
622 ;
626UsingDeclList' ::=
627 UsingDecl
628 | UsingDecl ',' UsingDeclList'
629 ;
633NameList ::=
634 Name
635 | Name ',' NameList
636 ;
638-}
639usingDeclList :: SyntaxInfo -> IdrisParser [Using]
640usingDeclList syn
641 = try (sepBy1 (usingDecl syn) (lchar ','))
642 <|> do ns <- sepBy1 name (lchar ',')
643 lchar ':'
644 t <- typeExpr (disallowImp syn)
645 return (map (\x -> UImplicit x t) ns)
646 <?> "using declaration list"
648{- |Parses a using declaration
651UsingDecl ::=
652 FnName TypeSig
653 | FnName FnName+
654 ;
656-}
657usingDecl :: SyntaxInfo -> IdrisParser Using
658usingDecl syn = try (do x <- fnName
659 lchar ':'
660 t <- typeExpr (disallowImp syn)
661 return (UImplicit x t))
662 <|> do c <- fnName
663 xs <- some fnName
664 return (UConstraint c xs)
665 <?> "using declaration"
667{- | Parse a clause with patterns
670Pattern ::= Clause;
672-}
673pattern :: SyntaxInfo -> IdrisParser PDecl
674pattern syn = do fc <- getFC
675 clause <- clause syn
676 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
677 <?> "pattern"
679{- | Parse a constant applicative form declaration
682CAF ::= 'let' FnName '=' Expr Terminator;
684-}
685caf :: SyntaxInfo -> IdrisParser PDecl
686caf syn = do reserved "let"
687 n_in <- fnName; let n = expandNS syn n_in
688 lchar '='
689 t <- expr syn
690 terminator
691 fc <- getFC
692 return (PCAF fc n t)
693 <?> "constant applicative form declaration"
695{- | Parse an argument expression
698ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
700-}
701argExpr :: SyntaxInfo -> IdrisParser PTerm
702argExpr syn = let syn' = syn { inPattern = True } in
703 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
704 <?> "argument expression"
706{- | Parse a right hand side of a function
709RHS ::= '=' Expr
710 | '?=' RHSName? Expr
711 | 'impossible'
712 ;
716RHSName ::= '{' FnName '}';
718-}
719rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
720rhs syn n = do lchar '='; expr syn
721 <|> do symbol "?=";
722 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
723 return n)
724 r <- expr syn
725 return (addLet name r)
726 <|> do reserved "impossible"; return PImpossible
727 <?> "function right hand side"
728 where mkN :: Name -> Name
729 mkN (UN x) = sUN (str x++"_lemma_1")
730 mkN (NS x n) = NS (mkN x) n
731 n' :: Name
732 n' = mkN n
733 addLet :: Name -> PTerm -> PTerm
734 addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)
735 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
736 where addLetC (l, r) = (l, addLet nm r)
737 addLet nm r = (PLet (sUN "value") Placeholder r (PMetavar nm))
739{- |Parses a function clause
742RHSOrWithBlock ::= RHS WhereOrTerminator
743 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
744 ;
748Clause ::= WExpr+ RHSOrWithBlock
749 | SimpleExpr '<==' FnName RHS WhereOrTerminator
750 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
751 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
752 ;
756ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
760WhereOrTerminator ::= WhereBlock | Terminator;
762-}
763clause :: SyntaxInfo -> IdrisParser PClause
764clause syn
765 = do wargs <- try (do pushIndent; some (wExpr syn))
766 fc <- getFC
767 ist <- get
768 n <- case lastParse ist of
769 Just t -> return t
770 Nothing -> fail "Invalid clause"
771 (do r <- rhs syn n
772 let ctxt = tt_ctxt ist
773 let wsyn = syn { syn_namespace = [] }
774 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
775 popIndent
776 return x,
777 do terminator
778 return ([], [])]
779 return $ PClauseR fc wargs r wheres) <|> (do
780 popIndent
781 reserved "with"
782 wval <- simpleExpr syn
783 openBlock
784 ds <- some $ fnDecl syn
785 let withs = concat ds
786 closeBlock
787 return $ PWithR fc wargs wval withs)
788 <|> do ty <- try (do pushIndent
789 ty <- simpleExpr syn
790 symbol "<=="
791 return ty)
792 fc <- getFC
793 n_in <- fnName; let n = expandNS syn n_in
794 r <- rhs syn n
795 ist <- get
796 let ctxt = tt_ctxt ist
797 let wsyn = syn { syn_namespace = [] }
798 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
799 popIndent
800 return x,
801 do terminator
802 return ([], [])]
803 let capp = PLet (sMN 0 "match")
804 ty
805 (PMatchApp fc n)
806 (PRef fc (sMN 0 "match"))
807 ist <- get
808 put (ist { lastParse = Just n })
809 return $ PClause fc n capp [] r wheres
810 <|> do (l, op) <- try (do
811 pushIndent
812 l <- argExpr syn
813 op <- operator
814 when (op == "=" || op == "?=" ) $
815 fail "infix clause definition with \"=\" and \"?=\" not supported "
816 return (l, op))
817 let n = expandNS syn (sUN op)
818 r <- argExpr syn
819 fc <- getFC
820 wargs <- many (wExpr syn)
821 (do rs <- rhs syn n
822 let wsyn = syn { syn_namespace = [] }
823 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
824 popIndent
825 return x,
826 do terminator
827 return ([], [])]
828 ist <- get
829 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
830 put (ist { lastParse = Just n })
831 return $ PClause fc n capp wargs rs wheres) <|> (do
832 popIndent
833 reserved "with"
834 wval <- bracketed syn
835 openBlock
836 ds <- some $ fnDecl syn
837 closeBlock
838 ist <- get
839 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
840 let withs = map (fillLHSD n capp wargs) $ concat ds
841 put (ist { lastParse = Just n })
842 return $ PWith fc n capp wargs wval withs)
843 <|> do pushIndent
844 n_in <- fnName; let n = expandNS syn n_in
845 cargs <- many (constraintArg syn)
846 fc <- getFC
847 args <- many (try (implicitArg (syn { inPattern = True } ))
848 <|> (fmap pexp (argExpr syn)))
849 wargs <- many (wExpr syn)
850 let capp = PApp fc (PRef fc n)
851 (cargs ++ args)
852 (do r <- rhs syn n
853 ist <- get
854 let ctxt = tt_ctxt ist
855 let wsyn = syn { syn_namespace = [] }
856 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
857 popIndent
858 return x,
859 do terminator
860 return ([], [])]
861 ist <- get
862 put (ist { lastParse = Just n })
863 return $ PClause fc n capp wargs r wheres) <|> (do
864 reserved "with"
865 ist <- get
866 put (ist { lastParse = Just n })
867 wval <- bracketed syn
868 openBlock
869 ds <- some $ fnDecl syn
870 let withs = map (fillLHSD n capp wargs) $ concat ds
871 closeBlock
872 popIndent
873 return $ PWith fc n capp wargs wval withs)
874 <?> "function clause"
875 where
876 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
877 fillLHS n capp owargs (PClauseR fc wargs v ws)
878 = PClause fc n capp (owargs ++ wargs) v ws
879 fillLHS n capp owargs (PWithR fc wargs v ws)
880 = PWith fc n capp (owargs ++ wargs) v
881 (map (fillLHSD n capp (owargs ++ wargs)) ws)
882 fillLHS _ _ _ c = c
884 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
885 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
886 fillLHSD n c a x = x
888{-| Parses with pattern
890@
891WExpr ::= '|' Expr';
893-}
894wExpr :: SyntaxInfo -> IdrisParser PTerm
895wExpr syn = do lchar '|'
896 expr' syn
897 <?> "with pattern"
899{- | Parses a where block
902WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
904-}
905whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
906whereBlock n syn
907 = do reserved "where"
908 ds <- indentedBlock1 (decl syn)
909 let dns = concatMap (concatMap declared) ds
910 return (concat ds, map (\x -> (x, decoration syn x)) dns)
911 <?> "where block"
913{- |Parses a code generation target language name
916Codegen ::= 'C'
917 | 'Java'
918 | 'JavaScript'
919 | 'Node'
920 | 'LLVM'
921 | 'Bytecode'
922 ;
924-}
925codegen_ :: IdrisParser Codegen
926codegen_ = do reserved "C"; return ViaC
927 <|> do reserved "Java"; return ViaJava
928 <|> do reserved "JavaScript"; return ViaJavaScript
929 <|> do reserved "Node"; return ViaNode
930 <|> do reserved "LLVM"; return ViaLLVM
931 <|> do reserved "Bytecode"; return Bytecode
932 <?> "code generation language"
934{- |Parses a compiler directive
936StringList ::=
937 String
938 | String ',' StringList
939 ;
943Directive ::= '%' Directive';
947Directive' ::= 'lib' CodeGen String_t
948 | 'link' CodeGen String_t
949 | 'flag' CodeGen String_t
950 | 'include' CodeGen String_t
951 | 'hide' Name
952 | 'freeze' Name
953 | 'access' Accessibility
954 | 'default' Totality
955 | 'logging' Natural
956 | 'dynamic' StringList
957 | 'name' Name NameList
958 | 'error_handlers' Name NameList
959 | 'language' 'TypeProviders'
960 | 'language' 'ErrorReflection'
961 ;
963-}
964directive :: SyntaxInfo -> IdrisParser [PDecl]
965directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
966 return [PDirective (do addLib cgn lib
967 addIBC (IBCLib cgn lib))]
968 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
969 return [PDirective (do dirs <- allImportDirs
970 o <- liftIO $ findInPath dirs obj
971 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
972 addObjectFile cgn o)]
973 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
974 flag <- stringLiteral
975 return [PDirective (do addIBC (IBCCGFlag cgn flag)
976 addFlag cgn flag)]
977 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
978 return [PDirective (do addHdr cgn hdr
979 addIBC (IBCHeader cgn hdr))]
980 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
981 return [PDirective (do setAccessibility n Hidden
982 addIBC (IBCAccess n Hidden))]
983 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
984 return [PDirective (do setAccessibility n Frozen
985 addIBC (IBCAccess n Frozen))]
986 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
987 return [PDirective (do i <- get
988 put(i { default_access = acc }))]
989 <|> do try (lchar '%' *> reserved "default"); tot <- totality
990 i <- get
991 put (i { default_total = tot } )
992 return [PDirective (do i <- get
993 put(i { default_total = tot }))]
994 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
995 return [PDirective (setLogLevel (fromInteger i))]
996 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
997 return [PDirective (do added <- addDyLib libs
998 case added of
999 Left lib -> addIBC (IBCDyLib (lib_name lib))
1000 Right msg ->
1001 fail $ msg)]
1002 <|> do try (lchar '%' *> reserved "name")
1003 ty <- iName []
1004 ns <- sepBy1 name (lchar ',')
1005 return [PDirective (do ty' <- disambiguate ty
1006 mapM_ (addNameHint ty') ns
1007 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1008 <|> do try (lchar '%' *> reserved "error_handlers")
1009 fn <- fnName
1010 arg <- fnName
1011 ns <- sepBy1 name (lchar ',')
1012 return [PDirective (do fn' <- disambiguate fn
1013 ns' <- mapM disambiguate ns
1014 addFunctionErrorHandlers fn' arg ns'
1015 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]
1016 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1017 return [PDirective (addLangExt ext)]
1018 <?> "directive"
1019 where disambiguate :: Name -> Idris Name
1020 disambiguate n = do i <- getIState
1021 case lookupCtxtName n (idris_implicits i) of
1022 [(n', _)] -> return n'
1023 [] -> throwError (NoSuchVariable n)
1024 more -> throwError (CantResolveAlts (map (show . fst) more))
1026pLangExt :: IdrisParser LanguageExt
1027pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1028 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1030{- | Parses a totality
1033Totality ::= 'partial' | 'total'
1037totality :: IdrisParser Bool
1038totality
1039 = do reserved "total"; return True
1040 <|> do reserved "partial"; return False
1042{- | Parses a type provider
1045Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1046ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1048 -}
1049provider :: SyntaxInfo -> IdrisParser [PDecl]
1050provider syn = do try (lchar '%' *> reserved "provide");
1051 what <- provideWhat
1052 lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1053 fc <- getFC
1054 reserved "with"
1055 e <- expr syn
1056 return [PProvider syn fc what n t e]
1057 <?> "type provider"
1058 where provideWhat :: IdrisParser ProvideWhat
1059 provideWhat = option ProvAny
1060 ( ((reserved "proof" <|> reserved "term" <|> reserved "type") *>
1061 pure ProvTerm)
1062 <|> (reserved "postulate" *> pure ProvPostulate)
1063 <?> "provider variety")
1064{- | Parses a transform
1067Transform ::= '%' 'transform' Expr '==>' Expr
1070transform :: SyntaxInfo -> IdrisParser [PDecl]
1071transform syn = do try (lchar '%' *> reserved "transform")
1072 -- leave it unchecked, until we work out what this should
1073 -- actually mean...
1074-- safety <- option True (do reserved "unsafe"
1075-- return False)
1076 l <- expr syn
1077 fc <- getFC
1078 symbol "==>"
1079 r <- expr syn
1080 return [PTransform fc False l r]
1081 <?> "transform"
1084{- * Loading and parsing -}
1085{- | Parses an expression from input -}
1086parseExpr :: IState -> String -> Result PTerm
1087parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1089{- | Parses a tactic from input -}
1090parseTactic :: IState -> String -> Result PTactic
1091parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1093-- | Parse module header and imports
1094parseImports :: FilePath -> String -> Idris ([String], [(String, Maybe String, FC)], Maybe Delta)
1095parseImports fname input
1096 = do i <- getIState
1097 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1098 Failure err -> fail (show err)
1099 Success (x, i) -> do putIState i
1100 return x
1101 where imports :: IdrisParser (([String], [(String, Maybe String, FC)], Maybe Delta), IState)
1102 imports = do whiteSpace
1103 mname <- moduleHeader
1104 ps <- many import_
1105 mrk <- mark
1106 isEof <- lookAheadMatches eof
1107 let mrk' = if isEof
1108 then Nothing
1109 else Just mrk
1110 i <- get
1111 return ((mname, ps, mrk'), i)
1113-- | There should be a better way of doing this...
1114findFC :: Doc -> (FC, String)
1115findFC x = let s = show (plain x) in
1116 case span (/= ':') s of
1117 (failname, ':':rest) -> case span isDigit rest of
1118 (line, ':':rest') -> case span isDigit rest' of
1119 (col, ':':msg) -> let pos = (read line, read col) in
1120 (FC failname pos pos, msg)
1122-- | Check if the coloring matches the options and corrects if necessary
1123fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1124fixColour False doc = ANSI.plain doc
1125fixColour True doc = doc
1127-- | A program is a list of declarations, possibly with associated
1128-- documentation strings.
1129parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1130 Idris [PDecl]
1131parseProg syn fname input mrk
1132 = do i <- getIState
1133 case runparser mainProg i fname input of
1134 Failure doc -> do -- FIXME: Get error location from trifecta
1135 -- this can't be the solution!
1136 let (fc, msg) = findFC doc
1137 i <- getIState
1138 case idris_outputmode i of
1139 RawOutput -> ihputStrLn (idris_outh i) (show $ fixColour (idris_colourRepl i) doc)
1140 IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)
1141 putIState (i { errSpan = Just fc })
1142 return []
1143 Success (x, i) -> do putIState i
1144 reportParserWarnings
1145 return $ collect x
1146 where mainProg :: IdrisParser ([PDecl], IState)
1147 mainProg = case mrk of
1148 Nothing -> do i <- get; return ([], i)
1149 Just mrk -> do
1150 release mrk
1151 ds <- prog syn
1152 i' <- get
1153 return (ds, i')
1155{- | Load idris module and show error if something wrong happens -}
1156loadModule :: Handle -> FilePath -> Idris String
1157loadModule outh f
1158 = idrisCatch (loadModule' outh f)
1159 (\e -> do setErrSpan (getErrSpan e)
1160 ist <- getIState
1161 ihWarn outh (getErrSpan e) $ pprintErr ist e
1162 return "")
1164{- | Load idris module -}
1165loadModule' :: Handle -> FilePath -> Idris String
1166loadModule' outh f
1167 = do i <- getIState
1168 let file = takeWhile (/= ' ') f
1169 ibcsd <- valIBCSubDir i
1170 ids <- allImportDirs
1171 fp <- findImport ids ibcsd file
1172 if file `elem` imported i
1173 then iLOG $ "Already read " ++ file
1174 else do putIState (i { imported = file : imported i })
1175 case fp of
1176 IDR fn -> loadSource outh False fn
1177 LIDR fn -> loadSource outh True fn
1178 IBC fn src ->
1179 idrisCatch (loadIBC fn)
1180 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1181 case src of
1182 IDR sfn -> loadSource outh False sfn
1183 LIDR sfn -> loadSource outh True sfn)
1184 let (dir, fh) = splitFileName file
1185 return (dropExtension fh)
1188{- | Load idris code from file -}
1189loadFromIFile :: Handle -> IFileType -> Idris ()
1190loadFromIFile h i@(IBC fn src)
1191 = do iLOG $ "Skipping " ++ getSrcFile i
1192 idrisCatch (loadIBC fn)
1193 (\err -> ierror $ LoadingFailed fn err)
1194 where
1195 getSrcFile (IDR fn) = fn
1196 getSrcFile (LIDR fn) = fn
1197 getSrcFile (IBC f src) = getSrcFile src
1199loadFromIFile h (IDR fn) = loadSource' h False fn
1200loadFromIFile h (LIDR fn) = loadSource' h True fn
1202{-| Load idris source code and show error if something wrong happens -}
1203loadSource' :: Handle -> Bool -> FilePath -> Idris ()
1204loadSource' h lidr r
1205 = idrisCatch (loadSource h lidr r)
1206 (\e -> do setErrSpan (getErrSpan e)
1207 ist <- getIState
1208 case e of
1209 At f e' -> ihWarn h f (pprintErr ist e')
1210 _ -> ihWarn h (getErrSpan e) (pprintErr ist e))
1212{- | Load Idris source code-}
1213loadSource :: Handle -> Bool -> FilePath -> Idris ()
1214loadSource h lidr f
1215 = do iLOG ("Reading " ++ f)
1216 i <- getIState
1217 let def_total = default_total i
1218 file_in <- runIO $ readFile f
1219 file <- if lidr then tclift $ unlit f file_in else return file_in
1220 (mname, imports, pos) <- parseImports f file
1221 ids <- allImportDirs
1222 ibcsd <- valIBCSubDir i
1223 mapM_ (\f -> do fp <- findImport ids ibcsd f
1224 case fp of
1225 LIDR fn -> ifail $ "No ibc for " ++ f
1226 IDR fn -> ifail $ "No ibc for " ++ f
1227 IBC fn src -> loadIBC fn)
1228 [fn | (fn, _, _) <- imports]
1229 reportParserWarnings
1231 -- process and check module aliases
1232 let modAliases = M.fromList
1233 [(prep alias, prep realName) | (realName, Just alias, fc) <- imports]
1234 prep = map T.pack . reverse . Spl.splitOn "/"
1235 aliasNames = [(alias, fc) | (_, Just alias, fc) <- imports]
1236 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1237 case map head . filter ((/= 1) . length) $ histogram of
1238 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1239 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1241 i <- getIState
1242 putIState (i { default_access = Hidden, module_aliases = modAliases })
1243 clearIBC -- start a new .ibc file
1244 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]
1245 let syntax = defaultSyntax{ syn_namespace = reverse mname }
1246 ds' <- parseProg syntax f file pos
1248 -- Parsing done, now process declarations
1250 let ds = namespaces mname ds'
1251 logLvl 3 (show $ showDecls verbosePPOption ds)
1252 i <- getIState
1253 logLvl 10 (show (toAlist (idris_implicits i)))
1254 logLvl 3 (show (idris_infixes i))
1255 -- Now add all the declarations to the context
1256 v <- verbose
1257 when v $ ihputStrLn h $ "Type checking " ++ f
1258 -- we totality check after every Mutual block, so if
1259 -- anything is a single definition, wrap it in a
1260 -- mutual block on its own
1261 elabDecls toplevel (map toMutual ds)
1262 i <- getIState
1263 -- simplify every definition do give the totality checker
1264 -- a better chance
1265 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1266 updateContext (simplifyCasedef n))
1267 (map snd (idris_totcheck i))
1268 -- build size change graph from simplified definitions
1269 iLOG "Totality checking"
1270 i <- getIState
1271 mapM_ buildSCG (idris_totcheck i)
1272 mapM_ checkDeclTotality (idris_totcheck i)
1274 -- Redo totality check for deferred names
1275 let deftots = idris_defertotcheck i
1276 iLOG $ "Totality checking " ++ show deftots
1277 mapM_ (\x -> do tot <- getTotality x
1278 case tot of
1279 Total _ -> setTotality x Unchecked
1280 _ -> return ()) (map snd deftots)
1281 mapM_ buildSCG deftots
1282 mapM_ checkDeclTotality deftots
1284 iLOG ("Finished " ++ f)
1285 ibcsd <- valIBCSubDir i
1286 iLOG "Universe checking"
1287 iucheck
1288 let ibc = ibcPathNoFallback ibcsd f
1289 i <- getIState
1290 addHides (hide_list i)
1292 -- Finally, write an ibc if checking was successful
1293 ok <- noErrors
1294 when ok $
1295 idrisCatch (do writeIBC f ibc; clearIBC)
1296 (\c -> return ()) -- failure is harmless
1297 i <- getIState
1298 putIState (i { default_total = def_total,
1299 hide_list = [] })
1300 return ()
1301 where
1302 namespaces :: [String] -> [PDecl] -> [PDecl]
1303 namespaces [] ds = ds
1304 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1306 toMutual :: PDecl -> PDecl
1307 toMutual m@(PMutual _ d) = m
1308 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1309 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1310 case x of
1311 PClauses _ _ _ _ -> r
1312 PClass _ _ _ _ _ _ _ _ -> r
1313 PInstance _ _ _ _ _ _ _ _ -> r
1314 _ -> x
1316{- | Adds names to hide list -}
1317addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1318addHides xs = do i <- getIState
1319 let defh = default_access i
1320 let (hs, as) = partition isNothing xs
1321 unless (null as) $
1322 mapM_ doHide
1323 (map (\ (n, _) -> (n, defh)) hs ++
1324 map (\ (n, Just a) -> (n, a)) as)
1325 where isNothing (_, Nothing) = True
1326 isNothing _ = False
1328 doHide (n, a) = do setAccessibility n a
1329 addIBC (IBCAccess n a)