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