@@ -8,7 +8,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
88 Context, initContext, ctxtAlist, uconstraints, next_tvar,
99 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,
1010 addDatatype, addCasedef, simplifyCasedef, addOperator,
11− lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
11+ lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
1212 lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
1313 mapDefCtxt,
1414 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, isTConName, isConName, isFnName,
@@ -92,7 +92,7 @@ normaliseTrace tr ctxt env t
9292
9393-- Return a specialised name, and an updated list of reductions available,
9494-- so that the caller can tell how much specialisation was achieved.
95−specialise :: Context -> Env -> [(Name, Int)] -> TT Name ->
95+specialise :: Context -> Env -> [(Name, Int)] -> TT Name ->
9696 (TT Name, [(Name, Int)])
9797specialise ctxt env limits t
9898 = let (tm, st) =
@@ -176,7 +176,7 @@ usable False n ns
176176
177177
178178fnCount :: Int -> Name -> Eval ()
179−fnCount inc n
179+fnCount inc n
180180 = do ES ls num b <- get
181181 case lookup n ls of
182182 Just i -> do put $ ES ((n, (i - inc)) :
@@ -255,7 +255,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
255255 ev ntimes stk top env (V i)
256256 | i < length env && i >= 0 = return $ snd (env !! i)
257257 | otherwise = return $ VV i
258− ev ntimes stk top env (Bind n (Let t v) sc)
258+ ev ntimes stk top env (Bind n (Let t v) sc)
259259 | not runtime || occurrences n sc < 2
260260 = do v' <- ev ntimes stk top env v --(finalise v)
261261 sc' <- ev ntimes stk top ((n, v') : env) sc
@@ -283,7 +283,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
283283 where vbind env t
284284 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
285285 -- block reduction immediately under codata (and not forced)
286− ev ntimes stk top env
286+ ev ntimes stk top env
287287 (App (App (App d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)
288288 | dly == txt "Delay" && lco == txt "LazyCodata" && not simpl
289289 = do let (f, _) = unApply arg
@@ -311,7 +311,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
311311 t' <- ev ntimes stk top env t
312312-- tfull' <- reapply ntimes stk top env t' []
313313 return (doProj t' (getValArgs t'))
314− where doProj t' (VP (DCon _ _ _) _ _, args)
314+ where doProj t' (VP (DCon _ _ _) _ _, args)
315315 | i >= 0 && i < length args = args!!i
316316 doProj t' _ = VProj t' i
317317
@@ -338,7 +338,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
338338 _ -> case args of
339339 (a : as) -> return $ unload env f (a : as)
340340 [] -> return f
341− reapply ntimes stk top env (VApp f a) args
341+ reapply ntimes stk top env (VApp f a) args
342342 = reapply ntimes stk top env f (a : args)
343343 reapply ntimes stk top env v args = return v
344344
@@ -356,7 +356,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
356356 do let val = lookupDefAcc n (spec || atRepl) ctxt
357357 case val of
358358 [(CaseOp ci _ _ _ _ cd, acc)]
359− | acc /= Frozen || sUN "assert_total" `elem` stk ->
359+ | acc /= Frozen || sUN "assert_total" `elem` stk ->
360360 -- unoptimised version
361361 let (ns, tree) = getCases cd in
362362 if blockSimplify ci n stk
@@ -402,7 +402,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
402402 t <- evTree ntimes stk top env (zip ns args') tree
403403 when spec $ case t of
404404 Nothing -> reinstate n -- Blocked, count n again
405− Just _ -> return ()
405+ Just _ -> return ()
406406-- (zipWith (\n , t) -> (n, t)) ns args') tree
407407 return (t, rest)
408408 | otherwise = return (Nothing, args)
@@ -416,7 +416,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
416416 (amap ++ env) etm
417417 return $ Just etm'
418418 evTree ntimes stk top env amap (ProjCase t alts)
419− = do t' <- ev ntimes stk top env t
419+ = do t' <- ev ntimes stk top env t
420420 doCase ntimes stk top env amap t' alts
421421 evTree ntimes stk top env amap (Case _ n alts)
422422 = case lookup n amap of
@@ -591,10 +591,10 @@ convEq ctxt holes topx topy = ceq [] topx topy where
591591 ceq ps x (Bind n (PVTy t) sc) = ceq ps x sc
592592
593593 ceq ps (V x) (V y) = return (x == y)
594− ceq ps (V x) (P _ y _)
594+ ceq ps (V x) (P _ y _)
595595 | x >= 0 && length ps > x = return (fst (ps!!x) == y)
596596 | otherwise = return False
597− ceq ps (P _ x _) (V y)
597+ ceq ps (P _ x _) (V y)
598598 | y >= 0 && length ps > y = return (x == snd (ps!!y))
599599 | otherwise = return False
600600 ceq ps (Bind n xb xs) (Bind n' yb ys)
@@ -833,6 +833,9 @@ addDatatype (Data n tag ty unique cons) uctxt
833833 (TyDecl (DCon tag (arity ty') unique) ty, Public, Unchecked, EmptyMI) ctxt)
834834
835835-- FIXME: Too many arguments! Refactor all these Bools.
836+--
837+-- Issue #1724 on the issue tracker.
838+-- https://github.com/idris-lang/Idris-dev/issues/1724
836839addCasedef :: Name -> ErasureInfo -> CaseInfo ->
837840 Bool -> Bool -> Bool -> Bool ->
838841 [Type] -> -- argument types