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