git.iko.soy/Idris-dev
on da672ec help sign in
Idris-dev/src/Idris/Interactive.hs
465 lines 20 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 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
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
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) -> (t, e, ns, False)
236 _ -> (Nothing, 0, [], True)
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 <- 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 if updatefile then
253 do let fb = fn ++ "~"
254 runIO $ writeSource fb (unlines before ++
255 updateMeta False tyline (show n) newmv ++ "\n"
256 ++ unlines later)
257 runIO $ copyFile fb fn
258 else iPrintResult newmv
259 where dropCtxt 0 sc = sc
260 dropCtxt i (PPi _ _ _ _ sc) = dropCtxt (i - 1) sc
261 dropCtxt i (PLet _ _ _ _ _ sc) = dropCtxt (i - 1) sc
262 dropCtxt i (PLam _ _ _ _ sc) = dropCtxt (i - 1) sc
263 dropCtxt _ t = t
265 stripNS tm = mapPT dens tm where
266 dens (PRef fc hls n) = PRef fc hls (nsroot n)
267 dens t = t
269 nsroot (NS n _) = nsroot n
270 nsroot (SN (WhereN _ _ n)) = nsroot n
271 nsroot n = n
273updateMeta brack ('?':cs) n new
274 | length cs >= length n
275 = case splitAt (length n) cs of
276 (mv, c:cs) ->
277 if ((isSpace c || c == ')' || c == '}') && mv == n)
278 then addBracket brack new ++ (c : cs)
279 else '?' : mv ++ c : updateMeta True cs n new
280 (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
281updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new
282updateMeta brack (c:cs) n new
283 = c : updateMeta (brack || not (isSpace c)) cs n new
284updateMeta brack [] n new = ""
286checkProv line n = isProv' False line n
287 where
288 isProv' p cs n | take (length n) cs == n = p
289 isProv' _ ('?':cs) n = isProv' False cs n
290 isProv' _ ('{':cs) n = isProv' True cs n
291 isProv' _ ('}':cs) n = isProv' True cs n
292 isProv' p (_:cs) n = isProv' p cs n
293 isProv' _ [] n = False
295addBracket False new = new
296addBracket True new@('(':xs) | last xs == ')' = new
297addBracket True new | any isSpace new = '(' : new ++ ")"
298 | otherwise = new
301makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()
302makeLemma fn updatefile l n
303 = do src <- runIO $ readSource fn
304 let (before, tyline : later) = splitAt (l-1) (lines src)
306 -- if the name is in braces, rather than preceded by a ?, treat it
307 -- as a lemma in a provisional definition
309 let isProv = checkProv tyline (show n)
311 ctxt <- getContext
312 (fname, mty) <- case lookupTyName n ctxt of
313 [t] -> return t
314 [] -> ierror (NoSuchVariable n)
315 ns -> ierror (CantResolveAlts (map fst ns))
316 i <- getIState
317 margs <- case lookup fname (idris_metavars i) of
318 Just (_, arity, _, _) -> return arity
319 _ -> return (-1)
321 if (not isProv) then do
322 let skip = guessImps i (tt_ctxt i) mty
323 let classes = guessClasses i (tt_ctxt i) mty
325 let lem = show n ++ " : " ++
326 constraints i classes mty ++
327 showTmOpts (defaultPPOption { ppopt_pinames = True })
328 (stripMNBind skip margs (delab i mty))
329 let lem_app = show n ++ appArgs skip margs mty
331 if updatefile then
332 do let fb = fn ++ "~"
333 runIO $ writeSource fb (addLem before tyline lem lem_app later)
334 runIO $ copyFile fb fn
335 else case idris_outputmode i of
336 RawOutput _ -> iPrintResult $ lem ++ "\n" ++ lem_app
337 IdeMode n h ->
338 let good = SexpList [SymbolAtom "ok",
339 SexpList [SymbolAtom "metavariable-lemma",
340 SexpList [SymbolAtom "replace-metavariable",
341 StringAtom lem_app],
342 SexpList [SymbolAtom "definition-type",
343 StringAtom lem]]]
344 in runIO . hPutStrLn h $ convSExp "return" good n
346 else do -- provisional definition
347 let lem_app = show n ++ appArgs [] (-1) mty ++
348 " = ?" ++ show n ++ "_rhs"
349 if updatefile then
350 do let fb = fn ++ "~"
351 runIO $ writeSource fb (addProv before tyline lem_app later)
352 runIO $ copyFile fb fn
353 else case idris_outputmode i of
354 RawOutput _ -> iPrintResult $ lem_app
355 IdeMode n h ->
356 let good = SexpList [SymbolAtom "ok",
357 SexpList [SymbolAtom "provisional-definition-lemma",
358 SexpList [SymbolAtom "definition-clause",
359 StringAtom lem_app]]]
360 in runIO . hPutStrLn h $ convSExp "return" good n
362 where getIndent s = length (takeWhile isSpace s)
364 appArgs skip 0 _ = ""
365 appArgs skip i (Bind n@(UN c) (Pi _ _ _) sc)
366 | (thead c /= '_' && n `notElem` skip)
367 = " " ++ show n ++ appArgs skip (i - 1) sc
368 appArgs skip i (Bind _ (Pi _ _ _) sc) = appArgs skip (i - 1) sc
369 appArgs skip i _ = ""
371 stripMNBind _ args t | args <= 0 = t
372 stripMNBind skip args (PPi b n@(UN c) _ ty sc)
373 | n `notElem` skip ||
374 take 4 (str c) == "__pi" -- keep in type, but not in app
375 = PPi b n NoFC ty (stripMNBind skip (args - 1) sc)
376 stripMNBind skip args (PPi b _ _ ty sc) = stripMNBind skip (args - 1) sc
377 stripMNBind skip args t = t
379 constraints :: IState -> [Name] -> Type -> String
380 constraints i [] ty = ""
381 constraints i [n] ty = showSep ", " (showConstraints i [n] ty) ++ " => "
382 constraints i ns ty = "(" ++ showSep ", " (showConstraints i ns ty) ++ ") => "
384 showConstraints i ns (Bind n (Pi _ ty _) sc)
385 | n `elem` ns = show (delab i ty) :
386 showConstraints i ns (substV (P Bound n Erased) sc)
387 | otherwise = showConstraints i ns (substV (P Bound n Erased) sc)
388 showConstraints _ _ _ = []
390 -- Guess which binders should be implicits in the generated lemma.
391 -- Make them implicit if they appear guarded by a top level constructor,
392 -- or at the top level themselves.
393 -- Also, make type class instances implicit
394 guessImps :: IState -> Context -> Term -> [Name]
395 -- machine names aren't lifted
396 guessImps ist ctxt (Bind n@(MN _ _) (Pi _ ty _) sc)
397 = n : guessImps ist ctxt sc
398 guessImps ist ctxt (Bind n (Pi _ ty _) sc)
399 | guarded ctxt n (substV (P Bound n Erased) sc)
400 = n : guessImps ist ctxt sc
401 | isClass ist ty
402 = n : guessImps ist ctxt sc
403 | TType _ <- ty = n : guessImps ist ctxt sc
404 | ignoreName n = n : guessImps ist ctxt sc
405 | otherwise = guessImps ist ctxt sc
406 guessImps ist ctxt _ = []
408 -- TMP HACK unusable name so don't lift
409 ignoreName n = case show n of
410 "_aX" -> True
411 _ -> False
413 guessClasses :: IState -> Context -> Term -> [Name]
414 guessClasses ist ctxt (Bind n (Pi _ ty _) sc)
415 | isParamClass ist ty
416 = n : guessClasses ist ctxt sc
417 | otherwise = guessClasses ist ctxt sc
418 guessClasses ist ctxt _ = []
420 isClass ist t
421 | (P _ n _, args) <- unApply t
422 = case lookupCtxtExact n (idris_classes ist) of
423 Just _ -> True
424 _ -> False
425 | otherwise = False
427 isParamClass ist t
428 | (P _ n _, args) <- unApply t
429 = case lookupCtxtExact n (idris_classes ist) of
430 Just _ -> any isV args
431 _ -> False
432 | otherwise = False
433 where isV (V _) = True
434 isV _ = False
436 guarded ctxt n (P _ n' _) | n == n' = True
437 guarded ctxt n ap@(App _ _ _)
438 | (P _ f _, args) <- unApply ap,
439 isConName f ctxt = any (guarded ctxt n) args
440-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows
441-- | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc
442 guarded ctxt n (Bind _ (Pi _ t _) sc)
443 = guarded ctxt n t || guarded ctxt n sc
444 guarded ctxt n _ = False
446 blank = all isSpace
448 addLem before tyline lem lem_app later
449 = let (bef_end, blankline : bef_start)
450 = case span (not . blank) (reverse before) of
451 (bef, []) -> (bef, "" : [])
452 x -> x
453 mvline = updateMeta False tyline (show n) lem_app in
454 unlines $ reverse bef_start ++
455 [blankline, lem, blankline] ++
456 reverse bef_end ++ mvline : later
458 addProv before tyline lem_app later
459 = let (later_bef, blankline : later_end)
460 = case span (not . blank) later of
461 (bef, []) -> (bef, "" : [])
462 x -> x in
463 unlines $ before ++ tyline :
464 (later_bef ++ [blankline, lem_app, blankline] ++
465 later_end)