git.iko.soy/Idris-dev
on c79fb21 help sign in
Idris-dev/src/Idris/Interactive.hs
354 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 Idris.Elab.Value
23import Util.Pretty
24import Util.System
26import System.FilePath
27import System.Directory
28import System.IO
29import Data.Char
30import Data.Maybe (fromMaybe)
31import Data.List (isSuffixOf)
33import Debug.Trace
35caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()
36caseSplitAt fn updatefile l n
37 = do src <- runIO $ readFile fn
38 res <- splitOnLine l n fn
39 iLOG (showSep "\n" (map show res))
40 let (before, (ap : later)) = splitAt (l-1) (lines src)
41 res' <- replaceSplits ap res
42 let new = concat res'
43 if updatefile
44 then do let fb = fn ++ "~" -- make a backup!
45 runIO $ writeFile fb (unlines before ++ new ++ unlines later)
46 runIO $ copyFile fb fn
47 else -- do iputStrLn (show res)
48 iPrintResult new
50addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
51addClauseFrom fn updatefile l n
52 = do src <- runIO $ readFile fn
53 let (before, tyline : later) = splitAt (l-1) (lines src)
54 let indent = getIndent 0 (show n) tyline
55 cl <- getClause l n fn
56 -- add clause before first blank line in 'later'
57 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
58 if updatefile
59 then do let fb = fn ++ "~"
60 runIO $ writeFile fb (unlines (before ++ nonblank) ++
61 replicate indent ' ' ++
62 cl ++ "\n" ++
63 unlines rest)
64 runIO $ copyFile fb fn
65 else iPrintResult cl
66 where
67 getIndent i n [] = 0
68 getIndent i n xs | take 9 xs == "instance " = i
69 getIndent i n xs | take (length n) xs == n = i
70 getIndent i n (x : xs) = getIndent (i + 1) n xs
72addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
73addProofClauseFrom fn updatefile l n
74 = do src <- runIO $ readFile fn
75 let (before, tyline : later) = splitAt (l-1) (lines src)
76 let indent = getIndent 0 (show n) tyline
77 cl <- getProofClause l n fn
78 -- add clause before first blank line in 'later'
79 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
80 if updatefile
81 then do let fb = fn ++ "~"
82 runIO $ writeFile fb (unlines (before ++ nonblank) ++
83 replicate indent ' ' ++
84 cl ++ "\n" ++
85 unlines rest)
86 runIO $ copyFile fb fn
87 else iPrintResult cl
88 where
89 getIndent i n [] = 0
90 getIndent i n xs | take (length n) xs == n = i
91 getIndent i n (x : xs) = getIndent (i + 1) n xs
93addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()
94addMissing fn updatefile l n
95 = do src <- runIO $ readFile fn
96 let (before, tyline : later) = splitAt (l-1) (lines src)
97 let indent = getIndent 0 (show n) tyline
98 i <- getIState
99 cl <- getInternalApp fn l
100 let n' = getAppName cl
102 extras <- case lookupCtxt n' (idris_patdefs i) of
103 [] -> return ""
104 [(_, tms)] -> do tms' <- nameMissing tms
105 showNew (show n ++ "_rhs") 1 indent tms'
106 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
107 if updatefile
108 then do let fb = fn ++ "~"
109 runIO $ writeFile 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 n) = PRef fc (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 $ readFile 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 $ writeFile 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)
162doProofSearch :: FilePath -> Bool -> Bool ->
163 Int -> Name -> [Name] -> Maybe Int -> Idris ()
164doProofSearch fn updatefile rec l n hints Nothing
165 = doProofSearch fn updatefile rec l n hints (Just 10)
166doProofSearch fn updatefile rec l n hints (Just depth)
167 = do src <- runIO $ readFile fn
168 let (before, tyline : later) = splitAt (l-1) (lines src)
169 ctxt <- getContext
170 mn <- case lookupNames n ctxt of
171 [x] -> return x
172 [] -> return n
173 ns -> ierror (CantResolveAlts ns)
174 i <- getIState
175 let (top, envlen, _) = case lookup mn (idris_metavars i) of
176 Just (t, e, False) -> (t, e, False)
177 _ -> (Nothing, 0, True)
178 let fc = fileFC fn
179 let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t hints))
180 (ProofSearch rec False depth t hints)]
181 let def = PClause fc mn (PRef fc mn) [] (body top) []
182 newmv <- idrisCatch
183 (do elabDecl' EAll recinfo (PClauses fc [] mn [def])
184 (tm, ty) <- elabVal recinfo ERHS (PRef fc mn)
185 ctxt <- getContext
186 i <- getIState
187 return . flip displayS "" . renderPretty 1.0 80 $
188 pprintPTerm defaultPPOption [] [] (idris_infixes i)
189 (stripNS
190 (dropCtxt envlen
191 (delab i (specialise ctxt [] [(mn, 1)] tm)))))
192 (\e -> return ("?" ++ show n))
193 if updatefile then
194 do let fb = fn ++ "~"
195 runIO $ writeFile fb (unlines before ++
196 updateMeta False tyline (show n) newmv ++ "\n"
197 ++ unlines later)
198 runIO $ copyFile fb fn
199 else iPrintResult newmv
200 where dropCtxt 0 sc = sc
201 dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc
202 dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc
203 dropCtxt i (PLam _ _ sc) = dropCtxt (i - 1) sc
204 dropCtxt _ t = t
206 stripNS tm = mapPT dens tm where
207 dens (PRef fc n) = PRef fc (nsroot n)
208 dens t = t
210 nsroot (NS n _) = nsroot n
211 nsroot (SN (WhereN _ _ n)) = nsroot n
212 nsroot n = n
214updateMeta brack ('?':cs) n new
215 | length cs >= length n
216 = case splitAt (length n) cs of
217 (mv, c:cs) ->
218 if ((isSpace c || c == ')' || c == '}') && mv == n)
219 then addBracket brack new ++ (c : cs)
220 else '?' : mv ++ c : updateMeta True cs n new
221 (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
222updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new
223updateMeta brack (c:cs) n new
224 = c : updateMeta (brack || not (isSpace c)) cs n new
225updateMeta brack [] n new = ""
227checkProv line n = isProv' False line n
228 where
229 isProv' p cs n | take (length n) cs == n = p
230 isProv' _ ('?':cs) n = isProv' False cs n
231 isProv' _ ('{':cs) n = isProv' True cs n
232 isProv' _ ('}':cs) n = isProv' True cs n
233 isProv' p (_:cs) n = isProv' p cs n
234 isProv' _ [] n = False
236addBracket False new = new
237addBracket True new@('(':xs) | last xs == ')' = new
238addBracket True new | any isSpace new = '(' : new ++ ")"
239 | otherwise = new
242makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()
243makeLemma fn updatefile l n
244 = do src <- runIO $ readFile fn
245 let (before, tyline : later) = splitAt (l-1) (lines src)
247 -- if the name is in braces, rather than preceded by a ?, treat it
248 -- as a lemma in a provisional definition
250 let isProv = checkProv tyline (show n)
252 ctxt <- getContext
253 mty <- case lookupTyName n ctxt of
254 [(_,t)] -> return t
255 [] -> ierror (NoSuchVariable n)
256 ns -> ierror (CantResolveAlts (map fst ns))
257 i <- getIState
258 margs <- case lookup n (idris_metavars i) of
259 Just (_, arity, _) -> return arity
260 _ -> return (-1)
262 if (not isProv) then do
263 let skip = guessImps (tt_ctxt i) mty
265 let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))
266 let lem_app = show n ++ appArgs skip margs mty
268 if updatefile then
269 do let fb = fn ++ "~"
270 runIO $ writeFile fb (addLem before tyline lem lem_app later)
271 runIO $ copyFile fb fn
272 else case idris_outputmode i of
273 RawOutput _ -> iPrintResult $ lem ++ "\n" ++ lem_app
274 IdeSlave n h ->
275 let good = SexpList [SymbolAtom "ok",
276 SexpList [SymbolAtom "metavariable-lemma",
277 SexpList [SymbolAtom "replace-metavariable",
278 StringAtom lem_app],
279 SexpList [SymbolAtom "definition-type",
280 StringAtom lem]]]
281 in runIO . hPutStrLn h $ convSExp "return" good n
283 else do -- provisional definition
284 let lem_app = show n ++ appArgs [] (-1) mty ++
285 " = ?" ++ show n ++ "_rhs"
286 if updatefile then
287 do let fb = fn ++ "~"
288 runIO $ writeFile fb (addProv before tyline lem_app later)
289 runIO $ copyFile fb fn
290 else case idris_outputmode i of
291 RawOutput _ -> iPrintResult $ lem_app
292 IdeSlave n h ->
293 let good = SexpList [SymbolAtom "ok",
294 SexpList [SymbolAtom "provisional-definition-lemma",
295 SexpList [SymbolAtom "definition-clause",
296 StringAtom lem_app]]]
297 in runIO . hPutStrLn h $ convSExp "return" good n
299 where getIndent s = length (takeWhile isSpace s)
301 appArgs skip 0 _ = ""
302 appArgs skip i (Bind n@(UN c) (Pi _) sc)
303 | (thead c /= '_' && n `notElem` skip)
304 = " " ++ show n ++ appArgs skip (i - 1) sc
305 appArgs skip i (Bind _ (Pi _) sc) = appArgs skip (i - 1) sc
306 appArgs skip i _ = ""
308 stripMNBind skip (PPi b n@(UN c) ty sc)
309 | (thead c /= '_' && n `notElem` skip) ||
310 take 4 (str c) == "__pi" -- keep in type, but not in app
311 = PPi b n ty (stripMNBind skip sc)
312 stripMNBind skip (PPi b _ ty sc) = stripMNBind skip sc
313 stripMNBind skip t = t
315 -- Guess which binders should be implicits in the generated lemma.
316 -- Make them implicit if they appear guarded by a top level constructor,
317 -- or at the top level themselves.
318 guessImps :: Context -> Term -> [Name]
319 guessImps ctxt (Bind n (Pi _) sc)
320 | guarded ctxt n (substV (P Bound n Erased) sc)
321 = n : guessImps ctxt sc
322 | otherwise = guessImps ctxt sc
323 guessImps ctxt _ = []
325 guarded ctxt n (P _ n' _) | n == n' = True
326 guarded ctxt n ap@(App _ _)
327 | (P _ f _, args) <- unApply ap,
328 isConName f ctxt = any (guarded ctxt n) args
329-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows
330-- | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc
331 guarded ctxt n (Bind _ (Pi t) sc)
332 = guarded ctxt n t || guarded ctxt n sc
333 guarded ctxt n _ = False
335 blank = all isSpace
337 addLem before tyline lem lem_app later
338 = let (bef_end, blankline : bef_start)
339 = case span (not . blank) (reverse before) of
340 (bef, []) -> (bef, "" : [])
341 x -> x
342 mvline = updateMeta False tyline (show n) lem_app in
343 unlines $ reverse bef_start ++
344 [blankline, lem, blankline] ++
345 reverse bef_end ++ mvline : later
347 addProv before tyline lem_app later
348 = let (later_bef, blankline : later_end)
349 = case span (not . blank) later of
350 (bef, []) -> (bef, "" : [])
351 x -> x in
352 unlines $ before ++ tyline :
353 (later_bef ++ [blankline, lem_app, blankline] ++
354 later_end)