diff options
| author | Vincent Laporte | 2019-07-22 12:47:53 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-07-22 13:02:49 +0000 |
| commit | 8675b9d1a574aceb9a9d40c9c135db9c042e00b1 (patch) | |
| tree | b5f5ce6497ab70344fed0966d59ea78cf122dff9 /plugins | |
| parent | c878a5e2c0c2a01512e263d3ed2dfdd8e611086f (diff) | |
[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.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/ExtrOCamlInt63.v | 8 |
1 files changed, 6 insertions, 2 deletions
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". |