Wrapping OCaml WrapOCaml.ml

(*
   This module shows all of the basic types you'll need going into and out of OCaml,
  correctly typed in both and fsti interface and an mli interface. In the ml we
  show how to transform everything into the native OCaml and back to the right
  type to return to F*.
 *)

let unit_to_unit (u : unit) : unit = ()

let bool_to_bool     (b : bool)      : bool       = b

let float_to_float   (f : float)     : float      = f

(* It is difficult to get a char across to ML, int is easiest. 
  Even though we can then make an unsigned Char of it from
  the newer module Uchar.t
 *)
let char_to_char     (c : int)       : int       = c

let uchar_to_uchar   (c : int)       : int       = (Uchar.to_int (Uchar.of_int c))

let byte_to_byte     (b : FStar_Bytes.byte) : FStar_Bytes.byte = b

let int_to_int       (i : Z.t)       : Z.t        = Z.of_int ((Z.to_int i) + 1)

let string_to_string (s : string)    : string     = (s ^ " There!")

let option_to_option (o : Z.t option) : Z.t option  =
  match o with
  | None -> None
  | Some x -> Some x

let list_to_list     (l : Z.t list )  : Z.t list    = 
  match l with
  | [] -> []
  | h::t -> t

(* Here are unsafe translation to and from int. *)
let int8_to_int8       (i : FStar_Int8.int8)     : FStar_Int8.int8    =
  (FStar_Int8.of_native_int (FStar_Int8.to_native_int i))

let uint8_to_uint8       (i : FStar_UInt8.uint8) : FStar_UInt8.uint8  = i

let uint16_to_uint16   (u : FStar_UInt16.uint16) : FStar_UInt16.uint16 = 
  (FStar_UInt16.of_native_int (FStar_UInt16.to_native_int u))

let int16_to_int16     (i : FStar_Int16.int16)   : FStar_Int16.int16   = 
  (FStar_Int16.of_native_int (FStar_Int16.to_native_int i))

let int32_to_int32     (i : FStar_Int32.int32)   : FStar_Int32.int32   = 
  (FStar_Int32.of_native_int (FStar_Int32.to_native_int i))

let uint32_to_uint32   (u : FStar_UInt32.uint32) : FStar_UInt32.uint32 = 
  (FStar_UInt32.of_native_int (FStar_UInt32.to_native_int u))

let int64_to_int64     (i : FStar_Int64.int64)   : FStar_Int64.int64   = 
  (FStar_Int64.of_native_int (FStar_Int64.to_native_int i))

let uint64_to_uint64   (u : FStar_UInt64.uint64) : FStar_UInt64.uint64 = 
  (FStar_UInt64.of_native_int (FStar_UInt64.to_native_int u))

(* At this point I don't know how to translate this. *)

let int128_to_int128   (i : FStar_Int128.t)      : FStar_Int128.t  = i

let uint128_to_uint128 (u : FStar_UInt128.t)     : FStar_UInt128.t = u

(* In FStar_Bytes.ml this is a string and we can treat it as such.
   But we are also translate it to OCaml bytes, set it, and 
   return it as a string. Both FStar and OCaml are treating this
   as immutable, so some OCaml wrapped calls have to change to
   return the byte array as a string.
*)
let bytes_to_bytes     (b : FStar_Bytes.bytes)   : FStar_Bytes.bytes   = 
  let len = String.length b in
  let bs  = Bytes.of_string b in
   Bytes.set bs 0 'H';
   Bytes.set bs 1 'I';
   Bytes.to_string bs

(*  Take an enum from another module and show its translation. *)

module Enum' = struct
 type enum = | One | Two 
end

type enum = | One | Two 

let of_enum (e : enum) : Enum'.enum =
  match e with
  | One -> Enum'.One
  | Two -> Enum'.Two

let to_enum (e : Enum'.enum) : enum =
  match e with
  | Enum'.One -> One
  | Enum'.Two -> Two

let enum_to_enum (e : enum) : enum = to_enum (of_enum e)

(* You can simply use an inductive type if you've defined it in
  F* and your OCaml, but the more common case is you're wrapping
  an exception from OCaml into one in F*.
 *)

type prime = | Three | Seven

let prime_to_prime (e: prime) : prime = e

(* 
  You can translate an exception and type a function on it in OCaml but
 not in F*.
*)

(* Exceptions *)

module HasExn = struct
  exception Bad of string
end  

exception Bad of string

let to_bad e =
  match e with
  | HasExn.Bad s -> Bad s
  | _            -> raise (Failure "Not a bad exception.")

let of_bad e =
  match e with
  | Bad s -> HasExn.Bad s
  | _            -> raise (Failure "Not a bad exception.")

let bad_to_bad (e : exn) : exn = (to_bad (of_bad e))