From 9c7fe7eb0cd3fdda6b64ff4dc9f6b68f631bdb44 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 27 Oct 2022 23:57:38 +0200
Subject: Make minor updates to account for Charon's changes

---
 compiler/Contexts.ml              |  4 ++--
 compiler/Crates.ml                |  1 -
 compiler/Driver.ml                |  2 +-
 compiler/FunsAnalysis.ml          |  3 +--
 compiler/Interpreter.ml           | 15 +++++++--------
 compiler/InterpreterStatements.ml |  9 ++++-----
 compiler/PrePasses.ml             |  2 +-
 compiler/Pure.ml                  | 36 ++++++++++++++++++------------------
 compiler/Translate.ml             | 20 ++++++++++----------
 compiler/TypesAnalysis.ml         |  6 +++---
 compiler/dune                     |  1 -
 11 files changed, 47 insertions(+), 52 deletions(-)
 delete mode 100644 compiler/Crates.ml

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 52815859..2d5fd907 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -210,7 +210,7 @@ let config_of_partial (mode : interpreter_mode) (config : partial_config) :
   }
 
 type type_context = {
-  type_decls_groups : Crates.type_declaration_group TypeDeclId.Map.t;
+  type_decls_groups : type_declaration_group TypeDeclId.Map.t;
   type_decls : type_decl TypeDeclId.Map.t;
   type_infos : TypesAnalysis.type_infos;
 }
@@ -391,7 +391,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 Crates.Rec _ -> true | Crates.NonRec _ -> false
+  match decl_group with Rec _ -> true | NonRec _ -> false
 
 (** Visitor to iterate over the values in the *current* frame *)
 class ['self] iter_frame =
diff --git a/compiler/Crates.ml b/compiler/Crates.ml
deleted file mode 100644
index 81f42cea..00000000
--- a/compiler/Crates.ml
+++ /dev/null
@@ -1 +0,0 @@
-include Charon.Crates
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index ae9d238a..c8a1fef4 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -148,7 +148,7 @@ let () =
 
   (* Load the module *)
   let json = Yojson.Basic.from_file filename in
-  match llbc_crate_of_json json with
+  match crate_of_json json with
   | Error s ->
       main_log#error "error: %s\n" s;
       exit 1
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index 39f85581..59373985 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -8,7 +8,6 @@
  *)
 
 open LlbcAst
-open Crates
 module EU = ExpressionsUtils
 
 (** Various information about a function.
@@ -26,7 +25,7 @@ type fun_info = {
 (** Various information about a module's functions *)
 type modules_funs_info = fun_info FunDeclId.Map.t
 
-let analyze_module (m : llbc_crate) (funs_map : fun_decl FunDeclId.Map.t)
+let analyze_module (m : 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/compiler/Interpreter.ml b/compiler/Interpreter.ml
index f93a0ae1..f92473f7 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -12,12 +12,12 @@ module SA = SymbolicAst
 (** The local logger *)
 let log = L.interpreter_log
 
-let compute_type_fun_global_contexts (m : Crates.llbc_crate) :
+let compute_type_fun_global_contexts (m : A.crate) :
     C.type_context * C.fun_context * C.global_context =
-  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_list, _, _ = split_declarations m.declarations in
+  let type_decls, fun_decls, global_decls = compute_defs_maps m in
   let type_decls_groups, _funs_defs_groups, _globals_defs_groups =
-    Crates.split_declarations_to_group_maps m.declarations
+    split_declarations_to_group_maps m.declarations
   in
   let type_infos =
     TypesAnalysis.analyze_type_declarations type_decls type_decls_list
@@ -276,7 +276,7 @@ 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) (crate : Crates.llbc_crate)
+  let test_unit_function (config : C.partial_config) (crate : A.crate)
       (fid : A.FunDeclId.id) : unit =
     (* Retrieve the function declaration *)
     let fdef = A.FunDeclId.nth crate.functions fid in
@@ -331,8 +331,7 @@ 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)
-      (crate : Crates.llbc_crate) : unit =
+  let test_unit_functions (config : C.partial_config) (crate : A.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 crate def.A.def_id
@@ -373,7 +372,7 @@ module Test = struct
       they are not supported by the symbolic interpreter.
    *)
   let test_functions_symbolic (config : C.partial_config) (synthesize : bool)
-      (crate : Crates.llbc_crate) : unit =
+      (crate : A.crate) : unit =
     (* Filter the functions which contain loops *)
     let no_loop_funs =
       List.filter
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 56ab05f3..fc3b0975 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -922,15 +922,14 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
   (* Compose and apply *)
   comp cc cf_eval_st cf ctx
 
-and eval_global (config : C.config) (dest : E.VarId.id)
-    (gid : LA.GlobalDeclId.id) : st_cm_fun =
+and eval_global (config : C.config) (dest : E.place) (gid : LA.GlobalDeclId.id)
+    : st_cm_fun =
  fun cf ctx ->
   let global = C.ctx_lookup_global_decl ctx gid in
-  let place = { E.var_id = dest; projection = [] } in
   match config.mode with
   | ConcreteMode ->
       (* Treat the evaluation of the global as a call to the global body (without arguments) *)
-      (eval_local_function_call_concrete config global.body_id [] [] [] place)
+      (eval_local_function_call_concrete config global.body_id [] [] [] dest)
         cf ctx
   | SymbolicMode ->
       (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
@@ -939,7 +938,7 @@ and eval_global (config : C.config) (dest : E.VarId.id)
         mk_fresh_symbolic_value V.Global (ety_no_regions_to_rty global.ty)
       in
       let cc =
-        assign_to_place config (mk_typed_value_from_symbolic_value sval) place
+        assign_to_place config (mk_typed_value_from_symbolic_value sval) dest
       in
       let e = cc (cf Unit) ctx in
       S.synthesize_global_eval gid sval e
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index a09ae476..8f1354b7 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -49,6 +49,6 @@ let filter_drop_assigns (f : A.fun_decl) : A.fun_decl =
   in
   { f with body }
 
-let apply_passes (m : Crates.llbc_crate) : Crates.llbc_crate =
+let apply_passes (m : A.crate) : A.crate =
   let functions = List.map filter_drop_assigns m.functions in
   { m with functions }
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index f9c693c6..7f71cf7f 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -48,7 +48,7 @@ let option_none_id = T.option_none_id
 type type_id = AdtId of TypeDeclId.id | Tuple | Assumed of assumed_ty
 [@@deriving show, ord]
 
-(** Ancestor for iter visitor for [ty] *)
+(** Ancestor for iter visitor for {!ty} *)
 class ['self] iter_ty_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.iter
@@ -57,7 +57,7 @@ class ['self] iter_ty_base =
     method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> ()
   end
 
-(** Ancestor for map visitor for [ty] *)
+(** Ancestor for map visitor for {!ty} *)
 class ['self] map_ty_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.map
@@ -164,8 +164,8 @@ type mplace = {
 
 type variant_id = VariantId.id [@@deriving show]
 
-(** Ancestor for [iter_pat_var_or_dummy] visitor *)
-class ['self] iter_value_base =
+(** Ancestor for {!iter_typed_pattern} visitor *)
+class ['self] iter_typed_pattern_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.iter
 
@@ -178,8 +178,8 @@ class ['self] iter_value_base =
     method visit_variant_id : 'env -> variant_id -> unit = fun _ _ -> ()
   end
 
-(** Ancestor for [map_typed_rvalue] visitor *)
-class ['self] map_value_base =
+(** Ancestor for {!map_typed_pattern} visitor *)
+class ['self] map_typed_pattern_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.map
 
@@ -192,8 +192,8 @@ class ['self] map_value_base =
     method visit_variant_id : 'env -> variant_id -> variant_id = fun _ x -> x
   end
 
-(** Ancestor for [reduce_typed_rvalue] visitor *)
-class virtual ['self] reduce_value_base =
+(** Ancestor for {!reduce_typed_pattern} visitor *)
+class virtual ['self] reduce_typed_pattern_base =
   object (self : 'self)
     inherit [_] VisitorsRuntime.reduce
 
@@ -206,8 +206,8 @@ class virtual ['self] reduce_value_base =
     method visit_variant_id : 'env -> variant_id -> 'a = fun _ _ -> self#zero
   end
 
-(** Ancestor for [mapreduce_typed_rvalue] visitor *)
-class virtual ['self] mapreduce_value_base =
+(** Ancestor for {!mapreduce_typed_pattern} visitor *)
+class virtual ['self] mapreduce_typed_pattern_base =
   object (self : 'self)
     inherit [_] VisitorsRuntime.mapreduce
 
@@ -247,7 +247,7 @@ and typed_pattern = { value : pattern; ty : ty }
       {
         name = "iter_typed_pattern";
         variety = "iter";
-        ancestors = [ "iter_value_base" ];
+        ancestors = [ "iter_typed_pattern_base" ];
         nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
         polymorphic = false;
@@ -256,7 +256,7 @@ and typed_pattern = { value : pattern; ty : ty }
       {
         name = "map_typed_pattern";
         variety = "map";
-        ancestors = [ "map_value_base" ];
+        ancestors = [ "map_typed_pattern_base" ];
         nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
         polymorphic = false;
@@ -265,7 +265,7 @@ and typed_pattern = { value : pattern; ty : ty }
       {
         name = "reduce_typed_pattern";
         variety = "reduce";
-        ancestors = [ "reduce_value_base" ];
+        ancestors = [ "reduce_typed_pattern_base" ];
         nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         polymorphic = false;
       },
@@ -273,7 +273,7 @@ and typed_pattern = { value : pattern; ty : ty }
       {
         name = "mapreduce_typed_pattern";
         variety = "mapreduce";
-        ancestors = [ "mapreduce_value_base" ];
+        ancestors = [ "mapreduce_typed_pattern_base" ];
         nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         polymorphic = false;
       }]
@@ -323,7 +323,7 @@ type qualif = { id : qualif_id; type_args : ty list } [@@deriving show]
 
 type var_id = VarId.id [@@deriving show]
 
-(** Ancestor for [iter_expression] visitor *)
+(** Ancestor for {!iter_expression} visitor *)
 class ['self] iter_expression_base =
   object (_self : 'self)
     inherit [_] iter_typed_pattern
@@ -332,7 +332,7 @@ class ['self] iter_expression_base =
     method visit_qualif : 'env -> qualif -> unit = fun _ _ -> ()
   end
 
-(** Ancestor for [map_expression] visitor *)
+(** Ancestor for {!map_expression} visitor *)
 class ['self] map_expression_base =
   object (_self : 'self)
     inherit [_] map_typed_pattern
@@ -344,7 +344,7 @@ class ['self] map_expression_base =
     method visit_qualif : 'env -> qualif -> qualif = fun _ x -> x
   end
 
-(** Ancestor for [reduce_expression] visitor *)
+(** Ancestor for {!reduce_expression} visitor *)
 class virtual ['self] reduce_expression_base =
   object (self : 'self)
     inherit [_] reduce_typed_pattern
@@ -356,7 +356,7 @@ class virtual ['self] reduce_expression_base =
     method visit_qualif : 'env -> qualif -> 'a = fun _ _ -> self#zero
   end
 
-(** Ancestor for [mapreduce_expression] visitor *)
+(** Ancestor for {!mapreduce_expression} visitor *)
 class virtual ['self] mapreduce_expression_base =
   object (self : 'self)
     inherit [_] mapreduce_typed_pattern
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 8f3b94c4..35633d29 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -285,7 +285,7 @@ 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) (crate : Crates.llbc_crate) :
+    (mp_config : Micro.config) (use_state : bool) (crate : A.crate) :
     trans_ctx * Pure.type_decl list * (bool * pure_fun_translation) list =
   (* Debug *)
   log#ldebug (lazy "translate_module_to_pure");
@@ -357,7 +357,7 @@ let translate_module_to_pure (config : C.partial_config)
 
 (** Extraction context *)
 type gen_ctx = {
-  crate : Crates.llbc_crate;
+  crate : A.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;
@@ -533,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 : Crates.declaration_group) : unit =
+  let export_decl (decl : A.declaration_group) : unit =
     match decl with
     | Type (NonRec id) ->
         if config.extract_types then export_type ExtractToFStar.Type id
@@ -627,7 +627,7 @@ 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)
-    (crate : Crates.llbc_crate) : unit =
+    (crate : A.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
@@ -654,7 +654,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
       (List.concat
          (List.map
             (fun decl ->
-              match decl with Crates.Fun (Rec ids) -> ids | _ -> [])
+              match decl with A.Fun (Rec ids) -> ids | _ -> [])
             crate.declarations))
   in
 
@@ -794,7 +794,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
         interface = has_opaque_types;
       }
     in
-    extract_file types_config gen_ctx types_filename crate.Crates.name
+    extract_file types_config gen_ctx types_filename crate.A.name
       types_module ": type definitions" [] [];
 
     (* Extract the template clauses *)
@@ -808,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 crate.Crates.name
+     extract_file clauses_config gen_ctx clauses_filename crate.A.name
        clauses_module ": templates for the decreases clauses" [ types_module ]
        []);
 
@@ -826,7 +826,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
             interface = true;
           }
         in
-        extract_file opaque_config gen_ctx opaque_filename crate.Crates.name
+        extract_file opaque_config gen_ctx opaque_filename crate.A.name
           opaque_module ": opaque function definitions" [] [ types_module ];
         [ opaque_module ])
       else []
@@ -845,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 crate.Crates.name fun_module
+    extract_file fun_config gen_ctx fun_filename crate.A.name fun_module
       ": function definitions" []
       ([ types_module ] @ opaque_funs_module @ clauses_module))
   else
@@ -867,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 crate.Crates.name
+    extract_file gen_config gen_ctx extract_filename crate.A.name
       module_name "" [] []
diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
index 60ce5149..db6d3b98 100644
--- a/compiler/TypesAnalysis.ml
+++ b/compiler/TypesAnalysis.ml
@@ -1,5 +1,5 @@
 open Types
-open Crates
+module A = LlbcAst
 
 type subtype_info = {
   under_borrow : bool;  (** Are we inside a borrow? *)
@@ -275,7 +275,7 @@ let analyze_type_decl (updated : bool ref) (infos : type_infos)
     infos
 
 let analyze_type_declaration_group (type_decls : type_decl TypeDeclId.Map.t)
-    (infos : type_infos) (decl : type_declaration_group) : type_infos =
+    (infos : type_infos) (decl : A.type_declaration_group) : type_infos =
   (* Collect the identifiers used in the declaration group *)
   let ids = match decl with NonRec id -> [ id ] | Rec ids -> ids in
   (* Retrieve the type definitions *)
@@ -309,7 +309,7 @@ let analyze_type_declaration_group (type_decls : type_decl TypeDeclId.Map.t)
     Rk.: pay attention to the difference between type definitions and types!
  *)
 let analyze_type_declarations (type_decls : type_decl TypeDeclId.Map.t)
-    (decls : type_declaration_group list) : type_infos =
+    (decls : A.type_declaration_group list) : type_infos =
   List.fold_left
     (fun infos decl -> analyze_type_declaration_group type_decls infos decl)
     TypeDeclId.Map.empty decls
diff --git a/compiler/dune b/compiler/dune
index af4cdb08..0d340d59 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -17,7 +17,6 @@
   ConstStrings
   Contexts
   Cps
-  Crates
   Expressions
   ExpressionsUtils
   ExtractToFStar
-- 
cgit v1.2.3