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