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