git.iko.soy/Idris-dev
on b4dbebd help sign in
Idris-dev/src/Idris/Interactive.hs
353 lines 15 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.Interactive(caseSplitAt, addClauseFrom, addProofClauseFrom,
4 addMissing, makeWith, 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 iLOG (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 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
106 if updatefile
107 then do let fb = fn ++ "~"
108 runIO $ writeSource fb (unlines (before ++ nonblank)
109 ++ extras ++ unlines rest)
110 runIO $ copyFile fb fn
111 else iPrintResult extras
112 where showPat = show . stripNS
113 stripNS tm = mapPT dens tm where
114 dens (PRef fc n) = PRef fc (nsroot n)
115 dens t = t
117 nsroot (NS n _) = nsroot n
118 nsroot (SN (WhereN _ _ n)) = nsroot n
119 nsroot n = n
121 getAppName (PApp _ r _) = getAppName r
122 getAppName (PRef _ r) = r
123 getAppName _ = n
125 makeIndent ind | ".lidr" `isSuffixOf` fn = '>' : ' ' : replicate (ind-2) ' '
126 | otherwise = replicate ind ' '
128 showNew nm i ind (tm : tms)
129 = do (nm', i') <- getUniq nm i
130 rest <- showNew nm i' ind tms
131 return (makeIndent ind ++
132 showPat tm ++ " = ?" ++ nm' ++
133 "\n" ++ rest)
134 showNew nm i _ [] = return ""
136 getIndent i n [] = 0
137 getIndent i n xs | take (length n) xs == n = i
138 getIndent i n (x : xs) = getIndent (i + 1) n xs
141makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()
142makeWith fn updatefile l n
143 = do src <- runIO $ readSource fn
144 let (before, tyline : later) = splitAt (l-1) (lines src)
145 let ind = getIndent tyline
146 let with = mkWith tyline n
147 -- add clause before first blank line in 'later',
148 -- or (TODO) before first line with same indentation as tyline
149 let (nonblank, rest) = span (\x -> not (all isSpace x) &&
150 not (ind == getIndent x)) later
151 if updatefile then
152 do let fb = fn ++ "~"
153 runIO $ writeSource fb (unlines (before ++ nonblank)
154 ++ with ++ "\n" ++
155 unlines rest)
156 runIO $ copyFile fb fn
157 else iPrintResult with
158 where getIndent s = length (takeWhile isSpace s)
161doProofSearch :: FilePath -> Bool -> Bool ->
162 Int -> Name -> [Name] -> Maybe Int -> Idris ()
163doProofSearch fn updatefile rec l n hints Nothing
164 = doProofSearch fn updatefile rec l n hints (Just 10)
165doProofSearch fn updatefile rec l n hints (Just depth)
166 = do src <- runIO $ readSource fn
167 let (before, tyline : later) = splitAt (l-1) (lines src)
168 ctxt <- getContext
169 mn <- case lookupNames n ctxt of
170 [x] -> return x
171 [] -> return n
172 ns -> ierror (CantResolveAlts ns)
173 i <- getIState
174 let (top, envlen, _) = case lookup mn (idris_metavars i) of
175 Just (t, e, False) -> (t, e, False)
176 _ -> (Nothing, 0, True)
177 let fc = fileFC fn
178 let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t hints))
179 (ProofSearch rec False depth t hints)]
180 let def = PClause fc mn (PRef fc mn) [] (body top) []
181 newmv <- idrisCatch
182 (do elabDecl' EAll recinfo (PClauses fc [] mn [def])
183 (tm, ty) <- elabVal recinfo ERHS (PRef fc mn)
184 ctxt <- getContext
185 i <- getIState
186 return . flip displayS "" . renderPretty 1.0 80 $
187 pprintPTerm defaultPPOption [] [] (idris_infixes i)
188 (stripNS
189 (dropCtxt envlen
190 (delab i (fst (specialise ctxt [] [(mn, 1)] tm))))))
191 (\e -> return ("?" ++ show n))
192 if updatefile then
193 do let fb = fn ++ "~"
194 runIO $ writeSource fb (unlines before ++
195 updateMeta False tyline (show n) newmv ++ "\n"
196 ++ unlines later)
197 runIO $ copyFile fb fn
198 else iPrintResult newmv
199 where dropCtxt 0 sc = sc
200 dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc
201 dropCtxt i (PLet _ _ _ _ sc) = dropCtxt (i - 1) sc
202 dropCtxt i (PLam _ _ _ sc) = dropCtxt (i - 1) sc
203 dropCtxt _ t = t
205 stripNS tm = mapPT dens tm where
206 dens (PRef fc n) = PRef fc (nsroot n)
207 dens t = t
209 nsroot (NS n _) = nsroot n
210 nsroot (SN (WhereN _ _ n)) = nsroot n
211 nsroot n = n
213updateMeta brack ('?':cs) n new
214 | length cs >= length n
215 = case splitAt (length n) cs of
216 (mv, c:cs) ->
217 if ((isSpace c || c == ')' || c == '}') && mv == n)
218 then addBracket brack new ++ (c : cs)
219 else '?' : mv ++ c : updateMeta True cs n new
220 (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
221updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new
222updateMeta brack (c:cs) n new
223 = c : updateMeta (brack || not (isSpace c)) cs n new
224updateMeta brack [] n new = ""
226checkProv line n = isProv' False line n
227 where
228 isProv' p cs n | take (length n) cs == n = p
229 isProv' _ ('?':cs) n = isProv' False cs n
230 isProv' _ ('{':cs) n = isProv' True cs n
231 isProv' _ ('}':cs) n = isProv' True cs n
232 isProv' p (_:cs) n = isProv' p cs n
233 isProv' _ [] n = False
235addBracket False new = new
236addBracket True new@('(':xs) | last xs == ')' = new
237addBracket True new | any isSpace new = '(' : new ++ ")"
238 | otherwise = new
241makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()
242makeLemma fn updatefile l n
243 = do src <- runIO $ readSource fn
244 let (before, tyline : later) = splitAt (l-1) (lines src)
246 -- if the name is in braces, rather than preceded by a ?, treat it
247 -- as a lemma in a provisional definition
249 let isProv = checkProv tyline (show n)
251 ctxt <- getContext
252 mty <- case lookupTyName n ctxt of
253 [(_,t)] -> return t
254 [] -> ierror (NoSuchVariable n)
255 ns -> ierror (CantResolveAlts (map fst ns))
256 i <- getIState
257 margs <- case lookup n (idris_metavars i) of
258 Just (_, arity, _) -> return arity
259 _ -> return (-1)
261 if (not isProv) then do
262 let skip = guessImps (tt_ctxt i) mty
264 let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))
265 let lem_app = show n ++ appArgs skip margs mty
267 if updatefile then
268 do let fb = fn ++ "~"
269 runIO $ writeSource fb (addLem before tyline lem lem_app later)
270 runIO $ copyFile fb fn
271 else case idris_outputmode i of
272 RawOutput _ -> iPrintResult $ lem ++ "\n" ++ lem_app
273 IdeMode n h ->
274 let good = SexpList [SymbolAtom "ok",
275 SexpList [SymbolAtom "metavariable-lemma",
276 SexpList [SymbolAtom "replace-metavariable",
277 StringAtom lem_app],
278 SexpList [SymbolAtom "definition-type",
279 StringAtom lem]]]
280 in runIO . hPutStrLn h $ convSExp "return" good n
282 else do -- provisional definition
283 let lem_app = show n ++ appArgs [] (-1) mty ++
284 " = ?" ++ show n ++ "_rhs"
285 if updatefile then
286 do let fb = fn ++ "~"
287 runIO $ writeSource fb (addProv before tyline lem_app later)
288 runIO $ copyFile fb fn
289 else case idris_outputmode i of
290 RawOutput _ -> iPrintResult $ lem_app
291 IdeMode n h ->
292 let good = SexpList [SymbolAtom "ok",
293 SexpList [SymbolAtom "provisional-definition-lemma",
294 SexpList [SymbolAtom "definition-clause",
295 StringAtom lem_app]]]
296 in runIO . hPutStrLn h $ convSExp "return" good n
298 where getIndent s = length (takeWhile isSpace s)
300 appArgs skip 0 _ = ""
301 appArgs skip i (Bind n@(UN c) (Pi _ _ _) sc)
302 | (thead c /= '_' && n `notElem` skip)
303 = " " ++ show n ++ appArgs skip (i - 1) sc
304 appArgs skip i (Bind _ (Pi _ _ _) sc) = appArgs skip (i - 1) sc
305 appArgs skip i _ = ""
307 stripMNBind skip (PPi b n@(UN c) ty sc)
308 | (thead c /= '_' && n `notElem` skip) ||
309 take 4 (str c) == "__pi" -- keep in type, but not in app
310 = PPi b n ty (stripMNBind skip sc)
311 stripMNBind skip (PPi b _ ty sc) = stripMNBind skip sc
312 stripMNBind skip t = t
314 -- Guess which binders should be implicits in the generated lemma.
315 -- Make them implicit if they appear guarded by a top level constructor,
316 -- or at the top level themselves.
317 guessImps :: Context -> Term -> [Name]
318 guessImps ctxt (Bind n (Pi _ _ _) sc)
319 | guarded ctxt n (substV (P Bound n Erased) sc)
320 = n : guessImps ctxt sc
321 | otherwise = guessImps ctxt sc
322 guessImps ctxt _ = []
324 guarded ctxt n (P _ n' _) | n == n' = True
325 guarded ctxt n ap@(App _ _ _)
326 | (P _ f _, args) <- unApply ap,
327 isConName f ctxt = any (guarded ctxt n) args
328-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows
329-- | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc
330 guarded ctxt n (Bind _ (Pi _ t _) sc)
331 = guarded ctxt n t || guarded ctxt n sc
332 guarded ctxt n _ = False
334 blank = all isSpace
336 addLem before tyline lem lem_app later
337 = let (bef_end, blankline : bef_start)
338 = case span (not . blank) (reverse before) of
339 (bef, []) -> (bef, "" : [])
340 x -> x
341 mvline = updateMeta False tyline (show n) lem_app in
342 unlines $ reverse bef_start ++
343 [blankline, lem, blankline] ++
344 reverse bef_end ++ mvline : later
346 addProv before tyline lem_app later
347 = let (later_bef, blankline : later_end)
348 = case span (not . blank) later of
349 (bef, []) -> (bef, "" : [])
350 x -> x in
351 unlines $ before ++ tyline :
352 (later_bef ++ [blankline, lem_app, blankline] ++
353 later_end)