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