git.iko.soy/Idris-dev
on d773edd help sign in
Idris-dev/src/Idris/Interactive.hs
504 lines 22 kB history raw
1{-|
2Module : Idris.Interactive
3Description : Bits and pieces for editing source files interactively, called from the REPL
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 appArgs skip 0 _ = ""
386 appArgs skip i (Bind n@(UN c) (Pi _ _ _ _) sc)
387 | (thead c /= '_' && n `notElem` skip)
388 = " " ++ show n ++ appArgs skip (i - 1) sc
389 appArgs skip i (Bind _ (Pi _ _ _ _) sc) = appArgs skip (i - 1) sc
390 appArgs skip i _ = ""
392 stripMNBind _ args t | args <= 0 = stripImp t
393 stripMNBind skip args (PPi b n@(UN c) _ ty sc)
394 | n `notElem` skip ||
395 take 4 (str c) == "__pi" -- keep in type, but not in app
396 = PPi b n NoFC (stripImp ty) (stripMNBind skip (args - 1) sc)
397 stripMNBind skip args (PPi b _ _ ty sc) = stripMNBind skip (args - 1) sc
398 stripMNBind skip args t = stripImp t
400 stripImp (PApp fc f as) = PApp fc (stripImp f) (map placeholderImp as)
401 where
402 placeholderImp tm@(PImp _ _ _ _ _) = tm { getTm = Placeholder }
403 placeholderImp tm = tm { getTm = stripImp (getTm tm) }
404 stripImp (PPi b n f ty sc) = PPi b n f (stripImp ty) (stripImp sc)
405 stripImp t = t
407 constraints :: IState -> [Name] -> Type -> String
408 constraints i [] ty = ""
409 constraints i [n] ty = showSep ", " (showConstraints i [n] ty) ++ " => "
410 constraints i ns ty = "(" ++ showSep ", " (showConstraints i ns ty) ++ ") => "
412 showConstraints i ns (Bind n (Pi _ _ ty _) sc)
413 | n `elem` ns = show (delab i ty) :
414 showConstraints i ns (substV (P Bound n Erased) sc)
415 | otherwise = showConstraints i ns (substV (P Bound n Erased) sc)
416 showConstraints _ _ _ = []
418 -- Guess which binders should be implicits in the generated lemma.
419 -- Make them implicit if they appear guarded by a top level constructor,
420 -- or at the top level themselves.
421 -- Also, make interface implementations implicit
422 guessImps :: IState -> Context -> Term -> [Name]
423 -- machine names aren't lifted
424 guessImps ist ctxt (Bind n@(MN _ _) (Pi _ _ ty _) sc)
425 = n : guessImps ist ctxt sc
426 guessImps ist ctxt (Bind n (Pi _ _ ty _) sc)
427 | guarded ctxt n (substV (P Bound n Erased) sc)
428 = n : guessImps ist ctxt sc
429 | isInterface ist ty
430 = n : guessImps ist ctxt sc
431 | paramty ty = n : guessImps ist ctxt sc
432 | ignoreName n = n : guessImps ist ctxt sc
433 | otherwise = guessImps ist ctxt sc
434 guessImps ist ctxt _ = []
436 paramty (TType _) = True
437 paramty (Bind _ (Pi _ _ (TType _) _) sc) = paramty sc
438 paramty _ = False
440 -- TMP HACK unusable name so don't lift
441 ignoreName n = case show n of
442 "_aX" -> True
443 _ -> False
445 guessInterfaces :: IState -> Context -> [Name] -> [Name] -> Term -> [Name]
446 guessInterfaces ist ctxt binders usednames (Bind n (Pi _ _ ty _) sc)
447 | isParamInterface ist ty && any (\x -> elem x usednames)
448 (paramNames binders ty)
449 = n : guessInterfaces ist ctxt (n : binders) usednames sc
450 | otherwise = guessInterfaces ist ctxt (n : binders) usednames sc
451 guessInterfaces ist ctxt _ _ _ = []
453 paramNames bs ty | (P _ _ _, args) <- unApply ty
454 = vnames args
455 where vnames [] = []
456 vnames (V i : xs) | i < length bs = bs !! i : vnames xs
457 vnames (_ : xs) = vnames xs
459 isInterface ist t
460 | (P _ n _, args) <- unApply t
461 = case lookupCtxtExact n (idris_interfaces ist) of
462 Just _ -> True
463 _ -> False
464 | otherwise = False
466 isParamInterface ist t
467 | (P _ n _, args) <- unApply t
468 = case lookupCtxtExact n (idris_interfaces ist) of
469 Just _ -> any isV args
470 _ -> False
471 | otherwise = False
472 where isV (V _) = True
473 isV _ = False
475 guarded ctxt n (P _ n' _) | n == n' = True
476 guarded ctxt n ap@(App _ _ _)
477 | (P _ f _, args) <- unApply ap,
478 isConName f ctxt = any (guarded ctxt n) args
479-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows
480-- | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc
481 guarded ctxt n (Bind _ (Pi _ _ t _) sc)
482 = guarded ctxt n t || guarded ctxt n sc
483 guarded ctxt n _ = False
485 blank = all isSpace
487 addLem before tyline lem lem_app later
488 = let (bef_end, blankline : bef_start)
489 = case span (not . blank) (reverse before) of
490 (bef, []) -> (bef, [""])
491 x -> x
492 mvline = updateMeta tyline (show n) lem_app in
493 unlines $ reverse bef_start ++
494 [blankline, lem, blankline] ++
495 reverse bef_end ++ mvline : later
497 addProv before tyline lem_app later
498 = let (later_bef, blankline : later_end)
499 = case span (not . blank) later of
500 (bef, []) -> (bef, [""])
501 x -> x in
502 unlines $ before ++ tyline :
503 (later_bef ++ [blankline, lem_app, blankline] ++
504 later_end)