git.iko.soy/Idris-dev
on dcdebfc help sign in
Idris-dev/src/Idris/Parser.hs
1331 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 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 lchar '(' <?> "parenthesized expression"
835 wval <- bracketed syn
836 openBlock
837 ds <- some $ fnDecl syn
838 closeBlock
839 ist <- get
840 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
841 let withs = map (fillLHSD n capp wargs) $ concat ds
842 put (ist { lastParse = Just n })
843 return $ PWith fc n capp wargs wval withs)
844 <|> do pushIndent
845 n_in <- fnName; let n = expandNS syn n_in
846 cargs <- many (constraintArg syn)
847 fc <- getFC
848 args <- many (try (implicitArg (syn { inPattern = True } ))
849 <|> (fmap pexp (argExpr syn)))
850 wargs <- many (wExpr syn)
851 let capp = PApp fc (PRef fc n)
852 (cargs ++ args)
853 (do r <- rhs syn n
854 ist <- get
855 let ctxt = tt_ctxt ist
856 let wsyn = syn { syn_namespace = [] }
857 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
858 popIndent
859 return x,
860 do terminator
861 return ([], [])]
862 ist <- get
863 put (ist { lastParse = Just n })
864 return $ PClause fc n capp wargs r wheres) <|> (do
865 reserved "with"
866 ist <- get
867 put (ist { lastParse = Just n })
868 lchar '(' <?> "parenthesized expression"
869 wval <- bracketed syn
870 openBlock
871 ds <- some $ fnDecl syn
872 let withs = map (fillLHSD n capp wargs) $ concat ds
873 closeBlock
874 popIndent
875 return $ PWith fc n capp wargs wval withs)
876 <?> "function clause"
877 where
878 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
879 fillLHS n capp owargs (PClauseR fc wargs v ws)
880 = PClause fc n capp (owargs ++ wargs) v ws
881 fillLHS n capp owargs (PWithR fc wargs v ws)
882 = PWith fc n capp (owargs ++ wargs) v
883 (map (fillLHSD n capp (owargs ++ wargs)) ws)
884 fillLHS _ _ _ c = c
886 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
887 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
888 fillLHSD n c a x = x
890{-| Parses with pattern
892@
893WExpr ::= '|' Expr';
895-}
896wExpr :: SyntaxInfo -> IdrisParser PTerm
897wExpr syn = do lchar '|'
898 expr' syn
899 <?> "with pattern"
901{- | Parses a where block
904WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
906-}
907whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
908whereBlock n syn
909 = do reserved "where"
910 ds <- indentedBlock1 (decl syn)
911 let dns = concatMap (concatMap declared) ds
912 return (concat ds, map (\x -> (x, decoration syn x)) dns)
913 <?> "where block"
915{- |Parses a code generation target language name
918Codegen ::= 'C'
919 | 'Java'
920 | 'JavaScript'
921 | 'Node'
922 | 'LLVM'
923 | 'Bytecode'
924 ;
926-}
927codegen_ :: IdrisParser Codegen
928codegen_ = do reserved "C"; return ViaC
929 <|> do reserved "Java"; return ViaJava
930 <|> do reserved "JavaScript"; return ViaJavaScript
931 <|> do reserved "Node"; return ViaNode
932 <|> do reserved "LLVM"; return ViaLLVM
933 <|> do reserved "Bytecode"; return Bytecode
934 <?> "code generation language"
936{- |Parses a compiler directive
938StringList ::=
939 String
940 | String ',' StringList
941 ;
945Directive ::= '%' Directive';
949Directive' ::= 'lib' CodeGen String_t
950 | 'link' CodeGen String_t
951 | 'flag' CodeGen String_t
952 | 'include' CodeGen String_t
953 | 'hide' Name
954 | 'freeze' Name
955 | 'access' Accessibility
956 | 'default' Totality
957 | 'logging' Natural
958 | 'dynamic' StringList
959 | 'name' Name NameList
960 | 'error_handlers' Name NameList
961 | 'language' 'TypeProviders'
962 | 'language' 'ErrorReflection'
963 ;
965-}
966directive :: SyntaxInfo -> IdrisParser [PDecl]
967directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
968 return [PDirective (do addLib cgn lib
969 addIBC (IBCLib cgn lib))]
970 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
971 return [PDirective (do dirs <- allImportDirs
972 o <- liftIO $ findInPath dirs obj
973 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
974 addObjectFile cgn o)]
975 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
976 flag <- stringLiteral
977 return [PDirective (do addIBC (IBCCGFlag cgn flag)
978 addFlag cgn flag)]
979 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
980 return [PDirective (do addHdr cgn hdr
981 addIBC (IBCHeader cgn hdr))]
982 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
983 return [PDirective (do setAccessibility n Hidden
984 addIBC (IBCAccess n Hidden))]
985 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
986 return [PDirective (do setAccessibility n Frozen
987 addIBC (IBCAccess n Frozen))]
988 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
989 return [PDirective (do i <- get
990 put(i { default_access = acc }))]
991 <|> do try (lchar '%' *> reserved "default"); tot <- totality
992 i <- get
993 put (i { default_total = tot } )
994 return [PDirective (do i <- get
995 put(i { default_total = tot }))]
996 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
997 return [PDirective (setLogLevel (fromInteger i))]
998 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
999 return [PDirective (do added <- addDyLib libs
1000 case added of
1001 Left lib -> addIBC (IBCDyLib (lib_name lib))
1002 Right msg ->
1003 fail $ msg)]
1004 <|> do try (lchar '%' *> reserved "name")
1005 ty <- iName []
1006 ns <- sepBy1 name (lchar ',')
1007 return [PDirective (do ty' <- disambiguate ty
1008 mapM_ (addNameHint ty') ns
1009 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1010 <|> do try (lchar '%' *> reserved "error_handlers")
1011 fn <- fnName
1012 arg <- fnName
1013 ns <- sepBy1 name (lchar ',')
1014 return [PDirective (do fn' <- disambiguate fn
1015 ns' <- mapM disambiguate ns
1016 addFunctionErrorHandlers fn' arg ns'
1017 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]
1018 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1019 return [PDirective (addLangExt ext)]
1020 <?> "directive"
1021 where disambiguate :: Name -> Idris Name
1022 disambiguate n = do i <- getIState
1023 case lookupCtxtName n (idris_implicits i) of
1024 [(n', _)] -> return n'
1025 [] -> throwError (NoSuchVariable n)
1026 more -> throwError (CantResolveAlts (map (show . fst) more))
1028pLangExt :: IdrisParser LanguageExt
1029pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1030 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1032{- | Parses a totality
1035Totality ::= 'partial' | 'total'
1039totality :: IdrisParser Bool
1040totality
1041 = do reserved "total"; return True
1042 <|> do reserved "partial"; return False
1044{- | Parses a type provider
1047Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1048ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1050 -}
1051provider :: SyntaxInfo -> IdrisParser [PDecl]
1052provider syn = do try (lchar '%' *> reserved "provide");
1053 what <- provideWhat
1054 lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1055 fc <- getFC
1056 reserved "with"
1057 e <- expr syn
1058 return [PProvider syn fc what n t e]
1059 <?> "type provider"
1060 where provideWhat :: IdrisParser ProvideWhat
1061 provideWhat = option ProvAny
1062 ( ((reserved "proof" <|> reserved "term" <|> reserved "type") *>
1063 pure ProvTerm)
1064 <|> (reserved "postulate" *> pure ProvPostulate)
1065 <?> "provider variety")
1066{- | Parses a transform
1069Transform ::= '%' 'transform' Expr '==>' Expr
1072transform :: SyntaxInfo -> IdrisParser [PDecl]
1073transform syn = do try (lchar '%' *> reserved "transform")
1074 -- leave it unchecked, until we work out what this should
1075 -- actually mean...
1076-- safety <- option True (do reserved "unsafe"
1077-- return False)
1078 l <- expr syn
1079 fc <- getFC
1080 symbol "==>"
1081 r <- expr syn
1082 return [PTransform fc False l r]
1083 <?> "transform"
1086{- * Loading and parsing -}
1087{- | Parses an expression from input -}
1088parseExpr :: IState -> String -> Result PTerm
1089parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1091{- | Parses a tactic from input -}
1092parseTactic :: IState -> String -> Result PTactic
1093parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1095-- | Parse module header and imports
1096parseImports :: FilePath -> String -> Idris ([String], [(String, Maybe String, FC)], Maybe Delta)
1097parseImports fname input
1098 = do i <- getIState
1099 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1100 Failure err -> fail (show err)
1101 Success (x, i) -> do putIState i
1102 return x
1103 where imports :: IdrisParser (([String], [(String, Maybe String, FC)], Maybe Delta), IState)
1104 imports = do whiteSpace
1105 mname <- moduleHeader
1106 ps <- many import_
1107 mrk <- mark
1108 isEof <- lookAheadMatches eof
1109 let mrk' = if isEof
1110 then Nothing
1111 else Just mrk
1112 i <- get
1113 return ((mname, ps, mrk'), i)
1115-- | There should be a better way of doing this...
1116findFC :: Doc -> (FC, String)
1117findFC x = let s = show (plain x) in
1118 case span (/= ':') s of
1119 (failname, ':':rest) -> case span isDigit rest of
1120 (line, ':':rest') -> case span isDigit rest' of
1121 (col, ':':msg) -> let pos = (read line, read col) in
1122 (FC failname pos pos, msg)
1124-- | Check if the coloring matches the options and corrects if necessary
1125fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1126fixColour False doc = ANSI.plain doc
1127fixColour True doc = doc
1129-- | A program is a list of declarations, possibly with associated
1130-- documentation strings.
1131parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1132 Idris [PDecl]
1133parseProg syn fname input mrk
1134 = do i <- getIState
1135 case runparser mainProg i fname input of
1136 Failure doc -> do -- FIXME: Get error location from trifecta
1137 -- this can't be the solution!
1138 let (fc, msg) = findFC doc
1139 i <- getIState
1140 case idris_outputmode i of
1141 RawOutput -> ihputStrLn (idris_outh i) (show $ fixColour (idris_colourRepl i) doc)
1142 IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)
1143 putIState (i { errSpan = Just fc })
1144 return []
1145 Success (x, i) -> do putIState i
1146 reportParserWarnings
1147 return $ collect x
1148 where mainProg :: IdrisParser ([PDecl], IState)
1149 mainProg = case mrk of
1150 Nothing -> do i <- get; return ([], i)
1151 Just mrk -> do
1152 release mrk
1153 ds <- prog syn
1154 i' <- get
1155 return (ds, i')
1157{- | Load idris module and show error if something wrong happens -}
1158loadModule :: Handle -> FilePath -> Idris String
1159loadModule outh f
1160 = idrisCatch (loadModule' outh f)
1161 (\e -> do setErrSpan (getErrSpan e)
1162 ist <- getIState
1163 msg <- showErr e
1164 ihputStrLn outh msg
1165 return "")
1167{- | Load idris module -}
1168loadModule' :: Handle -> FilePath -> Idris String
1169loadModule' outh f
1170 = do i <- getIState
1171 let file = takeWhile (/= ' ') f
1172 ibcsd <- valIBCSubDir i
1173 ids <- allImportDirs
1174 fp <- liftIO $ findImport ids ibcsd file
1175 if file `elem` imported i
1176 then iLOG $ "Already read " ++ file
1177 else do putIState (i { imported = file : imported i })
1178 case fp of
1179 IDR fn -> loadSource outh False fn
1180 LIDR fn -> loadSource outh True fn
1181 IBC fn src ->
1182 idrisCatch (loadIBC fn)
1183 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1184 case src of
1185 IDR sfn -> loadSource outh False sfn
1186 LIDR sfn -> loadSource outh True sfn)
1187 let (dir, fh) = splitFileName file
1188 return (dropExtension fh)
1191{- | Load idris code from file -}
1192loadFromIFile :: Handle -> IFileType -> Idris ()
1193loadFromIFile h i@(IBC fn src)
1194 = do iLOG $ "Skipping " ++ getSrcFile i
1195 idrisCatch (loadIBC fn)
1196 (\err -> ierror $ LoadingFailed fn err)
1197 where
1198 getSrcFile (IDR fn) = fn
1199 getSrcFile (LIDR fn) = fn
1200 getSrcFile (IBC f src) = getSrcFile src
1202loadFromIFile h (IDR fn) = loadSource' h False fn
1203loadFromIFile h (LIDR fn) = loadSource' h True fn
1205{-| Load idris source code and show error if something wrong happens -}
1206loadSource' :: Handle -> Bool -> FilePath -> Idris ()
1207loadSource' h lidr r
1208 = idrisCatch (loadSource h lidr r)
1209 (\e -> do setErrSpan (getErrSpan e)
1210 ist <- getIState
1211 ihRenderError h (pprintErr ist e))
1213{- | Load Idris source code-}
1214loadSource :: Handle -> Bool -> FilePath -> Idris ()
1215loadSource h lidr f
1216 = do iLOG ("Reading " ++ f)
1217 i <- getIState
1218 let def_total = default_total i
1219 file_in <- runIO $ readFile f
1220 file <- if lidr then tclift $ unlit f file_in else return file_in
1221 (mname, imports, pos) <- parseImports f file
1222 ids <- allImportDirs
1223 ibcsd <- valIBCSubDir i
1224 mapM_ (\f -> do fp <- runIO $ findImport ids ibcsd f
1225 case fp of
1226 LIDR fn -> ifail $ "No ibc for " ++ f
1227 IDR fn -> ifail $ "No ibc for " ++ f
1228 IBC fn src -> loadIBC fn)
1229 [fn | (fn, _, _) <- imports]
1230 reportParserWarnings
1232 -- process and check module aliases
1233 let modAliases = M.fromList
1234 [(prep alias, prep realName) | (realName, Just alias, fc) <- imports]
1235 prep = map T.pack . reverse . Spl.splitOn "/"
1236 aliasNames = [(alias, fc) | (_, Just alias, fc) <- imports]
1237 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1238 case map head . filter ((/= 1) . length) $ histogram of
1239 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1240 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1242 i <- getIState
1243 putIState (i { default_access = Hidden, module_aliases = modAliases })
1244 clearIBC -- start a new .ibc file
1245 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]
1246 let syntax = defaultSyntax{ syn_namespace = reverse mname }
1247 ds' <- parseProg syntax f file pos
1249 -- Parsing done, now process declarations
1251 let ds = namespaces mname ds'
1252 logLvl 3 (show $ showDecls True ds)
1253 i <- getIState
1254 logLvl 10 (show (toAlist (idris_implicits i)))
1255 logLvl 3 (show (idris_infixes i))
1256 -- Now add all the declarations to the context
1257 v <- verbose
1258 when v $ ihputStrLn h $ "Type checking " ++ f
1259 -- we totality check after every Mutual block, so if
1260 -- anything is a single definition, wrap it in a
1261 -- mutual block on its own
1262 elabDecls toplevel (map toMutual ds)
1263 i <- getIState
1264 -- simplify every definition do give the totality checker
1265 -- a better chance
1266 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1267 updateContext (simplifyCasedef n))
1268 (map snd (idris_totcheck i))
1269 -- build size change graph from simplified definitions
1270 iLOG "Totality checking"
1271 i <- getIState
1272 mapM_ buildSCG (idris_totcheck i)
1273 mapM_ checkDeclTotality (idris_totcheck i)
1275 -- Redo totality check for deferred names
1276 let deftots = idris_defertotcheck i
1277 iLOG $ "Totality checking " ++ show deftots
1278 mapM_ (\x -> do tot <- getTotality x
1279 case tot of
1280 Total _ -> setTotality x Unchecked
1281 _ -> return ()) (map snd deftots)
1282 mapM_ buildSCG deftots
1283 mapM_ checkDeclTotality deftots
1285 iLOG ("Finished " ++ f)
1286 ibcsd <- valIBCSubDir i
1287 iLOG "Universe checking"
1288 iucheck
1289 let ibc = ibcPathNoFallback ibcsd f
1290 i <- getIState
1291 addHides (hide_list i)
1293 -- Finally, write an ibc if checking was successful
1295 ok <- noErrors
1296 when ok $
1297 idrisCatch (do writeIBC f ibc; clearIBC)
1298 (\c -> return ()) -- failure is harmless
1299 i <- getIState
1300 putIState (i { default_total = def_total,
1301 hide_list = [] })
1302 return ()
1303 where
1304 namespaces :: [String] -> [PDecl] -> [PDecl]
1305 namespaces [] ds = ds
1306 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1308 toMutual :: PDecl -> PDecl
1309 toMutual m@(PMutual _ d) = m
1310 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1311 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1312 case x of
1313 PClauses _ _ _ _ -> r
1314 PClass _ _ _ _ _ _ _ -> r
1315 PInstance _ _ _ _ _ _ _ _ -> r
1316 _ -> x
1318{- | Adds names to hide list -}
1319addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1320addHides xs = do i <- getIState
1321 let defh = default_access i
1322 let (hs, as) = partition isNothing xs
1323 unless (null as) $
1324 mapM_ doHide
1325 (map (\ (n, _) -> (n, defh)) hs ++
1326 map (\ (n, Just a) -> (n, a)) as)
1327 where isNothing (_, Nothing) = True
1328 isNothing _ = False
1330 doHide (n, a) = do setAccessibility n a
1331 addIBC (IBCAccess n a)