git.iko.soy/Idris-dev
on 239c8ca help sign in
Idris-dev/src/Idris/CaseSplit.hs
435 lines 18 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.CaseSplit(splitOnLine, replaceSplits,
4 getClause, getProofClause,
5 mkWith,
6 nameMissing,
7 getUniq, nameRoot) where
8-- splitting a variable in a pattern clause
10import Idris.AbsSyntax
11import Idris.AbsSyntaxTree (Idris, IState, PTerm)
12import Idris.ElabDecls
13import Idris.Delaborate
14import Idris.Parser
15import Idris.Error
16import Idris.Output
18import Idris.Elab.Value
19import Idris.Elab.Term
21import Idris.Core.TT
22import Idris.Core.Typecheck
23import Idris.Core.Evaluate
25import Data.Maybe
26import Data.Char
27import Data.List (isPrefixOf, isSuffixOf)
28import Control.Monad
29import Control.Monad.State.Strict
31import Text.Parser.Combinators
32import Text.Parser.Char(anyChar)
33import Text.Trifecta(Result(..), parseString)
34import Text.Trifecta.Delta
36import Debug.Trace
38{-
40Given a pattern clause and a variable 'n', elaborate the clause and find the
41type of 'n'.
43Make new pattern clauses by replacing 'n' with all the possibly constructors
44applied to '_', and replacing all other variables with '_' in order to
45resolve other dependencies.
47Finally, merge the generated patterns with the original, by matching.
48Always take the "more specific" argument when there is a discrepancy, i.e.
49names over '_', patterns over names, etc.
50-}
52-- Given a variable to split, and a term application, return a list of
53-- variable updates
54split :: Name -> PTerm -> Idris [[(Name, PTerm)]]
55split n t'
56 = do ist <- getIState
57 -- Make sure all the names in the term are accessible
58 mapM_ (\n -> setAccessibility n Public) (allNamesIn t')
59 -- ETyDecl rather then ELHS because there'll be explicit type
60 -- matching
61 (tm, ty, pats) <- elabValBind recinfo ETyDecl True (addImplPat ist t')
62 -- ASSUMPTION: tm is in normal form after elabValBind, so we don't
63 -- need to do anything special to find out what family each argument
64 -- is in
65 logLvl 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)
66-- iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))
67-- iputStrLn (show pats)
68 let t = mergeUserImpl (addImplPat ist t') (delab ist tm)
69 let ctxt = tt_ctxt ist
70 case lookup n pats of
71 Nothing -> ifail $ show n ++ " is not a pattern variable"
72 Just ty ->
73 do let splits = findPats ist ty
74 logLvl 1 ("New patterns " ++ showSep ", "
75 (map showTmImpls splits))
76 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)
77 logLvl 4 ("Working from " ++ show t)
78 logLvl 4 ("Trying " ++ showSep "\n"
79 (map (showTmImpls) newPats_in))
80 newPats <- mapM elabNewPat newPats_in
81 logLvl 3 ("Original:\n" ++ show t)
82 logLvl 3 ("Split:\n" ++
83 (showSep "\n" (map show (mapMaybe id newPats))))
84 logLvl 3 "----"
85 let newPats' = mergeAllPats ist n t (mapMaybe id newPats)
86 logLvl 1 ("Name updates " ++ showSep "\n"
87 (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))
88 return (map snd newPats')
90data MergeState = MS { namemap :: [(Name, Name)],
91 invented :: [(Name, Name)],
92 explicit :: [Name],
93 updates :: [(Name, PTerm)] }
95addUpdate :: Name -> Idris.AbsSyntaxTree.PTerm -> State MergeState ()
96addUpdate n tm = do ms <- get
97 put (ms { updates = ((n, stripNS tm) : updates ms) } )
99inventName :: Idris.AbsSyntaxTree.IState -> Maybe Name -> Name -> State MergeState Name
100inventName ist ty n =
101 do ms <- get
102 let supp = case ty of
103 Nothing -> []
104 Just t -> getNameHints ist t
105 let nsupp = case n of
106 MN i n | not (tnull n) && thead n == '_'
107 -> mkSupply (supp ++ varlist)
108 MN i n -> mkSupply (UN n : supp ++ varlist)
109 UN n | thead n == '_'
110 -> mkSupply (supp ++ varlist)
111 x -> mkSupply (x : supp)
112 let badnames = map snd (namemap ms) ++ map snd (invented ms) ++
113 explicit ms
114 case lookup n (invented ms) of
115 Just n' -> return n'
116 Nothing ->
117 do let n' = uniqueNameFrom nsupp badnames
118 put (ms { invented = (n, n') : invented ms })
119 return n'
121mkSupply :: [Name] -> [Name]
122mkSupply ns = mkSupply' ns (map nextName ns)
123 where mkSupply' xs ns' = xs ++ mkSupply ns'
125varlist :: [Name]
126varlist = map (sUN . (:[])) "xyzwstuv" -- EB's personal preference :)
128stripNS :: Idris.AbsSyntaxTree.PTerm -> Idris.AbsSyntaxTree.PTerm
129stripNS tm = mapPT dens tm where
130 dens (PRef fc hls n) = PRef fc hls (nsroot n)
131 dens t = t
133mergeAllPats :: IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
134mergeAllPats ist cv t [] = []
135mergeAllPats ist cv t (p : ps)
136 = let (p', MS _ _ _ u) = runState (mergePat ist t p Nothing)
137 (MS [] [] (filter (/=cv) (patvars t)) [])
138 ps' = mergeAllPats ist cv t ps in
139 ((p', u) : ps')
140 where patvars (PRef _ _ n) = [n]
141 patvars (PApp _ _ as) = concatMap (patvars . getTm) as
142 patvars (PPatvar _ n) = [n]
143 patvars _ = []
145mergePat :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
146-- If any names are unified, make sure they stay unified. Always prefer
147-- user provided name (first pattern)
148mergePat ist (PPatvar fc n) new t
149 = mergePat ist (PRef fc [] n) new t
150mergePat ist old (PPatvar fc n) t
151 = mergePat ist old (PRef fc [] n) t
152mergePat ist orig@(PRef fc _ n) new@(PRef _ _ n') t
153 | isDConName n' (tt_ctxt ist) = do addUpdate n new
154 return new
155 | otherwise
156 = do ms <- get
157 case lookup n' (namemap ms) of
158 Just x -> do addUpdate n (PRef fc [] x)
159 return (PRef fc [] x)
160 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })
161 return (PRef fc [] n)
162mergePat ist (PApp _ _ args) (PApp fc f args') t
163 = do newArgs <- zipWithM mergeArg args (zip args' (argTys ist f))
164 return (PApp fc f newArgs)
165 where mergeArg x (y, t)
166 = do tm' <- mergePat ist (getTm x) (getTm y) t
167 case x of
168 (PImp _ _ _ _ _) ->
169 return (y { machine_inf = machine_inf x,
170 getTm = tm' })
171 _ -> return (y { getTm = tm' })
172mergePat ist (PRef fc _ n) tm ty = do tm <- tidy ist tm ty
173 addUpdate n tm
174 return tm
175mergePat ist x y t = return y
177mergeUserImpl :: PTerm -> PTerm -> PTerm
178mergeUserImpl x y = x
180argTys :: IState -> PTerm -> [Maybe Name]
181argTys ist (PRef fc hls n)
182 = case lookupTy n (tt_ctxt ist) of
183 [ty] -> map (tyName . snd) (getArgTys ty) ++ repeat Nothing
184 _ -> repeat Nothing
185 where tyName (Bind _ (Pi _ _ _) _) = Just (sUN "->")
186 tyName t | (P _ n _, _) <- unApply t = Just n
187 | otherwise = Nothing
188argTys _ _ = repeat Nothing
190tidy :: IState -> PTerm -> Maybe Name -> State MergeState PTerm
191tidy ist orig@(PRef fc hls n) ty
192 = do ms <- get
193 case lookup n (namemap ms) of
194 Just x -> return (PRef fc [] x)
195 Nothing -> case n of
196 (UN _) -> return orig
197 _ -> do n' <- inventName ist ty n
198 return (PRef fc [] n')
199tidy ist (PApp fc f args) ty
200 = do args' <- zipWithM tidyArg args (argTys ist f)
201 return (PApp fc f args')
202 where tidyArg x ty' = do tm' <- tidy ist (getTm x) ty'
203 return (x { getTm = tm' })
204tidy ist tm ty = return tm
207-- mapPT tidyVar tm
208-- where tidyVar (PRef _ _) = Placeholder
209-- tidyVar t = t
211elabNewPat :: PTerm -> Idris (Maybe PTerm)
212elabNewPat t = idrisCatch (do (tm, ty) <- elabVal recinfo ELHS t
213 i <- getIState
214 return (Just (delab i tm)))
215 (\e -> do i <- getIState
216 logLvl 5 $ "Not a valid split:\n" ++ pshow i e
217 return Nothing)
219findPats :: IState -> Type -> [PTerm]
220findPats ist t | (P _ n _, _) <- unApply t
221 = case lookupCtxt n (idris_datatypes ist) of
222 [ti] -> map genPat (con_names ti)
223 _ -> [Placeholder]
224 where genPat n = case lookupCtxt n (idris_implicits ist) of
225 [args] -> PApp emptyFC (PRef emptyFC [] n)
226 (map toPlaceholder args)
227 _ -> error $ "Can't happen (genPat) " ++ show n
228 toPlaceholder tm = tm { getTm = Placeholder }
229findPats ist t = [Placeholder]
231replaceVar :: Context -> Name -> PTerm -> PTerm -> PTerm
232replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)
233 where subst :: PTerm -> PTerm
234 subst orig@(PPatvar _ v) | v == n = t
235 | otherwise = Placeholder
236 subst orig@(PRef _ _ v) | v == n = t
237 | isDConName v ctxt = orig
238 subst (PRef _ _ _) = Placeholder
239 subst (PApp fc (PRef _ _ t) pats)
240 | isTConName t ctxt = Placeholder -- infer types
241 subst (PApp fc f pats) = PApp fc f (map substArg pats)
242 subst x = x
244 substArg arg = arg { getTm = subst (getTm arg) }
246replaceVar ctxt n t pat = pat
248splitOnLine :: Int -- ^ line number
249 -> Name -- ^ variable
250 -> FilePath -- ^ name of file
251 -> Idris [[(Name, PTerm)]]
252splitOnLine l n fn = do
253-- let (before, later) = splitAt (l-1) (lines inp)
254-- i <- getIState
255 cl <- getInternalApp fn l
256 logLvl 3 ("Working with " ++ showTmImpls cl)
257 tms <- split n cl
258-- iputStrLn (showSep "\n" (map show tms))
259 return tms -- "" -- not yet done...
261replaceSplits :: String -> [[(Name, PTerm)]] -> Idris [String]
262replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
263 where
264 rep str [] = str ++ "\n"
265 rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups
267 updateRHSs i [] = return []
268 updateRHSs i (x : xs) = do (x', i') <- updateRHS (null xs) i x
269 xs' <- updateRHSs i' xs
270 return (x' : xs')
272 updateRHS last i ('?':'=':xs) = do (xs', i') <- updateRHS last i xs
273 return ("?=" ++ xs', i')
274 updateRHS last i ('?':xs)
275 = do let (nm, rest_in) = span (not . (\x -> isSpace x || x == ')'
276 || x == '(')) xs
277 let rest = if last then rest_in else
278 case span (not . (=='\n')) rest_in of
279 (_, restnl) -> restnl
280 (nm', i') <- getUniq nm i
281 return ('?':nm' ++ rest, i')
282 updateRHS last i (x : xs) = do (xs', i') <- updateRHS last i xs
283 return (x : xs', i')
284 updateRHS last i [] = return ("", i)
287 -- TMP HACK: If there are Nats, we don't want to show as numerals since
288 -- this isn't supported in a pattern, so special case here
289 nshow (PRef _ _ (UN z)) | z == txt "Z" = "Z"
290 nshow (PApp _ (PRef _ _ (UN s)) [x]) | s == txt "S" =
291 "(S " ++ addBrackets (nshow (getTm x)) ++ ")"
292 nshow t = show t
294 -- if there's any {n} replace with {n=n}
295 -- but don't replace it in comments
296 expandBraces ('{' : '-' : xs) = '{' : '-' : xs
297 expandBraces ('{' : xs)
298 = let (brace, (_:rest)) = span (/= '}') xs in
299 if (not ('=' `elem` brace))
300 then ('{' : brace ++ " = " ++ brace ++ "}") ++
301 expandBraces rest
302 else ('{' : brace ++ "}") ++ expandBraces rest
303 expandBraces (x : xs) = x : expandBraces xs
304 expandBraces [] = []
306 updatePat start n tm [] = []
307 updatePat start n tm ('{':rest) =
308 let (space, rest') = span isSpace rest in
309 '{' : space ++ updatePat False n tm rest'
310 updatePat start n tm done@('?':rest) = done
311 updatePat True n tm xs@(c:rest) | length xs > length n
312 = let (before, after@(next:_)) = splitAt (length n) xs in
313 if (before == n && not (isAlphaNum next))
314 then addBrackets tm ++ updatePat False n tm after
315 else c : updatePat (not (isAlphaNum c)) n tm rest
316 updatePat start n tm (c:rest) = c : updatePat (not ((isAlphaNum c) || c == '_')) n tm rest
318 addBrackets tm | ' ' `elem` tm
319 , not (isPrefixOf "(" tm)
320 , not (isSuffixOf ")" tm) = "(" ++ tm ++ ")"
321 | otherwise = tm
324getUniq :: (Show t, Num t) => [Char] -> t -> Idris ([Char], t)
325getUniq nm i
326 = do ist <- getIState
327 let n = nameRoot [] nm ++ "_" ++ show i
328 case lookupTy (sUN n) (tt_ctxt ist) of
329 [] -> return (n, i+1)
330 _ -> getUniq nm (i+1)
332nameRoot acc nm | all isDigit nm = showSep "_" acc
333nameRoot acc nm =
334 case span (/='_') nm of
335 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after
336 _ -> showSep "_" (acc ++ [nm])
338getClause :: Int -- ^ line number that the type is declared on
339 -> Name -- ^ Function name
340 -> FilePath -- ^ Source file name
341 -> Idris String
342getClause l fn fp
343 = do i <- getIState
344 case lookupCtxt fn (idris_classes i) of
345 [c] -> return (mkClassBodies i (class_methods c))
346 _ -> do ty <- getInternalApp fp l
347 ist <- get
348 let ap = mkApp ist ty []
349 return (show fn ++ " " ++ ap ++ "= ?"
350 ++ show fn ++ "_rhs")
351 where mkApp :: IState -> PTerm -> [Name] -> String
352 mkApp i (PPi (Exp _ _ False) (MN _ _) _ ty sc) used
353 = let n = getNameFrom i used ty in
354 show n ++ " " ++ mkApp i sc (n : used)
355 mkApp i (PPi (Exp _ _ False) (UN n) _ ty sc) used
356 | thead n == '_'
357 = let n = getNameFrom i used ty in
358 show n ++ " " ++ mkApp i sc (n : used)
359 mkApp i (PPi (Exp _ _ False) n _ _ sc) used
360 = show n ++ " " ++ mkApp i sc (n : used)
361 mkApp i (PPi _ _ _ _ sc) used = mkApp i sc used
362 mkApp i _ _ = ""
364 getNameFrom i used (PPi _ _ _ _ _)
365 = uniqueNameFrom (mkSupply [sUN "f", sUN "g"]) used
366 getNameFrom i used (PApp fc f as) = getNameFrom i used f
367 getNameFrom i used (PRef fc _ f)
368 = case getNameHints i f of
369 [] -> uniqueNameFrom (mkSupply [sUN "x", sUN "y",
370 sUN "z"]) used
371 ns -> uniqueNameFrom (mkSupply ns) used
372 getNameFrom i used _ = uniqueNameFrom (mkSupply [sUN "x", sUN "y",
373 sUN "z"]) used
375 -- write method declarations, indent with 4 spaces
376 mkClassBodies :: IState -> [(Name, (FnOpts, PTerm))] -> String
377 mkClassBodies i ns
378 = showSep "\n"
379 (zipWith (\(n, (_, ty)) m -> " " ++
380 def (show (nsroot n)) ++ " "
381 ++ mkApp i ty []
382 ++ "= ?"
383 ++ show fn ++ "_rhs_" ++ show m) ns [1..])
385 def n@(x:xs) | not (isAlphaNum x) = "(" ++ n ++ ")"
386 def n = n
388getProofClause :: Int -- ^ line number that the type is declared
389 -> Name -- ^ Function name
390 -> FilePath -- ^ Source file name
391 -> Idris String
392getProofClause l fn fp
393 = do ty <- getInternalApp fp l
394 return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")
395 where mkApp (PPi _ _ _ _ sc) = mkApp sc
396 mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn
398-- Purely syntactic - turn a pattern match clause into a with and a new
399-- match clause
401mkWith :: String -> Name -> String
402mkWith str n = let str' = replaceRHS str "with (_)"
403 in str' ++ "\n" ++ newpat str
405 where replaceRHS [] str = str
406 replaceRHS ('?':'=': rest) str = str
407 replaceRHS ('=': rest) str
408 | not ('=' `elem` rest) = str
409 replaceRHS (x : rest) str = x : replaceRHS rest str
411 newpat ('>':patstr) = '>':newpat patstr
412 newpat patstr =
413 " " ++
414 replaceRHS patstr "| with_pat = ?" ++ show n ++ "_rhs"
416-- Replace _ with names in missing clauses
418nameMissing :: [PTerm] -> Idris [PTerm]
419nameMissing ps = do ist <- get
420 newPats <- mapM nm ps
421 let newPats' = mergeAllPats ist (sUN "_") (base (head ps))
422 newPats
423 return (map fst newPats')
424 where
425 base (PApp fc f args) = PApp fc f (map (fmap (const (PRef fc [] (sUN "_")))) args)
426 base t = t
428 nm ptm = do mptm <- elabNewPat ptm
429 case mptm of
430 Nothing -> return ptm
431 Just ptm' -> return ptm'