205ad70 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Tweak reduction rules for private/abstract names

It is better if private names reduce during typechecking (since such things arise in public functions which should reduce completely) and only abstract names are prevented from reducing. Fixes #348

commit205ad70c080e2264ccf68b7566eecdc880b27255 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 24 Nov 2013, 15:19 (13 years ago) parentc459480

2 files changed+5−3

compare with master

unifiedsplit

src/Core/Evaluate.hs+4−2 src/Idris/ElabTerm.hs+1−1

src/Core/Evaluate.hs+4−2

@@ -207,10 +207,12 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

207207 case val of

208208 [(Function _ tm, Public)] ->

209209 ev ntimes (n:stk) True env tm

210+ [(Function _ tm, Hidden)] ->

211+ ev ntimes (n:stk) True env tm

210212 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty

211213 return $ VP nt n vty

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

213− | acc == Public &&

215+ | (acc /= Frozen) &&

214216 null (fst (cases_totcheck cd)) -> -- unoptimised version

215217 let (ns, tree) = getCases cd in

216218 if blockSimplify ci n stk

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

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

309311 case val of

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

311− | acc == Public -> -- unoptimised version

313+ | acc /= Frozen -> -- unoptimised version

312314 let (ns, tree) = getCases cd in

313315 if blockSimplify ci n stk

314316 then return $ unload env (VP Ref n ty) args

src/Idris/ElabTerm.hs+1−1

@@ -653,7 +653,7 @@ resolveTC :: Int -> Name -> IState -> ElabD ()

653653resolveTC 0 fn ist = fail $ "Can't resolve type class"

654654resolveTC 1 fn ist = try' (trivial' ist) (resolveTC 0 fn ist) True

655655resolveTC depth fn ist

656− = do compute

656+ = do hnf_compute

657657 g <- goal

658658 ptm <- get_term

659659 hs <- get_holes