f2af303 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

:addproof now adds most recent proof if no argument given

Consistent with old behaviour, and with tutorial

commitf2af3031b6d03f4a3aa3224bfa6863e7cbae48ad authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 22 Oct 2012, 13:22 (14 years ago) parentadbe613

4 files changed+17−10

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/REPL.hs+7−2 src/Idris/REPLParser.hs+3−1 tutorial/examples/binary.idr+6−6

src/Idris/AbsSyntaxTree.hs+1−1

@@ -140,7 +140,7 @@ data Command = Quit

140140 | NewCompile String

141141 | Metavars

142142 | Prove Name

143− | AddProof Name

143+ | AddProof (Maybe Name)

144144 | RmProof Name

145145 | ShowProof Name

146146 | Proofs

src/Idris/REPL.hs+7−2

@@ -253,13 +253,18 @@ process fn (RmProof n')

253253 let ms = idris_metavars i

254254 put $ i { idris_metavars = n : ms }

255255

256−process fn (AddProof n')

256+process fn (AddProof prf)

257257 = do let fb = fn ++ "~"

258258 liftIO $ copyFile fn fb -- make a backup in case something goes wrong!

259259 prog <- liftIO $ readFile fb

260260 i <- get

261− n <- resolveProof n'

262261 let proofs = proof_list i

262+ n' <- case prf of

263+ Nothing -> case proofs of

264+ [] -> fail "No proof to add"

265+ ((x, p) : _) -> return x

266+ Just nm -> return nm

267+ n <- resolveProof n'

263268 case lookup n proofs of

264269 Nothing -> iputStrLn "No proof to add"

265270 Just p -> do let prog' = insertScript (showProof (lit fn) n p) ls

src/Idris/REPLParser.hs+3−1

@@ -32,7 +32,9 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

3232 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)

3333 <|> try (do cmd ["proofs"]; eof; return Proofs)

3434 <|> try (do cmd ["p", "prove"]; n <- pName; eof; return (Prove n))

35− <|> try (do cmd ["a", "addproof"]; n <- pName; eof; return (AddProof n))

35+ <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- pName;

36+ return (Just x))

37+ eof; return (AddProof n))

3638 <|> try (do cmd ["rmproof"]; n <- pName; eof; return (RmProof n))

3739 <|> try (do cmd ["showproof"]; n <- pName; eof; return (ShowProof n))

3840 <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))

tutorial/examples/binary.idr+6−6

@@ -40,25 +40,25 @@ main = do putStr "Enter a number: "

4040

4141---------- Proofs ----------

4242

43−natToBin_lemma_1 = proof {

44− intro;

45− intro;

43+main.parity_lemma_1 = proof {

44+ intros;

4645 rewrite sym (plusSuccRightSucc j j);

4746 trivial;

4847}

4948

50−parity_lemma_2 = proof {

49+natToBin_lemma_1 = proof {

5150 intro;

5251 intro;

5352 rewrite sym (plusSuccRightSucc j j);

5453 trivial;

5554}

5655

57−parity_lemma_1 = proof {

58− intro j;

56+parity_lemma_2 = proof {

57+ intro;

5958 intro;

6059 rewrite sym (plusSuccRightSucc j j);

6160 trivial;

6261}

6362

6463

64+