git.iko.soy/Idris-dev
on master help sign in
Normalise everything before 'with' abstraction

Now the TMP HACK in Data.Bits can go

commit6e39ba51da68ce7f14241e94d547a6f606bb6ef6 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 15 Jul 2014, 20:18 (12 years ago) parent1d23ad1
2 files changed+2−5
compare with master
unifiedsplit
libs/base/Data/Bits.idr−3 src/Idris/ElabDecls.hs+2−2
libs/base/Data/Bits.idr−3
@@ -18,9 +18,6 @@ nextPow2 x = if x == (2 `power` l2x)
1818nextBytes : Nat -> Nat
1919nextBytes bits = (nextPow2 (bits `divCeil` 8))
2020
21−-- TMP HACK while I find a better way to do 'with' abstraction
22−%freeze nextBytes
23−
2421machineTy : Nat -> Type
2522machineTy Z = Bits8
2623machineTy (S Z) = Bits16
src/Idris/ElabDecls.hs+2−2
@@ -1741,7 +1741,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
17411741 logLvl 3 (show lhs_tm)
17421742 (clhs, clhsty) <- recheckC fc [] lhs_tm
17431743 logLvl 5 ("Checked " ++ show clhs)
1744− let bargs = getPBtys lhs_tm
1744+ let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))
17451745 let wval = addImplBound i (map fst bargs) wval_in
17461746 logLvl 5 ("Checking " ++ showTmImpls wval)
17471747 -- Elaborate wval in this context
@@ -1763,7 +1763,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
17631763 logLvl 5 ("Checked wval " ++ show wval')
17641764 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')
17651765 let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)
1766− let cwvalN = explicitNames cwval
1766+ let cwvalN = explicitNames (normalise ctxt [] cwval)
17671767 logLvl 5 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)
17681768 let pvars = map fst (getPBtys cwvalty)
17691769 -- we need the unelaborated term to get the names it depends on