1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
2module Idris.Parser where
4import Prelude hiding (pi)
6import Text.Trifecta.Delta
7import Text.Trifecta hiding (span, token, whiteSpace, stringLiteral, charLiteral, natural, symbol, char, string)
8import Text.Parser.LookAhead
9import Text.Parser.Expression
10import qualified Text.Parser.Token as Tok
11import qualified Text.Parser.Char as Chr
12import qualified Text.Parser.Token.Highlight as Hi
19import Idris.ElabTerm hiding (namespace, params)
26import Util.DynamicLinker
31import Control.Applicative
33import Control.Monad.State.Strict
36import qualified Data.List.Split as Spl
40import qualified Data.HashSet as HS
41import qualified Data.Text as T
42import qualified Data.ByteString.UTF8 as UTF8
48 grammar shortcut notation:
49 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)
50 RULE? = optional rule (i.e. RULE or nothing)
51 RULE* = repeated rule (i.e. RULE zero or more times)
52 RULE+ = repeated rule with at least one match (i.e. RULE one or more times)
53 RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)
54 RULE{n} = rule repeated n times
58-- | Idris parser with state used during parsing
59type IdrisParser = StateT IState Parser
61-- | Generalized monadic parsing constraint type
62type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)
64{- * Space, comments and literals (token/lexing like parsers) -}
65-- | Parses a token by applying parser and then consuming all following whiteSpace
66lexeme :: MonadicParsing m => m a -> m a
67lexeme p = p <* whiteSpace
69-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)
70simpleWhiteSpace :: MonadicParsing m => m ()
71simpleWhiteSpace = satisfy isSpace *> pure ()
73-- | Checks if a charcter is end of line
76isEol '\0' = True -- Check eof too
79-- | Checks if a character is a documentation comment marker
80isDocCommentMarker :: Char -> Bool
81isDocCommentMarker '|' = True
82isDocCommentMarker '^' = True
83isDocCommentMarker _ = False
85{- | Consumes a single-line comment
86 SingleLineComment_t ::= '--' EOL_t
87 | '--' ~DocCommentMarker_t ~EOL_t* EOL_t
90singleLineComment :: MonadicParsing m => m ()
91singleLineComment = try (string "--" *> satisfy isEol *> pure ())
92 <|> string "--" *> satisfy (not . isDocCommentMarker) *> many (satisfy (not . isEol)) *> (satisfy isEol <?> "end of line") *> pure ()
95{- | Consumes a multi-line comment
96 MultiLineComment_t ::=
98 | '{ -' ~DocCommentMarker_t InCommentChars_t
103 | MultiLineComment_t InCommentChars_t
104 | ~'- }'+ InCommentChars_t
108multiLineComment :: MonadicParsing m => m ()
109multiLineComment = try (string "{-" *> (string "-}") *> pure ())
110 <|> string "{-" *> satisfy (not . isDocCommentMarker) *> inCommentChars
112 where inCommentChars :: MonadicParsing m => m ()
113 inCommentChars = string "-}" *> pure ()
114 <|> try (multiLineComment) *> inCommentChars
115 <|> try (docComment '|') *> inCommentChars
116 <|> try (docComment '^') *> inCommentChars
117 <|> skipSome (noneOf startEnd) *> inCommentChars
118 <|> oneOf startEnd *> inCommentChars
123{-| Parses a documentation comment (similar to haddoc) given a marker character
124 DocComment_t ::= '--' DocCommentMarker_t ~EOL_t* EOL_t
125 | '{ -' DocCommentMarket_t ~'- }'* '- }'
128docComment :: MonadicParsing m => Char -> m String
129docComment marker | isDocCommentMarker marker = do dc <- docComment' marker; return (T.unpack $ T.strip $ T.pack dc)
130 | otherwise = fail "internal error: tried to parse a documentation comment with invalid marker"
131 where docComment' :: MonadicParsing m => Char -> m String
132 docComment' marker = string "--" *> char marker *> many (satisfy (not . isEol)) <* satisfy isEol
133 <|> string "{-" *> char marker *> (manyTill anyChar (try (string "-}")) <?> "end of comment")
136-- | Consumes whitespace (and comments)
137whiteSpace :: MonadicParsing m => m ()
138whiteSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
140-- | Parses a string literal
141stringLiteral :: MonadicParsing m => m String
142stringLiteral = lexeme $ Tok.stringLiteral
144-- | Parses a char literal
145charLiteral :: MonadicParsing m => m Char
146charLiteral = lexeme $ Tok.charLiteral
148-- | Parses a natural number
149natural :: MonadicParsing m => m Integer
150natural = lexeme $ Tok.natural
152-- | Parses an integral number
153integer :: MonadicParsing m => m Integer
154integer = lexeme $ Tok.integer
156-- | Parses a floating point number
157float :: MonadicParsing m => m Double
158float = lexeme $ Tok.double
160{- * Symbols, identifiers, names and operators -}
163-- | Idris Style for parsing identifiers/reserved keywords
164idrisStyle :: MonadicParsing m => IdentifierStyle m
165idrisStyle = IdentifierStyle _styleName _styleStart _styleLetter _styleReserved Hi.Identifier Hi.ReservedIdentifier
166 where _styleName = "Idris"
167 _styleStart = satisfy isAlpha
168 _styleLetter = satisfy isAlphaNum <|> oneOf "_'" <|> (lchar '.')
169 _styleReserved = HS.fromList ["let", "in", "data", "codata", "record", "Type",
170 "do", "dsl", "import", "impossible",
171 "case", "of", "total", "partial", "mutual",
172 "infix", "infixl", "infixr", "rewrite",
173 "where", "with", "syntax", "proof", "postulate",
174 "using", "namespace", "class", "instance",
175 "public", "private", "abstract", "implicit",
177 "Int", "Integer", "Float", "Char", "String", "Ptr",
178 "Bits8", "Bits16", "Bits32", "Bits64",
179 "Bits8x16", "Bits16x8", "Bits32x4", "Bits64x2"]
181char :: MonadicParsing m => Char -> m Char
184string :: MonadicParsing m => String -> m String
187-- | Parses a character as a lexeme
188lchar :: MonadicParsing m => Char -> m Char
191-- | Parses string as a lexeme
192symbol :: MonadicParsing m => String -> m String
193symbol = lexeme . Tok.symbol
195-- | Parses a reserved identifier
196reserved :: MonadicParsing m => String -> m ()
197reserved = lexeme . Tok.reserve idrisStyle
199-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
200-- | Parses a reserved operator
201reservedOp :: MonadicParsing m => String -> m ()
202reservedOp name = lexeme $ try $
204 notFollowedBy (operatorLetter) <?> ("end of " ++ show name)
206-- | Parses an identifier as a lexeme
207identifier :: MonadicParsing m => m String
208identifier = lexeme $ Tok.ident idrisStyle
210-- | Parses an identifier with possible namespace as a name
211iName :: MonadicParsing m => [String] -> m Name
212iName bad = maybeWithNS identifier False bad <?> "name"
214-- | Parses an string possibly prefixed by a namespace
215maybeWithNS :: MonadicParsing m => m String -> Bool -> [String] -> m Name
216maybeWithNS parser ascend bad = do
217 i <- option "" (lookAhead identifier)
218 when (i `elem` bad) $ unexpected "reserved identifier"
219 let transf = if ascend then id else reverse
220 (x, xs) <- choice (transf (parserNoNS parser : parsersNS parser i))
221 return $ mkName (x, xs)
222 where parserNoNS :: MonadicParsing m => m String -> m (String, String)
223 parserNoNS parser = do x <- parser; return (x, "")
224 parserNS :: MonadicParsing m => m String -> String -> m (String, String)
225 parserNS parser ns = do xs <- string ns; lchar '.'; x <- parser; return (x, xs)
226 parsersNS :: MonadicParsing m => m String -> String -> [m (String, String)]
227 parsersNS parser i = [try (parserNS parser ns) | ns <- (initsEndAt (=='.') i)]
230name :: IdrisParser Name
232 iName (syntax_keywords i)
236{- | List of all initial segments in ascending order of a list. Every such
237 initial segment ends right before an element satisfying the given
240initsEndAt :: (a -> Bool) -> [a] -> [[a]]
242initsEndAt p (x:xs) | p x = [] : x_inits_xs
243 | otherwise = x_inits_xs
244 where x_inits_xs = [x : cs | cs <- initsEndAt p xs]
247{- | Create a `Name' from a pair of strings representing a base name and its
250mkName :: (String, String) -> Name
252mkName (n, ns) = NS (UN n) (reverse (parseNS ns))
253 where parseNS x = case span (/= '.') x of
255 (x, '.':y) -> x : parseNS y
257operatorLetter :: MonadicParsing m => m Char
258operatorLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
260-- | Parses an operator
261operator :: MonadicParsing m => m String
262operator = lexeme . some $ operatorLetter
264{- * Position helpers -}
265{- | Get filename from position (returns "(interactive)" when no source file is given) -}
266fileName :: Delta -> String
267fileName (Directed fn _ _ _ _) = UTF8.toString fn
268fileName _ = "(interactive)"
270{- | Get line number from position -}
271lineNum :: Delta -> Int
272lineNum (Lines l _ _ _) = fromIntegral l + 1
273lineNum (Directed _ l _ _ _) = fromIntegral l + 1
275{- | Get file position as FC -}
276getFC :: MonadicParsing m => m FC
277getFC = do s <- position
278 let (dir, file) = splitFileName (fileName s)
279 let f = if dir == addTrailingPathSeparator "." then file else fileName s
280 return $ FC f (lineNum s)
283-- | Bind constraints to term
284bindList :: (Name -> PTerm -> PTerm -> PTerm) -> [(Name, PTerm)] -> PTerm -> PTerm
286bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
288{- |Creates table for fixtiy declarations to build expression parser using
289 pre-build and user-defined operator/fixity declarations -}
290table :: [FixDecl] -> OperatorTable IdrisParser PTerm
292 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
293 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]
294 ++ toTable (reverse fixes) ++
296 [binary "=" PEq AssocLeft],
297 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
299{- |Calculates table for fixtiy declarations -}
300toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm
301toTable fs = map (map toBin)
302 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
303 where toBin (Fix (PrefixN _) op) = prefix op
304 (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
306 = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
307 assoc (Infixl _) = AssocLeft
308 assoc (Infixr _) = AssocRight
309 assoc (InfixN _) = AssocNone
311{- |Binary operator -}
312binary :: String -> (FC -> PTerm -> PTerm -> PTerm) -> Assoc -> Operator IdrisParser PTerm
313binary name f = Infix (do fc <- getFC
315 doc <- option "" (docComment '^')
318{- |Prefix operator -}
319prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm
320prefix name f = Prefix (do reservedOp name
324{- |Backtick operator -}
325backtick :: Operator IdrisParser PTerm
326backtick = Infix (do lchar '`'; n <- fnName
329 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
331-- | Allow implicit type declarations
332allowImp :: SyntaxInfo -> SyntaxInfo
333allowImp syn = syn { implicitAllowed = True }
335-- | Disallow implicit type declarations
336disallowImp :: SyntaxInfo -> SyntaxInfo
337disallowImp syn = syn { implicitAllowed = False }
339-- | Adds accessibility option for function
340addAcc :: Name -> Maybe Accessibility -> IdrisParser ()
341addAcc n a = do i <- get
342 put (i { hide_list = (n, a) : hide_list i })
344{- | Add accessbility option for data declarations
345 (works for classes too - 'abstract' means the data/class is visible but members not) -}
346accData :: Maybe Accessibility -> Name -> [Name] -> IdrisParser ()
347accData (Just Frozen) n ns = do addAcc n (Just Frozen)
348 mapM_ (\n -> addAcc n (Just Hidden)) ns
349accData a n ns = do addAcc n a
350 mapM_ (`addAcc` a) ns
353{- * Error reporting helpers -}
354{- | Error message with possible fixes list -}
355fixErrorMsg :: String -> [String] -> String
356fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)
358{- * Layout helpers -}
360-- | Push indentation to stack
361pushIndent :: IdrisParser ()
362pushIndent = do pos <- position
364 put (ist { indent_stack = (fromIntegral (column pos) + 1) : indent_stack ist })
366-- | Pops indentation from stack
367popIndent :: IdrisParser ()
368popIndent = do ist <- get
369 let (x : xs) = indent_stack ist
370 put (ist { indent_stack = xs })
372-- | Gets current indentation
373indent :: IdrisParser Int
374indent = liftM ((+1) . fromIntegral . column) position
376-- | Gets last indentation
377lastIndent :: IdrisParser Int
378lastIndent = do ist <- get
379 case indent_stack ist of
383-- | Applies parser in an indented position
384indented :: IdrisParser a -> IdrisParser a
385indented p = notEndBlock *> p <* keepTerminator
387-- | Applies parser to get a block (which has possibly indented statements)
388indentedBlock :: IdrisParser a -> IdrisParser [a]
389indentedBlock p = do openBlock
391 res <- many (indented p)
396-- | Applies parser to get a block with at least one statement (which has possibly indented statements)
397indentedBlock1 :: IdrisParser a -> IdrisParser [a]
398indentedBlock1 p = do openBlock
400 res <- some (indented p)
405-- | Applies parser to get a block with exactly one (possibly indented) statement
406indentedBlockS :: IdrisParser a -> IdrisParser a
407indentedBlockS p = do openBlock
415-- | Checks if the following character matches provided parser
416lookAheadMatches :: MonadicParsing m => m a -> m Bool
417lookAheadMatches p = do match <- lookAhead (optional p)
418 return $ isJust match
420-- | Parses a start of block
421openBlock :: IdrisParser ()
422openBlock = do lchar '{'
424 put (ist { brace_stack = Nothing : brace_stack ist })
427 -- if we're not indented further, it's an empty block, so
428 -- increment lvl to ensure we get to the end
429 let lvl = case brace_stack ist of
431 if lvl' <= lvl_old then lvl_old+1
433 [] -> if lvl' == 1 then 2 else lvl'
435 put (ist { brace_stack = Just lvl : brace_stack ist })
438-- | Parses an end of block
439closeBlock :: IdrisParser ()
440closeBlock = do ist <- get
441 bs <- case brace_stack ist of
442 [] -> eof >> return []
443 Nothing : xs -> lchar '}' >> return xs <?> "end of block"
444 Just lvl : xs -> (do i <- indent
445 isParen <- lookAheadMatches (char ')')
446 if i >= lvl && not isParen
447 then fail "not end of block"
449 <|> (do notOpenBraces
452 put (ist { brace_stack = bs })
454-- | Parses a terminator
455terminator :: IdrisParser ()
456terminator = do lchar ';'; popIndent
457 <|> do c <- indent; l <- lastIndent
458 if c <= l then popIndent else fail "not a terminator"
459 <|> do isParen <- lookAheadMatches (oneOf ")}")
460 if isParen then popIndent else fail "not a termiantor"
463-- | Parses and keeps a terminator
464keepTerminator :: IdrisParser ()
465keepTerminator = do lchar ';'; return ()
466 <|> do c <- indent; l <- lastIndent
467 unless (c <= l) $ fail "not a terminator"
468 <|> do isParen <- lookAheadMatches (oneOf ")}|")
469 unless isParen $ fail "not a terminator"
472-- | Checks if application expression does not end
473notEndApp :: IdrisParser ()
474notEndApp = do c <- indent; l <- lastIndent
475 when (c <= l) (fail "terminator")
477-- | Checks that it is not end of block
478notEndBlock :: IdrisParser ()
479notEndBlock = do ist <- get
480 case brace_stack ist of
481 Just lvl : xs -> do i <- indent
482 isParen <- lookAheadMatches (char ')')
483 when (i < lvl || isParen) (fail "end of block")
486notOpenBraces :: IdrisParser ()
487notOpenBraces = do ist <- get
488 when (hasNothing $ brace_stack ist) $ fail "end of input"
489 where hasNothing :: [Maybe a] -> Bool
490 hasNothing = any isNothing
494{- | Parses module definition
495 ModuleHeader ::= 'module' Identifier_t ';'?;
497moduleHeader :: IdrisParser [String]
498moduleHeader = try (do reserved "module"
500 option ';' (lchar ';')
501 return (moduleName i))
503 where moduleName x = case span (/='.') x of
505 (x, '.':y) -> x : moduleName y
507{- | Parses an import statement
508 Import ::= 'import' Identifier_t ';'?;
510import_ :: IdrisParser String
511import_ = do reserved "import"
513 option ';' (lchar ';')
515 <?> "import statement"
516 where toPath f = foldl1' (</>) (Spl.splitOn "." f)
518{- | Parses program source
521prog :: SyntaxInfo -> IdrisParser [PDecl]
522prog syn = do whiteSpace
523 decls <- many (decl syn)
526 let c = (concat decls)
529{- | Parses a top-level declaration
545decl :: SyntaxInfo -> IdrisParser [PDecl]
546decl syn = do notEndBlock
548 where declBody :: IdrisParser [PDecl]
556 <|> do d <- dsl syn; return [d]
560 <|> do import_; fail "imports must be at top of file"
562 declBody' :: IdrisParser [PDecl]
563 declBody' = do d <- decl' syn
565 let d' = fmap (desugar syn i) d
568{- | Parses a top-level declaration with possible syntax sugar
577decl' :: SyntaxInfo -> IdrisParser PDecl
585{- | Parses a syntax extension declaration (and adds the rule to parser state)
586 SyntaxDecl ::= SyntaxRule;
588syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
589syntaxDecl syn = do s <- syntaxRule syn
591 let rs = syntax_rules i
592 let ns = syntax_keywords i
593 let ibc = ibc_write i
594 let ks = map show (names s)
595 put (i { syntax_rules = s : rs,
596 syntax_keywords = ks ++ ns,
597 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc })
599 return (PSyntax fc s)
600 where names (Rule syms _ _) = mapMaybe ename syms
601 ename (Keyword n) = Just n
604{- | Parses a syntax extension declaration
605SyntaxRuleOpts ::= 'term' | 'pattern';
608 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
610SyntaxSym ::= '[' Name_t ']'
616syntaxRule :: SyntaxInfo -> IdrisParser Syntax
620 sty <- option AnySyntax (do reserved "term"; return TermSyntax
621 <|> do reserved "pattern"; return PatternSyntax)
624 syms <- some syntaxSym
625 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
626 let ns = mapMaybe getName syms
627 when (length ns /= length (nub ns))
628 $ unexpected "repeated variable in syntax rule"
630 tm <- typeExpr (allowImp syn)
632 return (Rule (mkSimple syms) tm sty)
634 isExpr (Expr _) = True
636 getName (Expr n) = Just n
638 -- Can't parse two full expressions (i.e. expressions with application) in a row
639 -- so change them both to a simple expression
640 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
641 mkSimple xs = mkSimple' xs
643 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
645 mkSimple' (e : es) = e : mkSimple' es
649{- | Parses a syntax symbol (either binding variable, keyword or expression)
650SyntaxSym ::= '[' Name_t ']'
656syntaxSym :: IdrisParser SSymbol
657syntaxSym = try (do lchar '['; n <- name; lchar ']'
659 <|> try (do lchar '{'; n <- name; lchar '}'
663 <|> do sym <- stringLiteral
667{- | Parses a function declaration with possible syntax sugar
668 FunDecl ::= FunDecl';
670fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
672 = try (do notEndBlock
675 let d' = fmap (desugar syn i) d
677 <?> "function declaration"
679{- Parses a function declaration
681 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
687fnDecl' :: SyntaxInfo -> IdrisParser PDecl
688fnDecl' syn = try (do doc <- option "" (docComment '|')
691 let initOpts = if default_total ist
694 opts <- fnOpts initOpts
695 acc <- optional accessibility
698 let n = expandNS syn n_in
700 ty <- typeSig (allowImp syn)
703 return (PTy doc syn fc opts' n ty))
707 <?> "function declaration"
710{- Parses function options given initial options
716 | '%' 'specialise' '[' NameTimesList? ']'
719NameTimes ::= FnName Natural?;
723 | NameTimes ',' NameTimesList
727-- FIXME: Check compatability for function options (i.e. partal/total)
728fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
730 = do reserved "total"; fnOpts (TotalFn : opts)
731 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
732 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;
733 fnOpts (CExport c : opts)
734 <|> do try (lchar '%' *> reserved "assert_total");
735 fnOpts (AssertTotal : opts)
736 <|> do try (lchar '%' *> reserved "reflection");
737 fnOpts (Reflection : opts)
738 <|> do lchar '%'; reserved "specialise";
739 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
740 fnOpts (Specialise ns : opts)
741 <|> do reserved "implicit"; fnOpts (Implicit : opts)
743 <?> "function modifier"
744 where nameTimes :: IdrisParser (Name, Maybe Int)
745 nameTimes = do n <- fnName
746 t <- option Nothing (do reds <- natural
747 return (Just (fromInteger reds)))
750{- | Parses an operator in function position i.e. enclosed by `()', with an
753 OperatorFront ::= (Identifier_t '.')? '(' Operator_t ')';
755operatorFront :: IdrisParser Name
756operatorFront = maybeWithNS (lchar '(' *> operator <* lchar ')') False []
758{- | Parses a function (either normal name or operator)
759 FnName ::= Name | OperatorFront;
761fnName :: IdrisParser Name
762fnName = try operatorFront <|> name <?> "function name"
764{- | Parses an accessibilty modifier (e.g. public, private) -}
765accessibility :: IdrisParser Accessibility
766accessibility = do reserved "public"; return Public
767 <|> do reserved "abstract"; return Frozen
768 <|> do reserved "private"; return Hidden
769 <?> "accessibility modifier"
773{- | Parses a postulate
776 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
779postulate :: SyntaxInfo -> IdrisParser PDecl
780postulate syn = do doc <- try $ do doc <- option "" (docComment '|')
785 let initOpts = if default_total ist
788 opts <- fnOpts initOpts
789 acc <- optional accessibility
792 let n = expandNS syn n_in
793 ty <- typeSig (allowImp syn)
797 return (PPostulate doc syn fc opts' n ty)
800{- | Parses a using declaration
803 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
806using_ :: SyntaxInfo -> IdrisParser [PDecl]
808 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
810 let uvars = using syn
811 ds <- many (decl (syn { using = uvars ++ ns }))
814 <?> "using declaration"
816{- | Parses a parameters declaration
819 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
822params :: SyntaxInfo -> IdrisParser [PDecl]
824 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
826 let pvars = syn_params syn
827 ds <- many (decl syn { syn_params = pvars ++ ns })
830 return [PParams fc ns (concat ds)]
831 <?> "parameters declaration"
833{- | Parses a mutual declaration (for mutually recursive functions)
836 'mutual' OpenBlock Decl* CloseBlock
839mutual :: SyntaxInfo -> IdrisParser [PDecl]
843 let pvars = syn_params syn
844 ds <- many (decl syn)
847 return [PMutual fc (concat ds)]
850{- | Parses a namespace declaration
853 'namespace' identifier OpenBlock Decl+ CloseBlock
856namespace :: SyntaxInfo -> IdrisParser [PDecl]
858 do reserved "namespace"; n <- identifier;
860 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
862 return [PNamespace n (concat ds)]
863 <?> "namespace declaration"
865{- | Parses a fixity declaration
868 FixityType Natural_t OperatorList Terminator
871fixity :: IdrisParser PDecl
872fixity = do pushIndent
873 f <- fixityType; i <- natural; ops <- sepBy1 operator (lchar ',')
875 let prec = fromInteger i
877 let infixes = idris_infixes istate
878 let fs = map (Fix (f prec)) ops
879 let redecls = map (alreadyDeclared infixes) fs
880 let ill = filter (not . checkValidity) redecls
882 then do put (istate { idris_infixes = nub $ sort (fs ++ infixes)
883 , ibc_write = map IBCFix fs ++ ibc_write istate
886 return (PFix fc (f prec) ops)
887 else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
888 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
889 <?> "fixity declaration"
890 where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
891 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
893 checkValidity :: (FixDecl, [FixDecl]) -> Bool
894 checkValidity (f, fs) = all (== f) fs
896 extractName :: FixDecl -> String
897 extractName (Fix _ n) = n
899{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)
907fixityType :: IdrisParser (Int -> Fixity)
908fixityType = do reserved "infixl"; return Infixl
909 <|> do reserved "infixr"; return Infixr
910 <|> do reserved "infix"; return InfixN
911 <|> do reserved "prefix"; return PrefixN
914{- |Parses a methods block (for type classes and instances)
915 MethodsBlock ::= 'where' OpenBlock FnDecl* CloseBlock
917methodsBlock :: SyntaxInfo -> IdrisParser [PDecl]
918methodsBlock syn = do reserved "where"
920 ds <- many (fnDecl syn)
925{- |Parses a type class declaration
929 | '(' Name ':' Expr ')'
933 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* MethodsBlock?
936class_ :: SyntaxInfo -> IdrisParser [PDecl]
937class_ syn = do (doc, acc) <- try (do
938 doc <- option "" (docComment '|')
939 acc <- optional accessibility
941 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- name
942 let n = expandNS syn n_in
944 ds <- option [] (methodsBlock syn)
945 accData acc n (concatMap declared ds)
946 return [PClass doc syn fc cons n cs ds]
947 <?> "type-class declaration"
949 carg :: IdrisParser (Name, PTerm)
950 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
955{- |Parses a type class instance declaration
958 'instance' InstanceName? ConstraintList? Name SimpleExpr* MethodsBlock?
961 InstanceName ::= '[' Name ']';
963instance_ :: SyntaxInfo -> IdrisParser [PDecl]
964instance_ syn = do reserved "instance"; fc <- getFC
965 en <- optional instanceName
966 cs <- constraintList syn
968 args <- many (simpleExpr syn)
969 let sc = PApp fc (PRef fc cn) (map pexp args)
970 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
971 ds <- option [] (methodsBlock syn)
972 return [PInstance syn fc cs cn args t en ds]
973 <?> "instance declaratioN"
974 where instanceName :: IdrisParser Name
975 instanceName = do lchar '['; n_in <- fnName; lchar ']'
976 let n = expandNS syn n_in
981{- | Parses an expression as a whole
982 FullExpr ::= Expr EOF_t;
984fullExpr :: SyntaxInfo -> IdrisParser PTerm
985fullExpr syn = do x <- expr syn
988 return $ desugar syn i x
991{- |Parses an expression
994expr :: SyntaxInfo -> IdrisParser PTerm
995expr syn = do i <- get
996 buildExpressionParser (table (idris_infixes i)) (expr' syn)
998{- | Parses either an internally defined expression or
1001Expr' ::= "External (User-defined) Syntax"
1005expr' :: SyntaxInfo -> IdrisParser PTerm
1006expr' syn = try (externalExpr syn)
1007 <|> internalExpr syn
1010{- | Parses a user-defined expression -}
1011externalExpr :: SyntaxInfo -> IdrisParser PTerm
1012externalExpr syn = do i <- get
1013 extensions syn (syntax_rules i)
1014 <?> "user-defined expression"
1016{- | Parses a simple user-defined expression -}
1017simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm
1018simpleExternalExpr syn = do i <- get
1019 extensions syn (filter isSimple (syntax_rules i))
1021 isSimple (Rule (Expr x:xs) _ _) = False
1022 isSimple (Rule (SimpleExpr x:xs) _ _) = False
1023 isSimple (Rule [Keyword _] _ _) = True
1024 isSimple (Rule [Symbol _] _ _) = True
1025 isSimple (Rule (_:xs) _ _) = case last xs of
1031{- | Tries to parse a user-defined expression given a list of syntactic extensions -}
1032extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm
1033extensions syn rules = choice (map (try . extension syn) (filter isValid rules))
1034 <?> "user-defined expression"
1036 isValid :: Syntax -> Bool
1037 isValid (Rule _ _ AnySyntax) = True
1038 isValid (Rule _ _ PatternSyntax) = inPattern syn
1039 isValid (Rule _ _ TermSyntax) = not (inPattern syn)
1042data SynMatch = SynTm PTerm | SynBind Name
1044{- | Tries to parse an expression given a user-defined rule -}
1045extension :: SyntaxInfo -> Syntax -> IdrisParser PTerm
1046extension syn (Rule ssym ptm _)
1047 = do smap <- mapM extensionSymbol ssym
1048 let ns = mapMaybe id smap
1049 return (update ns ptm) -- updated with smap
1051 extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
1052 extensionSymbol (Keyword n) = do reserved (show n); return Nothing
1053 extensionSymbol (Expr n) = do tm <- expr syn
1054 return $ Just (n, SynTm tm)
1055 extensionSymbol (SimpleExpr n) = do tm <- simpleExpr syn
1056 return $ Just (n, SynTm tm)
1057 extensionSymbol (Binding n) = do b <- name
1058 return $ Just (n, SynBind b)
1059 extensionSymbol (Symbol s) = do symbol s
1061 dropn :: Name -> [(Name, a)] -> [(Name, a)]
1063 dropn n ((x,t) : xs) | n == x = xs
1064 | otherwise = (x,t):dropn n xs
1066 updateB :: [(Name, SynMatch)] -> Name -> Name
1067 updateB ns n = case lookup n ns of
1068 Just (SynBind t) -> t
1071 update :: [(Name, SynMatch)] -> PTerm -> PTerm
1072 update ns (PRef fc n) = case lookup n ns of
1075 update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)
1076 update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc)
1077 update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)
1078 (update (dropn n ns) sc)
1079 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
1080 update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)
1081 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)
1082 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)
1083 update ns (PAlternative a as) = PAlternative a (map (update ns) as)
1084 update ns (PHidden t) = PHidden (update ns t)
1085 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
1086 where upd :: [(Name, SynMatch)] -> [PDo] -> [PDo]
1087 upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
1088 upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds
1089 upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)
1090 : upd (dropn n ns) ds
1091 upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t)
1093 upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)
1095 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
1098{- |Parses a (normal) built-in expression
1114internalExpr :: SyntaxInfo -> IdrisParser PTerm
1117 <|> try (matchApp syn)
1118 <|> try (unifyLog syn)
1120 <|> try (simpleExpr syn)
1129{- | Parses a case expression
1131 'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;
1133caseExpr :: SyntaxInfo -> IdrisParser PTerm
1134caseExpr syn = do reserved "case"; fc <- getFC
1135 scr <- expr syn; reserved "of";
1136 opts <- indentedBlock1 (caseOption syn)
1137 return (PCase fc scr opts)
1138 <?> "case expression"
1140{- | Parses a case in a case expression
1142 Expr '=>' Expr Terminator
1145caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
1146caseOption syn = do lhs <- expr (syn { inPattern = True })
1147 symbol "=>"; r <- expr syn
1151{- | Parses a proof block
1153 'proof' OpenBlock Tactic'* CloseBlock
1156proofExpr :: SyntaxInfo -> IdrisParser PTerm
1157proofExpr syn = do reserved "proof"
1158 ts <- indentedBlock (tactic syn)
1162{- | Parses a tactics block
1164 'tactics' OpenBlock Tactic'* CloseBlock
1167tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
1168tacticsExpr syn = do reserved "tactics"
1169 ts <- indentedBlock (tactic syn)
1170 return $ PTactics ts
1173{- | Parses a simple expresion
1178 | 'refl' ('{' Expr '}')?
1193 | {- External (User-defined) Simple Expression -}
1196simpleExpr :: SyntaxInfo -> IdrisParser PTerm
1198 {-try (do symbol "!["; t <- term; lchar ']'; return $ PQuote t)
1199 <|>-} do lchar '?'; x <- name; return (PMetavar x)
1200 <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)
1201 <|> do reserved "refl"; fc <- getFC;
1202 tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';
1204 return (PRefl fc tm)
1208 <|> try (do fc <- getFC
1211 <|> try (listExpr syn)
1212 <|> try (comprehension syn)
1215 <|> try (do lchar '('
1216 bracketed (disallowImp syn))
1217 <|> try (do c <- constant
1219 return (modifyConst syn fc (PConstant c)))
1220 <|> do reserved "Type"; return PType
1221 <|> try (do symbol "()"
1224 <|> try (do symbol "_|_"
1227 <|> do lchar '_'; return Placeholder
1228 <|> simpleExternalExpr syn
1232{- |Parses the rest of an expression in braces
1240bracketed :: SyntaxInfo -> IdrisParser PTerm
1243 <|> try (do e <- expr syn; lchar ')'; return e)
1244 <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
1245 return $ PLam (MN 1000 "ARG") Placeholder
1246 (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),
1248 <|> try (do fc <- getFC; e <- simpleExpr syn; o <- operator; lchar ')'
1249 return $ PLam (MN 1000 "ARG") Placeholder
1250 (PApp fc (PRef fc (UN o)) [pexp e,
1251 pexp (PRef fc (MN 1000 "ARG"))]))
1252 <?> "end of expression in braces"
1254-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
1255-- big integer, otherwise try fromInteger and the constants as alternatives.
1256-- a better solution would be to fix fromInteger to work with Integer, as the
1257-- name suggests, rather than Int
1258{-| Finds optimal type for integer constant -}
1259modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
1260modifyConst syn fc (PConstant (BI x))
1261 | not (inPattern syn)
1262 = PAlternative False
1263 (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI (fromInteger x)))]
1265 | otherwise = PAlternative False consts
1267 consts = [ PConstant (BI x)
1268 , PConstant (I (fromInteger x))
1269 , PConstant (B8 (fromInteger x))
1270 , PConstant (B16 (fromInteger x))
1271 , PConstant (B32 (fromInteger x))
1272 , PConstant (B64 (fromInteger x))
1274modifyConst syn fc x = x
1276{- | Parses a list literal expression e.g. [1,2,3]
1287listExpr :: SyntaxInfo -> IdrisParser PTerm
1288listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lchar ']'
1289 return (mkList fc xs)
1290 <?> "list expression"
1292 mkList :: FC -> [PTerm] -> PTerm
1293 mkList fc [] = PRef fc (UN "Nil")
1294 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
1296{- | Parses rest of pair expression
1300 | Name ':' Expr '**' 'Expr' ')'
1313pair :: SyntaxInfo -> IdrisParser PTerm
1314pair syn = try (do l <- expr syn
1319 [Left r] -> return (PPair fc l r)
1320 [Right r] -> return (PDPair fc l Placeholder r))
1321 <|> try (do x <- ntuple
1324 <|> do ln <- name; lchar ':'
1330 return (PDPair fc (PRef fc ln) lty r)
1331 <?> "pair expression"
1333 restTuple :: IdrisParser [Either PTerm PTerm]
1334 restTuple = do lchar ')'; return []
1339 <|> do reservedOp "**"
1343 <?> "end of pair expression"
1344 ntuple :: IdrisParser PTerm
1345 ntuple = try (do l <- expr syn; fc <- getFC; lchar ','
1347 return (PPair fc l rest))
1348 <|> (do l <- expr syn; fc <- getFC; lchar ','
1350 return (PPair fc l r))
1351 <?> "tuple expression"
1353{- | Parses an alternative expression
1354 Alt ::= '(|' Expr_List '|)';
1358 | Expr' ',' Expr_List
1361alt :: SyntaxInfo -> IdrisParser PTerm
1362alt syn = do symbol "(|"; alts <- sepBy1 (expr' syn) (lchar ','); symbol "|)"
1363 return (PAlternative False alts)
1365{- | Parses a possibly hidden simple expression
1371hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm
1379{- | Parses a matching application expression
1381 SimpleExpr '<==' FnName
1384matchApp :: SyntaxInfo -> IdrisParser PTerm
1385matchApp syn = do ty <- simpleExpr syn
1389 return (PLet (MN 0 "match")
1392 (PRef fc (MN 0 "match")))
1393 <?> "matching application expression"
1395{- | Parses a unification log expression
1397 '%' 'unifyLog' SimpleExpr
1400unifyLog :: SyntaxInfo -> IdrisParser PTerm
1401unifyLog syn = do lchar '%'; reserved "unifyLog";
1402 tm <- simpleExpr syn
1403 return (PUnifyLog tm)
1404 <?> "unification log expression"
1406{- | Parses a function application expression
1408 'mkForeign' Arg Arg*
1412app :: SyntaxInfo -> IdrisParser PTerm
1413app syn = do f <- reserved "mkForeign"
1416 args <- many (do notEndApp; arg syn)
1418 -- mkForeign f args ==>
1419 -- liftPrimIO (\w => mkForeignPrim f args w)
1420 let ap = PApp fc (PRef fc (UN "liftPrimIO"))
1421 [pexp (PLam (MN 0 "w")
1423 (PApp fc (PRef fc (UN "mkForeignPrim"))
1425 [pexp (PRef fc (MN 0 "w"))])))]
1426 return (dslify i ap)
1428 <|> do f <- simpleExpr syn
1430 args <- some (do notEndApp; arg syn)
1432 return (dslify i $ PApp fc f args)
1433 <?> "function application"
1435 dslify :: IState -> PTerm -> PTerm
1436 dslify i (PApp fc (PRef _ f) [a])
1437 | [d] <- lookupCtxt f (idris_dsls i)
1438 = desugar (syn { dsl_info = d }) i (getTm a)
1441{- |Parses a function argument
1448arg :: SyntaxInfo -> IdrisParser PArg
1449arg syn = implicitArg syn
1450 <|> constraintArg syn
1451 <|> do e <- simpleExpr syn
1453 <?> "function argument"
1455{- |Parses an implicit function argument
1457 '{' Name ('=' Expr)? '}'
1460implicitArg :: SyntaxInfo -> IdrisParser PArg
1461implicitArg syn = do lchar '{'
1464 v <- option (PRef fc n) (do lchar '='
1468 <?> "implicit function argument"
1470{- |Parses a constraint argument (for selecting a named type class instance)
1475constraintArg :: SyntaxInfo -> IdrisParser PArg
1476constraintArg syn = do symbol "@{"
1480 <?> "constraint argument"
1483{- |Parses a record field setter expression
1485 'record' '{' FieldTypeList '}';
1489 | FieldType ',' FieldTypeList
1496recordType :: SyntaxInfo -> IdrisParser PTerm
1498 = do reserved "record"
1500 fields <- sepBy1 fieldType (lchar ',')
1503 rec <- optional (simpleExpr syn)
1506 return (PLam (MN 0 "fldx") Placeholder
1507 (applyAll fc fields (PRef fc (MN 0 "fldx"))))
1508 Just v -> return (applyAll fc fields v)
1509 <?> "record setting expression"
1510 where fieldType :: IdrisParser (Name, PTerm)
1511 fieldType = do n <- fnName
1516 applyAll :: FC -> [(Name, PTerm)] -> PTerm -> PTerm
1517 applyAll fc [] x = x
1518 applyAll fc ((n, e) : es) x
1519 = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])
1521{- |Creates setters for record types on necessary functions -}
1522mkType :: Name -> Name
1523mkType (UN n) = UN ("set_" ++ n)
1524mkType (MN 0 n) = MN 0 ("set_" ++ n)
1525mkType (NS n s) = NS (mkType n) s
1527{- |Parses a type for an expression
1532typeSig :: SyntaxInfo -> IdrisParser PTerm
1533typeSig syn = lchar ':' *> typeExpr syn <?> "type"
1535{- |Parses a type signature
1536TypeExpr ::= ConstraintList? Expr;
1538typeExpr :: SyntaxInfo -> IdrisParser PTerm
1539typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []
1541 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
1542 <?> "type signature"
1544{- |Parses a lambda expression
1546 '\\' TypeOptDeclList '=>' Expr
1547 | '\\' SimpleExprList '=>' Expr
1551 | SimpleExpr ',' SimpleExprList
1554lambda :: SyntaxInfo -> IdrisParser PTerm
1555lambda syn = do lchar '\\'
1556 try (do xt <- tyOptDeclList syn
1559 return (bindList PLam xt sc)
1560 <|> (do ps <- sepBy (do fc <- getFC
1562 return (fc, e)) (lchar ',')
1565 return (pmList (zip [0..] ps) sc)))
1566 <?> "lambda expression"
1567 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm
1569 pmList ((i, (fc, x)) : xs) sc
1570 = PLam (MN i "lamp") Placeholder
1571 (PCase fc (PRef fc (MN i "lamp"))
1572 [(x, pmList xs sc)])
1574{- |Parses a term rewrite expression
1576 'rewrite' Expr ('==>' Expr)? 'in' Expr
1579rewriteTerm :: SyntaxInfo -> IdrisParser PTerm
1580rewriteTerm syn = do reserved "rewrite"
1583 giving <- optional (do symbol "==>"; expr' syn)
1584 reserved "in"; sc <- expr syn
1586 (PApp fc (PRef fc (UN "sym")) [pexp prf]) sc
1588 <?> "term rewrite expression"
1590{- |Parses a let binding
1592 'let' Name TypeSig'? '=' Expr 'in' Expr
1593| 'let' Expr' '=' Expr' 'in' Expr
1599let_ :: SyntaxInfo -> IdrisParser PTerm
1600let_ syn = try (do reserved "let"; n <- name;
1601 ty <- option Placeholder (do lchar ':'; expr' syn)
1604 reserved "in"; sc <- expr syn
1605 return (PLet n ty v sc))
1606 <|> (do reserved "let"; fc <- getFC; pat <- expr' (syn { inPattern = True } )
1607 symbol "="; v <- expr syn
1608 reserved "in"; sc <- expr syn
1609 return (PCase fc v [(pat, sc)]))
1612{- |Parses a quote goal
1614 'quoteGoal' Name 'by' Expr 'in' Expr
1617quoteGoal :: SyntaxInfo -> IdrisParser PTerm
1618quoteGoal syn = do reserved "quoteGoal"; n <- name;
1624 return (PGoal fc r n sc)
1625 <?> "quote goal expression"
1627{- |Parses a dependent type signature
1629 '|'? Static? '(' TypeDeclList ')' DocComment '->' Expr
1630 | '|'? Static? '{' TypeDeclList '}' '->' Expr
1631 | '{' 'auto' TypeDeclList '}' '->' Expr
1632 | '{' 'default' TypeDeclList '}' '->' Expr
1633 | '{' 'static' '}' Expr' '->' Expr
1637 try (do lazy <- if implicitAllowed syn -- laziness is top level only
1638 then option False (do lchar '|'; return True)
1641 lchar '('; xt <- typeDeclList syn; lchar ')'
1642 doc <- option "" (docComment '^')
1645 return (bindList (PPi (Exp lazy st doc)) xt sc))
1646 <|> try (if implicitAllowed syn
1647 then do lazy <- option False (do lchar '|'
1651 xt <- typeDeclList syn
1655 return (bindList (PPi (Imp lazy st "")) xt sc)
1656 else fail "no implicit arguments allowed here")
1657 <|> try (do lchar '{'
1659 xt <- typeDeclList syn
1663 return (bindList (PPi
1664 (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))
1665 <|> try (do lchar '{'
1667 script <- simpleExpr syn
1668 xt <- typeDeclList syn
1672 return (bindList (PPi (TacImp False Dynamic script "")) xt sc))
1679 return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)
1680 <?> "dependent type signature"
1682{- | Parses a type constraint list
1684 '(' Expr_List ')' '=>'
1688constraintList :: SyntaxInfo -> IdrisParser [PTerm]
1689constraintList syn = try (do lchar '('
1690 tys <- sepBy1 (expr' (disallowImp syn)) (lchar ',')
1694 <|> try (do t <- expr (disallowImp syn)
1698 <?> "type constraint list"
1700{- | Parses a using declaration list
1708 | UsingDecl ',' UsingDeclList'
1716usingDeclList :: SyntaxInfo -> IdrisParser [Using]
1718 = try (sepBy1 (usingDecl syn) (lchar ','))
1719 <|> do ns <- sepBy1 name (lchar ',')
1720 t <- typeSig (disallowImp syn)
1721 return (map (\x -> UImplicit x t) ns)
1722 <?> "using declaration list"
1724{- |Parses a using declaration
1730usingDecl :: SyntaxInfo -> IdrisParser Using
1731usingDecl syn = try (do x <- fnName
1732 t <- typeSig (disallowImp syn)
1733 return (UImplicit x t))
1736 return (UConstraint c xs)
1737 <?> "using declaration"
1739{- |Parses a type declaration list
1741 FunctionSignatureList
1745FunctionSignatureList ::=
1747 | Name TypeSig ',' FunctionSignatureList
1750typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
1751typeDeclList syn = try (sepBy1 (do x <- fnName
1752 t <- typeSig (disallowImp syn)
1755 <|> do ns <- sepBy1 name (lchar ',')
1756 t <- typeSig (disallowImp syn)
1757 return (map (\x -> (x, t)) ns)
1758 <?> "type declaration list"
1760{- |Parses a type declaration list with optional parameters
1762 NameOrPlaceholder TypeSig?
1763 | NameOrPlaceholder TypeSig? ',' TypeOptDeclList
1766NameOrPlaceHolder ::= Name | '_';
1768tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
1769tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder
1770 t <- option Placeholder (do lchar ':'
1774 <?> "type declaration list"
1775 where nameOrPlaceholder :: IdrisParser Name
1776 nameOrPlaceholder = fnName
1778 return (MN 0 "underscore")
1779 <?> "name or placeholder"
1781{- |Parses a list comprehension
1782Comprehension ::= '[' Expr '|' DoList ']';
1789comprehension :: SyntaxInfo -> IdrisParser PTerm
1795 qs <- sepBy1 (do_ syn) (lchar ',')
1797 return (PDoBlock (map addGuard qs ++
1798 [DoExp fc (PApp fc (PRef fc (UN "return"))
1800 <?> "list comprehension"
1801 where addGuard :: PDo -> PDo
1802 addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
1806{- |Parses a do-block
1807Do' ::= Do KeepTerminator;
1810 'do' OpenBlock Do'+ CloseBlock
1813doBlock :: SyntaxInfo -> IdrisParser PTerm
1816 ds <- indentedBlock (do_ syn)
1817 return (PDoBlock ds)
1820{- |Parses an expression inside a do block
1822 'let' Name TypeSig'? '=' Expr
1823 | 'let' Expr' '=' Expr
1829do_ :: SyntaxInfo -> IdrisParser PDo
1831 = try (do reserved "let"
1833 ty <- option Placeholder (do lchar ':'
1838 return (DoLet fc i ty e))
1839 <|> try (do reserved "let"
1844 return (DoLetP fc i sc))
1845 <|> try (do i <- name
1849 return (DoBind fc i e))
1850 <|> try (do i <- expr' syn
1854 return (DoBindP fc i e))
1855 <|> do e <- expr syn
1858 <?> "do block expression"
1860{- |Parses an expression in idiom brackets
1861Idiom ::= '[|' Expr '|]';
1863idiom :: SyntaxInfo -> IdrisParser PTerm
1869 return (PIdiom fc e)
1870 <?> "expression in idiom brackets"
1872{- |Parses a constant or literal expression
1894constant :: IdrisParser Core.TT.Const
1895constant = do reserved "Integer";return (AType (ATInt ITBig))
1896 <|> do reserved "Int"; return (AType (ATInt ITNative))
1897 <|> do reserved "Char"; return (AType (ATInt ITChar))
1898 <|> do reserved "Float"; return (AType ATFloat)
1899 <|> do reserved "String"; return StrType
1900 <|> do reserved "Ptr"; return PtrType
1901 <|> do reserved "Bits8"; return (AType (ATInt (ITFixed IT8)))
1902 <|> do reserved "Bits16"; return (AType (ATInt (ITFixed IT16)))
1903 <|> do reserved "Bits32"; return (AType (ATInt (ITFixed IT32)))
1904 <|> do reserved "Bits64"; return (AType (ATInt (ITFixed IT64)))
1905 <|> do reserved "Bits8x16"; return (AType (ATInt (ITVec IT8 16)))
1906 <|> do reserved "Bits16x8"; return (AType (ATInt (ITVec IT16 8)))
1907 <|> do reserved "Bits32x4"; return (AType (ATInt (ITVec IT32 4)))
1908 <|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2)))
1909 <|> try (do f <- float; return $ Fl f)
1910 <|> try (do i <- natural; return $ BI i)
1911 <|> try (do s <- stringLiteral; return $ Str s)
1912 <|> try (do c <- charLiteral; return $ Ch c)
1913 <?> "constant or literal"
1915{- |Parses a static modifier
1920static :: IdrisParser Static
1921static = do lchar '['; reserved "static"; lchar ']'; return Static
1923 <?> "static modifier"
1925{- |Parses a record type declaration
1927 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
1929record :: SyntaxInfo -> IdrisParser PDecl
1930record syn = do (doc, acc) <- try (do
1931 doc <- option "" (docComment '|')
1932 acc <- optional accessibility
1937 ty <- typeSig (allowImp syn)
1938 let tyn = expandNS syn tyn_in
1940 (cdoc, cn, cty, _) <- indentedBlockS (constructor syn)
1941 accData acc tyn [cn]
1942 let rsyn = syn { syn_namespace = show (nsroot tyn) :
1944 let fns = getRecNames rsyn cty
1945 mapM_ (\n -> addAcc n acc) fns
1946 return $ PRecord doc rsyn fc tyn ty cdoc cn cty
1947 <?> "record type declaration"
1949 getRecNames :: SyntaxInfo -> PTerm -> [Name]
1950 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
1951 ++ getRecNames syn sc
1952 getRecNames _ _ = []
1954 toFreeze :: Maybe Accessibility -> Maybe Accessibility
1955 toFreeze (Just Frozen) = Just Hidden
1958{- | Parses data declaration type (normal or codata)
1959DataI ::= 'data' | 'codata';
1961dataI :: IdrisParser Bool
1962dataI = do reserved "data"; return False
1963 <|> do reserved "codata"; return True
1965{- | Parses a data type declaration
1966Data ::= DocComment? Accessibility? DataI FnName TypeSig ExplicitTypeDataRest?
1967 | DocComment? Accessibility? DataI FnName Name* DataRest?
1969Constructor' ::= Constructor KeepTerminator;
1970ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;
1972DataRest ::= '=' SimpleConstructorList Terminator
1975SimpleConstructorList ::=
1977 | SimpleConstructor '|' SimpleConstructorList
1980data_ :: SyntaxInfo -> IdrisParser PDecl
1981data_ syn = try (do doc <- option "" (docComment '|')
1982 acc <- optional accessibility
1986 ty <- typeSig (allowImp syn)
1987 let tyn = expandNS syn tyn_in
1988 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1990 cons <- indentedBlock (constructor syn)
1991 accData acc tyn (map (\ (_, n, _, _) -> n) cons)
1992 return $ PData doc syn fc co (PDatadecl tyn ty cons)))
1993 <|> try (do doc <- option "" (docComment '|')
1995 acc <- optional accessibility
2000 let ty = bindArgs (map (const PType) args) PType
2001 let tyn = expandNS syn tyn_in
2002 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
2003 try (lchar '=') <|> do reserved "where"
2004 let kw = (if co then "co" else "") ++ "data "
2005 let n = show tyn_in ++ " "
2007 let as = concat (intersperse " " $ map show args) ++ " "
2008 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
2009 let ss = concat (intersperse " -> " $ map (const "Type") args)
2010 let fix1 = s ++ as ++ " = ..."
2011 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
2012 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
2013 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
2014 cons <- sepBy1 (simpleConstructor syn) (lchar '|')
2016 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
2017 cons' <- mapM (\ (doc, x, cargs, cfc) ->
2018 do let cty = bindArgs cargs conty
2019 return (doc, x, cty, cfc)) cons
2020 accData acc tyn (map (\ (_, n, _, _) -> n) cons')
2021 return $ PData doc syn fc co (PDatadecl tyn ty cons')))
2022 <?> "data type declaration"
2024 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
2026 mkPApp fc t xs = PApp fc t (map pexp xs)
2027 bindArgs :: [PTerm] -> PTerm -> PTerm
2028 bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
2031{- | Parses a type constructor declaration
2032 Constructor ::= DocComment? FnName TypeSig;
2034constructor :: SyntaxInfo -> IdrisParser (String, Name, PTerm, FC)
2036 = do doc <- option "" (docComment '|')
2037 cn_in <- fnName; fc <- getFC
2038 let cn = expandNS syn cn_in
2039 ty <- typeSig (allowImp syn)
2040 return (doc, cn, ty, fc)
2043{- | Parses a constructor for simple discriminative union data types
2044 SimpleConstructor ::= FnName SimpleExpr* DocComment?
2046simpleConstructor :: SyntaxInfo -> IdrisParser (String, Name, [PTerm], FC)
2047simpleConstructor syn
2048 = do cn_in <- fnName
2049 let cn = expandNS syn cn_in
2051 args <- many (do notEndApp
2053 doc <- option "" (docComment '^')
2054 return (doc, cn, args, fc)
2057{- | Parses a dsl block declaration
2058DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;
2060dsl :: SyntaxInfo -> IdrisParser PDecl
2061dsl syn = do reserved "dsl"
2063 bs <- indentedBlock (overload syn)
2064 let dsl = mkDSL bs (dsl_info syn)
2067 put (i { idris_dsls = addDef n dsl (idris_dsls i) })
2069 <?> "dsl block declaration"
2070 where mkDSL :: [(String, PTerm)] -> DSL -> DSL
2071 mkDSL bs dsl = let var = lookup "variable" bs
2072 first = lookup "index_first" bs
2073 next = lookup "index_next" bs
2074 leto = lookup "let" bs
2075 lambda = lookup "lambda" bs in
2076 initDSL { dsl_var = var,
2077 index_first = first,
2079 dsl_lambda = lambda,
2082{- | Checks DSL for errors -}
2083-- FIXME: currently does nothing, check if DSL is really sane
2084checkDSL :: DSL -> IdrisParser ()
2085checkDSL dsl = return ()
2087{- | Parses a DSL overload declaration
2088OverloadIdentifier ::= 'let' | Identifier;
2089Overload ::= OverloadIdentifier '=' Expr;
2091overload :: SyntaxInfo -> IdrisParser (String, PTerm)
2092overload syn = do o <- identifier <|> do reserved "let"
2094 if o `notElem` overloadable
2095 then fail $ show o ++ " is not an overloading"
2100 <?> "dsl overload declaratioN"
2101 where overloadable = ["let","lambda","index_first","index_next","variable"]
2103{- | Parse a clause with patterns
2106pattern :: SyntaxInfo -> IdrisParser PDecl
2107pattern syn = do fc <- getFC
2108 clause <- clause syn
2109 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
2112{- | Parse a constant applicative form declaration
2113 CAF ::= 'let' FnName '=' Expr Terminator;
2115caf :: SyntaxInfo -> IdrisParser PDecl
2116caf syn = do reserved "let"
2117 n_in <- fnName; let n = expandNS syn n_in
2122 return (PCAF fc n t)
2123 <?> "constant applicative form declaration"
2125{- | Parse an argument expression
2126 ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
2128argExpr :: SyntaxInfo -> IdrisParser PTerm
2129argExpr syn = let syn' = syn { inPattern = True } in
2130 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
2131 <?> "argument expression"
2133{- | Parse a right hand side of a function
2135 | '?=' RHSName? Expr
2139RHSName ::= '{' FnName '}';
2141rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
2142rhs syn n = do lchar '='; expr syn
2144 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
2147 return (addLet name r)
2148 <|> do reserved "impossible"; return PImpossible
2149 <?> "function right hand side"
2150 where mkN :: Name -> Name
2151 mkN (UN x) = UN (x++"_lemma_1")
2152 mkN (NS x n) = NS (mkN x) n
2155 addLet :: Name -> PTerm -> PTerm
2156 addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)
2157 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
2158 where addLetC (l, r) = (l, addLet nm r)
2159 addLet nm r = (PLet (UN "value") Placeholder r (PMetavar nm))
2161{- |Parses a function clause
2162RHSOrWithBlock ::= RHS WhereOrTerminator
2163 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
2165Clause ::= WExpr+ RHSOrWithBlock
2166 | SimpleExpr '<==' FnName RHS WhereOrTerminator
2167 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
2168 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
2170ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
2171WhereOrTerminator ::= WhereBlock | Terminator;
2173clause :: SyntaxInfo -> IdrisParser PClause
2175 = do wargs <- try (do pushIndent; some (wExpr syn))
2178 n <- case lastParse ist of
2180 Nothing -> fail "Invalid clause"
2182 let ctxt = tt_ctxt ist
2183 let wsyn = syn { syn_namespace = [] }
2184 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2189 return $ PClauseR fc wargs r wheres) <|> (do
2192 wval <- simpleExpr syn
2194 ds <- some $ fnDecl syn
2195 let withs = concat ds
2197 return $ PWithR fc wargs wval withs)
2198 <|> do ty <- try (do pushIndent
2199 ty <- simpleExpr syn
2203 n_in <- fnName; let n = expandNS syn n_in
2206 let ctxt = tt_ctxt ist
2207 let wsyn = syn { syn_namespace = [] }
2208 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2213 let capp = PLet (MN 0 "match")
2216 (PRef fc (MN 0 "match"))
2218 put (ist { lastParse = Just n })
2219 return $ PClause fc n capp [] r wheres
2220 <|> do (l, op) <- try (do
2224 when (op == "=" || op == "?=" ) (fail "infix clause definition with \"=\" and \"?=\" not supported ")
2226 let n = expandNS syn (UN op)
2229 wargs <- many (wExpr syn)
2231 let wsyn = syn { syn_namespace = [] }
2232 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2238 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
2239 put (ist { lastParse = Just n })
2240 return $ PClause fc n capp wargs rs wheres) <|> (do
2243 lchar '(' <?> "parenthesized expression"
2244 wval <- bracketed syn
2246 ds <- some $ fnDecl syn
2249 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
2250 let withs = map (fillLHSD n capp wargs) $ concat ds
2251 put (ist { lastParse = Just n })
2252 return $ PWith fc n capp wargs wval withs)
2254 n_in <- fnName; let n = expandNS syn n_in
2255 cargs <- many (constraintArg syn)
2257 args <- many (try (implicitArg (syn { inPattern = True } ))
2258 <|> (fmap pexp (argExpr syn)))
2259 wargs <- many (wExpr syn)
2260 let capp = PApp fc (PRef fc n)
2264 let ctxt = tt_ctxt ist
2265 let wsyn = syn { syn_namespace = [] }
2266 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2272 put (ist { lastParse = Just n })
2273 return $ PClause fc n capp wargs r wheres) <|> (do
2276 put (ist { lastParse = Just n })
2277 lchar '(' <?> "parenthesized expression"
2278 wval <- bracketed syn
2280 ds <- some $ fnDecl syn
2281 let withs = map (fillLHSD n capp wargs) $ concat ds
2284 return $ PWith fc n capp wargs wval withs)
2285 <?> "function clause"
2287 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
2288 fillLHS n capp owargs (PClauseR fc wargs v ws)
2289 = PClause fc n capp (owargs ++ wargs) v ws
2290 fillLHS n capp owargs (PWithR fc wargs v ws)
2291 = PWith fc n capp (owargs ++ wargs) v
2292 (map (fillLHSD n capp (owargs ++ wargs)) ws)
2295 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
2296 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
2297 fillLHSD n c a x = x
2299{- |Parses with pattern
2300 WExpr ::= '|' Expr';
2302wExpr :: SyntaxInfo -> IdrisParser PTerm
2303wExpr syn = do lchar '|'
2307{- |Parses a where block
2308WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
2310whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
2312 = do reserved "where"
2313 ds <- indentedBlock1 (decl syn)
2314 let dns = concatMap (concatMap declared) ds
2315 return (concat ds, map (\x -> (x, decoration syn x)) dns)
2318{- |Parses a code generation target language name
2327codegen_ :: IdrisParser Codegen
2328codegen_ = do reserved "C"; return ViaC
2329 <|> do reserved "Java"; return ViaJava
2330 <|> do reserved "JavaScript"; return ViaJavaScript
2331 <|> do reserved "Node"; return ViaNode
2332 <|> do reserved "LLVM"; return ViaLLVM
2333 <|> do reserved "Bytecode"; return Bytecode
2334 <?> "code generation language"
2336{- |Parses a compiler directive
2339 | String ',' StringList
2342Directive ::= '%' Directive';
2344Directive' ::= 'lib' CodeGen String_t
2345 | 'link' CodeGen String_t
2346 | 'flag' CodeGen String_t
2347 | 'include' CodeGen String_t
2350 | 'access' Accessibility
2351 | 'default' Totality
2353 | 'dynamic' StringList
2354 | 'language' 'TypeProviders'
2355 | 'language' 'ErrorReflection'
2358directive :: SyntaxInfo -> IdrisParser [PDecl]
2359directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
2360 return [PDirective (do addLib cgn lib
2361 addIBC (IBCLib cgn lib))]
2362 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
2363 return [PDirective (do dirs <- allImportDirs
2364 o <- liftIO $ findInPath dirs obj
2365 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
2366 addObjectFile cgn o)]
2367 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
2368 flag <- stringLiteral
2369 return [PDirective (do addIBC (IBCCGFlag cgn flag)
2371 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
2372 return [PDirective (do addHdr cgn hdr
2373 addIBC (IBCHeader cgn hdr))]
2374 <|> do try (lchar '%' *> reserved "hide"); n <- iName []
2375 return [PDirective (do setAccessibility n Hidden
2376 addIBC (IBCAccess n Hidden))]
2377 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
2378 return [PDirective (do setAccessibility n Frozen
2379 addIBC (IBCAccess n Frozen))]
2380 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
2381 return [PDirective (do i <- get
2382 put(i { default_access = acc }))]
2383 <|> do try (lchar '%' *> reserved "default"); tot <- totality
2385 put (i { default_total = tot } )
2386 return [PDirective (do i <- get
2387 put(i { default_total = tot }))]
2388 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
2389 return [PDirective (setLogLevel (fromInteger i))]
2390 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
2391 return [PDirective (do added <- addDyLib libs
2393 Left lib -> addIBC (IBCDyLib (lib_name lib))
2396 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
2397 return [PDirective (addLangExt ext)]
2400pLangExt :: IdrisParser LanguageExt
2401pLangExt = (reserved "TypeProviders" >> return TypeProviders)
2402 <|> (reserved "ErrorReflection" >> return ErrorReflection)
2404{- | Parses a totality
2405Totality ::= 'partial' | 'total'
2407totality :: IdrisParser Bool
2409 = do reserved "total"; return True
2410 <|> do reserved "partial"; return False
2412{- | Parses a type provider
2413Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;
2415provider :: SyntaxInfo -> IdrisParser [PDecl]
2416provider syn = do try (lchar '%' *> reserved "provide");
2417 lchar '('; n <- fnName; t <- typeSig syn; lchar ')'
2421 return [PProvider syn fc n t e]
2424{- | Parses a transform
2425Transform ::= '%' 'transform' Expr '==>' Expr
2427transform :: SyntaxInfo -> IdrisParser [PDecl]
2428transform syn = do try (lchar '%' *> reserved "transform")
2429 -- leave it unchecked, until we work out what this should
2431-- safety <- option True (do reserved "unsafe"
2437 return [PTransform fc False l r]
2440{- | Parses a tactic script
2441Tactic ::= 'intro' NameList?
2443 | 'refine' Name Imp+
2447 | 'let' Name ':' Expr' '=' Expr
2448 | 'let' Name '=' Expr
2451 | 'applyTactic' Expr
2454 | 'try' Tactic '|' Tactic
2472 | Tactic ';' TacticSeq
2477tactic :: SyntaxInfo -> IdrisParser PTactic
2478tactic syn = do reserved "intro"; ns <- sepBy name (lchar ',')
2480 <|> do reserved "intros"; return Intros
2481 <|> try (do reserved "refine"; n <- name
2483 return $ Refine n imps)
2484 <|> do reserved "refine"; n <- name
2486 return $ Refine n []
2487 <|> do reserved "mrefine"; n <- name
2489 return $ MatchRefine n
2490 <|> do reserved "rewrite"; t <- expr syn;
2492 return $ Rewrite (desugar syn i t)
2493 <|> do reserved "equiv"; t <- expr syn;
2495 return $ Equiv (desugar syn i t)
2496 <|> try (do reserved "let"; n <- name; lchar ':';
2497 ty <- expr' syn; lchar '='; t <- expr syn;
2499 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
2500 <|> try (do reserved "let"; n <- name; lchar '=';
2503 return $ LetTac n (desugar syn i t))
2504 <|> do reserved "focus"; n <- name
2506 <|> do reserved "exact"; t <- expr syn;
2508 return $ Exact (desugar syn i t)
2509 <|> do reserved "applyTactic"; t <- expr syn;
2511 return $ ApplyTactic (desugar syn i t)
2512 <|> do reserved "reflect"; t <- expr syn;
2514 return $ Reflect (desugar syn i t)
2515 <|> do reserved "fill"; t <- expr syn;
2517 return $ Fill (desugar syn i t)
2518 <|> do reserved "try"; t <- tactic syn;
2525 ts <- sepBy1 (tactic syn) (lchar ';')
2527 return $ TSeq t (mergeSeq ts)
2528 <|> do reserved "compute"; return Compute
2529 <|> do reserved "trivial"; return Trivial
2530 <|> do reserved "solve"; return Solve
2531 <|> do reserved "attack"; return Attack
2532 <|> do reserved "state"; return ProofState
2533 <|> do reserved "term"; return ProofTerm
2534 <|> do reserved "undo"; return Undo
2535 <|> do reserved "qed"; return Qed
2536 <|> do reserved "abandon"; return Abandon
2537 <|> do lchar ':'; reserved "q"; return Abandon
2540 imp :: IdrisParser Bool
2541 imp = do lchar '?'; return False
2542 <|> do lchar '_'; return True
2543 mergeSeq :: [PTactic] -> PTactic
2545 mergeSeq (t:ts) = TSeq t (mergeSeq ts)
2547{- | Parses a tactic as a whole -}
2548fullTactic :: SyntaxInfo -> IdrisParser PTactic
2549fullTactic syn = do t <- tactic syn
2553{- * Loading and parsing -}
2554{- | Parses an expression from input -}
2555parseExpr :: IState -> String -> Result PTerm
2556parseExpr st = parseString (evalStateT (fullExpr defaultSyntax) st) (Directed (UTF8.fromString "(input)") 0 0 0 0)
2558{- | Parses a tactic from input -}
2559parseTactic :: IState -> String -> Result PTactic
2560parseTactic st = parseString (evalStateT (fullTactic defaultSyntax) st) (Directed (UTF8.fromString "(input)") 0 0 0 0)
2562-- | Parse module header and imports
2563parseImports :: FilePath -> String -> Idris ([String], [String], Maybe Delta)
2564parseImports fname input
2566 case parseString (evalStateT imports i) (Directed (UTF8.fromString fname) 0 0 0 0) input of
2567 Failure err -> fail (show err)
2568 Success (x, i) -> do -- Discard state updates (there should be
2571 where imports :: IdrisParser (([String], [String], Maybe Delta), IState)
2572 imports = do whiteSpace
2573 mname <- moduleHeader
2576 isEof <- lookAheadMatches eof
2581 return ((mname, ps, mrk'), i)
2584-- | A program is a list of declarations, possibly with associated
2585-- documentation strings.
2586parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
2588parseProg syn fname input mrk
2590 case parseString (evalStateT mainProg i) (Directed (UTF8.fromString fname) 0 0 0 0) input of
2591 Failure doc -> do iputStrLn (show doc)
2592 -- FIXME: Get error location from trifecta
2593 --let errl = sourceLine (errorPos err)
2595 putIState (i { errLine = Just 0 }) -- Just errl })
2597 Success (x, i) -> do putIState i
2599 where mainProg :: IdrisParser ([PDecl], IState)
2600 mainProg = case mrk of
2601 Nothing -> do i <- get; return ([], i)
2608-- | Collect 'PClauses' with the same function name
2609collect :: [PDecl] -> [PDecl]
2610collect (c@(PClauses _ o _ _) : ds)
2611 = clauses (cname c) [] (c : ds)
2612 where clauses :: Maybe Name -> [PClause] -> [PDecl] -> [PDecl]
2613 clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)
2614 | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds
2615 clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds)
2616 | n == n' = clauses j (PWith fc' n' l ws r (collect w) : acc) ds
2617 clauses (Just n) acc xs = PClauses (fcOf c) o n (reverse acc) : collect xs
2618 clauses Nothing acc (x:xs) = collect xs
2619 clauses Nothing acc [] = []
2621 cname :: PDecl -> Maybe Name
2622 cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n
2623 cname (PClauses fc _ _ [PWith _ n _ _ _ _]) = Just n
2624 cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing
2625 cname (PClauses fc _ _ [PWithR _ _ _ _]) = Nothing
2627 fcOf (PClauses fc _ _ _) = fc
2628collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
2629collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds
2630collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds
2631collect (PClass doc f s cs n ps ds : ds')
2632 = PClass doc f s cs n ps (collect ds) : collect ds'
2633collect (PInstance f s cs n ps t en ds : ds')
2634 = PInstance f s cs n ps t en (collect ds) : collect ds'
2635collect (d : ds) = d : collect ds
2638{- | Load idris module -}
2639loadModule :: FilePath -> Idris String
2641 = idrisCatch (do i <- getIState
2642 let file = takeWhile (/= ' ') f
2643 ibcsd <- valIBCSubDir i
2644 ids <- allImportDirs
2645 fp <- liftIO $ findImport ids ibcsd file
2646 if file `elem` imported i
2647 then iLOG $ "Already read " ++ file
2648 else do putIState (i { imported = file : imported i })
2650 IDR fn -> loadSource False fn
2651 LIDR fn -> loadSource True fn
2653 idrisCatch (loadIBC fn)
2654 (\c -> do iLOG $ fn ++ " failed " ++ show c
2656 IDR sfn -> loadSource False sfn
2657 LIDR sfn -> loadSource True sfn)
2658 let (dir, fh) = splitFileName file
2659 return (dropExtension fh))
2660 (\e -> do let msg = show e
2661 setErrLine (getErrLine msg)
2665{- | Load idris code from file -}
2666loadFromIFile :: IFileType -> Idris ()
2667loadFromIFile i@(IBC fn src)
2668 = do iLOG $ "Skipping " ++ getSrcFile i
2669 idrisCatch (loadIBC fn)
2670 (\c -> do fail $ fn ++ " failed " ++ show c)
2672 getSrcFile (IDR fn) = fn
2673 getSrcFile (LIDR fn) = fn
2674 getSrcFile (IBC f src) = getSrcFile src
2676loadFromIFile (IDR fn) = loadSource' False fn
2677loadFromIFile (LIDR fn) = loadSource' True fn
2679{-| Load idris source code and show error if something wrong happens -}
2680loadSource' :: Bool -> FilePath -> Idris ()
2682 = idrisCatch (loadSource lidr r)
2683 (\e -> do let msg = show e
2684 setErrLine (getErrLine msg)
2687{- | Load Idris source code-}
2688loadSource :: Bool -> FilePath -> Idris ()
2690 = do iLOG ("Reading " ++ f)
2692 let def_total = default_total i
2693 file_in <- liftIO $ readFile f
2694 file <- if lidr then tclift $ unlit f file_in else return file_in
2695 (mname, modules, pos) <- parseImports f file
2697 putIState (i { default_access = Hidden })
2698 clearIBC -- start a new .ibc file
2699 mapM_ (addIBC . IBCImport) modules
2700 ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
2702 unless (null ds') $ do
2703 let ds = namespaces mname ds'
2704 logLvl 3 (dumpDecls ds)
2706 logLvl 10 (show (toAlist (idris_implicits i)))
2707 logLvl 3 (show (idris_infixes i))
2708 -- Now add all the declarations to the context
2710 when v $ iputStrLn $ "Type checking " ++ f
2711 -- we totality check after every Mutual block, so if
2712 -- anything is a single definition, wrap it in a
2713 -- mutual block on its own
2714 elabDecls toplevel (map toMutual ds)
2716 -- simplify every definition do give the totality checker
2718 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
2719 updateContext (simplifyCasedef n))
2720 (map snd (idris_totcheck i))
2721 -- build size change graph from simplified definitions
2722 iLOG "Totality checking"
2724 mapM_ buildSCG (idris_totcheck i)
2725 mapM_ checkDeclTotality (idris_totcheck i)
2726 iLOG ("Finished " ++ f)
2727 ibcsd <- valIBCSubDir i
2728 iLOG "Universe checking"
2730 let ibc = ibcPathNoFallback ibcsd f
2732 addHides (hide_list i)
2735 idrisCatch (do writeIBC f ibc; clearIBC)
2736 (\c -> return ()) -- failure is harmless
2738 putIState (i { default_total = def_total,
2743 namespaces :: [String] -> [PDecl] -> [PDecl]
2744 namespaces [] ds = ds
2745 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
2747 toMutual :: PDecl -> PDecl
2748 toMutual m@(PMutual _ d) = m
2749 toMutual x = let r = PMutual (FC "single mutual" 0) [x] in
2751 PClauses _ _ _ _ -> r
2752 PClass _ _ _ _ _ _ _ -> r
2753 PInstance _ _ _ _ _ _ _ _ -> r
2756{- | Adds names to hide list -}
2757addHides :: [(Name, Maybe Accessibility)] -> Idris ()
2758addHides xs = do i <- getIState
2759 let defh = default_access i
2760 let (hs, as) = partition isNothing xs
2763 (map (\ (n, _) -> (n, defh)) hs ++
2764 map (\ (n, Just a) -> (n, a)) as)
2765 where isNothing (_, Nothing) = True
2768 doHide (n, a) = do setAccessibility n a
2769 addIBC (IBCAccess n a)
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list