80d1a88 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix implicit spotting in case blocks

80d1a88Edwin Brady12 years ago

src/Idris/AbsSyntaxTree.hs+4−1

@@ -1663,7 +1663,10 @@ namesIn uvars ist tm = nub $ ni [] tm

1663 _ -> if n `elem` (map fst uvars) then [n] else []

1664 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1665 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1666+ ni env (PCase _ c os) = ni env c ++

1667+ -- names in 'os', not counting the names bound in the cases

1666− ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1668+ (nub (concatMap (ni env) (map snd os))

1669+ \\ nub (concatMap (ni env) (map fst os)))

1667 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1670 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1668 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1671 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1669 ni env (PEq _ l r) = ni env l ++ ni env r

1672 ni env (PEq _ l r) = ni env l ++ ni env r

src/Idris/ElabDecls.hs+2

@@ -969,6 +969,8 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

969 def' <- checkDef fc defer

970 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

971 addDeferred def''

972+ mapM_ (\(n, _) -> addIBC (IBCDef n)) def''

973+

972 mapM_ (elabCaseBlock info []) is

974 mapM_ (elabCaseBlock info []) is

973 ctxt <- getContext

975 ctxt <- getContext

974 (cty, _) <- recheckC fc [] t'

976 (cty, _) <- recheckC fc [] t'