Repository : ssh://darcs.haskell.org//srv/darcs/ghc On branch : type-nats
http://hackage.haskell.org/trac/ghc/changeset/13a31947e39093ae3cd39b55be78a8fcbdfd7a9e >--------------------------------------------------------------- commit 13a31947e39093ae3cd39b55be78a8fcbdfd7a9e Author: Iavor S. Diatchki <[email protected]> Date: Mon Apr 30 22:28:36 2012 -0700 Remove the 3rd argument of TnLeqDef, as in the other functions. >--------------------------------------------------------------- compiler/coreSyn/CoreLint.lhs | 3 +-- compiler/iface/BinIface.hs | 6 +++--- compiler/types/Coercion.lhs | 4 ++-- 3 files changed, 6 insertions(+), 7 deletions(-) diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs index 2c02b70..0baba18 100644 --- a/compiler/coreSyn/CoreLint.lhs +++ b/compiler/coreSyn/CoreLint.lhs @@ -905,8 +905,7 @@ lintCoercion (TypeNatCo co ts cs) (TnAddDef a b, [], []) -> return (kN, mkAdd (mkN a) (mkN b), mkN (a + b)) (TnMulDef a b, [], []) -> return (kN, mkMul (mkN a) (mkN b), mkN (a * b)) (TnExpDef a b, [], []) -> return (kN, mkExp (mkN a) (mkN b), mkN (a ^ b)) - (TnLeqDef a b c, [], []) - | (a <= b) == c -> return (kB, mkLeq (mkN a) (mkN b), mkB c) + (TnLeqDef a b, [], []) -> return (kB, mkLeq (mkN a) (mkN b), mkB (a <= b)) -- XXX: Check proofs (TnLeqASym, [a,b], [_,_]) -> return (kN, a, b) diff --git a/compiler/iface/BinIface.hs b/compiler/iface/BinIface.hs index c16253f..1c3972e 100644 --- a/compiler/iface/BinIface.hs +++ b/compiler/iface/BinIface.hs @@ -1082,8 +1082,8 @@ instance Binary TypeNatCoAxiom where TnAddDef a b -> byte 0x00 >> putNatural bh a >> putNatural bh b TnMulDef a b -> byte 0x01 >> putNatural bh a >> putNatural bh b TnExpDef a b -> byte 0x02 >> putNatural bh a >> putNatural bh b - TnLeqDef a b c -> byte 0x03 >> putNatural bh a >> putNatural bh b - >> put_ bh c + TnLeqDef a b -> byte 0x03 >> putNatural bh a >> putNatural bh b + TnLeqASym -> byte 0x04 TnLeq0 -> byte 0x05 TnLeqRefl -> byte 0x06 @@ -1118,7 +1118,7 @@ instance Binary TypeNatCoAxiom where 0x00 -> liftM2 TnAddDef (getNatural bh) (getNatural bh) 0x01 -> liftM2 TnMulDef (getNatural bh) (getNatural bh) 0x02 -> liftM2 TnExpDef (getNatural bh) (getNatural bh) - 0x03 -> liftM3 TnLeqDef (getNatural bh) (getNatural bh) (get bh) + 0x03 -> liftM2 TnLeqDef (getNatural bh) (getNatural bh) 0x04 -> return TnLeqASym 0x05 -> return TnLeq0 diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index a27df34..503bb63 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -165,7 +165,7 @@ data TypeNatCoAxiom = TnAddDef Integer Integer -- 2 + 3 ~ 5 | TnMulDef Integer Integer -- 2 * 3 ~ 6 | TnExpDef Integer Integer -- 2 ^ 3 ~ 8 - | TnLeqDef Integer Integer Bool -- 2 <=? 3 ~ True + | TnLeqDef Integer Integer -- 2 <=? 3 ~ True -- Order | TnLeqASym -- forall a b. (a <=? b ~ True, b <=? a ~ True) => a ~ b @@ -1212,7 +1212,7 @@ coercionKindTypeNat ax ts = (TnAddDef a b, ~[]) -> Pair (mkAdd (mkN a) (mkN b)) (mkN (a + b)) (TnMulDef a b, ~[]) -> Pair (mkMul (mkN a) (mkN b)) (mkN (a * b)) (TnExpDef a b, ~[]) -> Pair (mkExp (mkN a) (mkN b)) (mkN (a ^ b)) - (TnLeqDef _ _ _, ~[]) -> panic "tcCoercionKindTypeNat" "XXX: LeqDef" + (TnLeqDef _ _, ~[]) -> panic "tcCoercionKindTypeNat" "XXX: LeqDef" (TnLeqASym, ~[a,b]) -> Pair a b (TnLeq0, ~[_]) -> panic "tcCoercionKindTypeNat" "XXX: Leq0" _______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
