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