99fd819 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #47 from raichoo/master

REPL improvements

commit99fd8199ea4d46d95e00ad490390399054b3cb12 authorEdwin Brady <edwin.brady@gmail.com> dateTue 4 Sep 2012, 09:36 (14 years ago) parent4e0fe22 b8815e2

4 files changed+39−12

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+3−3 src/Idris/Prover.hs+2−1 src/Idris/REPL.hs+31−7 src/Idris/REPLParser.hs+3−1

src/Idris/AbsSyntaxTree.hs+3−3

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

7070 idris_objs :: [FilePath],

7171 idris_libs :: [String],

7272 idris_hdrs :: [String],

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

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

7474 errLine :: Maybe Int,

7575 lastParse :: Maybe Name,

7676 indent_stack :: [Int],

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

109109 emptyContext emptyContext emptyContext emptyContext

110110 emptyContext emptyContext emptyContext

111111 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []

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

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

113113

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

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

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

121121 | Reload | Edit

122122 | Compile String | Execute | ExecVal PTerm

123123 | NewCompile String

124− | Metavars | Prove Name | AddProof | Universes

125125 | TTShell

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

127127 | Info Name | DebugInfo Name

src/Idris/Prover.hs+2−1

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

4444 iLOG $ "Adding " ++ show tm

4545 iputStrLn $ showProof lit n prf

4646 i <- get

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

47+ let proofs = proof_list i

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

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

4950 logLvl 3 (show tree)

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

src/Idris/REPL.hs+31−7

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

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

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

8484 return (Just inputs)

85+ Right RmProof -> do rmProof orig

86+ return (Just inputs)

87+ Right Proofs -> do proofs orig

88+ return (Just inputs)

8589 Right Quit -> do iputStrLn "Bye bye"

8690 return Nothing

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

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

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

116120 prog <- liftIO $ readFile fb

117121 i <- get

118− case last_proof i of

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

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

121− liftIO $ writeFile f (unlines prog')

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

123− put (i { last_proof = Nothing })

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

122+ case proof_list i of

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

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

125+ liftIO $ writeFile f (unlines prog')

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

127+ put (i { proof_list = proofs })

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

125147

126148insertScript :: String -> [String] -> [String]

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

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

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

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

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

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

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

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

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

337361 ([":?",":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)

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

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

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

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

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

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

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

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

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

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

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