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