8996abf · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Parse to line now reads whole definition

Instead of stopping at the first declaration after it reaches the line it wants, stop at the first non-pattern-match, so that it still reads the entire definition to avoid strange totality errors. This mostly helps the vim mode, and :addmissing.

commit8996abfa8e5a27155f8e1dd93001e3b5009a058b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 16 Oct 2015, 23:22 (11 years ago) parentc98e24f

2 files changed+29−13

compare with master

unifiedsplit

src/Idris/Parser.hs+28−12 src/Idris/REPL.hs+1−1

src/Idris/Parser.hs+28−12

@@ -153,7 +153,7 @@ import_ = do fc <- getFC

153153prog :: SyntaxInfo -> IdrisParser [PDecl]

154154prog syn = do whiteSpace

155155 decls <- many (decl syn)

156− let c = (concat decls)

156+ let c = concat decls

157157 case maxline syn of

158158 Nothing -> do notOpenBraces; eof

159159 _ -> return ()

@@ -191,17 +191,27 @@ decl syn = try (externalDecl syn)

191191internalDecl :: SyntaxInfo -> IdrisParser [PDecl]

192192internalDecl syn

193193 = do fc <- getFC

194− -- if we're after maxline, stop here

194+ -- if we're after maxline, stop at the next type declaration

195+ -- (so we get all cases of a definition to preserve totality

196+ -- results, in particular).

195197 let continue = case maxline syn of

196198 Nothing -> True

197199 Just l -> if fst (fc_end fc) > l

198200 then mut_nesting syn /= 0

199201 else True

200− if continue then do notEndBlock

201− declBody

202− else fail "End of readable input"

203− where declBody :: IdrisParser [PDecl]

204− declBody = declBody'

202+ -- What I'd really like to do here is explicitly save the

203+ -- current state, then if reading ahead finds we've passed

204+ -- the end of the definition, reset the state. But I've lost

205+ -- patience with trying to find out how to do that from the

206+ -- trifecta docs, so this does the job instead.

207+ if continue then

208+ do notEndBlock

209+ declBody continue

210+ else try (do notEndBlock

211+ declBody continue)

212+ <|> fail "End of readable input"

213+ where declBody :: Bool -> IdrisParser [PDecl]

214+ declBody b = declBody' b

205215 <|> using_ syn

206216 <|> params syn

207217 <|> mutual syn

@@ -214,11 +224,17 @@ internalDecl syn

214224 <|> transform syn

215225 <|> do import_; fail "imports must be at top of file"

216226 <?> "declaration"

217− declBody' :: IdrisParser [PDecl]

218− declBody' = do d <- decl' syn

219− i <- get

220− let d' = fmap (debindApp syn . (desugar syn i)) d

221− return [d']

227+ declBody' :: Bool -> IdrisParser [PDecl]

228+ declBody' cont = do d <- decl' syn

229+ i <- get

230+ let d' = fmap (debindApp syn . (desugar syn i)) d

231+ if continue cont d'

232+ then return [d']

233+ else fail "End of readable input"

234+

235+ -- Keep going while we're still parsing clauses

236+ continue False (PClauses _ _ _ _) = True

237+ continue c _ = c

222238

223239{- | Parses a top-level declaration with possible syntax sugar

224240

src/Idris/REPL.hs+1−1

@@ -1227,7 +1227,7 @@ process fn (Missing n)

12271227 = do i <- getIState

12281228 ppOpts <- fmap ppOptionIst getIState

12291229 case lookupCtxt n (idris_patdefs i) of

1230− [] -> iPrintError $ "Unknown operator " ++ show n

1230+ [] -> iPrintError $ "Unknown name " ++ show n

12311231 [(_, tms)] ->

12321232 iRenderResult (vsep (map (pprintPTerm ppOpts {ppopt_impl = True}

12331233 []