// Copyright 2016 The Go Authors. All rights reserved.
// Use of this source code is governed by a BSD-style
// license that can be found in the LICENSE file.

// This file contains rules to decompose [u]int64 types on 32-bit
// architectures. These rules work together with the decomposeBuiltIn
// pass which handles phis of these types.

(Int64Hi (Int64Make hi _)) -> hi
(Int64Lo (Int64Make _ lo)) -> lo

// Assuming little endian (we don't support big endian 32-bit architecture yet)
(Load <t> ptr mem) && is64BitInt(t) && t.IsSigned() ->
	(Int64Make
		(Load <config.fe.TypeInt32()> (OffPtr <config.fe.TypeInt32().PtrTo()> [4] ptr) mem)
		(Load <config.fe.TypeUInt32()> ptr mem))
(Load <t> ptr mem) && is64BitInt(t) && !t.IsSigned() ->
	(Int64Make
		(Load <config.fe.TypeUInt32()> (OffPtr <config.fe.TypeUInt32().PtrTo()> [4] ptr) mem)
		(Load <config.fe.TypeUInt32()> ptr mem))

(Store [8] dst (Int64Make hi lo) mem) ->
	(Store [4]
		(OffPtr <hi.Type.PtrTo()> [4] dst)
		hi
		(Store [4] dst lo mem))

(Arg {n} [off]) && is64BitInt(v.Type) && v.Type.IsSigned() ->
  (Int64Make
    (Arg <config.fe.TypeInt32()> {n} [off+4])
    (Arg <config.fe.TypeUInt32()> {n} [off]))
(Arg {n} [off]) && is64BitInt(v.Type) && !v.Type.IsSigned() ->
  (Int64Make
    (Arg <config.fe.TypeUInt32()> {n} [off+4])
    (Arg <config.fe.TypeUInt32()> {n} [off]))

(Add64 x y) ->
	(Int64Make
		(Add32withcarry <config.fe.TypeInt32()>
			(Int64Hi x)
			(Int64Hi y)
			(Select0 <TypeFlags> (Add32carry (Int64Lo x) (Int64Lo y))))
		(Select1 <config.fe.TypeUInt32()> (Add32carry (Int64Lo x) (Int64Lo y))))

(Sub64 x y) ->
	(Int64Make
		(Sub32withcarry <config.fe.TypeInt32()>
			(Int64Hi x)
			(Int64Hi y)
			(Select0 <TypeFlags> (Sub32carry (Int64Lo x) (Int64Lo y))))
		(Select1 <config.fe.TypeUInt32()> (Sub32carry (Int64Lo x) (Int64Lo y))))

(Mul64 x y) ->
	(Int64Make
		(Add32 <config.fe.TypeUInt32()>
			(Mul32 <config.fe.TypeUInt32()> (Int64Lo x) (Int64Hi y))
			(Add32 <config.fe.TypeUInt32()>
				(Mul32 <config.fe.TypeUInt32()> (Int64Hi x) (Int64Lo y))
				(Select0 <config.fe.TypeUInt32()> (Mul32uhilo (Int64Lo x) (Int64Lo y)))))
		(Select1 <config.fe.TypeUInt32()> (Mul32uhilo (Int64Lo x) (Int64Lo y))))

(And64 x y) ->
	(Int64Make
		(And32 <config.fe.TypeUInt32()> (Int64Hi x) (Int64Hi y))
		(And32 <config.fe.TypeUInt32()> (Int64Lo x) (Int64Lo y)))

(Or64 x y) ->
	(Int64Make
		(Or32 <config.fe.TypeUInt32()> (Int64Hi x) (Int64Hi y))
		(Or32 <config.fe.TypeUInt32()> (Int64Lo x) (Int64Lo y)))

(Xor64 x y) ->
	(Int64Make
		(Xor32 <config.fe.TypeUInt32()> (Int64Hi x) (Int64Hi y))
		(Xor32 <config.fe.TypeUInt32()> (Int64Lo x) (Int64Lo y)))

(Neg64 <t> x) -> (Sub64 (Const64 <t> [0]) x)

(Com64 x) ->
	(Int64Make
		(Com32 <config.fe.TypeUInt32()> (Int64Hi x))
		(Com32 <config.fe.TypeUInt32()> (Int64Lo x)))

(SignExt32to64 x) -> (Int64Make (Signmask x) x)
(SignExt16to64 x) -> (SignExt32to64 (SignExt16to32 x))
(SignExt8to64 x) -> (SignExt32to64 (SignExt8to32 x))

(ZeroExt32to64 x) -> (Int64Make (Const32 <config.fe.TypeUInt32()> [0]) x)
(ZeroExt16to64 x) -> (ZeroExt32to64 (ZeroExt16to32 x))
(ZeroExt8to64 x) -> (ZeroExt32to64 (ZeroExt8to32 x))

(Trunc64to32 (Int64Make _ lo)) -> lo
(Trunc64to16 (Int64Make _ lo)) -> (Trunc32to16 lo)
(Trunc64to8 (Int64Make _ lo)) -> (Trunc32to8 lo)

(Lsh32x64 _ (Int64Make (Const32 [c]) _)) && c != 0 -> (Const32 [0])
(Rsh32x64 x (Int64Make (Const32 [c]) _)) && c != 0 -> (Signmask x)
(Rsh32Ux64 _ (Int64Make (Const32 [c]) _)) && c != 0 -> (Const32 [0])
(Lsh16x64 _ (Int64Make (Const32 [c]) _)) && c != 0 -> (Const32 [0])
(Rsh16x64 x (Int64Make (Const32 [c]) _)) && c != 0 -> (Signmask (SignExt16to32 x))
(Rsh16Ux64 _ (Int64Make (Const32 [c]) _)) && c != 0 -> (Const32 [0])
(Lsh8x64 _ (Int64Make (Const32 [c]) _)) && c != 0 -> (Const32 [0])
(Rsh8x64 x (Int64Make (Const32 [c]) _)) && c != 0 -> (Signmask (SignExt8to32 x))
(Rsh8Ux64 _ (Int64Make (Const32 [c]) _)) && c != 0 -> (Const32 [0])

(Lsh32x64 x (Int64Make (Const32 [0]) lo)) -> (Lsh32x32 x lo)
(Rsh32x64 x (Int64Make (Const32 [0]) lo)) -> (Rsh32x32 x lo)
(Rsh32Ux64 x (Int64Make (Const32 [0]) lo)) -> (Rsh32Ux32 x lo)
(Lsh16x64 x (Int64Make (Const32 [0]) lo)) -> (Lsh16x32 x lo)
(Rsh16x64 x (Int64Make (Const32 [0]) lo)) -> (Rsh16x32 x lo)
(Rsh16Ux64 x (Int64Make (Const32 [0]) lo)) -> (Rsh16Ux32 x lo)
(Lsh8x64 x (Int64Make (Const32 [0]) lo)) -> (Lsh8x32 x lo)
(Rsh8x64 x (Int64Make (Const32 [0]) lo)) -> (Rsh8x32 x lo)
(Rsh8Ux64 x (Int64Make (Const32 [0]) lo)) -> (Rsh8Ux32 x lo)

(Lsh64x64 _ (Int64Make (Const32 [c]) _)) && c != 0 -> (Const64 [0])
(Rsh64x64 x (Int64Make (Const32 [c]) _)) && c != 0 -> (Int64Make (Signmask (Int64Hi x)) (Signmask (Int64Hi x)))
(Rsh64Ux64 _ (Int64Make (Const32 [c]) _)) && c != 0 -> (Const64 [0])

(Lsh64x64 x (Int64Make (Const32 [0]) lo)) -> (Lsh64x32 x lo)
(Rsh64x64 x (Int64Make (Const32 [0]) lo)) -> (Rsh64x32 x lo)
(Rsh64Ux64 x (Int64Make (Const32 [0]) lo)) -> (Rsh64Ux32 x lo)

// turn x64 non-constant shifts to x32 shifts
// if high 32-bit of the shift is nonzero, make a huge shift
(Lsh64x64 x (Int64Make hi lo)) && hi.Op != OpConst32 ->
	(Lsh64x32 x (Or32 <config.fe.TypeUInt32()> (Zeromask hi) lo))
(Rsh64x64 x (Int64Make hi lo)) && hi.Op != OpConst32 ->
	(Rsh64x32 x (Or32 <config.fe.TypeUInt32()> (Zeromask hi) lo))
(Rsh64Ux64 x (Int64Make hi lo)) && hi.Op != OpConst32 ->
	(Rsh64Ux32 x (Or32 <config.fe.TypeUInt32()> (Zeromask hi) lo))
(Lsh32x64 x (Int64Make hi lo)) && hi.Op != OpConst32 ->
	(Lsh32x32 x (Or32 <config.fe.TypeUInt32()> (Zeromask hi) lo))
(Rsh32x64 x (Int64Make hi lo)) && hi.Op != OpConst32 ->
	(Rsh32x32 x (Or32 <config.fe.TypeUInt32()> (Zeromask hi) lo))
(Rsh32Ux64 x (Int64Make hi lo)) && hi.Op != OpConst32 ->
	(Rsh32Ux32 x (Or32 <config.fe.TypeUInt32()> (Zeromask hi) lo))
(Lsh16x64 x (Int64Make hi lo)) && hi.Op != OpConst32 ->
	(Lsh16x32 x (Or32 <config.fe.TypeUInt32()> (Zeromask hi) lo))
(Rsh16x64 x (Int64Make hi lo)) && hi.Op != OpConst32 ->
	(Rsh16x32 x (Or32 <config.fe.TypeUInt32()> (Zeromask hi) lo))
(Rsh16Ux64 x (Int64Make hi lo)) && hi.Op != OpConst32 ->
	(Rsh16Ux32 x (Or32 <config.fe.TypeUInt32()> (Zeromask hi) lo))
(Lsh8x64 x (Int64Make hi lo)) && hi.Op != OpConst32 ->
	(Lsh8x32 x (Or32 <config.fe.TypeUInt32()> (Zeromask hi) lo))
(Rsh8x64 x (Int64Make hi lo)) && hi.Op != OpConst32 ->
	(Rsh8x32 x (Or32 <config.fe.TypeUInt32()> (Zeromask hi) lo))
(Rsh8Ux64 x (Int64Make hi lo)) && hi.Op != OpConst32 ->
	(Rsh8Ux32 x (Or32 <config.fe.TypeUInt32()> (Zeromask hi) lo))

// 64x left shift
// result.hi = hi<<s | lo>>(32-s) | lo<<(s-32) // >> is unsigned, large shifts result 0
// result.lo = lo<<s
(Lsh64x32 (Int64Make hi lo) s) ->
	(Int64Make
		(Or32 <config.fe.TypeUInt32()>
			(Or32 <config.fe.TypeUInt32()>
				(Lsh32x32 <config.fe.TypeUInt32()> hi s)
				(Rsh32Ux32 <config.fe.TypeUInt32()>
					lo
					(Sub32 <config.fe.TypeUInt32()> (Const32 <config.fe.TypeUInt32()> [32]) s)))
			(Lsh32x32 <config.fe.TypeUInt32()>
				lo
				(Sub32 <config.fe.TypeUInt32()> s (Const32 <config.fe.TypeUInt32()> [32]))))
		(Lsh32x32 <config.fe.TypeUInt32()> lo s))
(Lsh64x16 (Int64Make hi lo) s) ->
	(Int64Make
		(Or32 <config.fe.TypeUInt32()>
			(Or32 <config.fe.TypeUInt32()>
				(Lsh32x16 <config.fe.TypeUInt32()> hi s)
				(Rsh32Ux16 <config.fe.TypeUInt32()>
					lo
					(Sub16 <config.fe.TypeUInt16()> (Const16 <config.fe.TypeUInt16()> [32]) s)))
			(Lsh32x16 <config.fe.TypeUInt32()>
				lo
				(Sub16 <config.fe.TypeUInt16()> s (Const16 <config.fe.TypeUInt16()> [32]))))
		(Lsh32x16 <config.fe.TypeUInt32()> lo s))
(Lsh64x8 (Int64Make hi lo) s) ->
	(Int64Make
		(Or32 <config.fe.TypeUInt32()>
			(Or32 <config.fe.TypeUInt32()>
				(Lsh32x8 <config.fe.TypeUInt32()> hi s)
				(Rsh32Ux8 <config.fe.TypeUInt32()>
					lo
					(Sub8 <config.fe.TypeUInt8()> (Const8 <config.fe.TypeUInt8()> [32]) s)))
			(Lsh32x8 <config.fe.TypeUInt32()>
				lo
				(Sub8 <config.fe.TypeUInt8()> s (Const8 <config.fe.TypeUInt8()> [32]))))
		(Lsh32x8 <config.fe.TypeUInt32()> lo s))

// 64x unsigned right shift
// result.hi = hi>>s
// result.lo = lo>>s | hi<<(32-s) | hi>>(s-32) // >> is unsigned, large shifts result 0
(Rsh64Ux32 (Int64Make hi lo) s) ->
	(Int64Make
		(Rsh32Ux32 <config.fe.TypeUInt32()> hi s)
		(Or32 <config.fe.TypeUInt32()>
			(Or32 <config.fe.TypeUInt32()>
				(Rsh32Ux32 <config.fe.TypeUInt32()> lo s)
				(Lsh32x32 <config.fe.TypeUInt32()>
					hi
					(Sub32 <config.fe.TypeUInt32()> (Const32 <config.fe.TypeUInt32()> [32]) s)))
			(Rsh32Ux32 <config.fe.TypeUInt32()>
				hi
				(Sub32 <config.fe.TypeUInt32()> s (Const32 <config.fe.TypeUInt32()> [32])))))
(Rsh64Ux16 (Int64Make hi lo) s) ->
	(Int64Make
		(Rsh32Ux16 <config.fe.TypeUInt32()> hi s)
		(Or32 <config.fe.TypeUInt32()>
			(Or32 <config.fe.TypeUInt32()>
				(Rsh32Ux16 <config.fe.TypeUInt32()> lo s)
				(Lsh32x16 <config.fe.TypeUInt32()>
					hi
					(Sub16 <config.fe.TypeUInt16()> (Const16 <config.fe.TypeUInt16()> [32]) s)))
			(Rsh32Ux16 <config.fe.TypeUInt32()>
				hi
				(Sub16 <config.fe.TypeUInt16()> s (Const16 <config.fe.TypeUInt16()> [32])))))
(Rsh64Ux8 (Int64Make hi lo) s) ->
	(Int64Make
		(Rsh32Ux8 <config.fe.TypeUInt32()> hi s)
		(Or32 <config.fe.TypeUInt32()>
			(Or32 <config.fe.TypeUInt32()>
				(Rsh32Ux8 <config.fe.TypeUInt32()> lo s)
				(Lsh32x8 <config.fe.TypeUInt32()>
					hi
					(Sub8 <config.fe.TypeUInt8()> (Const8 <config.fe.TypeUInt8()> [32]) s)))
			(Rsh32Ux8 <config.fe.TypeUInt32()>
				hi
				(Sub8 <config.fe.TypeUInt8()> s (Const8 <config.fe.TypeUInt8()> [32])))))

// 64x signed right shift
// result.hi = hi>>s
// result.lo = lo>>s | hi<<(32-s) | (hi>>(s-32))&zeromask(s>>5) // hi>>(s-32) is signed, large shifts result 0/-1
(Rsh64x32 (Int64Make hi lo) s) ->
	(Int64Make
		(Rsh32x32 <config.fe.TypeUInt32()> hi s)
		(Or32 <config.fe.TypeUInt32()>
			(Or32 <config.fe.TypeUInt32()>
				(Rsh32Ux32 <config.fe.TypeUInt32()> lo s)
				(Lsh32x32 <config.fe.TypeUInt32()>
					hi
					(Sub32 <config.fe.TypeUInt32()> (Const32 <config.fe.TypeUInt32()> [32]) s)))
			(And32 <config.fe.TypeUInt32()>
				(Rsh32x32 <config.fe.TypeUInt32()>
					hi
					(Sub32 <config.fe.TypeUInt32()> s (Const32 <config.fe.TypeUInt32()> [32])))
				(Zeromask
					(Rsh32Ux32 <config.fe.TypeUInt32()> s (Const32 <config.fe.TypeUInt32()> [5]))))))
(Rsh64x16 (Int64Make hi lo) s) ->
	(Int64Make
		(Rsh32x16 <config.fe.TypeUInt32()> hi s)
		(Or32 <config.fe.TypeUInt32()>
			(Or32 <config.fe.TypeUInt32()>
				(Rsh32Ux16 <config.fe.TypeUInt32()> lo s)
				(Lsh32x16 <config.fe.TypeUInt32()>
					hi
					(Sub16 <config.fe.TypeUInt16()> (Const16 <config.fe.TypeUInt16()> [32]) s)))
			(And32 <config.fe.TypeUInt32()>
				(Rsh32x16 <config.fe.TypeUInt32()>
					hi
					(Sub16 <config.fe.TypeUInt16()> s (Const16 <config.fe.TypeUInt16()> [32])))
				(Zeromask
					(ZeroExt16to32
						(Rsh16Ux32 <config.fe.TypeUInt16()> s (Const32 <config.fe.TypeUInt32()> [5])))))))
(Rsh64x8 (Int64Make hi lo) s) ->
	(Int64Make
		(Rsh32x8 <config.fe.TypeUInt32()> hi s)
		(Or32 <config.fe.TypeUInt32()>
			(Or32 <config.fe.TypeUInt32()>
				(Rsh32Ux8 <config.fe.TypeUInt32()> lo s)
				(Lsh32x8 <config.fe.TypeUInt32()>
					hi
					(Sub8 <config.fe.TypeUInt8()> (Const8 <config.fe.TypeUInt8()> [32]) s)))
			(And32 <config.fe.TypeUInt32()>
				(Rsh32x8 <config.fe.TypeUInt32()>
					hi
					(Sub8 <config.fe.TypeUInt8()> s (Const8 <config.fe.TypeUInt8()> [32])))
				(Zeromask
					(ZeroExt8to32
						(Rsh8Ux32 <config.fe.TypeUInt8()> s (Const32 <config.fe.TypeUInt32()> [5])))))))

// 64xConst32 shifts
// we probably do not need them -- lateopt may take care of them just fine
//(Lsh64x32 _ (Const32 [c])) && uint32(c) >= 64 -> (Const64 [0])
//(Rsh64x32 x (Const32 [c])) && uint32(c) >= 64 -> (Int64Make (Signmask (Int64Hi x)) (Signmask (Int64Hi x)))
//(Rsh64Ux32 _ (Const32 [c])) && uint32(c) >= 64 -> (Const64 [0])
//
//(Lsh64x32 x (Const32 [c])) && c < 64 && c > 32 ->
//	(Int64Make
//		(Lsh32x32 <config.fe.TypeUInt32()> (Int64Lo x) (Const32 <config.fe.TypeUInt32()> [c-32]))
//		(Const32 <config.fe.TypeUInt32()> [0]))
//(Rsh64x32 x (Const32 [c])) && c < 64 && c > 32 ->
//	(Int64Make
//		(Signmask (Int64Hi x))
//		(Rsh32x32 <config.fe.TypeInt32()> (Int64Hi x) (Const32 <config.fe.TypeUInt32()> [c-32])))
//(Rsh64Ux32 x (Const32 [c])) && c < 64 && c > 32 ->
//	(Int64Make
//		(Const32 <config.fe.TypeUInt32()> [0])
//		(Rsh32Ux32 <config.fe.TypeUInt32()> (Int64Hi x) (Const32 <config.fe.TypeUInt32()> [c-32])))
//
//(Lsh64x32 x (Const32 [32])) -> (Int64Make (Int64Lo x) (Const32 <config.fe.TypeUInt32()> [0]))
//(Rsh64x32 x (Const32 [32])) -> (Int64Make (Signmask (Int64Hi x)) (Int64Hi x))
//(Rsh64Ux32 x (Const32 [32])) -> (Int64Make (Const32 <config.fe.TypeUInt32()> [0]) (Int64Hi x))
//
//(Lsh64x32 x (Const32 [c])) && c < 32 && c > 0 ->
//	(Int64Make
//		(Or32 <config.fe.TypeUInt32()>
//			(Lsh32x32 <config.fe.TypeUInt32()> (Int64Hi x) (Const32 <config.fe.TypeUInt32()> [c]))
//			(Rsh32Ux32 <config.fe.TypeUInt32()> (Int64Lo x) (Const32 <config.fe.TypeUInt32()> [32-c])))
//		(Lsh32x32 <config.fe.TypeUInt32()> (Int64Lo x) (Const32 <config.fe.TypeUInt32()> [c])))
//(Rsh64x32 x (Const32 [c])) && c < 32 && c > 0 ->
//	(Int64Make
//		(Rsh32x32 <config.fe.TypeInt32()> (Int64Hi x) (Const32 <config.fe.TypeUInt32()> [c]))
//		(Or32 <config.fe.TypeUInt32()>
//			(Rsh32Ux32 <config.fe.TypeUInt32()> (Int64Lo x) (Const32 <config.fe.TypeUInt32()> [c]))
//			(Lsh32x32 <config.fe.TypeUInt32()> (Int64Hi x) (Const32 <config.fe.TypeUInt32()> [32-c]))))
//(Rsh64Ux32 x (Const32 [c])) && c < 32 && c > 0 ->
//	(Int64Make
//		(Rsh32Ux32 <config.fe.TypeUInt32()> (Int64Hi x) (Const32 <config.fe.TypeUInt32()> [c]))
//		(Or32 <config.fe.TypeUInt32()>
//			(Rsh32Ux32 <config.fe.TypeUInt32()> (Int64Lo x) (Const32 <config.fe.TypeUInt32()> [c]))
//			(Lsh32x32 <config.fe.TypeUInt32()> (Int64Hi x) (Const32 <config.fe.TypeUInt32()> [32-c]))))
//
//(Lsh64x32 x (Const32 [0])) -> x
//(Rsh64x32 x (Const32 [0])) -> x
//(Rsh64Ux32 x (Const32 [0])) -> x

(Lrot64 (Int64Make hi lo) [c]) && c <= 32 ->
	(Int64Make
		(Or32 <config.fe.TypeUInt32()>
			(Lsh32x32 <config.fe.TypeUInt32()> hi (Const32 <config.fe.TypeUInt32()> [c]))
			(Rsh32Ux32 <config.fe.TypeUInt32()> lo (Const32 <config.fe.TypeUInt32()> [32-c])))
		(Or32 <config.fe.TypeUInt32()>
			(Lsh32x32 <config.fe.TypeUInt32()> lo (Const32 <config.fe.TypeUInt32()> [c]))
			(Rsh32Ux32 <config.fe.TypeUInt32()> hi (Const32 <config.fe.TypeUInt32()> [32-c]))))
(Lrot64 (Int64Make hi lo) [c]) && c > 32 -> (Lrot64 (Int64Make lo hi) [c-32])

(Const64 <t> [c]) && t.IsSigned() ->
	(Int64Make (Const32 <config.fe.TypeInt32()> [c>>32]) (Const32 <config.fe.TypeUInt32()> [int64(int32(c))]))
(Const64 <t> [c]) && !t.IsSigned() ->
	(Int64Make (Const32 <config.fe.TypeUInt32()> [c>>32]) (Const32 <config.fe.TypeUInt32()> [int64(int32(c))]))

(Eq64 x y) ->
	(AndB
		(Eq32 (Int64Hi x) (Int64Hi y))
		(Eq32 (Int64Lo x) (Int64Lo y)))

(Neq64 x y) ->
	(OrB
		(Neq32 (Int64Hi x) (Int64Hi y))
		(Neq32 (Int64Lo x) (Int64Lo y)))

(Less64U x y) ->
	(OrB
		(Less32U (Int64Hi x) (Int64Hi y))
		(AndB
			(Eq32 (Int64Hi x) (Int64Hi y))
			(Less32U (Int64Lo x) (Int64Lo y))))

(Leq64U x y) ->
	(OrB
		(Less32U (Int64Hi x) (Int64Hi y))
		(AndB
			(Eq32 (Int64Hi x) (Int64Hi y))
			(Leq32U (Int64Lo x) (Int64Lo y))))

(Greater64U x y) ->
	(OrB
		(Greater32U (Int64Hi x) (Int64Hi y))
		(AndB
			(Eq32 (Int64Hi x) (Int64Hi y))
			(Greater32U (Int64Lo x) (Int64Lo y))))

(Geq64U x y) ->
	(OrB
		(Greater32U (Int64Hi x) (Int64Hi y))
		(AndB
			(Eq32 (Int64Hi x) (Int64Hi y))
			(Geq32U (Int64Lo x) (Int64Lo y))))

(Less64 x y) ->
	(OrB
		(Less32 (Int64Hi x) (Int64Hi y))
		(AndB
			(Eq32 (Int64Hi x) (Int64Hi y))
			(Less32U (Int64Lo x) (Int64Lo y))))

(Leq64 x y) ->
	(OrB
		(Less32 (Int64Hi x) (Int64Hi y))
		(AndB
			(Eq32 (Int64Hi x) (Int64Hi y))
			(Leq32U (Int64Lo x) (Int64Lo y))))

(Greater64 x y) ->
	(OrB
		(Greater32 (Int64Hi x) (Int64Hi y))
		(AndB
			(Eq32 (Int64Hi x) (Int64Hi y))
			(Greater32U (Int64Lo x) (Int64Lo y))))

(Geq64 x y) ->
	(OrB
		(Greater32 (Int64Hi x) (Int64Hi y))
		(AndB
			(Eq32 (Int64Hi x) (Int64Hi y))
			(Geq32U (Int64Lo x) (Int64Lo y))))