git.iko.soy/Idris-dev
on ccda94e help sign in
Idris-dev/src/Idris/Interactive.hs
350 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)
32import Debug.Trace
34caseSplitAt :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
35caseSplitAt h fn updatefile l n
36 = do src <- runIO $ readFile 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 $ writeFile fb (unlines before ++ new ++ unlines later)
45 runIO $ copyFile fb fn
46 else -- do ihputStrLn h (show res)
47 ihPrintResult h new
49addClauseFrom :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
50addClauseFrom h fn updatefile l n
51 = do src <- runIO $ readFile 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 $ writeFile fb (unlines (before ++ nonblank) ++
60 replicate indent ' ' ++
61 cl ++ "\n" ++
62 unlines rest)
63 runIO $ copyFile fb fn
64 else ihPrintResult h 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 :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
72addProofClauseFrom h fn updatefile l n
73 = do src <- runIO $ readFile 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 $ writeFile fb (unlines (before ++ nonblank) ++
82 replicate indent ' ' ++
83 cl ++ "\n" ++
84 unlines rest)
85 runIO $ copyFile fb fn
86 else ihPrintResult h 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 :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
93addMissing h fn updatefile l n
94 = do src <- runIO $ readFile 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 $ writeFile fb (unlines (before ++ nonblank)
109 ++ extras ++ unlines rest)
110 runIO $ copyFile fb fn
111 else ihPrintResult h 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 showNew nm i ind (tm : tms)
126 = do (nm', i') <- getUniq nm i
127 rest <- showNew nm i' ind tms
128 return (replicate ind ' ' ++
129 showPat tm ++ " = ?" ++ nm' ++
130 "\n" ++ rest)
131 showNew nm i _ [] = return ""
133 getIndent i n [] = 0
134 getIndent i n xs | take (length n) xs == n = i
135 getIndent i n (x : xs) = getIndent (i + 1) n xs
138makeWith :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
139makeWith h fn updatefile l n
140 = do src <- runIO $ readFile fn
141 let (before, tyline : later) = splitAt (l-1) (lines src)
142 let ind = getIndent tyline
143 let with = mkWith tyline n
144 -- add clause before first blank line in 'later',
145 -- or (TODO) before first line with same indentation as tyline
146 let (nonblank, rest) = span (\x -> not (all isSpace x) &&
147 not (ind == getIndent x)) later
148 if updatefile then
149 do let fb = fn ++ "~"
150 runIO $ writeFile fb (unlines (before ++ nonblank)
151 ++ with ++ "\n" ++
152 unlines rest)
153 runIO $ copyFile fb fn
154 else ihPrintResult h with
155 where getIndent s = length (takeWhile isSpace s)
158doProofSearch :: Handle -> FilePath -> Bool -> Bool ->
159 Int -> Name -> [Name] -> Maybe Int -> Idris ()
160doProofSearch h fn updatefile rec l n hints Nothing
161 = doProofSearch h fn updatefile rec l n hints (Just 10)
162doProofSearch h fn updatefile rec l n hints (Just depth)
163 = do src <- runIO $ readFile fn
164 let (before, tyline : later) = splitAt (l-1) (lines src)
165 ctxt <- getContext
166 mn <- case lookupNames n ctxt of
167 [x] -> return x
168 [] -> return n
169 ns -> ierror (CantResolveAlts ns)
170 i <- getIState
171 let (top, envlen, _) = case lookup mn (idris_metavars i) of
172 Just (t, e, False) -> (t, e, False)
173 _ -> (Nothing, 0, True)
174 let fc = fileFC fn
175 let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t hints))
176 (ProofSearch rec False depth t hints)]
177 let def = PClause fc mn (PRef fc mn) [] (body top) []
178 newmv <- idrisCatch
179 (do elabDecl' EAll recinfo (PClauses fc [] mn [def])
180 (tm, ty) <- elabVal recinfo ERHS (PRef fc mn)
181 ctxt <- getContext
182 i <- getIState
183 return . flip displayS "" . renderPretty 1.0 80 $
184 pprintPTerm defaultPPOption [] [] (idris_infixes i)
185 (stripNS
186 (dropCtxt envlen
187 (delab i (specialise ctxt [] [(mn, 1)] tm)))))
188 (\e -> return ("?" ++ show n))
189 if updatefile then
190 do let fb = fn ++ "~"
191 runIO $ writeFile fb (unlines before ++
192 updateMeta False tyline (show n) newmv ++ "\n"
193 ++ unlines later)
194 runIO $ copyFile fb fn
195 else ihPrintResult h newmv
196 where dropCtxt 0 sc = sc
197 dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc
198 dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc
199 dropCtxt i (PLam _ _ sc) = dropCtxt (i - 1) sc
200 dropCtxt _ t = t
202 stripNS tm = mapPT dens tm where
203 dens (PRef fc n) = PRef fc (nsroot n)
204 dens t = t
206 nsroot (NS n _) = nsroot n
207 nsroot (SN (WhereN _ _ n)) = nsroot n
208 nsroot n = n
210updateMeta brack ('?':cs) n new
211 | length cs >= length n
212 = case splitAt (length n) cs of
213 (mv, c:cs) ->
214 if ((isSpace c || c == ')' || c == '}') && mv == n)
215 then addBracket brack new ++ (c : cs)
216 else '?' : mv ++ c : updateMeta True cs n new
217 (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
218updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new
219updateMeta brack (c:cs) n new
220 = c : updateMeta (brack || not (isSpace c)) cs n new
221updateMeta brack [] n new = ""
223checkProv line n = isProv' False line n
224 where
225 isProv' p cs n | take (length n) cs == n = p
226 isProv' _ ('?':cs) n = isProv' False cs n
227 isProv' _ ('{':cs) n = isProv' True cs n
228 isProv' _ ('}':cs) n = isProv' True cs n
229 isProv' p (_:cs) n = isProv' p cs n
230 isProv' _ [] n = False
232addBracket False new = new
233addBracket True new@('(':xs) | last xs == ')' = new
234addBracket True new | any isSpace new = '(' : new ++ ")"
235 | otherwise = new
238makeLemma :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
239makeLemma h fn updatefile l n
240 = do src <- runIO $ readFile fn
241 let (before, tyline : later) = splitAt (l-1) (lines src)
243 -- if the name is in braces, rather than preceded by a ?, treat it
244 -- as a lemma in a provisional definition
246 let isProv = checkProv tyline (show n)
248 ctxt <- getContext
249 mty <- case lookupTyName n ctxt of
250 [(_,t)] -> return t
251 [] -> ierror (NoSuchVariable n)
252 ns -> ierror (CantResolveAlts (map fst ns))
253 i <- getIState
254 margs <- case lookup n (idris_metavars i) of
255 Just (_, arity, _) -> return arity
256 _ -> return (-1)
258 if (not isProv) then do
259 let skip = guessImps (tt_ctxt i) mty
261 let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))
262 let lem_app = show n ++ appArgs skip margs mty
264 if updatefile then
265 do let fb = fn ++ "~"
266 runIO $ writeFile fb (addLem before tyline lem lem_app later)
267 runIO $ copyFile fb fn
268 else case idris_outputmode i of
269 RawOutput -> ihPrintResult h $ lem ++ "\n" ++ lem_app
270 IdeSlave n ->
271 let good = SexpList [SymbolAtom "ok",
272 SexpList [SymbolAtom "metavariable-lemma",
273 SexpList [SymbolAtom "replace-metavariable",
274 StringAtom lem_app],
275 SexpList [SymbolAtom "definition-type",
276 StringAtom lem]]]
277 in runIO . hPutStrLn h $ convSExp "return" good n
279 else do -- provisional definition
280 let lem_app = show n ++ appArgs [] (-1) mty ++
281 " = ?" ++ show n ++ "_rhs"
282 if updatefile then
283 do let fb = fn ++ "~"
284 runIO $ writeFile fb (addProv before tyline lem_app later)
285 runIO $ copyFile fb fn
286 else case idris_outputmode i of
287 RawOutput -> ihPrintResult h $ lem_app
288 IdeSlave n ->
289 let good = SexpList [SymbolAtom "ok",
290 SexpList [SymbolAtom "provisional-definition-lemma",
291 SexpList [SymbolAtom "definition-clause",
292 StringAtom lem_app]]]
293 in runIO . hPutStrLn h $ convSExp "return" good n
295 where getIndent s = length (takeWhile isSpace s)
297 appArgs skip 0 _ = ""
298 appArgs skip i (Bind n@(UN c) (Pi _) sc)
299 | (thead c /= '_' && n `notElem` skip)
300 = " " ++ show n ++ appArgs skip (i - 1) sc
301 appArgs skip i (Bind _ (Pi _) sc) = appArgs skip (i - 1) sc
302 appArgs skip i _ = ""
304 stripMNBind skip (PPi b n@(UN c) ty sc)
305 | (thead c /= '_' && n `notElem` skip) ||
306 take 4 (str c) == "__pi" -- keep in type, but not in app
307 = PPi b n ty (stripMNBind skip sc)
308 stripMNBind skip (PPi b _ ty sc) = stripMNBind skip sc
309 stripMNBind skip t = t
311 -- Guess which binders should be implicits in the generated lemma.
312 -- Make them implicit if they appear guarded by a top level constructor,
313 -- or at the top level themselves.
314 guessImps :: Context -> Term -> [Name]
315 guessImps ctxt (Bind n (Pi _) sc)
316 | guarded ctxt n (substV (P Bound n Erased) sc)
317 = n : guessImps ctxt sc
318 | otherwise = guessImps ctxt sc
319 guessImps ctxt _ = []
321 guarded ctxt n (P _ n' _) | n == n' = True
322 guarded ctxt n ap@(App _ _)
323 | (P _ f _, args) <- unApply ap,
324 isConName f ctxt = any (guarded ctxt n) args
325-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows
326-- | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc
327 guarded ctxt n (Bind _ (Pi t) sc)
328 = guarded ctxt n t || guarded ctxt n sc
329 guarded ctxt n _ = False
331 blank = all isSpace
333 addLem before tyline lem lem_app later
334 = let (bef_end, blankline : bef_start)
335 = case span (not . blank) (reverse before) of
336 (bef, []) -> (bef, "" : [])
337 x -> x
338 mvline = updateMeta False tyline (show n) lem_app in
339 unlines $ reverse bef_start ++
340 [blankline, lem, blankline] ++
341 reverse bef_end ++ mvline : later
343 addProv before tyline lem_app later
344 = let (later_bef, blankline : later_end)
345 = case span (not . blank) later of
346 (bef, []) -> (bef, "" : [])
347 x -> x in
348 unlines $ before ++ tyline :
349 (later_bef ++ [blankline, lem_app, blankline] ++
350 later_end)