git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/src/Idris/CaseSplit.hs
429 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.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 :: Name -> Idris.AbsSyntaxTree.PTerm -> State MergeState ()
95addUpdate n tm = do ms <- get
96 put (ms { updates = ((n, stripNS tm) : updates ms) } )
98inventName :: Idris.AbsSyntaxTree.IState -> Maybe Name -> Name -> State MergeState Name
99inventName ist ty n =
100 do ms <- get
101 let supp = case ty of
102 Nothing -> []
103 Just t -> getNameHints ist t
104 let nsupp = case n of
105 MN i n | not (tnull n) && thead n == '_'
106 -> mkSupply (supp ++ varlist)
107 MN i n -> mkSupply (UN n : supp ++ varlist)
108 UN n | thead n == '_'
109 -> mkSupply (supp ++ varlist)
110 x -> mkSupply (x : supp)
111 let badnames = map snd (namemap ms) ++ map snd (invented ms) ++
112 explicit ms
113 case lookup n (invented ms) of
114 Just n' -> return n'
115 Nothing ->
116 do let n' = uniqueNameFrom nsupp badnames
117 put (ms { invented = (n, n') : invented ms })
118 return n'
120mkSupply :: [Name] -> [Name]
121mkSupply ns = mkSupply' ns (map nextName ns)
122 where mkSupply' xs ns' = xs ++ mkSupply ns'
124varlist :: [Name]
125varlist = map (sUN . (:[])) "xyzwstuv" -- EB's personal preference :)
127stripNS :: Idris.AbsSyntaxTree.PTerm -> Idris.AbsSyntaxTree.PTerm
128stripNS tm = mapPT dens tm where
129 dens (PRef fc n) = PRef fc (nsroot n)
130 dens t = t
132mergeAllPats :: IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
133mergeAllPats ist cv t [] = []
134mergeAllPats ist cv t (p : ps)
135 = let (p', MS _ _ _ u) = runState (mergePat ist t p Nothing)
136 (MS [] [] (filter (/=cv) (patvars t)) [])
137 ps' = mergeAllPats ist cv t ps in
138 ((p', u) : ps')
139 where patvars (PRef _ n) = [n]
140 patvars (PApp _ _ as) = concatMap (patvars . getTm) as
141 patvars (PPatvar _ n) = [n]
142 patvars _ = []
144mergePat :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
145-- If any names are unified, make sure they stay unified. Always prefer
146-- user provided name (first pattern)
147mergePat ist (PPatvar fc n) new t
148 = mergePat ist (PRef fc n) new t
149mergePat ist old (PPatvar fc n) t
150 = mergePat ist old (PRef fc n) t
151mergePat ist orig@(PRef fc n) new@(PRef _ n') t
152 | isDConName n' (tt_ctxt ist) = do addUpdate n new
153 return new
154 | otherwise
155 = do ms <- get
156 case lookup n' (namemap ms) of
157 Just x -> do addUpdate n (PRef fc x)
158 return (PRef fc x)
159 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })
160 return (PRef fc n)
161mergePat ist (PApp _ _ args) (PApp fc f args') t
162 = do newArgs <- zipWithM mergeArg args (zip args' (argTys ist f))
163 return (PApp fc f newArgs)
164 where mergeArg x (y, t)
165 = do tm' <- mergePat ist (getTm x) (getTm y) t
166 case x of
167 (PImp _ _ _ _ _) ->
168 return (y { machine_inf = machine_inf x,
169 getTm = tm' })
170 _ -> return (y { getTm = tm' })
171mergePat ist (PRef fc n) tm ty = do tm <- tidy ist tm ty
172 addUpdate n tm
173 return tm
174mergePat ist x y t = return y
176mergeUserImpl :: PTerm -> PTerm -> PTerm
177mergeUserImpl x y = x
179argTys :: IState -> PTerm -> [Maybe Name]
180argTys ist (PRef fc n)
181 = case lookupTy n (tt_ctxt ist) of
182 [ty] -> map (tyName . snd) (getArgTys ty) ++ repeat Nothing
183 _ -> repeat Nothing
184 where tyName (Bind _ (Pi _ _) _) = Just (sUN "->")
185 tyName t | (P _ n _, _) <- unApply t = Just n
186 | otherwise = Nothing
187argTys _ _ = repeat Nothing
189tidy :: IState -> PTerm -> Maybe Name -> State MergeState PTerm
190tidy ist orig@(PRef fc n) ty
191 = do ms <- get
192 case lookup n (namemap ms) of
193 Just x -> return (PRef fc x)
194 Nothing -> case n of
195 (UN _) -> return orig
196 _ -> do n' <- inventName ist ty n
197 return (PRef fc n')
198tidy ist (PApp fc f args) ty
199 = do args' <- zipWithM tidyArg args (argTys ist f)
200 return (PApp fc f args')
201 where tidyArg x ty' = do tm' <- tidy ist (getTm x) ty'
202 return (x { getTm = tm' })
203tidy ist tm ty = return tm
206-- mapPT tidyVar tm
207-- where tidyVar (PRef _ _) = Placeholder
208-- tidyVar t = t
210elabNewPat :: PTerm -> Idris (Maybe PTerm)
211elabNewPat t = idrisCatch (do (tm, ty) <- elabVal recinfo ELHS t
212 i <- getIState
213 return (Just (delab i tm)))
214 (\e -> do i <- getIState
215 logLvl 5 $ "Not a valid split:\n" ++ pshow i e
216 return Nothing)
218findPats :: IState -> Type -> [PTerm]
219findPats ist t | (P _ n _, _) <- unApply t
220 = case lookupCtxt n (idris_datatypes ist) of
221 [ti] -> map genPat (con_names ti)
222 _ -> [Placeholder]
223 where genPat n = case lookupCtxt n (idris_implicits ist) of
224 [args] -> PApp emptyFC (PRef emptyFC n)
225 (map toPlaceholder args)
226 _ -> error $ "Can't happen (genPat) " ++ show n
227 toPlaceholder tm = tm { getTm = Placeholder }
228findPats ist t = [Placeholder]
230replaceVar :: Context -> Name -> PTerm -> PTerm -> PTerm
231replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)
232 where subst :: PTerm -> PTerm
233 subst orig@(PPatvar _ v) | v == n = t
234 | otherwise = Placeholder
235 subst orig@(PRef _ v) | v == n = t
236 | isDConName v ctxt = orig
237 subst (PRef _ _) = Placeholder
238 subst (PApp fc (PRef _ t) pats)
239 | isTConName t ctxt = Placeholder -- infer types
240 subst (PApp fc f pats) = PApp fc f (map substArg pats)
241 subst (PEq fc _ _ l r) = Placeholder -- PEq fc (subst l) (subst r)
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 (PEq _ _ _ _ _) = uniqueNameFrom [sUN "prf"] used
363 getNameFrom i used (PRef fc f)
364 = case getNameHints i f of
365 [] -> uniqueName (sUN "x") used
366 ns -> uniqueNameFrom (mkSupply ns) used
367 getNameFrom i used _ = uniqueName (sUN "x") used
369 -- write method declarations, indent with 4 spaces
370 mkClassBodies :: IState -> [(Name, (FnOpts, PTerm))] -> String
371 mkClassBodies i ns
372 = showSep "\n"
373 (zipWith (\(n, (_, ty)) m -> " " ++
374 def (show (nsroot n)) ++ " "
375 ++ mkApp i ty []
376 ++ "= ?"
377 ++ show fn ++ "_rhs_" ++ show m) ns [1..])
379 def n@(x:xs) | not (isAlphaNum x) = "(" ++ n ++ ")"
380 def n = n
382getProofClause :: Int -- ^ line number that the type is declared
383 -> Name -- ^ Function name
384 -> FilePath -- ^ Source file name
385 -> Idris String
386getProofClause l fn fp
387 = do ty <- getInternalApp fp l
388 return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")
389 where mkApp (PPi _ _ _ sc) = mkApp sc
390 mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn
392-- Purely syntactic - turn a pattern match clause into a with and a new
393-- match clause
395mkWith :: String -> Name -> String
396mkWith str n = let str' = replaceRHS str "with (_)"
397 in str' ++ "\n" ++ newpat str
399 where replaceRHS [] str = str
400 replaceRHS ('?':'=': rest) str = str
401 replaceRHS ('=': rest) str
402 | not ('=' `elem` rest) = str
403 replaceRHS (x : rest) str = x : replaceRHS rest str
405 newpat ('>':patstr) = '>':newpat patstr
406 newpat patstr =
407 " " ++
408 replaceRHS patstr "| with_pat = ?" ++ show n ++ "_rhs"
410-- Replace _ with names in missing clauses
412nameMissing :: [PTerm] -> Idris [PTerm]
413nameMissing ps = do ist <- get
414 newPats <- mapM nm ps
415 let newPats' = mergeAllPats ist (sUN "_") (base (head ps))
416 newPats
417 return (map fst newPats')
418 where
419 base (PApp fc f args) = PApp fc f (map (fmap (const (PRef fc (sUN "_")))) args)
420 base t = t
422 nm ptm = do mptm <- elabNewPat ptm
423 case mptm of
424 Nothing -> return ptm
425 Just ptm' -> return ptm'