...

Text file src/cmd/compile/internal/ssa/_gen/dec64.rules

Documentation: cmd/compile/internal/ssa/_gen

     1// Copyright 2016 The Go Authors. All rights reserved.
     2// Use of this source code is governed by a BSD-style
     3// license that can be found in the LICENSE file.
     4
     5// This file contains rules to decompose [u]int64 types on 32-bit
     6// architectures. These rules work together with the decomposeBuiltIn
     7// pass which handles phis of these typ.
     8
     9(Int64Hi (Int64Make hi _)) => hi
    10(Int64Lo (Int64Make _ lo)) => lo
    11
    12(Load <t> ptr mem) && is64BitInt(t) && !config.BigEndian && t.IsSigned() =>
    13	(Int64Make
    14		(Load <typ.Int32> (OffPtr <typ.Int32Ptr> [4] ptr) mem)
    15		(Load <typ.UInt32> ptr mem))
    16
    17(Load <t> ptr mem) && is64BitInt(t) && !config.BigEndian && !t.IsSigned() =>
    18	(Int64Make
    19		(Load <typ.UInt32> (OffPtr <typ.UInt32Ptr> [4] ptr) mem)
    20		(Load <typ.UInt32> ptr mem))
    21
    22(Load <t> ptr mem) && is64BitInt(t) && config.BigEndian && t.IsSigned() =>
    23	(Int64Make
    24		(Load <typ.Int32> ptr mem)
    25		(Load <typ.UInt32> (OffPtr <typ.UInt32Ptr> [4] ptr) mem))
    26
    27(Load <t> ptr mem) && is64BitInt(t) && config.BigEndian && !t.IsSigned() =>
    28	(Int64Make
    29		(Load <typ.UInt32> ptr mem)
    30		(Load <typ.UInt32> (OffPtr <typ.UInt32Ptr> [4] ptr) mem))
    31
    32(Store {t} dst (Int64Make hi lo) mem) && t.Size() == 8 && !config.BigEndian =>
    33	(Store {hi.Type}
    34		(OffPtr <hi.Type.PtrTo()> [4] dst)
    35		hi
    36		(Store {lo.Type} dst lo mem))
    37
    38(Store {t} dst (Int64Make hi lo) mem) && t.Size() == 8 && config.BigEndian =>
    39	(Store {lo.Type}
    40		(OffPtr <lo.Type.PtrTo()> [4] dst)
    41		lo
    42		(Store {hi.Type} dst hi mem))
    43
    44// These are not enabled during decomposeBuiltin if late call expansion, but they are always enabled for softFloat
    45(Arg {n} [off]) && is64BitInt(v.Type) && !config.BigEndian && v.Type.IsSigned() && !(b.Func.pass.name == "decompose builtin") =>
    46  (Int64Make
    47    (Arg <typ.Int32> {n} [off+4])
    48    (Arg <typ.UInt32> {n} [off]))
    49(Arg {n} [off]) && is64BitInt(v.Type) && !config.BigEndian && !v.Type.IsSigned() && !(b.Func.pass.name == "decompose builtin")  =>
    50  (Int64Make
    51    (Arg <typ.UInt32> {n} [off+4])
    52    (Arg <typ.UInt32> {n} [off]))
    53
    54(Arg {n} [off]) && is64BitInt(v.Type) && config.BigEndian && v.Type.IsSigned() && !(b.Func.pass.name == "decompose builtin") =>
    55  (Int64Make
    56    (Arg <typ.Int32> {n} [off])
    57    (Arg <typ.UInt32> {n} [off+4]))
    58(Arg {n} [off]) && is64BitInt(v.Type) && config.BigEndian && !v.Type.IsSigned() && !(b.Func.pass.name == "decompose builtin") =>
    59  (Int64Make
    60    (Arg <typ.UInt32> {n} [off])
    61    (Arg <typ.UInt32> {n} [off+4]))
    62
    63(Add64 x y) =>
    64	(Int64Make
    65		(Add32withcarry <typ.Int32>
    66			(Int64Hi x)
    67			(Int64Hi y)
    68			(Select1 <types.TypeFlags> (Add32carry (Int64Lo x) (Int64Lo y))))
    69		(Select0 <typ.UInt32> (Add32carry (Int64Lo x) (Int64Lo y))))
    70
    71(Sub64 x y) =>
    72	(Int64Make
    73		(Sub32withcarry <typ.Int32>
    74			(Int64Hi x)
    75			(Int64Hi y)
    76			(Select1 <types.TypeFlags> (Sub32carry (Int64Lo x) (Int64Lo y))))
    77		(Select0 <typ.UInt32> (Sub32carry (Int64Lo x) (Int64Lo y))))
    78
    79(Mul64 x y) =>
    80	(Int64Make
    81		(Add32 <typ.UInt32>
    82			(Mul32 <typ.UInt32> (Int64Lo x) (Int64Hi y))
    83			(Add32 <typ.UInt32>
    84				(Mul32 <typ.UInt32> (Int64Hi x) (Int64Lo y))
    85				(Select0 <typ.UInt32> (Mul32uhilo (Int64Lo x) (Int64Lo y)))))
    86		(Select1 <typ.UInt32> (Mul32uhilo (Int64Lo x) (Int64Lo y))))
    87
    88(And64 x y) =>
    89	(Int64Make
    90		(And32 <typ.UInt32> (Int64Hi x) (Int64Hi y))
    91		(And32 <typ.UInt32> (Int64Lo x) (Int64Lo y)))
    92
    93(Or64 x y) =>
    94	(Int64Make
    95		(Or32 <typ.UInt32> (Int64Hi x) (Int64Hi y))
    96		(Or32 <typ.UInt32> (Int64Lo x) (Int64Lo y)))
    97
    98(Xor64 x y) =>
    99	(Int64Make
   100		(Xor32 <typ.UInt32> (Int64Hi x) (Int64Hi y))
   101		(Xor32 <typ.UInt32> (Int64Lo x) (Int64Lo y)))
   102
   103(Neg64 <t> x) => (Sub64 (Const64 <t> [0]) x)
   104
   105(Com64 x) =>
   106	(Int64Make
   107		(Com32 <typ.UInt32> (Int64Hi x))
   108		(Com32 <typ.UInt32> (Int64Lo x)))
   109
   110// Sadly, just because we know that x is non-zero,
   111// we don't know whether either component is,
   112// so just treat Ctz64NonZero the same as Ctz64.
   113(Ctz64NonZero ...) => (Ctz64 ...)
   114
   115(Ctz64 x) =>
   116	(Add32 <typ.UInt32>
   117		(Ctz32 <typ.UInt32> (Int64Lo x))
   118		(And32 <typ.UInt32>
   119			(Com32 <typ.UInt32> (Zeromask (Int64Lo x)))
   120			(Ctz32 <typ.UInt32> (Int64Hi x))))
   121
   122(BitLen64 x) =>
   123	(Add32 <typ.Int>
   124		(BitLen32 <typ.Int> (Int64Hi x))
   125		(BitLen32 <typ.Int>
   126			(Or32 <typ.UInt32>
   127				(Int64Lo x)
   128				(Zeromask (Int64Hi x)))))
   129
   130(Bswap64 x) =>
   131	(Int64Make
   132		(Bswap32 <typ.UInt32> (Int64Lo x))
   133		(Bswap32 <typ.UInt32> (Int64Hi x)))
   134
   135(SignExt32to64 x) => (Int64Make (Signmask x) x)
   136(SignExt16to64 x) => (SignExt32to64 (SignExt16to32 x))
   137(SignExt8to64 x) => (SignExt32to64 (SignExt8to32 x))
   138
   139(ZeroExt32to64 x) => (Int64Make (Const32 <typ.UInt32> [0]) x)
   140(ZeroExt16to64 x) => (ZeroExt32to64 (ZeroExt16to32 x))
   141(ZeroExt8to64 x) => (ZeroExt32to64 (ZeroExt8to32 x))
   142
   143(Trunc64to32 (Int64Make _ lo)) => lo
   144(Trunc64to16 (Int64Make _ lo)) => (Trunc32to16 lo)
   145(Trunc64to8 (Int64Make _ lo)) => (Trunc32to8 lo)
   146// Most general
   147(Trunc64to32 x) => (Int64Lo x)
   148(Trunc64to16 x) => (Trunc32to16 (Int64Lo x))
   149(Trunc64to8 x) => (Trunc32to8 (Int64Lo x))
   150
   151(Lsh32x64 _ (Int64Make (Const32 [c]) _)) && c != 0 => (Const32 [0])
   152(Rsh32x64 x (Int64Make (Const32 [c]) _)) && c != 0 => (Signmask x)
   153(Rsh32Ux64 _ (Int64Make (Const32 [c]) _)) && c != 0 => (Const32 [0])
   154(Lsh16x64 _ (Int64Make (Const32 [c]) _)) && c != 0 => (Const32 [0])
   155(Rsh16x64 x (Int64Make (Const32 [c]) _)) && c != 0 => (Signmask (SignExt16to32 x))
   156(Rsh16Ux64 _ (Int64Make (Const32 [c]) _)) && c != 0 => (Const32 [0])
   157(Lsh8x64 _ (Int64Make (Const32 [c]) _)) && c != 0 => (Const32 [0])
   158(Rsh8x64 x (Int64Make (Const32 [c]) _)) && c != 0 => (Signmask (SignExt8to32 x))
   159(Rsh8Ux64 _ (Int64Make (Const32 [c]) _)) && c != 0 => (Const32 [0])
   160
   161(Lsh32x64 [c] x (Int64Make (Const32 [0]) lo)) => (Lsh32x32 [c] x lo)
   162(Rsh32x64 [c] x (Int64Make (Const32 [0]) lo)) => (Rsh32x32 [c] x lo)
   163(Rsh32Ux64 [c] x (Int64Make (Const32 [0]) lo)) => (Rsh32Ux32 [c] x lo)
   164(Lsh16x64 [c] x (Int64Make (Const32 [0]) lo)) => (Lsh16x32 [c] x lo)
   165(Rsh16x64 [c] x (Int64Make (Const32 [0]) lo)) => (Rsh16x32 [c] x lo)
   166(Rsh16Ux64 [c] x (Int64Make (Const32 [0]) lo)) => (Rsh16Ux32 [c] x lo)
   167(Lsh8x64 [c] x (Int64Make (Const32 [0]) lo)) => (Lsh8x32 [c] x lo)
   168(Rsh8x64 [c] x (Int64Make (Const32 [0]) lo)) => (Rsh8x32 [c] x lo)
   169(Rsh8Ux64 [c] x (Int64Make (Const32 [0]) lo)) => (Rsh8Ux32 [c] x lo)
   170
   171(Lsh64x64 _ (Int64Make (Const32 [c]) _)) && c != 0 => (Const64 [0])
   172(Rsh64x64 x (Int64Make (Const32 [c]) _)) && c != 0 => (Int64Make (Signmask (Int64Hi x)) (Signmask (Int64Hi x)))
   173(Rsh64Ux64 _ (Int64Make (Const32 [c]) _)) && c != 0 => (Const64 [0])
   174
   175(Lsh64x64 [c] x (Int64Make (Const32 [0]) lo)) => (Lsh64x32 [c] x lo)
   176(Rsh64x64 [c] x (Int64Make (Const32 [0]) lo)) => (Rsh64x32 [c] x lo)
   177(Rsh64Ux64 [c] x (Int64Make (Const32 [0]) lo)) => (Rsh64Ux32 [c] x lo)
   178
   179// turn x64 non-constant shifts to x32 shifts
   180// if high 32-bit of the shift is nonzero, make a huge shift
   181(Lsh64x64 x (Int64Make hi lo)) && hi.Op != OpConst32 =>
   182       (Lsh64x32 x (Or32 <typ.UInt32> (Zeromask hi) lo))
   183(Rsh64x64 x (Int64Make hi lo)) && hi.Op != OpConst32 =>
   184       (Rsh64x32 x (Or32 <typ.UInt32> (Zeromask hi) lo))
   185(Rsh64Ux64 x (Int64Make hi lo)) && hi.Op != OpConst32 =>
   186       (Rsh64Ux32 x (Or32 <typ.UInt32> (Zeromask hi) lo))
   187(Lsh32x64 x (Int64Make hi lo)) && hi.Op != OpConst32 =>
   188       (Lsh32x32 x (Or32 <typ.UInt32> (Zeromask hi) lo))
   189(Rsh32x64 x (Int64Make hi lo)) && hi.Op != OpConst32 =>
   190       (Rsh32x32 x (Or32 <typ.UInt32> (Zeromask hi) lo))
   191(Rsh32Ux64 x (Int64Make hi lo)) && hi.Op != OpConst32 =>
   192       (Rsh32Ux32 x (Or32 <typ.UInt32> (Zeromask hi) lo))
   193(Lsh16x64 x (Int64Make hi lo)) && hi.Op != OpConst32 =>
   194       (Lsh16x32 x (Or32 <typ.UInt32> (Zeromask hi) lo))
   195(Rsh16x64 x (Int64Make hi lo)) && hi.Op != OpConst32 =>
   196       (Rsh16x32 x (Or32 <typ.UInt32> (Zeromask hi) lo))
   197(Rsh16Ux64 x (Int64Make hi lo)) && hi.Op != OpConst32 =>
   198       (Rsh16Ux32 x (Or32 <typ.UInt32> (Zeromask hi) lo))
   199(Lsh8x64 x (Int64Make hi lo)) && hi.Op != OpConst32 =>
   200       (Lsh8x32 x (Or32 <typ.UInt32> (Zeromask hi) lo))
   201(Rsh8x64 x (Int64Make hi lo)) && hi.Op != OpConst32 =>
   202       (Rsh8x32 x (Or32 <typ.UInt32> (Zeromask hi) lo))
   203(Rsh8Ux64 x (Int64Make hi lo)) && hi.Op != OpConst32 =>
   204       (Rsh8Ux32 x (Or32 <typ.UInt32> (Zeromask hi) lo))
   205
   206// Most general
   207(Lsh64x64 x y)  => (Lsh64x32  x (Or32 <typ.UInt32> (Zeromask (Int64Hi y)) (Int64Lo y)))
   208(Rsh64x64 x y)  => (Rsh64x32  x (Or32 <typ.UInt32> (Zeromask (Int64Hi y)) (Int64Lo y)))
   209(Rsh64Ux64 x y) => (Rsh64Ux32 x (Or32 <typ.UInt32> (Zeromask (Int64Hi y)) (Int64Lo y)))
   210(Lsh32x64 x y)  => (Lsh32x32  x (Or32 <typ.UInt32> (Zeromask (Int64Hi y)) (Int64Lo y)))
   211(Rsh32x64 x y)  => (Rsh32x32  x (Or32 <typ.UInt32> (Zeromask (Int64Hi y)) (Int64Lo y)))
   212(Rsh32Ux64 x y) => (Rsh32Ux32 x (Or32 <typ.UInt32> (Zeromask (Int64Hi y)) (Int64Lo y)))
   213(Lsh16x64 x y)  => (Lsh16x32  x (Or32 <typ.UInt32> (Zeromask (Int64Hi y)) (Int64Lo y)))
   214(Rsh16x64 x y)  => (Rsh16x32  x (Or32 <typ.UInt32> (Zeromask (Int64Hi y)) (Int64Lo y)))
   215(Rsh16Ux64 x y) => (Rsh16Ux32 x (Or32 <typ.UInt32> (Zeromask (Int64Hi y)) (Int64Lo y)))
   216(Lsh8x64 x y)   => (Lsh8x32   x (Or32 <typ.UInt32> (Zeromask (Int64Hi y)) (Int64Lo y)))
   217(Rsh8x64 x y)   => (Rsh8x32   x (Or32 <typ.UInt32> (Zeromask (Int64Hi y)) (Int64Lo y)))
   218(Rsh8Ux64 x y)  => (Rsh8Ux32  x (Or32 <typ.UInt32> (Zeromask (Int64Hi y)) (Int64Lo y)))
   219
   220(RotateLeft64 x (Int64Make hi lo)) => (RotateLeft64 x lo)
   221(RotateLeft32 x (Int64Make hi lo)) => (RotateLeft32 x lo)
   222(RotateLeft16 x (Int64Make hi lo)) => (RotateLeft16 x lo)
   223(RotateLeft8  x (Int64Make hi lo)) => (RotateLeft8  x lo)
   224
   225// Clean up constants a little
   226(Or32 <typ.UInt32> (Zeromask (Const32 [c])) y) && c == 0 => y
   227(Or32 <typ.UInt32> (Zeromask (Const32 [c])) y) && c != 0 => (Const32 <typ.UInt32> [-1])
   228
   229// 64x left shift
   230// result.hi = hi<<s | lo>>(32-s) | lo<<(s-32) // >> is unsigned, large shifts result 0
   231// result.lo = lo<<s
   232(Lsh64x32 x s) =>
   233	(Int64Make
   234		(Or32 <typ.UInt32>
   235			(Or32 <typ.UInt32>
   236				(Lsh32x32 <typ.UInt32> (Int64Hi x) s)
   237				(Rsh32Ux32 <typ.UInt32>
   238					(Int64Lo x)
   239					(Sub32 <typ.UInt32> (Const32 <typ.UInt32> [32]) s)))
   240			(Lsh32x32 <typ.UInt32>
   241				(Int64Lo x)
   242				(Sub32 <typ.UInt32> s (Const32 <typ.UInt32> [32]))))
   243		(Lsh32x32 <typ.UInt32> (Int64Lo x) s))
   244(Lsh64x16 x s) =>
   245	(Int64Make
   246		(Or32 <typ.UInt32>
   247			(Or32 <typ.UInt32>
   248				(Lsh32x16 <typ.UInt32> (Int64Hi x) s)
   249				(Rsh32Ux16 <typ.UInt32>
   250					(Int64Lo x)
   251					(Sub16 <typ.UInt16> (Const16 <typ.UInt16> [32]) s)))
   252			(Lsh32x16 <typ.UInt32>
   253				(Int64Lo x)
   254				(Sub16 <typ.UInt16> s (Const16 <typ.UInt16> [32]))))
   255		(Lsh32x16 <typ.UInt32> (Int64Lo x) s))
   256(Lsh64x8 x s) =>
   257	(Int64Make
   258		(Or32 <typ.UInt32>
   259			(Or32 <typ.UInt32>
   260				(Lsh32x8 <typ.UInt32> (Int64Hi x) s)
   261				(Rsh32Ux8 <typ.UInt32>
   262					(Int64Lo x)
   263					(Sub8 <typ.UInt8> (Const8 <typ.UInt8> [32]) s)))
   264			(Lsh32x8 <typ.UInt32>
   265				(Int64Lo x)
   266				(Sub8 <typ.UInt8> s (Const8 <typ.UInt8> [32]))))
   267		(Lsh32x8 <typ.UInt32> (Int64Lo x) s))
   268
   269// 64x unsigned right shift
   270// result.hi = hi>>s
   271// result.lo = lo>>s | hi<<(32-s) | hi>>(s-32) // >> is unsigned, large shifts result 0
   272(Rsh64Ux32 x s) =>
   273	(Int64Make
   274		(Rsh32Ux32 <typ.UInt32> (Int64Hi x) s)
   275		(Or32 <typ.UInt32>
   276			(Or32 <typ.UInt32>
   277				(Rsh32Ux32 <typ.UInt32> (Int64Lo x) s)
   278				(Lsh32x32 <typ.UInt32>
   279					(Int64Hi x)
   280					(Sub32 <typ.UInt32> (Const32 <typ.UInt32> [32]) s)))
   281			(Rsh32Ux32 <typ.UInt32>
   282				(Int64Hi x)
   283				(Sub32 <typ.UInt32> s (Const32 <typ.UInt32> [32])))))
   284(Rsh64Ux16 x s) =>
   285	(Int64Make
   286		(Rsh32Ux16 <typ.UInt32> (Int64Hi x) s)
   287		(Or32 <typ.UInt32>
   288			(Or32 <typ.UInt32>
   289				(Rsh32Ux16 <typ.UInt32> (Int64Lo x) s)
   290				(Lsh32x16 <typ.UInt32>
   291					(Int64Hi x)
   292					(Sub16 <typ.UInt16> (Const16 <typ.UInt16> [32]) s)))
   293			(Rsh32Ux16 <typ.UInt32>
   294				(Int64Hi x)
   295				(Sub16 <typ.UInt16> s (Const16 <typ.UInt16> [32])))))
   296(Rsh64Ux8 x s) =>
   297	(Int64Make
   298		(Rsh32Ux8 <typ.UInt32> (Int64Hi x) s)
   299		(Or32 <typ.UInt32>
   300			(Or32 <typ.UInt32>
   301				(Rsh32Ux8 <typ.UInt32> (Int64Lo x) s)
   302				(Lsh32x8 <typ.UInt32>
   303					(Int64Hi x)
   304					(Sub8 <typ.UInt8> (Const8 <typ.UInt8> [32]) s)))
   305			(Rsh32Ux8 <typ.UInt32>
   306				(Int64Hi x)
   307				(Sub8 <typ.UInt8> s (Const8 <typ.UInt8> [32])))))
   308
   309// 64x signed right shift
   310// result.hi = hi>>s
   311// result.lo = lo>>s | hi<<(32-s) | (hi>>(s-32))&zeromask(s>>5) // hi>>(s-32) is signed, large shifts result 0/-1
   312(Rsh64x32 x s) =>
   313	(Int64Make
   314		(Rsh32x32 <typ.UInt32> (Int64Hi x) s)
   315		(Or32 <typ.UInt32>
   316			(Or32 <typ.UInt32>
   317				(Rsh32Ux32 <typ.UInt32> (Int64Lo x) s)
   318				(Lsh32x32 <typ.UInt32>
   319					(Int64Hi x)
   320					(Sub32 <typ.UInt32> (Const32 <typ.UInt32> [32]) s)))
   321			(And32 <typ.UInt32>
   322				(Rsh32x32 <typ.UInt32>
   323					(Int64Hi x)
   324					(Sub32 <typ.UInt32> s (Const32 <typ.UInt32> [32])))
   325				(Zeromask
   326					(Rsh32Ux32 <typ.UInt32> s (Const32 <typ.UInt32> [5]))))))
   327(Rsh64x16 x s) =>
   328	(Int64Make
   329		(Rsh32x16 <typ.UInt32> (Int64Hi x) s)
   330		(Or32 <typ.UInt32>
   331			(Or32 <typ.UInt32>
   332				(Rsh32Ux16 <typ.UInt32> (Int64Lo x) s)
   333				(Lsh32x16 <typ.UInt32>
   334					(Int64Hi x)
   335					(Sub16 <typ.UInt16> (Const16 <typ.UInt16> [32]) s)))
   336			(And32 <typ.UInt32>
   337				(Rsh32x16 <typ.UInt32>
   338					(Int64Hi x)
   339					(Sub16 <typ.UInt16> s (Const16 <typ.UInt16> [32])))
   340				(Zeromask
   341					(ZeroExt16to32
   342						(Rsh16Ux32 <typ.UInt16> s (Const32 <typ.UInt32> [5])))))))
   343(Rsh64x8 x s) =>
   344	(Int64Make
   345		(Rsh32x8 <typ.UInt32> (Int64Hi x) s)
   346		(Or32 <typ.UInt32>
   347			(Or32 <typ.UInt32>
   348				(Rsh32Ux8 <typ.UInt32> (Int64Lo x) s)
   349				(Lsh32x8 <typ.UInt32>
   350					(Int64Hi x)
   351					(Sub8 <typ.UInt8> (Const8 <typ.UInt8> [32]) s)))
   352			(And32 <typ.UInt32>
   353				(Rsh32x8 <typ.UInt32>
   354					(Int64Hi x)
   355					(Sub8 <typ.UInt8> s (Const8 <typ.UInt8> [32])))
   356				(Zeromask
   357					(ZeroExt8to32
   358						(Rsh8Ux32 <typ.UInt8> s (Const32 <typ.UInt32> [5])))))))
   359
   360(Const64 <t> [c]) && t.IsSigned() =>
   361	(Int64Make (Const32 <typ.Int32> [int32(c>>32)]) (Const32 <typ.UInt32> [int32(c)]))
   362(Const64 <t> [c]) && !t.IsSigned() =>
   363	(Int64Make (Const32 <typ.UInt32> [int32(c>>32)]) (Const32 <typ.UInt32> [int32(c)]))
   364
   365(Eq64 x y) =>
   366	(AndB
   367		(Eq32 (Int64Hi x) (Int64Hi y))
   368		(Eq32 (Int64Lo x) (Int64Lo y)))
   369
   370(Neq64 x y) =>
   371	(OrB
   372		(Neq32 (Int64Hi x) (Int64Hi y))
   373		(Neq32 (Int64Lo x) (Int64Lo y)))
   374
   375(Less64U x y) =>
   376	(OrB
   377		(Less32U (Int64Hi x) (Int64Hi y))
   378		(AndB
   379			(Eq32 (Int64Hi x) (Int64Hi y))
   380			(Less32U (Int64Lo x) (Int64Lo y))))
   381
   382(Leq64U x y) =>
   383	(OrB
   384		(Less32U (Int64Hi x) (Int64Hi y))
   385		(AndB
   386			(Eq32 (Int64Hi x) (Int64Hi y))
   387			(Leq32U (Int64Lo x) (Int64Lo y))))
   388
   389(Less64 x y) =>
   390	(OrB
   391		(Less32 (Int64Hi x) (Int64Hi y))
   392		(AndB
   393			(Eq32 (Int64Hi x) (Int64Hi y))
   394			(Less32U (Int64Lo x) (Int64Lo y))))
   395
   396(Leq64 x y) =>
   397	(OrB
   398		(Less32 (Int64Hi x) (Int64Hi y))
   399		(AndB
   400			(Eq32 (Int64Hi x) (Int64Hi y))
   401			(Leq32U (Int64Lo x) (Int64Lo y))))

View as plain text