From 85a99b576412c668f272c0cad3210e2bd2f0ec6a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= Date: Sun, 21 Jun 2026 16:09:31 +0000 Subject: [PATCH] ExtrOcamlZBigInt: Use shifts/masks to build and match `positive` values This is particularly valuable for FMapPositive and other structures like stdpp's Pmap that walk a binary number's encoding, because walks can now be done without general-purpose division. Micro-benchmark on OCaml 5.2.1+flambda: Name Time/Run mWd/Run FMapPositive.find x100k (stock) 88.04ms 17_403_012w FMapPositive.find x100k (shift+mask) 57.32ms 6w --- theories/extraction/ExtrOcamlZBigInt.v | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/theories/extraction/ExtrOcamlZBigInt.v b/theories/extraction/ExtrOcamlZBigInt.v index 2c7a1dec90..e3972e565c 100644 --- a/theories/extraction/ExtrOcamlZBigInt.v +++ b/theories/extraction/ExtrOcamlZBigInt.v @@ -27,12 +27,14 @@ Extraction Blacklist Z Big_int_Z. emulate the matching, see documentation of [Extract Inductive]. *) Extract Inductive positive => "Big_int_Z.big_int" - [ "(fun x -> Big_int_Z.succ_big_int (Big_int_Z.mult_int_big_int 2 x))" - "Big_int_Z.mult_int_big_int 2" "Big_int_Z.unit_big_int" ] + [ "(fun p -> Big_int_Z.succ_big_int (Big_int_Z.shift_left_big_int p 1))" + "(fun p -> Big_int_Z.shift_left_big_int p 1)" "Big_int_Z.unit_big_int" ] "(fun f2p1 f2p f1 p -> if Big_int_Z.le_big_int p Big_int_Z.unit_big_int then f1 () else - let (q,r) = Big_int_Z.quomod_big_int p (Big_int_Z.big_int_of_int 2) in - if Big_int_Z.eq_big_int r Big_int_Z.zero_big_int then f2p q else f2p1 q)". + let q = Big_int_Z.shift_right_big_int p 1 in + if Big_int_Z.eq_big_int (Big_int_Z.and_big_int p Big_int_Z.unit_big_int) + Big_int_Z.unit_big_int + then f2p1 q else f2p q)". Extract Inductive Z => "Big_int_Z.big_int" [ "Big_int_Z.zero_big_int" "" "Big_int_Z.minus_big_int" ]