@@ -1,13 +1,22 @@
1−{-# LANGUAGE PatternGuards, ScopedTypeVariables #-}
2−-- | Parse the full Idris language.
1+{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
32module Idris.Parser where
43
4+import Prelude hiding (pi)
5+
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
13+
514import Idris.AbsSyntax
615import Idris.DSL
716import Idris.Imports
817import Idris.Error
918import Idris.ElabDecls
10−import Idris.ElabTerm
19+import Idris.ElabTerm hiding (namespace, params)
1120import Idris.Coverage
1221import Idris.IBC
1322import Idris.Unlit
@@ -16,443 +25,614 @@ import Paths_idris
1625
1726import Util.DynamicLinker
1827
19−import Core.CoreParser
2028import Core.TT
2129import Core.Evaluate
2230
23−import Text.Parsec
24−import Text.Parsec.Error
25−import Text.Parsec.Expr
26−import Text.Parsec.Language
27−import Text.Parsec.String
28−import qualified Text.Parsec.Token as PTok
31+import Control.Applicative
32+import Control.Monad
33+import Control.Monad.State.Strict
2934
35+import Data.Maybe
36+import qualified Data.List.Split as Spl
3037import Data.List
31−import Data.List.Split(splitOn)
32−import Control.Monad.State
33−import Control.Monad.Error
38+import Data.Monoid
39+import Data.Char
40+import qualified Data.HashSet as HS
41+import qualified Data.Text as T
42+import qualified Data.ByteString.UTF8 as UTF8
43+
3444import Debug.Trace
35−import Data.Maybe
45+
3646import System.FilePath
47+{-
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
55+-}
56+
57+
58+-- | Idris parser with state used during parsing
59+type IdrisParser = StateT IState Parser
60+
61+-- | Generalized monadic parsing constraint type
62+type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)
63+
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
68+
69+-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)
70+simpleWhiteSpace :: MonadicParsing m => m ()
71+simpleWhiteSpace = satisfy isSpace *> pure ()
72+
73+-- | Checks if a charcter is end of line
74+isEol :: Char -> Bool
75+isEol '\n' = True
76+isEol '\0' = True -- Check eof too
77+isEol _ = False
78+
79+-- | Checks if a character is a documentation comment marker
80+isDocCommentMarker :: Char -> Bool
81+isDocCommentMarker '|' = True
82+isDocCommentMarker '^' = True
83+isDocCommentMarker _ = False
84+
85+{- | Consumes a single-line comment
86+ SingleLineComment_t ::= '--' EOL_t
87+ | '--' ~DocCommentMarker_t ~EOL_t* EOL_t
88+ ;
89+ -}
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"
94+
95+{- | Consumes a multi-line comment
96+ MultiLineComment_t ::=
97+ '{ -- }'
98+ | '{ -' ~DocCommentMarker_t InCommentChars_t
99+ ;
100+
101+ InCommentChars_t ::=
102+ '- }'
103+ | MultiLineComment_t InCommentChars_t
104+ | ~'- }'+ InCommentChars_t
105+ ;
106+ -}
107+
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"
118+ startEnd :: String
119+ startEnd = "{}-"
120+
121+{-| Parses a documentation comment (similar to haddoc) given a marker character
122+ DocComment_t ::= '--' DocCommentMarker_t ~EOL_t* EOL_t
123+ | '{ -' DocCommentMarket_t ~'- }'* '- }'
124+ ;
125+ -}
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"
133+
134+-- | Consumes whitespace (and comments)
135+whiteSpace :: MonadicParsing m => m ()
136+whiteSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
137+
138+-- | Parses a string literal
139+stringLiteral :: MonadicParsing m => m String
140+stringLiteral = lexeme $ Tok.stringLiteral
141+
142+-- | Parses a char literal
143+charLiteral :: MonadicParsing m => m Char
144+charLiteral = lexeme $ Tok.charLiteral
145+
146+-- | Parses a natural number
147+natural :: MonadicParsing m => m Integer
148+natural = lexeme $ Tok.natural
149+
150+-- | Parses an integral number
151+integer :: MonadicParsing m => m Integer
152+integer = lexeme $ Tok.integer
153+
154+-- | Parses a floating point number
155+float :: MonadicParsing m => m Double
156+float = lexeme $ Tok.double
157+
158+{- * Symbols, identifiers, names and operators -}
159+
160+
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",
174+ "quoteGoal",
175+ "Int", "Integer", "Float", "Char", "String", "Ptr",
176+ "Bits8", "Bits16", "Bits32", "Bits64",
177+ "Bits8x16", "Bits16x8", "Bits32x4", "Bits64x2"]
178+
179+char :: MonadicParsing m => Char -> m Char
180+char = Chr.char
181+
182+string :: MonadicParsing m => String -> m String
183+string = Chr.string
184+
185+-- | Parses a character as a lexeme
186+lchar :: MonadicParsing m => Char -> m Char
187+lchar = lexeme . char
188+
189+-- | Parses string as a lexeme
190+symbol :: MonadicParsing m => String -> m String
191+symbol = lexeme . Tok.symbol
192+
193+-- | Parses a reserved identifier
194+reserved :: MonadicParsing m => String -> m ()
195+reserved = lexeme . Tok.reserve idrisStyle
196+
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 $
201+ do string name
202+ notFollowedBy (operatorLetter) <?> ("end of " ++ show name)
203+
204+-- | Parses an identifier as a lexeme
205+identifier :: MonadicParsing m => m String
206+identifier = lexeme $ Tok.ident idrisStyle
207+
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"
211+
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)]
226+
227+-- | Parses a name
228+name :: IdrisParser Name
229+name = do i <- get
230+ iName (syntax_keywords i)
231+ <?> "name"
232+
233+
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
236+ condition.
237+-}
238+initsEndAt :: (a -> Bool) -> [a] -> [[a]]
239+initsEndAt p [] = []
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]
243+
244+
245+{- | Create a `Name' from a pair of strings representing a base name and its
246+ namespace.
247+-}
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
252+ (x, "") -> [x]
253+ (x, '.':y) -> x : parseNS y
254+
255+operatorLetter :: MonadicParsing m => m Char
256+operatorLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
257+
258+-- | Parses an operator
259+operator :: MonadicParsing m => m String
260+operator = lexeme . some $ operatorLetter
261+
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)"
267+
268+{- | Get line number from position -}
269+lineNum :: Delta -> Int
270+lineNum (Lines l _ _ _) = fromIntegral l + 1
271+lineNum (Directed _ l _ _ _) = fromIntegral l + 1
272+
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)
279+
280+{-* Syntax helpers-}
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)
37285
38−type TokenParser a = PTok.TokenParser a
39−
40−type IParser = GenParser Char IState
41−
42−lexer :: TokenParser IState
43−lexer = idrisLexer
44−
45−whiteSpace = PTok.whiteSpace lexer
46−lexeme = PTok.lexeme lexer
47−symbol = PTok.symbol lexer
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
60−lchar = lexeme.char
286+{- |Creates table for fixtiy declarations to build expression parser using
287+ pre-build and user-defined operator/fixity declarations -}
288+table :: [FixDecl] -> OperatorTable IdrisParser PTerm
289+table fixes
290+ = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
291+ [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]
292+ ++ toTable (reverse fixes) ++
293+ [[backtick],
294+ [binary "=" PEq AssocLeft],
295+ [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
61296
62−fixErrorMsg :: String -> [String] -> String
63−fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)
297+{- |Calculates table for fixtiy declarations -}
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])
303+ toBin (Fix f op)
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
64308
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
312+ reservedOp name
313+ doc <- option "" (docComment '^')
314+ return (f fc))
66315
67−loadModule :: FilePath -> Idris String
68−loadModule f
69− = idrisCatch (do i <- getIState
70− let file = takeWhile (/= ' ') f
71− ibcsd <- valIBCSubDir i
72− ids <- allImportDirs
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 })
77− case fp of
78− IDR fn -> loadSource False fn
79− LIDR fn -> loadSource True fn
80− IBC fn src ->
81− idrisCatch (loadIBC fn)
82− (\c -> do iLOG $ fn ++ " failed " ++ show c
83− case src of
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)
90− iputStrLn msg
91− return "")
316+{- |Prefix operator -}
317+prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm
318+prefix name f = Prefix (do reservedOp name
319+ fc <- getFC
320+ return (f fc))
92321
93−loadFromIFile :: IFileType -> Idris ()
94−loadFromIFile i@(IBC fn src)
95− = do iLOG $ "Skipping " ++ getSrcFile i
96− idrisCatch (loadIBC fn)
97− (\c -> do fail $ fn ++ " failed " ++ show c)
98−-- loadFromIFile src)
99− where
100− getSrcFile (IDR fn) = fn
101− getSrcFile (LIDR fn) = fn
102− getSrcFile (IBC f src) = getSrcFile src
322+{- |Backtick operator -}
323+backtick :: Operator IdrisParser PTerm
324+backtick = Infix (do lchar '`'; n <- fnName
325+ lchar '`'
326+ fc <- getFC
327+ return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
103328
104−loadFromIFile (IDR fn) = loadSource' False fn
105−loadFromIFile (LIDR fn) = loadSource' True fn
329+-- | Allow implicit type declarations
330+allowImp :: SyntaxInfo -> SyntaxInfo
331+allowImp syn = syn { implicitAllowed = True }
106332
107−loadSource' lidr r
108− = idrisCatch (loadSource lidr r)
109− (\e -> do let msg = show e
110− setErrLine (getErrLine msg)
111− iputStrLn msg)
333+-- | Disallow implicit type declarations
334+disallowImp :: SyntaxInfo -> SyntaxInfo
335+disallowImp syn = syn { implicitAllowed = False }
112336
113−loadSource :: Bool -> FilePath -> Idris ()
114−loadSource lidr f
115− = do iLOG ("Reading " ++ f)
116− i <- getIState
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
121− i <- getIState
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 })
127− f rest pos
128− unless (null ds') $ do
129− let ds = namespaces mname ds'
130− logLvl 3 (dumpDecls ds)
131− i <- getIState
132− logLvl 10 (show (toAlist (idris_implicits i)))
133− logLvl 3 (show (idris_infixes i))
134− -- Now add all the declarations to the context
135− v <- verbose
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)
141− i <- getIState
142− -- simplify every definition do give the totality checker
143− -- a better chance
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"
149− i <- getIState
150− mapM_ buildSCG (idris_totcheck i)
151− mapM_ checkDeclTotality (idris_totcheck i)
152− iLOG ("Finished " ++ f)
153− ibcsd <- valIBCSubDir i
154− iLOG "Universe checking"
155− iucheck
156− let ibc = ibcPathNoFallback ibcsd f
157− i <- getIState
158− addHides (hide_list i)
159− ok <- noErrors
160− when ok $
161− idrisCatch (do writeIBC f ibc; clearIBC)
162− (\c -> return ()) -- failure is harmless
163− i <- getIState
164− putIState (i { default_total = def_total,
165− hide_list = [] })
166− return ()
167− return ()
168− where
169− namespaces [] ds = ds
170− namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
337+-- | Adds accessibility option for function
338+addAcc :: Name -> Maybe Accessibility -> IdrisParser ()
339+addAcc n a = do i <- get
340+ put (i { hide_list = (n, a) : hide_list i })
171341
172− toMutual m@(PMutual _ d) = m
173− toMutual x = let r = PMutual (FC "single mutual" 0) [x] in
174− case x of
175− PClauses _ _ _ _ -> r
176− PClass _ _ _ _ _ _ _ -> r
177− PInstance _ _ _ _ _ _ _ _ -> r
178− _ -> x
342+{- | Add accessbility option for data declarations
343+ (works for classes too - 'abstract' means the data/class is visible but members not) -}
344+accData :: Maybe Accessibility -> Name -> [Name] -> IdrisParser ()
345+accData (Just Frozen) n ns = do addAcc n (Just Frozen)
346+ mapM_ (\n -> addAcc n (Just Hidden)) ns
347+accData a n ns = do addAcc n a
348+ mapM_ (`addAcc` a) ns
179349
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
184− unless (null as) $
185− mapM_ doHide
186− (map (\ (n, _) -> (n, defh)) hs ++
187− map (\ (n, Just a) -> (n, a)) as)
188− where isNothing (_, Nothing) = True
189− isNothing _ = False
190350
191− doHide (n, a) = do setAccessibility n a
192− addIBC (IBCAccess n a)
351+{- * Error reporting helpers -}
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)
193355
194−parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"
195−parseTac i = runParser (do t <- pTactic defaultSyntax
196− eof
197− return t) i "(proof)"
356+{- * Layout helpers -}
198357
199−parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)
200−parseImports fname input
201− = do i <- getIState
202− case runParser (do whiteSpace
203− mname <- pHeader
204− ps <- many pImport
205− rest <- getInput
206− pos <- getPosition
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
210− -- none anyway)
211− return x
212−
213−pHeader :: IParser [String]
214−pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')
215− return (parseName i))
216− <|> return []
217− where parseName x = case span (/='.') x of
218− (x, "") -> [x]
219− (x, '.':y) -> x : parseName y
358+-- | Push indentation to stack
359+pushIndent :: IdrisParser ()
360+pushIndent = do pos <- position
361+ ist <- get
362+ put (ist { indent_stack = (fromIntegral (column pos) + 1) : indent_stack ist })
220363
221−pushIndent :: IParser ()
222−pushIndent = do pos <- getPosition
223− ist <- getState
224− setState (ist { indent_stack = sourceColumn pos :
225− indent_stack ist })
364+-- | Pops indentation from stack
365+popIndent :: IdrisParser ()
366+popIndent = do ist <- get
367+ let (x : xs) = indent_stack ist
368+ put (ist { indent_stack = xs })
226369
227−lastIndent :: IParser Int
228−lastIndent = do ist <- getState
229− case indent_stack ist of
230− (x : xs) -> return x
231− _ -> return 1
370+-- | Gets current indentation
371+indent :: IdrisParser Int
372+indent = liftM ((+1) . fromIntegral . column) position
232373
233−indent :: IParser Int
234−indent = liftM sourceColumn getPosition
374+-- | Gets last indentation
375+lastIndent :: IdrisParser Int
376+lastIndent = do ist <- get
377+ case indent_stack ist of
378+ (x : xs) -> return x
379+ _ -> return 1
380+
381+-- | Applies parser in an indented position
382+indented :: IdrisParser a -> IdrisParser a
383+indented p = notEndBlock *> p <* keepTerminator
384+
385+-- | Applies parser to get a block (which has possibly indented statements)
386+indentedBlock :: IdrisParser a -> IdrisParser [a]
387+indentedBlock p = do openBlock
388+ pushIndent
389+ res <- many (indented p)
390+ popIndent
391+ closeBlock
392+ return res
393+
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
397+ pushIndent
398+ res <- some (indented p)
399+ popIndent
400+ closeBlock
401+ return res
235402
236−popIndent :: IParser ()
237−popIndent = do ist <- getState
238− let (x : xs) = indent_stack ist
239− setState (ist { indent_stack = xs })
240−
241−openBlock :: IParser ()
242−openBlock = do lchar '{'
243− ist <- getState
244− setState (ist { brace_stack = Nothing : brace_stack ist })
245− <|> do ist <- getState
246− lvl' <- indent
247− -- if we're not indented further, it's an empty block, so
248− -- increment lvl to ensure we get to the end
249− let lvl = case brace_stack ist of
250− Just lvl_old : _ ->
251− if lvl' <= lvl_old then lvl_old+1
252− else lvl'
253− [] -> if lvl' == 1 then 2 else lvl'
254− _ -> lvl'
255− setState (ist { brace_stack = Just lvl : brace_stack ist })
256−
257−closeBlock :: IParser ()
258−closeBlock = do ist <- getState
403+-- | Applies parser to get a block with exactly one (possibly indented) statement
404+indentedBlockS :: IdrisParser a -> IdrisParser a
405+indentedBlockS p = do openBlock
406+ pushIndent
407+ res <- indented p
408+ popIndent
409+ closeBlock
410+ return res
411+
412+
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
417+
418+-- | Parses a start of block
419+openBlock :: IdrisParser ()
420+openBlock = do lchar '{'
421+ ist <- get
422+ put (ist { brace_stack = Nothing : brace_stack ist })
423+ <|> do ist <- get
424+ lvl' <- indent
425+ -- if we're not indented further, it's an empty block, so
426+ -- increment lvl to ensure we get to the end
427+ let lvl = case brace_stack ist of
428+ Just lvl_old : _ ->
429+ if lvl' <= lvl_old then lvl_old+1
430+ else lvl'
431+ [] -> if lvl' == 1 then 2 else lvl'
432+ _ -> lvl'
433+ put (ist { brace_stack = Just lvl : brace_stack ist })
434+ <?> "start of block"
435+
436+-- | Parses an end of block
437+closeBlock :: IdrisParser ()
438+closeBlock = do ist <- get
259439 bs <- case brace_stack ist of
260440 [] -> eof >> return []
261− Nothing : xs -> (lchar '}' >> return xs) <|> (eof >> return [])
441+ Nothing : xs -> lchar '}' >> return xs <?> "end of block"
262442 Just lvl : xs -> (do i <- indent
263− inp <- getInput
264−-- trace (show (take 10 inp, i, lvl)) $
265− if i >= lvl && take 1 inp /= ")"
266− then fail "Not end of block"
267− else return xs) <|> (eof >> return [])
268− setState (ist { brace_stack = bs })
269−
270−pTerminator = do lchar ';'; popIndent
271− <|> do c <- indent; l <- lastIndent
272− if c <= l
273− then popIndent
274− else fail "Not a terminator"
275− <|> do i <- getInput
276− if "}" `isPrefixOf` i || ")" `isPrefixOf` i
277− then popIndent
278− else fail "Not a terminator"
279− <|> lookAhead eof
280−
281−pBarTerminator
282− = do lchar '|'; return ()
283− <|> do c <- indent; l <- lastIndent
284− unless (c <= l) $ fail "Not a terminator"
285− <|> lookAhead eof
286−
287−pKeepTerminator
288− = do lchar ';'; return ()
289− <|> do c <- indent; l <- lastIndent
290− unless (c <= l) $ fail "Not a terminator"
291− <|> do i <- getInput
292− let h = take 1 i
293− unless (h `elem` ["}", ")", "|"]) $ fail "Not a terminator"
294− <|> lookAhead eof
295−
443+ isParen <- lookAheadMatches (char ')')
444+ if i >= lvl && not isParen
445+ then fail "not end of block"
446+ else return xs)
447+ <|> (do notOpenBraces
448+ eof
449+ return [])
450+ put (ist { brace_stack = bs })
451+
452+-- | Parses a terminator
453+terminator :: IdrisParser ()
454+terminator = do lchar ';'; popIndent
455+ <|> do c <- indent; l <- lastIndent
456+ if c <= l then popIndent else fail "not a terminator"
457+ <|> do isParen <- lookAheadMatches (oneOf ")}")
458+ if isParen then popIndent else fail "not a termiantor"
459+ <|> lookAhead eof
460+
461+-- | Parses and keeps a terminator
462+keepTerminator :: IdrisParser ()
463+keepTerminator = do lchar ';'; return ()
464+ <|> do c <- indent; l <- lastIndent
465+ unless (c <= l) $ fail "not a terminator"
466+ <|> do isParen <- lookAheadMatches (oneOf ")}|")
467+ unless isParen $ fail "not a terminator"
468+ <|> lookAhead eof
469+
470+-- | Checks if application expression does not end
471+notEndApp :: IdrisParser ()
296472notEndApp = do c <- indent; l <- lastIndent
297− i <- getInput
298− when (c <= l) $ fail "Terminator"
473+ when (c <= l) (fail "terminator")
299474
300−notEndBlock = do ist <- getState
475+-- | Checks that it is not end of block
476+notEndBlock :: IdrisParser ()
477+notEndBlock = do ist <- get
301478 case brace_stack ist of
302− Just lvl : xs -> do i <- indent
303− inp <- getInput
304− when (i < lvl || ")" `isPrefixOf` inp) $ fail "End of block"
305− _ -> return ()
306−
307−-- | Use Parsec's internal state to construct a source code position
308−pfc :: IParser FC
309−pfc = do s <- getPosition
310− let (dir, file) = splitFileName (sourceName s)
311− let f = if dir == addTrailingPathSeparator "." then file else sourceName s
312− return $ FC f (sourceLine s)
313−
314−pImport :: IParser String
315−pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')
316− return (toPath f)
317− where toPath n = foldl1' (</>) $ splitOn "." n
318−
319−-- | A program is a list of declarations, possibly with associated
320−-- documentation strings.
321−parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos ->
322− Idris [PDecl]
323−parseProg syn fname input pos
324− = do i <- getIState
325− case runParser (do setPosition pos
326− whiteSpace
327− ps <- many (pDecl syn)
328− eof
329− i' <- getState
330− return (concat ps, i')) i fname input of
331− Left err -> do iputStrLn (show err)
332− let errl = sourceLine (errorPos err)
333− i <- getIState
334− putIState (i { errLine = Just errl })
335− return []
336− Right (x, i) -> do putIState i
337− return (collect x)
338−
339−-- | Collect 'PClauses' with the same function name
340−collect :: [PDecl] -> [PDecl]
341−collect (c@(PClauses _ o _ _) : ds)
342− = clauses (cname c) [] (c : ds)
343− where clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)
344− | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds
345− clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds)
346− | n == n' = clauses j (PWith fc' n' l ws r (collect w) : acc) ds
347− clauses (Just n) acc xs = PClauses (getfc c) o n (reverse acc) : collect xs
348− clauses Nothing acc (x:xs) = collect xs
349− clauses Nothing acc [] = []
350−
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
356−
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
365−collect [] = []
366−
367−pFullExpr :: SyntaxInfo -> IParser PTerm
368−pFullExpr syn
369− = do x <- pExpr syn; eof;
370− i <- getState
371− return $ desugar syn i x
372−
373−-- | Parse a top-level declaration
374−pDecl :: SyntaxInfo -> IParser [PDecl]
375−pDecl syn = do notEndBlock
376− pDeclBody where
377− pDeclBody
378− = do d <- pDecl' syn
379− i <- getState
380− let d' = fmap (desugar syn i) d
381− return [d']
382− <|> pUsing syn
383− <|> pParams syn
384− <|> pMutual syn
385− <|> pNamespace syn
386− <|> pClass syn
387− <|> pInstance syn
388− <|> do d <- pDSL syn; return [d]
389− <|> pDirective syn
390− <|> try (pProvider syn)
391− <|> pTransform syn
392− <|> try (do reserved "import"; fp <- identifier
393− fail "imports must be at the top of file")
394−
395−pFunDecl :: SyntaxInfo -> IParser [PDecl]
396−pFunDecl syn
397− = try (do notEndBlock
398− d <- pFunDecl' syn
399− i <- getState
400− let d' = fmap (desugar syn i) d
401− return [d'])
402−
403−--------- Top Level Declarations ---------
404−
405−pDecl' :: SyntaxInfo -> IParser PDecl
406−pDecl' syn
407− = try pFixity
408− <|> try (pFunDecl' syn)
409− <|> try (pData syn)
410− <|> try (pRecord syn)
411− <|> try (pSyntaxDecl syn)
412−
413−pSyntaxDecl :: SyntaxInfo -> IParser PDecl
414−pSyntaxDecl syn
415− = do s <- pSyntaxRule syn
416− i <- getState
417− let rs = syntax_rules i
418− let ns = syntax_keywords i
419− let ibc = ibc_write i
420− let ks = map show (names s)
421− setState (i { syntax_rules = s : rs,
422− syntax_keywords = ks ++ ns,
423− ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc
424− })
425− fc <- pfc
426− return (PSyntax fc s)
427− where
428− names (Rule syms _ _) = mapMaybe ename syms
429− ename (Keyword n) = Just n
430− ename _ = Nothing
431−
432−pSyntaxRule :: SyntaxInfo -> IParser Syntax
433−pSyntaxRule syn
479+ Just lvl : xs -> do i <- indent
480+ isParen <- lookAheadMatches (char ')')
481+ when (i < lvl || isParen) (fail "end of block")
482+ _ -> return ()
483+
484+notOpenBraces :: IdrisParser ()
485+notOpenBraces = do ist <- get
486+ when (hasNothing $ brace_stack ist) $ fail "end of input"
487+ where hasNothing :: [Maybe a] -> Bool
488+ hasNothing = any isNothing
489+
490+{- * Main grammar -}
491+
492+{- | Parses module definition
493+ ModuleHeader ::= 'module' Identifier_t ';'?;
494+-}
495+moduleHeader :: IdrisParser [String]
496+moduleHeader = try (do reserved "module"
497+ i <- identifier
498+ option ';' (lchar ';')
499+ return (moduleName i))
500+ <|> return []
501+ where moduleName x = case span (/='.') x of
502+ (x, "") -> [x]
503+ (x, '.':y) -> x : moduleName y
504+
505+{- | Parses an import statement
506+ Import ::= 'import' Identifier_t ';'?;
507+ -}
508+import_ :: IdrisParser String
509+import_ = do reserved "import"
510+ id <- identifier
511+ option ';' (lchar ';')
512+ return (toPath id)
513+ <?> "import statement"
514+ where toPath f = foldl1' (</>) (Spl.splitOn "." f)
515+
516+{- | Parses program source
517+ Prog ::= Decl* EOF;
518+ -}
519+prog :: SyntaxInfo -> IdrisParser [PDecl]
520+prog syn = do whiteSpace
521+ decls <- many (decl syn)
522+ notOpenBraces
523+ eof
524+ let c = (concat decls)
525+ return c
526+
527+{- | Parses a top-level declaration
528+Decl ::=
529+ Decl'
530+ | Using
531+ | Params
532+ | Mutual
533+ | Namespace
534+ | Class
535+ | Instance
536+ | DSL
537+ | Directive
538+ | Provider
539+ | Transform
540+ | Import!
541+ ;
542+-}
543+decl :: SyntaxInfo -> IdrisParser [PDecl]
544+decl syn = do notEndBlock
545+ declBody
546+ where declBody :: IdrisParser [PDecl]
547+ declBody = declBody'
548+ <|> using_ syn
549+ <|> params syn
550+ <|> mutual syn
551+ <|> namespace syn
552+ <|> class_ syn
553+ <|> instance_ syn
554+ <|> do d <- dsl syn; return [d]
555+ <|> directive syn
556+ <|> try(provider syn)
557+ <|> transform syn
558+ <|> try(do import_; fail "imports must be at top of file")
559+ <?> "declaration"
560+ declBody' :: IdrisParser [PDecl]
561+ declBody' = do d <- decl' syn
562+ i <- get
563+ let d' = fmap (desugar syn i) d
564+ return [d']
565+
566+{- | Parses a top-level declaration with possible syntax sugar
567+Decl' ::=
568+ Fixity
569+ | FunDecl'
570+ | Data
571+ | Record
572+ | SyntaxDecl
573+ ;
574+-}
575+decl' :: SyntaxInfo -> IdrisParser PDecl
576+decl' syn = try fixity
577+ <|> try (fnDecl' syn)
578+ <|> try (data_ syn)
579+ <|> try (record syn)
580+ <|> try (syntaxDecl syn)
581+ <?> "declaration"
582+
583+{- | Parses a syntax extension declaration (and adds the rule to parser state)
584+ SyntaxDecl ::= SyntaxRule;
585+-}
586+syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
587+syntaxDecl syn = do s <- syntaxRule syn
588+ i <- get
589+ let rs = syntax_rules i
590+ let ns = syntax_keywords i
591+ let ibc = ibc_write i
592+ let ks = map show (names s)
593+ put (i { syntax_rules = s : rs,
594+ syntax_keywords = ks ++ ns,
595+ ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc })
596+ fc <- getFC
597+ return (PSyntax fc s)
598+ where names (Rule syms _ _) = mapMaybe ename syms
599+ ename (Keyword n) = Just n
600+ ename _ = Nothing
601+
602+{- | Parses a syntax extension declaration
603+SyntaxRuleOpts ::= 'term' | 'pattern';
604+
605+SyntaxRule ::=
606+ SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
607+
608+SyntaxSym ::= '[' Name_t ']'
609+ | '{' Name_t '}'
610+ | Name_t
611+ | StringLiteral_t
612+ ;
613+-}
614+syntaxRule :: SyntaxInfo -> IdrisParser Syntax
615+syntaxRule syn
434616 = do pushIndent
435617 sty <- option AnySyntax (do reserved "term"; return TermSyntax
436618 <|> do reserved "pattern"; return PatternSyntax)
437619 reserved "syntax"
438− syms <- many1 pSynSym
439− when (all expr syms) $ fail "No keywords in syntax rule"
440− let ns = mapMaybe name syms
441− when (length ns /= length (nub ns))
442− $ fail "Repeated variable in syntax rule"
620+ syms <- some syntaxSym
621+ when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
622+ let ns = mapMaybe getName syms
623+ when (length ns /= length (nub ns))
624+ $ unexpected "repeated variable in syntax rule"
443625 lchar '='
444− tm <- pTExpr (impOK syn)
445− pTerminator
626+ tm <- typeExpr (allowImp syn)
627+ terminator
446628 return (Rule (mkSimple syms) tm sty)
447629 where
448− expr (Expr _) = True
449− expr _ = False
450− name (Expr n) = Just n
451− name _ = Nothing
452−
630+ isExpr (Expr _) = True
631+ isExpr _ = False
632+ getName (Expr n) = Just n
633+ getName _ = Nothing
453634 -- Can't parse two full expressions (i.e. expressions with application) in a row
454635 -- so change them both to a simple expression
455−
456636 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
457637 mkSimple xs = mkSimple' xs
458638
@@ -461,115 +641,247 @@ pSyntaxRule syn
461641 mkSimple' (e : es) = e : mkSimple' es
462642 mkSimple' [] = []
463643
464−pSynSym :: IParser SSymbol
465−pSynSym = try (do lchar '['; n <- pName; lchar ']'
466− return (Expr n))
467− <|> try (do lchar '{'; n <- pName; lchar '}'
468− return (Binding n))
469− <|> do n <- iName []
470− return (Keyword n)
471− <|> do sym <- strlit
472− return (Symbol sym)
473−
474−pFunDecl' :: SyntaxInfo -> IParser PDecl
475−pFunDecl' syn = try (do doc <- option "" (pDocComment '|')
476− pushIndent
477− ist <- getState
478− let initOpts = if default_total ist
479− then [TotalFn]
480− else []
481− opts <- pFnOpts initOpts
482− acc <- pAccessibility
483− opts' <- pFnOpts opts
484− n_in <- pfName
485− let n = expandNS syn n_in
486− fc <- pfc
487− ty <- pTSig (impOK syn)
488− pTerminator
489−-- ty' <- implicit syn n ty
490− addAcc n acc
491− return (PTy doc syn fc opts' n ty))
492− <|> try (pPostulate syn)
493− <|> try (pPattern syn)
494− <|> try (pCAF syn)
495−
496−pPostulate :: SyntaxInfo -> IParser PDecl
497−pPostulate syn = do doc <- option "" (pDocComment '|')
498− pushIndent
499− reserved "postulate"
500− ist <- getState
501− let initOpts = if default_total ist
502− then [TotalFn]
503− else []
504− opts <- pFnOpts initOpts
505− acc <- pAccessibility
506− opts' <- pFnOpts opts
507− n_in <- pfName
508− let n = expandNS syn n_in
509− ty <- pTSig (impOK syn)
510− fc <- pfc
511− pTerminator
512− addAcc n acc
513− return (PPostulate doc syn fc opts' n ty)
514−
515−
516−pUsing :: SyntaxInfo -> IParser [PDecl]
517−pUsing syn =
644+
645+{- | Parses a syntax symbol (either binding variable, keyword or expression)
646+SyntaxSym ::= '[' Name_t ']'
647+ | '{' Name_t '}'
648+ | Name_t
649+ | StringLiteral_t
650+ ;
651+ -}
652+syntaxSym :: IdrisParser SSymbol
653+syntaxSym = try (do lchar '['; n <- name; lchar ']'
654+ return (Expr n))
655+ <|> try (do lchar '{'; n <- name; lchar '}'
656+ return (Binding n))
657+ <|> do n <- iName []
658+ return (Keyword n)
659+ <|> do sym <- stringLiteral
660+ return (Symbol sym)
661+ <?> "syntax symbol"
662+
663+{- | Parses a function declaration with possible syntax sugar
664+ FunDecl ::= FunDecl';
665+-}
666+fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
667+fnDecl syn
668+ = try (do notEndBlock
669+ d <- fnDecl' syn
670+ i <- get
671+ let d' = fmap (desugar syn i) d
672+ return [d'])
673+ <?> "function declaration"
674+
675+{- Parses a function declaration
676+ FunDecl' ::=
677+ DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
678+ | Postulate
679+ | Pattern
680+ | CAF
681+ ;
682+-}
683+fnDecl' :: SyntaxInfo -> IdrisParser PDecl
684+fnDecl' syn = try (do doc <- option "" (docComment '|')
685+ pushIndent
686+ ist <- get
687+ let initOpts = if default_total ist
688+ then [TotalFn]
689+ else []
690+ opts <- fnOpts initOpts
691+ acc <- optional accessibility
692+ opts' <- fnOpts opts
693+ n_in <- fnName
694+ let n = expandNS syn n_in
695+ fc <- getFC
696+ ty <- typeSig (allowImp syn)
697+ terminator
698+ addAcc n acc
699+ return (PTy doc syn fc opts' n ty))
700+ <|> try (postulate syn)
701+ <|> try (pattern syn)
702+ <|> try (caf syn)
703+ <?> "function declaration"
704+
705+
706+{- Parses function options given initial options
707+FnOpts ::= 'total'
708+ | 'partial'
709+ | 'implicit'
710+ | '%' 'assert_total'
711+ | '%' 'reflection'
712+ | '%' 'specialise' '[' NameTimesList? ']'
713+ ;
714+
715+NameTimes ::= FnName Natural?;
716+
717+NameTimesList ::=
718+ NameTimes
719+ | NameTimes ',' NameTimesList
720+ ;
721+
722+-}
723+-- FIXME: Check compatability for function options (i.e. partal/total)
724+fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
725+fnOpts opts
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)
738+ <|> return 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)))
744+ return (n, t)
745+
746+{- | Parses an operator in function position i.e. enclosed by `()', with an
747+ optional namespace
748+
749+ OperatorFront ::= (Identifier_t '.')? '(' Operator_t ')';
750+-}
751+operatorFront :: IdrisParser Name
752+operatorFront = maybeWithNS (lchar '(' *> operator <* lchar ')') False []
753+
754+{- | Parses a function (either normal name or operator)
755+ FnName ::= Name | OperatorFront;
756+-}
757+fnName :: IdrisParser Name
758+fnName = try operatorFront <|> name <?> "function name"
759+
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"
766+
767+
768+
769+{- | Parses a postulate
770+
771+Postulate ::=
772+ DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
773+ ;
774+-}
775+postulate :: SyntaxInfo -> IdrisParser PDecl
776+postulate syn = do doc <- option "" (docComment '|')
777+ pushIndent
778+ reserved "postulate"
779+ ist <- get
780+ let initOpts = if default_total ist
781+ then [TotalFn]
782+ else []
783+ opts <- fnOpts initOpts
784+ acc <- optional accessibility
785+ opts' <- fnOpts opts
786+ n_in <- fnName
787+ let n = expandNS syn n_in
788+ ty <- typeSig (allowImp syn)
789+ fc <- getFC
790+ terminator
791+ addAcc n acc
792+ return (PPostulate doc syn fc opts' n ty)
793+ <?> "postulate"
794+
795+{- | Parses a using declaration
796+
797+Using ::=
798+ 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
799+ ;
800+ -}
801+using_ :: SyntaxInfo -> IdrisParser [PDecl]
802+using_ syn =
518803 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
519804 openBlock
520805 let uvars = using syn
521− ds <- many1 (pDecl (syn { using = uvars ++ ns }))
806+ ds <- many (decl (syn { using = uvars ++ ns }))
522807 closeBlock
523808 return (concat ds)
809+ <?> "using declaration"
810+
811+{- | Parses a parameters declaration
524812
525−pParams :: SyntaxInfo -> IParser [PDecl]
526−pParams syn =
527− do reserved "parameters"; lchar '('; ns <- tyDeclList syn; lchar ')'
528− openBlock
813+Params ::=
814+ 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
815+ ;
816+ -}
817+params :: SyntaxInfo -> IdrisParser [PDecl]
818+params syn =
819+ do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
820+ openBlock
529821 let pvars = syn_params syn
530− ds <- many1 (pDecl syn { syn_params = pvars ++ ns })
531− closeBlock
532− fc <- pfc
822+ ds <- many (decl syn { syn_params = pvars ++ ns })
823+ closeBlock
824+ fc <- getFC
533825 return [PParams fc ns (concat ds)]
826+ <?> "parameters declaration"
534827
535−pMutual :: SyntaxInfo -> IParser [PDecl]
536−pMutual syn =
828+{- | Parses a mutual declaration (for mutually recursive functions)
829+
830+Mutual ::=
831+ 'mutual' OpenBlock Decl* CloseBlock
832+ ;
833+-}
834+mutual :: SyntaxInfo -> IdrisParser [PDecl]
835+mutual syn =
537836 do reserved "mutual"
538− openBlock
837+ openBlock
539838 let pvars = syn_params syn
540− ds <- many1 (pDecl syn)
541− closeBlock
542− fc <- pfc
839+ ds <- many (decl syn)
840+ closeBlock
841+ fc <- getFC
543842 return [PMutual fc (concat ds)]
843+ <?> "mutual block"
544844
545−pNamespace :: SyntaxInfo -> IParser [PDecl]
546−pNamespace syn =
845+{- | Parses a namespace declaration
846+
847+Namespace ::=
848+ 'namespace' identifier OpenBlock Decl+ CloseBlock
849+ ;
850+-}
851+namespace :: SyntaxInfo -> IdrisParser [PDecl]
852+namespace syn =
547853 do reserved "namespace"; n <- identifier;
548− openBlock
549− ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
854+ openBlock
855+ ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
550856 closeBlock
551− return [PNamespace n (concat ds)]
552−
553−--------- Fixity ---------
554−
555−pFixity :: IParser PDecl
556−pFixity = do pushIndent
557− f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
558− pTerminator
559− let prec = fromInteger i
560− istate <- getState
561− let infixes = idris_infixes istate
562− let fs = map (Fix (f prec)) ops
563− let redecls = map (alreadyDeclared infixes) fs
564− let ill = filter (not . checkValidity) redecls
565− if null ill
566− then do setState (istate { idris_infixes = nub $ sort (fs ++ infixes)
567− , ibc_write = map IBCFix fs ++ ibc_write istate
568− })
569− fc <- pfc
570− return (PFix fc (f prec) ops)
571− else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
857+ return [PNamespace n (concat ds)]
858+ <?> "namespace declaration"
859+
860+{- | Parses a fixity declaration
861+
862+Fixity ::=
863+ FixityType Natural_t OperatorList Terminator
864+ ;
865+-}
866+fixity :: IdrisParser PDecl
867+fixity = do pushIndent
868+ f <- fixityType; i <- natural; ops <- sepBy1 operator (lchar ',')
869+ terminator
870+ let prec = fromInteger i
871+ istate <- get
872+ let infixes = idris_infixes istate
873+ let fs = map (Fix (f prec)) ops
874+ let redecls = map (alreadyDeclared infixes) fs
875+ let ill = filter (not . checkValidity) redecls
876+ if null ill
877+ then do put (istate { idris_infixes = nub $ sort (fs ++ infixes)
878+ , ibc_write = map IBCFix fs ++ ibc_write istate
879+ })
880+ fc <- getFC
881+ return (PFix fc (f prec) ops)
882+ else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
572883 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
884+ <?> "fixity declaration"
573885 where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
574886 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
575887
@@ -579,287 +891,366 @@ pFixity = do pushIndent
579891 extractName :: FixDecl -> String
580892 extractName (Fix _ n) = n
581893
582−fixity :: IParser (Int -> Fixity)
583−fixity = try (do reserved "infixl"; return Infixl)
584− <|> try (do reserved "infixr"; return Infixr)
585− <|> try (do reserved "infix"; return InfixN)
586− <|> try (do reserved "prefix"; return PrefixN)
587−
588−--------- Type classes ---------
589−
590−pClass :: SyntaxInfo -> IParser [PDecl]
591−pClass syn = do doc <- option "" (pDocComment '|')
592− acc <- pAccessibility
593− reserved "class"; fc <- pfc; cons <- pConstList syn; n_in <- pName
894+{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)
895+FixityType ::=
896+ 'infixl'
897+ | 'infixr'
898+ | 'infix'
899+ | 'prefix'
900+ ;
901+ -}
902+fixityType :: IdrisParser (Int -> Fixity)
903+fixityType = try (do reserved "infixl"; return Infixl)
904+ <|> try (do reserved "infixr"; return Infixr)
905+ <|> try (do reserved "infix"; return InfixN)
906+ <|> try (do reserved "prefix"; return PrefixN)
907+ <?> "fixity type"
908+
909+{- |Parses a methods block (for type classes and instances)
910+ MethodsBlock ::= 'where' OpenBlock FnDecl* CloseBlock
911+ -}
912+methodsBlock :: SyntaxInfo -> IdrisParser [PDecl]
913+methodsBlock syn = do reserved "where"
914+ openBlock
915+ ds <- many (fnDecl syn)
916+ closeBlock
917+ return (concat ds)
918+ <?> "methods block"
919+
920+{- |Parses a type class declaration
921+
922+ClassArgument ::=
923+ Name
924+ | '(' Name ':' Expr ')'
925+ ;
926+
927+Class ::=
928+ DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* MethodsBlock?
929+ ;
930+-}
931+class_ :: SyntaxInfo -> IdrisParser [PDecl]
932+class_ syn = do doc <- option "" (docComment '|')
933+ acc <- optional accessibility
934+ reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- name
594935 let n = expandNS syn n_in
595936 cs <- many carg
596− reserved "where"; openBlock
597− ds <- many $ pFunDecl syn
598− closeBlock
599− let allDs = concat ds
600− accData acc n (concatMap declared allDs)
601− return [PClass doc syn fc cons n cs allDs]
937+ ds <- option [] (methodsBlock syn)
938+ accData acc n (concatMap declared ds)
939+ return [PClass doc syn fc cons n cs ds]
940+ <?> "type-class declaration"
602941 where
603− carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'
942+ carg :: IdrisParser (Name, PTerm)
943+ carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
604944 return (i, ty)
605− <|> do i <- pName;
945+ <|> do i <- name;
606946 return (i, PType)
607947
608−pInstance :: SyntaxInfo -> IParser [PDecl]
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
613− return (Just n))
614− cs <- pConstList syn
615− cn <- pName
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
621− closeBlock
622− return [PInstance syn fc cs cn args t en (concat ds)]
623−
624−--------- Expressions ---------
625−
626−pExpr syn = do i <- getState
627− buildExpressionParser (table (idris_infixes i)) (pExpr' syn)
628−
629−pExpr' :: SyntaxInfo -> IParser PTerm
630−pExpr' syn
631− = try (pExtExpr syn)
632− <|> pNoExtExpr syn
948+{- |Parses a type class instance declaration
633949
634−pExtExpr :: SyntaxInfo -> IParser PTerm
635−pExtExpr syn = do i <- getState
636− pExtensions syn (syntax_rules i)
950+ Instance ::=
951+ 'instance' InstanceName? ConstraintList? Name SimpleExpr* MethodsBlock?
952+ ;
637953
638−pSimpleExtExpr :: SyntaxInfo -> IParser PTerm
639−pSimpleExtExpr syn = do i <- getState
640− pExtensions syn (filter simple (syntax_rules i))
954+ InstanceName ::= '[' Name ']';
955+-}
956+instance_ :: SyntaxInfo -> IdrisParser [PDecl]
957+instance_ syn = do reserved "instance"; fc <- getFC
958+ en <- optional instanceName
959+ cs <- constraintList syn
960+ cn <- name
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
970+ return n
971+ <?> "instance name"
972+
973+
974+{- | Parses an expression as a whole
975+ FullExpr ::= Expr EOF_t;
976+ -}
977+fullExpr :: SyntaxInfo -> IdrisParser PTerm
978+fullExpr syn = do x <- expr syn
979+ eof
980+ i <- get
981+ return $ desugar syn i x
982+
983+
984+{- |Parses an expression
985+ Expr ::= Expr';
986+-}
987+expr :: SyntaxInfo -> IdrisParser PTerm
988+expr syn = do i <- get
989+ buildExpressionParser (table (idris_infixes i)) (expr' syn)
990+
991+{- | Parses either an internally defined expression or
992+ a user-defined one
993+
994+Expr' ::= "External (User-defined) Syntax"
995+ | InternalExpr;
996+
997+ -}
998+expr' :: SyntaxInfo -> IdrisParser PTerm
999+expr' syn = try (externalExpr syn)
1000+ <|> internalExpr syn
1001+ <?> "expression"
1002+
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"
1008+
1009+{- | Parses a simple user-defined expression -}
1010+simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm
1011+simpleExternalExpr syn = do i <- get
1012+ extensions syn (filter isSimple (syntax_rules i))
6411013 where
642− simple (Rule (Expr x:xs) _ _) = False
643− simple (Rule (SimpleExpr x:xs) _ _) = False
644− simple (Rule [Keyword _] _ _) = True
645− simple (Rule [Symbol _] _ _) = True
646− simple (Rule (_:xs) _ _) = case last xs of
1014+ isSimple (Rule (Expr x:xs) _ _) = False
1015+ isSimple (Rule (SimpleExpr x:xs) _ _) = False
1016+ isSimple (Rule [Keyword _] _ _) = True
1017+ isSimple (Rule [Symbol _] _ _) = True
1018+ isSimple (Rule (_:xs) _ _) = case last xs of
6471019 Keyword _ -> True
6481020 Symbol _ -> True
6491021 _ -> False
650− simple _ = False
651−
652−pNoExtExpr syn =
653− try (pApp syn)
654− <|> try (pMatchApp syn)
655− <|> try (pUnifyLog syn)
656− <|> pRecordType syn
657− <|> try (pSimpleExpr syn)
658− <|> pLambda syn
659− <|> pQuoteGoal syn
660− <|> pLet syn
661− <|> pRewriteTerm syn
662− <|> pPi syn
663− <|> pDoBlock syn
664−
665−pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
666−pExtensions syn rules = choice (map (try . pExt syn) (filter valid rules))
1022+ isSimple _ = False
1023+
1024+{- | Tries to parse a user-defined expression given a list of syntactic extensions -}
1025+extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm
1026+extensions syn rules = choice (map (try . extension syn) (filter isValid rules))
1027+ <?> "user-defined expression"
6671028 where
668− valid (Rule _ _ AnySyntax) = True
669− valid (Rule _ _ PatternSyntax) = inPattern syn
670− valid (Rule _ _ TermSyntax) = not (inPattern syn)
1029+ isValid :: Syntax -> Bool
1030+ isValid (Rule _ _ AnySyntax) = True
1031+ isValid (Rule _ _ PatternSyntax) = inPattern syn
1032+ isValid (Rule _ _ TermSyntax) = not (inPattern syn)
6711033
6721034
6731035data SynMatch = SynTm PTerm | SynBind Name
6741036
675−pExt :: SyntaxInfo -> Syntax -> IParser PTerm
676−pExt syn (Rule ssym ptm _)
677− = do smap <- mapM pSymbol ssym
1037+{- | Tries to parse an expression given a user-defined rule -}
1038+extension :: SyntaxInfo -> Syntax -> IdrisParser PTerm
1039+extension syn (Rule ssym ptm _)
1040+ = do smap <- mapM extensionSymbol ssym
6781041 let ns = mapMaybe id smap
6791042 return (update ns ptm) -- updated with smap
6801043 where
681− pSymbol (Keyword n) = do reserved (show n); return Nothing
682− pSymbol (Expr n) = do tm <- pExpr syn
683− return $ Just (n, SynTm tm)
684− pSymbol (SimpleExpr n) = do tm <- pSimpleExpr syn
685− return $ Just (n, SynTm tm)
686− pSymbol (Binding n) = do b <- pName
687− return $ Just (n, SynBind b)
688− pSymbol (Symbol s) = do symbol s
689− return Nothing
1044+ extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
1045+ extensionSymbol (Keyword n) = do reserved (show n); return Nothing
1046+ extensionSymbol (Expr n) = do tm <- expr syn
1047+ return $ Just (n, SynTm tm)
1048+ extensionSymbol (SimpleExpr n) = do tm <- simpleExpr syn
1049+ return $ Just (n, SynTm tm)
1050+ extensionSymbol (Binding n) = do b <- name
1051+ return $ Just (n, SynBind b)
1052+ extensionSymbol (Symbol s) = do symbol s
1053+ return Nothing
1054+ dropn :: Name -> [(Name, a)] -> [(Name, a)]
6901055 dropn n [] = []
6911056 dropn n ((x,t) : xs) | n == x = xs
6921057 | otherwise = (x,t):dropn n xs
6931058
1059+ updateB :: [(Name, SynMatch)] -> Name -> Name
6941060 updateB ns n = case lookup n ns of
6951061 Just (SynBind t) -> t
6961062 _ -> n
6971063
1064+ update :: [(Name, SynMatch)] -> PTerm -> PTerm
6981065 update ns (PRef fc n) = case lookup n ns of
6991066 Just (SynTm t) -> t
7001067 _ -> PRef fc n
7011068 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)
7031070 update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)
7041071 (update (dropn n ns) sc)
7051072 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)
7071074 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)
7081075 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)
7091076 update ns (PAlternative a as) = PAlternative a (map (update ns) as)
7101077 update ns (PHidden t) = PHidden (update ns t)
7111078 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
712− where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
1079+ where upd :: [(Name, SynMatch)] -> [PDo] -> [PDo]
1080+ upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
7131081 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)
7151083 : 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)
7171085 : 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)
7191087 : upd ns ds
7201088 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
7211089 update ns t = t
7221090
723−pName = do i <- getState
724− iName (syntax_keywords i)
725− <|> do reserved "instance"
726− i <- getState
727− UN n <- iName (syntax_keywords i)
728− return (UN ('@':n))
729−
730−-- | Parser for an operator in function position, i.e. enclosed by `()', with an
731−-- optional namespace.
732−pOpFront = maybeWithNS pOpFrontNoNS False []
733− where pOpFrontNoNS = do lchar '('; o <- operator; lchar ')'; return o
734−
735−pfName = try pOpFront
736− <|> pName
737−
738−pTotality :: IParser Bool
739−pTotality
740− = do reserved "total"; return True
741− <|> do reserved "partial"; return False
742−
743−pAccessibility' :: IParser Accessibility
744−pAccessibility'
745− = do reserved "public"; return Public
746− <|> do reserved "abstract"; return Frozen
747− <|> do reserved "private"; return Hidden
748−
749−pAccessibility :: IParser (Maybe Accessibility)
750−pAccessibility
751− = do acc <- pAccessibility'; return (Just acc)
752− <|> return Nothing
753−
754−pFnOpts :: [FnOpt] -> IParser [FnOpt]
755−pFnOpts opts
756− = do reserved "total"; pFnOpts (TotalFn : opts)
757− <|> do reserved "partial"; pFnOpts (PartialFn : (opts \\ [TotalFn]))
758− <|> try (do lchar '%'; reserved "export"; c <- strlit;
759− pFnOpts (CExport c : opts))
760− <|> try (do lchar '%'; reserved "assert_total";
761− pFnOpts (AssertTotal : opts))
762− <|> try (do lchar '%'; reserved "reflection";
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)
768− <|> return opts
769− where nameTimes = do n <- pfName
770− t <- option Nothing (do reds <- natural
771− return (Just (fromInteger reds)))
772− return (n, t)
773−
774−addAcc :: Name -> Maybe Accessibility -> IParser ()
775−addAcc n a = do i <- getState
776− setState (i { hide_list = (n, a) : hide_list i })
777−
778−pCaseExpr syn = do
779− reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
780− openBlock
781− pushIndent
782− opts <- many1 (do notEndBlock
783− x <- pCaseOpt syn
784− pKeepTerminator
785− return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
786− popIndent
787− closeBlock
788− return (PCase fc scr opts)
789−
790−pProofExpr syn = do
791− reserved "proof"; lchar '{'
792− ts <- endBy (pTactic syn) (lchar ';')
793− lchar '}'
794− return (PProof ts)
795−
796−pTacticsExpr syn = do
797− reserved "tactics"; lchar '{'
798− ts <- endBy (pTactic syn) (lchar ';')
799− lchar '}'
800− return (PTactics ts)
801−
802−pSimpleExpr syn =
803− try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t)
804− <|> do lchar '?'; x <- pName; return (PMetavar x)
805− <|> do lchar '%'; fc <- pfc; reserved "instance"; return (PResolveTC fc)
806− <|> do reserved "refl"; fc <- pfc;
807− tm <- option Placeholder (do lchar '{'; t <- pExpr syn; lchar '}';
1091+{- |Parses a (normal) built-in expression
1092+
1093+InternalExpr ::=
1094+ App
1095+ | MatchApp
1096+ | UnifyLog
1097+ | RecordType
1098+ | SimpleExpr
1099+ | Lambda
1100+ | QuoteGoal
1101+ | Let
1102+ | RewriteTerm
1103+ | Pi
1104+ | DoBlock
1105+ ;
1106+-}
1107+internalExpr :: SyntaxInfo -> IdrisParser PTerm
1108+internalExpr syn =
1109+ try (app syn)
1110+ <|> try (matchApp syn)
1111+ <|> try (unifyLog syn)
1112+ <|> recordType syn
1113+ <|> try (simpleExpr syn)
1114+ <|> lambda syn
1115+ <|> quoteGoal syn
1116+ <|> let_ syn
1117+ <|> rewriteTerm syn
1118+ <|> pi syn
1119+ <|> doBlock syn
1120+ <?> "expression"
1121+
1122+{- | Parses a case expression
1123+CaseExpr ::=
1124+ 'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;
1125+-}
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"
1132+
1133+{- | Parses a case in a case expression
1134+CaseOption ::=
1135+ Expr '=>' Expr Terminator
1136+ ;
1137+-}
1138+caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
1139+caseOption syn = do lhs <- expr (syn { inPattern = True })
1140+ symbol "=>"; r <- expr syn
1141+ return (lhs, r)
1142+ <?> "case option"
1143+
1144+{- | Parses a proof block
1145+ProofExpr ::=
1146+ 'proof' OpenBlock Tactic'* CloseBlock
1147+ ;
1148+-}
1149+proofExpr :: SyntaxInfo -> IdrisParser PTerm
1150+proofExpr syn = do reserved "proof"
1151+ ts <- indentedBlock (tactic syn)
1152+ return $ PProof ts
1153+ <?> "proof block"
1154+
1155+{- | Parses a tactics block
1156+TacticsExpr :=
1157+ 'tactics' OpenBlock Tactic'* CloseBlock
1158+;
1159+-}
1160+tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
1161+tacticsExpr syn = do reserved "tactics"
1162+ ts <- indentedBlock (tactic syn)
1163+ return $ PTactics ts
1164+ <?> "tactics block"
1165+
1166+{- | Parses a simple expresion
1167+SimpleExpr ::=
1168+ '![' Term ']'
1169+ | '?' Name
1170+ | % 'instance'
1171+ | 'refl' ('{' Expr '}')?
1172+ | ProofExpr
1173+ | TacticsExpr
1174+ | CaseExpr
1175+ | FnName
1176+ | List
1177+ | Comprehension
1178+ | Alt
1179+ | Idiom
1180+ | '(' Bracketed
1181+ | Constant
1182+ | Type
1183+ | '()'
1184+ | '_|_'
1185+ | '_'
1186+ | {- External (User-defined) Simple Expression -}
1187+ ;
1188+-}
1189+simpleExpr :: SyntaxInfo -> IdrisParser PTerm
1190+simpleExpr syn =
1191+ {-try (do symbol "!["; t <- term; lchar ']'; return $ PQuote t)
1192+ <|>-} do lchar '?'; x <- name; return (PMetavar x)
1193+ <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)
1194+ <|> do reserved "refl"; fc <- getFC;
1195+ tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';
8081196 return t)
8091197 return (PRefl fc tm)
810−-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)
811− <|> pProofExpr syn
812− <|> pTacticsExpr syn
813− <|> pCaseExpr syn
814− <|> try (do x <- pfName
815− fc <- pfc
1198+ <|> proofExpr syn
1199+ <|> tacticsExpr syn
1200+ <|> caseExpr syn
1201+ <|> try (do fc <- getFC
1202+ x <- fnName
8161203 return (PRef fc x))
817− <|> try (pList syn)
818− <|> try (pComprehension syn)
819− <|> try (pAlt syn)
820− <|> try (pIdiom syn)
1204+ <|> try (listExpr syn)
1205+ <|> try (comprehension syn)
1206+ <|> try (alt syn)
1207+ <|> try (idiom syn)
8211208 <|> try (do lchar '('
822− bracketed (noImp syn))
823− <|> try (do c <- pConstant
824− fc <- pfc
1209+ bracketed (disallowImp syn))
1210+ <|> try (do c <- constant
1211+ fc <- getFC
8251212 return (modifyConst syn fc (PConstant c)))
8261213 <|> do reserved "Type"; return PType
8271214 <|> try (do symbol "()"
828− fc <- pfc
1215+ fc <- getFC
8291216 return (PTrue fc))
8301217 <|> try (do symbol "_|_"
831− fc <- pfc
1218+ fc <- getFC
8321219 return (PFalse fc))
8331220 <|> do lchar '_'; return Placeholder
834− <|> pSimpleExtExpr syn
835−
1221+ <|> simpleExternalExpr syn
1222+ <?> "expression"
1223+
1224+
1225+{- |Parses the rest of an expression in braces
1226+Bracketed ::=
1227+ | Pair
1228+ | Expr ')'
1229+ | Operator Expr ')'
1230+ | Expr Operator ')'
1231+ ;
1232+-}
1233+bracketed :: SyntaxInfo -> IdrisParser PTerm
8361234bracketed syn =
837− try (pPair syn)
838− <|> try (do e <- pExpr 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 ')'
1235+ try (pair syn)
1236+ <|> try (do e <- expr syn; lchar ')'; return e)
1237+ <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
8431238 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")),
8451240 pexp e]))
846− <|> try (do fc <- pfc; e <- pSimpleExpr syn; o <- operator; lchar ')'
1241+ <|> try (do fc <- getFC; e <- simpleExpr syn; o <- operator; lchar ')'
8471242 return $ PLam (MN 1000 "ARG") Placeholder
8481243 (PApp fc (PRef fc (UN o)) [pexp e,
8491244 pexp (PRef fc (MN 1000 "ARG"))]))
850−
851−pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
852−pCaseOpt syn = do lhs <- pExpr (syn { inPattern = True })
853− symbol "=>"; rhs <- pExpr syn
854− return (lhs, rhs)
1245+ <?> "end of expression in braces"
8551246
8561247-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
8571248-- big integer, otherwise try fromInteger and the constants as alternatives.
8581249-- a better solution would be to fix fromInteger to work with Integer, as the
8591250-- name suggests, rather than Int
860−
1251+{-| Finds optimal type for integer constant -}
8611252modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
862−modifyConst syn fc (PConstant (BI x))
1253+modifyConst syn fc (PConstant (BI x))
8631254 | not (inPattern syn)
8641255 = PAlternative False
8651256 (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI (fromInteger x)))]
@@ -875,351 +1266,626 @@ modifyConst syn fc (PConstant (BI x))
8751266 ]
8761267modifyConst syn fc x = x
8771268
878−
879−pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']'
880− return (mkList fc xs)
1269+{- | Parses a list literal expression e.g. [1,2,3]
1270+ListExpr ::=
1271+ '[' ExprList? ']'
1272+;
1273+
1274+ExprList ::=
1275+ Expr
1276+ | Expr ',' ExprList
1277+ ;
1278+
1279+ -}
1280+listExpr :: SyntaxInfo -> IdrisParser PTerm
1281+listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lchar ']'
1282+ return (mkList fc xs)
1283+ <?> "list expression"
8811284 where
1285+ mkList :: FC -> [PTerm] -> PTerm
8821286 mkList fc [] = PRef fc (UN "Nil")
883− mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
884−
885−pPair syn = try (do l <- pExpr syn
886− fc <- pfc
887− rest <- restTuple
888− case rest of
889− [] -> return l
890− [Left r] -> return (PPair fc l r)
891− [Right r] -> return (PDPair fc l Placeholder r))
1287+ mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
1288+
1289+{- | Parses rest of pair expression
1290+Pair ::=
1291+ Expr RestTuple? ')'
1292+ | NTuple ')'
1293+ | Name ':' Expr '**' 'Expr' ')'
1294+ ;
1295+
1296+RestTuple ::=
1297+ ',' Expr
1298+ | '**' Expr
1299+ ;
1300+
1301+NTuple ::=
1302+ Expr ',' Expr
1303+ | Expr ',' NTuple
1304+ ;
1305+-}
1306+pair :: SyntaxInfo -> IdrisParser PTerm
1307+pair syn = try (do l <- expr syn
1308+ fc <- getFC
1309+ rest <- restTuple
1310+ case rest of
1311+ [] -> return l
1312+ [Left r] -> return (PPair fc l r)
1313+ [Right r] -> return (PDPair fc l Placeholder r))
8921314 <|> try (do x <- ntuple
8931315 lchar ')'
894− return x)
895− <|> do ln <- pName; lchar ':'
896− lty <- pExpr syn
1316+ return x)
1317+ <|> do ln <- name; lchar ':'
1318+ lty <- expr syn
8971319 reservedOp "**"
898− fc <- pfc
899− r <- pExpr syn
1320+ fc <- getFC
1321+ r <- expr syn
9001322 lchar ')'
901− return (PDPair fc (PRef fc ln) lty r)
1323+ return (PDPair fc (PRef fc ln) lty r)
1324+ <?> "pair expression"
9021325 where
1326+ restTuple :: IdrisParser [Either PTerm PTerm]
9031327 restTuple = do lchar ')'; return []
9041328 <|> do lchar ','
905− r <- pExpr syn
1329+ r <- expr syn
9061330 lchar ')'
9071331 return [Left r]
9081332 <|> do reservedOp "**"
909− r <- pExpr syn
1333+ r <- expr syn
9101334 lchar ')'
9111335 return [Right r]
912− ntuple = try (do l <- pExpr syn; fc <- pfc; lchar ','
1336+ <?> "end of pair expression"
1337+ ntuple :: IdrisParser PTerm
1338+ ntuple = try (do l <- expr syn; fc <- getFC; lchar ','
9131339 rest <- ntuple
9141340 return (PPair fc l rest))
915− <|> (do l <- pExpr syn; fc <- pfc; lchar ','
916− r <- pExpr syn
1341+ <|> (do l <- expr syn; fc <- getFC; lchar ','
1342+ r <- expr syn
9171343 return (PPair fc l r))
918−
919−pAlt syn = do symbol "(|"; alts <- sepBy1 (pExpr' syn) (lchar ','); symbol "|)"
920− return (PAlternative False alts)
921−
922−pHSimpleExpr syn
923− = do lchar '.'
924− e <- pSimpleExpr syn
925− return $ PHidden e
926− <|> pSimpleExpr syn
927−
928−pMatchApp syn = do ty <- pSimpleExpr syn
929− symbol "<=="
930− fc <- pfc
931− f <- pfName
932− return (PLet (MN 0 "match")
1344+ <?> "tuple expression"
1345+
1346+{- | Parses an alternative expression
1347+ Alt ::= '(|' Expr_List '|)';
1348+
1349+ Expr_List ::=
1350+ Expr'
1351+ | Expr' ',' Expr_List
1352+ ;
1353+-}
1354+alt :: SyntaxInfo -> IdrisParser PTerm
1355+alt syn = do symbol "(|"; alts <- sepBy1 (expr' syn) (lchar ','); symbol "|)"
1356+ return (PAlternative False alts)
1357+
1358+{- | Parses a possibly hidden simple expression
1359+HSimpleExpr ::=
1360+ '.' SimpleExpr
1361+ | SimpleExpr
1362+ ;
1363+-}
1364+hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm
1365+hsimpleExpr syn =
1366+ do lchar '.'
1367+ e <- simpleExpr syn
1368+ return $ PHidden e
1369+ <|> simpleExpr syn
1370+ <?> "expression"
1371+
1372+{- | Parses a matching application expression
1373+MatchApp ::=
1374+ SimpleExpr '<==' FnName
1375+ ;
1376+-}
1377+matchApp :: SyntaxInfo -> IdrisParser PTerm
1378+matchApp syn = do ty <- simpleExpr syn
1379+ symbol "<=="
1380+ fc <- getFC
1381+ f <- fnName
1382+ return (PLet (MN 0 "match")
9331383 ty
9341384 (PMatchApp fc f)
9351385 (PRef fc (MN 0 "match")))
936−
937−pUnifyLog syn = do lchar '%'; reserved "unifyLog";
938− tm <- pSimpleExpr syn
939− return (PUnifyLog tm)
940−
941−pApp syn = do f <- reserved "mkForeign"
942− fc <- pfc
943− fn <- pArg syn
944− args <- many (do notEndApp; pArg syn)
945− i <- getState
946− -- mkForeign f args ==>
947− -- liftPrimIO (\w => mkForeignPrim f args w)
948− let ap = PApp fc (PRef fc (UN "liftPrimIO"))
949− [pexp (PLam (MN 0 "w")
950− Placeholder
951− (PApp fc (PRef fc (UN "mkForeignPrim"))
952− (fn : args ++
953− [pexp (PRef fc (MN 0 "w"))])))]
954− return (dslify i ap)
955−
956− <|> do f <- pSimpleExpr syn
957− fc <- pfc
958− args <- many1 (do notEndApp
959− pArg syn)
960− i <- getState
1386+ <?> "matching application expression"
1387+
1388+{- | Parses a unification log expression
1389+UnifyLog ::=
1390+ '%' 'unifyLog' SimpleExpr
1391+ ;
1392+-}
1393+unifyLog :: SyntaxInfo -> IdrisParser PTerm
1394+unifyLog syn = do lchar '%'; reserved "unifyLog";
1395+ tm <- simpleExpr syn
1396+ return (PUnifyLog tm)
1397+ <?> "unification log expression"
1398+
1399+{- | Parses a function application expression
1400+App ::=
1401+ 'mkForeign' Arg Arg*
1402+ | SimpleExpr Arg+
1403+ ;
1404+-}
1405+app :: SyntaxInfo -> IdrisParser PTerm
1406+app syn = do f <- reserved "mkForeign"
1407+ fc <- getFC
1408+ fn <- arg syn
1409+ args <- many (do notEndApp; arg syn)
1410+ i <- get
1411+ -- mkForeign f args ==>
1412+ -- liftPrimIO (\w => mkForeignPrim f args w)
1413+ let ap = PApp fc (PRef fc (UN "liftPrimIO"))
1414+ [pexp (PLam (MN 0 "w")
1415+ Placeholder
1416+ (PApp fc (PRef fc (UN "mkForeignPrim"))
1417+ (fn : args ++
1418+ [pexp (PRef fc (MN 0 "w"))])))]
1419+ return (dslify i ap)
1420+
1421+ <|> do f <- simpleExpr syn
1422+ fc <- getFC
1423+ args <- some (do notEndApp; arg syn)
1424+ i <- get
9611425 return (dslify i $ PApp fc f args)
1426+ <?> "function application"
9621427 where
1428+ dslify :: IState -> PTerm -> PTerm
9631429 dslify i (PApp fc (PRef _ f) [a])
9641430 | [d] <- lookupCtxt f (idris_dsls i)
9651431 = desugar (syn { dsl_info = d }) i (getTm a)
9661432 dslify i t = t
9671433
968−pArg :: SyntaxInfo -> IParser PArg
969−pArg syn = try (pImplicitArg syn)
970− <|> try (pConstraintArg syn)
971− <|> do e <- pSimpleExpr syn
1434+{- |Parses a function argument
1435+Arg ::=
1436+ ImplicitArg
1437+ | ConstraintArg
1438+ | SimpleExpr
1439+ ;
1440+-}
1441+arg :: SyntaxInfo -> IdrisParser PArg
1442+arg syn = try (implicitArg syn)
1443+ <|> try (constraintArg syn)
1444+ <|> do e <- simpleExpr syn
9721445 return (pexp e)
973−
974−pImplicitArg syn = do lchar '{'
975− n <- pName
976− fc <- pfc
977− v <- option (PRef fc n) (do lchar '='
978− pExpr syn)
979− lchar '}'
980− return (pimp n v)
981−
982−pConstraintArg syn = do symbol "@{"
983− e <- pExpr syn
984− symbol "}"
985− return (pconst e)
986−
987−pRecordType syn
1446+ <?> "function argument"
1447+
1448+{- |Parses an implicit function argument
1449+ImplicitArg ::=
1450+ '{' Name ('=' Expr)? '}'
1451+ ;
1452+-}
1453+implicitArg :: SyntaxInfo -> IdrisParser PArg
1454+implicitArg syn = do lchar '{'
1455+ n <- name
1456+ fc <- getFC
1457+ v <- option (PRef fc n) (do lchar '='
1458+ expr syn)
1459+ lchar '}'
1460+ return (pimp n v)
1461+ <?> "implicit function argument"
1462+
1463+{- |Parses a constraint argument (for selecting a named type class instance)
1464+ConstraintArg ::=
1465+ '@{' Expr '}'
1466+ ;
1467+-}
1468+constraintArg :: SyntaxInfo -> IdrisParser PArg
1469+constraintArg syn = do symbol "@{"
1470+ e <- expr syn
1471+ symbol "}"
1472+ return (pconst e)
1473+ <?> "constraint argument"
1474+
1475+
1476+{- |Parses a record field setter expression
1477+RecordType ::=
1478+ 'record' '{' FieldTypeList '}';
1479+
1480+FieldTypeList ::=
1481+ FieldType
1482+ | FieldType ',' FieldTypeList
1483+ ;
1484+
1485+FieldType ::=
1486+ FnName '=' Expr
1487+ ;
1488+-}
1489+recordType :: SyntaxInfo -> IdrisParser PTerm
1490+recordType syn
9881491 = do reserved "record"
9891492 lchar '{'
990− fields <- sepBy1 pFieldType (lchar ',')
1493+ fields <- sepBy1 fieldType (lchar ',')
9911494 lchar '}'
992− fc <- pfc
993− rec <- option Nothing (do e <- pSimpleExpr syn
994− return (Just e))
1495+ fc <- getFC
1496+ rec <- optional (simpleExpr syn)
9951497 case rec of
9961498 Nothing ->
9971499 return (PLam (MN 0 "fldx") Placeholder
9981500 (applyAll fc fields (PRef fc (MN 0 "fldx"))))
9991501 Just v -> return (applyAll fc fields v)
1000− where pFieldType = do n <- pfName
1001− lchar '='
1002− e <- pExpr syn
1003− return (n, e)
1502+ <?> "record setting expression"
1503+ where fieldType :: IdrisParser (Name, PTerm)
1504+ fieldType = do n <- fnName
1505+ lchar '='
1506+ e <- expr syn
1507+ return (n, e)
1508+ <?> "field setter"
1509+ applyAll :: FC -> [(Name, PTerm)] -> PTerm -> PTerm
10041510 applyAll fc [] x = x
10051511 applyAll fc ((n, e) : es) x
10061512 = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])
1007−
1513+
1514+{- |Creates setters for record types on necessary functions -}
1515+mkType :: Name -> Name
10081516mkType (UN n) = UN ("set_" ++ n)
10091517mkType (MN 0 n) = MN 0 ("set_" ++ n)
10101518mkType (NS n s) = NS (mkType n) s
10111519
1012−noImp syn = syn { implicitAllowed = False }
1013−impOK syn = syn { implicitAllowed = True }
1014−
1015−pTSig syn = do lchar ':'; pTExpr syn
1016−
1017−pTExpr syn = do cs <- if implicitAllowed syn then pConstList syn else return []
1018− sc <- pExpr syn
1019− return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
1020−
1021−pLambda syn = do lchar '\\'
1022− try (do xt <- tyOptDeclList syn
1520+{- |Parses a type for an expression
1521+TypeSig ::=
1522+ ':' Expr
1523+ ;
1524+-}
1525+typeSig :: SyntaxInfo -> IdrisParser PTerm
1526+typeSig syn = lchar ':' *> typeExpr syn <?> "type"
1527+
1528+{- |Parses a type signature
1529+TypeExpr ::= ConstraintList? Expr;
1530+ -}
1531+typeExpr :: SyntaxInfo -> IdrisParser PTerm
1532+typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []
1533+ sc <- expr syn
1534+ return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
1535+ <?> "type signature"
1536+
1537+{- |Parses a lambda expression
1538+Lambda ::=
1539+ '\\' TypeOptDeclList '=>' Expr
1540+ | '\\' SimpleExprList '=>' Expr
1541+ ;
1542+SimpleExprList ::=
1543+ SimpleExpr
1544+ | SimpleExpr ',' SimpleExprList
1545+ ;
1546+-}
1547+lambda :: SyntaxInfo -> IdrisParser PTerm
1548+lambda syn = do lchar '\\'
1549+ try (do xt <- tyOptDeclList syn
1550+ symbol "=>"
1551+ sc <- expr syn
1552+ return (bindList PLam xt sc)
1553+ <|> (do ps <- sepBy (do fc <- getFC
1554+ e <- simpleExpr syn
1555+ return (fc, e)) (lchar ',')
10231556 symbol "=>"
1024− sc <- pExpr syn
1025− return (bindList PLam xt sc)
1026− <|> (do ps <- sepBy (do fc <- pfc
1027− e <- pSimpleExpr syn
1028− return (fc, e)) (lchar ',')
1029− symbol "=>"
1030− sc <- pExpr syn
1031− return (pmList (zip [0..] ps) sc)))
1032− where pmList [] sc = sc
1033− pmList ((i, (fc, x)) : xs) sc
1557+ sc <- expr syn
1558+ return (pmList (zip [0..] ps) sc)))
1559+ <?> "lambda expression"
1560+ where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm
1561+ pmList [] sc = sc
1562+ pmList ((i, (fc, x)) : xs) sc
10341563 = PLam (MN i "lamp") Placeholder
10351564 (PCase fc (PRef fc (MN i "lamp"))
10361565 [(x, pmList xs sc)])
10371566
1038−pRewriteTerm syn =
1039− do reserved "rewrite"
1040− fc <- pfc
1041− prf <- pExpr syn
1042− giving <- option Nothing
1043− (do symbol "==>"; tm <- pExpr' syn
1044− return (Just tm))
1045− reserved "in"; sc <- pExpr syn
1046− return (PRewrite fc
1567+{- |Parses a term rewrite expression
1568+RewriteTerm ::=
1569+ 'rewrite' Expr ('==>' Expr)? 'in' Expr
1570+ ;
1571+-}
1572+rewriteTerm :: SyntaxInfo -> IdrisParser PTerm
1573+rewriteTerm syn = do reserved "rewrite"
1574+ fc <- getFC
1575+ prf <- expr syn
1576+ giving <- optional (do symbol "==>"; expr' syn)
1577+ reserved "in"; sc <- expr syn
1578+ return (PRewrite fc
10471579 (PApp fc (PRef fc (UN "sym")) [pexp prf]) sc
10481580 giving)
1049−
1050−pLet syn = try (do reserved "let"; n <- pName;
1051− ty <- option Placeholder (do lchar ':'; pExpr' syn)
1581+ <?> "term rewrite expression"
1582+
1583+{- |Parses a let binding
1584+Let ::=
1585+ 'let' Name TypeSig'? '=' Expr 'in' Expr
1586+| 'let' Expr' '=' Expr' 'in' Expr
1587+
1588+TypeSig' ::=
1589+ ':' Expr'
1590+ ;
1591+ -}
1592+let_ :: SyntaxInfo -> IdrisParser PTerm
1593+let_ syn = try (do reserved "let"; n <- name;
1594+ ty <- option Placeholder (do lchar ':'; expr' syn)
10521595 lchar '='
1053− v <- pExpr syn
1054− reserved "in"; sc <- pExpr syn
1596+ v <- expr syn
1597+ reserved "in"; sc <- expr syn
10551598 return (PLet n ty v sc))
1056− <|> (do reserved "let"; fc <- pfc; pat <- pExpr' (syn { inPattern = True } )
1057− symbol "="; v <- pExpr syn
1058− reserved "in"; sc <- pExpr syn
1599+ <|> (do reserved "let"; fc <- getFC; pat <- expr' (syn { inPattern = True } )
1600+ symbol "="; v <- expr syn
1601+ reserved "in"; sc <- expr syn
10591602 return (PCase fc v [(pat, sc)]))
1060−
1061−pQuoteGoal syn = do reserved "quoteGoal"; n <- pName;
1062− reserved "by"
1063− r <- pExpr syn
1064− reserved "in"
1065− fc <- pfc
1066− sc <- pExpr syn
1067− return (PGoal fc r n sc)
1068−
1069−pPi syn =
1603+ <?> "let binding"
1604+
1605+{- |Parses a quote goal
1606+QuoteGoal ::=
1607+ 'quoteGoal' Name 'by' Expr 'in' Expr
1608+ ;
1609+ -}
1610+quoteGoal :: SyntaxInfo -> IdrisParser PTerm
1611+quoteGoal syn = do reserved "quoteGoal"; n <- name;
1612+ reserved "by"
1613+ r <- expr syn
1614+ reserved "in"
1615+ fc <- getFC
1616+ sc <- expr syn
1617+ return (PGoal fc r n sc)
1618+ <?> "quote goal expression"
1619+
1620+{- |Parses a dependent type signature
1621+Pi ::=
1622+ '|'? Static? '(' TypeDeclList ')' DocComment '->' Expr
1623+ | '|'? Static? '{' TypeDeclList '}' '->' Expr
1624+ | '{' 'auto' TypeDeclList '}' '->' Expr
1625+ | '{' 'default' TypeDeclList '}' '->' Expr
1626+ | '{' 'static' '}' Expr' '->' Expr
1627+ ;
1628+ -}
1629+pi syn =
10701630 try (do lazy <- if implicitAllowed syn -- laziness is top level only
10711631 then option False (do lchar '|'; return True)
10721632 else return False
1073− st <- pStatic
1074− lchar '('; xt <- tyDeclList syn; lchar ')'
1075− doc <- option "" (pDocComment '^')
1633+ st <- static
1634+ lchar '('; xt <- typeDeclList syn; lchar ')'
1635+ doc <- option "" (docComment '^')
10761636 symbol "->"
1077− sc <- pExpr syn
1637+ sc <- expr syn
10781638 return (bindList (PPi (Exp lazy st doc)) xt sc))
1079− <|> try (if implicitAllowed syn
1639+ <|> try (if implicitAllowed syn
10801640 then do lazy <- option False (do lchar '|'
10811641 return True)
1082− st <- pStatic
1642+ st <- static
10831643 lchar '{'
1084− xt <- tyDeclList syn
1644+ xt <- typeDeclList syn
10851645 lchar '}'
10861646 symbol "->"
1087− sc <- pExpr syn
1647+ sc <- expr syn
10881648 return (bindList (PPi (Imp lazy st "")) xt sc)
1089− else fail "No implicit arguments allowed here")
1649+ else fail "no implicit arguments allowed here")
10901650 <|> try (do lchar '{'
10911651 reserved "auto"
1092− xt <- tyDeclList syn
1652+ xt <- typeDeclList syn
10931653 lchar '}'
10941654 symbol "->"
1095− sc <- pExpr syn
1096− return (bindList (PPi
1655+ sc <- expr syn
1656+ return (bindList (PPi
10971657 (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))
10981658 <|> try (do lchar '{'
10991659 reserved "default"
1100− script <- pSimpleExpr syn
1101− xt <- tyDeclList syn
1660+ script <- simpleExpr syn
1661+ xt <- typeDeclList syn
11021662 lchar '}'
11031663 symbol "->"
1104− sc <- pExpr syn
1664+ sc <- expr syn
11051665 return (bindList (PPi (TacImp False Dynamic script "")) xt sc))
1106− <|> do --lazy <- option False (do lchar '|'; return True)
1107− lchar '{'
1108− reserved "static"
1109− lchar '}'
1110− t <- pExpr' syn
1111− symbol "->"
1112− sc <- pExpr syn
1113− return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)
1114−
1115−pConstList :: SyntaxInfo -> IParser [PTerm]
1116−pConstList syn = try (do lchar '('
1117− tys <- sepBy1 (pExpr' (noImp syn)) (lchar ',')
1118− lchar ')'
1119− reservedOp "=>"
1120− return tys)
1121− <|> try (do t <- pExpr (noImp syn)
1122− reservedOp "=>"
1123− return [t])
1124− <|> return []
1125−
1126−usingDeclList syn
1666+ <|> do lchar '{'
1667+ reserved "static"
1668+ lchar '}'
1669+ t <- expr' syn
1670+ symbol "->"
1671+ sc <- expr syn
1672+ return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)
1673+ <?> "dependent type signature"
1674+
1675+{- | Parses a type constraint list
1676+ConstraintList ::=
1677+ '(' Expr_List ')' '=>'
1678+ | Expr '=>'
1679+ ;
1680+-}
1681+constraintList :: SyntaxInfo -> IdrisParser [PTerm]
1682+constraintList syn = try (do lchar '('
1683+ tys <- sepBy1 (expr' (disallowImp syn)) (lchar ',')
1684+ lchar ')'
1685+ reservedOp "=>"
1686+ return tys)
1687+ <|> try (do t <- expr (disallowImp syn)
1688+ reservedOp "=>"
1689+ return [t])
1690+ <|> return []
1691+ <?> "type constraint list"
1692+
1693+{- | Parses a using declaration list
1694+UsingDeclList ::=
1695+ UsingDeclList'
1696+ | NameList TypeSig
1697+ ;
1698+
1699+UsingDeclList' ::=
1700+ UsingDecl
1701+ | UsingDecl ',' UsingDeclList'
1702+ ;
1703+
1704+NameList ::=
1705+ Name
1706+ | Name ',' NameList
1707+ ;
1708+-}
1709+usingDeclList :: SyntaxInfo -> IdrisParser [Using]
1710+usingDeclList syn
11271711 = try (sepBy1 (usingDecl syn) (lchar ','))
1128− <|> do ns <- sepBy1 pName (lchar ',')
1129− t <- pTSig (noImp syn)
1712+ <|> do ns <- sepBy1 name (lchar ',')
1713+ t <- typeSig (disallowImp syn)
11301714 return (map (\x -> UImplicit x t) ns)
1131−
1132−usingDecl syn = try (do x <- pfName
1133− t <- pTSig (noImp syn)
1715+ <?> "using declaration list"
1716+
1717+{- |Parses a using declaration
1718+UsingDecl ::=
1719+ FnName TypeSig
1720+ | FnName FnName+
1721+ ;
1722+-}
1723+usingDecl :: SyntaxInfo -> IdrisParser Using
1724+usingDecl syn = try (do x <- fnName
1725+ t <- typeSig (disallowImp syn)
11341726 return (UImplicit x t))
1135− <|> do c <- pfName
1136− xs <- many1 pfName
1727+ <|> do c <- fnName
1728+ xs <- some fnName
11371729 return (UConstraint c xs)
1138−
1139−tyDeclList syn = try (sepBy1 (do x <- pfName
1140− t <- pTSig (noImp syn)
1141− return (x,t))
1142− (lchar ','))
1143− <|> do ns <- sepBy1 pName (lchar ',')
1144− t <- pTSig (noImp syn)
1145− return (map (\x -> (x, t)) ns)
1146−
1147−tyOptDeclList syn = sepBy1 (do x <- pNameOrPlaceholder
1730+ <?> "using declaration"
1731+
1732+{- |Parses a type declaration list
1733+TypeDeclList ::=
1734+ FunctionSignatureList
1735+ | NameList TypeSig
1736+ ;
1737+
1738+FunctionSignatureList ::=
1739+ Name TypeSig
1740+ | Name TypeSig ',' FunctionSignatureList
1741+ ;
1742+-}
1743+typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
1744+typeDeclList syn = try (sepBy1 (do x <- fnName
1745+ t <- typeSig (disallowImp syn)
1746+ return (x,t))
1747+ (lchar ','))
1748+ <|> do ns <- sepBy1 name (lchar ',')
1749+ t <- typeSig (disallowImp syn)
1750+ return (map (\x -> (x, t)) ns)
1751+ <?> "type declaration list"
1752+
1753+{- |Parses a type declaration list with optional parameters
1754+TypeOptDeclList ::=
1755+ NameOrPlaceholder TypeSig?
1756+ | NameOrPlaceholder TypeSig? ',' TypeOptDeclList
1757+ ;
1758+
1759+NameOrPlaceHolder ::= Name | '_';
1760+-}
1761+tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
1762+tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder
11481763 t <- option Placeholder (do lchar ':'
1149− pExpr syn)
1764+ expr syn)
11501765 return (x,t))
11511766 (lchar ',')
1152− where pNameOrPlaceholder = pfName
1767+ <?> "type declaration list"
1768+ where nameOrPlaceholder :: IdrisParser Name
1769+ nameOrPlaceholder = fnName
11531770 <|> do symbol "_"
11541771 return (MN 0 "underscore")
1155−
1156−bindList b [] sc = sc
1157−bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
1158−
1159−pComprehension syn
1772+ <?> "name or placeholder"
1773+
1774+{- |Parses a list comprehension
1775+Comprehension ::= '[' Expr '|' DoList ']';
1776+
1777+DoList ::=
1778+ Do
1779+ | Do ',' DoList
1780+ ;
1781+-}
1782+comprehension :: SyntaxInfo -> IdrisParser PTerm
1783+comprehension syn
11601784 = do lchar '['
1161− fc <- pfc
1162− pat <- pExpr syn
1785+ fc <- getFC
1786+ pat <- expr syn
11631787 lchar '|'
1164− qs <- sepBy1 (pDo syn) (lchar ',')
1788+ qs <- sepBy1 (do_ syn) (lchar ',')
11651789 lchar ']'
1166− return (PDoBlock (map addGuard qs ++
1790+ return (PDoBlock (map addGuard qs ++
11671791 [DoExp fc (PApp fc (PRef fc (UN "return"))
11681792 [pexp pat])]))
1169− where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
1793+ <?> "list comprehension"
1794+ where addGuard :: PDo -> PDo
1795+ addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
11701796 [pexp e])
11711797 addGuard x = x
11721798
1173−pDoBlock syn
1799+{- |Parses a do-block
1800+Do' ::= Do KeepTerminator;
1801+
1802+DoBlock ::=
1803+ 'do' OpenBlock Do'+ CloseBlock
1804+ ;
1805+ -}
1806+doBlock :: SyntaxInfo -> IdrisParser PTerm
1807+doBlock syn
11741808 = do reserved "do"
1175− openBlock
1176− pushIndent
1177− ds <- many1 (do notEndBlock
1178− x <- pDo syn
1179− pKeepTerminator
1180− return x)
1181− popIndent
1182− closeBlock
1809+ ds <- indentedBlock (do_ syn)
11831810 return (PDoBlock ds)
1184−
1185−pDo syn
1811+ <?> "do block"
1812+
1813+{- |Parses an expression inside a do block
1814+Do ::=
1815+ 'let' Name TypeSig'? '=' Expr
1816+ | 'let' Expr' '=' Expr
1817+ | Name '<-' Expr
1818+ | Expr' '<-' Expr
1819+ | Expr
1820+ ;
1821+-}
1822+do_ :: SyntaxInfo -> IdrisParser PDo
1823+do_ syn
11861824 = try (do reserved "let"
1187− i <- pName;
1825+ i <- name
11881826 ty <- option Placeholder (do lchar ':'
1189− pExpr' syn)
1827+ expr' syn)
11901828 reservedOp "="
1191− fc <- pfc
1192− e <- pExpr syn
1829+ fc <- getFC
1830+ e <- expr syn
11931831 return (DoLet fc i ty e))
11941832 <|> try (do reserved "let"
1195− i <- pExpr' syn
1833+ i <- expr' syn
11961834 reservedOp "="
1197− fc <- pfc
1198− sc <- pExpr syn
1835+ fc <- getFC
1836+ sc <- expr syn
11991837 return (DoLetP fc i sc))
1200− <|> try (do i <- pName
1838+ <|> try (do i <- name
12011839 symbol "<-"
1202− fc <- pfc
1203− e <- pExpr syn;
1840+ fc <- getFC
1841+ e <- expr syn;
12041842 return (DoBind fc i e))
1205− <|> try (do i <- pExpr' syn
1843+ <|> try (do i <- expr' syn
12061844 symbol "<-"
1207− fc <- pfc
1208− e <- pExpr syn;
1845+ fc <- getFC
1846+ e <- expr syn;
12091847 return (DoBindP fc i e))
1210− <|> try (do e <- pExpr syn
1211− fc <- pfc
1848+ <|> try (do e <- expr syn
1849+ fc <- getFC
12121850 return (DoExp fc e))
1851+ <?> "do block expression"
12131852
1214−pIdiom syn
1853+{- |Parses an expression in idiom brackets
1854+Idiom ::= '[|' Expr '|]';
1855+-}
1856+idiom :: SyntaxInfo -> IdrisParser PTerm
1857+idiom syn
12151858 = do symbol "[|"
1216− fc <- pfc
1217− e <- pExpr syn
1859+ fc <- getFC
1860+ e <- expr syn
12181861 symbol "|]"
12191862 return (PIdiom fc e)
1220−
1221−pConstant :: IParser Const
1222−pConstant = do reserved "Integer";return (AType (ATInt ITBig))
1863+ <?> "expression in idiom brackets"
1864+
1865+{- |Parses a constant or literal expression
1866+Constant ::=
1867+ 'Integer'
1868+ | 'Int'
1869+ | 'Char'
1870+ | 'Float'
1871+ | 'String'
1872+ | 'Ptr'
1873+ | 'Bits8'
1874+ | 'Bits16'
1875+ | 'Bits32'
1876+ | 'Bits64'
1877+ | 'Bits8x16'
1878+ | 'Bits16x8'
1879+ | 'Bits32x4'
1880+ | 'Bits64x2'
1881+ | Float_t
1882+ | Natural_t
1883+ | String_t
1884+ | Char_t
1885+ ;
1886+-}
1887+constant :: IdrisParser Core.TT.Const
1888+constant = do reserved "Integer";return (AType (ATInt ITBig))
12231889 <|> do reserved "Int"; return (AType (ATInt ITNative))
12241890 <|> do reserved "Char"; return (AType (ATInt ITChar))
12251891 <|> do reserved "Float"; return (AType ATFloat)
@@ -1235,121 +1901,100 @@ pConstant = do reserved "Integer";return (AType (ATInt ITBig))
12351901 <|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2)))
12361902 <|> try (do f <- float; return $ Fl f)
12371903 <|> try (do i <- natural; return $ BI i)
1238− <|> try (do s <- strlit; return $ Str s)
1239− <|> try (do c <- chlit; return $ Ch c)
1240−
1241−pStatic :: IParser Static
1242−pStatic = do lchar '['
1243− reserved "static"
1244− lchar ']';
1245− return Static
1904+ <|> try (do s <- stringLiteral; return $ Str s)
1905+ <|> try (do c <- charLiteral; return $ Ch c)
1906+ <?> "constant or literal"
1907+
1908+{- |Parses a static modifier
1909+Static ::=
1910+ '[' static ']'
1911+;
1912+-}
1913+static :: IdrisParser Static
1914+static = do lchar '['; reserved "static"; lchar ']'; return Static
12461915 <|> return Dynamic
1247−
1248−table fixes
1249− = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
1250− [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]
1251− ++ toTable (reverse fixes) ++
1252− [[backtick],
1253− [binary "=" PEq AssocLeft],
1254− [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
1255−
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])
1260− toBin (Fix f op)
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
1265−
1266−binary name f = Infix (do fc <- pfc
1267− reservedOp name
1268− doc <- option "" (pDocComment '^')
1269− return (f fc))
1270−prefix name f = Prefix (do reservedOp name
1271− fc <- pfc;
1272− return (f fc))
1273−backtick = Infix (do lchar '`'; n <- pfName
1274− lchar '`'
1275− fc <- pfc
1276− return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
1277−
1278−--------- Data declarations ---------
1279−
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
1286−
1287−pRecord :: SyntaxInfo -> IParser PDecl
1288−pRecord syn = do doc <- option "" (pDocComment '|')
1289− acc <- pAccessibility
1290− reserved "record"
1291− fc <- pfc
1292− tyn_in <- pfName
1293− ty <- pTSig (impOK syn)
1294− let tyn = expandNS syn tyn_in
1295− reserved "where"
1296− openBlock
1297− pushIndent
1298− (cdoc, cn, cty, _) <- pConstructor syn
1299− pKeepTerminator
1300− popIndent
1301− closeBlock
1302− accData acc tyn [cn]
1303− let rsyn = syn { syn_namespace = show (nsroot tyn) :
1304− syn_namespace syn }
1305− let fns = getRecNames rsyn cty
1306− mapM_ (\n -> addAcc n acc) fns
1307− return $ PRecord doc rsyn fc tyn ty cdoc cn cty
1916+ <?> "static modifier"
1917+
1918+{- |Parses a record type declaration
1919+Record ::=
1920+ DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
1921+-}
1922+record :: SyntaxInfo -> IdrisParser PDecl
1923+record syn = do doc <- option "" (docComment '|')
1924+ acc <- optional accessibility
1925+ reserved "record"
1926+ fc <- getFC
1927+ tyn_in <- fnName
1928+ ty <- typeSig (allowImp syn)
1929+ let tyn = expandNS syn tyn_in
1930+ reserved "where"
1931+ (cdoc, cn, cty, _) <- indentedBlockS (constructor syn)
1932+ accData acc tyn [cn]
1933+ let rsyn = syn { syn_namespace = show (nsroot tyn) :
1934+ syn_namespace syn }
1935+ let fns = getRecNames rsyn cty
1936+ mapM_ (\n -> addAcc n acc) fns
1937+ return $ PRecord doc rsyn fc tyn ty cdoc cn cty
1938+ <?> "record type declaration"
13081939 where
1940+ getRecNames :: SyntaxInfo -> PTerm -> [Name]
13091941 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
13101942 ++ getRecNames syn sc
13111943 getRecNames _ _ = []
13121944
1945+ toFreeze :: Maybe Accessibility -> Maybe Accessibility
13131946 toFreeze (Just Frozen) = Just Hidden
13141947 toFreeze x = x
13151948
1316−pDataI = do reserved "data"; return False
1317− <|> do reserved "codata"; return True
1318−
1319−pData :: SyntaxInfo -> IParser PDecl
1320−pData syn = try (do doc <- option "" (pDocComment '|')
1321− acc <- pAccessibility
1322− co <- pDataI
1323− fc <- pfc
1324− tyn_in <- pfName
1325− ty <- pTSig (impOK syn)
1949+{- | Parses data declaration type (normal or codata)
1950+DataI ::= 'data' | 'codata';
1951+-}
1952+dataI :: IdrisParser Bool
1953+dataI = do reserved "data"; return False
1954+ <|> do reserved "codata"; return True
1955+
1956+{- | Parses a data type declaration
1957+Data ::= DocComment? Accessibility? DataI FnName TypeSig ExplicitTypeDataRest?
1958+ | DocComment? Accessibility? DataI FnName Name* DataRest?
1959+ ;
1960+Constructor' ::= Constructor KeepTerminator;
1961+ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;
1962+
1963+DataRest ::= '=' SimpleConstructorList Terminator
1964+ | 'where'!
1965+ ;
1966+SimpleConstructorList ::=
1967+ SimpleConstructor
1968+ | SimpleConstructor '|' SimpleConstructorList
1969+ ;
1970+-}
1971+data_ :: SyntaxInfo -> IdrisParser PDecl
1972+data_ syn = try (do doc <- option "" (docComment '|')
1973+ acc <- optional accessibility
1974+ co <- dataI
1975+ fc <- getFC
1976+ tyn_in <- fnName
1977+ ty <- typeSig (allowImp syn)
13261978 let tyn = expandNS syn tyn_in
13271979 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
13281980 reserved "where"
1329− openBlock
1330− pushIndent
1331− cons <- many (do notEndBlock
1332− c <- pConstructor syn
1333− pKeepTerminator
1334− return c) -- (lchar '|')
1335− popIndent
1336− closeBlock
1981+ cons <- indentedBlock (constructor syn)
13371982 accData acc tyn (map (\ (_, n, _, _) -> n) cons)
13381983 return $ PData doc syn fc co (PDatadecl tyn ty cons)))
1339− <|> try (do doc <- option "" (pDocComment '|')
1984+ <|> try (do doc <- option "" (docComment '|')
13401985 pushIndent
1341− acc <- pAccessibility
1342− co <- pDataI
1343− fc <- pfc
1344− tyn_in <- pfName
1345− args <- many pName
1986+ acc <- optional accessibility
1987+ co <- dataI
1988+ fc <- getFC
1989+ tyn_in <- fnName
1990+ args <- many name
13461991 let ty = bindArgs (map (const PType) args) PType
13471992 let tyn = expandNS syn tyn_in
13481993 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
13491994 try (lchar '=') <|> do reserved "where"
13501995 let kw = (if co then "co" else "") ++ "data "
13511996 let n = show tyn_in ++ " "
1352− let s = kw ++ n
1997+ let s = kw ++ n
13531998 let as = concat (intersperse " " $ map show args) ++ " "
13541999 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
13552000 let ss = concat (intersperse " -> " $ map (const "Type") args)
@@ -1357,60 +2002,64 @@ pData syn = try (do doc <- option "" (pDocComment '|')
13572002 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
13582003 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
13592004 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
1360−
1361− cons <- sepBy1 (pSimpleCon syn) (lchar '|')
1362− pTerminator
2005+ cons <- sepBy1 (simpleConstructor syn) (lchar '|')
2006+ terminator
13632007 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) ->
13652009 do let cty = bindArgs cargs conty
13662010 return (doc, x, cty, cfc)) cons
13672011 accData acc tyn (map (\ (_, n, _, _) -> n) cons')
13682012 return $ PData doc syn fc co (PDatadecl tyn ty cons')))
2013+ <?> "data type declaration"
13692014 where
2015+ mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
13702016 mkPApp fc t [] = t
13712017 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
13722020
1373−bindArgs :: [PTerm] -> PTerm -> PTerm
1374−bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
13752021
1376−pConstructor :: SyntaxInfo -> IParser (String, Name, PTerm, FC)
1377−pConstructor syn
1378− = do doc <- option "" (pDocComment '|')
1379− cn_in <- pfName; fc <- pfc
2022+{- | Parses a type constructor declaration
2023+ Constructor ::= DocComment? FnName TypeSig;
2024+-}
2025+constructor :: SyntaxInfo -> IdrisParser (String, Name, PTerm, FC)
2026+constructor syn
2027+ = do doc <- option "" (docComment '|')
2028+ cn_in <- fnName; fc <- getFC
13802029 let cn = expandNS syn cn_in
1381− ty <- pTSig (impOK syn)
1382−-- ty' <- implicit syn cn ty
2030+ ty <- typeSig (allowImp syn)
13832031 return (doc, cn, ty, fc)
1384−
1385−
1386−pSimpleCon :: SyntaxInfo -> IParser (String, Name, [PTerm], FC)
1387−pSimpleCon syn
1388− = do cn_in <- pfName
2032+ <?> "constructor"
2033+
2034+{- | Parses a constructor for simple discriminative union data types
2035+ SimpleConstructor ::= FnName SimpleExpr* DocComment?
2036+-}
2037+simpleConstructor :: SyntaxInfo -> IdrisParser (String, Name, [PTerm], FC)
2038+simpleConstructor syn
2039+ = do cn_in <- fnName
13892040 let cn = expandNS syn cn_in
1390− fc <- pfc
2041+ fc <- getFC
13912042 args <- many (do notEndApp
1392− pSimpleExpr syn)
1393− doc <- option "" (pDocComment '^')
2043+ simpleExpr syn)
2044+ doc <- option "" (docComment '^')
13942045 return (doc, cn, args, fc)
1395−
1396−--------- DSL syntax overloading ---------
1397−
1398−pDSL :: SyntaxInfo -> IParser PDecl
1399−pDSL syn = do reserved "dsl"
1400− n <- pfName
1401− openBlock
1402− pushIndent
1403− bs <- many1 (do notEndBlock
1404− b <- pOverload syn
1405− pKeepTerminator
1406− return b)
1407− popIndent; closeBlock
1408− let dsl = mkDSL bs (dsl_info syn)
1409− checkDSL dsl
1410− i <- getState
1411− setState (i { idris_dsls = addDef n dsl (idris_dsls i) })
1412− return (PDSL n dsl)
1413− where mkDSL bs dsl = let var = lookup "variable" bs
2046+ <?> "constructor"
2047+
2048+{- | Parses a dsl block declaration
2049+DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;
2050+ -}
2051+dsl :: SyntaxInfo -> IdrisParser PDecl
2052+dsl syn = do reserved "dsl"
2053+ n <- fnName
2054+ bs <- indentedBlock (overload syn)
2055+ let dsl = mkDSL bs (dsl_info syn)
2056+ checkDSL dsl
2057+ i <- get
2058+ put (i { idris_dsls = addDef n dsl (idris_dsls i) })
2059+ return (PDSL n dsl)
2060+ <?> "dsl block declaration"
2061+ where mkDSL :: [(String, PTerm)] -> DSL -> DSL
2062+ mkDSL bs dsl = let var = lookup "variable" bs
14142063 first = lookup "index_first" bs
14152064 next = lookup "index_next" bs
14162065 leto = lookup "let" bs
@@ -1421,229 +2070,309 @@ pDSL syn = do reserved "dsl"
14212070 dsl_lambda = lambda,
14222071 dsl_let = leto }
14232072
1424−checkDSL :: DSL -> IParser ()
2073+{- | Checks DSL for errors -}
2074+-- FIXME: currently does nothing, check if DSL is really sane
2075+checkDSL :: DSL -> IdrisParser ()
14252076checkDSL dsl = return ()
14262077
1427−pOverload :: SyntaxInfo -> IParser (String, PTerm)
1428−pOverload syn = do o <- identifier <|> do reserved "let"
1429− return "let"
1430− if o `notElem` overloadable
1431− then fail $ show o ++ " is not an overloading"
1432− else do
1433− lchar '='
1434− t <- pExpr syn
1435− return (o, t)
2078+{- | Parses a DSL overload declaration
2079+OverloadIdentifier ::= 'let' | Identifier;
2080+Overload ::= OverloadIdentifier '=' Expr;
2081+-}
2082+overload :: SyntaxInfo -> IdrisParser (String, PTerm)
2083+overload syn = do o <- identifier <|> do reserved "let"
2084+ return "let"
2085+ if o `notElem` overloadable
2086+ then fail $ show o ++ " is not an overloading"
2087+ else do
2088+ lchar '='
2089+ t <- expr syn
2090+ return (o, t)
2091+ <?> "dsl overload declaratioN"
14362092 where overloadable = ["let","lambda","index_first","index_next","variable"]
14372093
1438−--------- Pattern match clauses ---------
1439−
1440−pPattern :: SyntaxInfo -> IParser PDecl
1441−pPattern syn = do fc <- pfc
1442− clause <- pClause syn
1443− return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
1444−
1445−pCAF :: SyntaxInfo -> IParser PDecl
1446−pCAF syn = do reserved "let"
1447− n_in <- pfName; let n = expandNS syn n_in
1448− lchar '='
1449− t <- pExpr syn
1450− pTerminator
1451− fc <- pfc
1452− return (PCAF fc n t)
1453−
1454−pArgExpr syn = let syn' = syn { inPattern = True } in
1455− try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
1456−
1457−pRHS :: SyntaxInfo -> Name -> IParser PTerm
1458−pRHS syn n = do lchar '='; pExpr syn
1459− <|> do symbol "?=";
1460− name <- option n' (do symbol "{"; n <- pfName; symbol "}";
1461− return n)
1462− rhs <- pExpr syn
1463− return (addLet name rhs)
1464− <|> do reserved "impossible"; return PImpossible
1465− where mkN (UN x) = UN (x++"_lemma_1")
2094+{- | Parse a clause with patterns
2095+Pattern ::= Clause;
2096+-}
2097+pattern :: SyntaxInfo -> IdrisParser PDecl
2098+pattern syn = do fc <- getFC
2099+ clause <- clause syn
2100+ return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
2101+ <?> "pattern"
2102+
2103+{- | Parse a constant applicative form declaration
2104+ CAF ::= 'let' FnName '=' Expr Terminator;
2105+-}
2106+caf :: SyntaxInfo -> IdrisParser PDecl
2107+caf syn = do reserved "let"
2108+ n_in <- fnName; let n = expandNS syn n_in
2109+ lchar '='
2110+ t <- expr syn
2111+ terminator
2112+ fc <- getFC
2113+ return (PCAF fc n t)
2114+ <?> "constant applicative form declaration"
2115+
2116+{- | Parse an argument expression
2117+ ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
2118+-}
2119+argExpr :: SyntaxInfo -> IdrisParser PTerm
2120+argExpr syn = let syn' = syn { inPattern = True } in
2121+ try (hsimpleExpr syn') <|> simpleExternalExpr syn'
2122+ <?> "argument expression"
2123+
2124+{- | Parse a right hand side of a function
2125+RHS ::= '=' Expr
2126+ | '?=' RHSName? Expr
2127+ | 'impossible'
2128+ ;
2129+
2130+RHSName ::= '{' FnName '}';
2131+-}
2132+rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
2133+rhs syn n = do lchar '='; expr syn
2134+ <|> do symbol "?=";
2135+ name <- option n' (do symbol "{"; n <- fnName; symbol "}";
2136+ return n)
2137+ r <- expr syn
2138+ return (addLet name r)
2139+ <|> do reserved "impossible"; return PImpossible
2140+ <?> "function right hand side"
2141+ where mkN :: Name -> Name
2142+ mkN (UN x) = UN (x++"_lemma_1")
14662143 mkN (NS x n) = NS (mkN x) n
2144+ n' :: Name
14672145 n' = mkN n
1468−
1469− addLet nm (PLet n ty val rhs) = PLet n ty val (addLet nm rhs)
2146+ addLet :: Name -> PTerm -> PTerm
2147+ addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)
14702148 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
14712149 where addLetC (l, r) = (l, addLet nm r)
1472− addLet nm rhs = (PLet (UN "value") Placeholder rhs (PMetavar nm))
1473−
1474−pClause :: SyntaxInfo -> IParser PClause
1475−pClause syn
2150+ addLet nm r = (PLet (UN "value") Placeholder r (PMetavar nm))
2151+
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
2160+ ;
2161+ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
2162+WhereOrTerminator ::= WhereBlock | Terminator;
2163+-}
2164+clause :: SyntaxInfo -> IdrisParser PClause
2165+clause syn
14762166 = try (do pushIndent
1477− n_in <- pfName; let n = expandNS syn n_in
1478− cargs <- many (pConstraintArg syn)
1479− iargs <- many (pImplicitArg (syn { inPattern = True } ))
1480− fc <- pfc
1481− args <- many (try (pImplicitArg (syn { inPattern = True } ))
1482− <|> (fmap pexp (pArgExpr syn)))
1483− wargs <- many (pWExpr syn)
1484− rhs <- pRHS syn n
1485− ist <- getState
2167+ n_in <- fnName; let n = expandNS syn n_in
2168+ cargs <- many (constraintArg syn)
2169+ fc <- getFC
2170+ args <- many (try (implicitArg (syn { inPattern = True } ))
2171+ <|> (fmap pexp (argExpr syn)))
2172+ wargs <- many (wExpr syn)
2173+ r <- rhs syn n
2174+ ist <- get
14862175 let ctxt = tt_ctxt ist
14872176 let wsyn = syn { syn_namespace = [] }
1488− (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
2177+ (wheres, nmap) <- choice [do x <- whereBlock n wsyn
14892178 popIndent
1490− return x,
1491− do pTerminator
2179+ return x,
2180+ do terminator
14922181 return ([], [])]
1493− let capp = PApp fc (PRef fc n)
1494− (iargs ++ cargs ++ args)
1495− ist <- getState
1496− setState (ist { lastParse = Just n })
1497− return $ PClause fc n capp wargs rhs wheres)
2182+ let capp = PApp fc (PRef fc n)
2183+ (cargs ++ args)
2184+ ist <- get
2185+ put (ist { lastParse = Just n })
2186+ return $ PClause fc n capp wargs r wheres)
14982187 <|> try (do pushIndent
1499− ty <- pSimpleExpr syn
2188+ ty <- simpleExpr syn
15002189 symbol "<=="
1501− fc <- pfc
1502− n_in <- pfName; let n = expandNS syn n_in
1503− rhs <- pRHS syn n
1504− ist <- getState
2190+ fc <- getFC
2191+ n_in <- fnName; let n = expandNS syn n_in
2192+ r <- rhs syn n
2193+ ist <- get
15052194 let ctxt = tt_ctxt ist
15062195 let wsyn = syn { syn_namespace = [] }
1507− (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
2196+ (wheres, nmap) <- choice [do x <- whereBlock n wsyn
15082197 popIndent
1509− return x,
1510− do pTerminator
2198+ return x,
2199+ do terminator
15112200 return ([], [])]
15122201 let capp = PLet (MN 0 "match")
15132202 ty
15142203 (PMatchApp fc n)
15152204 (PRef fc (MN 0 "match"))
1516− ist <- getState
1517− setState (ist { lastParse = Just n })
1518− return $ PClause fc n capp [] rhs wheres)
2205+ ist <- get
2206+ put (ist { lastParse = Just n })
2207+ return $ PClause fc n capp [] r wheres)
15192208 <|> try (do pushIndent
1520− wargs <- many1 (pWExpr syn)
1521− ist <- getState
2209+ wargs <- some (wExpr syn)
2210+ ist <- get
15222211 n <- case lastParse ist of
15232212 Just t -> return t
15242213 Nothing -> fail "Invalid clause"
1525− fc <- pfc
1526− rhs <- pRHS syn n
2214+ fc <- getFC
2215+ r <- rhs syn n
15272216 let ctxt = tt_ctxt ist
15282217 let wsyn = syn { syn_namespace = [] }
1529− (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
2218+ (wheres, nmap) <- choice [do x <- whereBlock n wsyn
15302219 popIndent
1531− return x,
1532− do pTerminator
2220+ return x,
2221+ do terminator
15332222 return ([], [])]
1534− return $ PClauseR fc wargs rhs wheres)
2223+ return $ PClauseR fc wargs r wheres)
15352224
15362225 <|> try (do pushIndent
1537− n_in <- pfName; let n = expandNS syn n_in
1538− cargs <- many (pConstraintArg syn)
1539− iargs <- many (pImplicitArg (syn { inPattern = True } ))
1540− fc <- pfc
1541− args <- many (try (pImplicitArg (syn { inPattern = True } ))
1542− <|> (fmap pexp (pArgExpr syn)))
1543− wargs <- many (pWExpr syn)
1544− let capp = PApp fc (PRef fc n)
1545− (iargs ++ cargs ++ args)
1546− ist <- getState
1547− setState (ist { lastParse = Just n })
2226+ n_in <- fnName; let n = expandNS syn n_in
2227+ cargs <- many (constraintArg syn)
2228+ fc <- getFC
2229+ args <- many (try (implicitArg (syn { inPattern = True } ))
2230+ <|> (fmap pexp (argExpr syn)))
2231+ wargs <- many (wExpr syn)
2232+ let capp = PApp fc (PRef fc n)
2233+ (cargs ++ args)
2234+ ist <- get
2235+ put (ist { lastParse = Just n })
15482236 reserved "with"
1549− wval <- pSimpleExpr syn
2237+ wval <- simpleExpr syn
15502238 openBlock
1551− ds <- many1 $ pFunDecl syn
2239+ ds <- some $ fnDecl syn
15522240 let withs = map (fillLHSD n capp wargs) $ concat ds
15532241 closeBlock
15542242 popIndent
15552243 return $ PWith fc n capp wargs wval withs)
15562244
1557− <|> try (do wargs <- many1 (pWExpr syn)
1558− fc <- pfc
2245+ <|> try (do wargs <- some (wExpr syn)
2246+ fc <- getFC
15592247 reserved "with"
1560− wval <- pSimpleExpr syn
2248+ wval <- simpleExpr syn
15612249 openBlock
1562− ds <- many1 $ pFunDecl syn
2250+ ds <- some $ fnDecl syn
15632251 let withs = concat ds
15642252 closeBlock
15652253 return $ PWithR fc wargs wval withs)
1566−
1567− <|> do pushIndent
1568− l <- pArgExpr syn
1569− op <- operator
1570− let n = expandNS syn (UN op)
1571− r <- pArgExpr syn
1572− fc <- pfc
1573− wargs <- many (pWExpr syn)
1574− rhs <- pRHS syn n
1575− let wsyn = syn { syn_namespace = [] }
1576− (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1577− popIndent
1578− return x,
1579− do pTerminator
1580− return ([], [])]
1581− ist <- getState
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
15852254
1586− <|> do l <- pArgExpr syn
2255+ <|> try(do pushIndent
2256+ l <- argExpr syn
2257+ op <- operator
2258+ let n = expandNS syn (UN op)
2259+ r <- argExpr syn
2260+ fc <- getFC
2261+ wargs <- many (wExpr syn)
2262+ rs <- rhs syn n
2263+ let wsyn = syn { syn_namespace = [] }
2264+ (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2265+ popIndent
2266+ return x,
2267+ do terminator
2268+ return ([], [])]
2269+ ist <- get
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)
2273+
2274+ <|> do l <- argExpr syn
15872275 op <- operator
15882276 let n = expandNS syn (UN op)
1589− r <- pArgExpr syn
1590− fc <- pfc
1591− wargs <- many (pWExpr syn)
2277+ r <- argExpr syn
2278+ fc <- getFC
2279+ wargs <- many (wExpr syn)
15922280 reserved "with"
1593− wval <- pSimpleExpr syn
1594− openBlock
1595− ds <- many1 $ pFunDecl syn
2281+ wval <- simpleExpr syn
2282+ openBlock
2283+ ds <- some $ fnDecl syn
15962284 closeBlock
1597− ist <- getState
2285+ ist <- get
15982286 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
15992287 let withs = map (fillLHSD n capp wargs) $ concat ds
1600− setState (ist { lastParse = Just n })
2288+ put (ist { lastParse = Just n })
16012289 return $ PWith fc n capp wargs wval withs
2290+ <?> "function clause"
16022291 where
1603− fillLHS n capp owargs (PClauseR fc wargs v ws)
2292+ fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
2293+ fillLHS n capp owargs (PClauseR fc wargs v ws)
16042294 = PClause fc n capp (owargs ++ wargs) v ws
1605− fillLHS n capp owargs (PWithR fc wargs v ws)
1606− = PWith fc n capp (owargs ++ wargs) v
2295+ fillLHS n capp owargs (PWithR fc wargs v ws)
2296+ = PWith fc n capp (owargs ++ wargs) v
16072297 (map (fillLHSD n capp (owargs ++ wargs)) ws)
16082298 fillLHS _ _ _ c = c
16092299
2300+ fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
16102301 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
16112302 fillLHSD n c a x = x
16122303
1613−pWExpr :: SyntaxInfo -> IParser PTerm
1614−pWExpr syn = do lchar '|'
1615− pExpr' syn
1616−
1617−pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
1618−pWhereblock n syn
1619− = do reserved "where"; openBlock
1620− ds <- many1 $ pDecl syn
2304+{- |Parses with pattern
2305+ WExpr ::= '|' Expr';
2306+-}
2307+wExpr :: SyntaxInfo -> IdrisParser PTerm
2308+wExpr syn = do lchar '|'
2309+ expr' syn
2310+ <?> "with pattern"
2311+
2312+{- |Parses a where block
2313+WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
2314+ -}
2315+whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
2316+whereBlock n syn
2317+ = do reserved "where"
2318+ ds <- indentedBlock1 (decl syn)
16212319 let dns = concatMap (concatMap declared) ds
1622− closeBlock
16232320 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1624−
1625−pCodegen :: IParser Codegen
1626−pCodegen = try (do reserved "C"; return ViaC)
1627− <|> try (do reserved "Java"; return ViaJava)
1628− <|> try (do reserved "JavaScript"; return ViaJavaScript)
1629− <|> try (do reserved "Node"; return ViaNode)
1630− <|> try (do reserved "LLVM"; return ViaLLVM)
1631− <|> try (do reserved "Bytecode"; return Bytecode)
1632−
1633−pDirective :: SyntaxInfo -> IParser [PDecl]
1634−pDirective syn = try (do lchar '%'; reserved "lib"; cgn <- pCodegen; lib <- strlit;
1635− return [PDirective (do addLib cgn lib
1636− addIBC (IBCLib cgn lib))])
1637− <|> try (do lchar '%'; reserved "link"; cgn <- pCodegen; obj <- strlit;
2321+ <?> "where block"
2322+
2323+{- |Parses a code generation target language name
2324+Codegen ::= 'C'
2325+ | 'Java'
2326+ | 'JavaScript'
2327+ | 'Node'
2328+ | 'LLVM'
2329+ | 'Bytecode'
2330+ ;
2331+-}
2332+codegen_ :: IdrisParser Codegen
2333+codegen_ = try (do reserved "C"; return ViaC)
2334+ <|> try (do reserved "Java"; return ViaJava)
2335+ <|> try (do reserved "JavaScript"; return ViaJavaScript)
2336+ <|> try (do reserved "Node"; return ViaNode)
2337+ <|> try (do reserved "LLVM"; return ViaLLVM)
2338+ <|> try (do reserved "Bytecode"; return Bytecode)
2339+ <?> "code generation language"
2340+
2341+{- |Parses a compiler directive
2342+StringList ::=
2343+ String
2344+ | String ',' StringList
2345+ ;
2346+
2347+Directive ::= '%' Directive';
2348+
2349+Directive' ::= 'lib' CodeGen String_t
2350+ | 'link' CodeGen String_t
2351+ | 'flag' CodeGen String_t
2352+ | 'include' CodeGen String_t
2353+ | 'hide' Name
2354+ | 'freeze' Name
2355+ | 'access' Accessibility
2356+ | 'default' Totality
2357+ | 'logging' Natural
2358+ | 'dynamic' StringList
2359+ | 'language' 'TypeProviders'
2360+ ;
2361+-}
2362+directive :: SyntaxInfo -> IdrisParser [PDecl]
2363+directive syn = try (do lchar '%'; reserved "lib"; cgn <- codegen_; lib <- stringLiteral;
2364+ return [PDirective (do addLib cgn lib
2365+ addIBC (IBCLib cgn lib))])
2366+ <|> try (do lchar '%'; reserved "link"; cgn <- codegen_; obj <- stringLiteral;
16382367 return [PDirective (do dirs <- allImportDirs
16392368 o <- liftIO $ findInPath dirs obj
16402369 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
16412370 addObjectFile cgn o)])
1642− <|> try (do lchar '%'; reserved "flag"; cgn <- pCodegen;
1643− flag <- strlit
2371+ <|> try (do lchar '%'; reserved "flag"; cgn <- codegen_;
2372+ flag <- stringLiteral
16442373 return [PDirective (do addIBC (IBCCGFlag cgn flag)
16452374 addFlag cgn flag)])
1646− <|> try (do lchar '%'; reserved "include"; cgn <- pCodegen; hdr <- strlit;
2375+ <|> try (do lchar '%'; reserved "include"; cgn <- codegen_; hdr <- stringLiteral;
16472376 return [PDirective (do addHdr cgn hdr
16482377 addIBC (IBCHeader cgn hdr))])
16492378 <|> try (do lchar '%'; reserved "hide"; n <- iName []
@@ -1652,17 +2381,17 @@ pDirective syn = try (do lchar '%'; reserved "lib"; cgn <- pCodegen; lib <- strl
16522381 <|> try (do lchar '%'; reserved "freeze"; n <- iName []
16532382 return [PDirective (do setAccessibility n Frozen
16542383 addIBC (IBCAccess n Frozen))])
1655− <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'
1656− return [PDirective (do i <- getIState
1657− putIState (i { default_access = acc }))])
1658− <|> try (do lchar '%'; reserved "default"; tot <- pTotality
1659− i <- getState
1660− setState (i { default_total = tot } )
1661− return [PDirective (do i <- getIState
1662− putIState (i { default_total = tot }))])
2384+ <|> try (do lchar '%'; reserved "access"; acc <- accessibility
2385+ return [PDirective (do i <- get
2386+ put(i { default_access = acc }))])
2387+ <|> try (do lchar '%'; reserved "default"; tot <- totality
2388+ i <- get
2389+ put (i { default_total = tot } )
2390+ return [PDirective (do i <- get
2391+ put(i { default_total = tot }))])
16632392 <|> try (do lchar '%'; reserved "logging"; i <- natural;
16642393 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 ',');
16662395 return [PDirective (do added <- addDyLib libs
16672396 case added of
16682397 Left lib -> addIBC (IBCDyLib (lib_name lib))
@@ -1670,78 +2399,132 @@ pDirective syn = try (do lchar '%'; reserved "lib"; cgn <- pCodegen; lib <- strl
16702399 fail $ msg)])
16712400 <|> try (do lchar '%'; reserved "language"; ext <- reserved "TypeProviders";
16722401 return [PDirective (addLangExt TypeProviders)])
2402+ <?> "directive"
16732403
1674−pProvider :: SyntaxInfo -> IParser [PDecl]
1675−pProvider syn = do lchar '%'; reserved "provide";
1676− lchar '('; n <- pfName; t <- pTSig syn; lchar ')'
1677− fc <- pfc
1678− reserved "with"
1679− e <- pExpr syn
1680− return [PProvider syn fc n t e]
2404+{- | Parses a totality
2405+Totality ::= 'partial' | 'total'
2406+-}
2407+totality :: IdrisParser Bool
2408+totality
2409+ = do reserved "total"; return True
2410+ <|> do reserved "partial"; return False
16812411
1682−pTransform :: SyntaxInfo -> IParser [PDecl]
1683−pTransform syn = do lchar '%'; reserved "transform";
2412+{- | Parses a type provider
2413+Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;
2414+ -}
2415+provider :: SyntaxInfo -> IdrisParser [PDecl]
2416+provider syn = do lchar '%'; reserved "provide";
2417+ lchar '('; n <- fnName; t <- typeSig syn; lchar ')'
2418+ fc <- getFC
2419+ reserved "with"
2420+ e <- expr syn
2421+ return [PProvider syn fc n t e]
2422+ <?> "type provider"
2423+
2424+{- | Parses a transform
2425+Transform ::= '%' 'transform' Expr '==>' Expr
2426+-}
2427+transform :: SyntaxInfo -> IdrisParser [PDecl]
2428+transform syn = do lchar '%'; reserved "transform";
16842429 -- leave it unchecked, until we work out what this should
16852430 -- actually mean...
16862431-- safety <- option True (do reserved "unsafe"
16872432-- return False)
1688− lhs <- pExpr syn
1689− fc <- pfc
1690− symbol "==>"
1691− rhs <- pExpr syn
1692− return [PTransform fc False lhs rhs]
1693−
1694−pTactic :: SyntaxInfo -> IParser PTactic
1695−pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
1696− return $ Intro ns
2433+ l <- expr syn
2434+ fc <- getFC
2435+ symbol "==>"
2436+ r <- expr syn
2437+ return [PTransform fc False l r]
2438+ <?> "transform"
2439+
2440+{- | Parses a tactic script
2441+Tactic ::= 'intro' NameList?
2442+ | 'intros'
2443+ | 'refine' Name Imp+
2444+ | 'mrefine' Name
2445+ | 'rewrite' Expr
2446+ | 'equiv' Expr
2447+ | 'let' Name ':' Expr' '=' Expr
2448+ | 'let' Name '=' Expr
2449+ | 'focus' Name
2450+ | 'exact' Expr
2451+ | 'applyTactic' Expr
2452+ | 'reflect' Expr
2453+ | 'fill' Expr
2454+ | 'try' Tactic '|' Tactic
2455+ | '{' TacticSeq '}'
2456+ | 'compute'
2457+ | 'trivial'
2458+ | 'solve'
2459+ | 'attack'
2460+ | 'state'
2461+ | 'term'
2462+ | 'undo'
2463+ | 'qed'
2464+ | 'abandon'
2465+ | ':' 'q'
2466+ ;
2467+
2468+Imp ::= '?' | '_';
2469+
2470+TacticSeq ::=
2471+ Tactic ';' Tactic
2472+ | Tactic ';' TacticSeq
2473+ ;
2474+
2475+-}
2476+
2477+tactic :: SyntaxInfo -> IdrisParser PTactic
2478+tactic syn = do reserved "intro"; ns <- sepBy name (lchar ',')
2479+ return $ Intro ns
16972480 <|> do reserved "intros"; return Intros
1698− <|> try (do reserved "refine"; n <- pName
1699− imps <- many1 imp
2481+ <|> try (do reserved "refine"; n <- name
2482+ imps <- some imp
17002483 return $ Refine n imps)
1701− <|> do reserved "refine"; n <- pName
1702− i <- getState
2484+ <|> do reserved "refine"; n <- name
2485+ i <- get
17032486 return $ Refine n []
1704− <|> do reserved "mrefine"; n <- pName
1705− i <- getState
2487+ <|> do reserved "mrefine"; n <- name
2488+ i <- get
17062489 return $ MatchRefine n
1707− <|> do reserved "rewrite"; t <- pExpr syn;
1708− i <- getState
2490+ <|> do reserved "rewrite"; t <- expr syn;
2491+ i <- get
17092492 return $ Rewrite (desugar syn i t)
1710− <|> do reserved "equiv"; t <- pExpr syn;
1711− i <- getState
2493+ <|> do reserved "equiv"; t <- expr syn;
2494+ i <- get
17122495 return $ Equiv (desugar syn i t)
1713− <|> try (do reserved "let"; n <- pName; lchar ':';
1714− ty <- pExpr' syn; lchar '='; t <- pExpr syn;
1715− i <- getState
2496+ <|> try (do reserved "let"; n <- name; lchar ':';
2497+ ty <- expr' syn; lchar '='; t <- expr syn;
2498+ i <- get
17162499 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
1717− <|> try (do reserved "let"; n <- pName; lchar '=';
1718− t <- pExpr syn;
1719− i <- getState
2500+ <|> try (do reserved "let"; n <- name; lchar '=';
2501+ t <- expr syn;
2502+ i <- get
17202503 return $ LetTac n (desugar syn i t))
1721− <|> do reserved "focus"; n <- pName
2504+ <|> do reserved "focus"; n <- name
17222505 return $ Focus n
1723− <|> do reserved "exact"; t <- pExpr syn;
1724− i <- getState
2506+ <|> do reserved "exact"; t <- expr syn;
2507+ i <- get
17252508 return $ Exact (desugar syn i t)
1726− <|> do reserved "applyTactic"; t <- pExpr syn;
1727− i <- getState
2509+ <|> do reserved "applyTactic"; t <- expr syn;
2510+ i <- get
17282511 return $ ApplyTactic (desugar syn i t)
1729− <|> do reserved "reflect"; t <- pExpr syn;
1730− i <- getState
2512+ <|> do reserved "reflect"; t <- expr syn;
2513+ i <- get
17312514 return $ Reflect (desugar syn i t)
1732− <|> do reserved "fill"; t <- pExpr syn;
1733− i <- getState
2515+ <|> do reserved "fill"; t <- expr syn;
2516+ i <- get
17342517 return $ Fill (desugar syn i t)
1735− <|> do reserved "try"; t <- pTactic syn;
2518+ <|> do reserved "try"; t <- tactic syn;
17362519 lchar '|';
1737− t1 <- pTactic syn
2520+ t1 <- tactic syn
17382521 return $ Try t t1
17392522 <|> do lchar '{'
1740− t <- pTactic syn;
2523+ t <- tactic syn;
17412524 lchar ';';
1742− t1 <- pTactic syn;
2525+ ts <- sepBy1 (tactic syn) (lchar ';')
17432526 lchar '}'
1744− return $ TSeq t t1
2527+ return $ TSeq t (mergeSeq ts)
17452528 <|> do reserved "compute"; return Compute
17462529 <|> do reserved "trivial"; return Trivial
17472530 <|> do reserved "solve"; return Solve
@@ -1752,7 +2535,229 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
17522535 <|> do reserved "qed"; return Qed
17532536 <|> do reserved "abandon"; return Abandon
17542537 <|> do lchar ':'; reserved "q"; return Abandon
2538+ <?> "tactic"
17552539 where
2540+ imp :: IdrisParser Bool
17562541 imp = do lchar '?'; return False
17572542 <|> do lchar '_'; return True
2543+ mergeSeq :: [PTactic] -> PTactic
2544+ mergeSeq [t] = t
2545+ mergeSeq (t:ts) = TSeq t (mergeSeq ts)
2546+
2547+{- | Parses a tactic as a whole -}
2548+fullTactic :: SyntaxInfo -> IdrisParser PTactic
2549+fullTactic syn = do t <- tactic syn
2550+ eof
2551+ return t
2552+
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)
2557+
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)
2561+
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
2569+ -- none anyway)
2570+ return x
2571+ where imports :: IdrisParser (([String], [String], Delta), IState)
2572+ imports = do whiteSpace
2573+ mname <- moduleHeader
2574+ ps <- many import_
2575+ mrk <- mark
2576+ i <- get
2577+ return ((mname, ps, mrk), i)
2578+
2579+
2580+-- | A program is a list of declarations, possibly with associated
2581+-- documentation strings.
2582+parseProg :: SyntaxInfo -> FilePath -> String -> Delta ->
2583+ Idris [PDecl]
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)
2590+ i <- getIState
2591+ putIState (i { errLine = Just 0 }) -- Just errl })
2592+ return []
2593+ Success (x, i) -> do putIState i
2594+ return $ collect x
2595+ where mainProg :: IdrisParser ([PDecl], IState)
2596+ mainProg = do release mrk
2597+ ds <- prog syn
2598+ i' <- get
2599+ return (ds, i')
2600+
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 [] = []
2613+
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
2629+collect [] = []
2630+
2631+{- | Load idris module -}
2632+loadModule :: FilePath -> Idris String
2633+loadModule f
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 })
2642+ case fp of
2643+ IDR fn -> loadSource False fn
2644+ LIDR fn -> loadSource True fn
2645+ IBC fn src ->
2646+ idrisCatch (loadIBC fn)
2647+ (\c -> do iLOG $ fn ++ " failed " ++ show c
2648+ case src of
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)
2655+ iputStrLn msg
2656+ return "")
2657+
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)
2664+ where
2665+ getSrcFile (IDR fn) = fn
2666+ getSrcFile (LIDR fn) = fn
2667+ getSrcFile (IBC f src) = getSrcFile src
2668+
2669+loadFromIFile (IDR fn) = loadSource' False fn
2670+loadFromIFile (LIDR fn) = loadSource' True fn
2671+
2672+{-| Load idris source code and show error if something wrong happens -}
2673+loadSource' :: Bool -> FilePath -> Idris ()
2674+loadSource' lidr r
2675+ = idrisCatch (loadSource lidr r)
2676+ (\e -> do let msg = show e
2677+ setErrLine (getErrLine msg)
2678+ iputStrLn msg)
2679+
2680+{- | Load Idris source code-}
2681+loadSource :: Bool -> FilePath -> Idris ()
2682+loadSource lidr f
2683+ = do iLOG ("Reading " ++ f)
2684+ i <- getIState
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
2689+ i <- getIState
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 })
2694+ f file pos
2695+ unless (null ds') $ do
2696+ let ds = namespaces mname ds'
2697+ logLvl 3 (dumpDecls ds)
2698+ i <- getIState
2699+ logLvl 10 (show (toAlist (idris_implicits i)))
2700+ logLvl 3 (show (idris_infixes i))
2701+ -- Now add all the declarations to the context
2702+ v <- verbose
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)
2708+ i <- getIState
2709+ -- simplify every definition do give the totality checker
2710+ -- a better chance
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"
2716+ i <- getIState
2717+ mapM_ buildSCG (idris_totcheck i)
2718+ mapM_ checkDeclTotality (idris_totcheck i)
2719+ iLOG ("Finished " ++ f)
2720+ ibcsd <- valIBCSubDir i
2721+ iLOG "Universe checking"
2722+ iucheck
2723+ let ibc = ibcPathNoFallback ibcsd f
2724+ i <- getIState
2725+ addHides (hide_list i)
2726+ ok <- noErrors
2727+ when ok $
2728+ idrisCatch (do writeIBC f ibc; clearIBC)
2729+ (\c -> return ()) -- failure is harmless
2730+ i <- getIState
2731+ putIState (i { default_total = def_total,
2732+ hide_list = [] })
2733+ return ()
2734+ return ()
2735+ where
2736+ namespaces :: [String] -> [PDecl] -> [PDecl]
2737+ namespaces [] ds = ds
2738+ namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
2739+
2740+ toMutual :: PDecl -> PDecl
2741+ toMutual m@(PMutual _ d) = m
2742+ toMutual x = let r = PMutual (FC "single mutual" 0) [x] in
2743+ case x of
2744+ PClauses _ _ _ _ -> r
2745+ PClass _ _ _ _ _ _ _ -> r
2746+ PInstance _ _ _ _ _ _ _ _ -> r
2747+ _ -> x
2748+
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
2754+ unless (null as) $
2755+ mapM_ doHide
2756+ (map (\ (n, _) -> (n, defh)) hs ++
2757+ map (\ (n, Just a) -> (n, a)) as)
2758+ where isNothing (_, Nothing) = True
2759+ isNothing _ = False
2760+
2761+ doHide (n, a) = do setAccessibility n a
2762+ addIBC (IBCAccess n a)
17582763