git.iko.soy/Idris-dev
on master help sign in
enhanced proof handeling
7f2d76craichoo
src/Idris/AbsSyntaxTree.hs+26−8
compare with master
unifiedsplit
@@ -117,16 +117,34 @@ type Idris = StateT IState (InputT IO)
117
117
118-- Commands in the REPL
118-- Commands in the REPL
119
119
120−data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name
120+data Command = Quit
121+ | Help
122+ | Eval PTerm
123+ | Check PTerm
124+ | TotCheck Name
121− | Reload | Edit
125+ | Reload
126+ | Edit
122− | Compile String | Execute | ExecVal PTerm
127+ | Compile String
128+ | Execute
129+ | ExecVal PTerm
123 | NewCompile String
130 | NewCompile String
124− | Metavars | Prove Name | AddProof | RmProof | Proofs | Universes
131+ | Metavars
132+ | Prove Name
133+ | AddProof Name
134+ | RmProof Name
135+ | ShowProof Name
136+ | Proofs
137+ | Universes
125− | TTShell
138+ | TTShell
126− | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name
139+ | LogLvl Int
140+ | Spec PTerm
141+ | HNF PTerm
142+ | Defn Name
143+ | Info Name
127− | Info Name | DebugInfo Name
144+ | DebugInfo Name
128 | Search PTerm
145 | Search PTerm
146+ | SetOpt Opt
129− | SetOpt Opt | UnsetOpt Opt
147+ | UnsetOpt Opt
130 | NOP
148 | NOP
131
149
132data Opt = Filename String
150data Opt = Filename String
src/Idris/REPL.hs+68−38
@@ -79,11 +79,6 @@ processInput cmd orig inputs
79 return (Just inputs)
79 return (Just inputs)
80 Right Edit -> do edit fn orig
80 Right Edit -> do edit fn orig
81 return (Just inputs)
81 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)
87 Right Proofs -> do proofs orig
82 Right Proofs -> do proofs orig
88 return (Just inputs)
83 return (Just inputs)
89 Right Quit -> do iputStrLn "Bye bye"
84 Right Quit -> do iputStrLn "Bye bye"
@@ -92,6 +87,23 @@ processInput cmd orig inputs
92 (\e -> iputStrLn (show e))
87 (\e -> iputStrLn (show e))
93 return (Just inputs)
88 return (Just inputs)
94
89
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+
95edit :: FilePath -> IState -> Idris ()
107edit :: FilePath -> IState -> Idris ()
96edit "" orig = iputStrLn "Nothing to edit"
108edit "" orig = iputStrLn "Nothing to edit"
97edit f orig
109edit f orig
@@ -112,38 +124,14 @@ edit f orig
112 | Just ed <- lookup "VISUAL" env = ed
124 | Just ed <- lookup "VISUAL" env = ed
113 | otherwise = "vi"
125 | otherwise = "vi"
114
126
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− })
140
127
141proofs :: IState -> Idris ()
128proofs :: IState -> Idris ()
142proofs orig
129proofs orig
143 = do i <- get
130 = do i <- get
144− case proof_list i of
131+ let ps = proof_list i
132+ case ps of
145− [] -> iputStrLn "No proofs"
133+ [] -> iputStrLn "No proofs available"
146− ps -> mapM_ (\(n, p) -> iputStrLn $ showProof False n p) ps
134+ _ -> iputStrLn $ "Proofs:\n\t" ++ (show $ map fst ps)
147
135
148insertScript :: String -> [String] -> [String]
136insertScript :: String -> [String] -> [String]
149insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
137insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
@@ -246,19 +234,60 @@ process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
246 ist <- get
234 ist <- get
247 let tm' = specialise ctxt [] [] {- (idris_statics ist) -} tm
235 let tm' = specialise ctxt [] [] {- (idris_statics ist) -} tm
248 iputStrLn (show (delab ist tm'))
236 iputStrLn (show (delab ist tm'))
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+
249−process fn (Prove n')
277+process fn (Prove n')
250 = do ctxt <- getContext
278 = do ctxt <- getContext
251 ist <- get
279 ist <- get
252 n <- case lookupNames Nothing n' ctxt of
280 n <- case lookupNames Nothing n' ctxt of
253 [x] -> return x
281 [x] -> return x
254 [] -> return n'
282 [] -> return n'
255− ns -> fail $ pshow ist (CantResolveAlts (map show ns))
283+ ns -> fail $ pshow ist (CantResolveAlts (map show ns))
256 prover (lit fn) n
284 prover (lit fn) n
257 -- recheck totality
285 -- recheck totality
258 i <- get
286 i <- get
259 totcheck (FC "(input)" 0, n)
287 totcheck (FC "(input)" 0, n)
260 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
288 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
261 mapM_ checkDeclTotality (idris_totcheck i)
289 mapM_ checkDeclTotality (idris_totcheck i)
290+
262process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t
291process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t
263 ctxt <- getContext
292 ctxt <- getContext
264 ist <- get
293 ist <- get
@@ -353,9 +382,10 @@ help =
353 ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"),
382 ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"),
354 ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),
383 ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),
355 ([":p",":prove"], "<name>", "Prove a metavariable"),
384 ([":p",":prove"], "<name>", "Prove a metavariable"),
356− ([":a",":addproof"], "", "Add last proof to source file"),
385+ ([":a",":addproof"], "<name>", "Add proof to source file"),
357− ([":rmproof"], "", "Remove last proof from proof stack"),
386+ ([":rmproof"], "<name>", "Remove proof from proof stack"),
358− ([":proofs"], "", "Show proof stack"),
387+ ([":showproof"], "<name>", "Show proof"),
388+ ([":proofs"], "", "Show available proofs"),
359 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),
389 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),
360 ([":exec",":execute"], "", "Compile to an executable and run"),
390 ([":exec",":execute"], "", "Compile to an executable and run"),
361 ([":?",":h",":help"], "", "Display this help text"),
391 ([":?",":h",":help"], "", "Display this help text"),
src/Idris/REPLParser.hs+3−2
@@ -31,8 +31,9 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)
31 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)
31 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)
32 <|> try (do cmd ["proofs"]; eof; return Proofs)
32 <|> try (do cmd ["proofs"]; eof; return Proofs)
33 <|> try (do cmd ["p", "prove"]; n <- pName; eof; return (Prove n))
33 <|> try (do cmd ["p", "prove"]; n <- pName; eof; return (Prove n))
34− <|> try (do cmd ["a", "addproof"]; eof; return AddProof)
34+ <|> try (do cmd ["a", "addproof"]; n <- pName; eof; return (AddProof n))
35− <|> try (do cmd ["rmproof"]; eof; return RmProof)
35+ <|> try (do cmd ["rmproof"]; n <- pName; eof; return (RmProof n))
36+ <|> try (do cmd ["showproof"]; n <- pName; eof; return (ShowProof n))
36 <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))
37 <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))
37 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))
38 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))
38 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))
39 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))