git.iko.soy/Idris-dev
on 751a6ee help sign in
Idris-dev/src/Idris/Parser.hs
1316 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 hiding (namespace, params)
22import Idris.DSL
23import Idris.Imports
24import Idris.Delaborate
25import Idris.Error
26import Idris.ElabDecls
27import Idris.ElabTerm
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 reserved "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))
388 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;
389 fnOpts (CExport c : opts)
390 <|> do try (lchar '%' *> reserved "assert_total");
391 fnOpts (AssertTotal : opts)
392 <|> do try (lchar '%' *> reserved "error_handler");
393 fnOpts (ErrorHandler : opts)
394 <|> do try (lchar '%' *> reserved "error_reverse");
395 fnOpts (ErrorReverse : opts)
396 <|> do try (lchar '%' *> reserved "reflection");
397 fnOpts (Reflection : opts)
398 <|> do lchar '%'; reserved "specialise";
399 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
400 fnOpts (Specialise ns : opts)
401 <|> do reserved "implicit"; fnOpts (Implicit : opts)
402 <|> return opts
403 <?> "function modifier"
404 where nameTimes :: IdrisParser (Name, Maybe Int)
405 nameTimes = do n <- fnName
406 t <- option Nothing (do reds <- natural
407 return (Just (fromInteger reds)))
408 return (n, t)
410{- | Parses a postulate
413Postulate ::=
414 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
415 ;
417-}
418postulate :: SyntaxInfo -> IdrisParser PDecl
419postulate syn = do doc <- try $ do doc <- option noDocs docComment
420 pushIndent
421 reserved "postulate"
422 return doc
423 ist <- get
424 let initOpts = if default_total ist
425 then [TotalFn]
426 else []
427 opts <- fnOpts initOpts
428 acc <- optional accessibility
429 opts' <- fnOpts opts
430 n_in <- fnName
431 let n = expandNS syn n_in
432 lchar ':'
433 ty <- typeExpr (allowImp syn)
434 fc <- getFC
435 terminator
436 addAcc n acc
437 return (PPostulate (fst doc) syn fc opts' n ty)
438 <?> "postulate"
440{- | Parses a using declaration
443Using ::=
444 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
445 ;
447 -}
448using_ :: SyntaxInfo -> IdrisParser [PDecl]
449using_ syn =
450 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
451 openBlock
452 let uvars = using syn
453 ds <- many (decl (syn { using = uvars ++ ns }))
454 closeBlock
455 return (concat ds)
456 <?> "using declaration"
458{- | Parses a parameters declaration
461Params ::=
462 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
463 ;
465 -}
466params :: SyntaxInfo -> IdrisParser [PDecl]
467params syn =
468 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
469 openBlock
470 let pvars = syn_params syn
471 ds <- many (decl syn { syn_params = pvars ++ ns })
472 closeBlock
473 fc <- getFC
474 return [PParams fc ns (concat ds)]
475 <?> "parameters declaration"
477{- | Parses a mutual declaration (for mutually recursive functions)
480Mutual ::=
481 'mutual' OpenBlock Decl* CloseBlock
482 ;
484-}
485mutual :: SyntaxInfo -> IdrisParser [PDecl]
486mutual syn =
487 do reserved "mutual"
488 openBlock
489 let pvars = syn_params syn
490 ds <- many (decl syn)
491 closeBlock
492 fc <- getFC
493 return [PMutual fc (concat ds)]
494 <?> "mutual block"
496{-| Parses a namespace declaration
499Namespace ::=
500 'namespace' identifier OpenBlock Decl+ CloseBlock
501 ;
503-}
504namespace :: SyntaxInfo -> IdrisParser [PDecl]
505namespace syn =
506 do reserved "namespace"; n <- identifier;
507 openBlock
508 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
509 closeBlock
510 return [PNamespace n (concat ds)]
511 <?> "namespace declaration"
513{- | Parses a methods block (for instances)
516 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
518-}
519instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
520instanceBlock syn = do reserved "where"
521 openBlock
522 ds <- many (fnDecl syn)
523 closeBlock
524 return (concat ds)
525 <?> "instance block"
527{- | Parses a methods and instances block (for type classes)
530MethodOrInstance ::=
531 FnDecl
532 | Instance
533 ;
537ClassBlock ::=
538 'where' OpenBlock MethodOrInstance* CloseBlock
539 ;
541-}
542classBlock :: SyntaxInfo -> IdrisParser [PDecl]
543classBlock syn = do reserved "where"
544 openBlock
545 ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)
546 closeBlock
547 return (concat ds)
548 <?> "class block"
550{-| Parses a type class declaration
553ClassArgument ::=
554 Name
555 | '(' Name ':' Expr ')'
556 ;
560Class ::=
561 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
562 ;
564-}
565class_ :: SyntaxInfo -> IdrisParser [PDecl]
566class_ syn = do (doc, acc) <- try (do
567 doc <- option noDocs docComment
568 acc <- optional accessibility
569 return (doc, acc))
570 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName
571 let n = expandNS syn n_in
572 cs <- many carg
573 ds <- option [] (classBlock syn)
574 accData acc n (concatMap declared ds)
575 return [PClass (fst doc) syn fc cons n cs ds]
576 <?> "type-class declaration"
577 where
578 carg :: IdrisParser (Name, PTerm)
579 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
580 return (i, ty)
581 <|> do i <- name;
582 return (i, PType)
584{- | Parses a type class instance declaration
587 Instance ::=
588 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
589 ;
593InstanceName ::= '[' Name ']';
595-}
596instance_ :: SyntaxInfo -> IdrisParser [PDecl]
597instance_ syn = do reserved "instance"; fc <- getFC
598 en <- optional instanceName
599 cs <- constraintList syn
600 cn <- fnName
601 args <- many (simpleExpr syn)
602 let sc = PApp fc (PRef fc cn) (map pexp args)
603 let t = bindList (PPi constraint) (map (\x -> (sMN 0 "constraint", x)) cs) sc
604 ds <- option [] (instanceBlock syn)
605 return [PInstance syn fc cs cn args t en ds]
606 <?> "instance declaration"
607 where instanceName :: IdrisParser Name
608 instanceName = do lchar '['; n_in <- fnName; lchar ']'
609 let n = expandNS syn n_in
610 return n
611 <?> "instance name"
614{- | Parses a using declaration list
617UsingDeclList ::=
618 UsingDeclList'
619 | NameList TypeSig
620 ;
624UsingDeclList' ::=
625 UsingDecl
626 | UsingDecl ',' UsingDeclList'
627 ;
631NameList ::=
632 Name
633 | Name ',' NameList
634 ;
636-}
637usingDeclList :: SyntaxInfo -> IdrisParser [Using]
638usingDeclList syn
639 = try (sepBy1 (usingDecl syn) (lchar ','))
640 <|> do ns <- sepBy1 name (lchar ',')
641 lchar ':'
642 t <- typeExpr (disallowImp syn)
643 return (map (\x -> UImplicit x t) ns)
644 <?> "using declaration list"
646{- |Parses a using declaration
649UsingDecl ::=
650 FnName TypeSig
651 | FnName FnName+
652 ;
654-}
655usingDecl :: SyntaxInfo -> IdrisParser Using
656usingDecl syn = try (do x <- fnName
657 lchar ':'
658 t <- typeExpr (disallowImp syn)
659 return (UImplicit x t))
660 <|> do c <- fnName
661 xs <- some fnName
662 return (UConstraint c xs)
663 <?> "using declaration"
665{- | Parse a clause with patterns
668Pattern ::= Clause;
670-}
671pattern :: SyntaxInfo -> IdrisParser PDecl
672pattern syn = do fc <- getFC
673 clause <- clause syn
674 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
675 <?> "pattern"
677{- | Parse a constant applicative form declaration
680CAF ::= 'let' FnName '=' Expr Terminator;
682-}
683caf :: SyntaxInfo -> IdrisParser PDecl
684caf syn = do reserved "let"
685 n_in <- fnName; let n = expandNS syn n_in
686 lchar '='
687 t <- expr syn
688 terminator
689 fc <- getFC
690 return (PCAF fc n t)
691 <?> "constant applicative form declaration"
693{- | Parse an argument expression
696ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
698-}
699argExpr :: SyntaxInfo -> IdrisParser PTerm
700argExpr syn = let syn' = syn { inPattern = True } in
701 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
702 <?> "argument expression"
704{- | Parse a right hand side of a function
707RHS ::= '=' Expr
708 | '?=' RHSName? Expr
709 | 'impossible'
710 ;
714RHSName ::= '{' FnName '}';
716-}
717rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
718rhs syn n = do lchar '='; expr syn
719 <|> do symbol "?=";
720 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
721 return n)
722 r <- expr syn
723 return (addLet name r)
724 <|> do reserved "impossible"; return PImpossible
725 <?> "function right hand side"
726 where mkN :: Name -> Name
727 mkN (UN x) = sUN (str x++"_lemma_1")
728 mkN (NS x n) = NS (mkN x) n
729 n' :: Name
730 n' = mkN n
731 addLet :: Name -> PTerm -> PTerm
732 addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)
733 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
734 where addLetC (l, r) = (l, addLet nm r)
735 addLet nm r = (PLet (sUN "value") Placeholder r (PMetavar nm))
737{- |Parses a function clause
740RHSOrWithBlock ::= RHS WhereOrTerminator
741 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
742 ;
746Clause ::= WExpr+ RHSOrWithBlock
747 | SimpleExpr '<==' FnName RHS WhereOrTerminator
748 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
749 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
750 ;
754ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
758WhereOrTerminator ::= WhereBlock | Terminator;
760-}
761clause :: SyntaxInfo -> IdrisParser PClause
762clause syn
763 = do wargs <- try (do pushIndent; some (wExpr syn))
764 fc <- getFC
765 ist <- get
766 n <- case lastParse ist of
767 Just t -> return t
768 Nothing -> fail "Invalid clause"
769 (do r <- rhs syn n
770 let ctxt = tt_ctxt ist
771 let wsyn = syn { syn_namespace = [] }
772 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
773 popIndent
774 return x,
775 do terminator
776 return ([], [])]
777 return $ PClauseR fc wargs r wheres) <|> (do
778 popIndent
779 reserved "with"
780 wval <- simpleExpr syn
781 openBlock
782 ds <- some $ fnDecl syn
783 let withs = concat ds
784 closeBlock
785 return $ PWithR fc wargs wval withs)
786 <|> do ty <- try (do pushIndent
787 ty <- simpleExpr syn
788 symbol "<=="
789 return ty)
790 fc <- getFC
791 n_in <- fnName; let n = expandNS syn n_in
792 r <- rhs syn n
793 ist <- get
794 let ctxt = tt_ctxt ist
795 let wsyn = syn { syn_namespace = [] }
796 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
797 popIndent
798 return x,
799 do terminator
800 return ([], [])]
801 let capp = PLet (sMN 0 "match")
802 ty
803 (PMatchApp fc n)
804 (PRef fc (sMN 0 "match"))
805 ist <- get
806 put (ist { lastParse = Just n })
807 return $ PClause fc n capp [] r wheres
808 <|> do (l, op) <- try (do
809 pushIndent
810 l <- argExpr syn
811 op <- operator
812 when (op == "=" || op == "?=" ) $
813 fail "infix clause definition with \"=\" and \"?=\" not supported "
814 return (l, op))
815 let n = expandNS syn (sUN op)
816 r <- argExpr syn
817 fc <- getFC
818 wargs <- many (wExpr syn)
819 (do rs <- rhs syn n
820 let wsyn = syn { syn_namespace = [] }
821 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
822 popIndent
823 return x,
824 do terminator
825 return ([], [])]
826 ist <- get
827 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
828 put (ist { lastParse = Just n })
829 return $ PClause fc n capp wargs rs wheres) <|> (do
830 popIndent
831 reserved "with"
832 lchar '(' <?> "parenthesized expression"
833 wval <- bracketed syn
834 openBlock
835 ds <- some $ fnDecl syn
836 closeBlock
837 ist <- get
838 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
839 let withs = map (fillLHSD n capp wargs) $ concat ds
840 put (ist { lastParse = Just n })
841 return $ PWith fc n capp wargs wval withs)
842 <|> do pushIndent
843 n_in <- fnName; let n = expandNS syn n_in
844 cargs <- many (constraintArg syn)
845 fc <- getFC
846 args <- many (try (implicitArg (syn { inPattern = True } ))
847 <|> (fmap pexp (argExpr syn)))
848 wargs <- many (wExpr syn)
849 let capp = PApp fc (PRef fc n)
850 (cargs ++ args)
851 (do r <- rhs syn n
852 ist <- get
853 let ctxt = tt_ctxt ist
854 let wsyn = syn { syn_namespace = [] }
855 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
856 popIndent
857 return x,
858 do terminator
859 return ([], [])]
860 ist <- get
861 put (ist { lastParse = Just n })
862 return $ PClause fc n capp wargs r wheres) <|> (do
863 reserved "with"
864 ist <- get
865 put (ist { lastParse = Just n })
866 lchar '(' <?> "parenthesized expression"
867 wval <- bracketed syn
868 openBlock
869 ds <- some $ fnDecl syn
870 let withs = map (fillLHSD n capp wargs) $ concat ds
871 closeBlock
872 popIndent
873 return $ PWith fc n capp wargs wval withs)
874 <?> "function clause"
875 where
876 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
877 fillLHS n capp owargs (PClauseR fc wargs v ws)
878 = PClause fc n capp (owargs ++ wargs) v ws
879 fillLHS n capp owargs (PWithR fc wargs v ws)
880 = PWith fc n capp (owargs ++ wargs) v
881 (map (fillLHSD n capp (owargs ++ wargs)) ws)
882 fillLHS _ _ _ c = c
884 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
885 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
886 fillLHSD n c a x = x
888{-| Parses with pattern
890@
891WExpr ::= '|' Expr';
893-}
894wExpr :: SyntaxInfo -> IdrisParser PTerm
895wExpr syn = do lchar '|'
896 expr' syn
897 <?> "with pattern"
899{- | Parses a where block
902WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
904-}
905whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
906whereBlock n syn
907 = do reserved "where"
908 ds <- indentedBlock1 (decl syn)
909 let dns = concatMap (concatMap declared) ds
910 return (concat ds, map (\x -> (x, decoration syn x)) dns)
911 <?> "where block"
913{- |Parses a code generation target language name
916Codegen ::= 'C'
917 | 'Java'
918 | 'JavaScript'
919 | 'Node'
920 | 'LLVM'
921 | 'Bytecode'
922 ;
924-}
925codegen_ :: IdrisParser Codegen
926codegen_ = do reserved "C"; return ViaC
927 <|> do reserved "Java"; return ViaJava
928 <|> do reserved "JavaScript"; return ViaJavaScript
929 <|> do reserved "Node"; return ViaNode
930 <|> do reserved "LLVM"; return ViaLLVM
931 <|> do reserved "Bytecode"; return Bytecode
932 <?> "code generation language"
934{- |Parses a compiler directive
936StringList ::=
937 String
938 | String ',' StringList
939 ;
943Directive ::= '%' Directive';
947Directive' ::= 'lib' CodeGen String_t
948 | 'link' CodeGen String_t
949 | 'flag' CodeGen String_t
950 | 'include' CodeGen String_t
951 | 'hide' Name
952 | 'freeze' Name
953 | 'access' Accessibility
954 | 'default' Totality
955 | 'logging' Natural
956 | 'dynamic' StringList
957 | 'name' Name NameList
958 | 'error_handlers' Name NameList
959 | 'language' 'TypeProviders'
960 | 'language' 'ErrorReflection'
961 ;
963-}
964directive :: SyntaxInfo -> IdrisParser [PDecl]
965directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
966 return [PDirective (do addLib cgn lib
967 addIBC (IBCLib cgn lib))]
968 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
969 return [PDirective (do dirs <- allImportDirs
970 o <- liftIO $ findInPath dirs obj
971 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
972 addObjectFile cgn o)]
973 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
974 flag <- stringLiteral
975 return [PDirective (do addIBC (IBCCGFlag cgn flag)
976 addFlag cgn flag)]
977 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
978 return [PDirective (do addHdr cgn hdr
979 addIBC (IBCHeader cgn hdr))]
980 <|> do try (lchar '%' *> reserved "hide"); n <- fnName
981 return [PDirective (do setAccessibility n Hidden
982 addIBC (IBCAccess n Hidden))]
983 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
984 return [PDirective (do setAccessibility n Frozen
985 addIBC (IBCAccess n Frozen))]
986 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
987 return [PDirective (do i <- get
988 put(i { default_access = acc }))]
989 <|> do try (lchar '%' *> reserved "default"); tot <- totality
990 i <- get
991 put (i { default_total = tot } )
992 return [PDirective (do i <- get
993 put(i { default_total = tot }))]
994 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
995 return [PDirective (setLogLevel (fromInteger i))]
996 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
997 return [PDirective (do added <- addDyLib libs
998 case added of
999 Left lib -> addIBC (IBCDyLib (lib_name lib))
1000 Right msg ->
1001 fail $ msg)]
1002 <|> do try (lchar '%' *> reserved "name")
1003 ty <- iName []
1004 ns <- sepBy1 name (lchar ',')
1005 return [PDirective (do ty' <- disambiguate ty
1006 mapM_ (addNameHint ty') ns
1007 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1008 <|> do try (lchar '%' *> reserved "error_handlers")
1009 fn <- fnName
1010 arg <- fnName
1011 ns <- sepBy1 name (lchar ',')
1012 return [PDirective (do fn' <- disambiguate fn
1013 ns' <- mapM disambiguate ns
1014 addFunctionErrorHandlers fn' arg ns'
1015 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]
1016 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1017 return [PDirective (addLangExt ext)]
1018 <?> "directive"
1019 where disambiguate :: Name -> Idris Name
1020 disambiguate n = do i <- getIState
1021 case lookupCtxtName n (idris_implicits i) of
1022 [(n', _)] -> return n'
1023 [] -> throwError (NoSuchVariable n)
1024 more -> throwError (CantResolveAlts (map (show . fst) more))
1026pLangExt :: IdrisParser LanguageExt
1027pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1028 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1030{- | Parses a totality
1033Totality ::= 'partial' | 'total'
1037totality :: IdrisParser Bool
1038totality
1039 = do reserved "total"; return True
1040 <|> do reserved "partial"; return False
1042{- | Parses a type provider
1045Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
1046ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
1048 -}
1049provider :: SyntaxInfo -> IdrisParser [PDecl]
1050provider syn = do try (lchar '%' *> reserved "provide");
1051 what <- provideWhat
1052 lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1053 fc <- getFC
1054 reserved "with"
1055 e <- expr syn
1056 return [PProvider syn fc what n t e]
1057 <?> "type provider"
1058 where provideWhat :: IdrisParser ProvideWhat
1059 provideWhat = option ProvAny
1060 ( ((reserved "proof" <|> reserved "term" <|> reserved "type") *>
1061 pure ProvTerm)
1062 <|> (reserved "postulate" *> pure ProvPostulate)
1063 <?> "provider variety")
1064{- | Parses a transform
1067Transform ::= '%' 'transform' Expr '==>' Expr
1070transform :: SyntaxInfo -> IdrisParser [PDecl]
1071transform syn = do try (lchar '%' *> reserved "transform")
1072 -- leave it unchecked, until we work out what this should
1073 -- actually mean...
1074-- safety <- option True (do reserved "unsafe"
1075-- return False)
1076 l <- expr syn
1077 fc <- getFC
1078 symbol "==>"
1079 r <- expr syn
1080 return [PTransform fc False l r]
1081 <?> "transform"
1084{- * Loading and parsing -}
1085{- | Parses an expression from input -}
1086parseExpr :: IState -> String -> Result PTerm
1087parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"
1089{- | Parses a tactic from input -}
1090parseTactic :: IState -> String -> Result PTactic
1091parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
1093-- | Parse module header and imports
1094parseImports :: FilePath -> String -> Idris ([String], [(String, Maybe String, FC)], Maybe Delta)
1095parseImports fname input
1096 = do i <- getIState
1097 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1098 Failure err -> fail (show err)
1099 Success (x, i) -> do putIState i
1100 return x
1101 where imports :: IdrisParser (([String], [(String, Maybe String, FC)], Maybe Delta), IState)
1102 imports = do whiteSpace
1103 mname <- moduleHeader
1104 ps <- many import_
1105 mrk <- mark
1106 isEof <- lookAheadMatches eof
1107 let mrk' = if isEof
1108 then Nothing
1109 else Just mrk
1110 i <- get
1111 return ((mname, ps, mrk'), i)
1113-- | There should be a better way of doing this...
1114findFC :: Doc -> (FC, String)
1115findFC x = let s = show (plain x) in
1116 case span (/= ':') s of
1117 (failname, ':':rest) -> case span isDigit rest of
1118 (line, ':':rest') -> case span isDigit rest' of
1119 (col, ':':msg) -> let pos = (read line, read col) in
1120 (FC failname pos pos, msg)
1122-- | A program is a list of declarations, possibly with associated
1123-- documentation strings.
1124parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1125 Idris [PDecl]
1126parseProg syn fname input mrk
1127 = do i <- getIState
1128 case runparser mainProg i fname input of
1129 Failure doc -> do -- FIXME: Get error location from trifecta
1130 -- this can't be the solution!
1131 let (fc, msg) = findFC doc
1132 i <- getIState
1133 case idris_outputmode i of
1134 RawOutput -> ihputStrLn (idris_outh i) (show doc)
1135 IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)
1136 putIState (i { errSpan = Just fc })
1137 return []
1138 Success (x, i) -> do putIState i
1139 reportParserWarnings
1140 return $ collect x
1141 where mainProg :: IdrisParser ([PDecl], IState)
1142 mainProg = case mrk of
1143 Nothing -> do i <- get; return ([], i)
1144 Just mrk -> do
1145 release mrk
1146 ds <- prog syn
1147 i' <- get
1148 return (ds, i')
1150{- | Load idris module and show error if something wrong happens -}
1151loadModule :: Handle -> FilePath -> Idris String
1152loadModule outh f
1153 = idrisCatch (loadModule' outh f)
1154 (\e -> do setErrSpan (getErrSpan e)
1155 ist <- getIState
1156 msg <- showErr e
1157 ihputStrLn outh msg
1158 return "")
1160{- | Load idris module -}
1161loadModule' :: Handle -> FilePath -> Idris String
1162loadModule' outh f
1163 = do i <- getIState
1164 let file = takeWhile (/= ' ') f
1165 ibcsd <- valIBCSubDir i
1166 ids <- allImportDirs
1167 fp <- liftIO $ findImport ids ibcsd file
1168 if file `elem` imported i
1169 then iLOG $ "Already read " ++ file
1170 else do putIState (i { imported = file : imported i })
1171 case fp of
1172 IDR fn -> loadSource outh False fn
1173 LIDR fn -> loadSource outh True fn
1174 IBC fn src ->
1175 idrisCatch (loadIBC fn)
1176 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c
1177 case src of
1178 IDR sfn -> loadSource outh False sfn
1179 LIDR sfn -> loadSource outh True sfn)
1180 let (dir, fh) = splitFileName file
1181 return (dropExtension fh)
1184{- | Load idris code from file -}
1185loadFromIFile :: Handle -> IFileType -> Idris ()
1186loadFromIFile h i@(IBC fn src)
1187 = do iLOG $ "Skipping " ++ getSrcFile i
1188 idrisCatch (loadIBC fn)
1189 (\err -> ierror $ LoadingFailed fn err)
1190 where
1191 getSrcFile (IDR fn) = fn
1192 getSrcFile (LIDR fn) = fn
1193 getSrcFile (IBC f src) = getSrcFile src
1195loadFromIFile h (IDR fn) = loadSource' h False fn
1196loadFromIFile h (LIDR fn) = loadSource' h True fn
1198{-| Load idris source code and show error if something wrong happens -}
1199loadSource' :: Handle -> Bool -> FilePath -> Idris ()
1200loadSource' h lidr r
1201 = idrisCatch (loadSource h lidr r)
1202 (\e -> do setErrSpan (getErrSpan e)
1203 ist <- getIState
1204 ihRenderError h (pprintErr ist e))
1206{- | Load Idris source code-}
1207loadSource :: Handle -> Bool -> FilePath -> Idris ()
1208loadSource h lidr f
1209 = do iLOG ("Reading " ++ f)
1210 i <- getIState
1211 let def_total = default_total i
1212 file_in <- runIO $ readFile f
1213 file <- if lidr then tclift $ unlit f file_in else return file_in
1214 (mname, imports, pos) <- parseImports f file
1215 reportParserWarnings
1217 -- process and check module aliases
1218 let modAliases = M.fromList
1219 [(prep alias, prep realName) | (realName, Just alias, fc) <- imports]
1220 prep = map T.pack . reverse . Spl.splitOn "/"
1221 aliasNames = [(alias, fc) | (_, Just alias, fc) <- imports]
1222 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1223 case map head . filter ((/= 1) . length) $ histogram of
1224 [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1225 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1227 i <- getIState
1228 putIState (i { default_access = Hidden, module_aliases = modAliases })
1229 clearIBC -- start a new .ibc file
1230 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]
1231 let syntax = defaultSyntax{ syn_namespace = reverse mname }
1232 ds' <- parseProg syntax f file pos
1234 -- Parsing done, now process declarations
1236 let ds = namespaces mname ds'
1237 logLvl 3 (show $ showDecls True ds)
1238 i <- getIState
1239 logLvl 10 (show (toAlist (idris_implicits i)))
1240 logLvl 3 (show (idris_infixes i))
1241 -- Now add all the declarations to the context
1242 v <- verbose
1243 when v $ ihputStrLn h $ "Type checking " ++ f
1244 -- we totality check after every Mutual block, so if
1245 -- anything is a single definition, wrap it in a
1246 -- mutual block on its own
1247 elabDecls toplevel (map toMutual ds)
1248 i <- getIState
1249 -- simplify every definition do give the totality checker
1250 -- a better chance
1251 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1252 updateContext (simplifyCasedef n))
1253 (map snd (idris_totcheck i))
1254 -- build size change graph from simplified definitions
1255 iLOG "Totality checking"
1256 i <- getIState
1257 mapM_ buildSCG (idris_totcheck i)
1258 mapM_ checkDeclTotality (idris_totcheck i)
1260 -- Redo totality check for deferred names
1261 let deftots = idris_defertotcheck i
1262 iLOG $ "Totality checking " ++ show deftots
1263 mapM_ (\x -> do tot <- getTotality x
1264 case tot of
1265 Total _ -> setTotality x Unchecked
1266 _ -> return ()) (map snd deftots)
1267 mapM_ buildSCG deftots
1268 mapM_ checkDeclTotality deftots
1270 iLOG ("Finished " ++ f)
1271 ibcsd <- valIBCSubDir i
1272 iLOG "Universe checking"
1273 iucheck
1274 let ibc = ibcPathNoFallback ibcsd f
1275 i <- getIState
1276 addHides (hide_list i)
1278 -- Finally, write an ibc if checking was successful
1280 ok <- noErrors
1281 when ok $
1282 idrisCatch (do writeIBC f ibc; clearIBC)
1283 (\c -> return ()) -- failure is harmless
1284 i <- getIState
1285 putIState (i { default_total = def_total,
1286 hide_list = [] })
1287 return ()
1288 where
1289 namespaces :: [String] -> [PDecl] -> [PDecl]
1290 namespaces [] ds = ds
1291 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1293 toMutual :: PDecl -> PDecl
1294 toMutual m@(PMutual _ d) = m
1295 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
1296 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
1297 case x of
1298 PClauses _ _ _ _ -> r
1299 PClass _ _ _ _ _ _ _ -> r
1300 PInstance _ _ _ _ _ _ _ _ -> r
1301 _ -> x
1303{- | Adds names to hide list -}
1304addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1305addHides xs = do i <- getIState
1306 let defh = default_access i
1307 let (hs, as) = partition isNothing xs
1308 unless (null as) $
1309 mapM_ doHide
1310 (map (\ (n, _) -> (n, defh)) hs ++
1311 map (\ (n, Just a) -> (n, a)) as)
1312 where isNothing (_, Nothing) = True
1313 isNothing _ = False
1315 doHide (n, a) = do setAccessibility n a
1316 addIBC (IBCAccess n a)