faa58ad · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix evaluation of non-total things

This was done the wrong way, by setting the access rules, but should be done by explicitly checking the totality. Otherwise, we might lose reduction rules when importing a module

commitfaa58adbb5ca45604da9e3c25133b391b8771bc6 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 29 Mar 2016, 14:23 (11 years ago) parent716b6a0

2 files changed+12−16

compare with master

unifiedsplit

src/Idris/Core/Evaluate.hs+12−2 src/Idris/Coverage.hs−14

src/Idris/Core/Evaluate.hs+12−2

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

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

247247 | otherwise

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

249− if u then

249+ let red = u && (tcReducible n ctxt || spec || atRepl || runtime)

250+ if red then

250251 do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt

251252 case val of

252253 [(Function _ tm, _)] | sUN "assert_total" `elem` stk ->

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

370371 _ -> return $ unload env f args

371372 | otherwise

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

373− if u then

374+ let red = u && (tcReducible n ctxt || spec || atRepl || runtime)

375+ if red then

374376 do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt

375377 case val of

376378 [(CaseOp ci _ _ _ _ cd, acc)]

@@ -1088,6 +1090,14 @@ lookupTotalExact :: Name -> Context -> Maybe Totality

10881090lookupTotalExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)

10891091 where mkt (d, a, t, m) = t

10901092

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+

10911101lookupMetaInformation :: Name -> Context -> [MetaInformation]

10921102lookupMetaInformation n ctxt = map mkm $ lookupCtxt n (definitions ctxt)

10931103 where mkm (d, a, t, m) = m

src/Idris/Coverage.hs−14

@@ -458,20 +458,6 @@ checkDeclTotality (fc, n)

458458 _ -> []

459459 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n

460460 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 ()

475461 return t

476462

477463