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