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