git.iko.soy/Idris-dev
on eac558e help sign in
Idris-dev/src/Idris/CaseSplit.hs
497 lines 21 kB history raw
1{-|
2Module : Idris.CaseSplit
3Description : Module to provide case split functionality.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
8Given a pattern clause and a variable 'n', elaborate the clause and find the
9type of 'n'.
11Make new pattern clauses by replacing 'n' with all the possibly constructors
12applied to '_', and replacing all other variables with '_' in order to
13resolve other dependencies.
15Finally, merge the generated patterns with the original, by matching.
16Always take the "more specific" argument when there is a discrepancy, i.e.
17names over '_', patterns over names, etc.
19-}
20{-# LANGUAGE PatternGuards #-}
22module Idris.CaseSplit(
23 splitOnLine, replaceSplits
24 , getClause, getProofClause
25 , mkWith
26 , nameMissing
27 , getUniq, nameRoot
28 ) where
30import Idris.AbsSyntax
31import Idris.AbsSyntaxTree (Idris, IState, PTerm)
32import Idris.ElabDecls
33import Idris.Delaborate
34import Idris.Parser
35import Idris.Parser.Helpers
36import Idris.Error
37import Idris.Output
39import Idris.Elab.Value
40import Idris.Elab.Term
42import Idris.Core.TT
43import Idris.Core.Typecheck
44import Idris.Core.Evaluate
46import Data.Maybe
47import Data.Char
48import Data.List (isPrefixOf, isSuffixOf)
49import Control.Monad
50import Control.Monad.State.Strict
52import Text.Parser.Combinators
53import Text.Parser.Char(anyChar)
54import Text.Trifecta(Result(..), parseString)
55import Text.Trifecta.Delta
57import Debug.Trace
59-- | Given a variable to split, and a term application, return a list
60-- of variable updates, paired with a flag to say whether the given
61-- update typechecks (False = impossible) if the flag is 'False' the
62-- splits should be output with the 'impossible' flag, otherwise they
63-- should be output as normal
64split :: Name -> PTerm -> Idris (Bool, [[(Name, PTerm)]])
65split n t'
66 = do ist <- getIState
67 -- Make sure all the names in the term are accessible
68 mapM_ (\n -> setAccessibility n Public) (allNamesIn t')
69 -- ETyDecl rather then ELHS because there'll be explicit type
70 -- matching
71 (tm, ty, pats) <- elabValBind (recinfo (fileFC "casesplit")) ETyDecl True (addImplPat ist t')
72 -- ASSUMPTION: tm is in normal form after elabValBind, so we don't
73 -- need to do anything special to find out what family each argument
74 -- is in
75 logElab 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)
76-- iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))
77-- iputStrLn (show pats)
78 let t = mergeUserImpl (addImplPat ist t') (delabDirect ist tm)
79 let ctxt = tt_ctxt ist
80 case lookup n pats of
81 Nothing -> ifail $ show n ++ " is not a pattern variable"
82 Just ty ->
83 do let splits = findPats ist ty
84 logElab 1 ("New patterns " ++ showSep ", "
85 (map showTmImpls splits))
86 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)
87 logElab 4 ("Working from " ++ showTmImpls t)
88 logElab 4 ("Trying " ++ showSep "\n"
89 (map (showTmImpls) newPats_in))
90 newPats_in <- mapM elabNewPat newPats_in
91 case anyValid [] [] newPats_in of
92 Left fails -> do
93 let fails' = mergeAllPats ist n t fails
94 return (False, (map snd fails'))
95 Right newPats -> do
96 logElab 3 ("Original:\n" ++ show t)
97 logElab 3 ("Split:\n" ++
98 (showSep "\n" (map show newPats)))
99 logElab 3 "----"
100 let newPats' = mergeAllPats ist n t newPats
101 logElab 1 ("Name updates " ++ showSep "\n"
102 (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))
103 return (True, (map snd newPats'))
104 where
105 anyValid ok bad [] = if null ok then Left (reverse bad)
106 else Right (reverse ok)
107 anyValid ok bad ((tc, p) : ps)
108 | tc = anyValid (p : ok) bad ps
109 | otherwise = anyValid ok (p : bad) ps
111data MergeState = MS { namemap :: [(Name, Name)],
112 invented :: [(Name, Name)],
113 explicit :: [Name],
114 updates :: [(Name, PTerm)] }
116addUpdate :: Name -> Idris.AbsSyntaxTree.PTerm -> State MergeState ()
117addUpdate n tm = do ms <- get
118 put (ms { updates = ((n, stripNS tm) : updates ms) } )
120inventName :: Idris.AbsSyntaxTree.IState -> Maybe Name -> Name -> State MergeState Name
121inventName ist ty n =
122 do ms <- get
123 let supp = case ty of
124 Nothing -> []
125 Just t -> getNameHints ist t
126 let nsupp = case n of
127 MN i n | not (tnull n) && thead n == '_'
128 -> mkSupply (supp ++ varlist)
129 MN i n -> mkSupply (UN n : supp ++ varlist)
130 UN n | thead n == '_'
131 -> mkSupply (supp ++ varlist)
132 x -> mkSupply (x : supp)
133 let badnames = map snd (namemap ms) ++ map snd (invented ms) ++
134 explicit ms
135 case lookup n (invented ms) of
136 Just n' -> return n'
137 Nothing ->
138 do let n' = uniqueNameFrom nsupp badnames
139 put (ms { invented = (n, n') : invented ms })
140 return n'
142mkSupply :: [Name] -> [Name]
143mkSupply ns = mkSupply' ns (map nextName ns)
144 where mkSupply' xs ns' = xs ++ mkSupply ns'
146varlist :: [Name]
147varlist = map (sUN . (:[])) "xyzwstuv" -- EB's personal preference :)
149stripNS :: Idris.AbsSyntaxTree.PTerm -> Idris.AbsSyntaxTree.PTerm
150stripNS tm = mapPT dens tm where
151 dens (PRef fc hls n) = PRef fc hls (nsroot n)
152 dens t = t
154mergeAllPats :: IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
155mergeAllPats ist cv t [] = []
156mergeAllPats ist cv t (p : ps)
157 = let (p', MS _ _ _ u) = runState (mergePat ist t p Nothing)
158 (MS [] [] (filter (/=cv) (patvars t)) [])
159 ps' = mergeAllPats ist cv t ps in
160 ((p', u) : ps')
161 where patvars (PRef _ _ n) = [n]
162 patvars (PApp _ _ as) = concatMap (patvars . getTm) as
163 patvars (PPatvar _ n) = [n]
164 patvars _ = []
166mergePat :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
167mergePat ist orig new t =
168 do -- collect user names for name map, by matching user pattern against
169 -- the generated pattern
170 case matchClause ist orig new of
171 Left _ -> return ()
172 Right ns -> mapM_ addNameMap ns
173 mergePat' ist orig new t
174 where
175 addNameMap (n, PRef fc _ n') = do ms <- get
176 put (ms { namemap = ((n', n) : namemap ms) })
177 addNameMap _ = return ()
179-- | If any names are unified, make sure they stay unified. Always
180-- prefer user provided name (first pattern)
181mergePat' ist (PPatvar fc n) new t
182 = mergePat' ist (PRef fc [] n) new t
183mergePat' ist old (PPatvar fc n) t
184 = mergePat' ist old (PRef fc [] n) t
185mergePat' ist orig@(PRef fc _ n) new@(PRef _ _ n') t
186 | isDConName n' (tt_ctxt ist) = do addUpdate n new
187 return new
188 | otherwise
189 = do ms <- get
190 case lookup n' (namemap ms) of
191 Just x -> do addUpdate n (PRef fc [] x)
192 return (PRef fc [] x)
193 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })
194 return (PRef fc [] n)
195mergePat' ist (PApp _ _ args) (PApp fc f args') t
196 = do newArgs <- zipWithM mergeArg args (zip args' (argTys ist f))
197 return (PApp fc f newArgs)
198 where mergeArg x (y, t)
199 = do tm' <- mergePat' ist (getTm x) (getTm y) t
200 case x of
201 (PImp _ _ _ _ _) ->
202 return (y { machine_inf = machine_inf x,
203 getTm = tm' })
204 _ -> return (y { getTm = tm' })
205mergePat' ist (PRef fc _ n) tm ty = do tm <- tidy ist tm ty
206 addUpdate n tm
207 return tm
208mergePat' ist x y t = return y
210mergeUserImpl :: PTerm -> PTerm -> PTerm
211mergeUserImpl x y = x
213argTys :: IState -> PTerm -> [Maybe Name]
214argTys ist (PRef fc hls n)
215 = case lookupTy n (tt_ctxt ist) of
216 [ty] -> let ty' = normalise (tt_ctxt ist) [] ty in
217 map (tyName . snd) (getArgTys ty') ++ repeat Nothing
218 _ -> repeat Nothing
219 where tyName (Bind _ (Pi _ _ _) _) = Just (sUN "->")
220 tyName t | (P _ d _, [_, ty]) <- unApply t,
221 d == sUN "Delayed" = tyName ty
222 | (P _ n _, _) <- unApply t = Just n
223 | otherwise = Nothing
224argTys _ _ = repeat Nothing
226tidy :: IState -> PTerm -> Maybe Name -> State MergeState PTerm
227tidy ist orig@(PRef fc hls n) ty
228 = do ms <- get
229 case lookup n (namemap ms) of
230 Just x -> return (PRef fc [] x)
231 Nothing -> case n of
232 (UN _) -> return orig
233 _ -> do n' <- inventName ist ty n
234 return (PRef fc [] n')
235tidy ist (PApp fc f args) ty
236 = do args' <- zipWithM tidyArg args (argTys ist f)
237 return (PApp fc f args')
238 where tidyArg x ty' = do tm' <- tidy ist (getTm x) ty'
239 return (x { getTm = tm' })
240tidy ist tm ty = return tm
243-- mapPT tidyVar tm
244-- where tidyVar (PRef _ _) = Placeholder
245-- tidyVar t = t
247elabNewPat :: PTerm -> Idris (Bool, PTerm)
248elabNewPat t = idrisCatch (do (tm, ty) <- elabVal (recinfo (fileFC "casesplit")) ELHS t
249 i <- getIState
250 return (True, delabDirect i tm))
251 (\e -> do i <- getIState
252 logElab 5 $ "Not a valid split:\n" ++ showTmImpls t ++ "\n"
253 ++ pshow i e
254 return (False, t))
256findPats :: IState -> Type -> [PTerm]
257findPats ist t | (P _ n _, _) <- unApply t
258 = case lookupCtxt n (idris_datatypes ist) of
259 [ti] -> map genPat (con_names ti)
260 _ -> [Placeholder]
261 where genPat n = case lookupCtxt n (idris_implicits ist) of
262 [args] -> PApp emptyFC (PRef emptyFC [] n)
263 (map toPlaceholder args)
264 _ -> error $ "Can't happen (genPat) " ++ show n
265 toPlaceholder tm = tm { getTm = Placeholder }
266findPats ist t = [Placeholder]
268replaceVar :: Context -> Name -> PTerm -> PTerm -> PTerm
269replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)
270 where subst :: PTerm -> PTerm
271 subst orig@(PPatvar _ v) | v == n = t
272 | otherwise = Placeholder
273 subst orig@(PRef _ _ v) | v == n = t
274 | isDConName v ctxt = orig
275 subst (PRef _ _ _) = Placeholder
276 subst (PApp fc (PRef _ _ t) pats)
277 | isTConName t ctxt = Placeholder -- infer types
278 subst (PApp fc f pats) = PApp fc f (map substArg pats)
279 subst x = x
281 substArg arg = arg { getTm = subst (getTm arg) }
283replaceVar ctxt n t pat = pat
285splitOnLine :: Int -- ^ line number
286 -> Name -- ^ variable
287 -> FilePath -- ^ name of file
288 -> Idris (Bool, [[(Name, PTerm)]])
289splitOnLine l n fn = do
290 cl <- getInternalApp fn l
291 logElab 3 ("Working with " ++ showTmImpls cl)
292 tms <- split n cl
293 return tms
295replaceSplits :: String -> [[(Name, PTerm)]] -> Bool -> Idris [String]
296replaceSplits l ups impossible
297 = do ist <- getIState
298 updateRHSs 1 (map (rep ist (expandBraces l)) ups)
299 where
300 rep ist str [] = str ++ "\n"
301 rep ist str ((n, tm) : ups)
302 = rep ist (updatePat False (show n) (nshow (resugar ist tm)) str) ups
304 updateRHSs i [] = return []
305 updateRHSs i (x : xs)
306 | impossible = do xs' <- updateRHSs i xs
307 return (setImpossible False x : xs')
308 | otherwise = do (x', i') <- updateRHS (null xs) i x
309 xs' <- updateRHSs i' xs
310 return (x' : xs')
312 updateRHS last i ('?':'=':xs) = do (xs', i') <- updateRHS last i xs
313 return ("?=" ++ xs', i')
314 updateRHS last i ('?':xs)
315 = do let (nm, rest_in) = span (not . (\x -> isSpace x || x == ')'
316 || x == '(')) xs
317 let rest = if last then rest_in else
318 case span (not . (=='\n')) rest_in of
319 (_, restnl) -> restnl
320 (nm', i') <- getUniq nm i
321 return ('?':nm' ++ rest, i')
322 updateRHS last i (x : xs) = do (xs', i') <- updateRHS last i xs
323 return (x : xs', i')
324 updateRHS last i [] = return ("", i)
326 setImpossible brace ('}':xs) = '}' : setImpossible False xs
327 setImpossible brace ('{':xs) = '{' : setImpossible True xs
328 setImpossible False ('=':xs) = "impossible\n"
329 setImpossible brace (x : xs) = x : setImpossible brace xs
330 setImpossible brace [] = ""
332 -- TMP HACK: If there are Nats, we don't want to show as numerals since
333 -- this isn't supported in a pattern, so special case here
334 nshow (PRef _ _ (UN z)) | z == txt "Z" = "Z"
335 nshow (PApp _ (PRef _ _ (UN s)) [x]) | s == txt "S" =
336 "(S " ++ addBrackets (nshow (getTm x)) ++ ")"
337 nshow t = show t
339 -- if there's any {n} replace with {n=n}
340 -- but don't replace it in comments
341 expandBraces ('{' : '-' : xs) = '{' : '-' : xs
342 expandBraces ('{' : xs)
343 = let (brace, (_:rest)) = span (/= '}') xs in
344 if (not ('=' `elem` brace))
345 then ('{' : brace ++ " = " ++ brace ++ "}") ++
346 expandBraces rest
347 else ('{' : brace ++ "}") ++ expandBraces rest
348 expandBraces (x : xs) = x : expandBraces xs
349 expandBraces [] = []
351 updatePat start n tm [] = []
352 updatePat start n tm ('{':rest) =
353 let (space, rest') = span isSpace rest in
354 '{' : space ++ updatePat False n tm rest'
355 updatePat start n tm done@('?':rest) = done
356 updatePat True n tm xs@(c:rest) | length xs > length n
357 = let (before, after@(next:_)) = splitAt (length n) xs in
358 if (before == n && not (isAlphaNum next))
359 then addBrackets tm ++ updatePat False n tm after
360 else c : updatePat (not (isAlphaNum c)) n tm rest
361 updatePat start n tm (c:rest) = c : updatePat (not ((isAlphaNum c) || c == '_')) n tm rest
363 addBrackets tm | ' ' `elem` tm
364 , not (isPrefixOf "(" tm && isSuffixOf ")" tm)
365 = "(" ++ tm ++ ")"
366 | otherwise = tm
369getUniq :: (Show t, Num t) => [Char] -> t -> Idris ([Char], t)
370getUniq nm i
371 = do ist <- getIState
372 let n = nameRoot [] nm ++ "_" ++ show i
373 case lookupTy (sUN n) (tt_ctxt ist) of
374 [] -> return (n, i+1)
375 _ -> getUniq nm (i+1)
377nameRoot acc nm | all isDigit nm = showSep "_" acc
378nameRoot acc nm =
379 case span (/='_') nm of
380 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after
381 _ -> showSep "_" (acc ++ [nm])
383-- Show a name for use in pattern definitions on the lhs
384showLHSName :: Name -> String
385showLHSName n = let fn = show n in
386 if any (flip elem opChars) fn
387 then "(" ++ fn ++ ")"
388 else fn
390-- Show a name for the purpose of generating a metavariable name on the rhs
391showRHSName :: Name -> String
392showRHSName n = let fn = show n in
393 if any (flip elem opChars) fn
394 then "op"
395 else fn
397getClause :: Int -- ^ line number that the type is declared on
398 -> Name -- ^ Function name
399 -> Name -- ^ User given name
400 -> FilePath -- ^ Source file name
401 -> Idris String
402getClause l fn un fp
403 = do i <- getIState
404 case lookupCtxt un (idris_classes i) of
405 [c] -> return (mkClassBodies i (class_methods c))
406 _ -> do ty_in <- getInternalApp fp l
407 let ty = case ty_in of
408 PTyped n t -> t
409 x -> x
410 ist <- get
411 let ap = mkApp ist ty []
412 return (showLHSName un ++ " " ++ ap ++ "= ?"
413 ++ showRHSName un ++ "_rhs")
414 where mkApp :: IState -> PTerm -> [Name] -> String
415 mkApp i (PPi (Exp _ _ False) (MN _ _) _ ty sc) used
416 = let n = getNameFrom i used ty in
417 show n ++ " " ++ mkApp i sc (n : used)
418 mkApp i (PPi (Exp _ _ False) (UN n) _ ty sc) used
419 | thead n == '_'
420 = let n = getNameFrom i used ty in
421 show n ++ " " ++ mkApp i sc (n : used)
422 mkApp i (PPi (Exp _ _ False) n _ _ sc) used
423 = show n ++ " " ++ mkApp i sc (n : used)
424 mkApp i (PPi _ _ _ _ sc) used = mkApp i sc used
425 mkApp i _ _ = ""
427 getNameFrom i used (PPi _ _ _ _ _)
428 = uniqueNameFrom (mkSupply [sUN "f", sUN "g"]) used
429 getNameFrom i used (PApp fc f as) = getNameFrom i used f
430 getNameFrom i used (PRef fc _ f)
431 = case getNameHints i f of
432 [] -> uniqueNameFrom (mkSupply [sUN "x", sUN "y",
433 sUN "z"]) used
434 ns -> uniqueNameFrom (mkSupply ns) used
435 getNameFrom i used _ = uniqueNameFrom (mkSupply [sUN "x", sUN "y",
436 sUN "z"]) used
438 -- write method declarations, indent with 4 spaces
439 mkClassBodies :: IState -> [(Name, (Bool, FnOpts, PTerm))] -> String
440 mkClassBodies i ns
441 = showSep "\n"
442 (zipWith (\(n, (_, _, ty)) m -> " " ++
443 def (show (nsroot n)) ++ " "
444 ++ mkApp i ty []
445 ++ "= ?"
446 ++ showRHSName un ++ "_rhs_" ++ show m) ns [1..])
448 def n@(x:xs) | not (isAlphaNum x) = "(" ++ n ++ ")"
449 def n = n
451getProofClause :: Int -- ^ line number that the type is declared
452 -> Name -- ^ Function name
453 -> FilePath -- ^ Source file name
454 -> Idris String
455getProofClause l fn fp
456 = do ty_in <- getInternalApp fp l
457 let ty = case ty_in of
458 PTyped n t -> t
459 x -> x
460 return (mkApp ty ++ " = ?" ++ showRHSName fn ++ "_rhs")
461 where mkApp (PPi _ _ _ _ sc) = mkApp sc
462 mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn
464-- Purely syntactic - turn a pattern match clause into a with and a new
465-- match clause
467mkWith :: String -> Name -> String
468mkWith str n = let str' = replaceRHS str "with (_)"
469 in str' ++ "\n" ++ newpat str
471 where replaceRHS [] str = str
472 replaceRHS ('?':'=': rest) str = str
473 replaceRHS ('=': rest) str
474 | not ('=' `elem` rest) = str
475 replaceRHS (x : rest) str = x : replaceRHS rest str
477 newpat ('>':patstr) = '>':newpat patstr
478 newpat patstr =
479 " " ++
480 replaceRHS patstr "| with_pat = ?" ++ showRHSName n ++ "_rhs"
482-- Replace _ with names in missing clauses
484nameMissing :: [PTerm] -> Idris [PTerm]
485nameMissing ps = do ist <- get
486 newPats <- mapM nm ps
487 let newPats' = mergeAllPats ist (sUN "_") (base (head ps))
488 newPats
489 return (map fst newPats')
490 where
491 base (PApp fc f args) = PApp fc f (map (fmap (const (PRef fc [] (sUN "_")))) args)
492 base t = t
494 nm ptm = do mptm <- elabNewPat ptm
495 case mptm of
496 (False, _) -> return ptm
497 (True, ptm') -> return ptm'