Take care of some TODOs

10 files changed, 10 insertions, 12 deletions

diff --git a/compiler/Errors.ml b/compiler/Errors.ml
deleted file mode 100644
index 58dd3a0b..00000000
--- a/compiler/Errors.ml
+++ /dev/null
@@ -1 +0,0 @@
-include Charon.Errors
diff --git a/compiler/ExtractToFStar.ml b/compiler/ExtractToFStar.ml
index b44b8f25..7267101c 100644
--- a/compiler/ExtractToFStar.ml
+++ b/compiler/ExtractToFStar.ml
@@ -1,6 +1,6 @@
 (** Extract to F* *)
 
-open Errors
+open Utils
 open Pure
 open PureUtils
 open TranslateCore
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 7f51c5b9..f93a0ae1 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -137,7 +137,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return
    * will end - this will allow us to, first, mark the other return
    * regions as non-endable, and, second, end those parent regions in
    * proper order. *)
-  let parent_rgs = list_parent_region_groups sg back_id in
+  let parent_rgs = list_ancestor_region_groups sg back_id in
   let parent_input_abs_ids =
     T.RegionGroupId.mapi
       (fun rg_id rg ->
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 16f68d9e..e2d2bb0a 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -442,7 +442,7 @@ let give_back_symbolic_value (_config : C.config)
   (* Substitution function, to replace the borrow projectors over symbolic values *)
   let subst (_abs : V.abs) local_given_back =
     (* See the below comments: there is something wrong here *)
-    let _ = raise Errors.Unimplemented in
+    let _ = raise Utils.Unimplemented in
     (* Compute the projection over the given back value *)
     let child_proj =
       match nsv.sv_kind with
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 9a944428..cd6df2b0 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -712,7 +712,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
         | T.Adt (Assumed (Vec | Option), _, _) ->
             (* We can't expand those *)
             raise (Failure "Attempted to greedily expand a Vec or an Option ")
-        | T.Array _ -> raise Errors.Unimplemented
+        | T.Array _ -> raise Utils.Unimplemented
         | T.Slice _ -> raise (Failure "Can't expand symbolic slices")
         | T.TypeVar _ | Bool | Char | Never | Integer _ | Str ->
             raise (Failure "Unreachable")
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 83cdfc9b..5a6947b0 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -4,7 +4,7 @@ module V = Values
 module LA = LlbcAst
 open Scalars
 module E = Expressions
-open Errors
+open Utils
 module C = Contexts
 module Subst = Substitute
 module L = Logging
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 308f561c..56ab05f3 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -10,7 +10,7 @@ open TypesUtils
 open ValuesUtils
 module Inv = Invariants
 module S = SynthesizeSymbolic
-open Errors
+open Utils
 open Cps
 open InterpreterUtils
 open InterpreterProjectors
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 81879883..9899cfcf 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -707,7 +707,7 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx)
                   in
                   (* Compute the set of ancestors of the function in call1 *)
                   let call1_ancestors =
-                    LlbcAstUtils.list_parent_region_groups sg rg_id1
+                    LlbcAstUtils.list_ancestor_region_groups sg rg_id1
                   in
                   (* Check if the function used in call0 is inside *)
                   T.RegionGroupId.Set.mem rg_id0 call1_ancestors
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index f393b059..1341bccc 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1,4 +1,4 @@
-open Errors
+open Utils
 open LlbcAstUtils
 open Pure
 open PureUtils
@@ -525,7 +525,7 @@ let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t)
     match bid with
     | None -> (None, T.RegionGroupId.Set.empty)
     | Some bid ->
-        let parents = list_parent_region_groups sg bid in
+        let parents = list_ancestor_region_groups sg bid in
         (Some bid, parents)
   in
   (* List the inputs for:
@@ -1721,7 +1721,7 @@ let translate_fun_decl (config : config) (ctx : bs_ctx)
           | None -> []
           | Some back_id ->
               let parents_ids =
-                list_ordered_parent_region_groups def.signature back_id
+                list_ordered_ancestor_region_groups def.signature back_id
               in
               let backward_ids = List.append parents_ids [ back_id ] in
               List.concat
diff --git a/compiler/dune b/compiler/dune
index d3f5eaec..af4cdb08 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -18,7 +18,6 @@
   Contexts
   Cps
   Crates
-  Errors
   Expressions
   ExpressionsUtils
   ExtractToFStar