374fc26 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+1−1

compare with master

unifiedsplit

@@ -316,7 +316,7 @@ mapPT f t = f (mpt t) where

316

317

318data PTactic' t = Intro [Name] | Focus Name

319− | Refine Name [Bool] | Rewrite t

319+ | Refine Name [Bool] | Rewrite t | LetTac Name t

320 | Exact t | Compute | Trivial

321 | Solve

322 | Attack

src/Idris/ElabDecls.hs+11

@@ -727,6 +727,17 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

727 elab ist toplevel False tm

728 rewrite (Var letn)

729 when autoSolve solveAll

730+ runT (LetTac n tm)

731+ = do attack

732+ tyn <- unique_hole (MN 0 "letty")

733+ claim tyn (RSet 0)

734+ valn <- unique_hole (MN 0 "letval")

735+ claim valn (Var tyn)

736+ letn <- unique_hole n

737+ letbind letn (Var tyn) (Var valn)

738+ focus valn

739+ elab ist toplevel False tm

740+ when autoSolve solveAll

730 runT Compute = compute

741 runT Compute = compute

731 runT Trivial = do trivial ist; when autoSolve solveAll

742 runT Trivial = do trivial ist; when autoSolve solveAll

732 runT (Focus n) = focus n

743 runT (Focus n) = focus n

src/Idris/Parser.hs+7−1

@@ -82,7 +82,9 @@ loadSource f = do iLOG ("Reading " ++ f)

82 return ()

83

84parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"

85−parseTac i = runParser (pTactic defaultSyntax) i "(proof)"

85+parseTac i = runParser (do t <- pTactic defaultSyntax

86+ eof

87+ return t) i "(proof)"

86

88

87parseImports :: FilePath -> String -> Idris ([String], String, SourcePos)

89parseImports :: FilePath -> String -> Idris ([String], String, SourcePos)

88parseImports fname input

90parseImports fname input

@@ -751,6 +753,10 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

751 <|> do reserved "rewrite"; t <- pExpr syn;

753 <|> do reserved "rewrite"; t <- pExpr syn;

752 i <- getState

754 i <- getState

753 return $ Rewrite (desugar syn i t)

755 return $ Rewrite (desugar syn i t)

756+ <|> do reserved "let"; n <- pName; lchar '=';

757+ t <- pExpr syn;

758+ i <- getState

759+ return $ LetTac n (desugar syn i t)

754 <|> do reserved "focus"; n <- pName

760 <|> do reserved "focus"; n <- pName

755 return $ Focus n

761 return $ Focus n

756 <|> do reserved "exact"; t <- pExpr syn;

762 <|> do reserved "exact"; t <- pExpr syn;