git.iko.soy/Idris-dev
on 239c8ca help sign in
Idris-dev/src/Idris/Interactive.hs
448 lines 19 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
51 = do src <- runIO $ readSource fn
52 let (before, tyline : later) = splitAt (l-1) (lines src)
53 let indent = getIndent 0 (show n) tyline
54 cl <- getClause l n fn
55 -- add clause before first blank line in 'later'
56 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
57 if updatefile
58 then do let fb = fn ++ "~"
59 runIO $ writeSource fb (unlines (before ++ nonblank) ++
60 replicate indent ' ' ++
61 cl ++ "\n" ++
62 unlines rest)
63 runIO $ copyFile fb fn
64 else iPrintResult cl
65 where
66 getIndent i n [] = 0
67 getIndent i n xs | take 9 xs == "instance " = i
68 getIndent i n xs | take (length n) xs == n = i
69 getIndent i n (x : xs) = getIndent (i + 1) n xs
71addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
72addProofClauseFrom fn updatefile l n
73 = do src <- runIO $ readSource fn
74 let (before, tyline : later) = splitAt (l-1) (lines src)
75 let indent = getIndent 0 (show n) tyline
76 cl <- getProofClause l n fn
77 -- add clause before first blank line in 'later'
78 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
79 if updatefile
80 then do let fb = fn ++ "~"
81 runIO $ writeSource fb (unlines (before ++ nonblank) ++
82 replicate indent ' ' ++
83 cl ++ "\n" ++
84 unlines rest)
85 runIO $ copyFile fb fn
86 else iPrintResult cl
87 where
88 getIndent i n [] = 0
89 getIndent i n xs | take (length n) xs == n = i
90 getIndent i n (x : xs) = getIndent (i + 1) n xs
92addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()
93addMissing 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 i <- getIState
98 cl <- getInternalApp fn l
99 let n' = getAppName cl
101 extras <- case lookupCtxt n' (idris_patdefs i) of
102 [] -> return ""
103 [(_, tms)] -> do tms' <- nameMissing tms
104 showNew (show n ++ "_rhs") 1 indent tms'
105 other -> return "" -- happens if called on a metavar, or with no clauses
106 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
107 if updatefile
108 then do let fb = fn ++ "~"
109 runIO $ writeSource fb (unlines (before ++ nonblank)
110 ++ extras ++ unlines rest)
111 runIO $ copyFile fb fn
112 else iPrintResult extras
113 where showPat = show . stripNS
114 stripNS tm = mapPT dens tm where
115 dens (PRef fc hls n) = PRef fc hls (nsroot n)
116 dens t = t
118 nsroot (NS n _) = nsroot n
119 nsroot (SN (WhereN _ _ n)) = nsroot n
120 nsroot n = n
122 getAppName (PApp _ r _) = getAppName r
123 getAppName (PRef _ _ r) = r
124 getAppName _ = n
126 makeIndent ind | ".lidr" `isSuffixOf` fn = '>' : ' ' : replicate (ind-2) ' '
127 | otherwise = replicate ind ' '
129 showNew nm i ind (tm : tms)
130 = do (nm', i') <- getUniq nm i
131 rest <- showNew nm i' ind tms
132 return (makeIndent ind ++
133 showPat tm ++ " = ?" ++ nm' ++
134 "\n" ++ rest)
135 showNew nm i _ [] = return ""
137 getIndent i n [] = 0
138 getIndent i n xs | take (length n) xs == n = i
139 getIndent i n (x : xs) = getIndent (i + 1) n xs
142makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()
143makeWith fn updatefile l n
144 = do src <- runIO $ readSource fn
145 let (before, tyline : later) = splitAt (l-1) (lines src)
146 let ind = getIndent tyline
147 let with = mkWith tyline n
148 -- add clause before first blank line in 'later',
149 -- or (TODO) before first line with same indentation as tyline
150 let (nonblank, rest) = span (\x -> not (all isSpace x) &&
151 not (ind == getIndent x)) later
152 if updatefile then
153 do let fb = fn ++ "~"
154 runIO $ writeSource fb (unlines (before ++ nonblank)
155 ++ with ++ "\n" ++
156 unlines rest)
157 runIO $ copyFile fb fn
158 else iPrintResult with
159 where getIndent s = length (takeWhile isSpace s)
161-- Replace the given metavariable on the given line with a 'case'
162-- block, using a _ for the scrutinee
163makeCase :: FilePath -> Bool -> Int -> Name -> Idris ()
164makeCase fn updatefile l n
165 = do src <- runIO $ readSource fn
166 let (before, tyline : later) = splitAt (l-1) (lines src)
167 let newcase = addCaseSkel (show n) tyline
169 if updatefile then
170 do let fb = fn ++ "~"
171 runIO $ writeSource fb (unlines (before ++ newcase ++ later))
172 runIO $ copyFile fb fn
173 else iPrintResult (showSep "\n" newcase)
174 where addCaseSkel n line =
175 let b = brackets False line in
176 case findSubstr ('?':n) line of
177 Just (before, pos, after) ->
178 [before ++ (if b then "(" else "") ++ "case _ of",
179 take (pos + (if b then 6 else 5)) (repeat ' ') ++
180 "case_val => ?" ++ n ++ if b then ")" else "",
181 after]
182 Nothing -> fail "No such metavariable"
184 -- Assume case needs to be bracketed unless the metavariable is
185 -- on its own after an =
186 brackets eq line | line == '?' : show n = not eq
187 brackets eq ('=':ls) = brackets True ls
188 brackets eq (' ':ls) = brackets eq ls
189 brackets eq (l : ls) = brackets False ls
190 brackets eq [] = True
192 findSubstr n xs = findSubstr' [] 0 n xs
194 findSubstr' acc i n xs | take (length n) xs == n
195 = Just (reverse acc, i, drop (length n) xs)
196 findSubstr' acc i n [] = Nothing
197 findSubstr' acc i n (x : xs) = findSubstr' (x : acc) (i + 1) n xs
203doProofSearch :: FilePath -> Bool -> Bool ->
204 Int -> Name -> [Name] -> Maybe Int -> Idris ()
205doProofSearch fn updatefile rec l n hints Nothing
206 = doProofSearch fn updatefile rec l n hints (Just 20)
207doProofSearch fn updatefile rec l n hints (Just depth)
208 = do src <- runIO $ readSource fn
209 let (before, tyline : later) = splitAt (l-1) (lines src)
210 ctxt <- getContext
211 mn <- case lookupNames n ctxt of
212 [x] -> return x
213 [] -> return n
214 ns -> ierror (CantResolveAlts ns)
215 i <- getIState
216 let (top, envlen, psnames, _)
217 = case lookup mn (idris_metavars i) of
218 Just (t, e, ns, False) -> (t, e, ns, False)
219 _ -> (Nothing, 0, [], True)
220 let fc = fileFC fn
221 let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t psnames hints))
222 (ProofSearch rec False depth t psnames hints)]
223 let def = PClause fc mn (PRef fc [] mn) [] (body top) []
224 newmv <- idrisCatch
225 (do elabDecl' EAll recinfo (PClauses fc [] mn [def])
226 (tm, ty) <- elabVal recinfo ERHS (PRef fc [] mn)
227 ctxt <- getContext
228 i <- getIState
229 return . flip displayS "" . renderPretty 1.0 80 $
230 pprintPTerm defaultPPOption [] [] (idris_infixes i)
231 (stripNS
232 (dropCtxt envlen
233 (delab i (fst (specialise ctxt [] [(mn, 1)] tm))))))
234 (\e -> return ("?" ++ show n))
235 if updatefile then
236 do let fb = fn ++ "~"
237 runIO $ writeSource fb (unlines before ++
238 updateMeta False tyline (show n) newmv ++ "\n"
239 ++ unlines later)
240 runIO $ copyFile fb fn
241 else iPrintResult newmv
242 where dropCtxt 0 sc = sc
243 dropCtxt i (PPi _ _ _ _ sc) = dropCtxt (i - 1) sc
244 dropCtxt i (PLet _ _ _ _ _ sc) = dropCtxt (i - 1) sc
245 dropCtxt i (PLam _ _ _ _ sc) = dropCtxt (i - 1) sc
246 dropCtxt _ t = t
248 stripNS tm = mapPT dens tm where
249 dens (PRef fc hls n) = PRef fc hls (nsroot n)
250 dens t = t
252 nsroot (NS n _) = nsroot n
253 nsroot (SN (WhereN _ _ n)) = nsroot n
254 nsroot n = n
256updateMeta brack ('?':cs) n new
257 | length cs >= length n
258 = case splitAt (length n) cs of
259 (mv, c:cs) ->
260 if ((isSpace c || c == ')' || c == '}') && mv == n)
261 then addBracket brack new ++ (c : cs)
262 else '?' : mv ++ c : updateMeta True cs n new
263 (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
264updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new
265updateMeta brack (c:cs) n new
266 = c : updateMeta (brack || not (isSpace c)) cs n new
267updateMeta brack [] n new = ""
269checkProv line n = isProv' False line n
270 where
271 isProv' p cs n | take (length n) cs == n = p
272 isProv' _ ('?':cs) n = isProv' False cs n
273 isProv' _ ('{':cs) n = isProv' True cs n
274 isProv' _ ('}':cs) n = isProv' True cs n
275 isProv' p (_:cs) n = isProv' p cs n
276 isProv' _ [] n = False
278addBracket False new = new
279addBracket True new@('(':xs) | last xs == ')' = new
280addBracket True new | any isSpace new = '(' : new ++ ")"
281 | otherwise = new
284makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()
285makeLemma fn updatefile l n
286 = do src <- runIO $ readSource fn
287 let (before, tyline : later) = splitAt (l-1) (lines src)
289 -- if the name is in braces, rather than preceded by a ?, treat it
290 -- as a lemma in a provisional definition
292 let isProv = checkProv tyline (show n)
294 ctxt <- getContext
295 (fname, mty) <- case lookupTyName n ctxt of
296 [t] -> return t
297 [] -> ierror (NoSuchVariable n)
298 ns -> ierror (CantResolveAlts (map fst ns))
299 i <- getIState
300 margs <- case lookup fname (idris_metavars i) of
301 Just (_, arity, _, _) -> return arity
302 _ -> return (-1)
304 if (not isProv) then do
305 let skip = guessImps i (tt_ctxt i) mty
306 let classes = guessClasses i (tt_ctxt i) mty
308 let lem = show n ++ " : " ++
309 constraints i classes mty ++
310 showTmOpts (defaultPPOption { ppopt_pinames = True })
311 (stripMNBind skip margs (delab i mty))
312 let lem_app = show n ++ appArgs skip margs mty
314 if updatefile then
315 do let fb = fn ++ "~"
316 runIO $ writeSource fb (addLem before tyline lem lem_app later)
317 runIO $ copyFile fb fn
318 else case idris_outputmode i of
319 RawOutput _ -> iPrintResult $ lem ++ "\n" ++ lem_app
320 IdeMode n h ->
321 let good = SexpList [SymbolAtom "ok",
322 SexpList [SymbolAtom "metavariable-lemma",
323 SexpList [SymbolAtom "replace-metavariable",
324 StringAtom lem_app],
325 SexpList [SymbolAtom "definition-type",
326 StringAtom lem]]]
327 in runIO . hPutStrLn h $ convSExp "return" good n
329 else do -- provisional definition
330 let lem_app = show n ++ appArgs [] (-1) mty ++
331 " = ?" ++ show n ++ "_rhs"
332 if updatefile then
333 do let fb = fn ++ "~"
334 runIO $ writeSource fb (addProv before tyline lem_app later)
335 runIO $ copyFile fb fn
336 else case idris_outputmode i of
337 RawOutput _ -> iPrintResult $ lem_app
338 IdeMode n h ->
339 let good = SexpList [SymbolAtom "ok",
340 SexpList [SymbolAtom "provisional-definition-lemma",
341 SexpList [SymbolAtom "definition-clause",
342 StringAtom lem_app]]]
343 in runIO . hPutStrLn h $ convSExp "return" good n
345 where getIndent s = length (takeWhile isSpace s)
347 appArgs skip 0 _ = ""
348 appArgs skip i (Bind n@(UN c) (Pi _ _ _) sc)
349 | (thead c /= '_' && n `notElem` skip)
350 = " " ++ show n ++ appArgs skip (i - 1) sc
351 appArgs skip i (Bind _ (Pi _ _ _) sc) = appArgs skip (i - 1) sc
352 appArgs skip i _ = ""
354 stripMNBind _ args t | args <= 0 = t
355 stripMNBind skip args (PPi b n@(UN c) _ ty sc)
356 | n `notElem` skip ||
357 take 4 (str c) == "__pi" -- keep in type, but not in app
358 = PPi b n NoFC ty (stripMNBind skip (args - 1) sc)
359 stripMNBind skip args (PPi b _ _ ty sc) = stripMNBind skip (args - 1) sc
360 stripMNBind skip args t = t
362 constraints :: IState -> [Name] -> Type -> String
363 constraints i [] ty = ""
364 constraints i [n] ty = showSep ", " (showConstraints i [n] ty) ++ " => "
365 constraints i ns ty = "(" ++ showSep ", " (showConstraints i ns ty) ++ ") => "
367 showConstraints i ns (Bind n (Pi _ ty _) sc)
368 | n `elem` ns = show (delab i ty) :
369 showConstraints i ns (substV (P Bound n Erased) sc)
370 | otherwise = showConstraints i ns (substV (P Bound n Erased) sc)
371 showConstraints _ _ _ = []
373 -- Guess which binders should be implicits in the generated lemma.
374 -- Make them implicit if they appear guarded by a top level constructor,
375 -- or at the top level themselves.
376 -- Also, make type class instances implicit
377 guessImps :: IState -> Context -> Term -> [Name]
378 -- machine names aren't lifted
379 guessImps ist ctxt (Bind n@(MN _ _) (Pi _ ty _) sc)
380 = n : guessImps ist ctxt sc
381 guessImps ist ctxt (Bind n (Pi _ ty _) sc)
382 | guarded ctxt n (substV (P Bound n Erased) sc)
383 = n : guessImps ist ctxt sc
384 | isClass ist ty
385 = n : guessImps ist ctxt sc
386 | TType _ <- ty = n : guessImps ist ctxt sc
387 | ignoreName n = n : guessImps ist ctxt sc
388 | otherwise = guessImps ist ctxt sc
389 guessImps ist ctxt _ = []
391 -- TMP HACK unusable name so don't lift
392 ignoreName n = case show n of
393 "_aX" -> True
394 _ -> False
396 guessClasses :: IState -> Context -> Term -> [Name]
397 guessClasses ist ctxt (Bind n (Pi _ ty _) sc)
398 | isParamClass ist ty
399 = n : guessClasses ist ctxt sc
400 | otherwise = guessClasses ist ctxt sc
401 guessClasses ist ctxt _ = []
403 isClass ist t
404 | (P _ n _, args) <- unApply t
405 = case lookupCtxtExact n (idris_classes ist) of
406 Just _ -> True
407 _ -> False
408 | otherwise = False
410 isParamClass ist t
411 | (P _ n _, args) <- unApply t
412 = case lookupCtxtExact n (idris_classes ist) of
413 Just _ -> any isV args
414 _ -> False
415 | otherwise = False
416 where isV (V _) = True
417 isV _ = False
419 guarded ctxt n (P _ n' _) | n == n' = True
420 guarded ctxt n ap@(App _ _ _)
421 | (P _ f _, args) <- unApply ap,
422 isConName f ctxt = any (guarded ctxt n) args
423-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows
424-- | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc
425 guarded ctxt n (Bind _ (Pi _ t _) sc)
426 = guarded ctxt n t || guarded ctxt n sc
427 guarded ctxt n _ = False
429 blank = all isSpace
431 addLem before tyline lem lem_app later
432 = let (bef_end, blankline : bef_start)
433 = case span (not . blank) (reverse before) of
434 (bef, []) -> (bef, "" : [])
435 x -> x
436 mvline = updateMeta False tyline (show n) lem_app in
437 unlines $ reverse bef_start ++
438 [blankline, lem, blankline] ++
439 reverse bef_end ++ mvline : later
441 addProv before tyline lem_app later
442 = let (later_bef, blankline : later_end)
443 = case span (not . blank) later of
444 (bef, []) -> (bef, "" : [])
445 x -> x in
446 unlines $ before ++ tyline :
447 (later_bef ++ [blankline, lem_app, blankline] ++
448 later_end)