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