Commit f428b633 authored by François Bobot's avatar François Bobot

Adds Peano.Int63 in ocaml64 driver

     and renames to_int63 into to_int63_partial
parent 06c4cb7c
...@@ -302,6 +302,12 @@ module mach.peano.MinMax ...@@ -302,6 +302,12 @@ module mach.peano.MinMax
syntax val min "min %1 %2" prec 4 3 3 syntax val min "min %1 %2" prec 4 3 3
end end
module mach.peano.Int63
syntax val defensive_to_int63 "%1"
syntax val to_int63 "%1"
syntax val of_int63 "%1"
end
module mach.onetime.OneTime module mach.onetime.OneTime
syntax type t "int" syntax type t "int"
syntax val to_int "Z.of_int %1" prec 4 3 syntax val to_int "Z.of_int %1" prec 4 3
......
...@@ -102,10 +102,19 @@ module MinMax ...@@ -102,10 +102,19 @@ module MinMax
end end
module Int63 module Int63
use int.Int
use mach.int.Int63 use mach.int.Int63
use Peano use Peano
val defensive_to_int63 (x:t) : int63
requires { Int63.in_bounds x.v }
ensures { result = x.v }
val partial to_int63 (x:t) : int63 val partial to_int63 (x:t) : int63
ensures { result = x.v } ensures { result = x.v }
val of_int63 (x:int63) (low high: t) : t
requires { low.v <= x <= high.v }
ensures { result.v = x }
end end
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