diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 10:36:12 +0200 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 10:36:12 +0200 |
| commit | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (patch) | |
| tree | 12e8931a4a56da1a1bdfb89d670f4ba38fe08e1f /kernel/nativevalues.ml | |
| parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) | |
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
Diffstat (limited to 'kernel/nativevalues.ml')
| -rw-r--r-- | kernel/nativevalues.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index d7a21950..e4a77999 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -370,6 +370,11 @@ type coq_pair = | Paccu of t | PPair of t * t +type coq_zn2z = + | Zaccu of t + | ZW0 + | ZWW of t * t + let mkCarry b i = if b then (Obj.magic (C1(of_uint i)):t) else (Obj.magic (C0(of_uint i)):t) @@ -413,8 +418,13 @@ let subcarryc accu x y = let of_pair (x, y) = (Obj.magic (PPair(of_uint x, of_uint y)):t) +let zn2z_of_pair (x,y) = + if Uint31.equal x (Uint31.of_uint 0) && + Uint31.equal y (Uint31.of_uint 0) then Obj.magic ZW0 + else (Obj.magic (ZWW(of_uint x, of_uint y)) : t) + let no_check_mulc x y = - of_pair(Uint31.mulc (to_uint x) (to_uint y)) + zn2z_of_pair(Uint31.mulc (to_uint x) (to_uint y)) let mulc accu x y = if is_int x && is_int y then no_check_mulc x y |