git.iko.soy/Idris-dev
on db306ca help sign in
Idris-dev/src/Idris/Parser.hs
1314 lines 46 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)
21import Idris.AbsSyntax
22import Idris.DSL
23import Idris.Imports
24import Idris.Delaborate
25import Idris.Error
26import Idris.ElabDecls
27import Idris.ElabTerm hiding (namespace, params)
28import Idris.Coverage
29import Idris.IBC
30import Idris.Unlit
31import Idris.Providers
33import Idris.ParseHelpers
34import Idris.ParseOps
35import Idris.ParseExpr
36import Idris.ParseData
38import Idris.Docstrings
40import Paths_idris
42import Util.DynamicLinker
43import qualified Util.Pretty as P
45import Idris.Core.TT
46import Idris.Core.Evaluate
48import Control.Applicative
49import Control.Monad
50import Control.Monad.Error (throwError, catchError)
51import Control.Monad.State.Strict
53import Data.Function
54import Data.Maybe
55import qualified Data.List.Split as Spl
56import Data.List
57import Data.Monoid
58import Data.Char
59import Data.Ord
60import qualified Data.Map as M
61import qualified Data.HashSet as HS
62import qualified Data.Text as T
63import qualified Data.ByteString.UTF8 as UTF8
64import qualified Data.Set as S
66import Debug.Trace
68import System.FilePath
69import System.IO
71{-
73 grammar shortcut notation:
74 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)
75 RULE? = optional rule (i.e. RULE or nothing)
76 RULE* = repeated rule (i.e. RULE zero or more times)
77 RULE+ = repeated rule with at least one match (i.e. RULE one or more times)
78 RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)
79 RULE{n} = rule repeated n times
81-}
83{- * Main grammar -}
85{- | Parses module definition
88 ModuleHeader ::= 'module' Identifier_t ';'?;
90-}
91moduleHeader :: IdrisParser [String]
92moduleHeader = try (do noDocCommentHere "Modules cannot have documentation comments"
93 reserved "module"
94 i <- identifier
95 option ';' (lchar ';')
96 return (moduleName i))
97 <|> try (do lchar '%'; reserved "unqualified"
98 return [])
99 <|> return (moduleName "Main")
100 where moduleName x = case span (/='.') x of
101 (x, "") -> [x]
102 (x, '.':y) -> x : moduleName y
104{- | Parses an import statement
107 Import ::= 'import' Identifier_t ';'?;
109 -}
110import_ :: IdrisParser (String, Maybe String, FC)
111import_ = do fc <- getFC
112 reserved "import"
113 id <- identifier
114 newName <- optional (reserved "as" *> identifier)
115 option ';' (lchar ';')
116 return (toPath id, toPath <$> newName, fc)
117 <?> "import statement"
118 where toPath = foldl1' (</>) . Spl.splitOn "."
120{- | Parses program source
123 Prog ::= Decl* EOF;
125 -}
126prog :: SyntaxInfo -> IdrisParser [PDecl]
127prog syn = do whiteSpace
128 decls <- many (decl syn)
129 notOpenBraces
130 eof
131 let c = (concat decls)
132 return c
134{-| Parses a top-level declaration
137Decl ::=
138 Decl'
139 | Using
140 | Params
141 | Mutual
142 | Namespace
143 | Class
144 | Instance
145 | DSL
146 | Directive
147 | Provider
148 | Transform
149 | Import!
150 ;
152-}
153decl :: SyntaxInfo -> IdrisParser [PDecl]
154decl syn = do notEndBlock
155 declBody
156 where declBody :: IdrisParser [PDecl]
157 declBody = declBody'
158 <|> using_ syn
159 <|> params syn
160 <|> mutual syn
161 <|> namespace syn
162 <|> class_ syn
163 <|> instance_ syn
164 <|> do d <- dsl syn; return [d]
165 <|> directive syn
166 <|> provider syn
167 <|> transform syn
168 <|> do import_; fail "imports must be at top of file"
169 <?> "declaration"
170 declBody' :: IdrisParser [PDecl]
171 declBody' = do d <- decl' syn
172 i <- get
173 let d' = fmap (debindApp syn . (desugar syn i)) d
174 return [d']
176{- | Parses a top-level declaration with possible syntax sugar
179Decl' ::=
180 Fixity
181 | FunDecl'
182 | Data
183 | Record
184 | SyntaxDecl
185 ;
187-}
188decl' :: SyntaxInfo -> IdrisParser PDecl
189decl' syn = fixity
190 <|> syntaxDecl syn
191 <|> fnDecl' syn
192 <|> data_ syn
193 <|> record syn
194 <?> "declaration"
196{- | Parses a syntax extension declaration (and adds the rule to parser state)
199 SyntaxDecl ::= SyntaxRule;
201-}
202syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
203syntaxDecl syn = do s <- syntaxRule syn
204 i <- get
205 let rs = syntax_rules i
206 let ns = syntax_keywords i
207 let ibc = ibc_write i
208 let ks = map show (names s)
209 put (i { syntax_rules = s : rs,
210 syntax_keywords = ks ++ ns,
211 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc })
212 fc <- getFC
213 return (PSyntax fc s)
214 where names (Rule syms _ _) = mapMaybe ename syms
215 ename (Keyword n) = Just n
216 ename _ = Nothing
218{- | Parses a syntax extension declaration
221SyntaxRuleOpts ::= 'term' | 'pattern';
225SyntaxRule ::=
226 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
230SyntaxSym ::= '[' Name_t ']'
231 | '{' Name_t '}'
232 | Name_t
233 | StringLiteral_t
234 ;
236-}
237syntaxRule :: SyntaxInfo -> IdrisParser Syntax
238syntaxRule syn
239 = do sty <- try (do
240 pushIndent
241 sty <- option AnySyntax (do reserved "term"; return TermSyntax
242 <|> do reserved "pattern"; return PatternSyntax)
243 reserved "syntax"
244 return sty)
245 syms <- some syntaxSym
246 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
247 let ns = mapMaybe getName syms
248 when (length ns /= length (nub ns))
249 $ unexpected "repeated variable in syntax rule"
250 lchar '='
251 tm <- typeExpr (allowImp syn)
252 terminator
253 return (Rule (mkSimple syms) tm sty)
254 where
255 isExpr (Expr _) = True
256 isExpr _ = False
257 getName (Expr n) = Just n
258 getName _ = Nothing
259 -- Can't parse two full expressions (i.e. expressions with application) in a row
260 -- so change them both to a simple expression
261 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
262 mkSimple xs = mkSimple' xs
264 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
265 mkSimple es
266 mkSimple' (e : es) = e : mkSimple' es
267 mkSimple' [] = []
270{- | Parses a syntax symbol (either binding variable, keyword or expression)
273SyntaxSym ::= '[' Name_t ']'
274 | '{' Name_t '}'
275 | Name_t
276 | StringLiteral_t
277 ;
279 -}
280syntaxSym :: IdrisParser SSymbol
281syntaxSym = try (do lchar '['; n <- name; lchar ']'
282 return (Expr n))
283 <|> try (do lchar '{'; n <- name; lchar '}'
284 return (Binding n))
285 <|> do n <- iName []
286 return (Keyword n)
287 <|> do sym <- stringLiteral
288 return (Symbol sym)
289 <?> "syntax symbol"
291{- | Parses a function declaration with possible syntax sugar
294 FunDecl ::= FunDecl';
296-}
297fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
298fnDecl syn = try (do notEndBlock
299 d <- fnDecl' syn
300 i <- get
301 let d' = fmap (desugar syn i) d
302 return [d']) <?> "function declaration"
304{-| Parses a function declaration
307 FunDecl' ::=
308 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
309 | Postulate
310 | Pattern
311 | CAF
312 ;
314-}
315fnDecl' :: SyntaxInfo -> IdrisParser PDecl
316fnDecl' syn = checkFixity $
317 do (doc, fc, opts', n, acc) <- try (do
318 pushIndent
319 ist <- get
320 doc <- option noDocs docComment
321 ist <- get
322 let initOpts = if default_total ist
323 then [TotalFn]
324 else []
325 opts <- fnOpts initOpts
326 acc <- optional accessibility
327 opts' <- fnOpts opts
328 n_in <- fnName
329 let n = expandNS syn n_in
330 fc <- getFC
331 lchar ':'
332 return (doc, fc, opts', n, acc))
333 ty <- typeExpr (allowImp syn)
334 terminator
335 addAcc n acc
336 return (PTy (fst doc) (snd doc) syn fc opts' n ty)
337 <|> postulate syn
338 <|> caf syn
339 <|> pattern syn
340 <?> "function declaration"
341 where checkFixity :: IdrisParser PDecl -> IdrisParser PDecl
342 checkFixity p = do decl <- p
343 case getName decl of
344 Nothing -> return decl
345 Just n -> do fOk <- fixityOK n
346 unless fOk . fail $
347 "Missing fixity declaration for " ++ show n
348 return decl
349 getName (PTy _ _ _ _ _ n _) = Just n
350 getName _ = Nothing
351 fixityOK (NS n _) = fixityOK n
352 fixityOK (UN n) | all (flip elem opChars) (str n) =
353 do fixities <- fmap idris_infixes get
354 return . elem (str n) . map (\ (Fix _ op) -> op) $ fixities
355 | otherwise = return True
356 fixityOK _ = return True
358{-| Parses function options given initial options
361FnOpts ::= 'total'
362 | 'partial'
363 | 'implicit'
364 | '%' 'assert_total'
365 | '%' 'error_handler'
366 | '%' 'reflection'
367 | '%' 'specialise' '[' NameTimesList? ']'
368 ;
372NameTimes ::= FnName Natural?;
376NameTimesList ::=
377 NameTimes
378 | NameTimes ',' NameTimesList
379 ;
381-}
382-- FIXME: Check compatability for function options (i.e. partal/total)
383fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
384fnOpts opts
385 = do reserved "total"; fnOpts (TotalFn : opts)
386 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
387 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;
388 fnOpts (CExport c : opts)
389 <|> do try (lchar '%' *> reserved "assert_total");
390 fnOpts (AssertTotal : opts)
391 <|> do try (lchar '%' *> reserved "error_handler");
392 fnOpts (ErrorHandler : opts)
393 <|> do try (lchar '%' *> reserved "error_reverse");
394 fnOpts (ErrorReverse : opts)
395 <|> do try (lchar '%' *> reserved "reflection");
396 fnOpts (Reflection : opts)
397 <|> do lchar '%'; reserved "specialise";
398 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
399 fnOpts (Specialise ns : opts)
400 <|> do reserved "implicit"; fnOpts (Implicit : opts)
401 <|> return opts
402 <?> "function modifier"
403 where nameTimes :: IdrisParser (Name, Maybe Int)
404 nameTimes = do n <- fnName
405 t <- option Nothing (do reds <- natural
406 return (Just (fromInteger reds)))
407 return (n, t)
409{- | Parses a postulate
412Postulate ::=
413 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
414 ;
416-}
417postulate :: SyntaxInfo -> IdrisParser PDecl
418postulate syn = do doc <- try $ do doc <- option noDocs docComment
419 pushIndent
420 reserved "postulate"
421 return doc
422 ist <- get
423 let initOpts = if default_total ist
424 then [TotalFn]
425 else []
426 opts <- fnOpts initOpts
427 acc <- optional accessibility
428 opts' <- fnOpts opts
429 n_in <- fnName
430 let n = expandNS syn n_in
431 lchar ':'
432 ty <- typeExpr (allowImp syn)
433 fc <- getFC
434 terminator
435 addAcc n acc
436 return (PPostulate (fst doc) syn fc opts' n ty)
437 <?> "postulate"
439{- | Parses a using declaration
442Using ::=
443 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
444 ;
446 -}
447using_ :: SyntaxInfo -> IdrisParser [PDecl]
448using_ syn =
449 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
450 openBlock
451 let uvars = using syn
452 ds <- many (decl (syn { using = uvars ++ ns }))
453 closeBlock
454 return (concat ds)
455 <?> "using declaration"
457{- | Parses a parameters declaration
460Params ::=
461 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
462 ;
464 -}
465params :: SyntaxInfo -> IdrisParser [PDecl]
466params syn =
467 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
468 openBlock
469 let pvars = syn_params syn
470 ds <- many (decl syn { syn_params = pvars ++ ns })
471 closeBlock
472 fc <- getFC
473 return [PParams fc ns (concat ds)]
474 <?> "parameters declaration"
476{- | Parses a mutual declaration (for mutually recursive functions)
479Mutual ::=
480 'mutual' OpenBlock Decl* CloseBlock
481 ;
483-}
484mutual :: SyntaxInfo -> IdrisParser [PDecl]
485mutual syn =
486 do reserved "mutual"
487 openBlock
488 let pvars = syn_params syn
489 ds <- many (decl syn)
490 closeBlock
491 fc <- getFC
492 return [PMutual fc (concat ds)]
493 <?> "mutual block"
495{-| Parses a namespace declaration
498Namespace ::=
499 'namespace' identifier OpenBlock Decl+ CloseBlock
500 ;
502-}
503namespace :: SyntaxInfo -> IdrisParser [PDecl]
504namespace syn =
505 do reserved "namespace"; n <- identifier;
506 openBlock
507 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
508 closeBlock
509 return [PNamespace n (concat ds)]
510 <?> "namespace declaration"
512{- | Parses a methods block (for instances)
515 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
517-}
518instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
519instanceBlock syn = do reserved "where"
520 openBlock
521 ds <- many (fnDecl syn)
522 closeBlock
523 return (concat ds)
524 <?> "instance block"
526{- | Parses a methods and instances block (for type classes)
529MethodOrInstance ::=
530 FnDecl
531 | Instance
532 ;
536ClassBlock ::=
537 'where' OpenBlock MethodOrInstance* CloseBlock
538 ;
540-}
541classBlock :: SyntaxInfo -> IdrisParser [PDecl]
542classBlock syn = do reserved "where"
543 openBlock
544 ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)
545 closeBlock
546 return (concat ds)
547 <?> "class block"
549{-| Parses a type class declaration
552ClassArgument ::=
553 Name
554 | '(' Name ':' Expr ')'
555 ;
559Class ::=
560 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
561 ;
563-}
564class_ :: SyntaxInfo -> IdrisParser [PDecl]
565class_ syn = do (doc, acc) <- try (do
566 doc <- option noDocs docComment
567 acc <- optional accessibility
568 return (doc, acc))
569 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName
570 let n = expandNS syn n_in
571 cs <- many carg
572 ds <- option [] (classBlock syn)
573 accData acc n (concatMap declared ds)
574 return [PClass (fst doc) syn fc cons n cs ds]
575 <?> "type-class declaration"
576 where
577 carg :: IdrisParser (Name, PTerm)
578 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
579 return (i, ty)
580 <|> do i <- name;
581 return (i, PType)
583{- | Parses a type class instance declaration
586 Instance ::=
587 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
588 ;
592InstanceName ::= '[' Name ']';
594-}
595instance_ :: SyntaxInfo -> IdrisParser [PDecl]
596instance_ syn = do reserved "instance"; fc <- getFC
597 en <- optional instanceName
598 cs <- constraintList syn
599 cn <- fnName
600 args <- many (simpleExpr syn)
601 let sc = PApp fc (PRef fc cn) (map pexp args)
602 let t = bindList (PPi constraint) (map (\x -> (sMN 0 "constraint", x)) cs) sc
603 ds <- option [] (instanceBlock syn)
604 return [PInstance syn fc cs cn args t en ds]
605 <?> "instance declaration"
606 where instanceName :: IdrisParser Name
607 instanceName = do lchar '['; n_in <- fnName; lchar ']'
608 let n = expandNS syn n_in
609 return n
610 <?> "instance name"
613{- | Parses a using declaration list
616UsingDeclList ::=
617 UsingDeclList'
618 | NameList TypeSig
619 ;
623UsingDeclList' ::=
624 UsingDecl
625 | UsingDecl ',' UsingDeclList'
626 ;
630NameList ::=
631 Name
632 | Name ',' NameList
633 ;
635-}
636usingDeclList :: SyntaxInfo -> IdrisParser [Using]
637usingDeclList syn
638 = try (sepBy1 (usingDecl syn) (lchar ','))
639 <|> do ns <- sepBy1 name (lchar ',')
640 lchar ':'
641 t <- typeExpr (disallowImp syn)
642 return (map (\x -> UImplicit x t) ns)
643 <?> "using declaration list"
645{- |Parses a using declaration
648UsingDecl ::=
649 FnName TypeSig
650 | FnName FnName+
651 ;
653-}
654usingDecl :: SyntaxInfo -> IdrisParser Using
655usingDecl syn = try (do x <- fnName
656 lchar ':'
657 t <- typeExpr (disallowImp syn)
658 return (UImplicit x t))
659 <|> do c <- fnName
660 xs <- some fnName
661 return (UConstraint c xs)
662 <?> "using declaration"
664{- | Parse a clause with patterns
667Pattern ::= Clause;
669-}
670pattern :: SyntaxInfo -> IdrisParser PDecl
671pattern syn = do fc <- getFC
672 clause <- clause syn
673 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
674 <?> "pattern"
676{- | Parse a constant applicative form declaration
679CAF ::= 'let' FnName '=' Expr Terminator;
681-}
682caf :: SyntaxInfo -> IdrisParser PDecl
683caf syn = do reserved "let"
684 n_in <- fnName; let n = expandNS syn n_in
685 lchar '='
686 t <- expr syn
687 terminator
688 fc <- getFC
689 return (PCAF fc n t)
690 <?> "constant applicative form declaration"
692{- | Parse an argument expression
695ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
697-}
698argExpr :: SyntaxInfo -> IdrisParser PTerm
699argExpr syn = let syn' = syn { inPattern = True } in
700 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
701 <?> "argument expression"
703{- | Parse a right hand side of a function
706RHS ::= '=' Expr
707 | '?=' RHSName? Expr
708 | 'impossible'
709 ;
713RHSName ::= '{' FnName '}';
715-}
716rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
717rhs syn n = do lchar '='; expr syn
718 <|> do symbol "?=";
719 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
720 return n)
721 r <- expr syn
722 return (addLet name r)
723 <|> do reserved "impossible"; return PImpossible
724 <?> "function right hand side"
725 where mkN :: Name -> Name
726 mkN (UN x) = sUN (str x++"_lemma_1")
727 mkN (NS x n) = NS (mkN x) n
728 n' :: Name
729 n' = mkN n
730 addLet :: Name -> PTerm -> PTerm
731 addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)
732 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
733 where addLetC (l, r) = (l, addLet nm r)
734 addLet nm r = (PLet (sUN "value") Placeholder r (PMetavar nm))
736{- |Parses a function clause
739RHSOrWithBlock ::= RHS WhereOrTerminator
740 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
741 ;
745Clause ::= WExpr+ RHSOrWithBlock
746 | SimpleExpr '<==' FnName RHS WhereOrTerminator
747 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
748 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
749 ;
753ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
757WhereOrTerminator ::= WhereBlock | Terminator;
759-}
760clause :: SyntaxInfo -> IdrisParser PClause
761clause syn
762 = do wargs <- try (do pushIndent; some (wExpr syn))
763 fc <- getFC
764 ist <- get
765 n <- case lastParse ist of
766 Just t -> return t
767 Nothing -> fail "Invalid clause"
768 (do r <- rhs syn n
769 let ctxt = tt_ctxt ist
770 let wsyn = syn { syn_namespace = [] }
771 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
772 popIndent
773 return x,
774 do terminator
775 return ([], [])]
776 return $ PClauseR fc wargs r wheres) <|> (do
777 popIndent
778 reserved "with"
779 wval <- simpleExpr syn
780 openBlock
781 ds <- some $ fnDecl syn
782 let withs = concat ds
783 closeBlock
784 return $ PWithR fc wargs wval withs)
785 <|> do ty <- try (do pushIndent
786 ty <- simpleExpr syn
787 symbol "<=="
788 return ty)
789 fc <- getFC
790 n_in <- fnName; let n = expandNS syn n_in
791 r <- rhs syn n
792 ist <- get
793 let ctxt = tt_ctxt ist
794 let wsyn = syn { syn_namespace = [] }
795 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
796 popIndent
797 return x,
798 do terminator
799 return ([], [])]
800 let capp = PLet (sMN 0 "match")
801 ty
802 (PMatchApp fc n)
803 (PRef fc (sMN 0 "match"))
804 ist <- get
805 put (ist { lastParse = Just n })
806 return $ PClause fc n capp [] r wheres
807 <|> do (l, op) <- try (do
808 pushIndent
809 l <- argExpr syn
810 op <- operator
811 when (op == "=" || op == "?=" ) $
812 fail "infix clause definition with \"=\" and \"?=\" not supported "
813 return (l, op))
814 let n = expandNS syn (sUN op)
815 r <- argExpr syn
816 fc <- getFC
817 wargs <- many (wExpr syn)
818 (do rs <- rhs syn n
819 let wsyn = syn { syn_namespace = [] }
820 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
821 popIndent
822 return x,
823 do terminator
824 return ([], [])]
825 ist <- get
826 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
827 put (ist { lastParse = Just n })
828 return $ PClause fc n capp wargs rs wheres) <|> (do
829 popIndent
830 reserved "with"
831 lchar '(' <?> "parenthesized expression"
832 wval <- bracketed syn
833 openBlock
834 ds <- some $ fnDecl syn
835 closeBlock
836 ist <- get
837 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
838 let withs = map (fillLHSD n capp wargs) $ concat ds
839 put (ist { lastParse = Just n })
840 return $ PWith fc n capp wargs wval withs)
841 <|> do pushIndent
842 n_in <- fnName; let n = expandNS syn n_in
843 cargs <- many (constraintArg syn)
844 fc <- getFC
845 args <- many (try (implicitArg (syn { inPattern = True } ))
846 <|> (fmap pexp (argExpr syn)))
847 wargs <- many (wExpr syn)
848 let capp = PApp fc (PRef fc n)
849 (cargs ++ args)
850 (do r <- rhs syn n
851 ist <- get
852 let ctxt = tt_ctxt ist
853 let wsyn = syn { syn_namespace = [] }
854 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
855 popIndent
856 return x,
857 do terminator
858 return ([], [])]
859 ist <- get
860 put (ist { lastParse = Just n })
861 return $ PClause fc n capp wargs r wheres) <|> (do
862 reserved "with"
863 ist <- get
864 put (ist { lastParse = Just n })
865 lchar '(' <?> "parenthesized expression"
866 wval <- bracketed syn
867 openBlock
868 ds <- some $ fnDecl syn
869 let withs = map (fillLHSD n capp wargs) $ concat ds
870 closeBlock
871 popIndent
872 return $ PWith fc n capp wargs wval withs)
873 <?> "function clause"
874 where
875 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
876 fillLHS n capp owargs (PClauseR fc wargs v ws)
877 = PClause fc n capp (owargs ++ wargs) v ws
878 fillLHS n capp owargs (PWithR fc wargs v ws)
879 = PWith fc n capp (owargs ++ wargs) v
880 (map (fillLHSD n capp (owargs ++ wargs)) ws)
881 fillLHS _ _ _ c = c
883 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
884 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
885 fillLHSD n c a x = x
887{-| Parses with pattern
889@
890WExpr ::= '|' Expr';
892-}
893wExpr :: SyntaxInfo -> IdrisParser PTerm
894wExpr syn = do lchar '|'
895 expr' syn
896 <?> "with pattern"
898{- | Parses a where block
901WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
903-}
904whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
905whereBlock n syn
906 = do reserved "where"
907 ds <- indentedBlock1 (decl syn)
908 let dns = concatMap (concatMap declared) ds
909 return (concat ds, map (\x -> (x, decoration syn x)) dns)
910 <?> "where block"
912{- |Parses a code generation target language name
915Codegen ::= 'C'
916 | 'Java'
917 | 'JavaScript'
918 | 'Node'
919 | 'LLVM'
920 | 'Bytecode'
921 ;
923-}
924codegen_ :: IdrisParser Codegen
925codegen_ = do reserved "C"; return ViaC
926 <|> do reserved "Java"; return ViaJava
927 <|> do reserved "JavaScript"; return ViaJavaScript
928 <|> do reserved "Node"; return ViaNode
929 <|> do reserved "LLVM"; return ViaLLVM
930 <|> do reserved "Bytecode"; return Bytecode
931 <?> "code generation language"
933{- |Parses a compiler directive
935StringList ::=
936 String
937 | String ',' StringList
938 ;
942Directive ::= '%' Directive';
946Directive' ::= 'lib' CodeGen String_t
947 | 'link' CodeGen String_t
948 | 'flag' CodeGen String_t
949 | 'include' CodeGen String_t
950 | 'hide' Name
951 | 'freeze' Name
952 | 'access' Accessibility
953 | 'default' Totality
954 | 'logging' Natural
955 | 'dynamic' StringList
956 | 'name' Name NameList
957 | 'error_handlers' Name NameList
958 | 'language' 'TypeProviders'
959 | 'language' 'ErrorReflection'
960 ;
962-}
963directive :: SyntaxInfo -> IdrisParser [PDecl]
964directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
965 return [PDirective (do addLib cgn lib
966 addIBC (IBCLib cgn lib))]
967 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
968 return [PDirective (do dirs <- allImportDirs
969 o <- liftIO $ findInPath dirs obj
970 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
971 addObjectFile cgn o)]
972 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
973 flag <- stringLiteral
974 return [PDirective (do addIBC (IBCCGFlag cgn flag)
975 addFlag cgn flag)]
976 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
977 return [PDirective (do addHdr cgn hdr
978 addIBC (IBCHeader cgn hdr))]
979 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
980 return [PDirective (do setAccessibility n Hidden
981 addIBC (IBCAccess n Hidden))]
982 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
983 return [PDirective (do setAccessibility n Frozen
984 addIBC (IBCAccess n Frozen))]
985 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
986 return [PDirective (do i <- get
987 put(i { default_access = acc }))]
988 <|> do try (lchar '%' *> reserved "default"); tot <- totality
989 i <- get
990 put (i { default_total = tot } )
991 return [PDirective (do i <- get
992 put(i { default_total = tot }))]
993 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
994 return [PDirective (setLogLevel (fromInteger i))]
995 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
996 return [PDirective (do added <- addDyLib libs
997 case added of
998 Left lib -> addIBC (IBCDyLib (lib_name lib))
999 Right msg ->
1000 fail $ msg)]
1001 <|> do try (lchar '%' *> reserved "name")
1002 ty <- iName []
1003 ns <- sepBy1 name (lchar ',')
1004 return [PDirective (do ty' <- disambiguate ty
1005 mapM_ (addNameHint ty') ns
1006 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1007 <|> do try (lchar '%' *> reserved "error_handlers")
1008 fn <- fnName
1009 arg <- fnName
1010 ns <- sepBy1 name (lchar ',')
1011 return [PDirective (do fn' <- disambiguate fn
1012 ns' <- mapM disambiguate ns
1013 addFunctionErrorHandlers fn' arg ns'
1014 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]
1015 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1016 return [PDirective (addLangExt ext)]
1017 <?> "directive"
1018 where disambiguate :: Name -> Idris Name
1019 disambiguate n = do i <- getIState
1020 case lookupCtxtName n (idris_implicits i) of
1021 [(n', _)] -> return n'
1022 [] -> throwError (NoSuchVariable n)
1023 more -> throwError (CantResolveAlts (map (show . fst) more))
1025pLangExt :: IdrisParser LanguageExt
1026pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1027 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1029{- | Parses a totality
1032Totality ::= 'partial' | 'total'
1036totality :: IdrisParser Bool
1037totality
1038 = do reserved "total"; return True
1039 <|> do reserved "partial"; return False
1041{- | Parses a type provider
1044Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1045ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1047 -}
1048provider :: SyntaxInfo -> IdrisParser [PDecl]
1049provider syn = do try (lchar '%' *> reserved "provide");
1050 what <- provideWhat
1051 lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1052 fc <- getFC
1053 reserved "with"
1054 e <- expr syn
1055 return [PProvider syn fc what n t e]
1056 <?> "type provider"
1057 where provideWhat :: IdrisParser ProvideWhat
1058 provideWhat = option ProvAny
1059 ( ((reserved "proof" <|> reserved "term" <|> reserved "type") *>
1060 pure ProvTerm)
1061 <|> (reserved "postulate" *> pure ProvPostulate)
1062 <?> "provider variety")
1063{- | Parses a transform
1066Transform ::= '%' 'transform' Expr '==>' Expr
1069transform :: SyntaxInfo -> IdrisParser [PDecl]
1070transform syn = do try (lchar '%' *> reserved "transform")
1071 -- leave it unchecked, until we work out what this should
1072 -- actually mean...
1073-- safety <- option True (do reserved "unsafe"
1074-- return False)
1075 l <- expr syn
1076 fc <- getFC
1077 symbol "==>"
1078 r <- expr syn
1079 return [PTransform fc False l r]
1080 <?> "transform"
1083{- * Loading and parsing -}
1084{- | Parses an expression from input -}
1085parseExpr :: IState -> String -> Result PTerm
1086parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1088{- | Parses a tactic from input -}
1089parseTactic :: IState -> String -> Result PTactic
1090parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1092-- | Parse module header and imports
1093parseImports :: FilePath -> String -> Idris ([String], [(String, Maybe String, FC)], Maybe Delta)
1094parseImports fname input
1095 = do i <- getIState
1096 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1097 Failure err -> fail (show err)
1098 Success (x, i) -> do putIState i
1099 return x
1100 where imports :: IdrisParser (([String], [(String, Maybe String, FC)], Maybe Delta), IState)
1101 imports = do whiteSpace
1102 mname <- moduleHeader
1103 ps <- many import_
1104 mrk <- mark
1105 isEof <- lookAheadMatches eof
1106 let mrk' = if isEof
1107 then Nothing
1108 else Just mrk
1109 i <- get
1110 return ((mname, ps, mrk'), i)
1112-- | There should be a better way of doing this...
1113findFC :: Doc -> (FC, String)
1114findFC x = let s = show (plain x) in
1115 case span (/= ':') s of
1116 (failname, ':':rest) -> case span isDigit rest of
1117 (line, ':':rest') -> case span isDigit rest' of
1118 (col, ':':msg) -> (FC failname (read line) (read col), msg)
1120-- | A program is a list of declarations, possibly with associated
1121-- documentation strings.
1122parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1123 Idris [PDecl]
1124parseProg syn fname input mrk
1125 = do i <- getIState
1126 case runparser mainProg i fname input of
1127 Failure doc -> do -- FIXME: Get error location from trifecta
1128 -- this can't be the solution!
1129 let (fc, msg) = findFC doc
1130 i <- getIState
1131 case idris_outputmode i of
1132 RawOutput -> ihputStrLn (idris_outh i) (show doc)
1133 IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)
1134 putIState (i { errLine = Just (fc_line fc) }) -- Just errl })
1135 return []
1136 Success (x, i) -> do putIState i
1137 reportParserWarnings
1138 return $ collect x
1139 where mainProg :: IdrisParser ([PDecl], IState)
1140 mainProg = case mrk of
1141 Nothing -> do i <- get; return ([], i)
1142 Just mrk -> do
1143 release mrk
1144 ds <- prog syn
1145 i' <- get
1146 return (ds, i')
1148{- | Load idris module and show error if something wrong happens -}
1149loadModule :: Handle -> FilePath -> Idris String
1150loadModule outh f
1151 = idrisCatch (loadModule' outh f)
1152 (\e -> do setErrLine (getErrLine e)
1153 ist <- getIState
1154 msg <- showErr e
1155 ihputStrLn outh msg
1156 return "")
1158{- | Load idris module -}
1159loadModule' :: Handle -> FilePath -> Idris String
1160loadModule' outh f
1161 = do i <- getIState
1162 let file = takeWhile (/= ' ') f
1163 ibcsd <- valIBCSubDir i
1164 ids <- allImportDirs
1165 fp <- liftIO $ findImport ids ibcsd file
1166 if file `elem` imported i
1167 then iLOG $ "Already read " ++ file
1168 else do putIState (i { imported = file : imported i })
1169 case fp of
1170 IDR fn -> loadSource outh False fn
1171 LIDR fn -> loadSource outh True fn
1172 IBC fn src ->
1173 idrisCatch (loadIBC fn)
1174 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1175 case src of
1176 IDR sfn -> loadSource outh False sfn
1177 LIDR sfn -> loadSource outh True sfn)
1178 let (dir, fh) = splitFileName file
1179 return (dropExtension fh)
1182{- | Load idris code from file -}
1183loadFromIFile :: Handle -> IFileType -> Idris ()
1184loadFromIFile h i@(IBC fn src)
1185 = do iLOG $ "Skipping " ++ getSrcFile i
1186 idrisCatch (loadIBC fn)
1187 (\err -> ierror $ LoadingFailed fn err)
1188 where
1189 getSrcFile (IDR fn) = fn
1190 getSrcFile (LIDR fn) = fn
1191 getSrcFile (IBC f src) = getSrcFile src
1193loadFromIFile h (IDR fn) = loadSource' h False fn
1194loadFromIFile h (LIDR fn) = loadSource' h True fn
1196{-| Load idris source code and show error if something wrong happens -}
1197loadSource' :: Handle -> Bool -> FilePath -> Idris ()
1198loadSource' h lidr r
1199 = idrisCatch (loadSource h lidr r)
1200 (\e -> do setErrLine (getErrLine e)
1201 ist <- getIState
1202 ihRenderError h (pprintErr ist e))
1204{- | Load Idris source code-}
1205loadSource :: Handle -> Bool -> FilePath -> Idris ()
1206loadSource h lidr f
1207 = do iLOG ("Reading " ++ f)
1208 i <- getIState
1209 let def_total = default_total i
1210 file_in <- runIO $ readFile f
1211 file <- if lidr then tclift $ unlit f file_in else return file_in
1212 (mname, imports, pos) <- parseImports f file
1213 reportParserWarnings
1215 -- process and check module aliases
1216 let modAliases = M.fromList
1217 [(prep alias, prep realName) | (realName, Just alias, fc) <- imports]
1218 prep = map T.pack . reverse . Spl.splitOn "/"
1219 aliasNames = [(alias, fc) | (_, Just alias, fc) <- imports]
1220 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1221 case map head . filter ((/= 1) . length) $ histogram of
1222 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1223 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1225 i <- getIState
1226 putIState (i { default_access = Hidden, module_aliases = modAliases })
1227 clearIBC -- start a new .ibc file
1228 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]
1229 let syntax = defaultSyntax{ syn_namespace = reverse mname }
1230 ds' <- parseProg syntax f file pos
1232 -- Parsing done, now process declarations
1234 let ds = namespaces mname ds'
1235 logLvl 3 (show $ showDecls True ds)
1236 i <- getIState
1237 logLvl 10 (show (toAlist (idris_implicits i)))
1238 logLvl 3 (show (idris_infixes i))
1239 -- Now add all the declarations to the context
1240 v <- verbose
1241 when v $ ihputStrLn h $ "Type checking " ++ f
1242 -- we totality check after every Mutual block, so if
1243 -- anything is a single definition, wrap it in a
1244 -- mutual block on its own
1245 elabDecls toplevel (map toMutual ds)
1246 i <- getIState
1247 -- simplify every definition do give the totality checker
1248 -- a better chance
1249 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1250 updateContext (simplifyCasedef n))
1251 (map snd (idris_totcheck i))
1252 -- build size change graph from simplified definitions
1253 iLOG "Totality checking"
1254 i <- getIState
1255 mapM_ buildSCG (idris_totcheck i)
1256 mapM_ checkDeclTotality (idris_totcheck i)
1258 -- Redo totality check for deferred names
1259 let deftots = idris_defertotcheck i
1260 iLOG $ "Totality checking " ++ show deftots
1261 mapM_ (\x -> do tot <- getTotality x
1262 case tot of
1263 Total _ -> setTotality x Unchecked
1264 _ -> return ()) (map snd deftots)
1265 mapM_ buildSCG deftots
1266 mapM_ checkDeclTotality deftots
1268 iLOG ("Finished " ++ f)
1269 ibcsd <- valIBCSubDir i
1270 iLOG "Universe checking"
1271 iucheck
1272 let ibc = ibcPathNoFallback ibcsd f
1273 i <- getIState
1274 addHides (hide_list i)
1276 -- Finally, write an ibc if checking was successful
1278 ok <- noErrors
1279 when ok $
1280 idrisCatch (do writeIBC f ibc; clearIBC)
1281 (\c -> return ()) -- failure is harmless
1282 i <- getIState
1283 putIState (i { default_total = def_total,
1284 hide_list = [] })
1285 return ()
1286 where
1287 namespaces :: [String] -> [PDecl] -> [PDecl]
1288 namespaces [] ds = ds
1289 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1291 toMutual :: PDecl -> PDecl
1292 toMutual m@(PMutual _ d) = m
1293 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1294 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1295 case x of
1296 PClauses _ _ _ _ -> r
1297 PClass _ _ _ _ _ _ _ -> r
1298 PInstance _ _ _ _ _ _ _ _ -> r
1299 _ -> x
1301{- | Adds names to hide list -}
1302addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1303addHides xs = do i <- getIState
1304 let defh = default_access i
1305 let (hs, as) = partition isNothing xs
1306 unless (null as) $
1307 mapM_ doHide
1308 (map (\ (n, _) -> (n, defh)) hs ++
1309 map (\ (n, Just a) -> (n, a)) as)
1310 where isNothing (_, Nothing) = True
1311 isNothing _ = False
1313 doHide (n, a) = do setAccessibility n a
1314 addIBC (IBCAccess n a)