File ‹gen_int.ML›
signature SPECCHECK_GEN_INT = sig
val pos : int -> int SpecCheck_Gen_Types.gen
val neg : int -> int SpecCheck_Gen_Types.gen
val nonneg : int -> int SpecCheck_Gen_Types.gen
val nonpos : int -> int SpecCheck_Gen_Types.gen
val coint : (int, 'b) SpecCheck_Gen_Types.cogen
end
structure SpecCheck_Gen_Int : SPECCHECK_GEN_INT =
struct
open SpecCheck_Gen_Base
fun pos m = range_int (1, m)
fun neg m = range_int (m, ~1)
fun nonneg m = range_int (0, m)
fun nonpos m = range_int (m, 0)
fun coint n =
if n = 0 then variant 0
else if n < 0 then coint (~n) o variant 1
else coint (n div 2) o variant 2
end