git.iko.soy/Idris-dev
on master help sign in
Fix evaluation of non-total things
faa58adEdwin Brady
src/Idris/Core/Evaluate.hs+12−2
compare with master
unifiedsplit
@@ -246,7 +246,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
246 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)
246 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)
247 | otherwise
247 | otherwise
248 = do (u, ntimes) <- usable spec n ntimes_in
248 = do (u, ntimes) <- usable spec n ntimes_in
249+ let red = u && (tcReducible n ctxt || spec || atRepl || runtime)
249− if u then
250+ if red then
250 do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt
251 do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt
251 case val of
252 case val of
252 [(Function _ tm, _)] | sUN "assert_total" `elem` stk ->
253 [(Function _ tm, _)] | sUN "assert_total" `elem` stk ->
@@ -370,7 +371,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
370 _ -> return $ unload env f args
371 _ -> return $ unload env f args
371 | otherwise
372 | otherwise
372 = do (u, ntimes) <- usable spec n ntimes_in
373 = do (u, ntimes) <- usable spec n ntimes_in
374+ let red = u && (tcReducible n ctxt || spec || atRepl || runtime)
373− if u then
375+ if red then
374 do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt
376 do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt
375 case val of
377 case val of
376 [(CaseOp ci _ _ _ _ cd, acc)]
378 [(CaseOp ci _ _ _ _ cd, acc)]
@@ -1088,6 +1090,14 @@ lookupTotalExact :: Name -> Context -> Maybe Totality
1088lookupTotalExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)
1090lookupTotalExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)
1089 where mkt (d, a, t, m) = t
1091 where mkt (d, a, t, m) = t
1090
1092
1093+-- Check if a name is reducible in the type checker. Partial definitions
1094+-- are not reducible (so treated as a constant)
1095+tcReducible :: Name -> Context -> Bool
1096+tcReducible n ctxt = case lookupTotalExact n ctxt of
1097+ Nothing -> False
1098+ Just (Partial _) -> False
1099+ _ -> True
1100+
1091lookupMetaInformation :: Name -> Context -> [MetaInformation]
1101lookupMetaInformation :: Name -> Context -> [MetaInformation]
1092lookupMetaInformation n ctxt = map mkm $ lookupCtxt n (definitions ctxt)
1102lookupMetaInformation n ctxt = map mkm $ lookupCtxt n (definitions ctxt)
1093 where mkm (d, a, t, m) = m
1103 where mkm (d, a, t, m) = m
src/Idris/Coverage.hs−14
@@ -458,20 +458,6 @@ checkDeclTotality (fc, n)
458 _ -> []
458 _ -> []
459 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
459 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
460 t <- checkTotality [] fc n
460 t <- checkTotality [] fc n
461− let acc = case lookupDefAccExact n False (tt_ctxt i) of
462− Just (n, a) -> a
463− _ -> Public
464− case t of
465− -- if it's not total, it can't reduce, to keep
466− -- typechecking decidable.
467− -- So if it's currently public export, set it as
468− -- export instead.
469− p@(Partial _) -> do let newacc = max Frozen acc
470− setAccessibility n newacc
471− addIBC (IBCAccess n newacc)
472− logCoverage 5 $ "Set to " ++ show newacc ++ ":"
473− ++ show n ++ show p
474− _ -> return ()
475 return t
461 return t
476
462
477
463