git.iko.soy/Idris-dev
on 307efbb help sign in
Idris-dev/src/Idris/CaseSplit.hs
381 lines 15 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.CaseSplit(splitOnLine, replaceSplits,
4 getClause, getProofClause,
5 mkWith,
6 nameMissing,
7 getUniq, nameRoot) where
9-- splitting a variable in a pattern clause
11import Idris.AbsSyntax
12import Idris.ElabDecls
13import Idris.ElabTerm
14import Idris.Delaborate
15import Idris.Parser
16import Idris.Error
18import Idris.Core.TT
19import Idris.Core.Typecheck
20import Idris.Core.Evaluate
22import Data.Maybe
23import Data.Char
24import Control.Monad
25import Control.Monad.State.Strict
27import Text.Parser.Combinators
28import Text.Parser.Char(anyChar)
29import Text.Trifecta(Result(..), parseString)
30import Text.Trifecta.Delta
31import qualified Data.ByteString.UTF8 as UTF8
33import Debug.Trace
35{-
37Given a pattern clause and a variable 'n', elaborate the clause and find the
38type of 'n'.
40Make new pattern clauses by replacing 'n' with all the possibly constructors
41applied to '_', and replacing all other variables with '_' in order to
42resolve other dependencies.
44Finally, merge the generated patterns with the original, by matching.
45Always take the "more specific" argument when there is a discrepancy, i.e.
46names over '_', patterns over names, etc.
47-}
49-- Given a variable to split, and a term application, return a list of
50-- variable updates
51split :: Name -> PTerm -> Idris [[(Name, PTerm)]]
52split n t'
53 = do ist <- getIState
54 (tm, ty, pats) <- elabValBind toplevel True (addImplPat ist t')
55 logLvl 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)
56-- iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))
57-- iputStrLn (show pats)
58 let t = mergeUserImpl (addImplPat ist t') (delab ist tm)
59 let ctxt = tt_ctxt ist
60 case lookup n pats of
61 Nothing -> fail $ show n ++ " is not a pattern variable"
62 Just ty ->
63 do let splits = findPats ist ty
64 iLOG ("New patterns " ++ showSep ", "
65 (map showTmImpls splits))
66 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)
67 logLvl 4 ("Working from " ++ show t)
68 logLvl 4 ("Trying " ++ showSep "\n"
69 (map (showTmImpls) newPats_in))
70 newPats <- mapM elabNewPat newPats_in
71 logLvl 3 ("Original:\n" ++ show t)
72 logLvl 3 ("Split:\n" ++
73 (showSep "\n" (map show (mapMaybe id newPats))))
74 logLvl 3 "----"
75 let newPats' = mergeAllPats ist n t (mapMaybe id newPats)
76 iLOG ("Name updates " ++ showSep "\n"
77 (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))
78 return (map snd newPats')
80data MergeState = MS { namemap :: [(Name, Name)],
81 invented :: [(Name, Name)],
82 explicit :: [Name],
83 updates :: [(Name, PTerm)] }
85addUpdate n tm = do ms <- get
86 put (ms { updates = ((n, stripNS tm) : updates ms) } )
88inventName ist ty n =
89 do ms <- get
90 let supp = case ty of
91 Nothing -> []
92 Just t -> getNameHints ist t
93 let nsupp = case n of
94 MN i n | not (tnull n) && thead n == '_'
95 -> mkSupply (supp ++ varlist)
96 MN i n -> mkSupply (UN n : supp ++ varlist)
97 x -> mkSupply (x : supp)
98 let badnames = map snd (namemap ms) ++ map snd (invented ms) ++
99 explicit ms
100 case lookup n (invented ms) of
101 Just n' -> return n'
102 Nothing ->
103 do let n' = uniqueNameFrom nsupp badnames
104 put (ms { invented = (n, n') : invented ms })
105 return n'
107mkSupply ns = mkSupply' ns (map nextName ns)
108 where mkSupply' xs ns' = xs ++ mkSupply ns'
110varlist = map (sUN . (:[])) "xyzwstuv" -- EB's personal preference :)
112stripNS tm = mapPT dens tm where
113 dens (PRef fc n) = PRef fc (nsroot n)
114 dens t = t
116mergeAllPats :: IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
117mergeAllPats ist cv t [] = []
118mergeAllPats ist cv t (p : ps)
119 = let (p', MS _ _ _ u) = runState (mergePat ist t p Nothing)
120 (MS [] [] (filter (/=cv) (patvars t)) [])
121 ps' = mergeAllPats ist cv t ps in
122 ((p', u) : ps')
123 where patvars (PRef _ n) = [n]
124 patvars (PApp _ _ as) = concatMap (patvars . getTm) as
125 patvars (PPatvar _ n) = [n]
126 patvars _ = []
128mergePat :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
129-- If any names are unified, make sure they stay unified. Always prefer
130-- user provided name (first pattern)
131mergePat ist (PPatvar fc n) new t
132 = mergePat ist (PRef fc n) new t
133mergePat ist old (PPatvar fc n) t
134 = mergePat ist old (PRef fc n) t
135mergePat ist orig@(PRef fc n) new@(PRef _ n') t
136 | isDConName n' (tt_ctxt ist) = do addUpdate n new
137 return new
138 | otherwise
139 = do ms <- get
140 case lookup n' (namemap ms) of
141 Just x -> do addUpdate n (PRef fc x)
142 return (PRef fc x)
143 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })
144 return (PRef fc n)
145mergePat ist (PApp _ _ args) (PApp fc f args') t
146 = do newArgs <- zipWithM mergeArg args (zip args' (argTys ist f))
147 return (PApp fc f newArgs)
148 where mergeArg x (y, t)
149 = do tm' <- mergePat ist (getTm x) (getTm y) t
150 case x of
151 (PImp _ _ _ _ _ _) ->
152 return (y { machine_inf = machine_inf x,
153 getTm = tm' })
154 _ -> return (y { getTm = tm' })
155mergePat ist (PRef fc n) tm ty = do tm <- tidy ist tm ty
156 addUpdate n tm
157 return tm
158mergePat ist x y t = return y
160mergeUserImpl :: PTerm -> PTerm -> PTerm
161mergeUserImpl x y = x
163argTys :: IState -> PTerm -> [Maybe Name]
164argTys ist (PRef fc n)
165 = case lookupTy n (tt_ctxt ist) of
166 [ty] -> map (tyName . snd) (getArgTys ty) ++ repeat Nothing
167 _ -> repeat Nothing
168 where tyName (Bind _ (Pi _) _) = Just (sUN "->")
169 tyName t | (P _ n _, _) <- unApply t = Just n
170 | otherwise = Nothing
171argTys _ _ = repeat Nothing
173tidy :: IState -> PTerm -> Maybe Name -> State MergeState PTerm
174tidy ist orig@(PRef fc n) ty
175 = do ms <- get
176 case lookup n (namemap ms) of
177 Just x -> return (PRef fc x)
178 Nothing -> case n of
179 (UN _) -> return orig
180 _ -> do n' <- inventName ist ty n
181 return (PRef fc n')
182tidy ist (PApp fc f args) ty
183 = do args' <- zipWithM tidyArg args (argTys ist f)
184 return (PApp fc f args')
185 where tidyArg x ty' = do tm' <- tidy ist (getTm x) ty'
186 return (x { getTm = tm' })
187tidy ist tm ty = return tm
190-- mapPT tidyVar tm
191-- where tidyVar (PRef _ _) = Placeholder
192-- tidyVar t = t
194elabNewPat :: PTerm -> Idris (Maybe PTerm)
195elabNewPat t = idrisCatch (do (tm, ty) <- elabVal toplevel True t
196 i <- getIState
197 return (Just (delab i tm)))
198 (\e -> do i <- getIState
199 logLvl 5 $ "Not a valid split:\n" ++ pshow i e
200 return Nothing)
202findPats :: IState -> Type -> [PTerm]
203findPats ist t | (P _ n _, _) <- unApply t
204 = case lookupCtxt n (idris_datatypes ist) of
205 [ti] -> map genPat (con_names ti)
206 _ -> [Placeholder]
207 where genPat n = case lookupCtxt n (idris_implicits ist) of
208 [args] -> PApp emptyFC (PRef emptyFC n)
209 (map toPlaceholder args)
210 _ -> error $ "Can't happen (genPat) " ++ show n
211 toPlaceholder tm = tm { getTm = Placeholder }
212findPats ist t = [Placeholder]
214replaceVar :: Context -> Name -> PTerm -> PTerm -> PTerm
215replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)
216 where subst :: PTerm -> PTerm
217 subst orig@(PPatvar _ v) | v == n = t
218 | otherwise = Placeholder
219 subst orig@(PRef _ v) | v == n = t
220 | isDConName v ctxt = orig
221 subst (PRef _ _) = Placeholder
222 subst (PApp fc (PRef _ t) pats)
223 | isTConName t ctxt = Placeholder -- infer types
224 subst (PApp fc f pats) = PApp fc f (map substArg pats)
225 subst (PEq fc l r) = Placeholder -- PEq fc (subst l) (subst r)
226 subst x = x
228 substArg arg = arg { getTm = subst (getTm arg) }
230replaceVar ctxt n t pat = pat
232splitOnLine :: Int -- ^ line number
233 -> Name -- ^ variable
234 -> FilePath -- ^ name of file
235 -> Idris [[(Name, PTerm)]]
236splitOnLine l n fn = do
237-- let (before, later) = splitAt (l-1) (lines inp)
238-- i <- getIState
239 cl <- getInternalApp fn l
240 logLvl 3 ("Working with " ++ showTmImpls cl)
241 tms <- split n cl
242-- iputStrLn (showSep "\n" (map show tms))
243 return tms -- "" -- not yet done...
245replaceSplits :: String -> [[(Name, PTerm)]] -> Idris [String]
246replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
247 where
248 rep str [] = str ++ "\n"
249 rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups
251 updateRHSs i [] = return []
252 updateRHSs i (x : xs) = do (x', i') <- updateRHS i x
253 xs' <- updateRHSs i' xs
254 return (x' : xs')
256 updateRHS i ('?':'=':xs) = do (xs', i') <- updateRHS i xs
257 return ("?=" ++ xs', i')
258 updateRHS i ('?':xs) = do let (nm, rest) = span (not . isSpace) xs
259 (nm', i') <- getUniq nm i
260 return ('?':nm' ++ rest, i')
261 updateRHS i (x : xs) = do (xs', i') <- updateRHS i xs
262 return (x : xs', i')
263 updateRHS i [] = return ("", i)
266 -- TMP HACK: If there are Nats, we don't want to show as numerals since
267 -- this isn't supported in a pattern, so special case here
268 nshow (PRef _ (UN z)) | z == txt "Z" = "Z"
269 nshow (PApp _ (PRef _ (UN s)) [x]) | s == txt "S" =
270 "S " ++ addBrackets (nshow (getTm x))
271 nshow t = show t
273 -- if there's any {n} replace with {n=n}
274 expandBraces ('{' : xs)
275 = let (brace, (_:rest)) = span (/= '}') xs in
276 if (not ('=' `elem` brace))
277 then ('{' : brace ++ " = " ++ brace ++ "}") ++
278 expandBraces rest
279 else ('{' : brace ++ "}") ++ expandBraces rest
280 expandBraces (x : xs) = x : expandBraces xs
281 expandBraces [] = []
283 updatePat start n tm [] = []
284 updatePat start n tm ('{':rest) =
285 let (space, rest') = span isSpace rest in
286 '{' : space ++ updatePat False n tm rest'
287 updatePat True n tm xs@(c:rest) | length xs > length n
288 = let (before, after@(next:_)) = splitAt (length n) xs in
289 if (before == n && not (isAlphaNum next))
290 then addBrackets tm ++ updatePat False n tm after
291 else c : updatePat (not (isAlphaNum c)) n tm rest
292 updatePat start n tm (c:rest) = c : updatePat (not (isAlpha c)) n tm rest
294 addBrackets tm | ' ' `elem` tm = "(" ++ tm ++ ")"
295 | otherwise = tm
297getUniq nm i
298 = do ist <- getIState
299 let n = nameRoot [] nm ++ "_" ++ show i
300 case lookupTy (sUN n) (tt_ctxt ist) of
301 [] -> return (n, i+1)
302 _ -> getUniq nm (i+1)
304nameRoot acc nm | all isDigit nm = showSep "_" acc
305nameRoot acc nm =
306 case span (/='_') nm of
307 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after
308 _ -> showSep "_" (acc ++ [nm])
310getClause :: Int -- ^ line number that the type is declared on
311 -> Name -- ^ Function name
312 -> FilePath -- ^ Source file name
313 -> Idris String
314getClause l fn fp = do ty <- getInternalApp fp l
315 ist <- get
316 let ap = mkApp ist ty []
317 return (show fn ++ " " ++ ap ++
318 "= ?" ++ show fn ++ "_rhs")
319 where mkApp i (PPi (Exp _ _ _ False) (MN _ _) ty sc) used
320 = let n = getNameFrom i used ty in
321 show n ++ " " ++ mkApp i sc (n : used)
322 mkApp i (PPi (Exp _ _ _ False) n _ sc) used
323 = show n ++ " " ++ mkApp i sc (n : used)
324 mkApp i (PPi _ _ _ sc) used = mkApp i sc used
325 mkApp i _ _ = ""
327 getNameFrom i used (PPi _ _ _ _)
328 = uniqueNameFrom (mkSupply [sUN "f", sUN "g"]) used
329 getNameFrom i used (PApp fc f as) = getNameFrom i used f
330 getNameFrom i used (PEq _ _ _) = uniqueNameFrom [sUN "prf"] used
331 getNameFrom i used (PRef fc f)
332 = case getNameHints i f of
333 [] -> uniqueName (sUN "x") used
334 ns -> uniqueNameFrom (mkSupply ns) used
335 getNameFrom i used _ = uniqueName (sUN "x") used
337getProofClause :: Int -- ^ line number that the type is declared
338 -> Name -- ^ Function name
339 -> FilePath -- ^ Source file name
340 -> Idris String
341getProofClause l fn fp
342 = do ty <- getInternalApp fp l
343 return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")
344 where mkApp (PPi _ _ _ sc) = mkApp sc
345 mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn
347-- Purely syntactic - turn a pattern match clause into a with and a new
348-- match clause
350mkWith :: String -> Name -> String
351mkWith str n = let str' = replaceRHS str "with (_)"
352 newpat = " " ++
353 replaceRHS str "| with_pat = ?" ++ show n ++ "_rhs" in
354 str' ++ "\n" ++ newpat
356 where replaceRHS [] str = str
357 replaceRHS ('?':'=': rest) str = str
358 replaceRHS ('=': rest) str
359 | not ('=' `elem` rest) = str
360 replaceRHS (x : rest) str = x : replaceRHS rest str
362-- Replace _ with names in missing clauses
364nameMissing :: [PTerm] -> Idris [PTerm]
365nameMissing ps = do ist <- get
366 newPats <- mapM nm ps
367 let newPats' = mergeAllPats ist (sUN "_") (base (head ps))
368 newPats
369 return (map fst newPats')
370 where
371 base (PApp fc f args) = PApp fc f (map (fmap (const (PRef fc (sUN "_")))) args)
372 base t = t
374 nm ptm = do mptm <- elabNewPat ptm
375 case mptm of
376 Nothing -> return ptm
377 Just ptm' -> return ptm'