simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

chore: upgrade bare autogen-code

Browse source
This commit is contained in:
Simon Cruanes 2021-12-07 21:16:25 -05:00
parent 110f3f8527
commit e64013c660
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 27 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/proof-trace/proof_ser.ml
View file

@ -1,3 +1,4 @@
(* generated from "proof_ser.bare" using bare-codegen *)
[@@@ocaml.warning "-26-27"] [@@@ocaml.warning "-26-27"]
(* embedded runtime library *) (* embedded runtime library *)
@ -258,17 +259,40 @@ let of_string dec s = of_bytes dec (Bytes.unsafe_of_string s)
1 (let s = to_s Encode.int (-1209433446454112432L) in 0x1 land (Char.code s.[0])) 1 (let s = to_s Encode.int (-1209433446454112432L) in 0x1 land (Char.code s.[0]))
*) *)
(*$Q (*$Q & ~count:1000
Q.(int64) (fun s -> \ Q.(int64) (fun s -> \
s = (of_s Decode.uint (to_s Encode.uint s))) s = (of_s Decode.uint (to_s Encode.uint s)))
Q.(small_nat) (fun n -> \
let n = Int64.of_int n in \
n = (of_s Decode.uint (to_s Encode.uint n)))
*) *)
(*$Q (*$Q & ~count:1000
Q.(int64) (fun s -> \ Q.(int64) (fun s -> \
s = (of_s Decode.int (to_s Encode.int s))) s = (of_s Decode.int (to_s Encode.int s)))
Q.(small_signed_int) (fun n -> \
let n = Int64.of_int n in \
n = (of_s Decode.int (to_s Encode.int n)))
*) *)
(* TODO: some tests with qtest *) (*$R
for i=0 to 1_000 do
let i = Int64.of_int i in
assert_equal ~printer:Int64.to_string i (of_s Decode.int (to_s Encode.int i))
done
*)
(*$R
for i=0 to 1_000 do
let i = Int64.of_int i in
assert_equal ~printer:Int64.to_string i (of_s Decode.uint (to_s Encode.uint i))
done
*)
(*$Q & ~count:1000
Q.(string) (fun s -> \
s = (of_s Decode.string (to_s Encode.string s)))
*)
end end