git.iko.soy/Idris-dev
on e23ebda help sign in
Idris-dev/src/Idris/Interactive.hs
289 lines 12 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
19import Util.Pretty
20import Util.System
22import System.FilePath
23import System.Directory
24import System.IO
25import Data.Char
28caseSplitAt :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
29caseSplitAt h fn updatefile l n
30 = do src <- runIO $ readFile fn
31 res <- splitOnLine l n fn
32 iLOG (showSep "\n" (map show res))
33 let (before, (ap : later)) = splitAt (l-1) (lines src)
34 res' <- replaceSplits ap res
35 let new = concat res'
36 if updatefile
37 then do let fb = fn ++ "~" -- make a backup!
38 runIO $ writeFile fb (unlines before ++ new ++ unlines later)
39 runIO $ copyFile fb fn
40 else -- do ihputStrLn h (show res)
41 ihPrintResult h new
43addClauseFrom :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
44addClauseFrom h fn updatefile l n
45 = do src <- runIO $ readFile fn
46 let (before, tyline : later) = splitAt (l-1) (lines src)
47 let indent = getIndent 0 (show n) tyline
48 cl <- getClause l n fn
49 -- add clause before first blank line in 'later'
50 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
51 if updatefile
52 then do let fb = fn ++ "~"
53 runIO $ writeFile fb (unlines (before ++ nonblank) ++
54 replicate indent ' ' ++
55 cl ++ "\n" ++
56 unlines rest)
57 runIO $ copyFile fb fn
58 else ihPrintResult h cl
59 where
60 getIndent i n [] = 0
61 getIndent i n xs | take 9 xs == "instance " = i
62 getIndent i n xs | take (length n) xs == n = i
63 getIndent i n (x : xs) = getIndent (i + 1) n xs
65addProofClauseFrom :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
66addProofClauseFrom h fn updatefile l n
67 = do src <- runIO $ readFile fn
68 let (before, tyline : later) = splitAt (l-1) (lines src)
69 let indent = getIndent 0 (show n) tyline
70 cl <- getProofClause l n fn
71 -- add clause before first blank line in 'later'
72 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
73 if updatefile
74 then do let fb = fn ++ "~"
75 runIO $ writeFile fb (unlines (before ++ nonblank) ++
76 replicate indent ' ' ++
77 cl ++ "\n" ++
78 unlines rest)
79 runIO $ copyFile fb fn
80 else ihPrintResult h cl
81 where
82 getIndent i n [] = 0
83 getIndent i n xs | take (length n) xs == n = i
84 getIndent i n (x : xs) = getIndent (i + 1) n xs
86addMissing :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
87addMissing h fn updatefile l n
88 = do src <- runIO $ readFile fn
89 let (before, tyline : later) = splitAt (l-1) (lines src)
90 let indent = getIndent 0 (show n) tyline
91 i <- getIState
92 cl <- getInternalApp fn l
93 let n' = getAppName cl
95 extras <- case lookupCtxt n' (idris_patdefs i) of
96 [] -> return ""
97 [(_, tms)] -> do tms' <- nameMissing tms
98 showNew (show n ++ "_rhs") 1 indent tms'
99 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
100 if updatefile
101 then do let fb = fn ++ "~"
102 runIO $ writeFile fb (unlines (before ++ nonblank)
103 ++ extras ++ unlines rest)
104 runIO $ copyFile fb fn
105 else ihPrintResult h extras
106 where showPat = show . stripNS
107 stripNS tm = mapPT dens tm where
108 dens (PRef fc n) = PRef fc (nsroot n)
109 dens t = t
111 nsroot (NS n _) = nsroot n
112 nsroot (SN (WhereN _ _ n)) = nsroot n
113 nsroot n = n
115 getAppName (PApp _ r _) = getAppName r
116 getAppName (PRef _ r) = r
117 getAppName _ = n
119 showNew nm i ind (tm : tms)
120 = do (nm', i') <- getUniq nm i
121 rest <- showNew nm i' ind tms
122 return (replicate ind ' ' ++
123 showPat tm ++ " = ?" ++ nm' ++
124 "\n" ++ rest)
125 showNew nm i _ [] = return ""
127 getIndent i n [] = 0
128 getIndent i n xs | take (length n) xs == n = i
129 getIndent i n (x : xs) = getIndent (i + 1) n xs
132makeWith :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
133makeWith h fn updatefile l n
134 = do src <- runIO $ readFile fn
135 let (before, tyline : later) = splitAt (l-1) (lines src)
136 let ind = getIndent tyline
137 let with = mkWith tyline n
138 -- add clause before first blank line in 'later',
139 -- or (TODO) before first line with same indentation as tyline
140 let (nonblank, rest) = span (\x -> not (all isSpace x) &&
141 not (ind == getIndent x)) later
142 if updatefile then
143 do let fb = fn ++ "~"
144 runIO $ writeFile fb (unlines (before ++ nonblank)
145 ++ with ++ "\n" ++
146 unlines rest)
147 runIO $ copyFile fb fn
148 else ihPrintResult h with
149 where getIndent s = length (takeWhile isSpace s)
152doProofSearch :: Handle -> FilePath -> Bool -> Bool ->
153 Int -> Name -> [Name] -> Idris ()
154doProofSearch h fn updatefile rec l n hints
155 = do src <- runIO $ readFile fn
156 let (before, tyline : later) = splitAt (l-1) (lines src)
157 ctxt <- getContext
158 mn <- case lookupNames n ctxt of
159 [x] -> return x
160 [] -> return n
161 ns -> ierror (CantResolveAlts (map show ns))
162 i <- getIState
163 let (top, envlen, _) = case lookup mn (idris_metavars i) of
164 Just (t, e, False) -> (t, e, False)
165 _ -> (Nothing, 0, True)
166 let fc = fileFC fn
167 let body t = PProof [Try (TSeq Intros (ProofSearch rec False t hints))
168 (ProofSearch rec False t hints)]
169 let def = PClause fc mn (PRef fc mn) [] (body top) []
170 newmv <- idrisCatch
171 (do elabDecl' EAll toplevel (PClauses fc [] mn [def])
172 (tm, ty) <- elabVal toplevel False (PRef fc mn)
173 ctxt <- getContext
174 i <- getIState
175 return . flip displayS "" . renderPretty 1.0 80 $
176 pprintPTerm defaultPPOption [] [] (idris_infixes i)
177 (stripNS
178 (dropCtxt envlen
179 (delab i (specialise ctxt [] [(mn, 1)] tm)))))
180 (\e -> return ("?" ++ show n))
181 if updatefile then
182 do let fb = fn ++ "~"
183 runIO $ writeFile fb (unlines before ++
184 updateMeta False tyline (show n) newmv ++ "\n"
185 ++ unlines later)
186 runIO $ copyFile fb fn
187 else ihPrintResult h newmv
188 where dropCtxt 0 sc = sc
189 dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc
190 dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc
191 dropCtxt i (PLam _ _ sc) = dropCtxt (i - 1) sc
192 dropCtxt _ t = t
194 stripNS tm = mapPT dens tm where
195 dens (PRef fc n) = PRef fc (nsroot n)
196 dens t = t
198 nsroot (NS n _) = nsroot n
199 nsroot (SN (WhereN _ _ n)) = nsroot n
200 nsroot n = n
202updateMeta brack ('?':cs) n new
203 | length cs >= length n
204 = case splitAt (length n) cs of
205 (mv, c:cs) ->
206 if ((isSpace c || c == ')' || c == '}') && mv == n)
207 then addBracket brack new ++ (c : cs)
208 else '?' : mv ++ c : updateMeta True cs n new
209 (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
210updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new
211updateMeta brack (c:cs) n new
212 = c : updateMeta (brack || not (isSpace c)) cs n new
213updateMeta brack [] n new = ""
215addBracket False new = new
216addBracket True new@('(':xs) | last xs == ')' = new
217addBracket True new | any isSpace new = '(' : new ++ ")"
218 | otherwise = new
221makeLemma :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
222makeLemma h fn updatefile l n
223 = do src <- runIO $ readFile fn
224 let (before, tyline : later) = splitAt (l-1) (lines src)
226 ctxt <- getContext
227 mty <- case lookupTy n ctxt of
228 [t] -> return t
229 [] -> ierror (NoSuchVariable n)
230 ns -> ierror (CantResolveAlts (map show ns))
232 i <- getIState
233 let skip = guessImps (tt_ctxt i) mty
235 let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))
236 let lem_app = show n ++ appArgs skip mty
238 if updatefile then
239 do let fb = fn ++ "~"
240 runIO $ writeFile fb (addLem before tyline lem lem_app later)
241 runIO $ copyFile fb fn
242 else ihPrintResult h $ lem ++ "\n" ++ lem_app
244 where getIndent s = length (takeWhile isSpace s)
246 appArgs skip (Bind n@(UN c) (Pi _) sc)
247 | thead c /= '_' && n `notElem` skip
248 = " " ++ show n ++ appArgs skip sc
249 appArgs skip (Bind _ (Pi _) sc) = appArgs skip sc
250 appArgs skip _ = ""
252 stripMNBind skip (PPi b n@(UN c) ty sc)
253 | thead c /= '_' &&
254 n `notElem` skip = PPi b n ty (stripMNBind skip sc)
255 stripMNBind skip (PPi b _ ty sc) = stripMNBind skip sc
256 stripMNBind skip t = t
258 -- Guess which binders should be implicits in the generated lemma.
259 -- Make them implicit if they appear guarded by a top level constructor,
260 -- or at the top level themselves.
261 guessImps :: Context -> Term -> [Name]
262 guessImps ctxt (Bind n (Pi _) sc)
263 | guarded ctxt n (substV (P Bound n Erased) sc)
264 = n : guessImps ctxt sc
265 | otherwise = guessImps ctxt sc
266 guessImps ctxt _ = []
268 guarded ctxt n (P _ n' _) | n == n' = True
269 guarded ctxt n ap@(App _ _)
270 | (P _ f _, args) <- unApply ap,
271 isConName f ctxt = any (guarded ctxt n) args
272-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows
273-- | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc
274 guarded ctxt n (Bind _ (Pi t) sc)
275 = guarded ctxt n t || guarded ctxt n sc
276 guarded ctxt n _ = False
278 blank = all isSpace
280 addLem before tyline lem lem_app later
281 = let (bef_end, blankline : bef_start)
282 = span (not . blank) (reverse before)
283 mvline = updateMeta False tyline (show n) lem_app in
284 unlines $ reverse bef_start ++
285 [blankline, lem, blankline] ++
286 reverse bef_end ++ mvline : later