@@ -212,6 +212,15 @@ updateMeta brack (c:cs) n new
212 = c : updateMeta (brack || not (isSpace c)) cs n new
212 = c : updateMeta (brack || not (isSpace c)) cs n new
213updateMeta brack [] n new = ""
213updateMeta brack [] n new = ""
215+checkProv line n = isProv' False line n
217+ isProv' p cs n | take (length n) cs == n = p
218+ isProv' _ ('?':cs) n = isProv' False cs n
219+ isProv' _ ('{':cs) n = isProv' True cs n
220+ isProv' _ ('}':cs) n = isProv' True cs n
221+ isProv' p (_:cs) n = isProv' p cs n
222+ isProv' _ [] n = False
215addBracket False new = new
224addBracket False new = new
216addBracket True new@('(':xs) | last xs == ')' = new
225addBracket True new@('(':xs) | last xs == ')' = new
217addBracket True new | any isSpace new = '(' : new ++ ")"
226addBracket True new | any isSpace new = '(' : new ++ ")"
@@ -223,23 +232,37 @@ makeLemma h fn updatefile l n
223 = do src <- runIO $ readFile fn
232 = do src <- runIO $ readFile fn
224 let (before, tyline : later) = splitAt (l-1) (lines src)
233 let (before, tyline : later) = splitAt (l-1) (lines src)
235+ -- if the name is in braces, rather than preceded by a ?, treat it
236+ -- as a lemma in a provisional definition
238+ let isProv = checkProv tyline (show n)
226 ctxt <- getContext
240 ctxt <- getContext
227 mty <- case lookupTy n ctxt of
241 mty <- case lookupTy n ctxt of
228 [t] -> return t
242 [t] -> return t
229 [] -> ierror (NoSuchVariable n)
243 [] -> ierror (NoSuchVariable n)
230 ns -> ierror (CantResolveAlts (map show ns))
244 ns -> ierror (CantResolveAlts (map show ns))
232 i <- getIState
245 i <- getIState
233− let skip = guessImps (tt_ctxt i) mty
235− let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))
247+ if (not isProv) then do
236− let lem_app = show n ++ appArgs skip mty
248+ let skip = guessImps (tt_ctxt i) mty
250+ let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))
251+ let lem_app = show n ++ appArgs skip mty
238− if updatefile then
253+ if updatefile then
239− do let fb = fn ++ "~"
254+ do let fb = fn ++ "~"
240− runIO $ writeFile fb (addLem before tyline lem lem_app later)
255+ runIO $ writeFile fb (addLem before tyline lem lem_app later)
241− runIO $ copyFile fb fn
256+ runIO $ copyFile fb fn
242− else ihPrintResult h $ lem ++ "\n" ++ lem_app
257+ else ihPrintResult h $ lem ++ "\n" ++ lem_app
258+ else do -- provisional definition
259+ let lem_app = show n ++ appArgs [] mty ++
260+ " = ?" ++ show n ++ "_rhs"
262+ do let fb = fn ++ "~"
263+ runIO $ writeFile fb (addProv before tyline lem_app later)
264+ runIO $ copyFile fb fn
265+ else ihPrintResult h $ lem_app
244 where getIndent s = length (takeWhile isSpace s)
267 where getIndent s = length (takeWhile isSpace s)
@@ -279,11 +302,21 @@ makeLemma h fn updatefile l n
280 addLem before tyline lem lem_app later
303 addLem before tyline lem lem_app later
281 = let (bef_end, blankline : bef_start)
304 = let (bef_end, blankline : bef_start)
282− = span (not . blank) (reverse before)
305+ = case span (not . blank) (reverse before) of
306+ (bef, []) -> (bef, "" : [])
283 mvline = updateMeta False tyline (show n) lem_app in
308 mvline = updateMeta False tyline (show n) lem_app in
284 unlines $ reverse bef_start ++
309 unlines $ reverse bef_start ++
285 [blankline, lem, blankline] ++
310 [blankline, lem, blankline] ++
286 reverse bef_end ++ mvline : later
311 reverse bef_end ++ mvline : later
288−
313+ addProv before tyline lem_app later
314+ = let (later_bef, blankline : later_end)
315+ = case span (not . blank) later of
316+ (bef, []) -> (bef, "" : [])
318+ unlines $ before ++ tyline :
319+ (later_bef ++ [blankline, lem_app, blankline] ++