git.iko.soy/Idris-dev
on cb005bc help sign in
Idris-dev/src/Idris/CaseSplit.hs
431 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 -- 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 -> fail $ 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 (PEq fc _ _ l r) = Placeholder -- PEq fc (subst l) (subst r)
244 subst x = x
246 substArg arg = arg { getTm = subst (getTm arg) }
248replaceVar ctxt n t pat = pat
250splitOnLine :: Int -- ^ line number
251 -> Name -- ^ variable
252 -> FilePath -- ^ name of file
253 -> Idris [[(Name, PTerm)]]
254splitOnLine l n fn = do
255-- let (before, later) = splitAt (l-1) (lines inp)
256-- i <- getIState
257 cl <- getInternalApp fn l
258 logLvl 3 ("Working with " ++ showTmImpls cl)
259 tms <- split n cl
260-- iputStrLn (showSep "\n" (map show tms))
261 return tms -- "" -- not yet done...
263replaceSplits :: String -> [[(Name, PTerm)]] -> Idris [String]
264replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
265 where
266 rep str [] = str ++ "\n"
267 rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups
269 updateRHSs i [] = return []
270 updateRHSs i (x : xs) = do (x', i') <- updateRHS i x
271 xs' <- updateRHSs i' xs
272 return (x' : xs')
274 updateRHS i ('?':'=':xs) = do (xs', i') <- updateRHS i xs
275 return ("?=" ++ xs', i')
276 updateRHS i ('?':xs) = do let (nm, rest) = span (not . isSpace) xs
277 (nm', i') <- getUniq nm i
278 return ('?':nm' ++ rest, i')
279 updateRHS i (x : xs) = do (xs', i') <- updateRHS i xs
280 return (x : xs', i')
281 updateRHS i [] = return ("", i)
284 -- TMP HACK: If there are Nats, we don't want to show as numerals since
285 -- this isn't supported in a pattern, so special case here
286 nshow (PRef _ (UN z)) | z == txt "Z" = "Z"
287 nshow (PApp _ (PRef _ (UN s)) [x]) | s == txt "S" =
288 "(S " ++ addBrackets (nshow (getTm x)) ++ ")"
289 nshow t = show t
291 -- if there's any {n} replace with {n=n}
292 -- but don't replace it in comments
293 expandBraces ('{' : '-' : xs) = '{' : '-' : xs
294 expandBraces ('{' : xs)
295 = let (brace, (_:rest)) = span (/= '}') xs in
296 if (not ('=' `elem` brace))
297 then ('{' : brace ++ " = " ++ brace ++ "}") ++
298 expandBraces rest
299 else ('{' : brace ++ "}") ++ expandBraces rest
300 expandBraces (x : xs) = x : expandBraces xs
301 expandBraces [] = []
303 updatePat start n tm [] = []
304 updatePat start n tm ('{':rest) =
305 let (space, rest') = span isSpace rest in
306 '{' : space ++ updatePat False n tm rest'
307 updatePat start n tm done@('?':rest) = done
308 updatePat True n tm xs@(c:rest) | length xs > length n
309 = let (before, after@(next:_)) = splitAt (length n) xs in
310 if (before == n && not (isAlphaNum next))
311 then addBrackets tm ++ updatePat False n tm after
312 else c : updatePat (not (isAlphaNum c)) n tm rest
313 updatePat start n tm (c:rest) = c : updatePat (not ((isAlphaNum c) || c == '_')) n tm rest
315 addBrackets tm | ' ' `elem` tm
316 , not (isPrefixOf "(" tm)
317 , not (isSuffixOf ")" tm) = "(" ++ tm ++ ")"
318 | otherwise = tm
321getUniq :: (Show t, Num t) => [Char] -> t -> Idris ([Char], t)
322getUniq nm i
323 = do ist <- getIState
324 let n = nameRoot [] nm ++ "_" ++ show i
325 case lookupTy (sUN n) (tt_ctxt ist) of
326 [] -> return (n, i+1)
327 _ -> getUniq nm (i+1)
329nameRoot acc nm | all isDigit nm = showSep "_" acc
330nameRoot acc nm =
331 case span (/='_') nm of
332 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after
333 _ -> showSep "_" (acc ++ [nm])
335getClause :: Int -- ^ line number that the type is declared on
336 -> Name -- ^ Function name
337 -> FilePath -- ^ Source file name
338 -> Idris String
339getClause l fn fp
340 = do i <- getIState
341 case lookupCtxt fn (idris_classes i) of
342 [c] -> return (mkClassBodies i (class_methods c))
343 _ -> do ty <- getInternalApp fp l
344 ist <- get
345 let ap = mkApp ist ty []
346 return (show fn ++ " " ++ ap ++ "= ?"
347 ++ show fn ++ "_rhs")
348 where mkApp :: IState -> PTerm -> [Name] -> String
349 mkApp i (PPi (Exp _ _ False) (MN _ _) ty sc) used
350 = let n = getNameFrom i used ty in
351 show n ++ " " ++ mkApp i sc (n : used)
352 mkApp i (PPi (Exp _ _ False) (UN n) ty sc) used
353 | thead n == '_'
354 = let n = getNameFrom i used ty in
355 show n ++ " " ++ mkApp i sc (n : used)
356 mkApp i (PPi (Exp _ _ False) n _ sc) used
357 = show n ++ " " ++ mkApp i sc (n : used)
358 mkApp i (PPi _ _ _ sc) used = mkApp i sc used
359 mkApp i _ _ = ""
361 getNameFrom i used (PPi _ _ _ _)
362 = uniqueNameFrom (mkSupply [sUN "f", sUN "g"]) used
363 getNameFrom i used (PApp fc f as) = getNameFrom i used f
364 getNameFrom i used (PEq _ _ _ _ _) = uniqueNameFrom (mkSupply [sUN "prf"]) used
365 getNameFrom i used (PRef fc f)
366 = case getNameHints i f of
367 [] -> uniqueName (sUN "x") used
368 ns -> uniqueNameFrom (mkSupply ns) used
369 getNameFrom i used _ = uniqueName (sUN "x") used
371 -- write method declarations, indent with 4 spaces
372 mkClassBodies :: IState -> [(Name, (FnOpts, PTerm))] -> String
373 mkClassBodies i ns
374 = showSep "\n"
375 (zipWith (\(n, (_, ty)) m -> " " ++
376 def (show (nsroot n)) ++ " "
377 ++ mkApp i ty []
378 ++ "= ?"
379 ++ show fn ++ "_rhs_" ++ show m) ns [1..])
381 def n@(x:xs) | not (isAlphaNum x) = "(" ++ n ++ ")"
382 def n = n
384getProofClause :: Int -- ^ line number that the type is declared
385 -> Name -- ^ Function name
386 -> FilePath -- ^ Source file name
387 -> Idris String
388getProofClause l fn fp
389 = do ty <- getInternalApp fp l
390 return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")
391 where mkApp (PPi _ _ _ sc) = mkApp sc
392 mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn
394-- Purely syntactic - turn a pattern match clause into a with and a new
395-- match clause
397mkWith :: String -> Name -> String
398mkWith str n = let str' = replaceRHS str "with (_)"
399 in str' ++ "\n" ++ newpat str
401 where replaceRHS [] str = str
402 replaceRHS ('?':'=': rest) str = str
403 replaceRHS ('=': rest) str
404 | not ('=' `elem` rest) = str
405 replaceRHS (x : rest) str = x : replaceRHS rest str
407 newpat ('>':patstr) = '>':newpat patstr
408 newpat patstr =
409 " " ++
410 replaceRHS patstr "| with_pat = ?" ++ show n ++ "_rhs"
412-- Replace _ with names in missing clauses
414nameMissing :: [PTerm] -> Idris [PTerm]
415nameMissing ps = do ist <- get
416 newPats <- mapM nm ps
417 let newPats' = mergeAllPats ist (sUN "_") (base (head ps))
418 newPats
419 return (map fst newPats')
420 where
421 base (PApp fc f args) = PApp fc f (map (fmap (const (PRef fc (sUN "_")))) args)
422 base t = t
424 nm ptm = do mptm <- elabNewPat ptm
425 case mptm of
426 Nothing -> return ptm
427 Just ptm' -> return ptm'