git.iko.soy/Idris-dev
on c79fb21 help sign in
Idris-dev/src/Idris/Parser.hs
1353 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 reserved "C"; return ViaC
945 <|> do reserved "Java"; return ViaJava
946 <|> do reserved "JavaScript"; return ViaJavaScript
947 <|> do reserved "Node"; return ViaNode
948 <|> do reserved "LLVM"; return ViaLLVM
949 <|> do reserved "Bytecode"; return Bytecode
950 <?> "code generation language"
952{- |Parses a compiler directive
954StringList ::=
955 String
956 | String ',' StringList
957 ;
961Directive ::= '%' Directive';
965Directive' ::= 'lib' CodeGen String_t
966 | 'link' CodeGen String_t
967 | 'flag' CodeGen String_t
968 | 'include' CodeGen String_t
969 | 'hide' Name
970 | 'freeze' Name
971 | 'access' Accessibility
972 | 'default' Totality
973 | 'logging' Natural
974 | 'dynamic' StringList
975 | 'name' Name NameList
976 | 'error_handlers' Name NameList
977 | 'language' 'TypeProviders'
978 | 'language' 'ErrorReflection'
979 ;
981-}
982directive :: SyntaxInfo -> IdrisParser [PDecl]
983directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
984 return [PDirective (do addLib cgn lib
985 addIBC (IBCLib cgn lib))]
986 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
987 return [PDirective (do dirs <- allImportDirs
988 o <- liftIO $ findInPath dirs obj
989 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
990 addObjectFile cgn o)]
991 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
992 flag <- stringLiteral
993 return [PDirective (do addIBC (IBCCGFlag cgn flag)
994 addFlag cgn flag)]
995 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
996 return [PDirective (do addHdr cgn hdr
997 addIBC (IBCHeader cgn hdr))]
998 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
999 return [PDirective (do setAccessibility n Hidden
1000 addIBC (IBCAccess n Hidden))]
1001 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
1002 return [PDirective (do setAccessibility n Frozen
1003 addIBC (IBCAccess n Frozen))]
1004 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1005 return [PDirective (do i <- get
1006 put(i { default_access = acc }))]
1007 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1008 i <- get
1009 put (i { default_total = tot } )
1010 return [PDirective (do i <- get
1011 put(i { default_total = tot }))]
1012 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
1013 return [PDirective (setLogLevel (fromInteger i))]
1014 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
1015 return [PDirective (do added <- addDyLib libs
1016 case added of
1017 Left lib -> addIBC (IBCDyLib (lib_name lib))
1018 Right msg ->
1019 fail $ msg)]
1020 <|> do try (lchar '%' *> reserved "name")
1021 ty <- fnName
1022 ns <- sepBy1 name (lchar ',')
1023 return [PDirective (do ty' <- disambiguate ty
1024 mapM_ (addNameHint ty') ns
1025 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1026 <|> do try (lchar '%' *> reserved "error_handlers")
1027 fn <- fnName
1028 arg <- fnName
1029 ns <- sepBy1 name (lchar ',')
1030 return [PDirective (do fn' <- disambiguate fn
1031 ns' <- mapM disambiguate ns
1032 addFunctionErrorHandlers fn' arg ns'
1033 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]
1034 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1035 return [PDirective (addLangExt ext)]
1036 <?> "directive"
1037 where disambiguate :: Name -> Idris Name
1038 disambiguate n = do i <- getIState
1039 case lookupCtxtName n (idris_implicits i) of
1040 [(n', _)] -> return n'
1041 [] -> throwError (NoSuchVariable n)
1042 more -> throwError (CantResolveAlts (map fst more))
1044pLangExt :: IdrisParser LanguageExt
1045pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1046 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1048{- | Parses a totality
1051Totality ::= 'partial' | 'total'
1055totality :: IdrisParser Bool
1056totality
1057 = do reserved "total"; return True
1058 <|> do reserved "partial"; return False
1060{- | Parses a type provider
1063Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1064ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1066 -}
1067provider :: SyntaxInfo -> IdrisParser [PDecl]
1068provider syn = do try (lchar '%' *> reserved "provide");
1069 provideTerm <|> providePostulate
1070 <?> "type provider"
1071 where provideTerm = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1072 fc <- getFC
1073 reserved "with"
1074 e <- expr syn <?> "provider expression"
1075 return [PProvider syn fc (ProvTerm t e) n]
1076 providePostulate = do reserved "postulate"
1077 n <- fnName
1078 fc <- getFC
1079 reserved "with"
1080 e <- expr syn <?> "provider expression"
1081 return [PProvider syn fc (ProvPostulate e) n]
1083{- | Parses a transform
1086Transform ::= '%' 'transform' Expr '==>' Expr
1089transform :: SyntaxInfo -> IdrisParser [PDecl]
1090transform syn = do try (lchar '%' *> reserved "transform")
1091 -- leave it unchecked, until we work out what this should
1092 -- actually mean...
1093-- safety <- option True (do reserved "unsafe"
1094-- return False)
1095 l <- expr syn
1096 fc <- getFC
1097 symbol "==>"
1098 r <- expr syn
1099 return [PTransform fc False l r]
1100 <?> "transform"
1103{- * Loading and parsing -}
1104{- | Parses an expression from input -}
1105parseExpr :: IState -> String -> Result PTerm
1106parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1108{- | Parses a constant form input -}
1109parseConst :: IState -> String -> Result Const
1110parseConst st = runparser constant st "(input)"
1112{- | Parses a tactic from input -}
1113parseTactic :: IState -> String -> Result PTactic
1114parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1116-- | Parse module header and imports
1117parseImports :: FilePath -> String -> Idris ([String], [(String, Maybe String, FC)], Maybe Delta)
1118parseImports fname input
1119 = do i <- getIState
1120 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1121 Failure err -> fail (show err)
1122 Success (x, i) -> do putIState i
1123 return x
1124 where imports :: IdrisParser (([String], [(String, Maybe String, FC)], Maybe Delta), IState)
1125 imports = do whiteSpace
1126 mname <- moduleHeader
1127 ps <- many import_
1128 mrk <- mark
1129 isEof <- lookAheadMatches eof
1130 let mrk' = if isEof
1131 then Nothing
1132 else Just mrk
1133 i <- get
1134 return ((mname, ps, mrk'), i)
1136-- | There should be a better way of doing this...
1137findFC :: Doc -> (FC, String)
1138findFC x = let s = show (plain x) in
1139 case span (/= ':') s of
1140 (failname, ':':rest) -> case span isDigit rest of
1141 (line, ':':rest') -> case span isDigit rest' of
1142 (col, ':':msg) -> let pos = (read line, read col) in
1143 (FC failname pos pos, msg)
1145-- | Check if the coloring matches the options and corrects if necessary
1146fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1147fixColour False doc = ANSI.plain doc
1148fixColour True doc = doc
1150-- | A program is a list of declarations, possibly with associated
1151-- documentation strings.
1152parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1153 Idris [PDecl]
1154parseProg syn fname input mrk
1155 = do i <- getIState
1156 case runparser mainProg i fname input of
1157 Failure doc -> do -- FIXME: Get error location from trifecta
1158 -- this can't be the solution!
1159 let (fc, msg) = findFC doc
1160 i <- getIState
1161 case idris_outputmode i of
1162 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)
1163 IdeSlave n h -> iWarn fc (P.text msg)
1164 putIState (i { errSpan = Just fc })
1165 return []
1166 Success (x, i) -> do putIState i
1167 reportParserWarnings
1168 return $ collect x
1169 where mainProg :: IdrisParser ([PDecl], IState)
1170 mainProg = case mrk of
1171 Nothing -> do i <- get; return ([], i)
1172 Just mrk -> do
1173 release mrk
1174 ds <- prog syn
1175 i' <- get
1176 return (ds, i')
1178{- | Load idris module and show error if something wrong happens -}
1179loadModule :: FilePath -> Idris String
1180loadModule f
1181 = idrisCatch (loadModule' f)
1182 (\e -> do setErrSpan (getErrSpan e)
1183 ist <- getIState
1184 iWarn (getErrSpan e) $ pprintErr ist e
1185 return "")
1187{- | Load idris module -}
1188loadModule' :: FilePath -> Idris String
1189loadModule' f
1190 = do i <- getIState
1191 let file = takeWhile (/= ' ') f
1192 ibcsd <- valIBCSubDir i
1193 ids <- allImportDirs
1194 fp <- findImport ids ibcsd file
1195 if file `elem` imported i
1196 then iLOG $ "Already read " ++ file
1197 else do putIState (i { imported = file : imported i })
1198 case fp of
1199 IDR fn -> loadSource False fn Nothing
1200 LIDR fn -> loadSource True fn Nothing
1201 IBC fn src ->
1202 idrisCatch (loadIBC fn)
1203 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1204 case src of
1205 IDR sfn -> loadSource False sfn Nothing
1206 LIDR sfn -> loadSource True sfn Nothing)
1207 let (dir, fh) = splitFileName file
1208 return (dropExtension fh)
1211{- | Load idris code from file -}
1212loadFromIFile :: IFileType -> Maybe Int -> Idris ()
1213loadFromIFile i@(IBC fn src) maxline
1214 = do iLOG $ "Skipping " ++ getSrcFile i
1215 idrisCatch (loadIBC fn)
1216 (\err -> ierror $ LoadingFailed fn err)
1217 where
1218 getSrcFile (IDR fn) = fn
1219 getSrcFile (LIDR fn) = fn
1220 getSrcFile (IBC f src) = getSrcFile src
1222loadFromIFile (IDR fn) maxline = loadSource' False fn maxline
1223loadFromIFile (LIDR fn) maxline = loadSource' True fn maxline
1225{-| Load idris source code and show error if something wrong happens -}
1226loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
1227loadSource' lidr r maxline
1228 = idrisCatch (loadSource lidr r maxline)
1229 (\e -> do setErrSpan (getErrSpan e)
1230 ist <- getIState
1231 case e of
1232 At f e' -> iWarn f (pprintErr ist e')
1233 _ -> iWarn (getErrSpan e) (pprintErr ist e))
1235{- | Load Idris source code-}
1236loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
1237loadSource lidr f toline
1238 = do iLOG ("Reading " ++ f)
1239 i <- getIState
1240 let def_total = default_total i
1241 file_in <- runIO $ readFile f
1242 file <- if lidr then tclift $ unlit f file_in else return file_in
1243 (mname, imports, pos) <- parseImports f file
1244 ids <- allImportDirs
1245 ibcsd <- valIBCSubDir i
1246 mapM_ (\f -> do fp <- findImport ids ibcsd f
1247 case fp of
1248 LIDR fn -> ifail $ "No ibc for " ++ f
1249 IDR fn -> ifail $ "No ibc for " ++ f
1250 IBC fn src -> loadIBC fn)
1251 [fn | (fn, _, _) <- imports]
1252 reportParserWarnings
1254 -- process and check module aliases
1255 let modAliases = M.fromList
1256 [(prep alias, prep realName) | (realName, Just alias, fc) <- imports]
1257 prep = map T.pack . reverse . Spl.splitOn "/"
1258 aliasNames = [(alias, fc) | (_, Just alias, fc) <- imports]
1259 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1260 case map head . filter ((/= 1) . length) $ histogram of
1261 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1262 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1264 i <- getIState
1265 putIState (i { default_access = Hidden, module_aliases = modAliases })
1266 clearIBC -- start a new .ibc file
1267 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]
1268 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1269 maxline = toline }
1270 ds' <- parseProg syntax f file pos
1272 -- Parsing done, now process declarations
1274 let ds = namespaces mname ds'
1275 logLvl 3 (show $ showDecls verbosePPOption ds)
1276 i <- getIState
1277 logLvl 10 (show (toAlist (idris_implicits i)))
1278 logLvl 3 (show (idris_infixes i))
1279 -- Now add all the declarations to the context
1280 v <- verbose
1281 when v $ iputStrLn $ "Type checking " ++ f
1282 -- we totality check after every Mutual block, so if
1283 -- anything is a single definition, wrap it in a
1284 -- mutual block on its own
1285 elabDecls toplevel (map toMutual ds)
1286 i <- getIState
1287 -- simplify every definition do give the totality checker
1288 -- a better chance
1289 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1290 updateContext (simplifyCasedef n $ getErasureInfo i))
1291 (map snd (idris_totcheck i))
1292 -- build size change graph from simplified definitions
1293 iLOG "Totality checking"
1294 i <- getIState
1295 mapM_ buildSCG (idris_totcheck i)
1296 mapM_ checkDeclTotality (idris_totcheck i)
1298 -- Redo totality check for deferred names
1299 let deftots = idris_defertotcheck i
1300 iLOG $ "Totality checking " ++ show deftots
1301 mapM_ (\x -> do tot <- getTotality x
1302 case tot of
1303 Total _ -> setTotality x Unchecked
1304 _ -> return ()) (map snd deftots)
1305 mapM_ buildSCG deftots
1306 mapM_ checkDeclTotality deftots
1308 iLOG ("Finished " ++ f)
1309 ibcsd <- valIBCSubDir i
1310 iLOG "Universe checking"
1311 iucheck
1312 let ibc = ibcPathNoFallback ibcsd f
1313 i <- getIState
1314 addHides (hide_list i)
1316 -- Finally, write an ibc if checking was successful
1317 ok <- noErrors
1318 when ok $
1319 idrisCatch (do writeIBC f ibc; clearIBC)
1320 (\c -> return ()) -- failure is harmless
1321 i <- getIState
1322 putIState (i { default_total = def_total,
1323 hide_list = [] })
1324 return ()
1325 where
1326 namespaces :: [String] -> [PDecl] -> [PDecl]
1327 namespaces [] ds = ds
1328 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1330 toMutual :: PDecl -> PDecl
1331 toMutual m@(PMutual _ d) = m
1332 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1333 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1334 case x of
1335 PClauses _ _ _ _ -> r
1336 PClass _ _ _ _ _ _ _ _ -> r
1337 PInstance _ _ _ _ _ _ _ _ -> r
1338 _ -> x
1340{- | Adds names to hide list -}
1341addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1342addHides xs = do i <- getIState
1343 let defh = default_access i
1344 let (hs, as) = partition isNothing xs
1345 unless (null as) $
1346 mapM_ doHide
1347 (map (\ (n, _) -> (n, defh)) hs ++
1348 map (\ (n, Just a) -> (n, a)) as)
1349 where isNothing (_, Nothing) = True
1350 isNothing _ = False
1352 doHide (n, a) = do setAccessibility n a
1353 addIBC (IBCAccess n a)