git.iko.soy/Idris-dev
on e23ebda help sign in
Idris-dev/src/Idris/Parser.hs
1333 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 hiding (Const)
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 <- fnName
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 constant form input -}
1090parseConst :: IState -> String -> Result Const
1091parseConst st = runparser constant st "(input)"
1093{- | Parses a tactic from input -}
1094parseTactic :: IState -> String -> Result PTactic
1095parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1097-- | Parse module header and imports
1098parseImports :: FilePath -> String -> Idris ([String], [(String, Maybe String, FC)], Maybe Delta)
1099parseImports fname input
1100 = do i <- getIState
1101 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1102 Failure err -> fail (show err)
1103 Success (x, i) -> do putIState i
1104 return x
1105 where imports :: IdrisParser (([String], [(String, Maybe String, FC)], Maybe Delta), IState)
1106 imports = do whiteSpace
1107 mname <- moduleHeader
1108 ps <- many import_
1109 mrk <- mark
1110 isEof <- lookAheadMatches eof
1111 let mrk' = if isEof
1112 then Nothing
1113 else Just mrk
1114 i <- get
1115 return ((mname, ps, mrk'), i)
1117-- | There should be a better way of doing this...
1118findFC :: Doc -> (FC, String)
1119findFC x = let s = show (plain x) in
1120 case span (/= ':') s of
1121 (failname, ':':rest) -> case span isDigit rest of
1122 (line, ':':rest') -> case span isDigit rest' of
1123 (col, ':':msg) -> let pos = (read line, read col) in
1124 (FC failname pos pos, msg)
1126-- | Check if the coloring matches the options and corrects if necessary
1127fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1128fixColour False doc = ANSI.plain doc
1129fixColour True doc = doc
1131-- | A program is a list of declarations, possibly with associated
1132-- documentation strings.
1133parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1134 Idris [PDecl]
1135parseProg syn fname input mrk
1136 = do i <- getIState
1137 case runparser mainProg i fname input of
1138 Failure doc -> do -- FIXME: Get error location from trifecta
1139 -- this can't be the solution!
1140 let (fc, msg) = findFC doc
1141 i <- getIState
1142 case idris_outputmode i of
1143 RawOutput -> ihputStrLn (idris_outh i) (show $ fixColour (idris_colourRepl i) doc)
1144 IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)
1145 putIState (i { errSpan = Just fc })
1146 return []
1147 Success (x, i) -> do putIState i
1148 reportParserWarnings
1149 return $ collect x
1150 where mainProg :: IdrisParser ([PDecl], IState)
1151 mainProg = case mrk of
1152 Nothing -> do i <- get; return ([], i)
1153 Just mrk -> do
1154 release mrk
1155 ds <- prog syn
1156 i' <- get
1157 return (ds, i')
1159{- | Load idris module and show error if something wrong happens -}
1160loadModule :: Handle -> FilePath -> Idris String
1161loadModule outh f
1162 = idrisCatch (loadModule' outh f)
1163 (\e -> do setErrSpan (getErrSpan e)
1164 ist <- getIState
1165 ihWarn outh (getErrSpan e) $ pprintErr ist e
1166 return "")
1168{- | Load idris module -}
1169loadModule' :: Handle -> FilePath -> Idris String
1170loadModule' outh f
1171 = do i <- getIState
1172 let file = takeWhile (/= ' ') f
1173 ibcsd <- valIBCSubDir i
1174 ids <- allImportDirs
1175 fp <- findImport ids ibcsd file
1176 if file `elem` imported i
1177 then iLOG $ "Already read " ++ file
1178 else do putIState (i { imported = file : imported i })
1179 case fp of
1180 IDR fn -> loadSource outh False fn
1181 LIDR fn -> loadSource outh True fn
1182 IBC fn src ->
1183 idrisCatch (loadIBC fn)
1184 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1185 case src of
1186 IDR sfn -> loadSource outh False sfn
1187 LIDR sfn -> loadSource outh True sfn)
1188 let (dir, fh) = splitFileName file
1189 return (dropExtension fh)
1192{- | Load idris code from file -}
1193loadFromIFile :: Handle -> IFileType -> Idris ()
1194loadFromIFile h i@(IBC fn src)
1195 = do iLOG $ "Skipping " ++ getSrcFile i
1196 idrisCatch (loadIBC fn)
1197 (\err -> ierror $ LoadingFailed fn err)
1198 where
1199 getSrcFile (IDR fn) = fn
1200 getSrcFile (LIDR fn) = fn
1201 getSrcFile (IBC f src) = getSrcFile src
1203loadFromIFile h (IDR fn) = loadSource' h False fn
1204loadFromIFile h (LIDR fn) = loadSource' h True fn
1206{-| Load idris source code and show error if something wrong happens -}
1207loadSource' :: Handle -> Bool -> FilePath -> Idris ()
1208loadSource' h lidr r
1209 = idrisCatch (loadSource h lidr r)
1210 (\e -> do setErrSpan (getErrSpan e)
1211 ist <- getIState
1212 case e of
1213 At f e' -> ihWarn h f (pprintErr ist e')
1214 _ -> ihWarn h (getErrSpan e) (pprintErr ist e))
1216{- | Load Idris source code-}
1217loadSource :: Handle -> Bool -> FilePath -> Idris ()
1218loadSource h lidr f
1219 = do iLOG ("Reading " ++ f)
1220 i <- getIState
1221 let def_total = default_total i
1222 file_in <- runIO $ readFile f
1223 file <- if lidr then tclift $ unlit f file_in else return file_in
1224 (mname, imports, pos) <- parseImports f file
1225 ids <- allImportDirs
1226 ibcsd <- valIBCSubDir i
1227 mapM_ (\f -> do fp <- findImport ids ibcsd f
1228 case fp of
1229 LIDR fn -> ifail $ "No ibc for " ++ f
1230 IDR fn -> ifail $ "No ibc for " ++ f
1231 IBC fn src -> loadIBC fn)
1232 [fn | (fn, _, _) <- imports]
1233 reportParserWarnings
1235 -- process and check module aliases
1236 let modAliases = M.fromList
1237 [(prep alias, prep realName) | (realName, Just alias, fc) <- imports]
1238 prep = map T.pack . reverse . Spl.splitOn "/"
1239 aliasNames = [(alias, fc) | (_, Just alias, fc) <- imports]
1240 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1241 case map head . filter ((/= 1) . length) $ histogram of
1242 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1243 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1245 i <- getIState
1246 putIState (i { default_access = Hidden, module_aliases = modAliases })
1247 clearIBC -- start a new .ibc file
1248 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]
1249 let syntax = defaultSyntax{ syn_namespace = reverse mname }
1250 ds' <- parseProg syntax f file pos
1252 -- Parsing done, now process declarations
1254 let ds = namespaces mname ds'
1255 logLvl 3 (show $ showDecls verbosePPOption ds)
1256 i <- getIState
1257 logLvl 10 (show (toAlist (idris_implicits i)))
1258 logLvl 3 (show (idris_infixes i))
1259 -- Now add all the declarations to the context
1260 v <- verbose
1261 when v $ ihputStrLn h $ "Type checking " ++ f
1262 -- we totality check after every Mutual block, so if
1263 -- anything is a single definition, wrap it in a
1264 -- mutual block on its own
1265 elabDecls toplevel (map toMutual ds)
1266 i <- getIState
1267 -- simplify every definition do give the totality checker
1268 -- a better chance
1269 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1270 updateContext (simplifyCasedef n))
1271 (map snd (idris_totcheck i))
1272 -- build size change graph from simplified definitions
1273 iLOG "Totality checking"
1274 i <- getIState
1275 mapM_ buildSCG (idris_totcheck i)
1276 mapM_ checkDeclTotality (idris_totcheck i)
1278 -- Redo totality check for deferred names
1279 let deftots = idris_defertotcheck i
1280 iLOG $ "Totality checking " ++ show deftots
1281 mapM_ (\x -> do tot <- getTotality x
1282 case tot of
1283 Total _ -> setTotality x Unchecked
1284 _ -> return ()) (map snd deftots)
1285 mapM_ buildSCG deftots
1286 mapM_ checkDeclTotality deftots
1288 iLOG ("Finished " ++ f)
1289 ibcsd <- valIBCSubDir i
1290 iLOG "Universe checking"
1291 iucheck
1292 let ibc = ibcPathNoFallback ibcsd f
1293 i <- getIState
1294 addHides (hide_list i)
1296 -- Finally, write an ibc if checking was successful
1297 ok <- noErrors
1298 when ok $
1299 idrisCatch (do writeIBC f ibc; clearIBC)
1300 (\c -> return ()) -- failure is harmless
1301 i <- getIState
1302 putIState (i { default_total = def_total,
1303 hide_list = [] })
1304 return ()
1305 where
1306 namespaces :: [String] -> [PDecl] -> [PDecl]
1307 namespaces [] ds = ds
1308 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1310 toMutual :: PDecl -> PDecl
1311 toMutual m@(PMutual _ d) = m
1312 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1313 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1314 case x of
1315 PClauses _ _ _ _ -> r
1316 PClass _ _ _ _ _ _ _ _ -> r
1317 PInstance _ _ _ _ _ _ _ _ -> r
1318 _ -> x
1320{- | Adds names to hide list -}
1321addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1322addHides xs = do i <- getIState
1323 let defh = default_access i
1324 let (hs, as) = partition isNothing xs
1325 unless (null as) $
1326 mapM_ doHide
1327 (map (\ (n, _) -> (n, defh)) hs ++
1328 map (\ (n, Just a) -> (n, a)) as)
1329 where isNothing (_, Nothing) = True
1330 isNothing _ = False
1332 doHide (n, a) = do setAccessibility n a
1333 addIBC (IBCAccess n a)