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