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