git.iko.soy/Idris-dev
on db306ca help sign in
Idris-dev/src/Idris/CaseSplit.hs
387 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
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 UN n | thead n == '_'
98 -> mkSupply (supp ++ varlist)
99 x -> mkSupply (x : supp)
100 let badnames = map snd (namemap ms) ++ map snd (invented ms) ++
101 explicit ms
102 case lookup n (invented ms) of
103 Just n' -> return n'
104 Nothing ->
105 do let n' = uniqueNameFrom nsupp badnames
106 put (ms { invented = (n, n') : invented ms })
107 return n'
109mkSupply ns = mkSupply' ns (map nextName ns)
110 where mkSupply' xs ns' = xs ++ mkSupply ns'
112varlist = map (sUN . (:[])) "xyzwstuv" -- EB's personal preference :)
114stripNS tm = mapPT dens tm where
115 dens (PRef fc n) = PRef fc (nsroot n)
116 dens t = t
118mergeAllPats :: IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
119mergeAllPats ist cv t [] = []
120mergeAllPats ist cv t (p : ps)
121 = let (p', MS _ _ _ u) = runState (mergePat ist t p Nothing)
122 (MS [] [] (filter (/=cv) (patvars t)) [])
123 ps' = mergeAllPats ist cv t ps in
124 ((p', u) : ps')
125 where patvars (PRef _ n) = [n]
126 patvars (PApp _ _ as) = concatMap (patvars . getTm) as
127 patvars (PPatvar _ n) = [n]
128 patvars _ = []
130mergePat :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
131-- If any names are unified, make sure they stay unified. Always prefer
132-- user provided name (first pattern)
133mergePat ist (PPatvar fc n) new t
134 = mergePat ist (PRef fc n) new t
135mergePat ist old (PPatvar fc n) t
136 = mergePat ist old (PRef fc n) t
137mergePat ist orig@(PRef fc n) new@(PRef _ n') t
138 | isDConName n' (tt_ctxt ist) = do addUpdate n new
139 return new
140 | otherwise
141 = do ms <- get
142 case lookup n' (namemap ms) of
143 Just x -> do addUpdate n (PRef fc x)
144 return (PRef fc x)
145 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })
146 return (PRef fc n)
147mergePat ist (PApp _ _ args) (PApp fc f args') t
148 = do newArgs <- zipWithM mergeArg args (zip args' (argTys ist f))
149 return (PApp fc f newArgs)
150 where mergeArg x (y, t)
151 = do tm' <- mergePat ist (getTm x) (getTm y) t
152 case x of
153 (PImp _ _ _ _ _) ->
154 return (y { machine_inf = machine_inf x,
155 getTm = tm' })
156 _ -> return (y { getTm = tm' })
157mergePat ist (PRef fc n) tm ty = do tm <- tidy ist tm ty
158 addUpdate n tm
159 return tm
160mergePat ist x y t = return y
162mergeUserImpl :: PTerm -> PTerm -> PTerm
163mergeUserImpl x y = x
165argTys :: IState -> PTerm -> [Maybe Name]
166argTys ist (PRef fc n)
167 = case lookupTy n (tt_ctxt ist) of
168 [ty] -> map (tyName . snd) (getArgTys ty) ++ repeat Nothing
169 _ -> repeat Nothing
170 where tyName (Bind _ (Pi _) _) = Just (sUN "->")
171 tyName t | (P _ n _, _) <- unApply t = Just n
172 | otherwise = Nothing
173argTys _ _ = repeat Nothing
175tidy :: IState -> PTerm -> Maybe Name -> State MergeState PTerm
176tidy ist orig@(PRef fc n) ty
177 = do ms <- get
178 case lookup n (namemap ms) of
179 Just x -> return (PRef fc x)
180 Nothing -> case n of
181 (UN _) -> return orig
182 _ -> do n' <- inventName ist ty n
183 return (PRef fc n')
184tidy ist (PApp fc f args) ty
185 = do args' <- zipWithM tidyArg args (argTys ist f)
186 return (PApp fc f args')
187 where tidyArg x ty' = do tm' <- tidy ist (getTm x) ty'
188 return (x { getTm = tm' })
189tidy ist tm ty = return tm
192-- mapPT tidyVar tm
193-- where tidyVar (PRef _ _) = Placeholder
194-- tidyVar t = t
196elabNewPat :: PTerm -> Idris (Maybe PTerm)
197elabNewPat t = idrisCatch (do (tm, ty) <- elabVal toplevel True t
198 i <- getIState
199 return (Just (delab i tm)))
200 (\e -> do i <- getIState
201 logLvl 5 $ "Not a valid split:\n" ++ pshow i e
202 return Nothing)
204findPats :: IState -> Type -> [PTerm]
205findPats ist t | (P _ n _, _) <- unApply t
206 = case lookupCtxt n (idris_datatypes ist) of
207 [ti] -> map genPat (con_names ti)
208 _ -> [Placeholder]
209 where genPat n = case lookupCtxt n (idris_implicits ist) of
210 [args] -> PApp emptyFC (PRef emptyFC n)
211 (map toPlaceholder args)
212 _ -> error $ "Can't happen (genPat) " ++ show n
213 toPlaceholder tm = tm { getTm = Placeholder }
214findPats ist t = [Placeholder]
216replaceVar :: Context -> Name -> PTerm -> PTerm -> PTerm
217replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)
218 where subst :: PTerm -> PTerm
219 subst orig@(PPatvar _ v) | v == n = t
220 | otherwise = Placeholder
221 subst orig@(PRef _ v) | v == n = t
222 | isDConName v ctxt = orig
223 subst (PRef _ _) = Placeholder
224 subst (PApp fc (PRef _ t) pats)
225 | isTConName t ctxt = Placeholder -- infer types
226 subst (PApp fc f pats) = PApp fc f (map substArg pats)
227 subst (PEq fc l r) = Placeholder -- PEq fc (subst l) (subst r)
228 subst x = x
230 substArg arg = arg { getTm = subst (getTm arg) }
232replaceVar ctxt n t pat = pat
234splitOnLine :: Int -- ^ line number
235 -> Name -- ^ variable
236 -> FilePath -- ^ name of file
237 -> Idris [[(Name, PTerm)]]
238splitOnLine l n fn = do
239-- let (before, later) = splitAt (l-1) (lines inp)
240-- i <- getIState
241 cl <- getInternalApp fn l
242 logLvl 3 ("Working with " ++ showTmImpls cl)
243 tms <- split n cl
244-- iputStrLn (showSep "\n" (map show tms))
245 return tms -- "" -- not yet done...
247replaceSplits :: String -> [[(Name, PTerm)]] -> Idris [String]
248replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
249 where
250 rep str [] = str ++ "\n"
251 rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups
253 updateRHSs i [] = return []
254 updateRHSs i (x : xs) = do (x', i') <- updateRHS i x
255 xs' <- updateRHSs i' xs
256 return (x' : xs')
258 updateRHS i ('?':'=':xs) = do (xs', i') <- updateRHS i xs
259 return ("?=" ++ xs', i')
260 updateRHS i ('?':xs) = do let (nm, rest) = span (not . isSpace) xs
261 (nm', i') <- getUniq nm i
262 return ('?':nm' ++ rest, i')
263 updateRHS i (x : xs) = do (xs', i') <- updateRHS i xs
264 return (x : xs', i')
265 updateRHS i [] = return ("", i)
268 -- TMP HACK: If there are Nats, we don't want to show as numerals since
269 -- this isn't supported in a pattern, so special case here
270 nshow (PRef _ (UN z)) | z == txt "Z" = "Z"
271 nshow (PApp _ (PRef _ (UN s)) [x]) | s == txt "S" =
272 "S " ++ addBrackets (nshow (getTm x))
273 nshow t = show t
275 -- if there's any {n} replace with {n=n}
276 expandBraces ('{' : xs)
277 = let (brace, (_:rest)) = span (/= '}') xs in
278 if (not ('=' `elem` brace))
279 then ('{' : brace ++ " = " ++ brace ++ "}") ++
280 expandBraces rest
281 else ('{' : brace ++ "}") ++ expandBraces rest
282 expandBraces (x : xs) = x : expandBraces xs
283 expandBraces [] = []
285 updatePat start n tm [] = []
286 updatePat start n tm ('{':rest) =
287 let (space, rest') = span isSpace rest in
288 '{' : space ++ updatePat False n tm rest'
289 updatePat True n tm xs@(c:rest) | length xs > length n
290 = let (before, after@(next:_)) = splitAt (length n) xs in
291 if (before == n && not (isAlphaNum next))
292 then addBrackets tm ++ updatePat False n tm after
293 else c : updatePat (not (isAlphaNum c)) n tm rest
294 updatePat start n tm (c:rest) = c : updatePat (not (isAlpha c)) n tm rest
296 addBrackets tm | ' ' `elem` tm = "(" ++ tm ++ ")"
297 | otherwise = tm
299getUniq nm i
300 = do ist <- getIState
301 let n = nameRoot [] nm ++ "_" ++ show i
302 case lookupTy (sUN n) (tt_ctxt ist) of
303 [] -> return (n, i+1)
304 _ -> getUniq nm (i+1)
306nameRoot acc nm | all isDigit nm = showSep "_" acc
307nameRoot acc nm =
308 case span (/='_') nm of
309 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after
310 _ -> showSep "_" (acc ++ [nm])
312getClause :: Int -- ^ line number that the type is declared on
313 -> Name -- ^ Function name
314 -> FilePath -- ^ Source file name
315 -> Idris String
316getClause l fn fp = do ty <- getInternalApp fp l
317 ist <- get
318 let ap = mkApp ist ty []
319 return (show fn ++ " " ++ ap ++
320 "= ?" ++ show fn ++ "_rhs")
321 where mkApp i (PPi (Exp _ _ False) (MN _ _) ty sc) used
322 = let n = getNameFrom i used ty in
323 show n ++ " " ++ mkApp i sc (n : used)
324 mkApp i (PPi (Exp _ _ False) (UN n) ty sc) used
325 | thead n == '_'
326 = let n = getNameFrom i used ty in
327 show n ++ " " ++ mkApp i sc (n : used)
328 mkApp i (PPi (Exp _ _ False) n _ sc) used
329 = show n ++ " " ++ mkApp i sc (n : used)
330 mkApp i (PPi _ _ _ sc) used = mkApp i sc used
331 mkApp i _ _ = ""
333 getNameFrom i used (PPi _ _ _ _)
334 = uniqueNameFrom (mkSupply [sUN "f", sUN "g"]) used
335 getNameFrom i used (PApp fc f as) = getNameFrom i used f
336 getNameFrom i used (PEq _ _ _) = uniqueNameFrom [sUN "prf"] used
337 getNameFrom i used (PRef fc f)
338 = case getNameHints i f of
339 [] -> uniqueName (sUN "x") used
340 ns -> uniqueNameFrom (mkSupply ns) used
341 getNameFrom i used _ = uniqueName (sUN "x") used
343getProofClause :: Int -- ^ line number that the type is declared
344 -> Name -- ^ Function name
345 -> FilePath -- ^ Source file name
346 -> Idris String
347getProofClause l fn fp
348 = do ty <- getInternalApp fp l
349 return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")
350 where mkApp (PPi _ _ _ sc) = mkApp sc
351 mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn
353-- Purely syntactic - turn a pattern match clause into a with and a new
354-- match clause
356mkWith :: String -> Name -> String
357mkWith str n = let str' = replaceRHS str "with (_)"
358 newpat = " " ++
359 replaceRHS str "| with_pat = ?" ++ show n ++ "_rhs" in
360 str' ++ "\n" ++ newpat
362 where replaceRHS [] str = str
363 replaceRHS ('?':'=': rest) str = str
364 replaceRHS ('=': rest) str
365 | not ('=' `elem` rest) = str
366 replaceRHS (x : rest) str = x : replaceRHS rest str
368-- Replace _ with names in missing clauses
370nameMissing :: [PTerm] -> Idris [PTerm]
371nameMissing ps = do ist <- get
372 newPats <- mapM nm ps
373 let newPats' = mergeAllPats ist (sUN "_") (base (head ps))
374 newPats
375 return (map fst newPats')
376 where
377 base (PApp fc f args) = PApp fc f (map (fmap (const (PRef fc (sUN "_")))) args)
378 base t = t
380 nm ptm = do mptm <- elabNewPat ptm
381 case mptm of
382 Nothing -> return ptm
383 Just ptm' -> return ptm'