Commit 03d30160 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix extraction of ocaml32/mach.int.UInt32.

parent 77a7ca18
...@@ -47,20 +47,20 @@ module mach.int.UInt32 ...@@ -47,20 +47,20 @@ module mach.int.UInt32
syntax val (>=) "(>=)" syntax val (>=) "(>=)"
syntax val (>) "(>)" syntax val (>) "(>)"
(* direct realization of add_with_carry, mul_with_carry, fused_mul_add. (* direct realization of add_with_carry, add3, mul_with_carry.
Remember that parameters x y and c are assumed to denote unsigned integers Remember that parameters are assumed to denote unsigned integers
less than 2^{32} *) less than 2^{32} *)
syntax val add_with_carry "(fun x y c -> syntax val add_with_carry "(fun x y c ->
let r = Int64.add x (Int64.add y c) in let r = Int64.add x (Int64.add y c) in
(Int64.logand r 0xFFFFFFFFL,Int64.shift_right_logical r 32))" (Int64.logand r 0xFFFFFFFFL,Int64.shift_right_logical r 32))"
syntax val mul_with_carry "(fun x y -> syntax val add3 "(fun x y z ->
let r = Int64.mul x y in let r = Int64.add x (Int64.add y z) in
(Int64.logand r 0xFFFFFFFFL,Int64.shift_right_logical r 32))" (Int64.logand r 0xFFFFFFFFL,Int64.shift_right_logical r 32))"
syntax val fused_mul_add "(fun x y c -> syntax val mul_double "(fun x y ->
let r = Int64.add (Int64.mul x y) c in let r = Int64.mul x y in
(Int64.logand r 0xFFFFFFFFL,Int64.shift_right_logical r 32))" (Int64.logand r 0xFFFFFFFFL,Int64.shift_right_logical r 32))"
end end
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment