git.iko.soy/Idris-dev
on 0cb9b4e help sign in
Idris-dev/src/Idris/CaseSplit.hs
459 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 " ++ showTmImpls 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" ++ showTmImpls t ++ "\n"
231 ++ pshow i e
232 return (False, t))
234findPats :: IState -> Type -> [PTerm]
235findPats ist t | (P _ n _, _) <- unApply t
236 = case lookupCtxt n (idris_datatypes ist) of
237 [ti] -> map genPat (con_names ti)
238 _ -> [Placeholder]
239 where genPat n = case lookupCtxt n (idris_implicits ist) of
240 [args] -> PApp emptyFC (PRef emptyFC [] n)
241 (map toPlaceholder args)
242 _ -> error $ "Can't happen (genPat) " ++ show n
243 toPlaceholder tm = tm { getTm = Placeholder }
244findPats ist t = [Placeholder]
246replaceVar :: Context -> Name -> PTerm -> PTerm -> PTerm
247replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)
248 where subst :: PTerm -> PTerm
249 subst orig@(PPatvar _ v) | v == n = t
250 | otherwise = Placeholder
251 subst orig@(PRef _ _ v) | v == n = t
252 | isDConName v ctxt = orig
253 subst (PRef _ _ _) = Placeholder
254 subst (PApp fc (PRef _ _ t) pats)
255 | isTConName t ctxt = Placeholder -- infer types
256 subst (PApp fc f pats) = PApp fc f (map substArg pats)
257 subst x = x
259 substArg arg = arg { getTm = subst (getTm arg) }
261replaceVar ctxt n t pat = pat
263splitOnLine :: Int -- ^ line number
264 -> Name -- ^ variable
265 -> FilePath -- ^ name of file
266 -> Idris (Bool, [[(Name, PTerm)]])
267splitOnLine l n fn = do
268 cl <- getInternalApp fn l
269 logElab 3 ("Working with " ++ showTmImpls cl)
270 tms <- split n cl
271 return tms
273replaceSplits :: String -> [[(Name, PTerm)]] -> Bool -> Idris [String]
274replaceSplits l ups impossible
275 = updateRHSs 1 (map (rep (expandBraces l)) ups)
276 where
277 rep str [] = str ++ "\n"
278 rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups
280 updateRHSs i [] = return []
281 updateRHSs i (x : xs)
282 | impossible = do xs' <- updateRHSs i xs
283 return (setImpossible False x : xs')
284 | otherwise = do (x', i') <- updateRHS (null xs) i x
285 xs' <- updateRHSs i' xs
286 return (x' : xs')
288 updateRHS last i ('?':'=':xs) = do (xs', i') <- updateRHS last i xs
289 return ("?=" ++ xs', i')
290 updateRHS last i ('?':xs)
291 = do let (nm, rest_in) = span (not . (\x -> isSpace x || x == ')'
292 || x == '(')) xs
293 let rest = if last then rest_in else
294 case span (not . (=='\n')) rest_in of
295 (_, restnl) -> restnl
296 (nm', i') <- getUniq nm i
297 return ('?':nm' ++ rest, i')
298 updateRHS last i (x : xs) = do (xs', i') <- updateRHS last i xs
299 return (x : xs', i')
300 updateRHS last i [] = return ("", i)
302 setImpossible brace ('}':xs) = '}' : setImpossible False xs
303 setImpossible brace ('{':xs) = '{' : setImpossible True xs
304 setImpossible False ('=':xs) = "impossible\n"
305 setImpossible brace (x : xs) = x : setImpossible brace xs
306 setImpossible brace [] = ""
308 -- TMP HACK: If there are Nats, we don't want to show as numerals since
309 -- this isn't supported in a pattern, so special case here
310 nshow (PRef _ _ (UN z)) | z == txt "Z" = "Z"
311 nshow (PApp _ (PRef _ _ (UN s)) [x]) | s == txt "S" =
312 "(S " ++ addBrackets (nshow (getTm x)) ++ ")"
313 nshow t = show t
315 -- if there's any {n} replace with {n=n}
316 -- but don't replace it in comments
317 expandBraces ('{' : '-' : xs) = '{' : '-' : xs
318 expandBraces ('{' : xs)
319 = let (brace, (_:rest)) = span (/= '}') xs in
320 if (not ('=' `elem` brace))
321 then ('{' : brace ++ " = " ++ brace ++ "}") ++
322 expandBraces rest
323 else ('{' : brace ++ "}") ++ expandBraces rest
324 expandBraces (x : xs) = x : expandBraces xs
325 expandBraces [] = []
327 updatePat start n tm [] = []
328 updatePat start n tm ('{':rest) =
329 let (space, rest') = span isSpace rest in
330 '{' : space ++ updatePat False n tm rest'
331 updatePat start n tm done@('?':rest) = done
332 updatePat True n tm xs@(c:rest) | length xs > length n
333 = let (before, after@(next:_)) = splitAt (length n) xs in
334 if (before == n && not (isAlphaNum next))
335 then addBrackets tm ++ updatePat False n tm after
336 else c : updatePat (not (isAlphaNum c)) n tm rest
337 updatePat start n tm (c:rest) = c : updatePat (not ((isAlphaNum c) || c == '_')) n tm rest
339 addBrackets tm | ' ' `elem` tm
340 , not (isPrefixOf "(" tm)
341 , not (isSuffixOf ")" tm) = "(" ++ tm ++ ")"
342 | otherwise = tm
345getUniq :: (Show t, Num t) => [Char] -> t -> Idris ([Char], t)
346getUniq nm i
347 = do ist <- getIState
348 let n = nameRoot [] nm ++ "_" ++ show i
349 case lookupTy (sUN n) (tt_ctxt ist) of
350 [] -> return (n, i+1)
351 _ -> getUniq nm (i+1)
353nameRoot acc nm | all isDigit nm = showSep "_" acc
354nameRoot acc nm =
355 case span (/='_') nm of
356 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after
357 _ -> showSep "_" (acc ++ [nm])
359getClause :: Int -- ^ line number that the type is declared on
360 -> Name -- ^ Function name
361 -> Name -- ^ User given name
362 -> FilePath -- ^ Source file name
363 -> Idris String
364getClause l fn un fp
365 = do i <- getIState
366 case lookupCtxt un (idris_classes i) of
367 [c] -> return (mkClassBodies i (class_methods c))
368 _ -> do ty_in <- getInternalApp fp l
369 let ty = case ty_in of
370 PTyped n t -> t
371 x -> x
372 ist <- get
373 let ap = mkApp ist ty []
374 return (show un ++ " " ++ ap ++ "= ?"
375 ++ show un ++ "_rhs")
376 where mkApp :: IState -> PTerm -> [Name] -> String
377 mkApp i (PPi (Exp _ _ False) (MN _ _) _ ty sc) used
378 = let n = getNameFrom i used ty in
379 show n ++ " " ++ mkApp i sc (n : used)
380 mkApp i (PPi (Exp _ _ False) (UN n) _ ty sc) used
381 | thead n == '_'
382 = let n = getNameFrom i used ty in
383 show n ++ " " ++ mkApp i sc (n : used)
384 mkApp i (PPi (Exp _ _ False) n _ _ sc) used
385 = show n ++ " " ++ mkApp i sc (n : used)
386 mkApp i (PPi _ _ _ _ sc) used = mkApp i sc used
387 mkApp i _ _ = ""
389 getNameFrom i used (PPi _ _ _ _ _)
390 = uniqueNameFrom (mkSupply [sUN "f", sUN "g"]) used
391 getNameFrom i used (PApp fc f as) = getNameFrom i used f
392 getNameFrom i used (PRef fc _ f)
393 = case getNameHints i f of
394 [] -> uniqueNameFrom (mkSupply [sUN "x", sUN "y",
395 sUN "z"]) used
396 ns -> uniqueNameFrom (mkSupply ns) used
397 getNameFrom i used _ = uniqueNameFrom (mkSupply [sUN "x", sUN "y",
398 sUN "z"]) used
400 -- write method declarations, indent with 4 spaces
401 mkClassBodies :: IState -> [(Name, (FnOpts, PTerm))] -> String
402 mkClassBodies i ns
403 = showSep "\n"
404 (zipWith (\(n, (_, ty)) m -> " " ++
405 def (show (nsroot n)) ++ " "
406 ++ mkApp i ty []
407 ++ "= ?"
408 ++ show un ++ "_rhs_" ++ show m) ns [1..])
410 def n@(x:xs) | not (isAlphaNum x) = "(" ++ n ++ ")"
411 def n = n
413getProofClause :: Int -- ^ line number that the type is declared
414 -> Name -- ^ Function name
415 -> FilePath -- ^ Source file name
416 -> Idris String
417getProofClause l fn fp
418 = do ty_in <- getInternalApp fp l
419 let ty = case ty_in of
420 PTyped n t -> t
421 x -> x
422 return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")
423 where mkApp (PPi _ _ _ _ sc) = mkApp sc
424 mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn
426-- Purely syntactic - turn a pattern match clause into a with and a new
427-- match clause
429mkWith :: String -> Name -> String
430mkWith str n = let str' = replaceRHS str "with (_)"
431 in str' ++ "\n" ++ newpat str
433 where replaceRHS [] str = str
434 replaceRHS ('?':'=': rest) str = str
435 replaceRHS ('=': rest) str
436 | not ('=' `elem` rest) = str
437 replaceRHS (x : rest) str = x : replaceRHS rest str
439 newpat ('>':patstr) = '>':newpat patstr
440 newpat patstr =
441 " " ++
442 replaceRHS patstr "| with_pat = ?" ++ show n ++ "_rhs"
444-- Replace _ with names in missing clauses
446nameMissing :: [PTerm] -> Idris [PTerm]
447nameMissing ps = do ist <- get
448 newPats <- mapM nm ps
449 let newPats' = mergeAllPats ist (sUN "_") (base (head ps))
450 newPats
451 return (map fst newPats')
452 where
453 base (PApp fc f args) = PApp fc f (map (fmap (const (PRef fc [] (sUN "_")))) args)
454 base t = t
456 nm ptm = do mptm <- elabNewPat ptm
457 case mptm of
458 (False, _) -> return ptm
459 (True, ptm') -> return ptm'