git.iko.soy/Idris-dev
on master help sign in
Merge pull request #48 from raichoo/master
ef1d7baEdwin Brady
src/Idris/AbsSyntaxTree.hs+26−8
compare with master
unifiedsplit
@@ -114,16 +114,34 @@ type Idris = StateT IState (InputT IO)
114
114
115-- Commands in the REPL
115-- Commands in the REPL
116
116
117−data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name
117+data Command = Quit
118+ | Help
119+ | Eval PTerm
120+ | Check PTerm
121+ | TotCheck Name
118− | Reload | Edit
122+ | Reload
123+ | Edit
119− | Compile String | Execute | ExecVal PTerm
124+ | Compile String
125+ | Execute
126+ | ExecVal PTerm
120 | NewCompile String
127 | NewCompile String
121− | Metavars | Prove Name | AddProof | RmProof | Proofs | Universes
128+ | Metavars
129+ | Prove Name
130+ | AddProof Name
131+ | RmProof Name
132+ | ShowProof Name
133+ | Proofs
134+ | Universes
122− | TTShell
135+ | TTShell
123− | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name
136+ | LogLvl Int
137+ | Spec PTerm
138+ | HNF PTerm
139+ | Defn Name
140+ | Info Name
124− | Info Name | DebugInfo Name
141+ | DebugInfo Name
125 | Search PTerm
142 | Search PTerm
143+ | SetOpt Opt
126− | SetOpt Opt | UnsetOpt Opt
144+ | UnsetOpt Opt
127 | NOP
145 | NOP
128
146
129data Opt = Filename String
147data Opt = Filename String
src/Idris/REPL.hs+68−38
@@ -81,11 +81,6 @@ processInput cmd orig inputs
81 return (Just inputs)
81 return (Just inputs)
82 Right Edit -> do edit fn orig
82 Right Edit -> do edit fn orig
83 return (Just inputs)
83 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)
89 Right Proofs -> do proofs orig
84 Right Proofs -> do proofs orig
90 return (Just inputs)
85 return (Just inputs)
91 Right Quit -> do iputStrLn "Bye bye"
86 Right Quit -> do iputStrLn "Bye bye"
@@ -94,6 +89,23 @@ processInput cmd orig inputs
94 (\e -> iputStrLn (show e))
89 (\e -> iputStrLn (show e))
95 return (Just inputs)
90 return (Just inputs)
96
91
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+
97edit :: FilePath -> IState -> Idris ()
109edit :: FilePath -> IState -> Idris ()
98edit "" orig = iputStrLn "Nothing to edit"
110edit "" orig = iputStrLn "Nothing to edit"
99edit f orig
111edit f orig
@@ -114,38 +126,14 @@ edit f orig
114 | Just ed <- lookup "VISUAL" env = ed
126 | Just ed <- lookup "VISUAL" env = ed
115 | otherwise = "vi"
127 | otherwise = "vi"
116
128
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− })
142
129
143proofs :: IState -> Idris ()
130proofs :: IState -> Idris ()
144proofs orig
131proofs orig
145 = do i <- get
132 = do i <- get
146− case proof_list i of
133+ let ps = proof_list i
134+ case ps of
147− [] -> iputStrLn "No proofs"
135+ [] -> iputStrLn "No proofs available"
148− ps -> mapM_ (\(n, p) -> iputStrLn $ showProof False n p) ps
136+ _ -> iputStrLn $ "Proofs:\n\t" ++ (show $ map fst ps)
149
137
150insertScript :: String -> [String] -> [String]
138insertScript :: String -> [String] -> [String]
151insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
139insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
@@ -235,19 +223,60 @@ process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
235 ist <- get
223 ist <- get
236 let tm' = specialise ctxt [] [] {- (idris_statics ist) -} tm
224 let tm' = specialise ctxt [] [] {- (idris_statics ist) -} tm
237 iputStrLn (show (delab ist tm'))
225 iputStrLn (show (delab ist tm'))
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+
238−process fn (Prove n')
266+process fn (Prove n')
239 = do ctxt <- getContext
267 = do ctxt <- getContext
240 ist <- get
268 ist <- get
241 n <- case lookupNames Nothing n' ctxt of
269 n <- case lookupNames Nothing n' ctxt of
242 [x] -> return x
270 [x] -> return x
243 [] -> return n'
271 [] -> return n'
244− ns -> fail $ pshow ist (CantResolveAlts (map show ns))
272+ ns -> fail $ pshow ist (CantResolveAlts (map show ns))
245 prover (lit fn) n
273 prover (lit fn) n
246 -- recheck totality
274 -- recheck totality
247 i <- get
275 i <- get
248 totcheck (FC "(input)" 0, n)
276 totcheck (FC "(input)" 0, n)
249 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
277 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
250 mapM_ checkDeclTotality (idris_totcheck i)
278 mapM_ checkDeclTotality (idris_totcheck i)
279+
251process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t
280process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t
252 ctxt <- getContext
281 ctxt <- getContext
253 ist <- get
282 ist <- get
@@ -354,9 +383,10 @@ help =
354 ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"),
383 ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"),
355 ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),
384 ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),
356 ([":p",":prove"], "<name>", "Prove a metavariable"),
385 ([":p",":prove"], "<name>", "Prove a metavariable"),
357− ([":a",":addproof"], "", "Add last proof to source file"),
386+ ([":a",":addproof"], "<name>", "Add proof to source file"),
358− ([":rmproof"], "", "Remove last proof from proof stack"),
387+ ([":rmproof"], "<name>", "Remove proof from proof stack"),
359− ([":proofs"], "", "Show proof stack"),
388+ ([":showproof"], "<name>", "Show proof"),
389+ ([":proofs"], "", "Show available proofs"),
360 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),
390 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),
361 ([":exec",":execute"], "", "Compile to an executable and run"),
391 ([":exec",":execute"], "", "Compile to an executable and run"),
362 ([":?",":h",":help"], "", "Display this help text"),
392 ([":?",":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))