71a968c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Change reduction rules for coinductive definitions

71a968cEdwin Brady13 years ago

src/Idris/Core/Evaluate.hs+13

@@ -262,6 +262,19 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

262 n' b' (\x -> ev ntimes stk False ((n', x):env) sc)

263 where vbind env t

264 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t

265+ -- block reduction immediately under codata (and not forced)

266+ ev ntimes stk top env

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

268+ | dly == txt "Delay" && lco == txt "LazyCodata"

269+ = do let (f, _) = unApply arg

270+ let ntimes' = case f of

271+ P _ fn _ -> (fn, 0) : ntimes

272+ _ -> ntimes

273+ d' <- ev ntimes' stk False env d

274+ l' <- ev ntimes' stk False env l

275+ t' <- ev ntimes' stk False env t

276+ arg' <- ev ntimes' stk False env arg

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

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

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

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

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

267 | [(CaseOp _ _ _ _ _ _, _)] <- lookupDefAcc n (spec || atRepl) ctxt,

280 | [(CaseOp _ _ _ _ _ _, _)] <- lookupDefAcc n (spec || atRepl) ctxt,

src/Idris/ElabDecls.hs−2

@@ -144,8 +144,6 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

144 addIBC (IBCErrorHandler n)

145 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"

146 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."

147− when corec $ do setAccessibility n Frozen

148− addIBC (IBCAccess n Frozen)

149 return usety

147 return usety

150 where

148 where

151 -- for making an internalapp, we only want the explicit ones, and don't

149 -- for making an internalapp, we only want the explicit ones, and don't