b8815e2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

added proof list

b8815e2raichoo14 years ago

src/Idris/AbsSyntaxTree.hs+3−3

compare with master

unifiedsplit

@@ -70,7 +70,7 @@ data IState = IState { tt_ctxt :: Context,

70 idris_objs :: [FilePath],

71 idris_libs :: [String],

72 idris_hdrs :: [String],

73− last_proof :: Maybe (Name, [String]),

73+ proof_list :: [(Name, [String])],

74 errLine :: Maybe Int,

75 lastParse :: Maybe Name,

76 indent_stack :: [Int],

@@ -109,7 +109,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

109 emptyContext emptyContext emptyContext emptyContext

110 emptyContext emptyContext emptyContext

111 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []

112− Nothing Nothing Nothing [] [] [] Hidden [] Nothing

112+ [] Nothing Nothing [] [] [] Hidden [] Nothing

113

114-- The monad for the main REPL - reading and processing files and updating

115-- global state (hence the IO inner monad).

@@ -121,7 +121,7 @@ data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name

121 | Reload | Edit

122 | Compile String | Execute | ExecVal PTerm

123 | NewCompile String

124− | Metavars | Prove Name | AddProof | Universes

125 | TTShell

126 | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name

127 | Info Name | DebugInfo Name

src/Idris/Prover.hs+2−1

@@ -44,7 +44,8 @@ prove ctxt lit n ty

44 iLOG $ "Adding " ++ show tm

45 iputStrLn $ showProof lit n prf

46 i <- get

47− put (i { last_proof = Just (n, prf) })

47+ let proofs = proof_list i

48+ put (i { proof_list = (n, prf) : proofs })

48 let tree = simpleCase False True (FC "proof" 0) [([], P Ref n ty, tm)]

49 let tree = simpleCase False True (FC "proof" 0) [([], P Ref n ty, tm)]

49 logLvl 3 (show tree)

50 logLvl 3 (show tree)

50 (ptm, pty) <- recheckC (FC "proof" 0) [] tm

51 (ptm, pty) <- recheckC (FC "proof" 0) [] tm

src/Idris/REPL.hs+31−7

@@ -82,6 +82,10 @@ processInput cmd orig inputs

82 Right AddProof -> do idrisCatch (addProof fn orig)

83 (\e -> iputStrLn (show e))

84 return (Just inputs)

85+ Right RmProof -> do rmProof orig

86+ return (Just inputs)

87+ Right Proofs -> do proofs orig

88+ return (Just inputs)

85 Right Quit -> do iputStrLn "Bye bye"

89 Right Quit -> do iputStrLn "Bye bye"

86 return Nothing

90 return Nothing

87 Right cmd -> do idrisCatch (process fn cmd)

91 Right cmd -> do idrisCatch (process fn cmd)

@@ -115,13 +119,31 @@ addProof f orig

115 liftIO $ copyFile f fb -- make a backup in case something goes wrong!

119 liftIO $ copyFile f fb -- make a backup in case something goes wrong!

116 prog <- liftIO $ readFile fb

120 prog <- liftIO $ readFile fb

117 i <- get

121 i <- get

118− case last_proof i of

122+ case proof_list i of

119− Nothing -> iputStrLn "No proof to add"

123+ [] -> iputStrLn "No proof to add"

120− Just (n, p) -> do let prog' = insertScript (showProof (lit f) n p) (lines prog)

124+ (n, p) : proofs -> do let prog' = insertScript (showProof (lit f) n p) (lines prog)

121− liftIO $ writeFile f (unlines prog')

125+ liftIO $ writeFile f (unlines prog')

122− iputStrLn $ "Added proof " ++ show n

126+ iputStrLn $ "Added proof " ++ show n

123− put (i { last_proof = Nothing })

127+ put (i { proof_list = proofs })

124− -- lift $ removeFile fb -- uncomment when less scared :)

128+ -- lift $ removeFile fb -- uncomment when less scared :)

129+

130+rmProof :: IState -> Idris ()

131+rmProof orig

132+ = do i <- get

133+ case proof_list i of

134+ [] -> iputStrLn "Nothing to remove"

135+ (n, p) : ps -> do iputStrLn $ "Removed proof " ++ show n

136+ let metavars = idris_metavars i

137+ put (i { proof_list = ps

138+ , idris_metavars = n : metavars

139+ })

140+

141+proofs :: IState -> Idris ()

142+proofs orig

143+ = do i <- get

144+ case proof_list i of

145+ [] -> iputStrLn "No proofs"

146+ ps -> mapM_ (\(n, p) -> iputStrLn $ showProof False n p) ps

125

147

126insertScript :: String -> [String] -> [String]

148insertScript :: String -> [String] -> [String]

127insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]

149insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]

@@ -332,6 +354,8 @@ help =

332 ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),

354 ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),

333 ([":p",":prove"], "<name>", "Prove a metavariable"),

355 ([":p",":prove"], "<name>", "Prove a metavariable"),

334 ([":a",":addproof"], "", "Add last proof to source file"),

356 ([":a",":addproof"], "", "Add last proof to source file"),

357+ ([":rmproof"], "", "Remove last proof from proof stack"),

358+ ([":proofs"], "", "Show proof stack"),

335 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),

359 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),

336 ([":exec",":execute"], "", "Compile to an executable and run"),

360 ([":exec",":execute"], "", "Compile to an executable and run"),

337 ([":?",":h",":help"], "", "Display this help text"),

361 ([":?",":h",":help"], "", "Display this help text"),

src/Idris/REPLParser.hs+3−1

@@ -29,8 +29,10 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

29 <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile f))

30 <|> try (do cmd ["nc", "newcompile"]; f <- identifier; eof; return (NewCompile f))

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

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

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

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

33 <|> try (do cmd ["a", "addproof"]; eof; return AddProof)

34 <|> try (do cmd ["a", "addproof"]; eof; return AddProof)

35+ <|> try (do cmd ["rmproof"]; eof; return RmProof)

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

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

35 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))

37 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))

36 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))

38 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))