@@ -50,8 +50,11 @@ names over '_', patterns over names, etc.
5050-}
5151
5252-- Given a variable to split, and a term application, return a list of
53−-- variable updates
54−split :: Name -> PTerm -> Idris [[(Name, PTerm)]]
53+-- variable updates, paired with a flag to say whether the given update
54+-- typechecks (False = impossible)
55+-- if the flag is 'False' the splits should be output with the 'impossible'
56+-- flag, otherwise they should be output as normal
57+split :: Name -> PTerm -> Idris (Bool, [[(Name, PTerm)]])
5558split n t'
5659 = do ist <- getIState
5760 -- Make sure all the names in the term are accessible
@@ -77,15 +80,26 @@ split n t'
7780 logLvl 4 ("Working from " ++ show t)
7881 logLvl 4 ("Trying " ++ showSep "\n"
7982 (map (showTmImpls) newPats_in))
80− newPats <- mapM elabNewPat newPats_in
81− logLvl 3 ("Original:\n" ++ show t)
82− logLvl 3 ("Split:\n" ++
83− (showSep "\n" (map show (mapMaybe id newPats))))
84− logLvl 3 "----"
85− let newPats' = mergeAllPats ist n t (mapMaybe id newPats)
86− logLvl 1 ("Name updates " ++ showSep "\n"
87− (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))
88− return (map snd newPats')
83+ newPats_in <- mapM elabNewPat newPats_in
84+ case anyValid [] [] newPats_in of
85+ Left fails -> do
86+ let fails' = mergeAllPats ist n t fails
87+ return (False, (map snd fails'))
88+ Right newPats -> do
89+ logLvl 3 ("Original:\n" ++ show t)
90+ logLvl 3 ("Split:\n" ++
91+ (showSep "\n" (map show newPats)))
92+ logLvl 3 "----"
93+ let newPats' = mergeAllPats ist n t newPats
94+ logLvl 1 ("Name updates " ++ showSep "\n"
95+ (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))
96+ return (True, (map snd newPats'))
97+ where
98+ anyValid ok bad [] = if null ok then Left (reverse bad)
99+ else Right (reverse ok)
100+ anyValid ok bad ((tc, p) : ps)
101+ | tc = anyValid (p : ok) bad ps
102+ | otherwise = anyValid ok (p : bad) ps
89103
90104data MergeState = MS { namemap :: [(Name, Name)],
91105 invented :: [(Name, Name)],
@@ -208,13 +222,13 @@ tidy ist tm ty = return tm
208222-- where tidyVar (PRef _ _) = Placeholder
209223-- tidyVar t = t
210224
211−elabNewPat :: PTerm -> Idris (Maybe PTerm)
225+elabNewPat :: PTerm -> Idris (Bool, PTerm)
212226elabNewPat t = idrisCatch (do (tm, ty) <- elabVal recinfo ELHS t
213227 i <- getIState
214− return (Just (delab i tm)))
228+ return (True, delab i tm))
215229 (\e -> do i <- getIState
216230 logLvl 5 $ "Not a valid split:\n" ++ pshow i e
217− return Nothing)
231+ return (False, t))
218232
219233findPats :: IState -> Type -> [PTerm]
220234findPats ist t | (P _ n _, _) <- unApply t
@@ -248,26 +262,27 @@ replaceVar ctxt n t pat = pat
248262splitOnLine :: Int -- ^ line number
249263 -> Name -- ^ variable
250264 -> FilePath -- ^ name of file
251− -> Idris [[(Name, PTerm)]]
265+ -> Idris (Bool, [[(Name, PTerm)]])
252266splitOnLine l n fn = do
253−-- let (before, later) = splitAt (l-1) (lines inp)
254−-- i <- getIState
255267 cl <- getInternalApp fn l
256268 logLvl 3 ("Working with " ++ showTmImpls cl)
257269 tms <- split n cl
258−-- iputStrLn (showSep "\n" (map show tms))
259− return tms -- "" -- not yet done...
270+ return tms
260271
261−replaceSplits :: String -> [[(Name, PTerm)]] -> Idris [String]
262−replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
272+replaceSplits :: String -> [[(Name, PTerm)]] -> Bool -> Idris [String]
273+replaceSplits l ups impossible
274+ = updateRHSs 1 (map (rep (expandBraces l)) ups)
263275 where
264276 rep str [] = str ++ "\n"
265277 rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups
266278
267279 updateRHSs i [] = return []
268− updateRHSs i (x : xs) = do (x', i') <- updateRHS (null xs) i x
269− xs' <- updateRHSs i' xs
270− return (x' : xs')
280+ updateRHSs i (x : xs)
281+ | impossible = do xs' <- updateRHSs i xs
282+ return (setImpossible False x : xs')
283+ | otherwise = do (x', i') <- updateRHS (null xs) i x
284+ xs' <- updateRHSs i' xs
285+ return (x' : xs')
271286
272287 updateRHS last i ('?':'=':xs) = do (xs', i') <- updateRHS last i xs
273288 return ("?=" ++ xs', i')
@@ -283,6 +298,11 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
283298 return (x : xs', i')
284299 updateRHS last i [] = return ("", i)
285300
301+ setImpossible brace ('}':xs) = '}' : setImpossible False xs
302+ setImpossible brace ('{':xs) = '{' : setImpossible True xs
303+ setImpossible False ('=':xs) = "impossible\n"
304+ setImpossible brace (x : xs) = x : setImpossible brace xs
305+ setImpossible brace [] = ""
286306
287307 -- TMP HACK: If there are Nats, we don't want to show as numerals since
288308 -- this isn't supported in a pattern, so special case here
@@ -434,8 +454,8 @@ nameMissing ps = do ist <- get
434454
435455 nm ptm = do mptm <- elabNewPat ptm
436456 case mptm of
437− Nothing -> return ptm
438− Just ptm' -> return ptm'
457+ (False, _) -> return ptm
458+ (True, ptm') -> return ptm'
439459
440460
441461