-
Notifications
You must be signed in to change notification settings - Fork 235
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