git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/src/Idris/Interactive.hs
506 lines 22 kB history raw
1{-|
2Module : Idris.Interactive
3Description : Bits and pieces for editing source files interactively, called from the REPL
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
9{-# LANGUAGE PatternGuards #-}
11module Idris.Interactive(
12 caseSplitAt, addClauseFrom, addProofClauseFrom
13 , addMissing, makeWith, makeCase, doProofSearch
14 , makeLemma
15 ) where
17import Idris.AbsSyntax
18import Idris.CaseSplit
19import Idris.Core.Evaluate
20import Idris.Core.TT
21import Idris.Delaborate
22import Idris.Elab.Term
23import Idris.Elab.Value
24import Idris.ElabDecls
25import Idris.Error
26import Idris.ErrReverse
27import Idris.IdeMode hiding (IdeModeCommand(..))
28import Idris.Output
30import Util.Pretty
31import Util.System
33import Data.Char
34import Data.List (isSuffixOf)
35import System.Directory
36import System.IO
38caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()
39caseSplitAt fn updatefile l n
40 = do src <- runIO $ readSourceStrict fn
41 (ok, res) <- splitOnLine l n fn
42 logLvl 1 (showSep "\n" (map show res))
43 let (before, (ap : later)) = splitAt (l-1) (lines src)
44 res' <- replaceSplits ap res (not ok)
45 let new = concat res'
46 if updatefile
47 then do let fb = fn ++ "~" -- make a backup!
48 runIO $ writeSource fb (unlines before ++ new ++ unlines later)
49 runIO $ copyFile fb fn
50 else -- do iputStrLn (show res)
51 iPrintResult new
53addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
54addClauseFrom fn updatefile l n = do
55 -- if a definition already exists, add missing cases rather than
56 -- adding a new definition.
57 ist <- getIState
58 cl <- getInternalApp fn l
59 let fulln = getAppName cl
60 let metavars = lookup fulln (idris_metavars ist)
61 case metavars of
62 Nothing -> addMissing fn updatefile l n
63 Just _ -> do
64 src <- runIO $ readSourceStrict fn
65 let (before, tyline : later) = splitAt (l-1) (lines src)
66 let indent = getIndent 0 (show n) tyline
67 cl <- getClause l fulln n fn
68 -- add clause before first blank line in 'later'
69 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
70 if updatefile
71 then do let fb = fn ++ "~"
72 runIO $ writeSource fb (unlines (before ++ nonblank) ++
73 replicate indent ' ' ++
74 cl ++ "\n" ++
75 unlines rest)
76 runIO $ copyFile fb fn
77 else iPrintResult cl
78 where
79 getIndent i n [] = 0
80 getIndent i n xs | take 9 xs == "implementation " = i
81 getIndent i n xs | take (length n) xs == n = i
82 getIndent i n (x : xs) = getIndent (i + 1) n xs
84 getAppName (PApp _ r _) = getAppName r
85 getAppName (PRef _ _ r) = r
86 getAppName (PTyped n _) = getAppName n
87 getAppName _ = n
89addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
90addProofClauseFrom fn updatefile l n
91 = do src <- runIO $ readSourceStrict fn
92 let (before, tyline : later) = splitAt (l-1) (lines src)
93 let indent = getIndent 0 (show n) tyline
94 cl <- getProofClause l n fn
95 -- add clause before first blank line in 'later'
96 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
97 if updatefile
98 then do let fb = fn ++ "~"
99 runIO $ writeSource fb (unlines (before ++ nonblank) ++
100 replicate indent ' ' ++
101 cl ++ "\n" ++
102 unlines rest)
103 runIO $ copyFile fb fn
104 else iPrintResult cl
105 where
106 getIndent i n [] = 0
107 getIndent i n xs | take (length n) xs == n = i
108 getIndent i n (x : xs) = getIndent (i + 1) n xs
110addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()
111addMissing fn updatefile l n
112 = do src <- runIO $ readSourceStrict fn
113 let (before, tyline : later) = splitAt (l-1) (lines src)
114 let indent = getIndent tyline
115 i <- getIState
116 cl <- getInternalApp fn l
117 let n' = getAppName cl
119 extras <- case lookupCtxtExact n' (idris_patdefs i) of
120 Nothing -> return ""
121 Just (_, tms) -> do tms' <- nameMissing tms
122 showNew (show n ++ "_rhs") 1 indent tms'
123 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
124 if updatefile
125 then do let fb = fn ++ "~"
126 runIO $ writeSource fb (unlines (before ++ nonblank)
127 ++ extras
128 ++ (if null extras then "" else "\n")
129 ++ unlines rest)
130 runIO $ (length src `seq` copyFile fb fn)
131 else iPrintResult extras
132 where showPat = show . stripNS
133 stripNS tm = mapPT dens tm where
134 dens (PRef fc hls n) = PRef fc hls (nsroot n)
135 dens t = t
137 nsroot (NS n _) = nsroot n
138 nsroot (SN (WhereN _ _ n)) = nsroot n
139 nsroot n = n
141 getAppName (PApp _ r _) = getAppName r
142 getAppName (PRef _ _ r) = r
143 getAppName (PTyped n _) = getAppName n
144 getAppName _ = n
146 makeIndent ind | ".lidr" `isSuffixOf` fn = '>' : ' ' : replicate (ind-2) ' '
147 | otherwise = replicate ind ' '
149 showNew nm i ind (tm : tms)
150 = do (nm', i') <- getUniq nm i
151 rest <- showNew nm i' ind tms
152 return (makeIndent ind ++
153 showPat tm ++ " = ?" ++ nm' ++
154 (if null rest then "" else
155 "\n" ++ rest))
156 showNew nm i _ [] = return ""
158 getIndent s = length (takeWhile isSpace s)
161makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()
162makeWith fn updatefile l n = do
163 src <- runIO $ readSourceStrict fn
164 i <- getIState
165 indentWith <- getIndentWith
166 let (before, tyline : later) = splitAt (l-1) (lines src)
167 let ind = getIndent tyline
168-- runIO . traceIO $ "indentWith = " ++ show indentWith
169 let with = mkWith tyline n indentWith
170 -- add clause before first blank line in 'later',
171 -- or (TODO) before first line with same indentation as tyline
172 let (nonblank, rest) = span (\x -> not (all isSpace x) &&
173 not (ind == getIndent x)) later
174 if updatefile
175 then do
176 let fb = fn ++ "~"
177 runIO $ writeSource fb (unlines (before ++ nonblank) ++
178 with ++ "\n" ++ unlines rest)
179 runIO $ copyFile fb fn
180 else iPrintResult (with ++ "\n")
181 where getIndent s = length (takeWhile isSpace s)
183-- Replace the given metavariable on the given line with a 'case'
184-- block, using a _ for the scrutinee
185makeCase :: FilePath -> Bool -> Int -> Name -> Idris ()
186makeCase fn updatefile l n
187 = do src <- runIO $ readSourceStrict fn
188 let (before, tyline : later) = splitAt (l-1) (lines src)
189 let newcase = addCaseSkel (show n) tyline
191 if updatefile then
192 do let fb = fn ++ "~"
193 runIO $ writeSource fb (unlines (before ++ newcase ++ later))
194 runIO $ copyFile fb fn
195 else iPrintResult (showSep "\n" newcase ++"\n")
196 where addCaseSkel n line =
197 let b = brackets False line in
198 case findSubstr ('?':n) line of
199 Just (before, pos, after) ->
200 [before ++ (if b then "(" else "") ++ "case _ of",
201 take (pos + (if b then 6 else 5)) (repeat ' ') ++
202 "case_val => ?" ++ n ++ (if b then ")" else "")
203 ++ after]
204 Nothing -> fail "No such metavariable"
206 -- Assume case needs to be bracketed unless the metavariable is
207 -- on its own after an =
208 brackets eq line | line == '?' : show n = not eq
209 brackets eq ('=':ls) = brackets True ls
210 brackets eq (' ':ls) = brackets eq ls
211 brackets eq (l : ls) = brackets False ls
212 brackets eq [] = True
214 findSubstr n xs = findSubstr' [] 0 n xs
216 findSubstr' acc i n xs | take (length n) xs == n
217 = Just (reverse acc, i, drop (length n) xs)
218 findSubstr' acc i n [] = Nothing
219 findSubstr' acc i n (x : xs) = findSubstr' (x : acc) (i + 1) n xs
222doProofSearch :: FilePath -> Bool -> Bool ->
223 Int -> Name -> [Name] -> Maybe Int -> Idris ()
224doProofSearch fn updatefile rec l n hints Nothing
225 = doProofSearch fn updatefile rec l n hints (Just 20)
226doProofSearch fn updatefile rec l n hints (Just depth)
227 = do src <- runIO $ readSourceStrict fn
228 let (before, tyline : later) = splitAt (l-1) (lines src)
229 ctxt <- getContext
230 mn <- case lookupNames n ctxt of
231 [x] -> return x
232 [] -> return n
233 ns -> ierror (CantResolveAlts ns)
234 i <- getIState
235 let (top, envlen, psnames)
236 = case lookup mn (idris_metavars i) of
237 Just (t, e, ns, False, d) -> (t, e, ns)
238 _ -> (Nothing, 0, [])
239 let fc = fileFC fn
240 let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t psnames hints))
241 (ProofSearch rec False depth t psnames hints)]
242 let def = PClause fc mn (PRef fc [] mn) [] (body top) []
243 newmv_pre <- idrisCatch
244 (do elabDecl' EAll (recinfo (fileFC "proofsearch")) (PClauses fc [] mn [def])
245 (tm, ty) <- elabVal (recinfo (fileFC "proofsearch")) ERHS (PRef fc [] mn)
246 ctxt <- getContext
247 i <- getIState
248 return . flip displayS "" . renderPretty 1.0 80 $
249 pprintPTerm defaultPPOption [] [] (idris_infixes i)
250 (stripNS
251 (dropCtxt envlen
252 (delab i (fst (specialise ctxt [] [(mn, 1)] tm))))))
253 (\e -> return ("?" ++ show n))
254 let newmv = guessBrackets False tyline (show n) newmv_pre
255 if updatefile then
256 do let fb = fn ++ "~"
257 runIO $ writeSource fb (unlines before ++
258 updateMeta tyline (show n) newmv ++ "\n"
259 ++ unlines later)
260 runIO $ copyFile fb fn
261 else iPrintResult newmv
262 where dropCtxt 0 sc = sc
263 dropCtxt i (PPi _ _ _ _ sc) = dropCtxt (i - 1) sc
264 dropCtxt i (PLet _ _ _ _ _ sc) = dropCtxt (i - 1) sc
265 dropCtxt i (PLam _ _ _ _ sc) = dropCtxt (i - 1) sc
266 dropCtxt _ t = t
268 stripNS tm = mapPT dens tm where
269 dens (PRef fc hls n) = PRef fc hls (nsroot n)
270 dens t = t
272 nsroot (NS n _) = nsroot n
273 nsroot (SN (WhereN _ _ n)) = nsroot n
274 nsroot n = n
276updateMeta ('?':cs) n new
277 | length cs >= length n
278 = case splitAt (length n) cs of
279 (mv, c:cs) ->
280 if ((isSpace c || c == ')' || c == '}') && mv == n)
281 then new ++ (c : cs)
282 else '?' : mv ++ c : updateMeta cs n new
283 (mv, []) -> if (mv == n) then new else '?' : mv
284updateMeta ('=':'>':cs) n new = '=':'>':updateMeta cs n new
285updateMeta ('=':cs) n new = '=':updateMeta cs n new
286updateMeta (c:cs) n new
287 = c : updateMeta cs n new
288updateMeta [] n new = ""
290guessBrackets brack ('?':cs) n new
291 | length cs >= length n
292 = case splitAt (length n) cs of
293 (mv, c:cs) ->
294 if ((isSpace c || c == ')' || c == '}') && mv == n)
295 then addBracket brack new
296 else guessBrackets True cs n new
297 (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
298guessBrackets brack ('=':'>':cs) n new = guessBrackets False cs n new
299guessBrackets brack ('-':'>':cs) n new = guessBrackets False cs n new
300guessBrackets brack ('=':cs) n new = guessBrackets False cs n new
301guessBrackets brack (c:cs) n new
302 = guessBrackets (brack || not (isSpace c)) cs n new
303guessBrackets brack [] n new = ""
305checkProv line n = isProv' False line n
306 where
307 isProv' p cs n | take (length n) cs == n = p
308 isProv' _ ('?':cs) n = isProv' False cs n
309 isProv' _ ('{':cs) n = isProv' True cs n
310 isProv' _ ('}':cs) n = isProv' True cs n
311 isProv' p (_:cs) n = isProv' p cs n
312 isProv' _ [] n = False
314addBracket False new = new
315addBracket True new@('(':xs) | last xs == ')' = new
316addBracket True new | any isSpace new = '(' : new ++ ")"
317 | otherwise = new
320makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()
321makeLemma fn updatefile l n
322 = do src <- runIO $ readSourceStrict fn
323 let (before, tyline : later) = splitAt (l-1) (lines src)
325 -- if the name is in braces, rather than preceded by a ?, treat it
326 -- as a lemma in a provisional definition
328 let isProv = checkProv tyline (show n)
330 ctxt <- getContext
331 (fname, mty_full) <- case lookupTyName n ctxt of
332 [t] -> return t
333 [] -> ierror (NoSuchVariable n)
334 ns -> ierror (CantResolveAlts (map fst ns))
336 i <- getIState
337 let mty = errReverse i mty_full
339 margs <- case lookup fname (idris_metavars i) of
340 Just (_, arity, _, _, _) -> return arity
341 _ -> return (-1)
343 if (not isProv) then do
344 let skip = guessImps i (tt_ctxt i) mty
345 let impty = stripMNBind skip margs (delab i mty)
346 let interfaces = guessInterfaces i (tt_ctxt i) [] (allNamesIn impty) mty
348 let lem = show n ++ " : " ++
349 constraints i interfaces mty ++
350 showTmOpts (defaultPPOption { ppopt_pinames = True })
351 impty
352 let lem_app = guessBrackets False tyline (show n) (show n ++ appArgs skip margs mty)
354 if updatefile then
355 do let fb = fn ++ "~"
356 runIO $ writeSource fb (addLem before tyline lem lem_app later)
357 runIO $ copyFile fb fn
358 else case idris_outputmode i of
359 RawOutput _ -> iPrintResult $ lem ++ "\n" ++ lem_app
360 IdeMode n h ->
361 let good = SexpList [SymbolAtom "ok",
362 SexpList [SymbolAtom "metavariable-lemma",
363 SexpList [SymbolAtom "replace-metavariable",
364 StringAtom lem_app],
365 SexpList [SymbolAtom "definition-type",
366 StringAtom lem]]]
367 in runIO . hPutStrLn h $ convSExp "return" good n
369 else do -- provisional definition
370 let lem_app = show n ++ appArgs [] (-1) mty ++
371 " = ?" ++ show n ++ "_rhs"
372 if updatefile then
373 do let fb = fn ++ "~"
374 runIO $ writeSource fb (addProv before tyline lem_app later)
375 runIO $ copyFile fb fn
376 else case idris_outputmode i of
377 RawOutput _ -> iPrintResult lem_app
378 IdeMode n h ->
379 let good = SexpList [SymbolAtom "ok",
380 SexpList [SymbolAtom "provisional-definition-lemma",
381 SexpList [SymbolAtom "definition-clause",
382 StringAtom lem_app]]]
383 in runIO . hPutStrLn h $ convSExp "return" good n
385 where getIndent s = length (takeWhile isSpace s)
387 appArgs skip 0 _ = ""
388 appArgs skip i (Bind n@(UN c) (Pi _ _ _ _) sc)
389 | (thead c /= '_' && n `notElem` skip)
390 = " " ++ show n ++ appArgs skip (i - 1) sc
391 appArgs skip i (Bind _ (Pi _ _ _ _) sc) = appArgs skip (i - 1) sc
392 appArgs skip i _ = ""
394 stripMNBind _ args t | args <= 0 = stripImp t
395 stripMNBind skip args (PPi b n@(UN c) _ ty sc)
396 | n `notElem` skip ||
397 take 4 (str c) == "__pi" -- keep in type, but not in app
398 = PPi b n NoFC (stripImp ty) (stripMNBind skip (args - 1) sc)
399 stripMNBind skip args (PPi b _ _ ty sc) = stripMNBind skip (args - 1) sc
400 stripMNBind skip args t = stripImp t
402 stripImp (PApp fc f as) = PApp fc (stripImp f) (map placeholderImp as)
403 where
404 placeholderImp tm@(PImp _ _ _ _ _) = tm { getTm = Placeholder }
405 placeholderImp tm = tm { getTm = stripImp (getTm tm) }
406 stripImp (PPi b n f ty sc) = PPi b n f (stripImp ty) (stripImp sc)
407 stripImp t = t
409 constraints :: IState -> [Name] -> Type -> String
410 constraints i [] ty = ""
411 constraints i [n] ty = showSep ", " (showConstraints i [n] ty) ++ " => "
412 constraints i ns ty = "(" ++ showSep ", " (showConstraints i ns ty) ++ ") => "
414 showConstraints i ns (Bind n (Pi _ _ ty _) sc)
415 | n `elem` ns = show (delab i ty) :
416 showConstraints i ns (substV (P Bound n Erased) sc)
417 | otherwise = showConstraints i ns (substV (P Bound n Erased) sc)
418 showConstraints _ _ _ = []
420 -- Guess which binders should be implicits in the generated lemma.
421 -- Make them implicit if they appear guarded by a top level constructor,
422 -- or at the top level themselves.
423 -- Also, make interface implementations implicit
424 guessImps :: IState -> Context -> Term -> [Name]
425 -- machine names aren't lifted
426 guessImps ist ctxt (Bind n@(MN _ _) (Pi _ _ ty _) sc)
427 = n : guessImps ist ctxt sc
428 guessImps ist ctxt (Bind n (Pi _ _ ty _) sc)
429 | guarded ctxt n (substV (P Bound n Erased) sc)
430 = n : guessImps ist ctxt sc
431 | isInterface ist ty
432 = n : guessImps ist ctxt sc
433 | paramty ty = n : guessImps ist ctxt sc
434 | ignoreName n = n : guessImps ist ctxt sc
435 | otherwise = guessImps ist ctxt sc
436 guessImps ist ctxt _ = []
438 paramty (TType _) = True
439 paramty (Bind _ (Pi _ _ (TType _) _) sc) = paramty sc
440 paramty _ = False
442 -- TMP HACK unusable name so don't lift
443 ignoreName n = case show n of
444 "_aX" -> True
445 _ -> False
447 guessInterfaces :: IState -> Context -> [Name] -> [Name] -> Term -> [Name]
448 guessInterfaces ist ctxt binders usednames (Bind n (Pi _ _ ty _) sc)
449 | isParamInterface ist ty && any (\x -> elem x usednames)
450 (paramNames binders ty)
451 = n : guessInterfaces ist ctxt (n : binders) usednames sc
452 | otherwise = guessInterfaces ist ctxt (n : binders) usednames sc
453 guessInterfaces ist ctxt _ _ _ = []
455 paramNames bs ty | (P _ _ _, args) <- unApply ty
456 = vnames args
457 where vnames [] = []
458 vnames (V i : xs) | i < length bs = bs !! i : vnames xs
459 vnames (_ : xs) = vnames xs
461 isInterface ist t
462 | (P _ n _, args) <- unApply t
463 = case lookupCtxtExact n (idris_interfaces ist) of
464 Just _ -> True
465 _ -> False
466 | otherwise = False
468 isParamInterface ist t
469 | (P _ n _, args) <- unApply t
470 = case lookupCtxtExact n (idris_interfaces ist) of
471 Just _ -> any isV args
472 _ -> False
473 | otherwise = False
474 where isV (V _) = True
475 isV _ = False
477 guarded ctxt n (P _ n' _) | n == n' = True
478 guarded ctxt n ap@(App _ _ _)
479 | (P _ f _, args) <- unApply ap,
480 isConName f ctxt = any (guarded ctxt n) args
481-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows
482-- | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc
483 guarded ctxt n (Bind _ (Pi _ _ t _) sc)
484 = guarded ctxt n t || guarded ctxt n sc
485 guarded ctxt n _ = False
487 blank = all isSpace
489 addLem before tyline lem lem_app later
490 = let (bef_end, blankline : bef_start)
491 = case span (not . blank) (reverse before) of
492 (bef, []) -> (bef, [""])
493 x -> x
494 mvline = updateMeta tyline (show n) lem_app in
495 unlines $ reverse bef_start ++
496 [blankline, lem, blankline] ++
497 reverse bef_end ++ mvline : later
499 addProv before tyline lem_app later
500 = let (later_bef, blankline : later_end)
501 = case span (not . blank) later of
502 (bef, []) -> (bef, [""])
503 x -> x in
504 unlines $ before ++ tyline :
505 (later_bef ++ [blankline, lem_app, blankline] ++
506 later_end)