git.iko.soy/Idris-dev
on master help sign in
parser tinkering
b85965eEdwin Brady
src/Core/ProofState.hs+1
compare with master
unifiedsplit
@@ -140,6 +140,7 @@ goal h tm = g [] tm where
140 gb env (Let t v) = g env t `mplus` g env v
140 gb env (Let t v) = g env t `mplus` g env v
141 gb env (Guess t v) = g env t `mplus` g env v
141 gb env (Guess t v) = g env t `mplus` g env v
142 gb env t = g env (binderTy t)
142 gb env t = g env (binderTy t)
143+
143tactic :: Hole -> RunTactic -> StateT TState TC ()
144tactic :: Hole -> RunTactic -> StateT TState TC ()
144tactic h f = do ps <- get
145tactic h f = do ps <- get
145 tm' <- atH (context ps) [] (pterm ps)
146 tm' <- atH (context ps) [] (pterm ps)
src/Idris/Parser.hs+11−11
@@ -274,8 +274,8 @@ pExpr' syn
274pNoExtExpr syn =
274pNoExtExpr syn =
275 try (pApp syn)
275 try (pApp syn)
276 <|> pSimpleExpr syn
276 <|> pSimpleExpr syn
277− <|> try (pLambda syn)
277+ <|> pLambda syn
278− <|> try (pLet syn)
278+ <|> pLet syn
279 <|> pPi syn
279 <|> pPi syn
280 <|> pDoBlock syn
280 <|> pDoBlock syn
281
281
@@ -325,9 +325,9 @@ pfName = try pName
325pSimpleExpr syn =
325pSimpleExpr syn =
326 try (do symbol "!["; t <- pTerm; lchar ']'
326 try (do symbol "!["; t <- pTerm; lchar ']'
327 return $ PQuote t)
327 return $ PQuote t)
328− <|> try (do lchar '?'; x <- pName; return (PMetavar x))
328+ <|> do lchar '?'; x <- pName; return (PMetavar x)
329− <|> try (do reserved "refl"; fc <- pfc; return (PRefl fc))
329+ <|> do reserved "refl"; fc <- pfc; return (PRefl fc)
330− <|> try (do reserved "return"; fc <- pfc; return (PReturn fc))
330+ <|> do reserved "return"; fc <- pfc; return (PReturn fc)
331 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))
331 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))
332 <|> try (pPair syn)
332 <|> try (pPair syn)
333 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)
333 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)
@@ -346,10 +346,10 @@ pPair syn = do lchar '('; l <- pExpr syn; op <- pairOp
346 <|> do reservedOp "**"; return PDPair
346 <|> do reservedOp "**"; return PDPair
347
347
348pHSimpleExpr syn
348pHSimpleExpr syn
349− = try (pSimpleExpr syn)
350− <|> do lchar '.'
349+ = do lchar '.'
351 e <- pSimpleExpr syn
350 e <- pSimpleExpr syn
352 return $ PHidden e
351 return $ PHidden e
352+ <|> pSimpleExpr syn
353
353
354pApp syn = do f <- pSimpleExpr syn
354pApp syn = do f <- pSimpleExpr syn
355 fc <- pfc
355 fc <- pfc
@@ -408,12 +408,12 @@ pDoBlock syn
408 return (PDoBlock ds)
408 return (PDoBlock ds)
409
409
410pDo syn
410pDo syn
411+ = do reserved "let"; i <- pName; reservedOp "="; fc <- pfc
412+ e <- pExpr syn
413+ return (DoLet fc i e)
411− = try (do i <- pName; symbol "<-"; fc <- pfc
414+ <|> try (do i <- pName; symbol "<-"; fc <- pfc
412 e <- pExpr syn;
415 e <- pExpr syn;
413 return (DoBind fc i e))
416 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))
417 <|> try (do e <- pExpr syn; fc <- pfc
417 <|> try (do e <- pExpr syn; fc <- pfc
418 return (DoExp fc e))
418 return (DoExp fc e))
419
419