git.iko.soy/Idris-dev
on af2fb53 help sign in
Idris-dev/src/Idris/Parser.hs
1354 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 | '%' 'no_implicit'
380 | '%' 'assert_total'
381 | '%' 'error_handler'
382 | '%' 'reflection'
383 | '%' 'specialise' '[' NameTimesList? ']'
384 ;
388NameTimes ::= FnName Natural?;
392NameTimesList ::=
393 NameTimes
394 | NameTimes ',' NameTimesList
395 ;
397-}
398-- FIXME: Check compatability for function options (i.e. partal/total)
399fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
400fnOpts opts
401 = do reserved "total"; fnOpts (TotalFn : opts)
402 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
403 <|> do reserved "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))
404 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;
405 fnOpts (CExport c : opts)
406 <|> do try (lchar '%' *> reserved "no_implicit");
407 fnOpts (NoImplicit : opts)
408 <|> do try (lchar '%' *> reserved "assert_total");
409 fnOpts (AssertTotal : opts)
410 <|> do try (lchar '%' *> reserved "error_handler");
411 fnOpts (ErrorHandler : opts)
412 <|> do try (lchar '%' *> reserved "error_reverse");
413 fnOpts (ErrorReverse : opts)
414 <|> do try (lchar '%' *> reserved "reflection");
415 fnOpts (Reflection : opts)
416 <|> do lchar '%'; reserved "specialise";
417 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
418 fnOpts (Specialise ns : opts)
419 <|> do reserved "implicit"; fnOpts (Implicit : opts)
420 <|> return opts
421 <?> "function modifier"
422 where nameTimes :: IdrisParser (Name, Maybe Int)
423 nameTimes = do n <- fnName
424 t <- option Nothing (do reds <- natural
425 return (Just (fromInteger reds)))
426 return (n, t)
428{- | Parses a postulate
431Postulate ::=
432 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
433 ;
435-}
436postulate :: SyntaxInfo -> IdrisParser PDecl
437postulate syn = do doc <- try $ do doc <- option noDocs docComment
438 pushIndent
439 reserved "postulate"
440 return doc
441 ist <- get
442 let initOpts = if default_total ist
443 then [TotalFn]
444 else []
445 opts <- fnOpts initOpts
446 acc <- optional accessibility
447 opts' <- fnOpts opts
448 n_in <- fnName
449 let n = expandNS syn n_in
450 lchar ':'
451 ty <- typeExpr (allowImp syn)
452 fc <- getFC
453 terminator
454 addAcc n acc
455 return (PPostulate (fst doc) syn fc opts' n ty)
456 <?> "postulate"
458{- | Parses a using declaration
461Using ::=
462 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
463 ;
465 -}
466using_ :: SyntaxInfo -> IdrisParser [PDecl]
467using_ syn =
468 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
469 openBlock
470 let uvars = using syn
471 ds <- many (decl (syn { using = uvars ++ ns }))
472 closeBlock
473 return (concat ds)
474 <?> "using declaration"
476{- | Parses a parameters declaration
479Params ::=
480 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
481 ;
483 -}
484params :: SyntaxInfo -> IdrisParser [PDecl]
485params syn =
486 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
487 openBlock
488 let pvars = syn_params syn
489 ds <- many (decl syn { syn_params = pvars ++ ns })
490 closeBlock
491 fc <- getFC
492 return [PParams fc ns (concat ds)]
493 <?> "parameters declaration"
495{- | Parses a mutual declaration (for mutually recursive functions)
498Mutual ::=
499 'mutual' OpenBlock Decl* CloseBlock
500 ;
502-}
503mutual :: SyntaxInfo -> IdrisParser [PDecl]
504mutual syn =
505 do reserved "mutual"
506 openBlock
507 let pvars = syn_params syn
508 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
509 closeBlock
510 fc <- getFC
511 return [PMutual fc (concat ds)]
512 <?> "mutual block"
514{-| Parses a namespace declaration
517Namespace ::=
518 'namespace' identifier OpenBlock Decl+ CloseBlock
519 ;
521-}
522namespace :: SyntaxInfo -> IdrisParser [PDecl]
523namespace syn =
524 do reserved "namespace"; n <- identifier;
525 openBlock
526 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
527 closeBlock
528 return [PNamespace n (concat ds)]
529 <?> "namespace declaration"
531{- | Parses a methods block (for instances)
534 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
536-}
537instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
538instanceBlock syn = do reserved "where"
539 openBlock
540 ds <- many (fnDecl syn)
541 closeBlock
542 return (concat ds)
543 <?> "instance block"
545{- | Parses a methods and instances block (for type classes)
548MethodOrInstance ::=
549 FnDecl
550 | Instance
551 ;
555ClassBlock ::=
556 'where' OpenBlock MethodOrInstance* CloseBlock
557 ;
559-}
560classBlock :: SyntaxInfo -> IdrisParser [PDecl]
561classBlock syn = do reserved "where"
562 openBlock
563 ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)
564 closeBlock
565 return (concat ds)
566 <?> "class block"
568{-| Parses a type class declaration
571ClassArgument ::=
572 Name
573 | '(' Name ':' Expr ')'
574 ;
578Class ::=
579 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
580 ;
582-}
583class_ :: SyntaxInfo -> IdrisParser [PDecl]
584class_ syn = do (doc, acc) <- try (do
585 doc <- option noDocs docComment
586 acc <- optional accessibility
587 return (doc, acc))
588 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName
589 let n = expandNS syn n_in
590 cs <- many carg
591 ds <- option [] (classBlock syn)
592 accData acc n (concatMap declared ds)
593 return [PClass (fst doc) syn fc cons n cs (snd doc) ds]
594 <?> "type-class declaration"
595 where
596 carg :: IdrisParser (Name, PTerm)
597 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
598 return (i, ty)
599 <|> do i <- name;
600 return (i, PType)
602{- | Parses a type class instance declaration
605 Instance ::=
606 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
607 ;
611InstanceName ::= '[' Name ']';
613-}
614instance_ :: SyntaxInfo -> IdrisParser [PDecl]
615instance_ syn = do reserved "instance"; fc <- getFC
616 en <- optional instanceName
617 cs <- constraintList syn
618 cn <- fnName
619 args <- many (simpleExpr syn)
620 let sc = PApp fc (PRef fc cn) (map pexp args)
621 let t = bindList (PPi constraint) (map (\x -> (sMN 0 "constraint", x)) cs) sc
622 ds <- option [] (instanceBlock syn)
623 return [PInstance syn fc cs cn args t en ds]
624 <?> "instance declaration"
625 where instanceName :: IdrisParser Name
626 instanceName = do lchar '['; n_in <- fnName; lchar ']'
627 let n = expandNS syn n_in
628 return n
629 <?> "instance name"
632{- | Parses a using declaration list
635UsingDeclList ::=
636 UsingDeclList'
637 | NameList TypeSig
638 ;
642UsingDeclList' ::=
643 UsingDecl
644 | UsingDecl ',' UsingDeclList'
645 ;
649NameList ::=
650 Name
651 | Name ',' NameList
652 ;
654-}
655usingDeclList :: SyntaxInfo -> IdrisParser [Using]
656usingDeclList syn
657 = try (sepBy1 (usingDecl syn) (lchar ','))
658 <|> do ns <- sepBy1 name (lchar ',')
659 lchar ':'
660 t <- typeExpr (disallowImp syn)
661 return (map (\x -> UImplicit x t) ns)
662 <?> "using declaration list"
664{- |Parses a using declaration
667UsingDecl ::=
668 FnName TypeSig
669 | FnName FnName+
670 ;
672-}
673usingDecl :: SyntaxInfo -> IdrisParser Using
674usingDecl syn = try (do x <- fnName
675 lchar ':'
676 t <- typeExpr (disallowImp syn)
677 return (UImplicit x t))
678 <|> do c <- fnName
679 xs <- some fnName
680 return (UConstraint c xs)
681 <?> "using declaration"
683{- | Parse a clause with patterns
686Pattern ::= Clause;
688-}
689pattern :: SyntaxInfo -> IdrisParser PDecl
690pattern syn = do fc <- getFC
691 clause <- clause syn
692 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
693 <?> "pattern"
695{- | Parse a constant applicative form declaration
698CAF ::= 'let' FnName '=' Expr Terminator;
700-}
701caf :: SyntaxInfo -> IdrisParser PDecl
702caf syn = do reserved "let"
703 n_in <- fnName; let n = expandNS syn n_in
704 lchar '='
705 t <- expr syn
706 terminator
707 fc <- getFC
708 return (PCAF fc n t)
709 <?> "constant applicative form declaration"
711{- | Parse an argument expression
714ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
716-}
717argExpr :: SyntaxInfo -> IdrisParser PTerm
718argExpr syn = let syn' = syn { inPattern = True } in
719 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
720 <?> "argument expression"
722{- | Parse a right hand side of a function
725RHS ::= '=' Expr
726 | '?=' RHSName? Expr
727 | 'impossible'
728 ;
732RHSName ::= '{' FnName '}';
734-}
735rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
736rhs syn n = do lchar '='; expr syn
737 <|> do symbol "?=";
738 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
739 return n)
740 r <- expr syn
741 return (addLet name r)
742 <|> do reserved "impossible"; return PImpossible
743 <?> "function right hand side"
744 where mkN :: Name -> Name
745 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
746 then sUN "infix_op_lemma_1"
747 else sUN (str x++"_lemma_1")
748 mkN (NS x n) = NS (mkN x) n
749 n' :: Name
750 n' = mkN n
751 addLet :: Name -> PTerm -> PTerm
752 addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)
753 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
754 where addLetC (l, r) = (l, addLet nm r)
755 addLet nm r = (PLet (sUN "value") Placeholder r (PMetavar nm))
757{- |Parses a function clause
760RHSOrWithBlock ::= RHS WhereOrTerminator
761 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
762 ;
766Clause ::= WExpr+ RHSOrWithBlock
767 | SimpleExpr '<==' FnName RHS WhereOrTerminator
768 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
769 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
770 ;
774ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
778WhereOrTerminator ::= WhereBlock | Terminator;
780-}
781clause :: SyntaxInfo -> IdrisParser PClause
782clause syn
783 = do wargs <- try (do pushIndent; some (wExpr syn))
784 fc <- getFC
785 ist <- get
786 n <- case lastParse ist of
787 Just t -> return t
788 Nothing -> fail "Invalid clause"
789 (do r <- rhs syn n
790 let ctxt = tt_ctxt ist
791 let wsyn = syn { syn_namespace = [] }
792 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
793 popIndent
794 return x,
795 do terminator
796 return ([], [])]
797 return $ PClauseR fc wargs r wheres) <|> (do
798 popIndent
799 reserved "with"
800 wval <- simpleExpr syn
801 openBlock
802 ds <- some $ fnDecl syn
803 let withs = concat ds
804 closeBlock
805 return $ PWithR fc wargs wval withs)
806 <|> do ty <- try (do pushIndent
807 ty <- simpleExpr syn
808 symbol "<=="
809 return ty)
810 fc <- getFC
811 n_in <- fnName; let n = expandNS syn n_in
812 r <- rhs syn n
813 ist <- get
814 let ctxt = tt_ctxt ist
815 let wsyn = syn { syn_namespace = [] }
816 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
817 popIndent
818 return x,
819 do terminator
820 return ([], [])]
821 let capp = PLet (sMN 0 "match")
822 ty
823 (PMatchApp fc n)
824 (PRef fc (sMN 0 "match"))
825 ist <- get
826 put (ist { lastParse = Just n })
827 return $ PClause fc n capp [] r wheres
828 <|> do (l, op) <- try (do
829 pushIndent
830 l <- argExpr syn
831 op <- operator
832 when (op == "=" || op == "?=" ) $
833 fail "infix clause definition with \"=\" and \"?=\" not supported "
834 return (l, op))
835 let n = expandNS syn (sUN op)
836 r <- argExpr syn
837 fc <- getFC
838 wargs <- many (wExpr syn)
839 (do rs <- rhs syn n
840 let wsyn = syn { syn_namespace = [] }
841 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
842 popIndent
843 return x,
844 do terminator
845 return ([], [])]
846 ist <- get
847 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
848 put (ist { lastParse = Just n })
849 return $ PClause fc n capp wargs rs wheres) <|> (do
850 popIndent
851 reserved "with"
852 wval <- bracketed syn
853 openBlock
854 ds <- some $ fnDecl syn
855 closeBlock
856 ist <- get
857 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
858 let withs = map (fillLHSD n capp wargs) $ concat ds
859 put (ist { lastParse = Just n })
860 return $ PWith fc n capp wargs wval withs)
861 <|> do pushIndent
862 n_in <- fnName; let n = expandNS syn n_in
863 cargs <- many (constraintArg syn)
864 fc <- getFC
865 args <- many (try (implicitArg (syn { inPattern = True } ))
866 <|> (fmap pexp (argExpr syn)))
867 wargs <- many (wExpr syn)
868 let capp = PApp fc (PRef fc n)
869 (cargs ++ args)
870 (do r <- rhs syn n
871 ist <- get
872 let ctxt = tt_ctxt ist
873 let wsyn = syn { syn_namespace = [] }
874 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
875 popIndent
876 return x,
877 do terminator
878 return ([], [])]
879 ist <- get
880 put (ist { lastParse = Just n })
881 return $ PClause fc n capp wargs r wheres) <|> (do
882 reserved "with"
883 ist <- get
884 put (ist { lastParse = Just n })
885 wval <- bracketed syn
886 openBlock
887 ds <- some $ fnDecl syn
888 let withs = map (fillLHSD n capp wargs) $ concat ds
889 closeBlock
890 popIndent
891 return $ PWith fc n capp wargs wval withs)
892 <?> "function clause"
893 where
894 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
895 fillLHS n capp owargs (PClauseR fc wargs v ws)
896 = PClause fc n capp (owargs ++ wargs) v ws
897 fillLHS n capp owargs (PWithR fc wargs v ws)
898 = PWith fc n capp (owargs ++ wargs) v
899 (map (fillLHSD n capp (owargs ++ wargs)) ws)
900 fillLHS _ _ _ c = c
902 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
903 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
904 fillLHSD n c a x = x
906{-| Parses with pattern
908@
909WExpr ::= '|' Expr';
911-}
912wExpr :: SyntaxInfo -> IdrisParser PTerm
913wExpr syn = do lchar '|'
914 expr' syn
915 <?> "with pattern"
917{- | Parses a where block
920WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
922-}
923whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
924whereBlock n syn
925 = do reserved "where"
926 ds <- indentedBlock1 (decl syn)
927 let dns = concatMap (concatMap declared) ds
928 return (concat ds, map (\x -> (x, decoration syn x)) dns)
929 <?> "where block"
931{- |Parses a code generation target language name
934Codegen ::= 'C'
935 | 'Java'
936 | 'JavaScript'
937 | 'Node'
938 | 'LLVM'
939 | 'Bytecode'
940 ;
942-}
943codegen_ :: IdrisParser Codegen
944codegen_ = do n <- identifier; return (Via (map toLower n))
945 <|> do reserved "Bytecode"; return Bytecode
946 <?> "code generation language"
948{- |Parses a compiler directive
950StringList ::=
951 String
952 | String ',' StringList
953 ;
957Directive ::= '%' Directive';
961Directive' ::= 'lib' CodeGen String_t
962 | 'link' CodeGen String_t
963 | 'flag' CodeGen String_t
964 | 'include' CodeGen String_t
965 | 'hide' Name
966 | 'freeze' Name
967 | 'access' Accessibility
968 | 'default' Totality
969 | 'logging' Natural
970 | 'dynamic' StringList
971 | 'name' Name NameList
972 | 'error_handlers' Name NameList
973 | 'language' 'TypeProviders'
974 | 'language' 'ErrorReflection'
975 ;
977-}
978directive :: SyntaxInfo -> IdrisParser [PDecl]
979directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
980 return [PDirective (do addLib cgn lib
981 addIBC (IBCLib cgn lib))]
982 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
983 return [PDirective (do dirs <- allImportDirs
984 o <- liftIO $ findInPath dirs obj
985 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
986 addObjectFile cgn o)]
987 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
988 flag <- stringLiteral
989 return [PDirective (do addIBC (IBCCGFlag cgn flag)
990 addFlag cgn flag)]
991 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
992 return [PDirective (do addHdr cgn hdr
993 addIBC (IBCHeader cgn hdr))]
994 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
995 return [PDirective (do setAccessibility n Hidden
996 addIBC (IBCAccess n Hidden))]
997 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
998 return [PDirective (do setAccessibility n Frozen
999 addIBC (IBCAccess n Frozen))]
1000 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1001 return [PDirective (do i <- get
1002 put(i { default_access = acc }))]
1003 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1004 i <- get
1005 put (i { default_total = tot } )
1006 return [PDirective (do i <- get
1007 put(i { default_total = tot }))]
1008 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
1009 return [PDirective (setLogLevel (fromInteger i))]
1010 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
1011 return [PDirective (do added <- addDyLib libs
1012 case added of
1013 Left lib -> addIBC (IBCDyLib (lib_name lib))
1014 Right msg ->
1015 fail $ msg)]
1016 <|> do try (lchar '%' *> reserved "name")
1017 ty <- fnName
1018 ns <- sepBy1 name (lchar ',')
1019 return [PDirective (do ty' <- disambiguate ty
1020 mapM_ (addNameHint ty') ns
1021 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1022 <|> do try (lchar '%' *> reserved "error_handlers")
1023 fn <- fnName
1024 arg <- fnName
1025 ns <- sepBy1 name (lchar ',')
1026 return [PDirective (do fn' <- disambiguate fn
1027 ns' <- mapM disambiguate ns
1028 addFunctionErrorHandlers fn' arg ns'
1029 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]
1030 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1031 return [PDirective (addLangExt ext)]
1032 <?> "directive"
1033 where disambiguate :: Name -> Idris Name
1034 disambiguate n = do i <- getIState
1035 case lookupCtxtName n (idris_implicits i) of
1036 [(n', _)] -> return n'
1037 [] -> throwError (NoSuchVariable n)
1038 more -> throwError (CantResolveAlts (map fst more))
1040pLangExt :: IdrisParser LanguageExt
1041pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1042 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1044{- | Parses a totality
1047Totality ::= 'partial' | 'total'
1051totality :: IdrisParser Bool
1052totality
1053 = do reserved "total"; return True
1054 <|> do reserved "partial"; return False
1056{- | Parses a type provider
1059Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1060ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1062 -}
1063provider :: SyntaxInfo -> IdrisParser [PDecl]
1064provider syn = do try (lchar '%' *> reserved "provide");
1065 provideTerm <|> providePostulate
1066 <?> "type provider"
1067 where provideTerm = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1068 fc <- getFC
1069 reserved "with"
1070 e <- expr syn <?> "provider expression"
1071 return [PProvider syn fc (ProvTerm t e) n]
1072 providePostulate = do reserved "postulate"
1073 n <- fnName
1074 fc <- getFC
1075 reserved "with"
1076 e <- expr syn <?> "provider expression"
1077 return [PProvider syn fc (ProvPostulate e) n]
1079{- | Parses a transform
1082Transform ::= '%' 'transform' Expr '==>' Expr
1085transform :: SyntaxInfo -> IdrisParser [PDecl]
1086transform syn = do try (lchar '%' *> reserved "transform")
1087 -- leave it unchecked, until we work out what this should
1088 -- actually mean...
1089-- safety <- option True (do reserved "unsafe"
1090-- return False)
1091 l <- expr syn
1092 fc <- getFC
1093 symbol "==>"
1094 r <- expr syn
1095 return [PTransform fc False l r]
1096 <?> "transform"
1099{- * Loading and parsing -}
1100{- | Parses an expression from input -}
1101parseExpr :: IState -> String -> Result PTerm
1102parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1104{- | Parses a constant form input -}
1105parseConst :: IState -> String -> Result Const
1106parseConst st = runparser constant st "(input)"
1108{- | Parses a tactic from input -}
1109parseTactic :: IState -> String -> Result PTactic
1110parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1112-- | Parse module header and imports
1113parseImports :: FilePath -> String -> Idris ([String], [(String, Maybe String, FC)], Maybe Delta)
1114parseImports fname input
1115 = do i <- getIState
1116 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1117 Failure err -> fail (show err)
1118 Success (x, i) -> do putIState i
1119 return x
1120 where imports :: IdrisParser (([String], [(String, Maybe String, FC)], Maybe Delta), IState)
1121 imports = do whiteSpace
1122 mname <- moduleHeader
1123 ps <- many import_
1124 mrk <- mark
1125 isEof <- lookAheadMatches eof
1126 let mrk' = if isEof
1127 then Nothing
1128 else Just mrk
1129 i <- get
1130 return ((mname, ps, mrk'), i)
1132-- | There should be a better way of doing this...
1133findFC :: Doc -> (FC, String)
1134findFC x = let s = show (plain x) in
1135 case span (/= ':') s of
1136 (failname, ':':rest) -> case span isDigit rest of
1137 (line, ':':rest') -> case span isDigit rest' of
1138 (col, ':':msg) -> let pos = (read line, read col) in
1139 (FC failname pos pos, msg)
1141-- | Check if the coloring matches the options and corrects if necessary
1142fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1143fixColour False doc = ANSI.plain doc
1144fixColour True doc = doc
1146-- | A program is a list of declarations, possibly with associated
1147-- documentation strings.
1148parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1149 Idris [PDecl]
1150parseProg syn fname input mrk
1151 = do i <- getIState
1152 case runparser mainProg i fname input of
1153 Failure doc -> do -- FIXME: Get error location from trifecta
1154 -- this can't be the solution!
1155 let (fc, msg) = findFC doc
1156 i <- getIState
1157 case idris_outputmode i of
1158 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1159 IdeSlave n h -> iWarn fc (P.text msg)
1160 putIState (i { errSpan = Just fc })
1161 return []
1162 Success (x, i) -> do putIState i
1163 reportParserWarnings
1164 return $ collect x
1165 where mainProg :: IdrisParser ([PDecl], IState)
1166 mainProg = case mrk of
1167 Nothing -> do i <- get; return ([], i)
1168 Just mrk -> do
1169 release mrk
1170 ds <- prog syn
1171 i' <- get
1172 return (ds, i')
1174{- | Load idris module and show error if something wrong happens -}
1175loadModule :: FilePath -> Idris String
1176loadModule f
1177 = idrisCatch (loadModule' f)
1178 (\e -> do setErrSpan (getErrSpan e)
1179 ist <- getIState
1180 iWarn (getErrSpan e) $ pprintErr ist e
1181 return "")
1183{- | Load idris module -}
1184loadModule' :: FilePath -> Idris String
1185loadModule' f
1186 = do i <- getIState
1187 let file = takeWhile (/= ' ') f
1188 ibcsd <- valIBCSubDir i
1189 ids <- allImportDirs
1190 fp <- findImport ids ibcsd file
1191 if file `elem` imported i
1192 then iLOG $ "Already read " ++ file
1193 else do putIState (i { imported = file : imported i })
1194 case fp of
1195 IDR fn -> loadSource False fn Nothing
1196 LIDR fn -> loadSource True fn Nothing
1197 IBC fn src ->
1198 idrisCatch (loadIBC fn)
1199 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1200 case src of
1201 IDR sfn -> loadSource False sfn Nothing
1202 LIDR sfn -> loadSource True sfn Nothing)
1203 let (dir, fh) = splitFileName file
1204 return (dropExtension fh)
1207{- | Load idris code from file -}
1208loadFromIFile :: IFileType -> Maybe Int -> Idris ()
1209loadFromIFile i@(IBC fn src) maxline
1210 = do iLOG $ "Skipping " ++ getSrcFile i
1211 idrisCatch (loadIBC fn)
1212 (\err -> ierror $ LoadingFailed fn err)
1213 where
1214 getSrcFile (IDR fn) = fn
1215 getSrcFile (LIDR fn) = fn
1216 getSrcFile (IBC f src) = getSrcFile src
1218loadFromIFile (IDR fn) maxline = loadSource' False fn maxline
1219loadFromIFile (LIDR fn) maxline = loadSource' True fn maxline
1221{-| Load idris source code and show error if something wrong happens -}
1222loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1223loadSource' lidr r maxline
1224 = idrisCatch (loadSource lidr r maxline)
1225 (\e -> do setErrSpan (getErrSpan e)
1226 ist <- getIState
1227 case e of
1228 At f e' -> iWarn f (pprintErr ist e')
1229 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1231{- | Load Idris source code-}
1232loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1233loadSource lidr f toline
1234 = do iLOG ("Reading " ++ f)
1235 i <- getIState
1236 let def_total = default_total i
1237 file_in <- runIO $ readFile f
1238 file <- if lidr then tclift $ unlit f file_in else return file_in
1239 (mname, imports_in, pos) <- parseImports f file
1240 ai <- getAutoImports
1241 let imports = map (\n -> (n, Just n, emptyFC)) ai ++ imports_in
1242 ids <- allImportDirs
1243 ibcsd <- valIBCSubDir i
1244 mapM_ (\f -> do fp <- findImport ids ibcsd f
1245 case fp of
1246 LIDR fn -> ifail $ "No ibc for " ++ f
1247 IDR fn -> ifail $ "No ibc for " ++ f
1248 IBC fn src -> loadIBC fn)
1249 [fn | (fn, _, _) <- imports]
1250 reportParserWarnings
1252 -- process and check module aliases
1253 let modAliases = M.fromList
1254 [(prep alias, prep realName) | (realName, Just alias, fc) <- imports]
1255 prep = map T.pack . reverse . Spl.splitOn "/"
1256 aliasNames = [(alias, fc) | (_, Just alias, fc) <- imports]
1257 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1258 case map head . filter ((/= 1) . length) $ histogram of
1259 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1260 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1262 i <- getIState
1263 putIState (i { default_access = Hidden, module_aliases = modAliases })
1264 clearIBC -- start a new .ibc file
1265 -- record package info in .ibc
1266 imps <- allImportDirs
1267 mapM_ addIBC (map IBCImportDir imps)
1268 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]
1269 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1270 maxline = toline }
1271 ds' <- parseProg syntax f file pos
1273 -- Parsing done, now process declarations
1275 let ds = namespaces mname ds'
1276 logLvl 3 (show $ showDecls verbosePPOption ds)
1277 i <- getIState
1278 logLvl 10 (show (toAlist (idris_implicits i)))
1279 logLvl 3 (show (idris_infixes i))
1280 -- Now add all the declarations to the context
1281 v <- verbose
1282 when v $ iputStrLn $ "Type checking " ++ f
1283 -- we totality check after every Mutual block, so if
1284 -- anything is a single definition, wrap it in a
1285 -- mutual block on its own
1286 elabDecls toplevel (map toMutual ds)
1287 i <- getIState
1288 -- simplify every definition do give the totality checker
1289 -- a better chance
1290 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1291 updateContext (simplifyCasedef n $ getErasureInfo i))
1292 (map snd (idris_totcheck i))
1293 -- build size change graph from simplified definitions
1294 iLOG "Totality checking"
1295 i <- getIState
1296 mapM_ buildSCG (idris_totcheck i)
1297 mapM_ checkDeclTotality (idris_totcheck i)
1299 -- Redo totality check for deferred names
1300 let deftots = idris_defertotcheck i
1301 iLOG $ "Totality checking " ++ show deftots
1302 mapM_ (\x -> do tot <- getTotality x
1303 case tot of
1304 Total _ -> setTotality x Unchecked
1305 _ -> return ()) (map snd deftots)
1306 mapM_ buildSCG deftots
1307 mapM_ checkDeclTotality deftots
1309 iLOG ("Finished " ++ f)
1310 ibcsd <- valIBCSubDir i
1311 iLOG "Universe checking"
1312 iucheck
1313 let ibc = ibcPathNoFallback ibcsd f
1314 i <- getIState
1315 addHides (hide_list i)
1317 -- Finally, write an ibc if checking was successful
1318 ok <- noErrors
1319 when ok $
1320 idrisCatch (do writeIBC f ibc; clearIBC)
1321 (\c -> return ()) -- failure is harmless
1322 i <- getIState
1323 putIState (i { default_total = def_total,
1324 hide_list = [] })
1325 return ()
1326 where
1327 namespaces :: [String] -> [PDecl] -> [PDecl]
1328 namespaces [] ds = ds
1329 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1331 toMutual :: PDecl -> PDecl
1332 toMutual m@(PMutual _ d) = m
1333 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1334 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1335 case x of
1336 PClauses _ _ _ _ -> r
1337 PClass _ _ _ _ _ _ _ _ -> r
1338 PInstance _ _ _ _ _ _ _ _ -> r
1339 _ -> x
1341{- | Adds names to hide list -}
1342addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1343addHides xs = do i <- getIState
1344 let defh = default_access i
1345 let (hs, as) = partition isNothing xs
1346 unless (null as) $
1347 mapM_ doHide
1348 (map (\ (n, _) -> (n, defh)) hs ++
1349 map (\ (n, Just a) -> (n, a)) as)
1350 where isNothing (_, Nothing) = True
1351 isNothing _ = False
1353 doHide (n, a) = do setAccessibility n a
1354 addIBC (IBCAccess n a)