adding some missing functions in fstarlib

ulib/ml/FStar_Bytes.ml

@@ -31,7 +31,7 @@ let get (b:bytes) (pos:u32) = int_of_char (String.get b pos)
 let op_String_Access = get
 
 let set_byte (bs:bytes) (pos:u32) (b:byte) =
-    Bytes.set (Bytes.copy bs) pos (char_of_int b)
+    let x = (Bytes.copy bs) in Bytes.set x pos (char_of_int b); x
 let op_String_Assignment = set_byte
 let index (b:bytes) (i:Z.t) = get b (Z.to_int i)
 
@@ -141,6 +141,7 @@ let xor_idempotent (n:U32.t) (b1:bytes) (b2:bytes) = ()
 (*********************************************************************************)
 (* Under discussion *)
 let utf8 (x:string) : bytes = x (* TODO: use Camomile *)
+let utf8_encode = utf8
 let iutf8 (x:bytes) : string = x (* TODO: use Camomile *)
 let iutf8_opt (x:bytes) : string option = Some (x)
 (*********************************************************************************)

ulib/ml/FStar_Dyn.ml

@@ -0,0 +1,3 @@
+type dyn = Obj.t
+let mkdyn (x:'a) : dyn = Obj.repr x
+let undyn (x:dyn) : 'a = Obj.obj x

ulib/ml/FStar_Heap.ml

@@ -1,3 +1,5 @@
 open FStar_Monotonic_Heap
 
 type 'a ref = 'a FStar_Monotonic_Heap.ref
+type ('a, 'b, 'c) trivial_rel = Prims.l_True
+type ('a, 'b, 'c) trivial_preorder = ('a, 'b, 'c) trivial_rel

ulib/ml/FStar_HyperStack_ST.ml

@@ -48,12 +48,19 @@ let get () = HS (Prims.parse_int "0", FStar_Map.const FStar_Monotonic_Heap.emp,
 let recall = (fun r -> ())
 
 let recall_region = (fun r -> ())
+let witness_region _ = ()
+let witness_hsref _ _ = ()
+type erid = rid
 
 type 'a ref = 'a FStar_HyperStack.reference
 let alloc = salloc
 type ('a, 'b) mref = 'a ref
 type ('a, 'b, 'c) m_rref = 'b ref
+type ('a, 'b, 'c, 'd, 'e) stable_on_t = unit
 let mr_witness _ _ _ _ _ = ()
-let mr_testify _ _ _ _ _ = ()
-type erid = rid
+let testify _ = ()
+let testify_forall _ = ()
+let testify_forall_region_contains_pred _ _ = ()
+
+type ex_rid = erid
 type 'a witnessed = 'a FStar_CommonST.witnessed

ulib/ml/FStar_Int16.ml

@@ -69,3 +69,4 @@ let cmod x =
 
 let to_string s = string_of_int (cmod s)
 let int_to_t s = int_to_int16 s
+let __int_to_t = int_to_t

ulib/ml/FStar_Int32.ml

@@ -69,3 +69,4 @@ let cmod x =
 
 let to_string s = string_of_int (cmod s)
 let int_to_t s = int_to_int32 s
+let __int_to_t = int_to_t

ulib/ml/FStar_Int63.ml

@@ -66,3 +66,4 @@ let op_Less_Equals_Hat = lte
 
 let to_string = string_of_int
 let int_to_t s = s
+let __int_to_t = int_to_t

ulib/ml/FStar_Int64.ml

@@ -67,3 +67,4 @@ let op_Less_Equals_Hat = lte
 
 let to_string = Int64.to_string                     
 let int_to_t s = int_to_int64 s
+let __int_to_t = int_to_t

ulib/ml/FStar_Int8.ml

@@ -69,3 +69,4 @@ let op_Less_Equals_Hat = lte
 
 let to_string s = string_of_int (cmod s)
 let int_to_t s = int_to_int8 s
+let __int_to_t = int_to_t

ulib/ml/FStar_UInt16.ml

@@ -69,3 +69,4 @@ let op_Less_Equals_Hat = lte
 
 let to_string s = string_of_int s
 let uint_to_t s = int_to_uint16 s
+let __uint_to_t = uint_to_t

ulib/ml/FStar_UInt32.ml

@@ -76,3 +76,4 @@ let of_string s = int_of_string s
 let to_string s = string_of_int s
 let to_int s = s
 let uint_to_t s = int_to_uint32 s
+let __uint_to_t = uint_to_t

ulib/ml/FStar_UInt63.ml

@@ -69,3 +69,4 @@ let op_Less_Equals_Hat = lte
 
 let to_string s = Int64.to_string (Int64.logand (Int64.of_int s) (Int64.of_string "0x7fffffffffffffff"))
 let uint_to_t s = int_to_uint63 s
+let __uint_to_t = uint_to_t

ulib/ml/FStar_UInt64.ml

@@ -84,3 +84,4 @@ let to_string s = Stdint.Uint64.to_string s
 let of_string s = Stdint.Uint64.of_string s
 
 let uint_to_t s = Stdint.Uint64.of_string (Z.to_string s)
+let __uint_to_t = uint_to_t

ulib/ml/FStar_UInt8.ml

@@ -77,3 +77,4 @@ let to_string s = string_of_int s
 let to_string_hex s = Printf.sprintf "%02x" s
 let uint_to_t s = int_to_uint8 s
 let to_int s = s
+let __uint_to_t = uint_to_t

ulib/ml/Makefile.include

@@ -3,7 +3,7 @@
 
 # This Makefile assumes that $(FSTAR_HOME) is properly defined.
 
-FSTAR_REALIZED_MODULES=All BaseTypes Buffer Bytes Char CommonST Constructive Float Ghost Heap Monotonic.Heap \
+FSTAR_REALIZED_MODULES=All BaseTypes Buffer Bytes Char CommonST Constructive Dyn Float Ghost Heap Monotonic.Heap \
 	HyperStack.All HyperStack.ST Int16 Int32 Int63 Int64 Int8 Int.Cast IO \
 	List List.Tot.Base Mul Option Pervasives.Native Set ST Exn String \
 	UInt16 UInt32 UInt63 UInt64 UInt8 \