From c878a5e2c0c2a01512e263d3ed2dfdd8e611086f Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 25 Jun 2019 09:10:44 +0000 Subject: [Extraction] Add support for primitive integers The ExtrOCamlInt63 module can be required to map primitives from the Int63 module to their OCaml implementation (module Uint63 from the kernel). --- doc/changelog/08-tools/10430-extraction-int63.rst | 5 +++ doc/sphinx/language/gallina-extensions.rst | 19 ++++++--- doc/stdlib/hidden-files | 1 + plugins/extraction/ExtrOCamlInt63.v | 52 +++++++++++++++++++++++ 4 files changed, 72 insertions(+), 5 deletions(-) create mode 100644 doc/changelog/08-tools/10430-extraction-int63.rst create mode 100644 plugins/extraction/ExtrOCamlInt63.v diff --git a/doc/changelog/08-tools/10430-extraction-int63.rst b/doc/changelog/08-tools/10430-extraction-int63.rst new file mode 100644 index 0000000000..68ae4591a4 --- /dev/null +++ b/doc/changelog/08-tools/10430-extraction-int63.rst @@ -0,0 +1,5 @@ +- Fix extraction to OCaml of primitive machine integers; + see :ref:`primitive-integers` + (`#10430 `_, + fixes `#10361 `_, + by Vincent Laporte). diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index c93984661e..070fc44775 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2443,11 +2443,20 @@ The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement dedicated, efficient, rules to reduce the applications of these primitive operations. -These primitives, when extracted to OCaml (see :ref:`extraction`), are mapped to -types and functions of a :g:`Uint63` module. Said module is not produced by -extraction. Instead, it has to be provided by the user (if they want to compile -or execute the extracted code). For instance, an implementation of this module -can be taken from the kernel of Coq. +The extraction of these primitives can be customized similarly to the extraction +of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlInt63` +module can be used when extracting to OCaml: it maps the Coq primitives to types +and functions of a :g:`Uint63` module (excepted :g:`addc`, :g:`addcarryc`, +:g:`subc`, :g:`subcarryc`, and :g:`diveucl` whose implementation in OCaml is +left to the reader). Said OCaml module is not produced by extraction. Instead, +it has to be provided by the user (if they want to compile or execute the +extracted code). For instance, an implementation of this module can be taken +from the kernel of Coq. + +Literal values (at type :g:`Int63.int`) are extracted to literal OCaml values +wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on +64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the +function :g:`Uint63.compile` from the kernel). Bidirectionality hints ---------------------- diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index b25104ddb9..46175e37ed 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -12,6 +12,7 @@ plugins/extraction/ExtrHaskellZInteger.v plugins/extraction/ExtrHaskellZNum.v plugins/extraction/ExtrOcamlBasic.v plugins/extraction/ExtrOcamlBigIntConv.v +plugins/extraction/ExtrOCamlInt63.v plugins/extraction/ExtrOcamlIntConv.v plugins/extraction/ExtrOcamlNatBigInt.v plugins/extraction/ExtrOcamlNatInt.v diff --git a/plugins/extraction/ExtrOCamlInt63.v b/plugins/extraction/ExtrOCamlInt63.v new file mode 100644 index 0000000000..b0e918c013 --- /dev/null +++ b/plugins/extraction/ExtrOCamlInt63.v @@ -0,0 +1,52 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* bool [ true false ]. +Extract Inductive prod => "( * )" [ "" ]. +Extract Inductive comparison => int [ "0" "(-1)" "1" ]. + +(** Primitive types and operators. *) +Extract Constant Int63.int => "Uint63.t". +Extraction Inline Int63.int. +(* Otherwise, the name conflicts with the primitive OCaml type [int] *) + +Extract Constant Int63.lsl => "Uint63.l_sl". +Extract Constant Int63.lsr => "Uint63.l_sr". +Extract Constant Int63.land => "Uint63.l_and". +Extract Constant Int63.lor => "Uint63.l_or". +Extract Constant Int63.lxor => "Uint63.l_xor". + +Extract Constant Int63.add => "Uint63.add". +Extract Constant Int63.sub => "Uint63.sub". +Extract Constant Int63.mul => "Uint63.mul". +Extract Constant Int63.mulc => "Uint63.mulc". +Extract Constant Int63.div => "Uint63.div". +Extract Constant Int63.mod => "Uint63.rem". + +Extract Constant Int63.eqb => "Uint63.equal". +Extract Constant Int63.ltb => "Uint63.lt". +Extract Constant Int63.leb => "Uint63.le". + +(* TODO: a few primitive operations have no implementation in the kernel module +Uint63. Namely addc, addcarryc, subc, subcarryc, and diveucl. *) + +Extract Constant Int63.diveucl_21 => "Uint63.div21". +Extract Constant Int63.addmuldiv => "Uint63.addmuldiv". + +Extract Constant Int63.compare => "Uint63.compare". + +Extract Constant Int63.head0 => "Uint63.head0". +Extract Constant Int63.tail0 => "Uint63.tail0". -- cgit v1.2.3 From 8675b9d1a574aceb9a9d40c9c135db9c042e00b1 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 22 Jul 2019 12:47:53 +0000 Subject: [Int63] Implement all primitives in OCaml Primitive operations addc, addcarryc, subc, subcarryc, and diveucl are implemented in the kernel so that they can be used by OCaml code (e.g., extracted code) as the other primitives. --- doc/sphinx/language/gallina-extensions.rst | 10 ++++------ kernel/uint63.mli | 12 ++++++++++++ kernel/uint63_amd64_63.ml | 23 +++++++++++++++++++++++ kernel/uint63_i386_31.ml | 23 +++++++++++++++++++++++ plugins/extraction/ExtrOCamlInt63.v | 8 ++++++-- 5 files changed, 68 insertions(+), 8 deletions(-) diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 070fc44775..acf68e9fd2 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2446,12 +2446,10 @@ operations. The extraction of these primitives can be customized similarly to the extraction of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlInt63` module can be used when extracting to OCaml: it maps the Coq primitives to types -and functions of a :g:`Uint63` module (excepted :g:`addc`, :g:`addcarryc`, -:g:`subc`, :g:`subcarryc`, and :g:`diveucl` whose implementation in OCaml is -left to the reader). Said OCaml module is not produced by extraction. Instead, -it has to be provided by the user (if they want to compile or execute the -extracted code). For instance, an implementation of this module can be taken -from the kernel of Coq. +and functions of a :g:`Uint63` module. Said OCaml module is not produced by +extraction. Instead, it has to be provided by the user (if they want to compile +or execute the extracted code). For instance, an implementation of this module +can be taken from the kernel of Coq. Literal values (at type :g:`Int63.int`) are extracted to literal OCaml values wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on diff --git a/kernel/uint63.mli b/kernel/uint63.mli index 93632da110..5542716af2 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -37,6 +37,8 @@ val mul : t -> t -> t val div : t -> t -> t val rem : t -> t -> t +val diveucl : t -> t -> t * t + (* Specific arithmetic operations *) val mulc : t -> t -> t * t val addmuldiv : t -> t -> t -> t @@ -57,3 +59,13 @@ val head0 : t -> t val tail0 : t -> t val is_uint63 : Obj.t -> bool + +(* Arithmetic with explicit carries *) + +(* Analog of Numbers.Abstract.Cyclic.carry *) +type 'a carry = C0 of 'a | C1 of 'a + +val addc : t -> t -> t carry +val addcarryc : t -> t -> t carry +val subc : t -> t -> t carry +val subcarryc : t -> t -> t carry diff --git a/kernel/uint63_amd64_63.ml b/kernel/uint63_amd64_63.ml index 20b2f58496..d6b077a9f5 100644 --- a/kernel/uint63_amd64_63.ml +++ b/kernel/uint63_amd64_63.ml @@ -82,6 +82,8 @@ let div (x : int) (y : int) = let rem (x : int) (y : int) = if y = 0 then 0 else Int64.to_int (Int64.rem (to_uint64 x) (to_uint64 y)) +let diveucl x y = (div x y, rem x y) + let addmuldiv p x y = l_or (l_sl x p) (l_sr y (uint_size - p)) @@ -225,3 +227,24 @@ let tail0 x = let is_uint63 t = Obj.is_int t [@@ocaml.inline always] + +(* Arithmetic with explicit carries *) + +(* Analog of Numbers.Abstract.Cyclic.carry *) +type 'a carry = C0 of 'a | C1 of 'a + +let addc x y = + let r = x + y in + if lt r x then C1 r else C0 r + +let addcarryc x y = + let r = x + y + 1 in + if le r x then C1 r else C0 r + +let subc x y = + let r = x - y in + if le y x then C0 r else C1 r + +let subcarryc x y = + let r = x - y - 1 in + if lt y x then C0 r else C1 r diff --git a/kernel/uint63_i386_31.ml b/kernel/uint63_i386_31.ml index c3279779e1..2a3fc75ec1 100644 --- a/kernel/uint63_i386_31.ml +++ b/kernel/uint63_i386_31.ml @@ -83,6 +83,8 @@ let div x y = let rem x y = if y = 0L then 0L else Int64.rem x y +let diveucl x y = (div x y, rem x y) + let addmuldiv p x y = l_or (l_sl x p) (l_sr y Int64.(sub (of_int uint_size) p)) @@ -191,6 +193,27 @@ let is_uint63 t = Obj.is_block t && Int.equal (Obj.tag t) Obj.custom_tag && le (Obj.magic t) maxuint63 +(* Arithmetic with explicit carries *) + +(* Analog of Numbers.Abstract.Cyclic.carry *) +type 'a carry = C0 of 'a | C1 of 'a + +let addc x y = + let r = add x y in + if lt r x then C1 r else C0 r + +let addcarryc x y = + let r = addcarry x y in + if le r x then C1 r else C0 r + +let subc x y = + let r = sub x y in + if le y x then C0 r else C1 r + +let subcarryc x y = + let r = subcarry x y in + if lt y x then C0 r else C1 r + (* Register all exported functions so that they can be called from C code *) let () = diff --git a/plugins/extraction/ExtrOCamlInt63.v b/plugins/extraction/ExtrOCamlInt63.v index b0e918c013..a2ee602313 100644 --- a/plugins/extraction/ExtrOCamlInt63.v +++ b/plugins/extraction/ExtrOCamlInt63.v @@ -17,6 +17,7 @@ From Coq Require Int63 Extraction. Extract Inductive bool => bool [ true false ]. Extract Inductive prod => "( * )" [ "" ]. Extract Inductive comparison => int [ "0" "(-1)" "1" ]. +Extract Inductive DoubleType.carry => "Uint63.carry" [ "Uint63.C0" "Uint63.C1" ]. (** Primitive types and operators. *) Extract Constant Int63.int => "Uint63.t". @@ -40,9 +41,12 @@ Extract Constant Int63.eqb => "Uint63.equal". Extract Constant Int63.ltb => "Uint63.lt". Extract Constant Int63.leb => "Uint63.le". -(* TODO: a few primitive operations have no implementation in the kernel module -Uint63. Namely addc, addcarryc, subc, subcarryc, and diveucl. *) +Extract Constant Int63.addc => "Uint63.addc". +Extract Constant Int63.addcarryc => "Uint63.addcarryc". +Extract Constant Int63.subc => "Uint63.subc". +Extract Constant Int63.subcarryc => "Uint63.subcarryc". +Extract Constant Int63.diveucl => "Uint63.diveucl". Extract Constant Int63.diveucl_21 => "Uint63.div21". Extract Constant Int63.addmuldiv => "Uint63.addmuldiv". -- cgit v1.2.3