From 10e9c20073e1fcd3acf1194b9074a21bdccd44ca Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Oct 2022 18:22:28 +0200
Subject: Rename Modules to Crates

---
 src/Contexts.ml         |  5 ++-
 src/Crates.ml           | 90 +++++++++++++++++++++++++++++++++++++++++++++++++
 src/FunsAnalysis.ml     |  4 +--
 src/Interpreter.ml      | 31 ++++++++---------
 src/LlbcOfJson.ml       | 27 +++++++--------
 src/Modules.ml          | 90 -------------------------------------------------
 src/PrePasses.ml        |  3 +-
 src/Print.ml            | 11 +++---
 src/PrintSymbolicAst.ml |  1 -
 src/SymbolicToPure.ml   |  1 -
 src/Translate.ml        | 51 ++++++++++++++--------------
 src/TranslateCore.ml    |  1 -
 src/TypesAnalysis.ml    |  2 +-
 src/main.ml             |  2 +-
 14 files changed, 158 insertions(+), 161 deletions(-)
 create mode 100644 src/Crates.ml
 delete mode 100644 src/Modules.ml

(limited to 'src')

diff --git a/src/Contexts.ml b/src/Contexts.ml
index 716326cf..07535e06 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -3,7 +3,6 @@ open Values
 open LlbcAst
 module V = Values
 open ValuesUtils
-module M = Modules
 
 (** Some global counters.
  *
@@ -210,7 +209,7 @@ let config_of_partial (mode : interpreter_mode) (config : partial_config) :
   }
 
 type type_context = {
-  type_decls_groups : M.type_declaration_group TypeDeclId.Map.t;
+  type_decls_groups : Crates.type_declaration_group TypeDeclId.Map.t;
   type_decls : type_decl TypeDeclId.Map.t;
   type_infos : TypesAnalysis.type_infos;
 }
@@ -391,7 +390,7 @@ let ctx_lookup_abs (ctx : eval_ctx) (abs_id : V.AbstractionId.id) : V.abs =
 
 let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool =
   let decl_group = TypeDeclId.Map.find id ctx.type_context.type_decls_groups in
-  match decl_group with M.Rec _ -> true | M.NonRec _ -> false
+  match decl_group with Crates.Rec _ -> true | Crates.NonRec _ -> false
 
 (** Visitor to iterate over the values in the *current* frame *)
 class ['self] iter_frame =
diff --git a/src/Crates.ml b/src/Crates.ml
new file mode 100644
index 00000000..844afb94
--- /dev/null
+++ b/src/Crates.ml
@@ -0,0 +1,90 @@
+open Types
+open LlbcAst
+
+type 'id g_declaration_group = NonRec of 'id | Rec of 'id list
+[@@deriving show]
+
+type type_declaration_group = TypeDeclId.id g_declaration_group
+[@@deriving show]
+
+type fun_declaration_group = FunDeclId.id g_declaration_group [@@deriving show]
+
+(** Module declaration. Globals cannot be mutually recursive. *)
+type declaration_group =
+  | Type of type_declaration_group
+  | Fun of fun_declaration_group
+  | Global of GlobalDeclId.id
+[@@deriving show]
+
+type llbc_crate = {
+  name : string;
+  declarations : declaration_group list;
+  types : type_decl list;
+  functions : fun_decl list;
+  globals : global_decl list;
+}
+(** LLBC crate *)
+
+let compute_defs_maps (c : llbc_crate) :
+    type_decl TypeDeclId.Map.t
+    * fun_decl FunDeclId.Map.t
+    * global_decl GlobalDeclId.Map.t =
+  let types_map =
+    List.fold_left
+      (fun m (def : type_decl) -> TypeDeclId.Map.add def.def_id def m)
+      TypeDeclId.Map.empty c.types
+  in
+  let funs_map =
+    List.fold_left
+      (fun m (def : fun_decl) -> FunDeclId.Map.add def.def_id def m)
+      FunDeclId.Map.empty c.functions
+  in
+  let globals_map =
+    List.fold_left
+      (fun m (def : global_decl) -> GlobalDeclId.Map.add def.def_id def m)
+      GlobalDeclId.Map.empty c.globals
+  in
+  (types_map, funs_map, globals_map)
+
+(** Split a module's declarations between types, functions and globals *)
+let split_declarations (decls : declaration_group list) :
+    type_declaration_group list
+    * fun_declaration_group list
+    * GlobalDeclId.id list =
+  let rec split decls =
+    match decls with
+    | [] -> ([], [], [])
+    | d :: decls' -> (
+        let types, funs, globals = split decls' in
+        match d with
+        | Type decl -> (decl :: types, funs, globals)
+        | Fun decl -> (types, decl :: funs, globals)
+        | Global decl -> (types, funs, decl :: globals))
+  in
+  split decls
+
+(** Split a module's declarations into three maps from type/fun/global ids to
+    declaration groups.
+ *)
+let split_declarations_to_group_maps (decls : declaration_group list) :
+    type_declaration_group TypeDeclId.Map.t
+    * fun_declaration_group FunDeclId.Map.t
+    * GlobalDeclId.Set.t =
+  let module G (M : Map.S) = struct
+    let add_group (map : M.key g_declaration_group M.t)
+        (group : M.key g_declaration_group) : M.key g_declaration_group M.t =
+      match group with
+      | NonRec id -> M.add id group map
+      | Rec ids -> List.fold_left (fun map id -> M.add id group map) map ids
+
+    let create_map (groups : M.key g_declaration_group list) :
+        M.key g_declaration_group M.t =
+      List.fold_left add_group M.empty groups
+  end in
+  let types, funs, globals = split_declarations decls in
+  let module TG = G (TypeDeclId.Map) in
+  let types = TG.create_map types in
+  let module FG = G (FunDeclId.Map) in
+  let funs = FG.create_map funs in
+  let globals = GlobalDeclId.Set.of_list globals in
+  (types, funs, globals)
diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml
index 615f45b3..248ad8b3 100644
--- a/src/FunsAnalysis.ml
+++ b/src/FunsAnalysis.ml
@@ -8,7 +8,7 @@
  *)
 
 open LlbcAst
-open Modules
+open Crates
 module EU = ExpressionsUtils
 
 type fun_info = {
@@ -26,7 +26,7 @@ type fun_info = {
 type modules_funs_info = fun_info FunDeclId.Map.t
 (** Various information about a module's functions *)
 
-let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
+let analyze_module (m : llbc_crate) (funs_map : fun_decl FunDeclId.Map.t)
     (globals_map : global_decl GlobalDeclId.Map.t) (use_state : bool) :
     modules_funs_info =
   let infos = ref FunDeclId.Map.empty in
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 3a2939ef..9308fa16 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -7,18 +7,17 @@ open LlbcAstUtils
 module L = Logging
 module T = Types
 module A = LlbcAst
-module M = Modules
 module SA = SymbolicAst
 
 (** The local logger *)
 let log = L.interpreter_log
 
-let compute_type_fun_global_contexts (m : M.llbc_module) :
+let compute_type_fun_global_contexts (m : Crates.llbc_crate) :
     C.type_context * C.fun_context * C.global_context =
-  let type_decls_list, _, _ = M.split_declarations m.declarations in
-  let type_decls, fun_decls, global_decls = M.compute_defs_maps m in
+  let type_decls_list, _, _ = Crates.split_declarations m.declarations in
+  let type_decls, fun_decls, global_decls = Crates.compute_defs_maps m in
   let type_decls_groups, _funs_defs_groups, _globals_defs_groups =
-    M.split_declarations_to_group_maps m.declarations
+    Crates.split_declarations_to_group_maps m.declarations
   in
   let type_infos =
     TypesAnalysis.analyze_type_declarations type_decls type_decls_list
@@ -277,10 +276,10 @@ module Test = struct
   (** Test a unit function (taking no arguments) by evaluating it in an empty
       environment.
    *)
-  let test_unit_function (config : C.partial_config) (m : M.llbc_module)
+  let test_unit_function (config : C.partial_config) (crate : Crates.llbc_crate)
       (fid : A.FunDeclId.id) : unit =
     (* Retrieve the function declaration *)
-    let fdef = A.FunDeclId.nth m.functions fid in
+    let fdef = A.FunDeclId.nth crate.functions fid in
     let body = Option.get fdef.body in
 
     (* Debug *)
@@ -294,7 +293,7 @@ module Test = struct
 
     (* Create the evaluation context *)
     let type_context, fun_context, global_context =
-      compute_type_fun_global_contexts m
+      compute_type_fun_global_contexts crate
     in
     let ctx =
       initialize_eval_context type_context fun_context global_context []
@@ -332,11 +331,11 @@ module Test = struct
         && List.length def.A.signature.inputs = 0
 
   (** Test all the unit functions in a list of function definitions *)
-  let test_unit_functions (config : C.partial_config) (m : M.llbc_module) : unit
-      =
-    let unit_funs = List.filter fun_decl_is_transparent_unit m.functions in
+  let test_unit_functions (config : C.partial_config)
+      (crate : Crates.llbc_crate) : unit =
+    let unit_funs = List.filter fun_decl_is_transparent_unit crate.functions in
     let test_unit_fun (def : A.fun_decl) : unit =
-      test_unit_function config m def.A.def_id
+      test_unit_function config crate def.A.def_id
     in
     List.iter test_unit_fun unit_funs
 
@@ -374,15 +373,17 @@ module Test = struct
       they are not supported by the symbolic interpreter.
    *)
   let test_functions_symbolic (config : C.partial_config) (synthesize : bool)
-      (m : M.llbc_module) : unit =
+      (crate : Crates.llbc_crate) : unit =
     (* Filter the functions which contain loops *)
     let no_loop_funs =
-      List.filter (fun f -> not (LlbcAstUtils.fun_decl_has_loops f)) m.functions
+      List.filter
+        (fun f -> not (LlbcAstUtils.fun_decl_has_loops f))
+        crate.functions
     in
     (* Filter the opaque functions *)
     let no_loop_funs = List.filter fun_decl_is_transparent no_loop_funs in
     let type_context, fun_context, global_context =
-      compute_type_fun_global_contexts m
+      compute_type_fun_global_contexts crate
     in
     let test_fun (def : A.fun_decl) : unit =
       (* Execute the function - note that as the symbolic interpreter explores
diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml
index 4e10c642..44abedf2 100644
--- a/src/LlbcOfJson.ml
+++ b/src/LlbcOfJson.ml
@@ -14,7 +14,6 @@ open OfJsonBasic
 module T = Types
 module V = Values
 module S = Scalars
-module M = Modules
 module E = Expressions
 module A = LlbcAst
 module TU = TypesUtils
@@ -680,24 +679,24 @@ let global_decl_of_json (js : json) (gid_conv : global_id_converter) :
     | _ -> Error "")
 
 let g_declaration_group_of_json (id_of_json : json -> ('id, string) result)
-    (js : json) : ('id M.g_declaration_group, string) result =
+    (js : json) : ('id Crates.g_declaration_group, string) result =
   combine_error_msgs js "g_declaration_group_of_json"
     (match js with
     | `Assoc [ ("NonRec", `List [ id ]) ] ->
         let* id = id_of_json id in
-        Ok (M.NonRec id)
+        Ok (Crates.NonRec id)
     | `Assoc [ ("Rec", `List [ ids ]) ] ->
         let* ids = list_of_json id_of_json ids in
-        Ok (M.Rec ids)
+        Ok (Crates.Rec ids)
     | _ -> Error "")
 
 let type_declaration_group_of_json (js : json) :
-    (M.type_declaration_group, string) result =
+    (Crates.type_declaration_group, string) result =
   combine_error_msgs js "type_declaration_group_of_json"
     (g_declaration_group_of_json T.TypeDeclId.id_of_json js)
 
 let fun_declaration_group_of_json (js : json) :
-    (M.fun_declaration_group, string) result =
+    (Crates.fun_declaration_group, string) result =
   combine_error_msgs js "fun_declaration_group_of_json"
     (g_declaration_group_of_json A.FunDeclId.id_of_json js)
 
@@ -711,19 +710,19 @@ let global_declaration_group_of_json (js : json) :
     | `Assoc [ ("Rec", `List [ _ ]) ] -> Error "got mutually dependent globals"
     | _ -> Error "")
 
-let declaration_group_of_json (js : json) : (M.declaration_group, string) result
-    =
+let declaration_group_of_json (js : json) :
+    (Crates.declaration_group, string) result =
   combine_error_msgs js "declaration_of_json"
     (match js with
     | `Assoc [ ("Type", `List [ decl ]) ] ->
         let* decl = type_declaration_group_of_json decl in
-        Ok (M.Type decl)
+        Ok (Crates.Type decl)
     | `Assoc [ ("Fun", `List [ decl ]) ] ->
         let* decl = fun_declaration_group_of_json decl in
-        Ok (M.Fun decl)
+        Ok (Crates.Fun decl)
     | `Assoc [ ("Global", `List [ decl ]) ] ->
         let* id = global_declaration_group_of_json decl in
-        Ok (M.Global id)
+        Ok (Crates.Global id)
     | _ -> Error "")
 
 let length_of_json_list (js : json) : (int, string) result =
@@ -732,8 +731,8 @@ let length_of_json_list (js : json) : (int, string) result =
     | `List jsl -> Ok (List.length jsl)
     | _ -> Error ("not a list: " ^ show js))
 
-let llbc_module_of_json (js : json) : (M.llbc_module, string) result =
-  combine_error_msgs js "llbc_module_of_json"
+let llbc_crate_of_json (js : json) : (Crates.llbc_crate, string) result =
+  combine_error_msgs js "llbc_crate_of_json"
     (match js with
     | `Assoc
         [
@@ -763,7 +762,7 @@ let llbc_module_of_json (js : json) : (M.llbc_module, string) result =
         let globals, global_bodies = List.split globals in
         Ok
           {
-            M.name;
+            Crates.name;
             declarations;
             types;
             functions = functions @ global_bodies;
diff --git a/src/Modules.ml b/src/Modules.ml
deleted file mode 100644
index 7f372d09..00000000
--- a/src/Modules.ml
+++ /dev/null
@@ -1,90 +0,0 @@
-open Types
-open LlbcAst
-
-type 'id g_declaration_group = NonRec of 'id | Rec of 'id list
-[@@deriving show]
-
-type type_declaration_group = TypeDeclId.id g_declaration_group
-[@@deriving show]
-
-type fun_declaration_group = FunDeclId.id g_declaration_group [@@deriving show]
-
-(** Module declaration. Globals cannot be mutually recursive. *)
-type declaration_group =
-  | Type of type_declaration_group
-  | Fun of fun_declaration_group
-  | Global of GlobalDeclId.id
-[@@deriving show]
-
-type llbc_module = {
-  name : string;
-  declarations : declaration_group list;
-  types : type_decl list;
-  functions : fun_decl list;
-  globals : global_decl list;
-}
-(** LLBC module - TODO: rename to crate *)
-
-let compute_defs_maps (m : llbc_module) :
-    type_decl TypeDeclId.Map.t
-    * fun_decl FunDeclId.Map.t
-    * global_decl GlobalDeclId.Map.t =
-  let types_map =
-    List.fold_left
-      (fun m (def : type_decl) -> TypeDeclId.Map.add def.def_id def m)
-      TypeDeclId.Map.empty m.types
-  in
-  let funs_map =
-    List.fold_left
-      (fun m (def : fun_decl) -> FunDeclId.Map.add def.def_id def m)
-      FunDeclId.Map.empty m.functions
-  in
-  let globals_map =
-    List.fold_left
-      (fun m (def : global_decl) -> GlobalDeclId.Map.add def.def_id def m)
-      GlobalDeclId.Map.empty m.globals
-  in
-  (types_map, funs_map, globals_map)
-
-(** Split a module's declarations between types, functions and globals *)
-let split_declarations (decls : declaration_group list) :
-    type_declaration_group list
-    * fun_declaration_group list
-    * GlobalDeclId.id list =
-  let rec split decls =
-    match decls with
-    | [] -> ([], [], [])
-    | d :: decls' -> (
-        let types, funs, globals = split decls' in
-        match d with
-        | Type decl -> (decl :: types, funs, globals)
-        | Fun decl -> (types, decl :: funs, globals)
-        | Global decl -> (types, funs, decl :: globals))
-  in
-  split decls
-
-(** Split a module's declarations into three maps from type/fun/global ids to
-    declaration groups.
- *)
-let split_declarations_to_group_maps (decls : declaration_group list) :
-    type_declaration_group TypeDeclId.Map.t
-    * fun_declaration_group FunDeclId.Map.t
-    * GlobalDeclId.Set.t =
-  let module G (M : Map.S) = struct
-    let add_group (map : M.key g_declaration_group M.t)
-        (group : M.key g_declaration_group) : M.key g_declaration_group M.t =
-      match group with
-      | NonRec id -> M.add id group map
-      | Rec ids -> List.fold_left (fun map id -> M.add id group map) map ids
-
-    let create_map (groups : M.key g_declaration_group list) :
-        M.key g_declaration_group M.t =
-      List.fold_left add_group M.empty groups
-  end in
-  let types, funs, globals = split_declarations decls in
-  let module TG = G (TypeDeclId.Map) in
-  let types = TG.create_map types in
-  let module FG = G (FunDeclId.Map) in
-  let funs = FG.create_map funs in
-  let globals = GlobalDeclId.Set.of_list globals in
-  (types, funs, globals)
diff --git a/src/PrePasses.ml b/src/PrePasses.ml
index c9d496ea..3159907e 100644
--- a/src/PrePasses.ml
+++ b/src/PrePasses.ml
@@ -7,7 +7,6 @@ module V = Values
 module E = Expressions
 module C = Contexts
 module A = LlbcAst
-module M = Modules
 module L = Logging
 
 let log = L.pre_passes_log
@@ -50,6 +49,6 @@ let filter_drop_assigns (f : A.fun_decl) : A.fun_decl =
   in
   { f with body }
 
-let apply_passes (m : M.llbc_module) : M.llbc_module =
+let apply_passes (m : Crates.llbc_crate) : Crates.llbc_crate =
   let functions = List.map filter_drop_assigns m.functions in
   { m with functions }
diff --git a/src/Print.ml b/src/Print.ml
index c10c5989..1439a74d 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -6,7 +6,6 @@ module VU = ValuesUtils
 module E = Expressions
 module A = LlbcAst
 module C = Contexts
-module M = Modules
 
 let option_to_string (to_string : 'a -> string) (x : 'a option) : string =
   match x with Some x -> "Some (" ^ to_string x ^ ")" | None -> "None"
@@ -1194,19 +1193,21 @@ module Module = struct
     in
     PA.fun_decl_to_string fmt "" "  " def
 
-  let module_to_string (m : M.llbc_module) : string =
+  let module_to_string (m : Crates.llbc_crate) : string =
     let types_defs_map, funs_defs_map, globals_defs_map =
-      M.compute_defs_maps m
+      Crates.compute_defs_maps m
     in
 
     (* The types *)
-    let type_decls = List.map (type_decl_to_string types_defs_map) m.M.types in
+    let type_decls =
+      List.map (type_decl_to_string types_defs_map) m.Crates.types
+    in
 
     (* The functions *)
     let fun_decls =
       List.map
         (fun_decl_to_string types_defs_map funs_defs_map globals_defs_map)
-        m.M.functions
+        m.Crates.functions
     in
 
     (* Put everything together *)
diff --git a/src/PrintSymbolicAst.ml b/src/PrintSymbolicAst.ml
index e44b422a..37b7555e 100644
--- a/src/PrintSymbolicAst.ml
+++ b/src/PrintSymbolicAst.ml
@@ -14,7 +14,6 @@ module V = Values
 module E = Expressions
 module A = LlbcAst
 module C = Contexts
-module M = Modules
 open SymbolicAst
 module P = Print
 module PT = Print.Types
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index f321ce8c..77c5e0e8 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -3,7 +3,6 @@ open LlbcAstUtils
 open Pure
 open PureUtils
 module Id = Identifiers
-module M = Modules
 module S = SymbolicAst
 module TA = TypesAnalysis
 module L = Logging
diff --git a/src/Translate.ml b/src/Translate.ml
index 61300ed8..8024d910 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -3,7 +3,6 @@ open Interpreter
 module L = Logging
 module T = Types
 module A = LlbcAst
-module M = Modules
 module SA = SymbolicAst
 module Micro = PureMicroPasses
 open PureUtils
@@ -286,24 +285,24 @@ let translate_function_to_pure (config : C.partial_config)
   (pure_forward, pure_backwards)
 
 let translate_module_to_pure (config : C.partial_config)
-    (mp_config : Micro.config) (use_state : bool) (m : M.llbc_module) :
+    (mp_config : Micro.config) (use_state : bool) (crate : Crates.llbc_crate) :
     trans_ctx * Pure.type_decl list * (bool * pure_fun_translation) list =
   (* Debug *)
   log#ldebug (lazy "translate_module_to_pure");
 
   (* Compute the type and function contexts *)
   let type_context, fun_context, global_context =
-    compute_type_fun_global_contexts m
+    compute_type_fun_global_contexts crate
   in
   let fun_infos =
-    FA.analyze_module m fun_context.C.fun_decls global_context.C.global_decls
-      use_state
+    FA.analyze_module crate fun_context.C.fun_decls
+      global_context.C.global_decls use_state
   in
   let fun_context = { fun_decls = fun_context.fun_decls; fun_infos } in
   let trans_ctx = { type_context; fun_context; global_context } in
 
   (* Translate all the type definitions *)
-  let type_decls = SymbolicToPure.translate_type_decls m.types in
+  let type_decls = SymbolicToPure.translate_type_decls crate.types in
 
   (* Compute the type definition map *)
   let type_decls_map =
@@ -330,7 +329,7 @@ let translate_module_to_pure (config : C.partial_config)
                 (LlbcAstUtils.fun_body_get_input_vars body)
         in
         (A.Regular fdef.def_id, input_names, fdef.signature))
-      m.functions
+      crate.functions
   in
   let sigs = List.append assumed_sigs local_sigs in
   let fun_sigs =
@@ -343,7 +342,7 @@ let translate_module_to_pure (config : C.partial_config)
     List.map
       (translate_function_to_pure config mp_config trans_ctx fun_sigs
          type_decls_map)
-      m.functions
+      crate.functions
   in
 
   (* Apply the micro-passes *)
@@ -357,7 +356,7 @@ let translate_module_to_pure (config : C.partial_config)
   (trans_ctx, type_decls, pure_translations)
 
 type gen_ctx = {
-  m : M.llbc_module;
+  crate : Crates.llbc_crate;
   extract_ctx : PureToExtract.extraction_ctx;
   trans_types : Pure.type_decl Pure.TypeDeclId.Map.t;
   trans_funs : (bool * pure_fun_translation) A.FunDeclId.Map.t;
@@ -534,7 +533,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
     ExtractToFStar.extract_state_type fmt ctx.extract_ctx qualif
   in
 
-  let export_decl (decl : M.declaration_group) : unit =
+  let export_decl (decl : Crates.declaration_group) : unit =
     match decl with
     | Type (NonRec id) ->
         if config.extract_types then export_type ExtractToFStar.Type id
@@ -574,7 +573,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
    *)
   if config.extract_state_type && config.extract_fun_decls then
     export_state_type ();
-  List.iter export_decl ctx.m.declarations;
+  List.iter export_decl ctx.crate.declarations;
   if config.extract_state_type && not config.extract_fun_decls then
     export_state_type ()
 
@@ -628,11 +627,11 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
     TODO: rename to translate_crate
  *)
 let translate_module (filename : string) (dest_dir : string) (config : config)
-    (m : M.llbc_module) : unit =
+    (crate : Crates.llbc_crate) : unit =
   (* Translate the module to the pure AST *)
   let trans_ctx, trans_types, trans_funs =
     translate_module_to_pure config.eval_config config.mp_config
-      config.use_state m
+      config.use_state crate
   in
 
   (* Initialize the extraction context - for now we extract only to F* *)
@@ -641,7 +640,8 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
   in
   let variant_concatenate_type_name = true in
   let fstar_fmt =
-    ExtractToFStar.mk_formatter trans_ctx m.name variant_concatenate_type_name
+    ExtractToFStar.mk_formatter trans_ctx crate.name
+      variant_concatenate_type_name
   in
   let ctx =
     { PureToExtract.trans_ctx; names_map; fmt = fstar_fmt; indent_incr = 2 }
@@ -653,8 +653,9 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
     A.FunDeclId.Set.of_list
       (List.concat
          (List.map
-            (fun decl -> match decl with M.Fun (Rec ids) -> ids | _ -> [])
-            m.declarations))
+            (fun decl ->
+              match decl with Crates.Fun (Rec ids) -> ids | _ -> [])
+            crate.declarations))
   in
 
   (* Register unique names for all the top-level types, globals and functions.
@@ -686,7 +687,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
 
   let ctx =
     List.fold_left ExtractToFStar.extract_global_decl_register_names ctx
-      m.globals
+      crate.globals
   in
 
   (* Open the output file *)
@@ -746,7 +747,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
   (* Extract the file(s) *)
   let gen_ctx =
     {
-      m;
+      crate;
       extract_ctx = ctx;
       trans_types;
       trans_funs;
@@ -793,8 +794,8 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
         interface = has_opaque_types;
       }
     in
-    extract_file types_config gen_ctx types_filename m.M.name types_module
-      ": type definitions" [] [];
+    extract_file types_config gen_ctx types_filename crate.Crates.name
+      types_module ": type definitions" [] [];
 
     (* Extract the template clauses *)
     let needs_clauses_module =
@@ -807,7 +808,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
      let clauses_config =
        { base_gen_config with extract_template_decreases_clauses = true }
      in
-     extract_file clauses_config gen_ctx clauses_filename m.M.name
+     extract_file clauses_config gen_ctx clauses_filename crate.Crates.name
        clauses_module ": templates for the decreases clauses" [ types_module ]
        []);
 
@@ -825,7 +826,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
             interface = true;
           }
         in
-        extract_file opaque_config gen_ctx opaque_filename m.M.name
+        extract_file opaque_config gen_ctx opaque_filename crate.Crates.name
           opaque_module ": opaque function definitions" [] [ types_module ];
         [ opaque_module ])
       else []
@@ -844,7 +845,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
     let clauses_module =
       if needs_clauses_module then [ module_name ^ ".Clauses" ] else []
     in
-    extract_file fun_config gen_ctx fun_filename m.M.name fun_module
+    extract_file fun_config gen_ctx fun_filename crate.Crates.name fun_module
       ": function definitions" []
       ([ types_module ] @ opaque_funs_module @ clauses_module))
   else
@@ -866,5 +867,5 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
     in
     (* Add the extension for F* *)
     let extract_filename = extract_filebasename ^ ".fst" in
-    extract_file gen_config gen_ctx extract_filename m.M.name module_name "" []
-      []
+    extract_file gen_config gen_ctx extract_filename crate.Crates.name
+      module_name "" [] []
diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml
index 326bb05f..a658147d 100644
--- a/src/TranslateCore.ml
+++ b/src/TranslateCore.ml
@@ -4,7 +4,6 @@ open InterpreterStatements
 module L = Logging
 module T = Types
 module A = LlbcAst
-module M = Modules
 module SA = SymbolicAst
 module FA = FunsAnalysis
 
diff --git a/src/TypesAnalysis.ml b/src/TypesAnalysis.ml
index e84b4f58..0d23e92b 100644
--- a/src/TypesAnalysis.ml
+++ b/src/TypesAnalysis.ml
@@ -1,5 +1,5 @@
 open Types
-open Modules
+open Crates
 
 type subtype_info = {
   under_borrow : bool;  (** Are we inside a borrow? *)
diff --git a/src/main.ml b/src/main.ml
index 6b1083f5..b7868722 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -141,7 +141,7 @@ let () =
   translate_log#set_level EL.Info;
   (* Load the module *)
   let json = Yojson.Basic.from_file filename in
-  match llbc_module_of_json json with
+  match llbc_crate_of_json json with
   | Error s ->
       main_log#error "error: %s\n" s;
       exit 1
-- 
cgit v1.2.3


From aa0b10a24b8e6b8323b0741e8573ba4fc6283409 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 20 Oct 2022 21:11:57 +0200
Subject: Fix the semantics of drop

---
 src/Collections.ml           | 14 ++++++++++++++
 src/InterpreterPaths.ml      |  1 +
 src/InterpreterStatements.ml | 20 ++++++++++++++++----
 3 files changed, 31 insertions(+), 4 deletions(-)

(limited to 'src')

diff --git a/src/Collections.ml b/src/Collections.ml
index 2cb298a7..351b6523 100644
--- a/src/Collections.ml
+++ b/src/Collections.ml
@@ -184,6 +184,7 @@ module type Set = sig
 
   val pp : Format.formatter -> t -> unit
   val show : t -> string
+  val pairwise_distinct : elt list -> bool
 end
 
 module MakeSet (Ord : OrderedType) : Set with type elt = Ord.t = struct
@@ -218,6 +219,19 @@ module MakeSet (Ord : OrderedType) : Set with type elt = Ord.t = struct
     pp_string "}"
 
   let show s = to_string None s
+
+  let pairwise_distinct ls =
+    let s = ref empty in
+    let rec check ls =
+      match ls with
+      | [] -> true
+      | x :: ls' ->
+          if mem x !s then false
+          else (
+            s := add x !s;
+            check ls')
+    in
+    check ls
 end
 
 (** A map where the bindings are injective (i.e., if two keys are distinct,
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index edd27138..16ab9aad 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -771,6 +771,7 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
     
     [end_borrows]: if false, we only end the outer loans we find. If true, we
     end all the loans and the borrows we find.
+    TODO: end_borrows is not necessary anymore.
  *)
 let prepare_lplace (config : C.config) (end_borrows : bool) (p : E.place)
     (cf : V.typed_value -> m_fun) : m_fun =
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 34310ea1..ae9e59fe 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -20,20 +20,32 @@ open InterpreterExpressions
 (** The local logger *)
 let log = L.statements_log
 
-(** Drop a value at a given place *)
+(** Drop a value at a given place - TODO: factorize this with [assign_to_place] *)
 let drop_value (config : C.config) (p : E.place) : cm_fun =
  fun cf ctx ->
-  log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p));
-  (* Prepare the place (by ending the outer loans and the borrows).
+  log#ldebug
+    (lazy
+      ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Initial context:\n"
+     ^ eval_ctx_to_string ctx));
+  (* Prepare the place (by ending the outer loans).
    * Note that [prepare_lplace] will use the `Write` access kind:
    * it is ok, because when updating the value with [Bottom] below,
    * we will use the `Move` access *)
-  let end_borrows = true in
+  let end_borrows = false in
   let prepare = prepare_lplace config end_borrows p in
   (* Replace the value with [Bottom] *)
   let replace cf (v : V.typed_value) ctx =
+    (* Move the value at destination (that we will overwrite) to a dummy variable
+     * to preserve the borrows *)
+    let mv = read_place_unwrap config Write p ctx in
+    let ctx = C.ctx_push_dummy_var ctx mv in
+    (* Update the destination to ⊥ *)
     let nv = { v with value = V.Bottom } in
     let ctx = write_place_unwrap config Move p nv ctx in
+    log#ldebug
+      (lazy
+        ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n"
+       ^ eval_ctx_to_string ctx));
     cf ctx
   in
   (* Compose and apply *)
-- 
cgit v1.2.3