f2af303 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+1−1

compare with master

unifiedsplit

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

140 | NewCompile String

141 | Metavars

142 | Prove Name

143− | AddProof Name

143+ | AddProof (Maybe Name)

144 | RmProof Name

145 | ShowProof Name

146 | Proofs

src/Idris/REPL.hs+7−2

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

253 let ms = idris_metavars i

254 put $ i { idris_metavars = n : ms }

255

256−process fn (AddProof n')

256+process fn (AddProof prf)

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

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

259 prog <- liftIO $ readFile fb

260 i <- get

261− n <- resolveProof n'

262 let proofs = proof_list i

261 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'

263 case lookup n proofs of

268 case lookup n proofs of

264 Nothing -> iputStrLn "No proof to add"

269 Nothing -> iputStrLn "No proof to add"

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

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

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

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

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

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

36+ return (Just x))

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

37+ eof; return (AddProof n))

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

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

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

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

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

40 <|> 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: "

40

41---------- Proofs ----------

42

43−natToBin_lemma_1 = proof {

43+main.parity_lemma_1 = proof {

44− intro;

44+ intros;

45− intro;

46 rewrite sym (plusSuccRightSucc j j);

45 rewrite sym (plusSuccRightSucc j j);

47 trivial;

46 trivial;

48}

47}

49

48

50−parity_lemma_2 = proof {

49+natToBin_lemma_1 = proof {

51 intro;

50 intro;

52 intro;

51 intro;

53 rewrite sym (plusSuccRightSucc j j);

52 rewrite sym (plusSuccRightSucc j j);

54 trivial;

53 trivial;

55}

54}

56

55

57−parity_lemma_1 = proof {

56+parity_lemma_2 = proof {

58− intro j;

57+ intro;

59 intro;

58 intro;

60 rewrite sym (plusSuccRightSucc j j);

59 rewrite sym (plusSuccRightSucc j j);

61 trivial;

60 trivial;

62}

61}

63

62

64

63

64+