@@ -81,11 +81,6 @@ processInput cmd orig inputs
8181 return (Just inputs)
8282 Right Edit -> do edit fn orig
8383 return (Just inputs)
84− Right AddProof -> do idrisCatch (addProof fn orig)
85− (\e -> iputStrLn (show e))
86− return (Just inputs)
87− Right RmProof -> do rmProof orig
88− return (Just inputs)
8984 Right Proofs -> do proofs orig
9085 return (Just inputs)
9186 Right Quit -> do iputStrLn "Bye bye"
@@ -94,6 +89,23 @@ processInput cmd orig inputs
9489 (\e -> iputStrLn (show e))
9590 return (Just inputs)
9691
92+resolveProof :: Name -> Idris Name
93+resolveProof n'
94+ = do i <- get
95+ ctxt <- getContext
96+ n <- case lookupNames Nothing n' ctxt of
97+ [x] -> return x
98+ [] -> return n'
99+ ns -> fail $ pshow i (CantResolveAlts (map show ns))
100+ return n
101+
102+removeProof :: Name -> Idris ()
103+removeProof n =
104+ do i <- get
105+ let proofs = proof_list i
106+ let ps = filter ((/= n) . fst) proofs
107+ put $ i { proof_list = ps }
108+
97109edit :: FilePath -> IState -> Idris ()
98110edit "" orig = iputStrLn "Nothing to edit"
99111edit f orig
@@ -114,38 +126,14 @@ edit f orig
114126 | Just ed <- lookup "VISUAL" env = ed
115127 | otherwise = "vi"
116128
117−addProof :: FilePath -> IState -> Idris ()
118−addProof "" orig = iputStrLn "Nothing to add to"
119−addProof f orig
120− = do let fb = f ++ "~"
121− liftIO $ copyFile f fb -- make a backup in case something goes wrong!
122− prog <- liftIO $ readFile fb
123− i <- get
124− case proof_list i of
125− [] -> iputStrLn "No proof to add"
126− (n, p) : proofs -> do let prog' = insertScript (showProof (lit f) n p) (lines prog)
127− liftIO $ writeFile f (unlines prog')
128− iputStrLn $ "Added proof " ++ show n
129− put (i { proof_list = proofs })
130− -- lift $ removeFile fb -- uncomment when less scared :)
131−
132−rmProof :: IState -> Idris ()
133−rmProof orig
134− = do i <- get
135− case proof_list i of
136− [] -> iputStrLn "Nothing to remove"
137− (n, p) : ps -> do iputStrLn $ "Removed proof " ++ show n
138− let metavars = idris_metavars i
139− put (i { proof_list = ps
140− , idris_metavars = n : metavars
141− })
142129
143130proofs :: IState -> Idris ()
144131proofs orig
145132 = do i <- get
146− case proof_list i of
147− [] -> iputStrLn "No proofs"
148− ps -> mapM_ (\(n, p) -> iputStrLn $ showProof False n p) ps
133+ let ps = proof_list i
134+ case ps of
135+ [] -> iputStrLn "No proofs available"
136+ _ -> iputStrLn $ "Proofs:\n\t" ++ (show $ map fst ps)
149137
150138insertScript :: String -> [String] -> [String]
151139insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
@@ -235,19 +223,60 @@ process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
235223 ist <- get
236224 let tm' = specialise ctxt [] [] {- (idris_statics ist) -} tm
237225 iputStrLn (show (delab ist tm'))
238−process fn (Prove n')
226+
227+process fn (RmProof n')
228+ = do i <- get
229+ n <- resolveProof n'
230+ let proofs = proof_list i
231+ case lookup n proofs of
232+ Nothing -> iputStrLn "No proof to remove"
233+ Just _ -> do removeProof n
234+ insertMetavar n
235+ iputStrLn $ "Removed proof " ++ show n
236+ where
237+ insertMetavar :: Name -> Idris ()
238+ insertMetavar n =
239+ do i <- get
240+ let ms = idris_metavars i
241+ put $ i { idris_metavars = n : ms }
242+
243+process fn (AddProof n')
244+ = do let fb = fn ++ "~"
245+ liftIO $ copyFile fn fb -- make a backup in case something goes wrong!
246+ prog <- liftIO $ readFile fb
247+ i <- get
248+ n <- resolveProof n'
249+ let proofs = proof_list i
250+ case lookup n proofs of
251+ Nothing -> iputStrLn "No proof to add"
252+ Just p -> do let prog' = insertScript (showProof (lit fn) n p) ls
253+ liftIO $ writeFile fn (unlines prog')
254+ removeProof n
255+ iputStrLn $ "Added proof " ++ show n
256+ where ls = (lines prog)
257+
258+process fn (ShowProof n')
259+ = do i <- get
260+ n <- resolveProof n'
261+ let proofs = proof_list i
262+ case lookup n proofs of
263+ Nothing -> iputStrLn "No proof to show"
264+ Just p -> iputStrLn $ showProof False n p
265+
266+process fn (Prove n')
239267 = do ctxt <- getContext
240268 ist <- get
241269 n <- case lookupNames Nothing n' ctxt of
242270 [x] -> return x
243271 [] -> return n'
244− ns -> fail $ pshow ist (CantResolveAlts (map show ns))
272+ ns -> fail $ pshow ist (CantResolveAlts (map show ns))
245273 prover (lit fn) n
246274 -- recheck totality
247275 i <- get
248276 totcheck (FC "(input)" 0, n)
249277 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
250278 mapM_ checkDeclTotality (idris_totcheck i)
279+
251280process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t
252281 ctxt <- getContext
253282 ist <- get
@@ -354,9 +383,10 @@ help =
354383 ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"),
355384 ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),
356385 ([":p",":prove"], "<name>", "Prove a metavariable"),
357− ([":a",":addproof"], "", "Add last proof to source file"),
358− ([":rmproof"], "", "Remove last proof from proof stack"),
359− ([":proofs"], "", "Show proof stack"),
386+ ([":a",":addproof"], "<name>", "Add proof to source file"),
387+ ([":rmproof"], "<name>", "Remove proof from proof stack"),
388+ ([":showproof"], "<name>", "Show proof"),
389+ ([":proofs"], "", "Show available proofs"),
360390 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),
361391 ([":exec",":execute"], "", "Compile to an executable and run"),
362392 ([":?",":h",":help"], "", "Display this help text"),