git.iko.soy/Idris-dev
on master help sign in
Normalise before abstracting over 'with' type

Otherwise we don't necessarily abstract over the scrutinee properly in the resulting function. This has necessitated a hack in Data.Bits, which I will sort out ASAP.

commit1d23ad17b1eea5c55014529c596135046886f25f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 15 Jul 2014, 19:19 (12 years ago) parent4d62d30
2 files changed+7−4
compare with master
unifiedsplit
libs/base/Data/Bits.idr+3 src/Idris/ElabDecls.hs+4−4
libs/base/Data/Bits.idr+3
@@ -18,6 +18,9 @@ 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+
2124machineTy : Nat -> Type
2225machineTy Z = Bits8
2326machineTy (S Z) = Bits16
src/Idris/ElabDecls.hs+4−4
@@ -1737,7 +1737,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
17371737 (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )
17381738 let lhs_tm = orderPats (getInferTerm lhs')
17391739 let lhs_ty = getInferType lhs'
1740− let ret_ty = getRetTy lhs_ty
1740+ let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))
17411741 logLvl 3 (show lhs_tm)
17421742 (clhs, clhsty) <- recheckC fc [] lhs_tm
17431743 logLvl 5 ("Checked " ++ show clhs)
@@ -1762,7 +1762,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
17621762 mapM_ (elabCaseBlock info opts) is
17631763 logLvl 5 ("Checked wval " ++ show wval')
17641764 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')
1765− let cwvaltyN = explicitNames cwvalty
1765+ let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)
17661766 let cwvalN = explicitNames cwval
17671767 logLvl 5 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)
17681768 let pvars = map fst (getPBtys cwvalty)
@@ -1778,12 +1778,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
17781778 -- (ps : Xs) -> (withval : cwvalty) -> (ps' : Xs') -> ret_ty
17791779 let wargval = getRetTy cwvalN
17801780 let wargtype = getRetTy cwvaltyN
1781− logLvl 5 ("Abstract over " ++ show wargval)
1781+ logLvl 5 ("Abstract over " ++ show wargval ++ " in " ++ show wargtype)
17821782 let wtype = bindTyArgs Pi (bargs_pre ++
17831783 (sMN 0 "warg", wargtype) :
17841784 map (abstract (sMN 0 "warg") wargval wargtype) bargs_post)
17851785 (substTerm wargval (P Bound (sMN 0 "warg") wargtype) ret_ty)
1786− logLvl 3 ("New function type " ++ show wtype)
1786+ logLvl 5 ("New function type " ++ show wtype)
17871787 let wname = sMN windex (show fname)
17881788
17891789 let imps = getImps wtype -- add to implicits context