8697358 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+4−1

compare with master

unifiedsplit

@@ -1978,8 +1978,11 @@ shadow :: Name -> Name -> PTerm -> PTerm

1978shadow n n' t = sm t where

1979 sm (PRef fc x) | n == x = PRef fc n'

1980 sm (PLam fc x t sc) | n /= x = PLam fc x (sm t) (sm sc)

1981+ | otherwise = PLam fc x (sm t) sc

1981− sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)

1982+ sm (PPi p x t sc) | n /= x = PPi p x (sm t) (sm sc)

1983+ | otherwise = PPi p x (sm t) sc

1982 sm (PLet fc x t v sc) | n /= x = PLet fc x (sm t) (sm v) (sm sc)

1984 sm (PLet fc x t v sc) | n /= x = PLet fc x (sm t) (sm v) (sm sc)

1985+ | otherwise = PLet fc x (sm t) (sm v) sc

1983 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1986 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1984 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)

1987 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)

1985 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

1988 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

src/Idris/Core/Evaluate.hs+3−3

@@ -286,17 +286,17 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

286 -- block reduction immediately under codata (and not forced)

287 ev ntimes stk top env

288 (App (App (App d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)

289− | dly == txt "Delay" && lco == txt "LazyCodata" && not simpl

289+ | dly == txt "Delay" && lco == txt "LazyCodata" -- && not simpl

290 = do let (f, _) = unApply arg

291 let ntimes' = case f of

292 P _ fn _ -> (fn, 0) : ntimes

293 _ -> ntimes

294− when spec $ setBlock True

294+ when (spec || simpl) $ setBlock True

295 d' <- ev ntimes' stk False env d

296 l' <- ev ntimes' stk False env l

297 t' <- ev ntimes' stk False env t

298 arg' <- ev ntimes' stk False env arg

299− when spec $ setBlock False

299+ when (spec || simpl) $ setBlock False

300 evApply ntimes' stk top env [l',t',arg'] d'

301 -- Treat "assert_total" specially, as long as it's defined!

302 ev ntimes stk top env (App (App (P _ n@(UN at) _) _) arg)

src/Idris/Elab/Clause.hs+3−3

@@ -648,9 +648,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

648 -- Now build the RHS, using the type of the LHS as the goal.

649 i <- getIState -- new implicits from where block

650 logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))

651− let rhs = addImplBoundInf i (map fst newargs) (defs \\ decls)

651+ let rhs = addImplBoundInf i (map fst newargs_all) (defs \\ decls)

652 (expandParams decorate newargs defs (defs \\ decls) rhs_in)

653− logLvl 2 $ "RHS: " ++ showTmImpls rhs

653+ logLvl 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs

654 ctxt <- getContext -- new context with where block added

655 logLvl 5 "STARTING CHECK"

656 ((rhs', defer, is, probs), _) <-

@@ -673,7 +673,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

673 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

674

675 logLvl 5 "DONE CHECK"

676− logLvl 2 $ "---> " ++ show rhs'

676+ logLvl 4 $ "---> " ++ show rhs'

677 when (not (null defer)) $ iLOG $ "DEFERRED " ++

678 show (map (\ (n, (_,_,t)) -> (n, t)) defer)

679 def' <- checkDef fc defer

src/Idris/ElabTerm.hs+9−1

@@ -893,9 +893,17 @@ elab ist info emode opts fn tm

893 -- Drop the unique arguments used in the term already

894 -- and in the scrutinee (since it's

895 -- not valid to use them again anyway)

896+ --

897+ -- Also drop unique arguments which don't appear explicitly

898+ -- in either case branch so they don't count as used

899+ -- unnecessarily (can only do this for unique things, since we

900+ -- assume they don't appear implicitly in types)

896 ptm <- get_term

901 ptm <- get_term

902+ let inOpts = (filter (/= scvn) (map fst args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)

903+

897 let argsDropped = filter (isUnique envU)

904 let argsDropped = filter (isUnique envU)

898− (nub $ allNamesIn scr ++ inApp ptm)

905+ (nub $ allNamesIn scr ++ inApp ptm ++

906+ inOpts)

899

907

900 let args' = filter (\(n, _) -> n `notElem` argsDropped) args

908 let args' = filter (\(n, _) -> n `notElem` argsDropped) args

901

909