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).
---
 plugins/extraction/ExtrOCamlInt63.v | 52 +++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100644 plugins/extraction/ExtrOCamlInt63.v

(limited to 'plugins')

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       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Extraction to OCaml of native 63-bit machine integers. *)
+
+From Coq Require Int63 Extraction.
+
+(** Basic data types used by some primitive operators. *)
+
+Extract Inductive bool => 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.
---
 plugins/extraction/ExtrOCamlInt63.v | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'plugins')

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