git.iko.soy/Idris-dev
on master help sign in
Normalise everything before 'with' abstraction
6e39ba5Edwin Brady
libs/base/Data/Bits.idr−3
compare with master
unifiedsplit
@@ -18,9 +18,6 @@ nextPow2 x = if x == (2 `power` l2x)
18nextBytes : Nat -> Nat
18nextBytes : Nat -> Nat
19nextBytes bits = (nextPow2 (bits `divCeil` 8))
19nextBytes bits = (nextPow2 (bits `divCeil` 8))
20
20
21−-- TMP HACK while I find a better way to do 'with' abstraction
22−%freeze nextBytes
23−
24machineTy : Nat -> Type
21machineTy : Nat -> Type
25machineTy Z = Bits8
22machineTy Z = Bits8
26machineTy (S Z) = Bits16
23machineTy (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)
1741 logLvl 3 (show lhs_tm)
1741 logLvl 3 (show lhs_tm)
1742 (clhs, clhsty) <- recheckC fc [] lhs_tm
1742 (clhs, clhsty) <- recheckC fc [] lhs_tm
1743 logLvl 5 ("Checked " ++ show clhs)
1743 logLvl 5 ("Checked " ++ show clhs)
1744− let bargs = getPBtys lhs_tm
1744+ let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))
1745 let wval = addImplBound i (map fst bargs) wval_in
1745 let wval = addImplBound i (map fst bargs) wval_in
1746 logLvl 5 ("Checking " ++ showTmImpls wval)
1746 logLvl 5 ("Checking " ++ showTmImpls wval)
1747 -- Elaborate wval in this context
1747 -- Elaborate wval in this context
@@ -1763,7 +1763,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1763 logLvl 5 ("Checked wval " ++ show wval')
1763 logLvl 5 ("Checked wval " ++ show wval')
1764 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')
1764 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')
1765 let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)
1765 let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)
1766− let cwvalN = explicitNames cwval
1766+ let cwvalN = explicitNames (normalise ctxt [] cwval)
1767 logLvl 5 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)
1767 logLvl 5 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)
1768 let pvars = map fst (getPBtys cwvalty)
1768 let pvars = map fst (getPBtys cwvalty)
1769 -- we need the unelaborated term to get the names it depends on
1769 -- we need the unelaborated term to get the names it depends on