git.iko.soy/Idris-dev
on master help sign in
Normalise before abstracting over 'with' type
1d23ad1Edwin Brady
libs/base/Data/Bits.idr+3
compare with master
unifiedsplit
@@ -18,6 +18,9 @@ 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+
21machineTy : Nat -> Type
24machineTy : Nat -> Type
22machineTy Z = Bits8
25machineTy Z = Bits8
23machineTy (S Z) = Bits16
26machineTy (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)
1737 (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )
1737 (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )
1738 let lhs_tm = orderPats (getInferTerm lhs')
1738 let lhs_tm = orderPats (getInferTerm lhs')
1739 let lhs_ty = getInferType lhs'
1739 let lhs_ty = getInferType lhs'
1740− let ret_ty = getRetTy lhs_ty
1740+ let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))
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)
@@ -1762,7 +1762,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1762 mapM_ (elabCaseBlock info opts) is
1762 mapM_ (elabCaseBlock info opts) is
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 cwvalty
1765+ let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)
1766 let cwvalN = explicitNames cwval
1766 let cwvalN = explicitNames 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)
@@ -1778,12 +1778,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1778 -- (ps : Xs) -> (withval : cwvalty) -> (ps' : Xs') -> ret_ty
1778 -- (ps : Xs) -> (withval : cwvalty) -> (ps' : Xs') -> ret_ty
1779 let wargval = getRetTy cwvalN
1779 let wargval = getRetTy cwvalN
1780 let wargtype = getRetTy cwvaltyN
1780 let wargtype = getRetTy cwvaltyN
1781− logLvl 5 ("Abstract over " ++ show wargval)
1781+ logLvl 5 ("Abstract over " ++ show wargval ++ " in " ++ show wargtype)
1782 let wtype = bindTyArgs Pi (bargs_pre ++
1782 let wtype = bindTyArgs Pi (bargs_pre ++
1783 (sMN 0 "warg", wargtype) :
1783 (sMN 0 "warg", wargtype) :
1784 map (abstract (sMN 0 "warg") wargval wargtype) bargs_post)
1784 map (abstract (sMN 0 "warg") wargval wargtype) bargs_post)
1785 (substTerm wargval (P Bound (sMN 0 "warg") wargtype) ret_ty)
1785 (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)
1787 let wname = sMN windex (show fname)
1787 let wname = sMN windex (show fname)
1788
1788
1789 let imps = getImps wtype -- add to implicits context
1789 let imps = getImps wtype -- add to implicits context