git.iko.soy/Idris-dev
on b3b7bb7 help sign in
Idris-dev/src/Idris/CaseSplit.hs
458 lines 19 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, paired with a flag to say whether the given update
54-- typechecks (False = impossible)
55-- if the flag is 'False' the splits should be output with the 'impossible'
56-- flag, otherwise they should be output as normal
57split :: Name -> PTerm -> Idris (Bool, [[(Name, PTerm)]])
58split n t'
59 = do ist <- getIState
60 -- Make sure all the names in the term are accessible
61 mapM_ (\n -> setAccessibility n Public) (allNamesIn t')
62 -- ETyDecl rather then ELHS because there'll be explicit type
63 -- matching
64 (tm, ty, pats) <- elabValBind recinfo ETyDecl True (addImplPat ist t')
65 -- ASSUMPTION: tm is in normal form after elabValBind, so we don't
66 -- need to do anything special to find out what family each argument
67 -- is in
68 logElab 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)
69-- iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))
70-- iputStrLn (show pats)
71 let t = mergeUserImpl (addImplPat ist t') (delab ist tm)
72 let ctxt = tt_ctxt ist
73 case lookup n pats of
74 Nothing -> ifail $ show n ++ " is not a pattern variable"
75 Just ty ->
76 do let splits = findPats ist ty
77 logElab 1 ("New patterns " ++ showSep ", "
78 (map showTmImpls splits))
79 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)
80 logElab 4 ("Working from " ++ show t)
81 logElab 4 ("Trying " ++ showSep "\n"
82 (map (showTmImpls) newPats_in))
83 newPats_in <- mapM elabNewPat newPats_in
84 case anyValid [] [] newPats_in of
85 Left fails -> do
86 let fails' = mergeAllPats ist n t fails
87 return (False, (map snd fails'))
88 Right newPats -> do
89 logElab 3 ("Original:\n" ++ show t)
90 logElab 3 ("Split:\n" ++
91 (showSep "\n" (map show newPats)))
92 logElab 3 "----"
93 let newPats' = mergeAllPats ist n t newPats
94 logElab 1 ("Name updates " ++ showSep "\n"
95 (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))
96 return (True, (map snd newPats'))
97 where
98 anyValid ok bad [] = if null ok then Left (reverse bad)
99 else Right (reverse ok)
100 anyValid ok bad ((tc, p) : ps)
101 | tc = anyValid (p : ok) bad ps
102 | otherwise = anyValid ok (p : bad) ps
104data MergeState = MS { namemap :: [(Name, Name)],
105 invented :: [(Name, Name)],
106 explicit :: [Name],
107 updates :: [(Name, PTerm)] }
109addUpdate :: Name -> Idris.AbsSyntaxTree.PTerm -> State MergeState ()
110addUpdate n tm = do ms <- get
111 put (ms { updates = ((n, stripNS tm) : updates ms) } )
113inventName :: Idris.AbsSyntaxTree.IState -> Maybe Name -> Name -> State MergeState Name
114inventName ist ty n =
115 do ms <- get
116 let supp = case ty of
117 Nothing -> []
118 Just t -> getNameHints ist t
119 let nsupp = case n of
120 MN i n | not (tnull n) && thead n == '_'
121 -> mkSupply (supp ++ varlist)
122 MN i n -> mkSupply (UN n : supp ++ varlist)
123 UN n | thead n == '_'
124 -> mkSupply (supp ++ varlist)
125 x -> mkSupply (x : supp)
126 let badnames = map snd (namemap ms) ++ map snd (invented ms) ++
127 explicit ms
128 case lookup n (invented ms) of
129 Just n' -> return n'
130 Nothing ->
131 do let n' = uniqueNameFrom nsupp badnames
132 put (ms { invented = (n, n') : invented ms })
133 return n'
135mkSupply :: [Name] -> [Name]
136mkSupply ns = mkSupply' ns (map nextName ns)
137 where mkSupply' xs ns' = xs ++ mkSupply ns'
139varlist :: [Name]
140varlist = map (sUN . (:[])) "xyzwstuv" -- EB's personal preference :)
142stripNS :: Idris.AbsSyntaxTree.PTerm -> Idris.AbsSyntaxTree.PTerm
143stripNS tm = mapPT dens tm where
144 dens (PRef fc hls n) = PRef fc hls (nsroot n)
145 dens t = t
147mergeAllPats :: IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
148mergeAllPats ist cv t [] = []
149mergeAllPats ist cv t (p : ps)
150 = let (p', MS _ _ _ u) = runState (mergePat ist t p Nothing)
151 (MS [] [] (filter (/=cv) (patvars t)) [])
152 ps' = mergeAllPats ist cv t ps in
153 ((p', u) : ps')
154 where patvars (PRef _ _ n) = [n]
155 patvars (PApp _ _ as) = concatMap (patvars . getTm) as
156 patvars (PPatvar _ n) = [n]
157 patvars _ = []
159mergePat :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
160-- If any names are unified, make sure they stay unified. Always prefer
161-- user provided name (first pattern)
162mergePat ist (PPatvar fc n) new t
163 = mergePat ist (PRef fc [] n) new t
164mergePat ist old (PPatvar fc n) t
165 = mergePat ist old (PRef fc [] n) t
166mergePat ist orig@(PRef fc _ n) new@(PRef _ _ n') t
167 | isDConName n' (tt_ctxt ist) = do addUpdate n new
168 return new
169 | otherwise
170 = do ms <- get
171 case lookup n' (namemap ms) of
172 Just x -> do addUpdate n (PRef fc [] x)
173 return (PRef fc [] x)
174 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })
175 return (PRef fc [] n)
176mergePat ist (PApp _ _ args) (PApp fc f args') t
177 = do newArgs <- zipWithM mergeArg args (zip args' (argTys ist f))
178 return (PApp fc f newArgs)
179 where mergeArg x (y, t)
180 = do tm' <- mergePat ist (getTm x) (getTm y) t
181 case x of
182 (PImp _ _ _ _ _) ->
183 return (y { machine_inf = machine_inf x,
184 getTm = tm' })
185 _ -> return (y { getTm = tm' })
186mergePat ist (PRef fc _ n) tm ty = do tm <- tidy ist tm ty
187 addUpdate n tm
188 return tm
189mergePat ist x y t = return y
191mergeUserImpl :: PTerm -> PTerm -> PTerm
192mergeUserImpl x y = x
194argTys :: IState -> PTerm -> [Maybe Name]
195argTys ist (PRef fc hls n)
196 = case lookupTy n (tt_ctxt ist) of
197 [ty] -> map (tyName . snd) (getArgTys ty) ++ repeat Nothing
198 _ -> repeat Nothing
199 where tyName (Bind _ (Pi _ _ _) _) = Just (sUN "->")
200 tyName t | (P _ n _, _) <- unApply t = Just n
201 | otherwise = Nothing
202argTys _ _ = repeat Nothing
204tidy :: IState -> PTerm -> Maybe Name -> State MergeState PTerm
205tidy ist orig@(PRef fc hls n) ty
206 = do ms <- get
207 case lookup n (namemap ms) of
208 Just x -> return (PRef fc [] x)
209 Nothing -> case n of
210 (UN _) -> return orig
211 _ -> do n' <- inventName ist ty n
212 return (PRef fc [] n')
213tidy ist (PApp fc f args) ty
214 = do args' <- zipWithM tidyArg args (argTys ist f)
215 return (PApp fc f args')
216 where tidyArg x ty' = do tm' <- tidy ist (getTm x) ty'
217 return (x { getTm = tm' })
218tidy ist tm ty = return tm
221-- mapPT tidyVar tm
222-- where tidyVar (PRef _ _) = Placeholder
223-- tidyVar t = t
225elabNewPat :: PTerm -> Idris (Bool, PTerm)
226elabNewPat t = idrisCatch (do (tm, ty) <- elabVal recinfo ELHS t
227 i <- getIState
228 return (True, delab i tm))
229 (\e -> do i <- getIState
230 logElab 5 $ "Not a valid split:\n" ++ pshow i e
231 return (False, t))
233findPats :: IState -> Type -> [PTerm]
234findPats ist t | (P _ n _, _) <- unApply t
235 = case lookupCtxt n (idris_datatypes ist) of
236 [ti] -> map genPat (con_names ti)
237 _ -> [Placeholder]
238 where genPat n = case lookupCtxt n (idris_implicits ist) of
239 [args] -> PApp emptyFC (PRef emptyFC [] n)
240 (map toPlaceholder args)
241 _ -> error $ "Can't happen (genPat) " ++ show n
242 toPlaceholder tm = tm { getTm = Placeholder }
243findPats ist t = [Placeholder]
245replaceVar :: Context -> Name -> PTerm -> PTerm -> PTerm
246replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)
247 where subst :: PTerm -> PTerm
248 subst orig@(PPatvar _ v) | v == n = t
249 | otherwise = Placeholder
250 subst orig@(PRef _ _ v) | v == n = t
251 | isDConName v ctxt = orig
252 subst (PRef _ _ _) = Placeholder
253 subst (PApp fc (PRef _ _ t) pats)
254 | isTConName t ctxt = Placeholder -- infer types
255 subst (PApp fc f pats) = PApp fc f (map substArg pats)
256 subst x = x
258 substArg arg = arg { getTm = subst (getTm arg) }
260replaceVar ctxt n t pat = pat
262splitOnLine :: Int -- ^ line number
263 -> Name -- ^ variable
264 -> FilePath -- ^ name of file
265 -> Idris (Bool, [[(Name, PTerm)]])
266splitOnLine l n fn = do
267 cl <- getInternalApp fn l
268 logElab 3 ("Working with " ++ showTmImpls cl)
269 tms <- split n cl
270 return tms
272replaceSplits :: String -> [[(Name, PTerm)]] -> Bool -> Idris [String]
273replaceSplits l ups impossible
274 = updateRHSs 1 (map (rep (expandBraces l)) ups)
275 where
276 rep str [] = str ++ "\n"
277 rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups
279 updateRHSs i [] = return []
280 updateRHSs i (x : xs)
281 | impossible = do xs' <- updateRHSs i xs
282 return (setImpossible False x : xs')
283 | otherwise = do (x', i') <- updateRHS (null xs) i x
284 xs' <- updateRHSs i' xs
285 return (x' : xs')
287 updateRHS last i ('?':'=':xs) = do (xs', i') <- updateRHS last i xs
288 return ("?=" ++ xs', i')
289 updateRHS last i ('?':xs)
290 = do let (nm, rest_in) = span (not . (\x -> isSpace x || x == ')'
291 || x == '(')) xs
292 let rest = if last then rest_in else
293 case span (not . (=='\n')) rest_in of
294 (_, restnl) -> restnl
295 (nm', i') <- getUniq nm i
296 return ('?':nm' ++ rest, i')
297 updateRHS last i (x : xs) = do (xs', i') <- updateRHS last i xs
298 return (x : xs', i')
299 updateRHS last i [] = return ("", i)
301 setImpossible brace ('}':xs) = '}' : setImpossible False xs
302 setImpossible brace ('{':xs) = '{' : setImpossible True xs
303 setImpossible False ('=':xs) = "impossible\n"
304 setImpossible brace (x : xs) = x : setImpossible brace xs
305 setImpossible brace [] = ""
307 -- TMP HACK: If there are Nats, we don't want to show as numerals since
308 -- this isn't supported in a pattern, so special case here
309 nshow (PRef _ _ (UN z)) | z == txt "Z" = "Z"
310 nshow (PApp _ (PRef _ _ (UN s)) [x]) | s == txt "S" =
311 "(S " ++ addBrackets (nshow (getTm x)) ++ ")"
312 nshow t = show t
314 -- if there's any {n} replace with {n=n}
315 -- but don't replace it in comments
316 expandBraces ('{' : '-' : xs) = '{' : '-' : xs
317 expandBraces ('{' : xs)
318 = let (brace, (_:rest)) = span (/= '}') xs in
319 if (not ('=' `elem` brace))
320 then ('{' : brace ++ " = " ++ brace ++ "}") ++
321 expandBraces rest
322 else ('{' : brace ++ "}") ++ expandBraces rest
323 expandBraces (x : xs) = x : expandBraces xs
324 expandBraces [] = []
326 updatePat start n tm [] = []
327 updatePat start n tm ('{':rest) =
328 let (space, rest') = span isSpace rest in
329 '{' : space ++ updatePat False n tm rest'
330 updatePat start n tm done@('?':rest) = done
331 updatePat True n tm xs@(c:rest) | length xs > length n
332 = let (before, after@(next:_)) = splitAt (length n) xs in
333 if (before == n && not (isAlphaNum next))
334 then addBrackets tm ++ updatePat False n tm after
335 else c : updatePat (not (isAlphaNum c)) n tm rest
336 updatePat start n tm (c:rest) = c : updatePat (not ((isAlphaNum c) || c == '_')) n tm rest
338 addBrackets tm | ' ' `elem` tm
339 , not (isPrefixOf "(" tm)
340 , not (isSuffixOf ")" tm) = "(" ++ tm ++ ")"
341 | otherwise = tm
344getUniq :: (Show t, Num t) => [Char] -> t -> Idris ([Char], t)
345getUniq nm i
346 = do ist <- getIState
347 let n = nameRoot [] nm ++ "_" ++ show i
348 case lookupTy (sUN n) (tt_ctxt ist) of
349 [] -> return (n, i+1)
350 _ -> getUniq nm (i+1)
352nameRoot acc nm | all isDigit nm = showSep "_" acc
353nameRoot acc nm =
354 case span (/='_') nm of
355 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after
356 _ -> showSep "_" (acc ++ [nm])
358getClause :: Int -- ^ line number that the type is declared on
359 -> Name -- ^ Function name
360 -> Name -- ^ User given name
361 -> FilePath -- ^ Source file name
362 -> Idris String
363getClause l fn un fp
364 = do i <- getIState
365 case lookupCtxt un (idris_classes i) of
366 [c] -> return (mkClassBodies i (class_methods c))
367 _ -> do ty_in <- getInternalApp fp l
368 let ty = case ty_in of
369 PTyped n t -> t
370 x -> x
371 ist <- get
372 let ap = mkApp ist ty []
373 return (show un ++ " " ++ ap ++ "= ?"
374 ++ show un ++ "_rhs")
375 where mkApp :: IState -> PTerm -> [Name] -> String
376 mkApp i (PPi (Exp _ _ False) (MN _ _) _ ty sc) used
377 = let n = getNameFrom i used ty in
378 show n ++ " " ++ mkApp i sc (n : used)
379 mkApp i (PPi (Exp _ _ False) (UN n) _ ty sc) used
380 | thead n == '_'
381 = let n = getNameFrom i used ty in
382 show n ++ " " ++ mkApp i sc (n : used)
383 mkApp i (PPi (Exp _ _ False) n _ _ sc) used
384 = show n ++ " " ++ mkApp i sc (n : used)
385 mkApp i (PPi _ _ _ _ sc) used = mkApp i sc used
386 mkApp i _ _ = ""
388 getNameFrom i used (PPi _ _ _ _ _)
389 = uniqueNameFrom (mkSupply [sUN "f", sUN "g"]) used
390 getNameFrom i used (PApp fc f as) = getNameFrom i used f
391 getNameFrom i used (PRef fc _ f)
392 = case getNameHints i f of
393 [] -> uniqueNameFrom (mkSupply [sUN "x", sUN "y",
394 sUN "z"]) used
395 ns -> uniqueNameFrom (mkSupply ns) used
396 getNameFrom i used _ = uniqueNameFrom (mkSupply [sUN "x", sUN "y",
397 sUN "z"]) used
399 -- write method declarations, indent with 4 spaces
400 mkClassBodies :: IState -> [(Name, (FnOpts, PTerm))] -> String
401 mkClassBodies i ns
402 = showSep "\n"
403 (zipWith (\(n, (_, ty)) m -> " " ++
404 def (show (nsroot n)) ++ " "
405 ++ mkApp i ty []
406 ++ "= ?"
407 ++ show un ++ "_rhs_" ++ show m) ns [1..])
409 def n@(x:xs) | not (isAlphaNum x) = "(" ++ n ++ ")"
410 def n = n
412getProofClause :: Int -- ^ line number that the type is declared
413 -> Name -- ^ Function name
414 -> FilePath -- ^ Source file name
415 -> Idris String
416getProofClause l fn fp
417 = do ty_in <- getInternalApp fp l
418 let ty = case ty_in of
419 PTyped n t -> t
420 x -> x
421 return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")
422 where mkApp (PPi _ _ _ _ sc) = mkApp sc
423 mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn
425-- Purely syntactic - turn a pattern match clause into a with and a new
426-- match clause
428mkWith :: String -> Name -> String
429mkWith str n = let str' = replaceRHS str "with (_)"
430 in str' ++ "\n" ++ newpat str
432 where replaceRHS [] str = str
433 replaceRHS ('?':'=': rest) str = str
434 replaceRHS ('=': rest) str
435 | not ('=' `elem` rest) = str
436 replaceRHS (x : rest) str = x : replaceRHS rest str
438 newpat ('>':patstr) = '>':newpat patstr
439 newpat patstr =
440 " " ++
441 replaceRHS patstr "| with_pat = ?" ++ show n ++ "_rhs"
443-- Replace _ with names in missing clauses
445nameMissing :: [PTerm] -> Idris [PTerm]
446nameMissing ps = do ist <- get
447 newPats <- mapM nm ps
448 let newPats' = mergeAllPats ist (sUN "_") (base (head ps))
449 newPats
450 return (map fst newPats')
451 where
452 base (PApp fc f args) = PApp fc f (map (fmap (const (PRef fc [] (sUN "_")))) args)
453 base t = t
455 nm ptm = do mptm <- elabNewPat ptm
456 case mptm of
457 (False, _) -> return ptm
458 (True, ptm') -> return ptm'