@@ -1,13 +1,22 @@
1−{-# LANGUAGE PatternGuards, ScopedTypeVariables #-}
1+{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
2−-- | Parse the full Idris language.
3module Idris.Parser where
2module Idris.Parser where
4+import Prelude hiding (pi)
6+import Text.Trifecta.Delta
7+import Text.Trifecta hiding (span, token, whiteSpace, stringLiteral, charLiteral, natural, symbol, char, string)
8+import Text.Parser.LookAhead
9+import Text.Parser.Expression
10+import qualified Text.Parser.Token as Tok
11+import qualified Text.Parser.Char as Chr
12+import qualified Text.Parser.Token.Highlight as Hi
5import Idris.AbsSyntax
14import Idris.AbsSyntax
6import Idris.DSL
15import Idris.DSL
7import Idris.Imports
16import Idris.Imports
8import Idris.Error
17import Idris.Error
9import Idris.ElabDecls
18import Idris.ElabDecls
10−import Idris.ElabTerm
19+import Idris.ElabTerm hiding (namespace, params)
11import Idris.Coverage
20import Idris.Coverage
12import Idris.IBC
21import Idris.IBC
13import Idris.Unlit
22import Idris.Unlit
@@ -16,443 +25,614 @@ import Paths_idris
17import Util.DynamicLinker
26import Util.DynamicLinker
19−import Core.CoreParser
20import Core.TT
28import Core.TT
21import Core.Evaluate
29import Core.Evaluate
23−import Text.Parsec
31+import Control.Applicative
24−import Text.Parsec.Error
32+import Control.Monad
25−import Text.Parsec.Expr
33+import Control.Monad.State.Strict
26−import Text.Parsec.Language
27−import Text.Parsec.String
28−import qualified Text.Parsec.Token as PTok
36+import qualified Data.List.Split as Spl
30import Data.List
37import Data.List
31−import Data.List.Split(splitOn)
38+import Data.Monoid
32−import Control.Monad.State
39+import Data.Char
33−import Control.Monad.Error
40+import qualified Data.HashSet as HS
41+import qualified Data.Text as T
42+import qualified Data.ByteString.UTF8 as UTF8
34import Debug.Trace
44import Debug.Trace
36import System.FilePath
46import System.FilePath
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
59+type IdrisParser = StateT IState Parser
61+-- | Generalized monadic parsing constraint type
62+type 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
66+lexeme :: MonadicParsing m => m a -> m a
67+lexeme p = p <* whiteSpace
69+-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)
70+simpleWhiteSpace :: MonadicParsing m => m ()
71+simpleWhiteSpace = satisfy isSpace *> pure ()
73+-- | Checks if a charcter is end of line
76+isEol '\0' = True -- Check eof too
79+-- | Checks if a character is a documentation comment marker
80+isDocCommentMarker :: Char -> Bool
81+isDocCommentMarker '|' = True
82+isDocCommentMarker '^' = True
83+isDocCommentMarker _ = False
85+{- | Consumes a single-line comment
86+ SingleLineComment_t ::= '--' EOL_t
87+ | '--' ~DocCommentMarker_t ~EOL_t* EOL_t
90+singleLineComment :: MonadicParsing m => m ()
91+singleLineComment = try (string "--" *> satisfy isEol *> pure ())
92+ <|> try (string "--" *> satisfy (not . isDocCommentMarker) *> many (satisfy (not . isEol)) *> (satisfy isEol <?> "end of line") *> pure ())
93+ <?> "single-line comment"
95+{- | Consumes a multi-line comment
96+ MultiLineComment_t ::=
98+ | '{ -' ~DocCommentMarker_t InCommentChars_t
101+ InCommentChars_t ::=
103+ | MultiLineComment_t InCommentChars_t
104+ | ~'- }'+ InCommentChars_t
108+multiLineComment :: MonadicParsing m => m ()
109+multiLineComment = try (string "{-" *> (string "-}") *> pure ())
110+ <|> try (string "{-" *> satisfy (not . isDocCommentMarker) *> inCommentChars)
111+ <?> "multi-line comment"
112+ where inCommentChars :: MonadicParsing m => m ()
113+ inCommentChars = try (string "-}" *> pure ())
114+ <|> try (multiLineComment *> inCommentChars)
115+ <|> try (skipSome (noneOf startEnd) *> inCommentChars)
116+ <|> oneOf startEnd *> inCommentChars
117+ <?> "end of comment"
121+{-| Parses a documentation comment (similar to haddoc) given a marker character
122+ DocComment_t ::= '--' DocCommentMarker_t ~EOL_t* EOL_t
123+ | '{ -' DocCommentMarket_t ~'- }'* '- }'
126+docComment :: MonadicParsing m => Char -> m String
127+docComment marker | isDocCommentMarker marker = do dc <- docComment' marker; return (T.unpack $ T.strip $ T.pack dc)
128+ | otherwise = fail "internal error: tried to parse a documentation comment with invalid marker"
129+ where docComment' :: MonadicParsing m => Char -> m String
130+ docComment' marker = string "--" *> char marker *> many (satisfy (not . isEol)) <* satisfy isEol
131+ <|> string "{-" *> char marker *> (manyTill anyChar (try (string "-}")) <?> "end of comment")
132+ <?> "documentation comment"
134+-- | Consumes whitespace (and comments)
135+whiteSpace :: MonadicParsing m => m ()
136+whiteSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
138+-- | Parses a string literal
139+stringLiteral :: MonadicParsing m => m String
140+stringLiteral = lexeme $ Tok.stringLiteral
142+-- | Parses a char literal
143+charLiteral :: MonadicParsing m => m Char
144+charLiteral = lexeme $ Tok.charLiteral
146+-- | Parses a natural number
147+natural :: MonadicParsing m => m Integer
148+natural = lexeme $ Tok.natural
150+-- | Parses an integral number
151+integer :: MonadicParsing m => m Integer
152+integer = lexeme $ Tok.integer
154+-- | Parses a floating point number
155+float :: MonadicParsing m => m Double
156+float = lexeme $ Tok.double
158+{- * Symbols, identifiers, names and operators -}
161+-- | Idris Style for parsing identifiers/reserved keywords
162+idrisStyle :: MonadicParsing m => IdentifierStyle m
163+idrisStyle = IdentifierStyle _styleName _styleStart _styleLetter _styleReserved Hi.Identifier Hi.ReservedIdentifier
164+ where _styleName = "Idris"
165+ _styleStart = satisfy isAlpha
166+ _styleLetter = satisfy isAlphaNum <|> oneOf "_'" <|> (lchar '.')
167+ _styleReserved = HS.fromList ["let", "in", "data", "codata", "record", "Type",
168+ "do", "dsl", "import", "impossible",
169+ "case", "of", "total", "partial", "mutual",
170+ "infix", "infixl", "infixr", "rewrite",
171+ "where", "with", "syntax", "proof", "postulate",
172+ "using", "namespace", "class", "instance",
173+ "public", "private", "abstract", "implicit",
175+ "Int", "Integer", "Float", "Char", "String", "Ptr",
176+ "Bits8", "Bits16", "Bits32", "Bits64",
177+ "Bits8x16", "Bits16x8", "Bits32x4", "Bits64x2"]
179+char :: MonadicParsing m => Char -> m Char
182+string :: MonadicParsing m => String -> m String
185+-- | Parses a character as a lexeme
186+lchar :: MonadicParsing m => Char -> m Char
187+lchar = lexeme . char
189+-- | Parses string as a lexeme
190+symbol :: MonadicParsing m => String -> m String
191+symbol = lexeme . Tok.symbol
193+-- | Parses a reserved identifier
194+reserved :: MonadicParsing m => String -> m ()
195+reserved = lexeme . Tok.reserve idrisStyle
197+-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
198+-- | Parses a reserved operator
199+reservedOp :: MonadicParsing m => String -> m ()
200+reservedOp name = lexeme $ try $
202+ notFollowedBy (operatorLetter) <?> ("end of " ++ show name)
204+-- | Parses an identifier as a lexeme
205+identifier :: MonadicParsing m => m String
206+identifier = lexeme $ Tok.ident idrisStyle
208+-- | Parses an identifier with possible namespace as a name
209+iName :: MonadicParsing m => [String] -> m Name
210+iName bad = maybeWithNS identifier False bad <?> "name"
212+-- | Parses an string possibly prefixed by a namespace
213+maybeWithNS :: MonadicParsing m => m String -> Bool -> [String] -> m Name
214+maybeWithNS parser ascend bad = do
215+ i <- option "" (lookAhead identifier)
216+ when (i `elem` bad) $ unexpected "reserved identifier"
217+ let transf = if ascend then id else reverse
218+ (x, xs) <- choice (transf (parserNoNS parser : parsersNS parser i))
219+ return $ mkName (x, xs)
220+ where parserNoNS :: MonadicParsing m => m String -> m (String, String)
221+ parserNoNS parser = do x <- parser; return (x, "")
222+ parserNS :: MonadicParsing m => m String -> String -> m (String, String)
223+ parserNS parser ns = do xs <- string ns; lchar '.'; x <- parser; return (x, xs)
224+ parsersNS :: MonadicParsing m => m String -> String -> [m (String, String)]
225+ parsersNS parser i = [try (parserNS parser ns) | ns <- (initsEndAt (=='.') i)]
228+name :: IdrisParser Name
230+ iName (syntax_keywords i)
234+{- | List of all initial segments in ascending order of a list. Every such
235+ initial segment ends right before an element satisfying the given
238+initsEndAt :: (a -> Bool) -> [a] -> [[a]]
240+initsEndAt p (x:xs) | p x = [] : x_inits_xs
241+ | otherwise = x_inits_xs
242+ where x_inits_xs = [x : cs | cs <- initsEndAt p xs]
245+{- | Create a `Name' from a pair of strings representing a base name and its
248+mkName :: (String, String) -> Name
249+mkName (n, "") = UN n
250+mkName (n, ns) = NS (UN n) (reverse (parseNS ns))
251+ where parseNS x = case span (/= '.') x of
253+ (x, '.':y) -> x : parseNS y
255+operatorLetter :: MonadicParsing m => m Char
256+operatorLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
258+-- | Parses an operator
259+operator :: MonadicParsing m => m String
260+operator = lexeme . some $ operatorLetter
262+{- * Position helpers -}
263+{- | Get filename from position (returns "(interactive)" when no source file is given) -}
264+fileName :: Delta -> String
265+fileName (Directed fn _ _ _ _) = UTF8.toString fn
266+fileName _ = "(interactive)"
268+{- | Get line number from position -}
269+lineNum :: Delta -> Int
270+lineNum (Lines l _ _ _) = fromIntegral l + 1
271+lineNum (Directed _ l _ _ _) = fromIntegral l + 1
273+{- | Get file position as FC -}
274+getFC :: MonadicParsing m => m FC
275+getFC = do s <- position
276+ let (dir, file) = splitFileName (fileName s)
277+ let f = if dir == addTrailingPathSeparator "." then file else fileName s
278+ return $ FC f (lineNum s)
281+-- | Bind constraints to term
282+bindList :: (Name -> PTerm -> PTerm -> PTerm) -> [(Name, PTerm)] -> PTerm -> PTerm
283+bindList b [] sc = sc
284+bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
38−type TokenParser a = PTok.TokenParser a
286+{- |Creates table for fixtiy declarations to build expression parser using
39−
287+ pre-build and user-defined operator/fixity declarations -}
40−type IParser = GenParser Char IState
288+table :: [FixDecl] -> OperatorTable IdrisParser PTerm
42−lexer :: TokenParser IState
290+ = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
43−lexer = idrisLexer
291+ [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]
44−
292+ ++ toTable (reverse fixes) ++
45−whiteSpace = PTok.whiteSpace lexer
293+ [[backtick],
46−lexeme = PTok.lexeme lexer
294+ [binary "=" PEq AssocLeft],
47−symbol = PTok.symbol lexer
295+ [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
48−natural = PTok.natural lexer
49−parens = PTok.parens lexer
50−semi = PTok.semi lexer
51−comma = PTok.comma lexer
52−identifier = PTok.identifier lexer
53−reserved = PTok.reserved lexer
54−operator = PTok.operator lexer
55−reservedOp = PTok.reservedOp lexer
56−integer = PTok.integer lexer
57−float = PTok.float lexer
58−strlit = PTok.stringLiteral lexer
59−chlit = PTok.charLiteral lexer
62−fixErrorMsg :: String -> [String] -> String
297+{- |Calculates table for fixtiy declarations -}
63−fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)
298+toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm
299+toTable fs = map (map toBin)
300+ (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
301+ where toBin (Fix (PrefixN _) op) = prefix op
302+ (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
304+ = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
305+ assoc (Infixl _) = AssocLeft
306+ assoc (Infixr _) = AssocRight
307+ assoc (InfixN _) = AssocNone
65−-- Loading modules
309+{- |Binary operator -}
310+binary :: String -> (FC -> PTerm -> PTerm -> PTerm) -> Assoc -> Operator IdrisParser PTerm
311+binary name f = Infix (do fc <- getFC
313+ doc <- option "" (docComment '^')
67−loadModule :: FilePath -> Idris String
316+{- |Prefix operator -}
68−loadModule f
317+prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm
69− = idrisCatch (do i <- getIState
318+prefix name f = Prefix (do reservedOp name
70− let file = takeWhile (/= ' ') f
319+ fc <- getFC
71− ibcsd <- valIBCSubDir i
320+ return (f fc))
73− fp <- liftIO $ findImport ids ibcsd file
74− if file `elem` imported i
75− then iLOG $ "Already read " ++ file
76− else do putIState (i { imported = file : imported i })
78− IDR fn -> loadSource False fn
79− LIDR fn -> loadSource True fn
81− idrisCatch (loadIBC fn)
82− (\c -> do iLOG $ fn ++ " failed " ++ show c
84− IDR sfn -> loadSource False sfn
85− LIDR sfn -> loadSource True sfn)
86− let (dir, fh) = splitFileName file
87− return (dropExtension fh))
88− (\e -> do let msg = show e
89− setErrLine (getErrLine msg)
93−loadFromIFile :: IFileType -> Idris ()
322+{- |Backtick operator -}
94−loadFromIFile i@(IBC fn src)
323+backtick :: Operator IdrisParser PTerm
95− = do iLOG $ "Skipping " ++ getSrcFile i
324+backtick = Infix (do lchar '`'; n <- fnName
96− idrisCatch (loadIBC fn)
325+ lchar '`'
97− (\c -> do fail $ fn ++ " failed " ++ show c)
326+ fc <- getFC
98−-- loadFromIFile src)
327+ return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
100− getSrcFile (IDR fn) = fn
101− getSrcFile (LIDR fn) = fn
102− getSrcFile (IBC f src) = getSrcFile src
104−loadFromIFile (IDR fn) = loadSource' False fn
329+-- | Allow implicit type declarations
105−loadFromIFile (LIDR fn) = loadSource' True fn
330+allowImp :: SyntaxInfo -> SyntaxInfo
331+allowImp syn = syn { implicitAllowed = True }
107−loadSource' lidr r
333+-- | Disallow implicit type declarations
108− = idrisCatch (loadSource lidr r)
334+disallowImp :: SyntaxInfo -> SyntaxInfo
109− (\e -> do let msg = show e
335+disallowImp syn = syn { implicitAllowed = False }
110− setErrLine (getErrLine msg)
113−loadSource :: Bool -> FilePath -> Idris ()
337+-- | Adds accessibility option for function
114−loadSource lidr f
338+addAcc :: Name -> Maybe Accessibility -> IdrisParser ()
115− = do iLOG ("Reading " ++ f)
339+addAcc n a = do i <- get
116− i <- getIState
340+ put (i { hide_list = (n, a) : hide_list i })
117− let def_total = default_total i
118− file_in <- liftIO $ readFile f
119− file <- if lidr then tclift $ unlit f file_in else return file_in
120− (mname, modules, rest, pos) <- parseImports f file
122− putIState (i { default_access = Hidden })
123−-- mapM_ loadModule modules
124− clearIBC -- start a new .ibc file
125− mapM_ (addIBC . IBCImport) modules
126− ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
128− unless (null ds') $ do
129− let ds = namespaces mname ds'
130− logLvl 3 (dumpDecls ds)
132− logLvl 10 (show (toAlist (idris_implicits i)))
133− logLvl 3 (show (idris_infixes i))
134− -- Now add all the declarations to the context
136− when v $ iputStrLn $ "Type checking " ++ f
137− -- we totality check after every Mutual block, so if
138− -- anything is a single definition, wrap it in a
139− -- mutual block on its own
140− elabDecls toplevel (map toMutual ds)
142− -- simplify every definition do give the totality checker
144− mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
145− updateContext (simplifyCasedef n))
146− (map snd (idris_totcheck i))
147− -- build size change graph from simplified definitions
148− iLOG "Totality checking"
150− mapM_ buildSCG (idris_totcheck i)
151− mapM_ checkDeclTotality (idris_totcheck i)
152− iLOG ("Finished " ++ f)
153− ibcsd <- valIBCSubDir i
154− iLOG "Universe checking"
156− let ibc = ibcPathNoFallback ibcsd f
158− addHides (hide_list i)
161− idrisCatch (do writeIBC f ibc; clearIBC)
162− (\c -> return ()) -- failure is harmless
164− putIState (i { default_total = def_total,
169− namespaces [] ds = ds
170− namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
172− toMutual m@(PMutual _ d) = m
342+{- | Add accessbility option for data declarations
173− toMutual x = let r = PMutual (FC "single mutual" 0) [x] in
343+ (works for classes too - 'abstract' means the data/class is visible but members not) -}
174− case x of
344+accData :: Maybe Accessibility -> Name -> [Name] -> IdrisParser ()
175− PClauses _ _ _ _ -> r
345+accData (Just Frozen) n ns = do addAcc n (Just Frozen)
176− PClass _ _ _ _ _ _ _ -> r
346+ mapM_ (\n -> addAcc n (Just Hidden)) ns
177− PInstance _ _ _ _ _ _ _ _ -> r
347+accData a n ns = do addAcc n a
178− _ -> x
348+ mapM_ (`addAcc` a) ns
180−addHides :: [(Name, Maybe Accessibility)] -> Idris ()
181−addHides xs = do i <- getIState
182− let defh = default_access i
183− let (hs, as) = partition isNothing xs
186− (map (\ (n, _) -> (n, defh)) hs ++
187− map (\ (n, Just a) -> (n, a)) as)
188− where isNothing (_, Nothing) = True
191− doHide (n, a) = do setAccessibility n a
351+{- * Error reporting helpers -}
192− addIBC (IBCAccess n a)
352+{- | Error message with possible fixes list -}
353+fixErrorMsg :: String -> [String] -> String
354+fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)
194−parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"
356+{- * Layout helpers -}
195−parseTac i = runParser (do t <- pTactic defaultSyntax
197− return t) i "(proof)"
199−parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)
358+-- | Push indentation to stack
200−parseImports fname input
359+pushIndent :: IdrisParser ()
201− = do i <- getIState
360+pushIndent = do pos <- position
202− case runParser (do whiteSpace
361+ ist <- get
203− mname <- pHeader
362+ put (ist { indent_stack = (fromIntegral (column pos) + 1) : indent_stack ist })
207− return ((mname, ps, rest, pos), i)) i fname input of
208− Left err -> fail (show err)
209− Right (x, i) -> do -- Discard state updates (there should be
213−pHeader :: IParser [String]
214−pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')
215− return (parseName i))
217− where parseName x = case span (/='.') x of
219− (x, '.':y) -> x : parseName y
221−pushIndent :: IParser ()
364+-- | Pops indentation from stack
222−pushIndent = do pos <- getPosition
365+popIndent :: IdrisParser ()
223− ist <- getState
366+popIndent = do ist <- get
367+ let (x : xs) = indent_stack ist
224− setState (ist { indent_stack = sourceColumn pos :
368+ put (ist { indent_stack = xs })
227−lastIndent :: IParser Int
370+-- | Gets current indentation
228−lastIndent = do ist <- getState
371+indent :: IdrisParser Int
229− case indent_stack ist of
372+indent = liftM ((+1) . fromIntegral . column) position
230− (x : xs) -> return x
233−indent :: IParser Int
374+-- | Gets last indentation
234−indent = liftM sourceColumn getPosition
375+lastIndent :: IdrisParser Int
376+lastIndent = do ist <- get
377+ case indent_stack ist of
378+ (x : xs) -> return x
381+-- | Applies parser in an indented position
382+indented :: IdrisParser a -> IdrisParser a
383+indented p = notEndBlock *> p <* keepTerminator
385+-- | Applies parser to get a block (which has possibly indented statements)
386+indentedBlock :: IdrisParser a -> IdrisParser [a]
387+indentedBlock p = do openBlock
389+ res <- many (indented p)
394+-- | Applies parser to get a block with at least one statement (which has possibly indented statements)
395+indentedBlock1 :: IdrisParser a -> IdrisParser [a]
396+indentedBlock1 p = do openBlock
398+ res <- some (indented p)
236−popIndent :: IParser ()
403+-- | Applies parser to get a block with exactly one (possibly indented) statement
237−popIndent = do ist <- getState
404+indentedBlockS :: IdrisParser a -> IdrisParser a
238− let (x : xs) = indent_stack ist
405+indentedBlockS p = do openBlock
239− setState (ist { indent_stack = xs })
406+ pushIndent
240−
407+ res <- indented p
413+-- | Checks if the following character matches provided parser
414+lookAheadMatches :: MonadicParsing m => m a -> m Bool
415+lookAheadMatches p = do match <- lookAhead (optional p)
416+ return $ isJust match
418+-- | Parses a start of block
241−openBlock :: IParser ()
419+openBlock :: IdrisParser ()
242−openBlock = do lchar '{'
420+openBlock = do lchar '{'
243− ist <- getState
421+ ist <- get
244− setState (ist { brace_stack = Nothing : brace_stack ist })
422+ put (ist { brace_stack = Nothing : brace_stack ist })
245− <|> do ist <- getState
423+ <|> do ist <- get
246− lvl' <- indent
424+ lvl' <- indent
247− -- if we're not indented further, it's an empty block, so
425+ -- if we're not indented further, it's an empty block, so
248− -- increment lvl to ensure we get to the end
426+ -- increment lvl to ensure we get to the end
249− let lvl = case brace_stack ist of
427+ let lvl = case brace_stack ist of
250− Just lvl_old : _ ->
428+ Just lvl_old : _ ->
251− if lvl' <= lvl_old then lvl_old+1
429+ if lvl' <= lvl_old then lvl_old+1
252− else lvl'
430+ else lvl'
253− [] -> if lvl' == 1 then 2 else lvl'
431+ [] -> if lvl' == 1 then 2 else lvl'
254− _ -> lvl'
432+ _ -> lvl'
255− setState (ist { brace_stack = Just lvl : brace_stack ist })
433+ put (ist { brace_stack = Just lvl : brace_stack ist })
256−
434+ <?> "start of block"
436+-- | Parses an end of block
257−closeBlock :: IParser ()
437+closeBlock :: IdrisParser ()
258−closeBlock = do ist <- getState
438+closeBlock = do ist <- get
259 bs <- case brace_stack ist of
439 bs <- case brace_stack ist of
260 [] -> eof >> return []
440 [] -> eof >> return []
261− Nothing : xs -> (lchar '}' >> return xs) <|> (eof >> return [])
441+ Nothing : xs -> lchar '}' >> return xs <?> "end of block"
262 Just lvl : xs -> (do i <- indent
442 Just lvl : xs -> (do i <- indent
263− inp <- getInput
443+ isParen <- lookAheadMatches (char ')')
264−-- trace (show (take 10 inp, i, lvl)) $
265− if i >= lvl && take 1 inp /= ")"
444+ if i >= lvl && not isParen
266− then fail "Not end of block"
445+ then fail "not end of block"
267− else return xs) <|> (eof >> return [])
446+ else return xs)
447+ <|> (do notOpenBraces
268− setState (ist { brace_stack = bs })
450+ put (ist { brace_stack = bs })
452+-- | Parses a terminator
453+terminator :: IdrisParser ()
270−pTerminator = do lchar ';'; popIndent
454+terminator = do lchar ';'; popIndent
271− <|> do c <- indent; l <- lastIndent
455+ <|> do c <- indent; l <- lastIndent
274− else fail "Not a terminator"
456+ if c <= l then popIndent else fail "not a terminator"
275− <|> do i <- getInput
457+ <|> do isParen <- lookAheadMatches (oneOf ")}")
276− if "}" `isPrefixOf` i || ")" `isPrefixOf` i
277− then popIndent
458+ if isParen then popIndent else fail "not a termiantor"
278− else fail "Not a terminator"
279− <|> lookAhead eof
459+ <|> lookAhead eof
281−pBarTerminator
461+-- | Parses and keeps a terminator
282− = do lchar '|'; return ()
462+keepTerminator :: IdrisParser ()
283− <|> do c <- indent; l <- lastIndent
284− unless (c <= l) $ fail "Not a terminator"
288− = do lchar ';'; return ()
463+keepTerminator = do lchar ';'; return ()
289− <|> do c <- indent; l <- lastIndent
464+ <|> do c <- indent; l <- lastIndent
290− unless (c <= l) $ fail "Not a terminator"
465+ unless (c <= l) $ fail "not a terminator"
291− <|> do i <- getInput
466+ <|> do isParen <- lookAheadMatches (oneOf ")}|")
293− unless (h `elem` ["}", ")", "|"]) $ fail "Not a terminator"
467+ unless isParen $ fail "not a terminator"
294− <|> lookAhead eof
468+ <|> lookAhead eof
470+-- | Checks if application expression does not end
471+notEndApp :: IdrisParser ()
296notEndApp = do c <- indent; l <- lastIndent
472notEndApp = do c <- indent; l <- lastIndent
298− when (c <= l) $ fail "Terminator"
473+ when (c <= l) (fail "terminator")
475+-- | Checks that it is not end of block
476+notEndBlock :: IdrisParser ()
300−notEndBlock = do ist <- getState
477+notEndBlock = do ist <- get
301 case brace_stack ist of
478 case brace_stack ist of
302− Just lvl : xs -> do i <- indent
479+ Just lvl : xs -> do i <- indent
303− inp <- getInput
480+ isParen <- lookAheadMatches (char ')')
304− when (i < lvl || ")" `isPrefixOf` inp) $ fail "End of block"
481+ when (i < lvl || isParen) (fail "end of block")
305− _ -> return ()
482+ _ -> return ()
307−-- | Use Parsec's internal state to construct a source code position
484+notOpenBraces :: IdrisParser ()
308−pfc :: IParser FC
485+notOpenBraces = do ist <- get
309−pfc = do s <- getPosition
486+ when (hasNothing $ brace_stack ist) $ fail "end of input"
310− let (dir, file) = splitFileName (sourceName s)
487+ where hasNothing :: [Maybe a] -> Bool
311− let f = if dir == addTrailingPathSeparator "." then file else sourceName s
488+ hasNothing = any isNothing
312− return $ FC f (sourceLine s)
489+
313−
490+{- * Main grammar -}
314−pImport :: IParser String
491+
492+{- | Parses module definition
493+ ModuleHeader ::= 'module' Identifier_t ';'?;
495+moduleHeader :: IdrisParser [String]
496+moduleHeader = try (do reserved "module"
498+ option ';' (lchar ';')
499+ return (moduleName i))
501+ where moduleName x = case span (/='.') x of
503+ (x, '.':y) -> x : moduleName y
505+{- | Parses an import statement
506+ Import ::= 'import' Identifier_t ';'?;
508+import_ :: IdrisParser String
315−pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')
509+import_ = do reserved "import"
511+ option ';' (lchar ';')
316− return (toPath f)
512+ return (toPath id)
513+ <?> "import statement"
317− where toPath n = foldl1' (</>) $ splitOn "." n
514+ where toPath f = foldl1' (</>) (Spl.splitOn "." f)
319−-- | A program is a list of declarations, possibly with associated
516+{- | Parses program source
320−-- documentation strings.
517+ Prog ::= Decl* EOF;
321−parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos ->
518+ -}
322− Idris [PDecl]
519+prog :: SyntaxInfo -> IdrisParser [PDecl]
323−parseProg syn fname input pos
325− case runParser (do setPosition pos
326− whiteSpace
520+prog syn = do whiteSpace
327− ps <- many (pDecl syn)
521+ decls <- many (decl syn)
329− i' <- getState
524+ let c = (concat decls)
330− return (concat ps, i')) i fname input of
525+ return c
331− Left err -> do iputStrLn (show err)
526+
332− let errl = sourceLine (errorPos err)
527+{- | Parses a top-level declaration
333− i <- getIState
528+Decl ::=
334− putIState (i { errLine = Just errl })
529+ Decl'
335− return []
530+ | Using
336− Right (x, i) -> do putIState i
531+ | Params
337− return (collect x)
532+ | Mutual
339−-- | Collect 'PClauses' with the same function name
534+ | Class
340−collect :: [PDecl] -> [PDecl]
535+ | Instance
341−collect (c@(PClauses _ o _ _) : ds)
536+ | DSL
342− = clauses (cname c) [] (c : ds)
537+ | Directive
343− where clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)
538+ | Provider
344− | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds
539+ | Transform
345− clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds)
540+ | Import!
346− | n == n' = clauses j (PWith fc' n' l ws r (collect w) : acc) ds
541+ ;
347− clauses (Just n) acc xs = PClauses (getfc c) o n (reverse acc) : collect xs
542+-}
348− clauses Nothing acc (x:xs) = collect xs
349− clauses Nothing acc [] = []
351− cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n
352− cname (PClauses fc _ _ [PWith _ n _ _ _ _]) = Just n
353− cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing
354− cname (PClauses fc _ _ [PWithR _ _ _ _]) = Nothing
355− getfc (PClauses fc _ _ _) = fc
357−collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
358−collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds
359−collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds
360−collect (PClass doc f s cs n ps ds : ds')
361− = PClass doc f s cs n ps (collect ds) : collect ds'
362−collect (PInstance f s cs n ps t en ds : ds')
363− = PInstance f s cs n ps t en (collect ds) : collect ds'
364−collect (d : ds) = d : collect ds
367−pFullExpr :: SyntaxInfo -> IParser PTerm
369− = do x <- pExpr syn; eof;
371− return $ desugar syn i x
373−-- | Parse a top-level declaration
374−pDecl :: SyntaxInfo -> IParser [PDecl]
543+decl :: SyntaxInfo -> IdrisParser [PDecl]
375−pDecl syn = do notEndBlock
544+decl syn = do notEndBlock
376− pDeclBody where
545+ declBody
377− pDeclBody
546+ where declBody :: IdrisParser [PDecl]
378− = do d <- pDecl' syn
547+ declBody = declBody'
379− i <- getState
548+ <|> using_ syn
380− let d' = fmap (desugar syn i) d
549+ <|> params syn
381− return [d']
550+ <|> mutual syn
382− <|> pUsing syn
551+ <|> namespace syn
383− <|> pParams syn
552+ <|> class_ syn
384− <|> pMutual syn
553+ <|> instance_ syn
388− <|> do d <- pDSL syn; return [d]
554+ <|> do d <- dsl syn; return [d]
389− <|> pDirective syn
555+ <|> directive syn
390− <|> try (pProvider syn)
556+ <|> try(provider syn)
391− <|> pTransform syn
557+ <|> transform syn
392− <|> try (do reserved "import"; fp <- identifier
393− fail "imports must be at the top of file")
558+ <|> try(do import_; fail "imports must be at top of file")
394−
559+ <?> "declaration"
395−pFunDecl :: SyntaxInfo -> IParser [PDecl]
560+ declBody' :: IdrisParser [PDecl]
396−pFunDecl syn
561+ declBody' = do d <- decl' syn
397− = try (do notEndBlock
562+ i <- get
400− let d' = fmap (desugar syn i) d
563+ let d' = fmap (desugar syn i) d
401− return [d'])
564+ return [d']
403−--------- Top Level Declarations ---------
566+{- | Parses a top-level declaration with possible syntax sugar
405−pDecl' :: SyntaxInfo -> IParser PDecl
575+decl' :: SyntaxInfo -> IdrisParser PDecl
406−pDecl' syn
576+decl' syn = try fixity
408− <|> try (pFunDecl' syn)
577+ <|> try (fnDecl' syn)
409− <|> try (pData syn)
578+ <|> try (data_ syn)
410− <|> try (pRecord syn)
579+ <|> try (record syn)
411− <|> try (pSyntaxDecl syn)
580+ <|> try (syntaxDecl syn)
412−
581+ <?> "declaration"
583+{- | Parses a syntax extension declaration (and adds the rule to parser state)
584+ SyntaxDecl ::= SyntaxRule;
413−pSyntaxDecl :: SyntaxInfo -> IParser PDecl
586+syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
414−pSyntaxDecl syn
587+syntaxDecl syn = do s <- syntaxRule syn
415− = do s <- pSyntaxRule syn
588+ i <- get
417− let rs = syntax_rules i
589+ let rs = syntax_rules i
418− let ns = syntax_keywords i
590+ let ns = syntax_keywords i
419− let ibc = ibc_write i
591+ let ibc = ibc_write i
420− let ks = map show (names s)
592+ let ks = map show (names s)
421− setState (i { syntax_rules = s : rs,
593+ put (i { syntax_rules = s : rs,
422− syntax_keywords = ks ++ ns,
594+ syntax_keywords = ks ++ ns,
423− ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc
595+ ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc })
426− return (PSyntax fc s)
597+ return (PSyntax fc s)
428− names (Rule syms _ _) = mapMaybe ename syms
598+ where names (Rule syms _ _) = mapMaybe ename syms
429− ename (Keyword n) = Just n
599+ ename (Keyword n) = Just n
430− ename _ = Nothing
600+ ename _ = Nothing
602+{- | Parses a syntax extension declaration
603+SyntaxRuleOpts ::= 'term' | 'pattern';
606+ SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
608+SyntaxSym ::= '[' Name_t ']'
432−pSyntaxRule :: SyntaxInfo -> IParser Syntax
614+syntaxRule :: SyntaxInfo -> IdrisParser Syntax
433−pSyntaxRule syn
615+syntaxRule syn
434 = do pushIndent
616 = do pushIndent
435 sty <- option AnySyntax (do reserved "term"; return TermSyntax
617 sty <- option AnySyntax (do reserved "term"; return TermSyntax
436 <|> do reserved "pattern"; return PatternSyntax)
618 <|> do reserved "pattern"; return PatternSyntax)
437 reserved "syntax"
619 reserved "syntax"
438− syms <- many1 pSynSym
620+ syms <- some syntaxSym
439− when (all expr syms) $ fail "No keywords in syntax rule"
621+ when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
440− let ns = mapMaybe name syms
622+ let ns = mapMaybe getName syms
441− when (length ns /= length (nub ns))
623+ when (length ns /= length (nub ns))
442− $ fail "Repeated variable in syntax rule"
624+ $ unexpected "repeated variable in syntax rule"
443 lchar '='
625 lchar '='
444− tm <- pTExpr (impOK syn)
626+ tm <- typeExpr (allowImp syn)
445− pTerminator
627+ terminator
446 return (Rule (mkSimple syms) tm sty)
628 return (Rule (mkSimple syms) tm sty)
448− expr (Expr _) = True
630+ isExpr (Expr _) = True
449− expr _ = False
631+ isExpr _ = False
450− name (Expr n) = Just n
632+ getName (Expr n) = Just n
451− name _ = Nothing
633+ getName _ = Nothing
453 -- Can't parse two full expressions (i.e. expressions with application) in a row
634 -- Can't parse two full expressions (i.e. expressions with application) in a row
454 -- so change them both to a simple expression
635 -- so change them both to a simple expression
456 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
636 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
457 mkSimple xs = mkSimple' xs
637 mkSimple xs = mkSimple' xs
@@ -461,115 +641,247 @@ pSyntaxRule syn
461 mkSimple' (e : es) = e : mkSimple' es
641 mkSimple' (e : es) = e : mkSimple' es
462 mkSimple' [] = []
642 mkSimple' [] = []
464−pSynSym :: IParser SSymbol
644+
645+{- | Parses a syntax symbol (either binding variable, keyword or expression)
646+SyntaxSym ::= '[' Name_t ']'
652+syntaxSym :: IdrisParser SSymbol
465−pSynSym = try (do lchar '['; n <- pName; lchar ']'
653+syntaxSym = try (do lchar '['; n <- name; lchar ']'
466− return (Expr n))
654+ return (Expr n))
467− <|> try (do lchar '{'; n <- pName; lchar '}'
655+ <|> try (do lchar '{'; n <- name; lchar '}'
468− return (Binding n))
656+ return (Binding n))
469− <|> do n <- iName []
657+ <|> do n <- iName []
470− return (Keyword n)
658+ return (Keyword n)
471− <|> do sym <- strlit
659+ <|> do sym <- stringLiteral
472− return (Symbol sym)
660+ return (Symbol sym)
473−
661+ <?> "syntax symbol"
663+{- | Parses a function declaration with possible syntax sugar
664+ FunDecl ::= FunDecl';
474−pFunDecl' :: SyntaxInfo -> IParser PDecl
666+fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
668+ = try (do notEndBlock
671+ let d' = fmap (desugar syn i) d
673+ <?> "function declaration"
675+{- Parses a function declaration
677+ DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
683+fnDecl' :: SyntaxInfo -> IdrisParser PDecl
475−pFunDecl' syn = try (do doc <- option "" (pDocComment '|')
684+fnDecl' syn = try (do doc <- option "" (docComment '|')
476− pushIndent
685+ pushIndent
477− ist <- getState
686+ ist <- get
478− let initOpts = if default_total ist
687+ let initOpts = if default_total ist
479− then [TotalFn]
688+ then [TotalFn]
481− opts <- pFnOpts initOpts
690+ opts <- fnOpts initOpts
482− acc <- pAccessibility
691+ acc <- optional accessibility
483− opts' <- pFnOpts opts
692+ opts' <- fnOpts opts
484− n_in <- pfName
693+ n_in <- fnName
485− let n = expandNS syn n_in
694+ let n = expandNS syn n_in
486− fc <- pfc
695+ fc <- getFC
487− ty <- pTSig (impOK syn)
696+ ty <- typeSig (allowImp syn)
488− pTerminator
697+ terminator
489−-- ty' <- implicit syn n ty
698+ addAcc n acc
490− addAcc n acc
699+ return (PTy doc syn fc opts' n ty))
491− return (PTy doc syn fc opts' n ty))
700+ <|> try (postulate syn)
492− <|> try (pPostulate syn)
701+ <|> try (pattern syn)
493− <|> try (pPattern syn)
702+ <|> try (caf syn)
494− <|> try (pCAF syn)
703+ <?> "function declaration"
706+{- Parses function options given initial options
710+ | '%' 'assert_total'
712+ | '%' 'specialise' '[' NameTimesList? ']'
715+NameTimes ::= FnName Natural?;
719+ | NameTimes ',' NameTimesList
723+-- FIXME: Check compatability for function options (i.e. partal/total)
724+fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
726+ = do reserved "total"; fnOpts (TotalFn : opts)
727+ <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
728+ <|> try (do lchar '%'; reserved "export"; c <- stringLiteral;
729+ fnOpts (CExport c : opts))
730+ <|> try (do lchar '%'; reserved "assert_total";
731+ fnOpts (AssertTotal : opts))
732+ <|> try (do lchar '%'; reserved "reflection";
733+ fnOpts (Reflection : opts))
734+ <|> do lchar '%'; reserved "specialise";
735+ lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
736+ fnOpts (Specialise ns : opts)
737+ <|> do reserved "implicit"; fnOpts (Implicit : opts)
739+ <?> "function modifier"
740+ where nameTimes :: IdrisParser (Name, Maybe Int)
741+ nameTimes = do n <- fnName
742+ t <- option Nothing (do reds <- natural
743+ return (Just (fromInteger reds)))
746+{- | Parses an operator in function position i.e. enclosed by `()', with an
749+ OperatorFront ::= (Identifier_t '.')? '(' Operator_t ')';
751+operatorFront :: IdrisParser Name
752+operatorFront = maybeWithNS (lchar '(' *> operator <* lchar ')') False []
754+{- | Parses a function (either normal name or operator)
755+ FnName ::= Name | OperatorFront;
757+fnName :: IdrisParser Name
758+fnName = try operatorFront <|> name <?> "function name"
760+{- | Parses an accessibilty modifier (e.g. public, private) -}
761+accessibility :: IdrisParser Accessibility
762+accessibility = do reserved "public"; return Public
763+ <|> do reserved "abstract"; return Frozen
764+ <|> do reserved "private"; return Hidden
765+ <?> "accessibility modifier"
769+{- | Parses a postulate
772+ DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
496−pPostulate :: SyntaxInfo -> IParser PDecl
775+postulate :: SyntaxInfo -> IdrisParser PDecl
497−pPostulate syn = do doc <- option "" (pDocComment '|')
776+postulate syn = do doc <- option "" (docComment '|')
498− pushIndent
777+ pushIndent
499− reserved "postulate"
778+ reserved "postulate"
500− ist <- getState
779+ ist <- get
501− let initOpts = if default_total ist
780+ let initOpts = if default_total ist
502− then [TotalFn]
781+ then [TotalFn]
504− opts <- pFnOpts initOpts
783+ opts <- fnOpts initOpts
505− acc <- pAccessibility
784+ acc <- optional accessibility
506− opts' <- pFnOpts opts
785+ opts' <- fnOpts opts
507− n_in <- pfName
786+ n_in <- fnName
508− let n = expandNS syn n_in
787+ let n = expandNS syn n_in
509− ty <- pTSig (impOK syn)
788+ ty <- typeSig (allowImp syn)
510− fc <- pfc
789+ fc <- getFC
511− pTerminator
790+ terminator
512− addAcc n acc
791+ addAcc n acc
513− return (PPostulate doc syn fc opts' n ty)
792+ return (PPostulate doc syn fc opts' n ty)
795+{- | Parses a using declaration
798+ 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
516−pUsing :: SyntaxInfo -> IParser [PDecl]
801+using_ :: SyntaxInfo -> IdrisParser [PDecl]
517−pUsing syn =
802+using_ syn =
518 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
803 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
519 openBlock
804 openBlock
520 let uvars = using syn
805 let uvars = using syn
521− ds <- many1 (pDecl (syn { using = uvars ++ ns }))
806+ ds <- many (decl (syn { using = uvars ++ ns }))
522 closeBlock
807 closeBlock
523 return (concat ds)
808 return (concat ds)
809+ <?> "using declaration"
811+{- | Parses a parameters declaration
814+ 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
525−pParams :: SyntaxInfo -> IParser [PDecl]
817+params :: SyntaxInfo -> IdrisParser [PDecl]
526−pParams syn =
818+params syn =
527− do reserved "parameters"; lchar '('; ns <- tyDeclList syn; lchar ')'
819+ do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
528− openBlock
820+ openBlock
529 let pvars = syn_params syn
821 let pvars = syn_params syn
530− ds <- many1 (pDecl syn { syn_params = pvars ++ ns })
822+ ds <- many (decl syn { syn_params = pvars ++ ns })
531− closeBlock
823+ closeBlock
532− fc <- pfc
824+ fc <- getFC
533 return [PParams fc ns (concat ds)]
825 return [PParams fc ns (concat ds)]
826+ <?> "parameters declaration"
828+{- | Parses a mutual declaration (for mutually recursive functions)
831+ 'mutual' OpenBlock Decl* CloseBlock
535−pMutual :: SyntaxInfo -> IParser [PDecl]
834+mutual :: SyntaxInfo -> IdrisParser [PDecl]
536−pMutual syn =
835+mutual syn =
537 do reserved "mutual"
836 do reserved "mutual"
538− openBlock
837+ openBlock
539 let pvars = syn_params syn
838 let pvars = syn_params syn
540− ds <- many1 (pDecl syn)
839+ ds <- many (decl syn)
541− closeBlock
840+ closeBlock
542− fc <- pfc
841+ fc <- getFC
543 return [PMutual fc (concat ds)]
842 return [PMutual fc (concat ds)]
845+{- | Parses a namespace declaration
848+ 'namespace' identifier OpenBlock Decl+ CloseBlock
545−pNamespace :: SyntaxInfo -> IParser [PDecl]
851+namespace :: SyntaxInfo -> IdrisParser [PDecl]
546−pNamespace syn =
852+namespace syn =
547 do reserved "namespace"; n <- identifier;
853 do reserved "namespace"; n <- identifier;
548− openBlock
854+ openBlock
549− ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
855+ ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
550 closeBlock
856 closeBlock
551− return [PNamespace n (concat ds)]
857+ return [PNamespace n (concat ds)]
552−
858+ <?> "namespace declaration"
860+{- | Parses a fixity declaration
553−--------- Fixity ---------
862+Fixity ::=
554−
863+ FixityType Natural_t OperatorList Terminator
555−pFixity :: IParser PDecl
864+ ;
866+fixity :: IdrisParser PDecl
556−pFixity = do pushIndent
867+fixity = do pushIndent
557− f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
868+ f <- fixityType; i <- natural; ops <- sepBy1 operator (lchar ',')
558− pTerminator
869+ terminator
559− let prec = fromInteger i
870+ let prec = fromInteger i
560− istate <- getState
871+ istate <- get
561− let infixes = idris_infixes istate
872+ let infixes = idris_infixes istate
562− let fs = map (Fix (f prec)) ops
873+ let fs = map (Fix (f prec)) ops
563− let redecls = map (alreadyDeclared infixes) fs
874+ let redecls = map (alreadyDeclared infixes) fs
564− let ill = filter (not . checkValidity) redecls
875+ let ill = filter (not . checkValidity) redecls
565− if null ill
876+ if null ill
566− then do setState (istate { idris_infixes = nub $ sort (fs ++ infixes)
877+ then do put (istate { idris_infixes = nub $ sort (fs ++ infixes)
567− , ibc_write = map IBCFix fs ++ ibc_write istate
878+ , ibc_write = map IBCFix fs ++ ibc_write istate
569− fc <- pfc
880+ fc <- getFC
570− return (PFix fc (f prec) ops)
881+ return (PFix fc (f prec) ops)
571− else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
882+ else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
572 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
883 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
884+ <?> "fixity declaration"
573 where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
885 where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
574 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
886 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
@@ -579,287 +891,366 @@ pFixity = do pushIndent
579 extractName :: FixDecl -> String
891 extractName :: FixDecl -> String
580 extractName (Fix _ n) = n
892 extractName (Fix _ n) = n
582−fixity :: IParser (Int -> Fixity)
894+{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)
902+fixityType :: IdrisParser (Int -> Fixity)
583−fixity = try (do reserved "infixl"; return Infixl)
903+fixityType = try (do reserved "infixl"; return Infixl)
584− <|> try (do reserved "infixr"; return Infixr)
904+ <|> try (do reserved "infixr"; return Infixr)
585− <|> try (do reserved "infix"; return InfixN)
905+ <|> try (do reserved "infix"; return InfixN)
586− <|> try (do reserved "prefix"; return PrefixN)
906+ <|> try (do reserved "prefix"; return PrefixN)
587−
907+ <?> "fixity type"
588−--------- Type classes ---------
908+
589−
909+{- |Parses a methods block (for type classes and instances)
910+ MethodsBlock ::= 'where' OpenBlock FnDecl* CloseBlock
590−pClass :: SyntaxInfo -> IParser [PDecl]
912+methodsBlock :: SyntaxInfo -> IdrisParser [PDecl]
913+methodsBlock syn = do reserved "where"
915+ ds <- many (fnDecl syn)
920+{- |Parses a type class declaration
924+ | '(' Name ':' Expr ')'
928+ DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* MethodsBlock?
931+class_ :: SyntaxInfo -> IdrisParser [PDecl]
591−pClass syn = do doc <- option "" (pDocComment '|')
932+class_ syn = do doc <- option "" (docComment '|')
592− acc <- pAccessibility
933+ acc <- optional accessibility
593− reserved "class"; fc <- pfc; cons <- pConstList syn; n_in <- pName
934+ reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- name
594 let n = expandNS syn n_in
935 let n = expandNS syn n_in
595 cs <- many carg
936 cs <- many carg
596− reserved "where"; openBlock
937+ ds <- option [] (methodsBlock syn)
597− ds <- many $ pFunDecl syn
599− let allDs = concat ds
600− accData acc n (concatMap declared allDs)
938+ accData acc n (concatMap declared ds)
601− return [PClass doc syn fc cons n cs allDs]
939+ return [PClass doc syn fc cons n cs ds]
940+ <?> "type-class declaration"
942+ carg :: IdrisParser (Name, PTerm)
603− carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'
943+ carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
604 return (i, ty)
944 return (i, ty)
605− <|> do i <- pName;
945+ <|> do i <- name;
606 return (i, PType)
946 return (i, PType)
608−pInstance :: SyntaxInfo -> IParser [PDecl]
948+{- |Parses a type class instance declaration
609−pInstance syn = do reserved "instance"; fc <- pfc
610− en <- option Nothing
611− (do lchar '['; n_in <- pfName; lchar ']'
612− let n = expandNS syn n_in
614− cs <- pConstList syn
616− args <- many (pSimpleExpr syn)
617− let sc = PApp fc (PRef fc cn) (map pexp args)
618− let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
619− reserved "where"; openBlock
620− ds <- many $ pFunDecl syn
622− return [PInstance syn fc cs cn args t en (concat ds)]
624−--------- Expressions ---------
626−pExpr syn = do i <- getState
627− buildExpressionParser (table (idris_infixes i)) (pExpr' syn)
629−pExpr' :: SyntaxInfo -> IParser PTerm
631− = try (pExtExpr syn)
634−pExtExpr :: SyntaxInfo -> IParser PTerm
950+ Instance ::=
635−pExtExpr syn = do i <- getState
951+ 'instance' InstanceName? ConstraintList? Name SimpleExpr* MethodsBlock?
636− pExtensions syn (syntax_rules i)
952+ ;
638−pSimpleExtExpr :: SyntaxInfo -> IParser PTerm
954+ InstanceName ::= '[' Name ']';
639−pSimpleExtExpr syn = do i <- getState
955+-}
956+instance_ :: SyntaxInfo -> IdrisParser [PDecl]
957+instance_ syn = do reserved "instance"; fc <- getFC
958+ en <- optional instanceName
959+ cs <- constraintList syn
961+ args <- many (simpleExpr syn)
962+ let sc = PApp fc (PRef fc cn) (map pexp args)
963+ let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
964+ ds <- option [] (methodsBlock syn)
965+ return [PInstance syn fc cs cn args t en ds]
966+ <?> "instance declaratioN"
967+ where instanceName :: IdrisParser Name
968+ instanceName = do lchar '['; n_in <- fnName; lchar ']'
969+ let n = expandNS syn n_in
974+{- | Parses an expression as a whole
975+ FullExpr ::= Expr EOF_t;
977+fullExpr :: SyntaxInfo -> IdrisParser PTerm
978+fullExpr syn = do x <- expr syn
981+ return $ desugar syn i x
984+{- |Parses an expression
987+expr :: SyntaxInfo -> IdrisParser PTerm
988+expr syn = do i <- get
989+ buildExpressionParser (table (idris_infixes i)) (expr' syn)
991+{- | Parses either an internally defined expression or
994+Expr' ::= "External (User-defined) Syntax"
998+expr' :: SyntaxInfo -> IdrisParser PTerm
999+expr' syn = try (externalExpr syn)
1000+ <|> internalExpr syn
1003+{- | Parses a user-defined expression -}
1004+externalExpr :: SyntaxInfo -> IdrisParser PTerm
1005+externalExpr syn = do i <- get
1006+ extensions syn (syntax_rules i)
1007+ <?> "user-defined expression"
1009+{- | Parses a simple user-defined expression -}
1010+simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm
1011+simpleExternalExpr syn = do i <- get
640− pExtensions syn (filter simple (syntax_rules i))
1012+ extensions syn (filter isSimple (syntax_rules i))
642− simple (Rule (Expr x:xs) _ _) = False
1014+ isSimple (Rule (Expr x:xs) _ _) = False
643− simple (Rule (SimpleExpr x:xs) _ _) = False
1015+ isSimple (Rule (SimpleExpr x:xs) _ _) = False
644− simple (Rule [Keyword _] _ _) = True
1016+ isSimple (Rule [Keyword _] _ _) = True
645− simple (Rule [Symbol _] _ _) = True
1017+ isSimple (Rule [Symbol _] _ _) = True
646− simple (Rule (_:xs) _ _) = case last xs of
1018+ isSimple (Rule (_:xs) _ _) = case last xs of
647 Keyword _ -> True
1019 Keyword _ -> True
648 Symbol _ -> True
1020 Symbol _ -> True
649 _ -> False
1021 _ -> False
650− simple _ = False
1022+ isSimple _ = False
652−pNoExtExpr syn =
1024+{- | Tries to parse a user-defined expression given a list of syntactic extensions -}
654− <|> try (pMatchApp syn)
655− <|> try (pUnifyLog syn)
657− <|> try (pSimpleExpr syn)
661− <|> pRewriteTerm syn
665−pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
1025+extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm
666−pExtensions syn rules = choice (map (try . pExt syn) (filter valid rules))
1026+extensions syn rules = choice (map (try . extension syn) (filter isValid rules))
1027+ <?> "user-defined expression"
1029+ isValid :: Syntax -> Bool
668− valid (Rule _ _ AnySyntax) = True
1030+ isValid (Rule _ _ AnySyntax) = True
669− valid (Rule _ _ PatternSyntax) = inPattern syn
1031+ isValid (Rule _ _ PatternSyntax) = inPattern syn
670− valid (Rule _ _ TermSyntax) = not (inPattern syn)
1032+ isValid (Rule _ _ TermSyntax) = not (inPattern syn)
673data SynMatch = SynTm PTerm | SynBind Name
1035data SynMatch = SynTm PTerm | SynBind Name
1037+{- | Tries to parse an expression given a user-defined rule -}
675−pExt :: SyntaxInfo -> Syntax -> IParser PTerm
1038+extension :: SyntaxInfo -> Syntax -> IdrisParser PTerm
676−pExt syn (Rule ssym ptm _)
1039+extension syn (Rule ssym ptm _)
677− = do smap <- mapM pSymbol ssym
1040+ = do smap <- mapM extensionSymbol ssym
678 let ns = mapMaybe id smap
1041 let ns = mapMaybe id smap
679 return (update ns ptm) -- updated with smap
1042 return (update ns ptm) -- updated with smap
1044+ extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
681− pSymbol (Keyword n) = do reserved (show n); return Nothing
1045+ extensionSymbol (Keyword n) = do reserved (show n); return Nothing
682− pSymbol (Expr n) = do tm <- pExpr syn
1046+ extensionSymbol (Expr n) = do tm <- expr syn
683− return $ Just (n, SynTm tm)
1047+ return $ Just (n, SynTm tm)
684− pSymbol (SimpleExpr n) = do tm <- pSimpleExpr syn
1048+ extensionSymbol (SimpleExpr n) = do tm <- simpleExpr syn
685− return $ Just (n, SynTm tm)
1049+ return $ Just (n, SynTm tm)
686− pSymbol (Binding n) = do b <- pName
1050+ extensionSymbol (Binding n) = do b <- name
687− return $ Just (n, SynBind b)
1051+ return $ Just (n, SynBind b)
688− pSymbol (Symbol s) = do symbol s
1052+ extensionSymbol (Symbol s) = do symbol s
689− return Nothing
1053+ return Nothing
1054+ dropn :: Name -> [(Name, a)] -> [(Name, a)]
690 dropn n [] = []
1055 dropn n [] = []
691 dropn n ((x,t) : xs) | n == x = xs
1056 dropn n ((x,t) : xs) | n == x = xs
692 | otherwise = (x,t):dropn n xs
1057 | otherwise = (x,t):dropn n xs
1059+ updateB :: [(Name, SynMatch)] -> Name -> Name
694 updateB ns n = case lookup n ns of
1060 updateB ns n = case lookup n ns of
695 Just (SynBind t) -> t
1061 Just (SynBind t) -> t
1064+ update :: [(Name, SynMatch)] -> PTerm -> PTerm
698 update ns (PRef fc n) = case lookup n ns of
1065 update ns (PRef fc n) = case lookup n ns of
699 Just (SynTm t) -> t
1066 Just (SynTm t) -> t
700 _ -> PRef fc n
1067 _ -> PRef fc n
701 update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)
1068 update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)
702− update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc)
1069+ update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc)
703 update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)
1070 update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)
704 (update (dropn n ns) sc)
1071 (update (dropn n ns) sc)
705 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
1072 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
706− update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)
1073+ update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)
707 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)
1074 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)
708 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)
1075 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)
709 update ns (PAlternative a as) = PAlternative a (map (update ns) as)
1076 update ns (PAlternative a as) = PAlternative a (map (update ns) as)
710 update ns (PHidden t) = PHidden (update ns t)
1077 update ns (PHidden t) = PHidden (update ns t)
711 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
1078 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
1079+ where upd :: [(Name, SynMatch)] -> [PDo] -> [PDo]
712− where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
1080+ upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
713 upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds
1081 upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds
714− upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)
1082+ upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)
715 : upd (dropn n ns) ds
1083 : upd (dropn n ns) ds
716− upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t)
1084+ upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t)
717 : upd ns ds
1085 : upd ns ds
718− upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)
1086+ upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)
719 : upd ns ds
1087 : upd ns ds
720 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
1088 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
721 update ns t = t
1089 update ns t = t
723−pName = do i <- getState
1091+{- |Parses a (normal) built-in expression
724− iName (syntax_keywords i)
1092+
725− <|> do reserved "instance"
1093+InternalExpr ::=
726− i <- getState
1094+ App
727− UN n <- iName (syntax_keywords i)
1095+ | MatchApp
728− return (UN ('@':n))
1096+ | UnifyLog
730−-- | Parser for an operator in function position, i.e. enclosed by `()', with an
1098+ | SimpleExpr
731−-- optional namespace.
1099+ | Lambda
732−pOpFront = maybeWithNS pOpFrontNoNS False []
1100+ | QuoteGoal
733− where pOpFrontNoNS = do lchar '('; o <- operator; lchar ')'; return o
1101+ | Let
735−pfName = try pOpFront
1103+ | Pi
736− <|> pName
1104+ | DoBlock
738−pTotality :: IParser Bool
1106+-}
739−pTotality
1107+internalExpr :: SyntaxInfo -> IdrisParser PTerm
740− = do reserved "total"; return True
1108+internalExpr syn =
741− <|> do reserved "partial"; return False
1109+ try (app syn)
742−
1110+ <|> try (matchApp syn)
743−pAccessibility' :: IParser Accessibility
1111+ <|> try (unifyLog syn)
744−pAccessibility'
1112+ <|> recordType syn
745− = do reserved "public"; return Public
1113+ <|> try (simpleExpr syn)
746− <|> do reserved "abstract"; return Frozen
1114+ <|> lambda syn
747− <|> do reserved "private"; return Hidden
1115+ <|> quoteGoal syn
749−pAccessibility :: IParser (Maybe Accessibility)
1117+ <|> rewriteTerm syn
750−pAccessibility
1118+ <|> pi syn
751− = do acc <- pAccessibility'; return (Just acc)
1119+ <|> doBlock syn
1122+{- | Parses a case expression
1124+ 'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;
1126+caseExpr :: SyntaxInfo -> IdrisParser PTerm
1127+caseExpr syn = do reserved "case"; fc <- getFC
1128+ scr <- expr syn; reserved "of";
1129+ opts <- indentedBlock1 (caseOption syn)
1130+ return (PCase fc scr opts)
1131+ <?> "case expression"
1133+{- | Parses a case in a case expression
1135+ Expr '=>' Expr Terminator
1138+caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
1139+caseOption syn = do lhs <- expr (syn { inPattern = True })
1140+ symbol "=>"; r <- expr syn
752− <|> return Nothing
1141+ return (lhs, r)
753−
1142+ <?> "case option"
754−pFnOpts :: [FnOpt] -> IParser [FnOpt]
1143+
755−pFnOpts opts
1144+{- | Parses a proof block
756− = do reserved "total"; pFnOpts (TotalFn : opts)
1145+ProofExpr ::=
757− <|> do reserved "partial"; pFnOpts (PartialFn : (opts \\ [TotalFn]))
1146+ 'proof' OpenBlock Tactic'* CloseBlock
758− <|> try (do lchar '%'; reserved "export"; c <- strlit;
1147+ ;
759− pFnOpts (CExport c : opts))
1148+-}
760− <|> try (do lchar '%'; reserved "assert_total";
1149+proofExpr :: SyntaxInfo -> IdrisParser PTerm
761− pFnOpts (AssertTotal : opts))
1150+proofExpr syn = do reserved "proof"
762− <|> try (do lchar '%'; reserved "reflection";
1151+ ts <- indentedBlock (tactic syn)
763− pFnOpts (Reflection : opts))
764− <|> do lchar '%'; reserved "specialise";
765− lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
766− pFnOpts (Specialise ns : opts)
767− <|> do reserved "implicit"; pFnOpts (Implicit : opts)
769− where nameTimes = do n <- pfName
770− t <- option Nothing (do reds <- natural
771− return (Just (fromInteger reds)))
772− return (n, t)
1152+ return $ PProof ts
773−
1153+ <?> "proof block"
774−addAcc :: Name -> Maybe Accessibility -> IParser ()
1154+
775−addAcc n a = do i <- getState
1155+{- | Parses a tactics block
776− setState (i { hide_list = (n, a) : hide_list i })
1156+TacticsExpr :=
777−
1157+ 'tactics' OpenBlock Tactic'* CloseBlock
778−pCaseExpr syn = do
1158+;
779− reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
1159+-}
780− openBlock
1160+tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
782− opts <- many1 (do notEndBlock
785− return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
788− return (PCase fc scr opts)
791− reserved "proof"; lchar '{'
792− ts <- endBy (pTactic syn) (lchar ';')
796−pTacticsExpr syn = do
797− reserved "tactics"; lchar '{'
1161+tacticsExpr syn = do reserved "tactics"
798− ts <- endBy (pTactic syn) (lchar ';')
1162+ ts <- indentedBlock (tactic syn)
800− return (PTactics ts)
1163+ return $ PTactics ts
801−
1164+ <?> "tactics block"
802−pSimpleExpr syn =
1165+
1166+{- | Parses a simple expresion
1171+ | 'refl' ('{' Expr '}')?
1186+ | {- External (User-defined) Simple Expression -}
1189+simpleExpr :: SyntaxInfo -> IdrisParser PTerm
803− try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t)
1191+ {-try (do symbol "!["; t <- term; lchar ']'; return $ PQuote t)
804− <|> do lchar '?'; x <- pName; return (PMetavar x)
1192+ <|>-} do lchar '?'; x <- name; return (PMetavar x)
805− <|> do lchar '%'; fc <- pfc; reserved "instance"; return (PResolveTC fc)
1193+ <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)
806− <|> do reserved "refl"; fc <- pfc;
1194+ <|> do reserved "refl"; fc <- getFC;
807− tm <- option Placeholder (do lchar '{'; t <- pExpr syn; lchar '}';
1195+ tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';
808 return t)
1196 return t)
809 return (PRefl fc tm)
1197 return (PRefl fc tm)
810−-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)
1198+ <|> proofExpr syn
811− <|> pProofExpr syn
1199+ <|> tacticsExpr syn
812− <|> pTacticsExpr syn
1200+ <|> caseExpr syn
814− <|> try (do x <- pfName
1201+ <|> try (do fc <- getFC
815− fc <- pfc
1202+ x <- fnName
816 return (PRef fc x))
1203 return (PRef fc x))
817− <|> try (pList syn)
1204+ <|> try (listExpr syn)
818− <|> try (pComprehension syn)
1205+ <|> try (comprehension syn)
819− <|> try (pAlt syn)
1206+ <|> try (alt syn)
820− <|> try (pIdiom syn)
1207+ <|> try (idiom syn)
821 <|> try (do lchar '('
1208 <|> try (do lchar '('
822− bracketed (noImp syn))
1209+ bracketed (disallowImp syn))
823− <|> try (do c <- pConstant
1210+ <|> try (do c <- constant
824− fc <- pfc
1211+ fc <- getFC
825 return (modifyConst syn fc (PConstant c)))
1212 return (modifyConst syn fc (PConstant c)))
826 <|> do reserved "Type"; return PType
1213 <|> do reserved "Type"; return PType
827 <|> try (do symbol "()"
1214 <|> try (do symbol "()"
828− fc <- pfc
1215+ fc <- getFC
829 return (PTrue fc))
1216 return (PTrue fc))
830 <|> try (do symbol "_|_"
1217 <|> try (do symbol "_|_"
831− fc <- pfc
1218+ fc <- getFC
832 return (PFalse fc))
1219 return (PFalse fc))
833 <|> do lchar '_'; return Placeholder
1220 <|> do lchar '_'; return Placeholder
834− <|> pSimpleExtExpr syn
1221+ <|> simpleExternalExpr syn
835−
1222+ <?> "expression"
1225+{- |Parses the rest of an expression in braces
1229+ | Operator Expr ')'
1230+ | Expr Operator ')'
1233+bracketed :: SyntaxInfo -> IdrisParser PTerm
836bracketed syn =
1234bracketed syn =
837− try (pPair syn)
1235+ try (pair syn)
838− <|> try (do e <- pExpr syn; lchar ')'; return e)
1236+ <|> try (do e <- expr syn; lchar ')'; return e)
839−-- <|> try (do reserved "typed"
840−-- e <- pExpr syn; symbol ":"; t <- pExpr syn; lchar ')'
841−-- return (PTyped e t))
842− <|> try (do fc <- pfc; o <- operator; e <- pExpr syn; lchar ')'
1237+ <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
843 return $ PLam (MN 1000 "ARG") Placeholder
1238 return $ PLam (MN 1000 "ARG") Placeholder
844− (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),
1239+ (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),
845 pexp e]))
1240 pexp e]))
846− <|> try (do fc <- pfc; e <- pSimpleExpr syn; o <- operator; lchar ')'
1241+ <|> try (do fc <- getFC; e <- simpleExpr syn; o <- operator; lchar ')'
847 return $ PLam (MN 1000 "ARG") Placeholder
1242 return $ PLam (MN 1000 "ARG") Placeholder
848 (PApp fc (PRef fc (UN o)) [pexp e,
1243 (PApp fc (PRef fc (UN o)) [pexp e,
849 pexp (PRef fc (MN 1000 "ARG"))]))
1244 pexp (PRef fc (MN 1000 "ARG"))]))
850−
1245+ <?> "end of expression in braces"
851−pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
852−pCaseOpt syn = do lhs <- pExpr (syn { inPattern = True })
853− symbol "=>"; rhs <- pExpr syn
856-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
1247-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
857-- big integer, otherwise try fromInteger and the constants as alternatives.
1248-- big integer, otherwise try fromInteger and the constants as alternatives.
858-- a better solution would be to fix fromInteger to work with Integer, as the
1249-- a better solution would be to fix fromInteger to work with Integer, as the
859-- name suggests, rather than Int
1250-- name suggests, rather than Int
860−
1251+{-| Finds optimal type for integer constant -}
861modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
1252modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
862−modifyConst syn fc (PConstant (BI x))
1253+modifyConst syn fc (PConstant (BI x))
863 | not (inPattern syn)
1254 | not (inPattern syn)
864 = PAlternative False
1255 = PAlternative False
865 (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI (fromInteger x)))]
1256 (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI (fromInteger x)))]
@@ -875,351 +1266,626 @@ modifyConst syn fc (PConstant (BI x))
876modifyConst syn fc x = x
1267modifyConst syn fc x = x
878−
1269+{- | Parses a list literal expression e.g. [1,2,3]
1276+ | Expr ',' ExprList
1280+listExpr :: SyntaxInfo -> IdrisParser PTerm
879−pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']'
1281+listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lchar ']'
880− return (mkList fc xs)
1282+ return (mkList fc xs)
1283+ <?> "list expression"
1285+ mkList :: FC -> [PTerm] -> PTerm
882 mkList fc [] = PRef fc (UN "Nil")
1286 mkList fc [] = PRef fc (UN "Nil")
883− mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
1287+ mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
1289+{- | Parses rest of pair expression
1291+ Expr RestTuple? ')'
1293+ | Name ':' Expr '**' 'Expr' ')'
1306+pair :: SyntaxInfo -> IdrisParser PTerm
885−pPair syn = try (do l <- pExpr syn
1307+pair syn = try (do l <- expr syn
886− fc <- pfc
1308+ fc <- getFC
887− rest <- restTuple
1309+ rest <- restTuple
888− case rest of
1310+ case rest of
889− [] -> return l
1311+ [] -> return l
890− [Left r] -> return (PPair fc l r)
1312+ [Left r] -> return (PPair fc l r)
891− [Right r] -> return (PDPair fc l Placeholder r))
1313+ [Right r] -> return (PDPair fc l Placeholder r))
892 <|> try (do x <- ntuple
1314 <|> try (do x <- ntuple
893 lchar ')'
1315 lchar ')'
894− return x)
1316+ return x)
895− <|> do ln <- pName; lchar ':'
1317+ <|> do ln <- name; lchar ':'
896− lty <- pExpr syn
1318+ lty <- expr syn
897 reservedOp "**"
1319 reservedOp "**"
898− fc <- pfc
1320+ fc <- getFC
899− r <- pExpr syn
1321+ r <- expr syn
900 lchar ')'
1322 lchar ')'
901− return (PDPair fc (PRef fc ln) lty r)
1323+ return (PDPair fc (PRef fc ln) lty r)
1324+ <?> "pair expression"
1326+ restTuple :: IdrisParser [Either PTerm PTerm]
903 restTuple = do lchar ')'; return []
1327 restTuple = do lchar ')'; return []
904 <|> do lchar ','
1328 <|> do lchar ','
905− r <- pExpr syn
1329+ r <- expr syn
906 lchar ')'
1330 lchar ')'
907 return [Left r]
1331 return [Left r]
908 <|> do reservedOp "**"
1332 <|> do reservedOp "**"
909− r <- pExpr syn
1333+ r <- expr syn
910 lchar ')'
1334 lchar ')'
911 return [Right r]
1335 return [Right r]
1336+ <?> "end of pair expression"
1337+ ntuple :: IdrisParser PTerm
912− ntuple = try (do l <- pExpr syn; fc <- pfc; lchar ','
1338+ ntuple = try (do l <- expr syn; fc <- getFC; lchar ','
913 rest <- ntuple
1339 rest <- ntuple
914 return (PPair fc l rest))
1340 return (PPair fc l rest))
915− <|> (do l <- pExpr syn; fc <- pfc; lchar ','
1341+ <|> (do l <- expr syn; fc <- getFC; lchar ','
916− r <- pExpr syn
1342+ r <- expr syn
917 return (PPair fc l r))
1343 return (PPair fc l r))
918−
1344+ <?> "tuple expression"
1346+{- | Parses an alternative expression
1347+ Alt ::= '(|' Expr_List '|)';
1351+ | Expr' ',' Expr_List
1354+alt :: SyntaxInfo -> IdrisParser PTerm
919−pAlt syn = do symbol "(|"; alts <- sepBy1 (pExpr' syn) (lchar ','); symbol "|)"
1355+alt syn = do symbol "(|"; alts <- sepBy1 (expr' syn) (lchar ','); symbol "|)"
920− return (PAlternative False alts)
1356+ return (PAlternative False alts)
922−pHSimpleExpr syn
1358+{- | Parses a possibly hidden simple expression
1364+hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm
923− = do lchar '.'
1366+ do lchar '.'
924− e <- pSimpleExpr syn
1367+ e <- simpleExpr syn
925− return $ PHidden e
1368+ return $ PHidden e
926− <|> pSimpleExpr syn
1369+ <|> simpleExpr syn
927−
1370+ <?> "expression"
928−pMatchApp syn = do ty <- pSimpleExpr syn
1371+
1372+{- | Parses a matching application expression
1374+ SimpleExpr '<==' FnName
1377+matchApp :: SyntaxInfo -> IdrisParser PTerm
1378+matchApp syn = do ty <- simpleExpr syn
929− symbol "<=="
1379+ symbol "<=="
930− fc <- pfc
1380+ fc <- getFC
931− f <- pfName
1381+ f <- fnName
932− return (PLet (MN 0 "match")
1382+ return (PLet (MN 0 "match")
934 (PMatchApp fc f)
1384 (PMatchApp fc f)
935 (PRef fc (MN 0 "match")))
1385 (PRef fc (MN 0 "match")))
936−
1386+ <?> "matching application expression"
1388+{- | Parses a unification log expression
1390+ '%' 'unifyLog' SimpleExpr
1393+unifyLog :: SyntaxInfo -> IdrisParser PTerm
937−pUnifyLog syn = do lchar '%'; reserved "unifyLog";
1394+unifyLog syn = do lchar '%'; reserved "unifyLog";
938− tm <- pSimpleExpr syn
1395+ tm <- simpleExpr syn
939− return (PUnifyLog tm)
1396+ return (PUnifyLog tm)
940−
1397+ <?> "unification log expression"
1399+{- | Parses a function application expression
1401+ 'mkForeign' Arg Arg*
1405+app :: SyntaxInfo -> IdrisParser PTerm
941−pApp syn = do f <- reserved "mkForeign"
1406+app syn = do f <- reserved "mkForeign"
942− fc <- pfc
1407+ fc <- getFC
943− fn <- pArg syn
1408+ fn <- arg syn
944− args <- many (do notEndApp; pArg syn)
1409+ args <- many (do notEndApp; arg syn)
945− i <- getState
1410+ i <- get
946− -- mkForeign f args ==>
1411+ -- mkForeign f args ==>
947− -- liftPrimIO (\w => mkForeignPrim f args w)
1412+ -- liftPrimIO (\w => mkForeignPrim f args w)
948− let ap = PApp fc (PRef fc (UN "liftPrimIO"))
1413+ let ap = PApp fc (PRef fc (UN "liftPrimIO"))
949− [pexp (PLam (MN 0 "w")
1414+ [pexp (PLam (MN 0 "w")
950− Placeholder
1415+ Placeholder
951− (PApp fc (PRef fc (UN "mkForeignPrim"))
1416+ (PApp fc (PRef fc (UN "mkForeignPrim"))
952− (fn : args ++
1417+ (fn : args ++
953− [pexp (PRef fc (MN 0 "w"))])))]
1418+ [pexp (PRef fc (MN 0 "w"))])))]
954− return (dslify i ap)
1419+ return (dslify i ap)
956− <|> do f <- pSimpleExpr syn
1421+ <|> do f <- simpleExpr syn
957− fc <- pfc
1422+ fc <- getFC
958− args <- many1 (do notEndApp
1423+ args <- some (do notEndApp; arg syn)
959− pArg syn)
1424+ i <- get
961 return (dslify i $ PApp fc f args)
1425 return (dslify i $ PApp fc f args)
1426+ <?> "function application"
1428+ dslify :: IState -> PTerm -> PTerm
963 dslify i (PApp fc (PRef _ f) [a])
1429 dslify i (PApp fc (PRef _ f) [a])
964 | [d] <- lookupCtxt f (idris_dsls i)
1430 | [d] <- lookupCtxt f (idris_dsls i)
965 = desugar (syn { dsl_info = d }) i (getTm a)
1431 = desugar (syn { dsl_info = d }) i (getTm a)
966 dslify i t = t
1432 dslify i t = t
1434+{- |Parses a function argument
968−pArg :: SyntaxInfo -> IParser PArg
1441+arg :: SyntaxInfo -> IdrisParser PArg
969−pArg syn = try (pImplicitArg syn)
1442+arg syn = try (implicitArg syn)
970− <|> try (pConstraintArg syn)
1443+ <|> try (constraintArg syn)
971− <|> do e <- pSimpleExpr syn
1444+ <|> do e <- simpleExpr syn
972 return (pexp e)
1445 return (pexp e)
973−
1446+ <?> "function argument"
1448+{- |Parses an implicit function argument
1450+ '{' Name ('=' Expr)? '}'
1453+implicitArg :: SyntaxInfo -> IdrisParser PArg
974−pImplicitArg syn = do lchar '{'
1454+implicitArg syn = do lchar '{'
975− n <- pName
1455+ n <- name
976− fc <- pfc
1456+ fc <- getFC
977− v <- option (PRef fc n) (do lchar '='
1457+ v <- option (PRef fc n) (do lchar '='
978− pExpr syn)
1458+ expr syn)
979− lchar '}'
1459+ lchar '}'
980− return (pimp n v)
1460+ return (pimp n v)
981−
1461+ <?> "implicit function argument"
1463+{- |Parses a constraint argument (for selecting a named type class instance)
1468+constraintArg :: SyntaxInfo -> IdrisParser PArg
982−pConstraintArg syn = do symbol "@{"
1469+constraintArg syn = do symbol "@{"
983− e <- pExpr syn
1470+ e <- expr syn
984− symbol "}"
1471+ symbol "}"
985− return (pconst e)
1472+ return (pconst e)
986−
1473+ <?> "constraint argument"
987−pRecordType syn
1474+
1476+{- |Parses a record field setter expression
1478+ 'record' '{' FieldTypeList '}';
1482+ | FieldType ',' FieldTypeList
1489+recordType :: SyntaxInfo -> IdrisParser PTerm
988 = do reserved "record"
1491 = do reserved "record"
989 lchar '{'
1492 lchar '{'
990− fields <- sepBy1 pFieldType (lchar ',')
1493+ fields <- sepBy1 fieldType (lchar ',')
991 lchar '}'
1494 lchar '}'
992− fc <- pfc
1495+ fc <- getFC
993− rec <- option Nothing (do e <- pSimpleExpr syn
1496+ rec <- optional (simpleExpr syn)
995 case rec of
1497 case rec of
996 Nothing ->
1498 Nothing ->
997 return (PLam (MN 0 "fldx") Placeholder
1499 return (PLam (MN 0 "fldx") Placeholder
998 (applyAll fc fields (PRef fc (MN 0 "fldx"))))
1500 (applyAll fc fields (PRef fc (MN 0 "fldx"))))
999 Just v -> return (applyAll fc fields v)
1501 Just v -> return (applyAll fc fields v)
1000− where pFieldType = do n <- pfName
1502+ <?> "record setting expression"
1503+ where fieldType :: IdrisParser (Name, PTerm)
1504+ fieldType = do n <- fnName
1001− lchar '='
1505+ lchar '='
1002− e <- pExpr syn
1506+ e <- expr syn
1003− return (n, e)
1507+ return (n, e)
1509+ applyAll :: FC -> [(Name, PTerm)] -> PTerm -> PTerm
1004 applyAll fc [] x = x
1510 applyAll fc [] x = x
1005 applyAll fc ((n, e) : es) x
1511 applyAll fc ((n, e) : es) x
1006 = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])
1512 = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])
1514+{- |Creates setters for record types on necessary functions -}
1515+mkType :: Name -> Name
1008mkType (UN n) = UN ("set_" ++ n)
1516mkType (UN n) = UN ("set_" ++ n)
1009mkType (MN 0 n) = MN 0 ("set_" ++ n)
1517mkType (MN 0 n) = MN 0 ("set_" ++ n)
1010mkType (NS n s) = NS (mkType n) s
1518mkType (NS n s) = NS (mkType n) s
1012−noImp syn = syn { implicitAllowed = False }
1520+{- |Parses a type for an expression
1013−impOK syn = syn { implicitAllowed = True }
1521+TypeSig ::=
1525+typeSig :: SyntaxInfo -> IdrisParser PTerm
1015−pTSig syn = do lchar ':'; pTExpr syn
1526+typeSig syn = lchar ':' *> typeExpr syn <?> "type"
1528+{- |Parses a type signature
1529+TypeExpr ::= ConstraintList? Expr;
1531+typeExpr :: SyntaxInfo -> IdrisParser PTerm
1017−pTExpr syn = do cs <- if implicitAllowed syn then pConstList syn else return []
1532+typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []
1018− sc <- pExpr syn
1533+ sc <- expr syn
1019− return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
1534+ return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
1020−
1535+ <?> "type signature"
1537+{- |Parses a lambda expression
1539+ '\\' TypeOptDeclList '=>' Expr
1540+ | '\\' SimpleExprList '=>' Expr
1544+ | SimpleExpr ',' SimpleExprList
1547+lambda :: SyntaxInfo -> IdrisParser PTerm
1021−pLambda syn = do lchar '\\'
1548+lambda syn = do lchar '\\'
1022− try (do xt <- tyOptDeclList syn
1549+ try (do xt <- tyOptDeclList syn
1552+ return (bindList PLam xt sc)
1553+ <|> (do ps <- sepBy (do fc <- getFC
1554+ e <- simpleExpr syn
1555+ return (fc, e)) (lchar ',')
1023 symbol "=>"
1556 symbol "=>"
1024− sc <- pExpr syn
1557+ sc <- expr syn
1025− return (bindList PLam xt sc)
1026− <|> (do ps <- sepBy (do fc <- pfc
1027− e <- pSimpleExpr syn
1028− return (fc, e)) (lchar ',')
1031− return (pmList (zip [0..] ps) sc)))
1558+ return (pmList (zip [0..] ps) sc)))
1559+ <?> "lambda expression"
1032− where pmList [] sc = sc
1560+ where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm
1033− pmList ((i, (fc, x)) : xs) sc
1562+ pmList ((i, (fc, x)) : xs) sc
1034 = PLam (MN i "lamp") Placeholder
1563 = PLam (MN i "lamp") Placeholder
1035 (PCase fc (PRef fc (MN i "lamp"))
1564 (PCase fc (PRef fc (MN i "lamp"))
1036 [(x, pmList xs sc)])
1565 [(x, pmList xs sc)])
1038−pRewriteTerm syn =
1567+{- |Parses a term rewrite expression
1569+ 'rewrite' Expr ('==>' Expr)? 'in' Expr
1572+rewriteTerm :: SyntaxInfo -> IdrisParser PTerm
1039− do reserved "rewrite"
1573+rewriteTerm syn = do reserved "rewrite"
1040− fc <- pfc
1574+ fc <- getFC
1041− prf <- pExpr syn
1575+ prf <- expr syn
1042− giving <- option Nothing
1043− (do symbol "==>"; tm <- pExpr' syn
1576+ giving <- optional (do symbol "==>"; expr' syn)
1045− reserved "in"; sc <- pExpr syn
1577+ reserved "in"; sc <- expr syn
1046− return (PRewrite fc
1578+ return (PRewrite fc
1047 (PApp fc (PRef fc (UN "sym")) [pexp prf]) sc
1579 (PApp fc (PRef fc (UN "sym")) [pexp prf]) sc
1049−
1581+ <?> "term rewrite expression"
1583+{- |Parses a let binding
1585+ 'let' Name TypeSig'? '=' Expr 'in' Expr
1586+| 'let' Expr' '=' Expr' 'in' Expr
1592+let_ :: SyntaxInfo -> IdrisParser PTerm
1050−pLet syn = try (do reserved "let"; n <- pName;
1593+let_ syn = try (do reserved "let"; n <- name;
1051− ty <- option Placeholder (do lchar ':'; pExpr' syn)
1594+ ty <- option Placeholder (do lchar ':'; expr' syn)
1052 lchar '='
1595 lchar '='
1053− v <- pExpr syn
1596+ v <- expr syn
1054− reserved "in"; sc <- pExpr syn
1597+ reserved "in"; sc <- expr syn
1055 return (PLet n ty v sc))
1598 return (PLet n ty v sc))
1056− <|> (do reserved "let"; fc <- pfc; pat <- pExpr' (syn { inPattern = True } )
1599+ <|> (do reserved "let"; fc <- getFC; pat <- expr' (syn { inPattern = True } )
1057− symbol "="; v <- pExpr syn
1600+ symbol "="; v <- expr syn
1058− reserved "in"; sc <- pExpr syn
1601+ reserved "in"; sc <- expr syn
1059 return (PCase fc v [(pat, sc)]))
1602 return (PCase fc v [(pat, sc)]))
1060−
1603+ <?> "let binding"
1605+{- |Parses a quote goal
1607+ 'quoteGoal' Name 'by' Expr 'in' Expr
1610+quoteGoal :: SyntaxInfo -> IdrisParser PTerm
1061−pQuoteGoal syn = do reserved "quoteGoal"; n <- pName;
1611+quoteGoal syn = do reserved "quoteGoal"; n <- name;
1062− reserved "by"
1612+ reserved "by"
1063− r <- pExpr syn
1613+ r <- expr syn
1064− reserved "in"
1614+ reserved "in"
1065− fc <- pfc
1615+ fc <- getFC
1066− sc <- pExpr syn
1616+ sc <- expr syn
1067− return (PGoal fc r n sc)
1617+ return (PGoal fc r n sc)
1068−
1618+ <?> "quote goal expression"
1620+{- |Parses a dependent type signature
1622+ '|'? Static? '(' TypeDeclList ')' DocComment '->' Expr
1623+ | '|'? Static? '{' TypeDeclList '}' '->' Expr
1624+ | '{' 'auto' TypeDeclList '}' '->' Expr
1625+ | '{' 'default' TypeDeclList '}' '->' Expr
1626+ | '{' 'static' '}' Expr' '->' Expr
1069−pPi syn =
1629+pi syn =
1070 try (do lazy <- if implicitAllowed syn -- laziness is top level only
1630 try (do lazy <- if implicitAllowed syn -- laziness is top level only
1071 then option False (do lchar '|'; return True)
1631 then option False (do lchar '|'; return True)
1072 else return False
1632 else return False
1073− st <- pStatic
1633+ st <- static
1074− lchar '('; xt <- tyDeclList syn; lchar ')'
1634+ lchar '('; xt <- typeDeclList syn; lchar ')'
1075− doc <- option "" (pDocComment '^')
1635+ doc <- option "" (docComment '^')
1076 symbol "->"
1636 symbol "->"
1077− sc <- pExpr syn
1637+ sc <- expr syn
1078 return (bindList (PPi (Exp lazy st doc)) xt sc))
1638 return (bindList (PPi (Exp lazy st doc)) xt sc))
1079− <|> try (if implicitAllowed syn
1639+ <|> try (if implicitAllowed syn
1080 then do lazy <- option False (do lchar '|'
1640 then do lazy <- option False (do lchar '|'
1081 return True)
1641 return True)
1082− st <- pStatic
1642+ st <- static
1083 lchar '{'
1643 lchar '{'
1084− xt <- tyDeclList syn
1644+ xt <- typeDeclList syn
1085 lchar '}'
1645 lchar '}'
1086 symbol "->"
1646 symbol "->"
1087− sc <- pExpr syn
1647+ sc <- expr syn
1088 return (bindList (PPi (Imp lazy st "")) xt sc)
1648 return (bindList (PPi (Imp lazy st "")) xt sc)
1089− else fail "No implicit arguments allowed here")
1649+ else fail "no implicit arguments allowed here")
1090 <|> try (do lchar '{'
1650 <|> try (do lchar '{'
1091 reserved "auto"
1651 reserved "auto"
1092− xt <- tyDeclList syn
1652+ xt <- typeDeclList syn
1093 lchar '}'
1653 lchar '}'
1094 symbol "->"
1654 symbol "->"
1095− sc <- pExpr syn
1655+ sc <- expr syn
1096− return (bindList (PPi
1656+ return (bindList (PPi
1097 (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))
1657 (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))
1098 <|> try (do lchar '{'
1658 <|> try (do lchar '{'
1099 reserved "default"
1659 reserved "default"
1100− script <- pSimpleExpr syn
1660+ script <- simpleExpr syn
1101− xt <- tyDeclList syn
1661+ xt <- typeDeclList syn
1102 lchar '}'
1662 lchar '}'
1103 symbol "->"
1663 symbol "->"
1104− sc <- pExpr syn
1664+ sc <- expr syn
1105 return (bindList (PPi (TacImp False Dynamic script "")) xt sc))
1665 return (bindList (PPi (TacImp False Dynamic script "")) xt sc))
1106− <|> do --lazy <- option False (do lchar '|'; return True)
1666+ <|> do lchar '{'
1108− reserved "static"
1667+ reserved "static"
1109− lchar '}'
1668+ lchar '}'
1110− t <- pExpr' syn
1669+ t <- expr' syn
1111− symbol "->"
1670+ symbol "->"
1112− sc <- pExpr syn
1671+ sc <- expr syn
1113− return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)
1672+ return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)
1114−
1673+ <?> "dependent type signature"
1675+{- | Parses a type constraint list
1677+ '(' Expr_List ')' '=>'
1115−pConstList :: SyntaxInfo -> IParser [PTerm]
1681+constraintList :: SyntaxInfo -> IdrisParser [PTerm]
1116−pConstList syn = try (do lchar '('
1682+constraintList syn = try (do lchar '('
1117− tys <- sepBy1 (pExpr' (noImp syn)) (lchar ',')
1683+ tys <- sepBy1 (expr' (disallowImp syn)) (lchar ',')
1118− lchar ')'
1684+ lchar ')'
1119− reservedOp "=>"
1685+ reservedOp "=>"
1120− return tys)
1686+ return tys)
1121− <|> try (do t <- pExpr (noImp syn)
1687+ <|> try (do t <- expr (disallowImp syn)
1122− reservedOp "=>"
1688+ reservedOp "=>"
1123− return [t])
1689+ return [t])
1124− <|> return []
1690+ <|> return []
1125−
1691+ <?> "type constraint list"
1693+{- | Parses a using declaration list
1701+ | UsingDecl ',' UsingDeclList'
1706+ | Name ',' NameList
1709+usingDeclList :: SyntaxInfo -> IdrisParser [Using]
1126−usingDeclList syn
1710+usingDeclList syn
1127 = try (sepBy1 (usingDecl syn) (lchar ','))
1711 = try (sepBy1 (usingDecl syn) (lchar ','))
1128− <|> do ns <- sepBy1 pName (lchar ',')
1712+ <|> do ns <- sepBy1 name (lchar ',')
1129− t <- pTSig (noImp syn)
1713+ t <- typeSig (disallowImp syn)
1130 return (map (\x -> UImplicit x t) ns)
1714 return (map (\x -> UImplicit x t) ns)
1131−
1715+ <?> "using declaration list"
1717+{- |Parses a using declaration
1723+usingDecl :: SyntaxInfo -> IdrisParser Using
1132−usingDecl syn = try (do x <- pfName
1724+usingDecl syn = try (do x <- fnName
1133− t <- pTSig (noImp syn)
1725+ t <- typeSig (disallowImp syn)
1134 return (UImplicit x t))
1726 return (UImplicit x t))
1135− <|> do c <- pfName
1727+ <|> do c <- fnName
1136− xs <- many1 pfName
1728+ xs <- some fnName
1137 return (UConstraint c xs)
1729 return (UConstraint c xs)
1138−
1730+ <?> "using declaration"
1732+{- |Parses a type declaration list
1734+ FunctionSignatureList
1738+FunctionSignatureList ::=
1740+ | Name TypeSig ',' FunctionSignatureList
1743+typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
1139−tyDeclList syn = try (sepBy1 (do x <- pfName
1744+typeDeclList syn = try (sepBy1 (do x <- fnName
1140− t <- pTSig (noImp syn)
1745+ t <- typeSig (disallowImp syn)
1141− return (x,t))
1746+ return (x,t))
1142− (lchar ','))
1747+ (lchar ','))
1143− <|> do ns <- sepBy1 pName (lchar ',')
1748+ <|> do ns <- sepBy1 name (lchar ',')
1144− t <- pTSig (noImp syn)
1749+ t <- typeSig (disallowImp syn)
1145− return (map (\x -> (x, t)) ns)
1750+ return (map (\x -> (x, t)) ns)
1146−
1751+ <?> "type declaration list"
1753+{- |Parses a type declaration list with optional parameters
1755+ NameOrPlaceholder TypeSig?
1756+ | NameOrPlaceholder TypeSig? ',' TypeOptDeclList
1759+NameOrPlaceHolder ::= Name | '_';
1761+tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
1147−tyOptDeclList syn = sepBy1 (do x <- pNameOrPlaceholder
1762+tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder
1148 t <- option Placeholder (do lchar ':'
1763 t <- option Placeholder (do lchar ':'
1149− pExpr syn)
1764+ expr syn)
1150 return (x,t))
1765 return (x,t))
1151 (lchar ',')
1766 (lchar ',')
1152− where pNameOrPlaceholder = pfName
1767+ <?> "type declaration list"
1768+ where nameOrPlaceholder :: IdrisParser Name
1769+ nameOrPlaceholder = fnName
1153 <|> do symbol "_"
1770 <|> do symbol "_"
1154 return (MN 0 "underscore")
1771 return (MN 0 "underscore")
1155−
1772+ <?> "name or placeholder"
1156−bindList b [] sc = sc
1773+
1157−bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
1774+{- |Parses a list comprehension
1158−
1775+Comprehension ::= '[' Expr '|' DoList ']';
1159−pComprehension syn
1776+
1782+comprehension :: SyntaxInfo -> IdrisParser PTerm
1160 = do lchar '['
1784 = do lchar '['
1161− fc <- pfc
1785+ fc <- getFC
1162− pat <- pExpr syn
1786+ pat <- expr syn
1163 lchar '|'
1787 lchar '|'
1164− qs <- sepBy1 (pDo syn) (lchar ',')
1788+ qs <- sepBy1 (do_ syn) (lchar ',')
1165 lchar ']'
1789 lchar ']'
1166− return (PDoBlock (map addGuard qs ++
1790+ return (PDoBlock (map addGuard qs ++
1167 [DoExp fc (PApp fc (PRef fc (UN "return"))
1791 [DoExp fc (PApp fc (PRef fc (UN "return"))
1168 [pexp pat])]))
1792 [pexp pat])]))
1793+ <?> "list comprehension"
1794+ where addGuard :: PDo -> PDo
1169− where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
1795+ addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
1170 [pexp e])
1796 [pexp e])
1171 addGuard x = x
1797 addGuard x = x
1173−pDoBlock syn
1799+{- |Parses a do-block
1800+Do' ::= Do KeepTerminator;
1803+ 'do' OpenBlock Do'+ CloseBlock
1806+doBlock :: SyntaxInfo -> IdrisParser PTerm
1174 = do reserved "do"
1808 = do reserved "do"
1175− openBlock
1809+ ds <- indentedBlock (do_ syn)
1177− ds <- many1 (do notEndBlock
1183 return (PDoBlock ds)
1810 return (PDoBlock ds)
1184−
1811+ <?> "do block"
1813+{- |Parses an expression inside a do block
1815+ 'let' Name TypeSig'? '=' Expr
1816+ | 'let' Expr' '=' Expr
1822+do_ :: SyntaxInfo -> IdrisParser PDo
1186 = try (do reserved "let"
1824 = try (do reserved "let"
1187− i <- pName;
1825+ i <- name
1188 ty <- option Placeholder (do lchar ':'
1826 ty <- option Placeholder (do lchar ':'
1189− pExpr' syn)
1827+ expr' syn)
1190 reservedOp "="
1828 reservedOp "="
1191− fc <- pfc
1829+ fc <- getFC
1192− e <- pExpr syn
1830+ e <- expr syn
1193 return (DoLet fc i ty e))
1831 return (DoLet fc i ty e))
1194 <|> try (do reserved "let"
1832 <|> try (do reserved "let"
1195− i <- pExpr' syn
1833+ i <- expr' syn
1196 reservedOp "="
1834 reservedOp "="
1197− fc <- pfc
1835+ fc <- getFC
1198− sc <- pExpr syn
1836+ sc <- expr syn
1199 return (DoLetP fc i sc))
1837 return (DoLetP fc i sc))
1200− <|> try (do i <- pName
1838+ <|> try (do i <- name
1201 symbol "<-"
1839 symbol "<-"
1202− fc <- pfc
1840+ fc <- getFC
1203− e <- pExpr syn;
1841+ e <- expr syn;
1204 return (DoBind fc i e))
1842 return (DoBind fc i e))
1205− <|> try (do i <- pExpr' syn
1843+ <|> try (do i <- expr' syn
1206 symbol "<-"
1844 symbol "<-"
1207− fc <- pfc
1845+ fc <- getFC
1208− e <- pExpr syn;
1846+ e <- expr syn;
1209 return (DoBindP fc i e))
1847 return (DoBindP fc i e))
1210− <|> try (do e <- pExpr syn
1848+ <|> try (do e <- expr syn
1211− fc <- pfc
1849+ fc <- getFC
1212 return (DoExp fc e))
1850 return (DoExp fc e))
1851+ <?> "do block expression"
1214−pIdiom syn
1853+{- |Parses an expression in idiom brackets
1854+Idiom ::= '[|' Expr '|]';
1856+idiom :: SyntaxInfo -> IdrisParser PTerm
1215 = do symbol "[|"
1858 = do symbol "[|"
1216− fc <- pfc
1859+ fc <- getFC
1217− e <- pExpr syn
1860+ e <- expr syn
1218 symbol "|]"
1861 symbol "|]"
1219 return (PIdiom fc e)
1862 return (PIdiom fc e)
1220−
1863+ <?> "expression in idiom brackets"
1221−pConstant :: IParser Const
1864+
1865+{- |Parses a constant or literal expression
1887+constant :: IdrisParser Core.TT.Const
1222−pConstant = do reserved "Integer";return (AType (ATInt ITBig))
1888+constant = do reserved "Integer";return (AType (ATInt ITBig))
1223 <|> do reserved "Int"; return (AType (ATInt ITNative))
1889 <|> do reserved "Int"; return (AType (ATInt ITNative))
1224 <|> do reserved "Char"; return (AType (ATInt ITChar))
1890 <|> do reserved "Char"; return (AType (ATInt ITChar))
1225 <|> do reserved "Float"; return (AType ATFloat)
1891 <|> do reserved "Float"; return (AType ATFloat)
@@ -1235,121 +1901,100 @@ pConstant = do reserved "Integer";return (AType (ATInt ITBig))
1235 <|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2)))
1901 <|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2)))
1236 <|> try (do f <- float; return $ Fl f)
1902 <|> try (do f <- float; return $ Fl f)
1237 <|> try (do i <- natural; return $ BI i)
1903 <|> try (do i <- natural; return $ BI i)
1238− <|> try (do s <- strlit; return $ Str s)
1904+ <|> try (do s <- stringLiteral; return $ Str s)
1239− <|> try (do c <- chlit; return $ Ch c)
1905+ <|> try (do c <- charLiteral; return $ Ch c)
1240−
1906+ <?> "constant or literal"
1241−pStatic :: IParser Static
1907+
1242−pStatic = do lchar '['
1908+{- |Parses a static modifier
1913+static :: IdrisParser Static
1243− reserved "static"
1914+static = do lchar '['; reserved "static"; lchar ']'; return Static
1246 <|> return Dynamic
1915 <|> return Dynamic
1247−
1916+ <?> "static modifier"
1249− = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
1918+{- |Parses a record type declaration
1250− [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]
1919+Record ::=
1251− ++ toTable (reverse fixes) ++
1920+ DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
1252− [[backtick],
1921+-}
1253− [binary "=" PEq AssocLeft],
1254− [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
1256−toTable fs = map (map toBin)
1257− (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
1258− where toBin (Fix (PrefixN _) op) = prefix op
1259− (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
1261− = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
1262− assoc (Infixl _) = AssocLeft
1263− assoc (Infixr _) = AssocRight
1264− assoc (InfixN _) = AssocNone
1266−binary name f = Infix (do fc <- pfc
1268− doc <- option "" (pDocComment '^')
1270−prefix name f = Prefix (do reservedOp name
1273−backtick = Infix (do lchar '`'; n <- pfName
1276− return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
1278−--------- Data declarations ---------
1280−-- (works for classes too - 'abstract' means the data/class is visible but members not)
1281−accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()
1282−accData (Just Frozen) n ns = do addAcc n (Just Frozen)
1283− mapM_ (\n -> addAcc n (Just Hidden)) ns
1284−accData a n ns = do addAcc n a
1285− mapM_ (`addAcc` a) ns
1287−pRecord :: SyntaxInfo -> IParser PDecl
1922+record :: SyntaxInfo -> IdrisParser PDecl
1288−pRecord syn = do doc <- option "" (pDocComment '|')
1923+record syn = do doc <- option "" (docComment '|')
1289− acc <- pAccessibility
1924+ acc <- optional accessibility
1290− reserved "record"
1925+ reserved "record"
1291− fc <- pfc
1926+ fc <- getFC
1292− tyn_in <- pfName
1927+ tyn_in <- fnName
1293− ty <- pTSig (impOK syn)
1928+ ty <- typeSig (allowImp syn)
1294− let tyn = expandNS syn tyn_in
1929+ let tyn = expandNS syn tyn_in
1295− reserved "where"
1930+ reserved "where"
1298− (cdoc, cn, cty, _) <- pConstructor syn
1931+ (cdoc, cn, cty, _) <- indentedBlockS (constructor syn)
1302− accData acc tyn [cn]
1932+ accData acc tyn [cn]
1303− let rsyn = syn { syn_namespace = show (nsroot tyn) :
1933+ let rsyn = syn { syn_namespace = show (nsroot tyn) :
1304− syn_namespace syn }
1934+ syn_namespace syn }
1305− let fns = getRecNames rsyn cty
1935+ let fns = getRecNames rsyn cty
1306− mapM_ (\n -> addAcc n acc) fns
1936+ mapM_ (\n -> addAcc n acc) fns
1307− return $ PRecord doc rsyn fc tyn ty cdoc cn cty
1937+ return $ PRecord doc rsyn fc tyn ty cdoc cn cty
1938+ <?> "record type declaration"
1940+ getRecNames :: SyntaxInfo -> PTerm -> [Name]
1309 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
1941 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
1310 ++ getRecNames syn sc
1942 ++ getRecNames syn sc
1311 getRecNames _ _ = []
1943 getRecNames _ _ = []
1945+ toFreeze :: Maybe Accessibility -> Maybe Accessibility
1313 toFreeze (Just Frozen) = Just Hidden
1946 toFreeze (Just Frozen) = Just Hidden
1314 toFreeze x = x
1947 toFreeze x = x
1949+{- | Parses data declaration type (normal or codata)
1950+DataI ::= 'data' | 'codata';
1952+dataI :: IdrisParser Bool
1316−pDataI = do reserved "data"; return False
1953+dataI = do reserved "data"; return False
1317− <|> do reserved "codata"; return True
1954+ <|> do reserved "codata"; return True
1956+{- | Parses a data type declaration
1957+Data ::= DocComment? Accessibility? DataI FnName TypeSig ExplicitTypeDataRest?
1958+ | DocComment? Accessibility? DataI FnName Name* DataRest?
1960+Constructor' ::= Constructor KeepTerminator;
1961+ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;
1963+DataRest ::= '=' SimpleConstructorList Terminator
1966+SimpleConstructorList ::=
1968+ | SimpleConstructor '|' SimpleConstructorList
1319−pData :: SyntaxInfo -> IParser PDecl
1971+data_ :: SyntaxInfo -> IdrisParser PDecl
1320−pData syn = try (do doc <- option "" (pDocComment '|')
1972+data_ syn = try (do doc <- option "" (docComment '|')
1321− acc <- pAccessibility
1973+ acc <- optional accessibility
1322− co <- pDataI
1974+ co <- dataI
1323− fc <- pfc
1975+ fc <- getFC
1324− tyn_in <- pfName
1976+ tyn_in <- fnName
1325− ty <- pTSig (impOK syn)
1977+ ty <- typeSig (allowImp syn)
1326 let tyn = expandNS syn tyn_in
1978 let tyn = expandNS syn tyn_in
1327 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1979 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1328 reserved "where"
1980 reserved "where"
1329− openBlock
1981+ cons <- indentedBlock (constructor syn)
1331− cons <- many (do notEndBlock
1332− c <- pConstructor syn
1334− return c) -- (lchar '|')
1337 accData acc tyn (map (\ (_, n, _, _) -> n) cons)
1982 accData acc tyn (map (\ (_, n, _, _) -> n) cons)
1338 return $ PData doc syn fc co (PDatadecl tyn ty cons)))
1983 return $ PData doc syn fc co (PDatadecl tyn ty cons)))
1339− <|> try (do doc <- option "" (pDocComment '|')
1984+ <|> try (do doc <- option "" (docComment '|')
1340 pushIndent
1985 pushIndent
1341− acc <- pAccessibility
1986+ acc <- optional accessibility
1342− co <- pDataI
1987+ co <- dataI
1343− fc <- pfc
1988+ fc <- getFC
1344− tyn_in <- pfName
1989+ tyn_in <- fnName
1345− args <- many pName
1990+ args <- many name
1346 let ty = bindArgs (map (const PType) args) PType
1991 let ty = bindArgs (map (const PType) args) PType
1347 let tyn = expandNS syn tyn_in
1992 let tyn = expandNS syn tyn_in
1348 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1993 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1349 try (lchar '=') <|> do reserved "where"
1994 try (lchar '=') <|> do reserved "where"
1350 let kw = (if co then "co" else "") ++ "data "
1995 let kw = (if co then "co" else "") ++ "data "
1351 let n = show tyn_in ++ " "
1996 let n = show tyn_in ++ " "
1352− let s = kw ++ n
1997+ let s = kw ++ n
1353 let as = concat (intersperse " " $ map show args) ++ " "
1998 let as = concat (intersperse " " $ map show args) ++ " "
1354 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
1999 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
1355 let ss = concat (intersperse " -> " $ map (const "Type") args)
2000 let ss = concat (intersperse " -> " $ map (const "Type") args)
@@ -1357,60 +2002,64 @@ pData syn = try (do doc <- option "" (pDocComment '|')
1357 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
2002 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
1358 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
2003 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
1359 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
2004 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
1361− cons <- sepBy1 (pSimpleCon syn) (lchar '|')
2005+ cons <- sepBy1 (simpleConstructor syn) (lchar '|')
1362− pTerminator
2006+ terminator
1363 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
2007 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
1364− cons' <- mapM (\ (doc, x, cargs, cfc) ->
2008+ cons' <- mapM (\ (doc, x, cargs, cfc) ->
1365 do let cty = bindArgs cargs conty
2009 do let cty = bindArgs cargs conty
1366 return (doc, x, cty, cfc)) cons
2010 return (doc, x, cty, cfc)) cons
1367 accData acc tyn (map (\ (_, n, _, _) -> n) cons')
2011 accData acc tyn (map (\ (_, n, _, _) -> n) cons')
1368 return $ PData doc syn fc co (PDatadecl tyn ty cons')))
2012 return $ PData doc syn fc co (PDatadecl tyn ty cons')))
2013+ <?> "data type declaration"
2015+ mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
1370 mkPApp fc t [] = t
2016 mkPApp fc t [] = t
1371 mkPApp fc t xs = PApp fc t (map pexp xs)
2017 mkPApp fc t xs = PApp fc t (map pexp xs)
2018+ bindArgs :: [PTerm] -> PTerm -> PTerm
2019+ bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
1373−bindArgs :: [PTerm] -> PTerm -> PTerm
1374−bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
2022+{- | Parses a type constructor declaration
2023+ Constructor ::= DocComment? FnName TypeSig;
1376−pConstructor :: SyntaxInfo -> IParser (String, Name, PTerm, FC)
2025+constructor :: SyntaxInfo -> IdrisParser (String, Name, PTerm, FC)
1377−pConstructor syn
2026+constructor syn
1378− = do doc <- option "" (pDocComment '|')
2027+ = do doc <- option "" (docComment '|')
1379− cn_in <- pfName; fc <- pfc
2028+ cn_in <- fnName; fc <- getFC
1380 let cn = expandNS syn cn_in
2029 let cn = expandNS syn cn_in
1381− ty <- pTSig (impOK syn)
2030+ ty <- typeSig (allowImp syn)
1382−-- ty' <- implicit syn cn ty
1383 return (doc, cn, ty, fc)
2031 return (doc, cn, ty, fc)
1384−
2032+ <?> "constructor"
2034+{- | Parses a constructor for simple discriminative union data types
2035+ SimpleConstructor ::= FnName SimpleExpr* DocComment?
1386−pSimpleCon :: SyntaxInfo -> IParser (String, Name, [PTerm], FC)
2037+simpleConstructor :: SyntaxInfo -> IdrisParser (String, Name, [PTerm], FC)
1387−pSimpleCon syn
2038+simpleConstructor syn
1388− = do cn_in <- pfName
2039+ = do cn_in <- fnName
1389 let cn = expandNS syn cn_in
2040 let cn = expandNS syn cn_in
1390− fc <- pfc
2041+ fc <- getFC
1391 args <- many (do notEndApp
2042 args <- many (do notEndApp
1392− pSimpleExpr syn)
2043+ simpleExpr syn)
1393− doc <- option "" (pDocComment '^')
2044+ doc <- option "" (docComment '^')
1394 return (doc, cn, args, fc)
2045 return (doc, cn, args, fc)
1395−
2046+ <?> "constructor"
1396−--------- DSL syntax overloading ---------
2047+
1397−
2048+{- | Parses a dsl block declaration
2049+DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;
1398−pDSL :: SyntaxInfo -> IParser PDecl
2051+dsl :: SyntaxInfo -> IdrisParser PDecl
1399−pDSL syn = do reserved "dsl"
2052+dsl syn = do reserved "dsl"
1400− n <- pfName
2053+ n <- fnName
1401− openBlock
2054+ bs <- indentedBlock (overload syn)
1403− bs <- many1 (do notEndBlock
1407− popIndent; closeBlock
1408− let dsl = mkDSL bs (dsl_info syn)
2055+ let dsl = mkDSL bs (dsl_info syn)
1409− checkDSL dsl
2056+ checkDSL dsl
1410− i <- getState
2057+ i <- get
1411− setState (i { idris_dsls = addDef n dsl (idris_dsls i) })
2058+ put (i { idris_dsls = addDef n dsl (idris_dsls i) })
1412− return (PDSL n dsl)
2059+ return (PDSL n dsl)
2060+ <?> "dsl block declaration"
2061+ where mkDSL :: [(String, PTerm)] -> DSL -> DSL
1413− where mkDSL bs dsl = let var = lookup "variable" bs
2062+ mkDSL bs dsl = let var = lookup "variable" bs
1414 first = lookup "index_first" bs
2063 first = lookup "index_first" bs
1415 next = lookup "index_next" bs
2064 next = lookup "index_next" bs
1416 leto = lookup "let" bs
2065 leto = lookup "let" bs
@@ -1421,229 +2070,309 @@ pDSL syn = do reserved "dsl"
1421 dsl_lambda = lambda,
2070 dsl_lambda = lambda,
1422 dsl_let = leto }
2071 dsl_let = leto }
2073+{- | Checks DSL for errors -}
2074+-- FIXME: currently does nothing, check if DSL is really sane
1424−checkDSL :: DSL -> IParser ()
2075+checkDSL :: DSL -> IdrisParser ()
1425checkDSL dsl = return ()
2076checkDSL dsl = return ()
2078+{- | Parses a DSL overload declaration
2079+OverloadIdentifier ::= 'let' | Identifier;
2080+Overload ::= OverloadIdentifier '=' Expr;
1427−pOverload :: SyntaxInfo -> IParser (String, PTerm)
2082+overload :: SyntaxInfo -> IdrisParser (String, PTerm)
1428−pOverload syn = do o <- identifier <|> do reserved "let"
2083+overload syn = do o <- identifier <|> do reserved "let"
1429− return "let"
2084+ return "let"
1430− if o `notElem` overloadable
2085+ if o `notElem` overloadable
1431− then fail $ show o ++ " is not an overloading"
2086+ then fail $ show o ++ " is not an overloading"
1432− else do
2087+ else do
1433− lchar '='
2088+ lchar '='
1434− t <- pExpr syn
2089+ t <- expr syn
1435− return (o, t)
2090+ return (o, t)
2091+ <?> "dsl overload declaratioN"
1436 where overloadable = ["let","lambda","index_first","index_next","variable"]
2092 where overloadable = ["let","lambda","index_first","index_next","variable"]
2094+{- | Parse a clause with patterns
1438−--------- Pattern match clauses ---------
2095+Pattern ::= Clause;
1440−pPattern :: SyntaxInfo -> IParser PDecl
2097+pattern :: SyntaxInfo -> IdrisParser PDecl
1441−pPattern syn = do fc <- pfc
2098+pattern syn = do fc <- getFC
1442− clause <- pClause syn
2099+ clause <- clause syn
1443− return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
2100+ return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
2103+{- | Parse a constant applicative form declaration
2104+ CAF ::= 'let' FnName '=' Expr Terminator;
1445−pCAF :: SyntaxInfo -> IParser PDecl
2106+caf :: SyntaxInfo -> IdrisParser PDecl
1446−pCAF syn = do reserved "let"
2107+caf syn = do reserved "let"
1447− n_in <- pfName; let n = expandNS syn n_in
2108+ n_in <- fnName; let n = expandNS syn n_in
1448− lchar '='
2109+ lchar '='
1449− t <- pExpr syn
2110+ t <- expr syn
1450− pTerminator
2111+ terminator
1451− fc <- pfc
2112+ fc <- getFC
1452− return (PCAF fc n t)
2113+ return (PCAF fc n t)
1453−
2114+ <?> "constant applicative form declaration"
2116+{- | Parse an argument expression
2117+ ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
2119+argExpr :: SyntaxInfo -> IdrisParser PTerm
1454−pArgExpr syn = let syn' = syn { inPattern = True } in
2120+argExpr syn = let syn' = syn { inPattern = True } in
1455− try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
2121+ try (hsimpleExpr syn') <|> simpleExternalExpr syn'
1456−
2122+ <?> "argument expression"
2124+{- | Parse a right hand side of a function
2126+ | '?=' RHSName? Expr
2130+RHSName ::= '{' FnName '}';
1457−pRHS :: SyntaxInfo -> Name -> IParser PTerm
2132+rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
1458−pRHS syn n = do lchar '='; pExpr syn
2133+rhs syn n = do lchar '='; expr syn
1459− <|> do symbol "?=";
2134+ <|> do symbol "?=";
1460− name <- option n' (do symbol "{"; n <- pfName; symbol "}";
2135+ name <- option n' (do symbol "{"; n <- fnName; symbol "}";
1461− return n)
2136+ return n)
1462− rhs <- pExpr syn
2137+ r <- expr syn
1463− return (addLet name rhs)
2138+ return (addLet name r)
1464− <|> do reserved "impossible"; return PImpossible
2139+ <|> do reserved "impossible"; return PImpossible
2140+ <?> "function right hand side"
2141+ where mkN :: Name -> Name
1465− where mkN (UN x) = UN (x++"_lemma_1")
2142+ mkN (UN x) = UN (x++"_lemma_1")
1466 mkN (NS x n) = NS (mkN x) n
2143 mkN (NS x n) = NS (mkN x) n
1467 n' = mkN n
2145 n' = mkN n
1468−
2146+ addLet :: Name -> PTerm -> PTerm
1469− addLet nm (PLet n ty val rhs) = PLet n ty val (addLet nm rhs)
2147+ addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)
1470 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
2148 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
1471 where addLetC (l, r) = (l, addLet nm r)
2149 where addLetC (l, r) = (l, addLet nm r)
1472− addLet nm rhs = (PLet (UN "value") Placeholder rhs (PMetavar nm))
2150+ addLet nm r = (PLet (UN "value") Placeholder r (PMetavar nm))
2152+{- |Parses a function clause
2153+Clause ::= FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHS WhereOrTerminator
2154+ | SimpleExpr '<==' FnName RHS WhereOrTerminator
2155+ | WExpr+ RHS WhereOrTerminator
2156+ | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
2157+ | WExpr+ 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
2158+ | ArgExpr Operator ArgExpr WExpr* RHS WhereOrTerminator
2159+ | ArgExpr Operator ArgExpr WExpr* 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
2161+ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
2162+WhereOrTerminator ::= WhereBlock | Terminator;
1474−pClause :: SyntaxInfo -> IParser PClause
2164+clause :: SyntaxInfo -> IdrisParser PClause
1475−pClause syn
2165+clause syn
1476 = try (do pushIndent
2166 = try (do pushIndent
1477− n_in <- pfName; let n = expandNS syn n_in
2167+ n_in <- fnName; let n = expandNS syn n_in
1478− cargs <- many (pConstraintArg syn)
2168+ cargs <- many (constraintArg syn)
1479− iargs <- many (pImplicitArg (syn { inPattern = True } ))
2169+ fc <- getFC
1481− args <- many (try (pImplicitArg (syn { inPattern = True } ))
2170+ args <- many (try (implicitArg (syn { inPattern = True } ))
1482− <|> (fmap pexp (pArgExpr syn)))
2171+ <|> (fmap pexp (argExpr syn)))
1483− wargs <- many (pWExpr syn)
2172+ wargs <- many (wExpr syn)
1484− rhs <- pRHS syn n
2173+ r <- rhs syn n
1485− ist <- getState
2174+ ist <- get
1486 let ctxt = tt_ctxt ist
2175 let ctxt = tt_ctxt ist
1487 let wsyn = syn { syn_namespace = [] }
2176 let wsyn = syn { syn_namespace = [] }
1488− (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
2177+ (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1489 popIndent
2178 popIndent
1490− return x,
2179+ return x,
1491− do pTerminator
2180+ do terminator
1492 return ([], [])]
2181 return ([], [])]
1493− let capp = PApp fc (PRef fc n)
2182+ let capp = PApp fc (PRef fc n)
1494− (iargs ++ cargs ++ args)
2183+ (cargs ++ args)
1495− ist <- getState
2184+ ist <- get
1496− setState (ist { lastParse = Just n })
2185+ put (ist { lastParse = Just n })
1497− return $ PClause fc n capp wargs rhs wheres)
2186+ return $ PClause fc n capp wargs r wheres)
1498 <|> try (do pushIndent
2187 <|> try (do pushIndent
1499− ty <- pSimpleExpr syn
2188+ ty <- simpleExpr syn
1500 symbol "<=="
2189 symbol "<=="
1501− fc <- pfc
2190+ fc <- getFC
1502− n_in <- pfName; let n = expandNS syn n_in
2191+ n_in <- fnName; let n = expandNS syn n_in
1503− rhs <- pRHS syn n
2192+ r <- rhs syn n
1504− ist <- getState
2193+ ist <- get
1505 let ctxt = tt_ctxt ist
2194 let ctxt = tt_ctxt ist
1506 let wsyn = syn { syn_namespace = [] }
2195 let wsyn = syn { syn_namespace = [] }
1507− (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
2196+ (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1508 popIndent
2197 popIndent
1509− return x,
2198+ return x,
1510− do pTerminator
2199+ do terminator
1511 return ([], [])]
2200 return ([], [])]
1512 let capp = PLet (MN 0 "match")
2201 let capp = PLet (MN 0 "match")
1514 (PMatchApp fc n)
2203 (PMatchApp fc n)
1515 (PRef fc (MN 0 "match"))
2204 (PRef fc (MN 0 "match"))
1516− ist <- getState
2205+ ist <- get
1517− setState (ist { lastParse = Just n })
2206+ put (ist { lastParse = Just n })
1518− return $ PClause fc n capp [] rhs wheres)
2207+ return $ PClause fc n capp [] r wheres)
1519 <|> try (do pushIndent
2208 <|> try (do pushIndent
1520− wargs <- many1 (pWExpr syn)
2209+ wargs <- some (wExpr syn)
1521− ist <- getState
2210+ ist <- get
1522 n <- case lastParse ist of
2211 n <- case lastParse ist of
1523 Just t -> return t
2212 Just t -> return t
1524 Nothing -> fail "Invalid clause"
2213 Nothing -> fail "Invalid clause"
1525− fc <- pfc
2214+ fc <- getFC
1526− rhs <- pRHS syn n
2215+ r <- rhs syn n
1527 let ctxt = tt_ctxt ist
2216 let ctxt = tt_ctxt ist
1528 let wsyn = syn { syn_namespace = [] }
2217 let wsyn = syn { syn_namespace = [] }
1529− (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
2218+ (wheres, nmap) <- choice [do x <- whereBlock n wsyn
1530 popIndent
2219 popIndent
1531− return x,
2220+ return x,
1532− do pTerminator
2221+ do terminator
1533 return ([], [])]
2222 return ([], [])]
1534− return $ PClauseR fc wargs rhs wheres)
2223+ return $ PClauseR fc wargs r wheres)
1536 <|> try (do pushIndent
2225 <|> try (do pushIndent
1537− n_in <- pfName; let n = expandNS syn n_in
2226+ n_in <- fnName; let n = expandNS syn n_in
1538− cargs <- many (pConstraintArg syn)
2227+ cargs <- many (constraintArg syn)
1539− iargs <- many (pImplicitArg (syn { inPattern = True } ))
2228+ fc <- getFC
1541− args <- many (try (pImplicitArg (syn { inPattern = True } ))
2229+ args <- many (try (implicitArg (syn { inPattern = True } ))
1542− <|> (fmap pexp (pArgExpr syn)))
2230+ <|> (fmap pexp (argExpr syn)))
1543− wargs <- many (pWExpr syn)
2231+ wargs <- many (wExpr syn)
1544− let capp = PApp fc (PRef fc n)
2232+ let capp = PApp fc (PRef fc n)
1545− (iargs ++ cargs ++ args)
2233+ (cargs ++ args)
1546− ist <- getState
2234+ ist <- get
1547− setState (ist { lastParse = Just n })
2235+ put (ist { lastParse = Just n })
1548 reserved "with"
2236 reserved "with"
1549− wval <- pSimpleExpr syn
2237+ wval <- simpleExpr syn
1550 openBlock
2238 openBlock
1551− ds <- many1 $ pFunDecl syn
2239+ ds <- some $ fnDecl syn
1552 let withs = map (fillLHSD n capp wargs) $ concat ds
2240 let withs = map (fillLHSD n capp wargs) $ concat ds
1553 closeBlock
2241 closeBlock
1554 popIndent
2242 popIndent
1555 return $ PWith fc n capp wargs wval withs)
2243 return $ PWith fc n capp wargs wval withs)
1557− <|> try (do wargs <- many1 (pWExpr syn)
2245+ <|> try (do wargs <- some (wExpr syn)
1558− fc <- pfc
2246+ fc <- getFC
1559 reserved "with"
2247 reserved "with"
1560− wval <- pSimpleExpr syn
2248+ wval <- simpleExpr syn
1561 openBlock
2249 openBlock
1562− ds <- many1 $ pFunDecl syn
2250+ ds <- some $ fnDecl syn
1563 let withs = concat ds
2251 let withs = concat ds
1564 closeBlock
2252 closeBlock
1565 return $ PWithR fc wargs wval withs)
2253 return $ PWithR fc wargs wval withs)
1570− let n = expandNS syn (UN op)
1573− wargs <- many (pWExpr syn)
1575− let wsyn = syn { syn_namespace = [] }
1576− (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1582− let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1583− setState (ist { lastParse = Just n })
1584− return $ PClause fc n capp wargs rhs wheres
1586− <|> do l <- pArgExpr syn
2255+ <|> try(do pushIndent
2258+ let n = expandNS syn (UN op)
2261+ wargs <- many (wExpr syn)
2263+ let wsyn = syn { syn_namespace = [] }
2264+ (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2270+ let capp = PApp fc (PRef fc n) [pexp l, pexp r]
2271+ put (ist { lastParse = Just n })
2272+ return $ PClause fc n capp wargs rs wheres)
2274+ <|> do l <- argExpr syn
1587 op <- operator
2275 op <- operator
1588 let n = expandNS syn (UN op)
2276 let n = expandNS syn (UN op)
1589− r <- pArgExpr syn
2277+ r <- argExpr syn
1590− fc <- pfc
2278+ fc <- getFC
1591− wargs <- many (pWExpr syn)
2279+ wargs <- many (wExpr syn)
1592 reserved "with"
2280 reserved "with"
1593− wval <- pSimpleExpr syn
2281+ wval <- simpleExpr syn
1594− openBlock
2282+ openBlock
1595− ds <- many1 $ pFunDecl syn
2283+ ds <- some $ fnDecl syn
1596 closeBlock
2284 closeBlock
1597− ist <- getState
2285+ ist <- get
1598 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
2286 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1599 let withs = map (fillLHSD n capp wargs) $ concat ds
2287 let withs = map (fillLHSD n capp wargs) $ concat ds
1600− setState (ist { lastParse = Just n })
2288+ put (ist { lastParse = Just n })
1601 return $ PWith fc n capp wargs wval withs
2289 return $ PWith fc n capp wargs wval withs
2290+ <?> "function clause"
2292+ fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
1603− fillLHS n capp owargs (PClauseR fc wargs v ws)
2293+ fillLHS n capp owargs (PClauseR fc wargs v ws)
1604 = PClause fc n capp (owargs ++ wargs) v ws
2294 = PClause fc n capp (owargs ++ wargs) v ws
1605− fillLHS n capp owargs (PWithR fc wargs v ws)
2295+ fillLHS n capp owargs (PWithR fc wargs v ws)
1606− = PWith fc n capp (owargs ++ wargs) v
2296+ = PWith fc n capp (owargs ++ wargs) v
1607 (map (fillLHSD n capp (owargs ++ wargs)) ws)
2297 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1608 fillLHS _ _ _ c = c
2298 fillLHS _ _ _ c = c
2300+ fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
1610 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
2301 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1611 fillLHSD n c a x = x
2302 fillLHSD n c a x = x
2304+{- |Parses with pattern
2305+ WExpr ::= '|' Expr';
1613−pWExpr :: SyntaxInfo -> IParser PTerm
2307+wExpr :: SyntaxInfo -> IdrisParser PTerm
1614−pWExpr syn = do lchar '|'
2308+wExpr syn = do lchar '|'
1615− pExpr' syn
2309+ expr' syn
1616−
2310+ <?> "with pattern"
2312+{- |Parses a where block
2313+WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
1617−pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
2315+whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
1618−pWhereblock n syn
2316+whereBlock n syn
1619− = do reserved "where"; openBlock
2317+ = do reserved "where"
1620− ds <- many1 $ pDecl syn
2318+ ds <- indentedBlock1 (decl syn)
1621 let dns = concatMap (concatMap declared) ds
2319 let dns = concatMap (concatMap declared) ds
1623 return (concat ds, map (\x -> (x, decoration syn x)) dns)
2320 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1624−
2321+ <?> "where block"
1625−pCodegen :: IParser Codegen
2322+
2323+{- |Parses a code generation target language name
2332+codegen_ :: IdrisParser Codegen
1626−pCodegen = try (do reserved "C"; return ViaC)
2333+codegen_ = try (do reserved "C"; return ViaC)
1627− <|> try (do reserved "Java"; return ViaJava)
2334+ <|> try (do reserved "Java"; return ViaJava)
1628− <|> try (do reserved "JavaScript"; return ViaJavaScript)
2335+ <|> try (do reserved "JavaScript"; return ViaJavaScript)
1629− <|> try (do reserved "Node"; return ViaNode)
2336+ <|> try (do reserved "Node"; return ViaNode)
1630− <|> try (do reserved "LLVM"; return ViaLLVM)
2337+ <|> try (do reserved "LLVM"; return ViaLLVM)
1631− <|> try (do reserved "Bytecode"; return Bytecode)
2338+ <|> try (do reserved "Bytecode"; return Bytecode)
1632−
2339+ <?> "code generation language"
2341+{- |Parses a compiler directive
2344+ | String ',' StringList
2347+Directive ::= '%' Directive';
2349+Directive' ::= 'lib' CodeGen String_t
2350+ | 'link' CodeGen String_t
2351+ | 'flag' CodeGen String_t
2352+ | 'include' CodeGen String_t
2355+ | 'access' Accessibility
2356+ | 'default' Totality
2357+ | 'logging' Natural
2358+ | 'dynamic' StringList
2359+ | 'language' 'TypeProviders'
1633−pDirective :: SyntaxInfo -> IParser [PDecl]
2362+directive :: SyntaxInfo -> IdrisParser [PDecl]
1634−pDirective syn = try (do lchar '%'; reserved "lib"; cgn <- pCodegen; lib <- strlit;
2363+directive syn = try (do lchar '%'; reserved "lib"; cgn <- codegen_; lib <- stringLiteral;
1635− return [PDirective (do addLib cgn lib
2364+ return [PDirective (do addLib cgn lib
1636− addIBC (IBCLib cgn lib))])
2365+ addIBC (IBCLib cgn lib))])
1637− <|> try (do lchar '%'; reserved "link"; cgn <- pCodegen; obj <- strlit;
2366+ <|> try (do lchar '%'; reserved "link"; cgn <- codegen_; obj <- stringLiteral;
1638 return [PDirective (do dirs <- allImportDirs
2367 return [PDirective (do dirs <- allImportDirs
1639 o <- liftIO $ findInPath dirs obj
2368 o <- liftIO $ findInPath dirs obj
1640 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
2369 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
1641 addObjectFile cgn o)])
2370 addObjectFile cgn o)])
1642− <|> try (do lchar '%'; reserved "flag"; cgn <- pCodegen;
2371+ <|> try (do lchar '%'; reserved "flag"; cgn <- codegen_;
1643− flag <- strlit
2372+ flag <- stringLiteral
1644 return [PDirective (do addIBC (IBCCGFlag cgn flag)
2373 return [PDirective (do addIBC (IBCCGFlag cgn flag)
1645 addFlag cgn flag)])
2374 addFlag cgn flag)])
1646− <|> try (do lchar '%'; reserved "include"; cgn <- pCodegen; hdr <- strlit;
2375+ <|> try (do lchar '%'; reserved "include"; cgn <- codegen_; hdr <- stringLiteral;
1647 return [PDirective (do addHdr cgn hdr
2376 return [PDirective (do addHdr cgn hdr
1648 addIBC (IBCHeader cgn hdr))])
2377 addIBC (IBCHeader cgn hdr))])
1649 <|> try (do lchar '%'; reserved "hide"; n <- iName []
2378 <|> try (do lchar '%'; reserved "hide"; n <- iName []
@@ -1652,17 +2381,17 @@ pDirective syn = try (do lchar '%'; reserved "lib"; cgn <- pCodegen; lib <- strl
1652 <|> try (do lchar '%'; reserved "freeze"; n <- iName []
2381 <|> try (do lchar '%'; reserved "freeze"; n <- iName []
1653 return [PDirective (do setAccessibility n Frozen
2382 return [PDirective (do setAccessibility n Frozen
1654 addIBC (IBCAccess n Frozen))])
2383 addIBC (IBCAccess n Frozen))])
1655− <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'
2384+ <|> try (do lchar '%'; reserved "access"; acc <- accessibility
1656− return [PDirective (do i <- getIState
2385+ return [PDirective (do i <- get
1657− putIState (i { default_access = acc }))])
2386+ put(i { default_access = acc }))])
1658− <|> try (do lchar '%'; reserved "default"; tot <- pTotality
2387+ <|> try (do lchar '%'; reserved "default"; tot <- totality
1659− i <- getState
2388+ i <- get
1660− setState (i { default_total = tot } )
2389+ put (i { default_total = tot } )
1661− return [PDirective (do i <- getIState
2390+ return [PDirective (do i <- get
1662− putIState (i { default_total = tot }))])
2391+ put(i { default_total = tot }))])
1663 <|> try (do lchar '%'; reserved "logging"; i <- natural;
2392 <|> try (do lchar '%'; reserved "logging"; i <- natural;
1664 return [PDirective (setLogLevel (fromInteger i))])
2393 return [PDirective (setLogLevel (fromInteger i))])
1665− <|> try (do lchar '%'; reserved "dynamic"; libs <- sepBy1 strlit (lchar ',');
2394+ <|> try (do lchar '%'; reserved "dynamic"; libs <- sepBy1 stringLiteral (lchar ',');
1666 return [PDirective (do added <- addDyLib libs
2395 return [PDirective (do added <- addDyLib libs
1667 case added of
2396 case added of
1668 Left lib -> addIBC (IBCDyLib (lib_name lib))
2397 Left lib -> addIBC (IBCDyLib (lib_name lib))
@@ -1670,78 +2399,132 @@ pDirective syn = try (do lchar '%'; reserved "lib"; cgn <- pCodegen; lib <- strl
1670 fail $ msg)])
2399 fail $ msg)])
1671 <|> try (do lchar '%'; reserved "language"; ext <- reserved "TypeProviders";
2400 <|> try (do lchar '%'; reserved "language"; ext <- reserved "TypeProviders";
1672 return [PDirective (addLangExt TypeProviders)])
2401 return [PDirective (addLangExt TypeProviders)])
1674−pProvider :: SyntaxInfo -> IParser [PDecl]
2404+{- | Parses a totality
1675−pProvider syn = do lchar '%'; reserved "provide";
2405+Totality ::= 'partial' | 'total'
1676− lchar '('; n <- pfName; t <- pTSig syn; lchar ')'
2406+-}
1677− fc <- pfc
2407+totality :: IdrisParser Bool
2409+ = do reserved "total"; return True
1678− reserved "with"
2410+ <|> do reserved "partial"; return False
1680− return [PProvider syn fc n t e]
2412+{- | Parses a type provider
2413+Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;
2415+provider :: SyntaxInfo -> IdrisParser [PDecl]
2416+provider syn = do lchar '%'; reserved "provide";
2417+ lchar '('; n <- fnName; t <- typeSig syn; lchar ')'
2421+ return [PProvider syn fc n t e]
2422+ <?> "type provider"
2424+{- | Parses a transform
2425+Transform ::= '%' 'transform' Expr '==>' Expr
1682−pTransform :: SyntaxInfo -> IParser [PDecl]
2427+transform :: SyntaxInfo -> IdrisParser [PDecl]
1683−pTransform syn = do lchar '%'; reserved "transform";
2428+transform syn = do lchar '%'; reserved "transform";
1684 -- leave it unchecked, until we work out what this should
2429 -- leave it unchecked, until we work out what this should
1685 -- actually mean...
2430 -- actually mean...
1686-- safety <- option True (do reserved "unsafe"
2431-- safety <- option True (do reserved "unsafe"
1687-- return False)
2432-- return False)
1688− lhs <- pExpr syn
2433+ l <- expr syn
1689− fc <- pfc
2434+ fc <- getFC
1690− symbol "==>"
2435+ symbol "==>"
1691− rhs <- pExpr syn
2436+ r <- expr syn
1692− return [PTransform fc False lhs rhs]
2437+ return [PTransform fc False l r]
1693−
2438+ <?> "transform"
2440+{- | Parses a tactic script
2441+Tactic ::= 'intro' NameList?
2443+ | 'refine' Name Imp+
2447+ | 'let' Name ':' Expr' '=' Expr
2448+ | 'let' Name '=' Expr
2451+ | 'applyTactic' Expr
2454+ | 'try' Tactic '|' Tactic
2455+ | '{' TacticSeq '}'
2472+ | Tactic ';' TacticSeq
1694−pTactic :: SyntaxInfo -> IParser PTactic
2477+tactic :: SyntaxInfo -> IdrisParser PTactic
1695−pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
2478+tactic syn = do reserved "intro"; ns <- sepBy name (lchar ',')
1696− return $ Intro ns
2479+ return $ Intro ns
1697 <|> do reserved "intros"; return Intros
2480 <|> do reserved "intros"; return Intros
1698− <|> try (do reserved "refine"; n <- pName
2481+ <|> try (do reserved "refine"; n <- name
1699− imps <- many1 imp
2482+ imps <- some imp
1700 return $ Refine n imps)
2483 return $ Refine n imps)
1701− <|> do reserved "refine"; n <- pName
2484+ <|> do reserved "refine"; n <- name
1702− i <- getState
2485+ i <- get
1703 return $ Refine n []
2486 return $ Refine n []
1704− <|> do reserved "mrefine"; n <- pName
2487+ <|> do reserved "mrefine"; n <- name
1705− i <- getState
2488+ i <- get
1706 return $ MatchRefine n
2489 return $ MatchRefine n
1707− <|> do reserved "rewrite"; t <- pExpr syn;
2490+ <|> do reserved "rewrite"; t <- expr syn;
1708− i <- getState
2491+ i <- get
1709 return $ Rewrite (desugar syn i t)
2492 return $ Rewrite (desugar syn i t)
1710− <|> do reserved "equiv"; t <- pExpr syn;
2493+ <|> do reserved "equiv"; t <- expr syn;
1711− i <- getState
2494+ i <- get
1712 return $ Equiv (desugar syn i t)
2495 return $ Equiv (desugar syn i t)
1713− <|> try (do reserved "let"; n <- pName; lchar ':';
2496+ <|> try (do reserved "let"; n <- name; lchar ':';
1714− ty <- pExpr' syn; lchar '='; t <- pExpr syn;
2497+ ty <- expr' syn; lchar '='; t <- expr syn;
1715− i <- getState
2498+ i <- get
1716 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
2499 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
1717− <|> try (do reserved "let"; n <- pName; lchar '=';
2500+ <|> try (do reserved "let"; n <- name; lchar '=';
1718− t <- pExpr syn;
2501+ t <- expr syn;
1719− i <- getState
2502+ i <- get
1720 return $ LetTac n (desugar syn i t))
2503 return $ LetTac n (desugar syn i t))
1721− <|> do reserved "focus"; n <- pName
2504+ <|> do reserved "focus"; n <- name
1722 return $ Focus n
2505 return $ Focus n
1723− <|> do reserved "exact"; t <- pExpr syn;
2506+ <|> do reserved "exact"; t <- expr syn;
1724− i <- getState
2507+ i <- get
1725 return $ Exact (desugar syn i t)
2508 return $ Exact (desugar syn i t)
1726− <|> do reserved "applyTactic"; t <- pExpr syn;
2509+ <|> do reserved "applyTactic"; t <- expr syn;
1727− i <- getState
2510+ i <- get
1728 return $ ApplyTactic (desugar syn i t)
2511 return $ ApplyTactic (desugar syn i t)
1729− <|> do reserved "reflect"; t <- pExpr syn;
2512+ <|> do reserved "reflect"; t <- expr syn;
1730− i <- getState
2513+ i <- get
1731 return $ Reflect (desugar syn i t)
2514 return $ Reflect (desugar syn i t)
1732− <|> do reserved "fill"; t <- pExpr syn;
2515+ <|> do reserved "fill"; t <- expr syn;
1733− i <- getState
2516+ i <- get
1734 return $ Fill (desugar syn i t)
2517 return $ Fill (desugar syn i t)
1735− <|> do reserved "try"; t <- pTactic syn;
2518+ <|> do reserved "try"; t <- tactic syn;
1736 lchar '|';
2519 lchar '|';
1737− t1 <- pTactic syn
2520+ t1 <- tactic syn
1738 return $ Try t t1
2521 return $ Try t t1
1739 <|> do lchar '{'
2522 <|> do lchar '{'
1740− t <- pTactic syn;
2523+ t <- tactic syn;
1741 lchar ';';
2524 lchar ';';
1742− t1 <- pTactic syn;
2525+ ts <- sepBy1 (tactic syn) (lchar ';')
1743 lchar '}'
2526 lchar '}'
1744− return $ TSeq t t1
2527+ return $ TSeq t (mergeSeq ts)
1745 <|> do reserved "compute"; return Compute
2528 <|> do reserved "compute"; return Compute
1746 <|> do reserved "trivial"; return Trivial
2529 <|> do reserved "trivial"; return Trivial
1747 <|> do reserved "solve"; return Solve
2530 <|> do reserved "solve"; return Solve
@@ -1752,7 +2535,229 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
1752 <|> do reserved "qed"; return Qed
2535 <|> do reserved "qed"; return Qed
1753 <|> do reserved "abandon"; return Abandon
2536 <|> do reserved "abandon"; return Abandon
1754 <|> do lchar ':'; reserved "q"; return Abandon
2537 <|> do lchar ':'; reserved "q"; return Abandon
2540+ imp :: IdrisParser Bool
1756 imp = do lchar '?'; return False
2541 imp = do lchar '?'; return False
1757 <|> do lchar '_'; return True
2542 <|> do lchar '_'; return True
2543+ mergeSeq :: [PTactic] -> PTactic
2545+ mergeSeq (t:ts) = TSeq t (mergeSeq ts)
2547+{- | Parses a tactic as a whole -}
2548+fullTactic :: SyntaxInfo -> IdrisParser PTactic
2549+fullTactic syn = do t <- tactic syn
2553+{- * Loading and parsing -}
2554+{- | Parses an expression from input -}
2555+parseExpr :: IState -> String -> Result PTerm
2556+parseExpr st = parseString (evalStateT (fullExpr defaultSyntax) st) (Directed (UTF8.fromString "(input)") 0 0 0 0)
2558+{- | Parses a tactic from input -}
2559+parseTactic :: IState -> String -> Result PTactic
2560+parseTactic st = parseString (evalStateT (fullTactic defaultSyntax) st) (Directed (UTF8.fromString "(input)") 0 0 0 0)
2562+-- | Parse module header and imports
2563+parseImports :: FilePath -> String -> Idris ([String], [String], Delta)
2564+parseImports fname input
2565+ = do i <- getIState
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], Delta), IState)
2572+ imports = do whiteSpace
2573+ mname <- moduleHeader
2577+ return ((mname, ps, mrk), i)
2580+-- | A program is a list of declarations, possibly with associated
2581+-- documentation strings.
2582+parseProg :: SyntaxInfo -> FilePath -> String -> Delta ->
2584+parseProg syn fname input mrk
2585+ = do i <- getIState
2586+ case parseString (evalStateT mainProg i) (Directed (UTF8.fromString fname) 0 0 0 0) input of
2587+ Failure doc -> do iputStrLn (show doc)
2588+ -- FIXME: Get error location from trifecta
2589+ --let errl = sourceLine (errorPos err)
2591+ putIState (i { errLine = Just 0 }) -- Just errl })
2593+ Success (x, i) -> do putIState i
2595+ where mainProg :: IdrisParser ([PDecl], IState)
2596+ mainProg = do release mrk
2601+-- | Collect 'PClauses' with the same function name
2602+collect :: [PDecl] -> [PDecl]
2603+collect (c@(PClauses _ o _ _) : ds)
2604+ = clauses (cname c) [] (c : ds)
2605+ where clauses :: Maybe Name -> [PClause] -> [PDecl] -> [PDecl]
2606+ clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)
2607+ | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds
2608+ clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds)
2609+ | n == n' = clauses j (PWith fc' n' l ws r (collect w) : acc) ds
2610+ clauses (Just n) acc xs = PClauses (fcOf c) o n (reverse acc) : collect xs
2611+ clauses Nothing acc (x:xs) = collect xs
2612+ clauses Nothing acc [] = []
2614+ cname :: PDecl -> Maybe Name
2615+ cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n
2616+ cname (PClauses fc _ _ [PWith _ n _ _ _ _]) = Just n
2617+ cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing
2618+ cname (PClauses fc _ _ [PWithR _ _ _ _]) = Nothing
2619+ fcOf :: PDecl -> FC
2620+ fcOf (PClauses fc _ _ _) = fc
2621+collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
2622+collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds
2623+collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds
2624+collect (PClass doc f s cs n ps ds : ds')
2625+ = PClass doc f s cs n ps (collect ds) : collect ds'
2626+collect (PInstance f s cs n ps t en ds : ds')
2627+ = PInstance f s cs n ps t en (collect ds) : collect ds'
2628+collect (d : ds) = d : collect ds
2631+{- | Load idris module -}
2632+loadModule :: FilePath -> Idris String
2634+ = idrisCatch (do i <- getIState
2635+ let file = takeWhile (/= ' ') f
2636+ ibcsd <- valIBCSubDir i
2637+ ids <- allImportDirs
2638+ fp <- liftIO $ findImport ids ibcsd file
2639+ if file `elem` imported i
2640+ then iLOG $ "Already read " ++ file
2641+ else do putIState (i { imported = file : imported i })
2643+ IDR fn -> loadSource False fn
2644+ LIDR fn -> loadSource True fn
2646+ idrisCatch (loadIBC fn)
2647+ (\c -> do iLOG $ fn ++ " failed " ++ show c
2649+ IDR sfn -> loadSource False sfn
2650+ LIDR sfn -> loadSource True sfn)
2651+ let (dir, fh) = splitFileName file
2652+ return (dropExtension fh))
2653+ (\e -> do let msg = show e
2654+ setErrLine (getErrLine msg)
2658+{- | Load idris code from file -}
2659+loadFromIFile :: IFileType -> Idris ()
2660+loadFromIFile i@(IBC fn src)
2661+ = do iLOG $ "Skipping " ++ getSrcFile i
2662+ idrisCatch (loadIBC fn)
2663+ (\c -> do fail $ fn ++ " failed " ++ show c)
2665+ getSrcFile (IDR fn) = fn
2666+ getSrcFile (LIDR fn) = fn
2667+ getSrcFile (IBC f src) = getSrcFile src
2669+loadFromIFile (IDR fn) = loadSource' False fn
2670+loadFromIFile (LIDR fn) = loadSource' True fn
2672+{-| Load idris source code and show error if something wrong happens -}
2673+loadSource' :: Bool -> FilePath -> Idris ()
2675+ = idrisCatch (loadSource lidr r)
2676+ (\e -> do let msg = show e
2677+ setErrLine (getErrLine msg)
2680+{- | Load Idris source code-}
2681+loadSource :: Bool -> FilePath -> Idris ()
2683+ = do iLOG ("Reading " ++ f)
2685+ let def_total = default_total i
2686+ file_in <- liftIO $ readFile f
2687+ file <- if lidr then tclift $ unlit f file_in else return file_in
2688+ (mname, modules, pos) <- parseImports f file
2690+ putIState (i { default_access = Hidden })
2691+ clearIBC -- start a new .ibc file
2692+ mapM_ (addIBC . IBCImport) modules
2693+ ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
2695+ unless (null ds') $ do
2696+ let ds = namespaces mname ds'
2697+ logLvl 3 (dumpDecls ds)
2699+ logLvl 10 (show (toAlist (idris_implicits i)))
2700+ logLvl 3 (show (idris_infixes i))
2701+ -- Now add all the declarations to the context
2703+ when v $ iputStrLn $ "Type checking " ++ f
2704+ -- we totality check after every Mutual block, so if
2705+ -- anything is a single definition, wrap it in a
2706+ -- mutual block on its own
2707+ elabDecls toplevel (map toMutual ds)
2709+ -- simplify every definition do give the totality checker
2711+ mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
2712+ updateContext (simplifyCasedef n))
2713+ (map snd (idris_totcheck i))
2714+ -- build size change graph from simplified definitions
2715+ iLOG "Totality checking"
2717+ mapM_ buildSCG (idris_totcheck i)
2718+ mapM_ checkDeclTotality (idris_totcheck i)
2719+ iLOG ("Finished " ++ f)
2720+ ibcsd <- valIBCSubDir i
2721+ iLOG "Universe checking"
2723+ let ibc = ibcPathNoFallback ibcsd f
2725+ addHides (hide_list i)
2728+ idrisCatch (do writeIBC f ibc; clearIBC)
2729+ (\c -> return ()) -- failure is harmless
2731+ putIState (i { default_total = def_total,
2736+ namespaces :: [String] -> [PDecl] -> [PDecl]
2737+ namespaces [] ds = ds
2738+ namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
2740+ toMutual :: PDecl -> PDecl
2741+ toMutual m@(PMutual _ d) = m
2742+ toMutual x = let r = PMutual (FC "single mutual" 0) [x] in
2744+ PClauses _ _ _ _ -> r
2745+ PClass _ _ _ _ _ _ _ -> r
2746+ PInstance _ _ _ _ _ _ _ _ -> r
2749+{- | Adds names to hide list -}
2750+addHides :: [(Name, Maybe Accessibility)] -> Idris ()
2751+addHides xs = do i <- getIState
2752+ let defh = default_access i
2753+ let (hs, as) = partition isNothing xs
2756+ (map (\ (n, _) -> (n, defh)) hs ++
2757+ map (\ (n, Just a) -> (n, a)) as)
2758+ where isNothing (_, Nothing) = True
2759+ isNothing _ = False
2761+ doHide (n, a) = do setAccessibility n a
2762+ addIBC (IBCAccess n a)