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