@@ -79,11 +79,6 @@ processInput cmd orig inputs
7979 return (Just inputs)
8080 Right Edit -> do edit fn orig
8181 return (Just 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)
8782 Right Proofs -> do proofs orig
8883 return (Just inputs)
8984 Right Quit -> do iputStrLn "Bye bye"
@@ -92,6 +87,23 @@ processInput cmd orig inputs
9287 (\e -> iputStrLn (show e))
9388 return (Just inputs)
9489
90+resolveProof :: Name -> Idris Name
91+resolveProof n'
92+ = do i <- get
93+ ctxt <- getContext
94+ n <- case lookupNames Nothing n' ctxt of
95+ [x] -> return x
96+ [] -> return n'
97+ ns -> fail $ pshow i (CantResolveAlts (map show ns))
98+ return n
99+
100+removeProof :: Name -> Idris ()
101+removeProof n =
102+ do i <- get
103+ let proofs = proof_list i
104+ let ps = filter ((/= n) . fst) proofs
105+ put $ i { proof_list = ps }
106+
95107edit :: FilePath -> IState -> Idris ()
96108edit "" orig = iputStrLn "Nothing to edit"
97109edit f orig
@@ -112,38 +124,14 @@ edit f orig
112124 | Just ed <- lookup "VISUAL" env = ed
113125 | otherwise = "vi"
114126
115−addProof :: FilePath -> IState -> Idris ()
116−addProof "" orig = iputStrLn "Nothing to add to"
117−addProof f orig
118− = do let fb = f ++ "~"
119− liftIO $ copyFile f fb -- make a backup in case something goes wrong!
120− prog <- liftIO $ readFile fb
121− i <- get
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− })
140127
141128proofs :: IState -> Idris ()
142129proofs orig
143130 = do i <- get
144− case proof_list i of
145− [] -> iputStrLn "No proofs"
146− ps -> mapM_ (\(n, p) -> iputStrLn $ showProof False n p) ps
131+ let ps = proof_list i
132+ case ps of
133+ [] -> iputStrLn "No proofs available"
134+ _ -> iputStrLn $ "Proofs:\n\t" ++ (show $ map fst ps)
147135
148136insertScript :: String -> [String] -> [String]
149137insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
@@ -246,19 +234,60 @@ process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
246234 ist <- get
247235 let tm' = specialise ctxt [] [] {- (idris_statics ist) -} tm
248236 iputStrLn (show (delab ist tm'))
249−process fn (Prove n')
237+
238+process fn (RmProof n')
239+ = do i <- get
240+ n <- resolveProof n'
241+ let proofs = proof_list i
242+ case lookup n proofs of
243+ Nothing -> iputStrLn "No proof to remove"
244+ Just _ -> do removeProof n
245+ insertMetavar n
246+ iputStrLn $ "Removed proof " ++ show n
247+ where
248+ insertMetavar :: Name -> Idris ()
249+ insertMetavar n =
250+ do i <- get
251+ let ms = idris_metavars i
252+ put $ i { idris_metavars = n : ms }
253+
254+process fn (AddProof n')
255+ = do let fb = fn ++ "~"
256+ liftIO $ copyFile fn fb -- make a backup in case something goes wrong!
257+ prog <- liftIO $ readFile fb
258+ i <- get
259+ n <- resolveProof n'
260+ let proofs = proof_list i
261+ case lookup n proofs of
262+ Nothing -> iputStrLn "No proof to add"
263+ Just p -> do let prog' = insertScript (showProof (lit fn) n p) ls
264+ liftIO $ writeFile fn (unlines prog')
265+ removeProof n
266+ iputStrLn $ "Added proof " ++ show n
267+ where ls = (lines prog)
268+
269+process fn (ShowProof n')
270+ = do i <- get
271+ n <- resolveProof n'
272+ let proofs = proof_list i
273+ case lookup n proofs of
274+ Nothing -> iputStrLn "No proof to show"
275+ Just p -> iputStrLn $ showProof False n p
276+
277+process fn (Prove n')
250278 = do ctxt <- getContext
251279 ist <- get
252280 n <- case lookupNames Nothing n' ctxt of
253281 [x] -> return x
254282 [] -> return n'
255− ns -> fail $ pshow ist (CantResolveAlts (map show ns))
283+ ns -> fail $ pshow ist (CantResolveAlts (map show ns))
256284 prover (lit fn) n
257285 -- recheck totality
258286 i <- get
259287 totcheck (FC "(input)" 0, n)
260288 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
261289 mapM_ checkDeclTotality (idris_totcheck i)
290+
262291process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t
263292 ctxt <- getContext
264293 ist <- get
@@ -353,9 +382,10 @@ help =
353382 ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"),
354383 ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),
355384 ([":p",":prove"], "<name>", "Prove a metavariable"),
356− ([":a",":addproof"], "", "Add last proof to source file"),
357− ([":rmproof"], "", "Remove last proof from proof stack"),
358− ([":proofs"], "", "Show proof stack"),
385+ ([":a",":addproof"], "<name>", "Add proof to source file"),
386+ ([":rmproof"], "<name>", "Remove proof from proof stack"),
387+ ([":showproof"], "<name>", "Show proof"),
388+ ([":proofs"], "", "Show available proofs"),
359389 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),
360390 ([":exec",":execute"], "", "Compile to an executable and run"),
361391 ([":?",":h",":help"], "", "Display this help text"),