@@ -8,7 +8,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
8 Context, initContext, ctxtAlist, uconstraints, next_tvar,
8 Context, initContext, ctxtAlist, uconstraints, next_tvar,
9 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,
9 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,
10 addDatatype, addCasedef, simplifyCasedef, addOperator,
10 addDatatype, addCasedef, simplifyCasedef, addOperator,
11− lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
11+ lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
12 lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
12 lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
13 mapDefCtxt,
13 mapDefCtxt,
14 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, isTConName, isConName, isFnName,
14 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, isTConName, isConName, isFnName,
@@ -92,7 +92,7 @@ normaliseTrace tr ctxt env t
93-- Return a specialised name, and an updated list of reductions available,
93-- Return a specialised name, and an updated list of reductions available,
94-- so that the caller can tell how much specialisation was achieved.
94-- 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 ->
96 (TT Name, [(Name, Int)])
96 (TT Name, [(Name, Int)])
97specialise ctxt env limits t
97specialise ctxt env limits t
98 = let (tm, st) =
98 = let (tm, st) =
@@ -176,7 +176,7 @@ usable False n ns
178fnCount :: Int -> Name -> Eval ()
178fnCount :: Int -> Name -> Eval ()
179−fnCount inc n
179+fnCount inc n
180 = do ES ls num b <- get
180 = do ES ls num b <- get
181 case lookup n ls of
181 case lookup n ls of
182 Just i -> do put $ ES ((n, (i - inc)) :
182 Just i -> do put $ ES ((n, (i - inc)) :
@@ -255,7 +255,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
255 ev ntimes stk top env (V i)
255 ev ntimes stk top env (V i)
256 | i < length env && i >= 0 = return $ snd (env !! i)
256 | i < length env && i >= 0 = return $ snd (env !! i)
257 | otherwise = return $ VV i
257 | 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)
259 | not runtime || occurrences n sc < 2
259 | not runtime || occurrences n sc < 2
260 = do v' <- ev ntimes stk top env v --(finalise v)
260 = do v' <- ev ntimes stk top env v --(finalise v)
261 sc' <- ev ntimes stk top ((n, v') : env) sc
261 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
283 where vbind env t
283 where vbind env t
284 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
284 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
285 -- block reduction immediately under codata (and not forced)
285 -- block reduction immediately under codata (and not forced)
286− ev ntimes stk top env
286+ ev ntimes stk top env
287 (App (App (App d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)
287 (App (App (App d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)
288 | dly == txt "Delay" && lco == txt "LazyCodata" && not simpl
288 | dly == txt "Delay" && lco == txt "LazyCodata" && not simpl
289 = do let (f, _) = unApply arg
289 = do let (f, _) = unApply arg
@@ -311,7 +311,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
311 t' <- ev ntimes stk top env t
311 t' <- ev ntimes stk top env t
312-- tfull' <- reapply ntimes stk top env t' []
312-- tfull' <- reapply ntimes stk top env t' []
313 return (doProj t' (getValArgs t'))
313 return (doProj t' (getValArgs t'))
314− where doProj t' (VP (DCon _ _ _) _ _, args)
314+ where doProj t' (VP (DCon _ _ _) _ _, args)
315 | i >= 0 && i < length args = args!!i
315 | i >= 0 && i < length args = args!!i
316 doProj t' _ = VProj t' i
316 doProj t' _ = VProj t' i
@@ -338,7 +338,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
338 _ -> case args of
338 _ -> case args of
339 (a : as) -> return $ unload env f (a : as)
339 (a : as) -> return $ unload env f (a : as)
340 [] -> return f
340 [] -> return f
341− reapply ntimes stk top env (VApp f a) args
341+ reapply ntimes stk top env (VApp f a) args
342 = reapply ntimes stk top env f (a : args)
342 = reapply ntimes stk top env f (a : args)
343 reapply ntimes stk top env v args = return v
343 reapply ntimes stk top env v args = return v
@@ -356,7 +356,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
356 do let val = lookupDefAcc n (spec || atRepl) ctxt
356 do let val = lookupDefAcc n (spec || atRepl) ctxt
357 case val of
357 case val of
358 [(CaseOp ci _ _ _ _ cd, acc)]
358 [(CaseOp ci _ _ _ _ cd, acc)]
359− | acc /= Frozen || sUN "assert_total" `elem` stk ->
359+ | acc /= Frozen || sUN "assert_total" `elem` stk ->
360 -- unoptimised version
360 -- unoptimised version
361 let (ns, tree) = getCases cd in
361 let (ns, tree) = getCases cd in
362 if blockSimplify ci n stk
362 if blockSimplify ci n stk
@@ -402,7 +402,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
402 t <- evTree ntimes stk top env (zip ns args') tree
402 t <- evTree ntimes stk top env (zip ns args') tree
403 when spec $ case t of
403 when spec $ case t of
404 Nothing -> reinstate n -- Blocked, count n again
404 Nothing -> reinstate n -- Blocked, count n again
405− Just _ -> return ()
405+ Just _ -> return ()
406-- (zipWith (\n , t) -> (n, t)) ns args') tree
406-- (zipWith (\n , t) -> (n, t)) ns args') tree
407 return (t, rest)
407 return (t, rest)
408 | otherwise = return (Nothing, args)
408 | otherwise = return (Nothing, args)
@@ -416,7 +416,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
416 (amap ++ env) etm
416 (amap ++ env) etm
417 return $ Just etm'
417 return $ Just etm'
418 evTree ntimes stk top env amap (ProjCase t alts)
418 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
420 doCase ntimes stk top env amap t' alts
420 doCase ntimes stk top env amap t' alts
421 evTree ntimes stk top env amap (Case _ n alts)
421 evTree ntimes stk top env amap (Case _ n alts)
422 = case lookup n amap of
422 = case lookup n amap of
@@ -591,10 +591,10 @@ convEq ctxt holes topx topy = ceq [] topx topy where
591 ceq ps x (Bind n (PVTy t) sc) = ceq ps x sc
591 ceq ps x (Bind n (PVTy t) sc) = ceq ps x sc
593 ceq ps (V x) (V y) = return (x == y)
593 ceq ps (V x) (V y) = return (x == y)
594− ceq ps (V x) (P _ y _)
594+ ceq ps (V x) (P _ y _)
595 | x >= 0 && length ps > x = return (fst (ps!!x) == y)
595 | x >= 0 && length ps > x = return (fst (ps!!x) == y)
596 | otherwise = return False
596 | otherwise = return False
597− ceq ps (P _ x _) (V y)
597+ ceq ps (P _ x _) (V y)
598 | y >= 0 && length ps > y = return (x == snd (ps!!y))
598 | y >= 0 && length ps > y = return (x == snd (ps!!y))
599 | otherwise = return False
599 | otherwise = return False
600 ceq ps (Bind n xb xs) (Bind n' yb ys)
600 ceq ps (Bind n xb xs) (Bind n' yb ys)
@@ -833,6 +833,9 @@ addDatatype (Data n tag ty unique cons) uctxt
833 (TyDecl (DCon tag (arity ty') unique) ty, Public, Unchecked, EmptyMI) ctxt)
833 (TyDecl (DCon tag (arity ty') unique) ty, Public, Unchecked, EmptyMI) ctxt)
835-- FIXME: Too many arguments! Refactor all these Bools.
835-- FIXME: Too many arguments! Refactor all these Bools.
837+-- Issue #1724 on the issue tracker.
838+-- https://github.com/idris-lang/Idris-dev/issues/1724
836addCasedef :: Name -> ErasureInfo -> CaseInfo ->
839addCasedef :: Name -> ErasureInfo -> CaseInfo ->
837 Bool -> Bool -> Bool -> Bool ->
840 Bool -> Bool -> Bool -> Bool ->
838 [Type] -> -- argument types
841 [Type] -> -- argument types