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