git.iko.soy/Idris-dev
on 2b0224a 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.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
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 -- ETyDecl rather then ELHS because there'll be explicit type
61 -- matching
62 (tm, ty, pats) <- elabValBind recinfo ETyDecl True (addImplPat ist t')
63 -- ASSUMPTION: tm is in normal form after elabValBind, so we don't
64 -- need to do anything special to find out what family each argument
65 -- is in
66 logLvl 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)
67-- iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))
68-- iputStrLn (show pats)
69 let t = mergeUserImpl (addImplPat ist t') (delab ist tm)
70 let ctxt = tt_ctxt ist
71 case lookup n pats of
72 Nothing -> ifail $ show n ++ " is not a pattern variable"
73 Just ty ->
74 do let splits = findPats ist ty
75 iLOG ("New patterns " ++ showSep ", "
76 (map showTmImpls splits))
77 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)
78 logLvl 4 ("Working from " ++ show t)
79 logLvl 4 ("Trying " ++ showSep "\n"
80 (map (showTmImpls) newPats_in))
81 newPats <- mapM elabNewPat newPats_in
82 logLvl 3 ("Original:\n" ++ show t)
83 logLvl 3 ("Split:\n" ++
84 (showSep "\n" (map show (mapMaybe id newPats))))
85 logLvl 3 "----"
86 let newPats' = mergeAllPats ist n t (mapMaybe id newPats)
87 iLOG ("Name updates " ++ showSep "\n"
88 (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))
89 return (map snd newPats')
91data MergeState = MS { namemap :: [(Name, Name)],
92 invented :: [(Name, Name)],
93 explicit :: [Name],
94 updates :: [(Name, PTerm)] }
96addUpdate :: Name -> Idris.AbsSyntaxTree.PTerm -> State MergeState ()
97addUpdate n tm = do ms <- get
98 put (ms { updates = ((n, stripNS tm) : updates ms) } )
100inventName :: Idris.AbsSyntaxTree.IState -> Maybe Name -> Name -> State MergeState Name
101inventName ist ty n =
102 do ms <- get
103 let supp = case ty of
104 Nothing -> []
105 Just t -> getNameHints ist t
106 let nsupp = case n of
107 MN i n | not (tnull n) && thead n == '_'
108 -> mkSupply (supp ++ varlist)
109 MN i n -> mkSupply (UN n : supp ++ varlist)
110 UN n | thead n == '_'
111 -> mkSupply (supp ++ varlist)
112 x -> mkSupply (x : supp)
113 let badnames = map snd (namemap ms) ++ map snd (invented ms) ++
114 explicit ms
115 case lookup n (invented ms) of
116 Just n' -> return n'
117 Nothing ->
118 do let n' = uniqueNameFrom nsupp badnames
119 put (ms { invented = (n, n') : invented ms })
120 return n'
122mkSupply :: [Name] -> [Name]
123mkSupply ns = mkSupply' ns (map nextName ns)
124 where mkSupply' xs ns' = xs ++ mkSupply ns'
126varlist :: [Name]
127varlist = map (sUN . (:[])) "xyzwstuv" -- EB's personal preference :)
129stripNS :: Idris.AbsSyntaxTree.PTerm -> Idris.AbsSyntaxTree.PTerm
130stripNS tm = mapPT dens tm where
131 dens (PRef fc n) = PRef fc (nsroot n)
132 dens t = t
134mergeAllPats :: IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
135mergeAllPats ist cv t [] = []
136mergeAllPats ist cv t (p : ps)
137 = let (p', MS _ _ _ u) = runState (mergePat ist t p Nothing)
138 (MS [] [] (filter (/=cv) (patvars t)) [])
139 ps' = mergeAllPats ist cv t ps in
140 ((p', u) : ps')
141 where patvars (PRef _ n) = [n]
142 patvars (PApp _ _ as) = concatMap (patvars . getTm) as
143 patvars (PPatvar _ n) = [n]
144 patvars _ = []
146mergePat :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
147-- If any names are unified, make sure they stay unified. Always prefer
148-- user provided name (first pattern)
149mergePat ist (PPatvar fc n) new t
150 = mergePat ist (PRef fc n) new t
151mergePat ist old (PPatvar fc n) t
152 = mergePat ist old (PRef fc n) t
153mergePat ist orig@(PRef fc n) new@(PRef _ n') t
154 | isDConName n' (tt_ctxt ist) = do addUpdate n new
155 return new
156 | otherwise
157 = do ms <- get
158 case lookup n' (namemap ms) of
159 Just x -> do addUpdate n (PRef fc x)
160 return (PRef fc x)
161 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })
162 return (PRef fc n)
163mergePat ist (PApp _ _ args) (PApp fc f args') t
164 = do newArgs <- zipWithM mergeArg args (zip args' (argTys ist f))
165 return (PApp fc f newArgs)
166 where mergeArg x (y, t)
167 = do tm' <- mergePat ist (getTm x) (getTm y) t
168 case x of
169 (PImp _ _ _ _ _) ->
170 return (y { machine_inf = machine_inf x,
171 getTm = tm' })
172 _ -> return (y { getTm = tm' })
173mergePat ist (PRef fc n) tm ty = do tm <- tidy ist tm ty
174 addUpdate n tm
175 return tm
176mergePat ist x y t = return y
178mergeUserImpl :: PTerm -> PTerm -> PTerm
179mergeUserImpl x y = x
181argTys :: IState -> PTerm -> [Maybe Name]
182argTys ist (PRef fc n)
183 = case lookupTy n (tt_ctxt ist) of
184 [ty] -> map (tyName . snd) (getArgTys ty) ++ repeat Nothing
185 _ -> repeat Nothing
186 where tyName (Bind _ (Pi _ _ _) _) = Just (sUN "->")
187 tyName t | (P _ n _, _) <- unApply t = Just n
188 | otherwise = Nothing
189argTys _ _ = repeat Nothing
191tidy :: IState -> PTerm -> Maybe Name -> State MergeState PTerm
192tidy ist orig@(PRef fc n) ty
193 = do ms <- get
194 case lookup n (namemap ms) of
195 Just x -> return (PRef fc x)
196 Nothing -> case n of
197 (UN _) -> return orig
198 _ -> do n' <- inventName ist ty n
199 return (PRef fc n')
200tidy ist (PApp fc f args) ty
201 = do args' <- zipWithM tidyArg args (argTys ist f)
202 return (PApp fc f args')
203 where tidyArg x ty' = do tm' <- tidy ist (getTm x) ty'
204 return (x { getTm = tm' })
205tidy ist tm ty = return tm
208-- mapPT tidyVar tm
209-- where tidyVar (PRef _ _) = Placeholder
210-- tidyVar t = t
212elabNewPat :: PTerm -> Idris (Maybe PTerm)
213elabNewPat t = idrisCatch (do (tm, ty) <- elabVal recinfo ELHS t
214 i <- getIState
215 return (Just (delab i tm)))
216 (\e -> do i <- getIState
217 logLvl 5 $ "Not a valid split:\n" ++ pshow i e
218 return Nothing)
220findPats :: IState -> Type -> [PTerm]
221findPats ist t | (P _ n _, _) <- unApply t
222 = case lookupCtxt n (idris_datatypes ist) of
223 [ti] -> map genPat (con_names ti)
224 _ -> [Placeholder]
225 where genPat n = case lookupCtxt n (idris_implicits ist) of
226 [args] -> PApp emptyFC (PRef emptyFC n)
227 (map toPlaceholder args)
228 _ -> error $ "Can't happen (genPat) " ++ show n
229 toPlaceholder tm = tm { getTm = Placeholder }
230findPats ist t = [Placeholder]
232replaceVar :: Context -> Name -> PTerm -> PTerm -> PTerm
233replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)
234 where subst :: PTerm -> PTerm
235 subst orig@(PPatvar _ v) | v == n = t
236 | otherwise = Placeholder
237 subst orig@(PRef _ v) | v == n = t
238 | isDConName v ctxt = orig
239 subst (PRef _ _) = Placeholder
240 subst (PApp fc (PRef _ t) pats)
241 | isTConName t ctxt = Placeholder -- infer types
242 subst (PApp fc f pats) = PApp fc f (map substArg pats)
243 subst x = x
245 substArg arg = arg { getTm = subst (getTm arg) }
247replaceVar ctxt n t pat = pat
249splitOnLine :: Int -- ^ line number
250 -> Name -- ^ variable
251 -> FilePath -- ^ name of file
252 -> Idris [[(Name, PTerm)]]
253splitOnLine l n fn = do
254-- let (before, later) = splitAt (l-1) (lines inp)
255-- i <- getIState
256 cl <- getInternalApp fn l
257 logLvl 3 ("Working with " ++ showTmImpls cl)
258 tms <- split n cl
259-- iputStrLn (showSep "\n" (map show tms))
260 return tms -- "" -- not yet done...
262replaceSplits :: String -> [[(Name, PTerm)]] -> Idris [String]
263replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
264 where
265 rep str [] = str ++ "\n"
266 rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups
268 updateRHSs i [] = return []
269 updateRHSs i (x : xs) = do (x', i') <- updateRHS i x
270 xs' <- updateRHSs i' xs
271 return (x' : xs')
273 updateRHS i ('?':'=':xs) = do (xs', i') <- updateRHS i xs
274 return ("?=" ++ xs', i')
275 updateRHS i ('?':xs) = do let (nm, rest) = span (not . isSpace) xs
276 (nm', i') <- getUniq nm i
277 return ('?':nm' ++ rest, i')
278 updateRHS i (x : xs) = do (xs', i') <- updateRHS i xs
279 return (x : xs', i')
280 updateRHS i [] = return ("", i)
283 -- TMP HACK: If there are Nats, we don't want to show as numerals since
284 -- this isn't supported in a pattern, so special case here
285 nshow (PRef _ (UN z)) | z == txt "Z" = "Z"
286 nshow (PApp _ (PRef _ (UN s)) [x]) | s == txt "S" =
287 "(S " ++ addBrackets (nshow (getTm x)) ++ ")"
288 nshow t = show t
290 -- if there's any {n} replace with {n=n}
291 -- but don't replace it in comments
292 expandBraces ('{' : '-' : xs) = '{' : '-' : xs
293 expandBraces ('{' : xs)
294 = let (brace, (_:rest)) = span (/= '}') xs in
295 if (not ('=' `elem` brace))
296 then ('{' : brace ++ " = " ++ brace ++ "}") ++
297 expandBraces rest
298 else ('{' : brace ++ "}") ++ expandBraces rest
299 expandBraces (x : xs) = x : expandBraces xs
300 expandBraces [] = []
302 updatePat start n tm [] = []
303 updatePat start n tm ('{':rest) =
304 let (space, rest') = span isSpace rest in
305 '{' : space ++ updatePat False n tm rest'
306 updatePat start n tm done@('?':rest) = done
307 updatePat True n tm xs@(c:rest) | length xs > length n
308 = let (before, after@(next:_)) = splitAt (length n) xs in
309 if (before == n && not (isAlphaNum next))
310 then addBrackets tm ++ updatePat False n tm after
311 else c : updatePat (not (isAlphaNum c)) n tm rest
312 updatePat start n tm (c:rest) = c : updatePat (not ((isAlphaNum c) || c == '_')) n tm rest
314 addBrackets tm | ' ' `elem` tm
315 , not (isPrefixOf "(" tm)
316 , not (isSuffixOf ")" tm) = "(" ++ tm ++ ")"
317 | otherwise = tm
320getUniq :: (Show t, Num t) => [Char] -> t -> Idris ([Char], t)
321getUniq nm i
322 = do ist <- getIState
323 let n = nameRoot [] nm ++ "_" ++ show i
324 case lookupTy (sUN n) (tt_ctxt ist) of
325 [] -> return (n, i+1)
326 _ -> getUniq nm (i+1)
328nameRoot acc nm | all isDigit nm = showSep "_" acc
329nameRoot acc nm =
330 case span (/='_') nm of
331 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after
332 _ -> showSep "_" (acc ++ [nm])
334getClause :: Int -- ^ line number that the type is declared on
335 -> Name -- ^ Function name
336 -> FilePath -- ^ Source file name
337 -> Idris String
338getClause l fn fp
339 = do i <- getIState
340 case lookupCtxt fn (idris_classes i) of
341 [c] -> return (mkClassBodies i (class_methods c))
342 _ -> do ty <- getInternalApp fp l
343 ist <- get
344 let ap = mkApp ist ty []
345 return (show fn ++ " " ++ ap ++ "= ?"
346 ++ show fn ++ "_rhs")
347 where mkApp :: IState -> PTerm -> [Name] -> String
348 mkApp i (PPi (Exp _ _ False) (MN _ _) _ ty sc) used
349 = let n = getNameFrom i used ty in
350 show n ++ " " ++ mkApp i sc (n : used)
351 mkApp i (PPi (Exp _ _ False) (UN n) _ ty sc) used
352 | thead n == '_'
353 = let n = getNameFrom i used ty in
354 show n ++ " " ++ mkApp i sc (n : used)
355 mkApp i (PPi (Exp _ _ False) n _ _ sc) used
356 = show n ++ " " ++ mkApp i sc (n : used)
357 mkApp i (PPi _ _ _ _ sc) used = mkApp i sc used
358 mkApp i _ _ = ""
360 getNameFrom i used (PPi _ _ _ _ _)
361 = uniqueNameFrom (mkSupply [sUN "f", sUN "g"]) used
362 getNameFrom i used (PApp fc f as) = getNameFrom i used f
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'