e39254c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added 'abandon' command in proof mode

(Alternatively, :q)

commite39254c2248e28746a0a4221e85534a46e3ad1a8 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 18 Jan 2012, 17:38 (15 years ago) parenteec2b83

3 files changed+6−1

unifiedsplit

src/Idris/AbsSyntax.hs+1−1

@@ -487,7 +487,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

487487 | ProofState | ProofTerm | Undo

488488 | Try (PTactic' t) (PTactic' t)

489489 | TSeq (PTactic' t) (PTactic' t)

490− | Qed

490+ | Qed | Abandon

491491 deriving (Show, Eq, Functor)

492492{-!

493493deriving instance Binary PTactic'

src/Idris/Parser.hs+2

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

11841184 <|> do reserved "term"; return ProofTerm

11851185 <|> do reserved "undo"; return Undo

11861186 <|> do reserved "qed"; return Qed

1187+ <|> do reserved "abandon"; return Abandon

1188+ <|> do lchar ':'; reserved "q"; return Abandon

11871189 where

11881190 imp = do lchar '?'; return False

11891191 <|> do lchar '_'; return True

src/Idris/Prover.hs+3

@@ -93,6 +93,9 @@ ploop d prompt prf e

9393 (cmd, step) <- case x of

9494 Nothing -> fail "Abandoned"

9595 Just input -> do return (parseTac i input, input)

96+ case cmd of

97+ Right Abandon -> fail "Abandoned"

98+ _ -> return ()

9699 (d, st, done, prf') <- idrisCatch

97100 (case cmd of

98101 Left err -> do iputStrLn (show err)