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