Replace abstract bounded integers by range types.

drivers/ocaml64.drv

@@ -210,8 +210,8 @@ module mach.int.Int63
   syntax literal   int63    "%1"
   syntax converter of_int   "%1"
 
-  syntax val      of_int    "Z.to_int %1"
-  syntax function to_int    "Z.of_int %1"
+  syntax val of_int "Z.to_int %1"
+  syntax val to_int "Z.of_int %1"
 
   syntax constant min_int63 "Z.of_int min_int"
   syntax constant max_int63 "Z.of_int max_int"

modules/mach/int.mlw

@@ -44,9 +44,12 @@ module Bounded_int
   constant min : int
   constant max : int
 
-  val function to_int (n:t) : int
+  function to_int (n:t) : int
   meta coercion function to_int
 
+  val to_int (n:t) : int
+    ensures { result = n }
+
   predicate in_bounds (n:int) = min <= n <= max
 
   axiom to_int_in_bounds: forall n:t. in_bounds n
@@ -140,15 +143,19 @@ module Int31
 
   use import int.Int
 
-  type int31
+  type int31 = < range -0x4000_0000 0x3fff_ffff >
 
-  let constant min_int31 : int = - 0x40000000
-  let constant max_int31 : int =   0x3fffffff
+  let constant min_int31 : int = - 0x4000_0000
+  let constant max_int31 : int =   0x3fff_ffff
+  function to_int (x : int31) : int = int31'int x
 
   clone export Bounded_int with
     type t = int31,
-    constant min = min_int31,
-    constant max = max_int31
+    constant min = int31'minInt,
+    constant max = int31'maxInt,
+    function to_int = int31'int,
+    lemma to_int_in_bounds,
+    lemma extensionality
 
 (*  use bv.BV31
 
@@ -163,15 +170,19 @@ module Int32
 
   use import int.Int
 
-  type int32
+  type int32 = < range -0x8000_0000 0x7fff_ffff >
 
-  let constant min_int32 : int = - 0x80000000
-  let constant max_int32 : int =   0x7fffffff
+  let constant min_int32 : int = - 0x8000_0000
+  let constant max_int32 : int =   0x7fff_ffff
+  function to_int (x : int32) : int = int32'int x
 
   clone export Bounded_int with
     type t = int32,
-    constant min = min_int32,
-    constant max = max_int32
+    constant min = int32'minInt,
+    constant max = int32'maxInt,
+    function to_int = int32'int,
+    lemma to_int_in_bounds,
+    lemma extensionality
 
   use bv.BV32
 
@@ -184,13 +195,20 @@ end
 
 module UInt32
 
-  type uint32
+  use import int.Int
+
+  type uint32 = < range 0 0xffff_ffff >
 
-  let constant max_uint32 : int = 0xffffffff
+  let constant max_uint32 : int = 0xffff_ffff
+  function to_int (x : uint32) : int = uint32'int x
 
   clone export Unsigned with
     type t = uint32,
-    constant max = max_uint32
+    constant max = uint32'maxInt,
+    function to_int = uint32'int,
+    lemma zero_unsigned_is_zero,
+    lemma to_int_in_bounds,
+    lemma extensionality
 
 (*  use bv.BV32
 
@@ -205,15 +223,19 @@ module Int63
 
   use import int.Int
 
-  type int63
+  type int63 = < range -0x4000_0000_0000_0000 0x3fff_ffff_ffff_ffff >
 
-  let constant min_int63 : int = - 0x4000000000000000
-  let constant max_int63 : int =   0x3fffffffffffffff
+  let constant min_int63 : int = - 0x4000_0000_0000_0000
+  let constant max_int63 : int =   0x3fff_ffff_ffff_ffff
+  function to_int (x : int63) : int = int63'int x
 
   clone export Bounded_int with
     type t = int63,
-    constant min = min_int63,
-    constant max = max_int63
+    constant min = int63'minInt,
+    constant max = int63'maxInt,
+    function to_int = int63'int,
+    lemma to_int_in_bounds,
+    lemma extensionality
 
   let constant zero = of_int 0
   let constant one = of_int 1
@@ -332,15 +354,19 @@ module Int64
 
   use import int.Int
 
-  type int64
+  type int64 = < range -0x8000_0000_0000_0000 0x7fff_ffff_ffff_ffff >
 
-  let constant min_int64 : int = - 0x8000000000000000
-  let constant max_int64 : int =   0x7fffffffffffffff
+  let constant min_int64 : int = - 0x8000_0000_0000_0000
+  let constant max_int64 : int =   0x7fff_ffff_ffff_ffff
+  function to_int (x : int64) : int = int64'int x
 
   clone export Bounded_int with
     type t = int64,
-    constant min = min_int64,
-    constant max = max_int64
+    constant min = int64'minInt,
+    constant max = int64'maxInt,
+    function to_int = int64'int,
+    lemma to_int_in_bounds,
+    lemma extensionality
 
 (*  use bv.BV64
 
@@ -355,13 +381,18 @@ module UInt64
 
   use import int.Int
 
-  type uint64
+  type uint64 = < range 0 0xffff_ffff_ffff_ffff >
 
-  constant max_uint64 : int =  0xffffffffffffffff
+  constant max_uint64 : int = uint64'maxInt
+  function to_int (x : uint64) : int = uint64'int x
 
   clone export Unsigned with
     type t = uint64,
-    constant max = max_uint64
+    constant max = uint64'maxInt,
+    function to_int = uint64'int,
+    lemma zero_unsigned_is_zero,
+    lemma to_int_in_bounds,
+    lemma extensionality
 
 (*  use bv.BV64
 

tests/test-extraction/main.ml

@@ -3,14 +3,14 @@
 
 open Test
 
+let () = assert (test_array   () = 42)
+
 let (=) = Z.equal
 
 let b42 = Z.of_int 42
 let () = assert (test_int     () = b42)
 let () = assert (test_int63   () = b42)
-
 let () = assert (test_ref     () = b42)
-let () = assert (test_array   () = b42)
 let () = assert (test_array63 () = b42)
 
 let () = main ()

tests/test_extraction.mlw

@@ -29,7 +29,7 @@ module TestExtraction
   use import array.Array
 
   let test_array () =
-    let a = Array.make 43 0 in
+    let a = Array.make 43 (0:int63) in
     for i = 1 to 42 do a[i] <- a[i-1] + 1 done;
     a[42]
 
@@ -134,7 +134,7 @@ module TestExtraction
 *)
   let constructor1 () =
     let x = Cons in
-    x 42
+    x (42:int63)
 
   let foofoo (x: int) : int =
     let ghost y = x + 1 in
@@ -162,7 +162,7 @@ module TestExtraction
   (* functions with ghost arguments *)
 
   let test_filter_ghost_args (x: int) (ghost y: int) =
-    1 / 0
+    (1:int) / 0
 
   let test_call (x: int) : int =
     test_filter_ghost_args x 0 + 1
@@ -180,7 +180,7 @@ module TestExtraction
   let many_args (a b c d e f g h i j k l m: int) : int = 42
 
   let foo (x: int) : int =
-    let _ = 42 in (* FIXME? print _ in OCaml *)
+    let _ = (42:int63) in (* FIXME? print _ in OCaml *)
     x
 
   let test_fun (x: int) : int -> int =
@@ -214,10 +214,12 @@ module TestExtraction
 
   (** for loops *)
 
+(*
   let for_loop1 () =
-    let r = ref 0 in
+    let r = ref (0:int63) in
     for i = 0 to 10 do r := !r + i done;
     !r
+*)
 
   (** optional and named arguments *)
 
@@ -239,7 +241,7 @@ module TestExtraction
   use import ocaml.Pervasives
 
   let test1 () raises { AssertFailure } =
-    ocaml_assert (1 + 1 = 2)
+    ocaml_assert ((1:int63) + 1 = 2)
 
   (** parallel assignement *)