Skip to content

Instantly share code, notes, and snippets.

@osa1

osa1/gist:9217729

Created February 25, 2014 21:05
Show Gist options
  • Save osa1/9217729 to your computer and use it in GitHub Desktop.
Save osa1/9217729 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.diff
--- idris-0.9.8/src/Idris/Parser.hs 2014-02-14 04:30:09.058010954 +0200
+++ idris-0.9.8-indentation/src/Idris/Parser.hs 2014-02-25 16:52:21.678150163 +0200
@@ -35,9 +35,13 @@
import Data.Maybe
import System.FilePath
-type TokenParser a = PTok.TokenParser a
+import Text.Parsec.Indentation
+import Text.Parsec.Indentation.Char
-type IParser = GenParser Char IState
+import Control.Monad.Identity
+
+type TokenParser a = PTok.GenTokenParser (IndentStream (CharIndentStream String)) a Identity
+type IParser = Parsec (IndentStream (CharIndentStream [Char])) IState
lexer :: TokenParser IState
lexer = idrisLexer
@@ -165,15 +169,15 @@
eof
return t) i "(proof)"
-parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)
+parseImports :: FilePath -> String -> Idris ([String], [String], IndentStream (CharIndentStream String), SourcePos)
parseImports fname input
= do i <- getIState
case runParser (do whiteSpace
- mname <- pHeader
- ps <- many pImport
+ mname <- absoluteIndentation pHeader
+ ps <- liftM concat $ many (absoluteIndentation $ semiSepNE pImport)
rest <- getInput
pos <- getPosition
- return ((mname, ps, rest, pos), i)) i fname input of
+ return ((mname, ps, rest, pos), i)) i fname (mkIndentStream 1 1 False Gt (mkCharIndentStream input)) of
Left err -> fail (show err)
Right (x, i) -> do putIState i
return x
@@ -186,83 +190,41 @@
(x, "") -> [x]
(x, '.':y) -> x : parseName y
-pushIndent :: IParser ()
-pushIndent = do pos <- getPosition
- ist <- getState
- setState (ist { indent_stack = sourceColumn pos :
- indent_stack ist })
-lastIndent :: IParser Int
-lastIndent = do ist <- getState
- case indent_stack ist of
- (x : xs) -> return x
- _ -> return 1
-
-indent :: IParser Int
-indent = liftM sourceColumn getPosition
-
-popIndent :: IParser ()
-popIndent = do ist <- getState
- let (x : xs) = indent_stack ist
- setState (ist { indent_stack = xs })
-openBlock :: IParser ()
-openBlock = do lchar '{'
- ist <- getState
- setState (ist { brace_stack = Nothing : brace_stack ist })
- <|> do ist <- getState
- lvl <- indent
- setState (ist { brace_stack = Just lvl : brace_stack ist })
-
-closeBlock :: IParser ()
-closeBlock = do ist <- getState
- bs <- case brace_stack ist of
- [] -> eof >> return []
- Nothing : xs -> (lchar '}' >> return xs) <|> (eof >> return [])
- Just lvl : xs -> (do i <- indent
- inp <- getInput
--- trace (show (take 10 inp, i, lvl)) $
- if i >= lvl && take 1 inp /= ")"
- then fail "Not end of block"
- else return xs) <|> (eof >> return [])
- setState (ist { brace_stack = bs })
-
-pTerminator = do lchar ';'; popIndent
- <|> do c <- indent; l <- lastIndent
- if c <= l
- then popIndent
- else fail "Not a terminator"
- <|> do i <- getInput
- if "}" `isPrefixOf` i || ")" `isPrefixOf` i
- then popIndent
- else fail "Not a terminator"
- <|> lookAhead eof
-
-pBarTerminator
- = do lchar '|'; return ()
- <|> do c <- indent; l <- lastIndent
- unless (c <= l) $ fail "Not a terminator"
- <|> lookAhead eof
-
-pKeepTerminator
- = do lchar ';'; return ()
- <|> do c <- indent; l <- lastIndent
- unless (c <= l) $ fail "Not a terminator"
- <|> do i <- getInput
- let h = take 1 i
- unless (h `elem` ["}", ")", "|"]) $ fail "Not a terminator"
- <|> lookAhead eof
-
-notEndApp = do c <- indent; l <- lastIndent
- i <- getInput
- when (c <= l) $ fail "Terminator"
-
-notEndBlock = do ist <- getState
- case brace_stack ist of
- Just lvl : xs -> do i <- indent
- inp <- getInput
- when (i < lvl || ")" `isPrefixOf` inp) $ fail "End of block"
- _ -> return ()
+pBlock p =
+ between (lchar '{') (pClose) (localIndentation (Const 0) (semiSep p))
+ <|> (liftM concat $ localIndentation Gt $ many $ absoluteIndentation $ semiSepNE p)
+
+pBlock1 p =
+ between (lchar '{') (pClose) (localIndentation (Const 0) (semiSep1 p))
+ <|> (liftM concat $ localIndentation Gt $ many1 $ absoluteIndentation $ semiSepNE p)
+pBlockS p = between (lchar '{') (pClose) (localIndentation (Const 0) (optionTerm p))
+ <|> (localIndentation Gt $ absoluteIndentation (optionTerm p))
+pBlock1' p = -- this may be a bug in the original
+ between (lchar '{') (pClose) (liftM concat $ localIndentation Any $ many1 $ absoluteIndentation $ semiSepNE p)
+ <|> (liftM concat $ localIndentation Gt $ many1 $ absoluteIndentation $ semiSep1 p)
+
+pClose = localTokenMode (const Ge) (lchar '}')
+
+semiSep1 p = many (lchar ';') >> semiSep0 p
+semiSep p = many (lchar ';') >> option [] (semiSep0 p)
+
+semiSep0 p = liftM reverse $ go [] where
+ go xs = p >>= \x -> let opt = option (x : xs)
+ in opt (many1 (lchar ';') >> opt (go (x : xs)))
+
+semiSepNE p = liftM reverse $ go [] where
+ go' xs = option xs (go xs)
+ go xs = (lchar ';' >> go' xs)
+ <|> (p >>= \x -> option (x:xs) (lchar ';' >> go' (x : xs)))
+
+
+optionTerm p = do x <- p
+ option ';' (lchar ';')
+ return x
+
+docIndentation x = x
-- | Use Parsec's internal state to construct a source code position
pfc :: IParser FC
@@ -278,14 +240,14 @@
-- | A program is a list of declarations, possibly with associated
-- documentation strings.
-parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos ->
+parseProg :: SyntaxInfo -> FilePath -> IndentStream (CharIndentStream String) -> SourcePos ->
Idris [PDecl]
parseProg syn fname input pos
= do i <- getIState
case runParser (do setPosition pos
whiteSpace
- ps <- many (pDecl syn)
- eof
+ ps <- liftM concat $ many (absoluteIndentation $ semiSepNE $ pDecl syn)
+ localTokenMode (const Any) eof
i' <- getState
return (concat ps, i')) i fname input of
Left err -> do iputStrLn (show err)
@@ -329,10 +291,8 @@
-- | Parse a top-level declaration
pDecl :: SyntaxInfo -> IParser [PDecl]
-pDecl syn = do notEndBlock
- pDeclBody where
- pDeclBody
- = do d <- pDecl' syn
+pDecl syn = do
+ d <- pDecl' syn
i <- getState
let d' = fmap (desugar syn i) d
return [d']
@@ -350,8 +310,7 @@
pFunDecl :: SyntaxInfo -> IParser [PDecl]
pFunDecl syn
- = try (do notEndBlock
- d <- pFunDecl' syn
+ = try (do d <- pFunDecl' syn
i <- getState
let d' = fmap (desugar syn i) d
return [d'])
@@ -387,8 +346,7 @@
pSyntaxRule :: SyntaxInfo -> IParser Syntax
pSyntaxRule syn
- = do pushIndent
- sty <- option AnySyntax (do reserved "term"; return TermSyntax
+ = do sty <- option AnySyntax (do reserved "term"; return TermSyntax
<|> do reserved "pattern"; return PatternSyntax)
reserved "syntax"
syms <- many1 pSynSym
@@ -398,7 +356,6 @@
$ fail "Repeated variable in syntax rule"
lchar '='
tm <- pTExpr (impOK syn)
- pTerminator
return (Rule (mkSimple syms) tm sty)
where
expr (Expr _) = True
@@ -428,20 +385,18 @@
return (Symbol sym)
pFunDecl' :: SyntaxInfo -> IParser PDecl
-pFunDecl' syn = try (do doc <- option "" (pDocComment '|')
- pushIndent
+pFunDecl' syn = try (do doc <- docIndentation $ option "" (pDocComment '|')
ist <- getState
let initOpts = if default_total ist
then [TotalFn]
else []
opts <- pFnOpts initOpts
- acc <- pAccessibility
- opts' <- pFnOpts opts
- n_in <- pfName
+ acc <- localTokenMode (const Ge) $ pAccessibility
+ opts' <- localTokenMode (const Ge) $ pFnOpts opts
+ n_in <- localTokenMode (const Ge) pfName
let n = expandNS syn n_in
fc <- pfc
ty <- pTSig (impOK syn)
- pTerminator
-- ty' <- implicit syn n ty
addAcc n acc
return (PTy doc syn fc opts' n ty))
@@ -450,21 +405,19 @@
<|> try (pCAF syn)
pPostulate :: SyntaxInfo -> IParser PDecl
-pPostulate syn = do doc <- option "" (pDocComment '|')
- pushIndent
+pPostulate syn = do doc <- docIndentation $ option "" (pDocComment '|')
reserved "postulate"
ist <- getState
let initOpts = if default_total ist
then [TotalFn]
else []
opts <- pFnOpts initOpts
- acc <- pAccessibility
- opts' <- pFnOpts opts
- n_in <- pfName
+ acc <- localTokenMode (const Ge) $ pAccessibility
+ opts' <- localTokenMode (const Ge) $ pFnOpts opts
+ n_in <- localTokenMode (const Ge) pfName
let n = expandNS syn n_in
ty <- pTSig (impOK syn)
fc <- pfc
- pTerminator
addAcc n acc
return (PPostulate doc syn fc opts' n ty)
@@ -472,46 +425,35 @@
pUsing :: SyntaxInfo -> IParser [PDecl]
pUsing syn =
do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
- openBlock
let uvars = using syn
- ds <- many1 (pDecl (syn { using = uvars ++ ns }))
- closeBlock
+ ds <- pBlock1 (pDecl (syn { using = uvars ++ ns }))
return (concat ds)
pParams :: SyntaxInfo -> IParser [PDecl]
pParams syn =
do reserved "parameters"; lchar '('; ns <- tyDeclList syn; lchar ')'
- openBlock
let pvars = syn_params syn
- ds <- many1 (pDecl syn { syn_params = pvars ++ ns })
- closeBlock
+ ds <- pBlock1 (pDecl syn { syn_params = pvars ++ ns })
fc <- pfc
return [PParams fc ns (concat ds)]
pMutual :: SyntaxInfo -> IParser [PDecl]
pMutual syn =
do reserved "mutual"
- openBlock
- let pvars = syn_params syn
- ds <- many1 (pDecl syn)
- closeBlock
+ ds <- pBlock1 (pDecl syn)
fc <- pfc
return [PMutual fc (concat ds)]
pNamespace :: SyntaxInfo -> IParser [PDecl]
pNamespace syn =
do reserved "namespace"; n <- identifier;
- openBlock
- ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
- closeBlock
+ ds <- pBlock1' (pDecl syn { syn_namespace = n : syn_namespace syn })
return [PNamespace n (concat ds)]
--------- Fixity ---------
pFixity :: IParser PDecl
-pFixity = do pushIndent
- f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
- pTerminator
+pFixity = do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
let prec = fromInteger i
istate <- getState
let infixes = idris_infixes istate
@@ -546,12 +488,11 @@
pClass :: SyntaxInfo -> IParser [PDecl]
pClass syn = do doc <- option "" (pDocComment '|')
acc <- pAccessibility
- reserved "class"; fc <- pfc; cons <- pConstList syn; n_in <- pName
+ localTokenMode (const Ge) (reserved "class"); fc <- pfc; cons <- pConstList syn; n_in <- pName
let n = expandNS syn n_in
cs <- many carg
- reserved "where"; openBlock
- ds <- many $ pFunDecl syn
- closeBlock
+ reserved "where"
+ ds <- pBlock (pFunDecl syn)
let allDs = concat ds
accData acc n (concatMap declared allDs)
return [PClass doc syn fc cons n cs allDs]
@@ -572,9 +513,8 @@
args <- many (pSimpleExpr syn)
let sc = PApp fc (PRef fc cn) (map pexp args)
let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
- reserved "where"; openBlock
- ds <- many $ pFunDecl syn
- closeBlock
+ reserved "where"
+ ds <- pBlock (pFunDecl syn)
return [PInstance syn fc cs cn args t en (concat ds)]
--------- Expressions ---------
@@ -720,28 +660,22 @@
addAcc n a = do i <- getState
setState (i { hide_list = (n, a) : hide_list i })
+
pCaseExpr syn = do
reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
- openBlock
- pushIndent
- opts <- many1 (do notEndBlock
- x <- pCaseOpt syn
- pKeepTerminator
- return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
- popIndent
- closeBlock
+ opts <- pBlock1 (pCaseOpt syn)
return (PCase fc scr opts)
pProofExpr syn = do
reserved "proof"; lchar '{'
ts <- endBy (pTactic syn) (lchar ';')
- lchar '}'
+ pClose
return (PProof ts)
pTacticsExpr syn = do
reserved "tactics"; lchar '{'
ts <- endBy (pTactic syn) (lchar ';')
- lchar '}'
+ pClose
return (PTactics ts)
pSimpleExpr syn =
@@ -876,8 +810,7 @@
pApp syn = do f <- pSimpleExpr syn
fc <- pfc
- args <- many1 (do notEndApp
- pArg syn)
+ args <- many1 (pArg syn)
i <- getState
return (dslify i $ PApp fc f args)
where
@@ -1078,14 +1011,7 @@
pDoBlock syn
= do reserved "do"
- openBlock
- pushIndent
- ds <- many1 (do notEndBlock
- x <- pDo syn
- pKeepTerminator
- return x)
- popIndent
- closeBlock
+ ds <- pBlock1 (pDo syn)
return (PDoBlock ds)
pDo syn
@@ -1189,18 +1115,13 @@
pRecord :: SyntaxInfo -> IParser PDecl
pRecord syn = do doc <- option "" (pDocComment '|')
acc <- pAccessibility
- reserved "record"
+ localTokenMode (const Ge) (reserved "record")
fc <- pfc
tyn_in <- pfName
ty <- pTSig (impOK syn)
let tyn = expandNS syn tyn_in
reserved "where"
- openBlock
- pushIndent
- (cdoc, cn, cty, _) <- pConstructor syn
- pKeepTerminator
- popIndent
- closeBlock
+ (cdoc, cn, cty, _) <- pBlockS (pConstructor syn)
accData acc tyn [cn]
let rsyn = syn { syn_namespace = show (nsroot tyn) :
syn_namespace syn }
@@ -1221,27 +1142,19 @@
pData :: SyntaxInfo -> IParser PDecl
pData syn = try (do doc <- option "" (pDocComment '|')
acc <- pAccessibility
- co <- pDataI
+ co <- localTokenMode (const Ge) pDataI
fc <- pfc
tyn_in <- pfName
ty <- pTSig (impOK syn)
let tyn = expandNS syn tyn_in
option (PData doc syn fc co (PLaterdecl tyn ty)) (do
reserved "where"
- openBlock
- pushIndent
- cons <- many (do notEndBlock
- c <- pConstructor syn
- pKeepTerminator
- return c) -- (lchar '|')
- popIndent
- closeBlock
+ cons <- pBlock (pConstructor syn)
accData acc tyn (map (\ (_, n, _, _) -> n) cons)
return $ PData doc syn fc co (PDatadecl tyn ty cons)))
- <|> try (do doc <- option "" (pDocComment '|')
- pushIndent
+ <|> try (do doc <- docIndentation $ option "" (pDocComment '|')
acc <- pAccessibility
- co <- pDataI
+ co <- localTokenMode (const Ge) pDataI
fc <- pfc
tyn_in <- pfName
args <- many pName
@@ -1261,7 +1174,6 @@
fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
cons <- sepBy1 (pSimpleCon syn) (lchar '|')
- pTerminator
let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
cons' <- mapM (\ (doc, x, cargs, cfc) ->
do let cty = bindArgs cargs conty
@@ -1290,8 +1202,7 @@
= do cn_in <- pfName
let cn = expandNS syn cn_in
fc <- pfc
- args <- many (do notEndApp
- pSimpleExpr syn)
+ args <- many (do pSimpleExpr syn)
doc <- option "" (pDocComment '^')
return (doc, cn, args, fc)
@@ -1300,13 +1211,7 @@
pDSL :: SyntaxInfo -> IParser PDecl
pDSL syn = do reserved "dsl"
n <- pfName
- openBlock
- pushIndent
- bs <- many1 (do notEndBlock
- b <- pOverload syn
- pKeepTerminator
- return b)
- popIndent; closeBlock
+ bs <- pBlock1 (pOverload syn)
let dsl = mkDSL bs (dsl_info syn)
checkDSL dsl
i <- getState
@@ -1349,7 +1254,6 @@
n_in <- pfName; let n = expandNS syn n_in
lchar '='
t <- pExpr syn
- pTerminator
fc <- pfc
return (PCAF fc n t)
@@ -1372,8 +1276,7 @@
pClause :: SyntaxInfo -> IParser PClause
pClause syn
- = try (do pushIndent
- n_in <- pfName; let n = expandNS syn n_in
+ = try (do n_in <- pfName; let n = expandNS syn n_in
cargs <- many (pConstraintArg syn)
iargs <- many (pImplicitArg (syn { inPattern = True } ))
fc <- pfc
@@ -1384,18 +1287,14 @@
ist <- getState
let ctxt = tt_ctxt ist
let wsyn = syn { syn_namespace = [] }
- (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
- popIndent
- return x,
- do pTerminator
+ (wheres, nmap) <- choice [pWhereblock n wsyn,
return ([], [])]
let capp = PApp fc (PRef fc n)
(iargs ++ cargs ++ args)
ist <- getState
setState (ist { lastParse = Just n })
return $ PClause fc n capp wargs rhs wheres)
- <|> try (do pushIndent
- wargs <- many1 (pWExpr syn)
+ <|> try (do wargs <- many1 (pWExpr syn)
ist <- getState
n <- case lastParse ist of
Just t -> return t
@@ -1404,15 +1303,11 @@
rhs <- pRHS syn n
let ctxt = tt_ctxt ist
let wsyn = syn { syn_namespace = [] }
- (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
- popIndent
- return x,
- do pTerminator
+ (wheres, nmap) <- choice [pWhereblock n wsyn,
return ([], [])]
return $ PClauseR fc wargs rhs wheres)
- <|> try (do pushIndent
- n_in <- pfName; let n = expandNS syn n_in
+ <|> try (do n_in <- pfName; let n = expandNS syn n_in
cargs <- many (pConstraintArg syn)
iargs <- many (pImplicitArg (syn { inPattern = True } ))
fc <- pfc
@@ -1425,25 +1320,19 @@
setState (ist { lastParse = Just n })
reserved "with"
wval <- pSimpleExpr syn
- openBlock
- ds <- many1 $ pFunDecl syn
+ ds <- pBlock1 (pFunDecl syn)
let withs = map (fillLHSD n capp wargs) $ concat ds
- closeBlock
- popIndent
return $ PWith fc n capp wargs wval withs)
<|> try (do wargs <- many1 (pWExpr syn)
fc <- pfc
reserved "with"
wval <- pSimpleExpr syn
- openBlock
- ds <- many1 $ pFunDecl syn
+ ds <- pBlock1 (pFunDecl syn)
let withs = concat ds
- closeBlock
return $ PWithR fc wargs wval withs)
- <|> do pushIndent
- l <- pArgExpr syn
+ <|> do l <- pArgExpr syn
op <- operator
let n = expandNS syn (UN op)
r <- pArgExpr syn
@@ -1451,10 +1340,7 @@
wargs <- many (pWExpr syn)
rhs <- pRHS syn n
let wsyn = syn { syn_namespace = [] }
- (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
- popIndent
- return x,
- do pTerminator
+ (wheres, nmap) <- choice [pWhereblock n wsyn,
return ([], [])]
ist <- getState
let capp = PApp fc (PRef fc n) [pexp l, pexp r]
@@ -1469,9 +1355,7 @@
wargs <- many (pWExpr syn)
reserved "with"
wval <- pSimpleExpr syn
- openBlock
- ds <- many1 $ pFunDecl syn
- closeBlock
+ ds <- pBlock1 (pFunDecl syn)
ist <- getState
let capp = PApp fc (PRef fc n) [pexp l, pexp r]
let withs = map (fillLHSD n capp wargs) $ concat ds
@@ -1494,10 +1378,9 @@
pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
pWhereblock n syn
- = do reserved "where"; openBlock
- ds <- many1 $ pDecl syn
+ = do reserved "where"
+ ds <- pBlock1 (pDecl syn)
let dns = concatMap (concatMap declared) ds
- closeBlock
return (concat ds, map (\x -> (x, decoration syn x)) dns)
pDirective :: SyntaxInfo -> IParser [PDecl]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment