Skip to content

Wrapping OCaml WrapOCaml.fsti

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*.

module WrapOCaml

type float   = FStar.Float.float  // Which is a double in OCaml but non existant in F*.
type byte    = FStar.Bytes.byte
type char    = FStar.Char.char
type bytes   = FStar.Bytes.bytes
type uint8   = FStar.UInt8.t
type int8    = FStar.Int8.t
type uint16  = FStar.UInt16.t
type int16   = FStar.Int16.t
type int32   = FStar.Int32.t
type uint32  = FStar.UInt32.t
type int64   = FStar.Int64.t
type uint64  = FStar.UInt64.t
type uint128 = FStar.UInt128.t
type int128  = FStar.Int128.t

val unit_to_unit       : unit  -> unit
val bool_to_bool       : bool -> bool
/// val float_to_float    : float -> float
val char_to_char       : char -> char

/// TODO how are we typing this? We're getting back ^U for B.
val uchar_to_uchar     : char -> char
val byte_to_byte       : byte -> byte
val int_to_int         : int -> int 
val string_to_string   : string -> string
val option_to_option   : option int -> option int
val list_to_list       : list int   -> list int
val uint8_to_uint8     : uint8 -> uint8
val int8_to_int8       : int8 -> int8
val uint16_to_uint16   : uint16 -> uint16
val int16_to_int16     : int16 -> int16
val int32_to_int32     : int32 -> int32
val uint32_to_uint32   : uint32 -> uint32
val int64_to_int64     : int64 -> int64
val uint64_to_uint64   : uint64 -> uint64
val int128_to_int128   : int128 -> int128
val uint128_to_uint128 : uint128 -> uint128

val bytes_to_bytes     : 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

///  This is untypable in F*. 
/// val bad_to_bad : exn -> exn

Clone this wiki locally