Merge pull request #317 from mtzguido/fix

pulse2rust: update after F* change

Author: mtzguido

pulse2rust/src/Pulse2Rust.Deps.fst

@@ -175,8 +175,8 @@ let decl_reachable (reachable_defs:reachable_defs) (mname:string) (d:S.mlmodule1
 let rec topsort (d:dict) (grey:list string) (black:list string) (root:string)
   : (list string & list string) =  // grey and black
   let grey = root::grey in
-  let deps = root |> smap_try_find d |> must |> (fun (deps, _, _) -> deps) in
-  let deps = deps |> List.filter (fun f -> List.mem f (smap_keys d) && not (f = root)) in
+  let deps = root |> SMap.try_find d |> must |> (fun (deps, _, _) -> deps) in
+  let deps = deps |> List.filter (fun f -> List.mem f (SMap.keys d) && not (f = root)) in
   if List.existsb (fun d -> List.mem d grey) deps
   then failwith (format1 "cyclic dependency: %s" root);
   let deps = deps |> List.filter (fun f -> not (List.mem f black)) in
@@ -188,10 +188,10 @@ let rec topsort (d:dict) (grey:list string) (black:list string) (root:string)
 let rec topsort_all (d:dict) (black:list string)
   : list string =
 
-  if List.for_all (fun f -> List.contains f black) (smap_keys d)
+  if List.for_all (fun f -> List.contains f black) (SMap.keys d)
   then black
   else
-    let rem = List.filter (fun f -> not (List.contains f black)) (smap_keys d) in
+    let rem = List.filter (fun f -> not (List.contains f black)) (SMap.keys d) in
     let root = List.nth rem (List.length rem - 1) in
     let grey, black = topsort d [] black root in
     if List.length grey <> 0

pulse2rust/src/Pulse2Rust.Env.fsti

@@ -42,7 +42,7 @@ type reachable_defs = RBSet.t string
 
 val reachable_defs_to_string (d:reachable_defs) : string
 
-type dict = smap (list string & list UEnv.binding & S.mlmodule)
+type dict = SMap.t (list string & list UEnv.binding & S.mlmodule)
 
 type env = {
   external_libs : list string;

pulse2rust/src/Pulse2Rust.Extract.fst

@@ -67,9 +67,9 @@ let lookup_datacon_in_module1 (s:S.mlident) (m:S.mlmodule1) : option S.mlsymbol
   | _ -> None
 
 let lookup_datacon (g:env) (s:S.mlident) : option (list string & S.mlsymbol) =
-  let d_keys = smap_keys g.d in
+  let d_keys = SMap.keys g.d in
   find_map d_keys (fun k ->
-    let (_, _, decls) = smap_try_find g.d k |> must in
+    let (_, _, decls) = SMap.try_find g.d k |> must in
     let ropt = find_map decls (lookup_datacon_in_module1 s) in
     match ropt with
     | None -> None

pulse2rust/src/Pulse2Rust.fst

@@ -106,28 +106,28 @@ let file_to_module_name (f:string) : string =
   replace_chars s '_' "."
 
 let read_all_ast_files (files:list string) : dict =
-  let d = smap_create 100 in
+  let d = SMap.create 100 in
   files |> List.iter (fun f ->
     let contents  : (list string & list UEnv.binding & S.mlmodule) =
       match load_value_from_file f with
       | Some r -> r
       | None -> failwith (format1 "Could not load file %s" f) in
-    smap_add d (file_to_module_name f) contents);
+    SMap.add d (file_to_module_name f) contents);
   d
 
-let build_decls_dict (d:dict) : smap S.mlmodule1 =
-  let dd = smap_create 100 in
-  smap_iter d (fun module_nm (_, _, decls) ->
+let build_decls_dict (d:dict) : SMap.t S.mlmodule1 =
+  let dd = SMap.create 100 in
+  SMap.iter d (fun module_nm (_, _, decls) ->
     List.iter (fun (decl:S.mlmodule1) ->
       List.iter (fun decl_nm ->
-        smap_add dd (module_nm ^ "." ^ decl_nm) decl
+        SMap.add dd (module_nm ^ "." ^ decl_nm) decl
       ) (mlmodule1_name decl)
     ) decls
   );
   dd
 
 let rec collect_reachable_defs_aux
-  (dd:smap S.mlmodule1)
+  (dd:SMap.t S.mlmodule1)
   (worklist:reachable_defs)
   (reachable_defs:reachable_defs) =
 
@@ -138,7 +138,7 @@ let rec collect_reachable_defs_aux
       //  print1 "Adding %s to reachable_defs\n" hd;
        let reachable_defs = add hd reachable_defs in
        let worklist =
-         let hd_decl = smap_try_find dd hd in
+         let hd_decl = SMap.try_find dd hd in
          match hd_decl with
          | None -> worklist
          | Some hd_decl ->
@@ -153,7 +153,7 @@ let rec collect_reachable_defs_aux
 
 let collect_reachable_defs (d:dict) (root_module:string) : reachable_defs =
   let dd = build_decls_dict d in
-  let root_decls = smap_try_find d root_module |> must |> (fun (_, _, decls) -> decls) in
+  let root_decls = SMap.try_find d root_module |> must |> (fun (_, _, decls) -> decls) in
   let worklist = List.fold_left (fun worklist decl ->
     addn
       (decl |> mlmodule1_name |> List.map (fun s -> root_module ^ "." ^ s))
@@ -186,7 +186,7 @@ let extract (files:list string) (odir:string) (libs:string) : unit =
   let g = empty_env external_libs d all_modules reachable_defs in
   let _, all_rust_files = List.fold_left (fun (g, all_rust_files) f ->
     // print1 "Extracting file: %s\n" f;
-    let (_, bs, ds) = smap_try_find d f |> must in
+    let (_, bs, ds) = SMap.try_find d f |> must in
     let s, g = extract_one g f bs ds in
     let rust_fname = concat_dir_filename odir (rust_file_name f) in
     let rust_f = open_file_for_writing rust_fname in