f15aaef · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Postpone implicit addition in case blocks

f15aaefEdwin Brady12 years ago

src/Idris/AbsSyntax.hs+5−3

compare with master

unifiedsplit

@@ -1329,9 +1329,11 @@ addImpl' inpat env infns ist ptm

1329 as' = map (fmap (ai env ds)) as in

1330 mkPApp fc 1 f' as'

1331 ai env ds (PCase fc c os)

1332− = let c' = ai env ds c

1332+ = let c' = ai env ds c in

1333− os' = map (pmap (ai env ds)) os in

1333+ -- leave os alone, because they get lifted into a new pattern match

1334+ -- definition which is passed through addImpl again with more scope

1335+ -- information

1334− PCase fc c' os'

1336+ PCase fc c' os

1335 ai env ds (PLam n ty sc)

1337 ai env ds (PLam n ty sc)

1336 = let ty' = ai env ds ty

1338 = let ty' = ai env ds ty

1337 sc' = ai ((n, Just ty):env) ds sc in

1339 sc' = ai ((n, Just ty):env) ds sc in

src/Idris/ElabTerm.hs+18−4

@@ -265,7 +265,8 @@ elab ist info pattern opts fn tm

265 ty <- goal

266 ctxt <- get_context

267 let (tc, _) = unApply ty

268+ env <- get_env

268− let as' = pruneByType tc ctxt as

269+ let as' = pruneByType (map fst env) tc ctxt as

269-- trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $

270-- trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $

270 tryAll (zip (map (elab' ina) as') (map showHd as'))

271 tryAll (zip (map (elab' ina) as') (map showHd as'))

271 where showHd (PApp _ (PRef _ n) _) = show n

272 where showHd (PApp _ (PRef _ n) _) = show n

@@ -785,8 +786,21 @@ pruneAlt xs = map prune xs

785

786

786-- Rule out alternatives that don't return the same type as the head of the goal

787-- Rule out alternatives that don't return the same type as the head of the goal

787-- (If there are none left as a result, do nothing)

788-- (If there are none left as a result, do nothing)

788−pruneByType :: Term -> Context -> [PTerm] -> [PTerm]

789+pruneByType :: [Name] -> Term -> Context -> [PTerm] -> [PTerm]

790+-- if an alternative has a locally bound name at the head, take it

789−pruneByType (P _ n _) c as

791+pruneByType env t c as

792+ | Just a <- locallyBound as = [a]

793+ where

794+ locallyBound [] = Nothing

795+ locallyBound (t:ts)

796+ | Just n <- getName t,

797+ n `elem` env = Just t

798+ | otherwise = locallyBound ts

799+ getName (PRef _ n) = Just n

800+ getName (PApp _ f _) = getName f

801+ getName _ = Nothing

802+

803+pruneByType env (P _ n _) c as

790-- if the goal type is polymorphic, keep e

804-- if the goal type is polymorphic, keep e

791 | [] <- lookupTy n c = as

805 | [] <- lookupTy n c = as

792 | otherwise

806 | otherwise

@@ -812,7 +826,7 @@ pruneByType (P _ n _) c as

812 _ -> False

826 _ -> False

813 _ -> False

827 _ -> False

814

828

815−pruneByType t _ as = as

829+pruneByType _ t _ as = as

816

830

817findInstances :: IState -> Term -> [Name]

831findInstances :: IState -> Term -> [Name]

818findInstances ist t

832findInstances ist t