Skip to content

Wrapping OCaml WrapOCaml.mli

briangmilnes edited this page Sep 16, 2024 · 1 revision
(*
///   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*.
 *)

val unit_to_unit       : unit  -> unit
val bool_to_bool       : bool -> bool
val float_to_float     : float -> float  (* Ya can't get there from here. *)
val byte_to_byte       : FStar_Bytes.byte -> FStar_Bytes.byte
val char_to_char       : int -> int
val uchar_to_uchar     : int -> int

(* F* is translating our into and out of Z.t, the type of 
  arbitrary precision integers in OCaml. *)
val int_to_int         : Z.t -> Z.t

val string_to_string   : string     -> string
val option_to_option   : Z.t option -> Z.t option 
val list_to_list       : Z.t list   -> Z.t list 

val uint8_to_uint8     : FStar_UInt8.uint8    -> FStar_UInt8.uint8
val int8_to_int8       : FStar_Int8.int8      -> FStar_Int8.int8
val uint16_to_uint16   : FStar_UInt16.uint16  -> FStar_UInt16.uint16
val int16_to_int16     : FStar_Int16.int16    -> FStar_Int16.int16
val int32_to_int32     : FStar_Int32.int32    -> FStar_Int32.int32
val uint32_to_uint32   : FStar_UInt32.uint32  -> FStar_UInt32.uint32
val int64_to_int64     : FStar_Int64.int64    -> FStar_Int64.int64
val uint64_to_uint64   : FStar_UInt64.uint64  -> FStar_UInt64.uint64
val int128_to_int128   : FStar_Int128.t       -> FStar_Int128.t
val uint128_to_uint128 : FStar_UInt128.t      -> FStar_UInt128.t

val bytes_to_bytes     : FStar_Bytes.bytes -> FStar_Bytes.bytes

type enum = | One | Two 
val enum_to_enum : enum -> enum

type prime = | Three | Seven
val prime_to_prime : prime -> prime

exception Bad of string

val bad_to_bad : exn -> exn
Clone this wiki locally