Apply minor changes from PR comments

5 files changed, 23 insertions, 17 deletions

diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml
index 034575c0..427175de 100644
--- a/src/FunsAnalysis.ml
+++ b/src/FunsAnalysis.ml
@@ -56,12 +56,6 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
           inherit [_] iter_statement as super
 
           method may_fail b =
-            (* The fail flag is disabled for globals : the global body is
-             * normalised into its declaration, which is always successful.
-             * (we check that it is successful in the extracted code: if it is
-             *  not, it leads to a type-checking error in the generated files)
-             *)
-            if f.is_global_body then () else
             can_fail := !can_fail || b
 
           method! visit_Assert env a =
@@ -104,11 +98,10 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
           (* Opaque function *)
           obj#may_fail true;
           stateful := use_state
-      | Some body -> obj#visit_statement () body.body);
+      | Some body -> obj#visit_statement () body.body)
       (* We ignore on purpose functions that cannot fail: the result of the analysis
        * is not used yet to adjust the translation so that the functions which
        * syntactically can't fail don't use an error monad. *)
-      can_fail := not f.is_global_body
     in
     List.iter visit_fun d;
     { can_fail = !can_fail; stateful = !stateful; divergent = !divergent }
diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml
index aa9b0665..94566f9b 100644
--- a/src/LlbcAst.ml
+++ b/src/LlbcAst.ml
@@ -37,7 +37,7 @@ type assumed_fun_id =
 type fun_id = Regular of FunDeclId.id | Assumed of assumed_fun_id
 [@@deriving show, ord]
 
-type assign_global = {
+type global_assignment = {
   dst : VarId.id;
   global : GlobalDeclId.id;
 }
@@ -84,7 +84,7 @@ class ['self] iter_statement_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.iter
 
-    method visit_assign_global : 'env -> assign_global -> unit = fun _ _ -> ()
+    method visit_global_assignment : 'env -> global_assignment -> unit = fun _ _ -> ()
 
     method visit_place : 'env -> place -> unit = fun _ _ -> ()
 
@@ -108,7 +108,7 @@ class ['self] map_statement_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.map
 
-    method visit_assign_global : 'env -> assign_global -> assign_global = fun _ x -> x
+    method visit_global_assignment : 'env -> global_assignment -> global_assignment = fun _ x -> x
 
     method visit_place : 'env -> place -> place = fun _ x -> x
 
@@ -131,7 +131,7 @@ class ['self] map_statement_base =
 
 type statement =
   | Assign of place * rvalue
-  | AssignGlobal of assign_global
+  | AssignGlobal of global_assignment
   | FakeRead of place
   | SetDiscriminant of place * VariantId.id
   | Drop of place
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 7a10bb6b..2d76f348 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -671,7 +671,7 @@ let compute_type_decl_name (fmt : formatter) (def : type_decl) : string =
     TODO: move all those helpers.
 *)
 let default_fun_suffix
-    (is_global : bool)
+    (is_global_body : bool)
     (num_region_groups : int)
     (rg : region_group_info option)
     ((keep_fwd, num_backs) : bool * int)
@@ -691,7 +691,7 @@ let default_fun_suffix
      we could not add the "_fwd" suffix) to prevent name clashes between
      definitions (in particular between type and function definitions).
   *)
-  if is_global then "_c" else
+  if is_global_body then "_body" else
   match rg with
   | None -> "_fwd"
   | Some rg ->
diff --git a/src/PureTypeCheck.ml b/src/PureTypeCheck.ml
index 90b9ab09..c63814eb 100644
--- a/src/PureTypeCheck.ml
+++ b/src/PureTypeCheck.ml
@@ -40,6 +40,7 @@ let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
 
 type tc_ctx = {
   type_decls : type_decl TypeDeclId.Map.t;  (** The type declarations *)
+  global_decls : A.global_decl A.GlobalDeclId.Map.t;  (** The global declarations *)
   env : ty VarId.Map.t;  (** Environment from variables to types *)
 }
 
@@ -111,7 +112,11 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
       check_texpression ctx body
   | Qualif qualif -> (
       match qualif.id with
-      | Func _ | Global _ -> () (* TODO *)
+      | Func _ -> () (* TODO *)
+      | Global id ->
+        let global = A.GlobalDeclId.Map.find id ctx.global_decls in
+        (* TODO: something like assert (global.ty = e.ty) *)
+        failwith "PureTypeCheck.ml:118"
       | Proj { adt_id = proj_adt_id; field_id } ->
           (* Note we can only project fields of structures (not enumerations) *)
           (* Deconstruct the projector type *)
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 7d9e2906..83cce3e9 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -127,13 +127,21 @@ type bs_ctx = {
 
 let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit =
   let env = VarId.Map.empty in
-  let ctx = { PureTypeCheck.type_decls = ctx.type_context.type_decls; env } in
+  let ctx = {
+    PureTypeCheck.type_decls = ctx.type_context.type_decls; 
+    global_decls = ctx.global_context.llbc_global_decls;
+    env
+  } in
   let _ = PureTypeCheck.check_typed_pattern ctx v in
   ()
 
 let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit =
   let env = VarId.Map.empty in
-  let ctx = { PureTypeCheck.type_decls = ctx.type_context.type_decls; env } in
+  let ctx = {
+    PureTypeCheck.type_decls = ctx.type_context.type_decls;
+    global_decls = ctx.global_context.llbc_global_decls;
+    env
+  } in
   PureTypeCheck.check_texpression ctx e
 
 (* TODO: move *)