d6a185a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Reduction limit when simplifying

The totality checker reduces a bit, but shouldn't go too deep. The REPL also has a reduction limit, but it's useful if it can go further. This fixes a problem with test reg028

commitd6a185a0b8c8f3b6808c74f585f9dead1d350e81 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 11 Jun 2016, 16:19 (10 years ago) parentb03f823

1 file changed+9−6

compare with master

unifiedsplit

src/Idris/Core/Evaluate.hs+9−6

src/Idris/Core/Evaluate.hs+9−6

@@ -185,21 +185,22 @@ unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc

185185unbindEnv env tm = error $ "Impossible case occurred: couldn't unbind env."

186186

187187usable :: Bool -- specialising

188+ -> Int -- Reduction depth limit (when simplifying/at REPL)

188189 -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])

189190-- usable _ _ ns@((MN 0 "STOP", _) : _) = return (False, ns)

190−usable False n [] = return (True, [])

191−usable True n ns

191+usable False depthlimit n [] = return (True, [])

192+usable True depthlimit n ns

192193 = do ES ls num b <- get

193194 if b then return (False, ns)

194195 else case lookup n ls of

195196 Just 0 -> return (False, ns)

196197 Just i -> return (True, ns)

197198 _ -> return (False, ns)

198−usable False n ns

199+usable False depthlimit n ns

199200 = case lookup n ns of

200201 Just 0 -> return (False, ns)

201202 Just i -> return $ (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)

202− _ -> return $ (True, (n, 1000000) : filter (\ (n', _) -> n/=n') ns)

203+ _ -> return $ (True, (n, depthlimit) : filter (\ (n', _) -> n/=n') ns)

203204

204205

205206fnCount :: Int -> Name -> Eval ()

@@ -253,7 +254,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

253254 ev ntimes_in stk top env (P Ref n ty)

254255 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)

255256 | otherwise

256− = do (u, ntimes) <- usable spec n ntimes_in

257+ = do let limit = if simpl then 100 else 10000

258+ (u, ntimes) <- usable spec limit n ntimes_in

257259 let red = u && (tcReducible n ctxt || spec || atRepl || runtime

258260 || sUN "assert_total" `elem` stk)

259261 if red then

@@ -377,7 +379,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

377379 [] -> return f

378380 _ -> return $ unload env f args

379381 | otherwise

380− = do (u, ntimes) <- usable spec n ntimes_in

382+ = do let limit = if simpl then 100 else 10000

383+ (u, ntimes) <- usable spec limit n ntimes_in

381384 let red = u && (tcReducible n ctxt || spec || atRepl || runtime

382385 || sUN "assert_total" `elem` stk)

383386 if red then