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

git.iko.soy/Idris-dev

Change reduction rules for coinductive definitions

Allow reduction in types, but block any reduction immediately under a Delay. This means coinductive proofs should now be possible, and coinductive definitions should be runnable at the REPL even if the produce an infinite stream.

commit71a968cd3240cbd7e3a08bcf05815ae5317b47ae authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 22 Mar 2014, 18:18 (13 years ago) parent88aa6d1

2 files changed+13−2

compare with master

unifiedsplit

src/Idris/Core/Evaluate.hs+13 src/Idris/ElabDecls.hs−2

src/Idris/Core/Evaluate.hs+13

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

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

263263 where vbind env t

264264 = 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'

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

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

267280 | [(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

144144 addIBC (IBCErrorHandler n)

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

146146 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)

149147 return usety

150148 where

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