Commit 376f8e03 authored by MARCHE Claude's avatar MARCHE Claude

update drivers and example mp after last Why3 GT

parent 93f3d110
......@@ -29,6 +29,7 @@ module mach.int.UInt32
syntax converter of_int "%1"
syntax function to_int "(Why3__BigInt.of_int %1)"
syntax constant zero_unsigned "0"
syntax type uint32 "int"
syntax val ( + ) "( + )"
......@@ -43,6 +44,20 @@ module mach.int.UInt32
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
syntax val add_with_carry "(fun x y c ->
let r = x + y + c in
(r land 0xFFFFFFFF,r lsr 32))"
syntax val add3 "(fun x y z ->
let r = x + y + z in
(r land 0xFFFFFFFF,r lsr 32))"
syntax val mul_double "(fun x y ->
let r = Int64.mul (Int64.of_int x) (Int64.of_int y) in
(Int64.to_int (Int64.logand r 0xFFFFFFFFL),Int64.to_int (Int64.shift_right_logical r 32)))"
end
module mach.int.Int63
......
......@@ -44,7 +44,7 @@ module N
constant radix : int = Limb.max_uint32 + 1
(**)
(* *)
function l2i (x:limb) : int = Limb.to_int x
......@@ -508,8 +508,8 @@ module N
let zd = Array31.make (Int31.(+) lx ly) limb_zero in
assert { MapEq.map_eq_sub zd.elts (Map.const limb_zero) 0 (p2i lx + p2i ly) };
assert { value_sub zd.elts 0 (p2i lx + p2i ly) = 0 };
let c = mul_limbs zd x.digits y.digits zero zero lx zero ly in
assert { l2i c = 0 };
let _c = mul_limbs zd x.digits y.digits zero zero lx zero ly in
assert { l2i _c = 0 };
{ digits = zd }
end
......
......@@ -3,10 +3,10 @@
"http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>Javascript test for bigInt</title>
<title>Javascript test for mp</title>
</head>
<body id="test">
<h1>Javascript test for bigInt</h1>
<h1>Javascript test for mp</h1>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<script type="text/javascript" src="jsmain.js"></script>
</body>
......
......@@ -2,15 +2,18 @@
(* computation part *)
open Format
let compute_result text =
try
let a,i = Parse.parse_dec_ip text 0 in
let i = Parse.parse_sep_star text i in
let b,i = Parse.parse_dec_ip text i in
let m = Mp__N.mul a b in
Mp__N.add_in_place a b;
Parse.pr Format.str_formatter a;
Format.flush_str_formatter ()
fprintf str_formatter "addition = %a,@\nmultiplication = %a"
Parse.pr a Parse.pr m;
flush_str_formatter ()
with Parse.SyntaxError -> "syntax error"
(* HTML rendering *)
......@@ -22,7 +25,7 @@ let node x = (x : #Dom.node Js.t :> Dom.node Js.t)
let (<|) e l = List.iter (fun c -> Dom.appendChild e c) l; node e
let html_of_string (d : Html.document Js.t) (s:string) =
d##createElement (Js.string "p") <|
d##createElement (Js.string "pre") <|
[node (d##createTextNode (Js.string s))]
let replace_child p n =
......
......@@ -12,10 +12,10 @@ use import ref.Ref
type prdata = PrChar char | PrInt int
val flushed : ref (list (list prdata))
val current_line : ref (list prdata)
val cur_pos : ref int
val cur_linenum: ref int
val ghost flushed : ref (list (list prdata))
val ghost current_line : ref (list prdata)
val ghost cur_pos : ref int
val ghost cur_linenum: ref int
(** prints a character on standard output. *)
val print_char (c:char) : unit
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment