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