git.iko.soy/Idris-dev
on c1e2921 help sign in
Idris-dev/src/Idris/CaseSplit.hs
329 lines 13 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.CaseSplit(splitOnLine, replaceSplits,
4 getClause, getProofClause,
5 mkWith,
6 getUniq, nameRoot) where
8-- splitting a variable in a pattern clause
10import Idris.AbsSyntax
11import Idris.ElabDecls
12import Idris.ElabTerm
13import Idris.Delaborate
14import Idris.Parser
15import Idris.Error
17import Core.TT
18import Core.Typecheck
19import Core.Evaluate
21import Data.Maybe
22import Data.Char
23import Control.Monad
24import Control.Monad.State.Strict
26import Text.Parser.Combinators
27import Text.Parser.Char(anyChar)
28import Text.Trifecta(Result(..), parseString)
29import Text.Trifecta.Delta
30import qualified Data.ByteString.UTF8 as UTF8
32import Debug.Trace
34{-
36Given a pattern clause and a variable 'n', elaborate the clause and find the
37type of 'n'.
39Make new pattern clauses by replacing 'n' with all the possibly constructors
40applied to '_', and replacing all other variables with '_' in order to
41resolve other dependencies.
43Finally, merge the generated patterns with the original, by matching.
44Always take the "more specific" argument when there is a discrepancy, i.e.
45names over '_', patterns over names, etc.
46-}
48-- Given a variable to split, and a term application, return a list of
49-- variable updates
50split :: Name -> PTerm -> Idris [[(Name, PTerm)]]
51split n t'
52 = do ist <- getIState
53 (tm, ty, pats) <- elabValBind toplevel True (addImplPat ist t')
54 logLvl 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)
55-- iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))
56-- iputStrLn (show pats)
57 let t = mergeUserImpl (addImplPat ist t') (delab ist tm)
58 let ctxt = tt_ctxt ist
59 case lookup n pats of
60 Nothing -> fail $ show n ++ " is not a pattern variable"
61 Just ty ->
62 do let splits = findPats ist ty
63 iLOG ("New patterns " ++ showSep ", "
64 (map (showImp Nothing True False) splits))
65 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)
66 logLvl 4 ("Working from " ++ show t)
67 logLvl 4 ("Trying " ++ showSep "\n"
68 (map (showImp Nothing True False) newPats_in))
69 newPats <- mapM elabNewPat newPats_in
70 logLvl 3 ("Original:\n" ++ show t)
71 logLvl 3 ("Split:\n" ++
72 (showSep "\n" (map show (mapMaybe id newPats))))
73 logLvl 3 "----"
74 let newPats' = mergeAllPats ctxt t (mapMaybe id newPats)
75 iLOG ("Name updates " ++ showSep "\n"
76 (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))
77 return (map snd newPats')
79data MergeState = MS { namemap :: [(Name, Name)],
80 invented :: [(Name, Name)],
81 explicit :: [Name],
82 updates :: [(Name, PTerm)] }
84addUpdate n tm = do ms <- get
85 put (ms { updates = ((n, stripNS tm) : updates ms) } )
87inventName n =
88 do ms <- get
89 let badnames = map snd (namemap ms) ++ map snd (invented ms) ++
90 explicit ms
91 case lookup n (invented ms) of
92 Just n' -> return n'
93 Nothing ->
94 do let n' = case n of
95 MN i ('_':_) ->
96 uniqueName (UN "var") badnames
97 MN i n -> uniqueName (UN n) badnames
98 x -> x
99 put (ms { invented = (n, n') : invented ms })
100 return n'
102stripNS tm = mapPT dens tm where
103 dens (PRef fc n) = PRef fc (nsroot n)
104 dens t = t
106mergeAllPats :: Context -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
107mergeAllPats ctxt t [] = []
108mergeAllPats ctxt t (p : ps)
109 = let (p', MS _ _ _ u) = runState (mergePat ctxt t p)
110 (MS [] [] (patvars t) [])
111 ps' = mergeAllPats ctxt t ps in
112 ((p, u) : ps')
113 where patvars (PRef _ n) = [n]
114 patvars (PApp _ _ as) = concatMap (patvars . getTm) as
115 patvars (PPatvar _ n) = [n]
116 patvars _ = []
118mergePat :: Context -> PTerm -> PTerm -> State MergeState PTerm
119-- If any names are unified, make sure they stay unified. Always prefer
120-- user provided name (first pattern)
121mergePat ctxt (PPatvar fc n) new
122 = mergePat ctxt (PRef fc n) new
123mergePat ctxt old (PPatvar fc n)
124 = mergePat ctxt old (PRef fc n)
125mergePat ctxt orig@(PRef fc n) new@(PRef _ n')
126 | isDConName n' ctxt = do addUpdate n new;
127 return new
128 | otherwise
129 = do ms <- get
130 case lookup n' (namemap ms) of
131 Just x -> do addUpdate n (PRef fc x)
132 return (PRef fc x)
133 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })
134 return (PRef fc n)
135mergePat ctxt (PApp _ _ args) (PApp fc f args')
136 = do newArgs <- zipWithM mergeArg args args'
137 return (PApp fc f newArgs)
138 where mergeArg x y = do tm' <- mergePat ctxt (getTm x) (getTm y)
139 case x of
140 (PImp _ _ _ _ _ _) ->
141 return (y { machine_inf = machine_inf x,
142 getTm = tm' })
143 _ -> return (y { getTm = tm' })
144mergePat ctxt (PRef fc n) t = do tm <- tidy t
145 addUpdate n tm
146 return tm
147mergePat ctxt x y = return y
149mergeUserImpl :: PTerm -> PTerm -> PTerm
150mergeUserImpl x y = x
152tidy orig@(PRef fc n)
153 = do ms <- get
154 case lookup n (namemap ms) of
155 Just x -> return (PRef fc x)
156 Nothing -> case n of
157 (UN _) -> return orig
158 _ -> do n' <- inventName n
159 return (PRef fc n')
160tidy (PApp fc f args)
161 = do args' <- mapM tidyArg args
162 return (PApp fc f args')
163 where tidyArg x = do tm' <- tidy (getTm x)
164 return (x { getTm = tm' })
165tidy tm = return tm
168-- mapPT tidyVar tm
169-- where tidyVar (PRef _ _) = Placeholder
170-- tidyVar t = t
172elabNewPat :: PTerm -> Idris (Maybe PTerm)
173elabNewPat t = idrisCatch (do (tm, ty) <- elabVal toplevel True t
174 i <- getIState
175 return (Just (delab i tm)))
176 (\e -> do i <- getIState
177 logLvl 5 $ "Not a valid split:\n" ++ pshow i e
178 return Nothing)
180findPats :: IState -> Type -> [PTerm]
181findPats ist t | (P _ n _, _) <- unApply t
182 = case lookupCtxt n (idris_datatypes ist) of
183 [ti] -> map genPat (con_names ti)
184 _ -> [Placeholder]
185 where genPat n = case lookupCtxt n (idris_implicits ist) of
186 [args] -> PApp emptyFC (PRef emptyFC n)
187 (map toPlaceholder args)
188 _ -> error $ "Can't happen (genPat) " ++ show n
189 toPlaceholder tm = tm { getTm = Placeholder }
190findPats ist t = [Placeholder]
192replaceVar :: Context -> Name -> PTerm -> PTerm -> PTerm
193replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)
194 where subst :: PTerm -> PTerm
195 subst orig@(PPatvar _ v) | v == n = t
196 | otherwise = Placeholder
197 subst orig@(PRef _ v) | v == n = t
198 | isDConName v ctxt = orig
199 subst (PRef _ _) = Placeholder
200 subst (PApp fc (PRef _ t) pats)
201 | isTConName t ctxt = Placeholder -- infer types
202 subst (PApp fc f pats) = PApp fc f (map substArg pats)
203 subst (PEq fc l r) = PEq fc (subst l) (subst r)
204 subst x = x
206 substArg arg = arg { getTm = subst (getTm arg) }
208replaceVar ctxt n t pat = pat
210splitOnLine :: Int -- ^ line number
211 -> Name -- ^ variable
212 -> FilePath -- ^ name of file
213 -> Idris [[(Name, PTerm)]]
214splitOnLine l n fn = do
215-- let (before, later) = splitAt (l-1) (lines inp)
216-- i <- getIState
217 cl <- getInternalApp fn l
218 logLvl 3 ("Working with " ++ showImp Nothing True False cl)
219 tms <- split n cl
220-- iputStrLn (showSep "\n" (map show tms))
221 return tms -- "" -- not yet done...
223replaceSplits :: String -> [[(Name, PTerm)]] -> Idris [String]
224replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
225 where
226 rep str [] = str ++ "\n"
227 rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow False tm) str) ups
229 updateRHSs i [] = return []
230 updateRHSs i (x : xs) = do (x', i') <- updateRHS i x
231 xs' <- updateRHSs i' xs
232 return (x' : xs')
234 updateRHS i ('?':'=':xs) = do (xs', i') <- updateRHS i xs
235 return ("?=" ++ xs', i')
236 updateRHS i ('?':xs) = do let (nm, rest) = span (not . isSpace) xs
237 (nm', i') <- getUniq nm i
238 return ('?':nm' ++ rest, i')
239 updateRHS i (x : xs) = do (xs', i') <- updateRHS i xs
240 return (x : xs', i')
241 updateRHS i [] = return ("", i)
244 -- TMP HACK: If there are Nats, we don't want to show as numerals since
245 -- this isn't supported in a pattern, so special case here
246 nshow brack (PRef _ (UN "Z")) = "Z"
247 nshow brack (PApp _ (PRef _ (UN "S")) [x]) =
248 if brack then "(S " else "S " ++ nshow True (getTm x) ++
249 if brack then ")" else ""
250 nshow _ t = show t
252 -- if there's any {n} replace with {n=n}
253 expandBraces ('{' : xs)
254 = let (brace, (_:rest)) = span (/= '}') xs in
255 if (not ('=' `elem` brace))
256 then ('{' : brace ++ " = " ++ brace ++ "}") ++
257 expandBraces rest
258 else ('{' : brace ++ "}") ++ expandBraces rest
259 expandBraces (x : xs) = x : expandBraces xs
260 expandBraces [] = []
262 updatePat start n tm [] = []
263 updatePat start n tm ('{':rest) =
264 let (space, rest') = span isSpace rest in
265 '{' : space ++ updatePat False n tm rest'
266 updatePat True n tm xs@(c:rest) | length xs > length n
267 = let (before, after@(next:_)) = splitAt (length n) xs in
268 if (before == n && not (isAlpha next))
269 then addBrackets tm ++ updatePat False n tm after
270 else c : updatePat (not (isAlpha c)) n tm rest
271 updatePat start n tm (c:rest) = c : updatePat (not (isAlpha c)) n tm rest
273 addBrackets tm | ' ' `elem` tm = "(" ++ tm ++ ")"
274 | otherwise = tm
276getUniq nm i
277 = do ist <- getIState
278 let n = nameRoot [] nm ++ "_" ++ show i
279 case lookupTy (UN n) (tt_ctxt ist) of
280 [] -> return (n, i+1)
281 _ -> getUniq nm (i+1)
283nameRoot acc nm | all isDigit nm = showSep "_" acc
284nameRoot acc nm =
285 case span (/='_') nm of
286 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after
287 _ -> showSep "_" (acc ++ [nm])
289getClause :: Int -- ^ line number that the type is declared on
290 -> Name -- ^ Function name
291 -> FilePath -- ^ Source file name
292 -> Idris String
293getClause l fn fp = do ty <- getInternalApp fp l
294 let ap = mkApp ty [1..]
295 return (show fn ++ " " ++ ap ++
296 "= ?" ++ show fn ++ "_rhs")
297 where mkApp (PPi (Exp _ _ _ False) (MN _ _) _ sc) (n : ns)
298 = "x" ++ show n ++ " " ++ mkApp sc ns
299 mkApp (PPi (Exp _ _ _ False) n _ sc) ns
300 = show n ++ " " ++ mkApp sc ns
301 mkApp (PPi _ _ _ sc) ns = mkApp sc ns
302 mkApp _ _ = ""
304getProofClause :: Int -- ^ line number that the type is declared
305 -> Name -- ^ Function name
306 -> FilePath -- ^ Source file name
307 -> Idris String
308getProofClause l fn fp
309 = do ty <- getInternalApp fp l
310 return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")
311 where mkApp (PPi _ _ _ sc) = mkApp sc
312 mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn
314-- Purely syntactic - turn a pattern match clause into a with and a new
315-- match clause
317mkWith :: String -> Name -> String
318mkWith str n = let str' = replaceRHS str "with (_)"
319 newpat = " " ++
320 replaceRHS str "| with_pat = ?" ++ show n ++ "_rhs" in
321 str' ++ "\n" ++ newpat
323 where replaceRHS [] str = str
324 replaceRHS ('?':'=': rest) str = str
325 replaceRHS ('=': rest) str
326 | not ('=' `elem` rest) = str
327 replaceRHS (x : rest) str = x : replaceRHS rest str