Commit 18e48e16 by Jean-Christophe Filliâtre

### Int63: no more function eq (examples updated)

`hopefully fixing 'make bench' this time`
parent 9db4a5fe
 ... ... @@ -136,7 +136,7 @@ module N ensures { value result = to_int n } = let zero = of_int 0 in let a = if Int31.eq n zero then if n = zero then Array31.make zero zero else Array31.make (of_int 1) n ... ... @@ -231,7 +231,7 @@ module N let eq (x y:t) : bool requires { ok x /\ ok y } ensures { if result then value x = value y else value x <> value y } = Int31.eq (compare_array x.digits y.digits) (of_int 0) = compare_array x.digits y.digits = of_int 0 (** {2 arithmetic operations} *) ... ... @@ -277,7 +277,7 @@ module N if Int31.(>=) sum base31 then begin arr[!i] <- Int31.(-) sum base31; carry := one end else begin arr[!i] <- sum; carry := zero end; if Int31.ne arr[!i] zero then non_null_idx := !i; if arr[!i] <> zero then non_null_idx := !i; assert { MapEq.map_eq_sub arr.elts (arr at L).elts 0 (to_int !i) }; assert { value_sub arr.elts 0 (to_int !i) (to_int h + 1) = ... ... @@ -305,7 +305,7 @@ module N if Int31.(>=) sum base31 then begin arr[!i] <- Int31.(-) sum base31; carry := one end else begin arr[!i] <- sum; carry := zero end; if Int31.ne arr[!i] zero then non_null_idx := !i; if arr[!i] <> zero then non_null_idx := !i; assert { MapEq.map_eq_sub arr.elts (arr at L).elts 0 (to_int !i) }; assert { value_sub arr.elts 0 (to_int !i) (to_int h + 1) = ... ... @@ -324,7 +324,7 @@ module N ensures { to_int !non_null_idx >= 0 -> to_int arr[to_int !non_null_idx] <> 0 } ensures { forall j. to_int !non_null_idx < j <= to_int !i -> to_int arr[j] = 0 } (if Int31.ne arr[!i] zero then non_null_idx := !i) (if arr[!i] <> zero then non_null_idx := !i) end; let len = Int31.(+) !non_null_idx one in assert { value_sub arr.elts 0 (to_int !i + 1) (to_int h + 1) = ... ...
 ... ... @@ -252,7 +252,7 @@ module N invariant { value_sub x.elts (p2i !i) (p2i x2) = 0 } variant { p2i !i } i := Int31.(-) !i one; if Limb.ne x[!i] limb_zero then if not (Limb.(=) x[!i] limb_zero) then begin assert { l2i x[p2i !i] >= 1 }; assert { value_sub x.elts (p2i x1) (p2i !i + 1) >= ... ... @@ -325,7 +325,7 @@ module N let one = Int31.of_int 1 in let i = ref x1 in let c = ref y in while Int31.(<) !i x2 && Limb.ne !c limb_zero do while Int31.(<) !i x2 && not (Limb.(=) !c limb_zero) do invariant { forall j. 0 <= j < p2i x1 \/ p2i x2 <= j < p2i x.length -> x[j] = (old x)[j] } invariant { p2i x1 <= p2i !i <= p2i x2 } ... ... @@ -404,10 +404,10 @@ module N assert { value x + power radix (p2i lx) * l2i c = value (old x) + value_array y }; if Limb.eq c limb_zero then () else if Limb.(=) c limb_zero then () else begin (* we enlarge x *) if Int31.eq lx (of_int 0x3FFFFFFF) then raise TooManyDigits; if lx = of_int 0x3FFFFFFF then raise TooManyDigits; label L in enlarge x (Int31.(+) lx one); assert { l2i x.digits[p2i lx] = 0 }; ... ... @@ -435,7 +435,7 @@ module N let one = Int31.of_int 1 in let limb_zero = Limb.of_int 0 in let lx = x.length in if Int31.eq lx (of_int 0x3FFFFFFF) then raise TooManyDigits; if lx = of_int 0x3FFFFFFF then raise TooManyDigits; let r = Array31.make (Int31.(+) lx one) limb_zero in Array31.blit x zero r zero lx; assert { MapEq.map_eq_sub x.elts r.elts 0 (p2i lx) }; ... ...
 ... ... @@ -347,7 +347,7 @@ module N assert { 0 <= p2i !i < p2i sz }; lx := get_ofs x !i; ly := get_ofs y !i; if (UInt32.ne !lx !ly) if !lx <> !ly then begin value_sub_concat (pelts x) x.offset (x.offset+k) (x.offset+ p2i sz); value_sub_concat (pelts y) y.offset (y.offset+k) (y.offset+ p2i sz); ... ... @@ -411,7 +411,7 @@ module N i := Int32.(-) !i (Int32.of_int 1); assert { 0 <= p2i !i < p2i sz }; lx := get_ofs x !i; if (UInt32.ne !lx uzero) if !lx <> uzero then begin value_sub_concat (pelts x) x.offset (x.offset+k) (x.offset + p2i sz); value_sub_lower_bound_tight (pelts x) x.offset (x.offset+k); ... ... @@ -463,7 +463,7 @@ module N let c = ref y in let lx = ref limb_zero in let i = ref (Int32.of_int 0) in while Int32.(<) !i sz && UInt32.ne !c limb_zero do while Int32.(<) !i sz && !c <> limb_zero do invariant { 0 <= p2i !i <= p2i sz } invariant { p2i !i > 0 -> 0 <= l2i !c <= 1 } invariant { value_sub_shift r (p2i !i) + (power radix (p2i !i)) * l2i !c = ... ... @@ -499,7 +499,7 @@ module N done; assert { p2i !i = p2i sz \/ l2i !c = 0 }; assert { p2i !i < p2i sz -> l2i !c = 0 }; if Int32.eq !i sz then !c if !i = sz then !c else begin while Int32.(<) !i sz do invariant { l2i !c = 0 } ... ...
 ... ... @@ -562,9 +562,9 @@ this is true but with 2 different possible reasons: let n1 = of_int 1 in let n9 = of_int 9 in let n81 = of_int 81 in if Int31.eq i n81 then raise SolutionFound; if i = n81 then raise SolutionFound; (* assert { is_index i }; *) if not (Int31.eq g[i] n0) then if g[i] <> n0 then try (* assert { 1 <= t g[i] <= 9 }; *) check_valid_chunk g i s.column_start s.column_offsets; ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!