1 files changed, 37 insertions, 34 deletions

diff --git a/src/Print.ml b/src/Print.ml
index af6fc982..c10c5989 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -13,6 +13,7 @@ let option_to_string (to_string : 'a -> string) (x : 'a option) : string =
 
 let name_to_string (name : name) : string = Names.name_to_string name
 let fun_name_to_string (name : fun_name) : string = name_to_string name
+let global_name_to_string (name : global_name) : string = name_to_string name
 
 (** Pretty-printing for types *)
 module Types = struct
@@ -686,6 +687,7 @@ module LlbcAst = struct
     adt_field_names :
       T.TypeDeclId.id -> T.VariantId.id option -> string list option;
     fun_decl_id_to_string : A.FunDeclId.id -> string;
+    global_decl_id_to_string : A.GlobalDeclId.id -> string;
   }
 
   let ast_to_ctx_formatter (fmt : ast_formatter) : PC.ctx_formatter =
@@ -742,6 +744,10 @@ module LlbcAst = struct
       let def = C.ctx_lookup_fun_decl ctx def_id in
       fun_name_to_string def.name
     in
+    let global_decl_id_to_string def_id =
+      let def = C.ctx_lookup_global_decl ctx def_id in
+      global_name_to_string def.name
+    in
     {
       rvar_to_string = ctx_fmt.PV.rvar_to_string;
       r_to_string = ctx_fmt.PV.r_to_string;
@@ -752,10 +758,12 @@ module LlbcAst = struct
       adt_field_names = ctx_fmt.PV.adt_field_names;
       adt_field_to_string;
       fun_decl_id_to_string;
+      global_decl_id_to_string;
     }
 
   let fun_decl_to_ast_formatter (type_decls : T.type_decl T.TypeDeclId.Map.t)
-      (fun_decls : A.fun_decl A.FunDeclId.Map.t) (fdef : A.fun_decl) :
+      (fun_decls : A.fun_decl A.FunDeclId.Map.t)
+      (global_decls : A.global_decl A.GlobalDeclId.Map.t) (fdef : A.fun_decl) :
       ast_formatter =
     let rvar_to_string r =
       let rvar = T.RegionVarId.nth fdef.signature.region_params r in
@@ -784,6 +792,10 @@ module LlbcAst = struct
       let def = A.FunDeclId.Map.find def_id fun_decls in
       fun_name_to_string def.name
     in
+    let global_decl_id_to_string def_id =
+      let def = A.GlobalDeclId.Map.find def_id global_decls in
+      global_name_to_string def.name
+    in
     {
       rvar_to_string;
       r_to_string;
@@ -794,6 +806,7 @@ module LlbcAst = struct
       adt_field_names;
       adt_field_to_string;
       fun_decl_id_to_string;
+      global_decl_id_to_string;
     }
 
   let rec projection_to_string (fmt : ast_formatter) (inside : string)
@@ -859,35 +872,13 @@ module LlbcAst = struct
     | E.Shl -> "<<"
     | E.Shr -> ">>"
 
-  let rec operand_constant_value_to_string (fmt : ast_formatter)
-      (cv : E.operand_constant_value) : string =
-    match cv with
-    | E.ConstantValue cv -> PV.constant_value_to_string cv
-    | E.ConstantAdt (variant_id, field_values) ->
-        (* This is a bit annoying, because we don't have context information
-         * to convert the ADT to a value, so we do the best we can in the
-         * simplest manner. Anyway, those printing utilitites are only used
-         * for debugging, and complex constant values are not common.
-         * We might want to store type information in the operand constant values
-         * in the future.
-         *)
-        let variant_id = option_to_string T.VariantId.to_string variant_id in
-        let field_values =
-          List.map (operand_constant_value_to_string fmt) field_values
-        in
-        "ConstantAdt " ^ variant_id ^ " {"
-        ^ String.concat ", " field_values
-        ^ "}"
-
   let operand_to_string (fmt : ast_formatter) (op : E.operand) : string =
     match op with
     | E.Copy p -> "copy " ^ place_to_string fmt p
     | E.Move p -> "move " ^ place_to_string fmt p
     | E.Constant (ty, cv) ->
-        (* For clarity, we also print the typing information: see the comment in
-         * [operand_constant_value_to_string] *)
         "("
-        ^ operand_constant_value_to_string fmt cv
+        ^ PV.constant_value_to_string cv
         ^ " : "
         ^ PT.ety_to_string (ast_to_etype_formatter fmt) ty
         ^ ")"
@@ -948,6 +939,9 @@ module LlbcAst = struct
     match st with
     | A.Assign (p, rv) ->
         indent ^ place_to_string fmt p ^ " := " ^ rvalue_to_string fmt rv
+    | A.AssignGlobal { dst; global } ->
+        indent ^ fmt.var_id_to_string dst ^ " := global "
+        ^ fmt.global_decl_id_to_string global
     | A.FakeRead p -> indent ^ "fake_read " ^ place_to_string fmt p
     | A.SetDiscriminant (p, variant_id) ->
         (* TODO: improve this to lookup the variant name by using the def id *)
@@ -1138,7 +1132,8 @@ module Module = struct
   (** Generate an [ast_formatter] by using a definition context in combination
       with the variables local to a function's definition *)
   let def_ctx_to_ast_formatter (type_context : T.type_decl T.TypeDeclId.Map.t)
-      (fun_context : A.fun_decl A.FunDeclId.Map.t) (def : A.fun_decl) :
+      (fun_context : A.fun_decl A.FunDeclId.Map.t)
+      (global_context : A.global_decl A.GlobalDeclId.Map.t) (def : A.fun_decl) :
       PA.ast_formatter =
     let rvar_to_string vid =
       let var = T.RegionVarId.nth def.signature.region_params vid in
@@ -1160,6 +1155,10 @@ module Module = struct
       let def = A.FunDeclId.Map.find def_id fun_context in
       fun_name_to_string def.name
     in
+    let global_decl_id_to_string def_id =
+      let def = A.GlobalDeclId.Map.find def_id global_context in
+      global_name_to_string def.name
+    in
     let var_id_to_string vid =
       let var = V.VarId.nth (Option.get def.body).locals vid in
       PA.var_to_string var
@@ -1181,24 +1180,33 @@ module Module = struct
       var_id_to_string;
       adt_field_names;
       fun_decl_id_to_string;
+      global_decl_id_to_string;
     }
 
   (** This function pretty-prints a function definition by using a definition
       context *)
   let fun_decl_to_string (type_context : T.type_decl T.TypeDeclId.Map.t)
-      (fun_context : A.fun_decl A.FunDeclId.Map.t) (def : A.fun_decl) : string =
-    let fmt = def_ctx_to_ast_formatter type_context fun_context def in
+      (fun_context : A.fun_decl A.FunDeclId.Map.t)
+      (global_context : A.global_decl A.GlobalDeclId.Map.t) (def : A.fun_decl) :
+      string =
+    let fmt =
+      def_ctx_to_ast_formatter type_context fun_context global_context def
+    in
     PA.fun_decl_to_string fmt "" "  " def
 
   let module_to_string (m : M.llbc_module) : string =
-    let types_defs_map, funs_defs_map = M.compute_defs_maps m in
+    let types_defs_map, funs_defs_map, globals_defs_map =
+      M.compute_defs_maps m
+    in
 
     (* The types *)
     let type_decls = List.map (type_decl_to_string types_defs_map) m.M.types in
 
     (* The functions *)
     let fun_decls =
-      List.map (fun_decl_to_string types_defs_map funs_defs_map) m.M.functions
+      List.map
+        (fun_decl_to_string types_defs_map funs_defs_map globals_defs_map)
+        m.M.functions
     in
 
     (* Put everything together *)
@@ -1255,11 +1263,6 @@ module EvalCtxLlbcAst = struct
     let fmt = PC.eval_ctx_to_ctx_formatter ctx in
     PV.typed_avalue_to_string fmt v
 
-  let operand_constant_value_to_string (ctx : C.eval_ctx)
-      (cv : E.operand_constant_value) : string =
-    let fmt = PA.eval_ctx_to_ast_formatter ctx in
-    PA.operand_constant_value_to_string fmt cv
-
   let place_to_string (ctx : C.eval_ctx) (op : E.place) : string =
     let fmt = PA.eval_ctx_to_ast_formatter ctx in
     PA.place_to_string fmt op