@@ -50,8 +50,11 @@ names over '_', patterns over names, etc.
52-- Given a variable to split, and a term application, return a list of
52-- Given a variable to split, and a term application, return a list of
53−-- variable updates
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
54−split :: Name -> PTerm -> Idris [[(Name, PTerm)]]
57+split :: Name -> PTerm -> Idris (Bool, [[(Name, PTerm)]])
56 = do ist <- getIState
59 = do ist <- getIState
57 -- Make sure all the names in the term are accessible
60 -- Make sure all the names in the term are accessible
@@ -77,15 +80,26 @@ split n t'
77 logLvl 4 ("Working from " ++ show t)
80 logLvl 4 ("Working from " ++ show t)
78 logLvl 4 ("Trying " ++ showSep "\n"
81 logLvl 4 ("Trying " ++ showSep "\n"
79 (map (showTmImpls) newPats_in))
82 (map (showTmImpls) newPats_in))
80− newPats <- mapM elabNewPat newPats_in
83+ newPats_in <- mapM elabNewPat newPats_in
84+ case anyValid [] [] newPats_in of
86+ let fails' = mergeAllPats ist n t fails
87+ return (False, (map snd fails'))
81− logLvl 3 ("Original:\n" ++ show t)
89+ logLvl 3 ("Original:\n" ++ show t)
82− logLvl 3 ("Split:\n" ++
90+ logLvl 3 ("Split:\n" ++
83− (showSep "\n" (map show (mapMaybe id newPats))))
91+ (showSep "\n" (map show newPats)))
84− logLvl 3 "----"
92+ logLvl 3 "----"
85− let newPats' = mergeAllPats ist n t (mapMaybe id newPats)
93+ let newPats' = mergeAllPats ist n t newPats
86− logLvl 1 ("Name updates " ++ showSep "\n"
94+ logLvl 1 ("Name updates " ++ showSep "\n"
87− (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))
95+ (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))
88− return (map snd newPats')
96+ return (True, (map snd newPats'))
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
90data MergeState = MS { namemap :: [(Name, Name)],
104data MergeState = MS { namemap :: [(Name, Name)],
91 invented :: [(Name, Name)],
105 invented :: [(Name, Name)],
@@ -208,13 +222,13 @@ tidy ist tm ty = return tm
208-- where tidyVar (PRef _ _) = Placeholder
222-- where tidyVar (PRef _ _) = Placeholder
209-- tidyVar t = t
223-- tidyVar t = t
211−elabNewPat :: PTerm -> Idris (Maybe PTerm)
225+elabNewPat :: PTerm -> Idris (Bool, PTerm)
212elabNewPat t = idrisCatch (do (tm, ty) <- elabVal recinfo ELHS t
226elabNewPat t = idrisCatch (do (tm, ty) <- elabVal recinfo ELHS t
213 i <- getIState
227 i <- getIState
214− return (Just (delab i tm)))
228+ return (True, delab i tm))
215 (\e -> do i <- getIState
229 (\e -> do i <- getIState
216 logLvl 5 $ "Not a valid split:\n" ++ pshow i e
230 logLvl 5 $ "Not a valid split:\n" ++ pshow i e
217− return Nothing)
231+ return (False, t))
219findPats :: IState -> Type -> [PTerm]
233findPats :: IState -> Type -> [PTerm]
220findPats ist t | (P _ n _, _) <- unApply t
234findPats ist t | (P _ n _, _) <- unApply t
@@ -248,26 +262,27 @@ replaceVar ctxt n t pat = pat
248splitOnLine :: Int -- ^ line number
262splitOnLine :: Int -- ^ line number
249 -> Name -- ^ variable
263 -> Name -- ^ variable
250 -> FilePath -- ^ name of file
264 -> FilePath -- ^ name of file
251− -> Idris [[(Name, PTerm)]]
265+ -> Idris (Bool, [[(Name, PTerm)]])
252splitOnLine l n fn = do
266splitOnLine l n fn = do
253−-- let (before, later) = splitAt (l-1) (lines inp)
255 cl <- getInternalApp fn l
267 cl <- getInternalApp fn l
256 logLvl 3 ("Working with " ++ showTmImpls cl)
268 logLvl 3 ("Working with " ++ showTmImpls cl)
257 tms <- split n cl
269 tms <- split n cl
258−-- iputStrLn (showSep "\n" (map show tms))
259− return tms -- "" -- not yet done...
270+ return tms
261−replaceSplits :: String -> [[(Name, PTerm)]] -> Idris [String]
272+replaceSplits :: String -> [[(Name, PTerm)]] -> Bool -> Idris [String]
273+replaceSplits l ups impossible
262−replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
274+ = updateRHSs 1 (map (rep (expandBraces l)) ups)
264 rep str [] = str ++ "\n"
276 rep str [] = str ++ "\n"
265 rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups
277 rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups
267 updateRHSs i [] = return []
279 updateRHSs i [] = return []
280+ updateRHSs i (x : xs)
281+ | impossible = do xs' <- updateRHSs i xs
282+ return (setImpossible False x : xs')
268− updateRHSs i (x : xs) = do (x', i') <- updateRHS (null xs) i x
283+ | otherwise = do (x', i') <- updateRHS (null xs) i x
269− xs' <- updateRHSs i' xs
284+ xs' <- updateRHSs i' xs
270− return (x' : xs')
285+ return (x' : xs')
272 updateRHS last i ('?':'=':xs) = do (xs', i') <- updateRHS last i xs
287 updateRHS last i ('?':'=':xs) = do (xs', i') <- updateRHS last i xs
273 return ("?=" ++ xs', i')
288 return ("?=" ++ xs', i')
@@ -283,6 +298,11 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
283 return (x : xs', i')
298 return (x : xs', i')
284 updateRHS last i [] = return ("", i)
299 updateRHS last i [] = return ("", i)
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 [] = ""
287 -- TMP HACK: If there are Nats, we don't want to show as numerals since
307 -- TMP HACK: If there are Nats, we don't want to show as numerals since
288 -- this isn't supported in a pattern, so special case here
308 -- this isn't supported in a pattern, so special case here
@@ -434,8 +454,8 @@ nameMissing ps = do ist <- get
435 nm ptm = do mptm <- elabNewPat ptm
455 nm ptm = do mptm <- elabNewPat ptm
436 case mptm of
456 case mptm of
437− Nothing -> return ptm
457+ (False, _) -> return ptm
438− Just ptm' -> return ptm'
458+ (True, ptm') -> return ptm'