git.iko.soy/Idris-dev
on b0cb4e2 help sign in
Idris-dev/src/Idris/Interactive.hs
341 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.IdeSlave hiding (IdeSlaveCommand(..))
20import Util.Pretty
21import Util.System
23import System.FilePath
24import System.Directory
25import System.IO
26import Data.Char
27import Data.Maybe (fromMaybe)
30caseSplitAt :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
31caseSplitAt h fn updatefile l n
32 = do src <- runIO $ readFile fn
33 res <- splitOnLine l n fn
34 iLOG (showSep "\n" (map show res))
35 let (before, (ap : later)) = splitAt (l-1) (lines src)
36 res' <- replaceSplits ap res
37 let new = concat res'
38 if updatefile
39 then do let fb = fn ++ "~" -- make a backup!
40 runIO $ writeFile fb (unlines before ++ new ++ unlines later)
41 runIO $ copyFile fb fn
42 else -- do ihputStrLn h (show res)
43 ihPrintResult h new
45addClauseFrom :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
46addClauseFrom h fn updatefile l n
47 = do src <- runIO $ readFile fn
48 let (before, tyline : later) = splitAt (l-1) (lines src)
49 let indent = getIndent 0 (show n) tyline
50 cl <- getClause l n fn
51 -- add clause before first blank line in 'later'
52 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
53 if updatefile
54 then do let fb = fn ++ "~"
55 runIO $ writeFile fb (unlines (before ++ nonblank) ++
56 replicate indent ' ' ++
57 cl ++ "\n" ++
58 unlines rest)
59 runIO $ copyFile fb fn
60 else ihPrintResult h cl
61 where
62 getIndent i n [] = 0
63 getIndent i n xs | take 9 xs == "instance " = i
64 getIndent i n xs | take (length n) xs == n = i
65 getIndent i n (x : xs) = getIndent (i + 1) n xs
67addProofClauseFrom :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
68addProofClauseFrom h fn updatefile l n
69 = do src <- runIO $ readFile fn
70 let (before, tyline : later) = splitAt (l-1) (lines src)
71 let indent = getIndent 0 (show n) tyline
72 cl <- getProofClause l n fn
73 -- add clause before first blank line in 'later'
74 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
75 if updatefile
76 then do let fb = fn ++ "~"
77 runIO $ writeFile fb (unlines (before ++ nonblank) ++
78 replicate indent ' ' ++
79 cl ++ "\n" ++
80 unlines rest)
81 runIO $ copyFile fb fn
82 else ihPrintResult h cl
83 where
84 getIndent i n [] = 0
85 getIndent i n xs | take (length n) xs == n = i
86 getIndent i n (x : xs) = getIndent (i + 1) n xs
88addMissing :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
89addMissing h fn updatefile l n
90 = do src <- runIO $ readFile fn
91 let (before, tyline : later) = splitAt (l-1) (lines src)
92 let indent = getIndent 0 (show n) tyline
93 i <- getIState
94 cl <- getInternalApp fn l
95 let n' = getAppName cl
97 extras <- case lookupCtxt n' (idris_patdefs i) of
98 [] -> return ""
99 [(_, tms)] -> do tms' <- nameMissing tms
100 showNew (show n ++ "_rhs") 1 indent tms'
101 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
102 if updatefile
103 then do let fb = fn ++ "~"
104 runIO $ writeFile fb (unlines (before ++ nonblank)
105 ++ extras ++ unlines rest)
106 runIO $ copyFile fb fn
107 else ihPrintResult h extras
108 where showPat = show . stripNS
109 stripNS tm = mapPT dens tm where
110 dens (PRef fc n) = PRef fc (nsroot n)
111 dens t = t
113 nsroot (NS n _) = nsroot n
114 nsroot (SN (WhereN _ _ n)) = nsroot n
115 nsroot n = n
117 getAppName (PApp _ r _) = getAppName r
118 getAppName (PRef _ r) = r
119 getAppName _ = n
121 showNew nm i ind (tm : tms)
122 = do (nm', i') <- getUniq nm i
123 rest <- showNew nm i' ind tms
124 return (replicate ind ' ' ++
125 showPat tm ++ " = ?" ++ nm' ++
126 "\n" ++ rest)
127 showNew nm i _ [] = return ""
129 getIndent i n [] = 0
130 getIndent i n xs | take (length n) xs == n = i
131 getIndent i n (x : xs) = getIndent (i + 1) n xs
134makeWith :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
135makeWith h fn updatefile l n
136 = do src <- runIO $ readFile fn
137 let (before, tyline : later) = splitAt (l-1) (lines src)
138 let ind = getIndent tyline
139 let with = mkWith tyline n
140 -- add clause before first blank line in 'later',
141 -- or (TODO) before first line with same indentation as tyline
142 let (nonblank, rest) = span (\x -> not (all isSpace x) &&
143 not (ind == getIndent x)) later
144 if updatefile then
145 do let fb = fn ++ "~"
146 runIO $ writeFile fb (unlines (before ++ nonblank)
147 ++ with ++ "\n" ++
148 unlines rest)
149 runIO $ copyFile fb fn
150 else ihPrintResult h with
151 where getIndent s = length (takeWhile isSpace s)
154doProofSearch :: Handle -> FilePath -> Bool -> Bool ->
155 Int -> Name -> [Name] -> Maybe Int -> Idris ()
156doProofSearch h fn updatefile rec l n hints Nothing
157 = doProofSearch h fn updatefile rec l n hints (Just 10)
158doProofSearch h fn updatefile rec l n hints (Just depth)
159 = do src <- runIO $ readFile fn
160 let (before, tyline : later) = splitAt (l-1) (lines src)
161 ctxt <- getContext
162 mn <- case lookupNames n ctxt of
163 [x] -> return x
164 [] -> return n
165 ns -> ierror (CantResolveAlts ns)
166 i <- getIState
167 let (top, envlen, _) = case lookup mn (idris_metavars i) of
168 Just (t, e, False) -> (t, e, False)
169 _ -> (Nothing, 0, True)
170 let fc = fileFC fn
171 let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t hints))
172 (ProofSearch rec False depth t hints)]
173 let def = PClause fc mn (PRef fc mn) [] (body top) []
174 newmv <- idrisCatch
175 (do elabDecl' EAll toplevel (PClauses fc [] mn [def])
176 (tm, ty) <- elabVal toplevel False (PRef fc mn)
177 ctxt <- getContext
178 i <- getIState
179 return . flip displayS "" . renderPretty 1.0 80 $
180 pprintPTerm defaultPPOption [] [] (idris_infixes i)
181 (stripNS
182 (dropCtxt envlen
183 (delab i (specialise ctxt [] [(mn, 1)] tm)))))
184 (\e -> return ("?" ++ show n))
185 if updatefile then
186 do let fb = fn ++ "~"
187 runIO $ writeFile fb (unlines before ++
188 updateMeta False tyline (show n) newmv ++ "\n"
189 ++ unlines later)
190 runIO $ copyFile fb fn
191 else ihPrintResult h newmv
192 where dropCtxt 0 sc = sc
193 dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc
194 dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc
195 dropCtxt i (PLam _ _ sc) = dropCtxt (i - 1) sc
196 dropCtxt _ t = t
198 stripNS tm = mapPT dens tm where
199 dens (PRef fc n) = PRef fc (nsroot n)
200 dens t = t
202 nsroot (NS n _) = nsroot n
203 nsroot (SN (WhereN _ _ n)) = nsroot n
204 nsroot n = n
206updateMeta brack ('?':cs) n new
207 | length cs >= length n
208 = case splitAt (length n) cs of
209 (mv, c:cs) ->
210 if ((isSpace c || c == ')' || c == '}') && mv == n)
211 then addBracket brack new ++ (c : cs)
212 else '?' : mv ++ c : updateMeta True cs n new
213 (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
214updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new
215updateMeta brack (c:cs) n new
216 = c : updateMeta (brack || not (isSpace c)) cs n new
217updateMeta brack [] n new = ""
219checkProv line n = isProv' False line n
220 where
221 isProv' p cs n | take (length n) cs == n = p
222 isProv' _ ('?':cs) n = isProv' False cs n
223 isProv' _ ('{':cs) n = isProv' True cs n
224 isProv' _ ('}':cs) n = isProv' True cs n
225 isProv' p (_:cs) n = isProv' p cs n
226 isProv' _ [] n = False
228addBracket False new = new
229addBracket True new@('(':xs) | last xs == ')' = new
230addBracket True new | any isSpace new = '(' : new ++ ")"
231 | otherwise = new
234makeLemma :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
235makeLemma h fn updatefile l n
236 = do src <- runIO $ readFile fn
237 let (before, tyline : later) = splitAt (l-1) (lines src)
239 -- if the name is in braces, rather than preceded by a ?, treat it
240 -- as a lemma in a provisional definition
242 let isProv = checkProv tyline (show n)
244 ctxt <- getContext
245 mty <- case lookupTyName n ctxt of
246 [(_,t)] -> return t
247 [] -> ierror (NoSuchVariable n)
248 ns -> ierror (CantResolveAlts (map fst ns))
249 i <- getIState
251 if (not isProv) then do
252 let skip = guessImps (tt_ctxt i) mty
254 let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))
255 let lem_app = show n ++ appArgs skip mty
257 if updatefile then
258 do let fb = fn ++ "~"
259 runIO $ writeFile fb (addLem before tyline lem lem_app later)
260 runIO $ copyFile fb fn
261 else case idris_outputmode i of
262 RawOutput -> ihPrintResult h $ lem ++ "\n" ++ lem_app
263 IdeSlave n ->
264 let good = SexpList [SymbolAtom "ok",
265 SexpList [SymbolAtom "metavariable-lemma",
266 SexpList [SymbolAtom "replace-metavariable",
267 StringAtom lem_app],
268 SexpList [SymbolAtom "definition-type",
269 StringAtom lem]]]
270 in runIO . hPutStrLn h $ convSExp "return" good n
272 else do -- provisional definition
273 let lem_app = show n ++ appArgs [] mty ++
274 " = ?" ++ show n ++ "_rhs"
275 if updatefile then
276 do let fb = fn ++ "~"
277 runIO $ writeFile fb (addProv before tyline lem_app later)
278 runIO $ copyFile fb fn
279 else case idris_outputmode i of
280 RawOutput -> ihPrintResult h $ lem_app
281 IdeSlave n ->
282 let good = SexpList [SymbolAtom "ok",
283 SexpList [SymbolAtom "provisional-definition-lemma",
284 SexpList [SymbolAtom "definition-clause",
285 StringAtom lem_app]]]
286 in runIO . hPutStrLn h $ convSExp "return" good n
288 where getIndent s = length (takeWhile isSpace s)
290 appArgs skip (Bind n@(UN c) (Pi _) sc)
291 | thead c /= '_' && n `notElem` skip
292 = " " ++ show n ++ appArgs skip sc
293 appArgs skip (Bind _ (Pi _) sc) = appArgs skip sc
294 appArgs skip _ = ""
296 stripMNBind skip (PPi b n@(UN c) ty sc)
297 | thead c /= '_' &&
298 n `notElem` skip = PPi b n ty (stripMNBind skip sc)
299 stripMNBind skip (PPi b _ ty sc) = stripMNBind skip sc
300 stripMNBind skip t = t
302 -- Guess which binders should be implicits in the generated lemma.
303 -- Make them implicit if they appear guarded by a top level constructor,
304 -- or at the top level themselves.
305 guessImps :: Context -> Term -> [Name]
306 guessImps ctxt (Bind n (Pi _) sc)
307 | guarded ctxt n (substV (P Bound n Erased) sc)
308 = n : guessImps ctxt sc
309 | otherwise = guessImps ctxt sc
310 guessImps ctxt _ = []
312 guarded ctxt n (P _ n' _) | n == n' = True
313 guarded ctxt n ap@(App _ _)
314 | (P _ f _, args) <- unApply ap,
315 isConName f ctxt = any (guarded ctxt n) args
316-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows
317-- | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc
318 guarded ctxt n (Bind _ (Pi t) sc)
319 = guarded ctxt n t || guarded ctxt n sc
320 guarded ctxt n _ = False
322 blank = all isSpace
324 addLem before tyline lem lem_app later
325 = let (bef_end, blankline : bef_start)
326 = case span (not . blank) (reverse before) of
327 (bef, []) -> (bef, "" : [])
328 x -> x
329 mvline = updateMeta False tyline (show n) lem_app in
330 unlines $ reverse bef_start ++
331 [blankline, lem, blankline] ++
332 reverse bef_end ++ mvline : later
334 addProv before tyline lem_app later
335 = let (later_bef, blankline : later_end)
336 = case span (not . blank) later of
337 (bef, []) -> (bef, "" : [])
338 x -> x in
339 unlines $ before ++ tyline :
340 (later_bef ++ [blankline, lem_app, blankline] ++
341 later_end)