b85965e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

parser tinkering

commitb85965ef36165118d0f6558c3c7d0b05be7ff487 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 26 Oct 2011, 17:09 (15 years ago) parent1155e79

2 files changed+12−11

compare with master

unifiedsplit

src/Core/ProofState.hs+1 src/Idris/Parser.hs+11−11

src/Core/ProofState.hs+1

@@ -140,6 +140,7 @@ goal h tm = g [] tm where

140140 gb env (Let t v) = g env t `mplus` g env v

141141 gb env (Guess t v) = g env t `mplus` g env v

142142 gb env t = g env (binderTy t)

143+

143144tactic :: Hole -> RunTactic -> StateT TState TC ()

144145tactic h f = do ps <- get

145146 tm' <- atH (context ps) [] (pterm ps)

src/Idris/Parser.hs+11−11

@@ -274,8 +274,8 @@ pExpr' syn

274274pNoExtExpr syn =

275275 try (pApp syn)

276276 <|> pSimpleExpr syn

277− <|> try (pLambda syn)

278− <|> try (pLet syn)

277+ <|> pLambda syn

278+ <|> pLet syn

279279 <|> pPi syn

280280 <|> pDoBlock syn

281281

@@ -325,9 +325,9 @@ pfName = try pName

325325pSimpleExpr syn =

326326 try (do symbol "!["; t <- pTerm; lchar ']'

327327 return $ PQuote t)

328− <|> try (do lchar '?'; x <- pName; return (PMetavar x))

329− <|> try (do reserved "refl"; fc <- pfc; return (PRefl fc))

330− <|> try (do reserved "return"; fc <- pfc; return (PReturn fc))

328+ <|> do lchar '?'; x <- pName; return (PMetavar x)

329+ <|> do reserved "refl"; fc <- pfc; return (PRefl fc)

330+ <|> do reserved "return"; fc <- pfc; return (PReturn fc)

331331 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))

332332 <|> try (pPair syn)

333333 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)

@@ -346,10 +346,10 @@ pPair syn = do lchar '('; l <- pExpr syn; op <- pairOp

346346 <|> do reservedOp "**"; return PDPair

347347

348348pHSimpleExpr syn

349− = try (pSimpleExpr syn)

350− <|> do lchar '.'

349+ = do lchar '.'

351350 e <- pSimpleExpr syn

352351 return $ PHidden e

352+ <|> pSimpleExpr syn

353353

354354pApp syn = do f <- pSimpleExpr syn

355355 fc <- pfc

@@ -408,12 +408,12 @@ pDoBlock syn

408408 return (PDoBlock ds)

409409

410410pDo syn

411− = try (do i <- pName; symbol "<-"; fc <- pfc

411+ = do reserved "let"; i <- pName; reservedOp "="; fc <- pfc

412+ e <- pExpr syn

413+ return (DoLet fc i e)

414+ <|> try (do i <- pName; symbol "<-"; fc <- pfc

412415 e <- pExpr syn;

413416 return (DoBind fc i e))

414− <|> try (do reserved "let"; i <- pName; reservedOp "="; fc <- pfc

415− e <- pExpr syn

416− return (DoLet fc i e))

417417 <|> try (do e <- pExpr syn; fc <- pfc

418418 return (DoExp fc e))

419419