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