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