Add definitions to Primitives.fst and start on improving/fixing the

generated F* file

1 files changed, 43 insertions, 26 deletions

diff --git a/src/Assumed.ml b/src/Assumed.ml
index 5a9fb51b..527b2395 100644
--- a/src/Assumed.ml
+++ b/src/Assumed.ml
@@ -227,37 +227,54 @@ module Sig = struct
   let vec_index_mut_sig : A.fun_sig = vec_index_gen_sig true
 end
 
-(** The list of assumed functions, and their signatures.
+type assumed_info = A.assumed_fun_id * A.fun_sig * bool * Identifiers.name
+
+(** The list of assumed functions and all their information:
+    - their signature
+    - a boolean indicating whether they are monadic or not (i.e., if they
+      can fail or not)
+    - their name
 
     Rk.: following what is written above, we don't include `Box::free`.
+    
+    Remark about the vector functions: for `Vec::len` to be correct and return
+    a `usize`, we have to make sure that vectors are bounded by the max usize.
+    Followingly, `Vec::push` is monadic.
  *)
-let assumed_sigs : (A.assumed_fun_id * A.fun_sig) list =
+let assumed_infos : assumed_info list =
+  let deref_pre = [ "core"; "ops"; "deref" ] in
+  let vec_pre = [ "alloc"; "vec"; "Vec" ] in
+  let index_pre = [ "core"; "ops"; "index" ] in
   [
-    (Replace, Sig.mem_replace_sig);
-    (BoxNew, Sig.box_new_sig);
-    (BoxDeref, Sig.box_deref_shared_sig);
-    (BoxDerefMut, Sig.box_deref_mut_sig);
-    (VecNew, Sig.vec_new_sig);
-    (VecPush, Sig.vec_push_sig);
-    (VecInsert, Sig.vec_insert_sig);
-    (VecLen, Sig.vec_len_sig);
-    (VecIndex, Sig.vec_index_shared_sig);
-    (VecIndexMut, Sig.vec_index_mut_sig);
+    (Replace, Sig.mem_replace_sig, false, [ "core"; "mem"; "replace" ]);
+    (BoxNew, Sig.box_new_sig, false, [ "alloc"; "boxed"; "Box"; "new" ]);
+    (BoxDeref, Sig.box_deref_shared_sig, false, deref_pre @ [ "Deref"; "deref" ]);
+    ( BoxDerefMut,
+      Sig.box_deref_mut_sig,
+      false,
+      deref_pre @ [ "DerefMut"; "deref_mut" ] );
+    (VecNew, Sig.vec_new_sig, false, vec_pre @ [ "new" ]);
+    (VecPush, Sig.vec_push_sig, true, vec_pre @ [ "push" ]);
+    (VecInsert, Sig.vec_insert_sig, true, vec_pre @ [ "insert" ]);
+    (VecLen, Sig.vec_len_sig, false, vec_pre @ [ "len" ]);
+    (VecIndex, Sig.vec_index_shared_sig, true, index_pre @ [ "Index"; "index" ]);
+    ( VecIndexMut,
+      Sig.vec_index_mut_sig,
+      true,
+      index_pre @ [ "IndexMut"; "index_mut" ] );
   ]
 
+let get_assumed_info (id : A.assumed_fun_id) : assumed_info =
+  List.find (fun (id', _, _, _) -> id = id') assumed_infos
+
 let get_assumed_sig (id : A.assumed_fun_id) : A.fun_sig =
-  snd (List.find (fun (id', _) -> id = id') assumed_sigs)
+  let _, sg, _, _ = get_assumed_info id in
+  sg
 
-let assumed_names : (A.assumed_fun_id * Identifiers.name) list =
-  [
-    (Replace, [ "core"; "mem"; "replace" ]);
-    (BoxNew, [ "alloc"; "boxed"; "Box"; "new" ]);
-    (BoxDeref, [ "core"; "ops"; "deref"; "Deref"; "deref" ]);
-    (BoxDerefMut, [ "core"; "ops"; "deref"; "DerefMut"; "deref_mut" ]);
-    (VecNew, [ "alloc"; "vec"; "Vec"; "new" ]);
-    (VecPush, [ "alloc"; "vec"; "Vec"; "push" ]);
-    (VecInsert, [ "alloc"; "vec"; "Vec"; "insert" ]);
-    (VecLen, [ "alloc"; "vec"; "Vec"; "len" ]);
-    (VecIndex, [ "core"; "ops"; "index"; "Index"; "index" ]);
-    (VecIndexMut, [ "core"; "ops"; "index"; "IndexMut"; "index_mut" ]);
-  ]
+let get_assumed_name (id : A.assumed_fun_id) : Identifiers.name =
+  let _, _, _, name = get_assumed_info id in
+  name
+
+let assumed_is_monadic (id : A.assumed_fun_id) : bool =
+  let _, _, b, _ = get_assumed_info id in
+  b