git.iko.soy/Idris-dev
on d16d418 help sign in
Idris-dev/src/Idris/Interactive.hs
339 lines 14 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] -> Idris ()
156doProofSearch h fn updatefile rec l n hints
157 = do src <- runIO $ readFile fn
158 let (before, tyline : later) = splitAt (l-1) (lines src)
159 ctxt <- getContext
160 mn <- case lookupNames n ctxt of
161 [x] -> return x
162 [] -> return n
163 ns -> ierror (CantResolveAlts (map show ns))
164 i <- getIState
165 let (top, envlen, _) = case lookup mn (idris_metavars i) of
166 Just (t, e, False) -> (t, e, False)
167 _ -> (Nothing, 0, True)
168 let fc = fileFC fn
169 let body t = PProof [Try (TSeq Intros (ProofSearch rec False t hints))
170 (ProofSearch rec False t hints)]
171 let def = PClause fc mn (PRef fc mn) [] (body top) []
172 newmv <- idrisCatch
173 (do elabDecl' EAll toplevel (PClauses fc [] mn [def])
174 (tm, ty) <- elabVal toplevel False (PRef fc mn)
175 ctxt <- getContext
176 i <- getIState
177 return . flip displayS "" . renderPretty 1.0 80 $
178 pprintPTerm defaultPPOption [] [] (idris_infixes i)
179 (stripNS
180 (dropCtxt envlen
181 (delab i (specialise ctxt [] [(mn, 1)] tm)))))
182 (\e -> return ("?" ++ show n))
183 if updatefile then
184 do let fb = fn ++ "~"
185 runIO $ writeFile fb (unlines before ++
186 updateMeta False tyline (show n) newmv ++ "\n"
187 ++ unlines later)
188 runIO $ copyFile fb fn
189 else ihPrintResult h newmv
190 where dropCtxt 0 sc = sc
191 dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc
192 dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc
193 dropCtxt i (PLam _ _ sc) = dropCtxt (i - 1) sc
194 dropCtxt _ t = t
196 stripNS tm = mapPT dens tm where
197 dens (PRef fc n) = PRef fc (nsroot n)
198 dens t = t
200 nsroot (NS n _) = nsroot n
201 nsroot (SN (WhereN _ _ n)) = nsroot n
202 nsroot n = n
204updateMeta brack ('?':cs) n new
205 | length cs >= length n
206 = case splitAt (length n) cs of
207 (mv, c:cs) ->
208 if ((isSpace c || c == ')' || c == '}') && mv == n)
209 then addBracket brack new ++ (c : cs)
210 else '?' : mv ++ c : updateMeta True cs n new
211 (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
212updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new
213updateMeta brack (c:cs) n new
214 = c : updateMeta (brack || not (isSpace c)) cs n new
215updateMeta brack [] n new = ""
217checkProv line n = isProv' False line n
218 where
219 isProv' p cs n | take (length n) cs == n = p
220 isProv' _ ('?':cs) n = isProv' False cs n
221 isProv' _ ('{':cs) n = isProv' True cs n
222 isProv' _ ('}':cs) n = isProv' True cs n
223 isProv' p (_:cs) n = isProv' p cs n
224 isProv' _ [] n = False
226addBracket False new = new
227addBracket True new@('(':xs) | last xs == ')' = new
228addBracket True new | any isSpace new = '(' : new ++ ")"
229 | otherwise = new
232makeLemma :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
233makeLemma h fn updatefile l n
234 = do src <- runIO $ readFile fn
235 let (before, tyline : later) = splitAt (l-1) (lines src)
237 -- if the name is in braces, rather than preceded by a ?, treat it
238 -- as a lemma in a provisional definition
240 let isProv = checkProv tyline (show n)
242 ctxt <- getContext
243 mty <- case lookupTy n ctxt of
244 [t] -> return t
245 [] -> ierror (NoSuchVariable n)
246 ns -> ierror (CantResolveAlts (map show ns))
247 i <- getIState
249 if (not isProv) then do
250 let skip = guessImps (tt_ctxt i) mty
252 let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))
253 let lem_app = show n ++ appArgs skip mty
255 if updatefile then
256 do let fb = fn ++ "~"
257 runIO $ writeFile fb (addLem before tyline lem lem_app later)
258 runIO $ copyFile fb fn
259 else case idris_outputmode i of
260 RawOutput -> ihPrintResult h $ lem ++ "\n" ++ lem_app
261 IdeSlave n ->
262 let good = SexpList [SymbolAtom "ok",
263 SexpList [SymbolAtom "metavariable-lemma",
264 SexpList [SymbolAtom "replace-metavariable",
265 StringAtom lem_app],
266 SexpList [SymbolAtom "definition-type",
267 StringAtom lem]]]
268 in runIO . hPutStrLn h $ convSExp "return" good n
270 else do -- provisional definition
271 let lem_app = show n ++ appArgs [] mty ++
272 " = ?" ++ show n ++ "_rhs"
273 if updatefile then
274 do let fb = fn ++ "~"
275 runIO $ writeFile fb (addProv before tyline lem_app later)
276 runIO $ copyFile fb fn
277 else case idris_outputmode i of
278 RawOutput -> ihPrintResult h $ lem_app
279 IdeSlave n ->
280 let good = SexpList [SymbolAtom "ok",
281 SexpList [SymbolAtom "provisional-definition-lemma",
282 SexpList [SymbolAtom "definition-clause",
283 StringAtom lem_app]]]
284 in runIO . hPutStrLn h $ convSExp "return" good n
286 where getIndent s = length (takeWhile isSpace s)
288 appArgs skip (Bind n@(UN c) (Pi _) sc)
289 | thead c /= '_' && n `notElem` skip
290 = " " ++ show n ++ appArgs skip sc
291 appArgs skip (Bind _ (Pi _) sc) = appArgs skip sc
292 appArgs skip _ = ""
294 stripMNBind skip (PPi b n@(UN c) ty sc)
295 | thead c /= '_' &&
296 n `notElem` skip = PPi b n ty (stripMNBind skip sc)
297 stripMNBind skip (PPi b _ ty sc) = stripMNBind skip sc
298 stripMNBind skip t = t
300 -- Guess which binders should be implicits in the generated lemma.
301 -- Make them implicit if they appear guarded by a top level constructor,
302 -- or at the top level themselves.
303 guessImps :: Context -> Term -> [Name]
304 guessImps ctxt (Bind n (Pi _) sc)
305 | guarded ctxt n (substV (P Bound n Erased) sc)
306 = n : guessImps ctxt sc
307 | otherwise = guessImps ctxt sc
308 guessImps ctxt _ = []
310 guarded ctxt n (P _ n' _) | n == n' = True
311 guarded ctxt n ap@(App _ _)
312 | (P _ f _, args) <- unApply ap,
313 isConName f ctxt = any (guarded ctxt n) args
314-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows
315-- | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc
316 guarded ctxt n (Bind _ (Pi t) sc)
317 = guarded ctxt n t || guarded ctxt n sc
318 guarded ctxt n _ = False
320 blank = all isSpace
322 addLem before tyline lem lem_app later
323 = let (bef_end, blankline : bef_start)
324 = case span (not . blank) (reverse before) of
325 (bef, []) -> (bef, "" : [])
326 x -> x
327 mvline = updateMeta False tyline (show n) lem_app in
328 unlines $ reverse bef_start ++
329 [blankline, lem, blankline] ++
330 reverse bef_end ++ mvline : later
332 addProv before tyline lem_app later
333 = let (later_bef, blankline : later_end)
334 = case span (not . blank) later of
335 (bef, []) -> (bef, "" : [])
336 x -> x in
337 unlines $ before ++ tyline :
338 (later_bef ++ [blankline, lem_app, blankline] ++
339 later_end)