Wrapping OCaml Main.fst

module Main

open FStar.IO
open FStar.Class.Printable
open FStar.Bytes
open FStar.Char
open FStar.String

open WrapOCaml

///   Each test is going to create a value, so you have an F* side example,
///  send it over, get it back and print it, so you know you're getting the
///  right type.

let test_unit_to_unit () = 
 let u = unit_to_unit () in
  print_string ("unit_to_uint " ^ (to_string u) ^ "\n")

let test_bool_to_bool () = 
 let b = bool_to_bool true in
  print_string ("bool_to_bool " ^ (to_string b) ^ "\n")

///  Support is nearly non-existent for float. 
(*
let test_float_to_float () = 
 let f = float_to_float ? in
  print_string ("float_to_float " ^ (to_string f) ^ "\n")
*)

let test_char_to_char () =
 let c = char_to_char 'H' in
  print_string ("char_to_char " ^ (to_string c) ^ "\n")

let test_uchar_to_uchar () =
 let c = uchar_to_uchar (char_of_u32 21ul) in
  print_string ("uchar_to_uchar " ^ (to_string c) ^ "\n")

let test_byte_to_byte () = 
 let b = byte_to_byte 8uy in
  print_string ("byte_to_byte " ^ (to_string b) ^ "\n")

let test_int_to_int () = 
 let i = int_to_int 7 in
  print_string ("int_to_int " ^ (to_string i) ^ "\n")

let test_string_to_string () = 
 let s = string_to_string "HI" in
  print_string ("string_to_string " ^ s ^ "\n")

///  F* loses the typing here if option is polymorphic!

let test_option_to_option () = 
begin 
 let o = option_to_option None in
 let o' = option_to_option (Some 42) in
  (match o with 
   | None   -> print_string ("option_to_option None \n")
   | Some s -> print_string ("Error in option_to_option \n"));
  match o' with 
   | None   -> print_string ("Error in option_to_option \n")
   | Some s -> 
     print_string ("option_to_option Some " ^ (to_string s) ^ "\n")
end 

let test_list_to_list () = 
 let l = list_to_list [] in
  print_string ("list_to_list " ^ (to_string l) ^ "\n");
 let l = list_to_list [3; 4] in
  print_string ("list_to_list " ^ (to_string l) ^ "\n")

let test_uint8_to_uint8 () = 
 let u = uint8_to_uint8 8uy in
  print_string ("uint8_to_uint8 " ^ (to_string u) ^ "\n")

let test_int8_to_int8 () = 
 let i = int8_to_int8 8y in
  print_string ("int8_to_int8 " ^ (to_string i) ^ "\n")

let test_uint16_to_uint16 () = 
 let u = uint16_to_uint16 16us in
  print_string ("uint16_to_uint16 " ^ (to_string u) ^ "\n")

let test_int16_to_int16 () = 
 let i = int16_to_int16 16s in
  print_string ("int16_to_int16 " ^ (to_string i) ^ "\n")

let test_int32_to_int32 () = 
 let i = int32_to_int32 32l in
  print_string ("int32_to_int32 " ^ (to_string i) ^ "\n")

let test_uint32_to_uint32 () = 
 let u = uint32_to_uint32 32ul in
  print_string ("uint32_to_uint32 " ^ (to_string u) ^ "\n")

let test_int64_to_int64 () = 
 let i = int64_to_int64 64L in
  print_string ("int64_to_int64 " ^ (to_string i) ^ "\n")

let test_uint64_to_uint64 () = 
 let u = uint64_to_uint64 64uL in
  print_string ("uint64_to_uint64 " ^ (to_string u) ^ "\n")

(* There is an uint_of_t but not the other way.
let test_int128_to_int128 () = 
 let i = int128_to_int128  in
  print_string ("int128_to_int128 " ^ (to_string i) ^ "\n")

let test_uint128_to_uint128 () = 
 let u = uint128_to_uint128 ? in
  print_string ("uint128_to_uint128 " ^ (to_string u) ^ "\n")
*)

let test_bytes_to_bytes () = 
 let bs = FStar.Bytes.create 10ul 8uy in
  print_string ("test_bytes_to_bytes input  " ^ (print_bytes bs) ^ "\n");
 let b = bytes_to_bytes bs in 
  print_string ("test_bytes_to_bytes output " ^ (print_bytes b) ^ "\n")

let test_enum_to_enum () =
 let e = enum_to_enum One in
  match e with 
  | One -> print_string ("test_enum_to_enum One correct.\n")
  | Two -> print_string ("test_enum_to_enum Two ERROR.\n")

/// BUG F* can't find Three either as WrapOCaml.Three or Three !! 
/// This works above for enum One which is only trivially different.
/// It works in language server but not with either a recent
/// dev release or an opam development release.
/// The OCaml is not required for this bug.
/// F* 2024.08.14~dev
/// platform=Linux_x86_64
/// compiler=OCaml 4.14.2
/// date=2024-09-02 15:23:16 -0700
/// commit=445f713ad8b276864ba7e205e028813e19324b66
/// /home/milnes/.opam/default/bin/fstar.exe  --warn_error "-321-333-331"  --use_hints --use_hint_hashes --record_hints --hint_dir _build/fstar/fst/hints --print_universes --print_implicits  --cache_checked_modules   --cache_dir _build/fstar/fst/checked    --include src --include src/fstar/ --include src/fstar/fst/      --include /home/milnes/.opam/default/lib/fstar       src/fstar/fst/Main.fst 

(*
let test_prime_to_prime () =
 let e = prime_to_prime WrapOCaml.Three in
  match e with 
  | Three -> print_string ("test_prime_to_prime Three \n")
  | Seven -> print_string ("test_prime_to_prime Seven ERROR. \n")
*)

let main () = 
 print_string "Running WrapOCaml main\n";
 test_unit_to_unit     ();
 test_bool_to_bool     ();
 test_byte_to_byte     ();
 test_int_to_int       ();
 test_char_to_char     ();
 test_uchar_to_uchar   ();
 test_string_to_string ();
 test_option_to_option ();
 test_list_to_list     ();
 test_enum_to_enum     ();
(* test_prime_to_prime   (); *)
 test_uint8_to_uint8   ();
 test_int8_to_int8     ();
 test_uint16_to_uint16 ();
 test_int16_to_int16   ();
 test_int32_to_int32   ();
 test_uint32_to_uint32 ();
 test_int64_to_int64   ();
 test_uint64_to_uint64 ();
 test_bytes_to_bytes   ();
 ()
  
//Run ``main ()`` when the module loads
#push-options "--warn_error -272"
let _ = main ()
#pop-options