git.iko.soy/Idris-dev
on 2aed52a help sign in
Idris-dev/src/Idris/Parser.hs
1350 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) = if (tnull x || not (isAlpha (thead x)))
743 then sUN "infix_op_lemma_1"
744 else sUN (str x++"_lemma_1")
745 mkN (NS x n) = NS (mkN x) n
746 n' :: Name
747 n' = mkN n
748 addLet :: Name -> PTerm -> PTerm
749 addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)
750 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
751 where addLetC (l, r) = (l, addLet nm r)
752 addLet nm r = (PLet (sUN "value") Placeholder r (PMetavar nm))
754{- |Parses a function clause
757RHSOrWithBlock ::= RHS WhereOrTerminator
758 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
759 ;
763Clause ::= WExpr+ RHSOrWithBlock
764 | SimpleExpr '<==' FnName RHS WhereOrTerminator
765 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
766 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
767 ;
771ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
775WhereOrTerminator ::= WhereBlock | Terminator;
777-}
778clause :: SyntaxInfo -> IdrisParser PClause
779clause syn
780 = do wargs <- try (do pushIndent; some (wExpr syn))
781 fc <- getFC
782 ist <- get
783 n <- case lastParse ist of
784 Just t -> return t
785 Nothing -> fail "Invalid clause"
786 (do r <- rhs syn n
787 let ctxt = tt_ctxt ist
788 let wsyn = syn { syn_namespace = [] }
789 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
790 popIndent
791 return x,
792 do terminator
793 return ([], [])]
794 return $ PClauseR fc wargs r wheres) <|> (do
795 popIndent
796 reserved "with"
797 wval <- simpleExpr syn
798 openBlock
799 ds <- some $ fnDecl syn
800 let withs = concat ds
801 closeBlock
802 return $ PWithR fc wargs wval withs)
803 <|> do ty <- try (do pushIndent
804 ty <- simpleExpr syn
805 symbol "<=="
806 return ty)
807 fc <- getFC
808 n_in <- fnName; let n = expandNS syn n_in
809 r <- rhs syn n
810 ist <- get
811 let ctxt = tt_ctxt ist
812 let wsyn = syn { syn_namespace = [] }
813 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
814 popIndent
815 return x,
816 do terminator
817 return ([], [])]
818 let capp = PLet (sMN 0 "match")
819 ty
820 (PMatchApp fc n)
821 (PRef fc (sMN 0 "match"))
822 ist <- get
823 put (ist { lastParse = Just n })
824 return $ PClause fc n capp [] r wheres
825 <|> do (l, op) <- try (do
826 pushIndent
827 l <- argExpr syn
828 op <- operator
829 when (op == "=" || op == "?=" ) $
830 fail "infix clause definition with \"=\" and \"?=\" not supported "
831 return (l, op))
832 let n = expandNS syn (sUN op)
833 r <- argExpr syn
834 fc <- getFC
835 wargs <- many (wExpr syn)
836 (do rs <- rhs syn n
837 let wsyn = syn { syn_namespace = [] }
838 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
839 popIndent
840 return x,
841 do terminator
842 return ([], [])]
843 ist <- get
844 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
845 put (ist { lastParse = Just n })
846 return $ PClause fc n capp wargs rs wheres) <|> (do
847 popIndent
848 reserved "with"
849 wval <- bracketed syn
850 openBlock
851 ds <- some $ fnDecl syn
852 closeBlock
853 ist <- get
854 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
855 let withs = map (fillLHSD n capp wargs) $ concat ds
856 put (ist { lastParse = Just n })
857 return $ PWith fc n capp wargs wval withs)
858 <|> do pushIndent
859 n_in <- fnName; let n = expandNS syn n_in
860 cargs <- many (constraintArg syn)
861 fc <- getFC
862 args <- many (try (implicitArg (syn { inPattern = True } ))
863 <|> (fmap pexp (argExpr syn)))
864 wargs <- many (wExpr syn)
865 let capp = PApp fc (PRef fc n)
866 (cargs ++ args)
867 (do r <- rhs syn n
868 ist <- get
869 let ctxt = tt_ctxt ist
870 let wsyn = syn { syn_namespace = [] }
871 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
872 popIndent
873 return x,
874 do terminator
875 return ([], [])]
876 ist <- get
877 put (ist { lastParse = Just n })
878 return $ PClause fc n capp wargs r wheres) <|> (do
879 reserved "with"
880 ist <- get
881 put (ist { lastParse = Just n })
882 wval <- bracketed syn
883 openBlock
884 ds <- some $ fnDecl syn
885 let withs = map (fillLHSD n capp wargs) $ concat ds
886 closeBlock
887 popIndent
888 return $ PWith fc n capp wargs wval withs)
889 <?> "function clause"
890 where
891 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
892 fillLHS n capp owargs (PClauseR fc wargs v ws)
893 = PClause fc n capp (owargs ++ wargs) v ws
894 fillLHS n capp owargs (PWithR fc wargs v ws)
895 = PWith fc n capp (owargs ++ wargs) v
896 (map (fillLHSD n capp (owargs ++ wargs)) ws)
897 fillLHS _ _ _ c = c
899 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
900 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
901 fillLHSD n c a x = x
903{-| Parses with pattern
905@
906WExpr ::= '|' Expr';
908-}
909wExpr :: SyntaxInfo -> IdrisParser PTerm
910wExpr syn = do lchar '|'
911 expr' syn
912 <?> "with pattern"
914{- | Parses a where block
917WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
919-}
920whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
921whereBlock n syn
922 = do reserved "where"
923 ds <- indentedBlock1 (decl syn)
924 let dns = concatMap (concatMap declared) ds
925 return (concat ds, map (\x -> (x, decoration syn x)) dns)
926 <?> "where block"
928{- |Parses a code generation target language name
931Codegen ::= 'C'
932 | 'Java'
933 | 'JavaScript'
934 | 'Node'
935 | 'LLVM'
936 | 'Bytecode'
937 ;
939-}
940codegen_ :: IdrisParser Codegen
941codegen_ = do reserved "C"; return ViaC
942 <|> do reserved "Java"; return ViaJava
943 <|> do reserved "JavaScript"; return ViaJavaScript
944 <|> do reserved "Node"; return ViaNode
945 <|> do reserved "LLVM"; return ViaLLVM
946 <|> do reserved "Bytecode"; return Bytecode
947 <?> "code generation language"
949{- |Parses a compiler directive
951StringList ::=
952 String
953 | String ',' StringList
954 ;
958Directive ::= '%' Directive';
962Directive' ::= 'lib' CodeGen String_t
963 | 'link' CodeGen String_t
964 | 'flag' CodeGen String_t
965 | 'include' CodeGen String_t
966 | 'hide' Name
967 | 'freeze' Name
968 | 'access' Accessibility
969 | 'default' Totality
970 | 'logging' Natural
971 | 'dynamic' StringList
972 | 'name' Name NameList
973 | 'error_handlers' Name NameList
974 | 'language' 'TypeProviders'
975 | 'language' 'ErrorReflection'
976 ;
978-}
979directive :: SyntaxInfo -> IdrisParser [PDecl]
980directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
981 return [PDirective (do addLib cgn lib
982 addIBC (IBCLib cgn lib))]
983 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
984 return [PDirective (do dirs <- allImportDirs
985 o <- liftIO $ findInPath dirs obj
986 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
987 addObjectFile cgn o)]
988 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
989 flag <- stringLiteral
990 return [PDirective (do addIBC (IBCCGFlag cgn flag)
991 addFlag cgn flag)]
992 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
993 return [PDirective (do addHdr cgn hdr
994 addIBC (IBCHeader cgn hdr))]
995 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
996 return [PDirective (do setAccessibility n Hidden
997 addIBC (IBCAccess n Hidden))]
998 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
999 return [PDirective (do setAccessibility n Frozen
1000 addIBC (IBCAccess n Frozen))]
1001 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1002 return [PDirective (do i <- get
1003 put(i { default_access = acc }))]
1004 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1005 i <- get
1006 put (i { default_total = tot } )
1007 return [PDirective (do i <- get
1008 put(i { default_total = tot }))]
1009 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
1010 return [PDirective (setLogLevel (fromInteger i))]
1011 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
1012 return [PDirective (do added <- addDyLib libs
1013 case added of
1014 Left lib -> addIBC (IBCDyLib (lib_name lib))
1015 Right msg ->
1016 fail $ msg)]
1017 <|> do try (lchar '%' *> reserved "name")
1018 ty <- fnName
1019 ns <- sepBy1 name (lchar ',')
1020 return [PDirective (do ty' <- disambiguate ty
1021 mapM_ (addNameHint ty') ns
1022 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1023 <|> do try (lchar '%' *> reserved "error_handlers")
1024 fn <- fnName
1025 arg <- fnName
1026 ns <- sepBy1 name (lchar ',')
1027 return [PDirective (do fn' <- disambiguate fn
1028 ns' <- mapM disambiguate ns
1029 addFunctionErrorHandlers fn' arg ns'
1030 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]
1031 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1032 return [PDirective (addLangExt ext)]
1033 <?> "directive"
1034 where disambiguate :: Name -> Idris Name
1035 disambiguate n = do i <- getIState
1036 case lookupCtxtName n (idris_implicits i) of
1037 [(n', _)] -> return n'
1038 [] -> throwError (NoSuchVariable n)
1039 more -> throwError (CantResolveAlts (map fst more))
1041pLangExt :: IdrisParser LanguageExt
1042pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1043 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1045{- | Parses a totality
1048Totality ::= 'partial' | 'total'
1052totality :: IdrisParser Bool
1053totality
1054 = do reserved "total"; return True
1055 <|> do reserved "partial"; return False
1057{- | Parses a type provider
1060Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1061ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1063 -}
1064provider :: SyntaxInfo -> IdrisParser [PDecl]
1065provider syn = do try (lchar '%' *> reserved "provide");
1066 provideTerm <|> providePostulate
1067 <?> "type provider"
1068 where provideTerm = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1069 fc <- getFC
1070 reserved "with"
1071 e <- expr syn <?> "provider expression"
1072 return [PProvider syn fc (ProvTerm t e) n]
1073 providePostulate = do reserved "postulate"
1074 n <- fnName
1075 fc <- getFC
1076 reserved "with"
1077 e <- expr syn <?> "provider expression"
1078 return [PProvider syn fc (ProvPostulate e) n]
1080{- | Parses a transform
1083Transform ::= '%' 'transform' Expr '==>' Expr
1086transform :: SyntaxInfo -> IdrisParser [PDecl]
1087transform syn = do try (lchar '%' *> reserved "transform")
1088 -- leave it unchecked, until we work out what this should
1089 -- actually mean...
1090-- safety <- option True (do reserved "unsafe"
1091-- return False)
1092 l <- expr syn
1093 fc <- getFC
1094 symbol "==>"
1095 r <- expr syn
1096 return [PTransform fc False l r]
1097 <?> "transform"
1100{- * Loading and parsing -}
1101{- | Parses an expression from input -}
1102parseExpr :: IState -> String -> Result PTerm
1103parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1105{- | Parses a constant form input -}
1106parseConst :: IState -> String -> Result Const
1107parseConst st = runparser constant st "(input)"
1109{- | Parses a tactic from input -}
1110parseTactic :: IState -> String -> Result PTactic
1111parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1113-- | Parse module header and imports
1114parseImports :: FilePath -> String -> Idris ([String], [(String, Maybe String, FC)], Maybe Delta)
1115parseImports fname input
1116 = do i <- getIState
1117 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1118 Failure err -> fail (show err)
1119 Success (x, i) -> do putIState i
1120 return x
1121 where imports :: IdrisParser (([String], [(String, Maybe String, FC)], Maybe Delta), IState)
1122 imports = do whiteSpace
1123 mname <- moduleHeader
1124 ps <- many import_
1125 mrk <- mark
1126 isEof <- lookAheadMatches eof
1127 let mrk' = if isEof
1128 then Nothing
1129 else Just mrk
1130 i <- get
1131 return ((mname, ps, mrk'), i)
1133-- | There should be a better way of doing this...
1134findFC :: Doc -> (FC, String)
1135findFC x = let s = show (plain x) in
1136 case span (/= ':') s of
1137 (failname, ':':rest) -> case span isDigit rest of
1138 (line, ':':rest') -> case span isDigit rest' of
1139 (col, ':':msg) -> let pos = (read line, read col) in
1140 (FC failname pos pos, msg)
1142-- | Check if the coloring matches the options and corrects if necessary
1143fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1144fixColour False doc = ANSI.plain doc
1145fixColour True doc = doc
1147-- | A program is a list of declarations, possibly with associated
1148-- documentation strings.
1149parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1150 Idris [PDecl]
1151parseProg syn fname input mrk
1152 = do i <- getIState
1153 case runparser mainProg i fname input of
1154 Failure doc -> do -- FIXME: Get error location from trifecta
1155 -- this can't be the solution!
1156 let (fc, msg) = findFC doc
1157 i <- getIState
1158 case idris_outputmode i of
1159 RawOutput -> ihputStrLn (idris_outh i) (show $ fixColour (idris_colourRepl i) doc)
1160 IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)
1161 putIState (i { errSpan = Just fc })
1162 return []
1163 Success (x, i) -> do putIState i
1164 reportParserWarnings
1165 return $ collect x
1166 where mainProg :: IdrisParser ([PDecl], IState)
1167 mainProg = case mrk of
1168 Nothing -> do i <- get; return ([], i)
1169 Just mrk -> do
1170 release mrk
1171 ds <- prog syn
1172 i' <- get
1173 return (ds, i')
1175{- | Load idris module and show error if something wrong happens -}
1176loadModule :: Handle -> FilePath -> Idris String
1177loadModule outh f
1178 = idrisCatch (loadModule' outh f)
1179 (\e -> do setErrSpan (getErrSpan e)
1180 ist <- getIState
1181 ihWarn outh (getErrSpan e) $ pprintErr ist e
1182 return "")
1184{- | Load idris module -}
1185loadModule' :: Handle -> FilePath -> Idris String
1186loadModule' outh f
1187 = do i <- getIState
1188 let file = takeWhile (/= ' ') f
1189 ibcsd <- valIBCSubDir i
1190 ids <- allImportDirs
1191 fp <- findImport ids ibcsd file
1192 if file `elem` imported i
1193 then iLOG $ "Already read " ++ file
1194 else do putIState (i { imported = file : imported i })
1195 case fp of
1196 IDR fn -> loadSource outh False fn Nothing
1197 LIDR fn -> loadSource outh True fn Nothing
1198 IBC fn src ->
1199 idrisCatch (loadIBC fn)
1200 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1201 case src of
1202 IDR sfn -> loadSource outh False sfn Nothing
1203 LIDR sfn -> loadSource outh True sfn Nothing)
1204 let (dir, fh) = splitFileName file
1205 return (dropExtension fh)
1208{- | Load idris code from file -}
1209loadFromIFile :: Handle -> IFileType -> Maybe Int -> Idris ()
1210loadFromIFile h i@(IBC fn src) maxline
1211 = do iLOG $ "Skipping " ++ getSrcFile i
1212 idrisCatch (loadIBC fn)
1213 (\err -> ierror $ LoadingFailed fn err)
1214 where
1215 getSrcFile (IDR fn) = fn
1216 getSrcFile (LIDR fn) = fn
1217 getSrcFile (IBC f src) = getSrcFile src
1219loadFromIFile h (IDR fn) maxline = loadSource' h False fn maxline
1220loadFromIFile h (LIDR fn) maxline = loadSource' h True fn maxline
1222{-| Load idris source code and show error if something wrong happens -}
1223loadSource' :: Handle -> Bool -> FilePath -> Maybe Int -> Idris ()
1224loadSource' h lidr r maxline
1225 = idrisCatch (loadSource h lidr r maxline)
1226 (\e -> do setErrSpan (getErrSpan e)
1227 ist <- getIState
1228 case e of
1229 At f e' -> ihWarn h f (pprintErr ist e')
1230 _ -> ihWarn h (getErrSpan e) (pprintErr ist e))
1232{- | Load Idris source code-}
1233loadSource :: Handle -> Bool -> FilePath -> Maybe Int -> Idris ()
1234loadSource h lidr f toline
1235 = do iLOG ("Reading " ++ f)
1236 i <- getIState
1237 let def_total = default_total i
1238 file_in <- runIO $ readFile f
1239 file <- if lidr then tclift $ unlit f file_in else return file_in
1240 (mname, imports, pos) <- parseImports f file
1241 ids <- allImportDirs
1242 ibcsd <- valIBCSubDir i
1243 mapM_ (\f -> do fp <- findImport ids ibcsd f
1244 case fp of
1245 LIDR fn -> ifail $ "No ibc for " ++ f
1246 IDR fn -> ifail $ "No ibc for " ++ f
1247 IBC fn src -> loadIBC fn)
1248 [fn | (fn, _, _) <- imports]
1249 reportParserWarnings
1251 -- process and check module aliases
1252 let modAliases = M.fromList
1253 [(prep alias, prep realName) | (realName, Just alias, fc) <- imports]
1254 prep = map T.pack . reverse . Spl.splitOn "/"
1255 aliasNames = [(alias, fc) | (_, Just alias, fc) <- imports]
1256 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1257 case map head . filter ((/= 1) . length) $ histogram of
1258 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1259 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1261 i <- getIState
1262 putIState (i { default_access = Hidden, module_aliases = modAliases })
1263 clearIBC -- start a new .ibc file
1264 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]
1265 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1266 maxline = toline }
1267 ds' <- parseProg syntax f file pos
1269 -- Parsing done, now process declarations
1271 let ds = namespaces mname ds'
1272 logLvl 3 (show $ showDecls verbosePPOption ds)
1273 i <- getIState
1274 logLvl 10 (show (toAlist (idris_implicits i)))
1275 logLvl 3 (show (idris_infixes i))
1276 -- Now add all the declarations to the context
1277 v <- verbose
1278 when v $ ihputStrLn h $ "Type checking " ++ f
1279 -- we totality check after every Mutual block, so if
1280 -- anything is a single definition, wrap it in a
1281 -- mutual block on its own
1282 elabDecls toplevel (map toMutual ds)
1283 i <- getIState
1284 -- simplify every definition do give the totality checker
1285 -- a better chance
1286 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1287 updateContext (simplifyCasedef n $ getErasureInfo i))
1288 (map snd (idris_totcheck i))
1289 -- build size change graph from simplified definitions
1290 iLOG "Totality checking"
1291 i <- getIState
1292 mapM_ buildSCG (idris_totcheck i)
1293 mapM_ checkDeclTotality (idris_totcheck i)
1295 -- Redo totality check for deferred names
1296 let deftots = idris_defertotcheck i
1297 iLOG $ "Totality checking " ++ show deftots
1298 mapM_ (\x -> do tot <- getTotality x
1299 case tot of
1300 Total _ -> setTotality x Unchecked
1301 _ -> return ()) (map snd deftots)
1302 mapM_ buildSCG deftots
1303 mapM_ checkDeclTotality deftots
1305 iLOG ("Finished " ++ f)
1306 ibcsd <- valIBCSubDir i
1307 iLOG "Universe checking"
1308 iucheck
1309 let ibc = ibcPathNoFallback ibcsd f
1310 i <- getIState
1311 addHides (hide_list i)
1313 -- Finally, write an ibc if checking was successful
1314 ok <- noErrors
1315 when ok $
1316 idrisCatch (do writeIBC f ibc; clearIBC)
1317 (\c -> return ()) -- failure is harmless
1318 i <- getIState
1319 putIState (i { default_total = def_total,
1320 hide_list = [] })
1321 return ()
1322 where
1323 namespaces :: [String] -> [PDecl] -> [PDecl]
1324 namespaces [] ds = ds
1325 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1327 toMutual :: PDecl -> PDecl
1328 toMutual m@(PMutual _ d) = m
1329 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1330 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1331 case x of
1332 PClauses _ _ _ _ -> r
1333 PClass _ _ _ _ _ _ _ _ -> r
1334 PInstance _ _ _ _ _ _ _ _ -> r
1335 _ -> x
1337{- | Adds names to hide list -}
1338addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1339addHides xs = do i <- getIState
1340 let defh = default_access i
1341 let (hs, as) = partition isNothing xs
1342 unless (null as) $
1343 mapM_ doHide
1344 (map (\ (n, _) -> (n, defh)) hs ++
1345 map (\ (n, Just a) -> (n, a)) as)
1346 where isNothing (_, Nothing) = True
1347 isNothing _ = False
1349 doHide (n, a) = do setAccessibility n a
1350 addIBC (IBCAccess n a)