git.iko.soy/Idris-dev
on b0cb4e2 help sign in
Idris-dev/src/Idris/Parser.hs
1348 lines 48 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 let c = (concat decls)
132 case maxline syn of
133 Nothing -> do notOpenBraces; eof
134 _ -> return ()
135 ist <- get
136 fc <- getFC
137 put ist { idris_parsedSpan = Just (FC (fc_fname fc) (0,0) (fc_end fc)),
138 ibc_write = IBCParsedRegion fc : ibc_write ist }
139 return c
141{-| Parses a top-level declaration
144Decl ::=
145 Decl'
146 | Using
147 | Params
148 | Mutual
149 | Namespace
150 | Class
151 | Instance
152 | DSL
153 | Directive
154 | Provider
155 | Transform
156 | Import!
157 ;
159-}
160decl :: SyntaxInfo -> IdrisParser [PDecl]
161decl syn = do fc <- getFC
162 -- if we're after maxline, stop here
163 let continue = case maxline syn of
164 Nothing -> True
165 Just l -> if fst (fc_end fc) > l
166 then mut_nesting syn /= 0
167 else True
168 if continue then do notEndBlock
169 declBody
170 else fail "End of readable input"
171 where declBody :: IdrisParser [PDecl]
172 declBody = declBody'
173 <|> using_ syn
174 <|> params syn
175 <|> mutual syn
176 <|> namespace syn
177 <|> class_ syn
178 <|> instance_ syn
179 <|> do d <- dsl syn; return [d]
180 <|> directive syn
181 <|> provider syn
182 <|> transform syn
183 <|> do import_; fail "imports must be at top of file"
184 <?> "declaration"
185 declBody' :: IdrisParser [PDecl]
186 declBody' = do d <- decl' syn
187 i <- get
188 let d' = fmap (debindApp syn . (desugar syn i)) d
189 return [d']
191{- | Parses a top-level declaration with possible syntax sugar
194Decl' ::=
195 Fixity
196 | FunDecl'
197 | Data
198 | Record
199 | SyntaxDecl
200 ;
202-}
203decl' :: SyntaxInfo -> IdrisParser PDecl
204decl' syn = fixity
205 <|> syntaxDecl syn
206 <|> fnDecl' syn
207 <|> data_ syn
208 <|> record syn
209 <?> "declaration"
211{- | Parses a syntax extension declaration (and adds the rule to parser state)
214 SyntaxDecl ::= SyntaxRule;
216-}
217syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
218syntaxDecl syn = do s <- syntaxRule syn
219 i <- get
220 let rs = syntax_rules i
221 let ns = syntax_keywords i
222 let ibc = ibc_write i
223 let ks = map show (names s)
224 put (i { syntax_rules = s : rs,
225 syntax_keywords = ks ++ ns,
226 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc })
227 fc <- getFC
228 return (PSyntax fc s)
229 where names (Rule syms _ _) = mapMaybe ename syms
230 ename (Keyword n) = Just n
231 ename _ = Nothing
233{- | Parses a syntax extension declaration
236SyntaxRuleOpts ::= 'term' | 'pattern';
240SyntaxRule ::=
241 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
245SyntaxSym ::= '[' Name_t ']'
246 | '{' Name_t '}'
247 | Name_t
248 | StringLiteral_t
249 ;
251-}
252syntaxRule :: SyntaxInfo -> IdrisParser Syntax
253syntaxRule syn
254 = do sty <- try (do
255 pushIndent
256 sty <- option AnySyntax (do reserved "term"; return TermSyntax
257 <|> do reserved "pattern"; return PatternSyntax)
258 reserved "syntax"
259 return sty)
260 syms <- some syntaxSym
261 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
262 let ns = mapMaybe getName syms
263 when (length ns /= length (nub ns))
264 $ unexpected "repeated variable in syntax rule"
265 lchar '='
266 tm <- typeExpr (allowImp syn)
267 terminator
268 return (Rule (mkSimple syms) tm sty)
269 where
270 isExpr (Expr _) = True
271 isExpr _ = False
272 getName (Expr n) = Just n
273 getName _ = Nothing
274 -- Can't parse two full expressions (i.e. expressions with application) in a row
275 -- so change them both to a simple expression
276 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
277 mkSimple xs = mkSimple' xs
279 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
280 mkSimple es
281 mkSimple' (e : es) = e : mkSimple' es
282 mkSimple' [] = []
285{- | Parses a syntax symbol (either binding variable, keyword or expression)
288SyntaxSym ::= '[' Name_t ']'
289 | '{' Name_t '}'
290 | Name_t
291 | StringLiteral_t
292 ;
294 -}
295syntaxSym :: IdrisParser SSymbol
296syntaxSym = try (do lchar '['; n <- name; lchar ']'
297 return (Expr n))
298 <|> try (do lchar '{'; n <- name; lchar '}'
299 return (Binding n))
300 <|> do n <- iName []
301 return (Keyword n)
302 <|> do sym <- stringLiteral
303 return (Symbol sym)
304 <?> "syntax symbol"
306{- | Parses a function declaration with possible syntax sugar
309 FunDecl ::= FunDecl';
311-}
312fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
313fnDecl syn = try (do notEndBlock
314 d <- fnDecl' syn
315 i <- get
316 let d' = fmap (desugar syn i) d
317 return [d']) <?> "function declaration"
319{-| Parses a function declaration
322 FunDecl' ::=
323 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
324 | Postulate
325 | Pattern
326 | CAF
327 ;
329-}
330fnDecl' :: SyntaxInfo -> IdrisParser PDecl
331fnDecl' syn = checkFixity $
332 do (doc, fc, opts', n, acc) <- try (do
333 pushIndent
334 ist <- get
335 doc <- option noDocs docComment
336 ist <- get
337 let initOpts = if default_total ist
338 then [TotalFn]
339 else []
340 opts <- fnOpts initOpts
341 acc <- optional accessibility
342 opts' <- fnOpts opts
343 n_in <- fnName
344 let n = expandNS syn n_in
345 fc <- getFC
346 lchar ':'
347 return (doc, fc, opts', n, acc))
348 ty <- typeExpr (allowImp syn)
349 terminator
350 addAcc n acc
351 return (PTy (fst doc) (snd doc) syn fc opts' n ty)
352 <|> postulate syn
353 <|> caf syn
354 <|> pattern syn
355 <?> "function declaration"
356 where checkFixity :: IdrisParser PDecl -> IdrisParser PDecl
357 checkFixity p = do decl <- p
358 case getName decl of
359 Nothing -> return decl
360 Just n -> do fOk <- fixityOK n
361 unless fOk . fail $
362 "Missing fixity declaration for " ++ show n
363 return decl
364 getName (PTy _ _ _ _ _ n _) = Just n
365 getName _ = Nothing
366 fixityOK (NS n _) = fixityOK n
367 fixityOK (UN n) | all (flip elem opChars) (str n) =
368 do fixities <- fmap idris_infixes get
369 return . elem (str n) . map (\ (Fix _ op) -> op) $ fixities
370 | otherwise = return True
371 fixityOK _ = return True
373{-| Parses function options given initial options
376FnOpts ::= 'total'
377 | 'partial'
378 | 'implicit'
379 | '%' 'assert_total'
380 | '%' 'error_handler'
381 | '%' 'reflection'
382 | '%' 'specialise' '[' NameTimesList? ']'
383 ;
387NameTimes ::= FnName Natural?;
391NameTimesList ::=
392 NameTimes
393 | NameTimes ',' NameTimesList
394 ;
396-}
397-- FIXME: Check compatability for function options (i.e. partal/total)
398fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
399fnOpts opts
400 = do reserved "total"; fnOpts (TotalFn : opts)
401 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
402 <|> do reserved "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))
403 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;
404 fnOpts (CExport c : opts)
405 <|> do try (lchar '%' *> reserved "assert_total");
406 fnOpts (AssertTotal : opts)
407 <|> do try (lchar '%' *> reserved "error_handler");
408 fnOpts (ErrorHandler : opts)
409 <|> do try (lchar '%' *> reserved "error_reverse");
410 fnOpts (ErrorReverse : opts)
411 <|> do try (lchar '%' *> reserved "reflection");
412 fnOpts (Reflection : opts)
413 <|> do lchar '%'; reserved "specialise";
414 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
415 fnOpts (Specialise ns : opts)
416 <|> do reserved "implicit"; fnOpts (Implicit : opts)
417 <|> return opts
418 <?> "function modifier"
419 where nameTimes :: IdrisParser (Name, Maybe Int)
420 nameTimes = do n <- fnName
421 t <- option Nothing (do reds <- natural
422 return (Just (fromInteger reds)))
423 return (n, t)
425{- | Parses a postulate
428Postulate ::=
429 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
430 ;
432-}
433postulate :: SyntaxInfo -> IdrisParser PDecl
434postulate syn = do doc <- try $ do doc <- option noDocs docComment
435 pushIndent
436 reserved "postulate"
437 return doc
438 ist <- get
439 let initOpts = if default_total ist
440 then [TotalFn]
441 else []
442 opts <- fnOpts initOpts
443 acc <- optional accessibility
444 opts' <- fnOpts opts
445 n_in <- fnName
446 let n = expandNS syn n_in
447 lchar ':'
448 ty <- typeExpr (allowImp syn)
449 fc <- getFC
450 terminator
451 addAcc n acc
452 return (PPostulate (fst doc) syn fc opts' n ty)
453 <?> "postulate"
455{- | Parses a using declaration
458Using ::=
459 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
460 ;
462 -}
463using_ :: SyntaxInfo -> IdrisParser [PDecl]
464using_ syn =
465 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
466 openBlock
467 let uvars = using syn
468 ds <- many (decl (syn { using = uvars ++ ns }))
469 closeBlock
470 return (concat ds)
471 <?> "using declaration"
473{- | Parses a parameters declaration
476Params ::=
477 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
478 ;
480 -}
481params :: SyntaxInfo -> IdrisParser [PDecl]
482params syn =
483 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
484 openBlock
485 let pvars = syn_params syn
486 ds <- many (decl syn { syn_params = pvars ++ ns })
487 closeBlock
488 fc <- getFC
489 return [PParams fc ns (concat ds)]
490 <?> "parameters declaration"
492{- | Parses a mutual declaration (for mutually recursive functions)
495Mutual ::=
496 'mutual' OpenBlock Decl* CloseBlock
497 ;
499-}
500mutual :: SyntaxInfo -> IdrisParser [PDecl]
501mutual syn =
502 do reserved "mutual"
503 openBlock
504 let pvars = syn_params syn
505 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
506 closeBlock
507 fc <- getFC
508 return [PMutual fc (concat ds)]
509 <?> "mutual block"
511{-| Parses a namespace declaration
514Namespace ::=
515 'namespace' identifier OpenBlock Decl+ CloseBlock
516 ;
518-}
519namespace :: SyntaxInfo -> IdrisParser [PDecl]
520namespace syn =
521 do reserved "namespace"; n <- identifier;
522 openBlock
523 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
524 closeBlock
525 return [PNamespace n (concat ds)]
526 <?> "namespace declaration"
528{- | Parses a methods block (for instances)
531 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
533-}
534instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
535instanceBlock syn = do reserved "where"
536 openBlock
537 ds <- many (fnDecl syn)
538 closeBlock
539 return (concat ds)
540 <?> "instance block"
542{- | Parses a methods and instances block (for type classes)
545MethodOrInstance ::=
546 FnDecl
547 | Instance
548 ;
552ClassBlock ::=
553 'where' OpenBlock MethodOrInstance* CloseBlock
554 ;
556-}
557classBlock :: SyntaxInfo -> IdrisParser [PDecl]
558classBlock syn = do reserved "where"
559 openBlock
560 ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)
561 closeBlock
562 return (concat ds)
563 <?> "class block"
565{-| Parses a type class declaration
568ClassArgument ::=
569 Name
570 | '(' Name ':' Expr ')'
571 ;
575Class ::=
576 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
577 ;
579-}
580class_ :: SyntaxInfo -> IdrisParser [PDecl]
581class_ syn = do (doc, acc) <- try (do
582 doc <- option noDocs docComment
583 acc <- optional accessibility
584 return (doc, acc))
585 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName
586 let n = expandNS syn n_in
587 cs <- many carg
588 ds <- option [] (classBlock syn)
589 accData acc n (concatMap declared ds)
590 return [PClass (fst doc) syn fc cons n cs (snd doc) ds]
591 <?> "type-class declaration"
592 where
593 carg :: IdrisParser (Name, PTerm)
594 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
595 return (i, ty)
596 <|> do i <- name;
597 return (i, PType)
599{- | Parses a type class instance declaration
602 Instance ::=
603 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
604 ;
608InstanceName ::= '[' Name ']';
610-}
611instance_ :: SyntaxInfo -> IdrisParser [PDecl]
612instance_ syn = do reserved "instance"; fc <- getFC
613 en <- optional instanceName
614 cs <- constraintList syn
615 cn <- fnName
616 args <- many (simpleExpr syn)
617 let sc = PApp fc (PRef fc cn) (map pexp args)
618 let t = bindList (PPi constraint) (map (\x -> (sMN 0 "constraint", x)) cs) sc
619 ds <- option [] (instanceBlock syn)
620 return [PInstance syn fc cs cn args t en ds]
621 <?> "instance declaration"
622 where instanceName :: IdrisParser Name
623 instanceName = do lchar '['; n_in <- fnName; lchar ']'
624 let n = expandNS syn n_in
625 return n
626 <?> "instance name"
629{- | Parses a using declaration list
632UsingDeclList ::=
633 UsingDeclList'
634 | NameList TypeSig
635 ;
639UsingDeclList' ::=
640 UsingDecl
641 | UsingDecl ',' UsingDeclList'
642 ;
646NameList ::=
647 Name
648 | Name ',' NameList
649 ;
651-}
652usingDeclList :: SyntaxInfo -> IdrisParser [Using]
653usingDeclList syn
654 = try (sepBy1 (usingDecl syn) (lchar ','))
655 <|> do ns <- sepBy1 name (lchar ',')
656 lchar ':'
657 t <- typeExpr (disallowImp syn)
658 return (map (\x -> UImplicit x t) ns)
659 <?> "using declaration list"
661{- |Parses a using declaration
664UsingDecl ::=
665 FnName TypeSig
666 | FnName FnName+
667 ;
669-}
670usingDecl :: SyntaxInfo -> IdrisParser Using
671usingDecl syn = try (do x <- fnName
672 lchar ':'
673 t <- typeExpr (disallowImp syn)
674 return (UImplicit x t))
675 <|> do c <- fnName
676 xs <- some fnName
677 return (UConstraint c xs)
678 <?> "using declaration"
680{- | Parse a clause with patterns
683Pattern ::= Clause;
685-}
686pattern :: SyntaxInfo -> IdrisParser PDecl
687pattern syn = do fc <- getFC
688 clause <- clause syn
689 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
690 <?> "pattern"
692{- | Parse a constant applicative form declaration
695CAF ::= 'let' FnName '=' Expr Terminator;
697-}
698caf :: SyntaxInfo -> IdrisParser PDecl
699caf syn = do reserved "let"
700 n_in <- fnName; let n = expandNS syn n_in
701 lchar '='
702 t <- expr syn
703 terminator
704 fc <- getFC
705 return (PCAF fc n t)
706 <?> "constant applicative form declaration"
708{- | Parse an argument expression
711ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
713-}
714argExpr :: SyntaxInfo -> IdrisParser PTerm
715argExpr syn = let syn' = syn { inPattern = True } in
716 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
717 <?> "argument expression"
719{- | Parse a right hand side of a function
722RHS ::= '=' Expr
723 | '?=' RHSName? Expr
724 | 'impossible'
725 ;
729RHSName ::= '{' FnName '}';
731-}
732rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
733rhs syn n = do lchar '='; expr syn
734 <|> do symbol "?=";
735 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
736 return n)
737 r <- expr syn
738 return (addLet name r)
739 <|> do reserved "impossible"; return PImpossible
740 <?> "function right hand side"
741 where mkN :: Name -> Name
742 mkN (UN x) = sUN (str x++"_lemma_1")
743 mkN (NS x n) = NS (mkN x) n
744 n' :: Name
745 n' = mkN n
746 addLet :: Name -> PTerm -> PTerm
747 addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)
748 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
749 where addLetC (l, r) = (l, addLet nm r)
750 addLet nm r = (PLet (sUN "value") Placeholder r (PMetavar nm))
752{- |Parses a function clause
755RHSOrWithBlock ::= RHS WhereOrTerminator
756 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
757 ;
761Clause ::= WExpr+ RHSOrWithBlock
762 | SimpleExpr '<==' FnName RHS WhereOrTerminator
763 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
764 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
765 ;
769ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
773WhereOrTerminator ::= WhereBlock | Terminator;
775-}
776clause :: SyntaxInfo -> IdrisParser PClause
777clause syn
778 = do wargs <- try (do pushIndent; some (wExpr syn))
779 fc <- getFC
780 ist <- get
781 n <- case lastParse ist of
782 Just t -> return t
783 Nothing -> fail "Invalid clause"
784 (do r <- rhs syn n
785 let ctxt = tt_ctxt ist
786 let wsyn = syn { syn_namespace = [] }
787 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
788 popIndent
789 return x,
790 do terminator
791 return ([], [])]
792 return $ PClauseR fc wargs r wheres) <|> (do
793 popIndent
794 reserved "with"
795 wval <- simpleExpr syn
796 openBlock
797 ds <- some $ fnDecl syn
798 let withs = concat ds
799 closeBlock
800 return $ PWithR fc wargs wval withs)
801 <|> do ty <- try (do pushIndent
802 ty <- simpleExpr syn
803 symbol "<=="
804 return ty)
805 fc <- getFC
806 n_in <- fnName; let n = expandNS syn n_in
807 r <- rhs syn n
808 ist <- get
809 let ctxt = tt_ctxt ist
810 let wsyn = syn { syn_namespace = [] }
811 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
812 popIndent
813 return x,
814 do terminator
815 return ([], [])]
816 let capp = PLet (sMN 0 "match")
817 ty
818 (PMatchApp fc n)
819 (PRef fc (sMN 0 "match"))
820 ist <- get
821 put (ist { lastParse = Just n })
822 return $ PClause fc n capp [] r wheres
823 <|> do (l, op) <- try (do
824 pushIndent
825 l <- argExpr syn
826 op <- operator
827 when (op == "=" || op == "?=" ) $
828 fail "infix clause definition with \"=\" and \"?=\" not supported "
829 return (l, op))
830 let n = expandNS syn (sUN op)
831 r <- argExpr syn
832 fc <- getFC
833 wargs <- many (wExpr syn)
834 (do rs <- rhs syn n
835 let wsyn = syn { syn_namespace = [] }
836 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
837 popIndent
838 return x,
839 do terminator
840 return ([], [])]
841 ist <- get
842 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
843 put (ist { lastParse = Just n })
844 return $ PClause fc n capp wargs rs wheres) <|> (do
845 popIndent
846 reserved "with"
847 wval <- bracketed syn
848 openBlock
849 ds <- some $ fnDecl syn
850 closeBlock
851 ist <- get
852 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
853 let withs = map (fillLHSD n capp wargs) $ concat ds
854 put (ist { lastParse = Just n })
855 return $ PWith fc n capp wargs wval withs)
856 <|> do pushIndent
857 n_in <- fnName; let n = expandNS syn n_in
858 cargs <- many (constraintArg syn)
859 fc <- getFC
860 args <- many (try (implicitArg (syn { inPattern = True } ))
861 <|> (fmap pexp (argExpr syn)))
862 wargs <- many (wExpr syn)
863 let capp = PApp fc (PRef fc n)
864 (cargs ++ args)
865 (do r <- rhs syn n
866 ist <- get
867 let ctxt = tt_ctxt ist
868 let wsyn = syn { syn_namespace = [] }
869 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
870 popIndent
871 return x,
872 do terminator
873 return ([], [])]
874 ist <- get
875 put (ist { lastParse = Just n })
876 return $ PClause fc n capp wargs r wheres) <|> (do
877 reserved "with"
878 ist <- get
879 put (ist { lastParse = Just n })
880 wval <- bracketed syn
881 openBlock
882 ds <- some $ fnDecl syn
883 let withs = map (fillLHSD n capp wargs) $ concat ds
884 closeBlock
885 popIndent
886 return $ PWith fc n capp wargs wval withs)
887 <?> "function clause"
888 where
889 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
890 fillLHS n capp owargs (PClauseR fc wargs v ws)
891 = PClause fc n capp (owargs ++ wargs) v ws
892 fillLHS n capp owargs (PWithR fc wargs v ws)
893 = PWith fc n capp (owargs ++ wargs) v
894 (map (fillLHSD n capp (owargs ++ wargs)) ws)
895 fillLHS _ _ _ c = c
897 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
898 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
899 fillLHSD n c a x = x
901{-| Parses with pattern
903@
904WExpr ::= '|' Expr';
906-}
907wExpr :: SyntaxInfo -> IdrisParser PTerm
908wExpr syn = do lchar '|'
909 expr' syn
910 <?> "with pattern"
912{- | Parses a where block
915WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
917-}
918whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
919whereBlock n syn
920 = do reserved "where"
921 ds <- indentedBlock1 (decl syn)
922 let dns = concatMap (concatMap declared) ds
923 return (concat ds, map (\x -> (x, decoration syn x)) dns)
924 <?> "where block"
926{- |Parses a code generation target language name
929Codegen ::= 'C'
930 | 'Java'
931 | 'JavaScript'
932 | 'Node'
933 | 'LLVM'
934 | 'Bytecode'
935 ;
937-}
938codegen_ :: IdrisParser Codegen
939codegen_ = do reserved "C"; return ViaC
940 <|> do reserved "Java"; return ViaJava
941 <|> do reserved "JavaScript"; return ViaJavaScript
942 <|> do reserved "Node"; return ViaNode
943 <|> do reserved "LLVM"; return ViaLLVM
944 <|> do reserved "Bytecode"; return Bytecode
945 <?> "code generation language"
947{- |Parses a compiler directive
949StringList ::=
950 String
951 | String ',' StringList
952 ;
956Directive ::= '%' Directive';
960Directive' ::= 'lib' CodeGen String_t
961 | 'link' CodeGen String_t
962 | 'flag' CodeGen String_t
963 | 'include' CodeGen String_t
964 | 'hide' Name
965 | 'freeze' Name
966 | 'access' Accessibility
967 | 'default' Totality
968 | 'logging' Natural
969 | 'dynamic' StringList
970 | 'name' Name NameList
971 | 'error_handlers' Name NameList
972 | 'language' 'TypeProviders'
973 | 'language' 'ErrorReflection'
974 ;
976-}
977directive :: SyntaxInfo -> IdrisParser [PDecl]
978directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
979 return [PDirective (do addLib cgn lib
980 addIBC (IBCLib cgn lib))]
981 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
982 return [PDirective (do dirs <- allImportDirs
983 o <- liftIO $ findInPath dirs obj
984 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
985 addObjectFile cgn o)]
986 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
987 flag <- stringLiteral
988 return [PDirective (do addIBC (IBCCGFlag cgn flag)
989 addFlag cgn flag)]
990 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
991 return [PDirective (do addHdr cgn hdr
992 addIBC (IBCHeader cgn hdr))]
993 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
994 return [PDirective (do setAccessibility n Hidden
995 addIBC (IBCAccess n Hidden))]
996 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
997 return [PDirective (do setAccessibility n Frozen
998 addIBC (IBCAccess n Frozen))]
999 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1000 return [PDirective (do i <- get
1001 put(i { default_access = acc }))]
1002 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1003 i <- get
1004 put (i { default_total = tot } )
1005 return [PDirective (do i <- get
1006 put(i { default_total = tot }))]
1007 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
1008 return [PDirective (setLogLevel (fromInteger i))]
1009 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
1010 return [PDirective (do added <- addDyLib libs
1011 case added of
1012 Left lib -> addIBC (IBCDyLib (lib_name lib))
1013 Right msg ->
1014 fail $ msg)]
1015 <|> do try (lchar '%' *> reserved "name")
1016 ty <- fnName
1017 ns <- sepBy1 name (lchar ',')
1018 return [PDirective (do ty' <- disambiguate ty
1019 mapM_ (addNameHint ty') ns
1020 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1021 <|> do try (lchar '%' *> reserved "error_handlers")
1022 fn <- fnName
1023 arg <- fnName
1024 ns <- sepBy1 name (lchar ',')
1025 return [PDirective (do fn' <- disambiguate fn
1026 ns' <- mapM disambiguate ns
1027 addFunctionErrorHandlers fn' arg ns'
1028 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]
1029 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1030 return [PDirective (addLangExt ext)]
1031 <?> "directive"
1032 where disambiguate :: Name -> Idris Name
1033 disambiguate n = do i <- getIState
1034 case lookupCtxtName n (idris_implicits i) of
1035 [(n', _)] -> return n'
1036 [] -> throwError (NoSuchVariable n)
1037 more -> throwError (CantResolveAlts (map fst more))
1039pLangExt :: IdrisParser LanguageExt
1040pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1041 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1043{- | Parses a totality
1046Totality ::= 'partial' | 'total'
1050totality :: IdrisParser Bool
1051totality
1052 = do reserved "total"; return True
1053 <|> do reserved "partial"; return False
1055{- | Parses a type provider
1058Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1059ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1061 -}
1062provider :: SyntaxInfo -> IdrisParser [PDecl]
1063provider syn = do try (lchar '%' *> reserved "provide");
1064 provideTerm <|> providePostulate
1065 <?> "type provider"
1066 where provideTerm = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1067 fc <- getFC
1068 reserved "with"
1069 e <- expr syn <?> "provider expression"
1070 return [PProvider syn fc (ProvTerm t e) n]
1071 providePostulate = do reserved "postulate"
1072 n <- fnName
1073 fc <- getFC
1074 reserved "with"
1075 e <- expr syn <?> "provider expression"
1076 return [PProvider syn fc (ProvPostulate e) n]
1078{- | Parses a transform
1081Transform ::= '%' 'transform' Expr '==>' Expr
1084transform :: SyntaxInfo -> IdrisParser [PDecl]
1085transform syn = do try (lchar '%' *> reserved "transform")
1086 -- leave it unchecked, until we work out what this should
1087 -- actually mean...
1088-- safety <- option True (do reserved "unsafe"
1089-- return False)
1090 l <- expr syn
1091 fc <- getFC
1092 symbol "==>"
1093 r <- expr syn
1094 return [PTransform fc False l r]
1095 <?> "transform"
1098{- * Loading and parsing -}
1099{- | Parses an expression from input -}
1100parseExpr :: IState -> String -> Result PTerm
1101parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1103{- | Parses a constant form input -}
1104parseConst :: IState -> String -> Result Const
1105parseConst st = runparser constant st "(input)"
1107{- | Parses a tactic from input -}
1108parseTactic :: IState -> String -> Result PTactic
1109parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1111-- | Parse module header and imports
1112parseImports :: FilePath -> String -> Idris ([String], [(String, Maybe String, FC)], Maybe Delta)
1113parseImports fname input
1114 = do i <- getIState
1115 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1116 Failure err -> fail (show err)
1117 Success (x, i) -> do putIState i
1118 return x
1119 where imports :: IdrisParser (([String], [(String, Maybe String, FC)], Maybe Delta), IState)
1120 imports = do whiteSpace
1121 mname <- moduleHeader
1122 ps <- many import_
1123 mrk <- mark
1124 isEof <- lookAheadMatches eof
1125 let mrk' = if isEof
1126 then Nothing
1127 else Just mrk
1128 i <- get
1129 return ((mname, ps, mrk'), i)
1131-- | There should be a better way of doing this...
1132findFC :: Doc -> (FC, String)
1133findFC x = let s = show (plain x) in
1134 case span (/= ':') s of
1135 (failname, ':':rest) -> case span isDigit rest of
1136 (line, ':':rest') -> case span isDigit rest' of
1137 (col, ':':msg) -> let pos = (read line, read col) in
1138 (FC failname pos pos, msg)
1140-- | Check if the coloring matches the options and corrects if necessary
1141fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1142fixColour False doc = ANSI.plain doc
1143fixColour True doc = doc
1145-- | A program is a list of declarations, possibly with associated
1146-- documentation strings.
1147parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1148 Idris [PDecl]
1149parseProg syn fname input mrk
1150 = do i <- getIState
1151 case runparser mainProg i fname input of
1152 Failure doc -> do -- FIXME: Get error location from trifecta
1153 -- this can't be the solution!
1154 let (fc, msg) = findFC doc
1155 i <- getIState
1156 case idris_outputmode i of
1157 RawOutput -> ihputStrLn (idris_outh i) (show $ fixColour (idris_colourRepl i) doc)
1158 IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)
1159 putIState (i { errSpan = Just fc })
1160 return []
1161 Success (x, i) -> do putIState i
1162 reportParserWarnings
1163 return $ collect x
1164 where mainProg :: IdrisParser ([PDecl], IState)
1165 mainProg = case mrk of
1166 Nothing -> do i <- get; return ([], i)
1167 Just mrk -> do
1168 release mrk
1169 ds <- prog syn
1170 i' <- get
1171 return (ds, i')
1173{- | Load idris module and show error if something wrong happens -}
1174loadModule :: Handle -> FilePath -> Idris String
1175loadModule outh f
1176 = idrisCatch (loadModule' outh f)
1177 (\e -> do setErrSpan (getErrSpan e)
1178 ist <- getIState
1179 ihWarn outh (getErrSpan e) $ pprintErr ist e
1180 return "")
1182{- | Load idris module -}
1183loadModule' :: Handle -> FilePath -> Idris String
1184loadModule' outh f
1185 = do i <- getIState
1186 let file = takeWhile (/= ' ') f
1187 ibcsd <- valIBCSubDir i
1188 ids <- allImportDirs
1189 fp <- findImport ids ibcsd file
1190 if file `elem` imported i
1191 then iLOG $ "Already read " ++ file
1192 else do putIState (i { imported = file : imported i })
1193 case fp of
1194 IDR fn -> loadSource outh False fn Nothing
1195 LIDR fn -> loadSource outh True fn Nothing
1196 IBC fn src ->
1197 idrisCatch (loadIBC fn)
1198 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1199 case src of
1200 IDR sfn -> loadSource outh False sfn Nothing
1201 LIDR sfn -> loadSource outh True sfn Nothing)
1202 let (dir, fh) = splitFileName file
1203 return (dropExtension fh)
1206{- | Load idris code from file -}
1207loadFromIFile :: Handle -> IFileType -> Maybe Int -> Idris ()
1208loadFromIFile h i@(IBC fn src) maxline
1209 = do iLOG $ "Skipping " ++ getSrcFile i
1210 idrisCatch (loadIBC fn)
1211 (\err -> ierror $ LoadingFailed fn err)
1212 where
1213 getSrcFile (IDR fn) = fn
1214 getSrcFile (LIDR fn) = fn
1215 getSrcFile (IBC f src) = getSrcFile src
1217loadFromIFile h (IDR fn) maxline = loadSource' h False fn maxline
1218loadFromIFile h (LIDR fn) maxline = loadSource' h True fn maxline
1220{-| Load idris source code and show error if something wrong happens -}
1221loadSource' :: Handle -> Bool -> FilePath -> Maybe Int -> Idris ()
1222loadSource' h lidr r maxline
1223 = idrisCatch (loadSource h lidr r maxline)
1224 (\e -> do setErrSpan (getErrSpan e)
1225 ist <- getIState
1226 case e of
1227 At f e' -> ihWarn h f (pprintErr ist e')
1228 _ -> ihWarn h (getErrSpan e) (pprintErr ist e))
1230{- | Load Idris source code-}
1231loadSource :: Handle -> Bool -> FilePath -> Maybe Int -> Idris ()
1232loadSource h lidr f toline
1233 = do iLOG ("Reading " ++ f)
1234 i <- getIState
1235 let def_total = default_total i
1236 file_in <- runIO $ readFile f
1237 file <- if lidr then tclift $ unlit f file_in else return file_in
1238 (mname, imports, pos) <- parseImports f file
1239 ids <- allImportDirs
1240 ibcsd <- valIBCSubDir i
1241 mapM_ (\f -> do fp <- findImport ids ibcsd f
1242 case fp of
1243 LIDR fn -> ifail $ "No ibc for " ++ f
1244 IDR fn -> ifail $ "No ibc for " ++ f
1245 IBC fn src -> loadIBC fn)
1246 [fn | (fn, _, _) <- imports]
1247 reportParserWarnings
1249 -- process and check module aliases
1250 let modAliases = M.fromList
1251 [(prep alias, prep realName) | (realName, Just alias, fc) <- imports]
1252 prep = map T.pack . reverse . Spl.splitOn "/"
1253 aliasNames = [(alias, fc) | (_, Just alias, fc) <- imports]
1254 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1255 case map head . filter ((/= 1) . length) $ histogram of
1256 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1257 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1259 i <- getIState
1260 putIState (i { default_access = Hidden, module_aliases = modAliases })
1261 clearIBC -- start a new .ibc file
1262 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]
1263 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1264 maxline = toline }
1265 ds' <- parseProg syntax f file pos
1267 -- Parsing done, now process declarations
1269 let ds = namespaces mname ds'
1270 logLvl 3 (show $ showDecls verbosePPOption ds)
1271 i <- getIState
1272 logLvl 10 (show (toAlist (idris_implicits i)))
1273 logLvl 3 (show (idris_infixes i))
1274 -- Now add all the declarations to the context
1275 v <- verbose
1276 when v $ ihputStrLn h $ "Type checking " ++ f
1277 -- we totality check after every Mutual block, so if
1278 -- anything is a single definition, wrap it in a
1279 -- mutual block on its own
1280 elabDecls toplevel (map toMutual ds)
1281 i <- getIState
1282 -- simplify every definition do give the totality checker
1283 -- a better chance
1284 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1285 updateContext (simplifyCasedef n))
1286 (map snd (idris_totcheck i))
1287 -- build size change graph from simplified definitions
1288 iLOG "Totality checking"
1289 i <- getIState
1290 mapM_ buildSCG (idris_totcheck i)
1291 mapM_ checkDeclTotality (idris_totcheck i)
1293 -- Redo totality check for deferred names
1294 let deftots = idris_defertotcheck i
1295 iLOG $ "Totality checking " ++ show deftots
1296 mapM_ (\x -> do tot <- getTotality x
1297 case tot of
1298 Total _ -> setTotality x Unchecked
1299 _ -> return ()) (map snd deftots)
1300 mapM_ buildSCG deftots
1301 mapM_ checkDeclTotality deftots
1303 iLOG ("Finished " ++ f)
1304 ibcsd <- valIBCSubDir i
1305 iLOG "Universe checking"
1306 iucheck
1307 let ibc = ibcPathNoFallback ibcsd f
1308 i <- getIState
1309 addHides (hide_list i)
1311 -- Finally, write an ibc if checking was successful
1312 ok <- noErrors
1313 when ok $
1314 idrisCatch (do writeIBC f ibc; clearIBC)
1315 (\c -> return ()) -- failure is harmless
1316 i <- getIState
1317 putIState (i { default_total = def_total,
1318 hide_list = [] })
1319 return ()
1320 where
1321 namespaces :: [String] -> [PDecl] -> [PDecl]
1322 namespaces [] ds = ds
1323 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1325 toMutual :: PDecl -> PDecl
1326 toMutual m@(PMutual _ d) = m
1327 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1328 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1329 case x of
1330 PClauses _ _ _ _ -> r
1331 PClass _ _ _ _ _ _ _ _ -> r
1332 PInstance _ _ _ _ _ _ _ _ -> r
1333 _ -> x
1335{- | Adds names to hide list -}
1336addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1337addHides xs = do i <- getIState
1338 let defh = default_access i
1339 let (hs, as) = partition isNothing xs
1340 unless (null as) $
1341 mapM_ doHide
1342 (map (\ (n, _) -> (n, defh)) hs ++
1343 map (\ (n, Just a) -> (n, a)) as)
1344 where isNothing (_, Nothing) = True
1345 isNothing _ = False
1347 doHide (n, a) = do setAccessibility n a
1348 addIBC (IBCAccess n a)