git.iko.soy/Idris-dev
on 008fb1f help sign in
Idris-dev/src/Idris/Interactive.hs
508 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 $ readSource 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 $ readSource 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 $ readSource 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 $ readSource fn
113 let (before, tyline : later) = splitAt (l-1) (lines src)
114 let indent = getIndent 0 (show n) 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 ""
129 else "\n" ++ unlines rest))
130 runIO $ 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 i n [] = 0
159 getIndent i n xs | take (length n) xs == n = i
160 getIndent i n (x : xs) = getIndent (i + 1) n xs
163makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()
164makeWith fn updatefile l n = do
165 src <- runIO $ readSource fn
166 i <- getIState
167 indentWith <- getIndentWith
168 let (before, tyline : later) = splitAt (l-1) (lines src)
169 let ind = getIndent tyline
170-- runIO . traceIO $ "indentWith = " ++ show indentWith
171 let with = mkWith tyline n indentWith
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
177 then do
178 let fb = fn ++ "~"
179 runIO $ writeSource fb (unlines (before ++ nonblank) ++
180 with ++ "\n" ++ 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
224doProofSearch :: FilePath -> Bool -> Bool ->
225 Int -> Name -> [Name] -> Maybe Int -> Idris ()
226doProofSearch fn updatefile rec l n hints Nothing
227 = doProofSearch fn updatefile rec l n hints (Just 20)
228doProofSearch fn updatefile rec l n hints (Just depth)
229 = do src <- runIO $ readSource fn
230 let (before, tyline : later) = splitAt (l-1) (lines src)
231 ctxt <- getContext
232 mn <- case lookupNames n ctxt of
233 [x] -> return x
234 [] -> return n
235 ns -> ierror (CantResolveAlts ns)
236 i <- getIState
237 let (top, envlen, psnames)
238 = case lookup mn (idris_metavars i) of
239 Just (t, e, ns, False, d) -> (t, e, ns)
240 _ -> (Nothing, 0, [])
241 let fc = fileFC fn
242 let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t psnames hints))
243 (ProofSearch rec False depth t psnames hints)]
244 let def = PClause fc mn (PRef fc [] mn) [] (body top) []
245 newmv_pre <- idrisCatch
246 (do elabDecl' EAll (recinfo (fileFC "proofsearch")) (PClauses fc [] mn [def])
247 (tm, ty) <- elabVal (recinfo (fileFC "proofsearch")) ERHS (PRef fc [] mn)
248 ctxt <- getContext
249 i <- getIState
250 return . flip displayS "" . renderPretty 1.0 80 $
251 pprintPTerm defaultPPOption [] [] (idris_infixes i)
252 (stripNS
253 (dropCtxt envlen
254 (delab i (fst (specialise ctxt [] [(mn, 1)] tm))))))
255 (\e -> return ("?" ++ show n))
256 let newmv = guessBrackets False tyline (show n) newmv_pre
257 if updatefile then
258 do let fb = fn ++ "~"
259 runIO $ writeSource fb (unlines before ++
260 updateMeta tyline (show n) newmv ++ "\n"
261 ++ unlines later)
262 runIO $ copyFile fb fn
263 else iPrintResult newmv
264 where dropCtxt 0 sc = sc
265 dropCtxt i (PPi _ _ _ _ sc) = dropCtxt (i - 1) sc
266 dropCtxt i (PLet _ _ _ _ _ sc) = dropCtxt (i - 1) sc
267 dropCtxt i (PLam _ _ _ _ sc) = dropCtxt (i - 1) sc
268 dropCtxt _ t = t
270 stripNS tm = mapPT dens tm where
271 dens (PRef fc hls n) = PRef fc hls (nsroot n)
272 dens t = t
274 nsroot (NS n _) = nsroot n
275 nsroot (SN (WhereN _ _ n)) = nsroot n
276 nsroot n = n
278updateMeta ('?':cs) n new
279 | length cs >= length n
280 = case splitAt (length n) cs of
281 (mv, c:cs) ->
282 if ((isSpace c || c == ')' || c == '}') && mv == n)
283 then new ++ (c : cs)
284 else '?' : mv ++ c : updateMeta cs n new
285 (mv, []) -> if (mv == n) then new else '?' : mv
286updateMeta ('=':'>':cs) n new = '=':'>':updateMeta cs n new
287updateMeta ('=':cs) n new = '=':updateMeta cs n new
288updateMeta (c:cs) n new
289 = c : updateMeta cs n new
290updateMeta [] n new = ""
292guessBrackets brack ('?':cs) n new
293 | length cs >= length n
294 = case splitAt (length n) cs of
295 (mv, c:cs) ->
296 if ((isSpace c || c == ')' || c == '}') && mv == n)
297 then addBracket brack new
298 else guessBrackets True cs n new
299 (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
300guessBrackets brack ('=':'>':cs) n new = guessBrackets False cs n new
301guessBrackets brack ('-':'>':cs) n new = guessBrackets False cs n new
302guessBrackets brack ('=':cs) n new = guessBrackets False cs n new
303guessBrackets brack (c:cs) n new
304 = guessBrackets (brack || not (isSpace c)) cs n new
305guessBrackets brack [] n new = ""
307checkProv line n = isProv' False line n
308 where
309 isProv' p cs n | take (length n) cs == n = p
310 isProv' _ ('?':cs) n = isProv' False cs n
311 isProv' _ ('{':cs) n = isProv' True cs n
312 isProv' _ ('}':cs) n = isProv' True cs n
313 isProv' p (_:cs) n = isProv' p cs n
314 isProv' _ [] n = False
316addBracket False new = new
317addBracket True new@('(':xs) | last xs == ')' = new
318addBracket True new | any isSpace new = '(' : new ++ ")"
319 | otherwise = new
322makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()
323makeLemma fn updatefile l n
324 = do src <- runIO $ readSource fn
325 let (before, tyline : later) = splitAt (l-1) (lines src)
327 -- if the name is in braces, rather than preceded by a ?, treat it
328 -- as a lemma in a provisional definition
330 let isProv = checkProv tyline (show n)
332 ctxt <- getContext
333 (fname, mty_full) <- case lookupTyName n ctxt of
334 [t] -> return t
335 [] -> ierror (NoSuchVariable n)
336 ns -> ierror (CantResolveAlts (map fst ns))
338 i <- getIState
339 let mty = errReverse i mty_full
341 margs <- case lookup fname (idris_metavars i) of
342 Just (_, arity, _, _, _) -> return arity
343 _ -> return (-1)
345 if (not isProv) then do
346 let skip = guessImps i (tt_ctxt i) mty
347 let impty = stripMNBind skip margs (delab i mty)
348 let interfaces = guessInterfaces i (tt_ctxt i) [] (allNamesIn impty) mty
350 let lem = show n ++ " : " ++
351 constraints i interfaces mty ++
352 showTmOpts (defaultPPOption { ppopt_pinames = True })
353 impty
354 let lem_app = guessBrackets False tyline (show n) (show n ++ appArgs skip margs mty)
356 if updatefile then
357 do let fb = fn ++ "~"
358 runIO $ writeSource fb (addLem before tyline lem lem_app later)
359 runIO $ copyFile fb fn
360 else case idris_outputmode i of
361 RawOutput _ -> iPrintResult $ lem ++ "\n" ++ lem_app
362 IdeMode n h ->
363 let good = SexpList [SymbolAtom "ok",
364 SexpList [SymbolAtom "metavariable-lemma",
365 SexpList [SymbolAtom "replace-metavariable",
366 StringAtom lem_app],
367 SexpList [SymbolAtom "definition-type",
368 StringAtom lem]]]
369 in runIO . hPutStrLn h $ convSExp "return" good n
371 else do -- provisional definition
372 let lem_app = show n ++ appArgs [] (-1) mty ++
373 " = ?" ++ show n ++ "_rhs"
374 if updatefile then
375 do let fb = fn ++ "~"
376 runIO $ writeSource fb (addProv before tyline lem_app later)
377 runIO $ copyFile fb fn
378 else case idris_outputmode i of
379 RawOutput _ -> iPrintResult lem_app
380 IdeMode n h ->
381 let good = SexpList [SymbolAtom "ok",
382 SexpList [SymbolAtom "provisional-definition-lemma",
383 SexpList [SymbolAtom "definition-clause",
384 StringAtom lem_app]]]
385 in runIO . hPutStrLn h $ convSExp "return" good n
387 where getIndent s = length (takeWhile isSpace s)
389 appArgs skip 0 _ = ""
390 appArgs skip i (Bind n@(UN c) (Pi _ _ _ _) sc)
391 | (thead c /= '_' && n `notElem` skip)
392 = " " ++ show n ++ appArgs skip (i - 1) sc
393 appArgs skip i (Bind _ (Pi _ _ _ _) sc) = appArgs skip (i - 1) sc
394 appArgs skip i _ = ""
396 stripMNBind _ args t | args <= 0 = stripImp t
397 stripMNBind skip args (PPi b n@(UN c) _ ty sc)
398 | n `notElem` skip ||
399 take 4 (str c) == "__pi" -- keep in type, but not in app
400 = PPi b n NoFC (stripImp ty) (stripMNBind skip (args - 1) sc)
401 stripMNBind skip args (PPi b _ _ ty sc) = stripMNBind skip (args - 1) sc
402 stripMNBind skip args t = stripImp t
404 stripImp (PApp fc f as) = PApp fc (stripImp f) (map placeholderImp as)
405 where
406 placeholderImp tm@(PImp _ _ _ _ _) = tm { getTm = Placeholder }
407 placeholderImp tm = tm { getTm = stripImp (getTm tm) }
408 stripImp (PPi b n f ty sc) = PPi b n f (stripImp ty) (stripImp sc)
409 stripImp t = t
411 constraints :: IState -> [Name] -> Type -> String
412 constraints i [] ty = ""
413 constraints i [n] ty = showSep ", " (showConstraints i [n] ty) ++ " => "
414 constraints i ns ty = "(" ++ showSep ", " (showConstraints i ns ty) ++ ") => "
416 showConstraints i ns (Bind n (Pi _ _ ty _) sc)
417 | n `elem` ns = show (delab i ty) :
418 showConstraints i ns (substV (P Bound n Erased) sc)
419 | otherwise = showConstraints i ns (substV (P Bound n Erased) sc)
420 showConstraints _ _ _ = []
422 -- Guess which binders should be implicits in the generated lemma.
423 -- Make them implicit if they appear guarded by a top level constructor,
424 -- or at the top level themselves.
425 -- Also, make interface implementations implicit
426 guessImps :: IState -> Context -> Term -> [Name]
427 -- machine names aren't lifted
428 guessImps ist ctxt (Bind n@(MN _ _) (Pi _ _ ty _) sc)
429 = n : guessImps ist ctxt sc
430 guessImps ist ctxt (Bind n (Pi _ _ ty _) sc)
431 | guarded ctxt n (substV (P Bound n Erased) sc)
432 = n : guessImps ist ctxt sc
433 | isInterface ist ty
434 = n : guessImps ist ctxt sc
435 | paramty ty = n : guessImps ist ctxt sc
436 | ignoreName n = n : guessImps ist ctxt sc
437 | otherwise = guessImps ist ctxt sc
438 guessImps ist ctxt _ = []
440 paramty (TType _) = True
441 paramty (Bind _ (Pi _ _ (TType _) _) sc) = paramty sc
442 paramty _ = False
444 -- TMP HACK unusable name so don't lift
445 ignoreName n = case show n of
446 "_aX" -> True
447 _ -> False
449 guessInterfaces :: IState -> Context -> [Name] -> [Name] -> Term -> [Name]
450 guessInterfaces ist ctxt binders usednames (Bind n (Pi _ _ ty _) sc)
451 | isParamInterface ist ty && any (\x -> elem x usednames)
452 (paramNames binders ty)
453 = n : guessInterfaces ist ctxt (n : binders) usednames sc
454 | otherwise = guessInterfaces ist ctxt (n : binders) usednames sc
455 guessInterfaces ist ctxt _ _ _ = []
457 paramNames bs ty | (P _ _ _, args) <- unApply ty
458 = vnames args
459 where vnames [] = []
460 vnames (V i : xs) | i < length bs = bs !! i : vnames xs
461 vnames (_ : xs) = vnames xs
463 isInterface ist t
464 | (P _ n _, args) <- unApply t
465 = case lookupCtxtExact n (idris_interfaces ist) of
466 Just _ -> True
467 _ -> False
468 | otherwise = False
470 isParamInterface ist t
471 | (P _ n _, args) <- unApply t
472 = case lookupCtxtExact n (idris_interfaces ist) of
473 Just _ -> any isV args
474 _ -> False
475 | otherwise = False
476 where isV (V _) = True
477 isV _ = False
479 guarded ctxt n (P _ n' _) | n == n' = True
480 guarded ctxt n ap@(App _ _ _)
481 | (P _ f _, args) <- unApply ap,
482 isConName f ctxt = any (guarded ctxt n) args
483-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows
484-- | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc
485 guarded ctxt n (Bind _ (Pi _ _ t _) sc)
486 = guarded ctxt n t || guarded ctxt n sc
487 guarded ctxt n _ = False
489 blank = all isSpace
491 addLem before tyline lem lem_app later
492 = let (bef_end, blankline : bef_start)
493 = case span (not . blank) (reverse before) of
494 (bef, []) -> (bef, [""])
495 x -> x
496 mvline = updateMeta tyline (show n) lem_app in
497 unlines $ reverse bef_start ++
498 [blankline, lem, blankline] ++
499 reverse bef_end ++ mvline : later
501 addProv before tyline lem_app later
502 = let (later_bef, blankline : later_end)
503 = case span (not . blank) later of
504 (bef, []) -> (bef, [""])
505 x -> x in
506 unlines $ before ++ tyline :
507 (later_bef ++ [blankline, lem_app, blankline] ++
508 later_end)