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

git.iko.soy/Idris-dev

Add let x = t tactic

commit374fc26ccabb4fe4300715325e6fd169bae34399 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 17 Nov 2011, 22:06 (15 years ago) parentdf49a2a

3 files changed+19−2

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+1−1 src/Idris/ElabDecls.hs+11 src/Idris/Parser.hs+7−1

src/Idris/AbsSyntax.hs+1−1

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

316316

317317

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

319− | Refine Name [Bool] | Rewrite t

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

320320 | Exact t | Compute | Trivial

321321 | Solve

322322 | Attack

src/Idris/ElabDecls.hs+11

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

727727 elab ist toplevel False tm

728728 rewrite (Var letn)

729729 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

730741 runT Compute = compute

731742 runT Trivial = do trivial ist; when autoSolve solveAll

732743 runT (Focus n) = focus n

src/Idris/Parser.hs+7−1

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

8282 return ()

8383

8484parseExpr 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)"

8688

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

8890parseImports fname input

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

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

752754 i <- getState

753755 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)

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

755761 return $ Focus n

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