Extract smodB.

src/Extract.v

@@ -20,7 +20,7 @@ Extraction "extracted"
          rolB rorB shrB shrBB sarB sarBB shlB shlBB
          (* Arithmetic operations *)
          adcB addB carry_addB addB_ovf sbbB subB borrow_subB Saddo Ssubo
-         full_mul mulB Umulo Smulo udivB' uremB sdivB' sdivB sremB
+         full_mul mulB Umulo Smulo udivB' uremB sdivB' sdivB sremB smodB
          (* Comparison operations *)
          ltB leB gtB geB sltB sleB sgtB sgeB
          (* Testing operations *)

src/ocaml/extra.mli

@@ -1,53 +1,55 @@
 
-(* Converts Coq Z to ZArith Z. *)
+(** This module provides extra functions. *)
+
 val z_of_coqZ : Extracted.z -> Z.t
+(** Converts Coq Z to ZArith Z. *)
 
-(* Converts Zarith Z to Coq positive. *)
 val coqZ_of_z : Z.t -> Extracted.z
+(** Converts Zarith Z to Coq positive. *)
 
-(* Returns the unsigned value of a bit vector. *)
 val unsigned : Extracted.bits -> Z.t
+(** Returns the unsigned value of a bit vector. *)
 
-(* Returns the signed value of a bit vector. *)
 val signed : Extracted.bits -> Z.t
+(** Returns the signed value of a bit vector. *)
 
-(* Returns the bit vector of a Zarith Z. *)
 val bits_of_z : int -> Z.t -> Extracted.bits
+(** Returns the bit vector of a Zarith Z. *)
 
-(* Returns the string representation of a bit vector. MSB appears first. *)
 val string_of_bits : Extracted.bits -> string
+(** Returns the string representation of a bit vector. MSB appears first. *)
 
-(* Returns the bit vector represented as a binary string *)
 val bits_of_binary : string -> Extracted.bits
+(** Returns the bit vector represented as a binary string *)
 
-(* Returns the bit vector represented as a hex string *)
 val bits_of_hex : string -> Extracted.bits
+(** Returns the bit vector represented as a hex string *)
 
-(* Returns the bit vector represented as a numeric string. The bit width of
-   the result is minimal. If the numeric string is positive, the unsigned
-   value of the bit vector corresponds to the numeric string. If the numeric
-   string is negative, the signed value of the bit vector corresponds to the
-   numeric string. *)
 val bits_of_num : string -> Extracted.bits
+(** Returns the bit vector represented as a numeric string. The bit width of
+    the result is minimal. If the numeric string is positive, the unsigned
+    value of the bit vector corresponds to the numeric string. If the numeric
+    string is negative, the signed value of the bit vector corresponds to the
+    numeric string. *)
 
-(* Unsigned full multiplication. *)
 val umuljB : Extracted.bits -> Extracted.bits -> Extracted.bits
+(** Unsigned full multiplication. *)
 
-(* Signed full multiplication. *)
 val smuljB : Extracted.bits -> Extracted.bits -> Extracted.bits
+(** Signed full multiplication. *)
 
-(* Unsigned full multiplication. The first element of the result represents
-   high bits. The first element of the result represents low bits. Raises
-   Invalid_argument if the bit widths of the two inputs are different. *)
 val umullB : Extracted.bits -> Extracted.bits -> Extracted.bits * Extracted.bits
+(** Unsigned full multiplication. The first element of the result represents
+    high bits. The first element of the result represents low bits. Raises
+    Invalid_argument if the bit widths of the two inputs are different. *)
 
-(* Signed full multiplication. The first element of the result represents
-   high bits. The first element of the result represents low bits. Raises
-   Invalid_argument if the bit widths of the two inputs are different. *)
 val smullB : Extracted.bits -> Extracted.bits -> Extracted.bits * Extracted.bits
+(** Signed full multiplication. The first element of the result represents
+    high bits. The first element of the result represents low bits. Raises
+    Invalid_argument if the bit widths of the two inputs are different. *)
 
-(* Unsigned splitting. The results and the input have the same size. *)
 val usplB : Extracted.bits -> int -> Extracted.bits * Extracted.bits
+(** Unsigned splitting. The results and the input have the same size. *)
 
-(* Signed splitting. The results and the input have the same size. *)
 val ssplB : Extracted.bits -> int -> Extracted.bits * Extracted.bits
+(** Signed splitting. The results and the input have the same size. *)

src/ocaml/extracted.ml

@@ -1796,3 +1796,13 @@ let sremB bs1' bs2' =
   let bs1 = absB bs1' in
   let bs2 = absB bs2' in
   if msb bs1' then negB (snd (udivB bs1 bs2)) else snd (udivB bs1 bs2)
+
+(** val smodB : bits -> bits -> bits **)
+
+let smodB bs1 bs2 =
+  let r_sdiv = sremB bs1 bs2 in
+  if (||) (eq_op bool_eqType (Obj.magic msb bs1) (Obj.magic msb bs2))
+       (eq_op bitseq_eqType (Obj.magic r_sdiv)
+         (Obj.magic zeros (size0 r_sdiv)))
+  then r_sdiv
+  else addB r_sdiv bs2

src/ocaml/extracted.mli

@@ -528,3 +528,5 @@ val sdivB' : bits -> bits -> bits * bits
 val sdivB : bits -> bits -> bits
 
 val sremB : bits -> bits -> bits
+
+val smodB : bits -> bits -> bits