1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
2module Idris.Parser where
4import Prelude hiding (pi)
6import Text.Trifecta.Delta
7import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)
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 IdrisInnerParser
61newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }
62 deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing, Parsing, DeltaParsing, MarkParsing Delta, Monoid)
64instance TokenParsing IdrisInnerParser where
65 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
67-- | Generalized monadic parsing constraint type
68type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)
70{- * Space, comments and literals (token/lexing like parsers) -}
72-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)
73simpleWhiteSpace :: MonadicParsing m => m ()
74simpleWhiteSpace = satisfy isSpace *> pure ()
76-- | Checks if a charcter is end of line
81eol :: MonadicParsing m => m ()
82eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"
84-- | Checks if a character is a documentation comment marker
85isDocCommentMarker :: Char -> Bool
86isDocCommentMarker '|' = True
87isDocCommentMarker '^' = True
88isDocCommentMarker _ = False
90{- | Consumes a single-line comment
91 SingleLineComment_t ::= '--' EOL_t
92 | '--' ~DocCommentMarker_t ~EOL_t* EOL_t
95singleLineComment :: MonadicParsing m => m ()
96singleLineComment = try (string "--" *> eol *> pure ())
97 <|> string "--" *> satisfy (not . isDocCommentMarker) *> many (satisfy (not . isEol)) *> eol *> pure ()
100{- | Consumes a multi-line comment
101 MultiLineComment_t ::=
103 | '{ -' ~DocCommentMarker_t InCommentChars_t
108 | MultiLineComment_t InCommentChars_t
109 | ~'- }'+ InCommentChars_t
113multiLineComment :: MonadicParsing m => m ()
114multiLineComment = try (string "{-" *> (string "-}") *> pure ())
115 <|> string "{-" *> satisfy (not . isDocCommentMarker) *> inCommentChars
117 where inCommentChars :: MonadicParsing m => m ()
118 inCommentChars = string "-}" *> pure ()
119 <|> try (multiLineComment) *> inCommentChars
120 <|> try (docComment '|') *> inCommentChars
121 <|> try (docComment '^') *> inCommentChars
122 <|> skipSome (noneOf startEnd) *> inCommentChars
123 <|> oneOf startEnd *> inCommentChars
128{-| Parses a documentation comment (similar to haddoc) given a marker character
129 DocComment_t ::= '--' DocCommentMarker_t ~EOL_t* EOL_t
130 | '{ -' DocCommentMarket_t ~'- }'* '- }'
133docComment :: MonadicParsing m => Char -> m String
134docComment marker | isDocCommentMarker marker = do dc <- docComment' marker; return (T.unpack $ T.strip $ T.pack dc)
135 | otherwise = fail "internal error: tried to parse a documentation comment with invalid marker"
136 where docComment' :: MonadicParsing m => Char -> m String
137 docComment' marker = string "--" *> char marker *> many (satisfy (not . isEol)) <* eol
138 <|> string "{-" *> char marker *> (manyTill anyChar (try (string "-}")) <?> "end of comment")
141-- | Parses some white space
142whiteSpace :: MonadicParsing m => m ()
143whiteSpace = Tok.whiteSpace
145-- | Parses a string literal
146stringLiteral :: MonadicParsing m => m String
147stringLiteral = Tok.stringLiteral
149-- | Parses a char literal
150charLiteral :: MonadicParsing m => m Char
151charLiteral = Tok.charLiteral
153-- | Parses a natural number
154natural :: MonadicParsing m => m Integer
157-- | Parses an integral number
158integer :: MonadicParsing m => m Integer
161-- | Parses a floating point number
162float :: MonadicParsing m => m Double
165{- * Symbols, identifiers, names and operators -}
168-- | Idris Style for parsing identifiers/reserved keywords
169idrisStyle :: MonadicParsing m => IdentifierStyle m
170idrisStyle = IdentifierStyle _styleName _styleStart _styleLetter _styleReserved Hi.Identifier Hi.ReservedIdentifier
171 where _styleName = "Idris"
172 _styleStart = satisfy isAlpha
173 _styleLetter = satisfy isAlphaNum <|> oneOf "_'" <|> (lchar '.')
174 _styleReserved = HS.fromList ["let", "in", "data", "codata", "record", "Type",
175 "do", "dsl", "import", "impossible",
176 "case", "of", "total", "partial", "mutual",
177 "infix", "infixl", "infixr", "rewrite",
178 "where", "with", "syntax", "proof", "postulate",
179 "using", "namespace", "class", "instance",
180 "public", "private", "abstract", "implicit",
182 "Int", "Integer", "Float", "Char", "String", "Ptr",
183 "Bits8", "Bits16", "Bits32", "Bits64",
184 "Bits8x16", "Bits16x8", "Bits32x4", "Bits64x2"]
186char :: MonadicParsing m => Char -> m Char
189string :: MonadicParsing m => String -> m String
192-- | Parses a character as a token
193lchar :: MonadicParsing m => Char -> m Char
196-- | Parses string as a token
197symbol :: MonadicParsing m => String -> m String
200-- | Parses a reserved identifier
201reserved :: MonadicParsing m => String -> m ()
202reserved = Tok.reserve idrisStyle
204-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
205-- | Parses a reserved operator
206reservedOp :: MonadicParsing m => String -> m ()
207reservedOp name = token $ try $
209 notFollowedBy (operatorLetter) <?> ("end of " ++ show name)
211-- | Parses an identifier as a token
212identifier :: MonadicParsing m => m String
213identifier = token $ Tok.ident idrisStyle
215-- | Parses an identifier with possible namespace as a name
216iName :: MonadicParsing m => [String] -> m Name
217iName bad = maybeWithNS identifier False bad <?> "name"
219-- | Parses an string possibly prefixed by a namespace
220maybeWithNS :: MonadicParsing m => m String -> Bool -> [String] -> m Name
221maybeWithNS parser ascend bad = do
222 i <- option "" (lookAhead identifier)
223 when (i `elem` bad) $ unexpected "reserved identifier"
224 let transf = if ascend then id else reverse
225 (x, xs) <- choice (transf (parserNoNS parser : parsersNS parser i))
226 return $ mkName (x, xs)
227 where parserNoNS :: MonadicParsing m => m String -> m (String, String)
228 parserNoNS parser = do x <- parser; return (x, "")
229 parserNS :: MonadicParsing m => m String -> String -> m (String, String)
230 parserNS parser ns = do xs <- string ns; lchar '.'; x <- parser; return (x, xs)
231 parsersNS :: MonadicParsing m => m String -> String -> [m (String, String)]
232 parsersNS parser i = [try (parserNS parser ns) | ns <- (initsEndAt (=='.') i)]
235name :: IdrisParser Name
237 iName (syntax_keywords i)
241{- | List of all initial segments in ascending order of a list. Every such
242 initial segment ends right before an element satisfying the given
245initsEndAt :: (a -> Bool) -> [a] -> [[a]]
247initsEndAt p (x:xs) | p x = [] : x_inits_xs
248 | otherwise = x_inits_xs
249 where x_inits_xs = [x : cs | cs <- initsEndAt p xs]
252{- | Create a `Name' from a pair of strings representing a base name and its
255mkName :: (String, String) -> Name
257mkName (n, ns) = NS (UN n) (reverse (parseNS ns))
258 where parseNS x = case span (/= '.') x of
260 (x, '.':y) -> x : parseNS y
262operatorLetter :: MonadicParsing m => m Char
263operatorLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
265-- | Parses an operator
266operator :: MonadicParsing m => m String
267operator = do op <- token . some $ operatorLetter
268 when (op == ":") $ fail "(:) is not a valid operator"
271{- * Position helpers -}
272{- | Get filename from position (returns "(interactive)" when no source file is given) -}
273fileName :: Delta -> String
274fileName (Directed fn _ _ _ _) = UTF8.toString fn
275fileName _ = "(interactive)"
277{- | Get line number from position -}
278lineNum :: Delta -> Int
279lineNum (Lines l _ _ _) = fromIntegral l + 1
280lineNum (Directed _ l _ _ _) = fromIntegral l + 1
282{- | Get file position as FC -}
283getFC :: MonadicParsing m => m FC
284getFC = do s <- position
285 let (dir, file) = splitFileName (fileName s)
286 let f = if dir == addTrailingPathSeparator "." then file else fileName s
287 return $ FC f (lineNum s)
290-- | Bind constraints to term
291bindList :: (Name -> PTerm -> PTerm -> PTerm) -> [(Name, PTerm)] -> PTerm -> PTerm
293bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
295{- |Creates table for fixtiy declarations to build expression parser using
296 pre-build and user-defined operator/fixity declarations -}
297table :: [FixDecl] -> OperatorTable IdrisParser PTerm
299 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
300 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]
301 ++ toTable (reverse fixes) ++
303 [binary "=" PEq AssocLeft],
304 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
306{- |Calculates table for fixtiy declarations -}
307toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm
308toTable fs = map (map toBin)
309 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
310 where toBin (Fix (PrefixN _) op) = prefix op
311 (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
313 = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
314 assoc (Infixl _) = AssocLeft
315 assoc (Infixr _) = AssocRight
316 assoc (InfixN _) = AssocNone
318{- |Binary operator -}
319binary :: String -> (FC -> PTerm -> PTerm -> PTerm) -> Assoc -> Operator IdrisParser PTerm
320binary name f = Infix (do fc <- getFC
322 doc <- option "" (docComment '^')
325{- |Prefix operator -}
326prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm
327prefix name f = Prefix (do reservedOp name
331{- |Backtick operator -}
332backtick :: Operator IdrisParser PTerm
333backtick = Infix (do lchar '`'; n <- fnName
336 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
338-- | Allow implicit type declarations
339allowImp :: SyntaxInfo -> SyntaxInfo
340allowImp syn = syn { implicitAllowed = True }
342-- | Disallow implicit type declarations
343disallowImp :: SyntaxInfo -> SyntaxInfo
344disallowImp syn = syn { implicitAllowed = False }
346-- | Adds accessibility option for function
347addAcc :: Name -> Maybe Accessibility -> IdrisParser ()
348addAcc n a = do i <- get
349 put (i { hide_list = (n, a) : hide_list i })
351{- | Add accessbility option for data declarations
352 (works for classes too - 'abstract' means the data/class is visible but members not) -}
353accData :: Maybe Accessibility -> Name -> [Name] -> IdrisParser ()
354accData (Just Frozen) n ns = do addAcc n (Just Frozen)
355 mapM_ (\n -> addAcc n (Just Hidden)) ns
356accData a n ns = do addAcc n a
357 mapM_ (`addAcc` a) ns
360{- * Error reporting helpers -}
361{- | Error message with possible fixes list -}
362fixErrorMsg :: String -> [String] -> String
363fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)
365{- * Layout helpers -}
367-- | Push indentation to stack
368pushIndent :: IdrisParser ()
369pushIndent = do pos <- position
371 put (ist { indent_stack = (fromIntegral (column pos) + 1) : indent_stack ist })
373-- | Pops indentation from stack
374popIndent :: IdrisParser ()
375popIndent = do ist <- get
376 let (x : xs) = indent_stack ist
377 put (ist { indent_stack = xs })
379-- | Gets current indentation
380indent :: IdrisParser Int
381indent = liftM ((+1) . fromIntegral . column) position
383-- | Gets last indentation
384lastIndent :: IdrisParser Int
385lastIndent = do ist <- get
386 case indent_stack ist of
390-- | Applies parser in an indented position
391indented :: IdrisParser a -> IdrisParser a
392indented p = notEndBlock *> p <* keepTerminator
394-- | Applies parser to get a block (which has possibly indented statements)
395indentedBlock :: IdrisParser a -> IdrisParser [a]
396indentedBlock p = do openBlock
398 res <- many (indented p)
403-- | Applies parser to get a block with at least one statement (which has possibly indented statements)
404indentedBlock1 :: IdrisParser a -> IdrisParser [a]
405indentedBlock1 p = do openBlock
407 res <- some (indented p)
412-- | Applies parser to get a block with exactly one (possibly indented) statement
413indentedBlockS :: IdrisParser a -> IdrisParser a
414indentedBlockS p = do openBlock
422-- | Checks if the following character matches provided parser
423lookAheadMatches :: MonadicParsing m => m a -> m Bool
424lookAheadMatches p = do match <- lookAhead (optional p)
425 return $ isJust match
427-- | Parses a start of block
428openBlock :: IdrisParser ()
429openBlock = do lchar '{'
431 put (ist { brace_stack = Nothing : brace_stack ist })
434 -- if we're not indented further, it's an empty block, so
435 -- increment lvl to ensure we get to the end
436 let lvl = case brace_stack ist of
438 if lvl' <= lvl_old then lvl_old+1
440 [] -> if lvl' == 1 then 2 else lvl'
442 put (ist { brace_stack = Just lvl : brace_stack ist })
445-- | Parses an end of block
446closeBlock :: IdrisParser ()
447closeBlock = do ist <- get
448 bs <- case brace_stack ist of
449 [] -> eof >> return []
450 Nothing : xs -> lchar '}' >> return xs <?> "end of block"
451 Just lvl : xs -> (do i <- indent
452 isParen <- lookAheadMatches (char ')')
453 if i >= lvl && not isParen
454 then fail "not end of block"
456 <|> (do notOpenBraces
459 put (ist { brace_stack = bs })
461-- | Parses a terminator
462terminator :: IdrisParser ()
463terminator = do lchar ';'; popIndent
464 <|> do c <- indent; l <- lastIndent
465 if c <= l then popIndent else fail "not a terminator"
466 <|> do isParen <- lookAheadMatches (oneOf ")}")
467 if isParen then popIndent else fail "not a termiantor"
470-- | Parses and keeps a terminator
471keepTerminator :: IdrisParser ()
472keepTerminator = do lchar ';'; return ()
473 <|> do c <- indent; l <- lastIndent
474 unless (c <= l) $ fail "not a terminator"
475 <|> do isParen <- lookAheadMatches (oneOf ")}|")
476 unless isParen $ fail "not a terminator"
479-- | Checks if application expression does not end
480notEndApp :: IdrisParser ()
481notEndApp = do c <- indent; l <- lastIndent
482 when (c <= l) (fail "terminator")
484-- | Checks that it is not end of block
485notEndBlock :: IdrisParser ()
486notEndBlock = do ist <- get
487 case brace_stack ist of
488 Just lvl : xs -> do i <- indent
489 isParen <- lookAheadMatches (char ')')
490 when (i < lvl || isParen) (fail "end of block")
493notOpenBraces :: IdrisParser ()
494notOpenBraces = do ist <- get
495 when (hasNothing $ brace_stack ist) $ fail "end of input"
496 where hasNothing :: [Maybe a] -> Bool
497 hasNothing = any isNothing
501{- | Parses module definition
502 ModuleHeader ::= 'module' Identifier_t ';'?;
504moduleHeader :: IdrisParser [String]
505moduleHeader = try (do reserved "module"
507 option ';' (lchar ';')
508 return (moduleName i))
510 where moduleName x = case span (/='.') x of
512 (x, '.':y) -> x : moduleName y
514{- | Parses an import statement
515 Import ::= 'import' Identifier_t ';'?;
517import_ :: IdrisParser String
518import_ = do reserved "import"
520 option ';' (lchar ';')
522 <?> "import statement"
523 where toPath f = foldl1' (</>) (Spl.splitOn "." f)
525{- | Parses program source
528prog :: SyntaxInfo -> IdrisParser [PDecl]
529prog syn = do whiteSpace
530 decls <- many (decl syn)
533 let c = (concat decls)
536{- | Parses a top-level declaration
552decl :: SyntaxInfo -> IdrisParser [PDecl]
553decl syn = do notEndBlock
555 where declBody :: IdrisParser [PDecl]
563 <|> do d <- dsl syn; return [d]
567 <|> do import_; fail "imports must be at top of file"
569 declBody' :: IdrisParser [PDecl]
570 declBody' = do d <- decl' syn
572 let d' = fmap (desugar syn i) d
575{- | Parses a top-level declaration with possible syntax sugar
584decl' :: SyntaxInfo -> IdrisParser PDecl
592{- | Parses a syntax extension declaration (and adds the rule to parser state)
593 SyntaxDecl ::= SyntaxRule;
595syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
596syntaxDecl syn = do s <- syntaxRule syn
598 let rs = syntax_rules i
599 let ns = syntax_keywords i
600 let ibc = ibc_write i
601 let ks = map show (names s)
602 put (i { syntax_rules = s : rs,
603 syntax_keywords = ks ++ ns,
604 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc })
606 return (PSyntax fc s)
607 where names (Rule syms _ _) = mapMaybe ename syms
608 ename (Keyword n) = Just n
611{- | Parses a syntax extension declaration
612SyntaxRuleOpts ::= 'term' | 'pattern';
615 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
617SyntaxSym ::= '[' Name_t ']'
623syntaxRule :: SyntaxInfo -> IdrisParser Syntax
627 sty <- option AnySyntax (do reserved "term"; return TermSyntax
628 <|> do reserved "pattern"; return PatternSyntax)
631 syms <- some syntaxSym
632 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
633 let ns = mapMaybe getName syms
634 when (length ns /= length (nub ns))
635 $ unexpected "repeated variable in syntax rule"
637 tm <- typeExpr (allowImp syn)
639 return (Rule (mkSimple syms) tm sty)
641 isExpr (Expr _) = True
643 getName (Expr n) = Just n
645 -- Can't parse two full expressions (i.e. expressions with application) in a row
646 -- so change them both to a simple expression
647 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
648 mkSimple xs = mkSimple' xs
650 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
652 mkSimple' (e : es) = e : mkSimple' es
656{- | Parses a syntax symbol (either binding variable, keyword or expression)
657SyntaxSym ::= '[' Name_t ']'
663syntaxSym :: IdrisParser SSymbol
664syntaxSym = try (do lchar '['; n <- name; lchar ']'
666 <|> try (do lchar '{'; n <- name; lchar '}'
670 <|> do sym <- stringLiteral
674{- | Parses a function declaration with possible syntax sugar
675 FunDecl ::= FunDecl';
677fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
679 = try (do notEndBlock
682 let d' = fmap (desugar syn i) d
684 <?> "function declaration"
686{- Parses a function declaration
688 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
694fnDecl' :: SyntaxInfo -> IdrisParser PDecl
695fnDecl' syn = do (doc, fc, opts', n, acc) <- try (do
696 doc <- option "" (docComment '|')
699 let initOpts = if default_total ist
702 opts <- fnOpts initOpts
703 acc <- optional accessibility
706 let n = expandNS syn n_in
709 return (doc, fc, opts', n, acc))
710 ty <- typeExpr (allowImp syn)
713 return (PTy doc syn fc opts' n ty)
717 <?> "function declaration"
720{- Parses function options given initial options
726 | '%' 'specialise' '[' NameTimesList? ']'
729NameTimes ::= FnName Natural?;
733 | NameTimes ',' NameTimesList
737-- FIXME: Check compatability for function options (i.e. partal/total)
738fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
740 = do reserved "total"; fnOpts (TotalFn : opts)
741 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
742 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;
743 fnOpts (CExport c : opts)
744 <|> do try (lchar '%' *> reserved "assert_total");
745 fnOpts (AssertTotal : opts)
746 <|> do try (lchar '%' *> reserved "reflection");
747 fnOpts (Reflection : opts)
748 <|> do lchar '%'; reserved "specialise";
749 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
750 fnOpts (Specialise ns : opts)
751 <|> do reserved "implicit"; fnOpts (Implicit : opts)
753 <?> "function modifier"
754 where nameTimes :: IdrisParser (Name, Maybe Int)
755 nameTimes = do n <- fnName
756 t <- option Nothing (do reds <- natural
757 return (Just (fromInteger reds)))
760{- | Parses an operator in function position i.e. enclosed by `()', with an
763 OperatorFront ::= (Identifier_t '.')? '(' Operator_t ')';
765operatorFront :: IdrisParser Name
766operatorFront = maybeWithNS (lchar '(' *> operator <* lchar ')') False []
768{- | Parses a function (either normal name or operator)
769 FnName ::= Name | OperatorFront;
771fnName :: IdrisParser Name
772fnName = try operatorFront <|> name <?> "function name"
774{- | Parses an accessibilty modifier (e.g. public, private) -}
775accessibility :: IdrisParser Accessibility
776accessibility = do reserved "public"; return Public
777 <|> do reserved "abstract"; return Frozen
778 <|> do reserved "private"; return Hidden
779 <?> "accessibility modifier"
783{- | Parses a postulate
786 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
789postulate :: SyntaxInfo -> IdrisParser PDecl
790postulate syn = do doc <- try $ do doc <- option "" (docComment '|')
795 let initOpts = if default_total ist
798 opts <- fnOpts initOpts
799 acc <- optional accessibility
802 let n = expandNS syn n_in
804 ty <- typeExpr (allowImp syn)
808 return (PPostulate doc syn fc opts' n ty)
811{- | Parses a using declaration
814 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
817using_ :: SyntaxInfo -> IdrisParser [PDecl]
819 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
821 let uvars = using syn
822 ds <- many (decl (syn { using = uvars ++ ns }))
825 <?> "using declaration"
827{- | Parses a parameters declaration
830 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
833params :: SyntaxInfo -> IdrisParser [PDecl]
835 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
837 let pvars = syn_params syn
838 ds <- many (decl syn { syn_params = pvars ++ ns })
841 return [PParams fc ns (concat ds)]
842 <?> "parameters declaration"
844{- | Parses a mutual declaration (for mutually recursive functions)
847 'mutual' OpenBlock Decl* CloseBlock
850mutual :: SyntaxInfo -> IdrisParser [PDecl]
854 let pvars = syn_params syn
855 ds <- many (decl syn)
858 return [PMutual fc (concat ds)]
861{- | Parses a namespace declaration
864 'namespace' identifier OpenBlock Decl+ CloseBlock
867namespace :: SyntaxInfo -> IdrisParser [PDecl]
869 do reserved "namespace"; n <- identifier;
871 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
873 return [PNamespace n (concat ds)]
874 <?> "namespace declaration"
876{- | Parses a fixity declaration
879 FixityType Natural_t OperatorList Terminator
882fixity :: IdrisParser PDecl
883fixity = do pushIndent
884 f <- fixityType; i <- natural; ops <- sepBy1 operator (lchar ',')
886 let prec = fromInteger i
888 let infixes = idris_infixes istate
889 let fs = map (Fix (f prec)) ops
890 let redecls = map (alreadyDeclared infixes) fs
891 let ill = filter (not . checkValidity) redecls
893 then do put (istate { idris_infixes = nub $ sort (fs ++ infixes)
894 , ibc_write = map IBCFix fs ++ ibc_write istate
897 return (PFix fc (f prec) ops)
898 else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
899 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
900 <?> "fixity declaration"
901 where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
902 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
904 checkValidity :: (FixDecl, [FixDecl]) -> Bool
905 checkValidity (f, fs) = all (== f) fs
907 extractName :: FixDecl -> String
908 extractName (Fix _ n) = n
910{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)
918fixityType :: IdrisParser (Int -> Fixity)
919fixityType = do reserved "infixl"; return Infixl
920 <|> do reserved "infixr"; return Infixr
921 <|> do reserved "infix"; return InfixN
922 <|> do reserved "prefix"; return PrefixN
925{- |Parses a methods block (for type classes and instances)
926 MethodsBlock ::= 'where' OpenBlock FnDecl* CloseBlock
928methodsBlock :: SyntaxInfo -> IdrisParser [PDecl]
929methodsBlock syn = do reserved "where"
931 ds <- many (fnDecl syn)
936{- |Parses a type class declaration
940 | '(' Name ':' Expr ')'
944 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* MethodsBlock?
947class_ :: SyntaxInfo -> IdrisParser [PDecl]
948class_ syn = do (doc, acc) <- try (do
949 doc <- option "" (docComment '|')
950 acc <- optional accessibility
952 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- name
953 let n = expandNS syn n_in
955 ds <- option [] (methodsBlock syn)
956 accData acc n (concatMap declared ds)
957 return [PClass doc syn fc cons n cs ds]
958 <?> "type-class declaration"
960 carg :: IdrisParser (Name, PTerm)
961 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
966{- |Parses a type class instance declaration
969 'instance' InstanceName? ConstraintList? Name SimpleExpr* MethodsBlock?
972 InstanceName ::= '[' Name ']';
974instance_ :: SyntaxInfo -> IdrisParser [PDecl]
975instance_ syn = do reserved "instance"; fc <- getFC
976 en <- optional instanceName
977 cs <- constraintList syn
979 args <- many (simpleExpr syn)
980 let sc = PApp fc (PRef fc cn) (map pexp args)
981 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
982 ds <- option [] (methodsBlock syn)
983 return [PInstance syn fc cs cn args t en ds]
984 <?> "instance declaratioN"
985 where instanceName :: IdrisParser Name
986 instanceName = do lchar '['; n_in <- fnName; lchar ']'
987 let n = expandNS syn n_in
992{- | Parses an expression as a whole
993 FullExpr ::= Expr EOF_t;
995fullExpr :: SyntaxInfo -> IdrisParser PTerm
996fullExpr syn = do x <- expr syn
999 return $ desugar syn i x
1002{- |Parses an expression
1005expr :: SyntaxInfo -> IdrisParser PTerm
1006expr syn = do i <- get
1007 buildExpressionParser (table (idris_infixes i)) (expr' syn)
1009{- | Parses either an internally defined expression or
1012Expr' ::= "External (User-defined) Syntax"
1016expr' :: SyntaxInfo -> IdrisParser PTerm
1017expr' syn = try (externalExpr syn)
1018 <|> internalExpr syn
1021{- | Parses a user-defined expression -}
1022externalExpr :: SyntaxInfo -> IdrisParser PTerm
1023externalExpr syn = do i <- get
1024 extensions syn (syntax_rules i)
1025 <?> "user-defined expression"
1027{- | Parses a simple user-defined expression -}
1028simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm
1029simpleExternalExpr syn = do i <- get
1030 extensions syn (filter isSimple (syntax_rules i))
1032 isSimple (Rule (Expr x:xs) _ _) = False
1033 isSimple (Rule (SimpleExpr x:xs) _ _) = False
1034 isSimple (Rule [Keyword _] _ _) = True
1035 isSimple (Rule [Symbol _] _ _) = True
1036 isSimple (Rule (_:xs) _ _) = case last xs of
1042{- | Tries to parse a user-defined expression given a list of syntactic extensions -}
1043extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm
1044extensions syn rules = choice (map (try . extension syn) (filter isValid rules))
1045 <?> "user-defined expression"
1047 isValid :: Syntax -> Bool
1048 isValid (Rule _ _ AnySyntax) = True
1049 isValid (Rule _ _ PatternSyntax) = inPattern syn
1050 isValid (Rule _ _ TermSyntax) = not (inPattern syn)
1053data SynMatch = SynTm PTerm | SynBind Name
1055{- | Tries to parse an expression given a user-defined rule -}
1056extension :: SyntaxInfo -> Syntax -> IdrisParser PTerm
1057extension syn (Rule ssym ptm _)
1058 = do smap <- mapM extensionSymbol ssym
1059 let ns = mapMaybe id smap
1060 return (update ns ptm) -- updated with smap
1062 extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
1063 extensionSymbol (Keyword n) = do reserved (show n); return Nothing
1064 extensionSymbol (Expr n) = do tm <- expr syn
1065 return $ Just (n, SynTm tm)
1066 extensionSymbol (SimpleExpr n) = do tm <- simpleExpr syn
1067 return $ Just (n, SynTm tm)
1068 extensionSymbol (Binding n) = do b <- name
1069 return $ Just (n, SynBind b)
1070 extensionSymbol (Symbol s) = do symbol s
1072 dropn :: Name -> [(Name, a)] -> [(Name, a)]
1074 dropn n ((x,t) : xs) | n == x = xs
1075 | otherwise = (x,t):dropn n xs
1077 updateB :: [(Name, SynMatch)] -> Name -> Name
1078 updateB ns n = case lookup n ns of
1079 Just (SynBind t) -> t
1082 update :: [(Name, SynMatch)] -> PTerm -> PTerm
1083 update ns (PRef fc n) = case lookup n ns of
1086 update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)
1087 update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc)
1088 update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)
1089 (update (dropn n ns) sc)
1090 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
1091 update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)
1092 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)
1093 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)
1094 update ns (PAlternative a as) = PAlternative a (map (update ns) as)
1095 update ns (PHidden t) = PHidden (update ns t)
1096 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
1097 where upd :: [(Name, SynMatch)] -> [PDo] -> [PDo]
1098 upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
1099 upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds
1100 upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)
1101 : upd (dropn n ns) ds
1102 upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t)
1104 upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)
1106 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
1109{- |Parses a (normal) built-in expression
1125internalExpr :: SyntaxInfo -> IdrisParser PTerm
1128 <|> try (matchApp syn)
1129 <|> try (unifyLog syn)
1131 <|> try (simpleExpr syn)
1140{- | Parses a case expression
1142 'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;
1144caseExpr :: SyntaxInfo -> IdrisParser PTerm
1145caseExpr syn = do reserved "case"; fc <- getFC
1146 scr <- expr syn; reserved "of";
1147 opts <- indentedBlock1 (caseOption syn)
1148 return (PCase fc scr opts)
1149 <?> "case expression"
1151{- | Parses a case in a case expression
1153 Expr '=>' Expr Terminator
1156caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
1157caseOption syn = do lhs <- expr (syn { inPattern = True })
1158 symbol "=>"; r <- expr syn
1162{- | Parses a proof block
1164 'proof' OpenBlock Tactic'* CloseBlock
1167proofExpr :: SyntaxInfo -> IdrisParser PTerm
1168proofExpr syn = do reserved "proof"
1169 ts <- indentedBlock (tactic syn)
1173{- | Parses a tactics block
1175 'tactics' OpenBlock Tactic'* CloseBlock
1178tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
1179tacticsExpr syn = do reserved "tactics"
1180 ts <- indentedBlock (tactic syn)
1181 return $ PTactics ts
1184{- | Parses a simple expresion
1189 | 'refl' ('{' Expr '}')?
1203 | {- External (User-defined) Simple Expression -}
1206simpleExpr :: SyntaxInfo -> IdrisParser PTerm
1208 {-try (do symbol "!["; t <- term; lchar ']'; return $ PQuote t)
1209 <|>-} do lchar '?'; x <- name; return (PMetavar x)
1210 <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)
1211 <|> do reserved "refl"; fc <- getFC;
1212 tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';
1214 return (PRefl fc tm)
1218 <|> try (do fc <- getFC
1221 <|> try (listExpr syn)
1222 <|> try (comprehension syn)
1226 bracketed (disallowImp syn)
1227 <|> try (do c <- constant
1229 return (modifyConst syn fc (PConstant c)))
1230 <|> do reserved "Type"; return PType
1231 <|> try (do symbol "_|_"
1234 <|> do lchar '_'; return Placeholder
1235 <|> simpleExternalExpr syn
1239{- |Parses the rest of an expression in braces
1244 | Expr '**' Expr ')'
1247 | Name ':' Expr '**' Expr ')'
1250bracketed :: SyntaxInfo -> IdrisParser PTerm
1256 try (do l <- expr syn
1259 <|> do (l, fc) <- try (do
1264 rs <- sepBy1 (do fc' <- getFC; r <- expr syn; return (r, fc')) (lchar ',')
1266 return $ PPair fc l (mergePairs rs)
1267 <|> do (l, fc) <- try (do
1274 return (PDPair fc l Placeholder r)
1275 <|> try(do fc0 <- getFC
1279 return $ PLam (MN 1000 "ARG") Placeholder
1280 (PApp fc0 (PRef fc0 (UN o)) [pexp l,
1281 pexp (PRef fc0 (MN 1000 "ARG"))]))
1282 <|> try(do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
1283 return $ PLam (MN 1000 "ARG") Placeholder
1284 (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),
1286 <|> try (do ln <- name; lchar ':'
1292 return (PDPair fc (PRef fc ln) lty r))
1293 <?> "end of braced expression"
1294 where mergePairs :: [(PTerm, FC)] -> PTerm
1295 mergePairs [(t, fc)] = t
1296 mergePairs ((t, fc):rs) = PPair fc t (mergePairs rs)
1298-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
1299-- big integer, otherwise try fromInteger and the constants as alternatives.
1300-- a better solution would be to fix fromInteger to work with Integer, as the
1301-- name suggests, rather than Int
1302{-| Finds optimal type for integer constant -}
1303modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
1304modifyConst syn fc (PConstant (BI x))
1305 | not (inPattern syn)
1306 = PAlternative False
1307 (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI (fromInteger x)))]
1309 | otherwise = PAlternative False consts
1311 consts = [ PConstant (BI x)
1312 , PConstant (I (fromInteger x))
1313 , PConstant (B8 (fromInteger x))
1314 , PConstant (B16 (fromInteger x))
1315 , PConstant (B32 (fromInteger x))
1316 , PConstant (B64 (fromInteger x))
1318modifyConst syn fc x = x
1320{- | Parses a list literal expression e.g. [1,2,3]
1331listExpr :: SyntaxInfo -> IdrisParser PTerm
1332listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lchar ']'
1333 return (mkList fc xs)
1334 <?> "list expression"
1336 mkList :: FC -> [PTerm] -> PTerm
1337 mkList fc [] = PRef fc (UN "Nil")
1338 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
1341{- | Parses an alternative expression
1342 Alt ::= '(|' Expr_List '|)';
1346 | Expr' ',' Expr_List
1349alt :: SyntaxInfo -> IdrisParser PTerm
1350alt syn = do symbol "(|"; alts <- sepBy1 (expr' syn) (lchar ','); symbol "|)"
1351 return (PAlternative False alts)
1353{- | Parses a possibly hidden simple expression
1359hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm
1367{- | Parses a matching application expression
1369 SimpleExpr '<==' FnName
1372matchApp :: SyntaxInfo -> IdrisParser PTerm
1373matchApp syn = do ty <- simpleExpr syn
1377 return (PLet (MN 0 "match")
1380 (PRef fc (MN 0 "match")))
1381 <?> "matching application expression"
1383{- | Parses a unification log expression
1385 '%' 'unifyLog' SimpleExpr
1388unifyLog :: SyntaxInfo -> IdrisParser PTerm
1389unifyLog syn = do lchar '%'; reserved "unifyLog";
1390 tm <- simpleExpr syn
1391 return (PUnifyLog tm)
1392 <?> "unification log expression"
1394{- | Parses a function application expression
1396 'mkForeign' Arg Arg*
1400app :: SyntaxInfo -> IdrisParser PTerm
1401app syn = do f <- reserved "mkForeign"
1404 args <- many (do notEndApp; arg syn)
1406 -- mkForeign f args ==>
1407 -- liftPrimIO (\w => mkForeignPrim f args w)
1408 let ap = PApp fc (PRef fc (UN "liftPrimIO"))
1409 [pexp (PLam (MN 0 "w")
1411 (PApp fc (PRef fc (UN "mkForeignPrim"))
1413 [pexp (PRef fc (MN 0 "w"))])))]
1414 return (dslify i ap)
1416 <|> do f <- simpleExpr syn
1418 args <- some (do notEndApp; arg syn)
1420 return (dslify i $ PApp fc f args)
1421 <?> "function application"
1423 dslify :: IState -> PTerm -> PTerm
1424 dslify i (PApp fc (PRef _ f) [a])
1425 | [d] <- lookupCtxt f (idris_dsls i)
1426 = desugar (syn { dsl_info = d }) i (getTm a)
1429{- |Parses a function argument
1436arg :: SyntaxInfo -> IdrisParser PArg
1437arg syn = implicitArg syn
1438 <|> constraintArg syn
1439 <|> do e <- simpleExpr syn
1441 <?> "function argument"
1443{- |Parses an implicit function argument
1445 '{' Name ('=' Expr)? '}'
1448implicitArg :: SyntaxInfo -> IdrisParser PArg
1449implicitArg syn = do lchar '{'
1452 v <- option (PRef fc n) (do lchar '='
1456 <?> "implicit function argument"
1458{- |Parses a constraint argument (for selecting a named type class instance)
1463constraintArg :: SyntaxInfo -> IdrisParser PArg
1464constraintArg syn = do symbol "@{"
1468 <?> "constraint argument"
1471{- |Parses a record field setter expression
1473 'record' '{' FieldTypeList '}';
1477 | FieldType ',' FieldTypeList
1484recordType :: SyntaxInfo -> IdrisParser PTerm
1486 = do reserved "record"
1488 fields <- sepBy1 fieldType (lchar ',')
1491 rec <- optional (simpleExpr syn)
1494 return (PLam (MN 0 "fldx") Placeholder
1495 (applyAll fc fields (PRef fc (MN 0 "fldx"))))
1496 Just v -> return (applyAll fc fields v)
1497 <?> "record setting expression"
1498 where fieldType :: IdrisParser (Name, PTerm)
1499 fieldType = do n <- fnName
1504 applyAll :: FC -> [(Name, PTerm)] -> PTerm -> PTerm
1505 applyAll fc [] x = x
1506 applyAll fc ((n, e) : es) x
1507 = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])
1509{- |Creates setters for record types on necessary functions -}
1510mkType :: Name -> Name
1511mkType (UN n) = UN ("set_" ++ n)
1512mkType (MN 0 n) = MN 0 ("set_" ++ n)
1513mkType (NS n s) = NS (mkType n) s
1515{- |Parses a type signature
1519TypeExpr ::= ConstraintList? Expr;
1521typeExpr :: SyntaxInfo -> IdrisParser PTerm
1522typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []
1524 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
1525 <?> "type signature"
1527{- |Parses a lambda expression
1529 '\\' TypeOptDeclList '=>' Expr
1530 | '\\' SimpleExprList '=>' Expr
1534 | SimpleExpr ',' SimpleExprList
1537lambda :: SyntaxInfo -> IdrisParser PTerm
1538lambda syn = do lchar '\\'
1539 try (do xt <- tyOptDeclList syn
1542 return (bindList PLam xt sc)
1543 <|> (do ps <- sepBy (do fc <- getFC
1545 return (fc, e)) (lchar ',')
1548 return (pmList (zip [0..] ps) sc)))
1549 <?> "lambda expression"
1550 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm
1552 pmList ((i, (fc, x)) : xs) sc
1553 = PLam (MN i "lamp") Placeholder
1554 (PCase fc (PRef fc (MN i "lamp"))
1555 [(x, pmList xs sc)])
1557{- |Parses a term rewrite expression
1559 'rewrite' Expr ('==>' Expr)? 'in' Expr
1562rewriteTerm :: SyntaxInfo -> IdrisParser PTerm
1563rewriteTerm syn = do reserved "rewrite"
1566 giving <- optional (do symbol "==>"; expr' syn)
1567 reserved "in"; sc <- expr syn
1569 (PApp fc (PRef fc (UN "sym")) [pexp prf]) sc
1571 <?> "term rewrite expression"
1573{- |Parses a let binding
1575 'let' Name TypeSig'? '=' Expr 'in' Expr
1576| 'let' Expr' '=' Expr' 'in' Expr
1582let_ :: SyntaxInfo -> IdrisParser PTerm
1583let_ syn = try (do reserved "let"; n <- name;
1584 ty <- option Placeholder (do lchar ':'; expr' syn)
1587 reserved "in"; sc <- expr syn
1588 return (PLet n ty v sc))
1589 <|> (do reserved "let"; fc <- getFC; pat <- expr' (syn { inPattern = True } )
1590 symbol "="; v <- expr syn
1591 reserved "in"; sc <- expr syn
1592 return (PCase fc v [(pat, sc)]))
1595{- |Parses a quote goal
1597 'quoteGoal' Name 'by' Expr 'in' Expr
1600quoteGoal :: SyntaxInfo -> IdrisParser PTerm
1601quoteGoal syn = do reserved "quoteGoal"; n <- name;
1607 return (PGoal fc r n sc)
1608 <?> "quote goal expression"
1610{- |Parses a dependent type signature
1612 '|'? Static? '(' TypeDeclList ')' DocComment '->' Expr
1613 | '|'? Static? '{' TypeDeclList '}' '->' Expr
1614 | '{' 'auto' TypeDeclList '}' '->' Expr
1615 | '{' 'default' TypeDeclList '}' '->' Expr
1616 | '{' 'static' '}' Expr' '->' Expr
1620pi :: SyntaxInfo -> IdrisParser PTerm
1622 do lazy <- if implicitAllowed syn -- laziness is top level only
1623 then option False (do lchar '|'; return True)
1626 (do try(lchar '('); xt <- typeDeclList syn; lchar ')'
1627 doc <- option "" (docComment '^')
1630 return (bindList (PPi (Exp lazy st doc)) xt sc)) <|> (do
1633 when (lazy || (st == Static)) $ fail "auto type constraints can not be lazy or static"
1634 xt <- typeDeclList syn
1638 return (bindList (PPi
1639 (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc)) <|> (do
1641 when (lazy || (st == Static)) $ fail "default tactic constraints can not be lazy or static"
1642 script <- simpleExpr syn
1643 xt <- typeDeclList syn
1647 return (bindList (PPi (TacImp False Dynamic script "")) xt sc)) <|> (do
1653 return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)) <|> (
1654 if implicitAllowed syn then do
1655 xt <- typeDeclList syn
1659 return (bindList (PPi (Imp lazy st "")) xt sc)
1660 else do fail "no implicit arguments allowed here"))
1661 <?> "dependent type signature"
1663{- | Parses a type constraint list
1665 '(' Expr_List ')' '=>'
1669constraintList :: SyntaxInfo -> IdrisParser [PTerm]
1670constraintList syn = try (do lchar '('
1671 tys <- sepBy1 (expr' (disallowImp syn)) (lchar ',')
1675 <|> try (do t <- expr (disallowImp syn)
1679 <?> "type constraint list"
1681{- | Parses a using declaration list
1689 | UsingDecl ',' UsingDeclList'
1697usingDeclList :: SyntaxInfo -> IdrisParser [Using]
1699 = try (sepBy1 (usingDecl syn) (lchar ','))
1700 <|> do ns <- sepBy1 name (lchar ',')
1702 t <- typeExpr (disallowImp syn)
1703 return (map (\x -> UImplicit x t) ns)
1704 <?> "using declaration list"
1706{- |Parses a using declaration
1712usingDecl :: SyntaxInfo -> IdrisParser Using
1713usingDecl syn = try (do x <- fnName
1715 t <- typeExpr (disallowImp syn)
1716 return (UImplicit x t))
1719 return (UConstraint c xs)
1720 <?> "using declaration"
1722{- |Parses a type declaration list
1724 FunctionSignatureList
1728FunctionSignatureList ::=
1730 | Name TypeSig ',' FunctionSignatureList
1733typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
1734typeDeclList syn = try (sepBy1 (do x <- fnName
1736 t <- typeExpr (disallowImp syn)
1739 <|> do ns <- sepBy1 name (lchar ',')
1741 t <- typeExpr (disallowImp syn)
1742 return (map (\x -> (x, t)) ns)
1743 <?> "type declaration list"
1745{- |Parses a type declaration list with optional parameters
1747 NameOrPlaceholder TypeSig?
1748 | NameOrPlaceholder TypeSig? ',' TypeOptDeclList
1751NameOrPlaceHolder ::= Name | '_';
1753tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
1754tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder
1755 t <- option Placeholder (do lchar ':'
1759 <?> "type declaration list"
1760 where nameOrPlaceholder :: IdrisParser Name
1761 nameOrPlaceholder = fnName
1763 return (MN 0 "underscore")
1764 <?> "name or placeholder"
1766{- |Parses a list comprehension
1767Comprehension ::= '[' Expr '|' DoList ']';
1774comprehension :: SyntaxInfo -> IdrisParser PTerm
1780 qs <- sepBy1 (do_ syn) (lchar ',')
1782 return (PDoBlock (map addGuard qs ++
1783 [DoExp fc (PApp fc (PRef fc (UN "return"))
1785 <?> "list comprehension"
1786 where addGuard :: PDo -> PDo
1787 addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
1791{- |Parses a do-block
1792Do' ::= Do KeepTerminator;
1795 'do' OpenBlock Do'+ CloseBlock
1798doBlock :: SyntaxInfo -> IdrisParser PTerm
1801 ds <- indentedBlock (do_ syn)
1802 return (PDoBlock ds)
1805{- |Parses an expression inside a do block
1807 'let' Name TypeSig'? '=' Expr
1808 | 'let' Expr' '=' Expr
1814do_ :: SyntaxInfo -> IdrisParser PDo
1816 = try (do reserved "let"
1818 ty <- option Placeholder (do lchar ':'
1823 return (DoLet fc i ty e))
1824 <|> try (do reserved "let"
1829 return (DoLetP fc i sc))
1830 <|> try (do i <- name
1834 return (DoBind fc i e))
1835 <|> try (do i <- expr' syn
1839 return (DoBindP fc i e))
1840 <|> do e <- expr syn
1843 <?> "do block expression"
1845{- |Parses an expression in idiom brackets
1846Idiom ::= '[|' Expr '|]';
1848idiom :: SyntaxInfo -> IdrisParser PTerm
1854 return (PIdiom fc e)
1855 <?> "expression in idiom brackets"
1857{- |Parses a constant or literal expression
1879constant :: IdrisParser Core.TT.Const
1880constant = do reserved "Integer";return (AType (ATInt ITBig))
1881 <|> do reserved "Int"; return (AType (ATInt ITNative))
1882 <|> do reserved "Char"; return (AType (ATInt ITChar))
1883 <|> do reserved "Float"; return (AType ATFloat)
1884 <|> do reserved "String"; return StrType
1885 <|> do reserved "Ptr"; return PtrType
1886 <|> do reserved "Bits8"; return (AType (ATInt (ITFixed IT8)))
1887 <|> do reserved "Bits16"; return (AType (ATInt (ITFixed IT16)))
1888 <|> do reserved "Bits32"; return (AType (ATInt (ITFixed IT32)))
1889 <|> do reserved "Bits64"; return (AType (ATInt (ITFixed IT64)))
1890 <|> do reserved "Bits8x16"; return (AType (ATInt (ITVec IT8 16)))
1891 <|> do reserved "Bits16x8"; return (AType (ATInt (ITVec IT16 8)))
1892 <|> do reserved "Bits32x4"; return (AType (ATInt (ITVec IT32 4)))
1893 <|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2)))
1894 <|> try (do f <- float; return $ Fl f)
1895 <|> try (do i <- natural; return $ BI i)
1896 <|> try (do s <- stringLiteral; return $ Str s)
1897 <|> try (do c <- charLiteral; return $ Ch c)
1898 <?> "constant or literal"
1900{- |Parses a static modifier
1905static :: IdrisParser Static
1906static = do lchar '['; reserved "static"; lchar ']'; return Static
1908 <?> "static modifier"
1910{- |Parses a record type declaration
1912 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
1914record :: SyntaxInfo -> IdrisParser PDecl
1915record syn = do (doc, acc) <- try (do
1916 doc <- option "" (docComment '|')
1917 acc <- optional accessibility
1923 ty <- typeExpr (allowImp syn)
1924 let tyn = expandNS syn tyn_in
1926 (cdoc, cn, cty, _) <- indentedBlockS (constructor syn)
1927 accData acc tyn [cn]
1928 let rsyn = syn { syn_namespace = show (nsroot tyn) :
1930 let fns = getRecNames rsyn cty
1931 mapM_ (\n -> addAcc n acc) fns
1932 return $ PRecord doc rsyn fc tyn ty cdoc cn cty
1933 <?> "record type declaration"
1935 getRecNames :: SyntaxInfo -> PTerm -> [Name]
1936 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
1937 ++ getRecNames syn sc
1938 getRecNames _ _ = []
1940 toFreeze :: Maybe Accessibility -> Maybe Accessibility
1941 toFreeze (Just Frozen) = Just Hidden
1944{- | Parses data declaration type (normal or codata)
1945DataI ::= 'data' | 'codata';
1947dataI :: IdrisParser Bool
1948dataI = do reserved "data"; return False
1949 <|> do reserved "codata"; return True
1951{- | Parses a data type declaration
1952Data ::= DocComment? Accessibility? DataI FnName TypeSig ExplicitTypeDataRest?
1953 | DocComment? Accessibility? DataI FnName Name* DataRest?
1955Constructor' ::= Constructor KeepTerminator;
1956ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;
1958DataRest ::= '=' SimpleConstructorList Terminator
1961SimpleConstructorList ::=
1963 | SimpleConstructor '|' SimpleConstructorList
1966data_ :: SyntaxInfo -> IdrisParser PDecl
1967data_ syn = do (doc, acc, co) <- try (do
1968 doc <- option "" (docComment '|')
1970 acc <- optional accessibility
1972 return (doc, acc, co))
1977 ty <- typeExpr (allowImp syn)
1978 let tyn = expandNS syn tyn_in
1979 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1981 cons <- indentedBlock (constructor syn)
1982 accData acc tyn (map (\ (_, n, _, _) -> n) cons)
1983 return $ PData doc syn fc co (PDatadecl tyn ty cons))) <|> (do
1985 let ty = bindArgs (map (const PType) args) PType
1986 let tyn = expandNS syn tyn_in
1987 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1988 try (lchar '=') <|> do reserved "where"
1989 let kw = (if co then "co" else "") ++ "data "
1990 let n = show tyn_in ++ " "
1992 let as = concat (intersperse " " $ map show args) ++ " "
1993 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
1994 let ss = concat (intersperse " -> " $ map (const "Type") args)
1995 let fix1 = s ++ as ++ " = ..."
1996 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
1997 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
1998 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
1999 cons <- sepBy1 (simpleConstructor syn) (lchar '|')
2001 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
2002 cons' <- mapM (\ (doc, x, cargs, cfc) ->
2003 do let cty = bindArgs cargs conty
2004 return (doc, x, cty, cfc)) cons
2005 accData acc tyn (map (\ (_, n, _, _) -> n) cons')
2006 return $ PData doc syn fc co (PDatadecl tyn ty cons')))
2007 <?> "data type declaration"
2009 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
2011 mkPApp fc t xs = PApp fc t (map pexp xs)
2012 bindArgs :: [PTerm] -> PTerm -> PTerm
2013 bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
2016{- | Parses a type constructor declaration
2017 Constructor ::= DocComment? FnName TypeSig;
2019constructor :: SyntaxInfo -> IdrisParser (String, Name, PTerm, FC)
2021 = do doc <- option "" (docComment '|')
2022 cn_in <- fnName; fc <- getFC
2023 let cn = expandNS syn cn_in
2025 ty <- typeExpr (allowImp syn)
2026 return (doc, cn, ty, fc)
2029{- | Parses a constructor for simple discriminative union data types
2030 SimpleConstructor ::= FnName SimpleExpr* DocComment?
2032simpleConstructor :: SyntaxInfo -> IdrisParser (String, Name, [PTerm], FC)
2033simpleConstructor syn
2034 = do cn_in <- fnName
2035 let cn = expandNS syn cn_in
2037 args <- many (do notEndApp
2039 doc <- option "" (docComment '^')
2040 return (doc, cn, args, fc)
2043{- | Parses a dsl block declaration
2044DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;
2046dsl :: SyntaxInfo -> IdrisParser PDecl
2047dsl syn = do reserved "dsl"
2049 bs <- indentedBlock (overload syn)
2050 let dsl = mkDSL bs (dsl_info syn)
2053 put (i { idris_dsls = addDef n dsl (idris_dsls i) })
2055 <?> "dsl block declaration"
2056 where mkDSL :: [(String, PTerm)] -> DSL -> DSL
2057 mkDSL bs dsl = let var = lookup "variable" bs
2058 first = lookup "index_first" bs
2059 next = lookup "index_next" bs
2060 leto = lookup "let" bs
2061 lambda = lookup "lambda" bs in
2062 initDSL { dsl_var = var,
2063 index_first = first,
2065 dsl_lambda = lambda,
2068{- | Checks DSL for errors -}
2069-- FIXME: currently does nothing, check if DSL is really sane
2070checkDSL :: DSL -> IdrisParser ()
2071checkDSL dsl = return ()
2073{- | Parses a DSL overload declaration
2074OverloadIdentifier ::= 'let' | Identifier;
2075Overload ::= OverloadIdentifier '=' Expr;
2077overload :: SyntaxInfo -> IdrisParser (String, PTerm)
2078overload syn = do o <- identifier <|> do reserved "let"
2080 if o `notElem` overloadable
2081 then fail $ show o ++ " is not an overloading"
2086 <?> "dsl overload declaratioN"
2087 where overloadable = ["let","lambda","index_first","index_next","variable"]
2089{- | Parse a clause with patterns
2092pattern :: SyntaxInfo -> IdrisParser PDecl
2093pattern syn = do fc <- getFC
2094 clause <- clause syn
2095 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
2098{- | Parse a constant applicative form declaration
2099 CAF ::= 'let' FnName '=' Expr Terminator;
2101caf :: SyntaxInfo -> IdrisParser PDecl
2102caf syn = do reserved "let"
2103 n_in <- fnName; let n = expandNS syn n_in
2108 return (PCAF fc n t)
2109 <?> "constant applicative form declaration"
2111{- | Parse an argument expression
2112 ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
2114argExpr :: SyntaxInfo -> IdrisParser PTerm
2115argExpr syn = let syn' = syn { inPattern = True } in
2116 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
2117 <?> "argument expression"
2119{- | Parse a right hand side of a function
2121 | '?=' RHSName? Expr
2125RHSName ::= '{' FnName '}';
2127rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
2128rhs syn n = do lchar '='; expr syn
2130 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
2133 return (addLet name r)
2134 <|> do reserved "impossible"; return PImpossible
2135 <?> "function right hand side"
2136 where mkN :: Name -> Name
2137 mkN (UN x) = UN (x++"_lemma_1")
2138 mkN (NS x n) = NS (mkN x) n
2141 addLet :: Name -> PTerm -> PTerm
2142 addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)
2143 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
2144 where addLetC (l, r) = (l, addLet nm r)
2145 addLet nm r = (PLet (UN "value") Placeholder r (PMetavar nm))
2147{- |Parses a function clause
2148RHSOrWithBlock ::= RHS WhereOrTerminator
2149 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
2151Clause ::= WExpr+ RHSOrWithBlock
2152 | SimpleExpr '<==' FnName RHS WhereOrTerminator
2153 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
2154 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
2156ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
2157WhereOrTerminator ::= WhereBlock | Terminator;
2159clause :: SyntaxInfo -> IdrisParser PClause
2161 = do wargs <- try (do pushIndent; some (wExpr syn))
2164 n <- case lastParse ist of
2166 Nothing -> fail "Invalid clause"
2168 let ctxt = tt_ctxt ist
2169 let wsyn = syn { syn_namespace = [] }
2170 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2175 return $ PClauseR fc wargs r wheres) <|> (do
2178 wval <- simpleExpr syn
2180 ds <- some $ fnDecl syn
2181 let withs = concat ds
2183 return $ PWithR fc wargs wval withs)
2184 <|> do ty <- try (do pushIndent
2185 ty <- simpleExpr syn
2189 n_in <- fnName; let n = expandNS syn n_in
2192 let ctxt = tt_ctxt ist
2193 let wsyn = syn { syn_namespace = [] }
2194 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2199 let capp = PLet (MN 0 "match")
2202 (PRef fc (MN 0 "match"))
2204 put (ist { lastParse = Just n })
2205 return $ PClause fc n capp [] r wheres
2206 <|> do (l, op) <- try (do
2210 when (op == "=" || op == "?=" ) (fail "infix clause definition with \"=\" and \"?=\" not supported ")
2212 let n = expandNS syn (UN op)
2215 wargs <- many (wExpr syn)
2217 let wsyn = syn { syn_namespace = [] }
2218 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2224 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
2225 put (ist { lastParse = Just n })
2226 return $ PClause fc n capp wargs rs wheres) <|> (do
2229 lchar '(' <?> "parenthesized expression"
2230 wval <- bracketed syn
2232 ds <- some $ fnDecl syn
2235 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
2236 let withs = map (fillLHSD n capp wargs) $ concat ds
2237 put (ist { lastParse = Just n })
2238 return $ PWith fc n capp wargs wval withs)
2240 n_in <- fnName; let n = expandNS syn n_in
2241 cargs <- many (constraintArg syn)
2243 args <- many (try (implicitArg (syn { inPattern = True } ))
2244 <|> (fmap pexp (argExpr syn)))
2245 wargs <- many (wExpr syn)
2246 let capp = PApp fc (PRef fc n)
2250 let ctxt = tt_ctxt ist
2251 let wsyn = syn { syn_namespace = [] }
2252 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2258 put (ist { lastParse = Just n })
2259 return $ PClause fc n capp wargs r wheres) <|> (do
2262 put (ist { lastParse = Just n })
2263 lchar '(' <?> "parenthesized expression"
2264 wval <- bracketed syn
2266 ds <- some $ fnDecl syn
2267 let withs = map (fillLHSD n capp wargs) $ concat ds
2270 return $ PWith fc n capp wargs wval withs)
2271 <?> "function clause"
2273 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
2274 fillLHS n capp owargs (PClauseR fc wargs v ws)
2275 = PClause fc n capp (owargs ++ wargs) v ws
2276 fillLHS n capp owargs (PWithR fc wargs v ws)
2277 = PWith fc n capp (owargs ++ wargs) v
2278 (map (fillLHSD n capp (owargs ++ wargs)) ws)
2281 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
2282 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
2283 fillLHSD n c a x = x
2285{- |Parses with pattern
2286 WExpr ::= '|' Expr';
2288wExpr :: SyntaxInfo -> IdrisParser PTerm
2289wExpr syn = do lchar '|'
2293{- |Parses a where block
2294WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
2296whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
2298 = do reserved "where"
2299 ds <- indentedBlock1 (decl syn)
2300 let dns = concatMap (concatMap declared) ds
2301 return (concat ds, map (\x -> (x, decoration syn x)) dns)
2304{- |Parses a code generation target language name
2313codegen_ :: IdrisParser Codegen
2314codegen_ = do reserved "C"; return ViaC
2315 <|> do reserved "Java"; return ViaJava
2316 <|> do reserved "JavaScript"; return ViaJavaScript
2317 <|> do reserved "Node"; return ViaNode
2318 <|> do reserved "LLVM"; return ViaLLVM
2319 <|> do reserved "Bytecode"; return Bytecode
2320 <?> "code generation language"
2322{- |Parses a compiler directive
2325 | String ',' StringList
2328Directive ::= '%' Directive';
2330Directive' ::= 'lib' CodeGen String_t
2331 | 'link' CodeGen String_t
2332 | 'flag' CodeGen String_t
2333 | 'include' CodeGen String_t
2336 | 'access' Accessibility
2337 | 'default' Totality
2339 | 'dynamic' StringList
2340 | 'language' 'TypeProviders'
2341 | 'language' 'ErrorReflection'
2344directive :: SyntaxInfo -> IdrisParser [PDecl]
2345directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
2346 return [PDirective (do addLib cgn lib
2347 addIBC (IBCLib cgn lib))]
2348 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
2349 return [PDirective (do dirs <- allImportDirs
2350 o <- liftIO $ findInPath dirs obj
2351 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
2352 addObjectFile cgn o)]
2353 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
2354 flag <- stringLiteral
2355 return [PDirective (do addIBC (IBCCGFlag cgn flag)
2357 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
2358 return [PDirective (do addHdr cgn hdr
2359 addIBC (IBCHeader cgn hdr))]
2360 <|> do try (lchar '%' *> reserved "hide"); n <- iName []
2361 return [PDirective (do setAccessibility n Hidden
2362 addIBC (IBCAccess n Hidden))]
2363 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
2364 return [PDirective (do setAccessibility n Frozen
2365 addIBC (IBCAccess n Frozen))]
2366 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
2367 return [PDirective (do i <- get
2368 put(i { default_access = acc }))]
2369 <|> do try (lchar '%' *> reserved "default"); tot <- totality
2371 put (i { default_total = tot } )
2372 return [PDirective (do i <- get
2373 put(i { default_total = tot }))]
2374 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
2375 return [PDirective (setLogLevel (fromInteger i))]
2376 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
2377 return [PDirective (do added <- addDyLib libs
2379 Left lib -> addIBC (IBCDyLib (lib_name lib))
2382 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
2383 return [PDirective (addLangExt ext)]
2386pLangExt :: IdrisParser LanguageExt
2387pLangExt = (reserved "TypeProviders" >> return TypeProviders)
2388 <|> (reserved "ErrorReflection" >> return ErrorReflection)
2390{- | Parses a totality
2391Totality ::= 'partial' | 'total'
2393totality :: IdrisParser Bool
2395 = do reserved "total"; return True
2396 <|> do reserved "partial"; return False
2398{- | Parses a type provider
2399Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;
2401provider :: SyntaxInfo -> IdrisParser [PDecl]
2402provider syn = do try (lchar '%' *> reserved "provide");
2403 lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
2407 return [PProvider syn fc n t e]
2410{- | Parses a transform
2411Transform ::= '%' 'transform' Expr '==>' Expr
2413transform :: SyntaxInfo -> IdrisParser [PDecl]
2414transform syn = do try (lchar '%' *> reserved "transform")
2415 -- leave it unchecked, until we work out what this should
2417-- safety <- option True (do reserved "unsafe"
2423 return [PTransform fc False l r]
2426{- | Parses a tactic script
2427Tactic ::= 'intro' NameList?
2429 | 'refine' Name Imp+
2433 | 'let' Name ':' Expr' '=' Expr
2434 | 'let' Name '=' Expr
2437 | 'applyTactic' Expr
2440 | 'try' Tactic '|' Tactic
2458 | Tactic ';' TacticSeq
2463tactic :: SyntaxInfo -> IdrisParser PTactic
2464tactic syn = do reserved "intro"; ns <- sepBy name (lchar ',')
2466 <|> do reserved "intros"; return Intros
2467 <|> try (do reserved "refine"; n <- name
2469 return $ Refine n imps)
2470 <|> do reserved "refine"; n <- name
2472 return $ Refine n []
2473 <|> do reserved "mrefine"; n <- name
2475 return $ MatchRefine n
2476 <|> do reserved "rewrite"; t <- expr syn;
2478 return $ Rewrite (desugar syn i t)
2479 <|> do reserved "equiv"; t <- expr syn;
2481 return $ Equiv (desugar syn i t)
2482 <|> try (do reserved "let"; n <- name; lchar ':';
2483 ty <- expr' syn; lchar '='; t <- expr syn;
2485 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
2486 <|> try (do reserved "let"; n <- name; lchar '=';
2489 return $ LetTac n (desugar syn i t))
2490 <|> do reserved "focus"; n <- name
2492 <|> do reserved "exact"; t <- expr syn;
2494 return $ Exact (desugar syn i t)
2495 <|> do reserved "applyTactic"; t <- expr syn;
2497 return $ ApplyTactic (desugar syn i t)
2498 <|> do reserved "reflect"; t <- expr syn;
2500 return $ Reflect (desugar syn i t)
2501 <|> do reserved "fill"; t <- expr syn;
2503 return $ Fill (desugar syn i t)
2504 <|> do reserved "try"; t <- tactic syn;
2511 ts <- sepBy1 (tactic syn) (lchar ';')
2513 return $ TSeq t (mergeSeq ts)
2514 <|> do reserved "compute"; return Compute
2515 <|> do reserved "trivial"; return Trivial
2516 <|> do reserved "solve"; return Solve
2517 <|> do reserved "attack"; return Attack
2518 <|> do reserved "state"; return ProofState
2519 <|> do reserved "term"; return ProofTerm
2520 <|> do reserved "undo"; return Undo
2521 <|> do reserved "qed"; return Qed
2522 <|> do reserved "abandon"; return Abandon
2523 <|> do lchar ':'; reserved "q"; return Abandon
2526 imp :: IdrisParser Bool
2527 imp = do lchar '?'; return False
2528 <|> do lchar '_'; return True
2529 mergeSeq :: [PTactic] -> PTactic
2531 mergeSeq (t:ts) = TSeq t (mergeSeq ts)
2533{- | Parses a tactic as a whole -}
2534fullTactic :: SyntaxInfo -> IdrisParser PTactic
2535fullTactic syn = do t <- tactic syn
2539{- * Loading and parsing -}
2540{- | Parses an expression from input -}
2541parseExpr :: IState -> String -> Result PTerm
2542parseExpr st = parseString (runInnerParser (evalStateT (fullExpr defaultSyntax) st)) (Directed (UTF8.fromString "(input)") 0 0 0 0)
2544{- | Parses a tactic from input -}
2545parseTactic :: IState -> String -> Result PTactic
2546parseTactic st = parseString (runInnerParser (evalStateT (fullTactic defaultSyntax) st)) (Directed (UTF8.fromString "(input)") 0 0 0 0)
2548-- | Parse module header and imports
2549parseImports :: FilePath -> String -> Idris ([String], [String], Maybe Delta)
2550parseImports fname input
2552 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
2553 Failure err -> fail (show err)
2554 Success (x, i) -> do -- Discard state updates (there should be
2557 where imports :: IdrisParser (([String], [String], Maybe Delta), IState)
2558 imports = do whiteSpace
2559 mname <- moduleHeader
2562 isEof <- lookAheadMatches eof
2567 return ((mname, ps, mrk'), i)
2570-- | A program is a list of declarations, possibly with associated
2571-- documentation strings.
2572parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
2574parseProg syn fname input mrk
2576 case parseString (runInnerParser (evalStateT mainProg i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
2577 Failure doc -> do iputStrLn (show doc)
2578 -- FIXME: Get error location from trifecta
2579 --let errl = sourceLine (errorPos err)
2581 putIState (i { errLine = Just 0 }) -- Just errl })
2583 Success (x, i) -> do putIState i
2585 where mainProg :: IdrisParser ([PDecl], IState)
2586 mainProg = case mrk of
2587 Nothing -> do i <- get; return ([], i)
2594-- | Collect 'PClauses' with the same function name
2595collect :: [PDecl] -> [PDecl]
2596collect (c@(PClauses _ o _ _) : ds)
2597 = clauses (cname c) [] (c : ds)
2598 where clauses :: Maybe Name -> [PClause] -> [PDecl] -> [PDecl]
2599 clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)
2600 | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds
2601 clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds)
2602 | n == n' = clauses j (PWith fc' n' l ws r (collect w) : acc) ds
2603 clauses (Just n) acc xs = PClauses (fcOf c) o n (reverse acc) : collect xs
2604 clauses Nothing acc (x:xs) = collect xs
2605 clauses Nothing acc [] = []
2607 cname :: PDecl -> Maybe Name
2608 cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n
2609 cname (PClauses fc _ _ [PWith _ n _ _ _ _]) = Just n
2610 cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing
2611 cname (PClauses fc _ _ [PWithR _ _ _ _]) = Nothing
2613 fcOf (PClauses fc _ _ _) = fc
2614collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
2615collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds
2616collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds
2617collect (PClass doc f s cs n ps ds : ds')
2618 = PClass doc f s cs n ps (collect ds) : collect ds'
2619collect (PInstance f s cs n ps t en ds : ds')
2620 = PInstance f s cs n ps t en (collect ds) : collect ds'
2621collect (d : ds) = d : collect ds
2624{- | Load idris module -}
2625loadModule :: FilePath -> Idris String
2627 = idrisCatch (do i <- getIState
2628 let file = takeWhile (/= ' ') f
2629 ibcsd <- valIBCSubDir i
2630 ids <- allImportDirs
2631 fp <- liftIO $ findImport ids ibcsd file
2632 if file `elem` imported i
2633 then iLOG $ "Already read " ++ file
2634 else do putIState (i { imported = file : imported i })
2636 IDR fn -> loadSource False fn
2637 LIDR fn -> loadSource True fn
2639 idrisCatch (loadIBC fn)
2640 (\c -> do iLOG $ fn ++ " failed " ++ show c
2642 IDR sfn -> loadSource False sfn
2643 LIDR sfn -> loadSource True sfn)
2644 let (dir, fh) = splitFileName file
2645 return (dropExtension fh))
2646 (\e -> do let msg = show e
2647 setErrLine (getErrLine msg)
2651{- | Load idris code from file -}
2652loadFromIFile :: IFileType -> Idris ()
2653loadFromIFile i@(IBC fn src)
2654 = do iLOG $ "Skipping " ++ getSrcFile i
2655 idrisCatch (loadIBC fn)
2656 (\c -> do fail $ fn ++ " failed " ++ show c)
2658 getSrcFile (IDR fn) = fn
2659 getSrcFile (LIDR fn) = fn
2660 getSrcFile (IBC f src) = getSrcFile src
2662loadFromIFile (IDR fn) = loadSource' False fn
2663loadFromIFile (LIDR fn) = loadSource' True fn
2665{-| Load idris source code and show error if something wrong happens -}
2666loadSource' :: Bool -> FilePath -> Idris ()
2668 = idrisCatch (loadSource lidr r)
2669 (\e -> do let msg = show e
2670 setErrLine (getErrLine msg)
2673{- | Load Idris source code-}
2674loadSource :: Bool -> FilePath -> Idris ()
2676 = do iLOG ("Reading " ++ f)
2678 let def_total = default_total i
2679 file_in <- liftIO $ readFile f
2680 file <- if lidr then tclift $ unlit f file_in else return file_in
2681 (mname, modules, pos) <- parseImports f file
2683 putIState (i { default_access = Hidden })
2684 clearIBC -- start a new .ibc file
2685 mapM_ (addIBC . IBCImport) modules
2686 ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
2688 unless (null ds') $ do
2689 let ds = namespaces mname ds'
2690 logLvl 3 (dumpDecls ds)
2692 logLvl 10 (show (toAlist (idris_implicits i)))
2693 logLvl 3 (show (idris_infixes i))
2694 -- Now add all the declarations to the context
2696 when v $ iputStrLn $ "Type checking " ++ f
2697 -- we totality check after every Mutual block, so if
2698 -- anything is a single definition, wrap it in a
2699 -- mutual block on its own
2700 elabDecls toplevel (map toMutual ds)
2702 -- simplify every definition do give the totality checker
2704 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
2705 updateContext (simplifyCasedef n))
2706 (map snd (idris_totcheck i))
2707 -- build size change graph from simplified definitions
2708 iLOG "Totality checking"
2710 mapM_ buildSCG (idris_totcheck i)
2711 mapM_ checkDeclTotality (idris_totcheck i)
2712 iLOG ("Finished " ++ f)
2713 ibcsd <- valIBCSubDir i
2714 iLOG "Universe checking"
2716 let ibc = ibcPathNoFallback ibcsd f
2718 addHides (hide_list i)
2721 idrisCatch (do writeIBC f ibc; clearIBC)
2722 (\c -> return ()) -- failure is harmless
2724 putIState (i { default_total = def_total,
2729 namespaces :: [String] -> [PDecl] -> [PDecl]
2730 namespaces [] ds = ds
2731 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
2733 toMutual :: PDecl -> PDecl
2734 toMutual m@(PMutual _ d) = m
2735 toMutual x = let r = PMutual (FC "single mutual" 0) [x] in
2737 PClauses _ _ _ _ -> r
2738 PClass _ _ _ _ _ _ _ -> r
2739 PInstance _ _ _ _ _ _ _ _ -> r
2742{- | Adds names to hide list -}
2743addHides :: [(Name, Maybe Accessibility)] -> Idris ()
2744addHides xs = do i <- getIState
2745 let defh = default_access i
2746 let (hs, as) = partition isNothing xs
2749 (map (\ (n, _) -> (n, defh)) hs ++
2750 map (\ (n, Just a) -> (n, a)) as)
2751 where isNothing (_, Nothing) = True
2754 doHide (n, a) = do setAccessibility n a
2755 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